Added conformance tests for various subrules

eras/alonzo/impl/CHANGELOG.md

@@ -3,6 +3,7 @@
 ## 1.8.1.0
 
 * Add `AllegraEraScript` and `ShelleyEraScript` instances for `AlonzoEra`
+* Add `Inject` instance for `AlonzoTx`
 
 ## testlib
 

eras/alonzo/impl/src/Cardano/Ledger/Alonzo/Tx.hs

@@ -107,6 +107,7 @@ import Cardano.Ledger.Alonzo.TxWits (
   txrdmrs,
   unRedeemers,
  )
+import Cardano.Ledger.BaseTypes (Inject)
 import Cardano.Ledger.Binary (
   Annotator (..),
   DecCBOR (..),
@@ -164,6 +165,8 @@ data AlonzoTx era = AlonzoTx
   }
   deriving (Generic)
 
+instance Inject (AlonzoTx era) (AlonzoTx era)
+
 newtype AlonzoTxUpgradeError = ATUEBodyUpgradeError AlonzoTxBodyUpgradeError
   deriving (Show)
 

eras/conway/impl/CHANGELOG.md

@@ -2,12 +2,27 @@
 
 ## 1.14.1.0
 
-* Add `NFData` instance for `RatifySignal`
+* Add `Inject` instances for:
+  * `EnactState`
+  * `RatifyState`
+  * `RatifySignal`
+  * `RatifyEnv`
+  * `GovProcedures`
+  * `Proposals`
+  * `CertEnv`
+  * `EnactSignal`
+  * `GovEnv`
+  * `ConwayTxCert`
+* Add `NFData` instances for:
+  * `RatifySignal`
+  * `EnactSignal`
 * Add `AllegraEraScript` and `ShelleyEraScript` instances for `ConwayEra`
 
 ### `testlib`
 
-* Add `ToExpr` instance for `RatifySignal`
+* Add `ToExpr` instances for:
+  * `RatifySignal`
+  * `EnactSignal`
 
 ## 1.14.0.0
 

eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Internal.hs

@@ -5,6 +5,7 @@
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MonoLocalBinds #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE RecordWildCards #-}
@@ -57,6 +58,7 @@ module Cardano.Ledger.Conway.Governance.Internal (
 
 import Cardano.Ledger.BaseTypes (
   EpochNo (..),
+  Inject,
   ProtVer (..),
   StrictMaybe (..),
   UnitInterval,
@@ -149,6 +151,8 @@ data EnactState era = EnactState
   }
   deriving (Generic)
 
+instance Inject (EnactState era) (EnactState era)
+
 ensCommitteeL :: Lens' (EnactState era) (StrictMaybe (Committee era))
 ensCommitteeL = lens ensCommittee (\x y -> x {ensCommittee = y})
 
@@ -266,6 +270,8 @@ data RatifyState era = RatifyState
   }
   deriving (Generic)
 
+instance Inject (RatifyState era) (RatifyState era)
+
 deriving instance EraPParams era => Eq (RatifyState era)
 
 deriving instance EraPParams era => Show (RatifyState era)
@@ -533,6 +539,8 @@ reorderActions = SS.fromList . sortOn (actionPriority . gasAction) . toList
 newtype RatifySignal era = RatifySignal (StrictSeq (GovActionState era))
   deriving (Eq, Show, Generic)
 
+instance Inject (RatifySignal era) (RatifySignal era)
+
 instance EraPParams era => NFData (RatifySignal era)
 
 data RatifyEnv era = RatifyEnv
@@ -545,6 +553,7 @@ data RatifyEnv era = RatifyEnv
   }
   deriving (Generic)
 
+instance Inject (RatifyEnv era) (RatifyEnv era)
 deriving instance Show (RatifyEnv era)
 deriving instance Eq (RatifyEnv era)
 

eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Procedures.hs

@@ -81,6 +81,7 @@ import Cardano.Ledger.Babbage.Core
 import Cardano.Ledger.BaseTypes (
   Anchor (..),
   AnchorData (..),
+  Inject,
   ProtVer,
   UnitInterval,
   maybeToStrictMaybe,
@@ -468,6 +469,8 @@ data GovProcedures era = GovProcedures
   }
   deriving (Eq, Generic)
 
+instance Inject (GovProcedures era) (GovProcedures era)
+
 govProceduresProposalsL :: Lens' (GovProcedures era) (OSet.OSet (ProposalProcedure era))
 govProceduresProposalsL = lens gpProposalProcedures $ \x y -> x {gpProposalProcedures = y}
 

eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs

@@ -115,6 +115,7 @@ module Cardano.Ledger.Conway.Governance.Proposals (
 
 import Cardano.Ledger.Address (rewardAccountCredentialL)
 import Cardano.Ledger.BaseTypes (
+  Inject,
   StrictMaybe (..),
   isSJust,
   isSNothing,
@@ -223,6 +224,8 @@ data Proposals era = Proposals
   deriving stock (Show, Eq, Generic)
   deriving anyclass (NoThunks, NFData, Default)
 
+instance Inject (Proposals era) (Proposals era)
+
 pPropsL :: Lens' (Proposals era) (OMap.OMap (GovActionId (EraCrypto era)) (GovActionState era))
 pPropsL = lens pProps $ \x y -> x {pProps = y}
 

eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Cert.hs

@@ -22,7 +22,7 @@ module Cardano.Ledger.Conway.Rules.Cert (
   CertEnv (..),
 ) where
 
-import Cardano.Ledger.BaseTypes (EpochNo, ShelleyBase, SlotNo)
+import Cardano.Ledger.BaseTypes (EpochNo, Inject, ShelleyBase, SlotNo)
 import Cardano.Ledger.Binary (DecCBOR (..), EncCBOR (..))
 import Cardano.Ledger.Binary.Coders
 import Cardano.Ledger.Conway.Core
@@ -76,6 +76,8 @@ data CertEnv era = CertEnv
   }
   deriving (Generic)
 
+instance Inject (CertEnv era) (CertEnv era)
+
 deriving instance Eq (PParams era) => Eq (CertEnv era)
 deriving instance Show (PParams era) => Show (CertEnv era)
 

eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Enact.hs

@@ -36,6 +36,7 @@ import Cardano.Ledger.Conway.Governance (
 import Cardano.Ledger.Credential (Credential)
 import Cardano.Ledger.Keys (KeyRole (..))
 import Cardano.Ledger.Val (Val (..))
+import Control.DeepSeq (NFData)
 import Control.State.Transition.Extended (
   STS (..),
   TRC (..),
@@ -57,6 +58,9 @@ data EnactSignal era = EnactSignal
   }
   deriving (Eq, Show, Generic)
 
+instance EraPParams era => NFData (EnactSignal era)
+instance Inject (EnactSignal era) (EnactSignal era)
+
 instance EraGov era => STS (ConwayENACT era) where
   type Environment (ConwayENACT era) = ()
   type PredicateFailure (ConwayENACT era) = Void

eras/conway/impl/src/Cardano/Ledger/Conway/Rules/Gov.hs

@@ -29,6 +29,7 @@ import Cardano.Ledger.Address (RewardAccount, raNetwork)
 import Cardano.Ledger.BaseTypes (
   EpochInterval (..),
   EpochNo (..),
+  Inject,
   Network,
   ProtVer,
   ShelleyBase,
@@ -130,6 +131,7 @@ data GovEnv era = GovEnv
 instance (NFData (PParams era), Era era) => NFData (GovEnv era)
 deriving instance (Show (PParams era), Era era) => Show (GovEnv era)
 deriving instance Eq (PParams era) => Eq (GovEnv era)
+instance Inject (GovEnv era) (GovEnv era)
 
 data ConwayGovPredFailure era
   = GovActionsDoNotExist (NonEmpty (GovActionId (EraCrypto era)))

eras/conway/impl/src/Cardano/Ledger/Conway/TxCert.hs

@@ -3,6 +3,7 @@
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE PatternSynonyms #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -45,7 +46,7 @@ module Cardano.Ledger.Conway.TxCert (
 where
 
 import Cardano.Ledger.Babbage.Core
-import Cardano.Ledger.BaseTypes (StrictMaybe (..), invalidKey, kindObject)
+import Cardano.Ledger.BaseTypes (Inject, StrictMaybe (..), invalidKey, kindObject)
 import Cardano.Ledger.Binary (
   DecCBOR (..),
   Decoder,
@@ -516,6 +517,8 @@ data ConwayTxCert era
   | ConwayTxCertGov !(ConwayGovCert (EraCrypto era))
   deriving (Show, Generic, Eq, Ord)
 
+instance Inject (ConwayTxCert era) (ConwayTxCert era)
+
 instance Crypto (EraCrypto era) => NFData (ConwayTxCert era)
 
 instance NoThunks (ConwayTxCert era)

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/TreeDiff.hs

@@ -255,3 +255,5 @@ instance ToExpr (PParams era) => ToExpr (CertEnv era)
 instance ToExpr (PParams era) => ToExpr (ConwayDelegEnv era)
 
 instance ToExpr (PParamsHKD StrictMaybe era) => ToExpr (RatifySignal era)
+
+instance ToExpr (PParamsHKD StrictMaybe era) => ToExpr (EnactSignal era)

eras/shelley/impl/CHANGELOG.md

@@ -12,6 +12,9 @@
 * Change signatures of `evalMultiSig` and `validateMultiSig`:
   * replace `Era` constraint with `ShelleyEraScript`
   * replace `MultiSig` with `NativeScript`
+* Add `Inject` instances for:
+  * `UTxOState`
+  * `UtxoEnv`
 
 ### testlib
 * Change signatures of `Arbitrary` instances for `MultiSig`:

eras/shelley/impl/src/Cardano/Ledger/Shelley/LedgerState/Types.hs

@@ -24,6 +24,7 @@ module Cardano.Ledger.Shelley.LedgerState.Types where
 import Cardano.Ledger.BaseTypes (
   BlocksMade (..),
   EpochNo,
+  Inject,
   StrictMaybe (..),
  )
 import Cardano.Ledger.Binary (
@@ -285,6 +286,8 @@ data UTxOState era = UTxOState
   }
   deriving (Generic)
 
+instance Inject (UTxOState era) (UTxOState era)
+
 instance
   ( EraTxOut era
   , NFData (GovState era)

eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Utxo.hs

@@ -45,7 +45,7 @@ import Cardano.Ledger.Address (
   getNetwork,
   raNetwork,
  )
-import Cardano.Ledger.BaseTypes (Network, ShelleyBase, StrictMaybe, invalidKey, networkId)
+import Cardano.Ledger.BaseTypes (Inject, Network, ShelleyBase, StrictMaybe, invalidKey, networkId)
 import Cardano.Ledger.Binary (
   DecCBOR (..),
   EncCBOR (..),
@@ -131,6 +131,7 @@ deriving instance Show (PParams era) => Show (UtxoEnv era)
 deriving instance Eq (PParams era) => Eq (UtxoEnv era)
 
 instance (Era era, NFData (PParams era)) => NFData (UtxoEnv era)
+instance Inject (UtxoEnv era) (UtxoEnv era)
 
 data UtxoEvent era
   = TotalDeposits (SafeHash (EraCrypto era) EraIndependentTxBody) Coin

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway.hs

@@ -25,6 +25,7 @@ import Cardano.Ledger.Conway (Conway)
 import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParamsUpdate)
 import Cardano.Ledger.Conway.Governance (
   EnactState,
+  GovAction,
   GovActionState (..),
   GovProcedures (..),
   ProposalProcedure,
@@ -37,7 +38,7 @@ import Cardano.Ledger.Conway.Governance (
   toPrevGovActionIds,
  )
 import Cardano.Ledger.Conway.PParams (THKD (..))
-import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure, RatifyState)
+import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure, EnactSignal, RatifyState)
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
 import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
 import Cardano.Ledger.Credential (Credential)
@@ -67,7 +68,7 @@ import Test.Cardano.Ledger.Conformance (
   runConformance,
   runSpecTransM,
  )
-import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (ConwayExecEnactEnv)
 import Test.Cardano.Ledger.Constrained.Conway (
   IsConwayUniv,
   ProposalsSplit,
@@ -219,21 +220,27 @@ agdaCompatiblePPU ppup =
         (branch $ const False)
         (branch $ const True)
 
+agdaCompatibleGovAction ::
+  IsConwayUniv fn =>
+  Term fn (GovAction Conway) ->
+  Pred fn
+agdaCompatibleGovAction govAction =
+  caseOn
+    govAction
+    (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
+    (branch $ \_ _ -> True)
+    (branch $ \_ _ -> True)
+    (branch $ const True)
+    (branch $ \_ _ _ _ -> True)
+    (branch $ \_ _ -> True)
+    (branch $ const True)
+
 agdaCompatibleProposal ::
   IsConwayUniv fn =>
   Term fn (ProposalProcedure Conway) ->
   Pred fn
 agdaCompatibleProposal prop =
-  match prop $ \_ _ govAction _ ->
-    caseOn
-      govAction
-      (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
-      (branch $ \_ _ -> True)
-      (branch $ \_ _ -> True)
-      (branch $ const True)
-      (branch $ \_ _ _ _ -> True)
-      (branch $ \_ _ -> True)
-      (branch $ const True)
+  match prop $ \_ _ govAction _ -> agdaCompatibleGovAction govAction
 
 agdaCompatibleGAS ::
   IsConwayUniv fn =>
@@ -511,3 +518,18 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
     first (\case {})
       . computationResultToEither
       $ Agda.ratifyStep env st sig
+
+instance IsConwayUniv fn => ExecSpecRule fn "ENACT" Conway where
+  type ExecEnvironment fn "ENACT" Conway = ConwayExecEnactEnv Conway
+
+  environmentSpec _ = TrueSpec
+  stateSpec _ _ = TrueSpec
+  signalSpec _ _ _ = onlyMinFeeAUpdates
+    where
+      onlyMinFeeAUpdates :: Specification fn (EnactSignal Conway)
+      onlyMinFeeAUpdates = constrained $ \sig ->
+        match sig $ \_ ga -> agdaCompatibleGovAction ga
+  runAgdaRule env st sig =
+    first (error "ENACT failed")
+      . computationResultToEither
+      $ Agda.enactStep env st sig