Skip to content

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

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
May 2, 2026
Merged

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

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion deno.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
56 changes: 56 additions & 0 deletions src/interfaces/graphql/ffi_wrapper.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}
}

Expand Down Expand Up @@ -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,
}
}
56 changes: 56 additions & 0 deletions src/interfaces/graphql/resolvers.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,
}
}

Expand Down Expand Up @@ -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,
}
}
}
Expand Down
84 changes: 84 additions & 0 deletions src/interfaces/graphql/schema.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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,
}
}

Expand Down Expand Up @@ -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,
}
}
3 changes: 2 additions & 1 deletion src/rust/agent/swarm.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)]
Expand Down Expand Up @@ -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,
Expand Down
4 changes: 2 additions & 2 deletions src/rust/coprocessor/audio.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand Down
2 changes: 1 addition & 1 deletion src/rust/coprocessor/fpga.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion src/rust/coprocessor/io.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
2 changes: 1 addition & 1 deletion src/rust/coprocessor/math.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down
4 changes: 3 additions & 1 deletion src/rust/coprocessor/physics.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 {
Expand Down
2 changes: 1 addition & 1 deletion src/rust/coprocessor/singular.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -104,7 +104,7 @@ fn extract_generators(output: &str, ideal_name: &str) -> Vec<String> {
.filter_map(|line| {
let line = line.trim();
if line.starts_with(&prefix) {
line.splitn(2, '=').nth(1).map(|s| s.to_string())
line.split_once('=').map(|x| x.1).map(|s| s.to_string())
} else {
None
}
Expand Down
2 changes: 1 addition & 1 deletion src/rust/corpus/agda.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,7 @@

#![allow(dead_code)]

use std::collections::{HashMap, HashSet};
use std::collections::HashSet;
use std::path::{Path, PathBuf};

use anyhow::{Context, Result};
Expand Down
3 changes: 1 addition & 2 deletions src/rust/corpus/coq.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -561,15 +561,14 @@ fn top_level_colon(s: &str) -> Option<usize> {
'}' => depth_brace -= 1,
':' if depth_paren == 0 && depth_bracket == 0 && depth_brace == 0 => {
// Skip `::` (Coq has it for cons in some scopes).
let mut next_idx = i + ':'.len_utf8();
let next_idx = i + ':'.len_utf8();
if next_idx < s.len() && s[next_idx..].starts_with(':') {
continue;
}
// Skip `:=`.
if next_idx < s.len() && s[next_idx..].starts_with('=') {
continue;
}
let _ = next_idx;
return Some(i);
}
_ => {}
Expand Down
Loading
Loading