Skip to content

Verilog as the fourth arm, a nightly that exhausts it, and the theory that says why - #2203

Merged
gHashTag merged 2 commits into
masterfrom
loop/t27-verilog-exh
Aug 18, 2026
Merged

Verilog as the fourth arm, a nightly that exhausts it, and the theory that says why#2203
gHashTag merged 2 commits into
masterfrom
loop/t27-verilog-exh

Conversation

@gHashTag

@gHashTag gHashTag commented Aug 18, 2026 •
edited
Loading

Copy link
Copy Markdown
Owner

Verilog is the target that actually goes to silicon, and it was the least verified of the four: verify_emit_bitexact.py checks it by sample, while model/C/Rust are now exhaustive (#2200).

This adds Verilog as a fourth arm, under iverilog, folding the same FNV-1a digest over the same domain.

Result:

full_adder   model == C == Rust on ALL 16,777,216 inputs   digest d50715c5
             Verilog == model on a SLICE of 65,536 (0.4% of the domain)
maj3         model == C == Rust on ALL 16,777,216 inputs   digest 80f1d1c5
             Verilog == model on a SLICE of 524,288 (3.1% of the domain)
tmul         model == C == Rust == Verilog on ALL 65,536 inputs   digest 91a68892
negate       model == C == Rust == Verilog on ALL    256 inputs   digest eeede76b
pack2        model == C == Rust on ALL 65,536 inputs [3-way: no Verilog arm]

tmul and negate now have four independent implementations agreeing on every input.

Why the others are slices, measured rather than assumed. iverilog is an interpreter and the cost per input is not uniform:

function inputs/s whole domain
tmul ~330,000 0.2 s
maj3 21,061 13 min
full_adder 2,972 94 min

full_adder calls dot27 nine times per input at 27 lanes each. So the Verilog arm gets a budget and reports a labelled slice where the whole domain does not fit. A slice is never printed as exhaustive, and --verilog-full runs the long version.

Three mistakes of mine in this PR, all caught before it opened.

  1. I measured tmul's Verilog rate and extrapolated to full_adder — which does nine times the work per input. The run timed out at ten minutes. Measuring one thing and extrapolating to another is the error this whole line of work exists to catch.
  2. I then set the budget in inputs, a unit whose cost varies 100× across these functions, so one number was seconds for tmul and eleven minutes for full_adder. The budget is now in seconds, converted per function from the measured rates.
  3. The summary line read ALL 5 PRIMITIVES AGREE EXHAUSTIVELY across every arm (no sampling) — false for three of the five, while the per-line detail above it was correct. A summary that overstates its own detail is the exact failure this session has been finding elsewhere.

pack2 returns u64; the C and Rust folds take the low 32 bits and a matching Verilog fold needs a wider accumulator. Left three-way and labelled rather than quietly given a Verilog arm that compares something else.

Refs #2200

Two things the previous PRs left open, plus the theory that says why they matter.

1. --verilog-full as a nightly job. #2202 gates on a labelled Verilog slice because iverilog needs 13 minutes for maj3 and 94 for full_adder at its measured rates (21,061 and 2,972 inputs/s). Unacceptable per push; fine once a day. The slice keeps gating; this closes it, giving four independent implementations agreeing on all 16,777,216 inputs rather than on 0.4 % of them.

2. docs/EXHAUSTION_THEORY.md — why this line of work is worth the wall-clock, stated precisely.

The point, in three steps

Exhaustive agreement over a finite domain is a decision procedure, not a test. For f_A, f_B : D → R with D finite, checking equality on every x ∈ D decides f_A ≡ f_B. No induction, no invariants, no trusted prover kernel. It is not a weaker substitute for formal EC — on a finite domain it is the strongest statement available, and it is what HECTOR and ACL2 approximate when D is too large to walk.

|D| is set by the representation, not the semantics. A trit carries three values; these specs declare it u8.

Claim. For k trit arguments in a w-bit type, enumeration costs (2^w / 3)^k times more than the semantic domain requires.
Proof. Semantic domain 3^k; representational (2^w)^k; ratio (2^w/3)^k. ∎
Check. w=8, k=3 → (256/3)³ = 621,378.4. Measured here: 16,777,216 / 27 = 621,378.4. ✓

Only 1.61 × 10⁻⁶ of full_adder's enumerated space is a valid trit triple.

Both readings of that are true. It is waste — a 2-bit trit type would put full_adder at 4³ = 64 inputs, which iverilog finishes in 0.02 s instead of 94 minutes, a four-million-fold change from a type declaration with no algorithmic change. And it is coverage — nothing stops a caller passing 200, the spec has defined behaviour there (pack2 does not mask, so values above 3 spill into the next lane), and enumerating the byte-wide domain verifies it. A 2-bit type would make those inputs unrepresentable rather than verified: better, but a different guarantee, not the same one made cheaper.

Why this is a property of the number system

domain |D| C, ~10⁷/s iverilog, measured
trit primitive, 2-bit type, k=3 64 instant instant
trit primitive, u8, k=2 65,536 instant 0.2 s
trit primitive, u8, k=3 16,777,216 ~1.5 s 13–94 min
binary float add, 2 × 32-bit 1.8 × 10¹⁹ 58,561 years —

The line between enumerate and prove is crossed by representation width, and small alphabets sit below it. That is the one place choosing ternary buys a verification advantage rather than an area or energy claim — and unlike the area claims in this project's history, which were withdrawn twice, this one follows from counting and can be rechecked by anyone in seconds.

Refs #2202, #2200

Closes #2202
Closes #2204

🤖 Generated with Claude Code

@gHashTag @claude
verify: add Verilog as the fourth arm
737d430 
Verilog is the target that goes to silicon and was the least verified of the four:
verify_emit_bitexact.py samples it, while model/C/Rust became exhaustive in #2200.
It now folds the same FNV-1a digest over the same domain under iverilog.

  tmul, negate               four implementations agreeing on EVERY input
  full_adder, maj3           model/C/Rust exhaustive; Verilog on a labelled slice
  pack2                      three-way, labelled: u64 return needs a wider fold

Why slices, measured rather than assumed. iverilog is an interpreter and the cost
per input is not uniform: tmul ~330,000/s, maj3 21,061/s, full_adder 2,972/s,
because full_adder calls dot27 nine times per input at 27 lanes each. The whole
domains are 13 and 94 minutes. The Verilog arm therefore has a budget and prints a
labelled slice where the domain does not fit. A slice is never printed as
exhaustive; --verilog-full runs the long version.

Three of my own errors, all caught before this opened:

  I measured tmul's rate and extrapolated to full_adder, which does nine times the
  work per input. The run timed out at ten minutes. Measuring one thing and
  extrapolating to another is the error this line of work exists to catch.

  I then set the budget in INPUTS -- a unit whose cost varies 100x across these
  functions, so one number was seconds for tmul and eleven minutes for full_adder.
  The budget is in seconds now, converted per function from the measured rates.

  The summary line read 'ALL 5 PRIMITIVES AGREE EXHAUSTIVELY across every arm',
  false for three of the five, while the per-line detail above it was correct. A
  summary that overstates its own detail is the exact failure this session has
  been finding elsewhere.

Closes #2202
Refs #2200

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Aug 18, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-08-18 14:59:23 UTC

Summary

Status Count
Total Open PRs 29
PRs with Failing Checks 12
PRs with All Checks Green 17
READY 9
FAILING 12
PENDING 0

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=cd2822f290eb != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@github-actions

github-actions Bot commented Aug 18, 2026

Copy link
Copy Markdown
Contributor

📓 NotebookLM Notebook linked to this PR

This notebook contains session context, decisions, and artifacts for this work.

@gHashTag @claude
ci+docs: nightly --verilog-full, and why exhaustion is a decision pro…
23465f9 
…cedure

The per-PR gate runs the Verilog arm on a labelled slice because iverilog needs 13
minutes for maj3 and 94 for full_adder at its measured 21,061 and 2,972 inputs/s.
Unacceptable per push, fine once a day. exhaustive-nightly.yml runs --verilog-full
at 03:17 UTC and closes the slice: four independent implementations agreeing on
all 16,777,216 inputs instead of 0.4% of them.

docs/EXHAUSTION_THEORY.md states why the wall-clock is worth spending.

Exhaustive agreement over a finite domain is a decision procedure, not a test. For
f_A, f_B : D -> R with D finite, checking equality on every x decides f_A == f_B.
No induction, no invariants, no trusted prover kernel. On a finite domain it is
the strongest statement available, and it is what HECTOR and ACL2 approximate when
D is too large to walk.

|D| is set by the representation, not the semantics:

  Claim. For k trit arguments declared in a w-bit type, enumeration costs
  (2^w / 3)^k times more than the semantic domain requires.
  Proof. Semantic domain 3^k, representational (2^w)^k, ratio (2^w/3)^k.
  Check. w=8, k=3 gives (256/3)^3 = 621,378.4, and 16,777,216/27 = 621,378.4
  measured in this tree.

Only 1.61e-6 of full_adder's enumerated space is a valid trit triple. Both
readings of that are true: a 2-bit trit type would put full_adder at 64 inputs,
0.02s in iverilog rather than 94 minutes -- four million times cheaper from a type
declaration with no algorithmic change. And the byte-wide enumeration verifies
out-of-domain behaviour a caller can reach, since pack2 does not mask and values
above 3 spill into the neighbouring lane. A 2-bit type makes those unrepresentable
rather than verified: better, but a different guarantee, not the same one cheaper.

A binary float add over two 32-bit operands is 1.8e19 inputs -- 58,561 years at
10^7/s. Enumeration is unavailable there at any budget, which is why sequential
equivalence checking and theorem proving exist. Small alphabets sit below that
line, and that is the one place choosing ternary buys a verification advantage
rather than an area or energy claim -- and unlike the area claims withdrawn twice
in this project's history, this one follows from counting.

Closes #2204
Refs #2202

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Aug 18, 2026

Copy link
Copy Markdown
Contributor

📓 NotebookLM Notebook linked to this PR

This notebook contains session context, decisions, and artifacts for this work.

@github-actions

github-actions Bot commented Aug 18, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-08-18 15:03:12 UTC

Summary

Status Count
Total Open PRs 29
PRs with Failing Checks 12
PRs with All Checks Green 17
READY 9
FAILING 12
PENDING 0

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=cd2822f290eb != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

@gHashTag gHashTag changed the title Add Verilog as the fourth arm — exhaustive where it fits, a labelled slice where it does not Verilog as the fourth arm, a nightly that exhausts it, and the theory that says why Aug 18, 2026
@gHashTag
gHashTag merged commit 61d7cc1 into master Aug 18, 2026
19 checks passed
@gHashTag
gHashTag deleted the loop/t27-verilog-exh branch August 18, 2026 15:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

1 participant

@gHashTag