cvlr_spec/lib.rs
1//! Specification language for CVL (Certora Verification Language) in Rust.
2//!
3//! This module provides a framework for writing specifications with preconditions
4//! (requires) and postconditions (ensures) that can be used for formal verification.
5//!
6//! # Core Concepts
7//!
8//! ## Boolean Expressions
9//!
10//! The [`CvlrFormula`] trait represents boolean expressions that can be:
11//! - Evaluated to a boolean value
12//! - Asserted (checked for correctness)
13//! - Assumed (taken as preconditions)
14//!
15//! ## Composing Expressions
16//!
17//! Boolean expressions can be composed using:
18//! - [`cvlr_and`] - Logical AND
19//! - [`cvlr_impl`] - Logical implication (A → B)
20//! - [`cvlr_true`] - Constant true expression
21//!
22//! ## State Pairs
23//!
24//! Postconditions use [`eval_with_states`](CvlrFormula::eval_with_states) to evaluate
25//! over both pre-state and post-state contexts, allowing you to express postconditions
26//! that compare states before and after operations.
27//!
28//! ## Specifications
29//!
30//! The [`CvlrSpec`] trait represents a complete specification with:
31//! - Preconditions (requires) - conditions that must hold before an operation (assumed by the verifier)
32//! - Postconditions (ensures) - conditions that hold after an operation (asserted by the verifier)
33//!
34//! Use [`cvlr_spec`] to create a specification from requires and ensures clauses,
35//! or [`cvlr_invar_spec`] for specifications with invariants.
36//!
37//! ## Lemmas
38//!
39//! The [`CvlrLemma`](spec::CvlrLemma) trait represents a lemma: a logical statement where if the
40//! preconditions (requires) hold, then the postconditions (ensures) must also hold.
41//! Use [`cvlr_lemma!`] to define lemmas, or [`cvlr_predicate!`] to create anonymous
42//! predicates for use in lemmas.
43//!
44//! # Examples
45//!
46//! ```ignore
47//! use cvlr_spec::{cvlr_spec, cvlr_true};
48//!
49//! struct Counter {
50//! value: i32,
51//! }
52//!
53//! // Define a simple spec - cvlr_true uses eval_with_states for ensures
54//! let spec = cvlr_spec(cvlr_true::<Counter>(), cvlr_true::<Counter>());
55//! ```
56
57mod combinators;
58mod formula;
59mod macros;
60pub mod spec;
61
62#[doc(hidden)]
63pub mod __macro_support {
64 pub use cvlr_asserts::*;
65 pub use cvlr_macros::*;
66}
67
68// Re-export core types and traits
69pub use combinators::{cvlr_and, cvlr_implies, CvlrAnd, CvlrImplies};
70pub use formula::{cvlr_true, CvlrFormula, CvlrPredicate};
71pub use spec::{cvlr_invar_spec, cvlr_spec, CvlrInvarSpec, CvlrPropImpl, CvlrSpec};