diff --git a/.gitignore b/.gitignore index cfbaa79cb4..30dd244d45 100644 --- a/.gitignore +++ b/.gitignore @@ -120,6 +120,7 @@ specs/scratch/ # rather than into tools/seal_baseline.txt, which would turn a green invariant into # permanent debt. .trinity/seals/scratch_*.json +.trinity/seals/.*.part-* # Coq build artifacts. 208 of these were committed, carrying the absolute build # path of the machine that produced them -- which is what secret-scan kept diff --git a/.trinity/seals/verified_VerifiedSealWrite.json b/.trinity/seals/verified_VerifiedSealWrite.json index 99499fc543..2bae40b58b 100644 --- a/.trinity/seals/verified_VerifiedSealWrite.json +++ b/.trinity/seals/verified_VerifiedSealWrite.json @@ -1,5 +1,5 @@ { - "built_by": "t27c-bootstrap@0.5.2+89254d2", + "built_by": "t27c-bootstrap@0.5.2+1c8355564", "closure": [ { "spec": "specs/verified/reuse.t27", @@ -7,27 +7,27 @@ } ], "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", + "gen_hash_c": "sha256:83fc54f9e69b0bee6207596b3c42f717f39c5511bdf3c9f9f7a8c68de37d3af2", + "gen_hash_rust": "sha256:3d720a3281aafdb385553d605568744bc6d22737c36e191cb21bc0b312ddce71", + "gen_hash_verilog": "sha256:0ff338e626b39ad8e37e4d23f6138c77bb647ec61ba5031a007f614148924cb2", + "gen_hash_zig": "sha256:d40c2f9cf839b7b9ce15e741a6f7e9d8414b0543a031135bf20abdaee5180a57", "module": "VerifiedSealWrite", "ring": 12, "seal_schema": 2, - "sealed_at": "2026-10-18T12:55:35Z", + "sealed_at": "2026-10-18T13:37:42Z", "sealed_by": "t27c-bootstrap@0.5.2", - "spec_hash": "sha256:59262b1a210bd4775ef0dec0db9a52f1333069afb946cf4cd88c6cb894a6b6e0", + "spec_hash": "sha256:063e7ceb6f5c8106097b1185079c306108630bdff7877ebb947485deb27ac390", "spec_path": "specs/verified/seal_write.t27", "tests": { "failed": 0, "failing": [], "forced": false, - "passed": 14, - "total": 14, + "passed": 19, + "total": 19, "vacuous": 0 }, "toolchain": { - "test_runner": "sha256:1982ae948e24d00c5d221ccec12dfce1eb01204b53e37b0f857f93b16d64629d", + "test_runner": "sha256:8512b80da533b79289110fca4a65f3336abd7a059ca4b72ea595d5e33ff8ad10", "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..ac99637aaa --- /dev/null +++ b/bootstrap/gen/rust/verified/seal_write.rs @@ -0,0 +1,154 @@ +// Generated from .t27 spec +// DO NOT EDIT — generated by t27c +// NOT LOWERED BY THIS BACKEND: 19 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 WRITE_GEN_MOVED: u8 = 6; + +pub const SEAL_STAGE_SUFFIX: &'static str = ".part"; + +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 dest_allowed(code: u8, force: bool) -> bool { + if (code == WRITE_OK) { + return true; + } + if (code == WRITE_OWNER_UNKNOWN) { + return force; + } + return false; +} + +pub fn gens_check(code: u8, gens_same: bool) -> u8 { + if (code != WRITE_OK) { + return code; + } + if gens_same { + return WRITE_OK; + } + return WRITE_GEN_MOVED; +} + +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..c826932b61 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, #10454): what one seal write must check before and after it lands. +#[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)] @@ -5859,6 +5862,16 @@ fn seal_file_path(module: &str, input_path: &str) -> std::path::PathBuf { Path::new(".trinity").join("seals").join(name) } +/// seal_write.t27 STAGE_THEN_RENAME (#10454): stage `..part-` beside the seal, sync, let `check` judge the staged file, then one rename; any other answer removes the stage and leaves the old seal. +fn write_seal_atomic(path: &Path, bytes: &[u8], check: impl FnOnce(&Path) -> u8) -> anyhow::Result { + let (dir, part) = (path.parent().filter(|d| !d.as_os_str().is_empty()).unwrap_or(Path::new(".")), path.with_file_name(format!(".{}{}-{}", path.file_name().unwrap_or_default().to_string_lossy(), seal_write::SEAL_STAGE_SUFFIX, std::process::id()))); + let w = fs::File::create(&part).and_then(|mut f| { std::io::Write::write_all(&mut f, bytes)?; f.sync_all() }).map(|_| check(&part)).and_then(|c| if c == seal_write::WRITE_OK { fs::rename(&part, path).map(|_| c) } else { Ok(c) }); + if w.as_ref().map_or(true, |c| *c != seal_write::WRITE_OK) { let _ = fs::remove_file(&part); } let c = w.with_context(|| format!("writing {}", path.display()))?; if let Ok(d) = fs::File::open(dir) { let _ = d.sync_all(); } Ok(c) +} +/// The staged file read back equals what was written (seal_write.t27 post_write_check's readback_equal). +fn staged_is(bytes: &[u8]) -> impl FnOnce(&Path) -> u8 + '_ { move |p| seal_write::post_write_check(0, 0, 0, fs::read(p).map_or(false, |b| b == bytes)) } +/// The five hashes a seal records, in the order seal prints them. +fn hash_pairs(h: &SealHashes) -> [(&'static str, &String); 5] { [("spec_hash", &h.spec_hash), ("gen_hash_zig", &h.gen_hash_zig), ("gen_hash_verilog", &h.gen_hash_verilog), ("gen_hash_c", &h.gen_hash_c), ("gen_hash_rust", &h.gen_hash_rust)] } /// The producer identity a seal and a receipt both carry: `name@version+git`, /// defined ONCE. specs/verified/receipt.t27's `producer_matches` compares two /// producer identities verbatim -- no normalization anywhere, matching is not @@ -5939,13 +5952,7 @@ fn run_seal(input_path: &str, save: bool, verify: bool, force: bool) -> anyhow:: serde_json::from_str(&fs::read_to_string(&seal_path)?)?; let mut all_match = true; - let checks = [ - ("spec_hash", &hashes.spec_hash), - ("gen_hash_zig", &hashes.gen_hash_zig), - ("gen_hash_verilog", &hashes.gen_hash_verilog), - ("gen_hash_c", &hashes.gen_hash_c), - ("gen_hash_rust", &hashes.gen_hash_rust), - ]; + let checks = hash_pairs(&hashes); for (field, current) in &checks { let saved = saved_json @@ -6115,28 +6122,19 @@ 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); let pretty = serde_json::to_string_pretty(&seal_obj)?; - fs::write(&seal_path, &pretty)?; + // seal_write.t27 dest_check + dest_allowed (#10454): another spec's seal is refused, --force included; an unreadable owner (torn or legacy) only with --force. + let owner = fs::read(&seal_path).ok().and_then(|b| serde_json::from_slice::(&b).ok()).and_then(|v| v["spec_path"].as_str().map(|s| s.trim_start_matches("./").to_string())); + let dest = seal_write::dest_check(seal_path.exists(), owner.is_some(), owner.as_deref() == Some(hashes.spec_path.as_str())); + if !seal_write::dest_allowed(dest, force) { eprintln!("refusing to seal {}: {}", hashes.spec_path, if dest == seal_write::WRITE_COLLISION { format!("{} is the seal of {}, and both specs derive that name (parent directory + module). Rename one spec's module or directory; --force does not override this.", seal_path.display(), owner.unwrap_or_default()) } else { format!("{} names no readable spec_path (a torn write or a legacy seal); --force replaces it.", seal_path.display()) }); std::process::exit(1); } else if dest == seal_write::WRITE_OWNER_UNKNOWN { println!("{} names no readable spec_path: replacing it (--force)", seal_path.display()); } + // seal_write.t27 post_write_check + gens_check judge the staged file before the rename: the spec hashed and generated again, the bytes the tests read, the stage read back. + let tested = report.read.as_ref().map_or(0, |r| (format!("sha256:{r}") != hashes.spec_hash) as u64); // 0 = the recorded bytes, or no test read any + let code = write_seal_atomic(&seal_path, pretty.as_bytes(), |p| { let again = compute_seal_hashes(input_path).ok(); seal_write::gens_check(seal_write::post_write_check(0, again.as_ref().map_or(1, |a| (a.spec_hash != hashes.spec_hash) as u64), tested, staged_is(pretty.as_bytes())(p) == seal_write::WRITE_OK), again.map_or(false, |a| hash_pairs(&a)[1..] == hash_pairs(&hashes)[1..])) })?; + if code != seal_write::WRITE_OK { eprintln!("seal of {} not kept: {}; the old seal is untouched", hashes.spec_path, match code { seal_write::WRITE_TESTED_OTHER => "the tests read other bytes than the ones hashed", seal_write::WRITE_SPEC_MOVED => "the spec changed while it was being sealed", seal_write::WRITE_READBACK_DIFF => "the staged file read back is not the seal written", _ => "a second generation of the same spec gave other code (a gen hash nobody can reproduce)" }); std::process::exit(1); } // A spec can own MORE THAN ONE seal file, and writing only the // canonical name leaves the others describing output that no longer @@ -6154,62 +6152,23 @@ fn run_seal(input_path: &str, save: bool, verify: bool, force: bool) -> anyhow:: // each file has it, because the file is NAMED after that field and // overwriting it would leave a seal whose name and contents disagree -- // which is the defect this is repairing, not a second copy of it. - let mut also_updated = 0usize; - if let Ok(entries) = fs::read_dir(&seals_dir) { - for entry in entries.flatten() { - let path = entry.path(); - if path == seal_path || path.extension().and_then(|e| e.to_str()) != Some("json") { - continue; - } - let Ok(text) = fs::read_to_string(&path) else { continue }; - let Ok(mut existing) = serde_json::from_str::(&text) else { - continue; - }; - if existing.get("spec_path").and_then(|v| v.as_str()) != Some(hashes.spec_path.as_str()) - { - continue; - } - for (k, v) in [ - ("spec_hash", &hashes.spec_hash), - ("gen_hash_zig", &hashes.gen_hash_zig), - ("gen_hash_verilog", &hashes.gen_hash_verilog), - ("gen_hash_c", &hashes.gen_hash_c), - ("gen_hash_rust", &hashes.gen_hash_rust), - ] { - existing[k] = serde_json::Value::String(v.clone()); - } - existing["sealed_at"] = serde_json::Value::String(now.clone()); - existing["tests"] = tests_record.clone(); - if let Ok(out) = serde_json::to_string_pretty(&existing) { - if fs::write(&path, &out).is_ok() { - also_updated += 1; - } - } - } - } - - // Also print hashes to stdout - println!("spec_hash={}", hashes.spec_hash); - println!("gen_hash_zig={}", hashes.gen_hash_zig); - println!("gen_hash_verilog={}", hashes.gen_hash_verilog); - println!("gen_hash_c={}", hashes.gen_hash_c); - println!("gen_hash_rust={}", hashes.gen_hash_rust); + let (mut also_updated, mut twins_failed) = (0usize, Vec::new()); + for path in fs::read_dir(&seals_dir).into_iter().flatten().flatten().map(|e| e.path()).filter(|p| p != &seal_path && p.extension().and_then(|e| e.to_str()) == Some("json")) { + let Some(mut existing) = fs::read_to_string(&path).ok().and_then(|t| serde_json::from_str::(&t).ok()) else { continue }; + if existing.get("spec_path").and_then(|v| v.as_str()) != Some(hashes.spec_path.as_str()) { continue; } + for (k, v) in hash_pairs(&hashes) { existing[k] = serde_json::Value::String(v.clone()); } + existing["sealed_at"] = serde_json::Value::String(now.clone()); existing["tests"] = tests_record.clone(); + let out = serde_json::to_string_pretty(&existing)?; // #10454: staged, read back, renamed; a twin that failed is named and fails the command, not skipped + if write_seal_atomic(&path, out.as_bytes(), staged_is(out.as_bytes())).map_or(false, |c| c == seal_write::WRITE_OK) { also_updated += 1 } else { twins_failed.push(path.display().to_string()) } + } + for (k, v) in hash_pairs(&hashes) { println!("{k}={v}"); } println!("\nSeal saved to {}", seal_path.display()); - if also_updated > 0 { - // Said out loud: a command that silently touched other files would - // be worse than one that touches too few. - println!( - " and {} other seal file(s) naming the same spec", - also_updated - ); - } + // Said out loud: a command that silently touched other files would be worse than one that touches too few. + if also_updated > 0 { println!(" and {} other seal file(s) naming the same spec", also_updated); } + anyhow::ensure!(twins_failed.is_empty(), "{} other seal file(s) naming {} were not rewritten: {}", twins_failed.len(), hashes.spec_path, twins_failed.join(", ")); } else { // Default: just print hashes (existing behavior, enhanced with all backends) - println!("spec_hash={}", hashes.spec_hash); - println!("gen_hash_zig={}", hashes.gen_hash_zig); - println!("gen_hash_verilog={}", hashes.gen_hash_verilog); - println!("gen_hash_c={}", hashes.gen_hash_c); - println!("gen_hash_rust={}", hashes.gen_hash_rust); + for (k, v) in hash_pairs(&hashes) { println!("{k}={v}"); } } Ok(()) diff --git a/bootstrap/src/service.rs b/bootstrap/src/service.rs index e92b40fd7f..564841ccbe 100644 --- a/bootstrap/src/service.rs +++ b/bootstrap/src/service.rs @@ -5672,7 +5672,7 @@ pub fn run_frontier(list: bool, reseal: bool, audit: Option, watch: bool, o let keep = sealed && si::remint_keeps(new["seal_schema"].as_u64().unwrap_or(0) as u32, new.pointer("/tests/failed").and_then(|v| v.as_u64()) == Some(0), new.pointer("/tests/forced").and_then(|v| v.as_bool()) == Some(true), new.pointer("/tests/total").and_then(|v| v.as_u64()).unwrap_or(0) as u32, src.lines().filter(|l| l.trim_start().starts_with("invariant ")).count() as u32, new.pointer("/tests/vacuous").and_then(|v| v.as_u64()).unwrap_or(0) as u32, !old.iter().any(|(f, _, mine)| f == &primary && !mine)); let same = |o: &str| serde_json::from_str::(o).map_or(false, |mut v| { v["sealed_at"] = new["sealed_at"].clone(); v["built_by"] = new["built_by"].clone(); v == new }); // only when and by which build: no change if !keep && !old.iter().any(|(f, ..)| f == &primary) { let _ = std::fs::remove_file(&primary); } - for (f, o, mine) in &old { std::fs::write(f, if keep && *mine && !same(o) { serde_json::to_string_pretty(&new)? } else { o.clone() })? } + for (f, o, mine) in &old { let b = if keep && *mine && !same(o) { serde_json::to_string_pretty(&new)? } else { o.clone() }; anyhow::ensure!(crate::write_seal_atomic(f, b.as_bytes(), crate::staged_is(b.as_bytes()))? == crate::seal_write::WRITE_OK, "{} read back other bytes", f.display()) } // #10454 seal_write.t27 STAGE_THEN_RENAME: a killed reseal leaves no torn seal println!("{} {p}", if keep { "resealed" } else { "kept the old seal" }); } let _ = std::fs::remove_dir_all(&zc); diff --git a/bootstrap/src/test_report.rs b/bootstrap/src/test_report.rs index 6333735eac..d15e91db0b 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 post_write_check `tested`, #10454); 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/specs/verified/seal_write.t27 b/specs/verified/seal_write.t27 index d9fad6ad7b..0c997f6fbc 100644 --- a/specs/verified/seal_write.t27 +++ b/specs/verified/seal_write.t27 @@ -33,10 +33,12 @@ ; 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. +; read is not free: fail closed, as reuse.t27 does for an unrecorded part. --force opens an +; unreadable owner and never another spec's file (dest_allowed, #10454). ; - 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. +; back must equal what was written; the spec generated again must give the recorded gen hashes +; (gens_check). 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. @@ -53,6 +55,13 @@ 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; +/// gens_check(): the spec held still, but generating it again gave other code, so the seal would +/// record a gen hash nobody can reproduce. +pub const WRITE_GEN_MOVED : u8 = 6; + +/// The staging file is `.-` beside the seal. Seal readers take +/// only `*.json`, so a staged file a cut left behind is never read as a seal. +pub const SEAL_STAGE_SUFFIX : str = ".part"; /// How a seal reaches its file. /// IN_PLACE: `seal --save` today, fs::write straight onto the destination. @@ -115,6 +124,25 @@ pub fn post_write_check(recorded: u64, after: u64, tested: u64, readback_equal: return WRITE_OK; } +/// May `seal --save` write, given dest_check()'s answer? A collision is another spec's seal and +/// nothing lifts it, --force included: forcing would only move the damage to the other spec. An +/// unknown owner is a file that does not parse (a torn write from before staging) or a legacy seal +/// with no spec_path; the writer cannot prove it is someone else's, so it stays closed unless the +/// person sealing says --force. +pub fn dest_allowed(code: u8, force: bool) -> bool { + if (code == WRITE_OK) { return true; } + if (code == WRITE_OWNER_UNKNOWN) { return force; } + return false; +} + +/// The gen half of the check after the staged write: post_write_check()'s answer stands when it +/// refuses; otherwise the four gen hashes computed again must equal the ones recorded. +pub fn gens_check(code: u8, gens_same: bool) -> u8 { + if (code != WRITE_OK) { return code; } + if (gens_same) { return WRITE_OK; } + return WRITE_GEN_MOVED; +} + /// `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; @@ -260,3 +288,41 @@ test a_cut_never_reaches_back { 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; } + +test force_lifts_an_unknown_owner_and_never_a_collision { + // a free or own destination needs no force + assert dest_allowed(dest_check(false, false, false), false) == true; + assert dest_allowed(dest_check(true, true, true), false) == true; + // a torn or legacy seal (owner unreadable) stays closed until the person sealing says --force + assert dest_allowed(WRITE_OWNER_UNKNOWN, false) == false; + assert dest_allowed(WRITE_OWNER_UNKNOWN, true) == true; + // another spec's seal: --force does not open it + assert dest_allowed(WRITE_COLLISION, true) == false; + assert dest_allowed(dest_check(true, true, false), true) == false; +} + +test negative_control_force_for_everything_would_reopen_the_collision { + // a rule where --force lifts every refusal agrees on the unknown owner and differs only on the + // collision; if dest_allowed is ever weakened to that, this line fails + assert dest_allowed(WRITE_COLLISION, true) != dest_allowed(WRITE_OWNER_UNKNOWN, true); +} + +test a_second_generation_must_give_the_recorded_code { + assert gens_check(WRITE_OK, true) == 0; + assert gens_check(WRITE_OK, false) == 6; + // the spec check speaks first: a moved spec is reported as moved, not as moved gens + assert gens_check(post_write_check(0xeef95aea, 0x3c, 0xeef95aea, true), false) == 3; + assert gens_check(post_write_check(0xeef95aea, 0xeef95aea, 0x2b, true), true) == 4; +} + +test negative_control_the_spec_check_alone_misses_moved_gens { + // nothing about the spec moved, so post_write_check says OK; only gens_check refuses + assert post_write_check(0xeef95aea, 0xeef95aea, 0xeef95aea, true) == WRITE_OK; + assert gens_check(post_write_check(0xeef95aea, 0xeef95aea, 0xeef95aea, true), false) != WRITE_OK; +} + +test the_stage_suffix_is_not_a_seal_name { + // readers take *.json; the staged name ends in SEAL_STAGE_SUFFIX-, never in .json + assert SEAL_STAGE_SUFFIX == ".part"; + assert SEAL_STAGE_SUFFIX != ".json"; +}