Witness-preserving attainable-prefix extension

A source sampler only promises correct linear and factor queries on attained prefixes. The next witness is obtained by binary Gaussian elimination and replacing only the fresh register in the preceding witness. This preserves all earlier outputs and avoids enumerating the exponentially larger seed set.

theorem MIPRE.Introspection.AuxiliaryPrefix.mapOfPrefix_outputPrefix {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) : P.mapOfPrefix k (P.outputPrefix k y) = P.mapOfPrefix k y

theorem MIPRE.Introspection.AuxiliaryPrefix.outputPrefix_step {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y : ι → F) : P.outputPrefix (k + 1) y = P.outputPrefix k y + (CL.proj (P.factorOfPrefix k y)) y

def MIPRE.Introspection.AuxiliaryPrefix.replaceSeed {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} (P : CL.CLFun F ι ℓ) (k : ℕ) (u x z : ι → F) : ι → F

Retain the old seed outside the fresh register and insert a solved seed there.

Equations

• MIPRE.Introspection.AuxiliaryPrefix.replaceSeed P k u x z = (MIPRE.CL.proj (P.factorOfPrefix k u)ᶜ) x + (MIPRE.CL.proj (P.factorOfPrefix k u)) z

theorem MIPRE.Introspection.AuxiliaryPrefix.replaceSeed_old {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (u x z : ι → F) (hx : (CL.CLFun.truncate k P).eval x = u) : (CL.CLFun.truncate k P).eval (replaceSeed P k u x z) = u

theorem MIPRE.Introspection.AuxiliaryPrefix.replaceSeed_next {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (u x z : ι → F) (hx : (CL.CLFun.truncate k P).eval x = u) : (CL.CLFun.truncate (k + 1) P).eval (replaceSeed P k u x z) = u + (P.mapOfPrefix k u) z

theorem MIPRE.Introspection.AuxiliaryPrefix.extend_claimed {F : Type u_1} {ι : Type u_2} [Field F] [Fintype ι] [DecidableEq ι] {ℓ : ℕ} {P : CL.CLFun F ι ℓ} {T : Finset ι} (hP : P.SupportedOn T) (k : ℕ) (y x z : ι → F) (hx : (CL.CLFun.truncate k P).eval x = P.outputPrefix k y) (hz : (P.mapOfPrefix k (P.outputPrefix k y)) z = (CL.proj (P.factorOfPrefix k y)) y) : (CL.CLFun.truncate (k + 1) P).eval (replaceSeed P k (P.outputPrefix k y) x z) = P.outputPrefix (k + 1) y

A consistent stage equation extends a legal prefix using only a linear solve.

noncomputable def MIPRE.Introspection.AuxiliaryPrefix.solveStage {n : ℕ} (L : (Fin n → CL.𝔽₂) →ₗ[CL.𝔽₂] Fin n → CL.𝔽₂) (v : Fin n → CL.𝔽₂) : Fin n → CL.𝔽₂

The concrete polynomial-time matrix solver applied to the queried stage matrix.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.Introspection.AuxiliaryPrefix.solveStage_correct {n : ℕ} (L : (Fin n → CL.𝔽₂) →ₗ[CL.𝔽₂] Fin n → CL.𝔽₂) (v : Fin n → CL.𝔽₂) (hv : ∃ (x : Fin n → CL.𝔽₂), L x = v) : L (solveStage L v) = v