From 11b5e8a8785d92fcd8efe448ed082012d3d72af9 Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Tue, 28 Jul 2026 19:23:11 +0100
Subject: [PATCH] ci: wire the formal/ Coq proof gate into CI (Refs #513)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`formal/` holds 20 machine-checked Coq/Rocq proofs and `formal/justfile`
already implements a real, fail-closed check over them — but no workflow
ever invoked it, so the corpus was unchecked in CI.

Verified locally with coqc 8.20.1 before wiring: all 20 files check clean,
every `Print Assumptions` reports "Closed under the global context", and the
justfile's own assertion fires ("no axioms"). Deprecation warnings for
`app_length` only (8.18 -> 8.20 skew), no errors.

The gate is deliberately fail-closed: it does not probe for the prover and
skip when absent. The pinned container guarantees `coqc`, so a missing prover
is an infrastructure failure rather than a silent pass.

`formal/justfile` stays the single source of truth for the proof list and its
dependency order; the workflow parses that list instead of duplicating it, and
fails if any `formal/*.v` on disk is not named there — so adding a proof
without wiring it cannot go unnoticed.

Both guards were falsifier-tested locally:
  - an unwired `formal/*.v` is detected and fails the run
  - an `Axiom`-dependent theorem is caught by the "Axioms:" grep

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
---
 .github/workflows/coq-proof-gate.yml | 96 ++++++++++++++++++++++++++++
 1 file changed, 96 insertions(+)
 create mode 100644 .github/workflows/coq-proof-gate.yml

diff --git a/.github/workflows/coq-proof-gate.yml b/.github/workflows/coq-proof-gate.yml
new file mode 100644
index 00000000..819414ae
--- /dev/null
+++ b/.github/workflows/coq-proof-gate.yml
@@ -0,0 +1,96 @@
+# SPDX-License-Identifier: MPL-2.0
+# Coq/Rocq proof gate for the `formal/` mechanised-metatheory track (issue #513).
+#
+# This gate is deliberately FAIL-CLOSED. It does NOT probe for the prover and
+# skip when absent — the container guarantees `coqc` exists, so a missing
+# prover is an infrastructure failure, not a silent pass.
+#
+# `formal/justfile` remains the single source of truth for the proof list and
+# its dependency order; this workflow parses that list rather than duplicating
+# it, and fails if any `formal/*.v` on disk is not named there.
+name: Coq Proof Gate
+on:
+  pull_request:
+    paths:
+      - 'formal/**'
+      - '.github/workflows/coq-proof-gate.yml'
+  push:
+    branches: [main]
+    paths:
+      - 'formal/**'
+      - '.github/workflows/coq-proof-gate.yml'
+  workflow_dispatch:
+permissions: read-all
+concurrency:
+  group: ${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+jobs:
+  coq-proofs:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    container:
+      # coqorg/coq:8.20 — pinned by digest. `formal/README.adoc` documents 8.18;
+      # the corpus was verified to check clean on 8.20.1 (deprecation warnings
+      # for `app_length` only, no errors).
+      image: coqorg/coq@sha256:e50d77c4c5a9aa0d76ae1b343d79c5f922da3a75054b79c5dc635895438e4674
+      options: --user root
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+
+      - name: Record prover version
+        run: coqc --version
+
+      - name: Extract the ordered proof list from formal/justfile
+        id: list
+        run: |
+          set -euo pipefail
+          cd formal
+          list="$(sed -n '/for f in /,/; do/p' justfile \
+                  | tr '\n' ' ' \
+                  | sed 's/.*for f in //; s/; do.*//; s/\\//g' \
+                  | tr -s ' ')"
+          if [ -z "${list// /}" ]; then
+            echo "::error::could not parse the proof list out of formal/justfile"
+            exit 1
+          fi
+          echo "count=$(printf '%s' "$list" | wc -w)"
+          echo "list=$list" >> "$GITHUB_OUTPUT"
+
+      - name: Guard — every formal/*.v must be wired into the gate
+        env:
+          LIST: ${{ steps.list.outputs.list }}
+        run: |
+          set -euo pipefail
+          cd formal
+          missing=0
+          for f in *.v; do
+            b="${f%.v}"
+            case " $LIST " in
+              *" $b "*) ;;
+              *) echo "::error file=formal/$f::proof file is not listed in formal/justfile — it would never be checked"; missing=1 ;;
+            esac
+          done
+          [ "$missing" -eq 0 ] || exit 1
+          echo "all on-disk proofs are wired into the gate"
+
+      - name: Type-check every proof and reject any axiom / Admitted
+        env:
+          LIST: ${{ steps.list.outputs.list }}
+        run: |
+          set -euo pipefail
+          cd formal
+          all=""
+          for f in $LIST; do
+            echo "== coqc $f.v =="
+            o="$(coqc -Q . ASFormal "$f.v")"
+            printf '%s\n' "$o"
+            all+="$o"$'\n'
+          done
+          # `Print Assumptions` emits "Axioms:" when a theorem depends on an
+          # axiom or an `Admitted` proof; "Closed under the global context"
+          # is the clean result.
+          if printf '%s' "$all" | grep -q "Axioms:"; then
+            echo "::error::a proof depends on an axiom / Admitted"
+            exit 1
+          fi
+          echo "OK: all proofs mechanised; no axioms."