Field equations as constraints, as programs

Slice P4h of planning/aldous-lyons-track.md: the generic part of the answer-reduced verifier's linear-constraints processor. Every check of the answer-reduced game is a list of field equations E(z) = κ over F_{2^t} on the answer bits z, each giving t constraints (eqsCons): the coordinates of E at the unit vectors of the bits, then those of κ (fieldChecks_toCon). A program computing E(z) for every z therefore computes the constraints, by running on the unit vectors and transposing (fieldConsF, fieldConsF_eq); eqsConsF does it for an indexed list of equations (eqsConsF_eq). This is how the introspection stage computes its Pauli constraints (MIPRE.Tailored.Intro.PauliConsProg.fieldCons), here with targets.

A field element in the answer bits is a window of t bits (window, toBits_elt), read by windowF.

Windows

def MIPRE.Tailored.AnsRed.Typed.window (z : Cost.BitStr) (o t : ℕ) : Cost.BitStr

The t bits of a string from position o, bits beyond the string read as 0.

Equations

• MIPRE.Tailored.AnsRed.Typed.window z o t = List.ofFn fun (i : Fin t) => List.getD z (o + ↑i) false

@[simp]

theorem MIPRE.Tailored.AnsRed.Typed.length_window (z : Cost.BitStr) (o t : ℕ) : List.length (window z o t) = t

theorem MIPRE.Tailored.AnsRed.Typed.toBits_elt {t : ℕ} {ht : 1 ≤ t} (z : Cost.BitStr) (o : ℕ) : (SAT.shoupBinField t ht).toBits (elt t ht z o) = window z o t

The bits of the field element at position o are the window there.

noncomputable def MIPRE.Tailored.AnsRed.Typed.windowF : Cost.PolyTimeFun (Cost.Unary × Cost.Unary × Cost.BitStr) Cost.BitStr

The window program, on (t, o, z) with t and o in unary.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.windowF_apply (t o : ℕ) (z : Cost.BitStr) : windowF.toFun (Cost.unary t, Cost.unary o, z) = window z o t

Constraints from values at the unit vectors

noncomputable def MIPRE.Tailored.AnsRed.Typed.fieldConsF {I : Type} [Cost.SizedEncoding I] (uT uN : Cost.PolyTimeFun I Cost.Unary) (val : Cost.PolyTimeFun (I × Cost.BitStr) Cost.BitStr) (κ : Cost.PolyTimeFun I Cost.BitStr) : Cost.PolyTimeFun I (List Cost.BitStr)

The constraints of a field equation, from a program computing its value at every string of answer bits and one computing its target: coordinate s of the values at the N unit vectors, then coordinate s of the target, for s < t.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.range_map_unitBits (N : ℕ) (g : Cost.BitStr → Cost.BitStr) : List.map g (LowDegree.BinaryLinear.identityBits N) = List.ofFn fun (p : Fin N) => g (LowDegree.BinaryLinear.unitBits N ↑p)

theorem MIPRE.Tailored.AnsRed.Typed.fieldConsF_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] (uT uN : Cost.PolyTimeFun I Cost.Unary) (val : Cost.PolyTimeFun (I × Cost.BitStr) Cost.BitStr) (κ : Cost.PolyTimeFun I Cost.BitStr) {inp : I} {N : ℕ} (hT : uT.toFun inp = Cost.unary t) (hN : uN.toFun inp = Cost.unary N) (E : (Fin N → ZMod 2) →ₗ[ZMod 2] (SAT.shoupBinField t ht).carrier) (c : (SAT.shoupBinField t ht).carrier) (hval : ∀ (z : Cost.BitStr), List.length z = N → val.toFun (inp, z) = (SAT.shoupBinField t ht).toBits (E (Intro.bitVec N z))) (hκ : κ.toFun inp = (SAT.shoupBinField t ht).toBits c) : (fieldConsF uT uN val κ).toFun inp = List.map Intro.LinCheck.toCon (Intro.fieldChecks t ht E c)

A program of the values of a field equation computes its constraints.

noncomputable def MIPRE.Tailored.AnsRed.Typed.eqsConsF {I : Type} [Cost.SizedEncoding I] {J : Type} [Cost.SizedEncoding J] (uT uN : Cost.PolyTimeFun I Cost.Unary) (idx : Cost.PolyTimeFun I (List J)) (val : Cost.PolyTimeFun ((J × I) × Cost.BitStr) Cost.BitStr) (κ : Cost.PolyTimeFun (J × I) Cost.BitStr) : Cost.PolyTimeFun I (List Cost.BitStr)

The constraints of an indexed list of field equations: those of each equation, in the order of the indices.

Equations

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

theorem MIPRE.Tailored.AnsRed.Typed.eqsConsF_eq {t : ℕ} {ht : 1 ≤ t} {I : Type} [Cost.SizedEncoding I] {J : Type} [Cost.SizedEncoding J] (uT uN : Cost.PolyTimeFun I Cost.Unary) (idx : Cost.PolyTimeFun I (List J)) (val : Cost.PolyTimeFun ((J × I) × Cost.BitStr) Cost.BitStr) (κ : Cost.PolyTimeFun (J × I) Cost.BitStr) {inp : I} {N : ℕ} (hT : uT.toFun inp = Cost.unary t) (hN : uN.toFun inp = Cost.unary N) {is : List J} (hidx : idx.toFun inp = is) (E : J → (Fin N → ZMod 2) →ₗ[ZMod 2] (SAT.shoupBinField t ht).carrier) (c : J → (SAT.shoupBinField t ht).carrier) (hval : ∀ i ∈ is, ∀ (z : Cost.BitStr), List.length z = N → val.toFun ((i, inp), z) = (SAT.shoupBinField t ht).toBits ((E i) (Intro.bitVec N z))) (hκ : ∀ i ∈ is, κ.toFun (i, inp) = (SAT.shoupBinField t ht).toBits (c i)) : (eqsConsF uT uN idx val κ).toFun inp = eqsCons t ht (List.map (fun (i : J) => (E i, c i)) is)

Programs of the values of indexed field equations compute their constraints.