From 4e8f5cd177fabc2abeaaef36878b7f3d994fda32 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Mon, 3 Aug 2026 13:43:14 +0100 Subject: [PATCH] docs: record the Coq proof gate and the 2026-07-29 rescue session MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Human-readable and machine-readable documentation of the state established this session, using the conventions already in the repo rather than new ones. - docs/ci/COQ-PROOF-GATE.adoc — sits beside required-checks.adoc. Covers what the gate checks, why it is fail-closed (and why tools/check-proofs.sh is not a model to copy), the two coqorg-under-GitHub-Actions container faults that each cost a red run, 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. Records the gate, the rescue of 3 feature commits from a deleted checkout, three pieces of sweep damage (including the .gitattributes deletion that would have unlabelled 493 .affine files), the partial-merge incident that left main red, and method notes. - formal/README.adoc — note that CI gates on 8.20.1 while this file documents 8.18, and that reconciling them is outstanding. STATE.a2ml was deliberately left alone: it is 67KB, self-describes as stale and as mirroring rather than leading, so a session record is the correct home. Co-Authored-By: Claude Opus 5 --- .../2026-07-29-proof-gate-and-rescue.a2ml | 143 ++++++++++++++++++ docs/ci/COQ-PROOF-GATE.adoc | 125 +++++++++++++++ formal/README.adoc | 13 ++ 3 files changed, 281 insertions(+) create mode 100644 .machine_readable/sessions/2026-07-29-proof-gate-and-rescue.a2ml create mode 100644 docs/ci/COQ-PROOF-GATE.adoc diff --git a/.machine_readable/sessions/2026-07-29-proof-gate-and-rescue.a2ml b/.machine_readable/sessions/2026-07-29-proof-gate-and-rescue.a2ml new file mode 100644 index 00000000..b44324ce --- /dev/null +++ b/.machine_readable/sessions/2026-07-29-proof-gate-and-rescue.a2ml @@ -0,0 +1,143 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 hyperpolymath +# +# Session record — 2026-07-29 — Coq proof gate wired + stranded work rescued +# +# Human-readable companions: +# docs/ci/COQ-PROOF-GATE.adoc (the gate: design, gotchas, falsifiers) +# dev-notes/affinescript-sitrep-2026-07-29.md (estate-local, not in this repo) + +[metadata] +schema = "a2ml/session-record/v1" +session-date = "2026-07-29" +session-topic = "wire the formal/ Coq proof gate into CI; rescue feature work from a deleted checkout" +repo = "hyperpolymath/affinescript" +human-companion = "docs/ci/COQ-PROOF-GATE.adoc" +prs = [708, 709, 711] + +# ── Outcome 1: the Coq proof gate ────────────────────────────────────── +# 20 machine-checked proofs existed in formal/ with a real fail-closed +# runner in formal/justfile, but NO workflow invoked them. Now gated. + +[proof-gate] +workflow = ".github/workflows/coq-proof-gate.yml" +corpus-path = "formal/" +corpus-size = 20 +source-of-truth = "formal/justfile" +list-parsed-not-copied = true +fail-closed = true +prover-in-ci = "8.20.1" +prover-documented = "8.18" +prover-pin-reconciled = false +container-digest = "sha256:e50d77c4c5a9aa0d76ae1b343d79c5f922da3a75054b79c5dc635895438e4674" +all-proofs-axiom-free = true +assumptions-result = "Closed under the global context" +tracking-issue = 513 + +[[proof-gate.falsifier]] +id = "unwired-proof-file" +method = "add formal/ZZ_Falsifier.v not named in formal/justfile" +fires = true +guards = "completeness" + +[[proof-gate.falsifier]] +id = "axiom-dependent-theorem" +method = "prove a goal via `Axiom cheat : forall P : Prop, P`" +fires = true +guards = "Print Assumptions / grep Axioms:" + +# Two container faults, each cost one red CI run. Both are properties of +# coqorg/* images under GitHub Actions and will recur on any new Coq job. + +[[proof-gate.gotcha]] +id = "entrypoint-overridden" +symptom = "coqc: not found" +cause = "coqorg installs Coq into the `coq` user's opam switch and exposes it via ENTRYPOINT; GitHub Actions overrides the entrypoint for job containers" +remedy = "add /home/coq/.opam/*/bin to GITHUB_PATH, globbed not hard-coded, failing loudly if absent" + +[[proof-gate.gotcha]] +id = "shell-fell-back-to-dash" +symptom = "set: Illegal option -o pipefail" +cause = "GitHub used `sh -e {0}` despite the image shipping bash 5.2" +remedy = "declare defaults.run.shell: bash explicitly" + +# ── Outcome 2: rescue of stranded work ───────────────────────────────── +# An estate reorg renamed the working checkout to *.DUPLICATE-superseded-* +# and then DELETED it mid-session. It held 9 commits present nowhere else. +# The rename judged duplicates by directory identity, not by git rev-list. + +[rescue] +trigger = "checkout renamed *.DUPLICATE-superseded-2026-07-27 then deleted mid-session" +misjudgement = "duplicate decided by directory identity rather than `git rev-list` — the directory marked superseded held 9 unpushed commits; the one kept held 0" +estate-wide = "the same rename was reported backwards in all 8 affected repos" +commits-at-risk = 9 +commits-recovered-to-main = 3 +recovered-via = "git bundle taken before deletion" +cherry-pick-needed = false +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" +pr = 708 + +[[rescue.commit]] +sha = "220d7ca" +kind = "feature" +subject = "docs: resolve INT-02 satellite scope deferral" +closes = 489 + +[[rescue.commit]] +sha = "70ca15e" +kind = "feature" +subject = "feat(dom): browser host parity execution harness (INT-11)" + +[[rescue.commit]] +sha = "e959636" +kind = "feature" +subject = "feat(cadre): scaffold router navigation runtime wrapper (INT-09)" + +# ── Outcome 3: sweep damage found and reverted (uncommitted only) ────── + +[[sweep-damage]] +id = "gitattributes-language-declaration-deleted" +file = ".gitattributes" +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" +state = "reverted-in-working-tree" +severity = "high" +advice = "never `git commit -a` in this repo while an estate sweep is active" + +[[sweep-damage]] +id = "gitignore-foreign-template-entries" +file = ".gitignore" +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" +state = "reverted-in-working-tree" +severity = "low" + +[[sweep-damage]] +id = "patch-ecosystem-py-escape-corruption" +file = "docs/patch_ecosystem.py" +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" +state = "still-present-on-main" +severity = "medium" +fingerprint = "a leading letter missing after a would-be backslash escape; grep the estate for this shape — it produces scripts that appear to succeed" + +# ── Outcome 4: main was left red by a partial merge ──────────────────── + +[incident-partial-merge] +pr-that-broke-main = 709 +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`" +red-since = "ed4e223" +repair-pr = 711 +repair-verified = "workflow_dispatch green on the branch: 20/20 proofs, completeness guard passed, no axioms" +lesson = "after a squash merge, re-check that the merged tree contains the fix — a green PR check can belong to a superseded commit" + +# ── Method notes worth not re-deriving ───────────────────────────────── + +[[method-note]] +id = "always-fetch-before-judging-divergence" +detail = "a stale remote-tracking ref reported `ahead 16`; after `git fetch` the true figure was 9. Origin had already absorbed 7 via PRs." + +[[method-note]] +id = "a-red-run-is-not-a-red-branch" +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." + +[[method-note]] +id = "bundle-verify-is-not-restore" +detail = "`git bundle verify` proves internal consistency, not that the bundle restores what you wanted. Clone it and assert the expected SHA." diff --git a/docs/ci/COQ-PROOF-GATE.adoc b/docs/ci/COQ-PROOF-GATE.adoc new file mode 100644 index 00000000..c94dbf1a --- /dev/null +++ b/docs/ci/COQ-PROOF-GATE.adoc @@ -0,0 +1,125 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += The Coq Proof Gate +:toc: left +:toclevels: 3 + +Workflow: `.github/workflows/coq-proof-gate.yml` + +Proof corpus: `formal/` (20 `.v` files) + +Local runner: `formal/justfile` (`just check`) + +Tracking issue: #513 (umbrella), #514–#521 (individual obligations) + +== What it does + +Type-checks every Coq/Rocq proof in `formal/` and **fails if any theorem +depends on an axiom or an `Admitted` proof**. + +This is the mechanised half of the proof programme catalogued in +`docs/PROOF-NEEDS.adoc`. Until 2026-07-29 the corpus existed and checked +clean, but **no workflow invoked it** — a `grep` for coq/rocq across +`.github/workflows/` returned nothing. The proofs were real; the assurance +was simply being discarded. + +== Design decisions + +=== It is fail-closed + +The gate does *not* probe for the prover and skip when it is absent. The +pinned container guarantees `coqc`, so a missing prover is an infrastructure +failure, not a silent pass. + +This matters because the sibling script `tools/check-proofs.sh` takes the +opposite approach for Idris2/Lean/Agda — it gates each on +`command -v … || { note "SKIP"; return; }` and exits `0` with zero provers +present. That script reports "N passed, N failed, N skipped" and is green on a +machine with no provers at all. Do not model new gates on it. + +=== `formal/justfile` remains the single source of truth + +The proof list *and its dependency order* live in `formal/justfile`. The +workflow parses that list rather than restating it, so the two cannot drift. + +A completeness guard then fails the run if any `formal/*.v` on disk is **not** +named in the justfile. Adding a proof without wiring it is therefore a loud +failure rather than a silent omission. + +=== The axiom check + +Each proof ends with `Print Assumptions `. Coq emits: + +* `Closed under the global context` — clean; the theorem depends on nothing + outside the kernel +* `Axioms:` followed by a list — the theorem rests on an axiom or an + `Admitted` proof + +The gate greps the accumulated output for `Axioms:`. As of 2026-07-29 all 20 +files report `Closed under the global context`. + +== Container gotchas (both cost a red run before being found) + +[IMPORTANT] +==== +These two are properties of `coqorg/*` images under GitHub Actions +specifically. They will bite again on any new Coq job. +==== + +. **The entrypoint never runs.** The `coqorg` images install Coq into an opam + switch owned by the `coq` user and put it on `PATH` via an `ENTRYPOINT` + wrapper. GitHub Actions *overrides* the entrypoint for job containers, so the + wrapper never executes and `coqc` is not on `PATH` — the failure reads simply + `coqc: not found`. The workflow adds the switch explicitly, **globbed** + (`/home/coq/.opam/*/bin`) rather than hard-coded, so an image bump cannot + silently break it, and fails loudly if it cannot be located. + +. **The shell is not bash unless you say so.** GitHub fell back to + `sh -e {0}` (dash), which rejects `set -o pipefail` and the bash-only string + operations the gate uses. The image *does* ship bash 5.2, so the job declares + `defaults.run.shell: bash` rather than relying on runner detection. + +== Prover version + +[cols="1,2"] +|=== +| `formal/README.adoc` documents | Coq/Rocq **8.18** +| The pinned CI container is | `coqorg/coq@sha256:e50d77c4…` → **8.20.1** +|=== + +The corpus was verified to check clean on 8.20.1. The only friction is a +deprecation warning — `app_length` is deprecated since 8.20 in favour of +`length_app` — raised by `RealCompile.v`, `RealLoop.v` and `RealMem.v`. No +errors. Reconciling the documented pin with the gating version is outstanding. + +== Running it locally + +Requires `coqc` on `PATH` (any 8.18–8.20): + +[source,console] +---- +$ cd formal && just check +---- + +Expect, on success: + +---- +OK: K-1/K1Let/F-1 + P-2/P-3/F-3/F-4 mechanized; no axioms. +---- + +A cold run takes over two minutes; the workflow allows `timeout-minutes: 30`. + +== Verifying the gate can actually fail + +Both guards were falsifier-tested rather than assumed: + +[cols="2,1"] +|=== +| Falsifier | Result + +| Add an unwired `formal/ZZ_Falsifier.v` +| completeness guard fires, run fails + +| Add a theorem proved via `Axiom cheat : forall P : Prop, P` +| `Print Assumptions` emits `Axioms:`, grep catches it, run fails +|=== + +Re-run these if the gate is ever refactored. A proof gate that has never been +observed to fail is not evidence of anything. diff --git a/formal/README.adoc b/formal/README.adoc index 71aa4bd5..aa436f4f 100644 --- a/formal/README.adoc +++ b/formal/README.adoc @@ -11,6 +11,19 @@ issue #513 names for mechanized proofs. Prover: **Coq/Rocq 8.18** — chosen for the codegen/K-1 track because the typed-WASM target semantics interoperate with `typed-wasm` and ephapax, both of which use Coq (`Semantics.v`). +[NOTE] +.CI gates on 8.20.1, not 8.18 +==== +Since 2026-07-29 these proofs are gated in CI by +`.github/workflows/coq-proof-gate.yml`, whose pinned container provides +**Coq 8.20.1**. The whole corpus was verified to check clean on 8.20.1; the +only friction is a deprecation warning (`app_length` -> `length_app`, deprecated +since 8.20) from `RealCompile.v`, `RealLoop.v` and `RealMem.v`. No errors. + +Reconciling this documented 8.18 pin with the 8.20 gating version is +outstanding. See `docs/ci/COQ-PROOF-GATE.adoc`. +==== + [IMPORTANT] .`.v` here is Coq, not V-lang ====