hax library

This crate contains helpers that can be used when writing Rust code that is proven through the hax toolchain.

⚠️ The code in this crate has no effect when compiled without --cfg hax. hax sets this cfg automatically when extracting a crate; a regular cargo build leaves it unset.

Main features

• #[hax_lib::requires(...)] and #[hax_lib::ensures(...)]: pre- and postconditions on functions.
• #[hax_lib::attributes]: enables requires/ensures on trait methods and refinements on struct fields.
• hax_lib::loop_invariant!: loop invariants.
• Prop and the logical operators forall, exists, implies: propositions beyond bool.
• assume!, assert!, assert_prop!: assumptions and assertions for the backends.
• fstar!, coq!, proverif!, ...: inline backend code.

Example

/// The addition in `sum` does not overflow.
fn no_overflow(x: &[u32], y: &[u32]) -> hax_lib::Prop {
    hax_lib::forall(|i: usize| {
        hax_lib::implies(
            i < x.len(),
            x[i] as u64 + y[i] as u64 <= u32::MAX as u64,
        )
    })
}

#[hax_lib::requires(hax_lib::Prop::from(x.len() == y.len()) & no_overflow(&x, &y))]
#[hax_lib::ensures(|result| result.len() == x.len())]
fn sum(x: Vec<u32>, y: Vec<u32>) -> Vec<u32> {
    hax_lib::assert!(x.len() == y.len());
    hax_lib::assert_prop!(no_overflow(&x, &y));
    x.into_iter().zip(y).map(|(x, y)| x + y).collect()
}