Seals: 0 of 1072 specs verify, 928 with an unchanged spec_hash — gate it or remove it

[gHashTag]

The measurement

t27c seal --verify run over every one of the 1072 specs:

928   STALE, spec_hash MATCHES     the spec did not change; the generated code did
118   STALE, spec_hash DIFFERS     the spec changed too
 26   no seal at all
  0   VERIFY                       not one spec in the corpus verifies

This is known and deliberate — the question is whether it should stay that way

bootstrap/src/suite.rs, above the seal phase:

"W627: seal staleness is golden-file drift, not a defect population — 1056 of 1064 are stale and ~940 have an UNCHANGED spec_hash. It is recorded in the ledger for visibility and excluded from the corpus defect count below, because listing it as expected failure is debt."

And the ratchet agrees: docs/reports/suite_expectations.json has 326 entries and zero for seal-verify — 173 parse, 132 parse-no-discard, 21 no-vacuous-verilog-test.

So the phase runs, the failure is known, and it is tolerated with the reason written down. Nothing here is a surprise to the repository.

Why file it anyway

A seal answers exactly one question: did the generated code change while the specification did not? For 928 specs the answer is yes, and nothing acts on it. That is not a broken mechanism — it is a working mechanism whose alarm is disconnected.

Two honest options, and they are opposites:

1. Re-seal the corpus and make the phase a gate. Then a codegen change that alters output without a spec change fails CI, which is what seals are for. Cost: one blessing run, plus every future codegen change needs a deliberate re-seal.
2. Remove the mechanism. 1715 seal files, zero verifying, no gate. If the answer is never acted on, the files are storage and the phase is time.

What should not continue is the third state — keeping the files, running the phase, and ignoring the verdict — because it reads to a newcomer as evidence that does not exist. It cost this session a wave to discover that (T247 published wrong counts from an ad-hoc check before the authoritative one was run; corrected in T248).

Related

• t27c seal <spec> --verify is the authoritative check; a regex over .trinity/seals/*.json is not and was wrong by twenty-fold.
• Theorems T247, T248, T248a in docs/theory/IGLA-FORMAL-RESULTS.md.

[gHashTag]

The choice offered here is between two options; there is a third parameter that decides it

This issue frames it as re-seal-and-gate versus remove. Both are answers to "what do we do with the files". Neither answers the question that actually determines whether a seal is worth anything:

What is required to happen between a seal mismatch and that seal being updated?

If the answer is "nothing", then re-sealing the corpus produces the same disconnected alarm one blessing run later, and the third state this issue warns about returns by itself.

The repository already contains a second instance of exactly this construction

bootstrap/build.rs seals bootstrap/src/compiler.rs against bootstrap/stage0/FROZEN_HASH. It works: it stopped my first edit to the parser immediately, with a clear message.

Then it took one line to clear:

sha256sum bootstrap/src/compiler.rs > bootstrap/stage0/FROZEN_HASH

No check ran. Nothing verified the change. The seal proves "this file did not change unnoticed" — which is real, and worth having — and it proves nothing about whether the change is correct. Identity, not correctness.

So the corpus seals in this issue are not an isolated case of a working mechanism with a disconnected alarm. There are two, one of them guarding the compiler itself.

What follows for option 1

Re-sealing plus a CI gate is worth doing, but the gate has to bind the update, not the check. A mismatch already fails; the missing part is that clearing a mismatch should require evidence. Concretely, for the compiler seal, the evidence that makes a re-seal meaningful is a differential run against the binary being replaced — which is now one command (tri diffbin <old> <new> specs, #2151), and which exits non-zero on any regression. For the 928 corpus specs the analogous evidence is whatever explains why generated output changed while the spec did not; that explanation is the thing the seal is asking for, and re-sealing without it discards the only question the mechanism can answer.

tri freeze in #2151 re-seals the compiler and prints that warning out loud rather than silently. That is a mitigation, not a gate — a printed warning is not a check, and I am not claiming otherwise.

What I did not do

I did not run t27c seal --verify over the corpus myself, so the 928 / 118 / 26 / 0 split here is quoted, not independently reproduced. The compiler-seal observation above is first-hand.