Repository navigation
Conversation
…(REA 6.6.0 patterns) Three write-safety patterns from REA 6.6.0, checked against `t27c seal --save` and `t27c frontier --reseal` on the Railway lab (t27c 0.5.2, master 89254d2): - colliding seal paths refused before any write: missing - the spec hash re-checked after the final write: missing - completed seals survive a cut run: present, except the seal in flight specs/verified/seal_write.t27 writes the rule: dest_check (free, own or refused; an unreadable owner fails closed), post_write_check (re-hashed spec, tested bytes and read-back must all equal the recorded seal) and after_cut / proto_cut_safe (stage then rename leaves the old seal or the new checked one). Today's save and reseal are modelled as the unsafe references the negative controls compare against. 14 tests, 0 vacuous; three weakened mutants each fail their controls. Sealed on the lab with --save, no --force. Refs #10457 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…; t27b ledger names it names_collide() now holds the measured reason for the case-insensitive seal lookup (751 exact, 4 case-only, 558 bare-module names), so the Rust copy of that comment can go when run_seal calls the spec (draft fix PR). The t27b ledger gains the spec's entry (t27b pass), which the ratchet listed as UNLISTED. Resealed on the lab with --save, no --force: 14/14, 0 vacuous, all hashes MATCH. Refs #10457 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…ter the write, land it by rename run_seal now follows specs/verified/seal_write.t27 (#10457, spec #10458), calling its generated functions rather than restating them: - dest_check before any write: a seal file whose recorded spec_path is another spec, or cannot be read, is refused (exit 1) and left as it is. - post_write_check after the write: the seal goes to <seal>.json.staged; the spec is re-hashed, the bytes the tests were built from (new test_report::Report.read) must equal the recorded spec_hash, and the staged file must read back as written. Any difference removes the staged file and exits 1. - One fs::rename lands the checked seal, so a cut leaves the old seal or the new checked one. - The case-insensitive seal lookup now calls names_collide(), and its 9-line rationale comment moved into the spec (#10458), so the diff removes more hand-written Rust than it adds (+19/-20), as the foreign-budget shrink rule requires. Lab, t27c 0.5.2 built from this branch: the module collision and the case-variant collision are refused and the first seal still verifies; the spec swapped 0-4 ms into the save is refused (code 4, was sealed "1/1 pass" under the failing bytes); an edit during the tests is refused (code 3); a frontier killed mid-child no longer leaves the other spec's seal in the file; cut batches keep every finished seal. bootstrap/gen/rust/verified/seal_write.rs is t27c gen-rust output. Refs #10457 Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Contributor
This was referenced Oct 18, 2026
Merged
Merged
Merged
Merged
This was referenced Oct 19, 2026
Draft
Merged
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Draft: waits for the owner's
owner-approved-foreignlabel. Do not merge without it. This PR edits existing Rust in t27c (bootstrap/src/main.rs+15/-20,bootstrap/src/test_report.rs+4: fewer hand-written Rust lines than before). The rule it applies is the t27 specspecs/verified/seal_write.t27(#10458). The Rust calls the spec's generated functions (bootstrap/gen/rust/verified/seal_write.rs,t27c gen-rustoutput) instead of restating them.Closes the two gaps found in #10457 and protects the seal in flight.
What changes in
t27c seal --savedest_checkbefore any write. If the seal file exists and its recordedspec_pathis another spec, or cannot be read, the seal is refused with exit 1 and the file is left untouched.post_write_checkafter the write. The seal is written to<seal>.json.staged, then three checks run:Report.read, sha256 of the sourcetest_reportcompiled) must equal the recordedspec_hash;If any check fails, the staged file is removed and the old seal stays.
One
fs::renamelands the checked seal, so a cut leaves either the old seal or the new checked one.The case-insensitive seal lookup calls
names_collide. Its 9-line rationale comment (macOS hides case, the 751/4/558 store count, why an existing file wins) moved into the spec in feat(verified): seal_write.t27 -- what one seal write must guarantee (REA 6.6.0 patterns) #10458, so the Rust keeps a one-line pointer.frontier --resealneeds no change: its child isseal --save, so it now refuses a foreign file before writing and lands its own seal by rename.Owner's acceptance criteria (2026-10-18)
dest_checkthe_lab_collision_is_refused_before_any_write,an_unreadable_owner_fails_closedplus 2 negative controls; lab rows 1-2 belowpost_write_checkthe_lab_swap_is_refused,an_edit_during_the_tests_is_refused,a_short_or_torn_write_is_refusedplus 2 negative controls; lab rows 3-4stage_then_rename_survives_every_cut,a_cut_never_reaches_backplus 1 negative control; lab rows 5-6Lab: t27c built from this branch (Railway, commit e408800), the #10457 fixtures
module SameName;inspecs/a/sameandspecs/b/same, save A then B--verifyrefusing to seal specs/b/same/m.t27: .trinity/seals/same_SameName.json belongs to specs/a/same/m.t27, exit 1; Aall hashes MATCH; resealing A still worksmodule Upper;vsmodule upper;case_Upper.json--savethe tests read other bytes than the hash (seal_write.t27 code 4), 2 caught by the failing test itself. In the 12th (0 ms) the swap landed before the seal read the spec, so it sealed the passing bytes under their own hash (a rerun of 6 such trials: 5 refused, 1 sealed withspec_hashequal to the new file's sha256). No.stagedfile left in any trial--verifyMISMATCHthe spec changed during the seal (seal_write.t27 code 3), exit 1seal specs/b/same/m.t27 --saverunsall hashes MATCHtimeout -s INT/TERM/KILL 6 frontier --resealover six new specsA spec that is not being edited still seals and verifies (
calm.t27). On the lab,cargo test --release -p t27c test_reportpasses 19/19 andcargo test --release -p t27c sealpasses 17/17.Behaviour change to review
A seal file whose
spec_pathnames a different spec now refuses a reseal, where today it is silently overwritten. A spec moved without its seal is one example. This fails closed by design: move the seal file with the spec, or delete it, and reseal. The 8 colliding names in the corpus (#10457) will refuse their second seal until one module is renamed.Not changed
The twin-file loop in
run_seal, which rewrites other seal files that already name the samespec_path, still uses a plainfs::write. It only touches files that belong to this spec.Refs #10457 · spec #10458
🤖 Generated with Claude Code