fix(provers/isabelle): de-stub parse_string + verify_proof

parse_string previously discarded its content argument and returned a
single Term::Const("True") goal, which verify_proof then short-circuited
to Ok(true) — Isabelle was never actually invoked. Combined with the
filename/theory-name mismatch in the scaffolded export path
(echidna_verify.thy contained `theory GeneratedProof`, which isabelle
build refuses), the HTTP /api/verify endpoint with prover=Isabelle was
returning success regardless of input.

Now:
- parse_string extracts the theory name and every top-level
  theorem|lemma|corollary declaration via a nested-comment-aware scanner.
  Raw .thy content is stashed in ProofState.metadata["raw_thy_content"].
- verify_proof writes that raw content to a unique per-invocation temp
  dir as <theory_name>.thy and runs `isabelle process -l Main -e
  'use_thys ["<path>"]'`. Exit status determines the verdict.
- Fallback scaffolded-export path writes GeneratedProof.thy in its own
  unique temp dir, fixing the filename/theory-name mismatch.

Added 9 unit tests covering comment stripping (incl. nested blocks),
theory-name extraction (basic / commented-out / absent / prefix guard),
lemma extraction (basic / attributes / anonymous / commented-out),
and the parse_string contract. Verified end-to-end against a real
788-line Tropical.thy: extracts theory name and all 55 theorems/lemmas.

Audit of all 50 prover backends confirmed Isabelle was the only truly
stubbed one. metamath.rs and typed_wasm.rs are intentionally pure-Rust
in-process verifiers. The other 47 backends all spawn real solver
subprocesses.

Note: deployment to echidna-nesy on Fly.io requires the container to
bundle the `isabelle` binary on $PATH; otherwise Command::new fails at
runtime and verify_proof returns Ok(false) with a context error.

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>

Author: hyperpolymath

.machine_readable/6a2/STATE.a2ml

@@ -5,7 +5,7 @@
 [metadata]
 project = "echidna"
 version = "2.0.0"
-last-updated = "2026-03-29"
+last-updated = "2026-04-05"
 status = "active"
 
 [project-context]
@@ -41,3 +41,19 @@ changes = [
 ]
 test-counts = { rust = 756, julia = 63, shell-checks = 68, benchmarks = 13 }
 crg-c-status = "COMPLETE: unit + smoke + build + P2P + E2E + reflexive + contract + aspect + benchmarks baselined"
+
+[session-2026-04-05]
+summary = "Isabelle prover backend de-stubbed: real theory parser + isabelle process invocation"
+changes = [
+  "Audited all 50 prover backends for content-discarding parse_string stubs: only isabelle.rs was stubbed",
+  "Verified metamath.rs and typed_wasm.rs are legitimate pure-Rust verifiers (no subprocess needed by design)",
+  "isabelle.rs parse_string now extracts theory name and top-level theorem|lemma|corollary declarations",
+  "Added strip_isabelle_comments helper with nested (* ... *) block-comment support",
+  "isabelle.rs verify_proof now writes raw .thy content to a unique temp dir and invokes `isabelle process -l Main -e use_thys` (filename matches theory name, as Isabelle requires)",
+  "Fixed pre-existing bug: verify_proof previously wrote echidna_verify.thy containing `theory GeneratedProof`, which isabelle build would reject on filename/theory mismatch",
+  "Added 9 unit tests covering comment stripping, theory name extraction (basic/commented/absent/prefix-guard), lemma extraction (basic/attributes/anonymous/commented), and parse_string contract",
+  "Verified against real-world Tropical.thy (788 lines): parser correctly extracts theory name and all 55 theorems/lemmas",
+  "Deployment note: echidna-nesy Fly container must bundle the `isabelle` binary on $PATH before real verification fires at runtime — otherwise Command::new returns error and verify_proof returns Ok(false)",
+]
+test-counts = { rust = 765, julia = 63, shell-checks = 68, benchmarks = 13, isabelle-module = 13 }
+stub-audit-result = "Only Isabelle was truly stubbed; all other 47 external-solver backends spawn real subprocesses. 2 backends (metamath, typed_wasm) are intentionally pure-Rust in-process verifiers."

CHANGELOG.md

@@ -5,6 +5,50 @@ All notable changes to ECHIDNA will be documented in this file.
 The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
 and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html).
 
+## [Unreleased] - 2026-04-05
+
+### Fixed
+
+- **Isabelle prover backend de-stubbed** (`src/rust/provers/isabelle.rs`).
+  `parse_string` previously discarded its `content` argument and always
+  emitted a single `Term::Const("True")` goal, which `verify_proof` then
+  short-circuited to `Ok(true)` — Isabelle was never actually invoked.
+  It now extracts the theory name and top-level `theorem|lemma|corollary`
+  declarations with nested-comment-aware scanning, stashes the raw `.thy`
+  content in `ProofState.metadata["raw_thy_content"]`, and `verify_proof`
+  writes that content to a unique per-invocation temp directory under the
+  correct filename (Isabelle requires `<theory_name>.thy`) before invoking
+  `isabelle process -l Main -e 'use_thys ["<path>"]'`.
+- **Stale scaffolded temp-file path** in Isabelle's fallback verification
+  path: previously wrote `echidna_verify.thy` containing
+  `theory GeneratedProof`, causing filename/theory-name mismatch rejection
+  by `isabelle build`. Now writes `GeneratedProof.thy` in a unique temp dir.
+
+### Added
+
+- `strip_isabelle_comments` helper for the Isabelle backend (handles nested
+  `(* ... *)` blocks).
+- 9 new unit tests for the Isabelle theory-header parsers (`test_strip_*`,
+  `test_extract_theory_name_*`, `test_extract_lemma_names_*`) and the
+  `parse_string` contract (metadata populated, goals non-trivial, context
+  theorems enumerated, empty-theory fallback goal).
+- Parser verified against a real 788-line `Tropical.thy` (tropical semiring
+  formalisation): extracts theory name and all 55 theorems/lemmas.
+
+### Notes
+
+- Deployment of this fix to `echidna-nesy` on Fly.io requires rebuilding
+  the container with the `isabelle` binary on `$PATH`. Without it,
+  `verify_proof` returns `Ok(false)` with a `"Failed to run Isabelle
+  process"` context error.
+- Audit of all 50 prover backends confirmed Isabelle was the only truly
+  stubbed one. `metamath.rs` and `typed_wasm.rs` are intentionally pure-Rust
+  in-process verifiers (no subprocess needed by design). The remaining 47
+  external-solver backends all spawn real solver subprocesses via
+  `Command::new`.
+
+---
+
 ## [1.6.1] - 2026-03-23
 
 ### Fixed