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

.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"
+  }
+}

.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"
+  }
+}

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"},

specs/compiler/compile_output.t27

@@ -0,0 +1,138 @@
+// SPDX-License-Identifier: Apache-2.0
+; specs/compiler/compile_output.t27 -- when `t27c compile <spec>` 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/<file>", 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-<backend>, 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;
+}