feat(abi): model RSR capability-profile resolution in Idris2

.claude/CLAUDE.md

@@ -177,6 +177,7 @@ Training pipeline reads outcomes/*.jsonl for ESN (confidence time series) and pa
 | `RuleEngine.idr` | Rule-evaluation types |
 | `Verdict.idr` | Verdict records (HYP-01): support = Pattern / Observed n / Mechanical re-check; `Sound` only from a confirming re-check. Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) |
 | `Retraction.idr` | Quarantine as retraction (HYP-01): a token survives iff its support thins into what remains; a finding survives through one of its tokens. Transcribed from residual-evidence-types `Revision.agda` @ 97244f5 |
+| `RsrProfile.idr` | RSR capability-profile resolution (engineering model of `lib/rules/rsr_conformance.ex`): deed precedence, fail-closed duplicate/list-less clauses, a2ml fallback, and when criterion 3.2.2 agrees with the scorecard's `profile_present` (and the one case it does not). Gate: `scripts/check-verdicts.sh` (+ `tests/reject/`, `tests/accept/`) |
 
 **Build system:** `src/abi/hypatia-abi.ipkg` (compile), `verify/hypatia-verify.ipkg` (proofs), `pack.toml` (Pack package manager).
 The ipkg sets `sourcedir = ".."`, so **`src/Hypatia/ABI/` is what compiles** — that is the

.github/workflows/verify-proofs.yml

@@ -213,7 +213,9 @@ jobs:
       # from a confirming prover re-check. The typechecker is the falsifier:
       # tests/accept/ must be accepted, and every tests/reject/ module must be
       # refused at `invalid` with the diagnostic its `-- EXPECT:` line names.
-      - name: Verdict accept/reject fixtures (HYP-01)
+      # The same fixtures gate RsrProfile.idr, the model of the RSR
+      # capability-profile resolution (lib/rules/rsr_conformance.ex).
+      - name: Verdict + RSR-profile accept/reject fixtures (HYP-01)
         run: bash scripts/check-verdicts.sh
 
       - name: Summary

scripts/check-verdicts.sh

@@ -10,14 +10,20 @@
 #
 #   1. the ABI package builds (the positive set, first: a broken toolchain or
 #      a missing import must never turn into a "successful" rejection);
-#   2. Verdict.idr and Retraction.idr contain no escape-hatch marker at all;
+#   2. Verdict.idr, Retraction.idr and RsrProfile.idr contain no
+#      escape-hatch marker at all;
 #   3. every module under tests/accept/ is ACCEPTED (positive controls);
 #   4. every module under tests/reject/ is REFUSED, and refused only at its
 #      declaration `invalid`, with the diagnostic its `-- EXPECT:` line
 #      names — an error anywhere else, a different diagnostic (an arity
 #      slip is also "refused at invalid"), or a refusal for a missing name,
 #      import or parse, is a broken fixture, not a pass.
 #
+# The same accept/reject discipline gates src/Hypatia/ABI/RsrProfile.idr, the
+# model of the RSR capability-profile resolution in
+# lib/rules/rsr_conformance.ex (tests/accept/RsrProfileResolution.idr and the
+# RSR-profile modules under tests/reject/).
+#
 # An empty tests/accept/ or tests/reject/ is a broken checkout, not a pass.
 # The Lean half of the positive control (re-running the prover and comparing
 # digests) is scripts/recheck-lean-hole.sh.
@@ -35,12 +41,13 @@ mkdir -p "$logs"
 
 "$idris2" --version
 
-# 1. Positive set: the ABI package, Verdict included.
+# 1. Positive set: the ABI package, Verdict, Retraction and RsrProfile included.
 "$idris2" --build src/abi/hypatia-abi.ipkg
 export IDRIS2_PATH="$PWD/build/abi/ttc${IDRIS2_PATH:+:$IDRIS2_PATH}"
 
 # 2. No escape hatch in the modules the rejections are about.
-for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.idr; do
+for module in src/Hypatia/ABI/Verdict.idr src/Hypatia/ABI/Retraction.idr \
+              src/Hypatia/ABI/RsrProfile.idr; do
   if grep -nE 'believe_me|assert_total|assert_smaller|idris_crash|postulate|sorry|admit|native_decide|Admitted|unsafeCoerce|Obj\.magic' \
        "$module"; then
     echo "ERROR: escape-hatch marker in $module" >&2