Executable boundary edges of the hiding chain

The first edge compares the initial dual quotient and untouched tail. The last edge scans both reported prefixes, then compares those prefixes and the full dual answers. Query functions are parameters so the same programs use the proved padded-source interface.

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryBoundary.FirstInput : Type

Equations

• MIPRE.Introspection.AuxiliaryBoundary.FirstInput = (MIPRE.Introspection.AuxiliarySource.Context × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr × MIPRE.Cost.BitStr)

noncomputable def MIPRE.Introspection.AuxiliaryBoundary.firstContext : Cost.PolyTimeFun FirstInput AuxiliarySource.Context

Equations

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

theorem MIPRE.Introspection.AuxiliaryBoundary.firstContext_apply (ctx : AuxiliarySource.Context) (x a b c : Cost.BitStr) : firstContext.toFun (ctx, x, a, b, c) = AuxiliaryScan.contextAt ctx 1 (AuxiliaryScan.zeros.toFun x)

noncomputable def MIPRE.Introspection.AuxiliaryBoundary.first (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) : Cost.PolyTimeFun FirstInput Bool

Equations

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

theorem MIPRE.Introspection.AuxiliaryBoundary.first_correct (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {n ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin n) ℓ) (x a b c : Fin n → CL.𝔽₂) (hf : f.toFun (AuxiliaryScan.contextAt ctx 1 (CL.toBits 0)) = CL.indicatorBits (P.factorOfPrefix 0 0)) (hm : m.toFun (AuxiliaryScan.contextAt ctx 1 (CL.toBits 0)) = LowDegree.BinaryLinear.matrixBits (LinearMap.toMatrix' (P.mapOfPrefix 0 0))) : (first f m).toFun (ctx, CL.toBits x, CL.toBits a, CL.toBits b, CL.toBits c) = true ↔ AuxiliaryQuotient.hidingPauli P x (a, b, c)

theorem MIPRE.Introspection.AuxiliaryBoundary.first_correct_of_queries (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {n ℓ : ℕ} (P : CL.CLFun CL.𝔽₂ (Fin n) ℓ) (x a b c : Fin n → CL.𝔽₂) (hq : AuxiliaryScan.QueriesCorrectAt f m ctx P 0) : (first f m).toFun (ctx, CL.toBits x, CL.toBits a, CL.toBits b, CL.toBits c) = true ↔ AuxiliaryQuotient.hidingPauli P x (a, b, c)

@[reducible, inline]

abbrev MIPRE.Introspection.AuxiliaryBoundary.LastInput : Type

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryBoundary.leftScan (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ℓ : ℕ) : Cost.PolyTimeFun LastInput AuxiliaryScan.State

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryBoundary.rightScan (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ℓ : ℕ) : Cost.PolyTimeFun LastInput AuxiliaryScan.State

Equations

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

noncomputable def MIPRE.Introspection.AuxiliaryBoundary.last (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ℓ : ℕ) : Cost.PolyTimeFun LastInput Bool

Equations

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

theorem MIPRE.Introspection.AuxiliaryBoundary.last_apply_iff (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ℓ : ℕ) (ctx : AuxiliarySource.Context) (a b c v d : Cost.BitStr) : (last f m ℓ).toFun (ctx, (a, b, c), v, d) = true ↔ ((AuxiliaryScan.program f m (ℓ - 1)).toFun (ctx, a)).1 = true ∧ ((AuxiliaryScan.program f m (ℓ - 1)).toFun (ctx, v)).1 = true ∧ ((AuxiliaryScan.program f m (ℓ - 1)).toFun (ctx, a)).2.1 = ((AuxiliaryScan.program f m (ℓ - 1)).toFun (ctx, v)).2.1 ∧ b = d

theorem MIPRE.Introspection.AuxiliaryBoundary.last_correct (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (ctx : AuxiliarySource.Context) {n ℓ : ℕ} {P : CL.CLFun CL.𝔽₂ (Fin n) ℓ} {T : Finset (Fin n)} (hP : P.SupportedOn T) (a b c v d : Fin n → CL.𝔽₂) (hq : ∀ j < ℓ - 1, AuxiliaryScan.QueriesCorrectAt f m ctx P j) : (last f m ℓ).toFun (ctx, (CL.toBits a, CL.toBits b, CL.toBits c), CL.toBits v, CL.toBits d) = true ↔ (∃ (x : Fin n → CL.𝔽₂), (CL.CLFun.truncate (ℓ - 1) P).eval x = P.outputPrefix (ℓ - 1) a) ∧ (∃ (x : Fin n → CL.𝔽₂), (CL.CLFun.truncate (ℓ - 1) P).eval x = P.outputPrefix (ℓ - 1) v) ∧ CLChecks.hidingRead P (a, b, c) (v, d, ())