Merge pull request #1085 from input-output-hk/nc/slotting-2

Use slotting types shared with ouroboros-network

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

@@ -152,7 +152,7 @@ propMultipleOfSizesBlock b =
 propBlockAbstractSize :: Property
 propBlockAbstractSize
   = withTests 50 $ property $ do
-    tr <- forAll (trace @CHAIN 100)
+    tr <- forAll (trace @CHAIN () 100)
     let blocks = traceSignals OldestFirst tr :: [Block]
     mapM_ propMultipleOfSizesBlock blocks
 

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

@@ -30,7 +30,7 @@ import           Cardano.Spec.Chain.STS.Rule.Epoch (sEpoch)
 slotsIncrease :: Property
 slotsIncrease = property $ do
   let (maxTraceLength, step) = (100, 10)
-  tr <- forAll $ traceSigGen
+  tr <- forAll $ traceSigGen ()
                    (Maximum maxTraceLength)
                    (sigGenChain NoGenDelegation NoGenUTxO NoGenUpdate)
   classifyTraceLength tr maxTraceLength step
@@ -45,7 +45,7 @@ blockIssuersAreDelegates :: Property
 blockIssuersAreDelegates =
   withTests 300 $ property $ do
     let (maxTraceLength, step) = (100, 10)
-    tr <- forAll $ traceSigGen
+    tr <- forAll $ traceSigGen ()
                      (Maximum maxTraceLength)
                      (sigGenChain GenDelegation NoGenUTxO GenUpdate)
     classifyTraceLength tr maxTraceLength step
@@ -66,12 +66,13 @@ blockIssuersAreDelegates =
 
 onlyValidSignalsAreGenerated :: Property
 onlyValidSignalsAreGenerated =
-  withTests 200 $ Transition.Generator.onlyValidSignalsAreGenerated @CHAIN 100
+  withTests 200 $ Transition.Generator.onlyValidSignalsAreGenerated @CHAIN () 100
 
 signersListIsBoundedByK :: Property
 signersListIsBoundedByK =  withTests 300 $ property $ do
   let maxTraceLength = 100
   tr <- forAll $ traceSigGen
+                   ()
                    (Maximum maxTraceLength)
                    (sigGenChain GenDelegation NoGenUTxO GenUpdate)
   signersListIsBoundedByKInTrace tr
@@ -89,7 +90,7 @@ signersListIsBoundedByK =  withTests 300 $ property $ do
 
 relevantCasesAreCovered :: Property
 relevantCasesAreCovered = withTests 200 $ property $ do
-  tr <- forAll $ traceSigGen (Desired 200) (sigGenChain GenDelegation NoGenUTxO NoGenUpdate)
+  tr <- forAll $ traceSigGen () (Desired 200) (sigGenChain GenDelegation NoGenUTxO NoGenUpdate)
   let certs = traceDCerts tr
 
   -- for at least 1% of traces...
@@ -197,6 +198,7 @@ invalidSignalsAreGenerated =
   withTests 100
     $ Transition.Generator.invalidSignalsAreGenerated
         @CHAIN
+        ()
         [(1, invalidProofsBlockGen)]
         50
         (coverInvalidBlockProofs 20)

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)

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

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

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 = [] }
 
     ]

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

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

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 }

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)

byron/semantics/executable-spec/small-steps.cabal

@@ -23,6 +23,8 @@ flag development
 
 library
   exposed-modules:     Control.State.Transition
+                     , Control.State.Transition.Extended
+                     , Control.State.Transition.Simple
                      , Control.State.Transition.Invalid.Trace
                      , Control.State.Transition.Generator
                      , Control.State.Transition.Trace
@@ -90,17 +92,20 @@ test-suite examples
   hs-source-dirs:      test
   main-is:             examples/Main.hs
   other-modules:       Control.State.Transition.Examples.Sum
+  other-modules:       Control.State.Transition.Examples.GlobalSum
                      , Control.State.Transition.Examples.CommitReveal
   type:                exitcode-stdio-1.0
   default-language:    Haskell2010
   build-depends:       base
                      , containers
                      , hedgehog >= 1.0
+                     , mtl
                      , tasty
                      , tasty-hedgehog
                      , tasty-expected-failure
                      , QuickCheck
                      , tasty-quickcheck
+                     , tasty-hunit
                      , Unique
                      -- IOHK deps
                      , cardano-crypto-class