feat(provers): close Phase 4 — 6 DL/probabilistic/B-method/comp-crypto backends

Add the six backends from `ECHIDNA-EXPANSION-TOMORROW`'s Phase 4
("DL + probabilistic + comp-crypto"), completing the entire
expansion roadmap.  Each follows the dafny.rs / gnatprove.rs
template with three-stage shape: format serializer (`to_<fmt>`),
output parser (`parse_result`), 6+ unit tests.

New backends, sub-tier, FFI u8, trust tier:
  - ELK         (5h, 135, 3) — OWL 2 EL classifier
  - Konclude    (5h, 136, 3) — full SROIQ DL reasoner
  - Storm       (5i, 137, 2) — modern probabilistic model checker
  - ProB        (5j, 138, 2) — B-method / Event-B model checker
  - EasyCrypt   (5k, 139, 3) — game-based crypto proof assistant
  - CryptoVerif (5l, 140, 3) — automated computational crypto prover

Composes into the four-corner crypto-verification matrix:
  symbolic-automatic  → ProVerif
  symbolic-interactive → Tamarin
  computational-interactive → EasyCrypt
  computational-automatic   → CryptoVerif

Wired through:
  - ProverKind enum + factory dispatch
  - FromStr for CLI surface (multiple aliases each)
  - all() backend list
  - complexity / trust / implementation_time / default_executable
    tables
  - FFI kind_to_u8 / kind_from_u8 (135–140)
  - Phase 3 boundary test updated 134 → 140

40 new tests across 6 files; 972 lib tests passing
(up from 932 at session start; 13 phase 3+4 tests above the
867-baseline pre-Phase-3).  panic-attack assail clean
(0 critical / 0 high / 0 tainted on all six).

Phase 4 closes the expansion roadmap: with this and the prior
Phase 3 commit (dec54bf), every 🟡 OPEN entry from
`ECHIDNA-EXPANSION-TOMORROW-2026-04-28.md` is shipped.

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

Author: hyperpolymath

src/rust/ffi/mod.rs

@@ -536,6 +536,13 @@ pub fn kind_from_u8(kind: u8) -> Option<ProverKind> {
         132 => Some(ProverKind::IleanCoP),
         133 => Some(ProverKind::NanoCoP),
         134 => Some(ProverKind::MetTeL2),
+        // Phase 4 (2026-04-27): DL + probabilistic + B-method + computational crypto.
+        135 => Some(ProverKind::ELK),
+        136 => Some(ProverKind::Konclude),
+        137 => Some(ProverKind::Storm),
+        138 => Some(ProverKind::ProB),
+        139 => Some(ProverKind::EasyCrypt),
+        140 => Some(ProverKind::CryptoVerif),
         _ => None,
     }
 }
@@ -1284,6 +1291,13 @@ pub fn kind_to_u8(kind: ProverKind) -> u8 {
         ProverKind::IleanCoP => 132,
         ProverKind::NanoCoP => 133,
         ProverKind::MetTeL2 => 134,
+        // Phase 4 (2026-04-27): DL + probabilistic + B-method + computational crypto.
+        ProverKind::ELK => 135,
+        ProverKind::Konclude => 136,
+        ProverKind::Storm => 137,
+        ProverKind::ProB => 138,
+        ProverKind::EasyCrypt => 139,
+        ProverKind::CryptoVerif => 140,
     }
 }
 
@@ -1468,12 +1482,13 @@ mod tests {
 
     #[test]
     fn test_kind_from_u8_out_of_range() {
-        // 0–134 are valid; 135+ are out of range.
-        // (Boundary moved to 134 on 2026-04-27 adding Phase 3
-        // backends — KeYmaeraX (128), Qepcad (129), Redlog (130),
-        // MleanCoP (131), IleanCoP (132), NanoCoP (133), MetTeL2 (134).
-        // Previous boundary was 127 — Phase 1a/1b ATPs + Phase 5.)
-        assert!(kind_from_u8(135).is_none());
+        // 0–140 are valid; 141+ are out of range.
+        // (Boundary moved to 140 on 2026-04-27 adding Phase 4
+        // backends — ELK (135), Konclude (136), Storm (137),
+        // ProB (138), EasyCrypt (139), CryptoVerif (140).
+        // Previous boundary was 134 — Phase 3 connection-method /
+        // CAD / KeYmaeraX / MetTeL2.)
+        assert!(kind_from_u8(141).is_none());
         assert!(kind_from_u8(200).is_none());
         assert!(kind_from_u8(255).is_none());
     }

src/rust/provers/cryptoverif.rs

@@ -0,0 +1,294 @@
+// SPDX-FileCopyrightText: 2026 ECHIDNA Project Team
+// SPDX-License-Identifier: PMPL-1.0-or-later
+
+//! CryptoVerif backend — automatic prover for cryptographic protocols
+//! in the computational model.
+//!
+//! CryptoVerif is the **automatic** counterpart to EasyCrypt's
+//! interactive proof assistant: it produces concrete-security proofs
+//! by automated game-hopping using a built-in indistinguishability
+//! library.  It was used to prove the formal security of TLS 1.3,
+//! Signal, WireGuard, and Kerberos.
+//!
+//! ## Why this backend exists
+//!
+//! EasyCrypt produces interactive proofs with concrete-security
+//! bounds.  CryptoVerif produces *automated* proofs in the same model.
+//! Together they cover the computational-crypto verification space.
+//! ECHIDNA already has Tamarin and ProVerif (symbolic) — adding both
+//! computational tools gives us the four-corner crypto-verification
+//! matrix: symbolic-automatic (ProVerif), symbolic-interactive
+//! (Tamarin), computational-interactive (EasyCrypt),
+//! computational-automatic (CryptoVerif).
+//!
+//! ## Input format
+//!
+//! `.ocv` — CryptoVerif source (recommended modern syntax).
+//! `.cv`  — legacy format (still supported by upstream).
+//!
+//! ## CLI invocation
+//!
+//! `cryptoverif -in <ocv-file> -out <result-dir>` for full automation.
+//! `cryptoverif -interactive` for hand-driven game-hopping.
+//!
+//! ## Output parsing
+//!
+//! CryptoVerif emits per-game status with a final verdict line:
+//!
+//! - `RESULT Proved <event-or-property>`
+//! - `RESULT Could not prove ...`
+//! - `Cannot prove ...` (failure mid-script)
+//!
+//! ## Integration tier
+//!
+//! Tier-5l / Phase-4.  Trust tier 3 (small game-hopping engine,
+//! peer-reviewed, used for TLS 1.3 / Signal proofs).  Complexity 4
+//! (probabilistic process calculi + indistinguishability library +
+//! cryptographic-game search).
+
+#![allow(dead_code)]
+
+use anyhow::{Context, Result};
+use async_trait::async_trait;
+use std::path::PathBuf;
+use std::process::Stdio;
+use tokio::io::AsyncWriteExt;
+use tokio::process::Command;
+
+use super::{ProverBackend, ProverConfig, ProverKind};
+use crate::core::{Goal, ProofState, Tactic, TacticResult, Term};
+
+/// CryptoVerif backend for automated computational crypto proofs.
+pub struct CryptoVerifBackend {
+    config: ProverConfig,
+}
+
+impl CryptoVerifBackend {
+    pub fn new(config: ProverConfig) -> Self {
+        CryptoVerifBackend { config }
+    }
+
+    /// Render a `ProofState` into a minimal CryptoVerif `.ocv` file.
+    ///
+    /// Each axiom is emitted as a `def` declaration; the goal is
+    /// emitted as the `query` line that drives the prover.
+    fn to_ocv(state: &ProofState) -> String {
+        let mut ocv = String::new();
+        ocv.push_str("(* SPDX-License-Identifier: PMPL-1.0-or-later *)\n");
+        ocv.push_str("(* CryptoVerif input synthesised by ECHIDNA *)\n\n");
+        for axiom in &state.context.axioms {
+            ocv.push_str(&format!("def {}.\n", axiom));
+        }
+        if let Some(goal) = state.goals.first() {
+            ocv.push_str(&format!("\nquery {}.\n", goal.target));
+        }
+        ocv.push_str("\nprocess 0\n");
+        ocv
+    }
+
+    /// Parse CryptoVerif's stdout to a boolean verdict.
+    fn parse_result(output: &str) -> Result<bool> {
+        let lower = output.to_ascii_lowercase();
+        let positive = [
+            "result proved",
+            "all queries proved",
+            "successfully proved",
+            "[ok] proof complete",
+        ];
+        let negative = [
+            "could not prove",
+            "cannot prove",
+            "result not proved",
+            "result rand_failure",
+            "[error]",
+        ];
+        if positive.iter().any(|m| lower.contains(m)) {
+            return Ok(true);
+        }
+        if negative.iter().any(|m| lower.contains(m)) {
+            return Ok(false);
+        }
+        Err(anyhow::anyhow!(
+            "CryptoVerif output inconclusive: {}",
+            output.lines().take(10).collect::<Vec<_>>().join("\n")
+        ))
+    }
+}
+
+#[async_trait]
+impl ProverBackend for CryptoVerifBackend {
+    fn kind(&self) -> ProverKind {
+        ProverKind::CryptoVerif
+    }
+
+    async fn version(&self) -> Result<String> {
+        let output = Command::new(&self.config.executable)
+            .arg("-version")
+            .output()
+            .await
+            .context("Failed to run cryptoverif -version")?;
+        let stdout = String::from_utf8_lossy(&output.stdout);
+        let stderr = String::from_utf8_lossy(&output.stderr);
+        let version = if !stdout.is_empty() {
+            stdout.lines().next().unwrap_or("cryptoverif").to_string()
+        } else {
+            stderr.lines().next().unwrap_or("cryptoverif").to_string()
+        };
+        Ok(version.trim().to_string())
+    }
+
+    async fn parse_file(&self, path: PathBuf) -> Result<ProofState> {
+        let content = super::bounded_read_proof_file(&path)
+            .await
+            .context("Failed to read .ocv file")?;
+        let mut state = self.parse_string(&content).await?;
+        state.metadata.insert(
+            "source_path".to_string(),
+            serde_json::Value::String(path.to_string_lossy().into_owned()),
+        );
+        Ok(state)
+    }
+
+    async fn parse_string(&self, content: &str) -> Result<ProofState> {
+        let mut state = ProofState::default();
+        state.metadata.insert(
+            "ocv_source".to_string(),
+            serde_json::Value::String(content.to_string()),
+        );
+        for line in content.lines() {
+            let trimmed = line.trim();
+            if trimmed.is_empty() || trimmed.starts_with("(*") {
+                continue;
+            }
+            if let Some(rest) = trimmed.strip_prefix("def ") {
+                let body = rest.trim_end_matches('.').trim();
+                if !body.is_empty() {
+                    state.context.axioms.push(body.to_string());
+                }
+            } else if let Some(rest) = trimmed.strip_prefix("query ") {
+                let body = rest.trim_end_matches('.').trim();
+                state.goals.push(Goal {
+                    id: format!("goal_{}", state.goals.len()),
+                    target: Term::Const(body.to_string()),
+                    hypotheses: vec![],
+                });
+            }
+        }
+        Ok(state)
+    }
+
+    async fn apply_tactic(&self, _state: &ProofState, _tactic: &Tactic) -> Result<TacticResult> {
+        Err(anyhow::anyhow!(
+            "CryptoVerif is automation-first; interactive game-hopping is out of band"
+        ))
+    }
+
+    async fn verify_proof(&self, state: &ProofState) -> Result<bool> {
+        let ocv = Self::to_ocv(state);
+        let mut child = Command::new(&self.config.executable)
+            .arg("-in")
+            .arg("/dev/stdin")
+            .stdin(Stdio::piped())
+            .stdout(Stdio::piped())
+            .stderr(Stdio::piped())
+            .spawn()
+            .context("Failed to spawn cryptoverif")?;
+        {
+            let stdin = child
+                .stdin
+                .as_mut()
+                .ok_or_else(|| anyhow::anyhow!("Failed to open cryptoverif stdin"))?;
+            stdin
+                .write_all(ocv.as_bytes())
+                .await
+                .context("Failed to write to cryptoverif stdin")?;
+        }
+        let output = child
+            .wait_with_output()
+            .await
+            .context("Failed to wait for cryptoverif")?;
+        let combined = format!(
+            "{}\n{}",
+            String::from_utf8_lossy(&output.stdout),
+            String::from_utf8_lossy(&output.stderr)
+        );
+        Self::parse_result(&combined)
+    }
+
+    async fn export(&self, state: &ProofState) -> Result<String> {
+        Ok(Self::to_ocv(state))
+    }
+
+    async fn suggest_tactics(
+        &self,
+        _state: &ProofState,
+        _limit: usize,
+    ) -> Result<Vec<Tactic>> {
+        Ok(vec![])
+    }
+
+    async fn search_theorems(&self, _pattern: &str) -> Result<Vec<String>> {
+        Ok(vec![])
+    }
+
+    fn config(&self) -> &ProverConfig {
+        &self.config
+    }
+
+    fn set_config(&mut self, config: ProverConfig) {
+        self.config = config;
+    }
+}
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+
+    #[test]
+    fn test_cryptoverif_kind() {
+        let config = ProverConfig::default();
+        let backend = CryptoVerifBackend::new(config);
+        assert_eq!(backend.kind(), ProverKind::CryptoVerif);
+    }
+
+    #[test]
+    fn test_cryptoverif_to_ocv_emits_query() {
+        let mut state = ProofState::default();
+        state.context.axioms.push("MAC_secure".to_string());
+        state.goals.push(Goal {
+            id: "goal_0".to_string(),
+            target: Term::Const("event(authenticated(m)) ==> exists s. signed(s, m)".to_string()),
+            hypotheses: vec![],
+        });
+        let ocv = CryptoVerifBackend::to_ocv(&state);
+        assert!(ocv.contains("def MAC_secure"));
+        assert!(ocv.contains("query event(authenticated(m))"));
+        assert!(ocv.contains("process 0"));
+    }
+
+    #[test]
+    fn test_cryptoverif_parse_result_proved() {
+        assert!(CryptoVerifBackend::parse_result("RESULT Proved authentication").expect("parse"));
+    }
+
+    #[test]
+    fn test_cryptoverif_parse_result_could_not_prove() {
+        assert!(!CryptoVerifBackend::parse_result("RESULT Could not prove confidentiality")
+            .expect("parse"));
+    }
+
+    #[test]
+    fn test_cryptoverif_parse_result_silence_errors() {
+        assert!(CryptoVerifBackend::parse_result("warning: nothing").is_err());
+    }
+
+    #[tokio::test]
+    async fn test_cryptoverif_parse_string_extracts_def_and_query() {
+        let config = ProverConfig::default();
+        let backend = CryptoVerifBackend::new(config);
+        let ocv = "def MAC_secure.\nquery event(auth(m)) ==> sender(m).\n";
+        let state = backend.parse_string(ocv).await.expect("parse_string");
+        assert_eq!(state.context.axioms.len(), 1);
+        assert_eq!(state.goals.len(), 1);
+    }
+}