Skip to content

Commit 707fd5f

Browse files
hyperpolymathhyperpolymath
authored
docs: record the Coq proof gate and the 2026-07-29 rescue session (#712)
Documentation of the state established on 2026-07-29, in both human- and machine-readable form, using conventions already present in the repo. ## `docs/ci/COQ-PROOF-GATE.adoc` Sits beside the existing `docs/ci/required-checks.adoc`. Covers: - what the gate checks, and that all 20 proofs report `Closed under the global context` - **why it is fail-closed** — and why `tools/check-proofs.sh` is explicitly *not* a model to copy: it gates Idris2/Lean/Agda behind `command -v … || SKIP` and exits `0` on a machine with no provers at all - why `formal/justfile` stays the single source of truth for the proof list - the **two container faults** that each cost a red run, both properties of `coqorg/*` images under GitHub Actions that will recur on any new Coq job: the overridden `ENTRYPOINT`, and the silent fallback to `sh`/dash - how to run it locally, and the falsifiers proving both guards can actually fail ## `.machine_readable/sessions/2026-07-29-proof-gate-and-rescue.a2ml` Session record on the existing `a2ml/session-record/v1` schema, alongside the `2026-05-27` entry. Verified to parse as TOML. Records the gate, the rescue of three feature commits from a checkout that was deleted mid-session, three pieces of sweep damage, the partial-merge incident that left `main` red, and method notes worth not re-deriving. ## `formal/README.adoc` Notes that CI gates on **8.20.1** while the file documents **8.18**, that the corpus checks clean on 8.20, and that reconciling the two is outstanding. ## Not touched `STATE.a2ml` was deliberately left alone — it is 67KB, self-describes as stale and as mirroring rather than leading. A session record is the correct home for this. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
2 parents 7f6cb79 + f4cd3af commit 707fd5f

3 files changed

Lines changed: 281 additions & 0 deletions

File tree

‎.machine_readable/sessions/2026-07-29-proof-gate-and-rescue.a2ml‎

Lines changed: 143 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,143 @@
1+
# SPDX-License-Identifier: MPL-2.0
2+
# SPDX-FileCopyrightText: 2026 hyperpolymath
3+
#
4+
# Session record — 2026-07-29 — Coq proof gate wired + stranded work rescued
5+
#
6+
# Human-readable companions:
7+
# docs/ci/COQ-PROOF-GATE.adoc (the gate: design, gotchas, falsifiers)
8+
# dev-notes/affinescript-sitrep-2026-07-29.md (estate-local, not in this repo)
9+
10+
[metadata]
11+
schema = "a2ml/session-record/v1"
12+
session-date = "2026-07-29"
13+
session-topic = "wire the formal/ Coq proof gate into CI; rescue feature work from a deleted checkout"
14+
repo = "hyperpolymath/affinescript"
15+
human-companion = "docs/ci/COQ-PROOF-GATE.adoc"
16+
prs = [708, 709, 711]
17+
18+
# ── Outcome 1: the Coq proof gate ──────────────────────────────────────
19+
# 20 machine-checked proofs existed in formal/ with a real fail-closed
20+
# runner in formal/justfile, but NO workflow invoked them. Now gated.
21+
22+
[proof-gate]
23+
workflow = ".github/workflows/coq-proof-gate.yml"
24+
corpus-path = "formal/"
25+
corpus-size = 20
26+
source-of-truth = "formal/justfile"
27+
list-parsed-not-copied = true
28+
fail-closed = true
29+
prover-in-ci = "8.20.1"
30+
prover-documented = "8.18"
31+
prover-pin-reconciled = false
32+
container-digest = "sha256:e50d77c4c5a9aa0d76ae1b343d79c5f922da3a75054b79c5dc635895438e4674"
33+
all-proofs-axiom-free = true
34+
assumptions-result = "Closed under the global context"
35+
tracking-issue = 513
36+
37+
[[proof-gate.falsifier]]
38+
id = "unwired-proof-file"
39+
method = "add formal/ZZ_Falsifier.v not named in formal/justfile"
40+
fires = true
41+
guards = "completeness"
42+
43+
[[proof-gate.falsifier]]
44+
id = "axiom-dependent-theorem"
45+
method = "prove a goal via `Axiom cheat : forall P : Prop, P`"
46+
fires = true
47+
guards = "Print Assumptions / grep Axioms:"
48+
49+
# Two container faults, each cost one red CI run. Both are properties of
50+
# coqorg/* images under GitHub Actions and will recur on any new Coq job.
51+
52+
[[proof-gate.gotcha]]
53+
id = "entrypoint-overridden"
54+
symptom = "coqc: not found"
55+
cause = "coqorg installs Coq into the `coq` user's opam switch and exposes it via ENTRYPOINT; GitHub Actions overrides the entrypoint for job containers"
56+
remedy = "add /home/coq/.opam/*/bin to GITHUB_PATH, globbed not hard-coded, failing loudly if absent"
57+
58+
[[proof-gate.gotcha]]
59+
id = "shell-fell-back-to-dash"
60+
symptom = "set: Illegal option -o pipefail"
61+
cause = "GitHub used `sh -e {0}` despite the image shipping bash 5.2"
62+
remedy = "declare defaults.run.shell: bash explicitly"
63+
64+
# ── Outcome 2: rescue of stranded work ─────────────────────────────────
65+
# An estate reorg renamed the working checkout to *.DUPLICATE-superseded-*
66+
# and then DELETED it mid-session. It held 9 commits present nowhere else.
67+
# The rename judged duplicates by directory identity, not by git rev-list.
68+
69+
[rescue]
70+
trigger = "checkout renamed *.DUPLICATE-superseded-2026-07-27 then deleted mid-session"
71+
misjudgement = "duplicate decided by directory identity rather than `git rev-list` — the directory marked superseded held 9 unpushed commits; the one kept held 0"
72+
estate-wide = "the same rename was reported backwards in all 8 affected repos"
73+
commits-at-risk = 9
74+
commits-recovered-to-main = 3
75+
recovered-via = "git bundle taken before deletion"
76+
cherry-pick-needed = false
77+
cherry-pick-avoided-because = "the 3 feature commits were a contiguous linear chain whose base parent was origin/main, so branching preserved original SHAs, authorship and dates"
78+
pr = 708
79+
80+
[[rescue.commit]]
81+
sha = "220d7ca"
82+
kind = "feature"
83+
subject = "docs: resolve INT-02 satellite scope deferral"
84+
closes = 489
85+
86+
[[rescue.commit]]
87+
sha = "70ca15e"
88+
kind = "feature"
89+
subject = "feat(dom): browser host parity execution harness (INT-11)"
90+
91+
[[rescue.commit]]
92+
sha = "e959636"
93+
kind = "feature"
94+
subject = "feat(cadre): scaffold router navigation runtime wrapper (INT-09)"
95+
96+
# ── Outcome 3: sweep damage found and reverted (uncommitted only) ──────
97+
98+
[[sweep-damage]]
99+
id = "gitattributes-language-declaration-deleted"
100+
file = ".gitattributes"
101+
detail = "the uncommitted tree deleted `*.affine text eol=lf linguist-language=AffineScript` — the single line making GitHub recognise 493 .affine files as the project's own language, and enforcing LF on them"
102+
state = "reverted-in-working-tree"
103+
severity = "high"
104+
advice = "never `git commit -a` in this repo while an estate sweep is active"
105+
106+
[[sweep-damage]]
107+
id = "gitignore-foreign-template-entries"
108+
file = ".gitignore"
109+
detail = "11 additions from another repo's template: composer/*.beam, composer/build/, /target/, *.db*, .cache/, /exports/*. Neither composer/ nor target/ exists; ai-cli-crash-capture/ is TRACKED (5 files) so ignoring it is a no-op"
110+
state = "reverted-in-working-tree"
111+
severity = "low"
112+
113+
[[sweep-damage]]
114+
id = "patch-ecosystem-py-escape-corruption"
115+
file = "docs/patch_ecosystem.py"
116+
detail = "arrived via the `merge rogue duplicate repository` commit. Its search strings contain literal BEL/TAB/CR/BS where \\a \\t \\r \\b were interpreted by a non-raw Python string — `affinescript` reads as `ffinescript`, `readBytes` as `eadBytes`. The strings can never match the file, so the script runs, exits 0, and changes nothing"
117+
state = "still-present-on-main"
118+
severity = "medium"
119+
fingerprint = "a leading letter missing after a would-be backslash escape; grep the estate for this shape — it produces scripts that appear to succeed"
120+
121+
# ── Outcome 4: main was left red by a partial merge ────────────────────
122+
123+
[incident-partial-merge]
124+
pr-that-broke-main = 709
125+
detail = "PR #709 squash-merged the pre-fix revision of the workflow; the verified fix (af7c38c) was on the branch but not in the squash, so main received a gate that fails with `coqc: not found`"
126+
red-since = "ed4e223"
127+
repair-pr = 711
128+
repair-verified = "workflow_dispatch green on the branch: 20/20 proofs, completeness guard passed, no axioms"
129+
lesson = "after a squash merge, re-check that the merged tree contains the fix — a green PR check can belong to a superseded commit"
130+
131+
# ── Method notes worth not re-deriving ─────────────────────────────────
132+
133+
[[method-note]]
134+
id = "always-fetch-before-judging-divergence"
135+
detail = "a stale remote-tracking ref reported `ahead 16`; after `git fetch` the true figure was 9. Origin had already absorbed 7 via PRs."
136+
137+
[[method-note]]
138+
id = "a-red-run-is-not-a-red-branch"
139+
detail = "resolve which commit a CI run belongs to before calling a branch red; a failure observed in a stale duplicate checkout belonged to a superseded commit while main was green."
140+
141+
[[method-note]]
142+
id = "bundle-verify-is-not-restore"
143+
detail = "`git bundle verify` proves internal consistency, not that the bundle restores what you wanted. Clone it and assert the expected SHA."

‎docs/ci/COQ-PROOF-GATE.adoc‎

Lines changed: 125 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,125 @@
1+
// SPDX-License-Identifier: CC-BY-SA-4.0
2+
// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath)
3+
= The Coq Proof Gate
4+
:toc: left
5+
:toclevels: 3
6+
7+
Workflow: `.github/workflows/coq-proof-gate.yml` +
8+
Proof corpus: `formal/` (20 `.v` files) +
9+
Local runner: `formal/justfile` (`just check`) +
10+
Tracking issue: #513 (umbrella), #514–#521 (individual obligations)
11+
12+
== What it does
13+
14+
Type-checks every Coq/Rocq proof in `formal/` and **fails if any theorem
15+
depends on an axiom or an `Admitted` proof**.
16+
17+
This is the mechanised half of the proof programme catalogued in
18+
`docs/PROOF-NEEDS.adoc`. Until 2026-07-29 the corpus existed and checked
19+
clean, but **no workflow invoked it** — a `grep` for coq/rocq across
20+
`.github/workflows/` returned nothing. The proofs were real; the assurance
21+
was simply being discarded.
22+
23+
== Design decisions
24+
25+
=== It is fail-closed
26+
27+
The gate does *not* probe for the prover and skip when it is absent. The
28+
pinned container guarantees `coqc`, so a missing prover is an infrastructure
29+
failure, not a silent pass.
30+
31+
This matters because the sibling script `tools/check-proofs.sh` takes the
32+
opposite approach for Idris2/Lean/Agda — it gates each on
33+
`command -v … || { note "SKIP"; return; }` and exits `0` with zero provers
34+
present. That script reports "N passed, N failed, N skipped" and is green on a
35+
machine with no provers at all. Do not model new gates on it.
36+
37+
=== `formal/justfile` remains the single source of truth
38+
39+
The proof list *and its dependency order* live in `formal/justfile`. The
40+
workflow parses that list rather than restating it, so the two cannot drift.
41+
42+
A completeness guard then fails the run if any `formal/*.v` on disk is **not**
43+
named in the justfile. Adding a proof without wiring it is therefore a loud
44+
failure rather than a silent omission.
45+
46+
=== The axiom check
47+
48+
Each proof ends with `Print Assumptions <theorem>`. Coq emits:
49+
50+
* `Closed under the global context` — clean; the theorem depends on nothing
51+
outside the kernel
52+
* `Axioms:` followed by a list — the theorem rests on an axiom or an
53+
`Admitted` proof
54+
55+
The gate greps the accumulated output for `Axioms:`. As of 2026-07-29 all 20
56+
files report `Closed under the global context`.
57+
58+
== Container gotchas (both cost a red run before being found)
59+
60+
[IMPORTANT]
61+
====
62+
These two are properties of `coqorg/*` images under GitHub Actions
63+
specifically. They will bite again on any new Coq job.
64+
====
65+
66+
. **The entrypoint never runs.** The `coqorg` images install Coq into an opam
67+
switch owned by the `coq` user and put it on `PATH` via an `ENTRYPOINT`
68+
wrapper. GitHub Actions *overrides* the entrypoint for job containers, so the
69+
wrapper never executes and `coqc` is not on `PATH` — the failure reads simply
70+
`coqc: not found`. The workflow adds the switch explicitly, **globbed**
71+
(`/home/coq/.opam/*/bin`) rather than hard-coded, so an image bump cannot
72+
silently break it, and fails loudly if it cannot be located.
73+
74+
. **The shell is not bash unless you say so.** GitHub fell back to
75+
`sh -e {0}` (dash), which rejects `set -o pipefail` and the bash-only string
76+
operations the gate uses. The image *does* ship bash 5.2, so the job declares
77+
`defaults.run.shell: bash` rather than relying on runner detection.
78+
79+
== Prover version
80+
81+
[cols="1,2"]
82+
|===
83+
| `formal/README.adoc` documents | Coq/Rocq **8.18**
84+
| The pinned CI container is | `coqorg/coq@sha256:e50d77c4…` → **8.20.1**
85+
|===
86+
87+
The corpus was verified to check clean on 8.20.1. The only friction is a
88+
deprecation warning — `app_length` is deprecated since 8.20 in favour of
89+
`length_app` — raised by `RealCompile.v`, `RealLoop.v` and `RealMem.v`. No
90+
errors. Reconciling the documented pin with the gating version is outstanding.
91+
92+
== Running it locally
93+
94+
Requires `coqc` on `PATH` (any 8.18–8.20):
95+
96+
[source,console]
97+
----
98+
$ cd formal && just check
99+
----
100+
101+
Expect, on success:
102+
103+
----
104+
OK: K-1/K1Let/F-1 + P-2/P-3/F-3/F-4 mechanized; no axioms.
105+
----
106+
107+
A cold run takes over two minutes; the workflow allows `timeout-minutes: 30`.
108+
109+
== Verifying the gate can actually fail
110+
111+
Both guards were falsifier-tested rather than assumed:
112+
113+
[cols="2,1"]
114+
|===
115+
| Falsifier | Result
116+
117+
| Add an unwired `formal/ZZ_Falsifier.v`
118+
| completeness guard fires, run fails
119+
120+
| Add a theorem proved via `Axiom cheat : forall P : Prop, P`
121+
| `Print Assumptions` emits `Axioms:`, grep catches it, run fails
122+
|===
123+
124+
Re-run these if the gate is ever refactored. A proof gate that has never been
125+
observed to fail is not evidence of anything.

‎formal/README.adoc‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,19 @@ issue #513 names for mechanized proofs. Prover: **Coq/Rocq 8.18** — chosen for
1111
the codegen/K-1 track because the typed-WASM target semantics interoperate with
1212
`typed-wasm` and ephapax, both of which use Coq (`Semantics.v`).
1313

14+
[NOTE]
15+
.CI gates on 8.20.1, not 8.18
16+
====
17+
Since 2026-07-29 these proofs are gated in CI by
18+
`.github/workflows/coq-proof-gate.yml`, whose pinned container provides
19+
**Coq 8.20.1**. The whole corpus was verified to check clean on 8.20.1; the
20+
only friction is a deprecation warning (`app_length` -> `length_app`, deprecated
21+
since 8.20) from `RealCompile.v`, `RealLoop.v` and `RealMem.v`. No errors.
22+
23+
Reconciling this documented 8.18 pin with the 8.20 gating version is
24+
outstanding. See `docs/ci/COQ-PROOF-GATE.adoc`.
25+
====
26+
1427
[IMPORTANT]
1528
.`.v` here is Coq, not V-lang
1629
====

0 commit comments

Comments
 (0)