Executable adaptive register masks from legal source queries

noncomputable def MIPRE.Introspection.AuxiliaryScan.unionMask : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

Equations

• MIPRE.Introspection.AuxiliaryScan.unionMask = (MIPRE.Cost.PolyTimeFun.fst.ite (MIPRE.Cost.PolyTimeFun.const true) MIPRE.Cost.PolyTimeFun.snd).map.comp MIPRE.Cost.PolyTimeFun.zip

theorem MIPRE.Introspection.AuxiliaryScan.unionMask_correct {n : ℕ} (S T : Finset (Fin n)) : unionMask.toFun (CL.indicatorBits S, CL.indicatorBits T) = CL.indicatorBits (S ∪ T)

noncomputable def MIPRE.Introspection.AuxiliaryScan.factorAt (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) (k : ℕ) : Cost.PolyTimeFun Input Cost.BitStr

Equations

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

def MIPRE.Introspection.AuxiliaryScan.registers (f : Cost.PolyTimeFun AuxiliarySource.Context Cost.BitStr) (m : Cost.PolyTimeFun AuxiliarySource.Context (List Cost.BitStr)) : ℕ → Cost.PolyTimeFun Input Cost.BitStr

Equations

• One or more equations did not get rendered due to their size.
• MIPRE.Introspection.AuxiliaryScan.registers f m 0 = MIPRE.Introspection.AuxiliaryScan.zeros.comp MIPRE.Cost.PolyTimeFun.snd

theorem MIPRE.Introspection.AuxiliaryScan.factorAt_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) (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) : (factorAt f m k).toFun (ctx, CL.toBits y) = CL.indicatorBits (P.factorOfPrefix k y)

theorem MIPRE.Introspection.AuxiliaryScan.registers_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) (y : Fin n → CL.𝔽₂) (k : ℕ) (hq : ∀ j < k, QueriesCorrectAt f m ctx P j) (ha : ∃ (x : Fin n → CL.𝔽₂), (CL.CLFun.truncate (k - 1) P).eval x = P.outputPrefix (k - 1) y) : (registers f m k).toFun (ctx, CL.toBits y) = CL.indicatorBits (CLChecks.prefixRegister P k y)