From bfb3823128cf881c700e0eff4d51f57384ed19b0 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Thu, 16 Jul 2026 22:42:55 +0100 Subject: [PATCH 1/3] fix(L11): Modal.idr never compiled -- %hide Prelude.dup; machine-check dup-forces-omega Installing Idris2 0.7.0 -- which had never been installed in this estate -- and actually running `idris2 --check` revealed that Modal.idr HAS NEVER COMPILED: Error: While processing type of comonadLaw1. Ambiguous elaboration. Modal.dup b Prelude.dup b Error: No type declaration for Modal.comonadLaw1. Idris2 0.7.0's Prelude exports `dup : a -> (a, a)` ("Function that duplicates its input"). Every signature in Modal.idr mentioning `dup` failed to elaborate, so comonadLaw1/comonadLaw2 had no type declarations and were verified by NOTHING -- while the file header, the candidate checklist, and STATE.a2ml all recorded them as proved, believe_me-free, at 100%. Pre-existing, not introduced here: origin/main's copy fails identically (same errors, shifted line numbers). ROOT CAUSE of the false record: idris2 was never installed. IDRIS2_PREFIX and PACK_DIR were exported and pack/bin was on PATH, but the pack tree did not exist, so `idris2 --check` had never once been runnable locally -- and CI gates only a-sounder-constitution/, not research/. An unrunnable proof gate produces confident false records. Fixes: * `%hide Prelude.dup` in Modal.idr. It now checks clean (exit 0), believe_me-free -- the comonad laws are proved for the first time since the file was written. * New DupForcesOmega.idr machine-checks QTT-INTEGRATION.adoc s5 (exit 0): dupForcesOmega : (r : Multiplicity) -> plus r r = r -> Either (r = Zero) (r = Many) dupForcesOmega Zero Refl = Left Refl dupForcesOmega One Refl impossible dupForcesOmega Many Refl = Right Refl The One case is impossible: `plus One One` reduces to Many, so the premise would need `Refl : Many = One`. That one unwritable clause is the entire defect. The file also supplies the plus/mult tables Multiplicity never had. The name clash was never a coincidence: Prelude.dup IS unrestricted duplication, and at r = omega Box's dup is exactly Prelude.dup up to the MkBox wrapper. The compiler had been pointing at the defect all along. SECOND BROKEN PROOF (recorded, not fixed here): research/tropical/TropicalKleene.idr also fails (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. That file uses syntax which has never existed in the language, so it cannot ever have been run. Needs its own PR. Proof sweep with idris2 0.7.0, recorded in STATE.a2ml maintenance-status: PASS research/level-candidates/L11-modal-box/Modal.idr (after this fix) PASS research/level-candidates/L11-modal-box/DupForcesOmega.idr PASS a-sounder-constitution/formal/Constitution.idr (the CI-gated one) FAIL research/tropical/TropicalKleene.idr (pre-existing) Records corrected across MOTIVATION.adoc, README.adoc, SEMANTICS-DECISION.adoc, QTT-INTEGRATION.adoc and STATE.a2ml (open-failures 0 -> 1). Top next action is now to extend the Idris2 CI gate to research/, and to audit every other repo in the estate recording an Idris2 milestone for the same unrunnable-gate failure mode. Co-Authored-By: Claude Opus 4.8 (1M context) --- .machine_readable/6a2/STATE.a2ml | 23 ++-- .../L11-modal-box/DupForcesOmega.idr | 119 ++++++++++++++++++ .../L11-modal-box/MOTIVATION.adoc | 12 +- .../level-candidates/L11-modal-box/Modal.idr | 43 ++++++- .../L11-modal-box/QTT-INTEGRATION.adoc | 50 ++++++++ .../L11-modal-box/SEMANTICS-DECISION.adoc | 38 ++++-- research/level-candidates/README.adoc | 36 ++++-- 7 files changed, 289 insertions(+), 32 deletions(-) create mode 100644 research/level-candidates/L11-modal-box/DupForcesOmega.idr diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index c7e9630..f1966ad 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -28,7 +28,9 @@ 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 }, @@ -38,8 +40,12 @@ milestones = [ [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, fix first): idris2 was NEVER installed in this estate. IDRIS2_PREFIX and PACK_DIR were exported and pack/bin was on PATH, but the pack tree did not exist — so `idris2 --check` had never once been runnable locally. Consequence: research proofs were recorded as complete without anything ever checking them. Idris2 0.7.0 is now built and installed at that prefix (2026-07-16).", + "PROCESS: the Idris2 CI gate covers only a-sounder-constitution/, not research/. A research module can stay broken indefinitely while STATE.a2ml records it as proved at 100%. Extend the gate to research/ or stop recording research proofs as milestones.", + "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).", @@ -47,18 +53,21 @@ issues = [ [critical-next-actions] actions = [ + "FIRST: extend the Idris2 CI gate to research/ — with idris2 0.7.0 now installed, Modal.idr and DupForcesOmega.idr each check in under a second. Until this exists, no research proof milestone in this file is trustworthy.", + "Audit every other repo in the estate that records an Idris2 proof milestone: the same unrunnable-gate failure mode applies wherever idris2 --check was assumed rather than executed.", "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.", ] [maintenance-status] -last-run-utc = "2026-04-11T00:00:00Z" -last-result = "unknown" +last-run-utc = "2026-07-16T21:40:49Z" +last-result = "partial — idris2 0.7.0 installed and run here for the first time. PASS: Modal.idr (after the %hide Prelude.dup fix), DupForcesOmega.idr, a-sounder-constitution/formal/Constitution.idr. FAIL: research/tropical/TropicalKleene.idr (pre-existing, uses non-Idris2 syntax; not fixed here). asciidoctor clean on all docs." open-warnings = 0 -open-failures = 0 +open-failures = 1 [ecosystem] part-of = ["nextgen-typing pipeline"] diff --git a/research/level-candidates/L11-modal-box/DupForcesOmega.idr b/research/level-candidates/L11-modal-box/DupForcesOmega.idr new file mode 100644 index 0000000..4b71f45 --- /dev/null +++ b/research/level-candidates/L11-modal-box/DupForcesOmega.idr @@ -0,0 +1,119 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell +-- +-- research/level-candidates/L11-modal-box/DupForcesOmega.idr +-- +-- Machine-checks the central claim of QTT-INTEGRATION.adoc section 5: +-- +-- an ungraded `dup : Box a -> (Box a, Box a)` is admissible only where +-- r + r = r, hence only at r in {Zero, Many}. +-- +-- Verified with Idris2 0.7.0: idris2 --check DupForcesOmega.idr +-- +-- This file supplies the semiring content that Modal.idr's `Multiplicity` never +-- had. Modal.idr titles its section "the QTT multiplicity semiring from L10" +-- but defines a bare three-constructor enumeration: no (+), no (*), no laws, and +-- `Box` is not indexed by it. That absence is precisely why the `dup` defect +-- survived unnoticed -- with no (+) in scope, `r + r = r` was not a question +-- anyone could ask. + +module DupForcesOmega + +-- ───────────────────────────────────────────────────────────────────────────── +-- The L10 usage multiplicities +-- ───────────────────────────────────────────────────────────────────────────── + +data Multiplicity = Zero | One | Many + +-- ───────────────────────────────────────────────────────────────────────────── +-- Semiring addition: how uses combine when a resource is SPLIT +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- The key entry is `plus One One = Many`: using a linear thing twice is +-- unrestricted use. Everything below follows from that one line. + +plus : Multiplicity -> Multiplicity -> Multiplicity +plus Zero Zero = Zero +plus Zero One = One +plus Zero Many = Many +plus One Zero = One +plus One One = Many +plus One Many = Many +plus Many Zero = Many +plus Many One = Many +plus Many Many = Many + +-- ───────────────────────────────────────────────────────────────────────────── +-- Semiring multiplication: how uses compose when boxes NEST +-- ───────────────────────────────────────────────────────────────────────────── + +mult : Multiplicity -> Multiplicity -> Multiplicity +mult Zero Zero = Zero +mult Zero One = Zero +mult Zero Many = Zero +mult One Zero = Zero +mult One One = One +mult One Many = Many +mult Many Zero = Zero +mult Many One = Many +mult Many Many = Many + +-- ───────────────────────────────────────────────────────────────────────────── +-- The theorem +-- ───────────────────────────────────────────────────────────────────────────── + +||| `dup : Box a -> (Box a, Box a)` returns two boxes at the SAME grade as its +||| input. The only rule producing `Box r a` and `Box s a` from one box is +||| +||| split : Box (r + s) a -> (Box r a, Box s a) +||| +||| Instantiating s := r gives premise `Box (r + r) a`, while the input `dup` +||| declares is `Box r a`. Hence `dup` is admissible only where r + r = r. +||| +||| This proves that constraint pins r to {Zero, Many} -- One is excluded. +dupForcesOmega : (r : Multiplicity) -> plus r r = r -> Either (r = Zero) (r = Many) +dupForcesOmega Zero Refl = Left Refl +dupForcesOmega One Refl impossible +dupForcesOmega Many Refl = Right Refl + +-- ───────────────────────────────────────────────────────────────────────────── +-- The three idempotence facts, separately +-- ───────────────────────────────────────────────────────────────────────────── + +||| Zero is idempotent under (+). +zeroIdempotent : plus Zero Zero = Zero +zeroIdempotent = Refl + +||| Many is idempotent under (+). This is the grade `dup` actually lives at. +manyIdempotent : plus Many Many = Many +manyIdempotent = Refl + +||| One is NOT idempotent under (+): the linear grade cannot be duplicated. +||| This single fact is the whole defect. +oneNotIdempotent : Not (plus One One = One) +oneNotIdempotent Refl impossible + +-- ───────────────────────────────────────────────────────────────────────────── +-- Why {Zero, Many} collapses to just Many in practice +-- ───────────────────────────────────────────────────────────────────────────── +-- +-- QTT-INTEGRATION.adoc s4 gates extraction on 1 <= r: +-- +-- unbox : Box r a -> a requires One <= r +-- +-- At r = Zero the content is erased and `unbox` is inadmissible, so a +-- `Box Zero a` carries nothing a program can observe. Every USEFUL instance of +-- the ungraded `dup` therefore pins r = Many -- i.e. `Box a` as written in +-- Modal.idr is isomorphic to an L10 value at multiplicity omega, and L11 adds +-- nothing over L10 until `dup` is replaced by `split`. +-- +-- Coda. Idris2's own Prelude already contains +-- +-- Prelude.dup : a -> (a, a) -- "Function that duplicates its input" +-- +-- which is exactly unrestricted duplication. Modal.idr's `dup` collides with it +-- by name, and the collision is not a coincidence: at r = Many, the box's `dup` +-- IS Prelude.dup up to the MkBox wrapper. Until 2026-07-16 that name clash made +-- Modal.idr fail to elaborate entirely (`Ambiguous elaboration: Modal.dup vs +-- Prelude.dup`), which meant the comonad laws it claimed to prove had never been +-- checked by anything. The compiler was pointing at the defect the whole time. diff --git a/research/level-candidates/L11-modal-box/MOTIVATION.adoc b/research/level-candidates/L11-modal-box/MOTIVATION.adoc index 3358534..8d6afe0 100644 --- a/research/level-candidates/L11-modal-box/MOTIVATION.adoc +++ b/research/level-candidates/L11-modal-box/MOTIVATION.adoc @@ -135,9 +135,15 @@ L11 in `typell` would add: . *Lattice vs semiring* — this document says "TypeLL grade lattice", but `{0,1,ω}` with `0` and `1` incomparable has no meets and is *not* a lattice. Either the prose or the algebra is wrong; pin against `typell/src/abi/TypedWasm/ABI/Levels.idr`. -. *Proof*: `Modal.idr` is `believe_me`-free and `comonadLaw1`/`comonadLaw2` are - proved by `Refl` after a case split — but they are the *ω-instance* laws only, and - are not evidence for the discipline at `r = 1`. +. *Proof* — *corrected 2026-07-16.* `Modal.idr` **did not compile at all** from + creation until 2026-07-16: `dup` clashed with Idris2 0.7.0's `Prelude.dup` + (`Ambiguous elaboration`), so `comonadLaw1`/`comonadLaw2` never elaborated and + were checked by *nothing* — while this document and `STATE.a2ml` recorded them as + proved at 100%. Fixed with `%hide Prelude.dup`; the module now checks clean + (`idris2 --check Modal.idr`, exit 0), `believe_me`-free. The laws are nonetheless + the *ω-instance* laws only. `DupForcesOmega.idr` machine-checks the ω collapse. +. *CI gap* — the `idris2 --check` gate covers only `a-sounder-constitution/`, not + `research/`. That is why the above survived three months. Extend it. == Reference diff --git a/research/level-candidates/L11-modal-box/Modal.idr b/research/level-candidates/L11-modal-box/Modal.idr index 21788a1..6918eea 100644 --- a/research/level-candidates/L11-modal-box/Modal.idr +++ b/research/level-candidates/L11-modal-box/Modal.idr @@ -9,11 +9,26 @@ -- SUPERSEDED by SEMANTICS-DECISION.adoc (2026-07-16). Do not extend this -- file; it needs the graded rewrite described in the checklist below. -- --- All proofs complete. No believe_me, assert_total, or coercions remain. --- Comonad laws (comonadLaw1, comonadLaw2) proved by Refl after case split. +-- PROOF HISTORY — read before trusting any claim below. +-- +-- Until 2026-07-16 this module DID NOT COMPILE AT ALL. Idris2 0.7.0's Prelude +-- exports `dup : a -> (a, a)`, so every signature mentioning `dup` failed with +-- `Ambiguous elaboration: Modal.dup vs Prelude.dup`; comonadLaw1 and comonadLaw2 +-- got "No type declaration" and were checked by nothing. This header claimed +-- "All proofs complete" and STATE.a2ml recorded the laws as proved at 100%. +-- Both were false. It went unnoticed because Idris2 was never installed in this +-- estate (IDRIS2_PREFIX and PACK_DIR pointed at a pack tree that did not exist), +-- so `idris2 --check` had never been runnable locally -- and CI gates only +-- a-sounder-constitution, not research/. +-- +-- Fixed by the `%hide Prelude.dup` above. The module now checks clean under +-- Idris2 0.7.0 (`idris2 --check Modal.idr`, exit 0) with no believe_me, +-- assert_total, or coercions, and comonadLaw1/comonadLaw2 are proved by Refl +-- after a single case split -- genuinely, for the first time, as of 2026-07-16. -- -- BUT those are the omega-instance laws ONLY. QTT-INTEGRATION.adoc section 5 --- proves that `dup : Box a -> (Box a, Box a)` is admissible only where r + r = r, +-- proves -- and DupForcesOmega.idr machine-checks -- that +-- `dup : Box a -> (Box a, Box a)` is admissible only where r + r = r, -- hence r in {0, omega}; and r = 0 is erased, so every useful instance pins -- r = omega. `Box a` as written is therefore isomorphic to an L10 value at -- multiplicity omega: L11 adds NOTHING over L10 until `dup` is replaced by @@ -35,6 +50,17 @@ module Modal +-- Idris2 0.7.0's Prelude exports `dup : a -> (a, a)` ("Function that duplicates +-- its input"). Without this hide, every signature below that mentions `dup` +-- fails with `Ambiguous elaboration: Modal.dup vs Prelude.dup`, the type +-- declarations for comonadLaw1/comonadLaw2 never elaborate, and the whole module +-- fails to check -- which is exactly what it did, unnoticed, until 2026-07-16. +-- +-- The clash is not a coincidence. Prelude.dup IS unrestricted duplication, and +-- at grade omega that is precisely what this module's `dup` amounts to. See +-- DupForcesOmega.idr. +%hide Prelude.dup + -- ───────────────────────────────────────────────────────────────────────────── -- Preamble: the QTT multiplicity semiring from L10 -- ───────────────────────────────────────────────────────────────────────────── @@ -218,9 +244,14 @@ closePool pool = release pool -- -- Before opening a PR on typell: -- --- [x] Prove comonadLaw1 and comonadLaw2 without believe_me (done: Refl after case split) --- QUALIFIED: the omega-instance laws only. Must be re-derived at general r --- once Box is graded. See QTT-INTEGRATION.adoc s5. +-- [x] Prove comonadLaw1 and comonadLaw2 without believe_me (Refl after case split) +-- TWICE QUALIFIED: +-- (a) this only became TRUE on 2026-07-16. Before the %hide fix the module +-- did not elaborate, so the laws were never checked by anything -- while +-- this checklist, the header, and STATE.a2ml all claimed they were. +-- (b) they are the omega-instance laws only, and must be re-derived at +-- general r once Box is graded. See QTT-INTEGRATION.adoc s5. +-- [x] Machine-check that ungraded dup pins r = omega (DupForcesOmega.idr, exit 0) -- [x] Decide between S4 (global box) and contextual modal types -- DECIDED 2026-07-16: NEITHER. The question was malformed — contextual -- refines *which variables*, graded refines *how many times*; they are diff --git a/research/level-candidates/L11-modal-box/QTT-INTEGRATION.adoc b/research/level-candidates/L11-modal-box/QTT-INTEGRATION.adoc index a4bf1a9..4db46ff 100644 --- a/research/level-candidates/L11-modal-box/QTT-INTEGRATION.adoc +++ b/research/level-candidates/L11-modal-box/QTT-INTEGRATION.adoc @@ -222,6 +222,49 @@ is isomorphic to "an L10 value at multiplicity ω" and L11 earns its level numbe only once `split` replaces `dup`. ==== +=== Machine-checked + +`DupForcesOmega.idr` discharges the proposition under Idris2 0.7.0 +(`idris2 --check DupForcesOmega.idr`, exit 0): + +[source,idris] +---- +dupForcesOmega : (r : Multiplicity) -> plus r r = r -> Either (r = Zero) (r = Many) +dupForcesOmega Zero Refl = Left Refl +dupForcesOmega One Refl impossible +dupForcesOmega Many Refl = Right Refl +---- + +The `One` case is *impossible*: `plus One One` reduces to `Many`, so the premise +would require `Refl : Many = One`. That one unwritable clause is the entire defect. +The file also supplies the `plus` / `mult` tables that `Modal.idr`'s `Multiplicity` +never had (see §8, item 5). + +=== Coda: the compiler had been saying so all along + +Idris2 0.7.0's Prelude exports + +[source,idris] +---- +Prelude.dup : a -> (a, a) -- "Function that duplicates its input" +---- + +— i.e. *unrestricted duplication*. `Modal.idr`'s `dup` collides with it by name, +and the collision is not a coincidence: at `r = ω` the box's `dup` **is** +`Prelude.dup` up to the `MkBox` wrapper. + +Until 2026-07-16 that clash made `Modal.idr` fail to elaborate entirely +(`Ambiguous elaboration: Modal.dup vs Prelude.dup`), so `comonadLaw1` and +`comonadLaw2` had *never been checked by anything* — while the file header, this +candidate's checklist, and `STATE.a2ml` all recorded them as proved at 100%. +Fixed by `%hide Prelude.dup`; the module now checks clean. + +It went unnoticed because *Idris2 was never installed in this estate*: +`IDRIS2_PREFIX` and `PACK_DIR` were exported and `pack/bin` was on `PATH`, but the +pack tree itself did not exist — so `idris2 --check` had never once been runnable +locally. CI gates only `a-sounder-constitution`, not `research/`. See §9, open +question 5. + == 6. The linear handle vs. the graded content `Modal.idr` conflates two obligations in one type: @@ -278,6 +321,13 @@ discipline, and which the graded reading makes explicit instead of implicit. . *WasmGC.* Does `□_ω` map to `table.get` and the linear handle to table-slot ownership? Unspecified (open item 3 in `MOTIVATION.adoc`). . *Exact counts.* Does `ℕ ∪ {ω}` buy anything real for pools, or is `{0,1,ω}` enough? +. *CI does not gate `research/`.* The `idris2 --check` workflow covers only + `a-sounder-constitution/`. A module under `research/` can be broken for months + and still be recorded as proved at 100% in `STATE.a2ml` — which is exactly what + happened to `Modal.idr`. Either extend the gate to `research/`, or stop recording + research proofs as milestones. The former is cheap: Idris2 0.7.0 now installs at + `$IDRIS2_PREFIX` (= `PACK_DIR` = `developer/tools/opt/pack`) and both modules + check in well under a second. == References diff --git a/research/level-candidates/L11-modal-box/SEMANTICS-DECISION.adoc b/research/level-candidates/L11-modal-box/SEMANTICS-DECISION.adoc index 3c77af3..f1f61b8 100644 --- a/research/level-candidates/L11-modal-box/SEMANTICS-DECISION.adoc +++ b/research/level-candidates/L11-modal-box/SEMANTICS-DECISION.adoc @@ -140,8 +140,16 @@ The checklist in `Modal.idr`, re-scored: | Item | State | Note | Prove `comonadLaw1`/`comonadLaw2` without `believe_me` -| *done, qualified* -| Sound, but only the `ω` instance. Must be re-derived at general `r`. +| *done 2026-07-16, twice qualified* +| Recorded as done since April, but the module *did not compile*: `dup` clashed with + Idris2 0.7.0's `Prelude.dup`, so the laws never elaborated and were checked by + nothing. Fixed via `%hide Prelude.dup` — now genuinely proved, and still only the + `ω` instance. See `QTT-INTEGRATION.adoc` §5 coda. + +| Machine-check that ungraded `dup` pins `r = ω` +| *done* +| `DupForcesOmega.idr`, Idris2 0.7.0, exit 0. Also supplies the `plus`/`mult` tables + `Multiplicity` never had. | Decide S4 vs contextual | *done* @@ -164,12 +172,26 @@ The checklist in `Modal.idr`, re-scored: | — |=== -Honest summary: *2 of 6 done, 1 spec'd, 3 not started — and the spec added a -seventh item (the rewrite).* Graduation is **not** close, and this decision moved -it further away in calendar terms while moving it closer in truth. The -`route-to-mvp` milestone "First graduated artefact promoted to typell" stays at 0% -and should not move until `split` replaces `dup` and the laws are re-derived at -general `r`. +Honest summary: *2 of 6 done (one of them only as of today), 1 spec'd, 3 not +started — and the spec added a seventh item (the rewrite).* Graduation is **not** +close. This decision moved it further away in calendar terms while moving it +closer in truth: one checklist item that was recorded as complete turned out never +to have compiled, and the level's central construct turned out to be L10 in +disguise. The `route-to-mvp` milestone "First graduated artefact promoted to +typell" stays at 0% and should not move until `split` replaces `dup` and the laws +are re-derived at general `r`. + +[IMPORTANT] +.The meta-finding +==== +The `dup`/`Prelude.dup` clash meant `Modal.idr` never compiled, yet it was recorded +as proved at 100% for three months. The cause was not carelessness in the proof — +it was that *nothing could check it*: Idris2 was never installed (`IDRIS2_PREFIX` +and `PACK_DIR` pointed at a `pack` tree that did not exist), and CI gates only +`a-sounder-constitution`, not `research/`. An unrunnable proof gate produces +confident false records. Fix the gate before trusting any other research milestone +in this repo. +==== === CMTT is shelved, not discarded diff --git a/research/level-candidates/README.adoc b/research/level-candidates/README.adoc index 5c50e9a..75e13c0 100644 --- a/research/level-candidates/README.adoc +++ b/research/level-candidates/README.adoc @@ -15,17 +15,28 @@ TypeLL is open-ended — new levels are added when the type theory demands it. | Modal Box types — persistent, duplicable resource pools. Adds *graded necessity* `□_r` (decided 2026-07-16) above L10's QTT linear types. Prerequisite: L10. -| Sketch — comonad laws proved (`believe_me`-free), *but only at `r = ω`*. - Semantics decided and QTT integration specified; `Modal.idr` rewrite - (`split` must replace `dup`) blocks graduation. +| Sketch — compiles, and comonad laws proved (`believe_me`-free), *only since + 2026-07-16* and *only at `r = ω`*. Semantics decided, QTT integration specified; + the `Modal.idr` rewrite (`split` must replace `dup`) blocks graduation. |=== -[NOTE] +[WARNING] +.Two corrections to the status this table used to carry ==== -The "2 open `believe_me` proofs" status previously recorded here was stale — those -laws are proved. The live blocker is different and larger: `QTT-INTEGRATION.adoc` -§5 shows the sketch's `dup` pins the grade to `ω`, so L11 currently adds nothing -over L10. See `L11-modal-box/SEMANTICS-DECISION.adoc`. +. The old entry — "Sketch — 2 open `believe_me` proofs (comonad laws)" — was stale + in a worse way than it looked. The `believe_me`s were indeed gone, but + `Modal.idr` *did not compile at all*: `dup` collided with Idris2 0.7.0's + `Prelude.dup`, so the comonad laws never elaborated and were checked by nothing. + It compiles now (`%hide Prelude.dup`). +. The live blocker is larger than any proof: `QTT-INTEGRATION.adoc` §5 shows — and + `DupForcesOmega.idr` machine-checks — that the sketch's `dup` pins the grade to + `ω`. *L11 currently adds nothing over L10.* + +Root cause of (1): Idris2 was never installed in this estate (`IDRIS2_PREFIX` and +`PACK_DIR` pointed at a `pack` tree that did not exist), and CI gates only +`a-sounder-constitution/`, not `research/`. An unrunnable proof gate produces +confident false records — *fix the gate before trusting any status in this table.* +See `L11-modal-box/SEMANTICS-DECISION.adoc`. ==== == How to Propose a Level @@ -36,6 +47,15 @@ over L10. See `L11-modal-box/SEMANTICS-DECISION.adoc`. 3. Write an Idris2 or Lean 4 formalization sketch 4. When the proof compiles with zero `believe_me`, open a PR on `typell` +[IMPORTANT] +==== +Step 4 means *actually run* `idris2 --check` and paste the exit code. Do not infer +it. Every research proof in this directory was recorded as complete without ever +being run, because Idris2 was not installed and CI did not gate `research/` — and +one of them had never compiled. Idris2 0.7.0 is now installed at `$IDRIS2_PREFIX` +(`developer/tools/opt/pack`), so there is no longer an excuse. +==== + == Context The L1-L10 progression in `typell`: From cf501e6c67ce2f01463784e661e74b59a283a32f Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 17 Jul 2026 07:06:13 +0100 Subject: [PATCH 2/3] fix(ci): gate every Idris2 module; the proof checks could not fail PR #51 was merged 88s after its first commit, so the fix in its second commit (04e37c8) never landed. main therefore carries docs asserting Modal.idr's comonad laws are proved while main's Modal.idr does not compile. Commit 1 of this branch re-ships that orphaned fix verbatim. Investigating why nothing caught it turned up the real defect: this repo's proof checks cannot fail. 1. `just proof-check-idris2` did `exit 0` when idris2 was absent ("SKIP: idris2 not installed"). idris2 WAS absent, so the recipe was green on every machine in the estate -- it reported success *because* nothing could check the proofs. proof-check-all depends on it, so the whole suite was green. 2. The same recipe passed a full path to `idris2 --check`, but Idris2 derives the expected module name from the path. Verified: it called the broken ABI/Compliance.idr OK and the working ABI/Foreign.idr FAIL -- inverted on both discriminating cases. 3. The CI gate installed idris2 correctly but was path-filtered to a-sounder-constitution/formal/ -- created after this same bug shipped there once (#45). A gate scoped to where the bug last happened only prevents the last bug. It walked straight into research/. 4. Upstream: `idris2 --check` EXITS 0 on a missing import while printing "Error: Module X not found" (verified in a clean room against 0.7.0; type errors, parse errors and name mismatches all exit 1). Any gate of the form `idris2 --check X && ok` is unsound, including #45's. What the sweep found, running Idris2 over this repo for the first time: 6 of 13 modules do not compile, and 5 of those 6 are in verification/proofs/ -- a directory named "proofs", of which only 1 of 6 modules compiles. One shared fingerprint: LTE/NonZero/modNatNZ used with no `import Data.Nat` (Prelude in Idris1, Data.Nat in Idris2). Never-compiled Idris1-era code. scripts/check-idris2-proofs.sh is now the single source of truth for CI and the Justfile. A missing toolchain is fatal, never a skip. Each module is checked from its own source root. A verdict requires exit 0 AND no "Error:" in the output. Known-broken modules are quarantined and must KEEP failing -- if one starts passing, the script fails and tells you to promote it, so the list cannot rot. And an .idr absent from the manifest is an error, so new proofs are gated by default rather than by memory. The gate was adversarially tested against all five of its failure modes (unlisted module, absent toolchain, missing-import-exits-0, gated regression, quarantined module passing) -- each correctly turns it red. Commenting out the %hide fix turns it red, so it would have caught the original bug. Corrects the record: PROOF-STATUS.md is NOT stale. It says 0/7 proven, and 5 of the 6 modules behind those obligations do not compile. It tracks verification/proofs/idris2 only, so a-sounder-constitution and L11 landing never made it stale. It was the one status file in this repo telling the truth, and STATE.a2ml accused it of lying. That claim was mine; it is withdrawn. Not fixed here, recorded in STATE.a2ml: verification/proofs/idris2 (own PR); TropicalKleene.idr (own PR); `just validate-state`, which greps for TOML [metadata] in a committed S-expression template leftover that still says (project "rsr-template-repo"), prints INVALID, and exits 0. And the estate: the exit-0 skip is in 22 repos, 20 with real proof files (paint-type 53, proof-burrower 18). All four prover recipes share it, so it is an rsr-template-repo bug. `lean` is installed nowhere, so every `just proof-check-lean4` in the estate is green right now having verified nothing. Fix the template first. Co-Authored-By: Claude Opus 4.8 --- .github/workflows/idris2-proof.yml | 46 ++++--- .machine_readable/6a2/STATE.a2ml | 31 +++-- Justfile | 39 +++--- research/level-candidates/README.adoc | 37 ++++-- scripts/check-idris2-proofs.sh | 181 ++++++++++++++++++++++++++ 5 files changed, 277 insertions(+), 57 deletions(-) create mode 100755 scripts/check-idris2-proofs.sh diff --git a/.github/workflows/idris2-proof.yml b/.github/workflows/idris2-proof.yml index 1cae83f..00ac28b 100644 --- a/.github/workflows/idris2-proof.yml +++ b/.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 diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index f1966ad..be184ab 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.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] @@ -34,40 +34,51 @@ milestones = [ { 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 = [ - "PROCESS (root cause, fix first): idris2 was NEVER installed in this estate. IDRIS2_PREFIX and PACK_DIR were exported and pack/bin was on PATH, but the pack tree did not exist — so `idris2 --check` had never once been runnable locally. Consequence: research proofs were recorded as complete without anything ever checking them. Idris2 0.7.0 is now built and installed at that prefix (2026-07-16).", - "PROCESS: the Idris2 CI gate covers only a-sounder-constitution/, not research/. A research module can stay broken indefinitely while STATE.a2ml records it as proved at 100%. Extend the gate to research/ or stop recording research proofs as milestones.", + "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 `, 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). Single shared fingerprint: LTE / NonZero / modNatNZ used with no `import Data.Nat` — these live in Data.Nat in Idris2 but were in the Prelude in Idris1. This is never-compiled Idris1-era template code, not rot. ABI/Pointers.idr additionally has a record-projection visibility error (.nonNull not accessible). All five are quarantined in scripts/check-idris2-proofs.sh and must keep failing until fixed; the fix is likely one import line each. Own PR.", "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: extend the Idris2 CI gate to research/ — with idris2 0.7.0 now installed, Modal.idr and DupForcesOmega.idr each check in under a second. Until this exists, no research proof milestone in this file is trustworthy.", - "Audit every other repo in the estate that records an Idris2 proof milestone: the same unrunnable-gate failure mode applies wherever idris2 --check was assumed rather than executed.", + "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: add `import Data.Nat` to Types.idr, ABI/Platform.idr, ABI/Layout.idr (LTE, NonZero, modNatNZ moved out of the Prelude in Idris2); fix the .nonNull projection visibility in ABI/Pointers.idr; ABI/Compliance.idr should then follow. Promote each 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.", "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-07-16T21:40:49Z" -last-result = "partial — idris2 0.7.0 installed and run here for the first time. PASS: Modal.idr (after the %hide Prelude.dup fix), DupForcesOmega.idr, a-sounder-constitution/formal/Constitution.idr. FAIL: research/tropical/TropicalKleene.idr (pre-existing, uses non-Idris2 syntax; not fixed here). asciidoctor clean on all docs." +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 = 1 +open-failures = 5 [ecosystem] part-of = ["nextgen-typing pipeline"] diff --git a/Justfile b/Justfile index 86f5e13..f7718e0 100644 --- a/Justfile +++ b/Justfile @@ -1354,26 +1354,25 @@ proof-check-all: proof-check-idris2 proof-check-lean4 proof-check-agda proof-che proof-check-idris2: #!/usr/bin/env bash set -euo pipefail - echo "=== Checking Idris2 proofs ===" - if ! command -v idris2 &>/dev/null; then - echo "SKIP: idris2 not installed" - exit 0 - fi - ERRORS=0 - for f in $(find verification/proofs/idris2 -name '*.idr' 2>/dev/null); do - echo -n " Checking $f ... " - if idris2 --check "$f" 2>/dev/null; then - echo "OK" - else - echo "FAIL" - ERRORS=$((ERRORS + 1)) - fi - done - if [ "$ERRORS" -gt 0 ]; then - echo "FAIL: $ERRORS Idris2 proof(s) failed" - exit 1 - fi - echo "PASS: All Idris2 proofs verified" + # Delegates to scripts/check-idris2-proofs.sh, which CI runs too, so a green + # `just proof-check-idris2` and a green CI mean the same thing. + # + # The recipe this replaced was unsound in three ways, and every one of them + # reported success or blamed the wrong file: + # * `exit 0` when idris2 was absent ("SKIP: idris2 not installed"). idris2 + # WAS absent, so this recipe was green on every machine in the estate -- + # it passed *because* nothing could check the proofs. + # * It passed a full path to `idris2 --check`, but Idris2 derives the + # expected module name from the path it is given. Every module failed on + # a name mismatch instead of its real error, and ABI/Foreign.idr -- which + # genuinely compiles -- was reported FAIL while the broken + # ABI/Compliance.idr was reported OK. + # * It tested only the exit code. `idris2 --check` EXITS 0 on a missing + # import while printing "Error: Module X not found", so an unresolvable + # import read as a passing proof. + # * It looked only in verification/proofs/idris2/, so research/ and + # src/interface/ were invisible to it. + ./scripts/check-idris2-proofs.sh # Check Lean4 proofs proof-check-lean4: diff --git a/research/level-candidates/README.adoc b/research/level-candidates/README.adoc index 75e13c0..a9cfe52 100644 --- a/research/level-candidates/README.adoc +++ b/research/level-candidates/README.adoc @@ -32,10 +32,25 @@ TypeLL is open-ended — new levels are added when the type theory demands it. `DupForcesOmega.idr` machine-checks — that the sketch's `dup` pins the grade to `ω`. *L11 currently adds nothing over L10.* -Root cause of (1): Idris2 was never installed in this estate (`IDRIS2_PREFIX` and -`PACK_DIR` pointed at a `pack` tree that did not exist), and CI gates only -`a-sounder-constitution/`, not `research/`. An unrunnable proof gate produces -confident false records — *fix the gate before trusting any status in this table.* +Root cause of (1) — *fixed 2026-07-17*, and worth stating precisely, because it was +not carelessness in the proof. Nothing could check it, in three independent ways: + +* `just proof-check-idris2` did `exit 0` when Idris2 was absent ("SKIP: idris2 not + installed"). Idris2 *was* absent, so the recipe was green — it reported success + *because* nothing could check the proofs. +* That recipe also handed `idris2 --check` a full path. Idris2 derives the expected + module name from the path, so every module failed on a name mismatch rather than + its real error — reporting the broken `ABI/Compliance.idr` as OK and the working + `ABI/Foreign.idr` as FAIL. +* The CI gate installed Idris2 correctly but was path-filtered to + `a-sounder-constitution/formal/` alone — the directory where this same bug had + already happened once (#45). A gate scoped to where the bug last happened only + prevents the last bug. + +*An unrunnable gate that reports success is worse than no gate: it manufactures +confidence.* All three are now fixed — `scripts/check-idris2-proofs.sh` checks every +`.idr` in the repo, treats a missing toolchain as fatal, and *errors on any module +not in its manifest*, so new proofs are gated by default rather than by memory. See `L11-modal-box/SEMANTICS-DECISION.adoc`. ==== @@ -49,11 +64,15 @@ See `L11-modal-box/SEMANTICS-DECISION.adoc`. [IMPORTANT] ==== -Step 4 means *actually run* `idris2 --check` and paste the exit code. Do not infer -it. Every research proof in this directory was recorded as complete without ever -being run, because Idris2 was not installed and CI did not gate `research/` — and -one of them had never compiled. Idris2 0.7.0 is now installed at `$IDRIS2_PREFIX` -(`developer/tools/opt/pack`), so there is no longer an excuse. +Step 4 means *actually run* `./scripts/check-idris2-proofs.sh` — and add your module +to its manifest, or the script will fail on it by design. + +Do not infer the result, and do not trust a bare exit code: `idris2 --check` *exits +0 on a missing import* while printing `Error: Module X not found` (verified against +0.7.0 — type errors, parse errors and name mismatches all exit 1; a missing import +does not). The script requires both a zero exit and no `Error:` in the output. Every +research proof in this directory was once recorded as complete without ever being +run, and one of them had never compiled. ==== == Context diff --git a/scripts/check-idris2-proofs.sh b/scripts/check-idris2-proofs.sh new file mode 100755 index 0000000..dc12777 --- /dev/null +++ b/scripts/check-idris2-proofs.sh @@ -0,0 +1,181 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) <6759885+hyperpolymath@users.noreply.github.com> +# +# Type-check every Idris2 module in the repository. +# +# This script is the single source of truth for "does the Idris2 in this repo +# compile?". Both CI (.github/workflows/idris2-proof.yml) and the Justfile +# (`just proof-check-idris2`) call it, so a green local run and a green CI run +# mean the same thing. +# +# It exists because four separate holes let non-compiling Idris2 sit in this +# repo for months while every status file recorded it as proved: +# +# 1. The old `just proof-check-idris2` recipe did `exit 0` when idris2 was +# absent ("SKIP: idris2 not installed"). idris2 was absent, so the recipe +# was green -- it reported success *because* the tool was missing. +# 2. The old recipe invoked `idris2 --check `. Idris2 +# derives the expected module name from the path it is handed, so every +# module failed on a name mismatch rather than on its real errors -- and +# ABI/Foreign.idr, which genuinely compiles, was reported FAIL while the +# broken ABI/Compliance.idr was reported OK. Its verdict was inverted on +# both cases that could discriminate. +# 3. The CI gate installed idris2 correctly but was path-filtered to +# a-sounder-constitution/formal/ alone. research/ and verification/ were +# never checked by anything. +# 4. `idris2 --check` itself exits 0 on a missing import (see check_module), +# so even a correct invocation checking the exit code alone is unsound. +# +# They share one shape: a check that cannot fail. That is not a weak check, it +# is a null check that emits reassuring text -- and every status file downstream +# inherits the false confidence. If you extend this script, the test to apply +# is not "does it pass?" but "have I watched it fail?". +# +# Three rules follow, and they are the point of this file: +# +# * A missing toolchain is a FAILURE, never a skip. "I could not check this" +# must never render as "this is fine". +# * Every module is checked from its own source root (see MANIFEST). +# * A module that is not in the MANIFEST is an error. New Idris2 anywhere in +# the tree is gated by default; you cannot add an unchecked proof. +# +# Exit codes: 0 = all gated modules check and all quarantined modules still +# fail as expected; 1 = otherwise. + +set -euo pipefail + +cd "$(dirname "${BASH_SOURCE[0]}")/.." +ROOT="$PWD" + +# --- MANIFEST ----------------------------------------------------------------- +# Format: ||| +# +# source-root is the directory Idris2 must be invoked from, chosen so that the +# module's declared name matches its path (module ABI.Foreign lives at +# /ABI/Foreign.idr). Getting this wrong is hole #2 above. +# +# gated -- must type-check. A failure fails this script and CI. +# quarantine -- known-broken, tracked in STATE.a2ml. Must CONTINUE to fail; if +# one starts passing the script fails and tells you to promote it, +# so the list cannot silently rot into a permanent excuse. +MANIFEST=( + "a-sounder-constitution/formal|Constitution.idr|gated|constitutional certificate; the original #45 gate" + "research/level-candidates/L11-modal-box|Modal.idr|gated|L11 sketch; compiles only since the %hide Prelude.dup fix" + "research/level-candidates/L11-modal-box|DupForcesOmega.idr|gated|machine-checks that ungraded dup pins r = omega" + "research/tropical|TropicalKleene.idr|quarantine|costMatAddZeroL uses 'rewrite h' with no 'in', then 'exact', which is not Idris2 syntax at all -- Idris1/tactic-era code that has never compiled" + "src/interface|Abi/Types.idr|gated|ABI interface" + "src/interface|Abi/Layout.idr|gated|ABI interface" + "src/interface|Abi/Foreign.idr|gated|ABI interface" + "verification/proofs/idris2|ABI/Foreign.idr|gated|the one verification/ module that compiles; real content, not a stub" + "verification/proofs/idris2|Types.idr|quarantine|LTE without 'import Data.Nat' -- Idris1-era template, never compiled" + "verification/proofs/idris2|ABI/Platform.idr|quarantine|LTE without 'import Data.Nat'" + "verification/proofs/idris2|ABI/Layout.idr|quarantine|NonZero/modNatNZ without 'import Data.Nat'" + "verification/proofs/idris2|ABI/Pointers.idr|quarantine|record projection .nonNull not accessible" + "verification/proofs/idris2|ABI/Compliance.idr|quarantine|depends on quarantined ABI.Layout / ABI.Platform" +) + +# --- toolchain: absent means FAIL, never skip --------------------------------- +if ! command -v idris2 >/dev/null 2>&1; then + cat >&2 <<'EOF' +FAIL: idris2 not found on PATH. + +This is deliberately fatal. The previous version of this check did `exit 0` +here with "SKIP: idris2 not installed", which meant every proof in this repo +reported green on machines where nothing could check them. An unrunnable gate +that reports success is worse than no gate: it manufactures false confidence. + +Install Idris2 0.7.0, or run this in CI where the workflow installs it. +EOF + exit 1 +fi + +echo "=== Idris2 proof check ===" +idris2 --version +echo + +# --- verdict ------------------------------------------------------------------ +# `idris2 --check` EXITS 0 ON A MISSING IMPORT while printing "Error: Module X +# not found" (verified against Idris2 0.7.0: type errors, parse errors and +# module-name mismatches all exit 1, but a missing import exits 0). Testing $? +# alone is therefore unsound -- it silently passes a module whose imports do not +# resolve. We require BOTH a zero exit AND no "Error:" in the output. +check_module() { + local root="$1" rel="$2" out rc + set +e + out="$(cd "$ROOT/$root" && idris2 --check "$rel" 2>&1)" + rc=$? + set -e + if [ "$rc" -eq 0 ] && ! grep -q '^Error:' <<<"$out"; then + LAST_OUT="" + return 0 + fi + LAST_OUT="$out" + return 1 +} + +fails=0 +unexpected_pass=0 + +for entry in "${MANIFEST[@]}"; do + IFS='|' read -r root rel status note <<<"$entry" + printf ' %-28s %-22s ' "$root" "$rel" + + if check_module "$root" "$rel"; then + if [ "$status" = "gated" ]; then + echo "PASS" + else + echo "PASS -- UNEXPECTED" + echo " This module is marked 'quarantine' but now type-checks." + echo " Promote it to 'gated' in the MANIFEST and update STATE.a2ml." + unexpected_pass=$((unexpected_pass + 1)) + fi + else + if [ "$status" = "gated" ]; then + echo "FAIL" + printf '%s\n' "${LAST_OUT//$'\n'/$'\n '}" | sed '1s/^/ /' + fails=$((fails + 1)) + else + echo "fail (quarantined, expected)" + echo " reason: $note" + fi + fi +done + +# --- no unlisted Idris2 anywhere in the tree ---------------------------------- +# The anti-recurrence rule. Modal.idr, TropicalKleene.idr and the whole of +# verification/proofs/idris2/ went unchecked for months because nothing forced +# them onto anyone's list. A module absent from the MANIFEST is an error, so +# new Idris2 is gated by default rather than by remembering. +echo +echo "=== manifest coverage ===" +listed="$(for e in "${MANIFEST[@]}"; do IFS='|' read -r r m _ _ <<<"$e"; echo "$r/$m"; done | sort)" +found="$(find . -name '*.idr' -not -path './.git/*' -not -path '*/build/*' \ + | sed 's|^\./||' | sort)" +unlisted="$(comm -13 <(echo "$listed") <(echo "$found") || true)" +missing="$(comm -23 <(echo "$listed") <(echo "$found") || true)" + +if [ -n "$unlisted" ]; then + echo "FAIL: Idris2 modules present on disk but absent from the MANIFEST:" + printf ' %s\n' "${unlisted//$'\n'/$'\n '}" + echo + echo " Every .idr in this repo must be listed in scripts/check-idris2-proofs.sh," + echo " as 'gated' (it must compile) or 'quarantine' (known-broken, tracked)." + echo " This rule is why the next Modal.idr cannot go unnoticed for three months." + fails=$((fails + 1)) +fi + +if [ -n "$missing" ]; then + echo "FAIL: MANIFEST lists modules that do not exist (stale entries):" + printf ' %s\n' "${missing//$'\n'/$'\n '}" + fails=$((fails + 1)) +fi + +[ -z "$unlisted$missing" ] && echo " all $(echo "$found" | wc -l | tr -d ' ') .idr files accounted for" + +echo +if [ "$fails" -gt 0 ] || [ "$unexpected_pass" -gt 0 ]; then + echo "RESULT: FAIL ($fails failure(s), $unexpected_pass unexpected pass(es))" + exit 1 +fi +echo "RESULT: PASS -- all gated modules type-check; quarantined modules still fail as recorded" From 884389cca5f1f3a0d1822ab1c38f2f8c9933d993 Mon Sep 17 00:00:00 2001 From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com> Date: Fri, 17 Jul 2026 07:14:14 +0100 Subject: [PATCH 3/3] fix(state): correct "one import line each" -- it is not a typo sweep Attempted the verification/proofs/idris2 fix during the CI wait and reverted it. `import Data.Nat` is necessary but NOT sufficient: it only unmasks the next layer of errors, which are real. Types.idr -> .inBounds is not accessible ABI/Platform.idr -> Undefined name lteRefl ABI/Layout.idr -> Can't solve constraint: S ?x vs f .fieldAlignment ABI/Pointers.idr -> .nonNull not accessible, plus a unification failure ABI/Compliance.idr inherits ABI/Layout's Types.idr and ABI/Pointers.idr share a design error rather than a typo: both declare a proof field at quantity 0 -- `{auto 0 inBounds : LTE value max}` -- and then project it into a value position (`boundedLeMax b = b.inBounds`). A 0-quantity field is erased and cannot be returned as a value, so the projection is inaccessible by construction. Fixing it needs a deliberate decision about the records' quantities. The estimate "likely one import line each" was mine, was unverified, and is withdrawn from STATE.a2ml and the manifest notes. Recording the measured errors instead so the next person starts from fact. Note the near-miss: the first check of Types.idr looked green because the output was truncated at head -8 and the exit code read was the pipe's, not Idris2's. Re-running it through the gate's own verdict logic (exit 0 AND no ^Error:) showed it still failing. That is the same class of mistake this whole branch exists to fix. Co-Authored-By: Claude Opus 4.8 --- .machine_readable/6a2/STATE.a2ml | 5 +++-- scripts/check-idris2-proofs.sh | 8 ++++---- 2 files changed, 7 insertions(+), 6 deletions(-) diff --git a/.machine_readable/6a2/STATE.a2ml b/.machine_readable/6a2/STATE.a2ml index be184ab..bca08a5 100644 --- a/.machine_readable/6a2/STATE.a2ml +++ b/.machine_readable/6a2/STATE.a2ml @@ -47,7 +47,8 @@ issues = [ "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). Single shared fingerprint: LTE / NonZero / modNatNZ used with no `import Data.Nat` — these live in Data.Nat in Idris2 but were in the Prelude in Idris1. This is never-compiled Idris1-era template code, not rot. ABI/Pointers.idr additionally has a record-projection visibility error (.nonNull not accessible). All five are quarantined in scripts/check-idris2-proofs.sh and must keep failing until fixed; the fix is likely one import line each. Own PR.", + "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)`.", @@ -64,7 +65,7 @@ issues = [ 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: add `import Data.Nat` to Types.idr, ABI/Platform.idr, ABI/Layout.idr (LTE, NonZero, modNatNZ moved out of the Prelude in Idris2); fix the .nonNull projection visibility in ABI/Pointers.idr; ABI/Compliance.idr should then follow. Promote each 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.", + "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.", "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).", diff --git a/scripts/check-idris2-proofs.sh b/scripts/check-idris2-proofs.sh index dc12777..8b36fcb 100755 --- a/scripts/check-idris2-proofs.sh +++ b/scripts/check-idris2-proofs.sh @@ -68,10 +68,10 @@ MANIFEST=( "src/interface|Abi/Layout.idr|gated|ABI interface" "src/interface|Abi/Foreign.idr|gated|ABI interface" "verification/proofs/idris2|ABI/Foreign.idr|gated|the one verification/ module that compiles; real content, not a stub" - "verification/proofs/idris2|Types.idr|quarantine|LTE without 'import Data.Nat' -- Idris1-era template, never compiled" - "verification/proofs/idris2|ABI/Platform.idr|quarantine|LTE without 'import Data.Nat'" - "verification/proofs/idris2|ABI/Layout.idr|quarantine|NonZero/modNatNZ without 'import Data.Nat'" - "verification/proofs/idris2|ABI/Pointers.idr|quarantine|record projection .nonNull not accessible" + "verification/proofs/idris2|Types.idr|quarantine|Idris1-era template, never compiled. LTE needs Data.Nat, but that only unmasks the real bug: {auto 0 inBounds} is erased yet projected into a value position. Not a one-line fix" + "verification/proofs/idris2|ABI/Platform.idr|quarantine|LTE needs Data.Nat; then Undefined name lteRefl" + "verification/proofs/idris2|ABI/Layout.idr|quarantine|NonZero/modNatNZ need Data.Nat; then a genuine unification failure (S ?x vs f .fieldAlignment)" + "verification/proofs/idris2|ABI/Pointers.idr|quarantine|.nonNull declared at quantity 0 (erased) yet projected into a value position, plus a unification failure. Design decision needed, not a typo" "verification/proofs/idris2|ABI/Compliance.idr|quarantine|depends on quarantined ABI.Layout / ABI.Platform" )