Framed checked multiword arithmetic

The arithmetic programs reserve registers zero through three for workspace. Their frame preserves memory and every other register outside the destination list, including registers that are not source operands. Register lists are fixed when constructing the code.

Main definitions

• Arithmetic.Frame: preservation of all digit registers outside a destination list.
• Difference.truncatingProgram: subtraction with a branch that clears an underflowed result.

Main results

• Schoolbook.preserves_program: the syntactic register frame for schoolbook multiplication.
• Schoolbook.exec_framed: full multiplication with the digit-register frame.
• Schoolbook.exec_eighteen_framed: arbitrary layouts of eighteen-digit operands and a thirty-six-digit product, in exactly 2465 instructions.
• Difference.exec_framed: nonnegative subtraction with the digit-register frame.
• Difference.exec_eighteen_framed: eighteen-digit nonnegative subtraction in exactly 112 instructions.
• Difference.exec_eighteen_truncating: general eighteen-digit natural-number subtraction in at most 132 instructions, with the full digit-register frame.

References

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

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

Arithmetic preserves memory and all registers outside the destinations and the four reserved workspace registers.

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

Multiplication writes only destination digits and the four reserved workspace registers.

theorem Cslib.WordRAM.Multiword.Schoolbook.exec_framed {r w : ℕ} (hw : 2 ≤ w) (as bs ds os : List (Fin (r + 4))) (hlen : bs.length = ds.length) (hos : os.length = as.length) (hin : ∀ i ∈ as ++ bs, Workspace.IsDigit i) (hout : ∀ i ∈ ds ++ os, Workspace.IsDigit i) (hnd : (ds ++ os).Nodup) (hdis : (ds ++ os).Disjoint (as ++ bs)) (x : Data (r + 4)) (ha : Bounded (radix w) x as) (hb : Bounded (radix w) x bs) : ∃ (y : Data (r + 4)), Exec w (program as bs ds os) x y (7 + bs.length + rowCost as.length bs.length) ∧ Bounded (radix w) y (ds ++ os) ∧ value (radix w) y (ds ++ os) = value (radix w) x as * value (radix w) x bs ∧ Arithmetic.Frame x y (ds ++ os)

Full multiplication preserves every non-destination digit register. The destination lists and operands have arbitrary fixed lengths and arbitrary disjoint register layouts.

theorem Cslib.WordRAM.Multiword.Schoolbook.exec_eighteen_framed {r w : ℕ} (hw : 2 ≤ w) (as bs ds os : List (Fin (r + 4))) (has : as.length = 18) (hbs : bs.length = 18) (hds : ds.length = 18) (hos : os.length = 18) (hin : ∀ i ∈ as ++ bs, Workspace.IsDigit i) (hout : ∀ i ∈ ds ++ os, Workspace.IsDigit i) (hnd : (ds ++ os).Nodup) (hdis : (ds ++ os).Disjoint (as ++ bs)) (x : Data (r + 4)) (ha : Bounded (radix w) x as) (hb : Bounded (radix w) x bs) : ∃ (y : Data (r + 4)), Exec w (program as bs ds os) x y 2465 ∧ Bounded (radix w) y (ds ++ os) ∧ value (radix w) y (ds ++ os) = value (radix w) x as * value (radix w) x bs ∧ Arithmetic.Frame x y (ds ++ os)

An arbitrary eighteen-digit layout computes all thirty-six product digits in 2465 instructions while preserving every other digit register and memory.

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

Subtraction followed by clearing its output exactly when the final borrow is one. The second alternative is a self-copy, so both branches are executable for empty lists.

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

Truncating subtraction writes only its destinations and reserved workspace.

theorem Cslib.WordRAM.Multiword.Difference.size_truncatingProgram {r : ℕ} (w : ℕ) (bs ds : List (Fin (r + 4))) (hlen : bs.length = ds.length) : (truncatingProgram w bs ds).size = 7 * ds.length + 8

Exact static size of truncating subtraction, including both branch bodies.

theorem Cslib.WordRAM.Multiword.Difference.exec_truncating {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) : ∃ (y : Data (r + 4)), ExecWithin w (truncatingProgram w bs ds) x y (6 * ds.length + 4 + max (ds.length + 2) 3) ∧ Bounded (radix w) y ds ∧ value (radix w) y ds = value (radix w) x ds - value (radix w) x bs ∧ Arithmetic.Frame x y ds

General natural-number subtraction, including underflow. The result is Nat.sub, with bounded digits and preservation of every non-destination digit register and memory. The clear branch costs ds.length + 2; the other branch costs three instructions.

theorem Cslib.WordRAM.Multiword.Difference.exec_eighteen_truncating {r w : ℕ} (hw : 2 ≤ w) (bs ds : List (Fin (r + 4))) (hbslen : bs.length = 18) (hdslen : ds.length = 18) (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) : ∃ (y : Data (r + 4)), ExecWithin w (truncatingProgram w bs ds) x y 132 ∧ Bounded (radix w) y ds ∧ value (radix w) y ds = value (radix w) x ds - value (radix w) x bs ∧ Arithmetic.Frame x y ds

General eighteen-digit natural-number subtraction takes at most 132 instructions.

theorem Cslib.WordRAM.Multiword.Difference.exec_framed {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 ∧ Arithmetic.Frame x y ds

Nonnegative subtraction preserves every digit register outside its in-place output.

theorem Cslib.WordRAM.Multiword.Difference.exec_eighteen_framed {r w : ℕ} (hw : 2 ≤ w) (bs ds : List (Fin (r + 4))) (hbslen : bs.length = 18) (hdslen : ds.length = 18) (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 112 ∧ Bounded (radix w) y ds ∧ y.regs borrow = 0 ∧ value (radix w) y ds = value (radix w) x ds - value (radix w) x bs ∧ Arithmetic.Frame x y ds

Eighteen-digit nonnegative subtraction has an exact 112-instruction execution and preserves memory and every digit register outside the in-place destination list.