add 'liveness' properties that can be expressed (currently a no-op)

These don't yet go on to generate any code, but the eventual plan is to check
these in the verifier.

Github: related #47 "properties, covers, etc"