From 57e54a1e6b217a0b4b5a4ef685ed52e6f676681e Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 4 Nov 2026 23:54:01 +0000 Subject: [PATCH 1/5] fix(metadata): a failed save leaves the operation log unchanged (T-8); split out T-9 #166 moved MetadataStore::save onto the shared atomic writer, but every mutator still changed the in-memory log before `save()?`, so a failed save left memory and disk disagreeing: the T-5 bug, in the metadata log. append, mark_undone, prune and purge_path_entries now build the next log on a copy, save it, and only then make it the in-memory log. Tests: failed_save_leaves_every_mutation_unapplied fails each mutator's save at its last step and checks memory is unchanged and the retry applies once; a mutant that updates memory before the save fails it. The existing save_replaces_the_log_atomically now runs green, so T-8 moves OPEN -> TESTED. What T-8 also asked, retrying an undo whose mark_undone did not persist, is not a save-ordering problem: every execute and undo changes the filesystem before its record is saved, so a crash or failed save between the two leaves a change the log does not know about. That is now its own row, T-9 (OPEN), and needs a write-ahead intent record, a design decision. Also: the farm directive still claimed propagation through instant-sync.yml, which #156 deleted; it now says propagation is off and why. Dashboards: 136 -> 137 tests. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .../bot_directives/git-private-farm.a2ml | 7 +- EXPLAINME.adoc | 6 +- PROOF-NEEDS.adoc | 11 +- READINESS.adoc | 4 +- TOPOLOGY.adoc | 2 +- crates/reversible-core/src/metadata.rs | 102 ++++++++++++++---- 6 files changed, 100 insertions(+), 32 deletions(-) diff --git a/.machine_readable/bot_directives/git-private-farm.a2ml b/.machine_readable/bot_directives/git-private-farm.a2ml index 2285a06..ac683f4 100644 --- a/.machine_readable/bot_directives/git-private-farm.a2ml +++ b/.machine_readable/bot_directives/git-private-farm.a2ml @@ -3,12 +3,13 @@ [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" diff --git a/EXPLAINME.adoc b/EXPLAINME.adoc index 901f60a..279c7f9 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 and a failed save changes nothing (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 and a failed save changes nothing (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 32ae62f..807088d 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -74,7 +74,8 @@ tables must agree. | T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins) | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked -| T-8 | The operation metadata log is saved atomically, and an undo whose `+mark_undone+` fails to persist can be retried | OPEN | by inspection: the log now takes the same write, sync, rename path as the transaction log (`+crate::transaction::write_atomic+`), and `+metadata::tests::save_replaces_the_log_atomically+` asserts it, but the crate has not been built since that edit, so the row stays OPEN until the test is green in CI. Retry is unchanged: `+undo+` still runs the undo before `+mark_undone+` persists, so a failed persist still leaves the file undone and the log not +| T-8 | The operation metadata log is saved atomically, and a save that fails leaves every mutation (append, mark_undone, prune, purge) unapplied in memory | TESTED | `+metadata::tests::save_replaces_the_log_atomically+` (write, sync, rename through `+crate::transaction::write_atomic+`) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+`; a mutant that updates memory before the save fails the second +| T-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` changes the filesystem and then appends its record, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash or failed save between the two leaves a change the log does not know about (on undo: the file restored but the operation still marked not undone, so the retry tries the inverse again). Save ordering cannot close this; it needs a write-ahead intent record, which is a design decision, not a fix | V-1 | valence-shell depends on `+reversible-core+` for reversible operation data | DESIGNED | ARCHITECTURE.adoc §Consumption status — no repository outside this workspace depends on the crate; Phase 2 is unstarted | V-2 | ochrance verifies januskey A2ML manifests | DESIGNED | `+crates/reversible-core/src/manifest.rs+` — `+ManifestEmitter+` has never been parsed by ochrance; the SHA-256/BLAKE3 boundary mismatch is unresolved | V-3 | aletheia consumes `+reversible-core+` | DESIGNED | ARCHITECTURE.adoc §Deferred — Phase 0 research, no operation types yet @@ -181,7 +182,7 @@ attestations undermine trust |Content store integrity |Content-addressed storage never returns wrong content |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 @@ -249,7 +250,9 @@ the status table above. |E-1: An attacker cannot recover obliterated content or use a revoked key (adversaryCannotKnow holds only by construction of the model) |OPEN |`src/abi/JanusKey/ABI/Types.idr` |- |E-1m: In a world model, an adversary whose observation excludes the store does not know what it holds (adversary-ignorant), obliteration leaves nothing to recover (obliterate-cuts-recovery, obliterate-ignorance), and rotation leaves no agent — the system included — able to use the old key (rotate-forgets-old); the fixtures AdversaryKnows and OldKeyStillUsable are refused |PROVEN |`verification/proofs/agda/Epistemic.agda::adversary-ignorant` |`bash scripts/check-agda.sh` |The six security obligations under "What Needs Proving" (obliteration, key derivation, attestation chain, content store, transaction atomicity, reversible-core) are proved |OPEN |`PROOF-NEEDS.adoc` |- -|T-8: The operation metadata log is saved atomically, and an undo whose `+mark_undone+` fails to persist can be retried (by inspection: `+MetadataStore::save+` calls `+crate::transaction::write_atomic+`, the path `+transaction.rs+` already tests in T-5; `+metadata::tests::save_replaces_the_log_atomically+` covers the log itself and has not been run) |OPEN |`crates/reversible-core/src/metadata.rs` |- +|T-8: The operation metadata log is replaced by write, sync and rename, and leaves no temporary file |TESTED |`crates/reversible-core/src/metadata.rs::save_replaces_the_log_atomically` |`cargo test --locked -p reversible-core --lib save_replaces_the_log_atomically` +|T-8: A metadata save that fails leaves append, mark_undone, prune and purge unapplied in memory, and the retry applies it once |TESTED |`crates/reversible-core/src/metadata.rs::failed_save_leaves_every_mutation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_every_mutation_unapplied` +|T-9: A file operation or undo whose log record fails to persist can be recovered or retried (by inspection: the filesystem changes before the record is saved; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- |T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |- |Every operation is reversible (MPR), as a theorem linked to the Rust (needs G-2 made mechanical, and G-3) |OPEN |`verification/proofs/agda/Reversibility.agda` |- @@ -273,7 +276,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..f8cad14 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:* 137 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:* 137 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..db6a155 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% 137 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..68d90b4 100644 --- a/crates/reversible-core/src/metadata.rs +++ b/crates/reversible-core/src/metadata.rs @@ -280,11 +280,21 @@ impl MetadataStore { /// Append an operation to the log pub fn append(&mut self, metadata: OperationMetadata) -> Result<()> { - self.log.operations.push(metadata); - self.save() + let mut next = self.log.clone(); + next.operations.push(metadata); + self.persist(next) } - /// Save the log to disk. + /// 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 (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 `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 +305,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 +356,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 +417,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 +457,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) } } @@ -569,6 +585,54 @@ mod tests { /// 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. + /// T-8: a mutation whose save fails is not applied in memory, so memory and + /// disk stay at the previous log; once the fault is cleared the retry + /// applies it exactly once. The save is made to fail at its last step (a + /// non-empty directory where the log goes refuses the rename), which works + /// for root too. + #[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(); + + let block = || { + fs::remove_file(&path).ok(); + fs::create_dir_all(&path).unwrap(); + fs::write(path.join("blocker"), b"x").unwrap(); + }; + let unblock = || fs::remove_dir_all(&path).unwrap(); + + block(); + assert!(store.append(modify_entry("/c.txt", b"c0", b"c1")).is_err()); + assert_eq!(store.count(), 2, "a failed append is not recorded"); + 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(), 2, "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" + ); + unblock(); + + store.mark_undone(&first_id, "undo-1").unwrap(); + let reloaded = MetadataStore::new(path).unwrap(); + assert_eq!(reloaded.count(), 2); + assert!( + reloaded.get(&first_id).unwrap().undone, + "memory and disk agree" + ); + } + #[test] fn save_replaces_the_log_atomically() { let tmp = TempDir::new().unwrap(); From 861486897e62084a71bcc62375de7b50fa919b96 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 00:39:00 +0000 Subject: [PATCH 2/5] review: prove the disk side of a failed save; retire dead farm triggers; sync STATE Codex review on #168: - failed_save_leaves_every_mutation_unapplied injects its fault by replacing the log with a directory, so it cannot show the old log surviving on disk. Its doc now says only what it proves (memory unchanged, retry applies once), and the disk side gets its own test at the shared writer: a_failed_save_leaves_the_existing_log_intact fails a save without touching the log and checks the log's bytes are unchanged. A mutant that removes the log before saving fails it. New T-8 ledger row. - git-private-farm.a2ml still advertised triggers and an ungated dispatch step after propagation was retired; they are now marked historical. - STATE.a2ml (the machine-readable source of truth) still said 136 tests and 23 TESTED rows; it and the dashboards now say 138 and 26, measured. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .machine_readable/6a2/STATE.a2ml | 4 ++-- .../bot_directives/git-private-farm.a2ml | 5 +++-- PROOF-NEEDS.adoc | 5 +++-- READINESS.adoc | 4 ++-- TOPOLOGY.adoc | 2 +- crates/reversible-core/src/metadata.rs | 12 ++++++----- crates/reversible-core/src/transaction.rs | 21 +++++++++++++++++++ 7 files changed, 39 insertions(+), 14 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 21d815c..a1ec8a9 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 = "138 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 26 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 ac683f4..179169b 100644 --- a/.machine_readable/bot_directives/git-private-farm.a2ml +++ b/.machine_readable/bot_directives/git-private-farm.a2ml @@ -14,8 +14,9 @@ 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/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 807088d..314400d 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -74,7 +74,7 @@ tables must agree. | T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins) | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked -| T-8 | The operation metadata log is saved atomically, and a save that fails leaves every mutation (append, mark_undone, prune, purge) unapplied in memory | TESTED | `+metadata::tests::save_replaces_the_log_atomically+` (write, sync, rename through `+crate::transaction::write_atomic+`) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+`; a mutant that updates memory before the save fails the second +| T-8 | The operation metadata log is saved atomically, and a save that fails leaves every mutation (append, mark_undone, prune, purge) unapplied in memory | TESTED | `+metadata::tests::save_replaces_the_log_atomically+` (write, sync, rename through `+crate::transaction::write_atomic+`) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a failed save); a mutant that updates memory first, and one that removes the log before saving, each fail a test | T-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` changes the filesystem and then appends its record, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash or failed save between the two leaves a change the log does not know about (on undo: the file restored but the operation still marked not undone, so the retry tries the inverse again). Save ordering cannot close this; it needs a write-ahead intent record, which is a design decision, not a fix | V-1 | valence-shell depends on `+reversible-core+` for reversible operation data | DESIGNED | ARCHITECTURE.adoc §Consumption status — no repository outside this workspace depends on the crate; Phase 2 is unstarted | V-2 | ochrance verifies januskey A2ML manifests | DESIGNED | `+crates/reversible-core/src/manifest.rs+` — `+ManifestEmitter+` has never been parsed by ochrance; the SHA-256/BLAKE3 boundary mismatch is unresolved @@ -130,7 +130,7 @@ one, so the receipt covers these rows as they stand. Mathesis status for them: The other seven PROVEN rows — A-1, A-2, C-1 to C-5 — are Idris2 theorems. Under PROOF-POLICY §1 those are interface and ABI contracts, so the theory ladder does not grade them: they are PROVEN in the vocabulary above and nothing more. The -same holds for the 23 TESTED rows, which record observed behaviour and never +same holds for the 26 TESTED rows, which record observed behaviour and never grading. First-party Rust behaviour belongs to **Creusot** (not SPARK, and not Idris2); no Creusot contract exists in this tree, which is why no Rust row is graded. @@ -252,6 +252,7 @@ the status table above. |The six security obligations under "What Needs Proving" (obliteration, key derivation, attestation chain, content store, transaction atomicity, reversible-core) are proved |OPEN |`PROOF-NEEDS.adoc` |- |T-8: The operation metadata log is replaced by write, sync and rename, and leaves no temporary file |TESTED |`crates/reversible-core/src/metadata.rs::save_replaces_the_log_atomically` |`cargo test --locked -p reversible-core --lib save_replaces_the_log_atomically` |T-8: A metadata save that fails leaves append, mark_undone, prune and purge unapplied in memory, and the retry applies it once |TESTED |`crates/reversible-core/src/metadata.rs::failed_save_leaves_every_mutation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_every_mutation_unapplied` +|T-8: A save that fails leaves the existing log's bytes intact on disk (failure injected without touching the log; shared by the transaction and metadata logs) |TESTED |`crates/reversible-core/src/transaction.rs::a_failed_save_leaves_the_existing_log_intact` |`cargo test --locked -p reversible-core --lib a_failed_save_leaves_the_existing_log_intact` |T-9: A file operation or undo whose log record fails to persist can be recovered or retried (by inspection: the filesystem changes before the record is saved; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- |T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |- diff --git a/READINESS.adoc b/READINESS.adoc index f8cad14..68fb735 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:* 137 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the +*Justification:* 138 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:* 137 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:* 138 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 db6a155..bc18725 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% 137 tests + 5 benches; missing fuzz, mutation, + Testing (READINESS matrix) ██████░░░░ ~60% 138 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 68d90b4..6ab71f6 100644 --- a/crates/reversible-core/src/metadata.rs +++ b/crates/reversible-core/src/metadata.rs @@ -585,11 +585,13 @@ mod tests { /// 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. - /// T-8: a mutation whose save fails is not applied in memory, so memory and - /// disk stay at the previous log; once the fault is cleared the retry - /// applies it exactly once. The save is made to fail at its last step (a - /// non-empty directory where the log goes refuses the rename), which works - /// for root too. + /// T-8: a mutation whose save fails is not applied in memory; once the + /// fault is cleared the retry applies it exactly once, and memory and disk + /// agree. The save is made to fail at its last step by replacing the log + /// with a non-empty directory (which refuses the rename and works for root + /// too), 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(); diff --git a/crates/reversible-core/src/transaction.rs b/crates/reversible-core/src/transaction.rs index 8a182df..c44d45f 100644 --- a/crates/reversible-core/src/transaction.rs +++ b/crates/reversible-core/src/transaction.rs @@ -720,6 +720,27 @@ mod tests { assert!(!path.exists(), "the failed save wrote nothing"); } + /// T-5, T-8: a save that fails leaves the existing log exactly as it was on + /// disk. The failure is injected without touching the log (the save's + /// temporary name is already taken), so a save that removed or truncated the + /// destination before replacing it would be caught here. The final rename + /// itself 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. From 2a610c8adb8bb56356c1fd4559eaac637ebba5b3 Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 00:47:41 +0000 Subject: [PATCH 3/5] review: show rename-not-overwrite for both logs; retry every mutator Codex review of 8614868 on #168: - save_replaces_the_log_atomically could not tell a rename from a plain fs::write, so it did not back the "replaced atomically" claim (and the transaction log's equivalent test had the same gap once temporary names became random). New save_replaces_rather_than_overwrites_the_log tests, one per log, take a hard link to the log before a save and check it still holds the old bytes, which an in-place write would not leave. Mutants with an in-place metadata save and an in-place shared writer each fail them. The old test's ledger row now claims only what it shows (no temporary file left, a stale one ignored). - failed_save_leaves_every_mutation_unapplied retried only mark_undone. It now retries append, mark_undone, purge and prune, checking each applies once and that memory and the reloaded log agree after each; a mutant whose persist never updates memory fails it. Ledger: one new T-5 row and one new T-8 row. Dashboards and STATE: 140 tests, 28 TESTED rows, measured. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .machine_readable/6a2/STATE.a2ml | 4 +- PROOF-NEEDS.adoc | 10 ++-- READINESS.adoc | 4 +- TOPOLOGY.adoc | 2 +- crates/reversible-core/src/metadata.rs | 58 +++++++++++++++++++++-- crates/reversible-core/src/transaction.rs | 30 ++++++++++++ 6 files changed, 94 insertions(+), 14 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index a1ec8a9..f545301 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 = "138 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check" +total = "140 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 26 TESTED rows (observed behaviour); ASSUMED/DESIGNED/OPEN rows" +not-graded = "the 7 Idris2 PROVEN rows (ABI/interface contracts, PROOF-POLICY §1); all 28 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/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 314400d..76eb4a8 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -74,7 +74,7 @@ tables must agree. | T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins) | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked -| T-8 | The operation metadata log is saved atomically, and a save that fails leaves every mutation (append, mark_undone, prune, purge) unapplied in memory | TESTED | `+metadata::tests::save_replaces_the_log_atomically+` (write, sync, rename through `+crate::transaction::write_atomic+`) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a failed save); a mutant that updates memory first, and one that removes the log before saving, each fail a test +| T-8 | The operation metadata log is saved atomically, and a save that fails leaves every mutation (append, mark_undone, prune, purge) unapplied in memory | TESTED | `+metadata::tests::save_replaces_rather_than_overwrites_the_log+` (rename, not an in-place write, through `+crate::transaction::write_atomic+`; a plain `+fs::write+` mutant fails it) and `+save_replaces_the_log_atomically+` (no temporary file left) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a failed save); a mutant that updates memory first, and one that removes the log before saving, each fail a test | T-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` changes the filesystem and then appends its record, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash or failed save between the two leaves a change the log does not know about (on undo: the file restored but the operation still marked not undone, so the retry tries the inverse again). Save ordering cannot close this; it needs a write-ahead intent record, which is a design decision, not a fix | V-1 | valence-shell depends on `+reversible-core+` for reversible operation data | DESIGNED | ARCHITECTURE.adoc §Consumption status — no repository outside this workspace depends on the crate; Phase 2 is unstarted | V-2 | ochrance verifies januskey A2ML manifests | DESIGNED | `+crates/reversible-core/src/manifest.rs+` — `+ManifestEmitter+` has never been parsed by ochrance; the SHA-256/BLAKE3 boundary mismatch is unresolved @@ -130,7 +130,7 @@ one, so the receipt covers these rows as they stand. Mathesis status for them: The other seven PROVEN rows — A-1, A-2, C-1 to C-5 — are Idris2 theorems. Under PROOF-POLICY §1 those are interface and ABI contracts, so the theory ladder does not grade them: they are PROVEN in the vocabulary above and nothing more. The -same holds for the 26 TESTED rows, which record observed behaviour and never +same holds for the 28 TESTED rows, which record observed behaviour and never grading. First-party Rust behaviour belongs to **Creusot** (not SPARK, and not Idris2); no Creusot contract exists in this tree, which is why no Rust row is graded. @@ -239,6 +239,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` @@ -250,8 +251,9 @@ the status table above. |E-1: An attacker cannot recover obliterated content or use a revoked key (adversaryCannotKnow holds only by construction of the model) |OPEN |`src/abi/JanusKey/ABI/Types.idr` |- |E-1m: In a world model, an adversary whose observation excludes the store does not know what it holds (adversary-ignorant), obliteration leaves nothing to recover (obliterate-cuts-recovery, obliterate-ignorance), and rotation leaves no agent — the system included — able to use the old key (rotate-forgets-old); the fixtures AdversaryKnows and OldKeyStillUsable are refused |PROVEN |`verification/proofs/agda/Epistemic.agda::adversary-ignorant` |`bash scripts/check-agda.sh` |The six security obligations under "What Needs Proving" (obliteration, key derivation, attestation chain, content store, transaction atomicity, reversible-core) are proved |OPEN |`PROOF-NEEDS.adoc` |- -|T-8: The operation metadata log is replaced by write, sync and rename, and leaves no temporary file |TESTED |`crates/reversible-core/src/metadata.rs::save_replaces_the_log_atomically` |`cargo test --locked -p reversible-core --lib save_replaces_the_log_atomically` -|T-8: A metadata save that fails leaves append, mark_undone, prune and purge unapplied in memory, and the retry applies it once |TESTED |`crates/reversible-core/src/metadata.rs::failed_save_leaves_every_mutation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_every_mutation_unapplied` +|T-8: A metadata save leaves no temporary file behind and ignores a stale one from an earlier crash |TESTED |`crates/reversible-core/src/metadata.rs::save_replaces_the_log_atomically` |`cargo test --locked -p reversible-core --lib save_replaces_the_log_atomically` +|T-8: A metadata 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/metadata.rs::save_replaces_rather_than_overwrites_the_log` |`cargo test --locked -p reversible-core --lib metadata::tests::save_replaces_rather_than_overwrites_the_log` +|T-8: A metadata save that fails leaves append, mark_undone, prune and purge unapplied in memory, and each retried mutator then applies once with memory and the reloaded log agreeing |TESTED |`crates/reversible-core/src/metadata.rs::failed_save_leaves_every_mutation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_every_mutation_unapplied` |T-8: A save that fails leaves the existing log's bytes intact on disk (failure injected without touching the log; shared by the transaction and metadata logs) |TESTED |`crates/reversible-core/src/transaction.rs::a_failed_save_leaves_the_existing_log_intact` |`cargo test --locked -p reversible-core --lib a_failed_save_leaves_the_existing_log_intact` |T-9: A file operation or undo whose log record fails to persist can be recovered or retried (by inspection: the filesystem changes before the record is saved; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- diff --git a/READINESS.adoc b/READINESS.adoc index 68fb735..d9782c8 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:* 138 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the +*Justification:* 140 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:* 138 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:* 140 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 bc18725..8983647 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% 138 tests + 5 benches; missing fuzz, mutation, + Testing (READINESS matrix) ██████░░░░ ~60% 140 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 6ab71f6..eeeeb68 100644 --- a/crates/reversible-core/src/metadata.rs +++ b/crates/reversible-core/src/metadata.rs @@ -626,13 +626,61 @@ mod tests { ); unblock(); + // Retry every mutator once the fault is cleared: each applies exactly + // once, and after each one memory and the reloaded disk agree. + let agree = |store: &MetadataStore| { + let disk = MetadataStore::new(path.clone()).unwrap(); + let view = |s: &MetadataStore| -> Vec<(String, bool)> { + s.operations() + .iter() + .map(|op| (op.id.clone(), op.undone)) + .collect() + }; + assert_eq!(view(store), view(&disk), "memory and disk agree"); + }; + + store.append(modify_entry("/c.txt", b"c0", b"c1")).unwrap(); + assert_eq!(store.count(), 3, "the retried append is recorded once"); + agree(&store); + store.mark_undone(&first_id, "undo-1").unwrap(); - let reloaded = MetadataStore::new(path).unwrap(); - assert_eq!(reloaded.count(), 2); - assert!( - reloaded.get(&first_id).unwrap().undone, - "memory and disk agree" + assert!(store.get(&first_id).unwrap().undone); + 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"); } #[test] diff --git a/crates/reversible-core/src/transaction.rs b/crates/reversible-core/src/transaction.rs index c44d45f..e6f3aae 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] From eb604297b9a9e2f3c56c4bfba7b57c8af6e2d0df Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 00:57:44 +0000 Subject: [PATCH 4/5] fix(metadata): keep a failed append's record pending, not dropped CodeRabbit review on #168 (Major, verified): making `append` copy-on-write dropped the record from memory when its save failed. `jk delete` carries on to the next file after an error, so the next successful save then omitted the record of a deletion that had already happened, leaving it with nothing to undo it by. The previous code kept it and saved it on the next success. An append records a filesystem change that has already happened, so it is now applied in memory even when its save fails and is persisted by the next successful save. The edits that only change the log (mark_undone, prune, purge) stay copy-on-write: a failed save leaves them unapplied. Tests: a_failed_append_keeps_its_record_for_the_next_save (fails against the copy-on-write append that was flagged); failed_save_leaves_every_mutation_ unapplied now covers the three edits and also checks undo_operation_id (CodeRabbit nit), failing against mutants that update memory first or drop the undo id. A misplaced doc comment is back on save_replaces_the_log_ atomically. Ledger and docs now say what a failed save does for each mutator. Dashboards and STATE: 141 tests, 29 TESTED rows. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .machine_readable/6a2/STATE.a2ml | 4 +- EXPLAINME.adoc | 4 +- PROOF-NEEDS.adoc | 7 +- READINESS.adoc | 4 +- TOPOLOGY.adoc | 2 +- crates/reversible-core/src/metadata.rs | 125 +++++++++++++++++-------- 6 files changed, 95 insertions(+), 51 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index f545301..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 = "140 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 28 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/EXPLAINME.adoc b/EXPLAINME.adoc index 279c7f9..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 saves by rename and a failed save changes nothing (T-8, TESTED), but a file change whose log record fails to persist is not recoverable (T-9, 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. @@ -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 saves through the shared atomic writer and a failed save changes nothing (T-8, TESTED); a file change whose record fails to persist is T-9 (OPEN) +| `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 76eb4a8..a2aef8d 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -74,7 +74,7 @@ tables must agree. | T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins) | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked -| T-8 | The operation metadata log is saved atomically, and a save that fails leaves every mutation (append, mark_undone, prune, purge) unapplied in memory | TESTED | `+metadata::tests::save_replaces_rather_than_overwrites_the_log+` (rename, not an in-place write, through `+crate::transaction::write_atomic+`; a plain `+fs::write+` mutant fails it) and `+save_replaces_the_log_atomically+` (no temporary file left) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a failed save); a mutant that updates memory first, and one that removes the log before saving, each fail a test +| T-8 | The operation metadata log is saved atomically; a save that fails leaves mark_undone, prune and purge unapplied in memory, and keeps an append pending for the next save (its file change already happened) | TESTED | `+metadata::tests::save_replaces_rather_than_overwrites_the_log+` (rename, not an in-place write, through `+crate::transaction::write_atomic+`; a plain `+fs::write+` mutant fails it) and `+save_replaces_the_log_atomically+` (no temporary file left) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` and `+a_failed_append_keeps_its_record_for_the_next_save+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a failed save); a mutant that updates memory first, and one that removes the log before saving, each fail a test | T-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` changes the filesystem and then appends its record, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash or failed save between the two leaves a change the log does not know about (on undo: the file restored but the operation still marked not undone, so the retry tries the inverse again). Save ordering cannot close this; it needs a write-ahead intent record, which is a design decision, not a fix | V-1 | valence-shell depends on `+reversible-core+` for reversible operation data | DESIGNED | ARCHITECTURE.adoc §Consumption status — no repository outside this workspace depends on the crate; Phase 2 is unstarted | V-2 | ochrance verifies januskey A2ML manifests | DESIGNED | `+crates/reversible-core/src/manifest.rs+` — `+ManifestEmitter+` has never been parsed by ochrance; the SHA-256/BLAKE3 boundary mismatch is unresolved @@ -130,7 +130,7 @@ one, so the receipt covers these rows as they stand. Mathesis status for them: The other seven PROVEN rows — A-1, A-2, C-1 to C-5 — are Idris2 theorems. Under PROOF-POLICY §1 those are interface and ABI contracts, so the theory ladder does not grade them: they are PROVEN in the vocabulary above and nothing more. The -same holds for the 28 TESTED rows, which record observed behaviour and never +same holds for the 29 TESTED rows, which record observed behaviour and never grading. First-party Rust behaviour belongs to **Creusot** (not SPARK, and not Idris2); no Creusot contract exists in this tree, which is why no Rust row is graded. @@ -253,7 +253,8 @@ the status table above. |The six security obligations under "What Needs Proving" (obliteration, key derivation, attestation chain, content store, transaction atomicity, reversible-core) are proved |OPEN |`PROOF-NEEDS.adoc` |- |T-8: A metadata save leaves no temporary file behind and ignores a stale one from an earlier crash |TESTED |`crates/reversible-core/src/metadata.rs::save_replaces_the_log_atomically` |`cargo test --locked -p reversible-core --lib save_replaces_the_log_atomically` |T-8: A metadata 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/metadata.rs::save_replaces_rather_than_overwrites_the_log` |`cargo test --locked -p reversible-core --lib metadata::tests::save_replaces_rather_than_overwrites_the_log` -|T-8: A metadata save that fails leaves append, mark_undone, prune and purge unapplied in memory, and each retried mutator then applies once with memory and the reloaded log agreeing |TESTED |`crates/reversible-core/src/metadata.rs::failed_save_leaves_every_mutation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_every_mutation_unapplied` +|T-8: A metadata save that fails leaves mark_undone, prune and purge unapplied in memory, and each retried mutator then applies once with memory and the reloaded log agreeing |TESTED |`crates/reversible-core/src/metadata.rs::failed_save_leaves_every_mutation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_every_mutation_unapplied` +|T-8: An append whose save fails keeps its record pending, and the next successful save persists it once (so `jk delete` continuing after one failed record does not lose it) |TESTED |`crates/reversible-core/src/metadata.rs::a_failed_append_keeps_its_record_for_the_next_save` |`cargo test --locked -p reversible-core --lib a_failed_append_keeps_its_record_for_the_next_save` |T-8: A save that fails leaves the existing log's bytes intact on disk (failure injected without touching the log; shared by the transaction and metadata logs) |TESTED |`crates/reversible-core/src/transaction.rs::a_failed_save_leaves_the_existing_log_intact` |`cargo test --locked -p reversible-core --lib a_failed_save_leaves_the_existing_log_intact` |T-9: A file operation or undo whose log record fails to persist can be recovered or retried (by inspection: the filesystem changes before the record is saved; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- diff --git a/READINESS.adoc b/READINESS.adoc index d9782c8..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:* 140 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:* 140 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 8983647..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% 140 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 eeeeb68..60751f0 100644 --- a/crates/reversible-core/src/metadata.rs +++ b/crates/reversible-core/src/metadata.rs @@ -278,16 +278,24 @@ 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<()> { - let mut next = self.log.clone(); - next.operations.push(metadata); - self.persist(next) + self.log.operations.push(metadata); + 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 (T-8; the - /// transaction log does the same for T-5). + /// 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; @@ -582,15 +590,57 @@ mod tests { assert!(store2.get(&id).is_some()); } - /// 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. - /// T-8: a mutation whose save fails is not applied in memory; once the - /// fault is cleared the retry applies it exactly once, and memory and disk - /// agree. The save is made to fail at its last step by replacing the log - /// with a non-empty directory (which refuses the rename and works for root - /// too), 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`, + /// 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() { @@ -601,50 +651,40 @@ mod tests { 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(); - let block = || { - fs::remove_file(&path).ok(); - fs::create_dir_all(&path).unwrap(); - fs::write(path.join("blocker"), b"x").unwrap(); - }; - let unblock = || fs::remove_dir_all(&path).unwrap(); - - block(); - assert!(store.append(modify_entry("/c.txt", b"c0", b"c1")).is_err()); - assert_eq!(store.count(), 2, "a failed append is not recorded"); + 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(), 2, "a failed prune removes nothing"); + 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" ); - unblock(); + fs::remove_dir_all(&path).unwrap(); - // Retry every mutator once the fault is cleared: each applies exactly - // once, and after each one memory and the reloaded disk agree. + // 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| { - let disk = MetadataStore::new(path.clone()).unwrap(); - let view = |s: &MetadataStore| -> Vec<(String, bool)> { - s.operations() - .iter() - .map(|op| (op.id.clone(), op.undone)) - .collect() - }; - assert_eq!(view(store), view(&disk), "memory and disk agree"); + assert_eq!( + rows(store), + rows(&MetadataStore::new(path.clone()).unwrap()), + "memory and disk agree" + ) }; - store.append(modify_entry("/c.txt", b"c0", b"c1")).unwrap(); - assert_eq!(store.count(), 3, "the retried append is recorded once"); - agree(&store); - 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(); @@ -683,6 +723,9 @@ mod tests { 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. #[test] fn save_replaces_the_log_atomically() { let tmp = TempDir::new().unwrap(); From c500ad30b5727030c53dc4137dac3bda8cea79db Mon Sep 17 00:00:00 2001 From: Claude Date: Thu, 5 Nov 2026 01:22:22 +0000 Subject: [PATCH 5/5] docs(tests): narrow the failed-save disk claim to what the test shows CodeRabbit (review of 2a610c8): a_failed_save_leaves_the_existing_log_intact injects its failure before the temporary file is created, so it catches a save that removes or truncates the log before that point, not one that does so later and then fails during the write, sync or rename. Its doc comment and the T-8 ledger rows claimed the broader property; they now say exactly what is covered and what is not (that case needs a fault-injection seam in the writer). No code change. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- PROOF-NEEDS.adoc | 4 ++-- crates/reversible-core/src/transaction.rs | 12 +++++++----- 2 files changed, 9 insertions(+), 7 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index a2aef8d..a9a84c2 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -74,7 +74,7 @@ tables must agree. | T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins) | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked -| T-8 | The operation metadata log is saved atomically; a save that fails leaves mark_undone, prune and purge unapplied in memory, and keeps an append pending for the next save (its file change already happened) | TESTED | `+metadata::tests::save_replaces_rather_than_overwrites_the_log+` (rename, not an in-place write, through `+crate::transaction::write_atomic+`; a plain `+fs::write+` mutant fails it) and `+save_replaces_the_log_atomically+` (no temporary file left) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` and `+a_failed_append_keeps_its_record_for_the_next_save+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a failed save); a mutant that updates memory first, and one that removes the log before saving, each fail a test +| T-8 | The operation metadata log is saved atomically; a save that fails leaves mark_undone, prune and purge unapplied in memory, and keeps an append pending for the next save (its file change already happened) | TESTED | `+metadata::tests::save_replaces_rather_than_overwrites_the_log+` (rename, not an in-place write, through `+crate::transaction::write_atomic+`; a plain `+fs::write+` mutant fails it) and `+save_replaces_the_log_atomically+` (no temporary file left) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` and `+a_failed_append_keeps_its_record_for_the_next_save+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a save that fails before its temporary file exists); a mutant that updates memory first, and one that removes the log before saving, each fail a test | T-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` changes the filesystem and then appends its record, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash or failed save between the two leaves a change the log does not know about (on undo: the file restored but the operation still marked not undone, so the retry tries the inverse again). Save ordering cannot close this; it needs a write-ahead intent record, which is a design decision, not a fix | V-1 | valence-shell depends on `+reversible-core+` for reversible operation data | DESIGNED | ARCHITECTURE.adoc §Consumption status — no repository outside this workspace depends on the crate; Phase 2 is unstarted | V-2 | ochrance verifies januskey A2ML manifests | DESIGNED | `+crates/reversible-core/src/manifest.rs+` — `+ManifestEmitter+` has never been parsed by ochrance; the SHA-256/BLAKE3 boundary mismatch is unresolved @@ -255,7 +255,7 @@ the status table above. |T-8: A metadata 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/metadata.rs::save_replaces_rather_than_overwrites_the_log` |`cargo test --locked -p reversible-core --lib metadata::tests::save_replaces_rather_than_overwrites_the_log` |T-8: A metadata save that fails leaves mark_undone, prune and purge unapplied in memory, and each retried mutator then applies once with memory and the reloaded log agreeing |TESTED |`crates/reversible-core/src/metadata.rs::failed_save_leaves_every_mutation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_every_mutation_unapplied` |T-8: An append whose save fails keeps its record pending, and the next successful save persists it once (so `jk delete` continuing after one failed record does not lose it) |TESTED |`crates/reversible-core/src/metadata.rs::a_failed_append_keeps_its_record_for_the_next_save` |`cargo test --locked -p reversible-core --lib a_failed_append_keeps_its_record_for_the_next_save` -|T-8: A save that fails leaves the existing log's bytes intact on disk (failure injected without touching the log; shared by the transaction and metadata logs) |TESTED |`crates/reversible-core/src/transaction.rs::a_failed_save_leaves_the_existing_log_intact` |`cargo test --locked -p reversible-core --lib a_failed_save_leaves_the_existing_log_intact` +|T-8: A save that fails before creating its temporary file leaves the existing log's bytes intact on disk (failure injected without touching the log; shared by the transaction and metadata logs; a failure after the temporary file exists is not covered) |TESTED |`crates/reversible-core/src/transaction.rs::a_failed_save_leaves_the_existing_log_intact` |`cargo test --locked -p reversible-core --lib a_failed_save_leaves_the_existing_log_intact` |T-9: A file operation or undo whose log record fails to persist can be recovered or retried (by inspection: the filesystem changes before the record is saved; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- |T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |- diff --git a/crates/reversible-core/src/transaction.rs b/crates/reversible-core/src/transaction.rs index e6f3aae..4e9bca2 100644 --- a/crates/reversible-core/src/transaction.rs +++ b/crates/reversible-core/src/transaction.rs @@ -750,11 +750,13 @@ mod tests { assert!(!path.exists(), "the failed save wrote nothing"); } - /// T-5, T-8: a save that fails leaves the existing log exactly as it was on - /// disk. The failure is injected without touching the log (the save's - /// temporary name is already taken), so a save that removed or truncated the - /// destination before replacing it would be caught here. The final rename - /// itself is atomic by the filesystem's guarantee, not by a test. + /// 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");