formal-ledger-specifications
formal-ledger-specifications copied to clipboard
IntersectMBO
Formal specifications of the cardano ledger
# Description This PR is to address issue #367. # Checklist - [x] Commit sequence broadly makes sense and commits have useful messages - [x] Code is formatted according to...
# Description There were smaller changes that I made while responding to the audit. # Checklist - [x] Commit sequence broadly makes sense and commits have useful messages - [x]...
# Description This adds the Conway spec to nix as the attribute `ledger.conway` and link it from the README. Also updates a bunch of deprecated CI actions. # Checklist -...
We are currently ratifying the governance actions in order in which they were submitted, but this is only the secondary order. First, we need to sort them by their type....
# 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...
# Description This PR adds a script that builds the executable script Haskell library and copies all the files to the `cardano-ledger-executable-spec` repo. This will partially automate the bumping the...
Here are some things that we should add: - [ ] mapPartial - [ ] inj₁, inj₂ - [ ] proj₁, proj₂ - [ ] isInj₁, isInj₂ - [ ]...
There are almost no explanations for anything in this Section.
This is a little difficult, since `allEnactable` depends on the list of governance actions twice: once for the enactability criterion and then all elements in the list need to satisfy...
This property is somewhat difficult to state, since the obvious thing isn't true: A voter (the pair of credential & role) can vote twice on the same thing, in a...