{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TupleSections #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}

module Test.Byron.Spec.Ledger.Update.Properties (
  upiregTracesAreClassified,
  upiregRelevantTracesAreCovered,
  onlyValidSignalsAreGenerated,
  ublockTraceLengthsAreClassified,
  ublockOnlyValidSignalsAreGenerated,
  ublockRelevantTracesAreCovered,
  ublockSampleTraceMetrics,
) where

import Byron.Spec.Ledger.Core (
  BlockCount (BlockCount),
  Slot (Slot),
  SlotCount (SlotCount),
  dom,
  unBlockCount,
 )
import qualified Byron.Spec.Ledger.Core as Core
import Byron.Spec.Ledger.GlobalParams (slotsPerEpoch)
import Byron.Spec.Ledger.Update (
  PParams,
  ProtVer,
  UPIEND,
  UPIEnv,
  UPIREG,
  UPIState,
  UPIVOTES,
  UProp,
  Vote,
  emptyUPIState,
  protocolParameters,
 )
import qualified Byron.Spec.Ledger.Update as Update
import Control.State.Transition (
  Embed,
  Environment,
  IRC (IRC),
  PredicateFailure,
  STS (..),
  Signal,
  State,
  TRC (TRC),
  initialRules,
  judgmentContext,
  trans,
  transitionRules,
  wrapFailed,
  (?!),
 )
import qualified Data.Bimap as Bimap
import Data.Data (Data)
import Data.Foldable (fold, traverse_)
import Data.Function ((&))
import Data.List.Unique (count)
import Data.Maybe (catMaybes, isNothing)
import qualified Data.Set as Set
import Data.Word (Word64)
import GHC.Stack (HasCallStack)
import Hedgehog (Property, cover, forAll, property, withTests)
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Numeric.Natural (Natural)
import Test.Control.State.Transition.Generator (
  HasTrace,
  envGen,
  randomTraceOfSize,
  ratio,
  sigGen,
  trace,
  traceLengthsAreClassified,
  traceOfLength,
 )
import qualified Test.Control.State.Transition.Generator as Transition.Generator
import Test.Control.State.Transition.Trace (
  Trace,
  TraceOrder (OldestFirst),
  traceLength,
  traceSignals,
  traceStates,
  _traceEnv,
  _traceInitState,
 )

upiregTracesAreClassified :: Property
upiregTracesAreClassified :: Property
upiregTracesAreClassified =
  TestLimit -> Property -> Property
withTests TestLimit
100 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ forall s.
(HasTrace s, Show (Environment s), Show (State s),
 Show (Signal s)) =>
BaseEnv s -> Word64 -> Word64 -> Property
traceLengthsAreClassified @UPIREG () Word64
100 Word64
10

upiregRelevantTracesAreCovered :: Property
upiregRelevantTracesAreCovered :: Property
upiregRelevantTracesAreCovered = TestLimit -> Property -> Property
withTests TestLimit
300 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
  HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    sample <- Gen (Trace UPIREG) -> PropertyT IO (Trace UPIREG)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @UPIREG () Word64
200)

    cover
      40
      "at least 30% of the update proposals increase the major version"
      (0.25 <= ratio increaseMajor sample)

    cover
      40
      "at least 30% of the update proposals increase the minor version"
      (0.25 <= ratio increaseMinor sample)

    cover
      30
      "at least 10% of the update proposals do not change the protocol version"
      (0.10 <= ratio dontChangeProtocolVersion sample)

    -- We have a roughly fair distribution of issuers.
    --
    -- Here we simply compute how many update proposals a given issuer should
    -- have made if everybody made the same number of proposals, and check that
    -- each issuer didn't produce less than a certain percentage of that. So for
    -- instance, if we have 4 genesis keys and a trace length of 100, then in an
    -- completely fair distribution of issuers we would expect to have 25 update
    -- proposals per-genesis key. So in this test we would check that in 50% of
    -- the generated traces, the deviation from the fair distribution (25 update
    -- proposals per-key) is no greater than half its expected value (25 * 0.5 =
    -- 12.5).
    cover
      50
      "the distribution of the proposal issuers is roughly fair"
      ( safeMaximum (issuersDeviationsWrtUniformDistribution sample)
          <= expectedNumberOfUpdateProposalsPerKey sample * 0.5
      )

    --------------------------------------------------------------------------------
    -- Maximum block-size checks
    --------------------------------------------------------------------------------
    -- NOTE: since we want to generate valid signals, we cannot decrease the block
    -- size in most of the cases.
    cover
      20
      "at least 5% of the update proposals decrease the maximum block-size"
      (0.05 <= ratio (wrtCurrentProtocolParameters Update._maxBkSz Decreases) sample)

    cover
      50
      "at least 30% of the update proposals increase the maximum block-size"
      (0.3 <= ratio (wrtCurrentProtocolParameters Update._maxBkSz Increases) sample)

    cover
      30
      "at least 10% of the update proposals do not change the maximum block-size"
      (0.1 <= ratio (wrtCurrentProtocolParameters Update._maxBkSz RemainsTheSame) sample)

    --------------------------------------------------------------------------------
    -- Maximum header-size checks
    --------------------------------------------------------------------------------
    cover
      20
      "at least 5% of the update proposals decrease the maximum header-size"
      (0.05 <= ratio (wrtCurrentProtocolParameters Update._maxHdrSz Decreases) sample)

    cover
      50
      "at least 30% of the update proposals increase the maximum header-size"
      (0.3 <= ratio (wrtCurrentProtocolParameters Update._maxHdrSz Increases) sample)

    cover
      50
      "at least 10% of the update proposals do not change the maximum header-size"
      (0.1 <= ratio (wrtCurrentProtocolParameters Update._maxHdrSz RemainsTheSame) sample)

    --------------------------------------------------------------------------------
    -- Maximum transaction-size checks
    --------------------------------------------------------------------------------
    cover
      20
      "at least 5% of the update proposals decrease the maximum transaction-size"
      (0.05 <= ratio (wrtCurrentProtocolParameters Update._maxTxSz Decreases) sample)

    cover
      50
      "at least 30% of the update proposals increase the maximum transaction-size"
      (0.3 <= ratio (wrtCurrentProtocolParameters Update._maxTxSz Increases) sample)

    cover
      40
      "at least 10% of the update proposals do not change the maximum transaction-size"
      (0.1 <= ratio (wrtCurrentProtocolParameters Update._maxTxSz RemainsTheSame) sample)

    --------------------------------------------------------------------------------
    -- Maximum proposal-size checks
    --------------------------------------------------------------------------------
    cover
      20
      "at least 30% of the update proposals decrease the maximum proposal-size"
      (0.05 <= ratio (wrtCurrentProtocolParameters Update._maxPropSz Decreases) sample)

    cover
      50
      "at least 30% of the update proposals increase the maximum proposal-size"
      (0.3 <= ratio (wrtCurrentProtocolParameters Update._maxPropSz Increases) sample)

    cover
      50
      "at least 10% of the update proposals do not change the maximum proposal-size"
      (0.1 <= ratio (wrtCurrentProtocolParameters Update._maxPropSz RemainsTheSame) sample)
  where
    -- NOTE: after empirically determining the checks above are sensible, we can
    -- add more coverage tests for the other protocol parameters.

    increaseMajor :: Trace UPIREG -> Int
    increaseMajor :: Trace UPIREG -> Int
increaseMajor Trace UPIREG
traceSample =
      Trace UPIREG -> [ProtVer]
protocolVersions Trace UPIREG
traceSample
        [ProtVer] -> ([ProtVer] -> [Natural]) -> [Natural]
forall a b. a -> (a -> b) -> b
& (ProtVer -> Natural) -> [ProtVer] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProtVer -> Natural
Update._pvMaj
        [Natural] -> ([Natural] -> [Natural]) -> [Natural]
forall a b. a -> (a -> b) -> b
& (Natural -> Bool) -> [Natural] -> [Natural]
forall a. (a -> Bool) -> [a] -> [a]
filter (Trace UPIREG -> Natural
currPvMaj Trace UPIREG
traceSample Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<)
        [Natural] -> ([Natural] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [Natural] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length

    protocolVersions :: Trace UPIREG -> [Update.ProtVer]
    protocolVersions :: Trace UPIREG -> [ProtVer]
protocolVersions Trace UPIREG
tr =
      (UProp -> ProtVer) -> [UProp] -> [ProtVer]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UProp -> ProtVer
Update._upPV (TraceOrder -> Trace UPIREG -> [Signal UPIREG]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UPIREG
tr)

    -- We can take the current protocol version from the initial state of
    -- UPIREG, since this transition does not change the protocol version.
    currPvMaj :: Trace UPIREG -> Natural
    currPvMaj :: Trace UPIREG -> Natural
currPvMaj = ProtVer -> Natural
Update._pvMaj (ProtVer -> Natural)
-> (Trace UPIREG -> ProtVer) -> Trace UPIREG -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UPIState -> ProtVer
Update.protocolVersion (UPIState -> ProtVer)
-> (Trace UPIREG -> UPIState) -> Trace UPIREG -> ProtVer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace UPIREG -> UPIState
Trace UPIREG -> State UPIREG
forall s. Trace s -> State s
_traceInitState

    currentProtocolVersion :: Trace UPIREG -> Update.ProtVer
    currentProtocolVersion :: Trace UPIREG -> ProtVer
currentProtocolVersion = UPIState -> ProtVer
Update.protocolVersion (UPIState -> ProtVer)
-> (Trace UPIREG -> UPIState) -> Trace UPIREG -> ProtVer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace UPIREG -> UPIState
Trace UPIREG -> State UPIREG
forall s. Trace s -> State s
_traceInitState

    increaseMinor :: Trace UPIREG -> Int
    increaseMinor :: Trace UPIREG -> Int
increaseMinor Trace UPIREG
traceSample =
      Trace UPIREG -> [ProtVer]
protocolVersions Trace UPIREG
traceSample
        [ProtVer] -> ([ProtVer] -> [Natural]) -> [Natural]
forall a b. a -> (a -> b) -> b
& (ProtVer -> Natural) -> [ProtVer] -> [Natural]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProtVer -> Natural
Update._pvMin
        [Natural] -> ([Natural] -> [Natural]) -> [Natural]
forall a b. a -> (a -> b) -> b
& (Natural -> Bool) -> [Natural] -> [Natural]
forall a. (a -> Bool) -> [a] -> [a]
filter (Trace UPIREG -> Natural
currPvMaj Trace UPIREG
traceSample Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<)
        [Natural] -> ([Natural] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [Natural] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length

    dontChangeProtocolVersion :: Trace UPIREG -> Int
    dontChangeProtocolVersion :: Trace UPIREG -> Int
dontChangeProtocolVersion Trace UPIREG
traceSample =
      Trace UPIREG -> [ProtVer]
protocolVersions Trace UPIREG
traceSample
        [ProtVer] -> ([ProtVer] -> [ProtVer]) -> [ProtVer]
forall a b. a -> (a -> b) -> b
& (ProtVer -> Bool) -> [ProtVer] -> [ProtVer]
forall a. (a -> Bool) -> [a] -> [a]
filter (Trace UPIREG -> ProtVer
currentProtocolVersion Trace UPIREG
traceSample ProtVer -> ProtVer -> Bool
forall a. Eq a => a -> a -> Bool
==)
        [ProtVer] -> ([ProtVer] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [ProtVer] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length

    -- Given a accessor function for the protocol parameters, count the number
    -- of update proposals that change the parameter value in the way specified
    -- by the 'Change' parameter.
    wrtCurrentProtocolParameters ::
      Ord v =>
      (PParams -> v) ->
      Change ->
      Trace UPIREG ->
      Int
    wrtCurrentProtocolParameters :: forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> v
parameterValue Change
parameterValueChange Trace UPIREG
traceSample =
      (UProp -> v) -> [UProp] -> [v]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PParams -> v
parameterValue (PParams -> v) -> (UProp -> PParams) -> UProp -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UProp -> PParams
Update._upParams) (TraceOrder -> Trace UPIREG -> [Signal UPIREG]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UPIREG
traceSample)
        [v] -> ([v] -> [v]) -> [v]
forall a b. a -> (a -> b) -> b
& (v -> Bool) -> [v] -> [v]
forall a. (a -> Bool) -> [a] -> [a]
filter (Change -> v -> Bool
check Change
parameterValueChange)
        [v] -> ([v] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [v] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
      where
        currentParameterValue :: v
currentParameterValue = PParams -> v
parameterValue (PParams -> v) -> (Trace UPIREG -> PParams) -> Trace UPIREG -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UPIState -> PParams
protocolParameters (UPIState -> PParams)
-> (Trace UPIREG -> UPIState) -> Trace UPIREG -> PParams
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Trace UPIREG -> UPIState
Trace UPIREG -> State UPIREG
forall s. Trace s -> State s
_traceInitState (Trace UPIREG -> v) -> Trace UPIREG -> v
forall a b. (a -> b) -> a -> b
$ Trace UPIREG
traceSample
        check :: Change -> v -> Bool
check Change
Increases v
proposedParameterValue = v
currentParameterValue v -> v -> Bool
forall a. Ord a => a -> a -> Bool
< v
proposedParameterValue
        check Change
Decreases v
proposedParameterValue = v
proposedParameterValue v -> v -> Bool
forall a. Ord a => a -> a -> Bool
< v
currentParameterValue
        check Change
RemainsTheSame v
proposedParameterValue = v
currentParameterValue v -> v -> Bool
forall a. Eq a => a -> a -> Bool
== v
proposedParameterValue

    -- TODO: leaving this here as it might be useful in the future. Remove if it
    -- isn't (dnadales - 07/17/2019). We use git, but nobody will see if it sits
    -- in our history.
    --
    -- Count the number of times in the sequence of update proposals that the
    -- given protocol value is set to the given value.
    --
    -- Example usage:
    --
    -- > cover 20
    -- >    "at least 5% of the update proposals set the maximum proposal-size to 0"
    -- > (0.05 <= ratio (Update._maxPropSz `isSetTo` 0) sample)
    -- isSetTo
    --   :: Eq v
    --   => (PParams -> v)
    --   -> v
    --   -> Trace UPIREG
    --   -> Int
    -- isSetTo parameterValue value traceSample
    --   = fmap (parameterValue . Update._upParams) (traceSignals OldestFirst traceSample)
    --   & filter (value ==)
    --   & length

    expectedNumberOfUpdateProposalsPerKey :: Trace UPIREG -> Double
    expectedNumberOfUpdateProposalsPerKey :: Trace UPIREG -> Double
expectedNumberOfUpdateProposalsPerKey Trace UPIREG
traceSample =
      if Int
numberOfGenesisKeys Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0
        then Double
0
        else Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Double) -> Int -> Double
forall a b. (a -> b) -> a -> b
$ Trace UPIREG -> Int
forall s. Trace s -> Int
traceLength Trace UPIREG
traceSample Int -> Int -> Int
forall a. Integral a => a -> a -> a
`div` Int
numberOfGenesisKeys
      where
        numberOfGenesisKeys :: Int
        numberOfGenesisKeys :: Int
numberOfGenesisKeys =
          [VKeyGenesis] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([VKeyGenesis] -> Int) -> [VKeyGenesis] -> Int
forall a b. (a -> b) -> a -> b
$
            Bimap VKeyGenesis VKey -> [VKeyGenesis]
forall a b. Bimap a b -> [a]
Bimap.keys (Bimap VKeyGenesis VKey -> [VKeyGenesis])
-> Bimap VKeyGenesis VKey -> [VKeyGenesis]
forall a b. (a -> b) -> a -> b
$
              UPIEnv -> Bimap VKeyGenesis VKey
forall {a} {b} {c} {d}. (a, b, c, d) -> b
delegationMap (Trace UPIREG -> Environment UPIREG
forall s. Trace s -> Environment s
_traceEnv Trace UPIREG
traceSample)

    issuersDeviationsWrtUniformDistribution ::
      Trace UPIREG ->
      [Double]
    issuersDeviationsWrtUniformDistribution :: Trace UPIREG -> [Double]
issuersDeviationsWrtUniformDistribution Trace UPIREG
traceSample =
      (UProp -> VKey) -> [UProp] -> [VKey]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UProp -> VKey
Update._upIssuer (TraceOrder -> Trace UPIREG -> [Signal UPIREG]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UPIREG
traceSample)
        [VKey] -> ([VKey] -> [(VKey, Int)]) -> [(VKey, Int)]
forall a b. a -> (a -> b) -> b
& [VKey] -> [(VKey, Int)]
forall a. Ord a => [a] -> [(a, Int)]
count
        -- Take the list of (issuer, count) pairs and keep the count only.
        [(VKey, Int)] -> ([(VKey, Int)] -> [Int]) -> [Int]
forall a b. a -> (a -> b) -> b
& ((VKey, Int) -> Int) -> [(VKey, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (VKey, Int) -> Int
forall a b. (a, b) -> b
snd
        [Int] -> ([Int] -> [Double]) -> [Double]
forall a b. a -> (a -> b) -> b
& (Int -> Double) -> [Int] -> [Double]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> Double
deviationFromExpectation
      where
        deviationFromExpectation :: Int -> Double
        deviationFromExpectation :: Int -> Double
deviationFromExpectation Int
numberOfProposalsPerKey =
          Double -> Double
forall a. Num a => a -> a
abs (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numberOfProposalsPerKey Double -> Double -> Double
forall a. Num a => a -> a -> a
- Trace UPIREG -> Double
expectedNumberOfUpdateProposalsPerKey Trace UPIREG
traceSample)

    delegationMap :: (a, b, c, d) -> b
delegationMap (a
_, b
dms, c
_, d
_) = b
dms

    safeMaximum :: t a -> a
safeMaximum t a
xs = if t a -> Bool
forall a. t a -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
xs then a
0 else t a -> a
forall a. Ord a => t a -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum t a
xs

-- | Change of a value w.r.t. some other value.
data Change = Increases | Decreases | RemainsTheSame

onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated =
  TestLimit -> Property -> Property
withTests TestLimit
300 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ forall s.
(HasTrace s, Show (Environment s), Show (State s), Show (Signal s),
 HasCallStack) =>
BaseEnv s -> Word64 -> Property
Transition.Generator.onlyValidSignalsAreGenerated @UPIREG () Word64
100

-- | Dummy transition system to test blocks with update payload only.
data UBLOCK deriving (Typeable UBLOCK
Typeable UBLOCK =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> UBLOCK -> c UBLOCK)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c UBLOCK)
-> (UBLOCK -> Constr)
-> (UBLOCK -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c UBLOCK))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UBLOCK))
-> ((forall b. Data b => b -> b) -> UBLOCK -> UBLOCK)
-> (forall r r'.
    (r -> r' -> r)
    -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r)
-> (forall u. (forall d. Data d => d -> u) -> UBLOCK -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> UBLOCK -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK)
-> Data UBLOCK
UBLOCK -> Constr
UBLOCK -> DataType
(forall b. Data b => b -> b) -> UBLOCK -> UBLOCK
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> UBLOCK -> u
forall u. (forall d. Data d => d -> u) -> UBLOCK -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UBLOCK
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UBLOCK -> c UBLOCK
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UBLOCK)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UBLOCK)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UBLOCK -> c UBLOCK
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UBLOCK -> c UBLOCK
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UBLOCK
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UBLOCK
$ctoConstr :: UBLOCK -> Constr
toConstr :: UBLOCK -> Constr
$cdataTypeOf :: UBLOCK -> DataType
dataTypeOf :: UBLOCK -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UBLOCK)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UBLOCK)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UBLOCK)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UBLOCK)
$cgmapT :: (forall b. Data b => b -> b) -> UBLOCK -> UBLOCK
gmapT :: (forall b. Data b => b -> b) -> UBLOCK -> UBLOCK
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r
$cgmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r
gmapQr :: forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UBLOCK -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> UBLOCK -> [u]
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UBLOCK -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UBLOCK -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
Data)

-- | An update block
data UBlock = UBlock
  { UBlock -> VKey
issuer :: Core.VKey
  , UBlock -> ProtVer
blockVersion :: ProtVer
  , UBlock -> Slot
slot :: Core.Slot
  , UBlock -> Maybe UProp
optionalUpdateProposal :: Maybe UProp
  , UBlock -> [Vote]
votes :: [Vote]
  }
  deriving (UBlock -> UBlock -> Bool
(UBlock -> UBlock -> Bool)
-> (UBlock -> UBlock -> Bool) -> Eq UBlock
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UBlock -> UBlock -> Bool
== :: UBlock -> UBlock -> Bool
$c/= :: UBlock -> UBlock -> Bool
/= :: UBlock -> UBlock -> Bool
Eq, Int -> UBlock -> ShowS
[UBlock] -> ShowS
UBlock -> [Char]
(Int -> UBlock -> ShowS)
-> (UBlock -> [Char]) -> ([UBlock] -> ShowS) -> Show UBlock
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UBlock -> ShowS
showsPrec :: Int -> UBlock -> ShowS
$cshow :: UBlock -> [Char]
show :: UBlock -> [Char]
$cshowList :: [UBlock] -> ShowS
showList :: [UBlock] -> ShowS
Show)

-- | Update block state
data UBlockState = UBlockState
  { UBlockState -> UPIEnv
upienv :: UPIEnv
  , UBlockState -> UPIState
upistate :: UPIState
  }
  deriving (UBlockState -> UBlockState -> Bool
(UBlockState -> UBlockState -> Bool)
-> (UBlockState -> UBlockState -> Bool) -> Eq UBlockState
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UBlockState -> UBlockState -> Bool
== :: UBlockState -> UBlockState -> Bool
$c/= :: UBlockState -> UBlockState -> Bool
/= :: UBlockState -> UBlockState -> Bool
Eq, Int -> UBlockState -> ShowS
[UBlockState] -> ShowS
UBlockState -> [Char]
(Int -> UBlockState -> ShowS)
-> (UBlockState -> [Char])
-> ([UBlockState] -> ShowS)
-> Show UBlockState
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UBlockState -> ShowS
showsPrec :: Int -> UBlockState -> ShowS
$cshow :: UBlockState -> [Char]
show :: UBlockState -> [Char]
$cshowList :: [UBlockState] -> ShowS
showList :: [UBlockState] -> ShowS
Show)

data UBlockPredicateFailure
  = UPIREGFailure (PredicateFailure UPIREG)
  | UPIVOTESFailure (PredicateFailure UPIVOTES)
  | UPIENDFailure (PredicateFailure UPIEND)
  | NotIncreasingBlockSlot
  deriving (UBlockPredicateFailure -> UBlockPredicateFailure -> Bool
(UBlockPredicateFailure -> UBlockPredicateFailure -> Bool)
-> (UBlockPredicateFailure -> UBlockPredicateFailure -> Bool)
-> Eq UBlockPredicateFailure
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UBlockPredicateFailure -> UBlockPredicateFailure -> Bool
== :: UBlockPredicateFailure -> UBlockPredicateFailure -> Bool
$c/= :: UBlockPredicateFailure -> UBlockPredicateFailure -> Bool
/= :: UBlockPredicateFailure -> UBlockPredicateFailure -> Bool
Eq, Int -> UBlockPredicateFailure -> ShowS
[UBlockPredicateFailure] -> ShowS
UBlockPredicateFailure -> [Char]
(Int -> UBlockPredicateFailure -> ShowS)
-> (UBlockPredicateFailure -> [Char])
-> ([UBlockPredicateFailure] -> ShowS)
-> Show UBlockPredicateFailure
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UBlockPredicateFailure -> ShowS
showsPrec :: Int -> UBlockPredicateFailure -> ShowS
$cshow :: UBlockPredicateFailure -> [Char]
show :: UBlockPredicateFailure -> [Char]
$cshowList :: [UBlockPredicateFailure] -> ShowS
showList :: [UBlockPredicateFailure] -> ShowS
Show, Typeable UBlockPredicateFailure
Typeable UBlockPredicateFailure =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g)
 -> UBlockPredicateFailure
 -> c UBlockPredicateFailure)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c UBlockPredicateFailure)
-> (UBlockPredicateFailure -> Constr)
-> (UBlockPredicateFailure -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c UBlockPredicateFailure))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e))
    -> Maybe (c UBlockPredicateFailure))
-> ((forall b. Data b => b -> b)
    -> UBlockPredicateFailure -> UBlockPredicateFailure)
-> (forall r r'.
    (r -> r' -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> UBlockPredicateFailure
    -> r)
-> (forall r r'.
    (r' -> r -> r)
    -> r
    -> (forall d. Data d => d -> r')
    -> UBlockPredicateFailure
    -> r)
-> (forall u.
    (forall d. Data d => d -> u) -> UBlockPredicateFailure -> [u])
-> (forall u.
    Int -> (forall d. Data d => d -> u) -> UBlockPredicateFailure -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d)
    -> UBlockPredicateFailure -> m UBlockPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> UBlockPredicateFailure -> m UBlockPredicateFailure)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d)
    -> UBlockPredicateFailure -> m UBlockPredicateFailure)
-> Data UBlockPredicateFailure
UBlockPredicateFailure -> Constr
UBlockPredicateFailure -> DataType
(forall b. Data b => b -> b)
-> UBlockPredicateFailure -> UBlockPredicateFailure
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u.
Int -> (forall d. Data d => d -> u) -> UBlockPredicateFailure -> u
forall u.
(forall d. Data d => d -> u) -> UBlockPredicateFailure -> [u]
forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UBlockPredicateFailure
-> r
forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> UBlockPredicateFailure
-> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UBlockPredicateFailure -> m UBlockPredicateFailure
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UBlockPredicateFailure -> m UBlockPredicateFailure
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UBlockPredicateFailure
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UBlockPredicateFailure
-> c UBlockPredicateFailure
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UBlockPredicateFailure)
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UBlockPredicateFailure)
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UBlockPredicateFailure
-> c UBlockPredicateFailure
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g)
-> UBlockPredicateFailure
-> c UBlockPredicateFailure
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UBlockPredicateFailure
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UBlockPredicateFailure
$ctoConstr :: UBlockPredicateFailure -> Constr
toConstr :: UBlockPredicateFailure -> Constr
$cdataTypeOf :: UBlockPredicateFailure -> DataType
dataTypeOf :: UBlockPredicateFailure -> DataType
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UBlockPredicateFailure)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UBlockPredicateFailure)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UBlockPredicateFailure)
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e))
-> Maybe (c UBlockPredicateFailure)
$cgmapT :: (forall b. Data b => b -> b)
-> UBlockPredicateFailure -> UBlockPredicateFailure
gmapT :: (forall b. Data b => b -> b)
-> UBlockPredicateFailure -> UBlockPredicateFailure
$cgmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UBlockPredicateFailure
-> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r
-> (forall d. Data d => d -> r')
-> UBlockPredicateFailure
-> r
$cgmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> UBlockPredicateFailure
-> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r
-> (forall d. Data d => d -> r')
-> UBlockPredicateFailure
-> r
$cgmapQ :: forall u.
(forall d. Data d => d -> u) -> UBlockPredicateFailure -> [u]
gmapQ :: forall u.
(forall d. Data d => d -> u) -> UBlockPredicateFailure -> [u]
$cgmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UBlockPredicateFailure -> u
gmapQi :: forall u.
Int -> (forall d. Data d => d -> u) -> UBlockPredicateFailure -> u
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UBlockPredicateFailure -> m UBlockPredicateFailure
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d)
-> UBlockPredicateFailure -> m UBlockPredicateFailure
$cgmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UBlockPredicateFailure -> m UBlockPredicateFailure
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UBlockPredicateFailure -> m UBlockPredicateFailure
$cgmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UBlockPredicateFailure -> m UBlockPredicateFailure
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d)
-> UBlockPredicateFailure -> m UBlockPredicateFailure
Data)

instance STS UBLOCK where
  type Environment UBLOCK = UPIEnv

  type State UBLOCK = UBlockState

  type Signal UBLOCK = UBlock

  type PredicateFailure UBLOCK = UBlockPredicateFailure

  initialRules :: [InitialRule UBLOCK]
initialRules =
    [ do
        IRC env <- Rule UBLOCK 'Initial (RuleContext 'Initial UBLOCK)
F (Clause UBLOCK 'Initial) (IRC UBLOCK)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let (_, _, k, _) = env
            -- TODO: I (dnadales) should have used records for the UPIState :/
            ((pv, pps), fads, avs, rpus, raus, cps, vts, bvs, pws) = emptyUPIState
        -- We overwrite 'upTtl' in the UBLOCK initial rule, so that we have a system where update
        -- proposals can live long enough to allow for confirmation and consideration for
        -- adoption. We set the time to live of a proposal to half the number of slots in an
        -- epoch, which is about the same value we use in production.
        pure
          UBlockState
            { upienv = env
            , upistate =
                ( (pv, pps {Update._upTtl = SlotCount $ slotsPerEpoch k `div` 2})
                , fads
                , avs
                , rpus
                , raus
                , cps
                , vts
                , bvs
                , pws
                )
            }
    ]

  transitionRules :: [TransitionRule UBLOCK]
transitionRules =
    [ do
        TRC (_, UBlockState {upienv, upistate}, ublock) <- Rule UBLOCK 'Transition (RuleContext 'Transition UBLOCK)
F (Clause UBLOCK 'Transition) (TRC UBLOCK)
forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let (sn, dms, k, ngk) = upienv
        sn < slot ublock ?! NotIncreasingBlockSlot
        upistateAfterRegistration <-
          case optionalUpdateProposal ublock of
            Maybe UProp
Nothing -> UPIState -> F (Clause UBLOCK 'Transition) UPIState
forall a. a -> F (Clause UBLOCK 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure UPIState
upistate
            Just UProp
updateProposal ->
              forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIREG (RuleContext 'Transition UPIREG
 -> Rule UBLOCK 'Transition (State UPIREG))
-> RuleContext 'Transition UPIREG
-> Rule UBLOCK 'Transition (State UPIREG)
forall a b. (a -> b) -> a -> b
$ (Environment UPIREG, State UPIREG, Signal UPIREG) -> TRC UPIREG
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UPIEnv
Environment UPIREG
upienv, UPIState
State UPIREG
upistate, UProp
Signal UPIREG
updateProposal)
        upistateAfterVoting <-
          trans @UPIVOTES $ TRC (upienv, upistateAfterRegistration, votes ublock)
        upistateAfterEndorsement <-
          trans @UPIEND $ TRC (upienv, upistateAfterVoting, (blockVersion ublock, issuer ublock))
        pure
          UBlockState
            { upienv = (slot ublock, dms, k, ngk)
            , upistate = upistateAfterEndorsement
            }
    ]

instance Embed UPIREG UBLOCK where
  wrapFailed :: PredicateFailure UPIREG -> PredicateFailure UBLOCK
wrapFailed = PredicateFailure UPIREG -> PredicateFailure UBLOCK
PredicateFailure UPIREG -> UBlockPredicateFailure
UPIREGFailure

instance Embed UPIVOTES UBLOCK where
  wrapFailed :: PredicateFailure UPIVOTES -> PredicateFailure UBLOCK
wrapFailed = PredicateFailure UPIVOTES -> PredicateFailure UBLOCK
PredicateFailure UPIVOTES -> UBlockPredicateFailure
UPIVOTESFailure

instance Embed UPIEND UBLOCK where
  wrapFailed :: PredicateFailure UPIEND -> PredicateFailure UBLOCK
wrapFailed = PredicateFailure UPIEND -> PredicateFailure UBLOCK
PredicateFailure UPIEND -> UBlockPredicateFailure
UPIENDFailure

instance HasTrace UBLOCK where
  envGen :: Word64 -> Gen (Environment UBLOCK)
envGen Word64
_ =
    do
      let numberOfGenesisKeys :: Word8
numberOfGenesisKeys = Word8
7
      dms <- Word8 -> Gen (Bimap VKeyGenesis VKey)
Update.dmapGen Word8
numberOfGenesisKeys
      -- We don't want a large value of @k@, otherwise we won't see many
      -- confirmed proposals or epoch changes. The problem here is that the
      -- initial environment does not know anything about the trace size, and
      -- @k@ should be a function of it.
      pure (Slot 0, dms, BlockCount 10, numberOfGenesisKeys)

  sigGen :: SignalGenerator UBLOCK
sigGen Environment UBLOCK
_env UBlockState {UPIEnv
upienv :: UBlockState -> UPIEnv
upienv :: UPIEnv
upienv, UPIState
upistate :: UBlockState -> UPIState
upistate :: UPIState
upistate} = do
    (anOptionalUpdateProposal, aListOfVotes) <-
      UPIEnv -> UPIState -> Gen (Maybe UProp, [Vote])
Update.updateProposalAndVotesGen UPIEnv
upienv UPIState
upistate

    -- Don't shrink the issuer as this won't give us additional insight on a
    -- test failure.
    aBlockIssuer <-
      Gen.prune $
        -- Pick a delegate from the delegation map
        Gen.element $
          Bimap.elems (Update.delegationMap upienv)

    aBlockVersion <-
      Update.protocolVersionEndorsementGen upienv upistate

    UBlock
      <$> pure aBlockIssuer
      <*> pure aBlockVersion
      <*> nextSlotGen
      <*> pure anOptionalUpdateProposal
      <*> pure aListOfVotes
    where
      nextSlotGen :: GenT Identity Slot
nextSlotGen =
        Word64 -> Slot
incSlot
          (Word64 -> Slot) -> GenT Identity Word64 -> GenT Identity Slot
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int, GenT Identity Word64)] -> GenT Identity Word64
forall (m :: * -> *) a.
(HasCallStack, MonadGen m) =>
[(Int, m a)] -> m a
Gen.frequency
            [ (Int
5, Range Word64 -> GenT Identity Word64
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Word64 -> Word64 -> Range Word64
forall a. a -> a -> Range a
Range.constant Word64
1 Word64
10))
            , (Int
1, Range Word64 -> GenT Identity Word64
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Word64 -> Word64 -> Range Word64
forall a. Integral a => a -> a -> Range a
Range.linear Word64
10 (BlockCount -> Word64
unBlockCount BlockCount
k)))
            ]
        where
          incSlot :: Word64 -> Slot
incSlot Word64
c = Slot
sn Slot -> SlotCount -> Slot
`Core.addSlot` Word64 -> SlotCount
Core.SlotCount Word64
c
          (Slot
sn, Bimap VKeyGenesis VKey
_, BlockCount
k, Word8
_) = UPIEnv
upienv

ublockTraceLengthsAreClassified :: Property
ublockTraceLengthsAreClassified :: Property
ublockTraceLengthsAreClassified =
  TestLimit -> Property -> Property
withTests TestLimit
100 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ forall s.
(HasTrace s, Show (Environment s), Show (State s),
 Show (Signal s)) =>
BaseEnv s -> Word64 -> Word64 -> Property
traceLengthsAreClassified @UBLOCK () Word64
100 Word64
10

ublockOnlyValidSignalsAreGenerated :: HasCallStack => Property
ublockOnlyValidSignalsAreGenerated :: HasCallStack => Property
ublockOnlyValidSignalsAreGenerated =
  TestLimit -> Property -> Property
withTests TestLimit
300 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ forall s.
(HasTrace s, Show (Environment s), Show (State s), Show (Signal s),
 HasCallStack) =>
BaseEnv s -> Word64 -> Property
Transition.Generator.onlyValidSignalsAreGenerated @UBLOCK () Word64
100

ublockRelevantTracesAreCovered :: Property
ublockRelevantTracesAreCovered :: Property
ublockRelevantTracesAreCovered = TestLimit -> Property -> Property
withTests TestLimit
300 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
  HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
    sample <- Gen (Trace UBLOCK) -> PropertyT IO (Trace UBLOCK)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
traceOfLength @UBLOCK () Word64
100)

    -- Since we generate votes on the most voted proposals, we do not expect a very large percentage
    -- of confirmed proposals. As a reference, in the runs that were performed manually, for a trace
    -- of 500 blocks, 80-90 update proposals and 20-30 confirmed proposals were observed.
    cover
      75
      "at least 20% of the proposals get confirmed"
      (0.2 <= confirmedProposals sample / totalProposals sample)

    cover
      75
      "at least 30% of the proposals get unconfirmed"
      (0.3 <= 1 - (confirmedProposals sample / totalProposals sample))

    cover
      75
      "at least 2% of the proposals get voted in the same block "
      (0.02 <= fromIntegral (numberOfVotesForBlockProposal sample) / totalProposals sample)

    cover
      75
      "at least 30% of blocks contain no votes"
      (0.3 <= ratio numberOfBlocksWithoutVotes sample)

    -- Once the most voted update proposals get votes from all the genesis keys there is no
    -- possibility of generating any more votes. So we do not expect a large percentage of blocks with
    -- votes.
    cover
      70
      "at least 10% of blocks contain votes"
      (0.1 <= 1 - ratio numberOfBlocksWithoutVotes sample)

    -- We generate an update proposal with a probability 1/4, but we're conservative about the
    -- coverage requirements, since we have variable trace lengths.
    cover
      75
      "at least 70% of the blocks contain no update proposals"
      (0.7 <= ratio numberOfBlocksWithoutUpdateProposals sample)

    cover
      75
      "at least 10% of the blocks contain an update proposals"
      (0.1 <= 1 - ratio numberOfBlocksWithoutUpdateProposals sample)

    -- With traces of length 500, we expect to see about 80-90 proposals, which means that we will
    -- have about 8 to 9 proposals scheduled for adoption.
    cover
      60
      "at least 10% of the proposals get enough endorsements"
      (0.1 <= proposalsScheduledForAdoption sample / totalProposals sample)

    cover
      80
      "at least 5% of the proposals get enough endorsements"
      (0.05 <= proposalsScheduledForAdoption sample / totalProposals sample)

confirmedProposals :: Trace UBLOCK -> Double
confirmedProposals :: Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample =
  TraceOrder -> Trace UBLOCK -> [State UBLOCK]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace UBLOCK
sample
    [UBlockState] -> ([UBlockState] -> [UPIState]) -> [UPIState]
forall a b. a -> (a -> b) -> b
& (UBlockState -> UPIState) -> [UBlockState] -> [UPIState]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UBlockState -> UPIState
upistate
    [UPIState] -> ([UPIState] -> [Map UpId Slot]) -> [Map UpId Slot]
forall a b. a -> (a -> b) -> b
& (UPIState -> Map UpId Slot) -> [UPIState] -> [Map UpId Slot]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UPIState -> Map UpId Slot
Update.confirmedProposals
    [Map UpId Slot] -> ([Map UpId Slot] -> [Set UpId]) -> [Set UpId]
forall a b. a -> (a -> b) -> b
& (Map UpId Slot -> Set UpId) -> [Map UpId Slot] -> [Set UpId]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Map UpId Slot -> Set (Domain (Map UpId Slot))
Map UpId Slot -> Set UpId
forall m. (Relation m, Ord (Domain m)) => m -> Set (Domain m)
dom
    [Set UpId] -> ([Set UpId] -> Set UpId) -> Set UpId
forall a b. a -> (a -> b) -> b
& [Set UpId] -> Set UpId
forall m. Monoid m => [m] -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold
    Set UpId -> (Set UpId -> Int) -> Int
forall a b. a -> (a -> b) -> b
& Set UpId -> Int
forall a. Set a -> Int
Set.size
    Int -> (Int -> Double) -> Double
forall a b. a -> (a -> b) -> b
& Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral

totalProposals :: Trace UBLOCK -> Double
totalProposals :: Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample =
  TraceOrder -> Trace UBLOCK -> [Signal UBLOCK]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UBLOCK
sample
    [UBlock] -> ([UBlock] -> [Maybe UProp]) -> [Maybe UProp]
forall a b. a -> (a -> b) -> b
& (UBlock -> Maybe UProp) -> [UBlock] -> [Maybe UProp]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UBlock -> Maybe UProp
optionalUpdateProposal
    [Maybe UProp] -> ([Maybe UProp] -> [UProp]) -> [UProp]
forall a b. a -> (a -> b) -> b
& [Maybe UProp] -> [UProp]
forall a. [Maybe a] -> [a]
catMaybes
    [UProp] -> ([UProp] -> [UpId]) -> [UpId]
forall a b. a -> (a -> b) -> b
& (UProp -> UpId) -> [UProp] -> [UpId]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UProp -> UpId
Update._upId
    [UpId] -> ([UpId] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [UpId] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
    Int -> (Int -> Double) -> Double
forall a b. a -> (a -> b) -> b
& Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral

-- Count the number of votes for proposals that were included in the same
-- block as the votes.
numberOfVotesForBlockProposal :: Trace UBLOCK -> Int
numberOfVotesForBlockProposal :: Trace UBLOCK -> Int
numberOfVotesForBlockProposal Trace UBLOCK
sample =
  TraceOrder -> Trace UBLOCK -> [Signal UBLOCK]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UBLOCK
sample
    [UBlock] -> ([UBlock] -> [UBlock]) -> [UBlock]
forall a b. a -> (a -> b) -> b
& (UBlock -> Bool) -> [UBlock] -> [UBlock]
forall a. (a -> Bool) -> [a] -> [a]
filter UBlock -> Bool
voteForBlockProposal
    [UBlock] -> ([UBlock] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [UBlock] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length
  where
    voteForBlockProposal :: UBlock -> Bool
    voteForBlockProposal :: UBlock -> Bool
voteForBlockProposal UBlock {Maybe UProp
optionalUpdateProposal :: UBlock -> Maybe UProp
optionalUpdateProposal :: Maybe UProp
optionalUpdateProposal, [Vote]
votes :: UBlock -> [Vote]
votes :: [Vote]
votes} =
      case Maybe UProp
optionalUpdateProposal of
        Maybe UProp
Nothing ->
          Bool
False
        Just UProp
updateProposal ->
          UProp -> UpId
Update._upId UProp
updateProposal UpId -> [UpId] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Vote -> UpId
Update._vPropId (Vote -> UpId) -> [Vote] -> [UpId]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Vote]
votes)

numberOfBlocksWithoutVotes :: Trace UBLOCK -> Int
numberOfBlocksWithoutVotes :: Trace UBLOCK -> Int
numberOfBlocksWithoutVotes Trace UBLOCK
sample =
  TraceOrder -> Trace UBLOCK -> [Signal UBLOCK]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UBLOCK
sample
    [UBlock] -> ([UBlock] -> [UBlock]) -> [UBlock]
forall a b. a -> (a -> b) -> b
& (UBlock -> Bool) -> [UBlock] -> [UBlock]
forall a. (a -> Bool) -> [a] -> [a]
filter ([Vote] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Vote] -> Bool) -> (UBlock -> [Vote]) -> UBlock -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UBlock -> [Vote]
votes)
    [UBlock] -> ([UBlock] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [UBlock] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length

numberOfBlocksWithoutUpdateProposals :: Trace UBLOCK -> Int
numberOfBlocksWithoutUpdateProposals :: Trace UBLOCK -> Int
numberOfBlocksWithoutUpdateProposals Trace UBLOCK
sample =
  TraceOrder -> Trace UBLOCK -> [Signal UBLOCK]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UBLOCK
sample
    [UBlock] -> ([UBlock] -> [UBlock]) -> [UBlock]
forall a b. a -> (a -> b) -> b
& (UBlock -> Bool) -> [UBlock] -> [UBlock]
forall a. (a -> Bool) -> [a] -> [a]
filter (Maybe UProp -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe UProp -> Bool) -> (UBlock -> Maybe UProp) -> UBlock -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UBlock -> Maybe UProp
optionalUpdateProposal)
    [UBlock] -> ([UBlock] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [UBlock] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length

proposalsScheduledForAdoption :: Trace UBLOCK -> Double
proposalsScheduledForAdoption :: Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample =
  TraceOrder -> Trace UBLOCK -> [State UBLOCK]
forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace UBLOCK
sample
    [UBlockState] -> ([UBlockState] -> [UPIState]) -> [UPIState]
forall a b. a -> (a -> b) -> b
& (UBlockState -> UPIState) -> [UBlockState] -> [UPIState]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UBlockState -> UPIState
upistate
    -- We concat all the future adoptions together
    [UPIState]
-> ([UPIState] -> [(Slot, (ProtVer, PParams))])
-> [(Slot, (ProtVer, PParams))]
forall a b. a -> (a -> b) -> b
& (UPIState -> [(Slot, (ProtVer, PParams))])
-> [UPIState] -> [(Slot, (ProtVer, PParams))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap UPIState -> [(Slot, (ProtVer, PParams))]
Update.futureAdoptions
    -- Get the protocol versions of the future adoptions
    [(Slot, (ProtVer, PParams))]
-> ([(Slot, (ProtVer, PParams))] -> [ProtVer]) -> [ProtVer]
forall a b. a -> (a -> b) -> b
& ((Slot, (ProtVer, PParams)) -> ProtVer)
-> [(Slot, (ProtVer, PParams))] -> [ProtVer]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((ProtVer, PParams) -> ProtVer
forall a b. (a, b) -> a
fst ((ProtVer, PParams) -> ProtVer)
-> ((Slot, (ProtVer, PParams)) -> (ProtVer, PParams))
-> (Slot, (ProtVer, PParams))
-> ProtVer
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Slot, (ProtVer, PParams)) -> (ProtVer, PParams)
forall a b. (a, b) -> b
snd)
    -- Turn the list of versions into a list, since we're
    -- interested in the number of unique protocol-versions
    -- that are scheduled for adoption through the trace
    -- states.
    [ProtVer] -> ([ProtVer] -> Set ProtVer) -> Set ProtVer
forall a b. a -> (a -> b) -> b
& [ProtVer] -> Set ProtVer
forall a. Ord a => [a] -> Set a
Set.fromList
    Set ProtVer -> (Set ProtVer -> Int) -> Int
forall a b. a -> (a -> b) -> b
& Set ProtVer -> Int
forall a. Set a -> Int
Set.size
    Int -> (Int -> Double) -> Double
forall a b. a -> (a -> b) -> b
& Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral

-- | Sample a 'UBLOCK' trace, and print different metrics. This can be used in the REPL, and it is
-- useful for understanding the traces produced by the 'UBLOCK' transition system.
ublockSampleTraceMetrics :: Word64 -> IO ()
ublockSampleTraceMetrics :: Word64 -> IO ()
ublockSampleTraceMetrics Word64
maxTraceSize = do
  sample <- forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s)
randomTraceOfSize @UBLOCK () Word64
maxTraceSize
  let (_slot, _dms, k, numberOfGenesisKeys) = _traceEnv sample
  traverse_
    print
    [ "k = "
        ++ show k
    , "genesis keys = "
        ++ show numberOfGenesisKeys
    , "trace length = "
        ++ show (traceLength sample)
    , "proposals = "
        ++ show (totalProposals sample)
    , "confirmed proposals = "
        ++ show (confirmedProposals sample)
    , "scheduled proposals = "
        ++ show (proposalsScheduledForAdoption sample)
    , "total number of votes = "
        ++ show (numberOfVotes sample)
    , "blocks without votes = "
        ++ show (numberOfBlocksWithoutVotes sample)
    , "votes for block proposal in same block = "
        ++ show (numberOfVotesForBlockProposal sample)
    , "ratio of votes for block proposal in same block = "
        ++ show (fromIntegral (numberOfVotesForBlockProposal sample) / totalProposals sample)
    , "proposals scheduled for adoption = "
        ++ show (proposalsScheduledForAdoption sample)
    , "confirmed / total proposals = "
        ++ show (confirmedProposals sample / totalProposals sample)
    , "scheduled / total proposals = "
        ++ show (proposalsScheduledForAdoption sample / totalProposals sample)
    , "scheduled / confirmed proposals = "
        ++ show (proposalsScheduledForAdoption sample / confirmedProposals sample)
    ]

numberOfVotes :: Trace UBLOCK -> Int
numberOfVotes :: Trace UBLOCK -> Int
numberOfVotes Trace UBLOCK
sample =
  TraceOrder -> Trace UBLOCK -> [Signal UBLOCK]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UBLOCK
sample
    [UBlock] -> ([UBlock] -> [Vote]) -> [Vote]
forall a b. a -> (a -> b) -> b
& (UBlock -> [Vote]) -> [UBlock] -> [Vote]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap UBlock -> [Vote]
votes
    [Vote] -> ([Vote] -> Int) -> Int
forall a b. a -> (a -> b) -> b
& [Vote] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length