Fixed banks of multiword registers

Each bank entry contains eighteen little-endian half-word digits. The first forty-four physical registers are reserved for arithmetic and transfer workspaces. Register indices are part of the code, so even width two requires no address large enough to name the bank.

Main definitions

• Bank.regs: the eighteen registers of a bank entry.
• Bank.Encodes: bounded digits with specified reconstructed bank values.

Main results

• Bank.encodes_update: composition through a framed update of one bank entry.

References

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

def Cslib.WordRAM.Multiword.Bank.capacity (n : ℕ) : ℕ

Number of non-workspace registers in a bank with n entries.

def Cslib.WordRAM.Multiword.Bank.regs {n : ℕ} (j : Fin n) : List (Fin (capacity n + 4))

The fixed eighteen-digit register list for entry j.

theorem Cslib.WordRAM.Multiword.Bank.length_regs {n : ℕ} (j : Fin n) : (regs j).length = 18

theorem Cslib.WordRAM.Multiword.Bank.mem_regs {n : ℕ} {j : Fin n} {i : Fin (capacity n + 4)} (hi : i ∈ regs j) : 44 + 18 * ↑j ≤ ↑i ∧ ↑i < 44 + 18 * ↑j + 18

theorem Cslib.WordRAM.Multiword.Bank.digit_regs {n : ℕ} (j : Fin n) (i : Fin (capacity n + 4)) : i ∈ regs j → Workspace.IsDigit i

theorem Cslib.WordRAM.Multiword.Bank.nodup_regs {n : ℕ} (j : Fin n) : (regs j).Nodup

theorem Cslib.WordRAM.Multiword.Bank.disjoint_regs {n : ℕ} {j k : Fin n} (hjk : j ≠ k) : (regs j).Disjoint (regs k)

def Cslib.WordRAM.Multiword.Bank.Encodes {n : ℕ} (w : ℕ) (x : Data (capacity n + 4)) (v : Fin n → ℕ) : Prop

Bounded half-word digits and the values of all virtual registers.

theorem Cslib.WordRAM.Multiword.Bank.encodes_update {n w : ℕ} {x y : Data (capacity n + 4)} {v : Fin n → ℕ} (hx : Encodes w x v) (d : Fin n) (z : ℕ) (hy : Bounded (radix w) y (regs d)) (hz : value (radix w) y (regs d) = z) (hp : ∀ (i : Fin (capacity n + 4)), 44 ≤ ↑i → i ∉ regs d → y.regs i = x.regs i) : Encodes w y (Function.update v d z)

Updating one entry preserves the encodings of every other entry. Workspace registers below forty-four may change freely.

theorem Cslib.WordRAM.Multiword.Bank.six_word_capacity {w : ℕ} (hw : 2 ≤ w) : 2 ^ (6 * w) ≤ radix w ^ 18

Every six-word value fits in one bank entry, including odd physical widths.