diff --git a/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXOWS.hs b/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXOWS.hs index 08d10ef60e5..afeed79a093 100644 --- a/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXOWS.hs +++ b/byron/ledger/executable-spec/src/Cardano/Ledger/Spec/STS/UTXOWS.hs @@ -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) diff --git a/byron/ledger/executable-spec/src/Ledger/Delegation.hs b/byron/ledger/executable-spec/src/Ledger/Delegation.hs index 14ccd752564..4255f3bfcd7 100644 --- a/byron/ledger/executable-spec/src/Ledger/Delegation.hs +++ b/byron/ledger/executable-spec/src/Ledger/Delegation.hs @@ -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 diff --git a/byron/ledger/executable-spec/test/Ledger/AbstractSize/Properties.hs b/byron/ledger/executable-spec/test/Ledger/AbstractSize/Properties.hs index d1685c0cad5..55275d838f6 100644 --- a/byron/ledger/executable-spec/test/Ledger/AbstractSize/Properties.hs +++ b/byron/ledger/executable-spec/test/Ledger/AbstractSize/Properties.hs @@ -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 diff --git a/byron/ledger/executable-spec/test/Ledger/Delegation/Examples.hs b/byron/ledger/executable-spec/test/Ledger/Delegation/Examples.hs index 4f0956ee0ca..1a9c063bde4 100644 --- a/byron/ledger/executable-spec/test/Ledger/Delegation/Examples.hs +++ b/byron/ledger/executable-spec/test/Ledger/Delegation/Examples.hs @@ -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) @@ -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 [] []) @@ -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 [] []) @@ -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 [] []) @@ -74,7 +74,7 @@ deleg = ] , testGroup "Multiple Activations" - [ testCase "Example 0" $ checkTrace @ADELEGS genKeys $ + [ testCase "Example 0" $ checkTrace @ADELEGS runIdentity genKeys $ pure (DState [] []) @@ -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 [] []) @@ -146,7 +146,7 @@ deleg = ] } in - checkTrace @DELEG env $ + checkTrace @DELEG runIdentity env $ pure st .- [] .-> st { _dIStateScheduledDelegations = [] } ] diff --git a/byron/ledger/executable-spec/test/Ledger/Delegation/Properties.hs b/byron/ledger/executable-spec/test/Ledger/Delegation/Properties.hs index 5ecb6e7452d..405c77f9c06 100644 --- a/byron/ledger/executable-spec/test/Ledger/Delegation/Properties.hs +++ b/byron/ledger/executable-spec/test/Ledger/Delegation/Properties.hs @@ -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 @@ -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. @@ -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 @@ -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 @@ -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 @@ -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. @@ -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 diff --git a/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs b/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs index 9c8e7e4b5f4..33b120c1efe 100644 --- a/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs +++ b/byron/ledger/executable-spec/test/Ledger/UTxO/Properties.hs @@ -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 @@ -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 @@ -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 @@ -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 @@ -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 diff --git a/byron/ledger/executable-spec/test/Ledger/Update/Examples.hs b/byron/ledger/executable-spec/test/Ledger/Update/Examples.hs index f79387a0ab5..12b212e8b5d 100644 --- a/byron/ledger/executable-spec/test/Ledger/Update/Examples.hs +++ b/byron/ledger/executable-spec/test/Ledger/Update/Examples.hs @@ -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) @@ -55,6 +55,7 @@ upiendExamples = } in checkTrace @UPIEND + runIdentity ( Slot { unSlot = 15 } , [ ( VKeyGenesis { unVKeyGenesis = VKey Owner { unOwner = 0 } } , VKey Owner { unOwner = 0 } diff --git a/byron/ledger/executable-spec/test/Ledger/Update/Properties.hs b/byron/ledger/executable-spec/test/Ledger/Update/Properties.hs index 32030893d50..c9c2fb91056 100644 --- a/byron/ledger/executable-spec/test/Ledger/Update/Properties.hs +++ b/byron/ledger/executable-spec/test/Ledger/Update/Properties.hs @@ -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" @@ -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. @@ -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 @@ -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 = " @@ -567,6 +567,7 @@ invalidRegistrationsAreGenerated = withTests 300 $ Transition.Generator.invalidSignalsAreGenerated @UPIREG + () [(1, invalidUPropGen)] 100 (Update.Test.coverUpiregFailures 2) @@ -582,6 +583,7 @@ invalidSignalsAreGenerated = withTests 300 $ Transition.Generator.invalidSignalsAreGenerated @UBLOCK + () [(1, invalidUBlockGen)] 100 (Update.Test.coverUpivoteFailures 2) diff --git a/byron/semantics/executable-spec/src/Control/State/Transition/Generator.hs b/byron/semantics/executable-spec/src/Control/State/Transition/Generator.hs index 2d979c7a69d..9b3c355d2b3 100644 --- a/byron/semantics/executable-spec/src/Control/State/Transition/Generator.hs +++ b/byron/semantics/executable-spec/src/Control/State/Transition/Generator.hs @@ -24,6 +24,8 @@ module Control.State.Transition.Generator ( HasTrace , SignalGenerator + , BaseEnv + , interpretSTS , envGen , sigGen , traceSigGen diff --git a/byron/semantics/executable-spec/src/Control/State/Transition/Trace.hs b/byron/semantics/executable-spec/src/Control/State/Transition/Trace.hs index f11c2a08dcc..63d625ff48f 100644 --- a/byron/semantics/executable-spec/src/Control/State/Transition/Trace.hs +++ b/byron/semantics/executable-spec/src/Control/State/Transition/Trace.hs @@ -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. -- diff --git a/byron/semantics/executable-spec/src/Control/State/Transition/Trace/Generator/QuickCheck.hs b/byron/semantics/executable-spec/src/Control/State/Transition/Trace/Generator/QuickCheck.hs index 0146b857874..d7a0565ccc1 100644 --- a/byron/semantics/executable-spec/src/Control/State/Transition/Trace/Generator/QuickCheck.hs +++ b/byron/semantics/executable-spec/src/Control/State/Transition/Trace/Generator/QuickCheck.hs @@ -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