{-# 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 qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S
import           Test.Ouroboros.Consensus.ChainGenerator.Slot
                     (E (ActiveSlotE, EmptySlotE, SlotE))
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 {
    -- | The adversarial race window
    forall hon adv. RaceViolation hon adv -> Race adv
rvAdv :: !(RI.Race adv)
  ,
    -- | The honest race window
    forall hon adv. RaceViolation hon adv -> Race hon
rvHon :: !(RI.Race hon)
  }
  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
    Except (AdversarialViolation hon adv) ()
checkStart
    Except (AdversarialViolation hon adv) ()
checkCount
    Except (AdversarialViolation hon adv) ()
checkRaces
    Except (AdversarialViolation hon adv) ()
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 :: Except (AdversarialViolation hon adv) ()
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
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
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) (Except (AdversarialViolation hon adv) ()
 -> Except (AdversarialViolation hon adv) ())
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
forall a b. (a -> b) -> a -> b
$ AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
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
 -> Except (AdversarialViolation hon adv) ())
-> AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
forall a b. (a -> b) -> a -> b
$ AnchorViolation -> AdversarialViolation hon adv
forall hon adv. AnchorViolation -> AdversarialViolation hon adv
BadAnchor AnchorViolation
HonestActiveMustAnchorAdversarial
              Bool
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
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) (Except (AdversarialViolation hon adv) ()
 -> Except (AdversarialViolation hon adv) ())
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
forall a b. (a -> b) -> a -> b
$ AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
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
 -> Except (AdversarialViolation hon adv) ())
-> AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
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
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
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) (Except (AdversarialViolation hon adv) ()
 -> Except (AdversarialViolation hon adv) ())
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
forall a b. (a -> b) -> a -> b
$ do
                    AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
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
 -> Except (AdversarialViolation hon adv) ())
-> AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
forall a b. (a -> b) -> a -> b
$ AnchorViolation -> AdversarialViolation hon adv
forall hon adv. AnchorViolation -> AdversarialViolation hon adv
BadAnchor AnchorViolation
HonestActiveMustAnchorAdversarial

                C.SomeWindow Proxy skolem
Proxy Contains 'SlotE hon (Win "foo" skolem)
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 :: Size (Win "foo" skolem) (PreImage 'NotInverted 'ActiveSlotE)
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
                Bool
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Contains 'SlotE hon (Win "foo" skolem)
-> Var (Win "foo" skolem) 'ActiveSlotE -> Var hon 'ActiveSlotE
forall {kelem1} {kelem2} (elem :: kelem1) outer inner
       (x :: kelem2).
Contains elem outer inner -> Var inner x -> Var outer x
C.fromWindowVar Contains 'SlotE hon (Win "foo" skolem)
precedingSlots (Count (Win "foo" skolem) 'ActiveSlotE Total
-> Var (Win "foo" skolem) 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Var base elem
C.toVar Count (Win "foo" skolem) 'ActiveSlotE Total
pc) Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE -> Bool
forall a. Eq a => a -> a -> Bool
/= Var hon 'ActiveSlotE
arPrefix) (Except (AdversarialViolation hon adv) ()
 -> Except (AdversarialViolation hon adv) ())
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
forall a b. (a -> b) -> a -> b
$ do
                    AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
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
 -> Except (AdversarialViolation hon adv) ())
-> AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
forall a b. (a -> b) -> a -> b
$ AnchorViolation -> AdversarialViolation hon adv
forall hon adv. AnchorViolation -> AdversarialViolation hon adv
BadAnchor AnchorViolation
WrongNumberOfHonestPredecessors

    checkCount :: Except (AdversarialViolation hon adv) ()
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
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
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) (Except (AdversarialViolation hon adv) ()
 -> Except (AdversarialViolation hon adv) ())
-> Except (AdversarialViolation hon adv) ()
-> Except (AdversarialViolation hon adv) ()
forall a b. (a -> b) -> a -> b
$ AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
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 :: Except (AdversarialViolation hon adv) ()
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    -> () -> Except (AdversarialViolation hon adv) ()
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 -> Except (AdversarialViolation hon adv) ()
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 skolem
Proxy Contains 'SlotE hon (Win RaceLbl skolem)
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 skolem
Proxy Contains 'SlotE adv (Win RaceLbl skolem)
raceWinA <- SomeWindow RaceLbl adv 'SlotE -> m (SomeWindow RaceLbl adv 'SlotE)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow RaceLbl adv 'SlotE
 -> m (SomeWindow RaceLbl adv 'SlotE))
-> SomeWindow RaceLbl adv 'SlotE
-> m (SomeWindow RaceLbl adv 'SlotE)
forall a b. (a -> b) -> a -> b
$ let RI.Race SomeWindow RaceLbl adv 'SlotE
x = Race adv
iterA in SomeWindow RaceLbl adv 'SlotE
x

        -- lift both windows to @base@ so that they're comparable
        let raceWinH' :: Contains 'SlotE base (Win RaceLbl skolem)
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 (Win RaceLbl skolem)
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
          | Index base 'SlotE
youngestStableA Index base 'SlotE -> Index base 'SlotE -> Bool
forall a. Ord a => a -> a -> Bool
< Contains 'SlotE base (Win RaceLbl skolem) -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE base (Win RaceLbl skolem)
raceWinH' 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 -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

          -- advance the adversarial Race Window if its start is <= the honest Race Window's start
          | Contains 'SlotE base (Win RaceLbl skolem) -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE base (Win RaceLbl skolem)
raceWinA' Index base 'SlotE -> Index base 'SlotE -> Bool
forall a. Ord a => a -> a -> Bool
<= Contains 'SlotE base (Win RaceLbl skolem) -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE base (Win RaceLbl skolem)
raceWinH' ->
            case 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 Race adv
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
          | Contains 'SlotE base (Win RaceLbl skolem) -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE base (Win RaceLbl skolem)
raceWinA' Index base 'SlotE -> Index base 'SlotE -> Bool
forall a. Ord a => a -> a -> Bool
<= Contains 'SlotE base (Win RaceLbl skolem) -> Index base 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE base (Win RaceLbl skolem)
raceWinH' 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 ->
                -- 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.
                AdversarialViolation hon adv -> m ()
forall a. AdversarialViolation hon adv -> m a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError (AdversarialViolation hon adv -> m ())
-> AdversarialViolation hon adv -> m ()
forall a b. (a -> b) -> a -> b
$ RaceViolation hon adv -> AdversarialViolation hon adv
forall hon adv.
RaceViolation hon adv -> AdversarialViolation hon adv
BadRace AdversaryWonRace {
                    rvAdv :: Race adv
rvAdv = Race adv
iterA
                  ,
                    rvHon :: Race hon
rvHon = Race hon
iterH
                  }

          -- advance the honest Race Window
          | Bool
otherwise -> case Vector hon 'SlotE S -> Race hon -> Maybe (Race hon)
forall base. Vector base 'SlotE S -> Race base -> Maybe (Race base)
RI.next Vector hon 'SlotE S
vH Race hon
iterH Maybe (Race hon) -> Maybe (Race hon) -> Maybe (Race hon)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Vector hon 'SlotE S -> Race hon -> Maybe (Race hon)
forall base. Vector base 'SlotE S -> Race base -> Maybe (Race base)
RI.nextConservative Vector hon 'SlotE S
vH Race hon
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 :: Except (AdversarialViolation hon adv) ()
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 Proxy skolem
pw0 Contains 'SlotE adv (Win RaceLbl skolem)
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)
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 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 S
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 :: Vector Int
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 :: Vector Int
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 :: [Int]
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 :: [Int]
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 [ (Int, (Int, Int))
cmp | cmp :: (Int, (Int, Int))
cmp@(Int
_, (Int
x, Int
y)) <- [Int] -> [(Int, Int)] -> [(Int, (Int, Int))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
hwSum [Int]
awSum), Int
x Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
y ] of
          []         -> () -> Except (AdversarialViolation hon adv) ()
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
-> Except (AdversarialViolation hon adv) ()
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
 -> Except (AdversarialViolation hon adv) ())
-> AdversarialViolation hon adv
-> Except (AdversarialViolation hon adv) ()
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 {
        -- | The honest chain to branch off of
        forall base hon. AdversarialRecipe base hon -> ChainSchema base hon
arHonest :: !(ChainSchema base hon)
      ,
        -- | protocol parameters
        forall base hon. AdversarialRecipe base hon -> (Kcp, Scg, Delta)
arParams :: (Kcp, Scg, Delta)
      ,
        -- | 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
        forall base hon. AdversarialRecipe base hon -> Var hon 'ActiveSlotE
arPrefix :: !(C.Var hon ActiveSlotE)
      }
  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 Any
 -> CheckedAdversarialRecipe base hon Any
 -> SomeCheckedAdversarialRecipe base hon)
-> String
-> ReadBuilder
     (Proxy Any
      -> CheckedAdversarialRecipe base hon Any
      -> SomeCheckedAdversarialRecipe base hon)
forall a. a -> String -> ReadBuilder a
Some.readCtor Proxy Any
-> CheckedAdversarialRecipe base hon Any
-> SomeCheckedAdversarialRecipe base hon
forall base hon adv.
Proxy adv
-> CheckedAdversarialRecipe base hon adv
-> SomeCheckedAdversarialRecipe base hon
SomeCheckedAdversarialRecipe String
"SomeCheckedAdversarialRecipe"
            ReadBuilder
  (Proxy Any
   -> CheckedAdversarialRecipe base hon Any
   -> SomeCheckedAdversarialRecipe base hon)
-> ReadBuilder (Proxy Any)
-> ReadBuilder
     (CheckedAdversarialRecipe base hon Any
      -> 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 Any)
forall a. Read a => ReadBuilder a
Some.readArg
            ReadBuilder
  (CheckedAdversarialRecipe base hon Any
   -> SomeCheckedAdversarialRecipe base hon)
-> ReadBuilder (CheckedAdversarialRecipe base hon Any)
-> 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 Any)
forall a. Read a => ReadBuilder a
Some.readArg

-- | Image of 'checkAdversarialRecipe' when it accepts the recipe
data CheckedAdversarialRecipe base hon adv =
    UnsafeCheckedAdversarialRecipe {
        -- | The honest chain to branch off of
        forall base hon adv.
CheckedAdversarialRecipe base hon adv -> ChainSchema base hon
carHonest :: !(ChainSchema base hon)
      ,
        -- | protocol parameters
        forall base hon adv.
CheckedAdversarialRecipe base hon adv -> (Kcp, Scg, Delta)
carParams :: (Kcp, Scg, Delta)
      ,
        -- | 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.
        forall base hon adv.
CheckedAdversarialRecipe base hon adv -> Contains 'SlotE hon adv
carWin    :: !(C.Contains SlotE hon adv)
      }
  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'
    Index hon 'SlotE
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 skolem
Proxy Contains 'SlotE hon (Win AdvLbl skolem)
winA <- SomeWindow AdvLbl hon 'SlotE
-> ExceptT
     NoSuchAdversarialChainSchema
     Identity
     (SomeWindow AdvLbl hon 'SlotE)
forall a. a -> ExceptT NoSuchAdversarialChainSchema Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow AdvLbl hon 'SlotE
 -> ExceptT
      NoSuchAdversarialChainSchema
      Identity
      (SomeWindow AdvLbl hon 'SlotE))
-> SomeWindow AdvLbl hon 'SlotE
-> ExceptT
     NoSuchAdversarialChainSchema
     Identity
     (SomeWindow AdvLbl hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ Size hon 'SlotE
-> Lbl AdvLbl -> Index hon 'SlotE -> SomeWindow AdvLbl hon 'SlotE
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl).
Size outer elem
-> Lbl lbl -> Index outer elem -> SomeWindow lbl outer elem
C.withSuffixWindow (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 lbl. Lbl lbl
forall {k} (lbl :: k). Lbl lbl
C.Lbl @AdvLbl) Index hon 'SlotE
firstAdvSlot

    -- there must be at least one honest active slot in @adv@
    case Proxy 'Inverted
-> Vector (Win AdvLbl skolem) 'SlotE S
-> Index (Win AdvLbl skolem) (PreImage 'Inverted 'EmptySlotE)
-> MaybeFound (Win AdvLbl skolem)
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 (Win AdvLbl skolem)
-> Vector hon 'SlotE S -> Vector (Win AdvLbl 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 AdvLbl skolem)
winA Vector hon 'SlotE S
vH) (Int -> Count (Win AdvLbl skolem) 'ActiveSlotE Preds
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
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 ()

    SomeCheckedAdversarialRecipe base hon
-> Except
     NoSuchAdversarialChainSchema
     (SomeCheckedAdversarialRecipe base hon)
forall a. a -> ExceptT NoSuchAdversarialChainSchema Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeCheckedAdversarialRecipe base hon
 -> Except
      NoSuchAdversarialChainSchema
      (SomeCheckedAdversarialRecipe base hon))
-> SomeCheckedAdversarialRecipe base hon
-> Except
     NoSuchAdversarialChainSchema
     (SomeCheckedAdversarialRecipe base hon)
forall a b. (a -> b) -> a -> b
$ Proxy (Win AdvLbl skolem)
-> CheckedAdversarialRecipe base hon (Win AdvLbl skolem)
-> SomeCheckedAdversarialRecipe base hon
forall base hon adv.
Proxy adv
-> CheckedAdversarialRecipe base hon adv
-> SomeCheckedAdversarialRecipe base hon
SomeCheckedAdversarialRecipe Proxy (Win AdvLbl skolem)
forall {k} (t :: k). Proxy t
Proxy (CheckedAdversarialRecipe base hon (Win AdvLbl skolem)
 -> SomeCheckedAdversarialRecipe base hon)
-> CheckedAdversarialRecipe base hon (Win AdvLbl skolem)
-> SomeCheckedAdversarialRecipe base hon
forall a b. (a -> b) -> a -> b
$ UnsafeCheckedAdversarialRecipe {
        carHonest :: ChainSchema base hon
carHonest = ChainSchema base hon
arHonest
      ,
        carParams :: (Kcp, Scg, Delta)
carParams = (Kcp, Scg, Delta)
arParams
      ,
        carWin :: Contains 'SlotE hon (Win AdvLbl skolem)
carWin    = Contains 'SlotE hon (Win AdvLbl skolem)
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
  => Maybe Asc   -- ^ 'Nothing' means @1@
  -> CheckedAdversarialRecipe base hon adv
  -> g
  -> ChainSchema base adv
{-# INLINABLE 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
    STGenM g s
g <- g -> ST s (STGenM g s)
forall g s. g -> ST s (STGenM g s)
R.newSTGenM g
g0

    let sz :: Count adv 'SlotE Total
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
    MVector adv 'SlotE s S
mv <- Count adv 'SlotE Total -> ST s S -> ST s (MVector adv 'SlotE s S)
forall {k} a base (elem :: k) s.
Unbox a =>
Size base elem -> ST s a -> ST s (MVector base elem s a)
C.replicateMV Count adv 'SlotE Total
sz (ST s S -> ST s (MVector adv 'SlotE s S))
-> ST s S -> ST s (MVector adv 'SlotE s S)
forall a b. (a -> b) -> a -> b
$ case Maybe Asc
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
trailingSlots = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
k
           szFirstActive :: Count adv 'SlotE Total
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
       Bool -> ST s () -> ST s ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Count adv 'SlotE Total
szFirstActive Count adv 'SlotE Total -> Count adv 'SlotE Total -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Count adv 'SlotE Total
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) (ST s () -> ST s ()) -> ST s () -> ST s ()
forall a b. (a -> b) -> a -> b
$
         String -> ST s ()
forall a. HasCallStack => String -> a
error String
"the adversarial schema length should be greater than s+k"
       ST s (Var adv 'ActiveSlotE) -> ST s ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ST s (Var adv 'ActiveSlotE) -> ST s ())
-> ST s (Var adv 'ActiveSlotE) -> ST s ()
forall a b. (a -> b) -> a -> b
$ Proxy 'NotInverted
-> SomeDensityWindow 'NotInverted
-> STGenM g s
-> MVector adv 'SlotE s S
-> ST s (Var adv (PreImage 'NotInverted '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 'NotInverted
S.notInverted
            (Var adv (PreImage 'NotInverted 'ActiveSlotE)
-> Count adv 'SlotE Total -> SomeDensityWindow 'NotInverted
forall (pol :: Pol) slidingWindow.
Var slidingWindow (PreImage pol 'ActiveSlotE)
-> Size slidingWindow 'SlotE -> SomeDensityWindow pol
BV.SomeDensityWindow (Int -> Var adv 'ActiveSlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
1) Count adv 'SlotE Total
szFirstActive)
            STGenM g s
g
            (Contains 'SlotE adv adv
-> MVector adv 'SlotE s S -> MVector adv '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 (Index adv 'SlotE
-> Count adv 'SlotE Total -> Contains 'SlotE adv adv
forall kelem (elem :: kelem) outer inner.
Index outer elem -> Size inner elem -> Contains elem outer inner
C.UnsafeContains (Int -> Index adv 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) Count adv 'SlotE Total
szFirstActive) MVector adv 'SlotE s S
mv)

    -- find the slot of the k+1 honest block
    let kPlus1st :: C.Index adv SlotE
        kPlus1st :: 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
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.
    Index adv 'SlotE
firstActive <- Proxy 'Inverted
-> MVector adv 'SlotE s S
-> Index adv (PreImage 'Inverted 'EmptySlotE)
-> ST s (MaybeFound adv)
forall (proxy :: Pol -> *) (pol :: Pol) base s.
POL pol =>
proxy pol
-> MVector base 'SlotE s S
-> Index base (PreImage pol 'EmptySlotE)
-> ST s (MaybeFound base)
BV.findIthEmptyInMV Proxy 'Inverted
S.inverted MVector adv 'SlotE s S
mv (Int -> Count adv 'ActiveSlotE Preds
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) ST s (MaybeFound adv)
-> (MaybeFound adv -> ST s (Index adv 'SlotE))
-> ST s (Index adv 'SlotE)
forall a b. ST s a -> (a -> ST s b) -> ST s b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \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

    Index adv 'SlotE
-> Race adv -> STGenM g s -> MVector adv 'SlotE s S -> ST s ()
forall sg s.
StatefulGen sg (ST s) =>
Index adv 'SlotE
-> Race adv -> sg -> MVector adv 'SlotE s S -> ST s ()
ensureLowerDensityInWindows Index adv 'SlotE
firstActive Race adv
iterH STGenM g s
g MVector adv 'SlotE s S
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.
    Index adv 'SlotE
-> Index adv 'SlotE
-> MaybeYS adv
-> Race adv
-> STGenM g s
-> MVector adv 'SlotE s S
-> ST s ()
forall {p} {s}.
StatefulGen p (ST s) =>
Index adv 'SlotE
-> Index adv 'SlotE
-> MaybeYS adv
-> Race adv
-> p
-> MVector adv 'SlotE s S
-> ST s ()
unfillRaces Index adv 'SlotE
kPlus1st (Index adv 'SlotE
firstActive 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) MaybeYS adv
forall base. MaybeYS base
UnknownYS Race adv
iterH STGenM g s
g MVector adv 'SlotE s S
mv

    -- Fill active slots after the stability window to ensure the alternative
    -- schema has more than k active slots
    let trailingSlots :: Int
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
    [Int] -> (Int -> ST s ()) -> ST s ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
t a -> (a -> m b) -> m ()
forM_ [Int
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
1] ((Int -> ST s ()) -> ST s ()) -> (Int -> ST s ()) -> ST s ()
forall a b. (a -> b) -> a -> b
$ \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)

    MVector adv 'SlotE s S -> ST s (MVector adv 'SlotE s S)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MVector adv 'SlotE s S
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
-> p
-> MVector adv 'SlotE s S
-> ST s ()
unfillRaces Index adv 'SlotE
kPlus1st !Index adv 'SlotE
scope !MaybeYS adv
mbYS !Race adv
iter !p
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 skolem
Proxy Contains 'SlotE adv (Win RaceLbl skolem)
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 skolem
Proxy :: Proxy skolem) Contains 'SlotE adv (Win RaceAssumptionLbl skolem)
win <-
            SomeWindow RaceAssumptionLbl adv 'SlotE
-> ST s (SomeWindow RaceAssumptionLbl adv 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          (SomeWindow RaceAssumptionLbl adv 'SlotE
 -> ST s (SomeWindow RaceAssumptionLbl adv 'SlotE))
-> SomeWindow RaceAssumptionLbl adv 'SlotE
-> ST s (SomeWindow RaceAssumptionLbl adv 'SlotE)
forall a b. (a -> b) -> a -> b
$ Count adv 'SlotE Total
-> Lbl RaceAssumptionLbl
-> Index adv 'SlotE
-> Index adv 'SlotE
-> SomeWindow RaceAssumptionLbl 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 @RaceAssumptionLbl)
                (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.windowLast  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
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 Index adv 'SlotE
_ = Index adv 'SlotE
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  Var adv 'EmptySlotE
untouchZeroCount :: C.Var adv EmptySlotE <- do
                C.SomeWindow Proxy skolem
Proxy Contains 'SlotE adv (Win UntouchableLbl skolem)
untouch <-   -- untouchable slots
                    SomeWindow UntouchableLbl adv 'SlotE
-> ST s (SomeWindow UntouchableLbl adv 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
                  (SomeWindow UntouchableLbl adv 'SlotE
 -> ST s (SomeWindow UntouchableLbl adv 'SlotE))
-> SomeWindow UntouchableLbl adv 'SlotE
-> ST s (SomeWindow UntouchableLbl adv 'SlotE)
forall a b. (a -> b) -> a -> b
$ Count adv 'SlotE Total
-> Lbl UntouchableLbl
-> Index adv 'SlotE
-> Index adv 'SlotE
-> SomeWindow UntouchableLbl 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 @UntouchableLbl)
                        (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
scope 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)   -- window will be empty if scope is 0
                Contains 'SlotE adv (Win UntouchableLbl skolem)
-> Var (Win UntouchableLbl 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 UntouchableLbl skolem)
untouch (Var (Win UntouchableLbl skolem) 'EmptySlotE
 -> Var adv 'EmptySlotE)
-> ST s (Var (Win UntouchableLbl skolem) 'EmptySlotE)
-> ST s (Var adv 'EmptySlotE)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy 'Inverted
-> MVector (Win UntouchableLbl skolem) 'SlotE s S
-> ST
     s
     (Var (Win UntouchableLbl skolem) (PreImage 'Inverted 'ActiveSlotE))
forall (pol :: Pol) (proxy :: Pol -> *) base s.
POL pol =>
proxy pol
-> MVector base 'SlotE s S
-> ST s (Var base (PreImage pol 'ActiveSlotE))
BV.countActivesInMV Proxy 'Inverted
S.inverted (Contains 'SlotE adv (Win UntouchableLbl skolem)
-> MVector adv 'SlotE s S
-> MVector (Win UntouchableLbl skolem) '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 adv (Win UntouchableLbl skolem)
untouch MVector adv 'SlotE s S
mv)

            C.SomeWindow (Proxy skolem
Proxy :: Proxy skolem2) Contains 'SlotE adv (Win TouchableLbl skolem)
touch <-   -- touchable slots
                SomeWindow TouchableLbl adv 'SlotE
-> ST s (SomeWindow TouchableLbl adv 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
              (SomeWindow TouchableLbl adv 'SlotE
 -> ST s (SomeWindow TouchableLbl adv 'SlotE))
-> SomeWindow TouchableLbl adv 'SlotE
-> ST s (SomeWindow TouchableLbl adv 'SlotE)
forall a b. (a -> b) -> a -> b
$ Count adv 'SlotE Total
-> Lbl TouchableLbl
-> Index adv 'SlotE
-> Index adv 'SlotE
-> SomeWindow TouchableLbl 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 @TouchableLbl)
                    Index adv 'SlotE
scope
                    (Contains 'SlotE adv (Win RaceLbl skolem) -> Index adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast 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
d)


            let
              maxActive :: C.Var (C.Win RaceAssumptionLbl skolem) ActiveSlotE
              maxActive :: Var (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 :: Var (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
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

            ST s (Var (Win TouchableLbl skolem) 'EmptySlotE) -> ST s ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ST s (Var (Win TouchableLbl skolem) 'EmptySlotE) -> ST s ())
-> ST s (Var (Win TouchableLbl skolem) 'EmptySlotE) -> ST s ()
forall a b. (a -> b) -> a -> b
$ Proxy 'Inverted
-> SomeDensityWindow 'Inverted
-> p
-> MVector (Win TouchableLbl skolem) 'SlotE s S
-> ST
     s (Var (Win TouchableLbl skolem) (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 (Win TouchableLbl skolem) (PreImage 'Inverted 'ActiveSlotE)
-> Size (Win TouchableLbl skolem) 'SlotE
-> SomeDensityWindow 'Inverted
forall (pol :: Pol) slidingWindow.
Var slidingWindow (PreImage pol 'ActiveSlotE)
-> Size slidingWindow 'SlotE -> SomeDensityWindow pol
BV.SomeDensityWindow (Contains 'SlotE adv (Win TouchableLbl skolem)
-> Var adv 'EmptySlotE -> Var (Win TouchableLbl skolem) 'EmptySlotE
forall {kelem1} {kelem2} (elem :: kelem1) outer inner
       (x :: kelem2).
Contains elem outer inner -> Var outer x -> Var inner x
C.toWindowVar Contains 'SlotE adv (Win TouchableLbl skolem)
touch Var adv 'EmptySlotE
touchableEmpty) (Contains 'SlotE adv (Win TouchableLbl skolem)
-> Size (Win TouchableLbl skolem) 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE adv (Win TouchableLbl skolem)
touch))
                p
g
                (Contains 'SlotE adv (Win TouchableLbl skolem)
-> MVector adv 'SlotE s S
-> MVector (Win TouchableLbl skolem) '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 adv (Win TouchableLbl skolem)
touch MVector adv 'SlotE s S
mv)

        case 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
vHAfterIntersection Race adv
iter
              Maybe (Race adv) -> Maybe (Race adv) -> Maybe (Race adv)
forall a. Maybe a -> Maybe a -> Maybe a
forall (f :: * -> *) a. Alternative f => f a -> f a -> f a
<|> Vector adv 'SlotE S -> Race adv -> Maybe (Race adv)
forall base. Vector base 'SlotE S -> Race base -> Maybe (Race base)
RI.nextConservative Vector adv 'SlotE S
vHAfterIntersection Race adv
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 skolem
Proxy Contains 'SlotE adv (Win RaceLbl skolem)
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
                MaybeYS adv
mbYS' <- case MaybeYS adv
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 skolem
Proxy Contains 'SlotE adv (Win SettledLbl skolem)
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)
                        MaybeFound (Win SettledLbl skolem)
mbFound <- Proxy 'Inverted
-> MVector (Win SettledLbl skolem) 'SlotE s S
-> Index (Win SettledLbl skolem) (PreImage 'Inverted 'EmptySlotE)
-> ST s (MaybeFound (Win SettledLbl skolem))
forall (proxy :: Pol -> *) (pol :: Pol) base s.
POL pol =>
proxy pol
-> MVector base 'SlotE s S
-> Index base (PreImage pol 'EmptySlotE)
-> ST s (MaybeFound base)
BV.findIthEmptyInMV Proxy 'Inverted
S.inverted (Contains 'SlotE adv (Win SettledLbl skolem)
-> MVector adv 'SlotE s S
-> MVector (Win SettledLbl skolem) '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 adv (Win SettledLbl skolem)
settledSlots MVector adv 'SlotE s S
mv) (Int -> Count (Win SettledLbl skolem) 'ActiveSlotE Preds
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0)
                        case MaybeFound (Win SettledLbl skolem)
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)
                Index adv 'SlotE
-> Index adv 'SlotE
-> MaybeYS adv
-> Race adv
-> p
-> MVector adv 'SlotE s S
-> ST s ()
unfillRaces Index adv 'SlotE
kPlus1st (Index adv 'SlotE -> Index adv 'SlotE -> Index adv 'SlotE
forall a. Ord a => a -> a -> a
max Index adv 'SlotE
scope (Contains 'SlotE adv (Win RaceAssumptionLbl skolem)
-> Index adv 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE adv (Win RaceAssumptionLbl skolem)
win 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)) MaybeYS adv
mbYS' Race adv
iter' p
g MVector adv 'SlotE s S
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)

        Var (Win RaceLbl skolem) 'ActiveSlotE
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

        ST
  s
  (Var (Win RaceLbl skolem) 'ActiveSlotE,
   Var (Win RaceLbl skolem) 'ActiveSlotE)
-> ST s ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ST
   s
   (Var (Win RaceLbl skolem) 'ActiveSlotE,
    Var (Win RaceLbl skolem) 'ActiveSlotE)
 -> ST s ())
-> ST
     s
     (Var (Win RaceLbl skolem) 'ActiveSlotE,
      Var (Win RaceLbl skolem) 'ActiveSlotE)
-> ST s ()
forall a b. (a -> b) -> a -> b
$ ((Var (Win RaceLbl skolem) 'ActiveSlotE,
  Var (Win RaceLbl skolem) 'ActiveSlotE)
 -> Contains 'SlotE adv (Win RaceLbl skolem)
 -> ST
      s
      (Var (Win RaceLbl skolem) 'ActiveSlotE,
       Var (Win RaceLbl skolem) 'ActiveSlotE))
-> (Var (Win RaceLbl skolem) 'ActiveSlotE,
    Var (Win RaceLbl skolem) 'ActiveSlotE)
-> [Contains 'SlotE adv (Win RaceLbl skolem)]
-> ST
     s
     (Var (Win RaceLbl skolem) 'ActiveSlotE,
      Var (Win RaceLbl skolem) 'ActiveSlotE)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM
          (Var (Win RaceLbl skolem) 'ActiveSlotE,
 Var (Win RaceLbl skolem) 'ActiveSlotE)
-> Contains 'SlotE adv (Win RaceLbl skolem)
-> ST
     s
     (Var (Win RaceLbl skolem) 'ActiveSlotE,
      Var (Win RaceLbl skolem) 'ActiveSlotE)
forall {base}.
(Count base 'ActiveSlotE Other, Count base 'ActiveSlotE Other)
-> Contains 'SlotE adv base
-> ST
     s (Count base 'ActiveSlotE Other, Count base 'ActiveSlotE Other)
updateDensityOfMv
          (Var (Win RaceLbl skolem) 'ActiveSlotE
hCount, Var (Win RaceLbl skolem) 'ActiveSlotE
aCount)
          (Contains 'SlotE adv (Win RaceLbl skolem)
-> [Contains 'SlotE adv (Win RaceLbl skolem)]
forall {kelem} {elem :: kelem} {outer} {base} {inner}.
Contains elem outer base -> [Contains elem outer inner]
stablePrefixWindowsContaining Contains 'SlotE adv (Win RaceLbl skolem)
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
sizeInt -> 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
          Bool
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' :: Count base 'ActiveSlotE Other
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 :: Bool
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' :: Count base 'ActiveSlotE Other
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

          Count base 'ActiveSlotE Other
ac'' <-
              if Count base 'ActiveSlotE Other
ac' Count base 'ActiveSlotE Other
-> Count base 'ActiveSlotE Other -> Bool
forall a. Ord a => a -> a -> Bool
>= Count base 'ActiveSlotE Other
hc' then
                Index adv 'SlotE
-> Contains 'SlotE adv base
-> sg
-> MVector adv 'SlotE s S
-> Count base 'ActiveSlotE Other
-> ST s (Count base 'ActiveSlotE Other)
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 base
w sg
g MVector adv 'SlotE s S
mv Count base 'ActiveSlotE Other
hc'
              else
                Count base 'ActiveSlotE Other
-> ST s (Count base 'ActiveSlotE Other)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Count base 'ActiveSlotE Other
ac'

          (Count base 'ActiveSlotE Other, Count base 'ActiveSlotE Other)
-> ST
     s (Count base 'ActiveSlotE Other, Count base 'ActiveSlotE Other)
forall a. a -> ST s a
forall (m :: * -> *) a. Monad m => a -> m a
return (Count base 'ActiveSlotE Other
hc', Count base 'ActiveSlotE Other
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

        Var base 'EmptySlotE
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

        Var base 'ActiveSlotE -> ST s (Var base 'ActiveSlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var base 'ActiveSlotE -> ST s (Var base 'ActiveSlotE))
-> Var base 'ActiveSlotE -> ST s (Var base 'ActiveSlotE)
forall a b. (a -> b) -> a -> b
$ Var base 'ActiveSlotE -> Var base 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Var base elem
C.toVar (Var base 'ActiveSlotE -> Var base 'ActiveSlotE)
-> Var base 'ActiveSlotE -> Var base 'ActiveSlotE
forall a b. (a -> b) -> a -> b
$ Proxy 'Inverted
-> Size base 'SlotE
-> Count base (PreImage 'Inverted 'ActiveSlotE) Other
-> Count base (PreImage 'Inverted '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 'Inverted
S.inverted (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 'Inverted 'ActiveSlotE) Other
Var base 'EmptySlotE
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