formal-ledger-specifications
formal-ledger-specifications copied to clipboard
IntersectMBO
Formal specifications of the cardano ledger
`EPOCH` is very complicated, especially considering that we use a lot of `open` and record stuff. Some of the logic that is responsible for splitting up rewards into what we...
I like this notation, but the issue is that it can be accidentally mixed up with the regular function arrow. It would have been nice to force parentheses around the...
This issue contains various items that don't really fit anywhere else. I've divided this into smaller and bigger tasks. None of this is really urgent ATM, so we can do...
## Unavoidable (Do later) Things that we can either not avoid for technical reasons or because they would make things massively more difficult. These need to be explained. - [x]...
The implementation as of Conway forbids duplicate certificates in the same transaction. We don't have to add this restriction right away since the implementation is allowed to be more restrictive...
The `minUTxOValue` field was removed from `PParams` some eras ago, so it shouldn't be in Conway PParams.
- [ ] Rename `VDeleg` to `DRep` - [ ] Rename `credVoter` to `drepCredential` - [ ] Rename `abstainRep` to `drepAlwaysAbstain` - [ ] Rename `noConfidenceRep` to `drepAlwaysNoConfidence` - [...
As @Soupstraw pointed out, it's sometimes confusing to read something like `proj₁`, since it's not always clear if we're projecting out from something we think of as a pair, or...
We need to translate all ledger types to Haskell. The types for which we'll need `Convertible` instances are all those that appear in `Computational` instances. The root types of these...
This is a Conway feature that has been implemented but is still missing from the spec.