Constrained generators for EPOCH rule (#4740)

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

@@ -346,10 +346,17 @@ instance
     pure $ ProposalsNewActions ps gass
 
 instance
-  (EraPParams era, Arbitrary (PParamsUpdate era), Arbitrary (PParamsHKD StrictMaybe era)) =>
+  (EraPParams era, Arbitrary (PParamsHKD StrictMaybe era)) =>
   Arbitrary (Proposals era)
   where
   arbitrary = genProposals (0, 30)
+  shrink ps =
+    [ ps'
+    | gais' <- shrink gais
+    , let (ps', _) = proposalsRemoveWithDescendants (gais Set.\\ gais') ps
+    ]
+    where
+      gais = Set.fromList (toList $ proposalsIds ps)
 
 genProposals ::
   forall era.

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

@@ -14,6 +14,7 @@
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
 {-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
@@ -30,6 +31,8 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
   externalFunctions,
 ) where
 
+import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN)
+import Cardano.Ledger.Address (RewardAccount)
 import Cardano.Ledger.BaseTypes (
   EpochInterval (..),
   EpochNo (..),
@@ -72,14 +75,18 @@ import Cardano.Ledger.Conway.Rules (
   spoAccepted,
   spoAcceptedRatio,
  )
+import Cardano.Ledger.Credential (Credential)
 import Cardano.Ledger.DRep (DRep (..))
 import Cardano.Ledger.PoolDistr (IndividualPoolStake (..))
 import Constrained hiding (inject)
+import Data.Either (isRight)
 import Data.Foldable (Foldable (..))
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
+import Data.Maybe (fromMaybe)
 import Data.Ratio (denominator, numerator, (%))
 import qualified Data.Sequence.Strict as SSeq
+import Data.Set (Set)
 import qualified Data.Set as Set
 import GHC.Generics (Generic)
 import Lens.Micro (Lens', lens, (^.))
@@ -103,29 +110,19 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
   signatureFromInteger,
  )
 import Test.Cardano.Ledger.Constrained.Conway (
-  EpochExecEnv,
-  IsConwayUniv,
-  coerce_,
-  epochEnvSpec,
-  epochSignalSpec,
-  epochStateSpec,
   newEpochStateSpec,
  )
+import Test.Cardano.Ledger.Constrained.Conway.Epoch
+import Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger
 import Test.Cardano.Ledger.Constrained.Conway.Instances.PParams (
   committeeMaxTermLength_,
   committeeMinSize_,
   protocolVersion_,
  )
 
-import Cardano.Crypto.DSIGN (SignedDSIGN (..), verifySignedDSIGN)
 import Cardano.Crypto.Hash (ByteString, Hash)
-import Cardano.Ledger.Address (RewardAccount)
-import Cardano.Ledger.Credential (Credential)
 import Cardano.Ledger.Crypto (DSIGN, HASH)
 import Cardano.Ledger.Keys (KeyRole (..), VKey (..))
-import Data.Either (isRight)
-import Data.Maybe (fromMaybe)
-import Data.Set (Set)
 import Test.Cardano.Ledger.Conway.Arbitrary ()
 import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)
 
@@ -572,15 +569,17 @@ nameGovAction UpdateCommittee {} = "UpdateCommittee"
 nameGovAction NewConstitution {} = "NewConstitution"
 nameGovAction InfoAction {} = "InfoAction"
 
-instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" ConwayEra where
+-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias
+-- and those shouldn't go in instance heads apparently.
+instance fn ~ ConwayFn => ExecSpecRule fn "EPOCH" ConwayEra where
   type ExecContext fn "EPOCH" ConwayEra = [GovActionState ConwayEra]
   type ExecEnvironment fn "EPOCH" ConwayEra = EpochExecEnv ConwayEra
 
   environmentSpec _ = epochEnvSpec
 
-  stateSpec _ _ = epochStateSpec
+  stateSpec _ = epochStateSpec . lit . eeeEpochNo
 
-  signalSpec _ _ _ = epochSignalSpec
+  signalSpec _ env _ = epochSignalSpec (eeeEpochNo env)
 
   runAgdaRule env st sig = unComputationResult_ $ Agda.epochStep env st sig
 
@@ -589,15 +588,17 @@ instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" ConwayEra where
 nameEpoch :: EpochNo -> String
 nameEpoch x = show x
 
-instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" ConwayEra where
+-- The `fn ~ ConwayFn` thing here is because `ConwayFn` is a type alias
+-- and those shouldn't go in instance heads apparently.
+instance fn ~ ConwayFn => ExecSpecRule fn "NEWEPOCH" ConwayEra where
   type ExecContext fn "NEWEPOCH" ConwayEra = [GovActionState ConwayEra]
   type ExecEnvironment fn "NEWEPOCH" ConwayEra = EpochExecEnv ConwayEra
 
   environmentSpec _ = epochEnvSpec
 
   stateSpec _ _ = newEpochStateSpec
 
-  signalSpec _ _ _ = epochSignalSpec
+  signalSpec _ env _ = epochSignalSpec (eeeEpochNo env)
 
   runAgdaRule env st sig = unComputationResult_ $ Agda.newEpochStep env st sig
 

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

@@ -1,8 +1,11 @@
 {-# LANGUAGE DataKinds #-}
 {-# LANGUAGE DeriveGeneric #-}
 {-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE ViewPatterns #-}
 
 -- | Specs necessary to generate, environment, state, and signal
 -- for the EPOCH rule
@@ -11,21 +14,96 @@ module Test.Cardano.Ledger.Constrained.Conway.Epoch where
 import Cardano.Ledger.BaseTypes
 import Cardano.Ledger.Coin
 import Cardano.Ledger.Conway (ConwayEra)
+import Cardano.Ledger.Conway.Governance
 import Cardano.Ledger.Shelley.API.Types
 import Constrained
-import Data.Map.Strict
+import Data.Foldable
+import Data.Map.Strict (Map)
 import GHC.Generics (Generic)
+import Lens.Micro.Extras
+import Test.Cardano.Ledger.Constrained.Conway.Gov
+import Test.Cardano.Ledger.Constrained.Conway.Instances
 
-newtype EpochExecEnv era = EpochExecEnv
+data EpochExecEnv era = EpochExecEnv
   { eeeStakeDistr :: Map (Credential 'Staking) (CompactForm Coin)
+  , eeeEpochNo :: EpochNo
   }
   deriving (Generic, Eq, Show)
 
 epochEnvSpec :: Specification fn (EpochExecEnv ConwayEra)
 epochEnvSpec = TrueSpec
 
-epochStateSpec :: Specification fn (EpochState ConwayEra)
-epochStateSpec = TrueSpec
+epochStateSpec ::
+  Term ConwayFn EpochNo ->
+  Specification ConwayFn (EpochState ConwayEra)
+epochStateSpec epochNo = constrained $ \es ->
+  match es $ \_accountState ledgerState _snapShots _nonMyopic ->
+    match ledgerState $ \utxoState certState ->
+      match utxoState $ \_utxo _deposited _fees govState _stakeDistr _donation ->
+        match govState $ \ [var| proposals |] _committee constitution _curPParams _prevPParams _futPParams drepPulsingState ->
+          [ match constitution $ \_ policy ->
+              proposals `satisfies` proposalsSpec epochNo policy certState
+          , caseOn
+              drepPulsingState
+              -- DRPulsing
+              ( branch $ \pulser ->
+                  match pulser $ \_size _stakeMap _index _stakeDistr _stakePoolDistr _drepDistr _drepState pulseEpoch _committeeState _enactState pulseProposals _proposalDeposits _poolParams ->
+                    [ assert $ pulseEpoch ==. epochNo
+                    , forAll pulseProposals $ \gas ->
+                        match gas $ \gasId _ _ _ _ _ _ ->
+                          proposalExists gasId proposals
+                    , -- TODO: something is wrong in this case and I haven't figured out what yet
+                      assert False
+                    ]
+              )
+              -- DRComplete
+              ( branch $ \_snap ratifyState ->
+                  match ratifyState $ \enactState [var| enacted |] expired _delayed ->
+                    [ forAll expired $ \ [var| gasId |] ->
+                        proposalExists gasId proposals
+                    , -- TODO: this isn't enough, we need to ensure it's at most
+                      -- one of each type of action that's being enacted
+                      forAll enacted $ \govact ->
+                        [ reify proposals enactableProposals $ \enactable -> govact `elem_` enactable
+                        , assert $ not_ $ gasId_ govact `member_` expired
+                        ]
+                    , -- TODO: this is a hack to get around the todo above!
+                      assert $ sizeOf_ enacted <=. 1
+                    , match enactState $
+                        \_cc _con _cpp _ppp _tr _wth prevGACTIDS ->
+                          reify proposals (toPrevGovActionIds . view pRootsL) (prevGACTIDS ==.)
+                    ]
+              )
+          ]
 
-epochSignalSpec :: Specification fn EpochNo
-epochSignalSpec = TrueSpec
+proposalExists ::
+  Term ConwayFn GovActionId ->
+  Term ConwayFn (Proposals ConwayEra) ->
+  Pred ConwayFn
+proposalExists gasId proposals =
+  reify proposals proposalsActionsMap $ \actionMap ->
+    gasId `member_` dom_ actionMap
+
+epochSignalSpec :: EpochNo -> Specification ConwayFn EpochNo
+epochSignalSpec curEpoch = constrained $ \e ->
+  elem_ e (lit [curEpoch, succ curEpoch])
+
+enactableProposals :: Proposals era -> [GovActionState era]
+enactableProposals proposals =
+  [ gact'
+  | gact <- toList (proposalsActions proposals)
+  , gact' <- withGovActionParent gact [gact] $
+      \_ mparent _ ->
+        case mparent of
+          SNothing -> [gact]
+          SJust (GovPurposeId gpid')
+            | isRoot gpid' proposals -> [gact]
+            | otherwise -> []
+  ]
+
+isRoot :: GovActionId -> Proposals era -> Bool
+isRoot gid (view pRootsL -> GovRelation {..}) =
+  SJust gid
+    `elem` [getGID grPParamUpdate, getGID grHardFork, getGID grCommittee, getGID grConstitution]
+  where
+    getGID = fmap unGovPurposeId . prRoot

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

@@ -47,13 +47,13 @@ govProposalsSpec ::
   GovEnv ConwayEra ->
   Specification fn (Proposals ConwayEra)
 govProposalsSpec GovEnv {geEpoch, gePPolicy, geCertState} =
-  proposalsSpec (lit geEpoch) (lit gePPolicy) geCertState
+  proposalsSpec (lit geEpoch) (lit gePPolicy) (lit geCertState)
 
 proposalsSpec ::
   IsConwayUniv fn =>
   Term fn EpochNo ->
   Term fn (StrictMaybe ScriptHash) ->
-  CertState ConwayEra ->
+  Term fn (CertState ConwayEra) ->
   Specification fn (Proposals ConwayEra)
 proposalsSpec geEpoch gePPolicy geCertState =
   constrained $ \ [var|props|] ->
@@ -155,11 +155,14 @@ proposalsSpec geEpoch gePPolicy geCertState =
                 Explain (pure "TreasuryWithdrawal fails") $
                   Block
                     [ dependsOn gasOther withdrawMap
-                    , forAll (dom_ withdrawMap) $ \ [var|rewAcnt|] ->
-                        match rewAcnt $ \ [var|network|] [var|credential|] ->
-                          [ network ==. lit Testnet
-                          , credential `member_` lit registeredCredentials
-                          ]
+                    , match geCertState $ \_vState _pState [var|dState|] ->
+                        match dState $ \ [var|rewardMap|] _ _ _ ->
+                          reify rewardMap (Map.keysSet . umElems) $ \ [var|registeredCredentials|] ->
+                            forAll (dom_ withdrawMap) $ \ [var|rewAcnt|] ->
+                              match rewAcnt $ \ [var|network|] [var|credential|] ->
+                                [ network ==. lit Testnet
+                                , credential `member_` registeredCredentials
+                                ]
                     , assert $ policy ==. gePPolicy
                     ]
             )
@@ -173,7 +176,6 @@ proposalsSpec geEpoch gePPolicy geCertState =
   where
     treeGenHint = (Just 2, 10)
     listSizeHint = 5
-    registeredCredentials = Map.keysSet $ umElems $ dsUnified $ certDState geCertState
 
 allGASInTree ::
   (IsConwayUniv fn, IsPred p fn) =>
@@ -279,6 +281,7 @@ withPrevActId gas k =
         -- InfoAction
         (branch $ \_ -> True)
     ]
+
 onHardFork ::
   (IsConwayUniv fn, IsPred p fn) =>
   Term fn (GovActionState ConwayEra) ->