blvm_primitives/spec_types/mod.rs
1//! Specification-aware type wrappers for formal verification (spec-lock/Z3).
2//!
3//! Transparent wrappers around standard collections so types can be aligned with
4//! Orange Paper / spec-lock. Use `SpecVec` / `SpecHashMap` or the `spec_wrap!` macro.
5
6mod spec_hashmap;
7mod spec_vec;
8
9pub use spec_hashmap::SpecHashMap;
10pub use spec_vec::SpecVec;
11
12/// Macro for type aliases using spec wrappers (for spec alignment / formal verification).
13///
14/// # Example
15///
16/// ```ignore
17/// use blvm_primitives::spec_wrap;
18///
19/// spec_wrap!(ByteString = Vec<u8>);
20/// // pub type ByteString = SpecVec<u8>;
21/// ```
22#[macro_export]
23macro_rules! spec_wrap {
24 ($name:ident = Vec<$t:ty>) => {
25 pub type $name = $crate::SpecVec<$t>;
26 };
27 ($name:ident = HashMap<$k:ty, $v:ty>) => {
28 pub type $name = $crate::SpecHashMap<$k, $v>;
29 };
30}