Joosep Jääger

- [ ] Ledgers - [ ] Ledger - [ ] Utxow

# Description # Checklist - [ ] Commit sequence broadly makes sense and commits have useful messages - [ ] New tests are added if needed and existing tests are...

# Description This is supposed to make it easier to find a counterexample for IntersectMBO/formal-ledger-specifications#514 I managed to catch the bug with the modified generators by making it more likely...

# Description The implementation sorts proposals at the epoch boundary, but the spec sorts whenever a new proposal is added. This PR changes the `SpecTranslate` instance of `Proposals` so that...

IntersectMBO/formal-ledger-specifications#516 was merged recently and that has caused GOV conformance tests to fail. Investigate why that is happening and fix the problem.

Currently the constrained generators are pretty unlikely to generate a proposal that gets enacted. Right now all the votes are generated randomly and a large part of the votes are...

# Description This PR modifies the alternative spec so that the deposit update happens in the LEDGER rule instead of the UTXO rule like in the implementation. # Checklist -...

In the implementation we store the deposits inside the DRep/PoolParams data structure. To align the Haskell version of the spec better with the implementation we should get rid of the...

# Description # Checklist - [ ] Commit sequence broadly makes sense and commits have useful messages - [ ] Code is formatted according to [CONTRIBUTING.md](https://github.com/input-output-hk/formal-ledger-specifications/blob/master/CONTRIBUTING.md) - [ ] Self-reviewed...