Plumb the test for execution

Make the test type-check and execute, but without
any adjustment to the generators.

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

@@ -75,13 +75,17 @@ import Test.Cardano.Ledger.Conformance (
  )
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (ConwayExecEnactEnv)
 import Test.Cardano.Ledger.Constrained.Conway (
+  EpochExecEnv,
   IsConwayUniv,
   ProposalsSplit,
   certEnvSpec,
   certStateSpec,
   dStateSpec,
   delegCertSpec,
   delegEnvSpec,
+  epochEnvSpec,
+  epochSignalSpec,
+  epochStateSpec,
   genProposalsSplit,
   govCertEnvSpec,
   govCertSpec,
@@ -465,16 +469,23 @@ instance IsConwayUniv fn => ExecSpecRule fn "POOL" Conway where
       . computationResultToEither
       $ Agda.poolStep env st sig
 
-instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" Conway where
-  environmentSpec _ = delegEnvSpec
+instance Inject (EpochExecEnv era) () where
+  inject _ = ()
 
-  stateSpec _ _ = dStateSpec
+instance
+  IsConwayUniv fn =>
+  ExecSpecRule fn "EPOCH" Conway
+  where
+  type ExecContext fn "EPOCH" Conway = [GovActionState Conway]
+  type ExecEnvironment fn "EPOCH" Conway = EpochExecEnv Conway
 
-  signalSpec _ env st =
-    delegCertSpec env st
-      <> constrained disableRegCertsDelegCert
+  environmentSpec _ = epochEnvSpec
+
+  stateSpec _ _ = epochStateSpec
+
+  signalSpec _ _ _ = epochSignalSpec
 
   runAgdaRule env st sig =
-    first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
+    first (error "ENACT failed")
       . computationResultToEither
-      $ Agda.delegStep env st sig
+      $ Agda.epochStep env st sig

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

@@ -59,6 +59,14 @@ deriving instance Generic PoolThresholds
 
 deriving instance Generic DrepThresholds
 
+deriving instance Generic NewEpochEnv
+
+deriving instance Generic EpochState
+
+deriving instance Generic LedgerState
+
+deriving instance Generic Acnt
+
 deriving instance Ord Tag
 
 deriving instance Ord Credential
@@ -131,6 +139,12 @@ deriving instance Eq CertState
 
 deriving instance Eq RatifyState
 
+deriving instance Eq EpochState
+
+deriving instance Eq Acnt
+
+deriving instance Eq LedgerState
+
 instance (NFData k, NFData v) => NFData (HSMap k v)
 
 instance NFData a => NFData (HSSet a)
@@ -203,6 +217,14 @@ instance NFData EnactEnv
 
 instance NFData DelegEnv
 
+instance NFData NewEpochEnv
+
+instance NFData EpochState
+
+instance NFData Acnt
+
+instance NFData LedgerState
+
 instance ToExpr a => ToExpr (HSSet a)
 
 instance ToExpr Credential where
@@ -278,6 +300,14 @@ instance ToExpr EnactEnv
 
 instance ToExpr DelegEnv
 
+instance ToExpr NewEpochEnv
+
+instance ToExpr EpochState
+
+instance ToExpr LedgerState
+
+instance ToExpr Acnt
+
 instance Default (HSMap k v)
 
 instance FixupSpecRep OpaqueErrorString
@@ -353,3 +383,9 @@ instance FixupSpecRep EnactState
 instance FixupSpecRep RatifyEnv
 
 instance FixupSpecRep RatifyState
+
+instance FixupSpecRep EpochState
+
+instance FixupSpecRep Acnt
+
+instance FixupSpecRep LedgerState

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

@@ -34,54 +34,13 @@ import Cardano.Ledger.Alonzo.Scripts (AlonzoPlutusPurpose (..))
 import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..))
 import Cardano.Ledger.Alonzo.TxWits (AlonzoTxWits (..), Redeemers (..), TxDats (..))
 import Cardano.Ledger.Babbage.TxOut (BabbageTxOut (..))
-import Cardano.Ledger.BaseTypes (
-  Anchor,
-  BoundedRational (..),
-  EpochInterval (..),
-  EpochNo (..),
-  Inject (..),
-  Network,
-  ProtVer (..),
-  SlotNo (..),
-  StrictMaybe (..),
-  TxIx (..),
-  UnitInterval,
-  getVersion,
-  strictMaybeToMaybe,
- )
+import Cardano.Ledger.BaseTypes
 import Cardano.Ledger.Binary (Sized (..))
 import Cardano.Ledger.CertState (CommitteeAuthorization (..), CommitteeState (..))
 import Cardano.Ledger.Coin (Coin (..), CompactForm)
 import Cardano.Ledger.Compactible (Compactible)
 import Cardano.Ledger.Conway.Core
-import Cardano.Ledger.Conway.Governance (
-  Committee (Committee),
-  Constitution (..),
-  EnactState (..),
-  GovAction (..),
-  GovActionId (GovActionId),
-  GovActionIx (..),
-  GovActionState (..),
-  GovProcedures (..),
-  GovPurposeId (..),
-  GovRelation (..),
-  ProposalProcedure (..),
-  Proposals,
-  RatifyEnv (..),
-  RatifySignal (..),
-  Vote (..),
-  Voter (..),
-  VotingProcedure (..),
-  VotingProcedures (..),
-  ensPrevGovActionIdsL,
-  ensProtVerL,
-  foldrVotingProcedures,
-  gasAction,
-  gasReturnAddr,
-  pPropsL,
-  pRootsL,
-  toPrevGovActionIds,
- )
+import Cardano.Ledger.Conway.Governance
 import Cardano.Ledger.Conway.PParams (ConwayPParams (..), THKD (..))
 import Cardano.Ledger.Conway.Rules (
   CertEnv (..),
@@ -94,7 +53,6 @@ import Cardano.Ledger.Conway.Rules (
   ConwayUtxoPredFailure,
   EnactSignal (..),
   GovEnv (..),
-  RatifyState (..),
  )
 import Cardano.Ledger.Conway.Scripts (AlonzoScript, ConwayPlutusPurpose (..))
 import Cardano.Ledger.Conway.TxCert (
@@ -114,13 +72,7 @@ import Cardano.Ledger.Plutus (CostModels, ExUnits (..), Prices)
 import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
 import Cardano.Ledger.PoolParams (PoolParams (..))
 import Cardano.Ledger.SafeHash (SafeHash, extractHash)
-import Cardano.Ledger.Shelley.LedgerState (
-  CertState (..),
-  DState (..),
-  PState (..),
-  UTxOState (..),
-  VState (..),
- )
+import Cardano.Ledger.Shelley.LedgerState
 import Cardano.Ledger.Shelley.Rules (Identity, PoolEnv (..), ShelleyPoolPredFailure, UtxoEnv (..))
 import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
 import Cardano.Ledger.UMap (dRepMap, fromCompact, rewardMap, sPoolMap)
@@ -159,6 +111,7 @@ import Test.Cardano.Ledger.Conformance (
   askCtx,
  )
 import Test.Cardano.Ledger.Constrained.Conway (IsConwayUniv)
+import Test.Cardano.Ledger.Constrained.Conway.Epoch
 import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..), showExpr)
 
 instance SpecTranslate ctx Void where
@@ -1227,6 +1180,29 @@ instance
 
   toSpecRep (EnactSignal _ ga) = toSpecRep ga
 
+-- data EpochExecEnv era = EpochExecEnv
+--   { eeeStakeDistr :: !(Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin))
+--   } deriving (Generic, Eq, Show)
+
+instance ToExpr (EpochExecEnv era)
+instance Era era => NFData (EpochExecEnv era)
+
+instance HasSimpleRep (EpochExecEnv era)
+instance (IsConwayUniv fn, Era era) => HasSpec fn (EpochExecEnv era)
+
+instance SpecTranslate ctx (EpochExecEnv era) where
+  type SpecRep (EpochExecEnv era) = Agda.NewEpochEnv
+
+  toSpecRep (EpochExecEnv stakeDistr) = do
+    let
+      transStakeDistr (c, s) = do
+        c' <- toSpecRep c
+        s' <- toSpecRep s
+        pure (Agda.CredVoter Agda.SPO c', s')
+      stakeDistrsMap = traverse transStakeDistr $ Map.toList stakeDistr
+      stakeDistrs = Agda.MkStakeDistrs . Agda.MkHSMap <$> stakeDistrsMap
+    Agda.MkNewEpochEnv <$> stakeDistrs
+
 data ConwayExecEnactEnv era = ConwayExecEnactEnv
   { ceeeGid :: GovActionId (EraCrypto era)
   , ceeeTreasury :: Coin
@@ -1303,3 +1279,55 @@ instance SpecTranslate ctx (ShelleyPoolPredFailure era) where
   type SpecRep (ShelleyPoolPredFailure era) = OpaqueErrorString
 
   toSpecRep e = pure . OpaqueErrorString . show $ toExpr e
+
+instance
+  ( EraPParams era
+  , ConwayEraGov era
+  , SpecTranslate ctx (PParamsHKD Identity era)
+  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
+  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
+  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
+  , Inject ctx [GovActionState era]
+  , ToExpr (PParamsHKD StrictMaybe era)
+  , SpecRep (TxOut era) ~ Agda.TxOut
+  , SpecTranslate ctx (TxOut era)
+  ) =>
+  SpecTranslate ctx (EpochState era)
+  where
+  type SpecRep (EpochState era) = Agda.EpochState
+
+  toSpecRep (EpochState {esLState = esLState@LedgerState {..}, ..}) =
+    Agda.MkEpochState
+      <$> toSpecRep esAccountState
+      <*> toSpecRep esLState
+      <*> toSpecRep enactState
+      <*> toSpecRep ratifyState
+    where
+      enactState = mkEnactState $ utxosGovState lsUTxOState
+      ratifyState = RatifyState enactState mempty mempty False
+
+instance SpecTranslate ctx AccountState where
+  type SpecRep AccountState = Agda.Acnt
+
+  toSpecRep (AccountState {..}) =
+    Agda.MkAcnt
+      <$> toSpecRep asTreasury
+      <*> toSpecRep asReserves
+
+instance
+  ( ConwayEraGov era
+  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
+  , SpecTranslate ctx (PParamsHKD StrictMaybe era)
+  , SpecRep (PParamsHKD StrictMaybe era) ~ Agda.PParamsUpdate
+  , SpecRep (TxOut era) ~ Agda.TxOut
+  , SpecTranslate ctx (TxOut era)
+  ) =>
+  SpecTranslate ctx (LedgerState era)
+  where
+  type SpecRep (LedgerState era) = Agda.LedgerState
+
+  toSpecRep (LedgerState {..}) =
+    Agda.MkLedgerState
+      <$> toSpecRep lsUTxOState
+      <*> toSpecRep (utxosGovState lsUTxOState ^. proposalsGovStateL)
+      <*> toSpecRep lsCertState

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway.hs

@@ -4,6 +4,7 @@ module Test.Cardano.Ledger.Constrained.Conway (
 
 import Test.Cardano.Ledger.Constrained.Conway.Cert as X
 import Test.Cardano.Ledger.Constrained.Conway.Deleg as X
+import Test.Cardano.Ledger.Constrained.Conway.Epoch as X
 import Test.Cardano.Ledger.Constrained.Conway.Gov as X
 import Test.Cardano.Ledger.Constrained.Conway.GovCert as X
 import Test.Cardano.Ledger.Constrained.Conway.Instances as X

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Epoch.hs

@@ -1,3 +1,5 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE RankNTypes #-}
 {-# LANGUAGE ScopedTypeVariables #-}
@@ -6,32 +8,26 @@
 -- for the EPOCH rule
 module Test.Cardano.Ledger.Constrained.Conway.Epoch where
 
-import Cardano.Ledger.Conway.TxCert
+import Cardano.Ledger.BaseTypes
+import Cardano.Ledger.Coin
+import Cardano.Ledger.Conway (Conway, ConwayEra)
+import Cardano.Ledger.Core
+import Cardano.Ledger.Crypto (StandardCrypto)
 import Cardano.Ledger.Shelley.API.Types
-import Cardano.Ledger.UMap (RDPair (..), fromCompact, unUnify)
-import qualified Data.Map as Map
-import Lens.Micro
-
 import Constrained
+import Data.Map.Strict
+import GHC.Generics (Generic)
 
-import Cardano.Ledger.Conway (Conway, ConwayEra)
-import Cardano.Ledger.Conway.Rules (ConwayDelegEnv (..))
-import Cardano.Ledger.Core (ppKeyDepositL)
-import Cardano.Ledger.Crypto (StandardCrypto)
-import Test.Cardano.Ledger.Constrained.Conway.Instances
-import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
+data EpochExecEnv era = EpochExecEnv
+  { eeeStakeDistr :: !(Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin))
+  }
+  deriving (Generic, Eq, Show)
 
-epochEnvSpec :: 
-  IsConwayUniv fn =>
-  Specification fn ()
-epochEnvSpec = undefined
+epochEnvSpec :: Specification fn (EpochExecEnv Conway)
+epochEnvSpec = TrueSpec
 
-epochStateSpec ::
-  IsConwayUniv fn =>
-  Specification fn (EpochState (ConwayEra StandardCrypto))
-epochStateSpec = undefined
+epochStateSpec :: Specification fn (EpochState (ConwayEra StandardCrypto))
+epochStateSpec = TrueSpec
 
-epochSignalSpec ::
-  IsConwayUniv fn =>
-  Specification fn (EpochState (ConwayEra StandardCrypto))
-epochSignalSpec = undefined
+epochSignalSpec :: Specification fn EpochNo
+epochSignalSpec = TrueSpec