chore(audit): clear lib+test warnings, fix prober dispatch bug, sync GraphQL ProverKind (#41)

Cargo `--lib --tests` and `cargo clippy --lib --tests` now run clean (0
warnings, 0 errors). 1460 unit + integration tests pass.

Real bugs found and fixed:

* `provers::mod::from_str`: `"prob"` alias was double-claimed. Line 525
  routes it to `ProverKind::ProB` (B-method model checker); a later arm
  also tried to claim it for `ProverKind::ProbabilisticTypeChecker`
  (unreachable). Removed the dead alias — `prob-types` and
  `probabilistic` still reach the type-checker.
* `gnn::fallback_monitor::record_fallback`: comment claimed
  "exponential moving average" with an unused `ema_weight = 0.2` local,
  but the formula is a cumulative arithmetic mean (and tests assert
  cumulative-mean values). Updated the comment to reflect actual
  behaviour and dropped the dead variable; SLA semantics unchanged.
* `dispatch::cross_check_dispatch`: the cross-checker filter held the
  `health_status` `MutexGuard` across an `await` (clippy
  `await_holding_lock`). Restructured into an explicit scope so the
  guard is released before any await.
* GraphQL workspace member did not compile: `cargo check -p
  echidna-graphql` reported 28 missing `ProverKind` variants. Synced
  `schema.rs` enum + `core_to_gql` + `gql_to_core`, `resolvers.rs`
  `ProverKindExt::{from_core,to_core}`, and `ffi_wrapper.rs` ordinals
  113-140 with the core enum. (Mizar/MizAR are intentionally distinct.)

Compliance fix:

* `deno.json` license was `MIT OR AGPL-3.0-or-later` — project policy
  per CLAUDE.md is `PMPL-1.0-or-later` (explicitly "not AGPL").

Diagnostics fields preserved as ML acronyms:

* `ModelHealth.{last_validation_nDCG, last_validation_MRR,
  nDCG_meets_threshold}` and `GnnTrainingMetrics.{nDCG, MRR}` now
  carry an `#[allow(non_snake_case)]` with a comment explaining that
  these field names match the JSON keys emitted by the Julia training
  pipeline (`src/julia/train_and_evaluate.jl`). Renaming would have
  silently broken the cross-language contract.

Resilience accessors:

* Exposed `CircuitBreaker::name(&self) -> &str` and
  `Bulkhead::config(&self) -> &BulkheadConfig` so the previously
  dead-but-stored fields are usable for diagnostics output.

Remaining clippy items (mechanical): unused imports, doc list
indentation, a few `field_reassign_with_default` cases (kept as-is
with `#[allow(...)]` where the alternative is uglier), and type
aliases for two complex closure-box types.

Out of scope (left untouched): pre-existing `cargo fmt` drift across
~820 files, `cargo test --workspace` requires `protoc` (gRPC build),
docs/* license-string drift in historical release notes, ROADMAP-
acknowledged ReScript→AffineScript migration.

https://claude.ai/code/session_01F6HnUof5QEwmf9nzbM8nc8

Co-authored-by: Claude <noreply@anthropic.com>

Author: hyperpolymath

deno.json

@@ -3,7 +3,7 @@
   "name": "@echidna/provers",
   "version": "0.1.0",
   "description": "ECHIDNA - Neurosymbolic Theorem Proving Platform",
-  "license": "MIT OR AGPL-3.0-or-later",
+  "license": "PMPL-1.0-or-later",
 
   "compilerOptions": {
     "allowJs": false,

src/interfaces/graphql/ffi_wrapper.rs

@@ -288,6 +288,34 @@ pub fn prover_kind_to_ffi(kind: &crate::schema::ProverKind) -> u8 {
         crate::schema::ProverKind::Rocq => 110,
         crate::schema::ProverKind::UppaalStratego => 111,
         crate::schema::ProverKind::MizAR => 112,
+        crate::schema::ProverKind::GPUVerify => 113,
+        crate::schema::ProverKind::Faial => 114,
+        crate::schema::ProverKind::Leo3 => 115,
+        crate::schema::ProverKind::Satallax => 116,
+        crate::schema::ProverKind::Lash => 117,
+        crate::schema::ProverKind::AgsyHOL => 118,
+        crate::schema::ProverKind::IProver => 119,
+        crate::schema::ProverKind::Princess => 120,
+        crate::schema::ProverKind::Twee => 121,
+        crate::schema::ProverKind::MetiTarski => 122,
+        crate::schema::ProverKind::CSI => 123,
+        crate::schema::ProverKind::AProVE => 124,
+        crate::schema::ProverKind::GNATprove => 125,
+        crate::schema::ProverKind::Stainless => 126,
+        crate::schema::ProverKind::LiquidHaskell => 127,
+        crate::schema::ProverKind::KeYmaeraX => 128,
+        crate::schema::ProverKind::Qepcad => 129,
+        crate::schema::ProverKind::Redlog => 130,
+        crate::schema::ProverKind::MleanCoP => 131,
+        crate::schema::ProverKind::IleanCoP => 132,
+        crate::schema::ProverKind::NanoCoP => 133,
+        crate::schema::ProverKind::MetTeL2 => 134,
+        crate::schema::ProverKind::ELK => 135,
+        crate::schema::ProverKind::Konclude => 136,
+        crate::schema::ProverKind::Storm => 137,
+        crate::schema::ProverKind::ProB => 138,
+        crate::schema::ProverKind::EasyCrypt => 139,
+        crate::schema::ProverKind::CryptoVerif => 140,
     }
 }
 
@@ -407,6 +435,34 @@ pub fn ffi_to_prover_kind(ordinal: u8) -> Option<crate::schema::ProverKind> {
         110 => Some(crate::schema::ProverKind::Rocq),
         111 => Some(crate::schema::ProverKind::UppaalStratego),
         112 => Some(crate::schema::ProverKind::MizAR),
+        113 => Some(crate::schema::ProverKind::GPUVerify),
+        114 => Some(crate::schema::ProverKind::Faial),
+        115 => Some(crate::schema::ProverKind::Leo3),
+        116 => Some(crate::schema::ProverKind::Satallax),
+        117 => Some(crate::schema::ProverKind::Lash),
+        118 => Some(crate::schema::ProverKind::AgsyHOL),
+        119 => Some(crate::schema::ProverKind::IProver),
+        120 => Some(crate::schema::ProverKind::Princess),
+        121 => Some(crate::schema::ProverKind::Twee),
+        122 => Some(crate::schema::ProverKind::MetiTarski),
+        123 => Some(crate::schema::ProverKind::CSI),
+        124 => Some(crate::schema::ProverKind::AProVE),
+        125 => Some(crate::schema::ProverKind::GNATprove),
+        126 => Some(crate::schema::ProverKind::Stainless),
+        127 => Some(crate::schema::ProverKind::LiquidHaskell),
+        128 => Some(crate::schema::ProverKind::KeYmaeraX),
+        129 => Some(crate::schema::ProverKind::Qepcad),
+        130 => Some(crate::schema::ProverKind::Redlog),
+        131 => Some(crate::schema::ProverKind::MleanCoP),
+        132 => Some(crate::schema::ProverKind::IleanCoP),
+        133 => Some(crate::schema::ProverKind::NanoCoP),
+        134 => Some(crate::schema::ProverKind::MetTeL2),
+        135 => Some(crate::schema::ProverKind::ELK),
+        136 => Some(crate::schema::ProverKind::Konclude),
+        137 => Some(crate::schema::ProverKind::Storm),
+        138 => Some(crate::schema::ProverKind::ProB),
+        139 => Some(crate::schema::ProverKind::EasyCrypt),
+        140 => Some(crate::schema::ProverKind::CryptoVerif),
         _ => None,
     }
 }

src/interfaces/graphql/resolvers.rs

@@ -218,6 +218,34 @@ impl ProverKindExt for crate::schema::ProverKind {
             CoreProverKind::Rocq => crate::schema::ProverKind::Rocq,
             CoreProverKind::UppaalStratego => crate::schema::ProverKind::UppaalStratego,
             CoreProverKind::MizAR => crate::schema::ProverKind::MizAR,
+            CoreProverKind::GPUVerify => crate::schema::ProverKind::GPUVerify,
+            CoreProverKind::Faial => crate::schema::ProverKind::Faial,
+            CoreProverKind::Leo3 => crate::schema::ProverKind::Leo3,
+            CoreProverKind::Satallax => crate::schema::ProverKind::Satallax,
+            CoreProverKind::Lash => crate::schema::ProverKind::Lash,
+            CoreProverKind::AgsyHOL => crate::schema::ProverKind::AgsyHOL,
+            CoreProverKind::IProver => crate::schema::ProverKind::IProver,
+            CoreProverKind::Princess => crate::schema::ProverKind::Princess,
+            CoreProverKind::Twee => crate::schema::ProverKind::Twee,
+            CoreProverKind::MetiTarski => crate::schema::ProverKind::MetiTarski,
+            CoreProverKind::CSI => crate::schema::ProverKind::CSI,
+            CoreProverKind::AProVE => crate::schema::ProverKind::AProVE,
+            CoreProverKind::GNATprove => crate::schema::ProverKind::GNATprove,
+            CoreProverKind::Stainless => crate::schema::ProverKind::Stainless,
+            CoreProverKind::LiquidHaskell => crate::schema::ProverKind::LiquidHaskell,
+            CoreProverKind::KeYmaeraX => crate::schema::ProverKind::KeYmaeraX,
+            CoreProverKind::Qepcad => crate::schema::ProverKind::Qepcad,
+            CoreProverKind::Redlog => crate::schema::ProverKind::Redlog,
+            CoreProverKind::MleanCoP => crate::schema::ProverKind::MleanCoP,
+            CoreProverKind::IleanCoP => crate::schema::ProverKind::IleanCoP,
+            CoreProverKind::NanoCoP => crate::schema::ProverKind::NanoCoP,
+            CoreProverKind::MetTeL2 => crate::schema::ProverKind::MetTeL2,
+            CoreProverKind::ELK => crate::schema::ProverKind::ELK,
+            CoreProverKind::Konclude => crate::schema::ProverKind::Konclude,
+            CoreProverKind::Storm => crate::schema::ProverKind::Storm,
+            CoreProverKind::ProB => crate::schema::ProverKind::ProB,
+            CoreProverKind::EasyCrypt => crate::schema::ProverKind::EasyCrypt,
+            CoreProverKind::CryptoVerif => crate::schema::ProverKind::CryptoVerif,
         }
     }
 
@@ -336,6 +364,34 @@ impl ProverKindExt for crate::schema::ProverKind {
             crate::schema::ProverKind::Rocq => CoreProverKind::Rocq,
             crate::schema::ProverKind::UppaalStratego => CoreProverKind::UppaalStratego,
             crate::schema::ProverKind::MizAR => CoreProverKind::MizAR,
+            crate::schema::ProverKind::GPUVerify => CoreProverKind::GPUVerify,
+            crate::schema::ProverKind::Faial => CoreProverKind::Faial,
+            crate::schema::ProverKind::Leo3 => CoreProverKind::Leo3,
+            crate::schema::ProverKind::Satallax => CoreProverKind::Satallax,
+            crate::schema::ProverKind::Lash => CoreProverKind::Lash,
+            crate::schema::ProverKind::AgsyHOL => CoreProverKind::AgsyHOL,
+            crate::schema::ProverKind::IProver => CoreProverKind::IProver,
+            crate::schema::ProverKind::Princess => CoreProverKind::Princess,
+            crate::schema::ProverKind::Twee => CoreProverKind::Twee,
+            crate::schema::ProverKind::MetiTarski => CoreProverKind::MetiTarski,
+            crate::schema::ProverKind::CSI => CoreProverKind::CSI,
+            crate::schema::ProverKind::AProVE => CoreProverKind::AProVE,
+            crate::schema::ProverKind::GNATprove => CoreProverKind::GNATprove,
+            crate::schema::ProverKind::Stainless => CoreProverKind::Stainless,
+            crate::schema::ProverKind::LiquidHaskell => CoreProverKind::LiquidHaskell,
+            crate::schema::ProverKind::KeYmaeraX => CoreProverKind::KeYmaeraX,
+            crate::schema::ProverKind::Qepcad => CoreProverKind::Qepcad,
+            crate::schema::ProverKind::Redlog => CoreProverKind::Redlog,
+            crate::schema::ProverKind::MleanCoP => CoreProverKind::MleanCoP,
+            crate::schema::ProverKind::IleanCoP => CoreProverKind::IleanCoP,
+            crate::schema::ProverKind::NanoCoP => CoreProverKind::NanoCoP,
+            crate::schema::ProverKind::MetTeL2 => CoreProverKind::MetTeL2,
+            crate::schema::ProverKind::ELK => CoreProverKind::ELK,
+            crate::schema::ProverKind::Konclude => CoreProverKind::Konclude,
+            crate::schema::ProverKind::Storm => CoreProverKind::Storm,
+            crate::schema::ProverKind::ProB => CoreProverKind::ProB,
+            crate::schema::ProverKind::EasyCrypt => CoreProverKind::EasyCrypt,
+            crate::schema::ProverKind::CryptoVerif => CoreProverKind::CryptoVerif,
         }
     }
 }

src/interfaces/graphql/schema.rs

@@ -123,6 +123,34 @@ pub enum ProverKind {
     Rocq,
     UppaalStratego,
     MizAR,
+    GPUVerify,
+    Faial,
+    Leo3,
+    Satallax,
+    Lash,
+    AgsyHOL,
+    IProver,
+    Princess,
+    Twee,
+    MetiTarski,
+    CSI,
+    AProVE,
+    GNATprove,
+    Stainless,
+    LiquidHaskell,
+    KeYmaeraX,
+    Qepcad,
+    Redlog,
+    MleanCoP,
+    IleanCoP,
+    NanoCoP,
+    MetTeL2,
+    ELK,
+    Konclude,
+    Storm,
+    ProB,
+    EasyCrypt,
+    CryptoVerif,
 }
 
 /// Status of a proof attempt
@@ -567,6 +595,34 @@ fn core_to_gql(kind: &CoreProverKind) -> ProverKind {
         CoreProverKind::Rocq => ProverKind::Rocq,
         CoreProverKind::UppaalStratego => ProverKind::UppaalStratego,
         CoreProverKind::MizAR => ProverKind::MizAR,
+        CoreProverKind::GPUVerify => ProverKind::GPUVerify,
+        CoreProverKind::Faial => ProverKind::Faial,
+        CoreProverKind::Leo3 => ProverKind::Leo3,
+        CoreProverKind::Satallax => ProverKind::Satallax,
+        CoreProverKind::Lash => ProverKind::Lash,
+        CoreProverKind::AgsyHOL => ProverKind::AgsyHOL,
+        CoreProverKind::IProver => ProverKind::IProver,
+        CoreProverKind::Princess => ProverKind::Princess,
+        CoreProverKind::Twee => ProverKind::Twee,
+        CoreProverKind::MetiTarski => ProverKind::MetiTarski,
+        CoreProverKind::CSI => ProverKind::CSI,
+        CoreProverKind::AProVE => ProverKind::AProVE,
+        CoreProverKind::GNATprove => ProverKind::GNATprove,
+        CoreProverKind::Stainless => ProverKind::Stainless,
+        CoreProverKind::LiquidHaskell => ProverKind::LiquidHaskell,
+        CoreProverKind::KeYmaeraX => ProverKind::KeYmaeraX,
+        CoreProverKind::Qepcad => ProverKind::Qepcad,
+        CoreProverKind::Redlog => ProverKind::Redlog,
+        CoreProverKind::MleanCoP => ProverKind::MleanCoP,
+        CoreProverKind::IleanCoP => ProverKind::IleanCoP,
+        CoreProverKind::NanoCoP => ProverKind::NanoCoP,
+        CoreProverKind::MetTeL2 => ProverKind::MetTeL2,
+        CoreProverKind::ELK => ProverKind::ELK,
+        CoreProverKind::Konclude => ProverKind::Konclude,
+        CoreProverKind::Storm => ProverKind::Storm,
+        CoreProverKind::ProB => ProverKind::ProB,
+        CoreProverKind::EasyCrypt => ProverKind::EasyCrypt,
+        CoreProverKind::CryptoVerif => ProverKind::CryptoVerif,
     }
 }
 
@@ -685,5 +741,33 @@ fn gql_to_core(kind: &ProverKind) -> CoreProverKind {
         ProverKind::Rocq => CoreProverKind::Rocq,
         ProverKind::UppaalStratego => CoreProverKind::UppaalStratego,
         ProverKind::MizAR => CoreProverKind::MizAR,
+        ProverKind::GPUVerify => CoreProverKind::GPUVerify,
+        ProverKind::Faial => CoreProverKind::Faial,
+        ProverKind::Leo3 => CoreProverKind::Leo3,
+        ProverKind::Satallax => CoreProverKind::Satallax,
+        ProverKind::Lash => CoreProverKind::Lash,
+        ProverKind::AgsyHOL => CoreProverKind::AgsyHOL,
+        ProverKind::IProver => CoreProverKind::IProver,
+        ProverKind::Princess => CoreProverKind::Princess,
+        ProverKind::Twee => CoreProverKind::Twee,
+        ProverKind::MetiTarski => CoreProverKind::MetiTarski,
+        ProverKind::CSI => CoreProverKind::CSI,
+        ProverKind::AProVE => CoreProverKind::AProVE,
+        ProverKind::GNATprove => CoreProverKind::GNATprove,
+        ProverKind::Stainless => CoreProverKind::Stainless,
+        ProverKind::LiquidHaskell => CoreProverKind::LiquidHaskell,
+        ProverKind::KeYmaeraX => CoreProverKind::KeYmaeraX,
+        ProverKind::Qepcad => CoreProverKind::Qepcad,
+        ProverKind::Redlog => CoreProverKind::Redlog,
+        ProverKind::MleanCoP => CoreProverKind::MleanCoP,
+        ProverKind::IleanCoP => CoreProverKind::IleanCoP,
+        ProverKind::NanoCoP => CoreProverKind::NanoCoP,
+        ProverKind::MetTeL2 => CoreProverKind::MetTeL2,
+        ProverKind::ELK => CoreProverKind::ELK,
+        ProverKind::Konclude => CoreProverKind::Konclude,
+        ProverKind::Storm => CoreProverKind::Storm,
+        ProverKind::ProB => CoreProverKind::ProB,
+        ProverKind::EasyCrypt => CoreProverKind::EasyCrypt,
+        ProverKind::CryptoVerif => CoreProverKind::CryptoVerif,
     }
 }

src/rust/agent/swarm.rs

@@ -34,7 +34,7 @@ use serde::{Deserialize, Serialize};
 use tokio::sync::{mpsc, Mutex};
 use tokio::task::JoinSet;
 
-use crate::learning::design_search::{AnnealConfig, AnnealResult, DesignProblem};
+use crate::learning::design_search::{AnnealConfig, DesignProblem};
 
 /// Configuration for a swarm run.
 #[derive(Debug, Clone, Serialize, Deserialize)]
@@ -152,6 +152,7 @@ fn delta_scalar(from: &[i64], to: &[i64]) -> f64 {
 
 /// Run a swarm over `problem`. Returns the global best across agents
 /// plus per-agent reports.
+#[allow(clippy::type_complexity, clippy::needless_range_loop)]
 pub async fn run_swarm<P>(problem: Arc<P>, config: SwarmConfig) -> SwarmResult<P::State>
 where
     P: DesignProblem + Send + Sync + 'static,

src/rust/coprocessor/audio.rs

@@ -80,7 +80,7 @@ fn dispatch_sync(op: CoprocessorOp) -> Result<CoprocessorOutcome> {
             duration_ms,
             sample_rate,
         } => {
-            if sample_rate < 8_000 || sample_rate > 192_000 {
+            if !(8_000..=192_000).contains(&sample_rate) {
                 return Ok(CoprocessorOutcome::Failure(format!(
                     "AudioSineWave: sample_rate {} outside [8000, 192000]",
                     sample_rate
@@ -97,7 +97,7 @@ fn dispatch_sync(op: CoprocessorOp) -> Result<CoprocessorOutcome> {
             CoprocessorOutcome::Hex(hex(&wav_pack(&pcm, sample_rate)))
         }
         CoprocessorOp::AudioCompletionChime { sample_rate } => {
-            if sample_rate < 8_000 || sample_rate > 192_000 {
+            if !(8_000..=192_000).contains(&sample_rate) {
                 return Ok(CoprocessorOutcome::Failure(format!(
                     "AudioCompletionChime: sample_rate {} outside [8000, 192000]",
                     sample_rate

src/rust/coprocessor/fpga.rs

@@ -13,7 +13,7 @@
 //! `yosys -p "synth -top <top_module>" <file>`, and returns the netlist
 //! output.  Fail with a clear diagnostic if yosys is not on PATH.
 
-use anyhow::{anyhow, Result};
+use anyhow::Result;
 use async_trait::async_trait;
 use std::io::Write;
 use std::process::Stdio;

src/rust/coprocessor/io.rs

@@ -13,7 +13,7 @@
 //! Path arguments are passed verbatim — caller is responsible for any path
 //! sanitisation (the prover-side trust pipeline does this before dispatch).
 
-use anyhow::{anyhow, Result};
+use anyhow::Result;
 use async_trait::async_trait;
 use sha2::{Digest, Sha256};
 use tokio::fs;

src/rust/coprocessor/math.rs

@@ -391,7 +391,7 @@ fn fib_fast_doubling(n: u64) -> BigUint {
         let (a, b) = helper(n / 2);
         let c = &a * (BigUint::from(2u32) * &b - &a);
         let d = &a * &a + &b * &b;
-        if n % 2 == 0 {
+        if n.is_multiple_of(2) {
             (c, d)
         } else {
             let e = &c + &d;

src/rust/coprocessor/physics.rs

@@ -129,7 +129,9 @@ fn rk4_step(kernel: &str, params: &[f64], x: &[f64], dt: f64) -> std::result::Re
     Ok(next)
 }
 
-fn build_kernel(name: &str, params: &[f64]) -> std::result::Result<Box<dyn Fn(&[f64]) -> Vec<f64>>, String> {
+type KernelFn = Box<dyn Fn(&[f64]) -> Vec<f64>>;
+
+fn build_kernel(name: &str, params: &[f64]) -> std::result::Result<KernelFn, String> {
     match name {
         "harmonic-oscillator" => {
             if params.len() != 1 {