Attribute Macro creusot_contracts::macros::open

#[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::*;
    #[logic]
    #[open(self)]
    #[ensures(result == x + 1)]
    pub(super) fn foo(x: Int) -> Int {
        // ...
    }
}

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