telltale_lean_bridge/
runner.rs

1//! Lean Runner - Invokes the Lean validator binary.
2//!
3//! This module provides the [`LeanRunner`] struct which wraps invocation of
4//! the Lean `telltale_validator` binary for validating choreography projections.
5//!
6//! # Example
7//!
8//! ```ignore
9//! use telltale_lean_bridge::runner::LeanRunner;
10//! use serde_json::json;
11//!
12//! let runner = LeanRunner::new()?;
13//! let result = runner.validate(&choreography_json, &program_json)?;
14//! assert!(result.success);
15//! ```
16
17use serde::{Deserialize, Serialize};
18use serde_json::Value;
19use std::path::{Path, PathBuf};
20use std::process::{Child, Command, Output};
21use std::thread;
22use std::time::{Duration, Instant};
23use tempfile::NamedTempFile;
24use thiserror::Error;
25
26#[path = "runner_projection_export.rs"]
27mod projection;
28
29/// Errors from Lean runner operations.
30#[derive(Debug, Error)]
31pub enum LeanRunnerError {
32    /// The Lean binary was not found at the expected path.
33    #[error("Lean binary not found at {0}")]
34    BinaryNotFound(PathBuf),
35
36    /// Failed to create a temporary file for JSON exchange.
37    #[error("Failed to create temp file: {0}")]
38    TempFileError(#[from] std::io::Error),
39
40    /// The Lean process exited with a non-zero status.
41    #[error("Lean process failed with exit code {code}: {stderr}")]
42    ProcessFailed {
43        /// Exit code from the process.
44        code: i32,
45        /// Standard error output.
46        stderr: String,
47    },
48
49    /// Failed to parse Lean output or JSON.
50    #[error("Failed to parse Lean output: {0}")]
51    ParseError(String),
52
53    /// Validation failed with a specific reason.
54    #[error("Validation failed: {0}")]
55    ValidationFailed(String),
56
57    /// Lean process exceeded the configured timeout.
58    #[error("Lean process '{operation}' timed out after {timeout_ms}ms")]
59    TimedOut {
60        /// Operation name associated with the process invocation.
61        operation: String,
62        /// Timeout in milliseconds.
63        timeout_ms: u64,
64    },
65}
66
67/// Choreography input for the VM runner.
68#[derive(Debug, Clone, Serialize, Deserialize)]
69pub struct ChoreographyJson {
70    /// Schema version for this payload.
71    #[serde(default = "crate::schema::default_schema_version")]
72    pub schema_version: String,
73    /// Global type JSON (Lean-compatible).
74    pub global_type: Value,
75    /// Role list.
76    pub roles: Vec<String>,
77}
78
79/// Result of a Lean validation run.
80#[derive(Debug, Clone)]
81pub struct LeanValidationResult {
82    /// Whether validation succeeded.
83    pub success: bool,
84    /// The role that was validated.
85    pub role: String,
86    /// Human-readable message describing the result.
87    pub message: String,
88    /// Raw output from the Lean process.
89    pub raw_output: String,
90}
91
92/// Runner for invoking the Lean verification binary.
93///
94/// The runner manages invocation of the `telltale_validator` Lean executable,
95/// handling temporary file creation for JSON exchange and parsing results.
96pub struct LeanRunner {
97    binary_path: PathBuf,
98}
99
100impl LeanRunner {
101    /// Default path to the Lean binary (relative to workspace root).
102    pub const DEFAULT_BINARY_PATH: &'static str = "lean/.lake/build/bin/telltale_validator";
103    /// Default timeout for Lean process invocations.
104    pub const DEFAULT_TIMEOUT_MS: u64 = 120_000;
105
106    fn process_timeout() -> Duration {
107        let ms = std::env::var("TELLTALE_LEAN_TIMEOUT_MS")
108            .ok()
109            .and_then(|raw| raw.parse::<u64>().ok())
110            .unwrap_or(Self::DEFAULT_TIMEOUT_MS);
111        Duration::from_millis(ms.max(1))
112    }
113
114    fn wait_with_timeout(
115        mut child: Child,
116        timeout: Duration,
117        operation: &str,
118    ) -> Result<Output, LeanRunnerError> {
119        let start = Instant::now();
120        loop {
121            // bounded: exits on child completion or timeout
122            match child.try_wait()? {
123                Some(_) => return child.wait_with_output().map_err(LeanRunnerError::from),
124                None => {
125                    if start.elapsed() >= timeout {
126                        if let Err(err) = child.kill() {
127                            eprintln!(
128                                "best-effort child.kill failed during timeout handling: {err}"
129                            );
130                        }
131                        if let Err(err) = child.wait() {
132                            eprintln!(
133                                "best-effort child.wait failed during timeout handling: {err}"
134                            );
135                        }
136                        return Err(LeanRunnerError::TimedOut {
137                            operation: operation.to_string(),
138                            timeout_ms: u64::try_from(timeout.as_millis()).unwrap_or(u64::MAX),
139                        });
140                    }
141                    thread::sleep(Duration::from_millis(10));
142                }
143            }
144        }
145    }
146
147    fn run_command_with_timeout(
148        &self,
149        mut command: Command,
150        operation: &str,
151    ) -> Result<Output, LeanRunnerError> {
152        let child = command.spawn()?;
153        Self::wait_with_timeout(child, Self::process_timeout(), operation)
154    }
155
156    /// Get the workspace root path by walking up from the manifest directory.
157    fn find_workspace_root() -> Option<PathBuf> {
158        // Start from the manifest directory (rust/lean-bridge)
159        let manifest_dir = env!("CARGO_MANIFEST_DIR");
160        let mut path = PathBuf::from(manifest_dir);
161
162        // Walk up looking for the lean/.lake/ directory as a workspace root marker.
163        for _ in 0..5 {
164            if path.join("lean/.lake").is_dir() {
165                return Some(path);
166            }
167            if !path.pop() {
168                break;
169            }
170        }
171        None
172    }
173
174    /// Get the full path to the Lean binary.
175    fn get_binary_path() -> Option<PathBuf> {
176        Self::find_workspace_root()
177            .map(|root| root.join(Self::DEFAULT_BINARY_PATH))
178            .filter(|p| p.exists())
179    }
180
181    /// Create a new LeanRunner with the default binary path.
182    ///
183    /// # Errors
184    ///
185    /// Returns [`LeanRunnerError::BinaryNotFound`] if the binary doesn't exist.
186    pub fn new() -> Result<Self, LeanRunnerError> {
187        match Self::get_binary_path() {
188            Some(path) => Ok(Self { binary_path: path }),
189            None => Err(LeanRunnerError::BinaryNotFound(PathBuf::from(
190                Self::DEFAULT_BINARY_PATH,
191            ))),
192        }
193    }
194
195    /// Create a LeanRunner with a custom binary path.
196    ///
197    /// # Errors
198    ///
199    /// Returns [`LeanRunnerError::BinaryNotFound`] if the binary doesn't exist.
200    pub fn with_binary_path(path: impl AsRef<Path>) -> Result<Self, LeanRunnerError> {
201        let binary_path = PathBuf::from(path.as_ref());
202        if !binary_path.exists() || !binary_path.is_file() {
203            return Err(LeanRunnerError::BinaryNotFound(binary_path));
204        }
205        Ok(Self { binary_path })
206    }
207
208    /// Try to create a runner, returning None if the binary is unavailable.
209    ///
210    /// This is useful for tests that should skip gracefully when Lean isn't built.
211    #[must_use]
212    pub fn try_new() -> Option<Self> {
213        Self::new().ok()
214    }
215
216    /// Create a LeanRunner for projection export (uses the validator binary).
217    ///
218    /// # Errors
219    ///
220    /// Returns [`LeanRunnerError::BinaryNotFound`] if the validator binary doesn't exist.
221    pub fn for_projection() -> Result<Self, LeanRunnerError> {
222        Self::new()
223    }
224
225    /// Check if the Lean binary is available at the default path.
226    #[must_use]
227    pub fn is_available() -> bool {
228        Self::get_binary_path().is_some()
229    }
230
231    /// Require that the Lean binary is available.
232    ///
233    /// This function is intended for CI environments where Lean tests should not
234    /// be silently skipped. It panics with instructions if the binary is missing.
235    ///
236    /// # Panics
237    ///
238    /// Panics if the Lean binary is not available.
239    pub fn require_available() {
240        if !Self::is_available() {
241            panic!(
242                "\n\
243                ╔══════════════════════════════════════════════════════════════════╗\n\
244                ║  LEAN VERIFICATION REQUIRED                                       ║\n\
245                ╠══════════════════════════════════════════════════════════════════╣\n\
246                ║  The Lean binary is required but not found.                       ║\n\
247                ║                                                                   ║\n\
248                ║  To build Lean:                                                   ║\n\
249                ║    cd lean && lake build telltale_validator                       ║\n\
250                ║                                                                   ║\n\
251                ║  Or with Nix:                                                     ║\n\
252                ║    nix develop --command bash -c \"cd lean && lake build telltale_validator\"         ║\n\
253                ║                                                                   ║\n\
254                ║  Expected path: {path}           \n\
255                ╚══════════════════════════════════════════════════════════════════╝\n",
256                path = Self::DEFAULT_BINARY_PATH
257            );
258        }
259    }
260
261    /// Run validation with choreography and program JSON.
262    ///
263    /// The choreography JSON should be a GlobalType JSON object.
264    ///
265    /// The program JSON should have the format:
266    /// ```json
267    /// {
268    ///   "role": "A",
269    ///   "local_type": { "kind": "send", ... }
270    /// }
271    /// ```
272    ///
273    /// # Errors
274    ///
275    /// Returns an error if:
276    /// - Temporary files cannot be created
277    /// - JSON serialization fails
278    /// - The Lean process fails to execute
279    /// - Output parsing fails
280    pub fn validate(
281        &self,
282        choreography_json: &Value,
283        program_json: &Value,
284    ) -> Result<LeanValidationResult, LeanRunnerError> {
285        // Create temp files
286        let choreo_file = NamedTempFile::new()?;
287        let program_file = NamedTempFile::new()?;
288        let json_log = NamedTempFile::new()?;
289
290        // Write JSON to temp files
291        std::fs::write(
292            choreo_file.path(),
293            serde_json::to_string_pretty(choreography_json)
294                .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?,
295        )?;
296        std::fs::write(
297            program_file.path(),
298            serde_json::to_string_pretty(program_json)
299                .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?,
300        )?;
301
302        // Invoke Lean runner
303        let mut command = Command::new(&self.binary_path);
304        command
305            .arg("--choreography")
306            .arg(choreo_file.path())
307            .arg("--program")
308            .arg(program_file.path())
309            .arg("--json-log")
310            .arg(json_log.path());
311        let output = self.run_command_with_timeout(command, "validate")?;
312
313        self.parse_output(output, json_log.path())
314    }
315
316    /// Parse the output from the Lean runner process.
317    fn parse_output(
318        &self,
319        output: Output,
320        json_log_path: &Path,
321    ) -> Result<LeanValidationResult, LeanRunnerError> {
322        let stdout = String::from_utf8_lossy(&output.stdout).to_string();
323        let stderr = String::from_utf8_lossy(&output.stderr).to_string();
324
325        if !output.status.success() {
326            return Err(LeanRunnerError::ProcessFailed {
327                code: output.status.code().unwrap_or(-1),
328                stderr,
329            });
330        }
331
332        if !json_log_path.exists() {
333            return Err(LeanRunnerError::ParseError(
334                "Lean validator completed but did not emit a JSON log".to_string(),
335            ));
336        }
337
338        let log_content = std::fs::read_to_string(json_log_path)?;
339        if log_content.trim().is_empty() {
340            return Err(LeanRunnerError::ParseError(
341                "Lean validator emitted an empty JSON log".to_string(),
342            ));
343        }
344        let log_json: Value = serde_json::from_str(&log_content)
345            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;
346
347        self.parse_json_log(&log_json, stdout)
348    }
349
350    /// Parse the JSON log output from the runner.
351    fn parse_json_log(
352        &self,
353        log: &Value,
354        raw_output: String,
355    ) -> Result<LeanValidationResult, LeanRunnerError> {
356        let role = log
357            .get("role")
358            .and_then(Value::as_str)
359            .ok_or_else(|| LeanRunnerError::ParseError("missing string field: role".to_string()))?
360            .to_string();
361        let status = log.get("status").and_then(Value::as_str).ok_or_else(|| {
362            LeanRunnerError::ParseError("missing string field: status".to_string())
363        })?;
364        let success = match status {
365            "ok" => true,
366            "error" => false,
367            other => {
368                return Err(LeanRunnerError::ParseError(format!(
369                    "invalid status value in JSON log: {other}"
370                )))
371            }
372        };
373        let message = log
374            .get("message")
375            .and_then(Value::as_str)
376            .unwrap_or("")
377            .to_string();
378
379        Ok(LeanValidationResult {
380            success,
381            role,
382            message,
383            raw_output,
384        })
385    }
386}
387
388#[cfg(test)]
389mod tests {
390    use super::*;
391    use std::process::Command;
392    use std::time::Duration;
393
394    #[test]
395    fn test_is_available_returns_bool() {
396        // Just verify it doesn't panic and returns a bool
397        let _available = LeanRunner::is_available();
398    }
399
400    #[test]
401    fn test_try_new_returns_option() {
402        // Should return Some if binary exists, None otherwise
403        let result = LeanRunner::try_new();
404        if LeanRunner::is_available() {
405            assert!(result.is_some());
406        } else {
407            assert!(result.is_none());
408        }
409    }
410
411    #[test]
412    fn test_with_nonexistent_path_fails() {
413        let result = LeanRunner::with_binary_path("/nonexistent/path/to/binary");
414        assert!(matches!(result, Err(LeanRunnerError::BinaryNotFound(_))));
415    }
416
417    fn successful_output() -> std::process::Output {
418        Command::new("sh")
419            .arg("-c")
420            .arg("true")
421            .output()
422            .expect("invoke shell")
423    }
424
425    #[test]
426    fn test_parse_output_requires_json_log_file() {
427        let runner = LeanRunner {
428            binary_path: PathBuf::from("/tmp/fake-validator"),
429        };
430        let missing = std::env::temp_dir().join("missing-validator-log.json");
431        let result = runner.parse_output(successful_output(), &missing);
432        assert!(matches!(result, Err(LeanRunnerError::ParseError(_))));
433    }
434
435    #[test]
436    fn test_parse_output_rejects_empty_json_log() {
437        let runner = LeanRunner {
438            binary_path: PathBuf::from("/tmp/fake-validator"),
439        };
440        let empty = NamedTempFile::new().expect("create temp file");
441        let result = runner.parse_output(successful_output(), empty.path());
442        assert!(matches!(result, Err(LeanRunnerError::ParseError(_))));
443    }
444
445    #[test]
446    fn test_parse_json_log_rejects_invalid_status() {
447        let runner = LeanRunner {
448            binary_path: PathBuf::from("/tmp/fake-validator"),
449        };
450        let log = serde_json::json!({
451            "role": "A",
452            "status": "maybe",
453            "message": "test"
454        });
455        let result = runner.parse_json_log(&log, String::new());
456        assert!(matches!(result, Err(LeanRunnerError::ParseError(_))));
457    }
458
459    #[test]
460    fn test_parse_json_log_success() {
461        let runner = LeanRunner {
462            binary_path: PathBuf::from("/tmp/fake-validator"),
463        };
464        let log = serde_json::json!({
465            "role": "A",
466            "status": "ok",
467            "message": "coherent"
468        });
469        let result = runner
470            .parse_json_log(&log, "stdout".to_string())
471            .expect("parse valid log");
472        assert!(result.success);
473        assert_eq!(result.role, "A");
474        assert_eq!(result.message, "coherent");
475    }
476
477    #[test]
478    fn test_wait_with_timeout_returns_timeout_error() {
479        let child = Command::new("sh")
480            .arg("-c")
481            .arg("sleep 1")
482            .spawn()
483            .expect("spawn sleep");
484        let result = LeanRunner::wait_with_timeout(child, Duration::from_millis(10), "test_sleep");
485        assert!(matches!(result, Err(LeanRunnerError::TimedOut { .. })));
486    }
487}
telltale_lean_bridge/runner.rs

telltale_lean_bridge/
runner.rs
