Module creusot_contracts::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

• 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