Preconditions
The requires clause specifies conditions that must be true when a function is called. These are caller obligations: whoever calls the function must ensure the precondition holds.
Entry Guards
entry_requires is the runtime-facing counterpart to requires for public actor methods. It checks whether an external message is allowed to enter the verified method body.
Postconditions
The ensures clause specifies conditions that must be true when a function returns. These are function guarantees: the function promises to make the postcondition hold.
Result Keyword
The result keyword refers to the return value of a successful function return inside postconditions.
Multiple Contracts
You can write multiple requires and ensures clauses on the same function. All clauses of the same type are conjoined (AND-ed together).
Function Contracts
When a function is passed as a value (higher-order), the verifier cannot always see its body at the call site. Function type contracts provide a summary the verifier can rely on.
Contract Subtyping
Function values are only safe in verification when their behavior is summarized by contracts. This page explains how contract subtyping works and when contracts are required.