Merge pull request #4575 from IntersectMBO/ts-salvage-newtylespecs

Ts salvage newtylespecs
IntersectMBO · Sep 24, 2024 · c051be1 · c051be1
2 parents b8eab98 + 5fc4f81
commit c051be1
Show file tree

Hide file tree

Showing 20 changed files with 2,940 additions and 712 deletions.
diff --git a/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs b/...ardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs
@@ -114,7 +114,12 @@ import Test.Cardano.Ledger.Constrained.Conway (
   utxoStateSpec,
   utxoTxSpec,
  )
-import Test.Cardano.Ledger.Constrained.Conway.Instances ()
+import Test.Cardano.Ledger.Constrained.Conway.SimplePParams (
+  committeeMaxTermLength_,
+  committeeMinSize_,
+  protocolVersion_,
+ )
+
 import Test.Cardano.Ledger.Conway.Arbitrary ()
 import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)
 
@@ -390,19 +395,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
 
@@ -568,7 +573,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
     ]

diff --git a/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs b/libs/cardano-ledger-test/bench/Bench/Constrained/STS.hs
@@ -21,8 +21,13 @@ govEnv = genFromSpecWithSeed 10 30 (govEnvSpec @ConwayFn)
 singleProposalTreeSpec :: Specification ConwayFn ProposalTree
 singleProposalTreeSpec = constrained $ \ppupTree ->
   [ wellFormedChildren ppupTree
-  , allGASInTree ppupTree $ \gas ->
-      isCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas)
+  , satisfies
+      ppupTree
+      ( allGASInTree
+          ( \gas ->
+              isCon @"ParameterChange" (pProcGovAction_ . gasProposalProcedure_ $ gas)
+          )
+      )
   , forAll (snd_ ppupTree) (genHint $ (Just 2, 10))
   ]
 

diff --git a/libs/cardano-ledger-test/cardano-ledger-test.cabal b/libs/cardano-ledger-test/cardano-ledger-test.cabal
@@ -60,12 +60,16 @@ library
         Test.Cardano.Ledger.Constrained.Conway.Epoch
         Test.Cardano.Ledger.Constrained.Conway.Gov
         Test.Cardano.Ledger.Constrained.Conway.GovCert
+        Test.Cardano.Ledger.Constrained.Conway.InstancesBasic
         Test.Cardano.Ledger.Constrained.Conway.Instances
         Test.Cardano.Ledger.Constrained.Conway.Ledger
         Test.Cardano.Ledger.Constrained.Conway.NewEpoch
         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.LedgerTypes.Specs
+        Test.Cardano.Ledger.Constrained.Conway.LedgerTypes.WellFormed
         Test.Cardano.Ledger.Examples.BabbageFeatures
         Test.Cardano.Ledger.Examples.AlonzoValidTxUTXOW
         Test.Cardano.Ledger.Examples.AlonzoBBODY

diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Certs.hs
@@ -20,7 +20,6 @@ import Cardano.Ledger.Core
 import Cardano.Ledger.Credential (Credential (..))
 import Cardano.Ledger.Keys (KeyHash (..), KeyRole (..))
 import Cardano.Ledger.PoolParams (PoolParams (ppId))
-import Cardano.Ledger.UMap (dRepMap)
 import Constrained
 import Constrained.Base (Pred (..))
 import Data.Default.Class
@@ -34,15 +33,6 @@ import Test.Cardano.Ledger.Constrained.Conway.Cert (txCertSpec)
 import Test.Cardano.Ledger.Constrained.Conway.Deleg (someZeros)
 import Test.Cardano.Ledger.Constrained.Conway.Instances
 import Test.Cardano.Ledger.Constrained.Conway.PParams (pparamsSpec)
-import Test.Cardano.Ledger.Generic.PrettyCore
-import Test.QuickCheck hiding (forAll)
-
-main :: IO ()
-main = do
-  context <- generate $ genFromSpec @ConwayFn (constrained $ \x -> sizeOf_ x ==. 3)
-  state <- generate $ genFromSpec @ConwayFn (bootstrapDStateSpec context)
-  putStrLn ("\n\nDRepDelegs\n" ++ show (prettyA (dRepMap (dsUnified state))))
-  putStrLn ("\n\nContext\n" ++ show (prettyA context))
 
 -- =======================================================