flux_rs/
lib.rs

1#![no_std]
2#[cfg_attr(flux, flux::no_suggestions)]
3pub mod bitvec;
4
5pub use attrs::*;
6pub use flux_attrs as attrs;
7
8#[no_suggestions]
9#[sig(fn(bool[true]) )]
10pub fn assert(_: bool) {}
11
12#[no_suggestions]
13#[sig (fn() -> _ requires false)]
14pub fn unreachable() -> ! {
15    unreachable!("impossible case")
16}
17
18/// Macro for creating detached specifications.
19///
20/// # Example
21/// ```
22/// flux_rs::macros::detached_spec! {
23///     fn inc(n:i32) -> i32[n+1];
24///     fn watermelon(n:usize) -> usize[n+2];
25/// }
26/// ```
27#[macro_export]
28#[doc(hidden)]
29macro_rules! __private_detached_spec {
30    ($($e:tt)*) => {
31        #[$crate::specs {
32            $($e)*
33        }]
34        const _: () = ();
35    };
36}
37
38/// Macro for creating `invariant qualifier`s
39/// # Example
40/// ```
41/// invariant!(res: int, i: int, n: int ; res + i == n);
42/// ```
43#[macro_export]
44#[doc(hidden)]
45macro_rules! __private_invariant {
46    ($($param:ident : $ty:ty),* ; $expr:expr) => {
47        $crate::defs! {
48            invariant qualifier Auto($($param: $ty),*) { $expr }
49        }
50        $crate::assert($expr);
51    };
52}
53
54/// Macro for creating `invariant qualifier`s without an assertion.
55///
56/// Unlike [`invariant`](crate::macros::invariant), the body is never re-emitted as Rust, so it
57/// may use refinement-only syntax. Sorts are inferred; annotate the ones that can't be, using
58/// the same `params ; body` syntax as [`invariant`](crate::macros::invariant).
59///
60/// # Example
61/// ```
62/// flux_rs::macros::qualifier!(my_plus(res, i) == n);
63/// flux_rs::macros::qualifier!(res: int, i: int ; res + i == n);
64/// ```
65#[macro_export]
66#[doc(hidden)]
67macro_rules! __private_qualifier {
68    ($($param:ident : $ty:ty),+ ; $($body:tt)*) => {
69        $crate::defs! {
70            invariant qualifier Auto($($param: $ty),+) { $($body)* }
71        }
72    };
73    ($($body:tt)*) => {
74        $crate::defs! {
75            invariant qualifier Auto() { $($body)* }
76        }
77    };
78}
79
80pub mod macros {
81    /// Macro for creating detached specifications.
82    ///
83    /// # Example
84    /// ```
85    /// flux_rs::macros::detached_spec! {
86    ///     fn inc(n:i32) -> i32[n+1];
87    ///     fn watermelon(n:usize) -> usize[n+2];
88    /// }
89    /// ```
90    pub use crate::__private_detached_spec as detached_spec;
91    /// Macro for creating `invariant qualifier`s
92    /// # Example
93    /// ```
94    /// flux_rs::macros::invariant!(res: int, i: int, n: int ; res + i == n);
95    /// ```
96    pub use crate::__private_invariant as invariant;
97    /// Macro for creating a local `invariant qualifier` hint.
98    /// # Example
99    /// ```
100    /// flux_rs::macros::qualifier!(my_plus(res, i) == n);
101    /// flux_rs::macros::qualifier!(res: int, i: int ; res + i == n);
102    /// ```
103    pub use crate::__private_qualifier as qualifier;
104}
flux_rs/lib.rs

flux_rs/
lib.rs
