Merge pull request #4348 from IntersectMBO/aniketd/conformance-govcert

Conformance: GOVCERT

cabal.project

@@ -17,8 +17,8 @@ repository cardano-haskell-packages
 source-repository-package
   type: git
   location: https://github.com/input-output-hk/cardano-ledger-executable-spec.git
-  tag: d6effa703ed06ffc6239a963fdbccccd25dfa663
-  --sha256: sha256-b+HRjMrriceFM/fUn9Qn+LJjMh3I3/F9PtYxrmGOiug=
+  tag: c8651e5332b2d99e1f0ae0e1287c10bc187e91a8
+  --sha256: sha256-AOmMVq7GWixd9KnIRgo9p6oaSalSVHoITHRtlJUTJgg=
 
 index-state:
   -- Bump this if you need newer packages from Hackage

eras/conway/impl/CHANGELOG.md

@@ -2,6 +2,9 @@
 
 ## 1.14.1.0
 
+* Add instances for `ConwayGovCertEnv`. #4348
+  * `NFData`
+  * `ToExpr`
 * Add `NFData` instance for `RatifySignal`
 * Add `AllegraEraScript` and `ShelleyEraScript` instances for `ConwayEra`
 

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

@@ -67,6 +67,8 @@ data ConwayGovCertEnv era = ConwayGovCertEnv
   }
   deriving (Generic)
 
+instance (NFData (PParams era), Era era) => NFData (ConwayGovCertEnv era)
+
 deriving instance Show (PParams era) => Show (ConwayGovCertEnv era)
 
 deriving instance Eq (PParams era) => Eq (ConwayGovCertEnv era)

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

@@ -234,6 +234,8 @@ instance
 
 instance ToExpr (PParams era) => ToExpr (GovEnv era)
 
+instance ToExpr (PParams era) => ToExpr (ConwayGovCertEnv era)
+
 instance
   ( ToExpr (Value era)
   , ToExpr (TxOut era)

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

@@ -39,7 +39,7 @@ import Cardano.Ledger.Conway.Governance (
 import Cardano.Ledger.Conway.PParams (THKD (..))
 import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure, RatifyState)
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
-import Cardano.Ledger.Conway.TxCert (ConwayTxCert)
+import Cardano.Ledger.Conway.TxCert (ConwayGovCert, ConwayTxCert)
 import Cardano.Ledger.Credential (Credential)
 import Cardano.Ledger.Crypto (StandardCrypto)
 import Cardano.Ledger.Keys (KeyRole (..))
@@ -74,13 +74,16 @@ import Test.Cardano.Ledger.Constrained.Conway (
   certEnvSpec,
   certStateSpec,
   genProposalsSplit,
+  govCertEnvSpec,
+  govCertSpec,
   govEnvSpec,
   govProceduresSpec,
   govProposalsSpec,
   txCertSpec,
   utxoEnvSpec,
   utxoStateSpec,
   utxoTxSpec,
+  vStateSpec,
  )
 import Test.Cardano.Ledger.Constrained.Conway.Instances ()
 import Test.Cardano.Ledger.Conway.ImpTest (impAnn, logEntry)
@@ -201,10 +204,9 @@ agdaCompatiblePPU ppup =
       Term fn (THKD gs StrictMaybe a) ->
       Pred fn
     isUnmodified x =
-      caseOn
-        x
-        (branch $ const True)
-        (branch $ const False)
+      (caseOn x)
+        (branch $ \_ -> True)
+        (branch $ \_ -> False)
     isModified ::
       ( HasSpec fn a
       , Typeable gs
@@ -214,26 +216,24 @@ agdaCompatiblePPU ppup =
       Term fn (THKD gs StrictMaybe a) ->
       Pred fn
     isModified x =
-      caseOn
-        x
-        (branch $ const False)
-        (branch $ const True)
+      (caseOn x)
+        (branch $ \_ -> False)
+        (branch $ \_ -> True)
 
 agdaCompatibleProposal ::
   IsConwayUniv fn =>
   Term fn (ProposalProcedure Conway) ->
   Pred fn
 agdaCompatibleProposal prop =
   match prop $ \_ _ govAction _ ->
-    caseOn
-      govAction
+    (caseOn govAction)
       (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
       (branch $ \_ _ -> True)
       (branch $ \_ _ -> True)
-      (branch $ const True)
+      (branch $ \_ -> True)
       (branch $ \_ _ _ _ -> True)
       (branch $ \_ _ -> True)
-      (branch $ const True)
+      (branch $ \_ -> True)
 
 agdaCompatibleGAS ::
   IsConwayUniv fn =>
@@ -344,11 +344,10 @@ instance
                 \outs -> forAll' outs $
                   \txOut _ -> match txOut $
                     \_ _ dat _ ->
-                      caseOn
-                        dat
-                        (branch $ const True)
-                        (branch $ const True)
-                        (branch $ const False)
+                      (caseOn dat)
+                        (branch $ \_ -> True)
+                        (branch $ \_ -> True)
+                        (branch $ \_ -> False)
 
   runAgdaRule env st sig =
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
@@ -391,7 +390,7 @@ instance
   signalSpec _ env st =
     txCertSpec env st
       <> constrained disableRegCerts
-      <> constrained disableDRepRegCerts
+      <> constrained disableDRepRegCerts'
     where
       disableRegCerts :: Term fn (ConwayTxCert Conway) -> Pred fn
       disableRegCerts cert =
@@ -405,24 +404,12 @@ instance
           )
           (branch $ \_ -> True)
           (branch $ \_ -> True)
-      -- ConwayRegDRep certificates seem to trigger some kind of a bug in the
-      -- MAlonzo code where it somehow reaches an uncovered case.
-      --
-      -- TODO investigate what's causing this bug and try to get rid of this
-      -- constraint
-      disableDRepRegCerts :: Term fn (ConwayTxCert Conway) -> Pred fn
-      disableDRepRegCerts cert =
+      disableDRepRegCerts' :: Term fn (ConwayTxCert Conway) -> Pred fn
+      disableDRepRegCerts' cert =
         (caseOn cert)
           (branch $ \_ -> True)
           (branch $ \_ -> True)
-          ( branch $ \govCert ->
-              (caseOn govCert)
-                (branch $ \_ _ _ -> False)
-                (branch $ \_ _ -> True)
-                (branch $ \_ _ -> False)
-                (branch $ \_ _ -> True)
-                (branch $ \_ _ -> True)
-          )
+          (branch disableDRepRegCerts)
 
   runAgdaRule env st sig =
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
@@ -511,3 +498,34 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
     first (\case {})
       . computationResultToEither
       $ Agda.ratifyStep env st sig
+
+-- ConwayRegDRep certificates seem to trigger some kind of a bug in the
+-- MAlonzo code where it somehow reaches an uncovered case.
+--
+-- TODO investigate what's causing this bug and try to get rid of this
+-- constraint
+disableDRepRegCerts ::
+  IsConwayUniv fn => Term fn (ConwayGovCert StandardCrypto) -> Pred fn
+disableDRepRegCerts govCert =
+  (caseOn govCert)
+    (branch $ \_ _ _ -> False)
+    (branch $ \_ _ -> True)
+    (branch $ \_ _ -> False)
+    (branch $ \_ _ -> True)
+    (branch $ \_ _ -> True)
+
+instance IsConwayUniv fn => ExecSpecRule fn "GOVCERT" Conway where
+  type ExecContext fn "GOVCERT" Conway = ConwayCertExecContext Conway
+
+  environmentSpec _ctx = govCertEnvSpec
+
+  stateSpec _ctx _env = vStateSpec
+
+  signalSpec _ctx env st =
+    govCertSpec env st
+      <> constrained disableDRepRegCerts
+
+  runAgdaRule env st sig =
+    first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
+      . computationResultToEither
+      $ Agda.govCertStep env st sig

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

@@ -18,6 +18,7 @@ spec = describe "Conway conformance tests" $ do
   prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway
   prop "CERT" $ conformsToImpl @"CERT" @ConwayFn @Conway
   xprop "RATIFY" $ conformsToImpl @"RATIFY" @ConwayFn @Conway
+  prop "GOVCERT" $ conformsToImpl @"GOVCERT" @ConwayFn @Conway
   describe "Generators" $ do
     let
       genEnv = do

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

@@ -84,6 +84,8 @@ import Cardano.Ledger.Conway.PParams (ConwayPParams (..), THKD (..))
 import Cardano.Ledger.Conway.Rules (
   CertEnv (..),
   ConwayCertPredFailure,
+  ConwayGovCertEnv (..),
+  ConwayGovCertPredFailure,
   ConwayGovPredFailure,
   ConwayUtxoPredFailure,
   GovEnv (..),
@@ -572,24 +574,29 @@ instance SpecTranslate ctx (ConwayTxCert era) where
     Agda.RetirePool
       <$> toSpecRep (KeyHashObj kh)
       <*> toSpecRep e
-  toSpecRep (ConwayTxCertGov (ConwayRegDRep c d _)) =
+  toSpecRep (ConwayTxCertGov c) = toSpecRep c
+
+instance SpecTranslate ctx (ConwayGovCert era) where
+  type SpecRep (ConwayGovCert era) = Agda.TxCert
+
+  toSpecRep (ConwayRegDRep c d _) =
     Agda.RegDRep
       <$> toSpecRep c
       <*> toSpecRep d
       <*> pure ()
-  toSpecRep (ConwayTxCertGov (ConwayUnRegDRep c _)) =
+  toSpecRep (ConwayUnRegDRep c _) =
     Agda.DeRegDRep
       <$> toSpecRep c
-  toSpecRep (ConwayTxCertGov (ConwayUpdateDRep c _)) =
+  toSpecRep (ConwayUpdateDRep c _) =
     Agda.RegDRep
       <$> toSpecRep c
       <*> pure 0
       <*> pure ()
-  toSpecRep (ConwayTxCertGov (ConwayAuthCommitteeHotKey c h)) =
+  toSpecRep (ConwayAuthCommitteeHotKey c h) =
     Agda.CCRegHot
       <$> toSpecRep c
       <*> toSpecRep (SJust h)
-  toSpecRep (ConwayTxCertGov (ConwayResignCommitteeColdKey c _)) =
+  toSpecRep (ConwayResignCommitteeColdKey c _) =
     Agda.CCRegHot
       <$> toSpecRep c
       <*> toSpecRep (SNothing @(Credential _ _))
@@ -947,6 +954,11 @@ instance
 
   toSpecRep = pure . OpaqueErrorString . showExpr
 
+instance SpecTranslate ctx (ConwayGovCertPredFailure era) where
+  type SpecRep (ConwayGovCertPredFailure era) = OpaqueErrorString
+
+  toSpecRep = pure . OpaqueErrorString . showExpr
+
 instance
   ( SpecTranslate ctx (PParamsHKD Identity era)
   , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
@@ -966,6 +978,25 @@ instance
       <*> toSpecRep votes
       <*> toSpecRep withdrawals
 
+instance
+  ( SpecTranslate ctx (PParamsHKD Identity era)
+  , SpecRep (PParamsHKD Identity era) ~ Agda.PParams
+  , Inject ctx (VotingProcedures era)
+  , Inject ctx (Map (Network, Credential 'Staking (EraCrypto era)) Coin)
+  ) =>
+  SpecTranslate ctx (ConwayGovCertEnv era)
+  where
+  type SpecRep (ConwayGovCertEnv era) = Agda.CertEnv
+
+  toSpecRep ConwayGovCertEnv {..} = do
+    votes <- askCtx @(VotingProcedures era)
+    withdrawals <- askCtx @(Map (Network, Credential 'Staking (EraCrypto era)) Coin)
+    Agda.MkCertEnv
+      <$> toSpecRep cgceCurrentEpoch
+      <*> toSpecRep cgcePParams
+      <*> toSpecRep votes
+      <*> toSpecRep withdrawals
+
 instance SpecTranslate ctx (DState era) where
   type SpecRep (DState era) = Agda.DState