diff --git a/analysis/markov/Linleios.lean b/analysis/markov/Linleios.lean index 3920332dc..c48d5238b 100644 --- a/analysis/markov/Linleios.lean +++ b/analysis/markov/Linleios.lean @@ -1 +1,5 @@ import Linleios.Evolve + +/-! +# Linleios: a Markovian model of Linear Leios +-/ diff --git a/analysis/markov/Linleios/Evolve.lean b/analysis/markov/Linleios/Evolve.lean index 149591076..39e25d049 100644 --- a/analysis/markov/Linleios/Evolve.lean +++ b/analysis/markov/Linleios/Evolve.lean @@ -11,6 +11,9 @@ open Lean.ToJson (toJson) open Std (HashMap) +/-- +Try to forge an RB in this substep, given the state and environment. +-/ def forgeRb {env : Environment} (state : State) : Outcomes := let state' := { @@ -23,6 +26,9 @@ def forgeRb {env : Environment} (state : State) : Outcomes := , ({state' with hasRb := false, canCertify := false}, 1 - p) ] +/-- +Try to include a certificate in the latest RB being forged in this substep, given the state and environment. +-/ def certify {env : Environment} (state : State) : Outcomes := if state.hasRb && state.canCertify then let p := env.pSpacingOkay @@ -32,6 +38,9 @@ def certify {env : Environment} (state : State) : Outcomes := ] else [(state, 1)] +/-- +Try to forge an EB in this substep, given the state and environment. +-/ def forgeEb {env : Environment} (state : State) : Outcomes := if state.hasRb then let p := 1 - env.pLate @@ -41,6 +50,9 @@ def forgeEb {env : Environment} (state : State) : Outcomes := ] else [(state, 1)] +/-- +Try to vote for an EB in this substep, given the state and environment. +-/ def vote {env : Environment} (state : State) : Outcomes := if state.hasRb then let p := env.pQuorum @@ -50,13 +62,22 @@ def vote {env : Environment} (state : State) : Outcomes := ] else [(state, 1)] +/-- +Step forward to the next potential block. +-/ def step {env : Environment} : List (State → Outcomes) := [@forgeRb env, @certify env, @forgeEb env, @vote env] +/-- +Discard probabilities below the specified threshold. +-/ def prune (ε : Float) : Probabilities → Probabilities := HashMap.filter (fun _ p => p > ε) +/-- +Evolve state probabilities on step forward according the a transition function. +-/ def evolve (transition : State → Outcomes) : Probabilities → Probabilities := HashMap.fold ( @@ -68,19 +89,32 @@ def evolve (transition : State → Outcomes) : Probabilities → Probabilities : ) ∅ +/-- +Chain a sequence of transitions sequentially, evolving probabilities. +-/ def chain (transitions : List (State → Outcomes)) : Probabilities → Probabilities := match transitions with | [] => id | (t :: ts) => chain ts ∘ evolve t +/-- +Simulate the specified number of potential blocks, given a starting set of probabilities. +-/ def simulate (env : Environment) (start : Probabilities) (ε : Float) : Nat → Probabilities | 0 => start | n + 1 => let state' := prune ε $ chain (@step env) start simulate env state' ε n + +/-- +Compute the total probabilities of a set of states. +-/ def totalProbability (states : Probabilities) : Probability := states.values.sum +/-- +Compute the distribution of EB counts. +-/ def ebDistribution : Probabilities → HashMap Nat Probability := HashMap.fold ( @@ -90,6 +124,9 @@ def ebDistribution : Probabilities → HashMap Nat Probability := ) ∅ +/-- +Format the distribution of EB counts as JSON. +-/ def ebDistributionJson : Probabilities → Json := Json.mkObj ∘ List.map (fun ⟨k, v⟩ => ⟨toString k, toJson v⟩) @@ -97,6 +134,9 @@ def ebDistributionJson : Probabilities → Json := ∘ HashMap.toList ∘ ebDistribution +/-- +Compute the RB efficiency, given a set of states. +-/ def rbEfficiency (states : Probabilities) : Float := let clock := states.keys.head!.clock let rbCount := @@ -106,6 +146,9 @@ def rbEfficiency (states : Probabilities) : Float := states rbCount / clock.toFloat +/-- +Compute the EB efficiency, given a set of states. +-/ def ebEfficiency (states : Probabilities) : Float := let clock := states.keys.head!.clock let ebCount := @@ -115,6 +158,9 @@ def ebEfficiency (states : Probabilities) : Float := states ebCount / (clock.toFloat - 1) +/-- +Compute the overall efficiency, give a set of states. +-/ def efficiency (states : Probabilities) : Float := let rb := rbEfficiency states let eb := ebEfficiency states diff --git a/analysis/markov/Linleios/Probability.lean b/analysis/markov/Linleios/Probability.lean index 5c061ca71..8ad4b606e 100644 --- a/analysis/markov/Linleios/Probability.lean +++ b/analysis/markov/Linleios/Probability.lean @@ -2,11 +2,20 @@ import Linleios.Util +/-- +Number of stake pools. +-/ def nPools : Nat := 2500 +/-- +Compute a realistic stake distribution for the specified number of pools. +-/ def stakeDistribution (nPools : Nat) : List Float := (List.range nPools).map (fun k => ((k + 1).toFloat / nPools.toFloat)^10 - (k.toFloat / nPools.toFloat)^10) +/-- +Determine the distribution parameter that achieves the specified committee size. +-/ private def calibrateCommittee(committeeSize : Float) : Float := let stakes : List Float := stakeDistribution nPools let f (m : Float) : Float := @@ -14,6 +23,9 @@ private def calibrateCommittee(committeeSize : Float) : Float := ps.sum - committeeSize bisectionSearch f committeeSize nPools.toFloat 0.5 10 +/-- +Compute the mean and standard deviation of the committee size, given the probability of a successful vote and a target committee size. +-/ private def committeeDistribution (pSuccessfulVote committeeSize : Float) : Float × Float := let stakes : List Float := stakeDistribution nPools let m := calibrateCommittee committeeSize @@ -22,6 +34,9 @@ private def committeeDistribution (pSuccessfulVote committeeSize : Float) : Floa let σ := (ps.map (fun p => p * (1 - p))).sum.sqrt ⟨ μ , σ ⟩ +/-- +Compute the probability of a quorum, given the probability of a successful vote, the target committee size, and the quorum fraction. +-/ def pQuorum (pSuccessfulVote committeeSize τ : Float) : Float := let ⟨ μ , σ ⟩ := committeeDistribution pSuccessfulVote committeeSize 1 - cdfGaussian (τ * committeeSize) μ σ diff --git a/analysis/markov/Linleios/Types.lean b/analysis/markov/Linleios/Types.lean index f1051b0a9..0cc4df299 100644 --- a/analysis/markov/Linleios/Types.lean +++ b/analysis/markov/Linleios/Types.lean @@ -7,20 +7,44 @@ import Linleios.Probability open Std (HashMap) +/-- +Represent probabilities as floating-point numbers. +-/ abbrev Probability := Float - +/-- +The constant parameters used for computing transitions. +-/ structure Environment where + /-- The active slot coefficient. -/ activeSlotCoefficient : Probability + /-- The $L_\text{hdr}$ protocol parameter. -/ Lheader : Nat + /-- The $L_\text{vote}$ protocol parameter. -/ Lvote : Nat + /-- The $L_\text{diff}$ protocol parameter. -/ Ldiff : Nat + /-- The probability that an RB occurs long enough after the previous RB so that an EB can be certified. -/ pSpacingOkay : Probability + /-- The per-step quorum probability. -/ pQuorum : Probability + /-- The probability that the EB and transaction data arrives too late to compute the ledger. -/ pLate : Probability + /-- The fraction of adversarial stake. -/ fAdversary : Float deriving Repr +/-- +Create an environment. + +- `activeSlotCoefficient`: the active slot coefficient +- `committeeSize`: the mean committee size +- `τ`: the quorum fraction +- `pRbHeaderArrives`: the probability that an RB header arrives before $L_\text{hdr}$ slots +- `pEBValidates`: the probability that an EB is validated before $3 L_\text{hdr} + L_\text{vote} + L_\text{diff}$ slots +- `pEbUnvalidated`: the probability that the EB and transaction data arrives too late to compute the ledger +- `fAdversary`: the fraction of adversarial stake +-/ def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committeeSize τ pRbHeaderArrives pEbValidates pEbUnvalidated fAdversary : Float) : Environment := { activeSlotCoefficient := activeSlotCoefficient @@ -34,14 +58,25 @@ def makeEnvironment (Lheader Lvote Ldiff : Nat) (activeSlotCoefficient committee } +/-- +The state of the chain's evolution. +-/ structure State where + /-- The number of potential RB oppurtunities. -/ clock : Nat + /-- The number of RBs actually forged. -/ rbCount : Nat + /-- The number of EBs certified. -/ ebCount : Nat + /-- Whether an RB was forged in the current step. -/ hasRb : Bool + /-- Whether an EB could be certified in the current step. -/ canCertify : Bool deriving Repr, BEq, Hashable, Inhabited +/-- +The genesis state starts when zero counts. +-/ theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 ∧ (default : State).ebCount = 0 := by constructor rfl @@ -50,6 +85,9 @@ theorem genesis : (default : State).clock = 0 ∧ (default : State).rbCount = 0 rfl +/-- +The active states and their probabilities. +-/ def Probabilities := HashMap State Probability deriving Repr, EmptyCollection @@ -57,4 +95,6 @@ instance : Inhabited Probabilities where default := (∅ : Probabilities).insert Inhabited.default 1 +/-- +An outcome is a list of new states and their probabilities. -/ abbrev Outcomes := List (State × Probability) diff --git a/analysis/markov/Linleios/Util.lean b/analysis/markov/Linleios/Util.lean index 9c55bd4e7..6398abda4 100644 --- a/analysis/markov/Linleios/Util.lean +++ b/analysis/markov/Linleios/Util.lean @@ -1,4 +1,7 @@ +/-- +The error function. +-/ partial def erf (x : Float) : Float := if x < 0 then - erf (- x) @@ -12,9 +15,15 @@ partial def erf (x : Float) : Float := let t := 1 / (1 + p * x) 1 - (a₁ * t + a₂ * t^2 + a₃ * t^3 + a₄ * t^4 + a₅ * t^5) * Float.exp (- x^2) +/-- +The CDF for a normal distribution. +-/ def cdfGaussian (x μ σ : Float) : Float := (1 + erf ((x - μ) / σ / Float.sqrt 2)) / 2 +/-- +A bisection search. +-/ def bisectionSearch (f : Float → Float) (low high : Float) (ε : Float) (maxIter : Nat) : Float := match maxIter with | 0 => (low + high) / 2 diff --git a/analysis/markov/docbuild/.gitignore b/analysis/markov/docbuild/.gitignore new file mode 100644 index 000000000..2b0095269 --- /dev/null +++ b/analysis/markov/docbuild/.gitignore @@ -0,0 +1 @@ +.lake diff --git a/analysis/markov/docbuild/ReadMe.md b/analysis/markov/docbuild/ReadMe.md new file mode 100644 index 000000000..de6ed664e --- /dev/null +++ b/analysis/markov/docbuild/ReadMe.md @@ -0,0 +1,7 @@ +# Building the documentation + +See https://github.com/leanprover/doc-gen4/tree/v4.24.0 for detailed instructions. + +1. In this folder, execute `MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4`. +2. Also in this folder, execute `lake build Linleios:docs`. +3. View the documentation at `./.lake/doc/index.html`. diff --git a/analysis/markov/docbuild/lake-manifest.json b/analysis/markov/docbuild/lake-manifest.json new file mode 100644 index 000000000..b194078cc --- /dev/null +++ b/analysis/markov/docbuild/lake-manifest.json @@ -0,0 +1,152 @@ +{"version": "1.1.0", + "packagesDir": "../.lake/packages", + "packages": + [{"url": "https://github.com/leanprover/doc-gen4", + "type": "git", + "subDir": null, + "scope": "leanprover", + "rev": "efe744c75a6ab384619513b9762db1cfc40b0fe4", + "name": "«doc-gen4»", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.20.0", + "inherited": false, + "configFile": "lakefile.lean"}, + {"type": "path", + "scope": "", + "name": "linleios", + "manifestFile": "lake-manifest.json", + "inherited": false, + "dir": "../", + "configFile": "lakefile.toml"}, + {"url": "https://github.com/mhuisi/lean4-cli", + "type": "git", + "subDir": null, + "scope": "", + "rev": "4f22c09e7ded721e6ecd3cf59221c4647ca49664", + "name": "Cli", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/fgdorais/lean4-unicode-basic", + "type": "git", + "subDir": null, + "scope": "", + "rev": "45c426d1cb016fcb4fcbe043f1cd2d97acb2dbc3", + "name": "UnicodeBasic", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/dupuisf/BibtexQuery", + "type": "git", + "subDir": null, + "scope": "", + "rev": "dbfe2b7630c5f7c5c1cf71e7747ffc0a30337f69", + "name": "BibtexQuery", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/acmepjz/md4lean", + "type": "git", + "subDir": null, + "scope": "", + "rev": "8ba0ef10d178ab95a5d6fe3cfbd586c6ecef2717", + "name": "MD4Lean", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/fgdorais/lean4-parser", + "type": "git", + "subDir": null, + "scope": "", + "rev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad", + "name": "Parser", + "manifestFile": "lake-manifest.json", + "inputRev": "26d5ce4d60195a869b1fdb100b442794ea63e1ad", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/mathlib4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "c211948581bde9846a99e32d97a03f0d5307c31e", + "name": "mathlib", + "manifestFile": "lake-manifest.json", + "inputRev": "v4.20.0", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/batteries", + "type": "git", + "subDir": null, + "scope": "", + "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e", + "name": "batteries", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/plausible", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2ac43674e92a695e96caac19f4002b25434636da", + "name": "plausible", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/LeanSearchClient", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120", + "name": "LeanSearchClient", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/import-graph", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d", + "name": "importGraph", + "manifestFile": "lake-manifest.json", + "inputRev": "main", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/ProofWidgets4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306", + "name": "proofwidgets", + "manifestFile": "lake-manifest.json", + "inputRev": "v0.0.60", + "inherited": true, + "configFile": "lakefile.lean"}, + {"url": "https://github.com/leanprover-community/aesop", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a", + "name": "aesop", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}, + {"url": "https://github.com/leanprover-community/quote4", + "type": "git", + "subDir": null, + "scope": "leanprover-community", + "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a", + "name": "Qq", + "manifestFile": "lake-manifest.json", + "inputRev": "master", + "inherited": true, + "configFile": "lakefile.toml"}], + "name": "docbuild", + "lakeDir": ".lake"} diff --git a/analysis/markov/docbuild/lakefile.toml b/analysis/markov/docbuild/lakefile.toml new file mode 100644 index 000000000..e03061e5e --- /dev/null +++ b/analysis/markov/docbuild/lakefile.toml @@ -0,0 +1,15 @@ +name = "docbuild" +reservoir = false +version = "0.1.0" +packagesDir = "../.lake/packages" + +[[require]] +name = "linleios" +path = "../" + +[[require]] +scope = "leanprover" +name = "doc-gen4" +# If you are developing against a release candidate or a stable version `v4.x`, replace `main` below by `v4.x`. +# If you do not use `main` keep in mind to update this field as you update your Lean version. +rev = "v4.20.0" diff --git a/analysis/markov/docbuild/lean-toolchain b/analysis/markov/docbuild/lean-toolchain new file mode 100644 index 000000000..52fe77473 --- /dev/null +++ b/analysis/markov/docbuild/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.20.0 diff --git a/leios-trace-verifier/hs-src/app/linear/Main.hs b/leios-trace-verifier/hs-src/app/linear/Main.hs index b3af08a8b..a0cbad28c 100644 --- a/leios-trace-verifier/hs-src/app/linear/Main.hs +++ b/leios-trace-verifier/hs-src/app/linear/Main.hs @@ -2,6 +2,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +-- | Main entry for trace verification of Linear Leios. module Main where import Control.Monad (unless) @@ -18,6 +19,7 @@ import System.IO (hPutStrLn, stderr) import qualified Data.Text as T (unpack) +-- | Run the CLI. main :: IO () main = do @@ -47,6 +49,7 @@ main = putStrLn . T.unpack $ snd (snd result) exitFailure +-- | CLI commands. data Command = Command { logFile :: FilePath , configFile :: FilePath @@ -55,6 +58,7 @@ data Command = Command } deriving (Eq, Ord, Read, Show) +-- | Command parser. commandParser :: ParserInfo Command commandParser = info (com <**> helper) $ diff --git a/leios-trace-verifier/hs-src/app/short/Main.hs b/leios-trace-verifier/hs-src/app/short/Main.hs index ee43f3fa0..08713099d 100644 --- a/leios-trace-verifier/hs-src/app/short/Main.hs +++ b/leios-trace-verifier/hs-src/app/short/Main.hs @@ -2,6 +2,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +-- | Main entry for trace verification of Short Leios. module Main where import Control.Monad (unless) @@ -18,6 +19,7 @@ import System.IO (hPutStrLn, stderr) import qualified Data.Text as T (unpack) +-- | Run the CLI. main :: IO () main = do @@ -47,6 +49,7 @@ main = putStrLn . T.unpack $ snd (snd result) exitFailure +-- | CLI commands. data Command = Command { logFile :: FilePath , configFile :: FilePath @@ -55,6 +58,7 @@ data Command = Command } deriving (Eq, Ord, Read, Show) +-- | Command parser. commandParser :: ParserInfo Command commandParser = info (com <**> helper) $ diff --git a/leios-trace-verifier/hs-src/src/LinearLeiosLib.hs b/leios-trace-verifier/hs-src/src/LinearLeiosLib.hs index 0306b83f9..4b22fd89a 100644 --- a/leios-trace-verifier/hs-src/src/LinearLeiosLib.hs +++ b/leios-trace-verifier/hs-src/src/LinearLeiosLib.hs @@ -1,3 +1,4 @@ +-- | Imports from Agda. module LinearLeiosLib ( module P, module V, diff --git a/leios-trace-verifier/hs-src/src/ShortLeiosLib.hs b/leios-trace-verifier/hs-src/src/ShortLeiosLib.hs index 82e34b0cc..1d2f3f665 100644 --- a/leios-trace-verifier/hs-src/src/ShortLeiosLib.hs +++ b/leios-trace-verifier/hs-src/src/ShortLeiosLib.hs @@ -1,3 +1,4 @@ +-- | Imports from Agda. module ShortLeiosLib ( module P, module V, diff --git a/leios-trace-verifier/hs-src/test/Spec.hs b/leios-trace-verifier/hs-src/test/Spec.hs index 82d71b21c..c58a79e6a 100644 --- a/leios-trace-verifier/hs-src/test/Spec.hs +++ b/leios-trace-verifier/hs-src/test/Spec.hs @@ -1,9 +1,12 @@ +-- | Main entry point. + module Main where import Spec.Generated (generated) import Spec.Golden (golden) import Test.Hspec (describe, hspec) +-- | Test the trace verifier. main :: IO () main = hspec $ do diff --git a/leios-trace-verifier/hs-src/test/Spec/Generated.hs b/leios-trace-verifier/hs-src/test/Spec/Generated.hs index acc689266..124538aef 100644 --- a/leios-trace-verifier/hs-src/test/Spec/Generated.hs +++ b/leios-trace-verifier/hs-src/test/Spec/Generated.hs @@ -3,6 +3,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +-- | Arbitrary and generated tests. module Spec.Generated where import Control.Monad (join, liftM2, mzero, replicateM) @@ -20,6 +21,7 @@ import Test.QuickCheck hiding (scale) import qualified Data.Map.Strict as M import qualified Spec.Scenario as Scenario (config, idSut, topology) +-- | Run the verify on a list of events. verify :: [TraceEvent] -> (Integer, (Text, Text)) verify = let @@ -33,12 +35,14 @@ verify = in verifyTrace nrNodes Scenario.idSut stakeDistribution stageLength' ledgerQuality lateIBInclusion +-- | Expectation for checking a trace. data Check = MustBeOkay | MustNotBeOkay | MustBe Text deriving (Show) +-- | Check that a trace has the expected number of actions and result. check :: Maybe Integer -> Check -> @@ -57,6 +61,7 @@ check expectedActions expectedMessage events = Nothing -> checkMessage $ fst (snd result) Just expectedActions' -> fst result === expectedActions' .&&. checkMessage (fst (snd result)) +-- | Generate the initial IB and events leading up to it. initStageIB :: Gen [Transition] initStageIB = let @@ -65,6 +70,7 @@ initStageIB = in join <$> replicateM stageLength' ((: [NextSlot]) <$> gIB) +-- | Generate the initial EB and events leading up to it. initStageEB :: Gen [Transition] initStageEB = let @@ -79,6 +85,7 @@ initStageEB = a <- join <$> replicateM (stageLength' - 1) ((: [NextSlot]) <$> gIB) pure $ l ++ [NextSlot] ++ a +-- | Generate the initial vote and events leading up to it. initStageVT :: Gen [Transition] initStageVT = let @@ -103,6 +110,7 @@ initStageVT = ) pure $ l ++ [NextSlot] ++ a +-- | Generate the initial events. initPipelines :: Gen [Transition] initPipelines = do s1 <- initStageIB @@ -112,6 +120,7 @@ initPipelines = do s5 <- initStageVT pure $ s1 ++ s2 ++ s3 ++ s4 ++ s5 +-- | Wrapper for skipping production of RBs, IBs, EBs, or votes. newtype SkipProduction = SkipProduction {unSkipProduction :: [Transition]} deriving (Show) @@ -127,6 +136,7 @@ instance Arbitrary SkipProduction where pure $ SkipProduction (i ++ r) shrink = fmap SkipProduction . init . inits . unSkipProduction +-- | Wrapper for sporadic production of RBs, IBs, EBs, or votes. newtype SporadicProduction = SporadicProduction {unSporadicProduction :: [Transition]} deriving (Show) @@ -153,6 +163,7 @@ instance Arbitrary SporadicProduction where pure $ SporadicProduction (i ++ r) shrink = fmap SporadicProduction . init . inits . unSporadicProduction +-- | Wrapper for noisy production (i.e., shuffled) of RBs, IBs, EB, and votes. newtype NoisyProduction = NoisyProduction {unNoisyProduction :: [Transition]} deriving (Show) @@ -182,6 +193,7 @@ instance Arbitrary NoisyProduction where pure $ NoisyProduction (i ++ r) shrink = fmap NoisyProduction . init . inits . unNoisyProduction +-- | Wrapper for sporadically missing RBs, IBs, EB, and votes. newtype SporadicMisses = SporadicMisses {unSporadicMisses :: [Transition]} deriving (Show) @@ -192,6 +204,7 @@ instance Arbitrary SporadicMisses where i <- choose (1, length valid - 1) pure . SporadicMisses $ take i valid <> drop (i + 1) valid <> pure NextSlot +-- | Generate tests. generated :: Spec generated = do diff --git a/leios-trace-verifier/hs-src/test/Spec/Golden.hs b/leios-trace-verifier/hs-src/test/Spec/Golden.hs index c4ac0c8dd..cd76b4161 100644 --- a/leios-trace-verifier/hs-src/test/Spec/Golden.hs +++ b/leios-trace-verifier/hs-src/test/Spec/Golden.hs @@ -3,6 +3,7 @@ {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} +-- | Golden tests. module Spec.Golden ( golden, ) where @@ -22,6 +23,7 @@ import System.Directory (listDirectory) import System.FilePath (()) import Test.Hspec (Expectation, Spec, SpecWith, describe, it, runIO, shouldBe, shouldNotBe) +-- | Run golden tests. golden :: Spec golden = do dir <- runIO $ Paths.getDataDir diff --git a/leios-trace-verifier/hs-src/test/Spec/Scenario.hs b/leios-trace-verifier/hs-src/test/Spec/Scenario.hs index cc0e6801b..b18ca7ecd 100644 --- a/leios-trace-verifier/hs-src/test/Spec/Scenario.hs +++ b/leios-trace-verifier/hs-src/test/Spec/Scenario.hs @@ -3,6 +3,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +-- | Scenario variables for tests. module Spec.Scenario ( config, topology, @@ -19,14 +20,18 @@ import LeiosTypes (Point (..)) import qualified Data.Map.Strict as M import qualified Data.Set as S +-- | The protocol configuration. config :: Config config = def{relayStrategy = RequestFromFirst, tcpCongestionControl = True, multiplexMiniProtocols = True, treatBlocksAsFull = False, cleanupPolicies = CleanupPolicies (S.fromList [CleanupExpiredVote]), simulateTransactions = True, leiosStageLengthSlots = 2, leiosStageActiveVotingSlots = 1, leiosVoteSendRecvStages = False, leiosVariant = Short, leiosLateIbInclusion = False, leiosHeaderDiffusionTimeMs = 1000.0, praosChainQuality = 20.0, txGenerationDistribution = Exp{lambda = 0.85, scale = pure 1000.0}, txSizeBytesDistribution = LogNormal{mu = 6.833, sigma = 1.127}, txValidationCpuTimeMs = 1.5, txMaxSizeBytes = 16384, rbGenerationProbability = 5.0e-2, rbGenerationCpuTimeMs = 1.0, rbHeadValidationCpuTimeMs = 1.0, rbHeadSizeBytes = 1024, rbBodyMaxSizeBytes = 90112, rbBodyLegacyPraosPayloadValidationCpuTimeMsConstant = 50.0, rbBodyLegacyPraosPayloadValidationCpuTimeMsPerByte = 5.0e-4, rbBodyLegacyPraosPayloadAvgSizeBytes = 0, ibGenerationProbability = 5.0, ibGenerationCpuTimeMs = 130.0, ibHeadSizeBytes = 304, ibHeadValidationCpuTimeMs = 1.0, ibBodyValidationCpuTimeMsConstant = 50.0, ibBodyValidationCpuTimeMsPerByte = 5.0e-4, ibBodyMaxSizeBytes = 327680, ibBodyAvgSizeBytes = 98304, ibDiffusionStrategy = FreshestFirst, ibDiffusionMaxWindowSize = 100, ibDiffusionMaxHeadersToRequest = 100, ibDiffusionMaxBodiesToRequest = 1, ibShards = 50, ebGenerationProbability = 1.5, ebGenerationCpuTimeMs = 75.0, ebValidationCpuTimeMs = 1.0, ebSizeBytesConstant = 240, ebSizeBytesPerIb = 32, ebDiffusionStrategy = PeerOrder, ebDiffusionMaxWindowSize = 100, ebDiffusionMaxHeadersToRequest = 100, ebDiffusionMaxBodiesToRequest = 1, ebMaxAgeSlots = 100, ebMaxAgeForRelaySlots = 40, voteGenerationProbability = 500.0, voteGenerationCpuTimeMsConstant = 0.164, voteGenerationCpuTimeMsPerIb = 0.0, voteValidationCpuTimeMs = 0.816, voteThreshold = 300, voteBundleSizeBytesConstant = 0, voteBundleSizeBytesPerEb = 105, voteDiffusionStrategy = PeerOrder, voteDiffusionMaxWindowSize = 100, voteDiffusionMaxHeadersToRequest = 100, voteDiffusionMaxBodiesToRequest = 1, certGenerationCpuTimeMsConstant = 90.0, certGenerationCpuTimeMsPerNode = 0.0, certValidationCpuTimeMsConstant = 130.0, certValidationCpuTimeMsPerNode = 0.0, certSizeBytesConstant = 7168, certSizeBytesPerNode = 0} +-- | The topology. topology :: Topology 'COORD2D topology = Topology{nodes = M.fromList [(NodeName "node-0", Node{nodeInfo = NodeInfo{stake = 500, cpuCoreCount = CpuCoreCount mzero, location = LocCoord2D{coord2D = Point{_1 = 0.12000040231003672, _2 = 0.1631004621065356}}, adversarial = mzero}, producers = M.fromList [(NodeName "node-1", LinkInfo{latencyMs = 141.01364015418432, bandwidthBytesPerSecond = BandwidthBps $ pure 1024000}), (NodeName "node-2", LinkInfo{latencyMs = 254.6249782835189, bandwidthBytesPerSecond = BandwidthBps $ pure 1024000})]}), (NodeName "node-1", Node{nodeInfo = NodeInfo{stake = 200, cpuCoreCount = CpuCoreCount mzero, location = LocCoord2D{coord2D = Point{_1 = 0.34276660615051174, _2 = 0.2636899791034371}}, adversarial = mzero}, producers = M.fromList [(NodeName "node-2", LinkInfo{latencyMs = 175.32530255486685, bandwidthBytesPerSecond = BandwidthBps $ pure 1024000}), (NodeName "node-3", LinkInfo{latencyMs = 379.1167948193313, bandwidthBytesPerSecond = BandwidthBps $ pure 1024000})]}), (NodeName "node-2", Node{nodeInfo = NodeInfo{stake = 100, cpuCoreCount = CpuCoreCount mzero, location = LocCoord2D{coord2D = Point{_1 = 0.5150493264153491, _2 = 0.27873594531347595}}, adversarial = mzero}, producers = M.fromList [(NodeName "node-3", LinkInfo{latencyMs = 248.31457793649423, bandwidthBytesPerSecond = BandwidthBps $ pure 1024000})]}), (NodeName "node-3", Node{nodeInfo = NodeInfo{stake = 0, cpuCoreCount = CpuCoreCount mzero, location = LocCoord2D{coord2D = Point{_1 = 0.3503537969220088, _2 = 0.13879558055660354}}, adversarial = mzero}, producers = M.fromList [(NodeName "node-0", LinkInfo{latencyMs = 140.19739576271448, bandwidthBytesPerSecond = BandwidthBps $ pure 1024000})]})]} +-- | The system under test. idSut :: Integer idSut = 0 +-- | The system not under test. idOther :: Integer idOther = 1 diff --git a/leios-trace-verifier/hs-src/test/Spec/Transition.hs b/leios-trace-verifier/hs-src/test/Spec/Transition.hs index ed9e05ec5..b830d5ee1 100644 --- a/leios-trace-verifier/hs-src/test/Spec/Transition.hs +++ b/leios-trace-verifier/hs-src/test/Spec/Transition.hs @@ -3,6 +3,7 @@ {-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} +-- | Generation of valid sequences of events. module Spec.Transition where import Control.Lens hiding (elements) @@ -23,6 +24,7 @@ import qualified Data.Set as S import qualified Data.Text as T import qualified Spec.Scenario as Scenario (config, idOther, idSut) +-- | The context for tracking the state, used in generating valid events. data TracingContext = TracingContext { _clock :: Time , _slotNo :: SlotNo @@ -51,6 +53,8 @@ instance Default TracingContext where Scenario.idOther (leiosStageLengthSlots Scenario.config) +-- Various lenses. + clock :: Lens' TracingContext Time clock = lens _clock $ \ctx x -> ctx{_clock = x} @@ -87,6 +91,7 @@ other = to $ T.pack . ("node-" <>) . show . _idOther stageLength :: Getter TracingContext Word stageLength = to _stageLength +-- | An abstract (i.e., contextless) event. data Transition = NextSlot | SkipSlot @@ -103,6 +108,7 @@ data Transition | ReceiveVT deriving (Show) +-- | Generate a new identifier. genId :: Integer -> Word64 -> Set Text -> Gen Text genId system slot forbidden = let @@ -110,6 +116,7 @@ genId system slot forbidden = in g `suchThat` (not . (`S.member` forbidden)) +-- | Generate a valid RB. genRB :: Integer -> StateT TracingContext Gen (Text, Nullable BlockRef) genRB i = do @@ -123,6 +130,7 @@ genRB i = rbs %= M.insert block_id parent pure (block_id, Nullable . pure $ BlockRef parent) +-- | Generate a valid IB. genIB :: Integer -> StateT TracingContext Gen Text genIB i = do @@ -132,6 +140,7 @@ genIB i = ibs %= S.insert ib pure ib +-- | Generate a valid EB. genEB :: Integer -> StateT TracingContext Gen Text genEB i = do @@ -141,6 +150,7 @@ genEB i = ebs %= S.insert eb pure eb +-- | Generate a valid vote. genVT :: Integer -> StateT TracingContext Gen Text genVT i = do @@ -150,9 +160,11 @@ genVT i = vts %= S.insert vt pure vt +-- | Advance the clock. tick :: StateT TracingContext Gen () tick = clock %= (+ 0.000001) +-- | Generate an actual valid event from its abstract representation. transition :: Transition -> StateT TracingContext Gen [Event] transition SkipSlot = do @@ -257,6 +269,7 @@ transition ReceiveVT = block_id <- genVT =<< use idOther pure [VTBundleReceived{..}] +-- | Generate a valid trace from abstract events. transitions :: [Transition] -> Gen [TraceEvent] transitions = (`evalStateT` def) @@ -264,5 +277,6 @@ transitions = . fmap concat . mapM transition +-- | Timestamp an event. timestamp :: Monad m => Event -> StateT TracingContext m TraceEvent timestamp = uses clock . flip TraceEvent