Offsets of nodes within linear work space

The offset of the node at a path is a fold over the path from the root: a step adds the length of a table and, to the right child, the length of the body of the left one. With the lengths computed by iteration, and the path read off the stack, it is tidily computable within work space linear in the encoded stack, the height and the value length.

Main results

• Cslib.TreeEval.Reader.foldl_pathStep: the offset as a fold over the path.
• Cslib.TreeEval.Reader.pathOffset_inSpace: the offset within linear work space.

Folding over the path

def Cslib.TreeEval.Reader.pathStep (ℓ : ℕ) (s : ℕ × ℕ) (b : Bool) : ℕ × ℕ

A step of the offset along a path from the root, on the height left and the sum.

theorem Cslib.TreeEval.Reader.foldl_pathStep (ℓ : ℕ) (P : List Bool) (d acc : ℕ) : List.foldl (pathStep ℓ) (d, acc) P = (d - P.length, acc + pathOffset ℓ d P)

The offset as a fold over the path: folding pathStep ℓ over P from the height d and the sum acc gives the height d - P.length and the sum acc + pathOffset ℓ d P.

theorem Cslib.TreeEval.Reader.path_eq_reverse (st : List Iter.Frame) : Iter.path st = (List.map Iter.Frame.dir st).reverse

theorem Cslib.TreeEval.Reader.foldl_cons_dir (st : List Iter.Frame) (acc : List Bool) : List.foldl (fun (acc : List Bool) (fr : Iter.Frame) => fr.dir :: acc) acc st = (List.map Iter.Frame.dir st).reverse ++ acc

Certificates

theorem Cslib.TreeEval.Reader.length_tableLength_le (ℓ : ℕ) : (Turing.MultiTapeTM.encNat (tableLength ℓ)).length ≤ 3 * ℓ + 1

theorem Cslib.TreeEval.Reader.tableLength_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace tableLength Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat fun (ℓ : ℕ) => 4096 * (ℓ + 1)

The length of a table, 4^ℓ * ℓ from ℓ.

Frames

@[reducible, inline]

abbrev Cslib.TreeEval.Reader.encFrameTuple : ℕ × Fin 4 × Bool × Fin 3 ↪ List Bool

The encoding of tuples of frames.

theorem Cslib.TreeEval.Reader.encFrame_apply (fr : Iter.Frame) : encFrame fr = encFrameTuple (Frame.equiv fr)

theorem Cslib.TreeEval.Reader.frameFinite_inSpace {β : Type} {encB : β ↪ List Bool} (g : Fin 4 × Bool × Fin 3 → β) : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (fr : Iter.Frame) => g (Frame.equiv fr).2) encFrame encB fun (fr : Iter.Frame) => (encFrame fr).length

A function of the finite fields of a frame.

theorem Cslib.TreeEval.Reader.round_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (fr : Iter.Frame) => fr.round) encFrame Turing.MultiTapeTM.encNat fun (fr : Iter.Frame) => (encFrame fr).length

The round of a frame.

The offset of the node at the path of a stack

theorem Cslib.TreeEval.Reader.dirs_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (st : List Iter.Frame) => List.foldl (fun (acc : List Bool) (fr : Iter.Frame) => fr.dir :: acc) [] st) (Turing.MultiTapeTM.encList encFrame) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool) fun (st : List Iter.Frame) => 64 * (((Turing.MultiTapeTM.encList encFrame) st).length + 1)

theorem Cslib.TreeEval.Reader.pathOffset_inSpace : Turing.MultiTapeTM.ComputableTidilyInSpace (fun (q : (ℕ × ℕ) × List Bool) => pathOffset q.1.1 q.1.2 q.2) (Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) Turing.MultiTapeTM.encNat fun (q : (ℕ × ℕ) × List Bool) => 2 ^ 30 * (q.1.1 + q.1.2 + ((Turing.MultiTapeTM.encPair (Turing.MultiTapeTM.encPair Turing.MultiTapeTM.encNat Turing.MultiTapeTM.encNat) (Turing.MultiTapeTM.encList Turing.MultiTapeTM.encBool)) q).length + 1)

The offset of the node at a path, pathOffset ℓ d P from ((ℓ, d), P).