{-# 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 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.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 (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
alwaysFailsHash :: forall era. Scriptic era => Natural -> Proof era -> ScriptHash
alwaysFailsHash Natural
n Proof era
pf = forall era. EraScript era => Script era -> ScriptHash
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
alwaysSucceedsHash :: forall era. Scriptic era => Natural -> Proof era -> ScriptHash
alwaysSucceedsHash Natural
n Proof era
pf = forall era. EraScript era => Script era -> ScriptHash
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. Proof era -> KeyPair 'Payment
someKeys :: forall era. Proof era -> KeyPair 'Payment
someKeys Proof era
_pf = forall (kd :: KeyRole). VKey kd -> SignKeyDSIGN DSIGN -> KeyPair kd
KeyPair forall {kd :: KeyRole}. VKey kd
vk SignKeyDSIGN DSIGN
sk
  where
    (SignKeyDSIGN DSIGN
sk, VKey kd
vk) = forall (kd :: KeyRole). RawSeed -> (SignKeyDSIGN DSIGN, VKey kd)
mkKeyPair (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> RawSeed
RawSeed Word64
1 Word64
1 Word64
1 Word64
1 Word64
1)

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

-- Create an address with a given payment script.
someScriptAddr :: forall era. Scriptic era => Script era -> Addr
someScriptAddr :: forall era. Scriptic era => Script era -> Addr
someScriptAddr Script era
s = Network -> PaymentCredential -> StakeReference -> Addr
Addr Network
Testnet PaymentCredential
pCred StakeReference
sCred
  where
    pCred :: PaymentCredential
pCred = forall (kr :: KeyRole). ScriptHash -> Credential kr
ScriptHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraScript era => Script era -> ScriptHash
hashScript @era forall a b. (a -> b) -> a -> b
$ Script era
s
    (SignKeyDSIGN DSIGN
_ssk, VKey kd
svk) = forall (kd :: KeyRole). RawSeed -> (SignKeyDSIGN DSIGN, VKey kd)
mkKeyPair (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> RawSeed
RawSeed Word64
0 Word64
0 Word64
0 Word64
0 Word64
0)
    sCred :: StakeReference
sCred = StakeCredential -> StakeReference
StakeRefBase forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey forall a b. (a -> b) -> a -> b
$ forall {kd :: KeyRole}. VKey kd
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
timelockHash :: forall era. PostShelley era => Int -> Proof era -> ScriptHash
timelockHash Int
n Proof era
pf = forall era. EraScript era => Script era -> ScriptHash
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
timelockStakeCred :: forall era. PostShelley era => Proof era -> StakeCredential
timelockStakeCred Proof era
pf = forall (kr :: KeyRole). ScriptHash -> Credential kr
ScriptHashObj (forall era. PostShelley era => Int -> Proof era -> ScriptHash
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 (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
$
      [ (HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
1, TxOut era
alwaysSucceedsOutput)
      , (HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
2, TxOut era
alwaysFailsOutput)
      ]
        forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map (\Integer
i -> (HasCallStack => Integer -> TxIn
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 -> (HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
i, TxOut era
collateralOutput)) [Integer
11 .. Integer
18]
        forall a. [a] -> [a] -> [a]
++ [ (HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
100, TxOut era
timelockOut)
           , (HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
101, TxOut era
unspendableOut)
           , (HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
102, TxOut era
alwaysSucceedsOutputV1)
           , (HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
103, TxOut era
nonScriptOutWithDatum)
           ]
  where
    alwaysSucceedsOutput :: TxOut era
alwaysSucceedsOutput =
      forall era. Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr -> TxOutField era
Address (forall era. Scriptic era => Script era -> Addr
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] -> TxOutField era
DHash' [forall era. Data era -> DataHash
hashData forall a b. (a -> b) -> a -> b
$ forall era. Era era => Data era
datumExample1 @era]
        ]
    alwaysFailsOutput :: TxOut era
alwaysFailsOutput =
      forall era. Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr -> TxOutField era
Address (forall era. Scriptic era => Script era -> Addr
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] -> TxOutField era
DHash' [forall era. Data era -> DataHash
hashData forall a b. (a -> b) -> a -> b
$ forall era. Era era => Data era
datumExample2 @era]
        ]
    someOutput :: TxOut era
someOutput = forall era. Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [forall era. Addr -> TxOutField era
Address forall a b. (a -> b) -> a -> b
$ forall era. Proof era -> Addr
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. Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [forall era. Addr -> TxOutField era
Address forall a b. (a -> b) -> a -> b
$ forall era. Proof era -> Addr
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. Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [forall era. Addr -> TxOutField era
Address forall a b. (a -> b) -> a -> b
$ Addr
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
timelockAddr = Network -> PaymentCredential -> StakeReference -> Addr
Addr Network
Testnet PaymentCredential
pCred StakeReference
sCred
      where
        (SignKeyDSIGN DSIGN
_ssk, VKey kd
svk) = forall (kd :: KeyRole). RawSeed -> (SignKeyDSIGN DSIGN, VKey kd)
mkKeyPair (Word64 -> Word64 -> Word64 -> Word64 -> Word64 -> RawSeed
RawSeed Word64
0 Word64
0 Word64
0 Word64
0 Word64
2)
        pCred :: PaymentCredential
pCred = forall (kr :: KeyRole). ScriptHash -> Credential kr
ScriptHashObj ScriptHash
tlh
        sCred :: StakeReference
sCred = StakeCredential -> StakeReference
StakeRefBase forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kr :: KeyRole). KeyHash kr -> Credential kr
KeyHashObj forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (kd :: KeyRole). VKey kd -> KeyHash kd
hashKey forall a b. (a -> b) -> a -> b
$ forall {kd :: KeyRole}. VKey kd
svk
        tlh :: ScriptHash
tlh = forall era. EraScript era => Script era -> ScriptHash
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. Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr -> TxOutField era
Address (forall era. Scriptic era => Script era -> Addr
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. Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr -> TxOutField era
Address (forall era. Scriptic era => Script era -> Addr
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] -> TxOutField era
DHash' [forall era. Data era -> DataHash
hashData forall a b. (a -> b) -> a -> b
$ forall era. Era era => Data era
datumExample1 @era]
        ]
    nonScriptOutWithDatum :: TxOut era
nonScriptOutWithDatum =
      forall era. Proof era -> [TxOutField era] -> TxOut era
newTxOut
        Proof era
pf
        [ forall era. Addr -> TxOutField era
Address (forall era. Proof era -> Addr
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] -> TxOutField era
DHash' [forall era. Data era -> DataHash
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 :: HasCallStack => Integer -> TxIn
mkGenesisTxIn :: HasCallStack => Integer -> TxIn
mkGenesisTxIn = TxId -> TxIx -> TxIn
TxIn TxId
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 (Data era) -> TxDats era
TxDats forall a b. (a -> b) -> a -> b
$ forall k a. k -> a -> Map k a
Map.singleton (forall era. Data era -> DataHash
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
b TxWits AlonzoEra
w IsValid
_ StrictMaybe (TxAuxData AlonzoEra)
m) = forall era.
TxBody era
-> TxWits era
-> IsValid
-> StrictMaybe (TxAuxData era)
-> AlonzoTx era
AlonzoTx TxBody AlonzoEra
b TxWits AlonzoEra
w (Bool -> IsValid
IsValid Bool
iv') StrictMaybe (TxAuxData AlonzoEra)
m
trustMeP Proof era
Babbage Bool
iv' (AlonzoTx TxBody BabbageEra
b TxWits BabbageEra
w IsValid
_ StrictMaybe (TxAuxData BabbageEra)
m) = forall era.
TxBody era
-> TxWits era
-> IsValid
-> StrictMaybe (TxAuxData era)
-> AlonzoTx era
AlonzoTx TxBody BabbageEra
b TxWits BabbageEra
w (Bool -> IsValid
IsValid Bool
iv') StrictMaybe (TxAuxData BabbageEra)
m
trustMeP Proof era
Conway Bool
iv' (AlonzoTx TxBody ConwayEra
b TxWits ConwayEra
w IsValid
_ StrictMaybe (TxAuxData ConwayEra)
m) = forall era.
TxBody era
-> TxWits era
-> IsValid
-> StrictMaybe (TxAuxData era)
-> AlonzoTx era
AlonzoTx TxBody ConwayEra
b TxWits ConwayEra
w (Bool -> IsValid
IsValid Bool
iv') StrictMaybe (TxAuxData ConwayEra)
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 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 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 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 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 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 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.
(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
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.
(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.
(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.
(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.
(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.
(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.
  ( EraTx era
  , EraGov era
  ) =>
  WitRule "UTXOW" era ->
  (Result era -> Result era -> Assertion) ->
  UTxO era ->
  PParams era ->
  Tx era ->
  Result era ->
  Assertion
testUTXOWwith :: forall 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.
  ( 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.
(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
-> Maybe EpochNo
-> TxIx
-> PParams era
-> AccountState
-> Bool
-> LedgerEnv era
LedgerEnv (Word64 -> SlotNo
SlotNo Word64
0) forall a. Maybe a
Nothing 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)
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)
x
findMismatch Proof era
Babbage (Babbage.UtxoFailure (AlonzoInBabbageUtxoPredFailure (UtxosFailure x :: PredicateFailure (EraRule "UTXOS" BabbageEra)
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)
x
findMismatch
  Proof era
Conway
  ( Conway.UtxoFailure
      (Conway.UtxosFailure x :: PredicateFailure (EraRule "UTXOS" ConwayEra)
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)
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