feat(arbitration): ECH-05 fidelity evidence and belief/epi/sound verdict levels

[hyperpolymath]

Summary

Implements ECH-05 (drafted in issues/echidna-05-fidelity-evidence.md; not yet filed). When backends agree, that doesn't show they proved the same statement. So the arbiter now takes per-attempt fidelity evidence and gives each fused verdict a level: belief < epi < sound. A synonym collision (statements aligned only by name) can no longer reach sound, however many backends agree. The numeric fusion is unchanged; a regression fixture taken before the change shows this.

The ECH-05 plan asks for three stacked PRs. This session can push to one branch only, so the three parts are three separate commits here, and each can be reviewed on its own:

Commit	Part
6b6f54a	A: FidelityEvidence on ProverAttempt; level / retracted / warranted_term on ArbitratedVerdict; the policy; regression fixture
48e8034	B: src/abi/EchidnaABI/Arbitration.idr, plus an accept/reject fixture falsifier wired into idris2-abi-ci.yml
33a3dc7	C: tests/arbitration_fidelity_test.rs, ROADMAP stage 6 acceptance, backend-pair table, issues/README.md row and issue draft

Changes

A: input and output types (src/rust/verification/result_arbiter.rs, src/rust/exchange/mod.rs)

• FidelityEvidence = KernelTranslation { format, checked_by, term_hash } | DeclaredCorrespondence { consequence_tests, failures } | None. The default is None, and ProverAttempt::new keeps its signature.
• EpistemicLevel { Belief, Epi, Sound } (ordered); fidelity_level() is the policy:
  • belief if the verdict needs review, rests on a retracted backend, fused nothing, or any attempt has None evidence.
  • sound only if every fused attempt is a KernelTranslation to the same non-empty term_hash.
  • epi if every fused attempt is a kernel translation or a correspondence with ≥ 1 consequence test and 0 failures, and the kernel hashes agree.
  • belief otherwise, e.g. two kernel translations to different terms.
• ResultArbiter::retract(prover) marks a backend unsound. Any verdict that fuses one of its attempts drops to belief, and retracted lists the backend.
• exchange::ExchangeFormat (one variant per bridge) and exchange::term_hash: a BLAKE3 hash of the rendered term, separated by format, with no canonicalisation. The failure mode is a missed sound, never a false one.
• tests/fixtures/arbitration_regression.json was generated at 29b18ea before the change (16 scenarios × 4 policies). tests/arbitration_regression_test.rs replays it field by field (floats to 1e-12) and checks every verdict is at belief.

B: Idris2 ABI (EchidnaABI.Arbitration)

• Level fused is a closed sum indexed by the fused evidence. Sound h requires an All (KernelAt h) fused proof, and each KernelAt holds the hash-equality proof. So a collision, a correspondence or missing evidence in fused cannot be typed Sound, whatever produced the value (collisionNotSound, correspondenceNotSound, noEvidenceNotSound).
• The classifier level comes with blockedIsBelief, noEvidenceIsBelief, failedCorrespondenceIsBelief, untestedCorrespondenceIsBelief, emptyFusedIsBelief, blockingNeverRaises, and evaluation controls (alignedPairIsSound, collisionPairIsBelief, mixedPairIsEpi). It is total and needs only DecEq on the hash type.
• epistemic-types 6a68de3 and residual-evidence-types 97244f5 are cited by pin in the module header, not imported. The cited lemma names were checked at those commits.
• Falsifier: tests/abi/accept/ArbitrationAligned.idr must type-check, and tests/abi/reject/ArbitrationCollision.idr (identical apart from one hash) must fail with Mismatch between.
  • scripts/abi-fixtures.sh judges by output, because idris2 --check exits 0 on a missing import.
  • It checks each fixture in a fresh temp directory, because a stale build/ cache can silently skip the check (this bit me locally).
  • It runs in idris2-abi-ci.yml, whose path filter now includes tests/abi/ and the script, and as just abi-fixtures.

C: acceptance tests and docs

• Synonym collision (Lean ℕ vs set.mm NN), under the portfolio, Bayesian and Dempster–Shafer policies. Four cases all stay at belief while verified = true / CrossChecked: lexical only; kernel translations to different terms; a correspondence with a failed consequence test; an untested correspondence.
• MiniF2F mathd_numbertheory_3 positive control: the Lean and Isabelle statements were checked against openai/miniF2F@4e433ff and translate to one term, which reaches sound. Negative control: the same pair with an off-by-one translation does not.
• Retraction: retracting Lean lowers the two verdicts that rested on it. The Isabelle + HOL Light verdict stays sound, and the numbers don't change.
• The exchange-layer terms are hand-written translation targets. These tests check the arbiter given certificates, not that certificates can be produced (that is stage 6).
• Docs:
  • ROADMAP stage 6 acceptance (§2) and a "Cross-prover semantics" row (§3).
  • Gap-analysis table "Backend pairs that can share a term": every row is DESIGNED in ECHIDNA, and external routes are named but not run.
  • Short notes in the comparison doc and Guides.
  • issues/README.md gains the ECH-05 row and lists its four labels missing on this repo.
  • CHANGELOG [Unreleased] entry.

RSR Quality Checklist

Required

• Tests pass: cargo test --lib (1208 passed, 3 ignored) plus both new integration tests; full --workspace run is left to CI (see Testing)
• Code is formatted (cargo fmt --all -- --check)
• Linter is clean (cargo clippy --locked --workspace --exclude echidna-rest --all-targets -- -D warnings; see Testing for the exclusion)
• No banned language patterns (Rust, Idris2, Bash only)
• No unsafe blocks
• No banned functions (the ABI dangerous-pattern grep over src/abi and tests/abi is empty)
• SPDX license headers present on all new/modified source files
• No secrets, credentials, or .env files included

As Applicable

• Repo deed (status) / (maturity) updated: not touched; nothing ships to dispatch yet (every dispatched verdict is belief)
• Repo deed (ecosystem) updated: n/a
• Repo deed (meta) and/or docs/decisions/ updated: policy decisions are listed below for the owner
• docs/ROADMAP.adoc updated (stage 6 acceptance + §3 row)
• Documentation updated for user-facing changes (Guides, gap analysis, comparison doc)
• TOPOLOGY.md updated: n/a
• CHANGELOG updated
• New dependencies reviewed: none added (blake3 already a dependency)
• ABI changes validated: new module has no foreign declarations; ffi/zig untouched

Testing

$ cargo test --lib -- result_arbiter term_hash          → 23 passed
$ cargo test --test arbitration_regression_test        → 1 passed, 1 ignored (the generator)
$ cargo test --test arbitration_fidelity_test          → 4 passed
$ cargo test --lib                                     → 1208 passed; 0 failed; 3 ignored
$ cd src/abi && idris2 --build echidnaabi.ipkg         → 20/20 modules, exit 0 (Idris2 0.8.0)
$ bash scripts/abi-fixtures.sh
ok   accept: tests/abi/accept/ArbitrationAligned.idr
ok   reject: tests/abi/reject/ArbitrationCollision.idr
    Mismatch between: True and False.

Negative controls (applied, observed, then reverted):

• A 1e-6 relative perturbation of the Bayesian conflict metric fails the regression test at unanimous_proven_three / bayesian(0.5): verdict.conflict.
• Removing the term-hash equality check in fidelity_level fails synonym_collision_cannot_reach_sound and minif2f_mistranslated_pair_does_not_reach_sound.
• Making the reject fixture aligned makes the falsifier fail ("type-checked"); breaking its import makes it fail ("non-type reason").

Not run locally:

• echidna-rest builds utoipa-swagger-ui, whose build script downloads Swagger UI from GitHub, and the sandbox proxy blocks that. It is the only crate excluded from local clippy; CI builds the full workspace.
• The full cargo test --workspace --all-targets was not run here; that is left to CI.

Decisions for the owner

1. Stacked PRs: one branch with three commits, because of this session's single-branch constraint. Happy to split into A → B → C stacked PRs.
2. Policy choices beyond the spec's text:
   • A correspondence needs ≥ 1 consequence test (otherwise zero failures is vacuous).
   • Mismatched kernel hashes among fused attempts give belief, not epi.
   • A verdict with needs_review (which covers inconsistent premises) is belief.
   • An empty term_hash is not a certificate.
3. Stage 6 "pair X": proposed HOL4 ↔ HOL Light via OpenTheory first, then Lean 4 ↔ Rocq via Dedukti.
4. Labels area:arbitration, area:exchange, epistemic-types, residual-evidence-types don't exist on this repo yet. They need creating before ECH-05 is filed.
5. Open questions from the issue are unchanged: whether Dempster–Shafer stays limited to same-encoding provers, and who runs consequence testing.

🤖 Generated with Claude Code

https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3

---

Generated by Claude Code

[coderabbitai]

Note

Currently processing new changes in this PR. This may take a few minutes, please wait...

⚙️ Run configuration

• Configuration used: Organization UI
• Review profile: ASSERTIVE
• Plan: Advanced
• Run ID: 776e4918-aa98-4fb3-870e-5eee34949f97

📥 Commits

Reviewing files that changed from the base of the PR and between 29b18ea and 33a3dc7.

📒 Files selected for processing: 20

• .github/workflows/idris2-abi-ci.yml
• CHANGELOG.adoc
• Justfile
• docs/ROADMAP.adoc
• docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc
• docs/design/TYPING_CAPABILITIES_COMPARISON.adoc
• docs/wikis/Guides.md
• issues/README.md
• issues/echidna-05-fidelity-evidence.md
• scripts/abi-fixtures.sh
• src/abi/EchidnaABI/Arbitration.idr
• src/abi/echidnaabi.ipkg
• src/rust/exchange/mod.rs
• src/rust/verification/mod.rs
• src/rust/verification/result_arbiter.rs
• tests/abi/accept/ArbitrationAligned.idr
• tests/abi/reject/ArbitrationCollision.idr
• tests/arbitration_fidelity_test.rs
• tests/arbitration_regression_test.rs
• tests/fixtures/arbitration_regression.json

 ________________________________________
< Ship it? Sure-after we unship the bug. >
 ----------------------------------------
  \
   \   (\__/)
       (•ㅅ•)
       / 　 づ

✨ Finishing Touches

📝 Generate docstrings

• Commit to this branch
• Create a new PR

• 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.}

[hyperpolymath]

CI: Cargo Audit / Dependency audit is red, and the cause is not in this PR.

• What fails: cargo audit reports five advisories against quinn-proto 0.11.15: RUSTSEC-2026-0338, -0339, -0340, -0341 and -0342 (two rated 7.5 high). It is pulled in only through reqwest → quinn 0.11.9, an optional HTTP/3 path. cargo audit scans the whole lockfile, so it is flagged anyway.
• Why it isn't this PR's: this PR doesn't touch Cargo.toml or Cargo.lock, and the PR's lockfile is byte-identical to main's at 29b18ea. Cargo Audit last passed on main in its scheduled run on 2026-10-12, so the advisories reached the RustSec database after that. Running cargo audit -f on main's lockfile locally reproduces the same five IDs. I didn't re-run the job: it is deterministic, and the local reproduction is the stronger check.
• Fix: no open PR addresses it. The proposed patch is lockfile-only and semver-compatible (quinn 0.11.9 requires quinn-proto ^0.11.12):

  cargo update -p quinn-proto   # 0.11.15 -> 0.11.19 (pulls rand 0.10 / getrandom 0.4 / rand_pcg into quinn-proto's subtree)

  cargo audit on the bumped lockfile reports no vulnerabilities. I've left it out of this PR to keep ECH-05's scope; it can land on its own, or ride here if the owner prefers.

---

Generated by Claude Code

[hyperpolymath]

CI: governance / Validate Hypatia Baseline is red, and it is already red on main.

• What fails: Gate failed: 6 unfiltered finding(s) at or above 'info'. Five are SD022 "doc references src/…/ but no such directory exists", in issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md (×3: src/api/, src/scheduler/, src/modes/), .github/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md (src/api/) and docs/handover/PARADISEO-ROADMAP-PROMPT.adoc (src/dispatcher/). The sixth is download_then_run_shell at echidna-playground/ci-templates/mirror.yml:131 (curl -sSf https://radicle.xyz/install | sh).

• Why it isn't this PR's: none of these files is in this PR's diff. main's Governance run at 29b18ea (run 38003834638) fails with the same six findings. They arrived with Merge arena/16d27c7e-echidna: ParadisEO roadmap and issue specs #426 and Arena/9aef7602 echidna #427.

• Fix: no open PR addresses it. Proposed patch:

  1. The five SD022 hits: the paths name echidnabot's tree, not echidna's (the drafts and the handover describe the other repository), so they are false positives. Add baseline entries in the existing .hypatia-baseline.json form, one per (file, type) pair:

     { "severity": "medium", "rule_module": "structural_drift", "type": "SD022",
       "file": "issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md",
       "note": "cross-repo draft: src/ paths are hyperpolymath/echidnabot's tree",
       "tracking_issue": "hyperpolymath/echidna#314" }

     plus the same for .github/issues/echidnabot-01-adaptive-ci-portfolio-scheduler.md and docs/handover/PARADISEO-ROADMAP-PROMPT.adoc.
  2. mirror.yml:131: this is a real pipe-to-shell, so it wants a real fix: pin the Radicle installer version and verify a checksum before running it. A baseline acknowledgement is the alternative, and that one is the owner's call.

  I've left both out of this PR to keep ECH-05's scope.

---

Generated by Claude Code