From e935d7b5ee2bf3a411b9505c14ad7ab54ac8236c Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:11:51 +0000 Subject: [PATCH 1/3] =?UTF-8?q?proofs:=20Proof=20Witness=20Grades=20(PROOF?= =?UTF-8?q?-POLICY=20=C2=A78),=20invariant=20checked=20at=20load=20(T-10),?= =?UTF-8?q?=20lost=20T-8/T-9=20rows=20restored?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Ledger repair. When #167 was merged into the #168 branch, PROOF-NEEDS.adoc kept #167's side of the conflict. Main therefore lost T-8's TESTED status and its five rows, and both T-9 rows, while the prose still cited T-9. This commit restores them. dashboard-check could not catch the loss, because it reconciles counts and PROVEN checkers, not rows against the previous head. Proof review (T-2, T-3). The Agda lifecycle theorems take the invariant Good as a premise, and the Rust never checked it on a log read from disk. TransactionManager::new now refuses such a log as MetadataCorrupted (T-10, TESTED: five ways of breaking Good, a positive control, and three mutants that each fail). The unused public active_mut, which could change a transaction outside the four transitions, is removed. The model's match to the Rust is recorded as T-11 (ASSUMED). Stale "not claimed" notes in two Agda headers now point at T-4, T-5, T-7 and T-10. These are comments only, and the propositions are unchanged. Grades. The Mathesis-brief "Grade 3" wording is replaced by PROOF-POLICY §8: a census (PWG-3 5, ungraded 3, of 8 theory rows), §8.5 records with the Rocq and Lean legs OPEN, and receipt lineage (runs 40867211509, 41687715055 and 42076969251 superseded). The Agda gate now prints the remaining §8.2 and §8.4 receipt fields: the import cone (from --dependency-graph), per-file and total SHA-256 input digests, and a comment-aware escape-hatch scan of every non-builtin cone file. The scan checks itself against planted hatches on every run, under gawk and mawk. Rust obligations name Creusot, Pearlite and Verus (§1.2), all OPEN with a reason. The stale [proof-grades] block is deleted from the legacy STATE.a2ml, which gains no facts. The test count is now 143. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .machine_readable/6a2/STATE.a2ml | 18 +- CHANGELOG.adoc | 10 + PROOF-NEEDS.adoc | 107 ++-- READINESS.adoc | 4 +- TOPOLOGY.adoc | 2 +- crates/reversible-core/src/transaction.rs | 139 ++++- docs/theory/PROOF-GRADES.adoc | 565 ++++++++---------- scripts/agda-cone.sh | 132 ++++ scripts/check-agda.sh | 7 +- verification/proofs/agda/Reversibility.agda | 9 +- .../proofs/agda/TransactionAtomicity.agda | 20 +- 11 files changed, 622 insertions(+), 391 deletions(-) create mode 100755 scripts/agda-cone.sh diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index d68c5af..2548909 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -44,20 +44,12 @@ property-tests = "9 (2026-04-03 assessment, not re-derived)" regression-tests = "5 (2026-04-03 assessment, not re-derived)" idris2-proofs = "12 PROVEN ledger rows (the former 30 counted lemmas before the tautology purge; PROOF-NEEDS.adoc is authoritative)" benchmarks = "5 Criterion groups (no baseline recorded)" -total = "141 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared in READINESS.adoc and measured by dashboard-check" +total = "143 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-grades] removed 2026-11-09: its receipt, flag and row facts had gone +# stale. Proof Witness Grades (PROOF-POLICY §8) are recorded in PROOF-NEEDS.adoc +# §Proof Witness Grades, with receipts in docs/theory/PROOF-GRADES.adoc. A2ML +# is retired: this legacy file may lose facts but gains none. [test-categories-complete] unit = true diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index d2b3b84..fc7b2a6 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -17,6 +17,16 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. ==== Added +* feat(transactions): a transaction log read from disk is checked against the +lifecycle invariant the Agda theorems preserve, and refused if it breaks it +(T-10, TESTED); the unused `TransactionManager::active_mut` is removed; the +model's match to the Rust is recorded as T-11 (ASSUMED) +* feat(proofs): proof grades restated as Proof Witness Grades (PROOF-POLICY +§8): five `PWG-3` rows, census of 8 theory rows; the Agda gate now prints the +import cone, input digests and a self-tested comment-aware escape-hatch scan +into its receipt; Rust obligations name Creusot, Pearlite and Verus (§1.2) +* fix(ledger): restore the T-8 TESTED and T-9 OPEN rows that the #167 merge +into #168 dropped * feat(proofs): `Epistemic.agda` replaces the vacuous Idris `Knows` modality with knowledge as indiscriminability: ignorance, obliteration and rotation-forgetting become propositions, with two expected-rejection fixtures; new ledger row E-1m diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9ea6b33..e66f7cd 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -74,7 +74,10 @@ tables must agree. | 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-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 saved atomically; a save that fails leaves mark_undone, prune and purge unapplied in memory, and keeps an append pending for the next save (its file change already happened) | TESTED | `+metadata::tests::save_replaces_rather_than_overwrites_the_log+` (rename, not an in-place write, through `+crate::transaction::write_atomic+`; a plain `+fs::write+` mutant fails it) and `+save_replaces_the_log_atomically+` (no temporary file left) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` and `+a_failed_append_keeps_its_record_for_the_next_save+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a save that fails before its temporary file exists); a mutant that updates memory first, and one that removes the log before saving, each fail a test +| T-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` changes the filesystem and then appends its record, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash or failed save between the two leaves a change the log does not know about (on undo: the file restored but the operation still marked not undone, so the retry tries the inverse again). Save ordering cannot close this; it needs a write-ahead intent record, which is a design decision, not a fix +| T-10 | A transaction log read from disk satisfies the invariant `+Good+` that T-2 and T-3 preserve, so their premise holds for a loaded log too; a log that breaks it is refused as corrupted, not loaded | TESTED | `+transaction::tests::a_loaded_log_that_breaks_the_invariant_is_refused+` (five ways of breaking `+Good+`: pointer to a missing or a settled transaction, an Active one with no pointer, two Active, a pointer whose first transaction with that id is settled) and the positive control `+a_log_the_manager_wrote_loads_back+`; mutants (no check at load, last-with-id instead of first, no stray-Active scan) each fail the first test. Before this row the premise was unchecked at load, and the unused `+active_mut+`, which could change a transaction outside the four transitions, has been removed +| T-11 | The Agda lifecycle model (`+TransactionAtomicity.Lifecycle+`) corresponds to `+TransactionManager+` (by transcription, like G-2) | ASSUMED | no mechanical link; PROOF-POLICY §2.1: a translated model does not prove runtime refinement. The Rust is tested against the same transitions (T-5, T-10) | 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) @@ -110,46 +113,56 @@ IO do-notation at all. The dashboards (README, TOPOLOGY, READINESS) carry the proof count that `+dashboard-check+` measures from the PROVEN rows of the ledger below. -=== Proof grades under mathesis (2026-11-01) - -The five statuses above are this repository's claim vocabulary — the estate's -README-EXPLAINME ledger, as used across it. A *proof grade* is a second, -orthogonal axis, governed by `+hyperpolymath/mathesis+` -(`+estate-mathematical-architecture+` §5 and §6) and by -`+hyperpolymath/standards+` `+3-practice/PROOF-POLICY.adoc+`. Neither uses a -confidence percentage and this repository does not publish one. - -Of the 12 PROVEN rows, five are the theory rows — **G-1, T-1, T-2, T-3, E-1m** — and -their artefact is Agda (`+verification/proofs/agda/+`). They are **Grade 3**: -each type-checks in Agda and none has been translated to an independent -foundational system, which is mathesis §5's definition as written. The receipt -is a green `+agda-proofs.yml+` run -(https://github.com/hyperpolymath/januskey/actions/runs/41687715055[41687715055]) -at commit `+fc188c4+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at -`+cf9235c+`. That run used the current gate (`+Reversibility+`, -`+TransactionAtomicity+` and `+Epistemic+` under `+--safe --without-K ---cubical-compatible+`), and the modules, the gate script, the sibling fetch and -the workflow are byte-identical at that commit and at this one, so the receipt -covers these rows, E-1m included, as they stand. (An earlier receipt cited here, -run 40867211509 at `+4afb710+`, predates `+Epistemic.agda+` and the -`+--cubical-compatible+` flag, so it never covered E-1m.) Mathesis status for them: -`+AGDA-VERIFIED+`. - -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 -same holds for the 27 TESTED rows, which record observed behaviour and never -grading. First-party Rust behaviour belongs to **Creusot** (not SPARK, and not -Idris2); no Creusot contract exists in this tree, which is why no Rust row is -graded. - -No row of this ledger is Grade 2i, Grade 2ii or Grade 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 …+`), which was verified locally -with Agda 2.6.4.3 before being committed; the CI receipt for that flag set is -the next `+agda-proofs.yml+` run, not the older one. +=== Proof Witness Grades (PROOF-POLICY §8) + +The five statuses above are this repository's claim vocabulary (the +README-EXPLAINME ledger; DESIGNED aside, they are the §5 tokens of the +estate's `+metadatastician/standards+` `+3-practice/PROOF-POLICY.adoc+`, +read at `+9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5+`, 2026-11-08). A *Proof Witness +Grade* is a separate field, defined by that policy's §8 (owner ruling +2026-11-04). It says how many independent machine-checked witnesses a +*theory* theorem has: `+PWG-3+` (the Agda proof checks under §2.1), then +`+PWG-2i+` and `+PWG-2ii+` (one or both Rocq and Lean recheck legs counted), +then `+PWG-1+` (per-commit receipts for every witness). Lower is stronger. +Grades are derived from receipts, never asserted. The Mathesis brief's +grade ladder, whose wording this file used until 2026-11-09, is superseded by +§8 and is not used here. + +*Census of theory theorems (by ledger row): `+PWG-3+` 5 (G-1, T-1, T-2, +T-3, E-1m), `+PWG-2i+` 0, `+PWG-2ii+` 0, `+PWG-1+` 0, `+ungraded+` 3 (G-3, +E-1 and the reversibility theorem "every operation is reversible", all +`+OPEN+`), of 8.* None of the five rests on an axiom: each is `+PROVEN+`, +not `+PROVEN-WITH-AXIOMS+`. A `+PWG-3+` grade is not a discharge. Each of the +five still owes its Rocq and Lean legs (§2, §8.4 rule 1). + +The §8.5 record for each graded row: + +[cols="1,1,1,2,2,2",options="header"] +|=== +| Row | `+pwg+` | `+foundation_diverse+` | Agda leg | Rocq leg | Lean leg + +| G-1 | 3 | false .5+| `+PROVEN+`; correspondence `+AGDA-VERIFIED+`; receipt: the +`+agda-proofs.yml+` run on the source commit, `+current+` (see +`+docs/theory/PROOF-GRADES.adoc+` for the fields and the lineage) +.5+| `+OPEN+`: not attempted, so no route is chosen yet and no +correspondence state applies (§2: Dedukti transport first, re-proof as the +fallback) +.5+| `+OPEN+`: not attempted, as for Rocq (§2: no released Lambdapi Lean +exporter is pinned, so this leg is expected to be re-proved) +| T-1 | 3 | false +| T-2 | 3 | false +| T-3 | 3 | false +| E-1m | 3 | false +|=== + +The other seven PROVEN rows (A-1, A-2, C-1 to C-5) are Idris2 theorems about +the ABI. The 35 TESTED rows record observed behaviour. §8.1 grades neither: +engineering proofs carry the §5 tokens only. First-party Rust behaviour belongs +to *Creusot*, with contracts in *Pearlite*, and to *Verus*, by default +(PROOF-POLICY §1.2). No Creusot, Pearlite or Verus artefact exists in this tree, +so every Rust obligation stays at its tested status. The obligations, their +entrypoints and why neither verifier has been run are listed in +`+docs/theory/PROOF-GRADES.adoc+` §Rust obligations. === Current State @@ -190,7 +203,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; a loaded log is checked against the proved invariant, T-10, and the model's match to the Rust is assumed, T-11; 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) |Partial transactions corrupt state |reversible-core |Undo/redo preserves data integrity |Core crate used by @@ -266,7 +279,15 @@ the status table above. |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-8: A metadata save leaves no temporary file behind and ignores a stale one 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 save replaces the log rather than overwriting it in place (a hard link to the old log keeps the old bytes; a regression to plain `fs::write` fails) |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 metadata save that fails leaves mark_undone, prune and purge unapplied in memory, and each retried mutator then applies once with memory and the reloaded log agreeing |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 pending, and the next successful save persists it once (so `jk delete` continuing after one failed record does not lose it) |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 save that fails before creating its temporary file leaves the existing log's bytes intact on disk (failure injected without touching the log; shared by the transaction and metadata logs; a failure after the temporary file exists is not covered) |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` +|T-9: A file operation or undo whose log record fails to persist can be recovered or retried (by inspection: the filesystem changes before the record is saved; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- +|T-10: A transaction log read from disk that breaks the lifecycle invariant (pointer to a missing or settled transaction, an Active one with no pointer, two Active, or a settled first transaction with the active id) is refused as corrupted |TESTED |`crates/reversible-core/src/transaction.rs::a_loaded_log_that_breaks_the_invariant_is_refused` |`cargo test --locked -p reversible-core --lib a_loaded_log_that_breaks_the_invariant_is_refused` +|T-10: Logs the manager writes, idle and busy, satisfy the invariant and load back (the positive control) |TESTED |`crates/reversible-core/src/transaction.rs::a_log_the_manager_wrote_loads_back` |`cargo test --locked -p reversible-core --lib a_log_the_manager_wrote_loads_back` +|T-11: The Agda lifecycle model corresponds to TransactionManager (by transcription) |ASSUMED |`verification/proofs/agda/TransactionAtomicity.agda` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- |T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |- |Every operation is reversible (MPR), as a theorem linked to the Rust (needs G-2 made mechanical, and G-3) |OPEN |`verification/proofs/agda/Reversibility.agda` |- diff --git a/READINESS.adoc b/READINESS.adoc index ef390ea..e59fd6e 100644 --- a/READINESS.adoc +++ b/READINESS.adoc @@ -8,7 +8,7 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0 === CRG Grade: D (Alpha — Unstable) -*Justification:* 141 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the +*Justification:* 143 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the Idris2 ABI typechecks and 12 proofs are checked (PROVEN ledger rows: ABI, grade, transaction-model and epistemic-model lemmas, not the security obligations); benchmarks exist (5 Criterion groups). But: no fuzz testing, no mutation testing, 241 unwrap() calls, E2E mostly skips, @@ -65,7 +65,7 @@ handling (run by idris-abi.yml, agda-proofs.yml and dashboard-check) |=== -*Total declared:* 141 tests + 5 benchmark groups; 12 proofs checked (PROVEN ledger rows; five of them Grade 3 under mathesis — see `docs/theory/PROOF-GRADES.adoc`) *Total +*Total declared:* 143 tests + 5 benchmark groups; 12 proofs checked (PROVEN ledger rows; five of them `PWG-3` under PROOF-POLICY §8 — see `docs/theory/PROOF-GRADES.adoc`) *Total missing:* Fuzz, mutation, chaos, compatibility === Aspect Matrix diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index 1133cfb..ba10832 100644 --- a/TOPOLOGY.adoc +++ b/TOPOLOGY.adoc @@ -79,7 +79,7 @@ INTERFACES & RESEARCH MPR Methodology ████░░░░░░ ~40% Design documented; FORMAL PROOFS PENDING (Idris2 ABI typechecks; 12 proofs checked: ABI, grade, transaction-model and epistemic-model lemmas, not the security obligations; MPR not linked to the Rust) - Testing (READINESS matrix) ██████░░░░ ~60% 141 tests + 5 benches; missing fuzz, mutation, + Testing (READINESS matrix) ██████░░░░ ~60% 143 tests + 5 benches; missing fuzz, mutation, chaos, compatibility (Grade D) REPO INFRASTRUCTURE diff --git a/crates/reversible-core/src/transaction.rs b/crates/reversible-core/src/transaction.rs index 4e9bca2..b4cde8a 100644 --- a/crates/reversible-core/src/transaction.rs +++ b/crates/reversible-core/src/transaction.rs @@ -106,6 +106,52 @@ impl TransactionLog { } } +/// Check the lifecycle invariant `Good` of +/// `verification/proofs/agda/TransactionAtomicity.agda` on a log read from disk. +/// +/// The Agda theorems (ledger rows T-2 and T-3) prove that begin, add_operation, +/// commit and mark_rolled_back preserve `Good`, so a log this code wrote +/// satisfies it. A log read from disk is not guaranteed to — it may have been +/// edited, or written by another version — and without this check the proved +/// invariant would rest on an unchecked premise at load (row T-10). +/// +/// `Good` holds when either the active pointer is unset and no transaction is +/// Active, or the pointer names an id whose *first* transaction is Active and +/// every other transaction is Committed or RolledBack. `begin`, the update path +/// and the rollback path all select the first transaction with the active id, +/// which is why "first" is the one checked. +fn check_invariant(log: &TransactionLog) -> std::result::Result<(), String> { + let active_at = match &log.active_transaction_id { + None => None, + Some(id) => { + let at = log + .transactions + .iter() + .position(|t| t.id == *id) + .ok_or_else(|| format!("active transaction {id} is not in the log"))?; + if !log.transactions[at].is_active() { + return Err(format!( + "active transaction {id} is {:?}, not Active", + log.transactions[at].state + )); + } + Some(at) + } + }; + match log + .transactions + .iter() + .enumerate() + .find(|(i, t)| t.is_active() && Some(*i) != active_at) + { + Some((_, t)) => Err(format!( + "transaction {} is Active but the active pointer is {:?}", + t.id, log.active_transaction_id + )), + None => Ok(()), + } +} + /// Build a sibling temporary pathname that is unique to this save. /// /// A random component, not a process id, so writers in different PID @@ -233,8 +279,10 @@ impl TransactionManager { Ok(buf) }) })?; - serde_json::from_str(&content) - .map_err(|e| ReversibleError::MetadataCorrupted(e.to_string()))? + let log: TransactionLog = serde_json::from_str(&content) + .map_err(|e| ReversibleError::MetadataCorrupted(e.to_string()))?; + check_invariant(&log).map_err(ReversibleError::MetadataCorrupted)?; + log } else { TransactionLog::new() }; @@ -330,12 +378,6 @@ impl TransactionManager { .and_then(|id| self.log.transactions.iter().find(|t| t.id == *id)) } - /// Get mutable active transaction - pub fn active_mut(&mut self) -> Option<&mut Transaction> { - let active_id = self.log.active_transaction_id.clone()?; - self.log.transactions.iter_mut().find(|t| t.id == active_id) - } - /// Append an operation ID to the active transaction and persist the log. /// /// IDs are recorded in the supplied order without validation or deduplication. @@ -826,4 +868,85 @@ mod tests { .expect("failed to begin first transaction"); assert!(manager.begin(None).is_err()); } + + /// Write `log` where a manager will load it, and try to load it. + fn load(log: &TransactionLog) -> Result { + let tmp = TempDir::new().expect("temp dir"); + let path = tmp.path().join("transactions.json"); + std::fs::write(&path, serde_json::to_string(log).expect("serialise")).expect("write"); + TransactionManager::new(path) + } + + fn tx_in(state: TransactionState, id: &str) -> Transaction { + let mut t = Transaction::new(None); + t.id = id.to_string(); + t.state = state; + t + } + + fn log_of(txs: Vec, active: Option<&str>) -> TransactionLog { + TransactionLog { + version: "1.0".to_string(), + transactions: txs, + active_transaction_id: active.map(str::to_string), + } + } + + /// T-10: a log read from disk must satisfy the invariant `Good` that the + /// Agda lifecycle theorems (T-2, T-3) preserve; each way of breaking it is + /// refused as corrupted rather than loaded. + #[test] + fn a_loaded_log_that_breaks_the_invariant_is_refused() { + use TransactionState::{Active, Committed, RolledBack}; + let cases = [ + ( + "pointer to a missing transaction", + log_of(vec![tx_in(Committed, "a")], Some("b")), + ), + ( + "pointer to a settled transaction", + log_of(vec![tx_in(Committed, "a")], Some("a")), + ), + ( + "Active with no pointer", + log_of(vec![tx_in(Active, "a")], None), + ), + ( + "two Active transactions", + log_of(vec![tx_in(Active, "a"), tx_in(Active, "b")], Some("a")), + ), + ( + "pointer id whose first transaction is settled", + log_of(vec![tx_in(RolledBack, "a"), tx_in(Active, "a")], Some("a")), + ), + ]; + for (what, log) in cases { + match load(&log) { + Err(ReversibleError::MetadataCorrupted(_)) => {} + Err(e) => panic!("{what}: refused with the wrong error: {e}"), + Ok(_) => panic!("{what}: a log that breaks the invariant was loaded"), + } + } + } + + /// T-10, the positive control: logs the manager writes satisfy the + /// invariant, idle and busy, and load back unchanged. + #[test] + fn a_log_the_manager_wrote_loads_back() { + let tmp = TempDir::new().expect("temp dir"); + let path = tmp.path().join("transactions.json"); + let mut manager = TransactionManager::new(path.clone()).expect("new"); + manager.begin(None).expect("begin"); + manager.add_operation("op-1".to_string()).expect("add"); + manager.commit().expect("commit"); + manager.begin(None).expect("begin again"); + manager.mark_rolled_back().expect("roll back"); + let idle = TransactionManager::new(path.clone()).expect("an idle log loads"); + assert_eq!(idle.all().len(), 2); + assert!(!idle.has_active()); + + manager.begin(None).expect("begin a third"); + let busy = TransactionManager::new(path).expect("a busy log loads"); + assert_eq!(busy.active_id(), manager.active_id()); + } } diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 6fed117..42d2a1c 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -1,347 +1,290 @@ -= Proof grades under mathesis and PROOF-POLICY += Proof Witness Grades: receipts, lineage and review :toc: preamble :icons: font -This page grades januskey's proof claims in the vocabulary its owner's estate -mathematics architecture uses, and records the receipt for every grade. It is -the answer to a single question a reader of `PROOF-NEEDS.adoc` should not have -to reconstruct: *which of these claims is a proof, and how good a proof is it?* +This page backs the Proof Witness Grade records in `PROOF-NEEDS.adoc` +(§Proof Witness Grades). It answers the question a reader of the ledger should +not have to reconstruct: *which claims are proofs, how many independent +witnesses each has, and what the receipts say.* It also records a design +review of what each graded theorem actually establishes. -It grades nothing by confidence. There is no percentage anywhere in this -repository, and none is introduced here. +No percentage appears here, and none is introduced. Grades are reported as a +census with their denominator. -== What governs the grades +== What governs -Two owner documents, both read at HEAD on 2026-11-01: - -[cols="1,2,3",options="header"] +[cols="1,3",options="header"] |=== -| Source | Section | Rule taken from it - -| `hyperpolymath/mathesis`, - file `estate-mathematical-architecture` -| §5 grades -| **Grade 3** — "a proof is Grade 3 if it type-checks locally in Agda but has - not been translated to an independent foundational system". Grade 2i adds one - translation, Grade 2ii two *foundationally distinct* ones (Agda, Rocq and - Lean are all dependent type theory, so 2ii needs Isabelle/HOL), Grade 1 is a - check served to headless CI tooling (AXLE, isabelle server, coq-lsp REST). - -| mathesis, same file -| §6 reporting -| No percentage; every axiom the development relies on is tracked; a grade - receipt records the **commit hash** it was produced at; a grade that stops - applying is marked `Superseded` or `Regressed`, never quietly deleted. - -| `hyperpolymath/standards`, - `3-practice/PROOF-POLICY.adoc` -| §1 mapping -| Theory is proved in **Agda** and rechecked in Rocq and Lean; the behaviour of - first-party Rust is **Creusot** on that code; API, ABI and wire-format - contracts are **Idris2**. The earlier "Rust always means Rust/SPARK" note is - withdrawn (owner ruling 2026-04-10): Rust is Creusot. - -| PROOF-POLICY -| §2.1 invocation -| `agda --safe --without-K --cubical-compatible `; pin and record - the Agda version and the library set per commit; a missing tool is an open - obligation, never a silent skip. - -| PROOF-POLICY -| §2.3 execution -| The policy text records policy; CI receipts establish the executions. §2.2's - statuses (`AGDA-PENDING`, `AGDA-VERIFIED`, `COQ-CHECKED`, `LEAN-CHECKED`, - `BRIDGE-PENDING`, `RECONCILED`, `COUNTEREXAMPLE`, `QUARANTINED`) name what - happened to one proposition. +| Source | Rule taken from it + +| `metadatastician/standards` `3-practice/PROOF-POLICY.adoc` §8, read at + `9bdf864cc7f2c8e24b4df84bf00d04158eee3ad5` (2026-11-08) +| *Proof Witness Grades* (owner ruling 2026-11-04): `PWG-3`, `PWG-2i`, + `PWG-2ii`, `PWG-1`, and `ungraded` below `PWG-3`. Always written with the + prefix. Grades apply to theory theorems only (§8.1), are derived from + receipts (§8.4 rule 2), never carried forward from an older commit (rule 4), + and keep their history on the receipt as `current`, `superseded` or + `regressed` (rule 5). For Agda, the axioms travel as `--safe`, a + comment-aware postulate scan of the import cone, and the recorded cone + (rule 6). + +| PROOF-POLICY §2.1 +| The canonical entrypoint invocation + `agda --safe --without-K --cubical-compatible `, with the Agda + version and the library set recorded per commit. Earlier `--safe` or + `--safe --without-K` successes are historical evidence, not receipts. + +| PROOF-POLICY §1 and §1.2 +| Theory is proved in Agda and rechecked in Rocq and Lean. API, ABI and + engineering contracts are Idris2. First-party Rust is verified with + *Creusot* (contracts in *Pearlite*) and *Verus*, by default (owner ruling + 2026-11-07). + +| PROOF-POLICY §5 +| The closed status vocabulary: `PROVEN`, `PROVEN-WITH-AXIOMS`, `TESTED`, + `ASSUMED`, `OPEN`. januskey's ledger also uses `DESIGNED` for consumption + rows, which are not proof obligations. + +| `hyperpolymath/mathesis`, `docs/proposals/estate-mathematical-architecture.adoc` +| Provenance only. Its §5–§6 grade ladder was adopted with corrections as + §8. This page used the brief's wording until 2026-11-09 and + no longer does. Mathesis may catalogue the grades below; it derives them + from these receipts and does not assign them (§8.5). |=== -januskey's own five-status ledger vocabulary (`PROVEN`, `TESTED`, `ASSUMED`, -`DESIGNED`, `OPEN`) is the estate's claim vocabulary and is unchanged by any of -this. A grade is a second axis laid over it, not a replacement: a row is -`PROVEN` *because* a named artefact checks it, and separately has (or has not) a -mathesis grade. +== Census + +Theory theorems, counted by ledger row: + +*`PWG-3` 5 (G-1, T-1, T-2, T-3, E-1m) · `PWG-2i` 0 · `PWG-2ii` 0 · `PWG-1` 0 · +`ungraded` 3 (G-3, E-1, "every operation is reversible") · of 8.* -== The Grade 3 receipt +None of the five `PWG-3` rows rests on an axiom. A `PWG-3` grade is not a +discharge: each of the five still owes its Rocq and Lean legs. -The theory artefacts are two Agda modules: +The three `ungraded` rows are `OPEN`. G-3 (the FFI bridge preserves grade 𝟙) +and the reversibility theorem need G-2 made mechanical first. E-1 is a claim +about an implementation under cryptographic assumptions (X-1). Its model-level +shadow is E-1m, and a model of channels does not grade E-1. -* `verification/proofs/agda/Reversibility.agda` — the Loss grade algebra: - lossless traces have only lossless steps, obliteration absorbs, and a - wrap/unwrap pair with a cancellation premise is a grade-𝟙 two-step trace. -* `verification/proofs/agda/TransactionAtomicity.agda` — rollback restores the - state the transaction began in; the `TransactionManager` lifecycle keeps its - log invariant under begin, add_operation, commit and mark_rolled_back, and at - most one transaction is Active. +== The `PWG-3` receipt -Both are checked by `scripts/check-agda.sh` (`just test-agda`), which is also -the ledger's recorded checker for rows G-1, T-1, T-2 and T-3. The receipt: +A receipt is the log of the `agda-proofs.yml` job (*Reversibility as a grade +(Loss instance), expected rejections*) on the exact source commit. From this +change on, `scripts/check-agda.sh` prints every §8.2 field into that log: [cols="1,3",options="header"] |=== -| Field | Value - -| Workflow, run | `agda-proofs.yml`, run - https://github.com/hyperpolymath/januskey/actions/runs/40867211509[40867211509], - branch `main`, conclusion **success** -| Commit | `4afb710e86646658f667f10bd6274ee47416bfc7` (started 2026-10-29T11:40:36Z) -| Prover | `agda-bin=2.6.4.3-1+b2` on Debian trixie-slim - (`@sha256:a29215f6…`), asserted by a passing step: - `test "$(agda --version)" = 'Agda version 2.6.4.3'` -| Flags | `--safe --without-K --no-libraries --ignore-interfaces --double-check` - at the receipt commit; the gate now runs PROOF-POLICY §2.1's canonical form - with `--cubical-compatible` added (see §The §2.1 invocation below) -| Sibling | `resource-algebra` at +| Field | Where it comes from + +| Checker and version | `agda --version`. CI pins `agda-bin=2.6.4.3-1+b2` on + `debian:trixie-slim@sha256:a29215f6…` and fails unless the version string is + exactly `Agda version 2.6.4.3`. +| Flags in force | `flags:` line: + `--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check` + plus the two include paths. This is §2.1's canonical form with three + tightenings: no library is resolved implicitly, the sibling is re-checked + from source rather than trusted from compiled interfaces, and the checker + re-verifies its own work. +| Standard library | `standard-library: none (--no-libraries)`. The modules + import only `Agda.Builtin.*` and the pinned sibling. +| Sibling pin | `sibling:` line: `hyperpolymath/resource-algebra` `cf9235c532712a783a404c359a1055f40134794a`, fetched by - `scripts/fetch-siblings.sh`; consumed by pin, not re-declared here -| Result | The two modules in this receipt type-check; the fixtures under - `tests/reject-agda/` are refused *with the message each fixture names*, so a - fixture that starts passing, or starts failing for the wrong reason, fails the - gate -| Transfer | `Reversibility.agda`, `TransactionAtomicity.agda`, - `scripts/fetch-siblings.sh` and `agda-proofs.yml` are byte-identical at that - commit and at this branch's HEAD (blobs `0d30206…`, `38c9b06…`, `9b66a48…`, - `7c7e653…`), so the receipt covers those two rows as they stand. It does - **not** cover `Epistemic.agda` (new) or the changed `check-agda.sh`: their - first CI evidence is the run on this branch's pull request + `scripts/fetch-siblings.sh`. +| Import cone | `cone():` lines, from Agda's own `--dependency-graph`. + At this writing: + `Reversibility` → `ResourceAlgebra.{Core,Instances.Loss,Prelude}` plus + builtins; `TransactionAtomicity` → `ResourceAlgebra.Prelude` plus builtins; + `Epistemic` → builtins only. +| Axioms | `--safe`, which refuses `postulate` and the unsafe pragmas in every + module checked; and `escape-hatch-scan:`, a comment-aware scan of every + cone file the checker does not ship (3 first-party, 3 sibling) for + `postulate`, trust primitives, check-disabling pragmas and unsafe + options. The scanner proves itself on every run against one clean control + and four planted hatches, so a scanner that stopped matching would fail + the gate. `Agda.Primitive` and `Agda.Builtin.*` bind the checker's + BUILTINs. They ship with the pinned checker and are attributed to it. +| Input digest | `input:` lines (SHA-256 per scanned file) and `input-digest:` + over them. +| Source commit | `source:` line, the full 40-character commit. +| Result | The three modules type-check, and each fixture under + `tests/reject-agda/` is refused with the message it names. |=== -That is a Grade 3 receipt in mathesis terms: the propositions type-check in -Agda, in CI, at a named commit, with the prover version pinned and recorded. -mathesis §5 illustrates "strict solver flags" with `--safe --erasure`; -januskey's strictness is `--safe --without-K` plus `--double-check`, which is -the same family and stricter than bare `--safe` (no K, no trusted compiled -interfaces, a second checking pass). -Nothing here has been translated to Rocq, Lean or Isabelle, so it is not -Grade 2i, and no headless proof service is involved, so it is not Grade 1. - -=== Why it stops at Grade 3 - -Grade 2i and above would 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 -in a second prover does not establish the same proposition unless the -correspondence is checked too. - -== The §2.1 invocation: adopted, and measured (2026-11-01) - -PROOF-POLICY §2.1's canonical form is -`agda --safe --without-K --cubical-compatible `. Until this branch -the gate ran `--safe --without-K --no-libraries --ignore-interfaces ---double-check` without the cubical flag, and an earlier revision of this page -predicted that adding it would fail, because the flag is *infectious* (direct -imports must use it too) and every module of the pinned sibling opens with -`{-# OPTIONS --safe --without-K #-}`. - -**That prediction was wrong and is withdrawn.** With Agda 2.6.4.3 installed in -the sandbox (PyPI wheel `agda==2.6.4.3.post1`, reporting -`Agda version 2.6.4.3-56f5f56`, the same version CI pins), the canonical -invocation type-checks both modules: - -[source,text] ----- -$ agda --safe --without-K --cubical-compatible --no-libraries \ - --ignore-interfaces --double-check \ - -i verification/proofs/agda -i _build/dependencies/resource-algebra/src \ - verification/proofs/agda/Reversibility.agda - → exit 0, 14 × warning: -W[no]UnsupportedIndexedMatch - -$ … verification/proofs/agda/TransactionAtomicity.agda - → exit 0, 16 × warning: -W[no]UnsupportedIndexedMatch - -$ AGDA=/tmp/tc/bin/agda bash scripts/check-agda.sh - → [PASS] refused as expected: tests/reject-agda/{CommitWhenIdle,ForwardRollback,HiddenLoss,ReviveAfterObliterate} - → [check-agda] OK ----- - -Agda warns where the earlier reading expected it to refuse: a `--without-K` -import is accepted, and what it reports is that particular clauses — the -sibling's `≤-trans`, and `obliterate-absorbs` here — will not compute when -applied to cubical transports. That is a statement about computation under -transport, not about the propositions these modules prove, so the gate keeps the -warnings visible rather than silencing them with `-WnoUnsupportedIndexedMatch`. - -`scripts/check-agda.sh` now runs the canonical invocation, so januskey matches -§2.1 exactly and is still stricter in two other respects (`--ignore-interfaces` -re-checks the sibling from source instead of trusting compiled interfaces; -`--double-check` re-verifies the type-checker's own work). - -=== Receipt bookkeeping for that change - -The CI receipt in the table above was produced **before** the flag changed. -Changing a graded artefact's checker invalidates its receipt's exactness, so: - -* the local run above is recorded as **reproduction** — same prover version, - PyPI provenance instead of Debian, and no CI provenance at all (PROOF-POLICY - §2.3: receipts of execution come from CI); -* the next `agda-proofs.yml` run on `main` is the new receipt, and this page - must cite it in place of the local run once it exists. Until then the rows - stay `AGDA-VERIFIED` on the strength of the four artefacts being unchanged - plus a matching local run, and that is the strongest claim available. - -One related inconsistency is an open obligation, not a claim: the Agda version -is pinned twice in CI and the two pins differ — `agda-proofs.yml` installs -2.6.4.3 (the receipt above), while `dashboard-check.yml` installs 2.6.3 on the -Idris2 image so it can run the PROVEN rows' checkers. A green dashboard -therefore does not extend the receipt at 2.6.4.3. One version, one receipt: -pinning the dashboard job to the same Agda is the fix. - -=== Upgrade path, measured - -`agda==2.7.0.1` runs in the sandbox once its wheel's missing `data/lib` is -supplied (bare install dies with "The lib directory … does not exist"), and -under 2.7.0.1 **both modules also type-check, exit 0**. The latest upstream -release is 2.8.0.2 (2026-09-13), which has not been tried. None of this is a -recommendation to move: the CI pin is Debian trixie's 2.6.4.3, and an upgrade -means a new container, a new pin and a new receipt. - -The sandbox's installable set, and the exact hosts that block Rust, Creusot and -Idris2, are recorded in `docs/estate/environment-toolchains.md`. - -== Grades, ledger row by ledger row - -The 47 ledger rows fall into three classes under PROOF-POLICY §1. Counts are -from `PROOF-NEEDS.adoc` at this commit and are `PROVEN` 12, `TESTED` 23, -`ASSUMED` 4, `DESIGNED` 3, `OPEN` 5. - -=== Grade 3 — theory, proved in Agda - -[cols="1,3,2",options="header"] +Caveat, not an axiom: Agda reports `UnsupportedIndexedMatch` warnings (14 in +`Reversibility`, 16 in `TransactionAtomicity`, 2 in `Epistemic`, including the +sibling's `≤-trans`). These clauses would not compute under cubical +transports. That is a statement about computation, not about the propositions, +so the gate leaves the warnings visible. + +=== Receipt lineage + +[cols="1,2,1,3",options="header"] |=== -| 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` -| 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` -| 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 | - `Epistemic.agda::adversary-ignorant`, `obliterate-cuts-recovery`, - `obliterate-ignorance`, `rotate-forgets-old` +| Run | Commit | State | Why + +| https://github.com/hyperpolymath/januskey/actions/runs/40867211509[40867211509] +| `4afb710e86646658f667f10bd6274ee47416bfc7` +| `superseded` +| Flags `--safe --without-K` without `--cubical-compatible`: §2.1 makes this + historical evidence, not a receipt. Predates `Epistemic.agda`, so it never + covered E-1m. + +| https://github.com/hyperpolymath/januskey/actions/runs/41687715055[41687715055] +| `fc188c44906faedfe91bfd414be3fda01ff4caf4` +| `superseded` +| First run under §2.1's flags, covering all five rows. Replaced by later + runs on the same graded bytes. Its log records version and flags, but no + import cone and no postulate scan. + +| https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251] +| `23bc8c38160a25c37917bce69cf05d91899b07e5` +| `superseded` by this change +| Same graded bytes as 41687715055 and green. Also lacks the cone and the + scan. This change edits comments in two graded modules and adds those + fields to the gate, so the run on its merge commit supersedes it. |=== -These five are the only rows in this repository with a mathesis grade. 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 -freshness of the transaction id (T-7, `ASSUMED`, probabilistic), the absence of -I/O, and, for E-1m, that the modelled channels are the only ones an attacker -has (X-1). §6 asks for the axioms to be tracked; they are, in the modules' -own "What is NOT claimed" blocks and in the ledger's T-6, T-7, G-2, X-1 rows. +*The current receipt is the green `agda-proofs.yml` run on the latest commit +of `main`.* It is the first receipt that carries every field §8.2 lists. Until +then the grade rests on the kernel runs above. Those runs prove the same +propositions with `--safe` in force, but they never recorded the cone, so they +are kept as evidence rather than cited as complete receipts. A red run on +`main` makes that receipt `regressed`, and the five rows fall to `ungraded` +until it is fixed (§8.4 rule 4). -=== Engineering contracts — no mathesis grade applies +=== One checker, two pins: an open obligation -Seven `PROVEN` rows are Idris2 theorems about this ABI: A-1, A-2, C-1, C-2, -C-3, C-4, C-5, checked by -`idris2 --typecheck src/abi/januskey-abi.ipkg`. Under PROOF-POLICY §1 these -are interface and wire-format contracts, so the theory ladder does not grade -them — they are `PROVEN` in the ledger's own vocabulary and that is the whole -of the claim. The `Rust/SPARK` shorthand is withdrawn; the mapping that -replaces it is Rust → **Creusot**, Ada → SPARK, API/ABI → Idris2, theory → -Agda. +`agda-proofs.yml` pins Agda 2.6.4.3, the receipt above. `dashboard-check.yml` +installs Agda 2.6.3 on the Idris2 image so that it can run the PROVEN rows' +checkers. Both are green, but a green dashboard is not a receipt at 2.6.4.3. +Pinning the dashboard's Agda to the same version means choosing a base +image, which is an owner decision. -The same heading covers every `TESTED` row (23): a test proves behaviour was -observed, never that it always holds. G-2 (the Idris2 ↔ Agda correspondence) is -`ASSUMED` by transcription and would have to become mechanical before any -"every operation is reversible" theorem could cite both halves. +== Design review of the graded theorems (2026-11-09) -=== Not graded, and what would grade them +A grade counts witnesses. It does not measure how much a theorem says. This +review records what each graded row actually establishes, so that a reader +does not take a `PWG-3` statement for more than it is. [cols="1,2,3",options="header"] |=== -| Rows | Today | What moves them - -| E-1 (`OPEN`) — the cryptographic claim that an attacker cannot recover - obliterated content or use a revoked key -| Its model-level shadow is proved as E-1m, and the row stays OPEN because a - model of channels is not a statement about cryptography. -| Nothing in Agda: recovering from ciphertext is the assumption X-1. Only a - different kind of evidence (a cryptanalysis, or a reduction) would move it, and - this repository would record that as an external assumption with its source. - -| `TESTED` rows describing Rust behaviour (T-4, T-5, the property tests) -| Claimed, tested. No Creusot annotation exists and Creusot is not installed in - the session that wrote this file. -| Creusot contracts on the Rust functions, run in CI: PROOF-POLICY §1 sends - first-party Rust behaviour to Creusot, not to Idris2 and not to Agda. - -| T-6, T-7, X-1, G-2, E-1, G-3 (`ASSUMED` / `OPEN`) -| 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 - strong as its weakest step"). - -| V-1, V-2, V-3 (`DESIGNED`) -| 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. +| Row and theorem | Kind | What it establishes, and its limits + +| G-1 `all-lossless-trace`, `lossless-trace-all`, `obliterate-absorbs`, + `obliterated-not-lossless` +| Substantive (induction over traces) +| The grade algebra: a trace is lossless exactly when every step is, and one + obliterating step makes the whole trace `inf`. Grades are annotations on + steps. Nothing derives a step's grade from its code. + +| G-1 `wrap-unwrap-𝟙`, `wrap-unwrap-id` +| Definitional or premise-restating +| `wrap-unwrap-𝟙` is `refl`, because both steps are annotated `fin 0`. + `wrap-unwrap-id` returns the record's own `cancels` premise. Their content + is the premise, which is TESTED as `execute_then_undo_is_identity`. + +| T-1 `rollback-restores` +| Substantive (induction over executed lists) +| Undoing a fully executed list in reverse restores the start state, given + each step's undo law (T-6, ASSUMED). `ForwardRollback.agda` pins that + execution-order undo is refused. + +| T-2 `lifecycle-preserves-good`, T-3 `at-most-one-active` +| Substantive (case analysis and list lemmas) +| The four transitions keep `Good`, rewrite only the Active transaction, and + leave at most one Active. The model matches the Rust by transcription (T-11, + ASSUMED). The premise `Good` is now checked when a log is loaded (T-10, + TESTED). Before 2026-11-09 a hand-edited or foreign log could start the + Rust outside the invariant, and the unused `TransactionManager::active_mut` + could change a transaction outside the four transitions. That method has + been removed. + +| E-1m `adversary-ignorant`, `obliterate-ignorance` +| Witness-specific +| Proved for two particular worlds whose stores differ and whose adversary + observations are both empty. The general form is + `different-store-unknown`, which needs such a pair as its hypothesis. These + statements show that ignorance is expressible and true in the model. They + do not show that the adversary is ignorant in every januskey state. + +| E-1m `obliterate-cuts-recovery` +| Substantive (small) +| After obliterating `h`, the model store holds nothing at `h`. + +| E-1m `rotate-forgets-old` +| Definitional +| Holds because the model's `rotate` sets the old key unusable for every + agent. `OldKeyStillUsable.agda` pins that the opposite is refused, but no + link exists to the Rust key subsystem. +|=== + +No row was found false. The two corrections that follow from this review are +made in this change: rows T-10 and T-11 now exist, and the narrower reading +of E-1m above is recorded. They do not change any grade. + +== Not graded, and why + +=== Idris2 ABI rows (engineering) + +A-1, A-2 and C-1 to C-5 are `PROVEN` Idris2 theorems, checked by +`idris2 --typecheck src/abi/januskey-abi.ipkg` (in `idris-abi.yml` and +`dashboard-check`). §8.1 does not grade engineering proofs. G-2 (Idris2 +`IsCNO`/`ReversibleOp` against Agda `ReversiblePair`) is `ASSUMED`, by +transcription. + +=== Rust obligations (Creusot, Pearlite and Verus) + +PROOF-POLICY §1.2 asks for the implementation entrypoint, the verifier, the +specification, the assumptions and the result of each obligation. Both +verifiers are planned by default. + +[cols="1,2,1,1,2",options="header"] +|=== +| Row | Entrypoint | Creusot / Pearlite | Verus | Today + +| T-4 | `cmd_rollback` (`crates/januskey-cli/src/main.rs`) | `OPEN` | `OPEN` | TESTED +| T-5, T-10 | `TransactionManager::{new, begin, add_operation, commit, mark_rolled_back}`, `write_atomic` (`crates/reversible-core/src/transaction.rs`) | `OPEN` | `OPEN` | TESTED +| T-8 | `MetadataStore::{append, mark_undone, prune, purge_path_entries}` (`crates/reversible-core/src/metadata.rs`) | `OPEN` | `OPEN` | TESTED +| S-1, S-2 | `ContentStore::{hash_path, store}` (`crates/reversible-core/src/content_store.rs`) | `OPEN` | `OPEN` | TESTED |=== +Every `OPEN` here has the same reason. No Creusot or Verus toolchain is set up +in this repository or its CI, and the agent sandboxes that wrote these rows +could not install one (`docs/estate/environment-toolchains.md`). Next action: +pick the smallest obligation, T-10's invariant check, write it as a Pearlite +contract and a Verus specification, and add a pinned CI job for each. File I/O +(T-5, T-8, S-2) sits at the edge of what either verifier models, so a +contract there covers the in-memory logic, with the filesystem as an +`ASSUMED` boundary. + +=== Other rows + +T-6, T-7, T-11, X-1 and G-2 are `ASSUMED`. G-3, E-1, T-9, L-1, L-2 and O-1 are +`OPEN`. V-1 to V-3 are `DESIGNED`. Each row names its own gap in +`PROOF-NEEDS.adoc`, and none may borrow the grade of a neighbouring row: "a +row is only as strong as its weakest step" (README-EXPLAINME). + == The epistemic rewrite: E-1 becomes E-1m -The one claim with an inheritance, rather than an invention, behind it. januskey's -Idris2 ABI carries `Knows : Agent → Type → Type` (`Types.idr` §Level 12), a -discrete epistemic modality inherited from the estate's epistemic-types work. It -could not state the security claims the ledger attributed to it: - -* `Knows Adversary a` is uninhabited **by construction** — there is no Adversary - constructor — so "an attacker cannot recover …" (E-1) was a property of a - datatype. The repository's own comment says as much: "a property of this - model, not a security proof". -* "The system forgets the old key" was **unstateable**, because `Knows` has no - negative form. The lemma was deleted rather than repaired, and the ledger - records the deletion. - -`verification/proofs/agda/Epistemic.agda` replaces the modality with one whose -ignorance is a proposition. Knowledge is indiscriminability over an observation -— an agent knows φ in *x* when φ holds in every world it cannot tell apart from -*x* — so: - -* ignorance is `¬ Knows`, proved by exhibiting a world that looks the same and is - not (`adversary-ignorant`, over two worlds that differ only in the store); -* obliteration is a change to the store channel, and recovery is a `Σ` that - becomes empty (`obliterate-cuts-recovery`), with the adversary's ignorance - surviving the operation because its observation did not change - (`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. - -Two fixtures pin the refusals: `AdversaryKnows.agda` (asserting the two stores -are identical — refused, `2 != 1`) and `OldKeyStillUsable.agda` (asserting the -old key survives rotation — refused, `!= true`). - -What this does **not** do is move E-1. A model of channels is not a model of -cryptography: that the store channel is the only one an attacker has, and that a -key which is not `usable` cannot decrypt, are assumptions (X-1), and E-1 stays -`OPEN`. The Idris module is unchanged — its typecheck status, its deleted lemma -and its comments now pointing here — because the theory belongs in Agda under -PROOF-POLICY §1 and the ABI belongs in Idris2. +januskey's Idris2 ABI carries `Knows : Agent → Type → Type` (`Types.idr`, +§Level 12). It could not state the security claims the ledger attributed to it: +`Knows Adversary a` is uninhabited *by construction*, and "the system forgets +the old key" was unstateable, because `Knows` has no negative form. +`verification/proofs/agda/Epistemic.agda` replaces it with knowledge as +indiscriminability over an observation, so that ignorance is a provable +proposition (`¬ Knows`). Its theorems, and what they do not establish, are in +the design review above. E-1 stays `OPEN`. The Idris module is unchanged, +because the theory belongs in Agda (§1) and the ABI in Idris2. == Reporting rules this repository follows -* No percentage, ever. Where a "completion" figure exists elsewhere in the - tree it is a project-plan measure, not a proof measure, and it is not a grade. -* Every grade names its receipt: commit, prover, prover version, flags, - sibling pin. The receipt above is the only one of its kind here. -* A receipt is invalidated by a change to a graded artefact, to its checker or - to its pin, and is then re-earned by the next run, not carried forward. The - blob comparison in §The Grade 3 receipt exists precisely to show which - changes do and do not invalidate it. -* When a graded artefact is replaced, the grade is marked `Superseded`; when a - green receipt goes red and is not immediately fixed, `Regressed`. Neither is - deleted from the history. -* `AGDA-PENDING` is the correct status for a module committed but not yet - checked. No row in this repository is in that state today: the four graded - rows are `AGDA-VERIFIED` at the commit above. +* No percentage for a proof claim, ever. The TOPOLOGY bars are project-plan + measures, not proof measures. +* Every grade is derived from a named receipt, and a receipt names its commit, + checker version, flags, library set, sibling pin, import cone, axiom scan + and inputs. +* A change to a graded artefact, its checker or its pin makes the next run the + receipt. Older receipts are kept with their lineage state and never deleted. +* Always write the `PWG-` prefix. A bare grade number collides with CRG, TRG, + ARG and FRG, and with ECHIDNA's `TrustLevel`, which counts the other way. diff --git a/scripts/agda-cone.sh b/scripts/agda-cone.sh new file mode 100755 index 0000000..2d4529b --- /dev/null +++ b/scripts/agda-cone.sh @@ -0,0 +1,132 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Import cone and escape-hatch scan for the Agda theory modules: the receipt +# fields PROOF-POLICY §8.2 (PWG-3) and §8.4 rule 6 ask for beyond the kernel +# run itself. +# +# * the import cone of each module, as Agda reports it (--dependency-graph); +# * a comment-aware scan of every cone file that is not bound by the checker +# (first-party and pinned sibling) for `postulate` and for the pragmas and +# options that switch a check off; +# * a SHA-256 digest of each scanned file and of the whole input set. +# +# Agda.Primitive and Agda.Builtin.* ship with the pinned checker and bind its +# BUILTINs (Agda.Primitive declares Level by `postulate`, which is how a +# BUILTIN is introduced); they are recorded in the cone and attributed to the +# checker, not scanned. +# +# Usage: agda-cone.sh AGDA RECEIPT_FILE MODULE... (called by check-agda.sh) +# agda-cone.sh --self-test +set -euo pipefail +export LC_ALL="${LC_ALL:-C.UTF-8}" + +# Print the escape hatches in one Agda source, one "file:line: token" each, +# ignoring `--` line comments, nested `{- -}` block comments and string +# literals. A pragma `{-# ... #-}` is code, not a comment, so it is scanned. +scan_file() { + awk -v F="$1" ' + function flag(tok) { printf "%s:%d: %s\n", F, NR, tok; hits++ } + { + line = $0; out = ""; i = 1; n = length(line) + while (i <= n) { + c2 = substr(line, i, 2); c3 = substr(line, i, 3) + if (depth > 0) { + if (c2 == "{-" && c3 != "{-#") { depth++; i += 2; continue } + if (c2 == "-}") { depth--; i += 2; continue } + i++; continue + } + if (inpragma) { + if (c3 == "#-}") { out = out c3; inpragma = 0; i += 3; continue } + out = out substr(line, i, 1); i++; continue + } + if (instr) { + ch = substr(line, i, 1) + if (ch == "\\") { i += 2; continue } + if (ch == "\"") instr = 0 + i++; continue + } + if (c3 == "{-#") { out = out c3; inpragma = 1; i += 3; continue } + if (c2 == "{-") { depth = 1; i += 2; continue } + if (c2 == "--" && (i == 1 || substr(line, i - 1, 1) ~ /[ \t(){};]/)) break + ch = substr(line, i, 1) + if (ch == "\"") { instr = 1; i++; continue } + out = out ch; i++ + } + if (out ~ /(^|[^A-Za-z0-9_-])postulate([^A-Za-z0-9_-]|$)/) flag("postulate") + if (out ~ /primTrustMe|primEraseEquality/) flag("trust primitive") + if (out ~ /\{-#[ \t]*(TERMINATING|NON_TERMINATING|NO_POSITIVITY_CHECK|NO_UNIVERSE_CHECK|INJECTIVE|ETA|REWRITE|BUILTIN[ \t]+REWRITE)/) flag("pragma") + if (out ~ /\{-#[ \t]*OPTIONS/ && out ~ /--(type-in-type|allow-unsolved-metas|allow-incomplete-matches|no-positivity-check|no-termination-check|rewriting|guardedness|sized-types|cubical([ \t]|#|$)|with-K|omega-in-omega|injective-type-constructors)/) flag("option") + } + END { exit (hits > 0) } + ' "$1" +} + +self_test() { + local tmp; tmp="$(mktemp -d)"; trap 'rm -rf "$tmp"' RETURN + printf '%s\n' '-- postulate in a line comment' '{- postulate {- nested -} postulate -}' \ + 'x = "postulate" -- in a string' 'f : Set -- trailing postulate' > "$tmp/clean.agda" + printf '%s\n' 'module M where' 'postulate' ' A : Set' > "$tmp/post.agda" + printf '%s\n' '{-# TERMINATING #-}' 'f : Set' > "$tmp/pragma.agda" + printf '%s\n' '{-# OPTIONS --safe --type-in-type #-}' > "$tmp/option.agda" + printf '%s\n' '{- a comment -} postulate B : Set' > "$tmp/after.agda" + scan_file "$tmp/clean.agda" >/dev/null || { echo "self-test: commented postulates flagged" >&2; return 1; } + local f + for f in post pragma option after; do + if scan_file "$tmp/$f.agda" >/dev/null; then echo "self-test: $f.agda not flagged" >&2; return 1; fi + done + echo "[agda-cone] scanner self-test: 1 clean control passed, 4 planted hatches flagged" +} + +if [ "${1:-}" = "--self-test" ]; then self_test; exit; fi + +prover="$1"; receipt="$2"; shift 2 +self_test +agda_dir="$("$prover" --print-agda-dir)" +flags=(--safe --without-K --cubical-compatible --no-libraries + -i verification/proofs/agda -i _build/dependencies/resource-algebra/src) +mkdir -p _build/check-logs +: > "$receipt" +{ + echo "checker: $("$prover" --version)" + echo "checker-prim-dir: $agda_dir/lib/prim" + echo "flags: ${AGDA_FLAGS:?check-agda.sh passes the flags in force}" + echo "standard-library: none (--no-libraries)" + echo "sibling: hyperpolymath/resource-algebra $(git -C _build/dependencies/resource-algebra rev-parse HEAD)" + echo "source: $(git rev-parse HEAD 2>/dev/null || echo unknown)" +} >> "$receipt" + +declare -A seen=() +scanned=() +for module in "$@"; do + dot="_build/check-logs/$module.deps.dot" + "$prover" "${flags[@]}" --dependency-graph="$dot" "verification/proofs/agda/$module.agda" >/dev/null 2>&1 \ + || { echo "ERROR: could not compute the import cone of $module" >&2; exit 1; } + mapfile -t cone < <(grep -o 'label="[^"]*"' "$dot" | sed 's/^label="//; s/"$//' | sort -u) + [ "${#cone[@]}" -gt 1 ] || { echo "ERROR: empty import cone for $module" >&2; exit 1; } + echo "cone($module): ${cone[*]}" >> "$receipt" + for m in "${cone[@]}"; do + case "$m" in Agda.Primitive|Agda.Builtin.*) continue ;; esac + rel="${m//.//}.agda"; file="" + for dir in verification/proofs/agda _build/dependencies/resource-algebra/src; do + [ -f "$dir/$rel" ] && { file="$dir/$rel"; break; } + done + [ -n "$file" ] || { echo "ERROR: $m is in the cone of $module but no source file was found" >&2; exit 1; } + [ -n "${seen[$file]:-}" ] && continue + seen[$file]=1; scanned+=("$file") + done +done + +hits=0 +for file in "${scanned[@]}"; do + echo "input: $(sha256sum "$file" | cut -d' ' -f1) $file" >> "$receipt" + scan_file "$file" >> "$receipt" || hits=$((hits + 1)) +done +echo "input-digest: $(for f in "${scanned[@]}"; do sha256sum "$f"; done | sha256sum | cut -d' ' -f1) (sha256 over the per-file lines above)" >> "$receipt" +if [ "$hits" -gt 0 ]; then + echo "escape-hatch-scan: FAILED in $hits of ${#scanned[@]} files" >> "$receipt" + cat "$receipt"; echo "ERROR: escape hatch in the import cone (see above)" >&2; exit 1 +fi +echo "escape-hatch-scan: 0 postulates, trust primitives, check-disabling pragmas or options in ${#scanned[@]} first-party and sibling files; Agda.Primitive and Agda.Builtin.* bound by the checker" >> "$receipt" +cat "$receipt" diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 27862c0..d460d0a 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -20,10 +20,15 @@ bash scripts/fetch-siblings.sh # them visible rather than silencing them with -WnoUnsupportedIndexedMatch. flags=(--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check -i verification/proofs/agda -i _build/dependencies/resource-algebra/src) -for module in Reversibility TransactionAtomicity Epistemic; do +modules=(Reversibility TransactionAtomicity Epistemic) +for module in "${modules[@]}"; do "$prover" "${flags[@]}" "verification/proofs/agda/$module.agda" done mkdir -p _build/check-logs +# PWG-3 receipt fields beyond the kernel run (PROOF-POLICY §8.2, §8.4 rule 6): +# the import cone of each module, a comment-aware scan of it for postulates +# and check-disabling pragmas, and the input digests. Printed into this log. +AGDA_FLAGS="${flags[*]}" bash scripts/agda-cone.sh "$prover" _build/check-logs/agda-receipt.txt "${modules[@]}" shopt -s nullglob rejects=(tests/reject-agda/*.agda) shopt -u nullglob diff --git a/verification/proofs/agda/Reversibility.agda b/verification/proofs/agda/Reversibility.agda index 0d30206..2b0ef6b 100644 --- a/verification/proofs/agda/Reversibility.agda +++ b/verification/proofs/agda/Reversibility.agda @@ -16,10 +16,11 @@ -- a TESTED row of the claims ledger in PROOF-NEEDS.adoc. -- -- Pinned sibling: hyperpolymath/resource-algebra, see scripts/fetch-siblings.sh. --- Kernel ruling (2026-10-12): Agda --safe --without-K is the proof kernel; --- the Idris2 ABI (src/abi/JanusKey/ABI) is the runtime layer. The Idris2 --- IsCNO / ReversibleOp pair corresponds to ReversiblePair below by --- transcription (ASSUMED; no mechanical link is claimed). +-- Kernel: Agda, checked by scripts/check-agda.sh under PROOF-POLICY §2.1 +-- (--safe --without-K --cubical-compatible); the Idris2 ABI +-- (src/abi/JanusKey/ABI) is the runtime layer. The Idris2 IsCNO / +-- ReversibleOp pair corresponds to ReversiblePair below by transcription +-- (ASSUMED; no mechanical link is claimed). module Reversibility where diff --git a/verification/proofs/agda/TransactionAtomicity.agda b/verification/proofs/agda/TransactionAtomicity.agda index 38c9b06..bffc807 100644 --- a/verification/proofs/agda/TransactionAtomicity.agda +++ b/verification/proofs/agda/TransactionAtomicity.agda @@ -25,19 +25,23 @@ -- -- 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. The Rust's save behaviour is tested, +-- not proved: a failed save leaves the in-memory log unchanged and the +-- log is replaced by write, sync and rename (ledger row T-5). `Good` is a +-- premise of Part B; a log read from disk is checked against it at load +-- (TransactionManager::new, row T-10, tested), so the premise holds for +-- a loaded log as well as for one this code wrote. -- * 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. +-- the first undo error and leaves the transaction Active with the later +-- operations already undone; the retry skips those and finishes (ledger +-- row T-4, tested). Part A does not model the partial case. -- * 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 +-- (row T-7, assumed; a log broken that way is refused at its next load, +-- row T-10). -- * 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. From 59f1d15693a74613704b556a36d82104b43d03e2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:21:48 +0000 Subject: [PATCH 2/3] ci(dashboard): run Agda 2.6.4.3 from the proof job's image; record the fsync and T-9 decisions Owner decisions of 2026-11-09: - One Agda pin. dashboard-check.yml installed Ubuntu's Agda 2.6.3 on the Idris2 image, which differed from agda-proofs.yml's 2.6.4.3 receipt. The job now runs on the host, and `agda` and `idris2` on PATH are wrappers around the two images the proof jobs already pin: the debian:trixie-slim digest with agda-bin=2.6.4.3-1+b2, and the idris2-pack digest. The job checks the Agda version string exactly as agda-proofs.yml does. Agda runs as the runner user. idris2 runs as root, because its toolchain lives under /root, and the wrapper hands any root-owned file back afterwards, so check-idris-reject.sh can still delete its scratch copy. A failing EXIT trap would otherwise turn a passing row red. - T-5: the directory fsync after the rename stays best-effort. - T-9: to be closed with a write-ahead intent log. Not built yet; still OPEN. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .github/workflows/dashboard-check.yml | 50 +++++++++++++++++++++------ PROOF-NEEDS.adoc | 6 ++-- docs/theory/PROOF-GRADES.adoc | 16 +++++---- 3 files changed, 52 insertions(+), 20 deletions(-) diff --git a/.github/workflows/dashboard-check.yml b/.github/workflows/dashboard-check.yml index 4475ee4..3fc5c44 100644 --- a/.github/workflows/dashboard-check.yml +++ b/.github/workflows/dashboard-check.yml @@ -24,20 +24,50 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 30 # PROVEN rows of the PROOF-NEEDS claims ledger run their checker, so this - # job needs Idris2 (the same pinned image as idris-abi.yml) and Agda. - container: - image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff + # job needs Idris2 and Agda. Each runs from the image its own proof job + # pins, so a green dashboard re-runs the same prover version as the + # receipt: Idris2 from idris-abi.yml's image, Agda 2.6.4.3 from + # agda-proofs.yml's Debian image (before 2026-11-09 this job installed + # Ubuntu's Agda 2.6.3, a second, different pin). `agda` and `idris2` on + # PATH are wrappers that run those images over the checkout. + env: + IDRIS2_IMAGE: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff + AGDA_BASE: debian:trixie-slim@sha256:a29215f6a35e51e22adffa17f89e9d2ef06214e64a2bad10d765c46aea49f11f steps: - - name: Install Agda, and curl for rustup - run: | - apt-get update - apt-get install --no-install-recommends -y ca-certificates curl agda-bin=2.6.3-1build1 - agda --version - idris2 --version - - name: Checkout repository uses: actions/checkout@v7.0.1 + - name: Provers from the pinned images (Agda 2.6.4.3, Idris2) + run: | + printf 'FROM %s\nRUN apt-get update && apt-get install --no-install-recommends -y agda-bin=2.6.4.3-1+b2 && rm -rf /var/lib/apt/lists/*\n' \ + "$AGDA_BASE" | docker build -t januskey-agda:2.6.4.3 - + docker pull -q "$IDRIS2_IMAGE" + mkdir -p "$RUNNER_TEMP/provers" + # Agda runs as the runner user. The Idris2 image keeps its toolchain + # under /root, so idris2 runs as root, and the wrapper then hands any + # root-owned file it left in the working tree back to the runner: a + # checker that cannot clean up its scratch copy would fail its row. + cat > "$RUNNER_TEMP/provers/agda" <<'WRAP' + #!/usr/bin/env bash + exec docker run --rm --user "$(id -u):$(id -g)" -e HOME=/tmp -e LC_ALL=C.UTF-8 \ + -v "$PWD:$PWD" -w "$PWD" --entrypoint agda januskey-agda:2.6.4.3 "$@" + WRAP + cat > "$RUNNER_TEMP/provers/idris2" <<'WRAP' + #!/usr/bin/env bash + docker run --rm -e LC_ALL=C.UTF-8 -v "$PWD:$PWD" -w "$PWD" --entrypoint "" "$IDRIS2_IMAGE" idris2 "$@" + rc=$? + docker run --rm -v "$PWD:$PWD" --entrypoint "" "$IDRIS2_IMAGE" \ + find "$PWD" -xdev -uid 0 -exec chown -h "$(id -u):$(id -g)" {} + + exit "$rc" + WRAP + chmod +x "$RUNNER_TEMP"/provers/* + echo "$RUNNER_TEMP/provers" >> "$GITHUB_PATH" + + - name: Verify the prover versions + run: | + test "$(agda --version)" = 'Agda version 2.6.4.3' + idris2 --version + - uses: dtolnay/rust-toolchain@v1 with: toolchain: stable diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index e66f7cd..da25993 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -71,11 +71,11 @@ tables must agree. | T-2 | begin, add_operation, commit and mark_rolled_back each preserve the log invariant (given a fresh id for begin) and rewrite only the Active transaction, so a completed one is never modified | PROVEN | `+TransactionAtomicity.lifecycle-preserves-good+`; `+tests/reject-agda/CommitWhenIdle.agda+` refused | T-3 | At most one transaction is Active, and exactly one when the active pointer is set | PROVEN | `+TransactionAtomicity.at-most-one-active+` | T-4 | A rollback that fails part-way can be retried to completion | 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 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 (owner decision 2026-11-09), 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; a save that fails leaves mark_undone, prune and purge unapplied in memory, and keeps an append pending for the next save (its file change already happened) | TESTED | `+metadata::tests::save_replaces_rather_than_overwrites_the_log+` (rename, not an in-place write, through `+crate::transaction::write_atomic+`; a plain `+fs::write+` mutant fails it) and `+save_replaces_the_log_atomically+` (no temporary file left) and `+metadata::tests::failed_save_leaves_every_mutation_unapplied+` and `+a_failed_append_keeps_its_record_for_the_next_save+` (memory), and `+transaction::tests::a_failed_save_leaves_the_existing_log_intact+` (disk: the old log survives a save that fails before its temporary file exists); a mutant that updates memory first, and one that removes the log before saving, each fail a test -| T-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` changes the filesystem and then appends its record, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash or failed save between the two leaves a change the log does not know about (on undo: the file restored but the operation still marked not undone, so the retry tries the inverse again). Save ordering cannot close this; it needs a write-ahead intent record, which is a design decision, not a fix +| T-9 | A file operation or undo whose log record fails to persist can be recovered or retried | OPEN | by inspection: every `+execute_*+` changes the filesystem and then appends its record, and `+undo+` runs the inverse and then calls `+mark_undone+`. A crash or failed save between the two leaves a change the log does not know about (on undo: the file restored but the operation still marked not undone, so the retry tries the inverse again). Save ordering cannot close this. Owner decision 2026-11-09: close it with a write-ahead intent log (an intent record written before the file change, completed or undone at startup); not built yet | T-10 | A transaction log read from disk satisfies the invariant `+Good+` that T-2 and T-3 preserve, so their premise holds for a loaded log too; a log that breaks it is refused as corrupted, not loaded | TESTED | `+transaction::tests::a_loaded_log_that_breaks_the_invariant_is_refused+` (five ways of breaking `+Good+`: pointer to a missing or a settled transaction, an Active one with no pointer, two Active, a pointer whose first transaction with that id is settled) and the positive control `+a_log_the_manager_wrote_loads_back+`; mutants (no check at load, last-with-id instead of first, no stray-Active scan) each fail the first test. Before this row the premise was unchecked at load, and the unused `+active_mut+`, which could change a transaction outside the four transitions, has been removed | T-11 | The Agda lifecycle model (`+TransactionAtomicity.Lifecycle+`) corresponds to `+TransactionManager+` (by transcription, like G-2) | ASSUMED | no mechanical link; PROOF-POLICY §2.1: a translated model does not prove runtime refinement. The Rust is tested against the same transitions (T-5, T-10) | 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+`) @@ -284,7 +284,7 @@ the status table above. |T-8: A metadata save that fails leaves mark_undone, prune and purge unapplied in memory, and each retried mutator then applies once with memory and the reloaded log agreeing |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 pending, and the next successful save persists it once (so `jk delete` continuing after one failed record does not lose it) |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 save that fails before creating its temporary file leaves the existing log's bytes intact on disk (failure injected without touching the log; shared by the transaction and metadata logs; a failure after the temporary file exists is not covered) |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` -|T-9: A file operation or undo whose log record fails to persist can be recovered or retried (by inspection: the filesystem changes before the record is saved; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- +|T-9: A file operation or undo whose log record fails to persist can be recovered or retried (by inspection: the filesystem changes before the record is saved; needs a write-ahead intent record, the design chosen 2026-11-09; not built) |OPEN |`crates/januskey-cli/src/operations.rs` |- |T-10: A transaction log read from disk that breaks the lifecycle invariant (pointer to a missing or settled transaction, an Active one with no pointer, two Active, or a settled first transaction with the active id) is refused as corrupted |TESTED |`crates/reversible-core/src/transaction.rs::a_loaded_log_that_breaks_the_invariant_is_refused` |`cargo test --locked -p reversible-core --lib a_loaded_log_that_breaks_the_invariant_is_refused` |T-10: Logs the manager writes, idle and busy, satisfy the invariant and load back (the positive control) |TESTED |`crates/reversible-core/src/transaction.rs::a_log_the_manager_wrote_loads_back` |`cargo test --locked -p reversible-core --lib a_log_the_manager_wrote_loads_back` |T-11: The Agda lifecycle model corresponds to TransactionManager (by transcription) |ASSUMED |`verification/proofs/agda/TransactionAtomicity.agda` |- diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 42d2a1c..46a5258 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -153,13 +153,15 @@ are kept as evidence rather than cited as complete receipts. A red run on `main` makes that receipt `regressed`, and the five rows fall to `ungraded` until it is fixed (§8.4 rule 4). -=== One checker, two pins: an open obligation - -`agda-proofs.yml` pins Agda 2.6.4.3, the receipt above. `dashboard-check.yml` -installs Agda 2.6.3 on the Idris2 image so that it can run the PROVEN rows' -checkers. Both are green, but a green dashboard is not a receipt at 2.6.4.3. -Pinning the dashboard's Agda to the same version means choosing a base -image, which is an owner decision. +=== One checker, one pin (resolved 2026-11-09) + +Until 2026-11-09 `dashboard-check.yml` installed Ubuntu's Agda 2.6.3 on the +Idris2 image, a second pin that differed from the receipt's 2.6.4.3. By owner +decision the dashboard now runs Agda from the image `agda-proofs.yml` pins: +the same `debian:trixie-slim` digest and `agda-bin=2.6.4.3-1+b2`. It runs +Idris2 from the image `idris-abi.yml` pins, and checks the version string as +the proof job does. A green dashboard therefore re-runs the PROVEN rows with +the prover version of the receipt. == Design review of the graded theorems (2026-11-09) From f50da8d160a5b50161454ca296569c0800157499 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:05:14 +0000 Subject: [PATCH 3/3] ci(dashboard): mount the temp dir and copy the prover's lib/prim for main's Agda gate Codex found this on #172. main's scripts/check-agda.sh (#170) writes Agda's dependency graphs under `mktemp -d`. The Agda wrapper mounted only $PWD, so the graphs were written into the container's private /tmp and lost. The gate then reads Agda.Primitive and the other prover modules on the host, at the path `agda --print-agda-dir` reports, and that path existed only inside the image. The wrapper now also mounts $TMPDIR (default /tmp). The setup step copies the image's lib/prim to the same path on the runner and checks that Agda/Primitive.agda arrived. Reproduced locally before the fix, with a stand-in image whose data dir exists only inside the container: "Reversibility.dot: withBinaryFile: does not exist". After the fix, running the workflow's own setup step and then check-agda.sh through the generated wrapper gives: import cone of 7 first-party modules and 8 prover-supplied; both scan controls behave; all seven fixtures refused as named; [check-agda] OK. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .github/workflows/dashboard-check.yml | 15 ++++++++++++++- 1 file changed, 14 insertions(+), 1 deletion(-) diff --git a/.github/workflows/dashboard-check.yml b/.github/workflows/dashboard-check.yml index 3fc5c44..9f605de 100644 --- a/.github/workflows/dashboard-check.yml +++ b/.github/workflows/dashboard-check.yml @@ -47,11 +47,24 @@ jobs: # under /root, so idris2 runs as root, and the wrapper then hands any # root-owned file it left in the working tree back to the runner: a # checker that cannot clean up its scratch copy would fail its row. + # The Agda gate writes its dependency graphs under mktemp -d, so the + # temporary directory is mounted too. It reads the prover's own + # lib/prim (Agda.Primitive, Agda.Builtin.*) on the host, at the path + # `agda --print-agda-dir` reports, so that directory is copied out of + # the image to the same path here. cat > "$RUNNER_TEMP/provers/agda" <<'WRAP' #!/usr/bin/env bash + tmp="${TMPDIR:-/tmp}" exec docker run --rm --user "$(id -u):$(id -g)" -e HOME=/tmp -e LC_ALL=C.UTF-8 \ - -v "$PWD:$PWD" -w "$PWD" --entrypoint agda januskey-agda:2.6.4.3 "$@" + -v "$PWD:$PWD" -v "$tmp:$tmp" -w "$PWD" --entrypoint agda januskey-agda:2.6.4.3 "$@" WRAP + agda_dir="$(docker run --rm --entrypoint agda januskey-agda:2.6.4.3 --print-agda-dir)" + sudo mkdir -p "$agda_dir/lib" + sudo chown "$(id -u):$(id -g)" "$agda_dir/lib" + cid="$(docker create januskey-agda:2.6.4.3)" + docker cp "$cid:$agda_dir/lib/prim" "$agda_dir/lib/prim" + docker rm -f "$cid" >/dev/null + test -f "$agda_dir/lib/prim/Agda/Primitive.agda" cat > "$RUNNER_TEMP/provers/idris2" <<'WRAP' #!/usr/bin/env bash docker run --rm -e LC_ALL=C.UTF-8 -v "$PWD:$PWD" -w "$PWD" --entrypoint "" "$IDRIS2_IMAGE" idris2 "$@"