diff --git a/bots/echidnabot/Cargo.lock b/bots/echidnabot/Cargo.lock index 2ec63f7f..d24802f3 100644 --- a/bots/echidnabot/Cargo.lock +++ b/bots/echidnabot/Cargo.lock @@ -247,13 +247,13 @@ dependencies = [ [[package]] name = "async-trait" -version = "0.1.89" +version = "0.1.92" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9035ad2d096bed7955a320ee7e2230574d28fd3c3a0f186cbea1ff3c7eed5dbb" +checksum = "82f6aeea286b8eb4dd3431a1be1b59d290ace00f5bfd8e2a159bc2a05e2c1667" dependencies = [ "proc-macro2", "quote", - "syn 2.0.117", + "syn 3.0.3", ] [[package]] @@ -1108,6 +1108,14 @@ version = "1.0.5" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "92773504d58c093f6de2459af4af33faa518c13451eb8f2b5698ed3d36e7c813" +[[package]] +name = "echidna-core-spark" +version = "0.1.0" +source = "git+https://github.com/hyperpolymath/echidna?rev=b761b3a832981be51d4e88076ef1b90fe5037e9c#b761b3a832981be51d4e88076ef1b90fe5037e9c" +dependencies = [ + "serde", +] + [[package]] name = "echidnabot" version = "0.1.0" @@ -1122,6 +1130,7 @@ dependencies = [ "clap", "config", "criterion", + "echidna-core-spark", "gitbot-shared-context", "hex", "hmac 0.13.0", @@ -1133,8 +1142,10 @@ dependencies = [ "proptest", "rand 0.10.2", "reqwest 0.12.28", + "semver", "serde", "serde_json", + "serde_json_canonicalizer", "sha2 0.11.0", "sqlx", "tempfile", @@ -3513,6 +3524,12 @@ version = "1.0.23" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9774ba4a74de5f7b1c1451ed6cd5285a32eddb5cccb8cc655a4e50009e06477f" +[[package]] +name = "ryu-js" +version = "1.0.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "04d056b875a9d2e6cb9a61d127afee9ac5999b9f87bcb32079d1318e505be714" + [[package]] name = "same-file" version = "1.0.6" @@ -3634,6 +3651,17 @@ dependencies = [ "zmij", ] +[[package]] +name = "serde_json_canonicalizer" +version = "0.3.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "fe52319a927259afbfa5180c5157cd8167edfd3e8c254f9558c7fef44c5649f2" +dependencies = [ + "ryu-js", + "serde", + "serde_json", +] + [[package]] name = "serde_path_to_error" version = "0.1.20" diff --git a/bots/echidnabot/Cargo.toml b/bots/echidnabot/Cargo.toml index 902523ac..4a9ac680 100644 --- a/bots/echidnabot/Cargo.toml +++ b/bots/echidnabot/Cargo.toml @@ -28,6 +28,19 @@ path = "src/main.rs" # Fleet coordination gitbot-shared-context = { version = "0.1.0", git = "https://github.com/hyperpolymath/gitbot-fleet", rev = "40ef6bf1a43813948476d33c764e3405adc950c2" } +# ECHIDNA trust kernel. Canonical trust-level algorithm and source-level +# axiom scanner, shared with ECHIDNA so echidnabot no longer re-implements +# them. Pinned by full rev (immutable). At this rev the crate is still named +# `echidna-core-spark`; it is being renamed `echidna-core-creusot` upstream, +# and the trust types are meant to move into `echidna-core` proper. Follow-up: +# re-point this line once that lands on echidna `main` (see +# docs/ECHIDNA-INTEGRATION.adoc). +echidna-core-spark = { git = "https://github.com/hyperpolymath/echidna", rev = "b761b3a832981be51d4e88076ef1b90fe5037e9c" } + +# Minimum-version handshake with the ECHIDNA server. +semver = "1" + + # Async runtime tokio = { version = "1", features = ["full"] } @@ -70,7 +83,12 @@ reqwest = { version = "0.12", default-features = false, features = ["json", "rus # Utilities async-trait = "0.1" -uuid = { version = "1", features = ["v4", "serde"] } +# v7 for records, v8 for content ids; minted only in src/ids.rs. +uuid = { version = "1.10", features = ["v7", "v8", "serde"] } +# RFC 8785 (JCS) canonical bytes for src/ids.rs content ids. The estate +# crate hyperpolymath/ijson-jcs is not public, so a public build cannot +# depend on it; swap once it is (docs/ECHIDNA-INTEGRATION.adoc). +serde_json_canonicalizer = "0.3" chrono = { version = "0.4", features = ["serde"] } thiserror = "2" anyhow = "1" diff --git a/bots/echidnabot/FLEET-SYNC.json b/bots/echidnabot/FLEET-SYNC.json index d58959ed..3f7c2c1a 100644 --- a/bots/echidnabot/FLEET-SYNC.json +++ b/bots/echidnabot/FLEET-SYNC.json @@ -1 +1 @@ -{"fleet_owned":["CANONICAL_SOURCE.adoc","FLEET-SYNC.json"],"include":[".cargo","Cargo.lock","Cargo.toml","Containerfile","LICENSE","LICENSES","README.adoc","benches","config","echidnabot.example.toml","fuzz","migrations","proofs","src","tests"],"repo":"https://github.com/hyperpolymath/echidnabot","rev":"bf2c0ffc9f5faee3c2072b516855a045400ac247","schema":"gitbot-fleet.vendor-sync/1","upstream_branch":"main"} +{"fleet_owned":["CANONICAL_SOURCE.adoc","FLEET-SYNC.json"],"include":[".cargo","Cargo.lock","Cargo.toml","Containerfile","LICENSE","LICENSES","README.adoc","benches","config","echidnabot.example.toml","fuzz","migrations","proofs","src","tests"],"repo":"https://github.com/hyperpolymath/echidnabot","rev":"faeb2808efcf1fc8149afc5811182cb14bf79091","schema":"gitbot-fleet.vendor-sync/1","upstream_branch":"main"} diff --git a/bots/echidnabot/README.adoc b/bots/echidnabot/README.adoc index 8ec330cf..edd52bdd 100644 --- a/bots/echidnabot/README.adoc +++ b/bots/echidnabot/README.adoc @@ -72,7 +72,7 @@ echidnabot init-db # Start the webhook server export DATABASE_URL=sqlite:echidnabot.db -export ECHIDNA_URL=http://localhost:8080 +export ECHIDNA_URL=http://127.0.0.1:8081 echidnabot serve --port 8080 ---- diff --git a/bots/echidnabot/benches/echidnabot_bench.rs b/bots/echidnabot/benches/echidnabot_bench.rs index 4605a68d..7f84d71d 100644 --- a/bots/echidnabot/benches/echidnabot_bench.rs +++ b/bots/echidnabot/benches/echidnabot_bench.rs @@ -24,7 +24,6 @@ use sha2::Sha256; // one; CI runs clippy with `-D warnings`, so the re-export is an error here. use std::hint::black_box; use std::net::{IpAddr, Ipv4Addr}; -use uuid::Uuid; // ────────────────────────────────────────────────────────────────────────────── // HMAC-SHA256 webhook signature verification @@ -158,7 +157,7 @@ fn bench_goal_fingerprint(c: &mut Criterion) { // ────────────────────────────────────────────────────────────────────────────── fn bench_proof_job_new(c: &mut Criterion) { - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); let prover = ProverKind::new("coq"); let files = vec![ "theories/Main.v".to_string(), diff --git a/bots/echidnabot/config/echidnabot.ncl b/bots/echidnabot/config/echidnabot.ncl index f31ac6e6..f95fb178 100644 --- a/bots/echidnabot/config/echidnabot.ncl +++ b/bots/echidnabot/config/echidnabot.ncl @@ -91,8 +91,8 @@ let Config = { max_connections = 5, }, echidna = { - endpoint = "http://localhost:8080/graphql", - rest_endpoint = "http://localhost:8080", + endpoint = "http://127.0.0.1:8081/", + rest_endpoint = "http://127.0.0.1:8081", mode = 'auto, timeout_seconds = 120, }, diff --git a/bots/echidnabot/echidnabot.example.toml b/bots/echidnabot/echidnabot.example.toml index 774bbbb5..77dbfcc4 100644 --- a/bots/echidnabot/echidnabot.example.toml +++ b/bots/echidnabot/echidnabot.example.toml @@ -17,9 +17,9 @@ max_connections = 5 [echidna] # ECHIDNA Core GraphQL endpoint -endpoint = "http://localhost:8080/graphql" +endpoint = "http://127.0.0.1:8081/" # ECHIDNA Core REST endpoint -rest_endpoint = "http://localhost:8080" +rest_endpoint = "http://127.0.0.1:8081" # API mode: auto, graphql, rest mode = "auto" # Timeout for proof verification (seconds) diff --git a/bots/echidnabot/migrations/20261008000001_proof_obligations.sql b/bots/echidnabot/migrations/20261008000001_proof_obligations.sql new file mode 100644 index 00000000..3b423f69 --- /dev/null +++ b/bots/echidnabot/migrations/20261008000001_proof_obligations.sql @@ -0,0 +1,19 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) +-- +-- proof_obligations — obligations received via the `submitProofObligation` +-- GraphQL mutation (hypatia FleetDispatcher / LearningScheduler). +-- Mirrors the SQLite DDL emitted at runtime by `SqliteStore::run_migrations`. +-- `id` is a UUIDv8 content id; `repo_id` is nullable because the sender +-- names a repo slug that need not be registered with echidnabot. +CREATE TABLE IF NOT EXISTS proof_obligations ( + id TEXT PRIMARY KEY, + repo_slug TEXT NOT NULL, + repo_id TEXT REFERENCES repositories(id), + claim TEXT NOT NULL, + context TEXT NOT NULL, + prover TEXT, + inline_requested INTEGER NOT NULL, + status TEXT NOT NULL, + created_at TEXT NOT NULL +); diff --git a/bots/echidnabot/src/api/graphql.rs b/bots/echidnabot/src/api/graphql.rs index f26f8429..9b6b0a10 100644 --- a/bots/echidnabot/src/api/graphql.rs +++ b/bots/echidnabot/src/api/graphql.rs @@ -14,7 +14,8 @@ use crate::dispatcher::{ }; use crate::scheduler::{JobPriority, JobScheduler}; use crate::store::models::{ - goal_fingerprint, ProofJobRecord, Repository as StoreRepository, TacticOutcomeRecord, + goal_fingerprint, ProofJobRecord, ProofObligationRecord, Repository as StoreRepository, + TacticOutcomeRecord, }; use crate::store::Store; @@ -385,6 +386,41 @@ pub struct RepoSettingsInput { pub auto_comment: Option, } +/// Upper bound on `claim` and `context`, in bytes. The endpoint has no auth, +/// so a cap keeps one request from writing an unbounded row. +pub const MAX_OBLIGATION_FIELD_BYTES: usize = 64 * 1024; + +/// Input for submitting a proof obligation (hypatia's wire contract) +#[derive(async_graphql::InputObject)] +pub struct SubmitProofObligationInput { + /// Repository slug `owner/name`; it need not be registered here + pub repo: String, + /// The claim to be proved, as prover-agnostic text + pub claim: String, + /// Free-text context for the claim + pub context: String, + /// Prover hint; absent means "echidnabot chooses" + pub prover: Option, + /// Sender asks for inline verification. Recorded, NOT acted on yet + pub inline: Option, +} + +/// Result of `submitProofObligation` +#[derive(SimpleObject, Clone)] +pub struct ProofObligationPayload { + /// `true` means the obligation is persisted. It does NOT mean proved: + /// failures are GraphQL errors, never `success: false` + pub success: bool, + /// UUIDv8 content id of the obligation (stable across resubmission) + pub proof_id: ID, + /// Always `PENDING` today: no dispatcher consumes obligations yet + pub status: String, + /// `false` when an identical obligation was already stored + pub newly_recorded: bool, + /// Whether `repo` matched a repository registered on GitHub here + pub repo_registered: bool, +} + #[Object] impl MutationRoot { /// Register a repository for monitoring @@ -585,6 +621,69 @@ impl MutationRoot { .map_err(|e| async_graphql::Error::new(e.to_string()))?; Ok(TacticOutcome::from(record)) } + + /// Accept a proof obligation from hypatia and persist it as `PENDING`. + /// + /// Accepted is not proved: nothing dispatches stored obligations to a + /// prover yet, and `inline: true` is recorded but not honoured. Invalid + /// input or a store failure is returned as a GraphQL error, because one of + /// the two senders reads only `errors` and ignores `success`. + async fn submit_proof_obligation( + &self, + ctx: &Context<'_>, + input: SubmitProofObligationInput, + ) -> async_graphql::Result { + let state = ctx.data::()?; + + let (owner, name) = match input.repo.split_once('/') { + Some((o, n)) if !o.is_empty() && !n.is_empty() && !n.contains('/') => (o, n), + _ => { + return Err(async_graphql::Error::new(format!( + "repo must be an owner/name slug, got {:?}", + input.repo + ))) + } + }; + if input.claim.trim().is_empty() { + return Err(async_graphql::Error::new("claim must not be empty")); + } + for (field, value) in [("claim", &input.claim), ("context", &input.context)] { + if value.len() > MAX_OBLIGATION_FIELD_BYTES { + return Err(async_graphql::Error::new(format!( + "{field} exceeds {MAX_OBLIGATION_FIELD_BYTES} bytes" + ))); + } + } + + let repo_id = state + .store + .get_repository_by_name(crate::adapters::Platform::GitHub, owner, name) + .await + .map_err(|e| async_graphql::Error::new(e.to_string()))? + .map(|r| r.id); + + let record = ProofObligationRecord::new( + input.repo.clone(), + repo_id, + input.claim, + input.context, + input.prover.map(map_prover_kind_to_core), + input.inline.unwrap_or(false), + ); + let newly_recorded = state + .store + .record_proof_obligation(&record) + .await + .map_err(|e| async_graphql::Error::new(e.to_string()))?; + + Ok(ProofObligationPayload { + success: true, + proof_id: ID::from(record.id.to_string()), + status: record.status, + newly_recorded, + repo_registered: repo_id.is_some(), + }) + } } impl From for Repository { diff --git a/bots/echidnabot/src/config.rs b/bots/echidnabot/src/config.rs index 33d57fe9..b062bc08 100644 --- a/bots/echidnabot/src/config.rs +++ b/bots/echidnabot/src/config.rs @@ -374,12 +374,16 @@ impl Default for EchidnaConfig { } } +/// Default ECHIDNA GraphQL endpoint: the separate `echidna-graphql` binary, +/// which serves GraphQL at `/` on 127.0.0.1:8081 (`echidna server` has no +/// GraphQL route; in `auto` mode the REST fallback reaches it instead). fn default_echidna_endpoint() -> String { - "http://localhost:8080/graphql".to_string() + "http://127.0.0.1:8081/".to_string() } +/// Default ECHIDNA REST base URL (same `echidna server`, port 8081). fn default_echidna_rest_endpoint() -> String { - "http://localhost:8080".to_string() + "http://127.0.0.1:8081".to_string() } fn default_echidna_mode() -> EchidnaApiMode { @@ -390,7 +394,7 @@ fn default_timeout() -> u64 { 300 // 5 minutes } -#[derive(Debug, Deserialize, Clone)] +#[derive(Deserialize, Clone)] pub struct GitHubConfig { /// GitHub App ID pub app_id: Option, @@ -405,7 +409,7 @@ pub struct GitHubConfig { pub webhook_secret: Option, } -#[derive(Debug, Deserialize, Clone)] +#[derive(Deserialize, Clone)] pub struct GitLabConfig { /// GitLab instance URL pub url: String, @@ -435,7 +439,7 @@ pub struct GitLabConfig { /// (statuses, comments, issues) require a token; the adapter /// returns `Error::Config("CODEBERG_TOKEN not set")` when missing. /// The `CODEBERG_TOKEN` env var also works as a fallback. -#[derive(Debug, Deserialize, Clone)] +#[derive(Deserialize, Clone)] pub struct CodebergConfig { /// Codeberg / Forgejo / Gitea instance URL. pub url: String, @@ -499,3 +503,80 @@ impl Config { Ok(parsed) } } + +/// Render a secret-bearing field for `Debug` without its value. +/// Returns `""` for `Some` and `""` for `None`. +/// +/// Pattern from the types fit map (secret-types is not yet a usable +/// library): tokens and webhook secrets never reach logs through `{:?}`. +pub fn redacted(value: &Option) -> &'static str { + if value.is_some() { + "" + } else { + "" + } +} + +impl std::fmt::Debug for GitHubConfig { + /// Debug output with `token` and `webhook_secret` redacted. + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("GitHubConfig") + .field("app_id", &self.app_id) + .field("private_key_path", &self.private_key_path) + .field("token", &redacted(&self.token)) + .field("webhook_secret", &redacted(&self.webhook_secret)) + .finish() + } +} + +impl std::fmt::Debug for GitLabConfig { + /// Debug output with `token` and `webhook_secret` redacted. + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("GitLabConfig") + .field("url", &self.url) + .field("token", &"") + .field("webhook_secret", &redacted(&self.webhook_secret)) + .finish() + } +} + +impl std::fmt::Debug for CodebergConfig { + /// Debug output with `token` and `webhook_secret` redacted. + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("CodebergConfig") + .field("url", &self.url) + .field("token", &redacted(&self.token)) + .field("webhook_secret", &redacted(&self.webhook_secret)) + .finish() + } +} + +#[cfg(test)] +mod redaction_tests { + use super::*; + + /// Secrets never appear in `Debug` output; their presence still does. + #[test] + fn forge_configs_redact_secrets_in_debug() { + let gh = GitHubConfig { + app_id: Some(1), + private_key_path: None, + token: Some("ghp_SECRET".into()), + webhook_secret: Some("whsec_SECRET".into()), + }; + let gl = GitLabConfig { + url: "https://gitlab.com".into(), + token: "glpat_SECRET".into(), + webhook_secret: None, + }; + let cb = CodebergConfig { + url: "https://codeberg.org".into(), + token: Some("cb_SECRET".into()), + webhook_secret: Some("cbwh_SECRET".into()), + }; + for out in [format!("{gh:?}"), format!("{gl:?}"), format!("{cb:?}")] { + assert!(!out.contains("SECRET"), "{out}"); + assert!(out.contains(""), "{out}"); + } + } +} diff --git a/bots/echidnabot/src/dispatcher/echidna_client.rs b/bots/echidnabot/src/dispatcher/echidna_client.rs index 096626eb..cf4a2889 100644 --- a/bots/echidnabot/src/dispatcher/echidna_client.rs +++ b/bots/echidnabot/src/dispatcher/echidna_client.rs @@ -5,14 +5,33 @@ use reqwest::Client; use serde::{Deserialize, Serialize}; +use std::sync::RwLock; use std::time::Duration; -use super::{ProofResult, ProofStatus, ProverKind, TacticSuggestion}; +use super::prove_result::ProveResult; +use super::{ProofResult, ProofStatus, ProverKind, TacticSuggestion, TrustSource}; use crate::config::{EchidnaApiMode, EchidnaConfig}; use crate::error::{Error, Result}; -use crate::trust::{axiom_tracker::AxiomTracker, confidence::assess_confidence}; +use crate::trust::axiom_tracker::{AxiomFlag, AxiomReport, AxiomTracker}; +use crate::trust::confidence::assess_confidence_with_axioms; use tracing::warn; +/// Oldest ECHIDNA server release echidnabot talks to. +/// +/// 2.3.0 is the first tagged release whose REST `/api/verify` returns the +/// typed `outcome` field and whose `/api/health` reports `version`. +pub const MIN_ECHIDNA_VERSION: &str = "2.3.0"; + +/// What the start-up handshake learned about the ECHIDNA server. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct EchidnaHandshake { + /// Server version, from `/api/provers` if it reports one, else + /// `/api/health`. + pub version: semver::Version, + /// ECHIDNA's own prover identifiers, as listed by `/api/provers`. + pub provers: Vec, +} + /// Client for ECHIDNA Core GraphQL API pub struct EchidnaClient { client: Client, @@ -20,10 +39,16 @@ pub struct EchidnaClient { rest_endpoint: String, timeout: Duration, mode: EchidnaApiMode, + /// Result of the last successful [`EchidnaClient::handshake`]; its + /// prover list maps echidnabot slugs onto ECHIDNA's names. + handshake: RwLock>, } impl EchidnaClient { /// Create a new ECHIDNA client + /// + /// # Panics + /// Panics if the HTTP client cannot be initialised. pub fn new(config: &EchidnaConfig) -> Self { let client = Client::builder() .timeout(Duration::from_secs(config.timeout_secs)) @@ -36,9 +61,102 @@ impl EchidnaClient { rest_endpoint: config.rest_endpoint.clone(), timeout: Duration::from_secs(config.timeout_secs), mode: config.mode, + handshake: RwLock::new(None), } } + /// Minimum-version handshake with the ECHIDNA server. + /// + /// Lists `/api/provers` (which also proves the REST surface is there) and + /// reads the version from that response if present, otherwise from + /// `/api/health`. Returns the version and prover names, caching them for + /// slug resolution unless the cache lock is poisoned. + /// + /// # Errors + /// Returns [`Error::Http`] for request failures, [`Error::Echidna`] for + /// 5xx responses, and [`Error::EchidnaIncompatible`] for other unsuccessful + /// statuses, unreadable response bodies, or a missing, unparseable or + /// older-than-[`MIN_ECHIDNA_VERSION`] version. + pub async fn handshake(&self) -> Result { + let response = self + .client + .get(self.rest_url("/api/provers")) + .timeout(Duration::from_secs(10)) + .send() + .await + .map_err(Error::Http)?; + check_handshake_status("/api/provers", response.status())?; + let provers: RestProversResponse = response.json().await.map_err(|e| { + Error::EchidnaIncompatible(format!("/api/provers body not understood: {e}")) + })?; + + let raw_version = match provers.version.clone().or(provers.echidna_version.clone()) { + Some(v) => v, + None => { + let health = self + .client + .get(self.rest_url("/api/health")) + .timeout(Duration::from_secs(5)) + .send() + .await + .map_err(Error::Http)?; + check_handshake_status("/api/health", health.status())?; + let health: RestHealthResponse = health.json().await.map_err(|e| { + Error::EchidnaIncompatible(format!("/api/health body not understood: {e}")) + })?; + health.version.ok_or_else(|| { + Error::EchidnaIncompatible(format!( + "ECHIDNA did not report a version; {MIN_ECHIDNA_VERSION} or newer is required" + )) + })? + } + }; + + let version = check_min_version(&raw_version)?; + let handshake = EchidnaHandshake { + version, + provers: provers.provers.into_iter().map(|p| p.name).collect(), + }; + if let Ok(mut slot) = self.handshake.write() { + *slot = Some(handshake.clone()); + } + Ok(handshake) + } + + /// Whether this client talks REST at all (and so can run the handshake). + /// + /// GraphQL-only deployments have no `/api/provers`; they skip it. + pub fn uses_rest(&self) -> bool { + !matches!(self.mode, EchidnaApiMode::Graphql) + } + + /// Run [`EchidnaClient::handshake`] unless one has already succeeded. + /// + /// Returns the cached result without rechecking the server. If the cache + /// is empty or unreadable, performs the handshake and propagates its errors. + pub async fn ensure_handshake(&self) -> Result { + let cached = self.handshake.read().ok().and_then(|slot| slot.clone()); + match cached { + Some(done) => Ok(done), + None => self.handshake().await, + } + } + + /// ECHIDNA's identifier for an echidnabot prover slug. + /// + /// Uses the list learned by [`EchidnaClient::handshake`] when one is + /// available, ignoring case, `-`, `_`, spaces and `/`. With no match, + /// uses the classic prover mapping or the prover's display name. + pub fn echidna_name(&self, prover: &ProverKind) -> String { + let known = self + .handshake + .read() + .ok() + .and_then(|slot| slot.as_ref().map(|h| h.provers.clone())) + .unwrap_or_default(); + resolve_echidna_name(prover, &known) + } + /// Verify a proof using ECHIDNA Core #[tracing::instrument( name = "echidna.verify", @@ -141,6 +259,12 @@ impl EchidnaClient { format!("{}{}", base, path) } + /// Submit proof source through GraphQL and derive confidence locally from + /// its source, prover output and certificate artefact names. + /// + /// Returns [`Error::Http`] for request or response-decoding failures and + /// [`Error::Echidna`] for unsuccessful HTTP statuses, GraphQL errors or + /// missing response data. async fn verify_proof_graphql( &self, prover: &ProverKind, @@ -207,8 +331,10 @@ impl EchidnaClient { || a.ends_with(".drat") || a.ends_with(".tstp") }); - let axioms = AxiomTracker::scan(prover, &prover_output); - let confidence = assess_confidence(prover, status, has_cert, 1); + let axioms = AxiomTracker::scan_source(prover, content) + .merge(AxiomTracker::scan(prover, &prover_output)); + let confidence = + assess_confidence_with_axioms(prover, status, has_cert, 1, axioms.worst_danger); Ok(ProofResult { status, message: data.verify_proof.message, @@ -217,6 +343,7 @@ impl EchidnaClient { artifacts, confidence: Some(confidence), axioms: Some(axioms), + trust_source: TrustSource::LocalFallback, }) } @@ -347,9 +474,14 @@ impl EchidnaClient { } } + /// Submit proof source to `/api/verify` using the resolved prover name. + /// + /// Returns [`Error::Http`] for request or JSON-decoding failures and + /// [`Error::Echidna`] for unsuccessful HTTP statuses. Result validation + /// errors from [`rest_verify_result`] are propagated. async fn verify_proof_rest(&self, prover: &ProverKind, content: &str) -> Result { let request = RestVerifyRequest { - prover: prover_to_echidna_name(prover), + prover: self.echidna_name(prover), content: content.to_string(), }; @@ -369,31 +501,16 @@ impl EchidnaClient { ))); } - let data: RestVerifyResponse = response.json().await.map_err(Error::Http)?; - let status = if data.valid { - ProofStatus::Verified - } else { - ProofStatus::Failed - }; - // REST endpoint returns no raw output; axiom scan over empty string = clean. - let prover_output = String::new(); - let axioms = AxiomTracker::scan(prover, &prover_output); - let confidence = assess_confidence(prover, status, false, 1); - Ok(ProofResult { - status, - message: if data.valid { - "Proof verified successfully".to_string() - } else { - "Proof verification failed".to_string() - }, - prover_output, - duration_ms: 0, - artifacts: Vec::new(), - confidence: Some(confidence), - axioms: Some(axioms), - }) + let body: serde_json::Value = response.json().await.map_err(Error::Http)?; + rest_verify_result(prover, content, body) } + /// Request up to five tactics for `goal_state`, or for `context` when the + /// goal state is blank. Each returned tactic receives confidence `0.5` + /// and a heuristic explanation. + /// + /// Returns [`Error::Http`] for request or response-decoding failures and + /// [`Error::Echidna`] for unsuccessful HTTP statuses. async fn suggest_tactics_rest( &self, prover: &ProverKind, @@ -407,7 +524,7 @@ impl EchidnaClient { }; let request = RestSuggestRequest { - prover: prover_to_echidna_name(prover), + prover: self.echidna_name(prover), content, limit: Some(5), }; @@ -454,6 +571,10 @@ impl EchidnaClient { } } + /// Check whether `/api/provers` lists a matching normalised prover name. + /// + /// An absent name yields `Unavailable`; unsuccessful HTTP statuses yield + /// `Unknown`. Request and response-decoding failures return [`Error::Http`]. async fn prover_status_rest(&self, prover: &ProverKind) -> Result { let response = self .client @@ -468,11 +589,11 @@ impl EchidnaClient { } let data: RestProversResponse = response.json().await.map_err(Error::Http)?; - let target = prover_to_echidna_name(prover).to_lowercase(); - let available = data - .provers - .into_iter() - .any(|info| info.name.to_lowercase() == target); + let names: Vec = data.provers.into_iter().map(|info| info.name).collect(); + let target = normalise_prover_name(&resolve_echidna_name(prover, &names)); + let available = names + .iter() + .any(|name| normalise_prover_name(name) == target); Ok(if available { ProverStatus::Available @@ -492,15 +613,154 @@ struct RestVerifyRequest { content: String, } +/// Legacy REST `/api/verify` body (ECHIDNA ≤ 2.3 shape). #[derive(Deserialize)] struct RestVerifyResponse { valid: bool, + /// Typed outcome (`PROVED`, `NO_PROOF_FOUND`, `TIMEOUT`, ...); absent on + /// very old servers. + #[serde(default)] + outcome: Option, #[allow(dead_code)] + #[serde(default)] goals_remaining: usize, #[allow(dead_code)] + #[serde(default)] tactics_used: usize, } +/// Build a [`ProofResult`] from a REST `/api/verify` body. +/// +/// An `echidna.prove.result/1` body supplies status, message, duration in +/// milliseconds and reported axioms ([`TrustSource::Echidna`]). Its axioms +/// are merged with a scan of `content`; confidence is recalculated locally, +/// ignoring the reported confidence. Other bodies use the legacy shape, +/// source-only axiom scanning and a zero duration. Both return empty prover +/// output and artefact lists. +/// +/// # Errors +/// Propagates [`ProveResult::from_value`] validation errors for tagged bodies +/// without trying the legacy shape. Legacy deserialisation errors return +/// [`Error::Json`]. +fn rest_verify_result( + prover: &ProverKind, + content: &str, + body: serde_json::Value, +) -> Result { + if ProveResult::is_prove_result(&body) { + let result = ProveResult::from_value(body)?; + let status = ProofStatus::from(result.status); + let reported = AxiomReport::from_reported( + prover.clone(), + result.trust.axioms.iter().map(|a| AxiomFlag::from_name(a)), + ); + // ECHIDNA's list is the receipt and counts at full severity (a named + // `sorry` caps the level even if the source looks clean, e.g. a hole + // in an imported module). The source scan is merged in as well, so a + // hole ECHIDNA did not name still counts. + let axioms = reported.merge(AxiomTracker::scan_source(prover, content)); + let confidence = + assess_confidence_with_axioms(prover, status, false, 1, axioms.worst_danger); + return Ok(ProofResult { + status, + message: result.message, + prover_output: String::new(), + duration_ms: result.duration_ms, + artifacts: Vec::new(), + confidence: Some(confidence), + axioms: Some(axioms), + trust_source: TrustSource::Echidna, + }); + } + + let data: RestVerifyResponse = serde_json::from_value(body)?; + let status = match data.outcome.as_deref() { + Some(outcome) => parse_rest_outcome(outcome, data.valid), + None if data.valid => ProofStatus::Verified, + None => ProofStatus::Failed, + }; + // The legacy REST body carries no prover output, so the only axiom + // signal is the source scan. + let axioms = AxiomTracker::scan_source(prover, content); + let confidence = assess_confidence_with_axioms(prover, status, false, 1, axioms.worst_danger); + Ok(ProofResult { + status, + message: match status { + ProofStatus::Verified => "Proof verified successfully".to_string(), + ProofStatus::Timeout => "Proof verification timed out".to_string(), + ProofStatus::Error => "ECHIDNA reported an error".to_string(), + _ => "Proof verification failed".to_string(), + }, + prover_output: String::new(), + duration_ms: 0, + artifacts: Vec::new(), + confidence: Some(confidence), + axioms: Some(axioms), + trust_source: TrustSource::LocalFallback, + }) +} + +/// Map ECHIDNA's typed REST outcome onto [`ProofStatus`]. +/// +/// Matching ignores ASCII case. Unknown outcomes yield `Verified` when +/// `valid` is true and `Unknown` otherwise; recognised outcomes ignore `valid`. +fn parse_rest_outcome(outcome: &str, valid: bool) -> ProofStatus { + match outcome.to_ascii_uppercase().as_str() { + "PROVED" => ProofStatus::Verified, + "NO_PROOF_FOUND" | "INVALID_INPUT" | "INCONSISTENT_PREMISES" => ProofStatus::Failed, + "TIMEOUT" => ProofStatus::Timeout, + "UNSUPPORTED_FEATURE" | "PROVER_ERROR" | "SYSTEM_ERROR" => ProofStatus::Error, + _ if valid => ProofStatus::Verified, + _ => ProofStatus::Unknown, + } +} + +#[derive(Deserialize)] +struct RestHealthResponse { + /// Absent on servers older than 2.3.0. + #[serde(default)] + version: Option, +} + +/// Accept successful handshake statuses and classify failures. +/// +/// Returns [`Error::Echidna`] for 5xx responses, classified as transient by +/// [`crate::scheduler::retry::is_transient_error`]. Other unsuccessful statuses +/// return [`Error::EchidnaIncompatible`]. `path` identifies the failing endpoint. +fn check_handshake_status(path: &str, status: reqwest::StatusCode) -> Result<()> { + if status.is_success() { + Ok(()) + } else if status.is_server_error() { + Err(Error::Echidna(format!( + "ECHIDNA {path} unavailable (status {status})" + ))) + } else { + Err(Error::EchidnaIncompatible(format!( + "ECHIDNA {path} returned status {status}" + ))) + } +} + +/// Parse a reported ECHIDNA version and enforce [`MIN_ECHIDNA_VERSION`]. +/// +/// Surrounding whitespace and leading lowercase `v` characters are ignored. +/// Returns [`Error::EchidnaIncompatible`] if parsing fails or the version is +/// below the minimum, using semantic-version ordering. +pub fn check_min_version(raw: &str) -> Result { + let trimmed = raw.trim().trim_start_matches('v'); + let version = semver::Version::parse(trimmed).map_err(|e| { + Error::EchidnaIncompatible(format!("ECHIDNA reported unparseable version {raw:?}: {e}")) + })?; + let minimum = semver::Version::parse(MIN_ECHIDNA_VERSION) + .map_err(|e| Error::Internal(format!("MIN_ECHIDNA_VERSION is not semver: {e}")))?; + if version < minimum { + return Err(Error::EchidnaIncompatible(format!( + "ECHIDNA {version} is older than the minimum supported {minimum}" + ))); + } + Ok(version) +} + #[derive(Serialize)] struct RestSuggestRequest { prover: String, @@ -516,21 +776,46 @@ struct RestSuggestResponse { #[derive(Deserialize)] struct RestProversResponse { provers: Vec, + /// Not sent by ECHIDNA 2.3; accepted if a later server adds it. + #[serde(default)] + version: Option, + /// Alternative spelling, matching the prove-result contract. + #[serde(default)] + echidna_version: Option, } #[derive(Deserialize)] struct RestProverInfo { name: String, #[allow(dead_code)] + #[serde(default)] tier: u8, #[allow(dead_code)] + #[serde(default)] complexity: u8, } -fn prover_to_echidna_name(prover: &ProverKind) -> String { - // These are ECHIDNA's serde enum names, not presentation labels. +/// Lower-case a prover name and drop `-`, `_`, spaces and `/` for matching. +fn normalise_prover_name(name: &str) -> String { + name.chars() + .filter(|c| !matches!(c, '-' | '_' | ' ' | '/')) + .flat_map(char::to_lowercase) + .collect() +} + +/// Map an echidnabot slug onto ECHIDNA's identifier. +/// +/// With a non-empty `known` list (from `/api/provers`) the first normalised +/// match wins. Without one, or with no match, the static mapping for the +/// classic provers applies; these are ECHIDNA's serde enum names, not +/// presentation labels. +fn resolve_echidna_name(prover: &ProverKind, known: &[String]) -> String { + let wanted = normalise_prover_name(prover.as_str()); + if let Some(hit) = known.iter().find(|k| normalise_prover_name(k) == wanted) { + return hit.clone(); + } match prover.as_str() { - "lean" => "Lean", + "lean" | "lean4" => "Lean", "isabelle" => "Isabelle", "hol-light" => "HOLLight", _ => prover.display_name(), @@ -653,4 +938,106 @@ mod tests { assert_eq!(ProverKind::new("lean").tier(), 1); assert_eq!(ProverKind::new("hol4").tier(), 3); } + + #[test] + fn test_min_version_gate() { + assert!(check_min_version("2.3.0").is_ok()); + assert!(check_min_version("v2.4.1").is_ok()); + assert!(check_min_version("2.2.9").is_err()); + assert!(check_min_version("not-a-version").is_err()); + } + + #[test] + fn test_resolve_name_prefers_handshake_list() { + let known = vec!["HOLLight".to_string(), "Idris2".to_string()]; + assert_eq!( + resolve_echidna_name(&ProverKind::new("hol-light"), &known), + "HOLLight" + ); + assert_eq!( + resolve_echidna_name(&ProverKind::new("idris2"), &known), + "Idris2" + ); + // Falls back to the static classic mapping without a list. + assert_eq!(resolve_echidna_name(&ProverKind::new("lean"), &[]), "Lean"); + } + + #[test] + fn test_rest_body_in_prove_result_shape_is_transported() { + let body = serde_json::json!({ + "schema": "echidna.prove.result/1", + "status": "verified", + "prover": "Lean", + "goal": "t", + "duration_ms": 7, + "message": "ok", + "trust": {"confidence": null, "axioms": ["propext"]}, + "echidna_version": "2.4.0" + }); + let r = rest_verify_result( + &ProverKind::new("lean"), + "theorem t : True := trivial", + body, + ) + .unwrap(); + assert_eq!(r.status, ProofStatus::Verified); + assert_eq!(r.trust_source, TrustSource::Echidna); + assert_eq!(r.duration_ms, 7); + assert!(r.axioms.unwrap().flags.contains(&AxiomFlag::ClassicalAxiom)); + } + + #[test] + fn test_reported_sorry_caps_level_even_with_clean_source() { + let body = serde_json::json!({ + "schema": "echidna.prove.result/1", + "status": "verified", + "prover": "Lean", + "goal": "t", + "duration_ms": 1, + "message": "ok", + "trust": {"confidence": null, "axioms": ["sorryAx"]}, + "echidna_version": "2.4.0" + }); + let r = rest_verify_result( + &ProverKind::new("lean"), + "theorem t : True := trivial", + body, + ) + .unwrap(); + assert!(r.axioms.as_ref().unwrap().has_unsound()); + assert_eq!( + r.confidence.unwrap().level, + crate::trust::confidence::ConfidenceLevel::Level1 + ); + } + + #[test] + fn test_handshake_status_classification() { + use reqwest::StatusCode; + assert!(check_handshake_status("/api/provers", StatusCode::OK).is_ok()); + let warmup = check_handshake_status("/api/provers", StatusCode::SERVICE_UNAVAILABLE); + assert!(matches!(warmup, Err(Error::Echidna(_)))); + assert!(crate::scheduler::retry::is_transient_error( + &warmup.unwrap_err() + )); + assert!(matches!( + check_handshake_status("/api/provers", StatusCode::NOT_FOUND), + Err(Error::EchidnaIncompatible(_)) + )); + assert!(matches!( + check_min_version("2.2.0"), + Err(Error::EchidnaIncompatible(_)) + )); + } + + #[test] + fn test_legacy_rest_body_uses_outcome_and_source_scan() { + let body = serde_json::json!({ + "valid": false, "outcome": "TIMEOUT", "goals_remaining": 1, "tactics_used": 0 + }); + let r = rest_verify_result(&ProverKind::new("lean"), " sorry\n", body).unwrap(); + assert_eq!(r.status, ProofStatus::Timeout); + assert_eq!(r.trust_source, TrustSource::LocalFallback); + assert!(r.axioms.unwrap().has_unsound()); + } } diff --git a/bots/echidnabot/src/dispatcher/mod.rs b/bots/echidnabot/src/dispatcher/mod.rs index b37912b8..4b48a47a 100644 --- a/bots/echidnabot/src/dispatcher/mod.rs +++ b/bots/echidnabot/src/dispatcher/mod.rs @@ -4,8 +4,10 @@ //! Prover dispatcher - communicates with ECHIDNA Core pub mod echidna_client; +pub mod prove_result; -pub use echidna_client::EchidnaClient; +pub use echidna_client::{EchidnaClient, EchidnaHandshake, MIN_ECHIDNA_VERSION}; +pub use prove_result::{ProveResult, PROVE_RESULT_SCHEMA}; use serde::{Deserialize, Serialize}; @@ -27,6 +29,37 @@ pub struct ProofResult { /// Axiom usage flags scanned from prover output. #[serde(default)] pub axioms: Option, + /// Where `confidence` and `axioms` came from. Results stored before this + /// field existed deserialise as [`TrustSource::LocalFallback`]. + #[serde(default)] + pub trust_source: TrustSource, +} + +/// Provenance of the trust data attached to a [`ProofResult`]. +/// +/// Pattern from `hyperpolymath/epistemic-types` (receipt vs warrant), adopted +/// as a plain enum; there is no Rust port of those types to depend on. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, Serialize, Deserialize)] +#[serde(rename_all = "kebab-case")] +pub enum TrustSource { + /// ECHIDNA reported the axiom data itself (an `echidna.prove.result/1` + /// `trust` object). echidnabot transports it unchanged (a receipt); the + /// level is still computed by ECHIDNA's trust kernel, linked in. + Echidna, + /// echidnabot computed the trust data from what ECHIDNA returned, using + /// ECHIDNA's trust kernel and source scanner: a warrant, not a receipt. + #[default] + LocalFallback, +} + +impl TrustSource { + /// Short label used in check-run summaries and PR comments. + pub fn label(&self) -> &'static str { + match self { + Self::Echidna => "axioms reported by ECHIDNA", + Self::LocalFallback => "derived locally by echidnabot (ECHIDNA did not report trust)", + } + } } /// Proof verification status diff --git a/bots/echidnabot/src/dispatcher/prove_result.rs b/bots/echidnabot/src/dispatcher/prove_result.rs new file mode 100644 index 00000000..2d25794c --- /dev/null +++ b/bots/echidnabot/src/dispatcher/prove_result.rs @@ -0,0 +1,199 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell +//! Consumer side of the shared `echidna.prove.result/1` contract. +//! +//! ECHIDNA's `echidna prove ... --output json` prints exactly one +//! JCS-canonical (RFC 8785) I-JSON (RFC 7493) object: +//! +//! ```json +//! {"duration_ms":12,"echidna_version":"2.3.0","goal":"t","message":"...", +//! "prover":"Lean","schema":"echidna.prove.result/1","status":"verified", +//! "trust":{"axioms":[],"confidence":null}} +//! ``` +//! +//! echidnabot accepts that object wherever it consumes a result: a REST +//! `/api/verify` body that carries `"schema":"echidna.prove.result/1"` is read +//! as this shape, and anything else falls back to the legacy REST shape. +//! +//! The `trust` object is ECHIDNA's own judgement (a *receipt*, in the +//! vocabulary of `hyperpolymath/epistemic-types`). echidnabot transports it +//! instead of re-deriving a score; see [`super::TrustSource`]. +//! +//! Validation here is deliberately strict about the parts a consumer depends +//! on (schema tag, status vocabulary, the I-JSON integer bound on +//! `duration_ms`, finite `confidence`) and liberal about key order, so a +//! non-canonical but otherwise valid object is still accepted. + +use serde::{Deserialize, Serialize}; + +use super::ProofStatus; +use crate::error::{Error, Result}; + +/// The schema tag every `echidna.prove.result/1` object carries. +pub const PROVE_RESULT_SCHEMA: &str = "echidna.prove.result/1"; + +/// Largest integer I-JSON (RFC 7493 §2.2) guarantees to round-trip: 2^53 − 1. +pub const IJSON_MAX_SAFE_INTEGER: u64 = (1 << 53) - 1; + +/// Status vocabulary of `echidna.prove.result/1`. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "lowercase")] +pub enum ProveStatus { + /// The prover accepted the proof. + Verified, + /// The prover rejected the proof. + Failed, + /// ECHIDNA or the backend failed before producing a verdict. + Error, + /// The backend ran out of time. + Timeout, + /// No verdict either way. + Unknown, +} + +impl From for ProofStatus { + /// Map the contract's status onto echidnabot's own status enum. + fn from(status: ProveStatus) -> Self { + match status { + ProveStatus::Verified => ProofStatus::Verified, + ProveStatus::Failed => ProofStatus::Failed, + ProveStatus::Error => ProofStatus::Error, + ProveStatus::Timeout => ProofStatus::Timeout, + ProveStatus::Unknown => ProofStatus::Unknown, + } + } +} + +/// ECHIDNA's trust judgement for one result. +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +pub struct ProveTrust { + /// ECHIDNA's confidence, or `null` when no receipt-backed computation + /// produced one. + pub confidence: Option, + /// Axioms / holes ECHIDNA found in the proof. + pub axioms: Vec, +} + +/// One `echidna.prove.result/1` object. +#[derive(Debug, Clone, PartialEq, Serialize, Deserialize)] +#[serde(deny_unknown_fields)] +pub struct ProveResult { + /// Always [`PROVE_RESULT_SCHEMA`]. + pub schema: String, + /// Verdict. + pub status: ProveStatus, + /// ECHIDNA's prover identifier. + pub prover: String, + /// The goal or theorem name. + pub goal: String, + /// Wall-clock duration; bounded by [`IJSON_MAX_SAFE_INTEGER`]. + pub duration_ms: u64, + /// Human-readable message. + pub message: String, + /// ECHIDNA's trust judgement. + pub trust: ProveTrust, + /// Version of the ECHIDNA that produced the object. + pub echidna_version: String, +} + +impl ProveResult { + /// Parse and validate one `echidna.prove.result/1` object from text. + /// + /// Accepts surrounding whitespace and non-canonical key order. Invalid + /// JSON returns [`Error::Json`]; validation errors from [`Self::from_value`] + /// are propagated. + pub fn parse(text: &str) -> Result { + let value: serde_json::Value = serde_json::from_str(text.trim())?; + Self::from_value(value) + } + + /// Validate an already-parsed JSON value as `echidna.prove.result/1`. + /// + /// # Errors + /// Returns [`Error::Echidna`] for a missing or different schema tag, a + /// supplied duration outside the integer range `0..=2^53-1` milliseconds, + /// or non-finite confidence. Returns [`Error::Json`] for deserialisation + /// failures, including missing required fields, unknown top-level fields + /// and unknown statuses. Unknown fields within `trust` are ignored. + pub fn from_value(value: serde_json::Value) -> Result { + if !Self::is_prove_result(&value) { + return Err(Error::Echidna(format!( + "not an {PROVE_RESULT_SCHEMA} object (schema tag missing or different)" + ))); + } + if let Some(d) = value.get("duration_ms") { + match d.as_u64() { + Some(n) if n <= IJSON_MAX_SAFE_INTEGER => {} + _ => { + return Err(Error::Echidna(format!( + "duration_ms must be a non-negative integer <= 2^53-1 (I-JSON), got {d}" + ))) + } + } + } + let parsed: ProveResult = serde_json::from_value(value)?; + if let Some(c) = parsed.trust.confidence { + if !c.is_finite() { + return Err(Error::Echidna( + "trust.confidence must be a finite number or null".to_string(), + )); + } + } + Ok(parsed) + } + + /// Whether a JSON value carries the `echidna.prove.result/1` schema tag. + pub fn is_prove_result(value: &serde_json::Value) -> bool { + value.get("schema").and_then(|s| s.as_str()) == Some(PROVE_RESULT_SCHEMA) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + const CANONICAL: &str = r#"{"duration_ms":12,"echidna_version":"2.3.0","goal":"t","message":"ok","prover":"Lean","schema":"echidna.prove.result/1","status":"verified","trust":{"axioms":[],"confidence":null}}"#; + + #[test] + fn parses_canonical_object() { + let r = ProveResult::parse(CANONICAL).unwrap(); + assert_eq!(r.status, ProveStatus::Verified); + assert_eq!(ProofStatus::from(r.status), ProofStatus::Verified); + assert_eq!(r.trust.confidence, None); + assert_eq!(r.duration_ms, 12); + } + + #[test] + fn accepts_non_canonical_key_order() { + let text = r#"{"schema":"echidna.prove.result/1","status":"timeout","prover":"Z3","goal":"g","duration_ms":5,"message":"","trust":{"confidence":0.5,"axioms":["classical"]},"echidna_version":"2.4.0"}"#; + let r = ProveResult::parse(text).unwrap(); + assert_eq!(ProofStatus::from(r.status), ProofStatus::Timeout); + assert_eq!(r.trust.axioms, vec!["classical".to_string()]); + } + + #[test] + fn rejects_wrong_schema_tag() { + let text = CANONICAL.replace("echidna.prove.result/1", "echidna.prove.result/2"); + assert!(ProveResult::parse(&text).is_err()); + } + + #[test] + fn rejects_unknown_status() { + let text = CANONICAL.replace("\"verified\"", "\"proved\""); + assert!(ProveResult::parse(&text).is_err()); + } + + #[test] + fn rejects_duration_outside_ijson_range() { + let text = CANONICAL.replace("\"duration_ms\":12", "\"duration_ms\":9007199254740992"); + assert!(ProveResult::parse(&text).is_err()); + let text = CANONICAL.replace("\"duration_ms\":12", "\"duration_ms\":9007199254740991"); + assert!(ProveResult::parse(&text).is_ok()); + } + + #[test] + fn rejects_unknown_fields() { + let text = CANONICAL.replace("\"goal\":\"t\"", "\"goal\":\"t\",\"extra\":1"); + assert!(ProveResult::parse(&text).is_err()); + } +} diff --git a/bots/echidnabot/src/error.rs b/bots/echidnabot/src/error.rs index 018285ba..c94a5d59 100644 --- a/bots/echidnabot/src/error.rs +++ b/bots/echidnabot/src/error.rs @@ -41,6 +41,11 @@ pub enum Error { #[error("ECHIDNA communication error: {0}")] Echidna(String), + /// The ECHIDNA server answered but is not one echidnabot can talk to + /// (too old, no version, or an unexpected REST shape). Never transient. + #[error("ECHIDNA server incompatible: {0}")] + EchidnaIncompatible(String), + #[error("Webhook verification failed: {0}")] WebhookVerification(String), diff --git a/bots/echidnabot/src/feedback/corpus_delta.rs b/bots/echidnabot/src/feedback/corpus_delta.rs index 3b43c0c7..09988571 100644 --- a/bots/echidnabot/src/feedback/corpus_delta.rs +++ b/bots/echidnabot/src/feedback/corpus_delta.rs @@ -333,10 +333,9 @@ pub struct RefreshStatus { mod tests { use super::*; use tokio::io::AsyncReadExt; - use uuid::Uuid; fn tmp_dir() -> PathBuf { - std::env::temp_dir().join(format!("echidnabot-corpus-{}", Uuid::new_v4())) + std::env::temp_dir().join(format!("echidnabot-corpus-{}", crate::ids::new_record_id())) } fn sample_row(succeeded: bool) -> DeltaRow { diff --git a/bots/echidnabot/src/feedback/reranker.rs b/bots/echidnabot/src/feedback/reranker.rs index cd1222ce..635dd379 100644 --- a/bots/echidnabot/src/feedback/reranker.rs +++ b/bots/echidnabot/src/feedback/reranker.rs @@ -141,11 +141,12 @@ impl Reranker { mod tests { use super::*; use crate::store::SqliteStore; - use uuid::Uuid; async fn fresh_store() -> (Arc, std::path::PathBuf) { - let path = - std::env::temp_dir().join(format!("echidnabot-rerank-test-{}.db", Uuid::new_v4())); + let path = std::env::temp_dir().join(format!( + "echidnabot-rerank-test-{}.db", + crate::ids::new_record_id() + )); let url = format!("sqlite://{}?mode=rwc", path.display()); let store = SqliteStore::new(&url).await.unwrap(); (Arc::new(store) as Arc, path) diff --git a/bots/echidnabot/src/fleet/mod.rs b/bots/echidnabot/src/fleet/mod.rs index f8706217..540d0b27 100644 --- a/bots/echidnabot/src/fleet/mod.rs +++ b/bots/echidnabot/src/fleet/mod.rs @@ -171,7 +171,6 @@ mod tests { use crate::dispatcher::ProverKind; use crate::scheduler::JobId; use chrono::Utc; - use uuid::Uuid; #[test] fn test_fleet_coordinator_lifecycle() { @@ -195,7 +194,7 @@ mod tests { let job = ProofJob { id: JobId::new(), - repo_id: Uuid::new_v4(), + repo_id: crate::ids::new_record_id(), commit_sha: "abc123".to_string(), prover: ProverKind::new("coq"), file_paths: vec!["test.v".to_string()], @@ -218,6 +217,7 @@ mod tests { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; coordinator.publish_finding(&job, &result).unwrap(); @@ -235,7 +235,7 @@ mod tests { let job = ProofJob { id: JobId::new(), - repo_id: Uuid::new_v4(), + repo_id: crate::ids::new_record_id(), commit_sha: "abc123".to_string(), prover: ProverKind::new("lean"), file_paths: vec!["test.lean".to_string()], @@ -258,6 +258,7 @@ mod tests { failed_files: vec!["test.lean".to_string()], confidence: None, axioms: None, + trust_source: Default::default(), }; coordinator.publish_finding(&job, &result).unwrap(); @@ -274,7 +275,7 @@ mod tests { let job = ProofJob { id: JobId::new(), - repo_id: Uuid::new_v4(), + repo_id: crate::ids::new_record_id(), commit_sha: "abc123".to_string(), prover: ProverKind::new("z3"), file_paths: vec!["test.smt2".to_string()], @@ -297,6 +298,7 @@ mod tests { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; // Should not error when not connected diff --git a/bots/echidnabot/src/ids.rs b/bots/echidnabot/src/ids.rs new file mode 100644 index 00000000..f8d506e4 --- /dev/null +++ b/bots/echidnabot/src/ids.rs @@ -0,0 +1,114 @@ +// SPDX-License-Identifier: MPL-2.0 +// Copyright (c) Jonathan D.A. Jewell +//! # Identifier minting — the only place echidnabot mints ids +//! +//! Two kinds of identifier, and nothing else in the crate mints one: +//! +//! * [`new_record_id`] — a **UUIDv7** (RFC 9562 §5.7) for *events and +//! records*: jobs, repositories, proof-result records, fleet findings. +//! Time-ordered, minted from the `uuid` crate's library API as +//! `standards/docs/UUID-V7-ESTATE-STANDARD.adoc` requires (no hand-set +//! version bits). +//! * [`content_id`] — a **UUIDv8** (RFC 9562 §5.8, Appendix B.2 style) for +//! *content*: proof goals and `echidna.prove.result/1` objects. It is +//! SHA-256 over the RFC 8785 (JCS) canonical bytes of the value, truncated +//! to the first 16 bytes, with the version nibble set to `8` and the +//! variant bits set to `10`. The same JSON content always yields the same +//! id, whatever key order or whitespace it arrived in. +//! +//! The v7/v8 split is the owner's delegated policy of 2026-10-05: v7 for +//! things that *happened*, v8 for things that *are* (content addressing). +//! The same split, with the same construction, is implemented in +//! `hyperpolymath/echidna` (`src/rust/ids.rs`) and +//! `hyperpolymath/proof-burrower` (`burrower-core/src/ids.rs`), so a content +//! id computed by any of the three agrees. See +//! `docs/ECHIDNA-INTEGRATION.adoc` § Identifiers. +//! +//! IDs that arrive from outside (a forge's repository id, an ECHIDNA job id) +//! keep whatever format they came with; this module only mints our own. + +use sha2::{Digest, Sha256}; +use uuid::Uuid; + +/// Mint a fresh time-ordered record id (UUIDv7). +/// +/// Use for events and records: jobs, repositories, result records, fleet +/// findings. Within one process successive ids sort in minting order (the +/// `uuid` crate keeps a monotonic counter inside the millisecond). +pub fn new_record_id() -> Uuid { + Uuid::now_v7() +} + +/// Content id of a JSON value: UUIDv8 over SHA-256 of its JCS bytes. +/// +/// Use for proof goals and prove results. Fails only if the value cannot be +/// canonicalised (RFC 8785 rejects non-finite numbers, which +/// `serde_json::Value` cannot hold anyway, so this is defensive). +pub fn content_id(value: &serde_json::Value) -> Result { + let canonical = serde_json_canonicalizer::to_vec(value)?; + let digest = Sha256::digest(&canonical); + let mut first16 = [0u8; 16]; + first16.copy_from_slice(&digest[..16]); + // `new_v8` overwrites the version nibble with 8 and the variant bits + // with RFC 9562's `10`; the other 122 bits are the hash prefix. + Ok(Uuid::new_v8(first16)) +} + +/// Content id of a proof goal's text (a JSON string). +/// +/// Hashes the exact text as a JSON string, without trimming or normalisation. +/// Returns the nil UUID if canonicalisation fails instead of propagating an error. +pub fn goal_content_id(goal_text: &str) -> Uuid { + content_id(&serde_json::Value::String(goal_text.to_string())).unwrap_or_else(|_| Uuid::nil()) +} + +#[cfg(test)] +mod tests { + use super::*; + use serde_json::json; + + /// Same JCS content gives the same v8 id regardless of key order and spacing. + #[test] + fn same_canonical_content_same_v8_id() { + let a: serde_json::Value = serde_json::from_str(r#"{"b":1,"a":[true,null]}"#).unwrap(); + let b: serde_json::Value = + serde_json::from_str("{ \"a\" : [ true , null ] , \"b\" : 1 }").unwrap(); + assert_eq!(content_id(&a).unwrap(), content_id(&b).unwrap()); + assert_ne!( + content_id(&a).unwrap(), + content_id(&json!({"a":[true,null],"b":2})).unwrap() + ); + } + + /// The v8 id is exactly the SHA-256 prefix with version/variant bits applied. + #[test] + fn v8_bits_and_hash_prefix() { + let id = content_id(&json!("lemma foo: x = y")).unwrap(); + assert_eq!(id.get_version_num(), 8); + assert_eq!(id.get_variant(), uuid::Variant::RFC4122); + let bytes = id.as_bytes(); + assert_eq!(bytes[6] >> 4, 0x8); + assert_eq!(bytes[8] >> 6, 0b10); + let digest = Sha256::digest(br#""lemma foo: x = y""#); + for (i, byte) in bytes.iter().enumerate() { + let mask = match i { + 6 => 0x0f, + 8 => 0x3f, + _ => 0xff, + }; + assert_eq!(byte & mask, digest[i] & mask, "byte {i}"); + } + assert_eq!(goal_content_id("lemma foo: x = y"), id); + } + + /// v7 record ids carry version 7 and sort in minting order. + #[test] + fn v7_record_ids_are_versioned_and_monotonic() { + let ids: Vec = (0..1000).map(|_| new_record_id()).collect(); + for w in ids.windows(2) { + assert!(w[0] < w[1], "{} !< {}", w[0], w[1]); + } + assert_eq!(ids[0].get_version_num(), 7); + assert_eq!(ids[0].get_variant(), uuid::Variant::RFC4122); + } +} diff --git a/bots/echidnabot/src/lib.rs b/bots/echidnabot/src/lib.rs index e9d17fe7..993c6164 100644 --- a/bots/echidnabot/src/lib.rs +++ b/bots/echidnabot/src/lib.rs @@ -21,7 +21,8 @@ pub mod dispatcher; pub mod error; pub mod executor; // Container isolation for secure prover execution pub mod feedback; // Double-loop: proof-history reranker + corpus delta (Package 7b) -pub mod fleet; // gitbot-fleet coordination layer +pub mod fleet; +pub mod ids; // The single ID-minting module (UUIDv7 records, UUIDv8 content ids) // gitbot-fleet coordination layer pub mod llm; // BoJ-mediated LLM client (Consultant-mode Q&A) pub mod modes; // Bot operating modes (Verifier/Advisor/Consultant/Regulator) pub mod observability; // Structured logging + OpenTelemetry distributed tracing (OTLP) diff --git a/bots/echidnabot/src/main.rs b/bots/echidnabot/src/main.rs index e0f62eb9..34b90c7a 100644 --- a/bots/echidnabot/src/main.rs +++ b/bots/echidnabot/src/main.rs @@ -238,6 +238,13 @@ type TracerFlushHook = Box< + 'static, >; +/// Initialise storage and the scheduler, then serve HTTP on `host:port`. +/// On shutdown, drain jobs within the configured timeout, close storage and +/// run `tracer_hook` if supplied. +/// +/// Propagates storage initialisation, incompatible ECHIDNA handshake and +/// listener-binding errors. HTTP serving errors trigger shutdown and are +/// consumed; other handshake failures allow start-up to continue. async fn serve( config: &Config, host: &str, @@ -288,6 +295,7 @@ async fn serve( config.scheduler.queue_size, )); let echidna = Arc::new(EchidnaClient::new(&config.echidna)); + startup_handshake(&echidna).await?; let graphql_state = GraphQLState { store: store.clone(), @@ -717,6 +725,11 @@ async fn init_db(config: &Config) -> Result<()> { Ok(()) } +/// Process queued jobs sequentially, persist outcomes and report them to the +/// originating platform. Job errors become unsuccessful results; persistence, +/// feedback and reporting failures do not stop the loop. +/// +/// Checks `shutdown` while waiting for work, without interrupting an active job. async fn run_scheduler_loop( scheduler: Arc, store: Arc, @@ -751,6 +764,7 @@ async fn run_scheduler_loop( failed_files: vec![], confidence: None, axioms: None, + trust_source: echidnabot::dispatcher::TrustSource::LocalFallback, } } }; @@ -796,17 +810,18 @@ async fn run_scheduler_loop( /// /// Cascade: /// 1. Look up the repository row to recover platform + bot mode. -/// 2. Resolve the effective mode via `modes::resolve_mode` (directive -/// content is None until the executor lands a clone-and-read step). +/// 2. Resolve the effective mode from the fetched repository directive, +/// repository settings and daemon default. /// 3. Build the platform-appropriate adapter. /// 4. Translate the `JobResult` into a `ProofResult` for the formatter, /// then format per-mode. -/// 5. Always create a check run; comment on the originating PR for +/// 5. Attempt a check run; comment on the originating PR for /// modes that opt in (Advisor / Consultant / Regulator). /// -/// All steps are best-effort. Errors are surfaced to the caller (which -/// logs but does not propagate them), so a 503 from GitHub or a missing -/// token never blocks the scheduler. +/// A missing repository is a no-op. Repository lookup and final adapter +/// construction errors reach the caller. Directive, suggestion, reranking, +/// coverage lookup and posting failures are handled locally. Failed inline +/// review comments fall back to general PR comments. async fn report_to_platform( store: Arc, echidna: &EchidnaClient, @@ -852,6 +867,7 @@ async fn report_to_platform( artifacts: vec![], confidence: job_result.confidence.clone(), axioms: job_result.axioms.clone(), + trust_source: job_result.trust_source, }; // Tactic suggestions for Advisor / Consultant / Regulator. Verifier @@ -1177,6 +1193,52 @@ async fn record_feedback( } } +/// Minimum-version handshake at start-up. +/// +/// Propagates `Error::EchidnaIncompatible` and converts all other handshake +/// errors to success, allowing start-up to continue. Delegated REST jobs +/// retry when no successful handshake is cached (see `process_job`). +/// GraphQL-only deployments skip the REST handshake. +async fn startup_handshake(echidna: &EchidnaClient) -> Result<()> { + if !echidna.uses_rest() { + tracing::info!("ECHIDNA mode is graphql: REST version handshake skipped"); + return Ok(()); + } + match echidna.handshake().await { + Ok(h) => { + tracing::info!( + "ECHIDNA {} handshake ok ({} provers listed; minimum {})", + h.version, + h.provers.len(), + echidnabot::dispatcher::MIN_ECHIDNA_VERSION + ); + Ok(()) + } + Err(echidnabot::Error::EchidnaIncompatible(msg)) => Err( + echidnabot::Error::EchidnaIncompatible(format!("ECHIDNA handshake failed: {msg}")), + ), + Err(other) => { + tracing::warn!( + "ECHIDNA not reachable at start-up ({other}); jobs will retry the handshake" + ); + Ok(()) + } + } +} + +/// Run one proof job and aggregate file verdicts, axioms and confidence. +/// +/// Checks ECHIDNA health and prover availability even for local execution; +/// delegated REST jobs also ensure a cached version handshake. Clones the +/// requested revision, discovers proof files when none were supplied and +/// stores the discovered paths. Duration includes these steps, in milliseconds. +/// No proof files yields an unsuccessful result without trust data. +/// +/// Propagates database, checkout, file-reading and ECHIDNA errors, and returns +/// a configuration error if local isolation has no available backend. Local +/// execution errors become failed file verdicts. File-discovery task failures +/// become an empty file list. Confidence is computed locally; trust provenance +/// is `Echidna` only when every delegated result reports that provenance. async fn process_job( job: &ProofJob, store: &dyn Store, @@ -1190,6 +1252,9 @@ async fn process_job( "ECHIDNA core reported unhealthy status".to_string(), )); } + if !config.executor.local_isolation && echidna.uses_rest() { + echidna.ensure_handshake().await?; + } let status = echidna.prover_status(&job.prover).await?; if status != ProverStatus::Available { @@ -1243,6 +1308,7 @@ async fn process_job( failed_files: vec![], confidence: None, axioms: None, + trust_source: echidnabot::dispatcher::TrustSource::LocalFallback, }); } @@ -1251,6 +1317,11 @@ async fn process_job( let mut verified = Vec::new(); let mut failed = Vec::new(); let mut prover_output = String::new(); + // Source-level axiom scan (ECHIDNA's canonical scanner) over every file, + // merged with whatever ECHIDNA itself reported per file. + let mut source_axioms: Option = None; + // `Echidna` only if ECHIDNA reported trust for every file it verified. + let mut all_trust_from_echidna = true; // Build the local sandboxed executor once (only when configured). // When `executor.local_isolation = false` (default), proofs delegate @@ -1297,6 +1368,12 @@ async fn process_job( repo_path.join(path) }; let content = fs::read_to_string(&full_path).await?; + let file_axioms = + echidnabot::trust::axiom_tracker::AxiomTracker::scan_source(&job.prover, &content); + source_axioms = Some(match source_axioms.take() { + Some(acc) => acc.merge(file_axioms), + None => file_axioms, + }); let (verified_ok, output_chunk) = if let Some(ref ex) = local_executor { // Local sandboxed path. ExecutionResult is success on @@ -1318,6 +1395,15 @@ async fn process_job( } else { // ECHIDNA-delegated path (default). let result = echidna.verify_proof(&job.prover, &content).await?; + if result.trust_source != echidnabot::dispatcher::TrustSource::Echidna { + all_trust_from_echidna = false; + } + if let Some(reported) = result.axioms { + source_axioms = Some(match source_axioms.take() { + Some(acc) => acc.merge(reported), + None => reported, + }); + } ( result.status == echidnabot::dispatcher::ProofStatus::Verified, result.prover_output, @@ -1349,9 +1435,26 @@ async fn process_job( } else { echidnabot::dispatcher::ProofStatus::Failed }; - let axioms = echidnabot::trust::axiom_tracker::AxiomTracker::scan(&job.prover, &prover_output); - let confidence = - echidnabot::trust::confidence::assess_confidence(&job.prover, final_status, false, 1); + let output_axioms = + echidnabot::trust::axiom_tracker::AxiomTracker::scan(&job.prover, &prover_output); + let axioms = match source_axioms { + Some(src) => src.merge(output_axioms), + None => output_axioms, + }; + let confidence = echidnabot::trust::confidence::assess_confidence_with_axioms( + &job.prover, + final_status, + false, + 1, + axioms.worst_danger, + ); + // The level is always computed by ECHIDNA's trust kernel (linked in); + // `Echidna` here means every file's axiom data was reported by ECHIDNA. + let trust_source = if local_executor.is_none() && all_trust_from_echidna { + echidnabot::dispatcher::TrustSource::Echidna + } else { + echidnabot::dispatcher::TrustSource::LocalFallback + }; Ok(echidnabot::scheduler::JobResult { success, message, @@ -1361,6 +1464,7 @@ async fn process_job( failed_files: failed, confidence: Some(confidence), axioms: Some(axioms), + trust_source, }) } diff --git a/bots/echidnabot/src/observability.rs b/bots/echidnabot/src/observability.rs index adc8f01e..8c8eb9f3 100644 --- a/bots/echidnabot/src/observability.rs +++ b/bots/echidnabot/src/observability.rs @@ -420,8 +420,11 @@ mod tests { hook().await; } - #[test] - fn into_coordinator_hook_drains_provider_idempotent_with_shutdown() { + /// After `into_coordinator_hook` takes the provider, `shutdown` is a no-op. + /// Runs inside a Tokio runtime: building the tonic exporter needs a + /// reactor since the hyper-util 0.1.20 / tracing-opentelemetry 0.34 bump. + #[tokio::test] + async fn into_coordinator_hook_drains_provider_idempotent_with_shutdown() { // Idempotency contract: after into_coordinator_hook() has taken // the provider, calling shutdown() consumes self without // touching anything (provider is None, branch elided). diff --git a/bots/echidnabot/src/result_formatter.rs b/bots/echidnabot/src/result_formatter.rs index 3167ea31..dd3ac56b 100644 --- a/bots/echidnabot/src/result_formatter.rs +++ b/bots/echidnabot/src/result_formatter.rs @@ -153,6 +153,7 @@ mod tests { artifacts: vec![], confidence: None, axioms: None, + trust_source: Default::default(), } } @@ -165,6 +166,7 @@ mod tests { artifacts: vec![], confidence: None, axioms: None, + trust_source: Default::default(), } } diff --git a/bots/echidnabot/src/scheduler/job_queue.rs b/bots/echidnabot/src/scheduler/job_queue.rs index 570f9939..28cb505f 100644 --- a/bots/echidnabot/src/scheduler/job_queue.rs +++ b/bots/echidnabot/src/scheduler/job_queue.rs @@ -282,14 +282,14 @@ mod tests { let scheduler = JobScheduler::new(2, 10); let job1 = ProofJob::new( - Uuid::new_v4(), + crate::ids::new_record_id(), "abc123".to_string(), ProverKind::new("metamath"), vec!["test.mm".to_string()], ); let job2 = ProofJob::new( - Uuid::new_v4(), + crate::ids::new_record_id(), "def456".to_string(), ProverKind::new("metamath"), vec!["test2.mm".to_string()], @@ -313,7 +313,7 @@ mod tests { #[tokio::test] async fn test_duplicate_detection() { let scheduler = JobScheduler::new(2, 10); - let repo_id = Uuid::new_v4(); + let repo_id = crate::ids::new_record_id(); let job1 = ProofJob::new( repo_id, @@ -339,7 +339,7 @@ mod tests { #[tokio::test] async fn test_priority_ordering() { let scheduler = JobScheduler::new(1, 10); - let repo_id = Uuid::new_v4(); + let repo_id = crate::ids::new_record_id(); let low_priority = ProofJob::new( repo_id, diff --git a/bots/echidnabot/src/scheduler/mod.rs b/bots/echidnabot/src/scheduler/mod.rs index d4485d07..ff853726 100644 --- a/bots/echidnabot/src/scheduler/mod.rs +++ b/bots/echidnabot/src/scheduler/mod.rs @@ -25,8 +25,9 @@ use crate::trust::{axiom_tracker::AxiomReport, confidence::ConfidenceReport}; pub struct JobId(pub Uuid); impl JobId { + /// Mint a fresh job id (UUIDv7 via [`crate::ids::new_record_id`]). pub fn new() -> Self { - Self(Uuid::new_v4()) + Self(crate::ids::new_record_id()) } } @@ -167,7 +168,10 @@ pub struct JobResult { /// Confidence level assessed over the aggregated prover output. #[serde(default)] pub confidence: Option, - /// Axiom usage flags found in the aggregated prover output. + /// Axiom usage flags found in the proof sources and prover output. #[serde(default)] pub axioms: Option, + /// Provenance of `confidence` / `axioms`. + #[serde(default)] + pub trust_source: crate::dispatcher::TrustSource, } diff --git a/bots/echidnabot/src/store/mod.rs b/bots/echidnabot/src/store/mod.rs index b26a8195..11a77fe5 100644 --- a/bots/echidnabot/src/store/mod.rs +++ b/bots/echidnabot/src/store/mod.rs @@ -15,7 +15,9 @@ use crate::adapters::Platform; use crate::dispatcher::ProverKind; use crate::error::Result; use crate::scheduler::JobId; -use models::{ProofJobRecord, ProofResultRecord, Repository, TacticOutcomeRecord}; +use models::{ + ProofJobRecord, ProofObligationRecord, ProofResultRecord, Repository, TacticOutcomeRecord, +}; /// Per-commit coverage view — total proof attempts vs successful ones. /// Empty results means no jobs run yet for that commit. @@ -86,6 +88,13 @@ pub trait Store: Send + Sync { limit: usize, ) -> Result>; + // Proof obligations (submitProofObligation) + /// Persist an obligation; returns `false` if one with the same content id + /// already existed (resubmission is idempotent, the first row is kept). + async fn record_proof_obligation(&self, obligation: &ProofObligationRecord) -> Result; + /// Fetch one obligation by its content id. + async fn get_proof_obligation(&self, id: Uuid) -> Result>; + // Utility async fn health_check(&self) -> Result; } diff --git a/bots/echidnabot/src/store/models.rs b/bots/echidnabot/src/store/models.rs index e67475f3..c32d5675 100644 --- a/bots/echidnabot/src/store/models.rs +++ b/bots/echidnabot/src/store/models.rs @@ -13,7 +13,7 @@ use crate::modes::BotMode; use crate::scheduler::{JobId, JobPriority, JobStatus}; /// Repository record -#[derive(Debug, Clone, Serialize, Deserialize)] +#[derive(Clone, Serialize, Deserialize)] pub struct Repository { pub id: Uuid, pub platform: Platform, @@ -43,15 +43,45 @@ pub struct Repository { pub regulator_coverage_threshold: u8, } +impl std::fmt::Debug for Repository { + /// Debug output with `webhook_secret` redacted (log-leak guard). + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + f.debug_struct("Repository") + .field("id", &self.id) + .field("platform", &self.platform) + .field("owner", &self.owner) + .field("name", &self.name) + .field( + "webhook_secret", + &crate::config::redacted(&self.webhook_secret), + ) + .field("enabled_provers", &self.enabled_provers) + .field("check_on_push", &self.check_on_push) + .field("check_on_pr", &self.check_on_pr) + .field("auto_comment", &self.auto_comment) + .field("enabled", &self.enabled) + .field("last_checked_commit", &self.last_checked_commit) + .field("created_at", &self.created_at) + .field("updated_at", &self.updated_at) + .field("mode", &self.mode) + .field( + "regulator_coverage_threshold", + &self.regulator_coverage_threshold, + ) + .finish() + } +} + fn default_regulator_threshold() -> u8 { 100 } impl Repository { + /// New repository record with defaults and a fresh UUIDv7 id. pub fn new(platform: Platform, owner: String, name: String) -> Self { let now = Utc::now(); Self { - id: Uuid::new_v4(), + id: crate::ids::new_record_id(), platform, owner, name, @@ -136,9 +166,10 @@ pub struct ProofResultRecord { } impl ProofResultRecord { + /// Persistable record of a job result, with a fresh UUIDv7 id. pub fn new(job_id: JobId, result: &crate::scheduler::JobResult) -> Self { Self { - id: Uuid::new_v4(), + id: crate::ids::new_record_id(), job_id: job_id.0, success: result.success, message: result.message.clone(), @@ -180,6 +211,7 @@ pub struct TacticOutcomeRecord { } impl TacticOutcomeRecord { + /// Record of one tactic attempt, with a fresh UUIDv7 id. pub fn new( job_id: Option, prover: ProverKind, @@ -189,7 +221,7 @@ impl TacticOutcomeRecord { duration_ms: i64, ) -> Self { Self { - id: Uuid::new_v4(), + id: crate::ids::new_record_id(), job_id, prover, goal_fingerprint, @@ -243,3 +275,57 @@ mod tests { assert_eq!(goal_fingerprint("any").len(), 64); } } + +/// A proof obligation submitted over GraphQL (`submitProofObligation`). +/// +/// Obligations come from hypatia's FleetDispatcher and LearningScheduler as +/// free-standing claim text: no commit and no file, and the repo is a slug +/// that need not be registered here. That is why this is its own record rather +/// than a [`ProofJobRecord`], whose `repo_id` must be a registered repository. +/// +/// The id is a UUIDv8 *content* id over `{repo, claim, context, prover}`, so +/// resubmitting the same obligation yields the same id. Nothing consumes +/// stored obligations yet: `status` stays `PENDING` until a dispatcher exists. +#[derive(Debug, Clone, Serialize, Deserialize)] +pub struct ProofObligationRecord { + pub id: Uuid, + pub repo_slug: String, + pub repo_id: Option, + pub claim: String, + pub context: String, + pub prover: Option, + pub inline_requested: bool, + pub status: String, + pub created_at: DateTime, +} + +impl ProofObligationRecord { + /// New `PENDING` obligation whose id is the content id of its fields. + pub fn new( + repo_slug: String, + repo_id: Option, + claim: String, + context: String, + prover: Option, + inline_requested: bool, + ) -> Self { + let id = crate::ids::content_id(&serde_json::json!({ + "repo": repo_slug, + "claim": claim, + "context": context, + "prover": prover.as_ref().map(|p| p.to_string()), + })) + .unwrap_or_else(|_| Uuid::nil()); + Self { + id, + repo_slug, + repo_id, + claim, + context, + prover, + inline_requested, + status: "PENDING".to_string(), + created_at: Utc::now(), + } + } +} diff --git a/bots/echidnabot/src/store/sqlite.rs b/bots/echidnabot/src/store/sqlite.rs index 9821bccc..8cb699be 100644 --- a/bots/echidnabot/src/store/sqlite.rs +++ b/bots/echidnabot/src/store/sqlite.rs @@ -195,6 +195,26 @@ impl SqliteStore { .execute(&self.pool) .await?; + // Proof obligations from `submitProofObligation`. `repo_id` is nullable: + // the sender names a repo slug that need not be registered here. + sqlx::query( + r#" + CREATE TABLE IF NOT EXISTS proof_obligations ( + id TEXT PRIMARY KEY, + repo_slug TEXT NOT NULL, + repo_id TEXT REFERENCES repositories(id), + claim TEXT NOT NULL, + context TEXT NOT NULL, + prover TEXT, + inline_requested INTEGER NOT NULL, + status TEXT NOT NULL, + created_at TEXT NOT NULL + ) + "#, + ) + .execute(&self.pool) + .await?; + Ok(()) } } @@ -540,6 +560,42 @@ impl Store for SqliteStore { rows.into_iter().map(|r| r.try_into()).collect() } + /// Insert-or-ignore on the content id; `true` only for a new row. + async fn record_proof_obligation(&self, obligation: &ProofObligationRecord) -> Result { + let done = sqlx::query( + r#" + INSERT OR IGNORE INTO proof_obligations ( + id, repo_slug, repo_id, claim, context, prover, + inline_requested, status, created_at + ) VALUES (?, ?, ?, ?, ?, ?, ?, ?, ?) + "#, + ) + .bind(obligation.id.to_string()) + .bind(&obligation.repo_slug) + .bind(obligation.repo_id.map(|id| id.to_string())) + .bind(&obligation.claim) + .bind(&obligation.context) + .bind(obligation.prover.as_ref().map(|p| p.to_string())) + .bind(obligation.inline_requested) + .bind(&obligation.status) + .bind(obligation.created_at.to_rfc3339()) + .execute(&self.pool) + .await?; + + Ok(done.rows_affected() == 1) + } + + /// Look up one obligation by content id. + async fn get_proof_obligation(&self, id: Uuid) -> Result> { + let row: Option = + sqlx::query_as("SELECT * FROM proof_obligations WHERE id = ?") + .bind(id.to_string()) + .fetch_optional(&self.pool) + .await?; + + row.map(|r| r.try_into()).transpose() + } + async fn health_check(&self) -> Result { let result: (i32,) = sqlx::query_as("SELECT 1").fetch_one(&self.pool).await?; Ok(result.0 == 1) @@ -778,6 +834,41 @@ impl TryFrom for TacticOutcomeRecord { } } +#[derive(sqlx::FromRow)] +struct ObligationRow { + id: String, + repo_slug: String, + repo_id: Option, + claim: String, + context: String, + prover: Option, + inline_requested: bool, + status: String, + created_at: String, +} + +impl TryFrom for ProofObligationRecord { + type Error = Error; + + /// Decode a stored row; the prover column holds the slug (`Display`). + fn try_from(row: ObligationRow) -> Result { + let parse = |s: &str| Uuid::parse_str(s).map_err(|e| Error::Internal(e.to_string())); + Ok(ProofObligationRecord { + id: parse(&row.id)?, + repo_slug: row.repo_slug, + repo_id: row.repo_id.as_deref().map(parse).transpose()?, + claim: row.claim, + context: row.context, + prover: row.prover.map(|s| ProverKind::new(s.as_str())), + inline_requested: row.inline_requested, + status: row.status, + created_at: chrono::DateTime::parse_from_rfc3339(&row.created_at) + .map_err(|e| Error::Internal(e.to_string()))? + .with_timezone(&chrono::Utc), + }) + } +} + fn parse_prover(s: &str) -> Result { match s { "Agda" => Ok(ProverKind::new("agda")), @@ -802,8 +893,10 @@ mod tests { use crate::store::models::{goal_fingerprint, TacticOutcomeRecord}; async fn fresh_store() -> (SqliteStore, std::path::PathBuf) { - let path = - std::env::temp_dir().join(format!("echidnabot-store-test-{}.db", Uuid::new_v4())); + let path = std::env::temp_dir().join(format!( + "echidnabot-store-test-{}.db", + crate::ids::new_record_id() + )); let url = format!("sqlite://{}?mode=rwc", path.display()); let store = SqliteStore::new(&url).await.expect("open store"); (store, path) @@ -931,4 +1024,31 @@ mod tests { let _ = std::fs::remove_file(&path); } + + #[tokio::test] + async fn proof_obligation_round_trips_and_resubmission_is_idempotent() { + use crate::store::models::ProofObligationRecord; + let (store, path) = fresh_store().await; + + let ob = ProofObligationRecord::new( + "hyperpolymath/requeue".into(), + None, + "requeue-of-1".into(), + "strategy-shift".into(), + Some(ProverKind::new("hol-light")), + true, + ); + assert_eq!(ob.id.get_version_num(), 8); + assert!(store.record_proof_obligation(&ob).await.unwrap()); + assert!(!store.record_proof_obligation(&ob).await.unwrap()); + + let back = store.get_proof_obligation(ob.id).await.unwrap().unwrap(); + assert_eq!(back.claim, "requeue-of-1"); + assert_eq!(back.prover, Some(ProverKind::new("hol-light"))); + assert!(back.inline_requested); + assert_eq!(back.status, "PENDING"); + assert!(back.repo_id.is_none()); + + let _ = std::fs::remove_file(&path); + } } diff --git a/bots/echidnabot/src/trust/axiom_tracker.rs b/bots/echidnabot/src/trust/axiom_tracker.rs index 43657d95..92de0121 100644 --- a/bots/echidnabot/src/trust/axiom_tracker.rs +++ b/bots/echidnabot/src/trust/axiom_tracker.rs @@ -15,7 +15,20 @@ //! - `axiom` (Lean4) -- user-declared axiom //! - `assume` (Metamath) -- hypothesis without proof //! - Classical logic axioms (excluded middle, double negation elimination) - +//! +//! Two scanners live here and they read different things: +//! +//! - [`AxiomTracker::scan_source`] reads the **proof source** and delegates to +//! ECHIDNA's canonical scanner (`echidna_core_spark::axiom_tracker`), which +//! skips comment lines and ECHIDNA's own scaffold markers. This is the +//! primary signal and is shared with ECHIDNA, not re-implemented. +//! - [`AxiomTracker::scan`] reads the **prover's output text** (for example +//! Lean's "declaration uses 'sorry'"). ECHIDNA has no equivalent, so this +//! stays local, as a fallback for when the source is unavailable. + +use echidna_core_spark::axiom_tracker::{ + AxiomTracker as EchidnaAxiomTracker, AxiomUsage, DangerLevel, +}; use serde::{Deserialize, Serialize}; use crate::dispatcher::ProverKind; @@ -79,6 +92,46 @@ impl AxiomFlag { pub fn is_unsound(&self) -> bool { self.severity() >= 3 } + + /// The ECHIDNA danger level this flag corresponds to. + /// + /// `--type-in-type` can manufacture false theorems, so it is `Reject`; + /// `Sorry`, `Admitted`, `Oops` and `Postulate` are `Warning`; + /// everything else is `Noted`. + pub fn danger_level(&self) -> DangerLevel { + match self { + Self::TypeInType => DangerLevel::Reject, + Self::Sorry | Self::Admitted | Self::Oops | Self::Postulate => DangerLevel::Warning, + _ => DangerLevel::Noted, + } + } + + /// Map one ECHIDNA source-scan finding onto the local flag vocabulary. + fn from_usage(usage: &AxiomUsage) -> Self { + Self::from_name(&usage.construct) + } + + /// Map an axiom / construct name onto the local flag vocabulary. + /// + /// Used for both ECHIDNA source-scan findings and the names ECHIDNA + /// reports in `echidna.prove.result/1` `trust.axioms` (which may use the + /// kernel names, e.g. Lean's `sorryAx` from `#print axioms`). + /// Surrounding whitespace is trimmed; unrecognised names become `Other`. + pub fn from_name(name: &str) -> Self { + match name.trim() { + "sorry" | "sorryAx" => Self::Sorry, + "Admitted" | "admit" | "admitted" => Self::Admitted, + "postulate" | "{!!}" => Self::Postulate, + "believe_me" | "assert_total" | "idris_crash" => Self::Postulate, + "--type-in-type" | "OPTIONS --type-in-type" | "type-in-type" => Self::TypeInType, + "oops" => Self::Oops, + "axiom" | "Axiom" => Self::UserAxiom, + "assume" => Self::UndischargedAssumption, + "Classical.choice" | "choice" => Self::AxiomOfChoice, + "Classical.em" | "propext" | "Quot.sound" | "excluded_middle" => Self::ClassicalAxiom, + other => Self::Other(other.to_string()), + } + } } impl std::fmt::Display for AxiomFlag { @@ -100,6 +153,15 @@ pub struct AxiomReport { pub warning_count: usize, /// Overall assessment pub clean: bool, + /// Worst ECHIDNA danger level found, the input to the trust kernel. + /// Older stored reports lack the field and deserialise as `Safe`. + #[serde(default = "safe")] + pub worst_danger: DangerLevel, +} + +/// Serde default for [`AxiomReport::worst_danger`]. +fn safe() -> DangerLevel { + DangerLevel::Safe } impl AxiomReport { @@ -116,6 +178,51 @@ impl AxiomReport { .collect() } + /// Combine two reports on the same proof (for example a source scan and + /// an output scan): the union of the flags and the worse danger level. + /// Retains this report's prover without checking that the other matches, + /// deduplicates flags and recalculates counts. + pub fn merge(mut self, other: AxiomReport) -> AxiomReport { + let worst = DangerLevel::max_danger(self.worst_danger, other.worst_danger); + self.flags.extend(other.flags); + let mut report = AxiomReport::from_flags(self.prover, self.flags); + report.worst_danger = DangerLevel::max_danger(report.worst_danger, worst); + report + } + + /// Build a report from axiom names ECHIDNA reported (the + /// `echidna.prove.result/1` `trust.axioms` list). + pub fn from_reported(prover: ProverKind, flags: impl IntoIterator) -> Self { + AxiomReport::from_flags(prover, flags.into_iter().collect()) + } + + /// Build a report from raw flags, deduplicating and counting them. + fn from_flags(prover: ProverKind, mut flags: Vec) -> AxiomReport { + // Sort by severity, then by identity, so equal flags are adjacent and + // `dedup` removes every duplicate (not only neighbouring ones). + flags.sort_by(|a, b| { + b.severity() + .cmp(&a.severity()) + .then_with(|| a.description().cmp(&b.description())) + }); + flags.dedup(); + let unsound_count = flags.iter().filter(|f| f.severity() >= 3).count(); + let warning_count = flags.iter().filter(|f| f.severity() == 2).count(); + let clean = flags.is_empty(); + let worst_danger = flags + .iter() + .map(AxiomFlag::danger_level) + .fold(DangerLevel::Safe, DangerLevel::max_danger); + AxiomReport { + prover, + flags, + unsound_count, + warning_count, + clean, + worst_danger, + } + } + /// Format as a human-readable summary pub fn summary(&self) -> String { if self.clean { @@ -166,21 +273,34 @@ impl AxiomTracker { // Universal patterns (apply to all provers) scan_universal(&output_lower, &mut flags); - // Deduplicate flags - flags.sort_by_key(|f| std::cmp::Reverse(f.severity())); - flags.dedup(); + AxiomReport::from_flags(prover.clone(), flags) + } - let unsound_count = flags.iter().filter(|f| f.severity() >= 3).count(); - let warning_count = flags.iter().filter(|f| f.severity() == 2).count(); - let clean = flags.is_empty(); + /// Scan proof **source** with ECHIDNA's canonical axiom scanner. + /// + /// Provers ECHIDNA has no pattern table for yield a clean report; the + /// slug is normalised (`hol-light` → `hollight`, `lean4` → `lean`) to + /// ECHIDNA's keys first. + pub fn scan_source(prover: &ProverKind, source: &str) -> AxiomReport { + let usages = EchidnaAxiomTracker::new().scan(&echidna_scanner_key(prover), source); + let flags = usages.iter().map(AxiomFlag::from_usage).collect(); + let mut report = AxiomReport::from_flags(prover.clone(), flags); + report.worst_danger = usages + .iter() + .map(|u| u.danger_level) + .fold(report.worst_danger, DangerLevel::max_danger); + report + } +} - AxiomReport { - prover: prover.clone(), - flags, - unsound_count, - warning_count, - clean, - } +/// ECHIDNA's scanner-table key for an echidnabot prover slug. +fn echidna_scanner_key(prover: &ProverKind) -> String { + match prover.as_str() { + "lean4" => "lean".to_string(), + "rocq" => "coq".to_string(), + "idris" => "idris2".to_string(), + "f*" | "f-star" => "fstar".to_string(), + other => other.replace(['-', '_'], ""), } } @@ -408,4 +528,65 @@ mod tests { let warnings = report.flags_at_severity(2); assert!(warnings.len() >= 2); // sorry + axiom } + + #[test] + fn test_source_scan_uses_echidna_patterns() { + let report = AxiomTracker::scan_source( + &ProverKind::new("lean"), + "theorem t : 1 = 1 := by\n sorry\n", + ); + assert!(report.flags.contains(&AxiomFlag::Sorry)); + assert_eq!(report.worst_danger, DangerLevel::Warning); + } + + #[test] + fn test_source_scan_skips_comments_and_scaffold() { + let report = AxiomTracker::scan_source( + &ProverKind::new("lean"), + "-- sorry in a comment is documentation\ntheorem t : True := trivial\n", + ); + assert!(report.clean, "{:?}", report.flags); + assert_eq!(report.worst_danger, DangerLevel::Safe); + } + + #[test] + fn test_source_scan_idris_believe_me_is_reject() { + let report = AxiomTracker::scan_source(&ProverKind::new("idris2"), "f = believe_me x\n"); + assert_eq!(report.worst_danger, DangerLevel::Reject); + } + + #[test] + fn test_from_flags_dedups_non_adjacent_duplicates() { + let report = AxiomReport::from_reported( + ProverKind::new("lean"), + [ + AxiomFlag::Sorry, + AxiomFlag::Admitted, + AxiomFlag::Sorry, + AxiomFlag::Other("x".into()), + AxiomFlag::AxiomOfChoice, + AxiomFlag::Other("x".into()), + ], + ); + assert_eq!(report.flags.len(), 4, "{:?}", report.flags); + } + + #[test] + fn test_from_name_maps_kernel_names() { + assert_eq!(AxiomFlag::from_name("sorryAx"), AxiomFlag::Sorry); + assert_eq!( + AxiomFlag::from_name("believe_me").danger_level(), + DangerLevel::Warning + ); + assert_eq!(AxiomFlag::from_name("propext"), AxiomFlag::ClassicalAxiom); + } + + #[test] + fn test_merge_keeps_worst_danger() { + let output = AxiomTracker::scan(&ProverKind::new("lean"), "All goals discharged"); + let source = AxiomTracker::scan_source(&ProverKind::new("lean"), " sorry\n"); + let merged = output.merge(source); + assert!(merged.has_unsound()); + assert_eq!(merged.worst_danger, DangerLevel::Warning); + } } diff --git a/bots/echidnabot/src/trust/confidence.rs b/bots/echidnabot/src/trust/confidence.rs index 89864410..5b350f05 100644 --- a/bots/echidnabot/src/trust/confidence.rs +++ b/bots/echidnabot/src/trust/confidence.rs @@ -3,30 +3,40 @@ // SPDX-FileCopyrightText: 2025 Jonathan D.A. Jewell //! Proof confidence level assessment //! -//! Maps ECHIDNA verification results to a 5-level trust scale based on: -//! - Prover kernel size (small-kernel = higher trust) -//! - Number of independent checkers used -//! - Presence of proof certificates -//! - Prover tier within ECHIDNA - +//! The trust-level *algorithm* is ECHIDNA's, not echidnabot's: every call +//! goes through [`echidna_core_spark::compute_trust_level`] (the Creusot- +//! annotated kernel shared with ECHIDNA). This module only translates +//! echidnabot's inputs (prover slug, status, artefacts, axiom scan) into +//! ECHIDNA's [`TrustFactors`] and wraps the answer in a report. +//! +//! Epistemic note (pattern from `hyperpolymath/epistemic-types`, not a +//! dependency): a level computed here is a *warrant* — echidnabot's own +//! reading of ECHIDNA's output. When ECHIDNA itself supplies trust data in an +//! `echidna.prove.result/1` object, that is the *receipt* and is preferred; +//! see [`crate::dispatcher::TrustSource`]. + +use echidna_core_spark::axiom_tracker::DangerLevel; +use echidna_core_spark::{compute_trust_level, ProverClass, TrustFactors, TrustLevel}; use serde::{Deserialize, Serialize}; use crate::dispatcher::{ProofStatus, ProverKind}; /// Confidence level for a proof verification result. /// -/// Higher levels indicate stronger trust in the result. +/// Mirrors ECHIDNA's [`TrustLevel`] one-to-one (see the `From` impls); it is +/// kept as a local type only so echidnabot can attach presentation methods +/// (`label`, `Display`) to it. #[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] pub enum ConfidenceLevel { - /// Large-TCB system or unchecked result + /// Large-TCB system, unchecked result, or dangerous axioms present Level1 = 1, - /// Single prover result without certificate + /// Single prover result without a verified certificate Level2 = 2, - /// Single prover with proof certificate (Alethe, DRAT/LRAT) + /// Verified certificate, or cross-checked by 2+ provers Level3 = 3, - /// Checked by small-kernel system (Lean4, Coq, Isabelle) with certificate + /// Small-kernel system with a verified certificate Level4 = 4, - /// Cross-checked by 2+ independent small-kernel systems + /// Cross-checked by 2+ small-kernel systems with verified certificates Level5 = 5, } @@ -39,11 +49,11 @@ impl ConfidenceLevel { /// Human-readable label pub fn label(&self) -> &'static str { match self { - Self::Level1 => "Minimal (large-TCB / unchecked)", - Self::Level2 => "Low (single prover, no certificate)", - Self::Level3 => "Moderate (single prover + certificate)", - Self::Level4 => "High (small-kernel + certificate)", - Self::Level5 => "Maximum (cross-checked by 2+ systems)", + Self::Level1 => "Minimal (large-TCB / unchecked / dangerous axioms)", + Self::Level2 => "Low (single prover, no verified certificate)", + Self::Level3 => "Moderate (verified certificate or cross-checked)", + Self::Level4 => "High (small-kernel + verified certificate)", + Self::Level5 => "Maximum (cross-checked by 2+ small-kernel systems)", } } @@ -53,7 +63,34 @@ impl ConfidenceLevel { } } +impl From for ConfidenceLevel { + /// Translate ECHIDNA's trust level into the local presentation type. + fn from(level: TrustLevel) -> Self { + match level { + TrustLevel::Level1 => Self::Level1, + TrustLevel::Level2 => Self::Level2, + TrustLevel::Level3 => Self::Level3, + TrustLevel::Level4 => Self::Level4, + TrustLevel::Level5 => Self::Level5, + } + } +} + +impl From for TrustLevel { + /// Translate the local presentation type back into ECHIDNA's trust level. + fn from(level: ConfidenceLevel) -> Self { + match level { + ConfidenceLevel::Level1 => Self::Level1, + ConfidenceLevel::Level2 => Self::Level2, + ConfidenceLevel::Level3 => Self::Level3, + ConfidenceLevel::Level4 => Self::Level4, + ConfidenceLevel::Level5 => Self::Level5, + } + } +} + impl std::fmt::Display for ConfidenceLevel { + /// Render as `Level N (label)`. fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { write!(f, "Level {} ({})", self.value(), self.label()) } @@ -76,7 +113,10 @@ pub struct ConfidenceReport { pub justification: String, } -/// Assess the confidence level of a proof verification result. +/// Assess the confidence level of a proof verification result with no +/// axiom information (treated as no dangerous axioms found). +/// +/// Prefer [`assess_confidence_with_axioms`] whenever an axiom scan exists. /// /// # Arguments /// * `prover` - Which prover produced the result @@ -89,6 +129,37 @@ pub fn assess_confidence( has_certificate: bool, checker_count: usize, ) -> ConfidenceReport { + assess_confidence_with_axioms( + prover, + status, + has_certificate, + checker_count, + DangerLevel::Safe, + ) +} + +/// Assess the confidence level of a proof result using ECHIDNA's canonical +/// trust algorithm. +/// +/// echidnabot never verifies certificates itself, so `certificate_verified` +/// is always passed as `false`: a certificate artefact raises nothing above +/// Level 2 on its own. Solver integrity is checked elsewhere +/// ([`crate::trust::SolverIntegrity`]) and is assumed here. +/// +/// `checker_count` is the number of independent checkers that confirmed the +/// result; values above `u32::MAX` are capped for assessment but retained in +/// the report. `worst_axiom_danger` is the highest danger found in the proof. +/// A status other than `Verified` returns Level 1 with no certificate and +/// zero checkers, regardless of the supplied values. +pub fn assess_confidence_with_axioms( + prover: &ProverKind, + status: ProofStatus, + has_certificate: bool, + checker_count: usize, + worst_axiom_danger: DangerLevel, +) -> ConfidenceReport { + let small_kernel = is_small_kernel(prover); + // Only verified proofs get meaningful confidence levels if status != ProofStatus::Verified { return ConfidenceReport { @@ -96,7 +167,7 @@ pub fn assess_confidence( prover: prover.clone(), has_certificate: false, checker_count: 0, - small_kernel: is_small_kernel(prover), + small_kernel, justification: format!( "Proof status is {:?} (not Verified) -- confidence is minimal", status @@ -104,83 +175,48 @@ pub fn assess_confidence( }; } - let small_kernel = is_small_kernel(prover); - - // Level 5: Cross-checked by 2+ independent small-kernel systems - if checker_count >= 2 && small_kernel { - return ConfidenceReport { - level: ConfidenceLevel::Level5, - prover: prover.clone(), - has_certificate, - checker_count, - small_kernel, - justification: format!( - "Cross-checked by {} independent small-kernel systems ({})", - checker_count, - prover.display_name() - ), - }; - } - - // Level 4: Small-kernel system with certificate - if small_kernel && has_certificate { - return ConfidenceReport { - level: ConfidenceLevel::Level4, - prover: prover.clone(), - has_certificate, - checker_count, - small_kernel, - justification: format!( - "Verified by small-kernel system ({}) with proof certificate", - prover.display_name() - ), - }; - } - - // Level 3: Single prover with proof certificate (e.g., Z3 with DRAT/LRAT) - if has_certificate { - return ConfidenceReport { - level: ConfidenceLevel::Level3, - prover: prover.clone(), - has_certificate, - checker_count, - small_kernel, - justification: format!( - "Verified by {} with proof certificate", - prover.display_name() - ), - }; - } + let factors = TrustFactors { + prover_class: prover_class(prover), + confirming_provers: u32::try_from(checker_count).unwrap_or(u32::MAX), + has_certificate, + certificate_verified: false, + worst_axiom_danger, + solver_integrity_ok: true, + }; + let level = ConfidenceLevel::from(compute_trust_level(&factors)); - // Level 2: Single prover without certificate but with small kernel - if small_kernel { - return ConfidenceReport { - level: ConfidenceLevel::Level2, - prover: prover.clone(), - has_certificate, - checker_count, - small_kernel, - justification: format!( - "Verified by small-kernel system ({}) without proof certificate", - prover.display_name() - ), - }; - } - - // Level 1: Large-TCB or stub prover ConfidenceReport { - level: ConfidenceLevel::Level1, + level, prover: prover.clone(), - has_certificate: false, + has_certificate, checker_count, - small_kernel: false, + small_kernel, justification: format!( - "Verified by large-TCB system ({}) -- consider cross-checking", - prover.display_name() + "ECHIDNA trust kernel: {} ({}, {} checker(s), certificate {}, worst axiom danger {})", + TrustLevel::from(level).description(), + prover.display_name(), + checker_count, + if has_certificate { + "present but not independently verified" + } else { + "absent" + }, + worst_axiom_danger ), } } +/// Classify a prover slug into ECHIDNA's coarse [`ProverClass`]. +pub fn prover_class(prover: &ProverKind) -> ProverClass { + if is_small_kernel(prover) { + return ProverClass::SmallKernel; + } + match prover.as_str() { + "z3" | "cvc5" | "alt-ergo" | "vampire" | "eprover" | "spass" => ProverClass::SmtOrAtp, + _ => ProverClass::Other, + } +} + /// Determine if a prover uses a small, trusted kernel. /// /// Small-kernel provers have a minimal trusted code base for proof checking, @@ -278,45 +314,58 @@ mod tests { } #[test] - fn test_assess_level5_cross_checked() { - let report = assess_confidence( - &ProverKind::new("lean"), - ProofStatus::Verified, - true, - 3, // 3 independent checkers - ); - assert_eq!(report.level, ConfidenceLevel::Level5); + fn test_assess_cross_checked_without_verified_cert_is_level3() { + // ECHIDNA's kernel needs a *verified* certificate for Level 5; two or + // more agreeing provers without one earn Level 3. + let report = assess_confidence(&ProverKind::new("lean"), ProofStatus::Verified, true, 3); + assert_eq!(report.level, ConfidenceLevel::Level3); assert!(report.small_kernel); assert_eq!(report.checker_count, 3); } #[test] - fn test_assess_level4_small_kernel_with_cert() { - let report = assess_confidence(&ProverKind::new("coq"), ProofStatus::Verified, true, 1); - assert_eq!(report.level, ConfidenceLevel::Level4); + fn test_assess_single_prover_with_unverified_cert_is_level2() { + // echidnabot never verifies certificates, so a cert artefact alone + // does not lift a single result above Level 2. + for slug in ["coq", "z3"] { + let report = assess_confidence(&ProverKind::new(slug), ProofStatus::Verified, true, 1); + assert_eq!(report.level, ConfidenceLevel::Level2, "{slug}"); + } } #[test] - fn test_assess_level3_cert_no_small_kernel() { - let report = assess_confidence( - &ProverKind::new("z3"), - ProofStatus::Verified, - true, // Has DRAT/LRAT certificate - 1, - ); - assert_eq!(report.level, ConfidenceLevel::Level3); + fn test_assess_single_prover_no_cert_is_level2() { + for slug in ["lean", "pvs"] { + let report = assess_confidence(&ProverKind::new(slug), ProofStatus::Verified, false, 1); + assert_eq!(report.level, ConfidenceLevel::Level2, "{slug}"); + } } #[test] - fn test_assess_level2_small_kernel_no_cert() { - let report = assess_confidence(&ProverKind::new("lean"), ProofStatus::Verified, false, 1); - assert_eq!(report.level, ConfidenceLevel::Level2); + fn test_assess_dangerous_axioms_cap_at_level1() { + for danger in [DangerLevel::Warning, DangerLevel::Reject] { + let report = assess_confidence_with_axioms( + &ProverKind::new("lean"), + ProofStatus::Verified, + true, + 3, + danger, + ); + assert_eq!(report.level, ConfidenceLevel::Level1); + } } #[test] - fn test_assess_level1_large_tcb() { - let report = assess_confidence(&ProverKind::new("pvs"), ProofStatus::Verified, false, 1); - assert_eq!(report.level, ConfidenceLevel::Level1); + fn test_level_round_trips_through_echidna() { + for level in [ + ConfidenceLevel::Level1, + ConfidenceLevel::Level2, + ConfidenceLevel::Level3, + ConfidenceLevel::Level4, + ConfidenceLevel::Level5, + ] { + assert_eq!(ConfidenceLevel::from(TrustLevel::from(level)), level); + } } #[test] diff --git a/bots/echidnabot/tests/integration_tests.rs b/bots/echidnabot/tests/integration_tests.rs index b9a33aab..8309063d 100644 --- a/bots/echidnabot/tests/integration_tests.rs +++ b/bots/echidnabot/tests/integration_tests.rs @@ -29,7 +29,6 @@ use axum::http::HeaderMap; use hmac::{Hmac, KeyInit, Mac}; use sha2::Sha256; use std::time::Duration; -use uuid::Uuid; // ============================================================================= // Webhook Signature Verification Tests @@ -146,6 +145,7 @@ fn test_proof_result_parsing() { artifacts: vec!["proof.cert".to_string()], confidence: None, axioms: None, + trust_source: Default::default(), }; assert_eq!(result.status, ProofStatus::Verified); @@ -214,6 +214,7 @@ fn test_result_formatter_truncates_long_output() { artifacts: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; let formatted = format_proof_result( @@ -264,7 +265,7 @@ fn test_check_run_conclusion_values() { #[test] fn test_job_creation() { - let repo_id = Uuid::new_v4(); + let repo_id = echidnabot::ids::new_record_id(); let job = ProofJob::new( repo_id, "abc123def".to_string(), @@ -284,7 +285,7 @@ fn test_job_creation() { #[test] fn test_job_start_sets_running() { let mut job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "abc123".to_string(), ProverKind::new("coq"), vec![], @@ -298,7 +299,7 @@ fn test_job_start_sets_running() { #[test] fn test_job_complete_success() { let mut job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "abc123".to_string(), ProverKind::new("z3"), vec![], @@ -314,6 +315,7 @@ fn test_job_complete_success() { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; job.complete(result); @@ -325,7 +327,7 @@ fn test_job_complete_success() { #[test] fn test_job_complete_failure() { let mut job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "abc123".to_string(), ProverKind::new("lean"), vec![], @@ -341,6 +343,7 @@ fn test_job_complete_failure() { failed_files: vec!["test.lean".to_string()], confidence: None, axioms: None, + trust_source: Default::default(), }; job.complete(result); @@ -350,7 +353,7 @@ fn test_job_complete_failure() { #[test] fn test_job_cancel() { let mut job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "abc123".to_string(), ProverKind::new("agda"), vec![], @@ -388,7 +391,7 @@ fn test_repository_model() { #[test] fn test_proof_job_record_from_job() { let job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "sha256hash".to_string(), ProverKind::new("metamath"), vec!["proof.mm".to_string()], @@ -413,6 +416,7 @@ fn test_proof_result_record() { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; let record = ProofResultRecord::new(job_id, &result); @@ -480,7 +484,7 @@ async fn test_executor_no_backend_refuses_proofs() { #[tokio::test] async fn test_scheduler_enqueue_dequeue_cycle() { let scheduler = JobScheduler::new(2, 10); - let repo_id = Uuid::new_v4(); + let repo_id = echidnabot::ids::new_record_id(); // Enqueue a job let job = ProofJob::new( @@ -511,6 +515,7 @@ async fn test_scheduler_enqueue_dequeue_cycle() { failed_files: vec![], confidence: None, axioms: None, + trust_source: Default::default(), }; scheduler.complete_job(job_id, result).await; @@ -530,7 +535,10 @@ async fn test_tactic_outcome_roundtrip_via_store() { use echidnabot::store::models::{goal_fingerprint, TacticOutcomeRecord}; use echidnabot::store::{SqliteStore, Store}; - let path = std::env::temp_dir().join(format!("echidnabot-test-outcomes-{}.db", Uuid::new_v4())); + let path = std::env::temp_dir().join(format!( + "echidnabot-test-outcomes-{}.db", + echidnabot::ids::new_record_id() + )); let url = format!("sqlite://{}?mode=rwc", path.display()); let store = SqliteStore::new(&url).await.unwrap(); @@ -574,7 +582,7 @@ async fn test_scheduler_metrics_methods() { assert_eq!(scheduler.queue_depth(), 0); // Enqueue some jobs and verify they become visible via stats - let repo_id = Uuid::new_v4(); + let repo_id = echidnabot::ids::new_record_id(); for i in 0..3 { let job = ProofJob::new( repo_id, @@ -594,13 +602,13 @@ async fn test_scheduler_respects_max_concurrent() { // Enqueue two jobs let job1 = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "commit1".to_string(), ProverKind::new("coq"), vec![], ); let job2 = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "commit2".to_string(), ProverKind::new("lean"), vec![], diff --git a/bots/echidnabot/tests/lifecycle.rs b/bots/echidnabot/tests/lifecycle.rs index 23f2089d..6eec638d 100644 --- a/bots/echidnabot/tests/lifecycle.rs +++ b/bots/echidnabot/tests/lifecycle.rs @@ -50,6 +50,7 @@ fn make_job_result(success: bool) -> JobResult { }, confidence: None, axioms: None, + trust_source: Default::default(), } } @@ -68,7 +69,7 @@ fn make_job(repo: Uuid, commit: &str, prover: &str) -> ProofJob { #[test] fn lifecycle_job_starts_queued() { - let job = make_job(Uuid::new_v4(), "abc123", "coq"); + let job = make_job(echidnabot::ids::new_record_id(), "abc123", "coq"); assert_eq!(job.status, JobStatus::Queued); assert!(job.started_at.is_none()); assert!(job.completed_at.is_none()); @@ -76,7 +77,7 @@ fn lifecycle_job_starts_queued() { #[test] fn lifecycle_job_transitions_queued_to_running() { - let mut job = make_job(Uuid::new_v4(), "abc123", "lean"); + let mut job = make_job(echidnabot::ids::new_record_id(), "abc123", "lean"); job.start(); assert_eq!(job.status, JobStatus::Running); assert!( @@ -87,7 +88,7 @@ fn lifecycle_job_transitions_queued_to_running() { #[test] fn lifecycle_job_transitions_running_to_completed() { - let mut job = make_job(Uuid::new_v4(), "def456", "coq"); + let mut job = make_job(echidnabot::ids::new_record_id(), "def456", "coq"); job.start(); job.complete(make_job_result(true)); assert_eq!(job.status, JobStatus::Completed); @@ -99,7 +100,7 @@ fn lifecycle_job_transitions_running_to_completed() { #[test] fn lifecycle_job_transitions_running_to_failed() { - let mut job = make_job(Uuid::new_v4(), "fail001", "lean"); + let mut job = make_job(echidnabot::ids::new_record_id(), "fail001", "lean"); job.start(); job.complete(make_job_result(false)); assert_eq!(job.status, JobStatus::Failed); @@ -107,14 +108,14 @@ fn lifecycle_job_transitions_running_to_failed() { #[test] fn lifecycle_job_cancel_from_queued() { - let mut job = make_job(Uuid::new_v4(), "ghi789", "metamath"); + let mut job = make_job(echidnabot::ids::new_record_id(), "ghi789", "metamath"); job.cancel(); assert_eq!(job.status, JobStatus::Cancelled); } #[test] fn lifecycle_job_duration_ms_after_completion() { - let mut job = make_job(Uuid::new_v4(), "abc", "lean"); + let mut job = make_job(echidnabot::ids::new_record_id(), "abc", "lean"); job.start(); job.complete(make_job_result(true)); let dur = job.duration_ms(); @@ -123,7 +124,7 @@ fn lifecycle_job_duration_ms_after_completion() { #[test] fn lifecycle_job_result_attached_after_completion() { - let mut job = make_job(Uuid::new_v4(), "res_check", "coq"); + let mut job = make_job(echidnabot::ids::new_record_id(), "res_check", "coq"); job.start(); job.complete(make_job_result(true)); assert!( @@ -150,7 +151,7 @@ async fn lifecycle_scheduler_empty_at_start() { #[tokio::test] async fn lifecycle_scheduler_full_job_cycle() { let sched = JobScheduler::new(2, 10); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); let job = make_job(repo, "sha001", "coq"); let job_id = sched @@ -178,7 +179,7 @@ async fn lifecycle_scheduler_full_job_cycle() { #[tokio::test] async fn lifecycle_scheduler_cancel_queued_job() { let sched = JobScheduler::new(1, 10); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); // Fill the single concurrent slot let blocker = make_job(repo, "sha_blocker", "lean"); @@ -201,7 +202,7 @@ async fn lifecycle_scheduler_cancel_queued_job() { #[tokio::test] async fn lifecycle_scheduler_max_concurrent_enforced() { let sched = JobScheduler::new(1, 10); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); sched.enqueue(make_job(repo, "sha1", "coq")).await.unwrap(); sched.enqueue(make_job(repo, "sha2", "lean")).await.unwrap(); @@ -217,7 +218,7 @@ async fn lifecycle_scheduler_max_concurrent_enforced() { #[tokio::test] async fn lifecycle_scheduler_get_job_by_id() { let sched = JobScheduler::new(2, 10); - let job = make_job(Uuid::new_v4(), "get_me", "z3"); + let job = make_job(echidnabot::ids::new_record_id(), "get_me", "z3"); let job_id = sched.enqueue(job).await.unwrap().unwrap(); let found = sched.get_job(job_id).await; @@ -232,8 +233,8 @@ async fn lifecycle_scheduler_get_job_by_id() { #[tokio::test] async fn lifecycle_scheduler_jobs_for_repo() { let sched = JobScheduler::new(4, 20); - let repo_a = Uuid::new_v4(); - let repo_b = Uuid::new_v4(); + let repo_a = echidnabot::ids::new_record_id(); + let repo_b = echidnabot::ids::new_record_id(); sched.enqueue(make_job(repo_a, "a1", "coq")).await.unwrap(); sched.enqueue(make_job(repo_a, "a2", "lean")).await.unwrap(); @@ -423,7 +424,7 @@ async fn lifecycle_shutdown_timeout_fires_with_warning_when_drain_exceeds_deadli // active_count; do that via the normal enqueue+try_start_next flow. let sched = Arc::new(JobScheduler::new(2, 10)); let job = ProofJob::new( - Uuid::new_v4(), + echidnabot::ids::new_record_id(), "deadlock_sha".to_string(), ProverKind::new("coq"), vec!["slow.v".to_string()], diff --git a/bots/echidnabot/tests/live_echidna.rs b/bots/echidnabot/tests/live_echidna.rs new file mode 100644 index 00000000..70790a92 --- /dev/null +++ b/bots/echidnabot/tests/live_echidna.rs @@ -0,0 +1,165 @@ +// SPDX-License-Identifier: MPL-2.0 +//! Live trace: echidnabot's ECHIDNA client against a real `echidna server`. +//! +//! Skipped unless `ECHIDNABOT_LIVE_ECHIDNA_URL` names a running server +//! (e.g. `http://127.0.0.1:8081`, the `echidna server` default). Each check +//! pairs a positive case with a planted negative control, so a client that +//! always answered "verified" would fail here. +//! +//! Run: `ECHIDNABOT_LIVE_ECHIDNA_URL=http://127.0.0.1:8081 cargo test --test live_echidna` + +use echidna_core_spark::axiom_tracker::DangerLevel; +use echidnabot::config::{EchidnaApiMode, EchidnaConfig}; +use echidnabot::dispatcher::echidna_client::{EchidnaClient, MIN_ECHIDNA_VERSION}; +use echidnabot::dispatcher::{ProofStatus, ProverKind}; + +/// Client for the live server named by the environment, or `None` to skip. +fn live_client() -> Option { + let url = std::env::var("ECHIDNABOT_LIVE_ECHIDNA_URL").ok()?; + let config = EchidnaConfig { + endpoint: format!("{url}/"), + rest_endpoint: url, + mode: EchidnaApiMode::Rest, + timeout_secs: 120, + }; + Some(EchidnaClient::new(&config)) +} + +/// Whether `bin` resolves on `PATH`. +fn on_path(bin: &str) -> bool { + std::env::var_os("PATH") + .map(|p| std::env::split_paths(&p).any(|d| d.join(bin).is_file())) + .unwrap_or(false) +} + +/// The REST handshake reads a version >= the minimum and ECHIDNA's prover names. +#[tokio::test] +async fn live_handshake_reads_version_and_prover_list() { + let Some(client) = live_client() else { + eprintln!("skipped: ECHIDNABOT_LIVE_ECHIDNA_URL not set"); + return; + }; + let hs = client + .handshake() + .await + .expect("handshake against live echidna"); + let min = semver::Version::parse(MIN_ECHIDNA_VERSION).unwrap(); + assert!(hs.version >= min, "version {} below {}", hs.version, min); + assert!( + hs.provers.iter().any(|p| p == "Z3"), + "Z3 missing: {:?}", + hs.provers + ); + // Name resolution must use the server's spelling, not the slug. + assert_eq!(client.echidna_name(&ProverKind::new("z3")), "Z3"); + assert_eq!(client.echidna_name(&ProverKind::new("cvc5")), "CVC5"); +} + +/// REST verify: a true Z3 obligation verifies; a planted false one fails. +#[tokio::test] +async fn live_verify_z3_true_goal_and_planted_false_goal() { + let Some(client) = live_client() else { + eprintln!("skipped: ECHIDNABOT_LIVE_ECHIDNA_URL not set"); + return; + }; + if !on_path("z3") { + eprintln!("skipped: z3 not on PATH"); + return; + } + client.ensure_handshake().await.expect("handshake"); + let z3 = ProverKind::new("z3"); + + // Negated obligation x+0=x is unsat -> discharged. + let good = "(declare-const x Int)\n(assert (not (= (+ x 0) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, good).await.expect("verify good"); + assert_eq!(r.status, ProofStatus::Verified, "{r:?}"); + + // Planted control: negated x+1=x is sat -> must NOT verify. + let bad = "(declare-const x Int)\n(assert (not (= (+ x 1) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, bad).await.expect("verify bad"); + assert_eq!(r.status, ProofStatus::Failed, "{r:?}"); +} + +/// REST verify: a true Coq proof verifies, a false one does not, and an +/// `Admitted` proof is flagged by the axiom scan. +#[tokio::test] +async fn live_verify_coq_true_goal_and_planted_false_goal() { + let Some(client) = live_client() else { + eprintln!("skipped: ECHIDNABOT_LIVE_ECHIDNA_URL not set"); + return; + }; + if !on_path("coqc") { + eprintln!("skipped: coqc not on PATH"); + return; + } + client.ensure_handshake().await.expect("handshake"); + let coq = ProverKind::new("coq"); + + let good = "Theorem t : True. Proof. exact I. Qed."; + let r = client.verify_proof(&coq, good).await.expect("verify good"); + assert_eq!(r.status, ProofStatus::Verified, "{r:?}"); + + let bad = "Theorem t : 1 = 2. Proof. reflexivity. Qed."; + let r = client.verify_proof(&coq, bad).await.expect("verify bad"); + assert_ne!(r.status, ProofStatus::Verified, "{r:?}"); + + // `Admitted` is reported PROVED by echidna's /api/verify (upstream gap); + // echidnabot's source scan must still flag it so trust is capped. + let admitted = "Lemma l : False. Admitted."; + let r = client + .verify_proof(&coq, admitted) + .await + .expect("verify admitted"); + let axioms = r.axioms.expect("axiom report"); + assert_ne!( + axioms.worst_danger, + DangerLevel::Safe, + "Admitted not flagged: {axioms:?}" + ); +} + +/// GraphQL verify against `echidna-graphql`: true goal verifies, false fails. +#[tokio::test] +async fn live_graphql_verify_z3_true_goal_and_planted_false_goal() { + // GraphQL is the separate `echidna-graphql` binary (serves at `/`). + let Ok(url) = std::env::var("ECHIDNABOT_LIVE_ECHIDNA_GRAPHQL_URL") else { + eprintln!("skipped: ECHIDNABOT_LIVE_ECHIDNA_GRAPHQL_URL not set"); + return; + }; + if !on_path("z3") { + eprintln!("skipped: z3 not on PATH"); + return; + } + let client = EchidnaClient::new(&EchidnaConfig { + endpoint: url, + rest_endpoint: "http://127.0.0.1:9".to_string(), + mode: EchidnaApiMode::Graphql, + timeout_secs: 120, + }); + let z3 = ProverKind::new("z3"); + let good = "(declare-const x Int)\n(assert (not (= (+ x 0) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, good).await.expect("graphql good"); + assert_eq!(r.status, ProofStatus::Verified, "{r:?}"); + let bad = "(declare-const x Int)\n(assert (not (= (+ x 1) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, bad).await.expect("graphql bad"); + assert_eq!(r.status, ProofStatus::Failed, "{r:?}"); +} + +/// The default config (auto mode) reaches whichever ECHIDNA binary is on 8081. +#[tokio::test] +async fn live_default_config_reaches_whichever_echidna_runs_on_8081() { + // Set ECHIDNABOT_LIVE_DEFAULTS=1 with either `echidna server` or + // `echidna-graphql` running on its default port. + if std::env::var("ECHIDNABOT_LIVE_DEFAULTS").is_err() || !on_path("z3") { + eprintln!("skipped: ECHIDNABOT_LIVE_DEFAULTS not set or z3 missing"); + return; + } + let client = EchidnaClient::new(&EchidnaConfig::default()); + let z3 = ProverKind::new("z3"); + let good = "(declare-const x Int)\n(assert (not (= (+ x 0) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, good).await.expect("default good"); + assert_eq!(r.status, ProofStatus::Verified, "{r:?}"); + let bad = "(declare-const x Int)\n(assert (not (= (+ x 1) x)))\n(check-sat)\n"; + let r = client.verify_proof(&z3, bad).await.expect("default bad"); + assert_eq!(r.status, ProofStatus::Failed, "{r:?}"); +} diff --git a/bots/echidnabot/tests/protocol_contract.rs b/bots/echidnabot/tests/protocol_contract.rs index c61100bc..ca7478b0 100644 --- a/bots/echidnabot/tests/protocol_contract.rs +++ b/bots/echidnabot/tests/protocol_contract.rs @@ -137,3 +137,138 @@ async fn graphql_uses_slug_for_verification_suggestions_and_status() { ); server.abort(); } + +// --------------------------------------------------------------------------- +// submitProofObligation — the wire contract hypatia sends (inbound). +// The query strings below are byte-for-byte what hypatia builds: +// FleetDispatcher.build_proof_obligation_mutation/4 (with and without a +// prover line) and LearningScheduler.submit_requeue/4 (with `inline: true`). +// --------------------------------------------------------------------------- + +/// Schema over an in-memory store, for executing inbound GraphQL directly. +async fn obligation_schema() -> echidnabot::api::graphql::EchidnabotSchema { + use echidnabot::api::graphql::GraphQLState; + use echidnabot::scheduler::JobScheduler; + use echidnabot::store::SqliteStore; + use std::sync::Arc; + + let config = echidnabot::config::Config::default(); + echidnabot::api::create_schema(GraphQLState { + store: Arc::new(SqliteStore::new("sqlite::memory:").await.unwrap()), + scheduler: Arc::new(JobScheduler::new(2, 10)), + echidna: Arc::new(EchidnaClient::new(&config.echidna)), + }) +} + +/// Execute `query` and return the response as JSON (data + errors). +async fn run(schema: &echidnabot::api::graphql::EchidnabotSchema, query: &str) -> Value { + serde_json::to_value(schema.execute(query).await).unwrap() +} + +/// FleetDispatcher's mutation; `prover_line` is "" or " prover: X,\n". +fn fleet_mutation(repo: &str, claim: &str, context: &str, prover_line: &str) -> String { + format!( + "mutation {{\n submitProofObligation(input: {{\n repo: \"{repo}\",\n \ + claim: \"{claim}\",\n context: \"{context}\",\n{prover_line} }}) {{\n \ + success\n proofId\n }}\n}}\n" + ) +} + +const LEARNING_SCHEDULER_MUTATION: &str = r#"mutation { + submitProofObligation(input: { + repo: "hyperpolymath/requeue", + claim: "requeue-of-attempt-42", + context: "strategy-shift class=lemma", + prover: LEAN, + inline: true + }) { success proofId } +} +"#; + +/// Assert a response has no errors and `success: true`; return the proofId. +fn accepted(resp: &Value) -> String { + assert!( + resp.get("errors") + .is_none_or(|e| e.as_array().unwrap().is_empty()), + "{resp}" + ); + let payload = &resp["data"]["submitProofObligation"]; + assert_eq!(payload["success"], json!(true), "{resp}"); + payload["proofId"].as_str().unwrap().to_string() +} + +#[tokio::test] +async fn fleet_dispatcher_obligation_with_prover_is_accepted_with_v8_id() { + let schema = obligation_schema().await; + let q = fleet_mutation( + "hyperpolymath/echidnabot", + "forall x, x = x", + "pattern P1", + " prover: COQ,\n", + ); + let id = uuid::Uuid::parse_str(&accepted(&run(&schema, &q).await)).unwrap(); + assert_eq!( + id.get_version_num(), + 8, + "proofId must be a UUIDv8 content id" + ); +} + +#[tokio::test] +async fn fleet_dispatcher_obligation_without_prover_is_accepted() { + let schema = obligation_schema().await; + let q = fleet_mutation( + "hyperpolymath/echidnabot", + "forall x, x = x", + "pattern P1", + "", + ); + accepted(&run(&schema, &q).await); +} + +#[tokio::test] +async fn learning_scheduler_inline_requeue_is_accepted() { + let schema = obligation_schema().await; + accepted(&run(&schema, LEARNING_SCHEDULER_MUTATION).await); +} + +#[tokio::test] +async fn resubmitting_an_obligation_is_idempotent() { + let schema = obligation_schema().await; + let q = + "mutation { submitProofObligation(input: { repo: \"a/b\", claim: \"c\", context: \"d\" }) \ + { success proofId status newlyRecorded repoRegistered } }"; + let first = run(&schema, q).await; + let second = run(&schema, q).await; + assert_eq!(accepted(&first), accepted(&second)); + let p1 = &first["data"]["submitProofObligation"]; + let p2 = &second["data"]["submitProofObligation"]; + assert_eq!(p1["status"], json!("PENDING")); + assert_eq!(p1["newlyRecorded"], json!(true)); + assert_eq!(p2["newlyRecorded"], json!(false)); + assert_eq!(p1["repoRegistered"], json!(false)); +} + +#[tokio::test] +async fn invalid_obligations_are_graphql_errors_not_success_false() { + let schema = obligation_schema().await; + let big = "x".repeat(echidnabot::api::graphql::MAX_OBLIGATION_FIELD_BYTES + 1); + for q in [ + // Unknown prover enum value: rejected at validation. + fleet_mutation("a/b", "c", "d", " prover: LEAN4,\n"), + // Not an owner/name slug. + fleet_mutation("no-slash", "c", "d", ""), + fleet_mutation("a/b/c", "c", "d", ""), + // Empty claim. + fleet_mutation("a/b", " ", "d", ""), + // Over the size cap. + fleet_mutation("a/b", &big, "d", ""), + ] { + let resp = run(&schema, &q).await; + let errors = resp["errors"].as_array().cloned().unwrap_or_default(); + assert!( + !errors.is_empty(), + "expected a GraphQL error for {q:.80}: {resp}" + ); + } +} diff --git a/bots/echidnabot/tests/regressions/mod.rs b/bots/echidnabot/tests/regressions/mod.rs index c855baaf..8733ada9 100644 --- a/bots/echidnabot/tests/regressions/mod.rs +++ b/bots/echidnabot/tests/regressions/mod.rs @@ -42,7 +42,7 @@ fn regression_prover_key_debug_format_bug_42e7bde() { #[tokio::test] async fn regression_duplicate_detection_respects_prover() { let sched = JobScheduler::new(4, 20); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); let j1 = ProofJob::new(repo, "sha_dup".to_string(), ProverKind::new("coq"), vec![]); let j2 = ProofJob::new(repo, "sha_dup".to_string(), ProverKind::new("lean"), vec![]); // diff prover @@ -71,7 +71,7 @@ fn regression_goal_fingerprint_always_64_chars() { #[tokio::test] async fn regression_priority_queue_ordering() { let sched = JobScheduler::new(1, 10); - let repo = Uuid::new_v4(); + let repo = echidnabot::ids::new_record_id(); let low = ProofJob::new(repo, "low_sha".to_string(), ProverKind::new("coq"), vec![]) .with_priority(JobPriority::Low);