Struct Validator 

pub struct Validator { /* private fields */ }

Validator for cross-checking Rust and Lean results.

Implementations

impl Validator

pub fn new() -> Self

Create a new validator.

pub fn with_lean_path(self, path: impl Into<String>) -> Self

Set the path to the Lean executable.

pub fn validate_global_roundtrip(&self, g: &GlobalType) -> ValidationResult

Validate that a GlobalType round-trips through JSON correctly.

pub fn validate_local_roundtrip(&self, lt: &LocalTypeR) -> ValidationResult

Validate that a LocalTypeR round-trips through JSON correctly.

pub fn compare_projection( &self, rust_result: &LocalTypeR, lean_json: &Value, ) -> Result<ValidationResult, ValidateError>

Compare Rust projection result with Lean JSON output.

pub fn compare_subtyping( &self, rust_result: SubtypingDecision, lean_result: SubtypingDecision, ) -> ValidationResult

Compare Rust subtyping result with Lean result.

pub fn validate_projection_with_lean( &self, choreography_json: &Value, program_json: &Value, ) -> Result<ValidationResult, ValidateError>

Validate a program against a choreography using the Lean runner.

This invokes the actual Lean verification binary to check that the exported program matches the projected local type.

Arguments

• choreography_json - The choreography in Lean-compatible JSON format
• program_json - The program export in Lean-compatible JSON format

Errors

Returns an error if the Lean runner is unavailable or fails.

pub fn lean_available(&self) -> bool

Check if the Lean runner is available.

Returns true if the Lean binary exists at the expected path.

Trait Implementations

impl Default for Validator

fn default() -> Self

Returns the “default value” for a type.