Fixed chain diffusion in external test harness.

peras-simulation/app/Pipe.hs

@@ -21,11 +21,12 @@ import qualified Data.Text.Lazy.Encoding as T
 import Data.Version (showVersion)
 import qualified Options.Applicative as O
 import Paths_peras_simulation (version)
+import Peras.Block (Party (pid))
 import Peras.Conformance.Params (PerasParams (perasΔ))
 import Peras.Conformance.Test.External (NodeRequest (..), NodeResponse (..))
 import Peras.Prototype.BlockCreation (blockCreation)
 import Peras.Prototype.BlockSelection (selectBlock)
-import Peras.Prototype.Crypto (mkCommitteeMember, mkSlotLeader)
+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.Fetching (fetching)
@@ -40,6 +41,7 @@ import Peras.Prototype.Trace (PerasLog (Protocol), perasTracer)
 import Peras.Prototype.Types (
   PerasState (certs, chains, votes),
   inRound,
+  newRound,
  )
 import Peras.Prototype.Visualizer (makeVisTracer)
 import Peras.Prototype.Voting (voting)
@@ -121,8 +123,13 @@ handle tracer node@MkNodeState{..} =
           Left e -> pure (Failed $ show e, node)
     NewSlot{..} -> do
       let clock' = clock + 1
+          party =
+            mkParty
+              (pid self)
+              (if isSlotLeader then pure clock' else mempty)
+              (if isCommitteeMember && newRound clock' protocol then pure $ inRound clock' protocol else mempty)
       void $ popChainsAndVotes diffuserVar (clock' + fromIntegral (perasΔ protocol) + 1)
-      tickNode tracer diffuserVar protocol self stateVar clock' (inRound clock' protocol) mempty newChains newVotes
+      tickNode tracer diffuserVar protocol party stateVar clock' (inRound clock' protocol) mempty newChains newVotes
         >>= \case
           Right () -> (,node{clock = clock'}) . uncurry NodeResponse <$> popChainsAndVotes diffuserVar (clock' + fromIntegral (perasΔ protocol) + 1)
           Left e -> pure (Failed $ show e, node{clock = clock'})

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

@@ -7,14 +7,15 @@
 module Peras.Conformance.Model where
 
 import Control.Monad (guard)
+import Data.Maybe (mapMaybe)
 import Numeric.Natural (Natural)
 import Peras.Block (Block (MkBlock, certificate, creatorId, leadershipProof, parentBlock, signature, slotNumber), Certificate (MkCertificate, blockRef, round), PartyId, tipHash)
 import Peras.Chain (Chain, Vote (MkVote, blockHash, votingRound), insertCert)
 import Peras.Conformance.Params (PerasParams (MkPerasParams, perasA, perasB, perasK, perasL, perasR, perasU, perasτ), defaultPerasParams)
 import Peras.Crypto (Hash (MkHash), Hashable (hash), emptyBS)
 import Peras.Foreign (checkLeadershipProof, checkSignedBlock, checkSignedVote, createLeadershipProof, createMembershipProof, createSignedBlock, createSignedVote, mkParty)
 import Peras.Numbering (RoundNumber (getRoundNumber), SlotNumber (getSlotNumber), nextRound, nextSlot, slotInRound, slotToRound)
-import Peras.Util (comparing, decP, decS, eqDec, ge, gt, isYes, mapMaybe, maximumBy, maybeToList)
+import Peras.Util (comparing, maximumBy, maybeToList)
 
 import Control.Monad.Identity
 import Data.Function (on)
@@ -270,20 +271,36 @@ 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 = rFromSlot s === nextRound (round (cert' s))
+vr1A s = nextRound (round (cert' s)) === rFromSlot 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 = extendsDec (votingBlockHash s) (cert' s) (allChains s)
+vr1B s = vr1B' s
 
 vr2A :: NodeModel -> Bool
 vr2A s =
@@ -298,15 +315,9 @@ vr2B s =
         (getRoundNumber (rFromSlot s))
         (getRoundNumber (round (certS s)))
     )
-    ( eqDec
-        ( mod
-            (fromIntegral (getRoundNumber (rFromSlot s)))
-            (fromIntegral (perasK (protocol s)))
-        )
-        ( mod
-            (fromIntegral (getRoundNumber (round (certS s))))
-            (fromIntegral (perasK (protocol s)))
-        )
+    ( eq
+        (mod (getRoundNumber (rFromSlot s)) (perasK (protocol s)))
+        (mod (getRoundNumber (round (certS s))) (perasK (protocol s)))
     )
 
 checkVotingRules :: NodeModel -> Bool

peras-simulation/src/Peras/Conformance/Test/External.hs

@@ -34,7 +34,6 @@ import Data.IORef (modifyIORef, newIORef, readIORef)
 import Data.List (sort)
 import Data.Maybe (fromJust)
 import Data.Set (Set)
-import Debug.Trace (traceShow)
 import GHC.Generics (Generic)
 import Peras.Block (Certificate, Party)
 import Peras.Chain (Chain, Vote (..))
@@ -182,19 +181,19 @@ instance Realized IO ([Chain], [Vote]) ~ ([Chain], [Vote]) => RunModel NetworkMo
       rs@RunState{..} <- get
       modify $ \rs -> rs{unfetchedChains = mempty, unfetchedVotes = mempty}
       let clock' = clock + 1
-          sut = modelSUT net
+          (isSlotLeader, isCommitteeMember) = sortition net
       ( lift $
           callSUT
             rs
             NewSlot
-              { isSlotLeader = Peras.Prototype.Crypto.isSlotLeader sut clock'
-              , isCommitteeMember = Peras.Prototype.Crypto.isCommitteeMember sut (inRound clock' protocol)
+              { isSlotLeader = isSlotLeader clock'
+              , isCommitteeMember = isCommitteeMember $ inRound clock' protocol
               , newChains = unfetchedChains
               , newVotes = unfetchedVotes
               }
         )
         >>= \case
-          NodeResponse{..} -> pure ([], diffuseVotes)
+          NodeResponse{..} -> pure (diffuseChains, diffuseVotes)
           _ -> pure (mempty, mempty) -- FIXME: The state model should define an error type.
     NewChain c -> do
       modify $ \rs -> rs{unfetchedChains = unfetchedChains rs ++ pure c}
@@ -208,7 +207,7 @@ instance Realized IO ([Chain], [Vote]) ~ ([Chain], [Vote]) => RunModel NetworkMo
 
   postcondition _ Initial{} _ () = pure True
   postcondition (net@NetworkModel{nodeModel = s}, net'@NetworkModel{nodeModel = s'}) (Step a) _ (cs, vs) = do
-    let (expectedChains, expectedVotes) = fst (fromJust (transition (sortition net) s a))
+    let (expectedChains, expectedVotes) = maybe (mempty, mempty) fst $ transition (sortition net) s a
     let eqVotes vs vs' =
           let f MkVote{..} = (votingRound, creatorId, blockHash)
            in sort (f <$> vs) == sort (f <$> vs')
@@ -218,9 +217,12 @@ instance Realized IO ([Chain], [Vote]) ~ ([Chain], [Vote]) => RunModel NetworkMo
     when (a == Peras.Conformance.Model.Tick && newRound (clock s') (protocol s')) $
       monitorPost . counterexample $
         "  -- round: " ++ show (getRoundNumber $ inRound (clock s') (protocol s'))
-    unless (null vs) $ do
-      monitorPost . counterexample . show $ "  --      got:" <+> pPrint vs
-    counterexamplePost . show $ "  -- expected:" <+> pPrint expectedVotes
+    unless (eqChains cs expectedChains) $ do
+      monitorPost . counterexample . show $ "  --      got chains:" <+> pPrint cs
+      monitorPost . counterexample . show $ "  --      expected chains:" <+> pPrint expectedChains
+    unless (eqVotes vs expectedVotes) $ do
+      monitorPost . counterexample . show $ "  --      got votes:" <+> pPrint vs
+      monitorPost . counterexample . show $ "  --      expected votes:" <+> pPrint expectedVotes
     counterexamplePost . show $ "  " <> hang "-- model state before:" 2 (pPrint net)
     pure ok