Praos headers validation properties and generators

[abailly]

Description

This PR introduces generators, properties, and an executable to be able to QuickCheck Praos headers validation in a somewhat exhaustive and explicit way. Here is a brief summary:

• Generators produce GeneratorContext with various keys and parameters used in the forging of headers, and valid Praos Header StandardCrypto from such a context
• From a valid Header one can apply a Mutation that invalidates one particular rule for headers validation, using Generators too
• Header and GeneratorContext have JSON serialisers, with keys and bytes being output as base64-encoded strings
• the gen-header program can be used to generate a Sample of headers and context to be stored as part of a regression test suite, and to provide reference test vectors for other projects interested in validating headers

The JSON output looks like the following:

{
  "context": {
    "coldSignKey": "WCDQ24vfOrWlhgg65ZbHHxtyBt+QAGBoUx+IhgP1jYdHMg==",
    "kesSignKey": "WQJgmgx5dL86RoXLVEB18TH...=",
    "nonce": "ggFYII+ejLTnuete4jqw0uaCyPDzh1xOLhiTO/RSqyZ3v/wt",
    "praosSlotsPerKESPeriod": 9496,
    "vrfSignKey": "WEBzzMvKExinGbhtUaOcCMvRUw77NVnEfq85OV+MSvEb5m+NMN2tyMLgmaZNOhuAifLI3K/FQVZkEU8Rmb7A6EAj"
  },
  "headers": [
    {
      "header": "gooaAK6SORoAud8OWCA+ah5Aq6Nyw4uKwFeVWEMJ4Dw1tcOrDFFciVxibi06a...=",
      "mutation": "NoMutation"
    },
    {
      "header": "gooaAEIEphoA2MMuWCDqcIOxbDmAD0BU8mv3D7DauIjLAGG/o301UMqD5...=",
      "mutation": "MutateColdKey"
    },

TODO:

• Don't restyle existing files (added by @nfrisby)
• Complete Mutation type to cover all kind of potential validation errors
• Include more components in the GeneratorContext (eg. stake distribution, KES period...)
• Add generate and validate commands to gen-header
• Add documentation
• Cover more Eras (?)

[nfrisby]

Perhaps helpful to note that the generator context doesn't necessarily need a full stake distribution: it only needs the relative stake of the vrf keys in the headers you expect that context to validate.

[nfrisby]

Do you have a sense yet of how difficult it would be to reuse the implementation's validation logic instead of re-specifying it here? Maybe we could do some rearranging upstream (eg factor out a "worker") to make it easier to invoke in this incomplete calling context.

Unless you were intending for this code to be independent?

[nfrisby]

Esgen also mentioned that maybe the Agda spec would be amenable to reuse here?

[nfrisby]

EG you're missing the chainChecks and the opcert checks. But I suppose that makes sense considering you're not so much interested in the actual incoming ledger/header state.

But maybe your generator could also generate a header state and the ledger view alongside each header? IE all three ingredients necessary to invoke Ouroboros.Consensus.HeaderValidation.validateHeader.

[abailly]

I agree the validate function in its current form is cumbersome, but ultimately it should just be a thin wrapper over calling the VRF and KES validation functions from Praos module. Creating the necessary environment to directly call validateHeader seemed like a more ambitious task at this stage, and something that could be done in a later PR to avoid "scope creep" as there really are 2 independent stages in the header validation.

re Agda spec: that's definitely something I think would be interesting to reuse as testing against an independent specification of the validation logic makes a lot of sense. This means the specification should be modular enough and separate the validation steps perhaps?

[amesgen]

re Agda spec: that's definitely something I think would be interesting to reuse as testing against an independent specification of the validation logic makes a lot of sense. This means the specification should be modular enough and separate the validation steps perhaps?

The spec is structured in STS style, with a DAG of rules, see e.g. Figure 6 in the Agda spec here. I guess that when exposing the spec as runnable Haskell functions (which I think shouldn't be that far off after #1270), this could be modular to e.g. have one function per STS sub-rule.¹

While being more granular that what is present in the current implementation, there is not directly something that corresponds exactly to VRF + KES validation. OCERT corresponds to KES validation, and PRTCL does VRF validation, but also a few more things like nonce evolution (not very complicated).

Footnotes

1. (Of course, we could also structure the existing Haskell code in such a way that different STS sub-rules can be invoked independently. ↩

[abailly]

Thanks for the links. Of course, modelling the tests after the specification's transitions or logic rules would be desirable. BTW, having a hyperlinked HTML rendering of the Agda spec would be much more convenient than a PDF. Or did I miss the link somehow?

[amesgen]

BTW, having a hyperlinked HTML rendering of the Agda spec would be much more convenient than a PDF. Or did I miss the link somehow?

Good point, we don't have that ATM, might to it later when I find the time 👍

[nfrisby]

• Cover more Eras (?)

So far, headers are very much specific to protocols more so than era. Byron (RealPBFT), Shelley (TPraos), and Babbage (proper Praos) were the only eras that altered the protocol.

[abailly]

Thanks a lot @nfrisby for taking the time to review this draft, it comforts me this can be useful and gives useful directions to improve it. The reason for this comment about eras is that the code pretty much pins down the block header's era to Conway which might or might not be desirable.