WIP

cabal.project

@@ -13,8 +13,8 @@ repository cardano-haskell-packages
 source-repository-package
   type: git
   location: https://github.com/input-output-hk/cardano-ledger-executable-spec.git
-  tag: 324fafa887b7b6b38e15d2b505c4eec5a3247176
-  --sha256: sha256-zpQToGA04NQ3TfkeWBJXIzisvoGLfYdWNbVQ/2BfeEI=
+  tag: 9233cb9f0e15dcdb5ef7ba49a21ee3820ee9aa76
+  --sha256: sha256-ea99nQ/j62FJkVdACKffVgLZ5mR1ZKwakSlNcSi5fJA=
 
 index-state:
   -- Bump this if you need newer packages from Hackage

eras/shelley/impl/testlib/Test/Cardano/Ledger/Shelley/ImpTest.hs

@@ -580,6 +580,17 @@ newtype ImpTestM era a = ImpTestM {unImpTestM :: ReaderT (ImpTestEnv era) (GenT
     , MonadReader (ImpTestEnv era)
     )
 
+instance
+  ( Testable a
+  , ShelleyEraImp era
+  ) =>
+  Testable (ImpTestM era a)
+  where
+  property m = property . fmap ioProperty . runGenT $ do
+    st <- liftIO mkImpState
+    res <- liftGen $ runImpTestGenM st m
+    liftIO $ fst <$> res
+
 instance MonadWriter [SomeSTSEvent era] (ImpTestM era) where
   writer (x, evs) = (impEventsL %= (<> evs)) $> x
   listen act = do
@@ -1102,26 +1113,21 @@ logEntry e = impLogL %= (<> pretty loc <> "\t" <> pretty e <> line)
 logToExpr :: (HasCallStack, ToExpr a) => a -> ImpTestM era ()
 logToExpr e = logEntry (showExpr e)
 
-withImpState ::
-  forall era.
-  ShelleyEraImp era =>
-  SpecWith (ImpTestState era) ->
-  Spec
-withImpState =
-  beforeAll $
-    execStateT addRootTxOut $
-      ImpTestState
-        { impNES = initImpNES
-        , impRootTxIn = rootTxIn
-        , impKeyPairs = mempty
-        , impByronKeyPairs = mempty
-        , impNativeScripts = mempty
-        , impLastTick = 0
-        , impGlobals = testGlobals
-        , impLog = mempty
-        , impGen = qcGen
-        , impEvents = mempty
-        }
+mkImpState :: ShelleyEraImp era => IO (ImpTestState era)
+mkImpState =
+  execStateT addRootTxOut $
+    ImpTestState
+      { impNES = initImpNES
+      , impRootTxIn = rootTxIn
+      , impKeyPairs = mempty
+      , impByronKeyPairs = mempty
+      , impNativeScripts = mempty
+      , impLastTick = 0
+      , impGlobals = testGlobals
+      , impLog = mempty
+      , impGen = qcGen
+      , impEvents = mempty
+      }
   where
     rootCoin = Coin 1_000_000_000
     rootTxIn = TxIn (mkTxId 0) minBound
@@ -1133,6 +1139,13 @@ withImpState =
       impNESL . nesEsL . esLStateL . lsUTxOStateL . utxosUtxoL
         %= (<> UTxO (Map.singleton rootTxIn rootTxOut))
 
+withImpState ::
+  forall era.
+  ShelleyEraImp era =>
+  SpecWith (ImpTestState era) ->
+  Spec
+withImpState = beforeAll mkImpState
+
 -- | Creates a fresh @SafeHash@
 freshSafeHash :: Era era => ImpTestM era (SafeHash (EraCrypto era) a)
 freshSafeHash = arbitrary

libs/cardano-data/testlib/Test/Cardano/Data/TreeDiff.hs

@@ -5,12 +5,14 @@
 
 module Test.Cardano.Data.TreeDiff where
 
+import Data.Foldable (Foldable (..))
 import Data.Foldable qualified as F
 import Data.OMap.Strict
 import Data.OSet.Strict
-import Test.Cardano.Ledger.Binary.TreeDiff (ToExpr (..))
+import Test.Cardano.Ledger.Binary.TreeDiff (Expr (..), ToExpr (..))
 
-deriving instance ToExpr a => ToExpr (OSet a)
+instance ToExpr a => ToExpr (OSet a) where
+  toExpr x = App "OSet.fromList" [toExpr $ toList x]
 
 instance (HasOKey k v, ToExpr v) => ToExpr (OMap k v) where
   listToExpr = listToExpr . F.toList

libs/cardano-ledger-conformance/cardano-ledger-conformance.cabal

@@ -41,6 +41,7 @@ library
         base >=4.14 && <5,
         cardano-data,
         cardano-strict-containers,
+        data-default-class,
         microlens,
         mtl,
         cardano-ledger-binary,

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

@@ -15,17 +15,20 @@
 
 module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway () where
 
-import Cardano.Ledger.BaseTypes (Inject (..))
+import Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe (..))
 import Cardano.Ledger.Conway (Conway)
-import Cardano.Ledger.Conway.Core (Era (..), EraPParams)
-import Cardano.Ledger.Conway.Governance (EnactState)
+import Cardano.Ledger.Conway.Core (Era (..), EraPParams, PParamsUpdate)
+import Cardano.Ledger.Conway.Governance (EnactState, GovProcedures, ProposalProcedure, Proposals)
+import Cardano.Ledger.Conway.PParams (THKD (..))
 import Cardano.Ledger.Conway.Rules (ConwayGovPredFailure)
 import Cardano.Ledger.Conway.Tx (AlonzoTx)
+import Cardano.Ledger.TxIn (TxId)
 import Constrained
 import Control.DeepSeq (NFData)
 import Data.Bifunctor (Bifunctor (..))
 import qualified Data.List.NonEmpty as NE
 import qualified Data.Text as T
+import Data.Typeable (Typeable)
 import GHC.Generics (Generic)
 import qualified Lib as Agda
 import Test.Cardano.Ledger.Conformance (
@@ -34,7 +37,6 @@ import Test.Cardano.Ledger.Conformance (
   computationResultToEither,
  )
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (
-  GovProceduresSpecTransCtx,
   OpaqueErrorString (..),
  )
 import Test.Cardano.Ledger.Constrained.Conway (
@@ -49,8 +51,8 @@ import Test.Cardano.Ledger.Constrained.Conway (
 
 data ConwayGovExecContext era
   = ConwayGovExecContext
-      (GovProceduresSpecTransCtx (EraCrypto era))
       (EnactState era)
+      (TxId (EraCrypto era))
   deriving (Generic)
 
 deriving instance EraPParams era => Eq (ConwayGovExecContext era)
@@ -66,12 +68,124 @@ instance
   ) =>
   HasSpec fn (ConwayGovExecContext era)
 
-instance c ~ EraCrypto era => Inject (ConwayGovExecContext era) (GovProceduresSpecTransCtx c) where
+instance Inject (ConwayGovExecContext era) (EnactState era) where
   inject (ConwayGovExecContext x _) = x
 
-instance Inject (ConwayGovExecContext era) (EnactState era) where
+instance EraCrypto era ~ c => Inject (ConwayGovExecContext era) (TxId c) where
   inject (ConwayGovExecContext _ 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)
+
+agdaCompatibleProposal ::
+  IsConwayUniv fn =>
+  Term fn (ProposalProcedure Conway) ->
+  Pred fn
+agdaCompatibleProposal prop =
+  match prop $ \_ _ govAction _ ->
+    caseOn
+      govAction
+      (branch $ \_ ppup _ -> agdaCompatiblePPU ppup)
+      (branch $ \_ _ -> True)
+      (branch $ \_ _ -> True)
+      (branch $ const True)
+      (branch $ \_ _ _ _ -> True)
+      (branch $ \_ _ -> True)
+      (branch $ const True)
+
 instance
   ( NFData (SpecRep (ConwayGovPredFailure Conway))
   , IsConwayUniv fn
@@ -82,9 +196,20 @@ instance
 
   environmentSpec = govEnvSpec
 
-  stateSpec = govProposalsSpec
+  stateSpec env = govProposalsSpec env -- <> constrained agdaConstraints
+    where
+      agdaConstraints :: Term fn (Proposals Conway) -> Pred fn
+      agdaConstraints props = match @fn props $ \ppups _ _ _ _ ->
+        match ppups $ \_ ppupForest ->
+          forAll ppupForest $ \ppupTree ->
+            forAll' ppupTree $ \gas _ ->
+              match gas $ \_ _ _ _ prop _ _ -> agdaCompatibleProposal prop
 
-  signalSpec = govProceduresSpec
+  signalSpec env st = govProceduresSpec env st <> constrained agdaConstraints
+    where
+      agdaConstraints :: Term fn (GovProcedures Conway) -> Pred fn
+      agdaConstraints procs = match @fn procs $ \_ props ->
+        forAll props agdaCompatibleProposal
 
   execContextSpec = TrueSpec
 
@@ -127,15 +252,14 @@ instance
            _ctbCurrentTreasuryValue
            _ctbTreasuryDonation ->
               match ctbOutputs $
-                \outs -> forAll outs $
-                  \x -> match x $
-                    \txOut _ -> match txOut $
-                      \_ _ dat _ ->
-                        caseOn
-                          dat
-                          (branch $ const True)
-                          (branch $ const True)
-                          (branch $ const False)
+                \outs -> forAll' outs $
+                  \txOut _ -> match txOut $
+                    \_ _ dat _ ->
+                      caseOn
+                        dat
+                        (branch $ const True)
+                        (branch $ const True)
+                        (branch $ const False)
 
   runAgdaRule env st sig =
     first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])