Module move_model::pragmas

source ·
Expand description

Provides pragmas and properties of the specification language.

Constants

  • ABORTS_IF_IS_PARTIAL_PRAGMA
    Pragma indicating whether aborts_if specification should be considered partial.
  • ABORTS_IF_IS_STRICT_PRAGMA
    Pragma indicating whether no explicit aborts_if specification should be treated like aborts_if false.
  • ADDITION_OVERFLOW_UNCHECKED_PRAGMA
    Pragma indicating that adding u64 or u128 values should not be checked for overflow.
  • ALWAYS_ABORTS_TEST_PRAGMA
    Pragma indicating that the function will run smoke tests
  • ASSUME_NO_ABORT_FROM_HERE_PRAGMA
    Pragma indicating that aborts from this function shall be ignored.
  • CONDITION_ABORT_ASSERT_PROP
    Property which indicates that an aborts_if should be asserted. For callers of a function with such an aborts_if, the negation of the condition becomes an assertion.
  • CONDITION_ABORT_ASSUME_PROP
    Property which indicates that an aborts_if should be assumed. For callers of a function with such an aborts_if, the negation of the condition becomes an assumption.
  • CONDITION_ABSTRACT_PROP
    Abstract property which can be used together with an opaque specification. An abstract property is not verified against the implementation, but will be used for the function’s behavior in the application context. This allows to “override” the specification with a more abstract version. In general we would need to prove the abstraction is subsumed by the implementation, but this is currently not done.
  • CONDITION_CHECK_ABORT_CODES_PROP
    A property which can be attached to an aborts_with to indicate that it should act as check whether the function produces exactly the provided number of error codes.
  • CONDITION_CONCRETE_PROP
    Opposite to the abstract property.
  • CONDITION_DEACTIVATED_PROP
    A property which can be attached to any condition to exclude it from verification. The condition will still be type checked.
  • CONDITION_EXPORT_PROP
    Property which can be attached to conditions to make them exported into the VC context even if they are injected.
  • CONDITION_GLOBAL_PROP
    Property which can be attached to a module invariant to make it global.
  • CONDITION_INJECTED_PROP
    Internal property attached to conditions if they are injected via an apply or a module invariant.
  • CONDITION_ISOLATED_PROP
    Property which can be attached to a global invariant to mark it as not to be used as an assumption in other verification steps. This can be used for invariants which are nonoperational constraints on system behavior, i.e. the systems “works” whether the invariant holds or not. Invariant marked as such are not assumed when memory is accessed, but only in the pre-state of a memory update.
  • CONDITION_SUSPENDABLE_PROP
    A property that can be attached to a global invariant to indicate that it should be enabled disabled by the disable_invariant_in_body pragma
  • DELEGATE_INVARIANTS_TO_CALLER_PRAGMA
    Pragma indicating that invariants are not to be checked between entry and exit to this function
  • DISABLE_INVARIANTS_IN_BODY_PRAGMA
    Pragma indicating that invariants are not to be checked between entry and exit to this function
  • EMITS_IS_PARTIAL_PRAGMA
    Pragma indicating whether emits specification should be considered partial.
  • EMITS_IS_STRICT_PRAGMA
    Pragma indicating whether no emits specification should mean that no events are to be emitted.
  • EXPORT_ENSURES_PRAGMA
    Pragma which indicates that the function’s abort and ensure conditions shall be exported to the verification context even if the implementation of the function is inlined.
  • FRIEND_PRAGMA
    Pragma indicating that the function can only be called from certain caller. Unlike other pragmas, this pragma expects a function name like 0x1::M::f instead of a boolean or a number.
  • INTRINSIC_PRAGMA
    Pragma indicating whether implementation of function should be ignored and instead treated to be like a native function.
  • OPAQUE_PRAGMA
    Pragma indicating whether implementation of function should be ignored and instead interpreted by its pre and post conditions only.
  • REQUIRES_IF_ABORTS_PRAGMA
    Pragma indicating that requires are also enforced if the aborts condition is true.
  • SEED_PRAGMA
    Pragma defining a random seed.
  • TIMEOUT_PRAGMA
    Pragma defining a timeout.
  • VERIFY_DURATION_ESTIMATE_PRAGMA
    Pragma indicating an estimate how long verification takes. Verification is skipped if the timeout is smaller than this.
  • VERIFY_PRAGMA
    Pragma indicating whether verification should be performed for a function.

Functions