diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml index 7c7e653..25696fe 100644 --- a/.github/workflows/agda-proofs.yml +++ b/.github/workflows/agda-proofs.yml @@ -31,3 +31,34 @@ jobs: run: test "$(agda --version)" = 'Agda version 2.6.4.3' - name: Proofs, sibling pin, expected rejections run: bash scripts/check-agda.sh + recheck: + # PROOF-POLICY §2 recheck legs: the Rocq and Lean re-proofs of the Agda + # theorems, with their expected-rejection fixtures. Local run: just test-recheck. + name: Rocq and Lean recheck legs, expected rejections + runs-on: ubuntu-24.04 + timeout-minutes: 15 + env: + LEAN_VERSION: 4.35.0 + LEAN_SHA256: 7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d + steps: + - name: Install the pinned provers + run: | + sudo apt-get update + sudo apt-get install --no-install-recommends -y coq=8.18.0+dfsg-1build2 zstd + curl --proto '=https' --tlsv1.2 -sSfL -o lean.tar.zst \ + "https://github.com/leanprover/lean4/releases/download/v${LEAN_VERSION}/lean-${LEAN_VERSION}-linux.tar.zst" + echo "${LEAN_SHA256} lean.tar.zst" | sha256sum -c - + mkdir -p "$RUNNER_TEMP/lean" + tar --zstd -xf lean.tar.zst -C "$RUNNER_TEMP/lean" + rm lean.tar.zst + echo "$RUNNER_TEMP/lean/lean-${LEAN_VERSION}-linux/bin" >> "$GITHUB_PATH" + - name: Checkout + uses: actions/checkout@v7.0.1 + with: + persist-credentials: false + - name: Verify the checked prover versions + run: | + test "$(coqc --version | head -1)" = 'The Coq Proof Assistant, version 8.18.0' + lean --version | grep -q "^Lean (version ${LEAN_VERSION}, " + - name: Recheck legs, no axioms, expected rejections + run: bash scripts/check-recheck.sh diff --git a/.gitignore b/.gitignore index fdb1a82..7f2a0d3 100644 --- a/.gitignore +++ b/.gitignore @@ -91,3 +91,12 @@ deps/ build/ dist/ *.agdai + +# Rocq and Lean build outputs (scripts/check-recheck.sh builds in a temporary directory) +*.vo +*.vok +*.vos +*.glob +.*.aux +*.olean +*.ilean diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index d68c5af..d18815f 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -47,17 +47,16 @@ 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" [proof-grades] -# mathesis (estate-mathematical-architecture §5/§6) + standards -# 3-practice/PROOF-POLICY.adoc. A grade is a second axis over the PROVEN/TESTED -# ledger vocabulary, never a percentage. Detail: docs/theory/PROOF-GRADES.adoc. -grade-3 = "G-1, T-1, T-2, T-3 — Agda theory modules under verification/proofs/agda; AGDA-VERIFIED" -grade-3-pending = "E-1m — Epistemic.agda; no receipt yet, because the receipt-commit predates this module" -receipt-commit = "4afb710e86646658f667f10bd6274ee47416bfc7 (agda-proofs.yml run 40867211509, success)" -receipt-prover = "Agda 2.6.4.3 (agda-bin=2.6.4.3-1+b2); resource-algebra pinned at cf9235c" -receipt-flags = "--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check (canonical per PROOF-POLICY §2.1 since 2026-11-01; the 4afb710 CI receipt predates the flag, so the next agda-proofs.yml run is its receipt)" -not-graded = "the 7 Idris2 PROVEN rows (ABI/interface contracts, PROOF-POLICY §1); all 29 TESTED rows (observed behaviour); ASSUMED/DESIGNED/OPEN rows" -open-obligations = "re-earn the Agda receipt in CI under the canonical flag set; one Agda version across CI (agda-proofs pins 2.6.4.3, dashboard-check installs 2.6.3); no Creusot contract on the Rust, and neither rustc nor crates.io is reachable from the agent sandbox (docs/estate/environment-toolchains.md), so no Rust behaviour is graded" -claimed-higher = "none — no Grade 2i, 2ii or 1 is claimed" +# Proof Witness Grades, standards 3-practice/PROOF-POLICY.adoc §8 (the +# Mathesis brief's §5/§6 ladder, adopted with corrections). Never a +# percentage. Receipts, lineage and per-row records: docs/theory/PROOF-GRADES.adoc. +grade-3 = "PWG-3: G-1, T-2, T-3, E-1m; PWG-2ii: T-1 (Rocq and Lean legs re-proved and reconciled) — census 4 + 1 of 5 theory theorems (G-3 and T-10 are engineering under PROOF-POLICY §1; T-2 and T-3 are stated over the abstract SingleActiveLog)" +receipt-commit = "see docs/theory/PROOF-GRADES.adoc, The PWG-3 receipt (the 4afb710 and fc188c4 receipts are superseded)" +receipt-prover = "Agda 2.6.4.3 (agda-bin=2.6.4.3-1+b2); no standard library; resource-algebra pinned at cf9235c" +receipt-flags = "--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check (PROOF-POLICY §2.1 canonical, plus two stricter flags)" +not-graded = "the 7 Idris2 PROVEN rows (ABI/interface contracts, PROOF-POLICY §8.1); all 33 TESTED rows (observed behaviour); ASSUMED/DESIGNED/OPEN rows" +open-obligations = "Rocq and Lean legs for the four PWG-3 rows (PROOF-POLICY §2); one Agda version across CI (agda-proofs pins 2.6.4.3, dashboard-check installs 2.6.3); no Creusot or Verus proof on the Rust, so no Rust behaviour is proved" +claimed-higher = "PWG-2ii for T-1 only (Rocq and Lean legs re-proved and reconciled); no PWG-2i or PWG-1 is claimed" [test-categories-complete] unit = true diff --git a/Justfile b/Justfile index 737427b..ffa2290 100644 --- a/Justfile +++ b/Justfile @@ -92,6 +92,10 @@ test-contracts: test-agda: bash scripts/check-agda.sh +# Rocq and Lean recheck legs of the Agda theorems (PROOF-POLICY §2), no axioms, expected rejections. +test-recheck: + bash scripts/check-recheck.sh + # Idris2 ABI <-> januskey.h <-> ffi/zig agreement (sizes, status codes, enums, symbols); no compiler needed. abi-layout-check: bash scripts/check-abi-layout.sh diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 38a303a..2044d30 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -62,19 +62,23 @@ tables must agree. | C-3 | A transaction containing an obliteration is not all-reversible | PROVEN | `+Layout.obliterateNotReversible+` | C-4 | Replacing a chain entry by one with a different hash breaks the link | PROVEN | `+Proofs.tamperBreaksLink+` | C-5 | Struct sizes 32/16/112 and 8-byte alignment as divisibility (statements about the literals) | PROVEN | `+Layout.{contentHashSize,keyIdSize,oblitProofSize,hashAligned,keyIdAligned,oblitAligned}+` -| G-1 | Reversibility as a Loss grade: lossless traces have only lossless steps; obliteration absorbs; wrap/unwrap is grade 𝟙 given cancellation | PROVEN | `+verification/proofs/agda/Reversibility.agda+` (Agda kernel, resource-algebra pinned at `+cf9235c+`); `+tests/reject-agda/*+` refused; the cancellation premise is the TESTED row `+execute_then_undo_is_identity+` +| G-1 | Reversibility as a Loss grade: lossless traces have only lossless steps; obliteration absorbs; a wrap/unwrap pair carries its cancellation law (its grade 𝟙 is assigned, not derived from that law) | PROVEN | `+verification/proofs/agda/Reversibility.agda+` (Agda kernel, resource-algebra pinned at `+cf9235c+`); `+tests/reject-agda/*+` refused; the cancellation premise is the TESTED row `+execute_then_undo_is_identity+` | G-2 | The Idris2 `+IsCNO+`/`+ReversibleOp+` pair corresponds to Agda `+ReversiblePair+` (by transcription) | ASSUMED | no mechanical link claimed | 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; the *model-level* half is now proved in Agda as row E-1m (#145 item 3) +| E-1m | In a world model, an adversary whose observation excludes the store does not know what it holds; obliteration leaves nothing to recover; rotation to a different key leaves no agent able to use the old one (premise `+old ≠ new+`; true by the definition of `+rotate+` in the model; that an unusable key cannot decrypt is X-1) | PROVEN | `+verification/proofs/agda/Epistemic.agda+`; `+tests/reject-agda/{AdversaryKnows,OldKeyStillUsable}.agda+` refused | 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-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+`; rechecked in Rocq and Lean (`+verification/proofs/{rocq,lean}/Rollback+`, `+PWG-2ii+`); `+tests/reject-agda/ForwardRollback.agda+` refused +| T-2 | In any single-active log (records with a decidable key and an active or settled phase), opening a fresh active record, a key- and phase-preserving edit, and a settling transition each preserve the invariant and rewrite only the active record, so a settled one is never modified | PROVEN | `+SingleActiveLog.{begin-good,modify-good,finish-good,update-active}+`; `+tests/reject-agda/SettleWithoutSettling.agda+` refused; januskey's instance is `+TransactionAtomicity.lifecycle-preserves-good+`; `+tests/reject-agda/CommitWhenIdle.agda+` refused +| T-3 | In any single-active log satisfying the invariant, at most one record is active, and exactly one when the pointer is set | PROVEN | `+SingleActiveLog.at-most-one-active+` (januskey's transactions are an instance) | T-4 | A rollback that fails part-way can be retried to completion | TESTED | `+rollback_resume_test+` drives the real `+jk+`: after one undo error and a repair, `+jk rollback+` skips the already undone operation and finishes (before the fix the retry stopped at it every time, reproduced 2026-10-26); fixed in `+cmd_rollback+` -| T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by write, fsync and rename (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins) +| T-5 | The transaction log is never left disagreeing with memory by a failed save, and is replaced by rename rather than overwritten in place, with an fsync before the rename by construction (no test observes the fsync) (a randomly named temporary file opened with the old file's mode, removed only if this save created it) rather than overwritten in place | TESTED | `+transaction::tests::failed_save_*+`: a save that fails at the final step leaves begin, add_operation, commit and rollback unapplied in memory; mutants (memory first, plain `+fs::write+`, no temp cleanup, shared temp name, truncating open, no permission copy) each fail a test. Not claimed: crash-safety of the rename itself is by construction, not crash-injected; the directory fsync is best effort, because failing the save after the rename would leave disk new and memory old; concurrent writers are out of scope (each save's content is intact, the last rename wins) | 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-8 | The operation metadata log is replaced by rename, never overwritten in place (the sync before the rename is there by construction; no test observes it); a log edit (`+mark_undone+`, `+prune+`, `+purge_path_entries+`) whose save fails is not applied in memory and applies exactly once on retry; an append whose save fails keeps its record for the next save | TESTED | `+metadata::tests::{failed_save_leaves_every_mutation_unapplied,a_failed_append_keeps_its_record_for_the_next_save,save_replaces_the_log_atomically,save_replaces_rather_than_overwrites_the_log}+` and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+`, each checked against a mutant in #168. Not claimed: a failure after the temporary file exists (during the write, sync or rename) is not injected; the rename's atomicity is the filesystem's guarantee +| T-9 | A forward file change is never left without a log record: `+execute_*+` changes the filesystem and then appends, so a crash or failed save between the two leaves a change the log does not know about | OPEN | needs a write-ahead intent record (a design decision); split out of T-8 in #168 +| T-11 | An undo whose `+mark_undone+` fails to persist can be retried safely: `+undo+` records the inverse as its own operation (each helper calls `+execute+`), then marks the original, so a failed mark leaves the original unmarked and a retry re-applies the inverse or fails against the changed filesystem | OPEN | the inverse is recorded, unlike T-9; the fix is an idempotent undo (find the existing inverse record before re-applying), not write-ahead intent +| T-10 | januskey's TransactionManager is an instance of the single-active log: the Rust begin, add_operation, commit and mark_rolled_back refine the abstract open, edit and settle transitions, as the hand-written instance in `+TransactionAtomicity.agda+` Part B assumes | OPEN | engineering (PROOF-POLICY §1): Creusot/Pearlite or Verus contracts on `+crates/reversible-core/src/transaction.rs+`; the instance itself is a transcription, like G-2 | 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) @@ -139,6 +143,13 @@ name and reported) and the superseded receipts (runs 41687715055 at link:docs/theory/PROOF-GRADES.adoc[`+docs/theory/PROOF-GRADES.adoc+`]. Correspondence state for them: `+AGDA-VERIFIED+`. +*PWG census, theory theorems of this repository (denominator 5):* `+PWG-3+` 4 +(G-1, T-2, T-3, E-1m) · `+PWG-2i+` 0 · `+PWG-2ii+` 1 (T-1) · `+PWG-1+` 0 · +`+ungraded+` 0. G-3 names this repository's FFI bridge, so PROOF-POLICY §1 +classes it as engineering and it is outside the ladder. T-1's Rocq and Lean legs are re-proved and reconciled +(`+docs/theory/PROOF-GRADES.adoc+`, §T-1); the other four have not been +attempted, and each still owes both (§8.4: a grade is not a discharge). + The other seven PROVEN rows — A-1, A-2, C-1 to C-5 — are Idris2 theorems. Under PROOF-POLICY §1 those are interface and ABI contracts, so the theory ladder does not grade them: they are PROVEN in the vocabulary above and nothing more. The @@ -148,8 +159,8 @@ contracts, and **Verus** (PROOF-POLICY §1.2, owner ruling 2026-11-07; not SPARK and not Idris2); neither verifier has a contract or proof in this tree yet, which is why no Rust row is proved. -No row of this ledger is `+PWG-2i+`, `+PWG-2ii+` or `+PWG-1+`, and none is claimed to -be. The row-by-row mapping and the receipt in full are in +Only T-1 is above `+PWG-3+`: it is `+PWG-2ii+`, with Rocq and Lean legs re-proved +and reconciled. No row is `+PWG-2i+` or `+PWG-1+`, and none is claimed to be. The row-by-row mapping and the receipt in full are in `+docs/theory/PROOF-GRADES.adoc+`. Since 2026-11-01 the gate runs PROOF-POLICY §2.1's canonical invocation (`+--safe --without-K --cubical-compatible …+`); the CI receipt for that flag @@ -194,7 +205,7 @@ attestations undermine trust |Content store integrity |Content-addressed storage never returns wrong content (paths confined to the store and damaged blobs repaired: S-1 and S-2 are TESTED; the write is atomic by construction, not by test; reads verify the hash) |Hash collisions or bugs corrupt stored data -|Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the Rust is tested for partial-rollback retry, T-4, and failed saves, T-5; the premises T-6 and T-7 are assumed; the metadata log is tested for atomic and failed saves, T-8; a file change whose log record fails to persist is OPEN, T-9) +|Transaction atomicity |Delta application is atomic and reversible (the model is proved, T-1 to T-3; the Rust is tested for partial-rollback retry, T-4, and failed saves, T-5; the premises T-6 and T-7 are assumed; the metadata log is tested for atomic and failed saves, T-8; a forward file change whose log record fails to persist is OPEN, T-9, and so is an undo whose mark fails to persist, T-11) |Partial transactions corrupt state |reversible-core |Undo/redo preserves data integrity |Core crate used by @@ -238,8 +249,8 @@ the status table above. |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` +|T-2: In any single-active log, opening a fresh active record, a key- and phase-preserving edit, and a settling transition each preserve the invariant and rewrite only the active record |PROVEN |`verification/proofs/agda/SingleActiveLog.agda::finish-good` |`bash scripts/check-agda.sh` +|T-3: In any single-active log satisfying the invariant, at most one record is active, and exactly one when the pointer is set |PROVEN |`verification/proofs/agda/SingleActiveLog.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` @@ -257,6 +268,11 @@ the status table above. |T-5: A save whose temporary file already exists (another writer's) fails without deleting that file or writing the log |TESTED |`crates/reversible-core/src/transaction.rs::a_save_never_removes_a_temporary_file_it_did_not_create` |`cargo test --locked -p reversible-core --lib a_save_never_removes_a_temporary_file_it_did_not_create` |T-5: The temporary file has the log's permissions from creation, before any content is written |TESTED |`crates/reversible-core/src/transaction.rs::the_temporary_file_is_restricted_before_any_content_is_written` |`cargo test --locked -p reversible-core --lib the_temporary_file_is_restricted_before_any_content_is_written` |T-5: The temporary file is opened with the log's mode, so it is never more readable than the log at any instant, not only after a later chmod (checked where the umask leaves owner read-write, the usual 022) |TESTED |`crates/reversible-core/src/transaction.rs::the_temporary_file_is_opened_with_the_logs_mode` |`cargo test --locked -p reversible-core --lib the_temporary_file_is_opened_with_the_logs_mode` +|T-8: A metadata-log edit (mark_undone, prune, purge) whose save fails is not applied in memory, and each retry applies it exactly once |TESTED |`crates/reversible-core/src/metadata.rs::failed_save_leaves_every_mutation_unapplied` |`cargo test --locked -p reversible-core --lib failed_save_leaves_every_mutation_unapplied` +|T-8: An append whose save fails keeps its record in memory, and the next successful save persists it exactly once |TESTED |`crates/reversible-core/src/metadata.rs::a_failed_append_keeps_its_record_for_the_next_save` |`cargo test --locked -p reversible-core --lib a_failed_append_keeps_its_record_for_the_next_save` +|T-8: A metadata-log save replaces the log by rename, leaves no temporary file, and ignores a stale temporary file from an earlier crash |TESTED |`crates/reversible-core/src/metadata.rs::save_replaces_the_log_atomically` |`cargo test --locked -p reversible-core --lib save_replaces_the_log_atomically` +|T-8: A metadata-log save replaces the log rather than overwriting it in place (a hard link to the old log keeps the old bytes) |TESTED |`crates/reversible-core/src/metadata.rs::save_replaces_rather_than_overwrites_the_log` |`cargo test --locked -p reversible-core --lib metadata::tests::save_replaces_rather_than_overwrites_the_log` +|T-8: A save that fails before its temporary file exists leaves the old log's bytes intact |TESTED |`crates/reversible-core/src/transaction.rs::a_failed_save_leaves_the_existing_log_intact` |`cargo test --locked -p reversible-core --lib a_failed_save_leaves_the_existing_log_intact` |S-1: A malformed content hash never resolves to a path outside the store root |TESTED |`crates/reversible-core/src/content_store.rs::malformed_hash_never_leaves_the_store_root` |`cargo test --locked -p reversible-core --lib malformed_hash_never_leaves_the_store_root` |S-1: A well-formed content hash keeps the existing two-level blob layout |TESTED |`crates/reversible-core/src/content_store.rs::well_formed_hash_keeps_the_existing_layout` |`cargo test --locked -p reversible-core --lib well_formed_hash_keeps_the_existing_layout` |S-2: Storing content again repairs a blob a crash left truncated |TESTED |`crates/reversible-core/src/content_store.rs::store_repairs_a_blob_truncated_by_a_crash` |`cargo test --locked -p reversible-core --lib store_repairs_a_blob_truncated_by_a_crash` @@ -265,12 +281,14 @@ the status table above. |X-1: Hash one-wayness and physical erasure (cryptographic and physical assumptions) |ASSUMED |`src/abi/JanusKey/ABI/Proofs.idr` |- |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` |- -|E-1m: In a world model, an adversary whose observation excludes the store does not know what it holds (adversary-ignorant), obliteration leaves nothing to recover (obliterate-cuts-recovery, obliterate-ignorance), and rotation leaves no agent — the system included — able to use the old key (rotate-forgets-old); the fixtures AdversaryKnows and OldKeyStillUsable are refused |PROVEN |`verification/proofs/agda/Epistemic.agda::adversary-ignorant` |`bash scripts/check-agda.sh` +|E-1m: In a world model, an adversary whose observation excludes the store does not know what it holds (adversary-ignorant), obliteration leaves nothing to recover (obliterate-cuts-recovery, obliterate-ignorance), and rotation to a different key leaves no agent — the system included — able to use the old one (rotate-forgets-old, premise old ≠ new); the fixtures AdversaryKnows and OldKeyStillUsable are refused |PROVEN |`verification/proofs/agda/Epistemic.agda::adversary-ignorant` |`bash scripts/check-agda.sh` |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` |- |L-1: Editing any field of any audit-log entry makes verify_integrity fail (false today: audit probes P1, P2) |OPEN |`crates/januskey-cli/src/attestation.rs` |- |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 forward file change is never left without a log record (execute changes the filesystem, then appends; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- +|T-11: An undo whose mark_undone fails to persist can be retried safely (the inverse is recorded as its own operation before the mark; needs an idempotent undo) |OPEN |`crates/januskey-cli/src/operations.rs` |- +|T-10: januskey's TransactionManager refines the single-active log (Rust begin, add_operation, commit, mark_rolled_back against the abstract transitions; engineering, for Creusot or Verus) |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` |- @@ -294,7 +312,7 @@ be systematically replaced with proven error handling. *HIGH* — reversibility is the product, and its exceptions are destructive: obliteration destroys data on purpose, and the operation log is the only thing -that makes undo possible (row T-9 is open). Any correctness bug in either is a +that makes undo possible (rows T-9 and T-11 are open). Any correctness bug in either is a critical vulnerability. The ABI layer now typechecks, but none of the security obligations above is proved. diff --git a/READINESS.adoc b/READINESS.adoc index ef390ea..10dec90 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -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:* 141 tests + 5 benchmark groups; 12 proofs checked (PROVEN ledger rows; five are theory theorems under PROOF-POLICY §8: four at PWG-3 and T-1 at PWG-2ii — see `docs/theory/PROOF-GRADES.adoc`) *Total missing:* Fuzz, mutation, chaos, compatibility === Aspect Matrix diff --git a/docs/estate/prompts/2026-11-01-mathesis-grade3-receipts.md b/docs/estate/prompts/2026-11-01-mathesis-grade3-receipts.md index c7c10be..496076e 100644 --- a/docs/estate/prompts/2026-11-01-mathesis-grade3-receipts.md +++ b/docs/estate/prompts/2026-11-01-mathesis-grade3-receipts.md @@ -1,5 +1,17 @@ # Paste-ready prompt — `hyperpolymath/mathesis` (`estate-mathematical-architecture`) +> **Status (2026-11-09): mostly answered; do not send as written.** The owner +> adopted the ladder as Proof Witness Grades in standards +> `3-practice/PROOF-POLICY.adoc` §8 (2026-11-04, standards#1410), which now +> governs over the Mathesis brief. Question 1: a `PWG-3` receipt records the +> Agda version, standard-library pin, flags and import cone (§8.2), and +> receipts of execution come from CI (§2.3). Question 3: a receipt that is no +> longer current carries `state: superseded` with a reason, and a grade is never +> carried forward from an older commit (§8.4). Question 2 (where a non-axiom +> caveat such as `UnsupportedIndexedMatch` is recorded) is still open; §8.4.6 +> covers axioms only. januskey records it as a separate "Caveat" line on the +> receipt (`docs/theory/PROOF-GRADES.adoc`). + Scope: **this repo only.** Do not edit `januskey`. Latest stable versions only (Agda 2.8.0.2; Rocq/Lean only if §2's transport work is in scope). diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index c9039dc..92a2445 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -1,4 +1,4 @@ -= Proof grades under mathesis and PROOF-POLICY += Proof Witness Grades (PROOF-POLICY §8) :toc: preamble :icons: font @@ -10,6 +10,26 @@ to reconstruct: *which of these claims is a proof, and how good a proof is it?* It grades nothing by confidence. There is no percentage anywhere in this repository, and none is introduced here. +[NOTE] +==== +*PWG census, theory theorems of this repository (denominator 5):* +`PWG-3` 4 (G-1, T-2, T-3, E-1m) · `PWG-2i` 0 · `PWG-2ii` 1 (T-1) · `PWG-1` 0 · +`ungraded` 0. `+foundation-diverse`: none. Axioms: none. + +The denominator is the ledger rows whose source of truth is an Agda theorem. +PROOF-POLICY §1 puts a statement that names one repository's type, function or +wire format in engineering, so these rows are outside it: G-3 (the FFI bridge +preserves grade 𝟙, `OPEN`), E-1 (a security property of the implementation; its +model half is E-1m), the MPR row (a refinement claim about Rust, which §1 sends +to Creusot and Verus) and G-2 (a bridge, `ASSUMED`). By the same test, T-2 +and T-3 used to be stated over a hand-transcribed model of this repository's +`TransactionManager`. On the owner's ruling of 2026-11-09 they were split. The +theorems now live in `SingleActiveLog.agda`, over any record type with a key and +an active or settled phase: theory, in the census. The claim that januskey's +Rust refines that log is the new engineering row T-10 (`OPEN`, for Creusot or +Verus). +==== + == What governs the grades Since the owner ruling of 2026-11-04, `PROOF-POLICY.adoc` §8 is normative for @@ -142,6 +162,19 @@ pending re-run. propositions, and are kept visible |=== +*The comment edits of hyperpolymath/januskey#171 (2026-11-09) are covered by +the same re-run.* #171 edits the explanatory comments of `Reversibility.agda` +and `TransactionAtomicity.agda`: the "What is NOT claimed" block named failure +modes since fixed by T-4, T-5 and T-8, and a G-1 comment implied that the grade +was derived from the cancellation law. No statement or proof term changed, but +the bytes did, so the receipt above does not cover them either. #171 also adds a fourth root, `SingleActiveLog.agda` (the T-2/T-3 split), so +the cone the next receipt records has seven first-party modules, not six. The first green +`agda-proofs.yml` run on `main` after both pull requests is the receipt for the +new gate and the new bytes together. On the branch the same gate passed on each +revision of the comments (for example run +https://github.com/hyperpolymath/januskey/actions/runs/42623188471[42623188471] +at `a71dc76`; branch evidence, not a receipt). + Earlier receipts, kept with their lineage (§8.4): [cols="1,1,3",options="header"] @@ -159,16 +192,18 @@ Earlier receipts, kept with their lineage (§8.4): Those are the `PWG-3` facts: the propositions type-check in Agda under the §2.1 invocation, in CI, at a named commit, with the prover version pinned and the import cone recorded; the receipt is re-earned by the first run of the -changed gate, as above. Nothing here has been translated to Rocq or Lean, so no -recheck leg counts and the grade is not `PWG-2i`; no witness in another -foundation exists, so `foundation_diverse` is false. +changed gate, as above. For G-1, T-2, T-3 and E-1m no Rocq or Lean leg exists, so +no recheck leg counts and their grade is `PWG-3`. T-1 has both legs and is +`PWG-2ii` (§T-1 below). No witness in another foundation exists, so +`foundation_diverse` is false throughout. -=== Why it stops at PWG-3 +=== Why four rows stop at PWG-3 -PWG-2i and above would require an Agda → Dedukti → Rocq/Lean transport or a +PWG-2i and above require an Agda → Dedukti → Rocq/Lean transport or a re-proof, with the outcome recorded as `transported`, `re-proved` or -`unavailable` (PROOF-POLICY §2). That work has not been done, is not claimed, -and would not change what these modules prove: §2.2 is explicit that compiling +`unavailable` (PROOF-POLICY §2). For T-1 that work is done (§T-1 below, now +`PWG-2ii`); for G-1, T-2, T-3 and E-1m it has not been done and is not +claimed. A recheck would not change what these modules prove: §2.2 is explicit that compiling in a second prover does not establish the same proposition unless the correspondence is checked too. @@ -256,22 +291,205 @@ repeated the counts, and the two copies drifted apart. | Row | Proposition | Theorem | G-1 | A lossless trace has only lossless steps; an obliterating step absorbs; - wrap/unwrap is grade 𝟙 given cancellation | `Reversibility.agda::lossless-trace-all`, - `obliterate-absorbs`, `wrap-unwrap-id` + a wrap/unwrap pair carries its cancellation law. The pair's grade 𝟙 is + *assigned* by `wrapStep`/`unwrapStep`, not derived from that law: + `wrap-unwrap-𝟙` holds by definition and does not use `cancels` | + `Reversibility.agda::lossless-trace-all`, `obliterate-absorbs`, + `wrap-unwrap-id` | T-1 | Undoing a fully executed transaction in reverse order restores the state it began in, given each step's undo restores its execute | `TransactionAtomicity.agda::rollback-restores` -| T-2 | The four lifecycle transitions preserve the log invariant and rewrite - only the Active transaction | `TransactionAtomicity.agda::lifecycle-preserves-good` -| T-3 | At most one transaction is Active, exactly one when the pointer is set | - `TransactionAtomicity.agda::at-most-one-active` +| T-2 | In any single-active log, opening a fresh active record, a key- and + phase-preserving edit, and a settling transition each preserve the invariant + and rewrite only the active record | + `SingleActiveLog.agda::begin-good`, `modify-good`, `finish-good`, + `update-active` (januskey's instance: `TransactionAtomicity.agda::lifecycle-preserves-good`) +| T-3 | In any single-active log satisfying the invariant, at most one record is + active, and exactly one when the pointer is set | + `SingleActiveLog.agda::at-most-one-active` | E-1m | In a world model, an agent whose observation excludes the store does not know what the store holds; obliteration leaves nothing to recover; rotation - leaves no agent — the system included — able to use the old key | + to a different key (premise `old ≠ new`) leaves no agent — the system included + — able to use the old one (true by the definition of `rotate` in the model) | `Epistemic.agda::adversary-ignorant`, `obliterate-cuts-recovery`, `obliterate-ignorance`, `rotate-forgets-old` |=== +==== Leg records (PROOF-POLICY §8.5) + +The same record holds for each of G-1, T-2, T-3 and E-1m, so it is given once. +`pwg: 3`, `foundation_diverse: false`. T-1 has its own record below +(§T-1: the first recheck legs). + +[cols="1,1,1,1,3",options="header"] +|=== +| Leg | Route | §5 token | §2.2 state | Receipts + +| Agda (source) +| source of truth +| `PROVEN` +| `AGDA-VERIFIED` +| §The PWG-3 receipt above, with its lineage + +| Rocq +| none: not attempted +| `OPEN` +| none: no target statement exists to compare +| none + +| Lean +| none: not attempted +| `OPEN` +| none: no target statement exists to compare +| none +|=== + +§8.5's route values (`transported`, `re-proved`, `waived`, `unavailable`) each +describe a leg that was tried, excused or found impossible. None applies to a +leg nobody has started, so the route field says that instead of borrowing one. +When a leg is started, its row gets the route, the target statement, the +comparison with the Agda statement and its receipts, and the PWG is recomputed. + +==== T-1: the first recheck legs (2026-11-09) + +T-1 is the pilot for PROOF-POLICY §2, chosen because its statement is small and +abstract. Its Agda module imports `ResourceAlgebra.Prelude` from the pinned +sibling, but the `Rollback` part uses only three things from it: `_≡_` (Agda's +builtin equality, re-exported) and the elementary `trans` and `cong`. Those are +accounted for in the comparison below. `pwg: 2ii`, `foundation_diverse: +false`. + +[cols="1,1,1,1,3",options="header"] +|=== +| Leg | Route | §5 token | §2.2 state | Receipts + +| Agda (source) +| source of truth +| `PROVEN` +| `AGDA-VERIFIED` +| §The PWG-3 receipt above + +| Rocq +| `re-proved` +| `PROVEN` +| `RECONCILED` +| `agda-proofs.yml` job "Rocq and Lean recheck legs", on this change and then + on `main` + +| Lean +| `re-proved` +| `PROVEN` +| `RECONCILED` +| the same job +|=== + +*Why re-proved.* §2 asks for transport first. The Agda → Dedukti translator +(`Deducteam/Agda2Dedukti`, last changed 2022-01-24 at `c7c7d67`) builds against +a forked Agda branch of that period and its documentation pins Lambdapi 2.1.0. +It cannot read modules checked by the pinned Agda 2.6.4.3, so no transport +route exists for this toolchain. For Lean, §2 already says to re-prove until a +released Lambdapi has a Lean exporter. Both legs are therefore re-proved by +hand, in each prover's core library: no Mathlib, no imports in the Lean file, +only the prelude in the Rocq file. + +*The statements, side by side.* + +[cols="1,3",options="header"] +|=== +| Prover | Proposition + +| Agda (`TransactionAtomicity.agda`, module `Rollback (S : Set)`) +| `rollback-restores : ∀ {os x z} → Executed os x z → rollback os z ≡ x` + +| Rocq (`verification/proofs/rocq/Rollback.v`) +| `rollback_restores : forall (S : Type) (os : list (Op S)) (x z : S), + Executed os x z -> rollback os z = x` + +| Lean (`verification/proofs/lean/Rollback.lean`) +| `rollback_restores {S : Type} {os : List (Op S)} {x z : S} : + Executed os x z → rollback os z = x` +|=== + +*How the comparison was made.* By reading, definition by definition. It was not +done by a round trip, since no translator exists. + +* `Op`: a record of `execute : S → Maybe S`, `undo : S → S` and + `undoes : execute x ≡ just y → undo y ≡ x`. The targets have the same three + fields over `option`/`Option`. Agda binds `x` and `y` implicitly and Rocq + explicitly, which is the same proposition. +* `Executed`: an inductive family in `Set` with constructors `done` and `next`. + The targets put it in `Type`, the same universe level, with the same two + constructors and the same indices. +* `rollback`: the same structural recursion on the list, undoing the head after + the tail. +* The source type `S` is a parameter in `Set` in all three (`Type` at level 0). +* Builtins: Agda's `List`/`Maybe` and the targets' `list`/`option` and + `List`/`Option` are the same free inductive types. +* The sibling's prelude: `_≡_` is `Agda.Builtin.Equality` re-exported, and + `trans` and `cong` are the usual one-clause definitions by pattern matching on + `refl`. Rocq's `eq` with `eq_trans`/`f_equal`, and Lean's `Eq` with + `Eq.trans`/`congrArg`, are the same inductive equality and the same + eliminations. The re-proofs use `rewrite` instead, which needs nothing beyond + the equality type. No other sibling definition reaches T-1's statement or + proof. + +*Residual differences, listed rather than hidden.* The logics differ in +what they add to equality. Axiom-free Rocq has neither K nor uniqueness of +identity proofs, like Agda under `--without-K`, and `Print Assumptions` confirms +that this leg adds no axiom that would supply them. Lean is stronger: its `Eq` +lives in a proof-irrelevant `Prop`, so it has uniqueness of identity proofs +definitionally. Neither proof uses these: each is the same +induction on `Executed`, a rewrite with the induction hypothesis and one use of +`undoes`. Proving the statement in a stronger logic adds no assumption to the +Agda source. + +*Axioms.* Rocq `Print Assumptions rollback_restores` reports "Closed under the +global context". Lean `#print axioms` reports that it "does not depend on any +axioms". The gate (`scripts/check-recheck.sh`) fails if either line is missing: +a mutant with `Admitted` in Rocq and one with `sorry` in Lean were each caught. + +*Non-vacuity.* `tests/reject-rocq/ForwardRollback.v` and +`tests/reject-lean/ForwardRollback.lean` are twins of +`tests/reject-agda/ForwardRollback.agda`. They build real double and increment +operations against the leg's own definitions and claim that undoing them in +execution order restores the start. Rocq refuses with `Unable to unify "1" with +"0"`, and Lean with "`decide` proved that the proposition … is false". The gate +checks each refusal message. + +*Pins and inputs.* + +[cols="1,3",options="header"] +|=== +| Field | Value + +| Rocq | The Coq Proof Assistant 8.18.0, Ubuntu `coq=8.18.0+dfsg-1build2` on the + `ubuntu-24.04` runner, asserted by version string. `coqc -q -Q . JanusKey`. +| Lean | Lean 4.35.0 (commit `eb6cafb7290e8bd5f2937522d8d804f58f02bafc`), the + release tarball `lean-4.35.0-linux.tar.zst`, SHA-256 + `7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d`, checked + before unpacking. `lean -o .olean `. +| Inputs (SHA-256) | `Rollback.v` + `662d51bf0b642ac28f816853c7d2c6a851583487a15e9f79c3b8184a53ff28e2`, + `Rollback.lean` + `808c32585ad582fced7497b93607668f92d9140b36ae4bd90b14f6b26bcd36c6`, the Rocq + fixture `4b2c01d4f70d1b60080babdf64aeaf873ec4db98c4682a6694e1981127160410`, + the Lean fixture + `813cae57494bee9c6457a63553489d83ad47c2ac538c18a0de8e86956cc477ee`, + `check-recheck.sh` + `5171d9d27a888e79dc9544f7b84d2a3557428c918a25194f9a88bcb2944f8483` +| Observed | Locally, with the same two versions: both legs check with no + axioms, both fixtures refused as named, `[check-recheck] OK`. The CI job on + this change is the receipt. +|=== + +The pilot answers the question the pilot was for. The transport route is not +available for any of the five theorems, for the reason above. A hand re-proof +in core Rocq and core Lean costs about forty lines per statement. The remaining +four take the same route. G-1 needs the Loss grade algebra restated, since the +targets cannot import `resource-algebra`. T-2 and T-3 are now stated over the abstract +log in `SingleActiveLog.agda`, built from builtins only, so their legs can +restate it directly. + These five are the only rows in this repository with a Proof Witness Grade (PWG). Each rests on a premise it names rather than assumes silently — the per-step cancellation law (`undoes`, TESTED as `execute_then_undo_is_identity`), the @@ -319,7 +537,7 @@ observed, never that it always holds. G-2 (the Idris2 ↔ Agda correspondence) i other, and where both cover it the correspondence is recorded. Not Idris2 and not Agda. -| T-6, T-7, X-1, G-2, E-1, G-3 (`ASSUMED` / `OPEN`) +| T-6, T-7, X-1, G-2, E-1, G-3 (`ASSUMED` / `OPEN`; G-3 is engineering under §1) | Premises, external assumptions, or filed obligations. | Each names its own gap in `PROOF-NEEDS.adoc`; none may be counted as proved by the grade of a neighbouring row (README-EXPLAINME: "a row is only as @@ -329,11 +547,15 @@ observed, never that it always holds. G-2 (the Idris2 ↔ Agda correspondence) i | Downstream consumption designed, never exercised. | A dependency edge in the consumer's manifest and a green test there. -| T-8 (`OPEN`) -| The metadata log now saves through the same write → sync → rename path as the - transaction log, but the crate has not been built since that change. -| The new test `metadata::tests::save_replaces_the_log_atomically` green in CI. - Its half of the row — retry after a failed `mark_undone` — is untouched. +| T-9 and T-11 (`OPEN`) +| Two different windows. T-9: `execute_*` changes the filesystem and then + appends, so a crash between them leaves a change with no record. T-11: + `undo` records the inverse as its own operation and then marks the original, + so a failed mark leaves the original unmarked and a retry re-applies the + inverse. (T-8, the metadata log's own saves, is TESTED since #168.) +| T-9: a write-ahead intent record, which is a design decision. T-11: an + idempotent undo that finds the existing inverse record before re-applying. + Each then needs a test that injects the failure between its two steps. |=== == The epistemic rewrite: E-1 becomes E-1m @@ -364,7 +586,9 @@ ignorance is a proposition. Knowledge is indiscriminability over an observation (`obliterate-ignorance`); * rotation is an update to a `usable` predicate, so "no agent can use the old key" is a theorem with a Bool on the right (`rotate-forgets-old`), and the - deleted Idris lemma now has a proved counterpart. + deleted Idris lemma now has a proved counterpart. It follows from the + definition of `rotate`; its content is that the statement is now + *expressible*, which the Idris modality could not manage, not that it is deep. Two fixtures pin the refusals: `AdversaryKnows.agda` (asserting the two stores are identical — refused, `2 != 1`) and `OldKeyStillUsable.agda` (asserting the @@ -391,5 +615,11 @@ PROOF-POLICY §1 and the ABI belongs in Idris2. and neither receipt is deleted from the history. * `AGDA-PENDING` is the correct correspondence state for a module committed but not yet checked. No row in this repository is in that state today: the five - graded rows are `AGDA-VERIFIED` at the commit above, and their Rocq and Lean - legs are `unavailable`, so the grade is `PWG-3`. + graded rows are `AGDA-VERIFIED` at the commit above. Except for T-1, whose + legs are re-proved and reconciled, their Rocq and Lean legs have not been + attempted, so each is `OPEN` with no route and no §2.2 record, + and the grade is `PWG-3`. They are not `unavailable`: under §2 that route + means a leg that cannot be built, and a hand re-proof is always available as + the fallback, so the legs are owed, not excused (§8.4.1). +* Grade counts appear only as the census at the top of this page: a count per + rung, with the denominator and the `ungraded` rung in the same line. diff --git a/docs/wiki/theory/rmr-primitive.md b/docs/wiki/theory/rmr-primitive.md index 2d425e6..26656b0 100644 --- a/docs/wiki/theory/rmr-primitive.md +++ b/docs/wiki/theory/rmr-primitive.md @@ -78,8 +78,8 @@ statement about bytes on a device. |---|---| | Commit/rollback settle a group of operations | yes — `TransactionManager`, states `Active`/`Committed`/`RolledBack`; at most one active (T-3, PROVEN) | | A rollback that fails part-way can be retried | yes (T-4, TESTED — `rollback_resume_test`, driving the real `jk`) | -| A failed save leaves memory and disk agreeing | yes for the transaction log (T-5, TESTED, write→fsync→rename with permission preservation) | -| The **operation metadata** log has the same guarantee | **unverified** — `MetadataStore::save` now calls `crate::transaction::write_atomic` (write → sync → rename), but that edit has not been built or run (T-8, **OPEN**); an undo whose `mark_undone` fails to persist still leaves the file undone and the log unchanged | +| A failed save leaves memory and disk agreeing | yes for the transaction log (T-5, TESTED: replaced by rename, never overwritten in place, with permission preservation; the fsync before the rename is by construction, not tested) | +| The **operation metadata** log has the same guarantee | yes for the log itself (T-8, TESTED): an edit whose save fails is not applied and applies exactly once on retry, and an append whose save fails keeps its record for the next save. **Not** for the file change it records: `execute_*` changes the filesystem before appending, so a crash between the two leaves a change the log does not know about (T-9, **OPEN**). An undo is recorded as its own operation before `mark_undone`, so a failed mark leaves the original unmarked and a retry re-applies the inverse (T-11, **OPEN**) | | A failed execute leaves the filesystem unchanged | assumed, not checked (T-6) | | Intermediate states are invisible to other processes | **false** — operations are applied to the filesystem one at a time as they are executed. A transaction gives you a recorded, resumable rollback, not isolation. Nothing in this tool locks, stages, or hides the working tree | @@ -144,7 +144,7 @@ fn execute(op: Operation) -> Result<()> { Ordering note, because this is where the guarantee is thinnest: in `execute_delete` the content is stored **before** the unlink and the metadata is appended **after** it (`operations.rs`). A crash between the unlink and the -append loses the ability to undo that delete. T-6 and T-8 are the ledger rows +append loses the ability to undo that delete. T-6 and T-9 are the ledger rows that would have to close to remove that window. ### Phase 5: Reversal @@ -155,7 +155,7 @@ fn undo(operation_id: &str) -> Result<()> { let content = content_store.retrieve(&metadata.content_hash)?; let inverse = construct_inverse(&metadata, content); inverse.perform()?; - metadata_store.mark_undone(operation_id)?; // T-8: save atomic since 2026-11-01, unbuilt + metadata_store.mark_undone(operation_id)?; // T-11: after the inverse is recorded (OPEN) Ok(()) } ``` @@ -189,13 +189,16 @@ present one until it exists. What exists, by ledger row: | Row | Statement | Status | |---|---|---| | T-1 | Undoing a fully executed transaction in reverse order restores the state it began in, given each step's undo restores its execute | **PROVEN** (Agda, model) | -| T-2 | The lifecycle preserves the log invariant and rewrites only the Active transaction | **PROVEN** (Agda, model) | -| T-3 | At most one transaction is Active | **PROVEN** (Agda, model) | +| T-2 | In any single-active log, the transitions preserve the invariant and rewrite only the active record (januskey's transactions are an instance) | **PROVEN** (Agda, abstract) | +| T-3 | In any single-active log, at most one record is active | **PROVEN** (Agda, abstract) | | T-4 | A partially failed rollback can be retried to completion | **TESTED** | -| T-5 | The transaction log is replaced atomically, with permissions preserved | **TESTED** | +| T-5 | A failed transaction-log save leaves memory unchanged; the log is replaced by rename with permissions preserved (fsync by construction) | **TESTED** | | T-6 | A failed execute leaves the filesystem unchanged; each undo restores its execute's pre-state | **ASSUMED** | | T-7 | Transaction ids never collide | **ASSUMED** | -| T-8 | The operation metadata log is saved atomically | **OPEN** — saves by rename since 2026-11-01, not yet built or run | +| T-8 | The operation metadata log is replaced by rename; a failed edit is unapplied and retries once; a failed append keeps its record | **TESTED** | +| T-9 | A forward file change is never left without a log record | **OPEN** — needs a write-ahead intent record | +| T-11 | An undo whose mark fails to persist can be retried safely | **OPEN** — needs an idempotent undo | +| T-10 | The Rust `TransactionManager` refines the abstract single-active log | **OPEN** — engineering, for Creusot or Verus | | — | "Every operation is reversible" as a theorem linked to the Rust | **OPEN** | | G-2 | The Idris2 and Agda presentations correspond | **ASSUMED** — "by transcription, no mechanical link claimed" | @@ -233,7 +236,7 @@ shared-blob rule in [RMO](rmo-primitive.md). impl MetadataStore { pub fn append(&mut self, metadata: OperationMetadata) -> Result<()> { self.log.operations.push(metadata); - self.save()?; // T-8: write→sync→rename, unbuilt + self.save()?; // T-8: rename; a failed save keeps the record Ok(()) } @@ -246,9 +249,10 @@ impl MetadataStore { The transaction log (`TransactionLog::save`) uses the atomic path in `transaction.rs`: a per-save temporary file, mode preservation, fsync and -rename. The operation metadata log now calls the same helper, so the asymmetry -is closed in source and still open in evidence — nothing has built or run the -change, which is why row T-8 stays OPEN. +rename. The operation metadata log calls the same helper, and row T-8 tests it. +The sketch above simplifies the metadata store: an edit is saved before it +becomes the in-memory log, and an append whose save fails keeps its record for +the next save. ## Performance @@ -266,8 +270,11 @@ their results are unbaselined (`READINESS.adoc` §Benchmark Classification). ## Limitations 1. **The store is the whole guarantee.** Lose `.januskey/` and undo is gone. -2. **Metadata consistency is weaker than it looks** — T-8 is open; the - metadata log now saves by rename, but that change is unverified. +2. **Metadata consistency is weaker than it looks.** The log itself saves + safely (T-8, TESTED), but a file change and its log record are not written + together: a crash between them leaves a change the log does not know about + (T-9, OPEN), and an undo whose mark fails can be re-applied on retry (T-11, + OPEN). 3. **Not everything captured is restored** — ownership, mtime and symlink identity are recorded but not applied (§2). 4. **No isolation.** Operations touch the live filesystem as they execute. @@ -279,5 +286,5 @@ their results are unbaselined (`READINESS.adoc` §Benchmark Classification). - [RMO: Obliterative Wipe Primitive](rmo-primitive.md) - [Formal Model of File System State](formal-model.md) -- `../../../PROOF-NEEDS.adoc` — the claims ledger, rows T-1..T-8 +- `../../../PROOF-NEEDS.adoc` — the claims ledger, rows T-1..T-11 - [Architecture](../architecture/index.md) diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index ee1e8b1..b02bd53 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -14,8 +14,9 @@ bash scripts/fetch-siblings.sh # infectious in principle — direct imports must use it too — but Agda 2.6.4.3 # accepts a --without-K sibling on the include path and reports the pattern # matches that will not compute under transports as UnsupportedIndexedMatch -# warnings (14 in Reversibility, 16 in TransactionAtomicity, 2 in Epistemic; the -# sibling's ≤-trans, obliterate-absorbs and just-inj). Those are warnings about +# warnings (14 in Reversibility, 20 in TransactionAtomicity, 2 in Epistemic, 14 +# in SingleActiveLog; among them the sibling's ≤-trans, obliterate-absorbs and +# just-inj). Those are warnings about # computation under transport, not about the propositions, so the gate keeps # them visible rather than silencing them with -WnoUnsupportedIndexedMatch. flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check @@ -24,13 +25,13 @@ flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interface # scan's controls. Removed on exit. work="$(mktemp -d)" trap 'rm -rf -- "$work"' EXIT -modules=(Reversibility TransactionAtomicity Epistemic) +modules=(Reversibility TransactionAtomicity Epistemic SingleActiveLog) for module in "${modules[@]}"; do "$prover" "${flags[@]}" --dependency-graph="$work/$module.dot" "verification/proofs/agda/$module.agda" done # PROOF-POLICY §8.4: a comment-aware postulate scan of the import cone. The cone -# is the module set Agda itself reports for the three roots (Agda.Primitive and +# is the module set Agda itself reports for the roots (Agda.Primitive and # the Agda.Builtin modules included); each module is resolved to its source on # the include path or in Agda's own library, and an unresolved module fails. agda_prim="$("$prover" --print-agda-dir)/lib/prim" diff --git a/scripts/check-recheck.sh b/scripts/check-recheck.sh new file mode 100755 index 0000000..a912a37 --- /dev/null +++ b/scripts/check-recheck.sh @@ -0,0 +1,84 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Recheck legs of the Agda theory theorems (PROOF-POLICY §2): the Rocq files +# under verification/proofs/rocq and the Lean files under +# verification/proofs/lean must check with no axioms, and every fixture under +# tests/reject-rocq and tests/reject-lean must be refused with the message its +# `expect:` line names. Prover versions are asserted by the caller (CI) and +# printed here. ROCQ and LEAN override the binaries. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." +export LC_ALL="${LC_ALL:-C.UTF-8}" +rocq="${ROCQ:-coqc}" +lean="${LEAN:-lean}" +"$rocq" --version | head -1 +"$lean" --version + +work="$(mktemp -d)" +trap 'rm -rf -- "$work"' EXIT +mkdir -p "$work/rocq" "$work/lean" + +shopt -s nullglob +rocq_src=(verification/proofs/rocq/*.v) +lean_src=(verification/proofs/lean/*.lean) +rocq_rej=(tests/reject-rocq/*.v) +lean_rej=(tests/reject-lean/*.lean) +shopt -u nullglob +for set in rocq_src lean_src rocq_rej lean_rej; do + declare -n arr="$set" + [ "${#arr[@]}" -gt 0 ] || { echo "ERROR: no files for $set" >&2; exit 1; } +done + +# Rocq: compile each leg under the JanusKey prefix; `Print Assumptions` at the +# foot of each file must report a closed theorem. +for f in "${rocq_src[@]}"; do + cp -- "$f" "$work/rocq/" +done +for f in "${rocq_src[@]}"; do + name="$(basename -- "$f")" + out="$(cd "$work/rocq" && "$rocq" -q -Q . JanusKey "$name" 2>&1)" || { + printf '%s\n' "$out"; echo "ERROR: $f does not check" >&2; exit 1; } + printf '%s\n' "$out" + grep -q '^Closed under the global context$' <<<"$out" || { + echo "ERROR: $f rests on assumptions (Print Assumptions is not closed)" >&2; exit 1; } + echo "[PASS] rocq leg checks, no assumptions: $f" +done + +# Lean: compile each leg to an .olean so the fixtures can import it; the +# `#print axioms` line must report no axioms. +for f in "${lean_src[@]}"; do + mod="$(basename -- "$f" .lean)" + out="$(LEAN_PATH="$work/lean" "$lean" -o "$work/lean/$mod.olean" "$f" 2>&1)" || { + printf '%s\n' "$out"; echo "ERROR: $f does not check" >&2; exit 1; } + printf '%s\n' "$out" + grep -q 'does not depend on any axioms' <<<"$out" || { + echo "ERROR: $f depends on axioms (or does not print them)" >&2; exit 1; } + echo "[PASS] lean leg checks, no axioms: $f" +done + +# Expected rejections: refused, and refused for the stated reason. +expect_of() { sed -n 's/^.*expect: \(.*\)$/\1/p' "$1" | head -1 | sed 's/ \*)$//'; } +reject() { + local file="$1"; shift + local want; want="$(expect_of "$file")" + [ -n "$want" ] || { echo "ERROR: $file has no 'expect: ' line" >&2; exit 1; } + local log + if log="$("$@" 2>&1)"; then + printf '%s\n' "$log"; echo "ERROR: $file was accepted but must be refused" >&2; exit 1 + fi + grep -qF -- "$want" <<<"$log" || { + printf '%s\n' "$log"; echo "ERROR: $file was refused, but not with '$want'" >&2; exit 1; } + echo "[PASS] refused as expected: $file ($want)" +} +# Fixtures are compiled from a copy in the work directory, so no build output +# (.glob, .aux) lands in the tree. +mkdir -p "$work/reject-rocq" +for f in "${rocq_rej[@]}"; do + cp -- "$f" "$work/reject-rocq/" + reject "$f" "$rocq" -q -Q "$work/rocq" JanusKey "$work/reject-rocq/$(basename -- "$f")" +done +for f in "${lean_rej[@]}"; do + reject "$f" env LEAN_PATH="$work/lean" "$lean" "$f" +done +echo "[check-recheck] OK" diff --git a/tests/reject-agda/SettleWithoutSettling.agda b/tests/reject-agda/SettleWithoutSettling.agda new file mode 100644 index 0000000..3a23b77 --- /dev/null +++ b/tests/reject-agda/SettleWithoutSettling.agda @@ -0,0 +1,40 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection: SingleActiveLog.finish-good needs its settling premise +-- (every finish transition lands in the settled phase). Here the "finish" +-- transition is the identity, so the record it should settle stays active: +-- the log ends with no pointer but one active record. The claim that +-- countActive matches the pointer (0) is false, and the checker must refuse +-- it. This pins that at-most-one-active is not vacuous about the premise. +-- expect: 1 != 0 +module SettleWithoutSettling where + +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Maybe using (Maybe; nothing; just) +open import Agda.Builtin.Nat using (Nat; zero; suc) +open import SingleActiveLog + +-- Records are bare keys, and every record is active. +_≟_ : (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 refl = inl refl +... | inr q = inr (λ { refl → q refl }) + +open Log Nat Nat _≟_ (λ k → k) (λ _ → active) + +-- One record, key 0, active and pointed to; then "finish" with the identity. +after : Maybe Log +after = finish (λ r → r) (log (0 ∷ []) (just 0)) + +count-after : Maybe Nat +count-after with after +... | nothing = nothing +... | just L = just (countActive (txs L)) + +no-active-left : count-after ≡ just 0 +no-active-left = refl diff --git a/tests/reject-lean/ForwardRollback.lean b/tests/reject-lean/ForwardRollback.lean new file mode 100644 index 0000000..94af4d3 --- /dev/null +++ b/tests/reject-lean/ForwardRollback.lean @@ -0,0 +1,35 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection, the Lean twin of tests/reject-agda/ForwardRollback.agda. +-- Two real, individually invertible operations (double, then add one) run +-- from 1 (1 -> 2 -> 3). Undoing them in EXECUTION order 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: is false + +import Rollback + +open JanusKey.Rollback + +def rollbackForward {S : Type} : List (Op S) → S → S + | [], z => z + | o :: os, z => rollbackForward os (o.undo z) + +def doubleOp : Op Nat where + execute x := some (x + x) + undo y := y / 2 + undoes := by + intro x y h + cases h + omega + +def incOp : Op Nat where + execute x := some (x + 1) + undo y := y - 1 + undoes := by + intro x y h + cases h + omega + +-- The correct order is a theorem (rollback_restores); the forward order is not. +example : rollbackForward [doubleOp, incOp] 3 = 1 := by decide diff --git a/tests/reject-rocq/ForwardRollback.v b/tests/reject-rocq/ForwardRollback.v new file mode 100644 index 0000000..277b390 --- /dev/null +++ b/tests/reject-rocq/ForwardRollback.v @@ -0,0 +1,35 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) +(* Expected rejection, the Rocq twin of tests/reject-agda/ForwardRollback.agda. + Two real, individually invertible operations (double, then add one) run + from 1 (1 -> 2 -> 3). Undoing them in EXECUTION order 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: Unable to unify "1" with "0" *) + +From JanusKey Require Import Rollback. +Require Import Arith Lia. + +Fixpoint rollbackForward {S : Type} (os : list (Op S)) (z : S) : S := + match os with + | nil => z + | cons o os' => rollbackForward os' (undo o z) + end. + +Definition doubleOp : Op nat. +Proof. + refine (mkOp (fun x => Some (x + x)) Nat.div2 _). + intros x y H. injection H as <-. + replace (x + x) with (2 * x) by lia. apply Nat.div2_double. +Defined. + +Definition incOp : Op nat. +Proof. + refine (mkOp (fun x => Some (S x)) pred _). + intros x y H. injection H as <-. reflexivity. +Defined. + +(* The correct order is a theorem (rollback_restores); the forward order is not. *) +Example forward_restores : + rollbackForward (cons doubleOp (cons incOp nil)) 3 = 1. +Proof. vm_compute. reflexivity. Qed. diff --git a/verification/proofs/agda/Reversibility.agda b/verification/proofs/agda/Reversibility.agda index 0d30206..d7dd983 100644 --- a/verification/proofs/agda/Reversibility.agda +++ b/verification/proofs/agda/Reversibility.agda @@ -128,8 +128,12 @@ module Steps (S : Set) where ---------------------------------------------------------------------- -- The reversible pair: wrap then unwrap. The cancellation law is the - -- operational premise (execute_then_undo_is_identity, cited above); - -- given it, both steps are graded 𝟙 and the two-step trace is lossless. + -- operational premise (execute_then_undo_is_identity, cited above). + -- Both steps are *assigned* grade 𝟙: wrap-unwrap-𝟙 holds by definition + -- and does not use `cancels`. The kernel-checked link between the pair + -- and its grade is only that a pair carries its cancellation law + -- (wrap-unwrap-id); that the law is why 𝟙 is the right annotation is + -- the informal reading, not a theorem here. ---------------------------------------------------------------------- record ReversiblePair : Set where @@ -150,8 +154,8 @@ module Steps (S : Set) where wrap-unwrap-𝟙 : ∀ p → traceGrade (wrapStep p ∷ unwrapStep p ∷ []) ≡ fin 0 wrap-unwrap-𝟙 p = refl - -- Running the pair really is the identity: the grade annotation above is - -- justified by this, not the other way round. + -- Running the pair really is the identity. This is what the 𝟙 + -- annotation above is meant to record; the kernel does not tie the two. wrap-unwrap-id : ∀ p x → run (unwrapStep p) (run (wrapStep p) x) ≡ x wrap-unwrap-id p x = cancels p x diff --git a/verification/proofs/agda/SingleActiveLog.agda b/verification/proofs/agda/SingleActiveLog.agda new file mode 100644 index 0000000..fe0c47c --- /dev/null +++ b/verification/proofs/agda/SingleActiveLog.agda @@ -0,0 +1,240 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- The single-active log, as theory. +-- +-- A log is a list of records, each with a key and a phase (active or +-- settled), plus a pointer to the key of the active record. Three kinds of +-- transition act on it: open a new record, edit the active record, and +-- settle the active record. Invariant `Good`: the pointer is set exactly when +-- one record is active, every other record is settled, and the active record +-- is the first with its key. The theorems below hold for every record type, +-- key type and transition that obey the stated laws. That is what makes them +-- theory in PROOF-POLICY §1's sense: they name no type or function of any +-- one implementation. +-- +-- januskey's TransactionManager is one instance (TransactionAtomicity.agda, +-- Part B). That the instance is faithful to the Rust is a separate, +-- engineering obligation (ledger row T-10), for Creusot and Verus. +-- +-- Nothing is imported beyond Agda's builtins, so the Rocq and Lean recheck +-- legs can restate every definition here without a library. + +module SingleActiveLog where + +open import Agda.Builtin.Equality using (_≡_; refl) +open import Agda.Builtin.List using (List; []; _∷_) +open import Agda.Builtin.Maybe using (Maybe; nothing; just) +open import Agda.Builtin.Nat using (Nat; zero; suc; _+_) + +---------------------------------------------------------------------- +-- A builtins-only prelude +---------------------------------------------------------------------- + +data ⊥ : Set where + +⊥-elim : {A : Set} → ⊥ → A +⊥-elim () + +_≢_ : {A : Set} → A → A → Set +x ≢ y = x ≡ y → ⊥ + +infix 4 _≢_ + +sym : {A : Set} {x y : A} → x ≡ y → y ≡ x +sym refl = refl + +trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z +trans refl q = q + +cong : {A B : Set} (f : A → B) {x y : A} → x ≡ y → f x ≡ f y +cong f refl = refl + +subst : {A : Set} (P : A → Set) {x y : A} → x ≡ y → P x → P y +subst P refl p = p + +data _⊎_ (A B : Set) : Set where + inl : A → A ⊎ B + inr : B → A ⊎ B + +infixr 5 _++_ +_++_ : {A : Set} → List A → List A → List A +[] ++ ys = ys +(x ∷ xs) ++ ys = x ∷ (xs ++ ys) + +data All {A : Set} (P : A → Set) : List A → Set where + [] : All P [] + _∷_ : ∀ {x xs} → P x → All P xs → All P (x ∷ xs) + +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 + +---------------------------------------------------------------------- +-- Phases +---------------------------------------------------------------------- + +data Phase : Set where + active settled : Phase + +active≢settled : active ≡ settled → ⊥ +active≢settled () + +---------------------------------------------------------------------- +-- The log, over any record type with a decidable key +---------------------------------------------------------------------- + +module Log (R I : Set) + (_≟_ : (a b : I) → (a ≡ b) ⊎ (a ≢ b)) + (key : R → I) + (phase : R → Phase) where + + record Log : Set where + constructor log + field + txs : List R + activeId : Maybe I + + open Log public + + Settled : R → Set + Settled r = phase r ≡ settled + + Fresh : I → List R → Set + Fresh i = All (λ u → key u ≢ i) + + -- Rewrite the FIRST record with key i; nothing if there is none. + update : I → (R → R) → List R → Maybe (List R) + update i f [] = nothing + update i f (t ∷ ts) with key t ≟ i + ... | inl _ = just (f t ∷ ts) + ... | inr _ with update i f ts + ... | nothing = nothing + ... | just us = just (t ∷ us) + + -- Open a new record; refused while a record is active. + begin : R → Log → Maybe Log + begin r (log ts (just _)) = nothing + begin r (log ts nothing) = just (log (ts ++ r ∷ []) (just (key r))) + + -- Edit the active record; refused when idle. + modify : (R → R) → Log → Maybe Log + modify f (log ts nothing) = nothing + modify f (log ts (just i)) with update i f ts + ... | nothing = nothing + ... | just us = just (log us (just i)) + + -- Settle the active record; refused when idle. + finish : (R → R) → Log → Maybe Log + finish g (log ts nothing) = nothing + finish g (log ts (just i)) with update i g ts + ... | nothing = nothing + ... | just us = just (log us nothing) + + data Good : Log → Set where + idle : ∀ {ts} → All Settled ts → Good (log ts nothing) + busy : ∀ {pre t post} + → All (λ u → key u ≢ key t) pre + → All Settled pre + → phase t ≡ active + → All Settled post + → Good (log (pre ++ t ∷ post) (just (key t))) + + good-empty : Good (log [] nothing) + good-empty = idle [] + + -- Only the active record is rewritten; everything before and after it is + -- untouched. + update-active : ∀ f pre t post + → All (λ u → key u ≢ key t) pre + → update (key t) f (pre ++ t ∷ post) ≡ just (pre ++ f t ∷ post) + update-active f [] t post [] with key t ≟ key t + ... | inl _ = refl + ... | inr n = ⊥-elim (n refl) + update-active f (u ∷ pre) t post (n ∷ ns) with key u ≟ key t + ... | inl e = ⊥-elim (n e) + ... | inr _ with update (key t) f (pre ++ t ∷ post) | update-active f pre t post ns + ... | .(just (pre ++ f t ∷ post)) | refl = refl + + -- A key-preserving edit keeps every record before the active one distinct + -- from it. + distinct-after : ∀ {k k' : I} pre → k' ≡ k + → All (λ u → key u ≢ k) pre + → All (λ u → key u ≢ k') pre + distinct-after [] e [] = [] + distinct-after (u ∷ pre) e (n ∷ ns) = + (λ q → n (trans q e)) ∷ distinct-after pre e ns + + ---------------------------------------------------------------------- + -- The transitions preserve Good + ---------------------------------------------------------------------- + + begin-refused-while-active : ∀ r ts j → begin r (log ts (just j)) ≡ nothing + begin-refused-while-active r ts j = refl + + begin-good : ∀ {r L L'} → phase r ≡ active → Good L → Fresh (key r) (txs L) + → begin r L ≡ just L' → Good L' + begin-good _ (busy _ _ _ _) _ () + begin-good {r} act (idle {ts} ss) fr refl = + busy {pre = ts} {t = r} {post = []} fr ss act [] + + modify-refused-when-idle : ∀ f ts → modify f (log ts nothing) ≡ nothing + modify-refused-when-idle f ts = refl + + -- An edit must keep the key and the phase of the record it edits. + modify-good : ∀ {f L L'} + → (∀ r → key (f r) ≡ key r) → (∀ r → phase (f r) ≡ phase r) + → Good L → modify f L ≡ just L' → Good L' + modify-good _ _ (idle _) () + modify-good {f} kf pf (busy {pre} {t} {post} np sp act sq) eq + with update (key t) f (pre ++ t ∷ post) | update-active f pre t post np + ... | .(just (pre ++ f t ∷ post)) | refl with eq + ... | refl = + subst (λ k → Good (log (pre ++ f t ∷ post) (just k))) (kf t) + (busy {pre = pre} {t = f t} {post = post} + (distinct-after pre (kf t) np) sp (trans (pf t) act) sq) + + finish-refused-when-idle : ∀ g ts → finish g (log ts nothing) ≡ nothing + finish-refused-when-idle g ts = refl + + -- A settling transition must keep the key and land in the settled phase. + finish-good : ∀ {g L L'} + → (∀ r → phase (g r) ≡ settled) + → Good L → finish g L ≡ just L' → Good L' + finish-good _ (idle _) () + finish-good {g} pg (busy {pre} {t} {post} np sp act sq) eq + with update (key t) g (pre ++ t ∷ post) | update-active g pre t post np + ... | .(just (pre ++ g t ∷ post)) | refl with eq + ... | refl = idle (all-++ sp (pg t ∷ sq)) + + ---------------------------------------------------------------------- + -- At most one record is active, and exactly when the pointer is set + ---------------------------------------------------------------------- + + countActive : List R → Nat + countActive [] = 0 + countActive (t ∷ ts) with phase t + ... | active = suc (countActive ts) + ... | settled = countActive ts + + expected : Maybe I → 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 phase t + ... | active = ⊥-elim (active≢settled s) + ... | settled = settled-count ss + + count-++ : ∀ xs ys → countActive (xs ++ ys) ≡ countActive xs + countActive ys + count-++ [] ys = refl + count-++ (x ∷ xs) ys with phase x + ... | active = cong suc (count-++ xs ys) + ... | settled = 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 diff --git a/verification/proofs/agda/TransactionAtomicity.agda b/verification/proofs/agda/TransactionAtomicity.agda index 38c9b06..0b56acb 100644 --- a/verification/proofs/agda/TransactionAtomicity.agda +++ b/verification/proofs/agda/TransactionAtomicity.agda @@ -25,19 +25,22 @@ -- -- 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. +-- * No I/O. Saving is not modelled. Some of the Rust's failed-save +-- behaviour is TESTED, not proved (ledger rows T-5 and T-8): a +-- transaction-log mutation, or a metadata-log edit, whose save fails is +-- not applied in memory, while a metadata append whose save fails keeps +-- its record for the next save; both logs are replaced by write, sync and +-- rename. A failure after the temporary file exists is not injected. A +-- file change whose log record fails to persist is OPEN (T-9). -- * 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. +-- executor is a no-op on failure (ASSUMED, T-6). +-- * Rollback is assumed to succeed on every step. In the Rust a rollback +-- that fails part-way stops, and a retry skips the operations already +-- undone (TESTED, T-4); Part A does not model the failure or the retry. -- * Transaction ids are assumed fresh (Fresh below). The Rust draws a --- UUID v4; a collision would break Good, and nothing here rules it out. +-- UUID v4; a collision would break Good, and nothing here rules it out +-- (ASSUMED, T-7). -- * 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. @@ -131,10 +134,19 @@ module Rollback (S : Set) where ---------------------------------------------------------------------- -- Part B. The TransactionManager lifecycle +-- +-- The invariant and its theorems are theory, proved once for every +-- single-active log in SingleActiveLog.agda (ledger rows T-2 and T-3). This +-- module is januskey's instance: a transaction is a record keyed by its id, +-- Active or settled by its state, and the four TransactionManager +-- transitions are the abstract ones at that record type. That the Rust +-- matches this instance is engineering (ledger row T-10), not proved here. ---------------------------------------------------------------------- module Lifecycle where + import SingleActiveLog as SAL + data TState : Set where Active Committed RolledBack : TState @@ -154,53 +166,41 @@ module Lifecycle where 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) + phaseOf : TState → SAL.Phase + phaseOf Active = SAL.active + phaseOf Committed = SAL.settled + phaseOf RolledBack = SAL.settled + + _≟ₛ_ : (m n : Nat) → (m ≡ n) SAL.⊎ (m SAL.≢ n) + m ≟ₛ n with m ≟ n + ... | inl p = SAL.inl p + ... | inr q = SAL.inr (λ e → ⊥-elim (q e)) + -- `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) + -- with that id changes (SAL.Log.update). + open SAL.Log Tx Nat _≟ₛ_ txId (λ t → phaseOf (txState t)) public + hiding (begin-refused-while-active; finish-refused-when-idle) + renaming (begin to openRecord; finish to settleActive; + begin-good to openRecord-good; finish-good to settleActive-good) -- 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)) + begin i = openRecord (tx i Active []) -- 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)) + addOp o = modify (addOpTx o) -- 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) + finish s = settleActive (settle s) commit : Log → Maybe Log commit = finish Committed @@ -209,92 +209,31 @@ module Lifecycle where 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. + -- Theorems B-1 to B-4, as instances of SingleActiveLog ---------------------------------------------------------------------- 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. - ---------------------------------------------------------------------- + begin-good g fr eq = openRecord-good refl g fr eq 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. - ---------------------------------------------------------------------- + addOp-good = modify-good (λ _ → refl) (λ _ → refl) finish-refused-when-idle : ∀ s ts → finish s (log ts nothing) ≡ nothing finish-refused-when-idle s ts = refl + settled-phase : ∀ {s} → s ≢ Active → phaseOf s ≡ SAL.settled + settled-phase {Active} sn = ⊥-elim (sn refl) + settled-phase {Committed} _ = refl + settled-phase {RolledBack} _ = 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)) + finish-good sn = settleActive-good (λ _ → settled-phase sn) commit-good : ∀ {L L'} → Good L → commit L ≡ just L' → Good L' commit-good = finish-good (λ e → Active≢Committed (sym e)) @@ -302,40 +241,7 @@ module Lifecycle where 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-4 (at-most-one-active) is SingleActiveLog's, at this instance. ---------------------------------------------------------------------- -- Theorem B-5 (lifecycle-preserves-good): the four transitions together. @@ -351,8 +257,8 @@ module Lifecycle where 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) + → SAL.All (λ u → txId u SAL.≢ txId t) pre + → update (txId t) f (pre SAL.++ t ∷ post) ≡ just (pre SAL.++ f t ∷ post) lifecycle-preserves-good : Preserves lifecycle-preserves-good = record diff --git a/verification/proofs/lean/Rollback.lean b/verification/proofs/lean/Rollback.lean new file mode 100644 index 0000000..b1963db --- /dev/null +++ b/verification/proofs/lean/Rollback.lean @@ -0,0 +1,51 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Lean recheck leg of ledger row T-1 (PROOF-POLICY §2, route: re-proved). +-- +-- Source of truth: verification/proofs/agda/TransactionAtomicity.agda, +-- module Rollback, theorem rollback-restores. This file restates that theorem +-- and proves it again by hand in core Lean 4: no Mathlib, no imports. +-- +-- Why re-proved and not transported: PROOF-POLICY §2 re-proves the Lean leg +-- until a released Lambdapi has a Lean exporter, and the Agda → Dedukti +-- translator (Deducteam/Agda2Dedukti, last changed January 2022) cannot read +-- modules checked by the pinned Agda 2.6.4.3. docs/theory/PROOF-GRADES.adoc +-- records the statement comparison. + +namespace JanusKey.Rollback + +/-- A recorded operation (Agda: record Op). `execute` may fail; `undo`, +applied to the state a successful execute produced, restores the state it +started from. -/ +structure Op (S : Type) : Type where + execute : S → Option S + undo : S → S + undoes : ∀ {x y : S}, execute x = some y → undo y = x + +/-- The recorded list ran successfully from `x` to `z` (Agda: data Executed). +It lives in `Type`, as the Agda family lives in `Set`. -/ +inductive Executed {S : Type} : List (Op S) → S → S → Type where + | done {x : S} : Executed [] x x + | next {o : Op S} {os : List (Op S)} {x y z : S} : + o.execute x = some y → Executed os y z → Executed (o :: os) x z + +/-- `cmd_rollback`: undo the last recorded operation first (Agda: rollback). -/ +def rollback {S : Type} : List (Op S) → S → S + | [], z => z + | o :: os, z => o.undo (rollback os z) + +/-- Theorem A-1 (Agda: rollback-restores). -/ +theorem rollback_restores {S : Type} {os : List (Op S)} {x z : S} : + Executed os x z → rollback os z = x := by + intro h + induction h with + | done => rfl + | @next o os x y z e _ ih => + show o.undo (rollback os z) = x + rw [ih] + exact o.undoes e + +end JanusKey.Rollback + +#print axioms JanusKey.Rollback.rollback_restores diff --git a/verification/proofs/rocq/Rollback.v b/verification/proofs/rocq/Rollback.v new file mode 100644 index 0000000..e13e803 --- /dev/null +++ b/verification/proofs/rocq/Rollback.v @@ -0,0 +1,52 @@ +(* SPDX-License-Identifier: MPL-2.0 *) +(* SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell *) +(* + Rocq recheck leg of ledger row T-1 (PROOF-POLICY §2, route: re-proved). + + Source of truth: verification/proofs/agda/TransactionAtomicity.agda, + module Rollback, theorem rollback-restores. This file restates that + theorem and proves it again by hand, using only the Rocq prelude. + + Why re-proved and not transported: the Agda → Dedukti translator + (Deducteam/Agda2Dedukti) was last changed in January 2022. It builds + against a forked Agda branch of that period and cannot read modules checked + by the pinned Agda 2.6.4.3, so no transport route exists for this + toolchain. docs/theory/PROOF-GRADES.adoc records the statement comparison. +*) + +Set Implicit Arguments. + +(* A recorded operation (Agda: record Op). `execute` may fail; `undo`, + applied to the state a successful execute produced, restores the state it + started from. *) +Record Op (S : Type) : Type := mkOp { + execute : S -> option S; + undo : S -> S; + undoes : forall x y, execute x = Some y -> undo y = x +}. + +(* The recorded list ran successfully from x to z (Agda: data Executed). *) +Inductive Executed (S : Type) : list (Op S) -> S -> S -> Type := + | done : forall x, Executed nil x x + | next : forall o os x y z, + execute o x = Some y -> Executed os y z -> Executed (cons o os) x z. + +(* cmd_rollback: undo the last recorded operation first (Agda: rollback). *) +Fixpoint rollback (S : Type) (os : list (Op S)) (z : S) : S := + match os with + | nil => z + | cons o os' => undo o (rollback os' z) + end. + +(* Theorem A-1 (Agda: rollback-restores). *) +Theorem rollback_restores : + forall (S : Type) (os : list (Op S)) (x z : S), + Executed os x z -> rollback os z = x. +Proof. + intros S os x z H. + induction H as [x | o os x y z e r IH]; simpl. + - reflexivity. + - rewrite IH. exact (@undoes S o x y e). +Qed. + +Print Assumptions rollback_restores.