hax_lib/
lib.rs

1//! Hax-specific helpers for Rust programs. Those helpers are usually
2//! no-ops when compiled normally but meaningful when compiled under
3//! hax.
4//!
5//! # Example:
6//!
7//! ```rust
8//! use hax_lib::*;
9//! fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
10//!   hax_lib::assume!(x.len() == y.len());
11//!   hax_lib::assert!(x.len() >= 0);
12//!   hax_lib::assert_prop!(forall(|i: usize| implies(i < x.len(), x[i] < 4242)));
13//!   hax_lib::debug_assert!(exists(|i: usize| implies(i < x.len(), x[i] > 123)));
14//!   x.into_iter().zip(y.into_iter()).map(|(x, y)| x + y).collect()
15//! }
16//! ```
17
18#![no_std]
19
20#[cfg(feature = "macros")]
21mod proc_macros;
22
23// hax engine relies on `hax-lib` names: to avoid cluttering names with
24// an additional `implementation` in all paths, we `include!` instead
25// of doing conditional `mod` and `pub use`.
26
27#[cfg(not(hax))]
28core::include!("dummy.rs");
29#[cfg(hax)]
30core::include!("implementation.rs");