Skip to content

spec: seal --verify owes the committed gen file; compile refuses a hand-written output (#10457) - #10472

Merged
gHashTag merged 1 commit into
masterfrom
claude/gen-file-safety
Oct 18, 2026
Merged

spec: seal --verify owes the committed gen file; compile refuses a hand-written output (#10457)#10472
gHashTag merged 1 commit into
masterfrom
claude/gen-file-safety

Conversation

@gHashTag

@gHashTag gHashTag commented Oct 18, 2026

Copy link
Copy Markdown
Owner

Refs #10457 (follow-ups A and B of issue comment 6250250375). Spec only: no Rust changes. The t27c change that applies these rules is a separate draft PR, which waits for the owner.

What the lab showed

Railway lab, t27c 0.5.2 built from master 982894c, fixtures in .t27 only.

A. seal --verify never reads the committed gen file

change to the committed file t27c seal <spec> --verify
bootstrap/gen/rust/verified/digest_cache.rs truncated to 200 bytes five MATCH lines, all hashes MATCH, exit 0
one pub fn hand_edit() {} appended to bootstrap/gen/rust/verified/bench_boards.rs (compiled into t27c via #[path]) all hashes MATCH, exit 0

B. t27c compile overwrites whatever is at its output path

command, against specs/x/k.t27 result
t27c compile specs/x/k.t27, with a hand-written specs/x/k.zig present wrote specs/x/k.zig, exit 0, hand-written line gone
--backend verilog with k.v, --backend c with k.c same
t27c compile specs/x/k.t27 -o specs/x/k.t27 wrote specs/x/k.t27, exit 0; the spec was replaced by its own Zig output

The finding that changed rule A

As first proposed, rule A said a committed file must hash to the recorded gen_hash_*. That false-alarms on untouched files. seal hashes the generation of the unresolved source, but gen-rust and gen-c (which write the committed files) resolve use first:

spec use committed file gen-<backend> today seal records
verified/digest_cache 0 cd6233d7.. cd6233d7.. cd6233d7..
verified/bench_boards 3 80cfd58e.. 80cfd58e.. adc58ade..
verified/die_binding 2 79025f3a.. 79025f3a.. f57ce0a9..
claw/gates (C) 1 acf1850e.. acf1850e.. 31f55358..

All four seals verify, and claw/gates.c is one of the six files spec-guards already proves fresh. Over the tree, 61 of the 124 committed files under gen/ and bootstrap/gen/ hash to some value a seal records, and 63 do not. So the spec compares the file with what its generator emits today (resolved, or unresolved when gen-rust/gen-c fall back), and keeps the recorded-hash rule as a negative control.

The specs

  • specs/verified/gen_file_check.t27: gen_file_check() returns OK, ABSENT, DRIFT, UNREADABLE or ORPHAN. ORPHAN means the backend no longer generates the spec. producer_hash() handles the fallback, and verify_passes() requires the seal check AND every committed file. 12 tests use the measured hash prefixes. The negative controls show that today's verify passes the truncation, that the recorded-hash rule refuses untouched use specs, and that fresh files do not rescue a mismatched seal.

  • specs/compiler/compile_output.t27: output_check() checks, in order:

    1. The input spec is never the output, -o or not.
    2. No file at the path: write.
    3. -o naming the path is consent: write.
    4. An unreadable file: refuse.
    5. Otherwise write only when generated by t27c is in the first 5 lines.

    All 75 committed .zig/.v/.c/.rs files next to a same-stem spec carry the marker, 14 on line 2 and 61 on line 3, so the rule refuses none of them. 10 tests. The negative controls cover today's overwrite, a head of 2 lines (which would refuse generated C and Verilog), and refusing every existing file.

Evidence

  • t27c test-report: 12/12 and 10/10 pass, 0 vacuous.
  • Sealed with t27c seal --save (no --force); --verify prints all hashes MATCH for both.
  • Mutants: 8, each failing at least one test.
    • gen_file_check:
      • drift returns OK: 4 tests fail.
      • unreadable check dropped: 1 fails.
      • seal result ignored: 1 fails.
      • orphan check dropped: 1 fails.
    • compile_output:
      • -o checked before the spec guard: 2 fail.
      • head of 2 lines: 2 fail.
      • any existing file written: 3 fail.
      • unreadable check dropped: 1 fails.
  • t27b: both pass natively (aarch64 cross-build under qemu-user, 22 tests, 0 vacuous). Recorded as pass in docs/reports/t27b_expectations.json.

Out of scope

  • The Rust change (draft PR, unlabelled, for the owner).
  • compile-all and compile-project, which write into an output directory they are given.
  • seal and gen-<backend>, which print to stdout.
  • A per-file producer sweep over all 124 committed gen files; the aggregate count and the four measured files stand in for it.

🤖 Generated with Claude Code

@gHashTag @claude
spec: seal --verify owes the committed gen file; compile refuses a ha…
9112500 
…nd-written output

Two follow-ups of #10457, both reproduced on the Railway lab with t27c built
from master 982894c, written as .t27 with tests and negative controls.

specs/verified/gen_file_check.t27 (follow-up A). `seal --verify` regenerates
every backend in memory and never opens bootstrap/gen/ or gen/: a
digest_cache.rs cut to 200 bytes, and a bench_boards.rs with a hand-appended
fn, both verified "all hashes MATCH", exit 0. The rule compares a committed
gen file with what `t27c gen-<backend>` emits today, not with the recorded
gen_hash_*: gen-rust and gen-c resolve `use` first and seal does not, so for
bench_boards, die_binding and claw/gates the untouched file differs from the
seal while equal to its generator. 61 of the 124 committed gen files hash to
a recorded seal value, 63 do not. Absent is not drift; unreadable and
no-longer-generated fail closed; the file check adds to the seal check.
12 tests, 0 vacuous.

specs/compiler/compile_output.t27 (follow-up B). `t27c compile specs/x/k.t27`
overwrote a hand-written k.zig (k.v, k.c with --backend), and
`-o specs/x/k.t27` replaced the spec with its own Zig output, all exit 0. The
rule: the input spec is never the output; no file, write; -o naming the path
is consent; otherwise write only when "generated by t27c" is in the first 5
lines, and refuse an unreadable file. All 75 committed outputs next to a
same-stem spec carry the marker (14 on line 2, 61 on line 3), so the rule
refuses none of them. 10 tests, 0 vacuous.

Sealed without --force, --verify all hashes MATCH. Eight hand-made mutants
(four per spec) each fail at least one test. t27b passes both natively
(aarch64 under qemu, 22 tests), recorded in docs/reports/t27b_expectations.json.

Refs #10457

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@gHashTag
gHashTag enabled auto-merge (squash) October 18, 2026 13:25
This was referenced Oct 18, 2026
Merged
Merged
@github-actions

github-actions Bot commented Oct 18, 2026

Copy link
Copy Markdown
Contributor

PR Dashboard

Generated at: 2026-10-18 13:34:44 UTC

Summary

Status Count
Total Open PRs 50
PRs with Failing Checks 49
PRs with All Checks Green 1
READY 0
FAILING 49
PENDING 0
NO CHECKS YET 0

These columns do not partition: 0 + 49 + 0 + 0 = 49, and there are 50 open PRs. A PR is being counted twice or not at all.

Seal Status

  • ⚠️ STALE -- sha256(compiler.rs)=fad12492937a != manifest seal=87e5cbd3ad94.
    The committed NMSE numbers were certified against an older compiler.rs.
    Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).

This was referenced Oct 18, 2026
Merged
Merged
Merged
This was referenced Oct 18, 2026
Draft
Closed
This was referenced Oct 18, 2026
Merged
Merged
Merged
Open
@gHashTag
gHashTag merged commit 5412bfc into master Oct 18, 2026
32 of 35 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

1 participant

@gHashTag