-
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
Draft
abailly
wants to merge
12
commits into
IntersectMBO:main
Choose a base branch
from
abailly:abailly/generate-headers
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Draft
Changes from all commits
Commits
Show all changes
12 commits
Select commit
Hold shift + click to select a range
2f6c80c
Add module to generate headers
abailly-iohk 75b34f1
Make header validation test compile (and fail)
abailly-iohk d981d0f
Can validate KES signature part of a valid header
abailly-iohk 30c5d5d
Can Validate VRF proof for a pool owning 100% of the stake
abailly-iohk d688a83
Introduce very basic faulty headers test
abailly-iohk ef259db
Separate context generation from header generation
abailly-iohk 7c0bafb
Scaffold executable to generate headers
abailly-iohk c1b39dd
Ensure test vectors can be serialised to/from JSON
abailly-iohk bb572e3
Restructure code to separate IOs from "pure" generators
abailly-iohk 6c1d2af
Mutate KES signature with different key than expected
abailly-iohk 71a3ee6
Better classification of test samples
abailly-iohk f62df8f
Mutate header signing cert with a different cold key
abailly-iohk File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
89 changes: 89 additions & 0 deletions
89
ouroboros-consensus-cardano/src/unstable-cardano-tools/Cardano/Tools/Headers.hs
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. Choose a reason for hiding this commentThe 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. |
||
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
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 fromPraos
module. Creating the necessary environment to directly callvalidateHeader
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.
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 👍