Bumped spec, enabled GOV Imp conformance

IntersectMBO · Feb 12, 2025 · 8c14e96 · 8c14e96
1 parent e5924af
commit 8c14e96
Show file tree

Hide file tree

Showing 4 changed files with 17 additions and 32 deletions.
diff --git a/cabal.project b/cabal.project
@@ -24,8 +24,8 @@ source-repository-package
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
   subdir: generated
-  --sha256: sha256-MSQpX5wkb/LfgGw5sHl5g0DeHVAZF7oNxlM1sUOEB3Q=
-  tag: 9ea3e2123e89538fa89ce633db0652650f7291dc
+  --sha256: sha256-vrxKI3I1kwt+XiHk+UAWm49veRPTWkVPOvwNzVxuFs8=
+  tag: 9b706ae8c332d5ad10def54aa51d4a66836df363
 
 -- NOTE: If you would like to update the above, look for the `MAlonzo-code`
 -- branch in the `formal-ledger-specifications` repo and copy the SHA of

diff --git a/...cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Gov.hs b/...cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Gov.hs
@@ -1,65 +1,42 @@
 {-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
-{-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov () where
 
-import Cardano.Ledger.BaseTypes
 import Cardano.Ledger.Conway (ConwayEra)
-import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance
 import Cardano.Ledger.Conway.Rules
-import Cardano.Ledger.TxIn (TxId)
-import Lens.Micro
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ()
 import Test.Cardano.Ledger.Constrained.Conway
 import Test.Cardano.Ledger.Conway.Arbitrary ()
 import Test.Cardano.Ledger.Imp.Common
 
-instance
-  Inject
-    (TxId, Proposals ConwayEra, EnactState ConwayEra)
-    (EnactState ConwayEra)
-  where
-  inject (_, _, x) = x
-
 instance
   ( NFData (SpecRep (ConwayGovPredFailure ConwayEra))
   , IsConwayUniv fn
   ) =>
   ExecSpecRule fn "GOV" ConwayEra
   where
-  type
-    ExecContext fn "GOV" ConwayEra =
-      (TxId, ProposalsSplit, EnactState ConwayEra)
+  type ExecContext fn "GOV" ConwayEra = EnactState ConwayEra
 
   environmentSpec _ = govEnvSpec
 
   stateSpec _ = govProposalsSpec
 
   signalSpec _ = govProceduresSpec
 
-  genExecContext = do
-    txId <- arbitrary
-    proposalsSplit <- genProposalsSplit 50
-    enactState <- arbitrary
-    pure
-      ( txId
-      , proposalsSplit
-      , enactState
-      )
-
   runAgdaRule env st sig = unComputationResult $ Agda.govStep env st sig
 
-  translateInputs env@GovEnv {gePParams} st sig (txId, _proposalsSplit, enactState) = do
+  translateInputs env st sig enactState = do
     agdaEnv <- expectRight $ runSpecTransM ctx $ toSpecRep env
     agdaSt <- expectRight $ runSpecTransM ctx $ toSpecRep st
     agdaSig <- expectRight $ runSpecTransM ctx $ toSpecRep sig
@@ -69,6 +46,8 @@ instance
         ( txId
         , st
         , enactState
-            & ensPrevGovActionIdsL .~ toPrevGovActionIds (st ^. pRootsL)
-            & ensProtVerL .~ (gePParams ^. ppProtocolVersionL)
+            & ensPrevGovActionIdsL
+            .~ toPrevGovActionIds (st ^. pRootsL)
+            & ensProtVerL
+            .~ (gePParams ^. ppProtocolVersionL)
         )
diff --git a/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Gov.hs b/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Gov.hs
@@ -1,3 +1,4 @@
+{-# LANGUAGE DataKinds #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
@@ -13,11 +14,14 @@
 module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Gov () where
 
 import Cardano.Ledger.BaseTypes
-import Cardano.Ledger.CertState (CertState)
+import Cardano.Ledger.CertState (CertState, certDStateL, dsUnifiedL)
 import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance
 import Cardano.Ledger.Conway.Rules
+import Cardano.Ledger.UMap (umElemsL)
 import Data.Functor.Identity (Identity)
+import qualified Data.Map.Strict as Map
+import Lens.Micro ((^.))
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Core
@@ -36,13 +40,15 @@ instance
 
   toSpecRep GovEnv {..} = do
     enactState <- askCtx @(EnactState era)
+    let rewardAccounts = Map.keysSet $ geCertState ^. certDStateL . dsUnifiedL . umElemsL
     Agda.MkGovEnv
       <$> toSpecRep geTxId
       <*> toSpecRep geEpoch
       <*> toSpecRep gePParams
       <*> toSpecRep gePPolicy
       <*> toSpecRep enactState
       <*> toSpecRep geCertState
+      <*> toSpecRep rewardAccounts
 
 instance
   ( EraPParams era

diff --git a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs
@@ -156,7 +156,7 @@ spec =
           describe "DELEG" Deleg.spec
           describe "ENACT" Enact.spec
           xdescribe "EPOCH" Epoch.spec
-          xdescribe "GOV" Gov.spec
+          describe "GOV" Gov.spec
           describe "GOVCERT" GovCert.spec
           -- LEDGER tests pending on the dRep delegations cleanup in the spec:
           -- https://github.com/IntersectMBO/formal-ledger-specifications/issues/635