Repository navigation
Conversation
…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>
…s a hand-written output Applies specs/verified/gen_file_check.t27 and specs/compiler/compile_output.t27 (#10472) to t27c. The decisions are the generated functions, wired in through #[path] modules; main.rs only gathers the inputs. seal --verify: after the hash check, each committed bootstrap/gen/rust/<rel>.rs, gen/rust/<rel>.rs, gen/c/<rel>.c and gen/verilog/<rel>.v is compared with what gen-rust, gen-c and gen-verilog emit today. Absent is fine; drift, unreadable and no-longer-generated fail with exit 1 and name the file. gen/json is not read yet: gen-json renders a spec-specific shape with no in-memory producer. compile: never writes over the input spec, and never over an existing file without "generated by t27c" in its first 5 lines unless -o names it. To read the same bytes the gen commands print, the three identical bodies of run_gen, run_gen_c and run_gen_rust become one gen_resolved(), so main.rs is +40/-60 and the foreign budget shrinks. Refs #10457 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This was referenced Oct 18, 2026
Contributor
This was referenced Oct 18, 2026
Merged
Merged
Merged
This was referenced Oct 18, 2026
Merged
Open
This branch has not been deployed
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.
Refs #10457. Draft, for the owner's
owner-approved-foreignlabel: this edits existing Rust inbootstrap/src/main.rs. Depends on #10472 (the specs); this branch sits on top of it, so until #10472 lands the diff also shows the two specs, their seals and the ledger lines.What it does
The rules are the generated functions of
specs/verified/gen_file_check.t27andspecs/compiler/compile_output.t27, wired in through#[path]modules (bootstrap/gen/rust/verified/gen_file_check.rs,bootstrap/gen/rust/compiler/compile_output.rs, written byt27c gen-rust).main.rsonly gathers the inputs and prints.seal --verify(follow-up A). After the hash check, each committedbootstrap/gen/rust/<rel>.rs,gen/rust/<rel>.rs,gen/c/<rel>.candgen/verilog/<rel>.vis compared with whatgen-rust,gen-candgen-verilogemit today. An absent file is fine. Drift, an unreadable file, or a file whose backend no longer generates the spec fails with exit 1 and names the file.compile(follow-up B). Never writes over the input spec, even with-o. Never overwrites an existing file that lacksgenerated by t27cin its first 5 lines, unless-onames it.To read the same bytes the gen commands print, the three identical bodies of
run_gen,run_gen_candrun_gen_rustbecome onegen_resolved(). Foreign budget:main.rs+40/-60, so hand-written Rust shrinks by 20 lines. The two.rsfiles are generated.Known limits
gen/jsonis not read:gen-jsonrenders a spec-specific shape and has no in-memory producer.compile_verilog_at_reportingon the unresolved source, which is whatgen-verilogdoes. A file written with--with-svawould show as drift; none is committed today.Lab results (Railway, this branch built from 982894c + #10472)
A.
t27c seal <spec> --verifydigest_cache,bench_boards,die_binding,claw/gates, and both new specsall hashes MATCH, exit 0bootstrap/gen/rust/verified/digest_cache.rstruncated to 200 bytesDRIFT,VERIFICATION FAILED, exit 1pub fn hand_edit() {}appended tobench_boards.rsDRIFT, exit 1git checkoutall hashes MATCH, exit 0B. Against
specs/x/k.t27:k.zigk.v(--backend verilog) ork.c(--backend c)-o specs/x/k.zigk.zig,k.vork.c-o specs/x/k.t27Tree-wide (
t27c suite, Phase 5 Seal Verify). 2116 specs pass and 158 fail. 143 of the failures exist without this change: hash mismatches and missing seals. The new check fails 15 specs over 16 committed files:bootstrap/gen/rust/base/ternary_add,ternary_encoding,ternary_memorybootstrap/gen/rust/memory/formula_embed,semantic_searchgen/c/numeric/gf16.cgen/verilog/numeric/gf16.vgen/rust/tools/t27o/rust_convertgen/rust/tri/t27b/blockers,coerce_plan,const_div_plan,elf,lencall,macho,tuple_local_plan,verdict_keyEach one checked by hand is genuinely stale.
gf16.candgf16.vdate from #408,elf.rskeeps an olderbytes_are(Vec<u8>)signature, andrust_convert.rsis one test behind its spec. No ORPHAN and no UNREADABLE files turned up. Before this merges, those 16 files need regenerating or the check needs to start in warn mode. That choice is the owner's.foreign-budgetandown-languagelefthook hooks pass; no--no-verify.🤖 Generated with Claude Code