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

Ratify governance actions in the correct order #516

Merged
merged 16 commits into from
Aug 21, 2024
Merged

Ratify governance actions in the correct order #516

merged 16 commits into from
Aug 21, 2024

Conversation

williamdemeo
Copy link
Contributor

Description

Will close #427.

Checklist

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

@williamdemeo williamdemeo linked an issue Jul 18, 2024 that may be closed by this pull request
Ratify governance actions in the correct order #427
Closed
@williamdemeo williamdemeo marked this pull request as ready for review July 18, 2024 19:22
@williamdemeo
Copy link
Contributor Author

@WhatisRT Will a GovState contain GovActions with different GovActionIDs? If so, should the ordering of elements in the GovState take into account GovActionIDs?

@williamdemeo williamdemeo marked this pull request as draft July 18, 2024 19:28
@williamdemeo
Copy link
Contributor Author

TODO: fix checks/invariants in Ledger.Ledger.Properties to account for inserting instead of appending new elements to GovState.

@WhatisRT
Copy link
Collaborator

The GovActionIDs are irrelevant for the order here.

@williamdemeo williamdemeo marked this pull request as ready for review July 25, 2024 20:47
WhatisRT
WhatisRT requested changes Jul 26, 2024
View reviewed changes
Copy link
Collaborator

@WhatisRT WhatisRT left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Overall I like it a lot, just a few cosmetic changes before we can merge it

src/Ledger/Gov.lagda Outdated
govActionPriority (TreasuryWdrl _) = 5
govActionPriority Info = 6

groupGovActions : GovState → GovState
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is unused

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, it's unused now, but wouldn't it be useful if/when we want to make sure all gov actions in a GovState are in the right order? Well, I'll just delete it for now. We can always add it back in later if needed.

src/Ledger/Gov.lagda
@@ -81,6 +82,40 @@ private variable
\end{code}
\emph{Functions used in the GOV rules}
\begin{AgdaMultiCode}
\begin{code}[hide]
govActionPriority : GovAction → ℕ
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This needs to be in the visible part of the PDF

src/Ledger/Gov.lagda
++ filter (λ x → govActionPriority (action (proj₂ x)) ≟ 5) gs
++ filter (λ x → govActionPriority (action (proj₂ x)) ≟ 6) gs

insertGovAction : GovState → GovActionID × GovActionState → GovState
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This also needs to be visible. Also, the with isn't that great there, since we'd have to explain it. But I think you should be able to do

if govActionPriority (action gaSt₀) ≤ govActionPriority (action gaSt₁) then ... else ...

and I expect that this probably doesn't break any proofs.

src/Ledger/Ledger/Properties.agda
@@ -134,6 +134,12 @@ module _ where

-- ** Proof that the set equality `govDepsMatch` (below) is a LEDGER invariant.

-- Mapping a list of `GovActionID × GovActionState`s to a list of
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It's very interesting to me that you're proving things about a more complicated relation now, but the proof has gotten a lot shorter.

Copy link
Contributor Author

@williamdemeo williamdemeo Jul 29, 2024 •
edited
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

New gov actions used to be appended to the end of the GovState. Now we insert according to the priority. So I don't think it's much more complicated, though all the lemmas about list concatenation became useless, so I deleted them. Also, this change gave me another chance to analyze, rework, and simplify the proof.

@WhatisRT WhatisRT changed the title 427 ratify governance actions in the correct order DO NOT MERGE: Ratify governance actions in the correct order Jul 26, 2024
@williamdemeo
Copy link
Contributor Author

I removed another unused lemma (insertGovAction-∈) and made the new definition of insertGovAction more compact, so now the insertGovAction and govActionPriority functions fit inside Fig 15.

@williamdemeo @WhatisRT
first draft of functions for ensuring gov actions in correct order
61c09a7
@williamdemeo @WhatisRT
improve functions for GovAction ordering and ordered insert
073d130
@williamdemeo @WhatisRT
minor cleanup
0277d1e
@williamdemeo @WhatisRT
addAction inserts at correct position (instead of appending action)
6dfd30f
@williamdemeo @WhatisRT
change function to order GovState instead of list of GovActions
9548bd6 
We'll probably never have to reorder a plain list of GovActions.

Question: Should the GovActionID be taken into account when reordering
the GovState?
@williamdemeo @WhatisRT
work on modified proof of ga deposits invariant for new prop order
9d06d35
@williamdemeo @WhatisRT
progress updating proof of ga deposits invariant
99a839b
@williamdemeo @WhatisRT
more progress
2a9d84e
@williamdemeo @WhatisRT
progress (nearly done)
2e0ac41
@williamdemeo @WhatisRT
progress
bb7e296
@williamdemeo @WhatisRT
revision of proof of ga deposits invariant complete
985bf18
@williamdemeo @WhatisRT
cleanup proof
96842d1
@williamdemeo @WhatisRT
final cleanup
0c6f306
@williamdemeo @WhatisRT
final final cleanup
d5af8ab
@williamdemeo @WhatisRT
address change requests
36561bb
@williamdemeo @WhatisRT
remove unused lemma
396e810
@WhatisRT WhatisRT force-pushed the 427-ratify-governance-actions-in-the-correct-order branch from 23155a5 to 396e810 Compare August 20, 2024 15:50
@WhatisRT WhatisRT merged commit bd6f17d into master Aug 21, 2024
2 of 3 checks passed
@WhatisRT WhatisRT deleted the 427-ratify-governance-actions-in-the-correct-order branch August 21, 2024 09:29
@Soupstraw Soupstraw mentioned this pull request Aug 28, 2024
Closed
@lehins lehins changed the title DO NOT MERGE: Ratify governance actions in the correct order Ratify governance actions in the correct order Aug 28, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@WhatisRT WhatisRT WhatisRT approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Ratify governance actions in the correct order
2 participants
@williamdemeo @WhatisRT