Expand description
Hax-specific helpers for Rust programs. Those helpers are usually no-ops when compiled normally but meaningful when compiled under hax.
§Example:
use hax_lib::*;
fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
hax_lib::assume!(x.len() == y.len());
hax_lib::assert!(x.len() >= 0);
hax_lib::assert_prop!(forall(|i: usize| implies(i < x.len(), x[i] < 4242)));
hax_lib::debug_assert!(exists(|i: usize| implies(i < x.len(), x[i] > 123)));
x.into_iter().zip(y.into_iter()).map(|(x, y)| x + y).collect()
}Re-exports§
Modules§
- coq
- Procedular macros that have an effect only for the backend coq.
- fstar
- Procedular macros that have an effect only for the backend fstar.
- int
- prop
- proverif
- Procedular macros that have an effect only for the backend proverif.