{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
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
data Outcome
= Absent
| Nominal
| Unable
| 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
data State = State
{ State -> Seq CoreNodeId
forgers :: !(Seq CoreNodeId)
, State -> NumNominals
nomCount :: !NumNominals
, State -> SlotNo
nextSlot :: !SlotNo
, State -> Seq Outcome
outs :: !(Seq Outcome)
}
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
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
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
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
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
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
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
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
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
i :: CoreNodeId
i = PBftParams -> State -> CoreNodeId
nextLeader PBftParams
params State
st
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
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
isFirst :: Bool
isFirst = State -> Bool
nullState State
st
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
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
data Result
= Forked !NumSlots !(Map CoreNodeId (Set SlotNo))
| Nondeterministic
| 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"
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
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
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
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
Maybe SlotNo
Nothing -> Set SlotNo
forall a. Set a
Set.empty
Just SlotNo
s
| 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
| 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
data DetOrNondet
= Det !State
| 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)
| 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'
data ShortState = ShortState
{ ShortState -> InvertedMap SlotNo CoreNodeId
ssAbsent :: !(InvertedMap SlotNo CoreNodeId)
, ShortState -> Map CoreNodeId SlotNo
ssChains :: !(Map CoreNodeId SlotNo)
, ShortState -> Map CoreNodeId SlotNo
ssJoined :: !(Map CoreNodeId SlotNo)
, 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
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
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
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]
]
}
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]
]
}
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
[] -> 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
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
[] -> 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
mbLeader :: Maybe CoreNodeId
mbLeader :: Maybe CoreNodeId
mbLeader
| 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
| (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
cid :: CoreNodeId
cid = SlotNo -> CoreNodeId
leaderOf SlotNo
ssNextSlot
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
| 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
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'
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
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
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)