From 3a6d7ac4687d6b94846889d67491908c9c14d55b Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Mon, 12 Oct 2026 21:47:21 +0000
Subject: [PATCH] =?UTF-8?q?refactor(abi):=20one=20ABI=20tree=20=E2=80=94?=
 =?UTF-8?q?=20module-path=20layout,=20JanusKey=20casing,=20symlink=20farm?=
 =?UTF-8?q?=20retired?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The Idris2 ABI surface was three trees: flat sources in src/abi/, the
src/idris-abi/ symlink farm from #140 (so an .ipkg could reach them), and
generated/idrisiser/. Collapse the first two into one:

- src/abi/JanusKey/ABI/{Types,Layout,Foreign,Proofs}.idr, laid out by
  module name; src/abi/januskey-abi.ipkg beside them (sourcedir ".").
- Foreign.idr now declares JanusKey.ABI.Foreign and imports
  JanusKey.ABI.{Types,Layout} (was Januskey.*, J1-3). No other content
  change in this commit.
- src/idris-abi/ deleted.
- scripts/check-abi-tree.sh (just abi-tree-check; first step of
  idris-abi.yml): fails on a second .ipkg, a second Foreign.idr, a symlink
  under src/abi, a module whose declared name differs from its path, or a
  package/file mismatch. Negative control run locally (symlink farm +
  casing split reintroduced -> FAIL; removed -> OK).
- References repointed: Justfile, .github/workflows/idris-abi.yml,
  .machine_readable/contractiles/{Justfile,Mustfile.a2ml} (the dead $$f
  recipe replaced by the package check), tests/aspect/cross_cutting_test.sh,
  ffi/zig/{src/main.zig,include/januskey.h} comments, QUICKSTART-DEV.adoc,
  bot directives, PROOF-NEEDS.adoc.

Not claimed here: the package still does not typecheck. Foreign.idr is the
RSR template FFI (januskey_init/process/...) and never described ffi/zig's
jk_* exports; the header's "generated from src/abi/Foreign.idr" comment was
false and is corrected. Types.idr keeps its ten known errors. Both are the
next commits. generated/idrisiser/ is outside the gate, unchanged.

Refs: JNK-01 (ISSUES-2026-10-12), J1-3, P0-2 (#140).
Assisted-by: Claude (claude.ai session, 2026-10-12)
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01Kjdf4Mf4Z41bNQh2TrsEp9
---
 .github/workflows/idris-abi.yml               | 15 ++++--
 .../bot_directives/gitbot-fleet.a2ml          |  2 +-
 .machine_readable/contractiles/Justfile       | 17 ++----
 .machine_readable/contractiles/Mustfile.a2ml  |  2 +-
 Justfile                                      | 10 ++--
 PROOF-NEEDS.adoc                              | 44 +++++++++++++--
 QUICKSTART-DEV.adoc                           |  2 +-
 ffi/zig/include/januskey.h                    |  2 +-
 ffi/zig/src/main.zig                          |  2 +-
 scripts/check-abi-tree.sh                     | 53 +++++++++++++++++++
 src/abi/{ => JanusKey/ABI}/Foreign.idr        |  6 +--
 src/abi/{ => JanusKey/ABI}/Layout.idr         |  0
 src/abi/{ => JanusKey/ABI}/Proofs.idr         |  0
 src/abi/{ => JanusKey/ABI}/Types.idr          |  0
 src/abi/januskey-abi.ipkg                     | 20 +++++++
 src/idris-abi/JanusKey/ABI/Layout.idr         |  1 -
 src/idris-abi/JanusKey/ABI/Proofs.idr         |  1 -
 src/idris-abi/JanusKey/ABI/Types.idr          |  1 -
 src/idris-abi/Januskey/ABI/Foreign.idr        |  1 -
 src/idris-abi/januskey-abi.ipkg               | 30 -----------
 tests/aspect/cross_cutting_test.sh            | 10 ++--
 21 files changed, 146 insertions(+), 73 deletions(-)
 create mode 100755 scripts/check-abi-tree.sh
 rename src/abi/{ => JanusKey/ABI}/Foreign.idr (98%)
 rename src/abi/{ => JanusKey/ABI}/Layout.idr (100%)
 rename src/abi/{ => JanusKey/ABI}/Proofs.idr (100%)
 rename src/abi/{ => JanusKey/ABI}/Types.idr (100%)
 create mode 100644 src/abi/januskey-abi.ipkg
 delete mode 120000 src/idris-abi/JanusKey/ABI/Layout.idr
 delete mode 120000 src/idris-abi/JanusKey/ABI/Proofs.idr
 delete mode 120000 src/idris-abi/JanusKey/ABI/Types.idr
 delete mode 120000 src/idris-abi/Januskey/ABI/Foreign.idr
 delete mode 100644 src/idris-abi/januskey-abi.ipkg

diff --git a/.github/workflows/idris-abi.yml b/.github/workflows/idris-abi.yml
index 04cb957..0dd020f 100644
--- a/.github/workflows/idris-abi.yml
+++ b/.github/workflows/idris-abi.yml
@@ -1,7 +1,10 @@
 # SPDX-License-Identifier: MPL-2.0
-# Typechecks the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg).
-# NOT a required check: it is expected to be red until J1-3 fixes the known
-# errors in src/abi (Types.idr, and the Januskey/JanusKey module-name casing).
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+# Checks the Idris2 ABI tree invariants (scripts/check-abi-tree.sh) and
+# typechecks the ABI package (src/abi/januskey-abi.ipkg).
+# NOT yet a required check: the typecheck step is expected to be red until the
+# follow-up commits land (Foreign.idr still carries the RSR template FFI, and
+# Types.idr has known errors); the tree-invariant step must be green now.
 name: Idris ABI typecheck
 on:
   pull_request:
@@ -12,7 +15,7 @@ permissions:
   contents: read
 jobs:
   idris-abi:
-    name: "idris-abi (expected red until J1-3)"
+    name: "idris-abi"
     runs-on: ubuntu-latest
     timeout-minutes: 15
     container:
@@ -22,7 +25,9 @@ jobs:
         uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
         with:
           persist-credentials: false
+      - name: ABI tree invariants
+        run: bash scripts/check-abi-tree.sh
       - name: Typecheck ABI package
         run: |
           idris2 --version
-          idris2 --typecheck src/idris-abi/januskey-abi.ipkg
+          idris2 --typecheck src/abi/januskey-abi.ipkg
diff --git a/.machine_readable/bot_directives/gitbot-fleet.a2ml b/.machine_readable/bot_directives/gitbot-fleet.a2ml
index 811213c..fc37beb 100644
--- a/.machine_readable/bot_directives/gitbot-fleet.a2ml
+++ b/.machine_readable/bot_directives/gitbot-fleet.a2ml
@@ -27,7 +27,7 @@ never-touch = [
   ".machine_readable/contractiles/Trustfile.a2ml",
   "LICENSE",
 ]
-never-touch-notes = "src/abi/ + generated/idrisiser/ are the Idris2 ABI proof surface (changes require proof re-verification); threat-model.a2ml awaits human sign-off; the Trustfile may never be widened by an agent (see its self-integrity rule)."
+never-touch-notes = "src/abi/ (one tree: src/abi/januskey-abi.ipkg + JanusKey/ABI/*.idr, invariants in scripts/check-abi-tree.sh) + generated/idrisiser/ are the Idris2 ABI proof surface (changes require proof re-verification); threat-model.a2ml awaits human sign-off; the Trustfile may never be widened by an agent (see its self-integrity rule)."
 
 [per-bot.sustainabot]
 allow = ["Cargo.toml", "Cargo.lock", ".github/workflows (SHA bumps via grouped dependabot PRs only)"]
diff --git a/.machine_readable/contractiles/Justfile b/.machine_readable/contractiles/Justfile
index db5a756..a4ab838 100644
--- a/.machine_readable/contractiles/Justfile
+++ b/.machine_readable/contractiles/Justfile
@@ -84,21 +84,10 @@ test-contracts:
         done; \
     fi
 
-# Check Idris2 ABI proofs (requires idris2)
+# Check Idris2 ABI proofs (requires idris2); mirrors the root Justfile recipe
 test-proofs:
-    @echo "=== Proof Regression ==="
-    @if command -v idris2 >/dev/null 2>&1; then \
-        for f in src/abi/Types.idr src/abi/Layout.idr src/abi/Foreign.idr src/abi/Proofs.idr; do \
-            if [ -f "$$f" ]; then \
-                echo "Checking $$f..."; \
-                idris2 --check "$$f" && echo "  [OK] $$f" || echo "  [FAIL] $$f"; \
-            else \
-                echo "  [SKIP] $$f not found"; \
-            fi; \
-        done; \
-    else \
-        echo "SKIP: idris2 not installed. Install via: pack install-app idris2"; \
-    fi
+    bash scripts/check-abi-tree.sh
+    idris2 --typecheck src/abi/januskey-abi.ipkg
 
 # Run full test suite (all categories)
 test-all: test test-p2p test-regressions test-e2e test-aspect test-contracts test-proofs smoke
diff --git a/.machine_readable/contractiles/Mustfile.a2ml b/.machine_readable/contractiles/Mustfile.a2ml
index 21d3e66..9b3602a 100644
--- a/.machine_readable/contractiles/Mustfile.a2ml
+++ b/.machine_readable/contractiles/Mustfile.a2ml
@@ -147,7 +147,7 @@ trust level: even maximal-trust agents cannot violate MUST constraints.
 
 ### abi-proofs-preserved
 - description: Idris2 ABI definitions and proofs must not be removed (changes require proof update)
-- run: test -f src/abi/Types.idr && test -f src/abi/Proofs.idr && test -f src/abi/Foreign.idr
+- run: test -f src/abi/JanusKey/ABI/Types.idr && test -f src/abi/JanusKey/ABI/Proofs.idr && test -f src/abi/JanusKey/ABI/Foreign.idr && test -f src/abi/januskey-abi.ipkg
 - severity: critical
 
 ### generated-code-in-generated
diff --git a/Justfile b/Justfile
index 44b485a..8176a69 100644
--- a/Justfile
+++ b/Justfile
@@ -88,13 +88,17 @@ test-contracts:
         done; \
     fi
 
-# Typecheck the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg).
+# One ABI tree: no symlink farm, one ipkg, one Foreign.idr, module names match paths.
+abi-tree-check:
+    bash scripts/check-abi-tree.sh
+
+# Typecheck the Idris2 ABI package (src/abi/januskey-abi.ipkg).
 # Fails if idris2 is missing (set ALLOW_NO_IDRIS=1 to skip) or any module fails.
-test-proofs:
+test-proofs: abi-tree-check
     #!/usr/bin/env bash
     set -euo pipefail
     echo "=== Proof Regression ==="
-    ipkg="src/idris-abi/januskey-abi.ipkg"
+    ipkg="src/abi/januskey-abi.ipkg"
     if ! command -v idris2 >/dev/null 2>&1; then
         if [ "${ALLOW_NO_IDRIS:-0}" = "1" ]; then
             echo "SKIP: idris2 not installed and ALLOW_NO_IDRIS=1 -- ABI proofs were NOT checked." >&2
diff --git a/PROOF-NEEDS.adoc b/PROOF-NEEDS.adoc
index 9f60ff6..6d6039e 100644
--- a/PROOF-NEEDS.adoc
+++ b/PROOF-NEEDS.adoc
@@ -1,11 +1,47 @@
 == PROOF-NEEDS.md — januskey
 
+=== One ABI tree (2026-10-12)
+
+The Idris2 ABI surface was three trees: the flat sources in `+src/abi/+`,
+the `+src/idris-abi/+` symlink farm added by PR #140 so that an `+.ipkg+`
+could reach them, and `+generated/idrisiser/+`. It is now one: the sources
+live at `+src/abi/JanusKey/ABI/{Types,Layout,Foreign,Proofs}.idr+`, laid out
+by module name, with the package file beside them at
+`+src/abi/januskey-abi.ipkg+`; the symlink farm is deleted; the
+`+Januskey.ABI.Foreign+` / `+JanusKey.ABI.*+` casing split (J1-3) is
+normalised to `+JanusKey+`. `+scripts/check-abi-tree.sh+` (`+just
+abi-tree-check+`, first step of `+idris-abi.yml+`) fails on a second package
+file, a second `+Foreign.idr+`, a symlink under `+src/abi+`, a module whose
+declared name differs from its path, or a package/file mismatch.
+
+What this commit does *not* claim: the package still does not typecheck.
+Two facts were established while relocating it and are the next two
+commits, not this one:
+
+* `+Foreign.idr+` is the RSR *template* FFI (`+januskey_init+`,
+  `+januskey_process+`, `+januskey_get_string+`, …) written against
+  template types (`+createHandle+`, `+handlePtr+`, `+Result+`) that the
+  hand-written `+Types.idr+` does not define. It never described
+  `+ffi/zig+`, which exports `+jk_init+` … `+jk_version+` against
+  `+ffi/zig/include/januskey.h+`; that header's former comment
+  "generated from src/abi/Foreign.idr" was false and has been corrected.
+* `+Types.idr+` has the ten known errors from PR #140 (first:
+  `+isInfixOf+` without `+import Data.String+`; also forward references in
+  `+ResultOf+`, a `+Handle+` whose only constructor cannot inhabit
+  `+Handle Locked+`, linear variables used twice or not at all, and
+  `+oblitMostExpensive (S k) = Oh+` on an open `+k+`).
+
+`+generated/idrisiser/+` is unchanged and outside the gate; whether it is
+regenerated with capitalised module names or removed is an owner decision
+(JNK-01, open question).
+
 === Current State
 
-_Re-verified 2026-06-29 (idris2 0.8.0)._
+_Re-verified 2026-06-29 (idris2 0.8.0); paths updated 2026-10-12 to the
+single tree._
 
-* **src/abi/*.idr**: PRESENT but **placeholder** —
-`+src/abi/Proofs.idr+` typechecks, but its theorems are
+* **src/abi/JanusKey/ABI/*.idr**: PRESENT but **placeholder** —
+`+src/abi/JanusKey/ABI/Proofs.idr+` typechecks (when the package does), but its theorems are
 trivial/tautological (e.g. `+memoryDefeatsGPU : So (65536 >= 65536)+`,
 `+timeCostMonotonic : So (a >= b) -> So (a >= b)+` returns its own
 hypothesis). NOT the security proofs listed below.
@@ -17,7 +53,7 @@ verified.
 * *Dangerous patterns*: *265* `+unwrap()+` calls across the Rust
 codebase.
 * *LOC*: ~12,200 (Rust)
-* *ABI layer*: present (`+src/abi/{Types,Foreign,Layout,Proofs}.idr+`)
+* *ABI layer*: present (`+src/abi/JanusKey/ABI/{Types,Foreign,Layout,Proofs}.idr+`, package `+src/abi/januskey-abi.ipkg+`)
 but carries no load-bearing security proof yet — the real obligations
 below are still open.
 
diff --git a/QUICKSTART-DEV.adoc b/QUICKSTART-DEV.adoc
index 461ea86..2e08174 100644
--- a/QUICKSTART-DEV.adoc
+++ b/QUICKSTART-DEV.adoc
@@ -55,7 +55,7 @@ just setup-dev
 ----
 januskey/
 ├── src/                  # Source code
-├── src/abi/              # Idris2 ABI definitions (if applicable)
+├── src/abi/              # Idris2 ABI package (januskey-abi.ipkg, JanusKey/ABI/*.idr)
 ├── ffi/zig/              # Zig FFI bridge (if applicable)
 ├── tests/                # Test suite
 ├── docs/                 # Documentation
diff --git a/ffi/zig/include/januskey.h b/ffi/zig/include/januskey.h
index 3690a76..18c595f 100644
--- a/ffi/zig/include/januskey.h
+++ b/ffi/zig/include/januskey.h
@@ -2,7 +2,7 @@
 // Copyright (c) Jonathan D.A. Jewell <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
diff --git a/ffi/zig/src/main.zig b/ffi/zig/src/main.zig
index 0adf65f..2e0a96f 100644
--- a/ffi/zig/src/main.zig
+++ b/ffi/zig/src/main.zig
@@ -110,7 +110,7 @@ pub const OblitProof = extern struct {
 };
 
 comptime {
-    // Layout invariants — these mirror src/abi/Layout.idr and the comments
+    // Layout invariants — these mirror src/abi/JanusKey/ABI/Layout.idr and the comments
     // in januskey.h. If any fires, the C ABI and the Idris spec disagree.
     std.debug.assert(@sizeOf(ContentHash) == 32);
     std.debug.assert(@sizeOf(KeyId) == 16);
diff --git a/scripts/check-abi-tree.sh b/scripts/check-abi-tree.sh
new file mode 100755
index 0000000..923e761
--- /dev/null
+++ b/scripts/check-abi-tree.sh
@@ -0,0 +1,53 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+# One ABI tree. Fails when the Idris2 ABI surface is duplicated, symlinked,
+# mis-cased or inconsistent with its package file. Pure shell: runs without
+# idris2, so it can gate PRs on hosts that cannot typecheck.
+set -euo pipefail
+cd "$(dirname "$0")/.."
+fail=0
+say() { echo "[check-abi-tree] $*"; }
+
+# 1. The symlink farm (PR #140, src/idris-abi/) is retired.
+if [ -e src/idris-abi ]; then say "FAIL: src/idris-abi exists (retired symlink farm)"; fail=1; fi
+
+# 2. Exactly one package file, and it is the one the gates name.
+n=$(find src/abi -name '*.ipkg' | wc -l)
+if [ "$n" -ne 1 ]; then say "FAIL: expected 1 .ipkg under src/abi, found $n"; fail=1; fi
+if [ ! -f src/abi/januskey-abi.ipkg ]; then say "FAIL: src/abi/januskey-abi.ipkg missing"; fail=1; fi
+
+# 3. Exactly one Foreign.idr under src/ (the FFI surface is declared once).
+n=$(find src -name 'Foreign.idr' | wc -l)
+if [ "$n" -ne 1 ]; then say "FAIL: expected 1 Foreign.idr under src/, found $n"; fail=1; fi
+
+# 4. No symlinks under src/abi.
+n=$(find src/abi -type l | wc -l)
+if [ "$n" -ne 0 ]; then say "FAIL: $n symlink(s) under src/abi"; fail=1; fi
+
+# 5. Every module declaration matches its path (this is what caught the
+#    Januskey/JanusKey casing split).
+while IFS= read -r f; do
+  rel=${f#src/abi/}; want=${rel%.idr}; want=${want//\//.}
+  have=$(grep -m1 -E '^module ' "$f" | awk '{print $2}')
+  if [ "$have" != "$want" ]; then say "FAIL: $f declares module '$have'; path says '$want'"; fail=1; fi
+done < <(find src/abi -name '*.idr' | sort)
+
+# 6. Every module the package lists has a file; every file is listed.
+listed=$(sed -n '/^modules *=/,/^[^ ,]/p' src/abi/januskey-abi.ipkg | tr ',' '\n' | sed 's/^modules *=//; s/^[ ,]*//; s/[ ,]*$//' | grep -E '^[A-Z]' || true)
+for m in $listed; do
+  p="src/abi/${m//./\/}.idr"
+  if [ ! -f "$p" ]; then say "FAIL: ipkg lists $m but $p is missing"; fail=1; fi
+done
+while IFS= read -r f; do
+  rel=${f#src/abi/}; mod=${rel%.idr}; mod=${mod//\//.}
+  if ! grep -qx "$mod" <<< "$listed"; then say "FAIL: $f is not listed in src/abi/januskey-abi.ipkg"; fail=1; fi
+done < <(find src/abi -name '*.idr' | sort)
+
+# 7. Report, do not fail, on generated trees: they are not part of this gate.
+if [ -d generated/idrisiser ]; then
+  say "note: generated/idrisiser is present and is NOT part of the ABI gate (its modules do not typecheck; see PROOF-NEEDS.adoc)"
+fi
+
+if [ "$fail" -ne 0 ]; then say "FAIL"; exit 1; fi
+say "OK: one ABI tree ($(find src/abi -name '*.idr' | wc -l) modules, 1 package)"
diff --git a/src/abi/Foreign.idr b/src/abi/JanusKey/ABI/Foreign.idr
similarity index 98%
rename from src/abi/Foreign.idr
rename to src/abi/JanusKey/ABI/Foreign.idr
index 1520f8d..358e5e4 100644
--- a/src/abi/Foreign.idr
+++ b/src/abi/JanusKey/ABI/Foreign.idr
@@ -9,10 +9,10 @@
 ||| All functions are declared here with type signatures and safety proofs.
 ||| Implementations live in ffi/zig/
 
-module Januskey.ABI.Foreign
+module JanusKey.ABI.Foreign
 
-import Januskey.ABI.Types
-import Januskey.ABI.Layout
+import JanusKey.ABI.Types
+import JanusKey.ABI.Layout
 
 %default total
 
diff --git a/src/abi/Layout.idr b/src/abi/JanusKey/ABI/Layout.idr
similarity index 100%
rename from src/abi/Layout.idr
rename to src/abi/JanusKey/ABI/Layout.idr
diff --git a/src/abi/Proofs.idr b/src/abi/JanusKey/ABI/Proofs.idr
similarity index 100%
rename from src/abi/Proofs.idr
rename to src/abi/JanusKey/ABI/Proofs.idr
diff --git a/src/abi/Types.idr b/src/abi/JanusKey/ABI/Types.idr
similarity index 100%
rename from src/abi/Types.idr
rename to src/abi/JanusKey/ABI/Types.idr
diff --git a/src/abi/januskey-abi.ipkg b/src/abi/januskey-abi.ipkg
new file mode 100644
index 0000000..172b308
--- /dev/null
+++ b/src/abi/januskey-abi.ipkg
@@ -0,0 +1,20 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell
+--
+-- Idris2 package for the JanusKey ABI layer.
+--
+-- Sources live under src/abi/JanusKey/ABI/<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
diff --git a/src/idris-abi/JanusKey/ABI/Layout.idr b/src/idris-abi/JanusKey/ABI/Layout.idr
deleted file mode 120000
index fd00422..0000000
--- a/src/idris-abi/JanusKey/ABI/Layout.idr
+++ /dev/null
@@ -1 +0,0 @@
-../../../abi/Layout.idr
\ No newline at end of file
diff --git a/src/idris-abi/JanusKey/ABI/Proofs.idr b/src/idris-abi/JanusKey/ABI/Proofs.idr
deleted file mode 120000
index d63c148..0000000
--- a/src/idris-abi/JanusKey/ABI/Proofs.idr
+++ /dev/null
@@ -1 +0,0 @@
-../../../abi/Proofs.idr
\ No newline at end of file
diff --git a/src/idris-abi/JanusKey/ABI/Types.idr b/src/idris-abi/JanusKey/ABI/Types.idr
deleted file mode 120000
index 2c77c1f..0000000
--- a/src/idris-abi/JanusKey/ABI/Types.idr
+++ /dev/null
@@ -1 +0,0 @@
-../../../abi/Types.idr
\ No newline at end of file
diff --git a/src/idris-abi/Januskey/ABI/Foreign.idr b/src/idris-abi/Januskey/ABI/Foreign.idr
deleted file mode 120000
index 7495952..0000000
--- a/src/idris-abi/Januskey/ABI/Foreign.idr
+++ /dev/null
@@ -1 +0,0 @@
-../../../abi/Foreign.idr
\ No newline at end of file
diff --git a/src/idris-abi/januskey-abi.ipkg b/src/idris-abi/januskey-abi.ipkg
deleted file mode 100644
index bdf9f92..0000000
--- a/src/idris-abi/januskey-abi.ipkg
+++ /dev/null
@@ -1,30 +0,0 @@
--- SPDX-License-Identifier: MPL-2.0
--- Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
---
--- Idris2 package for the JanusKey ABI layer (src/abi/*.idr).
---
--- Idris2 resolves module A.B.C to <sourcedir>/A/B/C.idr, but the ABI sources
--- live flat in src/abi/ (Types.idr declares JanusKey.ABI.Types, etc.), so no
--- sourcedir value can reach them directly. They also cannot be moved: the
--- aspect tests, the Mustfile and the Zig FFI all name src/abi/<File>.idr.
--- This directory therefore holds relative symlinks laid out by module name,
--- each pointing back to the single real file in src/abi/.
---
--- Known defect, deliberately NOT fixed here (tracked as J1-3):
---   src/abi/Foreign.idr declares `Januskey.ABI.Foreign` (lowercase k) while
---   Proofs.idr imports `JanusKey.ABI.Foreign`; Foreign.idr in turn imports
---   `Januskey.ABI.Types` and `Januskey.ABI.Layout`, which no file declares. The
---   module is listed below under the name it actually declares, so these
---   imports fail to resolve until J1-3 normalises the casing.
---   The Januskey/ and JanusKey/ directories also collide on case-insensitive
---   filesystems (macOS/Windows default); typecheck on Linux.
---
--- Run: idris2 --typecheck src/idris-abi/januskey-abi.ipkg   (or: just test-proofs)
-package januskey-abi
-
-sourcedir = "."
-
-modules = JanusKey.ABI.Types
-        , JanusKey.ABI.Layout
-        , Januskey.ABI.Foreign
-        , JanusKey.ABI.Proofs
diff --git a/tests/aspect/cross_cutting_test.sh b/tests/aspect/cross_cutting_test.sh
index 7b3599f..1324d80 100755
--- a/tests/aspect/cross_cutting_test.sh
+++ b/tests/aspect/cross_cutting_test.sh
@@ -60,11 +60,11 @@ check "LICENSE directory exists" "[ -d '${JK_DIR}/LICENSES' ]"
 
 # --- Proofs ---
 echo "--- Formal Proofs ---"
-check "Types.idr exists (L1-L12)" "[ -f '${JK_DIR}/src/abi/Types.idr' ]"
-check "Layout.idr exists (CNO)" "[ -f '${JK_DIR}/src/abi/Layout.idr' ]"
-check "Foreign.idr exists (FFI)" "[ -f '${JK_DIR}/src/abi/Foreign.idr' ]"
-check "Proofs.idr exists (30+ proofs)" "[ -f '${JK_DIR}/src/abi/Proofs.idr' ]"
-check "C header generated" "[ -f '${JK_DIR}/ffi/zig/include/januskey.h' ]"
+check "Types.idr exists (L1-L12)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Types.idr' ]"
+check "Layout.idr exists (CNO)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Layout.idr' ]"
+check "Foreign.idr exists (FFI)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Foreign.idr' ]"
+check "Proofs.idr exists (30+ proofs)" "[ -f '${JK_DIR}/src/abi/JanusKey/ABI/Proofs.idr' ]"
+check "C header present (mirrors Foreign.idr)" "[ -f '${JK_DIR}/ffi/zig/include/januskey.h' ]"
 
 # --- Build ---
 echo "--- Build ---"