Trait CvlrFormula 

pub trait CvlrFormula {
    type Context;

    // Required method
    fn eval(&self, ctx: &Self::Context) -> bool;

    // Provided methods
    fn assert(&self, ctx: &Self::Context) { ... }
    fn assume(&self, ctx: &Self::Context) { ... }
    fn eval_with_states(&self, ctx0: &Self::Context, _: &Self::Context) -> bool { ... }
    fn assert_with_states(&self, ctx0: &Self::Context, _: &Self::Context) { ... }
    fn assume_with_states(&self, ctx0: &Self::Context, _: &Self::Context) { ... }
}

A Boolean expression that can be evaluated, assumed, or asserted.

This trait represents a boolean expression with an associated context type. Expressions implementing this trait can be:

• Evaluated to a boolean value via eval (single state)
• Evaluated over two states via eval_with_states (pre-state and post-state)
• Asserted (checked) via assert or assert_with_states
• Assumed (taken as a precondition) via assume or assume_with_states

Associated Types

• Context - The context type used to evaluate the expression. This typically represents the state or environment in which the expression is evaluated.

Examples

use cvlr_spec::CvlrFormula;

struct MyContext {
    value: i32,
}

struct IsPositive;

impl CvlrFormula for IsPositive {
    type Context = MyContext;
    fn eval(&self, ctx: &Self::Context) -> bool {
        ctx.value > 0
    }
}

Required Associated Types

type Context

Required Methods

fn eval(&self, ctx: &Self::Context) -> bool

Evaluates the expression in the given context.

Returns true if the expression holds, false otherwise.

Provided Methods

fn assert(&self, ctx: &Self::Context)

Asserts that the expression holds in the given context.

This will cause a verification failure if the expression evaluates to false. The default implementation uses cvlr_assert! to check the result of eval.

fn assume(&self, ctx: &Self::Context)

Assumes that the expression holds in the given context.

This adds the expression as a precondition that the verifier will assume to be true. The default implementation uses cvlr_assume! to assume the result of eval.

fn eval_with_states(&self, ctx0: &Self::Context, _: &Self::Context) -> bool

Evaluates the expression over two states (pre-state and post-state).

This method allows expressions to be evaluated in contexts that require comparing values from two different states, such as checking invariants across state transitions or comparing before and after values.

Parameters

• ctx0 - The pre-state context (before the transition)
• ctx1 - The post-state context (after the transition)

Returns

Returns true if the expression holds across both states, false otherwise.

Default Implementation

The default implementation evaluates the expression using only the pre-state context (ctx0). Expressions that need to compare both states should override this method.

fn assert_with_states(&self, ctx0: &Self::Context, _: &Self::Context)

Asserts that the expression holds across two states (pre-state and post-state).

This will cause a verification failure if the expression evaluates to false when considering both the pre-state and post-state contexts.

Parameters

• ctx0 - The pre-state context (before the transition)
• ctx1 - The post-state context (after the transition)

Default Implementation

The default implementation asserts the expression using only the pre-state context (ctx0). Expressions that need to compare both states should override this method.

fn assume_with_states(&self, ctx0: &Self::Context, _: &Self::Context)

Assumes that the expression holds across two states (pre-state and post-state).

This adds the expression as a precondition that the verifier will assume to be true when considering both the pre-state and post-state contexts.

Parameters

• ctx0 - The pre-state context (before the transition)
• ctx1 - The post-state context (after the transition)

Default Implementation

The default implementation assumes the expression using only the pre-state context (ctx0). Expressions that need to compare both states should override this method.

Implementors

impl<A, B> CvlrFormula for CvlrAnd<A, B>

where A: CvlrFormula, B: CvlrFormula<Context = A::Context>,

type Context = <A as CvlrFormula>::Context

impl<A, B> CvlrFormula for CvlrImplies<A, B>

where A: CvlrFormula, B: CvlrFormula<Context = A::Context>,

type Context = <A as CvlrFormula>::Context