Map Operations
Model key-value facts like balances, owners, and configuration. Maps keep abstract state precise without adding deployed storage.
Set Operations
Track membership, uniqueness, and permission groups directly in specs. Sets make access and reachability properties easier to state.
Sequence Operations
Represent ordered histories, logs, and message traces. Sequences let proofs talk about position, prefixes, and append behavior.
Multiset Operations
Count resources without caring about order. Multisets are useful for inventories, votes, conservation rules, and bag-like state.
Collection Snapshots
Use collection snapshots to connect runtime enumerations to proof models without granting extra payload authority.