From 91125007b84163066c33649f6cb167d5cea20b63 Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 20:24:06 +0700 Subject: [PATCH 1/2] spec: seal --verify owes the committed gen file; compile refuses a hand-written output Two follow-ups of #10457, both reproduced on the Railway lab with t27c built from master 982894c96, 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-` 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 --- .../seals/compiler_CompilerCompileOutput.json | 28 +++ .../seals/verified_VerifiedGenFileCheck.json | 28 +++ docs/reports/t27b_expectations.json | 2 + specs/compiler/compile_output.t27 | 138 +++++++++++++ specs/verified/gen_file_check.t27 | 195 ++++++++++++++++++ 5 files changed, 391 insertions(+) create mode 100644 .trinity/seals/compiler_CompilerCompileOutput.json create mode 100644 .trinity/seals/verified_VerifiedGenFileCheck.json create mode 100644 specs/compiler/compile_output.t27 create mode 100644 specs/verified/gen_file_check.t27 diff --git a/.trinity/seals/compiler_CompilerCompileOutput.json b/.trinity/seals/compiler_CompilerCompileOutput.json new file mode 100644 index 0000000000..63718c06a5 --- /dev/null +++ b/.trinity/seals/compiler_CompilerCompileOutput.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+982894c96", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:a84649415aa5c6bbe2be5baa90cc40e4c4fb5fcd6f57e68a3a1d1ca34779f2ed", + "gen_hash_rust": "sha256:8b7153962dc243b734517ae797967603cfbba6a563c8f5b6d516d8338c5d0d73", + "gen_hash_verilog": "sha256:1603b3914bb4def3245218b76bdf0382e8914654c673088763dff0ae11fa2624", + "gen_hash_zig": "sha256:b8d225df8ee934349df94338052794675b38fb193341fd51fc2d85471341245e", + "module": "CompilerCompileOutput", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T13:18:10Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:7e4a2a30aa22c33d89e15c687431767fd7d09b6594d4ae3cbd179d38c381a6d8", + "spec_path": "specs/compiler/compile_output.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 10, + "total": 10, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/.trinity/seals/verified_VerifiedGenFileCheck.json b/.trinity/seals/verified_VerifiedGenFileCheck.json new file mode 100644 index 0000000000..186c42b254 --- /dev/null +++ b/.trinity/seals/verified_VerifiedGenFileCheck.json @@ -0,0 +1,28 @@ +{ + "built_by": "t27c-bootstrap@0.5.2+982894c96", + "closure": [], + "config": "gen=c,rust,verilog,zig;tests=zig", + "gen_hash_c": "sha256:67c58c41fb9bb8d8691db8700723129f94f0c8d162bc374bbee29349a115d142", + "gen_hash_rust": "sha256:261917e5273f951b5db6442775864938df9af37f03ebf631ca00ff9f98f0ce7f", + "gen_hash_verilog": "sha256:945382fc38e26c28c5bcc89df570a4381c5cda9ae55d2f9e3e915e8a39197b89", + "gen_hash_zig": "sha256:e0ddcf65cb1461153ee20ee684e402d41c5b0f6be071d0b2b0f54f4fd25c282a", + "module": "VerifiedGenFileCheck", + "ring": 12, + "seal_schema": 2, + "sealed_at": "2026-10-18T13:18:08Z", + "sealed_by": "t27c-bootstrap@0.5.2", + "spec_hash": "sha256:0b3cfb227609ab5494c8375ca42ce5813648e3ef8add0b8f967f29c3ba76c233", + "spec_path": "specs/verified/gen_file_check.t27", + "tests": { + "failed": 0, + "failing": [], + "forced": false, + "passed": 12, + "total": 12, + "vacuous": 0 + }, + "toolchain": { + "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "zig": "0.16.0" + } +} \ No newline at end of file diff --git a/docs/reports/t27b_expectations.json b/docs/reports/t27b_expectations.json index 59f54f0a39..99917a16e0 100644 --- a/docs/reports/t27b_expectations.json +++ b/docs/reports/t27b_expectations.json @@ -180,6 +180,7 @@ {"path": "specs/compiler/c_array_repeat_wrapper.t27", "t27b": "pass"}, {"path": "specs/compiler/c_fixed_array_return.t27", "t27b": "pass"}, {"path": "specs/compiler/codegen_conformance.t27", "t27b": "pass"}, + {"path": "specs/compiler/compile_output.t27", "t27b": "pass"}, {"path": "specs/compiler/core/t27core.t27", "t27b": "pass"}, {"path": "specs/compiler/core/t27core_ddc.t27", "t27b": "pass"}, {"path": "specs/compiler/cse_hoist.t27", "t27b": "pass"}, @@ -1793,6 +1794,7 @@ {"path": "specs/verified/failure_loop.t27", "t27b": "pass"}, {"path": "specs/verified/frontier.t27", "t27b": "pass"}, {"path": "specs/verified/frontier_scope.t27", "t27b": "pass"}, + {"path": "specs/verified/gen_file_check.t27", "t27b": "pass"}, {"path": "specs/verified/gen_hash_cache.t27", "t27b": "pass"}, {"path": "specs/verified/independence.t27", "t27b": "pass"}, {"path": "specs/verified/payout.t27", "t27b": "pass"}, diff --git a/specs/compiler/compile_output.t27 b/specs/compiler/compile_output.t27 new file mode 100644 index 0000000000..d2364feb4f --- /dev/null +++ b/specs/compiler/compile_output.t27 @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/compiler/compile_output.t27 -- when `t27c compile ` may write its output file. +; gHashTag/t27#10457, follow-up B. Measured on the Railway lab with t27c 0.5.2 built from master +; 982894c96, 2026-10-18. +; -- +; Without -o, `t27c compile specs/x/k.t27` writes specs/x/k.zig (k.v for --backend verilog, k.c for +; --backend c, k.zig again for --backend ml), next to the spec. bootstrap/src/main.rs run_compile +; calls fs::write on that path without looking at what is there. +; -- +; The gap, as found on the lab (fixture specs/x/k.t27, `module K;`, one passing test): +; - specs/x/k.zig, k.v and k.c each held one hand-written line. `t27c compile specs/x/k.t27`, +; `--backend verilog` and `--backend c` each printed "wrote specs/x/", exit 0, and the +; hand-written line was gone. +; - `t27c compile specs/x/k.t27 -o specs/x/k.t27` printed "wrote specs/x/k.t27", exit 0. The spec +; was replaced by its own Zig output, which starts "// Generated from t27 spec: K". +; -- +; What already marks a file as generated: every backend writes "generated by t27c" in its header. +; It is on line 2 for zig and rust ("// DO NOT EDIT -- generated by t27c") and on line 3 for +; verilog and c, below a rule line. In the tree today, 75 committed .zig/.v/.c/.rs files sit next to +; a same-stem spec under specs/. All 75 carry the marker: 14 on line 2 and 61 on line 3. So the +; rule below refuses none of them; it refuses only a file a person wrote. +; -- +; The rule, for the one output path a compile writes: +; - The path is the input spec itself: refuse, -o or not. The output of a spec is never its source. +; - No file at the path: write. +; - -o names the path: write. Naming it is the consent; a person who wants a hand-written file +; replaced says so. +; - A file is there and -o did not name it: write only when the marker is in its first +; MARK_HEAD_LINES lines. A file that cannot be read is refused (fail closed). A marker deeper in +; the body is a comment or a quote, not a header, and does not count. +; Out of scope: compile-all and compile-project, which write into an output directory they are +; given, and seal and gen-, which print to stdout. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module CompilerCompileOutput; + +/// output_check() answers. +pub const OUT_WRITE : u8 = 0; +pub const OUT_REFUSE_HAND_WRITTEN : u8 = 1; +pub const OUT_REFUSE_UNREADABLE : u8 = 2; +pub const OUT_REFUSE_SPEC : u8 = 3; + +/// How many leading lines may carry the marker. Every backend's header puts it on line 2 or 3. +pub const MARK_HEAD_LINES : u32 = 5; + +/// The line of the marker in each backend's own header, as generated today. +pub const MARK_LINE_ZIG : u32 = 2; +pub const MARK_LINE_RUST : u32 = 2; +pub const MARK_LINE_VERILOG : u32 = 3; +pub const MARK_LINE_C : u32 = 3; + +/// marker_line is the 1-based line of the first "generated by t27c" in the file, 0 for none. +pub fn marked_within(marker_line: u32, head: u32) -> bool { + if (marker_line == 0) { return false; } + return marker_line <= head; +} + +pub fn marked_generated(marker_line: u32) -> bool { + return marked_within(marker_line, MARK_HEAD_LINES); +} + +/// May compile write its output here? is_input_spec compares the resolved output path with the +/// resolved input path; named_by_o says -o gave this path. +pub fn output_check(is_input_spec: bool, exists: bool, readable: bool, marker_line: u32, named_by_o: bool) -> u8 { + if (is_input_spec) { return OUT_REFUSE_SPEC; } + if (exists == false) { return OUT_WRITE; } + if (named_by_o) { return OUT_WRITE; } + if (readable == false) { return OUT_REFUSE_UNREADABLE; } + if (marked_generated(marker_line)) { return OUT_WRITE; } + return OUT_REFUSE_HAND_WRITTEN; +} + +/// `t27c compile` today: fs::write whatever is there. The unsafe reference. +pub fn output_check_today(is_input_spec: bool, exists: bool, readable: bool, marker_line: u32, named_by_o: bool) -> u8 { + return OUT_WRITE; +} + +test a_new_output_is_written { + assert output_check(false, false, false, 0, false) == 0; +} + +test a_generated_output_is_rewritten { + // a second compile refreshes the file the first one wrote, for every backend's own header + assert output_check(false, true, true, MARK_LINE_ZIG, false) == 0; + assert output_check(false, true, true, MARK_LINE_RUST, false) == 0; + assert output_check(false, true, true, MARK_LINE_VERILOG, false) == 0; + assert output_check(false, true, true, MARK_LINE_C, false) == 0; +} + +test the_lab_overwrite_is_refused { + // hand-written specs/x/k.zig, k.v and k.c: no marker anywhere + assert output_check(false, true, true, 0, false) == 1; +} + +test o_naming_the_file_is_consent { + // `t27c compile specs/x/k.t27 -o specs/x/k.zig` replaces the hand-written file on purpose + assert output_check(false, true, true, 0, true) == 0; + assert output_check(false, true, false, 0, true) == 0; +} + +test the_spec_is_never_its_own_output { + // `-o specs/x/k.t27` replaced the spec on the lab; -o is no consent for that + assert output_check(true, true, true, 0, true) == 3; + assert output_check(true, true, true, 0, false) == 3; +} + +test an_unreadable_file_fails_closed { + assert output_check(false, true, false, 0, false) == 2; +} + +test a_marker_deep_in_the_body_does_not_count { + // a hand-written file that quotes the marker in a comment on line 40 + assert marked_generated(40) == false; + assert output_check(false, true, true, 40, false) == 1; + assert marked_generated(MARK_HEAD_LINES) == true; + assert marked_generated(MARK_HEAD_LINES + 1) == false; +} + +test negative_control_today_overwrites { + // today's compile writes where the rule refuses. Weaken the rule to today's and these fail. + assert output_check_today(false, true, true, 0, false) == OUT_WRITE; + assert output_check(false, true, true, 0, false) != output_check_today(false, true, true, 0, false); + assert output_check(true, true, true, 0, true) != output_check_today(true, true, true, 0, true); +} + +test negative_control_a_head_of_two_lines_refuses_generated_c { + // the verilog and c headers put the marker on line 3, below a rule line: 61 of the 75 + // committed outputs. A head shorter than 3 would refuse a compile's own earlier output. + assert marked_within(MARK_LINE_C, 2) == false; + assert marked_within(MARK_LINE_VERILOG, 2) == false; + assert MARK_HEAD_LINES >= MARK_LINE_C; + assert marked_generated(MARK_LINE_VERILOG) == true; +} + +test negative_control_refusing_every_existing_file_is_wrong_too { + // a rule that refuses any existing file would stop every recompile + assert output_check(false, true, true, MARK_LINE_ZIG, false) == OUT_WRITE; +} diff --git a/specs/verified/gen_file_check.t27 b/specs/verified/gen_file_check.t27 new file mode 100644 index 0000000000..4efbebab48 --- /dev/null +++ b/specs/verified/gen_file_check.t27 @@ -0,0 +1,195 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/verified/gen_file_check.t27 -- what `t27c seal --verify` owes the committed gen file of a +; spec: when one exists, its bytes are what the spec's generator emits today, or the verify fails. +; gHashTag/t27#10457, follow-up A. Measured on the Railway lab with t27c 0.5.2 built from master +; 982894c96, 2026-10-18. +; -- +; What already exists and is NOT restated here: +; - specs/verified/seal_check.t27 says how a seal is checked from its recorded inputs. That check +; regenerates every backend in memory and compares the recorded gen_hash_* with the fresh +; output. It never opens a file under gen/ or bootstrap/gen/. This file is that missing read. +; - specs/verified/seal_write.t27 (#10458) says what one seal write must guarantee. This file is +; about the generated files committed next to the seals, which no seal write produces. +; - .github/workflows/spec-guards.yml regenerates six named committed gen files and runs +; `git diff --exit-code`. The rule here covers every committed gen file, not only those six. +; -- +; The gap, as found on the lab: +; - bootstrap/gen/rust/verified/digest_cache.rs truncated to its first 200 bytes: `t27c seal +; specs/verified/digest_cache.t27 --verify` printed five MATCH lines, "all hashes MATCH", exit 0. +; - one hand-written fn appended to bootstrap/gen/rust/verified/bench_boards.rs: "all hashes +; MATCH", exit 0. That file is compiled into t27c itself (bootstrap/src/main.rs #[path]). +; -- +; Why the comparison is against the generator, not against the recorded gen_hash_*: +; the first version of this rule (issue comment 6250250375) said the committed file must hash to +; the recorded gen_hash_*. That is right only for a spec with no `use`. `seal` hashes the +; generation of the unresolved source; `t27c gen-rust` and `t27c gen-c`, which write the committed +; files, resolve `use` first. Measured: +; digest_cache (no use) file cd6233d7.. gen-rust cd6233d7.. seal gen_hash_rust cd6233d7.. +; bench_boards (3 use) file 80cfd58e.. gen-rust 80cfd58e.. seal gen_hash_rust adc58ade.. +; die_binding (2 use) file 79025f3a.. gen-rust 79025f3a.. seal gen_hash_rust f57ce0a9.. +; claw/gates (1 use) file acf1850e.. gen-c acf1850e.. seal gen_hash_c 31f55358.. +; claw/gates.c is one of the six files spec-guards proves fresh, and all four seals verify. 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. The recorded-hash rule would refuse untouched files like these; the +; generator rule refuses only the truncated and the hand-edited one. +; -- +; The rule, per backend of one spec: +; - The committed gen files of specs/.t27 are bootstrap/gen/rust/.rs, gen/rust/.rs, +; gen/c/.c, gen/verilog/.v and gen/json/.json. gen/json has no gen_hash_* field +; in any seal, so only the generator rule can check it. +; - No such file: nothing to check. Most specs have none, and the seal still certifies the +; regenerated output. +; - The file exists: it must hash to what `t27c gen- ` emits today. That is the +; generation of the `use`-resolved source, or of the unresolved source when the resolved one does +; not compile (gen-rust's fallback, which it announces with a note). +; - The file exists but cannot be read, or the backend no longer generates anything for the spec: +; fail closed. A file that no generator emits cannot be generated output. +; - `--verify` passes only when the recorded hashes match AND every committed gen file passes. +; This check adds to the seal check; it replaces none of it. +; Hashes are stand-ins: the first 32 bits of the measured sha256, compared whole. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module VerifiedGenFileCheck; + +/// gen_file_check() answers. +pub const GEN_OK : u8 = 0; +pub const GEN_ABSENT : u8 = 1; +pub const GEN_DRIFT : u8 = 2; +pub const GEN_UNREADABLE : u8 = 3; +pub const GEN_ORPHAN : u8 = 4; + +/// What `t27c gen- ` emits: the generation of the `use`-resolved source, unless +/// that does not compile and the generator falls back to the unresolved one. For a spec with no +/// `use` the two are the same bytes. +pub fn producer_hash(resolved_compiles: bool, unresolved: u64, resolved: u64) -> u64 { + if (resolved_compiles) { return resolved; } + return unresolved; +} + +/// One committed gen file against its generator. exists covers every home listed above; +/// readable says its bytes could be read; producer_ok says the backend generated anything today. +pub fn gen_file_check(exists: bool, readable: bool, file_hash: u64, producer_ok: bool, producer: u64) -> u8 { + if (exists == false) { return GEN_ABSENT; } + if (readable == false) { return GEN_UNREADABLE; } + if (producer_ok == false) { return GEN_ORPHAN; } + if (file_hash == producer) { return GEN_OK; } + return GEN_DRIFT; +} + +/// The rule as first proposed: the file against the recorded gen_hash_*. Kept as the reference +/// that false-alarms on every untouched file of a spec with `use`. +pub fn gen_file_check_recorded(exists: bool, file_hash: u64, recorded: u64) -> u8 { + if (exists == false) { return GEN_ABSENT; } + if (file_hash == recorded) { return GEN_OK; } + return GEN_DRIFT; +} + +/// `seal --verify` today: the committed file is never opened. The unsafe reference. +pub fn gen_file_check_today(exists: bool, readable: bool, file_hash: u64, producer_ok: bool, producer: u64) -> u8 { + return GEN_OK; +} + +/// A committed file passes when it is absent or equal to its generator's output. +pub fn gen_file_passes(code: u8) -> bool { + if (code == GEN_OK) { return true; } + return code == GEN_ABSENT; +} + +/// The verdict of `seal --verify` over the recorded hashes and the four backends' committed files +/// (rust covers both rust homes). +pub fn verify_passes(seal_all_match: bool, rust: u8, c: u8, verilog: u8, json: u8) -> bool { + if (seal_all_match == false) { return false; } + if (gen_file_passes(rust) == false) { return false; } + if (gen_file_passes(c) == false) { return false; } + if (gen_file_passes(verilog) == false) { return false; } + return gen_file_passes(json); +} + +/// `seal --verify` today: the recorded hashes decide alone. +pub fn verify_passes_today(seal_all_match: bool, rust: u8, c: u8, verilog: u8, json: u8) -> bool { + return seal_all_match; +} + +test an_untouched_file_of_a_spec_without_use_passes { + // digest_cache: the file, gen-rust and the seal all say cd6233d7.. + var producer : u64 = producer_hash(true, 0xcd6233d7, 0xcd6233d7); + assert producer == 0xcd6233d7; + assert gen_file_check(true, true, 0xcd6233d7, true, producer) == 0; + assert verify_passes(true, gen_file_check(true, true, 0xcd6233d7, true, producer), GEN_ABSENT, GEN_ABSENT, GEN_ABSENT) == true; +} + +test the_lab_truncation_fails_the_verify { + // digest_cache.rs cut to 200 bytes hashes to 675400d8..; today's verify said all hashes MATCH + assert gen_file_check(true, true, 0x675400d8, true, 0xcd6233d7) == 2; + assert verify_passes(true, GEN_DRIFT, GEN_ABSENT, GEN_ABSENT, GEN_ABSENT) == false; +} + +test the_lab_hand_edit_fails_the_verify { + // bench_boards.rs with one appended fn hashes to ea48aa9b..; gen-rust emits 80cfd58e.. + var producer : u64 = producer_hash(true, 0xadc58ade, 0x80cfd58e); + assert gen_file_check(true, true, 0xea48aa9b, true, producer) == 2; +} + +test an_untouched_file_of_a_spec_with_use_passes { + // bench_boards and die_binding (gen-rust) and claw/gates (gen-c): the file is the resolved + // generation, which the seal does not record + assert gen_file_check(true, true, 0x80cfd58e, true, producer_hash(true, 0xadc58ade, 0x80cfd58e)) == 0; + assert gen_file_check(true, true, 0x79025f3a, true, producer_hash(true, 0xf57ce0a9, 0x79025f3a)) == 0; + assert gen_file_check(true, true, 0xacf1850e, true, producer_hash(true, 0x31f55358, 0xacf1850e)) == 0; +} + +test negative_control_the_recorded_hash_refuses_untouched_files { + // the rule as first proposed calls all three untouched files drift; it would turn + // `seal --verify` red on files nobody edited + assert gen_file_check_recorded(true, 0x80cfd58e, 0xadc58ade) == GEN_DRIFT; + assert gen_file_check_recorded(true, 0x79025f3a, 0xf57ce0a9) == GEN_DRIFT; + assert gen_file_check_recorded(true, 0xacf1850e, 0x31f55358) == GEN_DRIFT; + assert gen_file_check(true, true, 0x80cfd58e, true, 0x80cfd58e) != gen_file_check_recorded(true, 0x80cfd58e, 0xadc58ade); + // where the spec has no `use`, the two rules agree + assert gen_file_check_recorded(true, 0xcd6233d7, 0xcd6233d7) == gen_file_check(true, true, 0xcd6233d7, true, 0xcd6233d7); +} + +test negative_control_today_passes_the_truncation { + // today's verify never reads the file. Weaken the rule to today's and these lines fail. + assert gen_file_check_today(true, true, 0x675400d8, true, 0xcd6233d7) == GEN_OK; + assert verify_passes_today(true, GEN_DRIFT, GEN_ABSENT, GEN_ABSENT, GEN_ABSENT) == true; + assert gen_file_check(true, true, 0x675400d8, true, 0xcd6233d7) != gen_file_check_today(true, true, 0x675400d8, true, 0xcd6233d7); + assert verify_passes(true, GEN_DRIFT, GEN_ABSENT, GEN_ABSENT, GEN_ABSENT) != verify_passes_today(true, GEN_DRIFT, GEN_ABSENT, GEN_ABSENT, GEN_ABSENT); +} + +test an_absent_file_is_not_drift { + // a spec with no committed gen file verifies on its recorded hashes alone + assert gen_file_check(false, false, 0, true, 0xcd6233d7) == 1; + assert gen_file_passes(GEN_ABSENT) == true; + assert verify_passes(true, GEN_ABSENT, GEN_ABSENT, GEN_ABSENT, GEN_ABSENT) == true; +} + +test an_unreadable_file_fails_closed { + assert gen_file_check(true, false, 0, true, 0xcd6233d7) == 3; + assert gen_file_passes(GEN_UNREADABLE) == false; +} + +test a_file_its_backend_no_longer_generates_fails { + // the spec stopped lowering to this backend; the committed file is left over, not generated + assert gen_file_check(true, true, 0xcd6233d7, false, 0) == 4; + assert gen_file_passes(GEN_ORPHAN) == false; +} + +test the_generator_falls_back_to_the_unresolved_source { + // gen-rust: a spliced source that does not compile is dropped, with a note + assert producer_hash(false, 0xadc58ade, 0x80cfd58e) == 0xadc58ade; + assert producer_hash(true, 0xadc58ade, 0x80cfd58e) == 0x80cfd58e; +} + +test one_drifting_backend_fails_the_verify { + // any of the four homes is enough; the c file of a spec whose rust file is fine + assert verify_passes(true, GEN_OK, GEN_DRIFT, GEN_ABSENT, GEN_ABSENT) == false; + assert verify_passes(true, GEN_OK, GEN_ABSENT, GEN_ABSENT, GEN_ORPHAN) == false; + assert verify_passes(true, GEN_OK, GEN_OK, GEN_OK, GEN_OK) == true; +} + +test negative_control_the_file_check_does_not_replace_the_seal_check { + // fresh committed files do not rescue a seal whose recorded hashes differ + assert verify_passes(false, GEN_OK, GEN_OK, GEN_OK, GEN_OK) == false; + assert verify_passes(false, GEN_ABSENT, GEN_ABSENT, GEN_ABSENT, GEN_ABSENT) == false; +} From a36a6255086b7b78f8495826d44fc21dc01a30fd Mon Sep 17 00:00:00 2001 From: Dmitrii Vasilev Date: Sun, 18 Oct 2026 20:38:51 +0700 Subject: [PATCH 2/2] fix(t27c): seal --verify reads the committed gen file; compile refuses 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/.rs, gen/rust/.rs, gen/c/.c and gen/verilog/.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 --- bootstrap/gen/rust/compiler/compile_output.rs | 58 ++++++++++ bootstrap/gen/rust/verified/gen_file_check.rs | 80 ++++++++++++++ bootstrap/src/main.rs | 100 +++++++----------- 3 files changed, 178 insertions(+), 60 deletions(-) create mode 100644 bootstrap/gen/rust/compiler/compile_output.rs create mode 100644 bootstrap/gen/rust/verified/gen_file_check.rs diff --git a/bootstrap/gen/rust/compiler/compile_output.rs b/bootstrap/gen/rust/compiler/compile_output.rs new file mode 100644 index 0000000000..fc257d7293 --- /dev/null +++ b/bootstrap/gen/rust/compiler/compile_output.rs @@ -0,0 +1,58 @@ +// Generated from .t27 spec +// DO NOT EDIT — generated by t27c +// NOT LOWERED BY THIS BACKEND: 10 test(s), 0 invariant(s), 0 function(s) with no body. +// This backend emits declarations only. The spec's checks live in +// the Zig and Verilog outputs; do not read this file as verified. + +pub const OUT_WRITE: u8 = 0; + +pub const OUT_REFUSE_HAND_WRITTEN: u8 = 1; + +pub const OUT_REFUSE_UNREADABLE: u8 = 2; + +pub const OUT_REFUSE_SPEC: u8 = 3; + +pub const MARK_HEAD_LINES: u32 = 5; + +pub const MARK_LINE_ZIG: u32 = 2; + +pub const MARK_LINE_RUST: u32 = 2; + +pub const MARK_LINE_VERILOG: u32 = 3; + +pub const MARK_LINE_C: u32 = 3; + +pub fn marked_within(marker_line: u32, head: u32) -> bool { + if (marker_line == 0) { + return false; + } + return (marker_line <= head); +} + +pub fn marked_generated(marker_line: u32) -> bool { + return marked_within(marker_line, MARK_HEAD_LINES); +} + +pub fn output_check(is_input_spec: bool, exists: bool, readable: bool, marker_line: u32, named_by_o: bool) -> u8 { + if is_input_spec { + return OUT_REFUSE_SPEC; + } + if (exists == false) { + return OUT_WRITE; + } + if named_by_o { + return OUT_WRITE; + } + if (readable == false) { + return OUT_REFUSE_UNREADABLE; + } + if marked_generated(marker_line) { + return OUT_WRITE; + } + return OUT_REFUSE_HAND_WRITTEN; +} + +pub fn output_check_today(is_input_spec: bool, exists: bool, readable: bool, marker_line: u32, named_by_o: bool) -> u8 { + return OUT_WRITE; +} + diff --git a/bootstrap/gen/rust/verified/gen_file_check.rs b/bootstrap/gen/rust/verified/gen_file_check.rs new file mode 100644 index 0000000000..80659d60a7 --- /dev/null +++ b/bootstrap/gen/rust/verified/gen_file_check.rs @@ -0,0 +1,80 @@ +// Generated from .t27 spec +// DO NOT EDIT — generated by t27c +// NOT LOWERED BY THIS BACKEND: 12 test(s), 0 invariant(s), 0 function(s) with no body. +// This backend emits declarations only. The spec's checks live in +// the Zig and Verilog outputs; do not read this file as verified. + +pub const GEN_OK: u8 = 0; + +pub const GEN_ABSENT: u8 = 1; + +pub const GEN_DRIFT: u8 = 2; + +pub const GEN_UNREADABLE: u8 = 3; + +pub const GEN_ORPHAN: u8 = 4; + +pub fn producer_hash(resolved_compiles: bool, unresolved: u64, resolved: u64) -> u64 { + if resolved_compiles { + return resolved; + } + return unresolved; +} + +pub fn gen_file_check(exists: bool, readable: bool, file_hash: u64, producer_ok: bool, producer: u64) -> u8 { + if (exists == false) { + return GEN_ABSENT; + } + if (readable == false) { + return GEN_UNREADABLE; + } + if (producer_ok == false) { + return GEN_ORPHAN; + } + if (file_hash == producer) { + return GEN_OK; + } + return GEN_DRIFT; +} + +pub fn gen_file_check_recorded(exists: bool, file_hash: u64, recorded: u64) -> u8 { + if (exists == false) { + return GEN_ABSENT; + } + if (file_hash == recorded) { + return GEN_OK; + } + return GEN_DRIFT; +} + +pub fn gen_file_check_today(exists: bool, readable: bool, file_hash: u64, producer_ok: bool, producer: u64) -> u8 { + return GEN_OK; +} + +pub fn gen_file_passes(code: u8) -> bool { + if (code == GEN_OK) { + return true; + } + return (code == GEN_ABSENT); +} + +pub fn verify_passes(seal_all_match: bool, rust: u8, c: u8, verilog: u8, json: u8) -> bool { + if (seal_all_match == false) { + return false; + } + if (gen_file_passes(rust) == false) { + return false; + } + if (gen_file_passes(c) == false) { + return false; + } + if (gen_file_passes(verilog) == false) { + return false; + } + return gen_file_passes(json); +} + +pub fn verify_passes_today(seal_all_match: bool, rust: u8, c: u8, verilog: u8, json: u8) -> bool { + return seal_all_match; +} + diff --git a/bootstrap/src/main.rs b/bootstrap/src/main.rs index 9c5481aa0b..3a4c64dfcd 100644 --- a/bootstrap/src/main.rs +++ b/bootstrap/src/main.rs @@ -76,6 +76,13 @@ use corpus_receipt as cr; #[path = "../gen/rust/verified/ddc_receipt.rs"] #[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)] mod ddc_receipt; +// #10457: specs/verified/gen_file_check.t27 (seal --verify) and specs/compiler/compile_output.t27 (compile). +#[path = "../gen/rust/verified/gen_file_check.rs"] +#[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)] +mod gen_file_check; +#[path = "../gen/rust/compiler/compile_output.rs"] +#[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)] +mod compile_output; fn cr_sha(parts: &[&[u8]]) -> [u8; 32] { use sha2::Digest; parts.iter().fold(sha2::Sha256::new(), |h, p| h.chain_update(p)).finalize().into() } fn cr_root(l: &[String]) -> [u8; 32] { let k = cr::split_point(l.len() as u32) as usize; if l.len() < 2 { l.first().map_or(cr_sha(&[]), |x| cr_sha(&[&[cr::LEAF_PREFIX], x.as_bytes()])) } else { cr_sha(&[&[cr::NODE_PREFIX], &cr_root(&l[..k]), &cr_root(&l[k..])]) } } @@ -4639,7 +4646,8 @@ fn gated_backend( } } -fn run_gen(input_path: &str) -> anyhow::Result<()> { +/// What gen, gen-c and gen-rust emit (W584: `use` resolution is backend-agnostic) and seal --verify reads. +fn gen_resolved(input_path: &str, compile: fn(&str) -> Result) -> anyhow::Result { let path = Path::new(input_path); let raw = fs::read_to_string(path)?; typecheck_gate(path, &raw)?; @@ -4655,9 +4663,9 @@ fn run_gen(input_path: &str) -> anyhow::Result<()> { for note in use_resolve::unresolved_notes(&resolved) { eprintln!("{}", note); } - let zig_code = match compiler::Compiler::compile(&resolved) { + let code = match compile(&resolved) { Ok(code) => code, - Err(spliced_err) => match compiler::Compiler::compile(&raw) { + Err(spliced_err) => match compile(&raw) { Ok(code) => { // The splice is discarded here and the unresolved source used // instead. Without this line that is invisible: the command @@ -4671,7 +4679,11 @@ fn run_gen(input_path: &str) -> anyhow::Result<()> { Err(_) => anyhow::bail!("Compile error: {}", spliced_err), }, }; - print!("{}", zig_code); + Ok(code) +} + +fn run_gen(input_path: &str) -> anyhow::Result<()> { + print!("{}", gen_resolved(input_path, compiler::Compiler::compile)?); Ok(()) } @@ -5481,64 +5493,12 @@ fn run_gen_testbench(input_path: &str, period_ns: u32, max_cycles: u32, output: } fn run_gen_c(input_path: &str) -> anyhow::Result<()> { - let path = Path::new(input_path); - let raw = fs::read_to_string(path)?; - typecheck_gate(path, &raw)?; - // W584: `use` resolution is a source-to-source pass (W569), so it is - // backend-agnostic -- only `gen` was calling it, which is why the C headers - // failed on types declared in modules they import. Same safety contract: - // if the spliced source stops compiling, the original is used. - let resolved = use_resolve::resolve(path, &raw); - for note in use_resolve::unresolved_notes(&resolved) { - eprintln!("{}", note); - } - let c_code = match compiler::Compiler::compile_c(&resolved) { - Ok(code) => code, - Err(spliced_err) => match compiler::Compiler::compile_c(&raw) { - Ok(code) => { - // The splice is discarded here and the unresolved source used - // instead. Without this line that is invisible: the command - // succeeds, and every import it resolved is silently gone. - eprintln!( - "note: spliced source did not compile, falling back to the \ - unresolved original -- imported declarations are NOT in this output" - ); - code - } - Err(_) => anyhow::bail!("Compile error: {}", spliced_err), - }, - }; - print!("{}", c_code); + print!("{}", gen_resolved(input_path, compiler::Compiler::compile_c)?); Ok(()) } fn run_gen_rust(input_path: &str) -> anyhow::Result<()> { - let path = Path::new(input_path); - let raw = fs::read_to_string(path)?; - typecheck_gate(path, &raw)?; - // W584: same as gen-c -- `use` resolution is backend-agnostic and only - // `gen` was calling it. - let resolved = use_resolve::resolve(path, &raw); - for note in use_resolve::unresolved_notes(&resolved) { - eprintln!("{}", note); - } - let rust_code = match compiler::Compiler::compile_rust(&resolved) { - Ok(code) => code, - Err(spliced_err) => match compiler::Compiler::compile_rust(&raw) { - Ok(code) => { - // The splice is discarded here and the unresolved source used - // instead. Without this line that is invisible: the command - // succeeds, and every import it resolved is silently gone. - eprintln!( - "note: spliced source did not compile, falling back to the \ - unresolved original -- imported declarations are NOT in this output" - ); - code - } - Err(_) => anyhow::bail!("Compile error: {}", spliced_err), - }, - }; - print!("{}", rust_code); + print!("{}", gen_resolved(input_path, compiler::Compiler::compile_rust)?); Ok(()) } @@ -5979,10 +5939,23 @@ fn run_seal(input_path: &str, save: bool, verify: bool, force: bool) -> anyhow:: std::process::exit(1); } - if all_match { + // specs/verified/gen_file_check.t27: a committed gen file is what its generator emits today. + // gen/json is not read yet: gen-json renders a spec-specific shape, with no in-memory producer. + let (rel, h) = (hashes.spec_path.trim_start_matches("specs/").trim_end_matches(".t27"), |b: &[u8]| u64::from_str_radix(&sha256_hex(b)[..16], 16).unwrap_or(0)); + let check = |file: String, made: Option<&str>| { + let read = fs::read(&file); + let code = gen_file_check::gen_file_check(Path::new(&file).exists(), read.is_ok(), read.as_deref().map_or(0, h), made.is_some(), made.map_or(0, |m| h(m.as_bytes()))); + if !gen_file_check::gen_file_passes(code) { println!("{}: {}", file, ["", "", "DRIFT (not what its generator emits today)", "UNREADABLE", "ORPHAN (its backend no longer generates this spec)"][code as usize]); } + code + }; + let rust = gen_resolved(input_path, compiler::Compiler::compile_rust).ok(); + let (r1, r2) = (check(format!("bootstrap/gen/rust/{rel}.rs"), rust.as_deref()), check(format!("gen/rust/{rel}.rs"), rust.as_deref())); + let c = check(format!("gen/c/{rel}.c"), gen_resolved(input_path, compiler::Compiler::compile_c).ok().as_deref()); + let v = check(format!("gen/verilog/{rel}.v"), compiler::Compiler::compile_verilog_at_reporting(&fs::read_to_string(input_path)?, Path::new(input_path)).ok().map(|r| r.0).as_deref()); + if gen_file_check::verify_passes(all_match, if gen_file_check::gen_file_passes(r1) { r2 } else { r1 }, c, v, gen_file_check::GEN_ABSENT) { println!("\nall hashes MATCH"); } else { - println!("\nVERIFICATION FAILED — hashes differ from saved seal"); + println!("\nVERIFICATION FAILED — {}", if all_match { "a committed gen file is not its generator's output" } else { "hashes differ from saved seal" }); std::process::exit(1); } } else if save { @@ -6290,6 +6263,13 @@ fn run_compile(input_path: &str, backend: &str, output: Option<&str>) -> anyhow: } }; + // specs/compiler/compile_output.t27: never the spec itself, never a hand-written file unless -o names it. + let existing = fs::read(&out_path); + let marker = existing.as_deref().map_or(0, |b| String::from_utf8_lossy(b).lines().position(|l| l.contains("generated by t27c")).map_or(0, |i| i as u32 + 1)); + match compile_output::output_check(fs::canonicalize(&out_path).ok() == fs::canonicalize(path).ok(), out_path.exists(), existing.is_ok(), marker, output.is_some()) { + compile_output::OUT_WRITE => {} + r => anyhow::bail!("refusing to write {}: {}", out_path.display(), ["", "it has no \"generated by t27c\" header; name it with -o to replace it", "it cannot be read", "it is the input spec"][r as usize]), + } if let Some(parent) = out_path.parent() { fs::create_dir_all(parent)?; }