Checked multiword subtraction

Digits use the half-word radix β = 2 ^ (w / 2). A subtraction cell computes t = β + a - b - c, then returns t % β and borrow 1 - t / β. For digits a, b < β and incoming borrow c ≤ 1, all intermediate values fit the physical word, even at width two. In particular, no modular overflow is used.

Main definitions

• Difference.borrow, Difference.one: reserved borrow and constant-one workspace registers (sharing Workspace.total, Workspace.base, Workspace.IsDigit, and Workspace.Frame).
• Difference.cell, Difference.cellResult: six standard instructions for a digit and outgoing borrow, and their mathematical state update.
• Difference.digits, Difference.program: unrolled digit cells and the fixed-length, in-place multiword difference routine.

Main results

• Difference.exec_cell: checked execution and the exact borrow equation.
• Difference.exec: execution and reconstruction of a nonnegative difference.

References

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

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.Difference.borrow {r : ℕ} : Fin (r + 4)

Incoming and outgoing borrow, reusing workspace register 1 (Workspace.carry).

@[reducible, inline]

abbrev Cslib.WordRAM.Multiword.Difference.one {r : ℕ} : Fin (r + 4)

Preserved one, reusing workspace register 3 (Workspace.zero, which holds 0 in addition and 1 in subtraction).

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

Subtract one digit and the incoming borrow, replacing the minuend digit.

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

Exact result, including arithmetic workspace.

theorem Cslib.WordRAM.Multiword.Difference.exec_cell {r w : ℕ} (hw : 2 ≤ w) (x : Data (r + 4)) (b d : Fin (r + 4)) (hb : Workspace.IsDigit b) (hd : Workspace.IsDigit d) (hbase : x.regs Workspace.base = radix w) (hone : x.regs one = 1) (hxb : x.regs b < radix w) (hxd : x.regs d < radix w) (hc : x.regs borrow ≤ 1) : Exec w (cell b d) x (cellResult x b d) 6 ∧ (cellResult x b d).regs d < radix w ∧ (cellResult x b d).regs borrow ≤ 1 ∧ (cellResult x b d).regs d + x.regs b + x.regs borrow = x.regs d + radix w * (cellResult x b d).regs borrow ∧ Workspace.Frame x (cellResult x b d) [d]

Every cell uses six instructions, with a zero-or-one outgoing borrow and exact reconstruction. The equality accounts for the borrow at both ends.

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

Unroll the digit cells. The final self-copy also handles an empty list.

theorem Cslib.WordRAM.Multiword.Difference.size_digits {r : ℕ} (bs ds : List (Fin (r + 4))) (hlen : bs.length = ds.length) : (digits bs ds).size = 6 * ds.length + 1

Unrolling ds.length subtraction cells takes 6 * ds.length + 1 instructions.

theorem Cslib.WordRAM.Multiword.Difference.exec_digits {r w : ℕ} (hw : 2 ≤ w) (bs ds : List (Fin (r + 4))) (hlen : bs.length = ds.length) (hbs : ∀ b ∈ bs, Workspace.IsDigit b) (hds : ∀ d ∈ ds, Workspace.IsDigit d) (hnd : ds.Nodup) (hdis : bs.Disjoint ds) (x : Data (r + 4)) (hbase : x.regs Workspace.base = radix w) (hone : x.regs one = 1) (hb : Bounded (radix w) x bs) (hd : Bounded (radix w) x ds) (hc : x.regs borrow ≤ 1) : ∃ (y : Data (r + 4)), Exec w (digits bs ds) x y (6 * ds.length + 1) ∧ Bounded (radix w) y ds ∧ y.regs borrow ≤ 1 ∧ value (radix w) y ds + value (radix w) x bs + x.regs borrow = value (radix w) x ds + radix w ^ ds.length * y.regs borrow ∧ Workspace.Frame x y ds

Execute an entire subtraction, retaining a possible final borrow. Source digits and all registers outside the destinations and arithmetic workspaces are preserved.

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

Width-only constants, followed by a zero incoming borrow and the unrolled cells.

theorem Cslib.WordRAM.Multiword.Difference.size_program {r : ℕ} (w : ℕ) (bs ds : List (Fin (r + 4))) (hlen : bs.length = ds.length) : (program w bs ds).size = 6 * ds.length + 4

Exact instruction count of program, including the three constant-setup instructions.

theorem Cslib.WordRAM.Multiword.Difference.preserves_program {r : ℕ} (w : ℕ) (bs ds : List (Fin (r + 4))) (i : Fin (r + 4)) (hi : Workspace.IsDigit i) (hid : i ∉ ds) : Code.Preserves i (program w bs ds)

Only destinations and the four named workspace registers are written.

theorem Cslib.WordRAM.Multiword.Difference.exec {r w : ℕ} (hw : 2 ≤ w) (bs ds : List (Fin (r + 4))) (hlen : bs.length = ds.length) (hbs : ∀ b ∈ bs, Workspace.IsDigit b) (hds : ∀ d ∈ ds, Workspace.IsDigit d) (hnd : ds.Nodup) (hdis : bs.Disjoint ds) (x : Data (r + 4)) (hb : Bounded (radix w) x bs) (hd : Bounded (radix w) x ds) (hle : value (radix w) x bs ≤ value (radix w) x ds) : ∃ (y : Data (r + 4)), Exec w (program w bs ds) x y (6 * ds.length + 4) ∧ Bounded (radix w) y ds ∧ y.regs borrow = 0 ∧ value (radix w) y ds = value (radix w) x ds - value (radix w) x bs ∧ y.mem = x.mem ∧ ∀ i ∈ bs, y.regs i = x.regs i

Nonnegative multiword subtraction, with charged constant installation and no preloaded radix or borrow. The running time depends only on the number of digits.