Compiling virtual arithmetic into checked standard RAM instructions

Each instruction graph node is expanded into concrete half-word arithmetic. Multiplication uses the schoolbook program, subtraction propagates and checks a borrow, and shifts use the checked digit division routine. Every emitted program has at most 4000 instructions and executes within the same bound, independently of the physical width.

Main definitions

• Circuit.emit: concrete standard-basis code for one virtual instruction.

Main results

• Circuit.exec_emit: checked execution of a node, with a frame for the other bank entries.

References

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

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

Compile one virtual instruction, preserving the original physical word width and standard operation basis.

theorem Cslib.WordRAM.Multiword.Circuit.size_emit {n : ℕ} (w : ℕ) (d : Fin n) (op : Operation n) : (emit w d op).size ≤ 4000

Static code length has a uniform bound, including branch bodies that are not executed.

theorem Cslib.WordRAM.Multiword.Circuit.exec_emit {n w : ℕ} (hw : 2 ≤ w) (d : Fin n) (op : Operation n) (x : Data (Bank.capacity n + 4)) {v : Fin n → ℕ} (hx : Bank.Encodes w x v) (hearlier : Operation.Earlier d op) (hadm : Operation.Admissible w v op) : ∃ (y : Data (Bank.capacity n + 4)), ExecWithin w (emit w d op) x y 4000 ∧ Bank.Encodes w y (Function.update v d (Operation.eval v op)) ∧ y.mem = x.mem

Every node executes through the concrete checked routines. The hypotheses assert only source ordering and numerical bounds; they contain no wide-operation correctness oracle.