Verilean / sparkle: RV32 Restoring Divider Hardware Proof (`Divider/Correct.lean`)
End-to-end cycle-34 correctness of a synthesized RISC-V 32-bit restoring divider hardware circuit (`dividerSignal`) on divide-by-zero and signed overflow boundary cases.
What was claimed: End-to-end cycle-34 correctness of a synthesized RISC-V 32-bit restoring divider hardware circuit (`dividerSignal`) on divide-by-zero and signed overflow boundary cases.
What Lean states: circuit_eq_run and 4 boundary theorems in Sparkle/Verification/Divider/Correct.lean (Verilean/sparkle at 1614cee8) — circuit_eq_run bridges dividerSignal at cycle 34 to pure runDiv; boundary theorems divu_by_zero, remu_by_zero, div_intmin_div_neg1, rem_intmin_rem_neg1 close via native_decide.
Prose only / the gap: General all-input V ≠ 0 theorems live in Sparkle.Verification.Divider.States33; dividerSignal_eq bridge is imported from Divider.Bridge.
Verification & replays: Static scan & 14 mutants generated by SeamCert (risk: elevated · 27, native_decide). Kernel replay not run.
What the public sources report
Every item below is attributed to the published paper, replay, or commentary that reported it.
| Bridge structure | circuit_eq_run rewrites the hardware signal (dividerSignal ...).val 34 to the pure functional model runDiv D V sgn rem using dividerSignal_eq from Sparkle.Verification.Divider.Bridge. [1] |
|---|---|
| Why SeamCert marks elevated risk (27) | The four concrete RISC-V boundary theorems (divu_by_zero, remu_by_zero, div_intmin_div_neg1, rem_intmin_rem_neg1) discharge evaluation over 34 cycles with by native_decide, introducing Lean.ofReduceBool. [1] |
| Custom definitions in file | startPulse (high only at t == 0) and runDiv (samples cycle 34 with Signal.pure constant operands). [1] |
Open specification seams (our reading)
Our reading of the sources above: the places where the formal Lean statement and the informal headline claim can still come apart.
native_decideon the 4 boundary theorems trusts the Lean compiler and any reachable@[implemented_by]/@[extern]inSignalorBitVec. Because these are concrete 34-cycle 32-bit vectors, replacingnative_decidewith kerneldecide(or auditing#print axioms) would remove the compiler-trust seam.circuit_eq_runholds for constantSignal.pure DandSignal.pure Vinputs withstartPulseat cycle 0; hardware integration must ensure operand lines are held stable across all 34 cycles.
Footnotes & Sources
Sources read on 7 November 2026. Spotted an error or a newer independent replay? Write to [email protected].