Checked multiword right shifts

Whole half-word digits are skipped by subtracting the half width from a physical scalar. The remaining shift is division by a power of two, performed from high digits to low digits with a remainder carry. Each intermediate is strictly below the square of the digit radix.

Main definitions

• Cslib.WordRAM.Multiword.Shift.program: variable right shift with fixed register lists.

Main results

• Cslib.WordRAM.Multiword.Shift.exec: bounded digits, exact reconstruction and a frame.
• Cslib.WordRAM.Multiword.Shift.exec_eighteen: the eighteen-digit bank interface.

The code may depend on the physical width through constants. Its size and runtime bounds depend only on the digit counts. Inputs and outputs are disjoint little-endian digit lists; the scalar is a separate physical word. All four reserved registers may change.

References

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

def Cslib.WordRAM.Multiword.Shift.cell {r : ℕ} (a d : Fin (r + 4)) : Code Basis.standard (r + 4)

One division digit. base is the radix, zero the divisor, and total the shift.

def Cslib.WordRAM.Multiword.Shift.cellResult {r : ℕ} (x : Data (r + 4)) (a d : Fin (r + 4)) : Data (r + 4)

Full result of a division digit, including the remainder workspace.

def Cslib.WordRAM.Multiword.Shift.digits {r : ℕ} : List (Fin (r + 4)) → List (Fin (r + 4)) → Code Basis.standard (r + 4)

Divide from high to low, padding the high output digits with zeros.

theorem Cslib.WordRAM.Multiword.Shift.size_digits {r : ℕ} (as ds : List (Fin (r + 4))) (hlen : as.length ≤ ds.length) : (digits as ds).size = ds.length + 3 * as.length + 1

def Cslib.WordRAM.Multiword.Shift.finish {r : ℕ} (as ds : List (Fin (r + 4))) : Code Basis.standard (r + 4)

Set up the residual power-of-two divisor and divide the remaining digits.

def Cslib.WordRAM.Multiword.Shift.dispatch {r : ℕ} : List (Fin (r + 4)) → List (Fin (r + 4)) → Code Basis.standard (r + 4)

Branch through the possible whole-digit shifts. Exhausting the input clears the output.

def Cslib.WordRAM.Multiword.Shift.codeSize : ℕ → ℕ → ℕ

Exact instruction-list size before the three-instruction initialization.

theorem Cslib.WordRAM.Multiword.Shift.size_dispatch {r : ℕ} (as ds : List (Fin (r + 4))) (hlen : as.length ≤ ds.length) : (dispatch as ds).size = codeSize as.length ds.length

def Cslib.WordRAM.Multiword.Shift.program {r : ℕ} (w : ℕ) (as ds : List (Fin (r + 4))) (s : Fin (r + 4)) : Code Basis.standard (r + 4)

Initialize the radix, half width and scalar shift, then execute checked division.

theorem Cslib.WordRAM.Multiword.Shift.size_program {r : ℕ} (w : ℕ) (as ds : List (Fin (r + 4))) (s : Fin (r + 4)) (hlen : as.length ≤ ds.length) : (program w as ds s).size = 3 + codeSize as.length ds.length

theorem Cslib.WordRAM.Multiword.Shift.exec {r w : ℕ} (hw : 2 ≤ w) (as ds : List (Fin (r + 4))) (s : Fin (r + 4)) (hlen : as.length ≤ ds.length) (hin : ∀ i ∈ as, Workspace.IsDigit i) (hout : ∀ i ∈ ds, Workspace.IsDigit i) (hsdigit : Workspace.IsDigit s) (hnd : ds.Nodup) (hdis : ds.Disjoint as) (hsout : s ∉ ds) (x : Data (r + 4)) (ha : Bounded (radix w) x as) (hs : Fits w (x.regs s)) : ∃ (y : Data (r + 4)), ExecWithin w (program w as ds s) x y (ds.length + 3 * as.length + 7) ∧ Bounded (radix w) y ds ∧ value (radix w) y ds = value (radix w) x as >>> x.regs s ∧ Workspace.Frame x y (Workspace.base :: Workspace.zero :: ds) ∧ y.regs s = x.regs s

Variable right shift from a physical scalar word. The output is padded to its fixed length. All arithmetic, including construction of the residual power of two, is checked at width w. The frame preserves memory and every register outside the output and reserved workspace.

theorem Cslib.WordRAM.Multiword.Shift.regs_eq_of_frame {r : ℕ} {x y : Data (r + 4)} {ds : List (Fin (r + 4))} (hf : Workspace.Frame x y (Workspace.base :: Workspace.zero :: ds)) {i : Fin (r + 4)} (hi : Workspace.IsDigit i) (hnot : i ∉ ds) : y.regs i = x.regs i

Extract the outside-output register guarantee from the complete four-register frame.

theorem Cslib.WordRAM.Multiword.Shift.shiftRight_eq_zero {r w s : ℕ} (hw : 2 ≤ w) (x : Data (r + 4)) (as : List (Fin (r + 4))) (ha : Bounded (radix w) x as) (hs : w / 2 * as.length ≤ s) : value (radix w) x as >>> s = 0

A shift beyond the full digit capacity is zero. Combined with exec, this also describes the runtime's large-shift branch, without requiring its scalar to fit the digit radix.

theorem Cslib.WordRAM.Multiword.Shift.codeSize_le (m n : ℕ) : codeSize m n ≤ (m + 1) * (n + 3 * m + 6)

A quadratic instruction-list bound, independent of the physical word width.

theorem Cslib.WordRAM.Multiword.Shift.size_program_eighteen {r : ℕ} (w : ℕ) (as ds : List (Fin (r + 4))) (s : Fin (r + 4)) (has : as.length = 18) (hds : ds.length = 18) : (program w as ds s).size = 970

Eighteen input and output digits have exactly 970 compiled instructions.

theorem Cslib.WordRAM.Multiword.Shift.exec_eighteen {r w : ℕ} (hw : 2 ≤ w) (as ds : List (Fin (r + 4))) (s : Fin (r + 4)) (has : as.length = 18) (hds : ds.length = 18) (hin : ∀ i ∈ as, Workspace.IsDigit i) (hout : ∀ i ∈ ds, Workspace.IsDigit i) (hsdigit : Workspace.IsDigit s) (hnd : ds.Nodup) (hdis : ds.Disjoint as) (hsout : s ∉ ds) (x : Data (r + 4)) (ha : Bounded (radix w) x as) (hs : Fits w (x.regs s)) : ∃ (y : Data (r + 4)), ExecWithin w (program w as ds s) x y 79 ∧ Bounded (radix w) y ds ∧ value (radix w) y ds = value (radix w) x as >>> x.regs s ∧ Workspace.Frame x y (Workspace.base :: Workspace.zero :: ds) ∧ ∀ (i : Fin (r + 4)), Workspace.IsDigit i → i ∉ ds → y.regs i = x.regs i

The MSB bank's eighteen-digit shift takes at most 79 instructions, including initialization. Every non-output register numbered at least four is preserved, including the scalar.