fix(a-sounder-constitution): make the Idris2 proof compile + machine-check it (Idris2 0.7.0) - #45
Merged
Merged
Conversation
…s2 0.7.0 The proof shipped in #29 did not type-check: it referenced `lteRefl`, which does not exist in Idris2 0.7.0's Data.Nat (it is the `reflexive` interface method), and `soundMonotone`'s `a` was an erased auto-implicit so `rank a` was not accessible in the `Keep` case. - Inline a small `lteRefl : {n : Nat} -> LTE n n` lemma so the module needs only `import Data.Nat`. - Bind `{a : Person}` explicitly in `soundMonotone` so it is relevant. - Update the verification-status notes (Constitution.idr header, formal/README, top-level README) from "pending" to machine-checked. Verified: `idris2 --check formal/Constitution.idr` => exit 0, clean, with `%default total` in force and zero believe_me / assert_total / postulate (Idris2 0.7.0). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6
hyperpolymath
marked this pull request as ready for review
June 27, 2026 18:56
|
hyperpolymath
added a commit
that referenced
this pull request
Jun 27, 2026
…k` (#46) ## Wire `idris2 --check` into CI Follow-up to #45. That PR fixed a proof that had been merged claiming to compile but didn't — because nothing ever ran Idris2 on it. This adds the missing gate so it can't happen again. ### What it does `.github/workflows/idris2-proof.yml`: 1. installs Chez Scheme (the Idris2 backend) via apt, 2. builds & installs **Idris2 0.7.0** from the v0.7.0 source tarball (bootstrap), and 3. runs `idris2 --check a-sounder-constitution/formal/Constitution.idr`. ### Conventions followed - **Path-filtered** to `a-sounder-constitution/formal/**` + the workflow file, so it only runs when the proof actually changes — keeps Actions burn low (the reason there's no caching: the repo pins no `actions/cache` SHA, and I won't introduce an unverifiable pin; a source build only fires on rare proof edits). - Passes `workflow-linter.yml`: SPDX header on line 1, top-level `permissions: contents: read`, all `uses:` SHA-pinned (`actions/checkout@de0fac2e…`), `concurrency` guardrail with `cancel-in-progress`. - `formal/README.adoc` updated to note CI now enforces the check. ### Verified locally (in the cloud session, where Idris2 0.7.0 is installed) - `python3 -c 'yaml.safe_load(...)'` → YAML valid - the three linter rules (SPDX / permissions / SHA-pin) → all pass - `idris2 --check formal/Constitution.idr` → exit 0, clean The workflow's own build path (apt `chezscheme` → tarball → `make bootstrap`/`install`) is exactly the sequence used to verify #45, so it mirrors a known-good install. It will run for the first time on this PR (it touches `formal/README.adoc`, matching the path filter), so CI here is itself the end-to-end test. Scope: one new workflow + one doc note. No code or simulator behaviour touched. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6 --- _Generated by [Claude Code](https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6)_ Co-authored-by: Claude <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Jul 17, 2026
…and #51's fix never landed) (#52) ## Why this exists **PR #51 was merged 88 seconds after its first commit landed.** Its second commit — the one with the actual fix — was pushed ten minutes *later*, to a branch whose PR was already closed. It never landed. | Event | Time (UTC) | |---|---| | `cf7f211` pushed (docs) | 21:30:50 | | **#51 merged** | **21:32:18** | | `04e37c8` committed (the fix) | 21:42:55 | So `main` right now says *"comonad laws proved (`believe_me`-free)"* while `main`'s `Modal.idr` **does not compile**. The docs made `main` sound more authoritative while the fix sat on a dead branch. **Commit 1 re-ships `04e37c8` verbatim** (tree-identical; verified). Then I asked why nothing caught it, and that turned out to be the real bug. ## The real defect: this repo's proof checks cannot fail | # | Hole | Effect | |---|---|---| | 1 | `just proof-check-idris2` did `exit 0` when idris2 was absent | idris2 **was** absent → recipe green on every machine. It passed **because** nothing could check the proofs. | | 2 | Same recipe passed a **full path** to `idris2 --check` | Idris2 derives module name from path → **verdict inverted**: broken `ABI/Compliance.idr` → *OK*; working `ABI/Foreign.idr` → *FAIL* | | 3 | CI gate path-filtered to `a-sounder-constitution/formal/` | Created after this same bug shipped there once (**#45**) — then it walked into `research/` | | 4 | **Upstream:** `idris2 --check` **exits 0 on a missing import** | `idris2 --check X && ok` is unsound — including #45's own gate | Hole 4, verified in a clean room against 0.7.0: | Failure mode | Exit | |---|---| | **Missing import** | **0** ← | | Type error | 1 | | Parse error | 1 | | Module name mismatch | 1 | They share one shape: **a check that cannot fail.** That's not a weak check, it's a null check that emits reassuring text — and every status file downstream inherits the false confidence. ## What the first-ever full sweep found **6 of 13 modules don't compile. Five are in `verification/proofs/` — a directory named _proofs_, where only 1 of 6 modules compiles.** One shared fingerprint: `LTE` / `NonZero` / `modNatNZ` used with **no `import Data.Nat`**. Those were Prelude in Idris**1**, `Data.Nat` in Idris**2**. This is never-compiled Idris1-era code, not rot. ## The fix `scripts/check-idris2-proofs.sh` — single source of truth for CI **and** the Justfile, so local green and CI green mean the same thing: - **Missing toolchain is fatal**, never a skip - Each module checked **from its own source root** - Verdict = **exit 0 AND no `Error:`** in output (defeats hole 4) - **Quarantine must keep failing** — if one starts passing, the script fails and tells you to promote it, so the list can't rot - **An `.idr` absent from the manifest is an error** — new proofs are gated by default rather than by memory ### The gate was tested by watching it fail A gate never observed failing is the bug under investigation, so: | Test | Result | |---|---| | Unlisted `.idr` in tree | ✅ red | | idris2 absent | ✅ red (was green) | | Missing import (bare idris2 exits **0**) | ✅ red | | Gated module regresses (un-`%hide` the fix) | ✅ red — **would have caught the original** | | Quarantined module starts passing | ✅ red, demands promotion | Result: 8 gated PASS · 5 quarantined fail as recorded · 13/13 accounted for. ## Correcting the record **`PROOF-STATUS.md` is NOT stale.** It says *0/7 proven* — and 5 of the 6 modules behind those obligations don't 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's withdrawn. Also softened: *"idris2 was never installed in this estate"* is too strong — committed `.ttc` artefacts show it ran somewhere around Aug 2025. ## Not fixed here (recorded in `STATE.a2ml`) - **`verification/proofs/idris2/` — attempted during the CI wait and reverted; it is NOT a typo sweep.** `import Data.Nat` is necessary but only unmasks the next layer: | Module | Error after the import | |---|---| | `Types.idr` | `.inBounds` 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 + unification failure | `Types.idr` and `ABI/Pointers.idr` share a **design error, not 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 — inaccessible by construction. Needs a deliberate decision about the records' quantities. My earlier estimate "one import line each" was unverified and is **withdrawn** (commit `884389c`). Near-miss worth recording: the first check of `Types.idr` *looked* green because output was truncated at `head -8` and the exit code read was the pipe's, not Idris2's. Re-run through this branch's own verdict logic (exit 0 **and** no `^Error:`), it still failed — the same class of mistake this branch exists to fix. - `TropicalKleene.idr` (own PR) - **`just validate-state` has never validated this project**: it greps for TOML `[metadata]` in a *committed S-expression template leftover* that still says `(project "rsr-template-repo")`, prints `INVALID`, and **exits 0** ##⚠️ Estate-wide, measured not guessed The `exit 0` skip is **rsr-template-repo's**, in **22 repos — 20 with real proof files** (paint-type 53, ideas-to-alphas 31, proof-burrower 18, snifs 15). **All four prover recipes share it** (idris2/lean4/agda/coq). **Live right now: `lean` is installed nowhere, so every `just proof-check-lean4` in the estate is green having verified nothing.** Fix the template first, or it re-seeds. Detection: `grep -rlE 'SKIP:.*not installed' */Justfile` 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
hyperpolymath
added a commit
that referenced
this pull request
Aug 28, 2026
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 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Make the Idris2 certificate actually compile
The proof shipped in #29 was written "to compile clean" but had not been run through Idris2 (none was on PATH in the cloud session). I've since installed Idris2 0.7.0 and checked it — and it did not type-check as merged. Two genuine fixes:
lteRefldoesn't exist in Idris2 0.7.0'sData.Nat(LTE-reflexivity is thereflexiveinterface method). → inlined a smalllteRefl : {n : Nat} -> LTE n nlemma, so the module needs onlyimport Data.Nat.soundMonotone'sawas an erased auto-implicit, sorank awasn't accessible in theKeepcase. → bound{a : Person}explicitly to make it relevant.Also flips the verification-status notes (the
Constitution.idrheader,formal/README.adoc, and the top-levelREADME.adocStatus line) from "pending CI" to machine-checked.Verification
Clean,
%default totalin force, zerobelieve_me/assert_total/postulate, on Idris 2, version 0.7.0. The substantive claims (soundNeverProperty,soundMonotone,SoundRestrict) all hold; only thesoundMonotoneplumbing changed.Scope:
formal/+ one README status line. No JS, dependencies, or simulator behaviour touched.🤖 Generated with Claude Code
https://claude.ai/code/session_015w8C1xaGwiDcHHjfuxHBd6
Generated by Claude Code