Skip to content

Commit

Permalink
OpaqueErrorString changes
Browse files Browse the repository at this point in the history
  • Loading branch information
Soupstraw committed Dec 13, 2024
1 parent b7fe1c3 commit 3bdb373
Show file tree
Hide file tree
Showing 31 changed files with 205 additions and 188 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -1,8 +1,10 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedLists #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

Expand All @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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)]
Expand All @@ -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
4 changes: 4 additions & 0 deletions eras/shelley/impl/src/Cardano/Ledger/Shelley/Rules/Ledgers.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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)
Expand Down Expand Up @@ -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)
Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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

Expand All @@ -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 {..}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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
Expand All @@ -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)
Original file line number Diff line number Diff line change
Expand Up @@ -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 ()
Expand All @@ -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
Expand Down
Original file line number Diff line number Diff line change
@@ -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 #-}

Expand All @@ -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
Expand Down Expand Up @@ -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
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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"
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -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 (
Expand All @@ -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)
Expand All @@ -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
Expand Down Expand Up @@ -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
Expand All @@ -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) <-
Expand All @@ -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
Expand All @@ -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
Expand Down
Loading

0 comments on commit 3bdb373

Please sign in to comment.