Census: 91 of 379 .idr files have own compile defects (47 parse failures) — revealed by fixing the module-1 stall

[hyperpolymath]

Summary

A per-file idris2 --find-ipkg --check census of all 379 .idr files under src/,
with each failure attributed to own-defect vs import-inherited:

	count
clean	233
failing — own defect	91
failing — inherited from an import only	52
unattributable	0
stalls (do not terminate)	3

Of the 91 own-defect files, 47 are parse failures.

Dominant error classes among own defects:

• 31 — Couldn't parse declaration
• 16 — Couldn't parse any alternatives
• 8 — When unifying
• 2 — Keyword 'public' is not a valid start to a declaration
• singletons: ffi_resource_new_handle is already defined, ffi_lru_new is already defined, Name Proven.SafeCron.minuteBounds is private, Multiple solutions found in search of, levelorder is not total, isTemplateSafe is not total, Expected 'where'

Concentration: Proven (20), Proven.FFI (13), then 2 each in SafeTOML, SafeHtml,
SafeHeader, SafeCookie, SafeContentType, SafeArgs.

⚠ These are authoring defects, not sweep damage

The parse-failure cluster looks at first glance like it could be substitution damage. It
is not. Sampling src/Proven/FFI/Buffer.idr:

ffi_buffer_write buf data = ...

data is a reserved keyword in Idris2. That file is clean vs HEAD — no sweep has
touched it. This appears to be the dominant sub-class of the parse failures, and it means
remediation is ordinary source fixing, not a revert.

Why this was invisible

The package build stopped at module 1 of 300 (non-terminating elaboration) and was
cancelled at the CI timeout, so no diagnostic was ever emitted for any of these files.
The whole set was behind a VOID gate.

Data

• .claude/forensics/proven-idr-file-census-2026-08-27.txt — rc|elapsed|file|firstError, 379 rows
• .claude/forensics/proven-idr-defect-attribution-2026-08-27.txt — OWN|IMPORT|NOLOC per failing file

Census taken against the working tree; 375/379 files identical to HEAD c83c7bf3.

[hyperpolymath]

Correction to this issue's central causal claim — measured, 2026-08-27

This issue states, under the heading "⚠ These are authoring defects, not sweep damage":

The parse-failure cluster looks at first glance like it could be substitution damage. It is not.
Sampling src/Proven/FFI/Buffer.idr: … data is a reserved keyword in Idris2. … This appears to
be the dominant sub-class of the parse failures.

That generalisation is wrong for 83 % of the cluster, and the sample that produced it was drawn
from the one subtree where it holds. Correcting my own record.

What was actually measured

postulate is not an Idris2 keyword (v0.7.0 answers Couldn't parse declaration; absent from
the changelog for v0.2.0–v0.8.0). Commit 6c80e0b5 "[P1] Explicit postulate sweep (Fork A) (#189)"
injected it in declaration position across the tree, making every affected file unparseable.

On pristine origin/main, Idris2 0.7.0, comment lines excluded:

	Files	Occurrences
Raw grep (^|[[:space:]])postulate[[:space:]]	46	369
Declaration position only	42	360
Comment-only mentions (-- / |||)	4	9

Intersected against this issue's 47 OWN-defect parse failures:

Set	Count	Reading
Both — postulate-damaged AND counted here	39 (83 %)	sweep damage, not authoring
This issue only	8 (17 %)	genuine authoring defects — the claim holds here
postulate only	3	never reached this census

The evidence, tiered

Textual — 39/39. Declaration-position postulate present on origin/main, absent in the
working tree, for all 39.

Compiled, treatment arm — 6/6. Six of the 39 re-checked in the cured working tree
(idris2 -p contrib --source-dir src --check):

src/Proven/SafeAPIKey/Proofs.idr     | rc=0 | parse_errors=0
src/Proven/SafeArchive/Proofs.idr    | rc=1 | parse_errors=0 | Error: While processing right hand side of maxCompressionRatioAnchor. When unifying:
src/Proven/SafeArgs/Proofs.idr       | rc=0 | parse_errors=0
src/Proven/SafeBase64/Proofs.idr     | rc=0 | parse_errors=0
src/Proven/SafeBloom/Proofs.idr      | rc=0 | parse_errors=0
src/Proven/SafeCalculator/Proofs.idr | rc=0 | parse_errors=0

SafeArchive still exits 1 — on a unification error, not a parse error. The parse class is
cured; other classes remain. That is the expected signature, not a counter-example.

Compiled, control arm — 8/8. The 8 files this issue counts that are not postulate-damaged
still fail to parse in the same cured tree:

src/Proven/FFI/Buffer.idr          | rc=1 | parse_errors=1 | Error: Couldn't parse declaration.
src/Proven/FFI/Echidna.idr         | rc=1 | parse_errors=1 | Error: Couldn't parse any alternatives:
src/Proven/FFI/SafeLRU.idr         | rc=1 | parse_errors=1 | Error: Couldn't parse declaration.
src/Proven/FFI/SafeMonotonic.idr   | rc=1 | parse_errors=1 | Error: Couldn't parse declaration.
src/Proven/FFI/SafeResource.idr    | rc=1 | parse_errors=1 | Error: Couldn't parse any alternatives:
src/Proven/FFI/SafeString.idr      | rc=1 | parse_errors=1 | Error: Couldn't parse declaration.
src/Proven/FFI/SafeTransaction.idr | rc=1 | parse_errors=1 | Error: Couldn't parse declaration.
src/Proven/SafeProbability.idr     | rc=1 | parse_errors=1 | Error: Couldn't parse declaration.

The control arm matters: without it, "these files parse now" would be consistent with the census
being wrong about everything. It was not — it measured something real and misattributed most of it.

Why the sample misled

Seven of the 8 genuine authoring defects are in src/Proven/FFI/. This issue sampled
FFI/Buffer.idr — inside the single subtree where its claim is true. The defect population is
spatially clustered, which makes any one sample maximally unrepresentative: the sample inherits
the cluster's character rather than the population's. Standing error class #1, with a mechanism.

Timing corroborates

• proven-idr-file-census-2026-08-27.txt — mtime 08:31:05
• postulate removal — 10:08:42

The census predates the cure by ~1.5 h, so it measured a tree that still contained the damage. This
is circumstantial; the compiler runs above are the actual warrant.

Second defect in this issue — the evidence path does not resolve

The issue cites .claude/forensics/proven-idr-file-census-2026-08-27.txt, which reads as
repo-relative. The files are not in this repo. They are at the developer root:

/home/hyperpolymath/developer/.claude/forensics/proven-idr-file-census-2026-08-27.txt
/home/hyperpolymath/developer/.claude/forensics/proven-idr-defect-attribution-2026-08-27.txt

Anyone attempting to verify this issue from a checkout finds nothing and cannot tell whether the
data is missing or the claim is fabricated.

Corrected statement of this issue

Of the 47 own-defect parse failures, 8 are authoring defects (7 of them in src/Proven/FFI/,
data used as an identifier) and 39 were sweep damage from the postulate injection in
6c80e0b5, cured in the working tree and carried by PR #206's sibling work. Remediation is
ordinary source fixing for the 8; for the 39 it was a revert-equivalent, already done.

⚠ Operational consequence — do not clean the working tree

The cure for all 42 declaration-position files exists only in the uncommitted working tree of
the local checkout. git checkout -- ., git stash or git clean would re-break every one of
them. Full detail, including the controlled pair and the reproduction commands, is in
docs/IDRIS2-BUILD-WORK-PACKAGE.adoc
on PR #206.

Measured on Idris2 0.7.0 (source/CI target 0.8.0). Every figure names the tree it was taken on.