-
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
25
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
25 commits
Select commit
Hold shift + click to select a range
006d94b
Add module to generate headers
abailly-iohk 71437d3
Make header validation test compile (and fail)
abailly-iohk f44e7f5
Can validate KES signature part of a valid header
abailly-iohk aaf3233
Can Validate VRF proof for a pool owning 100% of the stake
abailly-iohk 9e9b6f0
Introduce very basic faulty headers test
abailly-iohk 0527f6d
Separate context generation from header generation
abailly-iohk fa97fdd
Scaffold executable to generate headers
abailly-iohk 93b16f1
Ensure test vectors can be serialised to/from JSON
abailly-iohk 3cf5afd
Restructure code to separate IOs from "pure" generators
abailly-iohk 80904b8
Mutate KES signature with different key than expected
abailly-iohk 112a983
Better classification of test samples
abailly-iohk 77c4d76
Mutate header signing cert with a different cold key
abailly-iohk c1f9253
Provide simple 'generate' and 'validate' commands
abailly-iohk 499be18
Mutate KES period of certificate to be after current period
abailly-iohk c92d8b6
Mutate KES period of certificate to be too old (before current)
abailly-iohk 210c1ac
Remove dead code
abailly-iohk 167ec92
Can mutate both context and header
abailly-iohk aa8bc4d
Add operational certificate counters in generator context
abailly-iohk 21f90ab
Mutate context's operational counter to be lower than certificate
abailly-iohk 18c3279
Mutate context's operational counter to be greater than certificate's
abailly-iohk c0baef4
Replace CBOR encoding with raw encoding for context data
abailly-iohk abc4796
Use Hex encoding instead of Base64 in JSON
abailly-iohk 2105bfe
Generate active slot coefficient as part of test context
abailly-iohk 3ff32df
Add some documentation for (?!) combinator
abailly-iohk fbfdb6e
Format code using script
abailly 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,46 @@ | ||
module GenHeader.Parsers where | ||
|
||
import Cardano.Tools.Headers (Options (..)) | ||
import Data.Version (showVersion) | ||
import Options.Applicative (Parser, ParserInfo, auto, command, | ||
execParser, help, helper, hsubparser, info, long, metavar, | ||
option, progDesc, short, (<**>)) | ||
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 = | ||
hsubparser | ||
( command "generate" (info generateOptionsParser (progDesc "Generate Praos headers context and valid/invalid headers. Writes JSON formatted context to stdout and headers to stdout.")) | ||
<> command "validate" (info validateOptionsParser (progDesc "Validate a sample of Praos headers within a context. Reads JSON formatted sample from stdin.")) | ||
) | ||
|
||
validateOptionsParser :: Parser Options | ||
validateOptionsParser = pure Validate | ||
|
||
generateOptionsParser :: Parser Options | ||
generateOptionsParser = | ||
Generate <$> countParser | ||
|
||
countParser :: Parser Int | ||
countParser = | ||
option | ||
auto | ||
( long "count" | ||
<> short 'c' | ||
<> metavar "INT" | ||
<> help "Number of headers to generate" | ||
) |
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
86 changes: 86 additions & 0 deletions
86
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,86 @@ | ||
{-# LANGUAGE LambdaCase #-} | ||
{-# LANGUAGE NamedFieldPuns #-} | ||
{-# LANGUAGE OverloadedStrings #-} | ||
{-# LANGUAGE TypeApplications #-} | ||
{-# OPTIONS_GHC -Wno-missing-export-lists #-} | ||
|
||
-- | Tooling to generate and validate (Praos) headers. | ||
module Cardano.Tools.Headers where | ||
|
||
import Cardano.Crypto.DSIGN (deriveVerKeyDSIGN) | ||
import Cardano.Crypto.Hash (Blake2b_256, hashToBytes) | ||
import Cardano.Crypto.VRF | ||
(VRFAlgorithm (deriveVerKeyVRF, hashVerKeyVRF)) | ||
import Cardano.Ledger.Api (ConwayEra, StandardCrypto, VRF) | ||
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.Prelude (ExitCode (..), exitWith, forM_, hPutStrLn, | ||
stderr) | ||
import Control.Monad.Except (runExcept) | ||
import qualified Data.Aeson as Json | ||
import qualified Data.ByteString.Base16 as Hex | ||
import qualified Data.ByteString.Lazy as LBS | ||
import qualified Data.Map as Map | ||
import Data.Maybe (fromJust) | ||
import Data.Text (unpack) | ||
import Data.Text.Encoding (decodeUtf8) | ||
import Debug.Trace (trace) | ||
import Ouroboros.Consensus.Block (validateView) | ||
import Ouroboros.Consensus.Protocol.Praos (Praos, | ||
doValidateKESSignature, doValidateVRFSignature) | ||
import qualified Ouroboros.Consensus.Protocol.Praos.Views as Views | ||
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 | ||
= Generate Int | ||
| Validate | ||
|
||
run :: Options -> IO () | ||
run = \case | ||
Generate n -> do | ||
sample <- generateSamples n | ||
LBS.putStr $ Json.encode sample <> "\n" | ||
Validate -> | ||
Json.eitherDecode <$> LBS.getContents >>= \case | ||
Left err -> hPutStrLn stderr err >> exitWith (ExitFailure 1) | ||
Right Sample{sample} -> | ||
forM_ sample $ \(context, mutatedHeader) -> do | ||
print $ validate context mutatedHeader | ||
|
||
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) | expectedError mut err -> Valid mut | ||
(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, ocertCounters, activeSlotCoeff} = context | ||
-- TODO: get these from the context | ||
maxKESEvo = 62 | ||
coin = fromJust . toCompact . Coin | ||
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 | ||
|
||
headerView = validateView @ConwayBlock undefined (mkShelleyHeader header) | ||
validateKES = doValidateKESSignature maxKESEvo praosSlotsPerKESPeriod poolDistr ocertCounters headerView | ||
validateVRF = doValidateVRFSignature nonce poolDistr activeSlotCoeff headerView |
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
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 👍