{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

-- TODO rename to .Alternative?
module Test.Ouroboros.Consensus.ChainGenerator.Adversarial
  ( -- * Generating
    AdversarialRecipe (AdversarialRecipe, arHonest, arParams, arPrefix)
  , CheckedAdversarialRecipe (UnsafeCheckedAdversarialRecipe, carHonest, carParams, carWin)
  , NoSuchAdversarialChainSchema (NoSuchAdversarialBlock, NoSuchCompetitor, NoSuchIntersection)
  , SomeCheckedAdversarialRecipe (SomeCheckedAdversarialRecipe)
  , checkAdversarialRecipe
  , uniformAdversarialChain

    -- * Testing
  , AdversarialViolation (..)
  , AnchorViolation (HonestActiveMustAnchorAdversarial)
  , ChainSchema (ChainSchema)
  , RaceViolation (AdversaryWonRace, rvAdv, rvHon)
  , checkAdversarialChain
  , genPrefixBlockCount
  ) where

import Control.Applicative ((<|>))
import Control.Monad (foldM, forM_, void, when)
import qualified Control.Monad.Except as Exn
import Control.Monad.ST (ST)
import Data.Maybe (fromJust, fromMaybe)
import Data.Proxy (Proxy (Proxy))
import qualified Data.Vector.Unboxed as Vector
import qualified System.Random.Stateful as R
import qualified Test.Ouroboros.Consensus.ChainGenerator.BitVector as BV
import qualified Test.Ouroboros.Consensus.ChainGenerator.Counting as C
import Test.Ouroboros.Consensus.ChainGenerator.Honest
  ( ChainSchema (ChainSchema)
  , HonestRecipe (HonestRecipe)
  )
import Test.Ouroboros.Consensus.ChainGenerator.Params
  ( Asc
  , Delta (Delta)
  , Kcp (Kcp)
  , Scg (Scg)
  )
import qualified Test.Ouroboros.Consensus.ChainGenerator.RaceIterator as RI
import Test.Ouroboros.Consensus.ChainGenerator.Slot
  ( E (ActiveSlotE, EmptySlotE, SlotE)
  )
import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S
import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some

-----

data AnchorViolation
  = -- | An honest active slot must immediately precede the adversarial interval
    HonestActiveMustAnchorAdversarial
  | -- | The were not exactly 'arPrefix' many active slots preceding @adv@
    WrongNumberOfHonestPredecessors
  deriving (AnchorViolation -> AnchorViolation -> Bool
(AnchorViolation -> AnchorViolation -> Bool)
-> (AnchorViolation -> AnchorViolation -> Bool)
-> Eq AnchorViolation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: AnchorViolation -> AnchorViolation -> Bool
== :: AnchorViolation -> AnchorViolation -> Bool
$c/= :: AnchorViolation -> AnchorViolation -> Bool
/= :: AnchorViolation -> AnchorViolation -> Bool
Eq, ReadPrec [AnchorViolation]
ReadPrec AnchorViolation
Int -> ReadS AnchorViolation
ReadS [AnchorViolation]
(Int -> ReadS AnchorViolation)
-> ReadS [AnchorViolation]
-> ReadPrec AnchorViolation
-> ReadPrec [AnchorViolation]
-> Read AnchorViolation
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS AnchorViolation
readsPrec :: Int -> ReadS AnchorViolation
$creadList :: ReadS [AnchorViolation]
readList :: ReadS [AnchorViolation]
$creadPrec :: ReadPrec AnchorViolation
readPrec :: ReadPrec AnchorViolation
$creadListPrec :: ReadPrec [AnchorViolation]
readListPrec :: ReadPrec [AnchorViolation]
Read, Int -> AnchorViolation -> ShowS
[AnchorViolation] -> ShowS
AnchorViolation -> String
(Int -> AnchorViolation -> ShowS)
-> (AnchorViolation -> String)
-> ([AnchorViolation] -> ShowS)
-> Show AnchorViolation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> AnchorViolation -> ShowS
showsPrec :: Int -> AnchorViolation -> ShowS
$cshow :: AnchorViolation -> String
show :: AnchorViolation -> String
$cshowList :: [AnchorViolation] -> ShowS
showList :: [AnchorViolation] -> ShowS
Show)

-- | A violation of Races Before Acceleration Assumption
--
-- INVARIANT: @'C.windowLast' 'rvAdv' < 'C.windowLast' 'rvHon' + 'Delta'@
--
-- INVARIANT: @'C.windowStart' 'rvHon' <= 'C.windowStart' 'rvAdv'@
data RaceViolation hon adv = AdversaryWonRace
  { forall hon adv. RaceViolation hon adv -> Race adv
rvAdv :: !(RI.Race adv)
  -- ^ The adversarial race window
  , forall hon adv. RaceViolation hon adv -> Race hon
rvHon :: !(RI.Race hon)
  -- ^ The honest race window
  }
  deriving (RaceViolation hon adv -> RaceViolation hon adv -> Bool
(RaceViolation hon adv -> RaceViolation hon adv -> Bool)
-> (RaceViolation hon adv -> RaceViolation hon adv -> Bool)
-> Eq (RaceViolation hon adv)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall hon adv.
RaceViolation hon adv -> RaceViolation hon adv -> Bool
$c== :: forall hon adv.
RaceViolation hon adv -> RaceViolation hon adv -> Bool
== :: RaceViolation hon adv -> RaceViolation hon adv -> Bool
$c/= :: forall hon adv.
RaceViolation hon adv -> RaceViolation hon adv -> Bool
/= :: RaceViolation hon adv -> RaceViolation hon adv -> Bool
Eq, ReadPrec [RaceViolation hon adv]
ReadPrec (RaceViolation hon adv)
Int -> ReadS (RaceViolation hon adv)
ReadS [RaceViolation hon adv]
(Int -> ReadS (RaceViolation hon adv))
-> ReadS [RaceViolation hon adv]
-> ReadPrec (RaceViolation hon adv)
-> ReadPrec [RaceViolation hon adv]
-> Read (RaceViolation hon adv)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall hon adv. ReadPrec [RaceViolation hon adv]
forall hon adv. ReadPrec (RaceViolation hon adv)
forall hon adv. Int -> ReadS (RaceViolation hon adv)
forall hon adv. ReadS [RaceViolation hon adv]
$creadsPrec :: forall hon adv. Int -> ReadS (RaceViolation hon adv)
readsPrec :: Int -> ReadS (RaceViolation hon adv)
$creadList :: forall hon adv. ReadS [RaceViolation hon adv]
readList :: ReadS [RaceViolation hon adv]
$creadPrec :: forall hon adv. ReadPrec (RaceViolation hon adv)
readPrec :: ReadPrec (RaceViolation hon adv)
$creadListPrec :: forall hon adv. ReadPrec [RaceViolation hon adv]
readListPrec :: ReadPrec [RaceViolation hon adv]
Read, Int -> RaceViolation hon adv -> ShowS
[RaceViolation hon adv] -> ShowS
RaceViolation hon adv -> String
(Int -> RaceViolation hon adv -> ShowS)
-> (RaceViolation hon adv -> String)
-> ([RaceViolation hon adv] -> ShowS)
-> Show (RaceViolation hon adv)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall hon adv. Int -> RaceViolation hon adv -> ShowS
forall hon adv. [RaceViolation hon adv] -> ShowS
forall hon adv. RaceViolation hon adv -> String
$cshowsPrec :: forall hon adv. Int -> RaceViolation hon adv -> ShowS
showsPrec :: Int -> RaceViolation hon adv -> ShowS
$cshow :: forall hon adv. RaceViolation hon adv -> String
show :: RaceViolation hon adv -> String
$cshowList :: forall hon adv. [RaceViolation hon adv] -> ShowS
showList :: [RaceViolation hon adv] -> ShowS
Show)

data AdversarialViolation hon adv
  = BadAnchor !AnchorViolation
  | -- | The schema does not contain a positive number of active slots
    BadCount
  | BadRace !(RaceViolation hon adv)
  | -- | The density of the adversarial schema is higher than the density of
    -- the honest schema in the first stability window after the intersection.
    --
    -- In @BadDensity w h a@, @w@ is a prefix of the first stability window
    -- after the intersection where the density is higher in the adversarial
    -- schema. @h@ is the amount of active slots in @w@ in the honest schema.
    -- @a@ is the amount of active slots in @w@ in the adversarial schema.
    BadDensity (C.SomeWindow RI.RaceLbl adv SlotE) Int Int
  deriving (AdversarialViolation hon adv
-> AdversarialViolation hon adv -> Bool
(AdversarialViolation hon adv
 -> AdversarialViolation hon adv -> Bool)
-> (AdversarialViolation hon adv
    -> AdversarialViolation hon adv -> Bool)
-> Eq (AdversarialViolation hon adv)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall hon adv.
AdversarialViolation hon adv
-> AdversarialViolation hon adv -> Bool
$c== :: forall hon adv.
AdversarialViolation hon adv
-> AdversarialViolation hon adv -> Bool
== :: AdversarialViolation hon adv
-> AdversarialViolation hon adv -> Bool
$c/= :: forall hon adv.
AdversarialViolation hon adv
-> AdversarialViolation hon adv -> Bool
/= :: AdversarialViolation hon adv
-> AdversarialViolation hon adv -> Bool
Eq, ReadPrec [AdversarialViolation hon adv]
ReadPrec (AdversarialViolation hon adv)
Int -> ReadS (AdversarialViolation hon adv)
ReadS [AdversarialViolation hon adv]
(Int -> ReadS (AdversarialViolation hon adv))
-> ReadS [AdversarialViolation hon adv]
-> ReadPrec (AdversarialViolation hon adv)
-> ReadPrec [AdversarialViolation hon adv]
-> Read (AdversarialViolation hon adv)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall hon adv. ReadPrec [AdversarialViolation hon adv]
forall hon adv. ReadPrec (AdversarialViolation hon adv)
forall hon adv. Int -> ReadS (AdversarialViolation hon adv)
forall hon adv. ReadS [AdversarialViolation hon adv]
$creadsPrec :: forall hon adv. Int -> ReadS (AdversarialViolation hon adv)
readsPrec :: Int -> ReadS (AdversarialViolation hon adv)
$creadList :: forall hon adv. ReadS [AdversarialViolation hon adv]
readList :: ReadS [AdversarialViolation hon adv]
$creadPrec :: forall hon adv. ReadPrec (AdversarialViolation hon adv)
readPrec :: ReadPrec (AdversarialViolation hon adv)
$creadListPrec :: forall hon adv. ReadPrec [AdversarialViolation hon adv]
readListPrec :: ReadPrec [AdversarialViolation hon adv]
Read, Int -> AdversarialViolation hon adv -> ShowS
[AdversarialViolation hon adv] -> ShowS
AdversarialViolation hon adv -> String
(Int -> AdversarialViolation hon adv -> ShowS)
-> (AdversarialViolation hon adv -> String)
-> ([AdversarialViolation hon adv] -> ShowS)
-> Show (AdversarialViolation hon adv)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall hon adv. Int -> AdversarialViolation hon adv -> ShowS
forall hon adv. [AdversarialViolation hon adv] -> ShowS
forall hon adv. AdversarialViolation hon adv -> String
$cshowsPrec :: forall hon adv. Int -> AdversarialViolation hon adv -> ShowS
showsPrec :: Int -> AdversarialViolation hon adv -> ShowS
$cshow :: forall hon adv. AdversarialViolation hon adv -> String
show :: AdversarialViolation hon adv -> String
$cshowList :: forall hon adv. [AdversarialViolation hon adv] -> ShowS
showList :: [AdversarialViolation hon adv] -> ShowS
Show)

-- | Check the chain matches the given 'AdversarialRecipe'.
--
-- * It must intersect the honest chain at an active slot
-- * It must satisfy the Races Before Acceleration Assumption
--   (which implies the Length of Competing Chains Assumption)
--
-- Definition of a /Praos Race Window/ of a chain. It is an interval of slots
-- that contains at least @k+1@ blocks of the chain and exactly 'Delta' slots
-- after the @k+1@st block.
--
-- Definition of the /Length of Competing Chains Assumption/. We assume every adversarial
-- chain contains at most @k@ blocks in the Praos Race Window anchored at the
-- the intersection.
--
-- Definition of /Acceleration Lower Bound of an Adversarial Chain/. It is
-- the lowest slot at which an adversary could speed up its elections on a
-- given adversarial chain. It is defined as the 'Scg'-th slot after the first
-- adversarial block or the 'Delta'-th slot after the @k+1@st honest block after the
-- intersection, whichever is greater.
--
-- Definition of the /Races Before Acceleration Assumption/. Every adversarial
-- chain has at most @k@ blocks in every Praos Race Window of the honest chain
-- that starts after the intersection and ends before the acceleration lower
-- bound.
--
-- Definition of the /Genesis Implication Conjecture/. We conjecture that
-- assuming that the Genesis window length is no greater than the Stability
-- Window and that every possible adversarial chain satisfies the Races
-- in Stability Windows Assumption, then the honest chain strictly wins every possible density
-- comparison from the Ouroboros Genesis paper. The key intuition is that a less
-- dense chain would have to lose at least one Praos race within the Genesis window.
checkAdversarialChain ::
  forall base hon adv.
  AdversarialRecipe base hon ->
  ChainSchema base adv ->
  Exn.Except (AdversarialViolation hon adv) ()
checkAdversarialChain :: forall base hon adv.
AdversarialRecipe base hon
-> ChainSchema base adv -> Except (AdversarialViolation hon adv) ()
checkAdversarialChain AdversarialRecipe base hon
recipe ChainSchema base adv
adv = do
  ExceptT (AdversarialViolation hon adv) Identity ()
checkStart
  ExceptT (AdversarialViolation hon adv) Identity ()
checkCount
  ExceptT (AdversarialViolation hon adv) Identity ()
checkRaces
  ExceptT (AdversarialViolation hon adv) Identity ()
checkDensity
 where
  AdversarialRecipe
    { arHonest :: forall base hon. AdversarialRecipe base hon -> ChainSchema base hon
arHonest = ChainSchema Contains 'SlotE base hon
winH Vector hon 'SlotE S
vH
    , arParams :: forall base hon. AdversarialRecipe base hon -> (Kcp, Scg, Delta)
arParams = (Kcp Int
k, Scg Int
s, Delta Int
d)
    , Var hon 'ActiveSlotE
arPrefix :: forall base hon. AdversarialRecipe base hon -> Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
arPrefix
    } = AdversarialRecipe base hon
recipe

  ChainSchema Contains 'SlotE base adv
winA Vector adv 'SlotE S
vA = ChainSchema base adv
adv

  checkStart :: ExceptT (AdversarialViolation hon adv) Identity ()
checkStart = do
    let startA :: Index base 'SlotE
startA = Contains 'SlotE base adv -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE base adv
winA :: C.Index base SlotE
        intersection :: Index base 'SlotE
intersection = Index base 'SlotE
startA Index base 'SlotE -> Int -> Index base 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.- Int
1 :: C.Index base SlotE

    -- The intersection must be at an active slot in the honest chain.
    case Contains 'SlotE base hon
-> Index base 'SlotE -> Maybe (Index hon 'SlotE)
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner
-> Index outer elem -> Maybe (Index inner elem)
C.toWindow Contains 'SlotE base hon
winH Index base 'SlotE
intersection of
      Maybe (Index hon 'SlotE)
Nothing -> do
        -- the genesis block is the only permissible anchor outside of @hon@
        Bool
-> ExceptT (AdversarialViolation hon adv) Identity ()
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Index base 'SlotE
startA Index base 'SlotE -> Index base 'SlotE -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Index base 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) (ExceptT (AdversarialViolation hon adv) Identity ()
 -> ExceptT (AdversarialViolation hon adv) Identity ())
-> ExceptT (AdversarialViolation hon adv) Identity ()
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a b. (a -> b) -> a -> b
$ AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a.
AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError (AdversarialViolation hon adv
 -> ExceptT (AdversarialViolation hon adv) Identity ())
-> AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a b. (a -> b) -> a -> b
$ AnchorViolation -> AdversarialViolation hon adv
forall hon adv. AnchorViolation -> AdversarialViolation hon adv
BadAnchor AnchorViolation
HonestActiveMustAnchorAdversarial
        Bool
-> ExceptT (AdversarialViolation hon adv) Identity ()
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Var hon 'ActiveSlotE
arPrefix Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE -> Bool
forall a. Eq a => a -> a -> Bool
/= Int -> Var hon 'ActiveSlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) (ExceptT (AdversarialViolation hon adv) Identity ()
 -> ExceptT (AdversarialViolation hon adv) Identity ())
-> ExceptT (AdversarialViolation hon adv) Identity ()
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a b. (a -> b) -> a -> b
$ AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a.
AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError (AdversarialViolation hon adv
 -> ExceptT (AdversarialViolation hon adv) Identity ())
-> AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a b. (a -> b) -> a -> b
$ AnchorViolation -> AdversarialViolation hon adv
forall hon adv. AnchorViolation -> AdversarialViolation hon adv
BadAnchor AnchorViolation
WrongNumberOfHonestPredecessors
      Just Index hon 'SlotE
i -> do
        let Index hon 'SlotE
_ = Index hon 'SlotE
i :: C.Index hon SlotE

        Bool
-> ExceptT (AdversarialViolation hon adv) Identity ()
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Proxy 'Inverted -> Vector hon 'SlotE S -> Index hon 'SlotE -> Bool
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol -> Vector base 'SlotE S -> Index base 'SlotE -> Bool
BV.testV Proxy 'Inverted
S.inverted Vector hon 'SlotE S
vH Index hon 'SlotE
i) (ExceptT (AdversarialViolation hon adv) Identity ()
 -> ExceptT (AdversarialViolation hon adv) Identity ())
-> ExceptT (AdversarialViolation hon adv) Identity ()
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a b. (a -> b) -> a -> b
$ do
          AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a.
AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError (AdversarialViolation hon adv
 -> ExceptT (AdversarialViolation hon adv) Identity ())
-> AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a b. (a -> b) -> a -> b
$ AnchorViolation -> AdversarialViolation hon adv
forall hon adv. AnchorViolation -> AdversarialViolation hon adv
BadAnchor AnchorViolation
HonestActiveMustAnchorAdversarial

        C.SomeWindow Proxy precedingSlots <-
          SomeWindow "foo" hon 'SlotE
-> ExceptT
     (AdversarialViolation hon adv)
     Identity
     (SomeWindow "foo" hon 'SlotE)
forall a. a -> ExceptT (AdversarialViolation hon adv) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow "foo" hon 'SlotE
 -> ExceptT
      (AdversarialViolation hon adv)
      Identity
      (SomeWindow "foo" hon 'SlotE))
-> SomeWindow "foo" hon 'SlotE
-> ExceptT
     (AdversarialViolation hon adv)
     Identity
     (SomeWindow "foo" hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ Size hon 'SlotE
-> Lbl "foo"
-> Index hon 'SlotE
-> Index hon 'SlotE
-> SomeWindow "foo" hon 'SlotE
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl).
Size outer elem
-> Lbl lbl
-> Index outer elem
-> Index outer elem
-> SomeWindow lbl outer elem
C.withWindowBetween (Contains 'SlotE base hon -> Size hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE base hon
winH) (forall {k} (lbl :: k). Lbl lbl
forall (lbl :: Symbol). Lbl lbl
C.Lbl @"foo") (Int -> Index hon 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) Index hon 'SlotE
i
        let pc = Proxy 'NotInverted
-> Vector (Win "foo" skolem) 'SlotE S
-> Size (Win "foo" skolem) (PreImage 'NotInverted 'ActiveSlotE)
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S -> Size base (PreImage pol 'ActiveSlotE)
BV.countActivesInV Proxy 'NotInverted
S.notInverted (Contains 'SlotE hon (Win "foo" skolem)
-> Vector hon 'SlotE S -> Vector (Win "foo" skolem) 'SlotE S
forall {k} a (elem :: k) outer inner.
Unbox a =>
Contains elem outer inner
-> Vector outer elem a -> Vector inner elem a
C.sliceV Contains 'SlotE hon (Win "foo" skolem)
precedingSlots Vector hon 'SlotE S
vH)

        -- arPrefix must correctly count the active slots in the part of
        -- the chain upto the intersection
        when (C.fromWindowVar precedingSlots (C.toVar pc) /= arPrefix) $ do
          Exn.throwError $ BadAnchor WrongNumberOfHonestPredecessors

  checkCount :: ExceptT (AdversarialViolation hon adv) Identity ()
checkCount = do
    let pc :: Size adv (PreImage 'NotInverted 'ActiveSlotE)
pc = Proxy 'NotInverted
-> Vector adv 'SlotE S
-> Size adv (PreImage 'NotInverted 'ActiveSlotE)
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S -> Size base (PreImage pol 'ActiveSlotE)
BV.countActivesInV Proxy 'NotInverted
S.notInverted Vector adv 'SlotE S
vA
    Bool
-> ExceptT (AdversarialViolation hon adv) Identity ()
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Count adv 'ActiveSlotE Total -> Var adv 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Var base elem
C.toVar Count adv 'ActiveSlotE Total
pc Var adv 'ActiveSlotE -> Var adv 'ActiveSlotE -> Bool
forall a. Ord a => a -> a -> Bool
<= Var adv 'ActiveSlotE
0) (ExceptT (AdversarialViolation hon adv) Identity ()
 -> ExceptT (AdversarialViolation hon adv) Identity ())
-> ExceptT (AdversarialViolation hon adv) Identity ()
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a b. (a -> b) -> a -> b
$ AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a.
AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError AdversarialViolation hon adv
forall hon adv. AdversarialViolation hon adv
BadCount

  -- the youngest slot in which the adversarial schedule cannot have accelerated
  --
  -- (IE @s@ past the first active adversarial slot, or @d@ past the @k+1@st
  --  slot after the intersection)
  youngestStableA :: C.Index base SlotE
  youngestStableA :: Index base 'SlotE
youngestStableA =
    let sYoungest :: Index base 'SlotE
sYoungest = case Proxy 'Inverted
-> Vector adv 'SlotE S
-> Index adv (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound adv
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV Proxy 'Inverted
S.inverted Vector adv 'SlotE S
vA (Int -> Count adv 'ActiveSlotE Preds
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) of
          BV.JustFound Index adv 'SlotE
firstActiveA ->
            -- if s=0, then the slot of their block is the youngest stable slot
            Contains 'SlotE base adv -> Index adv 'SlotE -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index inner elem -> Index outer elem
C.fromWindow Contains 'SlotE base adv
winA (Index adv 'SlotE -> Index base 'SlotE)
-> Index adv 'SlotE -> Index base 'SlotE
forall a b. (a -> b) -> a -> b
$ Index adv 'SlotE
firstActiveA Index adv 'SlotE -> Int -> Index adv 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
s
          MaybeFound adv
BV.NothingFound ->
            -- the rest of the function won't force this since there are no
            -- adversarial active slots
            String -> Index base 'SlotE
forall a. HasCallStack => String -> a
error String
"dead code"
        kPlus1stYoungest :: Index base 'SlotE
kPlus1stYoungest = case Proxy 'Inverted
-> Vector hon 'SlotE S
-> Index hon (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound hon
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV Proxy 'Inverted
S.inverted Vector hon 'SlotE S
vH (Var hon 'ActiveSlotE -> Index hon 'ActiveSlotE
forall {kelem} base (elem :: kelem).
Var base elem -> Index base elem
C.toIndex Var hon 'ActiveSlotE
arPrefix Index hon 'ActiveSlotE -> Int -> Index hon 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
k) of
          BV.JustFound Index hon 'SlotE
kPlus1st -> Contains 'SlotE base hon -> Index hon 'SlotE -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index inner elem -> Index outer elem
C.fromWindow Contains 'SlotE base hon
winH Index hon 'SlotE
kPlus1st
          MaybeFound hon
BV.NothingFound ->
            -- If the honest fork didn't reach @k+1@ before it ended, then
            -- the conservative assumption that all slots after 'Len' are
            -- active on the honest chain implies the @k+1@st block is in
            -- slot @C.windowLast winH + (k+1-x)@, where the honest chain
            -- has @x@ remaining blocks such that @x<k+1@.
            let honestBlocksAfterIntersection :: Int
honestBlocksAfterIntersection =
                  Count hon 'ActiveSlotE Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Proxy 'NotInverted
-> Vector hon 'SlotE S
-> Size hon (PreImage 'NotInverted 'ActiveSlotE)
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S -> Size base (PreImage pol 'ActiveSlotE)
BV.countActivesInV Proxy 'NotInverted
S.notInverted Vector hon 'SlotE S
vH) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Var hon 'ActiveSlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Var hon 'ActiveSlotE
arPrefix
             in Contains 'SlotE base hon -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE base hon
winH
                  Index base 'SlotE -> Int -> Index base 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
honestBlocksAfterIntersection)
     in Index base 'SlotE -> Index base 'SlotE -> Index base 'SlotE
forall a. Ord a => a -> a -> a
max Index base 'SlotE
sYoungest (Index base 'SlotE
kPlus1stYoungest Index base 'SlotE -> Int -> Index base 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
d)

  checkRaces :: ExceptT (AdversarialViolation hon adv) Identity ()
checkRaces = do
    let iterH :: Race hon
iterH =
          Race hon -> (Race hon -> Race hon) -> Maybe (Race hon) -> Race hon
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Vector hon 'SlotE S -> Race hon
forall base. Vector base 'SlotE S -> Race base
RI.initConservative Vector hon 'SlotE S
vH) Race hon -> Race hon
forall a. a -> a
id (Maybe (Race hon) -> Race hon) -> Maybe (Race hon) -> Race hon
forall a b. (a -> b) -> a -> b
$
            Kcp -> Vector hon 'SlotE S -> Maybe (Race hon)
forall base. Kcp -> Vector base 'SlotE S -> Maybe (Race base)
RI.init (Int -> Kcp
Kcp Int
k) Vector hon 'SlotE S
vH
    case Kcp -> Vector adv 'SlotE S -> Maybe (Race adv)
forall base. Kcp -> Vector base 'SlotE S -> Maybe (Race base)
RI.init (Int -> Kcp
Kcp (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) Vector adv 'SlotE S
vA Maybe (Race adv)
-> (Race adv -> Maybe (Race adv)) -> Maybe (Race adv)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Vector adv 'SlotE S -> Race adv -> Maybe (Race adv)
forall base. Vector base 'SlotE S -> Race base -> Maybe (Race base)
RI.next Vector adv 'SlotE S
vA of
      Maybe (Race adv)
Nothing -> () -> ExceptT (AdversarialViolation hon adv) Identity ()
forall a. a -> ExceptT (AdversarialViolation hon adv) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- there are <= k total adversarial active slots
      Just Race adv
iterA ->
        -- TODO optimization: how to skip all the honest Race Windows that
        -- don't reach beyond the intersection? Perhaps skip to i - s + d?
        Race hon
-> Race adv -> ExceptT (AdversarialViolation hon adv) Identity ()
forall {m :: * -> *}.
MonadError (AdversarialViolation hon adv) m =>
Race hon -> Race adv -> m ()
go Race hon
iterH Race adv
iterA

  -- INVARIANT iterH spans k+1 active slots (possibly conservatively)
  --
  -- INVARIANT iterA spans k active slots (actually, not conservatively)
  go :: Race hon -> Race adv -> m ()
go !Race hon
iterH !Race adv
iterA = do
    C.SomeWindow Proxy raceWinH <- SomeWindow RaceLbl hon 'SlotE -> m (SomeWindow RaceLbl hon 'SlotE)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow RaceLbl hon 'SlotE
 -> m (SomeWindow RaceLbl hon 'SlotE))
-> SomeWindow RaceLbl hon 'SlotE
-> m (SomeWindow RaceLbl hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ let RI.Race SomeWindow RaceLbl hon 'SlotE
x = Race hon
iterH in SomeWindow RaceLbl hon 'SlotE
x
    C.SomeWindow Proxy raceWinA <- pure $ let RI.Race x = iterA in x

    -- lift both windows to @base@ so that they're comparable
    let raceWinH' = Contains 'SlotE base hon
-> Contains 'SlotE hon (Win RaceLbl skolem)
-> Contains 'SlotE base (Win RaceLbl skolem)
forall {kelem} (elem :: kelem) outer mid inner.
Contains elem outer mid
-> Contains elem mid inner -> Contains elem outer inner
C.joinWin Contains 'SlotE base hon
winH Contains 'SlotE hon (Win RaceLbl skolem)
raceWinH
        raceWinA' = Contains 'SlotE base adv
-> Contains 'SlotE adv (Win RaceLbl skolem)
-> Contains 'SlotE base (Win RaceLbl skolem)
forall {kelem} (elem :: kelem) outer mid inner.
Contains elem outer mid
-> Contains elem mid inner -> Contains elem outer inner
C.joinWin Contains 'SlotE base adv
winA Contains 'SlotE adv (Win RaceLbl skolem)
raceWinA

    if
      -- any Race Window that ends /after/ the adversary can accelerate is unconstrained
      | youngestStableA < C.windowLast raceWinH' C.+ d -> pure ()
      -- advance the adversarial Race Window if its start is <= the honest Race Window's start
      | C.windowStart raceWinA' <= C.windowStart raceWinH' ->
          case RI.next vA iterA of
            Just Race adv
iterA' -> Race hon -> Race adv -> m ()
go Race hon
iterH Race adv
iterA'
            Maybe (Race adv)
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- there are < k remaining adversarial active slots

      -- fail if the adversary won or tied the race
      | C.windowLast raceWinA' <= C.windowLast raceWinH' C.+ d ->
          -- iterA contains exactly k active slots, but A) it's anchored
          -- in an active slot and B) iterH contains that anchor. Thus
          -- adv has k+1 in iterH.
          Exn.throwError $
            BadRace
              AdversaryWonRace
                { rvAdv = iterA
                , rvHon = iterH
                }
      -- advance the honest Race Window
      | otherwise -> case RI.next vH iterH <|> RI.nextConservative vH iterH of
          Just Race hon
iterH' -> Race hon -> Race adv -> m ()
go Race hon
iterH' Race adv
iterA
          Maybe (Race hon)
Nothing -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- there are no remaining honest active slots
          --
          -- TODO hpc shows this never executes

  -- \| Check that the density of the adversarial schema is less than the
  -- density of the honest schema in the first stability window after the
  -- intersection and in any prefix that contains the first race to the
  -- k+1st block.
  --
  -- See description of @ensureLowerDensityInWindows@
  checkDensity :: ExceptT (AdversarialViolation hon adv) Identity ()
checkDensity = do
    let
      -- window of the honest schema after the intersection
      carWin :: Contains 'SlotE hon adv
carWin =
        Index hon 'SlotE -> Size adv 'SlotE -> Contains 'SlotE hon adv
forall kelem (elem :: kelem) outer inner.
Index outer elem -> Size inner elem -> Contains elem outer inner
C.UnsafeContains
          (Maybe (Index hon 'SlotE) -> Index hon 'SlotE
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Index hon 'SlotE) -> Index hon 'SlotE)
-> Maybe (Index hon 'SlotE) -> Index hon 'SlotE
forall a b. (a -> b) -> a -> b
$ Contains 'SlotE base hon
-> Index base 'SlotE -> Maybe (Index hon 'SlotE)
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner
-> Index outer elem -> Maybe (Index inner elem)
C.toWindow Contains 'SlotE base hon
winH (Index base 'SlotE -> Maybe (Index hon 'SlotE))
-> Index base 'SlotE -> Maybe (Index hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ Contains 'SlotE base adv -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE base adv
winA)
          (Contains 'SlotE base adv -> Size adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE base adv
winA)
      -- honest schema after the intersection
      vHAfterIntersection :: Vector adv 'SlotE S
vHAfterIntersection = Contains 'SlotE hon adv
-> Vector hon 'SlotE S -> Vector adv 'SlotE S
forall {k} a (elem :: k) outer inner.
Unbox a =>
Contains elem outer inner
-> Vector outer elem a -> Vector inner elem a
C.sliceV Contains 'SlotE hon adv
carWin Vector hon 'SlotE S
vH
      iterH :: RI.Race adv
      iterH :: Race adv
iterH =
        Race adv -> Maybe (Race adv) -> Race adv
forall a. a -> Maybe a -> a
fromMaybe (String -> Race adv
forall a. HasCallStack => String -> a
error (String -> Race adv) -> String -> Race adv
forall a b. (a -> b) -> a -> b
$ String
"there should be k+1 active slots after the intersection k=" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k) (Maybe (Race adv) -> Race adv) -> Maybe (Race adv) -> Race adv
forall a b. (a -> b) -> a -> b
$
          Kcp -> Vector adv 'SlotE S -> Maybe (Race adv)
forall base. Kcp -> Vector base 'SlotE S -> Maybe (Race base)
RI.init (Int -> Kcp
Kcp Int
k) Vector adv 'SlotE S
vHAfterIntersection

    -- first race window after the intersection
    C.SomeWindow pw0 w0 <- let RI.Race SomeWindow RaceLbl adv 'SlotE
x = Race adv
iterH in SomeWindow RaceLbl adv 'SlotE
-> ExceptT
     (AdversarialViolation hon adv)
     Identity
     (SomeWindow RaceLbl adv 'SlotE)
forall a. a -> ExceptT (AdversarialViolation hon adv) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeWindow RaceLbl adv 'SlotE
x

    let
      w0' = Contains 'SlotE adv (Win RaceLbl skolem)
-> Size (Win RaceLbl skolem) 'SlotE
-> Contains 'SlotE adv (Win RaceLbl skolem)
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner
-> Size inner elem -> Contains elem outer inner
C.truncateWin Contains 'SlotE adv (Win RaceLbl skolem)
w0 (Int -> Size (Win RaceLbl skolem) 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
s)
      vvH = Vector adv 'SlotE S -> Vector S
forall {k1} {k2} (base :: k1) (elem :: k2) a.
Vector base elem a -> Vector a
C.getVector Vector adv 'SlotE S
vHAfterIntersection
      vvA = Vector adv 'SlotE S -> Vector S
forall {k1} {k2} (base :: k1) (elem :: k2) a.
Vector base elem a -> Vector a
C.getVector Vector adv 'SlotE S
vA
      -- cumulative sums of active slots per slot after the intersection
      hSum = (Int -> Int -> Int) -> Int -> Vector Int -> Vector Int
forall a b.
(Unbox a, Unbox b) =>
(a -> b -> a) -> a -> Vector b -> Vector a
Vector.scanl Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Int
0 ((S -> Int) -> Vector S -> Vector Int
forall a b. (Unbox a, Unbox b) => (a -> b) -> Vector a -> Vector b
Vector.map (\S
x -> if Proxy 'NotInverted -> S -> Bool
forall (pol :: Pol) (proxy :: Pol -> *).
POL pol =>
proxy pol -> S -> Bool
forall (proxy :: Pol -> *). proxy 'NotInverted -> S -> Bool
S.test Proxy 'NotInverted
S.notInverted S
x then Int
1 else Int
0) Vector S
vvH)
      aSum = (Int -> Int -> Int) -> Int -> Vector Int -> Vector Int
forall a b.
(Unbox a, Unbox b) =>
(a -> b -> a) -> a -> Vector b -> Vector a
Vector.scanl Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) Int
0 ((S -> Int) -> Vector S -> Vector Int
forall a b. (Unbox a, Unbox b) => (a -> b) -> Vector a -> Vector b
Vector.map (\S
x -> if Proxy 'NotInverted -> S -> Bool
forall (pol :: Pol) (proxy :: Pol -> *).
POL pol =>
proxy pol -> S -> Bool
forall (proxy :: Pol -> *). proxy 'NotInverted -> S -> Bool
S.test Proxy 'NotInverted
S.notInverted S
x then Int
1 else Int
0) Vector S
vvA)
      -- cumulative sums of active slots per slot until the first stability
      -- window after the intersection
      hwSum = Vector Int -> [Int]
forall a. Unbox a => Vector a -> [a]
Vector.toList (Vector Int -> [Int]) -> Vector Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> Vector Int -> Vector Int
forall a. Unbox a => Int -> Vector a -> Vector a
Vector.drop (Size (Win RaceLbl skolem) 'SlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Size (Win RaceLbl skolem) 'SlotE -> Int)
-> Size (Win RaceLbl skolem) 'SlotE -> Int
forall a b. (a -> b) -> a -> b
$ Contains 'SlotE adv (Win RaceLbl skolem)
-> Size (Win RaceLbl skolem) 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE adv (Win RaceLbl skolem)
w0') (Vector Int -> Vector Int) -> Vector Int -> Vector Int
forall a b. (a -> b) -> a -> b
$ Int -> Vector Int -> Vector Int
forall a. Unbox a => Int -> Vector a -> Vector a
Vector.take (Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Vector Int
hSum
      awSum = Vector Int -> [Int]
forall a. Unbox a => Vector a -> [a]
Vector.toList (Vector Int -> [Int]) -> Vector Int -> [Int]
forall a b. (a -> b) -> a -> b
$ Int -> Vector Int -> Vector Int
forall a. Unbox a => Int -> Vector a -> Vector a
Vector.drop (Size (Win RaceLbl skolem) 'SlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Size (Win RaceLbl skolem) 'SlotE -> Int)
-> Size (Win RaceLbl skolem) 'SlotE -> Int
forall a b. (a -> b) -> a -> b
$ Contains 'SlotE adv (Win RaceLbl skolem)
-> Size (Win RaceLbl skolem) 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE adv (Win RaceLbl skolem)
w0') (Vector Int -> Vector Int) -> Vector Int -> Vector Int
forall a b. (a -> b) -> a -> b
$ Int -> Vector Int -> Vector Int
forall a. Unbox a => Int -> Vector a -> Vector a
Vector.take (Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Vector Int
aSum
    case [cmp | cmp@(_, (x, y)) <- zip [0 ..] (zip hwSum awSum), x <= y] of
      [] -> () -> ExceptT (AdversarialViolation hon adv) Identity ()
forall a. a -> ExceptT (AdversarialViolation hon adv) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      ((Int
i, (Int
x, Int
y)) : [(Int, (Int, Int))]
_) ->
        let
          w0'' :: Contains 'SlotE adv (Win RaceLbl skolem)
w0'' = Index adv 'SlotE
-> Size (Win RaceLbl skolem) 'SlotE
-> Contains 'SlotE adv (Win RaceLbl skolem)
forall kelem (elem :: kelem) outer inner.
Index outer elem -> Size inner elem -> Contains elem outer inner
C.UnsafeContains (Contains 'SlotE adv (Win RaceLbl skolem) -> Index adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE adv (Win RaceLbl skolem)
w0') (Contains 'SlotE adv (Win RaceLbl skolem)
-> Size (Win RaceLbl skolem) 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE adv (Win RaceLbl skolem)
w0' Size (Win RaceLbl skolem) 'SlotE
-> Int -> Size (Win RaceLbl skolem) 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
i)
         in
          AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a.
AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError (AdversarialViolation hon adv
 -> ExceptT (AdversarialViolation hon adv) Identity ())
-> AdversarialViolation hon adv
-> ExceptT (AdversarialViolation hon adv) Identity ()
forall a b. (a -> b) -> a -> b
$ SomeWindow RaceLbl adv 'SlotE
-> Int -> Int -> AdversarialViolation hon adv
forall hon adv.
SomeWindow RaceLbl adv 'SlotE
-> Int -> Int -> AdversarialViolation hon adv
BadDensity (Proxy skolem
-> Contains 'SlotE adv (Win RaceLbl skolem)
-> SomeWindow RaceLbl adv 'SlotE
forall klbl kelem (lbl :: klbl) outer (elem :: kelem) skolem.
Proxy skolem
-> Contains elem outer (Win lbl skolem)
-> SomeWindow lbl outer elem
C.SomeWindow Proxy skolem
pw0 Contains 'SlotE adv (Win RaceLbl skolem)
w0'') Int
x Int
y

-----

-- | Named arguments for 'checkAdversarialRecipe'
data AdversarialRecipe base hon
  = AdversarialRecipe
  { forall base hon. AdversarialRecipe base hon -> ChainSchema base hon
arHonest :: !(ChainSchema base hon)
  -- ^ The honest chain to branch off of
  , forall base hon. AdversarialRecipe base hon -> (Kcp, Scg, Delta)
arParams :: (Kcp, Scg, Delta)
  -- ^ protocol parameters
  , forall base hon. AdversarialRecipe base hon -> Var hon 'ActiveSlotE
arPrefix :: !(C.Var hon ActiveSlotE)
  -- ^ Where to branch off of 'arHonest'
  --
  -- It is the amount of blocks shared by the honest and the adversarial
  -- chain. In other words, the 0-based index of their intersection
  -- in blocks, such that
  --
  -- * @0@ identifies the genesis block
  -- * @1@ identifies the first block in arHonest
  -- * @2@ identifies the second block in arHonest
  -- * etc
  }
  deriving (AdversarialRecipe base hon -> AdversarialRecipe base hon -> Bool
(AdversarialRecipe base hon -> AdversarialRecipe base hon -> Bool)
-> (AdversarialRecipe base hon
    -> AdversarialRecipe base hon -> Bool)
-> Eq (AdversarialRecipe base hon)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall base hon.
AdversarialRecipe base hon -> AdversarialRecipe base hon -> Bool
$c== :: forall base hon.
AdversarialRecipe base hon -> AdversarialRecipe base hon -> Bool
== :: AdversarialRecipe base hon -> AdversarialRecipe base hon -> Bool
$c/= :: forall base hon.
AdversarialRecipe base hon -> AdversarialRecipe base hon -> Bool
/= :: AdversarialRecipe base hon -> AdversarialRecipe base hon -> Bool
Eq, ReadPrec [AdversarialRecipe base hon]
ReadPrec (AdversarialRecipe base hon)
Int -> ReadS (AdversarialRecipe base hon)
ReadS [AdversarialRecipe base hon]
(Int -> ReadS (AdversarialRecipe base hon))
-> ReadS [AdversarialRecipe base hon]
-> ReadPrec (AdversarialRecipe base hon)
-> ReadPrec [AdversarialRecipe base hon]
-> Read (AdversarialRecipe base hon)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall base hon. ReadPrec [AdversarialRecipe base hon]
forall base hon. ReadPrec (AdversarialRecipe base hon)
forall base hon. Int -> ReadS (AdversarialRecipe base hon)
forall base hon. ReadS [AdversarialRecipe base hon]
$creadsPrec :: forall base hon. Int -> ReadS (AdversarialRecipe base hon)
readsPrec :: Int -> ReadS (AdversarialRecipe base hon)
$creadList :: forall base hon. ReadS [AdversarialRecipe base hon]
readList :: ReadS [AdversarialRecipe base hon]
$creadPrec :: forall base hon. ReadPrec (AdversarialRecipe base hon)
readPrec :: ReadPrec (AdversarialRecipe base hon)
$creadListPrec :: forall base hon. ReadPrec [AdversarialRecipe base hon]
readListPrec :: ReadPrec [AdversarialRecipe base hon]
Read, Int -> AdversarialRecipe base hon -> ShowS
[AdversarialRecipe base hon] -> ShowS
AdversarialRecipe base hon -> String
(Int -> AdversarialRecipe base hon -> ShowS)
-> (AdversarialRecipe base hon -> String)
-> ([AdversarialRecipe base hon] -> ShowS)
-> Show (AdversarialRecipe base hon)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall base hon. Int -> AdversarialRecipe base hon -> ShowS
forall base hon. [AdversarialRecipe base hon] -> ShowS
forall base hon. AdversarialRecipe base hon -> String
$cshowsPrec :: forall base hon. Int -> AdversarialRecipe base hon -> ShowS
showsPrec :: Int -> AdversarialRecipe base hon -> ShowS
$cshow :: forall base hon. AdversarialRecipe base hon -> String
show :: AdversarialRecipe base hon -> String
$cshowList :: forall base hon. [AdversarialRecipe base hon] -> ShowS
showList :: [AdversarialRecipe base hon] -> ShowS
Show)

-- | See 'CheckedAdversarialRecipe'
data SomeCheckedAdversarialRecipe base hon
  = forall adv.
    SomeCheckedAdversarialRecipe
      !(Proxy adv)
      !(CheckedAdversarialRecipe base hon adv)

instance Show (SomeCheckedAdversarialRecipe base hon) where
  showsPrec :: Int -> SomeCheckedAdversarialRecipe base hon -> ShowS
showsPrec Int
p (SomeCheckedAdversarialRecipe Proxy adv
adv CheckedAdversarialRecipe base hon adv
car) =
    Int -> ShowBuilder (SomeCheckedAdversarialRecipe base hon) -> ShowS
forall a.
NoFun "runShowsPrec" a (AbsError "runShowsPrec" a) =>
Int -> ShowBuilder a -> ShowS
Some.runShowsPrec Int
p (ShowBuilder (SomeCheckedAdversarialRecipe base hon) -> ShowS)
-> ShowBuilder (SomeCheckedAdversarialRecipe base hon) -> ShowS
forall a b. (a -> b) -> a -> b
$
      (Proxy adv
 -> CheckedAdversarialRecipe base hon adv
 -> SomeCheckedAdversarialRecipe base hon)
-> String
-> ShowBuilder
     (Proxy adv
      -> CheckedAdversarialRecipe base hon adv
      -> SomeCheckedAdversarialRecipe base hon)
forall a. a -> String -> ShowBuilder a
Some.showCtor Proxy adv
-> CheckedAdversarialRecipe base hon adv
-> SomeCheckedAdversarialRecipe base hon
forall base hon adv.
Proxy adv
-> CheckedAdversarialRecipe base hon adv
-> SomeCheckedAdversarialRecipe base hon
SomeCheckedAdversarialRecipe String
"SomeCheckedAdversarialRecipe"
        ShowBuilder
  (Proxy adv
   -> CheckedAdversarialRecipe base hon adv
   -> SomeCheckedAdversarialRecipe base hon)
-> Proxy adv
-> ShowBuilder
     (CheckedAdversarialRecipe base hon adv
      -> SomeCheckedAdversarialRecipe base hon)
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` Proxy adv
adv
        ShowBuilder
  (CheckedAdversarialRecipe base hon adv
   -> SomeCheckedAdversarialRecipe base hon)
-> CheckedAdversarialRecipe base hon adv
-> ShowBuilder (SomeCheckedAdversarialRecipe base hon)
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` CheckedAdversarialRecipe base hon adv
car

instance Read (SomeCheckedAdversarialRecipe base hon) where
  readPrec :: ReadPrec (SomeCheckedAdversarialRecipe base hon)
readPrec =
    ReadBuilder (SomeCheckedAdversarialRecipe base hon)
-> ReadPrec (SomeCheckedAdversarialRecipe base hon)
forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
Some.runReadPrec (ReadBuilder (SomeCheckedAdversarialRecipe base hon)
 -> ReadPrec (SomeCheckedAdversarialRecipe base hon))
-> ReadBuilder (SomeCheckedAdversarialRecipe base hon)
-> ReadPrec (SomeCheckedAdversarialRecipe base hon)
forall a b. (a -> b) -> a -> b
$
      (Proxy (ZonkAny 0)
 -> CheckedAdversarialRecipe base hon (ZonkAny 0)
 -> SomeCheckedAdversarialRecipe base hon)
-> String
-> ReadBuilder
     (Proxy (ZonkAny 0)
      -> CheckedAdversarialRecipe base hon (ZonkAny 0)
      -> SomeCheckedAdversarialRecipe base hon)
forall a. a -> String -> ReadBuilder a
Some.readCtor Proxy (ZonkAny 0)
-> CheckedAdversarialRecipe base hon (ZonkAny 0)
-> SomeCheckedAdversarialRecipe base hon
forall base hon adv.
Proxy adv
-> CheckedAdversarialRecipe base hon adv
-> SomeCheckedAdversarialRecipe base hon
SomeCheckedAdversarialRecipe String
"SomeCheckedAdversarialRecipe"
        ReadBuilder
  (Proxy (ZonkAny 0)
   -> CheckedAdversarialRecipe base hon (ZonkAny 0)
   -> SomeCheckedAdversarialRecipe base hon)
-> ReadBuilder (Proxy (ZonkAny 0))
-> ReadBuilder
     (CheckedAdversarialRecipe base hon (ZonkAny 0)
      -> SomeCheckedAdversarialRecipe base hon)
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (Proxy (ZonkAny 0))
forall a. Read a => ReadBuilder a
Some.readArg
        ReadBuilder
  (CheckedAdversarialRecipe base hon (ZonkAny 0)
   -> SomeCheckedAdversarialRecipe base hon)
-> ReadBuilder (CheckedAdversarialRecipe base hon (ZonkAny 0))
-> ReadBuilder (SomeCheckedAdversarialRecipe base hon)
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (CheckedAdversarialRecipe base hon (ZonkAny 0))
forall a. Read a => ReadBuilder a
Some.readArg

-- | Image of 'checkAdversarialRecipe' when it accepts the recipe
data CheckedAdversarialRecipe base hon adv
  = UnsafeCheckedAdversarialRecipe
  { forall base hon adv.
CheckedAdversarialRecipe base hon adv -> ChainSchema base hon
carHonest :: !(ChainSchema base hon)
  -- ^ The honest chain to branch off of
  , forall base hon adv.
CheckedAdversarialRecipe base hon adv -> (Kcp, Scg, Delta)
carParams :: (Kcp, Scg, Delta)
  -- ^ protocol parameters
  , forall base hon adv.
CheckedAdversarialRecipe base hon adv -> Contains 'SlotE hon adv
carWin :: !(C.Contains SlotE hon adv)
  -- ^ The window starting at the first slot after the intersection
  -- and ending at the last slot of 'carHonest'.
  --
  -- INVARIANT: there is at least one active honest slot in @adv@
  --
  -- In other words, the adversarial leader schedule does not /extend/ the
  -- chain represented by 'carHonest', it competes with it.
  }
  deriving (CheckedAdversarialRecipe base hon adv
-> CheckedAdversarialRecipe base hon adv -> Bool
(CheckedAdversarialRecipe base hon adv
 -> CheckedAdversarialRecipe base hon adv -> Bool)
-> (CheckedAdversarialRecipe base hon adv
    -> CheckedAdversarialRecipe base hon adv -> Bool)
-> Eq (CheckedAdversarialRecipe base hon adv)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall base hon adv.
CheckedAdversarialRecipe base hon adv
-> CheckedAdversarialRecipe base hon adv -> Bool
$c== :: forall base hon adv.
CheckedAdversarialRecipe base hon adv
-> CheckedAdversarialRecipe base hon adv -> Bool
== :: CheckedAdversarialRecipe base hon adv
-> CheckedAdversarialRecipe base hon adv -> Bool
$c/= :: forall base hon adv.
CheckedAdversarialRecipe base hon adv
-> CheckedAdversarialRecipe base hon adv -> Bool
/= :: CheckedAdversarialRecipe base hon adv
-> CheckedAdversarialRecipe base hon adv -> Bool
Eq, ReadPrec [CheckedAdversarialRecipe base hon adv]
ReadPrec (CheckedAdversarialRecipe base hon adv)
Int -> ReadS (CheckedAdversarialRecipe base hon adv)
ReadS [CheckedAdversarialRecipe base hon adv]
(Int -> ReadS (CheckedAdversarialRecipe base hon adv))
-> ReadS [CheckedAdversarialRecipe base hon adv]
-> ReadPrec (CheckedAdversarialRecipe base hon adv)
-> ReadPrec [CheckedAdversarialRecipe base hon adv]
-> Read (CheckedAdversarialRecipe base hon adv)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall base hon adv.
ReadPrec [CheckedAdversarialRecipe base hon adv]
forall base hon adv.
ReadPrec (CheckedAdversarialRecipe base hon adv)
forall base hon adv.
Int -> ReadS (CheckedAdversarialRecipe base hon adv)
forall base hon adv. ReadS [CheckedAdversarialRecipe base hon adv]
$creadsPrec :: forall base hon adv.
Int -> ReadS (CheckedAdversarialRecipe base hon adv)
readsPrec :: Int -> ReadS (CheckedAdversarialRecipe base hon adv)
$creadList :: forall base hon adv. ReadS [CheckedAdversarialRecipe base hon adv]
readList :: ReadS [CheckedAdversarialRecipe base hon adv]
$creadPrec :: forall base hon adv.
ReadPrec (CheckedAdversarialRecipe base hon adv)
readPrec :: ReadPrec (CheckedAdversarialRecipe base hon adv)
$creadListPrec :: forall base hon adv.
ReadPrec [CheckedAdversarialRecipe base hon adv]
readListPrec :: ReadPrec [CheckedAdversarialRecipe base hon adv]
Read, Int -> CheckedAdversarialRecipe base hon adv -> ShowS
[CheckedAdversarialRecipe base hon adv] -> ShowS
CheckedAdversarialRecipe base hon adv -> String
(Int -> CheckedAdversarialRecipe base hon adv -> ShowS)
-> (CheckedAdversarialRecipe base hon adv -> String)
-> ([CheckedAdversarialRecipe base hon adv] -> ShowS)
-> Show (CheckedAdversarialRecipe base hon adv)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall base hon adv.
Int -> CheckedAdversarialRecipe base hon adv -> ShowS
forall base hon adv.
[CheckedAdversarialRecipe base hon adv] -> ShowS
forall base hon adv.
CheckedAdversarialRecipe base hon adv -> String
$cshowsPrec :: forall base hon adv.
Int -> CheckedAdversarialRecipe base hon adv -> ShowS
showsPrec :: Int -> CheckedAdversarialRecipe base hon adv -> ShowS
$cshow :: forall base hon adv.
CheckedAdversarialRecipe base hon adv -> String
show :: CheckedAdversarialRecipe base hon adv -> String
$cshowList :: forall base hon adv.
[CheckedAdversarialRecipe base hon adv] -> ShowS
showList :: [CheckedAdversarialRecipe base hon adv] -> ShowS
Show)

-- | Image of 'checkAdversarialRecipe' when it rejects the recipe
data NoSuchAdversarialChainSchema
  = -- | There is no slot the adversary can lead
    --
    -- Two possible reasons, where @X@ is the slot of 'arPrefix' and Y is the youngest slot of 'arHonest'.
    --
    --    * The interval @[X, Y)@ is empty.
    --
    --    * @k=0@
    --
    -- Suppose k=0 and slot x and slot y are two honest active slots with only
    -- honest empty slots between them.
    --
    -- Length of Competing Chains prohibits the adversary from leading in the interval (x,y].
    --
    -- In fact, by induction, the adversary can never lead: suppose the same y
    -- and a slot z are two honest active slots with only honest empty slots
    -- between them...
    NoSuchAdversarialBlock
  | -- | @not ('arPrefix' < C)@ where @C@ is the number of active slots in 'arHonest'
    NoSuchCompetitor
  | -- | @not (0 <= 'arPrefix' <= C)@ where @C@ is the number of active slots in 'arHonest'
    NoSuchIntersection
  deriving (NoSuchAdversarialChainSchema
-> NoSuchAdversarialChainSchema -> Bool
(NoSuchAdversarialChainSchema
 -> NoSuchAdversarialChainSchema -> Bool)
-> (NoSuchAdversarialChainSchema
    -> NoSuchAdversarialChainSchema -> Bool)
-> Eq NoSuchAdversarialChainSchema
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NoSuchAdversarialChainSchema
-> NoSuchAdversarialChainSchema -> Bool
== :: NoSuchAdversarialChainSchema
-> NoSuchAdversarialChainSchema -> Bool
$c/= :: NoSuchAdversarialChainSchema
-> NoSuchAdversarialChainSchema -> Bool
/= :: NoSuchAdversarialChainSchema
-> NoSuchAdversarialChainSchema -> Bool
Eq, Int -> NoSuchAdversarialChainSchema -> ShowS
[NoSuchAdversarialChainSchema] -> ShowS
NoSuchAdversarialChainSchema -> String
(Int -> NoSuchAdversarialChainSchema -> ShowS)
-> (NoSuchAdversarialChainSchema -> String)
-> ([NoSuchAdversarialChainSchema] -> ShowS)
-> Show NoSuchAdversarialChainSchema
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NoSuchAdversarialChainSchema -> ShowS
showsPrec :: Int -> NoSuchAdversarialChainSchema -> ShowS
$cshow :: NoSuchAdversarialChainSchema -> String
show :: NoSuchAdversarialChainSchema -> String
$cshowList :: [NoSuchAdversarialChainSchema] -> ShowS
showList :: [NoSuchAdversarialChainSchema] -> ShowS
Show)

-----

-- | The suffix of the slots starting strictly /after/ the intersection
data AdvLbl

-- | The interval of slots that have most recently attained their final value
data SettledLbl

-- | Reject a bad 'AdversarialRecipe'
checkAdversarialRecipe ::
  forall base hon.
  AdversarialRecipe base hon ->
  Exn.Except
    NoSuchAdversarialChainSchema
    (SomeCheckedAdversarialRecipe base hon)
checkAdversarialRecipe :: forall base hon.
AdversarialRecipe base hon
-> Except
     NoSuchAdversarialChainSchema
     (SomeCheckedAdversarialRecipe base hon)
checkAdversarialRecipe AdversarialRecipe base hon
recipe = do
  Bool
-> ExceptT NoSuchAdversarialChainSchema Identity ()
-> ExceptT NoSuchAdversarialChainSchema Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
0 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
k) (ExceptT NoSuchAdversarialChainSchema Identity ()
 -> ExceptT NoSuchAdversarialChainSchema Identity ())
-> ExceptT NoSuchAdversarialChainSchema Identity ()
-> ExceptT NoSuchAdversarialChainSchema Identity ()
forall a b. (a -> b) -> a -> b
$ NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity ()
forall a.
NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError NoSuchAdversarialChainSchema
NoSuchAdversarialBlock

  -- validate 'arPrefix'
  firstAdvSlot <- case Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Var hon 'ActiveSlotE
arPrefix Var hon 'ActiveSlotE
0 of
    Ordering
LT -> NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity (Index hon 'SlotE)
forall a.
NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError NoSuchAdversarialChainSchema
NoSuchIntersection
    Ordering
EQ -> Index hon 'SlotE
-> ExceptT NoSuchAdversarialChainSchema Identity (Index hon 'SlotE)
forall a. a -> ExceptT NoSuchAdversarialChainSchema Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Index hon 'SlotE
 -> ExceptT
      NoSuchAdversarialChainSchema Identity (Index hon 'SlotE))
-> Index hon 'SlotE
-> ExceptT NoSuchAdversarialChainSchema Identity (Index hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ Int -> Index hon 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0
    Ordering
GT -> case Proxy 'Inverted
-> Vector hon 'SlotE S
-> Index hon (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound hon
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV Proxy 'Inverted
S.inverted Vector hon 'SlotE S
vH (Index hon (PreImage 'Inverted 'EmptySlotE) -> MaybeFound hon)
-> Index hon (PreImage 'Inverted 'EmptySlotE) -> MaybeFound hon
forall a b. (a -> b) -> a -> b
$ Var hon (PreImage 'Inverted 'EmptySlotE)
-> Index hon (PreImage 'Inverted 'EmptySlotE)
forall {kelem} base (elem :: kelem).
Var base elem -> Index base elem
C.toIndex (Var hon (PreImage 'Inverted 'EmptySlotE)
 -> Index hon (PreImage 'Inverted 'EmptySlotE))
-> Var hon (PreImage 'Inverted 'EmptySlotE)
-> Index hon (PreImage 'Inverted 'EmptySlotE)
forall a b. (a -> b) -> a -> b
$ Var hon 'ActiveSlotE
arPrefix Var hon 'ActiveSlotE
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. Num a => a -> a -> a
- Var hon 'ActiveSlotE
1 of
      MaybeFound hon
BV.NothingFound -> NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity (Index hon 'SlotE)
forall a.
NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError NoSuchAdversarialChainSchema
NoSuchIntersection
      BV.JustFound Index hon 'SlotE
x -> do
        Bool
-> ExceptT NoSuchAdversarialChainSchema Identity ()
-> ExceptT NoSuchAdversarialChainSchema Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Index hon 'SlotE
x Index hon 'SlotE -> Index hon 'SlotE -> Bool
forall a. Eq a => a -> a -> Bool
== Size hon 'SlotE -> Index hon 'SlotE
forall {kelem} base (elem :: kelem).
Size base elem -> Index base elem
C.lastIndex (Contains 'SlotE base hon -> Size hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE base hon
winH)) (ExceptT NoSuchAdversarialChainSchema Identity ()
 -> ExceptT NoSuchAdversarialChainSchema Identity ())
-> ExceptT NoSuchAdversarialChainSchema Identity ()
-> ExceptT NoSuchAdversarialChainSchema Identity ()
forall a b. (a -> b) -> a -> b
$ NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity ()
forall a.
NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError NoSuchAdversarialChainSchema
NoSuchAdversarialBlock
        Index hon 'SlotE
-> ExceptT NoSuchAdversarialChainSchema Identity (Index hon 'SlotE)
forall a. a -> ExceptT NoSuchAdversarialChainSchema Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Index hon 'SlotE
x Index hon 'SlotE -> Int -> Index hon 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
1)

  C.SomeWindow Proxy winA <-
    pure $ C.withSuffixWindow (C.windowSize winH) (C.Lbl @AdvLbl) firstAdvSlot

  -- there must be at least one honest active slot in @adv@
  case BV.findIthEmptyInV S.inverted (C.sliceV winA vH) (C.Count 0) of
    MaybeFound (Win AdvLbl skolem)
BV.NothingFound -> NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity ()
forall a.
NoSuchAdversarialChainSchema
-> ExceptT NoSuchAdversarialChainSchema Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError NoSuchAdversarialChainSchema
NoSuchCompetitor
    BV.JustFound{} -> () -> ExceptT NoSuchAdversarialChainSchema Identity ()
forall a. a -> ExceptT NoSuchAdversarialChainSchema Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  pure $
    SomeCheckedAdversarialRecipe Proxy $
      UnsafeCheckedAdversarialRecipe
        { carHonest = arHonest
        , carParams = arParams
        , carWin = winA
        }
 where
  AdversarialRecipe
    { ChainSchema base hon
arHonest :: forall base hon. AdversarialRecipe base hon -> ChainSchema base hon
arHonest :: ChainSchema base hon
arHonest
    , (Kcp, Scg, Delta)
arParams :: forall base hon. AdversarialRecipe base hon -> (Kcp, Scg, Delta)
arParams :: (Kcp, Scg, Delta)
arParams
    , Var hon 'ActiveSlotE
arPrefix :: forall base hon. AdversarialRecipe base hon -> Var hon 'ActiveSlotE
arPrefix :: Var hon 'ActiveSlotE
arPrefix
    } = AdversarialRecipe base hon
recipe

  (Kcp Int
k, Scg
_scg, Delta
_delta) = (Kcp, Scg, Delta)
arParams

  ChainSchema Contains 'SlotE base hon
winH Vector hon 'SlotE S
vH = ChainSchema base hon
arHonest

-----

data RaceAssumptionLbl
data UntouchableLbl
data TouchableLbl

-- | Generate an adversarial 'ChainSchema' that satifies 'checkExtendedRaceAssumption'
--
-- The distribution this function samples from is not simple to describe. It
-- begins by drawing a sample of length 'adv' from the Bernoulli process
-- induced by the active slot coefficient 'Asc'. (IE 'adv' many i.i.d. samples
-- from @Uniform(f)@). Then it visits the Extended Praos Race Windows that
-- overlap with the prefix of that leader schedule that ends one stability
-- window after the first (remaining) active adversarial slot in it. In each
-- such Window, it removes the youngest active slots from the adversarial
-- leader schedule until it loses that Race.
--
-- Finally, it ensures that the density of the alternative schema is
-- less than the density of the honest schema in the first stability window
-- after the intersection.
uniformAdversarialChain ::
  forall g base hon adv.
  R.RandomGen g =>
  -- | 'Nothing' means @1@
  Maybe Asc ->
  CheckedAdversarialRecipe base hon adv ->
  g ->
  ChainSchema base adv
{-# INLINEABLE uniformAdversarialChain #-}
uniformAdversarialChain :: forall g base hon adv.
RandomGen g =>
Maybe Asc
-> CheckedAdversarialRecipe base hon adv
-> g
-> ChainSchema base adv
uniformAdversarialChain Maybe Asc
mbAsc CheckedAdversarialRecipe base hon adv
recipe g
g0 = Vector adv 'SlotE S -> ChainSchema base adv
wrap (Vector adv 'SlotE S -> ChainSchema base adv)
-> Vector adv 'SlotE S -> ChainSchema base adv
forall a b. (a -> b) -> a -> b
$ (forall s. ST s (MVector adv 'SlotE s S)) -> Vector adv 'SlotE S
forall {k1} {k2} a (base :: k1) (elem :: k2).
Unbox a =>
(forall s. ST s (MVector base elem s a)) -> Vector base elem a
C.createV ((forall s. ST s (MVector adv 'SlotE s S)) -> Vector adv 'SlotE S)
-> (forall s. ST s (MVector adv 'SlotE s S)) -> Vector adv 'SlotE S
forall a b. (a -> b) -> a -> b
$ do
  g <- g -> ST s (STGenM g s)
forall g s. g -> ST s (STGenM g s)
R.newSTGenM g
g0

  let sz = Contains 'SlotE hon adv -> Count adv 'SlotE Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE hon adv
carWin :: C.Size adv SlotE

  -- randomly initialize the bitstring
  mv <- C.replicateMV sz $ case mbAsc of
    Maybe Asc
Nothing -> S -> ST s S
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (S -> ST s S) -> S -> ST s S
forall a b. (a -> b) -> a -> b
$ Proxy 'NotInverted -> S
forall (pol :: Pol) (proxy :: Pol -> *). POL pol => proxy pol -> S
forall (proxy :: Pol -> *). proxy 'NotInverted -> S
S.mkActive Proxy 'NotInverted
S.notInverted
    Just Asc
asc -> Asc -> g -> (S, g)
forall g. RandomGen g => Asc -> g -> (S, g)
S.genS Asc
asc (g -> (S, g)) -> STGenM g s -> ST s S
forall g a s. (g -> (a, g)) -> STGenM g s -> ST s a
`R.applySTGen` STGenM g s
g

  -- ensure the adversarial leader schedule is not empty
  do
    -- Since the first active slot in the adversarial chain might determine
    -- the position of the acceleration bound, we ensure it is early enough
    -- so we can always fit k+1 blocks in the alternative schema.
    --
    -- There will be at least k unstable slots at the end, plus one more
    -- active slot a stability window earlier.
    -- See Note [Minimum schema length] in "Test.Ouroboros.Consensus.ChainGenerator.Honest"
    -- for the rationale.
    let trailingSlots = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k
        szFirstActive = Count adv 'SlotE Total
sz Count adv 'SlotE Total -> Int -> Count adv 'SlotE Total
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.- Int
trailingSlots
    when (szFirstActive <= C.Count 0) $
      error "the adversarial schema length should be greater than s+k"
    void $
      BV.fillInWindow
        S.notInverted
        (BV.SomeDensityWindow (C.Count 1) szFirstActive)
        g
        (C.sliceMV (C.UnsafeContains (C.Count 0) szFirstActive) mv)

  -- find the slot of the k+1 honest block
  let kPlus1st :: C.Index adv SlotE
      kPlus1st = case Proxy 'Inverted
-> Vector adv 'SlotE S
-> Index adv (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound adv
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S
-> Index base (PreImage pol 'EmptySlotE)
-> MaybeFound base
BV.findIthEmptyInV Proxy 'Inverted
S.inverted (Contains 'SlotE hon adv
-> Vector hon 'SlotE S -> Vector adv 'SlotE S
forall {k} a (elem :: k) outer inner.
Unbox a =>
Contains elem outer inner
-> Vector outer elem a -> Vector inner elem a
C.sliceV Contains 'SlotE hon adv
carWin Vector hon 'SlotE S
vH) (Int -> Count adv 'ActiveSlotE Preds
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
k) of
        MaybeFound adv
BV.NothingFound -> Index adv 'SlotE
-> (Index adv 'SlotE -> Index adv 'SlotE)
-> Maybe (Index adv 'SlotE)
-> Index adv 'SlotE
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (String -> Index adv 'SlotE
forall a. HasCallStack => String -> a
error String
"dead code") Index adv 'SlotE -> Index adv 'SlotE
forall a. a -> a
id (Maybe (Index adv 'SlotE) -> Index adv 'SlotE)
-> Maybe (Index adv 'SlotE) -> Index adv 'SlotE
forall a b. (a -> b) -> a -> b
$ Contains 'SlotE hon adv
-> Index hon 'SlotE -> Maybe (Index adv 'SlotE)
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner
-> Index outer elem -> Maybe (Index inner elem)
C.toWindow Contains 'SlotE hon adv
carWin (Index hon 'SlotE -> Maybe (Index adv 'SlotE))
-> Index hon 'SlotE -> Maybe (Index adv 'SlotE)
forall a b. (a -> b) -> a -> b
$ Contains 'SlotE hon adv -> Index hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE hon adv
carWin
        BV.JustFound Index adv 'SlotE
x -> Index adv 'SlotE
x

  -- ensure the adversarial leader schedule does not win any of the races for
  -- which the honest Race Window fits within the Stability Window anchored at
  -- the first adversarial active slot
  --
  -- TODO Why is it ok to skip early honest races, some of which overlap with
  -- @adv@? Is it because not having >k in some prefix [0, n] of adv ensures
  -- you can't have >k in the interval [0, C.frWindow adv n] either?
  let iterH :: RI.Race adv
      iterH =
        Race adv -> Maybe (Race adv) -> Race adv
forall a. a -> Maybe a -> a
fromMaybe (String -> Race adv
forall a. HasCallStack => String -> a
error String
"there should be k+1 active slots after the intersection") (Maybe (Race adv) -> Race adv) -> Maybe (Race adv) -> Race adv
forall a b. (a -> b) -> a -> b
$
          Kcp -> Vector adv 'SlotE S -> Maybe (Race adv)
forall base. Kcp -> Vector base 'SlotE S -> Maybe (Race base)
RI.init Kcp
kcp Vector adv 'SlotE S
vHAfterIntersection

  -- We don't want to change the first active slot in the adversarial chain
  -- Otherwise, we can't predict the position of the acceleration bound.
  firstActive <-
    BV.findIthEmptyInMV S.inverted mv (C.Count 0) >>= \case
      MaybeFound adv
BV.NothingFound -> String -> ST s (Index adv 'SlotE)
forall a. HasCallStack => String -> a
error String
"the adversarial schema is empty"
      BV.JustFound Index adv 'SlotE
x -> Index adv 'SlotE -> ST s (Index adv 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Index adv 'SlotE
x

  ensureLowerDensityInWindows firstActive iterH g mv

  -- While densities are lower in the adversarial schema, the adversarial
  -- schema could still win races to the k+1st block by less than 1+delta
  -- slots. Therefore, we call @unfillRaces@ to deactivate further slots.
  unfillRaces kPlus1st (firstActive C.+ 1) UnknownYS iterH g mv

  -- Fill active slots after the stability window to ensure the alternative
  -- schema has more than k active slots
  let trailingSlots = Count adv 'SlotE Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Count adv 'SlotE Total
sz Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
k
  forM_ [trailingSlots .. C.getCount sz - 1] $ \Int
i ->
    Proxy 'NotInverted
-> MVector adv 'SlotE s S -> Index adv 'SlotE -> ST s ()
forall (pol :: Pol) (proxy :: Pol -> *) base s.
POL pol =>
proxy pol
-> MVector base 'SlotE s S -> Index base 'SlotE -> ST s ()
BV.setMV Proxy 'NotInverted
S.notInverted MVector adv 'SlotE s S
mv (Int -> Index adv 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
i)

  pure mv
 where
  UnsafeCheckedAdversarialRecipe
    { ChainSchema base hon
carHonest :: forall base hon adv.
CheckedAdversarialRecipe base hon adv -> ChainSchema base hon
carHonest :: ChainSchema base hon
carHonest
    , carParams :: forall base hon adv.
CheckedAdversarialRecipe base hon adv -> (Kcp, Scg, Delta)
carParams = (Kcp
kcp, Scg
scg, Delta
delta)
    , Contains 'SlotE hon adv
carWin :: forall base hon adv.
CheckedAdversarialRecipe base hon adv -> Contains 'SlotE hon adv
carWin :: Contains 'SlotE hon adv
carWin
    } = CheckedAdversarialRecipe base hon adv
recipe

  wrap :: Vector adv 'SlotE S -> ChainSchema base adv
wrap Vector adv 'SlotE S
v = Contains 'SlotE base adv
-> Vector adv 'SlotE S -> ChainSchema base adv
forall base inner.
Contains 'SlotE base inner
-> Vector inner 'SlotE S -> ChainSchema base inner
ChainSchema (Contains 'SlotE base hon
-> Contains 'SlotE hon adv -> Contains 'SlotE base adv
forall {kelem} (elem :: kelem) outer mid inner.
Contains elem outer mid
-> Contains elem mid inner -> Contains elem outer inner
C.joinWin Contains 'SlotE base hon
winH Contains 'SlotE hon adv
carWin) Vector adv 'SlotE S
v

  Kcp Int
k = Kcp
kcp
  Scg Int
s = Scg
scg
  Delta Int
d = Delta
delta

  ChainSchema Contains 'SlotE base hon
winH Vector hon 'SlotE S
vH = ChainSchema base hon
carHonest

  vHAfterIntersection :: Vector adv 'SlotE S
vHAfterIntersection = Contains 'SlotE hon adv
-> Vector hon 'SlotE S -> Vector adv 'SlotE S
forall {k} a (elem :: k) outer inner.
Unbox a =>
Contains elem outer inner
-> Vector outer elem a -> Vector inner elem a
C.sliceV Contains 'SlotE hon adv
carWin Vector hon 'SlotE S
vH

  -- ensure the adversary loses this 'RI.Race' and each subsequent race that ends before it can accelerate
  unfillRaces :: Index adv 'SlotE
-> Index adv 'SlotE
-> MaybeYS adv
-> Race adv
-> t
-> MVector adv 'SlotE s S
-> ST s ()
unfillRaces Index adv 'SlotE
kPlus1st !Index adv 'SlotE
scope !MaybeYS adv
mbYS !Race adv
iter !t
g !MVector adv 'SlotE s S
mv = Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Delta -> MaybeYS adv -> Race adv -> Bool
forall base. Delta -> MaybeYS base -> Race base -> Bool
withinYS Delta
delta MaybeYS adv
mbYS Race adv
iter) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$ do
    C.SomeWindow Proxy rwin <- SomeWindow RaceLbl adv 'SlotE
-> ST s (SomeWindow RaceLbl adv 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow RaceLbl adv 'SlotE
 -> ST s (SomeWindow RaceLbl adv 'SlotE))
-> SomeWindow RaceLbl adv 'SlotE
-> ST s (SomeWindow RaceLbl adv 'SlotE)
forall a b. (a -> b) -> a -> b
$ let RI.Race SomeWindow RaceLbl adv 'SlotE
x = Race adv
iter in SomeWindow RaceLbl adv 'SlotE
x

    C.SomeWindow (Proxy :: Proxy skolem) win <-
      pure $
        C.withWindowBetween
          (C.windowSize carWin)
          (C.Lbl @RaceAssumptionLbl)
          (C.windowStart rwin)
          (C.windowLast rwin C.+ d) -- rwin ends in a block, so if d=0
          -- then the slot after that block
          -- is unconstrained; hence no +1

    -- INVARIANT: @win@ contains @scope@
    let _ = scope :: C.Index adv SlotE

    -- remove adversarial active slots as needed
    --
    -- But only remove them from /after/ @scope@ (ie do not remove them
    -- from slots in the previous Race Window).
    do
      untouchZeroCount :: C.Var adv EmptySlotE <- do
        C.SomeWindow Proxy untouch <- -- untouchable slots
          pure $
            C.withWindowBetween
              (C.windowSize carWin)
              (C.Lbl @UntouchableLbl)
              (C.windowStart rwin)
              (scope C.- 1) -- window will be empty if scope is 0
        C.fromWindowVar untouch <$> BV.countActivesInMV S.inverted (C.sliceMV untouch mv)

      C.SomeWindow (Proxy :: Proxy skolem2) touch <- -- touchable slots
        pure $
          C.withWindowBetween
            (C.windowSize carWin)
            (C.Lbl @TouchableLbl)
            scope
            (C.windowLast rwin C.+ d)

      let
        maxActive :: C.Var (C.Win RaceAssumptionLbl skolem) ActiveSlotE
        maxActive = Int -> Var (Win RaceAssumptionLbl skolem) 'ActiveSlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
k

        -- at most k can be active in this race window, so at least size - k must be empty
        minEmpty :: C.Var (C.Win RaceAssumptionLbl skolem) EmptySlotE
        minEmpty = Proxy 'NotInverted
-> Size (Win RaceAssumptionLbl skolem) 'SlotE
-> Count
     (Win RaceAssumptionLbl skolem)
     (PreImage 'NotInverted 'ActiveSlotE)
     Other
-> Count
     (Win RaceAssumptionLbl skolem)
     (PreImage 'NotInverted 'EmptySlotE)
     Other
forall (proxy :: Pol -> *) (pol :: Pol) base which.
proxy pol
-> Size base 'SlotE
-> Count base (PreImage pol 'ActiveSlotE) which
-> Count base (PreImage pol 'EmptySlotE) which
S.complementActive Proxy 'NotInverted
S.notInverted (Contains 'SlotE adv (Win RaceAssumptionLbl skolem)
-> Size (Win RaceAssumptionLbl skolem) 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE adv (Win RaceAssumptionLbl skolem)
win) Count
  (Win RaceAssumptionLbl skolem)
  (PreImage 'NotInverted 'ActiveSlotE)
  Other
Var (Win RaceAssumptionLbl skolem) 'ActiveSlotE
maxActive

      -- Discount that basic requirement by the number of zeros already
      -- in the untouchable portion of this race window.
      let touchableEmpty =
            Var adv 'EmptySlotE -> Var adv 'EmptySlotE -> Var adv 'EmptySlotE
forall a. Ord a => a -> a -> a
max Var adv 'EmptySlotE
0 (Var adv 'EmptySlotE -> Var adv 'EmptySlotE)
-> Var adv 'EmptySlotE -> Var adv 'EmptySlotE
forall a b. (a -> b) -> a -> b
$
              Contains 'SlotE adv (Win RaceAssumptionLbl skolem)
-> Var (Win RaceAssumptionLbl skolem) 'EmptySlotE
-> Var adv 'EmptySlotE
forall {kelem1} {kelem2} (elem :: kelem1) outer inner
       (x :: kelem2).
Contains elem outer inner -> Var inner x -> Var outer x
C.fromWindowVar Contains 'SlotE adv (Win RaceAssumptionLbl skolem)
win Var (Win RaceAssumptionLbl skolem) 'EmptySlotE
minEmpty Var adv 'EmptySlotE -> Var adv 'EmptySlotE -> Var adv 'EmptySlotE
forall a. Num a => a -> a -> a
- Var adv 'EmptySlotE
untouchZeroCount ::
              C.Var adv EmptySlotE

      void $
        BV.fillInWindow
          S.inverted
          (BV.SomeDensityWindow (C.toWindowVar touch touchableEmpty) (C.windowSize touch))
          g
          (C.sliceMV touch mv)

    case RI.next vHAfterIntersection iter
      <|> RI.nextConservative vHAfterIntersection iter of
      Maybe (Race adv)
Nothing -> () -> ST s ()
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure () -- there are no remaining honest active slots
      Just Race adv
iter' -> do
        C.SomeWindow Proxy rwin' <- SomeWindow RaceLbl adv 'SlotE
-> ST s (SomeWindow RaceLbl adv 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow RaceLbl adv 'SlotE
 -> ST s (SomeWindow RaceLbl adv 'SlotE))
-> SomeWindow RaceLbl adv 'SlotE
-> ST s (SomeWindow RaceLbl adv 'SlotE)
forall a b. (a -> b) -> a -> b
$ let RI.Race SomeWindow RaceLbl adv 'SlotE
x = Race adv
iter' in SomeWindow RaceLbl adv 'SlotE
x
        mbYS' <- case mbYS of
          KnownYS{} -> MaybeYS adv -> ST s (MaybeYS adv)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MaybeYS adv
mbYS
          MaybeYS adv
UnknownYS -> do
            -- check whether the slots that are settled as of just
            -- now contain the first adversarial active slot
            C.SomeWindow Proxy settledSlots <-
              SomeWindow SettledLbl adv 'SlotE
-> ST s (SomeWindow SettledLbl adv 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow SettledLbl adv 'SlotE
 -> ST s (SomeWindow SettledLbl adv 'SlotE))
-> SomeWindow SettledLbl adv 'SlotE
-> ST s (SomeWindow SettledLbl adv 'SlotE)
forall a b. (a -> b) -> a -> b
$
                Count adv 'SlotE Total
-> Lbl SettledLbl
-> Index adv 'SlotE
-> Index adv 'SlotE
-> SomeWindow SettledLbl adv 'SlotE
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl).
Size outer elem
-> Lbl lbl
-> Index outer elem
-> Index outer elem
-> SomeWindow lbl outer elem
C.withWindowBetween
                  (Contains 'SlotE hon adv -> Count adv 'SlotE Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE hon adv
carWin)
                  (forall lbl. Lbl lbl
forall {k} (lbl :: k). Lbl lbl
C.Lbl @SettledLbl)
                  (Contains 'SlotE adv (Win RaceLbl skolem) -> Index adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE adv (Win RaceLbl skolem)
rwin)
                  (Contains 'SlotE adv (Win RaceLbl skolem) -> Index adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE adv (Win RaceLbl skolem)
rwin' Index adv 'SlotE -> Int -> Index adv 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.- Int
1)
            mbFound <- BV.findIthEmptyInMV S.inverted (C.sliceMV settledSlots mv) (C.Count 0)
            case mbFound of
              MaybeFound (Win SettledLbl skolem)
BV.NothingFound -> MaybeYS adv -> ST s (MaybeYS adv)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MaybeYS adv
forall base. MaybeYS base
UnknownYS
              BV.JustFound Index (Win SettledLbl skolem) 'SlotE
x ->
                -- x is the first settled adversarial slot, so
                -- the adversary can accelerate its growth as
                -- of x+s+1 (If s were 0, it could accelerate
                -- in the very next slot, thus the plus 1.)
                MaybeYS adv -> ST s (MaybeYS adv)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MaybeYS adv -> ST s (MaybeYS adv))
-> MaybeYS adv -> ST s (MaybeYS adv)
forall a b. (a -> b) -> a -> b
$!
                  Index adv 'SlotE -> MaybeYS adv
forall base. Index base 'SlotE -> MaybeYS base
KnownYS (Index adv 'SlotE -> MaybeYS adv)
-> Index adv 'SlotE -> MaybeYS adv
forall a b. (a -> b) -> a -> b
$!
                    Index adv 'SlotE -> Index adv 'SlotE -> Index adv 'SlotE
forall a. Ord a => a -> a -> a
max
                      (Index adv 'SlotE
kPlus1st Index adv 'SlotE -> Int -> Index adv 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
d Index adv 'SlotE -> Int -> Index adv 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
1)
                      (Contains 'SlotE adv (Win SettledLbl skolem)
-> Index (Win SettledLbl skolem) 'SlotE -> Index adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index inner elem -> Index outer elem
C.fromWindow Contains 'SlotE adv (Win SettledLbl skolem)
settledSlots Index (Win SettledLbl skolem) 'SlotE
x Index adv 'SlotE -> Int -> Index adv 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
s Index adv 'SlotE -> Int -> Index adv 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
1)
        unfillRaces kPlus1st (max scope (C.windowLast win C.+ 1)) mbYS' iter' g mv

  -- \| Ensure the density of the adversarial schema is less than the density
  -- of the honest schema in the first stability window after the intersection
  -- and in any prefix window that contains the first race to the k+1st block.
  --
  -- Ensuring lower density of the prefix windows is necessary to avoid chains like
  --
  -- > k: 3
  -- > s: 9
  -- > H: 0111100
  -- > A: 1110011
  --
  -- where the honest chain wins the race to the k+1st block, might win the
  -- density comparison if the chains are extended to include a full stability
  -- window after the intersection, but loses the density comparison if the
  -- chains aren't extended.
  --
  -- For the sake of shrinking test inputs, we also prevent the above scenario
  -- to occur in any intersection, not just the intersections near the end of
  -- the chains.
  ensureLowerDensityInWindows ::
    R.StatefulGen sg (ST s) =>
    C.Index adv SlotE ->
    RI.Race adv ->
    sg ->
    C.MVector adv SlotE s S.S ->
    ST s ()
  ensureLowerDensityInWindows :: forall sg s.
StatefulGen sg (ST s) =>
Index adv 'SlotE
-> Race adv -> sg -> MVector adv 'SlotE s S -> ST s ()
ensureLowerDensityInWindows Index adv 'SlotE
firstActiveSlot (RI.Race (C.SomeWindow Proxy skolem
_ Contains 'SlotE adv (Win RaceLbl skolem)
w0)) sg
g MVector adv 'SlotE s S
mv = do
    let
      -- A window after the intersection as short as the shortest of the
      -- stability window or the first race to the k+1st block.
      w0' :: Contains 'SlotE adv (Win RaceLbl skolem)
w0' = Contains 'SlotE adv (Win RaceLbl skolem)
-> Size (Win RaceLbl skolem) 'SlotE
-> Contains 'SlotE adv (Win RaceLbl skolem)
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner
-> Size inner elem -> Contains elem outer inner
C.truncateWin Contains 'SlotE adv (Win RaceLbl skolem)
w0 (Int -> Size (Win RaceLbl skolem) 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
s)
      hCount :: Var (Win RaceLbl skolem) 'ActiveSlotE
hCount =
        Count (Win RaceLbl skolem) 'ActiveSlotE Total
-> Var (Win RaceLbl skolem) 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Var base elem
C.toVar (Count (Win RaceLbl skolem) 'ActiveSlotE Total
 -> Var (Win RaceLbl skolem) 'ActiveSlotE)
-> Count (Win RaceLbl skolem) 'ActiveSlotE Total
-> Var (Win RaceLbl skolem) 'ActiveSlotE
forall a b. (a -> b) -> a -> b
$
          Proxy 'NotInverted
-> Vector (Win RaceLbl skolem) 'SlotE S
-> Size (Win RaceLbl skolem) (PreImage 'NotInverted 'ActiveSlotE)
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S -> Size base (PreImage pol 'ActiveSlotE)
BV.countActivesInV Proxy 'NotInverted
S.notInverted (Contains 'SlotE adv (Win RaceLbl skolem)
-> Vector adv 'SlotE S -> Vector (Win RaceLbl skolem) 'SlotE S
forall {k} a (elem :: k) outer inner.
Unbox a =>
Contains elem outer inner
-> Vector outer elem a -> Vector inner elem a
C.sliceV Contains 'SlotE adv (Win RaceLbl skolem)
w0' Vector adv 'SlotE S
vHAfterIntersection)

    aCount <- Index adv 'SlotE
-> Contains 'SlotE adv (Win RaceLbl skolem)
-> sg
-> MVector adv 'SlotE s S
-> Var (Win RaceLbl skolem) 'ActiveSlotE
-> ST s (Var (Win RaceLbl skolem) 'ActiveSlotE)
forall {g} {s} {outer} {outer} {base} {which}.
StatefulGen g (ST s) =>
Count outer 'SlotE Preds
-> Contains 'SlotE outer base
-> g
-> MVector outer 'SlotE s S
-> Count base 'ActiveSlotE which
-> ST s (Var base 'ActiveSlotE)
ensureLowerDensityInWindow Index adv 'SlotE
firstActiveSlot Contains 'SlotE adv (Win RaceLbl skolem)
w0' sg
g MVector adv 'SlotE s S
mv Var (Win RaceLbl skolem) 'ActiveSlotE
hCount

    void $
      foldM
        updateDensityOfMv
        (hCount, aCount)
        (stablePrefixWindowsContaining w0')
   where
    -- Yields all windows of the adversarial schema with proper prefix @w@
    -- that are prefixes of the first stability window after the
    -- intersection.
    stablePrefixWindowsContaining :: Contains elem outer base -> [Contains elem outer inner]
stablePrefixWindowsContaining Contains elem outer base
w =
      let
        start :: Index outer elem
start = Contains elem outer base -> Index outer elem
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains elem outer base
w
        size :: Int
size = Count base elem Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Contains elem outer base -> Count base elem Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains elem outer base
w)
        end :: Int
end = Int
s Int -> Int -> Int
forall a. Ord a => a -> a -> a
`min` Count adv 'SlotE Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (MVector adv 'SlotE s S -> Count adv 'SlotE Total
forall {kelem} a base (elem :: kelem) s.
Unbox a =>
MVector base elem s a -> Size base elem
C.lengthMV MVector adv 'SlotE s S
mv)
       in
        [Index outer elem -> Size inner elem -> Contains elem outer inner
forall kelem (elem :: kelem) outer inner.
Index outer elem -> Size inner elem -> Contains elem outer inner
C.UnsafeContains Index outer elem
start (Int -> Size inner elem
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
size') | Int
size' <- [Int
size Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1 .. Int
end]]

    -- Updates mv to ensure the density of the adversarial schema is lower
    -- than the density of the honest schema in @increaseSizeW w@.
    --
    -- @hc@ is the number of active slots in the honest schema in @w@ minus
    -- the last slot
    --
    -- @ac@ is the number of active slots in the adversarial schema in @w@
    -- minus the last slot
    updateDensityOfMv :: (Count base 'ActiveSlotE Other, Count base 'ActiveSlotE Other)
-> Contains 'SlotE adv base
-> ST
     s (Count base 'ActiveSlotE Other, Count base 'ActiveSlotE Other)
updateDensityOfMv (Count base 'ActiveSlotE Other
hc, Count base 'ActiveSlotE Other
ac) Contains 'SlotE adv base
w = do
      sA <- Proxy 'NotInverted
-> MVector adv 'SlotE s S -> Index adv 'SlotE -> ST s Bool
forall (pol :: Pol) (proxy :: Pol -> *) base s.
POL pol =>
proxy pol
-> MVector base 'SlotE s S -> Index base 'SlotE -> ST s Bool
BV.testMV Proxy 'NotInverted
S.notInverted MVector adv 'SlotE s S
mv (Contains 'SlotE adv base -> Index adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE adv base
w)

      let
        ac' = if Bool
sA then Count base 'ActiveSlotE Other
ac Count base 'ActiveSlotE Other
-> Int -> Count base 'ActiveSlotE Other
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
1 else Count base 'ActiveSlotE Other
ac
        sH = Proxy 'NotInverted
-> Vector adv 'SlotE S -> Index adv 'SlotE -> Bool
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol -> Vector base 'SlotE S -> Index base 'SlotE -> Bool
BV.testV Proxy 'NotInverted
S.notInverted Vector adv 'SlotE S
vHAfterIntersection (Contains 'SlotE adv base -> Index adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE adv base
w)
        hc' = if Bool
sH then Count base 'ActiveSlotE Other
hc Count base 'ActiveSlotE Other
-> Int -> Count base 'ActiveSlotE Other
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
1 else Count base 'ActiveSlotE Other
hc

      ac'' <-
        if ac' >= hc'
          then
            ensureLowerDensityInWindow firstActiveSlot w g mv hc'
          else
            pure ac'

      return (hc', ac'')

  -- \| Ensure the density of the adversarial schema is less than the density
  -- of the honest schema in the given window.
  --
  -- @hCount@ is the number of active slots in the honest schema in the
  -- given window.
  ensureLowerDensityInWindow :: Count outer 'SlotE Preds
-> Contains 'SlotE outer base
-> g
-> MVector outer 'SlotE s S
-> Count base 'ActiveSlotE which
-> ST s (Var base 'ActiveSlotE)
ensureLowerDensityInWindow Count outer 'SlotE Preds
firstActiveSlot Contains 'SlotE outer base
w g
g MVector outer 'SlotE s S
mv Count base 'ActiveSlotE which
hCount = do
    let emptyCountTarget :: Var base 'EmptySlotE
emptyCountTarget = Count base 'EmptySlotE which -> Var base 'EmptySlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Var base elem
C.toVar (Count base 'EmptySlotE which -> Var base 'EmptySlotE)
-> Count base 'EmptySlotE which -> Var base 'EmptySlotE
forall a b. (a -> b) -> a -> b
$ Proxy 'NotInverted
-> Size base 'SlotE
-> Count base (PreImage 'NotInverted 'ActiveSlotE) which
-> Count base (PreImage 'NotInverted 'EmptySlotE) which
forall (proxy :: Pol -> *) (pol :: Pol) base which.
proxy pol
-> Size base 'SlotE
-> Count base (PreImage pol 'ActiveSlotE) which
-> Count base (PreImage pol 'EmptySlotE) which
S.complementActive Proxy 'NotInverted
S.notInverted (Contains 'SlotE outer base -> Size base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE outer base
w) Count base (PreImage 'NotInverted 'ActiveSlotE) which
Count base 'ActiveSlotE which
hCount Count base 'EmptySlotE which -> Int -> Count base 'EmptySlotE which
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
1

    emptyCount <-
      Count outer 'SlotE Preds
-> Var base 'EmptySlotE
-> Contains 'SlotE outer base
-> g
-> MVector outer 'SlotE s S
-> ST s (Var base 'EmptySlotE)
forall {g} {s} {outer} {base} {outer}.
StatefulGen g (ST s) =>
Count outer 'SlotE Preds
-> Count base 'EmptySlotE Other
-> Contains 'SlotE outer base
-> g
-> MVector outer 'SlotE s S
-> ST s (Count base 'EmptySlotE Other)
fillInWindowSkippingFirstActiveSlot
        Count outer 'SlotE Preds
firstActiveSlot
        Var base 'EmptySlotE
emptyCountTarget
        Contains 'SlotE outer base
w
        g
g
        MVector outer 'SlotE s S
mv

    pure $ C.toVar $ S.complementActive S.inverted (C.windowSize w) emptyCount

  fillInWindowSkippingFirstActiveSlot :: Count outer 'SlotE Preds
-> Count base 'EmptySlotE Other
-> Contains 'SlotE outer base
-> g
-> MVector outer 'SlotE s S
-> ST s (Count base 'EmptySlotE Other)
fillInWindowSkippingFirstActiveSlot Count outer 'SlotE Preds
firstActiveSlot Count base 'EmptySlotE Other
emptyCountTarget Contains 'SlotE outer base
w g
g MVector outer 'SlotE s S
mv
    | Count base 'SlotE Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Contains 'SlotE outer base -> Count base 'SlotE Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE outer base
w) Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Count outer 'SlotE Preds -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Count outer 'SlotE Preds
firstActiveSlot = Count base 'EmptySlotE Other -> ST s (Count base 'EmptySlotE Other)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Count base 'EmptySlotE Other
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0)
    | Bool
otherwise = do
        let
          slot :: Int
slot = Count outer 'SlotE Preds -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Count outer 'SlotE Preds
firstActiveSlot
          emptyCountTarget' :: Count base 'EmptySlotE Other
emptyCountTarget' = Count base 'EmptySlotE Other
emptyCountTarget Count base 'EmptySlotE Other -> Int -> Count base 'EmptySlotE Other
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.- Int
slot
          w' :: Contains 'SlotE outer base
w' =
            Count outer 'SlotE Preds
-> Count base 'SlotE Total -> Contains 'SlotE outer base
forall kelem (elem :: kelem) outer inner.
Index outer elem -> Size inner elem -> Contains elem outer inner
C.UnsafeContains
              (Count outer 'SlotE Preds
firstActiveSlot Count outer 'SlotE Preds -> Int -> Count outer 'SlotE Preds
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
1)
              (Contains 'SlotE outer base -> Count base 'SlotE Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE outer base
w Count base 'SlotE Total -> Int -> Count base 'SlotE Total
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.- (Int
slot Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))

        Proxy 'Inverted
-> SomeDensityWindow 'Inverted
-> g
-> MVector base 'SlotE s S
-> ST s (Var base (PreImage 'Inverted 'ActiveSlotE))
forall (proxy :: Pol -> *) (pol :: Pol) base g s.
(POL pol, StatefulGen g (ST s)) =>
proxy pol
-> SomeDensityWindow pol
-> g
-> MVector base 'SlotE s S
-> ST s (Var base (PreImage pol 'ActiveSlotE))
BV.fillInWindow
          Proxy 'Inverted
S.inverted
          (Var base (PreImage 'Inverted 'ActiveSlotE)
-> Count base 'SlotE Total -> SomeDensityWindow 'Inverted
forall (pol :: Pol) slidingWindow.
Var slidingWindow (PreImage pol 'ActiveSlotE)
-> Size slidingWindow 'SlotE -> SomeDensityWindow pol
BV.SomeDensityWindow Var base (PreImage 'Inverted 'ActiveSlotE)
Count base 'EmptySlotE Other
emptyCountTarget' (Contains 'SlotE outer base -> Count base 'SlotE Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE outer base
w'))
          g
g
          (Contains 'SlotE outer base
-> MVector outer 'SlotE s S -> MVector base 'SlotE s S
forall {k} a (elem :: k) outer inner s.
Unbox a =>
Contains elem outer inner
-> MVector outer elem s a -> MVector inner elem s a
C.sliceMV Contains 'SlotE outer base
w' MVector outer 'SlotE s S
mv)

-- | The youngest stable slot
--
-- If @x@ is the first adversarial active slot, then @x+s@ (see 'Scg') is the youngest stable slot.
data MaybeYS base = UnknownYS | KnownYS !(C.Index base SlotE)
  deriving (MaybeYS base -> MaybeYS base -> Bool
(MaybeYS base -> MaybeYS base -> Bool)
-> (MaybeYS base -> MaybeYS base -> Bool) -> Eq (MaybeYS base)
forall base. MaybeYS base -> MaybeYS base -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall base. MaybeYS base -> MaybeYS base -> Bool
== :: MaybeYS base -> MaybeYS base -> Bool
$c/= :: forall base. MaybeYS base -> MaybeYS base -> Bool
/= :: MaybeYS base -> MaybeYS base -> Bool
Eq, ReadPrec [MaybeYS base]
ReadPrec (MaybeYS base)
Int -> ReadS (MaybeYS base)
ReadS [MaybeYS base]
(Int -> ReadS (MaybeYS base))
-> ReadS [MaybeYS base]
-> ReadPrec (MaybeYS base)
-> ReadPrec [MaybeYS base]
-> Read (MaybeYS base)
forall base. ReadPrec [MaybeYS base]
forall base. ReadPrec (MaybeYS base)
forall base. Int -> ReadS (MaybeYS base)
forall base. ReadS [MaybeYS base]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall base. Int -> ReadS (MaybeYS base)
readsPrec :: Int -> ReadS (MaybeYS base)
$creadList :: forall base. ReadS [MaybeYS base]
readList :: ReadS [MaybeYS base]
$creadPrec :: forall base. ReadPrec (MaybeYS base)
readPrec :: ReadPrec (MaybeYS base)
$creadListPrec :: forall base. ReadPrec [MaybeYS base]
readListPrec :: ReadPrec [MaybeYS base]
Read, Int -> MaybeYS base -> ShowS
[MaybeYS base] -> ShowS
MaybeYS base -> String
(Int -> MaybeYS base -> ShowS)
-> (MaybeYS base -> String)
-> ([MaybeYS base] -> ShowS)
-> Show (MaybeYS base)
forall base. Int -> MaybeYS base -> ShowS
forall base. [MaybeYS base] -> ShowS
forall base. MaybeYS base -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall base. Int -> MaybeYS base -> ShowS
showsPrec :: Int -> MaybeYS base -> ShowS
$cshow :: forall base. MaybeYS base -> String
show :: MaybeYS base -> String
$cshowList :: forall base. [MaybeYS base] -> ShowS
showList :: [MaybeYS base] -> ShowS
Show)

-- | Does the Race Window end in a stable slot?
withinYS :: Delta -> MaybeYS base -> RI.Race base -> Bool
withinYS :: forall base. Delta -> MaybeYS base -> Race base -> Bool
withinYS (Delta Int
d) !MaybeYS base
mbYS !(RI.Race (C.SomeWindow Proxy skolem
Proxy Contains 'SlotE base (Win RaceLbl skolem)
win)) = case MaybeYS base
mbYS of
  KnownYS Count base 'SlotE Preds
ys -> Contains 'SlotE base (Win RaceLbl skolem)
-> Count base 'SlotE Preds
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE base (Win RaceLbl skolem)
win Count base 'SlotE Preds -> Int -> Count base 'SlotE Preds
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
d Count base 'SlotE Preds -> Count base 'SlotE Preds -> Bool
forall a. Ord a => a -> a -> Bool
< Count base 'SlotE Preds
ys
  MaybeYS base
UnknownYS -> Bool
True -- Honest Chain Growth ensures every Race Window is at most @'Scg' - 'Delta'@ slots wide

-- | Draw a random active slot count for the prefix of a fork.
--
-- The result is guaranteed to leave more than k active slots after the
-- intersection in the honest and the adversarial chains.
-- See Note [Minimum schema length] in "Test.Ouroboros.Consensus.ChainGenerator.Honest"
-- for the rationale of the precondition.
--
-- PRECONDITION: @schemaSize schedH >= s + d + k + 1@
genPrefixBlockCount ::
  R.RandomGen g => HonestRecipe -> g -> ChainSchema base hon -> C.Var hon 'ActiveSlotE
genPrefixBlockCount :: forall g base hon.
RandomGen g =>
HonestRecipe -> g -> ChainSchema base hon -> Var hon 'ActiveSlotE
genPrefixBlockCount (HonestRecipe (Kcp Int
k) (Scg Int
s) (Delta Int
d) Len
_len) g
g ChainSchema base hon
schedH
  | Vector hon 'SlotE S -> Size hon 'SlotE
forall {kelem} a base (elem :: kelem).
Unbox a =>
Vector base elem a -> Size base elem
C.lengthV Vector hon 'SlotE S
vH Size hon 'SlotE -> Size hon 'SlotE -> Bool
forall a. Ord a => a -> a -> Bool
< Int -> Size hon 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count (Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) =
      String -> Var hon 'ActiveSlotE
forall a. HasCallStack => String -> a
error String
"size of schema is smaller than s + d + k + 1"
  | Bool
otherwise =
      -- @uniformIndex n@ yields a value in @[0..n-1]@, we add 1 to the
      -- argument to account for the possibility of intersecting at the
      -- genesis block
      Count hon 'ActiveSlotE Preds -> Var hon 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Var base elem
C.toVar (Count hon 'ActiveSlotE Preds -> Var hon 'ActiveSlotE)
-> Count hon 'ActiveSlotE Preds -> Var hon 'ActiveSlotE
forall a b. (a -> b) -> a -> b
$ g
-> (forall s. STGenM g s -> ST s (Count hon 'ActiveSlotE Preds))
-> Count hon 'ActiveSlotE Preds
forall g a.
RandomGen g =>
g -> (forall s. STGenM g s -> ST s a) -> a
R.runSTGen_ g
g ((forall s. STGenM g s -> ST s (Count hon 'ActiveSlotE Preds))
 -> Count hon 'ActiveSlotE Preds)
-> (forall s. STGenM g s -> ST s (Count hon 'ActiveSlotE Preds))
-> Count hon 'ActiveSlotE Preds
forall a b. (a -> b) -> a -> b
$ Size hon 'ActiveSlotE
-> STGenM g s -> ST s (Count hon 'ActiveSlotE Preds)
forall {kelem} g (m :: * -> *) base (elem :: kelem).
StatefulGen g m =>
Size base elem -> g -> m (Index base elem)
C.uniformIndex (Size hon 'ActiveSlotE
activesInPrefix Size hon 'ActiveSlotE -> Int -> Size hon 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.+ Int
1)
 where
  ChainSchema Contains 'SlotE base hon
_winH Vector hon 'SlotE S
vH = ChainSchema base hon
schedH

  -- activesInPrefix is the amount of active slots in the honest schema with a
  -- suffix of s+d+k+1 slots.
  --
  -- In the honest chain, the suffix is sufficiently long to ensure there are
  -- k+1 active slots by the Extended Praos Chain Growth Assumption.
  --
  -- In the alternative chain, there is enough room to fit k+1 active slots
  -- as explained the Note [Minimum schema length] in
  -- "Test.Ouroboros.Consensus.ChainGenerator.Honest".

  activesInPrefix :: Size hon (PreImage 'NotInverted 'ActiveSlotE)
activesInPrefix =
    Proxy 'NotInverted
-> Vector hon 'SlotE S
-> Size hon (PreImage 'NotInverted 'ActiveSlotE)
forall (pol :: Pol) (proxy :: Pol -> *) base.
POL pol =>
proxy pol
-> Vector base 'SlotE S -> Size base (PreImage pol 'ActiveSlotE)
BV.countActivesInV Proxy 'NotInverted
S.notInverted (Vector hon 'SlotE S
 -> Size hon (PreImage 'NotInverted 'ActiveSlotE))
-> Vector hon 'SlotE S
-> Size hon (PreImage 'NotInverted 'ActiveSlotE)
forall a b. (a -> b) -> a -> b
$
      Contains 'SlotE hon hon
-> Vector hon 'SlotE S -> Vector hon 'SlotE S
forall {k} a (elem :: k) outer inner.
Unbox a =>
Contains elem outer inner
-> Vector outer elem a -> Vector inner elem a
C.sliceV
        (Index hon 'SlotE -> Size hon 'SlotE -> Contains 'SlotE hon hon
forall kelem (elem :: kelem) outer inner.
Index outer elem -> Size inner elem -> Contains elem outer inner
C.UnsafeContains (Int -> Index hon 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) (Size hon 'SlotE -> Contains 'SlotE hon hon)
-> Size hon 'SlotE -> Contains 'SlotE hon hon
forall a b. (a -> b) -> a -> b
$ Vector hon 'SlotE S -> Size hon 'SlotE
forall {kelem} a base (elem :: kelem).
Unbox a =>
Vector base elem a -> Size base elem
C.lengthV Vector hon 'SlotE S
vH Size hon 'SlotE -> Int -> Size hon 'SlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int -> Count base elem which
C.- (Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
d Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
        Vector hon 'SlotE S
vH