{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Cardano.Ledger.Examples.STSTestUtils (
  initUTxO,
  mkGenesisTxIn,
  mkTxDats,
  someAddr,
  someKeys,
  someScriptAddr,
  testBBODY,
  runLEDGER,
  testUTXOW,
  testUTXOWsubset,
  testUTXOspecialCase,
  trustMeP,
  alwaysFailsHash,
  alwaysSucceedsHash,
  timelockScript,
  timelockHash,
  timelockStakeCred,
)
where

import qualified Cardano.Crypto.Hash as CH
import Cardano.Ledger.Address (Addr (..))
import Cardano.Ledger.Alonzo.Rules (
  AlonzoUtxoPredFailure (..),
  AlonzoUtxosPredFailure (..),
  AlonzoUtxowPredFailure (..),
 )
import Cardano.Ledger.Alonzo.Tx (
  AlonzoTx (..),
  IsValid (..),
 )
import Cardano.Ledger.Alonzo.TxWits (TxDats (..))
import Cardano.Ledger.BHeaderView (BHeaderView (..))
import Cardano.Ledger.Babbage.Rules (BabbageUtxoPredFailure (..))
import Cardano.Ledger.Babbage.Rules as Babbage (BabbageUtxowPredFailure (..))
import Cardano.Ledger.BaseTypes (
  Network (..),
  mkTxIxPartial,
 )
import Cardano.Ledger.Coin (Coin (..))
import qualified Cardano.Ledger.Conway.Rules as Conway
import Cardano.Ledger.Credential (
  Credential (..),
  StakeCredential,
  StakeReference (..),
 )
import Cardano.Ledger.Crypto
import Cardano.Ledger.Keys (KeyRole (..), hashKey)
import Cardano.Ledger.Plutus.Data (Data (..), hashData)
import Cardano.Ledger.Shelley.API (
  Block (..),
  LedgerEnv (..),
  LedgerState (..),
  UTxO (..),
 )
import Cardano.Ledger.Shelley.Core hiding (TranslationError)
import Cardano.Ledger.Shelley.LedgerState (smartUTxOState)
import Cardano.Ledger.Shelley.Rules (
  BbodyEnv (..),
  ShelleyBbodyState,
  UtxoEnv (..),
 )
import Cardano.Ledger.Shelley.Rules as Shelley (ShelleyUtxowPredFailure (..))
import Cardano.Ledger.TxIn (TxIn (..))
import Cardano.Ledger.Val (inject)
import Cardano.Slotting.Slot (SlotNo (..))
import Control.State.Transition.Extended hiding (Assertion)
import Data.Default.Class (Default (..))
import Data.Foldable (toList)
import Data.List.NonEmpty (NonEmpty ((:|)))
import qualified Data.Map.Strict as Map
import GHC.Natural (Natural)
import GHC.Stack
import qualified PlutusLedgerApi.V1 as PV1
import Test.Cardano.Ledger.Core.KeyPair (KeyPair (..))
import Test.Cardano.Ledger.Generic.Fields (
  TxOutField (..),
 )
import Test.Cardano.Ledger.Generic.PrettyCore (PrettyA (..))
import Test.Cardano.Ledger.Generic.Proof
import Test.Cardano.Ledger.Generic.Scriptic (PostShelley, Scriptic (..), after, matchkey)
import Test.Cardano.Ledger.Generic.Updaters
import Test.Cardano.Ledger.Shelley.Generator.EraGen (genesisId)
import Test.Cardano.Ledger.Shelley.Utils (
  RawSeed (..),
  mkKeyPair,
 )
import Test.Tasty.HUnit (Assertion, assertFailure, (@?=))

import Test.Cardano.Ledger.Constrained.Preds.Tx (pcTxWithUTxO)

-- =================================================================
-- =========================  Shared data  =========================
--   Data with specific semantics ("constants")
-- =================================================================

alwaysFailsHash :: forall era. Scriptic era => Natural -> Proof era -> ScriptHash (EraCrypto era)
alwaysFailsHash :: forall era.
Scriptic era =>
Natural -> Proof era -> ScriptHash (EraCrypto era)
alwaysFailsHash Natural
n Proof era
pf = forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript @era forall a b. (a -> b) -> a -> b
$ forall era. Scriptic era => Natural -> Proof era -> Script era
never Natural
n Proof era
pf

alwaysSucceedsHash ::
  forall era.
  Scriptic era =>
  Natural ->
  Proof era ->
  ScriptHash (EraCrypto era)
alwaysSucceedsHash :: forall era.
Scriptic era =>
Natural -> Proof era -> ScriptHash (EraCrypto era)
alwaysSucceedsHash Natural
n Proof era
pf = forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript @era forall a b. (a -> b) -> a -> b
$ forall era. Scriptic era => Natural -> Proof era -> Script era
always Natural
n Proof era
pf

someKeys :: forall era. Era era => Proof era -> KeyPair 'Payment (EraCrypto era)
someKeys :: forall era.
Era era =>
Proof era -> KeyPair 'Payment (EraCrypto era)
someKeys Proof era
_pf = forall (kd :: KeyRole) c.
VKey kd c -> SignKeyDSIGN (DSIGN c) -> KeyPair kd c
KeyPair VKey 'Payment (EraCrypto era)
vk SignKeyDSIGN (DSIGN (EraCrypto era))
sk
  where
    (SignKeyDSIGN (DSIGN (EraCrypto era))
sk, VKey 'Payment (EraCrypto era)
vk) = forall c (kd :: KeyRole).
DSIGNAlgorithm (DSIGN c) =>
RawSeed -> (SignKeyDSIGN (DSIGN c), VKey kd c)
mkKeyPair @(EraCrypto era) (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> RawSeed
RawSeed Word64
1 Word64
1 Word64
1 Word64
1 Word64
1)

someAddr :: forall era. Era era => Proof era -> Addr (EraCrypto era)
someAddr :: forall era. Era era => Proof era -> Addr (EraCrypto era)
someAddr Proof era
pf = forall c.
Network -> PaymentCredential c -> StakeReference c -> Addr c
Addr Network
Testnet Credential 'Payment (EraCrypto era)
pCred StakeReference (EraCrypto era)
sCred
  where
    (SignKeyDSIGN (DSIGN (EraCrypto era))
_ssk, VKey 'Staking (EraCrypto era)
svk) = forall c (kd :: KeyRole).
DSIGNAlgorithm (DSIGN c) =>
RawSeed -> (SignKeyDSIGN (DSIGN c), VKey kd c)
mkKeyPair @(EraCrypto era) (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> RawSeed
RawSeed Word64
0 Word64
0 Word64
0 Word64
0 Word64
2)
    pCred :: Credential 'Payment (EraCrypto era)
pCred = forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (kd :: KeyRole). Crypto c => VKey kd c -> KeyHash kd c
hashKey forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kd :: KeyRole) c. KeyPair kd c -> VKey kd c
vKey forall a b. (a -> b) -> a -> b
$ forall era.
Era era =>
Proof era -> KeyPair 'Payment (EraCrypto era)
someKeys Proof era
pf
    sCred :: StakeReference (EraCrypto era)
sCred = forall c. StakeCredential c -> StakeReference c
StakeRefBase forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (kd :: KeyRole). Crypto c => VKey kd c -> KeyHash kd c
hashKey forall a b. (a -> b) -> a -> b
$ VKey 'Staking (EraCrypto era)
svk

-- Create an address with a given payment script.
someScriptAddr :: forall era. Scriptic era => Script era -> Addr (EraCrypto era)
someScriptAddr :: forall era. Scriptic era => Script era -> Addr (EraCrypto era)
someScriptAddr Script era
s = forall c.
Network -> PaymentCredential c -> StakeReference c -> Addr c
Addr Network
Testnet Credential 'Payment (EraCrypto era)
pCred StakeReference (EraCrypto era)
sCred
  where
    pCred :: Credential 'Payment (EraCrypto era)
pCred = forall (kr :: KeyRole) c. ScriptHash c -> Credential kr c
ScriptHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript @era forall a b. (a -> b) -> a -> b
$ Script era
s
    (SignKeyDSIGN (DSIGN (EraCrypto era))
_ssk, VKey 'Staking (EraCrypto era)
svk) = forall c (kd :: KeyRole).
DSIGNAlgorithm (DSIGN c) =>
RawSeed -> (SignKeyDSIGN (DSIGN c), VKey kd c)
mkKeyPair @(EraCrypto era) (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> RawSeed
RawSeed Word64
0 Word64
0 Word64
0 Word64
0 Word64
0)
    sCred :: StakeReference (EraCrypto era)
sCred = forall c. StakeCredential c -> StakeReference c
StakeRefBase forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (kd :: KeyRole). Crypto c => VKey kd c -> KeyHash kd c
hashKey forall a b. (a -> b) -> a -> b
$ VKey 'Staking (EraCrypto era)
svk

timelockScript :: PostShelley era => Int -> Proof era -> Script era
timelockScript :: forall era. PostShelley era => Int -> Proof era -> Script era
timelockScript Int
s = forall era. EraScript era => NativeScript era -> Script era
fromNativeScript forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
Scriptic era =>
[Proof era -> NativeScript era] -> Proof era -> NativeScript era
allOf [forall era. Scriptic era => Int -> Proof era -> NativeScript era
matchkey Int
1, forall era. PostShelley era => Int -> Proof era -> NativeScript era
after (Int
100 forall a. Num a => a -> a -> a
+ Int
s)]

timelockHash ::
  forall era.
  PostShelley era =>
  Int ->
  Proof era ->
  ScriptHash (EraCrypto era)
timelockHash :: forall era.
PostShelley era =>
Int -> Proof era -> ScriptHash (EraCrypto era)
timelockHash Int
n Proof era
pf = forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript @era forall a b. (a -> b) -> a -> b
$ forall era. PostShelley era => Int -> Proof era -> Script era
timelockScript Int
n Proof era
pf

timelockStakeCred :: PostShelley era => Proof era -> StakeCredential (EraCrypto era)
timelockStakeCred :: forall era.
PostShelley era =>
Proof era -> StakeCredential (EraCrypto era)
timelockStakeCred Proof era
pf = forall (kr :: KeyRole) c. ScriptHash c -> Credential kr c
ScriptHashObj (forall era.
PostShelley era =>
Int -> Proof era -> ScriptHash (EraCrypto era)
timelockHash Int
2 Proof era
pf)

-- ======================================================================
-- ========================= Initial Utxo ===============================
-- ======================================================================

initUTxO :: forall era. (EraTxOut era, PostShelley era) => Proof era -> UTxO era
initUTxO :: forall era.
(EraTxOut era, PostShelley era) =>
Proof era -> UTxO era
initUTxO Proof era
pf =
  forall era. Map (TxIn (EraCrypto era)) (TxOut era) -> UTxO era
UTxO forall a b. (a -> b) -> a -> b
$
    forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList forall a b. (a -> b) -> a -> b
$
      [ (forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
1, TxOut era
alwaysSucceedsOutput)
      , (forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
2, TxOut era
alwaysFailsOutput)
      ]
        forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (\Integer
i -> (forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
i, TxOut era
someOutput)) [Integer
3 .. Integer
8]
        forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (\Integer
i -> (forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
i, TxOut era
collateralOutput)) [Integer
11 .. Integer
18]
        forall a. [a] -> [a] -> [a]
++ [ (forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
100, TxOut era
timelockOut)
           , (forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
101, TxOut era
unspendableOut)
           , (forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
102, TxOut era
alwaysSucceedsOutputV1)
           , (forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
103, TxOut era
nonScriptOutWithDatum)
           ]
  where
    alwaysSucceedsOutput :: TxOut era
alwaysSucceedsOutput =
      forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr (EraCrypto era) -> TxOutField era
Address (forall era. Scriptic era => Script era -> Addr (EraCrypto era)
someScriptAddr (forall era. Scriptic era => Natural -> Proof era -> Script era
always Natural
3 Proof era
pf))
        , forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
5000)
        , forall era. [DataHash (EraCrypto era)] -> TxOutField era
DHash' [forall era. Era era => Data era -> DataHash (EraCrypto era)
hashData forall a b. (a -> b) -> a -> b
$ forall era. Era era => Data era
datumExample1 @era]
        ]
    alwaysFailsOutput :: TxOut era
alwaysFailsOutput =
      forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr (EraCrypto era) -> TxOutField era
Address (forall era. Scriptic era => Script era -> Addr (EraCrypto era)
someScriptAddr (forall era. Scriptic era => Natural -> Proof era -> Script era
never Natural
0 Proof era
pf))
        , forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
3000)
        , forall era. [DataHash (EraCrypto era)] -> TxOutField era
DHash' [forall era. Era era => Data era -> DataHash (EraCrypto era)
hashData forall a b. (a -> b) -> a -> b
$ forall era. Era era => Data era
datumExample2 @era]
        ]
    someOutput :: TxOut era
someOutput = forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [forall era. Addr (EraCrypto era) -> TxOutField era
Address forall a b. (a -> b) -> a -> b
$ forall era. Era era => Proof era -> Addr (EraCrypto era)
someAddr Proof era
pf, forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
1000)]
    collateralOutput :: TxOut era
collateralOutput = forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [forall era. Addr (EraCrypto era) -> TxOutField era
Address forall a b. (a -> b) -> a -> b
$ forall era. Era era => Proof era -> Addr (EraCrypto era)
someAddr Proof era
pf, forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
5)]
    timelockOut :: TxOut era
timelockOut = forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [forall era. Addr (EraCrypto era) -> TxOutField era
Address forall a b. (a -> b) -> a -> b
$ Addr (EraCrypto era)
timelockAddr, forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
1)]
    timelockAddr :: Addr (EraCrypto era)
timelockAddr = forall c.
Network -> PaymentCredential c -> StakeReference c -> Addr c
Addr Network
Testnet Credential 'Payment (EraCrypto era)
pCred StakeReference (EraCrypto era)
sCred
      where
        (SignKeyDSIGN (DSIGN (EraCrypto era))
_ssk, VKey 'Staking (EraCrypto era)
svk) = forall c (kd :: KeyRole).
DSIGNAlgorithm (DSIGN c) =>
RawSeed -> (SignKeyDSIGN (DSIGN c), VKey kd c)
mkKeyPair @(EraCrypto era) (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> RawSeed
RawSeed Word64
0 Word64
0 Word64
0 Word64
0 Word64
2)
        pCred :: Credential 'Payment (EraCrypto era)
pCred = forall (kr :: KeyRole) c. ScriptHash c -> Credential kr c
ScriptHashObj ScriptHash (EraCrypto era)
tlh
        sCred :: StakeReference (EraCrypto era)
sCred = forall c. StakeCredential c -> StakeReference c
StakeRefBase forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kr :: KeyRole) c. KeyHash kr c -> Credential kr c
KeyHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall c (kd :: KeyRole). Crypto c => VKey kd c -> KeyHash kd c
hashKey forall a b. (a -> b) -> a -> b
$ VKey 'Staking (EraCrypto era)
svk
        tlh :: ScriptHash (EraCrypto era)
tlh = forall era.
EraScript era =>
Script era -> ScriptHash (EraCrypto era)
hashScript @era forall a b. (a -> b) -> a -> b
$ Int -> Script era
tls Int
0
        tls :: Int -> Script era
tls Int
s = forall era. EraScript era => NativeScript era -> Script era
fromNativeScript forall a b. (a -> b) -> a -> b
$ forall era.
Scriptic era =>
[Proof era -> NativeScript era] -> Proof era -> NativeScript era
allOf [forall era. Scriptic era => Int -> Proof era -> NativeScript era
matchkey Int
1, forall era. PostShelley era => Int -> Proof era -> NativeScript era
after (Int
100 forall a. Num a => a -> a -> a
+ Int
s)] Proof era
pf
    -- This output is unspendable since it is locked by a plutus script, but has no datum hash.
    unspendableOut :: TxOut era
unspendableOut =
      forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr (EraCrypto era) -> TxOutField era
Address (forall era. Scriptic era => Script era -> Addr (EraCrypto era)
someScriptAddr (forall era. Scriptic era => Natural -> Proof era -> Script era
always Natural
3 Proof era
pf))
        , forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
5000)
        ]
    alwaysSucceedsOutputV1 :: TxOut era
alwaysSucceedsOutputV1 =
      forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr (EraCrypto era) -> TxOutField era
Address (forall era. Scriptic era => Script era -> Addr (EraCrypto era)
someScriptAddr (forall era. Scriptic era => Natural -> Proof era -> Script era
always Natural
3 Proof era
pf))
        , forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
5000)
        , forall era. [DataHash (EraCrypto era)] -> TxOutField era
DHash' [forall era. Era era => Data era -> DataHash (EraCrypto era)
hashData forall a b. (a -> b) -> a -> b
$ forall era. Era era => Data era
datumExample1 @era]
        ]
    nonScriptOutWithDatum :: TxOut era
nonScriptOutWithDatum =
      forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr (EraCrypto era) -> TxOutField era
Address (forall era. Era era => Proof era -> Addr (EraCrypto era)
someAddr Proof era
pf)
        , forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
1221)
        , forall era. [DataHash (EraCrypto era)] -> TxOutField era
DHash' [forall era. Era era => Data era -> DataHash (EraCrypto era)
hashData forall a b. (a -> b) -> a -> b
$ forall era. Era era => Data era
datumExample1 @era]
        ]

datumExample1 :: Era era => Data era
datumExample1 :: forall era. Era era => Data era
datumExample1 = forall era. Era era => Data -> Data era
Data (Integer -> Data
PV1.I Integer
123)

datumExample2 :: Era era => Data era
datumExample2 :: forall era. Era era => Data era
datumExample2 = forall era. Era era => Data -> Data era
Data (Integer -> Data
PV1.I Integer
0)

-- ======================================================================
-- ========================= Shared helper functions  ===================
-- ======================================================================

mkGenesisTxIn :: (CH.HashAlgorithm (HASH c), HasCallStack) => Integer -> TxIn c
mkGenesisTxIn :: forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn = forall c. TxId c -> TxIx -> TxIn c
TxIn forall c. HashAlgorithm (HASH c) => TxId c
genesisId forall b c a. (b -> c) -> (a -> b) -> a -> c
. HasCallStack => Integer -> TxIx
mkTxIxPartial

mkTxDats :: Era era => Data era -> TxDats era
mkTxDats :: forall era. Era era => Data era -> TxDats era
mkTxDats Data era
d = forall era.
Era era =>
Map (DataHash (EraCrypto era)) (Data era) -> TxDats era
TxDats forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton (forall era. Era era => Data era -> DataHash (EraCrypto era)
hashData Data era
d) Data era
d

trustMeP :: Proof era -> Bool -> Tx era -> Tx era
trustMeP :: forall era. Proof era -> Bool -> Tx era -> Tx era
trustMeP Proof era
Alonzo Bool
iv' (AlonzoTx TxBody (AlonzoEra StandardCrypto)
b TxWits (AlonzoEra StandardCrypto)
w IsValid
_ StrictMaybe (TxAuxData (AlonzoEra StandardCrypto))
m) = forall era.
TxBody era
-> TxWits era
-> IsValid
-> StrictMaybe (TxAuxData era)
-> AlonzoTx era
AlonzoTx TxBody (AlonzoEra StandardCrypto)
b TxWits (AlonzoEra StandardCrypto)
w (Bool -> IsValid
IsValid Bool
iv') StrictMaybe (TxAuxData (AlonzoEra StandardCrypto))
m
trustMeP Proof era
Babbage Bool
iv' (AlonzoTx TxBody (BabbageEra StandardCrypto)
b TxWits (BabbageEra StandardCrypto)
w IsValid
_ StrictMaybe (TxAuxData (BabbageEra StandardCrypto))
m) = forall era.
TxBody era
-> TxWits era
-> IsValid
-> StrictMaybe (TxAuxData era)
-> AlonzoTx era
AlonzoTx TxBody (BabbageEra StandardCrypto)
b TxWits (BabbageEra StandardCrypto)
w (Bool -> IsValid
IsValid Bool
iv') StrictMaybe (TxAuxData (BabbageEra StandardCrypto))
m
trustMeP Proof era
Conway Bool
iv' (AlonzoTx TxBody (ConwayEra StandardCrypto)
b TxWits (ConwayEra StandardCrypto)
w IsValid
_ StrictMaybe (TxAuxData (ConwayEra StandardCrypto))
m) = forall era.
TxBody era
-> TxWits era
-> IsValid
-> StrictMaybe (TxAuxData era)
-> AlonzoTx era
AlonzoTx TxBody (ConwayEra StandardCrypto)
b TxWits (ConwayEra StandardCrypto)
w (Bool -> IsValid
IsValid Bool
iv') StrictMaybe (TxAuxData (ConwayEra StandardCrypto))
m
trustMeP Proof era
_ Bool
_ Tx era
tx = Tx era
tx

-- This implements a special rule to test that for ValidationTagMismatch. Rather than comparing the insides of
-- ValidationTagMismatch (which are complicated and depend on Plutus) we just note that both the computed
-- and expected are ValidationTagMismatch. Of course the 'path' to ValidationTagMismatch differs by Era.
-- so we need to case over the Era proof, to get the path correctly.
testBBODY ::
  (Reflect era, HasCallStack) =>
  WitRule "BBODY" era ->
  ShelleyBbodyState era ->
  Block (BHeaderView (EraCrypto era)) era ->
  Either (NonEmpty (PredicateFailure (EraRule "BBODY" era))) (ShelleyBbodyState era) ->
  PParams era ->
  Assertion
testBBODY :: forall era.
(Reflect era, HasCallStack) =>
WitRule "BBODY" era
-> ShelleyBbodyState era
-> Block (BHeaderView (EraCrypto era)) era
-> Either
     (NonEmpty (PredicateFailure (EraRule "BBODY" era)))
     (ShelleyBbodyState era)
-> PParams era
-> Assertion
testBBODY wit :: WitRule "BBODY" era
wit@(BBODY Proof era
proof) ShelleyBbodyState era
initialSt Block (BHeaderView (EraCrypto era)) era
block Either
  (NonEmpty (PredicateFailure (EraRule "BBODY" era)))
  (ShelleyBbodyState era)
expected PParams era
pparams =
  let env :: BbodyEnv era
env = forall era. PParams era -> AccountState -> BbodyEnv era
BbodyEnv PParams era
pparams forall a. Default a => a
def
   in case Proof era
proof of
        Proof era
Alonzo -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "BBODY" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (BbodyEnv era
env, ShelleyBbodyState era
initialSt, Block (BHeaderView (EraCrypto era)) era
block)) (forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq y, PrettyA x, PrettyA y, HasCallStack) =>
[Char] -> Either (t x) y -> Either (t x) y -> Assertion
genericCont [Char]
"" Either
  (NonEmpty (PredicateFailure (EraRule "BBODY" era)))
  (ShelleyBbodyState era)
expected)
        Proof era
Babbage -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "BBODY" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (BbodyEnv era
env, ShelleyBbodyState era
initialSt, Block (BHeaderView (EraCrypto era)) era
block)) (forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq y, PrettyA x, PrettyA y, HasCallStack) =>
[Char] -> Either (t x) y -> Either (t x) y -> Assertion
genericCont [Char]
"" Either
  (NonEmpty (PredicateFailure (EraRule "BBODY" era)))
  (ShelleyBbodyState era)
expected)
        Proof era
Conway -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "BBODY" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (BbodyEnv era
env, ShelleyBbodyState era
initialSt, Block (BHeaderView (EraCrypto era)) era
block)) (forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq y, PrettyA x, PrettyA y, HasCallStack) =>
[Char] -> Either (t x) y -> Either (t x) y -> Assertion
genericCont [Char]
"" Either
  (NonEmpty (PredicateFailure (EraRule "BBODY" era)))
  (ShelleyBbodyState era)
expected)
        Proof era
other -> forall a. HasCallStack => [Char] -> a
error ([Char]
"We cannot testBBODY in era " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Proof era
other)

testUTXOW ::
  forall era.
  ( Reflect era
  , HasCallStack
  ) =>
  WitRule "UTXOW" era ->
  UTxO era ->
  PParams era ->
  Tx era ->
  Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) (State (EraRule "UTXOW" era)) ->
  Assertion

-- | Use an equality test on the expected and computed [PredicateFailure]
testUTXOW :: forall era.
(Reflect era, HasCallStack) =>
WitRule "UTXOW" era
-> UTxO era
-> PParams era
-> Tx era
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" era)))
     (State (EraRule "UTXOW" era))
-> Assertion
testUTXOW wit :: WitRule "UTXOW" era
wit@(UTXOW Proof era
Alonzo) UTxO era
utxo PParams era
p Tx era
tx =
  forall era.
(GoodCrypto (EraCrypto era), EraTx era, EraGov era) =>
WitRule "UTXOW" era
-> (Result era -> Result era -> Assertion)
-> UTxO era
-> PParams era
-> Tx era
-> Result era
-> Assertion
testUTXOWwith WitRule "UTXOW" era
wit (forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq y, PrettyA x, PrettyA y, HasCallStack) =>
[Char] -> Either (t x) y -> Either (t x) y -> Assertion
genericCont (forall a. Show a => a -> [Char]
show (forall era. Reflect era => Proof era -> UTxO era -> Tx era -> PDoc
pcTxWithUTxO Proof (AlonzoEra StandardCrypto)
Alonzo UTxO era
utxo Tx era
tx))) UTxO era
utxo PParams era
p Tx era
tx
testUTXOW wit :: WitRule "UTXOW" era
wit@(UTXOW Proof era
Babbage) UTxO era
utxo PParams era
p Tx era
tx = forall era.
(GoodCrypto (EraCrypto era), EraTx era, EraGov era) =>
WitRule "UTXOW" era
-> (Result era -> Result era -> Assertion)
-> UTxO era
-> PParams era
-> Tx era
-> Result era
-> Assertion
testUTXOWwith WitRule "UTXOW" era
wit (forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq y, PrettyA x, PrettyA y, HasCallStack) =>
[Char] -> Either (t x) y -> Either (t x) y -> Assertion
genericCont (forall a. Show a => a -> [Char]
show Tx era
tx)) UTxO era
utxo PParams era
p Tx era
tx
testUTXOW wit :: WitRule "UTXOW" era
wit@(UTXOW Proof era
Conway) UTxO era
utxo PParams era
p Tx era
tx = forall era.
(GoodCrypto (EraCrypto era), EraTx era, EraGov era) =>
WitRule "UTXOW" era
-> (Result era -> Result era -> Assertion)
-> UTxO era
-> PParams era
-> Tx era
-> Result era
-> Assertion
testUTXOWwith WitRule "UTXOW" era
wit (forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq y, PrettyA x, PrettyA y, HasCallStack) =>
[Char] -> Either (t x) y -> Either (t x) y -> Assertion
genericCont (forall a. Show a => a -> [Char]
show Tx era
tx)) UTxO era
utxo PParams era
p Tx era
tx
testUTXOW (UTXOW Proof era
other) UTxO era
_ PParams era
_ Tx era
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"Cannot use testUTXOW in era " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Proof era
other)

testUTXOWsubset
  , testUTXOspecialCase ::
    forall era.
    ( Reflect era
    , HasCallStack
    ) =>
    WitRule "UTXOW" era ->
    UTxO era ->
    PParams era ->
    Tx era ->
    Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) (State (EraRule "UTXOW" era)) ->
    Assertion

-- | Use a subset test on the expected and computed [PredicateFailure]
testUTXOWsubset :: forall era.
(Reflect era, HasCallStack) =>
WitRule "UTXOW" era
-> UTxO era
-> PParams era
-> Tx era
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" era)))
     (State (EraRule "UTXOW" era))
-> Assertion
testUTXOWsubset wit :: WitRule "UTXOW" era
wit@(UTXOW Proof era
Alonzo) UTxO era
utxo = forall era.
(GoodCrypto (EraCrypto era), EraTx era, EraGov era) =>
WitRule "UTXOW" era
-> (Result era -> Result era -> Assertion)
-> UTxO era
-> PParams era
-> Tx era
-> Result era
-> Assertion
testUTXOWwith WitRule "UTXOW" era
wit forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq x, Eq y, PrettyA x, PrettyA y,
 Show (t x), Show y) =>
Either (t x) y -> Either (t x) y -> Assertion
subsetCont UTxO era
utxo
testUTXOWsubset wit :: WitRule "UTXOW" era
wit@(UTXOW Proof era
Babbage) UTxO era
utxo = forall era.
(GoodCrypto (EraCrypto era), EraTx era, EraGov era) =>
WitRule "UTXOW" era
-> (Result era -> Result era -> Assertion)
-> UTxO era
-> PParams era
-> Tx era
-> Result era
-> Assertion
testUTXOWwith WitRule "UTXOW" era
wit forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq x, Eq y, PrettyA x, PrettyA y,
 Show (t x), Show y) =>
Either (t x) y -> Either (t x) y -> Assertion
subsetCont UTxO era
utxo
testUTXOWsubset wit :: WitRule "UTXOW" era
wit@(UTXOW Proof era
Conway) UTxO era
utxo = forall era.
(GoodCrypto (EraCrypto era), EraTx era, EraGov era) =>
WitRule "UTXOW" era
-> (Result era -> Result era -> Assertion)
-> UTxO era
-> PParams era
-> Tx era
-> Result era
-> Assertion
testUTXOWwith WitRule "UTXOW" era
wit forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq x, Eq y, PrettyA x, PrettyA y,
 Show (t x), Show y) =>
Either (t x) y -> Either (t x) y -> Assertion
subsetCont UTxO era
utxo
testUTXOWsubset (UTXOW Proof era
other) UTxO era
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"Cannot use testUTXOW in era " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Proof era
other)

-- | Use a test where any two (ValidationTagMismatch x y) failures match regardless of 'x' and 'y'
testUTXOspecialCase :: forall era.
(Reflect era, HasCallStack) =>
WitRule "UTXOW" era
-> UTxO era
-> PParams era
-> Tx era
-> Either
     (NonEmpty (PredicateFailure (EraRule "UTXOW" era)))
     (State (EraRule "UTXOW" era))
-> Assertion
testUTXOspecialCase wit :: WitRule "UTXOW" era
wit@(UTXOW Proof era
proof) UTxO era
utxo PParams era
pparam Tx era
tx Either
  (NonEmpty (PredicateFailure (EraRule "UTXOW" era)))
  (State (EraRule "UTXOW" era))
expected =
  let env :: UtxoEnv era
env = forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv (Word64 -> SlotNo
SlotNo Word64
0) PParams era
pparam forall a. Default a => a
def
      state :: UTxOState era
state = forall era.
EraTxOut era =>
PParams era
-> UTxO era
-> Coin
-> Coin
-> GovState era
-> Coin
-> UTxOState era
smartUTxOState PParams era
pparam UTxO era
utxo (Integer -> Coin
Coin Integer
0) (Integer -> Coin
Coin Integer
0) forall a. Default a => a
def forall a. Monoid a => a
mempty
   in case Proof era
proof of
        Proof era
Alonzo -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (forall era a.
(Eq (PredicateFailure (EraRule "UTXOW" era)), Eq a,
 Show (PredicateFailure (EraRule "UTXOW" era)), Show a,
 HasCallStack) =>
Proof era
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
-> Assertion
specialCont Proof era
proof Either
  (NonEmpty (PredicateFailure (EraRule "UTXOW" era)))
  (State (EraRule "UTXOW" era))
expected)
        Proof era
Babbage -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (forall era a.
(Eq (PredicateFailure (EraRule "UTXOW" era)), Eq a,
 Show (PredicateFailure (EraRule "UTXOW" era)), Show a,
 HasCallStack) =>
Proof era
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
-> Assertion
specialCont Proof era
proof Either
  (NonEmpty (PredicateFailure (EraRule "UTXOW" era)))
  (State (EraRule "UTXOW" era))
expected)
        Proof era
Conway -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (forall era a.
(Eq (PredicateFailure (EraRule "UTXOW" era)), Eq a,
 Show (PredicateFailure (EraRule "UTXOW" era)), Show a,
 HasCallStack) =>
Proof era
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
-> Assertion
specialCont Proof era
proof Either
  (NonEmpty (PredicateFailure (EraRule "UTXOW" era)))
  (State (EraRule "UTXOW" era))
expected)
        Proof era
other -> forall a. HasCallStack => [Char] -> a
error ([Char]
"Cannot use specialCase in era " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show Proof era
other)

-- | This type is what you get when you use runSTS in the UTXOW rule. It is also
--   the type one uses for expected answers, to compare the 'computed' against 'expected'
type Result era =
  Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) (State (EraRule "UTXOW" era))

testUTXOWwith ::
  forall era.
  ( GoodCrypto (EraCrypto era)
  , EraTx era
  , EraGov era
  ) =>
  WitRule "UTXOW" era ->
  (Result era -> Result era -> Assertion) ->
  UTxO era ->
  PParams era ->
  Tx era ->
  Result era ->
  Assertion
testUTXOWwith :: forall era.
(GoodCrypto (EraCrypto era), EraTx era, EraGov era) =>
WitRule "UTXOW" era
-> (Result era -> Result era -> Assertion)
-> UTxO era
-> PParams era
-> Tx era
-> Result era
-> Assertion
testUTXOWwith wit :: WitRule "UTXOW" era
wit@(UTXOW Proof era
proof) Result era -> Result era -> Assertion
cont UTxO era
utxo PParams era
pparams Tx era
tx Result era
expected =
  let env :: UtxoEnv era
env = forall era. SlotNo -> PParams era -> CertState era -> UtxoEnv era
UtxoEnv (Word64 -> SlotNo
SlotNo Word64
0) PParams era
pparams forall a. Default a => a
def
      state :: UTxOState era
state = forall era.
EraTxOut era =>
PParams era
-> UTxO era
-> Coin
-> Coin
-> GovState era
-> Coin
-> UTxOState era
smartUTxOState PParams era
pparams UTxO era
utxo (Integer -> Coin
Coin Integer
0) (Integer -> Coin
Coin Integer
0) forall a. Default a => a
def forall a. Monoid a => a
mempty
   in case Proof era
proof of
        Proof era
Conway -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (Result era -> Result era -> Assertion
cont Result era
expected)
        Proof era
Babbage -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (Result era -> Result era -> Assertion
cont Result era
expected)
        Proof era
Alonzo -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (Result era -> Result era -> Assertion
cont Result era
expected)
        Proof era
Mary -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (Result era -> Result era -> Assertion
cont Result era
expected)
        Proof era
Allegra -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (Result era -> Result era -> Assertion
cont Result era
expected)
        Proof era
Shelley -> forall (s :: Symbol) e ans.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> (Either
      (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
    -> ans)
-> ans
runSTS WitRule "UTXOW" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (UtxoEnv era
env, UTxOState era
state, Tx era
tx)) (Result era -> Result era -> Assertion
cont Result era
expected)

runLEDGER ::
  forall era.
  ( GoodCrypto (EraCrypto era)
  , EraTx era
  , EraGov era
  ) =>
  WitRule "LEDGER" era ->
  LedgerState era ->
  PParams era ->
  Tx era ->
  Either (NonEmpty (PredicateFailure (EraRule "LEDGER" era))) (State (EraRule "LEDGER" era))
runLEDGER :: forall era.
(GoodCrypto (EraCrypto era), EraTx era, EraGov era) =>
WitRule "LEDGER" era
-> LedgerState era
-> PParams era
-> Tx era
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era))
runLEDGER wit :: WitRule "LEDGER" era
wit@(LEDGER Proof era
proof) LedgerState era
state PParams era
pparams Tx era
tx =
  let env :: LedgerEnv era
env = forall era.
SlotNo
-> TxIx -> PParams era -> AccountState -> Bool -> LedgerEnv era
LedgerEnv (Word64 -> SlotNo
SlotNo Word64
0) forall a. Bounded a => a
minBound PParams era
pparams forall a. Default a => a
def Bool
False
   in case Proof era
proof of
        Proof era
Conway -> forall (s :: Symbol) e.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> Either
     (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
runSTS' WitRule "LEDGER" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
env, LedgerState era
state, Tx era
tx))
        Proof era
Babbage -> forall (s :: Symbol) e.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> Either
     (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
runSTS' WitRule "LEDGER" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
env, LedgerState era
state, Tx era
tx))
        Proof era
Alonzo -> forall (s :: Symbol) e.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> Either
     (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
runSTS' WitRule "LEDGER" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
env, LedgerState era
state, Tx era
tx))
        Proof era
Mary -> forall (s :: Symbol) e.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> Either
     (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
runSTS' WitRule "LEDGER" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
env, LedgerState era
state, Tx era
tx))
        Proof era
Allegra -> forall (s :: Symbol) e.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> Either
     (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
runSTS' WitRule "LEDGER" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
env, LedgerState era
state, Tx era
tx))
        Proof era
Shelley -> forall (s :: Symbol) e.
(BaseM (EraRule s e) ~ ShelleyBase, STS (EraRule s e)) =>
WitRule s e
-> TRC (EraRule s e)
-> Either
     (NonEmpty (PredicateFailure (EraRule s e))) (State (EraRule s e))
runSTS' WitRule "LEDGER" era
wit (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
env, LedgerState era
state, Tx era
tx))

-- ======================================================================
-- =========================  Internal helper functions  ================
-- ======================================================================

-- | A small example of what a continuation for 'runSTS' might look like
genericCont ::
  ( Foldable t
  , Eq (t x)
  , Eq y
  , PrettyA x
  , PrettyA y
  , HasCallStack
  ) =>
  String ->
  Either (t x) y ->
  Either (t x) y ->
  Assertion
genericCont :: forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq y, PrettyA x, PrettyA y, HasCallStack) =>
[Char] -> Either (t x) y -> Either (t x) y -> Assertion
genericCont [Char]
cause Either (t x) y
expected Either (t x) y
computed =
  case (Either (t x) y
computed, Either (t x) y
expected) of
    (Left t x
c, Left t x
e)
      | t x
c forall a. Eq a => a -> a -> Bool
/= t x
e -> forall a. HasCallStack => [Char] -> IO a
assertFailure forall a b. (a -> b) -> a -> b
$ [Char]
causedBy forall a. [a] -> [a] -> [a]
++ forall {a} {t :: * -> *}. (PrettyA a, Foldable t) => t a -> [Char]
expectedToFail t x
e forall a. [a] -> [a] -> [a]
++ forall {a} {t :: * -> *}. (PrettyA a, Foldable t) => t a -> [Char]
failedWith t x
c
    (Right y
c, Right y
e)
      | y
c forall a. Eq a => a -> a -> Bool
/= y
e -> forall a. HasCallStack => [Char] -> IO a
assertFailure forall a b. (a -> b) -> a -> b
$ [Char]
causedBy forall a. [a] -> [a] -> [a]
++ forall {t}. PrettyA t => t -> [Char]
expectedToPass y
e forall a. [a] -> [a] -> [a]
++ forall {t}. PrettyA t => t -> [Char]
passedWith y
c
    (Left t x
x, Right y
y) ->
      forall a. HasCallStack => [Char] -> IO a
assertFailure forall a b. (a -> b) -> a -> b
$ [Char]
causedBy forall a. [a] -> [a] -> [a]
++ forall {t}. PrettyA t => t -> [Char]
expectedToPass y
y forall a. [a] -> [a] -> [a]
++ forall {a} {t :: * -> *}. (PrettyA a, Foldable t) => t a -> [Char]
failedWith t x
x
    (Right y
x, Left t x
y) ->
      forall a. HasCallStack => [Char] -> IO a
assertFailure forall a b. (a -> b) -> a -> b
$ [Char]
causedBy forall a. [a] -> [a] -> [a]
++ forall {a} {t :: * -> *}. (PrettyA a, Foldable t) => t a -> [Char]
expectedToFail t x
y forall a. [a] -> [a] -> [a]
++ forall {t}. PrettyA t => t -> [Char]
passedWith y
x
    (Either (t x) y, Either (t x) y)
_ -> forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  where
    causedBy :: [Char]
causedBy
      | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Char]
cause = [Char]
""
      | Bool
otherwise = [Char]
"Caused by:\n" forall a. [a] -> [a] -> [a]
++ [Char]
cause forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
    expectedToPass :: t -> [Char]
expectedToPass t
y = [Char]
"Expected to pass with:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA t
y) forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
    expectedToFail :: t a -> [Char]
expectedToFail t a
x = [Char]
"Expected to fail with:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t a
x) forall a. [a] -> [a] -> [a]
++ [Char]
"\n"
    failedWith :: t a -> [Char]
failedWith t a
x = [Char]
"But failed with:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t a
x)
    passedWith :: t -> [Char]
passedWith t
y = [Char]
"But passed with:\n" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA t
y)

subsetCont ::
  ( Foldable t
  , Eq (t x)
  , Eq x
  , Eq y
  , PrettyA x
  , PrettyA y
  , Show (t x)
  , Show y
  ) =>
  Either (t x) y ->
  Either (t x) y ->
  Assertion
subsetCont :: forall (t :: * -> *) x y.
(Foldable t, Eq (t x), Eq x, Eq y, PrettyA x, PrettyA y,
 Show (t x), Show y) =>
Either (t x) y -> Either (t x) y -> Assertion
subsetCont Either (t x) y
expected Either (t x) y
computed =
  case (Either (t x) y
computed, Either (t x) y
expected) of
    (Left t x
c, Left t x
e) ->
      -- It is OK if the expected is a subset of what's computed
      if forall (t :: * -> *) a. (Foldable t, Eq a) => t a -> t a -> Bool
isSubset t x
e t x
c then t x
e forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= t x
e else t x
c forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= t x
e
    (Right y
c, Right y
e) -> y
c forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= y
e
    (Left t x
x, Right y
y) ->
      forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
        [Char]
"expected to pass with "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA y
y)
          forall a. [a] -> [a] -> [a]
++ [Char]
"\n\nBut failed with\n\n"
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t x
x)
    (Right y
y, Left t x
x) ->
      forall a. HasCallStack => [Char] -> a
error forall a b. (a -> b) -> a -> b
$
        [Char]
"expected to fail with "
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t a -> [a]
toList t x
x)
          forall a. [a] -> [a] -> [a]
++ [Char]
"\n\nBut passed with\n\n"
          forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall t. PrettyA t => t -> PDoc
prettyA y
y)

specialCont ::
  ( Eq (PredicateFailure (EraRule "UTXOW" era))
  , Eq a
  , Show (PredicateFailure (EraRule "UTXOW" era))
  , Show a
  , HasCallStack
  ) =>
  Proof era ->
  Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a ->
  Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a ->
  Assertion
specialCont :: forall era a.
(Eq (PredicateFailure (EraRule "UTXOW" era)), Eq a,
 Show (PredicateFailure (EraRule "UTXOW" era)), Show a,
 HasCallStack) =>
Proof era
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
-> Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
-> Assertion
specialCont Proof era
proof Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
expected Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
computed =
  case (Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
computed, Either (NonEmpty (PredicateFailure (EraRule "UTXOW" era))) a
expected) of
    (Left (PredicateFailure (EraRule "UTXOW" era)
x :| []), Left (PredicateFailure (EraRule "UTXOW" era)
y :| [])) ->
      case (forall era.
Proof era
-> PredicateFailure (EraRule "UTXOW" era)
-> Maybe (PredicateFailure (EraRule "UTXOS" era))
findMismatch Proof era
proof PredicateFailure (EraRule "UTXOW" era)
x, forall era.
Proof era
-> PredicateFailure (EraRule "UTXOW" era)
-> Maybe (PredicateFailure (EraRule "UTXOS" era))
findMismatch Proof era
proof PredicateFailure (EraRule "UTXOW" era)
y) of
        (Just PredicateFailure (EraRule "UTXOS" era)
_, Just PredicateFailure (EraRule "UTXOS" era)
_) -> PredicateFailure (EraRule "UTXOW" era)
y forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= PredicateFailure (EraRule "UTXOW" era)
y
        (Maybe (PredicateFailure (EraRule "UTXOS" era))
_, Maybe (PredicateFailure (EraRule "UTXOS" era))
_) -> forall a. HasCallStack => [Char] -> a
error [Char]
"Not both ValidationTagMismatch case 1"
    (Left NonEmpty (PredicateFailure (EraRule "UTXOW" era))
_, Left NonEmpty (PredicateFailure (EraRule "UTXOW" era))
_) -> forall a. HasCallStack => [Char] -> a
error [Char]
"Not both ValidationTagMismatch case 2"
    (Right a
x, Right a
y) -> a
x forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= a
y
    (Left NonEmpty (PredicateFailure (EraRule "UTXOW" era))
_, Right a
_) -> forall a. HasCallStack => [Char] -> a
error [Char]
"expected to pass, but failed."
    (Right a
_, Left NonEmpty (PredicateFailure (EraRule "UTXOW" era))
_) -> forall a. HasCallStack => [Char] -> a
error [Char]
"expected to fail, but passed."

-- ========================================
-- This implements a special rule to test that for ValidationTagMismatch. Rather than comparing the insides of
-- ValidationTagMismatch (which are complicated and depend on Plutus) we just note that both the computed
-- and expected are ValidationTagMismatch. Of course the 'path' to ValidationTagMismatch differs by Era.
-- so we need to case over the Era proof, to get the path correctly.
findMismatch ::
  Proof era ->
  PredicateFailure (EraRule "UTXOW" era) ->
  Maybe (PredicateFailure (EraRule "UTXOS" era))
findMismatch :: forall era.
Proof era
-> PredicateFailure (EraRule "UTXOW" era)
-> Maybe (PredicateFailure (EraRule "UTXOS" era))
findMismatch Proof era
Alonzo (ShelleyInAlonzoUtxowPredFailure (Shelley.UtxoFailure (UtxosFailure x :: PredicateFailure (EraRule "UTXOS" (AlonzoEra StandardCrypto))
x@(ValidationTagMismatch IsValid
_ TagMismatchDescription
_)))) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure PredicateFailure (EraRule "UTXOS" (AlonzoEra StandardCrypto))
x
findMismatch Proof era
Babbage (Babbage.UtxoFailure (AlonzoInBabbageUtxoPredFailure (UtxosFailure x :: PredicateFailure (EraRule "UTXOS" (BabbageEra StandardCrypto))
x@(ValidationTagMismatch IsValid
_ TagMismatchDescription
_)))) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure PredicateFailure (EraRule "UTXOS" (BabbageEra StandardCrypto))
x
findMismatch
  Proof era
Conway
  ( Conway.UtxoFailure
      (Conway.UtxosFailure x :: PredicateFailure (EraRule "UTXOS" (ConwayEra StandardCrypto))
x@(Conway.ValidationTagMismatch IsValid
_ TagMismatchDescription
_))
    ) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (rule :: Symbol) (t :: * -> *) era.
InjectRuleFailure rule t era =>
t era -> EraRuleFailure rule era
injectFailure PredicateFailure (EraRule "UTXOS" (ConwayEra StandardCrypto))
x
findMismatch Proof era
_ PredicateFailure (EraRule "UTXOW" era)
_ = forall a. Maybe a
Nothing

isSubset :: (Foldable t, Eq a) => t a -> t a -> Bool
isSubset :: forall (t :: * -> *) a. (Foldable t, Eq a) => t a -> t a -> Bool
isSubset t a
small t a
big = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t a
big) t a
small