From 3bdb37326c7b7349e03301d81de9dbd5a7560293 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Joosep=20J=C3=A4=C3=A4ger?= Date: Tue, 10 Dec 2024 12:37:53 +0200 Subject: [PATCH] OpaqueErrorString changes --- .../Test/Cardano/Ledger/Babbage/Imp.hs | 2 +- .../Cardano/Ledger/Babbage/Imp/UtxowSpec.hs | 32 ++++++++- .../Cardano/Ledger/Shelley/Rules/Ledgers.hs | 4 ++ .../Conformance/ExecSpecRule/Conway/Base.hs | 24 ++----- .../Conformance/ExecSpecRule/Conway/Cert.hs | 8 +-- .../Conformance/ExecSpecRule/Conway/Certs.hs | 16 +++-- .../Conformance/ExecSpecRule/Conway/Deleg.hs | 9 +-- .../Conformance/ExecSpecRule/Conway/Gov.hs | 13 +--- .../ExecSpecRule/Conway/GovCert.hs | 9 +-- .../Conformance/ExecSpecRule/Conway/Ledger.hs | 31 +++++---- .../ExecSpecRule/Conway/Ledgers.hs | 11 +-- .../Conformance/ExecSpecRule/Conway/Pool.hs | 10 +-- .../Conformance/ExecSpecRule/Conway/Utxo.hs | 10 +-- .../Conformance/ExecSpecRule/Conway/Utxow.hs | 11 ++- .../Ledger/Conformance/ExecSpecRule/Core.hs | 68 ++++++++++--------- .../Cardano/Ledger/Conformance/Orphans.hs | 7 ++ .../Conformance/SpecTranslate/Conway/Base.hs | 5 +- .../Conformance/SpecTranslate/Conway/Cert.hs | 2 +- .../Conformance/SpecTranslate/Conway/Certs.hs | 2 +- .../Conformance/SpecTranslate/Conway/Deleg.hs | 3 +- .../SpecTranslate/Conway/GovCert.hs | 4 +- .../SpecTranslate/Conway/Ledger.hs | 4 +- .../SpecTranslate/Conway/Ledgers.hs | 11 ++- .../Conformance/SpecTranslate/Conway/Pool.hs | 3 +- .../Conformance/SpecTranslate/Conway/Utxo.hs | 4 +- .../Conformance/SpecTranslate/Conway/Utxow.hs | 10 ++- .../Ledger/Conformance/SpecTranslate/Core.hs | 54 ++++++++++----- .../Test/Cardano/Ledger/Conformance/Utils.hs | 5 -- .../Test/Cardano/Ledger/Conformance/Imp.hs | 11 ++- .../Cardano/Ledger/Conformance/Imp/Ratify.hs | 8 ++- .../Test/Cardano/Ledger/Generic/Functions.hs | 2 + 31 files changed, 205 insertions(+), 188 deletions(-) diff --git a/eras/babbage/impl/testlib/Test/Cardano/Ledger/Babbage/Imp.hs b/eras/babbage/impl/testlib/Test/Cardano/Ledger/Babbage/Imp.hs index 7c0a849c1fb..409fa59f4d9 100644 --- a/eras/babbage/impl/testlib/Test/Cardano/Ledger/Babbage/Imp.hs +++ b/eras/babbage/impl/testlib/Test/Cardano/Ledger/Babbage/Imp.hs @@ -27,7 +27,7 @@ spec :: forall era. ( Arbitrary (TxAuxData era) , AlonzoEraImp era - , BabbageEraTxOut era + , BabbageEraTxBody era , InjectRuleFailure "LEDGER" ShelleyUtxoPredFailure era , InjectRuleFailure "LEDGER" AlonzoUtxoPredFailure era , InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure era diff --git a/eras/babbage/impl/testlib/Test/Cardano/Ledger/Babbage/Imp/UtxowSpec.hs b/eras/babbage/impl/testlib/Test/Cardano/Ledger/Babbage/Imp/UtxowSpec.hs index 128ae869925..026d1b3afa5 100644 --- a/eras/babbage/impl/testlib/Test/Cardano/Ledger/Babbage/Imp/UtxowSpec.hs +++ b/eras/babbage/impl/testlib/Test/Cardano/Ledger/Babbage/Imp/UtxowSpec.hs @@ -1,8 +1,10 @@ {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE NumericUnderscores #-} {-# LANGUAGE OverloadedLists #-} {-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -17,7 +19,13 @@ import Cardano.Ledger.Babbage.Core import Cardano.Ledger.Babbage.Rules (BabbageUtxowPredFailure (..)) import Cardano.Ledger.Babbage.TxInfo (BabbageContextError (..)) import Cardano.Ledger.BaseTypes +import Cardano.Ledger.Coin (Coin (..)) import Cardano.Ledger.Plutus +import Cardano.Ledger.Shelley.Scripts (pattern RequireAnyOf) +import Cardano.Ledger.TxIn (mkTxInPartial) +import Data.Either (isRight) +import qualified Data.Sequence.Strict as SSeq +import qualified Data.Set as Set import Lens.Micro import Test.Cardano.Ledger.Alonzo.Arbitrary (mkPlutusScript') import Test.Cardano.Ledger.Alonzo.ImpTest @@ -27,11 +35,11 @@ import Test.Cardano.Ledger.Plutus.Examples (redeemerSameAsDatum) spec :: forall era. ( AlonzoEraImp era - , BabbageEraTxOut era , InjectRuleFailure "LEDGER" BabbageUtxowPredFailure era , InjectRuleFailure "LEDGER" AlonzoUtxosPredFailure era , InjectRuleFailure "LEDGER" AlonzoUtxowPredFailure era , Inject (BabbageContextError era) (ContextError era) + , BabbageEraTxBody era ) => SpecWith (ImpInit (LedgerSpec era)) spec = describe "UTXOW" $ do @@ -73,7 +81,8 @@ spec = describe "UTXOW" $ do & bodyTxL . inputsTxBodyL .~ [txIn] & witsTxL . rdmrsTxWitsL <>~ Redeemers [(prp, (dt, ExUnits 0 0))] let submit = - submitFailingTx tx $ + submitFailingTx + tx [ injectFailure $ ExtraRedeemers [prp] , injectFailure $ CollectErrors [BadTranslation (inject $ RedeemerPointerPointsToNothing prp)] @@ -82,3 +91,22 @@ spec = describe "UTXOW" $ do then -- PlutusPurpose serialization was fixed in Conway withCborRoundTripFailures submit else submit + + it "P1 reference scripts must be witnessed" $ do + (_, addr) <- freshKeyAddr + let + timelock = fromNativeScript @era $ RequireAnyOf [] + txOut = + mkCoinTxOut addr (inject $ Coin 15_000_000) + & referenceScriptTxOutL .~ SJust timelock + tx0 <- + submitTx $ + mkBasicTx mkBasicTxBody + & bodyTxL . outputsTxBodyL .~ SSeq.singleton txOut + let + txIn = mkTxInPartial (txIdTx tx0) 0 + tx1 = + mkBasicTx mkBasicTxBody + & bodyTxL . referenceInputsTxBodyL .~ Set.singleton txIn + res <- trySubmitTx tx1 + res `shouldSatisfyExpr` isRight diff --git a/eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledgers.hs b/eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledgers.hs index 116a83cd033..8889db8bc2a 100644 --- a/eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledgers.hs +++ b/eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledgers.hs @@ -94,6 +94,10 @@ newtype ShelleyLedgersPredFailure era = LedgerFailure (PredicateFailure (EraRule "LEDGER" era)) -- Subtransition Failures deriving (Generic) +instance + NFData (PredicateFailure (EraRule "LEDGER" era)) => + NFData (ShelleyLedgersPredFailure era) + type instance EraRuleFailure "LEDGERS" (ShelleyEra c) = ShelleyLedgersPredFailure (ShelleyEra c) type instance EraRuleEvent "LEDGERS" (ShelleyEra c) = ShelleyLedgersEvent (ShelleyEra c) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs index 3a9b32d4d5f..d9cfb9afa89 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs @@ -76,7 +76,6 @@ import Cardano.Ledger.Conway.Rules ( import Cardano.Ledger.DRep (DRep (..)) import Cardano.Ledger.PoolDistr (IndividualPoolStake (..)) import Constrained hiding (inject) -import Data.Bifunctor (Bifunctor (..)) import Data.Foldable (Foldable (..)) import Data.Map.Strict (Map) import qualified Data.Map.Strict as Map @@ -92,9 +91,10 @@ import Test.Cardano.Ledger.Common (Arbitrary (..)) import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), SpecTranslate (..), - computationResultToEither, integerToHash, runSpecTransM, + unComputationResult, + unComputationResult_, ) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core (defaultTestConformance) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway (vkeyFromInteger) @@ -403,10 +403,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "RATIFY" Conway where signalSpec ctx _env _st = ratifySignalSpec ctx - runAgdaRule env st sig = - first (\case {}) - . computationResultToEither - $ Agda.ratifyStep env st sig + runAgdaRule env st sig = unComputationResult_ $ Agda.ratifyStep env st sig extraInfo _ ctx env@RatifyEnv {..} st sig@(RatifySignal actions) _ = PP.vsep $ specExtraInfo : (actionAcceptedRatio <$> toList actions) @@ -563,10 +560,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "ENACT" Conway where environmentSpec _ = TrueSpec stateSpec = enactStateSpec signalSpec = enactSignalSpec - runAgdaRule env st sig = - first (\e -> error $ "ENACT failed with:\n" <> show e) - . computationResultToEither - $ Agda.enactStep env st sig + runAgdaRule env st sig = unComputationResult $ Agda.enactStep env st sig classOf = Just . nameEnact @@ -595,10 +589,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "EPOCH" Conway where signalSpec _ _ _ = epochSignalSpec - runAgdaRule env st sig = - first (\case {}) - . computationResultToEither - $ Agda.epochStep env st sig + runAgdaRule env st sig = unComputationResult_ $ Agda.epochStep env st sig classOf = Just . nameEpoch @@ -615,10 +606,7 @@ instance IsConwayUniv fn => ExecSpecRule fn "NEWEPOCH" Conway where signalSpec _ _ _ = epochSignalSpec - runAgdaRule env st sig = - first (\case {}) - . computationResultToEither - $ Agda.newEpochStep env st sig + runAgdaRule env st sig = unComputationResult_ $ Agda.newEpochStep env st sig externalFunctions :: Agda.ExternalFunctions externalFunctions = Agda.MkExternalFunctions {..} diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Cert.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Cert.hs index dcf2e169121..249b4020162 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Cert.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Cert.hs @@ -19,10 +19,7 @@ import Cardano.Ledger.Conway import Cardano.Ledger.Conway.TxCert (ConwayTxCert (..)) import Cardano.Ledger.Crypto (StandardCrypto) import Constrained (lit) -import Data.Bifunctor (first) -import qualified Data.List.NonEmpty as NE import Data.Map.Strict (Map) -import qualified Data.Text as T import qualified Lib as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base @@ -41,10 +38,7 @@ instance environmentSpec _ = certEnvSpec stateSpec ctx _ = certStateSpec (lit $ ccecDelegatees ctx) signalSpec _ = txCertSpec - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.certStep env st sig + runAgdaRule env st sig = unComputationResult $ Agda.certStep env st sig classOf = Just . nameTxCert diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs index 192cb138fbd..5c538135d1e 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Certs.hs @@ -15,11 +15,9 @@ import Cardano.Ledger.Conway import Cardano.Ledger.Conway.TxCert import Constrained import Data.Bifunctor (first) -import qualified Data.List.NonEmpty as NE import qualified Data.Map.Strict as Map import Data.Sequence (Seq) import qualified Data.Set as Set -import qualified Data.Text as T import qualified Lib as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base @@ -45,10 +43,7 @@ instance signalSpec _ = txCertsSpec - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.certsStep env st sig + runAgdaRule env st sig = unComputationResult $ Agda.certsStep env st sig classOf = Just . nameCerts testConformance ctx env st sig = property $ do @@ -74,7 +69,14 @@ instance credsSet = Set.fromList creds zeroRewards (Agda.MkHSMap pairs) = Agda.MkHSMap (map (\(c, r) -> if c `Set.member` credsSet then (c, 0) else (c, r)) pairs) - _ -> checkConformance @"CERTS" @Conway @fn ctx env st sig implResTest agdaResTest + _ -> + checkConformance @"CERTS" @Conway @fn + ctx + env + st + sig + (first showOpaqueErrorString implResTest) + agdaResTest nameCerts :: Seq (ConwayTxCert Conway) -> String nameCerts x = "Certs length " ++ show (length x) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs index afe0f01511d..0534e41a265 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Deleg.hs @@ -14,10 +14,8 @@ import Cardano.Ledger.Credential (Credential) import Cardano.Ledger.Crypto (StandardCrypto) import Cardano.Ledger.Keys (KeyRole (..)) import Constrained (lit) -import Data.Bifunctor (bimap) -import qualified Data.List.NonEmpty as NE +import Data.Bifunctor (Bifunctor (..)) import Data.Set (Set) -import qualified Data.Text as T import qualified Lib as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.ExecSpecRule.Core () @@ -36,10 +34,9 @@ instance IsConwayUniv fn => ExecSpecRule fn "DELEG" Conway where signalSpec _ = conwayDelegCertSpec runAgdaRule env (Agda.MkCertState dState pState vState) sig = - bimap - (\e -> OpaqueErrorString (T.unpack e) NE.:| []) + second (\dState' -> Agda.MkCertState dState' pState vState) - . computationResultToEither + . unComputationResult $ Agda.delegStep env dState sig classOf = Just . nameDelegCert diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Gov.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Gov.hs index 7bb18e2c31d..dce1a96ae9a 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Gov.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Gov.hs @@ -1,15 +1,10 @@ {-# LANGUAGE DataKinds #-} -{-# LANGUAGE DeriveGeneric #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE NamedFieldPuns #-} -{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-} {-# OPTIONS_GHC -Wno-orphans #-} @@ -22,9 +17,6 @@ import Cardano.Ledger.Conway.Governance import Cardano.Ledger.Conway.Rules import Cardano.Ledger.Crypto import Cardano.Ledger.TxIn (TxId) -import Data.Bifunctor (first) -import qualified Data.List.NonEmpty as NE -import qualified Data.Text as T import Lens.Micro import qualified Lib as Agda import Test.Cardano.Ledger.Conformance @@ -66,10 +58,7 @@ instance , enactState ) - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.govStep env st sig + runAgdaRule env st sig = unComputationResult $ Agda.govStep env st sig translateInputs env@GovEnv {gePParams} st sig (txId, _proposalsSplit, enactState) = do agdaEnv <- expectRight $ runSpecTransM ctx $ toSpecRep env diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs index efa3a8ddba0..609bd307182 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/GovCert.hs @@ -22,9 +22,7 @@ import Cardano.Ledger.Conway.TxCert import Cardano.Ledger.Crypto (StandardCrypto) import Constrained (lit) import Data.Bifunctor (Bifunctor (..)) -import qualified Data.List.NonEmpty as NE import Data.Map.Strict (Map) -import qualified Data.Text as T import qualified Lib as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base @@ -47,11 +45,8 @@ instance classOf = Just . nameGovCert runAgdaRule env (Agda.MkCertState dState pState vState) sig = - bimap - (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - (Agda.MkCertState dState pState) - . computationResultToEither - $ Agda.govCertStep env vState sig + second (Agda.MkCertState dState pState) . unComputationResult $ + Agda.govCertStep env vState sig nameGovCert :: ConwayGovCert c -> String nameGovCert (ConwayRegDRep {}) = "ConwayRegDRep" diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs index 966b4593ec4..e58442333eb 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledger.hs @@ -17,7 +17,6 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledger (ConwayLedgerE import Data.Bifunctor (Bifunctor (..)) import Data.Functor.Identity (Identity) -import qualified Data.List.NonEmpty as NE import Cardano.Ledger.BaseTypes (Inject (..), StrictMaybe) import Cardano.Ledger.Conway.Core ( @@ -35,11 +34,11 @@ import Cardano.Ledger.Conway.Rules (EnactState) import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), FixupSpecRep (..), - OpaqueErrorString (..), checkConformance, - computationResultToEither, runSpecTransM, + showOpaqueErrorString, toTestRep, + unComputationResult, ) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway () import Test.Cardano.Ledger.Constrained.Conway (IsConwayUniv, UtxoExecContext (..), utxoStateSpec) @@ -62,7 +61,6 @@ import Cardano.Ledger.Binary.Coders (Encode (..), encode, (!>)) import Cardano.Ledger.Shelley.LedgerState (LedgerState (..)) import Cardano.Ledger.Shelley.Rules (LedgerEnv (..), UtxoEnv (..)) import Data.Bitraversable (bimapM) -import qualified Data.Text as T import GHC.Generics (Generic) import Lens.Micro.Mtl (use) import qualified Lib as Agda @@ -150,10 +148,7 @@ instance let UtxoExecContext {..} = clecUtxoExecContext in constrained (==. lit uecTx) - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.ledgerStep env st sig + runAgdaRule env st sig = unComputationResult $ Agda.ledgerStep env st sig extraInfo globals @@ -171,7 +166,9 @@ instance stFinal where utxoEnv = UtxoEnv ledgerSlotNo ledgerPp lsCertState - stFinal = runSTS @"UTXOW" @Conway globals utxoEnv lsUTxOState sig + stFinal = + first showOpaqueErrorString $ + runSTS @"UTXOW" @Conway globals utxoEnv lsUTxOState sig testConformance ctx env st sig = property $ do (specEnv, specSt, specSig) <- @@ -185,7 +182,7 @@ instance logDoc $ "specSt:\n" <> ansiExpr specSt logDoc $ "specSig:\n" <> ansiExpr specSig agdaResTest <- - fmap (bimap (fixup <$>) fixup) $ + fmap (second fixup) $ impAnn "Deep evaluating Agda output" $ evaluateDeep $ runAgdaRule @fn @"LEDGER" @Conway specEnv specSt specSig @@ -196,9 +193,19 @@ instance impAnn "Translating implementation values to SpecRep" $ expectRightExpr $ runSpecTransM ctx $ - bimapM (traverse toTestRep) (toTestRep . inject @_ @(ExecState fn "LEDGER" Conway) . fst) implRes + bimapM + (fmap showOpaqueErrorString . traverse toTestRep) + (toTestRep . inject @_ @(ExecState fn "LEDGER" Conway) . fst) + implRes globals <- use impGlobalsL - let extra = extraInfo @fn @"LEDGER" @Conway globals ctx (inject env) (inject st) (inject sig) implRes + let extra = + extraInfo @fn @"LEDGER" @Conway + globals + ctx + (inject env) + (inject st) + (inject sig) + (first showOpaqueErrorString implRes) logDoc extra checkConformance @"LEDGER" @Conway @fn ctx diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledgers.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledgers.hs index 9623922c669..6ea8df712a3 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledgers.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Ledgers.hs @@ -11,14 +11,10 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Ledgers () where import Cardano.Ledger.Conway (Conway) import Cardano.Ledger.Conway.Governance (EnactState) import Constrained (Specification (..)) -import Data.Bifunctor (Bifunctor (..)) -import qualified Data.List.NonEmpty as NE -import qualified Data.Text as T import qualified Lib as Agda import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), - OpaqueErrorString (..), - computationResultToEither, + unComputationResult, ) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway () import Test.Cardano.Ledger.Constrained.Conway (IsConwayUniv) @@ -29,7 +25,4 @@ instance IsConwayUniv fn => ExecSpecRule fn "LEDGERS" Conway where environmentSpec _ = TrueSpec stateSpec _ _ = TrueSpec signalSpec _ _ _ = TrueSpec - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.ledgersStep env st sig + runAgdaRule env st sig = unComputationResult $ Agda.ledgersStep env st sig diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Pool.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Pool.hs index 7e0a3eda6b7..71c5455444e 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Pool.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Pool.hs @@ -9,9 +9,6 @@ module Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Pool where import Cardano.Ledger.Conway import Cardano.Ledger.Core (PoolCert (..)) -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.Core () @@ -24,12 +21,9 @@ instance IsConwayUniv fn => ExecSpecRule fn "POOL" Conway where stateSpec _ _ = pStateSpec - signalSpec _ env st = poolCertSpec env st + signalSpec _ = poolCertSpec - runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.poolStep env st sig + runAgdaRule env st sig = unComputationResult $ Agda.poolStep env st sig classOf = Just . namePoolCert diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs index 995249c0317..a475d32ed95 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxo.hs @@ -19,8 +19,6 @@ import Cardano.Ledger.Conway (Conway) import Cardano.Ledger.Core (EraPParams (..), ppMaxTxSizeL, sizeTxF) import Cardano.Ledger.Shelley.LedgerState (LedgerState (..), UTxOState (..)) import Cardano.Ledger.Shelley.Rules (UtxoEnv (..)) -import Data.Bifunctor (Bifunctor (..)) -import qualified Data.List.NonEmpty as NE import qualified Data.Text as T import Lens.Micro ((&), (.~), (^.)) import qualified Lib as Agda @@ -29,10 +27,9 @@ import qualified Prettyprinter as PP import Test.Cardano.Ledger.Common (Arbitrary (..), Gen, showExpr) import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), - OpaqueErrorString (..), SpecTranslate (..), - computationResultToEither, runSpecTransM, + unComputationResult, ) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () @@ -99,9 +96,8 @@ instance signalSpec ctx _ _ = utxoTxSpec ctx runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.utxoStep externalFunctions env st sig + unComputationResult $ + Agda.utxoStep externalFunctions env st sig extraInfo _ ctx env@UtxoEnv {..} st@UTxOState {..} sig st' = PP.vcat diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs index 94cc42d1bdb..df045d4a1f4 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Utxow.hs @@ -16,17 +16,16 @@ import Cardano.Ledger.Conway (Conway, ConwayEra) import Cardano.Ledger.Conway.TxCert (ConwayTxCert) import Cardano.Ledger.Crypto (StandardCrypto) import Data.Bifunctor (Bifunctor (..)) -import qualified Data.List.NonEmpty as NE import qualified Data.Text as T import qualified Lib as Agda import qualified Prettyprinter as PP import Test.Cardano.Ledger.Conformance ( ExecSpecRule (..), - OpaqueErrorString (..), SpecTranslate, - computationResultToEither, runSpecTransM, + showOpaqueErrorString, toSpecRep, + unComputationResult, ) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Base (externalFunctions) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway.Utxo (genUtxoExecContext) @@ -57,9 +56,7 @@ instance stateSpec = utxoStateSpec signalSpec ctx _ _ = utxoTxSpec ctx runAgdaRule env st sig = - first (\e -> OpaqueErrorString (T.unpack e) NE.:| []) - . computationResultToEither - $ Agda.utxowStep externalFunctions env st sig + unComputationResult $ Agda.utxowStep externalFunctions env st sig extraInfo globals ctx env st sig _ = let result = @@ -68,7 +65,7 @@ instance <$> toSpecRep env <*> toSpecRep st <*> toSpecRep sig - stFinal = runSTS @"UTXO" @Conway globals env st sig + stFinal = first showOpaqueErrorString $ runSTS @"UTXO" @Conway globals env st sig utxoInfo = extraInfo @fn @"UTXO" @Conway globals ctx env st sig stFinal in PP.vcat diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs index 8e3d1208694..55ff051a498 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Core.hs @@ -38,10 +38,11 @@ import Control.State.Transition.Extended (STS (..)) import Data.Bifunctor (Bifunctor (..)) import Data.Bitraversable (bimapM) import Data.Functor (($>)) +import Data.List.NonEmpty (NonEmpty) import Data.String (fromString) import qualified Data.Text as T import Data.Typeable (Proxy (..), Typeable, typeRep) -import GHC.Base (Constraint, NonEmpty, Symbol, Type) +import GHC.Base (Constraint, Symbol, Type) import GHC.TypeLits (KnownSymbol) import Lens.Micro.Mtl (use) import Prettyprinter @@ -51,8 +52,10 @@ import Test.Cardano.Ledger.Api.DebugTools (writeCBOR) import Test.Cardano.Ledger.Binary.TreeDiff (Pretty (..), ansiWlPretty, ediff, ppEditExpr) import Test.Cardano.Ledger.Conformance.SpecTranslate.Core ( FixupSpecRep (..), + OpaqueErrorString (..), SpecTranslate (..), runSpecTransM, + showOpaqueErrorString, toTestRep, ) import Test.Cardano.Ledger.Imp.Common @@ -138,9 +141,7 @@ class SpecRep (ExecEnvironment fn rule era) -> SpecRep (ExecState fn rule era) -> SpecRep (ExecSignal fn rule era) -> - Either - (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) - (SpecRep (ExecState fn rule era)) + Either OpaqueErrorString (SpecRep (ExecState fn rule era)) translateInputs :: HasCallStack => @@ -203,6 +204,8 @@ class , EncCBOR (State (EraRule rule era)) , EncCBOR (Signal (EraRule rule era)) , ToExpr (ExecContext fn rule era) + , ToExpr (PredicateFailure (EraRule rule era)) + , NFData (PredicateFailure (EraRule rule era)) , HasCallStack ) => ExecContext fn rule era -> @@ -219,9 +222,7 @@ class Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> - Either - (NonEmpty (PredicateFailure (EraRule rule era))) - (State (EraRule rule era), [Event (EraRule rule era)]) -> + Either OpaqueErrorString (State (EraRule rule era), [Event (EraRule rule era)]) -> Doc AnsiStyle extraInfo _ _ _ _ _ = mempty @@ -253,9 +254,7 @@ diffConformance implRes agdaRes = checkConformance :: forall rule era fn. ( Era era - , ToExpr (SpecRep (PredicateFailure (EraRule rule era))) , ToExpr (SpecRep (ExecState fn rule era)) - , Eq (SpecRep (PredicateFailure (EraRule rule era))) , Eq (SpecRep (ExecState fn rule era)) , EncCBOR (ExecContext fn rule era) , EncCBOR (Environment (EraRule rule era)) @@ -267,12 +266,8 @@ checkConformance :: Environment (EraRule rule era) -> State (EraRule rule era) -> Signal (EraRule rule era) -> - Either - (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) - (SpecRep (ExecState fn rule era)) -> - Either - (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) - (SpecRep (ExecState fn rule era)) -> + Either OpaqueErrorString (SpecRep (ExecState fn rule era)) -> + Either OpaqueErrorString (SpecRep (ExecState fn rule era)) -> ImpTestM era () checkConformance ctx env st sig implResTest agdaResTest = do let @@ -300,24 +295,22 @@ checkConformance ctx env st sig implResTest agdaResTest = do defaultTestConformance :: forall fn era rule. - ( ShelleyEraImp era + ( HasCallStack + , ShelleyEraImp era , ExecSpecRule fn rule era , ForAllExecSpecRep NFData fn rule era , ForAllExecSpecRep ToExpr fn rule era - , NFData (SpecRep (PredicateFailure (EraRule rule era))) - , ToExpr (SpecRep (PredicateFailure (EraRule rule era))) - , Eq (SpecRep (PredicateFailure (EraRule rule era))) + , NFData (PredicateFailure (EraRule rule era)) , Eq (SpecRep (ExecState fn rule era)) , Inject (State (EraRule rule era)) (ExecState fn rule era) , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era) - , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))) , FixupSpecRep (SpecRep (ExecState fn rule era)) , EncCBOR (ExecContext fn rule era) , EncCBOR (Environment (EraRule rule era)) , EncCBOR (State (EraRule rule era)) , EncCBOR (Signal (EraRule rule era)) , ToExpr (ExecContext fn rule era) - , HasCallStack + , ToExpr (PredicateFailure (EraRule rule era)) ) => ExecContext fn rule era -> ExecEnvironment fn rule era -> @@ -327,22 +320,35 @@ defaultTestConformance :: defaultTestConformance ctx env st sig = property $ do (implResTest, agdaResTest, implRes) <- runConformance @rule @fn @era ctx env st sig globals <- use impGlobalsL - let extra = extraInfo @fn @rule @era globals ctx (inject env) (inject st) (inject sig) implRes + let + extra = + extraInfo @fn @rule @era + globals + ctx + (inject env) + (inject st) + (inject sig) + (first showOpaqueErrorString implRes) logDoc extra - checkConformance @rule @_ @fn ctx (inject env) (inject st) (inject sig) implResTest agdaResTest + checkConformance @rule @_ @fn + ctx + (inject env) + (inject st) + (inject sig) + (first showOpaqueErrorString implResTest) + agdaResTest runConformance :: forall (rule :: Symbol) (fn :: [Type] -> Type -> Type) era. ( ExecSpecRule fn rule era - , NFData (SpecRep (PredicateFailure (EraRule rule era))) , ForAllExecSpecRep NFData fn rule era , ForAllExecSpecRep ToExpr fn rule era - , FixupSpecRep (SpecRep (PredicateFailure (EraRule rule era))) , FixupSpecRep (SpecRep (ExecState fn rule era)) , Inject (State (EraRule rule era)) (ExecState fn rule era) , SpecTranslate (ExecContext fn rule era) (ExecState fn rule era) , ToExpr (ExecContext fn rule era) , HasCallStack + , NFData (PredicateFailure (EraRule rule era)) ) => ExecContext fn rule era -> ExecEnvironment fn rule era -> @@ -351,11 +357,9 @@ runConformance :: ImpTestM era ( Either - (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) - (SpecRep (ExecState fn rule era)) - , Either - (NonEmpty (SpecRep (PredicateFailure (EraRule rule era)))) + (NonEmpty (PredicateFailure (EraRule rule era))) (SpecRep (ExecState fn rule era)) + , Either OpaqueErrorString (SpecRep (ExecState fn rule era)) , Either (NonEmpty (PredicateFailure (EraRule rule era))) (State (EraRule rule era), [Event (EraRule rule era)]) @@ -372,7 +376,7 @@ runConformance execContext env st sig = do logDoc $ "specSt:\n" <> ansiExpr specSt logDoc $ "specSig:\n" <> ansiExpr specSig agdaResTest <- - fmap (bimap (fixup <$>) fixup) $ + fmap (second fixup) $ impAnn "Deep evaluating Agda output" $ evaluateDeep $ runAgdaRule @fn @rule @era specEnv specSt specSig @@ -381,7 +385,7 @@ runConformance execContext env st sig = do impAnn "Translating implementation values to SpecRep" $ expectRightExpr $ runSpecTransM execContext $ - bimapM (traverse toTestRep) (toTestRep . inject @_ @(ExecState fn rule era) . fst) implRes + bimapM pure (toTestRep . inject @_ @(ExecState fn rule era) . fst) implRes pure (implResTest, agdaResTest, implRes) conformsToImpl :: @@ -406,6 +410,8 @@ conformsToImpl :: , EncCBOR (State (EraRule rule era)) , EncCBOR (Signal (EraRule rule era)) , HasCallStack + , NFData (PredicateFailure (EraRule rule era)) + , ToExpr (PredicateFailure (EraRule rule era)) ) => Property conformsToImpl = property @(ImpTestM era Property) . (`runContT` pure) $ do diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs index 13eb3018a15..8ab1919bbfe 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Orphans.hs @@ -9,7 +9,9 @@ module Test.Cardano.Ledger.Conformance.Orphans where import Data.Bifunctor (Bifunctor (..)) import Data.Default (Default) import Data.List (nub, sortOn) +import Data.List.NonEmpty (NonEmpty) import qualified Data.Set as Set +import Data.Text (Text) import Data.Void (Void) import GHC.Generics (Generic) import Lib @@ -250,6 +252,11 @@ instance Default (HSMap k v) instance FixupSpecRep Void +instance FixupSpecRep a => FixupSpecRep (NonEmpty a) + +instance FixupSpecRep Text where + fixup = id + instance FixupSpecRep OpaqueErrorString instance FixupSpecRep a => FixupSpecRep [a] diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs index c8b242959f3..cb5bc23c10a 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Base.hs @@ -124,6 +124,7 @@ import Test.Cardano.Ledger.Conformance ( SpecTranslationError, askCtx, hashToInteger, + showOpaqueErrorString, withCtx, ) import Test.Cardano.Ledger.Constrained.Conway (DepositPurpose (..), IsConwayUniv) @@ -719,7 +720,7 @@ instance where type SpecRep (ConwayGovPredFailure era) = OpaqueErrorString - toSpecRep e = pure . OpaqueErrorString . show $ toExpr e + toSpecRep = pure . showOpaqueErrorString instance SpecTranslate ctx (GovPurposeId r c) where type SpecRep (GovPurposeId r c) = (Agda.TxId, Integer) @@ -1038,7 +1039,7 @@ instance where type SpecRep (ConwayCertPredFailure era) = OpaqueErrorString - toSpecRep = pure . OpaqueErrorString . showExpr + toSpecRep = pure . showOpaqueErrorString instance (SpecTranslate ctx a, Compactible a) => SpecTranslate ctx (CompactForm a) where type SpecRep (CompactForm a) = SpecRep a diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs index 3cc3e7f2267..2a9b673cd0c 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Cert.hs @@ -215,4 +215,4 @@ instance instance SpecTranslate ctx (ConwayNewEpochPredFailure era) where type SpecRep (ConwayNewEpochPredFailure era) = OpaqueErrorString - toSpecRep = pure . OpaqueErrorString . show . toExpr + toSpecRep = pure . showOpaqueErrorString diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Certs.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Certs.hs index 23fc179e169..b7af073dca6 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Certs.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Certs.hs @@ -28,7 +28,7 @@ import Test.Cardano.Ledger.Conway.TreeDiff instance ToExpr (PredicateFailure (EraRule "CERT" era)) => SpecTranslate ctx (ConwayCertsPredFailure era) where type SpecRep (ConwayCertsPredFailure era) = OpaqueErrorString - toSpecRep = pure . OpaqueErrorString . show . toExpr + toSpecRep = pure . showOpaqueErrorString instance ( SpecTranslate ctx (PParamsHKD Identity era) diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Deleg.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Deleg.hs index 0e8962dc05b..c5d69c24744 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Deleg.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Deleg.hs @@ -36,7 +36,6 @@ import Test.Cardano.Ledger.Conformance ( ) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base import Test.Cardano.Ledger.Conformance.SpecTranslate.Core -import Test.Cardano.Ledger.Conway.TreeDiff instance ( SpecRep (PParamsHKD Identity era) ~ Agda.PParams @@ -81,7 +80,7 @@ instance SpecTranslate ctx (ConwayDelegCert c) where instance SpecTranslate ctx (ConwayDelegPredFailure era) where type SpecRep (ConwayDelegPredFailure era) = OpaqueErrorString - toSpecRep e = pure . OpaqueErrorString . show $ toExpr e + toSpecRep = pure . showOpaqueErrorString instance SpecTranslate ctx (DState era) where type SpecRep (DState era) = Agda.DState diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/GovCert.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/GovCert.hs index 23b12add57a..cecb74b21b7 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/GovCert.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/GovCert.hs @@ -2,7 +2,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TypeApplications #-} @@ -40,7 +39,6 @@ import qualified Data.Map.Strict as Map import qualified Lib as Agda import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base import Test.Cardano.Ledger.Conformance.SpecTranslate.Core -import Test.Cardano.Ledger.Conway.TreeDiff (showExpr) instance Crypto c => SpecTranslate ctx (ConwayGovCert c) where type SpecRep (ConwayGovCert c) = Agda.DCert @@ -90,7 +88,7 @@ instance instance SpecTranslate ctx (ConwayGovCertPredFailure era) where type SpecRep (ConwayGovCertPredFailure era) = OpaqueErrorString - toSpecRep = pure . OpaqueErrorString . showExpr + toSpecRep = pure . showOpaqueErrorString instance SpecTranslate ctx (VState era) where type SpecRep (VState era) = Agda.GState diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledger.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledger.hs index 20e41521ac8..a7b9f33876d 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledger.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledger.hs @@ -21,7 +21,7 @@ import Control.State.Transition.Extended (STS (..)) import Data.Functor.Identity (Identity) import Data.Maybe.Strict (StrictMaybe) import qualified Lib as Agda -import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), askCtx) +import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), askCtx, showOpaqueErrorString) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..)) import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..)) @@ -55,4 +55,4 @@ instance where type SpecRep (ConwayLedgerPredFailure era) = OpaqueErrorString - toSpecRep e = pure . OpaqueErrorString . show $ toExpr e + toSpecRep = pure . showOpaqueErrorString diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledgers.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledgers.hs index 3317362fee2..e0c86e0d863 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledgers.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Ledgers.hs @@ -19,9 +19,14 @@ import Cardano.Ledger.Shelley.LedgerState (AccountState (..)) import Cardano.Ledger.Shelley.Rules (Identity, ShelleyLedgersEnv (..), ShelleyLedgersPredFailure) import Control.State.Transition.Extended (STS (..)) import qualified Lib as Agda -import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), SpecTranslate (..), askCtx) +import Test.Cardano.Ledger.Conformance ( + OpaqueErrorString (..), + SpecTranslate (..), + askCtx, + showOpaqueErrorString, + ) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base () -import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr, showExpr) +import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr) instance ( EraPParams era @@ -50,4 +55,4 @@ instance where type SpecRep (ShelleyLedgersPredFailure era) = OpaqueErrorString - toSpecRep = pure . OpaqueErrorString . showExpr + toSpecRep = pure . showOpaqueErrorString diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Pool.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Pool.hs index 599b4d2f3d7..ee0292ef678 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Pool.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Pool.hs @@ -18,7 +18,6 @@ import Data.Map.Strict (mapKeys) import qualified Lib as Agda import Test.Cardano.Ledger.Conformance import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base () -import Test.Cardano.Ledger.Conway.TreeDiff instance ( SpecRep (PParamsHKD Identity era) ~ Agda.PParams @@ -33,7 +32,7 @@ instance instance SpecTranslate ctx (ShelleyPoolPredFailure era) where type SpecRep (ShelleyPoolPredFailure era) = OpaqueErrorString - toSpecRep e = pure . OpaqueErrorString . show $ toExpr e + toSpecRep = pure . showOpaqueErrorString instance SpecTranslate ctx (PState era) where type SpecRep (PState era) = Agda.PState diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxo.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxo.hs index 208942ce139..afe84169e94 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxo.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxo.hs @@ -18,7 +18,7 @@ import Cardano.Ledger.Shelley.Rules (UtxoEnv (..)) import Control.State.Transition.Extended (STS (..)) import Data.Functor.Identity (Identity) import qualified Lib as Agda -import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..)) +import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), showOpaqueErrorString) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Base (SpecTranslate (..)) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Cert () import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr (..)) @@ -46,4 +46,4 @@ instance where type SpecRep (ConwayUtxoPredFailure era) = OpaqueErrorString - toSpecRep e = pure . OpaqueErrorString . show $ toExpr e + toSpecRep = pure . showOpaqueErrorString diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxow.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxow.hs index 5f45e169ea6..382b92dd384 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxow.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Conway/Utxow.hs @@ -10,8 +10,12 @@ module Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxow () where import Cardano.Ledger.Conway.Core (AlonzoEraScript (..), AsItem, AsIx, Era, EraRule, EraTxCert (..)) import Cardano.Ledger.Conway.Rules (ConwayUtxowPredFailure, PredicateFailure) -import Test.Cardano.Ledger.Conformance (OpaqueErrorString (..), SpecTranslate (..)) -import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr, showExpr) +import Test.Cardano.Ledger.Conformance ( + OpaqueErrorString (..), + SpecTranslate (..), + showOpaqueErrorString, + ) +import Test.Cardano.Ledger.Conway.TreeDiff (ToExpr) import Test.Cardano.Ledger.Conformance.SpecTranslate.Conway.Utxo () @@ -26,4 +30,4 @@ instance where type SpecRep (ConwayUtxowPredFailure era) = OpaqueErrorString - toSpecRep = pure . OpaqueErrorString . showExpr + toSpecRep = pure . showOpaqueErrorString diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Core.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Core.hs index 731540c88d8..5c4dbd9d981 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Core.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/SpecTranslate/Core.hs @@ -17,12 +17,15 @@ module Test.Cardano.Ledger.Conformance.SpecTranslate.Core ( SpecTranslationError, SpecTranslate (..), FixupSpecRep (..), + OpaqueErrorString (..), SpecTransM, runSpecTransM, askCtx, withCtx, toTestRep, - OpaqueErrorString (..), + showOpaqueErrorString, + unComputationResult, + unComputationResult_, ) where import Cardano.Ledger.BaseTypes (Inject (..)) @@ -30,26 +33,15 @@ import Constrained.Base () import Control.DeepSeq (NFData) import Control.Monad.Except (ExceptT, MonadError (..), runExceptT) import Control.Monad.Reader (MonadReader (..), Reader, asks, runReader) +import Data.Foldable (Foldable (..)) import Data.Kind (Type) +import Data.List.NonEmpty (NonEmpty) import Data.Text (Text) +import qualified Data.Text as T +import Data.Void (Void) import GHC.Generics (Generic (..), K1 (..), M1 (..), U1 (..), V1, (:*:) (..), (:+:) (..)) -import Test.Cardano.Ledger.TreeDiff (Expr (..), ToExpr (..)) - --- | OpaqueErrorString behaves like unit in comparisons, but contains an --- error string that can be displayed. -newtype OpaqueErrorString = OpaqueErrorString String - deriving (Generic, Show) - -instance Eq OpaqueErrorString where - _ == _ = True - -instance ToExpr OpaqueErrorString where - -- Using `toExpr` on a `String` displays escape codes in place of unicode - -- characters (e.g. "≡" becomes "\8802") - -- TODO figure out a less hacky way to solve this problem - toExpr (OpaqueErrorString x) = App x [] - -instance NFData OpaqueErrorString +import qualified Lib as Agda +import Test.Cardano.Ledger.TreeDiff (Expr (..), ToExpr (..), showExpr) type SpecTranslationError = Text @@ -103,3 +95,29 @@ withCtx ctx m = do case runSpecTransM ctx m of Right x -> pure x Left e -> throwError e + +-- | OpaqueErrorString behaves like unit in comparisons, but contains an +-- error string that can be displayed. +newtype OpaqueErrorString = OpaqueErrorString (NonEmpty Text) + deriving (Generic, Show, Semigroup) + +-- | This implementation violates referential transparency. Do not rely on it +-- unless you know what you're doing. +instance Eq OpaqueErrorString where + _ == _ = True + +instance ToExpr OpaqueErrorString where + toExpr (OpaqueErrorString x) = App (T.unpack . T.unlines $ toList x) [] + +instance NFData OpaqueErrorString + +showOpaqueErrorString :: ToExpr a => a -> OpaqueErrorString +showOpaqueErrorString = OpaqueErrorString . pure . T.pack . showExpr + +unComputationResult :: Agda.ComputationResult Text a -> Either OpaqueErrorString a +unComputationResult (Agda.Success x) = Right x +unComputationResult (Agda.Failure e) = Left (OpaqueErrorString $ pure e) + +unComputationResult_ :: Agda.ComputationResult Void a -> Either e a +unComputationResult_ (Agda.Success x) = Right x +unComputationResult_ (Agda.Failure x) = case x of {} diff --git a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs index 22484322652..3bec20c2b05 100644 --- a/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs +++ b/libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/Utils.hs @@ -9,7 +9,6 @@ import Cardano.Crypto.Util (bytesToNatural, naturalToBytes) import Cardano.Ledger.Crypto (Crypto (..), StandardCrypto) import qualified Data.ByteString.Base16 as B16 import Data.Data (Proxy (..)) -import qualified Lib as Agda import Test.Cardano.Ledger.TreeDiff (Expr, ToExpr (..)) standardHashSize :: Int @@ -26,7 +25,3 @@ hashToInteger = toInteger . bytesToNatural . hashToBytes integerToHash :: forall h a. HashAlgorithm h => Integer -> Maybe (Hash h a) integerToHash = hashFromBytes . naturalToBytes (fromIntegral . sizeHash $ Proxy @h) . fromInteger - -computationResultToEither :: Agda.ComputationResult e a -> Either e a -computationResultToEither (Agda.Success x) = Right x -computationResultToEither (Agda.Failure e) = Left e diff --git a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs index 0db1fe163d0..0bb042775bb 100644 --- a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs +++ b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp.hs @@ -19,7 +19,7 @@ import Cardano.Ledger.Core import Cardano.Ledger.Shelley.LedgerState import Cardano.Ledger.Shelley.Rules (LedgerEnv, UtxoEnv (..), ledgerSlotNoL) import Control.State.Transition -import Data.Bifunctor (bimap) +import Data.Bifunctor (Bifunctor (..)) import Data.Bitraversable (bimapM) import Data.List.NonEmpty import Lens.Micro @@ -44,9 +44,6 @@ testImpConformance :: , SpecTranslate (ExecContext ConwayFn "LEDGER" era) (ExecState ConwayFn "LEDGER" era) , SpecTranslate (ExecContext ConwayFn "LEDGER" era) (ExecEnvironment ConwayFn "LEDGER" era) , SpecTranslate (ExecContext ConwayFn "LEDGER" era) (TxWits era) - , NFData (SpecRep (PredicateFailure (EraRule "LEDGER" era))) - , Eq (SpecRep (PredicateFailure (EraRule "LEDGER" era))) - , FixupSpecRep (SpecRep (PredicateFailure (EraRule "LEDGER" era))) , HasCallStack , SpecRep (TxWits era) ~ Agda.TxWitnesses , SpecRep (TxBody era) ~ Agda.TxBody @@ -88,7 +85,7 @@ testImpConformance _ impRuleResult env state signal = do <*> expectRight (runSpecTransM ctx $ toSpecRep signal) -- get agda response agdaResponse <- - fmap (bimap (fixup <$>) fixup) $ + fmap (second fixup) $ evaluateDeep $ runAgdaRule @ConwayFn @"LEDGER" @era specEnv specState specSignal -- translate imp response @@ -96,7 +93,7 @@ testImpConformance _ impRuleResult env state signal = do expectRightExpr $ runSpecTransM ctx $ bimapM - (traverse toTestRep) + (pure . showOpaqueErrorString) (toTestRep . inject @_ @(ExecState ConwayFn "LEDGER" era) . fst) impRuleResult @@ -108,7 +105,7 @@ spec = withImpInit @(LedgerSpec Conway) $ modifyImpInitProtVer @Conway (natVersion @10) $ modifyImpInitExpectLedgerRuleConformance testImpConformance $ do - describe "Basic imp conformance" $ + describe "Basic imp conformance" $ do it "Submit constitution" $ do _ <- submitConstitution @Conway SNothing passNEpochs 2 diff --git a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs index c23dce5d154..13fd842b0aa 100644 --- a/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs +++ b/libs/cardano-ledger-conformance/test/Test/Cardano/Ledger/Conformance/Imp/Ratify.hs @@ -30,12 +30,13 @@ import Cardano.Ledger.Shelley.LedgerState ( nesELL, nesEsL, ) +import Data.Bifunctor (Bifunctor (..)) import qualified Data.List.NonEmpty as NE import qualified Data.Map as Map import qualified Data.Sequence.Strict as SSeq import Lens.Micro ((&), (.~)) import Lens.Micro.Mtl (use) -import Test.Cardano.Ledger.Conformance () +import Test.Cardano.Ledger.Conformance (showOpaqueErrorString) import Test.Cardano.Ledger.Conformance.ExecSpecRule.Conway ( ConwayRatifyExecContext (..), ) @@ -161,5 +162,6 @@ spec = withImpInit @(LedgerSpec Conway) $ describe "RATIFY" $ modifyImpInitProtV ratEnv ratSt ratSig - implRes' - impAnn "Conformance failed" $ implRes `shouldBeExpr` agdaRes + (first showOpaqueErrorString implRes') + impAnn "Conformance failed" $ + first showOpaqueErrorString implRes `shouldBeExpr` agdaRes diff --git a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/Functions.hs b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/Functions.hs index 45517dd2b86..c73361c296e 100644 --- a/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/Functions.hs +++ b/libs/cardano-ledger-test/src/Test/Cardano/Ledger/Generic/Functions.hs @@ -402,6 +402,8 @@ instance Reflect era => TotalAda (UTxOState era) where -- we don't add in the _deposits, because it is invariant that this -- is equal to the sum of the key deposit map and the pool deposit map -- So these are accounted for in the instance (TotalAda (CertState era)) +-- TODO I'm not sure this is true ^ +-- Imp conformance tests show in logs that totalAda is off by the deposit amount instance Reflect era => TotalAda (UTxO era) where totalAda (UTxO m) = foldl accum mempty m