Frames of the iterative Cook–Mertz procedure

Cslib.TreeEval.proc is recursive. Unravelled into a loop, its state is the three registers, a stack with one frame per level, and a mode. A frame records only the round, the phase within the round, the sign and the target register of its level, which is what makes the procedure space-efficient: the path to the current node is read off the phases of the frames.

In mode call neg t, the procedure is about to add ± the value of the node at the current path to register t. In mode ret, it continues the round of the top frame, which calls the children in the order left, right, left, right, with signs +, +, -, -, as in Cslib.TreeEval.gateRound, and moves on to the next round or returns. The read machine Cslib.TreeEval.Reader.machine runs this loop over ZMod p with the units 1, …, p - 1.

Main definitions

• Cslib.TreeEval.Iter.Frame, Cslib.TreeEval.Iter.Mode: frames and modes.
• Cslib.TreeEval.Iter.path: the path to the current node.
• Cslib.TreeEval.Iter.zmodUnit: the units 1, …, p - 1 of ZMod p.

References

• O. Goldreich, On the Cook–Mertz Tree Evaluation procedure, Algorithm 1.

structure Cslib.TreeEval.Iter.Frame : Type

A frame of the recursion: the round, the phase within the round, whether the level subtracts its value, and its target register. In phase n the frame has called its left child (n even) or its right child (n odd), adding for n < 2 and subtracting otherwise.

• round : ℕ

  The round, indexing the unit that masks the children.

• phase : Fin 4

  The phase within the round.

• neg : Bool

  Whether the value of this level is subtracted.

• target : Fin 3

  The target register.

@[instance_reducible]

instance Cslib.TreeEval.Iter.instDecidableEqFrame : DecidableEq Frame

def Cslib.TreeEval.Iter.instDecidableEqFrame.decEq (x✝ x✝¹ : Frame) : Decidable (x✝ = x✝¹)

def Cslib.TreeEval.Iter.Frame.dir (fr : Frame) : Bool

The child a frame has called: the right one in the odd phases.

def Cslib.TreeEval.Iter.path : List Frame → List Bool

The path to the node called by the top frame, from the root.

inductive Cslib.TreeEval.Iter.Mode : Type

The mode of the machine: about to evaluate the current node into a register, or returning to the top frame.

• call (neg : Bool) (t : Fin 3) : Mode

  About to add ± the value of the node at the current path to register t.

• ret : Mode

  Returning to the top frame.

@[instance_reducible]

instance Cslib.TreeEval.Iter.instDecidableEqMode : DecidableEq Mode

def Cslib.TreeEval.Iter.instDecidableEqMode.decEq (x✝ x✝¹ : Mode) : Decidable (x✝ = x✝¹)

def Cslib.TreeEval.Iter.sgn {K : Type u_1} [Field K] (neg : Bool) : K

The coefficient of a sign.

@[simp]

theorem Cslib.TreeEval.Iter.path_cons (fr : Frame) (st : List Frame) : path (fr :: st) = path st ++ [fr.dir]

@[simp]

theorem Cslib.TreeEval.Iter.length_path (st : List Frame) : (path st).length = st.length

@[simp]

theorem Cslib.TreeEval.Iter.sgn_false {K : Type u_1} [Field K] : sgn false = 1

@[simp]

theorem Cslib.TreeEval.Iter.sgn_true {K : Type u_1} [Field K] : sgn true = -1

def Cslib.TreeEval.Iter.zmodUnit (p : ℕ) [Fact (Nat.Prime p)] (j : ℕ) : (ZMod p)ˣ

The units 1, …, p - 1 of ZMod p, in order: zmodUnit j is j + 1 for j < p - 1.

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

theorem Cslib.TreeEval.Iter.nodup_zmodUnits {p : ℕ} [Fact (Nat.Prime p)] : (List.map (zmodUnit p) (List.range (p - 1))).Nodup

theorem Cslib.TreeEval.Iter.mem_zmodUnits {p : ℕ} [Fact (Nat.Prime p)] (u : (ZMod p)ˣ) : u ∈ List.map (zmodUnit p) (List.range (p - 1))