Scalar operations and variable shifts on multiword banks

Scalar operations assemble both operands before writing the destination, so the destination may coincide with either source. Their inputs and result must fit the physical word width. Variable right shifts assemble only the shift amount; the shifted input remains multiword.

Main definitions

• Bank.scalar: a checked physical binary operation between bank entries.
• Bank.shift: a variable right shift into a distinct bank entry.

Main results

• Bank.exec_scalar: exact execution in 133 instructions, preserving other entries and memory.
• Bank.exec_shift: execution within 123 instructions, preserving other entries and memory.

References

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

@[reducible, inline]

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

Physical register four stores the assembled left operand or shift amount.

@[reducible, inline]

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

Physical register five stores the assembled right operand.

@[reducible, inline]

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

Physical register six stores the checked scalar result.

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

Assemble into physical registers four and five, compute in register six, and split the checked result into the destination. Both inputs are read before any bank entry is written.

theorem Cslib.WordRAM.Multiword.Bank.size_scalar {n : ℕ} (f : BinOp) (a b d : Fin n) : (scalar f a b d).size = 133

Scalar operations compile to exactly 133 instructions, independently of word width.

theorem Cslib.WordRAM.Multiword.Bank.exec_scalar {n w : ℕ} (hw : 2 ≤ w) (f : BinOp) (a b d : Fin n) (x : Data (capacity n + 4)) {v : Fin n → ℕ} (hx : Encodes w x v) (hfa : Fits w (v a)) (hfb : Fits w (v b)) (hresult : Fits w (f.eval (v a) (v b))) : ∃ (y : Data (capacity n + 4)), Exec w (scalar f a b d) x y 133 ∧ Encodes w y (Function.update v d (f.eval (v a) (v b))) ∧ y.mem = x.mem

Checked scalar arithmetic permits either source to coincide with the destination.

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

Assemble the scalar shift amount in physical register four, then shift the multiword input. The destination must be distinct from the input, but may contain the original shift amount.

theorem Cslib.WordRAM.Multiword.Bank.size_shift {n : ℕ} (w : ℕ) (a b d : Fin n) : (shift w a b d).size = 1014

The compiled size is independent of physical word width.

theorem Cslib.WordRAM.Multiword.Bank.exec_shift {n w : ℕ} (hw : 2 ≤ w) (a b d : Fin n) (hda : d ≠ a) (x : Data (capacity n + 4)) {v : Fin n → ℕ} (hx : Encodes w x v) (hfb : Fits w (v b)) : ∃ (y : Data (capacity n + 4)), ExecWithin w (shift w a b d) x y 123 ∧ Encodes w y (Function.update v d (v a >>> v b)) ∧ y.mem = x.mem

Multiword right shifts require only the shift amount to fit a physical word.