diff --git a/.github/workflows/agda-proofs.yml b/.github/workflows/agda-proofs.yml new file mode 100644 index 0000000..2f53eef --- /dev/null +++ b/.github/workflows/agda-proofs.yml @@ -0,0 +1,32 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +name: Agda proofs +# DESIGNED until its first green run. Pattern: choreographic-types / +# residual-evidence-types (pinned Debian prover, sibling fetched by commit). +# Checks verification/proofs/agda/Reversibility.agda under the kernel flags +# and refuses the fixtures under tests/reject-agda. Local run: just test-agda. +on: + push: + branches: [main] + pull_request: +permissions: + contents: read +jobs: + proofs: + name: Reversibility as a grade (Loss instance), expected rejections + runs-on: ubuntu-latest + # trixie-slim, resolved 2026-10-13; re-pin deliberately, like the prover below. + container: debian:trixie-slim@sha256:a29215f6a35e51e22adffa17f89e9d2ef06214e64a2bad10d765c46aea49f11f + steps: + - name: Install the pinned prover + run: | + apt-get update + apt-get install --no-install-recommends -y ca-certificates git agda-bin=2.6.4.3-1+b2 + - name: Checkout + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + - name: Verify the checked Agda version + run: test "$(agda --version)" = 'Agda version 2.6.4.3' + - name: Proofs, sibling pin, expected rejections + run: bash scripts/check-agda.sh 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/.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..737427b 100644 --- a/Justfile +++ b/Justfile @@ -88,13 +88,25 @@ test-contracts: done; \ fi +# Agda kernel proofs (verification/proofs/agda) against the pinned resource-algebra. +test-agda: + bash scripts/check-agda.sh + +# Idris2 ABI <-> januskey.h <-> ffi/zig agreement (sizes, status codes, enums, symbols); no compiler needed. +abi-layout-check: + bash scripts/check-abi-layout.sh + +# Expected-rejection fixtures for the Idris2 ABI (double close, forgotten close, unknown status). +test-proofs-reject: + bash scripts/check-idris-reject.sh + # One ABI tree: no symlink farm, one ipkg, one Foreign.idr, module names match paths. abi-tree-check: bash scripts/check-abi-tree.sh # Typecheck the Idris2 ABI package (src/abi/januskey-abi.ipkg). # Fails if idris2 is missing (set ALLOW_NO_IDRIS=1 to skip) or any module fails. -test-proofs: abi-tree-check +test-proofs: abi-tree-check abi-layout-check #!/usr/bin/env bash set -euo pipefail echo "=== Proof Regression ===" 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-agda.sh b/scripts/check-agda.sh new file mode 100755 index 0000000..73e9d92 --- /dev/null +++ b/scripts/check-agda.sh @@ -0,0 +1,36 @@ +#!/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 +[ "${#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 + 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/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/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/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-agda/HiddenLoss.agda b/tests/reject-agda/HiddenLoss.agda new file mode 100644 index 0000000..a2097a7 --- /dev/null +++ b/tests/reject-agda/HiddenLoss.agda @@ -0,0 +1,20 @@ +{-# 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. +-- expect: 1 != 0 +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..ebf7526 --- /dev/null +++ b/tests/reject-agda/ReviveAfterObliterate.agda @@ -0,0 +1,22 @@ +{-# 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. +-- expect: inf != fin 0 +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/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 diff --git a/verification/proofs/agda/Reversibility.agda b/verification/proofs/agda/Reversibility.agda new file mode 100644 index 0000000..0d30206 --- /dev/null +++ b/verification/proofs/agda/Reversibility.agda @@ -0,0 +1,166 @@ +{-# 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, 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; +-- 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 (execute_then_undo_is_identity, cited above); + -- 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. +----------------------------------------------------------------------