From a3b6813f250d1a573f6e751b7163c1de11797ed1 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 20 Apr 2026 06:29:06 +0000 Subject: [PATCH] feat(types): wire backend consumers + fix z3 build + outcome module MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Step 3 of the native type-system plan: wire backends to consume TypeInfo decorations, extend GNN graph awareness, and fix a pre-existing build break. Changes: 1. Fix pre-existing z3 build break: - Create `src/rust/provers/outcome.rs` with `ProverOutcome` enum (8 variants: Proved, InconsistentPremises, NoProofFound, UnsupportedFeature, InvalidInput, Timeout, ProverError, SystemError) - Move orphan `check` method from `impl ProverBackend for Z3Backend` to its own `impl Z3Backend` block — it was not a trait member - Result: `cargo check --lib` now passes cleanly (0 errors, 0 warnings) 2. Idris2 QTT multiplicity wiring: - `export()` now reads `Definition.type_info.multiplicity` and emits QTT annotations (`0 `, `1 `, or unrestricted) on type signatures - Added `multiplicity_to_idris2()` helper mapping all Multiplicity variants to Idris2 QTT syntax - Removed duplicate local Multiplicity enum (now uses crate::types) 3. F* effect + refinement wiring: - `to_input_format()` now reads `Definition.type_info.effects` and emits F* effect prefixes (Tot, IO, ST, Exn, Div, GTot, ALL, Custom) - Reads `type_info.refinement` and emits `{v:T | P}` syntax - Added `effect_to_fstar()` helper 4. Dedukti exchange layer Sigma support: - `term_to_dedukti()` renders `Term::Sigma` as `dk_sigma A (x => B)` - `parse_dedukti_term()` parses `dk_sigma` back to `Term::Sigma` 5. GNN graph type-info awareness: - Added `EdgeKind::HasMultiplicity`, `HasEffect`, `HasModality` - `add_type_info_edges()` creates annotation nodes and edges from hypothesis/definition type_info decorations - Embeddings: added "sigma" label detection in feature extraction, updated quantifier feature to include sigma binders Test results: 587 passed, 0 failed, 0 clippy warnings. https://claude.ai/code/session_01FYkVX52Tdn6Arp9dWfPLxq --- src/rust/exchange/dedukti.rs | 60 +++++++ src/rust/gnn/embeddings.rs | 4 + src/rust/gnn/graph.rs | 86 +++++++++- src/rust/provers/fstar.rs | 40 +++++ src/rust/provers/idris2.rs | 35 ++-- src/rust/provers/mod.rs | 1 + src/rust/provers/outcome.rs | 83 ++++++++++ src/rust/provers/z3.rs | 309 +++++++++++++++-------------------- 8 files changed, 429 insertions(+), 189 deletions(-) create mode 100644 src/rust/provers/outcome.rs diff --git a/src/rust/exchange/dedukti.rs b/src/rust/exchange/dedukti.rs index 3849875..04bf345 100644 --- a/src/rust/exchange/dedukti.rs +++ b/src/rust/exchange/dedukti.rs @@ -211,6 +211,18 @@ impl DeduktiExporter { Self::term_to_dedukti(body) ) }, + Term::Sigma { + param, + param_type, + body, + } => { + format!( + "(dk_sigma {} ({} => {}))", + Self::term_to_dedukti(param_type), + param, + Self::term_to_dedukti(body) + ) + }, Term::Type(level) => format!("Type {}", level), Term::Sort(level) => format!("Sort {}", level), Term::Universe(level) => format!("Type {}", level), @@ -224,6 +236,32 @@ impl DeduktiExporter { if trimmed.starts_with('(') && trimmed.ends_with(')') { // Unwrap parentheses and recurse Self::dedukti_to_term(&trimmed[1..trimmed.len() - 1]) + } else if trimmed.starts_with("dk_sigma ") { + // Sigma type: dk_sigma A (x => B) + let rest = trimmed.trim_start_matches("dk_sigma ").trim(); + // Split into the type part and the binder part (x => B) + if let Some(paren_start) = rest.find('(') { + let type_part = rest[..paren_start].trim(); + let binder_part = rest[paren_start..].trim(); + let inner = if binder_part.starts_with('(') && binder_part.ends_with(')') { + &binder_part[1..binder_part.len() - 1] + } else { + binder_part + }; + if let Some(arrow_pos) = inner.find("=>") { + let param = inner[..arrow_pos].trim().to_string(); + let body_str = inner[arrow_pos + 2..].trim(); + Term::Sigma { + param, + param_type: Box::new(Self::dedukti_to_term(type_part)), + body: Box::new(Self::dedukti_to_term(body_str)), + } + } else { + Term::Const(trimmed.to_string()) + } + } else { + Term::Const(trimmed.to_string()) + } } else if trimmed.contains("->") { // Pi type: A -> B let parts: Vec<&str> = trimmed.splitn(2, "->").collect(); @@ -416,6 +454,28 @@ mod tests { assert_eq!(dk, "x"); } + #[test] + fn test_term_to_dedukti_sigma() { + let term = Term::Sigma { + param: "x".to_string(), + param_type: Box::new(Term::Const("Nat".to_string())), + body: Box::new(Term::Const("Prop".to_string())), + }; + let dk = DeduktiExporter::term_to_dedukti(&term); + assert!(dk.contains("dk_sigma"), "Sigma should render as dk_sigma, got: {}", dk); + assert!(dk.contains("Nat"), "Sigma param type should appear, got: {}", dk); + } + + #[test] + fn test_dedukti_to_term_sigma() { + let dk = "dk_sigma Nat (x => Prop)"; + let term = DeduktiExporter::dedukti_to_term(dk); + match term { + Term::Sigma { ref param, .. } => assert_eq!(param, "x"), + _ => panic!("Expected Sigma term, got: {:?}", term), + } + } + #[test] fn test_import_with_definition() { let module = DeduktiModule { diff --git a/src/rust/gnn/embeddings.rs b/src/rust/gnn/embeddings.rs index 2ba6839..fa296b0 100644 --- a/src/rust/gnn/embeddings.rs +++ b/src/rust/gnn/embeddings.rs @@ -190,9 +190,11 @@ impl TermFeatureExtractor { // Feature [29]: Contains quantifier (forall, exists, pi) if offset < FEATURE_DIM { features[offset] = if node.label.contains("pi_") + || node.label.contains("sigma_") || node.label.contains("forall") || node.label.contains("exists") || node.label.contains("Pi") + || node.label.contains("Sigma") { 1.0 } else { @@ -310,6 +312,8 @@ fn infer_term_kind_from_label(label: &str) -> usize { 3 // Lambda } else if label.starts_with("pi_") { 4 // Pi + } else if label.starts_with("sigma_") { + 13 // Sigma } else if label.starts_with("let_") { 7 // Let } else if label.starts_with("fix_") { diff --git a/src/rust/gnn/graph.rs b/src/rust/gnn/graph.rs index 169ff91..0bd344b 100644 --- a/src/rust/gnn/graph.rs +++ b/src/rust/gnn/graph.rs @@ -17,7 +17,7 @@ use serde::{Deserialize, Serialize}; use std::collections::HashMap; -use crate::core::{Context, Goal, Hypothesis, ProofState, Term, Theorem}; +use crate::core::{Context, Definition, Goal, Hypothesis, ProofState, Term, Theorem}; /// Kind of node in the proof graph. /// @@ -63,6 +63,12 @@ pub enum EdgeKind { DependsOn, /// Reverse of DependsOn (premise is useful for goal) UsefulFor, + /// Source has the target as its QTT multiplicity annotation + HasMultiplicity, + /// Source has the target as its algebraic effect annotation + HasEffect, + /// Source has the target as its modal decoration + HasModality, } /// A single node in the proof graph. @@ -185,18 +191,25 @@ impl ProofGraphBuilder { // Phase 2: Add hypothesis nodes from context let hyp_ids = self.add_hypotheses_from_context(&state.context); + // Phase 2b: Add definition nodes from context + let def_ids = self.add_definitions_from_context(&state.context); + // Phase 3: Add premise/theorem nodes from context for theorem in &state.context.theorems { let pid = self.add_premise(theorem); premise_node_ids.push(pid); } - // Phase 4: Add dependency edges from goals to hypotheses/premises + // Phase 4: Add dependency edges from goals to hypotheses/definitions/premises if let Some(gid) = goal_node_id { for &hid in &hyp_ids { self.add_edge(gid, hid, EdgeKind::DependsOn, 1.0); self.add_edge(hid, gid, EdgeKind::UsefulFor, 1.0); } + for &did in &def_ids { + self.add_edge(gid, did, EdgeKind::DependsOn, 0.9); + self.add_edge(did, gid, EdgeKind::UsefulFor, 0.9); + } for &pid in &premise_node_ids { self.add_edge(gid, pid, EdgeKind::DependsOn, 0.8); self.add_edge(pid, gid, EdgeKind::UsefulFor, 0.8); @@ -278,6 +291,11 @@ impl ProofGraphBuilder { self.expand_term(body, hid, 1); } + // Wire type_info annotations as edges + if let Some(ref info) = hyp.type_info { + self.add_type_info_edges(hid, info); + } + hid } @@ -288,11 +306,49 @@ impl ProofGraphBuilder { let label = format!("{}: {}", var.name, var.ty); let vid = self.add_node(NodeKind::Hypothesis, &label, 0); self.expand_term(&var.ty, vid, 1); + + // Wire type_info annotations as edges + if let Some(ref info) = var.type_info { + self.add_type_info_edges(vid, info); + } + ids.push(vid); } ids } + /// Add definition nodes from the global context. + fn add_definitions_from_context(&mut self, ctx: &Context) -> Vec { + let mut ids = Vec::new(); + for def in &ctx.definitions { + let did = self.add_definition(def); + ids.push(did); + } + ids + } + + /// Add a definition node. + fn add_definition(&mut self, def: &Definition) -> usize { + let label = format!("{}: {}", def.name, def.ty); + let did = self.add_node(NodeKind::Hypothesis, &label, 0); + + // Expand the definition type + let type_id = self.expand_term(&def.ty, did, 1); + if let Some(tid) = type_id { + self.add_edge(did, tid, EdgeKind::HasType, 1.0); + } + + // Expand the definition body + self.expand_term(&def.body, did, 1); + + // Wire type_info annotations as edges + if let Some(ref info) = def.type_info { + self.add_type_info_edges(did, info); + } + + did + } + /// Add a premise (theorem/lemma) node. fn add_premise(&mut self, theorem: &Theorem) -> usize { let label = format!("{}: {}", theorem.name, theorem.statement); @@ -456,6 +512,32 @@ impl ProofGraphBuilder { } } + /// Add edges from a node to represent its [`TypeInfo`] annotations. + /// + /// Creates labelled subterm nodes for multiplicity, effect, and modality + /// decorations and connects them with the appropriate edge kind. + fn add_type_info_edges(&mut self, node_id: usize, info: &crate::types::TypeInfo) { + if let Some(ref mult) = info.multiplicity { + let label = format!("mult:{:?}", mult); + let mid = self.add_node(NodeKind::Subterm, &label, 1); + self.add_edge(node_id, mid, EdgeKind::HasMultiplicity, 1.0); + } + + if !info.effects.is_empty() { + for eff in &info.effects.effects { + let label = format!("effect:{:?}", eff); + let eid = self.add_node(NodeKind::Subterm, &label, 1); + self.add_edge(node_id, eid, EdgeKind::HasEffect, 1.0); + } + } + + if let Some(ref modality) = info.modality { + let label = format!("modality:{:?}", modality); + let mid = self.add_node(NodeKind::Subterm, &label, 1); + self.add_edge(node_id, mid, EdgeKind::HasModality, 1.0); + } + } + /// Add shared-structure edges between premise nodes that share constants. /// /// Two premises sharing named constants likely have semantic overlap, diff --git a/src/rust/provers/fstar.rs b/src/rust/provers/fstar.rs index fd2cbc3..1a26c42 100644 --- a/src/rust/provers/fstar.rs +++ b/src/rust/provers/fstar.rs @@ -17,6 +17,7 @@ use tokio::process::Command; use super::{ProverBackend, ProverConfig, ProverKind}; use crate::core::{Goal, ProofState, Tactic, TacticResult, Term}; +use crate::types::{Effect, TypeInfo}; /// F* backend pub struct FStarBackend { @@ -33,12 +34,51 @@ impl FStarBackend { for (i, axiom) in state.context.axioms.iter().enumerate() { input.push_str(&format!("assume val axiom_{} : {}\n", i, axiom)); } + // Emit definitions with effect and refinement annotations from TypeInfo + for def in &state.context.definitions { + let effect_str = def + .type_info + .as_ref() + .map(Self::effect_to_fstar) + .unwrap_or_default(); + let refinement_str = def + .type_info + .as_ref() + .and_then(|ti| ti.refinement.as_ref()) + .map(|pred| format!("{{v:{} | {}}}", def.ty, pred)) + .unwrap_or_else(|| format!("{}", def.ty)); + input.push_str(&format!("val {} : {}{}\n", def.name, effect_str, refinement_str)); + } if let Some(goal) = state.goals.first() { input.push_str(&format!("\nval goal : {}\n", goal.target)); } Ok(input) } + /// Convert effect row from [`TypeInfo`] to an F* effect annotation prefix. + fn effect_to_fstar(ti: &TypeInfo) -> String { + if ti.effects.is_empty() { + return String::new(); + } + let effect_name = ti + .effects + .effects + .first() + .map(|e| match e { + Effect::Pure | Effect::Tot => "Tot", + Effect::IO => "IO", + Effect::State => "ST", + Effect::Exception => "Exn", + Effect::Div => "Div", + Effect::Ghost => "GTot", + Effect::NonDet => "ALL", + Effect::Async => "ALL", + Effect::Custom(s) => s.as_str(), + }) + .unwrap_or("Tot"); + format!("{} ", effect_name) + } + fn parse_result(&self, output: &str) -> Result { let lower = output.to_lowercase(); if lower.contains("verified") || lower.contains("all verification conditions discharged") { diff --git a/src/rust/provers/idris2.rs b/src/rust/provers/idris2.rs index 7d1aae0..64d24e3 100644 --- a/src/rust/provers/idris2.rs +++ b/src/rust/provers/idris2.rs @@ -30,6 +30,7 @@ use crate::core::{ Theorem, }; use crate::provers::{ProverBackend, ProverConfig, ProverKind}; +use crate::types::Multiplicity; /// Idris 2 backend implementation pub struct Idris2Backend { @@ -105,17 +106,6 @@ enum Idris2Term { AutoImplicit(String, Box), } -/// Quantitative type theory multiplicities -#[derive(Debug, Clone, Copy, PartialEq, Eq)] -enum Multiplicity { - /// Unrestricted (0, 1, or many uses) - Unrestricted, - /// Linear (exactly 1 use) - Linear, - /// Erased (0 uses at runtime) - Erased, -} - impl Idris2Backend { pub fn new(config: ProverConfig) -> Self { Idris2Backend { @@ -178,6 +168,17 @@ impl Idris2Backend { } } + /// Convert a [`Multiplicity`] to the Idris 2 QTT annotation string. + fn multiplicity_to_idris2(m: &Multiplicity) -> &'static str { + match m { + Multiplicity::Zero => "0", + Multiplicity::One | Multiplicity::Linear => "1", + Multiplicity::Omega | Multiplicity::Shared => "", + Multiplicity::Affine => "1", // closest QTT approximation + Multiplicity::Graded(_) => "", + } + } + /// Convert universal Term to Idris 2 syntax fn term_to_idris2(&self, term: &Term) -> String { match term { @@ -815,11 +816,17 @@ impl ProverBackend for Idris2Backend { output.push_str("import Data.Vect\n"); output.push_str("import Data.Nat\n\n"); - // Definitions + // Definitions (emit QTT multiplicity annotations when present) for def in &state.context.definitions { let ty_str = self.term_to_idris2(&def.ty); let body_str = self.term_to_idris2(&def.body); - output.push_str(&format!("{} : {}\n", def.name, ty_str)); + let mult_prefix = def + .type_info + .as_ref() + .and_then(|ti| ti.multiplicity.as_ref()) + .map(|m| format!("{} ", Self::multiplicity_to_idris2(m))) + .unwrap_or_default(); + output.push_str(&format!("{}{} : {}\n", mult_prefix, def.name, ty_str)); output.push_str(&format!("{} = {}\n\n", def.name, body_str)); } @@ -1210,7 +1217,7 @@ mod tests { // Test Pi type let pi_term = Idris2Term::Pi( "a".to_string(), - Multiplicity::Unrestricted, + Multiplicity::Omega, Box::new(Idris2Term::Type), Box::new(Idris2Term::Var("a".to_string())), ); diff --git a/src/rust/provers/mod.rs b/src/rust/provers/mod.rs index ed3f294..afa3bf6 100644 --- a/src/rust/provers/mod.rs +++ b/src/rust/provers/mod.rs @@ -45,6 +45,7 @@ pub mod mizar; pub mod nuprl; pub mod nusmv; pub mod ortools; +pub mod outcome; pub mod prism; pub mod proverif; pub mod pvs; diff --git a/src/rust/provers/outcome.rs b/src/rust/provers/outcome.rs new file mode 100644 index 0000000..023f521 --- /dev/null +++ b/src/rust/provers/outcome.rs @@ -0,0 +1,83 @@ +// SPDX-FileCopyrightText: 2026 ECHIDNA Project Team +// SPDX-License-Identifier: PMPL-1.0-or-later + +//! Structured prover outcome types. +//! +//! [`ProverOutcome`] provides a richer alternative to a plain `bool` for +//! verification results, distinguishing proved goals, counterexamples, +//! timeouts, input errors, inconsistent premises, and system failures. + +use serde::{Deserialize, Serialize}; + +/// Classification of a prover verification result. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub enum ProverOutcome { + /// The goal was proved (e.g. negation is UNSAT). + Proved { elapsed_ms: u64 }, + + /// The premises / axioms are themselves inconsistent — any goal follows + /// trivially, so the proof result cannot be trusted. + InconsistentPremises { detail: Option }, + + /// The prover terminated without proving the goal. + NoProofFound { + elapsed_ms: u64, + reason: Option, + }, + + /// The goal uses a feature / logic fragment the prover does not support. + UnsupportedFeature { feature: String }, + + /// The input was malformed or violated the prover's expectations. + InvalidInput { + reason: String, + location: Option, + }, + + /// The prover timed out before reaching a verdict. + Timeout { limit_secs: u64 }, + + /// An error internal to the prover (crash, assertion failure, etc.). + ProverError { + detail: String, + exit_code: Option, + }, + + /// A system-level error (binary not found, I/O failure, etc.). + SystemError { detail: String }, +} + +impl ProverOutcome { + /// Returns `true` when the outcome represents a successful proof. + pub fn is_proved(&self) -> bool { + matches!(self, Self::Proved { .. }) + } +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn proved_is_proved() { + let o = ProverOutcome::Proved { elapsed_ms: 42 }; + assert!(o.is_proved()); + } + + #[test] + fn timeout_is_not_proved() { + let o = ProverOutcome::Timeout { limit_secs: 60 }; + assert!(!o.is_proved()); + } + + #[test] + fn roundtrips_through_json() { + let o = ProverOutcome::NoProofFound { + elapsed_ms: 100, + reason: Some("counterexample".to_string()), + }; + let json = serde_json::to_string(&o).unwrap(); + let back: ProverOutcome = serde_json::from_str(&json).unwrap(); + assert_eq!(o, back); + } +} diff --git a/src/rust/provers/z3.rs b/src/rust/provers/z3.rs index bfb3196..bd4de25 100644 --- a/src/rust/provers/z3.rs +++ b/src/rust/provers/z3.rs @@ -211,6 +211,142 @@ impl Z3Backend { self.execute_command(&commands).await } + + /// Typed verification with precise outcome classification. + pub async fn check( + &self, + state: &ProofState, + ) -> anyhow::Result { + use super::outcome::ProverOutcome; + use std::time::Instant; + let start = Instant::now(); + + if state.goals.is_empty() { + return Ok(ProverOutcome::Proved { elapsed_ms: 0 }); + } + + let mut preamble = String::from("(set-logic ALL)\n"); + for var in &state.context.variables { + preamble.push_str(&format!( + "(declare-const {} {})\n", + var.name, + self.term_to_smt(&var.ty) + )); + } + + let axioms_inconsistent = if !state.context.axioms.is_empty() { + let mut hyp_check = preamble.clone(); + for axiom in &state.context.axioms { + hyp_check.push_str(&format!("(assert {})\n", axiom)); + } + hyp_check.push_str("(check-sat)\n"); + matches!(self.execute_command(&hyp_check).await, Ok(SmtResult::Unsat)) + } else { + false + }; + + let goals_inconsistent = if !axioms_inconsistent { + let mut goal_check = preamble.clone(); + for axiom in &state.context.axioms { + goal_check.push_str(&format!("(assert {})\n", axiom)); + } + for goal in &state.goals { + goal_check.push_str(&format!("(assert {})\n", self.term_to_smt(&goal.target))); + } + goal_check.push_str("(check-sat)\n"); + matches!(self.execute_command(&goal_check).await, Ok(SmtResult::Unsat)) + } else { + false + }; + + if axioms_inconsistent { + return Ok(ProverOutcome::InconsistentPremises { + detail: Some( + "axioms are mutually unsatisfiable; any goal follows trivially".to_string(), + ), + }); + } + if goals_inconsistent { + return Ok(ProverOutcome::InconsistentPremises { + detail: Some( + "goal set is self-contradictory (goals cannot all hold simultaneously)" + .to_string(), + ), + }); + } + + if state + .goals + .iter() + .all(|g| matches!(&g.target, Term::Const(c) if c == "true")) + { + return Ok(ProverOutcome::Proved { elapsed_ms: 0 }); + } + + let mut commands = preamble; + for axiom in &state.context.axioms { + commands.push_str(&format!("(assert {})\n", axiom)); + } + for goal in &state.goals { + commands.push_str(&format!("(assert (not {}))\n", self.term_to_smt(&goal.target))); + } + commands.push_str("(check-sat)\n"); + + let elapsed = || start.elapsed().as_millis() as u64; + + match self.execute_command(&commands).await { + Ok(SmtResult::Unsat) => { + Ok(ProverOutcome::Proved { elapsed_ms: elapsed() }) + }, + Ok(SmtResult::Sat) => Ok(ProverOutcome::NoProofFound { + elapsed_ms: elapsed(), + reason: Some("Z3 found a counterexample (SAT)".to_string()), + }), + Ok(SmtResult::Unknown) => Ok(ProverOutcome::NoProofFound { + elapsed_ms: elapsed(), + reason: Some( + "Z3 returned 'unknown' (goal may be undecidable in the selected logic)" + .to_string(), + ), + }), + Ok(SmtResult::Error(e)) => { + if e.to_lowercase().contains("unknown") + || e.to_lowercase().contains("unsupported") + || e.to_lowercase().contains("logic") + { + Ok(ProverOutcome::UnsupportedFeature { feature: e }) + } else { + Ok(ProverOutcome::InvalidInput { + reason: e, + location: None, + }) + } + }, + Ok(SmtResult::Output(_)) => Ok(ProverOutcome::NoProofFound { + elapsed_ms: elapsed(), + reason: Some("unexpected output from Z3 (check-sat returned non-standard response)" + .to_string()), + }), + Err(e) => { + let msg = e.to_string().to_lowercase(); + if msg.contains("timeout") || msg.contains("timed out") { + Ok(ProverOutcome::Timeout { + limit_secs: self.config.timeout, + }) + } else if msg.contains("failed to spawn") + || msg.contains("no such file") + || msg.contains("os error") + { + Ok(ProverOutcome::SystemError { detail: e.to_string() }) + } else { + Ok(ProverOutcome::ProverError { + detail: e.to_string(), + exit_code: None, + }) + } + }, + } + } } #[async_trait] @@ -354,179 +490,6 @@ impl ProverBackend for Z3Backend { } } - /// Typed verification with precise outcome classification. - /// - /// This override distinguishes: - /// - `Proved` (negation of goal is UNSAT with hypotheses) - /// - `InconsistentPremises` (hypotheses alone are UNSAT, making any proof trivial) - /// - `NoProofFound` with `reason: Some("counterexample")` (SAT result) - /// - `NoProofFound` with `reason: Some("SMT unknown")` (decidability limit) - /// - `Timeout` (Z3 process timed out before producing an answer) - /// - `InvalidInput` (Z3 reported `(error ...)` for a user input problem) - /// - `ProverError` (Z3 reported an internal error) - /// - `SystemError` (Z3 process could not be spawned) - async fn check( - &self, - state: &ProofState, - ) -> anyhow::Result { - use super::outcome::ProverOutcome; - use std::time::Instant; - let start = Instant::now(); - - // Vacuous case: no goals at all → trivially proved (no outstanding obligations). - if state.goals.is_empty() { - return Ok(ProverOutcome::Proved { elapsed_ms: 0 }); - } - - // Step 1: Consistency pre-check — must run before any trivial-goal - // short-circuit so that P∧¬P is never silently rubber-stamped as PROVED. - // - // Two sub-checks: - // (a) Axiom consistency: assert all axioms; if UNSAT, premises alone - // are contradictory — any goal follows trivially. - // (b) Goal consistency: assert all goals (without negation); if UNSAT, - // the goal set is self-contradictory (e.g. prove P and prove ¬P - // simultaneously). This is a weaker signal but still suspect. - // - // Either condition surfaces as InconsistentPremises so the caller knows - // the result cannot be trusted. - - // Build the common preamble (variable declarations) once. - let mut preamble = String::from("(set-logic ALL)\n"); - for var in &state.context.variables { - preamble.push_str(&format!( - "(declare-const {} {})\n", - var.name, - self.term_to_smt(&var.ty) - )); - } - - // (a) Axiom consistency. - let axioms_inconsistent = if !state.context.axioms.is_empty() { - let mut hyp_check = preamble.clone(); - for axiom in &state.context.axioms { - hyp_check.push_str(&format!("(assert {})\n", axiom)); - } - hyp_check.push_str("(check-sat)\n"); - matches!(self.execute_command(&hyp_check).await, Ok(SmtResult::Unsat)) - } else { - false - }; - - // (b) Goal consistency — only worth checking when axioms are fine, to - // avoid masking the more informative axiom-level diagnosis. - let goals_inconsistent = if !axioms_inconsistent { - let mut goal_check = preamble.clone(); - for axiom in &state.context.axioms { - goal_check.push_str(&format!("(assert {})\n", axiom)); - } - for goal in &state.goals { - // Assert goals as-is (no negation): if UNSAT, the goals themselves - // cannot all be true simultaneously. - goal_check.push_str(&format!("(assert {})\n", self.term_to_smt(&goal.target))); - } - goal_check.push_str("(check-sat)\n"); - matches!(self.execute_command(&goal_check).await, Ok(SmtResult::Unsat)) - } else { - false - }; - - if axioms_inconsistent { - return Ok(ProverOutcome::InconsistentPremises { - detail: Some( - "axioms are mutually unsatisfiable; any goal follows trivially".to_string(), - ), - }); - } - if goals_inconsistent { - return Ok(ProverOutcome::InconsistentPremises { - detail: Some( - "goal set is self-contradictory (goals cannot all hold simultaneously)" - .to_string(), - ), - }); - } - - // Trivial-goal short-circuit: only reached when premises are consistent - // (or there are no axioms at all). - if state - .goals - .iter() - .all(|g| matches!(&g.target, Term::Const(c) if c == "true")) - { - return Ok(ProverOutcome::Proved { elapsed_ms: 0 }); - } - - // Step 2: Build the main validity query. - // Reuse the preamble (variables already declared), add axioms and the - // negation of each goal. UNSAT → goal follows from axioms → PROVED. - let mut commands = preamble; - for axiom in &state.context.axioms { - commands.push_str(&format!("(assert {})\n", axiom)); - } - for goal in &state.goals { - commands.push_str(&format!("(assert (not {}))\n", self.term_to_smt(&goal.target))); - } - commands.push_str("(check-sat)\n"); - - let elapsed = || start.elapsed().as_millis() as u64; - - match self.execute_command(&commands).await { - // `inconsistent` is always false here (we returned early above if true). - Ok(SmtResult::Unsat) => { - Ok(ProverOutcome::Proved { elapsed_ms: elapsed() }) - }, - Ok(SmtResult::Sat) => Ok(ProverOutcome::NoProofFound { - elapsed_ms: elapsed(), - reason: Some("Z3 found a counterexample (SAT)".to_string()), - }), - Ok(SmtResult::Unknown) => Ok(ProverOutcome::NoProofFound { - elapsed_ms: elapsed(), - reason: Some( - "Z3 returned 'unknown' (goal may be undecidable in the selected logic)" - .to_string(), - ), - }), - Ok(SmtResult::Error(e)) => { - // Z3 `(error ...)` is almost always a user input problem. - if e.to_lowercase().contains("unknown") - || e.to_lowercase().contains("unsupported") - || e.to_lowercase().contains("logic") - { - Ok(ProverOutcome::UnsupportedFeature { feature: e }) - } else { - Ok(ProverOutcome::InvalidInput { - reason: e, - location: None, - }) - } - }, - Ok(SmtResult::Output(_)) => Ok(ProverOutcome::NoProofFound { - elapsed_ms: elapsed(), - reason: Some("unexpected output from Z3 (check-sat returned non-standard response)" - .to_string()), - }), - Err(e) => { - let msg = e.to_string().to_lowercase(); - if msg.contains("timeout") || msg.contains("timed out") { - Ok(ProverOutcome::Timeout { - limit_secs: self.config.timeout, - }) - } else if msg.contains("failed to spawn") - || msg.contains("no such file") - || msg.contains("os error") - { - Ok(ProverOutcome::SystemError { detail: e.to_string() }) - } else { - Ok(ProverOutcome::ProverError { - detail: e.to_string(), - exit_code: None, - }) - } - }, - } - } - async fn export(&self, state: &ProofState) -> Result { let mut output = String::new();