Struct VerificationSession 

pub struct VerificationSession { /* private fields */ }

A verification session for working with the Verification IR.

A session accumulates variable declarations and assumptions, then verifies assertions against that context. This is the recommended API for most verification tasks.

Each verification call creates a fresh Z3 context to avoid lifetime issues.

Examples

use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};

let mut session = VerificationSession::new();

// Declare variables
session.declare("x", VerifyType::Int);

// Add assumptions
session.assume(&VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(0)));

// Verify assertions
let result = session.verify(&VerifyExpr::gte(VerifyExpr::var("x"), VerifyExpr::int(0)));
assert!(result.is_ok());

Modus Ponens Example

use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};

let mut session = VerificationSession::new();
session.declare("x", VerifyType::Object);

// All mortals are human
session.assume(&VerifyExpr::implies(
    VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]),
    VerifyExpr::apply("Human", vec![VerifyExpr::var("x")]),
));

// x is mortal
session.assume(&VerifyExpr::apply("Mortal", vec![VerifyExpr::var("x")]));

// Therefore x is human
assert!(session.verify(&VerifyExpr::apply("Human", vec![VerifyExpr::var("x")])).is_ok());

Implementations

impl VerificationSession

pub fn new() -> Self

Create a new verification session.

Examples

use logicaffeine_verify::VerificationSession;

let session = VerificationSession::new();

pub fn declare(&mut self, name: &str, ty: VerifyType)

Declare a variable with a type.

Variables must be declared before they can be used in assumptions or verifications.

Examples

use logicaffeine_verify::{VerificationSession, VerifyType};

let mut session = VerificationSession::new();
session.declare("x", VerifyType::Int);
session.declare("p", VerifyType::Bool);
session.declare("socrates", VerifyType::Object);

pub fn assume(&mut self, expr: &VerifyExpr)

Add an assumption (constraint) to the session.

Assumptions constrain the verification context. Subsequent calls to verify will check validity under all assumptions.

Examples

use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};

let mut session = VerificationSession::new();
session.declare("x", VerifyType::Int);

// Assume x = 10
session.assume(&VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(10)));

// Assume x > 0
session.assume(&VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(0)));

pub fn verify_with_binding( &self, var_name: &str, var_type: VerifyType, value: &VerifyExpr, predicate: &VerifyExpr, ) -> VerificationResult

Verify a predicate with a temporary variable binding.

Used for refinement type checking. Creates a scoped context where var_name = value is assumed, then verifies that predicate holds.

Examples

use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};

let session = VerificationSession::new();

// Check that 10 satisfies the predicate x > 5
let result = session.verify_with_binding(
    "x",
    VerifyType::Int,
    &VerifyExpr::int(10),
    &VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5)),
);
assert!(result.is_ok());

pub fn verify(&self, expr: &VerifyExpr) -> VerificationResult

Verify that an assertion is valid given current assumptions.

Uses the standard validity check: P is valid iff ¬P is unsatisfiable. Returns Ok(()) if the assertion can be proven, an error otherwise.

Examples

use logicaffeine_verify::{VerificationSession, VerifyExpr, VerifyType};

let mut session = VerificationSession::new();
session.declare("x", VerifyType::Int);
session.assume(&VerifyExpr::eq(VerifyExpr::var("x"), VerifyExpr::int(10)));

// This should pass: 10 > 5
assert!(session.verify(&VerifyExpr::gt(VerifyExpr::var("x"), VerifyExpr::int(5))).is_ok());

// This should fail: 10 < 5
assert!(session.verify(&VerifyExpr::lt(VerifyExpr::var("x"), VerifyExpr::int(5))).is_err());

pub fn check_sat(&self) -> Result<bool, VerificationError>

Check the joint satisfiability of all assumptions (no goal).

Returns Ok(true) when Z3 finds a model, Ok(false) when the assumptions are jointly unsatisfiable, and Err on solver-unknown — three-valued, so an unknown never reads as either verdict.

pub fn verify_temporal( &self, initial: &VerifyExpr, transition: &VerifyExpr, property: &VerifyExpr, bound: u32, ) -> VerificationResult

Verify a temporal property via bounded model checking.

Unrolls the transition relation bound steps and checks if the property holds at every unrolled state.

• initial: constraint on the initial state (e.g., s == 0)
• transition: constraint relating current state to next state
• property: the property to verify at each state
• bound: number of unrolling steps

Returns Ok(()) if the property holds at all unrolled states, or an error with counterexample if a violation is found.

Trait Implementations

impl Default for VerificationSession

fn default() -> Self

Returns the “default value” for a type.