Repository navigation
62 of 67 DISCHARGED proof claims have never been verified; 4 confirmed false #211
Description
src/**/*.idr carries 67 DISCHARGED docstring claims across 23 files. A DISCHARGED marker
asserts that a proof obligation has been met. Nothing checks it.
| Count | |
|---|---|
Total DISCHARGED claims |
67, in 23 files |
Written during this campaign, each verified rc=0 at the time of writing |
5 |
| Pre-existing and never verified | 62 |
| Confirmed false so far | 4 |
The four confirmed-false claims were found incidentally — they surfaced while the build was being
driven forward, not by any search for them. The 62 have not been audited, so 4 is a floor, not
an estimate.
Why this is the highest-severity item on the list
A false DISCHARGED is strictly worse than an OWED marker. OWED is honest debt and shows up in
the debt register. DISCHARGED is a claim of completion that silences the register — it removes
the obligation from view while leaving it undischarged. The same shape as this repo's
believe_me = 0 badge: literally true, and the debt was relocated rather than met.
The audit instrument already exists
The build is the audit. Every module that compiles rc=0 with --total has had its
DISCHARGED claims mechanically checked, because a false claim in a proof body cannot typecheck.
So this issue is largely discharged as a side effect of finishing the build — which is a strong
additional reason to finish it.
What is needed beyond that:
- Enumerate all 67 with file:line.
- Mark the 62 unverified ones
DISCHARGED (UNVERIFIED)until their module compiles clean. - Add a gate: a
DISCHARGEDclaim in a module that does not compile--totalis a build failure.
Context: docs/IDRIS2-BUILD-WORK-PACKAGE.adoc §5.2.
Activity
fix(idris2): cure seven build blockers — build goes VOID → RED, front…
hyperpolymath commentedon Nov 4, 2026
Scoped fresh evidence from the assurance audit: Idris2 0.7.0 compiled Proven.SafeOrdering at proven commit 5360032 through proven-tests-and-benches/scripts/prove-proven-ordering.sh; all eight law checks ran and passed. Framework repair/evidence: hyperpolymath/proven-tests-and-benches#103. This does not validate the other DISCHARGED claims or current proven main.
One correction to the proposed audit criterion: compiling a module with --total checks its actual terms and totality obligations; it does not establish that a DISCHARGED prose marker corresponds to a theorem, that the theorem states the intended requirement, or that a foreign implementation refines it. The inventory needs marker → explicit statement → proof term → checked source/toolchain digest, plus declared assumptions and a separate runtime/FFI correspondence obligation. A module compile is necessary evidence for its checked terms, not sufficient validation of every comment claim.
The cross-repository receipt in cicd-suite PR #77 keeps this boundary explicit. No full proven build or closure of this issue is claimed.