[hyperpolymath]

Why

#163 auto-merged before the fixes for CodeRabbit's two review findings were pushed. Both findings were correct:

1. Major: PROOF-NEEDS.adoc and docs/proof-debt.adoc said check-abi.sh fails CI on postulate and on holes. Its keyword scan covered only believe_me, assert_total, assert_smaller, idris_crash and unsafePerformIO.
2. Minor: the proof-debt (d) section called every entry an unsafe block. Four of them, in coprocessor/mod.rs, are unsafe extern "C" fn type declarations.

What changes

• panel-clades/scripts/check-abi.sh: postulate joins the escape-hatch scan. No .idr file uses it, so the gate still passes.
• Both ledgers: they now say exactly what CI enforces (the six keywords) and that holes are not scanned. "No holes" stays as a measurement dated 2026-10-26.
• proof-debt (d): the wording now covers both blocks and declarations.

Verification

• The scan, run locally with the new pattern over panel-clades/src/abi/PanelClades/**/*.idr, finds no hits (exit 1, the passing case).
• bash -n on the script is clean.
• standards' check-trusted-base.sh still passes.

Note: Governance, Hypatia, Secret Scanner and Rust CI will fail at startup here, as they do on main. hyperpolymath/standards was transferred to metadatastician/standards, so the pins no longer resolve; see the #163 comment. This PR doesn't cause or fix that.

---

Generated by Claude Code

[coderabbitai]

Warning

Review limit reached

You've used all free OSS reviews for now. Wait for the free limit to reset to keep reviewing this public repository.

Next included review available in 32 minutes.

Check out review usage here.

View limit details

Limit details: You’ve used the included review currently available.

Learn how review limits work.

Review configuration:

Run configuration

• Source mode: Auto
• Repository: Unavailable
• Branch: Unavailable
• File: No configuration file from this repository applied
• Commit: Unavailable
• Layers: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: 2b7c29f1-bfb1-4b83-9ffd-d75e7c87f554

Commits

Reviewing files that changed from the base of the PR and between 1b6e767 and cb3211c.

Files selected for processing: 3

• PROOF-NEEDS.adoc
• docs/proof-debt.adoc
• panel-clades/scripts/check-abi.sh

• 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

_{Comment @coderabbitai help to get the list of available commands.}

[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

[chatgpt-codex-connector]

Codex Review Summary

This comment shows the latest Codex review activity on this pull request.

Review	Status	Commit	Review trigger
📝 Code Review	✅ Completed 2026-10-26T22:39:57.580070Z	cb3211c	Draft marked ready

ℹ️ About Codex in GitHub

Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you

• Open a pull request for review
• Mark a draft as ready
• Comment "@codex review" or "@codex security review".

Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings.