[Peras 3] Make ChainDB aware of PerasCertDB, and switch to weighted chain selection

[tbagrel1]

Description

This PR introduces:

• Weighted chain comparisons: We compare chains based on their weight instead of their length. Non-trivial weight is given by Peras certificates as introduced in [Peras 1] Introduce basic types to support Peras #1673.
• Weighted chain selection: Select the weightiest chain instead of the longest chain.
• Weighted immutability criterion: Define the immutable tip in terms of weight instead of length.

Commits

The commits are intended to be reviewed individually:

• ChainDB: expose PerasCertDB functionality

  The ChainDB maintains a PerasCertDB internally, and exposes most of its functionality through its public API. This is analogous to how the LedgerDB is managed by the ChainDB.

• SecurityParam: mention weighted nature

  Purely a documentation update to mention the richer dynamics under Peras, plus a small helper function.

• O.C.Peras.Weight: add takeVolatileSuffix

  In Praos, the volatile suffix of a chain is defined to be the k most recent blocks. Analogously, in Peras, the volatile suffix of a chain is defined to be the longest suffix with weight at most k.

  This commits adds an appropriate function (via a binary search), as well as documentation and tests.

• ChainDB: define getCurrentChain in terms of weight

  This makes use of the previous commit in the ChainDB. Note that Minimize exposure to exact immutability criterion #1619 guarantees that the LedgerDB automatically uses the same notion of immutability.

  Note that this means that the immutable tip will be less than k blocks behind the tip when Peras is working well, ie every Peras round is giving rise to a certificate. Concretely, for plausible parameters, ie a round length of $U = 90$ slots and a Peras boost of $B = 15$, the length of the volatile suffix decreases from $k=2160$ to

  $$\frac{k}{1+\frac{B}{U\cdot f}} \approx 499$$

  on average.

• ChainDB.StateMachine: check immutable tip monotonicity

  To make sure that the more refined immutability criterion doesn't introduce any surprises, we add a postcondition to the ChainDB q-s-m test that the immutable tip never recedes.

• GSM: allow candidateOverSelection to be stateful and ChainSel: make rollbackExceedsSuffix weight-aware

  Preparatory refactorings for when the chain comparison will become weighted and hence additionally depend on the PerasWeightSnapshot.

• Peras.SelectView: initialize, expose WeightedSelectView

  This introduces the notion of a weighted SelectView, making use of Refactor: SelectView = BlockNo × TiebreakerView #1591

  ouroboros-consensus/ouroboros-consensus/src/ouroboros-consensus/Ouroboros/Consensus/Peras/SelectView.hs

  Lines 35 to 48 in 90131b2

  	-- | Information from a non-empty chain fragment for a weighted chain comparison
  	-- against other fragments with the same anchor.
  	data WeightedSelectView proto = WeightedSelectView
  	{ wsvLength :: !Word64
  	-- ^ The length of the fragment.
  	--
  	-- If we ignore EBBs, then it would be equivalent to use the tip 'BlockNo'
  	-- here. However, with EBBs, the 'BlockNo' can result in misleading
  	-- comparisons if only one fragment contains EBBs.
  	, wsvWeightBoost :: !PerasWeight
  	-- ^ The weight boost of a fragment (w.r.t. a particular anchor).
  	, wsvTiebreaker :: TiebreakerView proto
  	-- ^ Lazy because it is only needed when 'wsvTotalWeight' is inconclusive.
  	}

  This will used in place of the "normal" SelectView. Eventually, we could also remove the normal SelectView and replace it with WeightedSelectView. However, to keep this already big PR more focused, we propose to do this in the future.

• Introduce weighted chain comparisons

  The core change in this commit is in the O.C.Util.AnchoredFragment to the preferAnchoredCandidate and compareAnchoredFragments functions. These now

  • have a slightly strengthened precondition, namely that they intersect (as we otherwise can't meaningfully compare their weight), that we ensure is satisfied anywhere, and
  • take PerasWeightSnapshot as an additional argument.

  We keep the old implementation in case the PerasWeightSnapshot is empty; which is semantically unnecessary, but is a trivial way to make sure that no performance regression is introduced.

  The rest of the diff of this commit is simply due to adapting the respective call sites in a rather straightforward fashion.

• Integrate weighted BlockFetch decision logic

  This commit plugs the weighted chain comparison logic into the BlockFetch decision logic. This relies on a (merged, but not yet released, hence the s-r-p) Network change, see Support weighted chain comparisons ouroboros-network#5161 for a detailed description.

• ChainDB: implement chain selection for Peras certificates

  We allow new Peras certificates to be added to the ChainDB (and therefore to the managed PerasCertDB). If the certificate is boosting a block that is not on the current selection, we perform chain selection for it, potentially switching to a fork containing it if it now is weightier than our selection.

• MockChainSel: switch to weighted chain selection

  This logic is for example used in tests.

• ChainDB q-s-m: test weighted chain selection

  We enrich the model ChainDB implementation with weighted chain selection, and add a new command with a simple generator for adding certificates. We also enrich labelling with the TagSwitchedToShorterChain tag that shows that we sometimes do switch to a shorter chain; which would be a bug without Peras.

  A follow-up PR (Better certificate generation in ChainDB q-s-m test #1670) will further improve the generators of this test.

---

Regression

As of today, there is no way to generate certificates, so PerasCertDB is always empty, and the change to the chain selection algorithm is therefore invisible: in the absence of certificates, the Peras weight of a chain is equal to its length. Therefore, this PR does not introduce any semantic changes.

Furthermore, from a performance standpoint, care is taken to ensure that if there are no certificates, we use the unweighted Praos logic, meaning that there is no change in performance when Peras is disabled.

[dnadales]

I reviewed the following commits:

• ChainDB: expose PerasCertDB functionality
• SecurityParam: mention weighted nature
• O.C.Peras.Weight: add takeVolatileSuffix
• ChainDB: define getCurrentChain in terms of weight
• ChainDB.StateMachine: check immutable tip monotonicity
• GSM: allow candidateOverSelection to be stateful
• ChainSel: make rollbackExceedsSuffix weight-aware
• Peras.SelectView: initialize, expose WeightedSelectView

I'll try to continue tomorrow

[bladyjoker]

Reviewed:

[x] ChainDB: expose PerasCertDB functionalityy

LGTM

[bladyjoker]

Took the time to understand the takeVolatileSuffix functions and AnchoredFragment library. Left a few comments, curious what you think.

[bladyjoker]

Fyi this is noop for you folks, just wanted to share my thoughts on the overall code structure. I'm a complete beginner in this codebase so consider this as merely a conversation starter (after all, you are much better positioned to structure this code).

While attempting to comprehend the overall changes, I try to reason about what's common and what's different between Vanilla Praos and Peras Praos. Thinkering with how to generalize the code structure such that the differences can be a matter of supplying a different argument to a function (ie. dependency injection).

From what I can tell, Peras is all about summarizing or measuring the chain suffix differently, which means it needs weights to calculate it. It's also a 'special' deal that Peras with empty weights is simply Vanilla Praos, and we explicitly differentiate between them such that we gain some efficiency (eg. vanilla suffix length rule) in several places.

Currently, we've seen a couple of things in this PR:

1. Peras artifacts like weights and friends is threaded through multiple functions
2. Often we differentiate between Vanilla and Peras cases using "empty" weights to gain efficiency and dispatch accordingly
3. The Vanilla and Peras code bits are often together side by side.

My question to you is whether you see a pragmatic refactoring that would further isolate Peras bits into separate modules (like you already did in some places), while generalizing the common parts to accommodate for what now is Vanila and Peras.

Ideally, I would like to see:

1. Explicit dispatching

import qualified Peras
import qualified Vanila
doSmtn = 
   | isVanila = Vanila.doSmtn
   | isPeras = Peras.doSmtn

2. Generalized functions

doSmtnWith : (AnchoredFragment -> s) -> AnchoredFragment -> ... 
doSmtnWith summarizeSuffix frag = ...

which would push the decision on the concrete version to the caller, hopefully further elucidating convenient code structures and minimizing the spread of Peras specific artifacts to only the necessary parts (where the wiring happens).

[bladyjoker]

Somehow overloading the meaning of a SecurityParameter implicitly makes me feel a bit uncomfortable. We collate the measure of "meters" with that of "grams" so to speak.

k in Praos means "count", and k in Peras means "weight", and there's an explicit relationship between them.

Do you see a way to perhaps be more explicit about this? Separating into Praos and Peras sub modules etc.

[bladyjoker]

Consider using Praos.SelectView (is such thing exists) to explicitly denote the relationship between Paros and Peras select views.

[bladyjoker]

Just seen it used in takeVolatileSuffix. Upon reflection I'm thinking that perhaps maxRollbackWeight to be in Peras/SecurityParameter.hs and the Peras spin on the documentation attached to the SecurityParameter here move to the new module and attached to maxRollbackWeight

[bladyjoker]

In terms keeping Peras/Praos line explicit, wdyt about having

forall b1 b2.
  ( HasHeader b1
  , HasHeader b2
  ) =>
  (AnchoredFragment b1 -> s) ->
  AnchoredFragment b1 ->
  ChainDiff b2 ->
  Bool
rollbackExceedsSuffix summarize curChain (ChainDiff nbRollback suffix) =
  summarize suffixToRollBack > summarize suffix
 where
  suffixToRollBack = AF.anchorNewest nbRollback curChain

Just thinking how to move direct mentions of Peras closer to the call sites.

[bladyjoker]

Not sure how committed you are to isEmpty weights optimization you used in different places, seems like it could be used here too.

[amesgen]

The only "expensive" part of rollbackExceedsSuffix is totalWeightOfFragment, and that one is already using the isEmpty weights optimization, so I opted to not use it here.

[bladyjoker]

A couple of questions here:

1. Is there a version of this function that for both cases Vanilla/Peras uses the same body? Can the vanilla case be expressed using the AF.intersect as well? Not sure how the cases in vanilla body relates to the Peras cases.
2. I suspect there's an opportunity to generalize this function over the 'type of select view'.

preferAnchoredCandidate selectView cfg ours cand =
...
        preferCandidate
          (projectChainOrderConfig cfg)
          (selectView cfg (getHeader1 ourTip))
          (selectView cfg (getHeader1 theirTip))
...

[amesgen]

Is there a version of this function that for both cases Vanilla/Peras uses the same body? Can the vanilla case be expressed using the AF.intersect as well? Not sure how the cases in vanilla body relates to the Peras cases.

Yes, the long-term goal here is to just always use the Peras logic. We even did this at first while developing on a branch, but switched to this approach (where we transparently use the Praos logic when there are no certificates) to make it trivial to argue that our changes are not introducing any (performance) regressions.

I suspect there's an opportunity to generalize this function over the 'type of select view'.

Yes, though if sharing as much code as possible is the goal, then using the Peras logic would be the way to go.

[bladyjoker]

Consider placing these in the Peras subdirectory you have?

[bladyjoker]

Is there a concise common body based on AF.intersect that can be used in both cases? If so, we can perhaps shorten this and generalize it?

[amesgen]

Cf #1678 (comment)

[bladyjoker]

Similar story, perhaps this could be decomposed into a generalized forksAtMost and then further provide the Vanilla version along with Peras version?

[amesgen]

@bladyjoker Thanks a lot for your thoughtful comments!

My question to you is whether you see a pragmatic refactoring that would further isolate Peras bits into separate modules (like you already did in some places), while generalizing the common parts to accommodate for what now is Vanila and Peras.

A high-level remark here is that we currently only keep the previous Praos logic for explicitness and to avoid any possible (performance) regression when Peras is disabled. Looking ahead, the idea would be to remove the Praos/"Vanilla" logic and uniformly make use of the Peras logic, leveraging the property you mention that Peras degrades to Praos when there are no certificates.

I think separating the Peras logic into its own module hierarchy more explicitly is an interesting idea to explore; I will definitely keep this in mind for future PRs. Eg if we make further tweaks to just the Peras logic in the future, it seems nice that this is made explicit just by looking at which directories/files are being modified.

Relatedly: Other changes due to Peras, such as the new mini-protocols (see eg #1679) are put behind explicit an explicit PerasFlag feature flag (IntersectMBO/cardano-base#547), so there, the distinction is made very explicit.

---

Finally, one option in the very long term would be to make the abstract Consensus layer (ie the ouroboros-consensus layer) so abstract that it wouldn't be aware of Peras at all (which would be much more ambitious than what you are suggesting here); rather, the interface would be sufficiently general that you can implement Peras (or any other protocol that somehow adds weights to chains in some fashion) by instantiating some type classes appropriately. In some sense, this would be the logical endpoint of trying to push Peras to boundaries as much as possible.

I discussed this with the team in the past, and we concluded that this would be premature at this point; building an abstractions at this level of generality is very hard of course. It is easy to end up with an abstraction that is too general, such that one can hardly reason about how code using it will behave (similar to how unconstrained/lawless type classes can cause trouble).