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 (>=.)
Added MinValSize to track size when using rngSet_
Fix omissions and problems with cardinality
Improved SizeSpec's in Sets, List, and Maps. Also add typeSpecOpt to Map and Set

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

@@ -23,7 +23,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway () where
 import Cardano.Ledger.BaseTypes (Inject (..), Network, StrictMaybe (..))
 import Cardano.Ledger.Coin (Coin)
 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 (
   Committee (..),
   EnactState (..),
@@ -41,7 +41,6 @@ import Cardano.Ledger.Conway.Governance (
   pRootsL,
   toPrevGovActionIds,
  )
-import Cardano.Ledger.Conway.PParams (THKD (..))
 import Cardano.Ledger.Conway.Rules (
   ConwayGovPredFailure,
   EnactSignal,
@@ -56,6 +55,7 @@ import Cardano.Ledger.Crypto (Crypto, StandardCrypto)
 import Cardano.Ledger.Keys (KeyRole (..))
 import Cardano.Ledger.TxIn (TxId)
 import Constrained
+import Constrained.Base (Pred (Block))
 import Control.Monad.Identity (Identity)
 import Data.Bifunctor (Bifunctor (..))
 import Data.Default.Class (Default (..))
@@ -64,7 +64,6 @@ import qualified Data.List.NonEmpty as NE
 import Data.Map.Strict (Map)
 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
@@ -99,7 +98,7 @@ import Test.Cardano.Ledger.Constrained.Conway (
   utxoTxSpec,
   vStateSpec,
  )
-import Test.Cardano.Ledger.Constrained.Conway.Instances ()
+import Test.Cardano.Ledger.Constrained.Conway.Instances (PPUpdate)
 import Test.Cardano.Ledger.Conway.ImpTest (impAnn, logEntry)
 import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop)
 
@@ -140,121 +139,138 @@ 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 $ \_ -> True)
-        (branch $ \_ -> False)
-    isModified ::
-      ( HasSpec fn a
-      , Typeable gs
-      , IsNormalType a
-      , IsConwayUniv fn
-      ) =>
-      Term fn (THKD gs StrictMaybe a) ->
-      Pred fn
-    isModified x =
-      (caseOn x)
-        (branch $ \_ -> False)
-        (branch $ \_ -> True)
-
 agdaCompatibleGovAction ::
   IsConwayUniv fn =>
   Term fn (GovAction Conway) ->
   Pred fn
 agdaCompatibleGovAction govAction =
   caseOn
     govAction
-    (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
+    (branch $ \_ ppup _ -> match ppup (\p -> satisfies p agdaCompatiblePPU))
     (branch $ \_ _ -> True)
     (branch $ \_ _ -> True)
     (branch $ const True)
     (branch $ \_ _ _ _ -> True)
     (branch $ \_ _ -> True)
     (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 =>
   Term fn (ProposalProcedure Conway) ->
   Pred fn
 agdaCompatibleProposal prop =
-  match prop $ \_ _ govAction _ -> agdaCompatibleGovAction govAction
+  match prop $ \_ _ govAction _ ->
+    caseOn
+      govAction
+      --  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)
+      (branch $ \_ _ _ _ -> True)
+      (branch $ \_ _ -> True)
+      (branch $ const True)
 
 agdaCompatibleGAS ::
   IsConwayUniv fn =>

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

@@ -41,7 +41,8 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (
   runSpecTransM,
   toTestRep,
  )
-import qualified Test.Cardano.Ledger.Generic.PrettyCore as Doc
+
+-- import qualified Test.Cardano.Ledger.Generic.PrettyCore as Doc
 import Test.Cardano.Ledger.Imp.Common
 import Test.Cardano.Ledger.Shelley.ImpTest (
   ImpTestM,
@@ -206,15 +207,15 @@ checkConformance implResTest agdaResTest = do
       ansiWlPretty
         { ppDel = \d ->
             mconcat
-              [ Doc.text "\ESC[91m(Impl: "
+              [ "\ESC[91m(Impl: "
               , d
-              , Doc.text ")\ESC[39m"
+              , ")\ESC[39m"
               ]
         , ppIns = \d ->
             mconcat
-              [ Doc.text "\ESC[92m(Agda: "
+              [ "\ESC[92m(Agda: "
               , d
-              , Doc.text ")\ESC[39m"
+              , ")\ESC[39m"
               ]
         }
     failMsg =

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

@@ -27,8 +27,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
       ]