fix(abi): type-check the Idris2 proofs in CI and re-prove line-comment stripping

.github/workflows/proven-tests.yml

@@ -22,6 +22,12 @@
 #   and it would make every contributor wait on a compiler that cannot change
 #   for them.
 #
+# `idris-abi` (every PR, blocking): type-checks this repo's own Idris2 ABI
+#   proofs in src/abi/. This is a departure from the rule above, made because
+#   these proofs are claims in PROOF-NEEDS.adoc and a claim needs a receipt on
+#   every change. Idris2 is built from source once and cached by version and
+#   commit, so after the first run a PR waits only for the check itself.
+#
 # 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.
@@ -191,3 +197,54 @@ jobs:
           path: .proven-tests/build/report/*.json
           retention-days: 30
           if-no-files-found: warn
+
+  # The Idris2 ABI proofs in src/abi/ (PA1, PA2, Layer 1.0 stripping,
+  # attestation unforgeability, ABI types). Until this job, none was ever
+  # type-checked. scripts/ci/check-idris-abi.sh fails on any type error,
+  # a missing `%default total`, or an escape hatch.
+  #
+  # Deviation (PROOF-POLICY §6), state: open. Leg: Idris2 ABI proofs. Tool:
+  # Idris2 0.7.0 built from the v0.7.0 tag (commit checked below) with the
+  # runner's Chez Scheme. Why not Guix or the container: panic-attack's Guix
+  # manifest and container do not provide Idris2 yet.
+  idris-abi:
+    name: Idris2 ABI proofs type-check
+    runs-on: ubuntu-latest
+    timeout-minutes: 45
+    env:
+      IDRIS2_COMMIT: 27780073c8631826d846499840b3857d9b9a4fd5
+    steps:
+      - name: Checkout this repository
+        uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1  # v7.0.1
+        with:
+          persist-credentials: false
+
+      - name: Cache the Idris2 toolchain built from source
+        id: idris2-cache
+        uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9  # v6.1.0
+        with:
+          path: ~/.idris2-src-build
+          key: idris2-src-${{ env.IDRIS2_VERSION }}-${{ env.IDRIS2_COMMIT }}-${{ runner.os }}
+
+      - name: Build Idris2 from the pinned tag (cache miss only)
+        if: steps.idris2-cache.outputs.cache-hit != 'true'
+        shell: bash
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y -qq chezscheme
+          src=$(mktemp -d)
+          git clone --quiet --depth 1 --branch "v${IDRIS2_VERSION}" \
+            https://github.com/idris-lang/Idris2.git "$src"
+          test "$(git -C "$src" rev-parse HEAD)" = "$IDRIS2_COMMIT"
+          make -C "$src" bootstrap SCHEME=scheme PREFIX="$HOME/.idris2-src-build"
+          make -C "$src" install PREFIX="$HOME/.idris2-src-build"
+
+      - name: Type-check every module in src/abi
+        shell: bash
+        run: |
+          set -euo pipefail
+          # The cached build still needs Chez Scheme at run time.
+          command -v scheme >/dev/null || { sudo apt-get update -qq && sudo apt-get install -y -qq chezscheme; }
+          export PATH="$HOME/.idris2-src-build/bin:$PATH"
+          bash scripts/ci/check-idris-abi.sh

CHANGELOG.adoc

@@ -2,6 +2,24 @@
 
 === [Unreleased]
 
+==== Fixed — the Idris2 ABI proofs are type-checked, and the stripping proof is re-proved
+
+* No CI job had ever type-checked `+src/abi/+`, and as committed none of its
+five modules checked. A new `+idris-abi+` job (`+proven-tests.yml+`, using
+`+scripts/ci/check-idris-abi.sh+`) now checks all five on every PR with Idris2
+0.7.0. It fails on a type error, on a missing `+%default total+`, or on
+`+believe_me+`, `+assert_total+`, `+assert_smaller+`, `+postulate+` or
+`+idris_crash+`.
+* `+Stripping.idr+`: the 2026-06-02 proof of `+stripLineCommentsIdempotent+`
+never type-checked, so it is re-proved through two facts: stripping is the
+identity on text with no `+//+`, and the strippers' output has no `+//+`. The
+strippers are restated with explicit `+Bool+` tests. An exhaustive run over
+29,524 inputs shows they behave exactly as before.
+* `+Types.idr+`: adds the missing `+Eq Severity+` that `+Ord+` needs, and fixes
+the `+LangId+` declaration syntax.
+* `+PROOF-NEEDS.adoc+` and `+EXPLAINME.adoc+` now say that the earlier claims had
+no receipt.
+
 ==== Added — `+assail --output-format kyaml+` writes a KYAML copy
 
 * With `+--output-format kyaml+` and `+--output report.json+`, `+assail+` writes

EXPLAINME.adoc

@@ -54,7 +54,7 @@ The README makes claims. This file backs them up.
 | `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/Stripping.idr` | Layer 1.0 — line-comment stripping is idempotent (`stripLineCommentsIdempotent`; re-proved 2026-11-09, type-checked by the `idris-abi` CI job)
 | `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

@@ -2,12 +2,23 @@
 
 === Current State
 
+*Receipts (2026-11-09).* Until this date no CI job type-checked
+`+src/abi/+`, and as committed none of the five modules checked: their module
+names did not match their paths, `+Types.idr+` and `+Stripping.idr+` had syntax
+errors, and `+Stripping.idr+`'s main theorem did not type-check at all. The ✅
+marks below therefore had no receipt before that date. Each module is now
+checked on every PR by the `+idris-abi+` job in
+`+.github/workflows/proven-tests.yml+` (`+scripts/ci/check-idris-abi.sh+`, Idris2
+0.7.0, `+%default total+`, no `+believe_me+`, `+assert_total+`,
+`+assert_smaller+`, `+postulate+` or `+idris_crash+`). PROOF-POLICY §6 deviation,
+state open: Idris2 is built from its v0.7.0 tag, because the repo's Guix
+manifest and container do not provide it.
+
 * **src/abi/*.idr**: 5 files — `+Types.idr+`,
 `+PatternCompleteness.idr+` (PA1 ✅ 2026-04-11),
 `+ClassificationSoundness.idr+` (PA2 ✅ 2026-04-11), `+Stripping.idr+`
-(PROOF-PROGRAMME Layer 1.0 line-comment slice ✅ 2026-06-02 —
-multi-comment semantics + slash-slash closure both Qed via
-mutual-recursive `+bodyIsFixedPoint+`),
+(PROOF-PROGRAMME Layer 1.0 line-comment slice: claimed 2026-06-02 but
+never checked; re-proved and checked 2026-11-09),
 `+AttestationUnforgeability.idr+` (PROOF-PROGRAMME §3.2 ✅ 2026-06-04 —
 conditional unforgeability from Ed25519 EUF-CMA + chain-hash
 collision-resistance hypotheses)
@@ -34,15 +45,19 @@ top-level theorem.
 preserves the ordering.
 
 |Layer 1.0 line-comment idempotence |`+src/abi/Stripping.idr+`
-|*2026-06-02 close-out (issue #113)*: corrects PR #111’s single-comment
-model to multi-comment via mutual recursion
-(`+stripLineComments ↔ stripLineCommentBody+` — body calls back into
-main after each preserved newline). Qed-closes
-`+stripLineCommentsIdempotent+` for ALL cases including the slash-slash
-inductive via the load-bearing `+bodyIsFixedPoint+` lemma proved by
-mutual induction with the main theorem. 7 sanity-check theorems
-including the two-comments-on-different-lines case PR #111 silently
-mis-stripped.
+|*Re-proved 2026-11-09.* The 2026-06-02 proof (issue #113) never
+type-checked: its `+//+` case relied on reductions that do not hold for a
+variable character, and it used `+decEq+` without importing it. The new proof
+shows `+stripLineCommentsIdempotent+` (stripping twice equals stripping once)
+through two facts: stripping is the identity on text with no `+//+`
+(`+stripIsIdOnClean+`), and the strippers' output has no `+//+`
+(`+stripIsClean+`/`+bodyIsClean+`, by mutual induction). `+bodyIsFixedPoint+`
+follows. The strippers are restated with explicit `+Bool+` tests. An
+exhaustive differential run over every string of length up to 9 on
+`+{/, x, \n}+` (29,524 inputs) found no difference from the previous
+definitions. A mutant that blanks with `+/+` instead of a space is rejected.
+Nine closed sanity theorems, including two comments on different lines and
+`+///+`.
 
 |Attestation chain unforgeability
 |`+src/abi/AttestationUnforgeability.idr+` |*PROOF-PROGRAMME §3.2

scripts/ci/check-idris-abi.sh

@@ -0,0 +1,68 @@
+#!/usr/bin/env bash
+# SPDX-License-Identifier: MPL-2.0
+# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+#
+# Type-check every Idris2 module in src/abi/ and fail loudly on any error or
+# escape hatch. This is the receipt for the ABI proofs listed in
+# PROOF-NEEDS.adoc: until this ran, none of them had ever been checked.
+#
+# The files declare `module PanicAttack.ABI.<Name>` but live flat in
+# src/abi/, and Idris2 requires a module's path to match its name. Moving
+# them would break paths cited in legacy A2ML metadata, which agents may not
+# edit, so this script stages a module-path view of the unchanged files as
+# symbolic links and checks that. The bytes checked are the committed bytes.
+#
+# Requirements per module:
+#   * `idris2 --check` succeeds under the pinned Idris2 version;
+#   * the file states `%default total`;
+#   * no believe_me, assert_total, assert_smaller, postulate or idris_crash
+#     outside comments.
+#
+# Usage: scripts/ci/check-idris-abi.sh   (idris2 0.7.0 on PATH)
+set -euo pipefail
+
+IDRIS2_VERSION=0.7.0
+root=$(cd "$(dirname "$0")/../.." && pwd)
+abi="$root/src/abi"
+
+version=$(idris2 --version)
+[[ "$version" == "Idris 2, version $IDRIS2_VERSION"* ]] ||
+    { echo "check-idris-abi: need Idris2 $IDRIS2_VERSION, got: $version" >&2; exit 2; }
+
+stage=$(mktemp -d)
+trap 'rm -rf "$stage"' EXIT
+mkdir -p "$stage/PanicAttack/ABI"
+
+failures=0
+shopt -s nullglob
+files=("$abi"/*.idr)
+[[ ${#files[@]} -gt 0 ]] || { echo "check-idris-abi: no modules in $abi" >&2; exit 2; }
+
+for file in "${files[@]}"; do
+    name=$(basename "$file" .idr)
+    declared=$(sed -n 's/^module[[:space:]]\{1,\}\([A-Za-z0-9_.]*\).*/\1/p' "$file" | head -1)
+    if [[ "$declared" != "PanicAttack.ABI.$name" ]]; then
+        echo "FAIL  $name: declares module '$declared', expected PanicAttack.ABI.$name"
+        failures=$((failures + 1)); continue
+    fi
+    ln -s "$file" "$stage/PanicAttack/ABI/$name.idr"
+done
+
+for file in "${files[@]}"; do
+    name=$(basename "$file" .idr)
+    [[ -L "$stage/PanicAttack/ABI/$name.idr" ]] || continue
+    # Code lines only: drop `--` and `|||` comment lines before searching.
+    code=$(grep -vE '^[[:space:]]*(--|\|\|\|)' "$file" || true)
+    if ! grep -qE '^%default[[:space:]]+total' <<<"$code"; then
+        echo "FAIL  $name: missing %default total"; failures=$((failures + 1)); continue
+    fi
+    if hatch=$(grep -nE '\b(believe_me|assert_total|assert_smaller|postulate|idris_crash)\b' <<<"$code"); then
+        echo "FAIL  $name: escape hatch: $hatch"; failures=$((failures + 1)); continue
+    fi
+    if out=$(cd "$stage" && idris2 --no-color --check "PanicAttack/ABI/$name.idr" 2>&1); then
+        echo "PASS  $name"
+    else
+        echo "FAIL  $name"; printf '%s\n' "$out" | sed -n '1,40p'; failures=$((failures + 1))
+    fi
+done
+exit "$failures"