Shared workspace for multiword operations

Register zero stores an arithmetic total, register one a carry, register two the half-word radix, and register three a preserved zero. All operand digits lie outside this workspace. Multiplication, transfers, bitwise operations and shifts share this layout.

Main definitions

• Workspace.IsDigit: a register outside the four reserved registers.
• Workspace.Frame: memory and registers outside destinations and arithmetic scratch are kept.
• Workspace.setup: initialize the radix and zero in six checked instructions.

Main results

• Workspace.exec_setup: exact initialization at every physical width at least two.
• Workspace.setup_digit: initialization leaves operand digits unchanged.

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.Workspace.total {r : ℕ} : Fin (r + 4)

Arithmetic total and partial-sum workspace.

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.Workspace.carry {r : ℕ} : Fin (r + 4)

Carry workspace.

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.Workspace.base {r : ℕ} : Fin (r + 4)

Half-word radix.

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.Workspace.zero {r : ℕ} : Fin (r + 4)

A preserved zero, used for padding and shifts.

def Cslib.WordRAM.Multiword.Workspace.IsDigit {r : ℕ} (i : Fin (r + 4)) : Prop

Registers outside the four reserved workspace registers.

theorem Cslib.WordRAM.Multiword.Workspace.digit_ne {r : ℕ} {i : Fin (r + 4)} (hi : IsDigit i) : i ≠ total ∧ i ≠ carry ∧ i ≠ base ∧ i ≠ zero

Digit registers are disjoint from the four reserved workspace registers.

def Cslib.WordRAM.Multiword.Workspace.Frame {r : ℕ} (x y : Data (r + 4)) (ds : List (Fin (r + 4))) : Prop

A routine changes only its destination digits and the total and carry workspace.

theorem Cslib.WordRAM.Multiword.Workspace.frame_mono {r : ℕ} {x y : Data (r + 4)} {ds es : List (Fin (r + 4))} (h : Frame x y ds) (hsub : ds ⊆ es) : Frame x y es

Enlarging the destination set weakens the preservation requirement.

theorem Cslib.WordRAM.Multiword.Workspace.frame_trans {r : ℕ} {x y z : Data (r + 4)} {ds : List (Fin (r + 4))} (h : Frame x y ds) (h' : Frame y z ds) : Frame x z ds

Two routines with the same frame compose.

def Cslib.WordRAM.Multiword.Workspace.setup {r : ℕ} : Code Basis.standard (r + 4)

Compute the half-word radix and a preserved zero in six standard instructions.

def Cslib.WordRAM.Multiword.Workspace.setupResult {r : ℕ} (w : ℕ) (x : Data (r + 4)) : Data (r + 4)

Exact workspace contents after initialization.

theorem Cslib.WordRAM.Multiword.Workspace.exec_setup {r w : ℕ} (hw : 2 ≤ w) (x : Data (r + 4)) : Exec w setup x (setupResult w x) 6

Initialization executes in exactly six instructions for every width at least two.

theorem Cslib.WordRAM.Multiword.Workspace.setup_digit {r : ℕ} (w : ℕ) (x : Data (r + 4)) {i : Fin (r + 4)} (hi : IsDigit i) : (setupResult w x).regs i = x.regs i

Initialization preserves every register outside the reserved workspace.