Correctness of the actual attained-prefix scan

The only query hypotheses are the source interface's legal-prefix clauses. The returned witness proves the next call is legal. Honest outputs pass all stages, while arbitrary malformed or unattainable claims may be rejected.

theorem MIPRE.Introspection.AuxiliaryScan.earlier_attained {n ℓ : ℕ} {P : CL.CLFun CL.𝔽₂ (Fin n) ℓ} {T : Finset (Fin n)} (hP : P.SupportedOn T) {j k : ℕ} (hj : j ≤ k) (y x : Fin n → CL.𝔽₂) (hx : (CL.CLFun.truncate k P).eval x = P.outputPrefix k y) : (CL.CLFun.truncate j P).eval x = P.outputPrefix j y

theorem MIPRE.Introspection.AuxiliaryScan.stage_of_attained_next {n ℓ : ℕ} {P : CL.CLFun CL.𝔽₂ (Fin n) ℓ} {T : Finset (Fin n)} (hP : P.SupportedOn T) (k : ℕ) (y x : Fin n → CL.𝔽₂) (hx : (CL.CLFun.truncate (k + 1) P).eval x = P.outputPrefix (k + 1) y) : (P.mapOfPrefix k (P.outputPrefix k y)) x = (CL.proj (P.factorOfPrefix k y)) y

def MIPRE.Introspection.AuxiliaryScan.QueriesCorrectAt {n ℓ : ℕ} (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) (P : CL.CLFun CL.𝔽₂ (Fin n) ℓ) (k : ℕ) : Prop

Equations

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

theorem MIPRE.Introspection.AuxiliaryScan.stage_at_claimed {n ℓ : ℕ} (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {P : CL.CLFun CL.𝔽₂ (Fin n) ℓ} {T : Finset (Fin n)} (hP : P.SupportedOn T) (k : ℕ) (y x : Fin n → CL.𝔽₂) (hx : (CL.CLFun.truncate k P).eval x = P.outputPrefix k y) (hq : QueriesCorrectAt f m ctx P k) : (stage f m).toFun (contextAt ctx (k + 1) (CL.toBits (P.outputPrefix k y)), CL.toBits y, CL.toBits x) = have v := (CL.proj (P.factorOfPrefix k y)) y; have L := P.mapOfPrefix k (P.outputPrefix k y); have z := AuxiliaryPrefix.solveStage L v; (decide (L z = v), CL.toBits (P.outputPrefix (k + 1) y), CL.toBits (AuxiliaryPrefix.replaceSeed P k (P.outputPrefix k y) x z))

theorem MIPRE.Introspection.AuxiliaryScan.program_sound {n ℓ : ℕ} (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {P : CL.CLFun CL.𝔽₂ (Fin n) ℓ} {T : Finset (Fin n)} (hP : P.SupportedOn T) (y : Fin n → CL.𝔽₂) (k : ℕ) (hq : ∀ j < k, QueriesCorrectAt f m ctx P j) (hok : ((program f m k).toFun (ctx, CL.toBits y)).1 = true) : ∃ (x : Fin n → CL.𝔽₂), (program f m k).toFun (ctx, CL.toBits y) = (true, CL.toBits (P.outputPrefix k y), CL.toBits x) ∧ (CL.CLFun.truncate k P).eval x = P.outputPrefix k y

A successful scan gives both the claimed prefix and a seed witnessing it.

theorem MIPRE.Introspection.AuxiliaryScan.program_complete {n ℓ : ℕ} (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {P : CL.CLFun CL.𝔽₂ (Fin n) ℓ} {T : Finset (Fin n)} (hP : P.SupportedOn T) (y : Fin n → CL.𝔽₂) (k : ℕ) (hq : ∀ j < k, QueriesCorrectAt f m ctx P j) (ha : ∃ (x : Fin n → CL.𝔽₂), (CL.CLFun.truncate k P).eval x = P.outputPrefix k y) : ((program f m k).toFun (ctx, CL.toBits y)).1 = true

Hiding answers only need the prefix requested at their own level to be attainable; the unvisited components are unrestricted.