fix(metadata): a failed save leaves the operation log unchanged (T-8); split out T-9

.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"
 

.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"]

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`

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.
 

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

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