From 47700b7116e0458a9c381b849f34c138d973f764 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:04:51 +0000 Subject: [PATCH 01/15] =?UTF-8?q?proofs:=20record=20theory=20grades=20as?= =?UTF-8?q?=20PROOF-POLICY=20=C2=A78=20PWG;=20scan=20the=20import=20cone?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The grade records were written against the mathesis brief on 2026-11-01, before the owner ruling of 2026-11-04 made PROOF-POLICY §8 normative: - The five theory rows (G-1, T-1, T-2, T-3, E-1m) are PWG-3, written with the prefix. The brief's "2ii needs Isabelle/HOL" is replaced by §8.3's +foundation-diverse tag. - The receipt is the current green agda-proofs run 42076969251 at 23bc8c3, covering all three modules under the §2.1 canonical invocation, with library pin, flags, import cone and axioms recorded. Runs 41687715055 and 40867211509 are kept as state: superseded. The page had still cited the pre-flag receipt it said it would replace. - The duplicated row counts, which had drifted (23 against 27 TESTED), are removed from PROOF-GRADES; PROOF-NEEDS stays the only count. - Rust's verifiers read Creusot/Pearlite and Verus (§1.2, 2026-11-07). §8.4 asks for a comment-aware postulate scan of the import cone beside --safe. scripts/scan-postulates.sh does that, and check-agda.sh runs it on the proofs and the pinned resource-algebra sibling with a negative and a positive control written at run time. Verified locally: cone 10 files, 0 postulates; a mutant scan that reports nothing fails the gate. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg --- PROOF-NEEDS.adoc | 55 ++++++----- docs/theory/PROOF-GRADES.adoc | 169 +++++++++++++++++++--------------- scripts/check-agda.sh | 19 ++++ scripts/scan-postulates.sh | 40 ++++++++ 4 files changed, 183 insertions(+), 100 deletions(-) create mode 100644 scripts/scan-postulates.sh diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9ea6b33..d0d73b4 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -110,46 +110,45 @@ 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) +=== Proof Witness Grades (PROOF-POLICY §8) 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. +README-EXPLAINME ledger, as used across it. A *Proof Witness Grade* is a second, +orthogonal axis, governed by `+hyperpolymath/standards+` +`+3-practice/PROOF-POLICY.adoc+` §8 (owner ruling 2026-11-04). The mathesis +brief (`+estate-mathematical-architecture+` §5 and §6) first proposed the ladder +and is kept for provenance only. 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+`. +their artefact is Agda (`+verification/proofs/agda/+`). They are **`+PWG-3+`** +(PROOF-POLICY §8, owner ruling 2026-11-04, which governs over the mathesis brief): +each is `+PROVEN+` under the §2.1 invocation and no Rocq or Lean leg exists. The +receipt is a green `+agda-proofs.yml+` run +(https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251]) +at commit `+23bc8c3+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at +`+cf9235c+`, running `+Reversibility+`, `+TransactionAtomicity+` and +`+Epistemic+` under `+--safe --without-K --cubical-compatible+`. Its import cone, +axioms (none) and the receipts it supersedes (runs 41687715055 at `+fc188c4+` +and 40867211509 at `+4afb710+`) are recorded in +link:docs/theory/PROOF-GRADES.adoc[`+docs/theory/PROOF-GRADES.adoc+`]. +Correspondence state 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. +same holds for the TESTED rows, which record observed behaviour and never +grading. First-party Rust behaviour belongs to **Creusot** with **Pearlite** +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 Grade 2i, Grade 2ii or Grade 1, and none is claimed to +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 `+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. +(`+--safe --without-K --cubical-compatible …+`); the CI receipt for that flag +set is run 42076969251 above. === Current State diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 6fed117..60e6367 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -12,32 +12,42 @@ repository, and none is introduced here. == What governs the grades -Two owner documents, both read at HEAD on 2026-11-01: +Since the owner ruling of 2026-11-04, `PROOF-POLICY.adoc` §8 is normative for +grades, and they are written with their prefix: `PWG-3`, `PWG-2i`, `PWG-2ii`, +`PWG-1`, or `ungraded`. The mathesis brief that first proposed the ladder is +kept for provenance only; where the two differ, §8 governs. This page was first +written against the brief (2026-11-01) and was brought in line with §8 on +2026-11-09. [cols="1,2,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` +| §8 Proof Witness Grades +| `PWG-3`: the Agda proof is `PROVEN` under the §2.1 invocation, with the + receipt recording the Agda version, library pin, flags and import cone. + `PWG-2i`: plus one counted Rocq or Lean leg (`RECONCILED`). `PWG-2ii`: plus + both. `PWG-1`: plus current receipts per commit for every counted witness. A + witness in a different foundation (Isabelle/HOL and the like) is the tag + `+foundation-diverse`, never a grade: the brief's "2ii needs Isabelle/HOL" + reading is corrected by §8.3. + +| PROOF-POLICY +| §8.4 rules +| A grade is derived from receipts, never asserted; no percentage, only a + census with its denominator; every counted witness lists its axioms (for + Agda: `--safe`, a comment-aware postulate scan of the import cone, and the + recorded cone); a receipt no longer current carries `state: superseded` or + `state: regressed`, never 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 + first-party Rust is **Creusot** with **Pearlite** contracts, and **Verus** + (§1.2, owner ruling 2026-11-07), 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. @@ -59,11 +69,11 @@ 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. +Proof Witness Grade. -== The Grade 3 receipt +== The PWG-3 receipt -The theory artefacts are two Agda modules: +The theory artefacts are three Agda modules: * `verification/proofs/agda/Reversibility.agda` — the Loss grade algebra: lossless traces have only lossless steps, obliteration absorbs, and a @@ -72,51 +82,70 @@ The theory artefacts are two Agda modules: 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. +* `verification/proofs/agda/Epistemic.agda` — the model-level half of E-1 + (row E-1m, §The epistemic rewrite below). -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: +All three 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, T-3 and E-1m. The +current receipt (PROOF-POLICY §8.2, `PWG-3`): [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) + https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251], + branch `main`, conclusion **success**, `state: current` +| Commit | `23bc8c38160a25c37917bce69cf05d91899b07e5` (started 2026-11-05T17:40:46Z) | 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 +| Library pin | none: `--no-libraries`; the only import outside this tree is the + sibling below +| Flags | `--safe --without-K --cubical-compatible --no-libraries + --ignore-interfaces --double-check`: the §2.1 canonical invocation, plus two + stricter options +| Import cone | roots `Reversibility`, `TransactionAtomicity`, `Epistemic`; the + cone is those modules and `resource-algebra` at `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 + `scripts/fetch-siblings.sh` and re-checked from source under the same flags + (`--ignore-interfaces`); consumed by pin, not re-declared here +| Axioms | none. `--safe` refuses `postulate`; postulate count 0. The + comment-aware scan of the cone (`scripts/scan-postulates.sh`, wired into the + gate with a positive and a negative control on every run) was added after this + run, so its first CI receipt is the next `agda-proofs.yml` run on `main`; + a local run at this receipt's sources reported 10 files, 0 postulates +| Result | The three modules 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 + gate. Agda reports `UnsupportedIndexedMatch` warnings (§The §2.1 invocation + below): they concern computation under cubical transports, not the + propositions, and are kept visible |=== -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. +Earlier receipts, kept with their lineage (§8.4): -=== Why it stops at Grade 3 +[cols="1,1,3",options="header"] +|=== +| Run, commit | State | Why + +| https://github.com/hyperpolymath/januskey/actions/runs/41687715055[41687715055], `fc188c4` +| `superseded` +| Canonical flags and all three modules; replaced by the run above at a later commit +| https://github.com/hyperpolymath/januskey/actions/runs/40867211509[40867211509], `4afb710` +| `superseded` +| Before `--cubical-compatible` and before `Epistemic.agda`; it never covered E-1m +|=== + +That is a `PWG-3` receipt: 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. 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. -Grade 2i and above would require an Agda → Dedukti → Rocq/Lean transport or a +=== Why it stops at PWG-3 + +PWG-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 @@ -168,16 +197,12 @@ re-checks the sibling from source instead of trusting compiled interfaces; === 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. +The local run above is recorded as **reproduction** only: same prover version, +PyPI provenance instead of Debian, and no CI provenance (PROOF-POLICY §2.3: +receipts of execution come from CI). The CI receipt it was waiting for now +exists: the table in §The PWG-3 receipt cites run 42076969251, which ran the +canonical invocation on all three modules, and the receipts from before the +flag changed are marked `superseded` there. 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 @@ -200,11 +225,11 @@ 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. +The ledger rows fall into three classes under PROOF-POLICY §1. `PROOF-NEEDS.adoc` +is the only place the rows are counted: an earlier revision of this page +repeated the counts, and the two copies drifted apart. -=== Grade 3 — theory, proved in Agda +=== PWG-3 — theory, proved in Agda [cols="1,3,2",options="header"] |=== @@ -227,7 +252,7 @@ from `PROOF-NEEDS.adoc` at this commit and are `PROVEN` 12, `TESTED` 23, `obliterate-ignorance`, `rotate-forgets-old` |=== -These five are the only rows in this repository with a mathesis grade. Each +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 freshness of the transaction id (T-7, `ASSUMED`, probabilistic), the absence of @@ -235,7 +260,7 @@ 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. -=== Engineering contracts — no mathesis grade applies +=== Engineering contracts — no Proof Witness Grade applies 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 @@ -336,12 +361,12 @@ PROOF-POLICY §1 and the ABI belongs in Idris2. * 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. + to its pin, and is then re-earned by the next run, not carried forward. +* A receipt that is no longer current carries `state: superseded` (a newer + receipt replaced it) or `state: regressed` (the source no longer checks), with + the reason (PROOF-POLICY §8.4). These are receipt states, not status tokens, + 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`. diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 27862c0..2683b79 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -20,6 +20,25 @@ 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) +# PROOF-POLICY §8.4: a comment-aware postulate scan of the import cone (the +# proofs and the pinned sibling), proved to work both ways on every run. +bash scripts/scan-postulates.sh verification/proofs/agda _build/dependencies/resource-algebra/src +# The controls are written at run time, so no file in the tree carries a real +# postulate for another scanner to count. +controls="$(mktemp -d)" +trap 'rm -rf -- "$controls"' EXIT +mkdir -p "$controls/comments-only" "$controls/planted" +printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \ + '{- postulate {- nested postulate -} postulate -}' 'x-postulate : Set₁' \ + 'x-postulate = Set' > "$controls/comments-only/CommentsOnly.agda" +printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' \ + > "$controls/planted/Planted.agda" +bash scripts/scan-postulates.sh "$controls/comments-only" >/dev/null \ + || { echo "ERROR: postulate scan reported a postulate that is only in comments" >&2; exit 1; } +if bash scripts/scan-postulates.sh "$controls/planted" >/dev/null; then + echo "ERROR: postulate scan missed the planted postulate" >&2; exit 1 +fi +echo "[PASS] postulate scan: cone clean, both controls behave" for module in Reversibility TransactionAtomicity Epistemic; do "$prover" "${flags[@]}" "verification/proofs/agda/$module.agda" done diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh new file mode 100644 index 0000000..1e4d77d --- /dev/null +++ b/scripts/scan-postulates.sh @@ -0,0 +1,40 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Comment-aware postulate scan of an Agda import cone (PROOF-POLICY §8.4, +# "Axioms travel with the grade"): --safe already refuses `postulate`, and this +# scan is the second of the three parts that make the absence of axioms visible +# on a receipt. Text inside nested {- -} comments and after a `--` line comment +# is ignored; pragmas ({-# … #-}) are treated as code. A `--` that starts an +# operator (`-->`) is not a comment, so the scan errs towards reporting. +# +# Usage: scan-postulates.sh DIR... Prints each hit as path:line: text and the +# count; exits 1 if there is any hit, 2 if no .agda file was found. +set -euo pipefail +[ "$#" -gt 0 ] || { echo "usage: $0 DIR..." >&2; exit 2; } +mapfile -t files < <(find "$@" -name '*.agda' -type f | LC_ALL=C sort) +[ "${#files[@]}" -gt 0 ] || { echo "ERROR: no .agda files under: $*" >&2; exit 2; } +hits="$(awk ' + FNR == 1 { depth = 0 } + { + line = $0; code = ""; i = 1; n = length(line) + while (i <= n) { + two = substr(line, i, 2) + if (depth == 0 && two == "{-" && substr(line, i + 2, 1) == "#") { + code = code "{-#"; i += 3; continue + } + if (two == "{-") { depth++; i += 2; continue } + if (depth > 0 && two == "-}") { depth--; i += 2; continue } + if (depth > 0) { i++; continue } + if (two == "--" && (i + 2 > n || substr(line, i + 2, 1) ~ /[ \t]/)) break + code = code substr(line, i, 1); i++ + } + if (code ~ /(^|[^A-Za-z0-9_-])postulate([^A-Za-z0-9_-]|$)/) + printf "%s:%d: %s\n", FILENAME, FNR, line + } +' "${files[@]}")" +count=0 +[ -n "$hits" ] && count="$(printf '%s\n' "$hits" | wc -l | tr -d ' ')" +[ -n "$hits" ] && printf '%s\n' "$hits" +echo "postulate scan: ${#files[@]} files, $count postulate(s)" +[ "$count" -eq 0 ] From a71dc7610b8978c5edd71df2c44e9c9177af4654 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:10:37 +0000 Subject: [PATCH 02/15] docs(proofs): restore T-8/T-9 ledger rows; PWG census; correct proof comments MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Stacked on #170, which records the theory grades as PROOF-POLICY §8 PWG-3 and adds the postulate scan. This adds what #170 does not cover. The ledger lost #168's T-8 and T-9 rows: main still showed T-8 OPEN ("not yet built") although its five tests are green in CI and locally, and T-9 existed only in prose. T-8 now has one TESTED row per test, T-9 is an OPEN row in both tables, and E-1m gains its missing status-table row so the two tables agree. A PWG census with its denominator (§8.4.7): PWG-3 5 of 6 theory theorems, G-3 ungraded. The Rocq and Lean legs are recorded as not attempted (OPEN) rather than `unavailable`: under §2 that route means a leg that cannot be built, and a hand re-proof is always the fallback. Two proof files had misleading comments, though no statement or proof changed. TransactionAtomicity's "What is NOT claimed" block described non-atomic saves and a non-resumable rollback, both since fixed (T-4, T-5, T-8). Reversibility implied that the 𝟙 grade of a wrap/unwrap pair derives from its cancellation law; the grade is assigned. The G-1 and E-1m wording now says so, and the receipt notes the re-earn. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- .machine_readable/6a2/STATE.a2ml | 21 ++++--- PROOF-NEEDS.adoc | 18 +++++- READINESS.adoc | 2 +- .../2026-11-01-mathesis-grade3-receipts.md | 12 ++++ docs/theory/PROOF-GRADES.adoc | 58 +++++++++++++++---- verification/proofs/agda/Reversibility.agda | 12 ++-- .../proofs/agda/TransactionAtomicity.agda | 21 +++---- 7 files changed, 103 insertions(+), 41 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index d68c5af..c53f2e1 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-1, T-2, T-3, E-1m — Agda theory modules under verification/proofs/agda; AGDA-VERIFIED; census 5 of 6 theory theorems, G-3 ungraded" +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 five 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 = "none — no PWG-2i, PWG-2ii or PWG-1 is claimed" [test-categories-complete] unit = true diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index d0d73b4..d5457fd 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -62,10 +62,11 @@ 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 leaves no agent able to use the old key (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 @@ -74,7 +75,8 @@ 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 replaced by write, sync and rename, never overwritten in place; 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 file change whose log record fails to persist is either recorded or reverted: `+execute_*+` changes the filesystem and then appends, and `+undo+` runs the inverse and then marks it, 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 | 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) @@ -134,6 +136,11 @@ and 40867211509 at `+4afb710+`) are recorded in 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 6):* `+PWG-3+` 5 +(G-1, T-1, T-2, T-3, E-1m) · `+PWG-2i+` 0 · `+PWG-2ii+` 0 · `+PWG-1+` 0 · +`+ungraded+` 1 (G-3). The Rocq and Lean legs of all five have not been +attempted; each row 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 @@ -252,6 +259,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,7 +277,7 @@ 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-9: A file change whose log record fails to persist is either recorded or reverted (execute changes the filesystem then appends; undo runs the inverse then marks it; needs a write-ahead intent record) |OPEN |`crates/reversible-core/src/metadata.rs` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- |T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |- |Every operation is reversible (MPR), as a theorem linked to the Rust (needs G-2 made mechanical, and G-3) |OPEN |`verification/proofs/agda/Reversibility.agda` |- diff --git a/READINESS.adoc b/READINESS.adoc index ef390ea..a1b93fc 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 at PWG-3 under PROOF-POLICY §8 — 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 60e6367..62276f5 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,17 @@ 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 6):* +`PWG-3` 5 (G-1, T-1, T-2, T-3, E-1m) · `PWG-2i` 0 · `PWG-2ii` 0 · `PWG-1` 0 · +`ungraded` 1 (G-3, `OPEN`: no Agda statement yet). `+foundation-diverse`: none. +Axioms: none. The denominator is the ledger rows whose source of truth is, or is +to be, an Agda theorem. 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`) are outside it. +==== + == What governs the grades Since the owner ruling of 2026-11-04, `PROOF-POLICY.adoc` §8 is normative for @@ -123,6 +134,17 @@ current receipt (PROOF-POLICY §8.2, `PWG-3`): propositions, and are kept visible |=== +*Re-earn pending (2026-11-09).* The change that follows this receipt 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 this receipt +does not cover them. The `agda-proofs.yml` run on that change, and after merge +the run on `main`, re-earns it; this receipt then becomes `state: superseded`. +A local run of the same invocation with the same Agda version passes on the new +bytes (three modules checked, six fixtures refused); that is a reproduction, not +a receipt (§2.3). + Earlier receipts, kept with their lineage (§8.4): [cols="1,1,3",options="header"] @@ -236,8 +258,11 @@ 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` @@ -247,7 +272,8 @@ repeated the counts, and the two copies drifted apart. `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 | + leaves no agent — the system included — able to use the old key (true by the + definition of `rotate` in the model) | `Epistemic.agda::adversary-ignorant`, `obliterate-cuts-recovery`, `obliterate-ignorance`, `rotate-forgets-old` |=== @@ -306,11 +332,12 @@ 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 (`OPEN`) +| A file change whose log record fails to persist: `execute_*` changes the + filesystem and then appends, and `undo` runs the inverse and then marks it. + (T-8, the metadata log's own saves, is TESTED since #168.) +| A write-ahead intent record, which is a design decision, then a test that + injects the failure between the two steps. |=== == The epistemic rewrite: E-1 becomes E-1m @@ -341,7 +368,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 @@ -368,5 +397,10 @@ 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. 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/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/TransactionAtomicity.agda b/verification/proofs/agda/TransactionAtomicity.agda index 38c9b06..913cbad 100644 --- a/verification/proofs/agda/TransactionAtomicity.agda +++ b/verification/proofs/agda/TransactionAtomicity.agda @@ -25,19 +25,20 @@ -- -- 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 behaviour on a failed or +-- interrupted save is TESTED, not proved: a failed save leaves the +-- in-memory log unchanged, and the log is replaced by write, sync and +-- rename (ledger rows T-5 and T-8). 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. From 77fcedbff8668b13efacfe7c9f74a0c84cc32c3a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:18:25 +0000 Subject: [PATCH 03/15] proofs: scan the import cone Agda reports; mark the receipt pending re-run MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review on #170 (Codex, CodeRabbit), each finding checked: - The cone is now the module set `agda --dependency-graph` reports for the three roots, resolved to files on the include path and in Agda's own library; an unresolved module fails the gate. The directory scan both missed the 8 prover-supplied modules and swept in unimported ones. - First-party modules (6) must have no postulate. Agda.Primitive's universe-level primitives (Level, lzero, lsuc, _⊔_, bound by BUILTIN) are reported as the prover's trusted base; a postulate in any other prover-supplied module fails. - The scanner takes explicit files, refuses unreadable ones, and lexes `--` comments with no space, and string and character literals. - Controls must exit exactly 0 and 1, and the planted one must be named. - Run 42076969251 predates the changed gate, so it is recorded as the last receipt for the modules; the first green run of this gate on main replaces it. - The stale "23 TESTED" is gone; Rust guidance names Creusot/Pearlite and Verus throughout. Verified locally: gate OK (6 first-party, 0 postulates; 2 BUILTIN blocks in Agda.Primitive); a never-reporting scanner, a comment-blind scanner and a planted postulate in Epistemic.agda each fail the gate. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg --- PROOF-NEEDS.adoc | 11 ++++-- docs/theory/PROOF-GRADES.adoc | 63 ++++++++++++++++++++----------- scripts/check-agda.sh | 71 ++++++++++++++++++++++++++--------- scripts/scan-postulates.sh | 50 ++++++++++++++++-------- 4 files changed, 135 insertions(+), 60 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index d0d73b4..0172a0a 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -124,13 +124,16 @@ Of the 12 PROVEN rows, five are the theory rows — **G-1, T-1, T-2, T-3, E-1m** their artefact is Agda (`+verification/proofs/agda/+`). They are **`+PWG-3+`** (PROOF-POLICY §8, owner ruling 2026-11-04, which governs over the mathesis brief): each is `+PROVEN+` under the §2.1 invocation and no Rocq or Lean leg exists. The -receipt is a green `+agda-proofs.yml+` run +last receipt for the modules is a green `+agda-proofs.yml+` run (https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251]) at commit `+23bc8c3+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at `+cf9235c+`, running `+Reversibility+`, `+TransactionAtomicity+` and -`+Epistemic+` under `+--safe --without-K --cubical-compatible+`. Its import cone, -axioms (none) and the receipts it supersedes (runs 41687715055 at `+fc188c4+` -and 40867211509 at `+4afb710+`) are recorded in +`+Epistemic+` under `+--safe --without-K --cubical-compatible+`. The gate gained +an import-cone postulate scan after it, so the first green run of the changed +gate on `+main+` is the receipt that replaces it. The cone, the axioms (none in +the development; the prover's universe-level primitives are reported) and the +superseded receipts (runs 41687715055 at `+fc188c4+` and 40867211509 at +`+4afb710+`) are recorded in link:docs/theory/PROOF-GRADES.adoc[`+docs/theory/PROOF-GRADES.adoc+`]. Correspondence state for them: `+AGDA-VERIFIED+`. diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 60e6367..a5d79ef 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -86,8 +86,15 @@ The theory artefacts are three Agda modules: (row E-1m, §The epistemic rewrite below). All three 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, T-3 and E-1m. The -current receipt (PROOF-POLICY §8.2, `PWG-3`): +also the ledger's recorded checker for rows G-1, T-1, T-2, T-3 and E-1m. + +The gate changed in hyperpolymath/januskey#170: it now derives the import cone +from Agda and scans it for postulates. A changed checker has to re-earn its +receipt (§8.4), so the receipt below is the **last receipt for the three +modules**, not yet a receipt for this gate. The first green `agda-proofs.yml` run +on `main` after #170 is the receipt for the gate, and replaces this row, which +then becomes `state: superseded`. Until then the grade is `PWG-3`, receipt +pending re-run. [cols="1,3",options="header"] |=== @@ -95,7 +102,8 @@ current receipt (PROOF-POLICY §8.2, `PWG-3`): | Workflow, run | `agda-proofs.yml`, run https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251], - branch `main`, conclusion **success**, `state: current` + branch `main`, conclusion **success**; last receipt for the modules, before + the gate change above | Commit | `23bc8c38160a25c37917bce69cf05d91899b07e5` (started 2026-11-05T17:40:46Z) | Prover | `agda-bin=2.6.4.3-1+b2` on Debian trixie-slim (`@sha256:a29215f6…`), asserted by a passing step: @@ -105,16 +113,23 @@ current receipt (PROOF-POLICY §8.2, `PWG-3`): | Flags | `--safe --without-K --cubical-compatible --no-libraries --ignore-interfaces --double-check`: the §2.1 canonical invocation, plus two stricter options -| Import cone | roots `Reversibility`, `TransactionAtomicity`, `Epistemic`; the - cone is those modules and `resource-algebra` at - `cf9235c532712a783a404c359a1055f40134794a`, fetched by +| Import cone | the module set Agda reports with `--dependency-graph` for the + roots `Reversibility`, `TransactionAtomicity` and `Epistemic`: 14 modules. + First-party (6): the three roots and `ResourceAlgebra.Prelude`, + `ResourceAlgebra.Core` and `ResourceAlgebra.Instances.Loss` from + `resource-algebra` at `cf9235c532712a783a404c359a1055f40134794a`, fetched by `scripts/fetch-siblings.sh` and re-checked from source under the same flags - (`--ignore-interfaces`); consumed by pin, not re-declared here -| Axioms | none. `--safe` refuses `postulate`; postulate count 0. The - comment-aware scan of the cone (`scripts/scan-postulates.sh`, wired into the - gate with a positive and a negative control on every run) was added after this - run, so its first CI receipt is the next `agda-proofs.yml` run on `main`; - a local run at this receipt's sources reported 10 files, 0 postulates + (`--ignore-interfaces`). Supplied with the prover (8): `Agda.Primitive` and + `Agda.Builtin.{Bool,Equality,List,Maybe,Nat,Sigma,Unit}` +| Axioms | none in the development. `--safe` refuses `postulate`, and the + comment-aware scan (`scripts/scan-postulates.sh`) finds 0 postulates in the + six first-party modules. The prover-supplied `Agda.Primitive` declares the + universe-level primitives (`Level`, `lzero`, `lsuc`, `_⊔_`) by two `postulate` + blocks, each bound by a `BUILTIN` pragma: they are the prover's trusted base, + not axioms of this development, and the gate reports them rather than hiding + them; a postulate in any other prover-supplied module fails it. The scan is + new in #170, so its first CI receipt is the run that replaces this row; the + figures here are from a local run at this receipt's sources | Result | The three modules 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 @@ -137,9 +152,10 @@ Earlier receipts, kept with their lineage (§8.4): | Before `--cubical-compatible` and before `Epistemic.agda`; it never covered E-1m |=== -That is a `PWG-3` receipt: 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. Nothing here has been translated to Rocq or Lean, so no +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. @@ -268,10 +284,10 @@ C-3, C-4, C-5, checked by 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. +replaces it is Rust → **Creusot** with **Pearlite** contracts, and **Verus** +(§1.2), Ada → SPARK, API/ABI → Idris2, theory → Agda. -The same heading covers every `TESTED` row (23): a test proves behaviour was +The same heading covers every `TESTED` row: 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. @@ -291,10 +307,13 @@ observed, never that it always holds. G-2 (the Idris2 ↔ Agda correspondence) i 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. +| Claimed, tested. No Creusot/Pearlite contract or Verus proof exists, and + neither verifier is installed in the session that wrote this file. +| Contracts and proofs on the Rust functions, run in CI: PROOF-POLICY §1.2 + plans first-party Rust for both Creusot (with Pearlite) and Verus, whose + scopes may differ; a property proved by one need not be duplicated in the + 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`) | Premises, external assumptions, or filed obligations. diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 2683b79..33782af 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -20,28 +20,63 @@ 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) -# PROOF-POLICY §8.4: a comment-aware postulate scan of the import cone (the -# proofs and the pinned sibling), proved to work both ways on every run. -bash scripts/scan-postulates.sh verification/proofs/agda _build/dependencies/resource-algebra/src +# The working directory for this run: the dependency graphs Agda writes and the +# scan's controls. Removed on exit. +work="$(mktemp -d)" +trap 'rm -rf -- "$work"' EXIT +modules=(Reversibility TransactionAtomicity Epistemic) +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 +# 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" +own=(); prover_lib=() +while IFS= read -r name; do + found="" + for root in verification/proofs/agda _build/dependencies/resource-algebra/src "$agda_prim"; do + candidate="$root/${name//.//}.agda" + if [ -f "$candidate" ]; then found="$root"; break; fi + done + [ -n "$found" ] || { echo "ERROR: cannot resolve module $name of the import cone to a source file" >&2; exit 1; } + if [ "$found" = "$agda_prim" ]; then prover_lib+=("$candidate"); else own+=("$candidate"); fi +done < <(sed -n 's/.*label="\([^"]*\)".*/\1/p' "$work"/*.dot | LC_ALL=C sort -u) +[ "${#own[@]}" -gt 0 ] || { echo "ERROR: Agda reported no first-party module in the import cone" >&2; exit 1; } +echo "import cone: ${#own[@]} first-party modules, ${#prover_lib[@]} supplied with the prover" +# The proofs and the pinned sibling: no postulate at all. +bash scripts/scan-postulates.sh "${own[@]}" +# Modules supplied with the prover are its trusted base. The only postulates +# allowed there are Agda.Primitive's universe-level primitives (Level, lzero, +# lsuc, _⊔_, each bound by a BUILTIN pragma); they are reported, not hidden, and +# a postulate in any other prover-supplied module of the cone fails the gate. +if [ "${#prover_lib[@]}" -gt 0 ]; then + status=0; bash scripts/scan-postulates.sh "${prover_lib[@]}" >"$work/prover.log" 2>&1 || status=$? + [ "$status" -le 1 ] || { cat "$work/prover.log"; exit 1; } + if grep -E '^[^ ]+:[0-9]+: ' "$work/prover.log" | grep -vqF -- "/Agda/Primitive.agda:"; then + cat "$work/prover.log"; echo "ERROR: a postulate in a prover-supplied module other than Agda.Primitive" >&2; exit 1 + fi + echo "prover-supplied: $(grep -cE '^[^ ]+:[0-9]+: ' "$work/prover.log" || true) postulate block(s), all in Agda.Primitive (universe-level primitives)" +fi + # The controls are written at run time, so no file in the tree carries a real -# postulate for another scanner to count. -controls="$(mktemp -d)" -trap 'rm -rf -- "$controls"' EXIT -mkdir -p "$controls/comments-only" "$controls/planted" +# postulate for another scanner to count. Each must give exactly its exit code. printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \ - '{- postulate {- nested postulate -} postulate -}' 'x-postulate : Set₁' \ - 'x-postulate = Set' > "$controls/comments-only/CommentsOnly.agda" -printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' \ - > "$controls/planted/Planted.agda" -bash scripts/scan-postulates.sh "$controls/comments-only" >/dev/null \ - || { echo "ERROR: postulate scan reported a postulate that is only in comments" >&2; exit 1; } -if bash scripts/scan-postulates.sh "$controls/planted" >/dev/null; then - echo "ERROR: postulate scan missed the planted postulate" >&2; exit 1 + '--postulate with no space after the dashes' \ + '{- postulate {- nested postulate -} postulate -}' \ + 'x--postulate : Set₁' 'x--postulate = Set' \ + 's : String' 's = "a postulate in a string \" still the string"' \ + > "$work/CommentsOnly.agda" +printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' > "$work/Planted.agda" +status=0; bash scripts/scan-postulates.sh "$work/CommentsOnly.agda" >"$work/neg.log" 2>&1 || status=$? +[ "$status" -eq 0 ] || { cat "$work/neg.log"; echo "ERROR: the comments-only control did not exit 0 (got $status)" >&2; exit 1; } +status=0; bash scripts/scan-postulates.sh "$work/Planted.agda" >"$work/pos.log" 2>&1 || status=$? +if [ "$status" -ne 1 ] || ! grep -qF -- "Planted.agda:2:" "$work/pos.log"; then + cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming Planted.agda:2 (got $status)" >&2; exit 1 fi echo "[PASS] postulate scan: cone clean, both controls behave" -for module in Reversibility TransactionAtomicity Epistemic; do - "$prover" "${flags[@]}" "verification/proofs/agda/$module.agda" -done mkdir -p _build/check-logs shopt -s nullglob rejects=(tests/reject-agda/*.agda) diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh index 1e4d77d..8d06ff2 100644 --- a/scripts/scan-postulates.sh +++ b/scripts/scan-postulates.sh @@ -1,40 +1,58 @@ #!/usr/bin/env bash # SPDX-License-Identifier: MPL-2.0 # SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -# Comment-aware postulate scan of an Agda import cone (PROOF-POLICY §8.4, +# Comment-aware postulate scan of Agda source files (PROOF-POLICY §8.4, # "Axioms travel with the grade"): --safe already refuses `postulate`, and this # scan is the second of the three parts that make the absence of axioms visible -# on a receipt. Text inside nested {- -} comments and after a `--` line comment -# is ignored; pragmas ({-# … #-}) are treated as code. A `--` that starts an -# operator (`-->`) is not a comment, so the scan errs towards reporting. +# on a receipt. check-agda.sh passes it the exact import cone that Agda itself +# reports, so the files scanned are the files checked. # -# Usage: scan-postulates.sh DIR... Prints each hit as path:line: text and the -# count; exits 1 if there is any hit, 2 if no .agda file was found. +# Lexing follows Agda closely enough for one keyword: text inside nested +# {- -} comments, after a `--` that starts a token (with or without a space +# after it), and inside string or character literals is ignored; pragmas +# ({-# … #-}) are code. A `--` inside a name such as `x--y` is part of the name. +# +# Usage: scan-postulates.sh FILE... Prints each hit as path:line: text and the +# count; exits 1 if there is any hit, 2 on a usage error or an unreadable file. set -euo pipefail -[ "$#" -gt 0 ] || { echo "usage: $0 DIR..." >&2; exit 2; } -mapfile -t files < <(find "$@" -name '*.agda' -type f | LC_ALL=C sort) -[ "${#files[@]}" -gt 0 ] || { echo "ERROR: no .agda files under: $*" >&2; exit 2; } +[ "$#" -gt 0 ] || { echo "usage: $0 FILE..." >&2; exit 2; } +for f in "$@"; do + [ -f "$f" ] && [ -r "$f" ] || { echo "ERROR: not a readable file: $f" >&2; exit 2; } +done hits="$(awk ' + # Agda name characters are everything except whitespace and .;{}()@" + function namechar(c) { return c != "" && c !~ /[ \t.;{}()@"]/ } FNR == 1 { depth = 0 } { line = $0; code = ""; i = 1; n = length(line) while (i <= n) { - two = substr(line, i, 2) + c = substr(line, i, 1); two = substr(line, i, 2) + prev = (i > 1) ? substr(line, i - 1, 1) : "" if (depth == 0 && two == "{-" && substr(line, i + 2, 1) == "#") { code = code "{-#"; i += 3; continue } if (two == "{-") { depth++; i += 2; continue } if (depth > 0 && two == "-}") { depth--; i += 2; continue } if (depth > 0) { i++; continue } - if (two == "--" && (i + 2 > n || substr(line, i + 2, 1) ~ /[ \t]/)) break - code = code substr(line, i, 1); i++ + if (c == "\"") { # string literal: skip to the closing quote + i++ + while (i <= n && substr(line, i, 1) != "\"") i += (substr(line, i, 1) == "\\") ? 2 : 1 + i++; code = code " "; continue + } + if (c == "'\''" && !namechar(prev)) { # character literal at a token start + i++ + while (i <= n && substr(line, i, 1) != "'\''") i += (substr(line, i, 1) == "\\") ? 2 : 1 + i++; code = code " "; continue + } + if (two == "--" && !namechar(prev)) break + code = code c; i++ } - if (code ~ /(^|[^A-Za-z0-9_-])postulate([^A-Za-z0-9_-]|$)/) + if (code ~ /(^|[ \t.;{}()@])postulate([ \t.;{}()@]|$)/) printf "%s:%d: %s\n", FILENAME, FNR, line } -' "${files[@]}")" +' "$@")" count=0 [ -n "$hits" ] && count="$(printf '%s\n' "$hits" | wc -l | tr -d ' ')" [ -n "$hits" ] && printf '%s\n' "$hits" -echo "postulate scan: ${#files[@]} files, $count postulate(s)" -[ "$count" -eq 0 ] +echo "postulate scan: $# files, $count postulate(s)" +[ "$count" -eq 0 ] || exit 1 From 5f123b947e91c1f55a780486965a459ce4e98fb1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:32:09 +0000 Subject: [PATCH 04/15] docs(proofs): cite the CI receipt for the re-commented proof modules agda-proofs.yml run 42623188471 at a71dc76 checked the edited Reversibility and TransactionAtomicity bytes under the same gate. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- docs/theory/PROOF-GRADES.adoc | 22 ++++++++++++---------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 62276f5..12886d8 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -134,16 +134,18 @@ current receipt (PROOF-POLICY §8.2, `PWG-3`): propositions, and are kept visible |=== -*Re-earn pending (2026-11-09).* The change that follows this receipt 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 this receipt -does not cover them. The `agda-proofs.yml` run on that change, and after merge -the run on `main`, re-earns it; this receipt then becomes `state: superseded`. -A local run of the same invocation with the same Agda version passes on the new -bytes (three modules checked, six fixtures refused); that is a reproduction, not -a receipt (§2.3). +*Re-earned on the change that edits the proof comments (2026-11-09).* That +change 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. Their receipt is +`agda-proofs.yml` run +https://github.com/hyperpolymath/januskey/actions/runs/42623188471[42623188471] +at `a71dc7610b8978c5edd71df2c44e9c9177af4654` (pull request #171, success, the +same container, prover, flags and gate as above, with the postulate scan +included). After merge, the run on `main` is the receipt of record, and run +42076969251 becomes `state: superseded`. Earlier receipts, kept with their lineage (§8.4): From c728a8c8d2d321401283947060ebf913ad7d6c17 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:39:04 +0000 Subject: [PATCH 05/15] proofs: Agda whitespace in the postulate scan; check Agda.Primitive by name MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The scanner treated only space and tab as keyword boundaries, so a postulate next to NO-BREAK SPACE, a Unicode space separator, CR, FF or VT went unreported. Agda reads every isSpace character other than tab and newline as a space (Agda.Syntax.Parser.Alex, toASCII); the scanner now does the same, byte-wise in the C locale so mawk and gawk agree. The planted control gains a NO-BREAK SPACE case, and the comments-only control `--postulate postulate`. The prover-supplied allowance was the path Agda/Primitive.agda. The gate now requires those blocks to declare exactly Level, lzero, lsuc and _⊔_, each with its BUILTIN binding, so a prover pin that adds a postulate fails. PROOF-NEEDS states the PWG-3 grade as pending its re-run receipt, and PROOF-GRADES cites the green branch run of the changed gate as evidence. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg --- PROOF-NEEDS.adoc | 10 +++++--- docs/theory/PROOF-GRADES.adoc | 12 ++++++--- scripts/check-agda.sh | 46 +++++++++++++++++++++++++++-------- scripts/scan-postulates.sh | 17 ++++++++++--- 4 files changed, 63 insertions(+), 22 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 0172a0a..38a303a 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -121,8 +121,9 @@ and is kept for provenance only. 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 **`+PWG-3+`** -(PROOF-POLICY §8, owner ruling 2026-11-04, which governs over the mathesis brief): +their artefact is Agda (`+verification/proofs/agda/+`). They are **`+PWG-3+`, +receipt pending re-run** (PROOF-POLICY §8, owner ruling 2026-11-04, which +governs over the mathesis brief): each is `+PROVEN+` under the §2.1 invocation and no Rocq or Lean leg exists. The last receipt for the modules is a green `+agda-proofs.yml+` run (https://github.com/hyperpolymath/januskey/actions/runs/42076969251[42076969251]) @@ -131,8 +132,9 @@ at commit `+23bc8c3+`, Agda 2.6.4.3, with `+resource-algebra+` pinned at `+Epistemic+` under `+--safe --without-K --cubical-compatible+`. The gate gained an import-cone postulate scan after it, so the first green run of the changed gate on `+main+` is the receipt that replaces it. The cone, the axioms (none in -the development; the prover's universe-level primitives are reported) and the -superseded receipts (runs 41687715055 at `+fc188c4+` and 40867211509 at +the development; the prover's four universe-level primitives are checked by +name and reported) and the superseded receipts (runs 41687715055 at +`+fc188c4+` and 40867211509 at `+4afb710+`) are recorded in link:docs/theory/PROOF-GRADES.adoc[`+docs/theory/PROOF-GRADES.adoc+`]. Correspondence state for them: `+AGDA-VERIFIED+`. diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index a5d79ef..c9039dc 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -126,10 +126,14 @@ pending re-run. six first-party modules. The prover-supplied `Agda.Primitive` declares the universe-level primitives (`Level`, `lzero`, `lsuc`, `_⊔_`) by two `postulate` blocks, each bound by a `BUILTIN` pragma: they are the prover's trusted base, - not axioms of this development, and the gate reports them rather than hiding - them; a postulate in any other prover-supplied module fails it. The scan is - new in #170, so its first CI receipt is the run that replaces this row; the - figures here are from a local run at this receipt's sources + not axioms of this development. The gate checks that those blocks declare + exactly those four names and that each has its `BUILTIN` binding, and fails on + any other prover-supplied postulate, so a prover pin that adds one does not + pass. The scan is new in #170, so its first receipt on `main` is the run that + replaces this row. The same figures came from the #170 branch in CI under + Agda 2.6.4.3 (run + https://github.com/hyperpolymath/januskey/actions/runs/42624327510[42624327510] + at `77fcedb`; branch evidence, not a receipt) | Result | The three modules 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 diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 33782af..2d98194 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -49,32 +49,58 @@ echo "import cone: ${#own[@]} first-party modules, ${#prover_lib[@]} supplied wi # The proofs and the pinned sibling: no postulate at all. bash scripts/scan-postulates.sh "${own[@]}" # Modules supplied with the prover are its trusted base. The only postulates -# allowed there are Agda.Primitive's universe-level primitives (Level, lzero, -# lsuc, _⊔_, each bound by a BUILTIN pragma); they are reported, not hidden, and -# a postulate in any other prover-supplied module of the cone fails the gate. +# allowed there are Agda.Primitive's universe-level primitives: exactly Level, +# lzero, lsuc and _⊔_, each bound by its BUILTIN pragma. The gate checks the +# declared names and the bindings, not the file name, so a prover pin that adds +# a postulate to Agda.Primitive fails here; a postulate in any other +# prover-supplied module of the cone fails too. if [ "${#prover_lib[@]}" -gt 0 ]; then status=0; bash scripts/scan-postulates.sh "${prover_lib[@]}" >"$work/prover.log" 2>&1 || status=$? [ "$status" -le 1 ] || { cat "$work/prover.log"; exit 1; } - if grep -E '^[^ ]+:[0-9]+: ' "$work/prover.log" | grep -vqF -- "/Agda/Primitive.agda:"; then - cat "$work/prover.log"; echo "ERROR: a postulate in a prover-supplied module other than Agda.Primitive" >&2; exit 1 + grep -E '^[^ ]+:[0-9]+: ' "$work/prover.log" >"$work/prover.hits" || true + prim="$agda_prim/Agda/Primitive.agda" + # Every hit is in Agda.Primitive and is a bare `postulate` line opening a block, + # the only shape the name check below reads. + if grep -vqE -- "^$prim:[0-9]+: postulate[[:space:]]*\$" "$work/prover.hits"; then + cat "$work/prover.log"; echo "ERROR: a prover-supplied postulate outside the Agda.Primitive level blocks" >&2; exit 1 fi - echo "prover-supplied: $(grep -cE '^[^ ]+:[0-9]+: ' "$work/prover.log" || true) postulate block(s), all in Agda.Primitive (universe-level primitives)" + # The names those blocks declare: the indented lines after `postulate`, up to the + # next line that is not indented; line comments removed. + declared="$(LC_ALL=C awk ' + { sub(/--.*/, "") } + /^postulate[ \t]*$/ { inblock = 1; next } + inblock && /^[ \t]*$/ { next } + inblock && /^[ \t]/ { split($0, lhs, ":"); n = split(lhs[1], names, /[ \t]+/) + for (k = 1; k <= n; k++) if (names[k] != "") print names[k]; next } + { inblock = 0 } + ' "$prim" | LC_ALL=C sort | tr '\n' ' ')" + expected="Level _⊔_ lsuc lzero " + [ "$declared" = "$expected" ] || { + echo "ERROR: Agda.Primitive postulates '$declared', expected exactly '$expected'" >&2; exit 1; } + for binding in "LEVEL Level" "LEVELZERO lzero" "LEVELSUC lsuc" "LEVELMAX _⊔_"; do + LC_ALL=C grep -qE -- "^\{-#[[:space:]]+BUILTIN[[:space:]]+${binding% *}[[:space:]]+${binding#* }[[:space:]]+#-\}" "$prim" || { + echo "ERROR: Agda.Primitive does not bind ${binding#* } with BUILTIN ${binding% *}" >&2; exit 1; } + done + echo "prover-supplied: Agda.Primitive postulates exactly ${expected% }, each bound by its BUILTIN pragma ($(wc -l <"$work/prover.hits" | tr -d ' ') block(s)); no other postulate" fi # The controls are written at run time, so no file in the tree carries a real # postulate for another scanner to count. Each must give exactly its exit code. printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \ - '--postulate with no space after the dashes' \ + '--postulate postulate: no space after the dashes' \ '{- postulate {- nested postulate -} postulate -}' \ 'x--postulate : Set₁' 'x--postulate = Set' \ 's : String' 's = "a postulate in a string \" still the string"' \ > "$work/CommentsOnly.agda" -printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' > "$work/Planted.agda" +# Line 2: a postulate after a block comment. Line 3: one bounded by NO-BREAK +# SPACE (U+00A0) on both sides, which Agda reads as whitespace. +printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' \ + $'\302\240postulate\302\240Y : Set' > "$work/Planted.agda" status=0; bash scripts/scan-postulates.sh "$work/CommentsOnly.agda" >"$work/neg.log" 2>&1 || status=$? [ "$status" -eq 0 ] || { cat "$work/neg.log"; echo "ERROR: the comments-only control did not exit 0 (got $status)" >&2; exit 1; } status=0; bash scripts/scan-postulates.sh "$work/Planted.agda" >"$work/pos.log" 2>&1 || status=$? -if [ "$status" -ne 1 ] || ! grep -qF -- "Planted.agda:2:" "$work/pos.log"; then - cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming Planted.agda:2 (got $status)" >&2; exit 1 +if [ "$status" -ne 1 ] || ! grep -qF -- "Planted.agda:2:" "$work/pos.log" || ! grep -qF -- "Planted.agda:3:" "$work/pos.log"; then + cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming Planted.agda:2 and :3 (got $status)" >&2; exit 1 fi echo "[PASS] postulate scan: cone clean, both controls behave" mkdir -p _build/check-logs diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh index 8d06ff2..59154cb 100644 --- a/scripts/scan-postulates.sh +++ b/scripts/scan-postulates.sh @@ -11,20 +11,29 @@ # {- -} comments, after a `--` that starts a token (with or without a space # after it), and inside string or character literals is ignored; pragmas # ({-# … #-}) are code. A `--` inside a name such as `x--y` is part of the name. +# Whitespace is Agda's: its lexer reads every character Haskell's isSpace accepts, +# other than tab and newline, as a space (Agda.Syntax.Parser.Alex, toASCII), so +# CR, FF, VT, NO-BREAK SPACE and the Unicode space separators (category Zs) are +# turned into spaces before the line is lexed. # # Usage: scan-postulates.sh FILE... Prints each hit as path:line: text and the # count; exits 1 if there is any hit, 2 on a usage error or an unreadable file. set -euo pipefail [ "$#" -gt 0 ] || { echo "usage: $0 FILE..." >&2; exit 2; } for f in "$@"; do - [ -f "$f" ] && [ -r "$f" ] || { echo "ERROR: not a readable file: $f" >&2; exit 2; } + [[ -f $f && -r $f ]] || { echo "ERROR: not a readable file: $f" >&2; exit 2; } done -hits="$(awk ' +# The non-ASCII spaces as UTF-8 byte sequences: U+00A0, U+1680, U+2000-U+200A, +# U+202F, U+205F, U+3000. awk runs in the C locale, so it matches bytes the same +# way whichever awk is installed. +ws="$(printf '\302\240|\341\232\200|\342\200[\200-\212]|\342\200\257|\342\201\237|\343\200\200')" +hits="$(LC_ALL=C awk -v ws="$ws" ' # Agda name characters are everything except whitespace and .;{}()@" function namechar(c) { return c != "" && c !~ /[ \t.;{}()@"]/ } FNR == 1 { depth = 0 } { - line = $0; code = ""; i = 1; n = length(line) + line = $0; gsub(/[\r\f\v]/, " ", line); gsub(ws, " ", line) + code = ""; i = 1; n = length(line) while (i <= n) { c = substr(line, i, 1); two = substr(line, i, 2) prev = (i > 1) ? substr(line, i - 1, 1) : "" @@ -48,7 +57,7 @@ hits="$(awk ' code = code c; i++ } if (code ~ /(^|[ \t.;{}()@])postulate([ \t.;{}()@]|$)/) - printf "%s:%d: %s\n", FILENAME, FNR, line + printf "%s:%d: %s\n", FILENAME, FNR, $0 } ' "$@")" count=0 From dcaac106132ef4a8e6843d68a41026dffcc4d18b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:40:47 +0000 Subject: [PATCH 06/15] docs(proofs): answer the Codex review of #171 MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - E-1m: state rotation's premise old ≠ new (rotate-forgets-old needs it; with old = new the key stays usable). - TransactionAtomicity comment: a failed metadata append keeps its record, and no failure after the temporary file exists is injected, so the failed-save summary no longer overgeneralises. - T-9's artefact is operations.rs, where execute appends after the file change and undo marks after the inverse. - G-3 names this repository's FFI bridge, so PROOF-POLICY §1 makes it engineering: the PWG census is 5 of 5, with no ungraded theory row. T-2 and T-3 are flagged as the same open classification question. - Per-leg records (§8.5) for the Agda, Rocq and Lean legs. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- .machine_readable/6a2/STATE.a2ml | 2 +- PROOF-NEEDS.adoc | 11 +-- docs/theory/PROOF-GRADES.adoc | 70 +++++++++++++++---- .../proofs/agda/TransactionAtomicity.agda | 12 ++-- 4 files changed, 70 insertions(+), 25 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index c53f2e1..0d5c86b 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -50,7 +50,7 @@ total = "141 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared # 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-1, T-2, T-3, E-1m — Agda theory modules under verification/proofs/agda; AGDA-VERIFIED; census 5 of 6 theory theorems, G-3 ungraded" +grade-3 = "PWG-3: G-1, T-1, T-2, T-3, E-1m — Agda theory modules under verification/proofs/agda; AGDA-VERIFIED; census 5 of 5 theory theorems (G-3 is engineering under PROOF-POLICY §1)" 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)" diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index d5457fd..6e3b4f1 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -66,7 +66,7 @@ tables must agree. | 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 leaves no agent able to use the old key (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 +| 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 @@ -136,9 +136,10 @@ and 40867211509 at `+4afb710+`) are recorded in 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 6):* `+PWG-3+` 5 +*PWG census, theory theorems of this repository (denominator 5):* `+PWG-3+` 5 (G-1, T-1, T-2, T-3, E-1m) · `+PWG-2i+` 0 · `+PWG-2ii+` 0 · `+PWG-1+` 0 · -`+ungraded+` 1 (G-3). The Rocq and Lean legs of all five have not been +`+ungraded+` 0. G-3 names this repository's FFI bridge, so PROOF-POLICY §1 +classes it as engineering and it is outside the ladder. The Rocq and Lean legs of all five have not been attempted; each row 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 @@ -272,12 +273,12 @@ 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-9: A file change whose log record fails to persist is either recorded or reverted (execute changes the filesystem then appends; undo runs the inverse then marks it; needs a write-ahead intent record) |OPEN |`crates/reversible-core/src/metadata.rs` |- +|T-9: A file change whose log record fails to persist is either recorded or reverted (execute changes the filesystem then appends; undo runs the inverse then marks it; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.rs` |- |T-6: A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1) |ASSUMED |`crates/januskey-cli/src/operations.rs` |- |T-7: Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) |ASSUMED |`crates/reversible-core/src/transaction.rs` |- |Every operation is reversible (MPR), as a theorem linked to the Rust (needs G-2 made mechanical, and G-3) |OPEN |`verification/proofs/agda/Reversibility.agda` |- diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 12886d8..18add9c 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -12,13 +12,20 @@ repository, and none is introduced here. [NOTE] ==== -*PWG census, theory theorems of this repository (denominator 6):* +*PWG census, theory theorems of this repository (denominator 5):* `PWG-3` 5 (G-1, T-1, T-2, T-3, E-1m) · `PWG-2i` 0 · `PWG-2ii` 0 · `PWG-1` 0 · -`ungraded` 1 (G-3, `OPEN`: no Agda statement yet). `+foundation-diverse`: none. -Axioms: none. The denominator is the ledger rows whose source of truth is, or is -to be, an Agda theorem. E-1 (a security property of the implementation; its +`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`) are outside it. +to Creusot and Verus) and G-2 (a bridge, `ASSUMED`). By the same test, T-2 and +T-3 are stated over a hand-transcribed model of this repository's +`TransactionManager`, so they may belong in engineering too. That is an open +classification question for the owner; until it is decided they stay in the +census as recorded since 2026-11-01. ==== == What governs the grades @@ -139,13 +146,14 @@ change 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. Their receipt is -`agda-proofs.yml` run +bytes did, so the receipt above does not cover them. The receipt of record for +the merged bytes is the `agda-proofs.yml` run on `main` after merge; run +42076969251 then becomes `state: superseded`. On the pull request the same +gate passed on each revision of the comments, for example run https://github.com/hyperpolymath/januskey/actions/runs/42623188471[42623188471] -at `a71dc7610b8978c5edd71df2c44e9c9177af4654` (pull request #171, success, the -same container, prover, flags and gate as above, with the postulate scan -included). After merge, the run on `main` is the receipt of record, and run -42076969251 becomes `state: superseded`. +at `a71dc76` (same container, prover and flags, postulate scan included). A +later review round reworded one comment again, so that run does not cover the +final bytes either; the run on the pull request's final head does. Earlier receipts, kept with their lineage (§8.4): @@ -274,12 +282,46 @@ repeated the counts, and the two copies drifted apart. `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 (true by the - definition of `rotate` in the model) | + 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-1, T-2, T-3 and E-1m, so it is given +once. `pwg: 3`, `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, 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. + 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 @@ -324,7 +366,7 @@ observed, never that it always holds. G-2 (the Idris2 ↔ Agda correspondence) i | 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`) +| 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 diff --git a/verification/proofs/agda/TransactionAtomicity.agda b/verification/proofs/agda/TransactionAtomicity.agda index 913cbad..730e91b 100644 --- a/verification/proofs/agda/TransactionAtomicity.agda +++ b/verification/proofs/agda/TransactionAtomicity.agda @@ -25,11 +25,13 @@ -- -- What is NOT claimed (the model is hand-transcribed from the Rust, like -- G-2, and these are deliberate limits): --- * No I/O. Saving is not modelled. The Rust's behaviour on a failed or --- interrupted save is TESTED, not proved: a failed save leaves the --- in-memory log unchanged, and the log is replaced by write, sync and --- rename (ledger rows T-5 and T-8). A file change whose log record fails --- to persist is OPEN (T-9). +-- * 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 (ASSUMED, T-6). From 9ff3043ac70cbd581e66aa990146d7db04052315 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 13:49:31 +0000 Subject: [PATCH 07/15] proofs: comments separate tokens in the scan; skip pragma bodies as Agda does A block comment was removed without leaving a token boundary, so `postulate{- c -}X : Set`, which Agda reads as a postulate, became `postulateX` and was not reported; in Agda.Primitive it would also have slipped past the name check. A comment now leaves a space behind. A pragma was scanned as code, so a FOREIGN payload using `postulate` as a Haskell name failed the gate, and a payload holding `{- {-` opened a comment Agda never sees, hiding a postulate after the pragma. Agda does not nest comments inside a pragma and closes it at a `#-}` token (Lexer.x); the scan now skips to the first `#-}`, which can end a pragma early but never late. Controls: the comments-only file gains a FOREIGN payload; the planted file gains the comment-separated and after-pragma cases, and must name lines 2-5. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01GVPPsHYqVJSoPzdNYD9tRg --- scripts/check-agda.sh | 16 +++++++++++----- scripts/scan-postulates.sh | 20 +++++++++++++++----- 2 files changed, 26 insertions(+), 10 deletions(-) diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 2d98194..ee1e8b1 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -91,16 +91,22 @@ printf '%s\n' 'module CommentsOnly where' '-- postulate in a line comment' \ '{- postulate {- nested postulate -} postulate -}' \ 'x--postulate : Set₁' 'x--postulate = Set' \ 's : String' 's = "a postulate in a string \" still the string"' \ + '{-# FOREIGN GHC postulate = () #-}' \ > "$work/CommentsOnly.agda" -# Line 2: a postulate after a block comment. Line 3: one bounded by NO-BREAK -# SPACE (U+00A0) on both sides, which Agda reads as whitespace. +# One planted postulate per line, 2 to 5: after a block comment; bounded by +# NO-BREAK SPACE (U+00A0), which Agda reads as whitespace; separated from its +# name by a block comment; after a pragma whose payload holds `{- {-`, which Agda +# does not read as a comment there. printf '%s\n' 'module Planted where' '{- c -} postulate X : Set' \ - $'\302\240postulate\302\240Y : Set' > "$work/Planted.agda" + $'\302\240postulate\302\240Y : Set' 'postulate{- c -}Z : Set' \ + '{-# FOREIGN GHC {- {- #-} postulate W : Set' > "$work/Planted.agda" status=0; bash scripts/scan-postulates.sh "$work/CommentsOnly.agda" >"$work/neg.log" 2>&1 || status=$? [ "$status" -eq 0 ] || { cat "$work/neg.log"; echo "ERROR: the comments-only control did not exit 0 (got $status)" >&2; exit 1; } status=0; bash scripts/scan-postulates.sh "$work/Planted.agda" >"$work/pos.log" 2>&1 || status=$? -if [ "$status" -ne 1 ] || ! grep -qF -- "Planted.agda:2:" "$work/pos.log" || ! grep -qF -- "Planted.agda:3:" "$work/pos.log"; then - cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming Planted.agda:2 and :3 (got $status)" >&2; exit 1 +missed="" +for line in 2 3 4 5; do grep -qF -- "Planted.agda:$line:" "$work/pos.log" || missed="$missed $line"; done +if [ "$status" -ne 1 ] || [ -n "$missed" ]; then + cat "$work/pos.log"; echo "ERROR: the planted control did not exit 1 naming lines 2-5 (got $status; missed:${missed:- none})" >&2; exit 1 fi echo "[PASS] postulate scan: cone clean, both controls behave" mkdir -p _build/check-logs diff --git a/scripts/scan-postulates.sh b/scripts/scan-postulates.sh index 59154cb..d20faeb 100644 --- a/scripts/scan-postulates.sh +++ b/scripts/scan-postulates.sh @@ -9,8 +9,14 @@ # # Lexing follows Agda closely enough for one keyword: text inside nested # {- -} comments, after a `--` that starts a token (with or without a space -# after it), and inside string or character literals is ignored; pragmas -# ({-# … #-}) are code. A `--` inside a name such as `x--y` is part of the name. +# after it), and inside string or character literals is ignored. A `--` inside +# a name such as `x--y` is part of the name. A comment separates tokens, as it +# does for Agda, so `postulate{- c -}X` is a postulate. +# A pragma ({-# … #-}) is skipped to the first `#-}`: its contents are pragma +# tokens or, for FOREIGN and COMPILE, another language's text, never an Agda +# declaration, and Agda does not nest comments inside it (Lexer.x). Agda closes +# a pragma at a `#-}` token, never before the first `#-}` in the text, so this +# rule can end a pragma early (an extra report) but never late (a missed one). # Whitespace is Agda's: its lexer reads every character Haskell's isSpace accepts, # other than tab and newline, as a space (Agda.Syntax.Parser.Alex, toASCII), so # CR, FF, VT, NO-BREAK SPACE and the Unicode space separators (category Zs) are @@ -30,17 +36,21 @@ ws="$(printf '\302\240|\341\232\200|\342\200[\200-\212]|\342\200\257|\342\201\23 hits="$(LC_ALL=C awk -v ws="$ws" ' # Agda name characters are everything except whitespace and .;{}()@" function namechar(c) { return c != "" && c !~ /[ \t.;{}()@"]/ } - FNR == 1 { depth = 0 } + FNR == 1 { depth = 0; pragma = 0 } { line = $0; gsub(/[\r\f\v]/, " ", line); gsub(ws, " ", line) code = ""; i = 1; n = length(line) while (i <= n) { c = substr(line, i, 1); two = substr(line, i, 2) prev = (i > 1) ? substr(line, i - 1, 1) : "" + if (pragma) { # inside {-# … #-}: skip to the first #-} + if (substr(line, i, 3) == "#-}") { pragma = 0; i += 3; code = code " " } else i++ + continue + } if (depth == 0 && two == "{-" && substr(line, i + 2, 1) == "#") { - code = code "{-#"; i += 3; continue + pragma = 1; i += 3; code = code " "; continue } - if (two == "{-") { depth++; i += 2; continue } + if (two == "{-") { if (depth == 0) code = code " "; depth++; i += 2; continue } if (depth > 0 && two == "-}") { depth--; i += 2; continue } if (depth > 0) { i++; continue } if (c == "\"") { # string literal: skip to the closing quote From 9eb9f5f0d7668f2272c8149b31e1999b0724e97a Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:05:33 +0000 Subject: [PATCH 08/15] docs(proofs): fold #171's receipt note into #170's pending re-run #170 now records its gate change as "PWG-3, receipt pending re-run". The comment edits here are covered by the same first green run on main. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- docs/theory/PROOF-GRADES.adoc | 22 ++++++++++------------ 1 file changed, 10 insertions(+), 12 deletions(-) diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 39fb83f..4ed0456 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -160,19 +160,17 @@ pending re-run. propositions, and are kept visible |=== -*Re-earned on the change that edits the proof comments (2026-11-09).* That -change 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. The receipt of record for -the merged bytes is the `agda-proofs.yml` run on `main` after merge; run -42076969251 then becomes `state: superseded`. On the pull request the same -gate passed on each revision of the comments, for example run +*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. 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` (same container, prover and flags, postulate scan included). A -later review round reworded one comment again, so that run does not cover the -final bytes either; the run on the pull request's final head does. +at `a71dc76`; branch evidence, not a receipt). Earlier receipts, kept with their lineage (§8.4): From be64d854d402951e0ed64f75d0f1d78ed1beae54 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:12:10 +0000 Subject: [PATCH 09/15] proofs: Rocq and Lean recheck legs for T-1 (PWG-2ii) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The PROOF-POLICY §2 pilot. Transport is not available: Agda2Dedukti was last changed in January 2022, builds against a forked Agda branch of that period, and cannot read modules checked by the pinned Agda 2.6.4.3. So both legs are re-proved by hand, in core Rocq 8.18 and core Lean 4.35.0 (no Mathlib, no imports). - verification/proofs/{rocq,lean}/Rollback: rollback_restores, with Print Assumptions / #print axioms showing no axioms. - tests/reject-{rocq,lean}/ForwardRollback: twins of the Agda fixture. Undoing real double and increment operations in execution order is refused, each with the message the fixture names. - scripts/check-recheck.sh (just test-recheck): fails on a leg that does not check, on any axiom, on an accepted fixture, and on a fixture refused for another reason. Mutants with Admitted and sorry are caught. - agda-proofs.yml gains a recheck job on ubuntu-24.04 with coq=8.18.0+dfsg-1build2 and the Lean 4.35.0 tarball checked by SHA-256. It sits in the same workflow so actions.lock is unchanged. - PROOF-GRADES records the §2.2 statement comparison and the residual logic differences. The census is now PWG-3 4, PWG-2ii 1 (T-1). Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- .github/workflows/agda-proofs.yml | 31 ++++++ .machine_readable/6a2/STATE.a2ml | 4 +- Justfile | 4 + PROOF-NEEDS.adoc | 11 +- docs/theory/PROOF-GRADES.adoc | 142 +++++++++++++++++++++++-- scripts/check-recheck.sh | 80 ++++++++++++++ tests/reject-lean/ForwardRollback.lean | 35 ++++++ tests/reject-rocq/.ForwardRollback.aux | 8 ++ tests/reject-rocq/ForwardRollback.glob | 67 ++++++++++++ tests/reject-rocq/ForwardRollback.v | 35 ++++++ verification/proofs/lean/Rollback.lean | 51 +++++++++ verification/proofs/rocq/Rollback.v | 52 +++++++++ 12 files changed, 504 insertions(+), 16 deletions(-) create mode 100755 scripts/check-recheck.sh create mode 100644 tests/reject-lean/ForwardRollback.lean create mode 100644 tests/reject-rocq/.ForwardRollback.aux create mode 100644 tests/reject-rocq/ForwardRollback.glob create mode 100644 tests/reject-rocq/ForwardRollback.v create mode 100644 verification/proofs/lean/Rollback.lean create mode 100644 verification/proofs/rocq/Rollback.v diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml index 7c7e653..9cabf19 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 -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/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 0d5c86b..e8caea4 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -50,12 +50,12 @@ total = "141 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared # 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-1, T-2, T-3, E-1m — Agda theory modules under verification/proofs/agda; AGDA-VERIFIED; census 5 of 5 theory theorems (G-3 is engineering under PROOF-POLICY §1)" +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 is engineering under PROOF-POLICY §1)" 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 five 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" +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 = "none — no PWG-2i, PWG-2ii or PWG-1 is claimed" [test-categories-complete] 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 902b465..7d32e62 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -68,7 +68,7 @@ tables must agree. | 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-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 | 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+` @@ -141,11 +141,12 @@ 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+` 5 -(G-1, T-1, T-2, T-3, E-1m) · `+PWG-2i+` 0 · `+PWG-2ii+` 0 · `+PWG-1+` 0 · +*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. The Rocq and Lean legs of all five have not been -attempted; each row still owes both (§8.4: a grade is not a discharge). +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 diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 4ed0456..56fe827 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -13,7 +13,7 @@ repository, and none is introduced here. [NOTE] ==== *PWG census, theory theorems of this repository (denominator 5):* -`PWG-3` 5 (G-1, T-1, T-2, T-3, E-1m) · `PWG-2i` 0 · `PWG-2ii` 0 · `PWG-1` 0 · +`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. @@ -193,12 +193,13 @@ 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. -=== 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. @@ -308,8 +309,9 @@ repeated the counts, and the two copies drifted apart. ==== Leg records (PROOF-POLICY §8.5) -The same record holds for each of G-1, T-1, T-2, T-3 and E-1m, so it is given -once. `pwg: 3`, `foundation_diverse: false`. +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"] |=== @@ -340,6 +342,127 @@ 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, +abstract and free of the sibling library. `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. + +*Residual differences, listed rather than hidden.* The targets' logics are +stronger than the source's. Rocq and Lean both have uniqueness of identity +proofs for their equality, which `--without-K` withholds from Agda, and Lean +has definitional proof irrelevance. 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` `662d51bf…ff28e2`, `Rollback.lean` + `808c3258…36c6`, the fixtures `4b2c01d4…0410` (Rocq) and `813cae57…77ee` + (Lean), `check-recheck.sh` `be20e857…b2a3` +| 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 wait for the split into an +abstract log algebra. + 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 @@ -462,8 +585,9 @@ 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. Their Rocq and Lean legs - have not been attempted, so each is `OPEN` with no route and no §2.2 record, + 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). diff --git a/scripts/check-recheck.sh b/scripts/check-recheck.sh new file mode 100755 index 0000000..95308e3 --- /dev/null +++ b/scripts/check-recheck.sh @@ -0,0 +1,80 @@ +#!/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)" +} +for f in "${rocq_rej[@]}"; do + reject "$f" "$rocq" -q -Q "$work/rocq" JanusKey "$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-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.aux b/tests/reject-rocq/.ForwardRollback.aux new file mode 100644 index 0000000..557dc2b --- /dev/null +++ b/tests/reject-rocq/.ForwardRollback.aux @@ -0,0 +1,8 @@ +COQAUX1 cd56b56c27b6d23fd6e71c9323d886c7 /home/user/januskey/tests/reject-rocq/ForwardRollback.v +0 0 VernacProof "tac:no using:no" +901 909 proof_build_time "0.005" +901 909 proof_check_time "0.001" +0 0 VernacProof "tac:no using:no" +1039 1047 proof_build_time "0.002" +1039 1047 proof_check_time "0.000" +0 0 VernacProof "tac:no using:no" diff --git a/tests/reject-rocq/ForwardRollback.glob b/tests/reject-rocq/ForwardRollback.glob new file mode 100644 index 0000000..c5de7dd --- /dev/null +++ b/tests/reject-rocq/ForwardRollback.glob @@ -0,0 +1,67 @@ +DIGEST cd56b56c27b6d23fd6e71c9323d886c7 +FForwardRollback +R522:529 JanusKey.Rollback <> <> lib +R547:551 Coq.Arith.Arith <> <> lib +R553:555 Coq.micromega.Lia <> <> lib +def 568:582 <> rollbackForward +binder 585:585 <> S:1 +R601:604 Coq.Init.Datatypes <> list ind +R607:608 JanusKey.Rollback <> Op rec +R610:610 ForwardRollback <> S:1 var +binder 596:597 <> os:2 +R619:619 ForwardRollback <> S:1 var +binder 615:615 <> z:3 +R624:624 ForwardRollback <> S:1 var +R637:638 ForwardRollback <> os:2 var +R649:651 Coq.Init.Datatypes <> nil constr +R656:656 ForwardRollback <> z:3 var +R662:665 Coq.Init.Datatypes <> cons constr +R676:690 ForwardRollback <> rollbackForward:4 def +R697:700 JanusKey.Rollback <> undo proj +R704:704 ForwardRollback <> z:3 var +def 726:733 <> doubleOp +R737:738 JanusKey.Rollback <> Op rec +R740:742 Coq.Init.Datatypes <> nat ind +R762:765 JanusKey.Rollback <> mkOp constr +R791:798 Coq.Arith.PeanoNat Nat div2 def +binder 772:772 <> x:6 +R777:780 Coq.Init.Datatypes <> Some constr +R784:786 Coq.Init.Peano <> ::nat_scope:x_'+'_x not +R783:783 ForwardRollback <> x:6 var +R787:787 ForwardRollback <> x:6 var +R762:765 JanusKey.Rollback <> mkOp constr +R791:798 Coq.Arith.PeanoNat Nat div2 def +binder 772:772 <> x:7 +R777:780 Coq.Init.Datatypes <> Some constr +R784:786 Coq.Init.Peano <> ::nat_scope:x_'+'_x not +R783:783 ForwardRollback <> x:7 var +R787:787 ForwardRollback <> x:7 var +R851:853 Coq.Init.Peano <> ::nat_scope:x_'+'_x not +R864:866 Coq.Init.Peano <> ::nat_scope:x_'*'_x not +R851:853 Coq.Init.Peano <> ::nat_scope:x_'+'_x not +R864:866 Coq.Init.Peano <> ::nat_scope:x_'*'_x not +R884:898 Coq.Arith.PeanoNat Nat div2_double thm +R884:898 Coq.Arith.PeanoNat Nat div2_double thm +def 922:926 <> incOp +R930:931 JanusKey.Rollback <> Op rec +R933:935 Coq.Init.Datatypes <> nat ind +R955:958 JanusKey.Rollback <> mkOp constr +R982:985 Coq.Init.Peano <> pred abbrev +binder 965:965 <> x:8 +R970:973 Coq.Init.Datatypes <> Some constr +R976:976 Coq.Init.Datatypes <> S constr +R978:978 ForwardRollback <> x:8 var +R955:958 JanusKey.Rollback <> mkOp constr +R982:985 Coq.Init.Peano <> pred abbrev +binder 965:965 <> x:9 +R970:973 Coq.Init.Datatypes <> Some constr +R976:976 Coq.Init.Datatypes <> S constr +R978:978 ForwardRollback <> x:9 var +def 1141:1156 <> forward_restores +R1212:1214 Coq.Init.Logic <> ::type_scope:x_'='_x not +R1162:1176 ForwardRollback <> rollbackForward def +R1179:1182 Coq.Init.Datatypes <> cons constr +R1194:1197 Coq.Init.Datatypes <> cons constr +R1205:1207 Coq.Init.Datatypes <> nil constr +R1199:1203 ForwardRollback <> incOp def +R1184:1191 ForwardRollback <> doubleOp def 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/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. From cf1ace7a44c6aa316a671bb797d0aa656bc6f919 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:18:07 +0000 Subject: [PATCH 10/15] proofs: split T-2/T-3 into an abstract single-active log and an instance MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PROOF-POLICY §1 puts a statement that names one repository's types in engineering. T-2 and T-3 were stated over a model of januskey's TransactionManager, so, per the owner's ruling, they are split: - SingleActiveLog.agda (new, builtins only) proves the invariant for any record type with a decidable key and an active or settled phase, under three transitions: open a fresh active record, a key- and phase-preserving edit, and a settling transition. finish-good needs only the settling law, not key preservation. These are T-2 and T-3, now theory. - TransactionAtomicity Part B is januskey's instance. Tx is keyed by id, its phase comes from its state, and begin, add_operation, commit and mark_rolled_back are the abstract transitions. Every theorem name the ledger, fixtures and docs cite is kept as a corollary. - T-10 (new, OPEN, engineering): the Rust TransactionManager refines the abstract log, for Creusot or Verus. - tests/reject-agda/SettleWithoutSettling.agda pins finish-good's settling premise. With an identity "finish", one record stays active with no pointer, and the claim that the count is 0 is refused with 1 != 0. Its true counterpart checks. - check-agda.sh gains the fourth root, and its warning counts are updated. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- .machine_readable/6a2/STATE.a2ml | 2 +- PROOF-NEEDS.adoc | 10 +- docs/theory/PROOF-GRADES.adoc | 32 ++- scripts/check-agda.sh | 9 +- tests/reject-agda/SettleWithoutSettling.agda | 40 +++ verification/proofs/agda/SingleActiveLog.agda | 240 ++++++++++++++++++ .../proofs/agda/TransactionAtomicity.agda | 175 +++---------- 7 files changed, 351 insertions(+), 157 deletions(-) create mode 100644 tests/reject-agda/SettleWithoutSettling.agda create mode 100644 verification/proofs/agda/SingleActiveLog.agda diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index e8caea4..2d8fd41 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -50,7 +50,7 @@ total = "141 tests + 5 benchmark groups + 12 PROVEN ledger rows — as declared # 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 is engineering under PROOF-POLICY §1)" +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)" diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 7d32e62..179804c 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -69,14 +69,15 @@ tables must agree. | 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+`; rechecked in Rocq and Lean (`+verification/proofs/{rocq,lean}/Rollback+`, `+PWG-2ii+`); `+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-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-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 replaced by write, sync and rename, never overwritten in place; 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 file change whose log record fails to persist is either recorded or reverted: `+execute_*+` changes the filesystem and then appends, and `+undo+` runs the inverse and then marks it, 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-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) @@ -247,8 +248,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` @@ -285,6 +286,7 @@ the status table above. |L-2: Removing trailing audit-log entries makes verify_integrity fail (false today: audit probe P3; needs an external anchor) |OPEN |`crates/januskey-cli/src/attestation.rs` |- |O-1: An ObliterationProof attests that the content it names was erased (false today: storage_cleared is hard-coded, audit probe P6) |OPEN |`crates/januskey-cli/src/obliteration.rs` |- |T-9: A file change whose log record fails to persist is either recorded or reverted (execute changes the filesystem then appends; undo runs the inverse then marks it; needs a write-ahead intent record) |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` |- diff --git a/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 56fe827..b189c4e 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -21,11 +21,13 @@ 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 are stated over a hand-transcribed model of this repository's -`TransactionManager`, so they may belong in engineering too. That is an open -classification question for the owner; until it is decided they stay in the -census as recorded since 2026-11-01. +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 @@ -165,7 +167,8 @@ 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. The first green +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 @@ -295,10 +298,14 @@ repeated the counts, and the two copies drifted apart. | 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 to a different key (premise `old ≠ new`) leaves no agent — the system included @@ -460,8 +467,9 @@ 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 wait for the split into an -abstract log algebra. +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 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/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/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 730e91b..0b56acb 100644 --- a/verification/proofs/agda/TransactionAtomicity.agda +++ b/verification/proofs/agda/TransactionAtomicity.agda @@ -134,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 @@ -157,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 @@ -212,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)) @@ -305,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. @@ -354,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 From 4882688540c2a81597f8870cab59116d7dc1ae06 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:26:15 +0000 Subject: [PATCH 11/15] fix(proofs): keep Rocq build output out of the tree; HTTPS-only prover download check-recheck.sh compiled each Rocq rejection fixture in place, so coqc's .glob and .aux files were committed next to the fixture. They are removed and ignored, and fixtures are now compiled from a copy in the gate's temporary directory. The Lean download is restricted to HTTPS with TLS 1.2 or later, so a redirect cannot downgrade it. The SHA-256 check still runs before unpacking. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- .github/workflows/agda-proofs.yml | 2 +- .gitignore | 9 ++++ scripts/check-recheck.sh | 6 ++- tests/reject-rocq/.ForwardRollback.aux | 8 --- tests/reject-rocq/ForwardRollback.glob | 67 -------------------------- 5 files changed, 15 insertions(+), 77 deletions(-) delete mode 100644 tests/reject-rocq/.ForwardRollback.aux delete mode 100644 tests/reject-rocq/ForwardRollback.glob diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml index 9cabf19..25696fe 100644 --- a/.github/workflows/agda-proofs.yml +++ b/.github/workflows/agda-proofs.yml @@ -45,7 +45,7 @@ jobs: run: | sudo apt-get update sudo apt-get install --no-install-recommends -y coq=8.18.0+dfsg-1build2 zstd - curl -sSfL -o lean.tar.zst \ + 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" 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/scripts/check-recheck.sh b/scripts/check-recheck.sh index 95308e3..a912a37 100755 --- a/scripts/check-recheck.sh +++ b/scripts/check-recheck.sh @@ -71,8 +71,12 @@ reject() { 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 - reject "$f" "$rocq" -q -Q "$work/rocq" JanusKey "$f" + 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" diff --git a/tests/reject-rocq/.ForwardRollback.aux b/tests/reject-rocq/.ForwardRollback.aux deleted file mode 100644 index 557dc2b..0000000 --- a/tests/reject-rocq/.ForwardRollback.aux +++ /dev/null @@ -1,8 +0,0 @@ -COQAUX1 cd56b56c27b6d23fd6e71c9323d886c7 /home/user/januskey/tests/reject-rocq/ForwardRollback.v -0 0 VernacProof "tac:no using:no" -901 909 proof_build_time "0.005" -901 909 proof_check_time "0.001" -0 0 VernacProof "tac:no using:no" -1039 1047 proof_build_time "0.002" -1039 1047 proof_check_time "0.000" -0 0 VernacProof "tac:no using:no" diff --git a/tests/reject-rocq/ForwardRollback.glob b/tests/reject-rocq/ForwardRollback.glob deleted file mode 100644 index c5de7dd..0000000 --- a/tests/reject-rocq/ForwardRollback.glob +++ /dev/null @@ -1,67 +0,0 @@ -DIGEST cd56b56c27b6d23fd6e71c9323d886c7 -FForwardRollback -R522:529 JanusKey.Rollback <> <> lib -R547:551 Coq.Arith.Arith <> <> lib -R553:555 Coq.micromega.Lia <> <> lib -def 568:582 <> rollbackForward -binder 585:585 <> S:1 -R601:604 Coq.Init.Datatypes <> list ind -R607:608 JanusKey.Rollback <> Op rec -R610:610 ForwardRollback <> S:1 var -binder 596:597 <> os:2 -R619:619 ForwardRollback <> S:1 var -binder 615:615 <> z:3 -R624:624 ForwardRollback <> S:1 var -R637:638 ForwardRollback <> os:2 var -R649:651 Coq.Init.Datatypes <> nil constr -R656:656 ForwardRollback <> z:3 var -R662:665 Coq.Init.Datatypes <> cons constr -R676:690 ForwardRollback <> rollbackForward:4 def -R697:700 JanusKey.Rollback <> undo proj -R704:704 ForwardRollback <> z:3 var -def 726:733 <> doubleOp -R737:738 JanusKey.Rollback <> Op rec -R740:742 Coq.Init.Datatypes <> nat ind -R762:765 JanusKey.Rollback <> mkOp constr -R791:798 Coq.Arith.PeanoNat Nat div2 def -binder 772:772 <> x:6 -R777:780 Coq.Init.Datatypes <> Some constr -R784:786 Coq.Init.Peano <> ::nat_scope:x_'+'_x not -R783:783 ForwardRollback <> x:6 var -R787:787 ForwardRollback <> x:6 var -R762:765 JanusKey.Rollback <> mkOp constr -R791:798 Coq.Arith.PeanoNat Nat div2 def -binder 772:772 <> x:7 -R777:780 Coq.Init.Datatypes <> Some constr -R784:786 Coq.Init.Peano <> ::nat_scope:x_'+'_x not -R783:783 ForwardRollback <> x:7 var -R787:787 ForwardRollback <> x:7 var -R851:853 Coq.Init.Peano <> ::nat_scope:x_'+'_x not -R864:866 Coq.Init.Peano <> ::nat_scope:x_'*'_x not -R851:853 Coq.Init.Peano <> ::nat_scope:x_'+'_x not -R864:866 Coq.Init.Peano <> ::nat_scope:x_'*'_x not -R884:898 Coq.Arith.PeanoNat Nat div2_double thm -R884:898 Coq.Arith.PeanoNat Nat div2_double thm -def 922:926 <> incOp -R930:931 JanusKey.Rollback <> Op rec -R933:935 Coq.Init.Datatypes <> nat ind -R955:958 JanusKey.Rollback <> mkOp constr -R982:985 Coq.Init.Peano <> pred abbrev -binder 965:965 <> x:8 -R970:973 Coq.Init.Datatypes <> Some constr -R976:976 Coq.Init.Datatypes <> S constr -R978:978 ForwardRollback <> x:8 var -R955:958 JanusKey.Rollback <> mkOp constr -R982:985 Coq.Init.Peano <> pred abbrev -binder 965:965 <> x:9 -R970:973 Coq.Init.Datatypes <> Some constr -R976:976 Coq.Init.Datatypes <> S constr -R978:978 ForwardRollback <> x:9 var -def 1141:1156 <> forward_restores -R1212:1214 Coq.Init.Logic <> ::type_scope:x_'='_x not -R1162:1176 ForwardRollback <> rollbackForward def -R1179:1182 Coq.Init.Datatypes <> cons constr -R1194:1197 Coq.Init.Datatypes <> cons constr -R1205:1207 Coq.Init.Datatypes <> nil constr -R1199:1203 ForwardRollback <> incOp def -R1184:1191 ForwardRollback <> doubleOp def From f73046b6498920495375e61f4c54a74f5cfa0157 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:28:09 +0000 Subject: [PATCH 12/15] docs(ledger): T-5 and T-8 claim replacement by rename, not a tested fsync None of the named tests observes sync_all: removing it would leave every failed-save, hard-link, temporary-file and retry assertion green. Both rows now claim what the tests show, which is that the log is replaced by rename and never overwritten in place. They say the sync before the rename is there by construction only. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- PROOF-NEEDS.adoc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 179804c..99020f2 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -72,10 +72,10 @@ tables must agree. | 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 replaced by write, sync and rename, never overwritten in place; 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-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 file change whose log record fails to persist is either recorded or reverted: `+execute_*+` changes the filesystem and then appends, and `+undo+` runs the inverse and then marks it, 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-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+`) From 99770a3d30818554dc6d544a4421b2886cdebc8b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:36:38 +0000 Subject: [PATCH 13/15] docs(proofs): answer the Codex review of f73046b MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - STATE: claimed-higher now records T-1 at PWG-2ii; it still said none. - PROOF-GRADES: T-1's Agda module imports the sibling's prelude. The comparison now accounts for the three things Rollback uses from it (builtin _≡_, trans, cong) instead of calling T-1 sibling-free. - PROOF-GRADES: full input digests, with check-recheck.sh's current 5171d9d2… replacing the stale be20e857…. - wiki rmr-primitive: T-8 is TESTED (the log itself) and T-9 is OPEN (a file change and its record are not written together). T-2/T-3 are abstract, T-10 is added, and T-5's fsync is noted as by construction. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- .machine_readable/6a2/STATE.a2ml | 2 +- docs/theory/PROOF-GRADES.adoc | 26 ++++++++++++++++++----- docs/wiki/theory/rmr-primitive.md | 35 ++++++++++++++++++------------- 3 files changed, 42 insertions(+), 21 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index 2d8fd41..d18815f 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -56,7 +56,7 @@ receipt-prover = "Agda 2.6.4.3 (agda-bin=2.6.4.3-1+b2); no standard library; res 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 = "none — no PWG-2i, PWG-2ii or PWG-1 is claimed" +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/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index b189c4e..0554d25 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -351,8 +351,11 @@ 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, -abstract and free of the sibling library. `pwg: 2ii`, `foundation_diverse: +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"] @@ -421,6 +424,13 @@ done by a round trip, since no translator exists. * 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 targets' logics are stronger than the source's. Rocq and Lean both have uniqueness of identity @@ -455,9 +465,15 @@ checks each refusal message. release tarball `lean-4.35.0-linux.tar.zst`, SHA-256 `7289597a44543246c9227b8cae501767e095ce17f6d448b95fc4a8dc97268f6d`, checked before unpacking. `lean -o .olean `. -| Inputs (SHA-256) | `Rollback.v` `662d51bf…ff28e2`, `Rollback.lean` - `808c3258…36c6`, the fixtures `4b2c01d4…0410` (Rocq) and `813cae57…77ee` - (Lean), `check-recheck.sh` `be20e857…b2a3` +| 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. diff --git a/docs/wiki/theory/rmr-primitive.md b/docs/wiki/theory/rmr-primitive.md index 2d425e6..19dbd57 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, and `undo` runs the inverse before `mark_undone`, so a crash or failed save between the two leaves a change the log does not know about (T-9, **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-9: runs after the inverse (OPEN) Ok(()) } ``` @@ -189,13 +189,15 @@ 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 file change whose log record fails to persist is recorded or reverted | **OPEN** — needs a write-ahead intent record | +| 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 +235,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 +248,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 +269,10 @@ 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). 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 +284,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-10 - [Architecture](../architecture/index.md) From 3716998f70d54c7b230430087aa1de92b33e7349 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:45:25 +0000 Subject: [PATCH 14/15] docs(proofs): split T-9 from T-11; correct the Rocq equality claim; no stale PWG text - T-9 was two failure modes. The forward window (execute changes the filesystem, then appends) can leave a change with no record, which needs write-ahead intent. Undo is different: every helper records the inverse as its own operation via execute before mark_undone, so a failed mark leaves the original unmarked and a retry re-applies the inverse. That is T-11 (OPEN), and its fix is an idempotent undo. The ledger, PROOF-GRADES and the RMR wiki are updated. - Axiom-free Rocq has neither K nor UIP. Only Lean's proof-irrelevant Prop adds UIP, so the residual-differences note now says so. - Two passages still said no row is above PWG-3. They now name T-1 at PWG-2ii. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- PROOF-NEEDS.adoc | 14 ++++++++------ docs/theory/PROOF-GRADES.adoc | 32 ++++++++++++++++++------------- docs/wiki/theory/rmr-primitive.md | 12 +++++++----- 3 files changed, 34 insertions(+), 24 deletions(-) diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 99020f2..2044d30 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -76,7 +76,8 @@ tables must agree. | T-6 | A failed execute leaves the filesystem unchanged, and each undo restores the state its execute started from (premises of T-1; single steps are TESTED by `+execute_then_undo_is_identity+`) | ASSUMED | not checked for the failure path | T-7 | Transaction ids (UUID v4) never collide within one log (the freshness premise of T-2) | ASSUMED | probabilistic, not checked | T-8 | The operation metadata log is 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 file change whose log record fails to persist is either recorded or reverted: `+execute_*+` changes the filesystem and then appends, and `+undo+` runs the inverse and then marks it, 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-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) @@ -158,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 @@ -204,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 @@ -285,7 +286,8 @@ 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-9: A file change whose log record fails to persist is either recorded or reverted (execute changes the filesystem then appends; undo runs the inverse then marks it; needs a write-ahead intent record) |OPEN |`crates/januskey-cli/src/operations.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` |- @@ -310,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/docs/theory/PROOF-GRADES.adoc b/docs/theory/PROOF-GRADES.adoc index 0554d25..92a2445 100644 --- a/docs/theory/PROOF-GRADES.adoc +++ b/docs/theory/PROOF-GRADES.adoc @@ -192,9 +192,10 @@ 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 four rows stop at PWG-3 @@ -432,10 +433,12 @@ done by a round trip, since no translator exists. the equality type. No other sibling definition reaches T-1's statement or proof. -*Residual differences, listed rather than hidden.* The targets' logics are -stronger than the source's. Rocq and Lean both have uniqueness of identity -proofs for their equality, which `--without-K` withholds from Agda, and Lean -has definitional proof irrelevance. Neither proof uses these: each is the same +*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. @@ -544,12 +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-9 (`OPEN`) -| A file change whose log record fails to persist: `execute_*` changes the - filesystem and then appends, and `undo` runs the inverse and then marks it. - (T-8, the metadata log's own saves, is TESTED since #168.) -| A write-ahead intent record, which is a design decision, then a test that - injects the failure between the two steps. +| 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 diff --git a/docs/wiki/theory/rmr-primitive.md b/docs/wiki/theory/rmr-primitive.md index 19dbd57..26656b0 100644 --- a/docs/wiki/theory/rmr-primitive.md +++ b/docs/wiki/theory/rmr-primitive.md @@ -79,7 +79,7 @@ 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: 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, and `undo` runs the inverse before `mark_undone`, so a crash or failed save between the two leaves a change the log does not know about (T-9, **OPEN**) | +| 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 | @@ -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-9: runs after the inverse (OPEN) + metadata_store.mark_undone(operation_id)?; // T-11: after the inverse is recorded (OPEN) Ok(()) } ``` @@ -196,7 +196,8 @@ present one until it exists. What exists, by ledger row: | 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 replaced by rename; a failed edit is unapplied and retries once; a failed append keeps its record | **TESTED** | -| T-9 | A file change whose log record fails to persist is recorded or reverted | **OPEN** — needs a write-ahead intent record | +| 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" | @@ -272,7 +273,8 @@ their results are unbaselined (`READINESS.adoc` §Benchmark Classification). 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). + (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. @@ -284,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-10 +- `../../../PROOF-NEEDS.adoc` — the claims ledger, rows T-1..T-11 - [Architecture](../architecture/index.md) From 231d1d8c654bbddcb12811dbf7916556197deeda Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:52:05 +0000 Subject: [PATCH 15/15] docs(readiness): four theory theorems at PWG-3 and T-1 at PWG-2ii READINESS still said all five were PWG-3, contradicting the census in PROOF-NEEDS and PROOF-GRADES. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_013CuBToxr5h9catptGiTsFX --- READINESS.adoc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/READINESS.adoc b/READINESS.adoc index a1b93fc..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 are theory theorems at PWG-3 under PROOF-POLICY §8 — 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