{-# 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, Typeable)
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 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 forall a b. (a -> b) -> a -> b
$
  HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
    Trace UPIREG
sample <- 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)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
40
      LabelName
"at least 30% of the update proposals increase the major version"
      (Double
0.25 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UPIREG -> Int
increaseMajor Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
40
      LabelName
"at least 30% of the update proposals increase the minor version"
      (Double
0.25 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UPIREG -> Int
increaseMinor Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
30
      LabelName
"at least 10% of the update proposals do not change the protocol version"
      (Double
0.10 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UPIREG -> Int
dontChangeProtocolVersion Trace UPIREG
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).
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"the distribution of the proposal issuers is roughly fair"
      ( forall {t :: * -> *} {a}. (Foldable t, Num a, Ord a) => t a -> a
safeMaximum (Trace UPIREG -> [Double]
issuersDeviationsWrtUniformDistribution Trace UPIREG
sample)
          forall a. Ord a => a -> a -> Bool
<= Trace UPIREG -> Double
expectedNumberOfUpdateProposalsPerKey Trace UPIREG
sample forall a. Num a => a -> a -> a
* Double
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.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
20
      LabelName
"at least 5% of the update proposals decrease the maximum block-size"
      (Double
0.05 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxBkSz Change
Decreases) Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 30% of the update proposals increase the maximum block-size"
      (Double
0.3 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxBkSz Change
Increases) Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
30
      LabelName
"at least 10% of the update proposals do not change the maximum block-size"
      (Double
0.1 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxBkSz Change
RemainsTheSame) Trace UPIREG
sample)

    --------------------------------------------------------------------------------
    -- Maximum header-size checks
    --------------------------------------------------------------------------------
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
20
      LabelName
"at least 5% of the update proposals decrease the maximum header-size"
      (Double
0.05 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxHdrSz Change
Decreases) Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 30% of the update proposals increase the maximum header-size"
      (Double
0.3 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxHdrSz Change
Increases) Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 10% of the update proposals do not change the maximum header-size"
      (Double
0.1 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxHdrSz Change
RemainsTheSame) Trace UPIREG
sample)

    --------------------------------------------------------------------------------
    -- Maximum transaction-size checks
    --------------------------------------------------------------------------------
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
20
      LabelName
"at least 5% of the update proposals decrease the maximum transaction-size"
      (Double
0.05 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxTxSz Change
Decreases) Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 30% of the update proposals increase the maximum transaction-size"
      (Double
0.3 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxTxSz Change
Increases) Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
40
      LabelName
"at least 10% of the update proposals do not change the maximum transaction-size"
      (Double
0.1 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxTxSz Change
RemainsTheSame) Trace UPIREG
sample)

    --------------------------------------------------------------------------------
    -- Maximum proposal-size checks
    --------------------------------------------------------------------------------
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
20
      LabelName
"at least 30% of the update proposals decrease the maximum proposal-size"
      (Double
0.05 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxPropSz Change
Decreases) Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 30% of the update proposals increase the maximum proposal-size"
      (Double
0.3 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxPropSz Change
Increases) Trace UPIREG
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"at least 10% of the update proposals do not change the maximum proposal-size"
      (Double
0.1 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio (forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxPropSz Change
RemainsTheSame) Trace UPIREG
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
        forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProtVer -> Natural
Update._pvMaj
        forall a b. a -> (a -> b) -> b
& forall a. (a -> Bool) -> [a] -> [a]
filter (Trace UPIREG -> Natural
currPvMaj Trace UPIREG
traceSample forall a. Ord a => a -> a -> Bool
<)
        forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) a. Foldable t => t a -> Int
length

    protocolVersions :: Trace UPIREG -> [Update.ProtVer]
    protocolVersions :: Trace UPIREG -> [ProtVer]
protocolVersions Trace UPIREG
tr =
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UProp -> ProtVer
Update._upPV (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 forall b c a. (b -> c) -> (a -> b) -> a -> c
. UPIState -> ProtVer
Update.protocolVersion forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Trace s -> State s
_traceInitState

    currentProtocolVersion :: Trace UPIREG -> Update.ProtVer
    currentProtocolVersion :: Trace UPIREG -> ProtVer
currentProtocolVersion = UPIState -> ProtVer
Update.protocolVersion forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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
        forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ProtVer -> Natural
Update._pvMin
        forall a b. a -> (a -> b) -> b
& forall a. (a -> Bool) -> [a] -> [a]
filter (Trace UPIREG -> Natural
currPvMaj Trace UPIREG
traceSample forall a. Ord a => a -> a -> Bool
<)
        forall a b. a -> (a -> b) -> b
& 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
        forall a b. a -> (a -> b) -> b
& forall a. (a -> Bool) -> [a] -> [a]
filter (Trace UPIREG -> ProtVer
currentProtocolVersion Trace UPIREG
traceSample forall a. Eq a => a -> a -> Bool
==)
        forall a b. a -> (a -> b) -> b
& 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 =
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (PParams -> v
parameterValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. UProp -> PParams
Update._upParams) (forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UPIREG
traceSample)
        forall a b. a -> (a -> b) -> b
& forall a. (a -> Bool) -> [a] -> [a]
filter (Change -> v -> Bool
check Change
parameterValueChange)
        forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) a. Foldable t => t a -> Int
length
      where
        currentParameterValue :: v
currentParameterValue = PParams -> v
parameterValue forall b c a. (b -> c) -> (a -> b) -> a -> c
. UPIState -> PParams
protocolParameters forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s. Trace s -> State s
_traceInitState forall a b. (a -> b) -> a -> b
$ Trace UPIREG
traceSample
        check :: Change -> v -> Bool
check Change
Increases v
proposedParameterValue = v
currentParameterValue forall a. Ord a => a -> a -> Bool
< v
proposedParameterValue
        check Change
Decreases v
proposedParameterValue = v
proposedParameterValue forall a. Ord a => a -> a -> Bool
< v
currentParameterValue
        check Change
RemainsTheSame v
proposedParameterValue = v
currentParameterValue 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 forall a. Eq a => a -> a -> Bool
== Int
0
        then Double
0
        else forall a b. (Integral a, Num b) => a -> b
fromIntegral forall a b. (a -> b) -> a -> b
$ forall s. Trace s -> Int
traceLength Trace UPIREG
traceSample forall a. Integral a => a -> a -> a
`div` Int
numberOfGenesisKeys
      where
        numberOfGenesisKeys :: Int
        numberOfGenesisKeys :: Int
numberOfGenesisKeys =
          forall (t :: * -> *) a. Foldable t => t a -> Int
length forall a b. (a -> b) -> a -> b
$
            forall a b. Bimap a b -> [a]
Bimap.keys forall a b. (a -> b) -> a -> b
$
              forall {a} {b} {c} {d}. (a, b, c, d) -> b
delegationMap (forall s. Trace s -> Environment s
_traceEnv Trace UPIREG
traceSample)

    issuersDeviationsWrtUniformDistribution ::
      Trace UPIREG ->
      [Double]
    issuersDeviationsWrtUniformDistribution :: Trace UPIREG -> [Double]
issuersDeviationsWrtUniformDistribution Trace UPIREG
traceSample =
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UProp -> VKey
Update._upIssuer (forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UPIREG
traceSample)
        forall a b. a -> (a -> b) -> b
& forall a. Ord a => [a] -> [(a, Int)]
count
        -- Take the list of (issuer, count) pairs and keep the count only.
        forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a b. (a, b) -> b
snd
        forall a b. a -> (a -> b) -> 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 =
          forall a. Num a => a -> a
abs (forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
numberOfProposalsPerKey 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 forall (t :: * -> *) a. Foldable t => t a -> Bool
null t a
xs then a
0 else 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 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
UBLOCK -> DataType
UBLOCK -> Constr
(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)
gmapMo :: 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
gmapMp :: forall (m :: * -> *).
MonadPlus 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
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
$cgmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> UBLOCK -> m UBLOCK
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UBLOCK -> u
$cgmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> UBLOCK -> u
gmapQ :: forall u. (forall d. Data d => d -> u) -> UBLOCK -> [u]
$cgmapQ :: forall u. (forall d. Data d => d -> u) -> UBLOCK -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r
$cgmapQl :: forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> UBLOCK -> r
gmapT :: (forall b. Data b => b -> b) -> UBLOCK -> UBLOCK
$cgmapT :: (forall b. Data b => b -> b) -> UBLOCK -> UBLOCK
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UBLOCK)
$cdataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c UBLOCK)
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UBLOCK)
$cdataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c UBLOCK)
dataTypeOf :: UBLOCK -> DataType
$cdataTypeOf :: UBLOCK -> DataType
toConstr :: UBLOCK -> Constr
$ctoConstr :: UBLOCK -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UBLOCK
$cgunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c UBLOCK
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UBLOCK -> c UBLOCK
$cgfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> UBLOCK -> c UBLOCK
Data, Typeable)

-- | 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
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: UBlock -> UBlock -> Bool
$c/= :: UBlock -> UBlock -> Bool
== :: UBlock -> UBlock -> Bool
$c== :: UBlock -> UBlock -> Bool
Eq, Int -> UBlock -> ShowS
[UBlock] -> ShowS
UBlock -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [UBlock] -> ShowS
$cshowList :: [UBlock] -> ShowS
show :: UBlock -> [Char]
$cshow :: UBlock -> [Char]
showsPrec :: Int -> UBlock -> ShowS
$cshowsPrec :: Int -> UBlock -> ShowS
Show)

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

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

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 Environment UBLOCK
env <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let (Slot
_, Bimap VKeyGenesis VKey
_, BlockCount
k, Word8
_) = Environment UBLOCK
env
            -- TODO: I (dnadales) should have used records for the UPIState :/
            ((ProtVer
pv, PParams
pps), [(Slot, (ProtVer, PParams))]
fads, Map ApName (ApVer, Slot, Metadata)
avs, Map UpId (ProtVer, PParams)
rpus, Map UpId (ApName, ApVer, Metadata)
raus, Map UpId Slot
cps, Set (UpId, VKeyGenesis)
vts, Set (ProtVer, VKeyGenesis)
bvs, Map UpId Slot
pws) = UPIState
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.
        forall (f :: * -> *) a. Applicative f => a -> f a
pure
          UBlockState
            { upienv :: UPIEnv
upienv = Environment UBLOCK
env
            , upistate :: UPIState
upistate =
                ( (ProtVer
pv, PParams
pps {_upTtl :: SlotCount
Update._upTtl = Word64 -> SlotCount
SlotCount forall a b. (a -> b) -> a -> b
$ forall n. Integral n => BlockCount -> n
slotsPerEpoch BlockCount
k forall a. Integral a => a -> a -> a
`div` Word64
2})
                , [(Slot, (ProtVer, PParams))]
fads
                , Map ApName (ApVer, Slot, Metadata)
avs
                , Map UpId (ProtVer, PParams)
rpus
                , Map UpId (ApName, ApVer, Metadata)
raus
                , Map UpId Slot
cps
                , Set (UpId, VKeyGenesis)
vts
                , Set (ProtVer, VKeyGenesis)
bvs
                , Map UpId Slot
pws
                )
            }
    ]

  transitionRules :: [TransitionRule UBLOCK]
transitionRules =
    [ do
        TRC (Environment UBLOCK
_, UBlockState {UPIEnv
upienv :: UPIEnv
upienv :: UBlockState -> UPIEnv
upienv, UPIState
upistate :: UPIState
upistate :: UBlockState -> UPIState
upistate}, Signal UBLOCK
ublock) <- forall sts (rtype :: RuleType).
Rule sts rtype (RuleContext rtype sts)
judgmentContext
        let (Slot
sn, Bimap VKeyGenesis VKey
dms, BlockCount
k, Word8
ngk) = UPIEnv
upienv
        Slot
sn forall a. Ord a => a -> a -> Bool
< UBlock -> Slot
slot Signal UBLOCK
ublock forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! UBlockPredicateFailure
NotIncreasingBlockSlot
        UPIState
upistateAfterRegistration <-
          case UBlock -> Maybe UProp
optionalUpdateProposal Signal UBLOCK
ublock of
            Maybe UProp
Nothing -> 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 forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UPIEnv
upienv, UPIState
upistate, UProp
updateProposal)
        UPIState
upistateAfterVoting <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIVOTES forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UPIEnv
upienv, UPIState
upistateAfterRegistration, UBlock -> [Vote]
votes Signal UBLOCK
ublock)
        UPIState
upistateAfterEndorsement <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIEND forall a b. (a -> b) -> a -> b
$ forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UPIEnv
upienv, UPIState
upistateAfterVoting, (UBlock -> ProtVer
blockVersion Signal UBLOCK
ublock, UBlock -> VKey
issuer Signal UBLOCK
ublock))
        forall (f :: * -> *) a. Applicative f => a -> f a
pure
          UBlockState
            { upienv :: UPIEnv
upienv = (UBlock -> Slot
slot Signal UBLOCK
ublock, Bimap VKeyGenesis VKey
dms, BlockCount
k, Word8
ngk)
            , upistate :: UPIState
upistate = UPIState
upistateAfterEndorsement
            }
    ]

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

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

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

instance HasTrace UBLOCK where
  envGen :: Word64 -> Gen (Environment UBLOCK)
envGen Word64
_ =
    do
      let numberOfGenesisKeys :: Word8
numberOfGenesisKeys = Word8
7
      Bimap VKeyGenesis VKey
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.
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (Word64 -> Slot
Slot Word64
0, Bimap VKeyGenesis VKey
dms, Word64 -> BlockCount
BlockCount Word64
10, Word8
numberOfGenesisKeys)

  sigGen :: SignalGenerator UBLOCK
sigGen Environment UBLOCK
_env UBlockState {UPIEnv
upienv :: UPIEnv
upienv :: UBlockState -> UPIEnv
upienv, UPIState
upistate :: UPIState
upistate :: UBlockState -> UPIState
upistate} = do
    (Maybe UProp
anOptionalUpdateProposal, [Vote]
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.
    VKey
aBlockIssuer <-
      forall (m :: * -> *) a. MonadGen m => m a -> m a
Gen.prune forall a b. (a -> b) -> a -> b
$
        -- Pick a delegate from the delegation map
        forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element forall a b. (a -> b) -> a -> b
$
          forall a b. Bimap a b -> [b]
Bimap.elems (UPIEnv -> Bimap VKeyGenesis VKey
Update.delegationMap UPIEnv
upienv)

    ProtVer
aBlockVersion <-
      UPIEnv -> UPIState -> Gen ProtVer
Update.protocolVersionEndorsementGen UPIEnv
upienv UPIState
upistate

    VKey -> ProtVer -> Slot -> Maybe UProp -> [Vote] -> UBlock
UBlock
      forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (f :: * -> *) a. Applicative f => a -> f a
pure VKey
aBlockIssuer
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure ProtVer
aBlockVersion
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity Slot
nextSlotGen
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe UProp
anOptionalUpdateProposal
      forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (f :: * -> *) a. Applicative f => a -> f a
pure [Vote]
aListOfVotes
    where
      nextSlotGen :: GenT Identity Slot
nextSlotGen =
        Word64 -> Slot
incSlot
          forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (m :: * -> *) a. MonadGen m => [(Int, m a)] -> m a
Gen.frequency
            [ (Int
5, forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (forall a. a -> a -> Range a
Range.constant Word64
1 Word64
10))
            , (Int
1, forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (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 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 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 forall a b. (a -> b) -> a -> b
$
  HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
    Trace UBLOCK
sample <- 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.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
75
      LabelName
"at least 20% of the proposals get confirmed"
      (Double
0.2 forall a. Ord a => a -> a -> Bool
<= Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
75
      LabelName
"at least 30% of the proposals get unconfirmed"
      (Double
0.3 forall a. Ord a => a -> a -> Bool
<= Double
1 forall a. Num a => a -> a -> a
- (Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample))

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
75
      LabelName
"at least 2% of the proposals get voted in the same block "
      (Double
0.02 forall a. Ord a => a -> a -> Bool
<= forall a b. (Integral a, Num b) => a -> b
fromIntegral (Trace UBLOCK -> Int
numberOfVotesForBlockProposal Trace UBLOCK
sample) forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
75
      LabelName
"at least 30% of blocks contain no votes"
      (Double
0.3 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UBLOCK -> Int
numberOfBlocksWithoutVotes Trace UBLOCK
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.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
70
      LabelName
"at least 10% of blocks contain votes"
      (Double
0.1 forall a. Ord a => a -> a -> Bool
<= Double
1 forall a. Num a => a -> a -> a
- forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UBLOCK -> Int
numberOfBlocksWithoutVotes Trace UBLOCK
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.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
75
      LabelName
"at least 70% of the blocks contain no update proposals"
      (Double
0.7 forall a. Ord a => a -> a -> Bool
<= forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UBLOCK -> Int
numberOfBlocksWithoutUpdateProposals Trace UBLOCK
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
75
      LabelName
"at least 10% of the blocks contain an update proposals"
      (Double
0.1 forall a. Ord a => a -> a -> Bool
<= Double
1 forall a. Num a => a -> a -> a
- forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UBLOCK -> Int
numberOfBlocksWithoutUpdateProposals Trace UBLOCK
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.
    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
60
      LabelName
"at least 10% of the proposals get enough endorsements"
      (Double
0.1 forall a. Ord a => a -> a -> Bool
<= Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)

    forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
80
      LabelName
"at least 5% of the proposals get enough endorsements"
      (Double
0.05 forall a. Ord a => a -> a -> Bool
<= Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)

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

totalProposals :: Trace UBLOCK -> Double
totalProposals :: Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample =
  forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UBLOCK
sample
    forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UBlock -> Maybe UProp
optionalUpdateProposal
    forall a b. a -> (a -> b) -> b
& forall a. [Maybe a] -> [a]
catMaybes
    forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UProp -> UpId
Update._upId
    forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) a. Foldable t => t a -> Int
length
    forall a b. a -> (a -> b) -> b
& 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 =
  forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UBLOCK
sample
    forall a b. a -> (a -> b) -> b
& forall a. (a -> Bool) -> [a] -> [a]
filter UBlock -> Bool
voteForBlockProposal
    forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) a. Foldable t => t a -> Int
length
  where
    voteForBlockProposal :: UBlock -> Bool
    voteForBlockProposal :: UBlock -> Bool
voteForBlockProposal UBlock {Maybe UProp
optionalUpdateProposal :: Maybe UProp
optionalUpdateProposal :: UBlock -> Maybe UProp
optionalUpdateProposal, [Vote]
votes :: [Vote]
votes :: UBlock -> [Vote]
votes} =
      case Maybe UProp
optionalUpdateProposal of
        Maybe UProp
Nothing ->
          Bool
False
        Just UProp
updateProposal ->
          UProp -> UpId
Update._upId UProp
updateProposal forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` (Vote -> UpId
Update._vPropId 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 =
  forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace UBLOCK
sample
    forall a b. a -> (a -> b) -> b
& forall a. (a -> Bool) -> [a] -> [a]
filter (forall (t :: * -> *) a. Foldable t => t a -> Bool
null forall b c a. (b -> c) -> (a -> b) -> a -> c
. UBlock -> [Vote]
votes)
    forall a b. a -> (a -> b) -> b
& forall (t :: * -> *) a. Foldable t => t a -> Int
length

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

proposalsScheduledForAdoption :: Trace UBLOCK -> Double
proposalsScheduledForAdoption :: Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample =
  forall s. TraceOrder -> Trace s -> [State s]
traceStates TraceOrder
OldestFirst Trace UBLOCK
sample
    forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap UBlockState -> UPIState
upistate
    -- We concat all the future adoptions together
    forall a b. a -> (a -> b) -> b
& 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
    forall a b. a -> (a -> b) -> b
& forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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.
    forall a b. a -> (a -> b) -> b
& forall a. Ord a => [a] -> Set a
Set.fromList
    forall a b. a -> (a -> b) -> b
& forall a. Set a -> Int
Set.size
    forall a b. a -> (a -> b) -> b
& 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
  Trace UBLOCK
sample <- forall s. HasTrace s => BaseEnv s -> Word64 -> IO (Trace s)
randomTraceOfSize @UBLOCK () Word64
maxTraceSize
  let (Slot
_slot, Bimap VKeyGenesis VKey
_dms, BlockCount
k, Word8
numberOfGenesisKeys) = forall s. Trace s -> Environment s
_traceEnv Trace UBLOCK
sample
  forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_
    forall a. Show a => a -> IO ()
print
    [ [Char]
"k = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show BlockCount
k
    , [Char]
"genesis keys = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Word8
numberOfGenesisKeys
    , [Char]
"trace length = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall s. Trace s -> Int
traceLength Trace UBLOCK
sample)
    , [Char]
"proposals = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)
    , [Char]
"confirmed proposals = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample)
    , [Char]
"scheduled proposals = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample)
    , [Char]
"total number of votes = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Int
numberOfVotes Trace UBLOCK
sample)
    , [Char]
"blocks without votes = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Int
numberOfBlocksWithoutVotes Trace UBLOCK
sample)
    , [Char]
"votes for block proposal in same block = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Int
numberOfVotesForBlockProposal Trace UBLOCK
sample)
    , [Char]
"ratio of votes for block proposal in same block = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall a b. (Integral a, Num b) => a -> b
fromIntegral (Trace UBLOCK -> Int
numberOfVotesForBlockProposal Trace UBLOCK
sample) forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)
    , [Char]
"proposals scheduled for adoption = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample)
    , [Char]
"confirmed / total proposals = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)
    , [Char]
"scheduled / total proposals = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)
    , [Char]
"scheduled / confirmed proposals = "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample)
    ]

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