{-# LANGUAGE PatternSynonyms #-}

module Test.Ouroboros.Consensus.ChainGenerator.Params (
    Asc (Asc, UnsafeAsc)
  , Delta (Delta)
  , Kcp (Kcp)
  , Len (Len)
  , Scg (Scg)
  , ascFromBits
  , ascFromDouble
  , ascVal
  , genAsc
  , genKSD
  ) where

import qualified Data.Bits as B
import           Data.Word (Word8)
import qualified Test.QuickCheck as QC
import           Test.QuickCheck.Extras (sized1)

-----

-- | The Δ parameter of the Praos theorems and so also of the Praos Race
-- Assumption
--
-- ASSUMPTION: If an honest block @b@ is minted at the start of slot @x@, then
-- every (healthy) honest node will have selected a chain no worse than @b@ by
-- the onset of slot @x + Δ + 1@.
--
-- NOTE: If @Δ=0@, then the best block minted in each slot is selected by every
-- (healthy) honest node before the onset of the next slot.
--
-- NOTE: If the honest block @k+1@ after its intersection with an alternative
-- chain was minted in slot @x@, then the alternative block @k+1@ after the
-- intersection can be minted no sooner than slot @x + Δ + 1@. Thus @x + Δ@ is
-- the youngest slot in the Praos Race Window.
newtype Delta = Delta Int
  deriving (Delta -> Delta -> Bool
(Delta -> Delta -> Bool) -> (Delta -> Delta -> Bool) -> Eq Delta
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Delta -> Delta -> Bool
== :: Delta -> Delta -> Bool
$c/= :: Delta -> Delta -> Bool
/= :: Delta -> Delta -> Bool
Eq, Eq Delta
Eq Delta =>
(Delta -> Delta -> Ordering)
-> (Delta -> Delta -> Bool)
-> (Delta -> Delta -> Bool)
-> (Delta -> Delta -> Bool)
-> (Delta -> Delta -> Bool)
-> (Delta -> Delta -> Delta)
-> (Delta -> Delta -> Delta)
-> Ord Delta
Delta -> Delta -> Bool
Delta -> Delta -> Ordering
Delta -> Delta -> Delta
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Delta -> Delta -> Ordering
compare :: Delta -> Delta -> Ordering
$c< :: Delta -> Delta -> Bool
< :: Delta -> Delta -> Bool
$c<= :: Delta -> Delta -> Bool
<= :: Delta -> Delta -> Bool
$c> :: Delta -> Delta -> Bool
> :: Delta -> Delta -> Bool
$c>= :: Delta -> Delta -> Bool
>= :: Delta -> Delta -> Bool
$cmax :: Delta -> Delta -> Delta
max :: Delta -> Delta -> Delta
$cmin :: Delta -> Delta -> Delta
min :: Delta -> Delta -> Delta
Ord, Int -> Delta -> ShowS
[Delta] -> ShowS
Delta -> String
(Int -> Delta -> ShowS)
-> (Delta -> String) -> ([Delta] -> ShowS) -> Show Delta
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Delta -> ShowS
showsPrec :: Int -> Delta -> ShowS
$cshow :: Delta -> String
show :: Delta -> String
$cshowList :: [Delta] -> ShowS
showList :: [Delta] -> ShowS
Show, ReadPrec [Delta]
ReadPrec Delta
Int -> ReadS Delta
ReadS [Delta]
(Int -> ReadS Delta)
-> ReadS [Delta]
-> ReadPrec Delta
-> ReadPrec [Delta]
-> Read Delta
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Delta
readsPrec :: Int -> ReadS Delta
$creadList :: ReadS [Delta]
readList :: ReadS [Delta]
$creadPrec :: ReadPrec Delta
readPrec :: ReadPrec Delta
$creadListPrec :: ReadPrec [Delta]
readListPrec :: ReadPrec [Delta]
Read)

-- | The maximum length of any leader schedule
--
-- This can be interpreted as the /end of time/, the final moment simulated
-- during a test.
newtype Len = Len Int
  deriving (Len -> Len -> Bool
(Len -> Len -> Bool) -> (Len -> Len -> Bool) -> Eq Len
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Len -> Len -> Bool
== :: Len -> Len -> Bool
$c/= :: Len -> Len -> Bool
/= :: Len -> Len -> Bool
Eq, Eq Len
Eq Len =>
(Len -> Len -> Ordering)
-> (Len -> Len -> Bool)
-> (Len -> Len -> Bool)
-> (Len -> Len -> Bool)
-> (Len -> Len -> Bool)
-> (Len -> Len -> Len)
-> (Len -> Len -> Len)
-> Ord Len
Len -> Len -> Bool
Len -> Len -> Ordering
Len -> Len -> Len
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Len -> Len -> Ordering
compare :: Len -> Len -> Ordering
$c< :: Len -> Len -> Bool
< :: Len -> Len -> Bool
$c<= :: Len -> Len -> Bool
<= :: Len -> Len -> Bool
$c> :: Len -> Len -> Bool
> :: Len -> Len -> Bool
$c>= :: Len -> Len -> Bool
>= :: Len -> Len -> Bool
$cmax :: Len -> Len -> Len
max :: Len -> Len -> Len
$cmin :: Len -> Len -> Len
min :: Len -> Len -> Len
Ord, Int -> Len -> ShowS
[Len] -> ShowS
Len -> String
(Int -> Len -> ShowS)
-> (Len -> String) -> ([Len] -> ShowS) -> Show Len
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Len -> ShowS
showsPrec :: Int -> Len -> ShowS
$cshow :: Len -> String
show :: Len -> String
$cshowList :: [Len] -> ShowS
showList :: [Len] -> ShowS
Show, ReadPrec [Len]
ReadPrec Len
Int -> ReadS Len
ReadS [Len]
(Int -> ReadS Len)
-> ReadS [Len] -> ReadPrec Len -> ReadPrec [Len] -> Read Len
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Len
readsPrec :: Int -> ReadS Len
$creadList :: ReadS [Len]
readList :: ReadS [Len]
$creadPrec :: ReadPrec Len
readPrec :: ReadPrec Len
$creadListPrec :: ReadPrec [Len]
readListPrec :: ReadPrec [Len]
Read)

-- | The @k@ parameter of the Praos Common Prefix property
--
-- Also known as the 'Ouroboros.Consensus.Config.SecurityParam.SecurityParam'.
newtype Kcp = Kcp Int
  deriving (Kcp -> Kcp -> Bool
(Kcp -> Kcp -> Bool) -> (Kcp -> Kcp -> Bool) -> Eq Kcp
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Kcp -> Kcp -> Bool
== :: Kcp -> Kcp -> Bool
$c/= :: Kcp -> Kcp -> Bool
/= :: Kcp -> Kcp -> Bool
Eq, Eq Kcp
Eq Kcp =>
(Kcp -> Kcp -> Ordering)
-> (Kcp -> Kcp -> Bool)
-> (Kcp -> Kcp -> Bool)
-> (Kcp -> Kcp -> Bool)
-> (Kcp -> Kcp -> Bool)
-> (Kcp -> Kcp -> Kcp)
-> (Kcp -> Kcp -> Kcp)
-> Ord Kcp
Kcp -> Kcp -> Bool
Kcp -> Kcp -> Ordering
Kcp -> Kcp -> Kcp
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Kcp -> Kcp -> Ordering
compare :: Kcp -> Kcp -> Ordering
$c< :: Kcp -> Kcp -> Bool
< :: Kcp -> Kcp -> Bool
$c<= :: Kcp -> Kcp -> Bool
<= :: Kcp -> Kcp -> Bool
$c> :: Kcp -> Kcp -> Bool
> :: Kcp -> Kcp -> Bool
$c>= :: Kcp -> Kcp -> Bool
>= :: Kcp -> Kcp -> Bool
$cmax :: Kcp -> Kcp -> Kcp
max :: Kcp -> Kcp -> Kcp
$cmin :: Kcp -> Kcp -> Kcp
min :: Kcp -> Kcp -> Kcp
Ord, Int -> Kcp -> ShowS
[Kcp] -> ShowS
Kcp -> String
(Int -> Kcp -> ShowS)
-> (Kcp -> String) -> ([Kcp] -> ShowS) -> Show Kcp
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Kcp -> ShowS
showsPrec :: Int -> Kcp -> ShowS
$cshow :: Kcp -> String
show :: Kcp -> String
$cshowList :: [Kcp] -> ShowS
showList :: [Kcp] -> ShowS
Show, ReadPrec [Kcp]
ReadPrec Kcp
Int -> ReadS Kcp
ReadS [Kcp]
(Int -> ReadS Kcp)
-> ReadS [Kcp] -> ReadPrec Kcp -> ReadPrec [Kcp] -> Read Kcp
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Kcp
readsPrec :: Int -> ReadS Kcp
$creadList :: ReadS [Kcp]
readList :: ReadS [Kcp]
$creadPrec :: ReadPrec Kcp
readPrec :: ReadPrec Kcp
$creadListPrec :: ReadPrec [Kcp]
readListPrec :: ReadPrec [Kcp]
Read)

-- | The @s@ parameter of the Praos Chain Growth property
--
-- Also known as the width of the /stability window/. In particular, we assume
-- that an adversarial stake holder cannot drastically increase their rate of
-- election until at least @s@ many slots after the first block on an
-- adversarial chain.
--
-- In other words: we're assuming that any serious attempt to corrupt the leader
-- schedule would be isolated to a private adversarial chain.
newtype Scg = Scg Int
  deriving (Scg -> Scg -> Bool
(Scg -> Scg -> Bool) -> (Scg -> Scg -> Bool) -> Eq Scg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Scg -> Scg -> Bool
== :: Scg -> Scg -> Bool
$c/= :: Scg -> Scg -> Bool
/= :: Scg -> Scg -> Bool
Eq, Eq Scg
Eq Scg =>
(Scg -> Scg -> Ordering)
-> (Scg -> Scg -> Bool)
-> (Scg -> Scg -> Bool)
-> (Scg -> Scg -> Bool)
-> (Scg -> Scg -> Bool)
-> (Scg -> Scg -> Scg)
-> (Scg -> Scg -> Scg)
-> Ord Scg
Scg -> Scg -> Bool
Scg -> Scg -> Ordering
Scg -> Scg -> Scg
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Scg -> Scg -> Ordering
compare :: Scg -> Scg -> Ordering
$c< :: Scg -> Scg -> Bool
< :: Scg -> Scg -> Bool
$c<= :: Scg -> Scg -> Bool
<= :: Scg -> Scg -> Bool
$c> :: Scg -> Scg -> Bool
> :: Scg -> Scg -> Bool
$c>= :: Scg -> Scg -> Bool
>= :: Scg -> Scg -> Bool
$cmax :: Scg -> Scg -> Scg
max :: Scg -> Scg -> Scg
$cmin :: Scg -> Scg -> Scg
min :: Scg -> Scg -> Scg
Ord, Int -> Scg -> ShowS
[Scg] -> ShowS
Scg -> String
(Int -> Scg -> ShowS)
-> (Scg -> String) -> ([Scg] -> ShowS) -> Show Scg
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Scg -> ShowS
showsPrec :: Int -> Scg -> ShowS
$cshow :: Scg -> String
show :: Scg -> String
$cshowList :: [Scg] -> ShowS
showList :: [Scg] -> ShowS
Show, ReadPrec [Scg]
ReadPrec Scg
Int -> ReadS Scg
ReadS [Scg]
(Int -> ReadS Scg)
-> ReadS [Scg] -> ReadPrec Scg -> ReadPrec [Scg] -> Read Scg
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Scg
readsPrec :: Int -> ReadS Scg
$creadList :: ReadS [Scg]
readList :: ReadS [Scg]
$creadPrec :: ReadPrec Scg
readPrec :: ReadPrec Scg
$creadListPrec :: ReadPrec [Scg]
readListPrec :: ReadPrec [Scg]
Read)

-----

-- | The /active slot coefficient/
--
-- INVARIANT: 0 < x < 1
--
-- It's as precise as 'Double', which likely suffices for all of our needs.
newtype Asc = UnsafeAsc Double
  deriving (Asc -> Asc -> Bool
(Asc -> Asc -> Bool) -> (Asc -> Asc -> Bool) -> Eq Asc
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Asc -> Asc -> Bool
== :: Asc -> Asc -> Bool
$c/= :: Asc -> Asc -> Bool
/= :: Asc -> Asc -> Bool
Eq, ReadPrec [Asc]
ReadPrec Asc
Int -> ReadS Asc
ReadS [Asc]
(Int -> ReadS Asc)
-> ReadS [Asc] -> ReadPrec Asc -> ReadPrec [Asc] -> Read Asc
forall a.
(Int -> ReadS a)
-> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
$creadsPrec :: Int -> ReadS Asc
readsPrec :: Int -> ReadS Asc
$creadList :: ReadS [Asc]
readList :: ReadS [Asc]
$creadPrec :: ReadPrec Asc
readPrec :: ReadPrec Asc
$creadListPrec :: ReadPrec [Asc]
readListPrec :: ReadPrec [Asc]
Read, Int -> Asc -> ShowS
[Asc] -> ShowS
Asc -> String
(Int -> Asc -> ShowS)
-> (Asc -> String) -> ([Asc] -> ShowS) -> Show Asc
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Asc -> ShowS
showsPrec :: Int -> Asc -> ShowS
$cshow :: Asc -> String
show :: Asc -> String
$cshowList :: [Asc] -> ShowS
showList :: [Asc] -> ShowS
Show)

pattern Asc :: Double -> Asc
pattern $mAsc :: forall {r}. Asc -> (Double -> r) -> ((# #) -> r) -> r
Asc d <- UnsafeAsc d

{-# COMPLETE Asc #-}

ascFromDouble :: Double -> Asc
ascFromDouble :: Double -> Asc
ascFromDouble Double
d
  | Double
d Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
0    = String -> Asc
forall a. HasCallStack => String -> a
error String
"Asc must be > 0"
  | Double
1 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
d    = String -> Asc
forall a. HasCallStack => String -> a
error String
"Asc must be < 1"
  | Bool
otherwise = Double -> Asc
UnsafeAsc Double
d

-- | PRECONDITION: the bits aren't all the same
--
-- The 'Asc' that equals the fraction @w \/ 2^widthW@.
ascFromBits :: (Enum w, B.FiniteBits w) => w -> Asc
ascFromBits :: forall w. (Enum w, FiniteBits w) => w -> Asc
ascFromBits w
w = Double -> Asc
ascFromDouble (Double -> Asc) -> Double -> Asc
forall a b. (a -> b) -> a -> b
$ Int -> Double
forall a. Enum a => Int -> a
toEnum (w -> Int
forall a. Enum a => a -> Int
fromEnum w
w) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ (Double
2 Double -> Int -> Double
forall a b. (Num a, Integral b) => a -> b -> a
^ w -> Int
forall b. FiniteBits b => b -> Int
B.finiteBitSize w
w)

-- | Interpret 'Asc' as a 'Double'
ascVal :: Asc -> Double
ascVal :: Asc -> Double
ascVal (Asc Double
x) = Double
x

genAsc :: QC.Gen Asc
genAsc :: Gen Asc
genAsc = Word8 -> Asc
forall w. (Enum w, FiniteBits w) => w -> Asc
ascFromBits (Word8 -> Asc) -> Gen Word8 -> Gen Asc
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Word8, Word8) -> Gen Word8
forall a. Random a => (a, a) -> Gen a
QC.choose (Word8
1 :: Word8, Word8
forall a. Bounded a => a
maxBound Word8 -> Word8 -> Word8
forall a. Num a => a -> a -> a
- Word8
1)

genKSD :: QC.Gen (Kcp, Scg, Delta)
genKSD :: Gen (Kcp, Scg, Delta)
genKSD = (Int -> Gen (Kcp, Scg, Delta)) -> Gen (Kcp, Scg, Delta)
forall a. (Int -> Gen a) -> Gen a
sized1 ((Int -> Gen (Kcp, Scg, Delta)) -> Gen (Kcp, Scg, Delta))
-> (Int -> Gen (Kcp, Scg, Delta)) -> Gen (Kcp, Scg, Delta)
forall a b. (a -> b) -> a -> b
$ \Int
sz -> do
    -- k > 0 so we can ensure an alternative schema loses the density comparison
    -- without having to deactivate the first active slot
    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
sz)
    Int
s <- (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
2 Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
sz)   -- ensures @(k+1) / s <= 1@
    Int
d <- (Int, Int) -> Gen Int
forall a. Random a => (a, a) -> Gen a
QC.choose (Int
0, Int -> Int -> Int
forall a. Ord a => a -> a -> a
max Int
0 (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Int
forall a. Ord a => a -> a -> a
min (Int -> Int -> Int
forall a. Integral a => a -> a -> a
div Int
sz Int
4) (Int
sInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1)) -- ensures @d < s@
    (Kcp, Scg, Delta) -> Gen (Kcp, Scg, Delta)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Kcp
Kcp Int
k, Int -> Scg
Scg Int
s, Int -> Delta
Delta Int
d)