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.