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 (>=.)

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

@@ -20,7 +20,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway () where
 
 import Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe (..))
 import Cardano.Ledger.Conway (Conway)
-import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParamsUpdate)
+import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..))
 import Cardano.Ledger.Conway.Governance (
   EnactState,
   GovProcedures (..),
@@ -30,7 +30,6 @@ import Cardano.Ledger.Conway.Governance (
   pRootsL,
   toPrevGovActionIds,
  )
-import Cardano.Ledger.Conway.PParams (THKD (..))
 import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure)
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
 import Cardano.Ledger.Crypto (StandardCrypto)
@@ -43,7 +42,6 @@ import Data.Foldable (Foldable (..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.OSet.Strict as OSet
 import qualified Data.Text as T
-import Data.Typeable (Typeable)
 import GHC.Generics (Generic)
 import Lens.Micro ((&), (.~), (^.))
 import qualified Lib as Agda
@@ -69,6 +67,7 @@ import Test.Cardano.Ledger.Constrained.Conway (
   utxoStateSpec,
   utxoTxSpec,
  )
+import Test.Cardano.Ledger.Constrained.Conway.Instances (PPUpdate)
 import Test.Cardano.Ledger.Conway.ImpTest (impAnn, logEntry)
 import Test.Cardano.Ledger.Imp.Common hiding (forAll, prop)
 
@@ -109,101 +108,106 @@ instance EraCrypto era ~ c => Inject (ConwayGovTransContext era) (TxId c) where
 instance EraCrypto era ~ c => Inject (ConwayGovTransContext era) (Proposals era) where
   inject (ConwayGovTransContext _ _ x) = x
 
-agdaCompatiblePPU :: IsConwayUniv fn => Term fn (PParamsUpdate Conway) -> Pred fn
-agdaCompatiblePPU ppup =
-  match ppup $
-    \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
-     cppMinFeeRefScriptCostPerByte ->
-        -- TODO enable pparam updates once they're properly
-        -- implemented in the spec
-        mconcat
-          [ isModified cppMinFeeA
-          , isUnmodified cppMinFeeB
-          , isUnmodified cppMaxBBSize
-          , isUnmodified cppMaxTxSize
-          , isUnmodified cppMaxBHSize
-          , isUnmodified cppKeyDeposit
-          , isUnmodified cppPoolDeposit
-          , isUnmodified cppEMax
-          , isUnmodified cppNOpt
-          , isUnmodified cppA0
-          , isUnmodified cppRho
-          , isUnmodified cppTau
-          , isUnmodified cppMinPoolCost
-          , isUnmodified cppCoinsPerUTxOByte
-          , isUnmodified cppCostModels
-          , isUnmodified cppPrices
-          , isUnmodified cppMaxTxExUnits
-          , isUnmodified cppMaxBlockExUnits
-          , isUnmodified cppMaxValSize
-          , isUnmodified cppCollateralPercentage
-          , isUnmodified cppMaxCollateralInputs
-          , isUnmodified cppPoolVotingThresholds
-          , isUnmodified cppDRepVotingThresholds
-          , isUnmodified cppCommitteeMinSize
-          , isUnmodified cppCommitteeMaxTermLength
-          , isUnmodified cppGovActionLifetime
-          , isUnmodified cppGovActionDeposit
-          , isUnmodified cppDRepDeposit
-          , isUnmodified cppDRepActivity
-          , isUnmodified cppMinFeeRefScriptCostPerByte
-          ]
-  where
-    isUnmodified ::
-      ( HasSpec fn a
-      , Typeable gs
-      , IsNormalType a
-      , IsConwayUniv fn
-      ) =>
-      Term fn (THKD gs StrictMaybe a) ->
-      Pred fn
-    isUnmodified x =
-      caseOn
-        x
-        (branch $ const True)
-        (branch $ const False)
-    isModified ::
-      ( HasSpec fn a
-      , Typeable gs
-      , IsNormalType a
-      , IsConwayUniv fn
-      ) =>
-      Term fn (THKD gs StrictMaybe a) ->
-      Pred fn
-    isModified x =
-      caseOn
-        x
-        (branch $ const False)
-        (branch $ const True)
+isUnmodified ::
+  forall fn t.
+  (IsConwayUniv fn, HasSpec fn t, IsNormalType t) =>
+  Term fn (StrictMaybe t) ->
+  Pred fn
+isUnmodified x =
+  caseOn
+    x
+    (branch $ const True)
+    (branch $ const False)
+
+isModified ::
+  forall fn t.
+  (IsConwayUniv fn, HasSpec fn t, IsNormalType t) =>
+  Term fn (StrictMaybe t) ->
+  Pred fn
+isModified x =
+  caseOn
+    x
+    (branch $ const False)
+    (branch $ const True)
+
+-- | Recall the PPUpdate is the SimpleRep of PParamsUpdate. So we constrain
+--   the that SimpleRep, instead of constraining PParamsUpdate
+agdaCompatiblePPU :: forall fn. IsConwayUniv fn => Specification fn PPUpdate
+agdaCompatiblePPU =
+  constrained
+    ( \ppupx ->
+        match
+          (ppupx :: Term fn PPUpdate)
+          ( \cppMinFeeA
+             cppMinFeeB
+             cppMaxBBSize
+             cppMaxTxSize
+             cppMaxBHSize
+             cppKeyDeposit
+             cppPoolDeposit
+             cppEMax
+             cppNOpt
+             cppA0
+             cppRho
+             cppTau
+             _decentral
+             _cppProtocolVersion
+             _minUTxOVal
+             cppMinPoolCost
+             cppCoinsPerUTxOByte
+             cppCostModels
+             cppPrices
+             cppMaxTxExUnits
+             cppMaxBlockExUnits
+             cppMaxValSize
+             cppCollateralPercentage
+             cppMaxCollateralInputs
+             _coinsPerUTxOByte
+             cppPoolVotingThresholds
+             cppDRepVotingThresholds
+             cppCommitteeMinSize
+             cppCommitteeMaxTermLength
+             cppGovActionLifetime
+             cppGovActionDeposit
+             cppDRepDeposit
+             cppDRepActivity
+             cppMinFeeRefScriptCostPerByte ->
+                -- TODO enable pparam updates once they're properly
+                -- implemented in the spec
+                Block
+                  [ isModified cppMinFeeA
+                  , isUnmodified cppMinFeeB
+                  , isUnmodified cppMaxBBSize
+                  , isUnmodified cppMaxTxSize
+                  , isUnmodified cppMaxBHSize
+                  , isUnmodified cppKeyDeposit
+                  , isUnmodified cppPoolDeposit
+                  , isUnmodified cppEMax
+                  , isUnmodified cppNOpt
+                  , isUnmodified cppA0
+                  , isUnmodified cppRho
+                  , isUnmodified cppTau
+                  , isUnmodified cppMinPoolCost
+                  , isUnmodified cppCoinsPerUTxOByte
+                  , isUnmodified cppCostModels
+                  , isUnmodified cppPrices
+                  , isUnmodified cppMaxTxExUnits
+                  , isUnmodified cppMaxBlockExUnits
+                  , isUnmodified cppMaxValSize
+                  , isUnmodified cppCollateralPercentage
+                  , isUnmodified cppMaxCollateralInputs
+                  , isUnmodified cppPoolVotingThresholds
+                  , isUnmodified cppDRepVotingThresholds
+                  , isUnmodified cppCommitteeMinSize
+                  , isUnmodified cppCommitteeMaxTermLength
+                  , isUnmodified cppGovActionLifetime
+                  , isUnmodified cppGovActionDeposit
+                  , isUnmodified cppDRepDeposit
+                  , isUnmodified cppDRepActivity
+                  , isUnmodified cppMinFeeRefScriptCostPerByte
+                  ]
+          )
+    )
 
 agdaCompatibleProposal ::
   IsConwayUniv fn =>
@@ -213,7 +217,8 @@ agdaCompatibleProposal prop =
   match prop $ \_ _ govAction _ ->
     caseOn
       govAction
-      (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
+      --  match against (ppup::PParamsUpdate) to get its SimpleRep (x::PPUpdate)
+      (branch $ \_ ppup _ -> match ppup (\x -> satisfies x agdaCompatiblePPU))
       (branch $ \_ _ -> True)
       (branch $ \_ _ -> True)
       (branch $ const True)
@@ -328,3 +333,42 @@ instance
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
       . computationResultToEither
       $ Agda.utxoStep env st sig
+
+{-
+PPUpdate
+  :: StrictMaybe Coin
+     -> StrictMaybe Coin
+     -> StrictMaybe Word32
+     -> StrictMaybe Word32
+     -> StrictMaybe Word32
+     -> StrictMaybe Coin
+     -> StrictMaybe Coin
+     -> StrictMaybe EpochInterval
+     -> StrictMaybe Natural
+     -> StrictMaybe NonNegativeInterval
+     -> StrictMaybe UnitInterval
+     -> StrictMaybe UnitInterval
+     -> StrictMaybe UnitInterval
+     -> StrictMaybe ProtVer
+     -> StrictMaybe Coin
+     -> StrictMaybe Coin
+     -> StrictMaybe Coin
+     -> StrictMaybe CostModels
+     -> StrictMaybe Prices
+     -> StrictMaybe ExUnits
+     -> StrictMaybe ExUnits
+     -> StrictMaybe Natural
+     -> StrictMaybe Natural
+     -> StrictMaybe Natural
+     -> StrictMaybe Coin
+     -> StrictMaybe PoolVotingThresholds
+     -> StrictMaybe DRepVotingThresholds
+     -> StrictMaybe Natural
+     -> StrictMaybe EpochInterval
+     -> StrictMaybe EpochInterval
+     -> StrictMaybe Coin
+     -> StrictMaybe Coin
+     -> StrictMaybe EpochInterval
+     -> StrictMaybe NonNegativeInterval
+     -> PPUpdate
+-}

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

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
       ]