Exhaust the input space wherever it is small: 33.7M inputs, C == Rust, seven seconds - #2199
Merged
Conversation
docs/POSITIONING.md established that multi-target emission is table stakes and that formal equivalence checking is stronger than what we do. It also named the one thing that is ours: ternary primitives have input spaces small enough to enumerate. A space you can exhaust needs neither a sample nor a prover. Coverage was four specs. ternary_ripple_adder.t27 generates 167 lines of C and had no cross-target check at all, despite containing the ternary full adder -- the core combinational cell of the line. full_adder(u8,u8,u8) 16,777,216 inputs C == Rust 1.5s maj3(u8,u8,u8) 16,777,216 inputs C == Rust 1.3s tmul(u8,u8) 65,536 inputs C == Rust 1.2s pack2(u8,u8) 65,536 inputs C == Rust 1.4s negate(u8) 256 inputs C == Rust 1.3s 33.7 million inputs, exhaustively, in about seven seconds. No sampling. What it does not prove is printed on every run: this compares C against Rust, so a fault shared by both backends -- a spec bug, or shared front-end lowering -- is invisible. verify_igla_race.py keeps the stronger form for ternary_mul, where an independent Python model is the third opinion. 'C == Rust on all inputs' and 'C == Rust == model on all inputs' are different claims and the first is easy to mistake for the second. Negative control: perturbing the C side at exactly one input out of 65,536 moves the digest 91a68892 -> b7b51485. It runs as its own CI step, ahead of the check. Two costs worth recording. The generated C emits assert_eq() from the spec's test blocks with no declaration, needing the same shim the existing harness uses. And my first failure output truncated to five stderr lines which were all -Wparentheses-equality warnings, hiding the real error underneath; the helper now prefers lines containing error:. A diagnostic that truncates can hide the thing it exists to show. Closes #2198 Refs #2197 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
This was referenced Aug 18, 2026
gHashTag
added a commit
that referenced
this pull request
Aug 18, 2026
#2199 shipped exhaustive cross-target checking and printed a limitation on every run: C against Rust only, so a fault shared by both backends -- a spec bug or shared front-end lowering -- was invisible. 'The backends agree' and 'the backends both match the specification' are different claims, and the first is easy to mistake for the second. tools/ternary_model.py is an independent transcription of the primitives, read from specs/ternary/ternary_ripple_adder.t27 and re-expressed in Python. It was NOT derived from the generated C or Rust; had it been, it would agree by construction and prove nothing. Transcribed faithfully, including what looks wrong: pack2 does not mask its arguments to two bits, so a value above 3 spills into the neighbouring trit lane. A model that 'fixed' that would report a divergence which is really the model disagreeing with the specification it exists to encode. full_adder(u8,u8,u8) 16,777,216 inputs model == C == Rust maj3(u8,u8,u8) 16,777,216 inputs model == C == Rust tmul(u8,u8) 65,536 inputs model == C == Rust pack2(u8,u8) 65,536 inputs model == C == Rust negate(u8) 256 inputs model == C == Rust 33.7 million inputs, three independent implementations, about eight seconds. Two negative controls, because the model arm needed its own. Perturbing C proves the C/Rust comparison has resolution; it says nothing about whether a model disagreeing with BOTH backends would be noticed, which is the entire reason the model exists. one-input perturbation of C 91a68892 -> b7b51485 one-input perturbation of MODEL 91a68892 -> cea51633, backends 91a68892 Measured rather than guessed: pure Python did not finish full_adder's 16.7M inputs in 600s -- nine dot27 calls per input, 27 lanes each, ~4e9 operations. Memoising dot27, a pure function whose semantics are untouched by it, took the rate from 179k calls/s to 2.2M/s. Targets added to TARGETS without a model entry stay two-way and are labelled [2-way: no model entry], so the weaker case cannot pass itself off as the stronger. Closes #2200 Refs #2198 Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
docs/POSITIONING.md(#2197) established that emitting several targets from one source is table stakes — Chisel/FIRRTL/CIRCT has done Verilog plus a C++ simulator for years — and that proving target equivalence is industrial practice by stronger methods than ours (HECTOR, ACL2/RAC, both proving over all inputs).It also named the one thing that is genuinely ours: ternary primitives have input spaces small enough to enumerate. A space you can exhaust needs neither a sample nor a prover.
Coverage before this PR: four specs.
ternary_mac,systolic_ternary,gft_smul,gft_sadd.ternary_ripple_adder.t27generates 167 lines of C and had no cross-target check at all, despite containing the ternary full adder — the core combinational cell of the whole line.After:
full_adder(u8,u8,u8)maj3(u8,u8,u8)tmul(u8,u8)pack2(u8,u8)negate(u8)33.7 million inputs, exhaustively, in about seven seconds. No sampling.
What this does NOT prove, stated in the tool's own output on every run. It compares C against Rust. A fault shared by both backends — a spec bug, or shared front-end lowering — is invisible to it.
verify_igla_race.pycarries the stronger form forternary_mul, where an independent Python model is the third opinion. "C == Rust on all inputs" and "C == Rust == independent model on all inputs" are different claims, and the first is easy to mistake for the second.Negative control: perturbing the C side at exactly one input out of 65,536 changes the digest (
91a68892→b7b51485), so the comparison has full resolution and is not vacuous. It runs as its own CI step, before the check.Two things this cost me, both worth recording. The generated C emits
assert_eq()from the spec'stestblocks with no declaration — the same#define assert_eq(x,y) ((void)0)shim the existing harness uses. And my first failure output truncated to the first five stderr lines, which were-Wparentheses-equalitywarnings, hiding the actual error underneath; the helper now prefers lines containingerror:. A diagnostic that truncates can hide the thing it exists to show.Refs #2197
Closes #2198
🤖 Generated with Claude Code