Skip to content

[Peras 10] Add pure voting rules #1785

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
Draft
agustinmista wants to merge 4 commits into
base: peras/main-pr/new-defs-and-plumbing
Choose a base branch
from
Draft

[Peras 10] Add pure voting rules #1785

agustinmista wants to merge 4 commits into from
+1,297 −9

Conversation

@agustinmista
Copy link
Contributor

@agustinmista agustinmista commented Nov 28, 2025 •
edited
Loading

This PR makes two main contributions:

  • Adds a simple boolean predicate evaluator DSL that allows computing boolean predicates while returning evidence for the outcome. This is needed by the Peras voting rules to be able to trace why we did or did not enter/exit a cooldown period with good granularity. This DSL is accompanied by some unit tests.

  • Implements the Peras voting rules (from the CIP-0140) in a pure fashion, given a PerasVotingView which abstracts the impure bits away and can be mocked-up for testing. This is tested using randomly generated PerasVotingViews against a simpler model implemented directly over booleans that the real implementation must conform to. In the future, this model could be reified directly from the Agda spec.

@agustinmista agustinmista changed the base branch from main to peras/main-pr/new-defs-and-plumbing November 28, 2025 12:32
@agustinmista agustinmista force-pushed the peras/main-pr/new-defs-and-plumbing branch 6 times, most recently from 14229b9 to 85e4b39 Compare December 1, 2025 11:49
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from 3130a1d to b4fc7da Compare December 1, 2025 20:47
@agustinmista agustinmista force-pushed the peras/main-pr/new-defs-and-plumbing branch 5 times, most recently from 95a3906 to c0e0683 Compare December 3, 2025 13:10
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from b4fc7da to 48e9b96 Compare December 4, 2025 12:01
@agustinmista agustinmista self-assigned this Dec 4, 2025
@agustinmista agustinmista force-pushed the peras/main-pr/new-defs-and-plumbing branch from c0e0683 to 2957426 Compare December 4, 2025 14:50
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from 48e9b96 to 1319e8f Compare December 4, 2025 15:17
@agustinmista agustinmista force-pushed the peras/main-pr/new-defs-and-plumbing branch from 2957426 to d51b1a1 Compare December 8, 2025 12:51
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from 1319e8f to 6148c6e Compare December 9, 2025 09:08
@agustinmista agustinmista force-pushed the peras/main-pr/new-defs-and-plumbing branch 3 times, most recently from bb97f3f to 43c1fdc Compare December 16, 2025 10:44
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from 6148c6e to 66802e1 Compare December 16, 2025 11:19
@agustinmista agustinmista force-pushed the peras/main-pr/new-defs-and-plumbing branch from 43c1fdc to e7eadb3 Compare December 16, 2025 12:00
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from 66802e1 to 5143cd4 Compare December 16, 2025 12:12
@agustinmista @amesgen
@geo2a @tbagrel1 @nbacquey
Move geometric into Test.Util.QuickCheck
d9bf920 
This commit moves the `geometric` QuickCheck generator into a common
place so that we can reuse it in the upcoming tests for the Peras voting
rules.

Co-authored-by: Agustin Mista <[email protected]>
Co-authored-by: Alexander Esgen <[email protected]>
Co-authored-by: Georgy Lukyanov <[email protected]>
Co-authored-by: Thomas BAGREL <[email protected]>
Co-authored-by: Nicolas BACQUEY <[email protected]>
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from 5143cd4 to f26bd83 Compare December 16, 2025 12:37
tbagrel1
tbagrel1 reviewed Dec 16, 2025
View reviewed changes
Copy link
Contributor

@tbagrel1 tbagrel1 left a comment

Choose a reason for hiding this comment

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

I really like the general idea of making voting rules as clear as possible, with a clearly defined view interface!

But I feel like it's hard to get away from implementation details sometimes. Typically mkPerasVotingView is probably the most brittle part of this infrastructure (given its many preconditions), and I don't think we have a very satisfying way to aleviate this, except more documentation.

On a different note, I like the usability/user interface of the predicate DSL, I think it definitely suits this use-case. But I think we are in a weird middle with no type-level safety over evidence construction, so I'm not sure what the evidence feature brings for us in its current form. I may have missed something though.

ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Voting/Rules.hs Outdated
--
-- NOTE: '_K - 1' here is treating the 'Origin' certificate as being
-- from round -1.
Origin -> currRoundNo `rmod` _K :==: _K - 1
Copy link
Contributor

@tbagrel1 tbagrel1 Dec 16, 2025

Choose a reason for hiding this comment

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

Are we sure the "initial" certificate will be created outside of any regular round (i.e. round -1)?

ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Util/Pred.hs Outdated
Comment on lines 130 to 131
p@(Bool b) ->
boolean b p
Copy link
Contributor

@tbagrel1 tbagrel1 Dec 16, 2025

Choose a reason for hiding this comment

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

Suggested change
p@(Bool b) ->
boolean b p
p@(Bool True) -> Right p
p@(Bool False) -> Left p

nbacquey
nbacquey approved these changes Dec 16, 2025
View reviewed changes
ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/Voting/Rules.hs Outdated
-- A slightly safer version of 'roundStart' that works with certificates.
--
-- NOTE: Instead of using 'roundStart' directly, this makes it more
-- harder for the user of the voting interface to accidentally pass a
Copy link
Contributor

@nbacquey nbacquey Dec 16, 2025

Choose a reason for hiding this comment

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

typo: more harder

@agustinmista @amesgen
@geo2a @tbagrel1 @nbacquey
Add explainable boolean predicate evaluator
f3e707e 
This commits adds a simple boolean predicate evaluator DSL that allows
computing boolean predicates while returning evidence for the outcome.

This is needed by the Peras voting rules to be able to trace why we did
or did not enter/exit a cooldown period with good granularity.

Co-authored-by: Agustin Mista <[email protected]>
Co-authored-by: Alexander Esgen <[email protected]>
Co-authored-by: Georgy Lukyanov <[email protected]>
Co-authored-by: Thomas BAGREL <[email protected]>
Co-authored-by: Nicolas BACQUEY <[email protected]>
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from 5ff5ef2 to 941aba7 Compare December 17, 2025 16:26
agustinmista and others added 2 commits December 18, 2025 11:48
@agustinmista @amesgen
@geo2a @tbagrel1 @nbacquey
Add pure Peras Voting rules
ca21a1f 
This PR implements the Peras voting rules in a pure fashion. That is,
given a PerasVotingView (which needs to be constructed in an impure
context), they determine purely if a node is allowed to vote or not in a
given round w.r.t. the voting rules from the CIP-0140. See:

https://github.com/cardano-foundation/CIPs/blob/master/CIP-0140/README.md#rules-for-voting-in-a-round

(Note that this is orthogonal from the committee selection: both
conditions need to be satisfied before a node is able to cast a vote in
a give round.)

Notably, our implementation needs to cover the somewhat special case of
deciding whether to start voting at genesis. The problem arises due to
the lack of a latestCertSeen to enable the "voting path" of the rules.
While the CIP uses a specially-defined cert0, our implementation encodes
this case via nullable certificate behind a WithOrigin.

In addition, this PR implements conformance tests against a simpler model
implemented directly over Bools. In the future, this model could be
reified from the Agda spec. Notably, we need to remark that, because VR-1A
is evaluated first, then:

  * VR-1A => !VR-2A

So, this case can't be covered by the test suite in a consistent way.
To hopefully convince you of this, we can show that VR-1A~True and
VR-2A~True leads to a contradiction. Using the following definitions:

  * r: current round (>=0)
  * C: round of the latest certificate seen (>=0)
  * R: Peras ignorance rounds (>0)

We have:

  * VR-1A := r + 1 == C
  * VR-2A := C + R <= r

If we replace C from VR-1A into VR-2A, we get:

  * r + 1 + R <= r

Since R>0:

  * 1 + R > 1

Therefore, we have:

  * r + 1 + R > r + 1 > r

And we conclude that:

  * C + R > r

Thus, !VR-2A, which is a contradiction.

With this in mind, the currently selected generation sizes and frequencies
lead to the following coverage of our testing property:

ouroboros-consensus
  Peras
    Peras voting rules
      isPerasVotingAllowed: OK (0.45s)
        +++ OK, passed 100000 tests.

        Actual result (100000 in total):
        33.708% VoteReason(VR-2A and VR-2B)
        32.242% NoVoteReason(VR-1A or VR-2B)
        30.538% NoVoteReason(VR-1A or VR-2A)
         1.871% VoteReason(VR-1A and VR-1B)
         1.641% NoVoteReason(VR-1B or VR-2A)

        Should vote according to model (100000 in total):
        64.421% False
        35.579% True

        VR-(1A|1B|2A|2B) (100000 in total):
        19.213% (False,True,True,True)
        18.595% (False,True,True,False)
        14.495% (False,False,True,True)
        13.647% (False,False,True,False)
         7.992% (False,True,False,False)
         7.835% (False,False,False,False)
         7.365% (False,False,False,True)
         7.346% (False,True,False,True)
         1.017% (True,True,False,False)
         0.860% (True,False,False,False)
         0.854% (True,True,False,True)
         0.781% (True,False,False,True)

        VR-1A (100000 in total):
        96.488% False
         3.512% True

        VR-1B (100000 in total):
        55.017% True
        44.983% False

        VR-2A (100000 in total):
        65.950% True
        34.050% False

        VR-2B (100000 in total):
        50.054% True
        49.946% False

Co-authored-by: Agustin Mista <[email protected]>
Co-authored-by: Alexander Esgen <[email protected]>
Co-authored-by: Georgy Lukyanov <[email protected]>
Co-authored-by: Thomas BAGREL <[email protected]>
Co-authored-by: Nicolas BACQUEY <[email protected]>
@agustinmista @amesgen
@geo2a @tbagrel1 @nbacquey
Add changelog entry
4b08904 
Co-authored-by: Agustin Mista <[email protected]>
Co-authored-by: Alexander Esgen <[email protected]>
Co-authored-by: Georgy Lukyanov <[email protected]>
Co-authored-by: Thomas BAGREL <[email protected]>
Co-authored-by: Nicolas BACQUEY <[email protected]>
@agustinmista agustinmista force-pushed the peras/main-pr/pure-voting-rules branch from 941aba7 to 4b08904 Compare December 18, 2025 10:48
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@tbagrel1 tbagrel1 Awaiting requested review from tbagrel1

@nbacquey nbacquey Awaiting requested review from nbacquey

@nfrisby nfrisby Awaiting requested review from nfrisby nfrisby will be requested when the pull request is marked ready for review nfrisby is a code owner

@jasagredo jasagredo Awaiting requested review from jasagredo jasagredo will be requested when the pull request is marked ready for review jasagredo is a code owner

@fraser-iohk fraser-iohk Awaiting requested review from fraser-iohk fraser-iohk will be requested when the pull request is marked ready for review fraser-iohk is a code owner

@dnadales dnadales Awaiting requested review from dnadales dnadales will be requested when the pull request is marked ready for review dnadales is a code owner

@geo2a geo2a Awaiting requested review from geo2a geo2a will be requested when the pull request is marked ready for review geo2a is a code owner

@bladyjoker bladyjoker Awaiting requested review from bladyjoker bladyjoker will be requested when the pull request is marked ready for review bladyjoker is a code owner

Assignees

@agustinmista agustinmista

Labels

peras

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@agustinmista @tbagrel1 @nbacquey