{-# 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 Cardano.Ledger.BaseTypes (unNonZero)
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 Test.Util.InvertedMap (InvertedMap)
import qualified Test.Util.InvertedMap as 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 (Word64 -> a) -> Word64 -> a
forall a b. (a -> b) -> a -> b
$ NonZero Word64 -> Word64
forall a. NonZero a -> a
unNonZero (NonZero Word64 -> Word64) -> NonZero Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> NonZero 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 (NonZero Word64 -> Word64
forall a. NonZero a -> a
unNonZero (NonZero Word64 -> Word64) -> NonZero Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> NonZero 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
  = -- | the leader hadn't yet joined
    Absent
  | -- | the leader extended the networks' common chain with a valid block
    --
    -- (We're using /nominal/ in the engineer's sense of \"according to
    -- plan\".)
    Nominal
  | -- | the leader could not forge a valid block
    Unable
  | -- | 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).
    Wasted
  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
  = -- | 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.
    Forked !NumSlots !(Map CoreNodeId (Set SlotNo))
  | -- | The outcomes cannot be determined statically.
    Nondeterministic
  | -- | The expected outcomes of each slot.
    Outcomes ![Outcome]
  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
  = -- | The plan is /deterministic/ and results in the given 'State'.
    Det !State
  | -- | The plan is /nondeterministic/; we cannot predict which 'State' it
    -- yields.
    --
    -- See 'Result'.
    Nondet

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{ssNextSlot = s'} <- HasCallStack =>
PBftParams -> ShortState -> Either DetOrNondet ShortState
PBftParams -> ShortState -> Either DetOrNondet ShortState
stepShort PBftParams
params ShortState
st
    (if s' < SlotNo t then go else Right) 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
    winner <- Maybe CoreNodeId
mbLeader
    leadSlot <- Map.lookup winner ssChains
    Just $
      Det
        State
          { forgers = Seq.fromList [winner, winner]
          , nomCount = NumNominals 2
          , nextSlot = ssNextSlot'
          , outs =
              Seq.fromList $
                [ let l = SlotNo -> CoreNodeId
leaderOf SlotNo
s
                   in if
                        | s == leadSlot || s == ssNextSlot -> Nominal
                        | s < joinSlotOf l -> Absent
                        | Just s == Map.lookup l ssChains -> Wasted
                        | otherwise -> Unable
                | s <- [0 .. 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
    leader <- Maybe CoreNodeId
mbLeader
    guard $ leader `Map.notMember` ssChains
    guard $ leader `Map.member` ssJoined
    case Map.toList 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 = NonZero Word64 -> Word64
forall a. NonZero a -> a
unNonZero (NonZero Word64 -> Word64) -> NonZero Word64 -> Word64
forall a b. (a -> b) -> a -> b
$ SecurityParam -> NonZero 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)