Attribute Macro ensures

#[ensures]

Add a logical postcondition to a function. Note you can use the forall and exists operators.

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

Example

use hax_lib_macros::*;
#[ensures(|result| result == x * 2)]
pub fn twice(x: u64) -> u64 {
    x + x
}