feat(proofs): reversibility as a Loss grade — Agda kernel module pinned to resource-algebra (JNK-01, B of 3)

.github/workflows/agda-proofs.yml

@@ -0,0 +1,32 @@
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+name: Agda proofs
+# DESIGNED until its first green run. Pattern: choreographic-types /
+# residual-evidence-types (pinned Debian prover, sibling fetched by commit).
+# Checks verification/proofs/agda/Reversibility.agda under the kernel flags
+# and refuses the fixtures under tests/reject-agda. Local run: just test-agda.
+on:
+  push:
+    branches: [main]
+  pull_request:
+permissions:
+  contents: read
+jobs:
+  proofs:
+    name: Reversibility as a grade (Loss instance), expected rejections
+    runs-on: ubuntu-latest
+    # trixie-slim, resolved 2026-10-13; re-pin deliberately, like the prover below.
+    container: debian:trixie-slim@sha256:a29215f6a35e51e22adffa17f89e9d2ef06214e64a2bad10d765c46aea49f11f
+    steps:
+      - name: Install the pinned prover
+        run: |
+          apt-get update
+          apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      - name: Verify the checked Agda version
+        run: test "$(agda --version)" = 'Agda version 2.6.4.3'
+      - name: Proofs, sibling pin, expected rejections
+        run: bash scripts/check-agda.sh

.github/workflows/dashboard-check.yml

@@ -22,8 +22,19 @@ jobs:
   dashboard-check:
     name: STATE vs dashboard reconciliation
     runs-on: ubuntu-latest
-    timeout-minutes: 15
+    timeout-minutes: 30
+    # PROVEN rows of the PROOF-NEEDS claims ledger run their checker, so this
+    # job needs Idris2 (the same pinned image as idris-abi.yml) and Agda.
+    container:
+      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff
     steps:
+      - name: Install Agda, and curl for rustup
+        run: |
+          apt-get update
+          apt-get install --no-install-recommends -y ca-certificates curl agda-bin=2.6.3-1build1
+          agda --version
+          idris2 --version
+
       - name: Checkout repository
         uses: actions/checkout@v7.0.1
 

.github/workflows/idris-abi.yml

@@ -27,7 +27,11 @@ jobs:
           persist-credentials: false
       - name: ABI tree invariants
         run: bash scripts/check-abi-tree.sh
+      - name: ABI <-> header <-> Zig agreement
+        run: bash scripts/check-abi-layout.sh
       - name: Typecheck ABI package
         run: |
           idris2 --version
           idris2 --typecheck src/abi/januskey-abi.ipkg
+      - name: Expected rejections
+        run: bash scripts/check-idris-reject.sh

.gitignore

@@ -90,3 +90,4 @@ deps/
 .cache/
 build/
 dist/
+*.agdai

Justfile

@@ -88,13 +88,25 @@ test-contracts:
         done; \
     fi
 
+# Agda kernel proofs (verification/proofs/agda) against the pinned resource-algebra.
+test-agda:
+    bash scripts/check-agda.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
+
+# Expected-rejection fixtures for the Idris2 ABI (double close, forgotten close, unknown status).
+test-proofs-reject:
+    bash scripts/check-idris-reject.sh
+
 # One ABI tree: no symlink farm, one ipkg, one Foreign.idr, module names match paths.
 abi-tree-check:
     bash scripts/check-abi-tree.sh
 
 # Typecheck the Idris2 ABI package (src/abi/januskey-abi.ipkg).
 # Fails if idris2 is missing (set ALLOW_NO_IDRIS=1 to skip) or any module fails.
-test-proofs: abi-tree-check
+test-proofs: abi-tree-check abi-layout-check
     #!/usr/bin/env bash
     set -euo pipefail
     echo "=== Proof Regression ==="

PROOF-NEEDS.adoc

@@ -35,16 +35,74 @@ commits, not this one:
 regenerated with capitalised module names or removed is an owner decision
 (JNK-01, open question).
 
+==== Same day, three commits later: the package typechecks
+
+`+idris2 --typecheck src/abi/januskey-abi.ipkg+` builds all four modules
+with zero warnings under Idris2 0.8.0 (bootstrap build, locally; the CI
+image `+idris2-pack@sha256:f0758996…+` is the gate of record). Bypass census
+in `+src/abi/+`: no `+believe_me+`, `+assert_total+`, `+assert_smaller+`,
+`+partial+` or holes (`+tests/aspect/cross_cutting_test.sh+`, 32/32; the
+last three checks were added when these rows entered the claims ledger).
+
+Status rows, in the five-status vocabulary. A status moves only with a named
+module, lemma, fixture or log line. Every row is also a row of the claims
+ledger below, which `+dashboard-check+` runs on every pull request; the two
+tables must agree.
+
+[cols="1,3,1,2",options="header"]
+|===
+| ID | Claim | Status | Artefact
+| A-1 | Status codes are a closed sum with a total decoder; encode/decode round-trips; encoding is injective | PROVEN | `+Foreign.statusFromCode+`, `+statusRoundTrip+`, `+statusCodeInjective+`
+| A-2 | Op-kind and algorithm encodings round-trip against januskey.h's enum order | PROVEN | `+Foreign.opKindRoundTrip+`, `+algorithmRoundTrip+`
+| A-3 | Idris2 sizes, status codes, enums and exported symbols agree with januskey.h and ffi/zig | TESTED | `+scripts/check-abi-layout.sh+` (negative control: one perturbed code → FAIL)
+| A-4 | A linearly held library handle is closed at most once and cannot be forgotten (multiplicity 1 on `+Foreign.closeOnce+`) | TESTED | `+tests/reject-idris/{DoubleClose,ForgottenClose}.idr+` refused with "2 uses" / "0 uses" of the handle
+| A-5 | A code the header does not define is never read as Ok | TESTED | `+tests/reject-idris/UnknownStatusIsOk.idr+` refused
+| C-1 | Composition of CNOs is a CNO | PROVEN | `+Proofs.seqCNO+`
+| C-2 | Copy-then-uncopy is a CNO in the (path, hash) log model | PROVEN | `+Layout.copyIsCNO+`
+| 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-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 (#145 item 3)
+| X-1 | Hash one-wayness; physical erasure (cryptographic and physical assumptions, external to this repository) | ASSUMED | not theorems of this repo
+|===
+
+Removed, with the reason recorded beside the replacement in source:
+`+memoryDefeatsGPU+`, `+timeCostMonotonic+`, `+outputIs256Bits+`,
+`+threePassMinimum+` (closed literals or restated hypotheses);
+`+defaultExceedsMinimum+`, `+defaultMeetsOWASP+`, `+defaultMemoryOWASP+`
+(restated record fields that already carry the bound); `+cnoPairCompose+`,
+`+tamperDetectable+` (returned Unit); `+identityIsCNO+` (`+s = s+`);
+`+hashOneWay+` (`+Void -> Void+`); `+canRollback+` (returned its argument);
+`+copyDeleteCNO+` (no body, false as stated); `+linearFileConsumed+`
+(ill-typed; claimed `+LinearFile -> Void+`); `+systemForgetsOldKey+`
+("forgets" has no negative form in the Knows model);
+`+revokedKeyUnusable+` (`+adversaryCannotKnow+` at `+KeyId+`; took no
+revocation); `+errorCodeDeterministic+` over an undefined `+CError+` (now
+`+statusCodeInjective+`).
+
+Model limits, stated so no reader over-counts them: `+Knows Adversary a+`
+being uninhabited is a modelling choice, not a security proof; `+FSState+`
+tracks (path, hash) pairs, not contents, so C-2 is about the operation log;
+linearity is a property of the binding — a handle bound by an IO `+<-+` is
+unrestricted, the guarantee holds for `+(1 h : LibHandle Open)+` parameters,
+and plain IO's bind is not linear, so such a handle cannot be closed inside
+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.
+
 === Current State
 
 _Re-verified 2026-06-29 (idris2 0.8.0); paths updated 2026-10-12 to the
-single tree._
+single tree; ABI bullet re-verified 2026-10-13._
 
-* **src/abi/JanusKey/ABI/*.idr**: PRESENT but **placeholder** —
-`+src/abi/JanusKey/ABI/Proofs.idr+` typechecks (when the package does), but its theorems are
-trivial/tautological (e.g. `+memoryDefeatsGPU : So (65536 >= 65536)+`,
-`+timeCostMonotonic : So (a >= b) -> So (a >= b)+` returns its own
-hypothesis). NOT the security proofs listed below.
+* **src/abi/JanusKey/ABI/*.idr**: typechecks (Idris2 0.8.0; `+idris-abi.yml+`
+and `+dashboard-check+`). The tautological placeholders are gone (list
+above). What it proves are ABI and model lemmas (ledger rows A-*, C-*),
+NOT the security proofs listed below.
 * **generated/idrisiser/idris2/Januskey/Verified/*.idr**: **DO NOT
 typecheck** — `+idris2 --check+` fails ("`Expected a capitalised
 identifier, got: key`") because the generated module names are
@@ -93,33 +151,56 @@ TOPOLOGY and READINESS must equal what that checker measures: tests by
 `cargo test --workspace --locked -- --list`, proofs by the PROVEN rows below.
 Each row is one line; the checker rejects a wrapped row.
 
-There are no PROVEN rows: the Idris2 ABI does not typecheck (#145), so no
-proof in this repository is checked by anything.
+PROVEN rows run their checker: `+idris2 --typecheck src/abi/januskey-abi.ipkg+`
+(Idris2 0.8.0) for the ABI, `+bash scripts/check-agda.sh+` (Agda, resource-algebra
+pinned) for the kernel. `+dashboard-check.yml+` therefore runs in the same pinned
+idris2-pack image as `+idris-abi.yml+` and installs Agda from apt. Row IDs match
+the status table above.
 
 [cols="3,1,3,3",options="header"]
 |===
 |Claim |Status |Artefact |Command
 |Obliterating a path shreds its unshared blobs and log entries, and undo then has nothing |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::obliterate_scrubs_blobs_log_and_undo` |`cargo test --locked -p januskey --test obliteration_cas_test obliterate_scrubs_blobs_log_and_undo`
 |Obliteration keeps a blob another path still references |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::obliterate_keeps_blob_shared_with_another_path` |`cargo test --locked -p januskey --test obliteration_cas_test obliterate_keeps_blob_shared_with_another_path`
 |`jk obliterate` scrubs the store end to end through the CLI |TESTED |`crates/januskey-cli/tests/obliteration_cas_test.rs::cli_obliterate_scrubs_store_and_undo_has_nothing` |`cargo test --locked -p januskey --test obliteration_cas_test cli_obliterate_scrubs_store_and_undo_has_nothing`
-|Execute then undo restores the prior state (property test over generated ops) |TESTED |`crates/januskey-cli/tests/property_tests.rs::execute_then_undo_is_identity` |`cargo test --locked -p januskey --test property_tests execute_then_undo_is_identity`
+|Execute then undo restores the prior state (property test over generated ops; the cancellation premise of G-1) |TESTED |`crates/januskey-cli/tests/property_tests.rs::execute_then_undo_is_identity` |`cargo test --locked -p januskey --test property_tests execute_then_undo_is_identity`
 |Content store round-trips arbitrary bytes (property test) |TESTED |`crates/reversible-core/tests/property_tests.rs::content_store_roundtrip` |`cargo test --locked -p reversible-core --test property_tests content_store_roundtrip`
 |A transaction rolled back ends RolledBack with none active (property test) |TESTED |`crates/reversible-core/tests/property_tests.rs::transaction_begin_rollback_roundtrip` |`cargo test --locked -p reversible-core --test property_tests transaction_begin_rollback_roundtrip`
 |The audit log verifies an untampered three-entry chain as valid (tamper detection is not tested) |TESTED |`crates/januskey-cli/src/attestation.rs::test_audit_log_chain_integrity` |`cargo test --locked -p januskey --lib test_audit_log_chain_integrity`
-|The Idris2 ABI typechecks and its six security claims are proved |OPEN |#145 |-
-|Every operation is reversible (MPR), as a theorem linked to the Rust |OPEN |#145 |-
+|A-1: Status codes are a closed sum with a total decoder; encoding round-trips and is injective |PROVEN |`src/abi/JanusKey/ABI/Foreign.idr::statusCodeInjective` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
+|A-2: Op-kind and algorithm encodings round-trip in januskey.h's enum order |PROVEN |`src/abi/JanusKey/ABI/Foreign.idr::opKindRoundTrip` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
+|C-1: Sequential composition of CNOs is a CNO |PROVEN |`src/abi/JanusKey/ABI/Proofs.idr::seqCNO` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
+|C-2: Copy-then-uncopy is a CNO in the (path, hash) log model |PROVEN |`src/abi/JanusKey/ABI/Layout.idr::copyIsCNO` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
+|C-3: A transaction containing an obliteration is not all-reversible |PROVEN |`src/abi/JanusKey/ABI/Layout.idr::obliterateNotReversible` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
+|C-4: Replacing an attestation-chain entry by one with a different hash breaks the link |PROVEN |`src/abi/JanusKey/ABI/Proofs.idr::tamperBreaksLink` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
+|C-5: The 32-, 16- and 112-byte ABI structs are 8-byte aligned (divisibility at the literals) |PROVEN |`src/abi/JanusKey/ABI/Layout.idr::oblitAligned` |`idris2 --typecheck src/abi/januskey-abi.ipkg`
+|G-1: Reversibility as a Loss grade: a trace is lossless only if every step is, and an obliterating step absorbs |PROVEN |`verification/proofs/agda/Reversibility.agda::lossless-trace-all` |`bash scripts/check-agda.sh`
+|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`
+|A-5: A status code the header does not define never decodes as Ok |TESTED |`tests/reject-idris/UnknownStatusIsOk.idr::UnknownStatusIsOk` |`bash scripts/check-idris-reject.sh UnknownStatusIsOk`
+|src/abi uses no proof bypass: no believe_me, assert_total, assert_smaller, partial, postulate, sorry or holes |TESTED |`tests/aspect/cross_cutting_test.sh::No holes in proofs` |`bash tests/aspect/cross_cutting_test.sh`
+|G-2: The Idris2 IsCNO / ReversibleOp pair corresponds to the Agda ReversiblePair (by transcription) |ASSUMED |`verification/proofs/agda/Reversibility.agda` |-
+|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` |-
+|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` |-
+|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` |-
 |===
 
 === Recommended Prover
 
-*Idris2* — Create `+src/abi/+` with dependent type proofs for
-obliteration completeness, attestation chain integrity, and transaction
-atomicity. The 225 `+unwrap()+` calls should be systematically replaced
-with proven error handling.
+*Agda* (`+--safe --without-K+`) is the proof kernel and *Idris2* the
+ABI/runtime layer (ruling 2026-10-12): kernel statements live in
+`+verification/proofs/agda/+` with siblings consumed by pin
+(`+scripts/fetch-siblings.sh+`); the ABI lives in `+src/abi/+`.
+Obliteration completeness, attestation chain integrity and transaction
+atomicity are still to be stated there. The 225 `+unwrap()+` calls should
+be systematically replaced with proven error handling.
 
 === Priority
 
 *HIGH* — JanusKey handles cryptographic key management, attestation
 chains, and data obliteration. Any correctness bug in obliteration or
-key derivation is a critical security vulnerability. Missing ABI layer
-entirely.
+key derivation is a critical security vulnerability. The ABI layer now
+typechecks, but none of the security obligations above is proved.

READINESS.adoc

@@ -9,13 +9,14 @@ standards/testing-and-benchmarking/TESTING-TAXONOMY.adoc v1.0
 === CRG Grade: D (Alpha — Unstable)
 
 *Justification:* 119 tests declared (`cargo test --workspace --locked -- --list`; rust-ci runs them); the
-Idris2 ABI does not typecheck, so 0 proofs are checked (#145); benchmarks exist (5 Criterion groups). But: no
+Idris2 ABI typechecks and 8 proofs are checked (PROVEN ledger rows: ABI and grade lemmas, not the
+security obligations); benchmarks exist (5 Criterion groups). But: no
 fuzz testing, no mutation testing, 225 unwrap() calls, E2E mostly skips,
 benchmarks measured fake crypto until this session. RSR compliance
 present. Deep annotation incomplete (TOPOLOGY.md exists but
 per-directory orientation missing → blocks C).
 
-*Promotion path D→C:* Fix unwrap() calls, wire Idris2 proof check in CI,
+*Promotion path D→C:* Fix unwrap() calls, make the Idris2 and Agda proof checks required in CI,
 complete per-directory annotation, add real E2E with built binary,
 dogfood in at least one real workflow.
 
@@ -60,11 +61,11 @@ handling
 
 |15 |Compatibility |MISSING |0 |— |No version migration tests
 
-|16 |Proof regression |✗ |0 checked (#145) |`+just test-proofs+` |Idris2 –check
-(requires idris2 binary)
+|16 |Proof regression |✓ |8 proofs checked |`+just test-proofs test-proofs-reject test-agda+` |Idris2 0.8.0 typecheck, Agda kernel, expected rejections
+(run by idris-abi.yml, agda-proofs.yml and dashboard-check)
 |===
 
-*Total declared:* 119 tests + 5 benchmark groups; 0 Idris2 proofs checked (#145) *Total
+*Total declared:* 119 tests + 5 benchmark groups; 8 proofs checked (PROVEN ledger rows) *Total
 missing:* Fuzz, mutation, chaos, compatibility
 
 === Aspect Matrix
@@ -128,7 +129,7 @@ recording.
 
 * 225 unwrap() calls (tracked in PROOF-NEEDS.md)
 * E2E test needs pre-built binary to exercise full lifecycle
-* Idris2 proofs not checked in CI (requires idris2 in CI image)
+* idris-abi.yml and agda-proofs.yml run on every PR but are not yet required checks
 * No code coverage measurement
 * No mutation testing
 * Benchmarks not baselined in VeriSimDB

README.adoc

@@ -142,7 +142,7 @@ Reversibility is the default. Secure obliteration (`jk shred`) is the deliberate
 
 [CAUTION]
 ====
-**Formal proofs are pending.** The claim "data loss is architecturally impossible" is an engineering intent supported by the inversion-metadata mechanism. It is not yet a mechanically verified theorem. The `src/abi/` and `idrisiser/` directories suggest Idris 2 specification targets, but these are not yet discharging the reversibility guarantee.
+**Formal proofs are pending.** The claim "data loss is architecturally impossible" is an engineering intent supported by the inversion-metadata mechanism. It is not yet a mechanically verified theorem. The `src/abi/` package typechecks (gate: `just test-proofs`) and discharges the ABI obligations listed in PROOF-NEEDS.adoc; it does not discharge "data loss is architecturally impossible", and `generated/idrisiser/` is outside the gate.
 ====
 
 [CAUTION]