ci(abi): gate the Idris2 proofs on every PR, with module-shaped paths

.github/workflows/proven-tests.yml

@@ -3,7 +3,7 @@
 #
 # proven-tests.yml — the estate's evidence-graded test framework, wired.
 #
-# THE TWO JOBS DO DIFFERENT THINGS AND NEITHER PRETENDS TO BE THE OTHER
+# THE JOBS DO DIFFERENT THINGS AND NONE PRETENDS TO BE ANOTHER
 # ---------------------------------------------------------------------
 # `ledger` (every PR, blocking, minutes): derives a proven-tests run report from
 #   THIS repo's suite — from a test inventory the runner emitted in the same
@@ -22,6 +22,10 @@
 #   and it would make every contributor wait on a compiler that cannot change
 #   for them.
 #
+# `abi-proofs` (every PR, blocking): type-checks this repository's own Idris2
+#   proofs in src/abi with the same pinned Idris2. It reuses the framework job's
+#   toolchain cache, so it costs a compiler build only on a cold cache.
+#
 # WHY THE REPORT IS A FILE, NOT A PARAGRAPH: docs/INTEROP-PANIC-ATTACK.adoc in
 # proven-tests-and-benches fixes the mapping in prose; a report plus a verifier
 # is the same mapping with something at stake.
@@ -142,6 +146,56 @@ jobs:
           retention-days: 30
           if-no-files-found: warn
 
+  abi-proofs:
+    # Every PR: type-check this repo's own Idris2 ABI proofs (src/abi). Without
+    # this, src/abi/PanicAttack/ABI/Stripping.idr sat on main not compiling
+    # while PROOF-NEEDS.adoc called it closed. The toolchain comes from the same
+    # pinned installer and cache key as the framework job, so a warm cache makes
+    # this a type-check, not a compiler build.
+    name: Idris2 — src/abi proofs type-check
+    runs-on: ubuntu-latest
+    timeout-minutes: 60
+    steps:
+      - name: Checkout this repository
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Checkout proven-tests-and-benches at the pinned commit
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
+        with:
+          repository: hyperpolymath/proven-tests-and-benches
+          ref: ${{ env.PROVEN_TESTS_PIN }}
+          path: .proven-tests
+          persist-credentials: false
+
+      - name: Cache the Idris2 toolchain
+        uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: ~/.idris2
+          key: idris2-v${{ env.IDRIS2_VERSION }}-${{ runner.os }}
+
+      - name: Install Idris2 (chez backend)
+        working-directory: .proven-tests
+        env:
+          IDRIS2_VERSION: v${{ env.IDRIS2_VERSION }}
+        run: bash scripts/install-idris2.sh
+
+      - name: Type-check src/abi
+        run: |
+          set -euo pipefail
+          export PATH="$HOME/.idris2/bin:$PATH"
+          idris2 --version
+          # `idris2 --check` can exit 0 while printing an error, so require
+          # both a zero exit and no `Error:` line.
+          status=0
+          out="$(idris2 --typecheck src/abi/panic-attack-abi.ipkg 2>&1)" || status=$?
+          printf '%s\n' "$out"
+          if [ "$status" -ne 0 ] || grep -q '^Error' <<<"$out"; then
+            echo "::error::src/abi Idris2 proofs do not type-check (exit $status)"
+            exit 1
+          fi
+
   framework:
     name: Framework — the grader is exercised (scheduled)
     if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'

EXPLAINME.adoc

@@ -52,9 +52,9 @@ The README makes claims. This file backs them up.
 | `src/comment_marker.rs` | Inline `// panic-attack: accepted [- reason]` suppression marker — `//` / `#` / `--` / `;` / `%` leaders, string-literal aware
 | `src/ffi_kind.rs` | UnsafeFFI (PA013) subtyping: BuildSystem (`build.zig` / `build.rs` — audit-accepted), RuntimeAbi (`bindings/` / `ffi/` / `sys/` / `cdef.zig`), TestMock (`tests/mocks/` / `_stub`), Unknown
 | `src/jit_context.rs` | JIT-framework classifier: Cranelift / Llvm / Wasm / Javascript / None; `transmute_targets_fn_ptr` recogniser for fn-ptr type-punning
-| `src/abi/PatternCompleteness.idr` | PA1 Idris2 proof — every Lang/Category has a detector
-| `src/abi/ClassificationSoundness.idr` | PA2 Idris2 proof — severity total order + maxSeverity commutativity
-| `src/abi/Stripping.idr` | Layer 1.0 partial — line-comment-strip foundation (shape lemma + base cases of `stripLineCommentsIdempotent` Qed-closed)
+| `src/abi/PanicAttack/ABI/PatternCompleteness.idr` | PA1 Idris2 model of analyzer dispatch; vacuous as stated (see `PROOF-NEEDS.adoc`)
+| `src/abi/PanicAttack/ABI/ClassificationSoundness.idr` | PA2 Idris2 proof — severity total order, `sevMax` upper bounds, monotone encoding
+| `src/abi/PanicAttack/ABI/Stripping.idr` | Layer 1.0 — Idris2 model of line-comment stripping, proved idempotent (`stripLineCommentsIdempotent`)
 | `src/kanren/` | Logic engine (unification, fact database, taint, cross-lang)
 | `src/kanren/core.rs` | Term, substitution, unification, FactDB, forward chaining
 | `src/kanren/taint.rs` | Source→sink tracking (user input, network, deserialization)

PROOF-NEEDS.adoc

@@ -27,29 +27,31 @@ compiles at `f2a6a70eaec0cb02331e3264e05f185b5faab0f7`. The only `unsafe`
 is in `examples/vulnerable_program.rs`, a deliberately buggy program that
 exists to be scanned.
 
-== Receipt for the Idris2 modules
-
-* *Checker:* Idris2 0.7.0, the version `proven-tests.yml` pins, built from
-  tag `v0.7.0` (`27780073c8631826d846499840b3857d9b9a4fd5`) on Chez Scheme
-  9.5.8.
-* *Source:* `src/abi/*.idr` at
-  `3dc4728762f37c1e5bebdb988783c7683c50fb55`. `Stripping.idr` was rechecked
-  after the comment-only edits in `ab0fdb2107e034e99b4b4f2fd7fb7366750d536e`
-  and still passes; the other four modules are unchanged since `3dc4728`.
-* *Invocation:* the modules are named `PanicAttack.ABI.<M>` but live in
-  `src/abi/`, so `idris2 --check src/abi/<M>.idr` fails on a module-name
-  mismatch from any directory. Each was checked from a tree that places
-  `src/abi/<M>.idr` at `PanicAttack/ABI/<M>.idr`, with
-  `idris2 --check PanicAttack/ABI/<M>.idr`. A pass is exit 0 *and* no
-  `Error:` line, because `idris2 --check` can exit 0 while printing an
-  error.
-* *Result:* all five modules pass. Every module sets `%default total` and
-  uses no `believe_me`, `assert_total`, `postulate` or holes.
-* *Negative controls:* a planted false lemma and a planted non-terminating
-  definition in `Stripping.idr` were both rejected, so the check can fail.
-* *Gate:* no CI job runs this check. That obligation is `OPEN` below. Until
-  it closes, the statuses here rest on this one local run, and any change
-  to `src/abi/` invalidates them.
+== How the Idris2 modules are checked
+
+The modules live at `src/abi/PanicAttack/ABI/<M>.idr`, so each path matches
+its module name, and `src/abi/panic-attack-abi.ipkg` lists them all.
+
+* *Gate:* the `abi-proofs` job in `.github/workflows/proven-tests.yml` runs
+  on every pull request and on pushes to `main`:
+  `idris2 --typecheck src/abi/panic-attack-abi.ipkg`. A pass is exit 0
+  *and* no `Error:` line, because `idris2 --check` can exit 0 while printing
+  an error. Its toolchain is Idris2 0.7.0 from the same pinned installer and
+  cache as the framework job. Each green run of that job is the current
+  receipt; a failing run revokes the statuses below.
+* *Negative controls* for the package route: a planted false lemma and a
+  planted missing import each make it exit non-zero with an `Error:` line.
+* *Hygiene:* every module sets `%default total` and uses no `believe_me`,
+  `assert_total`, `postulate` or holes.
+
+First receipt, before the gate existed: Idris2 0.7.0, built from tag
+`v0.7.0` (`27780073c8631826d846499840b3857d9b9a4fd5`) on Chez Scheme 9.5.8,
+over `src/abi/*.idr` at `3dc4728762f37c1e5bebdb988783c7683c50fb55`. Each
+module was checked from a module-shaped copy of the tree. All five passed,
+and a planted false lemma and a planted non-terminating definition in
+`Stripping.idr` were both rejected. `Stripping.idr` was rechecked after the
+comment-only edits in `ab0fdb2107e034e99b4b4f2fd7fb7366750d536e` and still
+passed.
 
 == Ledger
 
@@ -59,14 +61,14 @@ exists to be scanned.
 
 |Severity order: `Low < Medium < High < Critical` is a total order;
 `sevMax` is an upper bound; the numeric encoding is monotone (PA2)
-|`src/abi/ClassificationSoundness.idr`
+|`src/abi/PanicAttack/ABI/ClassificationSoundness.idr`
 |`PROVEN` (model)
 |The model's `Severity` matches the variant names and order of
 `src/types.rs`; that correspondence is `ASSUMED` (a hand transcription).
 The Rust order itself comes from `#[derive(PartialOrd, Ord)]`.
 
 |Line-comment stripping is idempotent: `strip (strip s) = strip s`
-|`src/abi/Stripping.idr`
+|`src/abi/PanicAttack/ABI/Stripping.idr`
 |`PROVEN` (model)
 |Did not compile on `main` before `3dc4728`; repaired there without
 changing the theorem. The repaired model equals the previous one:
@@ -82,7 +84,7 @@ string. The model also covers line comments only; block comments and string
 literals are not modelled.
 
 |Attestation chain: integrity, authenticity, non-repudiation
-|`src/abi/AttestationUnforgeability.idr`
+|`src/abi/PanicAttack/ABI/AttestationUnforgeability.idr`
 |`PROVEN` (model), relative to the `ASSUMED` hypotheses listed here
 |The module's `parameters` block assumes:
 
@@ -104,7 +106,7 @@ model, not a computational security reduction. Model to
 
 |Every language reaches an analyzer; every weak-point category has a
 detector; cross-language checks run on every file (PA1)
-|`src/abi/PatternCompleteness.idr`
+|`src/abi/PanicAttack/ABI/PatternCompleteness.idr`
 |`PROVEN` (model); supports no claim about the Rust code
 |The theorem is vacuous: `GenericAnalyzer : HasAnalyzer lang` inhabits
 the witness type for every language, so it holds whatever the dispatch
@@ -123,7 +125,7 @@ when `configuration.is_some()`. That model claim is false of the
 implementation.
 
 |Declarations for the ABI-facing types and their C integer encodings
-|`src/abi/Types.idr`
+|`src/abi/PanicAttack/ABI/Types.idr`
 |No theorem
 |Repaired in `3dc4728` so it compiles. It contains no proof and nothing
 imports it. Drift: its `Severity` is `Info / Warning / Error / Critical`
@@ -154,12 +156,6 @@ not establish a faithful hexad-to-octad map.
 |===
 |Obligation |Verifier (§1, §1.2) |Notes
 
-|Gate the Idris2 modules in CI
-|CI
-|Run the receipt's invocation on every change to `src/abi/`, failing on
-any `Error:` line. Moving the files to `src/abi/PanicAttack/ABI/` would
-let a plain `idris2 --check` work.
-
 |`strip_proof_comments` is idempotent and preserves positions outside
 comments and strings
 |Fix the implementation first; then Creusot/Pearlite and Verus

PROOF-PROGRAMME.adoc

@@ -1,3 +1,3 @@
 == PROOF-PROGRAMME.md — panic-attack from first principles
 
 ____
@@ -14,12 +14,12 @@
 [width="100%",cols="34%,33%,33%",options="header",]
 |===
 |ID |File |Mechanises
-|*PA1* |`+src/abi/PatternCompleteness.idr+` |Every `+Lang+` constructor
+|*PA1* |`+src/abi/PanicAttack/ABI/PatternCompleteness.idr+` |Every `+Lang+` constructor
 has at least one analyzer; every `+WPCategory+` has at least one
 detector; cross-language checks apply uniformly. Top theorem:
 `+completeScanForAll+`.
 
-|*PA2* |`+src/abi/ClassificationSoundness.idr+` |`+Severity+` is totally
+|*PA2* |`+src/abi/PanicAttack/ABI/ClassificationSoundness.idr+` |`+Severity+` is totally
 ordered (`+LTE+`); `+maxSeverity+` is commutative + idempotent; numeric
 ABI encoding preserves the ordering.
 |===
@@ -81,7 +81,7 @@
 
 [source,idris]
 ----
--- src/abi/PA004_UnsafeCode.idr
+-- src/abi/PanicAttack/ABI/PA004_UnsafeCode.idr
 SoundnessPA004 : (file : String) -> (loc : Loc)
               -> contains (stripStrings file) "unsafe " loc
               -> isUnsafeBlock (locate file loc)
@@ -266,7 +266,7 @@
 |===
 |# |Phase |Output |Estimated effort |Risk
 |1 |*Foundation*: Layer 1.0 (comment/string-strip idempotence + token
-preservation) |`+src/abi/Stripping.idr+` + 1 Idris2 module |3–5 days
+preservation) |`+src/abi/PanicAttack/ABI/Stripping.idr+` + 1 Idris2 module |3–5 days
 |low
 
 |2 |*Quick wins*: Hexad↔Octad roundtrip proptest + Layer 1
@@ -316,8 +316,8 @@
 
 * `+PROOF-NEEDS.md+` — current proof-debt ledger (this document is the
 long-term plan; that one tracks the immediate next step).
-* `+src/abi/PatternCompleteness.idr+` (PA1)
-* `+src/abi/ClassificationSoundness.idr+` (PA2)
+* `+src/abi/PanicAttack/ABI/PatternCompleteness.idr+` (PA1)
+* `+src/abi/PanicAttack/ABI/ClassificationSoundness.idr+` (PA2)
 * `+hyperpolymath/proven+` — leaf validator library; cross-fit
 candidates listed above.
 * ROADMAP.adoc "`Long-Term`" section: "`Formal verification of core

src/abi/panic-attack-abi.ipkg

@@ -0,0 +1,15 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+-- The Idris2 ABI models and proofs. Type-check with:
+--   idris2 --typecheck src/abi/panic-attack-abi.ipkg
+-- A pass is exit 0 and no `Error:` line in the output.
+package panic-attack-abi
+
+sourcedir = "."
+
+modules = PanicAttack.ABI.Types
+        , PanicAttack.ABI.PatternCompleteness
+        , PanicAttack.ABI.ClassificationSoundness
+        , PanicAttack.ABI.Stripping
+        , PanicAttack.ABI.AttestationUnforgeability