Skip to content

Commit ebbc24a

Browse files
authored
Documentation and test cases for conformance coverage (#364)
* Catalog of conformance-test coverage * Renamed agda test cases * Defined default topology * Defined default configuration * Test case for genesis slot * DSL for defining events in traces * Test for skipping block production * Test of sporadic block production * More elaborate sequences of trace messages * Applied fourmolu formatting * Updated logbook Fixes #361 Fixes #362
1 parent 6af9965 commit ebbc24a

File tree

10 files changed

+636
-46
lines changed

10 files changed

+636
-46
lines changed

Logbook.md

Lines changed: 60 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,5 +1,65 @@
11
# Leios logbook
22

3+
## 2025-05-22
4+
5+
### Catalog of conformance tests
6+
7+
The [Potential Conformance Tests](leios-trace-verifier/conformance-coverage.md) have been cataloged in order to assess how much positive and negative test coverage is possible for traces from the Leios simulator and (eventually) from the Leios node. This table provides guidance on property-based and other tests that will be added to the test suite.
8+
9+
### Test cases for trace verify and conformance tests
10+
11+
The test suite for the trace verify now contains property-based tests that check whether the conformance testing matches expectations. The suite has both manually curated golden tests and automatically generated property-based tests. Both positive and negative cases are tested. The list will be expanded as the Agda specification for Leios becomes more sophisticated.
12+
13+
```console
14+
Generated trace
15+
Positive cases
16+
Genesis slot [✔]
17+
+++ OK, passed 1 test.
18+
Generate RB [✔]
19+
+++ OK, passed 1 test.
20+
Generate IB [✔]
21+
+++ OK, passed 1 test.
22+
Generate no IB [✔]
23+
+++ OK, passed 1 test.
24+
Generate EB [✔]
25+
+++ OK, passed 1 test.
26+
Generate no EB [✔]
27+
+++ OK, passed 1 test.
28+
Generate VT [✔]
29+
+++ OK, passed 1 test.
30+
Generate no VT [✔]
31+
+++ OK, passed 1 test.
32+
Skip block production [✔]
33+
+++ OK, passed 100 tests.
34+
Sporadic block production [✔]
35+
+++ OK, passed 100 tests.
36+
Noisy block production [✔]
37+
+++ OK, passed 100 tests.
38+
Negative cases
39+
No actions [✔]
40+
+++ OK, passed 1 test.
41+
Start after genesis [✔]
42+
+++ OK, passed 1 test.
43+
Generate equivocated IBs [✔]
44+
+++ OK, passed 1 test.
45+
Generate equivocated EBs [✔]
46+
+++ OK, passed 1 test.
47+
Generate equivocated VTs [✔]
48+
+++ OK, passed 1 test.
49+
Sporadic gaps in production [✔]
50+
+++ OK, passed 100 tests.
51+
Golden traces
52+
Verify valid traces
53+
agda-1.jsonl [✔]
54+
agda-2.jsonl [✔]
55+
Reject invalid traces
56+
case-1.jsonl [✔]
57+
58+
Finished in 0.3541 seconds
59+
20 examples, 0 failures
60+
Test suite test-trace-verifier: PASS
61+
```
62+
363
## 2025-05-20
464

565
### Expected transaction lifecycle
Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,32 @@
1+
# Potential conformance tests
2+
3+
| Test | Currently<br/>in Agda spec | Potentially<br/>in Agda spec | Potentially<br/>outside of Agda spec |
4+
| -------------------------------------------------------------------------------------------- | :------------------------: | :--------------------------: | :----------------------------------: |
5+
| Node either produces an IB or declares not || | |
6+
| Node either produces and EB or declares not || | |
7+
| Node either votes or declares not || | |
8+
| Node produces IB iff sortition requires ||| |
9+
| Node produces EB iff sortition requires ||| |
10+
| Node produces a maximum of one IB per slot | **?** | | |
11+
| Node produces a maximum of one EB per stage | **?** | | |
12+
| Node produces a maximum of one vote per stage | **?** | | |
13+
| Node votes iff sortition requires ||| |
14+
| Node votes on EB iff it is in the same pipeline as the voting | **?** | | |
15+
| Node diffuses non-expired IBs iff not equivocated twice or more | **?** | | |
16+
| Node diffuses non-expired EBs iff not equivocated twice or more | **?** | | |
17+
| Node does not diffuse expired IBs | **?** | | |
18+
| Node does not reference expired IBs in EBs | **?** | | |
19+
| Node does not diffuse expired EBs | **?** | | |
20+
| Node does not reference expired EBs in EBs | **?** | | |
21+
| Node does not reference expired EBs in RB certificates | **?** | | |
22+
| Nodes does not reference an IB by a new EB if the IB is known to be referenced by another EB | **?** | | |
23+
| Node's produced EB references the most recent RB known to it | **?** | | |
24+
| Node's produced EB includes IBs from current pipeline iff the IB has arrived in time | **?** | | |
25+
| Node's produced EB includes IBs from prior pipelines iff the IBs are eligible | **?** | | |
26+
| Node certifies EB and includes it in RB iff there is a quorum of votes | **?** | | |
27+
| Node diffuses IBs in freshest-first order | **?** | | |
28+
| Node diffuses EBs in freshest-first order | **?** | | |
29+
| Node diffuses votes in freshest-first order | **?** | | |
30+
| Node includes txs in IB iff the IB has the correct shard || | |
31+
| Node does not include txs in IB if it has seen a conflicting tx in an IB || | |
32+
| | | | |
Lines changed: 6 additions & 43 deletions
Original file line numberDiff line numberDiff line change
@@ -1,48 +1,11 @@
1-
{-# LANGUAGE DataKinds #-}
2-
{-# LANGUAGE OverloadedStrings #-}
3-
{-# LANGUAGE RecordWildCards #-}
4-
{-# LANGUAGE ScopedTypeVariables #-}
5-
61
module Main where
72

8-
import Control.Monad (forM_)
9-
import Data.ByteString.Lazy as BSL (readFile)
10-
import Data.List (sort)
11-
import Data.Map (elems, keys)
12-
import Data.Text (Text)
13-
import Data.Yaml (decodeFileThrow)
14-
import LeiosConfig (Config (..))
15-
import LeiosEvents (decodeJSONL)
16-
import LeiosTopology (LocationKind (COORD2D), Node (..), NodeInfo (..), NodeName (..), Topology (..))
17-
import Lib (verifyTrace)
18-
import qualified Paths_trace_parser as Paths
19-
import System.Directory (listDirectory)
20-
import System.FilePath ((</>))
21-
import Test.Hspec (Expectation, SpecWith, describe, hspec, it, shouldBe, shouldNotBe)
3+
import Spec.Generated (generated)
4+
import Spec.Golden (golden)
5+
import Test.Hspec (describe, hspec)
226

237
main :: IO ()
24-
main = do
25-
dir <- Paths.getDataDir
26-
validFiles <- sort <$> listDirectory (dir </> "valid")
27-
invalidFiles <- sort <$> listDirectory (dir </> "invalid")
28-
(top :: Topology COORD2D) <- decodeFileThrow (dir </> "topology.yaml")
29-
(config :: Config) <- decodeFileThrow (dir </> "config.yaml")
30-
let nrNodes = toInteger $ Prelude.length (elems $ nodes top)
31-
let nodeNames = Prelude.map unNodeName (keys $ nodes top)
32-
let stakes = Prelude.map (toInteger . stake . nodeInfo) (elems $ nodes top)
33-
let stakeDistribution = Prelude.zip nodeNames stakes
34-
let stageLength = toInteger (leiosStageLengthSlots config)
35-
let idSut = 0
36-
let check :: String -> String -> [FilePath] -> (Text -> Text -> Expectation) -> SpecWith ()
37-
check label folder files predicate =
38-
describe label $ do
39-
forM_ files $ \file ->
40-
it file $ do
41-
result <-
42-
verifyTrace nrNodes idSut stakeDistribution stageLength
43-
. decodeJSONL
44-
<$> BSL.readFile (dir </> folder </> file)
45-
snd result `predicate` "ok"
8+
main =
469
hspec $ do
47-
check "Verify valid traces" "valid" validFiles shouldBe
48-
check "Reject invalid traces" "invalid" invalidFiles shouldNotBe
10+
describe "Generated trace" generated
11+
describe "Golden traces" golden
Lines changed: 186 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,186 @@
1+
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE FlexibleContexts #-}
3+
{-# LANGUAGE OverloadedStrings #-}
4+
{-# LANGUAGE RecordWildCards #-}
5+
6+
module Spec.Generated where
7+
8+
import Control.Monad (liftM2, mzero, replicateM)
9+
import Data.List (inits)
10+
import Data.Text (Text)
11+
import LeiosConfig (leiosStageLengthSlots)
12+
import LeiosEvents
13+
import LeiosTopology (nodeInfo, nodes, stake, unNodeName)
14+
import Lib (verifyTrace)
15+
import Spec.Transition
16+
import Test.Hspec
17+
import Test.Hspec.QuickCheck
18+
import Test.QuickCheck hiding (scale)
19+
20+
import qualified Data.Map.Strict as M
21+
import qualified Spec.Scenario as Scenario (config, idSut, topology)
22+
23+
verify :: [TraceEvent] -> (Integer, Text)
24+
verify =
25+
let
26+
nrNodes = toInteger . M.size $ nodes Scenario.topology
27+
nodeNames = unNodeName <$> (M.keys $ nodes Scenario.topology)
28+
stakes = toInteger . stake . nodeInfo <$> (M.elems $ nodes Scenario.topology)
29+
stakeDistribution = zip nodeNames stakes
30+
stageLength' = toInteger $ leiosStageLengthSlots Scenario.config
31+
in
32+
verifyTrace nrNodes Scenario.idSut stakeDistribution stageLength'
33+
34+
data Check
35+
= MustBeOkay
36+
| MustNotBeOkay
37+
| MustBe Text
38+
deriving (Show)
39+
40+
check ::
41+
Maybe Integer ->
42+
Check ->
43+
[TraceEvent] ->
44+
Property
45+
check expectedActions expectedMessage events =
46+
let
47+
result = verify events
48+
checkMessage =
49+
case expectedMessage of
50+
MustBeOkay -> (=== "ok")
51+
MustNotBeOkay -> (=/= "ok")
52+
MustBe expectedMessage' -> (=== expectedMessage')
53+
in
54+
case expectedActions of
55+
Nothing -> checkMessage $ snd result
56+
Just expectedActions' -> fst result === expectedActions' .&&. checkMessage (snd result)
57+
58+
newtype SkipProduction = SkipProduction {unSkipProduction :: [Transition]}
59+
deriving (Show)
60+
61+
instance Arbitrary SkipProduction where
62+
arbitrary =
63+
do
64+
let gOdd = (NextSlot :) <$> shuffle [SkipIB, SkipVT]
65+
gEven = (NextSlot :) <$> shuffle [SkipIB, SkipEB, SkipVT]
66+
g = liftM2 (<>) gOdd gEven
67+
n <- choose (1, 25)
68+
SkipProduction . concat <$> replicateM n g
69+
shrink = fmap SkipProduction . init . inits . unSkipProduction
70+
71+
newtype SporadicProduction = SporadicProduction {unSporadicProduction :: [Transition]}
72+
deriving (Show)
73+
74+
instance Arbitrary SporadicProduction where
75+
arbitrary =
76+
do
77+
let gIB = elements [GenerateIB, SkipIB]
78+
gEB = elements [GenerateEB, SkipEB]
79+
gVT = elements [GenerateVT, SkipVT]
80+
gOdd =
81+
do
82+
ib <- gIB
83+
vt <- gVT
84+
(NextSlot :) <$> shuffle [ib, vt]
85+
gEven =
86+
do
87+
ib <- gIB
88+
eb <- gEB
89+
vt <- gVT
90+
(NextSlot :) <$> shuffle [ib, eb, vt]
91+
g = liftM2 (<>) gOdd gEven
92+
n <- choose (1, 25)
93+
SporadicProduction . concat <$> replicateM n g
94+
shrink = fmap SporadicProduction . init . inits . unSporadicProduction
95+
96+
newtype NoisyProduction = NoisyProduction {unNoisyProduction :: [Transition]}
97+
deriving (Show)
98+
99+
instance Arbitrary NoisyProduction where
100+
arbitrary =
101+
do
102+
let gNoise = sublistOf [GenerateRB, ReceiveRB, ReceiveIB, ReceiveEB, ReceiveVT]
103+
gIB = elements [GenerateIB, SkipIB]
104+
gEB = elements [GenerateEB, SkipEB]
105+
gVT = elements [GenerateVT, SkipVT]
106+
gOdd =
107+
do
108+
noise <- gNoise
109+
ib <- gIB
110+
vt <- gVT
111+
(NextSlot :) <$> shuffle ([ib, vt] <> noise)
112+
gEven =
113+
do
114+
noise <- gNoise
115+
ib <- gIB
116+
eb <- gEB
117+
vt <- gVT
118+
(NextSlot :) <$> shuffle ([ib, eb, vt] <> noise)
119+
g = liftM2 (<>) gOdd gEven
120+
n <- choose (1, 25)
121+
NoisyProduction . concat <$> replicateM n g
122+
shrink = fmap NoisyProduction . init . inits . unNoisyProduction
123+
124+
newtype SporadicMisses = SporadicMisses {unSporadicMisses :: [Transition]}
125+
deriving (Show)
126+
127+
instance Arbitrary SporadicMisses where
128+
arbitrary =
129+
do
130+
valid <- unSporadicProduction <$> arbitrary
131+
i <- choose (1, length valid - 1)
132+
pure . SporadicMisses $ take i valid <> drop (i + 1) valid <> pure NextSlot
133+
134+
generated :: Spec
135+
generated =
136+
do
137+
let single = (modifyMaxSuccess (const 1) .) . prop
138+
describe "Positive cases" $ do
139+
single "Genesis slot" $
140+
check mzero MustBeOkay
141+
<$> transitions [NextSlot]
142+
single "Generate RB" $
143+
check mzero MustBeOkay
144+
<$> transitions [NextSlot, GenerateRB]
145+
single "Generate IB" $
146+
check mzero MustBeOkay
147+
<$> transitions [NextSlot, GenerateIB]
148+
single "Generate no IB" $
149+
check mzero MustBeOkay
150+
<$> transitions [NextSlot, SkipIB]
151+
single "Generate EB" $
152+
check mzero MustBeOkay
153+
<$> transitions [NextSlot, SkipIB, SkipVT, NextSlot, GenerateEB]
154+
single "Generate no EB" $
155+
check mzero MustBeOkay
156+
<$> transitions [NextSlot, SkipIB, SkipVT, NextSlot, SkipEB]
157+
single "Generate VT" $
158+
check mzero MustBeOkay
159+
<$> transitions [NextSlot, GenerateVT]
160+
single "Generate no VT" $
161+
check mzero MustBeOkay
162+
<$> transitions [NextSlot, SkipVT]
163+
prop "Skip block production" $ \(SkipProduction actions) ->
164+
check mzero MustBeOkay <$> transitions actions
165+
prop "Sporadic block production" $ \(SporadicProduction actions) ->
166+
check mzero MustBeOkay <$> transitions actions
167+
prop "Noisy block production" $ \(NoisyProduction actions) ->
168+
check mzero MustBeOkay <$> transitions actions
169+
describe "Negative cases" $ do
170+
single "No actions" $
171+
check mzero (MustBe "Invalid Action: Slot Slot-Action 1")
172+
<$> transitions [NextSlot, NextSlot]
173+
single "Start after genesis" $
174+
check mzero (MustBe "Invalid Action: Slot Base\8322b-Action 1")
175+
<$> transitions [SkipSlot, NextSlot]
176+
single "Generate equivocated IBs" $
177+
check mzero (MustBe "Invalid Action: Slot IB-Role-Action 1")
178+
<$> transitions [NextSlot, GenerateIB, GenerateIB]
179+
single "Generate equivocated EBs" $
180+
check mzero (MustBe "Invalid Action: Slot EB-Role-Action 2")
181+
<$> transitions [NextSlot, SkipIB, SkipVT, NextSlot, GenerateEB, GenerateEB]
182+
single "Generate equivocated VTs" $
183+
check mzero (MustBe "Invalid Action: Slot VT-Role-Action 1")
184+
<$> transitions [NextSlot, GenerateVT, GenerateVT]
185+
prop "Sporadic gaps in production" $ \(SporadicMisses actions) ->
186+
check mzero MustNotBeOkay <$> transitions actions
Lines changed: 49 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,49 @@
1+
{-# LANGUAGE DataKinds #-}
2+
{-# LANGUAGE OverloadedStrings #-}
3+
{-# LANGUAGE RecordWildCards #-}
4+
{-# LANGUAGE ScopedTypeVariables #-}
5+
6+
module Spec.Golden (
7+
golden,
8+
) where
9+
10+
import Control.Monad (forM_)
11+
import Data.ByteString.Lazy as BSL (readFile)
12+
import Data.List (sort)
13+
import Data.Map (elems, keys)
14+
import Data.Text (Text)
15+
import Data.Yaml (decodeFileThrow)
16+
import LeiosConfig (Config (..))
17+
import LeiosEvents (decodeJSONL)
18+
import LeiosTopology (LocationKind (COORD2D), Node (..), NodeInfo (..), NodeName (..), Topology (..))
19+
import Lib (verifyTrace)
20+
import qualified Paths_trace_parser as Paths
21+
import System.Directory (listDirectory)
22+
import System.FilePath ((</>))
23+
import Test.Hspec (Expectation, Spec, SpecWith, describe, it, runIO, shouldBe, shouldNotBe)
24+
25+
golden :: Spec
26+
golden = do
27+
dir <- runIO $ Paths.getDataDir
28+
validFiles <- runIO $ sort <$> listDirectory (dir </> "valid")
29+
invalidFiles <- runIO $ sort <$> listDirectory (dir </> "invalid")
30+
(top :: Topology COORD2D) <- runIO $ decodeFileThrow (dir </> "topology.yaml")
31+
(config :: Config) <- runIO $ decodeFileThrow (dir </> "config.yaml")
32+
let nrNodes = toInteger $ Prelude.length (elems $ nodes top)
33+
let nodeNames = Prelude.map unNodeName (keys $ nodes top)
34+
let stakes = Prelude.map (toInteger . stake . nodeInfo) (elems $ nodes top)
35+
let stakeDistribution = Prelude.zip nodeNames stakes
36+
let stageLength = toInteger (leiosStageLengthSlots config)
37+
let idSut = 0
38+
let check :: String -> String -> [FilePath] -> (Text -> Text -> Expectation) -> SpecWith ()
39+
check label folder files predicate =
40+
describe label $ do
41+
forM_ files $ \file ->
42+
it file $ do
43+
result <-
44+
verifyTrace nrNodes idSut stakeDistribution stageLength
45+
. decodeJSONL
46+
<$> BSL.readFile (dir </> folder </> file)
47+
snd result `predicate` "ok"
48+
check "Verify valid traces" "valid" validFiles shouldBe
49+
check "Reject invalid traces" "invalid" invalidFiles shouldNotBe

0 commit comments

Comments
 (0)