IntersectMBO / formal-ledger-specifications

Formal specifications of the cardano ledger

Apache License 2.0

38 stars 13 forks source link

Remove unenactable governance actions in EPOCH #549

Closed javierdiaz72 closed 2 months ago

javierdiaz72 commented 3 months ago

Description

This addresses issue #429.

Checklist

[x] Commit sequence broadly makes sense and commits have useful messages
[x] Code is formatted according to CONTRIBUTING.md
[x] Self-reviewed the diff

javierdiaz72 commented 3 months ago

NOTE: When merging masterinto this PR's branch some recently added properties broke. Therefore, @WhatisRT and I agreed on me dedicating some fixed time to try to fix the proof and, if failed, @WhatisRT taking over this fix. So, I have commented out the broken properties for the time being.

javierdiaz72 commented 3 months ago

@WhatisRT : Your fix for the proof looks great, thanks for helping! 🙂