Estate sweep: Fork A 'postulate' damage confined to proven — but the Idris2/Agda keyword misconception is hand-authored and predates it by 4 months

[hyperpolymath]

Answer: the Fork A sweep did not reach any other repo — but the misconception it mechanised is older than the sweep and hand-authored

Follow-up to the postulate sweep (6c80e0b5 "[P1] Explicit postulate sweep (Fork A) (#189)") that rendered 42 .idr files unparseable in hyperpolymath/proven. This issue reports the estate-wide check for the same defect, and one finding that is more consequential than the sweep itself.

Method

Every hyper-repos/ directory containing .idr files (122 repos) was scanned with a declaration-position detector — one that skips whole-line -- and ||| comments, strips trailing -- comments, and strips double-quoted string literals — then every hit was confirmed against Idris2 0.7.0, not merely grepped.

Result

Repo	.idr files	files with decl-position postulate	sites
civic-connect	4	1	4
ideas-to-alphas	13	1	7
bulk_update_oikos/cerro-torre	—	3	0 (false positives — see below)
all other 119 repos	—	0	0

The named high-risk candidates are all clean: proven-servers 755 files / 0 sites, proven-tests-and-benches 58 / 0, echidna 43 / 0, affinescript 9 / 0. stapeln has no .idr files at all.

So the sweep was confined to proven. That question is closed.

The finding that matters: this predates the sweep by four months, and it is hand-written

Both genuine sites were authored by hand, in April 2026, and git log -L names the intent:

File	Sites	Commit	Date	Subject
civic-connect/src/Abi/Layout.idr	4	0b07a57	2026-04-12	refactor(abi): eliminate believe_me in Layout.idr
ideas-to-alphas/research/tropical/TropicalKleene.idr	7	93d2e72	2026-04-11	feat(tropical): close blockers 2+3+4, fix type errors, reduce postulate count

Both are trusted-base reduction attempts that made the file worse. Replacing believe_me with postulate is correct in Agda, where postulate is an axiom keyword. In Idris2 it is not a keyword at all, so in declaration position it makes the entire file unparseable.

The August sweep therefore did not invent this error — it mechanised a cross-language keyword assumption that was already present in hand-written code. That is the root worth fixing, and a lint rule catches both.

Compiler evidence (Idris2 0.7.0)

$ cd civic-connect/src && idris2 -p contrib --check Abi/Layout.idr
1/2: Building Abi.Types (Abi/Types.idr)
2/2: Building Abi.Layout (Abi/Layout.idr)
Error: Keyword 'export' is not a valid start to a declaration.
Abi.Layout:45:1--45:7
 45 | export
      ^^^^^^
rc=1

$ idris2 -p contrib --check ideas-to-alphas/research/tropical/TropicalKleene.idr
Error: Expected a type declaration.
rc=1

Both files are of the form:

export
postulate alignUpDivides : (size : Nat) -> (align : Nat) -> ...

⚠ Three detector defects found while doing this — quote the corrected figures only

I am reporting my own instrument errors because each one would have produced a wrong number, and two of them were caught only by asking the compiler:

1. Comment blindness. A raw grep for postulate matched -- and ||| comment lines. On proven's origin/main this over-counted 46 files / 369 occurrences where the true declaration-position figure is 42 / 360.
2. String-literal blindness. The three cerro-torre files are false positives: the token appears inside idris_crash "tamperEvidence: cryptographic postulate — type-level use only". Valid code. All three parse.
3. Single-wording error matching. A success criterion of grep -ci "couldn't parse" scored TropicalKleene.idr as parse_errors=0 when it had genuinely failed to parse. Idris2 emits at least three distinct messages for this one defect — Couldn't parse declaration, Expected a type declaration., and Keyword 'export' is not a valid start to a declaration. Any detector keyed to one wording under-reports.

A fourth trap, which is why this survived since April: Idris2 reports the error at the line before the offender — at the export visibility modifier, or (in proven) at the docstring that precedes the declaration. Anyone who greps the reported line finds a perfectly good export or well-formed prose and concludes the report is spurious.

Blast radius: real but latent

Neither civic-connect nor ideas-to-alphas contains any .ipkg file, so neither unparseable file is in any package build. Nothing is red because of this. That is precisely why it has stood for four months.

Proposed remediation

1. Cure the 11 sites in the two files — same cure as proven: delete the postulate token and give the declaration a body, or mark the obligation with the estate's own trusted-base vocabulary. proven's own register already states "Do NOT use the postulate keyword."
2. Add a lint rule (hypatia is the natural home) for postulate in Idris2 declaration position — comment-aware and string-literal-aware, because a naive rule reproduces defects 1 and 2 above.
3. Note bulk_update_oikos vendors copies. bulk_update_oikos/civic-connect/src/Abi/Layout.idr is the same file again, so a fix must reach both or the vendored copy silently un-fixes it.