{-# 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
    Trace UPIREG
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)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UPIREG -> Int
increaseMajor Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio Trace UPIREG -> Int
increaseMinor Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
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).
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
50
      LabelName
"the distribution of the proposal issuers is roughly fair"
      ( [Double] -> Double
forall {t :: * -> *} {a}. (Foldable t, Num a, Ord a) => t a -> a
safeMaximum (Trace UPIREG -> [Double]
issuersDeviationsWrtUniformDistribution Trace UPIREG
sample)
          Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Trace UPIREG -> Double
expectedNumberOfUpdateProposalsPerKey Trace UPIREG
sample Double -> Double -> Double
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.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxBkSz Change
Decreases) Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxBkSz Change
Increases) Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxBkSz Change
RemainsTheSame) Trace UPIREG
sample)

    --------------------------------------------------------------------------------
    -- Maximum header-size checks
    --------------------------------------------------------------------------------
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxHdrSz Change
Decreases) Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxHdrSz Change
Increases) Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxHdrSz Change
RemainsTheSame) Trace UPIREG
sample)

    --------------------------------------------------------------------------------
    -- Maximum transaction-size checks
    --------------------------------------------------------------------------------
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxTxSz Change
Decreases) Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxTxSz Change
Increases) Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxTxSz Change
RemainsTheSame) Trace UPIREG
sample)

    --------------------------------------------------------------------------------
    -- Maximum proposal-size checks
    --------------------------------------------------------------------------------
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxPropSz Change
Decreases) Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
forall v. Ord v => (PParams -> v) -> Change -> Trace UPIREG -> Int
wrtCurrentProtocolParameters PParams -> Natural
Update._maxPropSz Change
Increases) Trace UPIREG
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= (Trace UPIREG -> Int) -> Trace UPIREG -> Double
forall a s. Integral a => (Trace s -> a) -> Trace s -> Double
ratio ((PParams -> Natural) -> Change -> Trace UPIREG -> Int
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
        [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 Environment UBLOCK
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 (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.
        UBlockState -> F (Clause UBLOCK 'Initial) UBlockState
forall a. a -> F (Clause UBLOCK 'Initial) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          UBlockState
            { upienv :: UPIEnv
upienv = UPIEnv
Environment UBLOCK
env
            , upistate :: UPIState
upistate =
                ( (ProtVer
pv, PParams
pps {Update._upTtl = SlotCount $ slotsPerEpoch k `div` 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 :: UBlockState -> UPIEnv
upienv :: UPIEnv
upienv, UPIState
upistate :: UBlockState -> UPIState
upistate :: UPIState
upistate}, Signal UBLOCK
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 (Slot
sn, Bimap VKeyGenesis VKey
dms, BlockCount
k, Word8
ngk) = UPIEnv
upienv
        Slot
sn Slot -> Slot -> Bool
forall a. Ord a => a -> a -> Bool
< UBlock -> Slot
slot Signal UBLOCK
UBlock
ublock Bool -> PredicateFailure UBLOCK -> Rule UBLOCK 'Transition ()
forall sts (ctx :: RuleType).
Bool -> PredicateFailure sts -> Rule sts ctx ()
?! PredicateFailure UBLOCK
UBlockPredicateFailure
NotIncreasingBlockSlot
        UPIState
upistateAfterRegistration <-
          case UBlock -> Maybe UProp
optionalUpdateProposal Signal UBLOCK
UBlock
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)
        UPIState
upistateAfterVoting <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIVOTES (RuleContext 'Transition UPIVOTES
 -> Rule UBLOCK 'Transition (State UPIVOTES))
-> RuleContext 'Transition UPIVOTES
-> Rule UBLOCK 'Transition (State UPIVOTES)
forall a b. (a -> b) -> a -> b
$ (Environment UPIVOTES, State UPIVOTES, Signal UPIVOTES)
-> TRC UPIVOTES
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UPIEnv
Environment UPIVOTES
upienv, UPIState
State UPIVOTES
upistateAfterRegistration, UBlock -> [Vote]
votes Signal UBLOCK
UBlock
ublock)
        UPIState
upistateAfterEndorsement <-
          forall sub super (rtype :: RuleType).
Embed sub super =>
RuleContext rtype sub -> Rule super rtype (State sub)
trans @UPIEND (RuleContext 'Transition UPIEND
 -> Rule UBLOCK 'Transition (State UPIEND))
-> RuleContext 'Transition UPIEND
-> Rule UBLOCK 'Transition (State UPIEND)
forall a b. (a -> b) -> a -> b
$ (Environment UPIEND, State UPIEND, Signal UPIEND) -> TRC UPIEND
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UPIEnv
Environment UPIEND
upienv, UPIState
State UPIEND
upistateAfterVoting, (UBlock -> ProtVer
blockVersion Signal UBLOCK
UBlock
ublock, UBlock -> VKey
issuer Signal UBLOCK
UBlock
ublock))
        UBlockState -> F (Clause UBLOCK 'Transition) UBlockState
forall a. a -> F (Clause UBLOCK 'Transition) a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
          UBlockState
            { upienv :: UPIEnv
upienv = (UBlock -> Slot
slot Signal UBLOCK
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 -> 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
      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.
      UPIEnv -> GenT Identity UPIEnv
forall a. a -> GenT Identity a
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 :: UBlockState -> UPIEnv
upienv :: UPIEnv
upienv, UPIState
upistate :: UBlockState -> UPIState
upistate :: 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 <-
      GenT Identity VKey -> GenT Identity VKey
forall (m :: * -> *) a. MonadGen m => m a -> m a
Gen.prune (GenT Identity VKey -> GenT Identity VKey)
-> GenT Identity VKey -> GenT Identity VKey
forall a b. (a -> b) -> a -> b
$
        -- Pick a delegate from the delegation map
        [VKey] -> GenT Identity VKey
forall (f :: * -> *) (m :: * -> *) a.
(Foldable f, MonadGen m) =>
f a -> m a
Gen.element ([VKey] -> GenT Identity VKey) -> [VKey] -> GenT Identity VKey
forall a b. (a -> b) -> a -> b
$
          Bimap VKeyGenesis VKey -> [VKey]
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
      (VKey -> ProtVer -> Slot -> Maybe UProp -> [Vote] -> UBlock)
-> GenT Identity VKey
-> GenT
     Identity (ProtVer -> Slot -> Maybe UProp -> [Vote] -> UBlock)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> VKey -> GenT Identity VKey
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure VKey
aBlockIssuer
      GenT Identity (ProtVer -> Slot -> Maybe UProp -> [Vote] -> UBlock)
-> Gen ProtVer
-> GenT Identity (Slot -> Maybe UProp -> [Vote] -> UBlock)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> ProtVer -> Gen ProtVer
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProtVer
aBlockVersion
      GenT Identity (Slot -> Maybe UProp -> [Vote] -> UBlock)
-> GenT Identity Slot
-> GenT Identity (Maybe UProp -> [Vote] -> UBlock)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> GenT Identity Slot
nextSlotGen
      GenT Identity (Maybe UProp -> [Vote] -> UBlock)
-> GenT Identity (Maybe UProp) -> GenT Identity ([Vote] -> UBlock)
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe UProp -> GenT Identity (Maybe UProp)
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe UProp
anOptionalUpdateProposal
      GenT Identity ([Vote] -> UBlock)
-> GenT Identity [Vote] -> GenT Identity UBlock
forall a b.
GenT Identity (a -> b) -> GenT Identity a -> GenT Identity b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> [Vote] -> GenT Identity [Vote]
forall a. a -> GenT Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Vote]
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. 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
    Trace UBLOCK
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.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
forall (m :: * -> *).
(MonadTest m, HasCallStack) =>
CoverPercentage -> LabelName -> Bool -> m ()
cover
      CoverPercentage
75
      LabelName
"at least 20% of the proposals get confirmed"
      (Double
0.2 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)

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

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Trace UBLOCK -> Int
numberOfVotesForBlockProposal Trace UBLOCK
sample) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)

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

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
1 Double -> Double -> Double
forall a. Num a => a -> a -> a
- (Trace UBLOCK -> Int) -> Trace UBLOCK -> Double
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.
    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)

    CoverPercentage -> LabelName -> Bool -> PropertyT IO ()
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 Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample Double -> Double -> Double
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 =
  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
  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) = Trace UBLOCK -> Environment UBLOCK
forall s. Trace s -> Environment s
_traceEnv Trace UBLOCK
sample
  ([Char] -> IO ()) -> [[Char]] -> IO ()
forall (t :: * -> *) (f :: * -> *) a b.
(Foldable t, Applicative f) =>
(a -> f b) -> t a -> f ()
traverse_
    [Char] -> IO ()
forall a. Show a => a -> IO ()
print
    [ [Char]
"k = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ BlockCount -> [Char]
forall a. Show a => a -> [Char]
show BlockCount
k
    , [Char]
"genesis keys = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Word8 -> [Char]
forall a. Show a => a -> [Char]
show Word8
numberOfGenesisKeys
    , [Char]
"trace length = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Int
forall s. Trace s -> Int
traceLength Trace UBLOCK
sample)
    , [Char]
"proposals = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)
    , [Char]
"confirmed proposals = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample)
    , [Char]
"scheduled proposals = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample)
    , [Char]
"total number of votes = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Int
numberOfVotes Trace UBLOCK
sample)
    , [Char]
"blocks without votes = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Int
numberOfBlocksWithoutVotes Trace UBLOCK
sample)
    , [Char]
"votes for block proposal in same block = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Int -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Int
numberOfVotesForBlockProposal Trace UBLOCK
sample)
    , [Char]
"ratio of votes for block proposal in same block = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Trace UBLOCK -> Int
numberOfVotesForBlockProposal Trace UBLOCK
sample) Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)
    , [Char]
"proposals scheduled for adoption = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample)
    , [Char]
"confirmed / total proposals = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
confirmedProposals Trace UBLOCK
sample Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)
    , [Char]
"scheduled / total proposals = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/ Trace UBLOCK -> Double
totalProposals Trace UBLOCK
sample)
    , [Char]
"scheduled / confirmed proposals = "
        [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Double -> [Char]
forall a. Show a => a -> [Char]
show (Trace UBLOCK -> Double
proposalsScheduledForAdoption Trace UBLOCK
sample Double -> Double -> Double
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 =
  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