Merge pull request #4565 from IntersectMBO/jj/enact-conformance

ENACT conformance

cabal.project

@@ -21,11 +21,11 @@ repository cardano-haskell-packages
 source-repository-package
   type: git
   location: https://github.com/IntersectMBO/formal-ledger-specifications.git
-  subdir: generated
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
-  tag: b5a8d47aebbdad92773be96c459f241d773d4771
-  --sha256: sha256-iEqucpja/0/5Tvnjr2drFlz58f3x3kUpInVjZfcePBQ=
+  subdir: generated
+  tag: d14f4b3f8f33a73890806dd1680069c7cfa8e54f
+  --sha256: sha256-OLJKEJ0u1v1Zah8qZ2nQD+ILsvG4BDoojWs+lKOcsIs=
 -- NOTE: If you would like to update the above, look for the `MAlonzo-code`
 -- branch in the `formal-ledger-specifications` repo and copy the SHA of
 -- the commit you need. The `MAlonzo-code` branch functions like an alternative

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

@@ -30,10 +30,12 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
 ) where
 
 import Cardano.Ledger.BaseTypes (
+  EpochInterval (..),
   EpochNo (..),
   Inject (..),
   Network,
   StrictMaybe (..),
+  addEpochInterval,
   natVersion,
  )
 import Cardano.Ledger.Binary (DecCBOR (decCBOR), EncCBOR (encCBOR))
@@ -95,7 +97,7 @@ import Test.Cardano.Ledger.Conformance (
  )
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (defaultTestConformance)
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway ()
-import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (ConwayExecEnactEnv)
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (ConwayExecEnactEnv (..))
 import Test.Cardano.Ledger.Constrained.Conway (
   EpochExecEnv,
   IsConwayUniv,
@@ -491,16 +493,72 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where
               . label (spoBucket x)
         | otherwise = id
 
+newtype ConwayEnactExecContext era = ConwayEnactExecContext
+  { ceecMaxTerm :: EpochInterval
+  }
+  deriving (Generic)
+
+instance Arbitrary (ConwayEnactExecContext era) where
+  arbitrary = ConwayEnactExecContext <$> arbitrary
+
+instance NFData (ConwayEnactExecContext era)
+
+instance ToExpr (ConwayEnactExecContext era)
+
+instance Era era => EncCBOR (ConwayEnactExecContext era) where
+  encCBOR (ConwayEnactExecContext x) = encCBOR x
+
+enactSignalSpec ::
+  IsConwayUniv fn =>
+  ConwayEnactExecContext Conway ->
+  ConwayExecEnactEnv Conway ->
+  EnactState Conway ->
+  Specification fn (EnactSignal Conway)
+enactSignalSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} EnactState {..} =
+  constrained' $ \gid action ->
+    [ assert $ gid ==. lit ceeeGid
+    , -- TODO get rid of this by modifying the spec so that ENACT can't fail.
+      -- Right now this constraint makes the generator avoid cases where
+      -- the spec would fail, because such proposals would be handled in RATIFY
+      -- and wouldn't make it to ENACT.
+      (caseOn action)
+        (branch $ \_ _ _ -> True)
+        (branch $ \_ _ -> True)
+        ( branch $ \newWdrls _ ->
+            sum_ (rng_ newWdrls) + lit (sum ensWithdrawals) <=. lit ceeeTreasury
+        )
+        (branch $ \_ -> True)
+        ( branch $ \_ _ newMembers _ ->
+            let maxTerm = addEpochInterval ceeeEpoch ceecMaxTerm
+             in forAll (rng_ newMembers) (<=. lit maxTerm)
+        )
+        (branch $ \_ _ -> True)
+        (branch $ \_ -> True)
+    ]
+
+enactStateSpec ::
+  IsConwayUniv fn =>
+  ConwayEnactExecContext Conway ->
+  ConwayExecEnactEnv Conway ->
+  Specification fn (EnactState Conway)
+enactStateSpec ConwayEnactExecContext {..} ConwayExecEnactEnv {..} =
+  constrained' $ \_ _ curPParams _ treasury wdrls _ ->
+    [ match curPParams $ \pp -> match (sel @25 pp) (==. lit ceecMaxTerm)
+    , assert $ sum_ (rng_ wdrls) <=. treasury
+    , assert $ treasury ==. lit ceeeTreasury
+    ]
+
 instance IsConwayUniv fn => ExecSpecRule fn "ENACT" Conway where
+  type ExecContext fn "ENACT" Conway = ConwayEnactExecContext Conway
   type ExecEnvironment fn "ENACT" Conway = ConwayExecEnactEnv Conway
   type ExecState fn "ENACT" Conway = EnactState Conway
   type ExecSignal fn "ENACT" Conway = EnactSignal Conway
 
   environmentSpec _ = TrueSpec
-  stateSpec _ _ = TrueSpec
-  signalSpec _ _ _ = TrueSpec
+  stateSpec = enactStateSpec
+  signalSpec = enactSignalSpec
   runAgdaRule env st sig =
-    first (error "ENACT failed")
+    first (\e -> error $ "ENACT failed with:\n" <> show e)
       . computationResultToEither
       $ Agda.enactStep env st sig
 

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

@@ -16,6 +16,7 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (
   ExecSpecRule (..),
   conformsToImpl,
   generatesWithin,
+  inputsGenerateWithin,
   runConformance,
   checkConformance,
   defaultTestConformance,
@@ -431,8 +432,34 @@ generatesWithin ::
   Int ->
   Spec
 generatesWithin gen timeout =
-  prop (aName <> " generates in reasonable time")
+  prop (aName <> " generates within " <> show timeout <> "μs")
     . forAllShow gen showExpr
     $ \x -> within timeout $ ioProperty (evaluateDeep x $> ())
   where
     aName = show (typeRep $ Proxy @a)
+
+inputsGenerateWithin ::
+  forall (fn :: [Type] -> Type -> Type) (rule :: Symbol) era.
+  ExecSpecRule fn rule era =>
+  Int ->
+  Spec
+inputsGenerateWithin timeout =
+  describe (aName <> " input generation time") $ do
+    let
+      genEnv = do
+        ctx <- genExecContext @fn @rule @era
+        CV2.genFromSpec $ environmentSpec @fn @rule @era ctx
+      genSt = do
+        ctx <- genExecContext @fn @rule @era
+        env <- genEnv
+        CV2.genFromSpec $ stateSpec @fn @rule @era ctx env
+      genSig = do
+        ctx <- genExecContext @fn @rule @era
+        env <- genEnv
+        st <- genSt
+        CV2.genFromSpec $ signalSpec @fn @rule @era ctx env st
+    genEnv `generatesWithin` timeout
+    genSt `generatesWithin` timeout
+    genSig `generatesWithin` timeout
+  where
+    aName = show (typeRep $ Proxy @rule)

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

@@ -298,8 +298,11 @@ instance SpecTranslate ctx (ConwayPParams Identity era) where
     ppPoolDeposit <- toSpecRep cppPoolDeposit
     ppEmax <- toSpecRep cppEMax
     ppNopt <- toSpecRep (toInteger $ unTHKD cppNOpt)
-    ppPv <- toSpecRep cppProtocolVersion
     let
+      -- We don't really care about `ppPv` in conformance testing, because
+      -- the actual protocol version is stored elsewhere starting from Conway
+      -- and this is just here for backwards compatibility
+      ppPv = (0, 0)
       ppMinUTxOValue = 0 -- minUTxOValue has been deprecated and is not supported in Conway
     ppCoinsPerUTxOByte <- toSpecRep cppCoinsPerUTxOByte
     ppCostmdls <- toSpecRep cppCostModels
@@ -1037,9 +1040,9 @@ instance SpecTranslate ctx (EpochExecEnv era) where
 
 -- | This type is used as the Env only in the Agda Spec
 data ConwayExecEnactEnv era = ConwayExecEnactEnv
-  { ceeeGid :: GovActionId (EraCrypto era)
-  , ceeeTreasury :: Coin
-  , ceeeEpoch :: EpochNo
+  { ceeeGid :: !(GovActionId (EraCrypto era))
+  , ceeeTreasury :: !Coin
+  , ceeeEpoch :: !EpochNo
   }
   deriving (Generic, Eq, Show)
 

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

@@ -5,8 +5,7 @@
 module Test.Cardano.Ledger.Conformance.Spec.Conway (spec) where
 
 import Cardano.Ledger.Conway (Conway)
-import qualified Constrained as CV2
-import Test.Cardano.Ledger.Conformance (ExecSpecRule (..), conformsToImpl, generatesWithin)
+import Test.Cardano.Ledger.Conformance (conformsToImpl, inputsGenerateWithin)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway ()
 import qualified Test.Cardano.Ledger.Conformance.ExecSpecRule.MiniTrace as MiniTrace
 import qualified Test.Cardano.Ledger.Conformance.Imp.Ratify as RatifyImp
@@ -18,25 +17,11 @@ spec :: Spec
 spec = do
   describe "MiniTrace" MiniTrace.spec
   describe "Generators" $ do
-    let
-      genEnv = do
-        ctx <- genExecContext @ConwayFn @"GOV" @Conway
-        CV2.genFromSpec $ environmentSpec @ConwayFn @"GOV" @Conway ctx
-      genSt = do
-        ctx <- genExecContext @ConwayFn @"GOV" @Conway
-        env <- genEnv
-        CV2.genFromSpec $ stateSpec @ConwayFn @"GOV" @Conway ctx env
-      genSig = do
-        ctx <- genExecContext @ConwayFn @"GOV" @Conway
-        env <- genEnv
-        st <- genSt
-        CV2.genFromSpec $ signalSpec @ConwayFn @"GOV" @Conway ctx env st
-    genEnv `generatesWithin` 3_000_000
-    genSt `generatesWithin` 40_000_000
-    genSig `generatesWithin` 60_000_000
+    inputsGenerateWithin @ConwayFn @"GOV" @Conway 60_000_000
+    inputsGenerateWithin @ConwayFn @"ENACT" @Conway 60_000_000
   describe "Conformance" $ do
     describe "Ticks transition graph" $ do
-      xprop "ENACT" $ conformsToImpl @"ENACT" @ConwayFn @Conway
+      prop "ENACT" $ conformsToImpl @"ENACT" @ConwayFn @Conway
       prop "RATIFY" $ conformsToImpl @"RATIFY" @ConwayFn @Conway
       xprop "EPOCH" $ conformsToImpl @"EPOCH" @ConwayFn @Conway
       xprop "NEWEPOCH" $ conformsToImpl @"NEWEPOCH" @ConwayFn @Conway
@@ -46,7 +31,7 @@ spec = do
       prop "POOL" $ conformsToImpl @"POOL" @ConwayFn @Conway
       xprop "CERTS" $ conformsToImpl @"CERTS" @ConwayFn @Conway
       prop "CERT" $ conformsToImpl @"CERT" @ConwayFn @Conway
-      prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway
+      xprop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway
       xprop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway
     describe "ImpTests" $ do
       RatifyImp.spec

libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Instances.hs

@@ -234,7 +234,7 @@ instance Crypto c => HasSimpleRep (ConwayTxBody (ConwayEra c)) where
 instance HasSimpleRep Coin where
   type SimpleRep Coin = Word64
   toSimpleRep (Coin i) = case integerToWord64 i of
-    Nothing -> error "The impossible happened in toSimpleRep for `Coin`"
+    Nothing -> error $ "Failed to convert Integer to Word64:\n" <> show i
     Just w -> w
   fromSimpleRep = word64ToCoin
 instance IsConwayUniv fn => HasSpec fn Coin