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 32ae62f..a9a84c2 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; 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 | V-3 | aletheia consumes `+reversible-core+` | DESIGNED | ARCHITECTURE.adoc §Deferred — Phase 0 research, no operation types yet @@ -129,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 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. @@ -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 @@ -238,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` @@ -249,7 +251,12 @@ 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: 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 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 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` |- |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 +280,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.