Skip to content

Commit 52d8b21

Browse files
dnadalesdnadales
authoredJul 19, 2019
Add update payload to chain traces (#649)
- Lower the coverage threshold for "at least 10% of the update proposals do not change the maximum transaction-size" - Increase the trace length to 300 in the `onlyValidSignalsAreGenerated @CHAIN` propoerty - Fix the update generator. It allowed to produce a maximum transaction size that was bigger than the current maximum block size. - Guard the `newMaxBkSize - 1` against underflows - Lower 10% the bounds for the "at least 10% of the proposals get enough endorsements" coverage check. - Generate `CHAIN` delegation payload only in 30% of the cases. - Tweak the coverage metrics to account for the fact that we do not want to decrease certain protocol parameter values to prevent the signal production (blocks, transactions, etc) from stopping. - Set a memory limit for the tests in `cs-blockchain` - Fix the abstract size test where the number of characters in the system tags were not being counted. - Fix arithmetic underflow when checking validity of proposed script version. - Factor out functions for generating update proposal and votes, and endorsements. See `updateProposalAndVotesGen` and `protocolVersionEndorsementGen`. - Ignore `stack` lock file. - Limit the line width to 80. 100 characters is not suitable for working with two vertical panes on a laptop, with a font size that is legible for people with less than optimal vision (like @dnadales :) ).
·
vector-map-1.1.0.01.16.0
1 parent dda7ebf commit 52d8b21

File tree

13 files changed

+380
-222
lines changed

13 files changed

+380
-222
lines changed
 

‎.editorconfig

+3-2
Original file line numberDiff line numberDiff line change
@@ -7,8 +7,9 @@ end_of_line = lf
77
charset = utf-8
88
trim_trailing_whitespace = true
99
insert_final_newline = true
10-
max_line_length = 100
10+
# See: https://github.com/input-output-hk/cardano-wallet/wiki/Coding-Standards
11+
max_line_length = 80
1112

1213
[*.hs]
1314
indent_size = 2
14-
max_line_length = 100
15+
max_line_length = 80

‎.gitignore

+1
Original file line numberDiff line numberDiff line change
@@ -31,6 +31,7 @@
3131
*~
3232
dist-newstyle/
3333
cabal.project.local
34+
stack.yaml.lock
3435

3536
# Editors
3637
TAGS

‎byron/chain/executable-spec/cs-blockchain.cabal

+3
Original file line numberDiff line numberDiff line change
@@ -76,5 +76,8 @@ test-suite chain-rules-test
7676
-Wincomplete-record-updates
7777
-Wincomplete-uni-patterns
7878
-Wredundant-constraints
79+
-- See `cs-ledger.cabal` for an explanation of the
80+
-- options below.
81+
"-with-rtsopts=-K4m -M300m"
7982
if (!flag(development))
8083
ghc-options: -Werror

‎byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Block.hs

+15-15
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,22 @@
1-
{-# LANGUAGE DeriveGeneric #-}
2-
{-# LANGUAGE OverloadedLists #-}
3-
{-# LANGUAGE TemplateHaskell #-}
1+
{-# LANGUAGE DeriveGeneric #-}
2+
{-# LANGUAGE OverloadedLists #-}
3+
{-# LANGUAGE TemplateHaskell #-}
44

55
module Cardano.Spec.Chain.STS.Block where
66

7-
import Control.Lens ((^.), makeLenses, view)
7+
import Control.Lens (makeLenses, view, (^.))
8+
import Control.State.Transition.Generator
9+
import Data.AbstractSize
810
import qualified Data.Hashable as H
9-
import Data.AbstractSize
1011
import qualified Data.Map.Strict as Map
11-
import Data.Sequence ((<|))
12-
import Data.Typeable (typeOf)
13-
import Numeric.Natural (Natural)
14-
import GHC.Generics (Generic)
15-
import Control.State.Transition.Generator
16-
import Ledger.Core (Hash(Hash), VKey, Slot, Sig)
17-
import Ledger.Delegation
18-
import Ledger.Update (STag, ProtVer, UProp, Vote)
19-
import Ledger.UTxO (TxWits, TxIn, TxOut, Wit)
12+
import Data.Sequence ((<|))
13+
import Data.Typeable (typeOf)
14+
import GHC.Generics (Generic)
15+
import Ledger.Core (Hash (Hash), Sig, Slot, VKey)
16+
import Ledger.Delegation
17+
import Ledger.Update (ProtVer, STag, UProp, Vote)
18+
import Ledger.UTxO (TxIn, TxOut, TxWits, Wit)
19+
import Numeric.Natural (Natural)
2020

2121
data BlockHeader
2222
= MkBlockHeader
@@ -39,7 +39,7 @@ data BlockHeader
3939
-- TODO: BlockVersion – the protocol (block) version that created the block
4040

4141
-- TODO: SoftwareVersion – the software version that created the block
42-
} deriving (Generic, Show)
42+
} deriving (Eq, Generic, Show)
4343

4444
makeLenses ''BlockHeader
4545

‎byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/BHead.hs

+4-2
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ module Cardano.Spec.Chain.STS.Rule.BHead where
66

77
import Control.Lens ((^.), _1)
88
import Data.Bimap (Bimap)
9+
import Numeric.Natural
910

1011
import Control.State.Transition
1112
import Ledger.Core
@@ -31,7 +32,7 @@ instance STS BHEAD where
3132

3233
data PredicateFailure BHEAD
3334
= HashesDontMatch -- TODO: Add fields so that users know the two hashes that don't match
34-
| HeaderSizeTooBig -- TODO: Add more information here as well.
35+
| HeaderSizeTooBig BlockHeader Natural (Threshold Natural)
3536
| SlotDidNotIncrease
3637
-- ^ The block header slot number did not increase w.r.t the last seen slot
3738
| SlotInTheFuture
@@ -47,7 +48,8 @@ instance STS BHEAD where
4748
TRC ((_, sLast, k), us, bh) <- judgmentContext
4849
us' <- trans @EPOCH $ TRC ((sEpoch sLast k, k), us, bh ^. bhSlot)
4950
let sMax = snd (us' ^. _1) ^. maxHdrSz
50-
bHeaderSize bh <= sMax ?! HeaderSizeTooBig
51+
bHeaderSize bh <= sMax
52+
?! HeaderSizeTooBig bh (bHeaderSize bh) (Threshold sMax)
5153
return $! us'
5254
]
5355

‎byron/chain/executable-spec/src/Cardano/Spec/Chain/STS/Rule/Chain.hs

+92-31
Original file line numberDiff line numberDiff line change
@@ -18,6 +18,7 @@ import qualified Data.Map as Map
1818
import Data.Sequence (Seq)
1919
import Data.Set (Set)
2020
import qualified Data.Set as Set
21+
import Data.Word (Word8)
2122
import Hedgehog (Gen)
2223
import qualified Hedgehog.Gen as Gen
2324
import qualified Hedgehog.Range as Range
@@ -31,12 +32,13 @@ import Ledger.Core
3132
import qualified Ledger.Core.Generators as CoreGen
3233
import Ledger.Delegation
3334
import Ledger.Update hiding (delegationMap)
35+
import qualified Ledger.Update as Update
3436
import Ledger.UTxO (UTxO)
3537

3638
import Cardano.Spec.Chain.STS.Block
3739
import Cardano.Spec.Chain.STS.Rule.BBody
3840
import Cardano.Spec.Chain.STS.Rule.BHead
39-
import Cardano.Spec.Chain.STS.Rule.Epoch (sEpoch)
41+
import Cardano.Spec.Chain.STS.Rule.Epoch (EPOCH, sEpoch)
4042
import Cardano.Spec.Chain.STS.Rule.Pbft
4143
import qualified Cardano.Spec.Chain.STS.Rule.SigCnt as SigCntGen
4244

@@ -189,45 +191,110 @@ instance HasTrace CHAIN where
189191
-- current slot to a sufficiently large value.
190192
gCurrentSlot = Slot <$> Gen.integral (Range.constant 32768 2147483648)
191193

192-
sigGen _ = sigGenChain GenDelegation GenUTxO Nothing
194+
sigGen _ = sigGenChain GenDelegation GenUTxO GenUpdate Nothing
193195

194196
data ShouldGenDelegation = GenDelegation | NoGenDelegation
195197

196198
data ShouldGenUTxO = GenUTxO | NoGenUTxO
197199

200+
data ShouldGenUpdate = GenUpdate | NoGenUpdate
201+
198202
sigGenChain
199203
:: ShouldGenDelegation
200204
-> ShouldGenUTxO
205+
-> ShouldGenUpdate
201206
-> Maybe (PredicateFailure CHAIN)
202207
-> Environment CHAIN
203208
-> State CHAIN
204209
-> Gen (Signal CHAIN)
205-
sigGenChain shouldGenDelegation shouldGenUTxO _ (_sNow, utxo0, ads, pps, k) (Slot s, sgs, h, utxo, ds, _us)
210+
sigGenChain
211+
shouldGenDelegation
212+
shouldGenUTxO
213+
shouldGenUpdate
214+
_
215+
(_sNow, utxo0, ads, _pps, k)
216+
(Slot s, sgs, h, utxo, ds, us)
206217
= do
218+
-- We'd expect the slot increment to be close to 1, even for large Gen's
219+
-- size numbers.
220+
nextSlot <- Slot . (s +) <$> Gen.integral (Range.exponential 1 10)
221+
222+
-- We need to generate delegation, update proposals, votes, and transactions
223+
-- after a potential update in the protocol parameters (which is triggered
224+
-- only at epoch boundaries). Otherwise the generators will use a state that
225+
-- won't hold when the rules that correspond to these generators are
226+
-- applied. For instance, the fees might change, which will render the
227+
-- transaction as invalid.
228+
--
229+
let (us', _) = applySTSIndifferently @EPOCH $ TRC ( (sEpoch (Slot s) k, k)
230+
, us
231+
, nextSlot
232+
)
233+
234+
pps' = protocolParameters us'
235+
236+
upienv =
237+
( Slot s
238+
, _dIStateDelegationMap ds
239+
, k
240+
, toNumberOfGenesisKeys $ Set.size ads
241+
)
242+
243+
-- TODO: we might need to make the number of genesis keys a newtype, and
244+
-- provide this function in the same module where this newtype is
245+
-- defined.
246+
toNumberOfGenesisKeys n
247+
| fromIntegral (maxBound :: Word8) < n =
248+
error $ "sigGenChain: too many genesis keys: " ++ show n
249+
| otherwise = fromIntegral n
250+
251+
aBlockVersion <-
252+
Update.protocolVersionEndorsementGen upienv us'
253+
207254
-- Here we do not want to shrink the issuer, since @Gen.element@ shrinks
208255
-- towards the first element of the list, which in this case won't provide
209256
-- us with better shrinks.
210-
vkI <- SigCntGen.issuer (pps, ds ^. dmsL, k) sgs
211-
nextSlot <- gNextSlot
212-
213-
delegationPayload <- case shouldGenDelegation of
214-
GenDelegation ->
215-
let dsEnv = DSEnv
216-
{ _dSEnvAllowedDelegators = ads
217-
, _dSEnvEpoch = sEpoch nextSlot k
218-
, _dSEnvSlot = nextSlot
219-
, _dSEnvK = k
220-
}
221-
in
222-
dcertsGen dsEnv ds
223-
NoGenDelegation -> pure []
224-
225-
utxoPayload <- case shouldGenUTxO of
226-
GenUTxO -> sigGen @UTXOWS Nothing utxoEnv utxo
227-
NoGenUTxO -> pure []
257+
vkI <- SigCntGen.issuer (pps', ds ^. dmsL, k) sgs
258+
259+
delegationPayload <-
260+
case shouldGenDelegation of
261+
GenDelegation ->
262+
-- In practice there won't be a delegation payload in every block, so we
263+
-- make this payload sparse.
264+
--
265+
-- NOTE: We arbitrarily chose to generate delegation payload in 30% of
266+
-- the cases. We could make this configurable.
267+
Gen.frequency
268+
[ (7, pure [])
269+
, (3,
270+
let dsEnv =
271+
DSEnv
272+
{ _dSEnvAllowedDelegators = ads
273+
, _dSEnvEpoch = sEpoch nextSlot k
274+
, _dSEnvSlot = nextSlot
275+
, _dSEnvK = k
276+
}
277+
in dcertsGen dsEnv ds
278+
)
279+
]
280+
NoGenDelegation -> pure []
281+
282+
utxoPayload <-
283+
case shouldGenUTxO of
284+
GenUTxO ->
285+
let utxoEnv = UTxOEnv utxo0 pps' in
286+
sigGen @UTXOWS Nothing utxoEnv utxo
287+
NoGenUTxO -> pure []
288+
289+
(anOptionalUpdateProposal, aListOfVotes) <-
290+
case shouldGenUpdate of
291+
GenUpdate ->
292+
Update.updateProposalAndVotesGen upienv us'
293+
NoGenUpdate ->
294+
pure (Nothing, [])
228295

229296
let
230-
dummySig = Sig genesisHash (owner vkI)
297+
dummySig = Sig genesisHash (owner vkI)
231298
unsignedHeader = MkBlockHeader
232299
h
233300
nextSlot
@@ -244,14 +311,8 @@ sigGenChain shouldGenDelegation shouldGenUTxO _ (_sNow, utxo0, ads, pps, k) (Slo
244311
BlockBody
245312
delegationPayload
246313
utxoPayload
247-
Nothing -- Update proposal
248-
[] -- Votes on update proposals
249-
(ProtVer 0 0 0)
314+
anOptionalUpdateProposal
315+
aListOfVotes
316+
aBlockVersion
250317

251318
pure $ Block signedHeader bb
252-
where
253-
-- We'd expect the slot increment to be close to 1, even for large
254-
-- Gen's size numbers.
255-
gNextSlot = Slot . (s +) <$> Gen.integral (Range.exponential 1 10)
256-
257-
utxoEnv = UTxOEnv {utxo0, pps}

‎byron/chain/executable-spec/test/Cardano/AbstractSize/Properties.hs

+9-6
Original file line numberDiff line numberDiff line change
@@ -17,14 +17,14 @@ import Data.Typeable (TypeRep, Typeable, typeOf)
1717
import Data.Word (Word64)
1818
import Numeric.Natural (Natural)
1919

20-
import Hedgehog (MonadTest, Property, forAll, property, withTests, (===))
20+
import Hedgehog (MonadTest, Property, diff, forAll, property, withTests, (===))
2121
import Test.Tasty.Hedgehog
2222

2323
import Control.State.Transition.Generator (trace)
2424
import Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)
2525
import Ledger.Core hiding ((<|))
2626
import Ledger.Delegation (DCert)
27-
import Ledger.Update (ProtVer (..), STag, UProp (..), Vote)
27+
import Ledger.Update (ProtVer (..), UProp (..), Vote)
2828
import Ledger.UTxO
2929

3030
import Cardano.Spec.Chain.STS.Block (Block (..), BlockBody (..), BlockHeader (..))
@@ -136,10 +136,13 @@ propMultipleOfSizesBlock b =
136136
abstractSize (mkCost @TxWits) b === length (_bUtxo body_)
137137
abstractSize (mkCost @Vote) b === length (_bUpdVotes body_)
138138
abstractSize (mkCost @UProp) b === length (maybeToList (_bUpdProp body_))
139-
abstractSize (mkCost @STag) b
140-
=== case _bUpdProp body_ of
141-
Just uprop -> Set.size (_upSTags uprop)
142-
Nothing -> 0
139+
-- A STag is a string, so we need to make sure that all the characters are
140+
-- accounted for in the size computation. We cannot use equality, since
141+
-- characters might appear in other parts of the block.
142+
diff
143+
(maybe 0 (sum . fmap length . Set.toList . _upSTags) (_bUpdProp body_))
144+
(<=)
145+
(abstractSize (mkCost @Char) b)
143146

144147
-- BlockHeader appears only once
145148
abstractSize (mkCost @BlockHeader) b === 1

‎byron/chain/executable-spec/test/Cardano/Spec/Chain/STS/Properties.hs

+10-4
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,9 @@ import Ledger.Core (BlockCount (BlockCount))
2323
slotsIncrease :: Property
2424
slotsIncrease = property $ do
2525
let (maxTraceLength, step) = (1000, 100)
26-
tr <- forAll $ traceSigGen (Maximum maxTraceLength) (sigGenChain NoGenDelegation NoGenUTxO)
26+
tr <- forAll $ traceSigGen
27+
(Maximum maxTraceLength)
28+
(sigGenChain NoGenDelegation NoGenUTxO NoGenUpdate)
2729
classifyTraceLength tr maxTraceLength step
2830
slotsIncreaseInTrace tr
2931

@@ -36,7 +38,9 @@ blockIssuersAreDelegates :: Property
3638
blockIssuersAreDelegates =
3739
withTests 200 $ property $ do
3840
let (maxTraceLength, step) = (1000, 100)
39-
tr <- forAll $ traceSigGen (Maximum maxTraceLength) (sigGenChain GenDelegation NoGenUTxO)
41+
tr <- forAll $ traceSigGen
42+
(Maximum maxTraceLength)
43+
(sigGenChain GenDelegation NoGenUTxO GenUpdate)
4044
classifyTraceLength tr maxTraceLength step
4145
checkBlockIssuersAreDelegates tr
4246
where
@@ -55,12 +59,14 @@ blockIssuersAreDelegates =
5559

5660
onlyValidSignalsAreGenerated :: Property
5761
onlyValidSignalsAreGenerated =
58-
withTests 300 $ TransitionGenerator.onlyValidSignalsAreGenerated @CHAIN 100
62+
withTests 200 $ TransitionGenerator.onlyValidSignalsAreGenerated @CHAIN 300
5963

6064
signersListIsBoundedByK :: Property
6165
signersListIsBoundedByK = property $ do
6266
let maxTraceLength = 1000
63-
tr <- forAll $ traceSigGen (Maximum maxTraceLength) (sigGenChain GenDelegation NoGenUTxO)
67+
tr <- forAll $ traceSigGen
68+
(Maximum maxTraceLength)
69+
(sigGenChain GenDelegation NoGenUTxO GenUpdate)
6470
signersListIsBoundedByKInTrace tr
6571
where
6672
signersListIsBoundedByKInTrace :: MonadTest m => Trace CHAIN -> m ()

‎byron/ledger/executable-spec/cs-ledger.cabal

+1-1
Original file line numberDiff line numberDiff line change
@@ -114,7 +114,7 @@ test-suite ledger-rules-test
114114
-- We set a bound here so that we're alerted of potential space
115115
-- leaks in our generators (or test) code.
116116
--
117-
-- The 4 megabytes stack bound and 50 megabytes heap bound were
117+
-- The 4 megabytes stack bound and 150 megabytes heap bound were
118118
-- determined ad-hoc.
119119
"-with-rtsopts=-K4m -M150m"
120120
if (!flag(development))

‎byron/ledger/executable-spec/src/Ledger/Update.hs

+168-40
Original file line numberDiff line numberDiff line change
@@ -33,7 +33,7 @@ import Data.Ix (inRange)
3333
import Data.List (notElem, sortOn)
3434
import Data.Map.Strict (Map)
3535
import qualified Data.Map.Strict as Map
36-
import Data.Maybe (fromMaybe)
36+
import Data.Maybe (catMaybes, fromMaybe)
3737
import Data.Ord (Down (Down))
3838
import Data.Set (Set, union, (\\))
3939
import qualified Data.Set as Set
@@ -49,13 +49,13 @@ import Control.State.Transition
4949
import Control.State.Transition.Generator (HasTrace, envGen, sigGen)
5050
import Data.AbstractSize (HasTypeReps)
5151

52-
import Ledger.Core (BlockCount (..), HasHash, Owner (Owner), Relation (..),
52+
import Ledger.Core (BlockCount (..), HasHash, Owner (Owner), Relation (..), Slot,
5353
SlotCount (..), VKey (VKey), VKeyGenesis (VKeyGenesis), dom, hash,
5454
minusSlotMaybe, skey, (*.), (-.), (∈), (∉), (⋪), (▷), (▷<=), (▷>=), (◁), (⨃))
5555
import qualified Ledger.Core as Core
5656
import qualified Ledger.Core.Generators as CoreGen
5757

58-
import Prelude hiding (min)
58+
import Prelude
5959

6060

6161
-- | Protocol parameters.
@@ -225,27 +225,57 @@ invertBijection
225225
a ==> b = not a || b
226226
infix 1 ==>
227227

228+
-- | Check whether a protocol version can follow the current protocol version.
228229
pvCanFollow
229230
:: ProtVer
231+
-- ^ Next protocol version
230232
-> ProtVer
233+
-- ^ Previous protocol version
231234
-> Bool
232-
pvCanFollow (ProtVer mjn min an) (ProtVer mjp mip ap)
233-
= (mjp, mip, ap) < (mjn, min, an)
235+
pvCanFollow (ProtVer mjn mn an) (ProtVer mjp mip ap)
236+
= (mjp, mip, ap) < (mjn, mn, an)
234237
&& (inRange (0,1) (mjn - mjp))
235-
&& ((mjp == mjn) ==> (mip +1 == min))
236-
&& ((mjp +1 == mjn) ==> (min == 0))
238+
&& ((mjp == mjn) ==> (mip + 1 == mn))
239+
&& ((mjp + 1 == mjn) ==> (mn == 0))
237240

238241
-- | Check whether an update proposal marks a valid update
239242
--
240-
-- TODO At the moment we don't check size in here - should we?
241-
canUpdate
243+
checkUpdateConstraints
242244
:: PParams
243245
-> UProp
244-
-> Bool
245-
canUpdate pps prop =
246-
(prop ^. upParams . maxBkSz <= 2 * pps ^. maxBkSz)
247-
&& (prop ^. upParams . maxBkSz > prop ^. upParams . maxTxSz)
248-
&& (inRange (0,1) $ prop ^. upParams . scriptVersion - pps ^. scriptVersion)
246+
-> [UpdateConstraintViolation]
247+
checkUpdateConstraints pps prop =
248+
catMaybes
249+
[ (prop ^. upParams . maxBkSz <=? 2 * pps ^. maxBkSz)
250+
`orError` BlockSizeTooLarge
251+
, (prop ^. upParams . maxTxSz + 1 <=? prop ^. upParams . maxBkSz)
252+
`orError` TransactionSizeTooLarge
253+
, (pps ^. scriptVersion <=? prop ^. upParams . scriptVersion)
254+
`orError` ScriptVersionTooSmall
255+
, (prop ^. upParams . scriptVersion <=? pps ^. scriptVersion + 1)
256+
`orError` ScriptVersionTooLarge
257+
]
258+
259+
(<=?) :: Ord a => a -> a -> Maybe (a, Threshold a)
260+
x <=? y = if x <= y then Nothing else Just (x, Threshold y)
261+
262+
infix 4 <=?
263+
264+
orError :: Maybe (a, b) -> (a -> b -> e) -> Maybe e
265+
orError mab ferr = uncurry ferr <$> mab
266+
267+
canUpdate :: PParams -> UProp -> Rule UPPVV ctx ()
268+
canUpdate pps prop = violations == [] ?! CannotUpdatePv violations
269+
where violations = checkUpdateConstraints pps prop
270+
271+
-- | Violations on the constraints of the allowed values for new protocol
272+
-- parameters.
273+
data UpdateConstraintViolation
274+
= BlockSizeTooLarge Natural (Threshold Natural)
275+
| TransactionSizeTooLarge Natural (Threshold Natural)
276+
| ScriptVersionTooLarge Natural (Threshold Natural)
277+
| ScriptVersionTooSmall Natural (Threshold Natural)
278+
deriving (Eq, Ord, Show)
249279

250280
svCanFollow
251281
:: Map ApName (ApVer, Core.Slot, Metadata)
@@ -303,7 +333,7 @@ instance STS UPPVV where
303333

304334
data PredicateFailure UPPVV
305335
= CannotFollowPv
306-
| CannotUpdatePv
336+
| CannotUpdatePv [UpdateConstraintViolation]
307337
| AlreadyProposedPv
308338
| InvalidSystemTags
309339
deriving (Eq, Show)
@@ -316,7 +346,7 @@ instance STS UPPVV where
316346
nv = up ^. upPV
317347
ppsn = up ^. upParams
318348
pvCanFollow nv pv ?! CannotFollowPv
319-
canUpdate pps up ?! CannotUpdatePv
349+
canUpdate pps up
320350
nv `notElem` (fst <$> Map.elems rpus) ?! AlreadyProposedPv
321351
all sTagValid (up ^. upSTags) ?! InvalidSystemTags
322352
return $! rpus ⨃ [(pid, (nv, ppsn))]
@@ -345,7 +375,7 @@ instance STS UPV where
345375
data PredicateFailure UPV
346376
= UPPVVFailure (PredicateFailure UPPVV)
347377
| UPSVVFailure (PredicateFailure UPSVV)
348-
| AVChangedInPVUpdate ApName ApVer
378+
| AVChangedInPVUpdate ApName ApVer (Maybe (ApVer, Slot, Metadata))
349379
| ParamsChangedInSVUpdate
350380
| PVChangedInSVUpdate
351381
deriving (Eq, Show)
@@ -359,7 +389,7 @@ instance STS UPV where
359389
) <- judgmentContext
360390
rpus' <- trans @UPPVV $ TRC ((pv, pps), rpus, up)
361391
let SwVer an av = up ^. upSwVer
362-
inMap an av (swVer <$> avs) ?! AVChangedInPVUpdate an av
392+
inMap an av (swVer <$> avs) ?! AVChangedInPVUpdate an av (Map.lookup an avs)
363393
pure $! (rpus', raus)
364394
, do
365395
TRC ( (pv, pps, avs)
@@ -717,8 +747,8 @@ emptyUPIState =
717747
initialPParams :: PParams
718748
initialPParams =
719749
PParams -- TODO: choose more sensible default values
720-
{ _maxBkSz = 1000 -- max sizes chosen as non-zero to allow progress
721-
, _maxHdrSz = 100
750+
{ _maxBkSz = 10000 -- max sizes chosen as non-zero to allow progress
751+
, _maxHdrSz = 1000
722752
, _maxTxSz = 500
723753
, _maxPropSz = 10
724754
, _bkSgnCntT = 0.22 -- As defined in the spec.
@@ -904,19 +934,19 @@ instance HasTrace UPIREG where
904934
-- is not part of the registered protocol-update proposals
905935
-- (@rpus@).
906936
nextAltVersion :: (Natural, Natural) -> ProtVer
907-
nextAltVersion (maj, min) = dom (range rpus)
937+
nextAltVersion (maj, mn) = dom (range rpus)
908938
& Set.filter protocolVersionEqualsMajMin
909939
& Set.map _pvAlt
910940
& Set.toDescList
911941
& nextVersion
912942
where
913943
protocolVersionEqualsMajMin :: ProtVer -> Bool
914944
protocolVersionEqualsMajMin pv' =
915-
_pvMaj pv' == maj && _pvMin pv' == min
945+
_pvMaj pv' == maj && _pvMin pv' == mn
916946

917947
nextVersion :: [Natural] -> ProtVer
918-
nextVersion [] = ProtVer maj min 0
919-
nextVersion (x:_) = ProtVer maj min (1 + x)
948+
nextVersion [] = ProtVer maj mn 0
949+
nextVersion (x:_) = ProtVer maj mn (1 + x)
920950

921951
-- Generate a software version update.
922952
swVerGen :: Gen SwVer
@@ -1017,20 +1047,32 @@ dmapGen ngk = Bimap.fromList . uncurry zip <$> vkgVkPairsGen
10171047
-- own modules.
10181048
ppsUpdateFrom :: PParams -> Gen PParams
10191049
ppsUpdateFrom pps = do
1050+
-- NOTE: we only generate small changes in the parameters to avoid leaving the
1051+
-- protocol parameters in a state that won't allow to produce any valid blocks
1052+
-- anymore (for instance if the maximum block size drops to a very small
1053+
-- value).
1054+
10201055
-- Determine the change in the block size: a decrement or an increment that
10211056
-- is no more than twice the current block maximum size.
10221057
--
10231058
-- We don't expect the maximum block size to change often, so we generate
10241059
-- more values around the current block size (@_maxBkSz@).
1025-
newMaxBkSize <- Gen.integral (Range.linearFrom _maxBkSz 1 (2 * _maxBkSz))
1026-
`increasingProbabilityAt`
1027-
(1, 2 * _maxBkSz)
1060+
newMaxBkSize <-
1061+
Gen.integral (Range.linearFrom
1062+
_maxBkSz
1063+
(_maxBkSz -? 100) -- Decrement value was determined ad-hoc
1064+
(2 * _maxBkSz)
1065+
)
1066+
`increasingProbabilityAt` (_maxBkSz -? 100, 2 * _maxBkSz)
10281067

10291068
-- Similarly, we don't expect the transaction size to be changed often, so we
10301069
-- also generate more values around the current maximum transaction size.
1031-
newMaxTxSize <- Gen.integral (Range.exponentialFrom _maxTxSz 0 (newMaxBkSize - 1))
1032-
`increasingProbabilityAt`
1033-
(0, newMaxBkSize - 1)
1070+
let minTxSzBound = _maxTxSz `min` newMaxBkSize -? 1
1071+
newMaxTxSize <-
1072+
Gen.integral (Range.exponential
1073+
(minTxSzBound -? 10) -- Decrement value determined ad-hoc
1074+
(newMaxBkSize -? 1)
1075+
)
10341076

10351077
PParams
10361078
<$> pure newMaxBkSize
@@ -1063,18 +1105,27 @@ ppsUpdateFrom pps = do
10631105

10641106
nextMaxHdrSzGen :: Gen Natural
10651107
nextMaxHdrSzGen =
1066-
Gen.integral (Range.exponentialFrom _maxHdrSz 0 (2 * _maxHdrSz))
1067-
`increasingProbabilityAt` (0, 2 * _maxHdrSz)
1108+
Gen.integral (Range.exponentialFrom
1109+
_maxHdrSz
1110+
(_maxHdrSz -? 10)
1111+
(2 * _maxHdrSz)
1112+
)
10681113

10691114
nextMaxPropSz :: Gen Natural
10701115
nextMaxPropSz =
1071-
Gen.integral (Range.exponentialFrom _maxPropSz 0 (2 * _maxPropSz))
1072-
`increasingProbabilityAt` (0, 2 * _maxPropSz)
1116+
Gen.integral (Range.exponentialFrom
1117+
_maxPropSz
1118+
(_maxPropSz -? 1)
1119+
(2 * _maxPropSz)
1120+
)
10731121

10741122
nextBkSgnCntT :: Gen Double
10751123
nextBkSgnCntT =
1076-
Gen.double (Range.exponentialFloatFrom _bkSgnCntT 0 1)
1077-
`increasingProbabilityAt` (0, 1)
1124+
Gen.double (Range.exponentialFloatFrom
1125+
_bkSgnCntT
1126+
(_bkSgnCntT - 0.01)
1127+
(_bkSgnCntT + 0.01)
1128+
)
10781129

10791130
nextUpTtl :: Gen SlotCount
10801131
nextUpTtl = SlotCount <$>
@@ -1113,6 +1164,9 @@ ppsUpdateFrom pps = do
11131164
Gen.integral (Range.exponentialFrom _factorB 0 10)
11141165
`increasingProbabilityAt` (0, 10)
11151166

1167+
(-?) :: Natural -> Natural -> Natural
1168+
n -? m = if n < m then 0 else n - m
1169+
11161170
-- | Generate values the given distribution in 90% of the cases, and values at
11171171
-- the bounds of the range in 10% of the cases.
11181172
--
@@ -1349,13 +1403,15 @@ instance STS UPIEND where
13491403
instance Embed UPEND UPIEND where
13501404
wrapFailed = UPENDFailure
13511405

1352-
-- | Generate a protocol version endorsement for a given key, or 'Nothing' if no stable and
1353-
-- confirmed protocol version update can be found.
1354-
protocolVersionEndorsementGen
1406+
-- | Given a list of protocol versions and keys endorsing those versions,
1407+
-- generate a protocol-version endorsement, or 'Nothing' if the list of
1408+
-- endorsements is empty. The version to be endorsed will be selected from those
1409+
-- versions that have the most endorsements.
1410+
pickHighlyEndorsedProtocolVersion
13551411
:: [(ProtVer, Set Core.VKeyGenesis)]
13561412
-- ^ Current set of endorsements
13571413
-> Gen (Maybe ProtVer)
1358-
protocolVersionEndorsementGen endorsementsList =
1414+
pickHighlyEndorsedProtocolVersion endorsementsList =
13591415
if null mostEndorsedProposals
13601416
then pure Nothing
13611417
else Just <$> Gen.element mostEndorsedProposals
@@ -1444,3 +1500,75 @@ instance STS UPIEC where
14441500

14451501
instance Embed PVBUMP UPIEC where
14461502
wrapFailed = PVBUMPFailure
1503+
1504+
-- | Generate an optional update-proposal and a list of votes, given an update
1505+
-- environment and state.
1506+
--
1507+
-- The update proposal and votes need to be generated at the same time, since
1508+
-- this allow us to generate update votes for update proposals issued in the
1509+
-- same block as the votes.
1510+
updateProposalAndVotesGen
1511+
:: UPIEnv
1512+
-> UPIState
1513+
-> Gen (Maybe UProp, [Vote])
1514+
updateProposalAndVotesGen upienv upistate = do
1515+
let rpus = registeredProtocolUpdateProposals upistate
1516+
if Set.null (dom rpus)
1517+
then generateUpdateProposalAndVotes
1518+
else Gen.frequency [ (5, generateOnlyVotes)
1519+
, (1, generateUpdateProposalAndVotes)
1520+
]
1521+
where
1522+
generateOnlyVotes = (Nothing,) <$> sigGen @UPIVOTES Nothing upienv upistate
1523+
generateUpdateProposalAndVotes = do
1524+
updateProposal <- sigGen @UPIREG Nothing upienv upistate
1525+
-- We want to have the possibility of generating votes for the proposal we
1526+
-- registered.
1527+
case applySTS @UPIREG (TRC (upienv, upistate, updateProposal)) of
1528+
Left _ ->
1529+
(Just updateProposal, )
1530+
<$> sigGen @UPIVOTES Nothing upienv upistate
1531+
Right upistateAfterRegistration ->
1532+
(Just updateProposal, )
1533+
<$> sigGen @UPIVOTES Nothing upienv upistateAfterRegistration
1534+
1535+
1536+
-- | Generate an endorsement given an update environment and state.
1537+
protocolVersionEndorsementGen
1538+
:: UPIEnv
1539+
-> UPIState
1540+
-> Gen ProtVer
1541+
protocolVersionEndorsementGen upienv upistate =
1542+
fromMaybe (protocolVersion upistate)
1543+
<$> pickHighlyEndorsedProtocolVersion endorsementsList
1544+
where
1545+
-- Generate a list of protocol version endorsements. For this we look at the
1546+
-- current endorsements, and confirmed and stable proposals.
1547+
--
1548+
-- If there are no endorsements, then the confirmed and stable proposals
1549+
-- provide fresh protocol versions that can be endorsed.
1550+
endorsementsList :: [(ProtVer, Set Core.VKeyGenesis)]
1551+
endorsementsList = endorsementsMap `Map.union` emptyEndorsements
1552+
& Map.toList
1553+
where
1554+
emptyEndorsements :: Map ProtVer (Set Core.VKeyGenesis)
1555+
emptyEndorsements = zip stableAndConfirmedVersions (repeat Set.empty)
1556+
& Map.fromList
1557+
where
1558+
stableAndConfirmedVersions
1559+
:: [ProtVer]
1560+
stableAndConfirmedVersions = stableAndConfirmedProposalIDs ◁ rpus
1561+
& Map.elems
1562+
& fmap fst
1563+
where
1564+
stableAndConfirmedProposalIDs =
1565+
dom (confirmedProposals upistate ▷<= sn -. 2 *. k)
1566+
where
1567+
(sn, _, k, _) = upienv
1568+
1569+
rpus = registeredProtocolUpdateProposals upistate
1570+
1571+
endorsementsMap :: Map ProtVer (Set Core.VKeyGenesis)
1572+
endorsementsMap = Set.toList (endorsements upistate)
1573+
& fmap (second Set.singleton)
1574+
& Map.fromListWith Set.union

‎byron/ledger/executable-spec/test/Ledger/Update/Properties.hs

+47-101
Original file line numberDiff line numberDiff line change
@@ -18,15 +18,11 @@ module Ledger.Update.Properties
1818

1919
import GHC.Stack (HasCallStack)
2020

21-
import Control.Arrow (second)
2221
import qualified Data.Bimap as Bimap
2322
import Data.Foldable (fold, traverse_)
2423
import Data.Function ((&))
2524
import Data.List.Unique (count)
26-
import Data.Map.Strict (Map)
27-
import qualified Data.Map.Strict as Map
28-
import Data.Maybe (catMaybes, fromMaybe, isNothing)
29-
import Data.Set (Set)
25+
import Data.Maybe (catMaybes, isNothing)
3026
import qualified Data.Set as Set
3127
import Data.Word (Word64)
3228
import Hedgehog (Property, cover, forAll, property, withTests)
@@ -35,7 +31,7 @@ import qualified Hedgehog.Range as Range
3531
import Numeric.Natural (Natural)
3632

3733
import Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS,
38-
Signal, State, TRC (TRC), applySTS, initialRules, judgmentContext, trans,
34+
Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
3935
transitionRules, wrapFailed, (?!))
4036
import Control.State.Transition.Generator (HasTrace, envGen, randomTraceOfSize, ratio,
4137
sigGen, trace, traceLengthsAreClassified, traceOfLength)
@@ -44,7 +40,7 @@ import Control.State.Transition.Trace (Trace, TraceOrder (OldestFirst)
4440
traceSignals, traceStates, _traceEnv, _traceInitState)
4541

4642
import Ledger.Core (BlockCount (BlockCount), Slot (Slot), SlotCount (SlotCount), dom,
47-
unBlockCount, (*.), (-.), (▷<=), (◁))
43+
unBlockCount)
4844
import qualified Ledger.Core as Core
4945
import Ledger.GlobalParams (slotsPerEpoch)
5046
import Ledger.Update (PParams, ProtVer, UPIEND, UPIEnv, UPIREG, UPIState, UPIVOTES, UProp,
@@ -92,9 +88,11 @@ upiregRelevantTracesAreCovered = withTests 300 $ property $ do
9288
--------------------------------------------------------------------------------
9389
-- Maximum block-size checks
9490
--------------------------------------------------------------------------------
95-
cover 50
96-
"at least 30% of the update proposals decrease the maximum block-size"
97-
(0.3 <= ratio (wrtCurrentProtocolParameters Update._maxBkSz Decreases) sample)
91+
-- NOTE: since we want to generate valid signals, we cannot decrease the block
92+
-- size in most of the cases.
93+
cover 20
94+
"at least 5% of the update proposals decrease the maximum block-size"
95+
(0.05 <= ratio (wrtCurrentProtocolParameters Update._maxBkSz Decreases) sample)
9896

9997
cover 50
10098
"at least 30% of the update proposals increase the maximum block-size"
@@ -104,18 +102,12 @@ upiregRelevantTracesAreCovered = withTests 300 $ property $ do
104102
"at least 10% of the update proposals do not change the maximum block-size"
105103
(0.1 <= ratio (wrtCurrentProtocolParameters Update._maxBkSz RemainsTheSame) sample)
106104

107-
-- TODO: in the future we should change 1 to the minimum allowed protocol
108-
-- value. But first we need to determine what that value is.
109-
cover 20
110-
"at least 5% of the update proposals set the maximum block-size to 1"
111-
(0.05 <= ratio (Update._maxBkSz `isSetTo` 1) sample)
112-
113105
--------------------------------------------------------------------------------
114106
-- Maximum header-size checks
115107
--------------------------------------------------------------------------------
116-
cover 50
117-
"at least 30% of the update proposals decrease the maximum header-size"
118-
(0.3 <= ratio (wrtCurrentProtocolParameters Update._maxHdrSz Decreases) sample)
108+
cover 20
109+
"at least 5% of the update proposals decrease the maximum header-size"
110+
(0.05 <= ratio (wrtCurrentProtocolParameters Update._maxHdrSz Decreases) sample)
119111

120112
cover 50
121113
"at least 30% of the update proposals increase the maximum header-size"
@@ -125,35 +117,27 @@ upiregRelevantTracesAreCovered = withTests 300 $ property $ do
125117
"at least 10% of the update proposals do not change the maximum header-size"
126118
(0.1 <= ratio (wrtCurrentProtocolParameters Update._maxHdrSz RemainsTheSame) sample)
127119

128-
cover 20
129-
"at least 5% of the update proposals set the maximum header-size to 0"
130-
(0.05 <= ratio (Update._maxHdrSz `isSetTo` 0) sample)
131-
132120
--------------------------------------------------------------------------------
133121
-- Maximum transaction-size checks
134122
--------------------------------------------------------------------------------
135-
cover 50
136-
"at least 30% of the update proposals decrease the maximum transaction-size"
137-
(0.3 <= ratio (wrtCurrentProtocolParameters Update._maxTxSz Decreases) sample)
123+
cover 20
124+
"at least 5% of the update proposals decrease the maximum transaction-size"
125+
(0.05 <= ratio (wrtCurrentProtocolParameters Update._maxTxSz Decreases) sample)
138126

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

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

147-
cover 20
148-
"at least 5% of the update proposals set the maximum transaction-size to 0"
149-
(0.05 <= ratio (Update._maxTxSz `isSetTo` 0) sample)
150-
151135
--------------------------------------------------------------------------------
152136
-- Maximum proposal-size checks
153137
--------------------------------------------------------------------------------
154-
cover 50
138+
cover 20
155139
"at least 30% of the update proposals decrease the maximum proposal-size"
156-
(0.3 <= ratio (wrtCurrentProtocolParameters Update._maxPropSz Decreases) sample)
140+
(0.05 <= ratio (wrtCurrentProtocolParameters Update._maxPropSz Decreases) sample)
157141

158142
cover 50
159143
"at least 30% of the update proposals increase the maximum proposal-size"
@@ -163,10 +147,6 @@ upiregRelevantTracesAreCovered = withTests 300 $ property $ do
163147
"at least 10% of the update proposals do not change the maximum proposal-size"
164148
(0.1 <= ratio (wrtCurrentProtocolParameters Update._maxPropSz RemainsTheSame) sample)
165149

166-
cover 20
167-
"at least 5% of the update proposals set the maximum proposal-size to 0"
168-
(0.05 <= ratio (Update._maxPropSz `isSetTo` 0) sample)
169-
170150
-- NOTE: after empirically determining the checks above are sensible, we can
171151
-- add more coverage tests for the other protocol parameters.
172152

@@ -222,18 +202,28 @@ upiregRelevantTracesAreCovered = withTests 300 $ property $ do
222202
check Decreases proposedParameterValue = proposedParameterValue < currentParameterValue
223203
check RemainsTheSame proposedParameterValue = currentParameterValue == proposedParameterValue
224204

205+
-- TODO: leaving this here as it might be useful in the future. Remove if it
206+
-- isn't (dnadales - 07/17/2019). We use git, but nobody will see if it sits
207+
-- in our history.
208+
--
225209
-- Count the number of times in the sequence of update proposals that the
226210
-- given protocol value is set to the given value.
227-
isSetTo
228-
:: Eq v
229-
=> (PParams -> v)
230-
-> v
231-
-> Trace UPIREG
232-
-> Int
233-
isSetTo parameterValue value traceSample
234-
= fmap (parameterValue . Update._upParams) (traceSignals OldestFirst traceSample)
235-
& filter (value ==)
236-
& length
211+
--
212+
-- Example usage:
213+
--
214+
-- > cover 20
215+
-- > "at least 5% of the update proposals set the maximum proposal-size to 0"
216+
-- > (0.05 <= ratio (Update._maxPropSz `isSetTo` 0) sample)
217+
-- isSetTo
218+
-- :: Eq v
219+
-- => (PParams -> v)
220+
-- -> v
221+
-- -> Trace UPIREG
222+
-- -> Int
223+
-- isSetTo parameterValue value traceSample
224+
-- = fmap (parameterValue . Update._upParams) (traceSignals OldestFirst traceSample)
225+
-- & filter (value ==)
226+
-- & length
237227

238228
expectedNumberOfUpdateProposalsPerKey :: Trace UPIREG -> Double
239229
expectedNumberOfUpdateProposalsPerKey traceSample =
@@ -364,58 +354,24 @@ instance HasTrace UBLOCK where
364354
do
365355
let numberOfGenesisKeys = 7
366356
dms <- Update.dmapGen numberOfGenesisKeys
367-
-- We don't want a large value of @k@, otherwise we won't see many confirmed proposals or
368-
-- epoch changes. The problem here is that the initial environment does not know anything
369-
-- about the trace size, and @k@ should be a function of it.
357+
-- We don't want a large value of @k@, otherwise we won't see many
358+
-- confirmed proposals or epoch changes. The problem here is that the
359+
-- initial environment does not know anything about the trace size, and
360+
-- @k@ should be a function of it.
370361
pure (Slot 0, dms, BlockCount 10, numberOfGenesisKeys)
371362

372363
sigGen _ _env UBlockState {upienv, upistate} = do
373-
let rpus = Update.registeredProtocolUpdateProposals upistate
374364
(anOptionalUpdateProposal, aListOfVotes) <-
375-
-- We want to generate update proposals when there is none registered. Otherwise we won't get
376-
-- any proposals or votes.
377-
if Set.null (dom rpus)
378-
then generateUpdateProposalAndVotes
379-
else Gen.frequency [ (5, generateOnlyVotes)
380-
, (1, generateUpdateProposalAndVotes)
381-
]
382-
-- Don't shrink the issuer as this won't give us additional insight on a test failure.
365+
Update.updateProposalAndVotesGen upienv upistate
366+
367+
-- Don't shrink the issuer as this won't give us additional insight on a
368+
-- test failure.
383369
aBlockIssuer <- Gen.prune $
384370
-- Pick a delegate from the delegation map
385371
Gen.element $ Bimap.elems (Update.delegationMap upienv)
386372

387-
let
388-
-- Generate a list of protocol version endorsements. For this we look at the current
389-
-- endorsements, and confirmed and stable proposals.
390-
--
391-
-- If there are no endorsements, then the confirmed and stable proposals provide fresh
392-
-- protocol versions that can be endorsed.
393-
endorsementsList :: [(ProtVer, Set Core.VKeyGenesis)]
394-
endorsementsList = endorsementsMap `Map.union` emptyEndorsements
395-
& Map.toList
396-
where
397-
emptyEndorsements :: Map ProtVer (Set Core.VKeyGenesis)
398-
emptyEndorsements = zip stableAndConfirmedVersions (repeat Set.empty)
399-
& Map.fromList
400-
where
401-
stableAndConfirmedVersions
402-
:: [ProtVer]
403-
stableAndConfirmedVersions = stableAndConfirmedProposalIDs ◁ rpus
404-
& Map.elems
405-
& fmap fst
406-
where
407-
stableAndConfirmedProposalIDs =
408-
dom (Update.confirmedProposals upistate ▷<= sn -. 2 *. k)
409-
where
410-
(sn, _, k, _) = upienv
411-
412-
endorsementsMap :: Map ProtVer (Set Core.VKeyGenesis)
413-
endorsementsMap = Set.toList (Update.endorsements upistate)
414-
& fmap (second Set.singleton)
415-
& Map.fromListWith Set.union
416-
417373
aBlockVersion <-
418-
fromMaybe (Update.protocolVersion upistate) <$> Update.protocolVersionEndorsementGen endorsementsList
374+
Update.protocolVersionEndorsementGen upienv upistate
419375

420376
UBlock
421377
<$> pure aBlockIssuer
@@ -424,16 +380,6 @@ instance HasTrace UBLOCK where
424380
<*> pure anOptionalUpdateProposal
425381
<*> pure aListOfVotes
426382
where
427-
generateOnlyVotes = (Nothing,) <$> sigGen @UPIVOTES Nothing upienv upistate
428-
generateUpdateProposalAndVotes = do
429-
updateProposal <- sigGen @UPIREG Nothing upienv upistate
430-
-- We want to have the possibility of generating votes for the proposal we
431-
-- registered.
432-
case applySTS @UPIREG (TRC (upienv, upistate, updateProposal)) of
433-
Left _ ->
434-
(Just updateProposal, ) <$> sigGen @UPIVOTES Nothing upienv upistate
435-
Right upistateAfterRegistration ->
436-
(Just updateProposal, ) <$> sigGen @UPIVOTES Nothing upienv upistateAfterRegistration
437383
nextSlotGen =
438384
incSlot <$> Gen.frequency
439385
[ (5, Gen.integral (Range.constant 1 10))
@@ -494,7 +440,7 @@ ublockRelevantTracesAreCovered = withTests 150 $ property $ do
494440

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

‎byron/semantics/executable-spec/src/Control/State/Transition.hs

+25-20
Original file line numberDiff line numberDiff line change
@@ -1,29 +1,29 @@
1-
{-# LANGUAGE AllowAmbiguousTypes #-}
2-
{-# LANGUAGE DataKinds #-}
3-
{-# LANGUAGE DeriveFunctor #-}
4-
{-# LANGUAGE FlexibleContexts #-}
5-
{-# LANGUAGE FlexibleInstances #-}
6-
{-# LANGUAGE GADTs #-}
7-
{-# LANGUAGE KindSignatures #-}
8-
{-# LANGUAGE MultiParamTypeClasses #-}
9-
{-# LANGUAGE PolyKinds #-}
10-
{-# LANGUAGE RankNTypes #-}
11-
{-# LANGUAGE ScopedTypeVariables #-}
12-
{-# LANGUAGE StandaloneDeriving #-}
13-
{-# LANGUAGE TypeApplications #-}
14-
{-# LANGUAGE TypeFamilies #-}
1+
{-# LANGUAGE AllowAmbiguousTypes #-}
2+
{-# LANGUAGE DataKinds #-}
3+
{-# LANGUAGE DeriveFunctor #-}
4+
{-# LANGUAGE FlexibleContexts #-}
5+
{-# LANGUAGE FlexibleInstances #-}
6+
{-# LANGUAGE GADTs #-}
7+
{-# LANGUAGE KindSignatures #-}
8+
{-# LANGUAGE MultiParamTypeClasses #-}
9+
{-# LANGUAGE PolyKinds #-}
10+
{-# LANGUAGE RankNTypes #-}
11+
{-# LANGUAGE ScopedTypeVariables #-}
12+
{-# LANGUAGE StandaloneDeriving #-}
13+
{-# LANGUAGE TypeApplications #-}
14+
{-# LANGUAGE TypeFamilies #-}
1515
{-# LANGUAGE TypeFamilyDependencies #-}
16-
{-# LANGUAGE UndecidableInstances #-}
16+
{-# LANGUAGE UndecidableInstances #-}
1717

1818
-- | Small step state transition systems.
1919
module Control.State.Transition where
2020

21-
import Control.Monad (unless)
22-
import Control.Monad.Free.Church
23-
import Control.Monad.Trans.State.Strict (modify, runState)
21+
import Control.Monad (unless)
22+
import Control.Monad.Free.Church
23+
import Control.Monad.Trans.State.Strict (modify, runState)
2424
import qualified Control.Monad.Trans.State.Strict as MonadState
25-
import Data.Foldable (find, traverse_)
26-
import Data.Kind (Type)
25+
import Data.Foldable (find, traverse_)
26+
import Data.Kind (Type)
2727

2828
data RuleType
2929
= Initial
@@ -186,3 +186,8 @@ applySTS :: forall s rtype
186186
applySTS ctx = case applySTSIndifferently ctx of
187187
(st, []) -> Right st
188188
(_, pfs) -> Left pfs
189+
190+
-- | This can be used to specify predicate failures in STS rules where a value
191+
-- is beyond a certain threshold.
192+
newtype Threshold a = Threshold a
193+
deriving (Eq, Ord, Show)

‎byron/semantics/executable-spec/src/Control/State/Transition/Generator.hs

+2
Original file line numberDiff line numberDiff line change
@@ -522,6 +522,8 @@ onlyValidSignalsAreGenerated maximumTraceLength = property $ do
522522
let result = applySTS @s (TRC(env, st', sig))
523523
-- TODO: For some reason the result that led to the failure is not shown
524524
-- (even without using tasty, and setting the condition to True === False)
525+
footnoteShow st'
526+
footnoteShow sig
525527
footnoteShow result
526528
void $ evalEither result
527529

0 commit comments

Comments
 (0)
Please sign in to comment.