Field arithmetic, as programs

Slice P4h of planning/aldous-lyons-track.md: combinators for programs computing elements of F_{2^t} in their Shoup bits, with the law that they compute a given field expression when their arguments do: sums (fAdd), products (fMul), 0 and 1, the assignment form g (1 - g) (fCert), indexed sums (fSum, by folding xorBits) and comparisons (fEq). The proof check of the answer-reduced game is written with them.

Summing bit strings

theorem MIPRE.Tailored.AnsRed.Typed.esize_xorBits_le (a b : Cost.BitStr) : Cost.esize (LowDegree.BinaryPolynomial.xorBits a b) ≤ 4 * Cost.esize b + 1

noncomputable def MIPRE.Tailored.AnsRed.Typed.xorSumF : Cost.PolyTimeFun (List Cost.BitStr × Cost.BitStr) Cost.BitStr

The sum of a list of bit strings, from an initial one, by folding xorBits.

Equations

• MIPRE.Tailored.AnsRed.Typed.xorSumF = MIPRE.LowDegree.BinaryPolynomial.xorBitsProg.foldlAdd (4 * Polynomial.X + 1) MIPRE.Tailored.AnsRed.Typed.xorSumF._proof_2

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.xorSumF_apply (l : List Cost.BitStr) (s : Cost.BitStr) : xorSumF.toFun (l, s) = List.foldl LowDegree.BinaryPolynomial.xorBits s l

theorem MIPRE.Tailored.AnsRed.Typed.foldl_xorBits_toBits {t : ℕ} {ht : 1 ≤ t} (l : List (Fq t ht)) (s : Fq t ht) : List.foldl LowDegree.BinaryPolynomial.xorBits ((SAT.shoupBinField t ht).toBits s) (List.map (SAT.shoupBinField t ht).toBits l) = (SAT.shoupBinField t ht).toBits (s + l.sum)

The sum of field elements, in their bits.

Combinators

noncomputable def MIPRE.Tailored.AnsRed.Typed.fAdd {I : Type} [Cost.SizedEncoding I] (a b : Cost.PolyTimeFun I Cost.BitStr) : Cost.PolyTimeFun I Cost.BitStr

The sum of two field elements.

Equations

• MIPRE.Tailored.AnsRed.Typed.fAdd a b = MIPRE.LowDegree.BinaryPolynomial.xorBitsProg.comp (a.pair b)

noncomputable def MIPRE.Tailored.AnsRed.Typed.fMul {I : Type} [Cost.SizedEncoding I] (uT : Cost.PolyTimeFun I Cost.Unary) (a b : Cost.PolyTimeFun I Cost.BitStr) : Cost.PolyTimeFun I Cost.BitStr

The product of two field elements.

Equations

• MIPRE.Tailored.AnsRed.Typed.fMul uT a b = MIPRE.SAT.shoupMulProg.comp (uT.pair (a.pair b))

noncomputable def MIPRE.Tailored.AnsRed.Typed.fZero {I : Type} [Cost.SizedEncoding I] (uT : Cost.PolyTimeFun I Cost.Unary) : Cost.PolyTimeFun I Cost.BitStr

The field element 0.

Equations

• MIPRE.Tailored.AnsRed.Typed.fZero uT = MIPRE.Cost.PolyTimeFun.replicate.comp (uT.pair (MIPRE.Cost.PolyTimeFun.const false))

noncomputable def MIPRE.Tailored.AnsRed.Typed.fOne {I : Type} [Cost.SizedEncoding I] (uT : Cost.PolyTimeFun I Cost.Unary) : Cost.PolyTimeFun I Cost.BitStr

The field element 1.

Equations

• MIPRE.Tailored.AnsRed.Typed.fOne uT = MIPRE.LowDegree.BinaryPolynomial.oneBitsProg.comp (MIPRE.Tailored.AnsRed.Typed.fZero uT)

noncomputable def MIPRE.Tailored.AnsRed.Typed.fCert {I : Type} [Cost.SizedEncoding I] (uT : Cost.PolyTimeFun I Cost.Unary) (a : Cost.PolyTimeFun I Cost.BitStr) : Cost.PolyTimeFun I Cost.BitStr

g (1 - g), as g (1 + g) in characteristic 2.

Equations

• MIPRE.Tailored.AnsRed.Typed.fCert uT a = MIPRE.Tailored.AnsRed.Typed.fMul uT a (MIPRE.Tailored.AnsRed.Typed.fAdd (MIPRE.Tailored.AnsRed.Typed.fOne uT) a)

noncomputable def MIPRE.Tailored.AnsRed.Typed.fSum {I : Type} [Cost.SizedEncoding I] (uT : Cost.PolyTimeFun I Cost.Unary) (f : Cost.PolyTimeFun (Cost.Unary × I) Cost.BitStr) (n : Cost.PolyTimeFun I Cost.Unary) : Cost.PolyTimeFun I Cost.BitStr

The sum of f i over i < n.

Equations

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

noncomputable def MIPRE.Tailored.AnsRed.Typed.fEq {I : Type} [Cost.SizedEncoding I] (a b : Cost.PolyTimeFun I Cost.BitStr) : Cost.PolyTimeFun I Bool

Whether two field elements are equal.

Equations

• MIPRE.Tailored.AnsRed.Typed.fEq a b = MIPRE.SAT.ArrayProg.eqBits.comp (a.pair b)

theorem MIPRE.Tailored.AnsRed.Typed.fAdd_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] {inp : I} {a b : Cost.PolyTimeFun I Cost.BitStr} {x y : Fq t ht} (ha : a.toFun inp = (SAT.shoupBinField t ht).toBits x) (hb : b.toFun inp = (SAT.shoupBinField t ht).toBits y) : (fAdd a b).toFun inp = (SAT.shoupBinField t ht).toBits (x + y)

theorem MIPRE.Tailored.AnsRed.Typed.fMul_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] {uT : Cost.PolyTimeFun I Cost.Unary} {inp : I} (hT : uT.toFun inp = Cost.unary t) {a b : Cost.PolyTimeFun I Cost.BitStr} {x y : Fq t ht} (ha : a.toFun inp = (SAT.shoupBinField t ht).toBits x) (hb : b.toFun inp = (SAT.shoupBinField t ht).toBits y) : (fMul uT a b).toFun inp = (SAT.shoupBinField t ht).toBits (x * y)

theorem MIPRE.Tailored.AnsRed.Typed.fZero_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] {uT : Cost.PolyTimeFun I Cost.Unary} {inp : I} (hT : uT.toFun inp = Cost.unary t) : (fZero uT).toFun inp = (SAT.shoupBinField t ht).toBits 0

theorem MIPRE.Tailored.AnsRed.Typed.fOne_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] {uT : Cost.PolyTimeFun I Cost.Unary} {inp : I} (hT : uT.toFun inp = Cost.unary t) : (fOne uT).toFun inp = (SAT.shoupBinField t ht).toBits 1

theorem MIPRE.Tailored.AnsRed.Typed.fCert_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] {uT : Cost.PolyTimeFun I Cost.Unary} {inp : I} (hT : uT.toFun inp = Cost.unary t) {a : Cost.PolyTimeFun I Cost.BitStr} {x : Fq t ht} (ha : a.toFun inp = (SAT.shoupBinField t ht).toBits x) : (fCert uT a).toFun inp = (SAT.shoupBinField t ht).toBits (x * (1 - x))

theorem MIPRE.Tailored.AnsRed.Typed.fSum_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] {uT : Cost.PolyTimeFun I Cost.Unary} {inp : I} (hT : uT.toFun inp = Cost.unary t) {f : Cost.PolyTimeFun (Cost.Unary × I) Cost.BitStr} {n : Cost.PolyTimeFun I Cost.Unary} {k : ℕ} (hn : n.toFun inp = Cost.unary k) (g : Fin k → Fq t ht) (hf : ∀ (i : Fin k), f.toFun (Cost.unary ↑i, inp) = (SAT.shoupBinField t ht).toBits (g i)) : (fSum uT f n).toFun inp = (SAT.shoupBinField t ht).toBits (∑ i : Fin k, g i)

theorem MIPRE.Tailored.AnsRed.Typed.fEq_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] {inp : I} {a b : Cost.PolyTimeFun I Cost.BitStr} {x y : Fq t ht} (ha : a.toFun inp = (SAT.shoupBinField t ht).toBits x) (hb : b.toFun inp = (SAT.shoupBinField t ht).toBits y) : (fEq a b).toFun inp = decide (x = y)