Constrained generators for EPOCH rule

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

@@ -347,10 +347,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-test/cardano-ledger-test.cabal

@@ -168,7 +168,8 @@ library
         vector,
         constrained-generators,
         random,
-        FailT
+        FailT,
+        lens
 
 test-suite cardano-ledger-test
     type:             exitcode-stdio-1.0

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,12 +14,17 @@ module Test.Cardano.Ledger.Constrained.Conway.Epoch where
 import Cardano.Ledger.BaseTypes
 import Cardano.Ledger.Coin
 import Cardano.Ledger.Conway (Conway, ConwayEra)
+import Cardano.Ledger.Conway.Governance
 import Cardano.Ledger.Core
 import Cardano.Ledger.Crypto (StandardCrypto)
 import Cardano.Ledger.Shelley.API.Types
 import Constrained
-import Data.Map.Strict
+import Control.Lens
+import Data.Foldable
+import Data.Map.Strict (Map)
 import GHC.Generics (Generic)
+import Test.Cardano.Ledger.Constrained.Conway.Gov
+import Test.Cardano.Ledger.Constrained.Conway.Instances
 
 newtype EpochExecEnv era = EpochExecEnv
   { eeeStakeDistr :: Map (Credential 'Staking (EraCrypto era)) (CompactForm Coin)
@@ -26,8 +34,77 @@ newtype EpochExecEnv era = EpochExecEnv
 epochEnvSpec :: Specification fn (EpochExecEnv Conway)
 epochEnvSpec = TrueSpec
 
-epochStateSpec :: Specification fn (EpochState (ConwayEra StandardCrypto))
-epochStateSpec = TrueSpec
+epochStateSpec ::
+  Term ConwayFn EpochNo ->
+  Specification ConwayFn (EpochState (ConwayEra StandardCrypto))
+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 StandardCrypto) ->
+  Term ConwayFn (Proposals Conway) ->
+  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 (EraCrypto era) -> 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

@@ -48,13 +48,13 @@ govProposalsSpec ::
   GovEnv (ConwayEra StandardCrypto) ->
   Specification fn (Proposals (ConwayEra StandardCrypto))
 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 StandardCrypto)) ->
-  CertState Conway ->
+  Term fn (CertState Conway) ->
   Specification fn (Proposals Conway)
 proposalsSpec geEpoch gePPolicy geCertState =
   constrained $ \ [var|props|] ->
@@ -156,11 +156,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
                     ]
             )
@@ -174,7 +177,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) =>
@@ -280,6 +282,7 @@ withPrevActId gas k =
         -- InfoAction
         (branch $ \_ -> True)
     ]
+
 onHardFork ::
   (IsConwayUniv fn, IsPred p fn) =>
   Term fn (GovActionState (ConwayEra StandardCrypto)) ->

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

@@ -19,6 +19,7 @@
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE ViewPatterns #-}
 {-# OPTIONS_GHC -Wno-orphans #-}
 {-# OPTIONS_GHC -Wno-redundant-constraints #-}
 
@@ -54,6 +55,7 @@ module Test.Cardano.Ledger.Constrained.Conway.Instances.Ledger (
   gasCommitteeVotes_,
   gasDRepVotes_,
   gasProposalProcedure_,
+  psPParamUpdate_,
   ProposalsSplit (..),
   genProposalsSplit,
   proposalSplitSum,
@@ -134,7 +136,7 @@ import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
 import Cardano.Ledger.UMap
 import Cardano.Ledger.UTxO
 import Cardano.Ledger.Val (Val)
-import Constrained hiding (Value)
+import Constrained hiding (Sized, Value)
 import Constrained qualified as C
 import Constrained.Base (Binder (..), HasGenHint (..), Pred (..), Term (..))
 import Constrained.Spec.Map
@@ -170,6 +172,7 @@ import PlutusLedgerApi.V1 qualified as PV1
 import Test.Cardano.Ledger.Allegra.Arbitrary ()
 import Test.Cardano.Ledger.Alonzo.Arbitrary ()
 import Test.Cardano.Ledger.Constrained.Conway.Instances.Basic
+import Test.Cardano.Ledger.Conway.Arbitrary ()
 import Test.Cardano.Ledger.Core.Utils
 import Test.Cardano.Ledger.Shelley.Utils
 import Test.Cardano.Ledger.TreeDiff (ToExpr)
@@ -221,7 +224,7 @@ type ConwayTxBodyTypes c =
 instance (EraSpecPParams (ConwayEra c), IsConwayUniv fn, Crypto c) => HasSpec fn (ConwayTxBody (ConwayEra c))
 
 instance Crypto c => HasSimpleRep (ConwayTxBody (ConwayEra c)) where
-  type SimpleRep (ConwayTxBody (ConwayEra c)) = SOP '["ConwayTxBody" ::: ConwayTxBodyTypes c]
+  type TheSop (ConwayTxBody (ConwayEra c)) = '["ConwayTxBody" ::: ConwayTxBodyTypes c]
   toSimpleRep ConwayTxBody {..} =
     inject @"ConwayTxBody" @'["ConwayTxBody" ::: ConwayTxBodyTypes c]
       ctbSpendInputs
@@ -296,12 +299,15 @@ instance HasSimpleRep (StrictSeq a) where
   toSimpleRep = toList
   fromSimpleRep = StrictSeq.fromList
 instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (StrictSeq a)
+instance Forallable (StrictSeq a) a
 
 instance HasSimpleRep (Seq a) where
   type SimpleRep (Seq a) = [a]
   toSimpleRep = toList
   fromSimpleRep = Seq.fromList
-instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Seq a)
+instance HasSpec fn a => HasSpec fn (Seq a)
+instance Forallable (Seq a) a
+instance HasSpec fn a => C.Sized fn (Seq a)
 
 instance HasSimpleRep (Sized a)
 instance (IsConwayUniv fn, HasSpec fn a) => HasSpec fn (Sized a)
@@ -323,7 +329,6 @@ type ShelleyTxOutTypes era =
    , Value era
    ]
 instance (Era era, Val (Value era)) => HasSimpleRep (ShelleyTxOut era) where
-  -- type SimpleRep (ShelleyTxOut era) = SOP '["ShelleyTxOut" ::: ShelleyTxOutTypes era]
   type TheSop (ShelleyTxOut era) = '["ShelleyTxOut" ::: ShelleyTxOutTypes era]
   toSimpleRep (ShelleyTxOut addr val) =
     inject @"ShelleyTxOut" @'["ShelleyTxOut" ::: ShelleyTxOutTypes era]
@@ -340,7 +345,6 @@ type AlonzoTxOutTypes era =
    , StrictMaybe (DataHash (EraCrypto era))
    ]
 instance (Era era, Val (Value era)) => HasSimpleRep (AlonzoTxOut era) where
-  -- type SimpleRep (AlonzoTxOut era) = SOP '["AlonzoTxOut" ::: AlonzoTxOutTypes era]
   type TheSop (AlonzoTxOut era) = '["AlonzoTxOut" ::: AlonzoTxOutTypes era]
   toSimpleRep (AlonzoTxOut addr val mdat) =
     inject @"AlonzoTxOut" @'["AlonzoTxOut" ::: AlonzoTxOutTypes era]
@@ -978,13 +982,13 @@ type UMapTypes c =
    , Map (Credential 'Staking c) (DRep c)
    ]
 instance Crypto c => HasSimpleRep (UMap c) where
-  type SimpleRep (UMap c) = SOP '["UMap" ::: UMapTypes c]
+  type TheSop (UMap c) = '["UMap" ::: UMapTypes c]
   toSimpleRep um = inject @"UMap" @'["UMap" ::: UMapTypes c] (rdPairMap um) (ptrMap um) (sPoolMap um) (dRepMap um)
   fromSimpleRep rep = algebra @'["UMap" ::: UMapTypes c] rep unify
 instance (IsConwayUniv fn, Crypto c) => HasSpec fn (UMap c)
 
 instance HasSimpleRep RDPair where
-  type SimpleRep RDPair = SOP '["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]]
+  type TheSop RDPair = '["RDPair" ::: '[SimpleRep Coin, SimpleRep Coin]]
   toSimpleRep (RDPair rew dep) =
     inject
       @"RDPair"
@@ -1076,7 +1080,7 @@ type ProposalsType era =
    -- this right now.
    ]
 instance EraPParams era => HasSimpleRep (Proposals era) where
-  type SimpleRep (Proposals era) = SOP '["Proposals" ::: ProposalsType era]
+  type TheSop (Proposals era) = '["Proposals" ::: ProposalsType era]
   toSimpleRep props =
     inject @"Proposals" @'["Proposals" ::: ProposalsType era]
       (buildProposalTree $ coerce grPParamUpdate)
@@ -1120,7 +1124,13 @@ instance EraPParams era => HasSimpleRep (Proposals era) where
     where
       mkOMap (Node a ts) = a OMap.<| foldMap mkOMap ts
 
-instance (EraSpecPParams era, IsConwayUniv fn) => HasSpec fn (Proposals era)
+instance (EraSpecPParams era, IsConwayUniv fn, Arbitrary (Proposals era)) => HasSpec fn (Proposals era) where
+  shrinkWithTypeSpec _ props = shrink props
+
+psPParamUpdate_ ::
+  (EraSpecPParams era, Arbitrary (Proposals era), IsConwayUniv fn) =>
+  Term fn (Proposals era) -> Term fn (ProposalTree era)
+psPParamUpdate_ = sel @0
 
 data ProposalsSplit = ProposalsSplit
   { psPPChange :: Integer
@@ -1347,8 +1357,8 @@ instance
     (DRepPulser Conway Identity (RatifyState Conway))
   where
   type
-    SimpleRep (DRepPulser Conway Identity (RatifyState Conway)) =
-      SOP '["DRepPulser" ::: DRepPulserTypes]
+    TheSop (DRepPulser Conway Identity (RatifyState Conway)) =
+      '["DRepPulser" ::: DRepPulserTypes]
   toSimpleRep DRepPulser {..} =
     inject @"DRepPulser" @'["DRepPulser" ::: DRepPulserTypes]
       dpPulseSize
@@ -1412,7 +1422,7 @@ instance
   HasSpec fn (ShelleyTx era)
 
 instance EraSpecPParams era => HasSimpleRep (ShelleyTx era) where
-  type SimpleRep (ShelleyTx era) = SOP '["ShelleyTx" ::: ShelleyTxTypes era]
+  type TheSop (ShelleyTx era) = '["ShelleyTx" ::: ShelleyTxTypes era]
   toSimpleRep (ShelleyTx body wits auxdata) =
     inject @"ShelleyTx" @'["ShelleyTx" ::: ShelleyTxTypes era]
       body
@@ -1436,8 +1446,8 @@ type AlonzoTxAuxDataTypes era =
    ]
 instance AlonzoEraScript era => HasSimpleRep (AlonzoTxAuxData era) where
   type
-    SimpleRep (AlonzoTxAuxData era) =
-      SOP '["AlonzoTxOutData" ::: AlonzoTxAuxDataTypes era]
+    TheSop (AlonzoTxAuxData era) =
+      '["AlonzoTxOutData" ::: AlonzoTxAuxDataTypes era]
   toSimpleRep (AlonzoTxAuxData metaMap tsSeq _) =
     inject @"AlonzoTxAuxData" @'["AlonzoTxAuxData" ::: AlonzoTxAuxDataTypes era]
       metaMap
@@ -1460,8 +1470,8 @@ type AllegraTxAuxDataTypes era =
    ]
 instance Era era => HasSimpleRep (AllegraTxAuxData era) where
   type
-    SimpleRep (AllegraTxAuxData era) =
-      SOP '["AllegraTxOutData" ::: AllegraTxAuxDataTypes era]
+    TheSop (AllegraTxAuxData era) =
+      '["AllegraTxOutData" ::: AllegraTxAuxDataTypes era]
   toSimpleRep (AllegraTxAuxData metaMap tsSeq) =
     inject @"AllegraTxAuxData" @'["AllegraTxAuxData" ::: AllegraTxAuxDataTypes era]
       metaMap
@@ -1483,8 +1493,8 @@ type ShelleyTxAuxDataTypes era =
    ]
 instance Era era => HasSimpleRep (ShelleyTxAuxData era) where
   type
-    SimpleRep (ShelleyTxAuxData era) =
-      SOP '["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era]
+    TheSop (ShelleyTxAuxData era) =
+      '["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era]
   toSimpleRep (ShelleyTxAuxData metaMap) =
     inject @"ShelleyTxAuxData" @'["ShelleyTxAuxData" ::: ShelleyTxAuxDataTypes era]
       metaMap
@@ -1512,8 +1522,8 @@ type AlonzoTxWitsTypes c =
    ]
 instance AlonzoEraScript era => HasSimpleRep (AlonzoTxWits era) where
   type
-    SimpleRep (AlonzoTxWits era) =
-      SOP '["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)]
+    TheSop (AlonzoTxWits era) =
+      '["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)]
   toSimpleRep (AlonzoTxWits vkeyWits bootstrapWits _ _ _) =
     inject @"AlonzoTxWits" @'["AlonzoTxWits" ::: AlonzoTxWitsTypes (EraCrypto era)]
       vkeyWits
@@ -1529,8 +1539,8 @@ type ShelleyTxWitsTypes era =
    ]
 instance EraScript era => HasSimpleRep (ShelleyTxWits era) where
   type
-    SimpleRep (ShelleyTxWits era) =
-      SOP '["ShelleyTxWits" ::: ShelleyTxWitsTypes era]
+    TheSop (ShelleyTxWits era) =
+      '["ShelleyTxWits" ::: ShelleyTxWitsTypes era]
   toSimpleRep (ShelleyTxWits vkeyWits _ bootstrapWits) =
     inject @"ShelleyTxWits" @'["ShelleyTxWits" ::: ShelleyTxWitsTypes era]
       vkeyWits
@@ -1648,7 +1658,7 @@ type PulserTypes c =
    , RewardAns c
    ]
 instance HasSimpleRep (Pulser c) where
-  type SimpleRep (Pulser c) = SOP '["Pulser" ::: PulserTypes c]
+  type TheSop (Pulser c) = '["Pulser" ::: PulserTypes c]
   toSimpleRep (RSLP n free bal ans) =
     inject @"Pulser" @'["Pulser" ::: PulserTypes c]
       n