Praos headers validation properties and generators #1285
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,23 @@ | ||
| module GenHeader.Parsers where | ||
|
|
||
| import Cardano.Tools.Headers (Options (..)) | ||
| import Data.Version (showVersion) | ||
| import Options.Applicative (Parser, ParserInfo, execParser, helper, info, progDesc, (<**>)) | ||
| import Paths_ouroboros_consensus_cardano (version) | ||
|
|
||
| parseOptions :: IO Options | ||
| parseOptions = execParser argsParser | ||
|
|
||
| argsParser :: ParserInfo Options | ||
| argsParser = | ||
| info | ||
| (optionsParser <**> helper) | ||
| ( progDesc $ | ||
| unlines | ||
| [ "gen-header - A utility to generate valid and invalid Praos headers for testing purpose" | ||
| , "version: " <> showVersion version | ||
| ] | ||
| ) | ||
|
|
||
| optionsParser :: Parser Options | ||
| optionsParser = pure Options |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| -- | This tool generates valid and invalid Cardano headers. | ||
| module Main (main) where | ||
|
|
||
| import Cardano.Crypto.Init (cryptoInit) | ||
| import Cardano.Tools.Headers (run) | ||
| import GenHeader.Parsers (parseOptions) | ||
| import Main.Utf8 (withUtf8) | ||
|
|
||
| main :: IO () | ||
| main = withUtf8 $ do | ||
| cryptoInit | ||
| parseOptions >>= run |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,89 @@ | ||
| {-# LANGUAGE NamedFieldPuns #-} | ||
| {-# LANGUAGE OverloadedStrings #-} | ||
| {-# LANGUAGE PatternSynonyms #-} | ||
| {-# LANGUAGE TypeApplications #-} | ||
|
|
||
| -- | Tooling to generate and validate (Praos) headers. | ||
| module Cardano.Tools.Headers where | ||
|
|
||
| import Cardano.Crypto.DSIGN (deriveVerKeyDSIGN) | ||
| import Cardano.Crypto.VRF (VRFAlgorithm (deriveVerKeyVRF, hashVerKeyVRF)) | ||
| import Cardano.Ledger.Api (ConwayEra, StandardCrypto) | ||
| import Cardano.Ledger.BaseTypes (BoundedRational (boundRational), PositiveUnitInterval, mkActiveSlotCoeff) | ||
| import Cardano.Ledger.Coin (Coin (..)) | ||
| import Cardano.Ledger.Compactible (toCompact) | ||
| import Cardano.Ledger.Keys (VKey (..), hashKey) | ||
| import Cardano.Ledger.PoolDistr (IndividualPoolStake (..)) | ||
| import Cardano.Protocol.TPraos.OCert (ocertN) | ||
| import Control.Monad.Except (runExcept) | ||
| import qualified Data.Aeson as Json | ||
| import qualified Data.ByteString.Lazy as LBS | ||
| import Data.Char (isSpace) | ||
| import qualified Data.Map as Map | ||
| import Data.Maybe (fromJust) | ||
| import qualified Data.Text as Text | ||
| import Ouroboros.Consensus.Block (validateView) | ||
| import Ouroboros.Consensus.Protocol.Praos ( | ||
| Praos, | ||
| doValidateKESSignature, | ||
| doValidateVRFSignature, | ||
| ) | ||
| import Ouroboros.Consensus.Protocol.Praos.Header (Header, hbOCert, pattern Header) | ||
| import Ouroboros.Consensus.Shelley.HFEras () | ||
| import Ouroboros.Consensus.Shelley.Ledger ( | ||
| ShelleyBlock, | ||
| mkShelleyHeader, | ||
| ) | ||
|
|
||
| import Ouroboros.Consensus.Shelley.Protocol.Praos () | ||
| import Test.Ouroboros.Consensus.Protocol.Praos.Header ( | ||
| GeneratorContext (..), | ||
| MutatedHeader (..), | ||
| Mutation (..), | ||
| Sample (..), | ||
| expectedError, | ||
| generateSamples, | ||
| header, | ||
| mutation, | ||
| ) | ||
|
|
||
| type ConwayBlock = ShelleyBlock (Praos StandardCrypto) (ConwayEra StandardCrypto) | ||
|
|
||
| -- * Running Generator | ||
| data Options = Options | ||
|
|
||
| run :: Options -> IO () | ||
| run Options = do | ||
| sample <- generateSamples | ||
| LBS.putStr $ Json.encode sample <> "\n" | ||
|
|
||
| data ValidationResult = Valid Mutation | Invalid Mutation String | ||
| deriving (Eq, Show) | ||
|
|
||
| validate :: GeneratorContext -> MutatedHeader -> ValidationResult | ||
| validate context MutatedHeader{header, mutation} = | ||
| case (runExcept $ validateKES >> validateVRF, mutation) of | ||
| (Left err, mut) | ctor err == expectedError mut -> Valid mut | ||
abailly marked this conversation as resolved.
Show resolved
Hide resolved
|
||
| (Left err, mut) -> Invalid mut (show err) | ||
| (Right _, NoMutation) -> Valid NoMutation | ||
| (Right _, mut) -> Invalid mut $ "Expected error from mutation " <> show mut <> ", but validation succeeded" | ||
| where | ||
| GeneratorContext{praosSlotsPerKESPeriod, nonce, coldSignKey, vrfSignKey} = context | ||
| -- TODO: get these from the context | ||
| maxKESEvo = 63 | ||
| 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. 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. |
||
| poolId = hashKey $ VKey $ deriveVerKeyDSIGN coldSignKey | ||
| hashVRFKey = hashVerKeyVRF $ deriveVerKeyVRF vrfSignKey | ||
| Header body _ = header | ||
| certCounter = ocertN . hbOCert $ body | ||
| ocertCounters = Map.fromList [(poolId, certCounter)] | ||
|
|
||
| headerView = validateView @ConwayBlock undefined (mkShelleyHeader header) | ||
| validateKES = doValidateKESSignature maxKESEvo praosSlotsPerKESPeriod poolDistr ocertCounters headerView | ||
| validateVRF = doValidateVRFSignature nonce poolDistr slotCoeff headerView | ||
|
|
||
| ctor :: (Show e) => e -> String | ||
| ctor err = Text.unpack $ head $ concatMap (Text.split isSpace) $ Text.split (== '(') $ Text.pack $ show err | ||
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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
chainChecksand 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
validatefunction in its current form is cumbersome, but ultimately it should just be a thin wrapper over calling the VRF and KES validation functions fromPraosmodule. Creating the necessary environment to directly callvalidateHeaderseemed 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.
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.
Good point, we don't have that ATM, might to it later when I find the time 👍