Trait Z3Provable 

pub trait Z3Provable {
    // Required methods
    fn proof_description(&self) -> &'static str;
    fn prove_equation(&self) -> Result<ProofResult, ProofError>;

    // Provided method
    fn theorems(&self) -> Vec<&'static str> { ... }
}

MANDATORY trait for all EDD simulations.

Every simulation MUST implement this trait to prove its governing equations using the Z3 SMT solver. This is enforced at compile time and as a quality gate (EDD-11, EDD-12).

Quality Gate Requirements

• EDD-11: Z3 equation proof passes (cargo test --features z3-proofs)
• EDD-12: Z3Provable trait implemented (compile-time enforcement)

Required Methods

fn proof_description(&self) -> &'static str

Get a human-readable description of what this proof demonstrates.

Example

fn proof_description(&self) -> &'static str {
    "2-Opt Improvement: Δ > 0 ⟹ shorter tour"
}

fn prove_equation(&self) -> Result<ProofResult, ProofError>

Prove the governing equation using Z3.

This method encodes the equation as Z3 assertions and attempts to prove it. Returns Ok(ProofResult) if the equation is provable, Err(ProofError) otherwise.

Errors

• ProofError::Unprovable - The equation has a counterexample
• ProofError::Timeout - Z3 timed out
• ProofError::Z3Error - Internal Z3 error

Provided Methods

fn theorems(&self) -> Vec<&'static str>

Get all theorems that this simulation proves.

Default implementation returns a single theorem from proof_description().

Implementors