Static register-bank copies on the word RAM

copyBank copies a finite sequence of source registers into an injective destination bank using only native register-copy instructions, with a terminal self-copy on idle supplying the zero-length code case without inspecting the word width or requiring a positive-width constant.

Main definitions

• copyBank: copy k source registers into k destination registers, ending with an idle self-copy.

Main results

• copyBank_not_readsWidth: copying a finite register bank does not inspect the word width.
• copyBank_exec: copying k disjoint source registers into an injective destination bank takes k + 1 instructions, preserving memory and all registers outside the destination bank.

def Cslib.WordRAM.copyBank {B : Basis} {r k : ℕ} : (Fin k → Fin r) → (Fin k → Fin r) → Fin r → Code B r

Native register copies need no word-size or arithmetic side condition.

theorem Cslib.WordRAM.copyBank_not_readsWidth {B : Basis} {r k : ℕ} (src dst : Fin k → Fin r) (idle : Fin r) : ¬(copyBank src dst idle).ReadsWidth

Copying a finite bank does not inspect the word width.

theorem Cslib.WordRAM.copyBank_exec {B : Basis} {r k : ℕ} (src dst : Fin k → Fin r) (idle : Fin r) (hi : Function.Injective dst) (hd : ∀ (i j : Fin k), src i ≠ dst j) (w : ℕ) (x : Data r) : ∃ (y : Data r), ExecWithin w (copyBank src dst idle) x y (k + 1) ∧ y.mem = x.mem ∧ (∀ (i : Fin k), y.regs (dst i) = x.regs (src i)) ∧ ∀ (j : Fin r), (∀ (i : Fin k), dst i ≠ j) → y.regs j = x.regs j

Copy disjoint source words into an injective destination bank, leaving the entire memory and all other registers unchanged. A neutral copy supplies the zero-length code case.