diff --git a/.github/workflows/idris2-abi-ci.yml b/.github/workflows/idris2-abi-ci.yml index f9a2068f..8ea18c7b 100644 --- a/.github/workflows/idris2-abi-ci.yml +++ b/.github/workflows/idris2-abi-ci.yml @@ -11,6 +11,8 @@ on: paths: - 'src/abi/**' - 'src/idris/**' + - 'tests/abi/**' + - 'scripts/abi-fixtures.sh' - '.github/workflows/idris2-abi-ci.yml' # No paths-filter on pull_request: this job is a REQUIRED status check, so it # must report on every PR (a path-filtered required check deadlocks PRs that @@ -44,7 +46,7 @@ jobs: GH_TOKEN: ${{ github.token }} run: | set -euo pipefail - PATTERN='^(src/abi/|src/idris/)' + PATTERN='^(src/abi/|src/idris/|tests/abi/|scripts/abi-fixtures\.sh$)' if [ "${{ github.event_name }}" = "pull_request" ]; then FILES=$(gh api "repos/${{ github.repository }}/pulls/${{ github.event.pull_request.number }}/files" \ --paginate --jq '.[].filename') @@ -93,6 +95,13 @@ jobs: idris2 --build echidnaabi.ipkg echo "✓ All ABI modules type-check successfully" + - name: Accept/reject fixtures (mechanical falsifier) + if: steps.detect.outputs.relevant == 'true' + run: | + # tests/abi/accept must type-check; tests/abi/reject must be refused + # with a unification error (each reject mirrors one accept fixture). + bash scripts/abi-fixtures.sh + - name: Type-check Idris2 proof validator (src/idris) if: steps.detect.outputs.relevant == 'true' run: | diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index d17696c2..60d6bef6 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -8,6 +8,24 @@ https://semver.org/spec/v2.0.0.html[Semantic Versioning]. === [Unreleased] +==== Added — arbitration 2026-10-14 (ECH-05) + +* *Fidelity-levelled arbitration*: `+ProverAttempt+` carries +`+FidelityEvidence+` (`+KernelTranslation+` / `+DeclaredCorrespondence+` / +`+None+`) and `+ArbitratedVerdict+` gains `+level+` (`+belief+` / `+epi+` / +`+sound+`), `+retracted+` and `+warranted_term+`. `+sound+` needs every +fused attempt to be a kernel-checked translation to one exchange-layer +term (`+exchange::term_hash+`); a synonym collision stays `+belief+` +however many backends agree. `+ResultArbiter::retract+` marks a backend +unsound and lowers every verdict that rested on it. Numeric fusion is +unchanged: `+tests/arbitration_regression_test.rs+` replays the +pre-change numbers. Dispatch attaches no evidence yet, so dispatched +verdicts are `+belief+`. +* *`+EchidnaABI.Arbitration+`* (Idris2): the three-level verdict as a +closed sum whose `+Sound+` constructor carries the hash-equality proofs, +with the classifier and its properties; `+tests/abi/{accept,reject}+` +fixtures checked by `+scripts/abi-fixtures.sh+` in `+idris2-abi-ci.yml+`. + ==== Added — integrations 2026-10-05 * *`+echidna prove --output json+`*: prints exactly one diff --git a/Justfile b/Justfile index 87629b02..207cfb06 100644 --- a/Justfile +++ b/Justfile @@ -311,6 +311,11 @@ proofs-verif-idris: fi echo "Idris2 verification corpus: all files type-check" +# Accept fixtures must type-check, reject fixtures must be refused (tests/abi). +# Type-check the Idris2 ABI accept/reject fixtures (mechanical falsifier). +abi-fixtures: + bash scripts/abi-fixtures.sh + # Heavy (downloads the ~500MB Isabelle release), so this is gated by the weekly # verification-proofs-cron workflow, not the per-PR `proofs` rollup. Covers the # base-HOL theories; algebra/GroupTheory.thy is excluded (see proofs/isabelle/ROOT). diff --git a/docs/ROADMAP.adoc b/docs/ROADMAP.adoc index 6ff24141..691128d8 100644 --- a/docs/ROADMAP.adoc +++ b/docs/ROADMAP.adoc @@ -108,6 +108,12 @@ Stage 6 Cross‑prover semantics translation actually works 6b Dedukti bridge real λΠ modulo as lingua franca 6c mathematical identity arbitration canonicalise across representations 6d Coursera delivery Zig ABI exposes capability + acceptance (ECH‑05) a KernelTranslation certificate + is producible for a named backend + pair; arbitration already levels + verdicts belief / epi / sound by + that evidence (row "Cross‑prover + semantics" in §3) Stage 7 Sovereign tooling surround the rest of the ecosystem 7a Stapeln container lifecycle @@ -198,6 +204,18 @@ schema; nightly CI ≥ 1 h; zero known panic paths orphans, verified 2026‑04‑27) |*`+ProverKind+` ≥ 65 variants, every one factory‑dispatched*; CLAUDE.md states the canonical count; no orphans — *target met and exceeded* + +|"`Cross‑prover semantics`" |The exchange bridges +(`+src/rust/exchange/+`) parse and emit their formats; none produces a +kernel‑checked translation. `+ResultArbiter+` grades each verdict +`+belief+` / `+epi+` / `+sound+` by per‑attempt `+FidelityEvidence+` +(ECH‑05), so a synonym collision cannot reach `+sound+`; dispatch attaches +no evidence yet, so every dispatched verdict is `+belief+` +|*A `+KernelTranslation+` certificate is producible for a named backend +pair*, and a verdict on that pair reaches `+sound+`. First candidate: +HOL4 ↔ HOL Light through OpenTheory (6a); then Lean 4 ↔ Rocq through +Dedukti (6b). Pair table: `+docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc+` +§ "Backend pairs that can share a term" |=== === 4. Current sprint — "`the smallest set that flips half the table`" diff --git a/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc b/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc index d8b7da5b..3f175714 100644 --- a/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc +++ b/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc @@ -95,6 +95,12 @@ epistemic type detection 3. Implement knowledge/belief type operators 4. Develop common knowledge analysis 5. Add secrecy/privacy type verification +*Meta-level use (ECH-05)*: result arbitration grades each verdict +`belief` / `epi` / `sound`, following epistemic-types' `Warrant` / +`Epi` / `SoundWarrant`; see "Backend pairs that can share a term" below. +That is a level on ECHIDNA's own verdicts, not epistemic typing of user +proofs, so the status above stands. + === 5. Advanced Substructural Types *Status*: ✅ Partial (via Idris2 linear types) @@ -216,6 +222,50 @@ analysis |Type Classes |❌ |✅ Multiple |Low |Low |=== +==== Backend pairs that can share a term + +Cross-prover agreement only warrants the source claim when the backends' +statements are the same term. `ResultArbiter` (ECH-05) grades a verdict +`sound` only if every fused attempt carries a `KernelTranslation` +certificate to one exchange-layer term, and `epi` for declared +correspondences validated by consequence testing; lexical alignment +through `data/synonyms/` alone is `belief`. The table names the backend +pairs whose type theories meet in an exchange format, so that a +kernel-checked shared term is possible in principle. + +The route column names external projects, which were not run for this +table. The last column is ECHIDNA's own state: no bridge in +`src/rust/exchange/` produces a kernel-checked translation yet, so every +row is DESIGNED and no pair reaches `sound` today. Producing one +certificate for one pair is the ROADMAP stage 6 acceptance. + +[cols="2,2,3,2",options="header"] +|=== +|Backend pair |`ExchangeFormat` |External route |In ECHIDNA +|HOL4 ↔ HOL Light |`open_theory` |OpenTheory articles, both directions; +checked by the OpenTheory article reader |DESIGNED (`opentheory.rs` +exports and imports proof states, not checked articles); first candidate +|Lean 4 ↔ Rocq |`dedukti` / `lambdapi` |Lean and Coq encodings in λΠ +modulo (Lean4Less/lean4dk, CoqInE); checked by Dedukti or Lambdapi +|DESIGNED (`dedukti.rs`, `lambdapi.rs` translate syntax only) +|HOL family ↔ Lean 4 / Rocq |`dedukti` |OpenTheory → Dedukti (Holide), +then as above |DESIGNED +|Agda ↔ Lean 4 / Rocq |`dedukti` |Agda → Dedukti (agda2dk, research +prototype) |DESIGNED +|cvc5 / veriT ↔ Rocq |`smt_coq` |Alethe or LFSC certificates replayed by +the Coq kernel (SMTCoq) |DESIGNED (`smtcoq.rs` parses certificates and +emits a skeleton) +|Z3 / cvc5 / veriT ↔ Isabelle/HOL |`smt_lib` |SMT proofs reconstructed by +Isabelle's `smt` method |DESIGNED +|Vampire / E ↔ Isabelle/HOL |`tptp` |TPTP problems generated by +Sledgehammer, proofs reconstructed with Metis |DESIGNED +|=== + +For the automated rows the exchange-layer term is the problem the +interactive side generated, so fidelity there is the interactive +system's translation into SMT-LIB or TPTP; that translation is what a +`KernelTranslation` certificate for the pair has to cover. + === Strategic Expansion Plan ==== Phase 1: Critical Gap Closure (6-12 months) diff --git a/docs/design/TYPING_CAPABILITIES_COMPARISON.adoc b/docs/design/TYPING_CAPABILITIES_COMPARISON.adoc index 125a6926..de8167d5 100644 --- a/docs/design/TYPING_CAPABILITIES_COMPARISON.adoc +++ b/docs/design/TYPING_CAPABILITIES_COMPARISON.adoc @@ -194,7 +194,11 @@ comparing: ==== What We Provide That Single Systems Cannot * *Cross-System Type Arbitration*: Determine when types from different -systems are equivalent +systems are equivalent. Today the arbiter grades each verdict `belief` / +`epi` / `sound` by per-backend fidelity evidence (ECH-05); `sound` needs a +kernel-checked shared term, which no backend pair can produce yet. Pair +table: `ADVANCED_TYPING_GAP_ANALYSIS.adoc`, "Backend pairs that can share +a term". * *Multi-Type-System Proof Routing*: Send proofs to the most appropriate type system * *Heterogeneous Type Safety*: Ensure type safety across mixed-system diff --git a/docs/wikis/Guides.md b/docs/wikis/Guides.md index 132f64d9..b146cdf9 100644 --- a/docs/wikis/Guides.md +++ b/docs/wikis/Guides.md @@ -105,6 +105,8 @@ Motivating examples: You normally don't call the four mechanisms directly. `ResultArbiter` (`src/rust/verification/result_arbiter.rs`) takes the per-prover `ProverOutcome`s from a cross-checked dispatch, adapts them into whichever mechanism `DispatchConfig.arbitration_policy` selects (`portfolio` default | `bayesian` | `dempster_shafer`), and returns an `ArbitratedVerdict`: winning verdict, agreeing/disagreeing/inconclusive camps, a `[0,1]` conflict metric, `needs_review`, and a Pareto-recommended prover among the agreeing set. `Dispatcher::verify_proof_cross_checked` attaches it to `DispatchResult.arbitration`. Key semantics: timeouts and errors are no-information (they no longer veto agreement), and a genuine Proven-vs-Refuted split is flagged for review instead of being flattened to `verified = false`. +Agreement is not identity: N backends proving N lexically aligned statements are N warrants for N propositions. Each `ProverAttempt` therefore carries `FidelityEvidence` — `KernelTranslation { format, checked_by, term_hash }` (a kernel-checked translation through `src/rust/exchange/`), `DeclaredCorrespondence { consequence_tests, failures }`, or `None` — and `ArbitratedVerdict.level` grades the fused verdict `belief` / `epi` / `sound` (ECH-05). `sound` needs every fused attempt to be a kernel translation to the same exchange-layer term; a tested correspondence with no failures gives `epi`; anything else, any attempt without evidence, a verdict that needs review, or one resting on a backend marked unsound with `ResultArbiter::retract` is `belief`. The numeric fusion is unchanged under the level. Dispatch does not attach evidence yet, so every dispatched verdict is `belief` until the exchange bridges can produce certificates (ROADMAP stage 6). The Idris2 statement is `src/abi/EchidnaABI/Arbitration.idr`. + ## Guide: Cross-prover semantic queries The synonym layer carries an optional `semantic_class` tag per entry. Combined with the three cross-prover dictionaries (`_msc2020.toml`, `_wordnet_math.toml`, `_conceptnet_seed.toml`) this gives "every prover's name for the same concept" lookups, fully offline. diff --git a/issues/README.md b/issues/README.md index f10324a6..7dba320e 100644 --- a/issues/README.md +++ b/issues/README.md @@ -4,7 +4,8 @@ SPDX-License-Identifier: CC-BY-SA-4.0 # Issue specifications -Drafted issue specifications for the ParadisEO metaheuristic integration roadmap. +Drafted issue specifications: ECH-01..04, PB and EB for the ParadisEO metaheuristic +integration roadmap; ECH-05 for fidelity-levelled result arbitration. Each file is the body for one GitHub issue; the title and labels are in the file header. To produce an issue body from a file (everything after the `# ` title line, without the SPDX header): @@ -19,6 +20,7 @@ awk 'f;/^# /{f=1}' issues/ | sed '1{/^$/d}' > /tmp/body.md | ECH-02 | hyperpolymath/echidna | #421 | `echidna-02-cmaes-julia-gnn.md` | | ECH-03 | hyperpolymath/echidna | #422 | `echidna-03-chapel-island-migration.md` | | ECH-04 | hyperpolymath/echidna | #424 | `echidna-04-ffi-abi-bridge.md` | +| ECH-05 | hyperpolymath/echidna | not filed | `echidna-05-fidelity-evidence.md` | | PB-01 | hyperpolymath/proof-burrower | not filed | `proof-burrower-01-combinatorial-tactic-synthesis.md` | | PB-02 | hyperpolymath/proof-burrower | not filed | `proof-burrower-02-ledger-fitness-formulation.md` | | EB-01 | hyperpolymath/echidnabot | not filed | `echidnabot-01-adaptive-ci-portfolio-scheduler.md` | @@ -28,6 +30,7 @@ awk 'f;/^# /{f=1}' issues/ | sed '1{/^$/d}' > /tmp/body.md ## Status - **ECH-01..04** are filed on hyperpolymath/echidna and carry all their labels. On 2026-10-09 their bodies were replaced by hand with a different text that is not these files; the owner decides which is canonical (see `docs/handover/PARADISEO-ROADMAP-PROMPT.adoc`, WP0). `scripts/issues/sync-roadmap-issues.sh` syncs the bodies from these files (dry run by default; refuses to replace hand-edited bodies without `--overwrite`). +- **ECH-05** is a draft for hyperpolymath/echidna, not filed. Its implementation (fidelity evidence on `ProverAttempt`, `level` on `ArbitratedVerdict`, `EchidnaABI.Arbitration`, the fidelity tests) lands with the PR that adds the file. - **PB-01, PB-02, EB-01** are drafts for copying to their own repositories. They are not filed. ## Provenance of the PB and EB drafts @@ -46,5 +49,6 @@ Labels named in the drafts that did not exist when they were written (checked 20 |------------------------------|---------------------------------------------------------------------| | hyperpolymath/proof-burrower | `area:swarm`, `rust`, `search-tactics`, `area:ledger`, `heuristics` | | hyperpolymath/echidnabot | `area:dispatcher`, `ci-optimization` (`rust` exists) | +| hyperpolymath/echidna | `area:arbitration`, `area:exchange`, `epistemic-types`, `residual-evidence-types` (ECH-05; checked 2026-10-14) | -All labels used by ECH-01..04 exist on hyperpolymath/echidna. +All labels used by ECH-01..04 exist on hyperpolymath/echidna; ECH-05's `enhancement` and `idris2` do. diff --git a/issues/echidna-05-fidelity-evidence.md b/issues/echidna-05-fidelity-evidence.md new file mode 100644 index 00000000..cb74d1e6 --- /dev/null +++ b/issues/echidna-05-fidelity-evidence.md @@ -0,0 +1,70 @@ + + +# ECH-05: feat(arbitration): consume fidelity evidence, not N re-proofs — type the arbiter's input by alignment certificate and level its verdict + +- **Repository:** hyperpolymath/echidna +- **Labels:** enhancement, area:arbitration, area:exchange, epistemic-types, residual-evidence-types, idris2 +- **Area:** result arbitration / cross-prover exchange / Idris2 ABI +- **Depends on:** epistemic-types `6a68de3`; residual-evidence-types `97244f5` + +## Summary + +`ResultArbiter::arbitrate(&[ProverAttempt]) -> ArbitratedVerdict` (`src/rust/verification/result_arbiter.rs`), with `pareto_arbiter.rs` and `dempster_shafer.rs` beside it, fuses N backend outcomes for what it treats as one goal. Alignment between backends is lexical — per-prover synonym tables under `data/synonyms/` with MSC2020 / WordNet / ConceptNet — and the exchange layer (`src/rust/exchange/`, six formats) is the kernel-checked translation tier that ROADMAP stage 6 ("cross-prover semantics — translation actually works") says is not yet real. N re-proofs of N possibly different statements are N warrants for N propositions, not one sound warrant for the source claim. + +What the arbiter should consume is fidelity evidence: per backend, a certificate that the formal statement denotes the source claim — a kernel-checked translation through the exchange layer, or a declared correspondence validated by consequence testing — and it fuses only attempts whose certificates agree. In epistemic-types' terms each prover is a standpoint (`K`); a proof is `Epi` for its formal statement; the source claim is `A`; the certificate is the `sound` map from the formal statement's evidence to `A`; without it the fused verdict is belief about the source claim (`no-receipt-reflection`), however many provers agree. Content in a formal statement with no counterpart in the source must not cross, and residual-evidence-types' coarsening gives the direction: a coarse claim transfers to the fine observation, not back (`coarsen-claim`). + +Not claimed: a solution to autoformalisation (undecidable in general). Claimed: the arbiter's input and output types change, and a synonym collision can no longer fuse to `sound`. echo-types' order-type "fidelity" (Buchholz, OPEN) is a different object and is not used here. + +## Context + +Proof work that applies now (sibling artefacts checked at the pinned commits on 2026-10-14): + +| ID | Claim | Status | Artefact | +|------|-------|--------|----------| +| E-1 | `Warrant` / `Epi` / `SoundWarrant` / `sound-epi` | PROVEN | epistemic-types `EpistemicTypes.Warrant` | +| E-2 | agreement without a soundness map is belief | PROVEN | epistemic-types `EpistemicTypes.Applications.RapidNJSkip.no-receipt-reflection` | +| RE-K | composed claims never derive the composed case; `component-left/right` | PROVEN | residual-evidence-types `ResidualEvidence.Composition.compose-claims` | +| RE-D | coarsening transfers one way only | PROVEN | `ResidualEvidence.Composition.coarsen-candidate/case/claim` | +| RE-R | retracting a source retracts what rested on it | PROVEN | `ResidualEvidence.Revision.retract-*`, `dependent-holds` | +| EC-1 | arbiters exist (Rust): result, Pareto, Dempster–Shafer | TESTED | `src/rust/verification/`; `cargo test --lib result_arbiter` | +| EC-2 | exchange layer: OpenTheory, Dedukti, TPTP, SMT-LIB, SMTCoq, Lambdapi | DESIGNED → partial | ROADMAP stage 6a/6b | +| EC-3 | Idris2 ABI gate: zero `believe_me`, postulates, admits | TESTED | `idris2-abi-ci.yml` | + +- `ProverAttempt { prover, outcome, elapsed_ms }` carries no statement identity beyond the goal it was handed; `ArbitratedVerdict` is scalar. +- `docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc` and `TYPING_CAPABILITIES_COMPARISON.adoc` already compare backend type theories; they are the place to say which pairs can share a kernel-checked term. +- ECH-01..04 are filed (#420–#422, #424); their canonical text is undecided and is not reopened here. + +## Proposed Work + +1. **Input type.** `ProverAttempt` gains `fidelity: FidelityEvidence` = `KernelTranslation { format, checked_by, term_hash }` | `DeclaredCorrespondence { consequence_tests, failures }` | `None`. `ArbitratedVerdict` gains `level ∈ {sound, epi, belief}`. Policy: any `None` attempt caps the level at `belief`; `sound` requires every fused attempt to carry `KernelTranslation` to the same exchange-layer term (`term_hash` equality); `DeclaredCorrespondence` with zero failures yields `epi`. Existing numeric fusion is unchanged below the level. +2. **ABI.** `src/abi/EchidnaABI/Arbitration.idr`: the three-level verdict as a closed sum whose `Sound` constructor takes the hash-equality proof; total; passes the ABI gate. +3. **Tests.** `tests/arbitration_fidelity_test.rs`: two backends proving two lexically aligned but formally distinct statements (a synonym collision) must not fuse above `belief`; a MiniF2F-aligned pair (aligned across Lean, Isabelle, HOL Light, Metamath, Coq) with kernel-checked translations is the positive control for `sound`; a retracted backend (marked unsound) lowers every verdict that rested on it (RE-R). +4. **Docs.** ROADMAP stage 6 acceptance becomes "a `KernelTranslation` certificate is producible for pair X"; `issues/README.md` gains ECH-05; the gap-analysis documents name which backend pairs can share a term. + +As the proofs progress: + +- Bidirectional exchange (OpenTheory, 6a) → the forward-then-back translation check becomes a round trip, and a lossless round trip is a Loss-grade-𝟙 witness (resource-algebra `Instances/Loss.agda`) — the certificate gets a grade. +- choreographic-types standpoints → multi-prover protocols as choreographies, with K-CUT-WARRANT giving what each backend can know of the global verdict. +- VeriSimDB → certificates stored as first-class objects with the term hash as key. + +## Acceptance Criteria + +- [ ] `ProverAttempt` / `ArbitratedVerdict` type change compiles; `cargo test` green; existing arbitration numbers unchanged at level `belief` (regression fixture). +- [ ] `Arbitration.idr` passes `idris2-abi-ci.yml`. +- [ ] Synonym-collision test cannot reach `sound`; MiniF2F positive control reaches `sound`; retraction test lowers dependent verdicts. +- [ ] ROADMAP, gap-analysis docs and `issues/README.md` updated; the ECH-01..04 canonical-text question is not reopened here. +- [ ] CodeRabbit findings and CI anomalies addressed per the standing rule. + +## Out of Scope + +- Making the Dedukti/OpenTheory bridges real (stage 6 itself). +- GNN tactic suggestion. +- VeriSimDB standup. +- The Chapel island migration (ECH-03). + +## Open Questions + +- Is Dempster–Shafer fusion retained for same-encoding automated provers only, or across kernels under a certificate? +- Who runs consequence testing for `DeclaredCorrespondence`, and against which corpus beyond MiniF2F? diff --git a/scripts/abi-fixtures.sh b/scripts/abi-fixtures.sh new file mode 100755 index 00000000..d8b41273 --- /dev/null +++ b/scripts/abi-fixtures.sh @@ -0,0 +1,62 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# Mechanical falsifier for the Idris2 ABI (src/abi): every fixture under +# tests/abi/accept must type-check, and every fixture under tests/abi/reject +# must be refused with a unification error. Each reject fixture names the +# accept fixture it mirrors, so a refusal is attributable to the one change. +# +# Exit codes alone are not trusted: `idris2 --check` exits 0 on an +# unresolved import (see the proofs-verif-idris recipe in the Justfile), so +# accept requires no `Error` in the output and reject requires a unification +# error specifically. +set -euo pipefail + +root="$(cd "$(dirname "$0")/.." && pwd)" +abi="$root/src/abi" +status=0 + +# Fixtures import EchidnaABI.* from the package's build output. +(cd "$abi" && idris2 --build echidnaabi.ipkg >/dev/null) +export IDRIS2_PATH="$abi/build/ttc${IDRIS2_PATH:+:$IDRIS2_PATH}" + +check() { + # Each fixture is checked in a fresh directory: a build/ cache left next + # to a fixture by an earlier run can make idris2 skip the check entirely. + local tmp + tmp="$(mktemp -d)" + cp "$1" "$tmp/" + (cd "$tmp" && idris2 --check "$(basename "$1")" 2>&1) || true + rm -rf "$tmp" +} + +for f in "$root"/tests/abi/accept/*.idr; do + rel="${f#"$root"/}" + out="$(check "$f")" + if printf '%s\n' "$out" | grep -q 'Error'; then + echo "FAIL accept fixture refused: $rel" + printf '%s\n' "$out" | sed 's/^/ /' + status=1 + else + echo "ok accept: $rel" + fi +done + +for f in "$root"/tests/abi/reject/*.idr; do + rel="${f#"$root"/}" + out="$(check "$f")" + if printf '%s\n' "$out" | grep -q 'Mismatch between'; then + echo "ok reject: $rel" + printf '%s\n' "$out" | grep -m1 'Mismatch between' | sed 's/^/ /' + elif printf '%s\n' "$out" | grep -q 'Error'; then + echo "FAIL reject fixture refused for a non-type reason: $rel" + printf '%s\n' "$out" | sed 's/^/ /' + status=1 + else + echo "FAIL reject fixture type-checked: $rel" + status=1 + fi +done + +exit "$status" diff --git a/src/abi/EchidnaABI/Arbitration.idr b/src/abi/EchidnaABI/Arbitration.idr new file mode 100644 index 00000000..309a0589 --- /dev/null +++ b/src/abi/EchidnaABI/Arbitration.idr @@ -0,0 +1,428 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell + +||| ECHIDNA ABI — Arbitration fidelity levels (ECH-05) +||| +||| The Idris2 statement of the level an arbitrated verdict carries for +||| the source claim. Rust mirror: `FidelityEvidence`, `EpistemicLevel` +||| and `fidelity_level` in `src/rust/verification/result_arbiter.rs`. +||| +||| `Level fused` is a closed sum indexed by the evidence of the fused +||| attempts. Its `Sound` constructor takes, for every fused attempt, a +||| proof that the attempt is a kernel-checked translation whose term +||| hash equals the shared hash `h`. A `Sound` value therefore cannot be +||| built for a list holding two different term hashes (a synonym +||| collision), a declared correspondence, or no evidence — whatever +||| produced it. `level` is the classifier. The Rust `fidelity_level` +||| implements the same policy; that correspondence is by review, not +||| mechanically checked. +||| +||| The module is parametric in the hash type and needs only `DecEq` on +||| it. The runtime hash is the BLAKE3 hex digest from +||| `src/rust/exchange/mod.rs::term_hash`; the examples below use `Bool` +||| as a two-point hash space so that distinctness is constructive. +||| +||| Proves: +||| 1. kernelAtHash: a KernelAt witness yields the hash equality +||| 2. collisionNotSound: two fused kernel translations with different +||| hashes make every `Level fused` non-Sound +||| 3. correspondenceNotSound / noEvidenceNotSound: such evidence in +||| the fused list makes every `Level fused` non-Sound +||| 4. blockedIsBelief: review or retraction caps `level` at Belief +||| 5. noEvidenceIsBelief: an attempt without evidence caps `level` at +||| Belief, fused or not +||| 6. failedCorrespondenceIsBelief / untestedCorrespondenceIsBelief +||| 7. emptyFusedIsBelief, blockingNeverRaises +||| 8. alignedPairIsSound / collisionPairIsBelief / mixedPairIsEpi +||| (positive and negative controls, by evaluation) +||| +||| Correspondence, not import: the levels follow epistemic-types +||| `EpistemicTypes.Warrant` (`Warrant`, `Epi`, `SoundWarrant`, +||| `sound-epi`) and `no-receipt-reflection` +||| (`EpistemicTypes.Applications.RapidNJSkip`) at pin 6a68de3; retraction +||| follows residual-evidence-types `ResidualEvidence.Revision` +||| (`retract-case`, `dependent-holds`) at pin 97244f5. Nothing here is +||| proved about those Agda developments; they are cited, not consumed. +||| +||| NO believe-me, NO postulates, NO admits. + +module EchidnaABI.Arbitration + +import Data.List +import Data.Nat +import Data.List.Elem +import Data.List.Quantifiers +import Decidable.Equality + +%default total + +------------------------------------------------------------------------ +-- Evidence +------------------------------------------------------------------------ + +||| Exchange-layer formats, one per bridge in `src/rust/exchange/`. +public export +data ExchangeFormat = OpenTheory | Dedukti | Lambdapi | Tptp | SmtLib | SmtCoq + +||| Evidence that a backend's formal statement denotes the source claim. +public export +data Fidelity : (hash : Type) -> Type where + ||| Translated through the exchange layer and checked by a kernel; + ||| `termHash` names the exchange-layer term. + KernelTranslation : (format : ExchangeFormat) -> (checkedBy : String) -> + (termHash : hash) -> Fidelity hash + ||| A declared correspondence checked by consequence testing. + DeclaredCorrespondence : (consequenceTests : Nat) -> (failures : Nat) -> + Fidelity hash + ||| No evidence beyond the goal handed to the backend. + NoEvidence : Fidelity hash + +||| `KernelAt h e`: `e` is a kernel translation whose term hash is `h`. +||| The constructor carries the hash-equality proof. +public export +data KernelAt : hash -> Fidelity hash -> Type where + MkKernelAt : (hashEq : h' = h) -> KernelAt h (KernelTranslation f c h') + +||| Projection of the hash equality. +export +kernelAtHash : KernelAt h (KernelTranslation f c h') -> h' = h +kernelAtHash (MkKernelAt hashEq) = hashEq + +export +noKernelAtCorrespondence : KernelAt h (DeclaredCorrespondence t k) -> Void +noKernelAtCorrespondence (MkKernelAt _) impossible + +export +noKernelAtNoEvidence : KernelAt h NoEvidence -> Void +noKernelAtNoEvidence (MkKernelAt _) impossible + +------------------------------------------------------------------------ +-- The three-level verdict +------------------------------------------------------------------------ + +||| The level of an arbitrated verdict, indexed by the evidence of the +||| attempts that were fused into it. +public export +data Level : List (Fidelity hash) -> Type where + ||| Agreement without a fidelity map to the source claim. + Belief : Level fused + ||| Every fused attempt has fidelity evidence, not all of it kernel. + Epi : Level fused + ||| Every fused attempt is a kernel translation to the term `h`. + Sound : (h : hash) -> NonEmpty fused -> All (KernelAt h) fused -> + Level fused + +||| Belief < Epi < Sound. +public export +rank : Level fused -> Nat +rank Belief = 0 +rank Epi = 1 +rank (Sound _ _ _) = 2 + +public export +isSound : Level fused -> Bool +isSound (Sound _ _ _) = True +isSound _ = False + +------------------------------------------------------------------------ +-- Sound is closed under the type +------------------------------------------------------------------------ + +elemAll : Elem x xs -> All p xs -> p x +elemAll Here (px :: _) = px +elemAll (There e) (_ :: pxs) = elemAll e pxs + +||| A synonym collision cannot be typed Sound: if two fused attempts are +||| kernel translations to different terms, no `Level fused` is Sound. +export +collisionNotSound : Elem (KernelTranslation f1 c1 h1) fused -> + Elem (KernelTranslation f2 c2 h2) fused -> + Not (h1 = h2) -> + (l : Level fused) -> isSound l = False +collisionNotSound _ _ _ Belief = Refl +collisionNotSound _ _ _ Epi = Refl +collisionNotSound e1 e2 neq (Sound _ _ allK) = + void (neq (trans (kernelAtHash (elemAll e1 allK)) + (sym (kernelAtHash (elemAll e2 allK))))) + +||| A fused declared correspondence rules out Sound. +export +correspondenceNotSound : Elem (DeclaredCorrespondence t k) fused -> + (l : Level fused) -> isSound l = False +correspondenceNotSound _ Belief = Refl +correspondenceNotSound _ Epi = Refl +correspondenceNotSound e (Sound _ _ allK) = + void (noKernelAtCorrespondence (elemAll e allK)) + +||| A fused attempt without evidence rules out Sound. +export +noEvidenceNotSound : Elem NoEvidence fused -> + (l : Level fused) -> isSound l = False +noEvidenceNotSound _ Belief = Refl +noEvidenceNotSound _ Epi = Refl +noEvidenceNotSound e (Sound _ _ allK) = + void (noKernelAtNoEvidence (elemAll e allK)) + +------------------------------------------------------------------------ +-- The classifier +------------------------------------------------------------------------ + +||| True when no attempt lacks evidence. +public export +allEvidenced : List (Fidelity hash) -> Bool +allEvidenced [] = True +allEvidenced (NoEvidence :: _) = False +allEvidenced (KernelTranslation _ _ _ :: es) = allEvidenced es +allEvidenced (DeclaredCorrespondence _ _ :: es) = allEvidenced es + +||| A correspondence counts with at least one test and no failures. +public export +correspondenceOk : (tests : Nat) -> (failures : Nat) -> Bool +correspondenceOk (S _) Z = True +correspondenceOk _ _ = False + +||| True when every item is a kernel translation or an accepted +||| correspondence. +public export +allWarranted : List (Fidelity hash) -> Bool +allWarranted [] = True +allWarranted (NoEvidence :: _) = False +allWarranted (KernelTranslation _ _ _ :: es) = allWarranted es +allWarranted (DeclaredCorrespondence t k :: es) = + if correspondenceOk t k then allWarranted es else False + +||| The term hashes of the kernel translations, in order. +public export +kernelHashes : List (Fidelity hash) -> List hash +kernelHashes [] = [] +kernelHashes (KernelTranslation _ _ h :: es) = h :: kernelHashes es +kernelHashes (DeclaredCorrespondence _ _ :: es) = kernelHashes es +kernelHashes (NoEvidence :: es) = kernelHashes es + +public export +allEqualTo : DecEq a => a -> List a -> Bool +allEqualTo _ [] = True +allEqualTo x (y :: ys) = case decEq x y of + Yes _ => allEqualTo x ys + No _ => False + +public export +allEqual : DecEq a => List a -> Bool +allEqual [] = True +allEqual (x :: xs) = allEqualTo x xs + +allHead : All p (x :: xs) -> p x +allHead (px :: _) = px + +allTail : All p (x :: xs) -> All p xs +allTail (_ :: pxs) = pxs + +public export +decAll : ((x : a) -> Dec (p x)) -> (xs : List a) -> Dec (All p xs) +decAll _ [] = Yes [] +decAll d (x :: xs) = case d x of + No contra => No (contra . allHead) + Yes px => case decAll d xs of + Yes pxs => Yes (px :: pxs) + No contra => No (contra . allTail) + +notKernelAt : Not (h' = h) -> Not (KernelAt h (KernelTranslation f c h')) +notKernelAt contra (MkKernelAt hashEq) = contra hashEq + +public export +decKernelAt : DecEq hash => (h : hash) -> (e : Fidelity hash) -> + Dec (KernelAt h e) +decKernelAt h (KernelTranslation f c h') = case decEq h' h of + Yes hashEq => Yes (MkKernelAt hashEq) + No contra => No (notKernelAt contra) +decKernelAt _ (DeclaredCorrespondence _ _) = No noKernelAtCorrespondence +decKernelAt _ NoEvidence = No noKernelAtNoEvidence + +||| Sound when every item is a kernel translation to the first item's +||| term, Epi otherwise. Called only on warranted, hash-agreeing lists. +public export +soundOrEpi : DecEq hash => (fused : List (Fidelity hash)) -> Level fused +soundOrEpi [] = Belief +soundOrEpi fused@(KernelTranslation _ _ h :: _) = + case decAll (decKernelAt h) fused of + Yes allK => Sound h IsNonEmpty allK + No _ => Epi +soundOrEpi (DeclaredCorrespondence _ _ :: _) = Epi +soundOrEpi (NoEvidence :: _) = Belief + +||| Pass `l` through when the flag holds, Belief otherwise. +public export +gateOk : Bool -> Level fused -> Level fused +gateOk True l = l +gateOk False _ = Belief + +||| The level of the fused attempts alone. +public export +fusedLevel : DecEq hash => (fused : List (Fidelity hash)) -> Level fused +fusedLevel fused = + gateOk (allWarranted fused) + (gateOk (allEqual (kernelHashes fused)) (soundOrEpi fused)) + +||| The ECH-05 levelling policy. `attempts` is every attempt's evidence, +||| `fused` the evidence of the attempts fused into the verdict, and +||| `blocked` is set when the verdict needs review or rests on a +||| retracted backend. (The Rust side also rejects an empty hash string, +||| which the abstract hash type has no counterpart for.) +public export +level : DecEq hash => (attempts, fused : List (Fidelity hash)) -> + (blocked : Bool) -> Level fused +level _ _ True = Belief +level attempts fused False = gateOk (allEvidenced attempts) (fusedLevel fused) + +------------------------------------------------------------------------ +-- Classifier properties +------------------------------------------------------------------------ + +gateOkFalse : (b : Bool) -> b = False -> (l : Level fused) -> + gateOk b l = Belief +gateOkFalse False Refl _ = Refl + +gateOkBelief : (b : Bool) -> (l : Level fused) -> l = Belief -> + gateOk b l = Belief +gateOkBelief True _ prf = prf +gateOkBelief False _ _ = Refl + +elemNoEvidence : (xs : List (Fidelity hash)) -> Elem NoEvidence xs -> + allEvidenced xs = False +elemNoEvidence (NoEvidence :: _) _ = Refl +elemNoEvidence (KernelTranslation _ _ _ :: es) (There e) = + elemNoEvidence es e +elemNoEvidence (DeclaredCorrespondence _ _ :: es) (There e) = + elemNoEvidence es e + +||| A correspondence that is not accepted falsifies `allWarranted`. +elemBadCorrespondence : (xs : List (Fidelity hash)) -> + correspondenceOk t k = False -> + Elem (DeclaredCorrespondence t k) xs -> + allWarranted xs = False +elemBadCorrespondence (NoEvidence :: _) _ _ = Refl +elemBadCorrespondence (DeclaredCorrespondence _ _ :: _) bad Here = + rewrite bad in Refl +elemBadCorrespondence (DeclaredCorrespondence t' k' :: es) bad (There e) with (correspondenceOk t' k') + _ | True = elemBadCorrespondence es bad e + _ | False = Refl +elemBadCorrespondence (KernelTranslation _ _ _ :: es) bad (There e) = + elemBadCorrespondence es bad e + +||| A correspondence with a failed consequence test is never accepted. +failedNotOk : (t : Nat) -> correspondenceOk t (S k) = False +failedNotOk Z = Refl +failedNotOk (S _) = Refl + +||| (4) A verdict that needs review or rests on a retracted backend is +||| Belief. +export +blockedIsBelief : DecEq hash => (attempts, fused : List (Fidelity hash)) -> + level attempts fused True = Belief +blockedIsBelief _ _ = Refl + +||| (5) One attempt without evidence anywhere in the input caps the level +||| at Belief. +export +noEvidenceIsBelief : DecEq hash => (attempts, fused : List (Fidelity hash)) -> + (blocked : Bool) -> Elem NoEvidence attempts -> + level attempts fused blocked = Belief +noEvidenceIsBelief _ _ True _ = Refl +noEvidenceIsBelief attempts fused False e = + gateOkFalse (allEvidenced attempts) (elemNoEvidence attempts e) + (fusedLevel fused) + +fusedBadCorrespondence : DecEq hash => (fused : List (Fidelity hash)) -> + correspondenceOk t k = False -> + Elem (DeclaredCorrespondence t k) fused -> + fusedLevel fused = Belief +fusedBadCorrespondence fused bad e = + gateOkFalse (allWarranted fused) (elemBadCorrespondence fused bad e) + (gateOk (allEqual (kernelHashes fused)) (soundOrEpi fused)) + +||| (6a) A fused correspondence with a failed consequence test is Belief. +export +failedCorrespondenceIsBelief : + DecEq hash => {t : Nat} -> + (attempts, fused : List (Fidelity hash)) -> (blocked : Bool) -> + Elem (DeclaredCorrespondence t (S k)) fused -> + level attempts fused blocked = Belief +failedCorrespondenceIsBelief _ _ True _ = Refl +failedCorrespondenceIsBelief {t} attempts fused False e = + gateOkBelief (allEvidenced attempts) (fusedLevel fused) + (fusedBadCorrespondence fused (failedNotOk t) e) + +||| (6b) A fused correspondence with no consequence tests is Belief. +export +untestedCorrespondenceIsBelief : + DecEq hash => (attempts, fused : List (Fidelity hash)) -> (blocked : Bool) -> + Elem (DeclaredCorrespondence Z k) fused -> + level attempts fused blocked = Belief +untestedCorrespondenceIsBelief _ _ True _ = Refl +untestedCorrespondenceIsBelief attempts fused False e = + gateOkBelief (allEvidenced attempts) (fusedLevel fused) + (fusedBadCorrespondence fused Refl e) + +||| (7a) Nothing fused, nothing warranted. +export +emptyFusedIsBelief : DecEq hash => (attempts : List (Fidelity hash)) -> + (blocked : Bool) -> + level attempts [] blocked = Belief +emptyFusedIsBelief _ True = Refl +emptyFusedIsBelief attempts False = + gateOkBelief (allEvidenced attempts) (fusedLevel []) Refl + +||| (7b) Blocking (review, retraction) never raises the level. +export +blockingNeverRaises : DecEq hash => (attempts, fused : List (Fidelity hash)) -> + (blocked : Bool) -> + LTE (rank (level attempts fused True)) + (rank (level attempts fused blocked)) +blockingNeverRaises _ _ _ = LTEZero + +------------------------------------------------------------------------ +-- Controls, by evaluation (hash space Bool) +------------------------------------------------------------------------ + +||| Two kernel translations of one term (MiniF2F-style aligned pair). +public export +alignedPair : List (Fidelity Bool) +alignedPair = [ KernelTranslation Dedukti "lean4" True + , KernelTranslation Dedukti "isabelle" True ] + +||| Two kernel translations of different terms (synonym collision). +public export +collisionPair : List (Fidelity Bool) +collisionPair = [ KernelTranslation Dedukti "lean4" True + , KernelTranslation Dedukti "metamath" False ] + +||| A kernel translation and a tested, failure-free correspondence. +public export +mixedPair : List (Fidelity Bool) +mixedPair = [ KernelTranslation Dedukti "lean4" True + , DeclaredCorrespondence 12 0 ] + +export +alignedPairIsSound : + isSound (level Arbitration.alignedPair Arbitration.alignedPair False) = True +alignedPairIsSound = Refl + +export +collisionPairIsBelief : + rank (level Arbitration.collisionPair Arbitration.collisionPair False) = 0 +collisionPairIsBelief = Refl + +export +mixedPairIsEpi : + rank (level Arbitration.mixedPair Arbitration.mixedPair False) = 1 +mixedPairIsEpi = Refl + +trueNotFalse : Not (True = False) +trueNotFalse Refl impossible + +||| The collision is ruled out by the type, not only by `level`. +export +collisionPairNeverSound : + (l : Level Arbitration.collisionPair) -> isSound l = False +collisionPairNeverSound = + collisionNotSound Here (There Here) trueNotFalse diff --git a/src/abi/echidnaabi.ipkg b/src/abi/echidnaabi.ipkg index 2b0ec6da..6c9a550b 100644 --- a/src/abi/echidnaabi.ipkg +++ b/src/abi/echidnaabi.ipkg @@ -21,6 +21,7 @@ depends = base modules = EchidnaABI.AxiomTracker , EchidnaABI.Gnn , EchidnaABI.TacticRecord + , EchidnaABI.Arbitration , EchidnaABI.Types , EchidnaABI.Layout , EchidnaABI.Foreign diff --git a/src/rust/exchange/mod.rs b/src/rust/exchange/mod.rs index f3ce2cb2..7ac5f5ea 100644 --- a/src/rust/exchange/mod.rs +++ b/src/rust/exchange/mod.rs @@ -27,3 +27,72 @@ pub mod tptp; pub use dedukti::DeduktiExporter; pub use opentheory::OpenTheoryExporter; + +use serde::{Deserialize, Serialize}; + +/// The exchange-layer formats a cross-prover translation can go through +/// — one per bridge module above. Named by a `KernelTranslation` +/// fidelity certificate (`crate::verification::result_arbiter`, ECH-05). +#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum ExchangeFormat { + OpenTheory, + Dedukti, + Lambdapi, + Tptp, + SmtLib, + SmtCoq, +} + +impl ExchangeFormat { + /// Stable tag used for domain separation in [`term_hash`]. + pub fn tag(self) -> &'static str { + match self { + ExchangeFormat::OpenTheory => "opentheory", + ExchangeFormat::Dedukti => "dedukti", + ExchangeFormat::Lambdapi => "lambdapi", + ExchangeFormat::Tptp => "tptp", + ExchangeFormat::SmtLib => "smtlib", + ExchangeFormat::SmtCoq => "smtcoq", + } + } +} + +/// BLAKE3 identity of an exchange-layer term, hex-encoded. +/// +/// The hash is domain-separated by `format`, so equal hashes imply the +/// same format as well as the same term text. It is taken over the term +/// *as rendered*: no canonicalisation (that is roadmap stage 6c), so two +/// renderings of α-equivalent terms hash differently. The failure mode +/// is therefore a missed `sound` level in arbitration, never a false one. +pub fn term_hash(format: ExchangeFormat, term: &str) -> String { + let mut hasher = blake3::Hasher::new(); + hasher.update(b"echidna/exchange-term/v1\0"); + hasher.update(format.tag().as_bytes()); + hasher.update(b"\0"); + hasher.update(term.as_bytes()); + hasher.finalize().to_hex().to_string() +} + +#[cfg(test)] +mod term_hash_tests { + use super::*; + + #[test] + fn term_hash_is_deterministic_and_format_separated() { + let t = "forall (n : nat), eq nat (add n zero) n"; + assert_eq!( + term_hash(ExchangeFormat::Dedukti, t), + term_hash(ExchangeFormat::Dedukti, t) + ); + assert_ne!( + term_hash(ExchangeFormat::Dedukti, t), + term_hash(ExchangeFormat::Lambdapi, t) + ); + assert_ne!( + term_hash(ExchangeFormat::Dedukti, t), + term_hash(ExchangeFormat::Dedukti, "forall (n : nat), eq nat n n") + ); + assert_eq!(term_hash(ExchangeFormat::Tptp, t).len(), 64); + } +} diff --git a/src/rust/verification/mod.rs b/src/rust/verification/mod.rs index 728c347a..731219f0 100644 --- a/src/rust/verification/mod.rs +++ b/src/rust/verification/mod.rs @@ -58,5 +58,8 @@ pub use portfolio::{PortfolioConfig, PortfolioResult, PortfolioSolver}; pub use proof::{ theorem_identity, Proof, ProofStateRecord, ProofVersion, TacticApplication, TacticStatus, }; -pub use result_arbiter::{ArbitratedVerdict, ArbitrationPolicy, ProverAttempt, ResultArbiter}; +pub use result_arbiter::{ + ArbitratedVerdict, ArbitrationPolicy, EpistemicLevel, FidelityEvidence, ProverAttempt, + ResultArbiter, +}; pub use statistics::{StatisticsTracker, StatsSummaryRecord}; diff --git a/src/rust/verification/result_arbiter.rs b/src/rust/verification/result_arbiter.rs index 4c9702e6..1051524e 100644 --- a/src/rust/verification/result_arbiter.rs +++ b/src/rust/verification/result_arbiter.rs @@ -26,6 +26,32 @@ //! - `InconsistentPremises` from any prover sets `suspect_premises` //! (and `needs_review`): an unqualified PROVED over inconsistent //! premises is epistemically worthless. +//! +//! # Fidelity level (ECH-05) +//! +//! Agreement between backends says nothing about whether they proved +//! the *same* statement: N re-proofs of N lexically aligned statements +//! are N warrants for N propositions. Each [`ProverAttempt`] therefore +//! carries [`FidelityEvidence`] that its formal statement denotes the +//! source claim, and [`ArbitratedVerdict::level`] grades the fused +//! verdict by that evidence ([`fidelity_level`]): +//! +//! - `Belief` if the verdict needs review, rests on a retracted backend +//! ([`ResultArbiter::retract`]), or any attempt carries +//! [`FidelityEvidence::None`]; also when no attempt was fused. +//! - `Sound` only if every fused attempt carries a +//! [`FidelityEvidence::KernelTranslation`] and all of them name the +//! same exchange-layer `term_hash`. +//! - `Epi` if every fused attempt is a kernel translation or a +//! [`FidelityEvidence::DeclaredCorrespondence`] with at least one +//! consequence test and zero failures, and the kernel translations +//! agree on the term. +//! - `Belief` otherwise — in particular when two kernel translations +//! name different terms (a synonym collision). +//! +//! The level sits on top of the numeric fusion, which is unchanged: +//! `tests/arbitration_regression_test.rs` replays the pre-ECH-05 numbers. +//! The Idris2 statement of the levels is `src/abi/EchidnaABI/Arbitration.idr`. use serde::{Deserialize, Serialize}; @@ -36,26 +62,81 @@ use super::dempster_shafer::{ }; use super::pareto_arbiter::{AttemptOutcome, ParetoArbiter}; use super::portfolio::{PortfolioConfidence, PortfolioSolver, SolverResult}; +use crate::exchange::ExchangeFormat; use crate::provers::outcome::ProverOutcome; use crate::provers::ProverKind; +/// Evidence that a backend's formal statement denotes the source claim. +#[derive(Debug, Clone, PartialEq, Eq, Default, Serialize, Deserialize)] +#[serde(tag = "kind", rename_all = "snake_case")] +pub enum FidelityEvidence { + /// The statement was translated through the exchange layer and the + /// translation was checked by `checked_by`'s kernel. `term_hash` + /// names the exchange-layer term (see [`crate::exchange::term_hash`]). + KernelTranslation { + format: ExchangeFormat, + checked_by: ProverKind, + term_hash: String, + }, + /// A declared correspondence (e.g. a synonym-table alignment) that + /// was checked by consequence testing: `failures` of + /// `consequence_tests` consequences of the source claim were not + /// consequences of the formal statement, or vice versa. + DeclaredCorrespondence { + consequence_tests: u32, + failures: u32, + }, + /// No evidence beyond the goal the backend was handed (lexical + /// alignment at best). Caps the arbitrated level at `Belief`. + #[default] + None, +} + +/// How far an arbitrated verdict is warranted for the source claim. +/// Ordered `Belief < Epi < Sound`. +#[derive( + Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Default, Serialize, Deserialize, +)] +#[serde(rename_all = "snake_case")] +pub enum EpistemicLevel { + /// Agreement without a fidelity map to the source claim. + #[default] + Belief, + /// Every fused attempt has fidelity evidence, not all of it a + /// kernel-checked translation. + Epi, + /// Every fused attempt is a kernel-checked translation to one + /// exchange-layer term. + Sound, +} + /// One prover's contribution to arbitration: which backend ran, what it -/// concluded, and how long it took. +/// concluded, how long it took, and the evidence that its statement is +/// the source claim. #[derive(Debug, Clone, Serialize, Deserialize)] pub struct ProverAttempt { pub prover: ProverKind, pub outcome: ProverOutcome, pub elapsed_ms: u64, + #[serde(default)] + pub fidelity: FidelityEvidence, } impl ProverAttempt { + /// An attempt with no fidelity evidence. pub fn new(prover: ProverKind, outcome: ProverOutcome, elapsed_ms: u64) -> Self { Self { prover, outcome, elapsed_ms, + fidelity: FidelityEvidence::None, } } + + pub fn with_fidelity(mut self, fidelity: FidelityEvidence) -> Self { + self.fidelity = fidelity; + self + } } /// Which fusion mechanism decides the verdict. @@ -114,6 +195,18 @@ pub struct ArbitratedVerdict { pub recommended: Option, /// The policy that produced this verdict. pub policy: ArbitrationPolicy, + /// How far `verdict` is warranted for the source claim, from the + /// attempts' fidelity evidence (see [`fidelity_level`]). + #[serde(default)] + pub level: EpistemicLevel, + /// Retracted backends among the fused attempts; non-empty forces + /// `level` to `Belief`. + #[serde(default)] + pub retracted: Vec, + /// The exchange-layer term hash all fused attempts share; set only + /// when `level` is `Sound`. + #[serde(default)] + pub warranted_term: Option, } /// Map a rich prover outcome onto the arbitration verdict frame. @@ -135,6 +228,58 @@ pub fn outcome_to_verdict(outcome: &ProverOutcome) -> Verdict { } } +/// The ECH-05 levelling policy (see the module docs). `attempts` is the +/// whole arbitration input, `fused` the attempts whose verdict was fused +/// into the winning one, and `blocked` is true when the verdict needs +/// review or rests on a retracted backend. Returns the level and, at +/// `Sound`, the shared term hash. +/// +/// Mirrors `level` in `src/abi/EchidnaABI/Arbitration.idr` (by review; no +/// test ties the two). +pub fn fidelity_level( + attempts: &[ProverAttempt], + fused: &[&ProverAttempt], + blocked: bool, +) -> (EpistemicLevel, Option) { + if blocked + || fused.is_empty() + || attempts + .iter() + .any(|a| a.fidelity == FidelityEvidence::None) + { + return (EpistemicLevel::Belief, None); + } + + let mut term: Option<&str> = None; + let mut all_kernel = true; + for a in fused { + match &a.fidelity { + FidelityEvidence::KernelTranslation { term_hash, .. } => { + if term_hash.is_empty() || term.is_some_and(|t| t != term_hash) { + return (EpistemicLevel::Belief, None); + } + term = Some(term_hash); + }, + FidelityEvidence::DeclaredCorrespondence { + consequence_tests, + failures, + } => { + if *consequence_tests == 0 || *failures > 0 { + return (EpistemicLevel::Belief, None); + } + all_kernel = false; + }, + FidelityEvidence::None => return (EpistemicLevel::Belief, None), + } + } + + if all_kernel { + (EpistemicLevel::Sound, term.map(str::to_owned)) + } else { + (EpistemicLevel::Epi, None) + } +} + /// Policy-driven result arbiter. Construct once per dispatch with the /// configured policy and the per-prover timeout (used by the /// Dempster-Shafer mass helpers to discount near-timeout verdicts). @@ -142,11 +287,31 @@ pub fn outcome_to_verdict(outcome: &ProverOutcome) -> Verdict { pub struct ResultArbiter { policy: ArbitrationPolicy, timeout_ms: u64, + retracted: Vec, } impl ResultArbiter { pub fn new(policy: ArbitrationPolicy, timeout_ms: u64) -> Self { - Self { policy, timeout_ms } + Self { + policy, + timeout_ms, + retracted: Vec::new(), + } + } + + /// Mark `prover` unsound. Every later verdict that fuses one of its + /// attempts drops to `Belief`; verdicts that do not rest on it keep + /// their level. The numeric fusion still counts its vote — drop the + /// attempt and re-arbitrate to fuse without it. + pub fn retract(&mut self, prover: ProverKind) { + if !self.retracted.contains(&prover) { + self.retracted.push(prover); + } + } + + /// Backends marked unsound via [`Self::retract`]. + pub fn retracted(&self) -> &[ProverKind] { + &self.retracted } /// Arbitrate a set of attempts on the same goal into one verdict. @@ -307,6 +472,25 @@ impl ResultArbiter { .recommended .map(|o| o.prover); + // Fidelity level over the fused attempts — the ones whose + // conclusive verdict is the winning one. + let needs_review = policy_needs_review || suspect_premises; + let fused: Vec<&ProverAttempt> = attempts + .iter() + .filter(|a| { + matches!(verdict, Verdict::Proven | Verdict::Refuted) + && outcome_to_verdict(&a.outcome) == verdict + }) + .collect(); + let mut retracted: Vec = Vec::new(); + for a in &fused { + if self.retracted.contains(&a.prover) && !retracted.contains(&a.prover) { + retracted.push(a.prover); + } + } + let (level, warranted_term) = + fidelity_level(attempts, &fused, needs_review || !retracted.is_empty()); + ArbitratedVerdict { verdict, verified, @@ -314,13 +498,16 @@ impl ResultArbiter { agreeing, disagreeing, inconclusive, - needs_review: policy_needs_review || suspect_premises, + needs_review, conflict, suspect_premises, posterior, belief, recommended, policy: self.policy, + level, + retracted, + warranted_term, } } } @@ -478,4 +665,148 @@ mod tests { assert_eq!(back.verified, v.verified); assert_eq!(back.needs_review, v.needs_review); } + + // --- ECH-05 fidelity level ------------------------------------------- + + fn kernel(term_hash: &str) -> FidelityEvidence { + FidelityEvidence::KernelTranslation { + format: ExchangeFormat::Dedukti, + checked_by: ProverKind::Dedukti, + term_hash: term_hash.into(), + } + } + + fn correspondence(consequence_tests: u32, failures: u32) -> FidelityEvidence { + FidelityEvidence::DeclaredCorrespondence { + consequence_tests, + failures, + } + } + + fn level_of(attempts: &[ProverAttempt]) -> ArbitratedVerdict { + arbiter(ArbitrationPolicy::Portfolio).arbitrate(attempts) + } + + #[test] + fn no_fidelity_evidence_is_belief() { + let v = level_of(&[proved(ProverKind::Z3, 100), proved(ProverKind::CVC5, 200)]); + assert_eq!(v.confidence, PortfolioConfidence::CrossChecked); + assert_eq!(v.level, EpistemicLevel::Belief); + assert_eq!(v.warranted_term, None); + } + + #[test] + fn kernel_translations_to_one_term_are_sound() { + let v = level_of(&[ + proved(ProverKind::Lean, 900).with_fidelity(kernel("h1")), + proved(ProverKind::Isabelle, 1_200).with_fidelity(kernel("h1")), + ]); + assert_eq!(v.level, EpistemicLevel::Sound); + assert_eq!(v.warranted_term.as_deref(), Some("h1")); + } + + #[test] + fn kernel_translations_to_different_terms_are_belief() { + let v = level_of(&[ + proved(ProverKind::Lean, 900).with_fidelity(kernel("h1")), + proved(ProverKind::Isabelle, 1_200).with_fidelity(kernel("h2")), + ]); + assert_eq!(v.verified, Some(true), "numeric fusion is untouched"); + assert_eq!(v.level, EpistemicLevel::Belief); + } + + #[test] + fn empty_term_hash_is_not_a_certificate() { + let v = level_of(&[ + proved(ProverKind::Lean, 900).with_fidelity(kernel("")), + proved(ProverKind::Isabelle, 1_200).with_fidelity(kernel("")), + ]); + assert_eq!(v.level, EpistemicLevel::Belief); + } + + #[test] + fn tested_correspondence_without_failures_is_epi() { + let v = level_of(&[ + proved(ProverKind::Lean, 900).with_fidelity(kernel("h1")), + proved(ProverKind::Coq, 1_100).with_fidelity(correspondence(12, 0)), + ]); + assert_eq!(v.level, EpistemicLevel::Epi); + assert_eq!(v.warranted_term, None); + } + + #[test] + fn failed_or_untested_correspondence_is_belief() { + for evidence in [correspondence(12, 1), correspondence(0, 0)] { + let v = level_of(&[ + proved(ProverKind::Lean, 900).with_fidelity(correspondence(12, 0)), + proved(ProverKind::Coq, 1_100).with_fidelity(evidence), + ]); + assert_eq!(v.level, EpistemicLevel::Belief); + } + } + + #[test] + fn any_attempt_without_evidence_caps_at_belief() { + // The timed-out attempt is not fused, but it carries no evidence. + let v = level_of(&[ + proved(ProverKind::Lean, 900).with_fidelity(kernel("h1")), + proved(ProverKind::Isabelle, 1_200).with_fidelity(kernel("h1")), + timeout(ProverKind::Vampire), + ]); + assert_eq!(v.verified, Some(true)); + assert_eq!(v.level, EpistemicLevel::Belief); + } + + #[test] + fn a_verdict_needing_review_is_belief() { + let v = arbiter(ArbitrationPolicy::Bayesian { prior_p_true: 0.5 }).arbitrate(&[ + proved(ProverKind::Lean, 900).with_fidelity(kernel("h1")), + no_proof(ProverKind::Coq, 200).with_fidelity(kernel("h1")), + ]); + assert!(v.needs_review); + assert_eq!(v.level, EpistemicLevel::Belief); + } + + #[test] + fn retracting_a_fused_backend_lowers_the_level() { + let attempts = [ + proved(ProverKind::Lean, 900).with_fidelity(kernel("h1")), + proved(ProverKind::Isabelle, 1_200).with_fidelity(kernel("h1")), + ]; + let mut a = arbiter(ArbitrationPolicy::Portfolio); + assert_eq!(a.arbitrate(&attempts).level, EpistemicLevel::Sound); + + a.retract(ProverKind::Lean); + a.retract(ProverKind::Lean); + assert_eq!(a.retracted(), &[ProverKind::Lean]); + let v = a.arbitrate(&attempts); + assert_eq!(v.level, EpistemicLevel::Belief); + assert_eq!(v.retracted, vec![ProverKind::Lean]); + assert_eq!(v.verified, Some(true), "numeric fusion is untouched"); + } + + #[test] + fn levels_are_ordered() { + assert!(EpistemicLevel::Belief < EpistemicLevel::Epi); + assert!(EpistemicLevel::Epi < EpistemicLevel::Sound); + } + + #[test] + fn pre_ech05_json_reads_back_at_belief() { + let attempt: ProverAttempt = serde_json::from_str( + r#"{"prover":"Z3","outcome":{"status":"PROVED","elapsed_ms":5},"elapsed_ms":5}"#, + ) + .unwrap(); + assert_eq!(attempt.fidelity, FidelityEvidence::None); + + let v = level_of(&[proved(ProverKind::Z3, 100)]); + let mut json = serde_json::to_value(&v).unwrap(); + let obj = json.as_object_mut().unwrap(); + for k in ["level", "retracted", "warranted_term"] { + obj.remove(k); + } + let back: ArbitratedVerdict = serde_json::from_value(json).unwrap(); + assert_eq!(back.level, EpistemicLevel::Belief); + assert!(back.retracted.is_empty()); + } } diff --git a/tests/abi/accept/ArbitrationAligned.idr b/tests/abi/accept/ArbitrationAligned.idr new file mode 100644 index 00000000..cfe079f8 --- /dev/null +++ b/tests/abi/accept/ArbitrationAligned.idr @@ -0,0 +1,20 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell + +||| Accept fixture (positive control for ../reject/ArbitrationCollision.idr): +||| two kernel translations of one term can be typed Sound. The reject +||| fixture is this file with the second hash changed. +module ArbitrationAligned + +import EchidnaABI.Arbitration +import Data.List +import Data.List.Quantifiers + +%default total + +fusedPair : List (Fidelity Bool) +fusedPair = [ KernelTranslation Dedukti "lean4" True + , KernelTranslation Dedukti "metamath" True ] + +verdict : Level ArbitrationAligned.fusedPair +verdict = Sound True IsNonEmpty [MkKernelAt Refl, MkKernelAt Refl] diff --git a/tests/abi/reject/ArbitrationCollision.idr b/tests/abi/reject/ArbitrationCollision.idr new file mode 100644 index 00000000..a5b9d123 --- /dev/null +++ b/tests/abi/reject/ArbitrationCollision.idr @@ -0,0 +1,21 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell + +||| Reject fixture: a synonym collision (two kernel translations of +||| different terms) must not type-check as Sound. Identical to +||| ../accept/ArbitrationAligned.idr except for the second hash: no single +||| `h` satisfies both `MkKernelAt Refl` proofs, so `Sound` is refused. +module ArbitrationCollision + +import EchidnaABI.Arbitration +import Data.List +import Data.List.Quantifiers + +%default total + +fusedPair : List (Fidelity Bool) +fusedPair = [ KernelTranslation Dedukti "lean4" True + , KernelTranslation Dedukti "metamath" False ] + +verdict : Level ArbitrationCollision.fusedPair +verdict = Sound True IsNonEmpty [MkKernelAt Refl, MkKernelAt Refl] diff --git a/tests/arbitration_fidelity_test.rs b/tests/arbitration_fidelity_test.rs new file mode 100644 index 00000000..5e3f2240 --- /dev/null +++ b/tests/arbitration_fidelity_test.rs @@ -0,0 +1,220 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! ECH-05 acceptance tests: the arbiter's level is set by fidelity +//! evidence, not by how many backends agree. +//! +//! - A synonym collision (lexically aligned, formally distinct +//! statements) never reaches `sound`, under any policy, even though the +//! numeric fusion still reports a cross-checked proof. +//! - A MiniF2F-aligned pair with kernel-checked translations to one term +//! reaches `sound` (positive control), and a one-token mistranslation +//! of the same pair does not (negative control). +//! - Retracting a backend lowers every verdict that rested on it and +//! leaves the others alone (residual-evidence-types `dependent-holds`). +//! +//! What this does not test: that a `KernelTranslation` certificate can be +//! produced. The exchange-layer terms below are the translation targets, +//! written by hand; no bridge in `src/rust/exchange/` emits them yet +//! (ROADMAP stage 6). The tests check the arbiter's policy given +//! certificates, not the certificates. + +use echidna::exchange::{term_hash, ExchangeFormat}; +use echidna::provers::outcome::ProverOutcome; +use echidna::provers::ProverKind; +use echidna::verification::portfolio::PortfolioConfidence; +use echidna::verification::{ + ArbitratedVerdict, ArbitrationPolicy, EpistemicLevel, FidelityEvidence, ProverAttempt, + ResultArbiter, +}; + +const TIMEOUT_MS: u64 = 300_000; + +/// `mathd_numbertheory_3` from MiniF2F (test split), checked against +/// openai/miniF2F@4e433ff. Lean (`lean/src/test.lean`): +/// `(∑ x in finset.range 10, ((x + 1)^2)) % 10 = 5` +/// Isabelle (`isabelle/test/mathd_numbertheory_3.thy`): +/// `(\ x < 10. ((x + 1)^2)) mod 10 = (5::nat)` +/// Both sum over {0, …, 9}, so both translate to this λΠ term. +const NT3_TERM: &str = "eq nat (mod (sum (range 10) (x : nat => pow (add x 1) 2)) 10) 5"; + +/// The same pair with Isabelle's `x < 10` mistranslated as `x ≤ 10`. +const NT3_OFF_BY_ONE: &str = "eq nat (mod (sum (range_le 10) (x : nat => pow (add x 1) 2)) 10) 5"; + +/// Constructed collision (not a MiniF2F problem): "for every natural +/// number n, 2 divides n(n+1)". A synonym table that aligns Lean's `ℕ` +/// (which contains 0) with set.mm's `NN` (positive integers; `NN0` is the +/// one with 0) lets both backends prove "it", but the Metamath statement +/// says nothing about n = 0. +const NAT_TERM: &str = "forall (n : nat), divides 2 (mul n (add n 1))"; +const NN_TERM: &str = "forall (n : nat), lt 0 n -> divides 2 (mul n (add n 1))"; + +fn proved(prover: ProverKind, ms: u64) -> ProverAttempt { + ProverAttempt::new(prover, ProverOutcome::Proved { elapsed_ms: ms }, ms) +} + +/// A Dedukti translation of `term`, checked by the Dedukti kernel. +fn kernel(term: &str) -> FidelityEvidence { + FidelityEvidence::KernelTranslation { + format: ExchangeFormat::Dedukti, + checked_by: ProverKind::Dedukti, + term_hash: term_hash(ExchangeFormat::Dedukti, term), + } +} + +fn policies() -> [ArbitrationPolicy; 3] { + [ + ArbitrationPolicy::Portfolio, + ArbitrationPolicy::Bayesian { prior_p_true: 0.5 }, + ArbitrationPolicy::DempsterShafer, + ] +} + +fn arbitrate(policy: ArbitrationPolicy, attempts: &[ProverAttempt]) -> ArbitratedVerdict { + ResultArbiter::new(policy, TIMEOUT_MS).arbitrate(attempts) +} + +#[test] +fn synonym_collision_cannot_reach_sound() { + let lean = || proved(ProverKind::Lean, 1_400); + let metamath = || proved(ProverKind::Metamath, 300); + + let variants: [(&str, Vec); 4] = [ + ("lexical alignment only", vec![lean(), metamath()]), + ( + "kernel translations to different terms", + vec![ + lean().with_fidelity(kernel(NAT_TERM)), + metamath().with_fidelity(kernel(NN_TERM)), + ], + ), + ( + // Consequence testing instantiates the source claim at n = 0; + // the Metamath statement does not entail that instance. + "declared correspondence with a failed consequence test", + vec![ + lean().with_fidelity(kernel(NAT_TERM)), + metamath().with_fidelity(FidelityEvidence::DeclaredCorrespondence { + consequence_tests: 8, + failures: 1, + }), + ], + ), + ( + "declared correspondence that was never tested", + vec![ + lean().with_fidelity(kernel(NAT_TERM)), + metamath().with_fidelity(FidelityEvidence::DeclaredCorrespondence { + consequence_tests: 0, + failures: 0, + }), + ], + ), + ]; + + for policy in policies() { + for (label, attempts) in &variants { + let v = arbitrate(policy, attempts); + // The numbers still say "both proved it" ... + assert_eq!(v.verified, Some(true), "{label} / {policy:?}"); + assert_eq!(v.confidence, PortfolioConfidence::CrossChecked); + // ... and the level says that is belief, not a warrant. + assert_eq!(v.level, EpistemicLevel::Belief, "{label} / {policy:?}"); + assert_eq!(v.warranted_term, None); + } + } +} + +#[test] +fn minif2f_aligned_pair_reaches_sound() { + let attempts = [ + proved(ProverKind::Lean, 2_100).with_fidelity(kernel(NT3_TERM)), + proved(ProverKind::Isabelle, 3_300).with_fidelity(kernel(NT3_TERM)), + ]; + for policy in policies() { + let v = arbitrate(policy, &attempts); + assert_eq!(v.verified, Some(true), "{policy:?}"); + assert!(!v.needs_review, "{policy:?}"); + assert_eq!(v.level, EpistemicLevel::Sound, "{policy:?}"); + assert_eq!( + v.warranted_term.as_deref(), + Some(term_hash(ExchangeFormat::Dedukti, NT3_TERM).as_str()) + ); + } +} + +#[test] +fn minif2f_mistranslated_pair_does_not_reach_sound() { + let attempts = [ + proved(ProverKind::Lean, 2_100).with_fidelity(kernel(NT3_TERM)), + proved(ProverKind::Isabelle, 3_300).with_fidelity(kernel(NT3_OFF_BY_ONE)), + ]; + for policy in policies() { + let v = arbitrate(policy, &attempts); + assert_eq!(v.verified, Some(true), "{policy:?}"); + assert_eq!(v.level, EpistemicLevel::Belief, "{policy:?}"); + } +} + +#[test] +fn retracted_backend_lowers_every_dependent_verdict() { + const TERM_B: &str = "forall (a b : nat), eq nat (add a b) (add b a)"; + const TERM_C: &str = "forall (n : nat), le n (mul n n)"; + let goals: [(&str, Vec); 3] = [ + ( + "A (Lean + Isabelle)", + vec![ + proved(ProverKind::Lean, 2_100).with_fidelity(kernel(NT3_TERM)), + proved(ProverKind::Isabelle, 3_300).with_fidelity(kernel(NT3_TERM)), + ], + ), + ( + "B (Lean + Coq)", + vec![ + proved(ProverKind::Lean, 900).with_fidelity(kernel(TERM_B)), + proved(ProverKind::Coq, 1_200).with_fidelity(kernel(TERM_B)), + ], + ), + ( + "C (Isabelle + HOL Light)", + vec![ + proved(ProverKind::Isabelle, 1_000).with_fidelity(kernel(TERM_C)), + proved(ProverKind::HOLLight, 1_800).with_fidelity(kernel(TERM_C)), + ], + ), + ]; + + for policy in policies() { + let mut arbiter = ResultArbiter::new(policy, TIMEOUT_MS); + let before: Vec = + goals.iter().map(|(_, a)| arbiter.arbitrate(a)).collect(); + for (v, (label, _)) in before.iter().zip(&goals) { + assert_eq!(v.level, EpistemicLevel::Sound, "{label} / {policy:?}"); + } + + arbiter.retract(ProverKind::Lean); + let after: Vec = + goals.iter().map(|(_, a)| arbiter.arbitrate(a)).collect(); + + for ((b, a), (label, _)) in before.iter().zip(&after).zip(&goals) { + // Numeric fusion is untouched by retraction. + assert_eq!(a.verified, b.verified, "{label} / {policy:?}"); + assert_eq!(a.confidence, b.confidence, "{label} / {policy:?}"); + assert_eq!(a.conflict, b.conflict, "{label} / {policy:?}"); + } + // A and B rested on Lean: lowered, and say why. + for (v, (label, _)) in after.iter().zip(&goals).take(2) { + assert_eq!(v.level, EpistemicLevel::Belief, "{label} / {policy:?}"); + assert_eq!(v.retracted, vec![ProverKind::Lean], "{label}"); + } + // C did not: it keeps its level (negative control). + assert_eq!(after[2].level, EpistemicLevel::Sound, "C / {policy:?}"); + assert!(after[2].retracted.is_empty()); + + // Dropping the retracted attempt and re-arbitrating fuses without it. + let a_without_lean = [goals[0].1[1].clone()]; + let v = arbiter.arbitrate(&a_without_lean); + assert_eq!(v.confidence, PortfolioConfidence::SingleSolver); + assert_eq!(v.level, EpistemicLevel::Sound, "{policy:?}"); + } +} diff --git a/tests/arbitration_regression_test.rs b/tests/arbitration_regression_test.rs new file mode 100644 index 00000000..167fd908 --- /dev/null +++ b/tests/arbitration_regression_test.rs @@ -0,0 +1,302 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! Regression fixture for `ResultArbiter` numeric fusion (ECH-05, PR A). +//! +//! ECH-05 adds a fidelity level (`belief` / `epi` / `sound`) on top of +//! the arbiter's numeric fusion and requires that fusion to be unchanged +//! below the level. This file replays a fixed scenario set under every +//! policy and compares each `ArbitratedVerdict` field by field with +//! `tests/fixtures/arbitration_regression.json`. +//! +//! The fixture was produced by `regenerate_arbitration_fixture` at the +//! pre-ECH-05 commit `29b18ea`, so it records the numbers the arbiter gave +//! before `FidelityEvidence` existed. Every field the fixture holds must +//! match (floats to 1e-12); the only fields allowed beyond the fixture are +//! the ECH-05 additions, and every replayed verdict must sit at level +//! `belief` — the attempts carry no fidelity evidence. +//! +//! Regenerate only at a commit whose numbers are the intended reference: +//! +//! ```sh +//! cargo test --test arbitration_regression_test -- --ignored regenerate +//! ``` + +use echidna::provers::outcome::ProverOutcome; +use echidna::provers::ProverKind; +use echidna::verification::{ArbitrationPolicy, ProverAttempt, ResultArbiter}; +use serde_json::{json, Value}; + +const FIXTURE: &str = concat!( + env!("CARGO_MANIFEST_DIR"), + "/tests/fixtures/arbitration_regression.json" +); + +/// Fields ECH-05 adds to `ArbitratedVerdict`; absent from the fixture. +const ECH05_FIELDS: &[&str] = &["level", "retracted", "warranted_term"]; + +const TOLERANCE: f64 = 1e-12; + +fn proved(p: ProverKind, ms: u64) -> ProverAttempt { + ProverAttempt::new(p, ProverOutcome::Proved { elapsed_ms: ms }, ms) +} + +fn no_proof(p: ProverKind, ms: u64) -> ProverAttempt { + ProverAttempt::new( + p, + ProverOutcome::NoProofFound { + elapsed_ms: ms, + reason: None, + }, + ms, + ) +} + +fn timeout(p: ProverKind) -> ProverAttempt { + ProverAttempt::new(p, ProverOutcome::Timeout { limit_secs: 300 }, 300_000) +} + +fn inconsistent(p: ProverKind, ms: u64) -> ProverAttempt { + ProverAttempt::new(p, ProverOutcome::InconsistentPremises { detail: None }, ms) +} + +fn prover_error(p: ProverKind) -> ProverAttempt { + ProverAttempt::new( + p, + ProverOutcome::ProverError { + detail: "internal assertion".into(), + exit_code: Some(2), + }, + 40, + ) +} + +fn system_error(p: ProverKind) -> ProverAttempt { + ProverAttempt::new( + p, + ProverOutcome::SystemError { + detail: "binary not found".into(), + }, + 1, + ) +} + +fn invalid(p: ProverKind) -> ProverAttempt { + ProverAttempt::new( + p, + ProverOutcome::InvalidInput { + reason: "parse error".into(), + location: Some(3), + }, + 5, + ) +} + +fn unsupported(p: ProverKind) -> ProverAttempt { + ProverAttempt::new( + p, + ProverOutcome::UnsupportedFeature { + feature: "higher-order".into(), + }, + 5, + ) +} + +/// `(name, per-prover timeout in ms, attempts)`. +fn scenarios() -> Vec<(&'static str, u64, Vec)> { + use ProverKind::*; + vec![ + ( + "unanimous_proven_three", + 300_000, + vec![proved(Z3, 100), proved(CVC5, 200), proved(Vampire, 400)], + ), + ( + "proven_vs_refuted", + 300_000, + vec![proved(Z3, 100), no_proof(CVC5, 200)], + ), + ( + "proven_with_timeout", + 300_000, + vec![proved(Z3, 100), proved(CVC5, 200), timeout(Vampire)], + ), + ("all_timed_out", 300_000, vec![timeout(Z3), timeout(CVC5)]), + ( + "inconsistent_premises", + 300_000, + vec![proved(Z3, 100), inconsistent(CVC5, 50)], + ), + ("empty", 300_000, vec![]), + ( + "two_vs_two_fast", + 300_000, + vec![ + proved(Z3, 100), + no_proof(Coq, 100), + proved(Lean, 100), + no_proof(Agda, 100), + ], + ), + ( + "two_proven_fast", + 300_000, + vec![proved(Z3, 100), proved(CVC5, 200)], + ), + ( + "pareto_three", + 300_000, + vec![proved(Vampire, 5_000), proved(Z3, 120), proved(CVC5, 900)], + ), + ( + "unanimous_refuted", + 300_000, + vec![no_proof(Z3, 50), no_proof(CVC5, 70)], + ), + ( + "errors_mixed", + 300_000, + vec![ + proved(Lean, 1_500), + prover_error(Coq), + system_error(Isabelle), + invalid(Agda), + unsupported(Z3), + ], + ), + ( + "interactive_majority", + 300_000, + vec![ + proved(Lean, 2_000), + proved(Isabelle, 3_000), + proved(Coq, 2_500), + no_proof(Z3, 40), + ], + ), + ( + "near_timeout", + 300_000, + vec![proved(Z3, 290_000), proved(CVC5, 299_000)], + ), + ( + "short_budget", + 10_000, + vec![proved(Z3, 9_000), no_proof(Vampire, 500)], + ), + ("single_proved", 300_000, vec![proved(Lean, 800)]), + ("single_refuted", 300_000, vec![no_proof(Coq, 900)]), + ] +} + +fn policies() -> Vec { + vec![ + ArbitrationPolicy::Portfolio, + ArbitrationPolicy::Bayesian { prior_p_true: 0.5 }, + ArbitrationPolicy::Bayesian { prior_p_true: 0.9 }, + ArbitrationPolicy::DempsterShafer, + ] +} + +/// One `(scenario, policy, verdict)` record per scenario × policy. +fn replay() -> Vec { + let mut cases = Vec::new(); + for (name, timeout_ms, attempts) in scenarios() { + for policy in policies() { + let verdict = ResultArbiter::new(policy, timeout_ms).arbitrate(&attempts); + cases.push(json!({ + "scenario": name, + "policy": serde_json::to_value(policy).unwrap(), + "verdict": serde_json::to_value(&verdict).unwrap(), + })); + } + } + cases +} + +/// Recursive comparison: objects by the expected side's keys, floats to +/// `TOLERANCE`, everything else exactly. Returns the first mismatch path. +fn close(expected: &Value, actual: &Value, path: &str) -> Result<(), String> { + match (expected, actual) { + (Value::Object(e), Value::Object(a)) => { + for (k, ev) in e { + let av = a + .get(k) + .ok_or_else(|| format!("{path}.{k}: missing in actual"))?; + close(ev, av, &format!("{path}.{k}"))?; + } + Ok(()) + }, + (Value::Array(e), Value::Array(a)) => { + if e.len() != a.len() { + return Err(format!("{path}: length {} != {}", e.len(), a.len())); + } + for (i, (ev, av)) in e.iter().zip(a).enumerate() { + close(ev, av, &format!("{path}[{i}]"))?; + } + Ok(()) + }, + (Value::Number(e), Value::Number(a)) => { + let (e, a) = (e.as_f64().unwrap(), a.as_f64().unwrap()); + if (e - a).abs() <= TOLERANCE * e.abs().max(1.0) { + Ok(()) + } else { + Err(format!("{path}: {e} != {a}")) + } + }, + (e, a) if e == a => Ok(()), + (e, a) => Err(format!("{path}: {e} != {a}")), + } +} + +#[test] +fn numeric_fusion_unchanged_and_level_is_belief() { + let raw = std::fs::read_to_string(FIXTURE).expect("fixture present"); + let fixture: Value = serde_json::from_str(&raw).expect("fixture is JSON"); + let expected = fixture["cases"].as_array().expect("cases array"); + let actual = replay(); + assert_eq!( + expected.len(), + actual.len(), + "scenario × policy set changed; the fixture no longer covers it" + ); + + for (e, a) in expected.iter().zip(&actual) { + assert_eq!(e["scenario"], a["scenario"]); + assert_eq!(e["policy"], a["policy"]); + let label = format!("{} / {}", e["scenario"], e["policy"]); + if let Err(diff) = close(&e["verdict"], &a["verdict"], "verdict") { + panic!("{label}: numeric fusion changed at {diff}"); + } + + let ev = e["verdict"].as_object().unwrap(); + let av = a["verdict"].as_object().unwrap(); + for k in av.keys() { + assert!( + ev.contains_key(k) || ECH05_FIELDS.contains(&k.as_str()), + "{label}: undocumented new field `{k}`" + ); + } + assert_eq!( + av.get("level"), + Some(&json!("belief")), + "{label}: no fidelity evidence, so the level must be belief" + ); + } +} + +/// Writes the fixture from the current arbiter. Ignored: run it only at a +/// commit whose numbers are the intended reference (see module docs). +#[test] +#[ignore] +fn regenerate_arbitration_fixture() { + let doc = json!({ + "provenance": "ResultArbiter numeric fusion at echidna 29b18ea (pre-ECH-05); \ + produced by tests/arbitration_regression_test.rs::regenerate_arbitration_fixture", + "tolerance": TOLERANCE, + "cases": replay(), + }); + let mut out = serde_json::to_string_pretty(&doc).unwrap(); + out.push('\n'); + std::fs::write(FIXTURE, out).expect("write fixture"); +} diff --git a/tests/fixtures/arbitration_regression.json b/tests/fixtures/arbitration_regression.json new file mode 100644 index 00000000..4ba86857 --- /dev/null +++ b/tests/fixtures/arbitration_regression.json @@ -0,0 +1,2052 @@ +{ + "cases": [ + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "unanimous_proven_three", + "verdict": { + "agreeing": [ + "Z3", + "CVC5", + "Vampire" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "unanimous_proven_three", + "verdict": { + "agreeing": [ + "Z3", + "CVC5", + "Vampire" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.00567268512118722, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.008990993195480591, + "p_proven": 0.9992380634907406, + "p_refuted": 0.0007619365092593755, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "unanimous_proven_three", + "verdict": { + "agreeing": [ + "Z3", + "CVC5", + "Vampire" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.0008001333747528126, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.0012681813945586758, + "p_proven": 0.9999152830110007, + "p_refuted": 0.00008471698899925606, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "unanimous_proven_three", + "verdict": { + "agreeing": [ + "Z3", + "CVC5", + "Vampire" + ], + "belief": { + "belief_proven": 0.999872359223, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 0.00012764077700000033 + }, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "proven_vs_refuted", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.5, + "disagreeing": [ + "Z3", + "CVC5" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "proven_vs_refuted", + "verdict": { + "agreeing": [ + "CVC5" + ], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.6096223209092397, + "disagreeing": [ + "Z3" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.9662285182437437, + "p_proven": 0.39223781998348506, + "p_refuted": 0.6077621800165149, + "p_unknown": 0.0, + "winning": "Refuted" + }, + "recommended": "CVC5", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "proven_vs_refuted", + "verdict": { + "agreeing": [ + "Z3" + ], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.3798002601162462, + "disagreeing": [ + "CVC5" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.6019691700483911, + "p_proven": 0.8531231291159451, + "p_refuted": 0.14687687088405488, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "proven_vs_refuted", + "verdict": { + "agreeing": [], + "belief": { + "belief_proven": 0.48788621127752185, + "belief_refuted": 0.4863544651497379, + "conflict_k": 0.902072545, + "plausibility_proven": 0.5136455348502625, + "plausibility_refuted": 0.5121137887224786 + }, + "confidence": "Inconclusive", + "conflict": 0.902072545, + "disagreeing": [ + "Z3", + "CVC5" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "proven_with_timeout", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [ + "Vampire" + ], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "proven_with_timeout", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.6048145266621299, + "disagreeing": [], + "inconclusive": [ + "Vampire" + ], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.9586083446508917, + "p_proven": 0.661972347526314, + "p_refuted": 0.004694319140352788, + "p_unknown": 0.3333333333333333, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "proven_with_timeout", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.5832722550928507, + "disagreeing": [], + "inconclusive": [ + "Vampire" + ], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.9244646520332328, + "p_proven": 0.6661417904021455, + "p_refuted": 0.0005248762645212087, + "p_unknown": 0.3333333333333333, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "proven_with_timeout", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": { + "belief_proven": 0.997477455, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 0.002522545000000002 + }, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [ + "Vampire" + ], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "all_timed_out", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "AllTimedOut", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [ + "Z3", + "CVC5" + ], + "needs_review": true, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Timeout", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "all_timed_out", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "AllTimedOut", + "conflict": 0.9463946303571862, + "disagreeing": [], + "inconclusive": [ + "Z3", + "CVC5" + ], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 1.5, + "p_proven": 0.25, + "p_refuted": 0.25, + "p_unknown": 0.5, + "winning": "Unknown" + }, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "all_timed_out", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "AllTimedOut", + "conflict": 0.7788813907161498, + "disagreeing": [], + "inconclusive": [ + "Z3", + "CVC5" + ], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 1.2344977967946407, + "p_proven": 0.44999999999999996, + "p_refuted": 0.050000000000000044, + "p_unknown": 0.5, + "winning": "Unknown" + }, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "all_timed_out", + "verdict": { + "agreeing": [], + "belief": { + "belief_proven": 0.0, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 1.0 + }, + "confidence": "AllTimedOut", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [ + "Z3", + "CVC5" + ], + "needs_review": true, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "inconsistent_premises", + "verdict": { + "agreeing": [ + "Z3" + ], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [ + "CVC5" + ], + "needs_review": true, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": true, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "inconsistent_premises", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.7551961816996249, + "disagreeing": [ + "Z3" + ], + "inconclusive": [ + "CVC5" + ], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 1.196957628681706, + "p_proven": 0.4611650485436893, + "p_refuted": 0.03883495145631072, + "p_unknown": 0.5, + "winning": "Unknown" + }, + "recommended": null, + "suspect_premises": true, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "inconsistent_premises", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.6548778998293792, + "disagreeing": [ + "Z3" + ], + "inconclusive": [ + "CVC5" + ], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 1.0379569137805915, + "p_proven": 0.49536500579374276, + "p_refuted": 0.004634994206257237, + "p_unknown": 0.5, + "winning": "Unknown" + }, + "recommended": null, + "suspect_premises": true, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "inconsistent_premises", + "verdict": { + "agreeing": [ + "Z3" + ], + "belief": { + "belief_proven": 0.94985, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 0.05015000000000003 + }, + "confidence": "SingleSolver", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [ + "CVC5" + ], + "needs_review": true, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": true, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "empty", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "AllTimedOut", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Timeout", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "empty", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "AllTimedOut", + "conflict": 0.6309297535714575, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 1.0, + "p_proven": 0.5, + "p_refuted": 0.5, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": null, + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "empty", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "AllTimedOut", + "conflict": 0.29590327428938484, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.46899559358928156, + "p_proven": 0.8999999999999999, + "p_refuted": 0.10000000000000009, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": null, + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "empty", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "AllTimedOut", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "two_vs_two_fast", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.5, + "disagreeing": [ + "Z3", + "Coq", + "Lean", + "Agda" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "two_vs_two_fast", + "verdict": { + "agreeing": [ + "Coq", + "Agda" + ], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.2827090405532507, + "disagreeing": [ + "Z3", + "Lean" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.4480832278917589, + "p_proven": 0.09351145038167956, + "p_refuted": 0.9064885496183205, + "p_unknown": 0.0, + "winning": "Refuted" + }, + "recommended": "Coq", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "two_vs_two_fast", + "verdict": { + "agreeing": [ + "Coq", + "Agda" + ], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.6303025735637556, + "disagreeing": [ + "Z3", + "Lean" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.9990059432065905, + "p_proven": 0.48144104803493515, + "p_refuted": 0.5185589519650649, + "p_unknown": 0.0, + "winning": "Refuted" + }, + "recommended": "Coq", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "two_vs_two_fast", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.9949762803381755, + "disagreeing": [ + "Z3", + "Coq", + "Lean", + "Agda" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "two_proven_fast", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "two_proven_fast", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.03815154356465222, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.0604687658946033, + "p_proven": 0.9929585212894708, + "p_refuted": 0.007041478710529181, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "two_proven_fast", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.005838136210733476, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.009253226968114864, + "p_proven": 0.9992126856032182, + "p_refuted": 0.000787314396781813, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "two_proven_fast", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": { + "belief_proven": 0.997477455, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 0.002522545000000002 + }, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "pareto_three", + "verdict": { + "agreeing": [ + "Vampire", + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "pareto_three", + "verdict": { + "agreeing": [ + "Vampire", + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.00567268512118722, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.008990993195480591, + "p_proven": 0.9992380634907406, + "p_refuted": 0.0007619365092593755, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "pareto_three", + "verdict": { + "agreeing": [ + "Vampire", + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.0008001333747528126, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.0012681813945586758, + "p_proven": 0.9999152830110007, + "p_refuted": 0.00008471698899925606, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "pareto_three", + "verdict": { + "agreeing": [ + "Vampire", + "Z3", + "CVC5" + ], + "belief": { + "belief_proven": 0.9998518372775, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 0.00014816272250000004 + }, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "unanimous_refuted", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "unanimous_refuted", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.018298544642544233, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.029002507076204623, + "p_proven": 0.0029449876310519547, + "p_refuted": 0.997055012368948, + "p_unknown": 0.0, + "winning": "Refuted" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "unanimous_refuted", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.10938235767326467, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.1733669351525935, + "p_proven": 0.025894809529289953, + "p_refuted": 0.9741051904707101, + "p_unknown": 0.0, + "winning": "Refuted" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "unanimous_refuted", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": { + "belief_proven": 0.0, + "belief_refuted": 0.997490992125, + "conflict_k": 0.0, + "plausibility_proven": 0.002509007875000008, + "plausibility_refuted": 1.0 + }, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "errors_mixed", + "verdict": { + "agreeing": [ + "Lean" + ], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [ + "Coq", + "Isabelle", + "Agda", + "Z3" + ], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "errors_mixed", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.7193161180738602, + "disagreeing": [ + "Lean" + ], + "inconclusive": [ + "Coq", + "Isabelle", + "Agda", + "Z3" + ], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 1.1400890733113798, + "p_proven": 0.47572815533980584, + "p_refuted": 0.024271844660194164, + "p_unknown": 0.5, + "winning": "Unknown" + }, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "errors_mixed", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.6467732094321391, + "disagreeing": [ + "Lean" + ], + "inconclusive": [ + "Coq", + "Isabelle", + "Agda", + "Z3" + ], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 1.0251112834210112, + "p_proven": 0.4971815107102593, + "p_refuted": 0.002818489289740711, + "p_unknown": 0.5, + "winning": "Unknown" + }, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "errors_mixed", + "verdict": { + "agreeing": [ + "Lean" + ], + "belief": { + "belief_proven": 0.94775, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 0.05225000000000002 + }, + "confidence": "SingleSolver", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [ + "Coq", + "Isabelle", + "Agda", + "Z3" + ], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "interactive_majority", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.25, + "disagreeing": [ + "Lean", + "Isabelle", + "Coq", + "Z3" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "interactive_majority", + "verdict": { + "agreeing": [ + "Lean", + "Isabelle", + "Coq" + ], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.015566868104288006, + "disagreeing": [ + "Z3" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.02467290219896872, + "p_proven": 0.9975622474806357, + "p_refuted": 0.002437752519364289, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "interactive_majority", + "verdict": { + "agreeing": [ + "Lean", + "Isabelle", + "Coq" + ], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.002276039190031149, + "disagreeing": [ + "Z3" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.0036074367663711244, + "p_proven": 0.9997285504072452, + "p_refuted": 0.0002714495927548244, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "interactive_majority", + "verdict": { + "agreeing": [ + "Lean", + "Isabelle", + "Coq" + ], + "belief": { + "belief_proven": 0.996907694622053, + "belief_refuted": 0.0029375045707274337, + "conflict_k": 0.9497925152841625, + "plausibility_proven": 0.997062495429273, + "plausibility_refuted": 0.0030923053779474846 + }, + "confidence": "Inconclusive", + "conflict": 0.9497925152841625, + "disagreeing": [ + "Z3" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "near_timeout", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "near_timeout", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.03815154356465222, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.0604687658946033, + "p_proven": 0.9929585212894708, + "p_refuted": 0.007041478710529181, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "near_timeout", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": null, + "confidence": "CrossChecked", + "conflict": 0.005838136210733476, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.009253226968114864, + "p_proven": 0.9992126856032182, + "p_refuted": 0.000787314396781813, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "near_timeout", + "verdict": { + "agreeing": [ + "Z3", + "CVC5" + ], + "belief": { + "belief_proven": 0.7582274999999999, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 0.24177250000000008 + }, + "confidence": "CrossChecked", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "short_budget", + "verdict": { + "agreeing": [], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.5, + "disagreeing": [ + "Z3", + "Vampire" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": null, + "suspect_premises": false, + "verdict": "Unknown", + "verified": null + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "short_budget", + "verdict": { + "agreeing": [ + "Vampire" + ], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.6302118508717413, + "disagreeing": [ + "Z3" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.9988621511417832, + "p_proven": 0.4801444043321299, + "p_refuted": 0.5198555956678701, + "p_unknown": 0.0, + "winning": "Refuted" + }, + "recommended": "Vampire", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "short_budget", + "verdict": { + "agreeing": [ + "Z3" + ], + "belief": null, + "confidence": "Inconclusive", + "conflict": 0.3103985770368175, + "disagreeing": [ + "Vampire" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.4919701048805627, + "p_proven": 0.8926174496644296, + "p_refuted": 0.10738255033557043, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Z3", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "short_budget", + "verdict": { + "agreeing": [ + "Vampire" + ], + "belief": { + "belief_proven": 0.07990192361163771, + "belief_refuted": 0.8533909658502061, + "conflict_k": 0.5054875, + "plausibility_proven": 0.14660903414979398, + "plausibility_refuted": 0.9200980763883624 + }, + "confidence": "Inconclusive", + "conflict": 0.5054875, + "disagreeing": [ + "Z3" + ], + "inconclusive": [], + "needs_review": true, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Vampire", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "single_proved", + "verdict": { + "agreeing": [ + "Lean" + ], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "single_proved", + "verdict": { + "agreeing": [ + "Lean" + ], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.17677272900480556, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.28017814662275986, + "p_proven": 0.9514563106796117, + "p_refuted": 0.04854368932038833, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "single_proved", + "verdict": { + "agreeing": [ + "Lean" + ], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.03168691172136324, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.05022256684202239, + "p_proven": 0.9943630214205186, + "p_refuted": 0.005636978579481422, + "p_unknown": 0.0, + "winning": "Proven" + }, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "single_proved", + "verdict": { + "agreeing": [ + "Lean" + ], + "belief": { + "belief_proven": 0.9488, + "belief_refuted": 0.0, + "conflict_k": 0.0, + "plausibility_proven": 1.0, + "plausibility_refuted": 0.05120000000000002 + }, + "confidence": "SingleSolver", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Lean", + "suspect_premises": false, + "verdict": "Proven", + "verified": true + } + }, + { + "policy": { + "mechanism": "portfolio" + }, + "scenario": "single_refuted", + "verdict": { + "agreeing": [ + "Coq" + ], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "portfolio" + }, + "posterior": null, + "recommended": "Coq", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "scenario": "single_refuted", + "verdict": { + "agreeing": [ + "Coq" + ], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.09142147998276146, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.5 + }, + "posterior": { + "entropy_bits": 0.1448996175331067, + "p_proven": 0.020618556701030945, + "p_refuted": 0.979381443298969, + "p_unknown": 0.0, + "winning": "Refuted" + }, + "recommended": "Coq", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "scenario": "single_refuted", + "verdict": { + "agreeing": [ + "Coq" + ], + "belief": null, + "confidence": "SingleSolver", + "conflict": 0.3991344810884815, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "bayesian", + "prior_p_true": 0.9 + }, + "posterior": { + "entropy_bits": 0.6326131852700406, + "p_proven": 0.15929203539823025, + "p_refuted": 0.8407079646017698, + "p_unknown": 0.0, + "winning": "Refuted" + }, + "recommended": "Coq", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + }, + { + "policy": { + "mechanism": "dempster_shafer" + }, + "scenario": "single_refuted", + "verdict": { + "agreeing": [ + "Coq" + ], + "belief": { + "belief_proven": 0.0, + "belief_refuted": 0.94865, + "conflict_k": 0.0, + "plausibility_proven": 0.05135000000000001, + "plausibility_refuted": 1.0 + }, + "confidence": "SingleSolver", + "conflict": 0.0, + "disagreeing": [], + "inconclusive": [], + "needs_review": false, + "policy": { + "mechanism": "dempster_shafer" + }, + "posterior": null, + "recommended": "Coq", + "suspect_premises": false, + "verdict": "Refuted", + "verified": false + } + } + ], + "provenance": "ResultArbiter numeric fusion at echidna 29b18ea (pre-ECH-05); produced by tests/arbitration_regression_test.rs::regenerate_arbitration_fixture", + "tolerance": 1e-12 +}