formal-ledger-specifications
formal-ledger-specifications copied to clipboard
Complete the implementation of stake pools and their scheduled retirement
Currently there is no scheduled retirement mechanism for pools implemented in Agda, in the way that it is in Haskell.
The incompleteness of the implementation is likely the reason we observe produce /= consumed errors from Agda, especially in tests that involve pool retirement and re-registration.