refactor(abi): one ABI tree — module-path layout, JanusKey casing, symlink farm retired (JNK-01, A of 3)

.github/workflows/idris-abi.yml

@@ -1,7 +1,10 @@
 # SPDX-License-Identifier: MPL-2.0
-# Typechecks the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg).
-# NOT a required check: it is expected to be red until J1-3 fixes the known
-# errors in src/abi (Types.idr, and the Januskey/JanusKey module-name casing).
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+# Checks the Idris2 ABI tree invariants (scripts/check-abi-tree.sh) and
+# typechecks the ABI package (src/abi/januskey-abi.ipkg).
+# NOT yet a required check: the typecheck step is expected to be red until the
+# follow-up commits land (Foreign.idr still carries the RSR template FFI, and
+# Types.idr has known errors); the tree-invariant step must be green now.
 name: Idris ABI typecheck
 on:
   pull_request:
@@ -12,7 +15,7 @@ permissions:
   contents: read
 jobs:
   idris-abi:
-    name: "idris-abi (expected red until J1-3)"
+    name: "idris-abi"
     runs-on: ubuntu-latest
     timeout-minutes: 15
     container:
@@ -22,7 +25,9 @@ jobs:
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           persist-credentials: false
+      - name: ABI tree invariants
+        run: bash scripts/check-abi-tree.sh
       - name: Typecheck ABI package
         run: |
           idris2 --version
-          idris2 --typecheck src/idris-abi/januskey-abi.ipkg
+          idris2 --typecheck src/abi/januskey-abi.ipkg

.machine_readable/bot_directives/gitbot-fleet.a2ml

@@ -27,7 +27,7 @@ never-touch = [
   ".machine_readable/contractiles/Trustfile.a2ml",
   "LICENSE",
 ]
-never-touch-notes = "src/abi/ + generated/idrisiser/ are the Idris2 ABI proof surface (changes require proof re-verification); threat-model.a2ml awaits human sign-off; the Trustfile may never be widened by an agent (see its self-integrity rule)."
+never-touch-notes = "src/abi/ (one tree: src/abi/januskey-abi.ipkg + JanusKey/ABI/*.idr, invariants in scripts/check-abi-tree.sh) + generated/idrisiser/ are the Idris2 ABI proof surface (changes require proof re-verification); threat-model.a2ml awaits human sign-off; the Trustfile may never be widened by an agent (see its self-integrity rule)."
 
 [per-bot.sustainabot]
 allow = ["Cargo.toml", "Cargo.lock", ".github/workflows (SHA bumps via grouped dependabot PRs only)"]

.machine_readable/contractiles/Justfile

@@ -84,21 +84,10 @@ test-contracts:
         done; \
     fi
 
-# Check Idris2 ABI proofs (requires idris2)
+# Check Idris2 ABI proofs (requires idris2); mirrors the root Justfile recipe
 test-proofs:
-    @echo "=== Proof Regression ==="
-    @if command -v idris2 >/dev/null 2>&1; then \
-        for f in src/abi/Types.idr src/abi/Layout.idr src/abi/Foreign.idr src/abi/Proofs.idr; do \
-            if [ -f "$$f" ]; then \
-                echo "Checking $$f..."; \
-                idris2 --check "$$f" && echo "  [OK] $$f" || echo "  [FAIL] $$f"; \
-            else \
-                echo "  [SKIP] $$f not found"; \
-            fi; \
-        done; \
-    else \
-        echo "SKIP: idris2 not installed. Install via: pack install-app idris2"; \
-    fi
+    bash scripts/check-abi-tree.sh
+    idris2 --typecheck src/abi/januskey-abi.ipkg
 
 # Run full test suite (all categories)
 test-all: test test-p2p test-regressions test-e2e test-aspect test-contracts test-proofs smoke

.machine_readable/contractiles/Mustfile.a2ml

@@ -147,7 +147,7 @@ trust level: even maximal-trust agents cannot violate MUST constraints.
 
 ### abi-proofs-preserved
 - description: Idris2 ABI definitions and proofs must not be removed (changes require proof update)
-- run: test -f src/abi/Types.idr && test -f src/abi/Proofs.idr && test -f src/abi/Foreign.idr
+- run: test -f src/abi/JanusKey/ABI/Types.idr && test -f src/abi/JanusKey/ABI/Proofs.idr && test -f src/abi/JanusKey/ABI/Foreign.idr && test -f src/abi/januskey-abi.ipkg
 - severity: critical
 
 ### generated-code-in-generated

Justfile

@@ -88,13 +88,17 @@ test-contracts:
         done; \
     fi
 
-# Typecheck the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg).
+# One ABI tree: no symlink farm, one ipkg, one Foreign.idr, module names match paths.
+abi-tree-check:
+    bash scripts/check-abi-tree.sh
+
+# Typecheck the Idris2 ABI package (src/abi/januskey-abi.ipkg).
 # Fails if idris2 is missing (set ALLOW_NO_IDRIS=1 to skip) or any module fails.
-test-proofs:
+test-proofs: abi-tree-check
     #!/usr/bin/env bash
     set -euo pipefail
     echo "=== Proof Regression ==="
-    ipkg="src/idris-abi/januskey-abi.ipkg"
+    ipkg="src/abi/januskey-abi.ipkg"
     if ! command -v idris2 >/dev/null 2>&1; then
         if [ "${ALLOW_NO_IDRIS:-0}" = "1" ]; then
             echo "SKIP: idris2 not installed and ALLOW_NO_IDRIS=1 -- ABI proofs were NOT checked." >&2

PROOF-NEEDS.adoc

@@ -1,11 +1,47 @@
 == PROOF-NEEDS.md — januskey
 
+=== One ABI tree (2026-10-12)
+
+The Idris2 ABI surface was three trees: the flat sources in `+src/abi/+`,
+the `+src/idris-abi/+` symlink farm added by PR #140 so that an `+.ipkg+`
+could reach them, and `+generated/idrisiser/+`. It is now one: the sources
+live at `+src/abi/JanusKey/ABI/{Types,Layout,Foreign,Proofs}.idr+`, laid out
+by module name, with the package file beside them at
+`+src/abi/januskey-abi.ipkg+`; the symlink farm is deleted; the
+`+Januskey.ABI.Foreign+` / `+JanusKey.ABI.*+` casing split (J1-3) is
+normalised to `+JanusKey+`. `+scripts/check-abi-tree.sh+` (`+just
+abi-tree-check+`, first step of `+idris-abi.yml+`) fails on a second package
+file, a second `+Foreign.idr+`, a symlink under `+src/abi+`, a module whose
+declared name differs from its path, or a package/file mismatch.
+
+What this commit does *not* claim: the package still does not typecheck.
+Two facts were established while relocating it and are the next two
+commits, not this one:
+
+* `+Foreign.idr+` is the RSR *template* FFI (`+januskey_init+`,
+  `+januskey_process+`, `+januskey_get_string+`, …) written against
+  template types (`+createHandle+`, `+handlePtr+`, `+Result+`) that the
+  hand-written `+Types.idr+` does not define. It never described
+  `+ffi/zig+`, which exports `+jk_init+` … `+jk_version+` against
+  `+ffi/zig/include/januskey.h+`; that header's former comment
+  "generated from src/abi/Foreign.idr" was false and has been corrected.
+* `+Types.idr+` has the ten known errors from PR #140 (first:
+  `+isInfixOf+` without `+import Data.String+`; also forward references in
+  `+ResultOf+`, a `+Handle+` whose only constructor cannot inhabit
+  `+Handle Locked+`, linear variables used twice or not at all, and
+  `+oblitMostExpensive (S k) = Oh+` on an open `+k+`).
+
+`+generated/idrisiser/+` is unchanged and outside the gate; whether it is
+regenerated with capitalised module names or removed is an owner decision
+(JNK-01, open question).
+
 === Current State
 
-_Re-verified 2026-06-29 (idris2 0.8.0)._
+_Re-verified 2026-06-29 (idris2 0.8.0); paths updated 2026-10-12 to the
+single tree._
 
-* **src/abi/*.idr**: PRESENT but **placeholder** —
-`+src/abi/Proofs.idr+` typechecks, but its theorems are
+* **src/abi/JanusKey/ABI/*.idr**: PRESENT but **placeholder** —
+`+src/abi/JanusKey/ABI/Proofs.idr+` typechecks (when the package does), but its theorems are
 trivial/tautological (e.g. `+memoryDefeatsGPU : So (65536 >= 65536)+`,
 `+timeCostMonotonic : So (a >= b) -> So (a >= b)+` returns its own
 hypothesis). NOT the security proofs listed below.
@@ -17,7 +53,7 @@
 * *Dangerous patterns*: *265* `+unwrap()+` calls across the Rust
 codebase.
 * *LOC*: ~12,200 (Rust)
-* *ABI layer*: present (`+src/abi/{Types,Foreign,Layout,Proofs}.idr+`)
+* *ABI layer*: present (`+src/abi/JanusKey/ABI/{Types,Foreign,Layout,Proofs}.idr+`, package `+src/abi/januskey-abi.ipkg+`)
 but carries no load-bearing security proof yet — the real obligations
 below are still open.
 

QUICKSTART-DEV.adoc

@@ -55,7 +55,7 @@ just setup-dev
 ----
 januskey/
 ├── src/                  # Source code
-├── src/abi/              # Idris2 ABI definitions (if applicable)
+├── src/abi/              # Idris2 ABI package (januskey-abi.ipkg, JanusKey/ABI/*.idr)
 ├── ffi/zig/              # Zig FFI bridge (if applicable)
 ├── tests/                # Test suite
 ├── docs/                 # Documentation

ffi/zig/include/januskey.h

@@ -2,7 +2,7 @@
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 /* SPDX-License-Identifier: MPL-2.0 */
 /* Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) */
-/* JanusKey C FFI Header — generated from src/abi/Foreign.idr */
+/* JanusKey C FFI Header — hand-maintained; src/abi/JanusKey/ABI/Foreign.idr must mirror it (checked by the ABI package typecheck) */
 
 #ifndef JANUSKEY_H
 #define JANUSKEY_H

ffi/zig/src/main.zig

@@ -110,7 +110,7 @@ pub const OblitProof = extern struct {
 };
 
 comptime {
-    // Layout invariants — these mirror src/abi/Layout.idr and the comments
+    // Layout invariants — these mirror src/abi/JanusKey/ABI/Layout.idr and the comments
     // in januskey.h. If any fires, the C ABI and the Idris spec disagree.
     std.debug.assert(@sizeOf(ContentHash) == 32);
     std.debug.assert(@sizeOf(KeyId) == 16);

scripts/check-abi-tree.sh

@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+# One ABI tree. Fails when the Idris2 ABI surface is duplicated, symlinked,
+# mis-cased or inconsistent with its package file. Pure shell: runs without
+# idris2, so it can gate PRs on hosts that cannot typecheck.
+set -euo pipefail
+cd "$(dirname "$0")/.."
+fail=0
+say() { echo "[check-abi-tree] $*"; }
+
+# 1. The symlink farm (PR #140, src/idris-abi/) is retired.
+if [ -e src/idris-abi ]; then say "FAIL: src/idris-abi exists (retired symlink farm)"; fail=1; fi
+
+# 2. Exactly one package file, and it is the one the gates name.
+n=$(find src/abi -name '*.ipkg' | wc -l)
+if [ "$n" -ne 1 ]; then say "FAIL: expected 1 .ipkg under src/abi, found $n"; fail=1; fi
+if [ ! -f src/abi/januskey-abi.ipkg ]; then say "FAIL: src/abi/januskey-abi.ipkg missing"; fail=1; fi
+
+# 3. Exactly one Foreign.idr under src/ (the FFI surface is declared once).
+n=$(find src -name 'Foreign.idr' | wc -l)
+if [ "$n" -ne 1 ]; then say "FAIL: expected 1 Foreign.idr under src/, found $n"; fail=1; fi
+
+# 4. No symlinks under src/abi.
+n=$(find src/abi -type l | wc -l)
+if [ "$n" -ne 0 ]; then say "FAIL: $n symlink(s) under src/abi"; fail=1; fi
+
+# 5. Every module declaration matches its path (this is what caught the
+#    Januskey/JanusKey casing split).
+while IFS= read -r f; do
+  rel=${f#src/abi/}; want=${rel%.idr}; want=${want//\//.}
+  have=$(grep -m1 -E '^module ' "$f" | awk '{print $2}')
+  if [ "$have" != "$want" ]; then say "FAIL: $f declares module '$have'; path says '$want'"; fail=1; fi
+done < <(find src/abi -name '*.idr' | sort)
+
+# 6. Every module the package lists has a file; every file is listed.
+listed=$(sed -n '/^modules *=/,/^[^ ,]/p' src/abi/januskey-abi.ipkg | tr ',' '\n' | sed 's/^modules *=//; s/^[ ,]*//; s/[ ,]*$//' | grep -E '^[A-Z]' || true)
+for m in $listed; do
+  p="src/abi/${m//./\/}.idr"
+  if [ ! -f "$p" ]; then say "FAIL: ipkg lists $m but $p is missing"; fail=1; fi
+done
+while IFS= read -r f; do
+  rel=${f#src/abi/}; mod=${rel%.idr}; mod=${mod//\//.}
+  if ! grep -qx "$mod" <<< "$listed"; then say "FAIL: $f is not listed in src/abi/januskey-abi.ipkg"; fail=1; fi
+done < <(find src/abi -name '*.idr' | sort)
+
+# 7. Report, do not fail, on generated trees: they are not part of this gate.
+if [ -d generated/idrisiser ]; then
+  say "note: generated/idrisiser is present and is NOT part of the ABI gate (its modules do not typecheck; see PROOF-NEEDS.adoc)"
+fi
+
+if [ "$fail" -ne 0 ]; then say "FAIL"; exit 1; fi
+say "OK: one ABI tree ($(find src/abi -name '*.idr' | wc -l) modules, 1 package)"

src/abi/Foreign.idr → src/abi/JanusKey/ABI/Foreign.idr

@@ -9,10 +9,10 @@
 ||| All functions are declared here with type signatures and safety proofs.
 ||| Implementations live in ffi/zig/
 
-module Januskey.ABI.Foreign
+module JanusKey.ABI.Foreign
 
-import Januskey.ABI.Types
-import Januskey.ABI.Layout
+import JanusKey.ABI.Types
+import JanusKey.ABI.Layout
 
 %default total
 

src/abi/januskey-abi.ipkg

@@ -0,0 +1,20 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- Idris2 package for the JanusKey ABI layer.
+--
+-- Sources live under src/abi/JanusKey/ABI/<Module>.idr, laid out by module
+-- name, so `idris2 --typecheck src/abi/januskey-abi.ipkg` reaches them
+-- directly. The former src/idris-abi/ symlink farm (PR #140) and the
+-- Januskey/JanusKey casing split it worked around are gone; the tree
+-- invariants are enforced by scripts/check-abi-tree.sh (just abi-tree-check).
+--
+-- Run: idris2 --typecheck src/abi/januskey-abi.ipkg   (or: just test-proofs)
+package januskey-abi
+
+sourcedir = "."
+
+modules = JanusKey.ABI.Types
+        , JanusKey.ABI.Layout
+        , JanusKey.ABI.Foreign
+        , JanusKey.ABI.Proofs

tests/aspect/cross_cutting_test.sh

@@ -60,11 +60,11 @@ check "LICENSE directory exists" "[ -d '${JK_DIR}/LICENSES' ]"
 
 # --- Proofs ---
 echo "--- Formal Proofs ---"
-check "Types.idr exists (L1-L12)" "[ -f '${JK_DIR}/src/abi/Types.idr' ]"
-check "Layout.idr exists (CNO)" "[ -f '${JK_DIR}/src/abi/Layout.idr' ]"
-check "Foreign.idr exists (FFI)" "[ -f '${JK_DIR}/src/abi/Foreign.idr' ]"
-check "Proofs.idr exists (30+ proofs)" "[ -f '${JK_DIR}/src/abi/Proofs.idr' ]"
-check "C header generated" "[ -f '${JK_DIR}/ffi/zig/include/januskey.h' ]"
+check "Types.idr exists (L1-L12)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Types.idr' ]"
+check "Layout.idr exists (CNO)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Layout.idr' ]"
+check "Foreign.idr exists (FFI)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Foreign.idr' ]"
+check "Proofs.idr exists (30+ proofs)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Proofs.idr' ]"
+check "C header present (mirrors Foreign.idr)" "[ -f '${JK_DIR}/ffi/zig/include/januskey.h' ]"
 
 # --- Build ---
 echo "--- Build ---"