Encoded field vectors and their circuit-coordinate slices

theorem MIPRE.SAT.BinField.vecBits_eq_ofFn {k : ℕ} (E : BinField k) {n : ℕ} (v : Fin n → E.carrier) : E.vecBits v = List.ofFn fun (i : Fin n) => E.toBits (v i)

theorem MIPRE.SAT.BinField.vecBits_cast {k : ℕ} (E : BinField k) {n m : ℕ} (h : n = m) (v : Fin m → E.carrier) : E.vecBits (v ∘ Fin.cast h) = E.vecBits v

@[simp]

theorem MIPRE.SAT.BinField.getD_vecBits {k : ℕ} (E : BinField k) {n : ℕ} (v : Fin n → E.carrier) (i : Fin n) : (E.vecBits v).getD ↑i [] = E.toBits (v i)

theorem MIPRE.SAT.BinField.slice_vecBits {k : ℕ} (E : BinField k) {n : ℕ} (v : Fin n → E.carrier) (a b : ℕ) (h : a + b ≤ n) : List.take b (List.drop a (E.vecBits v)) = E.vecBits fun (i : Fin b) => v ⟨a + ↑i, ⋯⟩

Slicing the raw blocks is exactly slicing the typed coordinate function.

theorem MIPRE.SAT.BinField.zip_vecBits {k : ℕ} (E : BinField k) {n : ℕ} (v w : Fin n → E.carrier) : (E.vecBits v).zip (E.vecBits w) = List.ofFn fun (i : Fin n) => (E.toBits (v i), E.toBits (w i))

theorem MIPRE.SAT.BinField.eval_circuitBits_vecBits {k : ℕ} (E : BinField k) (C : Circuit) (hC : C.WellFormed) (p : Cost.BitStr) (hp : p ≠ []) (hpk : List.length p = k) [CharP E.carrier 2] (root : E.carrier) (hroot : root ^ List.length p = LowDegree.BinaryPolynomial.evalBits root p) (hencode : ∀ (a : E.carrier), LowDegree.BinaryPolynomial.evalBits root (E.toBits a) = a) (v : Fin (C.inputs + C.size) → E.carrier) : LowDegree.BinaryPolynomial.evalBits root (Circuit.circuitBits p (List.take C.inputs (E.vecBits v)) (List.drop C.inputs (E.vecBits v)) C.gates) = (MvPolynomial.eval v) C.finiteArith

The circuit evaluator on a raw vector computes the finite polynomial at the original typed point, for any correct coefficient representation.