gHashTag · Oct 18, 2026 · Oct 18, 2026
@@ -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"
+  }
+}
@@ -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"
+  }
+}
@@ -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;
+}
+
@@ -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;
+}
+
@@ -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<String, String>) -> anyhow::Result<String> {
     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)?;
     }

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