Distinguish rules by kind

We have different kinds of rules. Some are to do with the operation of the system (state transitions), others express properties/invariants. We could distinguish these (eg using colors). We should then also have high level consistency rules (is the system well formed, do transitions within an epoch terminate, are the rules confluent, etc), as well as the rules governing resource properties (rewards calculation, timing constraints etc). The latter will be extracted to provide your verifiable resource analysis (and can be embedded as a calculus within the executable spec).