[Peras 2] Introduce PerasCertDB and related tests

[tbagrel1]

This pull request introduces the PerasCertDB datatype, used to hold and access all PerasCerts known by a node that could affect chain selection.

In the mid/near-term future, this will be enriched to persist certificates across restarts, and probably also to store historical certificates.

---

Peras types

• Added modules Ouroboros.Consensus.Storage.PerasCertDB{,.API,.Impl}, notably defining the typesPerasCertDB, PerasCertSnapshot (read-only snapshot of certs contained in the DB), and AddPerasCertResult; alongside their respectives methods

---

Tests

• Added modules Test.Ouroboros.Storage.PerasCertDB{,.StateMachine,.Model} for q-s-m testing of the PerasCertDB datatype. The corresponding tests have been included in the test suite defined by Test.Ouroboros.Storage

---

Regression

As the previous PR, all the components introduced by this PR are not used at the moment by the rest of the code, so no regression is expected.

[dnadales]

Why do we need ticket numbers for Peras certificates?

[amesgen]

We allocate PerasCertTicketNos in monotonically increasing fashion as new certificates arrive, just as we do for transactions in the mempool (we should add this in a Haddock comment). This way, anyone can subscribe to certificates as they arrive, by asking for more certificates after the last ticket number they know of, using getCertsAfter.

One thing to note here is that Peras round numbers almost could play the role of ticket numbers: Apart from edge cases, we will never receive a Peras certificate for round r after we received one for round s if r < s. However, because of these edge cases and a general concern for robustness, we are not using round numbers as "almost ticket numbers".

---

Lastly, we could also hide the ticket numbers by exposing a more monadic API (essentially a dequeue interface), where the PerasCertNo is maintained "internally". (This would be possible both here and in the Mempool API)

Status quo (simplified) in this PR:

getCertSnapshot :: STM m (PerasCertSnapshot blk)

data PerasCertSnapshot blk = PerasCertSnapshot
  { getCertsAfter :: PerasCertTicketNo -> [(ValidatedPerasCert blk, PerasCertTicketNo)]
  }

Here, the caller is responsible for maintaining the PerasCertTicketNo across calls to getCertsAfter/getCertSnapshot.

More monadic option without ticket numbers:

getCertFollower :: STM m (PerasCertFollower blk)

data PerasCertFollower blk = PerasCertFollower
  { getNextPerasCert :: STM m (ValidatedPerasCert blk)]
  }

Here, getNextPerasCert would internally maintain the PerasCertTicketNo in a TVar (or we could change the implementation to be based on a TChan 🤔 ).

Let us know if you find this appealing, we can explore that.

[dnadales]

However, because of these edge cases and a general concern for robustness, we are not using round numbers as "almost ticket numbers".

That makes sense. Should we document this properly (if it's not documented already). Thanks!

Let us know if you find this appealing, we can explore that.

I can't say I have a preference, but the current design seems simpler.

[amesgen]

Should we document this properly (if it's not documented already). Thanks!

I enriched the Haddocks of PerasCertTicketNo appropriately 👍

[dnadales]

Perhaps we should add some invariant checking here. For instance:

• Should the different maps have all the same size?
• For every certificate in pvcsCerts, is there a corresponding weight in pvcsWeightByPoint?
• Should the range of pvcsCerts and pvcsCertsByTicket be the same?
• etc.

[dnadales]

It might also be worth explaining why we're splitting the information of Peras certificates into multiple maps.

[bladyjoker]

I believe the answer to the last question is that these are particular indices that make call site queries execute optimally, otherwise we'd be scanning the entire pvcsCerts looking for a ticketNo.

[amesgen]

@bladyjoker is exactly right, we want to efficiently support different use cases using different representations, so that's why we have some redundancy.

In fact, we opened #1649 and submitted #1651 precisely to easily attach an invariant for this particular case, but somehow forgot to do this before opening this PR. Thanks for catching that!

[amesgen]

Done, see invariantForPerasVolatileCertState

[bladyjoker]

This was a lovely read! Looks good :)