Sequential execution of multiword instruction graphs

An instruction graph whose sources precede their destinations can be executed in node order. The execution theorem composes a checked implementation of each node over the standard RAM basis. It tracks the encoded prefix, instruction count, and preservation of memory.

Main definitions

• Circuit.prefix: completed node values, with future entries zeroed.
• Circuit.run: sequential composition of a supplied node compiler.

Main results

• Circuit.size_run: a linear code-size bound from the node-size bound.
• Circuit.exec_run: a linear execution bound from the checked node-execution contract.

References

• Cormen, Leiserson, Rivest and Stein, Introduction to Algorithms.

def Cslib.WordRAM.Multiword.Circuit.prefix {n : ℕ} (v : Fin n → ℕ) (k : ℕ) : Fin n → ℕ

Values of completed nodes, with future entries zeroed.

theorem Cslib.WordRAM.Multiword.Circuit.update_prefix {n : ℕ} (v : Fin n → ℕ) (d : Fin n) : Function.update («prefix» v ↑d) d (v d) = «prefix» v (↑d + 1)

Completing the next node extends the encoded prefix by one entry.

theorem Cslib.WordRAM.Multiword.Circuit.Operation.eval_congr {n : ℕ} {d : Fin n} {op : Operation n} {v u : Fin n → ℕ} (he : Earlier d op) (h : ∀ (j : Fin n), ↑j < ↑d → v j = u j) : eval v op = eval u op

Evaluation depends only on the earlier source values of a node.

theorem Cslib.WordRAM.Multiword.Circuit.Operation.admissible_congr {n w : ℕ} {d : Fin n} {op : Operation n} {v u : Fin n → ℕ} (he : Earlier d op) (h : ∀ (j : Fin n), ↑j < ↑d → v j = u j) : Admissible w v op ↔ Admissible w u op

The admissibility bounds depend only on the earlier source values of a node.

def Cslib.WordRAM.Multiword.Circuit.nop {n : ℕ} : Code Basis.standard (Bank.capacity n + 4)

A one-instruction terminator that copies a workspace register to itself.

def Cslib.WordRAM.Multiword.Circuit.run {n : ℕ} (emit : Fin n → Operation n → Code Basis.standard (Bank.capacity n + 4)) (ops : Fin n → Operation n) (k : ℕ) : ℕ → Code Basis.standard (Bank.capacity n + 4)

Execute up to fuel consecutive nodes, stopping at the end of the graph.

theorem Cslib.WordRAM.Multiword.Circuit.size_run {n : ℕ} (emit : Fin n → Operation n → Code Basis.standard (Bank.capacity n + 4)) (hsize : ∀ (d : Fin n) (op : Operation n), (emit d op).size ≤ 4000) (ops : Fin n → Operation n) (k fuel : ℕ) : (run emit ops k fuel).size ≤ fuel * 4000 + 1

A node compiler of size at most four thousand gives a linear compiled-size bound.

theorem Cslib.WordRAM.Multiword.Circuit.exec_run {n : ℕ} (emit : Fin n → Operation n → Code Basis.standard (Bank.capacity n + 4)) {w : ℕ} (hnode : ∀ (d : Fin n) (op : Operation n) (x : Data (Bank.capacity n + 4)) (v : Fin n → ℕ), Operation.Earlier d op → Operation.Admissible w v op → Bank.Encodes w x v → ∃ (y : Data (Bank.capacity n + 4)), ExecWithin w (emit d op) x y 4000 ∧ Bank.Encodes w y (Function.update v d (Operation.eval v op)) ∧ y.mem = x.mem) (ops : Fin n → Operation n) (v : Fin n → ℕ) (k fuel : ℕ) (hbound : k + fuel ≤ n) (hgraph : ∀ (i : Fin n), k ≤ ↑i → ↑i < k + fuel → Operation.Earlier i (ops i) ∧ Operation.eval v (ops i) = v i ∧ Operation.Admissible w v (ops i)) (x : Data (Bank.capacity n + 4)) (hx : Bank.Encodes w x («prefix» v k)) : ∃ (y : Data (Bank.capacity n + 4)), ExecWithin w (run emit ops k fuel) x y (fuel * 4000 + 1) ∧ Bank.Encodes w y («prefix» v (k + fuel)) ∧ y.mem = x.mem

Sequential composition of checked node executions reconstructs the prescribed graph values. Only nodes in the executed interval need satisfy the graph specification.