seal write safety: colliding seal paths are not refused and the spec hash is not re-checked after the write (REA 6.6.0 patterns) #10457

REA 6.6.0 (release) shipped three write-safety fixes: "Reject colliding extraction paths before writing", "Recheck staged output identity after its final write", and keeping completed Evidence through cancellation. Its 6.7.0 (release) duplicate-member fix is already #10421 / draft #10442. This issue checks the other three against the seal pipeline: t27c seal --save (run_seal, bootstrap/src/main.rs) and t27c frontier --reseal (run_frontier, bootstrap/src/service.rs).

Result: two gaps, one pattern present. All evidence below comes from the Railway lab, t27c 0.5.2 at master 89254d2, using only t27c commands and .t27 fixtures.

The rule is written as specs/verified/seal_write.t27 (module VerifiedSealWrite), with 14 tests and negative controls. Three weakened mutants (destination check, post-write check, rename protocol) each fail 3, 3 and 1 tests.

Gap 1: colliding seal paths are not refused before any write

seal_file_path derives .trinity/seals/<parentdir>_<module>.json, so two specs can derive one file, and --save also matches an existing file case-insensitively. seal --save writes over whatever is there. specs/verified/seal_identity.t27 (remint_keeps, file_is_its_own) already records the collision and makes frontier write the other seal back, but seal --save itself never refuses.

Fixtures: specs/a/same/m.t27 and specs/b/same/m.t27, both module SameName;.

$ t27c seal specs/a/same/m.t27 --save
tests 1/1 pass
Seal saved to .trinity/seals/same_SameName.json        rc=0  spec_path specs/a/same/m.t27
$ t27c seal specs/b/same/m.t27 --save
tests 1/1 pass
Seal saved to .trinity/seals/same_SameName.json        rc=0  spec_path specs/b/same/m.t27
$ t27c seal specs/a/same/m.t27 --verify
spec_hash: MISMATCH (saved=sha256:775339...6fe6, current=sha256:21d796...0d63)
gen_hash_zig / verilog / c / rust: MISMATCH            rc=1

• Case variant: module Upper; in specs/c/case/m.t27 and module upper; in specs/d/case/m.t27. Saving D writes into C's case_Upper.json, and seal --verify of C then reports VERIFICATION FAILED.
• Corpus: 2198 specs have a module line, and 8 derived names collide case-insensitively: a_b_c_spec, coder_igla-coder-pipeline, openxc7-synth_quantum_bridge_top, openxc7-synth_trinity_top (about 35 specs), rtl-root_trinity_top (11), scripts_port-scripts, src_port::trios::crates::trios_igla_trainer::src, tri_port::trinity::src::tri (5).
• frontier --reseal: if the run is not cut, frontier prints "kept the old seal specs/b/same/m.t27" and A still verifies. If the frontier parent is killed (SIGKILL) while its child t27c seal specs/b/same/m.t27 --save runs, the file is left holding spec_path specs/b/same/m.t27, and A reports "VERIFICATION FAILED". The copy needed to restore the file was held only in the parent's memory.

Gap 2: the hash is not re-checked after the final write

compute_seal_hashes reads and hashes the spec once. test_report::run then reads the file again to run the tests, and fs::write writes the seal. Nothing re-hashes the spec or reads the seal back after the write.

Fixtures:

• old.t27: module Flip;, which() returns 1, test which_is_two fails.
• new.t27: returns 2, the test passes.

Steps: copy old into specs/r/flip.t27. Swap in new atomically 0 to 4 ms after seal --save starts. Once the save finishes, swap old back.

delay=0..0.004  save_rc=0  tests 1/1 pass    (14 of 18 trials; at 5 ms and later: "refusing to seal ... 1 of 1 test(s) FAIL")
$ grep spec_hash .trinity/seals/r_Flip.json
  "spec_hash": "sha256:eef95aeac1a1bcf4e11d4ffc321ebe6bc9fff90d4f04951ff092195e9847b243"   <- the FAILING bytes
$ t27c seal specs/r/flip.t27 --verify
all hashes MATCH                                       verify_rc=0
$ t27c test-report specs/r/flip.t27
  -  which_is_two   (failed, not counted)
$ t27c frontier --list
frontier: reused 1 of 1 (1000 permille)

The seal certifies a passing run for bytes that fail, and frontier reuses it.

• Non-atomic swap: with cp instead of mv at 5 ms, the save sealed "tests 0/0 pass", and verify reported MATCH.
• Edit during the test run: a 0.3 s sleep, then a comment-only edit. seal --save printed "Seal saved" and exited 0, and an immediate seal --verify reported spec_hash MISMATCH, rc=1. The seal was already stale when written, and the writer never noticed.

Pattern 3: completed seals survive a cut run (present, with one caveat)

Steps: run timeout -s <SIG> 6 t27c frontier --reseal over six never-sealed specs (specs/batch/s1..s6.t27).

Caveat: the seal in flight is not protected. The child writes in place with a non-atomic fs::write, and the restore happens only if the parent survives, which is the gap 1 frontier case above. A torn seal file is possible from reading the code but was not reproduced.

The rule (specs/verified/seal_write.t27)

• dest_check: the destination is free only when no file answers to the name (case-insensitively), or the file there records exactly this spec_path. An unreadable owner fails closed.
• post_write_check: after the seal is written to a staging file, three things must hold, or the seal is refused:
  • the spec re-hashes to the recorded spec_hash;
  • the tests ran on the bytes that hash names;
  • the staged file reads back as written.
• after_cut / proto_cut_safe: the checked staging file replaces the old seal with one rename. A cut at any point leaves either the old seal or the new checked one. seal --save (in place) and frontier --reseal (write, then restore from memory) both fail this today.

Closing the gaps

Closing these needs Rust changes in run_seal and run_frontier. They are in a separate draft PR that waits for the owner's owner-approved-foreign label.

User Scenarios

• Given two specs at different paths (specs/a/same/m.t27 and specs/b/same/m.t27) that derive the same seal file name case-insensitively, when running t27c seal --save on the first then the second, then the second save MUST be refused before any write occurs and exit non-zero.
• Given a spec file that is atomically replaced with different content during t27c seal --save execution, when the write completes, then the seal MUST be refused because the re-checked spec hash no longer matches the recorded spec_hash.
• Given a t27c frontier --reseal run processing multiple specs, when the parent process is killed by SIGKILL while a child t27c seal --save is writing, then the pre-existing seal file for that spec MUST remain intact and verifiable with t27c seal --verify.

Requirements

• FR-001: t27c seal --save MUST refuse to write if the destination seal file exists and records a different spec_path (case-insensitive collision check on the derived seal name).
• FR-002: t27c seal --save MUST re-hash the spec file after the final write and refuse the seal if the hash differs from the recorded spec_hash.
• FR-003: t27c seal --save MUST write to a staging file and atomically rename it to the destination, ensuring a torn write leaves either the old seal or the new verified seal.
• FR-004: t27c frontier --reseal MUST protect in-flight seal writes by using the same staging-and-rename protocol, so that a killed parent does not leave a corrupted seal file.
• FR-005: The post-write verification MUST confirm that the tests ran on the bytes that hash to the recorded spec_hash and that the staged file reads back as written.

Success Criteria

• t27c test specs/verified/seal_write.t27 passes all 14 tests (exit 0)
• t27c seal specs/a/same/m.t27 --save then t27c seal specs/b/same/m.t27 --save results in the second command exiting non-zero
• t27c seal specs/c/case/m.t27 --save then t27c seal specs/d/case/m.t27 --save results in the second command exiting non-zero
• Atomic swap of spec content during t27c seal --save causes the command to exit non-zero and no seal is written
• t27c frontier --reseal interrupted by SIGKILL leaves all pre-existing seals verifiable via t27c seal --verify (exit 0 for each)

Boundary

• specs/verified/seal_write.t27
• specs/verified/seal_identity.t27
• bootstrap/src/main.rs
• bootstrap/src/service.rs
• .trinity/seals/same_SameName.json
• .trinity/seals/r_Flip.json