Skip to content

Commit

Permalink
Fix cs-ledger
Browse files Browse the repository at this point in the history
  • Loading branch information
nc6 committed Dec 11, 2019
1 parent 62cf056 commit 31dd115
Show file tree
Hide file tree
Showing 11 changed files with 43 additions and 36 deletions.
Expand Up @@ -56,4 +56,4 @@ instance HasTrace UTXOWS where

-- We generate signal for UTXOWS as a list of signals from UTXOW
sigGen env st =
traceSignals OldestFirst <$> genTrace @UTXOW 20 env st (sigGen @UTXOW)
traceSignals OldestFirst <$> genTrace @UTXOW () 20 env st (sigGen @UTXOW)
2 changes: 1 addition & 1 deletion byron/ledger/executable-spec/src/Ledger/Delegation.hs
Expand Up @@ -544,7 +544,7 @@ dcertsGen env st =
-- This generator can result in an empty list of delegation certificates if
-- no delegation certificates can be produced, according to the delegation
-- rules, given the initial state and environment.
catMaybes . traceSignals OldestFirst <$> genTrace @MSDELEG n env subSt (sigGen @MSDELEG)
catMaybes . traceSignals OldestFirst <$> genTrace @MSDELEG () n env subSt (sigGen @MSDELEG)
where n = env ^. allowedDelegators . to length . to fromIntegral
subSt = DSState
{ _dSStateScheduledDelegations = _dIStateScheduledDelegations st
Expand Down
Expand Up @@ -145,7 +145,7 @@ propMultipleOfSizes txw =
propTxAbstractSize :: Property
propTxAbstractSize
= withTests 50 $ property $ do
tr <- forAll (trace @UTXOW 100)
tr <- forAll (trace @UTXOW () 100)
let txs = traceSignals OldestFirst tr :: [TxWits]
mapM_ propSize txs
where
Expand Down
14 changes: 7 additions & 7 deletions byron/ledger/executable-spec/test/Ledger/Delegation/Examples.hs
Expand Up @@ -12,7 +12,7 @@ import Data.Word (Word64)
import Numeric.Natural (Natural)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.HUnit (testCase)

import Data.Functor.Identity (runIdentity)
import Control.State.Transition.Trace (checkTrace, (.-), (.->))
import Ledger.Core (BlockCount (BlockCount), Epoch (Epoch), Owner (Owner), Sig (Sig),
Slot (Slot), VKey (VKey), VKeyGenesis (VKeyGenesis), owner)
Expand All @@ -26,7 +26,7 @@ import Ledger.Delegation (ADELEG, ADELEGS, DCert (DCert), DELEG, DISta
deleg :: [TestTree]
deleg =
[ testGroup "Activation"
[ testCase "Example 0" $ checkTrace @ADELEG genKeys $
[ testCase "Example 0" $ checkTrace @ADELEG runIdentity genKeys $

pure (DState [] [])

Expand All @@ -44,7 +44,7 @@ deleg =
.- (s 3, (gk 2, k 12)) .-> DState [(gk 0, k 10), (gk 1, k 11), (gk 2, k 12)]
[(gk 0, s 0), (gk 1, s 1), (gk 2, s 3)]

, testCase "Example 1" $ checkTrace @ADELEG genKeys $
, testCase "Example 1" $ checkTrace @ADELEG runIdentity genKeys $

pure (DState [] [])

Expand All @@ -55,7 +55,7 @@ deleg =
-- should be a no-op on the delegation state.
.- (s 1, (gk 1, k 2)) .-> DState [(gk 0, k 2)]
[(gk 0, s 0)]
, testCase "Example 2" $ checkTrace @ADELEG genKeys $
, testCase "Example 2" $ checkTrace @ADELEG runIdentity genKeys $

pure (DState [] [])

Expand All @@ -74,7 +74,7 @@ deleg =
]

, testGroup "Multiple Activations"
[ testCase "Example 0" $ checkTrace @ADELEGS genKeys $
[ testCase "Example 0" $ checkTrace @ADELEGS runIdentity genKeys $

pure (DState [] [])

Expand All @@ -86,7 +86,7 @@ deleg =
]

, testGroup "Scheduling"
[ testCase "Example 0" $ checkTrace @SDELEG (DSEnv [gk 0, gk 1, gk 2] (e 8) (s 2) (bk 2160)) $
[ testCase "Example 0" $ checkTrace @SDELEG runIdentity (DSEnv [gk 0, gk 1, gk 2] (e 8) (s 2) (bk 2160)) $

pure (DSState [] [])

Expand Down Expand Up @@ -146,7 +146,7 @@ deleg =
]
}
in
checkTrace @DELEG env $
checkTrace @DELEG runIdentity env $
pure st .- [] .-> st { _dIStateScheduledDelegations = [] }

]
Expand Down
Expand Up @@ -224,7 +224,7 @@ expectedDms s d sbs =
dcertsAreNotReplayed :: Property
dcertsAreNotReplayed = withTests 300 $ property $ do
let (thisTraceLength, step) = (100, 10)
sample <- forAll (traceWithProfile @DBLOCK thisTraceLength profile)
sample <- forAll (traceWithProfile @DBLOCK () thisTraceLength profile)
classifyTraceLength sample thisTraceLength step
dcertsAreNotReplayedInTrace sample
where
Expand Down Expand Up @@ -302,12 +302,12 @@ dcertsAreTriggered :: Property
dcertsAreTriggered = withTests 300 $ property $
-- The number of tests was determined ad-hoc, since the default failed to
-- uncover the presence of errors.
forAll (nonTrivialTrace 100) >>= dcertsAreTriggeredInTrace
forAll (nonTrivialTrace () 100) >>= dcertsAreTriggeredInTrace

dblockTracesAreClassified :: Property
dblockTracesAreClassified = withTests 200 $ property $ do
let (tl, step) = (100, 10)
tr <- forAll (trace @DBLOCK tl)
tr <- forAll (trace @DBLOCK () tl)
classifyTraceLength tr tl step
-- Classify the traces by the total number of delegation certificates on
-- them.
Expand All @@ -326,7 +326,7 @@ traceDCerts = concat . traceDCertsByBlock
relevantCasesAreCovered :: Property
relevantCasesAreCovered = withTests 400 $ property $ do
let tl = 100
tr <- forAll (trace @DBLOCK tl)
tr <- forAll (trace @DBLOCK () tl)

-- 40% of the traces must contain as many delegation certificates as blocks.
cover 40
Expand Down Expand Up @@ -370,7 +370,7 @@ relevantCasesAreCovered = withTests 400 $ property $ do

onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated =
withTests 300 $ Transition.Generator.onlyValidSignalsAreGenerated @DBLOCK 100
withTests 300 $ Transition.Generator.onlyValidSignalsAreGenerated @DBLOCK () 100

--------------------------------------------------------------------------------
-- Properties related to the transition rules
Expand All @@ -386,7 +386,7 @@ onlyValidSignalsAreGenerated =
rejectDupSchedDelegs :: Property
rejectDupSchedDelegs = withTests 300 $ property $ do
(tr, dcert) <- forAll $ do
tr <- trace @DELEG 100
tr <- trace @DELEG () 100
`suchThatLastState` (not . null . view scheduledDelegations)
let vkS =
case lastState tr ^. scheduledDelegations of
Expand All @@ -404,7 +404,7 @@ rejectDupSchedDelegs = withTests 300 $ property $ do

-- | Classify the traces.
tracesAreClassified :: Property
tracesAreClassified = traceLengthsAreClassified @DELEG 1000 100
tracesAreClassified = traceLengthsAreClassified @DELEG () 1000 100

-- | The signal generator generates invalid signals with high probability when
-- invalid signals are requested.
Expand All @@ -413,6 +413,7 @@ invalidSignalsAreGenerated =
withTests 300
$ Transition.Generator.invalidSignalsAreGenerated
@DBLOCK
()
(failures profile)
100
-- We have 6 failures we're interested in. However demanding an uniform
Expand Down
12 changes: 6 additions & 6 deletions byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs
Expand Up @@ -32,13 +32,13 @@ import Ledger.UTxO (Tx (Tx), TxIn (TxIn), TxOut (TxOut), TxWits, UTxO
-- | Check that the money is constant in the system.
moneyIsConstant :: Property
moneyIsConstant = withTests 300 . property $ do
(st0, st) <- firstAndLastState <$> forAll (trace @UTXOW 100)
(st0, st) <- firstAndLastState <$> forAll (trace @UTXOW () 100)
reserves st0 + balance (utxo st0) === reserves st + balance (utxo st)

-- | Check that there is no double spending
noDoubleSpending :: Property
noDoubleSpending = withTests 300 . property $ do
t <- forAll (trace @UTXOW 100)
t <- forAll (trace @UTXOW () 100)
let
UTxOState {utxo = utxo0} = _traceInitState t
txs = body <$> traceSignals OldestFirst t
Expand All @@ -55,7 +55,7 @@ noDoubleSpending = withTests 300 . property $ do
-- | Check that UTxO is outputs minus inputs
utxoDiff :: Property
utxoDiff = withTests 300 . property $ do
t <- forAll (trace @UTXOW 100)
t <- forAll (trace @UTXOW () 100)
let
(utxo0, utxoSt) = (utxo *** utxo) . firstAndLastState $ t
txs = body <$> traceSignals OldestFirst t
Expand All @@ -70,7 +70,7 @@ utxoDiff = withTests 300 . property $ do

utxoAndTxoutsMustBeDisjoint :: Property
utxoAndTxoutsMustBeDisjoint = withTests 300 . property $ do
t <- forAll (trace @UTXOW 100)
t <- forAll (trace @UTXOW () 100)
traverse_ utxoAndTxoutsAreDisjoint
$ fmap (second body)
$ preStatesAndSignals OldestFirst t
Expand All @@ -85,7 +85,7 @@ utxoAndTxoutsMustBeDisjoint = withTests 300 . property $ do
relevantCasesAreCovered :: Property
relevantCasesAreCovered = withTests 400 $ property $ do
let tl = 300
tr <- forAll (traceOfLength @UTXOW tl)
tr <- forAll (traceOfLength @UTXOW () tl)
let n :: Integer
n = fromIntegral $ traceLength tr

Expand Down Expand Up @@ -171,7 +171,7 @@ avgInputsOutputs txs
tracesAreClassified :: Property
tracesAreClassified = withTests 200 . property $ do
let (tl, step) = (100, 10)
tr <- forAll (trace @UTXOW tl)
tr <- forAll (trace @UTXOW () tl)
classifyTraceLength tr tl step

let
Expand Down
3 changes: 2 additions & 1 deletion byron/ledger/executable-spec/test/Ledger/Update/Examples.hs
Expand Up @@ -5,7 +5,7 @@
module Ledger.Update.Examples where

import GHC.Exts (fromList)

import Data.Functor.Identity (runIdentity)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.HUnit (testCase)

Expand Down Expand Up @@ -55,6 +55,7 @@ upiendExamples =
}
in
checkTrace @UPIEND
runIdentity
( Slot { unSlot = 15 }
, [ ( VKeyGenesis { unVKeyGenesis = VKey Owner { unOwner = 0 } }
, VKey Owner { unOwner = 0 }
Expand Down
16 changes: 9 additions & 7 deletions byron/ledger/executable-spec/test/Ledger/Update/Properties.hs
Expand Up @@ -56,11 +56,11 @@ import qualified Ledger.Update.Test as Update.Test

upiregTracesAreClassified :: Property
upiregTracesAreClassified =
withTests 100 $ traceLengthsAreClassified @UPIREG 100 10
withTests 100 $ traceLengthsAreClassified @UPIREG () 100 10

upiregRelevantTracesAreCovered :: Property
upiregRelevantTracesAreCovered = withTests 300 $ property $ do
sample <- forAll (trace @UPIREG 200)
sample <- forAll (trace @UPIREG () 200)

cover 40
"at least 30% of the update proposals increase the major version"
Expand Down Expand Up @@ -266,7 +266,7 @@ data Change = Increases | Decreases | RemainsTheSame

onlyValidSignalsAreGenerated :: Property
onlyValidSignalsAreGenerated =
withTests 300 $ Transition.Generator.onlyValidSignalsAreGenerated @UPIREG 100
withTests 300 $ Transition.Generator.onlyValidSignalsAreGenerated @UPIREG () 100


-- | Dummy transition system to test blocks with update payload only.
Expand Down Expand Up @@ -399,15 +399,15 @@ instance HasTrace UBLOCK where

ublockTraceLengthsAreClassified :: Property
ublockTraceLengthsAreClassified =
withTests 100 $ traceLengthsAreClassified @UBLOCK 100 10
withTests 100 $ traceLengthsAreClassified @UBLOCK () 100 10

ublockOnlyValidSignalsAreGenerated :: HasCallStack => Property
ublockOnlyValidSignalsAreGenerated =
withTests 300 $ Transition.Generator.onlyValidSignalsAreGenerated @UBLOCK 100
withTests 300 $ Transition.Generator.onlyValidSignalsAreGenerated @UBLOCK () 100

ublockRelevantTracesAreCovered :: Property
ublockRelevantTracesAreCovered = withTests 300 $ property $ do
sample <- forAll (traceOfLength @UBLOCK 100)
sample <- forAll (traceOfLength @UBLOCK () 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
Expand Down Expand Up @@ -519,7 +519,7 @@ proposalsScheduledForAdoption sample = traceStates OldestFirst sample
-- useful for understanding the traces produced by the 'UBLOCK' transition system.
ublockSampleTraceMetrics :: Word64 -> IO ()
ublockSampleTraceMetrics maxTraceSize = do
sample <- randomTraceOfSize @UBLOCK maxTraceSize
sample <- randomTraceOfSize @UBLOCK () maxTraceSize
let
(_slot, _dms, k, numberOfGenesisKeys) = _traceEnv sample
traverse_ print [ "k = "
Expand Down Expand Up @@ -567,6 +567,7 @@ invalidRegistrationsAreGenerated =
withTests 300
$ Transition.Generator.invalidSignalsAreGenerated
@UPIREG
()
[(1, invalidUPropGen)]
100
(Update.Test.coverUpiregFailures 2)
Expand All @@ -582,6 +583,7 @@ invalidSignalsAreGenerated =
withTests 300
$ Transition.Generator.invalidSignalsAreGenerated
@UBLOCK
()
[(1, invalidUBlockGen)]
100
(Update.Test.coverUpivoteFailures 2)
Expand Down
Expand Up @@ -24,6 +24,8 @@
module Control.State.Transition.Generator
( HasTrace
, SignalGenerator
, BaseEnv
, interpretSTS
, envGen
, sigGen
, traceSigGen
Expand Down
Expand Up @@ -376,11 +376,12 @@ mSt .-> stExpected = do
checkTrace
:: forall s m
. (STS s, BaseM s ~ m)
=> Environment s
-> ReaderT (State s -> Signal s -> m (Either [[PredicateFailure s]] (State s))) IO (State s)
=> (forall a. m a -> a)
-> Environment s
-> ReaderT (State s -> Signal s -> (Either [[PredicateFailure s]] (State s))) IO (State s)
-> IO ()
checkTrace env act =
void $ runReaderT act (\st sig -> applySTS (TRC(env, st, sig)))
checkTrace interp env act =
void $ runReaderT act (\st sig -> interp $ applySTS (TRC(env, st, sig)))

-- | Extract all the values of a given type.
--
Expand Down
Expand Up @@ -15,7 +15,7 @@
{-# LANGUAGE UndecidableInstances #-}

module Control.State.Transition.Trace.Generator.QuickCheck
( HasTrace (envGen, sigGen, shrinkSignal)
( HasTrace (BaseEnv, envGen, sigGen, shrinkSignal, interpretSTS)
, traceFrom
, traceFromInitState
, trace
Expand Down

0 comments on commit 31dd115

Please sign in to comment.