Conformance: UTxO plumbing and translation

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

@@ -29,13 +29,15 @@ library
         Test.Cardano.Ledger.Conformance.SpecTranslate.Core
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base
+        Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool
         Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert
         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.ExecSpecRule.Conway.Base
+        Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool
         Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Cert

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

@@ -21,3 +21,4 @@ import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Deleg (nameDelegCert)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Gov ()
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.GovCert (nameGovCert)
 import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool (namePoolCert)
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo ()

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

@@ -62,7 +62,6 @@ import Cardano.Ledger.Conway.Rules (
   spoAccepted,
   spoAcceptedRatio,
  )
-import Cardano.Ledger.Conway.Tx (AlonzoTx)
 import Cardano.Ledger.Credential (Credential (..))
 import Cardano.Ledger.DRep (DRep (..))
 import Cardano.Ledger.Keys (KeyRole (..))
@@ -71,7 +70,6 @@ import Constrained
 import Constrained.Base (fromList_)
 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 ((%))
@@ -83,7 +81,6 @@ import qualified Lib as Agda
 import Test.Cardano.Ledger.Common (Arbitrary (..))
 import Test.Cardano.Ledger.Conformance (
   ExecSpecRule (..),
-  OpaqueErrorString (..),
   SpecTranslate (..),
   computationResultToEither,
   runSpecTransM,
@@ -99,63 +96,11 @@ import Test.Cardano.Ledger.Constrained.Conway (
   epochSignalSpec,
   epochStateSpec,
   newEpochStateSpec,
-  utxoEnvSpec,
-  utxoStateSpec,
-  utxoTxSpec,
  )
 import Test.Cardano.Ledger.Constrained.Conway.Instances ()
 import Test.Cardano.Ledger.Conway.Arbitrary ()
 import Test.Cardano.Ledger.Imp.Common hiding (arbitrary, forAll, prop, var)
 
-instance
-  forall fn.
-  IsConwayUniv fn =>
-  ExecSpecRule fn "UTXO" Conway
-  where
-  environmentSpec _ = utxoEnvSpec
-
-  stateSpec _ = utxoStateSpec
-
-  signalSpec _ env st =
-    utxoTxSpec env st
-      <> constrained disableInlineDatums
-    where
-      disableInlineDatums :: Term fn (AlonzoTx Conway) -> Pred fn
-      disableInlineDatums tx = match @fn tx $ \txBody _ _ _ ->
-        match txBody $
-          \_ctbSpendInputs
-           _ctbCollateralInputs
-           _ctbReferenceInputs
-           ctbOutputs
-           _ctbCollateralReturn
-           _ctbTotalCollateral
-           _ctbCerts
-           _ctbWithdrawals
-           _ctbTxfee
-           _ctbVldt
-           _ctbReqSignerHashes
-           _ctbMint
-           _ctbScriptIntegrityHash
-           _ctbAdHash
-           _ctbTxNetworkId
-           _ctbVotingProcedures
-           _ctbProposalProcedures
-           _ctbCurrentTreasuryValue
-           _ctbTreasuryDonation ->
-              match ctbOutputs $
-                \outs -> forAll' outs $
-                  \txOut _ -> match txOut $
-                    \_ _ dat _ ->
-                      (caseOn dat)
-                        (branch $ \_ -> True)
-                        (branch $ \_ -> True)
-                        (branch $ \_ -> False)
-
-  runAgdaRule env st sig =
-    first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
-      . computationResultToEither
-      $ Agda.utxoStep env st sig
-
 data ConwayCertExecContext era = ConwayCertExecContext
   { ccecWithdrawals :: !(Map (Network, Credential 'Staking (EraCrypto era)) Coin)
   , ccecVotes :: !(VotingProcedures era)

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

@@ -0,0 +1,72 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo () where
+
+import Cardano.Ledger.Alonzo.Tx (AlonzoTx)
+import Cardano.Ledger.Conway (Conway)
+import Constrained
+import Data.Bifunctor (first)
+import qualified Data.List.NonEmpty as NE
+import qualified Data.Text as T
+import qualified Lib as Agda
+import Test.Cardano.Ledger.Conformance
+import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base ()
+import Test.Cardano.Ledger.Constrained.Conway
+import Test.Cardano.Ledger.Conway.Arbitrary ()
+
+instance
+  forall fn.
+  IsConwayUniv fn =>
+  ExecSpecRule fn "UTXO" Conway
+  where
+  environmentSpec _ = utxoEnvSpec
+
+  stateSpec _ = utxoStateSpec
+
+  signalSpec _ env st =
+    utxoTxSpec env st
+      <> constrained disableInlineDatums
+    where
+      disableInlineDatums :: Term fn (AlonzoTx Conway) -> Pred fn
+      disableInlineDatums tx = match @fn tx $ \txBody _ _ _ ->
+        match txBody $
+          \_ctbSpendInputs
+           _ctbCollateralInputs
+           _ctbReferenceInputs
+           ctbOutputs
+           _ctbCollateralReturn
+           _ctbTotalCollateral
+           _ctbCerts
+           _ctbWithdrawals
+           _ctbTxfee
+           _ctbVldt
+           _ctbReqSignerHashes
+           _ctbMint
+           _ctbScriptIntegrityHash
+           _ctbAdHash
+           _ctbTxNetworkId
+           _ctbVotingProcedures
+           _ctbProposalProcedures
+           _ctbCurrentTreasuryValue
+           _ctbTreasuryDonation ->
+              match ctbOutputs $
+                \outs -> forAll' outs $
+                  \txOut _ -> match txOut $
+                    \_ _ dat _ ->
+                      (caseOn dat)
+                        (branch $ \_ -> True)
+                        (branch $ \_ -> True)
+                        (branch $ \_ -> False)
+
+  runAgdaRule env st sig =
+    first (\e -> OpaqueErrorString (T.unpack e) NE.:| [])
+      . computationResultToEither
+      $ Agda.utxoStep env st sig

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

@@ -62,8 +62,6 @@ import Cardano.Ledger.Plutus.Data (BinaryData, Data, Datum (..), hashBinaryData)
 import Cardano.Ledger.PoolDistr (IndividualPoolStake (..), PoolDistr (..))
 import Cardano.Ledger.PoolParams (PoolParams (..))
 import Cardano.Ledger.SafeHash (SafeHash, extractHash)
-import Cardano.Ledger.Shelley.LedgerState
-import Cardano.Ledger.Shelley.Rules (Identity, UtxoEnv (..))
 import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
 import Cardano.Ledger.UMap (fromCompact)
 import Cardano.Ledger.UTxO (UTxO (..))
@@ -77,6 +75,7 @@ import Data.Bitraversable (bimapM)
 import Data.Data (Typeable)
 import Data.Default.Class (Default (..))
 import Data.Foldable (Foldable (..))
+import Data.Functor.Identity (Identity)
 import Data.Map.Strict (Map)
 import qualified Data.Map.Strict as Map
 import Data.OMap.Strict (OMap, assocList)
@@ -205,19 +204,6 @@ instance
   type SpecRep (UTxO era) = SpecRep (Map (TxIn (EraCrypto era)) (TxOut era))
   toSpecRep (UTxO m) = toSpecRep m
 
-instance
-  ( SpecTranslate ctx (TxOut era)
-  , SpecRep (TxOut era) ~ Agda.TxOut
-  ) =>
-  SpecTranslate ctx (UTxOState era)
-  where
-  type SpecRep (UTxOState era) = Agda.UTxOState
-
-  toSpecRep x =
-    Agda.MkUTxOState
-      <$> toSpecRep (utxosUtxo x)
-      <*> toSpecRep (utxosFees x)
-
 deriving instance SpecTranslate ctx SlotNo
 
 deriving instance SpecTranslate ctx EpochNo
@@ -328,20 +314,6 @@ instance
 
   toSpecRep (PParams x) = toSpecRep x
 
-instance
-  ( SpecRep (PParams era) ~ Agda.PParams
-  , SpecTranslate ctx (PParamsHKD Identity era)
-  ) =>
-  SpecTranslate ctx (UtxoEnv era)
-  where
-  type SpecRep (UtxoEnv era) = Agda.UTxOEnv
-
-  toSpecRep x =
-    Agda.MkUTxOEnv
-      <$> toSpecRep (ueSlot x)
-      <*> toSpecRep (uePParams x)
-      <*> toSpecRep (Coin 10_000_000) -- TODO: Fix generating types
-
 instance SpecTranslate ctx a => SpecTranslate ctx (Set a) where
   type SpecRep (Set a) = Agda.HSSet (SpecRep a)
 

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

@@ -34,6 +34,7 @@ import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (emptyDeposits)
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Deleg ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.GovCert ()
 import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Pool ()
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo ()
 import Test.Cardano.Ledger.Conway.TreeDiff
 
 instance

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

@@ -0,0 +1,50 @@
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE NamedFieldPuns #-}
+{-# LANGUAGE NumericUnderscores #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo () where
+
+import Cardano.Ledger.Coin
+import Cardano.Ledger.Conway.Core
+import Cardano.Ledger.Shelley.LedgerState (UTxOState (..))
+import Cardano.Ledger.Shelley.Rules (UtxoEnv (..))
+import Data.Functor.Identity (Identity)
+import qualified Lib as Agda
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base ()
+import Test.Cardano.Ledger.Conformance.SpecTranslate.Core
+
+instance
+  ( SpecRep (PParams era) ~ Agda.PParams
+  , SpecTranslate ctx (PParamsHKD Identity era)
+  ) =>
+  SpecTranslate ctx (UtxoEnv era)
+  where
+  type SpecRep (UtxoEnv era) = Agda.UTxOEnv
+
+  toSpecRep x =
+    Agda.MkUTxOEnv
+      <$> toSpecRep (ueSlot x)
+      <*> toSpecRep (uePParams x)
+      <*> toSpecRep (Coin 10_000_000) -- TODO: Fix generating types
+
+instance
+  ( SpecTranslate ctx (TxOut era)
+  , SpecRep (TxOut era) ~ Agda.TxOut
+  ) =>
+  SpecTranslate ctx (UTxOState era)
+  where
+  type SpecRep (UTxOState era) = Agda.UTxOState
+
+  toSpecRep x =
+    Agda.MkUTxOState
+      <$> toSpecRep (utxosUtxo x)
+      <*> toSpecRep (utxosFees x)

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

@@ -53,6 +53,6 @@ spec = do
       xprop "CERT" $ conformsToImpl @"CERT" @ConwayFn @Conway
       xprop "CERTS" $ conformsToImpl @"CERTS" @ConwayFn @Conway
       prop "GOV" $ conformsToImpl @"GOV" @ConwayFn @Conway
-      xprop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway
+      prop "UTXO" $ conformsToImpl @"UTXO" @ConwayFn @Conway
     describe "ImpTests" $ do
       RatifyImp.spec