Add code comments to leios trace verifier

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) $

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) $

leios-trace-verifier/hs-src/src/LinearLeiosLib.hs

@@ -1,3 +1,4 @@
+-- | Imports from Agda.
 module LinearLeiosLib (
   module P,
   module V,

leios-trace-verifier/hs-src/src/ShortLeiosLib.hs

@@ -1,3 +1,4 @@
+-- | Imports from Agda.
 module ShortLeiosLib (
   module P,
   module V,

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

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

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

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

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,13 +108,15 @@ data Transition
   | ReceiveVT
   deriving (Show)
 
+-- | Generate a new identifier.
 genId :: Integer -> Word64 -> Set Text -> Gen Text
 genId system slot forbidden =
   let
     g = T.pack . ((show system <> "-" <> show slot <> "-") <>) . show <$> (arbitrary :: Gen Word16)
    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,12 +269,14 @@ transition ReceiveVT =
     block_id <- genVT =<< use idOther
     pure [VTBundleReceived{..}]
 
+-- | Generate a valid trace from abstract events.
 transitions :: [Transition] -> Gen [TraceEvent]
 transitions =
   (`evalStateT` def)
     . (mapM timestamp =<<)
     . fmap concat
     . mapM transition
 
+-- | Timestamp an event.
 timestamp :: Monad m => Event -> StateT TracingContext m TraceEvent
 timestamp = uses clock . flip TraceEvent