Checked transfers between scalar words and digit lists

Register lists and supplied constants determine the unrolled standard-basis code. Digits are little endian in the half-word radix. Registers zero through three are reserved workspace.

Main definitions

• Cslib.WordRAM.Multiword.Transfer.copy: copy disjoint equal-length register lists.
• Cslib.WordRAM.Multiword.Transfer.constants: install a supplied list of constants.
• Cslib.WordRAM.Multiword.Transfer.assemble: reconstruct a scalar from digit registers.
• Cslib.WordRAM.Multiword.Transfer.split: split a physical scalar into digit registers.

Main results

• Cslib.WordRAM.Multiword.Transfer.exec_copy: exact copying and register preservation.
• Cslib.WordRAM.Multiword.Transfer.exec_constants: exact installation of bounded constants.
• Cslib.WordRAM.Multiword.Transfer.exec_assemble: reconstruction when the scalar fits.
• Cslib.WordRAM.Multiword.Transfer.exec_split_eighteen: exact eighteen-digit conversion.

References

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

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

Copy one register per instruction, with a final workspace self-copy.

theorem Cslib.WordRAM.Multiword.Transfer.size_copy {r : ℕ} (as ds : List (Fin (r + 4))) (hlen : as.length = ds.length) : (copy as ds).size = ds.length + 1

Exact width-independent code size.

theorem Cslib.WordRAM.Multiword.Transfer.exec_copy {r w : ℕ} (as ds : List (Fin (r + 4))) (hlen : as.length = ds.length) (hnd : ds.Nodup) (hdis : ds.Disjoint as) (x : Data (r + 4)) : ∃ (y : Data (r + 4)), Exec w (copy as ds) x y (ds.length + 1) ∧ List.map y.regs ds = List.map x.regs as ∧ Workspace.Frame x y ds ∧ ∀ i ∉ ds, y.regs i = x.regs i

Copying preserves the exact digit sequence, memory, and every register outside the outputs. Source registers need not be distinct.

theorem Cslib.WordRAM.Multiword.Transfer.value_copy {r β : ℕ} {x y : Data (r + 4)} {as ds : List (Fin (r + 4))} (h : List.map y.regs ds = List.map x.regs as) : value β y ds = value β x as

Exact reconstruction follows from the copied digit sequence, at any radix.

theorem Cslib.WordRAM.Multiword.Transfer.bounded_copy {r β : ℕ} {x y : Data (r + 4)} {as ds : List (Fin (r + 4))} (h : List.map y.regs ds = List.map x.regs as) (hb : Bounded β x as) : Bounded β y ds

Copying an exact digit sequence preserves its digit bound.

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

Install supplied constants; they may depend on the physical width but not runtime data.

theorem Cslib.WordRAM.Multiword.Transfer.size_constants {r : ℕ} (ds : List (Fin (r + 4))) (cs : List ℕ) (hlen : ds.length = cs.length) : (constants ds cs).size = ds.length + 1

Exact width-independent instruction count for supplied constants.

theorem Cslib.WordRAM.Multiword.Transfer.exec_constants {r w : ℕ} (ds : List (Fin (r + 4))) (cs : List ℕ) (hlen : ds.length = cs.length) (hnd : ds.Nodup) (hfit : ∀ c ∈ cs, Fits w c) (x : Data (r + 4)) : ∃ (y : Data (r + 4)), Exec w (constants ds cs) x y (ds.length + 1) ∧ List.map y.regs ds = cs ∧ Workspace.Frame x y ds ∧ ∀ i ∉ ds, y.regs i = x.regs i

Constants are checked against the physical width. No initial destination contents matter.

theorem Cslib.WordRAM.Multiword.Transfer.exec_digits {r w : ℕ} (hw : 2 ≤ w) (ds : List (Fin (r + 4))) (cs : List ℕ) (hlen : ds.length = cs.length) (hnd : ds.Nodup) (hb : ∀ c ∈ cs, c < radix w) (x : Data (r + 4)) : ∃ (y : Data (r + 4)), Exec w (constants ds cs) x y (ds.length + 1) ∧ Bounded (radix w) y ds ∧ value (radix w) y ds = Nat.ofDigits (radix w) cs ∧ Workspace.Frame x y ds ∧ ∀ i ∉ ds, y.regs i = x.regs i

Installing bounded digits gives the requested value in the half-word radix.

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

Reconstruct by Horner evaluation, high digits first, into workspace register zero.

theorem Cslib.WordRAM.Multiword.Transfer.size_accumulate {r : ℕ} (as : List (Fin (r + 4))) : (accumulate as).size = 2 * as.length + 1

Horner evaluation costs two instructions per digit plus initialization.

def Cslib.WordRAM.Multiword.Transfer.assemble {r : ℕ} (as : List (Fin (r + 4))) (d : Fin (r + 4)) : Code Basis.standard (r + 4)

Initialize the radix, reconstruct, and copy to the physical destination register.

theorem Cslib.WordRAM.Multiword.Transfer.size_assemble {r : ℕ} (as : List (Fin (r + 4))) (d : Fin (r + 4)) : (assemble as d).size = 2 * as.length + 8

Assembly has a linear instruction count independent of the physical width.

theorem Cslib.WordRAM.Multiword.Transfer.exec_assemble {r w : ℕ} (hw : 2 ≤ w) (as : List (Fin (r + 4))) (d : Fin (r + 4)) (hin : ∀ i ∈ as, Workspace.IsDigit i) (x : Data (r + 4)) (hfit : Fits w (value (radix w) x as)) : ∃ (y : Data (r + 4)), Exec w (assemble as d) x y (2 * as.length + 8) ∧ y.regs d = value (radix w) x as ∧ Workspace.Frame x y [Workspace.base, Workspace.zero, d] ∧ ∀ (i : Fin (r + 4)), Workspace.IsDigit i → i ≠ d → y.regs i = x.regs i

Reconstruction is checked at the original physical width. All intermediate Horner values fit because the nonnegative final scalar fits. Inputs are preserved when disjoint from d. The frame includes the radix and zero workspace alongside the destination.

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

Extract low digits by remainder and division, retaining the final quotient in total.

theorem Cslib.WordRAM.Multiword.Transfer.size_extract {r : ℕ} (ds : List (Fin (r + 4))) : (extract ds).size = 2 * ds.length + 1

Two checked instructions per extracted digit, followed by a workspace self-copy.

def Cslib.WordRAM.Multiword.Transfer.split {r : ℕ} (a : Fin (r + 4)) (ds : List (Fin (r + 4))) : Code Basis.standard (r + 4)

Initialize the half-word radix and extract a scalar into fixed output registers.

theorem Cslib.WordRAM.Multiword.Transfer.size_split {r : ℕ} (a : Fin (r + 4)) (ds : List (Fin (r + 4))) : (split a ds).size = 2 * ds.length + 8

Conversion has a linear width-independent instruction count, including radix setup.

theorem Cslib.WordRAM.Multiword.Transfer.exec_split {r w : ℕ} (hw : 2 ≤ w) (a : Fin (r + 4)) (ds : List (Fin (r + 4))) (ha : Workspace.IsDigit a) (hout : ∀ i ∈ ds, Workspace.IsDigit i) (hnd : ds.Nodup) (x : Data (r + 4)) (hfit : Fits w (x.regs a)) (hcap : x.regs a < radix w ^ ds.length) : ∃ (y : Data (r + 4)), Exec w (split a ds) x y (2 * ds.length + 8) ∧ Bounded (radix w) y ds ∧ value (radix w) y ds = x.regs a ∧ Workspace.Frame x y (Workspace.base :: Workspace.zero :: ds) ∧ ∀ (i : Fin (r + 4)), Workspace.IsDigit i → i ∉ ds → y.regs i = x.regs i

Exact conversion when the supplied digit list has enough capacity. The input may occur among the outputs: its value is copied into workspace before any digit is written.

theorem Cslib.WordRAM.Multiword.Transfer.exec_split_eighteen {r w : ℕ} (hw : 2 ≤ w) (a : Fin (r + 4)) (ds : List (Fin (r + 4))) (hlen : ds.length = 18) (ha : Workspace.IsDigit a) (hout : ∀ i ∈ ds, Workspace.IsDigit i) (hnd : ds.Nodup) (x : Data (r + 4)) (hfit : Fits w (x.regs a)) : ∃ (y : Data (r + 4)), Exec w (split a ds) x y 44 ∧ Bounded (radix w) y ds ∧ value (radix w) y ds = x.regs a ∧ Workspace.Frame x y (Workspace.base :: Workspace.zero :: ds) ∧ ∀ (i : Fin (r + 4)), Workspace.IsDigit i → i ∉ ds → y.regs i = x.regs i

Eighteen half-word digits suffice for every physical scalar at widths at least two, including odd widths. This conversion always executes exactly 44 instructions.