verification/PROOF-STATUS.adoc is stale: wrong path, wrong LOC, wrong proofs

What

verification/PROOF-STATUS.adoc describes a file that no longer looks like
what it describes.

It records src/abi/Types.idr as 140 LOC, proving "Confidence refined
type, Severity ordering". The live module — src/Hypatia/ABI/Types.idr, which
is what the ipkg actually compiles — is 242 lines and its principal content
is the Connector datatype, connectorWireId, connectorName,
connectorPort and the proof connectorCount : length allConnectors = 16.

So the document names the dead path (see the duplicate-modules issue), states a
wrong line count, and lists the wrong proofs.

A proof-status document that is wrong is worse than one that is missing: it is
read as evidence.

Acceptance criteria

Every row is re-derived by running a command, not by editing the number
that is there. Line counts from wc -l, proof names from the source.
The path column points at src/Hypatia/ABI/, not src/abi/.
connectorCount = Refl appears, since it is the live pin on the
16-connector wire contract and PR feat(abi): generate the Zig and Rust wire enums from the normative Idris2 ABI (#120) #811's drift gate deliberately declines
to re-assert 16 on the grounds that this proof owns it.
A check exists that can make this document go stale loudly — at
minimum, a CI step asserting each named file exists and each named proof
name is present in it. A document nothing verifies will rot again.
That check is proven by a mutant: rename one proof, confirm red.

Heads-up from #815 / PR #821: the six paths this issue's table cites no longer exist.

PR #821 deletes src/abi/{Types,FFI,GRPC,GraphQL,REST,RuleEngine}.idr — byte-identical dead copies that hypatia-abi.ipkg never compiled (its sourcedir = ".." resolves to src/, so it builds src/Hypatia/ABI/*.idr).

I deliberately left verification/PROOF-STATUS.adoc entirely alone rather than half-fixing it, because this issue owns the path column and two PRs editing the same six rows would collide. So after #821 merges, all six rows at lines 22, 25, 29, 32, 35 and 38 point at files that are gone, and the fix here is a repoint to src/Hypatia/ABI/… rather than a correction of the old paths.

One extra reference for the scope of this issue, not in the table: line 266, the directory-tree diagram, reads

├── src/abi/  # Idris2 ABI definitions + proofs (1027 LOC)

After #821 that directory holds only hypatia-abi.ipkg, hypatia-abi-gen.ipkg and README.adoc, so both the description and the LOC figure need to move to src/Hypatia/ABI/.

Also worth folding into the LOC column while you are in here: the live Types.idr is 242 lines and defines the 16-connector Connector wire contract, not the "140 LOC / Confidence refined type, Severity ordering" the table currently claims — and the live tree now contains a seventh module, Gen.idr (the generator added by #120), which the table has no row for at all.

🤖 Generated with Claude Code

https://claude.ai/code/session_0113HQM9LVGkNCzU1WwkJZSV

Delete the six duplicated src/abi/*.idr modules and repoint every ref…

Advanced by #835 on ACs 1-3. Not closed — ACs 4 and 5 are unreachable today,
and this comment records why, with the measurement.

AC1 — superseded, deliberately

AC1 asked for the LOC column to be re-derived from wc -l. On measuring it,
all twenty figures were wrong, several by more than 100%
(GRPC.idr recorded ~150, actual 64; GraphQL.idr ~200, actual 93;
VerisimdbConnector.idr ~110, actual 175). Nothing reads the column. A
re-derived hand-written number drifts again on the first edit, so #835 deletes
the column, the two derived total lines and the duplicate "File Locations" file
tree instead, with a NOTE recording why so it is not restored.

AC2, AC3 — landed

Paths repointed to src/Hypatia/ABI/, and the Types.idr row now names
connectorCount : length allConnectors = 16. The removed "Severity ordering"
claim was provably false — src/Hypatia/ABI/Types.idr:157-159 says so itself:
"has never existed in this module; connectorCount is the real pin."

AC4 / AC5 — blocked, with the measurement

AC4 wants a live CI check that fails when the document drifts; AC5 wants a mutant
proving it goes red. Both candidate homes fail:

ExUnit is not a home — the whole tier is dead. There is exactly one mix test
in the repository, .github/workflows/tests.yml:347, inside integration-tests.
That job declares needs: [build-images], and Build Test Images fails, so
Integration Tests resolves to skipped. Measured on the run for 3bf9674a:

Build Test Images    failure
Integration Tests    skipped      <- the only mix test in the repo

Every ExUnit test in hypatia therefore executes nowhere. Filed separately.

A new workflow needs workflow token scope, which this session's credential
has lost (current scopes: admin:public_key, gist, read:org, repo).

When the scope is restored, the correct home — and a trap in it

verify-proofs.yml. It already bootstraps Idris2 v0.7.0 with a warm cache, and
it demonstrably runs.

⚠ Its paths: filter covers verification/proofs/* but not
verification/*.adoc. A gate on PROOF-STATUS.adoc added there unmodified
would never fire on a change to its own subject — the filter/required deadlock
this estate has already hit. Widen the filter to include
verification/PROOF-STATUS.adoc, or give the gate its own unfiltered workflow.

AC5's mutant, concretely: repoint one table row back to src/abi/Types.idr
and confirm the gate goes red on a path failure, not a parse error; reverting
restores green. The gate must print its denominator (N rows checked) — a check
that cannot state how many rows it verified is not evidence.

docs: repoint the 8 surviving src/abi/*.idr references and drop the L…

Correction to my previous comment, and a second class of defect #835 missed

1. The "twenty wrong LOC figures" claim was itself an overclaim.

I wrote that "every one of the twenty" hand-written LOC figures in
PROOF-STATUS.adoc was wrong. Re-checking my own measurement table: sixteen
were wrong. Four tilde-approximations landed within two lines of the truth:

File	documented	actual
`PageRankInvariants`	~120	120
`ESNSpectralScaling`	~145	144
`BayesianUpdate`	~190	188
`ParserTotality`	~190	191

The decision does not change — 16/20 wrong, several by more than double, with no
consumer, still means the column was drift surface rather than information. But
the NOTE that #835 wrote into the document carried the false figure, i.e. a
wrong count inside a note explaining why wrong counts are unacceptable. Fixed in
#839.

2. #835 fixed only the half of the defect its regex could see.

The acceptance test I used was git grep -nE 'src/abi/[A-Za-z]+\.idr' — it
matches references naming a file. It is structurally blind to prose naming
the directory and asserting it holds the Idris2 ABI, which is the same false
claim in a different shape. Eight such sites survived #835 untouched:

docs/EXPLAINME.adoc:76,119
docs/operations/prover-wars-integration.adoc:39
docs/proofs/gap-analysis.adoc:79
docs/quickstart/llm-warmup-dev.adoc:117
docs/quickstart/llm-warmup-user.adoc:47
docs/quickstart/user.adoc:43
docs/wiki-pages/Architecture.md:102

The probe that finds this class — grep the path, filter by claim
vocabulary, then read each hit, because roughly half the survivors are
legitimate:

git grep -n 'src/abi/' -- . ':!data/' | grep -iE 'idris|proof|\.idr|module'

Of the 20 hits that survive #839, every one is an ipkg/build reference (correct
— sourcedir = ".."), past-tense history of the deleted duplicates (correct
because it names the old path), or the src/abi/README.adoc title. A
path-level search-and-replace would have broken all of them.

Two stated module counts were wrong alongside the paths and are fixed in #839:
five modules listed against seven live ones — RuleEngine.idr and Gen.idr
were absent from every enumeration.

ACs 4–5 remain blocked exactly as previously recorded: ExUnit is dead in CI
(#836) and a new workflow needs the workflow token scope. verify-proofs.yml
is still the correct home, and its paths: filter still covers
verification/proofs/* but not verification/*.adoc, so whoever builds the
gate must widen the filter or it deadlocks on its own subject.

docs: correct 8 prose sites claiming src/abi/ holds the Idris2 modules (

fix: address the open issue set — CI truth, proof gates, scanner prec…

Navigation Menu

Repository navigation

verification/PROOF-STATUS.adoc is stale: wrong path, wrong LOC, wrong proofs #816

What

Acceptance criteria

AC1 — superseded, deliberately

AC2, AC3 — landed

AC4 / AC5 — blocked, with the measurement

When the scope is restored, the correct home — and a trap in it

Correction to my previous comment, and a second class of defect #835 missed

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

verification/PROOF-STATUS.adoc is stale: wrong path, wrong LOC, wrong proofs #816

Description

What

Acceptance criteria

Activity

hyperpolymath commented on Sep 22, 2026

hyperpolymath commented on Sep 22, 2026

AC1 — superseded, deliberately

AC2, AC3 — landed

AC4 / AC5 — blocked, with the measurement

When the scope is restored, the correct home — and a trap in it

hyperpolymath commented on Sep 22, 2026

Correction to my previous comment, and a second class of defect #835 missed

Metadata

Metadata

Assignees

Labels

Projects

Milestone

Relationships

Development

Issue actions