From 3a6d7ac4687d6b94846889d67491908c9c14d55b Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 12 Oct 2026 21:47:21 +0000 Subject: [PATCH 1/5] =?UTF-8?q?refactor(abi):=20one=20ABI=20tree=20?= =?UTF-8?q?=E2=80=94=20module-path=20layout,=20JanusKey=20casing,=20symlin?= =?UTF-8?q?k=20farm=20retired?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Idris2 ABI surface was three trees: flat sources in src/abi/, the src/idris-abi/ symlink farm from #140 (so an .ipkg could reach them), and generated/idrisiser/. Collapse the first two into one: - src/abi/JanusKey/ABI/{Types,Layout,Foreign,Proofs}.idr, laid out by module name; src/abi/januskey-abi.ipkg beside them (sourcedir "."). - Foreign.idr now declares JanusKey.ABI.Foreign and imports JanusKey.ABI.{Types,Layout} (was Januskey.*, J1-3). No other content change in this commit. - src/idris-abi/ deleted. - scripts/check-abi-tree.sh (just abi-tree-check; first step of idris-abi.yml): fails on a second .ipkg, a second Foreign.idr, a symlink under src/abi, a module whose declared name differs from its path, or a package/file mismatch. Negative control run locally (symlink farm + casing split reintroduced -> FAIL; removed -> OK). - References repointed: Justfile, .github/workflows/idris-abi.yml, .machine_readable/contractiles/{Justfile,Mustfile.a2ml} (the dead $$f recipe replaced by the package check), tests/aspect/cross_cutting_test.sh, ffi/zig/{src/main.zig,include/januskey.h} comments, QUICKSTART-DEV.adoc, bot directives, PROOF-NEEDS.adoc. Not claimed here: the package still does not typecheck. Foreign.idr is the RSR template FFI (januskey_init/process/...) and never described ffi/zig's jk_* exports; the header's "generated from src/abi/Foreign.idr" comment was false and is corrected. Types.idr keeps its ten known errors. Both are the next commits. generated/idrisiser/ is outside the gate, unchanged. Refs: JNK-01 (ISSUES-2026-10-12), J1-3, P0-2 (#140). Assisted-by: Claude (claude.ai session, 2026-10-12) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .github/workflows/idris-abi.yml | 15 ++++-- .../bot_directives/gitbot-fleet.a2ml | 2 +- .machine_readable/contractiles/Justfile | 17 ++---- .machine_readable/contractiles/Mustfile.a2ml | 2 +- Justfile | 10 ++-- PROOF-NEEDS.adoc | 44 +++++++++++++-- QUICKSTART-DEV.adoc | 2 +- ffi/zig/include/januskey.h | 2 +- ffi/zig/src/main.zig | 2 +- scripts/check-abi-tree.sh | 53 +++++++++++++++++++ src/abi/{ => JanusKey/ABI}/Foreign.idr | 6 +-- src/abi/{ => JanusKey/ABI}/Layout.idr | 0 src/abi/{ => JanusKey/ABI}/Proofs.idr | 0 src/abi/{ => JanusKey/ABI}/Types.idr | 0 src/abi/januskey-abi.ipkg | 20 +++++++ src/idris-abi/JanusKey/ABI/Layout.idr | 1 - src/idris-abi/JanusKey/ABI/Proofs.idr | 1 - src/idris-abi/JanusKey/ABI/Types.idr | 1 - src/idris-abi/Januskey/ABI/Foreign.idr | 1 - src/idris-abi/januskey-abi.ipkg | 30 ----------- tests/aspect/cross_cutting_test.sh | 10 ++-- 21 files changed, 146 insertions(+), 73 deletions(-) create mode 100755 scripts/check-abi-tree.sh rename src/abi/{ => JanusKey/ABI}/Foreign.idr (98%) rename src/abi/{ => JanusKey/ABI}/Layout.idr (100%) rename src/abi/{ => JanusKey/ABI}/Proofs.idr (100%) rename src/abi/{ => JanusKey/ABI}/Types.idr (100%) create mode 100644 src/abi/januskey-abi.ipkg delete mode 120000 src/idris-abi/JanusKey/ABI/Layout.idr delete mode 120000 src/idris-abi/JanusKey/ABI/Proofs.idr delete mode 120000 src/idris-abi/JanusKey/ABI/Types.idr delete mode 120000 src/idris-abi/Januskey/ABI/Foreign.idr delete mode 100644 src/idris-abi/januskey-abi.ipkg diff --git a/.github/workflows/idris-abi.yml b/.github/workflows/idris-abi.yml index 04cb957..0dd020f 100644 --- a/.github/workflows/idris-abi.yml +++ b/.github/workflows/idris-abi.yml @@ -1,7 +1,10 @@ # SPDX-License-Identifier: MPL-2.0 -# Typechecks the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg). -# NOT a required check: it is expected to be red until J1-3 fixes the known -# errors in src/abi (Types.idr, and the Januskey/JanusKey module-name casing). +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Checks the Idris2 ABI tree invariants (scripts/check-abi-tree.sh) and +# typechecks the ABI package (src/abi/januskey-abi.ipkg). +# NOT yet a required check: the typecheck step is expected to be red until the +# follow-up commits land (Foreign.idr still carries the RSR template FFI, and +# Types.idr has known errors); the tree-invariant step must be green now. name: Idris ABI typecheck on: pull_request: @@ -12,7 +15,7 @@ permissions: contents: read jobs: idris-abi: - name: "idris-abi (expected red until J1-3)" + name: "idris-abi" runs-on: ubuntu-latest timeout-minutes: 15 container: @@ -22,7 +25,9 @@ jobs: uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 with: persist-credentials: false + - name: ABI tree invariants + run: bash scripts/check-abi-tree.sh - name: Typecheck ABI package run: | idris2 --version - idris2 --typecheck src/idris-abi/januskey-abi.ipkg + idris2 --typecheck src/abi/januskey-abi.ipkg diff --git a/.machine_readable/bot_directives/gitbot-fleet.a2ml b/.machine_readable/bot_directives/gitbot-fleet.a2ml index 811213c..fc37beb 100644 --- a/.machine_readable/bot_directives/gitbot-fleet.a2ml +++ b/.machine_readable/bot_directives/gitbot-fleet.a2ml @@ -27,7 +27,7 @@ never-touch = [ ".machine_readable/contractiles/Trustfile.a2ml", "LICENSE", ] -never-touch-notes = "src/abi/ + generated/idrisiser/ are the Idris2 ABI proof surface (changes require proof re-verification); threat-model.a2ml awaits human sign-off; the Trustfile may never be widened by an agent (see its self-integrity rule)." +never-touch-notes = "src/abi/ (one tree: src/abi/januskey-abi.ipkg + JanusKey/ABI/*.idr, invariants in scripts/check-abi-tree.sh) + generated/idrisiser/ are the Idris2 ABI proof surface (changes require proof re-verification); threat-model.a2ml awaits human sign-off; the Trustfile may never be widened by an agent (see its self-integrity rule)." [per-bot.sustainabot] allow = ["Cargo.toml", "Cargo.lock", ".github/workflows (SHA bumps via grouped dependabot PRs only)"] diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile index db5a756..a4ab838 100644 --- a/.machine_readable/contractiles/Justfile +++ b/.machine_readable/contractiles/Justfile @@ -84,21 +84,10 @@ test-contracts: done; \ fi -# Check Idris2 ABI proofs (requires idris2) +# Check Idris2 ABI proofs (requires idris2); mirrors the root Justfile recipe test-proofs: - @echo "=== Proof Regression ===" - @if command -v idris2 >/dev/null 2>&1; then \ - for f in src/abi/Types.idr src/abi/Layout.idr src/abi/Foreign.idr src/abi/Proofs.idr; do \ - if [ -f "$$f" ]; then \ - echo "Checking $$f..."; \ - idris2 --check "$$f" && echo " [OK] $$f" || echo " [FAIL] $$f"; \ - else \ - echo " [SKIP] $$f not found"; \ - fi; \ - done; \ - else \ - echo "SKIP: idris2 not installed. Install via: pack install-app idris2"; \ - fi + bash scripts/check-abi-tree.sh + idris2 --typecheck src/abi/januskey-abi.ipkg # Run full test suite (all categories) test-all: test test-p2p test-regressions test-e2e test-aspect test-contracts test-proofs smoke diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml index 21d3e66..9b3602a 100644 --- a/.machine_readable/contractiles/Mustfile.a2ml +++ b/.machine_readable/contractiles/Mustfile.a2ml @@ -147,7 +147,7 @@ trust level: even maximal-trust agents cannot violate MUST constraints. ### abi-proofs-preserved - description: Idris2 ABI definitions and proofs must not be removed (changes require proof update) -- run: test -f src/abi/Types.idr && test -f src/abi/Proofs.idr && test -f src/abi/Foreign.idr +- run: test -f src/abi/JanusKey/ABI/Types.idr && test -f src/abi/JanusKey/ABI/Proofs.idr && test -f src/abi/JanusKey/ABI/Foreign.idr && test -f src/abi/januskey-abi.ipkg - severity: critical ### generated-code-in-generated diff --git a/Justfile b/Justfile index 44b485a..8176a69 100644 --- a/Justfile +++ b/Justfile @@ -88,13 +88,17 @@ test-contracts: done; \ fi -# Typecheck the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg). +# 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: +test-proofs: abi-tree-check #!/usr/bin/env bash set -euo pipefail echo "=== Proof Regression ===" - ipkg="src/idris-abi/januskey-abi.ipkg" + ipkg="src/abi/januskey-abi.ipkg" if ! command -v idris2 >/dev/null 2>&1; then if [ "${ALLOW_NO_IDRIS:-0}" = "1" ]; then echo "SKIP: idris2 not installed and ALLOW_NO_IDRIS=1 -- ABI proofs were NOT checked." >&2 diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 9f60ff6..6d6039e 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -1,11 +1,47 @@ == PROOF-NEEDS.md — januskey +=== One ABI tree (2026-10-12) + +The Idris2 ABI surface was three trees: the flat sources in `+src/abi/+`, +the `+src/idris-abi/+` symlink farm added by PR #140 so that an `+.ipkg+` +could reach them, and `+generated/idrisiser/+`. It is now one: the sources +live at `+src/abi/JanusKey/ABI/{Types,Layout,Foreign,Proofs}.idr+`, laid out +by module name, with the package file beside them at +`+src/abi/januskey-abi.ipkg+`; the symlink farm is deleted; the +`+Januskey.ABI.Foreign+` / `+JanusKey.ABI.*+` casing split (J1-3) is +normalised to `+JanusKey+`. `+scripts/check-abi-tree.sh+` (`+just +abi-tree-check+`, first step of `+idris-abi.yml+`) fails on a second package +file, a second `+Foreign.idr+`, a symlink under `+src/abi+`, a module whose +declared name differs from its path, or a package/file mismatch. + +What this commit does *not* claim: the package still does not typecheck. +Two facts were established while relocating it and are the next two +commits, not this one: + +* `+Foreign.idr+` is the RSR *template* FFI (`+januskey_init+`, + `+januskey_process+`, `+januskey_get_string+`, …) written against + template types (`+createHandle+`, `+handlePtr+`, `+Result+`) that the + hand-written `+Types.idr+` does not define. It never described + `+ffi/zig+`, which exports `+jk_init+` … `+jk_version+` against + `+ffi/zig/include/januskey.h+`; that header's former comment + "generated from src/abi/Foreign.idr" was false and has been corrected. +* `+Types.idr+` has the ten known errors from PR #140 (first: + `+isInfixOf+` without `+import Data.String+`; also forward references in + `+ResultOf+`, a `+Handle+` whose only constructor cannot inhabit + `+Handle Locked+`, linear variables used twice or not at all, and + `+oblitMostExpensive (S k) = Oh+` on an open `+k+`). + +`+generated/idrisiser/+` is unchanged and outside the gate; whether it is +regenerated with capitalised module names or removed is an owner decision +(JNK-01, open question). + === Current State -_Re-verified 2026-06-29 (idris2 0.8.0)._ +_Re-verified 2026-06-29 (idris2 0.8.0); paths updated 2026-10-12 to the +single tree._ -* **src/abi/*.idr**: PRESENT but **placeholder** — -`+src/abi/Proofs.idr+` typechecks, but its theorems are +* **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. @@ -17,7 +53,7 @@ verified. * *Dangerous patterns*: *265* `+unwrap()+` calls across the Rust codebase. * *LOC*: ~12,200 (Rust) -* *ABI layer*: present (`+src/abi/{Types,Foreign,Layout,Proofs}.idr+`) +* *ABI layer*: present (`+src/abi/JanusKey/ABI/{Types,Foreign,Layout,Proofs}.idr+`, package `+src/abi/januskey-abi.ipkg+`) but carries no load-bearing security proof yet — the real obligations below are still open. diff --git a/QUICKSTART-DEV.adoc b/QUICKSTART-DEV.adoc index 461ea86..2e08174 100644 --- a/QUICKSTART-DEV.adoc +++ b/QUICKSTART-DEV.adoc @@ -55,7 +55,7 @@ just setup-dev ---- januskey/ ├── src/ # Source code -├── src/abi/ # Idris2 ABI definitions (if applicable) +├── src/abi/ # Idris2 ABI package (januskey-abi.ipkg, JanusKey/ABI/*.idr) ├── ffi/zig/ # Zig FFI bridge (if applicable) ├── tests/ # Test suite ├── docs/ # Documentation diff --git a/ffi/zig/include/januskey.h b/ffi/zig/include/januskey.h index 3690a76..18c595f 100644 --- a/ffi/zig/include/januskey.h +++ b/ffi/zig/include/januskey.h @@ -2,7 +2,7 @@ // Copyright (c) Jonathan D.A. Jewell /* SPDX-License-Identifier: MPL-2.0 */ /* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) */ -/* JanusKey C FFI Header — generated from src/abi/Foreign.idr */ +/* JanusKey C FFI Header — hand-maintained; src/abi/JanusKey/ABI/Foreign.idr must mirror it (checked by the ABI package typecheck) */ #ifndef JANUSKEY_H #define JANUSKEY_H diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig index 0adf65f..2e0a96f 100644 --- a/ffi/zig/src/main.zig +++ b/ffi/zig/src/main.zig @@ -110,7 +110,7 @@ pub const OblitProof = extern struct { }; comptime { - // Layout invariants — these mirror src/abi/Layout.idr and the comments + // Layout invariants — these mirror src/abi/JanusKey/ABI/Layout.idr and the comments // in januskey.h. If any fires, the C ABI and the Idris spec disagree. std.debug.assert(@sizeOf(ContentHash) == 32); std.debug.assert(@sizeOf(KeyId) == 16); diff --git a/scripts/check-abi-tree.sh b/scripts/check-abi-tree.sh new file mode 100755 index 0000000..923e761 --- /dev/null +++ b/scripts/check-abi-tree.sh @@ -0,0 +1,53 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# One ABI tree. Fails when the Idris2 ABI surface is duplicated, symlinked, +# mis-cased or inconsistent with its package file. Pure shell: runs without +# idris2, so it can gate PRs on hosts that cannot typecheck. +set -euo pipefail +cd "$(dirname "$0")/.." +fail=0 +say() { echo "[check-abi-tree] $*"; } + +# 1. The symlink farm (PR #140, src/idris-abi/) is retired. +if [ -e src/idris-abi ]; then say "FAIL: src/idris-abi exists (retired symlink farm)"; fail=1; fi + +# 2. Exactly one package file, and it is the one the gates name. +n=$(find src/abi -name '*.ipkg' | wc -l) +if [ "$n" -ne 1 ]; then say "FAIL: expected 1 .ipkg under src/abi, found $n"; fail=1; fi +if [ ! -f src/abi/januskey-abi.ipkg ]; then say "FAIL: src/abi/januskey-abi.ipkg missing"; fail=1; fi + +# 3. Exactly one Foreign.idr under src/ (the FFI surface is declared once). +n=$(find src -name 'Foreign.idr' | wc -l) +if [ "$n" -ne 1 ]; then say "FAIL: expected 1 Foreign.idr under src/, found $n"; fail=1; fi + +# 4. No symlinks under src/abi. +n=$(find src/abi -type l | wc -l) +if [ "$n" -ne 0 ]; then say "FAIL: $n symlink(s) under src/abi"; fail=1; fi + +# 5. Every module declaration matches its path (this is what caught the +# Januskey/JanusKey casing split). +while IFS= read -r f; do + rel=${f#src/abi/}; want=${rel%.idr}; want=${want//\//.} + have=$(grep -m1 -E '^module ' "$f" | awk '{print $2}') + if [ "$have" != "$want" ]; then say "FAIL: $f declares module '$have'; path says '$want'"; fail=1; fi +done < <(find src/abi -name '*.idr' | sort) + +# 6. Every module the package lists has a file; every file is listed. +listed=$(sed -n '/^modules *=/,/^[^ ,]/p' src/abi/januskey-abi.ipkg | tr ',' '\n' | sed 's/^modules *=//; s/^[ ,]*//; s/[ ,]*$//' | grep -E '^[A-Z]' || true) +for m in $listed; do + p="src/abi/${m//./\/}.idr" + if [ ! -f "$p" ]; then say "FAIL: ipkg lists $m but $p is missing"; fail=1; fi +done +while IFS= read -r f; do + rel=${f#src/abi/}; mod=${rel%.idr}; mod=${mod//\//.} + if ! grep -qx "$mod" <<< "$listed"; then say "FAIL: $f is not listed in src/abi/januskey-abi.ipkg"; fail=1; fi +done < <(find src/abi -name '*.idr' | sort) + +# 7. Report, do not fail, on generated trees: they are not part of this gate. +if [ -d generated/idrisiser ]; then + say "note: generated/idrisiser is present and is NOT part of the ABI gate (its modules do not typecheck; see PROOF-NEEDS.adoc)" +fi + +if [ "$fail" -ne 0 ]; then say "FAIL"; exit 1; fi +say "OK: one ABI tree ($(find src/abi -name '*.idr' | wc -l) modules, 1 package)" diff --git a/src/abi/Foreign.idr b/src/abi/JanusKey/ABI/Foreign.idr similarity index 98% rename from src/abi/Foreign.idr rename to src/abi/JanusKey/ABI/Foreign.idr index 1520f8d..358e5e4 100644 --- a/src/abi/Foreign.idr +++ b/src/abi/JanusKey/ABI/Foreign.idr @@ -9,10 +9,10 @@ ||| All functions are declared here with type signatures and safety proofs. ||| Implementations live in ffi/zig/ -module Januskey.ABI.Foreign +module JanusKey.ABI.Foreign -import Januskey.ABI.Types -import Januskey.ABI.Layout +import JanusKey.ABI.Types +import JanusKey.ABI.Layout %default total diff --git a/src/abi/Layout.idr b/src/abi/JanusKey/ABI/Layout.idr similarity index 100% rename from src/abi/Layout.idr rename to src/abi/JanusKey/ABI/Layout.idr diff --git a/src/abi/Proofs.idr b/src/abi/JanusKey/ABI/Proofs.idr similarity index 100% rename from src/abi/Proofs.idr rename to src/abi/JanusKey/ABI/Proofs.idr diff --git a/src/abi/Types.idr b/src/abi/JanusKey/ABI/Types.idr similarity index 100% rename from src/abi/Types.idr rename to src/abi/JanusKey/ABI/Types.idr diff --git a/src/abi/januskey-abi.ipkg b/src/abi/januskey-abi.ipkg new file mode 100644 index 0000000..172b308 --- /dev/null +++ b/src/abi/januskey-abi.ipkg @@ -0,0 +1,20 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Idris2 package for the JanusKey ABI layer. +-- +-- Sources live under src/abi/JanusKey/ABI/.idr, laid out by module +-- name, so `idris2 --typecheck src/abi/januskey-abi.ipkg` reaches them +-- directly. The former src/idris-abi/ symlink farm (PR #140) and the +-- Januskey/JanusKey casing split it worked around are gone; the tree +-- invariants are enforced by scripts/check-abi-tree.sh (just abi-tree-check). +-- +-- Run: idris2 --typecheck src/abi/januskey-abi.ipkg (or: just test-proofs) +package januskey-abi + +sourcedir = "." + +modules = JanusKey.ABI.Types + , JanusKey.ABI.Layout + , JanusKey.ABI.Foreign + , JanusKey.ABI.Proofs diff --git a/src/idris-abi/JanusKey/ABI/Layout.idr b/src/idris-abi/JanusKey/ABI/Layout.idr deleted file mode 120000 index fd00422..0000000 --- a/src/idris-abi/JanusKey/ABI/Layout.idr +++ /dev/null @@ -1 +0,0 @@ -../../../abi/Layout.idr \ No newline at end of file diff --git a/src/idris-abi/JanusKey/ABI/Proofs.idr b/src/idris-abi/JanusKey/ABI/Proofs.idr deleted file mode 120000 index d63c148..0000000 --- a/src/idris-abi/JanusKey/ABI/Proofs.idr +++ /dev/null @@ -1 +0,0 @@ -../../../abi/Proofs.idr \ No newline at end of file diff --git a/src/idris-abi/JanusKey/ABI/Types.idr b/src/idris-abi/JanusKey/ABI/Types.idr deleted file mode 120000 index 2c77c1f..0000000 --- a/src/idris-abi/JanusKey/ABI/Types.idr +++ /dev/null @@ -1 +0,0 @@ -../../../abi/Types.idr \ No newline at end of file diff --git a/src/idris-abi/Januskey/ABI/Foreign.idr b/src/idris-abi/Januskey/ABI/Foreign.idr deleted file mode 120000 index 7495952..0000000 --- a/src/idris-abi/Januskey/ABI/Foreign.idr +++ /dev/null @@ -1 +0,0 @@ -../../../abi/Foreign.idr \ No newline at end of file diff --git a/src/idris-abi/januskey-abi.ipkg b/src/idris-abi/januskey-abi.ipkg deleted file mode 100644 index bdf9f92..0000000 --- a/src/idris-abi/januskey-abi.ipkg +++ /dev/null @@ -1,30 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- --- Idris2 package for the JanusKey ABI layer (src/abi/*.idr). --- --- Idris2 resolves module A.B.C to /A/B/C.idr, but the ABI sources --- live flat in src/abi/ (Types.idr declares JanusKey.ABI.Types, etc.), so no --- sourcedir value can reach them directly. They also cannot be moved: the --- aspect tests, the Mustfile and the Zig FFI all name src/abi/.idr. --- This directory therefore holds relative symlinks laid out by module name, --- each pointing back to the single real file in src/abi/. --- --- Known defect, deliberately NOT fixed here (tracked as J1-3): --- src/abi/Foreign.idr declares `Januskey.ABI.Foreign` (lowercase k) while --- Proofs.idr imports `JanusKey.ABI.Foreign`; Foreign.idr in turn imports --- `Januskey.ABI.Types` and `Januskey.ABI.Layout`, which no file declares. The --- module is listed below under the name it actually declares, so these --- imports fail to resolve until J1-3 normalises the casing. --- The Januskey/ and JanusKey/ directories also collide on case-insensitive --- filesystems (macOS/Windows default); typecheck on Linux. --- --- Run: idris2 --typecheck src/idris-abi/januskey-abi.ipkg (or: just test-proofs) -package januskey-abi - -sourcedir = "." - -modules = JanusKey.ABI.Types - , JanusKey.ABI.Layout - , Januskey.ABI.Foreign - , JanusKey.ABI.Proofs diff --git a/tests/aspect/cross_cutting_test.sh b/tests/aspect/cross_cutting_test.sh index 7b3599f..1324d80 100755 --- a/tests/aspect/cross_cutting_test.sh +++ b/tests/aspect/cross_cutting_test.sh @@ -60,11 +60,11 @@ check "LICENSE directory exists" "[ -d '${JK_DIR}/LICENSES' ]" # --- Proofs --- echo "--- Formal Proofs ---" -check "Types.idr exists (L1-L12)" "[ -f '${JK_DIR}/src/abi/Types.idr' ]" -check "Layout.idr exists (CNO)" "[ -f '${JK_DIR}/src/abi/Layout.idr' ]" -check "Foreign.idr exists (FFI)" "[ -f '${JK_DIR}/src/abi/Foreign.idr' ]" -check "Proofs.idr exists (30+ proofs)" "[ -f '${JK_DIR}/src/abi/Proofs.idr' ]" -check "C header generated" "[ -f '${JK_DIR}/ffi/zig/include/januskey.h' ]" +check "Types.idr exists (L1-L12)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Types.idr' ]" +check "Layout.idr exists (CNO)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Layout.idr' ]" +check "Foreign.idr exists (FFI)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Foreign.idr' ]" +check "Proofs.idr exists (30+ proofs)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Proofs.idr' ]" +check "C header present (mirrors Foreign.idr)" "[ -f '${JK_DIR}/ffi/zig/include/januskey.h' ]" # --- Build --- echo "--- Build ---" From 8c30b177ee80d08b33ba43ba9f90c6881ad61efd Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 12 Oct 2026 22:01:21 +0000 Subject: [PATCH 2/5] =?UTF-8?q?feat(proofs):=20reversibility=20as=20a=20Lo?= =?UTF-8?q?ss=20grade=20=E2=80=94=20Agda=20kernel=20module=20pinned=20to?= =?UTF-8?q?=20resource-algebra?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit verification/proofs/agda/Reversibility.agda (--safe --without-K, builtins only, resource-algebra's Prelude) grades januskey steps in the Loss instance (echo loss: 𝟙 = fin 0, 𝟘 = inf) and proves, for traces of steps: - all-lossless-trace: a trace of 𝟙 steps has grade 𝟙 (⊗ unit law). - lossless-trace-all: a trace of grade 𝟙 has only 𝟙 steps — a hidden loss cannot be papered over by composition. - obliterate-absorbs / obliterated-not-lossless: a trace containing an inf step has grade inf whatever precedes or follows it (annihilation, both sides), so it is never lossless. - wrap-unwrap-𝟙 / wrap-unwrap-id: the wrap/unwrap pair is a two-step trace of grade 𝟙, with the cancellation law `unwrap (wrap x) ≡ x` carried as an explicit premise (ReversiblePair.cancels), discharged outside Agda by crates/reversible-core's wrap/unwrap round-trip property test — cited, not assumed away. Expected rejections (tests/reject-agda, both refused at the intended claim): HiddenLoss (`1 != 0`), ReviveAfterObliterate (`inf != fin 0`). Gate: scripts/check-agda.sh (just test-agda; .github/workflows/agda-proofs.yml, DESIGNED until its first green run on the Debian 2.6.4.3 pin). Sibling: scripts/fetch-siblings.sh pins hyperpolymath/resource-algebra at cf9235c532712a783a404c359a1055f40134794a. Verified locally with Agda 2.6.3 under --safe --without-K --no-libraries --ignore-interfaces --double-check. Not claimed: a step's grade is derived from its code (it is an annotation whose soundness condition is the cancellation premise); file contents; anything cryptographic; the FFI-bridge homomorphism (OPEN on resource-algebra, filed from JNK-01). The Idris2 IsCNO/ReversibleOp pair corresponds to ReversiblePair by transcription — ASSUMED. Refs: JNK-01 step 3 (ISSUES-2026-10-12). Assisted-by: Claude (claude.ai session, 2026-10-12) Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .github/workflows/agda-proofs.yml | 31 ++++ .gitignore | 1 + Justfile | 4 + scripts/check-agda.sh | 27 +++ scripts/fetch-siblings.sh | 17 ++ tests/reject-agda/HiddenLoss.agda | 19 +++ tests/reject-agda/ReviveAfterObliterate.agda | 21 +++ verification/proofs/agda/Reversibility.agda | 164 +++++++++++++++++++ 8 files changed, 284 insertions(+) create mode 100644 .github/workflows/agda-proofs.yml create mode 100755 scripts/check-agda.sh create mode 100755 scripts/fetch-siblings.sh create mode 100644 tests/reject-agda/HiddenLoss.agda create mode 100644 tests/reject-agda/ReviveAfterObliterate.agda create mode 100644 verification/proofs/agda/Reversibility.agda diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml new file mode 100644 index 0000000..b0a1479 --- /dev/null +++ b/.github/workflows/agda-proofs.yml @@ -0,0 +1,31 @@ +# 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 + container: debian:trixie-slim + 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 diff --git a/.gitignore b/.gitignore index e773be4..fdb1a82 100644 --- a/.gitignore +++ b/.gitignore @@ -90,3 +90,4 @@ deps/ .cache/ build/ dist/ +*.agdai diff --git a/Justfile b/Justfile index 8176a69..bf28723 100644 --- a/Justfile +++ b/Justfile @@ -88,6 +88,10 @@ test-contracts: done; \ fi +# Agda kernel proofs (verification/proofs/agda) against the pinned resource-algebra. +test-agda: + bash scripts/check-agda.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 diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh new file mode 100755 index 0000000..787b9e3 --- /dev/null +++ b/scripts/check-agda.sh @@ -0,0 +1,27 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Agda gate for verification/proofs/agda: kernel flags, sibling on the include +# path, and the expected-rejection fixtures under tests/reject-agda refused. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." +export LC_ALL="${LC_ALL:-C.UTF-8}" +prover="${AGDA:-agda}" +"$prover" --version +bash scripts/fetch-siblings.sh +flags=(--safe --without-K --no-libraries --ignore-interfaces --double-check + -i verification/proofs/agda -i _build/dependencies/resource-algebra/src) +"$prover" "${flags[@]}" verification/proofs/agda/Reversibility.agda +mkdir -p _build/check-logs +shopt -s nullglob +rejects=(tests/reject-agda/*.agda) +shopt -u nullglob +for file in "${rejects[@]}"; do + name="$(basename -- "$file" .agda)" + log="_build/check-logs/$name.log" + if "$prover" "${flags[@]}" -i tests/reject-agda "$file" >"$log" 2>&1; then + cat "$log"; echo "ERROR: $file was accepted but must be refused" >&2; exit 1 + fi + echo "refused as expected: $file ($(grep -m1 -E 'error|Error' "$log" | cut -c1-80))" +done +echo "[check-agda] OK" diff --git a/scripts/fetch-siblings.sh b/scripts/fetch-siblings.sh new file mode 100755 index 0000000..9b66a48 --- /dev/null +++ b/scripts/fetch-siblings.sh @@ -0,0 +1,17 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Fetch the proof sibling at a pinned commit (pattern: choreographic-types, +# residual-evidence-types). The Agda module under verification/proofs/agda +# imports resource-algebra's Loss instance; it is consumed by pin, never +# re-declared here. Re-pin deliberately, one commit per pin. +set -euo pipefail +cd -- "$(dirname -- "${BASH_SOURCE[0]}")/.." +RESOURCE_ALGEBRA_COMMIT="${RESOURCE_ALGEBRA_COMMIT:-cf9235c532712a783a404c359a1055f40134794a}" # Loss/MaxPlus/HWM as read 2026-10-12 +mkdir -p _build/dependencies +if [ ! -d _build/dependencies/resource-algebra ]; then + git clone --quiet https://github.com/hyperpolymath/resource-algebra.git _build/dependencies/resource-algebra +fi +git -C _build/dependencies/resource-algebra fetch --quiet origin +git -C _build/dependencies/resource-algebra checkout --quiet "$RESOURCE_ALGEBRA_COMMIT" +echo "resource-algebra at $(git -C _build/dependencies/resource-algebra rev-parse --short HEAD)" diff --git a/tests/reject-agda/HiddenLoss.agda b/tests/reject-agda/HiddenLoss.agda new file mode 100644 index 0000000..9331de4 --- /dev/null +++ b/tests/reject-agda/HiddenLoss.agda @@ -0,0 +1,19 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection: a trace with a lossy step cannot be certified lossless. +-- The claim below is false (fin 1 +g fin 0 = fin 1), and the checker must +-- refuse it; this fixture pins that Theorem 2 is not vacuous. +module HiddenLoss where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Instances.Loss +open import Reversibility + +open Steps Nat + +lossy : Step +lossy = step (λ x → x) (fin 1) + +hidden : traceGrade (lossy ∷ []) ≡ fin 0 +hidden = refl diff --git a/tests/reject-agda/ReviveAfterObliterate.agda b/tests/reject-agda/ReviveAfterObliterate.agda new file mode 100644 index 0000000..2cf6fd9 --- /dev/null +++ b/tests/reject-agda/ReviveAfterObliterate.agda @@ -0,0 +1,21 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection: nothing after an obliterating step restores a lossless +-- grade. The claim below is false (inf +g fin 0 = inf) and must be refused. +module ReviveAfterObliterate where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Instances.Loss +open import Reversibility + +open Steps Nat + +obliterate : Step +obliterate = step (λ x → 0) inf + +restore : Step +restore = step (λ x → x) (fin 0) + +revived : traceGrade (obliterate ∷ restore ∷ []) ≡ fin 0 +revived = refl diff --git a/verification/proofs/agda/Reversibility.agda b/verification/proofs/agda/Reversibility.agda new file mode 100644 index 0000000..3430d82 --- /dev/null +++ b/verification/proofs/agda/Reversibility.agda @@ -0,0 +1,164 @@ +{-# OPTIONS --safe --without-K #-} +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- Reversibility as a grade. +-- +-- januskey's operations are graded in resource-algebra's Loss instance (the +-- echo loss grade): a reversible step costs 𝟙 = fin 0, information loss is +-- fin n, obliteration is inf = 𝟘. Everything below is about the grade +-- algebra and the trace shape; the one operational fact it rests on — that +-- unwrap after wrap is the identity — is a *premise* carried by the +-- ReversiblePair record, discharged outside this module by +-- crates/reversible-core/tests/property_tests.rs (wrap/unwrap round trip), +-- never assumed here. +-- +-- Pinned sibling: hyperpolymath/resource-algebra, see scripts/fetch-siblings.sh. +-- Kernel ruling (2026-10-12): Agda --safe --without-K is the proof kernel; +-- the Idris2 ABI (src/abi/JanusKey/ABI) is the runtime layer. The Idris2 +-- IsCNO / ReversibleOp pair corresponds to ReversiblePair below by +-- transcription (ASSUMED; no mechanical link is claimed). + +module Reversibility where + +open import ResourceAlgebra.Prelude +open import ResourceAlgebra.Core +open import ResourceAlgebra.Instances.Loss + +open IsSeqMonoid (ResourceAlgebra.seq Loss) renaming (unitˡ to ⊗-unitˡ; unitʳ to ⊗-unitʳ; assoc to ⊗-assoc) +open IsAnnihilating Loss-annihilating + +---------------------------------------------------------------------- +-- Steps and traces over an abstract state +---------------------------------------------------------------------- + +module Steps (S : Set) where + + -- A step: what it does to the state, and what it costs in Loss. + record Step : Set where + constructor step + field + run : S → S + grade : Grade + + open Step public + + -- A trace is a list of steps; its grade is the sequence product. + data Trace : Set where + [] : Trace + _∷_ : Step → Trace → Trace + + infixr 5 _∷_ + + traceGrade : Trace → Grade + traceGrade [] = fin 0 + traceGrade (s ∷ ts) = grade s +g traceGrade ts + + -- Lossless: grade 𝟙. + Lossless : Step → Set + Lossless s = grade s ≡ fin 0 + + data AllLossless : Trace → Set where + [] : AllLossless [] + _∷_ : ∀ {s ts} → Lossless s → AllLossless ts → AllLossless (s ∷ ts) + + ---------------------------------------------------------------------- + -- Theorem 1. A trace of lossless steps is lossless (the ⊗ unit law). + ---------------------------------------------------------------------- + + all-lossless-trace : ∀ ts → AllLossless ts → traceGrade ts ≡ fin 0 + all-lossless-trace [] [] = refl + all-lossless-trace (s ∷ ts) (p ∷ ps) = + trans (cong (_+g traceGrade ts) p) + (trans (⊗-unitˡ (traceGrade ts)) (all-lossless-trace ts ps)) + + ---------------------------------------------------------------------- + -- Theorem 2. A lossless trace hides no lossy step: if the product is + -- fin 0 then every factor is fin 0. This is what makes "reversible by + -- construction" checkable — a hidden loss cannot be papered over by + -- composition. + ---------------------------------------------------------------------- + + private + +g-zero-left : ∀ a b → a +g b ≡ fin 0 → a ≡ fin 0 + +g-zero-left (fin zero) (fin n) _ = refl + +g-zero-left (fin (suc m)) (fin n) () + +g-zero-left (fin m) inf () + +g-zero-left inf _ () + + +g-zero-right : ∀ a b → a +g b ≡ fin 0 → b ≡ fin 0 + +g-zero-right (fin m) (fin zero) _ = refl + +g-zero-right (fin zero) (fin (suc n)) () + +g-zero-right (fin (suc m)) (fin (suc n)) () + +g-zero-right (fin m) inf () + +g-zero-right inf _ () + + lossless-trace-all : ∀ ts → traceGrade ts ≡ fin 0 → AllLossless ts + lossless-trace-all [] _ = [] + lossless-trace-all (s ∷ ts) p = + +g-zero-left (grade s) (traceGrade ts) p + ∷ lossless-trace-all ts (+g-zero-right (grade s) (traceGrade ts) p) + + ---------------------------------------------------------------------- + -- Theorem 3. Obliteration absorbs: a trace containing an inf step has + -- grade inf, whatever comes before or after (annihilation, both sides). + ---------------------------------------------------------------------- + + data Contains (s : Step) : Trace → Set where + here : ∀ {ts} → Contains s (s ∷ ts) + there : ∀ {t ts} → Contains s ts → Contains s (t ∷ ts) + + Obliterating : Step → Set + Obliterating s = grade s ≡ inf + + obliterate-absorbs : ∀ {s} ts → Obliterating s → Contains s ts → traceGrade ts ≡ inf + obliterate-absorbs {s} (.s ∷ ts) o here = + trans (cong (_+g traceGrade ts) o) (annihilˡ (traceGrade ts)) + obliterate-absorbs (t ∷ ts) o (there c) = + trans (cong (grade t +g_) (obliterate-absorbs ts o c)) (annihilʳ (grade t)) + + -- And so no trace with an obliteration is lossless. + inf≢fin0 : inf ≡ fin 0 → ⊥ + inf≢fin0 () + + obliterated-not-lossless : ∀ {s} ts → Obliterating s → Contains s ts → traceGrade ts ≡ fin 0 → ⊥ + obliterated-not-lossless ts o c p = inf≢fin0 (trans (sym (obliterate-absorbs ts o c)) p) + + ---------------------------------------------------------------------- + -- The reversible pair: wrap then unwrap. The cancellation law is the + -- operational premise (januskey's wrap/unwrap round-trip property test); + -- given it, both steps are graded 𝟙 and the two-step trace is lossless. + ---------------------------------------------------------------------- + + record ReversiblePair : Set where + constructor pair + field + wrap : S → S + unwrap : S → S + cancels : ∀ x → unwrap (wrap x) ≡ x + + open ReversiblePair public + + wrapStep : ReversiblePair → Step + wrapStep p = step (wrap p) (fin 0) + + unwrapStep : ReversiblePair → Step + unwrapStep p = step (unwrap p) (fin 0) + + 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. + wrap-unwrap-id : ∀ p x → run (unwrapStep p) (run (wrapStep p) x) ≡ x + wrap-unwrap-id p x = cancels p x + +---------------------------------------------------------------------- +-- What is NOT claimed. The grade of a step is an annotation; this module +-- proves what follows from the annotations under the Loss algebra. It does +-- not derive a step's grade from its code, does not model file contents, +-- and says nothing cryptographic about obliteration. The bridge obligation +-- — that the Zig/Rust FFI wrapper of a grade-𝟙 operation is grade-𝟙 — is a +-- homomorphism statement that resource-algebra lists as OPEN; it is filed, +-- not proved here. +---------------------------------------------------------------------- From 5f17a4573a224a8d3acad8c80e5a4640538b4c0e Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 23:40:50 +0000 Subject: [PATCH 3/5] test(proofs): Agda fixtures must fail for their stated reason; cite the test that discharges the premise check-agda.sh counted any failure of a tests/reject-agda fixture as the expected refusal, so a fixture broken by an unrelated change (a renamed import, a parse error) would keep the gate green while testing nothing. Its reason column was also always empty: Agda does not print "error". - Each fixture now carries `-- expect: `; the gate fails if the line is missing, if the fixture is accepted, or if the refusal log does not contain that text. An empty fixture directory also fails. HiddenLoss expects `1 != 0`, ReviveAfterObliterate `inf != fin 0`. - Passing fixtures print `[PASS] refused as expected: ()`. Negative controls run locally (Agda 2.6.3, not committed): a fixture refused for a missing import -> FAIL "refused, but not with '1 != 0'"; no expect line -> FAIL; an accepted fixture -> FAIL. Reversibility.agda (comments only, no definition changed): the cancellation premise was cited as "crates/reversible-core/tests/ property_tests.rs (wrap/unwrap round trip)". No such test or API exists; unwrap_safety_test.rs is about Rust's .unwrap(). The premise is execute/undo (ReversibleExecutor in crates/reversible-core/src/lib.rs), tested by crates/januskey-cli/tests/property_tests.rs:: execute_then_undo_is_identity, already a TESTED ledger row. The comments now say so. Refs: JNK-01 step 3. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- scripts/check-agda.sh | 11 ++++++++++- tests/reject-agda/HiddenLoss.agda | 1 + tests/reject-agda/ReviveAfterObliterate.agda | 1 + verification/proofs/agda/Reversibility.agda | 10 ++++++---- 4 files changed, 18 insertions(+), 5 deletions(-) diff --git a/scripts/check-agda.sh b/scripts/check-agda.sh index 787b9e3..73e9d92 100755 --- a/scripts/check-agda.sh +++ b/scripts/check-agda.sh @@ -16,12 +16,21 @@ mkdir -p _build/check-logs shopt -s nullglob rejects=(tests/reject-agda/*.agda) shopt -u nullglob +[ "${#rejects[@]}" -gt 0 ] || { echo "ERROR: no fixtures under tests/reject-agda" >&2; exit 1; } +# Each fixture names the refusal it exists for in a `-- expect: ` line; +# a fixture refused for any other reason (a broken import, a parse error) has +# stopped testing its claim, so it fails the gate too. for file in "${rejects[@]}"; do name="$(basename -- "$file" .agda)" log="_build/check-logs/$name.log" + want="$(sed -n 's/^-- expect: //p' "$file" | head -1)" + [ -n "$want" ] || { echo "ERROR: $file has no '-- expect: ' line" >&2; exit 1; } if "$prover" "${flags[@]}" -i tests/reject-agda "$file" >"$log" 2>&1; then cat "$log"; echo "ERROR: $file was accepted but must be refused" >&2; exit 1 fi - echo "refused as expected: $file ($(grep -m1 -E 'error|Error' "$log" | cut -c1-80))" + if ! grep -qF -- "$want" "$log"; then + cat "$log"; echo "ERROR: $file was refused, but not with '$want'" >&2; exit 1 + fi + echo "[PASS] refused as expected: $file ($want)" done echo "[check-agda] OK" diff --git a/tests/reject-agda/HiddenLoss.agda b/tests/reject-agda/HiddenLoss.agda index 9331de4..a2097a7 100644 --- a/tests/reject-agda/HiddenLoss.agda +++ b/tests/reject-agda/HiddenLoss.agda @@ -4,6 +4,7 @@ -- Expected rejection: a trace with a lossy step cannot be certified lossless. -- The claim below is false (fin 1 +g fin 0 = fin 1), and the checker must -- refuse it; this fixture pins that Theorem 2 is not vacuous. +-- expect: 1 != 0 module HiddenLoss where open import ResourceAlgebra.Prelude diff --git a/tests/reject-agda/ReviveAfterObliterate.agda b/tests/reject-agda/ReviveAfterObliterate.agda index 2cf6fd9..ebf7526 100644 --- a/tests/reject-agda/ReviveAfterObliterate.agda +++ b/tests/reject-agda/ReviveAfterObliterate.agda @@ -3,6 +3,7 @@ -- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -- Expected rejection: nothing after an obliterating step restores a lossless -- grade. The claim below is false (inf +g fin 0 = inf) and must be refused. +-- expect: inf != fin 0 module ReviveAfterObliterate where open import ResourceAlgebra.Prelude diff --git a/verification/proofs/agda/Reversibility.agda b/verification/proofs/agda/Reversibility.agda index 3430d82..0d30206 100644 --- a/verification/proofs/agda/Reversibility.agda +++ b/verification/proofs/agda/Reversibility.agda @@ -9,9 +9,11 @@ -- fin n, obliteration is inf = 𝟘. Everything below is about the grade -- algebra and the trace shape; the one operational fact it rests on — that -- unwrap after wrap is the identity — is a *premise* carried by the --- ReversiblePair record, discharged outside this module by --- crates/reversible-core/tests/property_tests.rs (wrap/unwrap round trip), --- never assumed here. +-- ReversiblePair record, never assumed here. In the Rust, wrap is +-- `ReversibleExecutor::execute` and unwrap is `undo` +-- (crates/reversible-core/src/lib.rs); the premise is tested by +-- crates/januskey-cli/tests/property_tests.rs::execute_then_undo_is_identity, +-- a TESTED row of the claims ledger in PROOF-NEEDS.adoc. -- -- Pinned sibling: hyperpolymath/resource-algebra, see scripts/fetch-siblings.sh. -- Kernel ruling (2026-10-12): Agda --safe --without-K is the proof kernel; @@ -126,7 +128,7 @@ module Steps (S : Set) where ---------------------------------------------------------------------- -- The reversible pair: wrap then unwrap. The cancellation law is the - -- operational premise (januskey's wrap/unwrap round-trip property test); + -- operational premise (execute_then_undo_is_identity, cited above); -- given it, both steps are graded 𝟙 and the two-step trace is lossless. ---------------------------------------------------------------------- From dca00f829f56838a53e34323dfbb014103e59599 Mon Sep 17 00:00:00 2001 From: Claude Date: Tue, 13 Oct 2026 23:52:58 +0000 Subject: [PATCH 4/5] ci(proofs): pin the Agda job's Debian image by digest agda-proofs.yml ran in `debian:trixie-slim` by tag while the rest of the prover setup is pinned (agda-bin=2.6.4.3-1+b2, resource-algebra by commit, actions/checkout by SHA) and idris-abi.yml pins its image by digest. The tag moves with every Debian point release, so the job could change under the same commit. Pinned to the trixie-slim index digest resolved from registry-1.docker.io on 2026-10-13. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .github/workflows/agda-proofs.yml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml index b0a1479..2f53eef 100644 --- a/.github/workflows/agda-proofs.yml +++ b/.github/workflows/agda-proofs.yml @@ -15,7 +15,8 @@ jobs: proofs: name: Reversibility as a grade (Loss instance), expected rejections runs-on: ubuntu-latest - container: debian:trixie-slim + # 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: | From ad0c833a0799911d7c90706ca7e9e0da31367300 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Wed, 14 Oct 2026 00:58:55 +0100 Subject: [PATCH 5/5] fix(abi): real jk_* FFI, ABI typechecks under Idris2 0.8.0, gates and claims ledger (JNK-01, C of 3) (#151) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit ## Summary JNK-01, stacked PR **C of 3**. The base is B, #150, which sits on A, #149. Review the commits from `0e477cb` on. With this PR the Idris2 ABI typechecks, its obligations are gated, and the dashboards carry a proof count that `dashboard-check` measures. It covers #145's acceptance criteria; #145 will be closed with the gate link once this is green. | Commit | What | |---|---| | `0e477cb` | Handoff patch 0003, unchanged. `Foreign.idr` declares the 13 real `jk_*` symbols from `januskey.h`; `Status` closed sum with total decoder, round-trip and injectivity; op-kind/algorithm codecs; `closeOnce : (1 h : LibHandle Open) -> IO (LibHandle Closed)` | | `7ff5767` | Handoff patch 0004, unchanged. Types/Layout/Proofs typecheck; placeholders replaced by `seqCNO`, `copyIsCNO`, `tamperBreaksLink`, `obliterateNotReversible`, or removed | | `91ee42f` | Handoff patch 0005, unchanged. `check-abi-layout.sh` (Idris ↔ header ↔ Zig), `check-idris-reject.sh` with three fixtures, status table in PROOF-NEEDS | | `922fa43` | **Found while verifying.** Rejection fixtures must fail for their stated reason, and `DoubleClose` was not testing a double close (below). The aspect-test census now covers `assert_smaller`, `partial` and holes, as PROOF-NEEDS already claimed it did | | `8327321` | #145 items 3 and 5: the Proofs header and the adversary lemmas restated honestly. `revokedKeyUnusable` removed: it took no revocation | | `c132e0f` | **Runbook step 4.** Claims ledger: 8 PROVEN, 5 new TESTED, 2 ASSUMED, 4 OPEN rows. README/TOPOLOGY/READINESS reconciled. `dashboard-check.yml` gets Idris2 and Agda | | `4a89651` | Merge of B's Debian digest pin (no new content) | ### Two findings the handoff did not have 1. **`DoubleClose` did not test a double close.** Idris2 refused it at the *first* `closeOnce h` (line 14, col 18) with "Trying to use linear name h in non-linear context". IO's `>>=` is not linear, so a *single* close in `do` is refused the same way. The fixture now puts both closes in a linear pair (`closeOnce h # closeOnce h`) and is refused with **"There are 2 uses of linear name h"**. Positive controls typecheck: `closeOnce h` and `closeOnce h # pure ()`. The consequence, now in `LibHandle`'s docstring: a linearly held handle cannot be closed inside plain IO `do` at all. Sequencing linear steps needs `Control.Linear.LIO`, which this module does not use. 2. **Pinning the expected message has its own trap.** Idris echoes source lines in its errors, so a fixture's `-- expect:` comment matched itself, and my first wrong-reason control *passed*. The gate now matches message lines only (` NN | ` excerpts excluded), and that control now fails. ## How has this been verified? ### HANDOFF §3, run exactly on the unmodified five-patch stack (`d565dbf`), Idris2 0.8.0 (bootstrap build of tag v0.8.0) and Agda 2.6.3 Every line matches the handoff. Filtered for length: Agda's per-dependency "Checking" lines, the 29 individual aspect `[PASS]` lines and section banners. ``` $ bash scripts/check-abi-tree.sh [check-abi-tree] OK: one ABI tree (4 modules, 1 package) $ bash scripts/check-abi-layout.sh [check-abi-layout] OK struct sizes (hash, keyid, oblit): 32 16 112 [check-abi-layout] OK oblit proof size vs header comment: 112 [check-abi-layout] OK status codes: 0 1 2 3 4 5 6 7 8 9 10 11 [check-abi-layout] OK status count: 12 [check-abi-layout] OK op kinds: 0 1 2 3 4 5 6 7 [check-abi-layout] OK algorithms: 0 1 2 3 4 [check-abi-layout] OK exported symbols: jk_close jk_execute jk_generate_key jk_init jk_obliterate jk_open jk_revoke_key jk_rotate_key jk_tx_begin jk_tx_commit jk_tx_rollback jk_undo jk_version [check-abi-layout] OK zig exports: (same 13) [check-abi-layout] OK: Idris2 ABI, januskey.h and ffi/zig agree $ idris2 --version Idris 2, version 0.8.0 $ idris2 --typecheck src/abi/januskey-abi.ipkg 1/4: Building JanusKey.ABI.Types (JanusKey/ABI/Types.idr) 2/4: Building JanusKey.ABI.Layout (JanusKey/ABI/Layout.idr) 3/4: Building JanusKey.ABI.Foreign (JanusKey/ABI/Foreign.idr) 4/4: Building JanusKey.ABI.Proofs (JanusKey/ABI/Proofs.idr) $ bash scripts/check-idris-reject.sh [check-idris-reject] refused as expected: tests/reject-idris/DoubleClose.idr (Error: While processing right hand side of twice. Trying to use linear name h in non-linea) [check-idris-reject] refused as expected: tests/reject-idris/ForgottenClose.idr (Error: While processing right hand side of leak. There are 0 uses of linear name h. ) [check-idris-reject] refused as expected: tests/reject-idris/UnknownStatusIsOk.idr (Error: While processing right hand side of twelveIsOk. When unifying:) $ bash scripts/check-agda.sh Agda version 2.6.3 resource-algebra at cf9235c refused as expected: tests/reject-agda/HiddenLoss.agda () refused as expected: tests/reject-agda/ReviveAfterObliterate.agda () [check-agda] OK $ bash tests/aspect/cross_cutting_test.sh PASS: 29 FAIL: 0 $ just test-proofs test-proofs-reject test-agda ... (the same output) ... exit 0 ``` The empty `()` reasons and the `DoubleClose` reason ("non-linear context") are the two anomalies that commits `5f17a45` (in B) and `922fa43` fix. ### This head: `just test-proofs test-proofs-reject test-agda` and the aspect test ``` [check-abi-tree] OK: one ABI tree (4 modules, 1 package) [check-abi-layout] PASS: Idris2 ABI, januskey.h and ffi/zig agree [OK] ABI package typechecks [check-idris-reject] PASS refused as expected: tests/reject-idris/DoubleClose.idr (There are 2 uses of linear name h) [check-idris-reject] PASS refused as expected: tests/reject-idris/ForgottenClose.idr (There are 0 uses of linear name h) [check-idris-reject] PASS refused as expected: tests/reject-idris/UnknownStatusIsOk.idr (Mismatch between: Just Ok and Nothing) [PASS] refused as expected: tests/reject-agda/HiddenLoss.agda (1 != 0) [PASS] refused as expected: tests/reject-agda/ReviveAfterObliterate.agda (inf != fin 0) [check-agda] OK PASS: 32 FAIL: 0 ``` ### `cargo run -q -p dashboard-check -- --check .` on this head The command exits 0 and every row is discharged; the final line is `✓ 119 tests measured, 8 PROVEN claims`. - Positive control: before the dashboard edits, the checker reported exactly the three stale "0 proofs" claims (TOPOLOGY:80, READINESS:12, READINESS:67). - Negative control: in a scratch copy with `seqCNO`'s proof broken, all seven Idris PROVEN rows fail with `` `idris2 --typecheck src/abi/januskey-abi.ipkg` failed ``. This is the first time PROVEN has been exercised on real rows rather than the unit tests' fake runner (#146). Negative controls for the gates, run locally and not committed: - **Rejection gate:** a fixture refused for a missing import fails; the old `DoubleClose` shape fails ("refused, but not with 'There are 2 uses of linear name h'"); a missing expect line fails; an accepted fixture fails; an unknown fixture name fails. - **Census:** each of `assert_smaller`, bare `partial`, `%default partial` and `?hole` in a scratch module fails its own check, and the same words in comments or docstrings do not. - **Layout gate:** a perturbed status code fails. ## Status rows moved | ID | Was | Now | Artefact | |---|---|---|---| | A-1, A-2, C-1…C-5 | — (the package did not typecheck) | PROVEN | `Foreign.idr::statusCodeInjective`, `::opKindRoundTrip`; `Proofs.idr::seqCNO`, `::tamperBreaksLink`; `Layout.idr::copyIsCNO`, `::obliterateNotReversible`, `::oblitAligned`; command `idris2 --typecheck src/abi/januskey-abi.ipkg` | | G-1 | — | PROVEN | `Reversibility.agda::lossless-trace-all`; command `bash scripts/check-agda.sh` | | A-3, A-4 ×2, A-5, bypass census | — | TESTED | `check-abi-layout.sh`; `tests/reject-idris/{DoubleClose,ForgottenClose,UnknownStatusIsOk}.idr`; `tests/aspect/cross_cutting_test.sh` | | A-4 (status table) | "PROVEN at the type; TESTED" | TESTED | one status per row; the fixtures are the evidence | | X-1 | EXTERNAL | ASSUMED | EXTERNAL is not a ledger status | | G-2 | ASSUMED (transcription) | ASSUMED | unchanged, now a ledger row | | G-3, E-1 (new), six security obligations, MPR-linked-to-Rust | OPEN (#145) | OPEN | file artefacts; #145 closes with this stack | ## Type of change - [x] 🐛 Bug fix: the ABI did not typecheck; the FFI described a template, not `ffi/zig` - [x] 🕳️ Soundness fix: tautological "proofs" removed; non-discriminating fixture fixed; census enforced - [x] 📖 Documentation: PROOF-NEEDS, README, TOPOLOGY, READINESS - [x] 🔧 Build / CI / tooling ## 📌 New pins - `dashboard-check.yml` runs in `ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff`. This is the digest `idris-abi.yml` already uses; it is new to this workflow. - `agda-bin=2.6.3-1build1` (Ubuntu noble), installed in that container, the version every local check here used. **Assumption to confirm in CI:** that the pinned pack image is the noble build. pack publishes noble and jammy; `latest` is noble. I could not read the image config from this session. ## Checklist - [x] Commits are signed, each with a `gpgsig` header. Note: the merge commit `4a89651` lacks the session trailer lines; it carries no content of its own. - [x] Project checks pass locally (above). No Rust source changed. - [x] New files carry SPDX identifiers. - [x] Docs updated. The dashboard numbers come from the ledger via `dashboard-check`, not written by hand. - [x] No soundness hole introduced: bypass census 32/32, enforced by a TESTED ledger row. ## Notes for reviewers - **Expected review questions, answered here:** - **`seqOp` keeps the first op's kind tag.** `ReversibleOp` has no sequence kind, and nothing depends on the tag. Documented at the definition. - **`LibHandle` vs `Types.Handle` are two notions, deliberately.** `LibHandle` is the wire handle with ownership. `Types.Handle` is the L7 aliasing model. - **Owner decision still needed: `generated/idrisiser/`.** Regenerate it with capitalised module names, or remove it. It is outside the gate and still does not typecheck. - **Not claimed:** "data loss is architecturally impossible" (the README caution stays); hash one-wayness and physical erasure (X-1, ASSUMED); the FFI-bridge homomorphism (G-3, OPEN). - **Not touched:** `STATE.a2ml` `[test-coverage]`, a dated 2026-04 snapshot that still says `idris2-proofs = "30"`, and its `idris2-in-ci` blocker. `dashboard-check` does not reconcile those fields. Owner's call. - Each red check will be examined once CI reports. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- _Generated by [Claude Code](https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9)_ --------- Co-authored-by: Claude --- .github/workflows/dashboard-check.yml | 13 +- .github/workflows/idris-abi.yml | 4 + Justfile | 10 +- PROOF-NEEDS.adoc | 115 +++++- READINESS.adoc | 13 +- README.adoc | 2 +- TOPOLOGY.adoc | 6 +- scripts/check-abi-layout.sh | 50 +++ scripts/check-idris-reject.sh | 44 +++ src/abi/JanusKey/ABI/Foreign.idr | 455 +++++++++++++++-------- src/abi/JanusKey/ABI/Layout.idr | 61 +-- src/abi/JanusKey/ABI/Proofs.idr | 161 ++++---- src/abi/JanusKey/ABI/Types.idr | 57 +-- tests/aspect/cross_cutting_test.sh | 8 +- tests/reject-idris/DoubleClose.idr | 18 + tests/reject-idris/ForgottenClose.idr | 13 + tests/reject-idris/UnknownStatusIsOk.idr | 13 + 17 files changed, 714 insertions(+), 329 deletions(-) create mode 100755 scripts/check-abi-layout.sh create mode 100755 scripts/check-idris-reject.sh create mode 100644 tests/reject-idris/DoubleClose.idr create mode 100644 tests/reject-idris/ForgottenClose.idr create mode 100644 tests/reject-idris/UnknownStatusIsOk.idr diff --git a/.github/workflows/dashboard-check.yml b/.github/workflows/dashboard-check.yml index ad2219e..4475ee4 100644 --- a/.github/workflows/dashboard-check.yml +++ b/.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 diff --git a/.github/workflows/idris-abi.yml b/.github/workflows/idris-abi.yml index 0dd020f..617cfd3 100644 --- a/.github/workflows/idris-abi.yml +++ b/.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 diff --git a/Justfile b/Justfile index bf28723..737427b 100644 --- a/Justfile +++ b/Justfile @@ -92,13 +92,21 @@ test-contracts: 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 ===" diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 6d6039e..6a51e9f 100644 --- a/PROOF-NEEDS.adoc +++ b/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,8 +151,11 @@ 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"] |=== @@ -102,24 +163,44 @@ proof in this repository is checked by anything. |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. diff --git a/READINESS.adoc b/READINESS.adoc index f81065c..a344e22 100644 --- a/READINESS.adoc +++ b/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 diff --git a/README.adoc b/README.adoc index 50f3067..9a9ed63 100644 --- a/README.adoc +++ b/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] diff --git a/TOPOLOGY.adoc b/TOPOLOGY.adoc index fecd46f..5733453 100644 --- a/TOPOLOGY.adoc +++ b/TOPOLOGY.adoc @@ -1,5 +1,5 @@ == JanusKey — Project Topology -// Last updated: 2026-10-02 (test and proof counts reconciled to the PROOF-NEEDS claims ledger by dashboard-check) +// Last updated: 2026-10-13 (proof count reconciled to the PROOF-NEEDS claims ledger by dashboard-check) === System Architecture @@ -77,8 +77,8 @@ SECURITY (honest) INTERFACES & RESEARCH CLI Interface (jk) ████████░░ ~85% Full command set; no user testing yet MPR Methodology ████░░░░░░ ~40% Design documented; FORMAL PROOFS PENDING - (Idris2 ABI does not typecheck, #145; 0 proofs checked; not linked - to the Rust) + (Idris2 ABI typechecks; 8 proofs checked: ABI and grade + lemmas, not the security obligations; MPR not linked to the Rust) Testing (READINESS matrix) ██████░░░░ ~60% 119 tests + 5 benches; missing fuzz, mutation, chaos, compatibility (Grade D) diff --git a/scripts/check-abi-layout.sh b/scripts/check-abi-layout.sh new file mode 100755 index 0000000..cf80c77 --- /dev/null +++ b/scripts/check-abi-layout.sh @@ -0,0 +1,50 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Idris2 ABI <-> C header <-> Zig agreement, mechanically, without a compiler: +# - struct sizes: Layout.idr StructSize vs ffi/zig/src/main.zig @sizeOf asserts +# - status codes: Foreign.idr statusCode table vs januskey.h JK_* #defines +# - op kinds / algorithms: Foreign.idr code tables vs januskey.h enum values +# Any drift between the three fails the gate. +set -euo pipefail +cd "$(dirname "$0")/.." +F=src/abi/JanusKey/ABI/Foreign.idr +L=src/abi/JanusKey/ABI/Layout.idr +H=ffi/zig/include/januskey.h +Z=ffi/zig/src/main.zig +fail=0 +say() { echo "[check-abi-layout] $*"; } +same() { # name, expected-list, actual-list + if [ "$2" = "$3" ]; then say "OK $1: $2"; else say "FAIL $1: Idris [$2] vs C/Zig [$3]"; fail=1; fi +} + +# 1. Struct sizes (name order: content hash, key id, obliteration proof) +idris_sizes=$(grep -oE '^(contentHashSize|keyIdSize|oblitProofSize) : StructSize [0-9]+' "$L" | awk '{print $NF}' | tr '\n' ' ' | sed 's/ $//') +zig_sizes=$(grep -oE '@sizeOf\((ContentHash|KeyId|OblitProof)\) == [0-9]+' "$Z" | sort -u | awk '{print $NF}' | tr '\n' ' ' | sed 's/ $//') +same "struct sizes (hash, keyid, oblit)" "$idris_sizes" "$zig_sizes" +hdr_oblit=$(grep -oE 'jk_oblit_proof_t; /\* [0-9]+ bytes' "$H" | grep -oE '[0-9]+' | head -1) +same "oblit proof size vs header comment" "$(echo "$idris_sizes" | awk '{print $3}')" "$hdr_oblit" + +# 2. Status codes, in table order +idris_status=$(grep -oE '^statusCode [A-Za-z]+ += [0-9]+' "$F" | awk '{print $NF}' | tr '\n' ' ' | sed 's/ $//') +hdr_status=$(grep -oE '^#define JK_(OK|ERR_[A-Z_]+) +[0-9]+' "$H" | awk '{print $NF}' | tr '\n' ' ' | sed 's/ $//') +same "status codes" "$idris_status" "$hdr_status" +n_idris=$(grep -cE '^ (Ok|Err[A-Za-z]+) +: Status' "$F"); n_hdr=$(grep -cE '^#define JK_(OK|ERR_)' "$H") +same "status count" "$n_idris" "$n_hdr" + +# 3. Op kinds and algorithms, in enum order +idris_ops=$(grep -oE '^opKindCode [A-Za-z]+ += [0-9]+' "$F" | awk '{print $NF}' | tr '\n' ' ' | sed 's/ $//') +hdr_ops=$(grep -oE 'JK_OP_[A-Z_]+ += [0-9]+' "$H" | awk '{print $NF}' | tr '\n' ' ' | sed 's/ $//') +same "op kinds" "$idris_ops" "$hdr_ops" +idris_alg=$(grep -oE '^algorithmCode [A-Za-z0-9]+ += [0-9]+' "$F" | awk '{print $NF}' | tr '\n' ' ' | sed 's/ $//') +hdr_alg=$(grep -oE 'JK_ALGO_[A-Z0-9_]+ += [0-9]+' "$H" | awk '{print $NF}' | tr '\n' ' ' | sed 's/ $//') +same "algorithms" "$idris_alg" "$hdr_alg" + +# 4. Every exported jk_* symbol in the header has a %foreign declaration, and vice versa +hdr_syms=$(grep -oE '\bjk_[a-z_]+\(' "$H" | tr -d '(' | sort -u | tr '\n' ' ' | sed 's/ $//') +idris_syms=$(grep -oE '%foreign "C:jk_[a-z_]+' "$F" | sed 's/%foreign "C://' | sort -u | tr '\n' ' ' | sed 's/ $//') +same "exported symbols" "$idris_syms" "$hdr_syms" +zig_syms=$(grep -oE 'pub export fn jk_[a-z_]+' "$Z" | awk '{print $NF}' | sort -u | tr '\n' ' ' | sed 's/ $//') +same "zig exports" "$idris_syms" "$zig_syms" + +[ "$fail" -eq 0 ] && say "PASS: Idris2 ABI, januskey.h and ffi/zig agree" || { say "FAIL"; exit 1; } diff --git a/scripts/check-idris-reject.sh b/scripts/check-idris-reject.sh new file mode 100755 index 0000000..978a769 --- /dev/null +++ b/scripts/check-idris-reject.sh @@ -0,0 +1,44 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# Expected-rejection fixtures for the Idris2 ABI. Each file under +# tests/reject-idris is appended to a scratch copy of the package as +# JanusKey.ABI.Reject. and must FAIL to typecheck; a fixture that +# typechecks means a guarantee has been lost. Each fixture names the refusal +# it exists for in a `-- expect: ` line; a fixture refused for another +# reason (a renamed import, a parse error) has stopped testing its claim and +# fails too. Requires idris2 (0.8.0 in CI). +# Usage: check-idris-reject.sh [Name ...] (default: every fixture) +set -euo pipefail +cd "$(dirname "$0")/.." +command -v idris2 >/dev/null 2>&1 || { echo "FAIL: idris2 not installed" >&2; exit 1; } +if [ "$#" -gt 0 ]; then + fixtures=(); for n in "$@"; do fixtures+=("tests/reject-idris/$n.idr"); done +else + shopt -s nullglob; fixtures=(tests/reject-idris/*.idr); shopt -u nullglob +fi +[ "${#fixtures[@]}" -gt 0 ] || { echo "FAIL: no fixtures under tests/reject-idris" >&2; exit 1; } +tmp=$(mktemp -d); trap 'rm -rf "$tmp"' EXIT +cp -r src/abi "$tmp/abi" +mkdir -p "$tmp/abi/JanusKey/ABI/Reject" "$tmp/logs" +status=0 +for f in "${fixtures[@]}"; do + name=$(basename "$f" .idr) + if [ ! -f "$f" ]; then echo "[check-idris-reject] FAIL: $f does not exist"; status=1; continue; fi + want=$(sed -n 's/^-- expect: //p' "$f" | head -1) + if [ -z "$want" ]; then echo "[check-idris-reject] FAIL: $f has no '-- expect: ' line"; status=1; continue; fi + cp "$f" "$tmp/abi/JanusKey/ABI/Reject/$name.idr" + { cat src/abi/januskey-abi.ipkg; echo " , JanusKey.ABI.Reject.$name"; } > "$tmp/abi/reject-$name.ipkg" + if (cd "$tmp/abi" && idris2 --typecheck "reject-$name.ipkg" > "$tmp/logs/$name.log" 2>&1); then + echo "[check-idris-reject] FAIL: $f typechecked but must be refused"; status=1 + # Match the message only: Idris echoes source lines (` NN | ...`), and the + # fixture's own `-- expect:` comment must not count as the refusal. + elif ! grep -vE '^ *[0-9]+ \| ' "$tmp/logs/$name.log" | grep -qF -- "$want"; then + cat "$tmp/logs/$name.log" + echo "[check-idris-reject] FAIL: $f was refused, but not with '$want'"; status=1 + else + echo "[check-idris-reject] PASS refused as expected: $f ($want)" + fi + rm -f "$tmp/abi/JanusKey/ABI/Reject/$name.idr" "$tmp/abi/reject-$name.ipkg" +done +exit $status diff --git a/src/abi/JanusKey/ABI/Foreign.idr b/src/abi/JanusKey/ABI/Foreign.idr index 358e5e4..f1ef8ca 100644 --- a/src/abi/JanusKey/ABI/Foreign.idr +++ b/src/abi/JanusKey/ABI/Foreign.idr @@ -1,219 +1,368 @@ -- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell -||| SPDX-License-Identifier: MPL-2.0 -||| Foreign Function Interface Declarations for JANUSKEY -||| -||| This module declares all C-compatible functions that will be -||| implemented in the Zig FFI layer. -||| -||| All functions are declared here with type signatures and safety proofs. -||| Implementations live in ffi/zig/ +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- +-- JanusKey ABI — foreign function interface. +-- +-- This module is the Idris2 side of ffi/zig/include/januskey.h. Every +-- `%foreign` declaration below names one exported symbol of libjanuskey +-- (implemented in ffi/zig/src/main.zig) with the C signature the header +-- gives it. The header is hand-maintained; this module must mirror it, and +-- the two are kept honest by the status, op-kind and algorithm codecs here, +-- whose encodings are the header's `#define`s and enum values, each with a +-- total decoder and a machine-checked round-trip lemma. +-- +-- What is and is not claimed: +-- * Claimed: the codecs are total and injective (lemmas below); the +-- foreign signatures agree with januskey.h at the level of C types. +-- * Not claimed: that the Zig implementation returns only the codes it +-- documents, or anything about its behaviour. That is ffi/zig's test +-- suite's job (ffi/zig/test/integration_test.zig). +-- * Out-pointer parameters (`jk_handle_t*`, `jk_key_id_t*`, +-- `jk_oblit_proof_t*`) are declared as `AnyPtr` cells the caller owns. +-- Allocation of those cells is a C/Zig-side concern, not modelled here. +-- +-- History: until 2026-10-12 this file carried the RSR template FFI +-- (`januskey_init`, `januskey_process`, `januskey_get_string`, …) written +-- against template types that Types.idr never defined; it did not describe +-- ffi/zig at all. See PROOF-NEEDS.adoc, "One ABI tree". module JanusKey.ABI.Foreign import JanusKey.ABI.Types import JanusKey.ABI.Layout +import Data.Vect +import Data.So +import Data.Maybe +import Control.Function %default total -------------------------------------------------------------------------------- --- Library Lifecycle +-- Status codes: januskey.h JK_OK / JK_ERR_* (0..11), ffi/zig `Error` -------------------------------------------------------------------------------- -||| Initialize the library -||| Returns a handle to the library instance, or Nothing on failure +||| Every status libjanuskey can return. A closed sum: there is no +||| "unknown status" constructor, so a code the header does not define +||| decodes to Nothing and must be handled as a contract violation. +public export +data Status : Type where + Ok : Status -- JK_OK 0 + ErrNotInitialized : Status -- JK_ERR_NOT_INITIALIZED 1 + ErrInvalidPath : Status -- JK_ERR_INVALID_PATH 2 + ErrIo : Status -- JK_ERR_IO 3 + ErrCrypto : Status -- JK_ERR_CRYPTO 4 + ErrTxNotActive : Status -- JK_ERR_TX_NOT_ACTIVE 5 + ErrTxConflict : Status -- JK_ERR_TX_CONFLICT 6 + ErrKeyNotFound : Status -- JK_ERR_KEY_NOT_FOUND 7 + ErrKeyRevoked : Status -- JK_ERR_KEY_REVOKED 8 + ErrObliteration : Status -- JK_ERR_OBLITERATION 9 + ErrAttestation : Status -- JK_ERR_ATTESTATION 10 + ErrBufferTooSmall : Status -- JK_ERR_BUFFER_TOO_SMALL 11 + +||| Wire value of a status (januskey.h). +public export +statusCode : Status -> Nat +statusCode Ok = 0 +statusCode ErrNotInitialized = 1 +statusCode ErrInvalidPath = 2 +statusCode ErrIo = 3 +statusCode ErrCrypto = 4 +statusCode ErrTxNotActive = 5 +statusCode ErrTxConflict = 6 +statusCode ErrKeyNotFound = 7 +statusCode ErrKeyRevoked = 8 +statusCode ErrObliteration = 9 +statusCode ErrAttestation = 10 +statusCode ErrBufferTooSmall = 11 + +||| Total decoder: every natural number decodes, to a status or to Nothing. +public export +statusFromCode : Nat -> Maybe Status +statusFromCode 0 = Just Ok +statusFromCode 1 = Just ErrNotInitialized +statusFromCode 2 = Just ErrInvalidPath +statusFromCode 3 = Just ErrIo +statusFromCode 4 = Just ErrCrypto +statusFromCode 5 = Just ErrTxNotActive +statusFromCode 6 = Just ErrTxConflict +statusFromCode 7 = Just ErrKeyNotFound +statusFromCode 8 = Just ErrKeyRevoked +statusFromCode 9 = Just ErrObliteration +statusFromCode 10 = Just ErrAttestation +statusFromCode 11 = Just ErrBufferTooSmall +statusFromCode _ = Nothing + +||| Round trip: decoding an encoded status gives it back. Checked by cases, +||| one `Refl` per constructor; a wrong table entry fails to typecheck. export -%foreign "C:januskey_init, libjanuskey" -prim__init : PrimIO Bits64 - -||| Safe wrapper for library initialization +statusRoundTrip : (s : Status) -> statusFromCode (statusCode s) = Just s +statusRoundTrip Ok = Refl +statusRoundTrip ErrNotInitialized = Refl +statusRoundTrip ErrInvalidPath = Refl +statusRoundTrip ErrIo = Refl +statusRoundTrip ErrCrypto = Refl +statusRoundTrip ErrTxNotActive = Refl +statusRoundTrip ErrTxConflict = Refl +statusRoundTrip ErrKeyNotFound = Refl +statusRoundTrip ErrKeyRevoked = Refl +statusRoundTrip ErrObliteration = Refl +statusRoundTrip ErrAttestation = Refl +statusRoundTrip ErrBufferTooSmall = Refl + +||| Codes are injective: two statuses with the same wire value are the same +||| status. Follows from the round trip, so it cannot drift from the table. export -init : IO (Maybe Handle) -init = do - ptr <- primIO prim__init - pure (createHandle ptr) +statusCodeInjective : (s, t : Status) -> statusCode s = statusCode t -> s = t +statusCodeInjective s t prf = + injective (trans (sym (statusRoundTrip s)) + (trans (cong statusFromCode prf) (statusRoundTrip t))) + +||| The C `int` seen at the boundary. Negative values and values above 11 +||| decode to Nothing: the caller must treat them as a broken contract, never +||| as success. +public export +statusFromInt : Int -> Maybe Status +statusFromInt x = if x < 0 then Nothing else statusFromCode (cast x) + +-------------------------------------------------------------------------------- +-- Operation kinds and algorithms: januskey.h enums, in Types.idr's order +-------------------------------------------------------------------------------- + +||| jk_op_kind_t. The order is Types.idr's constructor order, which is the +||| header's enum order; the round trip below is what pins that. +public export +opKindCode : OpKind -> Nat +opKindCode Copy = 0 +opKindCode Move = 1 +opKindCode Delete = 2 +opKindCode Modify = 3 +opKindCode Obliterate = 4 +opKindCode KeyGen = 5 +opKindCode KeyRotate = 6 +opKindCode KeyRevoke = 7 + +public export +opKindFromCode : Nat -> Maybe OpKind +opKindFromCode 0 = Just Copy +opKindFromCode 1 = Just Move +opKindFromCode 2 = Just Delete +opKindFromCode 3 = Just Modify +opKindFromCode 4 = Just Obliterate +opKindFromCode 5 = Just KeyGen +opKindFromCode 6 = Just KeyRotate +opKindFromCode 7 = Just KeyRevoke +opKindFromCode _ = Nothing -||| Clean up library resources export -%foreign "C:januskey_free, libjanuskey" -prim__free : Bits64 -> PrimIO () +opKindRoundTrip : (k : OpKind) -> opKindFromCode (opKindCode k) = Just k +opKindRoundTrip Copy = Refl +opKindRoundTrip Move = Refl +opKindRoundTrip Delete = Refl +opKindRoundTrip Modify = Refl +opKindRoundTrip Obliterate = Refl +opKindRoundTrip KeyGen = Refl +opKindRoundTrip KeyRotate = Refl +opKindRoundTrip KeyRevoke = Refl + +||| jk_algorithm_t. +public export +algorithmCode : KeyAlgorithm -> Nat +algorithmCode AES256GCM = 0 +algorithmCode ChaCha20 = 1 +algorithmCode Ed25519 = 2 +algorithmCode X25519 = 3 +algorithmCode Argon2id = 4 + +public export +algorithmFromCode : Nat -> Maybe KeyAlgorithm +algorithmFromCode 0 = Just AES256GCM +algorithmFromCode 1 = Just ChaCha20 +algorithmFromCode 2 = Just Ed25519 +algorithmFromCode 3 = Just X25519 +algorithmFromCode 4 = Just Argon2id +algorithmFromCode _ = Nothing -||| Safe wrapper for cleanup export -free : Handle -> IO () -free h = primIO (prim__free (handlePtr h)) +algorithmRoundTrip : (a : KeyAlgorithm) -> algorithmFromCode (algorithmCode a) = Just a +algorithmRoundTrip AES256GCM = Refl +algorithmRoundTrip ChaCha20 = Refl +algorithmRoundTrip Ed25519 = Refl +algorithmRoundTrip X25519 = Refl +algorithmRoundTrip Argon2id = Refl -------------------------------------------------------------------------------- --- Core Operations +-- Opaque handles: jk_handle_t and jk_tx_t are `void*` -------------------------------------------------------------------------------- -||| Example operation: process data -export -%foreign "C:januskey_process, libjanuskey" -prim__process : Bits64 -> Bits32 -> PrimIO Bits32 +||| Library-handle lifecycle state. +public export +data LibState = Open | Closed + +||| A library instance handle (jk_handle_t) indexed by its state. Operations +||| take an Open handle unrestricted; `closeOnce` takes it at multiplicity 1 +||| and returns the Closed witness, so in any context that holds the handle +||| linearly a second close is a type error (tests/reject-idris/DoubleClose.idr) +||| and forgetting to close, where a Closed witness is demanded, is too. +||| Scope, stated plainly: linearity is a property of the binding. A handle +||| bound by an IO `<-` is unrestricted; the discipline holds for handles +||| passed as `(1 h : LibHandle Open)` parameters, which is how callers that +||| want the guarantee must receive it. Plain IO's bind is not linear, so such +||| a handle cannot be closed inside IO do-notation at all; sequencing linear +||| steps needs a linear monad (Control.Linear.LIO), which is not used here. +public export +data LibHandle : LibState -> Type where + Opened : (ptr : AnyPtr) -> LibHandle Open + Shut : LibHandle Closed -||| Safe wrapper with error handling -export -process : Handle -> Bits32 -> IO (Either Result Bits32) -process h input = do - result <- primIO (prim__process (handlePtr h) input) - pure $ case result of - 0 => Left Error - n => Right n +||| The raw pointer of an open handle (wire form for the %foreign calls). +public export +libPtr : LibHandle Open -> AnyPtr +libPtr (Opened p) = p + +||| A transaction token (jk_tx_t). +public export +record TxToken where + constructor MkTxToken + ptr : AnyPtr -------------------------------------------------------------------------------- --- String Operations +-- Foreign declarations: one per exported symbol, C types as in januskey.h -------------------------------------------------------------------------------- -||| Convert C string to Idris String +-- Library lifecycle -------------------------------------------------------- + +||| int jk_init(const char* path, jk_handle_t* out_handle) export -%foreign "support:idris2_getString, libidris2_support" -prim__getString : Bits64 -> String +%foreign "C:jk_init, libjanuskey" +prim__jk_init : String -> AnyPtr -> PrimIO Int -||| Free C string +||| int jk_open(const char* path, jk_handle_t* out_handle) export -%foreign "C:januskey_free_string, libjanuskey" -prim__freeString : Bits64 -> PrimIO () +%foreign "C:jk_open, libjanuskey" +prim__jk_open : String -> AnyPtr -> PrimIO Int -||| Get string result from library +||| void jk_close(jk_handle_t handle) export -%foreign "C:januskey_get_string, libjanuskey" -prim__getResult : Bits64 -> PrimIO Bits64 +%foreign "C:jk_close, libjanuskey" +prim__jk_close : AnyPtr -> PrimIO () + +-- File operations ---------------------------------------------------------- -||| Safe string getter +||| int jk_execute(jk_handle_t handle, jk_op_kind_t op, const char* src, const char* dst) export -getString : Handle -> IO (Maybe String) -getString h = do - ptr <- primIO (prim__getResult (handlePtr h)) - if ptr == 0 - then pure Nothing - else do - let str = prim__getString ptr - primIO (prim__freeString ptr) - pure (Just str) +%foreign "C:jk_execute, libjanuskey" +prim__jk_execute : AnyPtr -> Int -> String -> String -> PrimIO Int --------------------------------------------------------------------------------- --- Array/Buffer Operations --------------------------------------------------------------------------------- +||| int jk_undo(jk_handle_t handle) +export +%foreign "C:jk_undo, libjanuskey" +prim__jk_undo : AnyPtr -> PrimIO Int -||| Process array data -export -%foreign "C:januskey_process_array, libjanuskey" -prim__processArray : Bits64 -> Bits64 -> Bits32 -> PrimIO Bits32 - -||| Safe array processor -export -processArray : Handle -> (buffer : Bits64) -> (len : Bits32) -> IO (Either Result ()) -processArray h buf len = do - result <- primIO (prim__processArray (handlePtr h) buf len) - pure $ case resultFromInt result of - Just Ok => Right () - Just err => Left err - Nothing => Left Error - where - resultFromInt : Bits32 -> Maybe Result - resultFromInt 0 = Just Ok - resultFromInt 1 = Just Error - resultFromInt 2 = Just InvalidParam - resultFromInt 3 = Just OutOfMemory - resultFromInt 4 = Just NullPointer - resultFromInt _ = Nothing +||| int jk_obliterate(jk_handle_t handle, const char* path, jk_oblit_proof_t* out_proof) +||| out_proof is a caller-owned cell of oblitProofSize bytes (Layout.idr: 112). +export +%foreign "C:jk_obliterate, libjanuskey" +prim__jk_obliterate : AnyPtr -> String -> AnyPtr -> PrimIO Int --------------------------------------------------------------------------------- --- Error Handling --------------------------------------------------------------------------------- +-- Key management ----------------------------------------------------------- -||| Get last error message +||| int jk_generate_key(jk_handle_t handle, jk_algorithm_t algo, const char* passphrase, jk_key_id_t* out_id) export -%foreign "C:januskey_last_error, libjanuskey" -prim__lastError : PrimIO Bits64 +%foreign "C:jk_generate_key, libjanuskey" +prim__jk_generate_key : AnyPtr -> Int -> String -> AnyPtr -> PrimIO Int -||| Retrieve last error as string +||| int jk_rotate_key(jk_handle_t handle, const jk_key_id_t* old_id, const char* new_passphrase, jk_key_id_t* out_new_id) export -lastError : IO (Maybe String) -lastError = do - ptr <- primIO prim__lastError - if ptr == 0 - then pure Nothing - else pure (Just (prim__getString ptr)) +%foreign "C:jk_rotate_key, libjanuskey" +prim__jk_rotate_key : AnyPtr -> AnyPtr -> String -> AnyPtr -> PrimIO Int -||| Get error description for result code +||| int jk_revoke_key(jk_handle_t handle, const jk_key_id_t* key_id) export -errorDescription : Result -> String -errorDescription Ok = "Success" -errorDescription Error = "Generic error" -errorDescription InvalidParam = "Invalid parameter" -errorDescription OutOfMemory = "Out of memory" -errorDescription NullPointer = "Null pointer" +%foreign "C:jk_revoke_key, libjanuskey" +prim__jk_revoke_key : AnyPtr -> AnyPtr -> PrimIO Int --------------------------------------------------------------------------------- --- Version Information --------------------------------------------------------------------------------- +-- Transactions ------------------------------------------------------------- -||| Get library version +||| int jk_tx_begin(jk_handle_t handle, jk_tx_t* out_tx) export -%foreign "C:januskey_version, libjanuskey" -prim__version : PrimIO Bits64 +%foreign "C:jk_tx_begin, libjanuskey" +prim__jk_tx_begin : AnyPtr -> AnyPtr -> PrimIO Int -||| Get version as string +||| int jk_tx_commit(jk_handle_t handle, jk_tx_t tx) export -version : IO String -version = do - ptr <- primIO prim__version - pure (prim__getString ptr) +%foreign "C:jk_tx_commit, libjanuskey" +prim__jk_tx_commit : AnyPtr -> AnyPtr -> PrimIO Int -||| Get library build info +||| int jk_tx_rollback(jk_handle_t handle, jk_tx_t tx) export -%foreign "C:januskey_build_info, libjanuskey" -prim__buildInfo : PrimIO Bits64 +%foreign "C:jk_tx_rollback, libjanuskey" +prim__jk_tx_rollback : AnyPtr -> AnyPtr -> PrimIO Int -||| Get build information +-- Version -------------------------------------------------------------------- + +||| const char* jk_version(void) export -buildInfo : IO String -buildInfo = do - ptr <- primIO prim__buildInfo - pure (prim__getString ptr) +%foreign "C:jk_version, libjanuskey" +prim__jk_version : PrimIO String -------------------------------------------------------------------------------- --- Callback Support +-- Typed wrappers. Each returns `Either Int Status`: Right for a code the +-- header defines, Left carrying the raw int for one it does not. Nothing is +-- ever read as success by default. -------------------------------------------------------------------------------- -||| Callback function type (C ABI) +||| Decode a raw status; keep the raw value on failure so the caller can log it. public export -Callback : Type -Callback = Bits64 -> Bits32 -> Bits32 +decodeStatus : Int -> Either Int Status +decodeStatus x = maybe (Left x) Right (statusFromInt x) -||| Register a callback +||| Destroy a handle at most once: consumes it (multiplicity 1) and returns +||| the Closed witness. export -%foreign "C:januskey_register_callback, libjanuskey" -prim__registerCallback : Bits64 -> AnyPtr -> PrimIO Bits32 +closeOnce : (1 h : LibHandle Open) -> IO (LibHandle Closed) +closeOnce (Opened p) = do + primIO (prim__jk_close p) + pure Shut -||| Safe callback registration export -registerCallback : Handle -> Callback -> IO (Either Result ()) -registerCallback h cb = do - result <- primIO (prim__registerCallback (handlePtr h) (cast cb)) - pure $ case resultFromInt result of - Just Ok => Right () - Just err => Left err - Nothing => Left Error - where - resultFromInt : Bits32 -> Maybe Result - resultFromInt 0 = Just Ok - resultFromInt _ = Just Error +undo : LibHandle Open -> IO (Either Int Status) +undo h = map decodeStatus (primIO (prim__jk_undo (libPtr h))) --------------------------------------------------------------------------------- --- Utility Functions --------------------------------------------------------------------------------- +||| Execute a file operation. The op kind crosses the boundary as its +||| header enum value (opKindCode), so an OpKind that Zig does not know is +||| unrepresentable here rather than an invalid int there. +export +execute : LibHandle Open -> OpKind -> (src : String) -> (dst : String) -> IO (Either Int Status) +execute h k src dst = + map decodeStatus (primIO (prim__jk_execute (libPtr h) (cast (opKindCode k)) src dst)) + +||| Obliterate `path`, writing the proof into a caller-owned 112-byte cell. +export +obliterate : LibHandle Open -> (path : String) -> (outProof : AnyPtr) -> IO (Either Int Status) +obliterate h path cell = map decodeStatus (primIO (prim__jk_obliterate (libPtr h) path cell)) + +export +generateKey : LibHandle Open -> KeyAlgorithm -> (passphrase : String) -> (outId : AnyPtr) -> IO (Either Int Status) +generateKey h a pass cell = + map decodeStatus (primIO (prim__jk_generate_key (libPtr h) (cast (algorithmCode a)) pass cell)) + +export +rotateKey : LibHandle Open -> (oldId : AnyPtr) -> (newPassphrase : String) -> (outNewId : AnyPtr) -> IO (Either Int Status) +rotateKey h old pass cell = + map decodeStatus (primIO (prim__jk_rotate_key (libPtr h) old pass cell)) + +export +revokeKey : LibHandle Open -> (keyId : AnyPtr) -> IO (Either Int Status) +revokeKey h kid = map decodeStatus (primIO (prim__jk_revoke_key (libPtr h) kid)) -||| Check if library is initialized export -%foreign "C:januskey_is_initialized, libjanuskey" -prim__isInitialized : Bits64 -> PrimIO Bits32 +txCommit : LibHandle Open -> TxToken -> IO (Either Int Status) +txCommit h t = map decodeStatus (primIO (prim__jk_tx_commit (libPtr h) t.ptr)) -||| Check initialization status export -isInitialized : Handle -> IO Bool -isInitialized h = do - result <- primIO (prim__isInitialized (handlePtr h)) - pure (result /= 0) +txRollback : LibHandle Open -> TxToken -> IO (Either Int Status) +txRollback h t = map decodeStatus (primIO (prim__jk_tx_rollback (libPtr h) t.ptr)) + +export +version : IO String +version = primIO prim__jk_version diff --git a/src/abi/JanusKey/ABI/Layout.idr b/src/abi/JanusKey/ABI/Layout.idr index 5a69502..6cb171c 100644 --- a/src/abi/JanusKey/ABI/Layout.idr +++ b/src/abi/JanusKey/ABI/Layout.idr @@ -10,6 +10,8 @@ import JanusKey.ABI.Types import Data.Vect import Data.Fin import Data.So +import Data.List +import Data.List.Elem %default total @@ -43,25 +45,28 @@ oblitProofSize = MkSize 112 -- Alignment Proofs -- ============================================================ -||| Proof that a size is aligned to a boundary +||| Proof that a size is aligned to a boundary: size is a whole number of +||| boundaries. Stated as divisibility with an explicit quotient (`mod` on Nat +||| does not reduce at compile time, so `mod size boundary = 0` could never +||| be discharged by Refl). public export data Aligned : (size : Nat) -> (boundary : Nat) -> Type where - MkAligned : (prf : mod size boundary = 0) -> Aligned size boundary + MkAligned : {size, boundary : Nat} -> (k : Nat) -> (prf : size = k * boundary) -> Aligned size boundary ||| ContentHash is 8-byte aligned public export hashAligned : Aligned 32 8 -hashAligned = MkAligned Refl +hashAligned = MkAligned 4 Refl ||| KeyId is 8-byte aligned public export keyIdAligned : Aligned 16 8 -keyIdAligned = MkAligned Refl +keyIdAligned = MkAligned 2 Refl ||| ObliterationProof is 8-byte aligned public export oblitAligned : Aligned 112 8 -oblitAligned = MkAligned Refl +oblitAligned = MkAligned 14 Refl -- ============================================================ -- Endianness-Safe Serialization @@ -109,12 +114,27 @@ data IsCNO : ReversibleOp -> Type where MkCNO : ((s : FSState) -> inverse op (forward op s) = s) -> IsCNO op -||| Copy-then-delete is a CNO (move + unmove = identity) +||| Copy, on the state model: forward records (dst, h) at the head of +||| `files`; inverse removes exactly that head. This replaces the former +||| `copyDeleteCNO`, which claimed IsCNO for *any* op of kind Copy and had +||| no body (it never typechecked): that statement is false for an op whose +||| forward and inverse are arbitrary functions. public export -copyDeleteCNO : (src, dst : ValidPath) -> (h : ContentHash) - -> (op : ReversibleOp) - -> (prf : kind op = Copy) - -> IsCNO op +copyOp : (dst : ValidPath) -> (h : ContentHash) -> ReversibleOp +copyOp dst h = MkRevOp Copy + (\s => { files $= ((dst, h) ::) } s) + (\s => { files $= drop 1 } s) + +||| Copy-then-uncopy is a CNO in this model: a theorem, by cases on the state. +||| Scope: the model tracks (path, hash) pairs, keys and a counter, not file +||| contents, so this is a statement about the operation log, not about bytes. +copyCancels : (dst : ValidPath) -> (h : ContentHash) -> (s : FSState) + -> inverse (copyOp dst h) (forward (copyOp dst h) s) = s +copyCancels dst h (MkFSState fs ks n) = Refl + +public export +copyIsCNO : (dst : ValidPath) -> (h : ContentHash) -> IsCNO (copyOp dst h) +copyIsCNO dst h = MkCNO (copyCancels dst h) ||| Obliterate does NOT have a CNO inverse — this is intentional ||| The type system prevents constructing IsCNO for Obliterate @@ -142,12 +162,13 @@ data AllReversible : List OpKind -> Type where -> AllReversible ks -> AllReversible (k :: ks) -||| Proof: a committed transaction can be rolled back if all ops are reversible +||| A transaction containing an obliteration is not all-reversible, so it +||| cannot be rolled back by inversion. This replaces `canRollback`, which +||| returned its argument unchanged. public export -canRollback : AllReversible ops -> TxOps Active ops -> TxOps Active ops -canRollback NilReversible Empty = Empty -canRollback (ConsReversible notOblit rest) (Append txOps k) = - Append (canRollback rest txOps) k +obliterateNotReversible : AllReversible ops -> Elem Obliterate ops -> Void +obliterateNotReversible (ConsReversible notOblit _) Here = notOblit Refl +obliterateNotReversible (ConsReversible _ rest) (There later) = obliterateNotReversible rest later -- ============================================================ -- Key Derivation Safety @@ -171,11 +192,5 @@ public export defaultArgon2 : Argon2Params defaultArgon2 = MkArgon2 3 65536 4 32 Oh Oh Oh Oh -||| Proof: default parameters meet OWASP recommendations -public export -defaultMeetsOWASP : So (timeCost defaultArgon2 >= 3) -defaultMeetsOWASP = Oh - -public export -defaultMemoryOWASP : So (memoryCost defaultArgon2 >= 65536) -defaultMemoryOWASP = Oh +-- The bounds are the record's own fields (timeOk, memoryOk, parallelOk, +-- outputOk); `defaultArgon2` discharges them with Oh at the literals. diff --git a/src/abi/JanusKey/ABI/Proofs.idr b/src/abi/JanusKey/ABI/Proofs.idr index d58caaf..1a4af99 100644 --- a/src/abi/JanusKey/ABI/Proofs.idr +++ b/src/abi/JanusKey/ABI/Proofs.idr @@ -1,9 +1,10 @@ -- SPDX-License-Identifier: MPL-2.0 -- Copyright (c) Jonathan D.A. Jewell -- --- JanusKey ABI Proofs — Standalone formal verification module --- Proves correctness properties for all JanusKey operations --- No believe_me, no assert_total, no postulate — fully total +-- JanusKey ABI lemmas: CNO composition, transaction and attestation-chain +-- lemmas, tropical costs, status-code injectivity. What each states, and +-- what is not claimed, is the claims ledger in PROOF-NEEDS.adoc; the +-- bypass census over src/abi is tests/aspect/cross_cutting_test.sh. module JanusKey.ABI.Proofs @@ -21,52 +22,50 @@ import Data.Nat -- 1. CNO Composition Proofs -- ============================================================ -||| Sequential composition of CNOs is a CNO -||| If f;f⁻¹ = id and g;g⁻¹ = id, then (f;g);(g⁻¹;f⁻¹) = id +-- Sequential composition of reversible operations: forward runs f then g, +-- inverse runs g⁻¹ then f⁻¹. The composite keeps f's kind tag (ReversibleOp +-- has no "sequence" kind); nothing below depends on the tag. public export -cnoPairCompose : IsCNO op1 -> IsCNO op2 -> Type -cnoPairCompose _ _ = Unit -- The proof is structural: given two CNO witnesses, - -- their sequential composition is also a CNO by - -- associativity of function composition and the - -- individual inverse properties. +seqOp : (f, g : ReversibleOp) -> ReversibleOp +seqOp f g = MkRevOp (kind f) (\s => forward g (forward f s)) (\s => inverse f (inverse g s)) -||| The identity operation is trivially a CNO +-- Composition of CNOs is a CNO: (f;g);(g⁻¹;f⁻¹) = id. This is the theorem +-- the former `cnoPairCompose` (which returned Unit) claimed in a comment. public export -identityIsCNO : (s : FSState) -> s = s -identityIsCNO s = Refl +seqCNO : {f, g : ReversibleOp} -> IsCNO f -> IsCNO g -> IsCNO (seqOp f g) +seqCNO (MkCNO pf) (MkCNO pg) = + MkCNO (\s => trans (cong (inverse f) (pg (forward f s))) (pf s)) -- ============================================================ -- 2. Obliteration Completeness -- ============================================================ -||| Overwrite pass covers all bytes -||| For a file of size n, each pass writes exactly n bytes +-- Overwrite pass covers all bytes +-- For a file of size n, each pass writes exactly n bytes public export overwriteCoversAll : (fileSize : Nat) -> (pass : OverwritePassIdx) -> (bytesWritten : Nat) -> bytesWritten = fileSize -> So (bytesWritten >= fileSize) -overwriteCoversAll Z _ Z Refl = Oh -overwriteCoversAll (S k) _ (S k) Refl = Oh +overwriteCoversAll n _ _ Refl = gteRefl n + where + gteRefl : (m : Nat) -> So (m >= m) + gteRefl Z = Oh + gteRefl (S j) = gteRefl j -||| Three passes is the minimum for secure deletion -||| (DoD 5220.22-M standard requires 3 passes minimum) -public export -threePassMinimum : So (3 >= 3) -threePassMinimum = Oh - -||| After obliteration, content hash cannot be reversed to content -||| This is a consequence of SHA256 being a one-way function -public export -hashOneWay : ContentHash -> Type -hashOneWay h = Void -> Void -- Content cannot be recovered from hash alone +-- The three-pass minimum is carried by ObliterationProof itself: its +-- `passesValid : So (overwritePasses >= 3)` field cannot be filled otherwise +-- (the former `threePassMinimum : So (3 >= 3)` restated a literal). Hash +-- one-wayness is a cryptographic assumption, not a theorem of this module; +-- it is recorded in PROOF-NEEDS.adoc as external, and the former +-- `hashOneWay` (which returned `Void -> Void`) is gone. -- ============================================================ -- 3. Transaction Safety Proofs -- ============================================================ -||| A transaction cannot be committed twice -||| (Committed is a terminal state — no TxTransition from Committed) +-- A transaction cannot be committed twice +-- (Committed is a terminal state — no TxTransition from Committed) public export noDoubleCommit : TxTransition Committed s -> Void noDoubleCommit _ impossible @@ -107,28 +106,13 @@ txLifecycleComplete RolledBack _ = Right (\case _ impossible) -- 4. Key Derivation Correctness -- ============================================================ -||| Argon2 time cost is monotonic with security -||| Higher time cost → harder to brute force -public export -timeCostMonotonic : (a, b : Nat) -> So (a >= b) -> So (a >= b) -timeCostMonotonic a b prf = prf - -||| Memory cost of 64 MiB defeats GPU attacks -||| (GPUs have limited per-thread memory) -public export -memoryDefeatsGPU : So (65536 >= 65536) -memoryDefeatsGPU = Oh - -||| Output length of 32 bytes = 256 bits of key material -public export -outputIs256Bits : So (32 * 8 >= 256) -outputIs256Bits = Oh - -||| Default parameters exceed minimum requirements -public export -defaultExceedsMinimum : (p : Argon2Params) -> p = defaultArgon2 - -> (So (timeCost p >= 3), So (memoryCost p >= 65536)) -defaultExceedsMinimum _ Refl = (Oh, Oh) +||| Argon2 parameter bounds are carried by Layout.Argon2Params: a record can +||| only be built with proofs of timeCost >= 3, memoryCost >= 65536 KiB, +||| parallelism >= 1 and outputLen >= 32, and `defaultArgon2` supplies them. +||| The former `timeCostMonotonic` (returned its hypothesis), +||| `memoryDefeatsGPU` and `outputIs256Bits` (closed literals) and +||| `defaultExceedsMinimum` (restated the record fields) are gone; none was +||| a statement about key derivation. -- ============================================================ -- 5. Attestation Chain Integrity @@ -156,17 +140,18 @@ data ValidChain : List AttestEntry -> Type where public export chainNoGaps : ValidChain chain -> (i : Fin (length chain)) -> So (length chain > 0) -chainNoGaps (SingleEntry) FZ = Oh -chainNoGaps (ChainLink _ _) FZ = Oh +chainNoGaps EmptyChain i = absurd i +chainNoGaps SingleEntry _ = Oh +chainNoGaps (ChainLink _ _) _ = Oh -||| Tampering with any entry breaks the chain -||| If an attacker modifies entry i, the hash at i+1 won't match +||| Tampering breaks the chain: replace e1 by an entry whose hash differs and +||| the link from e2 cannot be re-established. This is the theorem the former +||| `tamperDetectable` (which returned Unit) claimed in a comment. public export -tamperDetectable : (chain : List AttestEntry) - -> ValidChain chain - -> Type -tamperDetectable _ _ = Unit -- Structural: any modification to entryHash - -- invalidates the next entry's prevHash check +tamperBreaksLink : ValidChain (e2 :: e1 :: rest) + -> Not (entryHash e1' = entryHash e1) + -> ValidChain (e2 :: e1' :: rest) -> Void +tamperBreaksLink (ChainLink p _) neq (ChainLink p' _) = neq (trans (sym p') p) -- ============================================================ -- 6. Effect Safety Proofs @@ -191,22 +176,18 @@ oblitNeedsEntropy = There (There (Here)) -- 7. Linearity Proofs -- ============================================================ -||| A linear file consumed by obliteration cannot be used again -||| (This is enforced by QTT multiplicities — included for documentation) -public export -linearFileConsumed : (1 f : LinearFile) -> (ObliterationProof, LinearFile -> Void) -linearFileConsumed f = (obliterateLinear f, \_ => ()) --- Note: after obliterateLinear consumes f with multiplicity 1, --- there is no remaining reference to construct a second use. +||| Linearity is carried by signatures, not restated here: `obliterateLinear` +||| and `zeroize` in Types.idr take their argument at multiplicity 1, so a +||| second use of the same value is a type error at the call site. (The +||| former `linearFileConsumed` claimed `LinearFile -> Void`, which is false — +||| LinearFile is inhabited — and was ill-typed.) -- ============================================================ -- 8. Tropical Cost Proofs -- ============================================================ -||| Copy is cheaper than obliteration for any file size > 0 -public export -copyCheaperThanOblit : (n : Nat) -> So (n > 0) -> So (3 * n > n) -copyCheaperThanOblit (S k) Oh = Oh +||| Obliteration cost dominates copy cost: see Types.oblitCostDominates +||| (LTE n (3 * n)); the strict form for n > 0 is not stated. ||| Sequential cost is additive (tropical multiplication) public export @@ -222,11 +203,9 @@ parallelCostMin a b = Refl -- 9. Epistemic Safety Proofs -- ============================================================ -||| After key revocation, adversary cannot use the key -||| (No constructor for Knows Adversary _ exists) -public export -revokedKeyUnusable : Knows Adversary KeyId -> Void -revokedKeyUnusable = adversaryCannotKnow +-- The former `revokedKeyUnusable` was `adversaryCannotKnow` at KeyId: it took +-- no revocation and said nothing about one, so it is gone. That an attacker +-- cannot use a revoked key is OPEN in the claims ledger (PROOF-NEEDS.adoc). ||| Auditor can see operations but not key material public export @@ -234,28 +213,18 @@ data AuditorView : Type where CanSeeOps : List OpKind -> AuditorView -- No constructor for seeing key bytes -||| System forgets old key material after rotation -public export -systemForgetsOldKey : KeyRotated old new -> Knows System KeyId -systemForgetsOldKey rot = systemKnowsNewKey rot --- Returns knowledge of NEW key only — old key is not in the result +||| "The system forgets the old key" is not expressible in the Knows model: +||| Knows has no negative form, so the former `systemForgetsOldKey` (which +||| returned knowledge of the new key and said nothing about the old) is gone. +||| Types.systemKnowsNewKey remains as the positive statement. -- ============================================================ -- 10. Error Code Proofs -- ============================================================ -||| Every operation returns exactly one error code +||| Status codes are a closed sum with a total decoder and an injective +||| encoding: Foreign.statusRoundTrip and Foreign.statusCodeInjective. +||| Re-exported here under the name the old (never-typechecking) proof used. public export -errorCodeDeterministic : (e1, e2 : CError) -> errorCode e1 = errorCode e2 -> e1 = e2 -errorCodeDeterministic JK_OK JK_OK Refl = Refl -errorCodeDeterministic JK_ERR_NOT_INITIALIZED JK_ERR_NOT_INITIALIZED Refl = Refl -errorCodeDeterministic JK_ERR_INVALID_PATH JK_ERR_INVALID_PATH Refl = Refl -errorCodeDeterministic JK_ERR_IO JK_ERR_IO Refl = Refl -errorCodeDeterministic JK_ERR_CRYPTO JK_ERR_CRYPTO Refl = Refl -errorCodeDeterministic JK_ERR_TX_NOT_ACTIVE JK_ERR_TX_NOT_ACTIVE Refl = Refl -errorCodeDeterministic JK_ERR_TX_CONFLICT JK_ERR_TX_CONFLICT Refl = Refl -errorCodeDeterministic JK_ERR_KEY_NOT_FOUND JK_ERR_KEY_NOT_FOUND Refl = Refl -errorCodeDeterministic JK_ERR_KEY_REVOKED JK_ERR_KEY_REVOKED Refl = Refl -errorCodeDeterministic JK_ERR_OBLITERATION JK_ERR_OBLITERATION Refl = Refl -errorCodeDeterministic JK_ERR_ATTESTATION JK_ERR_ATTESTATION Refl = Refl -errorCodeDeterministic JK_ERR_BUFFER_TOO_SMALL JK_ERR_BUFFER_TOO_SMALL Refl = Refl +errorCodeDeterministic : (e1, e2 : Status) -> statusCode e1 = statusCode e2 -> e1 = e2 +errorCodeDeterministic = statusCodeInjective diff --git a/src/abi/JanusKey/ABI/Types.idr b/src/abi/JanusKey/ABI/Types.idr index d734694..5037c5f 100644 --- a/src/abi/JanusKey/ABI/Types.idr +++ b/src/abi/JanusKey/ABI/Types.idr @@ -13,6 +13,8 @@ module JanusKey.ABI.Types import Data.Vect import Data.Fin import Data.So +import Data.String +import Data.Nat %default total @@ -161,25 +163,13 @@ data SizeMatch : (expected : Nat) -> (actual : Nat) -> Type where -- Return type of every operation is statically known -- ============================================================ -||| Type-level function: given an OpKind, what does it return? -public export -ResultOf : OpKind -> Type -ResultOf Copy = (ContentHash, FileMetadata) -ResultOf Move = (ContentHash, FileMetadata) -ResultOf Delete = ContentHash -ResultOf Modify = (ContentHash, ContentHash) -- old hash, new hash -ResultOf Obliterate = ObliterationProof -ResultOf KeyGen = KeyId -ResultOf KeyRotate = (KeyId, KeyId) -- old, new -ResultOf KeyRevoke = KeyId - ||| Key identifier — opaque, unique public export record KeyId where constructor MkKeyId uuid : Vect 16 Bits8 -||| Forward declaration for obliteration proof (defined in Layout.idr) +||| Obliteration proof record (wire form in Layout.idr: 112 bytes, 8-aligned) public export record ObliterationProof where constructor MkOblitProof @@ -189,6 +179,18 @@ record ObliterationProof where overwritePasses : Nat passesValid : So (overwritePasses >= 3) +||| Type-level function: given an OpKind, what does it return? +public export +ResultOf : OpKind -> Type +ResultOf Copy = (ContentHash, FileMetadata) +ResultOf Move = (ContentHash, FileMetadata) +ResultOf Delete = ContentHash +ResultOf Modify = (ContentHash, ContentHash) -- old hash, new hash +ResultOf Obliterate = ObliterationProof +ResultOf KeyGen = KeyId +ResultOf KeyRotate = (KeyId, KeyId) -- old, new +ResultOf KeyRevoke = KeyId + -- ============================================================ -- Level 7: Aliasing Safety -- Mutable references are exclusive — no aliased writes @@ -204,7 +206,7 @@ data ResourceState : Type where ||| A resource handle with exclusive access tracking public export data Handle : (state : ResourceState) -> Type -> Type where - MkHandle : (tag : Nat) -> (val : a) -> Handle Available a + MkHandle : (tag : Nat) -> (val : a) -> Handle st a ||| Acquire exclusive access — transitions Available -> Locked public export @@ -283,7 +285,7 @@ data TxTransition : TxState -> TxState -> Type where ||| A transaction with compile-time state tracking public export data Tx : TxState -> Type where - MkTx : (id : Nat) -> Tx Pending + MkTx : (id : Nat) -> Tx st ||| Begin a transaction — type-level state change public export @@ -313,7 +315,7 @@ rollbackTx (MkTx id) = MkTx id ||| Uses Idris2 multiplicities: (1 x : a) means x used exactly once public export data LinearFile : Type where - MkLinearFile : (1 _ : ValidPath) -> (1 _ : ContentHash) -> LinearFile + MkLinearFile : ValidPath -> ContentHash -> LinearFile ||| Consume a linear file by obliterating it — returns proof of destruction public export @@ -324,7 +326,7 @@ obliterateLinear (MkLinearFile path hash) = ||| Linear key material — must be zeroized after use public export data LinearKey : Type where - MkLinearKey : (1 _ : Vect n Bits8) -> (1 _ : KeyId) -> LinearKey + MkLinearKey : Vect n Bits8 -> KeyId -> LinearKey ||| Zeroize key material — consumes the linear key public export @@ -366,11 +368,11 @@ public export oblitCost : (fileSize : Nat) -> TropCost (3 * fileSize) oblitCost n = MkCost (3 * n) -||| Proof: obliteration is the most expensive file operation +||| Obliteration cost dominates copy cost: n <= 3 * n. (3 * n reduces to +||| n + (n + (n + 0)), so this is lteAddRight.) public export -oblitMostExpensive : (n : Nat) -> So (3 * n >= n) -oblitMostExpensive Z = Oh -oblitMostExpensive (S k) = Oh +oblitCostDominates : (n : Nat) -> LTE n (3 * n) +oblitCostDominates n = lteAddRight n -- ============================================================ -- Level 12: Epistemic Safety @@ -392,15 +394,15 @@ data Knows : Agent -> Type -> Type where SystemKnows : (val : a) -> Knows System a AuditorKnows : (val : a) -> Knows Auditor a -||| After obliteration, adversary cannot know content -||| (There is no constructor `AdversaryKnows` — this is an impossibility proof) +||| Marker that the content with this hash has been obliterated. public export data PostObliteration : ContentHash -> Type where Obliterated : (hash : ContentHash) -> PostObliteration hash -||| Proof: adversary cannot recover obliterated content -||| No term of type `Knows Adversary content -> PostObliteration hash -> Void` -||| can be constructed because `Knows Adversary content` is uninhabited +||| `Knows Adversary a` is uninhabited because `Knows` has no Adversary +||| constructor: a property of this model, not a security proof. What a real +||| attacker can recover after obliteration is OPEN in the claims ledger +||| (PROOF-NEEDS.adoc). public export adversaryCannotKnow : Knows Adversary a -> Void adversaryCannotKnow _ impossible @@ -410,7 +412,8 @@ public export data KeyRotated : KeyId -> KeyId -> Type where Rotated : (old : KeyId) -> (new : KeyId) -> KeyRotated old new -||| System knows the new key but not the old after rotation +||| After rotation the system knows the new key. ("And not the old one" is +||| not stated: `Knows` has no negative form.) public export systemKnowsNewKey : KeyRotated old new -> Knows System KeyId systemKnowsNewKey (Rotated _ new) = SystemKnows new diff --git a/tests/aspect/cross_cutting_test.sh b/tests/aspect/cross_cutting_test.sh index 1324d80..978ae0d 100755 --- a/tests/aspect/cross_cutting_test.sh +++ b/tests/aspect/cross_cutting_test.sh @@ -45,6 +45,12 @@ check "No believe_me in proofs" "! grep -rh 'believe_me' '${JK_DIR}/src/abi/' 2> check "No assert_total in proofs" "! grep -rh 'assert_total' '${JK_DIR}/src/abi/' 2>/dev/null | grep -v '^\s*--' | grep -q ." check "No postulate in proofs" "! grep -rq '^postulate' '${JK_DIR}/src/abi/' 2>/dev/null" check "No sorry in proofs" "! grep -rh 'sorry' '${JK_DIR}/src/abi/' 2>/dev/null | grep -v '^\s*--' | grep -q ." +# The rest of the census PROOF-NEEDS.adoc cites: each of these lets a +# definition typecheck without being proved. Comment and docstring lines are +# stripped first. +check "No assert_smaller in proofs" "! grep -rh 'assert_smaller' '${JK_DIR}/src/abi/' 2>/dev/null | grep -vE '^\s*(--|\|\|\|)' | grep -q ." +check "No partial in proofs" "! grep -rhw 'partial' '${JK_DIR}/src/abi/' 2>/dev/null | grep -vE '^\s*(--|\|\|\|)' | grep -q ." +check "No holes in proofs" "! grep -rhE '\?[A-Za-z_][A-Za-z0-9_]*' '${JK_DIR}/src/abi/' 2>/dev/null | grep -vE '^\s*(--|\|\|\|)' | grep -q ." # NB: exclude the '#![forbid(unsafe_code)]' attribute (which BANS unsafe) # and '//' comment lines from the unsafe check. check "No unsafe in reversible-core" "! grep -rh 'unsafe' '${JK_DIR}/crates/reversible-core/src/' 2>/dev/null | grep -v 'forbid(unsafe_code)' | grep -v '^\s*//' | grep -q ." @@ -63,7 +69,7 @@ echo "--- Formal Proofs ---" check "Types.idr exists (L1-L12)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Types.idr' ]" check "Layout.idr exists (CNO)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Layout.idr' ]" check "Foreign.idr exists (FFI)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Foreign.idr' ]" -check "Proofs.idr exists (30+ proofs)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Proofs.idr' ]" +check "Proofs.idr exists" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Proofs.idr' ]" check "C header present (mirrors Foreign.idr)" "[ -f '${JK_DIR}/ffi/zig/include/januskey.h' ]" # --- Build --- diff --git a/tests/reject-idris/DoubleClose.idr b/tests/reject-idris/DoubleClose.idr new file mode 100644 index 0000000..bfde091 --- /dev/null +++ b/tests/reject-idris/DoubleClose.idr @@ -0,0 +1,18 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection: closing a library handle twice. `closeOnce` takes the +-- handle at multiplicity 1, so two closes of one linear handle are refused +-- with a use count of 2. The two closes sit in a linear pair (`#`): plain IO +-- do-notation would not test this, because IO's bind is not linear and even +-- a single close there is refused ("non-linear context"). A single close, +-- `closeOnce h` or `closeOnce h # pure ()`, typechecks. If this file ever +-- typechecks, the destroy-at-most-once obligation has been lost. +-- expect: There are 2 uses of linear name h +module JanusKey.ABI.Reject.DoubleClose + +import JanusKey.ABI.Foreign + +%default total + +twice : (1 h : LibHandle Open) -> LPair (IO (LibHandle Closed)) (IO (LibHandle Closed)) +twice h = closeOnce h # closeOnce h diff --git a/tests/reject-idris/ForgottenClose.idr b/tests/reject-idris/ForgottenClose.idr new file mode 100644 index 0000000..f8ba0ae --- /dev/null +++ b/tests/reject-idris/ForgottenClose.idr @@ -0,0 +1,13 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection: a linear handle that is never closed. The parameter +-- has multiplicity 1 and is not used, which Idris2 refuses. +-- expect: There are 0 uses of linear name h +module JanusKey.ABI.Reject.ForgottenClose + +import JanusKey.ABI.Foreign + +%default total + +leak : (1 h : LibHandle Open) -> IO () +leak h = pure () diff --git a/tests/reject-idris/UnknownStatusIsOk.idr b/tests/reject-idris/UnknownStatusIsOk.idr new file mode 100644 index 0000000..c8101a2 --- /dev/null +++ b/tests/reject-idris/UnknownStatusIsOk.idr @@ -0,0 +1,13 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +-- Expected rejection: decoding a code the header does not define as success. +-- statusFromCode 12 is Nothing, so this equality cannot hold. +-- expect: Mismatch between: Just Ok and Nothing +module JanusKey.ABI.Reject.UnknownStatusIsOk + +import JanusKey.ABI.Foreign + +%default total + +twelveIsOk : statusFromCode 12 = Just Ok +twelveIsOk = Refl