Merge #1922

1922: Make STS rules above UTXO era-independent. r=mrBliss a=nc6 Honestly it's embarassing that I failed to notice that this worked. We carry a few more constraints in the STS instances and Embed instances. But the payoff is that we only have to override the specific rules we want to change in each era, and not re-plumb everything. Obviously this means that, in the future, if we make a change in a different rule then we have to go back and turn the era-independent one into an era-dependent version (and add instances for all intermediate eras). But still, this feels like a definite improvement. Co-authored-by: Nicholas Clarke <nicholas.clarke@iohk.io>
IntersectMBO · Oct 20, 2020 · d379312 · d379312
2 parents 95f9679 + ed6ca70
commit d379312
Show file tree

Hide file tree

Showing 13 changed files with 174 additions and 213 deletions.
diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Mempool.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Mempool.hs
@@ -26,13 +26,17 @@ import Cardano.Ledger.Shelley (ShelleyBased)
 import Control.Arrow (left)
 import Control.Monad.Except
 import Control.Monad.Trans.Reader (runReader)
-import Control.State.Transition.Extended (BaseM, Environment, PredicateFailure, STS, Signal, State, TRC (..), applySTS)
+import Control.State.Transition.Extended
+  ( PredicateFailure,
+    STS,
+    TRC (..),
+    applySTS,
+  )
 import Data.Sequence (Seq)
 import Shelley.Spec.Ledger.API.Validation
-import Shelley.Spec.Ledger.BaseTypes (Globals, ShelleyBase)
-import Shelley.Spec.Ledger.LedgerState (LedgerState)
+import Shelley.Spec.Ledger.BaseTypes (Globals)
 import qualified Shelley.Spec.Ledger.LedgerState as LedgerState
-import Shelley.Spec.Ledger.STS.Ledgers (LEDGERS, LedgersEnv)
+import Shelley.Spec.Ledger.STS.Ledgers (LEDGERS)
 import qualified Shelley.Spec.Ledger.STS.Ledgers as Ledgers
 import Shelley.Spec.Ledger.Slot (SlotNo)
 import Shelley.Spec.Ledger.Tx (Tx)
@@ -107,10 +111,6 @@ instance
 applyTxs ::
   forall era m.
   ( STS (LEDGERS era),
-    BaseM (LEDGERS era) ~ ShelleyBase,
-    Environment (LEDGERS era) ~ LedgersEnv era,
-    State (LEDGERS era) ~ LedgerState era,
-    Signal (LEDGERS era) ~ Seq (Tx era),
     MonadError (ApplyTxError era) m
   ) =>
   Globals ->

diff --git a/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Validation.hs b/shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/API/Validation.hs
@@ -29,7 +29,7 @@ import Control.Monad.Trans.Reader (runReader)
 import Control.State.Transition.Extended
 import GHC.Generics (Generic)
 import NoThunks.Class (NoThunks (..))
-import Shelley.Spec.Ledger.BaseTypes (Globals (..), ShelleyBase)
+import Shelley.Spec.Ledger.BaseTypes (Globals (..))
 import Shelley.Spec.Ledger.BlockChain
 import qualified Shelley.Spec.Ledger.LedgerState as LedgerState
 import qualified Shelley.Spec.Ledger.STS.Bbody as STS
@@ -46,7 +46,6 @@ type ShelleyState = LedgerState.NewEpochState
 chainChecks ::
   forall era m.
   ( Era era,
-    PredicateFailure (STS.CHAIN era) ~ STS.ChainPredicateFailure era,
     MonadError (STS.PredicateFailure (STS.CHAIN era)) m
   ) =>
   Globals ->
@@ -126,10 +125,6 @@ instance
 applyBlockTransition ::
   forall era m.
   ( STS (STS.BBODY era),
-    BaseM (STS.BBODY era) ~ ShelleyBase,
-    Environment (STS.BBODY era) ~ STS.BbodyEnv era,
-    State (STS.BBODY era) ~ STS.BbodyState era,
-    Signal (STS.BBODY era) ~ Block era,
     MonadError (BlockTransitionError era) m
   ) =>
   Globals ->
@@ -163,11 +158,7 @@ applyBlockTransition globals state blk =
 --   `applyBlockTransition` on the same block and that this was successful.
 reapplyBlockTransition ::
   forall era.
-  ( STS (STS.BBODY era),
-    BaseM (STS.BBODY era) ~ ShelleyBase,
-    Environment (STS.BBODY era) ~ STS.BbodyEnv era,
-    State (STS.BBODY era) ~ STS.BbodyState era,
-    Signal (STS.BBODY era) ~ Block era
+  ( STS (STS.BBODY era)
   ) =>
   Globals ->
   ShelleyState era ->

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
@@ -20,9 +20,8 @@ module Shelley.Spec.Ledger.STS.Bbody
   )
 where
 
-import qualified Cardano.Ledger.Crypto as CryptoClass
 import Cardano.Ledger.Era (Era (Crypto))
-import Cardano.Ledger.Shelley (ShelleyBased, ShelleyEra)
+import Cardano.Ledger.Shelley (ShelleyBased)
 import Control.Monad.Trans.Reader (asks)
 import Control.State.Transition
   ( Embed (..),
@@ -34,7 +33,6 @@ import Control.State.Transition
     trans,
     (?!),
   )
-import Data.Sequence (Seq)
 import qualified Data.Sequence.Strict as StrictSeq
 import GHC.Generics (Generic)
 import NoThunks.Class (NoThunks (..))
@@ -61,7 +59,6 @@ import Shelley.Spec.Ledger.OverlaySchedule (isOverlaySlot)
 import Shelley.Spec.Ledger.PParams (PParams, PParams' (..))
 import Shelley.Spec.Ledger.STS.Ledgers (LEDGERS, LedgersEnv (..))
 import Shelley.Spec.Ledger.Slot (epochInfoEpoch, epochInfoFirst)
-import Shelley.Spec.Ledger.Tx (Tx)
 import Shelley.Spec.Ledger.TxBody (EraIndependentTxBody)
 
 data BBODY era
@@ -107,40 +104,34 @@ instance
   NoThunks (BbodyPredicateFailure era)
 
 instance
-  ( CryptoClass.Crypto c,
-    DSignable c (Hash c EraIndependentTxBody)
+  ( Era era,
+    ShelleyBased era,
+    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
+    Embed (LEDGERS era) (BBODY era)
   ) =>
-  STS (BBODY (ShelleyEra c))
+  STS (BBODY era)
   where
   type
-    State (BBODY (ShelleyEra c)) =
-      BbodyState (ShelleyEra c)
+    State (BBODY era) =
+      BbodyState era
 
   type
-    Signal (BBODY (ShelleyEra c)) =
-      Block (ShelleyEra c)
+    Signal (BBODY era) =
+      Block era
 
-  type Environment (BBODY (ShelleyEra c)) = BbodyEnv (ShelleyEra c)
+  type Environment (BBODY era) = BbodyEnv era
 
-  type BaseM (BBODY (ShelleyEra c)) = ShelleyBase
+  type BaseM (BBODY era) = ShelleyBase
 
-  type PredicateFailure (BBODY (ShelleyEra c)) = BbodyPredicateFailure (ShelleyEra c)
+  type PredicateFailure (BBODY era) = BbodyPredicateFailure era
 
   initialRules = []
   transitionRules = [bbodyTransition]
 
 bbodyTransition ::
   forall era.
   ( ShelleyBased era,
-    BaseM (BBODY era) ~ ShelleyBase,
-    Embed (LEDGERS era) (BBODY era),
-    Environment (BBODY era) ~ BbodyEnv era,
-    State (BBODY era) ~ BbodyState era,
-    Signal (BBODY era) ~ Block era,
-    PredicateFailure (BBODY era) ~ BbodyPredicateFailure era,
-    Environment (LEDGERS era) ~ LedgersEnv era,
-    State (LEDGERS era) ~ LedgerState era,
-    Signal (LEDGERS era) ~ Seq (Tx era)
+    Embed (LEDGERS era) (BBODY era)
   ) =>
   TransitionRule (BBODY era)
 bbodyTransition =
@@ -183,9 +174,11 @@ bbodyTransition =
             )
 
 instance
-  ( CryptoClass.Crypto c,
-    DSignable c (Hash c EraIndependentTxBody)
+  ( Era era,
+    STS (LEDGERS era),
+    DSignable (Crypto era) (Hash (Crypto era) EraIndependentTxBody),
+    ShelleyBased era
   ) =>
-  Embed (LEDGERS (ShelleyEra c)) (BBODY (ShelleyEra c))
+  Embed (LEDGERS era) (BBODY era)
   where
   wrapFailed = LedgersFailure
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
@@ -30,9 +30,8 @@ where
 
 import qualified Cardano.Crypto.VRF as VRF
 import Cardano.Ledger.Crypto (VRF)
-import qualified Cardano.Ledger.Crypto as CryptoClass
 import Cardano.Ledger.Era (Crypto, Era)
-import Cardano.Ledger.Shelley (ShelleyBased, ShelleyEra)
+import Cardano.Ledger.Shelley (ShelleyBased)
 import qualified Cardano.Ledger.Val as Val
 import Cardano.Slotting.Slot (WithOrigin (..))
 import Control.DeepSeq (NFData)
@@ -225,26 +224,32 @@ initialShelleyState lab e utxo reserves genDelegs pp initNonce =
     cs = Map.fromList (fmap (\(GenDelegPair hk _) -> (coerceKeyRole hk, 0)) (Map.elems genDelegs))
 
 instance
-  ( CryptoClass.Crypto c,
+  ( Era era,
+    c ~ Crypto era,
+    ShelleyBased era,
+    Embed (BBODY era) (CHAIN era),
+    Embed TICKN (CHAIN era),
+    Embed (TICK era) (CHAIN era),
+    Embed (PRTCL (Crypto era)) (CHAIN era),
     DSignable c (OCertSignable c),
     DSignable c (Hash c EraIndependentTxBody),
     KESignable c (BHBody c),
     VRF.Signable (VRF c) Seed
   ) =>
-  STS (CHAIN (ShelleyEra c))
+  STS (CHAIN era)
   where
   type
-    State (CHAIN (ShelleyEra c)) =
-      ChainState (ShelleyEra c)
+    State (CHAIN era) =
+      ChainState era
 
   type
-    Signal (CHAIN (ShelleyEra c)) =
-      Block (ShelleyEra c)
+    Signal (CHAIN era) =
+      Block era
 
-  type Environment (CHAIN (ShelleyEra c)) = ()
-  type BaseM (CHAIN (ShelleyEra c)) = ShelleyBase
+  type Environment (CHAIN era) = ()
+  type BaseM (CHAIN era) = ShelleyBase
 
-  type PredicateFailure (CHAIN (ShelleyEra c)) = ChainPredicateFailure (ShelleyEra c)
+  type PredicateFailure (CHAIN era) = ChainPredicateFailure era
 
   initialRules = []
   transitionRules = [chainTransition]
@@ -266,7 +271,6 @@ pparamsToChainChecksData pp =
 
 chainChecks ::
   ( Era era,
-    PredicateFailure (CHAIN era) ~ ChainPredicateFailure era,
     MonadError (PredicateFailure (CHAIN era)) m
   ) =>
   Natural ->
@@ -287,14 +291,7 @@ chainChecks maxpv ccd bh = do
 chainTransition ::
   forall era.
   ( ShelleyBased era,
-    BaseM (CHAIN era) ~ ShelleyBase,
-    State (CHAIN era) ~ ChainState era,
-    Signal (CHAIN era) ~ Block era,
-    PredicateFailure (CHAIN era) ~ ChainPredicateFailure era,
     Embed (BBODY era) (CHAIN era),
-    Environment (BBODY era) ~ BbodyEnv era,
-    State (BBODY era) ~ BbodyState era,
-    Signal (BBODY era) ~ Block era,
     Embed TICKN (CHAIN era),
     Embed (TICK era) (CHAIN era),
     Embed (PRTCL (Crypto era)) (CHAIN era)
@@ -372,46 +369,42 @@ chainTransition =
         pure $ ChainState nes'' cs' eta0' etaV' etaC' etaH' lab'
 
 instance
-  ( CryptoClass.Crypto c,
-    DSignable c (OCertSignable c),
-    DSignable c (Hash c EraIndependentTxBody),
-    KESignable c (BHBody c),
-    VRF.Signable (VRF c) Seed
+  ( Era era,
+    ShelleyBased era,
+    STS (CHAIN era),
+    STS (BBODY era)
   ) =>
-  Embed (BBODY (ShelleyEra c)) (CHAIN (ShelleyEra c))
+  Embed (BBODY era) (CHAIN era)
   where
   wrapFailed = BbodyFailure
 
 instance
-  ( CryptoClass.Crypto c,
-    DSignable c (OCertSignable c),
-    DSignable c (Hash c EraIndependentTxBody),
-    KESignable c (BHBody c),
-    VRF.Signable (VRF c) Seed
+  ( Era era,
+    ShelleyBased era,
+    STS (CHAIN era)
   ) =>
-  Embed TICKN (CHAIN (ShelleyEra c))
+  Embed TICKN (CHAIN era)
   where
   wrapFailed = TicknFailure
 
 instance
-  ( CryptoClass.Crypto c,
-    DSignable c (OCertSignable c),
-    DSignable c (Hash c EraIndependentTxBody),
-    KESignable c (BHBody c),
-    VRF.Signable (VRF c) Seed
+  ( Era era,
+    ShelleyBased era,
+    STS (CHAIN era),
+    STS (TICK era)
   ) =>
-  Embed (TICK (ShelleyEra c)) (CHAIN (ShelleyEra c))
+  Embed (TICK era) (CHAIN era)
   where
   wrapFailed = TickFailure
 
 instance
-  ( CryptoClass.Crypto c,
-    DSignable c (OCertSignable c),
-    DSignable c (Hash c EraIndependentTxBody),
-    KESignable c (BHBody c),
-    VRF.Signable (VRF c) Seed
+  ( Era era,
+    c ~ Crypto era,
+    ShelleyBased era,
+    STS (CHAIN era),
+    STS (PRTCL c)
   ) =>
-  Embed (PRTCL c) (CHAIN (ShelleyEra c))
+  Embed (PRTCL c) (CHAIN era)
   where
   wrapFailed = PrtclFailure
 

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
@@ -27,9 +27,8 @@ import Cardano.Binary
     encodeListLen,
   )
 import qualified Cardano.Ledger.Core as Core
-import qualified Cardano.Ledger.Crypto as CryptoClass
 import Cardano.Ledger.Era (Crypto, Era)
-import Cardano.Ledger.Shelley (ShelleyBased, ShelleyEra)
+import Cardano.Ledger.Shelley (ShelleyBased)
 import Control.Monad.Trans.Reader (asks)
 import Control.SetAlgebra (dom, eval, (∈), (⨃))
 import Control.State.Transition
@@ -109,19 +108,25 @@ data DelegsPredicateFailure era
   | DelplFailure (PredicateFailure (DELPL era)) -- Subtransition Failures
   deriving (Show, Eq, Generic)
 
-instance CryptoClass.Crypto c => STS (DELEGS (ShelleyEra c)) where
-  type State (DELEGS (ShelleyEra c)) = DPState (ShelleyEra c)
-  type Signal (DELEGS (ShelleyEra c)) = Seq (DCert (ShelleyEra c))
-  type Environment (DELEGS (ShelleyEra c)) = DelegsEnv (ShelleyEra c)
-  type BaseM (DELEGS (ShelleyEra c)) = ShelleyBase
+instance
+  ( Era era,
+    ShelleyBased era,
+    HasField "wdrls" (Core.TxBody era) (Wdrl era)
+  ) =>
+  STS (DELEGS era)
+  where
+  type State (DELEGS era) = DPState era
+  type Signal (DELEGS era) = Seq (DCert era)
+  type Environment (DELEGS era) = DelegsEnv era
+  type BaseM (DELEGS era) = ShelleyBase
   type
-    PredicateFailure (DELEGS (ShelleyEra c)) =
-      DelegsPredicateFailure (ShelleyEra c)
+    PredicateFailure (DELEGS era) =
+      DelegsPredicateFailure era
 
   initialRules = [pure emptyDelegation]
   transitionRules = [delegsTransition]
 
-instance NoThunks (DelegsPredicateFailure (ShelleyEra c))
+instance NoThunks (DelegsPredicateFailure era)
 
 instance
   (Typeable era, Era era) =>
@@ -163,11 +168,6 @@ delegsTransition ::
   forall era.
   ( ShelleyBased era,
     HasField "wdrls" (Core.TxBody era) (Wdrl era),
-    State (DELEGS era) ~ DPState era,
-    Environment (DELEGS era) ~ DelegsEnv era,
-    PredicateFailure (DELEGS era)
-      ~ DelegsPredicateFailure era,
-    Signal (DELEGS era) ~ Seq (DCert era),
     Embed (DELPL era) (DELEGS era)
   ) =>
   TransitionRule (DELEGS era)
@@ -229,7 +229,10 @@ delegsTransition = do
             ]
 
 instance
-  CryptoClass.Crypto c =>
-  Embed (DELPL (ShelleyEra c)) (DELEGS (ShelleyEra c))
+  ( Era era,
+    ShelleyBased era,
+    HasField "wdrls" (Core.TxBody era) (Wdrl era)
+  ) =>
+  Embed (DELPL era) (DELEGS era)
   where
   wrapFailed = DelplFailure