Conversation
The corpus ratchet has been red on master since #2854, with UNEXPECTED FAILURES: 3 + specs/fpga/bridge.t27 [typecheck] + specs/numeric/gf16.t27 [typecheck] + specs/pins/emitter_xdc.t27 [typecheck] Bisected across six binaries built from six commits. None of the branches from this session fail; only builds from master do, and the first is #2854 -- which made `t27c typecheck` carry its printed verdict in its exit code. The binary before it prints, on `specs/fpga/bridge.t27`: Typecheck FAILED (6 errors, 0 warnings): - error: cannot assign to immutable array element 'tx_buffer[...]':223 ... and exits 0. So the three specs were always failing typecheck and the ratchet could not see it. That is not a regression; it is a measurement that started working, and the response to one is a re-bless with a stated reason. Each entry says which, and names #2852 rather than the placeholder issue `--bless-expectations` writes. Running the ratchet locally needed a fix first. `reg_decl` computes `width - 1` behind a guard testing `width == 1`, so a zero width panics the entire suite in a debug build -- `attempt to subtract with overflow` at compiler.rs:14784 -- and in release emits `reg [18446744073709551615:0]`. The guard is wrong in both profiles and loud in only one. Now `width <= 1`. Two things `--bless-expectations` does not do, both done by hand here: it writes `reason: "unclassified: blessed by --bless-expectations"`, and it does not raise `max_entries`, so a freshly blessed ledger still fails on the cap (166 entries against a 166 cap, with 3 more to add). Ratchet now exits 0: ledger 169 / 169 cap, observed 169, everything else zero. FROZEN_HASH resealed. Suite 2455 passed, 0 failed. Refs #2852
gHashTag
enabled auto-merge (squash)
August 29, 2026 18:14
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
Contributor
|
📓 NotebookLM Notebook linked to this PR
This notebook contains session context, decisions, and artifacts for this work. |
Contributor
PR DashboardGenerated at: 2026-08-29 18:14:40 UTC
Summary
Seal Status
|
gHashTag
added a commit
that referenced
this pull request
Aug 29, 2026
* ledger: four github specs became classifiable, and the theorem is the stale side
`corpus_classifier_matches_lean_completeness` is red on master:
NEW Rust/Lean lowerability disagreement(s), not in the ledger:
github_auth, github_comments, github_issues, github_prs
-- Rust=false, Lean theorem=true
Not new work of mine: reproduced on a clean `origin/master` checkout
before touching anything, and none of the four specs contains the word
`else`, so the parser change in the branch this was found from cannot
reach them.
The cause is #2882, which taught the parser to read a hyphenated module
name whole and thereby unblocked six specs. Four of them are these. A
spec that did not parse could not be classified; now it can be, and the
classifier says `false`.
The classifier is right. `t27c gen-rust specs/github/auth.t27` exits 1
and emits 0 lines. The Lean theorem, written while the spec did not
parse at all, is the stale side.
So this is the same shape as #2862: not a regression, a measurement that
started working. Recorded with the reason each entry carries, in the
same field shape the other 73 use, and `max_entries` raised to match --
`--bless` equivalents in this repo do not raise the cap, and a blessed
ledger that still fails on the cap is not blessed.
Refs #2882
* ledger: raise max_vacuous 40 -> 44, and say why in the file
Adding the four github_* entries fired a second ratchet:
vacuous completeness theorems rose 40 -> 44. A theorem about an
empty module says nothing about its spec; the ledger's max_vacuous
moves down only.
The mark is correct, and I checked it after setting it rather than
before, which is the wrong order. `github_auth_module` in
Completeness.lean is `functions := [], globals := [], tests := []`. All
four are genuinely empty models.
Those four were ALWAYS vacuous. They became COUNTABLE, because #2882
made their specs parse and the classifier could finally disagree with
the theorem. Nothing new became vacuous.
Raised to 44 with the reason written into the ledger itself, including
the part that matters: this is the SECOND-BEST answer. The ratchet
exists to stop this number growing, and the right repair is to write
real Lean models for those four rather than to raise the cap. A raise
with a reason is not a raise that is justified -- it is one the next
reader can argue with.
Suite 2455 passed, 0 failed. `--test icarus_lowerable` 358 passed, 0
failed.
Refs #2882
gHashTag
added a commit
that referenced
this pull request
Aug 29, 2026
#2887) The corpus ratchet was red on master: UNEXPECTED FAILURES: 1 + specs/api/sdk_contract.t27 [parse-no-discard] UNEXPECTED PASSES : 19 - specs/api/c_api_contract.t27 [parse] (fixed -- remove from the ledger) ... eighteen more ... All nineteen are `[parse]`, and all nineteen are specs #2877 and #2882 unblocked -- thirteen by reading `#` as a line comment and six by reading a hyphenated module name whole. The ratchet fails on an improvement exactly as it fails on a regression, because an entry that starts passing must be removed, and that is the design. The one new failure is the same story from the other side. `specs/api/sdk_contract.t27` is in the passes list for `[parse]`: it now parses, and a spec that could not be parsed could not be measured for discard either. Not new loss -- newly countable loss. The entry says so. ledger 169 -> 151 max_entries 169 -> 151 RATCHET FAIL -> CLEAN `--bless-expectations` still does not raise `max_entries` and still writes `unclassified: blessed by --bless-expectations` as the reason. Both set by hand, as in #2862. Refs #2882
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.
The corpus ratchet has been red on master since #2854.
Bisected, not guessed
Six binaries built from six commits. None of this session's branches fail — including the one for #2856, which was the obvious suspect. Only builds from master do, and the first is #2854.
#2854 made
t27c typecheckcarry its printed verdict in its exit code. The binary before it, onspecs/fpga/bridge.t27:exit 0.
So the three were always failing and the ratchet could not see it. Not a regression — a measurement that started working. The response to one of those is a re-bless with a stated reason, and each entry now carries one and names #2852 rather than the placeholder
--bless-expectationswrites.Running the ratchet locally needed a fix first
reg_declcomputeswidth - 1behind a guard testingwidth == 1. A zero width panics the whole suite in a debug build —— and in release emits
reg [18446744073709551615:0]. The guard is wrong in both profiles and loud in only one. Nowwidth <= 1.Two things
--bless-expectationsdoes not doBoth done by hand here, and worth knowing about the tool:
reason: "unclassified: blessed by --bless-expectations";max_entries, so a freshly blessed ledger still fails on the cap — 166 entries against a 166 cap with three more to add.Result
exit 0.
bootstrap/stage0/FROZEN_HASHresealed. Suite 2455 passed, 0 failed.Refs #2852