Checked operations on multiword register banks

The constants are installed as explicit half-word digits. Boolean operations execute one standard instruction per digit. Scalar arithmetic is provided separately in BankScalar.

Main definitions

• Bank.constantDigits, Bank.constant: canonical eighteen-digit decomposition and installation of a width-dependent constant.
• Bank.boolean: limbwise Boolean operations.
• Bank.inputReg, Bank.allRegs, Bank.clear, Bank.input: the physical input register, the list of all bank digit registers, bank initialization, and input loading.

Main results

• Bank.exec_constant, Bank.exec_boolean: execution and preservation of the other bank entries.

References

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

def Cslib.WordRAM.Multiword.Bank.constantDigits (w z : ℕ) : List ℕ

Canonical fixed-length digits; no computation depending on the run-time input is performed by the constant installer.

def Cslib.WordRAM.Multiword.Bank.constant {n : ℕ} (w z : ℕ) (d : Fin n) : Code Basis.standard (capacity n + 4)

Install an eighteen-digit constant, charging all eighteen constants and the final copy.

theorem Cslib.WordRAM.Multiword.Bank.size_constant {n : ℕ} (w z : ℕ) (d : Fin n) : (constant w z d).size = 19

Installing an eighteen-digit constant takes 19 instructions.

theorem Cslib.WordRAM.Multiword.Bank.exec_constant {n w : ℕ} (hw : 2 ≤ w) (d : Fin n) (z : ℕ) (hz : z < 2 ^ (6 * w)) (x : Data (capacity n + 4)) {v : Fin n → ℕ} (hx : Encodes w x v) : ∃ (y : Data (capacity n + 4)), Exec w (constant w z d) x y 19 ∧ Encodes w y (Function.update v d z) ∧ y.mem = x.mem ∧ ∀ i ∉ regs d, y.regs i = x.regs i

Executing constant w z d installs z in bank entry d in 19 instructions, preserving memory and all other registers.

def Cslib.WordRAM.Multiword.Bank.boolean {n : ℕ} (f : BinOp) (a b d : Fin n) : Code Basis.standard (capacity n + 4)

A Boolean operation on two bank entries with a fresh destination.

theorem Cslib.WordRAM.Multiword.Bank.size_boolean {n : ℕ} (f : BinOp) (a b d : Fin n) : (boolean f a b d).size = 19

A limbwise Boolean operation on two bank entries takes 19 instructions.

theorem Cslib.WordRAM.Multiword.Bank.exec_boolean {n w : ℕ} (hw : 2 ≤ w) {f : BinOp} (hf : Bitwise.Supported f) (a b d : Fin n) (hda : d ≠ a) (hdb : d ≠ b) (x : Data (capacity n + 4)) {v : Fin n → ℕ} (hx : Encodes w x v) : ∃ (y : Data (capacity n + 4)), Exec w (boolean f a b d) x y 19 ∧ Encodes w y (Function.update v d (f.eval (v a) (v b))) ∧ y.mem = x.mem

Executing boolean f a b d writes f.eval (v a) (v b) to bank entry d in 19 instructions, preserving memory and all other bank entries.

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.Bank.inputReg {n : ℕ} : Fin (capacity n + 4)

Physical register receiving the ordinary one-word input.

def Cslib.WordRAM.Multiword.Bank.allRegs (n : ℕ) : List (Fin (capacity n + 4))

All bank digits, excluding the forty-four physical workspace registers.

def Cslib.WordRAM.Multiword.Bank.clear (n : ℕ) : Code Basis.standard (capacity n + 4)

Initialize every bank digit, charging one constant instruction per digit.

theorem Cslib.WordRAM.Multiword.Bank.size_clear (n : ℕ) : (clear n).size = 18 * n + 1

Clearing n bank entries takes 18 * n + 1 instructions.

theorem Cslib.WordRAM.Multiword.Bank.exec_clear {n w : ℕ} (hw : 2 ≤ w) (x : Data (capacity n + 4)) : ∃ (y : Data (capacity n + 4)), Exec w (clear n) x y (18 * n + 1) ∧ (Encodes w y fun (x : Fin n) => 0) ∧ y.mem = x.mem ∧ y.regs inputReg = x.regs inputReg

Clearing starts from arbitrary registers and memory, and preserves the physical input.

def Cslib.WordRAM.Multiword.Bank.input {n : ℕ} (d : Fin n) : Code Basis.standard (capacity n + 4)

Load the sole input from the usual RAM input memory, then split it into a bank entry. The input memory contains its length at address zero and its value at address one.

theorem Cslib.WordRAM.Multiword.Bank.size_input {n : ℕ} (d : Fin n) : (input d).size = 46

Loading and splitting the one-word input into a bank entry takes 46 instructions.

theorem Cslib.WordRAM.Multiword.Bank.exec_input {n w z : ℕ} (hw : 2 ≤ w) (hz : Fits w z) (d : Fin n) : ∃ (y : Data (capacity n + 4)), Exec w (input d) (Data.init [z]) y 46 ∧ Encodes w y (Function.update (fun (x : Fin n) => 0) d z) ∧ y.mem = (Data.init [z]).mem ∧ y.regs inputReg = z

Input delivery and conversion are charged: two input instructions and forty-four digit-conversion instructions. All remaining bank entries start at zero.