chapel: bench_mrr outcome telemetry (#162) + prover-count reconciliation (#251)

.gitignore

@@ -65,6 +65,9 @@ src/chapel/chapel_smoke
 src/chapel/chapel_smoke_real
 src/chapel/bench_mrr
 src/chapel/bench_mrr_real
+# bench_mrr generated CSVs (#162) — regenerated per run, not tracked
+src/chapel/bench_mrr_telemetry.csv
+src/chapel/bench_mrr_summary.csv
 src/chapel/libechidna_chapel.h
 
 # Zig

.machine_readable/policies/MAINTENANCE-AXES.a2ml

@@ -20,7 +20,7 @@ sources = ["README.adoc", "ROADMAP.adoc", "docs/maintenance/MAINTENANCE-CHECKLIS
 
 [axes.axis-1.must]
 items = [
-  "30 prover backends compile and pass smoke tests",
+  "All prover backends compile and pass smoke tests (figure: docs/PROVER_COUNT.adoc)",
   "cargo test --lib passes with zero failures",
   "No believe-me or assert_total in Idris2 source",
   "No unsafe blocks without SAFETY comments",

.machine_readable/provers.a2ml

@@ -19,8 +19,8 @@
 [metadata]
 version = "1.0.0"
 source  = "src/rust/provers/mod.rs::ProverKind"
-date    = "2026-04-24"
-count   = 113
+date    = "2026-09-25"
+count   = 141
 
 [prover.ABC]
 slug = "abc"
@@ -40,12 +40,18 @@ slug = "affine_type_checker"
 [prover.Agda]
 slug = "agda"
 
+[prover.AgsyHOL]
+slug = "agsy_hol"
+
 [prover.Alloy]
 slug = "alloy"
 
 [prover.AltErgo]
 slug = "alt_ergo"
 
+[prover.AProVE]
+slug = "a_pro_ve"
+
 [prover.Arend]
 slug = "arend"
 
@@ -82,6 +88,12 @@ slug = "coeffect_type_checker"
 [prover.Coq]
 slug = "coq"
 
+[prover.CryptoVerif]
+slug = "crypto_verif"
+
+[prover.CSI]
+slug = "csi"
+
 [prover.CubicalAgda]
 slug = "cubical_agda"
 
@@ -106,12 +118,18 @@ slug = "d_real"
 [prover.DyadicTypeChecker]
 slug = "dyadic_type_checker"
 
+[prover.EasyCrypt]
+slug = "easy_crypt"
+
 [prover.EchoTypeChecker]
 slug = "echo_type_checker"
 
 [prover.EffectRowTypeChecker]
 slug = "effect_row_type_checker"
 
+[prover.ELK]
+slug = "elk"
+
 [prover.EpistemicTypeChecker]
 slug = "epistemic_type_checker"
 
@@ -121,6 +139,9 @@ slug = "e_prover"
 [prover.ExistentialTypeChecker]
 slug = "existential_type_checker"
 
+[prover.Faial]
+slug = "faial"
+
 [prover.FramaC]
 slug = "frama_c"
 
@@ -130,6 +151,12 @@ slug = "f_star"
 [prover.GLPK]
 slug = "glpk"
 
+[prover.GNATprove]
+slug = "gna_tprove"
+
+[prover.GPUVerify]
+slug = "gpu_verify"
+
 [prover.GradualTypeChecker]
 slug = "gradual_type_checker"
 
@@ -151,6 +178,9 @@ slug = "homotopy_type_checker"
 [prover.Idris2]
 slug = "idris2"
 
+[prover.IleanCoP]
+slug = "ilean_co_p"
+
 [prover.Imandra]
 slug = "imandra"
 
@@ -166,6 +196,9 @@ slug = "indexed_type_checker"
 [prover.IntersectionTypeChecker]
 slug = "intersection_type_checker"
 
+[prover.IProver]
+slug = "i_prover"
+
 [prover.Isabelle]
 slug = "isabelle"
 
@@ -178,21 +211,36 @@ slug = "katagoria_verifier"
 [prover.KeY]
 slug = "ke_y"
 
+[prover.KeYmaeraX]
+slug = "ke_ymaera_x"
+
 [prover.Kissat]
 slug = "kissat"
 
+[prover.Konclude]
+slug = "konclude"
+
 [prover.LambdaProlog]
 slug = "lambda_prolog"
 
+[prover.Lash]
+slug = "lash"
+
 [prover.Lean]
 slug = "lean"
 
 [prover.Lean3]
 slug = "lean3"
 
+[prover.Leo3]
+slug = "leo3"
+
 [prover.LinearTypeChecker]
 slug = "linear_type_checker"
 
+[prover.LiquidHaskell]
+slug = "liquid_haskell"
+
 [prover.Matita]
 slug = "matita"
 
@@ -202,6 +250,12 @@ slug = "mercury"
 [prover.Metamath]
 slug = "metamath"
 
+[prover.MetiTarski]
+slug = "meti_tarski"
+
+[prover.MetTeL2]
+slug = "met_te_l2"
+
 [prover.MiniSat]
 slug = "mini_sat"
 
@@ -217,9 +271,15 @@ slug = "mizar"
 [prover.MizAR]
 slug = "miz_ar"
 
+[prover.MleanCoP]
+slug = "mlean_co_p"
+
 [prover.ModalTypeChecker]
 slug = "modal_type_checker"
 
+[prover.NanoCoP]
+slug = "nano_co_p"
+
 [prover.Naproche]
 slug = "naproche"
 
@@ -256,9 +316,15 @@ slug = "phantom_type_checker"
 [prover.PolymorphicTypeChecker]
 slug = "polymorphic_type_checker"
 
+[prover.Princess]
+slug = "princess"
+
 [prover.Prism]
 slug = "prism"
 
+[prover.ProB]
+slug = "pro_b"
+
 [prover.ProbabilisticTypeChecker]
 slug = "probabilistic_type_checker"
 
@@ -274,9 +340,15 @@ slug = "pro_verif"
 [prover.PVS]
 slug = "pvs"
 
+[prover.Qepcad]
+slug = "qepcad"
+
 [prover.QTTTypeChecker]
 slug = "qtt_type_checker"
 
+[prover.Redlog]
+slug = "redlog"
+
 [prover.RefinementTypeChecker]
 slug = "refinement_type_checker"
 
@@ -289,6 +361,9 @@ slug = "rocq"
 [prover.RowTypeChecker]
 slug = "row_type_checker"
 
+[prover.Satallax]
+slug = "satallax"
+
 [prover.SCIP]
 slug = "scip"
 
@@ -307,6 +382,12 @@ slug = "spass"
 [prover.SPIN]
 slug = "spin"
 
+[prover.Stainless]
+slug = "stainless"
+
+[prover.Storm]
+slug = "storm"
+
 [prover.SubtypingTypeChecker]
 slug = "subtyping_type_checker"
 
@@ -325,6 +406,9 @@ slug = "tlc"
 [prover.TropicalTypeChecker]
 slug = "tropical_type_checker"
 
+[prover.Twee]
+slug = "twee"
+
 [prover.Twelf]
 slug = "twelf"
 

Justfile

@@ -666,6 +666,27 @@ bench-chapel-mrr:
     cd src/chapel
     chpl -o bench_mrr bench_mrr.chpl
     ./bench_mrr --verbose=false --timeout=10
+    echo "# wrote src/chapel/bench_mrr_telemetry.csv + src/chapel/bench_mrr_summary.csv" >&2
+
+# Same bench, but surface only the corpus-level outcome breakdown: the
+# per-prover preempted / timed-out / success counts and the preemption
+# rate next to wall-clock, one line per strategy. This is the #162 view —
+# it answers "how much of the speculative win is preemption?" without
+# opening the 360-row telemetry file.
+bench-chapel-mrr-telemetry:
+    #!/usr/bin/env bash
+    set -euo pipefail
+    if command -v idris2 >/dev/null 2>&1 && [ -z "${IDRIS2_PREFIX:-}" ]; then
+      export IDRIS2_PREFIX="$(dirname "$(dirname "$(readlink -f "$(command -v idris2)")")")"
+    fi
+    cd src/chapel
+    chpl -o bench_mrr bench_mrr.chpl
+    ./bench_mrr --verbose=false --timeout=10 --telemetry-only=true
+    echo "corpus-level outcome breakdown (fixture=ALL):"
+    grep '^ALL,' bench_mrr_summary.csv | while IFS=, read -r _ strategy att ok fail preempt timeout na err notatt rate wall _ _; do
+      printf '  %-22s attempted=%-3s success=%-3s failure=%-3s preempted=%-3s timed_out=%-3s rate=%s wall=%ss\n' \
+        "$strategy" "$att" "$ok" "$fail" "$preempt" "$timeout" "$rate" "$wall"
+    done
 
 # Rebuild Chapel 2.8.0 from source with CHPL_LIB_PIC=pic so that
 # `chpl --library --dynamic` can produce a shared-library form of the

docs-site/content/api/graphql.adoc

@@ -21,7 +21,9 @@ query {
 }
 ----
 
-Returns all 30 prover backends.
+Returns all registered prover backends — 141 `+ProverKind+` variants over
+105 backend implementations. See `+docs/PROVER_COUNT.adoc+` (canonical) for
+the tier split and reproduction commands.
 
 ===== Get Proof State
 

docs/ARCHITECTURE.adoc

@@ -43,14 +43,14 @@ independently reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
 │              └──┬───────────────────────────────┬───┘                   │
 │                 │                               │                        │
 │   ┌─────────────▼────────────┐    ┌─────────────▼───────────────────┐   │
-│   │   Trust pipeline          │    │  128 ProverKind backends         │  │
-│   │   (verification/)         │    │  (provers/)                      │  │
-│   │   - integrity             │    │   89 external prover bindings    │  │
-│   │   - portfolio             │    │   39 TypeChecker disciplines     │  │
-│   │   - certificates          │    │      via TypedWasm Sigma         │  │
+│   │   Trust pipeline          │    │  141 ProverKind variants         │  │
+│   │   (verification/)         │    │  105 backend impl files          │  │
+│   │   - integrity             │    │  (provers/)                      │  │
+│   │   - portfolio             │    │  see docs/PROVER_COUNT.adoc      │  │
+│   │   - certificates          │    │                                  │  │
 │   │   - axiom tracker         │    │                                  │  │
-│   │   - confidence            │    │   Tier 1: 12 core (REST default) │  │
-│   │   - mutation              │    │   Tier 2–10: by capability       │  │
+│   │   - confidence            │    │  Tier 1: 12 core (REST default)  │  │
+│   │   - mutation              │    │  Tier 2–10: by capability        │  │
 │   │   - pareto                │    └──────────────────────────────────┘  │
 │   │   - statistics            │                                          │
 │   └───────────────────────────┘                                          │
@@ -80,13 +80,14 @@ independently reproduced where formats allow (Alethe, DRAT/LRAT, TSTP).
 
 === Tier overview
 
-ECHIDNA carries *128 ProverKind variants*. The exposed surface depends
-on tier:
+ECHIDNA carries *141 `+ProverKind+` variants* across *105 backend
+implementation files*. The exposed surface depends on tier:
 
-* *Tier 1 (12 core)* — the default REST `+/api/verify+` surface:
-Coq/Rocq, Lean 4, Agda, Isabelle/HOL, Idris 2, F*, Z3, CVC5, Alt-Ergo,
-Dafny, Vampire, E Prover.
-* *Tier 2–10* — 116 additional backends: ATPs, SMT, model checkers,
+* *Tier 1 (12 core)* — the default REST `+/api/verify+` surface, and
+exactly the set returned by `+ProverKind::all_core()+`: Coq, Lean 4,
+Agda, Isabelle/HOL, Z3, CVC5, Metamath, HOL Light, Mizar, PVS, ACL2,
+HOL4.
+* *Tier 2–10* — the remaining variants: ATPs, SMT, model checkers,
 constraint solvers, niche provers, ecosystem type-checkers. Available
 via explicit `+ProverKind+` selection in CLI / REPL / GraphQL but not
 auto-routed.

docs/ASPECT_IMPLEMENTATION_SUMMARY.adoc

@@ -250,7 +250,7 @@ file)
 * Uses `+crate::core::Term+` for theorem representation
 * Integrates with `+Theorem+` struct (has `+aspects: Vec<String>+`
 field)
-* Compatible with all 12 prover backends
+* Compatible with all Tier 1 (core) prover backends
 * Works with `+ProofState+` and `+Context+`
 
 ==== With Neural Components (Julia)

docs/ECOSYSTEM-INTEGRATION.adoc

@@ -141,7 +141,7 @@ Needs entry in `+repos+` section of farm-manifest.json
 [source,json]
 ----
 "echidna": {
-  "description": "Neurosymbolic theorem proving platform with 30 prover backends",
+  "description": "Neurosymbolic theorem proving platform with 141 ProverKind variants over 105 backend implementations",
   "forges": ["github", "gitlab", "sourcehut", "codeberg", "bitbucket"],
   "priority": "high",
   "auto_propagate": true,