Repository navigation
feat(abi): model RSR capability-profile resolution in Idris2 - #1033
Conversation
Add src/Hypatia/ABI/RsrProfile.idr, an engineering model of how lib/rules/rsr_conformance.ex resolves a repository's RSR capability profile (declared_capabilities/1, deed_profile_capabilities/1, clause_capabilities/1, a2ml_capabilities/1) and how criterion 3.2.2 (profile_present/0) and the scorecard's profile_present read it. Theorems about the model: deed precedence, fail-closed duplicate and list-less clauses, a2ml fallback, and agreement of 3.2.2 with profile_present whenever the deed decides (the bffd76a fix). The model also shows they still disagree in exactly one case: no deed clause and an rsr-profile.a2ml that exists but yields no capabilities list (3.2.2 checks presence only). That case is recorded OPEN. The Elixir is not extracted from the model; correspondence is by review and ExUnit cases (ASSUMED). Wired into scripts/check-verdicts.sh with one positive control and four expected rejections; the ABI package and PROOF-STATUS list the module. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E294yTkKk127qgKEXFFDBE
|
Caution Review failedThe pull request is closed.
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. |
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01E294yTkKk127qgKEXFFDBE
Codex Review Summary: ❌ FailedThis comment shows the latest Codex review activity on this pull request.
ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
Codex reacts with 👀 while any review is running, comments if it has suggestions, and reacts with 👍 once all reviews finish with no findings. |
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
Signed-off-by: Jonathan D.A. Jewell <6759885+hyperpolymath@users.noreply.github.com>
|
This security review couldn’t start because the paying account has exhausted its Codex allowance and has insufficient available credits. The payer can check their balance and add credits in the Codex usage dashboard, then try again. If you do not manage the paying account, contact this repository's admins. |
|
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 8e1022b522
ℹ️ 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".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| `+scorecardProfilePresent+` whenever the deed decides | ||
| (`+deedDecidedAgrees+`, the bffd76a fix) or the a2ml is not present-but- | ||
| declaring-nothing (`+a2mlDecidedAgrees+`); they disagree in exactly that | ||
| case (`+disagreementIsExactly+`) |PROVEN — Verify Proofs run 42634000625, idris2 --check job 129217248108, at commit 34c7bc7cff0cf54b1b5707a497d9f8abf826e844 (Idris2 v0.7.0, ABI package build) |
There was a problem hiding this comment.
These new proof and fixture statuses are recorded only in this hand-written table: verification/proof-ledger.jsonl contains no RsrProfile obligation, even though the generated ledger immediately above declares that JSONL file canonical. Consequently its published census remains 22/42 and omits the newly claimed proven/tested work, while the schema and currency checks cannot validate these claims. Add the corresponding engineering rows to the JSONL ledger and regenerate the status table.
Useful? React with 👍 / 👎.
| |API type safety |`+Types.idr+`, `+GraphQL.idr+`, `+REST.idr+`, | ||
| `+GRPC.idr+`, `+FFI.idr+` |Full |
There was a problem hiding this comment.
The Coverage section starts emitting table cells without a table attribute or opening |===; the only delimiter is the one at line 559, so AsciiDoc interprets the coverage rows as ordinary text and may treat that final delimiter as the start of an unterminated table containing the following sections. Restore an opening delimiter and header before the first row, or retain the prose-only Coverage section from the parent.
Useful? React with 👍 / 👎.
| |RSR capability-profile resolution |`+RsrProfile.idr+` |Model only; | ||
| correspondence to the Elixir ASSUMED | ||
|
|
||
| |VCL parser totality |`+ParserTotality.lean+` |Full (FROM-clause subset) |
There was a problem hiding this comment.
This entry names ParserTotality.lean, but that artifact was removed before this commit and the current proof is verification/proofs/idris2/ParserTotality.idr; a repository-wide search finds only historical references to the Lean filename. The PageRank and ESN entries immediately below have the same stale .lean references, so this restored coverage map directs readers to nonexistent proof artifacts and should use the Idris2 paths.
Useful? React with 👍 / 👎.
| disagreementIsExactly : (src : ProfileSource) | ||
| -> Not (passes (criterion322 src) = scorecardProfilePresent (declaredCapabilities src)) | ||
| -> (resolve (deed src) = Absent, a2ml src = A2mlDeclaresNothing) |
There was a problem hiding this comment.
disagreementIsExactly proves only the necessary direction: given a disagreement, it derives resolve (deed src) = Absent and a2ml src = A2mlDeclaresNothing. residualDivergence then demonstrates only one concrete source, rather than proving that every source satisfying those two conditions disagrees. Thus consumers cannot obtain the advertised exact characterization from these theorems; add the general converse (or an equivalence theorem) before claiming that this is exactly the disagreement case.
Useful? React with 👍 / 👎.
Owner decision 2026-11-09: write the RSR capability-profile resolution rule as an Idris2 engineering property (estate PROOF-POLICY §1). It is not graded on the PWG ladder (§8.1), so statuses use the §5 tokens only.
What this adds
src/Hypatia/ABI/RsrProfile.idr(added tohypatia-abi.ipkg). It modelsdeclared_capabilities/1,deed_profile_capabilities/1,clause_capabilities/1,a2ml_capabilities/1,profile_present/0(criterion 3.2.2) and the scorecard'sprofile_present(caps != :none) fromlib/rules/rsr_conformance.ex. The module uses%default totaland has no escape hatches.deedPrecedence,a2mlIgnoredUnlessAbsent.duplicateDeclaresNothing,listlessDeclaresNothing,duplicateFailsCriterion,listlessFailsCriterion.fallbackNoDeed,fallbackNoClause,fallbackCriterionNoClause.deedDecidedAgrees(the bffd76a fix),a2mlDecidedAgrees,disagreementIsExactly,residualDivergence.tests/accept/RsrProfileResolution.idrrestates the profile-reader ExUnit cases against the model.tests/reject/:DuplicatedClauseIsAProfile,DuplicatedClausePassesProfileCriterion,ListlessClauseFallsBack,A2mlOverridesDeed.scripts/check-verdicts.shnow also checks the new module for escape-hatch markers. Its accept/reject loops already pick up the new fixtures.verification/PROOF-STATUS.adoc,.claude/CLAUDE.mdandsrc/abi/README.adoc.Finding: 3.2.2 and
profile_presentcan still disagreeThe model shows that the two readers do not always agree. When the deed has no top-level
(rsr-profile …)clause:present_mr("rsr-profile.a2ml"), which only checks that the file exists.profile_presentneedsa2ml_capabilities/1to return a list.So an
rsr-profile.a2mlthat does not parse, or has nocapabilitieslist, passes 3.2.2 whileprofile_presentis false.disagreementIsExactlyproves this is the only case where they disagree.residualDivergenceshows that it happens. This PR does not change the Elixir. The row is recorded as OPEN.What is not claimed
The Elixir is not extracted from this model. The correspondence comes from review plus ExUnit, so it is recorded as ASSUMED. The theorems are properties of the model, not verified code. No local Idris2 toolchain was available, so these rows only become PROVEN/TESTED once the Verify Proofs
idris2 --checkjob passes.Generated by Claude Code