From c1f1e109636fabaaaaa6f4ce217dffb6e20aa3f6 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 08:31:48 +0000 Subject: [PATCH 1/4] chore(ech05): regression fixture -> JCS; stage 6 first target; ECH-05 filed as #431 - tests/fixtures/arbitration_regression.json is now JCS (RFC 8785) I-JSON plus a final LF, the estate format standard. Re-serialised, not regenerated: all 327 numbers and the whole document compare equal to the 29b18ea fixture (only spellings like 0.0 -> 0 change). The regenerator writes JCS, and fixture_is_jcs_canonical fails on a pretty-printed fixture (negative control run). - ROADMAP stage 6 and the gap-analysis pair table: HOL4 <-> HOL Light through OpenTheory is the first target (owner decision 2026-10-14); Lean 4 <-> Rocq through Dedukti is the next candidate. - issues/README.md: ECH-05 is #431, closed as completed by #430, the arbiter-typing slice of #429 (open). Its four labels now exist on the repo (created by filing) but not yet in the estate label source. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- docs/ROADMAP.adoc | 7 +- docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc | 2 +- issues/README.md | 8 +- tests/arbitration_regression_test.rs | 20 +- tests/fixtures/arbitration_regression.json | 2053 +---------------- 5 files changed, 29 insertions(+), 2061 deletions(-) diff --git a/docs/ROADMAP.adoc b/docs/ROADMAP.adoc index 691128d8..d2a00f3a 100644 --- a/docs/ROADMAP.adoc +++ b/docs/ROADMAP.adoc @@ -212,9 +212,10 @@ kernel‑checked translation. `+ResultArbiter+` grades each verdict (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+` +pair*, and a verdict on that pair reaches `+sound+`. First target (owner +decision, 2026-10-14): HOL4 ↔ HOL Light through OpenTheory (6a); next +candidate Lean 4 ↔ Rocq through Dedukti (6b). Pair table: +`+docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc+` § "Backend pairs that can share a term" |=== diff --git a/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc b/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc index 3f175714..da95178d 100644 --- a/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc +++ b/docs/design/ADVANCED_TYPING_GAP_ANALYSIS.adoc @@ -244,7 +244,7 @@ certificate for one pair is the ROADMAP stage 6 acceptance. |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 +exports and imports proof states, not checked articles); first target (2026-10-14) |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) diff --git a/issues/README.md b/issues/README.md index 7dba320e..27f55315 100644 --- a/issues/README.md +++ b/issues/README.md @@ -20,7 +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` | +| ECH-05 | hyperpolymath/echidna | #431 | `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` | @@ -30,7 +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. +- **ECH-05** is filed as #431 and closed as completed by #430 (fidelity evidence on `ProverAttempt`, `level` on `ArbitratedVerdict`, `EchidnaABI.Arbitration`, the fidelity tests). It is the arbiter-typing slice of #429, which stays open for one-kernel (Agda) ingestion of fibre coverage, round-trip and cross-prover agreement. - **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 @@ -49,6 +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) | +| hyperpolymath/echidna | none on the repo since #431 created `area:arbitration`, `area:exchange`, `epistemic-types`, `residual-evidence-types` (default colour, no description); they are not yet in the estate label source (`.github/labels.json` is generated from hyperpolymath/.git-private-farm) | -All labels used by ECH-01..04 exist on hyperpolymath/echidna; ECH-05's `enhancement` and `idris2` do. +All labels used by ECH-01..05 exist on hyperpolymath/echidna. diff --git a/tests/arbitration_regression_test.rs b/tests/arbitration_regression_test.rs index 167fd908..8082f999 100644 --- a/tests/arbitration_regression_test.rs +++ b/tests/arbitration_regression_test.rs @@ -16,6 +16,10 @@ //! the ECH-05 additions, and every replayed verdict must sit at level //! `belief` — the attempts carry no fidelity evidence. //! +//! The fixture is JCS (RFC 8785) I-JSON, the estate format standard; +//! `fixture_is_jcs_canonical` keeps it that way. It was re-serialised to +//! JCS after generation without changing any value. +//! //! Regenerate only at a commit whose numbers are the intended reference: //! //! ```sh @@ -296,7 +300,21 @@ fn regenerate_arbitration_fixture() { "tolerance": TOLERANCE, "cases": replay(), }); - let mut out = serde_json::to_string_pretty(&doc).unwrap(); + // Estate format standard: JCS (RFC 8785) I-JSON, plus the final LF + // that .editorconfig requires. + let mut out = serde_json_canonicalizer::to_string(&doc).unwrap(); out.push('\n'); std::fs::write(FIXTURE, out).expect("write fixture"); } + +#[test] +fn fixture_is_jcs_canonical() { + let raw = std::fs::read_to_string(FIXTURE).expect("fixture present"); + let body = raw.strip_suffix('\n').expect("fixture ends with one LF"); + let value: Value = serde_json::from_str(body).expect("fixture is JSON"); + assert_eq!( + body, + serde_json_canonicalizer::to_string(&value).unwrap(), + "fixture must be JCS (RFC 8785) canonical" + ); +} diff --git a/tests/fixtures/arbitration_regression.json b/tests/fixtures/arbitration_regression.json index 4ba86857..b94070b8 100644 --- a/tests/fixtures/arbitration_regression.json +++ b/tests/fixtures/arbitration_regression.json @@ -1,2052 +1 @@ -{ - "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 -} +{"cases":[{"policy":{"mechanism":"portfolio"},"scenario":"unanimous_proven_three","verdict":{"agreeing":["Z3","CVC5","Vampire"],"belief":null,"confidence":"CrossChecked","conflict":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,"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,"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,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":0.00012764077700000033},"confidence":"CrossChecked","conflict":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,"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,"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,"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,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":0.002522545000000002},"confidence":"CrossChecked","conflict":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,"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,"belief_refuted":0,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":1},"confidence":"AllTimedOut","conflict":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,"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,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":0.05015000000000003},"confidence":"SingleSolver","conflict":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,"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,"p_proven":0.5,"p_refuted":0.5,"p_unknown":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,"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,"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,"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,"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,"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,"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,"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,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":0.002522545000000002},"confidence":"CrossChecked","conflict":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,"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,"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,"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,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":0.00014816272250000004},"confidence":"CrossChecked","conflict":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,"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,"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,"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,"belief_refuted":0.997490992125,"conflict_k":0,"plausibility_proven":0.002509007875000008,"plausibility_refuted":1},"confidence":"CrossChecked","conflict":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,"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,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":0.05225000000000002},"confidence":"SingleSolver","conflict":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,"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,"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,"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,"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,"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,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":0.24177250000000008},"confidence":"CrossChecked","conflict":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,"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,"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,"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,"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,"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,"conflict_k":0,"plausibility_proven":1,"plausibility_refuted":0.05120000000000002},"confidence":"SingleSolver","conflict":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,"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,"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,"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,"belief_refuted":0.94865,"conflict_k":0,"plausibility_proven":0.05135000000000001,"plausibility_refuted":1},"confidence":"SingleSolver","conflict":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} From c0ff5b18f6d0a6bca464bc607a49796d06d1d4cc Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 08:45:31 +0000 Subject: [PATCH 2/4] =?UTF-8?q?docs(claude):=20record=20owner=20norms=20?= =?UTF-8?q?=E2=80=94=20selector=20questions,=20stacked=20PRs,=20KYAML=20/?= =?UTF-8?q?=20I-JSON+JCS=20/=20UUID=20v8?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Owner norms of 2026-10-14 for agent sessions in this repo: - decisions are asked with the selector tool, recommended option first; - work lands as stacked, independently reviewable PRs; - findings are fixed at source before any baseline/ledger entry. Format standards point at their normative source in hyperpolymath/standards rather than restating it: YAML-POLICY §3.4 (KYAML, .kyaml, no Python parser; D280/D307/D293), the workflow gate in standards#1025, JSON-POLICY (I-JSON as JCS + LF; D306) and ADR-008 (UUID v8 profiles T and C; D305/D305b/D320). A format is kept only where a consumer the owner does not control would break, with the reason recorded. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- .claude/CLAUDE.md | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 251dad16..0e3c2f3d 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -152,3 +152,31 @@ package definitions (not metadata files) and must NOT be deleted. - SHA-pinned dependencies - SPDX license headers on all files +## Owner norms (2026-10-14) + +These come from the owner. The format rules point at their normative +source in `hyperpolymath/standards`; read that, not a paraphrase. + +### Asking the owner + +- Ask decisions with the selector tool (structured options, the + recommended one first, with what each option implies). Use prose only + for reports and explanations. +- Work lands as **stacked PRs**: small, each independently reviewable. +- Fix a finding at its source before reaching for a baseline or ledger. + The governance exemption ratchet rejects ledger growth. + +### Formats (standard, estate-wide) + +| Kind | Standard | Source | +|------|----------|--------| +| YAML | KYAML, formatted with standards `scripts/kyaml-format.sh` (mikefarah yq v4 with the KYAML encoder). Estate-owned config uses `.kyaml` unless a tool fixes the name. No Python YAML parser. | `3-practice/YAML-POLICY.adoc` §3.4 (D280, D307, D293) | +| Workflows | KYAML too, but only through the step 6 gate in `standards#1025` (Dependabot / `gh actions-lock` drift accepted in writing, lock coverage, `actionlint`, a run proof per workflow). Lockfiles such as `actions.lock` are tool-owned: never hand-edit or reformat them. | `YAML-POLICY.adoc` §5–§6 | +| JSON | I-JSON (RFC 7493) serialised as JCS (RFC 8785), plus exactly one final LF. Extensions do not change. JSONL is one JCS object per line. JSONC files (`devcontainer.json`, `.vscode/`) are exempt. | `3-practice/JSON-POLICY.adoc` (D306) | +| UUID | Version 8 for every identifier. Profile T (time-ordered: the v7 layout with the version nibble set to 8) for records and events. Profile C (bytes 0..15 of SHA-256(`domain:name`), registered `domain`, no `:`) for content ids. No v4/v7 minting in new code. echidna mints only through `src/rust/ids.rs`. | `docs/decisions/ADR-008-uuid-v8-estate-standard.adoc` (D305, D305b, D320) | + +Keep another format only where a consumer the owner does not control +would break (for example a tool that rewrites the file). Record why +beside the file. Tools the owner controls are changed to handle the +standard instead of being exempted. + From 20715829622091b8ee91f4df8756fbfdfe74db84 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 08:56:51 +0000 Subject: [PATCH 3/4] docs(claude): the exemption ratchet admits declared ledger growth scripts/check-exemption-ratchet.sh in standards rejects growth of a ledger unless a commit message or the PR body carries a `Ratchet-exception:` line naming that ledger. The norm said it rejects all growth. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- .claude/CLAUDE.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 0e3c2f3d..1dff8646 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -164,7 +164,8 @@ source in `hyperpolymath/standards`; read that, not a paraphrase. for reports and explanations. - Work lands as **stacked PRs**: small, each independently reviewable. - Fix a finding at its source before reaching for a baseline or ledger. - The governance exemption ratchet rejects ledger growth. + The governance exemption ratchet rejects ledger growth unless a commit + or the PR body carries a `Ratchet-exception:` line naming that ledger. ### Formats (standard, estate-wide) From d53c96b2b51e9c0fdca75a0dac4597c39c1ae276 Mon Sep 17 00:00:00 2001 From: Claude Date: Wed, 14 Oct 2026 08:57:34 +0000 Subject: [PATCH 4/4] docs(claude): scope the UUID v8 rule until the ids.rs migration lands ids.rs still mints records as UUIDv7 and content ids as UUIDv8 over JCS bytes without a profile C domain. Stating profiles T and C as the active rule would have an agent mint ids that break the current contract. This matches the wording the owner accepted on proof-burrower#111. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_019a95kk88TZ1iegsBK3kox3 --- .claude/CLAUDE.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 1dff8646..c5a2b298 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -174,7 +174,7 @@ source in `hyperpolymath/standards`; read that, not a paraphrase. | YAML | KYAML, formatted with standards `scripts/kyaml-format.sh` (mikefarah yq v4 with the KYAML encoder). Estate-owned config uses `.kyaml` unless a tool fixes the name. No Python YAML parser. | `3-practice/YAML-POLICY.adoc` §3.4 (D280, D307, D293) | | Workflows | KYAML too, but only through the step 6 gate in `standards#1025` (Dependabot / `gh actions-lock` drift accepted in writing, lock coverage, `actionlint`, a run proof per workflow). Lockfiles such as `actions.lock` are tool-owned: never hand-edit or reformat them. | `YAML-POLICY.adoc` §5–§6 | | JSON | I-JSON (RFC 7493) serialised as JCS (RFC 8785), plus exactly one final LF. Extensions do not change. JSONL is one JCS object per line. JSONC files (`devcontainer.json`, `.vscode/`) are exempt. | `3-practice/JSON-POLICY.adoc` (D306) | -| UUID | Version 8 for every identifier. Profile T (time-ordered: the v7 layout with the version nibble set to 8) for records and events. Profile C (bytes 0..15 of SHA-256(`domain:name`), registered `domain`, no `:`) for content ids. No v4/v7 minting in new code. echidna mints only through `src/rust/ids.rs`. | `docs/decisions/ADR-008-uuid-v8-estate-standard.adoc` (D305, D305b, D320) | +| UUID | Current policy: UUIDv7 for records and events, and UUIDv8 over JCS content bytes for content IDs. Keep this split until the corresponding `ids.rs` migration lands. Apply the Profile T/C rule and prohibit new v4/v7 minting after that migration. echidna mints only through `src/rust/ids.rs`. | `docs/decisions/ADR-008-uuid-v8-estate-standard.adoc` (D305, D305b, D320) | Keep another format only where a consumer the owner does not control would break (for example a tool that rewrites the file). Record why