Provides an environment -- global state -- for translation, including helper functions to interpret metadata about the translation target.
Information about a verification condition stored in the environment.
Identifier for a field of a structure, relative to struct.
Identifier for a Move function, relative to module.
A global id. Instances of this type represent unique identifiers relative to
Represents a module environment.
Identifier for a module.
Named Constant Environment
Identifier for a named constant, relative to module.
Identifier for a node in the AST, relative to a module. This is used to associate attributes with the node, like source location and type.
Represents a parameter.
Identifier for a schema.
Identifier for a specification function, relative to module.
Identifier for a specification variable, relative to module.
Identifier for a structure/resource, relative to module.
A tag used to be associated with a condition info. Condition infos are identified in the environment by a pair of Loc and this type.
Pragma indicating whether aborts_if specification should be considered partial.
Pragma indicating whether no explicit aborts_if specification should be treated
Pragma indicating that adding u64 or u128 values should not be checked for overflow.
Pragma indicating that the function will run smoke tests
Pragma indicating that aborts from this function shall be ignored.
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.
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.
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 prover the abstraction is subsumed by the implementation, but this is currently not done.
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.
Opposite to the abstract property.
A property which can be attached to any condition to exclude it from verification. The condition will still be type checked.
Property which can be attached to conditions to make them exported into the VC context even if they are injected.
Property which can be attached to a module invariant to make it global.
Internal property attached to conditions if they are injected via an apply or a module invariant.
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.
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.
Pragma indicating whether implementation of function should be ignored and instead treated to be like a native function.
Pragma indicating whether implementation of function should be ignored and instead interpreted by its pre and post conditions only.
Pragma indicating that requires are also enforced if the aborts condition is true.
Names used in the bytecode/AST to represent the main function of a script
Pragma defining a random seed.
Pragma defining a timeout.
Pragma indicating an estimate how long verification takes. Verification is skipped if the timeout is smaller than this.
Pragma indicating whether verification should be performed for a function.
Checks whether a pragma is valid in a specific spec block.
A function which determines whether a property is valid for a given condition kind.
Alias for the Loc variant of MoveIR. This uses a