Crate prusti_contracts

Macros

• body_invariant
  A macro for writing a loop body invariant.
• body_variant
  A macro to annotate body variant of a loop to prove termination
• closure
  A macro for defining a closure with a specification. Note: this is a declarative macro defined in this crate because declarative macros can’t be exported from the prusti-contracts-proc-macros proc-macro crate. See https://github.com/rust-lang/rust/issues/40090.
• ghost
  A macro for defining ghost blocks which will be left in for verification but omitted during compilation.
• predicate
  A macro for defining a predicate using prusti expression syntax instead of just Rust expressions.
• prusti_assert
  A macro for writing assertions using the full prusti specifications
• prusti_assert_eq
• prusti_assert_ne
• prusti_assume
  A macro for writing assumptions using prusti syntax
• prusti_refute
  A macro for writing refutations using prusti syntax

Structs

• Ghost
• Int
  a mathematical (unbounded) integer type it should not be constructed from running rust code, hence the private unit inside
• Map
  A map type
• Seq
  A sequence type

Functions

• before_expiry
  This function is used to evaluate an expression in the context just before the borrows expires.
• exists
  Existential quantifier.
• forall
  Universal quantifier.
• old
  This function is used to evaluate an expression in the “old” context, that is at the beginning of the method call.
• snap
  Creates an owned copy of a reference. This should only be used from within ghost code, as it circumvents the borrow checker.
• snapshot_equality
  Snapshot, “logical”, or “mathematical” equality. Compares the in-memory representation of two instances of the same type, even if there is no PartialEq nor Copy implementation. The in-memory representation is constructed recursively: references are followed, unsafe pointers and cells are not. Importantly, addresses are not taken into consideration.

Attribute Macros

• after_expiry
  A macro for writing a pledge on a function.
• assert_on_expiry
  A macro for writing a two-state pledge on a function.
• ensures
  A macro for writing a postcondition on a function.
• extern_spec
  A macro for specifying external functions.
• invariant
  A macro for type invariants.
• model
  Macro for creating type models.
• print_counterexample
  A macro to customize how a struct or enum should be printed in a counterexample
• pure
  A macro for marking a function as pure.
• refine_spec
  A macro to add trait bounds on a generic type parameter and specifications which are active only when these bounds are satisfied for a call.
• refine_trait_spec
  A macro for impl blocks that refine trait specifications.
• requires
  A macro for writing a precondition on a function.
• terminates
  A macro to annotate termination of a function
• trusted
  A macro for marking a function as trusted.
• verified
  A macro for marking a function as opted into verification.