{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ViewPatterns #-}

module Test.Ouroboros.Consensus.ChainGenerator.Honest (
    -- * Generating
    ChainSchema (ChainSchema)
  , CheckedHonestRecipe (UnsafeCheckedHonestRecipe, chrScgDensity, chrWin)
  , HonestLbl
  , HonestRecipe (HonestRecipe)
  , NoSuchHonestChainSchema (BadKcp, BadLen)
  , SomeCheckedHonestRecipe (SomeCheckedHonestRecipe)
  , SomeHonestChainSchema (SomeHonestChainSchema)
  , checkHonestRecipe
  , countChainSchema
  , genHonestRecipe
  , uniformTheHonestChain
    -- * Testing
  , HonestChainViolation (BadCount, BadScgWindow, BadLength)
  , ScgLbl
  , ScgViolation (ScgViolation, scgvPopCount, scgvWindow)
  , checkHonestChain
  , prettyChainSchema
  , prettyWindow
  ) where

import           Control.Monad (void, when)
import qualified Control.Monad.Except as Exn
import           Data.Monoid (Endo (Endo, appEndo))
import           Data.Proxy (Proxy (Proxy))
import           Data.STRef (newSTRef, readSTRef, writeSTRef)
import qualified Data.Vector.Unboxed as V
import           Prelude hiding (words)
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.Params (Asc,
                     Delta (Delta), Kcp (Kcp), Len (Len), Scg (Scg), genKSD)
import qualified Test.Ouroboros.Consensus.ChainGenerator.Slot as S
import           Test.Ouroboros.Consensus.ChainGenerator.Slot
                     (E (ActiveSlotE, SlotE), S)
import qualified Test.Ouroboros.Consensus.ChainGenerator.Some as Some
import qualified Test.QuickCheck as QC
import           Test.QuickCheck.Extras (sized1)

-----

-- | The argument of checkHonestRecipe'
data HonestRecipe = HonestRecipe !Kcp !Scg !Delta !Len
  deriving (HonestRecipe -> HonestRecipe -> Bool
(HonestRecipe -> HonestRecipe -> Bool)
-> (HonestRecipe -> HonestRecipe -> Bool) -> Eq HonestRecipe
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: HonestRecipe -> HonestRecipe -> Bool
== :: HonestRecipe -> HonestRecipe -> Bool
$c/= :: HonestRecipe -> HonestRecipe -> Bool
/= :: HonestRecipe -> HonestRecipe -> Bool
Eq, ReadPrec [HonestRecipe]
ReadPrec HonestRecipe
Int -> ReadS HonestRecipe
ReadS [HonestRecipe]
(Int -> ReadS HonestRecipe)
-> ReadS [HonestRecipe]
-> ReadPrec HonestRecipe
-> ReadPrec [HonestRecipe]
-> Read HonestRecipe
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS HonestRecipe
readsPrec :: Int -> ReadS HonestRecipe
$creadList :: ReadS [HonestRecipe]
readList :: ReadS [HonestRecipe]
$creadPrec :: ReadPrec HonestRecipe
readPrec :: ReadPrec HonestRecipe
$creadListPrec :: ReadPrec [HonestRecipe]
readListPrec :: ReadPrec [HonestRecipe]
Read, Int -> HonestRecipe -> ShowS
[HonestRecipe] -> ShowS
HonestRecipe -> String
(Int -> HonestRecipe -> ShowS)
-> (HonestRecipe -> String)
-> ([HonestRecipe] -> ShowS)
-> Show HonestRecipe
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> HonestRecipe -> ShowS
showsPrec :: Int -> HonestRecipe -> ShowS
$cshow :: HonestRecipe -> String
show :: HonestRecipe -> String
$cshowList :: [HonestRecipe] -> ShowS
showList :: [HonestRecipe] -> ShowS
Show)

-- | The argument of 'uniformTheHonestChain' and the output of 'checkHonestRecipe'
--
-- * @base@ the type-level name of the top-level timeline
-- * @hon@ the type-level name of the honest chain's slot interval
--
-- TODO: Rename to CheckedHonestSchemaSpec
data CheckedHonestRecipe base hon = UnsafeCheckedHonestRecipe {
    -- | Desired density
    forall base hon.
CheckedHonestRecipe base hon -> SomeDensityWindow 'NotInverted
chrScgDensity :: !(BV.SomeDensityWindow S.NotInverted)
  , -- | Window in the @base@ containing sequence where the density should be
    -- ensured
    forall base hon.
CheckedHonestRecipe base hon -> Contains 'SlotE base hon
chrWin        :: !(C.Contains SlotE base hon)
  }
  deriving (CheckedHonestRecipe base hon
-> CheckedHonestRecipe base hon -> Bool
(CheckedHonestRecipe base hon
 -> CheckedHonestRecipe base hon -> Bool)
-> (CheckedHonestRecipe base hon
    -> CheckedHonestRecipe base hon -> Bool)
-> Eq (CheckedHonestRecipe base hon)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall base hon.
CheckedHonestRecipe base hon
-> CheckedHonestRecipe base hon -> Bool
$c== :: forall base hon.
CheckedHonestRecipe base hon
-> CheckedHonestRecipe base hon -> Bool
== :: CheckedHonestRecipe base hon
-> CheckedHonestRecipe base hon -> Bool
$c/= :: forall base hon.
CheckedHonestRecipe base hon
-> CheckedHonestRecipe base hon -> Bool
/= :: CheckedHonestRecipe base hon
-> CheckedHonestRecipe base hon -> Bool
Eq, ReadPrec [CheckedHonestRecipe base hon]
ReadPrec (CheckedHonestRecipe base hon)
Int -> ReadS (CheckedHonestRecipe base hon)
ReadS [CheckedHonestRecipe base hon]
(Int -> ReadS (CheckedHonestRecipe base hon))
-> ReadS [CheckedHonestRecipe base hon]
-> ReadPrec (CheckedHonestRecipe base hon)
-> ReadPrec [CheckedHonestRecipe base hon]
-> Read (CheckedHonestRecipe base hon)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall base hon. ReadPrec [CheckedHonestRecipe base hon]
forall base hon. ReadPrec (CheckedHonestRecipe base hon)
forall base hon. Int -> ReadS (CheckedHonestRecipe base hon)
forall base hon. ReadS [CheckedHonestRecipe base hon]
$creadsPrec :: forall base hon. Int -> ReadS (CheckedHonestRecipe base hon)
readsPrec :: Int -> ReadS (CheckedHonestRecipe base hon)
$creadList :: forall base hon. ReadS [CheckedHonestRecipe base hon]
readList :: ReadS [CheckedHonestRecipe base hon]
$creadPrec :: forall base hon. ReadPrec (CheckedHonestRecipe base hon)
readPrec :: ReadPrec (CheckedHonestRecipe base hon)
$creadListPrec :: forall base hon. ReadPrec [CheckedHonestRecipe base hon]
readListPrec :: ReadPrec [CheckedHonestRecipe base hon]
Read, Int -> CheckedHonestRecipe base hon -> ShowS
[CheckedHonestRecipe base hon] -> ShowS
CheckedHonestRecipe base hon -> String
(Int -> CheckedHonestRecipe base hon -> ShowS)
-> (CheckedHonestRecipe base hon -> String)
-> ([CheckedHonestRecipe base hon] -> ShowS)
-> Show (CheckedHonestRecipe base hon)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall base hon. Int -> CheckedHonestRecipe base hon -> ShowS
forall base hon. [CheckedHonestRecipe base hon] -> ShowS
forall base hon. CheckedHonestRecipe base hon -> String
$cshowsPrec :: forall base hon. Int -> CheckedHonestRecipe base hon -> ShowS
showsPrec :: Int -> CheckedHonestRecipe base hon -> ShowS
$cshow :: forall base hon. CheckedHonestRecipe base hon -> String
show :: CheckedHonestRecipe base hon -> String
$cshowList :: forall base hon. [CheckedHonestRecipe base hon] -> ShowS
showList :: [CheckedHonestRecipe base hon] -> ShowS
Show)

-- TODO: Rename to SomeCheckedHonestSpec
data SomeCheckedHonestRecipe =
    forall base hon.
    SomeCheckedHonestRecipe
        !(Proxy base)
        !(Proxy hon)
        !(CheckedHonestRecipe base hon)

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

instance Read SomeCheckedHonestRecipe where
    readPrec :: ReadPrec SomeCheckedHonestRecipe
readPrec =
        ReadBuilder SomeCheckedHonestRecipe
-> ReadPrec SomeCheckedHonestRecipe
forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
Some.runReadPrec
      (ReadBuilder SomeCheckedHonestRecipe
 -> ReadPrec SomeCheckedHonestRecipe)
-> ReadBuilder SomeCheckedHonestRecipe
-> ReadPrec SomeCheckedHonestRecipe
forall a b. (a -> b) -> a -> b
$ (Proxy Any
 -> Proxy Any
 -> CheckedHonestRecipe Any Any
 -> SomeCheckedHonestRecipe)
-> String
-> ReadBuilder
     (Proxy Any
      -> Proxy Any
      -> CheckedHonestRecipe Any Any
      -> SomeCheckedHonestRecipe)
forall a. a -> String -> ReadBuilder a
Some.readCtor Proxy Any
-> Proxy Any
-> CheckedHonestRecipe Any Any
-> SomeCheckedHonestRecipe
forall base hon.
Proxy base
-> Proxy hon
-> CheckedHonestRecipe base hon
-> SomeCheckedHonestRecipe
SomeCheckedHonestRecipe String
"SomeCheckedHonestRecipe"
            ReadBuilder
  (Proxy Any
   -> Proxy Any
   -> CheckedHonestRecipe Any Any
   -> SomeCheckedHonestRecipe)
-> ReadBuilder (Proxy Any)
-> ReadBuilder
     (Proxy Any
      -> CheckedHonestRecipe Any Any -> SomeCheckedHonestRecipe)
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
  (Proxy Any
   -> CheckedHonestRecipe Any Any -> SomeCheckedHonestRecipe)
-> ReadBuilder (Proxy Any)
-> ReadBuilder
     (CheckedHonestRecipe Any Any -> SomeCheckedHonestRecipe)
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
  (CheckedHonestRecipe Any Any -> SomeCheckedHonestRecipe)
-> ReadBuilder (CheckedHonestRecipe Any Any)
-> ReadBuilder SomeCheckedHonestRecipe
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (CheckedHonestRecipe Any Any)
forall a. Read a => ReadBuilder a
Some.readArg

data NoSuchHonestChainSchema =
    -- | must have @1 <= 'Kcp' < 'Scg'@
    --
    -- Chosing @Kcp > 0@ allows adversarial schemas to have at least 1 active
    -- slot and still lose density comparisons and races.
    BadKcp
  |
    -- | 'Len' must be positive
    BadLen
  deriving (NoSuchHonestChainSchema -> NoSuchHonestChainSchema -> Bool
(NoSuchHonestChainSchema -> NoSuchHonestChainSchema -> Bool)
-> (NoSuchHonestChainSchema -> NoSuchHonestChainSchema -> Bool)
-> Eq NoSuchHonestChainSchema
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NoSuchHonestChainSchema -> NoSuchHonestChainSchema -> Bool
== :: NoSuchHonestChainSchema -> NoSuchHonestChainSchema -> Bool
$c/= :: NoSuchHonestChainSchema -> NoSuchHonestChainSchema -> Bool
/= :: NoSuchHonestChainSchema -> NoSuchHonestChainSchema -> Bool
Eq, ReadPrec [NoSuchHonestChainSchema]
ReadPrec NoSuchHonestChainSchema
Int -> ReadS NoSuchHonestChainSchema
ReadS [NoSuchHonestChainSchema]
(Int -> ReadS NoSuchHonestChainSchema)
-> ReadS [NoSuchHonestChainSchema]
-> ReadPrec NoSuchHonestChainSchema
-> ReadPrec [NoSuchHonestChainSchema]
-> Read NoSuchHonestChainSchema
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS NoSuchHonestChainSchema
readsPrec :: Int -> ReadS NoSuchHonestChainSchema
$creadList :: ReadS [NoSuchHonestChainSchema]
readList :: ReadS [NoSuchHonestChainSchema]
$creadPrec :: ReadPrec NoSuchHonestChainSchema
readPrec :: ReadPrec NoSuchHonestChainSchema
$creadListPrec :: ReadPrec [NoSuchHonestChainSchema]
readListPrec :: ReadPrec [NoSuchHonestChainSchema]
Read, Int -> NoSuchHonestChainSchema -> ShowS
[NoSuchHonestChainSchema] -> ShowS
NoSuchHonestChainSchema -> String
(Int -> NoSuchHonestChainSchema -> ShowS)
-> (NoSuchHonestChainSchema -> String)
-> ([NoSuchHonestChainSchema] -> ShowS)
-> Show NoSuchHonestChainSchema
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NoSuchHonestChainSchema -> ShowS
showsPrec :: Int -> NoSuchHonestChainSchema -> ShowS
$cshow :: NoSuchHonestChainSchema -> String
show :: NoSuchHonestChainSchema -> String
$cshowList :: [NoSuchHonestChainSchema] -> ShowS
showList :: [NoSuchHonestChainSchema] -> ShowS
Show)

-- Note [Minimum schema length]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
--
-- We want schemas to have at least k+1 active slots after the intersection.
-- This would produce sufficiently long chains to test the long range attack and
-- rollbacks.
--
-- The minimum length is calculated to allow k+1 active slots in every schema,
-- and then allowing the intersection to be the genesis block. When the schemas
-- are longer than the minimum, chosing a later intersection is possible.
--
-- We divide the length of the schemas in the following three segments:
--
-- s + 1 | d | k
--
-- To ensure the honest schema has at least k+1 active slots, we need at least
-- the s slots, by the Extended Praos Chain Growth assumption. We draw these
-- slots from the first segment.
--
-- To ensure the alternative schema can have k+1 active slots, we reserve
-- k unstable slots at the end of the schema (this is the last of our segments),
-- and we make sure to activate one more earlier slot.
--
-- To reserve k unstable slots, we need to meet two conditions. One condition is
-- that there needs to be a gap of at lest d slots between the first unstable
-- slot and the k+1st active slot in the honest schema. This is the middle
-- segment in the schema.
--
-- The second condition for unstable slots requires that the first alternative
-- active slot after the intersection is s slots before the first unstable slot.
-- To ensure that we can activate a slot at this point or earlier, we chose k>0,
-- which we already needed to ensure that the alternative schema can have at
-- least one active slot, yet lose density and race comparisons; and we also
-- draw one more slot from the first segment to ensure there is an actual slot
-- to activate when d=0.
--
-- Therefore, to the total length is s + d + k + 1.

genHonestRecipe :: QC.Gen HonestRecipe
genHonestRecipe :: Gen HonestRecipe
genHonestRecipe = (Int -> Gen HonestRecipe) -> Gen HonestRecipe
forall a. (Int -> Gen a) -> Gen a
sized1 ((Int -> Gen HonestRecipe) -> Gen HonestRecipe)
-> (Int -> Gen HonestRecipe) -> Gen HonestRecipe
forall a b. (a -> b) -> a -> b
$ \Int
sz -> do
    (Kcp Int
k, Scg Int
s, Delta Int
d) <- Gen (Kcp, Scg, Delta)
genKSD
    -- See Note [Minimum schema length].
    Int
l <- (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (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)) (Int -> Int) -> Gen Int -> Gen Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (Int
0, Int
5 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
sz)
    HonestRecipe -> Gen HonestRecipe
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (HonestRecipe -> Gen HonestRecipe)
-> HonestRecipe -> Gen HonestRecipe
forall a b. (a -> b) -> a -> b
$ Kcp -> Scg -> Delta -> Len -> HonestRecipe
HonestRecipe (Int -> Kcp
Kcp Int
k) (Int -> Scg
Scg Int
s) (Int -> Delta
Delta Int
d) (Int -> Len
Len Int
l)

-- | Checks whether the given 'HonestRecipe' determines a valid input to
-- 'uniformTheHonestChain'
checkHonestRecipe :: HonestRecipe -> Exn.Except NoSuchHonestChainSchema SomeCheckedHonestRecipe
checkHonestRecipe :: HonestRecipe
-> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe
checkHonestRecipe HonestRecipe
recipe = do
    Bool
-> ExceptT NoSuchHonestChainSchema Identity ()
-> ExceptT NoSuchHonestChainSchema Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
l Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0) (ExceptT NoSuchHonestChainSchema Identity ()
 -> ExceptT NoSuchHonestChainSchema Identity ())
-> ExceptT NoSuchHonestChainSchema Identity ()
-> ExceptT NoSuchHonestChainSchema Identity ()
forall a b. (a -> b) -> a -> b
$ NoSuchHonestChainSchema
-> ExceptT NoSuchHonestChainSchema Identity ()
forall a.
NoSuchHonestChainSchema
-> ExceptT NoSuchHonestChainSchema Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError NoSuchHonestChainSchema
BadLen

    Bool
-> ExceptT NoSuchHonestChainSchema Identity ()
-> ExceptT NoSuchHonestChainSchema Identity ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 Bool -> Bool -> Bool
|| Int
s Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k) (ExceptT NoSuchHonestChainSchema Identity ()
 -> ExceptT NoSuchHonestChainSchema Identity ())
-> ExceptT NoSuchHonestChainSchema Identity ()
-> ExceptT NoSuchHonestChainSchema Identity ()
forall a b. (a -> b) -> a -> b
$ NoSuchHonestChainSchema
-> ExceptT NoSuchHonestChainSchema Identity ()
forall a.
NoSuchHonestChainSchema
-> ExceptT NoSuchHonestChainSchema Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError NoSuchHonestChainSchema
BadKcp

    Lbl HonestLbl
-> Int
-> (forall {base}.
    Proxy base
    -> SomeWindow HonestLbl base 'SlotE
    -> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe)
-> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe
forall {k1} {k2} (lbl :: k1) (elem :: k2) ans.
Lbl lbl
-> Int
-> (forall base. Proxy base -> SomeWindow lbl base elem -> ans)
-> ans
C.withTopWindow (forall lbl. Lbl lbl
forall {k} (lbl :: k). Lbl lbl
C.Lbl @HonestLbl) Int
l ((forall {base}.
  Proxy base
  -> SomeWindow HonestLbl base 'SlotE
  -> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe)
 -> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe)
-> (forall {base}.
    Proxy base
    -> SomeWindow HonestLbl base 'SlotE
    -> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe)
-> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe
forall a b. (a -> b) -> a -> b
$ \Proxy base
base SomeWindow HonestLbl base 'SlotE
topWindow -> do
        C.SomeWindow Proxy skolem
Proxy Contains 'SlotE base (Win HonestLbl skolem)
slots <- SomeWindow HonestLbl base 'SlotE
-> ExceptT
     NoSuchHonestChainSchema Identity (SomeWindow HonestLbl base 'SlotE)
forall a. a -> ExceptT NoSuchHonestChainSchema Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeWindow HonestLbl base 'SlotE
topWindow

        SomeCheckedHonestRecipe
-> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe
forall a. a -> ExceptT NoSuchHonestChainSchema Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeCheckedHonestRecipe
 -> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe)
-> SomeCheckedHonestRecipe
-> Except NoSuchHonestChainSchema SomeCheckedHonestRecipe
forall a b. (a -> b) -> a -> b
$ Proxy base
-> Proxy (Win HonestLbl skolem)
-> CheckedHonestRecipe base (Win HonestLbl skolem)
-> SomeCheckedHonestRecipe
forall base hon.
Proxy base
-> Proxy hon
-> CheckedHonestRecipe base hon
-> SomeCheckedHonestRecipe
SomeCheckedHonestRecipe Proxy base
base Proxy (Win HonestLbl skolem)
forall {k} (t :: k). Proxy t
Proxy UnsafeCheckedHonestRecipe {
            chrScgDensity :: SomeDensityWindow 'NotInverted
chrScgDensity = Var Any (PreImage 'NotInverted 'ActiveSlotE)
-> Size Any 'SlotE -> SomeDensityWindow 'NotInverted
forall (pol :: Pol) slidingWindow.
Var slidingWindow (PreImage pol 'ActiveSlotE)
-> Size slidingWindow 'SlotE -> SomeDensityWindow pol
BV.SomeDensityWindow (Int -> Count Any 'ActiveSlotE Other
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)) (Int -> Size Any 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
s)
          ,
            chrWin :: Contains 'SlotE base (Win HonestLbl skolem)
chrWin        = Contains 'SlotE base (Win HonestLbl skolem)
slots
          }
  where
    HonestRecipe (Kcp Int
k) (Scg Int
s) (Delta Int
_d) (Len Int
l) = HonestRecipe
recipe

-----

-- | The leader schedule of an honest /chain/
--
-- The represented chain grows by one block per active slot. A different data
-- type would represent a leader schedule in which leaders do not necessarily
-- extend the block from the previous active slot.
--
-- INVARIANT: at least one active slot
data ChainSchema base inner =
    ChainSchema
        !(C.Contains SlotE base inner)
        !(C.Vector inner SlotE S)
  deriving (ChainSchema base inner -> ChainSchema base inner -> Bool
(ChainSchema base inner -> ChainSchema base inner -> Bool)
-> (ChainSchema base inner -> ChainSchema base inner -> Bool)
-> Eq (ChainSchema base inner)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall base inner.
ChainSchema base inner -> ChainSchema base inner -> Bool
$c== :: forall base inner.
ChainSchema base inner -> ChainSchema base inner -> Bool
== :: ChainSchema base inner -> ChainSchema base inner -> Bool
$c/= :: forall base inner.
ChainSchema base inner -> ChainSchema base inner -> Bool
/= :: ChainSchema base inner -> ChainSchema base inner -> Bool
Eq, ReadPrec [ChainSchema base inner]
ReadPrec (ChainSchema base inner)
Int -> ReadS (ChainSchema base inner)
ReadS [ChainSchema base inner]
(Int -> ReadS (ChainSchema base inner))
-> ReadS [ChainSchema base inner]
-> ReadPrec (ChainSchema base inner)
-> ReadPrec [ChainSchema base inner]
-> Read (ChainSchema base inner)
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
forall base inner. ReadPrec [ChainSchema base inner]
forall base inner. ReadPrec (ChainSchema base inner)
forall base inner. Int -> ReadS (ChainSchema base inner)
forall base inner. ReadS [ChainSchema base inner]
$creadsPrec :: forall base inner. Int -> ReadS (ChainSchema base inner)
readsPrec :: Int -> ReadS (ChainSchema base inner)
$creadList :: forall base inner. ReadS [ChainSchema base inner]
readList :: ReadS [ChainSchema base inner]
$creadPrec :: forall base inner. ReadPrec (ChainSchema base inner)
readPrec :: ReadPrec (ChainSchema base inner)
$creadListPrec :: forall base inner. ReadPrec [ChainSchema base inner]
readListPrec :: ReadPrec [ChainSchema base inner]
Read, Int -> ChainSchema base inner -> ShowS
[ChainSchema base inner] -> ShowS
ChainSchema base inner -> String
(Int -> ChainSchema base inner -> ShowS)
-> (ChainSchema base inner -> String)
-> ([ChainSchema base inner] -> ShowS)
-> Show (ChainSchema base inner)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall base inner. Int -> ChainSchema base inner -> ShowS
forall base inner. [ChainSchema base inner] -> ShowS
forall base inner. ChainSchema base inner -> String
$cshowsPrec :: forall base inner. Int -> ChainSchema base inner -> ShowS
showsPrec :: Int -> ChainSchema base inner -> ShowS
$cshow :: forall base inner. ChainSchema base inner -> String
show :: ChainSchema base inner -> String
$cshowList :: forall base inner. [ChainSchema base inner] -> ShowS
showList :: [ChainSchema base inner] -> ShowS
Show)

countChainSchema :: ChainSchema base inner -> C.Size inner ActiveSlotE
countChainSchema :: forall base inner.
ChainSchema base inner -> Size inner 'ActiveSlotE
countChainSchema ChainSchema base inner
sched =
    Proxy 'NotInverted
-> Vector inner 'SlotE S
-> Size inner (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 inner 'SlotE S
v
  where
    ChainSchema Contains 'SlotE base inner
_slots Vector inner 'SlotE S
v = ChainSchema base inner
sched

prettyWindow :: C.Contains SlotE base inner -> String -> String
prettyWindow :: forall base inner. Contains 'SlotE base inner -> ShowS
prettyWindow Contains 'SlotE base inner
win String
s =
    -- for example, i=0 n=1 should be "[)"
    Int -> Char -> String
forall a. Int -> a -> [a]
replicate Int
i Char
' ' String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"[" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
theOpenBracket) Char
' ' String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
")" String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
s
  where
    C.Count Int
i = Contains 'SlotE base inner -> Count base 'SlotE Preds
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE base inner
win
    C.Count Int
n = Contains 'SlotE base inner -> Count inner 'SlotE Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE base inner
win

    theOpenBracket :: Int
theOpenBracket = Int
1

prettyChainSchema ::
  forall base inner.
     ChainSchema base inner
  -> String
  -> [String]
prettyChainSchema :: forall base inner. ChainSchema base inner -> String -> [String]
prettyChainSchema ChainSchema base inner
sched String
s =
    ShowS -> [String] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Char -> String
forall a. Int -> a -> [a]
replicate (Count base 'SlotE Preds -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Count base 'SlotE Preds
shift) Char
' ' String -> ShowS
forall a. Semigroup a => a -> a -> a
<>)
  ([String] -> [String]) -> [String] -> [String]
forall a b. (a -> b) -> a -> b
$ [ Contains 'SlotE base inner -> ShowS
forall base inner. Contains 'SlotE base inner -> ShowS
prettyWindow Contains 'SlotE base inner
slots String
s
    , (S -> Endo String) -> Vector S -> Endo String
forall m a. (Monoid m, Unbox a) => (a -> m) -> Vector a -> m
V.foldMap (ShowS -> Endo String
forall a. (a -> a) -> Endo a
Endo (ShowS -> Endo String) -> (S -> ShowS) -> S -> Endo String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. S -> ShowS
S.showS) (Vector inner 'SlotE S -> Vector S
forall {k1} {k2} (base :: k1) (elem :: k2) a.
Vector base elem a -> Vector a
C.getVector Vector inner 'SlotE S
v) Endo String -> ShowS
forall a. Endo a -> a -> a
`appEndo` String
""
    ]
  where
    ChainSchema Contains 'SlotE base inner
slots Vector inner 'SlotE S
v = ChainSchema base inner
sched

    shift :: Count base 'SlotE Preds
shift = Contains 'SlotE base inner -> Count base 'SlotE Preds
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE base inner
slots

data SomeHonestChainSchema =
     forall base hon.
     SomeHonestChainSchema
         !(Proxy base)
         !(Proxy hon)
         !(ChainSchema base hon)

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

instance Read SomeHonestChainSchema where
    readPrec :: ReadPrec SomeHonestChainSchema
readPrec =
        ReadBuilder SomeHonestChainSchema -> ReadPrec SomeHonestChainSchema
forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
Some.runReadPrec
      (ReadBuilder SomeHonestChainSchema
 -> ReadPrec SomeHonestChainSchema)
-> ReadBuilder SomeHonestChainSchema
-> ReadPrec SomeHonestChainSchema
forall a b. (a -> b) -> a -> b
$ (Proxy Any
 -> Proxy Any -> ChainSchema Any Any -> SomeHonestChainSchema)
-> String
-> ReadBuilder
     (Proxy Any
      -> Proxy Any -> ChainSchema Any Any -> SomeHonestChainSchema)
forall a. a -> String -> ReadBuilder a
Some.readCtor Proxy Any
-> Proxy Any -> ChainSchema Any Any -> SomeHonestChainSchema
forall base hon.
Proxy base
-> Proxy hon -> ChainSchema base hon -> SomeHonestChainSchema
SomeHonestChainSchema String
"SomeHonestChainSchema"
            ReadBuilder
  (Proxy Any
   -> Proxy Any -> ChainSchema Any Any -> SomeHonestChainSchema)
-> ReadBuilder (Proxy Any)
-> ReadBuilder
     (Proxy Any -> ChainSchema Any Any -> SomeHonestChainSchema)
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
  (Proxy Any -> ChainSchema Any Any -> SomeHonestChainSchema)
-> ReadBuilder (Proxy Any)
-> ReadBuilder (ChainSchema Any Any -> SomeHonestChainSchema)
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 (ChainSchema Any Any -> SomeHonestChainSchema)
-> ReadBuilder (ChainSchema Any Any)
-> ReadBuilder SomeHonestChainSchema
forall a b. ReadBuilder (a -> b) -> ReadBuilder a -> ReadBuilder b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ReadBuilder (ChainSchema Any Any)
forall a. Read a => ReadBuilder a
Some.readArg

data HonestLbl

data RemainingHcgWindowsLbl

{- TODO

Our original intent was for 'uniformTheHonestChain' to generate a chain
according to the given 'Asc' and then toggle /as few as possible/ empty slots
to active such that the Extended Chain Growth Assumption is satisfied.

However, the minimality of that is very difficult to ensure, in general. It's
an integer linear programming (ILP) problem, where:

  * Each empty slot in a sparse window is a binary aka ("zero-one") variable.

  * The objective is to minimize the sum of those binary variables.

  * Each sparse window imposes a minimum bound on the number of variables in
    that window that must be toggled.

Because all of the coefficients in the objective (the minimization) and each
constraint (one per window) are positive, this is a /set covering problem/:
each variable is an empty slot in some number of sparse windows, and we want to
choose as few such slots as possible such that no sparse window remain.

Moreover, each window needs a different number of slots (because some windows
may be more sparse than others). Because some windows may require multiple
empty slots, this is a /set multi-covering problem/.

Lastly, we can only toggle an empty slot once (recall that it's a /zero-one/
variable), so this is a /set multi-cover with multiplicity constraints
problem/.

After some searching, I found this reference

  * Qiang-Sheng Hua, Yuexuan Wang, Dongxiao Yu, Francis C. M. Lau: Dynamic
    programming based algorithms for set multicover and multiset multicover
    problems. Theor. Comput. Sci. 411(26-28): 2467-2474 (2010)

which includes the claim "[...] we give the first known exact algorithm for the
MSMC or the SMC with multiplicity constraints problem".

It /may/ be the case that our problem is particularly degenerate, and so easier
to solve. In particular, our variables are binary, their coefficients in the
constraints are binary, and in fact our constraints form a banded matrix. Only
the lower bound of each constraint can be greater than 1. But I have not yet
recognized how to do it.

The closest I have come to a solution is an incremental algorithm that toggles
one empty slot at a time. I /think/ the completeness of this algorithm requires
that the next toggle is one of the empty slots that occurs in the most number
of sparse windows. However, I have not proved that. Moreover, even if it is
true, a counterexample proves that choosing an arbitrary such slot is not
sufficient:

>     A   B   C
> -----   -----
> 01110111011101110
>     -----   -----

In this example, only slots A, B, and C occur in two sparse windows, so those
are the candidates for the next toggle by my conjecture. If we suppose that
each window is only missing one active slot (eg need 4 actives per 5 slots),
then toggling B would require three toggles in total, whereas toggling A and C
would solve the problem with just two toggles.

-}

-- | A 'ChainSchema' that satisfies 'checkHonestChain'
--
-- This generator proceeds in three stages to create a random schema that
-- satisfies the requirement of at least @k+1@ blocks in every @s@ slots.
--
-- * It begins by drawing a sample of length 'Len' from the Bernoulli process
--   induced by the active slot coefficient 'Asc', just like in Praos. (IE
--   'Len' many i.i.d. samples from @Uniform(asc)@).
-- * It then visits the first window in that sampled vector. If it has less
--   than @k+1@ active slots, the generator randomly toggles empty slots to be
--   active until the window contains exactly @k+1@ active slots.
-- * It then visits the rest of the windows in oldest-to-youngest order. Each
--   window must contain at least @k@ active slots when visited, since it
--   shares all but its youngest slot with the previous window, which was
--   already visited. In particular, when the window contains only @k@ active
--   slots, that youngest slot must be empty, and so the generator will toggle
--   it, thereby re-establishing the required density.
--
-- NOTE: This process may add more active slots to the initial sampled vector
-- than strictly necessary---ensuring the minimum number of toggles would be an
-- integer programming optimization problem as far as we can tell. We have
-- settled for this relatively simple algorithm that approaches the minimal
-- number of toggled slots (TODO calculate how tight the bounds are).
--
-- NOTE: When visting windows after the first, only the youngest slot can be
-- toggled. If we activated any other slot in the sliding window, then older
-- windows, which already have at least @k+1@ active slots, would unnecessarily
-- end up with even more active slots.
--
-- NOTE: The larger 'Asc' is, the more active slots there will be when sampling
-- from the Bernoulli process. When 'Asc' is much larger than @(k+1)/s@ the
-- sample will require toggling very few additional slots.
--
-- NOTE: When no 'Asc' value is provided, we start with a vector with no active
-- slots, and the second phase causes the first window to end up with @k+1@
-- active slots in a pattern that is then repeated exactly for the rest of the
-- chain. For instance,
--
-- > k=2, s=6
-- >
-- > 000000000000000000000000 -- stage 1
-- > 1 11                     -- stage 2
-- >       1 11  1 11  1 11   -- stage 3
-- > 101100101100101100101100 -- final
--
-- > k=2, s=6
-- >
-- > 000000000000000000000000 -- stage 1
-- >    111                   -- stage 2
-- >          111   111   111 -- stage 3
-- > 000111000111000111000111 -- final
--
-- NOTE: When @'Asc'@ is close to 0, the sample will have a few active slots.
-- In the relatively common case where none of those initially active slots are
-- in the same window, the final schema will be periodic between the active
-- slots from the sample, but the patterns in those intervals may vary. For
-- instance,
--
-- > k=2, s=6
-- >
-- > 000000000000010000000000000000001000000000000000000 -- stage 1
-- > 1 1 1                                               -- stage 2
-- >       1 1 1 1   1 11  1 11  1 11    111   111   111 -- stage 3
-- > 101010101010110010110010110010111000111000111000111 -- final
--
-- TODO sample from a disjunction of generators that explore interesting
-- boundary conditions. i.e. different windows could use different strategies
-- to fill each of the windows. For instance, we could arrange for some windows
-- to start with empty slots and be dense at the end.
uniformTheHonestChain ::
  forall base hon g.
     R.RandomGen g
  => Maybe Asc   -- ^ When @Nothing@, the generated schema has a minimal amount
                 -- of active slots. Deactivating any of them would violate
                 -- safety properties. Such a minimal schema is necessarily
                 -- completely periodic.
  -> CheckedHonestRecipe base hon
  -> g
  -> ChainSchema base hon
{-# INLINABLE uniformTheHonestChain #-}
uniformTheHonestChain :: forall base hon g.
RandomGen g =>
Maybe Asc
-> CheckedHonestRecipe base hon -> g -> ChainSchema base hon
uniformTheHonestChain Maybe Asc
mbAsc CheckedHonestRecipe base hon
recipe g
g0 = Vector hon 'SlotE S -> ChainSchema base hon
wrap (Vector hon 'SlotE S -> ChainSchema base hon)
-> Vector hon 'SlotE S -> ChainSchema base hon
forall a b. (a -> b) -> a -> b
$ (forall s. ST s (MVector hon 'SlotE s S)) -> Vector hon '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 hon 'SlotE s S)) -> Vector hon 'SlotE S)
-> (forall s. ST s (MVector hon 'SlotE s S)) -> Vector hon 'SlotE S
forall a b. (a -> b) -> a -> b
$ do
    BV.SomeDensityWindow (C.Count (Int -> Var hon 'ActiveSlotE
forall a. Enum a => Int -> a
toEnum -> Var hon 'ActiveSlotE
numerator)) (C.Count (Int -> Var hon 'SlotE
forall a. Enum a => Int -> a
toEnum -> Var hon 'SlotE
denominator)) <- SomeDensityWindow 'NotInverted
-> ST s (SomeDensityWindow 'NotInverted)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure SomeDensityWindow 'NotInverted
chrScgDensity
    let Var hon 'ActiveSlotE
_ = Var hon 'ActiveSlotE
numerator   :: C.Var hon ActiveSlotE
        Var hon 'SlotE
_ = Var hon 'SlotE
denominator :: C.Var hon SlotE

    STGenM g s
g <- g -> ST s (STGenM g s)
forall g s. g -> ST s (STGenM g s)
R.newSTGenM g
g0

    -- randomly initialize the bitstring
    MVector hon 'SlotE s S
mv <- Size hon 'SlotE -> ST s S -> ST s (MVector hon '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 Size hon 'SlotE
sz (ST s S -> ST s (MVector hon 'SlotE s S))
-> ST s S -> ST s (MVector hon '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 'Inverted -> S
forall (pol :: Pol) (proxy :: Pol -> *). POL pol => proxy pol -> S
forall (proxy :: Pol -> *). proxy 'Inverted -> S
S.mkActive Proxy 'Inverted
S.inverted
        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

    -- /always/ ensure at least one slot is filled
    ST s (Var hon 'ActiveSlotE) -> ST s ()
forall (f :: * -> *) a. Functor f => f a -> f ()
void (ST s (Var hon 'ActiveSlotE) -> ST s ())
-> ST s (Var hon 'ActiveSlotE) -> ST s ()
forall a b. (a -> b) -> a -> b
$ Proxy 'NotInverted
-> SomeDensityWindow 'NotInverted
-> STGenM g s
-> MVector hon 'SlotE s S
-> ST s (Var hon (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 (Int -> Var hon 'ActiveSlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
1 Var hon (PreImage 'NotInverted 'ActiveSlotE)
-> Size hon 'SlotE -> SomeDensityWindow 'NotInverted
forall (pol :: Pol) slidingWindow.
Var slidingWindow (PreImage pol 'ActiveSlotE)
-> Size slidingWindow 'SlotE -> SomeDensityWindow pol
`BV.SomeDensityWindow` Size hon 'SlotE
sz) STGenM g s
g MVector hon 'SlotE s S
mv

    -- fill the first window up to @k+1@
    STRef s (Var hon 'ActiveSlotE)
rtot <- do
        -- NB @withWindow@ truncates if it would reach past @slots@
        C.SomeWindow Proxy skolem
Proxy Contains 'SlotE hon (Win ScgLbl skolem)
scg <- SomeWindow ScgLbl hon 'SlotE -> ST s (SomeWindow ScgLbl hon 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow ScgLbl hon 'SlotE
 -> ST s (SomeWindow ScgLbl hon 'SlotE))
-> SomeWindow ScgLbl hon 'SlotE
-> ST s (SomeWindow ScgLbl hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ Size hon 'SlotE
-> Lbl ScgLbl
-> Index hon 'SlotE
-> Size hon 'SlotE
-> SomeWindow ScgLbl hon 'SlotE
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl) x.
Size outer elem
-> Lbl lbl
-> Index outer elem
-> Size x elem
-> SomeWindow lbl outer elem
C.withWindow Size hon 'SlotE
sz (forall lbl. Lbl lbl
forall {k} (lbl :: k). Lbl lbl
C.Lbl @ScgLbl) (Int -> Index hon 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0) (Var hon 'SlotE -> Size hon 'SlotE
forall {kelem} base (elem :: kelem).
Var base elem -> Size base elem
C.toSize Var hon 'SlotE
denominator)
        Var hon 'ActiveSlotE
tot <- Contains 'SlotE hon (Win ScgLbl skolem)
-> Var (Win ScgLbl 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 ScgLbl skolem)
scg (Var (Win ScgLbl skolem) 'ActiveSlotE -> Var hon 'ActiveSlotE)
-> ST s (Var (Win ScgLbl skolem) 'ActiveSlotE)
-> ST s (Var hon 'ActiveSlotE)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proxy 'NotInverted
-> SomeDensityWindow 'NotInverted
-> STGenM g s
-> MVector (Win ScgLbl skolem) 'SlotE s S
-> ST
     s (Var (Win ScgLbl skolem) (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 SomeDensityWindow 'NotInverted
chrScgDensity STGenM g s
g (Contains 'SlotE hon (Win ScgLbl skolem)
-> MVector hon 'SlotE s S -> MVector (Win ScgLbl 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 hon (Win ScgLbl skolem)
scg MVector hon 'SlotE s S
mv)

        Bool
firstSlot <- Proxy 'NotInverted
-> MVector hon 'SlotE s S -> Index hon '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 hon 'SlotE s S
mv (Int -> Index hon 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
0)
        Var hon 'ActiveSlotE -> ST s (STRef s (Var hon 'ActiveSlotE))
forall a s. a -> ST s (STRef s a)
newSTRef (Var hon 'ActiveSlotE -> ST s (STRef s (Var hon 'ActiveSlotE)))
-> Var hon 'ActiveSlotE -> ST s (STRef s (Var hon 'ActiveSlotE))
forall a b. (a -> b) -> a -> b
$ (if Bool
firstSlot then Var hon 'ActiveSlotE
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. Num a => a -> a -> a
subtract Var hon 'ActiveSlotE
1 else Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. a -> a
id) (Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE)
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a b. (a -> b) -> a -> b
$ (Var hon 'ActiveSlotE
tot :: C.Var hon ActiveSlotE)

    C.SomeWindow Proxy skolem
Proxy Contains 'SlotE hon (Win RemainingHcgWindowsLbl skolem)
remainingFullWindows <- do
        -- "number of windows that fit" is usually "total - windowWidth + 1",
        -- but we do not add the one here because the previous init step above
        -- already handled the first window
        let numRemainingFullWindows :: Size hon 'SlotE
numRemainingFullWindows = Size hon 'SlotE
sz 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.- Var hon 'SlotE -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Var hon 'SlotE
denominator
        SomeWindow RemainingHcgWindowsLbl hon 'SlotE
-> ST s (SomeWindow RemainingHcgWindowsLbl hon 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow RemainingHcgWindowsLbl hon 'SlotE
 -> ST s (SomeWindow RemainingHcgWindowsLbl hon 'SlotE))
-> SomeWindow RemainingHcgWindowsLbl hon 'SlotE
-> ST s (SomeWindow RemainingHcgWindowsLbl hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ Size hon 'SlotE
-> Lbl RemainingHcgWindowsLbl
-> Index hon 'SlotE
-> Size hon 'SlotE
-> SomeWindow RemainingHcgWindowsLbl hon 'SlotE
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl) x.
Size outer elem
-> Lbl lbl
-> Index outer elem
-> Size x elem
-> SomeWindow lbl outer elem
C.withWindow Size hon 'SlotE
sz (forall lbl. Lbl lbl
forall {k} (lbl :: k). Lbl lbl
C.Lbl @RemainingHcgWindowsLbl) (Int -> Index hon 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
1) Size hon 'SlotE
numRemainingFullWindows

    -- visit all subsequent windows that do not reach beyond @slots@
    --
    -- Visiting a window ensures it has at least k+1 active slots; thus the
    -- first window beyond @slots@ will have at least k actives in its actual
    -- slots. We assume slots beyond @slots@ are active; thus the first window
    -- beyond has at least k+1 active slots. And subsequent windows can only have
    -- more active slots than that; thus we don't need to visit windows that
    -- reach beyond @slots@.
    --
    -- LOOP INVARIANT: @rtot@ contains the count active slots in the current window excluding its youngest slot
    --
    -- LOOP INVARIANT: @numerator - 1 <= rtot@
    --
    -- This loop only alters the final slot in each window. That is key to this
    -- whole function being a /uniform/ sampler. In particular:
    --
    --     * Every excessive empty slot in the first window has an equal chance
    --       to be filled in (by the init step above).
    --
    --     * If some subsequent window is sparse, then its final slot is filled
    --       in (by this loop). It must never fill in any older slot in the
    --       window because those slots have already been sampled (either by
    --       the init step above or by previous iterations of this loop).
    --
    --     * Every slot that was not filled in was drawn from @mbAsc@.
    --
    --     * In total: the init step uniformly fills the first window up to
    --       @numerator@, and then each slot not in the first window is either
    --       forced to @1@ by its preceding @denominator - 1@ samples or is
    --       sampled from @mbAsc@.
    Size (Win RemainingHcgWindowsLbl skolem) 'SlotE
-> (Index (Win RemainingHcgWindowsLbl skolem) 'SlotE -> ST s ())
-> ST s ()
forall {kelem} (f :: * -> *) base (elem :: kelem) a.
Applicative f =>
Size base elem -> (Index base elem -> f a) -> f ()
C.forRange_ (Contains 'SlotE hon (Win RemainingHcgWindowsLbl skolem)
-> Size (Win RemainingHcgWindowsLbl skolem) 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE hon (Win RemainingHcgWindowsLbl skolem)
remainingFullWindows) ((Index (Win RemainingHcgWindowsLbl skolem) 'SlotE -> ST s ())
 -> ST s ())
-> (Index (Win RemainingHcgWindowsLbl skolem) 'SlotE -> ST s ())
-> ST s ()
forall a b. (a -> b) -> a -> b
$ \(Contains 'SlotE hon (Win RemainingHcgWindowsLbl skolem)
-> Index (Win RemainingHcgWindowsLbl skolem) 'SlotE
-> Index hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index inner elem -> Index outer elem
C.fromWindow Contains 'SlotE hon (Win RemainingHcgWindowsLbl skolem)
remainingFullWindows -> Index hon 'SlotE
islot) -> do
        -- NB will not be truncated
        C.SomeWindow Proxy skolem
Proxy Contains 'SlotE hon (Win ScgLbl skolem)
scgSlots <- SomeWindow ScgLbl hon 'SlotE -> ST s (SomeWindow ScgLbl hon 'SlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow ScgLbl hon 'SlotE
 -> ST s (SomeWindow ScgLbl hon 'SlotE))
-> SomeWindow ScgLbl hon 'SlotE
-> ST s (SomeWindow ScgLbl hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ Size hon 'SlotE
-> Lbl ScgLbl
-> Index hon 'SlotE
-> Size hon 'SlotE
-> SomeWindow ScgLbl hon 'SlotE
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl) x.
Size outer elem
-> Lbl lbl
-> Index outer elem
-> Size x elem
-> SomeWindow lbl outer elem
C.withWindow Size hon 'SlotE
sz (forall lbl. Lbl lbl
forall {k} (lbl :: k). Lbl lbl
C.Lbl @ScgLbl) Index hon 'SlotE
islot (Var hon 'SlotE -> Size hon 'SlotE
forall {kelem} base (elem :: kelem).
Var base elem -> Size base elem
C.toSize Var hon 'SlotE
denominator)

        Var hon 'ActiveSlotE
tot <- do
            Var hon 'ActiveSlotE
tot <- STRef s (Var hon 'ActiveSlotE) -> ST s (Var hon 'ActiveSlotE)
forall s a. STRef s a -> ST s a
readSTRef STRef s (Var hon 'ActiveSlotE)
rtot
            Bool
end <- Proxy 'NotInverted
-> MVector hon 'SlotE s S -> Index hon '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 hon 'SlotE s S
mv (Contains 'SlotE hon (Win ScgLbl skolem) -> Index hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE hon (Win ScgLbl skolem)
scgSlots)
            Var hon 'ActiveSlotE -> ST s (Var hon 'ActiveSlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Var hon 'ActiveSlotE -> ST s (Var hon 'ActiveSlotE))
-> Var hon 'ActiveSlotE -> ST s (Var hon 'ActiveSlotE)
forall a b. (a -> b) -> a -> b
$ (if Bool
end then (Var hon 'ActiveSlotE
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. Num a => a -> a -> a
+Var hon 'ActiveSlotE
1) else Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. a -> a
id) (Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE)
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a b. (a -> b) -> a -> b
$ Var hon 'ActiveSlotE
tot

        let sparse :: Bool
sparse = Var hon 'ActiveSlotE
tot Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE -> Bool
forall a. Eq a => a -> a -> Bool
== Var hon 'ActiveSlotE
numerator Var hon 'ActiveSlotE
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. Num a => a -> a -> a
- Var hon 'ActiveSlotE
1   -- see LOOP INVARIANT

        Var hon 'ActiveSlotE
tot' <- if Bool -> Bool
not Bool
sparse then Var hon 'ActiveSlotE -> ST s (Var hon 'ActiveSlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Var hon 'ActiveSlotE
tot else do
            Proxy 'NotInverted
-> MVector hon 'SlotE s S -> Index hon '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 hon 'SlotE s S
mv (Contains 'SlotE hon (Win ScgLbl skolem) -> Index hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowLast Contains 'SlotE hon (Win ScgLbl skolem)
scgSlots)
            Var hon 'ActiveSlotE -> ST s (Var hon 'ActiveSlotE)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Var hon 'ActiveSlotE
numerator

        Bool
start <- Proxy 'NotInverted
-> MVector hon 'SlotE s S -> Index hon '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 hon 'SlotE s S
mv (Contains 'SlotE hon (Win ScgLbl skolem) -> Index hon 'SlotE
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Index outer elem
C.windowStart Contains 'SlotE hon (Win ScgLbl skolem)
scgSlots)
        STRef s (Var hon 'ActiveSlotE) -> Var hon 'ActiveSlotE -> ST s ()
forall s a. STRef s a -> a -> ST s ()
writeSTRef STRef s (Var hon 'ActiveSlotE)
rtot (Var hon 'ActiveSlotE -> ST s ())
-> Var hon 'ActiveSlotE -> ST s ()
forall a b. (a -> b) -> a -> b
$! (if Bool
start then Var hon 'ActiveSlotE
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. Num a => a -> a -> a
subtract Var hon 'ActiveSlotE
1 else Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a. a -> a
id) (Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE)
-> Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall a b. (a -> b) -> a -> b
$ Var hon 'ActiveSlotE
tot'

    MVector hon 'SlotE s S -> ST s (MVector hon 'SlotE s S)
forall a. a -> ST s a
forall (f :: * -> *) a. Applicative f => a -> f a
pure MVector hon 'SlotE s S
mv
  where
    UnsafeCheckedHonestRecipe {
        SomeDensityWindow 'NotInverted
chrScgDensity :: forall base hon.
CheckedHonestRecipe base hon -> SomeDensityWindow 'NotInverted
chrScgDensity :: SomeDensityWindow 'NotInverted
chrScgDensity
      ,
        chrWin :: forall base hon.
CheckedHonestRecipe base hon -> Contains 'SlotE base hon
chrWin         = Contains 'SlotE base hon
slots
      }  = CheckedHonestRecipe base hon
recipe

    sz :: Size hon 'SlotE
sz  = 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
slots :: C.Size hon SlotE   -- ie 'Len'

    wrap :: Vector hon 'SlotE S -> ChainSchema base hon
wrap Vector hon 'SlotE S
v = Contains 'SlotE base hon
-> Vector hon 'SlotE S -> ChainSchema base hon
forall base inner.
Contains 'SlotE base inner
-> Vector inner 'SlotE S -> ChainSchema base inner
ChainSchema Contains 'SlotE base hon
slots Vector hon 'SlotE S
v

-----

data ScgViolation hon =
    forall skolem.
    ScgViolation {
        -- | How many active slots 'scgvWindow' has
        ()
scgvPopCount :: !(C.Size (C.Win ScgLbl skolem) ActiveSlotE)
      ,
        -- | The ChainGrowth window that doesn't have enough active slots
        ()
scgvWindow   :: !(C.Contains SlotE hon (C.Win ScgLbl skolem))
      }

instance Eq (ScgViolation hon) where
    ScgViolation Size (Win ScgLbl skolem) 'ActiveSlotE
l1 Contains 'SlotE hon (Win ScgLbl skolem)
l2 == :: ScgViolation hon -> ScgViolation hon -> Bool
== ScgViolation Size (Win ScgLbl skolem) 'ActiveSlotE
r1 Contains 'SlotE hon (Win ScgLbl skolem)
r2 =
      Size (Win ScgLbl skolem) 'ActiveSlotE
-> Forgotten (Count () 'ActiveSlotE Total)
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Forgotten (Count () elem which)
C.forgetBase Size (Win ScgLbl skolem) 'ActiveSlotE
l1 Forgotten (Count () 'ActiveSlotE Total)
-> Forgotten (Count () 'ActiveSlotE Total) -> Bool
forall a. Eq a => a -> a -> Bool
== Size (Win ScgLbl skolem) 'ActiveSlotE
-> Forgotten (Count () 'ActiveSlotE Total)
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Forgotten (Count () elem which)
C.forgetBase Size (Win ScgLbl skolem) 'ActiveSlotE
r1
      Bool -> Bool -> Bool
&&
      Contains 'SlotE hon (Win ScgLbl skolem)
-> Forgotten (Index hon 'SlotE, Index hon 'SlotE)
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner
-> Forgotten (Index outer elem, Index outer elem)
C.forgetWindow Contains 'SlotE hon (Win ScgLbl skolem)
l2 Forgotten (Index hon 'SlotE, Index hon 'SlotE)
-> Forgotten (Index hon 'SlotE, Index hon 'SlotE) -> Bool
forall a. Eq a => a -> a -> Bool
== Contains 'SlotE hon (Win ScgLbl skolem)
-> Forgotten (Index hon 'SlotE, Index hon 'SlotE)
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner
-> Forgotten (Index outer elem, Index outer elem)
C.forgetWindow Contains 'SlotE hon (Win ScgLbl skolem)
r2

instance Show (ScgViolation hon) where
    showsPrec :: Int -> ScgViolation hon -> ShowS
showsPrec Int
p (ScgViolation Size (Win ScgLbl skolem) 'ActiveSlotE
x Contains 'SlotE hon (Win ScgLbl skolem)
y) =
        Int -> ShowBuilder (ScgViolation hon) -> ShowS
forall a.
NoFun "runShowsPrec" a (AbsError "runShowsPrec" a) =>
Int -> ShowBuilder a -> ShowS
Some.runShowsPrec Int
p
      (ShowBuilder (ScgViolation hon) -> ShowS)
-> ShowBuilder (ScgViolation hon) -> ShowS
forall a b. (a -> b) -> a -> b
$ (Size (Win ScgLbl skolem) 'ActiveSlotE
 -> Contains 'SlotE hon (Win ScgLbl skolem) -> ScgViolation hon)
-> String
-> ShowBuilder
     (Size (Win ScgLbl skolem) 'ActiveSlotE
      -> Contains 'SlotE hon (Win ScgLbl skolem) -> ScgViolation hon)
forall a. a -> String -> ShowBuilder a
Some.showCtor Size (Win ScgLbl skolem) 'ActiveSlotE
-> Contains 'SlotE hon (Win ScgLbl skolem) -> ScgViolation hon
forall hon skolem.
Size (Win ScgLbl skolem) 'ActiveSlotE
-> Contains 'SlotE hon (Win ScgLbl skolem) -> ScgViolation hon
ScgViolation String
"ScgViolation"
            ShowBuilder
  (Size (Win ScgLbl skolem) 'ActiveSlotE
   -> Contains 'SlotE hon (Win ScgLbl skolem) -> ScgViolation hon)
-> Size (Win ScgLbl skolem) 'ActiveSlotE
-> ShowBuilder
     (Contains 'SlotE hon (Win ScgLbl skolem) -> ScgViolation hon)
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` Size (Win ScgLbl skolem) 'ActiveSlotE
x
            ShowBuilder
  (Contains 'SlotE hon (Win ScgLbl skolem) -> ScgViolation hon)
-> Contains 'SlotE hon (Win ScgLbl skolem)
-> ShowBuilder (ScgViolation hon)
forall a b. Show a => ShowBuilder (a -> b) -> a -> ShowBuilder b
`Some.showArg` Contains 'SlotE hon (Win ScgLbl skolem)
y

instance Read (ScgViolation hon) where
    readPrec :: ReadPrec (ScgViolation hon)
readPrec =
        ReadBuilder (ScgViolation hon) -> ReadPrec (ScgViolation hon)
forall a.
NoFun "runReadPrec" a (AbsError "runReadPrec" a) =>
ReadBuilder a -> ReadPrec a
Some.runReadPrec
      (ReadBuilder (ScgViolation hon) -> ReadPrec (ScgViolation hon))
-> ReadBuilder (ScgViolation hon) -> ReadPrec (ScgViolation hon)
forall a b. (a -> b) -> a -> b
$ (Size (Win ScgLbl Any) 'ActiveSlotE
 -> Contains 'SlotE hon (Win ScgLbl Any) -> ScgViolation hon)
-> String
-> ReadBuilder
     (Size (Win ScgLbl Any) 'ActiveSlotE
      -> Contains 'SlotE hon (Win ScgLbl Any) -> ScgViolation hon)
forall a. a -> String -> ReadBuilder a
Some.readCtor Size (Win ScgLbl Any) 'ActiveSlotE
-> Contains 'SlotE hon (Win ScgLbl Any) -> ScgViolation hon
forall hon skolem.
Size (Win ScgLbl skolem) 'ActiveSlotE
-> Contains 'SlotE hon (Win ScgLbl skolem) -> ScgViolation hon
ScgViolation String
"ScgViolation"
            ReadBuilder
  (Size (Win ScgLbl Any) 'ActiveSlotE
   -> Contains 'SlotE hon (Win ScgLbl Any) -> ScgViolation hon)
-> ReadBuilder (Size (Win ScgLbl Any) 'ActiveSlotE)
-> ReadBuilder
     (Contains 'SlotE hon (Win ScgLbl Any) -> ScgViolation 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 (Size (Win ScgLbl Any) 'ActiveSlotE)
forall a. Read a => ReadBuilder a
Some.readArg
            ReadBuilder
  (Contains 'SlotE hon (Win ScgLbl Any) -> ScgViolation hon)
-> ReadBuilder (Contains 'SlotE hon (Win ScgLbl Any))
-> ReadBuilder (ScgViolation 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 (Contains 'SlotE hon (Win ScgLbl Any))
forall a. Read a => ReadBuilder a
Some.readArg

data HonestChainViolation hon =
    -- | The schema does not contain a positive number of active slots
    BadCount
  |
    -- | The schema has some window of 'Scg' slots that contains less than
    -- 'Kcp+1' active slots, even despite optimistically assuming that all slots
    -- beyond 'Len' are active
    BadScgWindow !(ScgViolation hon)
  |
    -- | The schema does not span exactly 'Len' slots
    BadLength !(C.Size hon SlotE)
  deriving (HonestChainViolation hon -> HonestChainViolation hon -> Bool
(HonestChainViolation hon -> HonestChainViolation hon -> Bool)
-> (HonestChainViolation hon -> HonestChainViolation hon -> Bool)
-> Eq (HonestChainViolation hon)
forall hon.
HonestChainViolation hon -> HonestChainViolation hon -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall hon.
HonestChainViolation hon -> HonestChainViolation hon -> Bool
== :: HonestChainViolation hon -> HonestChainViolation hon -> Bool
$c/= :: forall hon.
HonestChainViolation hon -> HonestChainViolation hon -> Bool
/= :: HonestChainViolation hon -> HonestChainViolation hon -> Bool
Eq, ReadPrec [HonestChainViolation hon]
ReadPrec (HonestChainViolation hon)
Int -> ReadS (HonestChainViolation hon)
ReadS [HonestChainViolation hon]
(Int -> ReadS (HonestChainViolation hon))
-> ReadS [HonestChainViolation hon]
-> ReadPrec (HonestChainViolation hon)
-> ReadPrec [HonestChainViolation hon]
-> Read (HonestChainViolation hon)
forall hon. ReadPrec [HonestChainViolation hon]
forall hon. ReadPrec (HonestChainViolation hon)
forall hon. Int -> ReadS (HonestChainViolation hon)
forall hon. ReadS [HonestChainViolation hon]
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: forall hon. Int -> ReadS (HonestChainViolation hon)
readsPrec :: Int -> ReadS (HonestChainViolation hon)
$creadList :: forall hon. ReadS [HonestChainViolation hon]
readList :: ReadS [HonestChainViolation hon]
$creadPrec :: forall hon. ReadPrec (HonestChainViolation hon)
readPrec :: ReadPrec (HonestChainViolation hon)
$creadListPrec :: forall hon. ReadPrec [HonestChainViolation hon]
readListPrec :: ReadPrec [HonestChainViolation hon]
Read, Int -> HonestChainViolation hon -> ShowS
[HonestChainViolation hon] -> ShowS
HonestChainViolation hon -> String
(Int -> HonestChainViolation hon -> ShowS)
-> (HonestChainViolation hon -> String)
-> ([HonestChainViolation hon] -> ShowS)
-> Show (HonestChainViolation hon)
forall hon. Int -> HonestChainViolation hon -> ShowS
forall hon. [HonestChainViolation hon] -> ShowS
forall hon. HonestChainViolation hon -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall hon. Int -> HonestChainViolation hon -> ShowS
showsPrec :: Int -> HonestChainViolation hon -> ShowS
$cshow :: forall hon. HonestChainViolation hon -> String
show :: HonestChainViolation hon -> String
$cshowList :: forall hon. [HonestChainViolation hon] -> ShowS
showList :: [HonestChainViolation hon] -> ShowS
Show)

-- | A stability window
data ScgLbl

-- | Check the Extended Praos Chain Growth assumption
--
-- Definition of /window/ and /anchored window/. A window is a contiguous
-- sequence of slots. A window anchored at a block starts with the slot
-- immediately after that block.
--
-- Definition of /Extended Praos Chain Growth Assumption/. We assume the honest chain
-- contains at least @k+1@ blocks in every window that contains @s@ slots.
--
-- Definition of /Stability Window/. The @s@ parameter from the Praos Chain
-- Growth property. (At the time of writing, this is @2k@ during Byron and
-- @3k/f@ after Byron on Cardano @mainnet@.)
checkHonestChain ::
  forall base hon.
     HonestRecipe
  -> ChainSchema base hon
  -> Exn.Except (HonestChainViolation hon) ()
checkHonestChain :: forall base hon.
HonestRecipe
-> ChainSchema base hon -> Except (HonestChainViolation hon) ()
checkHonestChain HonestRecipe
recipe ChainSchema base hon
sched = do
    Bool
-> Except (HonestChainViolation hon) ()
-> Except (HonestChainViolation hon) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Count hon 'SlotE Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Count hon 'SlotE Total
sz Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
l) (Except (HonestChainViolation hon) ()
 -> Except (HonestChainViolation hon) ())
-> Except (HonestChainViolation hon) ()
-> Except (HonestChainViolation hon) ()
forall a b. (a -> b) -> a -> b
$ HonestChainViolation hon -> Except (HonestChainViolation hon) ()
forall a.
HonestChainViolation hon
-> ExceptT (HonestChainViolation hon) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError (HonestChainViolation hon -> Except (HonestChainViolation hon) ())
-> HonestChainViolation hon -> Except (HonestChainViolation hon) ()
forall a b. (a -> b) -> a -> b
$ Count hon 'SlotE Total -> HonestChainViolation hon
forall hon. Size hon 'SlotE -> HonestChainViolation hon
BadLength Count hon 'SlotE Total
sz

    do  let pc :: Size hon 'ActiveSlotE
pc = ChainSchema base hon -> Size hon 'ActiveSlotE
forall base inner.
ChainSchema base inner -> Size inner 'ActiveSlotE
countChainSchema ChainSchema base hon
sched
        Bool
-> Except (HonestChainViolation hon) ()
-> Except (HonestChainViolation hon) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Size hon 'ActiveSlotE -> Var hon 'ActiveSlotE
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Var base elem
C.toVar Size hon 'ActiveSlotE
pc Var hon 'ActiveSlotE -> Var hon 'ActiveSlotE -> Bool
forall a. Ord a => a -> a -> Bool
<= Var hon 'ActiveSlotE
0) (Except (HonestChainViolation hon) ()
 -> Except (HonestChainViolation hon) ())
-> Except (HonestChainViolation hon) ()
-> Except (HonestChainViolation hon) ()
forall a b. (a -> b) -> a -> b
$ HonestChainViolation hon -> Except (HonestChainViolation hon) ()
forall a.
HonestChainViolation hon
-> ExceptT (HonestChainViolation hon) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError HonestChainViolation hon
forall hon. HonestChainViolation hon
BadCount

    -- every slot is the first slot of a unique stability window
    Count hon 'SlotE Total
-> (Index hon 'SlotE -> Except (HonestChainViolation hon) ())
-> Except (HonestChainViolation hon) ()
forall {kelem} (f :: * -> *) base (elem :: kelem) a.
Applicative f =>
Size base elem -> (Index base elem -> f a) -> f ()
C.forRange_ Count hon 'SlotE Total
sz ((Index hon 'SlotE -> Except (HonestChainViolation hon) ())
 -> Except (HonestChainViolation hon) ())
-> (Index hon 'SlotE -> Except (HonestChainViolation hon) ())
-> Except (HonestChainViolation hon) ()
forall a b. (a -> b) -> a -> b
$ \Index hon 'SlotE
i -> do
        -- note that withWindow truncates if the requested slots reach past 'Len'
        C.SomeWindow Proxy skolem
Proxy Contains 'SlotE hon (Win ScgLbl skolem)
scg <- SomeWindow ScgLbl hon 'SlotE
-> ExceptT
     (HonestChainViolation hon) Identity (SomeWindow ScgLbl hon 'SlotE)
forall a. a -> ExceptT (HonestChainViolation hon) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (SomeWindow ScgLbl hon 'SlotE
 -> ExceptT
      (HonestChainViolation hon) Identity (SomeWindow ScgLbl hon 'SlotE))
-> SomeWindow ScgLbl hon 'SlotE
-> ExceptT
     (HonestChainViolation hon) Identity (SomeWindow ScgLbl hon 'SlotE)
forall a b. (a -> b) -> a -> b
$ Count hon 'SlotE Total
-> Lbl ScgLbl
-> Index hon 'SlotE
-> Size Any 'SlotE
-> SomeWindow ScgLbl hon 'SlotE
forall {kelem} {klbl} outer (elem :: kelem) (lbl :: klbl) x.
Size outer elem
-> Lbl lbl
-> Index outer elem
-> Size x elem
-> SomeWindow lbl outer elem
C.withWindow Count hon 'SlotE Total
sz (forall lbl. Lbl lbl
forall {k} (lbl :: k). Lbl lbl
C.Lbl @ScgLbl) Index hon 'SlotE
i (Int -> Size Any 'SlotE
forall kelem kwhich base (elem :: kelem) (which :: kwhich).
Int -> Count base elem which
C.Count Int
s)

        let pc :: Size (Win ScgLbl skolem) (PreImage 'NotInverted 'ActiveSlotE)
pc = Proxy 'NotInverted
-> Vector (Win ScgLbl skolem) 'SlotE S
-> Size (Win ScgLbl 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 ScgLbl skolem)
-> Vector hon 'SlotE S -> Vector (Win ScgLbl 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 ScgLbl skolem)
scg Vector hon 'SlotE S
v)

        -- generously assume that the slots of this stability window that extend past 'Len' are active
        let benefitOfTheDoubt :: Int
benefitOfTheDoubt = Int
s Int -> Int -> Int
forall a. Num a => a -> a -> a
- Count (Win ScgLbl skolem) 'SlotE Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount (Contains 'SlotE hon (Win ScgLbl skolem)
-> Count (Win ScgLbl skolem) 'SlotE Total
forall {kelem} (elem :: kelem) outer inner.
Contains elem outer inner -> Size inner elem
C.windowSize Contains 'SlotE hon (Win ScgLbl skolem)
scg)

        -- check the density in the stability window
        Bool
-> Except (HonestChainViolation hon) ()
-> Except (HonestChainViolation hon) ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Count (Win ScgLbl skolem) 'ActiveSlotE Total -> Int
forall {kelem} {kwhich} base (elem :: kelem) (which :: kwhich).
Count base elem which -> Int
C.getCount Count (Win ScgLbl skolem) 'ActiveSlotE Total
pc Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
benefitOfTheDoubt Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Except (HonestChainViolation hon) ()
 -> Except (HonestChainViolation hon) ())
-> Except (HonestChainViolation hon) ()
-> Except (HonestChainViolation hon) ()
forall a b. (a -> b) -> a -> b
$ do
            HonestChainViolation hon -> Except (HonestChainViolation hon) ()
forall a.
HonestChainViolation hon
-> ExceptT (HonestChainViolation hon) Identity a
forall e (m :: * -> *) a. MonadError e m => e -> m a
Exn.throwError (HonestChainViolation hon -> Except (HonestChainViolation hon) ())
-> HonestChainViolation hon -> Except (HonestChainViolation hon) ()
forall a b. (a -> b) -> a -> b
$ ScgViolation hon -> HonestChainViolation hon
forall hon. ScgViolation hon -> HonestChainViolation hon
BadScgWindow (ScgViolation hon -> HonestChainViolation hon)
-> ScgViolation hon -> HonestChainViolation hon
forall a b. (a -> b) -> a -> b
$ ScgViolation {
                scgvPopCount :: Count (Win ScgLbl skolem) 'ActiveSlotE Total
scgvPopCount = Count (Win ScgLbl skolem) 'ActiveSlotE Total
pc
              ,
                scgvWindow :: Contains 'SlotE hon (Win ScgLbl skolem)
scgvWindow   = Contains 'SlotE hon (Win ScgLbl skolem)
scg
              }

  where
    HonestRecipe (Kcp Int
k) (Scg Int
s) (Delta Int
_d) (Len Int
l) = HonestRecipe
recipe

    ChainSchema Contains 'SlotE base hon
hon Vector hon 'SlotE S
v = ChainSchema base hon
sched

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