Residues and registers of the Tree Evaluation read machine

The read machine computes with natural numbers below a prime p; this file relates them to ZMod p. The residue operations cast to the field operations, and the register operations to those of Cslib.TreeEval.Iter on the registers read as field elements. The weight of a table entry casts to the value of the indicator polynomial of its inputs, so that the sums over the table give the multilinear extension of a gate.

Main definitions

• Cslib.TreeEval.Reader.Regs.toState: the registers read in ZMod p.
• Cslib.TreeEval.Reader.Regs.WF: registers of length ℓ holding residues below p.

Main results

• Cslib.TreeEval.Reader.cast_weight: the weight casts to the product of x or 1 - x over the bits of the inputs.
• Cslib.TreeEval.Reader.eval_gatePoly_eq_sum: the multilinear extension of an output bit of a gate as a sum over the table indices k < 4^ℓ.

References

• J. Cook and I. Mertz, Tree Evaluation is in Space O(log n · log log n)
• O. Goldreich, On the Cook–Mertz Tree Evaluation procedure, Algorithm 1, which the machine runs.

Residues

@[simp]

theorem Cslib.TreeEval.Reader.cast_addMod {p : ℕ} (a b : ℕ) : ↑(addMod p a b) = ↑a + ↑b

@[simp]

theorem Cslib.TreeEval.Reader.cast_mulMod {p : ℕ} (a b : ℕ) : ↑(mulMod p a b) = ↑a * ↑b

@[simp]

theorem Cslib.TreeEval.Reader.cast_negMod {p : ℕ} [NeZero p] (a : ℕ) : ↑(negMod p a) = -↑a

@[simp]

theorem Cslib.TreeEval.Reader.cast_powMod {p : ℕ} (a n : ℕ) : ↑(powMod p a n) = ↑a ^ n

@[simp]

theorem Cslib.TreeEval.Reader.cast_chi {p : ℕ} [NeZero p] (b : Bool) (x : ℕ) : ↑(chi p b x) = if b = true then ↑x else 1 - ↑x

@[simp]

theorem Cslib.TreeEval.Reader.cast_sgnVal {p : ℕ} [Fact (Nat.Prime p)] (neg : Bool) : ↑(sgnVal p neg) = Iter.sgn neg

theorem Cslib.TreeEval.Reader.cast_unitVal {p : ℕ} [Fact (Nat.Prime p)] {j : ℕ} (hj : j < p - 1) : ↑(unitVal j) = ↑(Iter.zmodUnit p j)

The unit of round j casts to the unit Iter.zmodUnit p j, for j < p - 1.

theorem Cslib.TreeEval.Reader.cast_unitInv_eq {p : ℕ} [Fact (Nat.Prime p)] {j : ℕ} (hj : j < p - 1) : ↑(unitInv p j) = ↑(Iter.zmodUnit p j)⁻¹

The inverse of the unit of round j casts to the inverse of Iter.zmodUnit p j.

Registers

def Cslib.TreeEval.Reader.Regs.toState (p ℓ : ℕ) (R : Regs) : TreeEval.State (ZMod p) ℓ

The registers read as field elements: element i of register r, or 0.

def Cslib.TreeEval.Reader.Regs.WF (p ℓ : ℕ) (R : Regs) : Prop

Registers of length ℓ holding residues below p.

@[simp]

theorem Cslib.TreeEval.Reader.Regs.get_set_self (R : Regs) (r : Fin 3) (l : List ℕ) : (R.set r l).get r = l

theorem Cslib.TreeEval.Reader.modifyAt_addMod_wf {p : ℕ} (hp : 0 < p) {acc : List ℕ} (hacc : ∀ v ∈ acc, v < p) (i a : ℕ) : (modifyAt acc i (addMod p a)).length = acc.length ∧ ∀ v ∈ modifyAt acc i (addMod p a), v < p

theorem Cslib.TreeEval.Reader.toState_scale {p : ℕ} [Fact (Nat.Prime p)] {ℓ : ℕ} (R : Regs) (r : Fin 3) (a : ℕ) : Regs.toState p ℓ (Regs.scale p r a R) = scale r (↑a) (Regs.toState p ℓ R)

theorem Cslib.TreeEval.Reader.Regs.WF.scale {p ℓ : ℕ} (hp : 0 < p) {R : Regs} (hR : WF p ℓ R) (r : Fin 3) (a : ℕ) : WF p ℓ (Regs.scale p r a R)

theorem Cslib.TreeEval.Reader.toState_set_modifyAt {p : ℕ} [Fact (Nat.Prime p)] {ℓ : ℕ} (R : Regs) (t : Fin 3) (i : Fin ℓ) (hlen : (R.get t).length = ℓ) (g : ℕ → ℕ) : Regs.toState p ℓ (R.set t (modifyAt (R.get t) (↑i) g)) = Function.update (Regs.toState p ℓ R) t (Function.update (Regs.toState p ℓ R t) i ↑(g ((R.get t).getD (↑i) 0)))

theorem Cslib.TreeEval.Reader.Regs.WF.set_modifyAt {p ℓ : ℕ} (hp : 0 < p) {R : Regs} (hR : WF p ℓ R) (t : Fin 3) (i a : ℕ) : WF p ℓ (R.set t (modifyAt (R.get t) i (addMod p a)))

theorem Cslib.TreeEval.Reader.Regs.WF.subtractSums {p ℓ : ℕ} (hp : 0 < p) {R : Regs} (hR : WF p ℓ R) (c : ℕ) (t : Fin 3) (acc : List ℕ) : WF p ℓ (Reader.subtractSums p c t acc R)

theorem Cslib.TreeEval.Reader.toState_subtractSums {p : ℕ} [Fact (Nat.Prime p)] {ℓ : ℕ} (R : Regs) (c : ℕ) (t : Fin 3) (acc : List ℕ) (hlen : (R.get t).length = ℓ) : Regs.toState p ℓ (subtractSums p c t acc R) = Function.update (Regs.toState p ℓ R) t fun (i : Fin ℓ) => Regs.toState p ℓ R t i - ↑c * ↑(acc.getD (↑i) 0)

Weights and the multilinear extension

theorem Cslib.TreeEval.Reader.cast_weight {p : ℕ} [Fact (Nat.Prime p)] {ℓ : ℕ} (k : ℕ) (x y : List ℕ) : ↑(weight p ℓ k x y) = (∏ j : Fin ℓ, if lowBits ℓ k j = true then ↑(x.getD (↑j) 0) else 1 - ↑(x.getD (↑j) 0)) * ∏ j : Fin ℓ, if highBits ℓ k j = true then ↑(y.getD (↑j) 0) else 1 - ↑(y.getD (↑j) 0)

The weight casts to the product of x or 1 - x over the low bits of k, times the same over its high bits for y.

def Cslib.TreeEval.Reader.cubeEquiv (ℓ : ℕ) : (Fin ℓ ⊕ Fin ℓ → Bool) ≃ Fin (2 ^ (ℓ + ℓ))

The inputs of a gate as the indices below 2^(2ℓ).

theorem Cslib.TreeEval.Reader.cubeEquiv_symm_apply {ℓ : ℕ} (k : Fin (2 ^ (ℓ + ℓ))) : (cubeEquiv ℓ).symm k = Sum.elim (lowBits ℓ ↑k) (highBits ℓ ↑k)

An index reads as its low and high bits.

theorem Cslib.TreeEval.Reader.four_pow_eq (ℓ : ℕ) : 4 ^ ℓ = 2 ^ (ℓ + ℓ)

theorem Cslib.TreeEval.Reader.eval_gatePoly_eq_sum {p : ℕ} [Fact (Nat.Prime p)] {ℓ : ℕ} (f : Gate ℓ) (i : Fin ℓ) (X Y : Fin ℓ → ZMod p) : (MvPolynomial.eval (Sum.elim X Y)) (gatePoly f i) = ∑ k ∈ Finset.range (4 ^ ℓ), BitString.bitVal (ZMod p) (f (lowBits ℓ k) (highBits ℓ k) i) * ((∏ j : Fin ℓ, if lowBits ℓ k j = true then X j else 1 - X j) * ∏ j : Fin ℓ, if highBits ℓ k j = true then Y j else 1 - Y j)

The multilinear extension of an output bit as a sum over the table indices.