Attribute Macro requires

#[requires]

Add a logical precondition to a function. In the case of a function that has one or more &mut inputs, in the ensures clause, you can refer to such an &mut input x as x for its “past” value and future(x) for its “future” value.

You can use the (unqualified) macro fstar! (BACKEND! for any backend BACKEND) to inline F* (or Coq, ProVerif, etc.) code in the precondition, e.g. fstar!("true").

Example

use hax_lib_macros::*;
#[requires(x.len() == y.len())]
pub fn div_pairwise(x: Vec<u64>, y: Vec<u64>) -> Vec<u64> {
    x.iter()
        .copied()
        .zip(y.iter().copied())
        .map(|(x, y)| x / y)
        .collect()
}