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.cell: six standard instructions for a digit and outgoing borrow.
• Difference.program: a fixed-length, in-place multiword difference.

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.total {r : ℕ} : Fin (r + 4)

Arithmetic workspace.

@[reducible, inline]

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

Incoming and outgoing borrow.

@[reducible, inline]

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

Half-word radix.

@[reducible, inline]

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

Preserved one.

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

Registers available for operand digits.

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

Only destination digits and the two arithmetic workspaces may change.

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 : IsDigit b) (hd : IsDigit d) (hbase : x.regs 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 ∧ 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

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, IsDigit b) (hds : ∀ d ∈ ds, IsDigit d) (hnd : ds.Nodup) (hdis : bs.Disjoint ds) (x : Data (r + 4)) (hbase : x.regs 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 ∧ 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

theorem Cslib.WordRAM.Multiword.Difference.preserves_program {r : ℕ} (w : ℕ) (bs ds : List (Fin (r + 4))) (i : Fin (r + 4)) (hi : 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, IsDigit b) (hds : ∀ d ∈ ds, 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.