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.capacity: number of non-workspace registers in a bank of n entries.
• 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

Every bank entry has exactly 18 physical registers.

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

Physical register indices in regs j lie in [44 + 18 * j, 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

Every register of regs j is a non-scratch digit register (IsDigit).

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

The register list regs j of a bank entry has no duplicates.

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

Distinct bank entries occupy disjoint lists of physical registers.

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.