Properties about the rewards map

[WhatisRT]

There are at least these interesting properties:

• At the epoch boundary, dom DState.rewards is constant
• dom DState.rewards = DepositPurpose.CredentialDeposit^{-1} (dom UTxOState.deposits) is an invariant

The first property is implied by the second, but it's probably necessary to prove the second property anyway. The first property is also potentially more interesting since we do some insertions into rewards at the epoch boundary. So it would make sense to prove that as soon as we have time.