Added the file State.hs

Added ToDelta as operation on Coin, RngSetFn as operation on Map Added a tractible type PParamSubset as a SimpleRep type for PParam specs Added PPUdates, canFollow abstraction Added CertState, UTxOState, LedgerState, EpochState Use reify to propagate invariants Added class WellFormed Made a few changes to Base.hs, replacing (MemberSpec []) with ErrorSpec Added HSpec tests Work on canFollow and dependencies, added (>=.)
IntersectMBO · May 3, 2024 · e994785 · e994785
1 parent 572b6fd
commit e994785
Show file tree

Hide file tree

Showing 15 changed files with 1,799 additions and 274 deletions.
diff --git a/libs/cardano-ledger-test/cardano-ledger-test.cabal b/libs/cardano-ledger-test/cardano-ledger-test.cabal
@@ -64,6 +64,7 @@ library
         Test.Cardano.Ledger.Constrained.Conway.PParams
         Test.Cardano.Ledger.Constrained.Conway.Gov
         Test.Cardano.Ledger.Constrained.Conway.Utxo
+        Test.Cardano.Ledger.Constrained.Conway.State
         Test.Cardano.Ledger.Examples.BabbageFeatures
         Test.Cardano.Ledger.Examples.AlonzoValidTxUTXOW
         Test.Cardano.Ledger.Examples.AlonzoInvalidTxUTXOW

diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Deleg.hs
@@ -23,8 +23,8 @@ dStateSpec ::
   IsConwayUniv fn =>
   Specification fn (DState (ConwayEra StandardCrypto))
 dStateSpec = constrained $ \ds ->
-  match ds $ \rewardMap _futureGenDelegs _genDelegs _rewards ->
-    match rewardMap $ \rdMap ptrMap sPoolMap _dRepMap ->
+  match ds $ \umap _futureGenDelegs _genDelegs _rewards ->
+    match umap $ \rdMap ptrMap sPoolMap _dRepMap ->
       [ assertExplain ["dom sPoolMap is a subset of dom rdMap"] $ dom_ sPoolMap `subset_` dom_ rdMap
       , assertExplain ["dom ptrMap is empty"] $ dom_ ptrMap ==. mempty
       ]

diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Gov.hs
@@ -24,6 +24,7 @@ import Lens.Micro
 
 import Constrained
 
+import Cardano.Ledger.Coin (Coin (..))
 import Cardano.Ledger.Conway (ConwayEra)
 import Cardano.Ledger.Conway.Core
 import Cardano.Ledger.Crypto (StandardCrypto)
@@ -401,52 +402,48 @@ wfPParamsUpdate ::
   IsConwayUniv fn =>
   Term fn (PParamsUpdate (ConwayEra StandardCrypto)) ->
   Pred fn
-wfPParamsUpdate ppu =
+wfPParamsUpdate pparamsUpdate =
   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
-            ]
+    [ assert $ pparamsUpdate /=. lit emptyPParamsUpdate
+    , match
+        pparamsUpdate
+        ( \ppupdate ->
+            match
+              ppupdate
+              ( \_feeA
+                 _feeB
+                 _minPoolCost
+                 maxBBSize
+                 maxTxSize
+                 maxBHSize
+                 _keyDeposit
+                 poolDeposit
+                 _emax
+                 _protocol
+                 -- Alonzo
+                 maxValSize
+                 collateralPercentage
+                 costModels
+                 -- Babbage
+                 _coinsperbyte
+                 -- Conway
+                 committeeMaxTermLength
+                 govActionLifetime
+                 govActionDeposit
+                 drepDeposit ->
+                    [ 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 (Coin 0))
+                    , govActionDeposit /=. lit (SJust (Coin 0))
+                    , drepDeposit /=. lit (SJust (Coin 0))
+                    , costModels ==. lit SNothing -- NOTE: this is because the cost
+                    -- model generator is way too slow
+                    ]
+              )
+        )
     ]