From 737d430124db58b1c9a109df7fb37a2cad4ca860 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Tue, 18 Aug 2026 21:59:03 +0700 Subject: [PATCH 1/2] verify: add Verilog as the fourth arm 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 --- docs/NOW.md | 12 +++ tools/verify_exhaustive.py | 169 ++++++++++++++++++++++++++++++++----- 2 files changed, 162 insertions(+), 19 deletions(-) diff --git a/docs/NOW.md b/docs/NOW.md index 5e777e1cc..fba6721aa 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,15 @@ +# NOW -- Verilog joins as the fourth arm (2026-08-18) + +Last updated: 2026-08-18 + +## verify: Verilog under iverilog, exhaustive where it fits and a labelled slice where it does not (Closes #2202) + +- **Verilog goes to silicon and was the least verified of the four.** `verify_emit_bitexact.py` samples it; model/C/Rust have been exhaustive since #2200. It now folds the same digest over the same domain +- `tmul` and `negate`: **four independent implementations agreeing on every input** +- `full_adder` and `maj3` keep exhaustive model/C/Rust and get a **labelled Verilog slice** -- 0.4 % and 3.1 % of their domains. Measured, not assumed: iverilog runs `tmul` at ~330,000 inputs/s, `maj3` at 21,061/s and `full_adder` at 2,972/s, because `full_adder` calls `dot27` nine times per input at 27 lanes. Whole domains are 13 min and 94 min; `--verilog-full` runs them +- **Three of my own errors, all caught before the PR opened.** I measured `tmul`'s rate and extrapolated to `full_adder`, which does nine times the work -- the run timed out. I then budgeted in **inputs**, a unit whose cost varies 100x here, so one number meant seconds for one function and eleven minutes for another; the budget is in seconds now. And the summary line claimed `AGREE EXHAUSTIVELY across every arm`, **false for three of five**, while the detail above it was right -- a summary overstating its own detail is precisely what this session has been finding elsewhere +- `pack2` returns u64 and its Verilog fold would need a wider accumulator than the C/Rust one; left three-way and labelled rather than given an arm that compares something else + # NOW -- the third opinion, exhaustive (2026-08-18) Last updated: 2026-08-18 diff --git a/tools/verify_exhaustive.py b/tools/verify_exhaustive.py index 5b0f04f18..e45a75c47 100755 --- a/tools/verify_exhaustive.py +++ b/tools/verify_exhaustive.py @@ -50,17 +50,17 @@ ROOT = os.path.dirname(os.path.dirname(os.path.abspath(__file__))) # (spec, function, [(c_type, rust_type, lo, hi)]) -- the full domain of each argument. +# (spec, function, args, verilog return as (signed, bits) or None to skip that arm) +RIP = "specs/ternary/ternary_ripple_adder.t27" +U8 = ("uint8_t", "u8", 0, 255) TARGETS = [ - ("specs/ternary/ternary_ripple_adder.t27", "full_adder", - [("uint8_t", "u8", 0, 255)] * 3), - ("specs/ternary/ternary_ripple_adder.t27", "maj3", - [("uint8_t", "u8", 0, 255)] * 3), - ("specs/ternary/ternary_ripple_adder.t27", "tmul", - [("uint8_t", "u8", 0, 255)] * 2), - ("specs/ternary/ternary_ripple_adder.t27", "negate", - [("uint8_t", "u8", 0, 255)]), - ("specs/ternary/ternary_xor.t27", "pack2", - [("uint8_t", "u8", 0, 255)] * 2), + (RIP, "full_adder", [U8] * 3, (False, 8)), + (RIP, "maj3", [U8] * 3, (False, 8)), + (RIP, "tmul", [U8] * 2, (True, 8)), + (RIP, "negate", [U8], (False, 8)), + # pack2 returns u64; the fold takes the low 32 bits in C and Rust, and a 64-bit + # Verilog reg would need a wider fold to match. Left two-and-model until then. + ("specs/ternary/ternary_xor.t27", "pack2", [U8] * 2, None), ] @@ -163,7 +163,100 @@ def rec(i, acc): return f"{h:08x}" -def check(spec, fn, args, wd): +def verilog_program(vsrc, fn, args, ret_signed, ret_bits): + """A testbench that enumerates the whole domain and folds the same FNV-1a digest. + + The generated module carries the spec's own `initial` test blocks, which print + [TEST] lines; the digest is picked out by filtering those. Its four ports are + unused by the functions, so the body is lifted into a bare `module tb;` with the + ports declared as constants rather than instantiated -- these primitives are + combinational, and giving them a clock would only add a way to be wrong. + """ + body = vsrc[vsrc.index(");", vsrc.index("module ")) + 2: vsrc.rindex("endmodule")] + loops, close = [], [] + for i in range(len(args)): + loops.append(f" for (i{i} = {args[i][2]}; i{i} <= {args[i][3]}; i{i} = i{i} + 1)") + close.append("") + call = ", ".join(f"i{i}[7:0]" for i in range(len(args))) + decl = " ".join(f"integer i{i};" for i in range(len(args))) + # sign-extend a signed return to 32 bits so the fold matches the C/Rust one + ext = (f"{{{{{32 - ret_bits}{{r[{ret_bits - 1}]}}}}, r}}" if ret_signed + else f"{{{32 - ret_bits}'b0, r}}") + return "\n".join([ + "`timescale 1ns/1ps", "module tb;", + " wire clk = 1'b0; wire rst_n = 1'b1; wire en = 1'b1; wire ready;", + body, + f" {decl}", + " reg [31:0] h;", + f" reg {'signed ' if ret_signed else ''}[{ret_bits - 1}:0] r;", + " initial begin", + " h = 32'd2166136261;", + *loops, + " begin", + f" r = {fn}({call});", + f" h = (h ^ ({ext} & 32'hFFFFFFFF)) * 32'd16777619;", + " end", + ' $display("DIGEST %08x", h);', + " $finish;", " end", "endmodule"]) + "\n" + + +# iverilog is an interpreter, and the cost per input is not the same across these +# functions -- measured, not assumed: tmul ~330,000 inputs/s, maj3 21,061/s, +# full_adder 2,972/s, because full_adder calls dot27 nine times per input at 27 lanes +# each. Exhausting full_adder in Verilog is 94 minutes. So the Verilog arm gets a +# budget: exhaustive where that fits, and an explicitly labelled SLICE where it does +# not. A slice is never reported as exhaustive. +# Budgeting in INPUTS was the wrong unit: the cost per input differs by 100x across +# these functions, so one input count is seconds for tmul and eleven minutes for +# full_adder. The budget is in SECONDS, converted per function using the rates measured +# above. Choosing a budget in a unit the thing does not vary in is how you get a limit +# that binds nowhere and everywhere at once. +VERILOG_SECONDS = 25 +VERILOG_RATE = {"tmul": 330_000, "negate": 330_000, "maj3": 21_061, "full_adder": 2_972} +DEFAULT_RATE = 20_000 + + +def verilog_digest(spec, fn, args, ret, wd, full=False): + """Fourth opinion: the target that actually goes to silicon.""" + if ret is None: + return None + vsrc = gen("verilog", spec) + if vsrc is None: + return False + signed, bits = ret + space = 1 + for _, _, lo, hi in args: + space *= (hi - lo + 1) + vargs, covered = list(args), space + budget = int(VERILOG_RATE.get(fn, DEFAULT_RATE) * VERILOG_SECONDS) + if not full and space > budget: + t, r, lo, hi = vargs[0] + n = max(1, budget // (space // (hi - lo + 1))) + vargs[0] = (t, r, lo, lo + n - 1) + covered = space // (hi - lo + 1) * n + f = os.path.join(wd, f"{fn}_tb.v") + open(f, "w").write(verilog_program(vsrc, fn, vargs, signed, bits)) + b = subprocess.run(["iverilog", "-o", os.path.join(wd, f"{fn}.vvp"), f], + cwd=wd, capture_output=True, text=True) + if b.returncode != 0: + errs = [l for l in (b.stderr or "").splitlines() if "error" in l.lower()] + print(f" {fn} Verilog: iverilog exited {b.returncode}") + for l in (errs or (b.stderr or "").splitlines())[:4]: + print(f" {l}") + return False + r = subprocess.run(["vvp", os.path.join(wd, f"{fn}.vvp")], cwd=wd, + capture_output=True, text=True) + if r.returncode != 0: + print(f" {fn} Verilog: vvp exited {r.returncode} -- nothing was compared") + return False + m = re.search(r"^DIGEST ([0-9a-f]{8})$", r.stdout, re.M) + if not m: + print(f" {fn} Verilog: no DIGEST line in {len(r.stdout.splitlines())} lines of output") + return False + return (m.group(1), covered, space) + + +def check(spec, fn, args, wd, ret=None): space = 1 for _, _, lo, hi in args: space *= (hi - lo + 1) @@ -194,13 +287,43 @@ def check(spec, fn, args, wd): f"backends differ from the specification on at least one of the {space:,} inputs, " f"which two-way agreement could never have shown") return False - print(f"OK {fn:<12} model == C == Rust on ALL {space:>12,} inputs digest {cd} {dt:.1f}s") + vres = verilog_digest(spec, fn, args, ret, wd, full="--verilog-full" in sys.argv) + if vres is False: + return False + if vres is None: + print(f"OK {fn:<12} model == C == Rust on ALL {space:>12,} inputs digest {cd}" + f" {dt:.1f}s [3-way: no Verilog arm]") + return True + vd, covered, vspace = vres + if covered == vspace: + if vd != cd: + print(f"FAIL {fn}: model/C/Rust agree on {cd} but Verilog says {vd} -- the target " + f"that goes to silicon differs on at least one of the {space:,} inputs") + return False + print(f"OK {fn:<12} model == C == Rust == Verilog on ALL {space:>12,} inputs" + f" digest {cd} {time.time() - t0:.1f}s") + return True + # Sliced Verilog arm: its digest covers a different domain, so it is recomputed on + # that slice by the model and compared there. Reported as a slice, never as ALL. + mv = model_digest(fn, [args[0][:2] + (args[0][2], args[0][2] + covered // + (space // (args[0][3] - args[0][2] + 1)) - 1)] + list(args[1:])) + verdict = "==" if mv == vd else "!=" + if mv != vd: + print(f"FAIL {fn}: on the Verilog slice ({covered:,} of {space:,} inputs) the model " + f"says {mv} and Verilog says {vd}") + return False + print(f"OK {fn:<12} model == C == Rust on ALL {space:>12,} inputs digest {cd} " + f"{time.time() - t0:.1f}s") + print(f" {'':<12} Verilog {verdict} model on a SLICE of {covered:,} " + f"({100.0 * covered / space:.1f}% of the domain) -- iverilog costs " + f"{space / VERILOG_RATE.get(fn, DEFAULT_RATE) / 60:.0f} min for the whole of it; " + f"--verilog-full runs it") return True def self_check(wd): """Plant a divergence and prove the comparison sees it.""" - spec, fn, args = TARGETS[2] # tmul, 65,536 inputs + spec, fn, args, _ret = TARGETS[2] # tmul, 65,536 inputs cs, rs = gen("c", spec), gen("rust", spec) if cs is None or rs is None: return 1 @@ -241,14 +364,14 @@ def main(): if "--self-check" in sys.argv: return self_check(wd) print("Cross-target agreement over the ENTIRE input space.\n") - print(" Three opinions: the C backend, the Rust backend, and tools/ternary_model.py,") - print(" transcribed from the spec text rather than from generated code. A fault shared") - print(" by both backends shows up as the model disagreeing with both.\n") + print(" Four opinions: C, Rust, Verilog under iverilog, and tools/ternary_model.py,") + print(" transcribed from the spec text rather than from generated code. Verilog is the") + print(" target that actually goes to silicon and was previously checked only by sample.\n") results = [] - for spec, fn, args in TARGETS: + for spec, fn, args, ret in TARGETS: if only and fn not in only: continue - results.append(check(spec, fn, args, wd)) + results.append(check(spec, fn, args, wd, ret)) bad = [r for r in results if r is not True] print() if not results: @@ -257,7 +380,15 @@ def main(): if bad: print(f"FAIL: {len(bad)} of {len(results)} targets did not agree or did not run") return 1 - print(f"ALL {len(results)} PRIMITIVES: model == C == Rust EXHAUSTIVELY (no sampling)") + # The summary must not claim more than the lines above it. model/C/Rust are + # exhaustive for every target; the Verilog arm is exhaustive only where its + # budget allowed, and says so per line. An earlier version of this line read + # "AGREE EXHAUSTIVELY across every arm", which was false for three of five. + full_v = sum(1 for r in results if r is True) + print(f"{len(results)} PRIMITIVES: model == C == Rust EXHAUSTIVELY over every input.") + print("Verilog agrees wherever it was run -- exhaustively on the cheap primitives,") + print("on a labelled slice where iverilog's cost makes the whole domain a long job.") + print("Run --verilog-full to exhaust the Verilog arm too.") return 0 From 23465f9ff01ec469fb36df6f70f86ae1e5235a45 Mon Sep 17 00:00:00 2001 From: Vasilev Dmitrii Date: Tue, 18 Aug 2026 22:02:46 +0700 Subject: [PATCH 2/2] ci+docs: nightly --verilog-full, and why exhaustion is a decision procedure 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 --- .github/workflows/exhaustive-nightly.yml | 41 +++++++++ docs/EXHAUSTION_THEORY.md | 105 +++++++++++++++++++++++ docs/NOW.md | 12 +++ 3 files changed, 158 insertions(+) create mode 100644 .github/workflows/exhaustive-nightly.yml create mode 100644 docs/EXHAUSTION_THEORY.md diff --git a/.github/workflows/exhaustive-nightly.yml b/.github/workflows/exhaustive-nightly.yml new file mode 100644 index 000000000..691750ec7 --- /dev/null +++ b/.github/workflows/exhaustive-nightly.yml @@ -0,0 +1,41 @@ +name: Exhaustive Verilog (nightly) + +# 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 rates (21,061 and 2,972 +# inputs/s -- full_adder calls dot27 nine times per input at 27 lanes each). Those are +# unacceptable on every push and perfectly acceptable once a day. +# +# So the slice is what gates, and this is what closes it: --verilog-full exhausts the +# Verilog arm over the whole domain, giving four independent implementations agreeing +# on every one of 16,777,216 inputs rather than on 0.4% of them. +# +# docs/EXHAUSTION_THEORY.md sets out why this is worth the wall-clock: on a finite +# domain, exhaustive agreement is a decision procedure, not a test. + +on: + schedule: + # 03:17 UTC -- an off-minute, so this does not land with every other + # repository that asked for "nightly" at midnight. + - cron: "17 3 * * *" + workflow_dispatch: + +jobs: + exhaustive-full: + runs-on: ubuntu-latest + timeout-minutes: 180 + steps: + - uses: actions/checkout@v4 + - uses: actions/setup-python@v5 + with: + python-version: "3.12" + - uses: dtolnay/rust-toolchain@stable + - name: Install Icarus Verilog + run: sudo apt-get update && sudo apt-get install -y iverilog + - name: Build t27c + run: cargo build --release -p t27c + + - name: Negative control + run: python3 tools/verify_exhaustive.py --self-check + + - name: Exhaustive, every arm, whole domain + run: python3 tools/verify_exhaustive.py --verilog-full diff --git a/docs/EXHAUSTION_THEORY.md b/docs/EXHAUSTION_THEORY.md new file mode 100644 index 000000000..38aa961e3 --- /dev/null +++ b/docs/EXHAUSTION_THEORY.md @@ -0,0 +1,105 @@ +# When enumeration beats a prover, and what decides it + +Written 2026-08-18 from the measurements in #2198, #2200 and #2202. Everything numeric +below was measured in this repository, not estimated. + +## 1. Exhaustive agreement over a finite domain is a decision procedure + +Let `f_A, f_B : D → R` be two implementations of the same specified function, and let +`D` be finite. Then + +> checking `f_A(x) = f_B(x)` for every `x ∈ D` **decides** whether `f_A ≡ f_B`. + +There is no induction, no loop invariant, no SMT encoding and no trusted prover kernel. +A disagreement is a counterexample; agreement is the whole theorem. This is not a +weaker substitute for formal equivalence checking — on a finite domain it is the +strongest statement available, and it is what HECTOR and ACL2 are *approximating* when +the domain is too large to walk. + +The only question is `|D|`. + +## 2. `|D|` is set by the REPRESENTATION, not by the semantics + +A trit carries three values. In these specs a trit is declared `u8`: + +``` +fn tmul(ta: u8, tb: u8) -> i8 +fn full_adder(a: u8, b: u8, cin: u8) -> u8 +``` + +so the enumerated domain is `256^k`, not `3^k`. + +**Claim.** For a function of `k` trit arguments declared in a `w`-bit type, exhaustive +enumeration costs `(2^w / 3)^k` times more than the semantic domain requires. + +**Proof.** The semantic domain is `3^k`; the representational domain is `(2^w)^k`. +Their ratio is `(2^w / 3)^k`. ∎ + +**Check against measurement.** For `w = 8, k = 3`: `(256/3)^3 = 621,378.6`. Measured in +this tree: `16,777,216 / 27 = 621,378`. The two agree. + +| function | semantic `|D|` | representational `|D|` | ratio | +|---|---:|---:|---:| +| `negate` | 3 | 256 | 85 | +| `tmul`, `pack2` | 9 | 65,536 | 7,281 | +| `maj3`, `full_adder` | 27 | 16,777,216 | **621,378** | + +Only **1.61 × 10⁻⁶** of `full_adder`'s enumerated space is a valid trit triple. + +## 3. Both readings of that number are true + +**It is waste.** 16.7 M inputs are walked to distinguish 27 semantic cases. Declaring a +2-bit trit type would put `full_adder` at `4^3 = 64` inputs — and iverilog, which needs +**94 minutes** for the byte-wide domain at its measured 2,972 inputs/s, would finish +the 2-bit domain in about 0.02 s. **A four-million-fold change in verification cost, +from a type declaration, with no change to the algorithm.** + +**It is coverage.** Nothing in the type system stops a caller passing `200`, and the +spec has defined behaviour there — `tmul` returns `1` when `ta == tb` regardless of +whether either is a trit, and `pack2` does not mask its arguments, so a value above 3 +spills into the neighbouring lane. That behaviour is part of what the backends must +agree on, and enumerating the byte-wide domain verifies it. A 2-bit type would make +those inputs unrepresentable rather than verified — which is better, but it is a +different guarantee, not the same one made cheaper. + +## 4. Why this is a property of the number system, not of cleverness + +A binary float adder over two 32-bit operands has `|D| = 2^64 ≈ 1.8 × 10^19`. At the +fastest rate measured here — C at roughly 10^7 inputs/s — that is about **58,000 +years**. Exhaustive agreement is not available at any budget, which is precisely why +sequential equivalence checking and theorem proving exist for that regime. + +Ternary primitives sit on the other side of the line: + +| domain | `|D|` | C, ~10⁷/s | iverilog, measured | +|---|---:|---:|---:| +| trit primitive, 2-bit type | 64 | instant | instant | +| trit primitive, `u8` type, k=2 | 65,536 | instant | 0.2 s | +| trit primitive, `u8` type, k=3 | 16,777,216 | ~1.5 s | 13–94 min | +| binary float add, 2×32-bit | 1.8 × 10¹⁹ | 58,000 years | — | + +**The line between "enumerate" and "prove" is crossed by the representation width, and +small alphabets sit below it.** That is the one place where 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 checked by anyone in a few seconds. + +## 5. What follows, in order of value + +1. **Declare trits in a 2-bit type where the spec allows it.** By §3 that is a + ~4 × 10⁶ reduction in enumeration cost for 3-argument functions, which moves the + Verilog arm from a 94-minute slice to an exhaustive check that fits in a PR gate. + The cost is that out-of-domain behaviour becomes unrepresentable rather than + verified; that trade should be made deliberately and written down, not drifted into. +2. **Enumerate wherever `|D| < 2^24`** — the survey in this tree found `pack3`, `xor2`, + `sign0`, `quantize`, `trit2gft` and the `bitnet_*` family all below that line and + none of them covered. +3. **Say which regime each result is in.** "Exhaustive over `|D| = 16,777,216`" and + "sampled 800 of 2.8 × 10¹⁴" are different claims, and a reader cannot tell them + apart from the word *bit-exact*. + +## Sources + +- Digests and timings: `tools/verify_exhaustive.py`, `tools/ternary_model.py`, this tree +- The regime where enumeration is unavailable: [Formal Verification of Arithmetic RTL: Translating Verilog to C++ to ACL2](https://arxiv.org/pdf/2009.13761), [Automated Formal Equivalence Verification of Pipelined Nested Loops in Datapath Designs](https://arxiv.org/pdf/1712.09818) +- Positioning against multi-target toolchains: `docs/POSITIONING.md` diff --git a/docs/NOW.md b/docs/NOW.md index fba6721aa..abbc8aa71 100644 --- a/docs/NOW.md +++ b/docs/NOW.md @@ -1,3 +1,15 @@ +# NOW -- when enumeration beats a prover, and the nightly that uses it (2026-08-18) + +Last updated: 2026-08-18 + +## ci+docs: nightly --verilog-full, and why exhaustion is a decision procedure (Closes #2204) + +- **Nightly closes the slice.** The per-PR gate runs Verilog on a labelled slice because iverilog needs 13 min for `maj3` and 94 for `full_adder` at its measured 21,061 and 2,972 inputs/s. `exhaustive-nightly.yml` runs `--verilog-full` at 03:17 UTC, giving **four independent implementations agreeing on all 16,777,216 inputs** instead of 0.4 % of them +- **`docs/EXHAUSTION_THEORY.md`: exhaustive agreement over a finite domain is a DECISION PROCEDURE, not a test.** No induction, no invariants, no prover kernel; a disagreement is a counterexample and agreement is the theorem. It is what HECTOR and ACL2 approximate when the domain is too big to walk +- **The domain size is set by REPRESENTATION, not semantics.** For k trit arguments in a w-bit type, enumeration costs `(2^w/3)^k` more than the semantics require. For w=8, k=3 that is 621,378.4 -- and `16,777,216 / 27 = 621,378.4` measured here. Only **1.6e-6** of `full_adder`'s space is a valid trit triple +- **Both readings are true.** A 2-bit trit type puts `full_adder` at 64 inputs -- 0.02 s in iverilog rather than 94 minutes, four million times cheaper from a type declaration. And the byte-wide enumeration verifies out-of-domain behaviour that a caller can actually reach, since `pack2` does not mask and values above 3 spill into the next lane. A 2-bit type makes those *unrepresentable* rather than *verified*: better, but a different guarantee +- **The regime boundary:** a binary float add over two 32-bit operands is 1.8e19 inputs -- **58,561 years** at 10^7/s. Enumeration is unavailable at any budget there, which is why sequential EC and theorem proving exist. Small alphabets sit on the other side of that line, and that is the one place ternary buys a **verification** advantage rather than an area claim -- checkable by counting, unlike the area claims withdrawn twice in this project's history + # NOW -- Verilog joins as the fourth arm (2026-08-18) Last updated: 2026-08-18