vstd/
calc_macro.rs

Help
1//! The [`calc`] macro provides support for reasoning about a structured proof calculation.
2#![allow(unused_imports)]
3use super::pervasive::*;
4use super::prelude::*;
5
6verus! {
7
8/// The `calc!` macro supports structured proofs through calculations.
9///
10/// In particular, one can show `a_1 R a_n` for some transitive relation `R` by performing a series
11/// of steps `a_1 R a_2`, `a_2 R a_3`, ... `a_{n-1} R a_n`. The calc macro provides both convenient
12/// syntax sugar to perform such a proof conveniently, without repeating oneself too often, or
13/// exposing the internal steps to the outside context.
14///
15/// The expected usage looks like:
16///
17/// ```
18/// calc! {
19///   (R)
20///   a_1; { /* proof that a_1 R a_2 */ }
21///   a_2; { /* proof that a_2 R a_3 */ }
22///    ...
23///   a_n;
24/// }
25/// ```
26///
27/// Currently, the `calc!` macro supports common transitive relations for `R`, and this set of
28/// relations may be extended in the future.
29///
30/// Note that `calc!` also supports stating intermediate relations, as long as they are consistent
31/// with the main relation `R`. If consistency cannot be immediately shown, Verus will give a
32/// helpful message about this. Intermediate relations can be specified by placing them right before
33/// the proof block of that step.
34///
35/// A simple example of using intermediate relations looks like:
36///
37/// ```
38/// let x: int = 2;
39/// let y: int = 5;
40/// calc! {
41///   (<=)
42///   x; (==) {}
43///   5 - 3; (<) {}
44///   5; {} // Notice that no intermediate relation is specified here, so `calc!` will consider the top-level relation `R`; here `<=`.
45///   y;
46/// }
47/// ```
48#[allow(unused_macros)]
49#[macro_export]
50macro_rules! calc {
51    ($($tt:tt)*) => {
52        ::builtin_macros::calc_proc_macro!($($tt)*)
53    };
54}
55
56pub use calc;
57
58} // verus!
vstd/calc_macro.rs

vstd/
calc_macro.rs
