From c2f676a7350d22f4dd18dc81c6be4ce4ea79dd8c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:06:30 +0000 Subject: [PATCH 1/5] docs(maa): restate RMR two-sided, mark the MAA draft expired, defer the undo token MAA draft (draft-hyperpolymath-maa-framework-00.txt): - Mark it EXPIRED (dated 2025-10-13, expired 2026-04-13), not renewed, with no record of submission or ratification; corrected in place, original in git history (2361441), revision note appended. - Restate RMR as RMR-L / RMR-R (left and right inverse on the image), each relative to a named equality on states (~tree, ~model), with the ledger status of each part (RMR-R has no row: OPEN). - Remove the attributions of enforcement to Oblibeny and of verification to Isabelle/HOL and Z3: the repository contains none of them. - RMO now carries E-1 OPEN and X-1 ASSUMED instead of "proving non-existence". Wiki: maa-framework.md Formal Properties restated the same way and "formally verified primitives" / "RMO planned" corrected; theory/index.md RMR/RMO "guarantees" corrected; rmr-primitive.md points to the two-sided statement. Undo token: the survey's "T-8" is a different ledger row (atomic metadata log), and in-process and reloaded double undo is already refused at runtime. Add a regression test pinning that refusal (fails with the guard disabled) and ADR-0003, a design note deferring the typed token with its open questions. Test count 141 -> 142 in READINESS and TOPOLOGY; the now-false "141 tests" is deleted from STATE.a2ml's total. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- .machine_readable/6a2/STATE.a2ml | 2 +- READINESS.adoc | 4 +- TOPOLOGY.adoc | 2 +- crates/januskey-cli/src/operations.rs | 34 ++++ docs/adr/0003-undo-token-design-note.adoc | 73 ++++++++ docs/wiki/theory/index.md | 11 +- docs/wiki/theory/maa-framework.md | 51 ++++-- docs/wiki/theory/rmr-primitive.md | 5 +- draft-hyperpolymath-maa-framework-00.txt | 200 ++++++++++++++++------ 9 files changed, 313 insertions(+), 69 deletions(-) create mode 100644 docs/adr/0003-undo-token-design-note.adoc diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index d68c5af..6ed8c7a 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 = "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] # mathesis (estate-mathematical-architecture §5/§6) + standards diff --git a/READINESS.adoc b/READINESS.adoc index ef390ea..1463471 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:* 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, @@ -65,7 +65,7 @@ handling (run by idris-abi.yml, agda-proofs.yml and dashboard-check) |=== -*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 +*Total declared:* 142 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 1133cfb..a836445 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% 141 tests + 5 benches; missing fuzz, mutation, + Testing (READINESS matrix) ██████░░░░ ~60% 142 tests + 5 benches; missing fuzz, mutation, chaos, compatibility (Grade D) REPO INFRASTRUCTURE diff --git a/crates/januskey-cli/src/operations.rs b/crates/januskey-cli/src/operations.rs index 29803fe..b0b8124 100644 --- a/crates/januskey-cli/src/operations.rs +++ b/crates/januskey-cli/src/operations.rs @@ -511,6 +511,40 @@ 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 mut executor = OperationExecutor::new(&content_store, &mut metadata_store); + assert!(executor.undo(&modify.id).is_err()); + assert_eq!(fs::read(&file).unwrap(), b"three"); + + // The refusal survives a reload: the undone flag is persisted. + let mut reloaded = MetadataStore::new(tmp.path().join("metadata.json")).unwrap(); + let mut executor = OperationExecutor::new(&content_store, &mut reloaded); + assert!(executor.undo(&modify.id).is_err()); + assert_eq!(fs::read(&file).unwrap(), b"three"); + } + #[test] fn test_modify_and_undo() { let (tmp, content_store, mut metadata_store) = setup(); diff --git a/docs/adr/0003-undo-token-design-note.adoc b/docs/adr/0003-undo-token-design-note.adoc new file mode 100644 index 0000000..6fb59b5 --- /dev/null +++ b/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 += 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 turn "undo this operation at most once" from a runtime check into a compile-time one, for Rust callers that hold the value `execute` returned: + +[source,rust] +---- +#[must_use = "an UndoToken is the only way to undo this operation"] +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; +} +---- + +Because `undo_token` takes the token by value, a second call with the same token fails to compile. 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 ` 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 guarantee covers in-process library callers only. + +| 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, then reconcile it on the next start. This makes a retried undo idempotent. +| 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 library misuse visible at compile time, but it does not touch that path. 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 in-process callers only 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? diff --git a/docs/wiki/theory/index.md b/docs/wiki/theory/index.md index 464c228..8bb234a 100644 --- a/docs/wiki/theory/index.md +++ b/docs/wiki/theory/index.md @@ -56,9 +56,14 @@ 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 +- **RMR (Reversible Transaction)**: Records each change's inverse; undo restores + the prior state up to a stated equality, tested for single steps and proved + for a transaction model; the right-inverse direction and "every operation is + reversible" are OPEN (see [MAA Property 1](maa-framework.md)) + +- **RMO (Obliterative Wipe)**: Best-effort overwrite and removal with a + tamper-evident record; unrecoverability is OPEN (E-1) and physical erasure is + ASSUMED (X-1) diff --git a/docs/wiki/theory/maa-framework.md b/docs/wiki/theory/maa-framework.md index d0b2332..fa4effc 100644 --- a/docs/wiki/theory/maa-framework.md +++ b/docs/wiki/theory/maa-framework.md @@ -66,7 +66,8 @@ This pushes toward: *complete, verifiable deletion capability*. ## The MAA Solution -MAA introduces two formally verified primitives that satisfy both requirements: +MAA proposes two primitives, one for each requirement. Neither is formally +verified in full; the status of each part is stated below and in the ledger. ### RMR (Reversible Transaction) @@ -141,21 +142,48 @@ The key insight of MAA is that RMR and RMO are not alternatives—they are compl ## Formal Properties -### Property 1: Complete Reversibility (RMR) +These are target properties. Each is stated with its status in the claims ledger +(`PROOF-NEEDS.adoc`), and none is a theorem about the Rust as a whole. -For any sequence of operations $O_1, O_2, \ldots, O_n$: +### Property 1: Reversibility (RMR), two-sided and relative to an equality -$$O_n^{-1}(O_{n-1}^{-1}(\ldots O_1^{-1}(O_1(O_2(\ldots O_n(S)))))) = S$$ +A reversibility claim is an equality *up to* an equivalence $\sim$ on states, and +says nothing about any finer equality. Two are in use: -The system can always return to any previous state. +- $\sim_{tree}$: same relative paths and same bytes for the regular files under + the working tree. Permissions, owner/group, mtime, symlink identity, inode + identity and empty directories are not compared. This is what + `property_tests::execute_then_undo_is_identity` checks. Undo also restores + permission bits, but no test compares them; owner, group, mtime and symlink + identity are recorded and not restored ([RMR §2](rmr-primitive.md)). +- $\sim_{model}$: propositional equality on the abstract state of + `verification/proofs/agda/TransactionAtomicity.agda`, with no mechanical link + to the filesystem. -### Property 2: Formal Obliteration (RMO) +For an operation $F$ with precondition domain $D_F$ and recorded inverse $F^{-1}$: -After $\text{RMO}(d)$ for data $d$: +$$\text{RMR-L:}\quad \forall s \in D_F.\; F^{-1}(F(s)) \sim s \qquad\qquad \text{RMR-R:}\quad \forall t \in F(D_F).\; F(F^{-1}(t)) \sim t$$ -$$\nexists \text{ algorithm } A: A(\text{system\_state}) \to d$$ +Together they make $F$ a bijection from $D_F$ onto its image, up to $\sim$. +RMR-R is over the image only: $\text{Copy}^{-1}$ is a delete of the +destination, and copying again does not restore arbitrary destination content. +RMR-R follows from RMR-L when $F$ respects $\sim$; that congruence is not stated +or tested. -No algorithm can recover the obliterated data from system state. +| Part | Status | +|---|---| +| RMR-L, one step, $\sim_{tree}$ | **TESTED** for Delete, Modify, Move, Copy, Create; Chmod is not in the test; Chown undo is unimplemented; the failure path is ASSUMED (T-6) | +| RMR-L, a transaction undone in reverse order, $\sim_{model}$ | **PROVEN** in the model (T-1), given T-6 | +| RMR-R | **OPEN** — no ledger row; neither proved nor tested | +| "Every operation is reversible" | **OPEN** | + +### Property 2: Obliteration (RMO) — target, not established + +The target: after $\text{RMO}(d)$, no algorithm recovers $d$ from the system +state. That an attacker cannot recover obliterated content is **OPEN** (ledger +E-1; only its model-level shadow E-1m is proved). Hash one-wayness and physical +erasure are **ASSUMED**, external to this repository (X-1). See +[RMO Primitive Specification](rmo-primitive.md). ### Property 3: Accountability Preservation @@ -165,7 +193,10 @@ The fact of deletion is logged, maintaining accountability without content prese ## Implementation in JanusKey -JanusKey currently implements RMR fully. RMO support is planned. +JanusKey implements RMR at the strength stated under Property 1, and RMO as +`jk obliterate` (`crates/januskey-cli/src/obliteration.rs`). The "Planned RMO +Implementation" sketch below predates that module; its step 4 ("non-existence +proof") was never implemented and is not claimed (E-1, X-1). ### Current RMR Implementation diff --git a/docs/wiki/theory/rmr-primitive.md b/docs/wiki/theory/rmr-primitive.md index 2d425e6..3b3f91d 100644 --- a/docs/wiki/theory/rmr-primitive.md +++ b/docs/wiki/theory/rmr-primitive.md @@ -18,7 +18,10 @@ operation `F` it applies to state `S`, it records enough to apply an inverse `F⁻¹` with `F⁻¹(F(S)) = S`. -Whether that holds in general is **open**. What holds today, concretely: +Whether that holds in general is **open**. That sentence is one-sided and leaves +the equality on states implicit; the precise statement — both directions +(RMR-L, RMR-R), each relative to a named equality on states — is +[MAA Property 1](maa-framework.md). What holds today, concretely: - each operation type has a named inverse (`OperationType::inverse`: `Delete↔Create`, `Modify↔Modify`, `Move↔Move`, `Copy→Delete`, `Chmod`, diff --git a/draft-hyperpolymath-maa-framework-00.txt b/draft-hyperpolymath-maa-framework-00.txt index 01236fa..45c51ee 100644 --- a/draft-hyperpolymath-maa-framework-00.txt +++ b/draft-hyperpolymath-maa-framework-00.txt @@ -4,6 +4,20 @@ Intended status: Informational [October 13, 20 Expires: April 13, 2026 Mutually Assured Accountability (MAA) Framework + +STATUS OF THIS COPY (repository note, 2026-11-09) + + EXPIRED DRAFT. This is the -00 draft dated October 13, 2025. It + expired on April 13, 2026 and has not been renewed: no -01 exists. + Nothing in this repository records that it was submitted to the + IETF, adopted by a working group, or ratified by anyone, so it has + no standing as an IETF document. Read it as a design note. + + The text below was corrected in place on 2026-11-09. The changes are + listed under "Revision note" at the end, and the original -00 text + is in git history (commit 2361441). The claims ledger in + PROOF-NEEDS.adoc is the authority for every status word used here. + Abstract The widespread reliance on unverifiable, best-effort transactional @@ -11,94 +25,158 @@ integrity and data deletion mechanisms in decentralized systems constitutes a systemic trust deficit. This deficit leads to chronic compliance failures (e.g., GDPR Article 17) and unrecoverable state corruption in Edge and IoT deployments. This document introduces the -Mutually Assured Accountability (MAA) Framework, a novel ethical -and engineering paradigm. MAA operationalises the **Maximal -Principle Reduction (MPR)** axiom by defining a set of formally -verifiable, dual primitives (RMR and RMO) that structurally enforce -a balance between auditability and user autonomy. The MAA Framework -proposes achieving system dependability through mathematically -certain state reversibility and data obliteration, thereby replacing -operational logging reliance with structural, formal assurance. +Mutually Assured Accountability (MAA) Framework, an ethical and +engineering paradigm. MAA operationalises the **Maximal Principle +Reduction (MPR)** axiom by proposing a pair of dual primitives (RMR +and RMO) intended to balance auditability and user autonomy. Each +property claimed for them below is stated with its current evidence +status, and none of them is proved in full: reversibility is proved +only for a model and tested for single steps, and unrecoverability +after erasure is not proved. 1. Introduction The principles governing data management in high-assurance, decentralized systems remain fundamentally reliant on operational accountability methods (logging, monitoring, eventual consistency). -These methods fail to provide **epistemological certainty**—the +These methods do not provide **epistemological certainty**, the mathematical guarantee that a system state is correct, or that a deleted record no longer exists. This gap leads to structural trust deficits. -The MAA Framework addresses this by establishing two symmetrical, -formally verifiable primitives derived from the MPR axiom. These -primitives are structurally guaranteed by the **Oblíbený** language's -constraint-driven compilation model: +The MAA Framework addresses this by proposing two symmetrical +primitives derived from the MPR axiom. They are implemented in Rust +in this repository (crates/reversible-core, crates/januskey-cli). +No other language or toolchain enforces them: nothing here is +compiled by, constrained by, or depends on the Oblíbený toolchain +that the -00 text named. * **RMR (Reversible Transaction):** A primitive for state transitions - that guarantees instant, mathematically certain rollback to a - prior safe state via Algorithmic Reversibility. This maximizes - system auditability and dependability. + that records, before each change, what is needed to undo it. Its + reversibility claim is relative to a stated equality on states and + has two directions (Section 3). It supports auditability and + dependability. * **RMO (Obliterative Wipe):** A primitive for data erasure that - achieves Formal Obliteration, proving the non-existence of - specified data traces, thereby providing verifiable individual - autonomy. + overwrites and removes the data and leaves a tamper-evident record + that it did so. It does not prove that the data no longer exists + (Section 4). The MAA dynamic dictates that the deployment of RMR (Accountability) -must be coupled with RMO (Control), stabilizing the system through -a mutually enforced set of formal constraints. +must be coupled with RMO (Control). 2. Terminology The key terms defined within this document are: * **MAA (Mutually Assured Accountability):** The ethical and - engineering paradigm that structurally balances adversarial - system requirements using formal verification. + engineering paradigm that balances adversarial system requirements + by pairing a reversible primitive with an erasing one. * **MPR (Maximal Principle Reduction):** The core axiom used to - constrain system complexity to a minimal, verifiable subset. - -* **Oblíbený:** The specialized language and compiler toolchain that - enforces the MPR axiom via a Turing-Incomplete Deployment Subset. + constrain system complexity to a minimal, checkable subset. It is a + design philosophy; no tool in this repository enforces it. -* **RMR (Reversible Transaction):** A data primitive, implemented - via the **Oblíbený** toolchain (targeting Rust/WASM), that guarantees - the existence of a mathematically sound inverse function for every - state change. +* **RMR (Reversible Transaction):** A data primitive that records, for + each state change F, the information that determines an inverse + F^-1. Section 3 states exactly what is claimed about F^-1. -* **RMO (Obliterative Wipe):** A data primitive that guarantees, - via formal proof, the non-existence (unrecoverability) of specific - data after invocation, satisfying the Right to Erasure. +* **RMO (Obliterative Wipe):** A data primitive that overwrites and + removes specified data and records the fact. Whether the data is + unrecoverable afterwards is not established (Section 4). 3. MAA and Formal Integrity - + Current distributed transaction models (e.g., Two-Phase Commit, Saga) are complex and can enter blocking or inconsistent states. RMR -proposes replacement with a simple, formally verified mechanism -where the guarantee of integrity is based on the proven symmetry of -the underlying function: $F^{-1}(\text{F}(\text{State})) = \text{State}$. The -formal proof scripts for RMR demonstrate that the primitive is -structurally incapable of leaving the state corrupted. +proposes a simpler mechanism: each operation records the information +that determines its inverse before it changes anything. + +3.1. The equality the claim is relative to + +Every reversibility statement in this section is an equality up to an +equivalence ~ on states, and it says nothing about any finer equality. +Two equivalences are in use: + + ~tree Two states are ~tree-equal when the regular files under the + working tree have the same relative paths and the same byte + content. Permission bits, owner and group, timestamps, + symlink identity, inode identity and empty directories are + not compared. This is what the property test + execute_then_undo_is_identity checks. The implementation + also restores permission bits on undo, but no test compares + them, so they are not part of ~tree. Owner, group, mtime + and symlink identity are recorded but not restored. + + ~model Propositional equality on the abstract state type of + verification/proofs/agda/TransactionAtomicity.agda. Nothing + links that type to the filesystem mechanically. + +3.2. The claim, in both directions + +Let F be an operation, D_F the states on which its precondition holds, +and F^-1 the inverse determined by the metadata F recorded. + + RMR-L (left inverse): for every s in D_F, F^-1(F(s)) ~ s + RMR-R (right inverse): for every t in F(D_F), F(F^-1(t)) ~ t + +Together they say that F, restricted to D_F, is a bijection onto its +image up to ~. RMR-R ranges over the image F(D_F) only, not over every +state on which F^-1 is defined: Copy^-1 is Delete of the destination, +and copying again does not restore arbitrary destination content. +RMR-R follows from RMR-L when F respects ~ (s ~ s' implies +F(s) ~ F(s')), and that congruence is not stated or tested either. + +3.3. What is established today + + RMR-L, one step, ~tree TESTED for Delete, Modify, Move, Copy and + Create (property test above). Chmod is + not in that test; Chown undo is not + implemented. A failed execute leaving the + state unchanged is ASSUMED (ledger T-6). + RMR-L, sequences, ~model PROVEN as ledger T-1 + (TransactionAtomicity.rollback-restores), + given that each step's undo restores its + execute (T-6, ASSUMED). + RMR-R No ledger row. Not proved, not tested: + OPEN. + "Every operation is OPEN. + reversible" + Obliteration Excluded by construction: a transaction + containing one is not all-reversible + (ledger C-3, PROVEN in the model). + +The guarantee is therefore not that the primitive "is structurally +incapable of leaving the state corrupted". It is the conditional +statements above, at the strength the ledger gives them. 4. MAA and User Autonomy RMO addresses the chronic failure of data persistence to honour user -deletion requests. The primitive ensures that the integrity of the -data record is broken and its digital reminiscence is eliminated. This -capability is crucial for compliance with privacy frameworks, -providing a verifiable technical mechanism for the individual's -right to control their digital history. +deletion requests. The primitive overwrites the data in place, removes +it, scrubs the unshared content-store blobs and log entries for it, and +records a timestamped commitment to what was destroyed. That record is +tamper-evident; it is not a certificate that the data is gone. + +That an attacker cannot recover obliterated content is OPEN (ledger +E-1); only a model-level shadow of it is proved (E-1m). Hash +one-wayness and physical erasure on the storage media are ASSUMED, +external to this repository (ledger X-1). Overwrite in place does not +guarantee physical erasure on SSD, copy-on-write or journaling +filesystems. RMO is a mechanism relevant to the right to erasure; it +is not a compliance determination. 5. Security Considerations The MAA framework shifts the security focus from patch management -to structural design. Security is assured by forcing the smallest -possible Trusted Computing Base (TCB) at the protocol/primitive -layer. The integrity of the MAA framework itself relies on the rigor -of the formal verification proofs (e.g., using Isabelle/HOL and Z3) -which must be auditable and maintained openly (e.g., as FOSS). +to structural design, by keeping the Trusted Computing Base (TCB) at +the protocol/primitive layer as small as possible. The framework is +only as strong as its proofs, which must be auditable and maintained +openly (e.g., as FOSS). The proofs in this repository are Agda +(--safe --without-K, verification/proofs/agda) and an Idris2 ABI +(src/abi). They cover the models named in Sections 3 and 4, not the +Rust implementation. This repository contains no Isabelle/HOL theory +and no Z3 script, and none of its claims rests on either. 6. IANA Considerations @@ -114,7 +192,27 @@ epistemological dilemmas (Wittgenstein and Russell) and by the critical necessity to clearly articulate verifiable security concepts in response to challenges raised by Joshua Jewell. - Author's Address + Revision note (2026-11-09) + +Corrected in place. The draft was not renewed, and no new revision +number was assigned. + +* Status: marked expired and unratified (top of document). +* Oblíbený: the -00 text said the primitives are "structurally + guaranteed" by, and RMR "implemented via", the Oblíbený toolchain. + This repository contains no Oblíbený source, configuration or + dependency, so those attributions and the Oblíbený glossary entry + were removed. +* Isabelle/HOL and Z3: the -00 text named them as the verification + tools. This repository has neither, so Section 5 now names the + provers it actually uses. +* RMR: -00 stated F^-1(F(State)) = State as proved and unconditional. + Section 3 now states it in both directions, relative to a named + equality on states, with the evidence status of each part. +* RMO: -00 said it proves the non-existence of the data. Section 4 + now carries the ledger status (E-1 OPEN, X-1 ASSUMED). + +Author's Address Jonathan D.A. Jewell The Open University From e2b4f1d5224e07bc1b341e9ef85e3654435e7332 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:27:28 +0000 Subject: [PATCH 2/5] docs(maa): narrow RMO record, RMR ordering and undo-token claims to what the code does Address the CodeRabbit review on #173. - operations.rs: the second-undo test now asserts the reloaded log still holds the operation with `undone` set, and matches the exact `OperationFailed("Operation {id} already undone")` refusal in both the same-process and reloaded cases, so an unknown-id error cannot pass. - ADR-0003: option B's compile-time guarantee covers reuse of the same token only; undo by id stays available and is guarded at run time; the must_use message, the comparison row and the recommendation say so, and T-8 stays OPEN. Option D: start-up reconciliation covers a restart only; idempotency needs every undo attempt, in-process too, to finish a pending intent instead of changing the file again. - wiki index: the transaction-model proof is stated under its premise (each step's undo restores the state it started from); the RMO record is an unkeyed ledger kept only when a store exists, alterable without detection, and a failed ledger write after removal can leave the removal unrecorded while a re-run skips the missing blob. - maa-framework.md and the draft: RMR's "guaranteed reversal / no data loss" become goals; the bijection-modulo-~ claim is replaced by the inverse laws plus a note that the result does not identify its predecessor; the metadata log is written after the filesystem change (T-9 OPEN), so the inverse is not wholly recorded beforehand; every "tamper-evident" RMO claim is removed. rmr-primitive.md's ordering bullet is corrected the same way. Test count unchanged: 142 (cargo test --workspace --locked). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- crates/januskey-cli/src/operations.rs | 23 +++++++++++++-- docs/adr/0003-undo-token-design-note.adoc | 12 ++++---- docs/wiki/theory/index.md | 20 ++++++++----- docs/wiki/theory/maa-framework.md | 32 +++++++++++++-------- docs/wiki/theory/rmr-primitive.md | 5 ++-- draft-hyperpolymath-maa-framework-00.txt | 34 +++++++++++++++++------ 6 files changed, 88 insertions(+), 38 deletions(-) diff --git a/crates/januskey-cli/src/operations.rs b/crates/januskey-cli/src/operations.rs index b0b8124..da0c873 100644 --- a/crates/januskey-cli/src/operations.rs +++ b/crates/januskey-cli/src/operations.rs @@ -534,14 +534,31 @@ mod tests { // 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); - assert!(executor.undo(&modify.id).is_err()); + 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 undone flag is persisted. + // 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); - assert!(executor.undo(&modify.id).is_err()); + 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"); } diff --git a/docs/adr/0003-undo-token-design-note.adoc b/docs/adr/0003-undo-token-design-note.adoc index 6fb59b5..63b4aba 100644 --- a/docs/adr/0003-undo-token-design-note.adoc +++ b/docs/adr/0003-undo-token-design-note.adoc @@ -16,11 +16,11 @@ == 2. What a token would and would not add -A token would turn "undo this operation at most once" from a runtime check into a compile-time one, for Rust callers that hold the value `execute` returned: +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 = "an UndoToken is the only way to undo this operation"] +#[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<'_> { @@ -30,7 +30,7 @@ impl OperationExecutor<'_> { } ---- -Because `undo_token` takes the token by value, a second call with the same token fails to compile. A `compile_fail` doctest can pin that without new dependencies. A trybuild test is an alternative, but it adds a dev-dependency. +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: @@ -50,20 +50,20 @@ What it would not add: | 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 guarantee covers in-process library callers only. +| 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, then reconcile it on the next start. This makes a retried undo idempotent. +| 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. A retry is idempotent only if every undo attempt, in the same process as well as after a restart, first looks for a pending intent on that id and finishes it (records the undo, clears the intent) instead of changing the file again. How it tells whether the file change was applied before a crash is part of this design and not settled here. | 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 library misuse visible at compile time, but it does not touch that path. 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 in-process callers only and that T-8 remains open. +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 diff --git a/docs/wiki/theory/index.md b/docs/wiki/theory/index.md index 8bb234a..6f37ca7 100644 --- a/docs/wiki/theory/index.md +++ b/docs/wiki/theory/index.md @@ -57,13 +57,19 @@ The **Mutually Assured Accountability (MAA) Framework** balances two opposing re These are implemented through dual primitives: - **RMR (Reversible Transaction)**: Records each change's inverse; undo restores - the prior state up to a stated equality, tested for single steps and proved - for a transaction model; the right-inverse direction and "every operation is - reversible" are OPEN (see [MAA Property 1](maa-framework.md)) - -- **RMO (Obliterative Wipe)**: Best-effort overwrite and removal with a - tamper-evident record; unrecoverability is OPEN (E-1) and physical erasure is - ASSUMED (X-1) + the prior state up to a stated equality. This is tested for single steps. 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)) + +- **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) diff --git a/docs/wiki/theory/maa-framework.md b/docs/wiki/theory/maa-framework.md index fa4effc..2641b72 100644 --- a/docs/wiki/theory/maa-framework.md +++ b/docs/wiki/theory/maa-framework.md @@ -71,23 +71,25 @@ verified in full; the status of each part is stated below and in the ledger. ### RMR (Reversible Transaction) -> A primitive for state transitions that records, before each change, what is needed to undo it — so that undo is a metadata lookup rather than a restore from backup. Whether every operation is *in fact* reversible is an open obligation, not a guarantee; see the claims ledger. +> A primitive for state transitions that records what is needed to undo each change — so that undo is a metadata lookup rather than a restore from backup. For a delete or modify the original content is stored before the change; the operation's metadata is saved to the log after it, so a stop between the two leaves undo unable to find the operation (OPEN, T-9). Whether every operation is *in fact* reversible is an open obligation, not a guarantee; see the claims ledger. -RMR provides: +RMR aims at the following. These are goals, not established guarantees: -- Complete state capture before changes +- Capture of everything undo needs (the log record is written after the + change; T-9 is OPEN) -- Guaranteed reversal capability +- Reversal of every operation ("every operation is reversible" is OPEN, and + Chown undo is not implemented) -- Full audit trail of all operations +- A full audit trail of all operations -- Accountability without data loss risk +- Accountability without risk of data loss See: [RMR Primitive Specification](rmr-primitive.md) ### RMO (Obliterative Wipe) -> A primitive for data erasure: best-effort overwrite, removal, store scrub, and a tamper-evident record of what was destroyed. +> A primitive for data erasure: best-effort overwrite, removal, store scrub, and, when a JanusKey store exists, an unkeyed record of what was destroyed. The record is not tamper-evident. RMO provides: @@ -164,7 +166,12 @@ For an operation $F$ with precondition domain $D_F$ and recorded inverse $F^{-1} $$\text{RMR-L:}\quad \forall s \in D_F.\; F^{-1}(F(s)) \sim s \qquad\qquad \text{RMR-R:}\quad \forall t \in F(D_F).\; F(F^{-1}(t)) \sim t$$ -Together they make $F$ a bijection from $D_F$ onto its image, up to $\sim$. +Together they say that, up to $\sim$, the recorded inverse undoes $F$ on $D_F$ +and $F$ undoes it on $F(D_F)$. They do not say that the resulting state +identifies the state before it: deleting a file from two trees that differ only +in that file's content gives $\sim$-equal results, and the recorded metadata, +not the resulting state, selects what undo restores. + RMR-R is over the image only: $\text{Copy}^{-1}$ is a delete of the destination, and copying again does not restore arbitrary destination content. RMR-R follows from RMR-L when $F$ respects $\sim$; that congruence is not stated @@ -295,10 +302,11 @@ smaller, differently-shaped things, and the difference matters: (`verification/proofs/agda/TransactionAtomicity.agda`, ledger rows T-1..T-3). The claim "every operation is reversible" is **OPEN**, as is the mechanical correspondence between that model and the Rust. -- **RMO:** nothing is proved. Overwriting is best effort; the record is - tamper-evident, not a certificate of absence. There is no mathematical proof - of non-existence, and there cannot be one from inside this process: the tool - cannot observe the media, the journal, or the backups. +- **RMO:** nothing is proved. Overwriting is best effort; the record is an + unkeyed ledger that a writer can alter without detection, kept only when a + store exists, and it is not a certificate of absence. There is no + mathematical proof of non-existence, and there cannot be one from inside this + process: the tool cannot observe the media, the journal, or the backups. The claims ledger in `PROOF-NEEDS.adoc` is the authority for both, and `dashboard-check` fails the build when a dashboard's counts disagree with it. diff --git a/docs/wiki/theory/rmr-primitive.md b/docs/wiki/theory/rmr-primitive.md index 3b3f91d..366df73 100644 --- a/docs/wiki/theory/rmr-primitive.md +++ b/docs/wiki/theory/rmr-primitive.md @@ -26,8 +26,9 @@ the equality on states implicit; the precise statement — both directions - each operation type has a named inverse (`OperationType::inverse`: `Delete↔Create`, `Modify↔Modify`, `Move↔Move`, `Copy→Delete`, `Chmod`, `Chown` self-inverse); -- the information needed for that inverse is captured *before* the mutation - (content into the store, file metadata into the log); +- the content a delete or modify needs is stored *before* the mutation, but the + operation's metadata is appended to the log *after* it, so a stop between the + two leaves the operation unfindable by undo (OPEN, T-9); - `execute` then `undo` restores the prior state under property testing (`property_tests::execute_then_undo_is_identity`); - rolling back a whole transaction in reverse order restores the state it diff --git a/draft-hyperpolymath-maa-framework-00.txt b/draft-hyperpolymath-maa-framework-00.txt index 45c51ee..959d347 100644 --- a/draft-hyperpolymath-maa-framework-00.txt +++ b/draft-hyperpolymath-maa-framework-00.txt @@ -52,14 +52,17 @@ compiled by, constrained by, or depends on the Oblíbený toolchain that the -00 text named. * **RMR (Reversible Transaction):** A primitive for state transitions - that records, before each change, what is needed to undo it. Its + that, for a delete or modify, stores the original content before + the change, and appends the operation's metadata to its log after + the change; together these determine how to undo it. Its reversibility claim is relative to a stated equality on states and has two directions (Section 3). It supports auditability and dependability. * **RMO (Obliterative Wipe):** A primitive for data erasure that - overwrites and removes the data and leaves a tamper-evident record - that it did so. It does not prove that the data no longer exists + overwrites and removes the data and, when a JanusKey store exists, + writes an unkeyed record that it did so. The record is not + tamper-evident. It does not prove that the data no longer exists (Section 4). The MAA dynamic dictates that the deployment of RMR (Accountability) @@ -90,7 +93,12 @@ The key terms defined within this document are: Current distributed transaction models (e.g., Two-Phase Commit, Saga) are complex and can enter blocking or inconsistent states. RMR proposes a simpler mechanism: each operation records the information -that determines its inverse before it changes anything. +that determines its inverse. Only part of that is recorded before the +change: for a delete or modify the original content is stored first, +but the executor saves the operation's metadata after the filesystem +change. A process stop between the two leaves normal undo unable to +find the operation, even though the original content blob exists +(OPEN, T-9). 3.1. The equality the claim is relative to @@ -120,9 +128,15 @@ and F^-1 the inverse determined by the metadata F recorded. RMR-L (left inverse): for every s in D_F, F^-1(F(s)) ~ s RMR-R (right inverse): for every t in F(D_F), F(F^-1(t)) ~ t -Together they say that F, restricted to D_F, is a bijection onto its -image up to ~. RMR-R ranges over the image F(D_F) only, not over every -state on which F^-1 is defined: Copy^-1 is Delete of the destination, +Together they say that, up to ~, the recorded inverse undoes F on D_F +and F undoes it on F(D_F). They do not say that the resulting state +identifies the state before it: deleting a file from two trees that +differ only in that file's content gives ~-equal results, and the +recorded metadata, not the resulting state, selects what undo +restores. + +RMR-R ranges over the image F(D_F) only, not over every state on +which F^-1 is defined: Copy^-1 is Delete of the destination, and copying again does not restore arbitrary destination content. RMR-R follows from RMR-L when F respects ~ (s ~ s' implies F(s) ~ F(s')), and that congruence is not stated or tested either. @@ -156,7 +170,11 @@ RMO addresses the chronic failure of data persistence to honour user deletion requests. The primitive overwrites the data in place, removes it, scrubs the unshared content-store blobs and log entries for it, and records a timestamped commitment to what was destroyed. That record is -tamper-evident; it is not a certificate that the data is gone. +an unkeyed JSON ledger, kept only when a JanusKey store exists: a +writer can alter it, or recompute the commitment, without detection. +It is written after the data is removed, so a failed write can leave +a removal unrecorded, and a re-run skips the blob that is already +gone. It is not a certificate that the data is gone. That an attacker cannot recover obliterated content is OPEN (ledger E-1); only a model-level shadow of it is proved (E-1m). Hash From a0c493831e40c084a41b84732def8e035c5bc2d1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:19:31 +0000 Subject: [PATCH 3/5] =?UTF-8?q?docs(maa):=20add=20the=20T-9=20ledger=20row?= =?UTF-8?q?s,=20take=20the=20record=20into=20F=E2=81=BB=C2=B9,=20qualify?= =?UTF-8?q?=20Property=203?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - PROOF-NEEDS.adoc: T-9 had narrative mentions but no status-table or claims-ledger row. Add both, OPEN: every execute_* changes the filesystem and then appends its record, and undo runs the inverse and then calls mark_undone, so a stop between the two leaves a change the log does not record; closing it needs a write-ahead intent record. - maa-framework.md Property 1: execution now produces (post-state, record) and the inverse consumes the pair, so RMR-L and RMR-R are well-typed (the post-state alone cannot select what undo restores). Both assume the record was saved (T-9). - maa-framework.md Property 3: stated only for a store-backed run whose record saves succeed, TESTED by obliterate_scrubs_blobs_log_and_undo; the no-store path (cmd_obliterate -> obliterate_file writes no record), a failed record save after removal, and an absent file with only shared blobs are OPEN. Balancing rule 3 points there. - rmr-primitive.md: the informal definition takes the record too. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDjUNwStGwcKTtAQ3NY --- PROOF-NEEDS.adoc | 2 ++ docs/wiki/theory/maa-framework.md | 55 ++++++++++++++++++++++--------- docs/wiki/theory/rmr-primitive.md | 5 +-- 3 files changed, 45 insertions(+), 17 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9ea6b33..40c101b 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -75,6 +75,7 @@ tables must agree. | 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-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` in `+operations.rs+` changes the filesystem and then calls `+MetadataStore::append+`, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash, or a failed save that no later save in the same run repairs, between the two leaves a change the log does not record (on undo: the file restored but the operation still marked not undone, so a retry runs the inverse again). Save ordering cannot close this; it needs a write-ahead intent record, which is a design decision. Split out of T-8 in #168 | S-1 | A content hash that is not `+sha256:+` plus 64 lowercase hex digits never resolves to a path outside the store root | TESTED | `+content_store::tests::malformed_hash_never_leaves_the_store_root+`; fixed in #163 after audit probe P5 showed `+delete+` removing a file outside the store (`+docs/reports/audit/proof-statement-audit-2026-10-27.adoc+`) | S-2 | `+store+` repairs a blob a crash left damaged instead of deduplicating against it, and a successful store leaves no temporary file behind | TESTED | not claimed: cleanup after a failed write or rename, whose removal error `+store+` ignores, so a temporary file can remain; not claimed: that the write itself is atomic. `+store+` writes by temporary file, sync and rename, but by construction only; no test injects a failure mid-write. `+content_store::tests::store_repairs_a_blob_truncated_by_a_crash+`, `+store_leaves_no_temp_files_and_count_ignores_strays+`; fixed in #163 (probe P4) | L-1 | Editing any field of any audit-log entry makes `+verify_integrity+` fail | OPEN | false today, probes P1 and P2: algorithm, purpose, old_state, new_state, rotated_to and rotated_from are in neither the MAC nor the chain hash, and key_id, fingerprint and reason are chain-hashed only, so on the last entry nothing protects them. The fix is a MAC over every field (a scheme version bump) @@ -267,6 +268,7 @@ the status table above. |L-2: Removing trailing audit-log entries makes verify_integrity fail (false today: audit probe P3; needs an external anchor) |OPEN |`crates/januskey-cli/src/attestation.rs` |- |O-1: An ObliterationProof attests that the content it names was erased (false today: storage_cleared is hard-coded, audit probe P6) |OPEN |`crates/januskey-cli/src/obliteration.rs` |- |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-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` |- diff --git a/docs/wiki/theory/maa-framework.md b/docs/wiki/theory/maa-framework.md index 2641b72..b604ab5 100644 --- a/docs/wiki/theory/maa-framework.md +++ b/docs/wiki/theory/maa-framework.md @@ -138,7 +138,7 @@ The key insight of MAA is that RMR and RMO are not alternatives—they are compl 2. **RMO-on-request**: Users can invoke RMO to permanently erase -3. **Audit of RMO**: The *fact* that RMO was invoked is logged (but not the erased content) +3. **Audit of RMO**: The *fact* that RMO was invoked is logged (but not the erased content) when a JanusKey store exists and the record saves; see Property 3 for the cases where it is not 4. **No silent deletion**: RMO requires explicit user action @@ -162,20 +162,33 @@ says nothing about any finer equality. Two are in use: `verification/proofs/agda/TransactionAtomicity.agda`, with no mechanical link to the filesystem. -For an operation $F$ with precondition domain $D_F$ and recorded inverse $F^{-1}$: - -$$\text{RMR-L:}\quad \forall s \in D_F.\; F^{-1}(F(s)) \sim s \qquad\qquad \text{RMR-R:}\quad \forall t \in F(D_F).\; F(F^{-1}(t)) \sim t$$ - -Together they say that, up to $\sim$, the recorded inverse undoes $F$ on $D_F$ -and $F$ undoes it on $F(D_F)$. They do not say that the resulting state -identifies the state before it: deleting a file from two trees that differ only -in that file's content gives $\sim$-equal results, and the recorded metadata, -not the resulting state, selects what undo restores. +Executing an operation produces a state *and* a record. Write $S$ for states +(the working tree, or the model state) and $R$ for records: the operation's +`OperationMetadata` log entry together with the content-store blobs it names. +An operation $F$ with precondition domain $D_F \subseteq S$ is a map +$F : D_F \to S \times R$, with components $F(s) = (F_S(s),\, r_F(s))$. Its +recorded inverse consumes both, $F^{-1} : S \times R \to S$, because undo reads +the record (`OperationExecutor::undo` looks the operation up in the log and +retrieves the stored content by its hash): + +$$\text{RMR-L:}\quad \forall s \in D_F.\; F^{-1}(F_S(s),\, r_F(s)) \sim s \qquad\qquad \text{RMR-R:}\quad \forall s \in D_F.\; F_S\big(F^{-1}(F_S(s),\, r_F(s))\big) \sim F_S(s)$$ + +Together they say that, up to $\sim$, the inverse given the record undoes $F$ +on $D_F$, and $F$ undoes the inverse on the image of $D_F$. The post-state +alone does not determine what undo restores: deleting a file from two trees +that differ only in that file's content gives $\sim$-equal post-states with +different records, so no $F^{-1}$ of the post-state alone could satisfy RMR-L +for both. RMR-R compares states only; re-executing $F$ writes a new record (a +new id and timestamp), so it is not stated for records. RMR-R is over the image only: $\text{Copy}^{-1}$ is a delete of the destination, and copying again does not restore arbitrary destination content. -RMR-R follows from RMR-L when $F$ respects $\sim$; that congruence is not stated -or tested. +RMR-R follows from RMR-L when $F_S$ respects $\sim$ and the restored state is +again in $D_F$; neither is stated or tested. + +Both equations assume the record was saved. `execute_*` changes the filesystem +and then appends the record, so a stop between the two leaves a post-state with +no record for undo to consume (T-9, OPEN). | Part | Status | |---|---| @@ -192,11 +205,23 @@ E-1; only its model-level shadow E-1m is proved). Hash one-wayness and physical erasure are **ASSUMED**, external to this repository (X-1). See [RMO Primitive Specification](rmo-primitive.md). -### Property 3: Accountability Preservation +### Property 3: Accountability Preservation — store-backed path only + +The target, stated only for an RMO run in a directory with an initialized +JanusKey store, on the path where each record save succeeds: -$$\forall \text{RMO}(d): \text{log}(\text{timestamp}, \text{user}, \text{hash}(d))$$ +$$\forall\, \text{RMO}(d) \text{ store-backed, record saved}:\; \text{log}(\text{timestamp}, \text{user}, \text{hash}(d))$$ -The fact of deletion is logged, maintaining accountability without content preservation. +The record (`ObliterationRecord`) holds the timestamp, user and content hash, +never the content, and it is not tamper-evident (see RMO above). Outside that +path the property is not claimed: + +| Part | Status | +|---|---| +| Store-backed `jk obliterate` of a path with a working file and unshared blobs, every save succeeding: one record for the file and one per shredded blob, persisted | **TESTED** — `obliteration_cas_test::obliterate_scrubs_blobs_log_and_undo` reopens the obliteration log and counts one record for the file plus one per blob (the ledger row "Obliterating a path shreds its unshared blobs and log entries, and undo then has nothing") | +| `jk obliterate` with no initialized store | **OPEN**, false today, no ledger row — `cmd_obliterate` calls `obliterate_file` alone, which overwrites and removes the file and writes no record | +| Store-backed, a record save fails | **OPEN**, no ledger row — `record_proof` and `ObliterationManager::obliterate` remove the content first and save the record after, so a failed save leaves the erasure with no durable record unless a later save in the same run writes the pending one | +| Store-backed, working file absent and every blob shared with another path | **OPEN**, no ledger row, by inspection — `obliterate_path` purges the path's log entries and writes no obliteration record | ## Implementation in JanusKey diff --git a/docs/wiki/theory/rmr-primitive.md b/docs/wiki/theory/rmr-primitive.md index 366df73..f32cf39 100644 --- a/docs/wiki/theory/rmr-primitive.md +++ b/docs/wiki/theory/rmr-primitive.md @@ -15,8 +15,9 @@ ## Definition **RMR (Reversible Transaction)** is the property JanusKey aims at: for every -operation `F` it applies to state `S`, it records enough to apply an inverse -`F⁻¹` with `F⁻¹(F(S)) = S`. +operation `F` it applies to state `S`, producing a new state `S′` and a record +`r`, an inverse `F⁻¹` applied to the pair gives `F⁻¹(S′, r) = S`. The inverse +needs `r`: the new state alone does not say what undo restores. Whether that holds in general is **open**. That sentence is one-sided and leaves the equality on states implicit; the precise statement — both directions From 0c454e308b8dd43f8261b92641a034363f611775 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 9 Nov 2026 20:55:40 +0000 Subject: [PATCH 4/5] Update docs/wiki/theory/maa-framework.md Co-authored-by: coderabbitai[bot] <136622811+coderabbitai[bot]@users.noreply.github.com> Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com> --- docs/wiki/theory/maa-framework.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/wiki/theory/maa-framework.md b/docs/wiki/theory/maa-framework.md index b604ab5..cc2b512 100644 --- a/docs/wiki/theory/maa-framework.md +++ b/docs/wiki/theory/maa-framework.md @@ -327,7 +327,8 @@ smaller, differently-shaped things, and the difference matters: (`verification/proofs/agda/TransactionAtomicity.agda`, ledger rows T-1..T-3). The claim "every operation is reversible" is **OPEN**, as is the mechanical correspondence between that model and the Rust. -- **RMO:** nothing is proved. Overwriting is best effort; the record is an +- **RMO:** E-1m proves properties of an abstract model, not the Rust + implementation. Overwriting is best effort; the record is an unkeyed ledger that a writer can alter without detection, kept only when a store exists, and it is not a certificate of absence. There is no mathematical proof of non-existence, and there cannot be one from inside this From af1c10256c49e389fe9e9719ef18846f97014908 Mon Sep 17 00:00:00 2001 From: "coderabbitai[bot]" <136622811+coderabbitai[bot]@users.noreply.github.com> Date: Mon, 9 Nov 2026 21:19:25 +0000 Subject: [PATCH 5/5] docs(maa): define reversibility over saved executions and clarify undo recovery and erasure record limits --- docs/adr/0003-undo-token-design-note.adoc | 2 +- docs/wiki/theory/index.md | 10 +++- docs/wiki/theory/maa-framework.md | 53 +++++++++++++------- draft-hyperpolymath-maa-framework-00.txt | 61 ++++++++++++++--------- 4 files changed, 81 insertions(+), 45 deletions(-) diff --git a/docs/adr/0003-undo-token-design-note.adoc b/docs/adr/0003-undo-token-design-note.adoc index 63b4aba..8c9610d 100644 --- a/docs/adr/0003-undo-token-design-note.adoc +++ b/docs/adr/0003-undo-token-design-note.adoc @@ -57,7 +57,7 @@ What it would not add: | 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. A retry is idempotent only if every undo attempt, in the same process as well as after a restart, first looks for a pending intent on that id and finishes it (records the undo, clears the intent) instead of changing the file again. How it tells whether the file change was applied before a crash is part of this design and not settled here. +| 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. |=== diff --git a/docs/wiki/theory/index.md b/docs/wiki/theory/index.md index 6f37ca7..fc5bfa7 100644 --- a/docs/wiki/theory/index.md +++ b/docs/wiki/theory/index.md @@ -56,13 +56,21 @@ The **Mutually Assured Accountability (MAA) Framework** balances two opposing re These are implemented through dual primitives: + + + + - **RMR (Reversible Transaction)**: Records each change's inverse; undo restores - the prior state up to a stated equality. This is tested for single steps. For + 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)) + + - **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. diff --git a/docs/wiki/theory/maa-framework.md b/docs/wiki/theory/maa-framework.md index cc2b512..d2776e3 100644 --- a/docs/wiki/theory/maa-framework.md +++ b/docs/wiki/theory/maa-framework.md @@ -165,26 +165,41 @@ says nothing about any finer equality. Two are in use: Executing an operation produces a state *and* a record. Write $S$ for states (the working tree, or the model state) and $R$ for records: the operation's `OperationMetadata` log entry together with the content-store blobs it names. -An operation $F$ with precondition domain $D_F \subseteq S$ is a map -$F : D_F \to S \times R$, with components $F(s) = (F_S(s),\, r_F(s))$. Its -recorded inverse consumes both, $F^{-1} : S \times R \to S$, because undo reads -the record (`OperationExecutor::undo` looks the operation up in the log and -retrieves the stored content by its hash): - -$$\text{RMR-L:}\quad \forall s \in D_F.\; F^{-1}(F_S(s),\, r_F(s)) \sim s \qquad\qquad \text{RMR-R:}\quad \forall s \in D_F.\; F_S\big(F^{-1}(F_S(s),\, r_F(s))\big) \sim F_S(s)$$ - -Together they say that, up to $\sim$, the inverse given the record undoes $F$ -on $D_F$, and $F$ undoes the inverse on the image of $D_F$. The post-state -alone does not determine what undo restores: deleting a file from two trees -that differ only in that file's content gives $\sim$-equal post-states with -different records, so no $F^{-1}$ of the post-state alone could satisfy RMR-L -for both. RMR-R compares states only; re-executing $F$ writes a new record (a -new id and timestamp), so it is not stated for records. - -RMR-R is over the image only: $\text{Copy}^{-1}$ is a delete of the + + + + +An operation with precondition domain $D_F \subseteq S$ has a saved-execution +relation $F \subseteq D_F \times (S \times R)$. Write $s\;F\;(t,r)$ when an +execution from $s$ produces post-state $t$ and saves record $r$. The same input +state can have multiple outputs, including records differing only in IDs or +timestamps. Its recorded inverse consumes both, $F^{-1} : S \times R \to S$, +because undo reads the record (`OperationExecutor::undo` looks the operation up +in the log and retrieves the stored content by its hash). + +The target laws range over **every** saved output, including each such record: + +$$\text{RMR-L:}\quad \forall s \in D_F,\,(t,r).\; s\;F\;(t,r) \implies F^{-1}(t,r) \sim s$$ + +$$\text{RMR-R:}\quad \forall s \in D_F,\,(t,r).\; s\;F\;(t,r) \implies \big(\forall (t',r').\; F^{-1}(t,r)\;F\;(t',r') \implies t' \sim t\big)$$ + +RMR-R additionally requires that $F^{-1}(t,r)$ is in $D_F$ and has at least one +saved execution output; the universal clause must not hold merely because +re-execution is impossible. Together the laws say that, up to $\sim$, the +inverse given that execution's record undoes it, and every saved re-execution +restores its post-state. The post-state alone does not determine what undo +restores: deleting a file from two trees that differ only in that file's +content gives $\sim$-equal post-states with different records, so no $F^{-1}$ +of the post-state alone could satisfy RMR-L for both. RMR-R compares states +only; the new record $r'$ need not equal $r$ (IDs and timestamps may differ). + +RMR-R is over saved outputs only: $\text{Copy}^{-1}$ is a delete of the destination, and copying again does not restore arbitrary destination content. -RMR-R follows from RMR-L when $F_S$ respects $\sim$ and the restored state is -again in $D_F$; neither is stated or tested. +RMR-R follows from RMR-L if all state outputs on $\sim$-equivalent inputs are +$\sim$-equivalent and the restored state is again in $D_F$ with a saved output; +these additional conditions are not established or tested. + + Both equations assume the record was saved. `execute_*` changes the filesystem and then appends the record, so a stop between the two leaves a post-state with diff --git a/draft-hyperpolymath-maa-framework-00.txt b/draft-hyperpolymath-maa-framework-00.txt index 959d347..3144181 100644 --- a/draft-hyperpolymath-maa-framework-00.txt +++ b/draft-hyperpolymath-maa-framework-00.txt @@ -61,9 +61,11 @@ that the -00 text named. * **RMO (Obliterative Wipe):** A primitive for data erasure that overwrites and removes the data and, when a JanusKey store exists, - writes an unkeyed record that it did so. The record is not - tamper-evident. It does not prove that the data no longer exists - (Section 4). + writes an unkeyed record for each removal whose record save succeeds. + If the working file is absent and all stored blobs are shared with + other paths, the path's history can be purged without an obliteration + record. A record that is written is not tamper-evident. It does not + prove that the data no longer exists (Section 4). The MAA dynamic dictates that the deployment of RMR (Accountability) must be coupled with RMO (Control). @@ -122,24 +124,32 @@ Two equivalences are in use: 3.2. The claim, in both directions -Let F be an operation, D_F the states on which its precondition holds, -and F^-1 the inverse determined by the metadata F recorded. - - RMR-L (left inverse): for every s in D_F, F^-1(F(s)) ~ s - RMR-R (right inverse): for every t in F(D_F), F(F^-1(t)) ~ t - -Together they say that, up to ~, the recorded inverse undoes F on D_F -and F undoes it on F(D_F). They do not say that the resulting state -identifies the state before it: deleting a file from two trees that -differ only in that file's content gives ~-equal results, and the -recorded metadata, not the resulting state, selects what undo -restores. - -RMR-R ranges over the image F(D_F) only, not over every state on -which F^-1 is defined: Copy^-1 is Delete of the destination, -and copying again does not restore arbitrary destination content. -RMR-R follows from RMR-L when F respects ~ (s ~ s' implies -F(s) ~ F(s')), and that congruence is not stated or tested either. +Let F be the saved-execution relation of an operation, D_F the states +on which its precondition holds, and s F (t, r) mean an execution from +s produces state t and saves record r (metadata and referenced blobs). +Multiple records, including different IDs or timestamps, can accompany +the same state. F^-1(t, r) uses that execution's record to undo it. + + RMR-L (left inverse): for every s in D_F and saved output (t, r), + s F (t, r) implies F^-1(t, r) ~ s. + RMR-R (right inverse): for every s in D_F and saved output (t, r), + s F (t, r) implies that u = F^-1(t, r) is in D_F, has a saved + execution output, and every u F (t', r') satisfies t' ~ t. + +Together they say that, up to ~, the inverse given that execution's +record undoes it, and every saved re-execution restores its post-state. +Both laws require a saved record. They do not say that the resulting +state identifies the state before it: deleting a file from two trees +that differ only in that file's content gives ~-equal results, and +the record, not the resulting state, selects what undo restores. +RMR-R compares states only; the new record r' need not equal r. + +RMR-R ranges over saved outputs only, not over every state on which +F^-1 is defined: Copy^-1 is Delete of the destination, and copying +again does not restore arbitrary destination content. RMR-R follows +from RMR-L if all state outputs on ~-equivalent inputs are ~-equivalent +and the restored state is again in D_F with a saved output. These +additional conditions are not established or tested either. 3.3. What is established today @@ -169,9 +179,12 @@ statements above, at the strength the ledger gives them. RMO addresses the chronic failure of data persistence to honour user deletion requests. The primitive overwrites the data in place, removes it, scrubs the unshared content-store blobs and log entries for it, and -records a timestamped commitment to what was destroyed. That record is -an unkeyed JSON ledger, kept only when a JanusKey store exists: a -writer can alter it, or recompute the commitment, without detection. +records a timestamped commitment to each removal whose record save +succeeds, when a JanusKey store exists. If the working file is absent +and all stored blobs are shared with other paths, the path's history +can be purged without an obliteration record. When a record is written, +it is kept in an unkeyed JSON ledger: a writer can alter it, or +recompute the commitment, without detection. It is written after the data is removed, so a failed write can leave a removal unrecorded, and a re-run skips the blob that is already gone. It is not a certificate that the data is gone.