cvlr_spec/
formula.rs

1//! Boolean expression types and traits.
2
3use cvlr_asserts::{cvlr_assert, cvlr_assume};
4
5/// A Boolean expression that can be evaluated, assumed, or asserted.
6///
7/// This trait represents a boolean expression with an associated context type.
8/// Expressions implementing this trait can be:
9/// - Evaluated to a boolean value via [`eval`](CvlrFormula::eval) (single state)
10/// - Evaluated over two states via [`eval_with_states`](CvlrFormula::eval_with_states) (pre-state and post-state)
11/// - Asserted (checked) via [`assert`](CvlrFormula::assert) or [`assert_with_states`](CvlrFormula::assert_with_states)
12/// - Assumed (taken as a precondition) via [`assume`](CvlrFormula::assume) or [`assume_with_states`](CvlrFormula::assume_with_states)
13///
14/// # Associated Types
15///
16/// * [`Context`](CvlrFormula::Context) - The context type used to evaluate the expression. This typically
17///   represents the state or environment in which the expression is evaluated.
18///
19/// # Examples
20///
21/// ```
22/// use cvlr_spec::CvlrFormula;
23///
24/// struct MyContext {
25///     value: i32,
26/// }
27///
28/// struct IsPositive;
29///
30/// impl CvlrFormula for IsPositive {
31///     type Context = MyContext;
32///     fn eval(&self, ctx: &Self::Context) -> bool {
33///         ctx.value > 0
34///     }
35/// }
36/// ```
37pub trait CvlrFormula {
38    type Context;
39
40    /// Evaluates the expression in the given context.
41    ///
42    /// Returns `true` if the expression holds, `false` otherwise.
43    fn eval(&self, ctx: &Self::Context) -> bool;
44
45    /// Asserts that the expression holds in the given context.
46    ///
47    /// This will cause a verification failure if the expression evaluates to `false`.
48    /// The default implementation uses [`cvlr_assert!`] to check the result of [`eval`](CvlrFormula::eval).
49    fn assert(&self, ctx: &Self::Context) {
50        cvlr_assert!(self.eval(ctx));
51    }
52
53    /// Assumes that the expression holds in the given context.
54    ///
55    /// This adds the expression as a precondition that the verifier will assume to be true.
56    /// The default implementation uses [`cvlr_assume!`] to assume the result of [`eval`](CvlrFormula::eval).
57    fn assume(&self, ctx: &Self::Context) {
58        cvlr_assume!(self.eval(ctx));
59    }
60
61    /// Evaluates the expression over two states (pre-state and post-state).
62    ///
63    /// This method allows expressions to be evaluated in contexts that require
64    /// comparing values from two different states, such as checking invariants
65    /// across state transitions or comparing before and after values.
66    ///
67    /// # Parameters
68    ///
69    /// * `ctx0` - The pre-state context (before the transition)
70    /// * `ctx1` - The post-state context (after the transition)
71    ///
72    /// # Returns
73    ///
74    /// Returns `true` if the expression holds across both states, `false` otherwise.
75    ///
76    /// # Default Implementation
77    ///
78    /// The default implementation evaluates the expression using only the pre-state
79    /// context (`ctx0`). Expressions that need to compare both states should override
80    /// this method.
81    fn eval_with_states(&self, ctx0: &Self::Context, _: &Self::Context) -> bool {
82        self.eval(ctx0)
83    }
84
85    /// Asserts that the expression holds across two states (pre-state and post-state).
86    ///
87    /// This will cause a verification failure if the expression evaluates to `false`
88    /// when considering both the pre-state and post-state contexts.
89    ///
90    /// # Parameters
91    ///
92    /// * `ctx0` - The pre-state context (before the transition)
93    /// * `ctx1` - The post-state context (after the transition)
94    ///
95    /// # Default Implementation
96    ///
97    /// The default implementation asserts the expression using only the pre-state
98    /// context (`ctx0`). Expressions that need to compare both states should override
99    /// this method.
100    fn assert_with_states(&self, ctx0: &Self::Context, _: &Self::Context) {
101        self.assert(ctx0);
102    }
103
104    /// Assumes that the expression holds across two states (pre-state and post-state).
105    ///
106    /// This adds the expression as a precondition that the verifier will assume to be true
107    /// when considering both the pre-state and post-state contexts.
108    ///
109    /// # Parameters
110    ///
111    /// * `ctx0` - The pre-state context (before the transition)
112    /// * `ctx1` - The post-state context (after the transition)
113    ///
114    /// # Default Implementation
115    ///
116    /// The default implementation assumes the expression using only the pre-state
117    /// context (`ctx0`). Expressions that need to compare both states should override
118    /// this method.
119    fn assume_with_states(&self, ctx0: &Self::Context, _: &Self::Context) {
120        self.assume(ctx0);
121    }
122}
123
124pub trait CvlrPredicate: CvlrFormula {}
125
126/// A boolean expression that always evaluates to `true`.
127///
128/// This is a constant expression that can be used as a base case or placeholder
129/// in boolean expression compositions.
130#[derive(Copy, Clone)]
131pub struct CvlrTrue<Ctx>(core::marker::PhantomData<Ctx>);
132
133impl<Ctx> CvlrFormula for CvlrTrue<Ctx> {
134    type Context = Ctx;
135    fn eval(&self, _ctx: &Self::Context) -> bool {
136        true
137    }
138    fn assert(&self, _ctx: &Self::Context) {}
139    fn assume(&self, _ctx: &Self::Context) {}
140}
141
142pub fn cvlr_true<Ctx>() -> impl CvlrFormula<Context = Ctx> {
143    CvlrTrue(core::marker::PhantomData)
144}
cvlr_spec/formula.rs

cvlr_spec/
formula.rs
