Change the way SPO votes are counted #594

williamdemeo · 2024-10-11T21:59:42Z

Description

This closes issue #578.

Checklist

Commit sequence broadly makes sense and commits have useful messages
Any semantic changes to the specifications are documented in CHANGELOG.md
Code is formatted according to CONTRIBUTING.md
Self-reviewed the diff

This closes issue #578.

(It's unclear to me whether this is the intent of the WIP section of the CHANGELOG, or whether I should have left this issue in the 0.9 section.)

CHANGELOG.md

WhatisRT

Sorry, what actually needs to be done here is a bit more complicated. DState.voteDelegs needs to be available to actualSPOVotes. Then, if you have a credVoter SPO c, you need to lookup c in voteDelegs and the result of that lookup is the default vote.

williamdemeo · 2024-10-16T20:37:12Z

@WhatisRT @Lucsanszky I've revised the SPO default vote function. I think it's correct now, but let me know if you notice anything wrong with it. Thanks!

Lucsanszky · 2024-10-17T22:02:43Z

@WhatisRT @williamdemeo conformance is still failing for me. I had a better look at the ledger implementation (here's my PR which updates the SPO vote counting: IntersectMBO/cardano-ledger#4659) and the spec. To me it seems like that they indeed don't really match. In the implementation, we check if the SPO's reward address is delegated to an AlwaysAbstain or an AlwaysNoConfidence DRep. See: https://github.com/IntersectMBO/cardano-ledger/pull/4659/files#diff-d479e8ce99ea392464360b8cea0bb7c42e04863929fd3f4ae4c92dd5742e535cR222-R223
That is, on top of DState.voteDelegs, PState.pools needs to be available to actualSPOVotes as well, so we can first lookup the pool parameters of the given pool in pools, grab the reward address and look that up in voteDelegs. Unless:

My implementation is wrong.
I misunderstand something here as I'm not too familiar with Agda and the spec ~~and somehow the c in credVoter SPO c is the reward address of the given pool~~.

williamdemeo · 2024-10-18T02:29:00Z

@Lucsanszky Your description seems reasonable to me. I'll go ahead and try to change the Agda code to match your understanding of how the policy should be implemented. I'll let you know when the changes are done.

williamdemeo · 2024-10-18T04:22:36Z

@Lucsanszky I believe Ratify.lagda now agrees with the implementation as you describe it above. Thanks for the feedback. Let me know how the conformance tests go.

Lucsanszky · 2024-10-18T05:18:23Z

At a first glance, this looks good! Unfortunately, conformance is still failing but that could be because of something else (and I have an idea why). Anyways, I'll wait for @WhatisRT's approval. Thanks!

Lucsanszky · 2024-10-19T05:42:41Z

At a first glance, this looks good! Unfortunately, conformance is still failing but that could be because of something else (and I have an idea why). Anyways, I'll wait for @WhatisRT's approval. Thanks!

Okay, conformance passes. :) I opened a PR which also adds your changes to the conformance files, feel free to cherry pick the commits. Also, I took the liberty to slightly change your specification and opted not to pass in the complete CertState to RatifyEnv. I think it's better to be more specific with what we need and also helps with the conformance tests on the cardano-ledger side.

williamdemeo · 2024-10-21T15:21:39Z

Looks good. Thanks @Lucsanszky! I've merged your mods into this PR, so you can close your PR.

Andre's changes were addressed last week and he has been indisposed and busy with other things since then.

Lucsanszky

LGTM, thanks! 👍

This reverts commit 243cb32.

WhatisRT · 2024-10-25T12:44:52Z

src/Ledger/Conway/Conformance/Ratify.lagda

 \end{code}
 \begin{code}[hide]
-    λ where
+  getPoolParams : Credential → Maybe PoolParams
+  getPoolParams c = case lookupᵐ? stakeDelegs c of λ where  nothing → nothing


This lookup is incorrect, you just need to lookup c in pools (if it is a KeyHash).

That's good to know, thanks. If there is a particular place in a prior version of the spec or a CIP that would have helped me understand this better so that I wouldn't have made this mistake, please advise.

Not really. It's just that lookupᵐ? pools c is the PoolParams associated to c and contains c's RewardAddr, which is what you want. As the code is written here, it gives you the PoolParams of the pool that c is delegating to which could be any random pool.

I see. Thanks for the explanation. Very helpful. 👍🏼

WhatisRT · 2024-10-25T12:46:42Z

src/Ledger/Conway/Conformance/Ratify.lagda

+  SPODefaultVote _ _ = Vote.no
+
+  actualCCVote : Credential → Epoch → Vote
+  actualCCVote c e = case getCCHotCred (c , e) of λ where


Why did you un-hide the λ where? It just makes the PDF more confusing to people who don't know Agda.

For some reason, the only way I could get the TeX to compile without the "missing parameter l" error was to expose the λ where here and above. I tried many permutations of exposing and hiding various parts of the code, and the one I ended up with was the closest to what we want while still getting the pdf to compile without error.

It's probably just this bug again: agda/agda#7290

You probably just need to indent the clauses of the λ where a bit more.

Yes, it's exactly that bug. I tried indenting all sorts of ways, but I'll try again to get it to compile while hiding all the λ wheres and I'll also fix the bug in getPoolParams, of course.

WhatisRT · 2024-10-25T12:54:12Z

src/Ledger/Conway/Conformance/Ratify.lagda

+
+  SPODefaultVote : GovAction → VDeleg → Vote
+  SPODefaultVote (TriggerHF _) _ = Vote.no
+  SPODefaultVote NoConfidence (credVoter SPO c) = case getPoolParams c of λ where


Those λ wheres should be hidden as well

WhatisRT · 2024-10-25T13:00:07Z

Sorry, this is incorrect, and the implementation is probably too (if this is what makes conformance tests pass). Also, looking at this it would make much more sense to just use the credential of the stake pool itself instead of the reward account. Why should voting & setting the default for the vote require 2 different credentials?

lehins · 2024-10-25T21:32:20Z

looking at this it would make much more sense to just use the credential of the stake pool itself instead of the reward account.

It is too late to change implementation. cardano-node-10.x has already been released, which means at this point any discrepancies will have to be changed in the spec, instead of implementation.

Why should voting & setting the default for the vote require 2 different credentials?

Why would Stake Pool private key be used for both managing a pool and registering a stake credential?

Change the way SPO votes are counted

af8652a

This closes issue #578.

williamdemeo linked an issue Oct 11, 2024 that may be closed by this pull request

Change the way SPO votes are counted #578

Closed

moved issue in CHANGELOG from 0.9 section to WIP section

d484d42

(It's unclear to me whether this is the intent of the WIP section of the CHANGELOG, or whether I should have left this issue in the 0.9 section.)

williamdemeo marked this pull request as ready for review October 11, 2024 22:03

williamdemeo commented Oct 11, 2024

View reviewed changes

CHANGELOG.md Outdated Show resolved Hide resolved

williamdemeo requested a review from WhatisRT October 11, 2024 22:06

WhatisRT previously requested changes Oct 15, 2024

View reviewed changes

williamdemeo added 2 commits October 16, 2024 13:31

Merge branch 'master' into 578-change-to-spo-vote-counting

f576a2f

fix SPO vote count function

f02b856

williamdemeo requested a review from WhatisRT October 16, 2024 20:39

williamdemeo added 2 commits October 17, 2024 19:47

finally got TeX to compile with Conway pdf Fix 35 looking decent

1cfd800

Merge branch 'master' into 578-change-to-spo-vote-counting

5f68d68

change SPO votes calculation to agree with Haskell implementation

14872fb

Lucsanszky added 2 commits October 19, 2024 03:23

Stop passing in CertState to RatifyEnv

01ed236

Update SPO vote calculation conformance

a1a7188

williamdemeo self-assigned this Oct 21, 2024

Lucsanszky mentioned this pull request Oct 21, 2024

SPO votes conformance #596

Closed

4 tasks

williamdemeo requested review from Lucsanszky and removed request for WhatisRT October 24, 2024 13:41

Lucsanszky approved these changes Oct 24, 2024

View reviewed changes

williamdemeo merged commit 243cb32 into master Oct 24, 2024
15 checks passed

williamdemeo deleted the 578-change-to-spo-vote-counting branch October 24, 2024 17:28

github-actions bot added a commit that referenced this pull request Oct 24, 2024

Generate code for GH-594

c365539

WhatisRT added a commit that referenced this pull request Oct 25, 2024

Revert "Change the way SPO votes are counted (#594)"

4b90823

This reverts commit 243cb32.

WhatisRT mentioned this pull request Oct 25, 2024

Revert "Change the way SPO votes are counted" #599

Merged

WhatisRT added a commit that referenced this pull request Oct 25, 2024

Revert "Change the way SPO votes are counted (#594)"

e6e9aa4

This reverts commit 243cb32.

WhatisRT reviewed Oct 25, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Change the way SPO votes are counted #594

Change the way SPO votes are counted #594

williamdemeo commented Oct 11, 2024 •

edited

Loading

WhatisRT left a comment

williamdemeo commented Oct 16, 2024

Lucsanszky commented Oct 17, 2024 •

edited

Loading

williamdemeo commented Oct 18, 2024 •

edited

Loading

williamdemeo commented Oct 18, 2024

Lucsanszky commented Oct 18, 2024

Lucsanszky commented Oct 19, 2024

williamdemeo commented Oct 21, 2024

Lucsanszky left a comment

WhatisRT Oct 25, 2024 •

edited

Loading

williamdemeo Oct 25, 2024

WhatisRT Oct 25, 2024

williamdemeo Oct 25, 2024

WhatisRT Oct 25, 2024

williamdemeo Oct 25, 2024

WhatisRT Oct 25, 2024

williamdemeo Oct 25, 2024 •

edited

Loading

WhatisRT Oct 25, 2024

WhatisRT commented Oct 25, 2024 •

edited

Loading

lehins commented Oct 25, 2024

Change the way SPO votes are counted #594

Change the way SPO votes are counted #594

Conversation

williamdemeo commented Oct 11, 2024 • edited Loading

Description

Checklist

WhatisRT left a comment

Choose a reason for hiding this comment

williamdemeo commented Oct 16, 2024

Lucsanszky commented Oct 17, 2024 • edited Loading

williamdemeo commented Oct 18, 2024 • edited Loading

williamdemeo commented Oct 18, 2024

Lucsanszky commented Oct 18, 2024

Lucsanszky commented Oct 19, 2024

williamdemeo commented Oct 21, 2024

Lucsanszky left a comment

Choose a reason for hiding this comment

WhatisRT Oct 25, 2024 • edited Loading

Choose a reason for hiding this comment

williamdemeo Oct 25, 2024

Choose a reason for hiding this comment

WhatisRT Oct 25, 2024

Choose a reason for hiding this comment

williamdemeo Oct 25, 2024

Choose a reason for hiding this comment

WhatisRT Oct 25, 2024

Choose a reason for hiding this comment

williamdemeo Oct 25, 2024

Choose a reason for hiding this comment

WhatisRT Oct 25, 2024

Choose a reason for hiding this comment

williamdemeo Oct 25, 2024 • edited Loading

Choose a reason for hiding this comment

WhatisRT Oct 25, 2024

Choose a reason for hiding this comment

WhatisRT commented Oct 25, 2024 • edited Loading

lehins commented Oct 25, 2024

williamdemeo commented Oct 11, 2024 •

edited

Loading

Lucsanszky commented Oct 17, 2024 •

edited

Loading

williamdemeo commented Oct 18, 2024 •

edited

Loading

WhatisRT Oct 25, 2024 •

edited

Loading

williamdemeo Oct 25, 2024 •

edited

Loading

WhatisRT commented Oct 25, 2024 •

edited

Loading