Mutable Record Types
Records with var fields are mutable records. They use reference semantics, so the verifier tracks access with permissions and generated ownership predicates.
Ownership Predicates
Ownership predicates are the verification mechanism that tracks permissions for mutable records. They bundle field permissions into a single token that the verifier manages automatically at call boundaries and field accesses.
Aliasing Restrictions
Mutable records use reference semantics, so multiple variables can point to the same object. This page explains what aliasing patterns are supported, how the verifier handles aliased parameters, and what patterns are rejected.