# Masks are coPsets in the Coq development, not arbitrary subsets of natural numbers

The appendix suggests that masks for updates and weakest preconditions may be arbitrary sets (it does not say so explicitly when defining fancy updates, but on p. 29 the camera used for "enabled" invariants is said to be P(N)). However, in the Coq code, the representation used for masks is `coPset`

. @robbertkrebbers says that `coPsets`

are used so that the representation has extensional equality, but that in principle the constructions all could work with arbitrary sets.

It seems like either the discussion in the appendix should be changed to `coPset`

as well (in order to stick to the claim that everything is verified), or an explanatory note should be given. Unfortunately, it is not so easy to concisely describe `coPsets`

: they contain all finite and cofinite sets, and are closed under various set operations. However, as @jung points out, the namespace "suffix" construction is not so clearly derivable just from the closure properties.