Linear-time canonical binary subtraction -- pure proofs

The raw scan is verified through the standard full-subtractor invariant. Its final borrow decides underflow, while trimming is proved to recover the canonical Nat.bits representation of the raw fixed-width value.

def Complexity.BinaryRippleSub.boolValue (bit : Bool) : ℕ

Interpret a Boolean bit as a natural number.

Equations

• Complexity.BinaryRippleSub.boolValue bit = if bit = true then 1 else 0

theorem Complexity.BinaryRippleSub.scan_bits_length_internal (borrow : Bool) (lhs rhs : List Bool) : (scan borrow lhs rhs).bits.length = max lhs.length rhs.length

The raw borrow scan writes exactly the larger input width.

theorem Complexity.BinaryRippleSub.scan_value_internal (borrow : Bool) (lhs rhs : List Bool) : (Nat.fromBitsLE lhs + if (scan borrow lhs rhs).borrow = true then 2 ^ max lhs.length rhs.length else 0) = Nat.fromBitsLE rhs + boolValue borrow + Nat.fromBitsLE (scan borrow lhs rhs).bits

Arithmetic invariant for the fixed-width borrow scan. The final borrow is the coefficient of the width-sized wraparound term.

theorem Complexity.BinaryRippleSub.trimHighZeros_append_false_internal (bits : List Bool) : trimHighZeros (bits ++ [false]) = trimHighZeros bits

Appending a redundant high zero does not change canonical trimming.

theorem Complexity.BinaryRippleSub.trimHighZeros_append_true_internal (bits : List Bool) : trimHighZeros (bits ++ [true]) = bits ++ [true]

A high one makes the entire lower prefix significant.

theorem Complexity.BinaryRippleSub.trimHighZeros_eq_natBits_internal (bits : List Bool) : trimHighZeros bits = (Nat.fromBitsLE bits).bits

Trimming arbitrary little-endian bits produces the canonical bits of their decoded natural value.

theorem Complexity.BinaryRippleSub.subtract_natBits_internal (lhs rhs : ℕ) : subtract lhs.bits rhs.bits = (lhs - rhs).bits

The canonical pure subtraction result agrees with natural-number monus.

theorem Complexity.BinaryRippleSub.length_subtract_natBits_internal (lhs rhs : ℕ) : (subtract lhs.bits rhs.bits).length = (lhs - rhs).size

Canonical subtraction has exactly the width of natural-number monus.

theorem Complexity.TM.binaryRippleSubScanTime_natBits_internal (lhs rhs : ℕ) : binaryRippleSubScanTime lhs.bits rhs.bits = max lhs.size rhs.size + 1

The scan bound on canonical operands is the larger natural-number width.

theorem Complexity.TM.binaryRippleSubCleanupTime_natBits_internal (lhs rhs : ℕ) : binaryRippleSubCleanupTime lhs.bits rhs.bits = max lhs.size rhs.size + 1

The cleanup bound equals the scan bound on canonical operands.

theorem Complexity.TM.binaryRippleSubCoreTime_natBits_internal (lhs rhs : ℕ) : binaryRippleSubCoreTime lhs.bits rhs.bits = 2 * max lhs.size rhs.size + 2

The core bound is twice the larger width plus its two turning steps.

theorem Complexity.TM.binaryRippleSubTime_le_internal (lhs rhs : ℕ) : binaryRippleSubTime lhs rhs ≤ 3 * (lhs.size + rhs.size) + 10

The complete subtractor is linear in the sum of the operand widths.