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: 0f40403ba3b52a11ac8a44ec3be22ac272c732df
+  --sha256: sha256-8Lcp71PqMP9uBtiUPseyOwvZOSk4blR2+7Y2R6rkJoU=
 
 index-state:
   -- Bump this if you need newer packages from Hackage

eras/conway/impl/cardano-ledger-conway.cabal

@@ -124,6 +124,7 @@ library testlib
         Test.Cardano.Ledger.Conway.Imp.UtxoSpec
         Test.Cardano.Ledger.Conway.Imp.UtxosSpec
         Test.Cardano.Ledger.Conway.Imp.RatifySpec
+        Test.Cardano.Ledger.Conway.Imp.DelegSpec
         Test.Cardano.Ledger.Conway.Proposals
         Test.Cardano.Ledger.Conway.TreeDiff
         Test.Cardano.Ledger.Conway.Genesis

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/Imp.hs

@@ -17,6 +17,7 @@ import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance (ConwayGovState)
 import Cardano.Ledger.Conway.PParams (ConwayPParams)
 import Cardano.Ledger.Conway.Rules (
+  ConwayDelegPredFailure,
   ConwayEpochEvent,
   ConwayGovCertPredFailure,
   ConwayGovPredFailure,
@@ -28,6 +29,7 @@ import Data.Functor.Identity
 import Data.Typeable (Typeable)
 import qualified Test.Cardano.Ledger.Babbage.Imp as BabbageImp
 import Test.Cardano.Ledger.Common
+import qualified Test.Cardano.Ledger.Conway.Imp.DelegSpec as Deleg
 import qualified Test.Cardano.Ledger.Conway.Imp.EnactSpec as Enact
 import qualified Test.Cardano.Ledger.Conway.Imp.EpochSpec as Epoch
 import qualified Test.Cardano.Ledger.Conway.Imp.GovCertSpec as GovCert
@@ -42,21 +44,23 @@ spec ::
   ( ConwayEraImp era
   , GovState era ~ ConwayGovState era
   , PParamsHKD Identity era ~ ConwayPParams Identity era
-  , InjectRuleFailure "LEDGER" ConwayGovPredFailure era
   , Inject (BabbageContextError era) (ContextError era)
   , Inject (ConwayContextError era) (ContextError era)
+  , InjectRuleFailure "LEDGER" ConwayGovPredFailure era
   , InjectRuleFailure "LEDGER" BabbageUtxoPredFailure era
   , InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure era
   , InjectRuleFailure "LEDGER" ShelleyUtxoPredFailure era
   , InjectRuleFailure "LEDGER" ShelleyUtxowPredFailure era
   , InjectRuleFailure "LEDGER" ConwayGovCertPredFailure era
+  , InjectRuleFailure "LEDGER" ConwayDelegPredFailure era
   , NFData (Event (EraRule "ENACT" era))
   , ToExpr (Event (EraRule "ENACT" era))
   , Eq (Event (EraRule "ENACT" era))
   , Typeable (Event (EraRule "ENACT" era))
   , InjectRuleEvent "TICK" ConwayEpochEvent era
   , Event (EraRule "EPOCH" era) ~ ConwayEpochEvent era
   , Event (EraRule "NEWEPOCH" era) ~ ConwayNewEpochEvent era
+  , ToExpr (TxCert era)
   ) =>
   Spec
 spec = do
@@ -79,3 +83,4 @@ spec = do
       Utxo.spec @era
       Utxos.relevantDuringBootstrapSpec @era
       Ratify.relevantDuringBootstrapSpec @era
+      Deleg.spec @era

eras/conway/impl/testlib/Test/Cardano/Ledger/Conway/Imp/DelegSpec.hs

@@ -0,0 +1,56 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+
+module Test.Cardano.Ledger.Conway.Imp.DelegSpec (spec) where
+
+import Cardano.Ledger.Conway.Core (
+  EraTx (..),
+  EraTxBody (..),
+  EraTxCert (..),
+  InjectRuleFailure (..),
+ )
+import Cardano.Ledger.Conway.Rules (ConwayDelegPredFailure (..))
+import Cardano.Ledger.Conway.TxCert (
+  ConwayEraTxCert,
+  Delegatee (DelegStake),
+  pattern RegDepositDelegTxCert,
+ )
+import Cardano.Ledger.Credential (Credential (..))
+import Cardano.Ledger.Val (Val (..))
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Sequence.Strict as SSeq
+import Lens.Micro ((&), (.~))
+import Test.Cardano.Ledger.Conway.ImpTest
+import Test.Cardano.Ledger.Imp.Common
+
+spec ::
+  forall era.
+  ( ShelleyEraImp era
+  , ConwayEraTxCert era
+  , InjectRuleFailure "LEDGER" ConwayDelegPredFailure era
+  , ToExpr (TxCert era)
+  ) =>
+  SpecWith (ImpTestState era)
+spec = describe "DELEG" $ do
+  it "Deposit must be declared if the delegator is not yet registered" $ do
+    delegatorCred <- KeyHashObj <$> freshKeyHash
+    delegatee <- freshKeyHash
+    let
+      cert =
+        RegDepositDelegTxCert
+          delegatorCred
+          (DelegStake delegatee)
+          zero
+    logToExpr cert
+    let
+      tx =
+        mkBasicTx mkBasicTxBody
+          & bodyTxL . certsTxBodyL .~ SSeq.singleton cert
+    submitFailingTx
+      tx
+      (injectFailure (IncorrectDepositDELEG zero) NE.:| [])

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

@@ -1,4 +1,3 @@
-{-# LANGUAGE BangPatterns #-}
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
@@ -7,7 +6,6 @@
 {-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE RankNTypes #-}
-{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
@@ -61,10 +59,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 +329,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.certStep 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

@@ -50,6 +50,7 @@ import Cardano.Ledger.BaseTypes (
   strictMaybeToMaybe,
  )
 import Cardano.Ledger.Binary (Sized (..))
+import Cardano.Ledger.CertState (CommitteeAuthorization (..), CommitteeState (..))
 import Cardano.Ledger.Coin (Coin (..))
 import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance (
@@ -80,6 +81,8 @@ import Cardano.Ledger.Conway.Governance (
  )
 import Cardano.Ledger.Conway.PParams (ConwayPParams (..), THKD (..))
 import Cardano.Ledger.Conway.Rules (
+  CertEnv (..),
+  ConwayCertPredFailure,
   ConwayGovPredFailure,
   ConwayUtxoPredFailure,
   GovEnv (..),
@@ -94,17 +97,24 @@ import Cardano.Ledger.Conway.TxCert (
  )
 import Cardano.Ledger.Credential (Credential (..))
 import Cardano.Ledger.Crypto (Crypto (..))
-import Cardano.Ledger.DRep (DRep (..))
+import Cardano.Ledger.DRep (DRep (..), DRepState (..))
 import Cardano.Ledger.HKD (HKD)
-import Cardano.Ledger.Keys (KeyHash (..), VKey (..))
+import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..), VKey (..))
 import Cardano.Ledger.Keys.WitVKey (WitVKey (..))
 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 (..),
+  DState (..),
+  PState (..),
+  UTxOState (..),
+  VState (..),
+ )
 import Cardano.Ledger.Shelley.Rules (Identity, UtxoEnv (..))
 import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
+import Cardano.Ledger.UMap (dRepMap, rewardMap, sPoolMap)
 import Cardano.Ledger.UTxO (UTxO (..))
 import Cardano.Ledger.Val (Val (..))
 import Control.DeepSeq (NFData)
@@ -116,7 +126,7 @@ import Data.Data (Typeable)
 import Data.Default.Class (Default (..))
 import Data.Foldable (Foldable (..))
 import qualified Data.List as L
-import Data.Map.Strict (Map)
+import Data.Map.Strict (Map, mapKeys)
 import qualified Data.Map.Strict as Map
 import Data.OMap.Strict (OMap, assocList)
 import Data.OSet.Strict (OSet)
@@ -136,7 +146,7 @@ import Test.Cardano.Ledger.Conformance (
   SpecTranslationError,
   askTransCtx,
  )
-import Test.Cardano.Ledger.Conway.TreeDiff (Expr (..), ToExpr (..))
+import Test.Cardano.Ledger.Conway.TreeDiff (Expr (..), ToExpr (..), showExpr)
 
 -- | OpaqueErrorString behaves like unit in comparisons, but contains an
 -- error string that can be displayed.
@@ -326,6 +336,7 @@ instance SpecTranslate ctx (ConwayPParams Identity era) where
       <*> pure (toInteger . unTHKD $ cppMaxValSize x)
       <*> pure 0 -- minUTxOValue has been deprecated and is not supported in Conway
       <*> toSpecRep (cppPoolDeposit x)
+      <*> toSpecRep (cppKeyDeposit x)
       <*> toSpecRep (cppEMax x)
       <*> toSpecRep (toInteger . unTHKD $ cppNOpt x)
       <*> toSpecRep (cppProtocolVersion x)
@@ -959,3 +970,74 @@ instance Crypto c => SpecTranslate ctx (MaryValue c) where
   type SpecRep (MaryValue c) = Agda.Coin
 
   toSpecRep = toSpecRep . coin
+
+instance
+  ( ToExpr (PredicateFailure (EraRule "DELEG" era))
+  , ToExpr (PredicateFailure (EraRule "GOVCERT" era))
+  , ToExpr (PredicateFailure (EraRule "POOL" era))
+  ) =>
+  SpecTranslate ctx (ConwayCertPredFailure era)
+  where
+  type SpecRep (ConwayCertPredFailure era) = OpaqueErrorString
+
+  toSpecRep = pure . OpaqueErrorString . showExpr
+
+instance
+  ( SpecTranslate ctx (PParamsHKD Identity era)
+  , Eq (SpecRep (PParamsHKD Identity era))
+  , ToExpr (SpecRep (PParamsHKD Identity era))
+  , NFData (SpecRep (PParamsHKD Identity era))
+  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
+  ) =>
+  SpecTranslate ctx (CertEnv era)
+  where
+  type SpecRep (CertEnv era) = Agda.CertEnv
+  type SpecTransContext (CertEnv era) = ()
+
+  toSpecRep CertEnv {..} =
+    Agda.MkCertEnv
+      <$> toSpecRep ceCurrentEpoch
+      <*> toSpecRep cePParams
+      <*> pure def -- Unused?
+      <*> pure def -- Unused?
+
+instance SpecTranslate ctx (DState era) where
+  type SpecRep (DState era) = Agda.DState
+
+  toSpecRep DState {..} =
+    Agda.MkDState
+      <$> toSpecRep (dRepMap dsUnified)
+      <*> toSpecRep (KeyHashObj <$> sPoolMap dsUnified)
+      <*> toSpecRep (rewardMap dsUnified)
+
+instance SpecTranslate ctx (PState era) where
+  type SpecRep (PState era) = Agda.PState
+
+  toSpecRep PState {..} =
+    Agda.MkPState
+      <$> toSpecRep (mapKeys KeyHashObj psStakePoolParams)
+      <*> toSpecRep (mapKeys KeyHashObj psRetiring)
+
+committeeCredentialToStrictMaybe ::
+  CommitteeAuthorization c ->
+  StrictMaybe (Credential 'HotCommitteeRole c)
+committeeCredentialToStrictMaybe (CommitteeHotCredential c) = SJust c
+committeeCredentialToStrictMaybe (CommitteeMemberResigned _) = SNothing
+
+instance SpecTranslate ctx (VState era) where
+  type SpecRep (VState era) = Agda.GState
+
+  toSpecRep VState {..} =
+    Agda.MkGState
+      <$> toSpecRep (drepExpiry <$> vsDReps)
+      <*> toSpecRep
+        (committeeCredentialToStrictMaybe <$> csCommitteeCreds vsCommitteeState)
+
+instance SpecTranslate ctx (CertState era) where
+  type SpecRep (CertState era) = Agda.CertState
+
+  toSpecRep CertState {..} =
+    Agda.MkCertState
+      <$> toSpecRep certDState
+      <*> toSpecRep certPState
+      <*> toSpecRep certVState