Cardano Updates

Signed-off-by: wcatz <[email protected]>

Allows AccountState to pay to the correct reward account even though the
pool update won't take effect until after the refunds are paid and snapshot
taken.

Reverts previous commit - passing updates through immediately breaks
existing rewards which use previous registration

Fixes #493 - SPDD check now OK until epoch 220

Shd/accounts state validation outcomes

From https://github.com/IntersectMBO/cardano-api at bdc59418357acfb7bc52fc16d71126783b532952

Staking Page Refactor Part I

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

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

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

New Crowdin updates