{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}

-- | A reference simulator of the PBFT protocol under \"ideal circumstances\"
--
-- See 'step'.
--
module Test.ThreadNet.Ref.PBFT (
    Outcome (..)
  , Result (..)
  , State (..)
  , advanceUpTo
  , definitelyEnoughBlocks
  , emptyState
  , mkLeaderOf
  , nullState
  , pbftLimit
  , resultConstrName
  , simulate
  , simulateShort
  , step
  , viable
  ) where

import           Control.Applicative ((<|>))
import           Control.Arrow ((&&&))
import           Control.Monad (guard)
import           Data.Foldable as Foldable (foldl', toList)
import           Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import           Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import           Data.Set (Set)
import qualified Data.Set as Set
import           Data.Word (Word64)
import           GHC.Stack (HasCallStack)
import           Ouroboros.Consensus.Block
import           Ouroboros.Consensus.Config.SecurityParam
import           Ouroboros.Consensus.Node.ProtocolInfo
import           Ouroboros.Consensus.NodeId (CoreNodeId (..))
import           Ouroboros.Consensus.Protocol.PBFT (PBftParams (..),
                     PBftSignatureThreshold (..))
import           Ouroboros.Consensus.Util.Condense (Condense (..))
import           Test.ThreadNet.Util.NodeJoinPlan
import qualified Test.Util.InvertedMap as InvertedMap
import           Test.Util.InvertedMap (InvertedMap)
import           Test.Util.Slots (NumSlots (..))

oneK :: Num a => PBftParams -> a
oneK :: forall a. Num a => PBftParams -> a
oneK PBftParams{SecurityParam
pbftSecurityParam :: SecurityParam
pbftSecurityParam :: PBftParams -> SecurityParam
pbftSecurityParam} =
    Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SecurityParam -> Word64
maxRollbacks SecurityParam
pbftSecurityParam)

twoK :: Num a => PBftParams -> a
twoK :: forall a. Num a => PBftParams -> a
twoK PBftParams{SecurityParam
pbftSecurityParam :: PBftParams -> SecurityParam
pbftSecurityParam :: SecurityParam
pbftSecurityParam} =
    a
2 a -> a -> a
forall a. Num a => a -> a -> a
* Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral (SecurityParam -> Word64
maxRollbacks SecurityParam
pbftSecurityParam)

oneN :: Num a => PBftParams -> a
oneN :: forall a. Num a => PBftParams -> a
oneN PBftParams{pbftNumNodes :: PBftParams -> NumCoreNodes
pbftNumNodes = NumCoreNodes Word64
n} = Word64 -> a
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
n

{-------------------------------------------------------------------------------
  PBFT state
-------------------------------------------------------------------------------}

-- | Outcome of a node leading a slot
--
data Outcome

  = Absent
    -- ^ the leader hadn't yet joined

  | Nominal
    -- ^ the leader extended the networks' common chain with a valid block
    --
    -- (We're using /nominal/ in the engineer's sense of \"according to
    -- plan\".)

  | Unable
    -- ^ the leader could not forge a valid block

  | Wasted
    -- ^ the leader forged a valid-but-irrelevant block, because it forged
    -- before sufficiently synchronizing
    --
    -- As of commit 4eb23cfe \"Merge #1260\", this only happens if a node leads
    -- in the slot it joins. In that slot, it forges before the mini protocols
    -- are able to pull in any of the existing nodes' chain, and so it
    -- re-forges the epoch 0 boundary block (EBB).

  deriving (Outcome -> Outcome -> Bool
(Outcome -> Outcome -> Bool)
-> (Outcome -> Outcome -> Bool) -> Eq Outcome
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Outcome -> Outcome -> Bool
== :: Outcome -> Outcome -> Bool
$c/= :: Outcome -> Outcome -> Bool
/= :: Outcome -> Outcome -> Bool
Eq, Int -> Outcome -> ShowS
[Outcome] -> ShowS
Outcome -> String
(Int -> Outcome -> ShowS)
-> (Outcome -> String) -> ([Outcome] -> ShowS) -> Show Outcome
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Outcome -> ShowS
showsPrec :: Int -> Outcome -> ShowS
$cshow :: Outcome -> String
show :: Outcome -> String
$cshowList :: [Outcome] -> ShowS
showList :: [Outcome] -> ShowS
Show)

instance Condense Outcome where
  condense :: Outcome -> String
condense = Outcome -> String
forall a. Show a => a -> String
show

-- | The state of a PBFT net with only one longest chain
--
data State = State
  { State -> Seq CoreNodeId
forgers  :: !(Seq CoreNodeId)
    -- ^ who forged each of the last @k@ blocks

  , State -> NumNominals
nomCount :: !NumNominals
    -- ^ cache for optimization: number of 'Nominal's in 'outs'

  , State -> SlotNo
nextSlot :: !SlotNo

  , State -> Seq Outcome
outs     :: !(Seq Outcome)
    -- ^ the outcome of each the last @2k@ slots
  }
  deriving (State -> State -> Bool
(State -> State -> Bool) -> (State -> State -> Bool) -> Eq State
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: State -> State -> Bool
== :: State -> State -> Bool
$c/= :: State -> State -> Bool
/= :: State -> State -> Bool
Eq, Int -> State -> ShowS
[State] -> ShowS
State -> String
(Int -> State -> ShowS)
-> (State -> String) -> ([State] -> ShowS) -> Show State
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> State -> ShowS
showsPrec :: Int -> State -> ShowS
$cshow :: State -> String
show :: State -> String
$cshowList :: [State] -> ShowS
showList :: [State] -> ShowS
Show)

newtype NumNominals = NumNominals Int
  deriving (NumNominals -> NumNominals -> Bool
(NumNominals -> NumNominals -> Bool)
-> (NumNominals -> NumNominals -> Bool) -> Eq NumNominals
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NumNominals -> NumNominals -> Bool
== :: NumNominals -> NumNominals -> Bool
$c/= :: NumNominals -> NumNominals -> Bool
/= :: NumNominals -> NumNominals -> Bool
Eq, Eq NumNominals
Eq NumNominals =>
(NumNominals -> NumNominals -> Ordering)
-> (NumNominals -> NumNominals -> Bool)
-> (NumNominals -> NumNominals -> Bool)
-> (NumNominals -> NumNominals -> Bool)
-> (NumNominals -> NumNominals -> Bool)
-> (NumNominals -> NumNominals -> NumNominals)
-> (NumNominals -> NumNominals -> NumNominals)
-> Ord NumNominals
NumNominals -> NumNominals -> Bool
NumNominals -> NumNominals -> Ordering
NumNominals -> NumNominals -> NumNominals
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: NumNominals -> NumNominals -> Ordering
compare :: NumNominals -> NumNominals -> Ordering
$c< :: NumNominals -> NumNominals -> Bool
< :: NumNominals -> NumNominals -> Bool
$c<= :: NumNominals -> NumNominals -> Bool
<= :: NumNominals -> NumNominals -> Bool
$c> :: NumNominals -> NumNominals -> Bool
> :: NumNominals -> NumNominals -> Bool
$c>= :: NumNominals -> NumNominals -> Bool
>= :: NumNominals -> NumNominals -> Bool
$cmax :: NumNominals -> NumNominals -> NumNominals
max :: NumNominals -> NumNominals -> NumNominals
$cmin :: NumNominals -> NumNominals -> NumNominals
min :: NumNominals -> NumNominals -> NumNominals
Ord, Int -> NumNominals -> ShowS
[NumNominals] -> ShowS
NumNominals -> String
(Int -> NumNominals -> ShowS)
-> (NumNominals -> String)
-> ([NumNominals] -> ShowS)
-> Show NumNominals
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NumNominals -> ShowS
showsPrec :: Int -> NumNominals -> ShowS
$cshow :: NumNominals -> String
show :: NumNominals -> String
$cshowList :: [NumNominals] -> ShowS
showList :: [NumNominals] -> ShowS
Show)

emptyState :: State
emptyState :: State
emptyState = Seq CoreNodeId -> NumNominals -> SlotNo -> Seq Outcome -> State
State Seq CoreNodeId
forall a. Seq a
Seq.empty (Int -> NumNominals
NumNominals Int
0) SlotNo
0 Seq Outcome
forall a. Seq a
Seq.empty

-- | There are no recorded forgings
--
nullState :: State -> Bool
nullState :: State -> Bool
nullState State{Seq CoreNodeId
forgers :: State -> Seq CoreNodeId
forgers :: Seq CoreNodeId
forgers} = Seq CoreNodeId -> Bool
forall a. Seq a -> Bool
Seq.null Seq CoreNodeId
forgers

-- | Record the latest forging in the state
--
-- Should be followed by a call to 'extendOutcome'.
--
extendForger :: PBftParams -> State -> CoreNodeId -> State
extendForger :: PBftParams -> State -> CoreNodeId -> State
extendForger PBftParams
params st :: State
st@State{Seq CoreNodeId
forgers :: State -> Seq CoreNodeId
forgers :: Seq CoreNodeId
forgers} CoreNodeId
i = State
st
  { forgers = snd $ prune (oneK params) $ forgers Seq.|> i
  }

count :: (Eq a, Foldable t) => a -> t a -> Int
count :: forall a (t :: * -> *). (Eq a, Foldable t) => a -> t a -> Int
count a
a t a
bs = [()] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ () | a
b <- t a -> [a]
forall a. t a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t a
bs, a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b ]

prune :: Int -> Seq a -> (Seq a, Seq a)
prune :: forall a. Int -> Seq a -> (Seq a, Seq a)
prune Int
lim Seq a
x = Int -> Seq a -> (Seq a, Seq a)
forall a. Int -> Seq a -> (Seq a, Seq a)
Seq.splitAt Int
excess Seq a
x
  where
    excess :: Int
excess = Seq a -> Int
forall a. Seq a -> Int
Seq.length Seq a
x Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
lim

-- | Record the latest outcome in the state
--
extendOutcome :: PBftParams -> State -> Outcome -> State
extendOutcome :: PBftParams -> State -> Outcome -> State
extendOutcome PBftParams
params State{Seq CoreNodeId
forgers :: State -> Seq CoreNodeId
forgers :: Seq CoreNodeId
forgers, NumNominals
nomCount :: State -> NumNominals
nomCount :: NumNominals
nomCount, SlotNo
nextSlot :: State -> SlotNo
nextSlot :: SlotNo
nextSlot, Seq Outcome
outs :: State -> Seq Outcome
outs :: Seq Outcome
outs} Outcome
out = State
  { Seq CoreNodeId
forgers :: Seq CoreNodeId
forgers :: Seq CoreNodeId
forgers
  , nomCount :: NumNominals
nomCount = NumNominals
nomCount'
  , outs :: Seq Outcome
outs     = Seq Outcome
outs'
  , nextSlot :: SlotNo
nextSlot = SlotNo -> SlotNo
forall a. Enum a => a -> a
succ SlotNo
nextSlot
  }
  where
    (Seq Outcome
dropped, Seq Outcome
outs') = Int -> Seq Outcome -> (Seq Outcome, Seq Outcome)
forall a. Int -> Seq a -> (Seq a, Seq a)
prune (PBftParams -> Int
forall a. Num a => PBftParams -> a
twoK PBftParams
params) (Seq Outcome -> (Seq Outcome, Seq Outcome))
-> Seq Outcome -> (Seq Outcome, Seq Outcome)
forall a b. (a -> b) -> a -> b
$ Seq Outcome
outs Seq Outcome -> Outcome -> Seq Outcome
forall a. Seq a -> a -> Seq a
Seq.|> Outcome
out

    NumNominals Int
nc = NumNominals
nomCount
    nomCount' :: NumNominals
nomCount'      = Int -> NumNominals
NumNominals (Int -> NumNominals) -> Int -> NumNominals
forall a b. (a -> b) -> a -> b
$ Int
nc
      Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (if Outcome
Nominal Outcome -> Outcome -> Bool
forall a. Eq a => a -> a -> Bool
== Outcome
out then Int
1 else Int
0)
      Int -> Int -> Int
forall a. Num a => a -> a -> a
- Outcome -> Seq Outcome -> Int
forall a (t :: * -> *). (Eq a, Foldable t) => a -> t a -> Int
count Outcome
Nominal Seq Outcome
dropped

-- | @True@ if the state would violate 'pbftSignatureThreshold'
--
tooMany :: PBftParams -> State -> Bool
tooMany :: PBftParams -> State -> Bool
tooMany PBftParams
params st :: State
st@State{Seq CoreNodeId
forgers :: State -> Seq CoreNodeId
forgers :: Seq CoreNodeId
forgers} =
    CoreNodeId -> Seq CoreNodeId -> Int
forall a (t :: * -> *). (Eq a, Foldable t) => a -> t a -> Int
count CoreNodeId
i Seq CoreNodeId
forgers Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> PBftParams -> Int
forall a. Integral a => PBftParams -> a
pbftLimit PBftParams
params
  where
    i :: CoreNodeId
i = PBftParams -> State -> CoreNodeId
nextLeader PBftParams
params State
st

-- | How many blocks in the latest @k@-blocks that a single core node is
-- allowed to have signed
--
pbftLimit :: Integral a => PBftParams -> a
pbftLimit :: forall a. Integral a => PBftParams -> a
pbftLimit PBftParams
params =
    Double -> a
forall b. Integral b => Double -> b
forall a b. (RealFrac a, Integral b) => a -> b
floor (Double -> a) -> Double -> a
forall a b. (a -> b) -> a -> b
$ PBftParams -> Double
forall a. Num a => PBftParams -> a
oneK PBftParams
params Double -> Double -> Double
forall a. Num a => a -> a -> a
* PBftSignatureThreshold -> Double
getPBftSignatureThreshold PBftSignatureThreshold
pbftSignatureThreshold
  where
    PBftParams{PBftSignatureThreshold
pbftSignatureThreshold :: PBftParams -> PBftSignatureThreshold
pbftSignatureThreshold :: PBftSignatureThreshold
pbftSignatureThreshold} = PBftParams
params

-- | @True@ if the state resulted from a sequence of @2k@ slots that had less
-- than @k@ 'Nominal' outcomes
--
tooSparse :: PBftParams -> State -> Bool
tooSparse :: PBftParams -> State -> Bool
tooSparse PBftParams
params State{NumNominals
nomCount :: State -> NumNominals
nomCount :: NumNominals
nomCount, Seq Outcome
outs :: State -> Seq Outcome
outs :: Seq Outcome
outs} =
    Seq Outcome -> Int
forall a. Seq a -> Int
Seq.length Seq Outcome
outs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
nc Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> PBftParams -> Int
forall a. Num a => PBftParams -> a
oneK PBftParams
params
  where
    NumNominals Int
nc = NumNominals
nomCount

-- | @True@ if the state has a suffix of @n@ sequential 'Nominal' outcomes
--
-- Once this happens, by the assumption list on 'step', all remaining slots
-- will be 'Nominal'.
--
saturated :: PBftParams -> State -> Bool
saturated :: PBftParams -> State -> Bool
saturated PBftParams
params State{Seq Outcome
outs :: State -> Seq Outcome
outs :: Seq Outcome
outs} =
    Seq Outcome -> Int
forall a. Seq a -> Int
Seq.length Seq Outcome
outs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= PBftParams -> Int
forall a. Num a => PBftParams -> a
oneN PBftParams
params Bool -> Bool -> Bool
&& (Outcome -> Bool) -> Seq Outcome -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Outcome -> Outcome -> Bool
forall a. Eq a => a -> a -> Bool
== Outcome
Nominal) Seq Outcome
nouts
  where
    (Seq Outcome
_, Seq Outcome
nouts) = Int -> Seq Outcome -> (Seq Outcome, Seq Outcome)
forall a. Int -> Seq a -> (Seq a, Seq a)
prune (PBftParams -> Int
forall a. Num a => PBftParams -> a
oneN PBftParams
params) Seq Outcome
outs

{-------------------------------------------------------------------------------
  PBFT reference implementation
-------------------------------------------------------------------------------}

-- | Advance the state by one slot
--
-- ASSUMPTION Any new valid block is immediately selected by all nodes.
--
-- This assumption seems mild because of PBFT's fixed round-robin schedule; it
-- primarily constrains the network topology, network outages, node restarts,
-- clock skew, etc to be trivial. In other words, \"ideal circumstances\".
--
-- The assumption is useful in this reference implementation because it lets us
-- maintain a single \"global\" 'State' common to all nodes.
--
step :: PBftParams -> NodeJoinPlan -> State -> (Outcome, State)
step :: PBftParams -> NodeJoinPlan -> State -> (Outcome, State)
step PBftParams
params NodeJoinPlan
nodeJoinPlan State
st
  | Bool -> (SlotNo -> Bool) -> Maybe SlotNo -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
True (SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<) Maybe SlotNo
mbJ  = (Outcome -> Outcome
forall a. a -> a
id (Outcome -> Outcome)
-> (Outcome -> State) -> Outcome -> (Outcome, State)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Outcome -> State
stuck) Outcome
Absent
  | Bool
joinLead, Bool -> Bool
not Bool
isFirst = (Outcome -> Outcome
forall a. a -> a
id (Outcome -> Outcome)
-> (Outcome -> State) -> Outcome -> (Outcome, State)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Outcome -> State
stuck) Outcome
Wasted
  | PBftParams -> State -> Bool
tooMany PBftParams
params State
st'    = (Outcome -> Outcome
forall a. a -> a
id (Outcome -> Outcome)
-> (Outcome -> State) -> Outcome -> (Outcome, State)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& Outcome -> State
stuck) Outcome
Unable
  | Bool
otherwise             = (Outcome -> Outcome
forall a. a -> a
id (Outcome -> Outcome)
-> (Outcome -> State) -> Outcome -> (Outcome, State)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& PBftParams -> State -> Outcome -> State
extendOutcome PBftParams
params State
st') Outcome
Nominal
  where
    s :: SlotNo
s = State -> SlotNo
nextSlot State
st

    -- @s@'s scheduled leader
    i :: CoreNodeId
i = PBftParams -> State -> CoreNodeId
nextLeader PBftParams
params State
st

    -- when @i@ joins the network
    mbJ :: Maybe SlotNo
mbJ = CoreNodeId -> Map CoreNodeId SlotNo -> Maybe SlotNo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CoreNodeId
i Map CoreNodeId SlotNo
m where NodeJoinPlan Map CoreNodeId SlotNo
m = NodeJoinPlan
nodeJoinPlan

    -- @i@ is joining and also leading
    joinLead :: Bool
joinLead = SlotNo -> Maybe SlotNo
forall a. a -> Maybe a
Just SlotNo
s Maybe SlotNo -> Maybe SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe SlotNo
mbJ

    -- whether @i@ would be the first to lead
    isFirst :: Bool
isFirst = State -> Bool
nullState State
st

    -- the state that @i@ would make
    st' :: State
st' = PBftParams -> State -> CoreNodeId -> State
extendForger PBftParams
params State
st CoreNodeId
i

    stuck :: Outcome -> State
stuck Outcome
o = PBftParams -> State -> Outcome -> State
extendOutcome PBftParams
params State
st Outcome
o

-- | Iterate 'step'
--
-- POST 'nextSlot' is @>=@ the given slot
--
advanceUpTo :: PBftParams -> NodeJoinPlan -> State -> SlotNo -> State
advanceUpTo :: PBftParams -> NodeJoinPlan -> State -> SlotNo -> State
advanceUpTo PBftParams
params NodeJoinPlan
nodeJoinPlan = State -> SlotNo -> State
go
  where
    go :: State -> SlotNo -> State
go State
st SlotNo
s
      | State -> SlotNo
nextSlot State
st SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
>= SlotNo
s = State
st
      | Bool
otherwise        = State -> SlotNo -> State
go ((Outcome, State) -> State
forall a b. (a, b) -> b
snd ((Outcome, State) -> State) -> (Outcome, State) -> State
forall a b. (a -> b) -> a -> b
$ PBftParams -> NodeJoinPlan -> State -> (Outcome, State)
step PBftParams
params NodeJoinPlan
nodeJoinPlan State
st) SlotNo
s

-- | The result of a reference simulation
--
-- There is only one way that multiple competing chains arise given the PBFT
-- protocol under \"ideal circumstances\". When a node leads the slot in which
-- it joins, it will forge before syncing. The fresh one-block chain it creates
-- this way will be competitive if the other chains in the net are also only
-- one block long. Once there is a two-block chain in the net, it will be the
-- prefix of the net's one common chain going forward.
--
-- It is possible that the simulator is unable to statically determine which
-- one-block chain will be the prefix of the common prefix going forward. In
-- such a 'Nondeterministic' scenario, the simulator inherently can not predict
-- up to that slot. Moreover, it cannot predict past that slot, since the
-- choice of chain affects who may be able to lead next. Therefore, the
-- simulator offers no information beyond identifying this case.
--
data Result
  = Forked !NumSlots !(Map CoreNodeId (Set SlotNo))
    -- ^ All the chains in the net consist of 1 block. The map contains the
    -- deterministic block selections made by nodes, identifying each one-block
    -- chain by the slot in which its block was forged.
  | Nondeterministic
    -- ^ The outcomes cannot be determined statically.
  | Outcomes ![Outcome]
    -- ^ The expected outcomes of each slot.
  deriving (Int -> Result -> ShowS
[Result] -> ShowS
Result -> String
(Int -> Result -> ShowS)
-> (Result -> String) -> ([Result] -> ShowS) -> Show Result
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Result -> ShowS
showsPrec :: Int -> Result -> ShowS
$cshow :: Result -> String
show :: Result -> String
$cshowList :: [Result] -> ShowS
showList :: [Result] -> ShowS
Show)

resultConstrName :: Result -> String
resultConstrName :: Result -> String
resultConstrName = \case
  Outcomes{}       -> String
"Outcomes"
  Forked{}         -> String
"Forked"
  Result
Nondeterministic -> String
"Nondeterministic"

-- | Run 'simulateStep', switching to iterating 'step' once there is a 2-block
-- chain
--
-- See 'Result'.
--
simulate ::
     HasCallStack => PBftParams -> NodeJoinPlan -> NumSlots -> Result
simulate :: HasCallStack => PBftParams -> NodeJoinPlan -> NumSlots -> Result
simulate PBftParams
params NodeJoinPlan
nodeJoinPlan NumSlots
numSlots =
    case HasCallStack =>
PBftParams
-> NodeJoinPlan -> NumSlots -> Either DetOrNondet ShortState
PBftParams
-> NodeJoinPlan -> NumSlots -> Either DetOrNondet ShortState
simulateShort PBftParams
params NodeJoinPlan
nodeJoinPlan NumSlots
numSlots of
      Left (Det st :: State
st@State{Seq Outcome
outs :: State -> Seq Outcome
outs :: Seq Outcome
outs}) -> [Outcome] -> Result
Outcomes ([Outcome] -> Result) -> [Outcome] -> Result
forall a b. (a -> b) -> a -> b
$ Seq Outcome -> [Outcome]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Outcome
outs [Outcome] -> [Outcome] -> [Outcome]
forall a. Semigroup a => a -> a -> a
<> State -> [Outcome]
go State
st
      Left DetOrNondet
Nondet               -> Result
Nondeterministic
      Right ShortState
st                  -> NumSlots -> Map CoreNodeId (Set SlotNo) -> Result
Forked NumSlots
numSlots (Map CoreNodeId (Set SlotNo) -> Result)
-> Map CoreNodeId (Set SlotNo) -> Result
forall a b. (a -> b) -> a -> b
$ Map CoreNodeId (Set SlotNo)
selected Map CoreNodeId (Set SlotNo)
-> Map CoreNodeId (Set SlotNo) -> Map CoreNodeId (Set SlotNo)
forall a. Semigroup a => a -> a -> a
<> Map CoreNodeId (Set SlotNo)
forged
        where
          ShortState{Map CoreNodeId SlotNo
ssChains :: Map CoreNodeId SlotNo
ssChains :: ShortState -> Map CoreNodeId SlotNo
ssChains, Map CoreNodeId SlotNo
ssJoined :: Map CoreNodeId SlotNo
ssJoined :: ShortState -> Map CoreNodeId SlotNo
ssJoined} = ShortState
st

          -- nodes that forged a chain definitely selected it
          forged :: Map CoreNodeId (Set SlotNo)
          forged :: Map CoreNodeId (Set SlotNo)
forged = SlotNo -> Set SlotNo
forall a. a -> Set a
Set.singleton (SlotNo -> Set SlotNo)
-> Map CoreNodeId SlotNo -> Map CoreNodeId (Set SlotNo)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map CoreNodeId SlotNo
ssChains

          -- each chain is identified by the slot of the only block in the
          -- chain
          chains :: Set SlotNo
          chains :: Set SlotNo
chains = (SlotNo -> Set SlotNo) -> Map CoreNodeId SlotNo -> Set SlotNo
forall m a. Monoid m => (a -> m) -> Map CoreNodeId a -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap SlotNo -> Set SlotNo
forall a. a -> Set a
Set.singleton Map CoreNodeId SlotNo
ssChains

          -- nodes that did not forge their own chain select among the first
          -- available
          selected :: Map CoreNodeId (Set SlotNo)
          selected :: Map CoreNodeId (Set SlotNo)
selected = ((SlotNo -> Set SlotNo)
 -> Map CoreNodeId SlotNo -> Map CoreNodeId (Set SlotNo))
-> Map CoreNodeId SlotNo
-> (SlotNo -> Set SlotNo)
-> Map CoreNodeId (Set SlotNo)
forall a b c. (a -> b -> c) -> b -> a -> c
flip (SlotNo -> Set SlotNo)
-> Map CoreNodeId SlotNo -> Map CoreNodeId (Set SlotNo)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Map CoreNodeId SlotNo
ssJoined ((SlotNo -> Set SlotNo) -> Map CoreNodeId (Set SlotNo))
-> (SlotNo -> Set SlotNo) -> Map CoreNodeId (Set SlotNo)
forall a b. (a -> b) -> a -> b
$ \SlotNo
joinSlot ->
            case Set SlotNo -> Maybe SlotNo
forall a. Set a -> Maybe a
Set.lookupMin Set SlotNo
chains of
              -- if no chains /ever/ exist, the node selects none
              Maybe SlotNo
Nothing           -> Set SlotNo
forall a. Set a
Set.empty
              -- the first chain was forged in this slot
              Just SlotNo
s
                -- if the node joined before or during the forging of the first
                -- chain, it selects it
                | SlotNo
joinSlot SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= SlotNo
s -> SlotNo -> Set SlotNo
forall a. a -> Set a
Set.singleton SlotNo
s
                -- the node selects from among the chains that existed when it
                -- joined
                | Bool
otherwise     ->
                  ((Set SlotNo, Set SlotNo) -> Set SlotNo
forall a b. (a, b) -> a
fst ((Set SlotNo, Set SlotNo) -> Set SlotNo)
-> (Set SlotNo -> (Set SlotNo, Set SlotNo))
-> Set SlotNo
-> Set SlotNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SlotNo -> Set SlotNo -> (Set SlotNo, Set SlotNo)
forall a. Ord a => a -> Set a -> (Set a, Set a)
Set.split (SlotNo -> SlotNo
forall a. Enum a => a -> a
succ SlotNo
joinSlot)) (Set SlotNo -> Set SlotNo) -> Set SlotNo -> Set SlotNo
forall a b. (a -> b) -> a -> b
$
                  Set SlotNo
chains
  where
    NumSlots Word64
t = NumSlots
numSlots

    go :: State -> [Outcome]
go State
st
      | State -> SlotNo
nextSlot State
st SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
>= Word64 -> SlotNo
SlotNo Word64
t = []
      | Bool
otherwise               = Outcome
o Outcome -> [Outcome] -> [Outcome]
forall a. a -> [a] -> [a]
: State -> [Outcome]
go State
st'
      where
        (Outcome
o, State
st') = PBftParams -> NodeJoinPlan -> State -> (Outcome, State)
step PBftParams
params NodeJoinPlan
nodeJoinPlan State
st

{-------------------------------------------------------------------------------
  Prior to a 2-block chain arising
-------------------------------------------------------------------------------}

data DetOrNondet
  = Det !State
    -- ^ The plan is /deterministic/ and results in the given 'State'.
  | Nondet
    -- ^ The plan is /nondeterministic/; we cannot predict which 'State' it
    -- yields.
    --
    -- See 'Result'.

simulateShort ::
     HasCallStack
  => PBftParams -> NodeJoinPlan -> NumSlots -> Either DetOrNondet ShortState
simulateShort :: HasCallStack =>
PBftParams
-> NodeJoinPlan -> NumSlots -> Either DetOrNondet ShortState
simulateShort PBftParams
params NodeJoinPlan
nodeJoinPlan (NumSlots Word64
t)
  -- no one has time to forge
  | Word64
0 Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== Word64
t    = DetOrNondet -> Either DetOrNondet ShortState
forall a b. a -> Either a b
Left (DetOrNondet -> Either DetOrNondet ShortState)
-> DetOrNondet -> Either DetOrNondet ShortState
forall a b. (a -> b) -> a -> b
$ State -> DetOrNondet
Det State
emptyState
  | Bool
otherwise = ShortState -> Either DetOrNondet ShortState
go (ShortState -> Either DetOrNondet ShortState)
-> ShortState -> Either DetOrNondet ShortState
forall a b. (a -> b) -> a -> b
$ NodeJoinPlan -> ShortState
emptyShortState NodeJoinPlan
nodeJoinPlan
  where
    go :: ShortState -> Either DetOrNondet ShortState
    go :: ShortState -> Either DetOrNondet ShortState
go ShortState
st = do
      st' :: ShortState
st'@ShortState{ssNextSlot :: ShortState -> SlotNo
ssNextSlot = SlotNo
s'} <- HasCallStack =>
PBftParams -> ShortState -> Either DetOrNondet ShortState
PBftParams -> ShortState -> Either DetOrNondet ShortState
stepShort PBftParams
params ShortState
st
      (if SlotNo
s' SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< Word64 -> SlotNo
SlotNo Word64
t then ShortState -> Either DetOrNondet ShortState
go else ShortState -> Either DetOrNondet ShortState
forall a b. b -> Either a b
Right) ShortState
st'

-- | The state of a PBFT net with no chains or any number of one-blocks chains
--
-- See 'Result'.
--
data ShortState = ShortState
  { ShortState -> InvertedMap SlotNo CoreNodeId
ssAbsent   :: !(InvertedMap SlotNo CoreNodeId)
    -- ^ The nodes that haven't yet joined
    --
    -- INVARIANT @all (>= 'ssNextSlot') 'ssAbsent'@
  , ShortState -> Map CoreNodeId SlotNo
ssChains   :: !(Map CoreNodeId SlotNo)
    -- ^ The nodes that have forged a one-block chain and when
  , ShortState -> Map CoreNodeId SlotNo
ssJoined   :: !(Map CoreNodeId SlotNo)
    -- ^ The nodes that have joined in previous slots
  , ShortState -> SlotNo
ssNextSlot :: !SlotNo
  }
  deriving Int -> ShortState -> ShowS
[ShortState] -> ShowS
ShortState -> String
(Int -> ShortState -> ShowS)
-> (ShortState -> String)
-> ([ShortState] -> ShowS)
-> Show ShortState
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ShortState -> ShowS
showsPrec :: Int -> ShortState -> ShowS
$cshow :: ShortState -> String
show :: ShortState -> String
$cshowList :: [ShortState] -> ShowS
showList :: [ShortState] -> ShowS
Show

-- | Origin: no joined nodes and no chains
--
emptyShortState :: NodeJoinPlan -> ShortState
emptyShortState :: NodeJoinPlan -> ShortState
emptyShortState (NodeJoinPlan Map CoreNodeId SlotNo
m) = ShortState
  { ssAbsent :: InvertedMap SlotNo CoreNodeId
ssAbsent   = Map CoreNodeId SlotNo -> InvertedMap SlotNo CoreNodeId
forall v k. Ord v => Map k v -> InvertedMap v k
InvertedMap.fromMap Map CoreNodeId SlotNo
m
  , ssChains :: Map CoreNodeId SlotNo
ssChains   = Map CoreNodeId SlotNo
forall k a. Map k a
Map.empty
  , ssJoined :: Map CoreNodeId SlotNo
ssJoined   = Map CoreNodeId SlotNo
forall k a. Map k a
Map.empty
  , ssNextSlot :: SlotNo
ssNextSlot = SlotNo
0
  }

stepShort ::
     HasCallStack
  => PBftParams -> ShortState -> Either DetOrNondet ShortState
stepShort :: HasCallStack =>
PBftParams -> ShortState -> Either DetOrNondet ShortState
stepShort PBftParams
params ShortState
st
  | Just DetOrNondet
don <- Maybe DetOrNondet
mbDon = DetOrNondet -> Either DetOrNondet ShortState
forall a b. a -> Either a b
Left DetOrNondet
don
  | Bool
otherwise         = ShortState -> Either DetOrNondet ShortState
forall a b. b -> Either a b
Right ShortState
    { ssAbsent :: InvertedMap SlotNo CoreNodeId
ssAbsent   = InvertedMap SlotNo CoreNodeId
ssAbsent'
    , ssChains :: Map CoreNodeId SlotNo
ssChains   = Map CoreNodeId SlotNo
ssChains'
    , ssJoined :: Map CoreNodeId SlotNo
ssJoined   = Map CoreNodeId SlotNo
ssJoined'
    , ssNextSlot :: SlotNo
ssNextSlot = SlotNo
ssNextSlot'
    }
  where
    ShortState{InvertedMap SlotNo CoreNodeId
ssAbsent :: ShortState -> InvertedMap SlotNo CoreNodeId
ssAbsent :: InvertedMap SlotNo CoreNodeId
ssAbsent, Map CoreNodeId SlotNo
ssChains :: ShortState -> Map CoreNodeId SlotNo
ssChains :: Map CoreNodeId SlotNo
ssChains, Map CoreNodeId SlotNo
ssJoined :: ShortState -> Map CoreNodeId SlotNo
ssJoined :: Map CoreNodeId SlotNo
ssJoined, SlotNo
ssNextSlot :: ShortState -> SlotNo
ssNextSlot :: SlotNo
ssNextSlot} = ShortState
st

    leaderOf :: SlotNo -> CoreNodeId
    leaderOf :: SlotNo -> CoreNodeId
leaderOf = PBftParams -> SlotNo -> CoreNodeId
mkLeaderOf PBftParams
params

    joinSlotOf :: CoreNodeId -> SlotNo
    joinSlotOf :: CoreNodeId -> SlotNo
joinSlotOf =
      HasCallStack => NodeJoinPlan -> CoreNodeId -> SlotNo
NodeJoinPlan -> CoreNodeId -> SlotNo
coreNodeIdJoinSlot (NodeJoinPlan -> CoreNodeId -> SlotNo)
-> NodeJoinPlan -> CoreNodeId -> SlotNo
forall a b. (a -> b) -> a -> b
$ Map CoreNodeId SlotNo -> NodeJoinPlan
NodeJoinPlan (Map CoreNodeId SlotNo -> NodeJoinPlan)
-> Map CoreNodeId SlotNo -> NodeJoinPlan
forall a b. (a -> b) -> a -> b
$ Map CoreNodeId SlotNo
ssJoined' Map CoreNodeId SlotNo
-> Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo
forall a. Semigroup a => a -> a -> a
<> InvertedMap SlotNo CoreNodeId -> Map CoreNodeId SlotNo
forall k v. Ord k => InvertedMap v k -> Map k v
InvertedMap.toMap InvertedMap SlotNo CoreNodeId
ssAbsent'

    (InvertedMap SlotNo CoreNodeId
ssAbsent', Map CoreNodeId SlotNo
ssJoined') =
        (InvertedMap SlotNo CoreNodeId
later, Map CoreNodeId SlotNo
ssJoined Map CoreNodeId SlotNo
-> Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo
forall a. Semigroup a => a -> a -> a
<> InvertedMap SlotNo CoreNodeId -> Map CoreNodeId SlotNo
forall k v. Ord k => InvertedMap v k -> Map k v
InvertedMap.toMap InvertedMap SlotNo CoreNodeId
now)
      where
        (InvertedMap SlotNo CoreNodeId
now, InvertedMap SlotNo CoreNodeId
later) = (InvertedMap SlotNo CoreNodeId, InvertedMap SlotNo CoreNodeId)
-> (InvertedMap SlotNo CoreNodeId, InvertedMap SlotNo CoreNodeId)
forall a. a -> a
assertInvariant ((InvertedMap SlotNo CoreNodeId, InvertedMap SlotNo CoreNodeId)
 -> (InvertedMap SlotNo CoreNodeId, InvertedMap SlotNo CoreNodeId))
-> (InvertedMap SlotNo CoreNodeId, InvertedMap SlotNo CoreNodeId)
-> (InvertedMap SlotNo CoreNodeId, InvertedMap SlotNo CoreNodeId)
forall a b. (a -> b) -> a -> b
$
                       (SlotNo -> Bool)
-> InvertedMap SlotNo CoreNodeId
-> (InvertedMap SlotNo CoreNodeId, InvertedMap SlotNo CoreNodeId)
forall v k.
(v -> Bool)
-> InvertedMap v k -> (InvertedMap v k, InvertedMap v k)
InvertedMap.spanAntitone (SlotNo -> SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== SlotNo
ssNextSlot) InvertedMap SlotNo CoreNodeId
ssAbsent
    ssChains' :: Map CoreNodeId SlotNo
ssChains'              =
      (Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo)
-> (CoreNodeId -> Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo)
-> Maybe CoreNodeId
-> Map CoreNodeId SlotNo
-> Map CoreNodeId SlotNo
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo
forall a. a -> a
id (\CoreNodeId
l -> CoreNodeId
-> SlotNo -> Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CoreNodeId
l SlotNo
ssNextSlot) Maybe CoreNodeId
mbLeader (Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo)
-> Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo
forall a b. (a -> b) -> a -> b
$
      Map CoreNodeId SlotNo
ssChains
    ssNextSlot' :: SlotNo
ssNextSlot'            = SlotNo -> SlotNo
forall a. Enum a => a -> a
succ SlotNo
ssNextSlot

    assertInvariant :: forall a. a -> a
    assertInvariant :: forall a. a -> a
assertInvariant a
x = case InvertedMap SlotNo CoreNodeId
-> Maybe
     ((SlotNo, NonEmpty CoreNodeId), InvertedMap SlotNo CoreNodeId)
forall v k.
InvertedMap v k -> Maybe ((v, NonEmpty k), InvertedMap v k)
InvertedMap.minViewWithKey InvertedMap SlotNo CoreNodeId
ssAbsent of
      Just ((SlotNo
s, NonEmpty CoreNodeId
_), InvertedMap SlotNo CoreNodeId
_) | SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< SlotNo
ssNextSlot -> String -> a
forall a. HasCallStack => String -> a
error (String -> a) -> String -> a
forall a b. (a -> b) -> a -> b
$
        String
"ShortState invariant violation: " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> (SlotNo, InvertedMap SlotNo CoreNodeId) -> String
forall a. Show a => a -> String
show (SlotNo
ssNextSlot, InvertedMap SlotNo CoreNodeId
ssAbsent)
      Maybe
  ((SlotNo, NonEmpty CoreNodeId), InvertedMap SlotNo CoreNodeId)
_                                 -> a
x

    -- 'Just' if we can decide 'DetOrNondet'
    mbDon :: Maybe DetOrNondet
    mbDon :: Maybe DetOrNondet
mbDon =
      Maybe DetOrNondet
degenerateLim Maybe DetOrNondet -> Maybe DetOrNondet -> Maybe DetOrNondet
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
      Maybe DetOrNondet
detSecondLead Maybe DetOrNondet -> Maybe DetOrNondet -> Maybe DetOrNondet
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
      Maybe DetOrNondet
choiceMade Maybe DetOrNondet -> Maybe DetOrNondet -> Maybe DetOrNondet
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|>
      Maybe DetOrNondet
detAllHaveJoinedWithoutMultipleChains

    -- each node is 'Unable' to lead even once
    degenerateLim :: Maybe DetOrNondet
    degenerateLim :: Maybe DetOrNondet
degenerateLim = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ (Word64
0 :: Word64) Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== PBftParams -> Word64
forall a. Integral a => PBftParams -> a
pbftLimit PBftParams
params
      DetOrNondet -> Maybe DetOrNondet
forall a. a -> Maybe a
Just (DetOrNondet -> Maybe DetOrNondet)
-> DetOrNondet -> Maybe DetOrNondet
forall a b. (a -> b) -> a -> b
$ State -> DetOrNondet
Det State
        { forgers :: Seq CoreNodeId
forgers  = Seq CoreNodeId
forall a. Seq a
Seq.empty
        , nomCount :: NumNominals
nomCount = Int -> NumNominals
NumNominals Int
0
        , nextSlot :: SlotNo
nextSlot = SlotNo
ssNextSlot'
        , outs :: Seq Outcome
outs     = [Outcome] -> Seq Outcome
forall a. [a] -> Seq a
Seq.fromList ([Outcome] -> Seq Outcome) -> [Outcome] -> Seq Outcome
forall a b. (a -> b) -> a -> b
$
            [ if SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< CoreNodeId -> SlotNo
joinSlotOf (SlotNo -> CoreNodeId
leaderOf SlotNo
s) then Outcome
Absent else Outcome
Unable
            | SlotNo
s <- [SlotNo
0 .. SlotNo
ssNextSlot]
            ]
        }

    -- a node is leading for the second time; it has won the race
    detSecondLead :: Maybe DetOrNondet
    detSecondLead :: Maybe DetOrNondet
detSecondLead = do
      CoreNodeId
winner   <- Maybe CoreNodeId
mbLeader
      SlotNo
leadSlot <- CoreNodeId -> Map CoreNodeId SlotNo -> Maybe SlotNo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CoreNodeId
winner Map CoreNodeId SlotNo
ssChains
      DetOrNondet -> Maybe DetOrNondet
forall a. a -> Maybe a
Just (DetOrNondet -> Maybe DetOrNondet)
-> DetOrNondet -> Maybe DetOrNondet
forall a b. (a -> b) -> a -> b
$ State -> DetOrNondet
Det State
        { forgers :: Seq CoreNodeId
forgers  = [CoreNodeId] -> Seq CoreNodeId
forall a. [a] -> Seq a
Seq.fromList [CoreNodeId
winner, CoreNodeId
winner]
        , nomCount :: NumNominals
nomCount = Int -> NumNominals
NumNominals Int
2
        , nextSlot :: SlotNo
nextSlot = SlotNo
ssNextSlot'
        , outs :: Seq Outcome
outs     = [Outcome] -> Seq Outcome
forall a. [a] -> Seq a
Seq.fromList ([Outcome] -> Seq Outcome) -> [Outcome] -> Seq Outcome
forall a b. (a -> b) -> a -> b
$
          [ let l :: CoreNodeId
l = SlotNo -> CoreNodeId
leaderOf SlotNo
s in
            if | SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== SlotNo
leadSlot Bool -> Bool -> Bool
|| SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== SlotNo
ssNextSlot -> Outcome
Nominal
               | SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< CoreNodeId -> SlotNo
joinSlotOf CoreNodeId
l                 -> Outcome
Absent
               | SlotNo -> Maybe SlotNo
forall a. a -> Maybe a
Just SlotNo
s Maybe SlotNo -> Maybe SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== CoreNodeId -> Map CoreNodeId SlotNo -> Maybe SlotNo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CoreNodeId
l Map CoreNodeId SlotNo
ssChains  -> Outcome
Wasted
               | Bool
otherwise                        -> Outcome
Unable
          | SlotNo
s <- [SlotNo
0 .. SlotNo
ssNextSlot]
          ]
        }

    -- old node is leading for the first time in a slot later than its join
    -- slot
    choiceMade :: Maybe DetOrNondet
    choiceMade :: Maybe DetOrNondet
choiceMade = do
      CoreNodeId
leader <- Maybe CoreNodeId
mbLeader
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ CoreNodeId
leader CoreNodeId -> Map CoreNodeId SlotNo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.notMember` Map CoreNodeId SlotNo
ssChains
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ CoreNodeId
leader CoreNodeId -> Map CoreNodeId SlotNo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map CoreNodeId SlotNo
ssJoined
      case Map CoreNodeId SlotNo -> [(CoreNodeId, SlotNo)]
forall k a. Map k a -> [(k, a)]
Map.toList Map CoreNodeId SlotNo
ssChains of
        -- it's merely forging the first 1-block chain
        []                   -> Maybe DetOrNondet
forall a. Maybe a
Nothing

        [(CoreNodeId
winner, SlotNo
leadSlot)] -> DetOrNondet -> Maybe DetOrNondet
forall a. a -> Maybe a
Just (DetOrNondet -> Maybe DetOrNondet)
-> DetOrNondet -> Maybe DetOrNondet
forall a b. (a -> b) -> a -> b
$ State -> DetOrNondet
Det State
          { forgers :: Seq CoreNodeId
forgers  = [CoreNodeId] -> Seq CoreNodeId
forall a. [a] -> Seq a
Seq.fromList [CoreNodeId
winner, CoreNodeId
leader]
          , nomCount :: NumNominals
nomCount = Int -> NumNominals
NumNominals Int
2
          , nextSlot :: SlotNo
nextSlot = SlotNo
ssNextSlot'
          , outs :: Seq Outcome
outs     = [Outcome] -> Seq Outcome
forall a. [a] -> Seq a
Seq.fromList
            [ let l :: CoreNodeId
l = SlotNo -> CoreNodeId
leaderOf SlotNo
s in
              if | SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== SlotNo
leadSlot Bool -> Bool -> Bool
|| SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== SlotNo
ssNextSlot -> Outcome
Nominal
                 | SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< CoreNodeId -> SlotNo
joinSlotOf CoreNodeId
l                 -> Outcome
Absent
                 | SlotNo -> Maybe SlotNo
forall a. a -> Maybe a
Just SlotNo
s Maybe SlotNo -> Maybe SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== CoreNodeId -> Map CoreNodeId SlotNo -> Maybe SlotNo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CoreNodeId
l Map CoreNodeId SlotNo
ssChains  -> Outcome
Wasted
                 | Bool
otherwise                        -> Outcome
Unable
            | SlotNo
s <- [SlotNo
0 .. SlotNo
ssNextSlot]
            ]
          }

        (CoreNodeId, SlotNo)
_:(CoreNodeId, SlotNo)
_:[(CoreNodeId, SlotNo)]
_                -> DetOrNondet -> Maybe DetOrNondet
forall a. a -> Maybe a
Just DetOrNondet
Nondet

    -- all nodes have joined and there are not multiple chains
    detAllHaveJoinedWithoutMultipleChains :: Maybe DetOrNondet
    detAllHaveJoinedWithoutMultipleChains :: Maybe DetOrNondet
detAllHaveJoinedWithoutMultipleChains = do
      Bool -> Maybe ()
forall (f :: * -> *). Alternative f => Bool -> f ()
guard (Bool -> Maybe ()) -> Bool -> Maybe ()
forall a b. (a -> b) -> a -> b
$ InvertedMap SlotNo CoreNodeId -> Bool
forall v k. InvertedMap v k -> Bool
InvertedMap.null InvertedMap SlotNo CoreNodeId
ssAbsent'
      case Map CoreNodeId SlotNo -> [(CoreNodeId, SlotNo)]
forall k a. Map k a -> [(k, a)]
Map.toList Map CoreNodeId SlotNo
ssChains' of
        -- the degenerateLim guard should have prevented this evaluation; we
        -- know no other way for this state to be reachable
        []                   -> String -> Maybe DetOrNondet
forall a. HasCallStack => String -> a
error String
"impossible!"

        [(CoreNodeId
winner, SlotNo
leadSlot)] -> DetOrNondet -> Maybe DetOrNondet
forall a. a -> Maybe a
Just (DetOrNondet -> Maybe DetOrNondet)
-> DetOrNondet -> Maybe DetOrNondet
forall a b. (a -> b) -> a -> b
$ State -> DetOrNondet
Det State
          { forgers :: Seq CoreNodeId
forgers  = CoreNodeId -> Seq CoreNodeId
forall a. a -> Seq a
Seq.singleton CoreNodeId
winner
          , nomCount :: NumNominals
nomCount = Int -> NumNominals
NumNominals Int
1
          , nextSlot :: SlotNo
nextSlot = SlotNo
ssNextSlot'
          , outs :: Seq Outcome
outs     = [Outcome] -> Seq Outcome
forall a. [a] -> Seq a
Seq.fromList
            [ let l :: CoreNodeId
l = SlotNo -> CoreNodeId
leaderOf SlotNo
s in
              if | SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== SlotNo
leadSlot                   -> Outcome
Nominal
                 | SlotNo
s SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
< CoreNodeId -> SlotNo
joinSlotOf CoreNodeId
l                -> Outcome
Absent
                 | SlotNo -> Maybe SlotNo
forall a. a -> Maybe a
Just SlotNo
s Maybe SlotNo -> Maybe SlotNo -> Bool
forall a. Eq a => a -> a -> Bool
== CoreNodeId -> Map CoreNodeId SlotNo -> Maybe SlotNo
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup CoreNodeId
l Map CoreNodeId SlotNo
ssChains -> Outcome
Wasted
                 | Bool
otherwise                       -> Outcome
Unable
            | SlotNo
s <- [SlotNo
0 .. SlotNo
ssNextSlot]
            ]
          }

        (CoreNodeId, SlotNo)
_:(CoreNodeId, SlotNo)
_:[(CoreNodeId, SlotNo)]
_                -> Maybe DetOrNondet
forall a. Maybe a
Nothing

    -- the node that successfully leads in ssNextSlot
    mbLeader :: Maybe CoreNodeId
    mbLeader :: Maybe CoreNodeId
mbLeader
      -- node is 'Absent'
      | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ CoreNodeId
cid CoreNodeId -> Map CoreNodeId SlotNo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map CoreNodeId SlotNo
ssJoined'
      = Maybe CoreNodeId
forall a. Maybe a
Nothing

      -- each node is 'Unable' to lead twice before all lead once
      --
      -- Note: This whole function will reach a 'DetOrNondet' before any node
      -- leads twice.
      | (Word64
1 :: Word64) Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
< PBftParams -> Word64
forall a. Num a => PBftParams -> a
oneK PBftParams
params
      , (Word64
1 :: Word64) Word64 -> Word64 -> Bool
forall a. Eq a => a -> a -> Bool
== PBftParams -> Word64
forall a. Integral a => PBftParams -> a
pbftLimit PBftParams
params
      , CoreNodeId
cid CoreNodeId -> Map CoreNodeId SlotNo -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map CoreNodeId SlotNo
ssChains
      = Maybe CoreNodeId
forall a. Maybe a
Nothing

      | Bool
otherwise = CoreNodeId -> Maybe CoreNodeId
forall a. a -> Maybe a
Just CoreNodeId
cid
      where
        -- the node scheduled to lead in ssNextSlot
        cid :: CoreNodeId
cid = SlotNo -> CoreNodeId
leaderOf SlotNo
ssNextSlot

{-------------------------------------------------------------------------------
  Queries
-------------------------------------------------------------------------------}

-- | @True@ if there will be no necessary violations of \"@k@-blocks in
-- @2k@-slots\" before the given slot, assuming all remaining nodes join ASAP
--
-- PRE the given parameters and state are not already @tooSparse params st@
--
-- NOTE this function does not consider the competition between 1-block
-- multichains, so 'definitelyEnoughBlocks' must still be checked to confirm
--
viable :: PBftParams -> SlotNo -> NodeJoinPlan -> State -> Bool
viable :: PBftParams -> SlotNo -> NodeJoinPlan -> State -> Bool
viable PBftParams
params SlotNo
sentinel NodeJoinPlan
nodeJoinPlan State
st0 = State -> Bool
go State
st0
  where
    nodeJoinPlan' :: NodeJoinPlan
nodeJoinPlan' = PBftParams -> NodeJoinPlan -> SlotNo -> NodeJoinPlan
fillOut PBftParams
params NodeJoinPlan
nodeJoinPlan (State -> SlotNo
nextSlot State
st0)

    go :: State -> Bool
go State
st
      | SlotNo
sentinel SlotNo -> SlotNo -> Bool
forall a. Ord a => a -> a -> Bool
<= State -> SlotNo
nextSlot State
st = Bool
True
      | PBftParams -> State -> Bool
saturated PBftParams
params State
st     = Bool
True   -- an optimization
      | PBftParams -> State -> Bool
tooSparse PBftParams
params State
st'    = Bool
False
      | Bool
otherwise               = State -> Bool
go State
st'
      where
        (Outcome
_o, State
st') = PBftParams -> NodeJoinPlan -> State -> (Outcome, State)
step PBftParams
params NodeJoinPlan
nodeJoinPlan' State
st

-- | Confirm that the simulated chain includes at least @k@ blocks within every
-- @2k@-slot window
--
definitelyEnoughBlocks :: PBftParams -> Result -> Bool
definitelyEnoughBlocks :: PBftParams -> Result -> Bool
definitelyEnoughBlocks PBftParams
params = \case
    Forked NumSlots
numSlots Map CoreNodeId (Set SlotNo)
m ->
      let NumSlots Word64
t = NumSlots
numSlots
          nominals :: Word64
nominals   = if Map CoreNodeId (Set SlotNo) -> Bool
forall k a. Map k a -> Bool
Map.null Map CoreNodeId (Set SlotNo)
m then Word64
0 else Word64
1
          badCount :: Word64
badCount   = Word64 -> Word64 -> Word64
forall a. Ord a => a -> a -> a
max Word64
0 (Word64 -> Word64) -> Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ Word64
t Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
nominals
      in Word64
badCount Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
< Word64
k
    Result
Nondeterministic  -> Bool
False
    Outcomes [Outcome]
outcomes ->
      let enters :: [Word64]
enters = (Outcome -> Word64) -> [Outcome] -> [Word64]
forall a b. (a -> b) -> [a] -> [b]
map Outcome -> Word64
tick [Outcome]
outcomes
          exits :: [Word64]
exits  = Int -> Word64 -> [Word64]
forall a. Int -> a -> [a]
replicate (Int
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
k) Word64
0 [Word64] -> [Word64] -> [Word64]
forall a. [a] -> [a] -> [a]
++ [Word64]
enters
      in Word64 -> [(Word64, Word64)] -> Bool
go Word64
0 ([(Word64, Word64)] -> Bool) -> [(Word64, Word64)] -> Bool
forall a b. (a -> b) -> a -> b
$ [Word64] -> [Word64] -> [(Word64, Word64)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Word64]
exits [Word64]
enters
  where
    PBftParams{SecurityParam
pbftSecurityParam :: PBftParams -> SecurityParam
pbftSecurityParam :: SecurityParam
pbftSecurityParam} = PBftParams
params
    k :: Word64
k = SecurityParam -> Word64
maxRollbacks SecurityParam
pbftSecurityParam

    tick :: Outcome -> Word64
    tick :: Outcome -> Word64
tick Outcome
Nominal = Word64
0
    tick Outcome
_       = Word64
1

    go :: Word64 -> [(Word64, Word64)] -> Bool
    go :: Word64 -> [(Word64, Word64)] -> Bool
go Word64
badCount [(Word64, Word64)]
exens
      | Word64
badCount Word64 -> Word64 -> Bool
forall a. Ord a => a -> a -> Bool
> Word64
k = Bool
False
      | Bool
otherwise    = case [(Word64, Word64)]
exens of
          []                     -> Bool
True
          (Word64
exit, Word64
enter) : [(Word64, Word64)]
exens' -> Word64 -> [(Word64, Word64)] -> Bool
go (Word64
badCount Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
exit Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
enter) [(Word64, Word64)]
exens'

{-------------------------------------------------------------------------------
  Auxiliaries
-------------------------------------------------------------------------------}

mkLeaderOf :: PBftParams -> SlotNo -> CoreNodeId
mkLeaderOf :: PBftParams -> SlotNo -> CoreNodeId
mkLeaderOf PBftParams
params (SlotNo Word64
s) =
    Word64 -> CoreNodeId
CoreNodeId (Word64 -> CoreNodeId) -> Word64 -> CoreNodeId
forall a b. (a -> b) -> a -> b
$ Word64
s Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`mod` Word64
n
  where
    PBftParams{NumCoreNodes
pbftNumNodes :: PBftParams -> NumCoreNodes
pbftNumNodes :: NumCoreNodes
pbftNumNodes} = PBftParams
params
    NumCoreNodes Word64
n           = NumCoreNodes
pbftNumNodes

-- | The scheduled leader of 'nextSlot'
--
nextLeader :: PBftParams -> State -> CoreNodeId
nextLeader :: PBftParams -> State -> CoreNodeId
nextLeader PBftParams
params State{SlotNo
nextSlot :: State -> SlotNo
nextSlot :: SlotNo
nextSlot} = PBftParams -> SlotNo -> CoreNodeId
mkLeaderOf PBftParams
params SlotNo
nextSlot

-- | Finish an incomplete 'NodeJoinPlan': all remaining nodes join ASAP
--
-- Specifically, \"ASAP\" is either when the last already-scheduled node joins
-- or \"now\" (the given 'SlotNo'), whichever is latest.
--
fillOut :: PBftParams -> NodeJoinPlan -> SlotNo -> NodeJoinPlan
fillOut :: PBftParams -> NodeJoinPlan -> SlotNo -> NodeJoinPlan
fillOut PBftParams
params (NodeJoinPlan Map CoreNodeId SlotNo
m) SlotNo
s =
    Map CoreNodeId SlotNo -> NodeJoinPlan
NodeJoinPlan (Map CoreNodeId SlotNo -> NodeJoinPlan)
-> Map CoreNodeId SlotNo -> NodeJoinPlan
forall a b. (a -> b) -> a -> b
$
    (Map CoreNodeId SlotNo -> CoreNodeId -> Map CoreNodeId SlotNo)
-> Map CoreNodeId SlotNo -> [CoreNodeId] -> Map CoreNodeId SlotNo
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
Foldable.foldl' (\Map CoreNodeId SlotNo
acc CoreNodeId
i -> CoreNodeId
-> SlotNo -> Map CoreNodeId SlotNo -> Map CoreNodeId SlotNo
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert CoreNodeId
i SlotNo
j Map CoreNodeId SlotNo
acc) Map CoreNodeId SlotNo
m ([CoreNodeId] -> Map CoreNodeId SlotNo)
-> [CoreNodeId] -> Map CoreNodeId SlotNo
forall a b. (a -> b) -> a -> b
$
    Word64 -> CoreNodeId
CoreNodeId (Word64 -> CoreNodeId) -> [Word64] -> [CoreNodeId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Word64
i0 .. Word64
iN]
  where
    iN :: Word64
iN       = PBftParams -> Word64
forall a. Num a => PBftParams -> a
oneN PBftParams
params Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1
    j :: SlotNo
j        = SlotNo -> SlotNo -> SlotNo
forall a. Ord a => a -> a -> a
max SlotNo
s SlotNo
j0
    (Word64
i0, SlotNo
j0) = case Map CoreNodeId SlotNo -> Maybe (CoreNodeId, SlotNo)
forall k a. Map k a -> Maybe (k, a)
Map.lookupMax Map CoreNodeId SlotNo
m of
        Maybe (CoreNodeId, SlotNo)
Nothing                -> (Word64
0,      SlotNo
0)
        Just (CoreNodeId Word64
h, SlotNo
x) -> (Word64 -> Word64
forall a. Enum a => a -> a
succ Word64
h, SlotNo
x)