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/bootstrap/gen/rust/verified/seal_write.rs b/bootstrap/gen/rust/verified/seal_write.rs new file mode 100644 index 0000000000..b0d5fab194 --- /dev/null +++ b/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)); +} + diff --git a/bootstrap/src/main.rs b/bootstrap/src/main.rs index 9c5481aa0b..f6256b96e7 100644 --- a/bootstrap/src/main.rs +++ b/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-`` 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::(&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 diff --git a/bootstrap/src/test_report.rs b/bootstrap/src/test_report.rs index 6333735eac..2612ee3905 100644 --- a/bootstrap/src/test_report.rs +++ b/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, // 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, /// #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, } } 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; +}