From 4065f8ba71de521ea625d7e0a99e0a592e561f1d Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 00:17:41 +0000 Subject: [PATCH] chore(abi): remove the idrisiser tree (owner decision; it never typechecked) generated/idrisiser/ was the third Idris2 tree JNK-01 found: wrappers that the idrisiser tool generated from idrisiser/*.tsig per idrisiser.toml. Its module names were lowercase, so `idris2 --check` refused them ("Expected a capitalised identifier, got: key"), nothing in it was ever verified, and no ledger row depended on it. The owner decided to remove it rather than regenerate it. Removed: generated/idrisiser/ (6 files), idrisiser/*.tsig (3), and idrisiser.toml. generated/ is now empty, so it goes too. References updated: - scripts/check-abi-tree.sh: section 7 used to print a note when generated/idrisiser existed. It now fails if generated/idrisiser, idrisiser/ or idrisiser.toml comes back, like the retired src/idris-abi check, so a second ABI tree cannot return unnoticed. Negative control: `touch idrisiser.toml` -> FAIL. - .machine_readable/bot_directives/gitbot-fleet.a2ml: dropped from never-touch and its note (an entry removed, nothing added). - .machine_readable/contractiles/Mustfile.a2ml: no-dangerous-proof-escapes greps src/abi/ only. generated-code-in-generated is removed: its check was `test -d generated`, which fails once there is no generated code, and the stale contractile.just never ran it anyway. - README.adoc, PROOF-NEEDS.adoc: the idrisiser caveats now say it was removed and why. Left alone: CHANGELOG.adoc (generated from commits) and STATE.a2ml (A2ML is retired estate-wide; superseded by .deed, K9 and coordination.k9). Checks: check-abi-tree OK; aspect 32/32; dashboard-check OK with "119 tests measured, 8 PROVEN claims". Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9 --- .../bot_directives/gitbot-fleet.a2ml | 3 +- .machine_readable/contractiles/Mustfile.a2ml | 7 +- PROOF-NEEDS.adoc | 14 +- README.adoc | 2 +- generated/idrisiser/build.sh | 20 - .../Januskey/Verified/key_derivation.idr | 119 ----- .../Januskey/Verified/key_generation.idr | 421 ------------------ .../Verified/wrap_unwrap_round_trip.idr | 191 -------- generated/idrisiser/januskey_verified.ipkg | 8 - generated/idrisiser/zig/januskey_ffi.zig | 123 ----- idrisiser.toml | 117 ----- idrisiser/key-derivation.tsig | 5 - idrisiser/key-generation.tsig | 9 - idrisiser/wrap-unwrap.tsig | 6 - scripts/check-abi-tree.sh | 9 +- 15 files changed, 14 insertions(+), 1040 deletions(-) delete mode 100755 generated/idrisiser/build.sh delete mode 100644 generated/idrisiser/idris2/Januskey/Verified/key_derivation.idr delete mode 100644 generated/idrisiser/idris2/Januskey/Verified/key_generation.idr delete mode 100644 generated/idrisiser/idris2/Januskey/Verified/wrap_unwrap_round_trip.idr delete mode 100644 generated/idrisiser/januskey_verified.ipkg delete mode 100644 generated/idrisiser/zig/januskey_ffi.zig delete mode 100644 idrisiser.toml delete mode 100644 idrisiser/key-derivation.tsig delete mode 100644 idrisiser/key-generation.tsig delete mode 100644 idrisiser/wrap-unwrap.tsig diff --git a/.machine_readable/bot_directives/gitbot-fleet.a2ml b/.machine_readable/bot_directives/gitbot-fleet.a2ml index fc37beb..8b93b3c 100644 --- a/.machine_readable/bot_directives/gitbot-fleet.a2ml +++ b/.machine_readable/bot_directives/gitbot-fleet.a2ml @@ -22,12 +22,11 @@ ci-green-before-merge = true never-touch = [ ".claude/CLAUDE.md", "src/abi/", - "generated/idrisiser/", ".machine_readable/threat-model.a2ml", ".machine_readable/contractiles/Trustfile.a2ml", "LICENSE", ] -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)." +never-touch-notes = "src/abi/ (one tree: src/abi/januskey-abi.ipkg + JanusKey/ABI/*.idr, invariants in scripts/check-abi-tree.sh) is 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/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml index 9b3602a..b45050b 100644 --- a/.machine_readable/contractiles/Mustfile.a2ml +++ b/.machine_readable/contractiles/Mustfile.a2ml @@ -108,7 +108,7 @@ trust level: even maximal-trust agents cannot violate MUST constraints. ### no-dangerous-proof-escapes - description: No believe_me / assert_total in Idris2 proof code -- run: "! grep -rnE 'believe_me|assert_total' src/abi/ generated/idrisiser/ 2>/dev/null | head -1 | grep -q ." +- run: "! grep -rnE 'believe_me|assert_total' src/abi/ 2>/dev/null | head -1 | grep -q ." - severity: critical ### no-unsafe-without-comment @@ -150,11 +150,6 @@ trust level: even maximal-trust agents cannot violate MUST constraints. - 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 -- description: Generated code lives in generated/ only -- run: test -d generated -- severity: warning - ### tests-not-deleted - description: Test directories must not be deleted or emptied - run: test -d tests && test -d crates/januskey-cli/tests diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc index 6a51e9f..4ef422b 100644 --- a/PROOF-NEEDS.adoc +++ b/PROOF-NEEDS.adoc @@ -31,9 +31,9 @@ commits, not this one: `+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). +`+generated/idrisiser/+` was left outside the gate here; the owner decided +(2026-10-14) to remove it, with its `+idrisiser/*.tsig+` inputs and +`+idrisiser.toml+`. `+scripts/check-abi-tree.sh+` now fails if any of them returns. ==== Same day, three commits later: the package typechecks @@ -103,11 +103,9 @@ single tree; ABI bullet re-verified 2026-10-13._ 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 -lowercase. Despite the `+Verified/+` name, nothing there is currently -verified. +* **generated/idrisiser/**: removed 2026-10-14 (owner decision). It never +typechecked (lowercase generated module names), so nothing in it was +verified; no ledger row depended on it. * *Dangerous patterns*: *265* `+unwrap()+` calls across the Rust codebase. * *LOC*: ~12,200 (Rust) diff --git a/README.adoc b/README.adoc index 9a9ed63..d6feac8 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/` 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. +**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". (The former `generated/idrisiser/` tree, which never typechecked, was removed.) ==== [CAUTION] diff --git a/generated/idrisiser/build.sh b/generated/idrisiser/build.sh deleted file mode 100755 index 9e4c610..0000000 --- a/generated/idrisiser/build.sh +++ /dev/null @@ -1,20 +0,0 @@ -#!/usr/bin/env bash -# SPDX-License-Identifier: MPL-2.0 -# Auto-generated by idrisiser — build script for: januskey - -set -euo pipefail - -echo "=== idrisiser Build: januskey ===" - -echo "[1/3] Compiling Idris2 proofs..." -idris2 --build januskey_verified.ipkg --codegen chez - -echo "[2/3] Compiling Zig FFI bridge..." -zig build-obj -O ReleaseFast zig/januskey_ffi.zig -femit-bin=januskey_ffi.o - -echo "[3/3] Linking..." -# Link the Idris2 runtime + Zig FFI into a shared library -# zig build-lib -O ReleaseFast januskey_ffi.o -o libjanuskey_verified - -echo "=== Build complete ===" -echo "Idris2 proofs compiled and verified." diff --git a/generated/idrisiser/idris2/Januskey/Verified/key_derivation.idr b/generated/idrisiser/idris2/Januskey/Verified/key_derivation.idr deleted file mode 100644 index c18fa1e..0000000 --- a/generated/idrisiser/idris2/Januskey/Verified/key_derivation.idr +++ /dev/null @@ -1,119 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- Auto-generated by idrisiser — do not edit manually. --- Interface: key-derivation (type-sig) --- Source: idrisiser/key-derivation.tsig --- Regenerate with: idrisiser generate - -||| Formally verified wrapper for interface: key-derivation -||| -||| This module provides dependent-type proofs that: -||| - All functions are total (cover all inputs, terminate) -||| - Preconditions are checked before every call -||| - Postconditions hold after every call -||| - Invariants are preserved across all operations - -module Januskey.Verified.key_derivation - -import Data.So -import Data.Vect -import Data.Nat -import Linear -- quantitative type theory - -%default total - --- ================================================================ --- Contract Types --- ================================================================ - -||| Result of calling `derive_kek` -public export -data derive_kekResult : Type where - derive_kekOk : Result SecretKey KeyError -> derive_kekResult - derive_kekErr : String -> derive_kekResult - -||| Parameters for `derive_kek` -public export -record derive_kekParams where - constructor Mkderive_kekParams - arg0 : String - arg1 : Bytes 16 - -||| Preconditions for `derive_kek` -public export -derive_kekPre : derive_kekParams -> Bool -derive_kekPre params = - -- passphrase is a non-empty UTF-8 string - -- salt is exactly SALT_LENGTH (16) bytes - -- Argon2id parameters satisfy OWASP minimum: memory >= 64MB, iterations >= 3, parallelism >= 4 - True -- precondition witnesses generated here - -||| Postconditions for `derive_kek` -public export -derive_kekPost : Result SecretKey KeyError -> Bool -derive_kekPost result = - -- derive_kek returns Ok(kek) where kek.as_bytes().len() == 32 - -- derive_kek is deterministic: same (passphrase, salt) always produces the same kek bytes - -- derive_kek returns Err(CryptoError) only if Argon2 parameter construction fails - True -- postcondition witnesses generated here - --- ================================================================ --- Proof Obligations --- ================================================================ - -||| Proof that `derive_kek` is total (covers all inputs) -public export -data derive_kekTotal : Type where - Isderive_kekTotal : derive_kekTotal - -||| Proof that preconditions hold for given parameters -public export -data derive_kekPreSatisfied : (params : derive_kekParams) -> Type where - derive_kekPreOk : So (derive_kekPre params) -> derive_kekPreSatisfied params - -||| Proof that postconditions hold for a given result -public export -data derive_kekPostSatisfied : (result : Result SecretKey KeyError) -> Type where - derive_kekPostOk : So (derive_kekPost result) -> derive_kekPostSatisfied result - -||| Proof that serialise/deserialise round-trips for `derive_kek` results -public export -data derive_kekRoundTrip : Type where - derive_kekRoundTripOk : derive_kekRoundTrip - --- ================================================================ --- FFI Declarations (implemented in Zig bridge) --- ================================================================ - -export -%foreign "C:key_derivation_derive_kek, libkey_derivation_verified" -prim__derive_kek : Bits64 -> Bits64 -> PrimIO Bits32 - --- ================================================================ --- Safe Wrappers (enforce contracts at the type level) --- ================================================================ - -||| Safe wrapper for `derive_kek` with contract enforcement. -export -derive_kek : (params : derive_kekParams) -> {auto prf : derive_kekPreSatisfied params} -> IO (Either String Result SecretKey KeyError) -derive_kek params = do - rc <- primIO (prim__derive_kek params.arg0 params.arg1) - if rc == 0 - then pure (Right ()) - else pure (Left "Error in derive_kek") - --- ================================================================ --- Verification --- ================================================================ - -||| Witness that all proof obligations for this interface are met. -public export -data AllProofsComplete : Type where - MkAllProofsComplete : - derive_kekTotal -> - AllProofsComplete - -||| Verification entry point. -export -verify : IO () -verify = putStrLn "All proofs verified." diff --git a/generated/idrisiser/idris2/Januskey/Verified/key_generation.idr b/generated/idrisiser/idris2/Januskey/Verified/key_generation.idr deleted file mode 100644 index a44f219..0000000 --- a/generated/idrisiser/idris2/Januskey/Verified/key_generation.idr +++ /dev/null @@ -1,421 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- Auto-generated by idrisiser — do not edit manually. --- Interface: key-generation (type-sig) --- Source: idrisiser/key-generation.tsig --- Regenerate with: idrisiser generate - -||| Formally verified wrapper for interface: key-generation -||| -||| This module provides dependent-type proofs that: -||| - All functions are total (cover all inputs, terminate) -||| - Preconditions are checked before every call -||| - Postconditions hold after every call -||| - Invariants are preserved across all operations - -module Januskey.Verified.key_generation - -import Data.So -import Data.Vect -import Data.Nat -import Linear -- quantitative type theory - -%default total - --- ================================================================ --- Contract Types --- ================================================================ - -||| Result of calling `SecretKey.generate` -public export -data SecretKey.generateResult : Type where - SecretKey.generateOk : Result SecretKey KeyError -> SecretKey.generateResult - SecretKey.generateErr : String -> SecretKey.generateResult - -||| Parameters for `SecretKey.generate` -public export -record SecretKey.generateParams where - constructor MkSecretKey.generateParams - arg0 : () - -||| Preconditions for `SecretKey.generate` -public export -SecretKey.generatePre : SecretKey.generateParams -> Bool -SecretKey.generatePre params = - -- KeyManager is initialised (unlock or init called successfully before any key operation) - -- SecretKey.generate uses a cryptographically secure random number generator - -- KeyManager.rotate is called with a key ID that exists and is not already Revoked - -- KeyManager.revoke is called with a key ID that exists and is not already Revoked - -- KeyManager.retrieve is called with a key ID that is Active or Rotating - True -- precondition witnesses generated here - -||| Postconditions for `SecretKey.generate` -public export -SecretKey.generatePost : Result SecretKey KeyError -> Bool -SecretKey.generatePost result = - -- SecretKey.generate returns Ok(key) where key.as_bytes().len() == 32 - -- SecretKey.generate key material is not all-zero bytes - -- KeyManager.generate returns Ok(uuid) and the stored key has state == Active - -- KeyManager.rotate returns Ok(new_id) where new_id != old_id - -- KeyManager.rotate marks old key as Revoked - -- KeyManager.rotate new key has rotation_of == Some(old_id) - -- KeyManager.revoke sets key state to Revoked - -- KeyManager.retrieve returns Err(AlreadyRevoked) for any Revoked or Obliterated key - -- KeyManager.retrieve returns Ok(key) where key.as_bytes().len() == 32 - True -- postcondition witnesses generated here - -||| Result of calling `KeyManager.generate` -public export -data KeyManager.generateResult : Type where - KeyManager.generateOk : Result Uuid KeyError -> KeyManager.generateResult - KeyManager.generateErr : String -> KeyManager.generateResult - -||| Parameters for `KeyManager.generate` -public export -record KeyManager.generateParams where - constructor MkKeyManager.generateParams - arg0 : KeyManager - arg1 : KeyAlgorithm - arg2 : KeyPurpose - arg3 : Option String - arg4 : Option Nat - -||| Preconditions for `KeyManager.generate` -public export -KeyManager.generatePre : KeyManager.generateParams -> Bool -KeyManager.generatePre params = - -- KeyManager is initialised (unlock or init called successfully before any key operation) - -- SecretKey.generate uses a cryptographically secure random number generator - -- KeyManager.rotate is called with a key ID that exists and is not already Revoked - -- KeyManager.revoke is called with a key ID that exists and is not already Revoked - -- KeyManager.retrieve is called with a key ID that is Active or Rotating - True -- precondition witnesses generated here - -||| Postconditions for `KeyManager.generate` -public export -KeyManager.generatePost : Result Uuid KeyError -> Bool -KeyManager.generatePost result = - -- SecretKey.generate returns Ok(key) where key.as_bytes().len() == 32 - -- SecretKey.generate key material is not all-zero bytes - -- KeyManager.generate returns Ok(uuid) and the stored key has state == Active - -- KeyManager.rotate returns Ok(new_id) where new_id != old_id - -- KeyManager.rotate marks old key as Revoked - -- KeyManager.rotate new key has rotation_of == Some(old_id) - -- KeyManager.revoke sets key state to Revoked - -- KeyManager.retrieve returns Err(AlreadyRevoked) for any Revoked or Obliterated key - -- KeyManager.retrieve returns Ok(key) where key.as_bytes().len() == 32 - True -- postcondition witnesses generated here - -||| Result of calling `KeyManager.rotate` -public export -data KeyManager.rotateResult : Type where - KeyManager.rotateOk : Result Uuid KeyError -> KeyManager.rotateResult - KeyManager.rotateErr : String -> KeyManager.rotateResult - -||| Parameters for `KeyManager.rotate` -public export -record KeyManager.rotateParams where - constructor MkKeyManager.rotateParams - arg0 : KeyManager - arg1 : Uuid - -||| Preconditions for `KeyManager.rotate` -public export -KeyManager.rotatePre : KeyManager.rotateParams -> Bool -KeyManager.rotatePre params = - -- KeyManager is initialised (unlock or init called successfully before any key operation) - -- SecretKey.generate uses a cryptographically secure random number generator - -- KeyManager.rotate is called with a key ID that exists and is not already Revoked - -- KeyManager.revoke is called with a key ID that exists and is not already Revoked - -- KeyManager.retrieve is called with a key ID that is Active or Rotating - True -- precondition witnesses generated here - -||| Postconditions for `KeyManager.rotate` -public export -KeyManager.rotatePost : Result Uuid KeyError -> Bool -KeyManager.rotatePost result = - -- SecretKey.generate returns Ok(key) where key.as_bytes().len() == 32 - -- SecretKey.generate key material is not all-zero bytes - -- KeyManager.generate returns Ok(uuid) and the stored key has state == Active - -- KeyManager.rotate returns Ok(new_id) where new_id != old_id - -- KeyManager.rotate marks old key as Revoked - -- KeyManager.rotate new key has rotation_of == Some(old_id) - -- KeyManager.revoke sets key state to Revoked - -- KeyManager.retrieve returns Err(AlreadyRevoked) for any Revoked or Obliterated key - -- KeyManager.retrieve returns Ok(key) where key.as_bytes().len() == 32 - True -- postcondition witnesses generated here - -||| Result of calling `KeyManager.revoke` -public export -data KeyManager.revokeResult : Type where - KeyManager.revokeOk : Result () KeyError -> KeyManager.revokeResult - KeyManager.revokeErr : String -> KeyManager.revokeResult - -||| Parameters for `KeyManager.revoke` -public export -record KeyManager.revokeParams where - constructor MkKeyManager.revokeParams - arg0 : KeyManager - arg1 : Uuid - -||| Preconditions for `KeyManager.revoke` -public export -KeyManager.revokePre : KeyManager.revokeParams -> Bool -KeyManager.revokePre params = - -- KeyManager is initialised (unlock or init called successfully before any key operation) - -- SecretKey.generate uses a cryptographically secure random number generator - -- KeyManager.rotate is called with a key ID that exists and is not already Revoked - -- KeyManager.revoke is called with a key ID that exists and is not already Revoked - -- KeyManager.retrieve is called with a key ID that is Active or Rotating - True -- precondition witnesses generated here - -||| Postconditions for `KeyManager.revoke` -public export -KeyManager.revokePost : Result () KeyError -> Bool -KeyManager.revokePost result = - -- SecretKey.generate returns Ok(key) where key.as_bytes().len() == 32 - -- SecretKey.generate key material is not all-zero bytes - -- KeyManager.generate returns Ok(uuid) and the stored key has state == Active - -- KeyManager.rotate returns Ok(new_id) where new_id != old_id - -- KeyManager.rotate marks old key as Revoked - -- KeyManager.rotate new key has rotation_of == Some(old_id) - -- KeyManager.revoke sets key state to Revoked - -- KeyManager.retrieve returns Err(AlreadyRevoked) for any Revoked or Obliterated key - -- KeyManager.retrieve returns Ok(key) where key.as_bytes().len() == 32 - True -- postcondition witnesses generated here - -||| Result of calling `KeyManager.retrieve` -public export -data KeyManager.retrieveResult : Type where - KeyManager.retrieveOk : Result SecretKey KeyError -> KeyManager.retrieveResult - KeyManager.retrieveErr : String -> KeyManager.retrieveResult - -||| Parameters for `KeyManager.retrieve` -public export -record KeyManager.retrieveParams where - constructor MkKeyManager.retrieveParams - arg0 : KeyManager - arg1 : Uuid - -||| Preconditions for `KeyManager.retrieve` -public export -KeyManager.retrievePre : KeyManager.retrieveParams -> Bool -KeyManager.retrievePre params = - -- KeyManager is initialised (unlock or init called successfully before any key operation) - -- SecretKey.generate uses a cryptographically secure random number generator - -- KeyManager.rotate is called with a key ID that exists and is not already Revoked - -- KeyManager.revoke is called with a key ID that exists and is not already Revoked - -- KeyManager.retrieve is called with a key ID that is Active or Rotating - True -- precondition witnesses generated here - -||| Postconditions for `KeyManager.retrieve` -public export -KeyManager.retrievePost : Result SecretKey KeyError -> Bool -KeyManager.retrievePost result = - -- SecretKey.generate returns Ok(key) where key.as_bytes().len() == 32 - -- SecretKey.generate key material is not all-zero bytes - -- KeyManager.generate returns Ok(uuid) and the stored key has state == Active - -- KeyManager.rotate returns Ok(new_id) where new_id != old_id - -- KeyManager.rotate marks old key as Revoked - -- KeyManager.rotate new key has rotation_of == Some(old_id) - -- KeyManager.revoke sets key state to Revoked - -- KeyManager.retrieve returns Err(AlreadyRevoked) for any Revoked or Obliterated key - -- KeyManager.retrieve returns Ok(key) where key.as_bytes().len() == 32 - True -- postcondition witnesses generated here - --- ================================================================ --- Proof Obligations --- ================================================================ - -||| Proof that `SecretKey.generate` is total (covers all inputs) -public export -data SecretKey.generateTotal : Type where - IsSecretKey.generateTotal : SecretKey.generateTotal - -||| Proof that preconditions hold for given parameters -public export -data SecretKey.generatePreSatisfied : (params : SecretKey.generateParams) -> Type where - SecretKey.generatePreOk : So (SecretKey.generatePre params) -> SecretKey.generatePreSatisfied params - -||| Proof that postconditions hold for a given result -public export -data SecretKey.generatePostSatisfied : (result : Result SecretKey KeyError) -> Type where - SecretKey.generatePostOk : So (SecretKey.generatePost result) -> SecretKey.generatePostSatisfied result - -||| Proof that serialise/deserialise round-trips for `SecretKey.generate` results -public export -data SecretKey.generateRoundTrip : Type where - SecretKey.generateRoundTripOk : SecretKey.generateRoundTrip - -||| Proof that `KeyManager.generate` is total (covers all inputs) -public export -data KeyManager.generateTotal : Type where - IsKeyManager.generateTotal : KeyManager.generateTotal - -||| Proof that preconditions hold for given parameters -public export -data KeyManager.generatePreSatisfied : (params : KeyManager.generateParams) -> Type where - KeyManager.generatePreOk : So (KeyManager.generatePre params) -> KeyManager.generatePreSatisfied params - -||| Proof that postconditions hold for a given result -public export -data KeyManager.generatePostSatisfied : (result : Result Uuid KeyError) -> Type where - KeyManager.generatePostOk : So (KeyManager.generatePost result) -> KeyManager.generatePostSatisfied result - -||| Proof that serialise/deserialise round-trips for `KeyManager.generate` results -public export -data KeyManager.generateRoundTrip : Type where - KeyManager.generateRoundTripOk : KeyManager.generateRoundTrip - -||| Proof that `KeyManager.rotate` is total (covers all inputs) -public export -data KeyManager.rotateTotal : Type where - IsKeyManager.rotateTotal : KeyManager.rotateTotal - -||| Proof that preconditions hold for given parameters -public export -data KeyManager.rotatePreSatisfied : (params : KeyManager.rotateParams) -> Type where - KeyManager.rotatePreOk : So (KeyManager.rotatePre params) -> KeyManager.rotatePreSatisfied params - -||| Proof that postconditions hold for a given result -public export -data KeyManager.rotatePostSatisfied : (result : Result Uuid KeyError) -> Type where - KeyManager.rotatePostOk : So (KeyManager.rotatePost result) -> KeyManager.rotatePostSatisfied result - -||| Proof that serialise/deserialise round-trips for `KeyManager.rotate` results -public export -data KeyManager.rotateRoundTrip : Type where - KeyManager.rotateRoundTripOk : KeyManager.rotateRoundTrip - -||| Proof that `KeyManager.revoke` is total (covers all inputs) -public export -data KeyManager.revokeTotal : Type where - IsKeyManager.revokeTotal : KeyManager.revokeTotal - -||| Proof that preconditions hold for given parameters -public export -data KeyManager.revokePreSatisfied : (params : KeyManager.revokeParams) -> Type where - KeyManager.revokePreOk : So (KeyManager.revokePre params) -> KeyManager.revokePreSatisfied params - -||| Proof that postconditions hold for a given result -public export -data KeyManager.revokePostSatisfied : (result : Result () KeyError) -> Type where - KeyManager.revokePostOk : So (KeyManager.revokePost result) -> KeyManager.revokePostSatisfied result - -||| Proof that serialise/deserialise round-trips for `KeyManager.revoke` results -public export -data KeyManager.revokeRoundTrip : Type where - KeyManager.revokeRoundTripOk : KeyManager.revokeRoundTrip - -||| Proof that `KeyManager.retrieve` is total (covers all inputs) -public export -data KeyManager.retrieveTotal : Type where - IsKeyManager.retrieveTotal : KeyManager.retrieveTotal - -||| Proof that preconditions hold for given parameters -public export -data KeyManager.retrievePreSatisfied : (params : KeyManager.retrieveParams) -> Type where - KeyManager.retrievePreOk : So (KeyManager.retrievePre params) -> KeyManager.retrievePreSatisfied params - -||| Proof that postconditions hold for a given result -public export -data KeyManager.retrievePostSatisfied : (result : Result SecretKey KeyError) -> Type where - KeyManager.retrievePostOk : So (KeyManager.retrievePost result) -> KeyManager.retrievePostSatisfied result - -||| Proof that serialise/deserialise round-trips for `KeyManager.retrieve` results -public export -data KeyManager.retrieveRoundTrip : Type where - KeyManager.retrieveRoundTripOk : KeyManager.retrieveRoundTrip - --- ================================================================ --- FFI Declarations (implemented in Zig bridge) --- ================================================================ - -export -%foreign "C:key_generation_SecretKey.generate, libkey_generation_verified" -prim__SecretKey.generate : Bits64 -> PrimIO Bits32 - -export -%foreign "C:key_generation_KeyManager.generate, libkey_generation_verified" -prim__KeyManager.generate : Bits64 -> Bits64 -> Bits64 -> Bits64 -> Bits64 -> PrimIO Bits32 - -export -%foreign "C:key_generation_KeyManager.rotate, libkey_generation_verified" -prim__KeyManager.rotate : Bits64 -> Bits64 -> PrimIO Bits32 - -export -%foreign "C:key_generation_KeyManager.revoke, libkey_generation_verified" -prim__KeyManager.revoke : Bits64 -> Bits64 -> PrimIO Bits32 - -export -%foreign "C:key_generation_KeyManager.retrieve, libkey_generation_verified" -prim__KeyManager.retrieve : Bits64 -> Bits64 -> PrimIO Bits32 - --- ================================================================ --- Safe Wrappers (enforce contracts at the type level) --- ================================================================ - -||| Safe wrapper for `SecretKey.generate` with contract enforcement. -export -SecretKey.generate : (params : SecretKey.generateParams) -> {auto prf : SecretKey.generatePreSatisfied params} -> IO (Either String Result SecretKey KeyError) -SecretKey.generate params = do - rc <- primIO (prim__SecretKey.generate params.arg0) - if rc == 0 - then pure (Right ()) - else pure (Left "Error in SecretKey.generate") - -||| Safe wrapper for `KeyManager.generate` with contract enforcement. -export -KeyManager.generate : (params : KeyManager.generateParams) -> {auto prf : KeyManager.generatePreSatisfied params} -> IO (Either String Result Uuid KeyError) -KeyManager.generate params = do - rc <- primIO (prim__KeyManager.generate params.arg0 params.arg1 params.arg2 params.arg3 params.arg4) - if rc == 0 - then pure (Right ()) - else pure (Left "Error in KeyManager.generate") - -||| Safe wrapper for `KeyManager.rotate` with contract enforcement. -export -KeyManager.rotate : (params : KeyManager.rotateParams) -> {auto prf : KeyManager.rotatePreSatisfied params} -> IO (Either String Result Uuid KeyError) -KeyManager.rotate params = do - rc <- primIO (prim__KeyManager.rotate params.arg0 params.arg1) - if rc == 0 - then pure (Right ()) - else pure (Left "Error in KeyManager.rotate") - -||| Safe wrapper for `KeyManager.revoke` with contract enforcement. -export -KeyManager.revoke : (params : KeyManager.revokeParams) -> {auto prf : KeyManager.revokePreSatisfied params} -> IO (Either String Result () KeyError) -KeyManager.revoke params = do - rc <- primIO (prim__KeyManager.revoke params.arg0 params.arg1) - if rc == 0 - then pure (Right ()) - else pure (Left "Error in KeyManager.revoke") - -||| Safe wrapper for `KeyManager.retrieve` with contract enforcement. -export -KeyManager.retrieve : (params : KeyManager.retrieveParams) -> {auto prf : KeyManager.retrievePreSatisfied params} -> IO (Either String Result SecretKey KeyError) -KeyManager.retrieve params = do - rc <- primIO (prim__KeyManager.retrieve params.arg0 params.arg1) - if rc == 0 - then pure (Right ()) - else pure (Left "Error in KeyManager.retrieve") - --- ================================================================ --- Verification --- ================================================================ - -||| Witness that all proof obligations for this interface are met. -public export -data AllProofsComplete : Type where - MkAllProofsComplete : - SecretKey.generateTotal -> - KeyManager.generateTotal -> - KeyManager.rotateTotal -> - KeyManager.revokeTotal -> - KeyManager.retrieveTotal -> - AllProofsComplete - -||| Verification entry point. -export -verify : IO () -verify = putStrLn "All proofs verified." diff --git a/generated/idrisiser/idris2/Januskey/Verified/wrap_unwrap_round_trip.idr b/generated/idrisiser/idris2/Januskey/Verified/wrap_unwrap_round_trip.idr deleted file mode 100644 index c8d2cc4..0000000 --- a/generated/idrisiser/idris2/Januskey/Verified/wrap_unwrap_round_trip.idr +++ /dev/null @@ -1,191 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Copyright (c) Jonathan D.A. Jewell --- Auto-generated by idrisiser — do not edit manually. --- Interface: wrap-unwrap-round-trip (type-sig) --- Source: idrisiser/wrap-unwrap.tsig --- Regenerate with: idrisiser generate - -||| Formally verified wrapper for interface: wrap-unwrap-round-trip -||| -||| This module provides dependent-type proofs that: -||| - All functions are total (cover all inputs, terminate) -||| - Preconditions are checked before every call -||| - Postconditions hold after every call -||| - Invariants are preserved across all operations - -module Januskey.Verified.wrap_unwrap_round_trip - -import Data.So -import Data.Vect -import Data.Nat -import Linear -- quantitative type theory - -%default total - --- ================================================================ --- Contract Types --- ================================================================ - -||| Result of calling `wrap_key` -public export -data wrap_keyResult : Type where - wrap_keyOk : Result WrappedKey KeyError -> wrap_keyResult - wrap_keyErr : String -> wrap_keyResult - -||| Parameters for `wrap_key` -public export -record wrap_keyParams where - constructor Mkwrap_keyParams - arg0 : SecretKey - arg1 : Bytes 32 - arg2 : KeyMetadata - -||| Preconditions for `wrap_key` -public export -wrap_keyPre : wrap_keyParams -> Bool -wrap_keyPre params = - -- kek is a valid 32-byte SecretKey - -- key material passed to wrap_key is exactly KEY_LENGTH bytes - -- WrappedKey passed to unwrap_key was produced by wrap_key with the same kek - -- Nonce used in wrap_key is unique per wrapping operation (freshly generated) - True -- precondition witnesses generated here - -||| Postconditions for `wrap_key` -public export -wrap_keyPost : Result WrappedKey KeyError -> Bool -wrap_keyPost result = - -- wrap_key returns Ok(wrapped) where wrapped.metadata == the provided metadata - -- wrap_key nonce is exactly NONCE_LENGTH (12) bytes - -- unwrap_key(kek, wrap_key(kek, key, meta).unwrap()) == Ok(key) — round-trip - -- unwrap_key returns Err(CryptoError) if kek does not match the wrapping kek - -- unwrap_key returns Err(CryptoError) if plaintext.len() != 32 - True -- postcondition witnesses generated here - -||| Result of calling `unwrap_key` -public export -data unwrap_keyResult : Type where - unwrap_keyOk : Result SecretKey KeyError -> unwrap_keyResult - unwrap_keyErr : String -> unwrap_keyResult - -||| Parameters for `unwrap_key` -public export -record unwrap_keyParams where - constructor Mkunwrap_keyParams - arg0 : SecretKey - arg1 : WrappedKey - -||| Preconditions for `unwrap_key` -public export -unwrap_keyPre : unwrap_keyParams -> Bool -unwrap_keyPre params = - -- kek is a valid 32-byte SecretKey - -- key material passed to wrap_key is exactly KEY_LENGTH bytes - -- WrappedKey passed to unwrap_key was produced by wrap_key with the same kek - -- Nonce used in wrap_key is unique per wrapping operation (freshly generated) - True -- precondition witnesses generated here - -||| Postconditions for `unwrap_key` -public export -unwrap_keyPost : Result SecretKey KeyError -> Bool -unwrap_keyPost result = - -- wrap_key returns Ok(wrapped) where wrapped.metadata == the provided metadata - -- wrap_key nonce is exactly NONCE_LENGTH (12) bytes - -- unwrap_key(kek, wrap_key(kek, key, meta).unwrap()) == Ok(key) — round-trip - -- unwrap_key returns Err(CryptoError) if kek does not match the wrapping kek - -- unwrap_key returns Err(CryptoError) if plaintext.len() != 32 - True -- postcondition witnesses generated here - --- ================================================================ --- Proof Obligations --- ================================================================ - -||| Proof that `wrap_key` is total (covers all inputs) -public export -data wrap_keyTotal : Type where - Iswrap_keyTotal : wrap_keyTotal - -||| Proof that preconditions hold for given parameters -public export -data wrap_keyPreSatisfied : (params : wrap_keyParams) -> Type where - wrap_keyPreOk : So (wrap_keyPre params) -> wrap_keyPreSatisfied params - -||| Proof that postconditions hold for a given result -public export -data wrap_keyPostSatisfied : (result : Result WrappedKey KeyError) -> Type where - wrap_keyPostOk : So (wrap_keyPost result) -> wrap_keyPostSatisfied result - -||| Proof that serialise/deserialise round-trips for `wrap_key` results -public export -data wrap_keyRoundTrip : Type where - wrap_keyRoundTripOk : wrap_keyRoundTrip - -||| Proof that `unwrap_key` is total (covers all inputs) -public export -data unwrap_keyTotal : Type where - Isunwrap_keyTotal : unwrap_keyTotal - -||| Proof that preconditions hold for given parameters -public export -data unwrap_keyPreSatisfied : (params : unwrap_keyParams) -> Type where - unwrap_keyPreOk : So (unwrap_keyPre params) -> unwrap_keyPreSatisfied params - -||| Proof that postconditions hold for a given result -public export -data unwrap_keyPostSatisfied : (result : Result SecretKey KeyError) -> Type where - unwrap_keyPostOk : So (unwrap_keyPost result) -> unwrap_keyPostSatisfied result - -||| Proof that serialise/deserialise round-trips for `unwrap_key` results -public export -data unwrap_keyRoundTrip : Type where - unwrap_keyRoundTripOk : unwrap_keyRoundTrip - --- ================================================================ --- FFI Declarations (implemented in Zig bridge) --- ================================================================ - -export -%foreign "C:wrap_unwrap_round_trip_wrap_key, libwrap_unwrap_round_trip_verified" -prim__wrap_key : Bits64 -> Bits64 -> Bits64 -> PrimIO Bits32 - -export -%foreign "C:wrap_unwrap_round_trip_unwrap_key, libwrap_unwrap_round_trip_verified" -prim__unwrap_key : Bits64 -> Bits64 -> PrimIO Bits32 - --- ================================================================ --- Safe Wrappers (enforce contracts at the type level) --- ================================================================ - -||| Safe wrapper for `wrap_key` with contract enforcement. -export -wrap_key : (params : wrap_keyParams) -> {auto prf : wrap_keyPreSatisfied params} -> IO (Either String Result WrappedKey KeyError) -wrap_key params = do - rc <- primIO (prim__wrap_key params.arg0 params.arg1 params.arg2) - if rc == 0 - then pure (Right ()) - else pure (Left "Error in wrap_key") - -||| Safe wrapper for `unwrap_key` with contract enforcement. -export -unwrap_key : (params : unwrap_keyParams) -> {auto prf : unwrap_keyPreSatisfied params} -> IO (Either String Result SecretKey KeyError) -unwrap_key params = do - rc <- primIO (prim__unwrap_key params.arg0 params.arg1) - if rc == 0 - then pure (Right ()) - else pure (Left "Error in unwrap_key") - --- ================================================================ --- Verification --- ================================================================ - -||| Witness that all proof obligations for this interface are met. -public export -data AllProofsComplete : Type where - MkAllProofsComplete : - wrap_keyTotal -> - unwrap_keyTotal -> - AllProofsComplete - -||| Verification entry point. -export -verify : IO () -verify = putStrLn "All proofs verified." diff --git a/generated/idrisiser/januskey_verified.ipkg b/generated/idrisiser/januskey_verified.ipkg deleted file mode 100644 index f018f7f..0000000 --- a/generated/idrisiser/januskey_verified.ipkg +++ /dev/null @@ -1,8 +0,0 @@ --- Auto-generated by idrisiser for project: januskey -package januskey_verified - -sourcedir = "idris2" - -modules = Januskey.Verified.key_generation, Januskey.Verified.key_derivation, Januskey.Verified.wrap_unwrap_round_trip - -opts = "--total" diff --git a/generated/idrisiser/zig/januskey_ffi.zig b/generated/idrisiser/zig/januskey_ffi.zig deleted file mode 100644 index cef0b13..0000000 --- a/generated/idrisiser/zig/januskey_ffi.zig +++ /dev/null @@ -1,123 +0,0 @@ -// SPDX-License-Identifier: MPL-2.0 -// Copyright (c) Jonathan D.A. Jewell -// Auto-generated by idrisiser — do not edit manually. -// Zig FFI bridge for project: januskey -// Regenerate with: idrisiser generate - -const std = @import("std"); - -// Result codes matching Idris2 ABI -pub const Result = enum(c_int) { - ok = 0, - err = 1, - invalid_param = 2, - out_of_memory = 3, - null_pointer = 4, - proof_failure = 5, -}; - -// ---------------------------------------------------------------- -// Interface: key_generation -// ---------------------------------------------------------------- - -// User's implementation of SecretKey.generate -extern fn key_generation_SecretKey.generate(arg0: void) callconv(.C) ?*anyopaque; - -// Idris2-facing export for SecretKey.generate -export fn januskey_SecretKey.generate(arg0: u64) callconv(.C) u32 { - _ = key_generation_SecretKey.generate(arg0); - return 0; // ok -} - -// User's implementation of KeyManager.generate -extern fn key_generation_KeyManager.generate(arg0: ?*anyopaque, arg1: ?*anyopaque, arg2: ?*anyopaque, arg3: ?*anyopaque, arg4: ?*anyopaque) callconv(.C) ?*anyopaque; - -// Idris2-facing export for KeyManager.generate -export fn januskey_KeyManager.generate(arg0: u64, arg1: u64, arg2: u64, arg3: u64, arg4: u64) callconv(.C) u32 { - _ = key_generation_KeyManager.generate(arg0, arg1, arg2, arg3, arg4); - return 0; // ok -} - -// User's implementation of KeyManager.rotate -extern fn key_generation_KeyManager.rotate(arg0: ?*anyopaque, arg1: ?*anyopaque) callconv(.C) ?*anyopaque; - -// Idris2-facing export for KeyManager.rotate -export fn januskey_KeyManager.rotate(arg0: u64, arg1: u64) callconv(.C) u32 { - _ = key_generation_KeyManager.rotate(arg0, arg1); - return 0; // ok -} - -// User's implementation of KeyManager.revoke -extern fn key_generation_KeyManager.revoke(arg0: ?*anyopaque, arg1: ?*anyopaque) callconv(.C) ?*anyopaque; - -// Idris2-facing export for KeyManager.revoke -export fn januskey_KeyManager.revoke(arg0: u64, arg1: u64) callconv(.C) u32 { - _ = key_generation_KeyManager.revoke(arg0, arg1); - return 0; // ok -} - -// User's implementation of KeyManager.retrieve -extern fn key_generation_KeyManager.retrieve(arg0: ?*anyopaque, arg1: ?*anyopaque) callconv(.C) ?*anyopaque; - -// Idris2-facing export for KeyManager.retrieve -export fn januskey_KeyManager.retrieve(arg0: u64, arg1: u64) callconv(.C) u32 { - _ = key_generation_KeyManager.retrieve(arg0, arg1); - return 0; // ok -} - -// ---------------------------------------------------------------- -// Interface: key_derivation -// ---------------------------------------------------------------- - -// User's implementation of derive_kek -extern fn key_derivation_derive_kek(arg0: [*:0]const u8, arg1: ?*anyopaque) callconv(.C) ?*anyopaque; - -// Idris2-facing export for derive_kek -export fn januskey_derive_kek(arg0: u64, arg1: u64) callconv(.C) u32 { - _ = key_derivation_derive_kek(arg0, arg1); - return 0; // ok -} - -// ---------------------------------------------------------------- -// Interface: wrap_unwrap_round_trip -// ---------------------------------------------------------------- - -// User's implementation of wrap_key -extern fn wrap_unwrap_round_trip_wrap_key(arg0: ?*anyopaque, arg1: ?*anyopaque, arg2: ?*anyopaque) callconv(.C) ?*anyopaque; - -// Idris2-facing export for wrap_key -export fn januskey_wrap_key(arg0: u64, arg1: u64, arg2: u64) callconv(.C) u32 { - _ = wrap_unwrap_round_trip_wrap_key(arg0, arg1, arg2); - return 0; // ok -} - -// User's implementation of unwrap_key -extern fn wrap_unwrap_round_trip_unwrap_key(arg0: ?*anyopaque, arg1: ?*anyopaque) callconv(.C) ?*anyopaque; - -// Idris2-facing export for unwrap_key -export fn januskey_unwrap_key(arg0: u64, arg1: u64) callconv(.C) u32 { - _ = wrap_unwrap_round_trip_unwrap_key(arg0, arg1); - return 0; // ok -} - -// ---------------------------------------------------------------- -// Lifecycle -// ---------------------------------------------------------------- - -var initialized: bool = false; - -export fn januskey_verified_init() callconv(.C) c_int { - if (initialized) return 1; - initialized = true; - return 0; -} - -export fn januskey_verified_shutdown() callconv(.C) c_int { - if (!initialized) return 1; - initialized = false; - return 0; -} - -export fn idrisiser_version() callconv(.C) [*:0]const u8 { - return "0.1.0"; -} diff --git a/idrisiser.toml b/idrisiser.toml deleted file mode 100644 index b22f952..0000000 --- a/idrisiser.toml +++ /dev/null @@ -1,117 +0,0 @@ -# SPDX-License-Identifier: MPL-2.0 -# idrisiser manifest for januskey -# -# Generates Idris2 dependent-type wrappers for the JanusKey key-management -# library. JanusKey is security-critical: it handles key generation, -# wrapping, derivation, rotation, and revocation using Argon2id + AES-256-GCM. -# These wrappers prove that: -# - Generated key material is always exactly KEY_LENGTH (32) bytes -# - Key material is never the all-zero array after successful generation -# - KEK derivation from a passphrase is deterministic for a fixed salt -# - wrap_key / unwrap_key form an inverse pair (round-trip) -# - Revoked or Obliterated keys cannot be retrieved -# - Rotated key records its predecessor UUID in rotation_of - -[project] -name = "januskey" -module-prefix = "Januskey.Verified" - -# --------------------------------------------------------------------------- -# Interface 1 — key generation and lifecycle -# --------------------------------------------------------------------------- -[[interfaces]] -name = "key-generation" -source = "idrisiser/key-generation.tsig" -format = "type-sig" -verify = [ - "SecretKey.generate", - "KeyManager.generate", - "KeyManager.rotate", - "KeyManager.revoke", - "KeyManager.retrieve", -] -preconditions = [ - "KeyManager is initialised (unlock or init called successfully before any key operation)", - "SecretKey.generate uses a cryptographically secure random number generator", - "KeyManager.rotate is called with a key ID that exists and is not already Revoked", - "KeyManager.revoke is called with a key ID that exists and is not already Revoked", - "KeyManager.retrieve is called with a key ID that is Active or Rotating", -] -postconditions = [ - "SecretKey.generate returns Ok(key) where key.as_bytes().len() == 32", - "SecretKey.generate key material is not all-zero bytes", - "KeyManager.generate returns Ok(uuid) and the stored key has state == Active", - "KeyManager.rotate returns Ok(new_id) where new_id != old_id", - "KeyManager.rotate marks old key as Revoked", - "KeyManager.rotate new key has rotation_of == Some(old_id)", - "KeyManager.revoke sets key state to Revoked", - "KeyManager.retrieve returns Err(AlreadyRevoked) for any Revoked or Obliterated key", - "KeyManager.retrieve returns Ok(key) where key.as_bytes().len() == 32", -] -invariants = [ - "KEY_LENGTH is always 32 (AES-256 key size invariant)", - "Generated key material length is always exactly KEY_LENGTH bytes", - "Generated key material is never the all-zero array (security invariant)", - "A revoked key can never transition back to Active state", - "rotation_of for a rotated key is always Some(predecessor_uuid) — never None", - "Key fingerprint is always exactly 16 hex characters (8 bytes of SHA-256)", -] - -# --------------------------------------------------------------------------- -# Interface 2 — key derivation (KEK via Argon2id) -# --------------------------------------------------------------------------- -[[interfaces]] -name = "key-derivation" -source = "idrisiser/key-derivation.tsig" -format = "type-sig" -verify = ["derive_kek"] -preconditions = [ - "passphrase is a non-empty UTF-8 string", - "salt is exactly SALT_LENGTH (16) bytes", - "Argon2id parameters satisfy OWASP minimum: memory >= 64MB, iterations >= 3, parallelism >= 4", -] -postconditions = [ - "derive_kek returns Ok(kek) where kek.as_bytes().len() == 32", - "derive_kek is deterministic: same (passphrase, salt) always produces the same kek bytes", - "derive_kek returns Err(CryptoError) only if Argon2 parameter construction fails", -] -invariants = [ - "KEK derivation is deterministic for a fixed (passphrase, salt) pair", - "Output length is always exactly KEY_LENGTH (32) bytes", - "KEK bytes are not all-zero for any non-empty passphrase (probabilistic invariant)", - "Argon2id memory parameter is always >= 65536 KB (64 MB) per OWASP guidance", -] - -# --------------------------------------------------------------------------- -# Interface 3 — wrap/unwrap round-trip (AES-256-GCM) -# --------------------------------------------------------------------------- -[[interfaces]] -name = "wrap-unwrap-round-trip" -source = "idrisiser/wrap-unwrap.tsig" -format = "type-sig" -verify = ["wrap_key", "unwrap_key"] -preconditions = [ - "kek is a valid 32-byte SecretKey", - "key material passed to wrap_key is exactly KEY_LENGTH bytes", - "WrappedKey passed to unwrap_key was produced by wrap_key with the same kek", - "Nonce used in wrap_key is unique per wrapping operation (freshly generated)", -] -postconditions = [ - "wrap_key returns Ok(wrapped) where wrapped.metadata == the provided metadata", - "wrap_key nonce is exactly NONCE_LENGTH (12) bytes", - "unwrap_key(kek, wrap_key(kek, key, meta).unwrap()) == Ok(key) — round-trip", - "unwrap_key returns Err(CryptoError) if kek does not match the wrapping kek", - "unwrap_key returns Err(CryptoError) if plaintext.len() != 32", -] -invariants = [ - "wrap_key and unwrap_key form an inverse pair under the same kek", - "Tampering with ciphertext or AAD causes unwrap_key to return Err", - "Nonce in WrappedKey is always exactly NONCE_LENGTH (12) bytes", - "Unwrapped key length is always exactly KEY_LENGTH (32) bytes", -] - -[proofs] -require-totality = true -round-trip-proofs = true -qtt-tracking = true -search-depth = 150 diff --git a/idrisiser/key-derivation.tsig b/idrisiser/key-derivation.tsig deleted file mode 100644 index fbf8241..0000000 --- a/idrisiser/key-derivation.tsig +++ /dev/null @@ -1,5 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Type signatures for januskey KEK derivation (crates/januskey-cli/src/keys.rs) --- Format: name : Type (idrisiser type-sig format) - -derive_kek : String -> Bytes 16 -> Result SecretKey KeyError diff --git a/idrisiser/key-generation.tsig b/idrisiser/key-generation.tsig deleted file mode 100644 index c106002..0000000 --- a/idrisiser/key-generation.tsig +++ /dev/null @@ -1,9 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Type signatures for januskey key generation (crates/januskey-cli/src/keys.rs) --- Format: name : Type (idrisiser type-sig format) - -SecretKey.generate : () -> Result SecretKey KeyError -KeyManager.generate : KeyManager -> KeyAlgorithm -> KeyPurpose -> Option String -> Option Nat -> Result Uuid KeyError -KeyManager.rotate : KeyManager -> Uuid -> Result Uuid KeyError -KeyManager.revoke : KeyManager -> Uuid -> Result () KeyError -KeyManager.retrieve : KeyManager -> Uuid -> Result SecretKey KeyError diff --git a/idrisiser/wrap-unwrap.tsig b/idrisiser/wrap-unwrap.tsig deleted file mode 100644 index 10ededc..0000000 --- a/idrisiser/wrap-unwrap.tsig +++ /dev/null @@ -1,6 +0,0 @@ --- SPDX-License-Identifier: MPL-2.0 --- Type signatures for januskey AES-256-GCM wrap/unwrap (crates/januskey-cli/src/keys.rs) --- Format: name : Type (idrisiser type-sig format) - -wrap_key : SecretKey -> Bytes 32 -> KeyMetadata -> Result WrappedKey KeyError -unwrap_key : SecretKey -> WrappedKey -> Result SecretKey KeyError diff --git a/scripts/check-abi-tree.sh b/scripts/check-abi-tree.sh index 01ca042..c814354 100755 --- a/scripts/check-abi-tree.sh +++ b/scripts/check-abi-tree.sh @@ -45,10 +45,11 @@ while IFS= read -r f; do 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 +# 7. The idrisiser tree (generated/idrisiser/, idrisiser/, idrisiser.toml) is retired +# (removed 2026-10-14): a second, generated ABI tree must not come back. +for p in generated/idrisiser idrisiser idrisiser.toml; do + if [ -e "$p" ] || [ -L "$p" ]; then say "FAIL: $p exists (retired idrisiser tree)"; fail=1; fi +done 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)"