diff --git a/peras-simulation/app/Peras/Conformance/ExternalSpec.hs b/peras-simulation/app/Peras/Conformance/ExternalSpec.hs index 12adaabc1..34f971849 100644 --- a/peras-simulation/app/Peras/Conformance/ExternalSpec.hs +++ b/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) diff --git a/peras-simulation/app/Pipe.hs b/peras-simulation/app/Pipe.hs index d2998b813..717d18fda 100644 --- a/peras-simulation/app/Pipe.hs +++ b/peras-simulation/app/Pipe.hs @@ -5,10 +5,9 @@ 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 @@ -16,8 +15,6 @@ 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 diff --git a/peras-simulation/peras-simulation.cabal b/peras-simulation/peras-simulation.cabal index c9f583cdc..e30333809 100644 --- a/peras-simulation/peras-simulation.cabal +++ b/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 diff --git a/peras-simulation/src/Peras/Block.hs b/peras-simulation/src/Peras/Block.hs index 4ec4a6a03..b9fb09fce 100644 --- a/peras-simulation/src/Peras/Block.hs +++ b/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 diff --git a/peras-simulation/src/Peras/Chain.hs b/peras-simulation/src/Peras/Chain.hs index 409bf74ec..34e068c3c 100644 --- a/peras-simulation/src/Peras/Chain.hs +++ b/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 diff --git a/peras-simulation/src/Peras/Conformance/Generators.hs b/peras-simulation/src/Peras/Conformance/Generators.hs index 2388d108e..e13c1a818 100644 --- a/peras-simulation/src/Peras/Conformance/Generators.hs +++ b/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 diff --git a/peras-simulation/src/Peras/Conformance/Model.hs b/peras-simulation/src/Peras/Conformance/Model.hs index 0defe4c69..6cd273759 100644 --- a/peras-simulation/src/Peras/Conformance/Model.hs +++ b/peras-simulation/src/Peras/Conformance/Model.hs @@ -2,12 +2,16 @@ {-# 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) @@ -15,7 +19,7 @@ import Peras.Conformance.Params (PerasParams (MkPerasParams, perasA, perasB, per 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 diff --git a/peras-simulation/src/Peras/Conformance/Params.hs b/peras-simulation/src/Peras/Conformance/Params.hs index 8f17c8a68..6f1f702b8 100644 --- a/peras-simulation/src/Peras/Conformance/Params.hs +++ b/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 diff --git a/peras-simulation/src/Peras/Conformance/Test.hs b/peras-simulation/src/Peras/Conformance/Test.hs index 71ccf7808..4b292a66b 100644 --- a/peras-simulation/src/Peras/Conformance/Test.hs +++ b/peras-simulation/src/Peras/Conformance/Test.hs @@ -14,15 +14,35 @@ module Peras.Conformance.Test where import Control.Monad (when) -import Data.Bifunctor (second) import Data.Function (on) import Data.List (nubBy) -import Data.Maybe (Maybe (..), fromJust, fromMaybe, isJust) -import Data.Set (Set) +import Data.Maybe (isJust) import Peras.Arbitraries () -import Peras.Block (Block (..), Certificate (..), Party (pid), tipHash) +import Peras.Block (Block (..), Certificate (..), Party) import Peras.Chain (Chain, Vote (..)) -import Peras.Conformance.Generators +import Peras.Conformance.Generators ( + GenConstraints ( + MkGenConstraints, + selectionObeyAge, + selectionObeyChain, + twoParties, + useTestParams, + voteCurrent, + voteObeyVR1A, + voteObeyVR1B, + voteObeyVR2A, + voteObeyVR2B + ), + actionsSizeScaling, + genCommitteeMembership, + genHonestTick, + genProtocol, + genSlotLeadership, + genVote, + lenientGenConstraints, + rollbackNodeModel, + strictGenConstraints, + ) import Peras.Conformance.Model ( EnvAction (..), NodeModel (..), @@ -31,10 +51,8 @@ import Peras.Conformance.Model ( checkVotingRules, initialModelState, newQuora, - otherId, pref, sutId, - testParams, transition, votingBlockHash, ) @@ -49,17 +67,15 @@ import Peras.Numbering ( ) import Peras.Prototype.Crypto (mkParty) import Peras.Prototype.Trace qualified as Trace -import Peras.Prototype.Types (hashTip, inRound, newRound) +import Peras.Prototype.Types (inRound, newRound) import Test.QuickCheck ( Arbitrary (arbitrary), choose, elements, - frequency, - suchThat, tabulate, ) import Test.QuickCheck.DynamicLogic (DynLogicModel) -import Test.QuickCheck.Gen (elements, scale) +import Test.QuickCheck.Gen (scale) import Test.QuickCheck.StateModel ( Any (Some), HasVariables (..), @@ -210,7 +226,7 @@ instance StateModel NetworkModel where , initialized = useTestParams lenientGenConstraints } - arbitraryAction _ net@NetworkModel{nodeModel = s@NodeModel{clock, allChains, allVotes, protocol}, gen, initialized} = + arbitraryAction _ NetworkModel{nodeModel = s@NodeModel{clock, allChains, allVotes, protocol}, gen, initialized} = if initialized then do v <- @@ -235,7 +251,7 @@ instance StateModel NetworkModel where <$> genSlotLeadership 0.30 slotLimit <*> genCommitteeMembership 0.95 roundLimit where - equivocated MkVote{votingRound = r, creatorId = p} MkVote{votingRound = r', creatorId = p'} = r == r' && p == p' + equivocated MkVote{votingRound = r0, creatorId = p} MkVote{votingRound = r1, creatorId = p'} = r0 == r1 && p == p' cleanVotes = nubBy ( \a a' -> @@ -249,12 +265,12 @@ instance StateModel NetworkModel where _ -> True ) - badVoteCandidates = [(r, p) | MkVote r p _ _ _ <- allVotes, p /= sutId] + badVoteCandidates = [(r', p) | MkVote r' p _ _ _ <- allVotes, p /= sutId] canGenBadVote = canGenVotes && not (null badVoteCandidates) genBadVote = do block <- elements (concat allChains) - (r, p) <- elements badVoteCandidates - MkVote r p <$> arbitrary <*> pure (hash block) <*> arbitrary + (r', p) <- elements badVoteCandidates + MkVote r' p <$> arbitrary <*> pure (hash block) <*> arbitrary canGenVotes = not (all null allChains) -- There must be some block to vote for. && r > 0 -- No voting is allowed in the zeroth round. @@ -267,7 +283,7 @@ instance StateModel NetworkModel where shrinkAction _ _ Step{} = [Some (Step Tick)] precondition NetworkModel{initialized} Initial{} = not initialized - precondition NetworkModel{nodeModel = s, gen} (Step (NewChain [])) = False + precondition _ (Step (NewChain [])) = False precondition NetworkModel{nodeModel = s, gen} (Step (NewVote v)) = voteCurrent gen `implies` (slotToRound (protocol s) (clock s) == votingRound v) && Foreign.checkSignedVote v @@ -307,7 +323,7 @@ implies :: Bool -> Bool -> Bool implies x y = not x || y monitorChain :: Monad m => NetworkModel -> NetworkModel -> PostconditionM m () -monitorChain net@NetworkModel{nodeModel = s} net'@NetworkModel{nodeModel = s'@NodeModel{clock}} = +monitorChain net@NetworkModel{nodeModel = s} NetworkModel{nodeModel = s'@NodeModel{clock}} = do monitorPost $ tabulate "Slots (cumulative, rounded down)" [show $ (* 25) . (`div` 25) $ (fromIntegral clock :: Integer)] monitorPost $ tabulate "Slot leader" [show $ fst (sortition net) clock] @@ -315,7 +331,7 @@ monitorChain net@NetworkModel{nodeModel = s} net'@NetworkModel{nodeModel = s'@No monitorPost $ tabulate "Preferred chain lengthens" [show $ on (>) (length . pref) s' s] monitorCerts :: Monad m => NetworkModel -> NetworkModel -> PostconditionM m () -monitorCerts net@NetworkModel{nodeModel = s} net'@NetworkModel{nodeModel = s'@NodeModel{clock}} = +monitorCerts NetworkModel{nodeModel = s} NetworkModel{nodeModel = s'} = do monitorPost $ tabulate "Certs found or created during fetching" [show $ on (-) (length . allSeenCerts) s' s] monitorPost $ tabulate "New quora" [show $ length $ newQuora (fromIntegral (perasτ (protocol s))) (allSeenCerts s) (allVotes s')] diff --git a/peras-simulation/src/Peras/Conformance/Test/External.hs b/peras-simulation/src/Peras/Conformance/Test/External.hs index 7ef3a93b2..4ebec4756 100644 --- a/peras-simulation/src/Peras/Conformance/Test/External.hs +++ b/peras-simulation/src/Peras/Conformance/Test/External.hs @@ -13,8 +13,6 @@ module Peras.Conformance.Test.External where -import Control.Concurrent.Class.MonadSTM (MonadSTM (TVar)) -import Control.Concurrent.STM.TVar qualified as IO import Control.Monad (unless, void, when) import Control.Monad.IO.Class () import Control.Monad.State ( @@ -23,17 +21,13 @@ import Control.Monad.State ( StateT, modify, ) -import Control.Tracer (Tracer (Tracer), emit, nullTracer) import Data.Aeson (FromJSON, ToJSON) import Data.Aeson qualified as A import Data.ByteString.Char8 qualified as BS8 import Data.ByteString.Lazy qualified as LBS import Data.ByteString.Lazy.Char8 qualified as LBS8 import Data.Default (Default (def)) -import Data.IORef (modifyIORef, newIORef, readIORef) import Data.List (sort) -import Data.Maybe (fromJust) -import Data.Set (Set) import GHC.Generics (Generic) import Peras.Block (Certificate, Party) import Peras.Chain (Chain, Vote (..)) @@ -45,41 +39,29 @@ import Peras.Conformance.Model ( transition, ) import Peras.Conformance.Params (PerasParams) -import Peras.Conformance.Test +import Peras.Conformance.Test ( + Action (Initial, Step), + NetworkModel (NetworkModel, nodeModel), + sortition, + ) import Peras.Numbering (RoundNumber (getRoundNumber), SlotNumber) -import Peras.Prototype.BlockSelection (selectBlock) import Peras.Prototype.Crypto ( IsCommitteeMember, IsSlotLeader, - isCommitteeMember, - isSlotLeader, - mkCommitteeMember, mkParty, ) -import Peras.Prototype.Diffusion ( - Diffuser, - diffuseVote, - popChainsAndVotes, - ) -import Peras.Prototype.Fetching (fetching) -import Peras.Prototype.Trace qualified as Trace import Peras.Prototype.Types ( - PerasState, inRound, - initialPerasState, newRound, ) -import Peras.Prototype.Voting (voting) -import System.IO (Handle, IO) +import System.IO (Handle) import Test.QuickCheck ( Blind (Blind), Property, counterexample, ioProperty, noShrinking, - whenFail, ) -import Test.QuickCheck.DynamicLogic (DynLogicModel) import Test.QuickCheck.Extras (runPropertyStateT) import Test.QuickCheck.Monadic (monadicIO, monitor) import Test.QuickCheck.StateModel ( @@ -90,7 +72,7 @@ import Test.QuickCheck.StateModel ( monitorPost, runActions, ) -import Text.PrettyPrint (hang, vcat, (<+>)) +import Text.PrettyPrint (hang, (<+>)) import Text.PrettyPrint.HughesPJClass (Pretty (pPrint)) import Prelude hiding (round) @@ -162,7 +144,7 @@ callSUT RunState{hReader, hWriter} req = type Runtime = StateT RunState IO instance Realized IO ([Chain], [Vote]) ~ ([Chain], [Vote]) => RunModel NetworkModel Runtime where - perform net@NetworkModel{nodeModel = NodeModel{..}} a@(Initial params leaderSlots voterRounds) _ = + perform NetworkModel{nodeModel = NodeModel{..}} (Initial params leaderSlots voterRounds) _ = do rs <- get void . lift $ @@ -179,15 +161,15 @@ instance Realized IO ([Chain], [Vote]) ~ ([Chain], [Vote]) => RunModel NetworkMo perform net@NetworkModel{nodeModel = NodeModel{..}} (Step a) _ = case a of Peras.Conformance.Model.Tick -> do rs@RunState{..} <- get - modify $ \rs -> rs{unfetchedChains = mempty, unfetchedVotes = mempty} + modify $ \rs' -> rs'{unfetchedChains = mempty, unfetchedVotes = mempty} let clock' = clock + 1 - (isSlotLeader, isCommitteeMember) = sortition net - ( lift $ - callSUT + (isSlotLeader', isCommitteeMember') = sortition net + lift + ( callSUT rs NewSlot - { isSlotLeader = isSlotLeader clock' - , isCommitteeMember = isCommitteeMember $ inRound clock' protocol + { isSlotLeader = isSlotLeader' clock' + , isCommitteeMember = isCommitteeMember' $ inRound clock' protocol , newChains = unfetchedChains , newVotes = unfetchedVotes } @@ -206,12 +188,12 @@ instance Realized IO ([Chain], [Vote]) ~ ([Chain], [Vote]) => RunModel NetworkMo pure (mempty, mempty) postcondition _ Initial{} _ () = pure True - postcondition (net@NetworkModel{nodeModel = s}, net'@NetworkModel{nodeModel = s'}) (Step a) _ (cs, vs) = do + postcondition (net@NetworkModel{nodeModel = s}, NetworkModel{nodeModel = s'}) (Step a) _ (cs, vs) = do let (expectedChains, expectedVotes) = maybe (mempty, mempty) fst $ transition (sortition net) s a - let eqVotes vs vs' = + let eqVotes vs0 vs1 = let f MkVote{..} = (votingRound, creatorId, blockHash) - in sort (f <$> vs) == sort (f <$> vs') - eqChains cs cs' = cs == cs' + in sort (f <$> vs0) == sort (f <$> vs1) + eqChains cs0 cs1 = cs0 == cs1 let ok = eqChains cs expectedChains && eqVotes vs expectedVotes monitorPost . counterexample . show $ " action $" <+> pPrint a when (a == Peras.Conformance.Model.Tick && newRound (clock s') (protocol s')) $ diff --git a/peras-simulation/src/Peras/Conformance/Test/Prototype.hs b/peras-simulation/src/Peras/Conformance/Test/Prototype.hs index 860af7938..225a023e2 100644 --- a/peras-simulation/src/Peras/Conformance/Test/Prototype.hs +++ b/peras-simulation/src/Peras/Conformance/Test/Prototype.hs @@ -10,7 +10,7 @@ module Peras.Conformance.Test.Prototype where -import Control.Concurrent.Class.MonadSTM (MonadSTM (TVar), atomically, readTVarIO) +import Control.Concurrent.Class.MonadSTM (MonadSTM (TVar)) import Control.Concurrent.STM.TVar qualified as IO import Control.Monad (unless, when) import Control.Monad.State ( @@ -22,23 +22,21 @@ import Control.Monad.State ( import Control.Tracer (Tracer (Tracer), emit, nullTracer) import Data.Default (Default (def)) import Data.IORef (modifyIORef, newIORef, readIORef) -import Data.Maybe (fromJust, isJust) -import Data.Set (Set) -import Debug.Trace (traceShow) -import Peras.Block (Block (certificate)) import Peras.Chain (Chain, Vote) import Peras.Conformance.Model ( EnvAction (..), NodeModel (..), - checkVotingRules, - pref, transition, - vr1A, - vr1B, - vr2A, - vr2B, ) -import Peras.Conformance.Test +import Peras.Conformance.Test ( + Action (Initial, Step), + NetworkModel (NetworkModel, nodeModel), + modelSUT, + monitorCerts, + monitorChain, + monitorVoting, + sortition, + ) import Peras.Numbering (RoundNumber (getRoundNumber)) import Peras.Prototype.BlockCreation (blockCreation) import Peras.Prototype.BlockSelection (selectBlock) @@ -64,14 +62,11 @@ import Peras.Prototype.Voting (voting) import Test.QuickCheck ( Blind (Blind), Property, - classify, counterexample, ioProperty, noShrinking, - tabulate, whenFail, ) -import Test.QuickCheck.DynamicLogic (DynLogicModel) import Test.QuickCheck.Extras (runPropertyStateT) import Test.QuickCheck.Monadic (monadicIO, monitor) import Test.QuickCheck.StateModel ( @@ -135,13 +130,15 @@ instance (Realized m () ~ (), Realized m ([Chain], [Vote]) ~ ([Chain], [Vote]), when (a == Tick && newRound (clock s') (protocol s')) $ monitorPost . counterexample $ " -- round: " ++ show (getRoundNumber $ inRound (clock s') (protocol s')) - unless (null gotChains) $ do - monitorPost . counterexample . show $ " -- got chains:" <+> pPrint gotChains + unless (null gotChains) $ + monitorPost . counterexample . show $ + " -- got chains:" <+> pPrint gotChains when (gotChains /= expectedChains) $ counterexamplePost . show $ " -- expected chains:" <+> pPrint expectedChains - unless (null gotVotes) $ do - monitorPost . counterexample . show $ " -- got votes:" <+> pPrint gotVotes + unless (null gotVotes) $ + monitorPost . counterexample . show $ + " -- got votes:" <+> pPrint gotVotes when (gotVotes /= expectedVotes) $ counterexamplePost . show $ " -- expected votes:" <+> pPrint expectedVotes diff --git a/peras-simulation/src/Peras/Crypto.hs b/peras-simulation/src/Peras/Crypto.hs index 5d78e8935..3e0d7c25f 100644 --- a/peras-simulation/src/Peras/Crypto.hs +++ b/peras-simulation/src/Peras/Crypto.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.Crypto where diff --git a/peras-simulation/src/Peras/Foreign.hs b/peras-simulation/src/Peras/Foreign.hs index b86294685..7a39572a5 100644 --- a/peras-simulation/src/Peras/Foreign.hs +++ b/peras-simulation/src/Peras/Foreign.hs @@ -1,3 +1,10 @@ +{-# 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.Foreign where import Data.Functor.Identity (Identity (runIdentity)) diff --git a/peras-simulation/src/Peras/Numbering.hs b/peras-simulation/src/Peras/Numbering.hs index 6d01954fb..7510855e7 100644 --- a/peras-simulation/src/Peras/Numbering.hs +++ b/peras-simulation/src/Peras/Numbering.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.Numbering where diff --git a/peras-simulation/src/Peras/Prototype/BlockSelection.hs b/peras-simulation/src/Peras/Prototype/BlockSelection.hs index c4dc74b83..83b6af9ac 100644 --- a/peras-simulation/src/Peras/Prototype/BlockSelection.hs +++ b/peras-simulation/src/Peras/Prototype/BlockSelection.hs @@ -25,7 +25,7 @@ selectBlock tracer MkPerasParams{..} party stateVar round = do MkPerasState{chainPref} <- readTVarIO stateVar -- Let B be the youngest block at least L slots old on Cpref. - let oldEnough MkBlock{slotNumber, signature} = + let oldEnough MkBlock{slotNumber} = let r = fromIntegral round * perasU s = fromIntegral slotNumber + perasL in s <= r diff --git a/peras-simulation/src/Peras/Prototype/Diffusion.hs b/peras-simulation/src/Peras/Prototype/Diffusion.hs index 2c6909bd6..958f7a834 100644 --- a/peras-simulation/src/Peras/Prototype/Diffusion.hs +++ b/peras-simulation/src/Peras/Prototype/Diffusion.hs @@ -22,8 +22,6 @@ import Data.Foldable (toList) import Data.Function (on) import Data.Map (Map) import qualified Data.Map as Map (elems, insertWith, partitionWithKey, unionWith) -import Data.Set (Set) -import qualified Data.Set as Set (singleton, union, unions) import GHC.Generics (Generic) import Peras.Chain (Chain, Vote) import Peras.Numbering (SlotNumber) diff --git a/peras-simulation/src/Peras/Prototype/Fetching.hs b/peras-simulation/src/Peras/Prototype/Fetching.hs index 88fa6890a..1fd614d22 100644 --- a/peras-simulation/src/Peras/Prototype/Fetching.hs +++ b/peras-simulation/src/Peras/Prototype/Fetching.hs @@ -17,6 +17,7 @@ import Control.Tracer (Tracer, traceWith) import Data.Foldable (toList) import Data.Function (on) import Data.List (groupBy, maximumBy, nubBy, sortBy) +import Data.Map (Map) import Data.Map as Map (fromList, keys, keysSet, union) import Data.Maybe (mapMaybe) import Data.Set (Set) @@ -104,6 +105,7 @@ fetching tracer MkPerasParams{..} party stateVar slot newChains newVotes = , certStar = certStar' } +compareChains :: Integer -> Map Certificate SlotNumber -> Chain -> Chain -> Ordering compareChains perasB certs' a b = case (compare `on` chainWeight perasB (Map.keysSet certs')) a b of EQ -> diff --git a/peras-simulation/src/Peras/Prototype/Node.hs b/peras-simulation/src/Peras/Prototype/Node.hs index b86e0fb52..22cfd5a90 100644 --- a/peras-simulation/src/Peras/Prototype/Node.hs +++ b/peras-simulation/src/Peras/Prototype/Node.hs @@ -5,12 +5,10 @@ module Peras.Prototype.Node where import Control.Concurrent.Class.MonadSTM (MonadSTM (..)) -import Control.Monad (when) import Control.Monad.Except (ExceptT (ExceptT), runExceptT) import Control.Monad.State (StateT, gets, lift, modify') import Control.Tracer (Tracer, nullTracer, traceWith) import Data.Default (def) -import Data.Set (Set) import Peras.Block (Party) import Peras.Chain (Chain, Vote) import Peras.Numbering (RoundNumber, SlotNumber) @@ -27,7 +25,6 @@ import Peras.Prototype.Types ( PerasState, inRound, initialPerasState, - newRound, systemStart, ) import Peras.Prototype.Voting (voting) @@ -81,7 +78,7 @@ tickNode :: [Chain] -> [Vote] -> m (PerasResult ()) -tickNode tracer diffuser params party state s r payload newChains newVotes = +tickNode tracer diffuser params party state s _ payload newChains newVotes = -- 1. Get votes and chains from the network. runExceptT $ do -- 2. Invoke fetching. diff --git a/peras-simulation/src/Peras/Prototype/Node/Model.hs b/peras-simulation/src/Peras/Prototype/Node/Model.hs index 5ed0684f7..6af65142a 100644 --- a/peras-simulation/src/Peras/Prototype/Node/Model.hs +++ b/peras-simulation/src/Peras/Prototype/Node/Model.hs @@ -36,8 +36,6 @@ import Data.Default (Default (..)) import Data.Foldable (toList) import Data.List ((\\)) import qualified Data.Map as Map -import Data.Set (Set) -import qualified Data.Set as Set import Peras.Arbitraries () import Peras.Block ( Block (MkBlock, creatorId, slotNumber), diff --git a/peras-simulation/src/Peras/Prototype/Trace.hs b/peras-simulation/src/Peras/Prototype/Trace.hs index c21ddf76b..b4869058f 100644 --- a/peras-simulation/src/Peras/Prototype/Trace.hs +++ b/peras-simulation/src/Peras/Prototype/Trace.hs @@ -7,7 +7,6 @@ module Peras.Prototype.Trace where import Control.Tracer (Tracer (..), contramap, debugTracer) import Data.Aeson (FromJSON, ToJSON) import qualified Data.Aeson as A -import Data.Set (Set) import qualified Data.Text.Lazy as LT import qualified Data.Text.Lazy.Encoding as LE import GHC.Generics (Generic) diff --git a/peras-simulation/src/Peras/Prototype/Types.hs b/peras-simulation/src/Peras/Prototype/Types.hs index 1e02a0674..3191e25cd 100644 --- a/peras-simulation/src/Peras/Prototype/Types.hs +++ b/peras-simulation/src/Peras/Prototype/Types.hs @@ -1,6 +1,4 @@ {-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE OverloadedStrings #-} -{-# LANGUAGE RecordWildCards #-} module Peras.Prototype.Types ( module Peras.Prototype.Types, @@ -9,7 +7,6 @@ module Peras.Prototype.Types ( import Control.Concurrent.Class.MonadSTM (TVar) import Data.Aeson (FromJSON, ToJSON) -import qualified Data.ByteString as BS import Data.Default (Default (..)) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map (singleton) diff --git a/peras-simulation/src/Peras/Prototype/Voting.hs b/peras-simulation/src/Peras/Prototype/Voting.hs index ae21ab89c..4c48293f3 100644 --- a/peras-simulation/src/Peras/Prototype/Voting.hs +++ b/peras-simulation/src/Peras/Prototype/Voting.hs @@ -17,7 +17,7 @@ import qualified Data.Set as Set (insert, singleton) import Peras.Block (Block (..), Certificate (..), Party (pid)) import Peras.Chain (Chain) import Peras.Crypto (Hashable (..)) -import Peras.Numbering (RoundNumber, SlotNumber) +import Peras.Numbering (SlotNumber) import Peras.Orphans () import Peras.Prototype.Crypto (createMembershipProof, createSignedVote, isCommitteeMember) import Peras.Prototype.Trace (PerasLog (..)) diff --git a/peras-simulation/src/Peras/Util.hs b/peras-simulation/src/Peras/Util.hs index 07ba4ea14..7998c902a 100644 --- a/peras-simulation/src/Peras/Util.hs +++ b/peras-simulation/src/Peras/Util.hs @@ -1,3 +1,10 @@ +{-# 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.Util where import Numeric.Natural (Natural) diff --git a/peras-simulation/test/Peras/ChainSpec.hs b/peras-simulation/test/Peras/ChainSpec.hs index 577f1ec30..eb4f6a925 100644 --- a/peras-simulation/test/Peras/ChainSpec.hs +++ b/peras-simulation/test/Peras/ChainSpec.hs @@ -6,13 +6,13 @@ module Peras.ChainSpec where import Data.Data (Proxy (..)) import Peras.Arbitraries () import Peras.Block (Block (..), PartyId, Tx) -import Peras.Chain (Chain, commonPrefix, prefix) +import Peras.Chain (Chain, commonPrefix) import Peras.Crypto (Hash (..), LeadershipProof, MembershipProof) import Peras.Numbering (SlotNumber) import Peras.Orphans () -import Test.Hspec (Spec, describe, it, shouldBe) +import Test.Hspec (Spec, describe) import Test.Hspec.QuickCheck (prop) -import Test.QuickCheck (Arbitrary (..), Property, forAll, forAllShrink, (===), (==>)) +import Test.QuickCheck (Arbitrary (..), Property, forAllShrink, (===), (==>)) import Test.QuickCheck.Classes (lawsCheck, showReadLaws) import Test.QuickCheck.Property (once) @@ -33,6 +33,7 @@ spec = do once $ commonPrefix sampleChains === [block2] +sampleChains :: [Chain] sampleChains = [ chain1 , chain2 @@ -46,10 +47,16 @@ sampleChains = , chain1 ] +block1 :: Block block1 = MkBlock{slotNumber = 49, creatorId = 1, parentBlock = MkHash{hashBytes = ""}, certificate = Nothing, leadershipProof = "f2a6ab5f8122", bodyHash = MkHash{hashBytes = "12345678"}, signature = "06f34b7da9fd"} + +block2 :: Block block2 = MkBlock{slotNumber = 44, creatorId = 2, parentBlock = MkHash{hashBytes = ""}, certificate = Nothing, leadershipProof = "0faf57e3c126", bodyHash = MkHash{hashBytes = "12345678"}, signature = "c63cff5266ee"} +chain1 :: Chain chain1 = [block1, block2] + +chain2 :: Chain chain2 = [block2] propCommonPrefixSelf :: Property diff --git a/peras-simulation/test/Peras/Conformance/TestSpec.hs b/peras-simulation/test/Peras/Conformance/TestSpec.hs index 23e1124fd..19d0160ce 100644 --- a/peras-simulation/test/Peras/Conformance/TestSpec.hs +++ b/peras-simulation/test/Peras/Conformance/TestSpec.hs @@ -1,18 +1,10 @@ module Peras.Conformance.TestSpec where -import Control.Monad (replicateM_, (>>)) -import Control.Monad.State (evalStateT) -import Data.Default (def) -import Data.Functor (void) import Peras.Conformance.Generators (actionsSizeScaling) import Peras.Conformance.Test.Prototype (prop_node) import Test.Hspec (Spec, describe) -import Test.Hspec.QuickCheck (modifyMaxSuccess, prop) -import Test.QuickCheck (Blind (Blind), Gen, Property, Testable, arbitrary, expectFailure, forAll, property, resize, scale) -import Test.QuickCheck.DynamicLogic (DL, anyAction, 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 the prototype against the Agda executable specification. spec :: Spec diff --git a/peras-simulation/test/Peras/OrphansSpec.hs b/peras-simulation/test/Peras/OrphansSpec.hs index 6f9cef9b1..d62a4deff 100644 --- a/peras-simulation/test/Peras/OrphansSpec.hs +++ b/peras-simulation/test/Peras/OrphansSpec.hs @@ -4,7 +4,6 @@ module Peras.OrphansSpec where import Paths_peras_simulation (getDataDir) import Peras.Arbitraries () -import Peras.Block (Block) import Peras.Chain (Chain) import Peras.Event (Event) import Peras.Orphans () diff --git a/peras-simulation/test/Peras/Prototype/BlockCreationSpec.hs b/peras-simulation/test/Peras/Prototype/BlockCreationSpec.hs index 77aff2497..a804ac1a5 100644 --- a/peras-simulation/test/Peras/Prototype/BlockCreationSpec.hs +++ b/peras-simulation/test/Peras/Prototype/BlockCreationSpec.hs @@ -16,8 +16,6 @@ import Peras.Prototype.Types (PerasParams (..), PerasState (..), initialPerasSta import Test.Hspec (Spec, it, shouldReturn) import Test.QuickCheck (arbitrary) -import qualified Data.Set as Set (size) - spec :: Spec spec = do let params = def diff --git a/peras-simulation/test/Peras/Prototype/Node/ModelSpec.hs b/peras-simulation/test/Peras/Prototype/Node/ModelSpec.hs index ef6a2d47f..e11692b24 100644 --- a/peras-simulation/test/Peras/Prototype/Node/ModelSpec.hs +++ b/peras-simulation/test/Peras/Prototype/Node/ModelSpec.hs @@ -5,7 +5,7 @@ import Data.Default (def) import Data.Functor (void) import Peras.Prototype.Node.Model (NodeModel, RunMonad (runMonad)) import Test.Hspec (Spec, describe) -import Test.Hspec.QuickCheck (modifyMaxSuccess, prop) +import Test.Hspec.QuickCheck (prop) import Test.QuickCheck (Gen, Property, Testable, property) import Test.QuickCheck.DynamicLogic (DL, anyActions_, forAllDL) import Test.QuickCheck.Gen.Unsafe (Capture (..), capture) diff --git a/src/Peras/Block.lagda.md b/src/Peras/Block.lagda.md index 68d40885b..a62ad0546 100644 --- a/src/Peras/Block.lagda.md +++ b/src/Peras/Block.lagda.md @@ -14,6 +14,12 @@ open import Peras.Util {-# FOREIGN AGDA2HS {-# 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 #-} import GHC.Generics (Generic) import Peras.Crypto (Hash (..), Hashable (..)) import Prelude hiding (round) diff --git a/src/Peras/Chain.lagda.md b/src/Peras/Chain.lagda.md index d2eca7d90..3dfd54b0b 100644 --- a/src/Peras/Chain.lagda.md +++ b/src/Peras/Chain.lagda.md @@ -18,6 +18,12 @@ open import Peras.Util {-# FOREIGN AGDA2HS {-# 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 #-} import GHC.Generics (Generic) #-} diff --git a/src/Peras/Conformance/Model.agda b/src/Peras/Conformance/Model.agda index 005d001f0..ca38ed8a3 100644 --- a/src/Peras/Conformance/Model.agda +++ b/src/Peras/Conformance/Model.agda @@ -27,7 +27,12 @@ import Protocol.Peras {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE NamedFieldPuns #-} {-# 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 #-} import Prelude hiding (round) import Control.Monad.Identity diff --git a/src/Peras/Conformance/Params.agda b/src/Peras/Conformance/Params.agda index 1f15344f8..a31ba4ed3 100644 --- a/src/Peras/Conformance/Params.agda +++ b/src/Peras/Conformance/Params.agda @@ -7,6 +7,12 @@ open import Data.Nat {-# 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 #-} #-} {-# FOREIGN AGDA2HS diff --git a/src/Peras/Crypto.agda b/src/Peras/Crypto.agda index 35c6a3507..2f9722d29 100644 --- a/src/Peras/Crypto.agda +++ b/src/Peras/Crypto.agda @@ -25,6 +25,12 @@ postulate {-# FOREIGN AGDA2HS {-# 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 #-} import Data.ByteString as BS import Data.Word (Word8) import GHC.Generics (Generic) diff --git a/src/Peras/Foreign.agda b/src/Peras/Foreign.agda index c81c3719f..496c497c8 100644 --- a/src/Peras/Foreign.agda +++ b/src/Peras/Foreign.agda @@ -9,6 +9,12 @@ open import Peras.Numbering {-# FOREIGN AGDA2HS + {-# 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 #-} import Data.Functor.Identity ( Identity(runIdentity) ) import Peras.Block ( Block, Certificate, Party, PartyId, Payload ) import Peras.Chain ( Vote, VotingWeight ) diff --git a/src/Peras/Numbering.lagda.md b/src/Peras/Numbering.lagda.md index b8a573328..36fe83550 100644 --- a/src/Peras/Numbering.lagda.md +++ b/src/Peras/Numbering.lagda.md @@ -18,6 +18,12 @@ open import Peras.Util {-# FOREIGN AGDA2HS {-# 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 #-} import GHC.Generics (Generic) #-} diff --git a/src/Peras/Util.agda b/src/Peras/Util.agda index 22946240e..ea5020765 100644 --- a/src/Peras/Util.agda +++ b/src/Peras/Util.agda @@ -11,6 +11,12 @@ import Data.Bool open import Data.Nat using (ℕ; NonZero; _≤_; _<_; _≥_; _>_; z≤n; s≤s; z