formal-ledger-specifications
formal-ledger-specifications copied to clipboard
DRep expiration is "bumped" when there are no proposals even if the DRep has already expired
This behaviour shows up as a conformance testing failure as well, since the implementation only bumps the expiration epoch of DReps which are not expired.
This difference of behaviour is exhibited by the test:
LEDGER/Withdraw from a key delegated to a DRep that expired after delegation
Hmm, that's an interesting one. This behaviour isn't preserved by bisimulation, so I think we could also make the case that conformance shouldn't fail when two DReps are expired but have different epoch numbers associated with them.
It might also be interesting to prove this, and then test equality only up to that equivalence relation defined on our side. I feel like that shouldn't be that difficult.