[hyperpolymath]

Problem

PROOF-NEEDS.adoc marks panic-attack's Idris2 ABI proofs ✅, but no CI job ever type-checked src/abi/. With Idris2 0.7.0, none of the five modules checked as committed:

Module	On main
all five	module name PanicAttack.ABI.* does not match the flat path src/abi/*.idr
Types.idr	parse error at line 46; Ord Severity without Eq Severity
Stripping.idr	stray ||| block at line 222; stripLineCommentsIdempotent does not type-check (unsolved constraint in the // case; decEq not imported)
PatternCompleteness, ClassificationSoundness, AttestationUnforgeability	check once staged at the right module path

Change

• scripts/ci/check-idris-abi.sh:

  • stages a module-path view of the unchanged files as symlinks, so the bytes checked are the committed bytes;
  • runs idris2 --check on each module;
  • fails on any type error, a missing %default total, or believe_me, assert_total, assert_smaller, postulate or idris_crash in code.

• proven-tests.yml, new idris-abi job (blocking, every PR):

  • builds Idris2 from the v0.7.0 tag, checking commit 27780073…;
  • caches the build and runs the script;
  • records a PROOF-POLICY §6 deviation, because the Guix manifest and container lack Idris2.

  The workflow header explains why this departs from its "no Idris2 bootstrap on PRs" rule: a claim needs a receipt on every change, and the cache keeps it fast.

• Stripping.idr, re-proved:

  • stripIsIdOnClean: stripping is the identity on text with no //.
  • stripIsClean / bodyIsClean: the strippers' output has no //, by mutual induction.
  • stripLineCommentsIdempotent and bodyIsFixedPoint follow.
  • The strippers are restated with explicit Bool steps, which can be reasoned about.

• Types.idr: adds the missing Eq Severity and fixes the LangId declaration syntax.

• PROOF-NEEDS.adoc, EXPLAINME.adoc, CHANGELOG.adoc: state that the earlier ✅ claims had no receipt, and name the new one.

Validation (Idris2 0.7.0, built here from the same tag)

• scripts/ci/check-idris-abi.sh passes all 5 modules.
• The gate fails both ways:
  • on main's files: Stripping and Types FAIL;
  • on a planted believe_me: FAIL.
• Stripping mutant (blank with / instead of a space): rejected at bodyStepIsClean and the sanity tests.
• Differential run of the restated strippers against the original definitions: every string of length ≤ 9 over {/, x, \n} (29,524 inputs), 0 mismatches and 0 non-idempotent outputs.
• Nine closed sanity theorems check by evaluation.
• actionlint 1.7.7 is clean, and asciidoctor --failure-level=WARN is clean on the edited .adoc files.

Departure from the agreed plan

The agreed option was "CI job + ipkg". I did not add an .ipkg, because one needs the files moved to src/abi/PanicAttack/ABI/. Their paths are cited in about 13 places, including legacy A2ML metadata that agents may not edit. The staging script gives the same check with no moves. Moving the files plus an .ipkg is the cleaner long-term layout and is a natural follow-up.

---

Generated by Claude Code

[coderabbitai]

Caution

Review failed

The pull request is closed.

• Autofix · Keep fixing CodeRabbit findings and required CI, and resolving merge conflicts

Thanks for using CodeRabbit! It's free for OSS, and your support helps us grow. If you like it, consider giving us a shout-out.

Share

• X
• Mastodon
• Reddit
• LinkedIn

[sonarqubecloud]

Quality Gate passed

Issues
0 New issues
0 Accepted issues

Measures
0 Security Hotspots
0.0% Coverage on New Code
0.0% Duplication on New Code

See analysis details on SonarQube Cloud