vstd_extra/
extern_const.rs

1///! This module provides a macro to define a constant that can be used when
2///! crossing crates.
3#[macro_export]
4macro_rules! extern_const {
5    ($(#[$doc:meta])* $_vis:vis $name:ident [ $name_spec:ident, $name_const:ident ] : $_ty:ty = $value:expr) => {
6        verus! {
7        #[doc = concat!("The constant `", stringify!($name), "`.")]
8        $(#[$doc])*
9        $_vis const $name_const: $_ty = $value;
10
11        #[doc = concat!("The specification of the constant `", stringify!($name), "`.")]
12        #[verifier::inline]
13        #[allow(non_snake_case)]
14        $_vis open spec fn $name_spec() -> $_ty { $name_const }
15
16        #[doc = concat!("The executable code of constant `", stringify!($name), "` when used cross-crate.")]
17        #[allow(non_snake_case)]
18        #[inline(always)]
19        #[verifier::when_used_as_spec($name_spec)]
20        $_vis const fn $name() -> (val: $_ty)
21            ensures val == $name_const
22        { $name_const }
23    }
24    };
25}
26
27pub use extern_const;
vstd_extra/extern_const.rs

vstd_extra/
extern_const.rs
