The Cook–Mertz procedure for Tree Evaluation with fan-in d

This generalizes the binary procedure Cslib.TreeEval.proc to fan-in d; at d = 2 it is that procedure step for step (Cslib.TreeEval.Ary.proc_ofBinary, proved beside the binary procedure, which derives its correctness from this file). The procedure keeps d + 1 registers, each holding ℓ elements of a finite field K, as global storage shared by all levels of the recursion. Called on a subtree, a coefficient c and a target register t, it adds c times the value of the subtree (read as 0/1 field elements) to register t and leaves the other d registers unchanged, whatever their contents.

The child j of a target t uses the register reg t j = t + (j + 1), so the d children use exactly the registers other than t; for d = 2 these are the registers t + 1 and t + 2 of the binary procedure. At an internal node with gate f, the procedure runs one round for every unit u of K. A round scales the child registers by u, adds the children's values to them by recursive calls, subtracts c times the multilinear extension of f at the masked values from register t, and then undoes the recursive calls and the scaling. Summed over all units, the masks cancel (FiniteField.sum_units_eval_mul_add), because the extension has degree at most d * ℓ < |K| - 1, and register t has gained c • f (v₀, …, v_{d-1}).

This file proves correctness only; space bounds are separate.

Main definitions

• Cslib.TreeEval.embed: an ℓ-bit value read as 0/1 field elements, for any fan-in.
• Cslib.TreeEval.Ary.reg: the register of a child.
• Cslib.TreeEval.Ary.gatePoly: the multilinear extension of an output bit of a gate.
• Cslib.TreeEval.Ary.proc: the procedure, parametrized by an enumeration of the units of K.

Main results

• Cslib.TreeEval.Ary.proc_eq: the procedure adds c times the value of the tree to the target register and leaves the other registers unchanged.
• Cslib.TreeEval.Ary.proc_zero: started from zero registers, it leaves the value of the tree in the target register.
• Cslib.TreeEval.Ary.embed_eval_eq_proc: the same, for the canonical enumeration of the units.

References

• J. Cook and I. Mertz, Tree Evaluation is in Space O(log n · log log n), Lemma 13 and Theorem 10, for fan-in d.
• O. Goldreich, On the Cook–Mertz Tree Evaluation procedure, Algorithm 1, whose signed recursive calls are followed here.

def Cslib.TreeEval.embed {K : Type u_1} [Field K] {ℓ : ℕ} (v : Fin ℓ → Bool) : Fin ℓ → K

An ℓ-bit value read as 0/1 field elements.

@[reducible, inline]

abbrev Cslib.TreeEval.Ary.State (K : Type u_2) (d ℓ : ℕ) : Type u_2

The global storage: d + 1 registers of ℓ field elements.

def Cslib.TreeEval.Ary.reg {d : ℕ} (t : Fin (d + 1)) (j : Fin d) : Fin (d + 1)

The register of child j when the target register is t.

theorem Cslib.TreeEval.Ary.reg_injective {d : ℕ} (t : Fin (d + 1)) : Function.Injective (reg t)

def Cslib.TreeEval.Ary.childVal {K : Type u_1} [Field K] {d ℓ : ℕ} (t : Fin (d + 1)) (v : Fin d → Fin ℓ → K) (r : Fin (d + 1)) : Fin ℓ → K

The value of the child whose register is r, and 0 at the target register.

@[simp]

theorem Cslib.TreeEval.Ary.childVal_reg {K : Type u_1} [Field K] {d ℓ : ℕ} (t : Fin (d + 1)) (v : Fin d → Fin ℓ → K) (j : Fin d) : childVal t v (reg t j) = v j

noncomputable def Cslib.TreeEval.Ary.gatePoly {K : Type u_1} [Field K] {d ℓ : ℕ} (f : Gate d ℓ) (i : Fin ℓ) : MvPolynomial (Fin d × Fin ℓ) K

The multilinear extension of output bit i of a gate, in the bits of all its inputs.

def Cslib.TreeEval.Ary.scale {K : Type u_1} [Field K] {d ℓ : ℕ} (r : Fin (d + 1)) (a : K) (S : State K d ℓ) : State K d ℓ

Multiply register r by a.

noncomputable def Cslib.TreeEval.Ary.gateUpdate {K : Type u_1} [Field K] {d ℓ : ℕ} (f : Gate d ℓ) (c : K) (t : Fin (d + 1)) (S : State K d ℓ) : State K d ℓ

The update of a round at a gate f: subtract c times the gate's extension at the child registers from register t.

noncomputable def Cslib.TreeEval.Ary.gateRound {K : Type u_1} [Field K] {d ℓ : ℕ} (p : Fin d → K → Fin (d + 1) → State K d ℓ → State K d ℓ) (f : Gate d ℓ) (c : K) (t : Fin (d + 1)) (u : Kˣ) (S : State K d ℓ) : State K d ℓ

One round of the procedure at a gate f, for the unit u, given procedures p j for the subtrees. The target is t, and the child registers reg t j hold the masks.

noncomputable def Cslib.TreeEval.Ary.proc {K : Type u_1} [Field K] {d ℓ : ℕ} (us : List Kˣ) {h : ℕ} : Tree d ℓ h → K → Fin (d + 1) → State K d ℓ → State K d ℓ

The Cook–Mertz procedure: add c times the value of the tree to register t. At a gate it runs one gateRound for every unit in the enumeration us.

theorem Cslib.TreeEval.Ary.proc_eq {K : Type u_1} [Field K] {d ℓ : ℕ} [Fintype K] {us : List Kˣ} (hnd : us.Nodup) (hmem : ∀ (u : Kˣ), u ∈ us) (hK : d * ℓ < Fintype.card K - 1) {h : ℕ} (T : Tree d ℓ h) (c : K) (t : Fin (d + 1)) (S : State K d ℓ) : proc us T c t S = Function.update S t (S t + c • embed T.eval)

Correctness of the Cook–Mertz procedure for fan-in d. If us enumerates the units of K without repetition and d * ℓ < |K| - 1, then the procedure adds c times the value of the tree to the target register and leaves the other registers unchanged, whatever their initial contents.

theorem Cslib.TreeEval.Ary.proc_zero {K : Type u_1} [Field K] {d ℓ : ℕ} [Fintype K] {us : List Kˣ} (hnd : us.Nodup) (hmem : ∀ (u : Kˣ), u ∈ us) (hK : d * ℓ < Fintype.card K - 1) {h : ℕ} (T : Tree d ℓ h) (t : Fin (d + 1)) : proc us T 1 t 0 t = embed T.eval

Started from zero registers, the procedure leaves the value of the tree in the target register.

theorem Cslib.TreeEval.Ary.embed_eval_eq_proc {K : Type u_1} [Field K] {d ℓ : ℕ} [Fintype K] [DecidableEq K] (hK : d * ℓ < Fintype.card K - 1) {h : ℕ} (T : Tree d ℓ h) (t : Fin (d + 1)) : embed T.eval = proc Finset.univ.toList T 1 t 0 t

Tree Evaluation with fan-in d by the Cook–Mertz procedure. Run over the units of K in any order with d * ℓ < |K| - 1, from zero registers, the procedure computes the value of the tree into the target register.