From c6381e95b1d4f95d05595854cb13487008d249a6 Mon Sep 17 00:00:00 2001 From: Brian W Bush Date: Mon, 19 Feb 2024 13:26:08 -0700 Subject: [PATCH 1/2] Added Peras-compatible vote type. --- peras-iosim/src/Peras/IOSim/GraphViz.hs | 14 +++--- peras-iosim/src/Peras/IOSim/Message/Types.hs | 32 ++++++------- peras-iosim/src/Peras/IOSim/Network.hs | 47 +++++++++---------- peras-iosim/src/Peras/IOSim/Network/Types.hs | 19 ++++---- peras-iosim/src/Peras/IOSim/Node.hs | 25 +++++----- peras-iosim/src/Peras/IOSim/Node/Types.hs | 10 ++-- peras-iosim/src/Peras/IOSim/Protocol.hs | 35 +++++++++----- peras-iosim/src/Peras/IOSim/Protocol/Types.hs | 15 ++++-- peras-iosim/src/Peras/IOSim/Simulate.hs | 10 ++-- peras-iosim/src/Peras/IOSim/Types.hs | 41 ++++++++++++++++ peras-quickcheck/src/Peras/NetworkModel.hs | 9 ++-- peras-quickcheck/src/Peras/NodeModel.hs | 13 ++--- .../test/Peras/NetworkModelSpec.hs | 7 +-- 13 files changed, 167 insertions(+), 110 deletions(-) diff --git a/peras-iosim/src/Peras/IOSim/GraphViz.hs b/peras-iosim/src/Peras/IOSim/GraphViz.hs index 12f63de0..61128033 100644 --- a/peras-iosim/src/Peras/IOSim/GraphViz.hs +++ b/peras-iosim/src/Peras/IOSim/GraphViz.hs @@ -7,7 +7,7 @@ module Peras.IOSim.GraphViz ( ) where import Control.Lens ((^.)) -import Data.List (nub) +import Data.List (intercalate, nub) import Peras.Block (Block (..)) import Peras.Chain (Chain (..)) import Peras.IOSim.Network.Types (NetworkState, chainsSeen, currentStates) @@ -25,7 +25,7 @@ writeGraph :: writeGraph = (. G.renderDot) . writeFile peersGraph :: - NetworkState v -> + NetworkState -> G.Graph peersGraph networkState = let nodeStates = networkState ^. currentStates @@ -55,9 +55,7 @@ peersGraph networkState = [G.AssignmentStatement (G.NameId "rankdir") (G.StringId "LR")] <> nodes <> edges chainGraph :: - Eq v => - Show v => - NetworkState v -> + NetworkState -> G.Graph chainGraph networkState = let chains = S.toList (networkState ^. chainsSeen) @@ -68,7 +66,7 @@ chainGraph networkState = [ G.AttributeSetValue (G.NameId "shape") (G.StringId "oval") , G.AttributeSetValue (G.NameId "label") (G.StringId "genesis") ] - nodeId bid = G.NodeId (G.StringId $ show bid) Nothing + nodeId bid = G.NodeId (G.StringId . init . tail $ show bid) Nothing -- FIXME: The Agda types don't handle block hashes yet, so we use the signature as a placehodler for now. mkNode Block{..} = G.NodeStatement @@ -76,14 +74,14 @@ chainGraph networkState = [ G.AttributeSetValue (G.NameId "shape") (G.StringId "record") , G.AttributeSetValue (G.NameId "label") . G.XmlId . G.XmlText $ "" - <> show signature + <> (init . tail . show) signature <> "" <> "|slot=" <> show slotNumber <> "|creator=" <> show creatorId <> "|votes=" - <> show includedVotes + <> intercalate "," (show <$> S.toList includedVotes) ] blocks Genesis = [] blocks (Cons b p) = b : blocks p diff --git a/peras-iosim/src/Peras/IOSim/Message/Types.hs b/peras-iosim/src/Peras/IOSim/Message/Types.hs index 8a0283ee..4f1b8cef 100644 --- a/peras-iosim/src/Peras/IOSim/Message/Types.hs +++ b/peras-iosim/src/Peras/IOSim/Message/Types.hs @@ -14,22 +14,22 @@ import Control.Monad.Class.MonadTime (UTCTime) import GHC.Generics (Generic) import Peras.Block (Block) import Peras.IOSim.Node.Types (NodeState) -import Peras.IOSim.Types (ByteSize) +import Peras.IOSim.Types (ByteSize, Votes) import Peras.Message (Message, NodeId) import Peras.Orphans () import qualified Data.Aeson as A import qualified Data.Aeson.Types as A -data InEnvelope v +data InEnvelope = InEnvelope { origin :: Maybe NodeId - , inMessage :: Message v + , inMessage :: Message Votes } | Stop deriving stock (Eq, Generic, Ord, Read, Show) -instance (A.FromJSON v, Eq v) => A.FromJSON (InEnvelope v) where +instance A.FromJSON InEnvelope where parseJSON = A.withObject "InEnvelope" $ \o -> @@ -46,7 +46,7 @@ instance (A.FromJSON v, Eq v) => A.FromJSON (InEnvelope v) where else A.parseFail $ "Illegal action: " <> action in parseInEnvelope <|> parseStop -instance (A.ToJSON v, Eq v) => A.ToJSON (InEnvelope v) where +instance A.ToJSON InEnvelope where toJSON InEnvelope{..} = A.object [ "origin" A..= origin @@ -58,12 +58,12 @@ instance (A.ToJSON v, Eq v) => A.ToJSON (InEnvelope v) where ] -- TODO: Refactor (or eliminate) when the Agda and QuickCheck code stabilizes. -data OutMessage v - = FetchBlock (Block v) - | SendMessage (Message v) +data OutMessage + = FetchBlock (Block Votes) + | SendMessage (Message Votes) deriving stock (Eq, Generic, Ord, Read, Show) -instance (A.FromJSON v, Eq v) => A.FromJSON (OutMessage v) where +instance A.FromJSON OutMessage where parseJSON = A.withObject "OutMessage" $ \o -> @@ -74,7 +74,7 @@ instance (A.FromJSON v, Eq v) => A.FromJSON (OutMessage v) where "SendMessage" -> SendMessage <$> o A..: "message" _ -> A.parseFail $ "Illegal output: " <> output -instance (A.ToJSON v, Eq v) => A.ToJSON (OutMessage v) where +instance A.ToJSON OutMessage where toJSON (FetchBlock block) = A.object [ "output" A..= ("FetchBlock" :: String) @@ -86,27 +86,27 @@ instance (A.ToJSON v, Eq v) => A.ToJSON (OutMessage v) where , "message" A..= message ] -data OutEnvelope v +data OutEnvelope = OutEnvelope { timestamp :: UTCTime , source :: NodeId - , outMessage :: OutMessage v + , outMessage :: OutMessage , bytes :: ByteSize , destination :: NodeId } | Idle { timestamp :: UTCTime , source :: NodeId - , currentState :: NodeState v + , currentState :: NodeState } | Exit { timestamp :: UTCTime , source :: NodeId - , nodeState :: NodeState v + , nodeState :: NodeState } deriving stock (Eq, Generic, Ord, Read, Show) -instance (A.FromJSON v, Eq v) => A.FromJSON (OutEnvelope v) where +instance A.FromJSON OutEnvelope where parseJSON = A.withObject "OutEnvelope" $ \o -> @@ -121,7 +121,7 @@ instance (A.FromJSON v, Eq v) => A.FromJSON (OutEnvelope v) where parseExit = Exit <$> o A..: "timestamp" <*> o A..: "source" <*> o A..: "nodeState" in parseMessage <|> parseIdle <|> parseExit -instance (A.ToJSON v, Eq v) => A.ToJSON (OutEnvelope v) where +instance A.ToJSON OutEnvelope where toJSON OutEnvelope{..} = A.object [ "timestamp" A..= timestamp diff --git a/peras-iosim/src/Peras/IOSim/Network.hs b/peras-iosim/src/Peras/IOSim/Network.hs index 92e284bf..5e998a82 100644 --- a/peras-iosim/src/Peras/IOSim/Network.hs +++ b/peras-iosim/src/Peras/IOSim/Network.hs @@ -25,7 +25,6 @@ import Control.Monad.Class.MonadTime (MonadTime) import Control.Monad.Class.MonadTimer (MonadDelay (..)) import Control.Monad.Random (MonadRandom, getRandomR) import Control.Monad.State (StateT, execStateT, lift) -import Data.Default (Default) import Data.Foldable (foldrM) import Data.List (delete) import Data.Maybe (fromMaybe) @@ -84,7 +83,7 @@ connectNode upstream downstream = Topology . M.insertWith (<>) upstream (S.singl createNetwork :: MonadSTM m => Topology -> - m (Network v m) + m (Network m) createNetwork Topology{connections} = do nodesIn <- mapM (const newTQueueIO) connections @@ -95,9 +94,7 @@ createNetwork Topology{connections} = -- one like a tree barrier. -- TODO: Rewrite as a state machine. runNetwork :: - forall m v. - Default v => - Ord v => + forall m. MonadDelay m => MonadFork m => MonadSay m => @@ -105,11 +102,11 @@ runNetwork :: MonadTime m => Parameters -> Protocol -> - M.Map NodeId (NodeState v) -> - Network v m -> + M.Map NodeId NodeState -> + Network m -> Slot -> - NetworkState v -> - m (NetworkState v) + NetworkState -> + m NetworkState runNetwork parameters protocol states network@Network{..} endSlot initialState = flip execStateT (initialState & currentStates .~ states) $ do @@ -117,7 +114,7 @@ runNetwork parameters protocol states network@Network{..} endSlot initialState = -- Notify a node to stop. notifyStop destination nodeIn = output destination nodeIn Stop -- Receive and send messages. - loop :: MonadDelay m => MonadSay m => StateT (NetworkState v) m () + loop :: MonadDelay m => MonadSay m => StateT NetworkState m () loop = do stepToIdle parameters network @@ -134,12 +131,12 @@ runNetwork parameters protocol states network@Network{..} endSlot initialState = loop startNodes :: - (Monad m, Eq v, MonadSTM m, MonadSay m, Ord v, MonadDelay m, Default v, MonadFork m, MonadTime m) => + (Monad m, MonadSTM m, MonadSay m, MonadDelay m, MonadFork m, MonadTime m) => Parameters -> Protocol -> - M.Map NodeId (NodeState v) -> - Network v m -> - StateT (NetworkState v) m () + M.Map NodeId NodeState -> + Network m -> + StateT NetworkState m () startNodes parameters protocol states network = mapM_ forkNode $ M.toList nodesIn where @@ -156,10 +153,10 @@ startNodes parameters protocol states network = -- Wait for all nodes to exit. waitForExits :: - (Monad m, Eq v, MonadSTM m, MonadSay m, Ord v, MonadDelay m) => + (Monad m, MonadSTM m, MonadSay m, MonadDelay m) => Parameters -> - Network v m -> - StateT (NetworkState v) m () + Network m -> + StateT NetworkState m () waitForExits parameters network = do allIdle <- activeNodes `uses` null @@ -180,10 +177,10 @@ flush q = -- | Advance the network up to one single slot. -- This function loops until all nodes are idle stepToIdle :: - (Monad m, Eq v, MonadSTM m, MonadSay m, Ord v, MonadDelay m) => + (Monad m, MonadSTM m, MonadSay m, MonadDelay m) => Parameters -> - Network v m -> - StateT (NetworkState v) m () + Network m -> + StateT NetworkState m () stepToIdle parameters network = do -- Advance the slot counter and notify the nodes, if all nodes are idle. allIdle <- activeNodes `uses` null @@ -212,11 +209,11 @@ stepToIdle parameters network = do -- | Dispatch a single message through the network. routeEnvelope :: - (Monad m, Eq v, MonadSTM m, MonadSay m, Ord v) => + (Monad m, MonadSTM m, MonadSay m) => Parameters -> - Network v m -> - OutEnvelope v -> - StateT (NetworkState v) m () + Network m -> + OutEnvelope -> + StateT NetworkState m () routeEnvelope parameters Network{nodesIn} = \case out@OutEnvelope{..} -> do @@ -250,7 +247,7 @@ routeEnvelope parameters Network{nodesIn} = \case currentStates %= M.insert source nodeState -- Send a message and mark the destination as active. -output :: MonadSTM m => NodeId -> TQueue m p -> p -> StateT (NetworkState v) m () +output :: MonadSTM m => NodeId -> TQueue m p -> p -> StateT NetworkState m () output destination inChannel inEnvelope = do lift . atomically . writeTQueue inChannel $ inEnvelope diff --git a/peras-iosim/src/Peras/IOSim/Network/Types.hs b/peras-iosim/src/Peras/IOSim/Network/Types.hs index d6c3a9d3..c1098049 100644 --- a/peras-iosim/src/Peras/IOSim/Network/Types.hs +++ b/peras-iosim/src/Peras/IOSim/Network/Types.hs @@ -26,6 +26,7 @@ import Peras.Block (Slot) import Peras.Chain (Chain) import Peras.IOSim.Message.Types (InEnvelope, OutEnvelope) import Peras.IOSim.Node.Types (NodeState) +import Peras.IOSim.Types (Votes) import Peras.Message (NodeId) import Peras.Orphans () import System.Random (StdGen, mkStdGen) @@ -43,27 +44,27 @@ instance FromJSON Topology where instance ToJSON Topology where toJSON Topology{..} = A.object ["connections" A..= connections] -data Network v m = Network - { nodesIn :: M.Map NodeId (TQueue m (InEnvelope v)) - , nodesOut :: TQueue m (OutEnvelope v) +data Network m = Network + { nodesIn :: M.Map NodeId (TQueue m InEnvelope) + , nodesOut :: TQueue m OutEnvelope } deriving stock (Generic) -data NetworkState v = NetworkState +data NetworkState = NetworkState { _lastSlot :: Slot , _lastTime :: UTCTime , _activeNodes :: S.Set NodeId - , _chainsSeen :: S.Set (Chain v) - , _currentStates :: M.Map NodeId (NodeState v) - , _pending :: [OutEnvelope v] + , _chainsSeen :: S.Set (Chain Votes) + , _currentStates :: M.Map NodeId NodeState + , _pending :: [OutEnvelope] , _networkRandom :: StdGen -- FIXME: Is it okay not to serialize this? } deriving stock (Eq, Generic, Show) -instance Ord v => Default (NetworkState v) where +instance Default NetworkState where def = NetworkState 0 (read "1970-01-01 00:00:00.0 UTC") mempty mempty M.empty mempty $ mkStdGen 12345 -instance (ToJSON v, Eq v) => ToJSON (NetworkState v) where +instance ToJSON NetworkState where toJSON NetworkState{..} = A.object [ "lastSlot" A..= _lastSlot diff --git a/peras-iosim/src/Peras/IOSim/Node.hs b/peras-iosim/src/Peras/IOSim/Node.hs index 555427ea..7fad9fe3 100644 --- a/peras-iosim/src/Peras/IOSim/Node.hs +++ b/peras-iosim/src/Peras/IOSim/Node.hs @@ -47,9 +47,9 @@ import qualified Data.ByteString as BS import qualified Data.Map.Strict as M import qualified Data.Set as S -data NodeProcess v m = NodeProcess - { incoming :: TQueue m (InEnvelope v) - , outgoing :: TQueue m (OutEnvelope v) +data NodeProcess m = NodeProcess + { incoming :: TQueue m InEnvelope + , outgoing :: TQueue m OutEnvelope } deriving stock (Generic) @@ -58,7 +58,7 @@ initializeNodes :: Parameters -> UTCTime -> Topology -> - m (M.Map NodeId (NodeState v)) + m (M.Map NodeId NodeState) initializeNodes parameters now Topology{connections} = sequence $ initializeNode parameters now `M.mapWithKey` connections @@ -68,7 +68,7 @@ initializeNode :: UTCTime -> NodeId -> S.Set NodeId -> - m (NodeState v) + m NodeState initializeNode Parameters{maximumStake} clock' nodeId' downstreams' = NodeState nodeId' <$> (MkPartyId . VerificationKey . BS.pack <$> replicateM 6 getRandom) @@ -83,18 +83,17 @@ initializeNode Parameters{maximumStake} clock' nodeId' downstreams' = <*> pure False runNode :: - forall v m. - Default v => + forall m. MonadDelay m => MonadSTM m => MonadTime m => Protocol -> Coin -> - NodeState v -> - NodeProcess v m -> + NodeState -> + NodeProcess m -> m () runNode protocol total state NodeProcess{..} = - let go :: Default v => MonadDelay m => MonadSTM m => MonadTime m => RandomGen g => g -> StateT (NodeState v) m () + let go :: MonadDelay m => MonadSTM m => MonadTime m => RandomGen g => g -> StateT NodeState m () go gen = do let atomically' = lift . atomically @@ -106,7 +105,7 @@ runNode protocol total state NodeProcess{..} = >>= \case InEnvelope{..} -> do - (message, gen') <- + (messages, gen') <- case inMessage of NextSlot slot -> do @@ -117,9 +116,7 @@ runNode protocol total state NodeProcess{..} = currentState <- get atomically' $ do - case message of - Nothing -> pure () - Just message' -> mapM_ (writeTQueue outgoing . OutEnvelope now nodeId' (SendMessage message') 0) downstreams' + mapM_ (\message' -> mapM_ (writeTQueue outgoing . OutEnvelope now nodeId' (SendMessage message') 0) downstreams') messages writeTQueue outgoing $ Idle now nodeId' currentState clock .= now go gen' diff --git a/peras-iosim/src/Peras/IOSim/Node/Types.hs b/peras-iosim/src/Peras/IOSim/Node/Types.hs index 92b40430..a22cb887 100644 --- a/peras-iosim/src/Peras/IOSim/Node/Types.hs +++ b/peras-iosim/src/Peras/IOSim/Node/Types.hs @@ -24,14 +24,14 @@ import Control.Monad.Class.MonadTime (UTCTime) import GHC.Generics (Generic) import Peras.Block (PartyId, Slot) import Peras.Chain (Chain) -import Peras.IOSim.Types (Coin) +import Peras.IOSim.Types (Coin, Votes) import Peras.Message (NodeId) import Peras.Orphans () import qualified Data.Aeson as A import qualified Data.Set as S -data NodeState v = NodeState +data NodeState = NodeState { _nodeId :: NodeId , _owner :: PartyId , _initialSeed :: Int @@ -39,14 +39,14 @@ data NodeState v = NodeState , _slot :: Slot , _stake :: Coin , _vrfOutput :: Double - , _preferredChain :: Chain v + , _preferredChain :: Chain Votes , _downstreams :: S.Set NodeId , _slotLeader :: Bool , _committeeMember :: Bool } deriving stock (Eq, Generic, Ord, Read, Show) -instance (A.FromJSON v, Eq v) => A.FromJSON (NodeState v) where +instance A.FromJSON NodeState where parseJSON = A.withObject "NodeState" $ \o -> @@ -64,7 +64,7 @@ instance (A.FromJSON v, Eq v) => A.FromJSON (NodeState v) where _committeeMember <- o A..: "committeeMember" pure NodeState{..} -instance (A.ToJSON v, Eq v) => A.ToJSON (NodeState v) where +instance A.ToJSON NodeState where toJSON NodeState{..} = A.object [ "nodeId" A..= _nodeId diff --git a/peras-iosim/src/Peras/IOSim/Protocol.hs b/peras-iosim/src/Peras/IOSim/Protocol.hs index 7d152cc7..ac5e24fe 100644 --- a/peras-iosim/src/Peras/IOSim/Protocol.hs +++ b/peras-iosim/src/Peras/IOSim/Protocol.hs @@ -17,19 +17,18 @@ import Peras.Chain (Chain (..)) import Peras.Crypto (Hash (Hash), LeadershipProof (LeadershipProof), Signature (Signature)) import Peras.IOSim.Node.Types (NodeState, owner, preferredChain, slot, slotLeader, stake) import Peras.IOSim.Protocol.Types (Protocol (..)) -import Peras.IOSim.Types (Coin) +import Peras.IOSim.Types (Coin, Votes) import Peras.Message (Message (NewChain)) import qualified Data.ByteString as BS nextSlot :: - Default v => MonadRandom m => - MonadState (NodeState v) m => + MonadState NodeState m => Protocol -> Slot -> Coin -> - m (Maybe (Message v)) + m [Message Votes] nextSlot PseudoPraos{..} slotNumber total = do leader <- isSlotLeader activeSlotCoefficient total =<< use stake @@ -45,18 +44,18 @@ nextSlot PseudoPraos{..} slotNumber total = signature <- Signature . BS.pack <$> replicateM 6 getRandom chain <- preferredChain `uses` Cons (Block slotNumber creatorId parentBlock includedVotes leadershipProof payload signature) preferredChain .= chain - pure . Just $ NewChain chain - else pure Nothing + pure [NewChain chain] + else pure mempty nextSlot PseudoPeras{} _ _ = error "Pseudo-Peras protocol is not yet implemented." nextSlot OuroborosPraos{} _ _ = error "Ouroboros-Praos protocol is not yet implemented." nextSlot OuroborosGenesis{} _ _ = error "Ouroboros-Genesis protocol is not yet implemented." nextSlot OuroborosPeras{} _ _ = error "Ouroboros-Peras protocol is not yet implemented." newChain :: - MonadState (NodeState v) m => + MonadState NodeState m => Protocol -> - Chain v -> - m (Maybe (Message v)) + Chain Votes -> + m [Message Votes] newChain PseudoPraos{} chain = do let chainLength Genesis = (0 :: Int) @@ -65,8 +64,8 @@ newChain PseudoPraos{} chain = if on (>) chainLength chain preferred then do preferredChain .= chain - pure . Just $ NewChain chain - else pure Nothing + pure [NewChain chain] + else pure mempty newChain PseudoPeras{} _ = error "Pseudo-Peras protocol is not yet implemented." newChain OuroborosPraos{} _ = error "Ouroboros-Praos protocol is not yet implemented." newChain OuroborosGenesis{} _ = error "Ouroboros-Genesis protocol is not yet implemented." @@ -81,3 +80,17 @@ isSlotLeader :: isSlotLeader activeSlotCoefficient' total staked = let p = 1 - (1 - activeSlotCoefficient') ** (fromIntegral staked / fromIntegral total) in (<= p) <$> getRandomR (0, 1) + +isCommitteeMember :: + MonadRandom m => + Protocol -> + Coin -> + Coin -> + m Bool +isCommitteeMember PseudoPraos{} _ _ = pure False +isCommitteeMember PseudoPeras{..} total staked = + let p = 1 - (1 - pCommitteeLottery) ** (fromIntegral staked / fromIntegral total) + in (<= p) <$> getRandomR (0, 1) +isCommitteeMember OuroborosPraos{} _ _ = error "Ouroboros-Praos protocol is not yet implemented." +isCommitteeMember OuroborosGenesis{} _ _ = error "Ouroboros-Genesis protocol is not yet implemented." +isCommitteeMember OuroborosPeras{} _ _ = error "Ouroboros-Peras protocol is not yet implemented." diff --git a/peras-iosim/src/Peras/IOSim/Protocol/Types.hs b/peras-iosim/src/Peras/IOSim/Protocol/Types.hs index 340dbc8a..ebd4b600 100644 --- a/peras-iosim/src/Peras/IOSim/Protocol/Types.hs +++ b/peras-iosim/src/Peras/IOSim/Protocol/Types.hs @@ -21,10 +21,13 @@ data Protocol { activeSlotCoefficient :: Double -- ^ Low-fidelity version of Ouroboros Peras. , roundDuration :: Int - , meanCommitteeSize :: Int + , pCommitteeLottery :: Double , votingBoost :: Double , votingWindow :: (Int, Int) , votingQuorum :: Int + , voteMaximumAge :: Int + , cooldownDuration :: Int + , prefixCutoffWeight :: Double } | OuroborosPraos | -- | High-fidelity version of Ouroboros Praos. @@ -47,11 +50,14 @@ instance A.FromJSON Protocol where "PseudoPeras" -> PseudoPeras <$> o A..: "activeSlotCoefficient" - <*> o A..: "meanCommitteeSize" + <*> o A..: "pCommitteeLottery" <*> o A..: "roundDuration" <*> o A..: "votingBoost" <*> o A..: "votingWindow" <*> o A..: "votingQuorum" + <*> o A..: "voteMaximumAge" + <*> o A..: "cooldownDuration" + <*> o A..: "prefixCutoffWeight" "OuroborosPraos" -> pure OuroborosPraos "OuroborosGenesis" -> @@ -70,10 +76,13 @@ instance A.ToJSON Protocol where A.object [ "protocol" A..= ("PseudoPeras" :: String) , "activeSlotCoefficient" A..= activeSlotCoefficient - , "meanCommitteeSize" A..= meanCommitteeSize + , "pCommitteeLottery" A..= pCommitteeLottery , "roundDuration" A..= roundDuration , "votingBoost" A..= votingBoost , "votingWindow" A..= votingWindow + , "voteMaximumAge" A..= voteMaximumAge + , "cooldownDuration" A..= cooldownDuration + , "prefixCutoffWeight" A..= prefixCutoffWeight ] toJSON OuroborosPraos = A.object diff --git a/peras-iosim/src/Peras/IOSim/Simulate.hs b/peras-iosim/src/Peras/IOSim/Simulate.hs index 32935f1c..98941b8d 100644 --- a/peras-iosim/src/Peras/IOSim/Simulate.hs +++ b/peras-iosim/src/Peras/IOSim/Simulate.hs @@ -26,7 +26,7 @@ import qualified Data.ByteString.Lazy.Char8 as LBS8 simulation :: Parameters -> Protocol -> - IOSim s (NetworkState ()) + IOSim s NetworkState simulation parameters@Parameters{..} protocol = do let (gen, gen') = split $ mkStdGen randomSeed @@ -46,22 +46,20 @@ simulate :: Parameters -> Protocol -> Bool -> - (Either Failure (NetworkState ()), Maybe (SimTrace (NetworkState ()))) + (Either Failure NetworkState, Maybe (SimTrace NetworkState)) simulate parameters protocol False = (runSim $ simulation parameters protocol, Nothing) simulate parameters protocol True = let trace = runSimTrace $ simulation parameters protocol in (traceResult False trace, Just trace) writeTrace :: - Show v => FilePath -> - SimTrace (NetworkState v) -> + SimTrace NetworkState -> IO () writeTrace filename = writeFile filename . ppTrace writeReport :: - (A.ToJSON v, Eq v) => FilePath -> - NetworkState v -> + NetworkState -> IO () writeReport filename = LBS8.writeFile filename . A.encode diff --git a/peras-iosim/src/Peras/IOSim/Types.hs b/peras-iosim/src/Peras/IOSim/Types.hs index 93fd1971..348f98a0 100644 --- a/peras-iosim/src/Peras/IOSim/Types.hs +++ b/peras-iosim/src/Peras/IOSim/Types.hs @@ -1,11 +1,52 @@ +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DerivingVia #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RecordWildCards #-} + module Peras.IOSim.Types ( ByteSize, Coin, Round, + Vote, + Votes, ) where +import GHC.Generics (Generic) +import Peras.Block (Block, PartyId) +import Peras.Orphans () + +import qualified Data.Aeson as A +import qualified Data.Set as S + type Coin = Int type Round = Word type ByteSize = Word + +type Votes = S.Set Vote + +data Vote = Vote + { votingRound :: Round + , voter :: PartyId + , block :: Block Votes + } + deriving stock (Eq, Generic, Ord, Read, Show) + +instance A.FromJSON Vote where + parseJSON = + A.withObject "Vote" $ + \o -> + do + votingRound <- o A..: "round" + voter <- o A..: "voter" + block <- o A..: "block" + pure Vote{..} + +instance A.ToJSON Vote where + toJSON Vote{..} = + A.object + [ "round" A..= votingRound + , "voter" A..= voter + , "block" A..= block + ] diff --git a/peras-quickcheck/src/Peras/NetworkModel.hs b/peras-quickcheck/src/Peras/NetworkModel.hs index 135c46d6..7a776266 100644 --- a/peras-quickcheck/src/Peras/NetworkModel.hs +++ b/peras-quickcheck/src/Peras/NetworkModel.hs @@ -26,6 +26,7 @@ import GHC.Generics (Generic) import Numeric.Natural (Natural) import Peras.Block (Block, Slot) import Peras.Chain (Chain (..), asList, commonPrefix) +import Peras.IOSim.Types (Votes) import Peras.Message (Message (..), NodeId (..)) import Peras.Orphans () import Test.QuickCheck (Gen, choose, elements, frequency, tabulate) @@ -65,9 +66,9 @@ instance StateModel Network where -- Advance the time one or more slots possibly producing blocks. Tick :: Natural -> Action Network () -- Observe a node's best chain - ObserveBestChain :: NodeId -> Action Network (Chain ()) + ObserveBestChain :: NodeId -> Action Network (Chain Votes) -- Ensure chains have a common prefix - ChainsHaveCommonPrefix :: [Var (Chain ())] -> Action Network () + ChainsHaveCommonPrefix :: [Var (Chain Votes)] -> Action Network () arbitraryAction _ Network{nodeIds} = frequency @@ -107,7 +108,7 @@ instance HasVariables (Action Network a) where data Simulator m = Simulator { step :: m () -- ^ Step the network one slot - , preferredChain :: NodeId -> m (Chain ()) + , preferredChain :: NodeId -> m (Chain Votes) -- ^ Return preferred chain for a specific node in the network. , stop :: m () -- ^ Stop all nodes in the network @@ -135,7 +136,7 @@ instance Monad m => RunModel Network (RunMonad m) where performTick = ask >>= lift . step - currentChain :: NodeId -> RunMonad m (Chain ()) + currentChain :: NodeId -> RunMonad m (Chain Votes) currentChain nodeId = ask >>= lift . flip preferredChain nodeId diff --git a/peras-quickcheck/src/Peras/NodeModel.hs b/peras-quickcheck/src/Peras/NodeModel.hs index 1bf03b76..f0920bd6 100644 --- a/peras-quickcheck/src/Peras/NodeModel.hs +++ b/peras-quickcheck/src/Peras/NodeModel.hs @@ -36,6 +36,7 @@ import Peras.IOSim.Node (NodeProcess (..), initializeNode, runNode) import Peras.IOSim.Node.Types (stake) import Peras.IOSim.Protocol.Types (Protocol (..)) import Peras.IOSim.Simulate.Types (Parameters (..)) +import Peras.IOSim.Types (Votes) import Peras.Message (Message (..), NodeId (..)) import System.Random (mkStdGen) import Test.QuickCheck (choose, tabulate) @@ -45,7 +46,7 @@ import Test.QuickCheck.StateModel.Variables (HasVariables (..)) -- | A simple model of time passing and forged blocks data NodeModel = NodeModel - { forgedBlocks :: [Var [Block ()]] + { forgedBlocks :: [Var [Block Votes]] -- ^ List of forged blocks references as observed from the node's behaviour , slot :: Slot } @@ -56,8 +57,8 @@ instance DynLogicModel NodeModel instance StateModel NodeModel where data Action NodeModel a where -- Advance the time one or more slots possibly producing blocks. - Tick :: Natural -> Action NodeModel [Block ()] - ForgedBlocksRespectSchedule :: [Var [Block ()]] -> Action NodeModel Rational + Tick :: Natural -> Action NodeModel [Block Votes] + ForgedBlocksRespectSchedule :: [Var [Block Votes]] -> Action NodeModel Rational arbitraryAction _ NodeModel{} = Some . Tick . fromInteger <$> choose (500, 2000) @@ -92,7 +93,7 @@ instance HasVariables (Action NodeModel a) where data Node m = Node { nodeId :: NodeId , nodeThreadId :: ThreadId m - , nodeProcess :: NodeProcess () m + , nodeProcess :: NodeProcess m , nodeStake :: Rational } @@ -102,7 +103,7 @@ initialiseNodeEnv :: , MonadTime m , MonadFork m ) => - m (ThreadId m, NodeProcess () m, Rational) + m (ThreadId m, NodeProcess m, Rational) initialiseNodeEnv = do let gen = mkStdGen 42 now <- getCurrentTime @@ -144,7 +145,7 @@ instance forall m. MonadSTM m => RunModel NodeModel (RunMonad m) where mconcat <$> forM [1 .. n] tick ForgedBlocksRespectSchedule{} -> asks nodeStake where - tick :: Slot -> RunMonad m [Block ()] + tick :: Slot -> RunMonad m [Block Votes] tick k = do Node{nodeProcess = NodeProcess{incoming, outgoing}} <- ask -- tick the node diff --git a/peras-quickcheck/test/Peras/NetworkModelSpec.hs b/peras-quickcheck/test/Peras/NetworkModelSpec.hs index 0c04facf..66f85d1c 100644 --- a/peras-quickcheck/test/Peras/NetworkModelSpec.hs +++ b/peras-quickcheck/test/Peras/NetworkModelSpec.hs @@ -24,6 +24,7 @@ import Peras.IOSim.Node (initializeNodes) import qualified Peras.IOSim.Node.Types as Node import Peras.IOSim.Protocol.Types (Protocol (PseudoPraos)) import Peras.IOSim.Simulate.Types (Parameters (..)) +import Peras.IOSim.Types (Votes) import Peras.Message (NodeId) import Peras.NetworkModel (Action (..), Network (..), RunMonad, Simulator (..), runMonad) import Test.Hspec (Spec) @@ -82,7 +83,7 @@ runPropInIOSim p = do now <- getCurrentTime let (states, gen'') = runRand (initializeNodes parameters now topology) gen' network <- createNetwork topology - let initState :: NetworkState () = def & networkRandom .~ gen'' & currentStates .~ states + let initState :: NetworkState = def & networkRandom .~ gen'' & currentStates .~ states networkState <- newTVarIO initState runWithState networkState $ startNodes parameters protocol states network pure $ @@ -92,12 +93,12 @@ runPropInIOSim p = do , stop = pure () } -getPreferredChain :: Monad m => NodeId -> StateT (NetworkState ()) m (Chain ()) +getPreferredChain :: Monad m => NodeId -> StateT NetworkState m (Chain Votes) getPreferredChain nodeId = do nodeState <- currentStates `uses` (Map.! nodeId) pure $ nodeState ^. Node.preferredChain -runWithState :: (Monad m, MonadSTM m) => TVar m (NetworkState ()) -> StateT (NetworkState ()) m a -> m a +runWithState :: (Monad m, MonadSTM m) => TVar m NetworkState -> StateT NetworkState m a -> m a runWithState stateVar act = do st <- readTVarIO stateVar (res, st') <- runStateT act st From 13c8c65db7ad6ee534fdace897e7300a5e7ad918 Mon Sep 17 00:00:00 2001 From: Brian W Bush Date: Mon, 19 Feb 2024 14:23:48 -0700 Subject: [PATCH 2/2] Updated logbook. --- Logbook.md | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Logbook.md b/Logbook.md index 3c4971f1..aa412b50 100644 --- a/Logbook.md +++ b/Logbook.md @@ -1,5 +1,13 @@ ## 2024-02-19 +### BB - Voting + +Updated `peras-iosim` to track voting. + +### BB - Nix CI and Development Environment + +Fixed Nix CI and development environment to handle literate Agda and an Agda dependency on `agda2hs`. + ### AB fixing Common Prefix Trying to fix error in `NetworkModelSpec`, I first struggle with shrinking problems as I end up with traces without any `Tick` which is problematic as this means there won't be anything but a `Genesis` chain in all nodes.