diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 21d815c..d68c5af 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -44,7 +44,7 @@ property-tests = "9 (2026-04-03 assessment, not re-derived)" regression-tests = "5 (2026-04-03 assessment, not re-derived)" idris2-proofs = "12 PROVEN ledger rows (the former 30 counted lemmas before the tautology purge; PROOF-NEEDS.adoc is authoritative)" benchmarks = "5 Criterion groups (no baseline recorded)" -total = "136 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check" +total = "141 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check" [proof-grades] # mathesis (estate-mathematical-architecture §5/§6) + standards @@ -55,7 +55,7 @@ grade-3-pending = "E-1m — Epistemic.agda; no receipt yet, because the receipt- receipt-commit = "4afb710e86646658f667f10bd6274ee47416bfc7 (agda-proofs.yml run 40867211509, success)" receipt-prover = "Agda 2.6.4.3 (agda-bin=2.6.4.3-1+b2); resource-algebra pinned at cf9235c" receipt-flags = "--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check (canonical per PROOF-POLICY §2.1 since 2026-11-01; the 4afb710 CI receipt predates the flag, so the next agda-proofs.yml run is its receipt)" -not-graded = "the 7 Idris2 PROVEN rows (ABI/interface contracts, PROOF-POLICY §1); all 23 TESTED rows (observed behaviour); ASSUMED/DESIGNED/OPEN rows" +not-graded = "the 7 Idris2 PROVEN rows (ABI/interface contracts, PROOF-POLICY §1); all 29 TESTED rows (observed behaviour); ASSUMED/DESIGNED/OPEN rows" open-obligations = "re-earn the Agda receipt in CI under the canonical flag set; one Agda version across CI (agda-proofs pins 2.6.4.3, dashboard-check installs 2.6.3); no Creusot contract on the Rust, and neither rustc nor crates.io is reachable from the agent sandbox (docs/estate/environment-toolchains.md), so no Rust behaviour is graded" claimed-higher = "none — no Grade 2i, 2ii or 1 is claimed" diff --git a/.machine_readable/bot_directives/git-private-farm.a2ml b/.machine_readable/bot_directives/git-private-farm.a2ml index 2285a06..179169b 100644 --- a/.machine_readable/bot_directives/git-private-farm.a2ml +++ b/.machine_readable/bot_directives/git-private-farm.a2ml @@ -3,18 +3,20 @@ [metadata] repo = "januskey" -last-updated = "2026-06-12" +last-updated = "2026-11-04" owner = "hyperpolymath" [propagation] -enabled = true -workflow = ".github/workflows/instant-sync.yml" +enabled = false +workflow = "" +retired = "instant-sync.yml was deleted in #156 (it was already disabled); no workflow in this repo dispatches to the farm, so nothing propagates until one is added" target = "hyperpolymath/.git-private-farm" event-type = "propagate" secret-name = "FARM_DISPATCH_TOKEN" presence-gated = false -presence-gated-notes = "The dispatch step runs unconditionally on push to main/master and on published releases; there is no `if:` secret-presence gate, so the step fails (rather than skips) where the secret is absent (e.g. forks)." -triggers = ["push to main/master", "release published"] +presence-gated-notes = "Historical (inactive since #156): the retired instant-sync.yml dispatched unconditionally, with no secret-presence gate." +triggers = [] +historical-triggers = ["push to main/master", "release published"] [never-propagate] items = ["secrets", "unmerged branches", "work-in-progress"] diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 901f60a..9157535 100644 --- a/EXPLAINME.adoc +++ b/EXPLAINME.adoc @@ -21,7 +21,7 @@ operation-specific inverse — no filesystem scan, no tape restore. theorem. The ledger row "every operation is reversible, as a theorem linked to the Rust" is **OPEN**; the Agda proof covers a transaction *model* (T-1..T-3) whose step-level premise is tested, not proved (T-6), and the operation metadata -log now saves by rename but that change is unbuilt (T-8, OPEN). Reversibility also fails +log saves by rename, a failed save of an edit changes nothing and a failed append stays pending for the next save (T-8, TESTED), but a file change whose log record fails to persist is not recoverable (T-9, OPEN). Reversibility also fails outright if the store is lost, and `jk obliterate` and `jk gc` are deliberate exceptions that destroy what undo would need. What has been restored, and what has not, is tabulated in `docs/wiki/theory/rmr-primitive.md` §2. @@ -53,7 +53,7 @@ it does not make the file immutable, and an attacker with write access can delet the whole log. **Evidence:** `crates/reversible-core/src/metadata.rs` (log structure and -`save` — see the T-8 caveat), `crates/januskey-cli/src/attestation.rs` (HMAC +`save` — T-8, and the T-9 caveat), `crates/januskey-cli/src/attestation.rs` (HMAC chain, `AuditLog`), `crates/reversible-core/src/content_store.rs` (hashing and dedup). @@ -86,7 +86,7 @@ CLI crate (they were extracted in Phase 1, 2026-03-21). | `crates/januskey-cli/src/attestation.rs` | HMAC-SHA256 audit chain over operations | `crates/januskey-cli/src/keys.rs`, `keys_cli.rs` | AES-256-GCM key store (Argon2id), key lifecycle; the `jk-keys` binary | `crates/reversible-core/src/content_store.rs` | SHA-256 content-addressed storage, deduplication -| `crates/reversible-core/src/metadata.rs` | Append-only operation log (`MetadataStore`); it now calls the shared atomic writer, unbuilt — ledger row T-8 +| `crates/reversible-core/src/metadata.rs` | Append-only operation log (`MetadataStore`); it saves through the shared atomic writer; a failed edit is unapplied and a failed append stays pending (T-8, TESTED); a file change whose record fails to persist is T-9 (OPEN) | `crates/reversible-core/src/transaction.rs` | Transaction lifecycle and the atomic write→fsync→rename log save | `crates/reversible-core/src/manifest.rs` | A2ML manifest emitter (the intended ochrance boundary) | `crates/reversible-core/src/lib.rs` | `ReversibleExecutor` trait — `execute`, `undo`, `generate_manifest` diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 6513abe..9ea6b33 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -190,7 +190,7 @@ attestations undermine trust |Content store integrity |Content-addressed storage never returns wrong content (paths confined to the store and damaged blobs repaired: S-1 and S-2 are TESTED; the write is atomic by construction, not by test; reads verify the hash) |Hash collisions or bugs corrupt stored data -|Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the Rust is tested for partial-rollback retry, T-4, and failed saves, T-5; the premises T-6 and T-7 are assumed; the metadata log, T-8, now saves by rename but that is unverified) +|Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the Rust is tested for partial-rollback retry, T-4, and failed saves, T-5; the premises T-6 and T-7 are assumed; the metadata log is tested for atomic and failed saves, T-8; a file change whose log record fails to persist is OPEN, T-9) |Partial transactions corrupt state |reversible-core |Undo/redo preserves data integrity |Core crate used by @@ -247,6 +247,7 @@ the status table above. |T-5: An add_operation whose save fails is not applied in memory, and the retry records it exactly once on disk |TESTED |`crates/reversible-core/src/transaction.rs::failed_save_leaves_add_operation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_add_operation_unapplied` |T-5: A commit or rollback whose save fails leaves the transaction Active, and the retry settles it |TESTED |`crates/reversible-core/src/transaction.rs::failed_save_leaves_commit_and_rollback_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_commit_and_rollback_unapplied` |T-5: A save replaces the log by rename, leaves no temporary file, and ignores a torn temporary file from an earlier crash |TESTED |`crates/reversible-core/src/transaction.rs::save_replaces_atomically_and_leaves_no_temporary_file` |`cargo test --locked -p reversible-core --lib save_replaces_atomically_and_leaves_no_temporary_file` +|T-5: A transaction-log save replaces the log rather than overwriting it in place (a hard link to the old log keeps the old bytes; a regression to plain `fs::write` fails) |TESTED |`crates/reversible-core/src/transaction.rs::save_replaces_rather_than_overwrites_the_log` |`cargo test --locked -p reversible-core --lib transaction::tests::save_replaces_rather_than_overwrites_the_log` |T-5: Two saves never share a temporary file, and the open refuses one that exists, so a writer cannot truncate, rename or delete another's |TESTED |`crates/reversible-core/src/transaction.rs::each_save_uses_its_own_temporary_file` |`cargo test --locked -p reversible-core --lib each_save_uses_its_own_temporary_file` |T-5: A save keeps the permissions of the log it replaces (rename would otherwise widen a 0640 log to the umask default) |TESTED |`crates/reversible-core/src/transaction.rs::save_preserves_the_logs_permissions` |`cargo test --locked -p reversible-core --lib save_preserves_the_logs_permissions` |T-5: A save whose temporary file already exists (another writer's) fails without deleting that file or writing the log |TESTED |`crates/reversible-core/src/transaction.rs::a_save_never_removes_a_temporary_file_it_did_not_create` |`cargo test --locked -p reversible-core --lib a_save_never_removes_a_temporary_file_it_did_not_create` @@ -289,7 +290,7 @@ be systematically replaced with proven error handling. *HIGH* — reversibility is the product, and its exceptions are destructive: obliteration destroys data on purpose, and the operation log is the only thing -that makes undo possible (row T-8 is open). Any correctness bug in either is a +that makes undo possible (row T-9 is open). Any correctness bug in either is a critical vulnerability. The ABI layer now typechecks, but none of the security obligations above is proved. diff --git a/READINESS.adoc b/READINESS.adoc index d8561e8..ef390ea 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -8,7 +8,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0 === CRG Grade: D (Alpha — Unstable) -*Justification:* 136 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the +*Justification:* 141 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the Idris2 ABI typechecks and 12 proofs are checked (PROVEN ledger rows: ABI, grade, transaction-model and epistemic-model lemmas, not the security obligations); benchmarks exist (5 Criterion groups). But: no fuzz testing, no mutation testing, 241 unwrap() calls, E2E mostly skips, @@ -65,7 +65,7 @@ handling (run by idris-abi.yml, agda-proofs.yml and dashboard-check) |=== -*Total declared:* 136 tests + 5 benchmark groups; 12 proofs checked (PROVEN ledger rows; five of them Grade 3 under mathesis — see `docs/theory/PROOF-GRADES.adoc`) *Total +*Total declared:* 141 tests + 5 benchmark groups; 12 proofs checked (PROVEN ledger rows; five of them Grade 3 under mathesis — see `docs/theory/PROOF-GRADES.adoc`) *Total missing:* Fuzz, mutation, chaos, compatibility === Aspect Matrix diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index 52b61ba..1133cfb 100644 --- a/TOPOLOGY.adoc +++ b/TOPOLOGY.adoc @@ -79,7 +79,7 @@ INTERFACES & RESEARCH MPR Methodology ████░░░░░░ ~40% Design documented; FORMAL PROOFS PENDING (Idris2 ABI typechecks; 12 proofs checked: ABI, grade, transaction-model and epistemic-model lemmas, not the security obligations; MPR not linked to the Rust) - Testing (READINESS matrix) ██████░░░░ ~60% 136 tests + 5 benches; missing fuzz, mutation, + Testing (READINESS matrix) ██████░░░░ ~60% 141 tests + 5 benches; missing fuzz, mutation, chaos, compatibility (Grade D) REPO INFRASTRUCTURE diff --git a/crates/reversible-core/src/metadata.rs b/crates/reversible-core/src/metadata.rs index 600519d..60751f0 100644 --- a/crates/reversible-core/src/metadata.rs +++ b/crates/reversible-core/src/metadata.rs @@ -278,13 +278,31 @@ impl MetadataStore { Ok(Self { path, log }) } - /// Append an operation to the log + /// Append an operation to the log. + /// + /// Unlike the other mutators, an append is applied in memory even when its + /// save fails. The record describes a filesystem change that has already + /// happened, and callers such as `jk delete` carry on with the next file + /// after an error; keeping the record pending means the next successful + /// save persists it, rather than losing the only record that makes that + /// change undoable (T-8; the crash case is T-9). pub fn append(&mut self, metadata: OperationMetadata) -> Result<()> { self.log.operations.push(metadata); - self.save() + Self::save(&self.path, &self.log) + } + + /// Save `next` and, only once it is on disk, make it the in-memory log, so a + /// failed save leaves memory and disk both at the previous log. Used by the + /// mutators that only edit the log (mark_undone, prune, purge); see + /// [`Self::append`] for why an append differs (T-8; the transaction log + /// does the same for T-5). + fn persist(&mut self, next: OperationLog) -> Result<()> { + Self::save(&self.path, &next)?; + self.log = next; + Ok(()) } - /// Save the log to disk. + /// Save `log` to `path`. /// /// Replaces the log using [`crate::transaction::write_atomic`]. Parent /// directory sync is best effort, so success does not guarantee that the @@ -295,12 +313,12 @@ impl MetadataStore { /// Returns errors from creating the parent directory, serialising the log, /// or creating, setting permissions on, writing, syncing or renaming the /// temporary file. - fn save(&self) -> Result<()> { - if let Some(parent) = self.path.parent() { + fn save(path: &Path, log: &OperationLog) -> Result<()> { + if let Some(parent) = path.parent() { fs::create_dir_all(parent)?; } - let content = serde_json::to_string_pretty(&self.log)?; - crate::transaction::write_atomic(&self.path, content.as_bytes())?; + let content = serde_json::to_string_pretty(log)?; + crate::transaction::write_atomic(path, content.as_bytes())?; Ok(()) } @@ -346,12 +364,13 @@ impl MetadataStore { /// Mark operation as undone pub fn mark_undone(&mut self, id: &str, undo_op_id: &str) -> Result<()> { - if let Some(op) = self.get_mut(id) { - op.undone = true; - op.undo_operation_id = Some(undo_op_id.to_string()); - self.save()?; - } - Ok(()) + let mut next = self.log.clone(); + let Some(op) = next.operations.iter_mut().find(|op| op.id == id) else { + return Ok(()); + }; + op.undone = true; + op.undo_operation_id = Some(undo_op_id.to_string()); + self.persist(next) } /// Filter operations by type @@ -406,12 +425,16 @@ impl MetadataStore { pub fn purge_path_entries(&mut self, path: &Path) -> Result> { let matches = |op: &OperationMetadata| op.path == path || op.path_secondary.as_deref() == Some(path); - let (removed, kept): (Vec<_>, Vec<_>) = std::mem::take(&mut self.log.operations) - .into_iter() + let (removed, kept): (Vec<_>, Vec<_>) = self + .log + .operations + .iter() + .cloned() .partition(|op| matches(op)); - self.log.operations = kept; if !removed.is_empty() { - self.save()?; + let mut next = self.log.clone(); + next.operations = kept; + self.persist(next)?; } Ok(removed) } @@ -442,8 +465,9 @@ impl MetadataStore { } let to_remove = original_count - keep; - self.log.operations.drain(0..to_remove); - self.save()?; + let mut next = self.log.clone(); + next.operations.drain(0..to_remove); + self.persist(next)?; Ok(to_remove) } } @@ -566,6 +590,139 @@ mod tests { assert!(store2.get(&id).is_some()); } + /// Replace the log with a non-empty directory so the next save fails at + /// its last step (the rename is refused), for root too. + fn block_log(path: &Path) { + fs::remove_file(path).ok(); + fs::create_dir_all(path).unwrap(); + fs::write(path.join("blocker"), b"x").unwrap(); + } + + /// The in-memory log and the log reloaded from disk, as comparable rows. + fn rows(store: &MetadataStore) -> Vec<(String, bool, Option)> { + store + .operations() + .iter() + .map(|op| (op.id.clone(), op.undone, op.undo_operation_id.clone())) + .collect() + } + + /// T-8: an append whose save fails keeps its record in memory, and the + /// next successful save persists it exactly once. The record describes a + /// filesystem change that already happened (`jk delete` carries on to the + /// next file after an error), so dropping it would leave that change with + /// no record to undo it by. + #[test] + fn a_failed_append_keeps_its_record_for_the_next_save() { + let tmp = TempDir::new().unwrap(); + let path = tmp.path().join("metadata.json"); + let mut store = MetadataStore::new(path.clone()).unwrap(); + store.append(modify_entry("/a.txt", b"a0", b"a1")).unwrap(); + + block_log(&path); + let pending = modify_entry("/b.txt", b"b0", b"b1"); + let pending_id = pending.id.clone(); + assert!(store.append(pending).is_err()); + assert!( + store.get(&pending_id).is_some(), + "the record is kept pending" + ); + fs::remove_dir_all(&path).unwrap(); + + store.append(modify_entry("/c.txt", b"c0", b"c1")).unwrap(); + let disk = MetadataStore::new(path).unwrap(); + assert_eq!(rows(&store), rows(&disk), "memory and disk agree"); + assert_eq!(disk.count(), 3, "the pending record is saved, once"); + assert!(disk.get(&pending_id).is_some()); + } + + /// T-8: a mark_undone, prune or purge whose save fails is not applied in + /// memory; once the fault is cleared each retry applies exactly once, and + /// memory and disk agree. The fault replaces the log with a directory, so + /// this test cannot also show the old log surviving on disk; that half is + /// `transaction::tests::a_failed_save_leaves_the_existing_log_intact`, + /// which fails a save without touching the log. + #[test] + fn failed_save_leaves_every_mutation_unapplied() { + let tmp = TempDir::new().unwrap(); + let path = tmp.path().join("metadata.json"); + let mut store = MetadataStore::new(path.clone()).unwrap(); + let first = modify_entry("/a.txt", b"a0", b"a1"); + let first_id = first.id.clone(); + store.append(first).unwrap(); + store.append(modify_entry("/b.txt", b"b0", b"b1")).unwrap(); + store.append(modify_entry("/c.txt", b"c0", b"c1")).unwrap(); + + block_log(&path); + assert!(store.mark_undone(&first_id, "undo-1").is_err()); + assert!( + !store.get(&first_id).unwrap().undone, + "a failed mark is not applied" + ); + assert!(store.prune(1).is_err()); + assert_eq!(store.count(), 3, "a failed prune removes nothing"); + assert!(store.purge_path_entries(Path::new("/a.txt")).is_err()); + assert!( + store.get(&first_id).is_some(), + "a failed purge removes nothing" + ); + fs::remove_dir_all(&path).unwrap(); + + // Retry each mutator once the fault is cleared: each applies exactly + // once, and after each one memory and the reloaded disk agree. The log + // was removed with the fault, so the first retry rewrites all of it. + let agree = |store: &MetadataStore| { + assert_eq!( + rows(store), + rows(&MetadataStore::new(path.clone()).unwrap()), + "memory and disk agree" + ) + }; + + store.mark_undone(&first_id, "undo-1").unwrap(); + assert!(store.get(&first_id).unwrap().undone); + assert_eq!( + store.get(&first_id).unwrap().undo_operation_id.as_deref(), + Some("undo-1") + ); + agree(&store); + + let purged = store.purge_path_entries(Path::new("/b.txt")).unwrap(); + assert_eq!(purged.len(), 1, "the retried purge removes /b.txt once"); + assert_eq!(store.count(), 2); + agree(&store); + + assert_eq!(store.prune(1).unwrap(), 1, "the retried prune removes one"); + assert_eq!(store.count(), 1); + assert_eq!(store.operations()[0].path, PathBuf::from("/c.txt")); + agree(&store); + } + + /// T-8: a save replaces the log rather than overwriting it in place. A hard + /// link taken before the save still holds the old log afterwards, which a + /// plain `fs::write` (truncate and rewrite the same inode) would not leave, + /// so a regression of `MetadataStore::save` to an in-place write fails here. + #[test] + fn save_replaces_rather_than_overwrites_the_log() { + let tmp = TempDir::new().unwrap(); + let path = tmp.path().join("metadata.json"); + let mut store = MetadataStore::new(path.clone()).unwrap(); + store.append(modify_entry("/a.txt", b"a0", b"a1")).unwrap(); + + let old = tmp.path().join("metadata.json.old"); + fs::hard_link(&path, &old).unwrap(); + let before = fs::read(&old).unwrap(); + + store.append(modify_entry("/b.txt", b"b0", b"b1")).unwrap(); + + assert_eq!( + fs::read(&old).unwrap(), + before, + "the old log was replaced, not rewritten" + ); + assert_ne!(fs::read(&path).unwrap(), before, "the new log is in place"); + } + /// T-8: a save replaces the log by rename, so a reader never sees a torn /// log and no temporary file survives the save. A stale temporary file left /// by an earlier crash is not read and does not stop the next save. diff --git a/crates/reversible-core/src/transaction.rs b/crates/reversible-core/src/transaction.rs index 8a182df..4e9bca2 100644 --- a/crates/reversible-core/src/transaction.rs +++ b/crates/reversible-core/src/transaction.rs @@ -627,6 +627,36 @@ mod tests { } } + /// T-5: a save replaces the transaction log rather than overwriting it in + /// place. A hard link taken before the save still holds the old log + /// afterwards, which a plain `fs::write` (truncate and rewrite the same + /// inode) would not leave, so a regression of the save to an in-place write + /// fails here. + #[test] + fn save_replaces_rather_than_overwrites_the_log() { + let tmp = TempDir::new().expect("failed to create temp dir"); + let path = tmp.path().join("transactions.json"); + let mut manager = TransactionManager::new(path.clone()).expect("new manager"); + manager.begin(None).expect("begin"); + + let old = tmp.path().join("transactions.json.old"); + fs::hard_link(&path, &old).expect("link the current log"); + let before = fs::read(&old).expect("read old"); + + manager.add_operation("op-1".to_string()).expect("op-1"); + + assert_eq!( + fs::read(&old).expect("read old"), + before, + "the old log was replaced, not rewritten" + ); + assert_ne!( + fs::read(&path).expect("read new"), + before, + "the new log is in place" + ); + } + /// T-5: a save replaces the log by rename, leaves no temporary file, and is /// not confused by a torn temporary file left by an earlier crash. #[test] @@ -720,6 +750,29 @@ mod tests { assert!(!path.exists(), "the failed save wrote nothing"); } + /// T-5, T-8: a save that fails before it creates its temporary file leaves + /// the existing log exactly as it was on disk. The failure is injected + /// without touching the log (the temporary name is already taken), so a + /// save that removed or truncated the log before that point is caught here. + /// Not covered: a failure after the temporary file exists (during the write, + /// sync or rename), which would need a fault-injection seam in the writer; + /// the final rename is atomic by the filesystem's guarantee, not by a test. + #[test] + fn a_failed_save_leaves_the_existing_log_intact() { + let dir = TempDir::new().expect("failed to create temp dir"); + let path = dir.path().join("transactions.json"); + fs::write(&path, b"the previous log").expect("existing log"); + let taken = dir.path().join("transactions.json.taken.tmp"); + fs::write(&taken, b"another writer's bytes").expect("plant"); + + assert!(write_atomic_via(&path, &taken, b"the next log").is_err()); + + assert_eq!( + fs::read(&path).expect("the log is still there"), + b"the previous log" + ); + } + /// T-5: the temporary file has the log's permissions the moment it exists, /// before any content is written, so a restricted log is never exposed /// through its copy.