The executable seed enumeration for Pauli sampling

Field elements are numbered by their canonical little-endian bit strings. For m = 2^j and a field of size 2^k, the selector keeps the highest j bits. This is the paper's equal-block selector for this explicit enumeration; it does not identify the enumeration with Fintype.equivFin.

def MIPRE.Introspection.SeedProgram.fieldIndex {k : ℕ} (E : SAT.BinField k) (a : E.carrier) : Fin (2 ^ k)

Equations

• MIPRE.Introspection.SeedProgram.fieldIndex E a = ⟨MIPRE.Cost.bitsVal (E.toBits a), ⋯⟩

theorem MIPRE.Introspection.SeedProgram.fieldIndex_injective {k : ℕ} (E : SAT.BinField k) : Function.Injective (fieldIndex E)

noncomputable def MIPRE.Introspection.SeedProgram.fieldEnumeration {k : ℕ} (E : SAT.BinField k) : E.carrier ≃ Fin (2 ^ k)

A genuine field enumeration, with forward direction given by canonical binary rank. Only its inverse uses finite choice.

Equations

• MIPRE.Introspection.SeedProgram.fieldEnumeration E = Equiv.ofBijective (MIPRE.Introspection.SeedProgram.fieldIndex E) ⋯

def MIPRE.Introspection.SeedProgram.selector {k : ℕ} (E : SAT.BinField k) (j : ℕ) (hj : j ≤ k) (a : E.carrier) : Fin (2 ^ j)

Equations

• MIPRE.Introspection.SeedProgram.selector E j hj a = ⟨↑(MIPRE.Introspection.SeedProgram.fieldIndex E a) / 2 ^ (k - j), ⋯⟩

theorem MIPRE.Introspection.SeedProgram.bitsVal_drop (l : Cost.BitStr) (n : ℕ) : Cost.bitsVal (List.drop n l) = Cost.bitsVal l / 2 ^ n

theorem MIPRE.Introspection.SeedProgram.selector_eq_bits {k : ℕ} (E : SAT.BinField k) (j : ℕ) (hj : j ≤ k) (a : E.carrier) : ↑(selector E j hj a) = Cost.bitsVal (List.drop (k - j) (E.toBits a))

The exact connection between the equal-block selector and its bit scan.

noncomputable def MIPRE.Introspection.SeedProgram.seedCoordinates {k : ℕ} (E : SAT.BinField k) (j : ℕ) (hj : j ≤ k) : E.carrier ≃ Fin (2 ^ j) × Fin (2 ^ (k - j))

Equations

• MIPRE.Introspection.SeedProgram.seedCoordinates E j hj = ((MIPRE.Introspection.SeedProgram.fieldEnumeration E).trans (finCongr ⋯)).trans finProdFinEquiv.symm

theorem MIPRE.Introspection.SeedProgram.seedCoordinates_fst {k : ℕ} (E : SAT.BinField k) (j : ℕ) (hj : j ≤ k) (a : E.carrier) : ((seedCoordinates E j hj) a).1 = selector E j hj a

theorem MIPRE.Introspection.SeedProgram.card_selector_fiber {k : ℕ} (E : SAT.BinField k) (j : ℕ) (hj : j ≤ k) (i : Fin (2 ^ j)) : Fintype.card { a : E.carrier // selector E j hj a = i } = 2 ^ (k - j)

Every direction index occurs exactly 2^(k-j) times.

noncomputable def MIPRE.Introspection.SeedProgram.selectorProg : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr) ℕ

k, j, and the raw seed are supplied explicitly. The computation never constructs a unary representation of the field size.

Equations

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

theorem MIPRE.Introspection.SeedProgram.selectorProg_apply (k j : Cost.Unary) (s : Cost.BitStr) : selectorProg.toFun (k, j, s) = Cost.bitsVal (List.drop (List.length k - List.length j) s)

theorem MIPRE.Introspection.SeedProgram.selectorProg_correct {k : ℕ} (E : SAT.BinField k) (j : ℕ) (hj : j ≤ k) (a : E.carrier) : selectorProg.toFun (Cost.unary k, Cost.unary j, E.toBits a) = ↑(selector E j hj a)

theorem MIPRE.Introspection.SeedProgram.selectorProg_runs (x : Cost.Unary × Cost.Unary × Cost.BitStr) : ∃ r ≤ Polynomial.eval (Cost.esize x) selectorProg.timeBound, selectorProg.code.Runs (Cost.encode x) (Cost.encode (selectorProg.toFun x)) r