telltale-bridge 11.1.0

//! Lean runner projection export via the protocol-machine binary.

use super::*;
use std::io::Write;

impl LeanRunner {
    /// Default path to the protocol-machine runner binary (relative to workspace root).
    pub const PROTOCOL_MACHINE_RUNNER_BINARY_PATH: &'static str =
        "lean/.lake/build/bin/protocol_machine_runner";
    /// Fallback source-backed launcher for the protocol-machine runner.
    pub const PROTOCOL_MACHINE_RUNNER_FALLBACK_PATH: &'static str =
        "scripts/lean/protocol-machine-runner.sh";

    /// Get the full path to the protocol-machine runner binary.
    fn get_protocol_machine_runner_path() -> Option<PathBuf> {
        Self::find_workspace_root().and_then(|root| {
            let native = root.join(Self::PROTOCOL_MACHINE_RUNNER_BINARY_PATH);
            if native.is_file() {
                return Some(native);
            }
            let fallback = root.join(Self::PROTOCOL_MACHINE_RUNNER_FALLBACK_PATH);
            if fallback.is_file() {
                return Some(fallback);
            }
            None
        })
    }

    /// Check if the validator binary is available for projection export.
    #[must_use]
    pub fn is_projection_available() -> bool {
        Self::is_available()
    }

    /// Project a GlobalType for a list of roles using the Lean validator export mode.
    ///
    /// Writes the GlobalType JSON to a temp file, runs
    /// `telltale_validator --export-all-projections`, and parses the projections.
    ///
    /// # Output format (parsed from output file)
    ///
    /// ```json
    /// {
    ///   "success": true,
    ///   "projections": { "A": { "kind": "send", ... }, "B": { "kind": "recv", ... } }
    /// }
    /// ```
    pub fn project(
        &self,
        global_json: &Value,
        roles: &[String],
    ) -> Result<std::collections::HashMap<String, Value>, LeanRunnerError> {
        let mut input_file = NamedTempFile::new()?;
        serde_json::to_writer(&mut input_file, global_json)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;
        input_file.flush()?;

        let output_file = NamedTempFile::new()?;
        let output_path = output_file.path().to_path_buf();

        let mut command = Command::new(&self.binary_path);
        command
            .arg("--export-all-projections")
            .arg(input_file.path())
            .arg("--output")
            .arg(&output_path);
        let output = self.run_command_with_timeout(command, "project_all")?;

        if !output.status.success() {
            let stderr = String::from_utf8_lossy(&output.stderr).to_string();
            return Err(LeanRunnerError::ProcessFailed {
                code: output.status.code().unwrap_or(-1),
                stderr,
            });
        }

        let output_contents = std::fs::read_to_string(&output_path)?;
        let payload: Value = serde_json::from_str(&output_contents)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;

        if let Some(false) = payload.get("success").and_then(|v| v.as_bool()) {
            let err = payload
                .get("error")
                .and_then(|v| v.as_str())
                .unwrap_or("Lean export failed");
            return Err(LeanRunnerError::ParseError(err.to_string()));
        }

        let projections_map = crate::projection_payload::parse_projections_field(&payload)
            .map_err(LeanRunnerError::ParseError)?;

        if roles.is_empty() {
            return Ok(projections_map);
        }

        let mut selected = std::collections::HashMap::new();
        for role in roles {
            let projection = projections_map.get(role).ok_or_else(|| {
                LeanRunnerError::ParseError(format!("missing projection for role {role}"))
            })?;
            selected.insert(role.clone(), projection.clone());
        }
        Ok(selected)
    }

    /// Check conservative async-subtyping in Lean.
    ///
    /// Invokes the Lean validator with `--check-async-subtype` mode and returns
    /// whether the subtype relation holds.
    pub fn check_async_subtype(
        &self,
        subtype_json: &Value,
        supertype_json: &Value,
    ) -> Result<bool, LeanRunnerError> {
        let subtype_file = NamedTempFile::new()?;
        let supertype_file = NamedTempFile::new()?;
        let output_file = NamedTempFile::new()?;

        std::fs::write(
            subtype_file.path(),
            serde_json::to_string_pretty(subtype_json)
                .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?,
        )?;
        std::fs::write(
            supertype_file.path(),
            serde_json::to_string_pretty(supertype_json)
                .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?,
        )?;

        let mut command = Command::new(&self.binary_path);
        command
            .arg("--check-async-subtype")
            .arg(subtype_file.path())
            .arg(supertype_file.path())
            .arg("--output")
            .arg(output_file.path());
        let output = self.run_command_with_timeout(command, "check_async_subtype")?;

        if !output.status.success() {
            let stderr = String::from_utf8_lossy(&output.stderr).to_string();
            return Err(LeanRunnerError::ProcessFailed {
                code: output.status.code().unwrap_or(-1),
                stderr,
            });
        }

        let output_content = std::fs::read_to_string(output_file.path())?;
        let payload: Value = serde_json::from_str(&output_content)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;

        let success = payload
            .get("success")
            .and_then(|v| v.as_bool())
            .ok_or_else(|| LeanRunnerError::ParseError("missing success field".to_string()))?;
        if !success {
            let err = payload
                .get("error")
                .and_then(|v| v.as_str())
                .unwrap_or("Lean async-subtyping check failed");
            return Err(LeanRunnerError::ParseError(err.to_string()));
        }

        let result = payload
            .get("result")
            .and_then(|v| v.as_bool())
            .ok_or_else(|| LeanRunnerError::ParseError("missing result field".to_string()))?;
        Ok(result)
    }

    /// Check conservative orphan-freedom in Lean.
    ///
    /// Invokes the Lean validator with `--check-orphan-free` mode and returns
    /// whether the orphan-freedom predicate holds.
    pub fn check_orphan_free(&self, local_json: &Value) -> Result<bool, LeanRunnerError> {
        let local_file = NamedTempFile::new()?;
        let output_file = NamedTempFile::new()?;

        std::fs::write(
            local_file.path(),
            serde_json::to_string_pretty(local_json)
                .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?,
        )?;

        let mut command = Command::new(&self.binary_path);
        command
            .arg("--check-orphan-free")
            .arg(local_file.path())
            .arg("--output")
            .arg(output_file.path());
        let output = self.run_command_with_timeout(command, "check_orphan_free")?;

        if !output.status.success() {
            let stderr = String::from_utf8_lossy(&output.stderr).to_string();
            return Err(LeanRunnerError::ProcessFailed {
                code: output.status.code().unwrap_or(-1),
                stderr,
            });
        }

        let output_content = std::fs::read_to_string(output_file.path())?;
        let payload: Value = serde_json::from_str(&output_content)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;

        let success = payload
            .get("success")
            .and_then(|v| v.as_bool())
            .ok_or_else(|| LeanRunnerError::ParseError("missing success field".to_string()))?;
        if !success {
            let err = payload
                .get("error")
                .and_then(|v| v.as_str())
                .unwrap_or("Lean orphan-free check failed");
            return Err(LeanRunnerError::ParseError(err.to_string()));
        }

        let result = payload
            .get("result")
            .and_then(|v| v.as_bool())
            .ok_or_else(|| LeanRunnerError::ParseError("missing result field".to_string()))?;
        Ok(result)
    }

    /// Check whether a local type is in the regular practical fragment for automatic
    /// deadlock-freedom obligations.
    pub fn check_regular_practical_fragment(
        &self,
        local_json: &Value,
    ) -> Result<RegularPracticalFragmentCheckResult, LeanRunnerError> {
        let local_file = NamedTempFile::new()?;
        let output_file = NamedTempFile::new()?;

        std::fs::write(
            local_file.path(),
            serde_json::to_string_pretty(local_json)
                .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?,
        )?;

        let mut command = Command::new(&self.binary_path);
        command
            .arg("--check-regular-practical-fragment")
            .arg(local_file.path())
            .arg("--output")
            .arg(output_file.path());
        let output = self.run_command_with_timeout(command, "check_regular_practical_fragment")?;

        if !output.status.success() {
            let stderr = String::from_utf8_lossy(&output.stderr).to_string();
            return Err(LeanRunnerError::ProcessFailed {
                code: output.status.code().unwrap_or(-1),
                stderr,
            });
        }

        let output_content = std::fs::read_to_string(output_file.path())?;
        let payload: Value = serde_json::from_str(&output_content)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;

        let success = payload
            .get("success")
            .and_then(|v| v.as_bool())
            .ok_or_else(|| LeanRunnerError::ParseError("missing success field".to_string()))?;
        if !success {
            let err = payload
                .get("error")
                .and_then(|v| v.as_str())
                .unwrap_or("Lean regular-practical-fragment check failed");
            return Err(LeanRunnerError::ParseError(err.to_string()));
        }

        Ok(RegularPracticalFragmentCheckResult {
            result: payload
                .get("result")
                .and_then(|v| v.as_bool())
                .ok_or_else(|| LeanRunnerError::ParseError("missing result field".to_string()))?,
            reaches_communication: payload
                .get("reaches_communication")
                .and_then(|v| v.as_bool())
                .ok_or_else(|| {
                    LeanRunnerError::ParseError("missing reaches_communication field".to_string())
                })?,
            well_formed: payload
                .get("well_formed")
                .and_then(|v| v.as_bool())
                .ok_or_else(|| {
                    LeanRunnerError::ParseError("missing well_formed field".to_string())
                })?,
            full_unfold_head: payload
                .get("full_unfold_head")
                .and_then(|v| v.as_str())
                .ok_or_else(|| {
                    LeanRunnerError::ParseError("missing full_unfold_head field".to_string())
                })?
                .to_string(),
            reason: payload
                .get("reason")
                .and_then(|v| v.as_str())
                .map(str::to_string),
        })
    }

    /// Run one or more choreographies on the Lean ProtocolMachine at a given concurrency level.
    ///
    /// # Errors
    ///
    /// Returns an error if the ProtocolMachine runner binary is missing, the process fails,
    /// or the output is not valid JSON.
    pub fn run_protocol_machine(
        &self,
        choreographies: &[ChoreographyJson],
        concurrency: usize,
        max_steps: usize,
    ) -> Result<Value, LeanRunnerError> {
        let runner_path = Self::get_protocol_machine_runner_path().ok_or_else(|| {
            LeanRunnerError::BinaryNotFound(PathBuf::from(
                Self::PROTOCOL_MACHINE_RUNNER_BINARY_PATH,
            ))
        })?;

        let input = serde_json::json!({
            "schema_version": crate::schema::canonical_schema_version(),
            "choreographies": choreographies,
            "concurrency": concurrency,
            "max_steps": max_steps
        });
        let input_str = serde_json::to_string(&input)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;

        let mut child = Command::new(&runner_path)
            .stdin(std::process::Stdio::piped())
            .stdout(std::process::Stdio::piped())
            .stderr(std::process::Stdio::piped())
            .spawn()?;

        if let Some(mut stdin) = child.stdin.take() {
            stdin
                .write_all(input_str.as_bytes())
                .map_err(LeanRunnerError::TempFileError)?;
        }

        let output =
            Self::wait_with_timeout(child, Self::process_timeout(), "run_protocol_machine")?;
        let stdout = String::from_utf8_lossy(&output.stdout).to_string();
        let stderr = String::from_utf8_lossy(&output.stderr).to_string();

        if !output.status.success() {
            return Err(LeanRunnerError::ProcessFailed {
                code: output.status.code().unwrap_or(-1),
                stderr,
            });
        }

        let json: Value = serde_json::from_str(&stdout)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;
        Ok(json)
    }

    /// Export Lean's projection for a single role.
    ///
    /// Invokes the Lean runner with `--export-projection` mode and returns
    /// the JSON result containing either the computed LocalTypeR or an error.
    pub fn export_projection(
        &self,
        global_json: &Value,
        role: &str,
    ) -> Result<Value, LeanRunnerError> {
        let input_file = NamedTempFile::new()?;
        let output_file = NamedTempFile::new()?;

        std::fs::write(
            input_file.path(),
            serde_json::to_string_pretty(global_json)
                .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?,
        )?;

        let mut command = Command::new(&self.binary_path);
        command
            .arg("--export-projection")
            .arg(input_file.path())
            .arg("--role")
            .arg(role)
            .arg("--output")
            .arg(output_file.path());
        let output = self.run_command_with_timeout(command, "export_projection")?;

        if !output.status.success() {
            let stderr = String::from_utf8_lossy(&output.stderr).to_string();
            return Err(LeanRunnerError::ProcessFailed {
                code: output.status.code().unwrap_or(-1),
                stderr,
            });
        }

        let result_content = std::fs::read_to_string(output_file.path())?;
        let result: Value = serde_json::from_str(&result_content)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;
        Ok(result)
    }

    /// Export Lean's projection for all roles in a GlobalType.
    ///
    /// Invokes the Lean runner with `--export-all-projections` mode and returns
    /// the JSON result containing projections for all roles.
    pub fn export_all_projections(&self, global_json: &Value) -> Result<Value, LeanRunnerError> {
        let input_file = NamedTempFile::new()?;
        let output_file = NamedTempFile::new()?;

        std::fs::write(
            input_file.path(),
            serde_json::to_string_pretty(global_json)
                .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?,
        )?;

        let mut command = Command::new(&self.binary_path);
        command
            .arg("--export-all-projections")
            .arg(input_file.path())
            .arg("--output")
            .arg(output_file.path());
        let output = self.run_command_with_timeout(command, "export_all_projections")?;

        if !output.status.success() {
            let stderr = String::from_utf8_lossy(&output.stderr).to_string();
            return Err(LeanRunnerError::ProcessFailed {
                code: output.status.code().unwrap_or(-1),
                stderr,
            });
        }

        let result_content = std::fs::read_to_string(output_file.path())?;
        let result: Value = serde_json::from_str(&result_content)
            .map_err(|e| LeanRunnerError::ParseError(e.to_string()))?;

        Ok(result)
    }
}