[Peras 6] Improve generation of Peras events in ChainDB state machine tests

[agustinmista]

This PR introduces a sequence of changes to progressively improve the chances of observing possible-but-currently-uncommon Peras events in the ChainDB state machine tests. Concretely, we are interested in observing the chain selection algorithm switching from a longer to a shorter chain. For this, we rely on the following changes:

1. Tweaking the Cmd generation frequencies to produce more AddBlock and AddPerasCerts commands.
2. Enhancing the Cmd generator to "remember" previously generated blocks so that generated gaps can actually be filled sometimes (this previously relied entirely on randomness).
3. Generating a geometrically-distributed security parameter (k) on the fly, while first addressing Allow for k>2 in ChainDB state machine tests #1745. This includes a rationale for why we have chosen to sample k using a geometric distribution with p=0.5.

Please check the commit messages to find the empirical effect of these changes between commits. In short, we improve the chances of observing TagSwitchedToShorterChain from ~0.03% to about ~1.8%.

Closes #1745

[tbagrel1]

LGTM!

[nbacquey]

LGTM

[agustinmista]

NOTE: this hunk only contains formatting changes.

The formatter in my editor is very annoyed by this block not being properly formatted, so I need to remember to manually bypass format-on-save every time I touch this file.

I would appreciate if we can merge this hunk, but I can also revert it back if nobody agrees 🥲

[geo2a]

I've asked for some clarifications on how the new generator state is used.

Also, does this PR actually depend on #1679 or could it target main directly? I think we would prefer to merge directly to main to keep things independent.

[geo2a]

I do not understand where exactly these are used and what for. The only place I've found is in genBlk, where we check if the seen blocks are empty or not:

  savedGapBlocks = seenBlocks genState
  noSavedGapBlocks = Map.null savedGapBlocks

could you describe the use if this state in more detail? Preferably in its haddock in Model:

-- | Execution model
data Model blk m r = Model
  { dbModel :: DBModel blk
  , knownIters :: KnownIters blk m r
  , knownFollowers :: KnownFollowers blk m r
  , modelConfig :: Opaque (TopLevelConfig blk)
  , genState :: GenState blk
  -- ^ TODO: briefly describe how it's used
  }

[agustinmista]

The main idea here is to keep intermediate blocks generated by genBlk around, so that we no longer need to pray for them to be (re)generated from scratch in subsequent AddBlock and AddPerasCert invocations.

To illustrate, suppose the test has so far built the following chain:

A -> B -> C

Without this change, one of the options genBlk has is to generate a dangling block via genBlockAfterGap, by first building a random fork and then returning its tip. For instance, let's assume that genBlockAfterGap branches from B, and generates a block F, that fits on top of B via some (hypothetical) intermediate blocks D and E:

A -> B -> C
     |
     + -> (D) -> (E) -> F

From here, the state machine runs AddBlock F, leaving the gap between B and F to be potentially filled by other random invocations to AddBlock later on.

Now, the problem with this approach is that generating blocks compatible with D and E to fill the gap created by F completely at random is very unlikely. And since genBlk can only do it by adding new blocks on top of existing ones, it's very likely that any potential fork created this way will diverge and never reach F, rendering F rather useless IMO.

With this commit, whenever we genBlockAfterGap, we also save the hypothetical gap blocks (D and E) for later in the model state, so that genBlk can sample from this set later on (see the new genGapBlock subgenerator). This allows the hypothetical fork created by genBlockAfterGap to be recreated without having to redo all the original hard work leading to F.

Note that in the future we could also be more clever and store collections of gap blocks indexed by their tip (e.g. { F :-> {D, E} }) instead of individual ones:

seenBlocks :: 
  Map 
    (HeaderHash blk) -- tip of the fork
    ( Map 
      (HeaderHash blk) -- gap blocks
      blk
    )

(Using Map (HeaderHash blk) instead of Set just to satisfy Ord.) From there, we could first sample a fork, and then sample one of its gap blocks without replacement (i.e. removing the sampled value from the collection). This would avoid degrading the chances of filling gaps after a while by only remembering the gap blocks that haven't been sampled from yet.

---

Would adding something like this somewhere help justifying the changes?

[geo2a]

Ah, I see, genGapBlock was the missing piece for me to understand how the gap blocks were actually used. Thanks for the explanation @agustinmista! I think it would be great to have this comment incorporated into the test file.

[agustinmista]

Added a similar explanation (that doesn't focus on the before vs. after but rather on why we want this) in a6d4a00

[agustinmista]

Thanks for the review @geo2a, I left a comment trying to explain the rationale a bit better. As for:

Also, does this PR actually depend on #1679 or could it target main directly? I think we would prefer to merge directly to main to keep things independent.

This PR makes some trivial changes to ouroboros-consensus/test/consensus-test/Test/Consensus/MiniProtocol/ObjectDiffusion/PerasCert/Smoke.hs, which doesn't exist in main yet, so it kinda depends on #1679. However, we can rebase this one onto main and drop those changes. We just need to remember to reapply them to whichever of the two PRs ends up getting merged last.

Up to you 😸

[geo2a]

Thanks @agustinmista! If it's not too much work, please separate this PR into a standalone one targeting main.

[dnadales]

Looks good to me. I left some comments where I think the code would benefit from additional explanations.

[agustinmista]

Thanks @dnadales for the review! I added some extra documention to the code (derived mainly from the existing commit messages) in d521432.

Let me know if you're happy with these changes and I will squash them into their corresponding commits.

[agustinmista]

Rebased and reapplied the patch that depended on #1679.

This should be ready to go on our end at soon as it passes CI 🥳