Executable conversion to the introspection field basis

The sampler's field arithmetic uses canonical Shoup polynomial coordinates, whereas downsizing uses the constructed self-dual normal basis. These are two different encodings. The fixed programs below construct that basis from its unary odd degree and convert in both directions, including row-wise conversion. No basis matrix is supplied as an oracle or chosen independently of the code.

noncomputable def MIPRE.Introspection.BasisProgram.fromBasisProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr × Cost.BitStr) Cost.BitStr

Evaluate supplied basis coordinates in the canonical polynomial basis.

Equations

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

theorem MIPRE.Introspection.BasisProgram.fromBasisProg_correct (k : ℕ) (hk : 1 ≤ k) (b : Module.Basis (Fin k) (ZMod 2) (SAT.shoupBinField k hk).carrier) (a : (SAT.shoupBinField k hk).carrier) : fromBasisProg.toFun (Cost.unary k, List.ofFn fun (i : Fin k) => (SAT.shoupBinField k hk).toBits (b i), LowDegree.BinaryLinear.vectorBits (b.equivFun a)) = (SAT.shoupBinField k hk).toBits a

noncomputable def MIPRE.Introspection.BasisProgram.toSelfDualProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr) Cost.BitStr

Canonical field bits to the effective self-dual basis coordinates.

Equations

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

noncomputable def MIPRE.Introspection.BasisProgram.fromSelfDualProg : Cost.PolyTimeFun (Cost.Unary × Cost.BitStr) Cost.BitStr

Effective self-dual coordinates to canonical field bits.

Equations

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

theorem MIPRE.Introspection.BasisProgram.toSelfDualProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (a : (SAT.shoupBinField k hk).carrier) : toSelfDualProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).toBits a) = LowDegree.BinaryLinear.vectorBits ((SAT.shoupSelfDualNormalBasis k hk hodd).equivFun a)

theorem MIPRE.Introspection.BasisProgram.fromSelfDualProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) (a : (SAT.shoupBinField k hk).carrier) : fromSelfDualProg.toFun (Cost.unary k, LowDegree.BinaryLinear.vectorBits ((SAT.shoupSelfDualNormalBasis k hk hodd).equivFun a)) = (SAT.shoupBinField k hk).toBits a

noncomputable def MIPRE.Introspection.BasisProgram.toSelfDualRowsProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) (List Cost.BitStr)

Construct the basis once for the row list, then convert each row.

Equations

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

noncomputable def MIPRE.Introspection.BasisProgram.fromSelfDualRowsProg : Cost.PolyTimeFun (Cost.Unary × List Cost.BitStr) (List Cost.BitStr)

Equations

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

theorem MIPRE.Introspection.BasisProgram.toSelfDualRowsProg_apply (k : Cost.Unary) (vs : List Cost.BitStr) : toSelfDualRowsProg.toFun (k, vs) = List.map (fun (v : Cost.BitStr) => toSelfDualProg.toFun (k, v)) vs

theorem MIPRE.Introspection.BasisProgram.fromSelfDualRowsProg_apply (k : Cost.Unary) (vs : List Cost.BitStr) : fromSelfDualRowsProg.toFun (k, vs) = List.map (fun (v : Cost.BitStr) => fromSelfDualProg.toFun (k, v)) vs

theorem MIPRE.Introspection.BasisProgram.toSelfDualRowsProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) {n : ℕ} (u : Fin n → (SAT.shoupBinField k hk).carrier) : toSelfDualRowsProg.toFun (Cost.unary k, (SAT.shoupBinField k hk).vecBits u) = List.ofFn fun (i : Fin n) => LowDegree.BinaryLinear.vectorBits ((SAT.shoupSelfDualNormalBasis k hk hodd).equivFun (u i))

theorem MIPRE.Introspection.BasisProgram.fromSelfDualRowsProg_correct (k : ℕ) (hk : 1 ≤ k) [NeZero k] (hodd : Odd k) {n : ℕ} (u : Fin n → (SAT.shoupBinField k hk).carrier) : fromSelfDualRowsProg.toFun (Cost.unary k, List.ofFn fun (i : Fin n) => LowDegree.BinaryLinear.vectorBits ((SAT.shoupSelfDualNormalBasis k hk hodd).equivFun (u i))) = (SAT.shoupBinField k hk).vecBits u