From e1318512ef0909394c9d4f3f1e65324133bc8dde Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Mon, 10 May 2021 18:07:02 -0400
Subject: [PATCH 01/22] hacky

---
 semantics/executable-spec/small-steps.cabal   |  1 +
 .../src/Control/State/Transition/Extended.hs  | 88 ++++++++++++++++---
 .../src/Shelley/Spec/Ledger/STS/Pool.hs       |  7 +-
 3 files changed, 83 insertions(+), 13 deletions(-)

diff --git a/semantics/executable-spec/small-steps.cabal b/semantics/executable-spec/small-steps.cabal
index 585e7e125a4..a26dac2e16e 100644
--- a/semantics/executable-spec/small-steps.cabal
+++ b/semantics/executable-spec/small-steps.cabal
@@ -69,6 +69,7 @@ library
                      , strict-containers
                      , text
                      , transformers >= 0.5
+                     , writer-cps-mtl
                      -- IOHK deps
                      , cardano-crypto-class
                      , cardano-binary
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index 9f072b0dd48..b7022a796ee 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -44,6 +44,7 @@ module Control.State.Transition.Extended
     judgmentContext,
     trans,
     liftSTS,
+    tellEvent,
 
     -- * Apply STS
     AssertionPolicy (..),
@@ -71,14 +72,16 @@ import Control.Monad (when)
 import Control.Monad.Except (MonadError (..))
 import Control.Monad.Free.Church
 import Control.Monad.Identity (Identity (..))
-import Control.Monad.Trans.Class (lift)
-import Control.Monad.Trans.State.Strict (modify, runStateT)
-import qualified Control.Monad.Trans.State.Strict as MonadState
+import Control.Monad.Trans.Class (lift, MonadTrans)
+import Control.Monad.Trans.State.Strict (StateT(..))
+import Control.Monad.Writer.CPS (WriterT, runWriterT)
+import Control.Monad.Writer.Class (MonadWriter (..))
+import Control.Monad.State.Class (MonadState (..), modify)
 import Data.Data (Data, Typeable)
 import Data.Default.Class (Default, def)
 import Data.Foldable (find, traverse_)
-import Data.Functor ((<&>))
-import Data.Kind (Type)
+import Data.Functor ((<&>), ($>))
+import Data.Kind (Type, Constraint)
 import Data.Proxy (Proxy (..))
 import Data.Typeable (typeRep)
 import NoThunks.Class (NoThunks (..))
@@ -219,6 +222,35 @@ class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
 instance STS sts => Embed sts sts where
   wrapFailed = id
 
+data Event
+
+data EventPolicy =
+    EventPolicyReturn
+  | EventPolicyDiscard
+
+data SingEP ep where
+  EPReturn  :: SingEP 'EventPolicyReturn
+  EPDiscard :: SingEP 'EventPolicyDiscard
+
+type family EventReturnType ep a :: Type where
+  EventReturnType 'EventPolicyReturn a = (a, [Event])
+  EventReturnType _ a = a
+
+type family EventConstraintType e m :: Constraint where
+  EventConstraintType 'EventPolicyReturn m = MonadWriter [Event] m
+  EventConstraintType _ _ = ()
+
+class InterpretEvent (ep :: EventPolicy) m where
+  interpretEvent :: EventConstraintType ep m => Event -> m ()
+
+instance Applicative m => InterpretEvent 'EventPolicyDiscard m where
+  {-# INLINE interpretEvent #-}
+  interpretEvent = const (pure ())
+
+instance InterpretEvent 'EventPolicyReturn (RuleInterpreterT s m) where
+  {-# INLINE interpretEvent #-}
+  interpretEvent = tell . pure
+
 data Clause sts (rtype :: RuleType) a where
   Lift ::
     STS sts =>
@@ -234,6 +266,10 @@ data Clause sts (rtype :: RuleType) a where
     -- Subsequent computation with state introduced
     (State sub -> a) ->
     Clause sts rtype a
+  Writer ::
+    Event ->
+    a ->
+    Clause sts rtype a
   Predicate ::
     [Label] ->
     Either e a ->
@@ -353,7 +389,7 @@ applySTSOpts ::
   m (State s, [[PredicateFailure s]])
 applySTSOpts ApplySTSOpts {asoAssertions, asoValidation} ctx =
   let goRule :: RuleInterpreter
-      goRule = applyRuleInternal asoValidation goSTS
+      goRule = applyRuleInternal EPDiscard asoValidation goSTS
       goSTS :: STSInterpreter
       goSTS = applySTSInternal asoAssertions goRule
    in goSTS ctx
@@ -416,22 +452,45 @@ applySTSIndifferently =
           asoValidation = ValidateAll
         }
 
+newtype RuleInterpreterT s m a = RuleInterpreterT (StateT [PredicateFailure s] (WriterT [Event] m) a)
+  deriving (MonadWriter [Event], Monad, Applicative, Functor)
+
+deriving instance (x ~ [PredicateFailure s], Monad m) => MonadState x (RuleInterpreterT s m)
+
+instance MonadTrans (RuleInterpreterT s) where
+  lift = RuleInterpreterT . lift . lift
+
+runRuleInterpreterT :: forall s m a. RuleInterpreterT s m a -> [PredicateFailure s] -> m ((a, [PredicateFailure s]), [Event])
+runRuleInterpreterT (RuleInterpreterT m) s = runWriterT $ runStateT m s 
+
 -- | Apply a rule even if its predicates fail.
 --
 --   If the rule successfully applied, the list of predicate failures will be
 --   empty.
 applyRuleInternal ::
-  forall s m rtype.
+  forall (ep :: EventPolicy) s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
+  SingEP ep ->
   ValidationPolicy ->
   -- | Interpreter for subsystems
   STSInterpreter ->
   RuleContext rtype s ->
   Rule s rtype (State s) ->
-  m (State s, [PredicateFailure s])
-applyRuleInternal vp goSTS jc r = flip runStateT [] $ foldF runClause r
+  m (EventReturnType ep (State s, [PredicateFailure s]))
+applyRuleInternal ep vp goSTS jc r = 
+  case ep of
+    EPReturn -> flip (runRuleInterpreterT @s) [] $ foldF runClause r
+    EPDiscard -> flip runStateT [] $ foldF runClause r
   where
-    runClause :: Clause s rtype a -> MonadState.StateT [PredicateFailure s] m a
+    runClause :: forall f t a.
+      ( f ~ t m
+      , MonadState [PredicateFailure s] f
+      , EventConstraintType ep f
+      , MonadTrans t
+      , InterpretEvent ep f
+      )
+      => Clause s rtype a
+      -> t m a
     runClause (Lift f next) = next <$> lift f
     runClause (GetCtx next) = pure $ next jc
     runClause (Predicate lbls cond orElse val) =
@@ -445,7 +504,8 @@ applyRuleInternal vp goSTS jc r = flip runStateT [] $ foldF runClause r
       (ss, sfails) <- lift $ goSTS subCtx
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
       pure $ next ss
-
+    runClause (Writer w a) = do
+      interpretEvent @ep w $> a
     validateIf lbls = case vp of
       ValidateAll -> True
       ValidateNone -> False
@@ -588,3 +648,9 @@ straverse_ f = foldr c (pure ())
 sfor_ :: (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
 {-# INLINE sfor_ #-}
 sfor_ = flip straverse_
+
+tellEvent ::
+  Event ->
+  Rule sts ctx ()
+tellEvent e = liftF $ Writer e ()
+
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
index 482d13dfefc..d69b0322319 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
@@ -37,6 +37,7 @@ import Control.State.Transition
     judgmentContext,
     liftSTS,
     (?!),
+    tellEvent,
   )
 import Data.Kind (Type)
 import Data.Typeable (Typeable)
@@ -176,13 +177,15 @@ poolDelegationTransition = do
 
       let hk = _poolId poolParam
       if eval (hk ∉ dom stpools)
-        then -- register new, Pool-Reg
-
+        then do 
+          -- register new, Pool-Reg
+          tellEvent NewPoolParam
           pure $
             ps
               { _pParams = eval (_pParams ps ∪ singleton hk poolParam)
               }
         else do
+          tellEvent NewFuturePoolParam
           pure $
             ps
               { _fPParams = eval (_fPParams ps ⨃ singleton hk poolParam),

From e493566568fb2eb08d0041cf13b235f4542d2a0d Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Mon, 10 May 2021 18:51:43 -0400
Subject: [PATCH 02/22] let it build

---
 .../src/Control/State/Transition/Extended.hs               | 5 ++++-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs    | 7 ++++---
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index b7022a796ee..caaf0cc7f4d 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -38,6 +38,7 @@ module Control.State.Transition.Extended
     (?!),
     (?!:),
     Label,
+    Event(..),
     labeledPred,
     labeledPredE,
     failBecause,
@@ -222,7 +223,9 @@ class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
 instance STS sts => Embed sts sts where
   wrapFailed = id
 
-data Event
+data Event 
+  = NewPoolParam
+  | NewFuturePoolParam
 
 data EventPolicy =
     EventPolicyReturn
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
index d69b0322319..50395881099 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
@@ -30,14 +30,15 @@ import Control.Monad (when)
 import Control.Monad.Trans.Reader (asks)
 import Control.SetAlgebra (dom, eval, setSingleton, singleton, (∈), (∉), (∪), (⋪), (⨃))
 import Control.State.Transition
-  ( STS (..),
+  ( Event (..),
+    STS (..),
     TRC (..),
     TransitionRule,
     failBecause,
     judgmentContext,
     liftSTS,
-    (?!),
     tellEvent,
+    (?!),
   )
 import Data.Kind (Type)
 import Data.Typeable (Typeable)
@@ -177,7 +178,7 @@ poolDelegationTransition = do
 
       let hk = _poolId poolParam
       if eval (hk ∉ dom stpools)
-        then do 
+        then do
           -- register new, Pool-Reg
           tellEvent NewPoolParam
           pure $

From f657264ae758bd0842f1053dcb03a77c5b2e2852 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Mon, 10 May 2021 19:32:26 -0400
Subject: [PATCH 03/22] exports

---
 alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs          | 2 +-
 .../executable-spec/src/Control/State/Transition/Extended.hs  | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
index 90fd53d291f..8d414d5a35f 100644
--- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
+++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
@@ -346,7 +346,7 @@ constructValidated globals env@(UtxoEnv _ pp _ _) st tx =
             _ -> throwError errs
   where
     runTransitionRule :: RuleInterpreter
-    runTransitionRule = applyRuleInternal ValidateAll runSTS
+    runTransitionRule = applyRuleInternal EPDiscard ValidateAll runSTS
     runSTS :: STSInterpreter
     runSTS = applySTSInternal AssertionsOff runTransitionRule
     utxo = _utxo st
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index caaf0cc7f4d..0468e23d11c 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -39,6 +39,10 @@ module Control.State.Transition.Extended
     (?!:),
     Label,
     Event(..),
+    SingEP(..),
+    EventPolicy(..),
+    EventReturnType,
+    EventConstraintType,
     labeledPred,
     labeledPredE,
     failBecause,

From bcb6b6ed43b6000c35f837eac3a2272b207d3264 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Tue, 11 May 2021 09:26:57 -0400
Subject: [PATCH 04/22] remove some typeclasses

---
 .../src/Control/State/Transition/Extended.hs    | 17 +++--------------
 1 file changed, 3 insertions(+), 14 deletions(-)

diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index 0468e23d11c..f30a4517465 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -247,17 +247,6 @@ type family EventConstraintType e m :: Constraint where
   EventConstraintType 'EventPolicyReturn m = MonadWriter [Event] m
   EventConstraintType _ _ = ()
 
-class InterpretEvent (ep :: EventPolicy) m where
-  interpretEvent :: EventConstraintType ep m => Event -> m ()
-
-instance Applicative m => InterpretEvent 'EventPolicyDiscard m where
-  {-# INLINE interpretEvent #-}
-  interpretEvent = const (pure ())
-
-instance InterpretEvent 'EventPolicyReturn (RuleInterpreterT s m) where
-  {-# INLINE interpretEvent #-}
-  interpretEvent = tell . pure
-
 data Clause sts (rtype :: RuleType) a where
   Lift ::
     STS sts =>
@@ -494,7 +483,6 @@ applyRuleInternal ep vp goSTS jc r =
       , MonadState [PredicateFailure s] f
       , EventConstraintType ep f
       , MonadTrans t
-      , InterpretEvent ep f
       )
       => Clause s rtype a
       -> t m a
@@ -511,8 +499,9 @@ applyRuleInternal ep vp goSTS jc r =
       (ss, sfails) <- lift $ goSTS subCtx
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
       pure $ next ss
-    runClause (Writer w a) = do
-      interpretEvent @ep w $> a
+    runClause (Writer w a) = case ep of
+      EPReturn -> tell [w] $> a
+      EPDiscard -> pure a
     validateIf lbls = case vp of
       ValidateAll -> True
       ValidateNone -> False

From 12e268575ac47c7611b816ac8a5b8f19549ce3ae Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Tue, 11 May 2021 13:53:44 -0400
Subject: [PATCH 05/22] style

---
 .../src/Control/State/Transition/Extended.hs  | 29 +++++++++++--------
 1 file changed, 17 insertions(+), 12 deletions(-)

diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index f30a4517465..21c82faf0c2 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -50,6 +50,7 @@ module Control.State.Transition.Extended
     trans,
     liftSTS,
     tellEvent,
+    tellEvents,
 
     -- * Apply STS
     AssertionPolicy (..),
@@ -231,8 +232,8 @@ data Event
   = NewPoolParam
   | NewFuturePoolParam
 
-data EventPolicy =
-    EventPolicyReturn
+data EventPolicy 
+  = EventPolicyReturn
   | EventPolicyDiscard
 
 data SingEP ep where
@@ -263,7 +264,7 @@ data Clause sts (rtype :: RuleType) a where
     (State sub -> a) ->
     Clause sts rtype a
   Writer ::
-    Event ->
+    [Event] ->
     a ->
     Clause sts rtype a
   Predicate ::
@@ -448,16 +449,16 @@ applySTSIndifferently =
           asoValidation = ValidateAll
         }
 
-newtype RuleInterpreterT s m a = RuleInterpreterT (StateT [PredicateFailure s] (WriterT [Event] m) a)
+newtype RuleEventLoggerT s m a = RuleEventLoggerT (StateT [PredicateFailure s] (WriterT [Event] m) a)
   deriving (MonadWriter [Event], Monad, Applicative, Functor)
 
-deriving instance (x ~ [PredicateFailure s], Monad m) => MonadState x (RuleInterpreterT s m)
+deriving instance (x ~ [PredicateFailure s], Monad m) => MonadState x (RuleEventLoggerT s m)
 
-instance MonadTrans (RuleInterpreterT s) where
-  lift = RuleInterpreterT . lift . lift
+instance MonadTrans (RuleEventLoggerT s) where
+  lift = RuleEventLoggerT . lift . lift
 
-runRuleInterpreterT :: forall s m a. RuleInterpreterT s m a -> [PredicateFailure s] -> m ((a, [PredicateFailure s]), [Event])
-runRuleInterpreterT (RuleInterpreterT m) s = runWriterT $ runStateT m s 
+runRuleEventLoggerT :: forall s m a. RuleEventLoggerT s m a -> [PredicateFailure s] -> m ((a, [PredicateFailure s]), [Event])
+runRuleEventLoggerT (RuleEventLoggerT m) s = runWriterT $ runStateT m s 
 
 -- | Apply a rule even if its predicates fail.
 --
@@ -475,7 +476,7 @@ applyRuleInternal ::
   m (EventReturnType ep (State s, [PredicateFailure s]))
 applyRuleInternal ep vp goSTS jc r = 
   case ep of
-    EPReturn -> flip (runRuleInterpreterT @s) [] $ foldF runClause r
+    EPReturn -> flip (runRuleEventLoggerT @s) [] $ foldF runClause r
     EPDiscard -> flip runStateT [] $ foldF runClause r
   where
     runClause :: forall f t a.
@@ -500,7 +501,7 @@ applyRuleInternal ep vp goSTS jc r =
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
       pure $ next ss
     runClause (Writer w a) = case ep of
-      EPReturn -> tell [w] $> a
+      EPReturn -> tell w $> a
       EPDiscard -> pure a
     validateIf lbls = case vp of
       ValidateAll -> True
@@ -648,5 +649,9 @@ sfor_ = flip straverse_
 tellEvent ::
   Event ->
   Rule sts ctx ()
-tellEvent e = liftF $ Writer e ()
+tellEvent e = tellEvents [e]
 
+tellEvents ::
+  [Event] ->
+  Rule sts ctx ()
+tellEvents es = liftF $ Writer es ()

From cd6526203d0dcc0f75d0adafb97f00c1280a7277 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Wed, 19 May 2021 15:44:02 -0400
Subject: [PATCH 06/22] push back event policy

---
 .../src/Cardano/Ledger/Alonzo/Rules/Utxos.hs  |  6 +-
 .../Cardano/Ledger/Rules/ValidationMode.hs    |  2 +-
 .../src/Control/State/Transition/Extended.hs  | 67 ++++++++++++-------
 .../src/Control/State/Transition/Trace.hs     |  2 +-
 .../src/Test/Shelley/Spec/Ledger/Utils.hs     |  2 +-
 5 files changed, 48 insertions(+), 31 deletions(-)

diff --git a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
index 8d414d5a35f..f20266ab9f1 100644
--- a/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
+++ b/alonzo/impl/src/Cardano/Ledger/Alonzo/Rules/Utxos.hs
@@ -345,10 +345,10 @@ constructValidated globals env@(UtxoEnv _ pp _ _) st tx =
             [] -> pure (newState, vTx)
             _ -> throwError errs
   where
-    runTransitionRule :: RuleInterpreter
+    runTransitionRule :: RuleInterpreter 'EventPolicyDiscard
     runTransitionRule = applyRuleInternal EPDiscard ValidateAll runSTS
-    runSTS :: STSInterpreter
-    runSTS = applySTSInternal AssertionsOff runTransitionRule
+    runSTS :: STSInterpreter 'EventPolicyDiscard
+    runSTS = applySTSInternal EPDiscard AssertionsOff runTransitionRule
     utxo = _utxo st
     sysS = systemStart globals
     ei = epochInfo globals
diff --git a/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs b/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
index 7ec8f0d9610..71db7af9059 100644
--- a/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
+++ b/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
@@ -28,7 +28,7 @@ applySTSValidateSuchThat ::
   RuleContext rtype s ->
   m (Either [[PredicateFailure s]] (State s))
 applySTSValidateSuchThat cond ctx =
-  applySTSOpts opts ctx <&> \case
+  applySTSOpts EPDiscard opts ctx <&> \case
     (st, []) -> Right st
     (_, pfs) -> Left pfs
   where
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index 21c82faf0c2..b6980e72b11 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -248,6 +248,11 @@ type family EventConstraintType e m :: Constraint where
   EventConstraintType 'EventPolicyReturn m = MonadWriter [Event] m
   EventConstraintType _ _ = ()
 
+discardEvents :: forall ep a. SingEP ep -> EventReturnType ep a -> a
+discardEvents ep = case ep of
+  EPReturn -> fst
+  EPDiscard -> id
+
 data Clause sts (rtype :: RuleType) a where
   Lift ::
     STS sts =>
@@ -363,32 +368,33 @@ data ApplySTSOpts = ApplySTSOpts
     asoValidation :: ValidationPolicy
   }
 
-type STSInterpreter =
+type STSInterpreter ep =
   forall s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
   RuleContext rtype s ->
-  m (State s, [[PredicateFailure s]])
+  m (EventReturnType ep (State s, [[PredicateFailure s]]))
 
-type RuleInterpreter =
+type RuleInterpreter ep =
   forall s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
   RuleContext rtype s ->
   Rule s rtype (State s) ->
-  m (State s, [PredicateFailure s])
+  m (EventReturnType ep (State s, [PredicateFailure s]))
 
 -- | Apply an STS with options. Note that this returns both the final state and
 -- the list of predicate failures.
 applySTSOpts ::
-  forall s m rtype.
+  forall s m rtype ep.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
+  SingEP ep ->
   ApplySTSOpts ->
   RuleContext rtype s ->
-  m (State s, [[PredicateFailure s]])
-applySTSOpts ApplySTSOpts {asoAssertions, asoValidation} ctx =
-  let goRule :: RuleInterpreter
-      goRule = applyRuleInternal EPDiscard asoValidation goSTS
-      goSTS :: STSInterpreter
-      goSTS = applySTSInternal asoAssertions goRule
+  m (EventReturnType ep (State s, [[PredicateFailure s]]))
+applySTSOpts ep ApplySTSOpts {asoAssertions, asoValidation} ctx =
+  let goRule :: RuleInterpreter ep
+      goRule = applyRuleInternal ep asoValidation goSTS
+      goSTS :: STSInterpreter ep
+      goSTS = applySTSInternal ep asoAssertions goRule
    in goSTS ctx
 
 applySTS ::
@@ -397,7 +403,7 @@ applySTS ::
   RuleContext rtype s ->
   m (Either [[PredicateFailure s]] (State s))
 applySTS ctx =
-  applySTSOpts defaultOpts ctx <&> \case
+  applySTSOpts EPDiscard defaultOpts ctx <&> \case
     (st, []) -> Right st
     (_, pfs) -> Left pfs
   where
@@ -427,7 +433,7 @@ reapplySTS ::
   RuleContext rtype s ->
   m (State s)
 reapplySTS ctx =
-  applySTSOpts defaultOpts ctx <&> fst
+  applySTSOpts EPDiscard defaultOpts ctx <&> fst
   where
     defaultOpts =
       ApplySTSOpts
@@ -441,7 +447,7 @@ applySTSIndifferently ::
   RuleContext rtype s ->
   m (State s, [[PredicateFailure s]])
 applySTSIndifferently =
-  applySTSOpts opts
+  applySTSOpts EPDiscard opts
   where
     opts =
       ApplySTSOpts
@@ -470,7 +476,7 @@ applyRuleInternal ::
   SingEP ep ->
   ValidationPolicy ->
   -- | Interpreter for subsystems
-  STSInterpreter ->
+  STSInterpreter ep ->
   RuleContext rtype s ->
   Rule s rtype (State s) ->
   m (EventReturnType ep (State s, [PredicateFailure s]))
@@ -497,7 +503,10 @@ applyRuleInternal ep vp goSTS jc r =
             Right x -> pure x
         else pure val
     runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do
-      (ss, sfails) <- lift $ goSTS subCtx
+      s <- lift $ goSTS subCtx
+      let ss :: State sub
+          sfails :: [[PredicateFailure sub]]
+          (ss, sfails) = discardEvents ep s
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
       pure $ next ss
     runClause (Writer w a) = case ep of
@@ -509,28 +518,36 @@ applyRuleInternal ep vp goSTS jc r =
       ValidateSuchThat f -> f lbls
 
 applySTSInternal ::
-  forall s m rtype.
+  forall s m rtype ep.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
+  SingEP ep ->
   AssertionPolicy ->
   -- | Interpreter for rules
-  RuleInterpreter ->
+  RuleInterpreter ep ->
   RuleContext rtype s ->
-  m (State s, [[PredicateFailure s]])
-applySTSInternal ap goRule ctx =
+  m (EventReturnType ep (State s, [[PredicateFailure s]]))
+applySTSInternal ep ap goRule ctx =
   successOrFirstFailure <$> applySTSInternal' rTypeRep ctx
   where
+    successOrFirstFailure :: 
+         [EventReturnType ep (State s, [PredicateFailure s])] 
+      -> EventReturnType ep (State s, [[PredicateFailure s]])
     successOrFirstFailure xs =
-      case find (null . snd) xs of
+      case find (\x -> null $ snd $ (discardEvents ep x :: (State s, [PredicateFailure s]))) xs of
         Nothing ->
           case xs of
             [] -> error "applySTSInternal was called with an empty set of rules"
-            (s, _) : _ -> (s, snd <$> xs)
-        Just (s, _) -> (s, [])
+            s' : _ -> case ep of 
+              EPDiscard -> (fst s', snd <$> xs)
+              EPReturn -> ((fst $ fst s', (snd . fst) <$> xs), snd s')
+        Just s' -> case ep of
+          EPDiscard -> (fst s', [])
+          EPReturn -> ((fst $ fst s', []), snd s')
 
     applySTSInternal' ::
       SRuleType rtype ->
       RuleContext rtype s ->
-      m [(State s, [PredicateFailure s])]
+      m [EventReturnType ep (State s, [PredicateFailure s])]
     applySTSInternal' SInitial env =
       goRule env `traverse` initialRules
     applySTSInternal' STransition jc = do
@@ -555,7 +572,7 @@ applySTSInternal ap goRule ctx =
       res <- goRule jc `traverse` transitionRules
       -- We only care about running postconditions if the state transition was
       -- successful.
-      !_ <- case (assertPost ap, successOrFirstFailure res) of
+      !_ <- case (assertPost ap, discardEvents ep (successOrFirstFailure res) :: (State s, [[PredicateFailure s]])) of
         (True, (st, [])) ->
           sfor_ (assertions @s)
             $! ( \case
diff --git a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
index 41372eeb192..1e0f6443e61 100644
--- a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
+++ b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
@@ -495,7 +495,7 @@ applySTSTest ::
   RuleContext rtype s ->
   m (Either [[PredicateFailure s]] (State s))
 applySTSTest ctx =
-  applySTSOpts defaultOpts ctx <&> \case
+  applySTSOpts EPDiscard defaultOpts ctx <&> \case
     (st, []) -> Right st
     (_, pfs) -> Left pfs
   where
diff --git a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
index a178b291711..f82060457b4 100644
--- a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
+++ b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
@@ -326,7 +326,7 @@ applySTSTest ::
   RuleContext rtype s ->
   m (Either [[PredicateFailure s]] (State s))
 applySTSTest ctx =
-  applySTSOpts defaultOpts ctx <&> \case
+  applySTSOpts EPDiscard defaultOpts ctx <&> \case
     (st, []) -> Right st
     (_, pfs) -> Left pfs
   where

From 4facc36f281456a5c9c3f9707715f8079a1c6508 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Thu, 20 May 2021 18:49:17 -0400
Subject: [PATCH 07/22] add Event to STS typeclass

---
 .../src/Byron/Spec/Chain/STS/Rule/BBody.hs    | 14 +++-
 .../src/Byron/Spec/Chain/STS/Rule/Bupi.hs     | 12 +++-
 .../src/Byron/Spec/Chain/STS/Rule/Chain.hs    | 15 ++++
 .../src/Byron/Spec/Chain/STS/Rule/Epoch.hs    |  3 +
 .../src/Byron/Spec/Chain/STS/Rule/Pbft.hs     |  3 +
 .../src/Byron/Spec/Chain/STS/Rule/SigCnt.hs   |  2 +
 .../src/Byron/Spec/Ledger/Delegation.hs       | 15 +++-
 .../src/Byron/Spec/Ledger/STS/UTXO.hs         |  3 +-
 .../src/Byron/Spec/Ledger/STS/UTXOW.hs        |  4 +-
 .../src/Byron/Spec/Ledger/STS/UTXOWS.hs       |  6 +-
 .../src/Byron/Spec/Ledger/Update.hs           | 32 ++++++++-
 .../Spec/Ledger/Delegation/Properties.hs      |  7 +-
 .../Byron/Spec/Ledger/Update/Properties.hs    | 12 +++-
 .../src/Control/State/Transition/Extended.hs  | 69 ++++++++++---------
 .../src/Shelley/Spec/Ledger/STS/Bbody.hs      |  3 +
 .../src/Shelley/Spec/Ledger/STS/Chain.hs      | 10 +++
 .../src/Shelley/Spec/Ledger/STS/Deleg.hs      |  1 +
 .../src/Shelley/Spec/Ledger/STS/Delegs.hs     |  2 +
 .../src/Shelley/Spec/Ledger/STS/Delpl.hs      |  5 ++
 .../src/Shelley/Spec/Ledger/STS/Epoch.hs      |  7 ++
 .../src/Shelley/Spec/Ledger/STS/Ledger.hs     |  5 ++
 .../src/Shelley/Spec/Ledger/STS/Ledgers.hs    |  2 +
 .../src/Shelley/Spec/Ledger/STS/Mir.hs        |  1 +
 .../src/Shelley/Spec/Ledger/STS/NewEpoch.hs   |  6 ++
 .../src/Shelley/Spec/Ledger/STS/Newpp.hs      |  1 +
 .../src/Shelley/Spec/Ledger/STS/Ocert.hs      |  1 +
 .../src/Shelley/Spec/Ledger/STS/Overlay.hs    |  4 ++
 .../src/Shelley/Spec/Ledger/STS/Pool.hs       |  7 +-
 .../src/Shelley/Spec/Ledger/STS/PoolReap.hs   |  1 +
 .../src/Shelley/Spec/Ledger/STS/Ppup.hs       |  1 +
 .../src/Shelley/Spec/Ledger/STS/Prtcl.hs      |  6 ++
 .../src/Shelley/Spec/Ledger/STS/Rupd.hs       |  1 +
 .../src/Shelley/Spec/Ledger/STS/Snap.hs       |  1 +
 .../src/Shelley/Spec/Ledger/STS/Tick.hs       |  8 +++
 .../src/Shelley/Spec/Ledger/STS/Tickn.hs      |  1 +
 .../src/Shelley/Spec/Ledger/STS/Updn.hs       |  1 +
 .../src/Shelley/Spec/Ledger/STS/Upec.hs       |  3 +
 .../src/Shelley/Spec/Ledger/STS/Utxo.hs       |  4 +-
 .../src/Shelley/Spec/Ledger/STS/Utxow.hs      |  4 +-
 39 files changed, 233 insertions(+), 50 deletions(-)

diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs
index 5c437e143e1..2444f1b7ffd 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs
+++ b/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,
-                     (?!))
+                     (?!), wrapEvents)
 
 import           Byron.Spec.Chain.STS.Block
 
@@ -33,8 +33,8 @@ data BbodyPredicateFailure
   | InvalidUtxoHash
   | InvalidDelegationHash
   | InvalidUpdateProposalHash
-  | BUPIFailure (PredicateFailure BUPI)
-  | DelegationFailure (PredicateFailure DELEG)
+  | BUPIFailure (PredicateFailure BUPI)         
+  | DelegationFailure (PredicateFailure DELEG)  
   | UTXOWSFailure (PredicateFailure UTXOWS)
   deriving (Eq, Show, Data, Typeable)
 
@@ -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
+  wrapEvents = BUPIEvent
 
 instance Embed DELEG BBODY where
   wrapFailed = DelegationFailure
+  wrapEvents = DelegationEvent
 
 instance Embed UTXOWS BBODY where
   wrapFailed = UTXOWSFailure
+  wrapEvents = UTXOWSEvent
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs
index e704796632a..cad4214a780 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs
+++ b/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, wrapEvents)
 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
+  wrapEvents = UPIREGEvent
 
 instance Embed UPIVOTES BUPI where
   wrapFailed = UPIVOTESFailure
+  wrapEvents = UPVOTESEvent
 
 instance Embed UPIEND BUPI where
   wrapFailed = UPIENDFailure
+  wrapEvents = UPIENDEvent
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs
index b7b3ad52ec4..8a09609b9d4 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs
+++ b/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
+  wrapEvents = EpochEvent
 
 instance Embed BBODY CHAIN where
   wrapFailed = BBodyFailure
+  wrapEvents = BBodyEvent
 
 instance Embed PBFT CHAIN where
   wrapFailed = PBFTFailure
+  wrapEvents = PBFTEvent
 
 instance Embed DELEG CHAIN where
   wrapFailed = LedgerDelegationFailure
+  wrapEvents = LedgerDelegationEvent
 
 instance Embed UTXOWS CHAIN where
   wrapFailed = LedgerUTxOFailure
+  wrapEvents = LedgerUTxOEvent
 
 isHeaderSizeTooBigFailure :: PredicateFailure CHAIN -> Bool
 isHeaderSizeTooBigFailure (HeaderSizeTooBig _ _ _) = True
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs
index 7f08ae732fb..1fd8a675dda 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs
+++ b/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
+  wrapEvents = UPIECEvent
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs
index fcd43800f92..ce535e44326 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs
+++ b/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
+  wrapEvents = SigCountEvent
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/SigCnt.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/SigCnt.hs
index a042a32707b..b3630d25059 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/SigCnt.hs
+++ b/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 =
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs
index 4d972895d2c..dc782d874e6 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs
+++ b/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
+  wrapEvents = 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
+  wrapEvents = 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
+  wrapEvents = SDelegSEvent
 
 instance Embed ADELEGS DELEG where
   wrapFailed = ADelegSFailure
+  wrapEvents = 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
+  wrapEvents = SDELEGEvent
 
 instance HasTrace MSDELEG where
 
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXO.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXO.hs
index d626f5b01d2..fdab458960e 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXO.hs
+++ b/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
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs
index 439081c6451..2ee0706ae56 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs
+++ b/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
+  wrapEvents = UtxoEvent
 
 -- | Constant list of addresses intended to be used in the generators.
 traceAddrs :: [Addr]
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs
index c87834773bc..42b9c3b3ffc 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs
+++ b/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, wrapEvents)
 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
+  wrapEvents = UtxowEvent
 
 instance HasTrace UTXOWS where
   envGen = envGen @UTXOW
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
index 1c22a5421af..1445e86f2d1 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
+++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
@@ -385,6 +385,7 @@ instance STS UPSVV where
   type State UPSVV = Map UpId (ApName, ApVer, Metadata)
   type Signal UPSVV = UProp
   type PredicateFailure UPSVV = UpsvvPredicateFailure
+  data Event _
 
   initialRules = []
   transitionRules =
@@ -423,6 +424,7 @@ instance STS UPPVV where
   type State UPPVV = Map UpId (ProtVer, PParams)
   type Signal UPPVV = UProp
   type PredicateFailure UPPVV = UppvvPredicateFailure
+  data Event _
 
   initialRules = []
   transitionRules =
@@ -464,7 +466,10 @@ instance STS UPV where
 
   type Signal UPV = UProp
   type PredicateFailure UPV = UpvPredicateFailure
-
+  
+  data Event _ 
+    = UPPVVEvent (Event UPPVV)
+    | UPSVVEvent (Event UPSVV)
 
   initialRules = []
   transitionRules =
@@ -500,9 +505,11 @@ instance STS UPV where
 
 instance Embed UPPVV UPV where
   wrapFailed = UPPVVFailure
+  wrapEvents = UPPVVEvent
 
 instance Embed UPSVV UPV where
   wrapFailed = UPSVVFailure
+  wrapEvents = UPSVVEvent
 
 data UPREG deriving (Generic, Data, Typeable)
 -- | These `PredicateFailure`s are all throwable.
@@ -525,6 +532,8 @@ instance STS UPREG where
     )
   type Signal UPREG = UProp
   type PredicateFailure UPREG = UpregPredicateFailure
+  data Event _
+    = UPVEvent (Event UPV)
 
   initialRules = []
   transitionRules =
@@ -544,6 +553,7 @@ instance STS UPREG where
 
 instance Embed UPV UPREG where
   wrapFailed = UPVFailure
+  wrapEvents = UPVEvent
 
 ------------------------------------------------------------------------
 -- Update voting
@@ -592,6 +602,7 @@ instance STS ADDVOTE where
   type State ADDVOTE = Set (UpId, Core.VKeyGenesis)
   type Signal ADDVOTE = Vote
   type PredicateFailure ADDVOTE = AddvotePredicateFailure
+  data Event _
 
   initialRules = []
   transitionRules =
@@ -638,6 +649,7 @@ instance STS UPVOTE where
     )
   type Signal UPVOTE = Vote
   type PredicateFailure UPVOTE = UpvotePredicateFailure
+  data Event _ = ADDVOTEEvent (Event ADDVOTE)
 
   initialRules = []
   transitionRules =
@@ -669,6 +681,7 @@ instance STS UPVOTE where
 
 instance Embed ADDVOTE UPVOTE where
   wrapFailed = ADDVOTEFailure
+  wrapEvents = ADDVOTEEvent
 
 ------------------------------------------------------------------------
 -- Update voting
@@ -684,6 +697,7 @@ instance STS FADS where
   type State FADS = [(Core.Slot, (ProtVer, PParams))]
   type Signal FADS = (Core.Slot, (ProtVer, PParams))
   type PredicateFailure FADS = FadsPredicateFailure
+  data Event _
 
   initialRules = []
   transitionRules =
@@ -739,6 +753,7 @@ instance STS UPEND where
     )
   type Signal UPEND = (ProtVer, Core.VKey)
   type PredicateFailure UPEND = UpendPredicateFailure
+  data Event _ = FADSEvent (Event FADS)
 
   initialRules = []
   transitionRules =
@@ -810,6 +825,7 @@ instance STS UPEND where
 
 instance Embed FADS UPEND where
   wrapFailed = error "No possible failures in FADS"
+  wrapEvents = FADSEvent
 
 ------------------------------------------------------------------------
 -- Update interface
@@ -948,6 +964,7 @@ instance STS UPIREG where
   type State UPIREG = UPIState
   type Signal UPIREG = UProp
   type PredicateFailure UPIREG = UpiregPredicateFailure
+  data Event _ = UPREGEvent (Event UPREG)
 
   initialRules = [ return $! emptyUPIState ]
 
@@ -981,6 +998,7 @@ instance STS UPIREG where
 
 instance Embed UPREG UPIREG where
   wrapFailed = UPREGFailure
+  wrapEvents = UPREGEvent
 
 instance HasTrace UPIREG where
 
@@ -1324,6 +1342,7 @@ instance STS UPIVOTE where
   type State UPIVOTE = UPIState
   type Signal UPIVOTE = Vote
   type PredicateFailure UPIVOTE = UpivotePredicateFailure
+  data Event _ = UPVOTEEvent (Event UPVOTE)
 
   initialRules = []
   transitionRules =
@@ -1364,6 +1383,7 @@ instance STS UPIVOTE where
 
 instance Embed UPVOTE UPIVOTE where
   wrapFailed = UPVOTEFailure
+  wrapEvents = UPVOTEEvent
 
 
 data APPLYVOTES deriving (Generic, Data, Typeable)
@@ -1377,6 +1397,7 @@ instance STS APPLYVOTES where
   type State APPLYVOTES = UPIState
   type Signal APPLYVOTES = [Vote]
   type PredicateFailure APPLYVOTES = ApplyVotesPredicateFailure
+  data Event _ = UpivoteEvent (Event UPIVOTE)
 
   initialRules = [ return $! emptyUPIState ]
 
@@ -1393,6 +1414,7 @@ instance STS APPLYVOTES where
 
 instance Embed UPIVOTE APPLYVOTES where
   wrapFailed = UpivoteFailure
+  wrapEvents = UpivoteEvent
 
 data UPIVOTES deriving (Generic, Data, Typeable)
 
@@ -1405,6 +1427,7 @@ instance STS UPIVOTES where
   type State UPIVOTES = UPIState
   type Signal UPIVOTES = [Vote]
   type PredicateFailure UPIVOTES = UpivotesPredicateFailure
+  data Event _ = ApplyVotesEvent (Event APPLYVOTES)
 
   initialRules = [ return $! emptyUPIState ]
 
@@ -1451,6 +1474,7 @@ instance STS UPIVOTES where
 
 instance Embed APPLYVOTES UPIVOTES where
   wrapFailed = ApplyVotesFailure
+  wrapEvents = ApplyVotesEvent
 
 instance HasTrace UPIVOTES where
 
@@ -1551,6 +1575,7 @@ instance STS UPIEND where
   type State UPIEND = UPIState
   type Signal UPIEND = (ProtVer, Core.VKey)
   type PredicateFailure UPIEND = UpiendPredicateFailure
+  data Event _ = UPENDEvent (Event UPEND)
 
   initialRules = [ return $! emptyUPIState ]
 
@@ -1590,6 +1615,7 @@ instance STS UPIEND where
 
 instance Embed UPEND UPIEND where
   wrapFailed = UPENDFailure
+  wrapEvents = UPENDEvent
 
 -- | Given a list of protocol versions and keys endorsing those versions,
 -- generate a protocol-version endorsement, or 'Nothing' if the list of
@@ -1632,6 +1658,8 @@ instance STS PVBUMP where
   type Signal PVBUMP = ()
   type PredicateFailure PVBUMP = PvbumpPredicateFailure
 
+  data Event _
+
   initialRules = []
   transitionRules =
     [ do
@@ -1660,6 +1688,7 @@ instance STS UPIEC where
   type State UPIEC = UPIState
   type Signal UPIEC = ()
   type PredicateFailure UPIEC = UpiecPredicateFailure
+  data Event _ = PVBUMPEvent (Event PVBUMP)
 
   initialRules = []
   transitionRules =
@@ -1691,6 +1720,7 @@ instance STS UPIEC where
 
 instance Embed PVBUMP UPIEC where
   wrapFailed = PVBUMPFailure
+  wrapEvents = PVBUMPEvent
 
 -- | Generate an optional update-proposal and a list of votes, given an update
 -- environment and state.
diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
index 15006d60784..895abdaf76e 100644
--- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
+++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
@@ -40,8 +40,8 @@ import           Lens.Micro.Extras (view)
 import           Lens.Micro.TH (makeLenses)
 
 import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS,
-                     Signal, State, TRC (TRC), applySTS, initialRules, judgmentContext, trans,
-                     transitionRules, wrapFailed, (?!))
+                     Signal, State, TRC (TRC), Event, applySTS, initialRules, judgmentContext, trans,
+                     transitionRules, wrapFailed, (?!), wrapEvents)
 import           Control.State.Transition.Generator (HasSizeInfo, HasTrace, SignalGenerator,
                      TraceProfile (TraceProfile), classifySize, classifyTraceLength, envGen,
                      failures, isTrivial, nonTrivialTrace, proportionOfValidSignals, sigGen,
@@ -109,6 +109,8 @@ instance STS DBLOCK where
   type State DBLOCK = (DSEnv, DIState)
   type Signal DBLOCK = DBlock
   type PredicateFailure DBLOCK = DBlockPredicateFailure
+  data Event _ = 
+    DELEGEvent (Event DELEG)
 
   initialRules
     = [ do
@@ -132,6 +134,7 @@ instance STS DBLOCK where
 
 instance Embed DELEG DBLOCK where
   wrapFailed = DPF
+  wrapEvents = DELEGEvent
 
 -- | Check that all the delegation certificates in the trace were correctly
 -- applied.
diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs
index 95543ed0748..d0b936dfa3a 100644
--- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs
+++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs
@@ -34,9 +34,9 @@ import qualified Hedgehog.Gen as Gen
 import qualified Hedgehog.Range as Range
 import           Numeric.Natural (Natural)
 
-import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS,
+import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS, Event,
                      Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
-                     transitionRules, wrapFailed, (?!))
+                     transitionRules, wrapFailed, (?!), wrapEvents)
 import           Control.State.Transition.Generator (HasTrace, SignalGenerator, envGen,
                      randomTraceOfSize, ratio, sigGen, trace, traceLengthsAreClassified,
                      traceOfLength)
@@ -305,6 +305,11 @@ instance STS UBLOCK where
 
   type PredicateFailure UBLOCK = UBlockPredicateFailure
 
+  data Event _
+    = UPIREGEvent (Event UPIREG)
+    | UPIVOTESEvent (Event UPIVOTES)
+    | UPIENDEvent (Event UPIEND)
+
   initialRules
     = [ do
           IRC env <- judgmentContext
@@ -351,12 +356,15 @@ instance STS UBLOCK where
 
 instance Embed UPIREG UBLOCK where
   wrapFailed = UPIREGFailure
+  wrapEvents = UPIREGEvent
 
 instance Embed UPIVOTES UBLOCK where
   wrapFailed = UPIVOTESFailure
+  wrapEvents = UPIVOTESEvent
 
 instance Embed UPIEND UBLOCK where
   wrapFailed = UPIENDFailure
+  wrapEvents = UPIENDEvent
 
 instance HasTrace UBLOCK where
   envGen _ =
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index b6980e72b11..8e38666035b 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -38,7 +38,6 @@ module Control.State.Transition.Extended
     (?!),
     (?!:),
     Label,
-    Event(..),
     SingEP(..),
     EventPolicy(..),
     EventReturnType,
@@ -187,6 +186,12 @@ class
 
   type BaseM a = Identity
 
+  -- | Event type.
+  data Event a :: Type
+
+  -- type Event a :: Type
+  -- type Event a = Void
+
   -- | Descriptive type for the possible failures which might cause a transition
   -- to fail.
   --
@@ -224,13 +229,11 @@ class
 class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
   -- | Wrap a predicate failure of the subsystem in a failure of the super-system.
   wrapFailed :: PredicateFailure sub -> PredicateFailure super
+  wrapEvents :: Event sub -> Event super
 
 instance STS sts => Embed sts sts where
   wrapFailed = id
-
-data Event 
-  = NewPoolParam
-  | NewFuturePoolParam
+  wrapEvents = id
 
 data EventPolicy 
   = EventPolicyReturn
@@ -240,15 +243,15 @@ data SingEP ep where
   EPReturn  :: SingEP 'EventPolicyReturn
   EPDiscard :: SingEP 'EventPolicyDiscard
 
-type family EventReturnType ep a :: Type where
-  EventReturnType 'EventPolicyReturn a = (a, [Event])
-  EventReturnType _ a = a
+type family EventReturnType ep sts a :: Type where
+  EventReturnType 'EventPolicyReturn sts a = (a, [Event sts])
+  EventReturnType _ _ a = a
 
-type family EventConstraintType e m :: Constraint where
-  EventConstraintType 'EventPolicyReturn m = MonadWriter [Event] m
-  EventConstraintType _ _ = ()
+type family EventConstraintType e sts m :: Constraint where
+  EventConstraintType 'EventPolicyReturn sts m = MonadWriter [Event sts] m
+  EventConstraintType _ _ _ = ()
 
-discardEvents :: forall ep a. SingEP ep -> EventReturnType ep a -> a
+discardEvents :: forall ep a. SingEP ep -> forall s. EventReturnType ep s a -> a
 discardEvents ep = case ep of
   EPReturn -> fst
   EPDiscard -> id
@@ -269,7 +272,7 @@ data Clause sts (rtype :: RuleType) a where
     (State sub -> a) ->
     Clause sts rtype a
   Writer ::
-    [Event] ->
+    [Event sts] ->
     a ->
     Clause sts rtype a
   Predicate ::
@@ -372,14 +375,14 @@ type STSInterpreter ep =
   forall s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
   RuleContext rtype s ->
-  m (EventReturnType ep (State s, [[PredicateFailure s]]))
+  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
 
 type RuleInterpreter ep =
   forall s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
   RuleContext rtype s ->
   Rule s rtype (State s) ->
-  m (EventReturnType ep (State s, [PredicateFailure s]))
+  m (EventReturnType ep s (State s, [PredicateFailure s]))
 
 -- | Apply an STS with options. Note that this returns both the final state and
 -- the list of predicate failures.
@@ -389,7 +392,7 @@ applySTSOpts ::
   SingEP ep ->
   ApplySTSOpts ->
   RuleContext rtype s ->
-  m (EventReturnType ep (State s, [[PredicateFailure s]]))
+  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
 applySTSOpts ep ApplySTSOpts {asoAssertions, asoValidation} ctx =
   let goRule :: RuleInterpreter ep
       goRule = applyRuleInternal ep asoValidation goSTS
@@ -455,15 +458,15 @@ applySTSIndifferently =
           asoValidation = ValidateAll
         }
 
-newtype RuleEventLoggerT s m a = RuleEventLoggerT (StateT [PredicateFailure s] (WriterT [Event] m) a)
-  deriving (MonadWriter [Event], Monad, Applicative, Functor)
+newtype RuleEventLoggerT s m a = RuleEventLoggerT (StateT [PredicateFailure s] (WriterT [Event s] m) a)
+  deriving (MonadWriter [Event s], Monad, Applicative, Functor)
 
 deriving instance (x ~ [PredicateFailure s], Monad m) => MonadState x (RuleEventLoggerT s m)
 
 instance MonadTrans (RuleEventLoggerT s) where
   lift = RuleEventLoggerT . lift . lift
 
-runRuleEventLoggerT :: forall s m a. RuleEventLoggerT s m a -> [PredicateFailure s] -> m ((a, [PredicateFailure s]), [Event])
+runRuleEventLoggerT :: forall s m a. RuleEventLoggerT s m a -> [PredicateFailure s] -> m ((a, [PredicateFailure s]), [Event s])
 runRuleEventLoggerT (RuleEventLoggerT m) s = runWriterT $ runStateT m s 
 
 -- | Apply a rule even if its predicates fail.
@@ -479,7 +482,7 @@ applyRuleInternal ::
   STSInterpreter ep ->
   RuleContext rtype s ->
   Rule s rtype (State s) ->
-  m (EventReturnType ep (State s, [PredicateFailure s]))
+  m (EventReturnType ep s (State s, [PredicateFailure s]))
 applyRuleInternal ep vp goSTS jc r = 
   case ep of
     EPReturn -> flip (runRuleEventLoggerT @s) [] $ foldF runClause r
@@ -488,7 +491,7 @@ applyRuleInternal ep vp goSTS jc r =
     runClause :: forall f t a.
       ( f ~ t m
       , MonadState [PredicateFailure s] f
-      , EventConstraintType ep f
+      , EventConstraintType ep s f
       , MonadTrans t
       )
       => Clause s rtype a
@@ -503,11 +506,14 @@ applyRuleInternal ep vp goSTS jc r =
             Right x -> pure x
         else pure val
     runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do
-      s <- lift $ goSTS subCtx
+      s :: (EventReturnType ep sub (State sub, [[PredicateFailure sub]])) <- lift $ goSTS subCtx
       let ss :: State sub
           sfails :: [[PredicateFailure sub]]
-          (ss, sfails) = discardEvents ep s
+          (ss, sfails) = (discardEvents ep @sub) s
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
+      () <- case ep of
+        EPDiscard -> pure ()
+        EPReturn -> tell (wrapEvents <$> snd s)
       pure $ next ss
     runClause (Writer w a) = case ep of
       EPReturn -> tell w $> a
@@ -525,15 +531,15 @@ applySTSInternal ::
   -- | Interpreter for rules
   RuleInterpreter ep ->
   RuleContext rtype s ->
-  m (EventReturnType ep (State s, [[PredicateFailure s]]))
+  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
 applySTSInternal ep ap goRule ctx =
   successOrFirstFailure <$> applySTSInternal' rTypeRep ctx
   where
     successOrFirstFailure :: 
-         [EventReturnType ep (State s, [PredicateFailure s])] 
-      -> EventReturnType ep (State s, [[PredicateFailure s]])
+         [EventReturnType ep s (State s, [PredicateFailure s])] 
+      -> EventReturnType ep s (State s, [[PredicateFailure s]])
     successOrFirstFailure xs =
-      case find (\x -> null $ snd $ (discardEvents ep x :: (State s, [PredicateFailure s]))) xs of
+      case find (\x -> null $ snd $ (discardEvents ep @s x :: (State s, [PredicateFailure s]))) xs of
         Nothing ->
           case xs of
             [] -> error "applySTSInternal was called with an empty set of rules"
@@ -547,7 +553,7 @@ applySTSInternal ep ap goRule ctx =
     applySTSInternal' ::
       SRuleType rtype ->
       RuleContext rtype s ->
-      m [EventReturnType ep (State s, [PredicateFailure s])]
+      m [EventReturnType ep s (State s, [PredicateFailure s])]
     applySTSInternal' SInitial env =
       goRule env `traverse` initialRules
     applySTSInternal' STransition jc = do
@@ -572,7 +578,7 @@ applySTSInternal ep ap goRule ctx =
       res <- goRule jc `traverse` transitionRules
       -- We only care about running postconditions if the state transition was
       -- successful.
-      !_ <- case (assertPost ap, discardEvents ep (successOrFirstFailure res) :: (State s, [[PredicateFailure s]])) of
+      !_ <- case (assertPost ap, discardEvents ep @s (successOrFirstFailure res) :: (State s, [[PredicateFailure s]])) of
         (True, (st, [])) ->
           sfor_ (assertions @s)
             $! ( \case
@@ -633,6 +639,7 @@ instance
   type Signal (STUB e st si f m) = si
   type PredicateFailure (STUB e st si f m) = f
   type BaseM (STUB e st si f m) = m
+  data Event _
 
   transitionRules = []
   initialRules = []
@@ -664,11 +671,11 @@ sfor_ :: (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()
 sfor_ = flip straverse_
 
 tellEvent ::
-  Event ->
+  Event sts ->
   Rule sts ctx ()
 tellEvent e = tellEvents [e]
 
 tellEvents ::
-  [Event] ->
+  [Event sts] ->
   Rule sts ctx ()
 tellEvents es = liftF $ Writer es ()
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
index cf61facaf98..0e0f5153011 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
@@ -137,6 +137,8 @@ instance
   type BaseM (BBODY era) = ShelleyBase
 
   type PredicateFailure (BBODY era) = BbodyPredicateFailure era
+  data Event _ 
+    = LedgersEvent (Event (Core.EraRule "LEDGERS" era)) -- Subtransition Failures
 
   initialRules = []
   transitionRules = [bbodyTransition]
@@ -203,3 +205,4 @@ instance
   Embed ledgers (BBODY era)
   where
   wrapFailed = LedgersFailure
+  wrapEvents = LedgersEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
index 61d66710480..92bd1204402 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
@@ -270,6 +270,12 @@ instance
 
   type PredicateFailure (CHAIN era) = ChainPredicateFailure era
 
+  data Event _
+    = BbodyEvent (Event (BBODY era))
+    | TicknEvent (Event TICKN)
+    | TickEvent  (Event (TICK era))
+    | PrtclEvent (Event (PRTCL (Crypto era)))
+
   initialRules = []
   transitionRules = [chainTransition]
 
@@ -417,6 +423,7 @@ instance
   Embed (BBODY era) (CHAIN era)
   where
   wrapFailed = BbodyFailure
+  wrapEvents = BbodyEvent
 
 instance
   ( Era era,
@@ -426,6 +433,7 @@ instance
   Embed TICKN (CHAIN era)
   where
   wrapFailed = TicknFailure
+  wrapEvents = TicknEvent
 
 instance
   ( Era era,
@@ -436,6 +444,7 @@ instance
   Embed (TICK era) (CHAIN era)
   where
   wrapFailed = TickFailure
+  wrapEvents = TickEvent
 
 instance
   ( Era era,
@@ -446,6 +455,7 @@ instance
   Embed (PRTCL c) (CHAIN era)
   where
   wrapFailed = PrtclFailure
+  wrapEvents = PrtclEvent
 
 data AdaPots = AdaPots
   { treasuryAdaPot :: Coin,
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs
index 6e4d901a644..8252e1e1bb3 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Deleg.hs
@@ -149,6 +149,7 @@ instance
   type Environment (DELEG era) = DelegEnv era
   type BaseM (DELEG era) = ShelleyBase
   type PredicateFailure (DELEG era) = DelegPredicateFailure era
+  data Event _
 
   transitionRules = [delegationTransition]
 
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs
index 1ffba15f0a9..14384675310 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs
@@ -136,6 +136,7 @@ instance
   type
     PredicateFailure (DELEGS era) =
       DelegsPredicateFailure era
+  data Event _ = DelplEvent (Event (DELPL era))
 
   transitionRules = [delegsTransition]
 
@@ -262,3 +263,4 @@ instance
   Embed (DELPL era) (DELEGS era)
   where
   wrapFailed = DelplFailure
+  wrapEvents = DelplEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs
index 2e1670d3ed8..653c8fe38ac 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs
@@ -106,6 +106,9 @@ instance
   type Environment (DELPL era) = DelplEnv era
   type BaseM (DELPL era) = ShelleyBase
   type PredicateFailure (DELPL era) = DelplPredicateFailure era
+  data Event (DELPL era)
+    = DelegEvent (Event (DELEG era))
+    | PoolEvent (Event (POOL era))
 
   transitionRules = [delplTransition]
 
@@ -197,6 +200,7 @@ instance
   Embed (POOL era) (DELPL era)
   where
   wrapFailed = PoolFailure
+  wrapEvents = PoolEvent
 
 instance
   ( Era era,
@@ -206,3 +210,4 @@ instance
   Embed (DELEG era) (DELPL era)
   where
   wrapFailed = DelegFailure
+  wrapEvents = DelegEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs
index 4fd51c95e02..b9499dddcd1 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs
@@ -114,6 +114,10 @@ instance
   type Environment (EPOCH era) = ()
   type BaseM (EPOCH era) = ShelleyBase
   type PredicateFailure (EPOCH era) = EpochPredicateFailure era
+  data Event _
+    = SnapEvent (Event (SNAP era))
+    | PoolReapEvent (Event (POOLREAP era))
+    | UpecEvents (Event (UPEC era))
   transitionRules = [epochTransition]
 
 instance
@@ -206,6 +210,7 @@ instance
   Embed (SNAP era) (EPOCH era)
   where
   wrapFailed = SnapFailure
+  wrapEvents = SnapEvent
 
 instance
   ( Era era,
@@ -215,6 +220,7 @@ instance
   Embed (POOLREAP era) (EPOCH era)
   where
   wrapFailed = PoolReapFailure
+  wrapEvents = PoolReapEvent
 
 instance
   ( Era era,
@@ -224,3 +230,4 @@ instance
   Embed (UPEC era) (EPOCH era)
   where
   wrapFailed = UpecFailure
+  wrapEvents = UpecEvents
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
index c6b95497583..720e1d1474d 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
@@ -162,6 +162,9 @@ instance
   type Environment (LEDGER era) = LedgerEnv era
   type BaseM (LEDGER era) = ShelleyBase
   type PredicateFailure (LEDGER era) = LedgerPredicateFailure era
+  data Event _ 
+    = UtxowEvent (Event (UTXOW era))
+    | DelegsEvent (Event (DELEGS era))
 
   initialRules = []
   transitionRules = [ledgerTransition]
@@ -229,6 +232,7 @@ instance
   Embed (DELEGS era) (LEDGER era)
   where
   wrapFailed = DelegsFailure
+  wrapEvents = DelegsEvent
 
 instance
   ( Era era,
@@ -238,3 +242,4 @@ instance
   Embed (UTXOW era) (LEDGER era)
   where
   wrapFailed = UtxowFailure
+  wrapEvents = UtxowEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs
index a96c6154046..604270744cf 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs
@@ -118,6 +118,7 @@ instance
   type Environment (LEDGERS era) = LedgersEnv era
   type BaseM (LEDGERS era) = ShelleyBase
   type PredicateFailure (LEDGERS era) = LedgersPredicateFailure era
+  data Event _ = LedgerEvent (Event (LEDGER era))
 
   transitionRules = [ledgersTransition]
 
@@ -152,3 +153,4 @@ instance
   Embed (LEDGER era) (LEDGERS era)
   where
   wrapFailed = LedgerFailure
+  wrapEvents = LedgerEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Mir.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Mir.hs
index 35f95d15804..f8ed0ec4f59 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Mir.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Mir.hs
@@ -67,6 +67,7 @@ instance (Typeable era, Default (EpochState era)) => STS (MIR era) where
   type Environment (MIR era) = ()
   type BaseM (MIR era) = ShelleyBase
   type PredicateFailure (MIR era) = MirPredicateFailure era
+  data Event _
 
   transitionRules = [mirTransition]
 
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
index aa2fd835f75..cba41a675ff 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
@@ -98,6 +98,10 @@ instance
   type BaseM (NEWEPOCH era) = ShelleyBase
   type PredicateFailure (NEWEPOCH era) = NewEpochPredicateFailure era
 
+  data Event _ 
+    = EpochEvent (Event (EPOCH era))
+    | MirEvent (Event (MIR era))
+
   initialRules =
     [ pure $
         NewEpochState
@@ -186,6 +190,7 @@ instance
   Embed (EPOCH era) (NEWEPOCH era)
   where
   wrapFailed = EpochFailure
+  wrapEvents = EpochEvent
 
 instance
   ( Era era,
@@ -195,3 +200,4 @@ instance
   Embed (MIR era) (NEWEPOCH era)
   where
   wrapFailed = MirFailure
+  wrapEvents = MirEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Newpp.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Newpp.hs
index 812eecb000c..6bb15f6741c 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Newpp.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Newpp.hs
@@ -93,6 +93,7 @@ instance
   type Environment (NEWPP era) = NewppEnv era
   type BaseM (NEWPP era) = ShelleyBase
   type PredicateFailure (NEWPP era) = NewppPredicateFailure era
+  data Event _
   transitionRules = [newPpTransition]
 
 instance Default (Core.PParams era) => Default (NewppState era) where
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs
index e8a4b7fbab7..b057bdf3a3a 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ocert.hs
@@ -71,6 +71,7 @@ instance
   type Environment (OCERT crypto) = OCertEnv crypto
   type BaseM (OCERT crypto) = ShelleyBase
   type PredicateFailure (OCERT crypto) = OcertPredicateFailure crypto
+  data Event _
 
   initialRules = [pure Map.empty]
   transitionRules = [ocertTransition]
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs
index 7e78cc3468f..fab9597b404 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs
@@ -142,6 +142,9 @@ instance
   type BaseM (OVERLAY crypto) = ShelleyBase
   type PredicateFailure (OVERLAY crypto) = OverlayPredicateFailure crypto
 
+  data Event (OVERLAY crypto)
+    = OcertEvent (Event (OCERT crypto))
+
   initialRules = []
 
   transitionRules = [overlayTransition]
@@ -293,3 +296,4 @@ instance
   Embed (OCERT crypto) (OVERLAY crypto)
   where
   wrapFailed = OcertFailure
+  wrapEvents = OcertEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
index 50395881099..14d9814272a 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
@@ -30,8 +30,7 @@ import Control.Monad (when)
 import Control.Monad.Trans.Reader (asks)
 import Control.SetAlgebra (dom, eval, setSingleton, singleton, (∈), (∉), (∪), (⋪), (⨃))
 import Control.State.Transition
-  ( Event (..),
-    STS (..),
+  ( STS (..),
     TRC (..),
     TransitionRule,
     failBecause,
@@ -106,6 +105,10 @@ instance
   type BaseM (POOL era) = ShelleyBase
   type PredicateFailure (POOL era) = PoolPredicateFailure era
 
+  data Event (POOL era) 
+    = NewPoolParam
+    | NewFuturePoolParam
+
   transitionRules = [poolDelegationTransition]
 
 instance
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/PoolReap.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/PoolReap.hs
index 9e142e69743..3038072d0d2 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/PoolReap.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/PoolReap.hs
@@ -86,6 +86,7 @@ instance
   type Environment (POOLREAP era) = Core.PParams era
   type BaseM (POOLREAP era) = ShelleyBase
   type PredicateFailure (POOLREAP era) = PoolreapPredicateFailure era
+  data Event _
   transitionRules = [poolReapTransition]
   assertions =
     [ PostCondition
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ppup.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ppup.hs
index 181c15ea4ff..71c325269f7 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ppup.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ppup.hs
@@ -92,6 +92,7 @@ instance
   type Environment (PPUP era) = PPUPEnv era
   type BaseM (PPUP era) = ShelleyBase
   type PredicateFailure (PPUP era) = PpupPredicateFailure era
+  data Event _
 
   initialRules = []
 
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
index 6ac94582b0d..4a746769bee 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
@@ -148,6 +148,10 @@ instance
   type BaseM (PRTCL crypto) = ShelleyBase
   type PredicateFailure (PRTCL crypto) = PrtclPredicateFailure crypto
 
+  data Event _ 
+    = OverlayEvent (Event (OVERLAY crypto))
+    | UpdnEvent (Event (UPDN crypto))
+
   initialRules = []
 
   transitionRules = [prtclTransition]
@@ -199,6 +203,7 @@ instance
   Embed (OVERLAY crypto) (PRTCL crypto)
   where
   wrapFailed = OverlayFailure
+  wrapEvents = OverlayEvent
 
 instance
   ( Crypto crypto,
@@ -209,6 +214,7 @@ instance
   Embed (UPDN crypto) (PRTCL crypto)
   where
   wrapFailed = UpdnFailure
+  wrapEvents = UpdnEvent
 
 data PrtlSeqFailure crypto
   = WrongSlotIntervalPrtclSeq
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Rupd.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Rupd.hs
index fb06b34bcd7..9c5f916f245 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Rupd.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Rupd.hs
@@ -98,6 +98,7 @@ instance
   type Environment (RUPD era) = RupdEnv era
   type BaseM (RUPD era) = ShelleyBase
   type PredicateFailure (RUPD era) = RupdPredicateFailure era
+  data Event _
 
   initialRules = [pure SNothing]
   transitionRules = [rupdTransition]
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Snap.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Snap.hs
index aea9f59757e..437dff5f3a7 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Snap.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Snap.hs
@@ -49,6 +49,7 @@ instance (UsesTxOut era, UsesValue era) => STS (SNAP era) where
   type Environment (SNAP era) = LedgerState era
   type BaseM (SNAP era) = ShelleyBase
   type PredicateFailure (SNAP era) = SnapPredicateFailure era
+  data Event _
   initialRules = [pure emptySnapShots]
   transitionRules = [snapTransition]
 
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
index d114388112a..dc89279ab38 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
@@ -91,6 +91,9 @@ instance
   type Environment (TICK era) = ()
   type BaseM (TICK era) = ShelleyBase
   type PredicateFailure (TICK era) = TickPredicateFailure era
+  data Event _
+    = NewEpochEvent (Event (NEWEPOCH era))
+    | RupdEvent (Event (RUPD era))
 
   initialRules = []
   transitionRules = [bheadTransition]
@@ -192,6 +195,7 @@ instance
   Embed (NEWEPOCH era) (TICK era)
   where
   wrapFailed = NewEpochFailure
+  wrapEvents = NewEpochEvent
 
 instance
   ( Era era,
@@ -201,6 +205,7 @@ instance
   Embed (RUPD era) (TICK era)
   where
   wrapFailed = RupdFailure
+  wrapEvents = RupdEvent
 
 {------------------------------------------------------------------------------
 -- TICKF transition
@@ -252,6 +257,8 @@ instance
   type Environment (TICKF era) = ()
   type BaseM (TICKF era) = ShelleyBase
   type PredicateFailure (TICKF era) = TickfPredicateFailure era
+  data Event _ 
+    = TickfNewEpochEvent (Event (NEWEPOCH era))
 
   initialRules = []
   transitionRules =
@@ -270,3 +277,4 @@ instance
   Embed (NEWEPOCH era) (TICKF era)
   where
   wrapFailed = TickfNewEpochFailure
+  wrapEvents = TickfNewEpochEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tickn.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tickn.hs
index 66a91803f40..623f11d108b 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tickn.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tickn.hs
@@ -73,6 +73,7 @@ instance STS TICKN where
   type Environment TICKN = TicknEnv
   type BaseM TICKN = ShelleyBase
   type PredicateFailure TICKN = TicknPredicateFailure
+  data Event _
 
   initialRules =
     [ pure
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Updn.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Updn.hs
index 4fdf62d0335..db423a2bb10 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Updn.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Updn.hs
@@ -48,6 +48,7 @@ instance
   type Environment (UPDN crypto) = UpdnEnv
   type BaseM (UPDN crypto) = ShelleyBase
   type PredicateFailure (UPDN crypto) = UpdnPredicateFailure crypto
+  data Event _
   initialRules =
     [ pure
         ( UpdnState
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
index a1e661b13d4..ff44b3b07af 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
@@ -91,6 +91,8 @@ instance
   type Environment (UPEC era) = EpochState era
   type BaseM (UPEC era) = ShelleyBase
   type PredicateFailure (UPEC era) = UpecPredicateFailure era
+  data Event (UPEC era) 
+    = NewPpEvent (Event (NEWPP era))
   initialRules = []
   transitionRules =
     [ do
@@ -156,3 +158,4 @@ instance
   Embed (NEWPP era) (UPEC era)
   where
   wrapFailed = NewPpFailure
+  wrapEvents = NewPpEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
index 5e8dfdec92a..3b8dad661eb 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
@@ -53,7 +53,7 @@ import Control.State.Transition
     liftSTS,
     trans,
     wrapFailed,
-    (?!),
+    (?!), wrapEvents
   )
 import Data.Foldable (foldl', toList)
 import Data.Map.Strict (Map)
@@ -295,6 +295,7 @@ instance
   type Environment (UTXO era) = UtxoEnv era
   type BaseM (UTXO era) = ShelleyBase
   type PredicateFailure (UTXO era) = UtxoPredicateFailure era
+  data Event _ = UpdateEvent (Event (PPUP era))
 
   transitionRules = [utxoInductive]
 
@@ -438,3 +439,4 @@ instance
   Embed (PPUP era) (UTXO era)
   where
   wrapFailed = UpdateFailure
+  wrapEvents = UpdateEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
index 131d655bd88..c324eec452d 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
@@ -53,7 +53,7 @@ import Control.State.Transition
     trans,
     wrapFailed,
     (?!),
-    (?!:),
+    (?!:), wrapEvents
   )
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq (filter)
@@ -387,6 +387,7 @@ instance
   Embed (UTXO era) (UTXOW era)
   where
   wrapFailed = UtxoFailure
+  wrapEvents = UtxoEvent
 
 instance
   ( -- Fix Core.Witnesses to the Shelley Era
@@ -409,5 +410,6 @@ instance
   type Environment (UTXOW era) = UtxoEnv era
   type BaseM (UTXOW era) = ShelleyBase
   type PredicateFailure (UTXOW era) = UtxowPredicateFailure era
+  data Event _ = UtxoEvent (Event (UTXO era))
   transitionRules = [shelleyStyleWitness witsVKeyNeeded id]
   initialRules = [initialLedgerStateUTXOW]

From f8ddf90f63a2f9173e2f32f7bd42bf1ea3ecd95b Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Thu, 20 May 2021 18:49:58 -0400
Subject: [PATCH 08/22] rn wrapEvents

---
 .../src/Byron/Spec/Chain/STS/Rule/BBody.hs    |  8 +++----
 .../src/Byron/Spec/Chain/STS/Rule/Bupi.hs     |  8 +++----
 .../src/Byron/Spec/Chain/STS/Rule/Chain.hs    | 10 ++++-----
 .../src/Byron/Spec/Chain/STS/Rule/Epoch.hs    |  2 +-
 .../src/Byron/Spec/Chain/STS/Rule/Pbft.hs     |  2 +-
 .../src/Byron/Spec/Ledger/Delegation.hs       | 10 ++++-----
 .../src/Byron/Spec/Ledger/STS/UTXOW.hs        |  2 +-
 .../src/Byron/Spec/Ledger/STS/UTXOWS.hs       |  4 ++--
 .../src/Byron/Spec/Ledger/Update.hs           | 22 +++++++++----------
 .../Spec/Ledger/Delegation/Properties.hs      |  4 ++--
 .../Byron/Spec/Ledger/Update/Properties.hs    |  8 +++----
 .../src/Control/State/Transition/Extended.hs  |  6 ++---
 .../src/Shelley/Spec/Ledger/STS/Bbody.hs      |  2 +-
 .../src/Shelley/Spec/Ledger/STS/Chain.hs      |  8 +++----
 .../src/Shelley/Spec/Ledger/STS/Delegs.hs     |  2 +-
 .../src/Shelley/Spec/Ledger/STS/Delpl.hs      |  4 ++--
 .../src/Shelley/Spec/Ledger/STS/Epoch.hs      |  6 ++---
 .../src/Shelley/Spec/Ledger/STS/Ledger.hs     |  4 ++--
 .../src/Shelley/Spec/Ledger/STS/Ledgers.hs    |  2 +-
 .../src/Shelley/Spec/Ledger/STS/NewEpoch.hs   |  4 ++--
 .../src/Shelley/Spec/Ledger/STS/Overlay.hs    |  2 +-
 .../src/Shelley/Spec/Ledger/STS/Prtcl.hs      |  4 ++--
 .../src/Shelley/Spec/Ledger/STS/Tick.hs       |  6 ++---
 .../src/Shelley/Spec/Ledger/STS/Upec.hs       |  2 +-
 .../src/Shelley/Spec/Ledger/STS/Utxo.hs       |  4 ++--
 .../src/Shelley/Spec/Ledger/STS/Utxow.hs      |  4 ++--
 26 files changed, 70 insertions(+), 70 deletions(-)

diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs
index 2444f1b7ffd..3040827bb48 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs
+++ b/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,
-                     (?!), wrapEvents)
+                     (?!), wrapEvent)
 
 import           Byron.Spec.Chain.STS.Block
 
@@ -98,12 +98,12 @@ instance STS BBODY where
 
 instance Embed BUPI BBODY where
   wrapFailed = BUPIFailure
-  wrapEvents = BUPIEvent
+  wrapEvent = BUPIEvent
 
 instance Embed DELEG BBODY where
   wrapFailed = DelegationFailure
-  wrapEvents = DelegationEvent
+  wrapEvent = DelegationEvent
 
 instance Embed UTXOWS BBODY where
   wrapFailed = UTXOWSFailure
-  wrapEvents = UTXOWSEvent
+  wrapEvent = UTXOWSEvent
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs
index cad4214a780..79a09f88563 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs
+++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Bupi.hs
@@ -10,7 +10,7 @@ import           Data.Data (Data, Typeable)
 
 import           Control.State.Transition (Embed, Environment, PredicateFailure, STS, Signal, State,
                      TRC (TRC), TransitionRule, Event, initialRules, judgmentContext, trans,
-                     transitionRules, wrapFailed, wrapEvents)
+                     transitionRules, wrapFailed, wrapEvent)
 import           Byron.Spec.Ledger.Core (VKey)
 import           Byron.Spec.Ledger.Update (ProtVer, UPIEND, UPIEnv, UPIREG, UPIState, UPIVOTES, UProp, Vote)
 
@@ -72,12 +72,12 @@ instance STS BUPI where
 
 instance Embed UPIREG BUPI where
   wrapFailed = UPIREGFailure
-  wrapEvents = UPIREGEvent
+  wrapEvent = UPIREGEvent
 
 instance Embed UPIVOTES BUPI where
   wrapFailed = UPIVOTESFailure
-  wrapEvents = UPVOTESEvent
+  wrapEvent = UPVOTESEvent
 
 instance Embed UPIEND BUPI where
   wrapFailed = UPIENDFailure
-  wrapEvents = UPIENDEvent
+  wrapEvent = UPIENDEvent
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs
index 8a09609b9d4..7aa5f3df3c2 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs
+++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Chain.hs
@@ -172,23 +172,23 @@ instance STS CHAIN where
 
 instance Embed EPOCH CHAIN where
   wrapFailed = EpochFailure
-  wrapEvents = EpochEvent
+  wrapEvent = EpochEvent
 
 instance Embed BBODY CHAIN where
   wrapFailed = BBodyFailure
-  wrapEvents = BBodyEvent
+  wrapEvent = BBodyEvent
 
 instance Embed PBFT CHAIN where
   wrapFailed = PBFTFailure
-  wrapEvents = PBFTEvent
+  wrapEvent = PBFTEvent
 
 instance Embed DELEG CHAIN where
   wrapFailed = LedgerDelegationFailure
-  wrapEvents = LedgerDelegationEvent
+  wrapEvent = LedgerDelegationEvent
 
 instance Embed UTXOWS CHAIN where
   wrapFailed = LedgerUTxOFailure
-  wrapEvents = LedgerUTxOEvent
+  wrapEvent = LedgerUTxOEvent
 
 isHeaderSizeTooBigFailure :: PredicateFailure CHAIN -> Bool
 isHeaderSizeTooBigFailure (HeaderSizeTooBig _ _ _) = True
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs
index 1fd8a675dda..83a1e9676cf 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs
+++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Epoch.hs
@@ -59,4 +59,4 @@ instance STS EPOCH where
 
 instance Embed UPIEC EPOCH where
   wrapFailed = UPIECFailure
-  wrapEvents = UPIECEvent
+  wrapEvent = UPIECEvent
diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs
index ce535e44326..1ad560d5cd9 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs
+++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/Pbft.hs
@@ -63,4 +63,4 @@ instance STS PBFT where
 
 instance Embed SIGCNT PBFT where
   wrapFailed = SigCountFailure
-  wrapEvents = SigCountEvent
+  wrapEvent = SigCountEvent
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs
index dc782d874e6..be911521900 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs
+++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs
@@ -454,7 +454,7 @@ instance STS SDELEGS where
 
 instance Embed SDELEG SDELEGS where
   wrapFailed = SDelegFailure
-  wrapEvents = SDelegEvent
+  wrapEvent = SDelegEvent
 
 -- | Delegation rules sequencing
 data ADELEGS deriving (Data, Typeable)
@@ -489,7 +489,7 @@ instance STS ADELEGS where
 
 instance Embed ADELEG ADELEGS where
   wrapFailed = ADelegFailure
-  wrapEvents = ADelegEvent
+  wrapEvent = ADelegEvent
 
 -- | Delegation interface
 data DELEG deriving (Data, Typeable)
@@ -537,11 +537,11 @@ instance STS DELEG where
 
 instance Embed SDELEGS DELEG where
   wrapFailed = SDelegSFailure
-  wrapEvents = SDelegSEvent
+  wrapEvent = SDelegSEvent
 
 instance Embed ADELEGS DELEG where
   wrapFailed = ADelegSFailure
-  wrapEvents = ADelegSEvent
+  wrapEvent = ADelegSEvent
 
 --------------------------------------------------------------------------------
 -- Generators
@@ -635,7 +635,7 @@ instance STS MSDELEG where
 
 instance Embed SDELEG MSDELEG where
   wrapFailed = SDELEGFailure
-  wrapEvents = SDELEGEvent
+  wrapEvent = SDELEGEvent
 
 instance HasTrace MSDELEG where
 
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs
index 2ee0706ae56..a2418e52d64 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs
+++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOW.hs
@@ -94,7 +94,7 @@ witnessed (Tx tx wits) utxo =
 
 instance Embed UTXO UTXOW where
   wrapFailed = UtxoFailure
-  wrapEvents = UtxoEvent
+  wrapEvent = UtxoEvent
 
 -- | Constant list of addresses intended to be used in the generators.
 traceAddrs :: [Addr]
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs
index 42b9c3b3ffc..c14c5ba4fa2 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs
+++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/STS/UTXOWS.hs
@@ -22,7 +22,7 @@ import           Byron.Spec.Ledger.STS.UTXOW (UTXOW)
 import           Byron.Spec.Ledger.UTxO (Tx)
 import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS(..),
                      Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
-                     transitionRules, wrapFailed, wrapEvents)
+                     transitionRules, wrapFailed, wrapEvent)
 import           Control.State.Transition.Generator (HasTrace, envGen, genTrace, sigGen)
 import           Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)
 
@@ -58,7 +58,7 @@ instance STS UTXOWS where
 
 instance Embed UTXOW UTXOWS where
   wrapFailed = UtxowFailure
-  wrapEvents = UtxowEvent
+  wrapEvent = UtxowEvent
 
 instance HasTrace UTXOWS where
   envGen = envGen @UTXOW
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
index 1445e86f2d1..099c0fd3ff4 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
+++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
@@ -505,11 +505,11 @@ instance STS UPV where
 
 instance Embed UPPVV UPV where
   wrapFailed = UPPVVFailure
-  wrapEvents = UPPVVEvent
+  wrapEvent = UPPVVEvent
 
 instance Embed UPSVV UPV where
   wrapFailed = UPSVVFailure
-  wrapEvents = UPSVVEvent
+  wrapEvent = UPSVVEvent
 
 data UPREG deriving (Generic, Data, Typeable)
 -- | These `PredicateFailure`s are all throwable.
@@ -553,7 +553,7 @@ instance STS UPREG where
 
 instance Embed UPV UPREG where
   wrapFailed = UPVFailure
-  wrapEvents = UPVEvent
+  wrapEvent = UPVEvent
 
 ------------------------------------------------------------------------
 -- Update voting
@@ -681,7 +681,7 @@ instance STS UPVOTE where
 
 instance Embed ADDVOTE UPVOTE where
   wrapFailed = ADDVOTEFailure
-  wrapEvents = ADDVOTEEvent
+  wrapEvent = ADDVOTEEvent
 
 ------------------------------------------------------------------------
 -- Update voting
@@ -825,7 +825,7 @@ instance STS UPEND where
 
 instance Embed FADS UPEND where
   wrapFailed = error "No possible failures in FADS"
-  wrapEvents = FADSEvent
+  wrapEvent = FADSEvent
 
 ------------------------------------------------------------------------
 -- Update interface
@@ -998,7 +998,7 @@ instance STS UPIREG where
 
 instance Embed UPREG UPIREG where
   wrapFailed = UPREGFailure
-  wrapEvents = UPREGEvent
+  wrapEvent = UPREGEvent
 
 instance HasTrace UPIREG where
 
@@ -1383,7 +1383,7 @@ instance STS UPIVOTE where
 
 instance Embed UPVOTE UPIVOTE where
   wrapFailed = UPVOTEFailure
-  wrapEvents = UPVOTEEvent
+  wrapEvent = UPVOTEEvent
 
 
 data APPLYVOTES deriving (Generic, Data, Typeable)
@@ -1414,7 +1414,7 @@ instance STS APPLYVOTES where
 
 instance Embed UPIVOTE APPLYVOTES where
   wrapFailed = UpivoteFailure
-  wrapEvents = UpivoteEvent
+  wrapEvent = UpivoteEvent
 
 data UPIVOTES deriving (Generic, Data, Typeable)
 
@@ -1474,7 +1474,7 @@ instance STS UPIVOTES where
 
 instance Embed APPLYVOTES UPIVOTES where
   wrapFailed = ApplyVotesFailure
-  wrapEvents = ApplyVotesEvent
+  wrapEvent = ApplyVotesEvent
 
 instance HasTrace UPIVOTES where
 
@@ -1615,7 +1615,7 @@ instance STS UPIEND where
 
 instance Embed UPEND UPIEND where
   wrapFailed = UPENDFailure
-  wrapEvents = UPENDEvent
+  wrapEvent = UPENDEvent
 
 -- | Given a list of protocol versions and keys endorsing those versions,
 -- generate a protocol-version endorsement, or 'Nothing' if the list of
@@ -1720,7 +1720,7 @@ instance STS UPIEC where
 
 instance Embed PVBUMP UPIEC where
   wrapFailed = PVBUMPFailure
-  wrapEvents = PVBUMPEvent
+  wrapEvent = PVBUMPEvent
 
 -- | Generate an optional update-proposal and a list of votes, given an update
 -- environment and state.
diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
index 895abdaf76e..a308e55b4b7 100644
--- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
+++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
@@ -41,7 +41,7 @@ import           Lens.Micro.TH (makeLenses)
 
 import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS,
                      Signal, State, TRC (TRC), Event, applySTS, initialRules, judgmentContext, trans,
-                     transitionRules, wrapFailed, (?!), wrapEvents)
+                     transitionRules, wrapFailed, (?!), wrapEvent)
 import           Control.State.Transition.Generator (HasSizeInfo, HasTrace, SignalGenerator,
                      TraceProfile (TraceProfile), classifySize, classifyTraceLength, envGen,
                      failures, isTrivial, nonTrivialTrace, proportionOfValidSignals, sigGen,
@@ -134,7 +134,7 @@ instance STS DBLOCK where
 
 instance Embed DELEG DBLOCK where
   wrapFailed = DPF
-  wrapEvents = DELEGEvent
+  wrapEvent = DELEGEvent
 
 -- | Check that all the delegation certificates in the trace were correctly
 -- applied.
diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs
index d0b936dfa3a..41b53fd68eb 100644
--- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs
+++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Update/Properties.hs
@@ -36,7 +36,7 @@ import           Numeric.Natural (Natural)
 
 import           Control.State.Transition (Embed, Environment, IRC (IRC), PredicateFailure, STS, Event,
                      Signal, State, TRC (TRC), initialRules, judgmentContext, trans,
-                     transitionRules, wrapFailed, (?!), wrapEvents)
+                     transitionRules, wrapFailed, (?!), wrapEvent)
 import           Control.State.Transition.Generator (HasTrace, SignalGenerator, envGen,
                      randomTraceOfSize, ratio, sigGen, trace, traceLengthsAreClassified,
                      traceOfLength)
@@ -356,15 +356,15 @@ instance STS UBLOCK where
 
 instance Embed UPIREG UBLOCK where
   wrapFailed = UPIREGFailure
-  wrapEvents = UPIREGEvent
+  wrapEvent = UPIREGEvent
 
 instance Embed UPIVOTES UBLOCK where
   wrapFailed = UPIVOTESFailure
-  wrapEvents = UPIVOTESEvent
+  wrapEvent = UPIVOTESEvent
 
 instance Embed UPIEND UBLOCK where
   wrapFailed = UPIENDFailure
-  wrapEvents = UPIENDEvent
+  wrapEvent = UPIENDEvent
 
 instance HasTrace UBLOCK where
   envGen _ =
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index 8e38666035b..eefae623769 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -229,11 +229,11 @@ class
 class (STS sub, BaseM sub ~ BaseM super) => Embed sub super where
   -- | Wrap a predicate failure of the subsystem in a failure of the super-system.
   wrapFailed :: PredicateFailure sub -> PredicateFailure super
-  wrapEvents :: Event sub -> Event super
+  wrapEvent :: Event sub -> Event super
 
 instance STS sts => Embed sts sts where
   wrapFailed = id
-  wrapEvents = id
+  wrapEvent = id
 
 data EventPolicy 
   = EventPolicyReturn
@@ -513,7 +513,7 @@ applyRuleInternal ep vp goSTS jc r =
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
       () <- case ep of
         EPDiscard -> pure ()
-        EPReturn -> tell (wrapEvents <$> snd s)
+        EPReturn -> tell (wrapEvent <$> snd s)
       pure $ next ss
     runClause (Writer w a) = case ep of
       EPReturn -> tell w $> a
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
index 0e0f5153011..5a74964a4b6 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
@@ -205,4 +205,4 @@ instance
   Embed ledgers (BBODY era)
   where
   wrapFailed = LedgersFailure
-  wrapEvents = LedgersEvent
+  wrapEvent = LedgersEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
index 92bd1204402..4e54bdd5e4d 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
@@ -423,7 +423,7 @@ instance
   Embed (BBODY era) (CHAIN era)
   where
   wrapFailed = BbodyFailure
-  wrapEvents = BbodyEvent
+  wrapEvent = BbodyEvent
 
 instance
   ( Era era,
@@ -433,7 +433,7 @@ instance
   Embed TICKN (CHAIN era)
   where
   wrapFailed = TicknFailure
-  wrapEvents = TicknEvent
+  wrapEvent = TicknEvent
 
 instance
   ( Era era,
@@ -444,7 +444,7 @@ instance
   Embed (TICK era) (CHAIN era)
   where
   wrapFailed = TickFailure
-  wrapEvents = TickEvent
+  wrapEvent = TickEvent
 
 instance
   ( Era era,
@@ -455,7 +455,7 @@ instance
   Embed (PRTCL c) (CHAIN era)
   where
   wrapFailed = PrtclFailure
-  wrapEvents = PrtclEvent
+  wrapEvent = PrtclEvent
 
 data AdaPots = AdaPots
   { treasuryAdaPot :: Coin,
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs
index 14384675310..21fe8ed3682 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delegs.hs
@@ -263,4 +263,4 @@ instance
   Embed (DELPL era) (DELEGS era)
   where
   wrapFailed = DelplFailure
-  wrapEvents = DelplEvent
+  wrapEvent = DelplEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs
index 653c8fe38ac..383b56ab4ca 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Delpl.hs
@@ -200,7 +200,7 @@ instance
   Embed (POOL era) (DELPL era)
   where
   wrapFailed = PoolFailure
-  wrapEvents = PoolEvent
+  wrapEvent = PoolEvent
 
 instance
   ( Era era,
@@ -210,4 +210,4 @@ instance
   Embed (DELEG era) (DELPL era)
   where
   wrapFailed = DelegFailure
-  wrapEvents = DelegEvent
+  wrapEvent = DelegEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs
index b9499dddcd1..69832488f06 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Epoch.hs
@@ -210,7 +210,7 @@ instance
   Embed (SNAP era) (EPOCH era)
   where
   wrapFailed = SnapFailure
-  wrapEvents = SnapEvent
+  wrapEvent = SnapEvent
 
 instance
   ( Era era,
@@ -220,7 +220,7 @@ instance
   Embed (POOLREAP era) (EPOCH era)
   where
   wrapFailed = PoolReapFailure
-  wrapEvents = PoolReapEvent
+  wrapEvent = PoolReapEvent
 
 instance
   ( Era era,
@@ -230,4 +230,4 @@ instance
   Embed (UPEC era) (EPOCH era)
   where
   wrapFailed = UpecFailure
-  wrapEvents = UpecEvents
+  wrapEvent = UpecEvents
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
index 720e1d1474d..b9dfa02edba 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
@@ -232,7 +232,7 @@ instance
   Embed (DELEGS era) (LEDGER era)
   where
   wrapFailed = DelegsFailure
-  wrapEvents = DelegsEvent
+  wrapEvent = DelegsEvent
 
 instance
   ( Era era,
@@ -242,4 +242,4 @@ instance
   Embed (UTXOW era) (LEDGER era)
   where
   wrapFailed = UtxowFailure
-  wrapEvents = UtxowEvent
+  wrapEvent = UtxowEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs
index 604270744cf..c4adfe2cc29 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledgers.hs
@@ -153,4 +153,4 @@ instance
   Embed (LEDGER era) (LEDGERS era)
   where
   wrapFailed = LedgerFailure
-  wrapEvents = LedgerEvent
+  wrapEvent = LedgerEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
index cba41a675ff..8590d12d9e9 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
@@ -190,7 +190,7 @@ instance
   Embed (EPOCH era) (NEWEPOCH era)
   where
   wrapFailed = EpochFailure
-  wrapEvents = EpochEvent
+  wrapEvent = EpochEvent
 
 instance
   ( Era era,
@@ -200,4 +200,4 @@ instance
   Embed (MIR era) (NEWEPOCH era)
   where
   wrapFailed = MirFailure
-  wrapEvents = MirEvent
+  wrapEvent = MirEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs
index fab9597b404..4c97c754375 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Overlay.hs
@@ -296,4 +296,4 @@ instance
   Embed (OCERT crypto) (OVERLAY crypto)
   where
   wrapFailed = OcertFailure
-  wrapEvents = OcertEvent
+  wrapEvent = OcertEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
index 4a746769bee..5b79a356f3c 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
@@ -203,7 +203,7 @@ instance
   Embed (OVERLAY crypto) (PRTCL crypto)
   where
   wrapFailed = OverlayFailure
-  wrapEvents = OverlayEvent
+  wrapEvent = OverlayEvent
 
 instance
   ( Crypto crypto,
@@ -214,7 +214,7 @@ instance
   Embed (UPDN crypto) (PRTCL crypto)
   where
   wrapFailed = UpdnFailure
-  wrapEvents = UpdnEvent
+  wrapEvent = UpdnEvent
 
 data PrtlSeqFailure crypto
   = WrongSlotIntervalPrtclSeq
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
index dc89279ab38..e5fbe2cf02b 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
@@ -195,7 +195,7 @@ instance
   Embed (NEWEPOCH era) (TICK era)
   where
   wrapFailed = NewEpochFailure
-  wrapEvents = NewEpochEvent
+  wrapEvent = NewEpochEvent
 
 instance
   ( Era era,
@@ -205,7 +205,7 @@ instance
   Embed (RUPD era) (TICK era)
   where
   wrapFailed = RupdFailure
-  wrapEvents = RupdEvent
+  wrapEvent = RupdEvent
 
 {------------------------------------------------------------------------------
 -- TICKF transition
@@ -277,4 +277,4 @@ instance
   Embed (NEWEPOCH era) (TICKF era)
   where
   wrapFailed = TickfNewEpochFailure
-  wrapEvents = TickfNewEpochEvent
+  wrapEvent = TickfNewEpochEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
index ff44b3b07af..e1623354291 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
@@ -158,4 +158,4 @@ instance
   Embed (NEWPP era) (UPEC era)
   where
   wrapFailed = NewPpFailure
-  wrapEvents = NewPpEvent
+  wrapEvent = NewPpEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
index 3b8dad661eb..0d0a1de41b2 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
@@ -53,7 +53,7 @@ import Control.State.Transition
     liftSTS,
     trans,
     wrapFailed,
-    (?!), wrapEvents
+    (?!), wrapEvent
   )
 import Data.Foldable (foldl', toList)
 import Data.Map.Strict (Map)
@@ -439,4 +439,4 @@ instance
   Embed (PPUP era) (UTXO era)
   where
   wrapFailed = UpdateFailure
-  wrapEvents = UpdateEvent
+  wrapEvent = UpdateEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
index c324eec452d..42535a62bc7 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
@@ -53,7 +53,7 @@ import Control.State.Transition
     trans,
     wrapFailed,
     (?!),
-    (?!:), wrapEvents
+    (?!:), wrapEvent
   )
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq (filter)
@@ -387,7 +387,7 @@ instance
   Embed (UTXO era) (UTXOW era)
   where
   wrapFailed = UtxoFailure
-  wrapEvents = UtxoEvent
+  wrapEvent = UtxoEvent
 
 instance
   ( -- Fix Core.Witnesses to the Shelley Era

From 6bc1f61ed8af17cf48159bca0a2aec7868bf7e25 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Thu, 20 May 2021 18:50:35 -0400
Subject: [PATCH 09/22] ormolise

---
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs       | 2 +-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs       | 2 +-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs      | 2 +-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs    | 2 +-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs        | 2 +-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs       | 2 +-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs        | 2 +-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs        | 2 +-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs        | 3 ++-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs       | 3 ++-
 10 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
index 5a74964a4b6..01fb78a2716 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Bbody.hs
@@ -137,7 +137,7 @@ instance
   type BaseM (BBODY era) = ShelleyBase
 
   type PredicateFailure (BBODY era) = BbodyPredicateFailure era
-  data Event _ 
+  data Event _
     = LedgersEvent (Event (Core.EraRule "LEDGERS" era)) -- Subtransition Failures
 
   initialRules = []
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
index 4e54bdd5e4d..795c9641a2b 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
@@ -273,7 +273,7 @@ instance
   data Event _
     = BbodyEvent (Event (BBODY era))
     | TicknEvent (Event TICKN)
-    | TickEvent  (Event (TICK era))
+    | TickEvent (Event (TICK era))
     | PrtclEvent (Event (PRTCL (Crypto era)))
 
   initialRules = []
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
index b9dfa02edba..0ef72ba18be 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
@@ -162,7 +162,7 @@ instance
   type Environment (LEDGER era) = LedgerEnv era
   type BaseM (LEDGER era) = ShelleyBase
   type PredicateFailure (LEDGER era) = LedgerPredicateFailure era
-  data Event _ 
+  data Event _
     = UtxowEvent (Event (UTXOW era))
     | DelegsEvent (Event (DELEGS era))
 
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
index 8590d12d9e9..069ae7ad828 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/NewEpoch.hs
@@ -98,7 +98,7 @@ instance
   type BaseM (NEWEPOCH era) = ShelleyBase
   type PredicateFailure (NEWEPOCH era) = NewEpochPredicateFailure era
 
-  data Event _ 
+  data Event _
     = EpochEvent (Event (EPOCH era))
     | MirEvent (Event (MIR era))
 
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
index 14d9814272a..d79e59191dd 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Pool.hs
@@ -105,7 +105,7 @@ instance
   type BaseM (POOL era) = ShelleyBase
   type PredicateFailure (POOL era) = PoolPredicateFailure era
 
-  data Event (POOL era) 
+  data Event (POOL era)
     = NewPoolParam
     | NewFuturePoolParam
 
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
index 5b79a356f3c..bdeb516875b 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Prtcl.hs
@@ -148,7 +148,7 @@ instance
   type BaseM (PRTCL crypto) = ShelleyBase
   type PredicateFailure (PRTCL crypto) = PrtclPredicateFailure crypto
 
-  data Event _ 
+  data Event _
     = OverlayEvent (Event (OVERLAY crypto))
     | UpdnEvent (Event (UPDN crypto))
 
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
index e5fbe2cf02b..21feeb7719f 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Tick.hs
@@ -257,7 +257,7 @@ instance
   type Environment (TICKF era) = ()
   type BaseM (TICKF era) = ShelleyBase
   type PredicateFailure (TICKF era) = TickfPredicateFailure era
-  data Event _ 
+  data Event _
     = TickfNewEpochEvent (Event (NEWEPOCH era))
 
   initialRules = []
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
index e1623354291..3c8bacdf380 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Upec.hs
@@ -91,7 +91,7 @@ instance
   type Environment (UPEC era) = EpochState era
   type BaseM (UPEC era) = ShelleyBase
   type PredicateFailure (UPEC era) = UpecPredicateFailure era
-  data Event (UPEC era) 
+  data Event (UPEC era)
     = NewPpEvent (Event (NEWPP era))
   initialRules = []
   transitionRules =
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
index 0d0a1de41b2..0968891397c 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxo.hs
@@ -52,8 +52,9 @@ import Control.State.Transition
     judgmentContext,
     liftSTS,
     trans,
+    wrapEvent,
     wrapFailed,
-    (?!), wrapEvent
+    (?!),
   )
 import Data.Foldable (foldl', toList)
 import Data.Map.Strict (Map)
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
index 42535a62bc7..e7806dcea96 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
@@ -51,9 +51,10 @@ import Control.State.Transition
     judgmentContext,
     liftSTS,
     trans,
+    wrapEvent,
     wrapFailed,
     (?!),
-    (?!:), wrapEvent
+    (?!:),
   )
 import qualified Data.Map.Strict as Map
 import qualified Data.Sequence as Seq (filter)

From caced7046b8ffa8ece0ffd7578525b25553537f6 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Fri, 21 May 2021 16:12:53 -0400
Subject: [PATCH 10/22] finish instances

---
 .../Control/State/Transition/Examples/CommitReveal.hs     | 3 +++
 .../test/Control/State/Transition/Examples/GlobalSum.hs   | 2 ++
 .../test/Control/State/Transition/Examples/Sum.hs         | 2 ++
 .../impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs       | 2 ++
 .../impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs      | 7 ++++++-
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs | 6 ++++--
 .../src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs | 8 ++++++--
 7 files changed, 25 insertions(+), 5 deletions(-)

diff --git a/semantics/small-steps-test/test/Control/State/Transition/Examples/CommitReveal.hs b/semantics/small-steps-test/test/Control/State/Transition/Examples/CommitReveal.hs
index d9f282422ac..9c06ead4ef9 100644
--- a/semantics/small-steps-test/test/Control/State/Transition/Examples/CommitReveal.hs
+++ b/semantics/small-steps-test/test/Control/State/Transition/Examples/CommitReveal.hs
@@ -22,6 +22,7 @@ import Control.State.Transition
     STS,
     Signal,
     State,
+    Event,
     TRC (TRC),
     initialRules,
     judgmentContext,
@@ -137,6 +138,8 @@ instance
     PredicateFailure (CR hashAlgo hashToDataMap commitData) =
       CRPredicateFailure hashAlgo hashToDataMap commitData
 
+  data Event _ = Cert
+
   initialRules =
     [ pure
         $! CRSt
diff --git a/semantics/small-steps-test/test/Control/State/Transition/Examples/GlobalSum.hs b/semantics/small-steps-test/test/Control/State/Transition/Examples/GlobalSum.hs
index 8f3615ba9cd..ee190bda4e5 100644
--- a/semantics/small-steps-test/test/Control/State/Transition/Examples/GlobalSum.hs
+++ b/semantics/small-steps-test/test/Control/State/Transition/Examples/GlobalSum.hs
@@ -33,6 +33,8 @@ instance STS GSUM where
 
   type PredicateFailure GSUM = NoFailure
 
+  data Event _
+
   initialRules = [pure 0]
 
   transitionRules =
diff --git a/semantics/small-steps-test/test/Control/State/Transition/Examples/Sum.hs b/semantics/small-steps-test/test/Control/State/Transition/Examples/Sum.hs
index 2486f140131..f19a1bb78bd 100644
--- a/semantics/small-steps-test/test/Control/State/Transition/Examples/Sum.hs
+++ b/semantics/small-steps-test/test/Control/State/Transition/Examples/Sum.hs
@@ -34,6 +34,8 @@ instance STS SUM where
 
   type PredicateFailure SUM = NoFailure
 
+  data Event _
+
   initialRules = [pure 0]
 
   transitionRules =
diff --git a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs
index ad4239bcf4a..615dbe50853 100644
--- a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs
+++ b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxo.hs
@@ -378,6 +378,7 @@ instance
   type
     PredicateFailure (UTXO era) =
       UtxoPredicateFailure era
+  data Event _ = UpdateEvent (Event (PPUP era))
 
   initialRules = []
   transitionRules = [utxoTransition]
@@ -390,6 +391,7 @@ instance
   Embed (PPUP era) (UTXO era)
   where
   wrapFailed = UpdateFailure
+  wrapEvent = UpdateEvent
 
 --------------------------------------------------------------------------------
 -- Serialisation
diff --git a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs
index e9adc3f51a8..00aefd3864a 100644
--- a/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs
+++ b/shelley-ma/impl/src/Cardano/Ledger/ShelleyMA/Rules/Utxow.hs
@@ -66,6 +66,8 @@ instance
   type
     PredicateFailure (UTXOW era) =
       UtxowPredicateFailure era
+  data Event _ = UtxoEvent (Event (UTXO era))
+
   transitionRules = [shelleyStyleWitness witsVKeyNeeded id]
 
   -- The ShelleyMA Era uses the same PredicateFailure type
@@ -80,12 +82,15 @@ instance
   Embed (UTXO era) (UTXOW era)
   where
   wrapFailed = UtxoFailure
+  wrapEvent = UtxoEvent
 
 instance
   ( Era era,
     STS (UTXOW era),
-    PredicateFailure (Core.EraRule "UTXOW" era) ~ UtxowPredicateFailure era
+    PredicateFailure (Core.EraRule "UTXOW" era) ~ UtxowPredicateFailure era,
+    Event (Core.EraRule "UTXOW" era) ~ Event (UTXOW era)
   ) =>
   Embed (UTXOW era) (Shelley.LEDGER era)
   where
   wrapFailed = Shelley.UtxowFailure
+  wrapEvent = Shelley.UtxowEvent
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
index 0ef72ba18be..b399ab5e007 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
@@ -19,6 +19,7 @@ module Shelley.Spec.Ledger.STS.Ledger
   ( LEDGER,
     LedgerEnv (..),
     LedgerPredicateFailure (..),
+    Event(..),
     PredicateFailure,
   )
 where
@@ -163,7 +164,7 @@ instance
   type BaseM (LEDGER era) = ShelleyBase
   type PredicateFailure (LEDGER era) = LedgerPredicateFailure era
   data Event _
-    = UtxowEvent (Event (UTXOW era))
+    = UtxowEvent (Event (Core.EraRule "UTXOW" era))
     | DelegsEvent (Event (DELEGS era))
 
   initialRules = []
@@ -237,7 +238,8 @@ instance
 instance
   ( Era era,
     STS (UTXOW era),
-    PredicateFailure (Core.EraRule "UTXOW" era) ~ UtxowPredicateFailure era
+    PredicateFailure (Core.EraRule "UTXOW" era) ~ UtxowPredicateFailure era,
+    Event (Core.EraRule "UTXOW" era) ~ Event (UTXOW era)
   ) =>
   Embed (UTXOW era) (LEDGER era)
   where
diff --git a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs
index 783aa70d0ed..c98faaaaf2b 100644
--- a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs
+++ b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs
@@ -31,6 +31,7 @@ import Control.State.Transition
     Environment,
     PredicateFailure,
     STS,
+    Event,
     Signal,
     State,
     TRC (..),
@@ -39,7 +40,7 @@ import Control.State.Transition
     judgmentContext,
     trans,
     transitionRules,
-    wrapFailed,
+    wrapFailed, wrapEvent
   )
 import Control.State.Transition.Trace (TraceOrder (OldestFirst), lastState, traceSignals)
 import qualified Control.State.Transition.Trace.Generator.QuickCheck as QC
@@ -111,9 +112,11 @@ instance
   type State (CERTS era) = (DPState (Crypto era), Ix)
   type Signal (CERTS era) = Maybe (DCert (Crypto era), CertCred era)
   type PredicateFailure (CERTS era) = CertsPredicateFailure era
-
+  
   type BaseM (CERTS era) = ShelleyBase
 
+  data Event _ = DELPLEvent (Event (DELPL era))
+
   initialRules = []
   transitionRules = [certsTransition]
 
@@ -152,6 +155,7 @@ instance
   Embed (DELPL era) (CERTS era)
   where
   wrapFailed = CertsFailure
+  wrapEvent = DELPLEvent
 
 instance
   ( EraGen era,

From d6f49c9c963856355705769af5386858b14cdb59 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Fri, 21 May 2021 16:14:21 -0400
Subject: [PATCH 11/22] formatting

---
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs       | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
index b399ab5e007..ade71ee3ddc 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Ledger.hs
@@ -19,7 +19,7 @@ module Shelley.Spec.Ledger.STS.Ledger
   ( LEDGER,
     LedgerEnv (..),
     LedgerPredicateFailure (..),
-    Event(..),
+    Event (..),
     PredicateFailure,
   )
 where

From ab448c3beda5c4bd76248d8dc38b807b17feb326 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Fri, 21 May 2021 16:34:59 -0400
Subject: [PATCH 12/22] doctest

---
 semantics/small-steps-test/src/Control/State/Transition/Trace.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
index 1e0f6443e61..916fccedf6f 100644
--- a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
+++ b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
@@ -132,6 +132,7 @@ mkTrace env initState sigs = Trace env initState sigs'
 --   type State DUMMY = Int
 --   type Signal DUMMY = String
 --   type PredicateFailure DUMMY = DummyPredicateFailure
+--   data Event _
 --   initialRules = []
 --   transitionRules = []
 -- :}

From e9aa5141cefa232dd69439e4d8d9521adacb145a Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Fri, 21 May 2021 17:14:54 -0400
Subject: [PATCH 13/22] doctest

---
 semantics/small-steps-test/src/Control/State/Transition/Trace.hs | 1 +
 1 file changed, 1 insertion(+)

diff --git a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
index 916fccedf6f..108b010d4bd 100644
--- a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
+++ b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
@@ -355,6 +355,7 @@ preStatesAndSignals NewestFirst tr
 --   type State ADDER = Int
 --   type Signal ADDER = Int
 --   type PredicateFailure ADDER = AdderPredicateFailure
+--   data Event _
 --   initialRules = [ pure 0 ]
 --   transitionRules =
 --     [ do

From 6fb466079f93956e3d0452353a7dd5be10e50251 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Fri, 21 May 2021 18:07:06 -0400
Subject: [PATCH 14/22] test instance

---
 alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs       | 6 ++++--
 .../executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs    | 6 ++++--
 2 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs b/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs
index 4d8528243e8..8d576727767 100644
--- a/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs
+++ b/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 (LEDGER, LedgerEnv (..), LedgerPredicateFailure (UtxowFailure), Event(..))
 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
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
index 795c9641a2b..a6215e97ef6 100644
--- a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
+++ b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Chain.hs
@@ -18,6 +18,7 @@ module Shelley.Spec.Ledger.STS.Chain
   ( CHAIN,
     ChainState (..),
     ChainPredicateFailure (..),
+    Event (..),
     PredicateFailure,
     AdaPots (..),
     initialShelleyState,
@@ -271,7 +272,7 @@ instance
   type PredicateFailure (CHAIN era) = ChainPredicateFailure era
 
   data Event _
-    = BbodyEvent (Event (BBODY era))
+    = BbodyEvent (Event (Core.EraRule "BBODY" era))
     | TicknEvent (Event TICKN)
     | TickEvent (Event (TICK era))
     | PrtclEvent (Event (PRTCL (Crypto era)))
@@ -418,7 +419,8 @@ instance
   ( Era era,
     Era era,
     STS (BBODY era),
-    PredicateFailure (Core.EraRule "BBODY" era) ~ BbodyPredicateFailure era
+    PredicateFailure (Core.EraRule "BBODY" era) ~ BbodyPredicateFailure era,
+    Event (Core.EraRule "BBODY" era) ~ Event (BBODY era)
   ) =>
   Embed (BBODY era) (CHAIN era)
   where

From 9b69d63078742ff114f2cc3212f32cc7f4c50b58 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Mon, 24 May 2021 09:46:11 -0400
Subject: [PATCH 15/22] formatting

---
 alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs b/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs
index 8d576727767..44e43e1eded 100644
--- a/alonzo/test/test/Test/Cardano/Ledger/Alonzo/Trials.hs
+++ b/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 (..), Event(..))
-import Shelley.Spec.Ledger.STS.Ledger (LEDGER, LedgerEnv (..), LedgerPredicateFailure (UtxowFailure), Event(..))
+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)

From 0947eea86860dd4cbef1ed1e8a7f59587ae8c27c Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Mon, 24 May 2021 09:57:53 -0400
Subject: [PATCH 16/22] remove trailing whitespace

---
 .../src/Byron/Spec/Chain/STS/Rule/BBody.hs           |  4 ++--
 byron/crypto/test/Test/Cardano/Crypto/Limits.hs      |  2 +-
 .../src/Byron/Spec/Ledger/Delegation.hs              |  2 +-
 .../executable-spec/src/Byron/Spec/Ledger/Update.hs  |  4 ++--
 .../Test/Byron/Spec/Ledger/Delegation/Properties.hs  |  2 +-
 .../impl/test/Test/Cardano/Chain/Update/Gen.hs       |  2 +-
 .../src/Control/State/Transition/Extended.hs         | 12 ++++++------
 .../src/Test/Cardano/Ledger/TranslationTools.hs      |  2 +-
 .../Shelley/Spec/Ledger/Generator/Trace/DCert.hs     |  2 +-
 9 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs
index 3040827bb48..4378e016e1e 100644
--- a/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs
+++ b/byron/chain/executable-spec/src/Byron/Spec/Chain/STS/Rule/BBody.hs
@@ -33,8 +33,8 @@ data BbodyPredicateFailure
   | InvalidUtxoHash
   | InvalidDelegationHash
   | InvalidUpdateProposalHash
-  | BUPIFailure (PredicateFailure BUPI)         
-  | DelegationFailure (PredicateFailure DELEG)  
+  | BUPIFailure (PredicateFailure BUPI)
+  | DelegationFailure (PredicateFailure DELEG)
   | UTXOWSFailure (PredicateFailure UTXOWS)
   deriving (Eq, Show, Data, Typeable)
 
diff --git a/byron/crypto/test/Test/Cardano/Crypto/Limits.hs b/byron/crypto/test/Test/Cardano/Crypto/Limits.hs
index 9fdf3d556a5..e02d14b4c10 100644
--- a/byron/crypto/test/Test/Cardano/Crypto/Limits.hs
+++ b/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
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs
index be911521900..0053859c445 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs
+++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Delegation.hs
@@ -505,7 +505,7 @@ instance STS DELEG where
   type Environment DELEG = DIEnv
 
   type PredicateFailure DELEG = DelegPredicateFailure
-  data Event _ 
+  data Event _
     = SDelegSEvent (Event SDELEGS)
     | ADelegSEvent (Event ADELEGS)
 
diff --git a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
index 099c0fd3ff4..d4c7fb36e4b 100644
--- a/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
+++ b/byron/ledger/executable-spec/src/Byron/Spec/Ledger/Update.hs
@@ -466,8 +466,8 @@ instance STS UPV where
 
   type Signal UPV = UProp
   type PredicateFailure UPV = UpvPredicateFailure
-  
-  data Event _ 
+
+  data Event _
     = UPPVVEvent (Event UPPVV)
     | UPSVVEvent (Event UPSVV)
 
diff --git a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
index a308e55b4b7..1ec3ba05d9b 100644
--- a/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
+++ b/byron/ledger/executable-spec/test/Test/Byron/Spec/Ledger/Delegation/Properties.hs
@@ -109,7 +109,7 @@ instance STS DBLOCK where
   type State DBLOCK = (DSEnv, DIState)
   type Signal DBLOCK = DBlock
   type PredicateFailure DBLOCK = DBlockPredicateFailure
-  data Event _ = 
+  data Event _ =
     DELEGEvent (Event DELEG)
 
   initialRules
diff --git a/byron/ledger/impl/test/Test/Cardano/Chain/Update/Gen.hs b/byron/ledger/impl/test/Test/Cardano/Chain/Update/Gen.hs
index fea96c4afbb..456cdb37d0a 100644
--- a/byron/ledger/impl/test/Test/Cardano/Chain/Update/Gen.hs
+++ b/byron/ledger/impl/test/Test/Cardano/Chain/Update/Gen.hs
@@ -250,6 +250,6 @@ genEndorsementError = Endorsement.MultipleProposalsForProtocolVersion <$>
   genProtocolVersion
 
 genRegistrationTooLarge :: Gen (Registration.TooLarge Int)
-genRegistrationTooLarge = Registration.TooLarge 
+genRegistrationTooLarge = Registration.TooLarge
   <$> Gen.int Range.constantBounded
   <*> Gen.int Range.constantBounded
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index eefae623769..f1704adebb1 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -235,7 +235,7 @@ instance STS sts => Embed sts sts where
   wrapFailed = id
   wrapEvent = id
 
-data EventPolicy 
+data EventPolicy
   = EventPolicyReturn
   | EventPolicyDiscard
 
@@ -467,7 +467,7 @@ instance MonadTrans (RuleEventLoggerT s) where
   lift = RuleEventLoggerT . lift . lift
 
 runRuleEventLoggerT :: forall s m a. RuleEventLoggerT s m a -> [PredicateFailure s] -> m ((a, [PredicateFailure s]), [Event s])
-runRuleEventLoggerT (RuleEventLoggerT m) s = runWriterT $ runStateT m s 
+runRuleEventLoggerT (RuleEventLoggerT m) s = runWriterT $ runStateT m s
 
 -- | Apply a rule even if its predicates fail.
 --
@@ -483,7 +483,7 @@ applyRuleInternal ::
   RuleContext rtype s ->
   Rule s rtype (State s) ->
   m (EventReturnType ep s (State s, [PredicateFailure s]))
-applyRuleInternal ep vp goSTS jc r = 
+applyRuleInternal ep vp goSTS jc r =
   case ep of
     EPReturn -> flip (runRuleEventLoggerT @s) [] $ foldF runClause r
     EPDiscard -> flip runStateT [] $ foldF runClause r
@@ -535,15 +535,15 @@ applySTSInternal ::
 applySTSInternal ep ap goRule ctx =
   successOrFirstFailure <$> applySTSInternal' rTypeRep ctx
   where
-    successOrFirstFailure :: 
-         [EventReturnType ep s (State s, [PredicateFailure s])] 
+    successOrFirstFailure ::
+         [EventReturnType ep s (State s, [PredicateFailure s])]
       -> EventReturnType ep s (State s, [[PredicateFailure s]])
     successOrFirstFailure xs =
       case find (\x -> null $ snd $ (discardEvents ep @s x :: (State s, [PredicateFailure s]))) xs of
         Nothing ->
           case xs of
             [] -> error "applySTSInternal was called with an empty set of rules"
-            s' : _ -> case ep of 
+            s' : _ -> case ep of
               EPDiscard -> (fst s', snd <$> xs)
               EPReturn -> ((fst $ fst s', (snd . fst) <$> xs), snd s')
         Just s' -> case ep of
diff --git a/shelley-ma/shelley-ma-test/src/Test/Cardano/Ledger/TranslationTools.hs b/shelley-ma/shelley-ma-test/src/Test/Cardano/Ledger/TranslationTools.hs
index b1829ade9ab..b3c52e54799 100644
--- a/shelley-ma/shelley-ma-test/src/Test/Cardano/Ledger/TranslationTools.hs
+++ b/shelley-ma/shelley-ma-test/src/Test/Cardano/Ledger/TranslationTools.hs
@@ -79,7 +79,7 @@ decodeTestAnn _ x =
    let bytes = serialize x
        decoded = decodeAnnotator mempty fromCBOR bytes :: Either DecoderError b
     in case decoded of
-  Left e -> assertFailure $ 
+  Left e -> assertFailure $
        "\nerror: " <> show e
     <> "\nbytes: " <> show (B16.encode bytes) <> "\n"
   Right _ -> return ()
diff --git a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs
index 086de6bf50a..0033573feb6 100644
--- a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs
+++ b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Generator/Trace/DCert.hs
@@ -112,7 +112,7 @@ instance
   type State (CERTS era) = (DPState (Crypto era), Ix)
   type Signal (CERTS era) = Maybe (DCert (Crypto era), CertCred era)
   type PredicateFailure (CERTS era) = CertsPredicateFailure era
-  
+
   type BaseM (CERTS era) = ShelleyBase
 
   data Event _ = DELPLEvent (Event (DELPL era))

From 58e3a659651acfd797f697c0c288fa3c38d4c95f Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Wed, 2 Jun 2021 10:58:55 -0400
Subject: [PATCH 17/22] factor out EventReturnType

---
 .../Cardano/Ledger/Rules/ValidationMode.hs    |  4 +-
 .../src/Control/State/Transition/Extended.hs  | 81 +++++++++----------
 .../src/Control/State/Transition/Trace.hs     |  4 +-
 .../src/Test/Shelley/Spec/Ledger/Utils.hs     |  4 +-
 4 files changed, 44 insertions(+), 49 deletions(-)

diff --git a/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs b/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
index cba9cbcf9cf..adb6bf8d3a2 100644
--- a/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
+++ b/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
@@ -30,8 +30,8 @@ applySTSValidateSuchThat ::
   m (Either [[PredicateFailure s]] (State s))
 applySTSValidateSuchThat cond ctx =
   applySTSOpts EPDiscard opts ctx <&> \case
-    (st, []) -> Right st
-    (_, pfs) -> Left pfs
+    ((st, []), _) -> Right st
+    ((_, pfs), _) -> Left pfs
   where
     opts =
       ApplySTSOpts
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index f1704adebb1..725f90dcc88 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -40,7 +40,6 @@ module Control.State.Transition.Extended
     Label,
     SingEP(..),
     EventPolicy(..),
-    EventReturnType,
     EventConstraintType,
     labeledPred,
     labeledPredE,
@@ -243,19 +242,10 @@ data SingEP ep where
   EPReturn  :: SingEP 'EventPolicyReturn
   EPDiscard :: SingEP 'EventPolicyDiscard
 
-type family EventReturnType ep sts a :: Type where
-  EventReturnType 'EventPolicyReturn sts a = (a, [Event sts])
-  EventReturnType _ _ a = a
-
 type family EventConstraintType e sts m :: Constraint where
   EventConstraintType 'EventPolicyReturn sts m = MonadWriter [Event sts] m
   EventConstraintType _ _ _ = ()
 
-discardEvents :: forall ep a. SingEP ep -> forall s. EventReturnType ep s a -> a
-discardEvents ep = case ep of
-  EPReturn -> fst
-  EPDiscard -> id
-
 data Clause sts (rtype :: RuleType) a where
   Lift ::
     STS sts =>
@@ -371,18 +361,18 @@ data ApplySTSOpts = ApplySTSOpts
     asoValidation :: ValidationPolicy
   }
 
-type STSInterpreter ep =
+type STSInterpreter =
   forall s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
   RuleContext rtype s ->
-  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
+  m ((State s, [[PredicateFailure s]]), [Event s])
 
-type RuleInterpreter ep =
+type RuleInterpreter =
   forall s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
   RuleContext rtype s ->
   Rule s rtype (State s) ->
-  m (EventReturnType ep s (State s, [PredicateFailure s]))
+  m ((State s, [PredicateFailure s]), [Event s])
 
 -- | Apply an STS with options. Note that this returns both the final state and
 -- the list of predicate failures.
@@ -392,11 +382,11 @@ applySTSOpts ::
   SingEP ep ->
   ApplySTSOpts ->
   RuleContext rtype s ->
-  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
+  m ((State s, [[PredicateFailure s]]), [Event s])
 applySTSOpts ep ApplySTSOpts {asoAssertions, asoValidation} ctx =
-  let goRule :: RuleInterpreter ep
+  let goRule :: RuleInterpreter
       goRule = applyRuleInternal ep asoValidation goSTS
-      goSTS :: STSInterpreter ep
+      goSTS :: STSInterpreter
       goSTS = applySTSInternal ep asoAssertions goRule
    in goSTS ctx
 
@@ -407,8 +397,8 @@ applySTS ::
   m (Either [[PredicateFailure s]] (State s))
 applySTS ctx =
   applySTSOpts EPDiscard defaultOpts ctx <&> \case
-    (st, []) -> Right st
-    (_, pfs) -> Left pfs
+    ((st, []), _) -> Right st
+    ((_, pfs), _) -> Left pfs
   where
 
 #ifdef STS_ASSERT
@@ -436,7 +426,7 @@ reapplySTS ::
   RuleContext rtype s ->
   m (State s)
 reapplySTS ctx =
-  applySTSOpts EPDiscard defaultOpts ctx <&> fst
+  applySTSOpts EPDiscard defaultOpts ctx <&> (fst . fst)
   where
     defaultOpts =
       ApplySTSOpts
@@ -450,7 +440,7 @@ applySTSIndifferently ::
   RuleContext rtype s ->
   m (State s, [[PredicateFailure s]])
 applySTSIndifferently =
-  applySTSOpts EPDiscard opts
+  fmap fst . applySTSOpts EPDiscard opts
   where
     opts =
       ApplySTSOpts
@@ -479,14 +469,16 @@ applyRuleInternal ::
   SingEP ep ->
   ValidationPolicy ->
   -- | Interpreter for subsystems
-  STSInterpreter ep ->
+  STSInterpreter ->
   RuleContext rtype s ->
   Rule s rtype (State s) ->
-  m (EventReturnType ep s (State s, [PredicateFailure s]))
+  m ((State s, [PredicateFailure s]), [Event s])
 applyRuleInternal ep vp goSTS jc r =
   case ep of
     EPReturn -> flip (runRuleEventLoggerT @s) [] $ foldF runClause r
-    EPDiscard -> flip runStateT [] $ foldF runClause r
+    EPDiscard -> do 
+      s <- flip runStateT [] $ foldF runClause r
+      pure (s, [])
   where
     runClause :: forall f t a.
       ( f ~ t m
@@ -506,14 +498,11 @@ applyRuleInternal ep vp goSTS jc r =
             Right x -> pure x
         else pure val
     runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do
-      s :: (EventReturnType ep sub (State sub, [[PredicateFailure sub]])) <- lift $ goSTS subCtx
-      let ss :: State sub
-          sfails :: [[PredicateFailure sub]]
-          (ss, sfails) = (discardEvents ep @sub) s
+      ((ss, sfails), sevents) :: ((State sub, [[PredicateFailure sub]]), [Event sub]) <- lift $ goSTS subCtx
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
       () <- case ep of
         EPDiscard -> pure ()
-        EPReturn -> tell (wrapEvent <$> snd s)
+        EPReturn -> tell $ fmap wrapEvent sevents
       pure $ next ss
     runClause (Writer w a) = case ep of
       EPReturn -> tell w $> a
@@ -529,31 +518,37 @@ applySTSInternal ::
   SingEP ep ->
   AssertionPolicy ->
   -- | Interpreter for rules
-  RuleInterpreter ep ->
+  RuleInterpreter ->
   RuleContext rtype s ->
-  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
+  m ((State s, [[PredicateFailure s]]), [Event s])
 applySTSInternal ep ap goRule ctx =
   successOrFirstFailure <$> applySTSInternal' rTypeRep ctx
   where
     successOrFirstFailure ::
-         [EventReturnType ep s (State s, [PredicateFailure s])]
-      -> EventReturnType ep s (State s, [[PredicateFailure s]])
+         [((State s, [PredicateFailure s]), [Event s])]
+      -> ((State s, [[PredicateFailure s]]), [Event s])
     successOrFirstFailure xs =
-      case find (\x -> null $ snd $ (discardEvents ep @s x :: (State s, [PredicateFailure s]))) xs of
+      case find (null . snd . fst) xs of
         Nothing ->
           case xs of
             [] -> error "applySTSInternal was called with an empty set of rules"
-            s' : _ -> case ep of
-              EPDiscard -> (fst s', snd <$> xs)
-              EPReturn -> ((fst $ fst s', (snd . fst) <$> xs), snd s')
-        Just s' -> case ep of
-          EPDiscard -> (fst s', [])
-          EPReturn -> ((fst $ fst s', []), snd s')
+            ((s', _), _) : _ -> 
+              let evs = 
+                    case ep of
+                      EPDiscard -> []
+                      EPReturn -> concatMap snd xs
+              in ((s', (snd . fst) <$> xs), evs)
+        Just ((s', _), _) ->
+          let evs = 
+                case ep of
+                  EPDiscard -> []
+                  EPReturn -> concatMap snd xs
+          in ((s', []), evs)
 
     applySTSInternal' ::
       SRuleType rtype ->
       RuleContext rtype s ->
-      m [EventReturnType ep s (State s, [PredicateFailure s])]
+      m [((State s, [PredicateFailure s]), [Event s])]
     applySTSInternal' SInitial env =
       goRule env `traverse` initialRules
     applySTSInternal' STransition jc = do
@@ -578,8 +573,8 @@ applySTSInternal ep ap goRule ctx =
       res <- goRule jc `traverse` transitionRules
       -- We only care about running postconditions if the state transition was
       -- successful.
-      !_ <- case (assertPost ap, discardEvents ep @s (successOrFirstFailure res) :: (State s, [[PredicateFailure s]])) of
-        (True, (st, [])) ->
+      !_ <- case (assertPost ap, successOrFirstFailure res) of
+        (True, ((st, []), _)) ->
           sfor_ (assertions @s)
             $! ( \case
                    PostCondition msg cond ->
diff --git a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
index 108b010d4bd..8e7f88a471e 100644
--- a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
+++ b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
@@ -498,8 +498,8 @@ applySTSTest ::
   m (Either [[PredicateFailure s]] (State s))
 applySTSTest ctx =
   applySTSOpts EPDiscard defaultOpts ctx <&> \case
-    (st, []) -> Right st
-    (_, pfs) -> Left pfs
+    ((st, []), _) -> Right st
+    ((_, pfs), _) -> Left pfs
   where
     defaultOpts =
       ApplySTSOpts
diff --git a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
index 6a0afb6520f..0102fd4ba79 100644
--- a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
+++ b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
@@ -327,8 +327,8 @@ applySTSTest ::
   m (Either [[PredicateFailure s]] (State s))
 applySTSTest ctx =
   applySTSOpts EPDiscard defaultOpts ctx <&> \case
-    (st, []) -> Right st
-    (_, pfs) -> Left pfs
+    ((st, []), _) -> Right st
+    ((_, pfs), _) -> Left pfs
   where
     defaultOpts =
       ApplySTSOpts

From ad0975ad024660650f676917e798655b88a34d69 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Wed, 2 Jun 2021 18:17:47 -0400
Subject: [PATCH 18/22] simplify runClause

---
 .../executable-spec/src/Control/State/Transition/Extended.hs  | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index 725f90dcc88..14899062333 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -500,9 +500,7 @@ applyRuleInternal ep vp goSTS jc r =
     runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do
       ((ss, sfails), sevents) :: ((State sub, [[PredicateFailure sub]]), [Event sub]) <- lift $ goSTS subCtx
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
-      () <- case ep of
-        EPDiscard -> pure ()
-        EPReturn -> tell $ fmap wrapEvent sevents
+      runClause $ Writer (fmap wrapEvent sevents) ()
       pure $ next ss
     runClause (Writer w a) = case ep of
       EPReturn -> tell w $> a

From ecfd8ebc4ffe8c57abb1f9e0ad8496d6fd23a44b Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Tue, 8 Jun 2021 14:21:15 -0400
Subject: [PATCH 19/22] Revert "simplify runClause"

This reverts commit ad0975ad024660650f676917e798655b88a34d69.
---
 .../executable-spec/src/Control/State/Transition/Extended.hs  | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index 14899062333..725f90dcc88 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -500,7 +500,9 @@ applyRuleInternal ep vp goSTS jc r =
     runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do
       ((ss, sfails), sevents) :: ((State sub, [[PredicateFailure sub]]), [Event sub]) <- lift $ goSTS subCtx
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
-      runClause $ Writer (fmap wrapEvent sevents) ()
+      () <- case ep of
+        EPDiscard -> pure ()
+        EPReturn -> tell $ fmap wrapEvent sevents
       pure $ next ss
     runClause (Writer w a) = case ep of
       EPReturn -> tell w $> a

From 8e38d5cb822ed095227f4296dc2af397e036a9e7 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Tue, 8 Jun 2021 14:21:22 -0400
Subject: [PATCH 20/22] Revert "factor out EventReturnType"

This reverts commit 58e3a659651acfd797f697c0c288fa3c38d4c95f.
---
 .../Cardano/Ledger/Rules/ValidationMode.hs    |  4 +-
 .../src/Control/State/Transition/Extended.hs  | 81 ++++++++++---------
 .../src/Control/State/Transition/Trace.hs     |  4 +-
 .../src/Test/Shelley/Spec/Ledger/Utils.hs     |  4 +-
 4 files changed, 49 insertions(+), 44 deletions(-)

diff --git a/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs b/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
index adb6bf8d3a2..cba9cbcf9cf 100644
--- a/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
+++ b/cardano-ledger-core/src/Cardano/Ledger/Rules/ValidationMode.hs
@@ -30,8 +30,8 @@ applySTSValidateSuchThat ::
   m (Either [[PredicateFailure s]] (State s))
 applySTSValidateSuchThat cond ctx =
   applySTSOpts EPDiscard opts ctx <&> \case
-    ((st, []), _) -> Right st
-    ((_, pfs), _) -> Left pfs
+    (st, []) -> Right st
+    (_, pfs) -> Left pfs
   where
     opts =
       ApplySTSOpts
diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index 725f90dcc88..f1704adebb1 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -40,6 +40,7 @@ module Control.State.Transition.Extended
     Label,
     SingEP(..),
     EventPolicy(..),
+    EventReturnType,
     EventConstraintType,
     labeledPred,
     labeledPredE,
@@ -242,10 +243,19 @@ data SingEP ep where
   EPReturn  :: SingEP 'EventPolicyReturn
   EPDiscard :: SingEP 'EventPolicyDiscard
 
+type family EventReturnType ep sts a :: Type where
+  EventReturnType 'EventPolicyReturn sts a = (a, [Event sts])
+  EventReturnType _ _ a = a
+
 type family EventConstraintType e sts m :: Constraint where
   EventConstraintType 'EventPolicyReturn sts m = MonadWriter [Event sts] m
   EventConstraintType _ _ _ = ()
 
+discardEvents :: forall ep a. SingEP ep -> forall s. EventReturnType ep s a -> a
+discardEvents ep = case ep of
+  EPReturn -> fst
+  EPDiscard -> id
+
 data Clause sts (rtype :: RuleType) a where
   Lift ::
     STS sts =>
@@ -361,18 +371,18 @@ data ApplySTSOpts = ApplySTSOpts
     asoValidation :: ValidationPolicy
   }
 
-type STSInterpreter =
+type STSInterpreter ep =
   forall s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
   RuleContext rtype s ->
-  m ((State s, [[PredicateFailure s]]), [Event s])
+  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
 
-type RuleInterpreter =
+type RuleInterpreter ep =
   forall s m rtype.
   (STS s, RuleTypeRep rtype, m ~ BaseM s) =>
   RuleContext rtype s ->
   Rule s rtype (State s) ->
-  m ((State s, [PredicateFailure s]), [Event s])
+  m (EventReturnType ep s (State s, [PredicateFailure s]))
 
 -- | Apply an STS with options. Note that this returns both the final state and
 -- the list of predicate failures.
@@ -382,11 +392,11 @@ applySTSOpts ::
   SingEP ep ->
   ApplySTSOpts ->
   RuleContext rtype s ->
-  m ((State s, [[PredicateFailure s]]), [Event s])
+  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
 applySTSOpts ep ApplySTSOpts {asoAssertions, asoValidation} ctx =
-  let goRule :: RuleInterpreter
+  let goRule :: RuleInterpreter ep
       goRule = applyRuleInternal ep asoValidation goSTS
-      goSTS :: STSInterpreter
+      goSTS :: STSInterpreter ep
       goSTS = applySTSInternal ep asoAssertions goRule
    in goSTS ctx
 
@@ -397,8 +407,8 @@ applySTS ::
   m (Either [[PredicateFailure s]] (State s))
 applySTS ctx =
   applySTSOpts EPDiscard defaultOpts ctx <&> \case
-    ((st, []), _) -> Right st
-    ((_, pfs), _) -> Left pfs
+    (st, []) -> Right st
+    (_, pfs) -> Left pfs
   where
 
 #ifdef STS_ASSERT
@@ -426,7 +436,7 @@ reapplySTS ::
   RuleContext rtype s ->
   m (State s)
 reapplySTS ctx =
-  applySTSOpts EPDiscard defaultOpts ctx <&> (fst . fst)
+  applySTSOpts EPDiscard defaultOpts ctx <&> fst
   where
     defaultOpts =
       ApplySTSOpts
@@ -440,7 +450,7 @@ applySTSIndifferently ::
   RuleContext rtype s ->
   m (State s, [[PredicateFailure s]])
 applySTSIndifferently =
-  fmap fst . applySTSOpts EPDiscard opts
+  applySTSOpts EPDiscard opts
   where
     opts =
       ApplySTSOpts
@@ -469,16 +479,14 @@ applyRuleInternal ::
   SingEP ep ->
   ValidationPolicy ->
   -- | Interpreter for subsystems
-  STSInterpreter ->
+  STSInterpreter ep ->
   RuleContext rtype s ->
   Rule s rtype (State s) ->
-  m ((State s, [PredicateFailure s]), [Event s])
+  m (EventReturnType ep s (State s, [PredicateFailure s]))
 applyRuleInternal ep vp goSTS jc r =
   case ep of
     EPReturn -> flip (runRuleEventLoggerT @s) [] $ foldF runClause r
-    EPDiscard -> do 
-      s <- flip runStateT [] $ foldF runClause r
-      pure (s, [])
+    EPDiscard -> flip runStateT [] $ foldF runClause r
   where
     runClause :: forall f t a.
       ( f ~ t m
@@ -498,11 +506,14 @@ applyRuleInternal ep vp goSTS jc r =
             Right x -> pure x
         else pure val
     runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do
-      ((ss, sfails), sevents) :: ((State sub, [[PredicateFailure sub]]), [Event sub]) <- lift $ goSTS subCtx
+      s :: (EventReturnType ep sub (State sub, [[PredicateFailure sub]])) <- lift $ goSTS subCtx
+      let ss :: State sub
+          sfails :: [[PredicateFailure sub]]
+          (ss, sfails) = (discardEvents ep @sub) s
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
       () <- case ep of
         EPDiscard -> pure ()
-        EPReturn -> tell $ fmap wrapEvent sevents
+        EPReturn -> tell (wrapEvent <$> snd s)
       pure $ next ss
     runClause (Writer w a) = case ep of
       EPReturn -> tell w $> a
@@ -518,37 +529,31 @@ applySTSInternal ::
   SingEP ep ->
   AssertionPolicy ->
   -- | Interpreter for rules
-  RuleInterpreter ->
+  RuleInterpreter ep ->
   RuleContext rtype s ->
-  m ((State s, [[PredicateFailure s]]), [Event s])
+  m (EventReturnType ep s (State s, [[PredicateFailure s]]))
 applySTSInternal ep ap goRule ctx =
   successOrFirstFailure <$> applySTSInternal' rTypeRep ctx
   where
     successOrFirstFailure ::
-         [((State s, [PredicateFailure s]), [Event s])]
-      -> ((State s, [[PredicateFailure s]]), [Event s])
+         [EventReturnType ep s (State s, [PredicateFailure s])]
+      -> EventReturnType ep s (State s, [[PredicateFailure s]])
     successOrFirstFailure xs =
-      case find (null . snd . fst) xs of
+      case find (\x -> null $ snd $ (discardEvents ep @s x :: (State s, [PredicateFailure s]))) xs of
         Nothing ->
           case xs of
             [] -> error "applySTSInternal was called with an empty set of rules"
-            ((s', _), _) : _ -> 
-              let evs = 
-                    case ep of
-                      EPDiscard -> []
-                      EPReturn -> concatMap snd xs
-              in ((s', (snd . fst) <$> xs), evs)
-        Just ((s', _), _) ->
-          let evs = 
-                case ep of
-                  EPDiscard -> []
-                  EPReturn -> concatMap snd xs
-          in ((s', []), evs)
+            s' : _ -> case ep of
+              EPDiscard -> (fst s', snd <$> xs)
+              EPReturn -> ((fst $ fst s', (snd . fst) <$> xs), snd s')
+        Just s' -> case ep of
+          EPDiscard -> (fst s', [])
+          EPReturn -> ((fst $ fst s', []), snd s')
 
     applySTSInternal' ::
       SRuleType rtype ->
       RuleContext rtype s ->
-      m [((State s, [PredicateFailure s]), [Event s])]
+      m [EventReturnType ep s (State s, [PredicateFailure s])]
     applySTSInternal' SInitial env =
       goRule env `traverse` initialRules
     applySTSInternal' STransition jc = do
@@ -573,8 +578,8 @@ applySTSInternal ep ap goRule ctx =
       res <- goRule jc `traverse` transitionRules
       -- We only care about running postconditions if the state transition was
       -- successful.
-      !_ <- case (assertPost ap, successOrFirstFailure res) of
-        (True, ((st, []), _)) ->
+      !_ <- case (assertPost ap, discardEvents ep @s (successOrFirstFailure res) :: (State s, [[PredicateFailure s]])) of
+        (True, (st, [])) ->
           sfor_ (assertions @s)
             $! ( \case
                    PostCondition msg cond ->
diff --git a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
index 8e7f88a471e..108b010d4bd 100644
--- a/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
+++ b/semantics/small-steps-test/src/Control/State/Transition/Trace.hs
@@ -498,8 +498,8 @@ applySTSTest ::
   m (Either [[PredicateFailure s]] (State s))
 applySTSTest ctx =
   applySTSOpts EPDiscard defaultOpts ctx <&> \case
-    ((st, []), _) -> Right st
-    ((_, pfs), _) -> Left pfs
+    (st, []) -> Right st
+    (_, pfs) -> Left pfs
   where
     defaultOpts =
       ApplySTSOpts
diff --git a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
index 0102fd4ba79..6a0afb6520f 100644
--- a/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
+++ b/shelley/chain-and-ledger/shelley-spec-ledger-test/src/Test/Shelley/Spec/Ledger/Utils.hs
@@ -327,8 +327,8 @@ applySTSTest ::
   m (Either [[PredicateFailure s]] (State s))
 applySTSTest ctx =
   applySTSOpts EPDiscard defaultOpts ctx <&> \case
-    ((st, []), _) -> Right st
-    ((_, pfs), _) -> Left pfs
+    (st, []) -> Right st
+    (_, pfs) -> Left pfs
   where
     defaultOpts =
       ApplySTSOpts

From 88f70e3af077605f48f36ba87dd537934e8132cd Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Wed, 2 Jun 2021 18:17:47 -0400
Subject: [PATCH 21/22] simplify runClause

---
 .../executable-spec/src/Control/State/Transition/Extended.hs  | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index f1704adebb1..cf534430263 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -511,9 +511,7 @@ applyRuleInternal ep vp goSTS jc r =
           sfails :: [[PredicateFailure sub]]
           (ss, sfails) = (discardEvents ep @sub) s
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
-      () <- case ep of
-        EPDiscard -> pure ()
-        EPReturn -> tell (wrapEvent <$> snd s)
+      runClause $ Writer (fmap wrapEvent sevents) ()
       pure $ next ss
     runClause (Writer w a) = case ep of
       EPReturn -> tell w $> a

From 96a5629ac533c7b3d7516bde9b76ff3c903520a1 Mon Sep 17 00:00:00 2001
From: Zachary Churchill <zacharyachurchill@gmail.com>
Date: Tue, 8 Jun 2021 14:48:39 -0400
Subject: [PATCH 22/22] fix simplify runClause with EventReturnType

---
 .../src/Control/State/Transition/Extended.hs             | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/semantics/executable-spec/src/Control/State/Transition/Extended.hs b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
index cf534430263..10c486f0a03 100644
--- a/semantics/executable-spec/src/Control/State/Transition/Extended.hs
+++ b/semantics/executable-spec/src/Control/State/Transition/Extended.hs
@@ -256,6 +256,11 @@ discardEvents ep = case ep of
   EPReturn -> fst
   EPDiscard -> id
 
+getEvents :: forall ep. SingEP ep -> forall s a. EventReturnType ep s a -> [Event s]
+getEvents ep ert = case ep of
+  EPReturn -> snd ert
+  EPDiscard -> []
+
 data Clause sts (rtype :: RuleType) a where
   Lift ::
     STS sts =>
@@ -506,12 +511,12 @@ applyRuleInternal ep vp goSTS jc r =
             Right x -> pure x
         else pure val
     runClause (SubTrans (subCtx :: RuleContext _rtype sub) next) = do
-      s :: (EventReturnType ep sub (State sub, [[PredicateFailure sub]])) <- lift $ goSTS subCtx
+      s <- lift $ goSTS subCtx
       let ss :: State sub
           sfails :: [[PredicateFailure sub]]
           (ss, sfails) = (discardEvents ep @sub) s
       traverse_ (\a -> modify (a :)) $ wrapFailed @sub @s <$> concat sfails
-      runClause $ Writer (fmap wrapEvent sevents) ()
+      runClause $ Writer (fmap wrapEvent $ getEvents ep @sub @(State sub, [[PredicateFailure sub]]) s) ()
       pure $ next ss
     runClause (Writer w a) = case ep of
       EPReturn -> tell w $> a