{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE PatternSynonyms #-}
{-# 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.CertState (CertState, certDStateL, dsGenDelegsL)
import Cardano.Ledger.Coin (Coin (..), rationalToCoinViaCeiling)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Keys (
  GenDelegPair (..),
  GenDelegs (..),
  Hash,
  KeyHash,
  KeyRole (..),
  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.SafeHash (SafeHash, extractHash, hashAnnotated)
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.TxIn (TxIn (..))
import Cardano.Ledger.UTxO (EraUTxO (..), ScriptsProvided (..), UTxO (..))
import Cardano.Ledger.Val (Val (..), inject)
import Control.Monad (when)
import Control.State.Transition.Extended (STS (..), TRC (..))
import Data.Default.Class (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 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 Test.Cardano.Ledger.Constrained.Preds.Certs (certsStage)
import Test.Cardano.Ledger.Constrained.Preds.LedgerState (ledgerStateStage)
import Test.Cardano.Ledger.Constrained.Preds.NewEpochState (epochStateStage, newEpochStateStage)
import Test.Cardano.Ledger.Constrained.Preds.PParams (pParamsStage)
import Test.Cardano.Ledger.Constrained.Preds.Repl (ReplMode (..), goRepl, modeRepl)
import Test.Cardano.Ledger.Constrained.Preds.TxOut (txOutPreds)
import Test.Cardano.Ledger.Constrained.Preds.UTxO (utxoStage)
import Test.Cardano.Ledger.Constrained.Preds.Universes hiding (demo, demoTest, main)
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.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)

import Cardano.Ledger.DRep (drepDepositL)
import Cardano.Ledger.EpochBoundary (SnapShot (..), Stake (..), calculatePoolDistr)
import qualified Cardano.Ledger.UMap as UMap
import qualified Data.VMap as VMap
import qualified Test.Cardano.Ledger.Constrained.Preds.CertState as CertState
import qualified Test.Cardano.Ledger.Constrained.Preds.Certs as Certs
import qualified Test.Cardano.Ledger.Constrained.Preds.LedgerState as LedgerState
import qualified Test.Cardano.Ledger.Constrained.Preds.PParams as PParams
import qualified Test.Cardano.Ledger.Constrained.Preds.TxOut as TxOut
import qualified Test.Cardano.Ledger.Constrained.Preds.Universes as Universes
import Test.Cardano.Ledger.Constrained.Utils (checkForSoundness, testIO)

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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Sized a -> Int64
sizedSize (forall a. EncCBOR a => Version -> a -> Sized a
mkSized (ProtVer -> Version
pvMajor (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 = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Sized a -> Int64
sizedSize (forall a. EncCBOR a => Version -> a -> Sized a
mkSized (ProtVer -> Version
pvMajor (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 = forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"byteSize" (forall era a. (EncCBOR a, Reflect era) => Proof era -> a -> Int
byteSize (forall era. Reflect era => Proof era
reify @era)) 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. Lens' (TxF era) (Tx era)
txFL = 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 -> 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 (EraCrypto era)) (TxOutF era) ->
  Coin
computeFinalFee :: forall era.
EraUTxO era =>
PParamsF era
-> TxF era -> Map (TxIn (EraCrypto era)) (TxOutF era) -> Coin
computeFinalFee (PParamsF Proof era
_ PParams era
ppV) (TxF Proof era
_ Tx era
txV) Map (TxIn (EraCrypto era)) (TxOutF era)
ut = Tx era
newtx forall s a. s -> Getting a s a -> a
^. (forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL)
  where
    newtx :: Tx era
newtx = forall era.
EraUTxO era =>
PParams era -> Tx era -> UTxO era -> Tx era
setMinFeeTxUtxo PParams era
ppV Tx era
txV (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (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 (EraCrypto era1)) (Data era1)) ->
  Target era2 (Maybe (ScriptIntegrityHash (EraCrypto era1)))
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 (EraCrypto era1)) (Data era1))
-> Target era2 (Maybe (ScriptIntegrityHash (EraCrypto era1)))
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 (EraCrypto era1)) (Data era1))
ds = forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"integrityHash" PParamsF era1
-> Set Language
-> Map (PlutusPointerF era1) (Data era1, ExUnits)
-> Map (DataHash (EraCrypto era1)) (Data era1)
-> Maybe (ScriptIntegrityHash (EraCrypto era1))
hashfun forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era2 (PParamsF era1)
pp forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era2 (Set Language)
langs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits))
rs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era2 (Map (DataHash (EraCrypto era1)) (Data era1))
ds
  where
    hashfun :: PParamsF era1
-> Set Language
-> Map (PlutusPointerF era1) (Data era1, ExUnits)
-> Map (DataHash (EraCrypto era1)) (Data era1)
-> Maybe (ScriptIntegrityHash (EraCrypto era1))
hashfun (PParamsF Proof era1
_ PParams era1
ppp) Set Language
ls Map (PlutusPointerF era1) (Data era1, ExUnits)
r Map (DataHash (EraCrypto era1)) (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) <- forall k a. Map k a -> [(k, a)]
Map.toList Map (PlutusPointerF era1) (Data era1, ExUnits)
r]
       in forall a. StrictMaybe a -> Maybe a
strictMaybeToMaybe forall a b. (a -> b) -> a -> b
$
            forall era.
Proof era
-> PParams era
-> [Language]
-> Redeemers era
-> TxDats era
-> StrictMaybe (ScriptIntegrityHash (EraCrypto era))
newScriptIntegrityHash Proof era1
p PParams era1
ppp (forall a. Set a -> [a]
Set.toList Set Language
ls) (forall era.
Proof era
-> [(PlutusPurpose AsIx era, (Data era, ExUnits))] -> Redeemers era
mkRedeemers Proof era1
p [(PlutusPurpose AsIx era1, (Data era1, ExUnits))]
r') (forall era.
Era era =>
Map (DataHash (EraCrypto era)) (Data era) -> TxDats era
TxDats Map (DataHash (EraCrypto era1)) (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 (EraCrypto era)) (TxOutF era) ->
      ScriptsNeededF era
    )
needT :: forall era.
EraUTxO era =>
Proof era
-> Target
     era
     (TxBodyF era
      -> Map (TxIn (EraCrypto era)) (TxOutF era) -> ScriptsNeededF era)
needT Proof era
proof = forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"neededScripts" TxBodyF era
-> Map (TxIn (EraCrypto era)) (TxOutF era) -> ScriptsNeededF era
needed
  where
    needed :: TxBodyF era -> Map (TxIn (EraCrypto era)) (TxOutF era) -> ScriptsNeededF era
    needed :: TxBodyF era
-> Map (TxIn (EraCrypto era)) (TxOutF era) -> ScriptsNeededF era
needed (TxBodyF Proof era
_ TxBody era
txbodyV) Map (TxIn (EraCrypto era)) (TxOutF era)
ut = forall era. Proof era -> ScriptsNeeded era -> ScriptsNeededF era
ScriptsNeededF Proof era
proof (forall era.
EraUTxO era =>
UTxO era -> TxBody era -> ScriptsNeeded era
getScriptsNeeded (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
ut) TxBody era
txbodyV)

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

getRdmrPtrs ::
  AlonzoEraScript era =>
  [((PlutusPurposeF era), (ScriptHash (EraCrypto era)))] ->
  Map (ScriptHash (EraCrypto era)) any ->
  Set (PlutusPointerF era)
getRdmrPtrs :: forall era any.
AlonzoEraScript era =>
[(PlutusPurposeF era, ScriptHash (EraCrypto era))]
-> Map (ScriptHash (EraCrypto era)) any -> Set (PlutusPointerF era)
getRdmrPtrs [(PlutusPurposeF era, ScriptHash (EraCrypto era))]
xs Map (ScriptHash (EraCrypto era)) any
allplutus = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (PlutusPointerF era)
-> (PlutusPurposeF era, ScriptHash (EraCrypto era))
-> Set (PlutusPointerF era)
accum forall a. Set a
Set.empty [(PlutusPurposeF era, ScriptHash (EraCrypto era))]
xs
  where
    accum :: Set (PlutusPointerF era)
-> (PlutusPurposeF era, ScriptHash (EraCrypto era))
-> Set (PlutusPointerF era)
accum Set (PlutusPointerF era)
ans (PlutusPurposeF Proof era
p PlutusPurpose AsIxItem era
sp, ScriptHash (EraCrypto era)
hash)
      | forall k a. Ord k => k -> Map k a -> Bool
Map.member ScriptHash (EraCrypto era)
hash Map (ScriptHash (EraCrypto era)) any
allplutus =
          let ptr :: PlutusPurpose AsIx era
ptr = forall era (g :: * -> * -> *) (f :: * -> * -> *).
AlonzoEraScript era =>
(forall ix it. g ix it -> f ix it)
-> PlutusPurpose g era -> PlutusPurpose f era
hoistPlutusPurpose forall ix it. AsIxItem ix it -> AsIx ix it
toAsIx PlutusPurpose AsIxItem era
sp
           in forall a. Ord a => a -> Set a -> Set a
Set.insert (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 (EraCrypto era)) (TxOutF era) ->
  TxBodyF era ->
  Map (ScriptHash (EraCrypto era)) (ScriptF era) ->
  Set (DataHash (EraCrypto era))
getPlutusDataHashes :: forall era.
(AlonzoEraTxOut era, EraTxBody era, AlonzoEraScript era) =>
Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxBodyF era
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Set (DataHash (EraCrypto era))
getPlutusDataHashes Map (TxIn (EraCrypto era)) (TxOutF era)
ut (TxBodyF Proof era
_ TxBody era
txbodyV) Map (ScriptHash (EraCrypto era)) (ScriptF era)
m =
  forall a b. (a, b) -> a
fst forall a b. (a -> b) -> a -> b
$ forall era.
(EraTxBody era, AlonzoEraTxOut era, AlonzoEraScript era) =>
UTxO era
-> TxBody era
-> ScriptsProvided era
-> (Set (DataHash (EraCrypto era)), Set (TxIn (EraCrypto era)))
getInputDataHashesTxBody (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
ut) TxBody era
txbodyV (forall era.
Map (ScriptHash (EraCrypto era)) (Script era)
-> ScriptsProvided era
ScriptsProvided (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall era. ScriptF era -> Script era
unScriptF Map (ScriptHash (EraCrypto era)) (ScriptF era)
m))

bootWitsT ::
  forall era.
  Reflect era =>
  Proof era ->
  Map (TxIn (EraCrypto era)) (TxOutF era) ->
  TxBodyF era ->
  Map (KeyHash 'Payment (EraCrypto era)) (Addr (EraCrypto era), SigningKey) ->
  Set (BootstrapWitness (EraCrypto era))
bootWitsT :: forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxBodyF era
-> Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey)
-> Set (BootstrapWitness (EraCrypto era))
bootWitsT Proof era
proof Map (TxIn (EraCrypto era)) (TxOutF era)
spend (TxBodyF Proof era
_ TxBody era
txb) Map
  (KeyHash 'Payment (EraCrypto era))
  (Addr (EraCrypto era), SigningKey)
byronUniv = forall c.
(Crypto c, DSIGN c ~ Ed25519DSIGN) =>
Hash c EraIndependentTxBody
-> [BootstrapAddress c]
-> Map (KeyHash 'Payment c) (Addr c, SigningKey)
-> Set (BootstrapWitness c)
bootWitness Hash (EraCrypto era) EraIndependentTxBody
h [BootstrapAddress (EraCrypto era)]
boots Map
  (KeyHash 'Payment (EraCrypto era))
  (Addr (EraCrypto era), SigningKey)
byronUniv
  where
    boots :: [BootstrapAddress (EraCrypto era)] -- Not every Addr has a BootStrapAddress
    boots :: [BootstrapAddress (EraCrypto era)]
boots = forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' forall {era}.
EraTxOut era =>
[BootstrapAddress (EraCrypto era)]
-> TxOutF era -> [BootstrapAddress (EraCrypto era)]
accum [] Map (TxIn (EraCrypto era)) (TxOutF era)
spend -- Compute a list of them.
      where
        accum :: [BootstrapAddress (EraCrypto era)]
-> TxOutF era -> [BootstrapAddress (EraCrypto era)]
accum [BootstrapAddress (EraCrypto era)]
ans (TxOutF Proof era
_ TxOut era
out) = case TxOut era
out forall s a. s -> Getting a s a -> a
^. forall era.
EraTxOut era =>
Lens' (TxOut era) (Addr (EraCrypto era))
addrTxOutL of
          AddrBootstrap BootstrapAddress (EraCrypto era)
b -> BootstrapAddress (EraCrypto era)
b forall a. a -> [a] -> [a]
: [BootstrapAddress (EraCrypto era)]
ans
          Addr (EraCrypto era)
_ -> [BootstrapAddress (EraCrypto era)]
ans
    h :: Hash (EraCrypto era) EraIndependentTxBody
h = forall era.
Proof era
-> TxBody era -> Hash (EraCrypto era) EraIndependentTxBody
hashBody Proof era
proof TxBody era
txb

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

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

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

sufficientTxCert ::
  forall era.
  Reflect era =>
  [TxCertF era] ->
  Map (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)) ->
  Set (KeyHash 'Witness (EraCrypto era))
sufficientTxCert :: forall era.
Reflect era =>
[TxCertF era]
-> Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
-> Set (KeyHash 'Witness (EraCrypto era))
sufficientTxCert [TxCertF era]
cs Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
gendel = case forall era. Proof era -> TxCertWit era
whichTxCert (forall era. Reflect era => Proof era
reify @era) of
  TxCertWit era
TxCertShelleyToBabbage -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (KeyHash 'Witness StandardCrypto)
-> TxCertF era -> Set (KeyHash 'Witness StandardCrypto)
accum forall a. Set a
Set.empty [TxCertF era]
cs
    where
      accum :: Set (KeyHash 'Witness StandardCrypto)
-> TxCertF era -> Set (KeyHash 'Witness StandardCrypto)
accum Set (KeyHash 'Witness StandardCrypto)
ans (TxCertF Proof era
_ TxCert era
cert) =
        if forall era.
(ShelleyEraTxCert era, ProtVerAtMost era 8) =>
TxCert era -> Bool
isInstantaneousRewards TxCert era
cert
          then forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness StandardCrypto)
ans (forall k c. Map k (GenDelegPair c) -> Set (KeyHash 'Witness c)
sufficientGenDelegs Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
gendel)
          else Set (KeyHash 'Witness StandardCrypto)
ans
  TxCertWit era
TxCertConwayToConway -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (KeyHash 'Witness StandardCrypto)
-> TxCertF era -> Set (KeyHash 'Witness StandardCrypto)
accum forall a. Set a
Set.empty [TxCertF era]
cs
    where
      accum :: Set (KeyHash 'Witness StandardCrypto)
-> TxCertF era -> Set (KeyHash 'Witness StandardCrypto)
accum Set (KeyHash 'Witness StandardCrypto)
ans (TxCertF Proof era
_ TxCert era
_) = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness StandardCrypto)
ans (forall k c. Map k (GenDelegPair c) -> Set (KeyHash 'Witness c)
sufficientGenDelegs Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
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 (EraCrypto era)) (ScriptF era) ->
  Set (KeyHash 'Witness (EraCrypto era))
sufficientScriptKeys :: forall era.
Proof era
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Set (KeyHash 'Witness (EraCrypto era))
sufficientScriptKeys Proof era
proof Map (ScriptHash (EraCrypto era)) (ScriptF era)
scriptmap = forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' Set (KeyHash 'Witness (EraCrypto era))
-> ScriptF era -> Set (KeyHash 'Witness (EraCrypto era))
accum forall a. Set a
Set.empty Map (ScriptHash (EraCrypto era)) (ScriptF era)
scriptmap
  where
    accum :: Set (KeyHash 'Witness (EraCrypto era))
-> ScriptF era -> Set (KeyHash 'Witness (EraCrypto era))
accum Set (KeyHash 'Witness (EraCrypto era))
ans (ScriptF Proof era
_ Script era
s) = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness (EraCrypto era))
ans (forall era.
Proof era -> Script era -> Set (KeyHash 'Witness (EraCrypto era))
sufficientScript Proof era
proof Script era
s)

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

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

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

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

necessaryKeyHashTarget ::
  forall era.
  Reflect era =>
  Term era (TxBodyF era) ->
  Term era (Set (KeyHash 'Witness (EraCrypto era))) ->
  -- Target era (Set (WitVKey 'Witness (EraCrypto era)))
  Target era (Set (KeyHash 'Witness (EraCrypto era)))
necessaryKeyHashTarget :: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Target era (Set (KeyHash 'Witness (EraCrypto era)))
necessaryKeyHashTarget Term era (TxBodyF era)
txbodyparam Term era (Set (KeyHash 'Witness (EraCrypto era)))
reqSignersparam =
  ( forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"keywits" forall era.
Reflect era =>
TxBodyF era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
-> Set (KeyHash 'Witness (EraCrypto era))
-> Set (KeyHash 'Witness (EraCrypto era))
necessaryKeyHashes
      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
txbodyparam
      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo forall era. Reflect era => Proof era
reify)
      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
genDelegs
      --  ^$ keymapUniv
      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness (EraCrypto era)))
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 (EraCrypto era)) (TxOutF era) ->
  Map (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)) ->
  Set (KeyHash 'Witness (EraCrypto era)) -> -- Only in Eras Alonzo To Conway,
  Set (KeyHash 'Witness (EraCrypto era))
necessaryKeyHashes :: forall era.
Reflect era =>
TxBodyF era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
-> Set (KeyHash 'Witness (EraCrypto era))
-> Set (KeyHash 'Witness (EraCrypto era))
necessaryKeyHashes (TxBodyF Proof era
_ TxBody era
txb) Map (TxIn (EraCrypto era)) (TxOutF era)
u Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
gd Set (KeyHash 'Witness (EraCrypto era))
reqsigners =
  case forall era. Reflect era => Proof era
reify @era of
    Proof era
Shelley -> forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall era.
EraUTxO era =>
CertState era
-> UTxO era -> TxBody era -> Set (KeyHash 'Witness (EraCrypto era))
getWitsVKeyNeeded CertState era
certState (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness (EraCrypto era))
reqsigners
    Proof era
Allegra -> forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall era.
EraUTxO era =>
CertState era
-> UTxO era -> TxBody era -> Set (KeyHash 'Witness (EraCrypto era))
getWitsVKeyNeeded CertState era
certState (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness (EraCrypto era))
reqsigners
    Proof era
Mary -> forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall era.
EraUTxO era =>
CertState era
-> UTxO era -> TxBody era -> Set (KeyHash 'Witness (EraCrypto era))
getWitsVKeyNeeded CertState era
certState (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness (EraCrypto era))
reqsigners
    Proof era
Alonzo -> forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall era.
EraUTxO era =>
CertState era
-> UTxO era -> TxBody era -> Set (KeyHash 'Witness (EraCrypto era))
getWitsVKeyNeeded CertState era
certState (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness (EraCrypto era))
reqsigners
    Proof era
Babbage -> forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall era.
EraUTxO era =>
CertState era
-> UTxO era -> TxBody era -> Set (KeyHash 'Witness (EraCrypto era))
getWitsVKeyNeeded CertState era
certState (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness (EraCrypto era))
reqsigners
    Proof era
Conway -> forall a. Ord a => Set a -> Set a -> Set a
Set.union (forall era.
EraUTxO era =>
CertState era
-> UTxO era -> TxBody era -> Set (KeyHash 'Witness (EraCrypto era))
getWitsVKeyNeeded forall a. Default a => a
def (forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
u) TxBody era
txb) Set (KeyHash 'Witness (EraCrypto era))
reqsigners
  where
    certState :: CertState era
    certState :: CertState era
certState = forall a. Default a => a
def forall a b. a -> (a -> b) -> b
& forall era. Lens' (CertState era) (DState era)
certDStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. Lens' (DState era) (GenDelegs (EraCrypto era))
dsGenDelegsL forall s t a b. ASetter s t a b -> b -> s -> t
.~ forall c. Map (KeyHash 'Genesis c) (GenDelegPair c) -> GenDelegs c
GenDelegs Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
gd

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

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

makeKeyWitness ::
  forall era.
  Reflect era =>
  TxBodyF era ->
  Set (KeyHash 'Witness (EraCrypto era)) ->
  Set (KeyHash 'Witness (EraCrypto era)) ->
  Map (KeyHash 'Witness (EraCrypto era)) (KeyPair 'Witness (EraCrypto era)) ->
  Map (ScriptHash (EraCrypto era)) (ScriptF era) ->
  Map (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)) ->
  Map (KeyHash 'Payment (EraCrypto era)) ((Addr (EraCrypto era)), SigningKey) ->
  Set (WitVKey 'Witness (EraCrypto era))
makeKeyWitness :: forall era.
Reflect era =>
TxBodyF era
-> Set (KeyHash 'Witness (EraCrypto era))
-> Set (KeyHash 'Witness (EraCrypto era))
-> Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era))
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
-> Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey)
-> Set (WitVKey 'Witness (EraCrypto era))
makeKeyWitness (TxBodyF Proof era
proof TxBody era
txb) Set (KeyHash 'Witness (EraCrypto era))
necessary Set (KeyHash 'Witness (EraCrypto era))
sufficient Map
  (KeyHash 'Witness (EraCrypto era))
  (KeyPair 'Witness (EraCrypto era))
keyUniv Map (ScriptHash (EraCrypto era)) (ScriptF era)
scripts Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
gendel Map
  (KeyHash 'Payment (EraCrypto era))
  (Addr (EraCrypto era), SigningKey)
byronAdUniv = Set (WitVKey 'Witness StandardCrypto)
keywits
  where
    bodyhash :: SafeHash (EraCrypto era) EraIndependentTxBody
    bodyhash :: SafeHash (EraCrypto era) EraIndependentTxBody
bodyhash = forall x index c.
(HashAnnotated x index c, HashAlgorithm (HASH c)) =>
x -> SafeHash c index
hashAnnotated TxBody era
txb
    keywits :: Set (WitVKey 'Witness StandardCrypto)
keywits = forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' Set (WitVKey 'Witness StandardCrypto)
-> KeyHash 'Witness StandardCrypto
-> Set (WitVKey 'Witness StandardCrypto)
accum forall a. Set a
Set.empty (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness (EraCrypto era))
necessary Set (KeyHash 'Witness (EraCrypto era))
sufficient)
      where
        accum :: Set (WitVKey 'Witness StandardCrypto)
-> KeyHash 'Witness StandardCrypto
-> Set (WitVKey 'Witness StandardCrypto)
accum Set (WitVKey 'Witness StandardCrypto)
ans KeyHash 'Witness StandardCrypto
hash = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Witness StandardCrypto
hash Map
  (KeyHash 'Witness (EraCrypto era))
  (KeyPair 'Witness (EraCrypto era))
keyUniv of
          Just KeyPair 'Witness StandardCrypto
keypair -> forall a. Ord a => a -> Set a -> Set a
Set.insert (forall c (kr :: KeyRole).
(Crypto c, DSignable c (Hash (HASH c) EraIndependentTxBody)) =>
SafeHash c EraIndependentTxBody
-> KeyPair kr c -> WitVKey 'Witness c
mkWitnessVKey SafeHash (EraCrypto era) EraIndependentTxBody
bodyhash KeyPair 'Witness StandardCrypto
keypair) Set (WitVKey 'Witness StandardCrypto)
ans
          Maybe (KeyPair 'Witness StandardCrypto)
Nothing -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall (a :: KeyRole -> * -> *) (r :: KeyRole) c (r' :: KeyRole).
HasKeyRole a =>
a r c -> a r' c
coerceKeyRole KeyHash 'Witness StandardCrypto
hash) Map
  (KeyHash 'Payment (EraCrypto era))
  (Addr (EraCrypto era), SigningKey)
byronAdUniv of
            Just (AddrBootstrap BootstrapAddress StandardCrypto
_, SigningKey
_) -> Set (WitVKey 'Witness StandardCrypto)
ans -- Bootstrap witnesses are handled in bootWitsT, so we can ignore them here.
            Maybe (Addr StandardCrypto, SigningKey)
_ ->
              forall a. HasCallStack => TestName -> a
error
                ( TestName
"hash not in keymapUniv or byronAddrUniv"
                    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show KeyHash 'Witness StandardCrypto
hash
                    forall a. [a] -> [a] -> [a]
++ TestName
"\n member necessary = "
                    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (forall a. Ord a => a -> Set a -> Bool
Set.member KeyHash 'Witness StandardCrypto
hash Set (KeyHash 'Witness (EraCrypto era))
necessary)
                    forall a. [a] -> [a] -> [a]
++ TestName
"\n member sufficient = "
                    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (forall a. Ord a => a -> Set a -> Bool
Set.member KeyHash 'Witness StandardCrypto
hash Set (KeyHash 'Witness (EraCrypto era))
sufficient)
                    forall a. [a] -> [a] -> [a]
++ TestName
"\n scripts = "
                    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap forall era. ScriptHash era -> PDoc
pcScriptHash (\(ScriptF Proof era
p Script era
s) -> forall era. Reflect era => Proof era -> Script era -> PDoc
pcScript Proof era
p Script era
s) Map (ScriptHash (EraCrypto era)) (ScriptF era)
scripts)
                    forall a. [a] -> [a] -> [a]
++ TestName
"\n genDelegs = "
                    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap forall (discriminator :: KeyRole) c.
KeyHash discriminator c -> PDoc
pcKeyHash forall c. GenDelegPair c -> PDoc
pcGenDelegPair Map
  (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
gendel)
                    forall a. [a] -> [a] -> [a]
++ TestName
"\nbyronAddrUniv\n"
                    forall a. [a] -> [a] -> [a]
++ forall era t. Rep era t -> t -> TestName
format @era (forall t era b.
Ord t =>
Rep era t -> Rep era b -> Rep era (Map t b)
MapR forall era. Era era => Rep era (KeyHash 'Payment (EraCrypto era))
PayHashR (forall era t b. Rep era t -> Rep era b -> Rep era (t, b)
PairR forall era. Era era => Rep era (Addr (EraCrypto era))
AddrR forall era. Rep era SigningKey
SigningKeyR)) Map
  (KeyHash 'Payment (EraCrypto era))
  (Addr (EraCrypto era), SigningKey)
byronAdUniv
                    forall a. [a] -> [a] -> [a]
++ TestName
"\nTxBody =\n"
                    forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (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 (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 Map k (ScriptF era)
m = forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' forall era. Set Language -> ScriptF era -> Set Language
accum forall a. Set a
Set.empty Map k (ScriptF era)
m
  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 StandardCrypto)
ps)) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript (AlonzoEra StandardCrypto)
ps) Set Language
ans
    accum Set Language
ans (ScriptF Proof era
Babbage (PlutusScript PlutusScript (BabbageEra StandardCrypto)
ps)) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript (BabbageEra StandardCrypto)
ps) Set Language
ans
    accum Set Language
ans (ScriptF Proof era
Conway (PlutusScript PlutusScript (ConwayEra StandardCrypto)
ps)) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript (ConwayEra StandardCrypto)
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 (EraCrypto era))) ->
  (Set (TxIn (EraCrypto era))) ->
  (Map (TxIn (EraCrypto era)) (TxOutF era)) ->
  (Set (ScriptHash (EraCrypto era))) ->
  (Set (ScriptHash (EraCrypto era)))
adjustNeededByRefScripts :: forall era.
Proof era
-> Set (TxIn (EraCrypto era))
-> Set (TxIn (EraCrypto era))
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> Set (ScriptHash (EraCrypto era))
-> Set (ScriptHash (EraCrypto era))
adjustNeededByRefScripts Proof era
proof Set (TxIn (EraCrypto era))
inps Set (TxIn (EraCrypto era))
refinps Map (TxIn (EraCrypto era)) (TxOutF era)
ut Set (ScriptHash (EraCrypto era))
neededhashes = case forall era. Proof era -> TxOutWit era
whichTxOut Proof era
proof of
  TxOutWit era
TxOutShelleyToMary -> Set (ScriptHash (EraCrypto era))
neededhashes
  TxOutWit era
TxOutAlonzoToAlonzo -> Set (ScriptHash (EraCrypto era))
neededhashes
  TxOutWit era
TxOutBabbageToConway ->
    let spendUtxo :: UTxO era
spendUtxo = forall era. Map (TxIn (EraCrypto era)) (TxOutF era) -> UTxO era
liftUTxO Map (TxIn (EraCrypto era)) (TxOutF era)
ut
     in forall a. Ord a => Set a -> Set a -> Set a
Set.difference
          Set (ScriptHash (EraCrypto era))
neededhashes
          ( forall a. Ord a => Set a -> Set a -> Set a
Set.union
              (forall k a. Map k a -> Set k
Map.keysSet (forall era.
BabbageEraTxOut era =>
UTxO era
-> Set (TxIn (EraCrypto era))
-> Map (ScriptHash (EraCrypto era)) (Script era)
getReferenceScripts UTxO era
spendUtxo Set (TxIn (EraCrypto era))
inps))
              (forall k a. Map k a -> Set k
Map.keysSet (forall era.
BabbageEraTxOut era =>
UTxO era
-> Set (TxIn (EraCrypto era))
-> Map (ScriptHash (EraCrypto era)) (Script era)
getReferenceScripts UTxO era
spendUtxo Set (TxIn (EraCrypto era))
refinps))
          )

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

getUtxoCoinT ::
  Reflect era =>
  Term era (TxIn (EraCrypto era)) ->
  Term era (Map (TxIn (EraCrypto era)) (TxOutF era)) ->
  Target era Coin
getUtxoCoinT :: forall era.
Reflect era =>
Term era (TxIn (EraCrypto era))
-> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
-> Target era Coin
getUtxoCoinT Term era (TxIn (EraCrypto era))
feeinput Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
spending = forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"getUtxoCoin" forall {era} {k}.
(EraTxOut era, Ord k) =>
k -> Map k (TxOutF era) -> Coin
getUtxoCoin forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxIn (EraCrypto era))
feeinput forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
spending
  where
    getUtxoCoin :: k -> Map k (TxOutF era) -> Coin
getUtxoCoin k
input Map k (TxOutF era)
mp = case 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 forall s a. s -> Getting a s a -> a
^. forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
coinTxOutL
      Maybe (TxOutF era)
Nothing -> 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 forall a b. a -> (a -> b) -> b
& forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Integer -> Coin
Coin Integer
1000000)) forall a. a -> [a] -> [a]
: forall a. Int -> [a] -> [a]
take (Int
n forall a. Num a => a -> a -> a
- Int
1) [TxOutF era]
outputuniv
getNTxOut Size
x TxOutF era
_ [TxOutF era]
_ =
  forall a. HasCallStack => TestName -> a
error
    ( TestName
"Non (SzExact n): "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Size
x
        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 = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' forall {era}. EraTxOut era => Value era -> TxOutF era -> Value era
accum 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 forall s a. s -> Getting a s a -> a
^. forall era. EraTxOut era => Lens' (TxOut era) (Value era)
valueTxOutL forall t. Val t => t -> t -> t
<+> Value era
ans

minusMultiValue ::
  forall era.
  Reflect era =>
  Proof era ->
  Value era ->
  Value era ->
  Map (ScriptHash (EraCrypto era)) (Map AssetName Integer)
minusMultiValue :: forall era.
Reflect era =>
Proof era
-> Value era
-> Value era
-> Map (ScriptHash (EraCrypto era)) (Map AssetName Integer)
minusMultiValue Proof era
p Value era
v1 Value era
v2 = case forall era. Proof era -> ValueWit era
whichValue Proof era
p of
  ValueWit era
ValueMaryToConway -> case Value era
v1 forall t. Val t => t -> t -> t
<-> Value era
v2 of MaryValue Coin
_ (MultiAsset Map (PolicyID StandardCrypto) (Map AssetName Integer)
m) -> forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\(PolicyID ScriptHash StandardCrypto
x) -> ScriptHash StandardCrypto
x) Map (PolicyID StandardCrypto) (Map AssetName Integer)
m
  ValueWit era
ValueShelleyToAllegra -> 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
usCredScriptFreq :: UnivSize -> Int
usSpendScriptFreq :: UnivSize -> Int
usAllowReRegisterPool :: UnivSize -> Bool
usUnRegKeyFreq :: UnivSize -> Int
usRegKeyFreq :: UnivSize -> Int
usMaxCollaterals :: UnivSize -> Int
usMinCollaterals :: UnivSize -> Int
usMaxInputs :: UnivSize -> Int
usMinInputs :: UnivSize -> Int
usGenerateWithdrawals :: UnivSize -> Bool
usDatumFreq :: UnivSize -> Int
usMaxCerts :: UnivSize -> Int
usMinCerts :: UnivSize -> Int
usNumDReps :: UnivSize -> Int
usNumColUtxo :: UnivSize -> Int
usNumPreUtxo :: UnivSize -> Int
usNumTxIn :: UnivSize -> Int
usNumDatums :: UnivSize -> Int
usNumCredentials :: UnivSize -> Int
usNumVoteKeys :: UnivSize -> Int
usNumGenesisKeys :: UnivSize -> Int
usNumStakeKeys :: UnivSize -> Int
usNumPools :: UnivSize -> Int
usNumKeys :: UnivSize -> Int
usNumAddr :: UnivSize -> Int
usNumPtr :: UnivSize -> Int
usNumMultiAsset :: UnivSize -> Int
usMaxPolicyID :: UnivSize -> Int
usMaxAssets :: UnivSize -> Int
usNumTxOuts :: UnivSize -> Int
usCredScriptFreq :: Int
usSpendScriptFreq :: Int
usAllowReRegisterPool :: Bool
usUnRegKeyFreq :: Int
usRegKeyFreq :: Int
usMaxCollaterals :: Int
usMinCollaterals :: Int
usMaxInputs :: Int
usMinInputs :: Int
usGenerateWithdrawals :: Bool
usDatumFreq :: Int
usMaxCerts :: Int
usMinCerts :: Int
usNumDReps :: Int
usNumColUtxo :: Int
usNumPreUtxo :: Int
usNumTxIn :: Int
usNumDatums :: Int
usNumCredentials :: Int
usNumVoteKeys :: Int
usNumGenesisKeys :: Int
usNumStakeKeys :: Int
usNumPools :: Int
usNumKeys :: Int
usNumAddr :: Int
usNumPtr :: Int
usNumMultiAsset :: Int
usMaxPolicyID :: Int
usMaxAssets :: Int
usNumTxOuts :: Int
..} Proof era
p =
  (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 (forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof era
p))
    forall a. [a] -> [a] -> [a]
++ [ forall era.
Era era =>
Term era (Map (ScriptHash (EraCrypto era)) (Map AssetName Integer))
mint
          forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: ( forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"sumAssets" (\[TxOutF era]
out Map (TxIn StandardCrypto) (TxOutF era)
spend -> forall era.
Reflect era =>
Proof era
-> Value era
-> Value era
-> Map (ScriptHash (EraCrypto era)) (Map AssetName Integer)
minusMultiValue Proof era
p (forall era (t :: * -> *).
(Foldable t, Reflect era) =>
t (TxOutF era) -> Value era
txoutSum [TxOutF era]
out) (forall era (t :: * -> *).
(Foldable t, Reflect era) =>
t (TxOutF era) -> Value era
txoutSum Map (TxIn StandardCrypto) (TxOutF era)
spend))
                  forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. Era era => Proof era -> Term era [TxOutF era]
outputs Proof era
p)
                  forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (TxIn StandardCrypto) (TxOutF era))
spending
               )
       , forall era. Era era => Term era (Maybe Network)
networkID forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era t. Term era t -> Target era (Maybe t)
justTarget forall era. Era era => Term era Network
network
       , -- inputs
         forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
usMinInputs Int
usMaxInputs) forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
inputs
       , forall t era.
Ord t =>
Direct (Term era t) -> Term era (Set t) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Era era => Term era (TxIn (EraCrypto era))
feeTxIn) forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
inputs
       , forall t era.
Ord t =>
Term era (Set t) -> Term era (Set t) -> Pred era
Subset forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
inputs (forall t era b. Ord t => Term era (Map t b) -> Term era (Set t)
Dom (forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo Proof era
p))
       , -- collateral
         forall t era.
Ord t =>
Term era (Set t) -> Term era (Set t) -> Pred era
Disjoint forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
inputs forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
collateral
       , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range (Int
usMinCollaterals) (Int
usMaxCollaterals)) forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
collateral
       , forall t era.
Ord t =>
Term era (Set t) -> Term era (Set t) -> Pred era
Subset forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
collateral (forall t era b. Ord t => Term era (Map t b) -> Term era (Set t)
Dom Term era (Map (TxIn StandardCrypto) (TxOutF era))
colUtxo)
       , --       , Member (Left colInput) collateral
         Term era (Map (TxIn StandardCrypto) (TxOutF era))
colRestriction forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
collateral Term era (Map (TxIn StandardCrypto) (TxOutF era))
colUtxo
       , forall era t.
(Era era, Adds t) =>
Direct t -> Term era t -> OrdCond -> [Sum era t] -> Pred era
SumsTo (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1)) forall era. Era era => Term era Coin
sumCol OrdCond
EQL [forall t c b era.
Adds c =>
Rep era c -> Lens' t c -> Term era (Map b t) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL Term era (Map (TxIn StandardCrypto) (TxOutF era))
colRestriction]
       , Term era Coin
tempTotalCol forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall era. Era era => Term era Coin
sumCol
       , -- withdrawals
         forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
2) Term era (Set (Credential 'Staking StandardCrypto))
prewithdrawal
       , forall t era.
Ord t =>
Term era (Set t) -> Term era (Set t) -> Pred era
Subset Term era (Set (Credential 'Staking StandardCrypto))
prewithdrawal (forall t era b. Ord t => Term era (Map t b) -> Term era (Set t)
Dom Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
nonZeroRewards)
       , if Bool
usGenerateWithdrawals
          then
            forall era.
Era era =>
Term era (Map (RewardAccount (EraCrypto era)) Coin)
withdrawals
              forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: ( forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr
                      TestName
"mkRwrdAcnt"
                      ( \Set (Credential 'Staking StandardCrypto)
s Map (Credential 'Staking StandardCrypto) Coin
r ->
                          forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                            ( forall a b. (a -> b) -> [a] -> [b]
map
                                (\Credential 'Staking StandardCrypto
x -> (forall c. Network -> Credential 'Staking c -> RewardAccount c
RewardAccount Network
Testnet Credential 'Staking StandardCrypto
x, Map (Credential 'Staking StandardCrypto) Coin
r forall k a. Ord k => Map k a -> k -> a
Map.! Credential 'Staking StandardCrypto
x))
                                (forall a. Set a -> [a]
Set.toList Set (Credential 'Staking StandardCrypto)
s)
                            )
                      )
                      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (Credential 'Staking StandardCrypto))
prewithdrawal
                      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
rewards
                   )
          else forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
0) forall era.
Era era =>
Term era (Map (RewardAccount (EraCrypto era)) Coin)
withdrawals
       , Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
nonZeroRewards forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"filter (/=0)" (forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (forall a. Eq a => a -> a -> Bool
/= (Integer -> Coin
Coin Integer
0))) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
rewards)
       , -- refInputs
         forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
0 Int
1) forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
refInputs
       , forall t era.
Ord t =>
Term era (Set t) -> Term era (Set t) -> Pred era
Subset forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
refInputs (forall t era b. Ord t => Term era (Map t b) -> Term era (Set t)
Dom (forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo Proof era
p))
       , forall t era. Ord t => Term era t -> Term era (Set t) -> Pred era
NotMember forall era. Era era => Term era (TxIn (EraCrypto era))
feeTxIn forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
refInputs
       , forall t era.
Ord t =>
Term era (Set t) -> Term era (Set t) -> Pred era
Disjoint forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
refInputs forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
inputs -- New constraint in Conway, added PR #4024
       , forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Int -> Term era Size
Range Int
1 Int
2) forall era.
Era era =>
Term era (Set (KeyHash 'Witness (EraCrypto era)))
reqSignerHashes
       , forall t era.
Ord t =>
Term era (Set t) -> Term era (Set t) -> Pred era
Subset forall era.
Era era =>
Term era (Set (KeyHash 'Witness (EraCrypto era)))
reqSignerHashes (forall t era b. Ord t => Term era (Map t b) -> Term era (Set t)
Dom forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Witness (EraCrypto era))
     (KeyPair 'Witness (EraCrypto era)))
keymapUniv)
       , forall era. Era era => Term era SlotNo
ttl forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"(+5)" (\SlotNo
x -> SlotNo
x forall a. Num a => a -> a -> a
+ SlotNo
5) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era SlotNo
currentSlot)
       , Term era (Map (TxIn StandardCrypto) (TxOutF era))
spending forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
inputs (forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo Proof era
p)
       , forall era t.
(Era era, Adds t) =>
Direct t -> Term era t -> OrdCond -> [Sum era t] -> Pred era
SumsTo
          (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
          Term era Coin
balanceCoin
          OrdCond
EQL
          [forall t c b era.
Adds c =>
Rep era c -> Lens' t c -> Term era (Map b t) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL Term era (Map (TxIn StandardCrypto) (TxOutF era))
spending, forall c era t. Adds c => Term era (Map t c) -> Sum era c
SumMap forall era.
Era era =>
Term era (Map (RewardAccount (EraCrypto era)) Coin)
withdrawals, forall era c. Term era c -> Sum era c
One Term era Coin
txrefunds, forall era c. Term era c -> Sum era c
One Term era Coin
txdeposits]
       , Term era Coin
txrefunds
          forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: ( forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"certsRefunds" forall {era}.
EraTxCert era =>
PParamsF era
-> Map (Credential 'Staking (EraCrypto era)) Coin
-> Map (Credential 'DRepRole (EraCrypto era)) Coin
-> [TxCertF era]
-> Coin
certsRefunds
                  forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p
                  forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
stakeDeposits
                  forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term era (Map (Credential 'DRepRole (EraCrypto era)) Coin)
drepDepositsView
                  forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Reflect era => Term era [TxCertF era]
certs
               )
       , Term era Coin
txdeposits forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"certsDeposits" forall {era} {a}.
EraTxCert era =>
PParamsF era
-> Map (KeyHash 'StakePool (EraCrypto era)) a
-> [TxCertF era]
-> Coin
certsDeposits forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
regPools forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Reflect era => Term era [TxCertF era]
certs)
       , forall era. Reflect era => Term era (ScriptsNeededF era)
scriptsNeeded forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall era.
EraUTxO era =>
Proof era
-> Target
     era
     (TxBodyF era
      -> Map (TxIn (EraCrypto era)) (TxOutF era) -> ScriptsNeededF era)
needT Proof era
p forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
tempTxBody forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo Proof era
p)
       , forall era. Era era => Term era IsValid
txisvalid forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"allValid" [IsValid] -> IsValid
allValid forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era [IsValid]
valids)
       , forall t era b.
(Era era, Typeable t) =>
Term era (Maybe b) -> RootTarget era t b -> [Pred era] -> Pred era
Maybe forall era. Reflect era => Term era (Maybe (TxAuxDataF era))
txauxdata (forall era t. Term era t -> RootTarget era Void t
Simple Term era (TxAuxDataF era)
oneAuxdata) [forall era t. Term era t -> Pred era
Random Term era (TxAuxDataF era)
oneAuxdata]
       , forall era.
Era era =>
Term era (Maybe (AuxiliaryDataHash (EraCrypto era)))
adHash forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"hashMaybe" (forall era.
Reflect era =>
TxAuxDataF era -> AuxiliaryDataHash (EraCrypto era)
hashTxAuxDataF forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ 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.
         forall era t. Term era t -> Pred era
Random Term era (SafeHash StandardCrypto EraIndependentScriptIntegrity)
randomWppHash
       , Term
  era (Maybe (SafeHash StandardCrypto EraIndependentScriptIntegrity))
tempWppHash forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era t. Term era t -> Target era (Maybe t)
justTarget Term era (SafeHash StandardCrypto EraIndependentScriptIntegrity)
randomWppHash
       , Term era Coin
tempTxFee forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall t era. t -> Target era t
constTarget (Integer -> Coin
Coin (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word64)))
       , Term era (TxBodyF era)
tempTxBody
          forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe (ScriptIntegrityHash (EraCrypto era)))
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget Term era Coin
tempTxFee Term
  era (Maybe (SafeHash StandardCrypto EraIndependentScriptIntegrity))
tempWppHash (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall a. Bounded a => a
maxBound :: Word64))))
       , Term era (TxF era)
tempTx forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (BootstrapWitness (EraCrypto era)))
-> Term era (Set (WitVKey 'Witness (EraCrypto era)))
-> Target era (TxF era)
txTarget Term era (TxBodyF era)
tempTxBody Term era (Set (BootstrapWitness StandardCrypto))
tempBootWits Term era (Set (WitVKey 'Witness StandardCrypto))
tempKeyWits
       , -- Compute the real fee, and then recompute the TxBody and the Tx
         forall era. Era era => Term era Coin
txfee forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"finalFee" forall era.
EraUTxO era =>
PParamsF era
-> TxF era -> Map (TxIn (EraCrypto era)) (TxOutF era) -> Coin
computeFinalFee forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxF era)
tempTx forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo Proof era
p)
       , --  , txbodyterm :<-: txbodyTarget txfee wppHash totalCol
         --  , txterm :<-: txTarget txbodyterm bootWits keyWits
         forall t b t era.
Ord t =>
Lens' b t -> Rep era t -> Term era (Map t b) -> Term era (Map t t)
ProjM forall c. Lens' (DRepState c) Coin
drepDepositL forall era. Rep era Coin
CoinR forall era.
Era era =>
Term
  era
  (Map
     (Credential 'DRepRole (EraCrypto era)) (DRepState (EraCrypto era)))
currentDRepState forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall era.
Era era =>
Term era (Map (Credential 'DRepRole (EraCrypto era)) Coin)
drepDepositsView
       ]
    forall a. [a] -> [a] -> [a]
++ case 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
          forall era t. Term era t -> Pred era
Random forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers
        , forall era t. Term era t -> Pred era
Random forall era.
Reflect era =>
Term era (Map (DataHash (EraCrypto era)) (Data era))
dataWits
        , forall era t. Term era t -> Pred era
Random (forall era. Era era => Proof era -> Term era (TxOutF era)
collateralReturn Proof era
p)
        , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
extraCol
        , forall era t. Term era t -> Pred era
Random forall era. Era era => Term era Coin
totalCol
        , forall era t. Term era t -> Pred era
Random forall era.
Era era =>
Term
  era
  (Maybe (SafeHash (EraCrypto era) EraIndependentScriptIntegrity))
wppHash
        , forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict (forall t t era. Lens' t t -> Rep era t -> Term era t -> Term era t
Proj forall era.
(ScriptsNeeded era ~ ShelleyScriptsNeeded era) =>
Lens' (ScriptsNeededF era) (Set (ScriptHash (EraCrypto era)))
smNeededL (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era. Era era => Rep era (ScriptHash (EraCrypto era))
ScriptHashR) forall era. Reflect era => Term era (ScriptsNeededF era)
scriptsNeeded) (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
allScriptUniv Proof era
p) forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
scriptWits
        , forall t b era. (Ord t, Eq b) => Term era (Map t b) -> Term era [b]
Elems (forall t b t era.
Ord t =>
Lens' b t -> Rep era t -> Term era (Map t b) -> Term era (Map t t)
ProjM forall a b. Lens' (a, b) a
fstL forall era. Rep era IsValid
IsValidR (forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict (forall t era b. Ord t => Term era (Map t b) -> Term era (Set t)
Dom forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
scriptWits) forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (IsValid, ScriptF era))
plutusUniv)) forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall era. Era era => Term era [IsValid]
valids
        , Term era (Set (BootstrapWitness StandardCrypto))
tempBootWits forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"boots" (forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxBodyF era
-> Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey)
-> Set (BootstrapWitness (EraCrypto era))
bootWitsT Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (TxIn StandardCrypto) (TxOutF era))
spending forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
tempTxBody forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv)
        , Term era (Set (KeyHash 'Witness StandardCrypto))
necessaryHashes forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Target era (Set (KeyHash 'Witness (EraCrypto era)))
necessaryKeyHashTarget @era Term era (TxBodyF era)
tempTxBody (forall era t. Rep era t -> t -> Term era t
Lit (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era. Era era => Rep era (KeyHash 'Witness (EraCrypto era))
WitHashR) forall a. Set a
Set.empty)
        , Term era (Set (KeyHash 'Witness StandardCrypto))
sufficientHashes
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"sufficient" (forall era.
Reflect era =>
Proof era
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> [TxCertF era]
-> Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
-> Set (KeyHash 'Witness (EraCrypto era))
sufficientKeyHashes Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
scriptWits forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Reflect era => Term era [TxCertF era]
certs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
genDelegs)
        , Term era (Set (WitVKey 'Witness StandardCrypto))
tempKeyWits
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
-> Term
     era
     (Map
        (KeyHash 'Payment (EraCrypto era))
        (Addr (EraCrypto era), SigningKey))
-> Target era (Set (WitVKey 'Witness (EraCrypto era)))
makeKeyWitnessTarget Term era (TxBodyF era)
tempTxBody Term era (Set (KeyHash 'Witness StandardCrypto))
necessaryHashes Term era (Set (KeyHash 'Witness StandardCrypto))
sufficientHashes forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
scriptWits forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv
        , forall era.
Reflect era =>
Term era (Set (BootstrapWitness (EraCrypto era)))
bootWits forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"boots" (forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxBodyF era
-> Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey)
-> Set (BootstrapWitness (EraCrypto era))
bootWitsT Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (TxIn StandardCrypto) (TxOutF era))
spending forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv)
        , forall era.
Reflect era =>
Term era (Set (WitVKey 'Witness (EraCrypto era)))
keyWits
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
-> Term
     era
     (Map
        (KeyHash 'Payment (EraCrypto era))
        (Addr (EraCrypto era), SigningKey))
-> Target era (Set (WitVKey 'Witness (EraCrypto era)))
makeKeyWitnessTarget forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (Set (KeyHash 'Witness StandardCrypto))
necessaryHashes Term era (Set (KeyHash 'Witness StandardCrypto))
sufficientHashes forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
scriptWits forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv
        , forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe (ScriptIntegrityHash (EraCrypto era)))
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget forall era. Era era => Term era Coin
txfee Term
  era (Maybe (SafeHash StandardCrypto EraIndependentScriptIntegrity))
tempWppHash (forall era t. Rep era t -> t -> Term era t
Lit forall era. Rep era Coin
CoinR (Integer -> Coin
Coin Integer
0)) -- The WppHash and totalCol play no role in ShelleyToMary
        , forall era. Reflect era => Term era (TxF era)
txterm forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (BootstrapWitness (EraCrypto era)))
-> Term era (Set (WitVKey 'Witness (EraCrypto era)))
-> Target era (TxF era)
txTarget forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era.
Reflect era =>
Term era (Set (BootstrapWitness (EraCrypto era)))
bootWits forall era.
Reflect era =>
Term era (Set (WitVKey 'Witness (EraCrypto era)))
keyWits
        ]
      UTxOWit era
UTxOAlonzoToConway ->
        [ forall t era. Sizeable t => Term era Size -> Term era t -> Pred era
Sized (forall era. Era era => Int -> Term era Size
ExactSize Int
0) forall era. Era era => Term era Coin
txDonation
        , forall t t era. Lens' t t -> Rep era t -> Term era t -> Term era t
Proj forall era.
(ScriptsNeeded era ~ AlonzoScriptsNeeded era) =>
Lens'
  (ScriptsNeededF era)
  [(PlutusPurposeF era, ScriptHash (EraCrypto era))]
acNeededL (forall era t. Rep era t -> Rep era [t]
ListR (forall era t b. Rep era t -> Rep era b -> Rep era (t, b)
PairR (forall era. Era era => Proof era -> Rep era (PlutusPurposeF era)
ScriptPurposeR Proof era
p) forall era. Era era => Rep era (ScriptHash (EraCrypto era))
ScriptHashR)) forall era. Reflect era => Term era (ScriptsNeededF era)
scriptsNeeded forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: Term era [(PlutusPurposeF era, ScriptHash (EraCrypto era))]
acNeeded
        , -- Hashes of scripts that will be run. Not all of these will be in the 'scriptWits'
          Term era (Set (ScriptHash StandardCrypto))
neededHashSet forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"toSet" (\[(PlutusPurposeF era, ScriptHash StandardCrypto)]
x -> forall a. Ord a => [a] -> Set a
Set.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(PlutusPurposeF era, ScriptHash StandardCrypto)]
x)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [(PlutusPurposeF era, ScriptHash (EraCrypto era))]
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 StandardCrypto))
refAdjusted
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"adjust" (forall era.
Proof era
-> Set (TxIn (EraCrypto era))
-> Set (TxIn (EraCrypto era))
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> Set (ScriptHash (EraCrypto era))
-> Set (ScriptHash (EraCrypto era))
adjustNeededByRefScripts Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
inputs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
refInputs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (ScriptHash StandardCrypto))
neededHashSet)
        , -- , scriptWits :=: Restrict refAdjusted (allScriptUniv p)
          forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict Term era (Set (ScriptHash StandardCrypto))
refAdjusted (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
allScriptUniv Proof era
p) forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
scriptWits
        , forall t b era. (Ord t, Eq b) => Term era (Map t b) -> Term era [b]
Elems (forall t b t era.
Ord t =>
Lens' b t -> Rep era t -> Term era (Map t b) -> Term era (Map t t)
ProjM forall a b. Lens' (a, b) a
fstL forall era. Rep era IsValid
IsValidR (forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict Term era (Set (ScriptHash StandardCrypto))
neededHashSet forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (IsValid, ScriptF era))
plutusUniv)) forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall era. Era era => Term era [IsValid]
valids
        , Term era (Set (PlutusPointerF era))
rdmrPtrs forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall era any.
AlonzoEraScript era =>
Target
  era
  ([(PlutusPurposeF era, ScriptHash (EraCrypto era))]
   -> Map (ScriptHash (EraCrypto era)) any
   -> Set (PlutusPointerF era))
rdmrPtrsT forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [(PlutusPurposeF era, ScriptHash (EraCrypto era))]
acNeeded forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (IsValid, ScriptF era))
plutusUniv)
        , Term era (Set (PlutusPointerF era))
rdmrPtrs forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall t era b. Ord t => Term era (Map t b) -> Term era (Set t)
Dom forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers
        , forall era t.
RootTarget era t Bool -> Pred era -> Pred era -> Pred era
If
            (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"null" forall a. Set a -> Bool
Set.null forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (PlutusPointerF era))
rdmrPtrs)
            (forall era t b. Term era t -> Term era b -> Pred era
Before (forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers)
            (forall era t.
(Era era, Adds t) =>
Direct t -> Term era t -> OrdCond -> [Sum era t] -> Pred era
SumsTo (forall a b. a -> Either a b
Left (Natural -> Natural -> ExUnits
ExUnits Natural
1 Natural
1)) (forall era. AlonzoEraPParams era => Proof era -> Term era ExUnits
maxTxExUnits Proof era
p) OrdCond
GTE [forall t c b era.
Adds c =>
Rep era c -> Lens' t c -> Term era (Map b t) -> Sum era c
ProjMap forall era. Rep era ExUnits
ExUnitsR forall a b. Lens' (a, b) b
sndL forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers])
        , Term era (Set (DataHash StandardCrypto))
plutusDataHashes
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: ( forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"plutusDataHashes" forall era.
(AlonzoEraTxOut era, EraTxBody era, AlonzoEraScript era) =>
Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxBodyF era
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> Set (DataHash (EraCrypto era))
getPlutusDataHashes
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo Proof era
p
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
tempTxBody
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
allScriptUniv Proof era
p
                 )
        , forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict Term era (Set (DataHash StandardCrypto))
plutusDataHashes forall era.
Era era =>
Term era (Map (DataHash (EraCrypto era)) (Data era))
dataUniv forall t era. Eq t => Term era t -> Term era t -> Pred era
:=: forall era.
Reflect era =>
Term era (Map (DataHash (EraCrypto era)) (Data era))
dataWits
        , Term era (Set (BootstrapWitness StandardCrypto))
tempBootWits forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"boots" (forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxBodyF era
-> Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey)
-> Set (BootstrapWitness (EraCrypto era))
bootWitsT Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (TxIn StandardCrypto) (TxOutF era))
spending forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (TxBodyF era)
tempTxBody forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv)
        , Term era (Set (KeyHash 'Witness StandardCrypto))
necessaryHashes forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Target era (Set (KeyHash 'Witness (EraCrypto era)))
necessaryKeyHashTarget @era Term era (TxBodyF era)
tempTxBody forall era.
Era era =>
Term era (Set (KeyHash 'Witness (EraCrypto era)))
reqSignerHashes
        , Term era (Set (KeyHash 'Witness StandardCrypto))
sufficientHashes
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: ( forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"sufficient" (forall era.
Reflect era =>
Proof era
-> Map (ScriptHash (EraCrypto era)) (ScriptF era)
-> [TxCertF era]
-> Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era))
-> Set (KeyHash 'Witness (EraCrypto era))
sufficientKeyHashes Proof era
p)
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict Term era (Set (ScriptHash StandardCrypto))
neededHashSet (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
allScriptUniv Proof era
p))
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Reflect era => Term era [TxCertF era]
certs
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Genesis (EraCrypto era)) (GenDelegPair (EraCrypto era)))
genDelegs
                 )
        , Term era (Set (WitVKey 'Witness StandardCrypto))
tempKeyWits
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
-> Term
     era
     (Map
        (KeyHash 'Payment (EraCrypto era))
        (Addr (EraCrypto era), SigningKey))
-> Target era (Set (WitVKey 'Witness (EraCrypto era)))
makeKeyWitnessTarget Term era (TxBodyF era)
tempTxBody Term era (Set (KeyHash 'Witness StandardCrypto))
necessaryHashes Term era (Set (KeyHash 'Witness StandardCrypto))
sufficientHashes forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
scriptWits forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv
        , forall era.
Reflect era =>
Term era (Set (BootstrapWitness (EraCrypto era)))
bootWits forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"boots" (forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxBodyF era
-> Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey)
-> Set (BootstrapWitness (EraCrypto era))
bootWitsT Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map (TxIn StandardCrypto) (TxOutF era))
spending forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), SigningKey))
byronAddrUniv)
        , forall era.
Reflect era =>
Term era (Set (WitVKey 'Witness (EraCrypto era)))
keyWits
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Term era (Set (KeyHash 'Witness (EraCrypto era)))
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
-> Term
     era
     (Map
        (KeyHash 'Payment (EraCrypto era))
        (Addr (EraCrypto era), SigningKey))
-> Target era (Set (WitVKey 'Witness (EraCrypto era)))
makeKeyWitnessTarget forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (Set (KeyHash 'Witness StandardCrypto))
necessaryHashes Term era (Set (KeyHash 'Witness StandardCrypto))
sufficientHashes forall era.
Reflect era =>
Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
scriptWits forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'Payment (EraCrypto era))
     (Addr (EraCrypto era), 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 forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"languages" forall k era. Map k (ScriptF era) -> Set Language
scriptWitsLangs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall t era b.
Ord t =>
Term era (Set t) -> Term era (Map t b) -> Term era (Map t b)
Restrict Term era (Set (ScriptHash StandardCrypto))
neededHashSet (forall era.
Era era =>
Proof era
-> Term era (Map (ScriptHash (EraCrypto era)) (ScriptF era))
allScriptUniv Proof era
p)))
        , forall era.
Era era =>
Term
  era
  (Maybe (SafeHash (EraCrypto era) EraIndependentScriptIntegrity))
wppHash forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: 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 (EraCrypto era1)) (Data era1))
-> Target era2 (Maybe (ScriptIntegrityHash (EraCrypto era1)))
integrityHash Proof era
p (forall era. EraGov era => Proof era -> Term era (PParamsF era)
pparams Proof era
p) Term era (Set Language)
langs forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers forall era.
Reflect era =>
Term era (Map (DataHash (EraCrypto era)) (Data era))
dataWits
        , forall era. Era era => Term era Coin
owed
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: ( forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"owed" (\Natural
percent (Coin Integer
fee) -> Rational -> Coin
rationalToCoinViaCeiling ((forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
percent forall a. Num a => a -> a -> a
* Integer
fee) forall a. Integral a => a -> a -> Ratio a
% Integer
100))
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall era. AlonzoEraPParams era => Proof era -> Term era Natural
collateralPercentage Proof era
p)
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ 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'
          forall era. Era era => Term era Coin
extraCol
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"extraCol" (\(Coin Integer
suminputs) (Coin Integer
owe) -> (Integer -> Coin
Coin (Integer
owe forall a. Num a => a -> a -> a
+ Integer
1 forall a. Num a => a -> a -> a
- Integer
suminputs))) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Coin
sumCol forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Coin
owed)
        , forall era. Era era => Term era Coin
totalCol forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"(<+>)" (\Coin
x Coin
y -> Coin
x forall t. Val t => t -> t -> t
<+> Coin
y forall t. Val t => t -> t -> t
<-> Integer -> Coin
Coin Integer
1) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Coin
extraCol forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Coin
sumCol)
        , forall t era.
Ord t =>
Direct (Term era t) -> Term era (Set t) -> Pred era
Member (forall a b. b -> Either a b
Right forall era. Era era => Term era (Addr (EraCrypto era))
colRetAddr) forall era. Era era => Term era (Set (Addr (EraCrypto era)))
addrUniv
        , -- This ( collateralReturn) depends on the Coin in the TxOut being (Coin 1).
          -- The computation of 'owed' and 'extraCol" should ensure this.
          forall era. Era era => Proof era -> Term era (TxOutF era)
collateralReturn Proof era
p
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"colReturn" (\Addr StandardCrypto
ad -> forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
p (forall era.
(EraTxOut era, HasCallStack) =>
Addr (EraCrypto era) -> Value era -> TxOut era
mkBasicTxOut Addr StandardCrypto
ad (forall t s. Inject t s => t -> s
inject (Integer -> Coin
Coin Integer
1)))) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Addr (EraCrypto era))
colRetAddr)
        , -- We compute this, so that we can test that the (Coin 1) invariant holds.
          forall era. Era era => Term era Coin
colRetCoin
            forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: (forall t b era.
TestName -> (t -> b) -> RootTarget era Void (t -> b)
Constr TestName
"-" (\Coin
sumc Coin
extra Coin
owe -> (Coin
sumc forall a. Semigroup a => a -> a -> a
<> Coin
extra) forall t. Val t => t -> t -> t
<-> Coin
owe) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Coin
sumCol forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Coin
extraCol forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era Coin
owed)
        , forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe (ScriptIntegrityHash (EraCrypto era)))
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget forall era. Era era => Term era Coin
txfee forall era.
Era era =>
Term
  era
  (Maybe (SafeHash (EraCrypto era) EraIndependentScriptIntegrity))
wppHash forall era. Era era => Term era Coin
totalCol
        , forall era. Reflect era => Term era (TxF era)
txterm forall era t b. Term era t -> RootTarget era b t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (BootstrapWitness (EraCrypto era)))
-> Term era (Set (WitVKey 'Witness (EraCrypto era)))
-> Target era (TxF era)
txTarget forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era.
Reflect era =>
Term era (Set (BootstrapWitness (EraCrypto era)))
bootWits forall era.
Reflect era =>
Term era (Set (WitVKey 'Witness (EraCrypto era)))
keyWits
        ]
  where
    spending :: Term era (Map (TxIn StandardCrypto) (TxOutF era))
spending = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
TestName -> Rep era t -> Access era s t -> V era t
V TestName
"spending" (forall t era b.
Ord t =>
Rep era t -> Rep era b -> Rep era (Map t b)
MapR forall era. Era era => Rep era (TxIn (EraCrypto era))
TxInR (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) forall era s t. Access era s t
No)
    colUtxo :: Term era (Map (TxIn StandardCrypto) (TxOutF era))
colUtxo = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
TestName -> Rep era t -> Access era s t -> V era t
V TestName
"colUtxo" (forall t era b.
Ord t =>
Rep era t -> Rep era b -> Rep era (Map t b)
MapR forall era. Era era => Rep era (TxIn (EraCrypto era))
TxInR (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) forall era s t. Access era s t
No)
    colRestriction :: Term era (Map (TxIn StandardCrypto) (TxOutF era))
colRestriction = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
TestName -> Rep era t -> Access era s t -> V era t
V TestName
"colRestriction" (forall t era b.
Ord t =>
Rep era t -> Rep era b -> Rep era (Map t b)
MapR forall era. Era era => Rep era (TxIn (EraCrypto era))
TxInR (forall era. Era era => Proof era -> Rep era (TxOutF era)
TxOutR Proof era
p)) forall era s t. Access era s t
No)
    nonZeroRewards :: Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
nonZeroRewards = forall era t. Era era => TestName -> Rep era t -> Term era t
var TestName
"nonZeroRewards" (forall t era b.
Ord t =>
Rep era t -> Rep era b -> Rep era (Map t b)
MapR forall era.
Era era =>
Rep era (Credential 'Staking (EraCrypto era))
CredR forall era. Rep era Coin
CoinR)
    balanceCoin :: Term era Coin
balanceCoin = forall era t. V era t -> Term era t
Var (forall era t s.
Era era =>
TestName -> Rep era t -> Access era s t -> V era t
V TestName
"balanceCoin" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No)
    certsRefunds :: PParamsF era
-> Map (Credential 'Staking (EraCrypto era)) Coin
-> Map (Credential 'DRepRole (EraCrypto era)) Coin
-> [TxCertF era]
-> Coin
certsRefunds (PParamsF Proof era
_ PParams era
pp) Map (Credential 'Staking (EraCrypto era)) Coin
stakingDepositsx Map (Credential 'DRepRole (EraCrypto era)) Coin
drepDepositsx [TxCertF era]
certsx =
      forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (Credential 'Staking (EraCrypto era) -> Maybe Coin)
-> (Credential 'DRepRole (EraCrypto era) -> Maybe Coin)
-> f (TxCert era)
-> Coin
getTotalRefundsTxCerts
        PParams era
pp
        (forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map (Credential 'Staking (EraCrypto era)) Coin
stakingDepositsx)
        (forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map (Credential 'DRepRole (EraCrypto era)) Coin
drepDepositsx)
        (forall a b. (a -> b) -> [a] -> [b]
map forall era. TxCertF era -> TxCert era
unTxCertF [TxCertF era]
certsx)
    certsDeposits :: PParamsF era
-> Map (KeyHash 'StakePool (EraCrypto era)) a
-> [TxCertF era]
-> Coin
certsDeposits (PParamsF Proof era
_ PParams era
pp) Map (KeyHash 'StakePool (EraCrypto era)) a
regpools [TxCertF era]
certsx = Integer -> Coin
Coin (-Integer
n)
      where
        Coin Integer
n = forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (KeyHash 'StakePool (EraCrypto era) -> Bool)
-> f (TxCert era)
-> Coin
getTotalDepositsTxCerts PParams era
pp (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map (KeyHash 'StakePool (EraCrypto era)) a
regpools) (forall a b. (a -> b) -> [a] -> [b]
map forall era. TxCertF era -> TxCert era
unTxCertF [TxCertF era]
certsx)
    txrefunds :: Term era Coin
txrefunds = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"txrefunds" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No)
    txdeposits :: Term era Coin
txdeposits = forall era t. V era t -> Term era t
Var (forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"txdeposits" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No)
    acNeeded :: Term era [(PlutusPurposeF era, ScriptHash (EraCrypto era))]
    acNeeded :: Term era [(PlutusPurposeF era, ScriptHash (EraCrypto era))]
acNeeded = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"acNeeded" (forall era t. Rep era t -> Rep era [t]
ListR (forall era t b. Rep era t -> Rep era b -> Rep era (t, b)
PairR (forall era. Era era => Proof era -> Rep era (PlutusPurposeF era)
ScriptPurposeR Proof era
p) forall era. Era era => Rep era (ScriptHash (EraCrypto era))
ScriptHashR)) forall era s t. Access era s t
No
    neededHashSet :: Term era (Set (ScriptHash StandardCrypto))
neededHashSet = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"neededHashSet" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era. Era era => Rep era (ScriptHash (EraCrypto era))
ScriptHashR) forall era s t. Access era s t
No
    rdmrPtrs :: Term era (Set (PlutusPointerF era))
rdmrPtrs = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"rdmrPtrs" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR (forall era. Era era => Proof era -> Rep era (PlutusPointerF era)
RdmrPtrR Proof era
p)) forall era s t. Access era s t
No
    plutusDataHashes :: Term era (Set (DataHash StandardCrypto))
plutusDataHashes = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"plutusDataHashes" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era. Era era => Rep era (DataHash (EraCrypto era))
DataHashR) forall era s t. Access era s t
No
    oneAuxdata :: Term era (TxAuxDataF era)
oneAuxdata = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"oneAuxdata" (forall era. Era era => Proof era -> Rep era (TxAuxDataF era)
TxAuxDataR forall era. Reflect era => Proof era
reify) forall era s t. Access era s t
No
    tempTxFee :: Term era Coin
tempTxFee = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempTxFee" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No
    tempTx :: Term era (TxF era)
tempTx = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempTx" (forall era. Era era => Proof era -> Rep era (TxF era)
TxR Proof era
p) forall era s t. Access era s t
No
    tempTxBody :: Term era (TxBodyF era)
tempTxBody = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempTxBody" (forall era. Era era => Proof era -> Rep era (TxBodyF era)
TxBodyR forall era. Reflect era => Proof era
reify) forall era s t. Access era s t
No
    tempWppHash :: Term
  era (Maybe (SafeHash StandardCrypto EraIndependentScriptIntegrity))
tempWppHash = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempWppHash" (forall era t. Rep era t -> Rep era (Maybe t)
MaybeR forall era.
Era era =>
Rep era (SafeHash (EraCrypto era) EraIndependentScriptIntegrity)
ScriptIntegrityHashR) forall era s t. Access era s t
No
    randomWppHash :: Term era (SafeHash StandardCrypto EraIndependentScriptIntegrity)
randomWppHash = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"randomWppHash" forall era.
Era era =>
Rep era (SafeHash (EraCrypto era) EraIndependentScriptIntegrity)
ScriptIntegrityHashR forall era s t. Access era s t
No
    tempBootWits :: Term era (Set (BootstrapWitness StandardCrypto))
tempBootWits = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempBootWits" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR (forall era. Era era => Rep era (BootstrapWitness (EraCrypto era))
BootstrapWitnessR @era)) forall era s t. Access era s t
No
    tempKeyWits :: Term era (Set (WitVKey 'Witness StandardCrypto))
tempKeyWits = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempKeyWits" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR (forall era.
Era era =>
Proof era -> Rep era (WitVKey 'Witness (EraCrypto era))
WitVKeyR forall era. Reflect era => Proof era
reify)) forall era s t. Access era s t
No
    langs :: Term era (Set Language)
langs = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"langs" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era. Rep era Language
LanguageR) forall era s t. Access era s t
No
    tempTotalCol :: Term era Coin
tempTotalCol = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"tempTotalCol" forall era. Rep era Coin
CoinR forall era s t. Access era s t
No
    prewithdrawal :: Term era (Set (Credential 'Staking StandardCrypto))
prewithdrawal = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"preWithdrawal" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era.
Era era =>
Rep era (Credential 'Staking (EraCrypto era))
CredR) forall era s t. Access era s t
No
    refAdjusted :: Term era (Set (ScriptHash StandardCrypto))
refAdjusted = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"refAdjusted" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era. Era era => Rep era (ScriptHash (EraCrypto era))
ScriptHashR) forall era s t. Access era s t
No
    necessaryHashes :: Term era (Set (KeyHash 'Witness StandardCrypto))
necessaryHashes = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"necessaryHashes" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era. Era era => Rep era (KeyHash 'Witness (EraCrypto era))
WitHashR) forall era s t. Access era s t
No
    sufficientHashes :: Term era (Set (KeyHash 'Witness StandardCrypto))
sufficientHashes = forall era t. V era t -> Term era t
Var forall a b. (a -> b) -> a -> b
$ forall era t s.
Proof era -> TestName -> Rep era t -> Access era s t -> V era t
pV Proof era
p TestName
"sufficientHashes" (forall t era. Ord t => Rep era t -> Rep era (Set t)
SetR forall era. Era era => Rep era (KeyHash 'Witness (EraCrypto era))
WitHashR) 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 = forall era.
(HasCallStack, Reflect era) =>
UnivSize -> Proof era -> [Pred era]
txBodyPreds UnivSize
sizes Proof era
proof
  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 = 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) = forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (\t
t -> t
t forall a b. a -> (a -> b) -> b
& Lens' t Coin
l forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Coin
thecoin forall a. Semigroup a => a -> a -> a
<> t
t forall s a. s -> Getting a s a -> a
^. 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 forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo forall era. Reflect era => Proof era
reify of
  u :: Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
u@(Var V era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxoV) -> do
    TxIn StandardCrypto
feeinput <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env forall era. Era era => Term era (TxIn (EraCrypto era))
feeTxIn
    Coin
feecoin <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env forall era. Era era => Term era Coin
txfee
    Map (TxIn StandardCrypto) (TxOutF era)
utxomap <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
u
    forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall era t. V era t -> t -> Env era -> Env era
storeVar V era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxoV (forall k t.
Ord k =>
[(k, Coin)] -> Map k t -> Lens' t Coin -> Map k t
balanceMap [(TxIn StandardCrypto
feeinput, Coin
feecoin)] Map (TxIn StandardCrypto) (TxOutF era)
utxomap forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL) Env era
env)
  Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
other -> forall a. [TestName] -> Typed a
failT [TestName
"utxo does not match a Var Term: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Term era (Map (TxIn (EraCrypto era)) (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 (EraCrypto era)) ->
  -- 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 (EraCrypto era)) (TxOutF era))
utxoterm = forall era.
Era era =>
Proof era -> Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxo forall era. Reflect era => Proof era
reify
      utxoV :: V era (Map (TxIn StandardCrypto) (TxOutF era))
utxoV = forall era t. Term era t -> V era t
unVar Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxoterm
  Coin
extracoin <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env forall era. Era era => Term era Coin
extraCol
  Map (TxIn StandardCrypto) (TxOutF era)
utxomap <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map (TxIn (EraCrypto era)) (TxOutF era))
utxoterm
  Set (TxIn StandardCrypto)
col <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env forall era. Era era => Term era (Set (TxIn (EraCrypto era)))
collateral
  case forall k v.
(Ord k, Show k) =>
[k] -> Map k v -> Coin -> Lens' v Coin -> Maybe (Map k v)
adjustC (forall a. Set a -> [a]
Set.toList Set (TxIn StandardCrypto)
col) Map (TxIn StandardCrypto) (TxOutF era)
utxomap Coin
extracoin forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL of
    Maybe (Map (TxIn StandardCrypto) (TxOutF era))
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a
discard
    Just Map (TxIn StandardCrypto) (TxOutF era)
newutxo -> do
      let env2 :: Env era
env2 = forall era t. V era t -> t -> Env era -> Env era
storeVar V era (Map (TxIn StandardCrypto) (TxOutF era))
utxoV Map (TxIn StandardCrypto) (TxOutF era)
newutxo Env era
env
      (Env era
env5, TxBodyF era
body) <- forall a b era.
(a -> b -> a)
-> Term era a -> Target era b -> Env era -> Typed (Env era, b)
updateTarget forall x. x -> x -> x
override forall era. Reflect era => Term era (TxBodyF era)
txbodyterm (forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe (ScriptIntegrityHash (EraCrypto era)))
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget forall era. Era era => Term era Coin
txfee forall era.
Era era =>
Term
  era
  (Maybe (SafeHash (EraCrypto era) EraIndependentScriptIntegrity))
wppHash forall era. Era era => Term era Coin
totalCol) Env era
env2
      (Env era
env6, TxF era
_) <-
        forall a b era.
(a -> b -> a)
-> Term era a -> Target era b -> Env era -> Typed (Env era, b)
updateTarget forall x. x -> x -> x
override forall era. Reflect era => Term era (TxF era)
txterm (forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (BootstrapWitness (EraCrypto era)))
-> Term era (Set (WitVKey 'Witness (EraCrypto era)))
-> Target era (TxF era)
txTarget (forall era t. Rep era t -> t -> Term era t
Lit (forall era. Era era => Proof era -> Rep era (TxBodyF era)
TxBodyR forall era. Reflect era => Proof era
reify) TxBodyF era
body) forall era.
Reflect era =>
Term era (Set (BootstrapWitness (EraCrypto era)))
bootWits forall era.
Reflect era =>
Term era (Set (WitVKey 'Witness (EraCrypto era)))
keyWits) Env era
env5
      forall (f :: * -> *) a. Applicative f => a -> f a
pure (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 forall a. Ord a => a -> a -> Bool
< (Integer -> Coin
Coin Integer
0) = forall a. Maybe a
Nothing
adjustC [] Map k v
m Coin
_ Lens' v Coin
_ = 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 forall a. Ord a => a -> a -> Ordering
compare Integer
n Integer
0 of
  Ordering
EQ -> forall a. a -> Maybe a
Just Map k v
m
  Ordering
GT -> forall a. a -> Maybe a
Just (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 forall a b. a -> (a -> b) -> b
& Lens' v Coin
coinL forall s t a b. ASetter s t a b -> b -> s -> t
.~ ((v
outf forall s a. s -> Getting a s a -> a
^. Lens' v Coin
coinL) forall t. Val t => t -> t -> t
<+> Coin
extra)
  Ordering
LT ->
    if Integer
ex forall a. Ord a => a -> a -> Bool
>= Integer
0
      then forall a. a -> Maybe a
Just (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 forall k v.
(Ord k, Show k) =>
[k] -> Map k v -> Coin -> Lens' v Coin -> Maybe (Map k v)
adjustC [k]
is (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 Lens' v Coin
coinL
    where
      amount :: Coin
amount@(Coin Integer
ex) = case 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 forall s a. s -> Getting a s a -> a
^. Lens' v Coin
coinL) forall t. Val t => t -> t -> t
<+> Coin
extra forall t. Val t => t -> t -> t
<-> (Integer -> Coin
Coin Integer
1)
        Maybe v
Nothing -> forall a. HasCallStack => TestName -> a
error (TestName
"Collateral input: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show k
i forall a. [a] -> [a] -> [a]
++ TestName
" is not found in UTxO in 'adjust'")
      subextra :: v -> v
subextra v
outf = v
outf forall a b. a -> (a -> b) -> b
& Lens' v Coin
coinL forall s t a b. ASetter s t a b -> b -> s -> t
.~ (Integer -> Coin
Coin (forall a. Ord a => a -> a -> a
max Integer
1 (Coin -> Integer
unCoin ((v
outf forall s a. s -> Getting a s a -> a
^. Lens' v Coin
coinL) 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 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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
_ = forall a. [TestName] -> Typed a
failT [TestName
"Non Var in updateVal: " forall a. [a] -> [a] -> [a]
++ 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 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term
  b
deltaV <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era b
delta
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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
_ = forall a. [TestName] -> Typed a
failT [TestName
"Non Var in updateTerm: " forall a. [a] -> [a] -> [a]
++ 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 <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era a
term
  b
deltaV <- forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env Target era b
delta
  forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ (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
_ = forall a. [TestName] -> Typed a
failT [TestName
"Non Var in updateTarget: " forall a. [a] -> [a] -> [a]
++ 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 <-
    ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
txBodyStage UnivSize
sizes Proof era
proof
    )
  Env era
env0 <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv
  Env era
env1 <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env era
env0
  Env era
env2 <- forall t. HasCallStack => Typed t -> t
errorTyped forall a b. (a -> b) -> a -> b
$ forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env1
  LedgerState era
ledger <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env2 (forall era.
EraGov era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
proof)
  (TxF Proof era
_ Tx era
tx) <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era t. V era t -> Env era -> Typed t
findVar (forall era t. Term era t -> V era t
unVar forall era. Reflect era => Term era (TxF era)
txterm) Env era
env2)
  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 <-
    ( forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
txBodyStage UnivSize
sizes Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
epochStateStage Proof era
proof
        forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
newEpochStateStage Proof era
proof
    )
  Env era
env0 <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv
  Env era
env1 <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env era
env0
  Env era
env2 <- forall t. HasCallStack => Typed t -> t
errorTyped forall a b. (a -> b) -> a -> b
$ forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env1
  NewEpochState era
newepochst <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env2 (forall era.
EraGov era =>
Proof era -> RootTarget era (NewEpochState era) (NewEpochState era)
newEpochStateT Proof era
proof)
  TxF Proof era
_ Tx era
tx <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era t. V era t -> Env era -> Typed t
findVar (forall era t. Term era t -> V era t
unVar forall era. Reflect era => Term era (TxF era)
txterm) Env era
env2)
  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 StandardCrypto)
proof = Proof (ConwayEra StandardCrypto)
Conway
  (NewEpochState (ConwayEra StandardCrypto)
nes, AlonzoTx (ConwayEra StandardCrypto)
_tx, Env (ConwayEra StandardCrypto)
env) <- forall a. Gen a -> IO a
generate forall a b. (a -> b) -> a -> b
$ forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (NewEpochState era, Tx era, Env era)
genTxAndNewEpoch forall a. Default a => a
def Proof (ConwayEra StandardCrypto)
proof
  TestName -> IO ()
putStrLn (forall a. Show a => a -> TestName
show (forall era. Reflect era => Proof era -> NewEpochState era -> PDoc
psNewEpochState Proof (ConwayEra StandardCrypto)
proof NewEpochState (ConwayEra StandardCrypto)
nes))
  Map (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto)
pools <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era t. Env era -> Term era t -> Typed t
runTerm Env (ConwayEra StandardCrypto)
env forall era.
Era era =>
Term
  era
  (Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era)))
regPools
  Map
  (Credential 'Staking StandardCrypto)
  (KeyHash 'StakePool StandardCrypto)
deleg <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era t. Env era -> Term era t -> Typed t
runTerm Env (ConwayEra StandardCrypto)
env forall era.
Era era =>
Term
  era
  (Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era)))
delegations
  Map (Credential 'Staking StandardCrypto) Coin
stak <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era t. Env era -> Term era t -> Typed t
runTerm Env (ConwayEra StandardCrypto)
env forall era.
Era era =>
Term era (Map (Credential 'Staking (EraCrypto era)) Coin)
incrementalStake
  forall ann. Doc ann -> IO ()
putDoc (forall a. TestName -> Doc a
ppString TestName
"\nPool " forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> PDoc
prettyA Map (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto)
pools)
  forall ann. Doc ann -> IO ()
putDoc (forall a. TestName -> Doc a
ppString TestName
"\nDeleg " forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> PDoc
prettyA Map
  (Credential 'Staking StandardCrypto)
  (KeyHash 'StakePool StandardCrypto)
deleg)
  forall ann. Doc ann -> IO ()
putDoc (forall a. TestName -> Doc a
ppString TestName
"\nStake " forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> PDoc
prettyA Map (Credential 'Staking StandardCrypto) Coin
stak)
  let distr :: PoolDistr StandardCrypto
distr =
        forall c. SnapShot c -> PoolDistr c
calculatePoolDistr
          ( forall c.
Stake c
-> VMap VB VB (Credential 'Staking c) (KeyHash 'StakePool c)
-> VMap VB VB (KeyHash 'StakePool c) (PoolParams c)
-> SnapShot c
SnapShot
              (forall c.
VMap VB VP (Credential 'Staking c) (CompactForm Coin) -> Stake c
Stake (forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map HasCallStack => Coin -> CompactForm Coin
UMap.compactCoinOrError Map (Credential 'Staking StandardCrypto) Coin
stak)))
              (forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap Map
  (Credential 'Staking StandardCrypto)
  (KeyHash 'StakePool StandardCrypto)
deleg)
              (forall (kv :: * -> *) k (vv :: * -> *) v.
(Vector kv k, Vector vv v) =>
Map k v -> VMap kv vv k v
VMap.fromMap Map (KeyHash 'StakePool StandardCrypto) (PoolParams StandardCrypto)
pools)
          )
  forall ann. Doc ann -> IO ()
putDoc (forall a. TestName -> Doc a
ppString TestName
"\nPoolDistr " forall a. Semigroup a => a -> a -> a
<> forall t. PrettyA t => t -> PDoc
prettyA PoolDistr StandardCrypto
distr)
  forall era. Proof era -> Env era -> TestName -> IO ()
goRepl Proof (ConwayEra StandardCrypto)
proof Env (ConwayEra StandardCrypto)
env TestName
""

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

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

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

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

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 = forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ [forall a. Show a => a -> IO ()
print Int
i forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe Int -> IO ()
test (forall a. a -> Maybe a
Just Int
i) | Int
i <- [Int
n .. Int
113], Bool -> Bool
not (forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem 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 (EraCrypto era)) (TxOutF era) ->
  TxBodyField era ->
  [(Text, PDoc)]
pgenTxBodyField :: forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxBodyField era
-> [(Text, PDoc)]
pgenTxBodyField Proof era
proof Map (TxIn (EraCrypto era)) (TxOutF era)
ut TxBodyField era
x = case TxBodyField era
x of
  Inputs Set (TxIn (EraCrypto era))
s -> [(TestName -> Text
pack TestName
"spend inputs", forall era.
Reflect era =>
Map (TxIn (EraCrypto era)) (TxOutF era) -> PDoc
pcUtxoDoc (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map (TxIn (EraCrypto era)) (TxOutF era)
ut Set (TxIn (EraCrypto era))
s))]
  Collateral Set (TxIn (EraCrypto era))
s -> [(TestName -> Text
pack TestName
"coll inputs", forall era.
Reflect era =>
Map (TxIn (EraCrypto era)) (TxOutF era) -> PDoc
pcUtxoDoc (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map (TxIn (EraCrypto era)) (TxOutF era)
ut Set (TxIn (EraCrypto era))
s))]
  RefInputs Set (TxIn (EraCrypto era))
s -> [(TestName -> Text
pack TestName
"ref inputs", forall era.
Reflect era =>
Map (TxIn (EraCrypto era)) (TxOutF era) -> PDoc
pcUtxoDoc (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map (TxIn (EraCrypto era)) (TxOutF era)
ut Set (TxIn (EraCrypto era))
s))]
  TxBodyField era
other -> forall era. Proof era -> TxBodyField era -> [(Text, PDoc)]
pcTxBodyField Proof era
proof TxBodyField era
other

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

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

pgenTx :: Reflect era => Proof era -> Map (TxIn (EraCrypto era)) (TxOutF era) -> Tx era -> PDoc
pgenTx :: forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era) -> Tx era -> PDoc
pgenTx Proof era
proof Map (TxIn (EraCrypto era)) (TxOutF era)
ut Tx era
tx = Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"Tx") [(Text, PDoc)]
pairs
  where
    fields :: [TxField era]
fields = forall era. Proof era -> Tx era -> [TxField era]
abstractTx Proof era
proof Tx era
tx
    pairs :: [(Text, PDoc)]
pairs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxField era
-> [(Text, PDoc)]
pgenTxField Proof era
proof Map (TxIn (EraCrypto era)) (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 (EraCrypto era)) (TxOut era)
ut) Tx era
tx = Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"Tx") [(Text, PDoc)]
pairs
  where
    fields :: [TxField era]
fields = forall era. Proof era -> Tx era -> [TxField era]
abstractTx Proof era
proof Tx era
tx
    pairs :: [(Text, PDoc)]
pairs = forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (forall era.
Reflect era =>
Proof era
-> Map (TxIn (EraCrypto era)) (TxOutF era)
-> TxField era
-> [(Text, PDoc)]
pgenTxField Proof era
proof (forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
proof) Map (TxIn (EraCrypto era)) (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 <-
    forall (f :: * -> *) a. Applicative f => a -> f a
pure forall era. Subst era
emptySubst
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pParamsStage Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
universeStage UnivSize
sizes Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
utxoStage UnivSize
sizes Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
vstateStage Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
pstateStage Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
Proof era -> Subst era -> Gen (Subst era)
dstateStage Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
certsStage UnivSize
sizes Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
ledgerStateStage UnivSize
sizes Proof era
proof
      forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= forall era.
Reflect era =>
UnivSize -> Proof era -> Subst era -> Gen (Subst era)
txBodyStage UnivSize
sizes Proof era
proof
  Env era
env0 <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era. Subst era -> Env era -> Typed (Env era)
substToEnv Subst era
subst forall era. Env era
emptyEnv
  Env era
env1 <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Env era)
adjustFeeInput Env era
env0
  Env era
env2 <- forall t. HasCallStack => Typed t -> t
errorTyped forall a b. (a -> b) -> a -> b
$ forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env1
  LedgerState era
ledgerstate <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped forall a b. (a -> b) -> a -> b
$ forall era x t. Env era -> RootTarget era x t -> Typed t
runTarget Env era
env2 (forall era.
EraGov era =>
Proof era -> RootTarget era (LedgerState era) (LedgerState era)
ledgerStateT Proof era
proof)
  (TxF Proof era
_ Tx era
tx) <- forall (m :: * -> *) t. (HasCallStack, Monad m) => Typed t -> m t
monadTyped (forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env2 forall era. Reflect era => Term era (TxF era)
txterm)

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

main1 :: IO ()
main1 :: IO ()
main1 = forall prop. Testable prop => prop -> IO ()
quickCheck (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 (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 forall a. Default a => a
def Proof (BabbageEra StandardCrypto)
Babbage))

main2 :: IO ()
main2 :: IO ()
main2 = forall prop. Testable prop => prop -> IO ()
quickCheck (forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 (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 forall a. Default a => a
def Proof (ShelleyEra StandardCrypto)
Shelley))

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

demoTest :: TestTree
demoTest :: TestTree
demoTest =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Tests for Tx Stage"
    [ forall a. TestName -> IO a -> TestTree
testIO TestName
"Testing Tx Stage" (ReplMode -> IO ()
demo ReplMode
CI)
    , forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"One Tx Test Babbage" forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 (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 forall a. Default a => a
def Proof (BabbageEra StandardCrypto)
Babbage)
    , forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"One Tx Test Shelley" forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
30 (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 forall a. Default a => a
def Proof (ShelleyEra StandardCrypto)
Shelley)
    ]

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