Removed GovRelation from GovEnv

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: 9233cb9f0e15dcdb5ef7ba49a21ee3820ee9aa76
-  --sha256: sha256-ea99nQ/j62FJkVdACKffVgLZ5mR1ZKwakSlNcSi5fJA=
+  tag: 1ffb1d13b8892c0943780cd7bd9e2724b5c20cab
+  --sha256: sha256-iiC0AwhPce6XnaGYHyQBeMSIttvn2c+Legu0tUgYOEM=
 
 index-state:
   -- Bump this if you need newer packages from Hackage

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

@@ -71,10 +71,12 @@ import Cardano.Ledger.Conway.Governance (
   isCommitteeVotingAllowed,
   isDRepVotingAllowed,
   isStakePoolVotingAllowed,
+  pRootsL,
   proposalsActionsMap,
   proposalsAddAction,
   proposalsAddVote,
   proposalsLookupId,
+  toPrevGovActionIds,
  )
 import Cardano.Ledger.Conway.Governance.Procedures (GovAction (..), foldrVotingProcedures)
 import Cardano.Ledger.Conway.PParams (
@@ -112,6 +114,7 @@ import qualified Data.Sequence.Strict as SSeq
 import qualified Data.Set as Set
 import GHC.Generics (Generic)
 import Lens.Micro
+import qualified Lens.Micro as L
 import NoThunks.Class (NoThunks (..))
 import Validation (failureUnless)
 
@@ -121,7 +124,6 @@ data GovEnv era = GovEnv
   { geTxId :: !(TxId (EraCrypto era))
   , geEpoch :: !EpochNo
   , gePParams :: !(PParams era)
-  , gePrevGovActionIds :: !(GovRelation StrictMaybe era)
   , gePPolicy :: !(StrictMaybe (ScriptHash (EraCrypto era)))
   , geCommitteeState :: !(CommitteeState era)
   }
@@ -330,11 +332,12 @@ govTransition ::
   TransitionRule (EraRule "GOV" era)
 govTransition = do
   TRC
-    ( GovEnv txid currentEpoch pp prevGovActionIds constitutionPolicy committeeState
+    ( GovEnv txid currentEpoch pp constitutionPolicy committeeState
       , st
       , gp
       ) <-
     judgmentContext
+  let prevGovActionIds = st ^. pRootsL . L.to toPrevGovActionIds
 
   expectedNetworkId <- liftSTS $ asks networkId
 

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

@@ -50,9 +50,7 @@ import Cardano.Ledger.Conway.Governance (
   GovProcedures (..),
   Proposals,
   constitutionScriptL,
-  pRootsL,
   proposalsGovStateL,
-  toPrevGovActionIds,
  )
 import Cardano.Ledger.Conway.Rules.Cert (CertEnv, ConwayCertPredFailure)
 import Cardano.Ledger.Conway.Rules.Certs (
@@ -383,7 +381,6 @@ ledgerTransition = do
                   (txIdTxBody txBody)
                   currentEpoch
                   pp
-                  (utxoState ^. utxosGovStateL . proposalsGovStateL . pRootsL . L.to toPrevGovActionIds)
                   (utxoState ^. utxosGovStateL . constitutionGovStateL . constitutionScriptL)
                   (certState ^. certVStateL . vsCommitteeStateL)
               , utxoState ^. utxosGovStateL . proposalsGovStateL

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

@@ -562,7 +562,6 @@ instance (Era era, Arbitrary (PParamsHKD Identity era)) => Arbitrary (GovEnv era
       <*> arbitrary
       <*> arbitrary
       <*> arbitrary
-      <*> arbitrary
 
 instance Era era => Arbitrary (VotingProcedure era) where
   arbitrary = VotingProcedure <$> arbitrary <*> arbitrary

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

@@ -6,7 +6,9 @@ module Test.Cardano.Ledger.Conformance.Orphans () where
 
 import GHC.Generics (Generic)
 import Lib
+import Numeric (showHex)
 import Test.Cardano.Ledger.Common (NFData, ToExpr)
+import Test.Cardano.Ledger.Conway.TreeDiff (Expr (..), ToExpr (..))
 
 deriving instance Generic GovActionState
 
@@ -62,6 +64,8 @@ deriving instance Eq UTxOEnv
 
 instance NFData GovAction
 
+instance NFData TxId
+
 instance NFData UTxOState
 
 instance NFData Vote
@@ -100,10 +104,19 @@ instance NFData Tx
 
 instance NFData UTxOEnv
 
+instance ToExpr Credential where
+  toExpr (KeyHashObj h) = App "KeyHashObj" [toExpr $ showHex h ""]
+  toExpr (ScriptObj h) = App "ScriptObj" [toExpr $ showHex h ""]
+
 instance ToExpr GovAction
 
+instance ToExpr GovRole
+
 instance ToExpr Vote
 
+instance ToExpr TxId where
+  toExpr (MkTxId x) = App "TxId" [toExpr $ showHex x ""]
+
 instance ToExpr GovActionState
 
 instance ToExpr GovProposal
@@ -112,6 +125,26 @@ instance ToExpr GovVote
 
 instance ToExpr GovSignal
 
+instance ToExpr PParams
+
 instance ToExpr GovEnv
 
 instance ToExpr EnactState
+
+instance ToExpr VDeleg
+
+instance ToExpr TxCert
+
+instance ToExpr TxBody
+
+instance ToExpr AgdaEmpty
+
+instance ToExpr Tag
+
+instance ToExpr TxWitnesses
+
+instance ToExpr Tx
+
+instance ToExpr UTxOState
+
+instance ToExpr UTxOEnv

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

@@ -61,14 +61,15 @@ import Cardano.Ledger.Conway.Governance (
   GovActionIx (..),
   GovActionState (..),
   GovProcedures (..),
-  GovPurposeId (GovPurposeId),
+  GovPurposeId (..),
   GovRelation (..),
   ProposalProcedure (..),
   Proposals,
   Vote (..),
   Voter (..),
   VotingProcedure (..),
   VotingProcedures (..),
+  ensProtVerL,
   foldrVotingProcedures,
   gasAction,
   gasReturnAddr,
@@ -613,7 +614,10 @@ instance SpecTranslate ctx (ConwayTxCert era) where
       <$> toSpecRep c
       <*> toSpecRep (SNothing @(Credential _ _))
 
-deriving instance SpecTranslate ctx (TxId era)
+instance SpecTranslate ctx (TxId era) where
+  type SpecRep (TxId era) = Agda.TxId
+
+  toSpecRep (TxId x) = Agda.MkTxId <$> toSpecRep x
 
 toAgdaTxBody ::
   ( SpecRep (TxOut era) ~ Agda.TxOut
@@ -731,7 +735,7 @@ instance
         committee <- toSpecRep x
         agdaLastId <- case h of
           SJust lastId -> toSpecRep lastId
-          SNothing -> pure (0, 0)
+          SNothing -> pure (Agda.MkTxId 0, 0)
         pure (committee, agdaLastId)
 
 instance
@@ -747,12 +751,19 @@ instance
 
   toSpecRep GovEnv {..} = do
     enactState <- askTransCtx @(GovEnv era)
+    let
+      protVer = gePParams ^. ppProtocolVersionL
+      -- TODO express this in agdaConstraints rather than doing it during
+      -- translation
+      enactStatePV =
+        enactState
+          & ensProtVerL .~ protVer
     Agda.MkGovEnv
       <$> toSpecRep geTxId
       <*> toSpecRep geEpoch
       <*> toSpecRep gePParams
       <*> toSpecRep gePPolicy
-      <*> toSpecRep enactState
+      <*> toSpecRep enactStatePV
 
 instance SpecTranslate ctx (Voter era) where
   type SpecRep (Voter era) = Agda.Voter
@@ -883,15 +894,23 @@ instance
 instance EraPParams era => SpecTranslate ctx (GovActionState era) where
   type SpecRep (GovActionState era) = Agda.GovActionState
 
-  toSpecRep gas@GovActionState {..} =
+  toSpecRep gas@GovActionState {..} = do
     Agda.MkGovActionState
       <$> agdaVoteMap
       <*> toSpecRep (gasReturnAddr gas)
       <*> toSpecRep gasExpiresAfter
       <*> toSpecRep action
-      <*> toSpecRep (nullifyIfNotNeeded gasId action)
+      <*> toSpecRep (nullifyIfNotNeeded prevGovActionId action)
     where
       action = gasAction gas
+      prevGovActionId =
+        case action of
+          ParameterChange x _ _ -> unGovPurposeId <$> x
+          HardForkInitiation x _ -> unGovPurposeId <$> x
+          UpdateCommittee x _ _ _ -> unGovPurposeId <$> x
+          NoConfidence x -> unGovPurposeId <$> x
+          NewConstitution x _ -> unGovPurposeId <$> x
+          _ -> SNothing
       agdaVoteMap = do
         drepVotes <- toSpecRep gasDRepVotes
         ccVotes <- toSpecRep gasCommitteeVotes
@@ -903,7 +922,8 @@ instance EraPParams era => SpecTranslate ctx (GovActionState era) where
             , first (\h -> (Agda.SPO, Agda.KeyHashObj h)) <$> spoVotes
             ]
       nullGovActionId = GovActionId (TxId def) (GovActionIx 0)
-      nullifyIfNotNeeded gaId = \case
+      nullifyIfNotNeeded SNothing = const nullGovActionId
+      nullifyIfNotNeeded (SJust gaId) = \case
         TreasuryWithdrawals {} -> nullGovActionId
         InfoAction -> nullGovActionId
         _ -> gaId

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

@@ -26,14 +26,15 @@ import Constrained
 import Cardano.Ledger.Conway (ConwayEra)
 import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Crypto (StandardCrypto)
+import Lens.Micro qualified as L
 import Test.Cardano.Ledger.Constrained.Conway.Instances
 import Test.Cardano.Ledger.Constrained.Conway.PParams
 
 govEnvSpec ::
   IsConwayUniv fn =>
   Specification fn (GovEnv (ConwayEra StandardCrypto))
 govEnvSpec = constrained $ \ge ->
-  match ge $ \_ _ pp _ _ _ ->
+  match ge $ \_ _ pp _ _ ->
     satisfies pp pparamsSpec
 
 -- NOTE: it is probably OK not to check uniqueness of ids here, because a clash
@@ -43,11 +44,11 @@ govProposalsSpec ::
   IsConwayUniv fn =>
   GovEnv (ConwayEra StandardCrypto) ->
   Specification fn (Proposals (ConwayEra StandardCrypto))
-govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} =
+govProposalsSpec GovEnv {geEpoch, gePPolicy} =
   constrained $ \props ->
     match props $ \ppupTree hardForkTree committeeTree constitutionTree unorderedProposals ->
       [ -- Protocol parameter updates
-        wellFormedChildren (lit $ coerce grPParamUpdate) ppupTree
+        wellFormedChildren ppupTree
       , allGASInTree ppupTree $ \gas ->
           [ isCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas)
           , onCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas) $
@@ -59,7 +60,7 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} =
       , forAll (snd_ ppupTree) (genHint treeGenHint)
       , genHint listSizeHint (snd_ ppupTree)
       , -- Hard forks
-        wellFormedChildren (lit $ coerce grHardFork) hardForkTree
+        wellFormedChildren hardForkTree
       , allGASInTree hardForkTree $ \gas ->
           isCon @"HardForkInitiation" (pProcGovAction_ . gasProposalProcedure_ $ gas)
       , allGASAndChildInTree hardForkTree $ \gas gas' ->
@@ -82,7 +83,7 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} =
       , forAll (snd_ hardForkTree) (genHint treeGenHint)
       , genHint listSizeHint (snd_ hardForkTree)
       , -- Committee
-        wellFormedChildren (lit $ coerce grCommittee) committeeTree
+        wellFormedChildren committeeTree
       , -- TODO: it would be nice to have a trick like `isCon` that can
         -- do disjunction without having to write down all the cases.
         allGASInTree committeeTree $ \gas ->
@@ -102,7 +103,7 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} =
       , forAll (snd_ committeeTree) (genHint treeGenHint)
       , genHint listSizeHint (snd_ committeeTree)
       , -- Constitution
-        wellFormedChildren (lit $ coerce grConstitution) constitutionTree
+        wellFormedChildren constitutionTree
       , allGASInTree constitutionTree $ \gas ->
           isCon @"NewConstitution" (pProcGovAction_ . gasProposalProcedure_ $ gas)
       , forAll (snd_ constitutionTree) (genHint treeGenHint)
@@ -128,7 +129,6 @@ govProposalsSpec GovEnv {geEpoch, gePPolicy, gePrevGovActionIds} =
       , genHint listSizeHint unorderedProposals
       ]
   where
-    GovRelation {..} = gePrevGovActionIds
     treeGenHint = (Just 2, 10)
     listSizeHint = 5
 
@@ -158,15 +158,13 @@ allGASAndChildInTree t k =
 
 wellFormedChildren ::
   IsConwayUniv fn =>
-  Term fn (StrictMaybe (GovActionId StandardCrypto)) ->
   Term fn ProposalTree ->
   Pred fn
-wellFormedChildren root rootAndTrees =
+wellFormedChildren rootAndTrees =
   match rootAndTrees $ \root' trees ->
-    [ assert $ root ==. root' -- The root matches the root given in the environment
-    , forAll trees $ \t ->
+    [ forAll trees $ \t ->
         [ -- Every node just below the root has the root as its parent
-          withPrevActId (rootLabel_ t) (assert . (==. root))
+          withPrevActId (rootLabel_ t) (assert . (==. root'))
         , -- Every node's children have the id of the node as its parent
           forAll' t $ \gas children ->
             [ forAll children $ \t' ->
@@ -289,7 +287,7 @@ wfGovAction ::
   Proposals (ConwayEra StandardCrypto) ->
   Term fn (GovAction (ConwayEra StandardCrypto)) ->
   Pred fn
-wfGovAction GovEnv {gePPolicy, geEpoch, gePrevGovActionIds, gePParams} ps govAction =
+wfGovAction GovEnv {gePPolicy, geEpoch, gePParams} ps govAction =
   caseOn
     govAction
     -- ParameterChange
@@ -344,26 +342,27 @@ wfGovAction GovEnv {gePPolicy, geEpoch, gePrevGovActionIds, gePParams} ps govAct
     -- InfoAction
     (branch $ \_ -> True)
   where
+    prevGovActionIds = ps ^. pRootsL . L.to toPrevGovActionIds
     constitutionIds =
-      (gePrevGovActionIds ^. grConstitutionL)
+      (prevGovActionIds ^. grConstitutionL)
         : [ SJust $ coerce $ gasId gas
           | gas <- actions
           , NewConstitution {} <- [pProcGovAction $ gasProposalProcedure gas]
           ]
     committeeIds =
-      (gePrevGovActionIds ^. grCommitteeL)
+      (prevGovActionIds ^. grCommitteeL)
         : [ SJust $ coerce $ gasId gas
           | gas <- actions
           , isCommitteeAction (pProcGovAction $ gasProposalProcedure gas)
           ]
     ppupIds =
-      (gePrevGovActionIds ^. grPParamUpdateL)
+      (prevGovActionIds ^. grPParamUpdateL)
         : [ SJust $ coerce $ gasId gas
           | gas <- actions
           , ParameterChange {} <- [pProcGovAction $ gasProposalProcedure gas]
           ]
     hardForkIds =
-      (gePrevGovActionIds ^. grHardForkL)
+      (prevGovActionIds ^. grHardForkL)
         : [ SJust $ coerce $ gasId gas
           | gas <- actions
           , HardForkInitiation {} <- [pProcGovAction $ gasProposalProcedure gas]

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/PrettyCore.hs

@@ -3350,7 +3350,6 @@ pcGovEnv GovEnv {..} =
     [ ("TxId", pcTxId geTxId)
     , ("Epoch", ppEpochNo geEpoch)
     , ("PParams", pcPParams reify gePParams)
-    , ("PrevGovActionId", pcPrevGovActionIds gePrevGovActionIds)
     ]
 
 instance Reflect era => PrettyA (GovEnv era) where