Attribute Macro creusot_contracts::macros::trusted

#[trusted]

Instructs Creusot to ignore the body of a declaration, assuming any contract the declaration has is valid.

Example

#[trusted] // this is too hard to prove :(
#[ensures(result@ == 1)]
fn foo() -> i32 {
    // complicated code...
}

In practice you should strive to use this as little as possible.