Modifies Clause
The modifies clause declares which actor fields a function may change.
Reads Clause
The reads clause declares which actor fields a function observes without modifying.
Frame Conditions
Frame conditions guarantee that fields outside a function's modifies footprint are not written by that function. Callers can use the guarantee for fields they can mention through their own reads or modifies permissions.
Effect Inference
The verifier automatically computes which fields each function reads and writes by analyzing the call graph.