Crate cvlr_spec 

Specification language for CVL (Certora Verification Language) in Rust.

This module provides a framework for writing specifications with preconditions (requires) and postconditions (ensures) that can be used for formal verification.

Core Concepts

Boolean Expressions

The CvlrFormula trait represents boolean expressions that can be:

• Evaluated to a boolean value
• Asserted (checked for correctness)
• Assumed (taken as preconditions)

Composing Expressions

Boolean expressions can be composed using:

• [cvlr_and] - Logical AND
• [cvlr_impl] - Logical implication (A → B)
• cvlr_true - Constant true expression

State Pairs

Postconditions use eval_with_states to evaluate over both pre-state and post-state contexts, allowing you to express postconditions that compare states before and after operations.

Specifications

The CvlrSpec trait represents a complete specification with:

• Preconditions (requires) - conditions that must hold before an operation (assumed by the verifier)
• Postconditions (ensures) - conditions that hold after an operation (asserted by the verifier)

Use [cvlr_spec] to create a specification from requires and ensures clauses, or [cvlr_invar_spec] for specifications with invariants.

Lemmas

The CvlrLemma trait represents a lemma: a logical statement where if the preconditions (requires) hold, then the postconditions (ensures) must also hold. Use cvlr_lemma! to define lemmas, or cvlr_predicate! to create anonymous predicates for use in lemmas.

Examples

use cvlr_spec::{cvlr_spec, cvlr_true};

struct Counter {
    value: i32,
}

// Define a simple spec - cvlr_true uses eval_with_states for ensures
let spec = cvlr_spec(cvlr_true::<Counter>(), cvlr_true::<Counter>());

Re-exports

pub use spec::cvlr_invar_spec;

pub use spec::cvlr_spec;

pub use spec::CvlrInvarSpec;

pub use spec::CvlrPropImpl;

pub use spec::CvlrSpec;

Modules

spec

Specification types and traits.

Macros

cvlr_and

Creates a boolean expression representing the logical AND of two or more expressions.

cvlr_def_predicate

Defines a predicate (boolean expression) over a context type.

cvlr_def_predicates

Defines multiple predicates in a single macro invocation.

cvlr_def_states_predicate

Defines a predicate that evaluates over two states.

cvlr_def_states_predicates

Defines multiple state predicates in a single macro invocation.

cvlr_implies

Creates a boolean expression representing logical implication (A → B).

cvlr_invar_spec

Creates an invariant specification from an assumption and an invariant.

cvlr_invariant_rules

Defines multiple rules for an invariant specification across multiple base functions.

cvlr_lemma

Defines a lemma with preconditions (requires) and postconditions (ensures).

cvlr_pif_and

Creates a boolean expression representing the logical AND of two or more predicate functions.

cvlr_predicate

Creates an anonymous predicate (boolean expression) over a context type.

cvlr_rules

Defines multiple rules for a specification across multiple base functions.

cvlr_spec

Creates a specification from preconditions (requires) and postconditions (ensures).

Structs

CvlrAnd

A boolean expression representing the logical AND of two expressions.

CvlrImplies

A boolean expression representing logical implication (A → B).

Traits

CvlrFormula

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

CvlrPredicate

Functions

cvlr_and

Combines two boolean expressions with logical AND.

cvlr_implies

Creates a boolean expression representing logical implication (A → B).

cvlr_true