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

@@ -190,7 +190,7 @@ attestations undermine trust
 |Content store integrity |Content-addressed storage never returns wrong
 content (paths confined to the store and damaged blobs repaired: S-1 and S-2 are TESTED; the write is atomic by construction, not by test; reads verify the hash) |Hash collisions or bugs corrupt stored data
 
-|Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the Rust is tested for partial-rollback retry, T-4, and failed saves, T-5; the premises T-6 and T-7 are assumed; the metadata log, T-8, now saves by rename but that is unverified)
+|Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the Rust is tested for partial-rollback retry, T-4, and failed saves, T-5; the premises T-6 and T-7 are assumed; the metadata log is tested for atomic and failed saves, T-8; a file change whose log record fails to persist is OPEN, T-9)
 |Partial transactions corrupt state
 
 |reversible-core |Undo/redo preserves data integrity |Core crate used by
@@ -247,6 +247,7 @@ the status table above.
 |T-5: An add_operation whose save fails is not applied in memory, and the retry records it exactly once on disk |TESTED |`crates/reversible-core/src/transaction.rs::failed_save_leaves_add_operation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_add_operation_unapplied`
 |T-5: A commit or rollback whose save fails leaves the transaction Active, and the retry settles it |TESTED |`crates/reversible-core/src/transaction.rs::failed_save_leaves_commit_and_rollback_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_commit_and_rollback_unapplied`
 |T-5: A save replaces the log by rename, leaves no temporary file, and ignores a torn temporary file from an earlier crash |TESTED |`crates/reversible-core/src/transaction.rs::save_replaces_atomically_and_leaves_no_temporary_file` |`cargo test --locked -p reversible-core --lib save_replaces_atomically_and_leaves_no_temporary_file`
+|T-5: A transaction-log save replaces the log rather than overwriting it in place (a hard link to the old log keeps the old bytes; a regression to plain `fs::write` fails) |TESTED |`crates/reversible-core/src/transaction.rs::save_replaces_rather_than_overwrites_the_log` |`cargo test --locked -p reversible-core --lib transaction::tests::save_replaces_rather_than_overwrites_the_log`
 |T-5: Two saves never share a temporary file, and the open refuses one that exists, so a writer cannot truncate, rename or delete another's |TESTED |`crates/reversible-core/src/transaction.rs::each_save_uses_its_own_temporary_file` |`cargo test --locked -p reversible-core --lib each_save_uses_its_own_temporary_file`
 |T-5: A save keeps the permissions of the log it replaces (rename would otherwise widen a 0640 log to the umask default) |TESTED |`crates/reversible-core/src/transaction.rs::save_preserves_the_logs_permissions` |`cargo test --locked -p reversible-core --lib save_preserves_the_logs_permissions`
 |T-5: A save whose temporary file already exists (another writer's) fails without deleting that file or writing the log |TESTED |`crates/reversible-core/src/transaction.rs::a_save_never_removes_a_temporary_file_it_did_not_create` |`cargo test --locked -p reversible-core --lib a_save_never_removes_a_temporary_file_it_did_not_create`
@@ -289,7 +290,7 @@ be systematically replaced with proven error handling.
 
 *HIGH* — reversibility is the product, and its exceptions are destructive:
 obliteration destroys data on purpose, and the operation log is the only thing
-that makes undo possible (row T-8 is open). Any correctness bug in either is a
+that makes undo possible (row T-9 is open). Any correctness bug in either is a
 critical vulnerability. The ABI layer now typechecks, but none of the security
 obligations above is proved.
 

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