Attribute Macro ensures 

#[ensures]

A post-condition of a function or trait item

The post-condition can refer to the result of the function using the special variable result.

The inside of a ensures may look like Rust code, but it is in fact pearlite.

See also the guide: requires and ensures.

Example

#[ensures(result@ == 1)]
fn foo() -> i32 { 1 }