Ts newstyle specs

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

@@ -38,6 +38,8 @@ import Cardano.Ledger.Conway.Governance (
   gasAction,
   pRootsL,
   toPrevGovActionIds,
+  -- GovAction(..),
+  -- ProposalProcedure(..),
  )
 import Cardano.Ledger.Conway.Rules (
   ConwayGovPredFailure,
@@ -52,6 +54,8 @@ 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 (..))
@@ -97,7 +101,8 @@ 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)
 
@@ -138,6 +143,148 @@ instance EraCrypto era ~ c => Inject (ConwayGovTransContext era) (TxId c) where
 instance EraCrypto era ~ c => Inject (ConwayGovTransContext era) (Proposals era) where
   inject (ConwayGovTransContext _ _ x) = x
 
+{-
+agdaCompatibleGovAction ::
+  IsConwayUniv fn =>
+  Term fn (GovAction Conway) ->
+  Pred fn
+agdaCompatibleGovAction govAction =
+  caseOn
+    govAction
+    (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 _ ->
+    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 =>
+  Term fn (GovActionState Conway) ->
+  Pred fn
+agdaCompatibleGAS gas =
+  match gas $ \_ _ _ _ prop _ _ -> agdaCompatibleProposal prop
+-}
+
 instance
   ( NFData (SpecRep (ConwayGovPredFailure Conway))
   , IsConwayUniv fn

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

@@ -41,6 +41,7 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Core (
   runSpecTransM,
   toTestRep,
  )
+
 import Test.Cardano.Ledger.Imp.Common
 import Test.Cardano.Ledger.Shelley.ImpTest (
   ImpTestM,
@@ -341,7 +342,7 @@ generatesWithin ::
 generatesWithin gen timeout =
   prop (aName <> " generates in reasonable time")
     . forAllShow gen showExpr
-    $ \x -> within timeout $ ioProperty (evaluateDeep x $> ())
+    $ \x -> within timeout $ withMaxSuccess 2 $ ioProperty (evaluateDeep x $> ())
   where
     aName = show (typeRep $ Proxy @a)
 

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

@@ -17,6 +17,7 @@ spec = describe "Conway conformance tests" $ do
   xprop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway
   prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway
   prop "CERT" $ conformsToImpl @"CERT" @ConwayFn @Conway
+
   xprop "RATIFY" $ conformsToImpl @"RATIFY" @ConwayFn @Conway
   prop "GOVCERT" $ conformsToImpl @"GOVCERT" @ConwayFn @Conway
   xprop "ENACT" $ conformsToImpl @"ENACT" @ConwayFn @Conway

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

@@ -63,6 +63,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/Classes.hs

@@ -744,8 +744,8 @@ data ProposedPPUpdatesF era where
 unProposedPPUpdates :: ProposedPPUpdatesF era -> PP.ProposedPPUpdates era
 unProposedPPUpdates (ProposedPPUpdatesF _ x) = x
 
-instance PrettyA (PParamsUpdate e) => PrettyA (ProposedPPUpdatesF e) where
-  prettyA (ProposedPPUpdatesF _p x) = ppProposedPPUpdates x
+instance PrettyA (ProposedPPUpdatesF e) where
+  prettyA (ProposedPPUpdatesF p x) = ppProposedPPUpdates p x
 
 proposedCoreL ::
   Lens' (PP.ProposedPPUpdates era) (Map (KeyHash 'Genesis (EraCrypto era)) (PParamsUpdate era))

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
       ]