Removed lint.

peras-simulation/app/Peras/Conformance/ExternalSpec.hs

@@ -1,21 +1,17 @@
 module Peras.Conformance.ExternalSpec where
 
-import Control.Monad.State (evalStateT)
-import Data.Default (def)
-import Data.Functor (void)
+import Peras.Conformance.Generators (actionsSizeScaling)
 import Peras.Conformance.Test.External (prop_node)
 import System.IO (Handle)
 import Test.Hspec (Spec, describe)
-import Test.Hspec.QuickCheck (modifyMaxSuccess, prop)
-import Test.QuickCheck (Blind (Blind), Gen, Property, Testable, expectFailure, property)
-import Test.QuickCheck.DynamicLogic (DL, anyActions_, forAllDL)
-import Test.QuickCheck.Gen.Unsafe (Capture (..), capture)
-import Test.QuickCheck.Monadic (PropertyM, assert, monadic')
-import Test.QuickCheck.StateModel (Actions, runActions)
+import Test.Hspec.QuickCheck (prop)
+import Test.QuickCheck (Blind (Blind), arbitrary, forAll, scale)
 
 -- | Test an external implementation against the Agda executable specification.
 spec :: Handle -> Handle -> Spec
 spec hReader hWriter =
   describe "External node"
     . prop "Implementation respects Peras protocol"
-    $ forAllDL anyActions_ (prop_node hReader hWriter . Blind)
+    $ forAll
+      (scale (* actionsSizeScaling) arbitrary)
+      (prop_node hReader hWriter . Blind)

peras-simulation/app/Pipe.hs

@@ -5,19 +5,16 @@
 import Control.Concurrent.Class.MonadSTM (
   MonadSTM (atomically, modifyTVar'),
  )
-import Control.Monad (Monad ((>>=)), void, when, (=<<))
+import Control.Monad (void, when)
 import Control.Monad.IO.Class (MonadIO (..))
-import Control.Monad.State (lift)
-import Control.Tracer (Tracer, nullTracer, traceWith)
+import Control.Tracer (Tracer, nullTracer)
 import qualified Data.Aeson as A
 import qualified Data.ByteString.Char8 as BS8
 import qualified Data.ByteString.Lazy as LBS
 import qualified Data.ByteString.Lazy.Char8 as LBS8
 import Data.Default (def)
 import qualified Data.Map as Map (fromList)
 import qualified Data.Set as Set (fromList)
-import qualified Data.Text.Lazy as T
-import qualified Data.Text.Lazy.Encoding as T
 import Data.Version (showVersion)
 import qualified Options.Applicative as O
 import Paths_peras_simulation (version)
@@ -27,23 +24,20 @@ import Peras.Conformance.Test.External (NodeRequest (..), NodeResponse (..))
 import Peras.Prototype.BlockCreation (blockCreation)
 import Peras.Prototype.BlockSelection (selectBlock)
 import Peras.Prototype.Crypto (mkCommitteeMember, mkParty, mkSlotLeader)
-import Peras.Prototype.Diffusion (Diffuser, allPendingChains, defaultDiffuser, diffuseChain, diffuseVote, popChainsAndVotes)
-import Peras.Prototype.Environment (mkSimpleScenario)
+import Peras.Prototype.Diffusion (diffuseChain, diffuseVote, popChainsAndVotes)
 import Peras.Prototype.Fetching (fetching)
-import Peras.Prototype.Network (simulate, simulateNetwork)
 import Peras.Prototype.Node (
   NodeState (..),
   defaultNodeState,
   initialNodeState,
   tickNode,
  )
-import Peras.Prototype.Trace (PerasLog (Protocol), perasTracer)
+import Peras.Prototype.Trace (PerasLog, perasTracer)
 import Peras.Prototype.Types (
   PerasState (certs, chains, votes),
   inRound,
   newRound,
  )
-import Peras.Prototype.Visualizer (makeVisTracer)
 import Peras.Prototype.Voting (voting)
 import System.Exit (die)
 import System.IO
@@ -88,7 +82,7 @@ handle :: MonadIO m => MonadSTM m => Tracer m PerasLog -> NodeState m -> NodeReq
 handle tracer node@MkNodeState{..} =
   \case
     Initialize{..} -> do
-      node <- initialNodeState tracer party slotNumber parameters
+      node' <- initialNodeState tracer party slotNumber parameters
       atomically . modifyTVar' stateVar $
         \state ->
           state
@@ -98,7 +92,7 @@ handle tracer node@MkNodeState{..} =
             }
       pure
         ( def
-        , node
+        , node'
         )
     Tick ->
       pure (def, node{clock = clock + 1})
@@ -135,7 +129,7 @@ handle tracer node@MkNodeState{..} =
           Left e -> pure (Failed $ show e, node{clock = clock'})
     Stop -> pure (Stopped, node)
 
-data Command = Command
+newtype Command = Command
   { verbose :: Bool
   {-
     , simin :: FilePath

peras-simulation/peras-simulation.cabal

@@ -15,12 +15,6 @@ data-files:         *.json
 common warnings
     ghc-options: -O3
                  -Wall -Wunused-packages -Werror
-                 -fno-warn-missing-pattern-synonym-signatures
-                 -fno-warn-missing-signatures
-                 -fno-warn-name-shadowing
-                 -fno-warn-type-defaults
-                 -fno-warn-unused-imports
-                 -fno-warn-unused-matches
 
 library
     import:           warnings
@@ -94,10 +88,8 @@ executable  peras-simulation-pipe
                     , contra-tracer
                     , data-default
                     , io-classes
-                    , mtl
                     , optparse-applicative
                     , peras-simulation
-                    , text
 
 executable  peras-simulate
     import:           warnings
@@ -167,9 +159,6 @@ executable peras-conformance-test
                   , aeson
                   , base
                   , bytestring
-                  , data-default
                   , hspec
-                  , mtl
                   , peras-simulation
-                  , quickcheck-dynamic
     ghc-options: -rtsopts -threaded

peras-simulation/src/Peras/Block.hs

@@ -1,5 +1,11 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches #-}
 
 module Peras.Block where
 

peras-simulation/src/Peras/Chain.hs

@@ -1,4 +1,10 @@
 {-# LANGUAGE DeriveGeneric #-}
+{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches #-}
 
 module Peras.Chain where
 

peras-simulation/src/Peras/Conformance/Generators.hs

@@ -4,30 +4,17 @@
 
 module Peras.Conformance.Generators where
 
-import Control.Applicative (Applicative (pure, (<*>)), (<$>))
 import Control.Arrow (Arrow (first, second, (&&&), (***)))
-import Control.Monad (Functor (fmap), filterM, (=<<))
+import Control.Monad (filterM)
 import Data.Either (fromRight)
-import Data.Functor.Identity
+import Data.Functor.Identity (Identity (runIdentity))
 import Data.List (
-  all,
-  any,
-  concatMap,
-  dropWhile,
-  elem,
-  filter,
-  foldl,
-  maximum,
-  notElem,
   nub,
-  null,
   partition,
-  (++),
  )
-import Data.Maybe (Maybe (..), isNothing, mapMaybe, maybe)
+import Data.Maybe (isNothing, mapMaybe)
 import qualified Data.Set as Set (singleton)
 import GHC.Generics (Generic)
-import Numeric.Natural (Natural)
 import Peras.Arbitraries ()
 import Peras.Block (
   Block (MkBlock, certificate, creatorId, slotNumber),
@@ -44,24 +31,25 @@ import Peras.Conformance.Model (
   sutId,
   transition,
  )
-import Peras.Crypto
 import Peras.Crypto (Hash, Hashable (hash))
 import Peras.Numbering (
   RoundNumber (..),
   SlotNumber (..),
   slotInRound,
  )
-import Peras.Prototype.Crypto
+import Peras.Prototype.Crypto (
+  createMembershipProof,
+  createSignedVote,
+  mkParty,
+ )
 import Peras.Prototype.Types (PerasParams (..), hashTip, inRound)
 import Test.QuickCheck (
   Arbitrary (arbitrary),
   Gen,
   NonNegative (getNonNegative),
-  Positive (getPositive),
   choose,
   chooseInteger,
   elements,
-  frequency,
   sublistOf,
  )
 import Prelude hiding (round)
@@ -176,8 +164,6 @@ genNewChain :: GenConstraints -> NodeModel -> Gen Chain
 genNewChain gc@MkGenConstraints{blockCurrent} node@NodeModel{clock} =
   do
     prefChain <- genPrefChain gc node
-    cert1 <- genCertForBlock gc node prefChain
-    cert2 <- genCert gc node prefChain -- FIXME: Guard this with a setting.
     fmap (: prefChain) $
       MkBlock
         <$> (if blockCurrent then pure clock else genSlotNumber gc node)
@@ -188,7 +174,8 @@ genNewChain gc@MkGenConstraints{blockCurrent} node@NodeModel{clock} =
         <*> arbitrary
         <*> arbitrary
 
-genPrefChain gc@MkGenConstraints{blockWeightiest} node@NodeModel{protocol, allChains} =
+genPrefChain :: GenConstraints -> NodeModel -> Gen Chain
+genPrefChain MkGenConstraints{blockWeightiest} NodeModel{protocol, allChains} =
   let
     weigh :: Integer -> Block -> Integer
     weigh w MkBlock{certificate} = w + 1 + maybe 0 (const $ perasB protocol) certificate
@@ -205,7 +192,7 @@ genPrefChain gc@MkGenConstraints{blockWeightiest} node@NodeModel{protocol, allCh
       else sublistOf =<< elements allChains
 
 getCertPrimes :: NodeModel -> [Certificate]
-getCertPrimes NodeModel{clock, protocol, allSeenCerts} =
+getCertPrimes NodeModel{allSeenCerts} =
   let certRound = maximum $ round <$> allSeenCerts
    in filter ((== certRound) . round) allSeenCerts
 

peras-simulation/src/Peras/Conformance/Model.hs

@@ -2,20 +2,24 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE TypeOperators #-}
-{-# OPTIONS_GHC -Wno-name-shadowing -Wno-unused-matches #-}
+{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches #-}
 
 module Peras.Conformance.Model where
 
 import Control.Monad (guard)
-import Data.Maybe (mapMaybe)
 import Numeric.Natural (Natural)
 import Peras.Block (Block (MkBlock, certificate, creatorId, leadershipProof, parentBlock, signature, slotNumber), Certificate (MkCertificate, blockRef, round), PartyId, tipHash)
 import Peras.Chain (Chain, Vote (MkVote, blockHash, votingRound), insertCert)
 import Peras.Conformance.Params (PerasParams (MkPerasParams, perasA, perasB, perasK, perasL, perasR, perasU, perasτ), defaultPerasParams)
 import Peras.Crypto (Hash (MkHash), Hashable (hash), emptyBS)
 import Peras.Foreign (checkLeadershipProof, checkSignedBlock, checkSignedVote, createLeadershipProof, createMembershipProof, createSignedBlock, createSignedVote, mkParty)
 import Peras.Numbering (RoundNumber (getRoundNumber), SlotNumber (getSlotNumber), nextRound, nextSlot, slotInRound, slotToRound)
-import Peras.Util (comparing, maximumBy, maybeToList)
+import Peras.Util (comparing, decP, decS, eqDec, ge, gt, isYes, mapMaybe, maximumBy, maybeToList)
 
 import Control.Monad.Identity
 import Data.Function (on)
@@ -271,36 +275,20 @@ hasVoted :: PartyId -> RoundNumber -> NodeModel -> Bool
 hasVoted p r s =
   any (\v -> p == voterId v && r == votingRound v) (allVotes s)
 
-isYes :: Bool -> Bool
-isYes True = True
-isYes False = False
-
-decP :: Bool -> Bool -> Bool
-decP va vb = va && vb
-
-decS :: Bool -> Bool -> Bool
-decS va vb = va || vb
-
 (===) :: RoundNumber -> RoundNumber -> Bool
 x === y = x == y
 
-eq :: Integer -> Integer -> Bool
-eq = (==)
-
-gt :: Integer -> Integer -> Bool
-gt = gtInteger
-
-ge :: Integer -> Integer -> Bool
-ge = geInteger
-
 vr1A :: NodeModel -> Bool
-vr1A s = nextRound (round (cert' s)) === rFromSlot s
+vr1A s = rFromSlot s === nextRound (round (cert' s))
 
 vr1B' :: NodeModel -> Bool
 vr1B' s = extends (votingBlockHash s) (cert' s) (allChains s)
 
+extendsDec :: Hash Block -> Certificate -> [Chain] -> Bool
+extendsDec h c ch = extends h c ch
+
 vr1B :: NodeModel -> Bool
-vr1B s = vr1B' s
+vr1B s = extendsDec (votingBlockHash s) (cert' s) (allChains s)
 
 vr2A :: NodeModel -> Bool
 vr2A s =
@@ -315,9 +303,15 @@ vr2B s =
         (getRoundNumber (rFromSlot s))
         (getRoundNumber (round (certS s)))
     )
-    ( eq
-        (mod (getRoundNumber (rFromSlot s)) (perasK (protocol s)))
-        (mod (getRoundNumber (round (certS s))) (perasK (protocol s)))
+    ( eqDec
+        ( mod
+            (fromIntegral (getRoundNumber (rFromSlot s)))
+            (fromIntegral (perasK (protocol s)))
+        )
+        ( mod
+            (fromIntegral (getRoundNumber (round (certS s))))
+            (fromIntegral (perasK (protocol s)))
+        )
     )
 
 checkVotingRules :: NodeModel -> Bool

peras-simulation/src/Peras/Conformance/Params.hs

@@ -1,6 +1,12 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# OPTIONS_GHC -fno-warn-missing-pattern-synonym-signatures #-}
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+{-# OPTIONS_GHC -fno-warn-name-shadowing #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults #-}
+{-# OPTIONS_GHC -fno-warn-unused-imports #-}
+{-# OPTIONS_GHC -fno-warn-unused-matches #-}
 
 module Peras.Conformance.Params where