Event Log

alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs

@@ -58,8 +58,8 @@ import Data.Proxy (Proxy (..))
 import Shelley.Spec.Ledger.BlockChain (Block)
 import Shelley.Spec.Ledger.LedgerState (AccountState (..), DPState (..), DState, EpochState (..), LedgerState (..), NewEpochState (..), PState, UTxOState)
 import Shelley.Spec.Ledger.PParams (PParams' (..))
-import Shelley.Spec.Ledger.STS.Chain (CHAIN, ChainPredicateFailure (..), ChainState (..))
-import Shelley.Spec.Ledger.STS.Ledger (LEDGER, LedgerEnv (..), LedgerPredicateFailure (UtxowFailure))
+import Shelley.Spec.Ledger.STS.Chain (CHAIN, ChainPredicateFailure (..), ChainState (..), Event (..))
+import Shelley.Spec.Ledger.STS.Ledger (Event (..), LEDGER, LedgerEnv (..), LedgerPredicateFailure (UtxowFailure))
 import System.Timeout
 import Test.Cardano.Ledger.Alonzo.AlonzoEraGen ()
 import Test.Cardano.Ledger.EraBuffet (TestCrypto)
@@ -95,9 +95,11 @@ import Test.Tasty.QuickCheck
 
 instance Embed (AlonzoBBODY (AlonzoEra TestCrypto)) (CHAIN (AlonzoEra TestCrypto)) where
   wrapFailed = BbodyFailure
+  wrapEvent = BbodyEvent
 
 instance Embed (AlonzoUTXOW (AlonzoEra TestCrypto)) (LEDGER (AlonzoEra TestCrypto)) where
   wrapFailed = UtxowFailure
+  wrapEvent = UtxowEvent
 
 -- ======================================================================================
 -- It is incredably hard to debug property test generators.  These functions mimic the

byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs

@@ -22,7 +22,7 @@ import           Byron.Spec.Ledger.Update (PParams, UPIState, maxBkSz)
 import           Byron.Spec.Ledger.UTxO (UTxO)
 import           Control.State.Transition (Embed, Environment, STS (..), Signal, State,
                      TRC (TRC), initialRules, judgmentContext, trans, transitionRules, wrapFailed,
-                     (?!))
+                     (?!), wrapEvent)
 
 import           Byron.Spec.Chain.STS.Block
 
@@ -57,6 +57,11 @@ instance STS BBODY where
 
   type PredicateFailure BBODY = BbodyPredicateFailure
 
+  data Event _
+    = BUPIEvent (Event BUPI)
+    | DelegationEvent (Event DELEG)
+    | UTXOWSEvent (Event UTXOWS)
+
   initialRules = []
 
   transitionRules =
@@ -93,9 +98,12 @@ instance STS BBODY where
 
 instance Embed BUPI BBODY where
   wrapFailed = BUPIFailure
+  wrapEvent = BUPIEvent
 
 instance Embed DELEG BBODY where
   wrapFailed = DelegationFailure
+  wrapEvent = DelegationEvent
 
 instance Embed UTXOWS BBODY where
   wrapFailed = UTXOWSFailure
+  wrapEvent = UTXOWSEvent

byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs

@@ -9,8 +9,8 @@ import           Data.Data (Data, Typeable)
 
 
 import           Control.State.Transition (Embed, Environment, PredicateFailure, STS, Signal, State,
-                     TRC (TRC), TransitionRule, initialRules, judgmentContext, trans,
-                     transitionRules, wrapFailed)
+                     TRC (TRC), TransitionRule, Event, initialRules, judgmentContext, trans,
+                     transitionRules, wrapFailed, wrapEvent)
 import           Byron.Spec.Ledger.Core (VKey)
 import           Byron.Spec.Ledger.Update (ProtVer, UPIEND, UPIEnv, UPIREG, UPIState, UPIVOTES, UProp, Vote)
 
@@ -39,6 +39,11 @@ instance STS BUPI where
 
   type PredicateFailure BUPI = BupiPredicateFailure
 
+  data Event _
+    = UPIREGEvent  (Event UPIREG)
+    | UPVOTESEvent (Event UPIVOTES)
+    | UPIENDEvent  (Event UPIEND)
+
   initialRules = []
 
   transitionRules =
@@ -67,9 +72,12 @@ instance STS BUPI where
 
 instance Embed UPIREG BUPI where
   wrapFailed = UPIREGFailure
+  wrapEvent = UPIREGEvent
 
 instance Embed UPIVOTES BUPI where
   wrapFailed = UPIVOTESFailure
+  wrapEvent = UPVOTESEvent
 
 instance Embed UPIEND BUPI where
   wrapFailed = UPIENDFailure
+  wrapEvent = UPIENDEvent

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

@@ -87,6 +87,16 @@ instance STS CHAIN where
 
   type PredicateFailure CHAIN = ChainPredicateFailure
 
+  data Event _
+   = UPIREGEvent           ( Event UPIREG   )
+   | UPVOTESEvent          ( Event UPIVOTES )
+   | UPIENDEvent           ( Event UPIEND   )
+   | EpochEvent            ( Event EPOCH    )
+   | BBodyEvent            ( Event BBODY    )
+   | PBFTEvent             ( Event PBFT     )
+   | LedgerDelegationEvent ( Event DELEG    )
+   | LedgerUTxOEvent       ( Event UTXOWS   )
+
   initialRules =
     [ do
         IRC (_sNow, utxo0', ads, pps', k) <- judgmentContext
@@ -162,18 +172,23 @@ instance STS CHAIN where
 
 instance Embed EPOCH CHAIN where
   wrapFailed = EpochFailure
+  wrapEvent = EpochEvent
 
 instance Embed BBODY CHAIN where
   wrapFailed = BBodyFailure
+  wrapEvent = BBodyEvent
 
 instance Embed PBFT CHAIN where
   wrapFailed = PBFTFailure
+  wrapEvent = PBFTEvent
 
 instance Embed DELEG CHAIN where
   wrapFailed = LedgerDelegationFailure
+  wrapEvent = LedgerDelegationEvent
 
 instance Embed UTXOWS CHAIN where
   wrapFailed = LedgerUTxOFailure
+  wrapEvent = LedgerUTxOEvent
 
 isHeaderSizeTooBigFailure :: PredicateFailure CHAIN -> Bool
 isHeaderSizeTooBigFailure (HeaderSizeTooBig _ _ _) = True

byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs

@@ -42,6 +42,8 @@ instance STS EPOCH where
   type Signal EPOCH = Slot
   type PredicateFailure EPOCH = EpochPredicateFailure
 
+  data Event _ = UPIECEvent (Event UPIEC)
+
   initialRules = []
 
   transitionRules =
@@ -57,3 +59,4 @@ instance STS EPOCH where
 
 instance Embed UPIEC EPOCH where
   wrapFailed = UPIECFailure
+  wrapEvent = UPIECEvent

byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs

@@ -43,6 +43,8 @@ instance STS PBFT where
 
   type PredicateFailure PBFT = PbftPredicateFailure
 
+  data Event _ = SigCountEvent (Event SIGCNT)
+
   initialRules = []
 
   transitionRules =
@@ -61,3 +63,4 @@ instance STS PBFT where
 
 instance Embed SIGCNT PBFT where
   wrapFailed = SigCountFailure
+  wrapEvent = SigCountEvent

byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/SigCnt.hs

@@ -44,6 +44,8 @@ instance STS SIGCNT where
   type Signal SIGCNT = VKey
   type PredicateFailure SIGCNT = SigcntPredicateFailure
 
+  data Event _
+
   initialRules = []
 
   transitionRules =

byron/crypto/test/Test/Cardano/Crypto/Limits.hs

@@ -45,7 +45,7 @@ tests = checkParallel $$discover
 --   is almost certainly amiss.
 
 newtype Limit t = Limit
-  { getLimit :: Word32 
+  { getLimit :: Word32
   } deriving (Eq, Ord, Show, Num, Enum, Real, Integral)
 
 instance Functor Limit where

byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs

@@ -114,7 +114,7 @@ import           Lens.Micro (Lens', lens, to, (%~), (&), (.~), (<>~), (^.), _1)
 import           Lens.Micro.TH (makeFields)
 import           NoThunks.Class (NoThunks (..), allNoThunks, noThunksInKeysAndValues)
 
-import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS,
+import           Control.State.Transition (Embed(..), Environment, IRC (IRC), PredicateFailure, STS(..),
                      Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
                      transitionRules, wrapFailed, (?!))
 import           Control.State.Transition.Generator (HasTrace, SignalGenerator, envGen, genTrace,
@@ -301,6 +301,7 @@ instance STS SDELEG where
   type Signal SDELEG = DCert
   type Environment SDELEG = DSEnv
   type PredicateFailure SDELEG = SdelegPredicateFailure
+  data Event _
 
   initialRules = [ return DSState
                    { _dSStateScheduledDelegations = []
@@ -374,6 +375,7 @@ instance STS ADELEG where
   type Signal ADELEG = (Slot, (VKeyGenesis, VKey))
   type Environment ADELEG = Set VKeyGenesis
   type PredicateFailure ADELEG = AdelegPredicateFailure
+  data Event _
 
 
   initialRules = [
@@ -433,6 +435,7 @@ instance STS SDELEGS where
   type Signal SDELEGS = [DCert]
   type Environment SDELEGS = DSEnv
   type PredicateFailure SDELEGS = SdelegsPredicateFailure
+  data Event _ = SDelegEvent (Event SDELEG)
 
   initialRules = [ do
                      IRC env <- judgmentContext
@@ -451,6 +454,7 @@ instance STS SDELEGS where
 
 instance Embed SDELEG SDELEGS where
   wrapFailed = SDelegFailure
+  wrapEvent = SDelegEvent
 
 -- | Delegation rules sequencing
 data ADELEGS deriving (Data, Typeable)
@@ -463,6 +467,7 @@ instance STS ADELEGS where
   type State ADELEGS = DState
   type Signal ADELEGS = [(Slot, (VKeyGenesis, VKey))]
   type Environment ADELEGS = Set VKeyGenesis
+  data Event _ = ADelegEvent (Event ADELEG)
 
   type PredicateFailure ADELEGS
     = AdelegsPredicateFailure
@@ -484,6 +489,7 @@ instance STS ADELEGS where
 
 instance Embed ADELEG ADELEGS where
   wrapFailed = ADelegFailure
+  wrapEvent = ADelegEvent
 
 -- | Delegation interface
 data DELEG deriving (Data, Typeable)
@@ -499,6 +505,9 @@ instance STS DELEG where
   type Environment DELEG = DIEnv
 
   type PredicateFailure DELEG = DelegPredicateFailure
+  data Event _
+    = SDelegSEvent (Event SDELEGS)
+    | ADelegSEvent (Event ADELEGS)
 
   initialRules = [ do
                      IRC env <- judgmentContext
@@ -528,9 +537,11 @@ instance STS DELEG where
 
 instance Embed SDELEGS DELEG where
   wrapFailed = SDelegSFailure
+  wrapEvent = SDelegSEvent
 
 instance Embed ADELEGS DELEG where
   wrapFailed = ADelegSFailure
+  wrapEvent = ADelegSEvent
 
 --------------------------------------------------------------------------------
 -- Generators
@@ -610,6 +621,7 @@ instance STS MSDELEG where
   type State MSDELEG = DSState
   type Signal MSDELEG = Maybe DCert
   type PredicateFailure MSDELEG = MsdelegPredicateFailure
+  data Event _ = SDELEGEvent (Event SDELEG)
 
   initialRules = []
 
@@ -623,6 +635,7 @@ instance STS MSDELEG where
 
 instance Embed SDELEG MSDELEG where
   wrapFailed = SDELEGFailure
+  wrapEvent = SDELEGEvent
 
 instance HasTrace MSDELEG where
 

byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXO.hs

@@ -27,7 +27,7 @@ import           Data.Data (Data, Typeable)
 import qualified Data.Set as Set
 import           GHC.Generics (Generic)
 
-import           Control.State.Transition (Environment, IRC (IRC), PredicateFailure, STS, Signal,
+import           Control.State.Transition (Environment, IRC (IRC), PredicateFailure, STS, Event, Signal,
                      State, TRC (TRC), initialRules, judgmentContext, transitionRules, (?!))
 import           Byron.Spec.Ledger.Core (Lovelace, dom, range, (∪), (⊆), (⋪), (◁))
 import           Byron.Spec.Ledger.GlobalParams (lovelaceCap)
@@ -70,6 +70,7 @@ instance STS UTXO where
   type State UTXO = UTxOState
   type Signal UTXO = Tx
   type PredicateFailure UTXO = UtxoPredicateFailure
+  data Event _
 
   initialRules =
     [ do

byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs

@@ -25,7 +25,7 @@ import qualified Hedgehog.Gen as Gen
 import           Hedgehog.Internal.Property (CoverPercentage)
 import qualified Hedgehog.Range as Range
 
-import           Control.State.Transition (Embed, Environment, IRC (IRC), STS (..),
+import           Control.State.Transition (Embed(..), Environment, IRC (IRC), STS (..),
                      Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
                      transitionRules, wrapFailed, (?!))
 import           Control.State.Transition.Generator (HasTrace, SignalGenerator, coverFailures,
@@ -58,6 +58,7 @@ instance STS UTXOW where
   type State UTXOW = UTxOState
   type Signal UTXOW = Tx
   type PredicateFailure UTXOW = UtxowPredicateFailure
+  data Event _ = UtxoEvent (Event UTXO)
 
   initialRules =
     [ do
@@ -93,6 +94,7 @@ witnessed (Tx tx wits) utxo =
 
 instance Embed UTXO UTXOW where
   wrapFailed = UtxoFailure
+  wrapEvent = UtxoEvent
 
 -- | Constant list of addresses intended to be used in the generators.
 traceAddrs :: [Addr]

byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs

@@ -20,9 +20,9 @@ import           GHC.Generics (Generic)
 import           Byron.Spec.Ledger.STS.UTXO (UTxOEnv, UTxOState)
 import           Byron.Spec.Ledger.STS.UTXOW (UTXOW)
 import           Byron.Spec.Ledger.UTxO (Tx)
-import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS,
+import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS(..),
                      Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
-                     transitionRules, wrapFailed)
+                     transitionRules, wrapFailed, wrapEvent)
 import           Control.State.Transition.Generator (HasTrace, envGen, genTrace, sigGen)
 import           Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)
 
@@ -37,6 +37,7 @@ instance STS UTXOWS where
   type Signal UTXOWS = [Tx]
   type Environment UTXOWS = UTxOEnv
   type PredicateFailure UTXOWS = UtxowsPredicateFailure
+  data Event _ = UtxowEvent (Event UTXOW)
 
   initialRules =
     [ do
@@ -57,6 +58,7 @@ instance STS UTXOWS where
 
 instance Embed UTXOW UTXOWS where
   wrapFailed = UtxowFailure
+  wrapEvent = UtxowEvent
 
 instance HasTrace UTXOWS where
   envGen = envGen @UTXOW