Fixed-width register operations for the executable hiding scan

noncomputable def MIPRE.Introspection.AuxiliaryBits.mask : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr) Cost.BitStr

Equations

• MIPRE.Introspection.AuxiliaryBits.mask = (MIPRE.Cost.PolyTimeFun.fst.ite MIPRE.Cost.PolyTimeFun.snd (MIPRE.Cost.PolyTimeFun.const false)).map.comp MIPRE.Cost.PolyTimeFun.zip

noncomputable def MIPRE.Introspection.AuxiliaryBits.complement : Cost.PolyTimeFun Cost.BitStr Cost.BitStr

Equations

• MIPRE.Introspection.AuxiliaryBits.complement = ((MIPRE.Cost.PolyTimeFun.id Bool).ite (MIPRE.Cost.PolyTimeFun.const false) (MIPRE.Cost.PolyTimeFun.const true)).map

noncomputable def MIPRE.Introspection.AuxiliaryBits.replace : Cost.PolyTimeFun (Cost.BitStr × Cost.BitStr × Cost.BitStr) Cost.BitStr

Equations

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

theorem MIPRE.Introspection.AuxiliaryBits.mask_correct {n : ℕ} (S : Finset (Fin n)) (x : Fin n → CL.𝔽₂) : mask.toFun (CL.indicatorBits S, CL.toBits x) = CL.toBits ((CL.proj S) x)

theorem MIPRE.Introspection.AuxiliaryBits.complement_correct {n : ℕ} (S : Finset (Fin n)) : complement.toFun (CL.indicatorBits S) = CL.indicatorBits Sᶜ

theorem MIPRE.Introspection.AuxiliaryBits.replace_correct {n : ℕ} (S : Finset (Fin n)) (x z : Fin n → CL.𝔽₂) : replace.toFun (CL.indicatorBits S, CL.toBits x, CL.toBits z) = CL.toBits ((CL.proj Sᶜ) x + (CL.proj S) z)

theorem MIPRE.Introspection.AuxiliaryBits.matrixSolve_encoding {m n : ℕ} (A : Matrix (Fin m) (Fin n) CL.𝔽₂) (v : Fin m → CL.𝔽₂) : LowDegree.BinaryLinear.matrixSolveProg.toFun (Cost.unary n, LowDegree.BinaryLinear.matrixBits A, CL.toBits v) = CL.toBits (LowDegree.BinaryLinear.vectorValue n (LowDegree.BinaryLinear.matrixSolveProg.toFun (Cost.unary n, LowDegree.BinaryLinear.matrixBits A, CL.toBits v)))