WIP

cabal.project

@@ -13,8 +13,8 @@ repository cardano-haskell-packages
 source-repository-package
   type: git
   location: https://github.com/input-output-hk/cardano-ledger-executable-spec.git
-  tag: ac7af152d7d4c7b3ef1f3513e637c2c1e86ca30e
-  --sha256: sha256-hOdJTXA+vxm2Gh7t0hKXtSJ+3/iCoNyrzEiMzWGs6s4=
+  tag: d30dfe74f6ca8898e3eebcc8200148d6f4ea0c70
+  --sha256: sha256-0c+8+EyUYJ4Ksvg/AnQy1hCdYAQJdTIkbL7e4EDIAbE=
 
 index-state:
   -- Bump this if you need newer packages from Hackage

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

@@ -76,6 +76,8 @@ data CertEnv era = CertEnv
 deriving instance Eq (PParams era) => Eq (CertEnv era)
 deriving instance Show (PParams era) => Show (CertEnv era)
 
+instance NFData (PParams era) => NFData (CertEnv era)
+
 data ConwayCertPredFailure era
   = DelegFailure (PredicateFailure (EraRule "DELEG" era))
   | PoolFailure (PredicateFailure (EraRule "POOL" era))

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

@@ -249,3 +249,5 @@ instance
   , ToExpr (TxCert era)
   ) =>
   ToExpr (ConwayUtxowPredFailure era)
+
+instance ToExpr (PParamsHKD Identity era) => ToExpr (CertEnv era)

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

@@ -41,7 +41,6 @@ import Data.Bifunctor (Bifunctor (..))
 import Data.Default.Class (Default (..))
 import Data.Foldable (Foldable (..))
 import qualified Data.List.NonEmpty as NE
-import qualified Data.OSet.Strict as OSet
 import qualified Data.Text as T
 import Data.Typeable (Typeable)
 import GHC.Generics (Generic)
@@ -61,10 +60,13 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (
 import Test.Cardano.Ledger.Constrained.Conway (
   IsConwayUniv,
   ProposalsSplit,
+  certEnvSpec,
+  certStateSpec,
   genProposalsSplit,
   govEnvSpec,
   govProceduresSpec,
   govProposalsSpec,
+  txCertSpec,
   utxoEnvSpec,
   utxoStateSpec,
   utxoTxSpec,
@@ -328,3 +330,16 @@ instance
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
       . computationResultToEither
       $ Agda.utxoStep env st sig
+
+instance
+  IsConwayUniv fn =>
+  ExecSpecRule fn "CERT" Conway
+  where
+  environmentSpec _ = certEnvSpec
+  stateSpec _ _ = certStateSpec
+  signalSpec _ = txCertSpec
+
+  runAgdaRule env st sig =
+    first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
+      . computationResultToEither
+      $ Agda.certsStep env st sig

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

@@ -26,6 +26,16 @@ deriving instance Generic GovEnv
 
 deriving instance Generic EnactState
 
+deriving instance Generic CertEnv
+
+deriving instance Generic PState
+
+deriving instance Generic DState
+
+deriving instance Generic GState
+
+deriving instance Generic CertState
+
 deriving instance Eq AgdaEmpty
 
 deriving instance Eq TxBody
@@ -62,6 +72,16 @@ deriving instance Eq EnactState
 
 deriving instance Eq UTxOEnv
 
+deriving instance Eq CertEnv
+
+deriving instance Eq DState
+
+deriving instance Eq PState
+
+deriving instance Eq GState
+
+deriving instance Eq CertState
+
 instance NFData GovAction
 
 instance NFData TxId
@@ -104,6 +124,16 @@ instance NFData Tx
 
 instance NFData UTxOEnv
 
+instance NFData CertEnv
+
+instance NFData PState
+
+instance NFData DState
+
+instance NFData GState
+
+instance NFData CertState
+
 instance ToExpr Credential where
   toExpr (KeyHashObj h) = App "KeyHashObj" [agdaHashToExpr h]
   toExpr (ScriptObj h) = App "ScriptObj" [agdaHashToExpr h]
@@ -148,3 +178,13 @@ instance ToExpr Tx
 instance ToExpr UTxOState
 
 instance ToExpr UTxOEnv
+
+instance ToExpr CertEnv
+
+instance ToExpr DState
+
+instance ToExpr PState
+
+instance ToExpr GState
+
+instance ToExpr CertState

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

@@ -16,6 +16,7 @@ spec :: Spec
 spec = describe "Conway conformance tests" $ do
   xprop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway
   prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway
+  prop "CERT" $ conformsToImpl @"CERT" @ConwayFn @Conway
   describe "Generators" $ do
     let
       genEnv = do

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

@@ -102,7 +102,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 (UTxOState (..))
+import Cardano.Ledger.Shelley.LedgerState (CertState, UTxOState (..))
 import Cardano.Ledger.Shelley.Rules (Identity, UtxoEnv (..))
 import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
 import Cardano.Ledger.UTxO (UTxO (..))
@@ -959,3 +959,18 @@ instance Crypto c => SpecTranslate ctx (MaryValue c) where
   type SpecRep (MaryValue c) = Agda.Coin
 
   toSpecRep = toSpecRep . coin
+
+instance SpecTranslate ctx (ConwayCertPredFailure era) where
+  type SpecRep (ConwayCertPredFailure era) = OpaqueErrorString
+
+  toSpecRep = undefined
+
+instance SpecTranslate ctx (CertEnv era) where
+  type SpecRep (CertEnv era) = Agda.CertEnv
+
+  toSpecRep = undefined
+
+instance SpecTranslate ctx (CertState era) where
+  type SpecRep (CertState era) = Agda.CertState
+
+  toSpecRep = undefined