Struct LeanRunner 

pub struct LeanRunner { /* private fields */ }

Runner for invoking the Lean verification binary.

The runner manages invocation of the telltale_validator Lean executable, handling temporary file creation for JSON exchange and parsing results.

Implementations

impl LeanRunner

pub const PROTOCOL_MACHINE_RUNNER_BINARY_PATH: &'static str = "lean/.lake/build/bin/protocol_machine_runner"

Default path to the protocol-machine runner binary (relative to workspace root).

pub const PROTOCOL_MACHINE_RUNNER_FALLBACK_PATH: &'static str = "scripts/lean/protocol-machine-runner.sh"

Fallback source-backed launcher for the protocol-machine runner.

pub fn is_projection_available() -> bool

Check if the validator binary is available for projection export.

pub fn project( &self, global_json: &Value, roles: &[String], ) -> Result<HashMap<String, Value>, LeanRunnerError>

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)

{
  "success": true,
  "projections": { "A": { "kind": "send", ... }, "B": { "kind": "recv", ... } }
}

pub fn check_async_subtype( &self, subtype_json: &Value, supertype_json: &Value, ) -> Result<bool, LeanRunnerError>

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_orphan_free( &self, local_json: &Value, ) -> Result<bool, LeanRunnerError>

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_regular_practical_fragment( &self, local_json: &Value, ) -> Result<RegularPracticalFragmentCheckResult, LeanRunnerError>

Check whether a local type is in the regular practical fragment for automatic deadlock-freedom obligations.

pub fn run_protocol_machine( &self, choreographies: &[ChoreographyJson], concurrency: usize, max_steps: usize, ) -> Result<Value, LeanRunnerError>

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 export_projection( &self, global_json: &Value, role: &str, ) -> Result<Value, LeanRunnerError>

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_all_projections( &self, global_json: &Value, ) -> Result<Value, LeanRunnerError>

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.

impl LeanRunner

pub const DEFAULT_BINARY_PATH: &'static str = "lean/.lake/build/bin/telltale_validator"

Default path to the Lean binary (relative to workspace root).

pub const DEFAULT_TIMEOUT_MS: u64 = 120_000

Default timeout for Lean process invocations.

pub fn new() -> Result<Self, LeanRunnerError>

Create a new LeanRunner with the default binary path.

Errors

Returns LeanRunnerError::BinaryNotFound if the binary doesn’t exist.

pub fn with_binary_path(path: impl AsRef<Path>) -> Result<Self, LeanRunnerError>

Create a LeanRunner with a custom binary path.

Errors

Returns LeanRunnerError::BinaryNotFound if the binary doesn’t exist.

pub fn try_new() -> Option<Self>

Try to create a runner, returning None if the binary is unavailable.

This is useful for tests that should skip gracefully when Lean isn’t built.

pub fn for_projection() -> Result<Self, LeanRunnerError>

Create a LeanRunner for projection export (uses the validator binary).

Errors

Returns LeanRunnerError::BinaryNotFound if the validator binary doesn’t exist.

pub fn is_available() -> bool

Check if the Lean binary is available at the default path.

pub fn require_available()

Require that the Lean binary is available.

This function is intended for CI environments where Lean tests should not be silently skipped. It panics with instructions if the binary is missing.

Panics

Panics if the Lean binary is not available.

pub fn validate( &self, choreography_json: &Value, program_json: &Value, ) -> Result<LeanValidationResult, LeanRunnerError>

Run validation with choreography and program JSON.

The choreography JSON should be a GlobalType JSON object.

The program JSON should have the format:

{
  "role": "A",
  "local_type": { "kind": "send", ... }
}

Errors

Returns an error if:

• Temporary files cannot be created
• JSON serialization fails
• The Lean process fails to execute
• Output parsing fails