docs(maa): restate RMR two-sided, mark MAA draft expired; defer the undo token (ADR-0003)

.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 = "141 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check"
+total = "5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check"
 
 [proof-grades]
 # Proof Witness Grades, standards 3-practice/PROOF-POLICY.adoc §8 (the

READINESS.adoc

@@ -8,7 +8,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0
 
 === CRG Grade: D (Alpha — Unstable)
 
-*Justification:* 141 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
+*Justification:* 142 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,

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%   141 tests + 5 benches; missing fuzz, mutation,
+  Testing (READINESS matrix)        ██████░░░░  ~60%   142 tests + 5 benches; missing fuzz, mutation,
                                                         chaos, compatibility (Grade D)
 
 REPO INFRASTRUCTURE

crates/januskey-cli/src/operations.rs

@@ -511,6 +511,57 @@ mod tests {
         );
     }
 
+    /// A second undo of the same operation id is refused, in the same process
+    /// and after the log is reloaded from disk, and it leaves the file alone.
+    /// This is the runtime guard that `undo(&str)` has today; it is not a
+    /// typed, use-once undo token (see docs/adr/0003-undo-token-design-note.adoc).
+    #[test]
+    fn second_undo_of_the_same_operation_is_refused() {
+        let (tmp, content_store, mut metadata_store) = setup();
+        let file = tmp.path().join("f.txt");
+        fs::write(&file, "one").unwrap();
+
+        let mut executor = OperationExecutor::new(&content_store, &mut metadata_store);
+        let modify = executor
+            .execute(FileOperation::Modify {
+                path: file.clone(),
+                new_content: b"two".to_vec(),
+            })
+            .unwrap();
+        executor.undo(&modify.id).unwrap();
+        assert_eq!(fs::read(&file).unwrap(), b"one");
+
+        // A later edit that a second undo would clobber.
+        fs::write(&file, "three").unwrap();
+
+        let already_undone = format!("Operation {} already undone", modify.id);
+
+        let mut executor = OperationExecutor::new(&content_store, &mut metadata_store);
+        match executor.undo(&modify.id) {
+            Err(JanusError::OperationFailed(msg)) => assert_eq!(msg, already_undone),
+            other => panic!("expected the already-undone refusal, got {other:?}"),
+        }
+        assert_eq!(fs::read(&file).unwrap(), b"three");
+
+        // The refusal survives a reload: the operation is still in the log and
+        // its undone flag is persisted, so the refusal is the already-undone one
+        // and not an unknown-id error.
+        let mut reloaded = MetadataStore::new(tmp.path().join("metadata.json")).unwrap();
+        assert!(
+            reloaded
+                .get(&modify.id)
+                .expect("operation persisted")
+                .undone,
+            "reloaded operation is marked undone"
+        );
+        let mut executor = OperationExecutor::new(&content_store, &mut reloaded);
+        match executor.undo(&modify.id) {
+            Err(JanusError::OperationFailed(msg)) => assert_eq!(msg, already_undone),
+            other => panic!("expected the already-undone refusal, got {other:?}"),
+        }
+        assert_eq!(fs::read(&file).unwrap(), b"three");
+    }
+
     #[test]
     fn test_modify_and_undo() {
         let (tmp, content_store, mut metadata_store) = setup();

docs/adr/0003-undo-token-design-note.adoc

@@ -0,0 +1,73 @@
+// SPDX-License-Identifier: CC-BY-SA-4.0
+// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+= ADR-0003 — A use-once undo token (design note)
+:toc: left
+
+* *Status:* design note. Not proposed for acceptance, not decided, and nothing is built. §5 lists the questions the owner has to answer first.
+* *Date:* 2026-11-09
+* *Origin:* the ephapax v2 survey (2026-11-04) lists "Linear-token undo API (T-8)" as a januskey action, citing "`undo(&str)` allows double-undo" and sizing it S–M.
+* *Related:* `PROOF-NEEDS.adoc` rows T-1, T-6 and T-8; ADR-0001 (identity and scope).
+
+== 1. The survey item, checked against the tree
+
+* *The label is wrong.* T-8 in this repository's ledger is "the operation metadata log is saved atomically, and an undo whose `mark_undone` fails to persist can be retried". No roadmap, task list or ledger row here describes an undo-token API. This note keeps the survey's request and drops the label.
+* *The premise is partly wrong.* `OperationExecutor::undo(&str)` in `crates/januskey-cli/src/operations.rs` refuses an id whose `undone` flag is set, and `MetadataStore::mark_undone` persists that flag. A second undo of the same id is refused in the same process and after the log is reloaded. The test `operations::tests::second_undo_of_the_same_operation_is_refused` pins this. With the guard disabled the test fails, so it does exercise the guard.
+* *There is a real double-undo window, and it is T-8's second half.* `undo` changes the file first and then calls `mark_undone`. If that save fails, the file is undone but the log still says it is not, and a retry undoes it again. A typed token does not close this window, because the token lives in memory and the hazard is the order of persistence.
+
+== 2. What a token would and would not add
+
+A token would make one narrow thing a compile-time error: using the same token twice. It applies to Rust callers that hold the value `execute_with_token` returned. It does not make the operation undoable only once. `undo(&str)` stays, so a caller can still undo the same operation by its id, before or after using the token, and only the runtime `undone` check refuses the second attempt:
+
+[source,rust]
+----
+#[must_use = "dropping an UndoToken loses the typed undo path; the operation can still be undone by id"]
+pub struct UndoToken { id: String }          // not Clone, not Copy
+
+impl OperationExecutor<'_> {
+    pub fn execute_with_token(&mut self, op: FileOperation)
+        -> Result<(OperationMetadata, UndoToken)>;
+    pub fn undo_token(&mut self, token: UndoToken) -> Result<OperationMetadata>;
+}
+----
+
+Because `undo_token` takes the token by value, a second call with the same token fails to compile. A call to `undo` with the operation id still compiles, whether or not the token was used. A `compile_fail` doctest can pin that without new dependencies. A trybuild test is an alternative, but it adds a dev-dependency.
+
+What it would not add:
+
+* *Linearity.* Rust move semantics are affine: a token can be dropped without being used. `#[must_use]` only warns. "Consumed exactly once" cannot be stated in Rust, so the honest name is "use at most once".
+* *Cross-process safety.* `jk undo <id>` takes the id from the command line, and tokens do not survive a process. The CLI, the transaction rollback in `cmd_rollback` and any persisted log entry would still go through the string path and its runtime `undone` check.
+* *Protection on a failed `mark_undone` save* (§1, third point).
+
+== 3. Options
+
+[cols="1,3,3",options="header"]
+|===
+| Option | What it is | Cost
+
+| A. Leave the API, keep the test
+| The runtime `undone` check plus the new regression test.
+| Nothing new. Callers can still pass a stale id and get an error, not a compile failure.
+
+| B. Add a token API next to `undo(&str)`
+| §2's sketch. It is additive, and the CLI keeps the string path.
+| Two undo entry points. The compile-time guarantee covers reuse of the same token by in-process library callers only. Undo by id stays available for the same operation, and the failed-`mark_undone` window (T-8, OPEN) is untouched.
+
+| C. Put tokens on the `ReversibleExecutor` trait
+| `type Token; fn undo(&mut self, t: Self::Token)`.
+| Breaking. The trait has no implementor in this workspace today, and it is described as the intended mirror of ochrance's `VerifiedSubsystem`, so its shape is a cross-repository decision.
+
+| D. Close T-8's retry half first
+| Persist an "undo in progress" intent before changing the file. Reconciling it on the next start covers a restart only: in the same process, `mark_undone` failing leaves the in-memory log unchanged, so a retry would change the file again and could overwrite a later edit. Every undo attempt, in the same process as well as after a restart, must first reconcile any pending intent on that id. The intent must durably identify the operation, the intended inverse and evidence sufficient to distinguish an unapplied inverse from a fully applied one (including all affected paths, contents and metadata). Reconciliation must exclude concurrent changes while checking that evidence and acting on it. Only a confirmed fully applied inverse permits `mark_undone` without applying the inverse again; clear the intent only after that mark is durable. If the inverse is confirmed unapplied, leave the operation not undone, apply the inverse once under the same protection, verify completion, then persist `mark_undone` before clearing the intent. An intent alone is not evidence of application. If evidence is missing, ambiguous (including indistinguishable before/after states), shows a partial application, or cannot rule out intervening edits, retain the intent and return a recovery-required error without changing files or marking the operation undone. The evidence and exclusion mechanism still need a concrete design; D does not yet establish idempotence.
+| A log-format change and a recovery path. It addresses the real double-undo window that B and C do not.
+|===
+
+== 4. Recommendation
+
+D is the most correct long-term option, because it removes the double-undo that can actually happen. B is cheap and makes reuse of the same token a compile error, but it does not touch that path, and it does not stop a caller undoing the same operation by id. B on its own would let a reader believe double-undo is ruled out when it is not. If B is built, its docs must say that it covers reuse of one token by in-process callers only, that undo by id remains available and is guarded only at run time, and that T-8 remains open.
+
+== 5. Open questions for the owner
+
+. Is the survey's item about library callers (B or C), or about the double-undo window (D)? They are different work.
+. If B or C: is "use at most once" (affine) acceptable, given that Rust cannot express "exactly once"?
+. If C: does ochrance's `VerifiedSubsystem` constrain the trait's undo signature?
+. Should the survey's "(T-8)" reference be corrected upstream in the ephapax report, since T-8 here names a different obligation?

docs/wiki/theory/index.md

@@ -56,9 +56,28 @@ The **Mutually Assured Accountability (MAA) Framework** balances two opposing re
 
 These are implemented through dual primitives:
 
-- **RMR (Reversible Transaction)**: Guarantees perfect state reversal
-
-- **RMO (Obliterative Wipe)**: Guarantees permanent, verifiable data erasure
+<!-- coderabbit-ai-generated:v1 -->
+
+<!-- coderabbit-ai-generated-section:v1:84466b2489f7ee0e9fff9c3f8f42bf678e470d02788b73ed9e79778e5aa9d21c -->
+
+- **RMR (Reversible Transaction)**: Records each change's inverse; undo restores
+  the prior state up to a stated equality. This is tested for single steps when
+  the operation record is saved. If the process stops after a file change but
+  before the record is saved, undo cannot find the operation (T-9, OPEN). For
+  a transaction model it is proved under a premise: every step executed and each
+  step's undo restores the state that step started from (that premise is the
+  single-step property, tested, not proved). The right-inverse direction and
+  "every operation is reversible" are OPEN (see [MAA Property 1](maa-framework.md))
+
+
+<!-- /coderabbit-ai-generated:v1 -->
+- **RMO (Obliterative Wipe)**: Best-effort overwrite and removal. When a
+  JanusKey store exists, each removal is written to an unkeyed JSON ledger; a
+  writer can alter it without detection, and with no store no record is kept.
+  The ledger is written after the bytes are removed, so a failed ledger write
+  can leave a removal unrecorded, and a re-run skips the blob that is already
+  gone without recording it. Unrecoverability is OPEN (E-1) and physical
+  erasure is ASSUMED (X-1)
 
 <!-- -->