fix(seal): refuse a seal file another spec owns, re-check the hash after the write, land it by rename

.trinity/seals/verified_VerifiedSealWrite.json

@@ -0,0 +1,33 @@
+{
+  "built_by": "t27c-bootstrap@0.5.2+89254d2",
+  "closure": [
+    {
+      "spec": "specs/verified/reuse.t27",
+      "spec_hash": "sha256:79af2725711852461d2d71c0ad089fb55130199e320abed77f11e915cf9d970b"
+    }
+  ],
+  "config": "gen=c,rust,verilog,zig;tests=zig",
+  "gen_hash_c": "sha256:5f3682132cd429701a3c174527eafa73952f9ac6fd470a6e5ba8769a95a56db7",
+  "gen_hash_rust": "sha256:be2b7658bad3f36d544ee77a831c740aaa40bd390286bd6642a7c2d581ac24fc",
+  "gen_hash_verilog": "sha256:42c766404f36a48fb80d7fd861174133ab81463adea0493e8b6f019c3bdf4e52",
+  "gen_hash_zig": "sha256:a77c3bf9bd31868508b0f9545045233253a21342a56d16356cac9ef25791267a",
+  "module": "VerifiedSealWrite",
+  "ring": 12,
+  "seal_schema": 2,
+  "sealed_at": "2026-10-18T12:55:35Z",
+  "sealed_by": "t27c-bootstrap@0.5.2",
+  "spec_hash": "sha256:59262b1a210bd4775ef0dec0db9a52f1333069afb946cf4cd88c6cb894a6b6e0",
+  "spec_path": "specs/verified/seal_write.t27",
+  "tests": {
+    "failed": 0,
+    "failing": [],
+    "forced": false,
+    "passed": 14,
+    "total": 14,
+    "vacuous": 0
+  },
+  "toolchain": {
+    "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d",
+    "zig": "0.16.0"
+  }
+}

bootstrap/gen/rust/verified/seal_write.rs

@@ -0,0 +1,130 @@
+// Generated from .t27 spec
+// DO NOT EDIT — generated by t27c
+// NOT LOWERED BY THIS BACKEND: 14 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 WRITE_OK: u8 = 0;
+
+pub const WRITE_COLLISION: u8 = 1;
+
+pub const WRITE_OWNER_UNKNOWN: u8 = 2;
+
+pub const WRITE_SPEC_MOVED: u8 = 3;
+
+pub const WRITE_TESTED_OTHER: u8 = 4;
+
+pub const WRITE_READBACK_DIFF: u8 = 5;
+
+pub const PROTO_IN_PLACE: u8 = 1;
+
+pub const PROTO_WRITE_THEN_RESTORE: u8 = 2;
+
+pub const PROTO_STAGE_THEN_RENAME: u8 = 3;
+
+pub const CUT_BEFORE_WRITE: u8 = 1;
+
+pub const CUT_DURING_WRITE: u8 = 2;
+
+pub const CUT_AFTER_WRITE: u8 = 3;
+
+pub const CUT_AFTER_COMMIT: u8 = 4;
+
+pub const DISK_OLD: u8 = 1;
+
+pub const DISK_NEW_CHECKED: u8 = 2;
+
+pub const DISK_NEW_UNCHECKED: u8 = 3;
+
+pub const DISK_TORN: u8 = 4;
+
+pub const DISK_FOREIGN: u8 = 5;
+
+pub fn names_collide(exact_equal: bool, casefold_equal: bool) -> bool {
+    if exact_equal {
+        return true;
+    }
+    return casefold_equal;
+}
+
+pub fn dest_check(dest_exists: bool, owner_known: bool, owner_is_this_spec: bool) -> u8 {
+    if (dest_exists == false) {
+        return WRITE_OK;
+    }
+    if (owner_known == false) {
+        return WRITE_OWNER_UNKNOWN;
+    }
+    if owner_is_this_spec {
+        return WRITE_OK;
+    }
+    return WRITE_COLLISION;
+}
+
+pub fn dest_check_today(dest_exists: bool, owner_known: bool, owner_is_this_spec: bool) -> u8 {
+    return WRITE_OK;
+}
+
+pub fn post_write_check(recorded: u64, after: u64, tested: u64, readback_equal: bool) -> u8 {
+    if (tested != recorded) {
+        return WRITE_TESTED_OTHER;
+    }
+    if (after != recorded) {
+        return WRITE_SPEC_MOVED;
+    }
+    if (readback_equal == false) {
+        return WRITE_READBACK_DIFF;
+    }
+    return WRITE_OK;
+}
+
+pub fn post_write_check_today(recorded: u64, after: u64, tested: u64, readback_equal: bool) -> u8 {
+    return WRITE_OK;
+}
+
+pub fn after_cut(proto: u8, cut: u8, foreign: bool) -> u8 {
+    if (cut == CUT_BEFORE_WRITE) {
+        return DISK_OLD;
+    }
+    if (proto == PROTO_STAGE_THEN_RENAME) {
+        if (cut == CUT_AFTER_COMMIT) {
+            return DISK_NEW_CHECKED;
+        }
+        return DISK_OLD;
+    }
+    if (cut == CUT_DURING_WRITE) {
+        return DISK_TORN;
+    }
+    if foreign {
+        if (proto == PROTO_WRITE_THEN_RESTORE) {
+            if (cut == CUT_AFTER_COMMIT) {
+                return DISK_OLD;
+            }
+        }
+        return DISK_FOREIGN;
+    }
+    return DISK_NEW_UNCHECKED;
+}
+
+pub fn cut_safe(disk: u8) -> bool {
+    if (disk == DISK_OLD) {
+        return true;
+    }
+    return (disk == DISK_NEW_CHECKED);
+}
+
+pub fn proto_cut_safe(proto: u8) -> bool {
+    if (cut_safe(after_cut(proto, CUT_DURING_WRITE, false)) == false) {
+        return false;
+    }
+    if (cut_safe(after_cut(proto, CUT_AFTER_WRITE, false)) == false) {
+        return false;
+    }
+    if (cut_safe(after_cut(proto, CUT_AFTER_WRITE, true)) == false) {
+        return false;
+    }
+    if (cut_safe(after_cut(proto, CUT_AFTER_COMMIT, false)) == false) {
+        return false;
+    }
+    return cut_safe(after_cut(proto, CUT_AFTER_COMMIT, true));
+}
+

bootstrap/src/main.rs

@@ -118,6 +118,9 @@ mod test_report_exit;
 #[path = "../gen/rust/verified/seal_identity.rs"]
 #[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)]
 mod seal_identity;
+// specs/verified/seal_write.t27 (#10457): what `seal --save` must check before and after its write.
+#[path = "../gen/rust/verified/seal_write.rs"]
+#[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)] mod seal_write;
 // specs/verified/verdict_audit.t27 (#8542): which reused verdicts `frontier --audit` reruns.
 #[path = "../gen/rust/verified/verdict_audit.rs"]
 #[allow(dead_code, unused_parens, unused_mut, unused_assignments, unused_variables, non_snake_case, non_upper_case_globals, clippy::all)]
@@ -6115,28 +6118,20 @@ fn run_seal(input_path: &str, save: bool, verify: bool, force: bool) -> anyhow::
             "tests": tests_record
         });
 
-        // The derived name and the file on disk can differ ONLY IN CASE: the
-        // tool would write `ar_restraint.json` where `ar_Restraint.json` is
-        // tracked. macOS resolves those to one file and hides it; on the
-        // case-sensitive filesystem CI runs on, `--save` would create a SECOND
-        // seal for the same spec and neither would be wrong-looking. Measured
-        // over the store: 751 filenames match the derived name exactly, 4
-        // differ only by case, 558 use the older bare-`<module>` scheme.
-        //
-        // An existing file wins, so the store cannot grow a case-variant twin.
+        // An existing file wins, even one that differs only in case: seal_write.t27 names_collide() says why.
         let derived = seal_file_path(&hashes.module, &hashes.spec_path);
-        let seal_path = fs::read_dir(&seals_dir)
-            .ok()
-            .and_then(|entries| {
-                let want = derived.file_name()?.to_string_lossy().to_lowercase();
-                entries.flatten().find_map(|e| {
-                    let p = e.path();
-                    (p.file_name()?.to_string_lossy().to_lowercase() == want).then_some(p)
-                })
-            })
-            .unwrap_or(derived);
+        let want = derived.file_name().map(|n| n.to_string_lossy().into_owned()).unwrap_or_default();
+        let seal_path = fs::read_dir(&seals_dir).ok().and_then(|es| es.flatten().map(|e| e.path()).find(|p| p.file_name().map_or(false, |n| seal_write::names_collide(n.to_string_lossy() == want, n.to_string_lossy().to_lowercase() == want.to_lowercase())))).unwrap_or(derived);
+        // seal_write.t27 dest_check: a file another spec owns, or whose owner cannot be read, is refused before any write.
+        let owner = fs::read_to_string(&seal_path).ok().and_then(|s| serde_json::from_str::<serde_json::Value>(&s).ok()).and_then(|v| v.get("spec_path")?.as_str().map(String::from));
+        if seal_write::dest_check(seal_path.exists(), owner.is_some(), owner.as_deref() == Some(hashes.spec_path.as_str())) != seal_write::WRITE_OK { eprintln!("refusing to seal {}: {} belongs to {} (seal_write.t27 dest_check). Two specs derive one seal file; rename one of them.", hashes.spec_path, seal_path.display(), owner.as_deref().unwrap_or("an unreadable owner")); std::process::exit(1); }
         let pretty = serde_json::to_string_pretty(&seal_obj)?;
-        fs::write(&seal_path, &pretty)?;
+        // seal_write.t27 post_write_check on a staged file, then one rename: a cut leaves the old seal or this checked one.
+        let staged = seal_path.with_extension("json.staged"); fs::write(&staged, &pretty)?;
+        let moved = |h: &str| (h != hashes.spec_hash) as u64;
+        let code = seal_write::post_write_check(0, moved(&format!("sha256:{}", sha256_hex(&fs::read(input_path)?))), report.read.as_ref().map_or(0, |h| moved(&format!("sha256:{h}"))), fs::read_to_string(&staged).ok().as_deref() == Some(pretty.as_str()));
+        if code != seal_write::WRITE_OK { let _ = fs::remove_file(&staged); eprintln!("refusing to seal {}: {} (seal_write.t27 code {}); the old seal is untouched. Seal again once the spec is still.", hashes.spec_path, if code == seal_write::WRITE_TESTED_OTHER { "the tests read other bytes than the hash" } else if code == seal_write::WRITE_SPEC_MOVED { "the spec changed during the seal" } else { "the staged seal did not read back" }, code); std::process::exit(1); }
+        fs::rename(&staged, &seal_path)?;
 
         // A spec can own MORE THAN ONE seal file, and writing only the
         // canonical name leaves the others describing output that no longer

bootstrap/src/test_report.rs

@@ -68,6 +68,7 @@ pub struct Report {
     /// **unwritten**, which is W586's category, and the remedy is to write the
     /// spec, not to add a test to a file with nothing in it.
     pub stub: bool,
+    pub read: Option<String>, // sha256 hex of the spec bytes the tests were built from (seal_write.t27, #10457); None when unread
     /// Set when the spec never got as far as a runnable binary.
     pub blocked: Option<String>,
     /// #6509: set when the tests ran from the plain build because the counting
@@ -87,6 +88,7 @@ impl Report {
             invariants: 0,
             stub: false,
             blocked: Some(why.into()),
+            read: None,
             uncounted: None,
         }
     }
@@ -610,6 +612,7 @@ fn run_limited(spec: &Path, specs_root: &Path, limit: Duration) -> Report {
         stub,
         blocked: None,
         uncounted,
+        read: Some(crate::sha256_hex(raw.as_bytes())),
     }
 }
 
@@ -923,6 +926,7 @@ mod tests {
             stub: false,
             blocked: None,
             uncounted: None,
+            read: None,
         }
     }
 

docs/reports/t27b_expectations.json

@@ -1806,6 +1806,7 @@
   {"path": "specs/verified/run_record.t27", "t27b": "pass"},
   {"path": "specs/verified/seal_check.t27", "t27b": "pass"},
   {"path": "specs/verified/seal_identity.t27", "t27b": "pass"},
+  {"path": "specs/verified/seal_write.t27", "t27b": "pass"},
   {"path": "specs/verified/signed_receipt.t27", "t27b": "pass"},
   {"path": "specs/verified/silicon_queue.t27", "t27b": "pass"},
   {"path": "specs/verified/silicon_runs.t27", "t27b": "pass"},