fix(test-proofs): make the Idris2 ABI check able to fail (P0-2)

.github/workflows/idris-abi.yml

@@ -0,0 +1,28 @@
+# 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).
+name: Idris ABI typecheck
+on:
+  pull_request:
+  push:
+    branches: [main]
+  workflow_dispatch:
+permissions:
+  contents: read
+jobs:
+  idris-abi:
+    name: "idris-abi (expected red until J1-3)"
+    runs-on: ubuntu-latest
+    timeout-minutes: 15
+    container:
+      image: ghcr.io/stefan-hoeck/idris2-pack@sha256:f0758996a931fb35d9ecb1de273c4d59dabe2a09b433afc7e357f65a08b7e1ff
+    steps:
+      - name: Checkout
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+        with:
+          persist-credentials: false
+      - name: Typecheck ABI package
+        run: |
+          idris2 --version
+          idris2 --typecheck src/idris-abi/januskey-abi.ipkg

Justfile

@@ -88,21 +88,24 @@ test-contracts:
         done; \
     fi
 
-# Check Idris2 ABI proofs (requires idris2)
+# Typecheck the Idris2 ABI package (src/idris-abi/januskey-abi.ipkg).
+# Fails if idris2 is missing (set ALLOW_NO_IDRIS=1 to skip) or any module fails.
 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"; \
+    #!/usr/bin/env bash
+    set -euo pipefail
+    echo "=== Proof Regression ==="
+    ipkg="src/idris-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
+            exit 0
+        fi
+        echo "FAIL: idris2 not installed; cannot check ABI proofs. Install via: pack install-app idris2 (or set ALLOW_NO_IDRIS=1 to skip explicitly)." >&2
+        exit 1
     fi
+    echo "idris2 --typecheck $ipkg ($(idris2 --version))"
+    idris2 --typecheck "$ipkg"
+    echo "[OK] ABI package typechecks"
 
 # Run full test suite (all categories)
 test-all: test test-p2p test-regressions test-e2e test-aspect test-contracts test-proofs smoke

src/idris-abi/JanusKey/ABI/Layout.idr

@@ -0,0 +1 @@
+../../../abi/Layout.idr

src/idris-abi/JanusKey/ABI/Proofs.idr

@@ -0,0 +1 @@
+../../../abi/Proofs.idr

src/idris-abi/JanusKey/ABI/Types.idr

@@ -0,0 +1 @@
+../../../abi/Types.idr

src/idris-abi/Januskey/ABI/Foreign.idr

@@ -0,0 +1 @@
+../../../abi/Foreign.idr

src/idris-abi/januskey-abi.ipkg

@@ -0,0 +1,30 @@
+-- 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