IntersectMBO / IntersectMBO/formal-ledger-specifications
Property: `allEnactable` is an invariant of `CHAIN`
Open
blocked
era: conway
property
- Dominant language
- Agda
- Stars
- 52
- Forks
- 20
- Avg merge
- 6d 14h
- Merged PRs (30d)
- 7
Description
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 it. This means that this cannot be proven by a simple induction.
There are two sub-lemmas here:
- `allEnactable` is an invariant of `GOV`
- `allEnactable` is an invariant of `EPOCH` (this currently isn't true, need to filter things properly in `EPOCH`)
Contributor guide
Assessment
This issue has not been assessed yet.