Merge pull request #32 from input-output-hk/bwbush/peras-iosim

Vote tracking in `peras-iosim`

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.

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,22 +66,22 @@ 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
           (nodeId signature)
           [ G.AttributeSetValue (G.NameId "shape") (G.StringId "record")
           , G.AttributeSetValue (G.NameId "label") . G.XmlId . G.XmlText $
               "<b>"
-                <> show signature
+                <> (init . tail . show) signature
                 <> "</b>"
                 <> "|slot="
                 <> show slotNumber
                 <> "|creator="
                 <> show creatorId
                 <> "|votes="
-                <> show includedVotes
+                <> intercalate "," (show <$> S.toList includedVotes)
           ]
       blocks Genesis = []
       blocks (Cons b p) = b : blocks p

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

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,29 +94,27 @@ 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 =>
   MonadSTM m =>
   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
       let
         -- 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

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