Add messages handling to quicheck model

quickcheck-model/src/Peras/Block.hs

@@ -0,0 +1,25 @@
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+
+module Peras.Block where
+
+import Data.ByteString as BS
+import Numeric.Natural (Natural)
+
+newtype PartyId = PartyId {unPartyId :: ByteString}
+  deriving (Eq, Show, Ord)
+
+newtype BlockId = BlockId {unBlockId :: ByteString}
+  deriving (Eq, Show, Ord)
+
+newtype Slot = Slot Natural
+  deriving (Eq, Show, Num, Ord)
+
+data Block t = Block
+  { blockId :: BlockId
+  , slotNumber :: Slot
+  , creatorId :: PartyId
+  , parentBlock :: BlockId
+  , includedVotes :: t
+  , payload :: ByteString
+  }
+  deriving (Eq, Show, Ord)

quickcheck-model/src/Peras/Chain.hs

@@ -0,0 +1,7 @@
+module Peras.Chain where
+
+import Peras.Block (Block)
+
+data Chain t = Genesis
+             | Cons (Block t) (Chain t)
+

quickcheck-model/src/Peras/Crypto.hs

@@ -0,0 +1,15 @@
+module Peras.Crypto where
+
+import Data.ByteString as BS
+
+newtype Hash = Hash{hash :: ByteString}
+
+newtype MembershipProof = MembershipProof{proofM :: ByteString}
+
+newtype LeadershipProof = LeadershipProof{proof :: ByteString}
+
+newtype Signature = Signature{signature :: ByteString}
+
+newtype VerificationKey = VerificationKey{verificationKey ::
+                                          ByteString}
+

quickcheck-model/src/Peras/Message.hs

@@ -0,0 +1,24 @@
+{-# LANGUAGE LambdaCase #-}
+
+module Peras.Message where
+
+import Data.ByteString (ByteString)
+import Data.Maybe (mapMaybe)
+import Peras.Block (Block, BlockId, Slot)
+
+newtype NodeId = NodeId {nodeId :: ByteString}
+  deriving (Eq, Show, Ord)
+
+data Message votes
+  = NextSlot Slot
+  | RollForward (Block votes)
+  | RollBack BlockId
+  deriving (Eq, Show)
+
+selectBlocks :: [Message ()] -> [Block ()]
+selectBlocks = mapMaybe isRollForward
+
+isRollForward :: Message () -> Maybe (Block ())
+isRollForward = \case
+  RollForward block -> Just block
+  _other -> Nothing

quickcheck-model/src/Peras/Model.hs

@@ -4,7 +4,6 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
-{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -14,36 +13,30 @@
 module Peras.Model where
 
 import Control.Monad (replicateM)
-import Control.Monad.Reader (MonadReader, MonadTrans (..), ReaderT, asks)
-import Data.ByteString (ByteString, unfoldr)
+import Control.Monad.State (MonadState, StateT, gets, modify)
+import Control.Monad.Trans (MonadTrans (..))
+import Data.ByteString (unfoldr)
+import Data.Either (partitionEithers)
 import qualified Data.List as List
 import qualified Data.Map as Map
-import Data.Maybe (mapMaybe)
 import Data.Set (Set)
 import qualified Data.Set as Set
 import GHC.Generics (Generic)
 import Numeric.Natural (Natural)
+import Peras.Block (Block, Slot)
+import Peras.Message (Message (..), NodeId (..), selectBlocks)
 import System.Random (Random (random), RandomGen, mkStdGen, split)
 import Test.QuickCheck (choose, elements, frequency)
 import Test.QuickCheck.StateModel (Any (..), HasVariables, Realized, RunModel (..), StateModel (..))
 import Test.QuickCheck.StateModel.Variables (HasVariables (..))
 
-newtype Slot = Slot {unSlot :: Natural}
-  deriving newtype (Eq, Show, Num)
-
 -- | We model a network of nodes interconnected through a diffusion layer.
 data Network = Network
   { nodeIds :: [NodeId]
   , slot :: Slot
   }
   deriving (Show, Generic)
 
-newtype BlockId = BlockId {unBlockId :: ByteString}
-  deriving (Eq, Show, Ord, Generic)
-
-newtype NodeId = NodeId {unNodeId :: ByteString}
-  deriving (Eq, Show, Ord, Generic)
-
 baseNodes :: (RandomGen g) => g -> [NodeId]
 baseNodes g =
   take 10 $ NodeId <$> List.unfoldr (Just . genNodeId) g
@@ -52,22 +45,15 @@ baseNodes g =
     let (g1, g2) = split seed
      in (unfoldr (Just . random) g1, g2)
 
-data Block = Block
-  { blockId :: BlockId
-  , producer :: NodeId
-  , previousBlock :: BlockId
-  }
-  deriving (Eq, Show, Ord, Generic)
-
 data Chain
   = Genesis
-  | Chain Block Chain
+  | Chain (Block ()) Chain
   deriving (Eq, Show, Generic)
 
 instance StateModel Network where
   data Action Network a where
     -- Advance the time one or more slots possibly producing blocks.
-    Tick :: Natural -> Action Network (Set Block)
+    Tick :: Natural -> Action Network (Set (Block ()))
     -- Observe a node's best chain
     ObserveBestChain :: NodeId -> Action Network Chain
 
@@ -99,28 +85,15 @@ instance HasVariables Network where
 instance HasVariables (Action Network a) where
   getAllVariables = const mempty
 
--- | Messages sent to the node.
-data Input
-  = -- | New slot occurs (represents the passage of time)
-    NextSlot Slot
-  | -- | Some `NodeId` has sent a requested `Block` to this node.
-    SomeBlock NodeId Block
-  | -- | Some `NodeId` is notifying us their best chain has changed.
-    UpdatedChain NodeId Chain
-
-data Output
-  = -- | Node needs some block from given `NodeId`.
-    FetchBlock NodeId Block
-  | -- | Node changed its best chain
-    NewChain Chain
-
 -- | Basic interface to a `Node` instance.
 data Node m = Node
   { nodeId :: NodeId
-  , step :: Input -> m [Output]
+  , deliver :: Message () -> m ()
+  , step :: m [Message ()]
   -- ^ Nodes are assumed to progress in steps
-  , inbox :: [(Slot, Input)]
+  , inbox :: [(Slot, Message ())]
   -- ^ New inputs to be delivered to the node at some `Slot`
+  , bestChain :: m Chain
   }
 
 -- | All known nodes in the network.
@@ -129,8 +102,8 @@ data Nodes m = Nodes
   { nodes :: Map.Map NodeId (Node m)
   }
 
-newtype RunMonad m a = RunMonad {runMonad :: ReaderT (Nodes m) m a}
-  deriving newtype (Functor, Applicative, Monad, MonadReader (Nodes m))
+newtype RunMonad m a = RunMonad {runMonad :: StateT (Nodes m) m a}
+  deriving newtype (Functor, Applicative, Monad, MonadState (Nodes m))
 
 instance MonadTrans RunMonad where
   lift = RunMonad . lift
@@ -145,18 +118,28 @@ instance (Monad m) => RunModel Network (RunMonad m) where
       ObserveBestChain nodeId ->
         currentChain nodeId
    where
-    performTick :: RunMonad m [Block]
+    performTick :: RunMonad m [Block ()]
     performTick = do
-      nodes <- asks $ Map.elems . nodes
-      selectBlocks . mconcat <$> lift (traverse tick nodes)
-
-    tick Node{step} = step (NextSlot slot)
-
-    currentChain _nodeId = undefined
-
-selectBlocks :: [Output] -> [Block]
-selectBlocks = Data.Maybe.mapMaybe isBlockForged
-
-isBlockForged :: Output -> Maybe Block
-isBlockForged = \case
-  NewChain{} -> Nothing
+      allNodes <- gets (Map.elems . nodes)
+      selectBlocks . mconcat <$> traverse tick allNodes
+
+    tick :: Node m -> RunMonad m [Message ()]
+    tick node@Node{nodeId, step, deliver, inbox} = do
+      let (pending, deliverables) = partitionEithers $ map (deliverableAt slot) inbox
+      -- deliver all messages in inbox
+      mapM_ (lift . deliver) deliverables
+      -- update the node's state
+      modify $ Nodes . Map.insert nodeId (node{inbox = pending}) . nodes
+      -- then let the node advance one slot and return the messages it sends
+      lift step
+
+    currentChain :: NodeId -> RunMonad m Chain
+    currentChain nodeId =
+      gets (Map.lookup nodeId . nodes)
+        >>= maybe (error $ "Invalid node id:" <> show nodeId) (lift . bestChain)
+
+deliverableAt :: Slot -> (Slot, a) -> Either (Slot, a) a
+deliverableAt at m@(delay, msg) =
+  if at >= delay
+    then Right msg
+    else Left m