{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}

-- ==============================================

module Test.Cardano.Ledger.Constrained.Preds.Tx where

import Cardano.Crypto.Signing (SigningKey)
import Cardano.Ledger.Address (Addr (..), BootstrapAddress, RewardAccount (..))
import Cardano.Ledger.Alonzo.Scripts (AlonzoScript (..), ExUnits (..), plutusScriptLanguage, toAsIx)
import Cardano.Ledger.Alonzo.Tx (IsValid (..))
import Cardano.Ledger.Alonzo.TxWits (TxDats (..))
import Cardano.Ledger.Alonzo.UTxO (getInputDataHashesTxBody)
import Cardano.Ledger.Api (setMinFeeTxUtxo)
import Cardano.Ledger.Babbage.UTxO (getReferenceScripts)
import Cardano.Ledger.BaseTypes (Network (..), ProtVer (..), strictMaybeToMaybe)
import Cardano.Ledger.Binary.Decoding (mkSized, sizedSize)
import Cardano.Ledger.Binary.Encoding (EncCBOR)
import Cardano.Ledger.Coin (Coin (..), rationalToCoinViaCeiling)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.DRep (drepDepositL)
import Cardano.Ledger.Hashes (GenDelegPair (..), GenDelegs (..))
import Cardano.Ledger.Keys (WitVKey (..), asWitness, coerceKeyRole)
import Cardano.Ledger.Keys.Bootstrap (BootstrapWitness)
import Cardano.Ledger.Mary.Value (AssetName, MaryValue (..), MultiAsset (..), PolicyID (..))
import Cardano.Ledger.Plutus.Data (Data (..))
import Cardano.Ledger.Plutus.Language (Language (..))
import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody)
import Cardano.Ledger.Shelley.LedgerState (LedgerState, NewEpochState)
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..))
import Cardano.Ledger.Shelley.TxCert (isInstantaneousRewards)
import Cardano.Ledger.State hiding (delegations, rewards)
import Cardano.Ledger.TxIn (TxIn (..))
import qualified Cardano.Ledger.UMap as UMap
import Cardano.Ledger.Val (Val (..), inject)
import Control.Monad (join, when)
import Control.State.Transition.Extended (STS (..), TRC (..))
import Data.Default (Default (def))
import Data.Foldable as F (foldl', toList)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.Ratio ((%))
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Text (Text, pack)
import qualified Data.VMap as VMap
import Data.Word (Word64)
import GHC.Stack (HasCallStack)
import Lens.Micro
import Test.Cardano.Ledger.Constrained.Ast
import Test.Cardano.Ledger.Constrained.Classes
import Test.Cardano.Ledger.Constrained.Env
import Test.Cardano.Ledger.Constrained.Lenses (fstL, sndL)
import Test.Cardano.Ledger.Constrained.Monad (
  Typed,
  errorTyped,
  failT,
  generateWithSeed,
  monadTyped,
 )
import Test.Cardano.Ledger.Constrained.Preds.CertState (dstateStage, pstateStage, vstateStage)
import qualified Test.Cardano.Ledger.Constrained.Preds.CertState as CertState
import Test.Cardano.Ledger.Constrained.Preds.Certs (certsStage)
import qualified Test.Cardano.Ledger.Constrained.Preds.Certs as Certs
import Test.Cardano.Ledger.Constrained.Preds.LedgerState (ledgerStateStage)
import qualified Test.Cardano.Ledger.Constrained.Preds.LedgerState as LedgerState
import Test.Cardano.Ledger.Constrained.Preds.NewEpochState (epochStateStage, newEpochStateStage)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import qualified Test.Cardano.Ledger.Constrained.Preds.PParams as PParams
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), goRepl, modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.TxOut (txOutPreds)
import qualified Test.Cardano.Ledger.Constrained.Preds.TxOut as TxOut
import Test.Cardano.Ledger.Constrained.Preds.UTxO (utxoStage)
import Test.Cardano.Ledger.Constrained.Preds.Universes hiding (demo, demoTest, main)
import qualified Test.Cardano.Ledger.Constrained.Preds.Universes as Universes
import Test.Cardano.Ledger.Constrained.Rewrite
import Test.Cardano.Ledger.Constrained.Scripts (sufficientScript)
import Test.Cardano.Ledger.Constrained.Size (Size (..))
import Test.Cardano.Ledger.Constrained.Solver (toolChainSub)
import Test.Cardano.Ledger.Constrained.TypeRep
import Test.Cardano.Ledger.Constrained.Utils (checkForSoundness, testIO)
import Test.Cardano.Ledger.Constrained.Vars hiding (totalAda)
import Test.Cardano.Ledger.Core.KeyPair (KeyPair (..), mkWitnessVKey)
import Test.Cardano.Ledger.Generic.Fields (
  TxBodyField (..),
  TxField (..),
  abstractTx,
  abstractTxBody,
 )
import Test.Cardano.Ledger.Generic.Functions (TotalAda (totalAda), protocolVersion)
import Test.Cardano.Ledger.Generic.GenState (mkRedeemers)
import Test.Cardano.Ledger.Generic.PrettyCore (
  PDoc,
  PrettyA (..),
  pcGenDelegPair,
  pcKeyHash,
  pcLedgerState,
  pcScript,
  pcScriptHash,
  pcTx,
  pcTxBody,
  pcTxBodyField,
  pcTxField,
  pcTxIn,
  pcTxOut,
  ppMap,
  ppRecord,
  ppSafeHash,
  ppString,
  psNewEpochState,
  putDoc,
 )
import Test.Cardano.Ledger.Generic.Proof
import Test.Cardano.Ledger.Generic.TxGen (applySTSByProof)
import Test.Cardano.Ledger.Generic.Updaters (newScriptIntegrityHash)
import Test.QuickCheck
import Test.Tasty (TestTree, defaultMain, testGroup)
import Test.Tasty.QuickCheck (testProperty)

predsTests :: TestTree
predsTests :: TestTree
predsTests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Testing all Stages in the Preds directory"
    [ TestTree
PParams.demoTest
    , TestTree
Universes.demoTest
    , TestTree
TxOut.demoTest
    , TestTree
CertState.demoTest
    , TestTree
Certs.demoTest
    , TestTree
LedgerState.demoTest
    ]

-- ===========================================================

txBodySize :: forall era. Reflect era => TxBody era -> Int
txBodySize :: forall era. Reflect era => TxBody era -> Int
txBodySize TxBody era
txb = Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Sized (TxBody era) -> Int64
forall a. Sized a -> Int64
sizedSize (Version -> TxBody era -> Sized (TxBody era)
forall a. EncCBOR a => Version -> a -> Sized a
mkSized (ProtVer -> Version
pvMajor (Proof era -> ProtVer
forall era. Proof era -> ProtVer
protocolVersion (forall era. Reflect era => Proof era
reify @era))) TxBody era
txb))

byteSize :: forall era a. (EncCBOR a, Reflect era) => Proof era -> a -> Int
byteSize :: forall era a. (EncCBOR a, Reflect era) => Proof era -> a -> Int
byteSize Proof era
_ a
x = Int64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Sized a -> Int64
forall a. Sized a -> Int64
sizedSize (Version -> a -> Sized a
forall a. EncCBOR a => Version -> a -> Sized a
mkSized (ProtVer -> Version
pvMajor (Proof era -> ProtVer
forall era. Proof era -> ProtVer
protocolVersion (forall era. Reflect era => Proof era
reify @era))) a
x))

byteSizeT :: forall era a. (EncCBOR a, Reflect era) => Term era a -> Target era Int
byteSizeT :: forall era a.
(EncCBOR a, Reflect era) =>
Term era a -> Target era Int
byteSizeT Term era a
x = TestName -> (a -> Int) -> RootTarget era Void (a -> Int)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"byteSize" (Proof era -> a -> Int
forall era a. (EncCBOR a, Reflect era) => Proof era -> a -> Int
byteSize (forall era. Reflect era => Proof era
reify @era)) RootTarget era Void (a -> Int) -> Term era a -> Target era Int
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era a
x

-- ===============================================
-- Helpful Lenses

txFL :: Lens' (TxF era) (Tx era)
txFL :: forall era (f :: * -> *).
Functor f =>
(Tx era -> f (Tx era)) -> TxF era -> f (TxF era)
txFL = (TxF era -> Tx era)
-> (TxF era -> Tx era -> TxF era)
-> Lens (TxF era) (TxF era) (Tx era) (Tx era)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (\(TxF Proof era
_ Tx era
x) -> Tx era
x) (\(TxF Proof era
p Tx era
_) Tx era
x -> Proof era -> Tx era -> TxF era
forall era. Proof era -> Tx era -> TxF era
TxF Proof era
p Tx era
x)

-- ================================================
-- Auxiliary functions and Targets

computeFinalFee ::
  EraUTxO era =>
  PParamsF era ->
  TxF era ->
  Map TxIn (TxOutF era) ->
  Coin
computeFinalFee :: forall era.
EraUTxO era =>
PParamsF era -> TxF era -> Map TxIn (TxOutF era) -> Coin
computeFinalFee (PParamsF Proof era
_ PParams era
ppV) (TxF Proof era
_ Tx era
txV) Map TxIn (TxOutF era)
ut = Tx era
newtx Tx era -> Getting Coin (Tx era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. ((TxBody era -> Const Coin (TxBody era))
-> Tx era -> Const Coin (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const Coin (TxBody era))
 -> Tx era -> Const Coin (Tx era))
-> ((Coin -> Const Coin Coin)
    -> TxBody era -> Const Coin (TxBody era))
-> Getting Coin (Tx era) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Coin -> Const Coin Coin) -> TxBody era -> Const Coin (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody era) Coin
feeTxBodyL)
  where
    newtx :: Tx era
newtx = PParams era -> Tx era -> UTxO era -> Tx era
forall era.
EraUTxO era =>
PParams era -> Tx era -> UTxO era -> Tx era
setMinFeeTxUtxo PParams era
ppV Tx era
txV (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
ut)

integrityHash ::
  Era era1 =>
  Proof era1 ->
  Term era2 (PParamsF era1) ->
  Term era2 (Set Language) ->
  Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits)) ->
  Term era2 (Map DataHash (Data era1)) ->
  Target era2 (Maybe ScriptIntegrityHash)
integrityHash :: forall era1 era2.
Era era1 =>
Proof era1
-> Term era2 (PParamsF era1)
-> Term era2 (Set Language)
-> Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits))
-> Term era2 (Map DataHash (Data era1))
-> Target era2 (Maybe ScriptIntegrityHash)
integrityHash Proof era1
p Term era2 (PParamsF era1)
pp Term era2 (Set Language)
langs Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits))
rs Term era2 (Map DataHash (Data era1))
ds = TestName
-> (PParamsF era1
    -> Set Language
    -> Map (PlutusPointerF era1) (Data era1, ExUnits)
    -> Map DataHash (Data era1)
    -> Maybe ScriptIntegrityHash)
-> RootTarget
     era2
     Void
     (PParamsF era1
      -> Set Language
      -> Map (PlutusPointerF era1) (Data era1, ExUnits)
      -> Map DataHash (Data era1)
      -> Maybe ScriptIntegrityHash)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"integrityHash" PParamsF era1
-> Set Language
-> Map (PlutusPointerF era1) (Data era1, ExUnits)
-> Map DataHash (Data era1)
-> Maybe ScriptIntegrityHash
hashfun RootTarget
  era2
  Void
  (PParamsF era1
   -> Set Language
   -> Map (PlutusPointerF era1) (Data era1, ExUnits)
   -> Map DataHash (Data era1)
   -> Maybe ScriptIntegrityHash)
-> Term era2 (PParamsF era1)
-> Target
     era2
     (Set Language
      -> Map (PlutusPointerF era1) (Data era1, ExUnits)
      -> Map DataHash (Data era1)
      -> Maybe ScriptIntegrityHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era2 (PParamsF era1)
pp Target
  era2
  (Set Language
   -> Map (PlutusPointerF era1) (Data era1, ExUnits)
   -> Map DataHash (Data era1)
   -> Maybe ScriptIntegrityHash)
-> Term era2 (Set Language)
-> Target
     era2
     (Map (PlutusPointerF era1) (Data era1, ExUnits)
      -> Map DataHash (Data era1) -> Maybe ScriptIntegrityHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era2 (Set Language)
langs Target
  era2
  (Map (PlutusPointerF era1) (Data era1, ExUnits)
   -> Map DataHash (Data era1) -> Maybe ScriptIntegrityHash)
-> Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits))
-> Target
     era2 (Map DataHash (Data era1) -> Maybe ScriptIntegrityHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits))
rs Target era2 (Map DataHash (Data era1) -> Maybe ScriptIntegrityHash)
-> Term era2 (Map DataHash (Data era1))
-> Target era2 (Maybe ScriptIntegrityHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era2 (Map DataHash (Data era1))
ds
  where
    hashfun :: PParamsF era1
-> Set Language
-> Map (PlutusPointerF era1) (Data era1, ExUnits)
-> Map DataHash (Data era1)
-> Maybe ScriptIntegrityHash
hashfun (PParamsF Proof era1
_ PParams era1
ppp) Set Language
ls Map (PlutusPointerF era1) (Data era1, ExUnits)
r Map DataHash (Data era1)
d =
      let r' :: [(PlutusPurpose AsIx era1, (Data era1, ExUnits))]
r' = [(PlutusPurpose AsIx era1
ptr, (Data era1, ExUnits)
de) | (PlutusPointerF Proof era1
_ PlutusPurpose AsIx era1
ptr, (Data era1, ExUnits)
de) <- Map (PlutusPointerF era1) (Data era1, ExUnits)
-> [(PlutusPointerF era1, (Data era1, ExUnits))]
forall k a. Map k a -> [(k, a)]
Map.toList Map (PlutusPointerF era1) (Data era1, ExUnits)
r]
       in StrictMaybe ScriptIntegrityHash -> Maybe ScriptIntegrityHash
forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe (StrictMaybe ScriptIntegrityHash -> Maybe ScriptIntegrityHash)
-> StrictMaybe ScriptIntegrityHash -> Maybe ScriptIntegrityHash
forall a b. (a -> b) -> a -> b
$
            Proof era1
-> PParams era1
-> [Language]
-> Redeemers era1
-> TxDats era1
-> StrictMaybe ScriptIntegrityHash
forall era.
Proof era
-> PParams era
-> [Language]
-> Redeemers era
-> TxDats era
-> StrictMaybe ScriptIntegrityHash
newScriptIntegrityHash Proof era1
p PParams era1
ppp (Set Language -> [Language]
forall a. Set a -> [a]
Set.toList Set Language
ls) (Proof era1
-> [(PlutusPurpose AsIx era1, (Data era1, ExUnits))]
-> Redeemers era1
forall era.
Proof era
-> [(PlutusPurpose AsIx era, (Data era, ExUnits))] -> Redeemers era
mkRedeemers Proof era1
p [(PlutusPurpose AsIx era1, (Data era1, ExUnits))]
r') (Map DataHash (Data era1) -> TxDats era1
forall era. Era era => Map DataHash (Data era) -> TxDats era
TxDats Map DataHash (Data era1)
d)

-- | "Construct the Scripts Needed to compute the Script Witnesses from the UTxO and the partial TxBody
needT ::
  forall era.
  EraUTxO era =>
  Proof era ->
  Target
    era
    ( TxBodyF era ->
      Map TxIn (TxOutF era) ->
      ScriptsNeededF era
    )
needT :: forall era.
EraUTxO era =>
Proof era
-> Target
     era (TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era)
needT Proof era
proof = TestName
-> (TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era)
-> RootTarget
     era
     Void
     (TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"neededScripts" TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era
needed
  where
    needed :: TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era
    needed :: TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era
needed (TxBodyF Proof era
_ TxBody era
txbodyV) Map TxIn (TxOutF era)
ut = Proof era -> ScriptsNeeded era -> ScriptsNeededF era
forall era. Proof era -> ScriptsNeeded era -> ScriptsNeededF era
ScriptsNeededF Proof era
proof (UTxO era -> TxBody era -> ScriptsNeeded era
forall era.
EraUTxO era =>
UTxO era -> TxBody era -> ScriptsNeeded era
getScriptsNeeded (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
ut) TxBody era
txbodyV)

rdmrPtrsT ::
  AlonzoEraScript era =>
  Target
    era
    ( [(PlutusPurposeF era, ScriptHash)] ->
      Map ScriptHash any ->
      Set (PlutusPointerF era)
    )
rdmrPtrsT :: forall era any.
AlonzoEraScript era =>
Target
  era
  ([(PlutusPurposeF era, ScriptHash)]
   -> Map ScriptHash any -> Set (PlutusPointerF era))
rdmrPtrsT = TestName
-> ([(PlutusPurposeF era, ScriptHash)]
    -> Map ScriptHash any -> Set (PlutusPointerF era))
-> RootTarget
     era
     Void
     ([(PlutusPurposeF era, ScriptHash)]
      -> Map ScriptHash any -> Set (PlutusPointerF era))
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"getRdmrPtrs" [(PlutusPurposeF era, ScriptHash)]
-> Map ScriptHash any -> Set (PlutusPointerF era)
forall era any.
AlonzoEraScript era =>
[(PlutusPurposeF era, ScriptHash)]
-> Map ScriptHash any -> Set (PlutusPointerF era)
getRdmrPtrs

getRdmrPtrs ::
  AlonzoEraScript era =>
  [(PlutusPurposeF era, ScriptHash)] ->
  Map ScriptHash any ->
  Set (PlutusPointerF era)
getRdmrPtrs :: forall era any.
AlonzoEraScript era =>
[(PlutusPurposeF era, ScriptHash)]
-> Map ScriptHash any -> Set (PlutusPointerF era)
getRdmrPtrs [(PlutusPurposeF era, ScriptHash)]
xs Map ScriptHash any
allplutus = (Set (PlutusPointerF era)
 -> (PlutusPurposeF era, ScriptHash) -> Set (PlutusPointerF era))
-> Set (PlutusPointerF era)
-> [(PlutusPurposeF era, ScriptHash)]
-> Set (PlutusPointerF era)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (PlutusPointerF era)
-> (PlutusPurposeF era, ScriptHash) -> Set (PlutusPointerF era)
accum Set (PlutusPointerF era)
forall a. Set a
Set.empty [(PlutusPurposeF era, ScriptHash)]
xs
  where
    accum :: Set (PlutusPointerF era)
-> (PlutusPurposeF era, ScriptHash) -> Set (PlutusPointerF era)
accum Set (PlutusPointerF era)
ans (PlutusPurposeF Proof era
p PlutusPurpose AsIxItem era
sp, ScriptHash
hash)
      | ScriptHash -> Map ScriptHash any -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member ScriptHash
hash Map ScriptHash any
allplutus =
          let ptr :: PlutusPurpose AsIx era
ptr = (forall ix it. AsIxItem ix it -> AsIx ix it)
-> PlutusPurpose AsIxItem era -> PlutusPurpose AsIx era
forall era (g :: * -> * -> *) (f :: * -> * -> *).
AlonzoEraScript era =>
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
forall (g :: * -> * -> *) (f :: * -> * -> *).
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
hoistPlutusPurpose AsIxItem ix it -> AsIx ix it
forall ix it. AsIxItem ix it -> AsIx ix it
toAsIx PlutusPurpose AsIxItem era
sp
           in PlutusPointerF era
-> Set (PlutusPointerF era) -> Set (PlutusPointerF era)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Proof era -> PlutusPurpose AsIx era -> PlutusPointerF era
forall era.
Proof era -> PlutusPurpose AsIx era -> PlutusPointerF era
PlutusPointerF Proof era
p PlutusPurpose AsIx era
ptr) Set (PlutusPointerF era)
ans
      | Bool
otherwise = Set (PlutusPointerF era)
ans

getPlutusDataHashes ::
  (AlonzoEraTxOut era, EraTxBody era, AlonzoEraScript era) =>
  Map TxIn (TxOutF era) ->
  TxBodyF era ->
  Map ScriptHash (ScriptF era) ->
  Set DataHash
getPlutusDataHashes :: forall era.
(AlonzoEraTxOut era, EraTxBody era, AlonzoEraScript era) =>
Map TxIn (TxOutF era)
-> TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash
getPlutusDataHashes Map TxIn (TxOutF era)
ut (TxBodyF Proof era
_ TxBody era
txbodyV) Map ScriptHash (ScriptF era)
m =
  (Set DataHash, Set TxIn) -> Set DataHash
forall a b. (a, b) -> a
fst ((Set DataHash, Set TxIn) -> Set DataHash)
-> (Set DataHash, Set TxIn) -> Set DataHash
forall a b. (a -> b) -> a -> b
$ UTxO era
-> TxBody era -> ScriptsProvided era -> (Set DataHash, Set TxIn)
forall era.
(EraTxBody era, AlonzoEraTxOut era, AlonzoEraScript era) =>
UTxO era
-> TxBody era -> ScriptsProvided era -> (Set DataHash, Set TxIn)
getInputDataHashesTxBody (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
ut) TxBody era
txbodyV (Map ScriptHash (Script era) -> ScriptsProvided era
forall era. Map ScriptHash (Script era) -> ScriptsProvided era
ScriptsProvided ((ScriptF era -> Script era)
-> Map ScriptHash (ScriptF era) -> Map ScriptHash (Script era)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ScriptF era -> Script era
forall era. ScriptF era -> Script era
unScriptF Map ScriptHash (ScriptF era)
m))

bootWitsT ::
  Reflect era =>
  Proof era ->
  Map TxIn (TxOutF era) ->
  TxBodyF era ->
  Map (KeyHash 'Payment) (Addr, SigningKey) ->
  Set BootstrapWitness
bootWitsT :: forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
proof Map TxIn (TxOutF era)
spend (TxBodyF Proof era
_ TxBody era
txb) = Hash HASH EraIndependentTxBody
-> [BootstrapAddress]
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitness Hash HASH EraIndependentTxBody
h [BootstrapAddress]
boots
  where
    boots :: [BootstrapAddress] -- Not every Addr has a BootStrapAddress
    boots :: [BootstrapAddress]
boots = ([BootstrapAddress] -> TxOutF era -> [BootstrapAddress])
-> [BootstrapAddress]
-> Map TxIn (TxOutF era)
-> [BootstrapAddress]
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' [BootstrapAddress] -> TxOutF era -> [BootstrapAddress]
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era) =>
[BootstrapAddress] -> TxOutF era -> [BootstrapAddress]
accum [] Map TxIn (TxOutF era)
spend -- Compute a list of them.
      where
        accum :: [BootstrapAddress] -> TxOutF era -> [BootstrapAddress]
accum [BootstrapAddress]
ans (TxOutF Proof era
_ TxOut era
out) = case TxOut era
out TxOut era -> Getting Addr (TxOut era) Addr -> Addr
forall s a. s -> Getting a s a -> a
^. Getting Addr (TxOut era) Addr
forall era. EraTxOut era => Lens' (TxOut era) Addr
Lens' (TxOut era) Addr
addrTxOutL of
          AddrBootstrap BootstrapAddress
b -> BootstrapAddress
b BootstrapAddress -> [BootstrapAddress] -> [BootstrapAddress]
forall a. a -> [a] -> [a]
: [BootstrapAddress]
ans
          Addr
_ -> [BootstrapAddress]
ans
    h :: Hash HASH EraIndependentTxBody
h = Proof era -> TxBody era -> Hash HASH EraIndependentTxBody
forall era.
Proof era -> TxBody era -> Hash HASH EraIndependentTxBody
hashBody Proof era
proof TxBody era
txb

hashBody :: Proof era -> TxBody era -> Hash HASH EraIndependentTxBody
hashBody :: forall era.
Proof era -> TxBody era -> Hash HASH EraIndependentTxBody
hashBody Proof era
Shelley TxBody era
txb = SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
txb)
hashBody Proof era
Allegra TxBody era
txb = SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
txb)
hashBody Proof era
Mary TxBody era
txb = SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
txb)
hashBody Proof era
Alonzo TxBody era
txb = SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
txb)
hashBody Proof era
Babbage TxBody era
txb = SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
txb)
hashBody Proof era
Conway TxBody era
txb = SafeHash EraIndependentTxBody -> Hash HASH EraIndependentTxBody
forall i. SafeHash i -> Hash HASH i
extractHash (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
txb)

-- =======================================

-- | Get enough GenDeleg KeyHashes to satisfy the quorum constraint.
sufficientGenDelegs :: Map k GenDelegPair -> Set (KeyHash 'Witness)
sufficientGenDelegs :: forall k. Map k GenDelegPair -> Set (KeyHash 'Witness)
sufficientGenDelegs Map k GenDelegPair
gendel =
  [KeyHash 'Witness] -> Set (KeyHash 'Witness)
forall a. Ord a => [a] -> Set a
Set.fromList (Int -> [KeyHash 'Witness] -> [KeyHash 'Witness]
forall a. Int -> [a] -> [a]
take (Word64 -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word64
quorumConstant) (KeyHash 'GenesisDelegate -> KeyHash 'Witness
forall (a :: KeyRole -> *) (r :: KeyRole).
HasKeyRole a =>
a r -> a 'Witness
asWitness (KeyHash 'GenesisDelegate -> KeyHash 'Witness)
-> (GenDelegPair -> KeyHash 'GenesisDelegate)
-> GenDelegPair
-> KeyHash 'Witness
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenDelegPair -> KeyHash 'GenesisDelegate
genDelegKeyHash (GenDelegPair -> KeyHash 'Witness)
-> [GenDelegPair] -> [KeyHash 'Witness]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map k GenDelegPair -> [GenDelegPair]
forall k a. Map k a -> [a]
Map.elems Map k GenDelegPair
gendel))

sufficientTxCert ::
  forall era.
  Reflect era =>
  [TxCertF era] ->
  Map (KeyHash 'Genesis) GenDelegPair ->
  Set (KeyHash 'Witness)
sufficientTxCert :: forall era.
Reflect era =>
[TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness)
sufficientTxCert [TxCertF era]
cs Map (KeyHash 'Genesis) GenDelegPair
gendel = case Proof era -> TxCertWit era
forall era. Proof era -> TxCertWit era
whichTxCert (forall era. Reflect era => Proof era
reify @era) of
  TxCertWit era
TxCertShelleyToBabbage -> (Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness))
-> Set (KeyHash 'Witness)
-> [TxCertF era]
-> Set (KeyHash 'Witness)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness)
accum Set (KeyHash 'Witness)
forall a. Set a
Set.empty [TxCertF era]
cs
    where
      accum :: Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness)
accum Set (KeyHash 'Witness)
ans (TxCertF Proof era
_ TxCert era
cert) =
        if TxCert era -> Bool
forall era.
(ShelleyEraTxCert era, ProtVerAtMost era 8) =>
TxCert era -> Bool
isInstantaneousRewards TxCert era
cert
          then Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness)
ans (Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness)
forall k. Map k GenDelegPair -> Set (KeyHash 'Witness)
sufficientGenDelegs Map (KeyHash 'Genesis) GenDelegPair
gendel)
          else Set (KeyHash 'Witness)
ans
  TxCertWit era
TxCertConwayToConway -> (Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness))
-> Set (KeyHash 'Witness)
-> [TxCertF era]
-> Set (KeyHash 'Witness)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness)
accum Set (KeyHash 'Witness)
forall a. Set a
Set.empty [TxCertF era]
cs
    where
      accum :: Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness)
accum Set (KeyHash 'Witness)
ans (TxCertF Proof era
_ TxCert era
_) = Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness)
ans (Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness)
forall k. Map k GenDelegPair -> Set (KeyHash 'Witness)
sufficientGenDelegs Map (KeyHash 'Genesis) GenDelegPair
gendel)

-- IS THIS RIGHT, DO WE need the  isInstantaneousRewards  TEST?

-- | Compute sufficient set of keys to make the scripts succeed.
--   The script map is the map of all 'needed' scripts. Some of those
--   scripts may NOT be in the 'scriptWits' (those which are reference scripts)
--   but all needed scripts will need to have their KeyHashes added.
sufficientScriptKeys ::
  Proof era ->
  Map ScriptHash (ScriptF era) ->
  Set (KeyHash 'Witness)
sufficientScriptKeys :: forall era.
Proof era -> Map ScriptHash (ScriptF era) -> Set (KeyHash 'Witness)
sufficientScriptKeys Proof era
proof = (Set (KeyHash 'Witness) -> ScriptF era -> Set (KeyHash 'Witness))
-> Set (KeyHash 'Witness)
-> Map ScriptHash (ScriptF era)
-> Set (KeyHash 'Witness)
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' Set (KeyHash 'Witness) -> ScriptF era -> Set (KeyHash 'Witness)
accum Set (KeyHash 'Witness)
forall a. Set a
Set.empty
  where
    accum :: Set (KeyHash 'Witness) -> ScriptF era -> Set (KeyHash 'Witness)
accum Set (KeyHash 'Witness)
ans (ScriptF Proof era
_ Script era
s) = Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness)
ans (Proof era -> Script era -> Set (KeyHash 'Witness)
forall era. Proof era -> Script era -> Set (KeyHash 'Witness)
sufficientScript Proof era
proof Script era
s)

sufficientKeyHashes ::
  Reflect era =>
  Proof era ->
  Map ScriptHash (ScriptF era) ->
  [TxCertF era] ->
  Map (KeyHash 'Genesis) GenDelegPair ->
  Set (KeyHash 'Witness)
sufficientKeyHashes :: forall era.
Reflect era =>
Proof era
-> Map ScriptHash (ScriptF era)
-> [TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
sufficientKeyHashes Proof era
p Map ScriptHash (ScriptF era)
scriptmap [TxCertF era]
cs Map (KeyHash 'Genesis) GenDelegPair
gendel =
  Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union
    (Proof era -> Map ScriptHash (ScriptF era) -> Set (KeyHash 'Witness)
forall era.
Proof era -> Map ScriptHash (ScriptF era) -> Set (KeyHash 'Witness)
sufficientScriptKeys Proof era
p Map ScriptHash (ScriptF era)
scriptmap)
    ([TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness)
forall era.
Reflect era =>
[TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness)
sufficientTxCert [TxCertF era]
cs Map (KeyHash 'Genesis) GenDelegPair
gendel)

-- =======================================

pcUtxo :: Reflect era => Map TxIn (TxOutF era) -> String
pcUtxo :: forall era. Reflect era => Map TxIn (TxOutF era) -> TestName
pcUtxo Map TxIn (TxOutF era)
m = PDoc -> TestName
forall a. Show a => a -> TestName
show (Map TxIn (TxOutF era) -> PDoc
forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc Map TxIn (TxOutF era)
m)

pcUtxoDoc :: Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc :: forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc = (TxIn -> PDoc)
-> (TxOutF era -> PDoc) -> Map TxIn (TxOutF era) -> PDoc
forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap TxIn -> PDoc
pcTxIn (\(TxOutF Proof era
p TxOut era
o) -> Proof era -> TxOut era -> PDoc
forall era. Reflect era => Proof era -> TxOut era -> PDoc
pcTxOut Proof era
p TxOut era
o)

necessaryKeyHashTarget ::
  forall era.
  Reflect era =>
  Term era (TxBodyF era) ->
  Term era (Set (KeyHash 'Witness)) ->
  -- Target era (Set (WitVKey 'Witness ))
  Target era (Set (KeyHash 'Witness))
necessaryKeyHashTarget :: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Target era (Set (KeyHash 'Witness))
necessaryKeyHashTarget Term era (TxBodyF era)
txbodyparam Term era (Set (KeyHash 'Witness))
reqSignersparam =
  TestName
-> (TxBodyF era
    -> Map TxIn (TxOutF era)
    -> Map (KeyHash 'Genesis) GenDelegPair
    -> Set (KeyHash 'Witness)
    -> Set (KeyHash 'Witness))
-> RootTarget
     era
     Void
     (TxBodyF era
      -> Map TxIn (TxOutF era)
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Set (KeyHash 'Witness)
      -> Set (KeyHash 'Witness))
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"keywits" TxBodyF era
-> Map TxIn (TxOutF era)
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness)
forall era.
Reflect era =>
TxBodyF era
-> Map TxIn (TxOutF era)
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness)
necessaryKeyHashes
    RootTarget
  era
  Void
  (TxBodyF era
   -> Map TxIn (TxOutF era)
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Set (KeyHash 'Witness)
   -> Set (KeyHash 'Witness))
-> Term era (TxBodyF era)
-> Target
     era
     (Map TxIn (TxOutF era)
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Set (KeyHash 'Witness)
      -> Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
txbodyparam
    Target
  era
  (Map TxIn (TxOutF era)
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Set (KeyHash 'Witness)
   -> Set (KeyHash 'Witness))
-> Term era (Map TxIn (TxOutF era))
-> Target
     era
     (Map (KeyHash 'Genesis) GenDelegPair
      -> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
forall era. Reflect era => Proof era
reify
    Target
  era
  (Map (KeyHash 'Genesis) GenDelegPair
   -> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness))
-> Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> Target era (Set (KeyHash 'Witness) -> Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
    --  ^$ keymapUniv
    Target era (Set (KeyHash 'Witness) -> Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Target era (Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
reqSignersparam

-- | Compute the needed key witnesses from a transaction body.
--   First find all the key hashes from every use of keys in the transaction
--   Then find the KeyPair's associated with those hashes, then
--   using the hash of the TxBody, turn the KeyPair into a witness.
--   In Eras Shelley to Mary, 'reqsigners' should be empty. In Eras Alonzo to Conway
--   we will need to add the witnesses for the required signer hashes, so they are
--   passed in. To compute the witnsses we need the hash of the TxBody. We will call this function
--   twice. Once when we have constructed the 'tempTxBody' used to estimate the fee, and a second time
--   with 'txBodyTerm' where the fee is correct.
--   The underlying function 'shelleyWitsVKeyNeeded' computes the necesary (but not sufficient)
--   key witnesses. The missing ones have to do with MultiSig (and Timelock) scripts and Mir
--   certificates (ones where 'isInstantaneousRewards' predicate is True). So we have to add these as well.
--   A MultiSig (Timelock) scripts needs witnesses for enough Signature scripts to make it True.
--   MIRCert needs enough witnesses from genDelegs to make the quorum constraint true.
necessaryKeyHashes ::
  forall era.
  Reflect era =>
  TxBodyF era ->
  Map TxIn (TxOutF era) ->
  Map (KeyHash 'Genesis) GenDelegPair ->
  Set (KeyHash 'Witness) -> -- Only in Eras Alonzo To Conway,
  Set (KeyHash 'Witness)
necessaryKeyHashes :: forall era.
Reflect era =>
TxBodyF era
-> Map TxIn (TxOutF era)
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness)
necessaryKeyHashes (TxBodyF Proof era
_ TxBody era
txb) Map TxIn (TxOutF era)
u Map (KeyHash 'Genesis) GenDelegPair
gd Set (KeyHash 'Witness)
reqsigners =
  case forall era. Reflect era => Proof era
reify @era of
    Proof era
Shelley -> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
forall era.
EraUTxO era =>
CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getWitsVKeyNeeded CertState era
certState (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness)
reqsigners
    Proof era
Allegra -> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
forall era.
EraUTxO era =>
CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getWitsVKeyNeeded CertState era
certState (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness)
reqsigners
    Proof era
Mary -> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
forall era.
EraUTxO era =>
CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getWitsVKeyNeeded CertState era
certState (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness)
reqsigners
    Proof era
Alonzo -> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
forall era.
EraUTxO era =>
CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getWitsVKeyNeeded CertState era
certState (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness)
reqsigners
    Proof era
Babbage -> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
forall era.
EraUTxO era =>
CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getWitsVKeyNeeded CertState era
certState (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness)
reqsigners
    Proof era
Conway -> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union (CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
forall era.
EraUTxO era =>
CertState era -> UTxO era -> TxBody era -> Set (KeyHash 'Witness)
getWitsVKeyNeeded CertState era
ConwayCertState ConwayEra
forall a. Default a => a
def (Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness)
reqsigners
  where
    certState :: CertState era
    certState :: CertState era
certState = CertState era
forall a. Default a => a
def CertState era -> (CertState era -> CertState era) -> CertState era
forall a b. a -> (a -> b) -> b
& (DState era -> Identity (DState era))
-> CertState era -> Identity (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Identity (DState era))
 -> CertState era -> Identity (CertState era))
-> ((GenDelegs -> Identity GenDelegs)
    -> DState era -> Identity (DState era))
-> (GenDelegs -> Identity GenDelegs)
-> CertState era
-> Identity (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (GenDelegs -> Identity GenDelegs)
-> DState era -> Identity (DState era)
forall era (f :: * -> *).
Functor f =>
(GenDelegs -> f GenDelegs) -> DState era -> f (DState era)
dsGenDelegsL ((GenDelegs -> Identity GenDelegs)
 -> CertState era -> Identity (CertState era))
-> GenDelegs -> CertState era -> CertState era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ Map (KeyHash 'Genesis) GenDelegPair -> GenDelegs
GenDelegs Map (KeyHash 'Genesis) GenDelegPair
gd

-- ========================================================

makeKeyWitnessTarget ::
  Reflect era =>
  Term era (TxBodyF era) ->
  Term era (Set (KeyHash 'Witness)) ->
  Term era (Set (KeyHash 'Witness)) ->
  Term era (Map ScriptHash (ScriptF era)) ->
  Term era (Map (KeyHash 'Payment) (Addr, SigningKey)) ->
  Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget :: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget Term era (TxBodyF era)
txbparam Term era (Set (KeyHash 'Witness))
necessary Term era (Set (KeyHash 'Witness))
sufficient Term era (Map ScriptHash (ScriptF era))
scripts Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byAdUniv =
  TestName
-> (TxBodyF era
    -> Set (KeyHash 'Witness)
    -> Set (KeyHash 'Witness)
    -> Map (KeyHash 'Witness) (KeyPair 'Witness)
    -> Map ScriptHash (ScriptF era)
    -> Map (KeyHash 'Genesis) GenDelegPair
    -> Map (KeyHash 'Payment) (Addr, SigningKey)
    -> Set (WitVKey 'Witness))
-> RootTarget
     era
     Void
     (TxBodyF era
      -> Set (KeyHash 'Witness)
      -> Set (KeyHash 'Witness)
      -> Map (KeyHash 'Witness) (KeyPair 'Witness)
      -> Map ScriptHash (ScriptF era)
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set (WitVKey 'Witness))
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"makeKeyWitness" TxBodyF era
-> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness)
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> Map ScriptHash (ScriptF era)
-> Map (KeyHash 'Genesis) GenDelegPair
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set (WitVKey 'Witness)
forall era.
Reflect era =>
TxBodyF era
-> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness)
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> Map ScriptHash (ScriptF era)
-> Map (KeyHash 'Genesis) GenDelegPair
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set (WitVKey 'Witness)
makeKeyWitness
    RootTarget
  era
  Void
  (TxBodyF era
   -> Set (KeyHash 'Witness)
   -> Set (KeyHash 'Witness)
   -> Map (KeyHash 'Witness) (KeyPair 'Witness)
   -> Map ScriptHash (ScriptF era)
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set (WitVKey 'Witness))
-> Term era (TxBodyF era)
-> Target
     era
     (Set (KeyHash 'Witness)
      -> Set (KeyHash 'Witness)
      -> Map (KeyHash 'Witness) (KeyPair 'Witness)
      -> Map ScriptHash (ScriptF era)
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set (WitVKey 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
txbparam
    Target
  era
  (Set (KeyHash 'Witness)
   -> Set (KeyHash 'Witness)
   -> Map (KeyHash 'Witness) (KeyPair 'Witness)
   -> Map ScriptHash (ScriptF era)
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set (WitVKey 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Target
     era
     (Set (KeyHash 'Witness)
      -> Map (KeyHash 'Witness) (KeyPair 'Witness)
      -> Map ScriptHash (ScriptF era)
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set (WitVKey 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
necessary
    Target
  era
  (Set (KeyHash 'Witness)
   -> Map (KeyHash 'Witness) (KeyPair 'Witness)
   -> Map ScriptHash (ScriptF era)
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set (WitVKey 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Target
     era
     (Map (KeyHash 'Witness) (KeyPair 'Witness)
      -> Map ScriptHash (ScriptF era)
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set (WitVKey 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
sufficient
    Target
  era
  (Map (KeyHash 'Witness) (KeyPair 'Witness)
   -> Map ScriptHash (ScriptF era)
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set (WitVKey 'Witness))
-> Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
-> Target
     era
     (Map ScriptHash (ScriptF era)
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set (WitVKey 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv
    Target
  era
  (Map ScriptHash (ScriptF era)
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set (WitVKey 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Target
     era
     (Map (KeyHash 'Genesis) GenDelegPair
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set (WitVKey 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map ScriptHash (ScriptF era))
scripts
    Target
  era
  (Map (KeyHash 'Genesis) GenDelegPair
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set (WitVKey 'Witness))
-> Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> Target
     era
     (Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set (WitVKey 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
    Target
  era
  (Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set (WitVKey 'Witness))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byAdUniv

makeKeyWitness ::
  forall era.
  Reflect era =>
  TxBodyF era ->
  Set (KeyHash 'Witness) ->
  Set (KeyHash 'Witness) ->
  Map (KeyHash 'Witness) (KeyPair 'Witness) ->
  Map ScriptHash (ScriptF era) ->
  Map (KeyHash 'Genesis) GenDelegPair ->
  Map (KeyHash 'Payment) (Addr, SigningKey) ->
  Set (WitVKey 'Witness)
makeKeyWitness :: forall era.
Reflect era =>
TxBodyF era
-> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness)
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> Map ScriptHash (ScriptF era)
-> Map (KeyHash 'Genesis) GenDelegPair
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set (WitVKey 'Witness)
makeKeyWitness (TxBodyF Proof era
proof TxBody era
txb) Set (KeyHash 'Witness)
necessary Set (KeyHash 'Witness)
sufficient Map (KeyHash 'Witness) (KeyPair 'Witness)
keyUniv Map ScriptHash (ScriptF era)
scripts Map (KeyHash 'Genesis) GenDelegPair
gendel Map (KeyHash 'Payment) (Addr, SigningKey)
byronAdUniv = Set (WitVKey 'Witness)
keywits
  where
    bodyhash :: SafeHash EraIndependentTxBody
    bodyhash :: SafeHash EraIndependentTxBody
bodyhash = TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
txb
    keywits :: Set (WitVKey 'Witness)
keywits = (Set (WitVKey 'Witness)
 -> KeyHash 'Witness -> Set (WitVKey 'Witness))
-> Set (WitVKey 'Witness)
-> Set (KeyHash 'Witness)
-> Set (WitVKey 'Witness)
forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' Set (WitVKey 'Witness)
-> KeyHash 'Witness -> Set (WitVKey 'Witness)
accum Set (WitVKey 'Witness)
forall a. Set a
Set.empty (Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness) -> Set (KeyHash 'Witness)
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness)
necessary Set (KeyHash 'Witness)
sufficient)
      where
        accum :: Set (WitVKey 'Witness)
-> KeyHash 'Witness -> Set (WitVKey 'Witness)
accum Set (WitVKey 'Witness)
ans KeyHash 'Witness
hash = case KeyHash 'Witness
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> Maybe (KeyPair 'Witness)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Witness
hash Map (KeyHash 'Witness) (KeyPair 'Witness)
keyUniv of
          Just KeyPair 'Witness
keypair -> WitVKey 'Witness
-> Set (WitVKey 'Witness) -> Set (WitVKey 'Witness)
forall a. Ord a => a -> Set a -> Set a
Set.insert (SafeHash EraIndependentTxBody
-> KeyPair 'Witness -> WitVKey 'Witness
forall (kr :: KeyRole).
SafeHash EraIndependentTxBody -> KeyPair kr -> WitVKey 'Witness
mkWitnessVKey SafeHash EraIndependentTxBody
bodyhash KeyPair 'Witness
keypair) Set (WitVKey 'Witness)
ans
          Maybe (KeyPair 'Witness)
Nothing -> case KeyHash 'Payment
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Maybe (Addr, SigningKey)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (KeyHash 'Witness -> KeyHash 'Payment
forall (r :: KeyRole) (r' :: KeyRole). KeyHash r -> KeyHash r'
forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole KeyHash 'Witness
hash) Map (KeyHash 'Payment) (Addr, SigningKey)
byronAdUniv of
            Just (AddrBootstrap BootstrapAddress
_, SigningKey
_) -> Set (WitVKey 'Witness)
ans -- Bootstrap witnesses are handled in bootWitsT, so we can ignore them here.
            Maybe (Addr, SigningKey)
_ ->
              TestName -> Set (WitVKey 'Witness)
forall a. HasCallStack => TestName -> a
error
                ( TestName
"hash not in keymapUniv or byronAddrUniv"
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ KeyHash 'Witness -> TestName
forall a. Show a => a -> TestName
show KeyHash 'Witness
hash
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\n member necessary = "
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Bool -> TestName
forall a. Show a => a -> TestName
show (KeyHash 'Witness -> Set (KeyHash 'Witness) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member KeyHash 'Witness
hash Set (KeyHash 'Witness)
necessary)
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\n member sufficient = "
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Bool -> TestName
forall a. Show a => a -> TestName
show (KeyHash 'Witness -> Set (KeyHash 'Witness) -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member KeyHash 'Witness
hash Set (KeyHash 'Witness)
sufficient)
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\n scripts = "
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ PDoc -> TestName
forall a. Show a => a -> TestName
show ((ScriptHash -> PDoc)
-> (ScriptF era -> PDoc) -> Map ScriptHash (ScriptF era) -> PDoc
forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap ScriptHash -> PDoc
pcScriptHash (\(ScriptF Proof era
p Script era
s) -> Proof era -> Script era -> PDoc
forall era. Reflect era => Proof era -> Script era -> PDoc
pcScript Proof era
p Script era
s) Map ScriptHash (ScriptF era)
scripts)
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\n genDelegs = "
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ PDoc -> TestName
forall a. Show a => a -> TestName
show ((KeyHash 'Genesis -> PDoc)
-> (GenDelegPair -> PDoc)
-> Map (KeyHash 'Genesis) GenDelegPair
-> PDoc
forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap KeyHash 'Genesis -> PDoc
forall (discriminator :: KeyRole). KeyHash discriminator -> PDoc
pcKeyHash GenDelegPair -> PDoc
pcGenDelegPair Map (KeyHash 'Genesis) GenDelegPair
gendel)
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\nbyronAddrUniv\n"
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ forall era t. Rep era t -> t -> TestName
format @era (Rep era (KeyHash 'Payment)
-> Rep era (Addr, SigningKey)
-> Rep era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era (KeyHash 'Payment)
forall era. Era era => Rep era (KeyHash 'Payment)
PayHashR (Rep era Addr -> Rep era SigningKey -> Rep era (Addr, SigningKey)
forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR Rep era Addr
forall era. Era era => Rep era Addr
AddrR Rep era SigningKey
forall era. Rep era SigningKey
SigningKeyR)) Map (KeyHash 'Payment) (Addr, SigningKey)
byronAdUniv
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\nTxBody =\n"
                    TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ PDoc -> TestName
forall a. Show a => a -> TestName
show (Proof era -> TxBody era -> PDoc
forall era. Proof era -> TxBody era -> PDoc
pcTxBody Proof era
proof TxBody era
txb)
                )

-- ===============================================

allValid :: [IsValid] -> IsValid
allValid :: [IsValid] -> IsValid
allValid [IsValid]
xs = Bool -> IsValid
IsValid ((IsValid -> Bool) -> [IsValid] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all IsValid -> Bool
valid [IsValid]
xs)
  where
    valid :: IsValid -> Bool
valid (IsValid Bool
b) = Bool
b

scriptWitsLangs :: Map k (ScriptF era) -> Set Language
scriptWitsLangs :: forall k era. Map k (ScriptF era) -> Set Language
scriptWitsLangs = (Set Language -> ScriptF era -> Set Language)
-> Set Language -> Map k (ScriptF era) -> Set Language
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' Set Language -> ScriptF era -> Set Language
forall era. Set Language -> ScriptF era -> Set Language
accum Set Language
forall a. Set a
Set.empty
  where
    accum :: Set Language -> ScriptF era -> Set Language
    accum :: forall era. Set Language -> ScriptF era -> Set Language
accum Set Language
ans (ScriptF Proof era
Alonzo (PlutusScript PlutusScript AlonzoEra
ps)) = Language -> Set Language -> Set Language
forall a. Ord a => a -> Set a -> Set a
Set.insert (PlutusScript AlonzoEra -> Language
forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript AlonzoEra
ps) Set Language
ans
    accum Set Language
ans (ScriptF Proof era
Babbage (PlutusScript PlutusScript BabbageEra
ps)) = Language -> Set Language -> Set Language
forall a. Ord a => a -> Set a -> Set a
Set.insert (PlutusScript BabbageEra -> Language
forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript BabbageEra
ps) Set Language
ans
    accum Set Language
ans (ScriptF Proof era
Conway (PlutusScript PlutusScript ConwayEra
ps)) = Language -> Set Language -> Set Language
forall a. Ord a => a -> Set a -> Set a
Set.insert (PlutusScript ConwayEra -> Language
forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript ConwayEra
ps) Set Language
ans
    accum Set Language
ans ScriptF era
_ = Set Language
ans

-- | Starting in the Babbage era, we can adjust the script witnesses by not supplying
--   those that appear as a reference script in the UTxO resolved 'spending' inputs.
--   {- neededHashes − dom(refScripts tx utxo) = dom(txwitscripts txw) -}
--   This function computes the exact set of hashes that must appear in the witnesses.
adjustNeededByRefScripts ::
  Proof era ->
  Set TxIn ->
  Set TxIn ->
  Map TxIn (TxOutF era) ->
  Set ScriptHash ->
  Set ScriptHash
adjustNeededByRefScripts :: forall era.
Proof era
-> Set TxIn
-> Set TxIn
-> Map TxIn (TxOutF era)
-> Set ScriptHash
-> Set ScriptHash
adjustNeededByRefScripts Proof era
proof Set TxIn
inps Set TxIn
refinps Map TxIn (TxOutF era)
ut Set ScriptHash
neededhashes = case Proof era -> TxOutWit era
forall era. Proof era -> TxOutWit era
whichTxOut Proof era
proof of
  TxOutWit era
TxOutShelleyToMary -> Set ScriptHash
neededhashes
  TxOutWit era
TxOutAlonzoToAlonzo -> Set ScriptHash
neededhashes
  TxOutWit era
TxOutBabbageToConway ->
    let spendUtxo :: UTxO era
spendUtxo = Map TxIn (TxOutF era) -> UTxO era
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
ut
     in Set ScriptHash -> Set ScriptHash -> Set ScriptHash
forall a. Ord a => Set a -> Set a -> Set a
Set.difference
          Set ScriptHash
neededhashes
          ( Set ScriptHash -> Set ScriptHash -> Set ScriptHash
forall a. Ord a => Set a -> Set a -> Set a
Set.union
              (Map ScriptHash (Script era) -> Set ScriptHash
forall k a. Map k a -> Set k
Map.keysSet (UTxO era -> Set TxIn -> Map ScriptHash (Script era)
forall era.
BabbageEraTxOut era =>
UTxO era -> Set TxIn -> Map ScriptHash (Script era)
getReferenceScripts UTxO era
spendUtxo Set TxIn
inps))
              (Map ScriptHash (Script era) -> Set ScriptHash
forall k a. Map k a -> Set k
Map.keysSet (UTxO era -> Set TxIn -> Map ScriptHash (Script era)
forall era.
BabbageEraTxOut era =>
UTxO era -> Set TxIn -> Map ScriptHash (Script era)
getReferenceScripts UTxO era
spendUtxo Set TxIn
refinps))
          )

-- ==============================================================

getUtxoCoinT ::
  Reflect era =>
  Term era TxIn ->
  Term era (Map TxIn (TxOutF era)) ->
  Target era Coin
getUtxoCoinT :: forall era.
Reflect era =>
Term era TxIn
-> Term era (Map TxIn (TxOutF era)) -> Target era Coin
getUtxoCoinT Term era TxIn
feeinput Term era (Map TxIn (TxOutF era))
spending = TestName
-> (TxIn -> Map TxIn (TxOutF era) -> Coin)
-> RootTarget era Void (TxIn -> Map TxIn (TxOutF era) -> Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"getUtxoCoin" TxIn -> Map TxIn (TxOutF era) -> Coin
forall {era} {k}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era, Ord k) =>
k -> Map k (TxOutF era) -> Coin
getUtxoCoin RootTarget era Void (TxIn -> Map TxIn (TxOutF era) -> Coin)
-> Term era TxIn -> Target era (Map TxIn (TxOutF era) -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era TxIn
feeinput Target era (Map TxIn (TxOutF era) -> Coin)
-> Term era (Map TxIn (TxOutF era)) -> Target era Coin
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
spending
  where
    getUtxoCoin :: k -> Map k (TxOutF era) -> Coin
getUtxoCoin k
input Map k (TxOutF era)
mp = case k -> Map k (TxOutF era) -> Maybe (TxOutF era)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
input Map k (TxOutF era)
mp of
      Just (TxOutF Proof era
_ TxOut era
txout) -> TxOut era
txout TxOut era -> Getting Coin (TxOut era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxOut era) Coin
forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
Lens' (TxOut era) Coin
coinTxOutL
      Maybe (TxOutF era)
Nothing -> TestName -> Coin
forall a. HasCallStack => TestName -> a
error TestName
"feeinput not in spending"

getNTxOut :: (HasCallStack, Reflect era) => Size -> TxOutF era -> [TxOutF era] -> [TxOutF era]
getNTxOut :: forall era.
(HasCallStack, Reflect era) =>
Size -> TxOutF era -> [TxOutF era] -> [TxOutF era]
getNTxOut (SzExact Int
n) TxOutF era
feeoutput [TxOutF era]
outputuniv =
  (TxOutF era
feeoutput TxOutF era -> (TxOutF era -> TxOutF era) -> TxOutF era
forall a b. a -> (a -> b) -> b
& (Coin -> Identity Coin) -> TxOutF era -> Identity (TxOutF era)
forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
Lens' (TxOutF era) Coin
outputCoinL ((Coin -> Identity Coin) -> TxOutF era -> Identity (TxOutF era))
-> Coin -> TxOutF era -> TxOutF era
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Integer -> Coin
Coin Integer
1000000)) TxOutF era -> [TxOutF era] -> [TxOutF era]
forall a. a -> [a] -> [a]
: Int -> [TxOutF era] -> [TxOutF era]
forall a. Int -> [a] -> [a]
take (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) [TxOutF era]
outputuniv
getNTxOut Size
x TxOutF era
_ [TxOutF era]
_ =
  TestName -> [TxOutF era]
forall a. HasCallStack => TestName -> a
error
    ( TestName
"Non (SzExact n): "
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Size -> TestName
forall a. Show a => a -> TestName
show Size
x
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
" in getNTxOut. Use (MetaSize size x) to get a random (SzExact n)."
    )

-- | Compute the sum of all the Values in a List(Set,Map, ...) of TxOut
txoutSum :: forall era t. (Foldable t, Reflect era) => t (TxOutF era) -> Value era
txoutSum :: forall era (t :: * -> *).
(Foldable t, Reflect era) =>
t (TxOutF era) -> Value era
txoutSum t (TxOutF era)
xs = (Value era -> TxOutF era -> Value era)
-> Value era -> t (TxOutF era) -> Value era
forall b a. (b -> a -> b) -> b -> t a -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Value era -> TxOutF era -> Value era
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era) =>
Value era -> TxOutF era -> Value era
accum Value era
forall a. Monoid a => a
mempty t (TxOutF era)
xs
  where
    accum :: Value era -> TxOutF era -> Value era
accum Value era
ans (TxOutF Proof era
_ TxOut era
txout) = TxOut era
txout TxOut era
-> Getting (Value era) (TxOut era) (Value era) -> Value era
forall s a. s -> Getting a s a -> a
^. Getting (Value era) (TxOut era) (Value era)
forall era. EraTxOut era => Lens' (TxOut era) (Value era)
Lens' (TxOut era) (Value era)
valueTxOutL Value era -> Value era -> Value era
forall t. Val t => t -> t -> t
<+> Value era
ans

minusMultiValue ::
  forall era.
  Proof era ->
  Value era ->
  Value era ->
  Map ScriptHash (Map AssetName Integer)
minusMultiValue :: forall era.
Proof era
-> Value era -> Value era -> Map ScriptHash (Map AssetName Integer)
minusMultiValue Proof era
p Value era
v1 Value era
v2 = case Proof era -> ValueWit era
forall era. Proof era -> ValueWit era
whichValue Proof era
p of
  ValueWit era
ValueMaryToConway -> case Value era
MaryValue
v1 MaryValue -> MaryValue -> MaryValue
forall t. Val t => t -> t -> t
<-> Value era
MaryValue
v2 of MaryValue Coin
_ (MultiAsset Map PolicyID (Map AssetName Integer)
m) -> (PolicyID -> ScriptHash)
-> Map PolicyID (Map AssetName Integer)
-> Map ScriptHash (Map AssetName Integer)
forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\(PolicyID ScriptHash
x) -> ScriptHash
x) Map PolicyID (Map AssetName Integer)
m
  ValueWit era
ValueShelleyToAllegra -> Map ScriptHash (Map AssetName Integer)
forall a. Monoid a => a
mempty

-- ==============================================================
-- Using constraints to generate a TxBody
-- ==============================================================

txBodyPreds :: forall era. (HasCallStack, Reflect era) => UnivSize -> Proof era -> [Pred era]
txBodyPreds :: forall era.
(HasCallStack, Reflect era) =>
UnivSize -> Proof era -> [Pred era]
txBodyPreds sizes :: UnivSize
sizes@UnivSize {Bool
Int
usNumTxOuts :: Int
usMaxAssets :: Int
usMaxPolicyID :: Int
usNumMultiAsset :: Int
usNumPtr :: Int
usNumAddr :: Int
usNumKeys :: Int
usNumPools :: Int
usNumStakeKeys :: Int
usNumGenesisKeys :: Int
usNumVoteKeys :: Int
usNumCredentials :: Int
usNumDatums :: Int
usNumTxIn :: Int
usNumPreUtxo :: Int
usNumColUtxo :: Int
usNumDReps :: Int
usMinCerts :: Int
usMaxCerts :: Int
usDatumFreq :: Int
usGenerateWithdrawals :: Bool
usMinInputs :: Int
usMaxInputs :: Int
usMinCollaterals :: Int
usMaxCollaterals :: Int
usRegKeyFreq :: Int
usUnRegKeyFreq :: Int
usAllowReRegisterPool :: Bool
usSpendScriptFreq :: Int
usCredScriptFreq :: Int
usNumTxOuts :: UnivSize -> Int
usMaxAssets :: UnivSize -> Int
usMaxPolicyID :: UnivSize -> Int
usNumMultiAsset :: UnivSize -> Int
usNumPtr :: UnivSize -> Int
usNumAddr :: UnivSize -> Int
usNumKeys :: UnivSize -> Int
usNumPools :: UnivSize -> Int
usNumStakeKeys :: UnivSize -> Int
usNumGenesisKeys :: UnivSize -> Int
usNumVoteKeys :: UnivSize -> Int
usNumCredentials :: UnivSize -> Int
usNumDatums :: UnivSize -> Int
usNumTxIn :: UnivSize -> Int
usNumPreUtxo :: UnivSize -> Int
usNumColUtxo :: UnivSize -> Int
usNumDReps :: UnivSize -> Int
usMinCerts :: UnivSize -> Int
usMaxCerts :: UnivSize -> Int
usDatumFreq :: UnivSize -> Int
usGenerateWithdrawals :: UnivSize -> Bool
usMinInputs :: UnivSize -> Int
usMaxInputs :: UnivSize -> Int
usMinCollaterals :: UnivSize -> Int
usMaxCollaterals :: UnivSize -> Int
usRegKeyFreq :: UnivSize -> Int
usUnRegKeyFreq :: UnivSize -> Int
usAllowReRegisterPool :: UnivSize -> Bool
usSpendScriptFreq :: UnivSize -> Int
usCredScriptFreq :: UnivSize -> Int
..} Proof era
p =
  UnivSize
-> Proof era
-> Term era Coin
-> Term era [TxOutF era]
-> [Pred era]
forall era.
Reflect era =>
UnivSize
-> Proof era
-> Term era Coin
-> Term era [TxOutF era]
-> [Pred era]
txOutPreds UnivSize
sizes Proof era
p Term era Coin
balanceCoin (Proof era -> Term era [TxOutF era]
forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof era
p)
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ [ Term era (Map ScriptHash (Map AssetName Integer))
forall era.
Era era =>
Term era (Map ScriptHash (Map AssetName Integer))
mint
           Term era (Map ScriptHash (Map AssetName Integer))
-> RootTarget era Void (Map ScriptHash (Map AssetName Integer))
-> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( TestName
-> ([TxOutF era]
    -> Map TxIn (TxOutF era) -> Map ScriptHash (Map AssetName Integer))
-> RootTarget
     era
     Void
     ([TxOutF era]
      -> Map TxIn (TxOutF era) -> Map ScriptHash (Map AssetName Integer))
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"sumAssets" (\[TxOutF era]
out Map TxIn (TxOutF era)
spend -> Proof era
-> Value era -> Value era -> Map ScriptHash (Map AssetName Integer)
forall era.
Proof era
-> Value era -> Value era -> Map ScriptHash (Map AssetName Integer)
minusMultiValue Proof era
p ([TxOutF era] -> Value era
forall era (t :: * -> *).
(Foldable t, Reflect era) =>
t (TxOutF era) -> Value era
txoutSum [TxOutF era]
out) (Map TxIn (TxOutF era) -> Value era
forall era (t :: * -> *).
(Foldable t, Reflect era) =>
t (TxOutF era) -> Value era
txoutSum Map TxIn (TxOutF era)
spend))
                    RootTarget
  era
  Void
  ([TxOutF era]
   -> Map TxIn (TxOutF era) -> Map ScriptHash (Map AssetName Integer))
-> Term era [TxOutF era]
-> Target
     era
     (Map TxIn (TxOutF era) -> Map ScriptHash (Map AssetName Integer))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era [TxOutF era]
forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof era
p
                    Target
  era
  (Map TxIn (TxOutF era) -> Map ScriptHash (Map AssetName Integer))
-> Term era (Map TxIn (TxOutF era))
-> RootTarget era Void (Map ScriptHash (Map AssetName Integer))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
spending
                )
       , Term era (Maybe Network)
forall era. Era era => Term era (Maybe Network)
networkID Term era (Maybe Network)
-> RootTarget era Void (Maybe Network) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era Network -> RootTarget era Void (Maybe Network)
forall era t. Term era t -> Target era (Maybe t)
justTarget Term era Network
forall era. Era era => Term era Network
network
       , -- inputs
         Term era Size -> Term era (Set TxIn) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
usMinInputs Int
usMaxInputs) Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
inputs
       , Direct (Term era TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era TxIn -> Direct (Term era TxIn)
forall a b. a -> Either a b
Left Term era TxIn
forall era. Era era => Term era TxIn
feeTxIn) Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
inputs
       , Term era (Set TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
inputs (Term era (Map TxIn (TxOutF era)) -> Term era (Set TxIn)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p))
       , -- collateral
         Term era (Set TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
inputs Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
collateral
       , Term era Size -> Term era (Set TxIn) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
usMinCollaterals Int
usMaxCollaterals) Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
collateral
       , Term era (Set TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
collateral (Term era (Map TxIn (TxOutF era)) -> Term era (Set TxIn)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
colUtxo)
       , --       , Member (Left colInput) collateral
         Term era (Map TxIn (TxOutF era))
colRestriction Term era (Map TxIn (TxOutF era))
-> Term era (Map TxIn (TxOutF era)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Set TxIn)
-> Term era (Map TxIn (TxOutF era))
-> Term era (Map TxIn (TxOutF era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
collateral Term era (Map TxIn (TxOutF era))
colUtxo
       , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) Term era Coin
forall era. Era era => Term era Coin
sumCol OrdCond
EQL [Rep era Coin
-> Lens' (TxOutF era) Coin
-> Term era (Map TxIn (TxOutF era))
-> Sum era Coin
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era Coin
forall era. Rep era Coin
CoinR (Coin -> f Coin) -> TxOutF era -> f (TxOutF era)
forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
Lens' (TxOutF era) Coin
outputCoinL Term era (Map TxIn (TxOutF era))
colRestriction]
       , Term era Coin
tempTotalCol Term era Coin -> Term era Coin -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era Coin
forall era. Era era => Term era Coin
sumCol
       , -- withdrawals
         Term era Size -> Term era (Set (Credential 'Staking)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
2) Term era (Set (Credential 'Staking))
prewithdrawal
       , Term era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (Credential 'Staking))
prewithdrawal (Term era (Map (Credential 'Staking) Coin)
-> Term era (Set (Credential 'Staking))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
nonZeroRewards)
       , if Bool
usGenerateWithdrawals
           then
             Term era (Map RewardAccount Coin)
forall era. Era era => Term era (Map RewardAccount Coin)
withdrawals
               Term era (Map RewardAccount Coin)
-> RootTarget era Void (Map RewardAccount Coin) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( TestName
-> (Set (Credential 'Staking)
    -> Map (Credential 'Staking) Coin -> Map RewardAccount Coin)
-> RootTarget
     era
     Void
     (Set (Credential 'Staking)
      -> Map (Credential 'Staking) Coin -> Map RewardAccount Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr
                        TestName
"mkRwrdAcnt"
                        ( \Set (Credential 'Staking)
s Map (Credential 'Staking) Coin
r ->
                            [(RewardAccount, Coin)] -> Map RewardAccount Coin
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                              ( (Credential 'Staking -> (RewardAccount, Coin))
-> [Credential 'Staking] -> [(RewardAccount, Coin)]
forall a b. (a -> b) -> [a] -> [b]
map
                                  (\Credential 'Staking
x -> (Network -> Credential 'Staking -> RewardAccount
RewardAccount Network
Testnet Credential 'Staking
x, Map (Credential 'Staking) Coin
r Map (Credential 'Staking) Coin -> Credential 'Staking -> Coin
forall k a. Ord k => Map k a -> k -> a
Map.! Credential 'Staking
x))
                                  (Set (Credential 'Staking) -> [Credential 'Staking]
forall a. Set a -> [a]
Set.toList Set (Credential 'Staking)
s)
                              )
                        )
                        RootTarget
  era
  Void
  (Set (Credential 'Staking)
   -> Map (Credential 'Staking) Coin -> Map RewardAccount Coin)
-> Term era (Set (Credential 'Staking))
-> Target
     era (Map (Credential 'Staking) Coin -> Map RewardAccount Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (Credential 'Staking))
prewithdrawal
                        Target
  era (Map (Credential 'Staking) Coin -> Map RewardAccount Coin)
-> Term era (Map (Credential 'Staking) Coin)
-> RootTarget era Void (Map RewardAccount Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards
                    )
           else Term era Size -> Term era (Map RewardAccount Coin) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
0) Term era (Map RewardAccount Coin)
forall era. Era era => Term era (Map RewardAccount Coin)
withdrawals
       , Term era (Map (Credential 'Staking) Coin)
nonZeroRewards Term era (Map (Credential 'Staking) Coin)
-> RootTarget era Void (Map (Credential 'Staking) Coin) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Map (Credential 'Staking) Coin
    -> Map (Credential 'Staking) Coin)
-> RootTarget
     era
     Void
     (Map (Credential 'Staking) Coin -> Map (Credential 'Staking) Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"filter (/=0)" ((Coin -> Bool)
-> Map (Credential 'Staking) Coin -> Map (Credential 'Staking) Coin
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Coin -> Coin -> Bool
forall a. Eq a => a -> a -> Bool
/= (Integer -> Coin
Coin Integer
0))) RootTarget
  era
  Void
  (Map (Credential 'Staking) Coin -> Map (Credential 'Staking) Coin)
-> Term era (Map (Credential 'Staking) Coin)
-> RootTarget era Void (Map (Credential 'Staking) Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
rewards)
       , -- refInputs
         Term era Size -> Term era (Set TxIn) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
1) Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
refInputs
       , Term era (Set TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
refInputs (Term era (Map TxIn (TxOutF era)) -> Term era (Set TxIn)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p))
       , Term era TxIn -> Term era (Set TxIn) -> Pred era
forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember Term era TxIn
forall era. Era era => Term era TxIn
feeTxIn Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
refInputs
       , Term era (Set TxIn) -> Term era (Set TxIn) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
refInputs Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
inputs -- New constraint in Conway, added PR #4024
       , Term era Size -> Term era (Set (KeyHash 'Witness)) -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Int -> Term era Size
forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
2) Term era (Set (KeyHash 'Witness))
forall era. Era era => Term era (Set (KeyHash 'Witness))
reqSignerHashes
       , Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness)) -> Pred era
forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (KeyHash 'Witness))
forall era. Era era => Term era (Set (KeyHash 'Witness))
reqSignerHashes (Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
-> Term era (Set (KeyHash 'Witness))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)
       , Term era SlotNo
forall era. Era era => Term era SlotNo
ttl Term era SlotNo -> RootTarget era Void SlotNo -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (SlotNo -> SlotNo) -> RootTarget era Void (SlotNo -> SlotNo)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"(+5)" (SlotNo -> SlotNo -> SlotNo
forall a. Num a => a -> a -> a
+ SlotNo
5) RootTarget era Void (SlotNo -> SlotNo)
-> Term era SlotNo -> RootTarget era Void SlotNo
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era SlotNo
forall era. Era era => Term era SlotNo
currentSlot)
       , Term era (Map TxIn (TxOutF era))
spending Term era (Map TxIn (TxOutF era))
-> Term era (Map TxIn (TxOutF era)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Set TxIn)
-> Term era (Map TxIn (TxOutF era))
-> Term era (Map TxIn (TxOutF era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
inputs (Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p)
       , Direct Coin
-> Term era Coin -> OrdCond -> [Sum era Coin] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
           (Coin -> Direct Coin
forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
           Term era Coin
balanceCoin
           OrdCond
EQL
           [Rep era Coin
-> Lens' (TxOutF era) Coin
-> Term era (Map TxIn (TxOutF era))
-> Sum era Coin
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era Coin
forall era. Rep era Coin
CoinR (Coin -> f Coin) -> TxOutF era -> f (TxOutF era)
forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
Lens' (TxOutF era) Coin
outputCoinL Term era (Map TxIn (TxOutF era))
spending, Term era (Map RewardAccount Coin) -> Sum era Coin
forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap Term era (Map RewardAccount Coin)
forall era. Era era => Term era (Map RewardAccount Coin)
withdrawals, Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
txrefunds, Term era Coin -> Sum era Coin
forall era c. Term era c -> Sum era c
One Term era Coin
txdeposits]
       , Term era Coin
txrefunds
           Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( TestName
-> (PParamsF era
    -> Map (Credential 'Staking) Coin
    -> Map (Credential 'DRepRole) Coin
    -> [TxCertF era]
    -> Coin)
-> RootTarget
     era
     Void
     (PParamsF era
      -> Map (Credential 'Staking) Coin
      -> Map (Credential 'DRepRole) Coin
      -> [TxCertF era]
      -> Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"certsRefunds" PParamsF era
-> Map (Credential 'Staking) Coin
-> Map (Credential 'DRepRole) Coin
-> [TxCertF era]
-> Coin
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxCert era) =>
PParamsF era
-> Map (Credential 'Staking) Coin
-> Map (Credential 'DRepRole) Coin
-> [TxCertF era]
-> Coin
certsRefunds
                    RootTarget
  era
  Void
  (PParamsF era
   -> Map (Credential 'Staking) Coin
   -> Map (Credential 'DRepRole) Coin
   -> [TxCertF era]
   -> Coin)
-> Term era (PParamsF era)
-> Target
     era
     (Map (Credential 'Staking) Coin
      -> Map (Credential 'DRepRole) Coin -> [TxCertF era] -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p
                    Target
  era
  (Map (Credential 'Staking) Coin
   -> Map (Credential 'DRepRole) Coin -> [TxCertF era] -> Coin)
-> Term era (Map (Credential 'Staking) Coin)
-> Target
     era (Map (Credential 'DRepRole) Coin -> [TxCertF era] -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (Credential 'Staking) Coin)
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) Coin)
stakeDeposits
                    Target
  era (Map (Credential 'DRepRole) Coin -> [TxCertF era] -> Coin)
-> Term era (Map (Credential 'DRepRole) Coin)
-> Target era ([TxCertF era] -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (Credential 'DRepRole) Coin)
forall era. Era era => Term era (Map (Credential 'DRepRole) Coin)
drepDepositsView
                    Target era ([TxCertF era] -> Coin)
-> Term era [TxCertF era] -> RootTarget era Void Coin
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [TxCertF era]
forall era. Reflect era => Term era [TxCertF era]
certs
                )
       , Term era Coin
txdeposits Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (PParamsF era
    -> Map (KeyHash 'StakePool) PoolParams -> [TxCertF era] -> Coin)
-> RootTarget
     era
     Void
     (PParamsF era
      -> Map (KeyHash 'StakePool) PoolParams -> [TxCertF era] -> Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"certsDeposits" PParamsF era
-> Map (KeyHash 'StakePool) PoolParams -> [TxCertF era] -> Coin
forall {era} {a}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxCert era) =>
PParamsF era -> Map (KeyHash 'StakePool) a -> [TxCertF era] -> Coin
certsDeposits RootTarget
  era
  Void
  (PParamsF era
   -> Map (KeyHash 'StakePool) PoolParams -> [TxCertF era] -> Coin)
-> Term era (PParamsF era)
-> Target
     era (Map (KeyHash 'StakePool) PoolParams -> [TxCertF era] -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p Target
  era (Map (KeyHash 'StakePool) PoolParams -> [TxCertF era] -> Coin)
-> Term era (Map (KeyHash 'StakePool) PoolParams)
-> Target era ([TxCertF era] -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools Target era ([TxCertF era] -> Coin)
-> Term era [TxCertF era] -> RootTarget era Void Coin
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [TxCertF era]
forall era. Reflect era => Term era [TxCertF era]
certs)
       , Term era (ScriptsNeededF era)
forall era. Reflect era => Term era (ScriptsNeededF era)
scriptsNeeded Term era (ScriptsNeededF era)
-> RootTarget era Void (ScriptsNeededF era) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (Proof era
-> Target
     era (TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era)
forall era.
EraUTxO era =>
Proof era
-> Target
     era (TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era)
needT Proof era
p Target
  era (TxBodyF era -> Map TxIn (TxOutF era) -> ScriptsNeededF era)
-> Term era (TxBodyF era)
-> Target era (Map TxIn (TxOutF era) -> ScriptsNeededF era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
tempTxBody Target era (Map TxIn (TxOutF era) -> ScriptsNeededF era)
-> Term era (Map TxIn (TxOutF era))
-> RootTarget era Void (ScriptsNeededF era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p)
       , Term era IsValid
forall era. Era era => Term era IsValid
txisvalid Term era IsValid -> RootTarget era Void IsValid -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> ([IsValid] -> IsValid)
-> RootTarget era Void ([IsValid] -> IsValid)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"allValid" [IsValid] -> IsValid
allValid RootTarget era Void ([IsValid] -> IsValid)
-> Term era [IsValid] -> RootTarget era Void IsValid
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [IsValid]
forall era. Era era => Term era [IsValid]
valids)
       , Term era (Maybe (TxAuxDataF era))
-> RootTarget era Void (TxAuxDataF era) -> [Pred era] -> Pred era
forall r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [Pred era] -> Pred era
Maybe Term era (Maybe (TxAuxDataF era))
forall era. Reflect era => Term era (Maybe (TxAuxDataF era))
txauxdata (Term era (TxAuxDataF era) -> RootTarget era Void (TxAuxDataF era)
forall era t. Term era t -> RootTarget era Void t
Simple Term era (TxAuxDataF era)
oneAuxdata) [Term era (TxAuxDataF era) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (TxAuxDataF era)
oneAuxdata]
       , Term era (Maybe TxAuxDataHash)
forall era. Era era => Term era (Maybe TxAuxDataHash)
adHash Term era (Maybe TxAuxDataHash)
-> RootTarget era Void (Maybe TxAuxDataHash) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Maybe (TxAuxDataF era) -> Maybe TxAuxDataHash)
-> RootTarget
     era Void (Maybe (TxAuxDataF era) -> Maybe TxAuxDataHash)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"hashMaybe" (TxAuxDataF era -> TxAuxDataHash
forall era. Reflect era => TxAuxDataF era -> TxAuxDataHash
hashTxAuxDataF (TxAuxDataF era -> TxAuxDataHash)
-> Maybe (TxAuxDataF era) -> Maybe TxAuxDataHash
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) RootTarget era Void (Maybe (TxAuxDataF era) -> Maybe TxAuxDataHash)
-> Term era (Maybe (TxAuxDataF era))
-> RootTarget era Void (Maybe TxAuxDataHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Maybe (TxAuxDataF era))
forall era. Reflect era => Term era (Maybe (TxAuxDataF era))
txauxdata)
       , -- Construct a temporary 'Tx' with a size close to the size of the Tx we want.
         -- We will use this to compute the 'txfee' using a fix-point approach.
         Term era ScriptIntegrityHash -> Pred era
forall era t. Term era t -> Pred era
Random Term era ScriptIntegrityHash
randomWppHash
       , Term era (Maybe ScriptIntegrityHash)
tempWppHash Term era (Maybe ScriptIntegrityHash)
-> RootTarget era Void (Maybe ScriptIntegrityHash) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era ScriptIntegrityHash
-> RootTarget era Void (Maybe ScriptIntegrityHash)
forall era t. Term era t -> Target era (Maybe t)
justTarget Term era ScriptIntegrityHash
randomWppHash
       , Term era Coin
tempTxFee Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Coin -> RootTarget era Void Coin
forall t era. t -> Target era t
constTarget (Integer -> Coin
Coin (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64
forall a. Bounded a => a
maxBound :: Word64)))
       , Term era (TxBodyF era)
tempTxBody
           Term era (TxBodyF era)
-> RootTarget era Void (TxBodyF era) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> RootTarget era Void (TxBodyF era)
forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget Term era Coin
tempTxFee Term era (Maybe ScriptIntegrityHash)
tempWppHash (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin (Word64 -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Word64
forall a. Bounded a => a
maxBound :: Word64))))
       , Term era (TxF era)
tempTx Term era (TxF era) -> RootTarget era Void (TxF era) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> RootTarget era Void (TxF era)
forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> Target era (TxF era)
txTarget Term era (TxBodyF era)
tempTxBody Term era (Set BootstrapWitness)
tempBootWits Term era (Set (WitVKey 'Witness))
tempKeyWits
       , -- Compute the real fee, and then recompute the TxBody and the Tx
         Term era Coin
forall era. Era era => Term era Coin
txfee Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (PParamsF era -> TxF era -> Map TxIn (TxOutF era) -> Coin)
-> RootTarget
     era Void (PParamsF era -> TxF era -> Map TxIn (TxOutF era) -> Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"finalFee" PParamsF era -> TxF era -> Map TxIn (TxOutF era) -> Coin
forall era.
EraUTxO era =>
PParamsF era -> TxF era -> Map TxIn (TxOutF era) -> Coin
computeFinalFee RootTarget
  era Void (PParamsF era -> TxF era -> Map TxIn (TxOutF era) -> Coin)
-> Term era (PParamsF era)
-> Target era (TxF era -> Map TxIn (TxOutF era) -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p Target era (TxF era -> Map TxIn (TxOutF era) -> Coin)
-> Term era (TxF era) -> Target era (Map TxIn (TxOutF era) -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxF era)
tempTx Target era (Map TxIn (TxOutF era) -> Coin)
-> Term era (Map TxIn (TxOutF era)) -> RootTarget era Void Coin
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p)
         --  , txbodyterm :<-: txbodyTarget txfee wppHash totalCol
         --  , txterm :<-: txTarget txbodyterm bootWits keyWits
       ]
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ case Proof era -> CertStateWit era
forall era. Proof era -> CertStateWit era
whichCertState Proof era
p of
      CertStateWit era
CertStateShelleyToBabbage -> []
      CertStateWit era
CertStateConwayToConway -> [Lens' DRepState Coin
-> Rep era Coin
-> Term era (Map (Credential 'DRepRole) DRepState)
-> Term era (Map (Credential 'DRepRole) Coin)
forall a b t1 era.
Ord a =>
Lens' b t1
-> Rep era t1 -> Term era (Map a b) -> Term era (Map a t1)
ProjM (Coin -> f Coin) -> DRepState -> f DRepState
Lens' DRepState Coin
drepDepositL Rep era Coin
forall era. Rep era Coin
CoinR Term era (Map (Credential 'DRepRole) DRepState)
forall era.
ConwayEraCertState era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState Term era (Map (Credential 'DRepRole) Coin)
-> Term era (Map (Credential 'DRepRole) Coin) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (Credential 'DRepRole) Coin)
forall era. Era era => Term era (Map (Credential 'DRepRole) Coin)
drepDepositsView]
    [Pred era] -> [Pred era] -> [Pred era]
forall a. [a] -> [a] -> [a]
++ case Proof era -> UTxOWit era
forall era. Proof era -> UTxOWit era
whichUTxO Proof era
p of
      UTxOWit era
UTxOShelleyToMary ->
        [ -- The following have no effect in ShelleyToMary, but they need to be defined. So we make them random
          Term era (Map (PlutusPointerF era) (Data era, ExUnits)) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map (PlutusPointerF era) (Data era, ExUnits))
forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers
        , Term era (Map DataHash (Data era)) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Map DataHash (Data era))
forall era. Reflect era => Term era (Map DataHash (Data era))
dataWits
        , Term era (TxOutF era) -> Pred era
forall era t. Term era t -> Pred era
Random (Proof era -> Term era (TxOutF era)
forall era. Era era => Proof era -> Term era (TxOutF era)
collateralReturn Proof era
p)
        , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
extraCol
        , Term era Coin -> Pred era
forall era t. Term era t -> Pred era
Random Term era Coin
forall era. Era era => Term era Coin
totalCol
        , Term era (Maybe ScriptIntegrityHash) -> Pred era
forall era t. Term era t -> Pred era
Random Term era (Maybe ScriptIntegrityHash)
forall era. Era era => Term era (Maybe ScriptIntegrityHash)
wppHash
        , Term era (Set ScriptHash)
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map ScriptHash (ScriptF era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict (Lens' (ScriptsNeededF era) (Set ScriptHash)
-> Rep era (Set ScriptHash)
-> Term era (ScriptsNeededF era)
-> Term era (Set ScriptHash)
forall b t era. Lens' b t -> Rep era t -> Term era b -> Term era t
Proj (Set ScriptHash -> f (Set ScriptHash))
-> ScriptsNeededF era -> f (ScriptsNeededF era)
forall era.
(ScriptsNeeded era ~ ShelleyScriptsNeeded era) =>
Lens' (ScriptsNeededF era) (Set ScriptHash)
Lens' (ScriptsNeededF era) (Set ScriptHash)
smNeededL (Rep era ScriptHash -> Rep era (Set ScriptHash)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era ScriptHash
forall era. Era era => Rep era ScriptHash
ScriptHashR) Term era (ScriptsNeededF era)
forall era. Reflect era => Term era (ScriptsNeededF era)
scriptsNeeded) (Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p) Term era (Map ScriptHash (ScriptF era))
-> Term era (Map ScriptHash (ScriptF era)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map ScriptHash (ScriptF era))
forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits
        , Term era (Map ScriptHash IsValid) -> Term era [IsValid]
forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems (Lens' (IsValid, ScriptF era) IsValid
-> Rep era IsValid
-> Term era (Map ScriptHash (IsValid, ScriptF era))
-> Term era (Map ScriptHash IsValid)
forall a b t1 era.
Ord a =>
Lens' b t1
-> Rep era t1 -> Term era (Map a b) -> Term era (Map a t1)
ProjM (IsValid -> f IsValid)
-> (IsValid, ScriptF era) -> f (IsValid, ScriptF era)
forall a b (f :: * -> *).
Functor f =>
(a -> f a) -> (a, b) -> f (a, b)
Lens' (IsValid, ScriptF era) IsValid
fstL Rep era IsValid
forall era. Rep era IsValid
IsValidR (Term era (Set ScriptHash)
-> Term era (Map ScriptHash (IsValid, ScriptF era))
-> Term era (Map ScriptHash (IsValid, ScriptF era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict (Term era (Map ScriptHash (ScriptF era))
-> Term era (Set ScriptHash)
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map ScriptHash (ScriptF era))
forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits) Term era (Map ScriptHash (IsValid, ScriptF era))
forall era.
Reflect era =>
Term era (Map ScriptHash (IsValid, ScriptF era))
plutusUniv)) Term era [IsValid] -> Term era [IsValid] -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era [IsValid]
forall era. Era era => Term era [IsValid]
valids
        , Term era (Set BootstrapWitness)
tempBootWits Term era (Set BootstrapWitness)
-> RootTarget era Void (Set BootstrapWitness) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Map TxIn (TxOutF era)
    -> TxBodyF era
    -> Map (KeyHash 'Payment) (Addr, SigningKey)
    -> Set BootstrapWitness)
-> RootTarget
     era
     Void
     (Map TxIn (TxOutF era)
      -> TxBodyF era
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set BootstrapWitness)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"boots" (Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
p) RootTarget
  era
  Void
  (Map TxIn (TxOutF era)
   -> TxBodyF era
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set BootstrapWitness)
-> Term era (Map TxIn (TxOutF era))
-> Target
     era
     (TxBodyF era
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
spending Target
  era
  (TxBodyF era
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set BootstrapWitness)
-> Term era (TxBodyF era)
-> Target
     era
     (Map (KeyHash 'Payment) (Addr, SigningKey) -> Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
tempTxBody Target
  era
  (Map (KeyHash 'Payment) (Addr, SigningKey) -> Set BootstrapWitness)
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> RootTarget era Void (Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv)
        , Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
-> RootTarget era Void (Set (KeyHash 'Witness)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Target era (Set (KeyHash 'Witness))
necessaryKeyHashTarget @era Term era (TxBodyF era)
tempTxBody (Rep era (Set (KeyHash 'Witness))
-> Set (KeyHash 'Witness) -> Term era (Set (KeyHash 'Witness))
forall era t. Rep era t -> t -> Term era t
Lit (Rep era (KeyHash 'Witness) -> Rep era (Set (KeyHash 'Witness))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era (KeyHash 'Witness)
forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) Set (KeyHash 'Witness)
forall a. Set a
Set.empty)
        , Term era (Set (KeyHash 'Witness))
sufficientHashes
            Term era (Set (KeyHash 'Witness))
-> RootTarget era Void (Set (KeyHash 'Witness)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Map ScriptHash (ScriptF era)
    -> [TxCertF era]
    -> Map (KeyHash 'Genesis) GenDelegPair
    -> Set (KeyHash 'Witness))
-> RootTarget
     era
     Void
     (Map ScriptHash (ScriptF era)
      -> [TxCertF era]
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Set (KeyHash 'Witness))
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"sufficient" (Proof era
-> Map ScriptHash (ScriptF era)
-> [TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
forall era.
Reflect era =>
Proof era
-> Map ScriptHash (ScriptF era)
-> [TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
sufficientKeyHashes Proof era
p) RootTarget
  era
  Void
  (Map ScriptHash (ScriptF era)
   -> [TxCertF era]
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Target
     era
     ([TxCertF era]
      -> Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map ScriptHash (ScriptF era))
forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits Target
  era
  ([TxCertF era]
   -> Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness))
-> Term era [TxCertF era]
-> Target
     era (Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [TxCertF era]
forall era. Reflect era => Term era [TxCertF era]
certs Target
  era (Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness))
-> Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> RootTarget era Void (Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs)
        , Term era (Set (WitVKey 'Witness))
tempKeyWits
            Term era (Set (WitVKey 'Witness))
-> RootTarget era Void (Set (WitVKey 'Witness)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> RootTarget era Void (Set (WitVKey 'Witness))
forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget Term era (TxBodyF era)
tempTxBody Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
sufficientHashes Term era (Map ScriptHash (ScriptF era))
forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv
        , Term era (Set BootstrapWitness)
forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits Term era (Set BootstrapWitness)
-> RootTarget era Void (Set BootstrapWitness) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Map TxIn (TxOutF era)
    -> TxBodyF era
    -> Map (KeyHash 'Payment) (Addr, SigningKey)
    -> Set BootstrapWitness)
-> RootTarget
     era
     Void
     (Map TxIn (TxOutF era)
      -> TxBodyF era
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set BootstrapWitness)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"boots" (Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
p) RootTarget
  era
  Void
  (Map TxIn (TxOutF era)
   -> TxBodyF era
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set BootstrapWitness)
-> Term era (Map TxIn (TxOutF era))
-> Target
     era
     (TxBodyF era
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
spending Target
  era
  (TxBodyF era
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set BootstrapWitness)
-> Term era (TxBodyF era)
-> Target
     era
     (Map (KeyHash 'Payment) (Addr, SigningKey) -> Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Target
  era
  (Map (KeyHash 'Payment) (Addr, SigningKey) -> Set BootstrapWitness)
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> RootTarget era Void (Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv)
        , Term era (Set (WitVKey 'Witness))
forall era. Reflect era => Term era (Set (WitVKey 'Witness))
keyWits
            Term era (Set (WitVKey 'Witness))
-> RootTarget era Void (Set (WitVKey 'Witness)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> RootTarget era Void (Set (WitVKey 'Witness))
forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
sufficientHashes Term era (Map ScriptHash (ScriptF era))
forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv
        , Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (TxBodyF era)
-> RootTarget era Void (TxBodyF era) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> RootTarget era Void (TxBodyF era)
forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget Term era Coin
forall era. Era era => Term era Coin
txfee Term era (Maybe ScriptIntegrityHash)
tempWppHash (Rep era Coin -> Coin -> Term era Coin
forall era t. Rep era t -> t -> Term era t
Lit Rep era Coin
forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) -- The WppHash and totalCol play no role in ShelleyToMary
        , Term era (TxF era)
forall era. Reflect era => Term era (TxF era)
txterm Term era (TxF era) -> RootTarget era Void (TxF era) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> RootTarget era Void (TxF era)
forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> Target era (TxF era)
txTarget Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (Set BootstrapWitness)
forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits Term era (Set (WitVKey 'Witness))
forall era. Reflect era => Term era (Set (WitVKey 'Witness))
keyWits
        ]
      UTxOWit era
UTxOAlonzoToConway ->
        [ Term era Size -> Term era Coin -> Pred era
forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (Int -> Term era Size
forall era. Era era => Int -> Term era Size
ExactSize Int
0) Term era Coin
forall era. Era era => Term era Coin
txDonation
        , Lens' (ScriptsNeededF era) [(PlutusPurposeF era, ScriptHash)]
-> Rep era [(PlutusPurposeF era, ScriptHash)]
-> Term era (ScriptsNeededF era)
-> Term era [(PlutusPurposeF era, ScriptHash)]
forall b t era. Lens' b t -> Rep era t -> Term era b -> Term era t
Proj ([(PlutusPurposeF era, ScriptHash)]
 -> f [(PlutusPurposeF era, ScriptHash)])
-> ScriptsNeededF era -> f (ScriptsNeededF era)
forall era.
(ScriptsNeeded era ~ AlonzoScriptsNeeded era) =>
Lens' (ScriptsNeededF era) [(PlutusPurposeF era, ScriptHash)]
Lens' (ScriptsNeededF era) [(PlutusPurposeF era, ScriptHash)]
acNeededL (Rep era (PlutusPurposeF era, ScriptHash)
-> Rep era [(PlutusPurposeF era, ScriptHash)]
forall era a. Rep era a -> Rep era [a]
ListR (Rep era (PlutusPurposeF era)
-> Rep era ScriptHash -> Rep era (PlutusPurposeF era, ScriptHash)
forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR (Proof era -> Rep era (PlutusPurposeF era)
forall era. Era era => Proof era -> Rep era (PlutusPurposeF era)
ScriptPurposeR Proof era
p) Rep era ScriptHash
forall era. Era era => Rep era ScriptHash
ScriptHashR)) Term era (ScriptsNeededF era)
forall era. Reflect era => Term era (ScriptsNeededF era)
scriptsNeeded Term era [(PlutusPurposeF era, ScriptHash)]
-> Term era [(PlutusPurposeF era, ScriptHash)] -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era [(PlutusPurposeF era, ScriptHash)]
acNeeded
        , -- Hashes of scripts that will be run. Not all of these will be in the 'scriptWits'
          Term era (Set ScriptHash)
neededHashSet Term era (Set ScriptHash)
-> RootTarget era Void (Set ScriptHash) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> ([(PlutusPurposeF era, ScriptHash)] -> Set ScriptHash)
-> RootTarget
     era Void ([(PlutusPurposeF era, ScriptHash)] -> Set ScriptHash)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"toSet" (\[(PlutusPurposeF era, ScriptHash)]
x -> [ScriptHash] -> Set ScriptHash
forall a. Ord a => [a] -> Set a
Set.fromList (((PlutusPurposeF era, ScriptHash) -> ScriptHash)
-> [(PlutusPurposeF era, ScriptHash)] -> [ScriptHash]
forall a b. (a -> b) -> [a] -> [b]
map (PlutusPurposeF era, ScriptHash) -> ScriptHash
forall a b. (a, b) -> b
snd [(PlutusPurposeF era, ScriptHash)]
x)) RootTarget
  era Void ([(PlutusPurposeF era, ScriptHash)] -> Set ScriptHash)
-> Term era [(PlutusPurposeF era, ScriptHash)]
-> RootTarget era Void (Set ScriptHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [(PlutusPurposeF era, ScriptHash)]
acNeeded)
        , -- Only the refAdjusted scripts need to be in the 'scriptWits' but if the refscripts that are
          -- excluded from 'scriptWits' are Timelock scripts, a sufficient set keys must be added to
          -- the sufficient key hashes.
          Term era (Set ScriptHash)
refAdjusted
            Term era (Set ScriptHash)
-> RootTarget era Void (Set ScriptHash) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Set TxIn
    -> Set TxIn
    -> Map TxIn (TxOutF era)
    -> Set ScriptHash
    -> Set ScriptHash)
-> RootTarget
     era
     Void
     (Set TxIn
      -> Set TxIn
      -> Map TxIn (TxOutF era)
      -> Set ScriptHash
      -> Set ScriptHash)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"adjust" (Proof era
-> Set TxIn
-> Set TxIn
-> Map TxIn (TxOutF era)
-> Set ScriptHash
-> Set ScriptHash
forall era.
Proof era
-> Set TxIn
-> Set TxIn
-> Map TxIn (TxOutF era)
-> Set ScriptHash
-> Set ScriptHash
adjustNeededByRefScripts Proof era
p) RootTarget
  era
  Void
  (Set TxIn
   -> Set TxIn
   -> Map TxIn (TxOutF era)
   -> Set ScriptHash
   -> Set ScriptHash)
-> Term era (Set TxIn)
-> Target
     era
     (Set TxIn
      -> Map TxIn (TxOutF era) -> Set ScriptHash -> Set ScriptHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
inputs Target
  era
  (Set TxIn
   -> Map TxIn (TxOutF era) -> Set ScriptHash -> Set ScriptHash)
-> Term era (Set TxIn)
-> Target
     era (Map TxIn (TxOutF era) -> Set ScriptHash -> Set ScriptHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
refInputs Target
  era (Map TxIn (TxOutF era) -> Set ScriptHash -> Set ScriptHash)
-> Term era (Map TxIn (TxOutF era))
-> Target era (Set ScriptHash -> Set ScriptHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p) Target era (Set ScriptHash -> Set ScriptHash)
-> Term era (Set ScriptHash)
-> RootTarget era Void (Set ScriptHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set ScriptHash)
neededHashSet)
        , -- , scriptWits :=: Restrict refAdjusted (allScriptUniv p)
          Term era (Set ScriptHash)
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map ScriptHash (ScriptF era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set ScriptHash)
refAdjusted (Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p) Term era (Map ScriptHash (ScriptF era))
-> Term era (Map ScriptHash (ScriptF era)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map ScriptHash (ScriptF era))
forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits
        , Term era (Map ScriptHash IsValid) -> Term era [IsValid]
forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems (Lens' (IsValid, ScriptF era) IsValid
-> Rep era IsValid
-> Term era (Map ScriptHash (IsValid, ScriptF era))
-> Term era (Map ScriptHash IsValid)
forall a b t1 era.
Ord a =>
Lens' b t1
-> Rep era t1 -> Term era (Map a b) -> Term era (Map a t1)
ProjM (IsValid -> f IsValid)
-> (IsValid, ScriptF era) -> f (IsValid, ScriptF era)
forall a b (f :: * -> *).
Functor f =>
(a -> f a) -> (a, b) -> f (a, b)
Lens' (IsValid, ScriptF era) IsValid
fstL Rep era IsValid
forall era. Rep era IsValid
IsValidR (Term era (Set ScriptHash)
-> Term era (Map ScriptHash (IsValid, ScriptF era))
-> Term era (Map ScriptHash (IsValid, ScriptF era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set ScriptHash)
neededHashSet Term era (Map ScriptHash (IsValid, ScriptF era))
forall era.
Reflect era =>
Term era (Map ScriptHash (IsValid, ScriptF era))
plutusUniv)) Term era [IsValid] -> Term era [IsValid] -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era [IsValid]
forall era. Era era => Term era [IsValid]
valids
        , Term era (Set (PlutusPointerF era))
rdmrPtrs Term era (Set (PlutusPointerF era))
-> RootTarget era Void (Set (PlutusPointerF era)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (Target
  era
  ([(PlutusPurposeF era, ScriptHash)]
   -> Map ScriptHash (IsValid, ScriptF era)
   -> Set (PlutusPointerF era))
forall era any.
AlonzoEraScript era =>
Target
  era
  ([(PlutusPurposeF era, ScriptHash)]
   -> Map ScriptHash any -> Set (PlutusPointerF era))
rdmrPtrsT Target
  era
  ([(PlutusPurposeF era, ScriptHash)]
   -> Map ScriptHash (IsValid, ScriptF era)
   -> Set (PlutusPointerF era))
-> Term era [(PlutusPurposeF era, ScriptHash)]
-> Target
     era
     (Map ScriptHash (IsValid, ScriptF era) -> Set (PlutusPointerF era))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [(PlutusPurposeF era, ScriptHash)]
acNeeded Target
  era
  (Map ScriptHash (IsValid, ScriptF era) -> Set (PlutusPointerF era))
-> Term era (Map ScriptHash (IsValid, ScriptF era))
-> RootTarget era Void (Set (PlutusPointerF era))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map ScriptHash (IsValid, ScriptF era))
forall era.
Reflect era =>
Term era (Map ScriptHash (IsValid, ScriptF era))
plutusUniv)
        , Term era (Set (PlutusPointerF era))
rdmrPtrs Term era (Set (PlutusPointerF era))
-> Term era (Set (PlutusPointerF era)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map (PlutusPointerF era) (Data era, ExUnits))
-> Term era (Set (PlutusPointerF era))
forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (PlutusPointerF era) (Data era, ExUnits))
forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers
        , RootTarget era Void Bool -> Pred era -> Pred era -> Pred era
forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
            (TestName
-> (Set (PlutusPointerF era) -> Bool)
-> RootTarget era Void (Set (PlutusPointerF era) -> Bool)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"null" Set (PlutusPointerF era) -> Bool
forall a. Set a -> Bool
Set.null RootTarget era Void (Set (PlutusPointerF era) -> Bool)
-> Term era (Set (PlutusPointerF era)) -> RootTarget era Void Bool
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (PlutusPointerF era))
rdmrPtrs)
            (Term era ExUnits
-> Term era (Map (PlutusPointerF era) (Data era, ExUnits))
-> Pred era
forall era a b. Term era a -> Term era b -> Pred era
Before (Proof era -> Term era ExUnits
forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) Term era (Map (PlutusPointerF era) (Data era, ExUnits))
forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers)
            (Direct ExUnits
-> Term era ExUnits -> OrdCond -> [Sum era ExUnits] -> Pred era
forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo (ExUnits -> Direct ExUnits
forall a b. a -> Either a b
Left (Nat -> Nat -> ExUnits
ExUnits Nat
1 Nat
1)) (Proof era -> Term era ExUnits
forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) OrdCond
GTE [Rep era ExUnits
-> Lens' (Data era, ExUnits) ExUnits
-> Term era (Map (PlutusPointerF era) (Data era, ExUnits))
-> Sum era ExUnits
forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap Rep era ExUnits
forall era. Rep era ExUnits
ExUnitsR (ExUnits -> f ExUnits)
-> (Data era, ExUnits) -> f (Data era, ExUnits)
forall a b (f :: * -> *).
Functor f =>
(b -> f b) -> (a, b) -> f (a, b)
Lens' (Data era, ExUnits) ExUnits
sndL Term era (Map (PlutusPointerF era) (Data era, ExUnits))
forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers])
        , Term era (Set DataHash)
plutusDataHashes
            Term era (Set DataHash)
-> RootTarget era Void (Set DataHash) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( TestName
-> (Map TxIn (TxOutF era)
    -> TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash)
-> RootTarget
     era
     Void
     (Map TxIn (TxOutF era)
      -> TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"plutusDataHashes" Map TxIn (TxOutF era)
-> TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash
forall era.
(AlonzoEraTxOut era, EraTxBody era, AlonzoEraScript era) =>
Map TxIn (TxOutF era)
-> TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash
getPlutusDataHashes
                     RootTarget
  era
  Void
  (Map TxIn (TxOutF era)
   -> TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash)
-> Term era (Map TxIn (TxOutF era))
-> Target
     era (TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p
                     Target
  era (TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash)
-> Term era (TxBodyF era)
-> Target era (Map ScriptHash (ScriptF era) -> Set DataHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
tempTxBody
                     Target era (Map ScriptHash (ScriptF era) -> Set DataHash)
-> Term era (Map ScriptHash (ScriptF era))
-> RootTarget era Void (Set DataHash)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p
                 )
        , Term era (Set DataHash)
-> Term era (Map DataHash (Data era))
-> Term era (Map DataHash (Data era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set DataHash)
plutusDataHashes Term era (Map DataHash (Data era))
forall era. Era era => Term era (Map DataHash (Data era))
dataUniv Term era (Map DataHash (Data era))
-> Term era (Map DataHash (Data era)) -> Pred era
forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era (Map DataHash (Data era))
forall era. Reflect era => Term era (Map DataHash (Data era))
dataWits
        , Term era (Set BootstrapWitness)
tempBootWits Term era (Set BootstrapWitness)
-> RootTarget era Void (Set BootstrapWitness) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Map TxIn (TxOutF era)
    -> TxBodyF era
    -> Map (KeyHash 'Payment) (Addr, SigningKey)
    -> Set BootstrapWitness)
-> RootTarget
     era
     Void
     (Map TxIn (TxOutF era)
      -> TxBodyF era
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set BootstrapWitness)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"boots" (Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
p) RootTarget
  era
  Void
  (Map TxIn (TxOutF era)
   -> TxBodyF era
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set BootstrapWitness)
-> Term era (Map TxIn (TxOutF era))
-> Target
     era
     (TxBodyF era
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
spending Target
  era
  (TxBodyF era
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set BootstrapWitness)
-> Term era (TxBodyF era)
-> Target
     era
     (Map (KeyHash 'Payment) (Addr, SigningKey) -> Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
tempTxBody Target
  era
  (Map (KeyHash 'Payment) (Addr, SigningKey) -> Set BootstrapWitness)
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> RootTarget era Void (Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv)
        , Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
-> RootTarget era Void (Set (KeyHash 'Witness)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Target era (Set (KeyHash 'Witness))
necessaryKeyHashTarget @era Term era (TxBodyF era)
tempTxBody Term era (Set (KeyHash 'Witness))
forall era. Era era => Term era (Set (KeyHash 'Witness))
reqSignerHashes
        , Term era (Set (KeyHash 'Witness))
sufficientHashes
            Term era (Set (KeyHash 'Witness))
-> RootTarget era Void (Set (KeyHash 'Witness)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( TestName
-> (Map ScriptHash (ScriptF era)
    -> [TxCertF era]
    -> Map (KeyHash 'Genesis) GenDelegPair
    -> Set (KeyHash 'Witness))
-> RootTarget
     era
     Void
     (Map ScriptHash (ScriptF era)
      -> [TxCertF era]
      -> Map (KeyHash 'Genesis) GenDelegPair
      -> Set (KeyHash 'Witness))
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"sufficient" (Proof era
-> Map ScriptHash (ScriptF era)
-> [TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
forall era.
Reflect era =>
Proof era
-> Map ScriptHash (ScriptF era)
-> [TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
sufficientKeyHashes Proof era
p)
                     RootTarget
  era
  Void
  (Map ScriptHash (ScriptF era)
   -> [TxCertF era]
   -> Map (KeyHash 'Genesis) GenDelegPair
   -> Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Target
     era
     ([TxCertF era]
      -> Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set ScriptHash)
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map ScriptHash (ScriptF era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set ScriptHash)
neededHashSet (Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p)
                     Target
  era
  ([TxCertF era]
   -> Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness))
-> Term era [TxCertF era]
-> Target
     era (Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [TxCertF era]
forall era. Reflect era => Term era [TxCertF era]
certs
                     Target
  era (Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness))
-> Term era (Map (KeyHash 'Genesis) GenDelegPair)
-> RootTarget era Void (Set (KeyHash 'Witness))
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Genesis) GenDelegPair)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'Genesis) GenDelegPair)
genDelegs
                 )
        , Term era (Set (WitVKey 'Witness))
tempKeyWits
            Term era (Set (WitVKey 'Witness))
-> RootTarget era Void (Set (WitVKey 'Witness)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> RootTarget era Void (Set (WitVKey 'Witness))
forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget Term era (TxBodyF era)
tempTxBody Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
sufficientHashes Term era (Map ScriptHash (ScriptF era))
forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv
        , Term era (Set BootstrapWitness)
forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits Term era (Set BootstrapWitness)
-> RootTarget era Void (Set BootstrapWitness) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Map TxIn (TxOutF era)
    -> TxBodyF era
    -> Map (KeyHash 'Payment) (Addr, SigningKey)
    -> Set BootstrapWitness)
-> RootTarget
     era
     Void
     (Map TxIn (TxOutF era)
      -> TxBodyF era
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set BootstrapWitness)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"boots" (Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
p) RootTarget
  era
  Void
  (Map TxIn (TxOutF era)
   -> TxBodyF era
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set BootstrapWitness)
-> Term era (Map TxIn (TxOutF era))
-> Target
     era
     (TxBodyF era
      -> Map (KeyHash 'Payment) (Addr, SigningKey)
      -> Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
spending Target
  era
  (TxBodyF era
   -> Map (KeyHash 'Payment) (Addr, SigningKey)
   -> Set BootstrapWitness)
-> Term era (TxBodyF era)
-> Target
     era
     (Map (KeyHash 'Payment) (Addr, SigningKey) -> Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Target
  era
  (Map (KeyHash 'Payment) (Addr, SigningKey) -> Set BootstrapWitness)
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> RootTarget era Void (Set BootstrapWitness)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv)
        , Term era (Set (WitVKey 'Witness))
forall era. Reflect era => Term era (Set (WitVKey 'Witness))
keyWits
            Term era (Set (WitVKey 'Witness))
-> RootTarget era Void (Set (WitVKey 'Witness)) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> RootTarget era Void (Set (WitVKey 'Witness))
forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
sufficientHashes Term era (Map ScriptHash (ScriptF era))
forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv
        , -- 'langs' is not computed from the 'scriptWits' because that does not include needed
          -- scripts that are reference scripts, So get the scripts from the neededHashSet
          Term era (Set Language)
langs Term era (Set Language)
-> RootTarget era Void (Set Language) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Map ScriptHash (ScriptF era) -> Set Language)
-> RootTarget
     era Void (Map ScriptHash (ScriptF era) -> Set Language)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"languages" Map ScriptHash (ScriptF era) -> Set Language
forall k era. Map k (ScriptF era) -> Set Language
scriptWitsLangs RootTarget era Void (Map ScriptHash (ScriptF era) -> Set Language)
-> Term era (Map ScriptHash (ScriptF era))
-> RootTarget era Void (Set Language)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set ScriptHash)
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map ScriptHash (ScriptF era))
forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set ScriptHash)
neededHashSet (Proof era -> Term era (Map ScriptHash (ScriptF era))
forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p))
        , Term era (Maybe ScriptIntegrityHash)
forall era. Era era => Term era (Maybe ScriptIntegrityHash)
wppHash Term era (Maybe ScriptIntegrityHash)
-> RootTarget era Void (Maybe ScriptIntegrityHash) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Proof era
-> Term era (PParamsF era)
-> Term era (Set Language)
-> Term era (Map (PlutusPointerF era) (Data era, ExUnits))
-> Term era (Map DataHash (Data era))
-> RootTarget era Void (Maybe ScriptIntegrityHash)
forall era1 era2.
Era era1 =>
Proof era1
-> Term era2 (PParamsF era1)
-> Term era2 (Set Language)
-> Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits))
-> Term era2 (Map DataHash (Data era1))
-> Target era2 (Maybe ScriptIntegrityHash)
integrityHash Proof era
p (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p) Term era (Set Language)
langs Term era (Map (PlutusPointerF era) (Data era, ExUnits))
forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers Term era (Map DataHash (Data era))
forall era. Reflect era => Term era (Map DataHash (Data era))
dataWits
        , Term era Coin
forall era. Era era => Term era Coin
owed
            Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( TestName
-> (Nat -> Coin -> Coin)
-> RootTarget era Void (Nat -> Coin -> Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"owed" (\Nat
percent (Coin Integer
fee) -> Rational -> Coin
rationalToCoinViaCeiling ((Nat -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
percent Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
fee) Integer -> Integer -> Rational
forall a. Integral a => a -> a -> Ratio a
% Integer
100))
                     RootTarget era Void (Nat -> Coin -> Coin)
-> Term era Nat -> Target era (Coin -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Proof era -> Term era Nat
forall era. AlonzoEraPParams era => Proof era -> Term era Nat
collateralPercentage Proof era
p
                     Target era (Coin -> Coin)
-> Term era Coin -> RootTarget era Void Coin
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
forall era. Era era => Term era Coin
txfee
                 )
        , -- we need to add 'extraCol' to the colUtxo, to pay the collateral fee.
          -- we arrange this so adding the 'extraCol' will make the sum of the all the collateral inputs, one more than 'owed'
          Term era Coin
forall era. Era era => Term era Coin
extraCol
            Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Coin -> Coin -> Coin)
-> RootTarget era Void (Coin -> Coin -> Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"extraCol" (\(Coin Integer
suminputs) (Coin Integer
owe) -> (Integer -> Coin
Coin (Integer
owe Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
+ Integer
1 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
suminputs))) RootTarget era Void (Coin -> Coin -> Coin)
-> Term era Coin -> Target era (Coin -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
forall era. Era era => Term era Coin
sumCol Target era (Coin -> Coin)
-> Term era Coin -> RootTarget era Void Coin
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
forall era. Era era => Term era Coin
owed)
        , Term era Coin
forall era. Era era => Term era Coin
totalCol Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Coin -> Coin -> Coin)
-> RootTarget era Void (Coin -> Coin -> Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"(<+>)" (\Coin
x Coin
y -> Coin
x Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
y Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Integer -> Coin
Coin Integer
1) RootTarget era Void (Coin -> Coin -> Coin)
-> Term era Coin -> Target era (Coin -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
forall era. Era era => Term era Coin
extraCol Target era (Coin -> Coin)
-> Term era Coin -> RootTarget era Void Coin
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
forall era. Era era => Term era Coin
sumCol)
        , Direct (Term era Addr) -> Term era (Set Addr) -> Pred era
forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (Term era Addr -> Direct (Term era Addr)
forall a b. b -> Either a b
Right Term era Addr
forall era. Era era => Term era Addr
colRetAddr) Term era (Set Addr)
forall era. Era era => Term era (Set Addr)
addrUniv
        , -- This ( collateralReturn) depends on the Coin in the TxOut being (Coin 1).
          -- The computation of 'owed' and 'extraCol" should ensure this.
          Proof era -> Term era (TxOutF era)
forall era. Era era => Proof era -> Term era (TxOutF era)
collateralReturn Proof era
p
            Term era (TxOutF era)
-> RootTarget era Void (TxOutF era) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Addr -> TxOutF era) -> RootTarget era Void (Addr -> TxOutF era)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"colReturn" (\Addr
ad -> Proof era -> TxOut era -> TxOutF era
forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
p (Addr -> Value era -> TxOut era
forall era.
(EraTxOut era, HasCallStack) =>
Addr -> Value era -> TxOut era
mkBasicTxOut Addr
ad (Coin -> Value era
forall t s. Inject t s => t -> s
inject (Integer -> Coin
Coin Integer
1)))) RootTarget era Void (Addr -> TxOutF era)
-> Term era Addr -> RootTarget era Void (TxOutF era)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Addr
forall era. Era era => Term era Addr
colRetAddr)
        , -- We compute this, so that we can test that the (Coin 1) invariant holds.
          Term era Coin
forall era. Era era => Term era Coin
colRetCoin
            Term era Coin -> RootTarget era Void Coin -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (TestName
-> (Coin -> Coin -> Coin -> Coin)
-> RootTarget era Void (Coin -> Coin -> Coin -> Coin)
forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"-" (\Coin
sumc Coin
extra Coin
owe -> (Coin
sumc Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Coin
extra) Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Coin
owe) RootTarget era Void (Coin -> Coin -> Coin -> Coin)
-> Term era Coin -> RootTarget era Void (Coin -> Coin -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
forall era. Era era => Term era Coin
sumCol RootTarget era Void (Coin -> Coin -> Coin)
-> Term era Coin -> Target era (Coin -> Coin)
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
forall era. Era era => Term era Coin
extraCol Target era (Coin -> Coin)
-> Term era Coin -> RootTarget era Void Coin
forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era Coin
forall era. Era era => Term era Coin
owed)
        , Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (TxBodyF era)
-> RootTarget era Void (TxBodyF era) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> RootTarget era Void (TxBodyF era)
forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget Term era Coin
forall era. Era era => Term era Coin
txfee Term era (Maybe ScriptIntegrityHash)
forall era. Era era => Term era (Maybe ScriptIntegrityHash)
wppHash Term era Coin
forall era. Era era => Term era Coin
totalCol
        , Term era (TxF era)
forall era. Reflect era => Term era (TxF era)
txterm Term era (TxF era) -> RootTarget era Void (TxF era) -> Pred era
forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> RootTarget era Void (TxF era)
forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> Target era (TxF era)
txTarget Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (Set BootstrapWitness)
forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits Term era (Set (WitVKey 'Witness))
forall era. Reflect era => Term era (Set (WitVKey 'Witness))
keyWits
        ]
  where
    spending :: Term era (Map TxIn (TxOutF era))
spending = V era (Map TxIn (TxOutF era)) -> Term era (Map TxIn (TxOutF era))
forall era t. V era t -> Term era t
Var (TestName
-> Rep era (Map TxIn (TxOutF era))
-> Access era Any (Map TxIn (TxOutF era))
-> V era (Map TxIn (TxOutF era))
forall era t s.
Era era =>
TestName -> Rep era t -> Access era s t -> V era t
V TestName
"spending" (Rep era TxIn
-> Rep era (TxOutF era) -> Rep era (Map TxIn (TxOutF era))
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era TxIn
forall era. Era era => Rep era TxIn
TxInR (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) Access era Any (Map TxIn (TxOutF era))
forall era s t. Access era s t
No)
    colUtxo :: Term era (Map TxIn (TxOutF era))
colUtxo = V era (Map TxIn (TxOutF era)) -> Term era (Map TxIn (TxOutF era))
forall era t. V era t -> Term era t
Var (TestName
-> Rep era (Map TxIn (TxOutF era))
-> Access era Any (Map TxIn (TxOutF era))
-> V era (Map TxIn (TxOutF era))
forall era t s.
Era era =>
TestName -> Rep era t -> Access era s t -> V era t
V TestName
"colUtxo" (Rep era TxIn
-> Rep era (TxOutF era) -> Rep era (Map TxIn (TxOutF era))
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era TxIn
forall era. Era era => Rep era TxIn
TxInR (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) Access era Any (Map TxIn (TxOutF era))
forall era s t. Access era s t
No)
    colRestriction :: Term era (Map TxIn (TxOutF era))
colRestriction = V era (Map TxIn (TxOutF era)) -> Term era (Map TxIn (TxOutF era))
forall era t. V era t -> Term era t
Var (TestName
-> Rep era (Map TxIn (TxOutF era))
-> Access era Any (Map TxIn (TxOutF era))
-> V era (Map TxIn (TxOutF era))
forall era t s.
Era era =>
TestName -> Rep era t -> Access era s t -> V era t
V TestName
"colRestriction" (Rep era TxIn
-> Rep era (TxOutF era) -> Rep era (Map TxIn (TxOutF era))
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era TxIn
forall era. Era era => Rep era TxIn
TxInR (Proof era -> Rep era (TxOutF era)
forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) Access era Any (Map TxIn (TxOutF era))
forall era s t. Access era s t
No)
    nonZeroRewards :: Term era (Map (Credential 'Staking) Coin)
nonZeroRewards = TestName
-> Rep era (Map (Credential 'Staking) Coin)
-> Term era (Map (Credential 'Staking) Coin)
forall era t. Era era => TestName -> Rep era t -> Term era t
var TestName
"nonZeroRewards" (Rep era (Credential 'Staking)
-> Rep era Coin -> Rep era (Map (Credential 'Staking) Coin)
forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR Rep era (Credential 'Staking)
forall era. Era era => Rep era (Credential 'Staking)
CredR Rep era Coin
forall era. Rep era Coin
CoinR)
    balanceCoin :: Term era Coin
balanceCoin = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (TestName -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Era era =>
TestName -> Rep era t -> Access era s t -> V era t
V TestName
"balanceCoin" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No)
    certsRefunds :: PParamsF era
-> Map (Credential 'Staking) Coin
-> Map (Credential 'DRepRole) Coin
-> [TxCertF era]
-> Coin
certsRefunds (PParamsF Proof era
_ PParams era
pp) Map (Credential 'Staking) Coin
stakingDepositsx Map (Credential 'DRepRole) Coin
drepDepositsx [TxCertF era]
certsx =
      PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> [TxCert era]
-> Coin
forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> f (TxCert era)
-> Coin
forall (f :: * -> *).
Foldable f =>
PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> Maybe Coin)
-> f (TxCert era)
-> Coin
getTotalRefundsTxCerts
        PParams era
pp
        (Credential 'Staking -> Map (Credential 'Staking) Coin -> Maybe Coin
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map (Credential 'Staking) Coin
stakingDepositsx)
        (Credential 'DRepRole
-> Map (Credential 'DRepRole) Coin -> Maybe Coin
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map (Credential 'DRepRole) Coin
drepDepositsx)
        ((TxCertF era -> TxCert era) -> [TxCertF era] -> [TxCert era]
forall a b. (a -> b) -> [a] -> [b]
map TxCertF era -> TxCert era
forall era. TxCertF era -> TxCert era
unTxCertF [TxCertF era]
certsx)
    certsDeposits :: PParamsF era -> Map (KeyHash 'StakePool) a -> [TxCertF era] -> Coin
certsDeposits (PParamsF Proof era
_ PParams era
pp) Map (KeyHash 'StakePool) a
regpools [TxCertF era]
certsx = Integer -> Coin
Coin (-Integer
n)
      where
        Coin Integer
n = PParams era -> (KeyHash 'StakePool -> Bool) -> [TxCert era] -> Coin
forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (KeyHash 'StakePool -> Bool) -> f (TxCert era) -> Coin
forall (f :: * -> *).
Foldable f =>
PParams era
-> (KeyHash 'StakePool -> Bool) -> f (TxCert era) -> Coin
getTotalDepositsTxCerts PParams era
pp (KeyHash 'StakePool -> Map (KeyHash 'StakePool) a -> Bool
forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map (KeyHash 'StakePool) a
regpools) ((TxCertF era -> TxCert era) -> [TxCertF era] -> [TxCert era]
forall a b. (a -> b) -> [a] -> [b]
map TxCertF era -> TxCert era
forall era. TxCertF era -> TxCert era
unTxCertF [TxCertF era]
certsx)
    txrefunds :: Term era Coin
txrefunds = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (Proof era
-> TestName -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"txrefunds" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No)
    txdeposits :: Term era Coin
txdeposits = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (Proof era
-> TestName -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"txdeposits" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No)
    acNeeded :: Term era [(PlutusPurposeF era, ScriptHash)]
    acNeeded :: Term era [(PlutusPurposeF era, ScriptHash)]
acNeeded = V era [(PlutusPurposeF era, ScriptHash)]
-> Term era [(PlutusPurposeF era, ScriptHash)]
forall era t. V era t -> Term era t
Var (V era [(PlutusPurposeF era, ScriptHash)]
 -> Term era [(PlutusPurposeF era, ScriptHash)])
-> V era [(PlutusPurposeF era, ScriptHash)]
-> Term era [(PlutusPurposeF era, ScriptHash)]
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era [(PlutusPurposeF era, ScriptHash)]
-> Access era Any [(PlutusPurposeF era, ScriptHash)]
-> V era [(PlutusPurposeF era, ScriptHash)]
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"acNeeded" (Rep era (PlutusPurposeF era, ScriptHash)
-> Rep era [(PlutusPurposeF era, ScriptHash)]
forall era a. Rep era a -> Rep era [a]
ListR (Rep era (PlutusPurposeF era)
-> Rep era ScriptHash -> Rep era (PlutusPurposeF era, ScriptHash)
forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR (Proof era -> Rep era (PlutusPurposeF era)
forall era. Era era => Proof era -> Rep era (PlutusPurposeF era)
ScriptPurposeR Proof era
p) Rep era ScriptHash
forall era. Era era => Rep era ScriptHash
ScriptHashR)) Access era Any [(PlutusPurposeF era, ScriptHash)]
forall era s t. Access era s t
No
    neededHashSet :: Term era (Set ScriptHash)
neededHashSet = V era (Set ScriptHash) -> Term era (Set ScriptHash)
forall era t. V era t -> Term era t
Var (V era (Set ScriptHash) -> Term era (Set ScriptHash))
-> V era (Set ScriptHash) -> Term era (Set ScriptHash)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set ScriptHash)
-> Access era Any (Set ScriptHash)
-> V era (Set ScriptHash)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"neededHashSet" (Rep era ScriptHash -> Rep era (Set ScriptHash)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era ScriptHash
forall era. Era era => Rep era ScriptHash
ScriptHashR) Access era Any (Set ScriptHash)
forall era s t. Access era s t
No
    rdmrPtrs :: Term era (Set (PlutusPointerF era))
rdmrPtrs = V era (Set (PlutusPointerF era))
-> Term era (Set (PlutusPointerF era))
forall era t. V era t -> Term era t
Var (V era (Set (PlutusPointerF era))
 -> Term era (Set (PlutusPointerF era)))
-> V era (Set (PlutusPointerF era))
-> Term era (Set (PlutusPointerF era))
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set (PlutusPointerF era))
-> Access era Any (Set (PlutusPointerF era))
-> V era (Set (PlutusPointerF era))
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"rdmrPtrs" (Rep era (PlutusPointerF era) -> Rep era (Set (PlutusPointerF era))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR (Proof era -> Rep era (PlutusPointerF era)
forall era. Era era => Proof era -> Rep era (PlutusPointerF era)
RdmrPtrR Proof era
p)) Access era Any (Set (PlutusPointerF era))
forall era s t. Access era s t
No
    plutusDataHashes :: Term era (Set DataHash)
plutusDataHashes = V era (Set DataHash) -> Term era (Set DataHash)
forall era t. V era t -> Term era t
Var (V era (Set DataHash) -> Term era (Set DataHash))
-> V era (Set DataHash) -> Term era (Set DataHash)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set DataHash)
-> Access era Any (Set DataHash)
-> V era (Set DataHash)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"plutusDataHashes" (Rep era DataHash -> Rep era (Set DataHash)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era DataHash
forall era. Era era => Rep era DataHash
DataHashR) Access era Any (Set DataHash)
forall era s t. Access era s t
No
    oneAuxdata :: Term era (TxAuxDataF era)
oneAuxdata = V era (TxAuxDataF era) -> Term era (TxAuxDataF era)
forall era t. V era t -> Term era t
Var (V era (TxAuxDataF era) -> Term era (TxAuxDataF era))
-> V era (TxAuxDataF era) -> Term era (TxAuxDataF era)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (TxAuxDataF era)
-> Access era Any (TxAuxDataF era)
-> V era (TxAuxDataF era)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"oneAuxdata" (Proof era -> Rep era (TxAuxDataF era)
forall era. Era era => Proof era -> Rep era (TxAuxDataF era)
TxAuxDataR Proof era
forall era. Reflect era => Proof era
reify) Access era Any (TxAuxDataF era)
forall era s t. Access era s t
No
    tempTxFee :: Term era Coin
tempTxFee = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (V era Coin -> Term era Coin) -> V era Coin -> Term era Coin
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempTxFee" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No
    tempTx :: Term era (TxF era)
tempTx = V era (TxF era) -> Term era (TxF era)
forall era t. V era t -> Term era t
Var (V era (TxF era) -> Term era (TxF era))
-> V era (TxF era) -> Term era (TxF era)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (TxF era)
-> Access era Any (TxF era)
-> V era (TxF era)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempTx" (Proof era -> Rep era (TxF era)
forall era. Era era => Proof era -> Rep era (TxF era)
TxR Proof era
p) Access era Any (TxF era)
forall era s t. Access era s t
No
    tempTxBody :: Term era (TxBodyF era)
tempTxBody = V era (TxBodyF era) -> Term era (TxBodyF era)
forall era t. V era t -> Term era t
Var (V era (TxBodyF era) -> Term era (TxBodyF era))
-> V era (TxBodyF era) -> Term era (TxBodyF era)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (TxBodyF era)
-> Access era Any (TxBodyF era)
-> V era (TxBodyF era)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempTxBody" (Proof era -> Rep era (TxBodyF era)
forall era. Era era => Proof era -> Rep era (TxBodyF era)
TxBodyR Proof era
forall era. Reflect era => Proof era
reify) Access era Any (TxBodyF era)
forall era s t. Access era s t
No
    tempWppHash :: Term era (Maybe ScriptIntegrityHash)
tempWppHash = V era (Maybe ScriptIntegrityHash)
-> Term era (Maybe ScriptIntegrityHash)
forall era t. V era t -> Term era t
Var (V era (Maybe ScriptIntegrityHash)
 -> Term era (Maybe ScriptIntegrityHash))
-> V era (Maybe ScriptIntegrityHash)
-> Term era (Maybe ScriptIntegrityHash)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Maybe ScriptIntegrityHash)
-> Access era Any (Maybe ScriptIntegrityHash)
-> V era (Maybe ScriptIntegrityHash)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempWppHash" (Rep era ScriptIntegrityHash -> Rep era (Maybe ScriptIntegrityHash)
forall era t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR Rep era ScriptIntegrityHash
forall era. Era era => Rep era ScriptIntegrityHash
ScriptIntegrityHashR) Access era Any (Maybe ScriptIntegrityHash)
forall era s t. Access era s t
No
    randomWppHash :: Term era ScriptIntegrityHash
randomWppHash = V era ScriptIntegrityHash -> Term era ScriptIntegrityHash
forall era t. V era t -> Term era t
Var (V era ScriptIntegrityHash -> Term era ScriptIntegrityHash)
-> V era ScriptIntegrityHash -> Term era ScriptIntegrityHash
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era ScriptIntegrityHash
-> Access era Any ScriptIntegrityHash
-> V era ScriptIntegrityHash
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"randomWppHash" Rep era ScriptIntegrityHash
forall era. Era era => Rep era ScriptIntegrityHash
ScriptIntegrityHashR Access era Any ScriptIntegrityHash
forall era s t. Access era s t
No
    tempBootWits :: Term era (Set BootstrapWitness)
tempBootWits = V era (Set BootstrapWitness) -> Term era (Set BootstrapWitness)
forall era t. V era t -> Term era t
Var (V era (Set BootstrapWitness) -> Term era (Set BootstrapWitness))
-> V era (Set BootstrapWitness) -> Term era (Set BootstrapWitness)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set BootstrapWitness)
-> Access era Any (Set BootstrapWitness)
-> V era (Set BootstrapWitness)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempBootWits" (Rep era BootstrapWitness -> Rep era (Set BootstrapWitness)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR (forall era. Era era => Rep era BootstrapWitness
BootstrapWitnessR @era)) Access era Any (Set BootstrapWitness)
forall era s t. Access era s t
No
    tempKeyWits :: Term era (Set (WitVKey 'Witness))
tempKeyWits = V era (Set (WitVKey 'Witness)) -> Term era (Set (WitVKey 'Witness))
forall era t. V era t -> Term era t
Var (V era (Set (WitVKey 'Witness))
 -> Term era (Set (WitVKey 'Witness)))
-> V era (Set (WitVKey 'Witness))
-> Term era (Set (WitVKey 'Witness))
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set (WitVKey 'Witness))
-> Access era Any (Set (WitVKey 'Witness))
-> V era (Set (WitVKey 'Witness))
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempKeyWits" (Rep era (WitVKey 'Witness) -> Rep era (Set (WitVKey 'Witness))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR (Proof era -> Rep era (WitVKey 'Witness)
forall era. Era era => Proof era -> Rep era (WitVKey 'Witness)
WitVKeyR Proof era
forall era. Reflect era => Proof era
reify)) Access era Any (Set (WitVKey 'Witness))
forall era s t. Access era s t
No
    langs :: Term era (Set Language)
langs = V era (Set Language) -> Term era (Set Language)
forall era t. V era t -> Term era t
Var (V era (Set Language) -> Term era (Set Language))
-> V era (Set Language) -> Term era (Set Language)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set Language)
-> Access era Any (Set Language)
-> V era (Set Language)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"langs" (Rep era Language -> Rep era (Set Language)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era Language
forall era. Rep era Language
LanguageR) Access era Any (Set Language)
forall era s t. Access era s t
No
    tempTotalCol :: Term era Coin
tempTotalCol = V era Coin -> Term era Coin
forall era t. V era t -> Term era t
Var (V era Coin -> Term era Coin) -> V era Coin -> Term era Coin
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName -> Rep era Coin -> Access era Any Coin -> V era Coin
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempTotalCol" Rep era Coin
forall era. Rep era Coin
CoinR Access era Any Coin
forall era s t. Access era s t
No
    prewithdrawal :: Term era (Set (Credential 'Staking))
prewithdrawal = V era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking))
forall era t. V era t -> Term era t
Var (V era (Set (Credential 'Staking))
 -> Term era (Set (Credential 'Staking)))
-> V era (Set (Credential 'Staking))
-> Term era (Set (Credential 'Staking))
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set (Credential 'Staking))
-> Access era Any (Set (Credential 'Staking))
-> V era (Set (Credential 'Staking))
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"preWithdrawal" (Rep era (Credential 'Staking)
-> Rep era (Set (Credential 'Staking))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era (Credential 'Staking)
forall era. Era era => Rep era (Credential 'Staking)
CredR) Access era Any (Set (Credential 'Staking))
forall era s t. Access era s t
No
    refAdjusted :: Term era (Set ScriptHash)
refAdjusted = V era (Set ScriptHash) -> Term era (Set ScriptHash)
forall era t. V era t -> Term era t
Var (V era (Set ScriptHash) -> Term era (Set ScriptHash))
-> V era (Set ScriptHash) -> Term era (Set ScriptHash)
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set ScriptHash)
-> Access era Any (Set ScriptHash)
-> V era (Set ScriptHash)
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"refAdjusted" (Rep era ScriptHash -> Rep era (Set ScriptHash)
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era ScriptHash
forall era. Era era => Rep era ScriptHash
ScriptHashR) Access era Any (Set ScriptHash)
forall era s t. Access era s t
No
    necessaryHashes :: Term era (Set (KeyHash 'Witness))
necessaryHashes = V era (Set (KeyHash 'Witness)) -> Term era (Set (KeyHash 'Witness))
forall era t. V era t -> Term era t
Var (V era (Set (KeyHash 'Witness))
 -> Term era (Set (KeyHash 'Witness)))
-> V era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set (KeyHash 'Witness))
-> Access era Any (Set (KeyHash 'Witness))
-> V era (Set (KeyHash 'Witness))
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"necessaryHashes" (Rep era (KeyHash 'Witness) -> Rep era (Set (KeyHash 'Witness))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era (KeyHash 'Witness)
forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) Access era Any (Set (KeyHash 'Witness))
forall era s t. Access era s t
No
    sufficientHashes :: Term era (Set (KeyHash 'Witness))
sufficientHashes = V era (Set (KeyHash 'Witness)) -> Term era (Set (KeyHash 'Witness))
forall era t. V era t -> Term era t
Var (V era (Set (KeyHash 'Witness))
 -> Term era (Set (KeyHash 'Witness)))
-> V era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
forall a b. (a -> b) -> a -> b
$ Proof era
-> TestName
-> Rep era (Set (KeyHash 'Witness))
-> Access era Any (Set (KeyHash 'Witness))
-> V era (Set (KeyHash 'Witness))
forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"sufficientHashes" (Rep era (KeyHash 'Witness) -> Rep era (Set (KeyHash 'Witness))
forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR Rep era (KeyHash 'Witness)
forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) Access era Any (Set (KeyHash 'Witness))
forall era s t. Access era s t
No

txBodyStage ::
  Reflect era =>
  UnivSize ->
  Proof era ->
  Subst era ->
  Gen (Subst era)
txBodyStage :: forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
txBodyStage UnivSize
sizes Proof era
proof Subst era
subst0 = do
  let preds :: [Pred era]
preds = UnivSize -> Proof era -> [Pred era]
forall era.
(HasCallStack, Reflect era) =>
UnivSize -> Proof era -> [Pred era]
txBodyPreds UnivSize
sizes Proof era
proof
  Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
forall era.
Era era =>
Proof era
-> OrderInfo -> [Pred era] -> Subst era -> Gen (Subst era)
toolChainSub Proof era
proof OrderInfo
standardOrderInfo [Pred era]
preds Subst era
subst0

-- ===============================================================

balanceMap :: Ord k => [(k, Coin)] -> Map k t -> Lens' t Coin -> Map k t
balanceMap :: forall k t.
Ord k =>
[(k, Coin)] -> Map k t -> Lens' t Coin -> Map k t
balanceMap [(k, Coin)]
pairs Map k t
m0 Lens' t Coin
l = (Map k t -> (k, Coin) -> Map k t)
-> Map k t -> [(k, Coin)] -> Map k t
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Map k t -> (k, Coin) -> Map k t
accum Map k t
m0 [(k, Coin)]
pairs
  where
    accum :: Map k t -> (k, Coin) -> Map k t
accum Map k t
m (k
k, Coin
thecoin) = (t -> t) -> k -> Map k t -> Map k t
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\t
t -> t
t t -> (t -> t) -> t
forall a b. a -> (a -> b) -> b
& (Coin -> Identity Coin) -> t -> Identity t
Lens' t Coin
l ((Coin -> Identity Coin) -> t -> Identity t) -> Coin -> t -> t
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Coin
thecoin Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> t
t t -> Getting Coin t Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin t Coin
Lens' t Coin
l)) k
k Map k t
m

-- | Adjust the Coin part of the TxOut in the 'utxo' map for the TxIn 'feeTxIn' by adding 'txfee'
adjustFeeInput :: (HasCallStack, Reflect era) => Env era -> Typed (Env era)
adjustFeeInput :: forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env era
env = case Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
forall era. Reflect era => Proof era
reify of
  u :: Term era (Map TxIn (TxOutF era))
u@(Var V era (Map TxIn (TxOutF era))
utxoV) -> do
    TxIn
feeinput <- Env era -> Term era TxIn -> Typed TxIn
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era TxIn
forall era. Era era => Term era TxIn
feeTxIn
    Coin
feecoin <- Env era -> Term era Coin -> Typed Coin
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era Coin
forall era. Era era => Term era Coin
txfee
    Map TxIn (TxOutF era)
utxomap <- Env era
-> Term era (Map TxIn (TxOutF era))
-> Typed (Map TxIn (TxOutF era))
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map TxIn (TxOutF era))
u
    Env era -> Typed (Env era)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (V era (Map TxIn (TxOutF era))
-> Map TxIn (TxOutF era) -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era (Map TxIn (TxOutF era))
utxoV ([(TxIn, Coin)]
-> Map TxIn (TxOutF era)
-> Lens' (TxOutF era) Coin
-> Map TxIn (TxOutF era)
forall k t.
Ord k =>
[(k, Coin)] -> Map k t -> Lens' t Coin -> Map k t
balanceMap [(TxIn
feeinput, Coin
feecoin)] Map TxIn (TxOutF era)
utxomap (Coin -> f Coin) -> TxOutF era -> f (TxOutF era)
forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
Lens' (TxOutF era) Coin
outputCoinL) Env era
env)
  Term era (Map TxIn (TxOutF era))
other -> [TestName] -> Typed (Env era)
forall a. [TestName] -> Typed a
failT [TestName
"utxo does not match a Var Term: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Term era (Map TxIn (TxOutF era)) -> TestName
forall a. Show a => a -> TestName
show Term era (Map TxIn (TxOutF era))
other]

-- | Adjust UTxO image of 'collateral' to pay for the collateral fees. Do this by
--   adding 'extraCol' to the TxOuts associated with col inputs
adjustColInput ::
  (HasCallStack, Reflect era) =>
  -- Term era (TxIn ) ->
  -- Term era Coin ->
  -- Term era Coin ->
  Env era ->
  Typed (Gen (Env era))
adjustColInput :: forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env = do
  let utxoterm :: Term era (Map TxIn (TxOutF era))
utxoterm = Proof era -> Term era (Map TxIn (TxOutF era))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
forall era. Reflect era => Proof era
reify
      utxoV :: V era (Map TxIn (TxOutF era))
utxoV = Term era (Map TxIn (TxOutF era)) -> V era (Map TxIn (TxOutF era))
forall era t. Term era t -> V era t
unVar Term era (Map TxIn (TxOutF era))
utxoterm
  Coin
extracoin <- Env era -> Term era Coin -> Typed Coin
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era Coin
forall era. Era era => Term era Coin
extraCol
  Map TxIn (TxOutF era)
utxomap <- Env era
-> Term era (Map TxIn (TxOutF era))
-> Typed (Map TxIn (TxOutF era))
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map TxIn (TxOutF era))
utxoterm
  Set TxIn
col <- Env era -> Term era (Set TxIn) -> Typed (Set TxIn)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Set TxIn)
forall era. Era era => Term era (Set TxIn)
collateral
  case [TxIn]
-> Map TxIn (TxOutF era)
-> Coin
-> Lens' (TxOutF era) Coin
-> Maybe (Map TxIn (TxOutF era))
forall k v.
(Ord k, Show k) =>
[k] -> Map k v -> Coin -> Lens' v Coin -> Maybe (Map k v)
adjustC (Set TxIn -> [TxIn]
forall a. Set a -> [a]
Set.toList Set TxIn
col) Map TxIn (TxOutF era)
utxomap Coin
extracoin (Coin -> f Coin) -> TxOutF era -> f (TxOutF era)
forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
Lens' (TxOutF era) Coin
outputCoinL of
    Maybe (Map TxIn (TxOutF era))
Nothing -> Gen (Env era) -> Typed (Gen (Env era))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Gen (Env era)
forall a. a
discard
    Just Map TxIn (TxOutF era)
newutxo -> do
      let env2 :: Env era
env2 = V era (Map TxIn (TxOutF era))
-> Map TxIn (TxOutF era) -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era (Map TxIn (TxOutF era))
utxoV Map TxIn (TxOutF era)
newutxo Env era
env
      (Env era
env5, TxBodyF era
body) <- (TxBodyF era -> TxBodyF era -> TxBodyF era)
-> Term era (TxBodyF era)
-> Target era (TxBodyF era)
-> Env era
-> Typed (Env era, TxBodyF era)
forall a b era.
(a -> b -> a)
-> Term era a -> Target era b -> Env era -> Typed (Env era, b)
updateTarget TxBodyF era -> TxBodyF era -> TxBodyF era
forall x. x -> x -> x
override Term era (TxBodyF era)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm (Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> Target era (TxBodyF era)
forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget Term era Coin
forall era. Era era => Term era Coin
txfee Term era (Maybe ScriptIntegrityHash)
forall era. Era era => Term era (Maybe ScriptIntegrityHash)
wppHash Term era Coin
forall era. Era era => Term era Coin
totalCol) Env era
env2
      (Env era
env6, TxF era
_) <-
        (TxF era -> TxF era -> TxF era)
-> Term era (TxF era)
-> Target era (TxF era)
-> Env era
-> Typed (Env era, TxF era)
forall a b era.
(a -> b -> a)
-> Term era a -> Target era b -> Env era -> Typed (Env era, b)
updateTarget TxF era -> TxF era -> TxF era
forall x. x -> x -> x
override Term era (TxF era)
forall era. Reflect era => Term era (TxF era)
txterm (Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> Target era (TxF era)
forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> Target era (TxF era)
txTarget (Rep era (TxBodyF era) -> TxBodyF era -> Term era (TxBodyF era)
forall era t. Rep era t -> t -> Term era t
Lit (Proof era -> Rep era (TxBodyF era)
forall era. Era era => Proof era -> Rep era (TxBodyF era)
TxBodyR Proof era
forall era. Reflect era => Proof era
reify) TxBodyF era
body) Term era (Set BootstrapWitness)
forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits Term era (Set (WitVKey 'Witness))
forall era. Reflect era => Term era (Set (WitVKey 'Witness))
keyWits) Env era
env5
      Gen (Env era) -> Typed (Gen (Env era))
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era -> Gen (Env era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Env era
env6)

-- | Adjust the part of the UTxO that maps the 'collateral' inputs, to pay the collateral fee.
--   This will adjust 1 or more of the TxOuts associated with the collateral , to make up the difference.
--   It may happen on rare occaisions, there is not enough Coin to make the adjustment, so return Nothing
adjustC :: (Ord k, Show k) => [k] -> Map k v -> Coin -> Lens' v Coin -> Maybe (Map k v)
adjustC :: forall k v.
(Ord k, Show k) =>
[k] -> Map k v -> Coin -> Lens' v Coin -> Maybe (Map k v)
adjustC [] Map k v
_ Coin
extra Lens' v Coin
_ | Coin
extra Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
< (Integer -> Coin
Coin Integer
0) = Maybe (Map k v)
forall a. Maybe a
Nothing
adjustC [] Map k v
m Coin
_ Lens' v Coin
_ = Map k v -> Maybe (Map k v)
forall a. a -> Maybe a
Just Map k v
m
adjustC (k
i : [k]
is) Map k v
m extra :: Coin
extra@(Coin Integer
n) Lens' v Coin
coinL = case Integer -> Integer -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Integer
n Integer
0 of
  Ordering
EQ -> Map k v -> Maybe (Map k v)
forall a. a -> Maybe a
Just Map k v
m
  Ordering
GT -> Map k v -> Maybe (Map k v)
forall a. a -> Maybe a
Just ((v -> v) -> k -> Map k v -> Map k v
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust v -> v
addextra k
i Map k v
m)
    where
      addextra :: v -> v
addextra v
outf = v
outf v -> (v -> v) -> v
forall a b. a -> (a -> b) -> b
& (Coin -> Identity Coin) -> v -> Identity v
Lens' v Coin
coinL ((Coin -> Identity Coin) -> v -> Identity v) -> Coin -> v -> v
forall s t a b. ASetter s t a b -> b -> s -> t
.~ ((v
outf v -> Getting Coin v Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin v Coin
Lens' v Coin
coinL) Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
extra)
  Ordering
LT ->
    if Integer
ex Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer
0
      then Map k v -> Maybe (Map k v)
forall a. a -> Maybe a
Just ((v -> v) -> k -> Map k v -> Map k v
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust v -> v
subextra k
i Map k v
m)
      else [k] -> Map k v -> Coin -> Lens' v Coin -> Maybe (Map k v)
forall k v.
(Ord k, Show k) =>
[k] -> Map k v -> Coin -> Lens' v Coin -> Maybe (Map k v)
adjustC [k]
is ((v -> v) -> k -> Map k v -> Map k v
forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust v -> v
subextra k
i Map k v
m) Coin
amount (Coin -> f Coin) -> v -> f v
Lens' v Coin
coinL
    where
      amount :: Coin
amount@(Coin Integer
ex) = case k -> Map k v -> Maybe v
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
i Map k v
m of
        Just v
outf -> (v
outf v -> Getting Coin v Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin v Coin
Lens' v Coin
coinL) Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
extra Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> (Integer -> Coin
Coin Integer
1)
        Maybe v
Nothing -> TestName -> Coin
forall a. HasCallStack => TestName -> a
error (TestName
"Collateral input: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ k -> TestName
forall a. Show a => a -> TestName
show k
i TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
" is not found in UTxO in 'adjust'")
      subextra :: v -> v
subextra v
outf = v
outf v -> (v -> v) -> v
forall a b. a -> (a -> b) -> b
& (Coin -> Identity Coin) -> v -> Identity v
Lens' v Coin
coinL ((Coin -> Identity Coin) -> v -> Identity v) -> Coin -> v -> v
forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Integer -> Coin
Coin (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
1 (Coin -> Integer
unCoin ((v
outf v -> Getting Coin v Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin v Coin
Lens' v Coin
coinL) Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
extra))))

updateVal :: (a -> b -> a) -> Term era a -> b -> Env era -> Typed (Env era)
updateVal :: forall a b era.
(a -> b -> a) -> Term era a -> b -> Env era -> Typed (Env era)
updateVal a -> b -> a
adjust term :: Term era a
term@(Var V era a
v) b
delta Env era
env = do
  a
varV <- Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term
  Env era -> Typed (Env era)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era -> Typed (Env era)) -> Env era -> Typed (Env era)
forall a b. (a -> b) -> a -> b
$ V era a -> a -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era a
v (a -> b -> a
adjust a
varV b
delta) Env era
env
updateVal a -> b -> a
_ Term era a
v b
_ Env era
_ = [TestName] -> Typed (Env era)
forall a. [TestName] -> Typed a
failT [TestName
"Non Var in updateVal: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Term era a -> TestName
forall a. Show a => a -> TestName
show Term era a
v]

updateTerm :: (a -> b -> a) -> Term era a -> Term era b -> Env era -> Typed (Env era)
updateTerm :: forall a b era.
(a -> b -> a)
-> Term era a -> Term era b -> Env era -> Typed (Env era)
updateTerm a -> b -> a
adjust term :: Term era a
term@(Var V era a
v) Term era b
delta Env era
env = do
  a
varV <- Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term
  b
deltaV <- Env era -> Term era b -> Typed b
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era b
delta
  Env era -> Typed (Env era)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Env era -> Typed (Env era)) -> Env era -> Typed (Env era)
forall a b. (a -> b) -> a -> b
$ V era a -> a -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era a
v (a -> b -> a
adjust a
varV b
deltaV) Env era
env
updateTerm a -> b -> a
_ Term era a
v Term era b
_ Env era
_ = [TestName] -> Typed (Env era)
forall a. [TestName] -> Typed a
failT [TestName
"Non Var in updateTerm: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Term era a -> TestName
forall a. Show a => a -> TestName
show Term era a
v]

updateTarget :: (a -> b -> a) -> Term era a -> Target era b -> Env era -> Typed (Env era, b)
updateTarget :: forall a b era.
(a -> b -> a)
-> Term era a -> Target era b -> Env era -> Typed (Env era, b)
updateTarget a -> b -> a
adjust term :: Term era a
term@(Var V era a
v) Target era b
delta Env era
env = do
  a
varV <- Env era -> Term era a -> Typed a
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term
  b
deltaV <- Env era -> Target era b -> Typed b
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env Target era b
delta
  (Env era, b) -> Typed (Env era, b)
forall a. a -> Typed a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Env era, b) -> Typed (Env era, b))
-> (Env era, b) -> Typed (Env era, b)
forall a b. (a -> b) -> a -> b
$ (V era a -> a -> Env era -> Env era
forall era t. V era t -> t -> Env era -> Env era
storeVar V era a
v (a -> b -> a
adjust a
varV b
deltaV) Env era
env, b
deltaV)
updateTarget a -> b -> a
_ Term era a
v Target era b
_ Env era
_ = [TestName] -> Typed (Env era, b)
forall a. [TestName] -> Typed a
failT [TestName
"Non Var in updateTarget: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Term era a -> TestName
forall a. Show a => a -> TestName
show Term era a
v]

override :: x -> x -> x
override :: forall x. x -> x -> x
override x
_ x
y = x
y

-- ========================================

genTxAndLedger :: Reflect era => UnivSize -> Proof era -> Gen (LedgerState era, Tx era, Env era)
genTxAndLedger :: forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (LedgerState era, Tx era, Env era)
genTxAndLedger UnivSize
sizes Proof era
proof = do
  Subst era
subst <-
    ( Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
sizes Proof era
proof
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
sizes Proof era
proof
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
sizes Proof era
proof
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
sizes Proof era
proof
        Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
txBodyStage UnivSize
sizes Proof era
proof
    )
  Env era
env0 <- Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv
  Env era
env1 <- Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Env era -> Typed (Env era)
forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env era
env0
  Env era
env2 <- Typed (Gen (Env era)) -> Gen (Env era)
forall t. HasCallStack => Typed t -> t
errorTyped (Typed (Gen (Env era)) -> Gen (Env era))
-> Typed (Gen (Env era)) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Env era -> Typed (Gen (Env era))
forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env1
  LedgerState era
ledger <- Typed (LedgerState era) -> Gen (LedgerState era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (LedgerState era) -> Gen (LedgerState era))
-> Typed (LedgerState era) -> Gen (LedgerState era)
forall a b. (a -> b) -> a -> b
$ Env era
-> RootTarget era (LedgerState era) (LedgerState era)
-> Typed (LedgerState era)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env2 (Proof era -> RootTarget era (LedgerState era) (LedgerState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
proof)
  (TxF Proof era
_ Tx era
tx) <- Typed (TxF era) -> Gen (TxF era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V era (TxF era) -> Env era -> Typed (TxF era)
forall era t. V era t -> Env era -> Typed t
findVar (Term era (TxF era) -> V era (TxF era)
forall era t. Term era t -> V era t
unVar Term era (TxF era)
forall era. Reflect era => Term era (TxF era)
txterm) Env era
env2)
  (LedgerState era, Tx era, Env era)
-> Gen (LedgerState era, Tx era, Env era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LedgerState era
ledger, Tx era
tx, Env era
env2)

genTxAndNewEpoch :: Reflect era => UnivSize -> Proof era -> Gen (NewEpochState era, Tx era, Env era)
genTxAndNewEpoch :: forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (NewEpochState era, Tx era, Env era)
genTxAndNewEpoch UnivSize
sizes Proof era
proof = do
  Subst era
subst <-
    Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
txBodyStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
epochStateStage Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
newEpochStateStage Proof era
proof
  Env era
env0 <- Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv
  Env era
env1 <- Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Env era -> Typed (Env era)
forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env era
env0
  Env era
env2 <- Typed (Gen (Env era)) -> Gen (Env era)
forall t. HasCallStack => Typed t -> t
errorTyped (Typed (Gen (Env era)) -> Gen (Env era))
-> Typed (Gen (Env era)) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Env era -> Typed (Gen (Env era))
forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env1
  NewEpochState era
newepochst <- Typed (NewEpochState era) -> Gen (NewEpochState era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (NewEpochState era) -> Gen (NewEpochState era))
-> Typed (NewEpochState era) -> Gen (NewEpochState era)
forall a b. (a -> b) -> a -> b
$ Env era
-> RootTarget era (NewEpochState era) (NewEpochState era)
-> Typed (NewEpochState era)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env2 (Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof era
proof)
  TxF Proof era
_ Tx era
tx <- Typed (TxF era) -> Gen (TxF era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V era (TxF era) -> Env era -> Typed (TxF era)
forall era t. V era t -> Env era -> Typed t
findVar (Term era (TxF era) -> V era (TxF era)
forall era t. Term era t -> V era t
unVar Term era (TxF era)
forall era. Reflect era => Term era (TxF era)
txterm) Env era
env2)
  (NewEpochState era, Tx era, Env era)
-> Gen (NewEpochState era, Tx era, Env era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NewEpochState era
newepochst, Tx era
tx, Env era
env2)

demoTxNes :: IO ()
demoTxNes :: IO ()
demoTxNes = do
  let proof :: Proof ConwayEra
proof = Proof ConwayEra
Conway
  (NewEpochState ConwayEra
nes, AlonzoTx ConwayEra
_tx, Env ConwayEra
env) <- Gen (NewEpochState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
-> IO (NewEpochState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
forall a. Gen a -> IO a
generate (Gen (NewEpochState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
 -> IO (NewEpochState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra))
-> Gen (NewEpochState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
-> IO (NewEpochState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
forall a b. (a -> b) -> a -> b
$ UnivSize
-> Proof ConwayEra
-> Gen (NewEpochState ConwayEra, Tx ConwayEra, Env ConwayEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (NewEpochState era, Tx era, Env era)
genTxAndNewEpoch UnivSize
forall a. Default a => a
def Proof ConwayEra
proof
  PDoc -> IO ()
forall a. Show a => a -> IO ()
print (Proof ConwayEra -> NewEpochState ConwayEra -> PDoc
forall era. Reflect era => Proof era -> NewEpochState era -> PDoc
psNewEpochState Proof ConwayEra
proof NewEpochState ConwayEra
nes)
  Map (KeyHash 'StakePool) PoolParams
pools <- Typed (Map (KeyHash 'StakePool) PoolParams)
-> IO (Map (KeyHash 'StakePool) PoolParams)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Map (KeyHash 'StakePool) PoolParams)
 -> IO (Map (KeyHash 'StakePool) PoolParams))
-> Typed (Map (KeyHash 'StakePool) PoolParams)
-> IO (Map (KeyHash 'StakePool) PoolParams)
forall a b. (a -> b) -> a -> b
$ Env ConwayEra
-> Term ConwayEra (Map (KeyHash 'StakePool) PoolParams)
-> Typed (Map (KeyHash 'StakePool) PoolParams)
forall era t. Env era -> Term era t -> Typed t
runTerm Env ConwayEra
env Term ConwayEra (Map (KeyHash 'StakePool) PoolParams)
forall era.
EraCertState era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
  Map (Credential 'Staking) (KeyHash 'StakePool)
deleg <- Typed (Map (Credential 'Staking) (KeyHash 'StakePool))
-> IO (Map (Credential 'Staking) (KeyHash 'StakePool))
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Map (Credential 'Staking) (KeyHash 'StakePool))
 -> IO (Map (Credential 'Staking) (KeyHash 'StakePool)))
-> Typed (Map (Credential 'Staking) (KeyHash 'StakePool))
-> IO (Map (Credential 'Staking) (KeyHash 'StakePool))
forall a b. (a -> b) -> a -> b
$ Env ConwayEra
-> Term ConwayEra (Map (Credential 'Staking) (KeyHash 'StakePool))
-> Typed (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era t. Env era -> Term era t -> Typed t
runTerm Env ConwayEra
env Term ConwayEra (Map (Credential 'Staking) (KeyHash 'StakePool))
forall era.
EraCertState era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations
  Map (Credential 'Staking) Coin
stak <- Typed (Map (Credential 'Staking) Coin)
-> IO (Map (Credential 'Staking) Coin)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Map (Credential 'Staking) Coin)
 -> IO (Map (Credential 'Staking) Coin))
-> Typed (Map (Credential 'Staking) Coin)
-> IO (Map (Credential 'Staking) Coin)
forall a b. (a -> b) -> a -> b
$ Env ConwayEra
-> Term ConwayEra (Map (Credential 'Staking) Coin)
-> Typed (Map (Credential 'Staking) Coin)
forall era t. Env era -> Term era t -> Typed t
runTerm Env ConwayEra
env Term ConwayEra (Map (Credential 'Staking) Coin)
forall era. Era era => Term era (Map (Credential 'Staking) Coin)
instantStakeTerm
  PDoc -> IO ()
forall ann. Doc ann -> IO ()
putDoc (TestName -> PDoc
forall a. TestName -> Doc a
ppString TestName
"\nPool " PDoc -> PDoc -> PDoc
forall a. Semigroup a => a -> a -> a
<> Map (KeyHash 'StakePool) PoolParams -> PDoc
forall t. PrettyA t => t -> PDoc
prettyA Map (KeyHash 'StakePool) PoolParams
pools)
  PDoc -> IO ()
forall ann. Doc ann -> IO ()
putDoc (TestName -> PDoc
forall a. TestName -> Doc a
ppString TestName
"\nDeleg " PDoc -> PDoc -> PDoc
forall a. Semigroup a => a -> a -> a
<> Map (Credential 'Staking) (KeyHash 'StakePool) -> PDoc
forall t. PrettyA t => t -> PDoc
prettyA Map (Credential 'Staking) (KeyHash 'StakePool)
deleg)
  PDoc -> IO ()
forall ann. Doc ann -> IO ()
putDoc (TestName -> PDoc
forall a. TestName -> Doc a
ppString TestName
"\nStake " PDoc -> PDoc -> PDoc
forall a. Semigroup a => a -> a -> a
<> Map (Credential 'Staking) Coin -> PDoc
forall t. PrettyA t => t -> PDoc
prettyA Map (Credential 'Staking) Coin
stak)
  let distr :: PoolDistr
distr =
        SnapShot -> PoolDistr
calculatePoolDistr
          ( Stake
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (KeyHash 'StakePool) PoolParams
-> SnapShot
SnapShot
              (VMap VB VP (Credential 'Staking) (CompactForm Coin) -> Stake
Stake (Map (Credential 'Staking) (CompactForm Coin)
-> VMap VB VP (Credential 'Staking) (CompactForm Coin)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap ((Coin -> CompactForm Coin)
-> Map (Credential 'Staking) Coin
-> Map (Credential 'Staking) (CompactForm Coin)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
Coin -> CompactForm Coin
UMap.compactCoinOrError Map (Credential 'Staking) Coin
stak)))
              (Map (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap Map (Credential 'Staking) (KeyHash 'StakePool)
deleg)
              (Map (KeyHash 'StakePool) PoolParams
-> VMap VB VB (KeyHash 'StakePool) PoolParams
forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap Map (KeyHash 'StakePool) PoolParams
pools)
          )
  PDoc -> IO ()
forall ann. Doc ann -> IO ()
putDoc (TestName -> PDoc
forall a. TestName -> Doc a
ppString TestName
"\nPoolDistr " PDoc -> PDoc -> PDoc
forall a. Semigroup a => a -> a -> a
<> PoolDistr -> PDoc
forall t. PrettyA t => t -> PDoc
prettyA PoolDistr
distr)
  Proof ConwayEra -> Env ConwayEra -> TestName -> IO ()
forall era. Proof era -> Env era -> TestName -> IO ()
goRepl Proof ConwayEra
proof Env ConwayEra
env TestName
""

demoTx :: IO ()
demoTx :: IO ()
demoTx = do
  let proof :: Proof ConwayEra
proof = Proof ConwayEra
Conway
  (LedgerState ConwayEra
ls, AlonzoTx ConwayEra
tx, Env ConwayEra
env) <- Gen (LedgerState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
-> IO (LedgerState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
forall a. Gen a -> IO a
generate (Gen (LedgerState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
 -> IO (LedgerState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra))
-> Gen (LedgerState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
-> IO (LedgerState ConwayEra, AlonzoTx ConwayEra, Env ConwayEra)
forall a b. (a -> b) -> a -> b
$ UnivSize
-> Proof ConwayEra
-> Gen (LedgerState ConwayEra, Tx ConwayEra, Env ConwayEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (LedgerState era, Tx era, Env era)
genTxAndLedger UnivSize
forall a. Default a => a
def Proof ConwayEra
proof
  PDoc -> IO ()
forall a. Show a => a -> IO ()
print (Proof ConwayEra -> LedgerState ConwayEra -> PDoc
forall era. Reflect era => Proof era -> LedgerState era -> PDoc
pcLedgerState Proof ConwayEra
proof LedgerState ConwayEra
ls)
  PDoc -> IO ()
forall a. Show a => a -> IO ()
print (Proof ConwayEra -> Tx ConwayEra -> PDoc
forall era. Proof era -> Tx era -> PDoc
pcTx Proof ConwayEra
proof Tx ConwayEra
AlonzoTx ConwayEra
tx)
  Proof ConwayEra -> Env ConwayEra -> TestName -> IO ()
forall era. Proof era -> Env era -> TestName -> IO ()
goRepl Proof ConwayEra
proof Env ConwayEra
env TestName
""

-- ================================================================

gone :: Gen (IO ())
gone :: Gen (IO ())
gone = do
  TxIx
txIx <- Gen TxIx
forall a. Arbitrary a => Gen a
arbitrary
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
      sizes :: UnivSize
sizes = UnivSize
forall a. Default a => a
def
  (LedgerState BabbageEra
ledgerstate, AlonzoTx BabbageEra
tx, Env BabbageEra
env) <- UnivSize
-> Proof BabbageEra
-> Gen (LedgerState BabbageEra, Tx BabbageEra, Env BabbageEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (LedgerState era, Tx era, Env era)
genTxAndLedger UnivSize
sizes Proof BabbageEra
proof
  SlotNo
slot <- Typed SlotNo -> Gen SlotNo
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V BabbageEra SlotNo -> Env BabbageEra -> Typed SlotNo
forall era t. V era t -> Env era -> Typed t
findVar (Term BabbageEra SlotNo -> V BabbageEra SlotNo
forall era t. Term era t -> V era t
unVar Term BabbageEra SlotNo
forall era. Era era => Term era SlotNo
currentSlot) Env BabbageEra
env)
  (PParamsF Proof BabbageEra
_ PParams BabbageEra
pp) <- Typed (PParamsF BabbageEra) -> Gen (PParamsF BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V BabbageEra (PParamsF BabbageEra)
-> Env BabbageEra -> Typed (PParamsF BabbageEra)
forall era t. V era t -> Env era -> Typed t
findVar (Term BabbageEra (PParamsF BabbageEra)
-> V BabbageEra (PParamsF BabbageEra)
forall era t. Term era t -> V era t
unVar (Proof BabbageEra -> Term BabbageEra (PParamsF BabbageEra)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof BabbageEra
proof)) Env BabbageEra
env)
  ChainAccountState
accntState <- Typed ChainAccountState -> Gen ChainAccountState
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Env BabbageEra
-> RootTarget BabbageEra ChainAccountState ChainAccountState
-> Typed ChainAccountState
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env BabbageEra
env RootTarget BabbageEra ChainAccountState ChainAccountState
forall era.
Era era =>
RootTarget era ChainAccountState ChainAccountState
accountStateT)
  Map TxIn (TxOutF BabbageEra)
utxo1 <- Typed (Map TxIn (TxOutF BabbageEra))
-> Gen (Map TxIn (TxOutF BabbageEra))
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V BabbageEra (Map TxIn (TxOutF BabbageEra))
-> Env BabbageEra -> Typed (Map TxIn (TxOutF BabbageEra))
forall era t. V era t -> Env era -> Typed t
findVar (Term BabbageEra (Map TxIn (TxOutF BabbageEra))
-> V BabbageEra (Map TxIn (TxOutF BabbageEra))
forall era t. Term era t -> V era t
unVar (Proof BabbageEra -> Term BabbageEra (Map TxIn (TxOutF BabbageEra))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof BabbageEra
proof)) Env BabbageEra
env)
  let lenv :: LedgerEnv BabbageEra
lenv = SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams BabbageEra
-> ChainAccountState
-> LedgerEnv BabbageEra
forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
LedgerEnv SlotNo
slot Maybe EpochNo
forall a. Maybe a
Nothing TxIx
txIx PParams BabbageEra
pp ChainAccountState
accntState
  -- putStrLn (show (pcTx Babbage tx))
  IO () -> Gen (IO ())
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IO () -> Gen (IO ())) -> IO () -> Gen (IO ())
forall a b. (a -> b) -> a -> b
$ case Proof BabbageEra
-> RuleContext 'Transition (EraRule "LEDGER" BabbageEra)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" BabbageEra)))
     (State (EraRule "LEDGER" BabbageEra))
forall era.
Era era =>
Proof era
-> RuleContext 'Transition (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era))
applySTSByProof Proof BabbageEra
proof ((Environment (BabbageLEDGER BabbageEra),
 State (BabbageLEDGER BabbageEra),
 Signal (BabbageLEDGER BabbageEra))
-> TRC (BabbageLEDGER BabbageEra)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv BabbageEra
Environment (BabbageLEDGER BabbageEra)
lenv, State (BabbageLEDGER BabbageEra)
LedgerState BabbageEra
ledgerstate, AlonzoTx BabbageEra
Signal (BabbageLEDGER BabbageEra)
tx)) of
    Right State (EraRule "LEDGER" BabbageEra)
_ledgerState' -> do
      -- putStrLn (show (pcTx Babbage tx))
      TestName -> IO ()
putStrLn TestName
"SUCCESS"
    Left NonEmpty (PredicateFailure (EraRule "LEDGER" BabbageEra))
errs -> do
      TestName -> IO ()
putStrLn TestName
"FAIL"
      PDoc -> IO ()
forall a. Show a => a -> IO ()
print (PDoc -> IO ()) -> PDoc -> IO ()
forall a b. (a -> b) -> a -> b
$ Proof BabbageEra
-> Map TxIn (TxOutF BabbageEra) -> Tx BabbageEra -> PDoc
forall era.
Reflect era =>
Proof era -> Map TxIn (TxOutF era) -> Tx era -> PDoc
pgenTx Proof BabbageEra
proof Map TxIn (TxOutF BabbageEra)
utxo1 Tx BabbageEra
AlonzoTx BabbageEra
tx
      PDoc -> IO ()
forall a. Show a => a -> IO ()
print (PDoc -> IO ()) -> PDoc -> IO ()
forall a b. (a -> b) -> a -> b
$ NonEmpty (ShelleyLedgerPredFailure BabbageEra) -> PDoc
forall t. PrettyA t => t -> PDoc
prettyA NonEmpty (PredicateFailure (EraRule "LEDGER" BabbageEra))
NonEmpty (ShelleyLedgerPredFailure BabbageEra)
errs
      Proof BabbageEra -> Env BabbageEra -> TestName -> IO ()
forall era. Proof era -> Env era -> TestName -> IO ()
goRepl Proof BabbageEra
Babbage Env BabbageEra
env TestName
""

test :: Maybe Int -> IO ()
test :: Maybe Int -> IO ()
test (Just Int
seed) = IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Gen (IO ()) -> IO (IO ())
forall a. Int -> Gen a -> IO a
generateWithSeed Int
seed Gen (IO ())
gone
test Maybe Int
Nothing = do
  Int
seed <- Gen Int -> IO Int
forall a. Gen a -> IO a
generate Gen Int
forall a. Arbitrary a => Gen a
arbitrary
  TestName -> IO ()
putStrLn (TestName
"SEED = " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Int -> TestName
forall a. Show a => a -> TestName
show Int
seed)
  IO (IO ()) -> IO ()
forall (m :: * -> *) a. Monad m => m (m a) -> m a
join (IO (IO ()) -> IO ()) -> IO (IO ()) -> IO ()
forall a b. (a -> b) -> a -> b
$ Int -> Gen (IO ()) -> IO (IO ())
forall a. Int -> Gen a -> IO a
generateWithSeed Int
seed Gen (IO ())
gone

bad :: [Int]
bad :: [Int]
bad = [] -- [3, 8, 13, 41, 50, 60, 65, 82, 99, 100, 109, 112]

go :: Int -> IO ()
go :: Int -> IO ()
go Int
n = [IO ()] -> IO ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [Int -> IO ()
forall a. Show a => a -> IO ()
print Int
i IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Int -> IO ()
test (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i) | Int
i <- [Int
n .. Int
113], Int -> [Int] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
notElem Int
i [Int]
bad]

-- ========================================

-- ==============================

-- | Pretty print the fields of a Randomly generated TxBody, except resolve the
--   inputs with the given Ut map.
pgenTxBodyField ::
  Reflect era =>
  Proof era ->
  Map TxIn (TxOutF era) ->
  TxBodyField era ->
  [(Text, PDoc)]
pgenTxBodyField :: forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era) -> TxBodyField era -> [(Text, PDoc)]
pgenTxBodyField Proof era
proof Map TxIn (TxOutF era)
ut TxBodyField era
x = case TxBodyField era
x of
  Inputs Set TxIn
s -> [(TestName -> Text
pack TestName
"spend inputs", Map TxIn (TxOutF era) -> PDoc
forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc (Map TxIn (TxOutF era) -> Set TxIn -> Map TxIn (TxOutF era)
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map TxIn (TxOutF era)
ut Set TxIn
s))]
  Collateral Set TxIn
s -> [(TestName -> Text
pack TestName
"coll inputs", Map TxIn (TxOutF era) -> PDoc
forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc (Map TxIn (TxOutF era) -> Set TxIn -> Map TxIn (TxOutF era)
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map TxIn (TxOutF era)
ut Set TxIn
s))]
  RefInputs Set TxIn
s -> [(TestName -> Text
pack TestName
"ref inputs", Map TxIn (TxOutF era) -> PDoc
forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc (Map TxIn (TxOutF era) -> Set TxIn -> Map TxIn (TxOutF era)
forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map TxIn (TxOutF era)
ut Set TxIn
s))]
  TxBodyField era
other -> Proof era -> TxBodyField era -> [(Text, PDoc)]
forall era. Proof era -> TxBodyField era -> [(Text, PDoc)]
pcTxBodyField Proof era
proof TxBodyField era
other

pgenTxBody ::
  Reflect era => Proof era -> TxBody era -> Map TxIn (TxOutF era) -> PDoc
pgenTxBody :: forall era.
Reflect era =>
Proof era -> TxBody era -> Map TxIn (TxOutF era) -> PDoc
pgenTxBody Proof era
proof TxBody era
txBody Map TxIn (TxOutF era)
ut = Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"TxBody " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> TestName -> Text
pack (Proof era -> TestName
forall a. Show a => a -> TestName
show Proof era
proof)) [(Text, PDoc)]
pairs
  where
    fields :: [TxBodyField era]
fields = Proof era -> TxBody era -> [TxBodyField era]
forall era. Proof era -> TxBody era -> [TxBodyField era]
abstractTxBody Proof era
proof TxBody era
txBody
    pairs :: [(Text, PDoc)]
pairs = (TxBodyField era -> [(Text, PDoc)])
-> [TxBodyField era] -> [(Text, PDoc)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Proof era
-> Map TxIn (TxOutF era) -> TxBodyField era -> [(Text, PDoc)]
forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era) -> TxBodyField era -> [(Text, PDoc)]
pgenTxBodyField Proof era
proof Map TxIn (TxOutF era)
ut) [TxBodyField era]
fields

pgenTxField ::
  forall era.
  Reflect era =>
  Proof era ->
  Map TxIn (TxOutF era) ->
  TxField era ->
  [(Text, PDoc)]
pgenTxField :: forall era.
Reflect era =>
Proof era -> Map TxIn (TxOutF era) -> TxField era -> [(Text, PDoc)]
pgenTxField Proof era
proof Map TxIn (TxOutF era)
ut TxField era
x = case TxField era
x of
  Body TxBody era
b -> [(TestName -> Text
pack TestName
"txbody hash", SafeHash EraIndependentTxBody -> PDoc
forall index. SafeHash index -> PDoc
ppSafeHash (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
b)), (TestName -> Text
pack TestName
"body", Proof era -> TxBody era -> Map TxIn (TxOutF era) -> PDoc
forall era.
Reflect era =>
Proof era -> TxBody era -> Map TxIn (TxOutF era) -> PDoc
pgenTxBody Proof era
proof TxBody era
b Map TxIn (TxOutF era)
ut)]
  BodyI [TxBodyField era]
xs -> [(TestName -> Text
pack TestName
"body", Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"TxBody") ((TxBodyField era -> [(Text, PDoc)])
-> [TxBodyField era] -> [(Text, PDoc)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Proof era
-> Map TxIn (TxOutF era) -> TxBodyField era -> [(Text, PDoc)]
forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era) -> TxBodyField era -> [(Text, PDoc)]
pgenTxBodyField Proof era
proof Map TxIn (TxOutF era)
ut) [TxBodyField era]
xs))]
  TxField era
_other -> Proof era -> TxField era -> [(Text, PDoc)]
forall era.
Reflect era =>
Proof era -> TxField era -> [(Text, PDoc)]
pcTxField Proof era
proof TxField era
x

pgenTx :: Reflect era => Proof era -> Map TxIn (TxOutF era) -> Tx era -> PDoc
pgenTx :: forall era.
Reflect era =>
Proof era -> Map TxIn (TxOutF era) -> Tx era -> PDoc
pgenTx Proof era
proof Map TxIn (TxOutF era)
ut Tx era
tx = Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"Tx") [(Text, PDoc)]
pairs
  where
    fields :: [TxField era]
fields = Proof era -> Tx era -> [TxField era]
forall era. Proof era -> Tx era -> [TxField era]
abstractTx Proof era
proof Tx era
tx
    pairs :: [(Text, PDoc)]
pairs = (TxField era -> [(Text, PDoc)]) -> [TxField era] -> [(Text, PDoc)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Proof era -> Map TxIn (TxOutF era) -> TxField era -> [(Text, PDoc)]
forall era.
Reflect era =>
Proof era -> Map TxIn (TxOutF era) -> TxField era -> [(Text, PDoc)]
pgenTxField Proof era
proof Map TxIn (TxOutF era)
ut) [TxField era]
fields

pcTxWithUTxO :: Reflect era => Proof era -> UTxO era -> Tx era -> PDoc
pcTxWithUTxO :: forall era. Reflect era => Proof era -> UTxO era -> Tx era -> PDoc
pcTxWithUTxO Proof era
proof (UTxO Map TxIn (TxOut era)
ut) Tx era
tx = Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"Tx") [(Text, PDoc)]
pairs
  where
    fields :: [TxField era]
fields = Proof era -> Tx era -> [TxField era]
forall era. Proof era -> Tx era -> [TxField era]
abstractTx Proof era
proof Tx era
tx
    pairs :: [(Text, PDoc)]
pairs = (TxField era -> [(Text, PDoc)]) -> [TxField era] -> [(Text, PDoc)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Proof era -> Map TxIn (TxOutF era) -> TxField era -> [(Text, PDoc)]
forall era.
Reflect era =>
Proof era -> Map TxIn (TxOutF era) -> TxField era -> [(Text, PDoc)]
pgenTxField Proof era
proof ((TxOut era -> TxOutF era)
-> Map TxIn (TxOut era) -> Map TxIn (TxOutF era)
forall a b. (a -> b) -> Map TxIn a -> Map TxIn b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Proof era -> TxOut era -> TxOutF era
forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
proof) Map TxIn (TxOut era)
ut)) [TxField era]
fields

-- =================================================
-- Demos and Tests

oneTest ::
  ( Reflect era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , Show (PredicateFailure (EraRule "LEDGER" era))
  ) =>
  UnivSize ->
  Proof era ->
  Gen Property
oneTest :: forall era.
(Reflect era, Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
UnivSize -> Proof era -> Gen Property
oneTest UnivSize
sizes Proof era
proof = do
  Subst era
subst <-
    Subst era -> Gen (Subst era)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst era
forall era. Subst era
emptySubst
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
sizes Proof era
proof
      Gen (Subst era)
-> (Subst era -> Gen (Subst era)) -> Gen (Subst era)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize -> Proof era -> Subst era -> Gen (Subst era)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
txBodyStage UnivSize
sizes Proof era
proof
  Env era
env0 <- Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Subst era -> Env era -> Typed (Env era)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst Env era
forall era. Env era
emptyEnv
  Env era
env1 <- Typed (Env era) -> Gen (Env era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env era) -> Gen (Env era))
-> Typed (Env era) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Env era -> Typed (Env era)
forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env era
env0
  Env era
env2 <- Typed (Gen (Env era)) -> Gen (Env era)
forall t. HasCallStack => Typed t -> t
errorTyped (Typed (Gen (Env era)) -> Gen (Env era))
-> Typed (Gen (Env era)) -> Gen (Env era)
forall a b. (a -> b) -> a -> b
$ Env era -> Typed (Gen (Env era))
forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env1
  LedgerState era
ledgerstate <- Typed (LedgerState era) -> Gen (LedgerState era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (LedgerState era) -> Gen (LedgerState era))
-> Typed (LedgerState era) -> Gen (LedgerState era)
forall a b. (a -> b) -> a -> b
$ Env era
-> RootTarget era (LedgerState era) (LedgerState era)
-> Typed (LedgerState era)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env2 (Proof era -> RootTarget era (LedgerState era) (LedgerState era)
forall era.
Reflect era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
proof)
  (TxF Proof era
_ Tx era
tx) <- Typed (TxF era) -> Gen (TxF era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Env era -> Term era (TxF era) -> Typed (TxF era)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env2 Term era (TxF era)
forall era. Reflect era => Term era (TxF era)
txterm)

  SlotNo
slot <- Typed SlotNo -> Gen SlotNo
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Env era -> Term era SlotNo -> Typed SlotNo
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env2 Term era SlotNo
forall era. Era era => Term era SlotNo
currentSlot)
  (PParamsF Proof era
_ PParams era
pp) <- Typed (PParamsF era) -> Gen (PParamsF era)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Env era -> Term era (PParamsF era) -> Typed (PParamsF era)
forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env2 (Proof era -> Term era (PParamsF era)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
proof))
  ChainAccountState
accntState <- Typed ChainAccountState -> Gen ChainAccountState
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Env era
-> RootTarget era ChainAccountState ChainAccountState
-> Typed ChainAccountState
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env2 RootTarget era ChainAccountState ChainAccountState
forall era.
Era era =>
RootTarget era ChainAccountState ChainAccountState
accountStateT)
  TxIx
txIx <- Gen TxIx
forall a. Arbitrary a => Gen a
arbitrary
  let lenv :: LedgerEnv era
lenv = SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> ChainAccountState
-> LedgerEnv era
LedgerEnv SlotNo
slot Maybe EpochNo
forall a. Maybe a
Nothing TxIx
txIx PParams era
pp ChainAccountState
accntState
  case Proof era
-> RuleContext 'Transition (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era))
forall era.
Era era =>
Proof era
-> RuleContext 'Transition (EraRule "LEDGER" era)
-> Either
     (NonEmpty (PredicateFailure (EraRule "LEDGER" era)))
     (State (EraRule "LEDGER" era))
applySTSByProof Proof era
proof ((Environment (EraRule "LEDGER" era), State (EraRule "LEDGER" era),
 Signal (EraRule "LEDGER" era))
-> TRC (EraRule "LEDGER" era)
forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv era
Environment (EraRule "LEDGER" era)
lenv, State (EraRule "LEDGER" era)
LedgerState era
ledgerstate, Tx era
Signal (EraRule "LEDGER" era)
tx)) of
    Right State (EraRule "LEDGER" era)
ledgerState' -> Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (LedgerState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda State (EraRule "LEDGER" era)
LedgerState era
ledgerState' Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== LedgerState era -> Coin
forall t. TotalAda t => t -> Coin
totalAda LedgerState era
ledgerstate)
    Left NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs -> do
      let msg :: TestName
msg = [TestName] -> TestName
unlines ([TestName] -> TestName) -> [TestName] -> TestName
forall a b. (a -> b) -> a -> b
$ TestName
"" TestName -> [TestName] -> [TestName]
forall a. a -> [a] -> [a]
: TestName
"applySTS fails" TestName -> [TestName] -> [TestName]
forall a. a -> [a] -> [a]
: (PredicateFailure (EraRule "LEDGER" era) -> TestName)
-> [PredicateFailure (EraRule "LEDGER" era)] -> [TestName]
forall a b. (a -> b) -> [a] -> [b]
map PredicateFailure (EraRule "LEDGER" era) -> TestName
forall a. Show a => a -> TestName
show (NonEmpty (PredicateFailure (EraRule "LEDGER" era))
-> [PredicateFailure (EraRule "LEDGER" era)]
forall a. NonEmpty a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList NonEmpty (PredicateFailure (EraRule "LEDGER" era))
errs)
      Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$
        IO () -> Property -> Property
forall prop. Testable prop => IO () -> prop -> Property
whenFail
          (TestName -> IO ()
putStrLn TestName
msg IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Proof era -> Env era -> TestName -> IO ()
forall era. Proof era -> Env era -> TestName -> IO ()
goRepl Proof era
proof Env era
env2 TestName
"")
          (TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
msg Bool
False)

main1 :: IO ()
main1 :: IO ()
main1 = Property -> IO ()
forall prop. Testable prop => prop -> IO ()
quickCheck (Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 (UnivSize -> Proof BabbageEra -> Gen Property
forall era.
(Reflect era, Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
UnivSize -> Proof era -> Gen Property
oneTest UnivSize
forall a. Default a => a
def Proof BabbageEra
Babbage))

main2 :: IO ()
main2 :: IO ()
main2 = Property -> IO ()
forall prop. Testable prop => prop -> IO ()
quickCheck (Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 (UnivSize -> Proof ShelleyEra -> Gen Property
forall era.
(Reflect era, Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
UnivSize -> Proof era -> Gen Property
oneTest UnivSize
forall a. Default a => a
def Proof ShelleyEra
Shelley))

demo :: ReplMode -> IO ()
demo :: ReplMode -> IO ()
demo ReplMode
mode = do
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
  -- Conway
  -- Alonzo
  -- Mary
  -- Shelley
  let sizes :: UnivSize
sizes = UnivSize
forall a. Default a => a
def
  Subst BabbageEra
subst <-
    Gen (Subst BabbageEra) -> IO (Subst BabbageEra)
forall a. Gen a -> IO a
generate
      ( Subst BabbageEra -> Gen (Subst BabbageEra)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Subst BabbageEra
forall era. Subst era
emptySubst
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
sizes Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
sizes Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
sizes Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
sizes Proof BabbageEra
proof
          Gen (Subst BabbageEra)
-> (Subst BabbageEra -> Gen (Subst BabbageEra))
-> Gen (Subst BabbageEra)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= UnivSize
-> Proof BabbageEra -> Subst BabbageEra -> Gen (Subst BabbageEra)
forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
txBodyStage UnivSize
sizes Proof BabbageEra
proof
      )
  -- rewritten <- snd <$> generate (rewriteGen (1, txBodyPreds sizes proof))
  -- putStrLn (show rewritten)
  (Env BabbageEra
_, Maybe TestName
status) <- Typed (Env BabbageEra, Maybe TestName)
-> IO (Env BabbageEra, Maybe TestName)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env BabbageEra, Maybe TestName)
 -> IO (Env BabbageEra, Maybe TestName))
-> Typed (Env BabbageEra, Maybe TestName)
-> IO (Env BabbageEra, Maybe TestName)
forall a b. (a -> b) -> a -> b
$ [Pred BabbageEra]
-> Subst BabbageEra -> Typed (Env BabbageEra, Maybe TestName)
forall era.
Era era =>
[Pred era] -> Subst era -> Typed (Env era, Maybe TestName)
checkForSoundness (UnivSize -> Proof BabbageEra -> [Pred BabbageEra]
forall era.
(HasCallStack, Reflect era) =>
UnivSize -> Proof era -> [Pred era]
txBodyPreds UnivSize
sizes Proof BabbageEra
proof) Subst BabbageEra
subst
  (TestName -> IO Any) -> Maybe TestName -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ TestName -> IO Any
forall a. HasCallStack => TestName -> a
error Maybe TestName
status
  Env BabbageEra
env0 <- Typed (Env BabbageEra) -> IO (Env BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env BabbageEra) -> IO (Env BabbageEra))
-> Typed (Env BabbageEra) -> IO (Env BabbageEra)
forall a b. (a -> b) -> a -> b
$ Subst BabbageEra -> Env BabbageEra -> Typed (Env BabbageEra)
forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst BabbageEra
subst Env BabbageEra
forall era. Env era
emptyEnv
  Env BabbageEra
env1 <- Typed (Env BabbageEra) -> IO (Env BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (Env BabbageEra) -> IO (Env BabbageEra))
-> Typed (Env BabbageEra) -> IO (Env BabbageEra)
forall a b. (a -> b) -> a -> b
$ Env BabbageEra -> Typed (Env BabbageEra)
forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env BabbageEra
env0
  Env BabbageEra
env2 <- Gen (Env BabbageEra) -> IO (Env BabbageEra)
forall a. Gen a -> IO a
generate (Gen (Env BabbageEra) -> IO (Env BabbageEra))
-> Gen (Env BabbageEra) -> IO (Env BabbageEra)
forall a b. (a -> b) -> a -> b
$ Typed (Gen (Env BabbageEra)) -> Gen (Env BabbageEra)
forall t. HasCallStack => Typed t -> t
errorTyped (Typed (Gen (Env BabbageEra)) -> Gen (Env BabbageEra))
-> Typed (Gen (Env BabbageEra)) -> Gen (Env BabbageEra)
forall a b. (a -> b) -> a -> b
$ Env BabbageEra -> Typed (Gen (Env BabbageEra))
forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env BabbageEra
env1
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Env BabbageEra -> Term BabbageEra Coin -> IO ()
forall era a. Era era => Env era -> Term era a -> IO ()
displayTerm Env BabbageEra
env2 Term BabbageEra Coin
forall era. Era era => Term era Coin
txfee
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Env BabbageEra -> Term BabbageEra (TxF BabbageEra) -> IO ()
forall era a. Era era => Env era -> Term era a -> IO ()
displayTerm Env BabbageEra
env2 Term BabbageEra (TxF BabbageEra)
forall era. Reflect era => Term era (TxF era)
txterm
  -- compute Produced and Consumed
  (TxBodyF Proof BabbageEra
_ TxBody BabbageEra
txb) <- Typed (TxBodyF BabbageEra) -> IO (TxBodyF BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V BabbageEra (TxBodyF BabbageEra)
-> Env BabbageEra -> Typed (TxBodyF BabbageEra)
forall era t. V era t -> Env era -> Typed t
findVar (Term BabbageEra (TxBodyF BabbageEra)
-> V BabbageEra (TxBodyF BabbageEra)
forall era t. Term era t -> V era t
unVar Term BabbageEra (TxBodyF BabbageEra)
forall era. Reflect era => Term era (TxBodyF era)
txbodyterm) Env BabbageEra
env2)
  CertStateF BabbageEra
certState <- Typed (CertStateF BabbageEra) -> IO (CertStateF BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (Typed (CertStateF BabbageEra) -> IO (CertStateF BabbageEra))
-> (RootTarget
      BabbageEra (CertStateF BabbageEra) (CertStateF BabbageEra)
    -> Typed (CertStateF BabbageEra))
-> RootTarget
     BabbageEra (CertStateF BabbageEra) (CertStateF BabbageEra)
-> IO (CertStateF BabbageEra)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env BabbageEra
-> RootTarget
     BabbageEra (CertStateF BabbageEra) (CertStateF BabbageEra)
-> Typed (CertStateF BabbageEra)
forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env BabbageEra
env1 (RootTarget
   BabbageEra (CertStateF BabbageEra) (CertStateF BabbageEra)
 -> IO (CertStateF BabbageEra))
-> RootTarget
     BabbageEra (CertStateF BabbageEra) (CertStateF BabbageEra)
-> IO (CertStateF BabbageEra)
forall a b. (a -> b) -> a -> b
$ RootTarget
  BabbageEra (CertStateF BabbageEra) (CertStateF BabbageEra)
forall era.
Reflect era =>
RootTarget era (CertStateF era) (CertStateF era)
certStateT
  (PParamsF Proof BabbageEra
_ PParams BabbageEra
ppV) <- Typed (PParamsF BabbageEra) -> IO (PParamsF BabbageEra)
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V BabbageEra (PParamsF BabbageEra)
-> Env BabbageEra -> Typed (PParamsF BabbageEra)
forall era t. V era t -> Env era -> Typed t
findVar (Term BabbageEra (PParamsF BabbageEra)
-> V BabbageEra (PParamsF BabbageEra)
forall era t. Term era t -> V era t
unVar (Proof BabbageEra -> Term BabbageEra (PParamsF BabbageEra)
forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof BabbageEra
proof)) Env BabbageEra
env2)
  Map TxIn (TxOutF BabbageEra)
utxoV <- Typed (Map TxIn (TxOutF BabbageEra))
-> IO (Map TxIn (TxOutF BabbageEra))
forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (V BabbageEra (Map TxIn (TxOutF BabbageEra))
-> Env BabbageEra -> Typed (Map TxIn (TxOutF BabbageEra))
forall era t. V era t -> Env era -> Typed t
findVar (Term BabbageEra (Map TxIn (TxOutF BabbageEra))
-> V BabbageEra (Map TxIn (TxOutF BabbageEra))
forall era t. Term era t -> V era t
unVar (Proof BabbageEra -> Term BabbageEra (Map TxIn (TxOutF BabbageEra))
forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof BabbageEra
proof)) Env BabbageEra
env2)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ Produced -> IO ()
forall a. Show a => a -> IO ()
print (TxBody BabbageEra
-> PParams BabbageEra -> CertState BabbageEra -> Produced
forall era.
(EraTxBody era, EraCertState era) =>
TxBody era -> PParams era -> CertState era -> Produced
producedTxBody TxBody BabbageEra
txb PParams BabbageEra
ppV (CertState BabbageEra -> Produced)
-> CertState BabbageEra -> Produced
forall a b. (a -> b) -> a -> b
$ CertStateF BabbageEra -> CertState BabbageEra
forall era. CertStateF era -> CertState era
unCertStateF CertStateF BabbageEra
certState)
  Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (ReplMode
mode ReplMode -> ReplMode -> Bool
forall a. Eq a => a -> a -> Bool
== ReplMode
Interactive) (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$
    Consumed -> IO ()
forall a. Show a => a -> IO ()
print (TxBody BabbageEra
-> PParams BabbageEra
-> CertState BabbageEra
-> UTxO BabbageEra
-> Consumed
forall era.
(EraTxBody era, EraCertState era) =>
TxBody era -> PParams era -> CertState era -> UTxO era -> Consumed
consumedTxBody TxBody BabbageEra
txb PParams BabbageEra
ppV (CertStateF BabbageEra -> CertState BabbageEra
forall era. CertStateF era -> CertState era
unCertStateF CertStateF BabbageEra
certState) (Map TxIn (TxOutF BabbageEra) -> UTxO BabbageEra
forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF BabbageEra)
utxoV))
  ReplMode -> Proof BabbageEra -> Env BabbageEra -> TestName -> IO ()
forall era. ReplMode -> Proof era -> Env era -> TestName -> IO ()
modeRepl ReplMode
mode Proof BabbageEra
proof Env BabbageEra
env2 TestName
""

demoTest :: TestTree
demoTest :: TestTree
demoTest =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Tests for Tx Stage"
    [ TestName -> IO () -> TestTree
forall a. TestName -> IO a -> TestTree
testIO TestName
"Testing Tx Stage" (ReplMode -> IO ()
demo ReplMode
CI)
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"One Tx Test Babbage" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 (UnivSize -> Proof BabbageEra -> Gen Property
forall era.
(Reflect era, Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
UnivSize -> Proof era -> Gen Property
oneTest UnivSize
forall a. Default a => a
def Proof BabbageEra
Babbage)
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"One Tx Test Shelley" (Property -> TestTree) -> Property -> TestTree
forall a b. (a -> b) -> a -> b
$ Int -> Gen Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 (UnivSize -> Proof ShelleyEra -> Gen Property
forall era.
(Reflect era, Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Show (PredicateFailure (EraRule "LEDGER" era))) =>
UnivSize -> Proof era -> Gen Property
oneTest UnivSize
forall a. Default a => a
def Proof ShelleyEra
Shelley)
    ]

main :: IO ()
main :: IO ()
main = TestTree -> IO ()
defaultMain (TestTree -> IO ()) -> TestTree -> IO ()
forall a b. (a -> b) -> a -> b
$ TestName -> IO () -> TestTree
forall a. TestName -> IO a -> TestTree
testIO TestName
"Testing Tx Stage" (ReplMode -> IO ()
demo ReplMode
Interactive)