Stabilize MVP verification for Lean/Z3

Your Name · Your Name · commit b196739e13e3 · 2026-01-18T22:17:12.000Z
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/proofs/acl2/basic.lisp b/proofs/acl2/basic.lisp
@@ -0,0 +1,2 @@
+; Minimal ACL2 example for ECHIDNA MVP
+(defun mvp-id (x) x)
diff --git a/proofs/cvc5/basic.smt2 b/proofs/cvc5/basic.smt2
@@ -0,0 +1,9 @@
+; Simple SMT-LIB example for ECHIDNA CVC5 backend
+(set-logic QF_LIA)
+(declare-const x Int)
+(declare-const y Int)
+(assert (> x 0))
+(assert (> y 0))
+(assert (= (+ x y) 10))
+(assert (< x y))
+(check-sat)
diff --git a/proofs/hol4/basic.sml b/proofs/hol4/basic.sml
@@ -0,0 +1 @@
+(* Minimal HOL4 placeholder for ECHIDNA MVP *)
diff --git a/proofs/hol_light/basic.hl b/proofs/hol_light/basic.hl
@@ -0,0 +1 @@
+(* Minimal HOL Light placeholder for ECHIDNA MVP *)
diff --git a/proofs/lean/mvp_basic.lean b/proofs/lean/mvp_basic.lean
@@ -0,0 +1,2 @@
+-- Minimal Lean example for ECHIDNA MVP
+axiom A : Prop
diff --git a/proofs/metamath/basic.mm b/proofs/metamath/basic.mm
@@ -0,0 +1,4 @@
+$( Minimal Metamath example for ECHIDNA )$
+$c wff $.
+$v ph $.
+ph $f wff ph $.
diff --git a/proofs/mizar/mvp_basic.miz b/proofs/mizar/mvp_basic.miz
@@ -0,0 +1,12 @@
+:: Minimal Mizar example for ECHIDNA MVP
+
+environ
+
+begin
+
+theorem Th1:
+  for P being set holds P = P
+proof
+  let P be set;
+  thus P = P;
+end;
diff --git a/proofs/pvs/basic.pvs b/proofs/pvs/basic.pvs
@@ -0,0 +1,3 @@
+MVP: THEORY
+BEGIN
+END MVP
diff --git a/proofs/z3/basic.smt2 b/proofs/z3/basic.smt2
@@ -0,0 +1,4 @@
+; Minimal SMT-LIB example for ECHIDNA Z3 backend
+(set-logic QF_LIA)
+(assert true)
+(check-sat)
diff --git a/scripts/mvp-functional.sh b/scripts/mvp-functional.sh
@@ -0,0 +1,128 @@
+#!/usr/bin/env bash
+set -euo pipefail
+
+ROOT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)"
+BIN="${ROOT_DIR}/target/release/echidna"
+
+if [[ ! -x "$BIN" ]]; then
+  echo "[MVP] echidna binary not found: $BIN"
+  echo "[MVP] Build with: cargo build --release"
+  exit 1
+fi
+
+# Minimal proof samples (placeholders). If prover executable is missing,
+# we skip and record.
+PROVERS=(
+  agda coq lean isabelle z3 cvc5 metamath hollight mizar pvs acl2 hol4
+)
+
+missing=()
+passed=()
+failed=()
+
+check_cmd() {
+  local cmd="$1"
+  if ! command -v "$cmd" >/dev/null 2>&1; then
+    return 1
+  fi
+  return 0
+}
+
+check_mizar_toolchain() {
+  local verifier_cmd
+  local mizf_cmd
+  # Avoid invoking Mizar binaries in sandboxed environments unless explicitly allowed.
+  if [[ -z "${MIZAR_TOOLCHAIN_OK:-}" ]]; then
+    return 1
+  fi
+  verifier_cmd="$(command -v verifier || true)"
+  mizf_cmd="$(command -v mizf || true)"
+  if [[ -z "$verifier_cmd" || -z "$mizf_cmd" ]]; then
+    return 1
+  fi
+  return 0
+}
+
+# Map prover -> executable
+exe_for() {
+  case "$1" in
+    agda) echo agda;;
+    coq) echo coqtop;;
+    lean) echo lean;;
+    isabelle) echo isabelle;;
+    z3) echo z3;;
+    cvc5) echo cvc5;;
+    metamath) echo metamath;;
+    hollight) echo hol-light;;
+    mizar) echo mizar;;
+    pvs) echo pvs;;
+    acl2) echo acl2;;
+    hol4) echo hol4;;
+    *) echo "";;
+  esac
+}
+
+# Minimal sample files (expected to exist in proofs/)
+# If not present, we skip.
+FILE_MAP=(
+  "agda:proofs/agda/Basic.agda"
+  "coq:proofs/coq/basic.v"
+  "lean:proofs/lean/mvp_basic.lean"
+  "isabelle:proofs/isabelle/Basic.thy"
+  "z3:proofs/z3/basic.smt2"
+  "cvc5:proofs/cvc5/basic.smt2"
+  "metamath:proofs/metamath/basic.mm"
+  "hollight:proofs/hol_light/basic.hl"
+  "mizar:proofs/mizar/mvp_basic.miz"
+  "pvs:proofs/pvs/basic.pvs"
+  "acl2:proofs/acl2/basic.lisp"
+  "hol4:proofs/hol4/basic.sml"
+)
+
+file_for() {
+  local prover="$1"
+  for entry in "${FILE_MAP[@]}"; do
+    local key="${entry%%:*}"
+    local path="${entry#*:}"
+    if [[ "$key" == "$prover" ]]; then
+      echo "$ROOT_DIR/$path"
+      return
+    fi
+  done
+  echo ""
+}
+
+for prover in "${PROVERS[@]}"; do
+  exe="$(exe_for "$prover")"
+  if [[ -z "$exe" ]] || ! check_cmd "$exe"; then
+    missing+=("$prover")
+    continue
+  fi
+  if [[ "$prover" == "mizar" ]] && ! check_mizar_toolchain; then
+    missing+=("$prover")
+    continue
+  fi
+
+  sample_file="$(file_for "$prover")"
+  if [[ -z "$sample_file" || ! -f "$sample_file" ]]; then
+    echo "[MVP] Missing sample for $prover ($sample_file); skipping."
+    missing+=("$prover")
+    continue
+  fi
+
+  if "$BIN" verify --prover "$prover" "$sample_file" >/dev/null 2>&1; then
+    passed+=("$prover")
+  else
+    failed+=("$prover")
+  fi
+
+done
+
+echo "[MVP] Functional sweep summary"
+echo "  Passed: ${passed[*]:-none}"
+echo "  Failed: ${failed[*]:-none}"
+echo "  Missing: ${missing[*]:-none}"
+
+if [[ ${#failed[@]} -gt 0 ]]; then
+  exit 1
+fi
diff --git a/src/rust/provers/lean.rs b/src/rust/provers/lean.rs
@@ -1240,7 +1240,7 @@ impl ProverBackend for LeanBackend {
             .context("Failed to write temporary file")?;
 
         let result = self
-            .run_lean(&["--run", &temp_file.to_string_lossy()])
+            .run_lean(&[&temp_file.to_string_lossy()])
             .await;
 
         // Clean up
@@ -1283,6 +1283,10 @@ impl ProverBackend for LeanBackend {
     }
 
     async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
+        if state.goals.is_empty() {
+            return Ok(true);
+        }
+
         // Generate Lean code from the proof state
         let lean_code = self.export(state).await?;
 
diff --git a/src/rust/provers/z3.rs b/src/rust/provers/z3.rs
@@ -283,6 +283,12 @@ impl ProverBackend for Z3Backend {
         if state.goals.is_empty() {
             return Ok(true);
         }
+        if state.goals.iter().all(|g| matches!(&g.target, Term::Const(c) if c == "true")) {
+            return Ok(true);
+        }
+        if state.goals.iter().any(|g| matches!(&g.target, Term::Const(c) if c == "false")) {
+            return Ok(false);
+        }
 
         // Build complete SMT-LIB query with variable declarations
         let mut commands = String::new();

Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+; Minimal ACL2 example for ECHIDNA MVP`
	`2`	`+(defun mvp-id (x) x)`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+(* Minimal HOL4 placeholder for ECHIDNA MVP *)`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1 @@`
	`1`	`+(* Minimal HOL Light placeholder for ECHIDNA MVP *)`
Original file line number	Diff line number	Diff line change
`@@ -0,0 +1,2 @@`
	`1`	`+-- Minimal Lean example for ECHIDNA MVP`
	`2`	`+axiom A : Prop`