[WIP] Add pure Peras voting rules #1723
Conversation
| , perasVotingRule1A | ||
| , perasVotingRule1B | ||
| , perasVotingRule2A | ||
| , perasVotingRule2B | ||
| , perasVotingRule1 | ||
| , perasVotingRule2 |
There was a problem hiding this comment.
It might be a good idea not to export these unless we want to test them individually.
| withPerasVotingView :: | ||
| PerasParams -> | ||
| Set (AnchoredFragment blk) -> | ||
| WithArrivalTime (ValidatedPerasCert blk) -> | ||
| WithArrivalTime (ValidatedPerasCert blk) -> | ||
| (SlotNo -> PerasRoundNo) -> | ||
| (SlotNo -> SlotNo) -> | ||
| (SlotNo -> Point blk) -> | ||
| (Point blk -> WithArrivalTime (ValidatedPerasCert blk) -> Set (AnchoredFragment blk) -> Bool) -> | ||
| (WithArrivalTime (ValidatedPerasCert blk) -> SlotNo) -> | ||
| (PerasVotingView blk -> STM m a) -> | ||
| STM m a |
There was a problem hiding this comment.
This is a sketch for now. The idea is to derive most of these inputs from the context (e.g. a ChainDB instance)
| perasVotingRule1A :: StandardHash blk => SlotNo -> PerasVotingView blk -> Bool | ||
| perasVotingRule1A s t = | ||
| and | ||
| [ pvvRound t s == getPerasCertRound (pvvLatestCertSeen t) <> coerce @Word64 1 | ||
| , pvvArrivalSlot t (pvvLatestCertSeen t) <= pvvRoundStart t s + _X | ||
| ] | ||
| where | ||
| _X = coerce (perasCertArrivalThreshold (pvvPerasParams t)) |
There was a problem hiding this comment.
With the extended definition from tweag/cardano-peras#99, this should be the only rule that doesn't follow verbatim the CIP-0140
agustinmista
force-pushed
the
peras/pure-voting-rules
branch
from
abde225 to
8f63b94
Compare
| -- necessary inpure machinery to retrieve their inputs. These rules are translated | ||
| -- as verbatim as possible from: | ||
| -- | ||
| -- https://github.com/cardano-foundation/CIPs/blob/master/CIP-0140/README.md#rules-for-voting-in-a-round |
There was a problem hiding this comment.
Probably makes sense to mention that VR-1A is a bit different because it now also takes the arrival time of the certificate into account.
EDIT: Ah, didn't see #1723 (comment) in time
| -- | If either VR-1A and VR-1B hold, or VR-2A and VR-2B hold, then voting is allowed. | ||
| isPerasVotingAllowed :: StandardHash blk => SlotNo -> PerasVotingView blk -> Bool | ||
| isPerasVotingAllowed s t = | ||
| or | ||
| [ perasVotingRule1 s t, | ||
| perasVotingRule2 (pvvRound t s) t | ||
| ] |
There was a problem hiding this comment.
I think we want a somewhat richer return type, eg Either NoVoteReason VoteReason. This can then be used for tracing to signal why we did (not) vote, eg
- We did not vote because the previous round didn't give rise to a quorum.
- We did not vote because the cert from the previous round arrived too late.
- We voted for the first time after a cooldown period.
(More abstract perspective: We essentially want to explain why a predicate succeeded/failed, so there is some overlap with general certificates for the truthiness of logical terms, as well as libraries like explainable-predicates, but we should probably use sth ad-hoc; maybe there is room for a mini-DSL here)
Later, we could set up conformance testing against the Agda implementation.
| data PerasVotingView blk = PerasVotingView | ||
| { pvvPerasParams :: | ||
| PerasParams | ||
| -- ^ Peras protocol parameters | ||
| , pvvAllChains :: | ||
| Set (AnchoredFragment blk) | ||
| -- ^ All known chains fragments | ||
| , pvvLatestCertSeen :: | ||
| WithArrivalTime (ValidatedPerasCert blk) | ||
| -- ^ The most recent certificate seen by the voter. | ||
| , pvvLatestCertOnChain :: | ||
| WithArrivalTime (ValidatedPerasCert blk) | ||
| -- ^ The most recent certificate present in some chain. | ||
| , pvvRound :: | ||
| SlotNo -> | ||
| PerasRoundNo | ||
| -- ^ Get the Peras round number corresponding to a slot. | ||
| , pvvRoundStart :: | ||
| SlotNo -> | ||
| SlotNo | ||
| -- ^ Get the slot number corresponding to the start of the Peras round for a slot. | ||
| , pvvBlockSelection :: | ||
| SlotNo -> | ||
| Point blk | ||
| -- ^ The most recent block on the preferred chain that is at least L slots old. | ||
| , pvvExtends :: | ||
| Point blk -> | ||
| WithArrivalTime (ValidatedPerasCert blk) -> | ||
| Set (AnchoredFragment blk) -> | ||
| Bool | ||
| -- ^ Does this block extend the one boosted by a certificate and is present in some chain? | ||
| , pvvArrivalSlot :: | ||
| WithArrivalTime (ValidatedPerasCert blk) -> | ||
| SlotNo | ||
| -- ^ Transform the arrival time of a certificate into its corresponding slot number | ||
| } |
There was a problem hiding this comment.
Some of these things are fallible in practice for boring reasons (PastHorizonException for time translations due to the HFC). We should think about this a bit; I think we can add appropriate preconditions (eg pvvRoundStart may only be invoked for slots older than the current slot) to keep things simple.
agustinmista
force-pushed
the
peras/pure-voting-rules
branch
from
5ceeebd to
3c642f5
Compare
agustinmista
force-pushed
the
peras/pure-voting-rules
branch
from
3c642f5 to
7b568d4
Compare
2 participants
Closes tweag/cardano-peras#116