Merge pull request #4665 from IntersectMBO/jj/utxo-proposals

Remove the proposals workaround from UTXO conformance, add LEDGER conformance

Resolves #4672

cabal.project

@@ -24,8 +24,8 @@ source-repository-package
   -- !WARNING!:
   -- MAKE SURE THIS POINTS TO A COMMIT IN `MAlonzo-code` BEFORE MERGE!
   subdir: generated
-  tag: 544ab20985e3374a1d672354e25d8ca0ca89e7e4
-  --sha256: sha256-bhh09OZkHazXCPjsiU/50Hrmfg52i+6UORTZ6/bAx6c=
+  tag: 50a653f7a74791833268b648500c3677a84e7ea1
+  --sha256: sha256-jkFo6nIMXLbNcrqSfbhdoemnmGZMVZOt3YQ5Mag8YlM=
 -- 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

eras/conway/impl/src/Cardano/Ledger/Conway/Governance/Proposals.hs

@@ -332,7 +332,7 @@ mkProposals pgais omap = do
 --
 -- WARNING: Should only be used for testing!
 unsafeMkProposals ::
-  HasCallStack =>
+  (HasCallStack, EraPParams era) =>
   GovRelation StrictMaybe era ->
   OMap.OMap (GovActionId (EraCrypto era)) (GovActionState era) ->
   Proposals era
@@ -342,7 +342,15 @@ unsafeMkProposals pgais omap = F.foldl' unsafeProposalsAddAction initialProposal
     unsafeProposalsAddAction ps gas =
       case runProposalsAddAction gas ps of
         Just p -> p
-        Nothing -> error $ "unsafeMkProposals: runProposalsAddAction failed for " ++ show (gas ^. gasIdL)
+        Nothing ->
+          error $
+            unlines
+              [ "unsafeMkProposals: runProposalsAddAction failed for " ++ show (gas ^. gasIdL)
+              , "Proposals:"
+              , show ps
+              , "GovActionState:"
+              , show gas
+              ]
 
 instance EraPParams era => EncCBOR (Proposals era) where
   encCBOR ps =

eras/shelley/impl/CHANGELOG.md

@@ -1,8 +1,13 @@
 # Version history for `cardano-ledger-shelley`
 
-## 1.14.1.1
+## 1.14.2.0
 
-*
+* Added `EncCBOR` instance for `LedgerEnv`
+
+### `testlib`
+
+* Added `ToExpr` instance for `LedgerEnv`
+* Added `tryRunImpRuleNoAssertions` to `ImpTest`
 
 ## 1.14.1.0
 

eras/shelley/impl/cardano-ledger-shelley.cabal

@@ -1,6 +1,6 @@
 cabal-version:      3.0
 name:               cardano-ledger-shelley
-version:            1.14.1.0
+version:            1.14.2.0
 license:            Apache-2.0
 maintainer:         operations@iohk.io
 author:             IOHK

eras/shelley/impl/src/Cardano/Ledger/Shelley/AdaPots.hs

@@ -153,7 +153,8 @@ consumedTxBody ::
   Consumed
 consumedTxBody txBody pp dpstate utxo =
   Consumed
-    { conInputs = coinBalance (txInsFilter utxo (txBody ^. inputsTxBodyL))
+    { conInputs =
+        coinBalance (txInsFilter utxo (txBody ^. inputsTxBodyL))
     , conRefunds = certsTotalRefundsTxBody pp dpstate txBody
     , conWithdrawals = fold . unWithdrawals $ txBody ^. withdrawalsTxBodyL
     }

eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledger.hs

@@ -7,6 +7,7 @@
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
 {-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE RecordWildCards #-}
 {-# LANGUAGE ScopedTypeVariables #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE TypeApplications #-}
@@ -35,6 +36,7 @@ import Cardano.Ledger.Binary (
   decodeRecordSum,
   encodeListLen,
  )
+import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>))
 import Cardano.Ledger.Keys (DSignable, Hash)
 import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody)
 import Cardano.Ledger.Shelley.Core
@@ -98,6 +100,17 @@ deriving instance Eq (PParams era) => Eq (LedgerEnv era)
 instance NFData (PParams era) => NFData (LedgerEnv era) where
   rnf (LedgerEnv _slotNo _ix pp _account _mempool) = rnf pp
 
+instance EraPParams era => EncCBOR (LedgerEnv era) where
+  encCBOR env@(LedgerEnv _ _ _ _ _) =
+    let LedgerEnv {..} = env
+     in encode $
+          Rec LedgerEnv
+            !> To ledgerSlotNo
+            !> To ledgerIx
+            !> To ledgerPp
+            !> To ledgerAccount
+            !> To ledgerMempool
+
 data ShelleyLedgerPredFailure era
   = UtxowFailure (PredicateFailure (EraRule "UTXOW" era)) -- Subtransition Failures
   | DelegsFailure (PredicateFailure (EraRule "DELEGS" era)) -- Subtransition Failures

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

@@ -73,6 +73,7 @@ module Test.Cardano.Ledger.Shelley.ImpTest (
   impLogToExpr,
   runImpRule,
   tryRunImpRule,
+  tryRunImpRuleNoAssertions,
   delegateStake,
   registerRewardAccount,
   registerStakeCredential,
@@ -1295,14 +1296,43 @@ tryRunImpRule ::
         (NonEmpty (PredicateFailure (EraRule rule era)))
         (State (EraRule rule era), [Event (EraRule rule era)])
     )
-tryRunImpRule stsEnv stsState stsSignal = do
+tryRunImpRule = tryRunImpRule' @rule AssertionsAll
+
+tryRunImpRuleNoAssertions ::
+  forall rule era.
+  (STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase) =>
+  Environment (EraRule rule era) ->
+  State (EraRule rule era) ->
+  Signal (EraRule rule era) ->
+  ImpTestM
+    era
+    ( Either
+        (NonEmpty (PredicateFailure (EraRule rule era)))
+        (State (EraRule rule era), [Event (EraRule rule era)])
+    )
+tryRunImpRuleNoAssertions = tryRunImpRule' @rule AssertionsOff
+
+tryRunImpRule' ::
+  forall rule era.
+  (STS (EraRule rule era), BaseM (EraRule rule era) ~ ShelleyBase) =>
+  AssertionPolicy ->
+  Environment (EraRule rule era) ->
+  State (EraRule rule era) ->
+  Signal (EraRule rule era) ->
+  ImpTestM
+    era
+    ( Either
+        (NonEmpty (PredicateFailure (EraRule rule era)))
+        (State (EraRule rule era), [Event (EraRule rule era)])
+    )
+tryRunImpRule' assertionPolicy stsEnv stsState stsSignal = do
   let trc = TRC (stsEnv, stsState, stsSignal)
   let
     stsOpts =
       ApplySTSOpts
         { asoValidation = ValidateAll
         , asoEvents = EPReturn
-        , asoAssertions = AssertionsAll
+        , asoAssertions = assertionPolicy
         }
   runShelleyBase (applySTSOptsEither @(EraRule rule era) stsOpts trc)
 

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

@@ -269,3 +269,5 @@ instance ToExpr (ShelleyMirEvent era)
 instance ToExpr (RupdEvent era)
 
 instance ToExpr (PParamsHKD Identity era) => ToExpr (UtxoEnv era)
+
+instance ToExpr (PParamsHKD Identity era) => ToExpr (LedgerEnv era)

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

@@ -36,12 +36,18 @@ library
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Certs
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Gov
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert
+        Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo
+        Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxow
+        Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Ledger
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert
+        Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo
+        Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow
+        Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger
         Test.Cardano.Ledger.Conformance.Orphans
         Test.Cardano.Ledger.Conformance.Utils
 

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

@@ -16,4 +16,7 @@ import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Certs as X (nameCerts
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg as X (nameDelegCert)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov as X ()
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert as X (nameGovCert)
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger as X ()
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool as X (namePoolCert)
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo as X ()
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxow as X ()

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

@@ -4,7 +4,6 @@
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE GADTs #-}
-{-# LANGUAGE InstanceSigs #-}
 {-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE NamedFieldPuns #-}
@@ -28,13 +27,13 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (
   nameGovAction,
   crecTreasuryL,
   crecGovActionMapL,
+  enactStateSpec,
 ) where
 
 import Cardano.Ledger.BaseTypes (
   EpochInterval (..),
   EpochNo (..),
   Inject (..),
-  ProtVer (..),
   StrictMaybe (..),
   addEpochInterval,
   natVersion,
@@ -47,7 +46,7 @@ import Cardano.Ledger.CertState (
  )
 import Cardano.Ledger.Coin (Coin (..), CompactForm (..))
 import Cardano.Ledger.Conway (Conway)
-import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParams, ppMaxTxSizeL, sizeTxF)
+import Cardano.Ledger.Conway.Core (Era (..), EraPParams (..), PParams)
 import Cardano.Ledger.Conway.Governance (
   Committee (..),
   EnactState (..),
@@ -78,26 +77,21 @@ import Cardano.Ledger.PoolDistr (IndividualPoolStake (..))
 import Constrained hiding (inject)
 import Data.Bifunctor (Bifunctor (..))
 import Data.Foldable (Foldable (..))
-import qualified Data.List.NonEmpty as NE
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.Ratio (denominator, numerator, (%))
 import qualified Data.Sequence.Strict as SSeq
 import qualified Data.Set as Set
-import qualified Data.Text as T
 import GHC.Generics (Generic)
-import Lens.Micro (Lens', lens, (&), (.~), (^.))
+import Lens.Micro (Lens', lens, (^.))
 import qualified Lib as Agda
 import qualified Prettyprinter as PP
 import Test.Cardano.Ledger.Binary.TreeDiff (tableDoc)
 import Test.Cardano.Ledger.Common (Arbitrary (..))
 import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
-  OpaqueErrorString (..),
   SpecTranslate (..),
-  checkConformance,
   computationResultToEither,
-  runConformance,
   runSpecTransM,
  )
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (defaultTestConformance)
@@ -107,18 +101,13 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (
   DepositPurpose,
  )
 import Test.Cardano.Ledger.Constrained.Conway (
-  ConwayFn,
   EpochExecEnv,
   IsConwayUniv,
-  UtxoExecContext (..),
   coerce_,
   epochEnvSpec,
   epochSignalSpec,
   epochStateSpec,
   newEpochStateSpec,
-  utxoEnvSpec,
-  utxoStateSpec,
-  utxoTxSpec,
  )
 import Test.Cardano.Ledger.Constrained.Conway.SimplePParams (
   committeeMaxTermLength_,
@@ -127,93 +116,9 @@ import Test.Cardano.Ledger.Constrained.Conway.SimplePParams (
  )
 
 import Cardano.Ledger.Address (RewardAccount)
-import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
-import Cardano.Ledger.Shelley.Rules (UtxoEnv (..))
 import Test.Cardano.Ledger.Conway.Arbitrary ()
-import Test.Cardano.Ledger.Conway.ImpTest (logDoc, showConwayTxBalance)
-import Test.Cardano.Ledger.Generic.GenState (
-  GenEnv (..),
-  GenState (..),
-  invalidScriptFreq,
-  runGenRS,
- )
-import qualified Test.Cardano.Ledger.Generic.GenState as GenSize
-import qualified Test.Cardano.Ledger.Generic.PrettyCore as PP
-import qualified Test.Cardano.Ledger.Generic.Proof as Proof
-import Test.Cardano.Ledger.Generic.TxGen (genAlonzoTx)
 import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)
 
-instance
-  forall fn.
-  IsConwayUniv fn =>
-  ExecSpecRule fn "UTXO" Conway
-  where
-  type ExecContext fn "UTXO" Conway = UtxoExecContext Conway
-
-  genExecContext = do
-    let proof = Proof.reify @Conway
-    ueSlot <- arbitrary
-    let
-      genSize =
-        GenSize.small
-          { invalidScriptFreq = 0 -- TODO make the test work with invalid scripts
-          }
-    ((uecUTxO, uecTx), gs) <-
-      runGenRS proof genSize $
-        genAlonzoTx proof ueSlot
-    ueCertState <- arbitrary
-    let txSize = uecTx ^. sizeTxF
-    let
-      uePParams =
-        gePParams (gsGenEnv gs)
-          & ppMaxTxSizeL .~ fromIntegral txSize
-          & ppProtocolVersionL .~ ProtVer (natVersion @10) 0
-      uecUtxoEnv = UtxoEnv {..}
-    pure UtxoExecContext {..}
-
-  environmentSpec = utxoEnvSpec
-
-  stateSpec = utxoStateSpec
-
-  signalSpec ctx _ _ = utxoTxSpec ctx
-
-  runAgdaRule env st sig =
-    first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
-      . computationResultToEither
-      $ Agda.utxoStep env st sig
-
-  extraInfo ctx env@UtxoEnv {..} st@UTxOState {..} sig =
-    "Impl:\n"
-      <> PP.ppString (showConwayTxBalance uePParams ueCertState utxosUtxo sig)
-      <> "\n\nSpec:\n"
-      <> PP.ppString
-        ( either show T.unpack . runSpecTransM ctx $
-            Agda.utxoDebug
-              <$> toSpecRep env
-              <*> toSpecRep st
-              <*> toSpecRep sig
-        )
-
-  testConformance ctx env st sig = property $ do
-    (implResTest, agdaResTest) <- runConformance @"UTXO" @ConwayFn @Conway ctx env st sig
-    let extra = extraInfo @ConwayFn @"UTXO" @Conway ctx (inject env) (inject st) (inject sig)
-    logDoc extra
-    let
-      -- TODO make the deposit map updates match up exactly between the spec and
-      -- the implmentation
-      eraseDeposits Agda.MkUTxOState {..} =
-        Agda.MkUTxOState {deposits = Agda.MkHSMap mempty, ..}
-    checkConformance
-      @"UTXO"
-      @Conway
-      @ConwayFn
-      ctx
-      (inject env)
-      (inject st)
-      (inject sig)
-      (second eraseDeposits implResTest)
-      (second eraseDeposits agdaResTest)
-
 data ConwayCertExecContext era = ConwayCertExecContext
   { ccecWithdrawals :: !(Map (RewardAccount (EraCrypto era)) Coin)
   , ccecDeposits :: !(Map (DepositPurpose (EraCrypto era)) Coin)
@@ -663,10 +568,7 @@ nameGovAction UpdateCommittee {} = "UpdateCommittee"
 nameGovAction NewConstitution {} = "NewConstitution"
 nameGovAction InfoAction {} = "InfoAction"
 
-instance
-  IsConwayUniv fn =>
-  ExecSpecRule fn "EPOCH" Conway
-  where
+instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" Conway where
   type ExecContext fn "EPOCH" Conway = [GovActionState Conway]
   type ExecEnvironment fn "EPOCH" Conway = EpochExecEnv Conway
 
@@ -686,10 +588,7 @@ instance
 nameEpoch :: EpochNo -> String
 nameEpoch x = show x
 
-instance
-  IsConwayUniv fn =>
-  ExecSpecRule fn "NEWEPOCH" Conway
-  where
+instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" Conway where
   type ExecContext fn "NEWEPOCH" Conway = [GovActionState Conway]
   type ExecEnvironment fn "NEWEPOCH" Conway = EpochExecEnv Conway