Arithmetic instruction graphs for multiword RAM execution

Virtual registers are eighteen-digit entries of Multiword.Bank. A binary node names only standard RAM operations. Its execution is implemented by the checked digit routines rather than by enlarging the RAM's operation basis or physical width.

Main definitions

• Circuit.Operation: a constant or a binary standard operation on virtual registers.
• Circuit.Operation.eval: the mathematical value of one node.

References

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

inductive Cslib.WordRAM.Multiword.Circuit.Operation (n : ℕ) : Type

A node in a fixed register graph. Constants may depend on the physical width at code construction time; the two arguments of a binary node are run-time register values.

• constant {n : ℕ} (z : ℕ) : Operation n
• binary {n : ℕ} (f : BinOp) (a b : Fin n) : Operation n

@[instance_reducible]

instance Cslib.WordRAM.Multiword.Circuit.instDecidableEqOperation {n✝ : ℕ} : DecidableEq (Operation n✝)

def Cslib.WordRAM.Multiword.Circuit.instDecidableEqOperation.decEq {n✝ : ℕ} (x✝ x✝¹ : Operation n✝) : Decidable (x✝ = x✝¹)

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

Natural-number specification of a virtual instruction.

def Cslib.WordRAM.Multiword.Circuit.Operation.Earlier {n : ℕ} (d : Fin n) : Operation n → Prop

Sources are earlier nodes in the instruction graph.

def Cslib.WordRAM.Multiword.Circuit.Operation.Admissible {n : ℕ} (w : ℕ) (v : Fin n → ℕ) (o : Operation n) : Prop

Bounds needed by the concrete compiler. Multiplication, subtraction and Boolean operations use digit routines. A right-shift count is reconstructed as a physical scalar; the remaining operations use fitting physical operands and a fitting physical result.