ci(a-sounder-constitution): gate the Idris2 proof with idris2 --check

.github/workflows/idris2-proof.yml

@@ -0,0 +1,65 @@
+# SPDX-License-Identifier: MPL-2.0
+# Idris2 proof check — type-checks the a-sounder-constitution formal certificate
+# (formal/Constitution.idr) so the "rights are type constraints on legal state
+# transitions" claim cannot silently rot. The proof shipped once without being
+# machine-checked and did not actually compile (see #45); this gate prevents a
+# repeat. Path-filtered to the proof + this workflow to keep Actions burn low.
+name: Idris2 Proof
+
+on:
+  push:
+    branches: [main, master]
+    paths:
+      - 'a-sounder-constitution/formal/**'
+      - '.github/workflows/idris2-proof.yml'
+  pull_request:
+    paths:
+      - 'a-sounder-constitution/formal/**'
+      - '.github/workflows/idris2-proof.yml'
+  workflow_dispatch:
+
+# Estate guardrail: one run per ref, cancel superseded runs. Read-only check.
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
+permissions:
+  contents: read
+
+env:
+  IDRIS2_VERSION: "0.7.0"
+
+jobs:
+  idris2-check:
+    runs-on: ubuntu-latest
+    timeout-minutes: 20
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
+
+      - name: Install Chez Scheme (Idris2 backend)
+        run: |
+          set -euo pipefail
+          sudo apt-get update -qq
+          sudo apt-get install -y --no-install-recommends chezscheme libgmp-dev
+
+      - name: Build & install Idris2 ${{ env.IDRIS2_VERSION }}
+        run: |
+          set -euo pipefail
+          tarball="idris2-${IDRIS2_VERSION}.tar.gz"
+          curl -fsSL -o "$tarball" \
+            "https://codeload.github.com/idris-lang/Idris2/tar.gz/refs/tags/v${IDRIS2_VERSION}"
+          tar xzf "$tarball"
+          cd "Idris2-${IDRIS2_VERSION}"
+          make bootstrap SCHEME=chezscheme
+          make install SCHEME=chezscheme
+          echo "${HOME}/.idris2/bin" >> "$GITHUB_PATH"
+
+      - name: Type-check the constitutional proof
+        run: |
+          set -euo pipefail
+          idris2 --version
+          idris2 --check a-sounder-constitution/formal/Constitution.idr
+          echo "formal/Constitution.idr type-checks (exit 0)"

a-sounder-constitution/formal/README.adoc

@@ -54,10 +54,15 @@ downstream of exactly this one distinction. The JS side is exercised by
 
 [NOTE]
 ====
-*Machine-checked.* This module type-checks cleanly under *Idris2 0.7.0* with
-`%default total` and zero `believe_me` / `assert_total` / `postulate` (verified
-2026-06-27). The `Reflexive`-interface dependency for `LTE` is avoided by
-inlining a small `lteRefl` lemma, so the module needs only `import Data.Nat`.
+*Machine-checked, and enforced in CI.* This module type-checks cleanly under
+*Idris2 0.7.0* with `%default total` and zero `believe_me` / `assert_total` /
+`postulate` (verified 2026-06-27). The `Reflexive`-interface dependency for
+`LTE` is avoided by inlining a small `lteRefl` lemma, so the module needs only
+`import Data.Nat`.
+
+CI runs `idris2 --check` on every change under `formal/` via
+`.github/workflows/idris2-proof.yml`, so the proof can no longer drift out of
+sync with its claims without going red.
 ====
 
 To reproduce: