Carry-Save Step Definition

def Sparkle.Verification.MulProps.carrySaveStep (rd rdx rs1 rs2 : BitVec 64) : BitVec 64 × BitVec 64 × BitVec 64 × BitVec 64

One iteration of carry-save shift-and-add multiplication. Models PicoRV32 pcpi_mul with CARRY_CHAIN=0 (pure carry-save).

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Verification.MulProps.carrySaveN : Nat → BitVec 64 → BitVec 64 → BitVec 64 → BitVec 64 → BitVec 64 × BitVec 64 × BitVec 64 × BitVec 64

N iterations of carry-save shift-and-add.

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.Verification.MulProps.carrySaveN 0 x✝³ x✝² x✝¹ x✝ = (x✝³, x✝², x✝¹, x✝)

Core Lemma: Carry-Save Addition Identity

For any three bitvectors a, b, c: (a ^^^ b ^^^ c) + (((a &&& b) ||| (a &&& c) ||| (b &&& c)) <<< 1) = a + b + c

This is the fundamental property of carry-save adders: XOR computes the sum bits, majority computes the carry bits, and shifting the carry left by 1 propagates it to the next bit position.

theorem Sparkle.Verification.MulProps.carrySave_add_eq_4 (a b c : BitVec 4) : (a ^^^ b ^^^ c) + (a &&& b ||| a &&& c ||| b &&& c) <<< 1 = a + b + c

Carry-save addition identity for 4-bit vectors.

theorem Sparkle.Verification.MulProps.carrySave_add_eq_8 (a b c : BitVec 8) : (a ^^^ b ^^^ c) + (a &&& b ||| a &&& c ||| b &&& c) <<< 1 = a + b + c

Carry-save addition identity for 8-bit vectors.

Concrete Correctness Verification

We verify the carry-save algorithm produces correct results for specific test vectors using native_decide. These cover all MUL variants used by the MulOracle and serve as regression tests.

theorem Sparkle.Verification.MulProps.mul_7_6 : match carrySaveN 32 0 0 7 6 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 42

7 * 6 = 42

theorem Sparkle.Verification.MulProps.mul_100_100 : match carrySaveN 32 0 0 100 100 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 10000

100 * 100 = 10000

theorem Sparkle.Verification.MulProps.mul_12345_6789 : match carrySaveN 32 0 0 12345 6789 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 83810205

12345 * 6789 = 83810205

theorem Sparkle.Verification.MulProps.mul_0_anything : match carrySaveN 32 0 0 0 42 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 0

0 * x = 0

theorem Sparkle.Verification.MulProps.mul_anything_0 : match carrySaveN 32 0 0 42 0 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 0

x * 0 = 0

theorem Sparkle.Verification.MulProps.mul_1_1 : match carrySaveN 32 0 0 1 1 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 1

1 * 1 = 1

theorem Sparkle.Verification.MulProps.mul_362880_10 : match carrySaveN 32 0 0 362880 10 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 3628800

Factorial: 362880 * 10 = 3628800

theorem Sparkle.Verification.MulProps.mul_ffff_ffff : match carrySaveN 32 0 0 65535 65535 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 4294836225

Large: 0xFFFF * 0xFFFF = 0xFFFE0001

theorem Sparkle.Verification.MulProps.mul_256_256 : match carrySaveN 32 0 0 256 256 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 65536

Power of 2: 256 * 256 = 65536

theorem Sparkle.Verification.MulProps.mul_1_max : match carrySaveN 32 0 0 1 4294967295 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 4294967295

Asymmetric: 1 * 0xFFFFFFFF

theorem Sparkle.Verification.MulProps.mul_max_2 : match carrySaveN 32 0 0 4294967295 2 with | (rd, rdx, fst, snd) => rd ^^^ rdx = 8589934590

Large product: 0xFFFFFFFF * 2

Parametric Proof: Carry-Save Addition = True Addition

The carry-save identity holds for all bit widths. We prove it parametrically using the fact that for each bit position i: xor(a[i], b[i], c[i]) = (a[i] + b[i] + c[i]) mod 2 majority(a[i], b[i], c[i]) = (a[i] + b[i] + c[i]) / 2

The carry propagation via left-shift gives us a ripple-add.

theorem Sparkle.Verification.MulProps.full_adder_bit (a b c : Bool) : (a.toNat ^^^ b.toNat ^^^ c.toNat) + 2 * (a.toNat &&& b.toNat ||| a.toNat &&& c.toNat ||| b.toNat &&& c.toNat) = a.toNat + b.toNat + c.toNat

Full adder identity at the bit level: For single bits, xor is sum and majority is carry.

Loop Invariant and Main Theorem

The main correctness theorem states that after n steps of carry-save shift-and-add starting from (0, 0, rs1, rs2):

rd + rdx = (lower n bits of rs1) * rs2

We prove this by induction, using carrySave_add_eq at each step.

theorem Sparkle.Verification.MulProps.carrySave_add_eq_64 (a b c : BitVec 64) : (a ^^^ b ^^^ c) + (a &&& b ||| a &&& c ||| b &&& c) <<< 1 = a + b + c

Carry-save addition identity for 64-bit vectors. Proved by bv_decide (SAT-based bitvector decision procedure).

theorem Sparkle.Verification.MulProps.step_sum_invariant (rd rdx rs1 rs2 : BitVec 64) : match carrySaveStep rd rdx rs1 rs2 with | (rd', rdx', fst, snd) => rd' + rdx' = rd + rdx + if rs1.getLsbD 0 = true then rs2 else 0

After one step: rd' + rdx' = rd + rdx + partial_product. This holds because carry-save addition preserves the sum.

theorem Sparkle.Verification.MulProps.step_shifts (rd rdx rs1 rs2 : BitVec 64) : (carrySaveStep rd rdx rs1 rs2).snd.snd.fst = rs1 >>> 1 ∧ (carrySaveStep rd rdx rs1 rs2).snd.snd.snd = rs2 <<< 1

Shift properties of carrySaveStep.

def Sparkle.Verification.MulProps.carrySaveStep4 (rd rdx rs1 rs2 : BitVec 4) : BitVec 4 × BitVec 4 × BitVec 4 × BitVec 4

Small-width carry-save equals multiplication (4-bit, 2 steps). Proves the full equivalence for small inputs via bv_decide.

Equations

• One or more equations did not get rendered due to their size.

def Sparkle.Verification.MulProps.carrySaveN4 : Nat → BitVec 4 → BitVec 4 → BitVec 4 → BitVec 4 → BitVec 4 × BitVec 4 × BitVec 4 × BitVec 4

Equations

• One or more equations did not get rendered due to their size.
• Sparkle.Verification.MulProps.carrySaveN4 0 x✝³ x✝² x✝¹ x✝ = (x✝³, x✝², x✝¹, x✝)

theorem Sparkle.Verification.MulProps.carrySave_eq_mul_4 (a b : BitVec 4) : match carrySaveN4 4 0 0 a b with | (rd, rdx, fst, snd) => rd ^^^ rdx = a * b

4-bit carry-save multiplication: 4 steps of shift-and-add = multiply. Proved by bv_decide (exhaustive SAT over all 4-bit inputs).

theorem Sparkle.Verification.MulProps.oracle_correct_concrete_7_6 : have a := 7; have b := 6; match carrySaveN 32 0 0 a b with | (rd, rdx, fst, snd) => rd ^^^ rdx = a * b

Oracle correctness: for 32-bit unsigned multiply, carrySaveN 32 matches direct multiplication. Verified by concrete examples; parametric proof depends on carrySave_add_eq_64 + induction (WIP).

theorem Sparkle.Verification.MulProps.oracle_correct_concrete_12345_6789 : have a := 12345; have b := 6789; match carrySaveN 32 0 0 a b with | (rd, rdx, fst, snd) => rd ^^^ rdx = a * b

theorem Sparkle.Verification.MulProps.oracle_correct_concrete_362880_10 : have a := 362880; have b := 10; match carrySaveN 32 0 0 a b with | (rd, rdx, fst, snd) => rd ^^^ rdx = a * b