Correctness of the Tree Evaluation read machine

Run on the encoding of an instance, Cslib.TreeEval.Reader.machine halts with the value of the tree as its output: a call on a subtree performs the procedure Cslib.TreeEval.proc on it and returns, by induction on the subtree, with the rounds of a gate, the reading of a leaf and the pass over the table of a gate as loops of their own.

Main results

• Cslib.TreeEval.Reader.exists_runFrom_call: a call on a subtree performs the procedure and returns.
• Cslib.TreeEval.Reader.exists_run_eq: the machine halts with the value of the tree.

@[simp]

theorem Cslib.TreeEval.Reader.getElem?_encode_body {ℓ H : ℕ} (T : Tree ℓ H) (k : ℕ) : T.encode[ℓ + (H + (2 + k))]? = T.body[k]?

The input at an offset into the body, in the form produced by simp.

@[reducible, inline]

abbrev Cslib.TreeEval.Reader.cfg {ℓ H : ℕ} (p : ℕ) (R : Regs) (st : List Iter.Frame) (mode : Iter.Mode) (ctl : Ctl) (out : List Bool) : Turing.ReadMachine.Cfg State

A configuration of the machine on T, running with the prime p.

theorem Cslib.TreeEval.Reader.tableBit_mul_add {ℓ : ℕ} (f : Gate ℓ) (k : ℕ) (i : Fin ℓ) : tableBit f (k * ℓ + ↑i) = f (lowBits ℓ k) (highBits ℓ k) i

The bit of a table at position k * ℓ + i.

def Cslib.TreeEval.Reader.CallSpec {ℓ H : ℕ} (T : Tree ℓ H) (p : ℕ) [Fact (Nat.Prime p)] (P : List Bool) (pl : ZMod p → Fin 3 → TreeEval.State (ZMod p) ℓ → TreeEval.State (ZMod p) ℓ) : Prop

The hypothesis that calls on the subtree at a path perform pl.

theorem Cslib.TreeEval.Reader.exists_runFrom_call {ℓ H : ℕ} {T : Tree ℓ H} {p : ℕ} [Fact (Nat.Prime p)] {d : ℕ} (U : Tree ℓ d) (st : List Iter.Frame) : (∀ (Q : List Bool), T.nodeAt (Iter.path st ++ Q) = U.nodeAt Q) → CallSpec T p (Iter.path st) (proc (List.map (Iter.zmodUnit p) (List.range (p - 1))) U)

A call on a subtree at the path of the stack performs the procedure on it and returns, for every initial content of the registers.

The header, the prime and the output

theorem Cslib.TreeEval.Reader.getElem?_encode_lt_ell {ℓ H : ℕ} {T : Tree ℓ H} {n : ℕ} (hn : n < ℓ) : T.encode[n]? = some true

theorem Cslib.TreeEval.Reader.getElem?_encode_ell {ℓ H : ℕ} {T : Tree ℓ H} : T.encode[ℓ]? = some false

theorem Cslib.TreeEval.Reader.getElem?_encode_height {ℓ H : ℕ} {T : Tree ℓ H} {n : ℕ} (hn : n < H) : T.encode[ℓ + 1 + n]? = some true

theorem Cslib.TreeEval.Reader.getElem?_encode_height_end {ℓ H : ℕ} {T : Tree ℓ H} : T.encode[ℓ + 1 + H]? = some false

def Cslib.TreeEval.Reader.primeFor (ℓ : ℕ) : ℕ

The least prime p ≥ 2ℓ + 2.

theorem Cslib.TreeEval.Reader.primeFor_prime (ℓ : ℕ) : Nat.Prime (primeFor ℓ)

theorem Cslib.TreeEval.Reader.le_primeFor (ℓ : ℕ) : 2 * ℓ + 2 ≤ primeFor ℓ

theorem Cslib.TreeEval.Reader.exists_run_eq {ℓ H : ℕ} (T : Tree ℓ H) : ∃ (n : ℕ) (s : State), machine.run T.encode n = { state := s, out := List.ofFn T.eval } ∧ machine.halt s = true

The read machine evaluates the tree. On the encoding of an instance it halts, with the value of the tree as its output.