You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
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.
The text was updated successfully, but these errors were encountered:
There are at least these interesting properties:
dom DState.rewards
is constantdom DState.rewards = DepositPurpose.CredentialDeposit^{-1} (dom UTxOState.deposits)
is an invariantThe 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.The text was updated successfully, but these errors were encountered: