diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index d18815f..52721cd 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] # Proof Witness Grades, standards 3-practice/PROOF-POLICY.adoc §8 (the diff --git a/READINESS.adoc b/READINESS.adoc index 10dec90..b24d504 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, 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..da0c873 100644 --- a/crates/januskey-cli/src/operations.rs +++ b/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(); 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..8c9610d --- /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 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; +} +---- + +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 ` 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? diff --git a/docs/wiki/theory/index.md b/docs/wiki/theory/index.md index 464c228..fc5bfa7 100644 --- a/docs/wiki/theory/index.md +++ b/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 + + + + +- **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)) + + + +- **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 d0b2332..d2776e3 100644 --- a/docs/wiki/theory/maa-framework.md +++ b/docs/wiki/theory/maa-framework.md @@ -66,27 +66,30 @@ 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) -> 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: @@ -135,37 +138,112 @@ 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 ## 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) +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. + -After $\text{RMO}(d)$ for data $d$: + -$$\nexists \text{ algorithm } A: A(\text{system\_state}) \to d$$ +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). -No algorithm can recover the obliterated data from system state. +The target laws range over **every** saved output, including each such record: -### Property 3: Accountability Preservation +$$\text{RMR-L:}\quad \forall s \in D_F,\,(t,r).\; s\;F\;(t,r) \implies F^{-1}(t,r) \sim s$$ -$$\forall \text{RMO}(d): \text{log}(\text{timestamp}, \text{user}, \text{hash}(d))$$ +$$\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)$$ -The fact of deletion is logged, maintaining accountability without content preservation. +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 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 +no record for undo to consume (T-9, OPEN). + +| 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 — 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{ store-backed, record saved}:\; \text{log}(\text{timestamp}, \text{user}, \text{hash}(d))$$ + +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 -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 @@ -264,10 +342,12 @@ 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:** 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 + 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 26656b0..74c2b6e 100644 --- a/docs/wiki/theory/rmr-primitive.md +++ b/docs/wiki/theory/rmr-primitive.md @@ -15,16 +15,21 @@ ## 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**. 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`, `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 01236fa..3144181 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,189 @@ 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, 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 - achieves Formal Obliteration, proving the non-existence of - specified data traces, thereby providing verifiable individual - autonomy. + overwrites and removes the data and, when a JanusKey store exists, + 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), 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. 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 + +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 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 + + 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 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. + +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 +223,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