Attribute Macro logic 

#[logic]

Declare a function as being a logical function

This declaration must be pure and total. It cannot be called from Rust programs, but in exchange it can use logical operations and syntax with the help of the pearlite! macro.

open

Allows the body of a logical definition to be made visible to provers

By default, bodies are opaque: they are only visible to definitions in the same module (like pub(self) for visibility). An optional visibility modifier can be provided to restrict the context in which the body is opened.

A body can only be visible in contexts where all the symbols used in the body are also visible. This means you cannot open a body which refers to a pub(crate) symbol.

Example

mod inner {
    use creusot_contracts::prelude::*;
    #[logic]
    #[ensures(result == x + 1)]
    pub(super) fn foo(x: Int) -> Int {
        // ...
    }

    #[logic(open)]
    pub(super) fn bar(x: Int) -> Int {
        x + 1
    }
}

// The body of `foo` is not visible here, only the `ensures`.
// But the whole body of `bar` is visible

prophetic

If you wish to use the ^ operator on mutable borrows to get the final value, you need to specify that the function is prophetic, like so:

#[logic(prophetic)]
fn uses_prophecies(x: &mut Int) -> Int {
    pearlite! { if ^x == 0 { 0 } else { 1 } }
}

Such a logic function cannot be used in snapshot! anymore, and cannot be called from a regular logic function.

law

Declares a trait item as being a law which is autoloaded as soon another trait item is used in a function.

trait CommutativeOp {
    fn op(self, other: Self) -> Int;

    #[logic(law)]
    #[ensures(forall<x: Self, y: Self> x.op(y) == y.op(x))]
    fn commutative();
}