Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Property: allEnactable is an invariant of CHAIN #419

Open
WhatisRT opened this issue May 6, 2024 · 0 comments
Open

Property: allEnactable is an invariant of CHAIN #419

WhatisRT opened this issue May 6, 2024 · 0 comments
Labels
blocked era: conway property
Milestone
Aug - Oct

Comments

@WhatisRT
Copy link
Collaborator

WhatisRT commented May 6, 2024 •
edited
Loading

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)
@WhatisRT WhatisRT added this to the May - Jul milestone May 6, 2024
@WhatisRT WhatisRT changed the title Property: allEnactable is an invariant of GOV Property: allEnactable is an invariant of CHAIN May 6, 2024
@WhatisRT WhatisRT modified the milestones: May - Jul, Aug - Oct Jul 31, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
blocked era: conway property
Projects
None yet
Milestone
Aug - Oct
Development

No branches or pull requests
1 participant
@WhatisRT