ci: wire the formal/ Coq proof gate into CI (Refs #513)

[hyperpolymath]

Why

formal/ contains 20 machine-checked Coq/Rocq proofs, and formal/justfile
already implements a real, fail-closed check over them. No workflow ever
invoked it — grep for coq/rocq across .github/workflows/ returned nothing,
so the entire corpus was unchecked in CI.

This is the inverse of the usual fake-gate problem: the assurance already
existed and was simply being thrown away.

Verified before wiring

Ran the existing formal/justfile check locally with coqc 8.20.1:

• all 20 files check clean
• every Print Assumptions reports Closed under the global context — the
  strongest result, meaning no dependency on anything outside the kernel
• the justfile's own assertion fires: "OK: K-1/K1Let/F-1 + P-2/P-3/F-3/F-4
  mechanised; no axioms."
• only deprecation warnings (app_length, from the 8.18→8.20 skew), no errors

Note formal/README.adoc documents Coq/Rocq 8.18; the container here is
8.20, on which the corpus was confirmed to pass.

Design

Fail-closed by construction. The gate does not probe for the prover and
skip when absent. The pinned container guarantees coqc, so a missing prover is
an infrastructure failure, not a silent pass.

No duplicated proof list. formal/justfile stays the single source of truth
for the list and its dependency order; the workflow parses it rather than
re-stating it. A completeness guard fails the run if any formal/*.v on disk is
not named there — so adding a proof without wiring it cannot silently go
unchecked.

Falsifier-tested

Both guards were proven to actually fire, not merely to pass:

Falsifier	Result
Add an unwired formal/ZZ_Falsifier.v	guard fires, run fails
Add a theorem proved via Axiom cheat	Print Assumptions emits Axioms:, grep catches it, run fails

Notes

• Container pinned by digest (coqorg/coq@sha256:e50d77c4…)
• actions/checkout SHA-pinned to match repo convention
• SPDX header on line 1 and permissions: at column 0, per workflow-linter.yml
• A cold full run takes over 2 minutes locally, hence timeout-minutes: 30

Draft — this is the first time these proofs will run in CI.

🤖 Generated with Claude Code

[gitar-bot]

Note

Automatic reviews are paused because your trial's included automatic processing has been used for this period. Upgrade now, or comment "Gitar review" to run a review anytime.
Learn more

Code Review ✅ Approved 2 resolved / 2 findings

Integrates the Coq proof gate into CI with digest pinning and strict verification guards, but a malformed sed expression breaks proof parsing and the axiom check requires explicit Print Assumptions statements.

✅ 2 resolved

✅ Bug: Malformed sed expression makes proof-list parse step always fail

📄 .github/workflows/coq-proof-gate.yml:48-57
The pipeline sed 's/.*for f in //; s/; do.*//; s/\//g' aborts on GNU sed 4.9 (the sed shipped in the coqorg/coq container): the final s/\//g errors with "unterminated s command". Under set -euo pipefail the failed pipeline fails the command substitution and the step exits 1 on every run, so the gate never reaches the actual proof-checking steps and is permanently red on any PR touching formal/. I reproduced this with the exact YAML script; the empty-list guard is never reached. Strip the line-continuation backslashes with tr -d instead of a sed backslash substitution (verified to parse all 20 proofs).

✅ Edge Case: Axiom rejection only works for files containing Print Assumptions

📄 .github/workflows/coq-proof-gate.yml:89-95
The gate detects axioms/Admitted by grepping coqc stdout for Axioms:, which coqc only emits for files that contain a Print Assumptions command. Two of the 20 proofs (Siblings_Stated.v, QttSemiring.v) contain no Print Assumptions, so an Axiom/Admitted introduced in such a file (or any newly added proof lacking the directive) would pass silently, weakening the PR's "reject any axiom / Admitted" guarantee. Consider guarding that each listed proof contains a Print Assumptions line, or asserting the expected Closed under the global context marker appears for every proof.

Options

Display: compact → Showing less information.

Comment with these commands to change the behavior for this request:

Compact

gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}

[sonarqubecloud]

Quality Gate failed

Failed conditions
C Security Rating on New Code (required ≥ A)

See analysis details on SonarQube Cloud

Catch issues before they fail your Quality Gate with our IDE extension SonarQube for IDE