fix(ci): gate every Idris2 module — the proof checks could not fail (and #51's fix never landed)

.github/workflows/idris2-proof.yml

@@ -1,20 +1,37 @@
 # 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.
+# Idris2 proof check — type-checks EVERY Idris2 module in the repository via
+# scripts/check-idris2-proofs.sh (the same script `just proof-check-idris2`
+# runs, so local green and CI green mean the same thing).
+#
+# History, because the scope of this gate is the whole point:
+#
+#   v1 gated a-sounder-constitution/formal/ only. It was created after a proof
+#   shipped unchecked and did not compile (#45). It worked -- and the identical
+#   bug then walked into the two directories it did not cover. research/'s
+#   Modal.idr never compiled from creation until 2026-07-16 (`dup` collided with
+#   Prelude.dup), while every status file recorded its comonad laws as proved at
+#   100%. Five of the six modules under verification/proofs/idris2/ -- a
+#   directory named "proofs" -- still do not compile.
+#
+#   The lesson was not "gate that file". It was "gate the language". A gate
+#   scoped to where the bug last happened only ever prevents the last bug.
+#
+# Path filters are therefore deliberately broad: any .idr anywhere, the script,
+# and this workflow. The script itself fails on any .idr not in its manifest, so
+# new proofs cannot be added ungated.
 name: Idris2 Proof
 
 on:
   push:
     branches: [main, master]
     paths:
-      - 'a-sounder-constitution/formal/**'
+      - '**.idr'
+      - 'scripts/check-idris2-proofs.sh'
       - '.github/workflows/idris2-proof.yml'
   pull_request:
     paths:
-      - 'a-sounder-constitution/formal/**'
+      - '**.idr'
+      - 'scripts/check-idris2-proofs.sh'
       - '.github/workflows/idris2-proof.yml'
   workflow_dispatch:
 
@@ -57,14 +74,7 @@ jobs:
           make install SCHEME=chezscheme
           echo "${HOME}/.idris2/bin" >> "$GITHUB_PATH"
 
-      - name: Type-check the constitutional proof
-        # Run from the module's own directory: Idris2 derives the expected module
-        # name from the path it is given, so `module Constitution` must be checked
-        # as `Constitution.idr` (not `a-sounder-constitution/formal/Constitution.idr`,
-        # which it would expect to declare an — impossible, hyphenated — module name).
-        working-directory: a-sounder-constitution/formal
-        run: |
-          set -euo pipefail
-          idris2 --version
-          idris2 --check Constitution.idr
-          echo "Constitution.idr type-checks (exit 0)"
+      - name: Type-check every Idris2 module
+        # The script fails if idris2 is missing rather than skipping, so a broken
+        # install step can never render as a green proof run.
+        run: ./scripts/check-idris2-proofs.sh

.machine_readable/6a2/STATE.a2ml

@@ -6,7 +6,7 @@
 [metadata]
 project = "ideas-to-alphas"
 version = "0.1.0"
-last-updated = "2026-07-16"
+last-updated = "2026-07-17"
 status = "active"
 
 [project-context]
@@ -28,37 +28,58 @@ milestones = [
   { name = "Repo created and pushed to GitHub", completion = 100 },
   { name = "research/ directory structure created", completion = 100 },
   { name = "First L11 candidate formalized in Idris2 (L11-modal-box)", completion = 100 },
-  { name = "L11-modal-box comonad laws proved (believe_me-free)", completion = 100 },
+  { name = "L11-modal-box comonad laws proved (believe_me-free) — NB genuinely true only since 2026-07-16; Modal.idr did not compile before the `%hide Prelude.dup` fix, so this milestone was FALSE when first recorded at 100%", completion = 100 },
+  { name = "L11-modal-box Modal.idr actually compiles (idris2 0.7.0 --check, exit 0)", completion = 100 },
+  { name = "L11-modal-box dup-forces-omega machine-checked (DupForcesOmega.idr)", completion = 100 },
   { name = "L11-modal-box semantics decided (graded necessity; not S4, not contextual)", completion = 100 },
   { name = "L11-modal-box QTT grade propagation specified (QTT-INTEGRATION.adoc)", completion = 100 },
   { name = "L11-modal-box reading notes: contextual modal types (NPP 2008)", completion = 100 },
+  { name = "Idris2 gate covers EVERY .idr in the repo (scripts/check-idris2-proofs.sh; unlisted module = CI error)", completion = 100 },
   { name = "L11-modal-box Modal.idr rewritten to graded Box (split replaces dup)", completion = 0 },
+  { name = "verification/proofs/idris2 compiles (5 of 6 modules currently quarantined)", completion = 17 },
   { name = "First graduated artefact promoted to typell", completion = 0 },
 ]
 
 [blockers-and-issues]
 issues = [
-  "L11-modal-box: Modal.idr `dup : Box a -> (Box a, Box a)` is admissible only where r + r = r, hence r in {0, omega}; since 0 is erased, every useful instance pins r = omega. As written, Box a is isomorphic to an L10 value at multiplicity omega and L11 adds NOTHING over L10. Rewrite to graded Box required. See research/level-candidates/L11-modal-box/QTT-INTEGRATION.adoc section 5.",
-  "L11-modal-box: `Multiplicity` is a bare data type with no algebraic content — no +, no ., no semiring laws are defined on it at all.",
+  "PROCESS (root cause 1 — FIXED 2026-07-17): `just proof-check-idris2` did `exit 0` when idris2 was absent, printing 'SKIP: idris2 not installed'. idris2 WAS absent, so the recipe reported success on every machine in the estate — it passed *because* nothing could check the proofs. `just proof-check-all` depends on it, so the whole proof suite was green. A skip-on-missing-tool that exits 0 converts 'I cannot verify this' into 'this is verified'. The recipe now delegates to scripts/check-idris2-proofs.sh, which treats a missing toolchain as fatal.",
+  "PROCESS (root cause 2 — FIXED 2026-07-17): the same recipe invoked `idris2 --check <full/path/Mod.idr>`, but Idris2 derives the expected module name from the path it is handed. Every module therefore failed on a name mismatch rather than its real error. Verified: the recipe reported ABI/Compliance.idr OK (it is broken) and ABI/Foreign.idr FAIL (it is the one module that compiles) — its verdict was inverted on both discriminating cases. It agreed with reality elsewhere only by accident, because it failed everything.",
+  "PROCESS (root cause 3 — FIXED 2026-07-17): the Idris2 CI gate was path-filtered to a-sounder-constitution/formal/ only. It was created because a proof shipped unchecked and did not compile (#45) — and the identical bug then walked into research/ and verification/, which it did not cover. A gate scoped to where the bug last happened only prevents the last bug. The gate now covers every .idr in the repo, and an .idr absent from the manifest is a CI error, so new proofs are gated by default.",
+  "TOOLCHAIN (upstream, Idris2 0.7.0, NOT fixed — worked around): `idris2 --check` EXITS 0 on a missing import while printing 'Error: Module X not found'. Verified in a clean room: type errors, parse errors and module-name mismatches all exit 1, but a missing import exits 0. Any gate of the form `idris2 --check X && echo proved` is therefore unsound estate-wide, including the original a-sounder-constitution gate. scripts/check-idris2-proofs.sh requires BOTH exit 0 AND no '^Error:' in the output. Worth reporting upstream.",
+  "CORRECTION (my own earlier entry was wrong): PROOF-STATUS.md is NOT stale. It reports 0/7 proven, and that is very nearly the literal truth — of the 6 Idris2 modules backing its ABI-1..5 + TP-1 obligations, 5 do not compile at all and the 6th (ABI/Foreign.idr) compiles but was never credited. PROOF-STATUS.md tracks verification/proofs/idris2/ only; it says nothing about a-sounder-constitution or L11-modal-box, so those landing does not make it stale. It is the one status document in this repo that was telling the truth, and STATE.a2ml accused it of lying. Its header still says 'KATAGORIA' (pre-rename), which is a cosmetic staleness that masked its accuracy.",
+  "verification/proofs/idris2: 5 of 6 modules DO NOT COMPILE (Types.idr, ABI/Platform.idr, ABI/Layout.idr, ABI/Pointers.idr, ABI/Compliance.idr) — only ABI/Foreign.idr does. First error is `Undefined name LTE / NonZero / modNatNZ`: these were Prelude in Idris1 and are Data.Nat in Idris2, so the files are never-compiled Idris1-era template code. CORRECTION (attempted 2026-07-17, reverted): `import Data.Nat` is necessary but NOT sufficient — it only unmasks the next layer. This is NOT a one-line-each fix. Measured post-import errors: Types.idr -> '.inBounds is not accessible'; ABI/Platform.idr -> 'Undefined name lteRefl'; ABI/Layout.idr -> \"Can't solve constraint between: S ?x and f .fieldAlignment\"; ABI/Pointers.idr -> '.nonNull is not accessible' plus a unification failure; ABI/Compliance.idr inherits ABI/Layout's.",
+  "verification/proofs/idris2: Types.idr and ABI/Pointers.idr share a genuine DESIGN error, not a typo. Both declare a proof field at quantity 0 — e.g. `{auto 0 inBounds : LTE value max}` — and then project it into a value position (`boundedLeMax b = b.inBounds`). A 0-quantity field is erased, so it cannot be returned as a value; the projection is not accessible by construction. Fixing this needs a deliberate decision about the record's quantities (drop the 0, or restructure so the proof is returned by a separate unerased accessor), not a mechanical edit. Whoever takes this should expect real proof engineering per module. Own PR; all five stay quarantined until then.",
+  "L11-modal-box: Modal.idr did NOT COMPILE from creation until 2026-07-16 — `dup` collided with Idris2 0.7.0's `Prelude.dup : a -> (a, a)` (Ambiguous elaboration), so comonadLaw1/comonadLaw2 never elaborated and were verified by nothing, while the file header and this file both recorded them as proved. Fixed with `%hide Prelude.dup`; module now checks clean. The name clash was not a coincidence: Prelude.dup IS unrestricted duplication, which is what Box's dup collapses to at omega.",
+  "L11-modal-box: Modal.idr `dup : Box a -> (Box a, Box a)` is admissible only where r + r = r, hence r in {0, omega}; since 0 is erased, every useful instance pins r = omega. As written, Box a is isomorphic to an L10 value at multiplicity omega and L11 adds NOTHING over L10. Rewrite to graded Box required. Machine-checked in DupForcesOmega.idr; see research/level-candidates/L11-modal-box/QTT-INTEGRATION.adoc section 5.",
+  "research/tropical/TropicalKleene.idr ALSO does not compile (idris2 0.7.0, exit 1): 'Expected a type declaration'. costMatAddZeroL is written `rewrite h` with no `in`, followed by `exact ...` — and `exact` is not Idris2 term syntax at all (an Idris1/tactic-style habit). The file uses syntax that has never existed in the language, so it cannot ever have been run. Same root cause as Modal.idr. NOT fixed here — needs its own PR; there may be further errors hidden behind the first parse failure. Suggested fix: `costMatAddZeroL m1 m2 i h = rewrite h in latAddZeroL (m2 i i)`.",
+  "L11-modal-box: `Multiplicity` is a bare data type with no algebraic content — no +, no ., no semiring laws are defined on it at all. (DupForcesOmega.idr now supplies plus/mult standalone, but Modal.idr's Box is still not indexed by them.)",
   "L11-modal-box: comonadLaw1/comonadLaw2 are sound but are the omega-instance laws only; not evidence for the discipline at r = 1.",
   "L11-modal-box: MOTIVATION.adoc says 'TypeLL grade lattice', but {0,1,omega} with 0 and 1 incomparable has no meets and is an ordered semiring, not a lattice. Prose or algebra is wrong; pin against typell L10.",
-  "Repo-wide: PROOF-STATUS.md reports 0/7 proven — stale; predates the Idris2 proofs that have landed (a-sounder-constitution, L11-modal-box).",
+  "Repo-wide: src/interface/build/ttc/2025081600/Abi/*.ttc and *.ttm (6 files) are compiled Idris2 build artefacts committed to the repo, despite `build/` being in .gitignore (line 113) — force-added or predating the rule. They are stale, and their existence is the one piece of evidence that idris2 ran against src/interface at some point (TTC stamp suggests Aug 2025). Untrack them.",
+  "PROCESS (same disease, NOT fixed — own PR): `just validate-state` has never validated this project's state. It checks .machine_readable/STATE.a2ml, but the maintained file is .machine_readable/6a2/STATE.a2ml. The file it checks is a committed 1116-byte template leftover in S-EXPRESSION syntax that still declares (project \"rsr-template-repo\") and (last-updated \"2026-04-04\") — a different project's scaffolding. The recipe greps for TOML `^[metadata]` in an S-expression file, so it prints 'INVALID (missing required sections)' — AND EXITS 0. It has been printing INVALID forever against the wrong file in the wrong format, and nothing noticed because it cannot fail. Fix: point it at 6a2/, parse as TOML, exit non-zero on failure; delete or convert the leftover. Not referenced by any workflow either.",
+  "META-FINDING (the actual root cause, above all the individual bugs): this repo's checks cannot fail. Four independent instances found 2026-07-17 — (1) proof-check-idris2 exits 0 when idris2 is absent; (2) proof-check-{lean4,agda,coq} do the same for their provers; (3) validate-state reports INVALID and exits 0 against the wrong file; (4) upstream, `idris2 --check` exits 0 on a missing import. A check that cannot fail is not a weak check, it is a NULL check that emits reassuring text — and every status file downstream of it inherits false confidence. When auditing the rest of the estate, grep for the shape (a guard that echoes a problem then exits 0), not for the specific tools.",
+  "PROVENANCE NOTE: the claim 'idris2 was never installed in this estate' (recorded 2026-07-16) is too strong. IDRIS2_PREFIX and PACK_DIR pointed at a pack tree that did not exist, so it was not installed in the *current* toolchain and `idris2 --check` was not runnable locally — but the committed .ttc artefacts above show it ran somewhere, earlier. The accurate claim is: nothing in the current toolchain or CI had checked research/ or verification/ until 2026-07-16.",
 ]
 
 [critical-next-actions]
 actions = [
+  "FIRST — ESTATE AUDIT (measured 2026-07-17, not estimated): the exit-0-when-prover-absent pattern comes from rsr-template-repo and is present in 22 repos across hyper-repos/ and meta-repos/. 20 of those contain real proof files — paint-type (53), ideas-to-alphas (31), proof-burrower (18), snifs (15), email-octad-experiment (13), and 15 more at ~12 each. All four prover recipes share the defect (idris2, lean4, agda, coq), so it is a template bug, not an Idris2 one. LIVE RIGHT NOW: `lean` is not installed on this machine, so every `just proof-check-lean4` in the estate currently exits 0 and reports green having verified nothing. Fix rsr-template-repo FIRST so the pattern cannot be re-seeded into new repos, then sweep the 20. Detection: grep -rlE 'SKIP:.*not installed' */Justfile.",
+  "Report upstream to idris-lang/Idris2: `idris2 --check` exits 0 on a missing import while printing 'Error: Module X not found' (0.7.0). Every CI gate in the wild of the form `idris2 --check X && ok` is unsound against this.",
+  "Fix verification/proofs/idris2 in its own PR — budget real time, this is NOT a typo sweep (attempted and reverted 2026-07-17; see issues). `import Data.Nat` is step 1 of several per module and only unmasks the next error. The substantive blocker is a design decision shared by Types.idr and ABI/Pointers.idr: proof fields declared at quantity 0 are erased and cannot be projected into value positions, so the records need their quantities reconsidered. ABI/Layout.idr has a separate genuine unification failure (S ?x vs f .fieldAlignment) that ABI/Compliance.idr inherits. Promote each module from quarantine to gated in scripts/check-idris2-proofs.sh as it goes green — the script fails if a quarantined module starts passing, so the list cannot rot.",
+  "Refresh PROOF-STATUS.md — but note it is currently ACCURATE (0/7). The honest update is to credit ABI-4 (ABI/Foreign.idr compiles and mapIdPreserves is a real constructive proof) and to record that ABI-1/2/3/5 and TP-1 do not compile, rather than to mark anything proved. Fix the 'KATAGORIA' header (pre-rename).",
   "Rewrite Modal.idr to graded Box: replace dup with split : Box (r+s) a -> (Box r a, Box s a); add comult : Box (r*s) a -> Box r (Box s a); gate unbox on 1 <= r.",
-  "Give Multiplicity its semiring operations and laws, then prove dupForcesOmega : (r : Multiplicity) -> r + r = r -> Either (r = Zero) (r = Many) — machine-checking QTT-INTEGRATION.adoc section 5.",
+  "Fold DupForcesOmega.idr's plus/mult tables into Modal.idr and index Box by Multiplicity — dupForcesOmega itself is already machine-checked standalone; then prove the remaining semiring laws (associativity, distributivity, identities).",
+  "Fix research/tropical/TropicalKleene.idr in its own PR: costMatAddZeroL needs `rewrite h in latAddZeroL (m2 i i)` (currently `rewrite h` + `exact`, which is not Idris2 syntax); then re-check for errors hidden behind the first parse failure.",
   "Re-derive comonadLaw1/comonadLaw2 at general r rather than the implicit omega.",
   "Pin the ordering convention (is 0 <= 1?) and the lattice-vs-semiring question against typell/src/abi/TypedWasm/ABI/Levels.idr before graduation.",
-  "Refresh PROOF-STATUS.md against the proofs that have actually landed.",
+  "Untrack src/interface/build/ttc/**: 6 compiled .ttc/.ttm artefacts are committed despite `build/` being gitignored.",
 ]
 
 [maintenance-status]
-last-run-utc = "2026-04-11T00:00:00Z"
-last-result = "unknown"
+last-run-utc = "2026-07-17T00:00:00Z"
+last-result = "partial — first full-repo Idris2 sweep via scripts/check-idris2-proofs.sh. 13 modules found, 13 accounted for. PASS (8, gated): Constitution.idr, Modal.idr (only since the %hide Prelude.dup fix), DupForcesOmega.idr, src/interface Abi/{Types,Layout,Foreign}.idr, verification/proofs/idris2 ABI/Foreign.idr. FAIL (5, quarantined and tracked): research/tropical/TropicalKleene.idr, verification/proofs/idris2 {Types,ABI/Platform,ABI/Layout,ABI/Pointers,ABI/Compliance}.idr. The gate itself was adversarially tested against all five of its failure modes (unlisted module, absent toolchain, missing-import-exits-0, gated regression, quarantined module starting to pass) — each correctly turns it red."
 open-warnings = 0
-open-failures = 0
+open-failures = 5
 
 [ecosystem]
 part-of = ["nextgen-typing pipeline"]