A read machine for Tree Evaluation

The Cook–Mertz procedure as a Turing.ReadMachine on the encoding of an instance. Its state holds natural numbers only, so that one state type serves all instances: the value length, the height and the prime p found at the start, three registers of residues modulo p, the stack of frames of Cslib.TreeEval.Iter and a control state.

The machine reads the header, finds the least prime p ≥ 2ℓ + 2, and then follows the iterative procedure over ZMod p with the units 1, …, p - 1, reading the input only at a leaf, bit by bit, and for the update of a round, in one pass over the table of the gate. That pass accumulates, for every output bit i, the sum of the weights ∏ⱼ χ of the table entries for i that are set, which is the multilinear extension of output bit i at the masked registers. At the end it emits register 2.

Main definitions

• Cslib.TreeEval.Reader.State: the states of the machine.
• Cslib.TreeEval.Reader.machine: the machine.

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

def Cslib.TreeEval.Reader.addMod (p a b : ℕ) : ℕ

The sum modulo p.

def Cslib.TreeEval.Reader.mulMod (p a b : ℕ) : ℕ

The product modulo p.

def Cslib.TreeEval.Reader.negMod (p a : ℕ) : ℕ

The negation modulo p.

def Cslib.TreeEval.Reader.powMod (p a : ℕ) : ℕ → ℕ

The n-th power modulo p, by repeated multiplication.

def Cslib.TreeEval.Reader.unitVal (j : ℕ) : ℕ

The residue of the unit of round j.

def Cslib.TreeEval.Reader.unitInv (p j : ℕ) : ℕ

The inverse of the unit of round j modulo a prime p, by Fermat's little theorem.

def Cslib.TreeEval.Reader.sgnVal (p : ℕ) (neg : Bool) : ℕ

The residue of a sign.

def Cslib.TreeEval.Reader.chi (p : ℕ) (b : Bool) (x : ℕ) : ℕ

The residue of x if b, and of 1 - x otherwise.

def Cslib.TreeEval.Reader.weight (p ℓ k : ℕ) (x y : List ℕ) : ℕ

The weight of the table entries for the inputs indexed by k at the masked registers x and y: the product of chi over the low and the high ℓ bits of k.

def Cslib.TreeEval.Reader.modifyAt (l : List ℕ) (i : ℕ) (g : ℕ → ℕ) : List ℕ

Change the element at i of a list by g.

Registers

@[reducible, inline]

abbrev Cslib.TreeEval.Reader.Regs : Type

Three registers of residues.

def Cslib.TreeEval.Reader.Regs.get (R : Regs) : Fin 3 → List ℕ

Register r.

def Cslib.TreeEval.Reader.Regs.set (R : Regs) : Fin 3 → List ℕ → Regs

Replace register r.

def Cslib.TreeEval.Reader.Regs.scale (p : ℕ) (r : Fin 3) (a : ℕ) (R : Regs) : Regs

Multiply register r by a modulo p.

The machine

inductive Cslib.TreeEval.Reader.Ctl : Type

The control state.

• hdrLength (n : ℕ) : Ctl

  Reading the value length from the header, n ones read so far.

• hdrHeight (n : ℕ) : Ctl

  Reading the height from the header, n ones read so far.

• prime (q d : ℕ) : Ctl

  Searching the prime: testing the candidate q against the divisor d.

• run : Ctl

  A step of the iterative procedure.

• leaf (i : ℕ) : Ctl

  Reading bit i of the leaf at the current path.

• scan (k : ℕ) (acc : List ℕ) : Ctl

  Reading bit k of the table of the gate of the top frame, with the sums so far.

• done : Ctl

  Halted, after emitting the value.

structure Cslib.TreeEval.Reader.State : Type

A state of the machine.

• ell : ℕ

  The value length ℓ.

• height : ℕ

  The height.

• p : ℕ

  The prime.

• regs : Regs

  The registers.

• stack : List Iter.Frame

  The stack of frames, innermost first.

• mode : Iter.Mode

  The mode of the iterative procedure.

• ctl : Ctl

  The control state.

def Cslib.TreeEval.Reader.offset (s : State) (st : List Iter.Frame) : ℕ

The offset in the encoding of the node at the path of a stack.

def Cslib.TreeEval.Reader.runStep (s : State) : State × List Bool

The steps of the iterative procedure, without input.

def Cslib.TreeEval.Reader.subtractSums (p c : ℕ) (t : Fin 3) (acc : List ℕ) (R : Regs) : Regs

Subtract c times the sums acc from register t, modulo p.

def Cslib.TreeEval.Reader.step (s : State) (b : Bool) : State × List Bool

A step, given the bit read.

def Cslib.TreeEval.Reader.addr (s : State) : Option ℕ

The address read by a step.

def Cslib.TreeEval.Reader.init : State

The initial state: reading the header.

def Cslib.TreeEval.Reader.machine : Turing.ReadMachine State

The Tree Evaluation read machine.