Module macros

Specification are written using these macros

All of those are re-exported at the top of the crate.

Macros

extern_spec

Allows specifications to be attached to functions coming from external crates

ghost

Opens a ‘ghost block’.

pearlite

Enables pearlite syntax, granting access to Pearlite specific operators and syntax

proof_assert

Inserts a logical assertion into the code

snapshot

Create a new Snapshot object.

Attribute Macros

bitwise_proof

This attribute indicates that the function need to be proved in “bitwise” mode, which means that Creusot will use the bitvector theory of SMT solvers.

ensures

A post-condition of a function or trait item

invariant

A loop invariant

law

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

logic

Declare a function as being a logical function

maintains

Allows specifying both a pre- and post-condition in a single statement.

open

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

open_inv_result

This attribute can be used on a function or closure to instruct Creusot not to ensure as a postcondition that the return value of the function satisfies its type invariant.

predicate

Declare a function as being a predicate

pure

Indicate that the function is pure: fulfilling the requires clauses ensures that this function will terminate, and will not panic.

requires

A pre-condition of a function or trait item

terminates

Indicate that the function terminates: fulfilling the requires clauses ensures that this function will not loop forever.

trusted

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

variant

Declares a variant for a function