Attribute Macro ensures_ref 

#[ensures_ref]

Same as ensures, but the closure takes the result by reference: the binder has type &T where T is the function’s return type.

Example

use hax_lib_macros::*;
#[ensures_ref(|result| result.len() == 2)]
pub fn pair(x: u64) -> Vec<u64> {
    vec![x, x]
}