From 1af31905f1b3e13dae87b38509b9ad358418ff10 Mon Sep 17 00:00:00 2001
From: Claude <noreply@anthropic.com>
Date: Sat, 27 Jun 2026 19:04:50 +0000
Subject: [PATCH] ci(a-sounder-constitution): gate the Idris2 proof with
 `idris2 --check`
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Add .github/workflows/idris2-proof.yml: builds Idris2 0.7.0 (Chez Scheme
backend) and runs `idris2 --check a-sounder-constitution/formal/Constitution.idr`
on every change under `formal/`. The certificate shipped once without being
machine-checked and did not actually compile (#45); this gate stops the proof
from drifting out of sync with its claims again.

- Path-filtered to `formal/**` + the workflow file, so it only runs when the
  proof changes (keeps Actions burn low — no caching, builds from source).
- Passes the repo's workflow-linter rules: SPDX header, top-level
  `permissions: contents: read`, SHA-pinned actions, concurrency guardrail.
- formal/README.adoc: note that CI now enforces the check.

Verified locally: YAML parses, all linter rules pass, and
`idris2 --check Constitution.idr` exits 0 under Idris2 0.7.0.

Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6
---
 .github/workflows/idris2-proof.yml        | 65 +++++++++++++++++++++++
 a-sounder-constitution/formal/README.adoc | 13 +++--
 2 files changed, 74 insertions(+), 4 deletions(-)
 create mode 100644 .github/workflows/idris2-proof.yml

diff --git a/.github/workflows/idris2-proof.yml b/.github/workflows/idris2-proof.yml
new file mode 100644
index 0000000..3579c52
--- /dev/null
+++ b/.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)"
diff --git a/a-sounder-constitution/formal/README.adoc b/a-sounder-constitution/formal/README.adoc
index 0a6a2a5..705e92a 100644
--- a/a-sounder-constitution/formal/README.adoc
+++ b/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: