Added StateSpecs

Added names to variables in StateSpecs
Added better error messages, better printing of graphs
Added selector functions for SimplePParams
Fixed Hspec tests, still one to go.

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

@@ -111,7 +111,12 @@ import Test.Cardano.Ledger.Constrained.Conway (
   utxoStateSpec,
   utxoTxSpec,
  )
-import Test.Cardano.Ledger.Constrained.Conway.Instances ()
+import Test.Cardano.Ledger.Constrained.Conway.Instances (
+  committeeMaxTermLength_,
+  committeeMinSize_,
+  protocolVersion_,
+ )
+
 import Test.Cardano.Ledger.Conway.Arbitrary ()
 import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)
 
@@ -387,19 +392,19 @@ ratifyStateSpec _ RatifyEnv {..} =
        in Map.keysSet m
     -- Bootstrap is not in the spec
     disableBootstrap :: IsConwayUniv fn => Term fn (PParams Conway) -> Pred fn
-    disableBootstrap pp = match pp $ \pp' ->
-      match (sel @12 pp') $ \major _ ->
-        assert $ major ==. lit (natVersion @10)
+    disableBootstrap pp = match pp $ \simplepp ->
+      match (protocolVersion_ simplepp) $ \major _ ->
+        assert $ not_ (major ==. lit (natVersion @9))
+
     preferSmallerCCMinSizeValues ::
       IsConwayUniv fn =>
       Term fn (PParams Conway) ->
       Pred fn
-    preferSmallerCCMinSizeValues pp = match pp $ \pp' ->
-      match (sel @24 pp') $ \ccMinSize ->
-        satisfies ccMinSize $
-          chooseSpec
-            (1, TrueSpec)
-            (1, constrained (<=. committeeSize))
+    preferSmallerCCMinSizeValues pp = match pp $ \simplepp ->
+      satisfies (committeeMinSize_ simplepp) $
+        chooseSpec
+          (1, TrueSpec)
+          (1, constrained (<=. committeeSize))
       where
         committeeSize = lit . fromIntegral . Set.size $ ccColdKeys
 
@@ -558,7 +563,7 @@ enactStateSpec ::
   Specification fn (EnactState Conway)
 enactStateSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} =
   constrained' $ \_ _ curPParams _ treasury wdrls _ ->
-    [ match curPParams $ \pp -> match (sel @25 pp) (==. lit ceecMaxTerm)
+    [ match curPParams $ \simplepp -> committeeMaxTermLength_ simplepp ==. lit ceecMaxTerm
     , assert $ sum_ (rng_ wdrls) <=. treasury
     , assert $ treasury ==. lit ceeeTreasury
     ]

libs/cardano-ledger-test/cardano-ledger-test.cabal

@@ -66,6 +66,8 @@ library
         Test.Cardano.Ledger.Constrained.Conway.PParams
         Test.Cardano.Ledger.Constrained.Conway.Pool
         Test.Cardano.Ledger.Constrained.Conway.Utxo
+        Test.Cardano.Ledger.Constrained.Conway.SimplePParams
+        Test.Cardano.Ledger.Constrained.Conway.StateSpecs
         Test.Cardano.Ledger.Examples.BabbageFeatures
         Test.Cardano.Ledger.Examples.AlonzoValidTxUTXOW
         Test.Cardano.Ledger.Examples.AlonzoBBODY

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

@@ -4,32 +4,28 @@
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE QuasiQuotes #-}
 {-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE ViewPatterns #-}
 
 -- | Specs necessary to generate, environment, state, and signal
 -- for the GOV rule
 module Test.Cardano.Ledger.Constrained.Conway.Gov where
 
-import Cardano.Ledger.Shelley.HardForks qualified as HardForks
-import Data.Foldable
-
-import Data.Coerce
-
 import Cardano.Ledger.BaseTypes
 import Cardano.Ledger.CertState
+import Cardano.Ledger.Conway (Conway, ConwayEra)
+import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Conway.Governance
-import Cardano.Ledger.Conway.PParams
 import Cardano.Ledger.Conway.Rules
+import Cardano.Ledger.Crypto (StandardCrypto)
+import Cardano.Ledger.Shelley.HardForks qualified as HardForks
+import Constrained
+import Data.Coerce
+import Data.Foldable
 import Data.Map qualified as Map
 import Data.Set qualified as Set
 import Lens.Micro
-
-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
@@ -49,25 +45,26 @@ govProposalsSpec ::
   GovEnv (ConwayEra StandardCrypto) ->
   Specification fn (Proposals (ConwayEra StandardCrypto))
 govProposalsSpec GovEnv {geEpoch, gePPolicy} =
-  constrained $ \props ->
-    match props $ \ppupTree hardForkTree committeeTree constitutionTree unorderedProposals ->
+  constrained $ \ [var|props|] ->
+    match props $ \ [var|ppupTree|] [var|hardForkTree|] [var|committeeTree|] [var|constitutionTree|] [var|unorderedProposals|] ->
       [ -- Protocol parameter updates
         wellFormedChildren ppupTree
-      , allGASInTree ppupTree $ \gas ->
+      , allGASInTree ppupTree $ \ [var|gas|] ->
           [ isCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas)
           , onCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas) $
-              \_ ppup policy ->
-                [ wfPParamsUpdate ppup
+              \_ [var|ppup|] [var|policy|] ->
+                [ assert $ ppup /=. lit emptyPParamsUpdate
+                , satisfies ppup wfPParamsUpdateSpec
                 , assert $ policy ==. lit gePPolicy
                 ]
           ]
       , forAll (snd_ ppupTree) (genHint treeGenHint)
       , genHint listSizeHint (snd_ ppupTree)
       , -- Hard forks
         wellFormedChildren hardForkTree
-      , allGASInTree hardForkTree $ \gas ->
+      , allGASInTree hardForkTree $ \ [var|gas|] ->
           isCon @"HardForkInitiation" (pProcGovAction_ . gasProposalProcedure_ $ gas)
-      , allGASAndChildInTree hardForkTree $ \gas gas' ->
+      , allGASAndChildInTree hardForkTree $ \ [var|gas|] [var|gas'|] ->
           [ onHardFork gas $ \_ pv ->
               onHardFork gas' $ \_ pv' ->
                 match pv $ \majV minV ->
@@ -313,7 +310,8 @@ wfGovAction GovEnv {gePPolicy, geEpoch, gePParams} ps govAction =
     -- ParameterChange
     ( branch $ \mPrevActionId ppUpdate policy ->
         [ assert $ mPrevActionId `elem_` lit ppupIds
-        , wfPParamsUpdate ppUpdate
+        , assert $ ppUpdate /=. lit emptyPParamsUpdate
+        , satisfies ppUpdate wfPParamsUpdateSpec
         , assert $ policy ==. lit gePPolicy
         ]
     )
@@ -417,56 +415,58 @@ wfGovAction GovEnv {gePPolicy, geEpoch, gePParams} ps govAction =
 
     actions = toList $ proposalsActions ps
 
-wfPParamsUpdate ::
-  IsConwayUniv fn =>
-  Term fn (PParamsUpdate (ConwayEra StandardCrypto)) ->
-  Pred fn
-wfPParamsUpdate ppu =
-  toPred
-    [ assert $ ppu /=. lit emptyPParamsUpdate
-    , match ppu $
-        \_cppMinFeeA
-         _cppMinFeeB
-         cppMaxBBSize
-         cppMaxTxSize
-         cppMaxBHSize
-         _cppKeyDeposit
-         cppPoolDeposit
-         _cppEMax
-         _cppNOpt
-         _cppA0
-         _cppRho
-         _cppTau
-         _cppProtocolVersion
-         _cppMinPoolCost
-         _cppCoinsPerUTxOByte
-         cppCostModels
-         _cppPrices
-         _cppMaxTxExUnits
-         _cppMaxBlockExUnits
-         cppMaxValSize
-         cppCollateralPercentage
-         _cppMaxCollateralInputs
-         _cppPoolVotingThresholds
-         _cppDRepVotingThresholds
-         _cppCommitteeMinSize
-         cppCommitteeMaxTermLength
-         cppGovActionLifetime
-         cppGovActionDeposit
-         cppDRepDeposit
-         _cppDRepActivity
-         _cppMinFeeRefScriptCoinsPerByte ->
-            [ cppMaxBBSize /=. lit (THKD $ SJust 0)
-            , cppMaxTxSize /=. lit (THKD $ SJust 0)
-            , cppMaxBHSize /=. lit (THKD $ SJust 0)
-            , cppMaxValSize /=. lit (THKD $ SJust 0)
-            , cppCollateralPercentage /=. lit (THKD $ SJust 0)
-            , cppCommitteeMaxTermLength /=. lit (THKD $ SJust $ EpochInterval 0)
-            , cppGovActionLifetime /=. lit (THKD $ SJust $ EpochInterval 0)
-            , cppPoolDeposit /=. lit (THKD $ SJust mempty)
-            , cppGovActionDeposit /=. lit (THKD $ SJust mempty)
-            , cppDRepDeposit /=. lit (THKD $ SJust mempty)
-            , cppCostModels ==. lit (THKD SNothing) -- NOTE: this is because the cost
-            -- model generator is way too slow
-            ]
-    ]
+wfPParamsUpdateSpec :: forall fn. IsConwayUniv fn => Specification fn (PParamsUpdate Conway)
+wfPParamsUpdateSpec =
+  constrained' $ \ppupdate ->
+    -- Note that ppupdate :: SimplePPUpdate
+    match ppupdate $
+      \_minFeeA
+       _minFeeB
+       maxBBSize
+       maxTxSize
+       maxBHSize
+       _keyDeposit
+       poolDeposit
+       _eMax
+       _nOpt
+       _a0
+       _rho
+       _tau
+       _decentral
+       _protocolVersion
+       _minUTxOValue
+       _minPoolCost
+       -- Alonzo
+       _coinsPerUTxOWord
+       costModels
+       _prices
+       _maxTxExUnits
+       _maBlockExUnits
+       maxValSize
+       collateralPercentage
+       _MaxCollateralInputs
+       -- Babbage
+       _coinsPerUTxOByte
+       -- Conway
+       _poolVotingThresholds
+       _drepVotingThresholds
+       _committeeMinSize
+       committeeMaxTermLength
+       govActionLifetime
+       govActionDeposit
+       dRepDeposit
+       _drepActivity
+       _minFeeRefScriptCostPerByte ->
+          [ maxBBSize /=. lit (SJust 0)
+          , maxTxSize /=. lit (SJust 0)
+          , maxBHSize /=. lit (SJust 0)
+          , maxValSize /=. lit (SJust 0)
+          , collateralPercentage /=. lit (SJust 0)
+          , committeeMaxTermLength /=. lit (SJust $ EpochInterval 0)
+          , govActionLifetime /=. lit (SJust $ EpochInterval 0)
+          , poolDeposit /=. lit (SJust mempty)
+          , govActionDeposit /=. lit (SJust mempty)
+          , dRepDeposit /=. lit (SJust mempty)
+          , costModels ==. lit (SNothing) -- NOTE: this is because the cost
+          -- model generator is way too slow
+          ]