From 5710c1c304fa94501900814f3972d0883239948b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 22:18:29 +0000 Subject: [PATCH 1/2] proofs: transaction atomicity in the Agda kernel (T-1..T-3), with the gaps it exposes (T-4..T-7) New module verification/proofs/agda/TransactionAtomicity.agda, checked by scripts/check-agda.sh (--safe --without-K, resource-algebra pinned). Part A. rollback-restores: if every recorded operation executed successfully and each undo restores the state its execute started from, undoing the list in reverse order (what cmd_rollback does) restores the state the transaction began in. The per-step premise is the TESTED row execute_then_undo_is_identity; it is not proved here. Part B. A model of TransactionManager (begin, add_operation, commit, mark_rolled_back) with the invariant Good. lifecycle-preserves-good: each transition keeps Good (begin needs a fresh id) and rewrites only the Active transaction, so a completed one is never modified. at-most-one-active: at most one transaction is Active, and exactly one when the pointer is set. Negative controls (tests/reject-agda): ForwardRollback (undoing in execution order does not restore the state: 0 != 1) and CommitWhenIdle (commit with nothing active is an error, not a state change). Six mutants of the module, each breaking one definition (rollback order, begin without the freshness premise, settle keeping Active, wrong active count, commit when idle, begin while active), were refused by the checker. Ledger: T-1..T-3 PROVEN; T-4..T-7 added as OPEN/ASSUMED so the limits are on the record rather than implied: T-4 OPEN: a rollback that fails part-way cannot be retried. Reproduced with the real jk: after one undo error, the repaired retry stops at the first (already undone) operation and the transaction stays Active. cmd_rollback uses `?` on undo and has no resume. T-5 OPEN: by inspection, begin/add_operation/commit mutate the in-memory log before save()?, and save is a plain fs::write (not reproduced). T-6, T-7 ASSUMED: failed execute is a no-op; transaction ids do not collide. Dashboards: 8 -> 11 proofs (the PROVEN rows). The Idris2 rows could not be run in this sandbox (no idris2); CI's pinned image is the gate of record. No Rust changed. The T-4/T-5 gaps are recorded, not fixed. Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- PROOF-NEEDS.adoc | 21 +- READINESS.adoc | 6 +- TOPOLOGY.adoc | 2 +- scripts/check-agda.sh | 4 +- tests/reject-agda/CommitWhenIdle.agda | 19 + tests/reject-agda/ForwardRollback.agda | 42 ++ .../proofs/agda/TransactionAtomicity.agda | 364 ++++++++++++++++++ 7 files changed, 450 insertions(+), 8 deletions(-) create mode 100644 tests/reject-agda/CommitWhenIdle.agda create mode 100644 tests/reject-agda/ForwardRollback.agda create mode 100644 verification/proofs/agda/TransactionAtomicity.agda diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 4ef422b..eb16108 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -67,6 +67,13 @@ tables must agree. | G-3 | The FFI bridge preserves grade πŸ™ (homomorphism) | OPEN | resource-algebra lists homomorphisms OPEN; to file from JNK-01 | E-1 | An attacker cannot recover obliterated content or use a revoked key | OPEN | `+Types.adversaryCannotKnow+` holds only because `+Knows+` has no Adversary constructor (#145 item 3) | X-1 | Hash one-wayness; physical erasure (cryptographic and physical assumptions, external to this repository) | ASSUMED | not theorems of this repo +| T-1 | Undoing a fully executed transaction's operations in reverse order restores the state it began in, given each step's undo restores its execute (the sequential Theorem 3.4) | PROVEN | `+TransactionAtomicity.rollback-restores+`; `+tests/reject-agda/ForwardRollback.agda+` refused +| T-2 | begin, add_operation, commit and mark_rolled_back each preserve the log invariant (given a fresh id for begin) and rewrite only the Active transaction, so a completed one is never modified | PROVEN | `+TransactionAtomicity.lifecycle-preserves-good+`; `+tests/reject-agda/CommitWhenIdle.agda+` refused +| T-3 | At most one transaction is Active, and exactly one when the active pointer is set | PROVEN | `+TransactionAtomicity.at-most-one-active+` +| T-4 | A rollback that fails part-way can be retried to completion | OPEN | reproduced 2026-10-26 with the real `+jk+`: after one undo error the repaired retry stops at the first, already undone, operation and the transaction stays Active (`+cmd_rollback+`, `+?+` on `+undo+`) +| T-5 | The transaction log survives an I/O failure or a crash during save without disagreeing with memory or being corrupted | OPEN | by inspection, not reproduced: begin, add_operation and commit mutate the in-memory log before `+save()?+`, and `+save+` is a plain `+fs::write+` +| 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 |=== Removed, with the reason recorded beside the replacement in source: @@ -130,7 +137,7 @@ attestations undermine trust |Content store integrity |Content-addressed storage never returns wrong content |Hash collisions or bugs corrupt stored data -|Transaction atomicity |Delta application is atomic and reversible +|Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the partial-rollback, I/O-failure and id-freshness gaps are T-4 to T-7) |Partial transactions corrupt state |reversible-core |Undo/redo preserves data integrity |Core crate used by @@ -173,6 +180,9 @@ the status table above. |C-4: Replacing an attestation-chain entry by one with a different hash breaks the link |PROVEN |`src/abi/JanusKey/ABI/Proofs.idr::tamperBreaksLink` |`idris2 --typecheck src/abi/januskey-abi.ipkg` |C-5: The 32-, 16- and 112-byte ABI structs are 8-byte aligned (divisibility at the literals) |PROVEN |`src/abi/JanusKey/ABI/Layout.idr::oblitAligned` |`idris2 --typecheck src/abi/januskey-abi.ipkg` |G-1: Reversibility as a Loss grade: a trace is lossless only if every step is, and an obliterating step absorbs |PROVEN |`verification/proofs/agda/Reversibility.agda::lossless-trace-all` |`bash scripts/check-agda.sh` +|T-1: Undoing a fully executed transaction's operations in reverse order restores the state it began in, given each step's undo restores its execute |PROVEN |`verification/proofs/agda/TransactionAtomicity.agda::rollback-restores` |`bash scripts/check-agda.sh` +|T-2: begin, add_operation, commit and mark_rolled_back each preserve the log invariant (given a fresh id for begin) and rewrite only the Active transaction |PROVEN |`verification/proofs/agda/TransactionAtomicity.agda::lifecycle-preserves-good` |`bash scripts/check-agda.sh` +|T-3: At most one transaction is Active, and exactly one when the active pointer is set |PROVEN |`verification/proofs/agda/TransactionAtomicity.agda::at-most-one-active` |`bash scripts/check-agda.sh` |A-3: Idris2 struct sizes, status codes, enums and exported symbols agree with januskey.h and ffi/zig |TESTED |`scripts/check-abi-layout.sh::check-abi-layout` |`bash scripts/check-abi-layout.sh` |A-4: A linearly held library handle cannot be closed twice |TESTED |`tests/reject-idris/DoubleClose.idr::DoubleClose` |`bash scripts/check-idris-reject.sh DoubleClose` |A-4: A linearly held library handle cannot be forgotten |TESTED |`tests/reject-idris/ForgottenClose.idr::ForgottenClose` |`bash scripts/check-idris-reject.sh ForgottenClose` @@ -183,6 +193,10 @@ the status table above. |G-3: The FFI bridge preserves grade πŸ™ (a homomorphism; resource-algebra lists homomorphisms as OPEN) |OPEN |`verification/proofs/agda/Reversibility.agda` |- |E-1: An attacker cannot recover obliterated content or use a revoked key (adversaryCannotKnow holds only by construction of the model) |OPEN |`src/abi/JanusKey/ABI/Types.idr` |- |The six security obligations under "What Needs Proving" (obliteration, key derivation, attestation chain, content store, transaction atomicity, reversible-core) are proved |OPEN |`PROOF-NEEDS.adoc` |- +|T-4: A rollback that fails part-way can be retried to completion (reproduced 2026-10-26: after one undo error the repaired `jk rollback` stops at the first, already undone, operation and the transaction stays Active) |OPEN |`crates/januskey-cli/src/main.rs` |- +|T-5: The transaction log survives an I/O failure or a crash during save without disagreeing with memory or being corrupted (by inspection: the log is mutated before `save()?`, and `save` is a plain `fs::write`) |OPEN |`crates/reversible-core/src/transaction.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` |- |=== @@ -192,8 +206,9 @@ the status table above. ABI/runtime layer (ruling 2026-10-12): kernel statements live in `+verification/proofs/agda/+` with siblings consumed by pin (`+scripts/fetch-siblings.sh+`); the ABI lives in `+src/abi/+`. -Obliteration completeness, attestation chain integrity and transaction -atomicity are still to be stated there. The 225 `+unwrap()+` calls should +Transaction atomicity is stated there for the model +(`+verification/proofs/agda/TransactionAtomicity.agda+`, rows T-1 to T-3); +obliteration completeness and attestation chain integrity are still to be stated. The 225 `+unwrap()+` calls should be systematically replaced with proven error handling. === Priority diff --git a/READINESS.adoc b/READINESS.adoc index a344e22..8ee0d7a 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -9,7 +9,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0 === CRG Grade: D (Alpha β€” Unstable) *Justification:* 119 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the -Idris2 ABI typechecks and 8 proofs are checked (PROVEN ledger rows: ABI and grade lemmas, not the +Idris2 ABI typechecks and 11 proofs are checked (PROVEN ledger rows: ABI and grade lemmas, not the security obligations); benchmarks exist (5 Criterion groups). But: no fuzz testing, no mutation testing, 225 unwrap() calls, E2E mostly skips, benchmarks measured fake crypto until this session. RSR compliance @@ -61,11 +61,11 @@ handling |15 |Compatibility |MISSING |0 |β€” |No version migration tests -|16 |Proof regression |βœ“ |8 proofs checked |`+just test-proofs test-proofs-reject test-agda+` |Idris2 0.8.0 typecheck, Agda kernel, expected rejections +|16 |Proof regression |βœ“ |11 proofs checked |`+just test-proofs test-proofs-reject test-agda+` |Idris2 0.8.0 typecheck, Agda kernel, expected rejections (run by idris-abi.yml, agda-proofs.yml and dashboard-check) |=== -*Total declared:* 119 tests + 5 benchmark groups; 8 proofs checked (PROVEN ledger rows) *Total +*Total declared:* 119 tests + 5 benchmark groups; 11 proofs checked (PROVEN ledger rows) *Total missing:* Fuzz, mutation, chaos, compatibility === Aspect Matrix diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index 5733453..abf5b10 100644 --- a/TOPOLOGY.adoc +++ b/TOPOLOGY.adoc @@ -77,7 +77,7 @@ SECURITY (honest) INTERFACES & RESEARCH CLI Interface (jk) β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–‘β–‘ ~85% Full command set; no user testing yet MPR Methodology β–ˆβ–ˆβ–ˆβ–ˆβ–‘β–‘β–‘β–‘β–‘β–‘ ~40% Design documented; FORMAL PROOFS PENDING - (Idris2 ABI typechecks; 8 proofs checked: ABI and grade + (Idris2 ABI typechecks; 11 proofs checked: ABI and grade lemmas, not the security obligations; MPR not linked to the Rust) Testing (READINESS matrix) β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–‘β–‘β–‘β–‘ ~60% 119 tests + 5 benches; missing fuzz, mutation, chaos, compatibility (Grade D) diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 73e9d92..98b9f0d 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -11,7 +11,9 @@ prover="${AGDA:-agda}" bash scripts/fetch-siblings.sh flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check -i verification/proofs/agda -i _build/dependencies/resource-algebra/src) -"$prover" "${flags[@]}" verification/proofs/agda/Reversibility.agda +for module in Reversibility TransactionAtomicity; do + "$prover" "${flags[@]}" "verification/proofs/agda/$module.agda" +done mkdir -p _build/check-logs shopt -s nullglob rejects=(tests/reject-agda/*.agda) diff --git a/tests/reject-agda/CommitWhenIdle.agda b/tests/reject-agda/CommitWhenIdle.agda new file mode 100644 index 0000000..c38ad1f --- /dev/null +++ b/tests/reject-agda/CommitWhenIdle.agda @@ -0,0 +1,19 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection: with no active transaction, commit is an error +-- (NoActiveTransaction in the Rust), not a state change. The claim below +-- is false and the checker must refuse it; this pins the "refused in the +-- wrong state" half of the lifecycle model. +-- expect: nothing != just +module CommitWhenIdle where + +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Maybe using (Maybe; nothing; just) +open import ResourceAlgebra.Prelude +open import TransactionAtomicity + +open Lifecycle + +commit-when-idle : commit (log [] nothing) ≑ just (log [] nothing) +commit-when-idle = refl diff --git a/tests/reject-agda/ForwardRollback.agda b/tests/reject-agda/ForwardRollback.agda new file mode 100644 index 0000000..52911db --- /dev/null +++ b/tests/reject-agda/ForwardRollback.agda @@ -0,0 +1,42 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection: rollback must undo in reverse execution order. Two +-- real, individually invertible operations (double, then add one) are +-- executed from 1 (1 -> 2 -> 3); undoing them in EXECUTION order instead +-- ends at 0, not 1, so the checker must refuse the claim that it restores 1. +-- This pins that `rollback-restores` is not vacuous about order. +-- expect: 0 != 1 +module ForwardRollback where + +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Maybe using (Maybe; nothing; just) +open import ResourceAlgebra.Prelude +open import TransactionAtomicity + +open Rollback Nat + +half : Nat β†’ Nat +half zero = zero +half (suc zero) = zero +half (suc (suc n)) = suc (half n) + +half-double : βˆ€ x β†’ half (x + x) ≑ x +half-double zero = refl +half-double (suc y) rewrite +-suc y y = cong suc (half-double y) + +pred : Nat β†’ Nat +pred zero = zero +pred (suc n) = n + +doubleOp : Op +doubleOp = op (Ξ» x β†’ just (x + x)) half + (Ξ» {x} e β†’ trans (cong half (sym (just-inj e))) (half-double x)) + +incOp : Op +incOp = op (Ξ» x β†’ just (suc x)) pred + (Ξ» {x} e β†’ cong pred (sym (just-inj e))) + +-- The correct order is a theorem (rollback-restores); the forward order is not. +forward-restores : rollbackForward (doubleOp ∷ incOp ∷ []) 3 ≑ 1 +forward-restores = refl diff --git a/verification/proofs/agda/TransactionAtomicity.agda b/verification/proofs/agda/TransactionAtomicity.agda new file mode 100644 index 0000000..38c9b06 --- /dev/null +++ b/verification/proofs/agda/TransactionAtomicity.agda @@ -0,0 +1,364 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Transaction atomicity, in two parts that match the two places the Rust +-- keeps it. +-- +-- Part A (Rollback). `jk rollback` (crates/januskey-cli/src/main.rs, +-- cmd_rollback) undoes the recorded operations in reverse order +-- (Theorem 3.4, Sequential Reversibility). Theorem `rollback-restores`: +-- if every recorded operation executed successfully, and each one's undo +-- restores the state its execute started from, then undoing the whole +-- list in reverse order restores the state the transaction began in. +-- `rollback-restores` is the sequential generalisation of the one-step +-- premise TESTED as execute_then_undo_is_identity (cf. G-1). +-- +-- Part B (Lifecycle). `TransactionManager` +-- (crates/reversible-core/src/transaction.rs) is a log of transactions +-- plus a pointer to the active one. Invariant `Good`: the pointer is set +-- exactly when one transaction is Active; every other transaction is +-- Committed or RolledBack; and the Active one is the first with its id. +-- It is preserved by begin / add_operation / commit / mark_rolled_back, +-- and those operations rewrite only the Active transaction, so a +-- completed transaction is never modified. +-- +-- What is NOT claimed (the model is hand-transcribed from the Rust, like +-- G-2, and these are deliberate limits): +-- * No I/O. The Rust mutates the in-memory log and then calls save()?; +-- a save failure after the mutation leaves memory and disk disagreeing. +-- fs::write is not an atomic replace, so a crash mid-write can corrupt +-- the log. Neither is modelled. +-- * A failed execute is assumed to leave the state unchanged. Part A only +-- speaks about operations that executed; nothing here proves the Rust +-- executor is a no-op on failure. +-- * Rollback is assumed to succeed on every step. cmd_rollback stops at +-- the first undo error (`?`) and leaves the transaction Active with the +-- later operations already undone; a retry then meets "already undone". +-- Part A does not cover that case; see the OPEN ledger rows. +-- * Transaction ids are assumed fresh (Fresh below). The Rust draws a +-- UUID v4; a collision would break Good, and nothing here rules it out. +-- * Obliterating operations have no undo, so they have no `Op` here +-- (cf. C-3); a transaction containing one is outside this theorem. +-- * Concurrency: one process, no locking, is the whole model. + +module TransactionAtomicity where + +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Maybe using (Maybe; nothing; just) +open import ResourceAlgebra.Prelude + +---------------------------------------------------------------------- +-- Small prelude (the kernel pins builtins only; nothing is imported) +---------------------------------------------------------------------- + +infixr 5 _++_ +_++_ : {A : Set} β†’ List A β†’ List A β†’ List A +[] ++ ys = ys +(x ∷ xs) ++ ys = x ∷ (xs ++ ys) + +data _⊎_ (A B : Set) : Set where + inl : A β†’ A ⊎ B + inr : B β†’ A ⊎ B + +βŠ₯-elim : {A : Set} β†’ βŠ₯ β†’ A +βŠ₯-elim () + +just-inj : {A : Set} {a b : A} β†’ just a ≑ just b β†’ a ≑ b +just-inj refl = refl + +nothingβ‰’just : {A : Set} {a : A} β†’ nothing ≑ just a β†’ βŠ₯ +nothingβ‰’just () + +suc-inj : βˆ€ {m n} β†’ suc m ≑ suc n β†’ m ≑ n +suc-inj refl = refl + +_β‰Ÿ_ : (m n : Nat) β†’ (m ≑ n) ⊎ (m β‰’ n) +zero β‰Ÿ zero = inl refl +zero β‰Ÿ suc n = inr (Ξ» ()) +suc m β‰Ÿ zero = inr (Ξ» ()) +suc m β‰Ÿ suc n with m β‰Ÿ n +... | inl p = inl (cong suc p) +... | inr q = inr (Ξ» r β†’ q (suc-inj r)) + +data All {A : Set} (P : A β†’ Set) : List A β†’ Set where + [] : All P [] + _∷_ : βˆ€ {x xs} β†’ P x β†’ All P xs β†’ All P (x ∷ xs) + +---------------------------------------------------------------------- +-- Part A. Rollback undoes the recorded operations in reverse order +---------------------------------------------------------------------- + +module Rollback (S : Set) where + + -- A recorded operation: `execute` may fail (nothing); `undo`, applied to + -- the state a successful execute produced, restores the state it started + -- from. In the Rust: OperationExecutor::execute and ::undo + -- (crates/januskey-cli/src/operations.rs). `undoes` is the per-step + -- premise, TESTED as execute_then_undo_is_identity; it is not proved here. + record Op : Set where + constructor op + field + execute : S β†’ Maybe S + undo : S β†’ S + undoes : βˆ€ {x y} β†’ execute x ≑ just y β†’ undo y ≑ x + + open Op public + + -- The recorded list `os` (execution order) ran successfully from x to z. + data Executed : List Op β†’ S β†’ S β†’ Set where + done : βˆ€ {x} β†’ Executed [] x x + next : βˆ€ {o os x y z} β†’ execute o x ≑ just y β†’ Executed os y z β†’ Executed (o ∷ os) x z + + -- cmd_rollback: undo the last recorded operation first, the first last. + rollback : List Op β†’ S β†’ S + rollback [] z = z + rollback (o ∷ os) z = undo o (rollback os z) + + -- Theorem A-1 (rollback-restores). Undoing a fully executed transaction + -- in reverse order returns the state it began in. + rollback-restores : βˆ€ {os x z} β†’ Executed os x z β†’ rollback os z ≑ x + rollback-restores done = refl + rollback-restores (next {o} e r) = + trans (cong (undo o) (rollback-restores r)) (undoes o e) + + -- The order matters. Undoing in execution order instead is NOT a + -- theorem; it is here only so that tests/reject-agda/ForwardRollback.agda + -- can pin that the checker refuses the claim for it. + rollbackForward : List Op β†’ S β†’ S + rollbackForward [] z = z + rollbackForward (o ∷ os) z = rollbackForward os (undo o z) + +---------------------------------------------------------------------- +-- Part B. The TransactionManager lifecycle +---------------------------------------------------------------------- + +module Lifecycle where + + data TState : Set where + Active Committed RolledBack : TState + + Activeβ‰’Committed : Active ≑ Committed β†’ βŠ₯ + Activeβ‰’Committed () + + Activeβ‰’RolledBack : Active ≑ RolledBack β†’ βŠ₯ + Activeβ‰’RolledBack () + + -- id, state, operation ids in execution order. + record Tx : Set where + constructor tx + field + txId : Nat + txState : TState + txOps : List Nat + + open Tx public + + -- The log and the pointer to the active transaction. + record Log : Set where + constructor log + field + txs : List Tx + activeId : Maybe Nat + + open Log public + + Settled : Tx β†’ Set + Settled t = txState t β‰’ Active + + addOpTx : Nat β†’ Tx β†’ Tx + addOpTx o t = tx (txId t) (txState t) (txOps t ++ o ∷ []) + + settle : TState β†’ Tx β†’ Tx + settle s t = tx (txId t) s (txOps t) + + -- `iter_mut().find(|t| t.id == i)` then rewrite: only the FIRST transaction + -- with that id changes. nothing = no such transaction. + update : Nat β†’ (Tx β†’ Tx) β†’ List Tx β†’ Maybe (List Tx) + update i f [] = nothing + update i f (t ∷ ts) with txId t β‰Ÿ i + ... | inl _ = just (f t ∷ ts) + ... | inr _ with update i f ts + ... | nothing = nothing + ... | just us = just (t ∷ us) + + -- TransactionManager::begin(name), with the fresh id as an argument. + begin : Nat β†’ Log β†’ Maybe Log + begin i (log ts (just _)) = nothing + begin i (log ts nothing) = just (log (ts ++ tx i Active [] ∷ []) (just i)) + + -- TransactionManager::add_operation. + addOp : Nat β†’ Log β†’ Maybe Log + addOp o (log ts nothing) = nothing + addOp o (log ts (just i)) with update i (addOpTx o) ts + ... | nothing = nothing + ... | just us = just (log us (just i)) + + -- TransactionManager::commit (s = Committed) and ::mark_rolled_back + -- (s = RolledBack). + finish : TState β†’ Log β†’ Maybe Log + finish s (log ts nothing) = nothing + finish s (log ts (just i)) with update i (settle s) ts + ... | nothing = nothing + ... | just us = just (log us nothing) + + commit : Log β†’ Maybe Log + commit = finish Committed + + markRolledBack : Log β†’ Maybe Log + markRolledBack = finish RolledBack + + ---------------------------------------------------------------------- + -- The invariant + ---------------------------------------------------------------------- + + data Good : Log β†’ Set where + -- No pointer: nothing is Active. + idle : βˆ€ {ts} β†’ All Settled ts β†’ Good (log ts nothing) + -- Pointer to t: t is the first with its id, it is the one Active + -- transaction, and everything else is Committed or RolledBack. + busy : βˆ€ {pre t post} + β†’ All (Ξ» u β†’ txId u β‰’ txId t) pre + β†’ All Settled pre + β†’ txState t ≑ Active + β†’ All Settled post + β†’ Good (log (pre ++ t ∷ post) (just (txId t))) + + Fresh : Nat β†’ List Tx β†’ Set + Fresh i = All (Ξ» u β†’ txId u β‰’ i) + + good-empty : Good (log [] nothing) + good-empty = idle [] + + ---------------------------------------------------------------------- + -- Only the Active transaction is rewritten (completed ones are frozen) + ---------------------------------------------------------------------- + + update-active : βˆ€ f pre t post + β†’ All (Ξ» u β†’ txId u β‰’ txId t) pre + β†’ update (txId t) f (pre ++ t ∷ post) ≑ just (pre ++ f t ∷ post) + update-active f [] t post [] with txId t β‰Ÿ txId t + ... | inl _ = refl + ... | inr n = βŠ₯-elim (n refl) + update-active f (u ∷ pre) t post (n ∷ ns) with txId u β‰Ÿ txId t + ... | inl e = βŠ₯-elim (n e) + ... | inr _ with update (txId t) f (pre ++ t ∷ post) | update-active f pre t post ns + ... | .(just (pre ++ f t ∷ post)) | refl = refl + + ---------------------------------------------------------------------- + -- Settled transactions append and concatenate without becoming Active + ---------------------------------------------------------------------- + + all-++ : βˆ€ {A : Set} {P : A β†’ Set} {xs ys} + β†’ All P xs β†’ All P ys β†’ All P (xs ++ ys) + all-++ [] qs = qs + all-++ (p ∷ ps) qs = p ∷ all-++ ps qs + + ---------------------------------------------------------------------- + -- Theorem B-1: begin preserves Good (given a fresh id), and is refused + -- while a transaction is active. + ---------------------------------------------------------------------- + + begin-refused-while-active : βˆ€ i ts j β†’ begin i (log ts (just j)) ≑ nothing + begin-refused-while-active i ts j = refl + + begin-good : βˆ€ {i L L'} β†’ Good L β†’ Fresh i (txs L) β†’ begin i L ≑ just L' β†’ Good L' + begin-good (busy _ _ _ _) _ () + begin-good {i} (idle {ts} ss) fr refl = + busy {pre = ts} {t = tx i Active []} {post = []} fr ss refl [] + + ---------------------------------------------------------------------- + -- Theorem B-2: add_operation preserves Good, and is refused when idle. + ---------------------------------------------------------------------- + + addOp-refused-when-idle : βˆ€ o ts β†’ addOp o (log ts nothing) ≑ nothing + addOp-refused-when-idle o ts = refl + + addOp-good : βˆ€ {o L L'} β†’ Good L β†’ addOp o L ≑ just L' β†’ Good L' + addOp-good (idle _) () + addOp-good {o} (busy {pre} {t} {post} np sp act sq) eq + with update (txId t) (addOpTx o) (pre ++ t ∷ post) | update-active (addOpTx o) pre t post np + ... | .(just (pre ++ addOpTx o t ∷ post)) | refl with eq + ... | refl = busy {pre = pre} {t = addOpTx o t} {post = post} np sp act sq + + ---------------------------------------------------------------------- + -- Theorem B-3: commit and mark_rolled_back preserve Good, land idle, + -- and are refused when idle. + ---------------------------------------------------------------------- + + finish-refused-when-idle : βˆ€ s ts β†’ finish s (log ts nothing) ≑ nothing + finish-refused-when-idle s ts = refl + + finish-good : βˆ€ {s L L'} β†’ s β‰’ Active β†’ Good L β†’ finish s L ≑ just L' β†’ Good L' + finish-good _ (idle _) () + finish-good {s} sn (busy {pre} {t} {post} np sp act sq) eq + with update (txId t) (settle s) (pre ++ t ∷ post) | update-active (settle s) pre t post np + ... | .(just (pre ++ settle s t ∷ post)) | refl with eq + ... | refl = idle (all-++ sp ((Ξ» e β†’ sn e) ∷ sq)) + + commit-good : βˆ€ {L L'} β†’ Good L β†’ commit L ≑ just L' β†’ Good L' + commit-good = finish-good (Ξ» e β†’ Activeβ‰’Committed (sym e)) + + markRolledBack-good : βˆ€ {L L'} β†’ Good L β†’ markRolledBack L ≑ just L' β†’ Good L' + markRolledBack-good = finish-good (Ξ» e β†’ Activeβ‰’RolledBack (sym e)) + + ---------------------------------------------------------------------- + -- Theorem B-4: at most one transaction is Active, and exactly when the + -- pointer is set. + ---------------------------------------------------------------------- + + countActive : List Tx β†’ Nat + countActive [] = 0 + countActive (t ∷ ts) with txState t + ... | Active = suc (countActive ts) + ... | Committed = countActive ts + ... | RolledBack = countActive ts + + expected : Maybe Nat β†’ Nat + expected nothing = 0 + expected (just _) = 1 + + settled-count : βˆ€ {ts} β†’ All Settled ts β†’ countActive ts ≑ 0 + settled-count [] = refl + settled-count {t ∷ ts} (s ∷ ss) with txState t | s + ... | Active | s' = βŠ₯-elim (s' refl) + ... | Committed | _ = settled-count ss + ... | RolledBack | _ = settled-count ss + + count-++ : βˆ€ xs ys β†’ countActive (xs ++ ys) ≑ countActive xs + countActive ys + count-++ [] ys = refl + count-++ (x ∷ xs) ys with txState x + ... | Active = cong suc (count-++ xs ys) + ... | Committed = count-++ xs ys + ... | RolledBack = count-++ xs ys + + at-most-one-active : βˆ€ {L} β†’ Good L β†’ countActive (txs L) ≑ expected (activeId L) + at-most-one-active (idle ss) = settled-count ss + at-most-one-active (busy {pre} {t} {post} _ sp act sq) + rewrite count-++ pre (t ∷ post) | settled-count sp | act | settled-count sq = refl + + ---------------------------------------------------------------------- + -- Theorem B-5 (lifecycle-preserves-good): the four transitions together. + -- One name for the claims ledger: every transition that succeeds keeps + -- Good, begin additionally needs a fresh id, and each transition rewrites + -- only the Active transaction, leaving every settled one untouched. + ---------------------------------------------------------------------- + + record Preserves : Set where + field + onBegin : βˆ€ {i L L'} β†’ Good L β†’ Fresh i (txs L) β†’ begin i L ≑ just L' β†’ Good L' + onAddOp : βˆ€ {o L L'} β†’ Good L β†’ addOp o L ≑ just L' β†’ Good L' + onCommit : βˆ€ {L L'} β†’ Good L β†’ commit L ≑ just L' β†’ Good L' + onRollback : βˆ€ {L L'} β†’ Good L β†’ markRolledBack L ≑ just L' β†’ Good L' + onlyActive : βˆ€ f pre t post + β†’ All (Ξ» u β†’ txId u β‰’ txId t) pre + β†’ update (txId t) f (pre ++ t ∷ post) ≑ just (pre ++ f t ∷ post) + + lifecycle-preserves-good : Preserves + lifecycle-preserves-good = record + { onBegin = begin-good + ; onAddOp = addOp-good + ; onCommit = commit-good + ; onRollback = markRolledBack-good + ; onlyActive = update-active + } From ea1d5dd1d498ee201eb4360490426890af668b66 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 26 Oct 2026 22:25:36 +0000 Subject: [PATCH 2/2] docs: scope note says the PROVEN rows now include transaction-model lemmas READINESS and TOPOLOGY described the checked proofs as "ABI and grade lemmas"; T-1..T-3 added transaction-model lemmas (CodeRabbit on #161). Co-Authored-By: Claude Sonnet 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- READINESS.adoc | 2 +- TOPOLOGY.adoc | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/READINESS.adoc b/READINESS.adoc index 8ee0d7a..505a2db 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -9,7 +9,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0 === CRG Grade: D (Alpha β€” Unstable) *Justification:* 119 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the -Idris2 ABI typechecks and 11 proofs are checked (PROVEN ledger rows: ABI and grade lemmas, not the +Idris2 ABI typechecks and 11 proofs are checked (PROVEN ledger rows: ABI, grade and transaction-model lemmas, not the security obligations); benchmarks exist (5 Criterion groups). But: no fuzz testing, no mutation testing, 225 unwrap() calls, E2E mostly skips, benchmarks measured fake crypto until this session. RSR compliance diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index abf5b10..469db4b 100644 --- a/TOPOLOGY.adoc +++ b/TOPOLOGY.adoc @@ -77,7 +77,7 @@ SECURITY (honest) INTERFACES & RESEARCH CLI Interface (jk) β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–‘β–‘ ~85% Full command set; no user testing yet MPR Methodology β–ˆβ–ˆβ–ˆβ–ˆβ–‘β–‘β–‘β–‘β–‘β–‘ ~40% Design documented; FORMAL PROOFS PENDING - (Idris2 ABI typechecks; 11 proofs checked: ABI and grade + (Idris2 ABI typechecks; 11 proofs checked: ABI, grade and transaction-model lemmas, not the security obligations; MPR not linked to the Rust) Testing (READINESS matrix) β–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–ˆβ–‘β–‘β–‘β–‘ ~60% 119 tests + 5 benches; missing fuzz, mutation, chaos, compatibility (Grade D)