diff --git a/.trinity/seals/verified_VerifiedSealWrite.json b/.trinity/seals/verified_VerifiedSealWrite.json new file mode 100644 index 0000000000..99499fc543 --- /dev/null +++ b/.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" + } +} \ No newline at end of file diff --git a/docs/reports/t27b_expectations.json b/docs/reports/t27b_expectations.json index 4350020ffd..c39a945120 100644 --- a/docs/reports/t27b_expectations.json +++ b/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"}, diff --git a/specs/verified/seal_write.t27 b/specs/verified/seal_write.t27 new file mode 100644 index 0000000000..d9fad6ad7b --- /dev/null +++ b/specs/verified/seal_write.t27 @@ -0,0 +1,262 @@ +// SPDX-License-Identifier: Apache-2.0 +; specs/verified/seal_write.t27 -- what one seal write must guarantee before it may land in +; .trinity/seals/. The three write-safety patterns of REA 6.6.0 (github.com/morluto/rea releases), +; checked against `t27c seal --save` and `t27c frontier --reseal` on the Railway lab, t27c 0.5.2 at +; master 89254d2, 2026-10-18. +; -- +; What already exists and is NOT restated here: +; - specs/verified/seal_identity.t27 says when a new seal is kept (remint_keeps) and names the +; colliding file name: two specs can derive one seal file (parent dir and module), and frontier +; writes the other spec's seal back. `seal --save` itself never refuses. This file is the write. +; - specs/verified/seal_check.t27 says how a seal is checked later from recorded inputs. This file +; is the check the writer owes before its seal can be checked at all. +; - specs/verified/reuse.t27 owns the PART_* codes and the fail-closed rule (MISSING is never SAME). +; -- +; The three patterns, and where the pipeline stands (lab evidence: gHashTag/t27#10457): +; 1. Colliding paths are refused before any write -- MISSING. `seal --save specs/a/same/m.t27` then +; `seal --save specs/b/same/m.t27` (both `module SameName;`) both exit 0, "Seal saved to +; .trinity/seals/same_SameName.json"; the file then names specs/b, and `seal --verify` of specs/a +; reports all five hashes MISMATCH. `module Upper;` in c/case and `module upper;` in d/case collide +; the same way, through the case-insensitive lookup. The corpus has 8 such names over 2198 specs. +; 2. The hash is re-checked after the final write -- MISSING. The spec is hashed once, before its +; tests read it again. A failing spec swapped for a passing one 0-4 ms into `seal --save`, then +; swapped back, sealed "tests 1/1 pass" under the FAILING bytes' spec_hash in 14 of 18 trials; +; `seal --verify` said all hashes MATCH and `frontier --list` reused it (1000 permille) while +; `test-report` on those bytes fails. An edit during the test run left a seal whose spec_hash +; mismatched the moment it was written; `seal --save` still said "Seal saved" and exited 0. +; 3. Completed seals survive a cut run -- PRESENT for completed seals. SIGINT, SIGTERM and SIGKILL +; 6 s into a frontier reseal of six specs left 4, 2 and 3 finished seals, each verifying, and no +; partial file. The seal in flight is not safe: frontier writes first and restores from a copy +; held only in the parent's memory, so killing the parent while its child wrote specs/b's seal +; into specs/a's file left specs/a failing verification for good. +; -- +; The write rule: +; - The destination is free only when no file answers to its name (case-insensitively, as the +; lookup does), or the file there records exactly this spec_path. A file whose owner cannot be +; read is not free: fail closed, as reuse.t27 does for an unrecorded part. +; - After the seal is written to a staging file, the spec is hashed again and must equal the +; recorded spec_hash; the tests must have run on the bytes that hash names; the staged file read +; back must equal what was written. Any difference refuses the seal and leaves the old one. +; - The staged, checked file then replaces the old one by one rename. A cut at any point leaves +; the old seal or the new checked seal, never a torn file, an unchecked seal or another spec's. +; Tests pin literal codes where a code names itself, so renumbering the constants cannot pass. +; phi^2 + 1/phi^2 = 3 | TRINITY + +module VerifiedSealWrite; + +use verified::reuse; + +/// dest_check() and post_write_check() answers. +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; + +/// How a seal reaches its file. +/// IN_PLACE: `seal --save` today, fs::write straight onto the destination. +/// WRITE_THEN_RESTORE: `frontier --reseal` today, the child writes in place and the parent writes +/// the old text back from memory when remint_keeps() refuses the new seal. +/// STAGE_THEN_RENAME: the rule above. +pub const PROTO_IN_PLACE : u8 = 1; +pub const PROTO_WRITE_THEN_RESTORE : u8 = 2; +pub const PROTO_STAGE_THEN_RENAME : u8 = 3; + +/// Where a run can be cut while it seals one spec. +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; + +/// What the destination file holds after the cut. +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; + +/// Two derived seal file names name one file when they are equal or equal up to case: `--save` +/// matches an existing file case-insensitively, so case_Upper.json answers for `module upper;`. +/// Why the lookup folds case (moved here from run_seal, #10457): macOS resolves +/// ar_restraint.json and ar_Restraint.json to one file and hides the difference, while on the +/// case-sensitive filesystem CI runs on, `--save` would create a SECOND seal for the same spec and +/// neither would look wrong. Measured over the store: 751 file names match the derived name +/// exactly, 4 differ only by case, 558 use the older bare- scheme. An existing file wins, +/// so the store cannot grow a case-variant twin; dest_check() then says whose file it is. +pub fn names_collide(exact_equal: bool, casefold_equal: bool) -> bool { + if (exact_equal) { return true; } + return casefold_equal; +} + +/// May this spec's seal be written to its derived file? dest_exists covers a case-variant name; +/// owner_known says the existing file's spec_path could be read; owner_is_this_spec compares it. +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; +} + +/// `seal --save` today: it writes whatever is at the destination. Kept as the unsafe reference the +/// negative controls compare against. +pub fn dest_check_today(dest_exists: bool, owner_known: bool, owner_is_this_spec: bool) -> u8 { + return WRITE_OK; +} + +/// The check after the staged write. Hashes are stand-ins for the recorded sha256 values, compared +/// whole: recorded is the spec_hash in the seal, after is the spec hashed again once the seal is +/// staged, tested is the hash of the bytes the test run read. readback_equal says the staged file +/// read back equals the text that was written. +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; +} + +/// `seal --save` today: no check after the write. The unsafe reference. +pub fn post_write_check_today(recorded: u64, after: u64, tested: u64, readback_equal: bool) -> u8 { + return WRITE_OK; +} + +/// What the destination holds when a run sealing one spec is cut at `cut`. foreign says the new +/// seal belongs to a different spec that derived the same file name (pattern 1 not yet refused). +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) { + // the rename is the commit: before it the destination was never touched + if (cut == CUT_AFTER_COMMIT) { return DISK_NEW_CHECKED; } + return DISK_OLD; + } + if (cut == CUT_DURING_WRITE) { return DISK_TORN; } + if (foreign) { + // write-then-restore restores only after the child exits; in place never restores + if (proto == PROTO_WRITE_THEN_RESTORE) { + if (cut == CUT_AFTER_COMMIT) { return DISK_OLD; } + } + return DISK_FOREIGN; + } + return DISK_NEW_UNCHECKED; +} + +/// A cut is survivable when the file holds the old seal or the new checked one. +pub fn cut_safe(disk: u8) -> bool { + if (disk == DISK_OLD) { return true; } + return disk == DISK_NEW_CHECKED; +} + +/// A protocol is cut-safe when every cut point leaves a survivable file, for its own spec and for a +/// spec that derived the same name. +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)); +} + +test a_free_or_own_destination_is_written { + // a spec sealed for the first time + assert dest_check(false, false, false) == 0; + // a reseal of the spec's own seal + assert dest_check(true, true, true) == 0; +} + +test the_lab_collision_is_refused_before_any_write { + // specs/b/same/m.t27 into same_SameName.json, which records specs/a/same/m.t27 + assert dest_check(true, true, false) == 1; + // `module upper;` in d/case into case_Upper.json, which records c/case: the name lookup is + // case-insensitive, so the destination exists + assert names_collide(false, true) == true; + assert dest_check(names_collide(false, true), true, false) == 1; + // two names that differ beyond case are two files + assert names_collide(false, false) == false; +} + +test an_unreadable_owner_fails_closed { + // a file that answers to the name but records no readable spec_path is nobody's to overwrite + assert dest_check(true, false, false) == 2; + assert dest_check(true, false, true) == 2; +} + +test negative_control_today_writes_the_collision { + // today's save says OK where the rule refuses. If the rule is ever weakened to today's, these + // two lines stop differing and this test fails. + assert dest_check_today(true, true, false) == WRITE_OK; + assert dest_check(true, true, false) != dest_check_today(true, true, false); + assert dest_check(true, false, false) != dest_check_today(true, false, false); +} + +test negative_control_refusing_every_existing_file_is_wrong_too { + // a rule that refuses any existing file would block every reseal; the own-seal case must pass + assert dest_check(true, true, true) == WRITE_OK; +} + +test the_written_seal_names_the_bytes_it_tested { + // nothing moved: hashed, tested and re-hashed bytes agree and the read-back matches + assert post_write_check(0xeef95aea, 0xeef95aea, 0xeef95aea, true) == 0; +} + +test the_lab_swap_is_refused { + // 14 of 18 trials: spec_hash of the failing bytes (eef95aea...), tests run on the passing + // bytes, the failing bytes back on disk by the time the seal is written + assert post_write_check(0xeef95aea, 0xeef95aea, 0x2b, true) == 4; +} + +test an_edit_during_the_tests_is_refused { + // hashed and tested the same bytes, but the spec changed before the write: stale on arrival + assert post_write_check(0xeef95aea, 0x3c, 0xeef95aea, true) == 3; +} + +test a_short_or_torn_write_is_refused { + assert post_write_check(0xeef95aea, 0xeef95aea, 0xeef95aea, false) == 5; +} + +test negative_control_today_seals_the_swap { + // today's save says OK to the forged certificate the lab produced. Weaken the rule to today's + // and these lines fail. + assert post_write_check_today(0xeef95aea, 0xeef95aea, 0x2b, true) == WRITE_OK; + assert post_write_check(0xeef95aea, 0xeef95aea, 0x2b, true) != WRITE_OK; + assert post_write_check(0xeef95aea, 0x3c, 0xeef95aea, true) != WRITE_OK; + assert post_write_check(0xeef95aea, 0xeef95aea, 0xeef95aea, false) != WRITE_OK; +} + +test negative_control_a_check_of_the_hash_alone_misses_the_swap { + // re-hashing the spec after the write is not enough on its own: in the swap trials the + // failing bytes were back, so after == recorded; only the tested-bytes check catches it + var recorded : u64 = 0xeef95aea; + var after : u64 = 0xeef95aea; + assert after == recorded; + assert post_write_check(recorded, after, 0x2b, true) == WRITE_TESTED_OTHER; +} + +test stage_then_rename_survives_every_cut { + assert proto_cut_safe(PROTO_STAGE_THEN_RENAME) == true; + assert after_cut(PROTO_STAGE_THEN_RENAME, CUT_DURING_WRITE, false) == DISK_OLD; + assert after_cut(PROTO_STAGE_THEN_RENAME, CUT_AFTER_WRITE, true) == DISK_OLD; + assert after_cut(PROTO_STAGE_THEN_RENAME, CUT_AFTER_COMMIT, false) == DISK_NEW_CHECKED; +} + +test negative_control_todays_protocols_do_not { + // seal --save: fs::write in place, no check after it + assert proto_cut_safe(PROTO_IN_PLACE) == false; + assert after_cut(PROTO_IN_PLACE, CUT_DURING_WRITE, false) == DISK_TORN; + assert after_cut(PROTO_IN_PLACE, CUT_AFTER_COMMIT, true) == DISK_FOREIGN; + // frontier --reseal: the lab kill of the parent while its child wrote specs/b into specs/a's + // file left specs/a's file naming specs/b + assert proto_cut_safe(PROTO_WRITE_THEN_RESTORE) == false; + assert after_cut(PROTO_WRITE_THEN_RESTORE, CUT_AFTER_WRITE, true) == DISK_FOREIGN; + // when the parent lives to restore, the old seal is back (the lab control: "kept the old seal") + assert after_cut(PROTO_WRITE_THEN_RESTORE, CUT_AFTER_COMMIT, true) == DISK_OLD; +} + +test a_cut_never_reaches_back { + // pattern 3: each spec has its own file, so a cut while sealing one spec leaves every other + // spec where the run left it. A spec not reached yet is at CUT_BEFORE_WRITE under any protocol, + // and a finished one was committed before the cut. SIGINT, SIGTERM and SIGKILL after 6 s left + // 4, 2 and 3 finished seals, all verifying. + assert after_cut(PROTO_IN_PLACE, CUT_BEFORE_WRITE, true) == DISK_OLD; + assert after_cut(PROTO_WRITE_THEN_RESTORE, CUT_BEFORE_WRITE, true) == DISK_OLD; + assert after_cut(PROTO_STAGE_THEN_RENAME, CUT_BEFORE_WRITE, true) == DISK_OLD; +}