-
Notifications
You must be signed in to change notification settings - Fork 23
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Praos headers validation properties and generators #1285
base: main
Are you sure you want to change the base?
Conversation
...sus-protocol/src/unstable-protocol-testlib/Test/Ouroboros/Consensus/Protocol/Praos/Header.hs
Show resolved
Hide resolved
...sus-protocol/src/unstable-protocol-testlib/Test/Ouroboros/Consensus/Protocol/Praos/Header.hs
Show resolved
Hide resolved
ouroboros-consensus-cardano/src/unstable-cardano-tools/Cardano/Tools/Headers.hs
Outdated
Show resolved
Hide resolved
coin = fromJust . toCompact . Coin | ||
slotCoeff = mkActiveSlotCoeff $ fromJust $ boundRational @PositiveUnitInterval $ 1 | ||
ownsAllStake vrfKey = IndividualPoolStake 1 (coin 1) vrfKey | ||
poolDistr = Map.fromList [(poolId, ownsAllStake hashVRFKey)] |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.
data ValidationResult = Valid Mutation | Invalid Mutation String | ||
deriving (Eq, Show) | ||
|
||
validate :: GeneratorContext -> MutatedHeader -> ValidationResult |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Esgen also mentioned that maybe the Agda spec would be amenable to reuse here?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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
.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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.1
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
-
(Of course, we could also structure the existing Haskell code in such a way that different STS sub-rules can be invoked independently. ↩
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
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 👍
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. |
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 |
We base64-encode all binary data
* replace hash with hashVerKeyVRF as the output does not seem to be the same
Haddocks are automatically available from LSP
2249b54
to
2f64542
Compare
Noticed while looking at IntersectMBO#1285
2f64542
to
fbfdb6e
Compare
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:
GeneratorContext
with various keys and parameters used in the forging of headers, and valid PraosHeader StandardCrypto
from such a contextHeader
one can apply aMutation
that invalidates one particular rule for headers validation, usingGen
erators tooHeader
andGeneratorContext
have JSON serialisers, with keys and bytes being output as base64-encoded stringsgen-header
program can be used to generate aSample
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 headersThe JSON output looks like the following:
TODO:
Mutation
type to cover all kind of potential validation errorsGeneratorContext
(eg. stake distribution, KES period...)generate
andvalidate
commands togen-header