Change the way SPO votes are counted

[williamdemeo]

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

[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]

@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]

@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:

1. My implementation is wrong.
2. 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]

@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]

@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]

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]

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]

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