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

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

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

import Cardano.Crypto.Signing (SigningKey)
import Cardano.Ledger.Address (Addr (..), BootstrapAddress, RewardAccount (..))
import Cardano.Ledger.Alonzo.Scripts (AlonzoScript (..), ExUnits (..), plutusScriptLanguage, toAsIx)
import Cardano.Ledger.Alonzo.Tx (IsValid (..))
import Cardano.Ledger.Alonzo.TxWits (TxDats (..))
import Cardano.Ledger.Alonzo.UTxO (getInputDataHashesTxBody)
import Cardano.Ledger.Api (setMinFeeTxUtxo)
import Cardano.Ledger.Babbage.UTxO (getReferenceScripts)
import Cardano.Ledger.BaseTypes (Network (..), ProtVer (..), strictMaybeToMaybe)
import Cardano.Ledger.Binary.Decoding (mkSized, sizedSize)
import Cardano.Ledger.Binary.Encoding (EncCBOR)
import Cardano.Ledger.CertState (CertState, certDStateL, dsGenDelegsL)
import Cardano.Ledger.Coin (Coin (..), rationalToCoinViaCeiling)
import Cardano.Ledger.Conway.Core
import Cardano.Ledger.Hashes (GenDelegPair (..), GenDelegs (..))
import Cardano.Ledger.Keys (WitVKey (..), asWitness, coerceKeyRole)
import Cardano.Ledger.Keys.Bootstrap (BootstrapWitness)
import Cardano.Ledger.Mary.Value (AssetName, MaryValue (..), MultiAsset (..), PolicyID (..))
import Cardano.Ledger.Plutus.Data (Data (..))
import Cardano.Ledger.Plutus.Language (Language (..))
import Cardano.Ledger.Shelley.AdaPots (consumedTxBody, producedTxBody)
import Cardano.Ledger.Shelley.LedgerState (LedgerState, NewEpochState)
import Cardano.Ledger.Shelley.Rules (LedgerEnv (..))
import Cardano.Ledger.Shelley.TxCert (isInstantaneousRewards)
import Cardano.Ledger.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 (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 a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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 (TxOutF era) ->
  Coin
computeFinalFee :: forall era.
EraUTxO era =>
PParamsF era -> TxF era -> Map TxIn (TxOutF era) -> Coin
computeFinalFee (PParamsF Proof era
_ PParams era
ppV) (TxF Proof era
_ Tx era
txV) Map TxIn (TxOutF era)
ut = Tx era
newtx 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 (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF era)
ut)

integrityHash ::
  Era era1 =>
  Proof era1 ->
  Term era2 (PParamsF era1) ->
  Term era2 (Set Language) ->
  Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits)) ->
  Term era2 (Map DataHash (Data era1)) ->
  Target era2 (Maybe ScriptIntegrityHash)
integrityHash :: forall era1 era2.
Era era1 =>
Proof era1
-> Term era2 (PParamsF era1)
-> Term era2 (Set Language)
-> Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits))
-> Term era2 (Map DataHash (Data era1))
-> Target era2 (Maybe ScriptIntegrityHash)
integrityHash Proof era1
p Term era2 (PParamsF era1)
pp Term era2 (Set Language)
langs Term era2 (Map (PlutusPointerF era1) (Data era1, ExUnits))
rs Term era2 (Map DataHash (Data era1))
ds = forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"integrityHash" PParamsF era1
-> Set Language
-> Map (PlutusPointerF era1) (Data era1, ExUnits)
-> Map DataHash (Data era1)
-> Maybe ScriptIntegrityHash
hashfun 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 (Data era1))
ds
  where
    hashfun :: PParamsF era1
-> Set Language
-> Map (PlutusPointerF era1) (Data era1, ExUnits)
-> Map DataHash (Data era1)
-> Maybe ScriptIntegrityHash
hashfun (PParamsF Proof era1
_ PParams era1
ppp) Set Language
ls Map (PlutusPointerF era1) (Data era1, ExUnits)
r Map DataHash (Data era1)
d =
      let r' :: [(PlutusPurpose AsIx era1, (Data era1, ExUnits))]
r' = [(PlutusPurpose AsIx era1
ptr, (Data era1, ExUnits)
de) | (PlutusPointerF Proof era1
_ PlutusPurpose AsIx era1
ptr, (Data era1, ExUnits)
de) <- 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
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 (Data era) -> TxDats era
TxDats Map DataHash (Data era1)
d)

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

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

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

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

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

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

-- | Get enough GenDeleg KeyHashes to satisfy the quorum constraint.
sufficientGenDelegs :: Map k GenDelegPair -> Set (KeyHash 'Witness)
sufficientGenDelegs :: forall k. Map k GenDelegPair -> Set (KeyHash 'Witness)
sufficientGenDelegs Map k GenDelegPair
gendel =
  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).
HasKeyRole a =>
a r -> a 'Witness
asWitness forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenDelegPair -> KeyHash 'GenesisDelegate
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
gendel))

sufficientTxCert ::
  forall era.
  Reflect era =>
  [TxCertF era] ->
  Map (KeyHash 'Genesis) GenDelegPair ->
  Set (KeyHash 'Witness)
sufficientTxCert :: forall era.
Reflect era =>
[TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair -> Set (KeyHash 'Witness)
sufficientTxCert [TxCertF era]
cs Map (KeyHash 'Genesis) GenDelegPair
gendel = case 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) -> TxCertF era -> Set (KeyHash 'Witness)
accum forall a. Set a
Set.empty [TxCertF era]
cs
    where
      accum :: Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness)
accum Set (KeyHash 'Witness)
ans (TxCertF Proof era
_ TxCert era
cert) =
        if 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)
ans (forall k. Map k GenDelegPair -> Set (KeyHash 'Witness)
sufficientGenDelegs Map (KeyHash 'Genesis) GenDelegPair
gendel)
          else Set (KeyHash 'Witness)
ans
  TxCertWit era
TxCertConwayToConway -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness)
accum forall a. Set a
Set.empty [TxCertF era]
cs
    where
      accum :: Set (KeyHash 'Witness) -> TxCertF era -> Set (KeyHash 'Witness)
accum Set (KeyHash 'Witness)
ans (TxCertF Proof era
_ TxCert era
_) = forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness)
ans (forall k. Map k GenDelegPair -> Set (KeyHash 'Witness)
sufficientGenDelegs Map (KeyHash 'Genesis) GenDelegPair
gendel)

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

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

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

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

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

pcUtxoDoc :: Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc :: forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc Map TxIn (TxOutF era)
m = forall k v. (k -> PDoc) -> (v -> PDoc) -> Map k v -> PDoc
ppMap TxIn -> 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 (TxOutF era)
m

necessaryKeyHashTarget ::
  forall era.
  Reflect era =>
  Term era (TxBodyF era) ->
  Term era (Set (KeyHash 'Witness)) ->
  -- Target era (Set (WitVKey 'Witness ))
  Target era (Set (KeyHash 'Witness))
necessaryKeyHashTarget :: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Target era (Set (KeyHash 'Witness))
necessaryKeyHashTarget Term era (TxBodyF era)
txbodyparam Term era (Set (KeyHash 'Witness))
reqSignersparam =
  ( forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"keywits" forall era.
Reflect era =>
TxBodyF era
-> Map TxIn (TxOutF era)
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness)
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 (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) GenDelegPair)
genDelegs
      --  ^$ keymapUniv
      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (KeyHash 'Witness))
reqSignersparam
  )

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

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

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

makeKeyWitness ::
  forall era.
  Reflect era =>
  TxBodyF era ->
  Set (KeyHash 'Witness) ->
  Set (KeyHash 'Witness) ->
  Map (KeyHash 'Witness) (KeyPair 'Witness) ->
  Map ScriptHash (ScriptF era) ->
  Map (KeyHash 'Genesis) GenDelegPair ->
  Map (KeyHash 'Payment) (Addr, SigningKey) ->
  Set (WitVKey 'Witness)
makeKeyWitness :: forall era.
Reflect era =>
TxBodyF era
-> Set (KeyHash 'Witness)
-> Set (KeyHash 'Witness)
-> Map (KeyHash 'Witness) (KeyPair 'Witness)
-> Map ScriptHash (ScriptF era)
-> Map (KeyHash 'Genesis) GenDelegPair
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set (WitVKey 'Witness)
makeKeyWitness (TxBodyF Proof era
proof TxBody era
txb) Set (KeyHash 'Witness)
necessary Set (KeyHash 'Witness)
sufficient Map (KeyHash 'Witness) (KeyPair 'Witness)
keyUniv Map ScriptHash (ScriptF era)
scripts Map (KeyHash 'Genesis) GenDelegPair
gendel Map (KeyHash 'Payment) (Addr, SigningKey)
byronAdUniv = Set (WitVKey 'Witness)
keywits
  where
    bodyhash :: SafeHash EraIndependentTxBody
    bodyhash :: SafeHash EraIndependentTxBody
bodyhash = forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
txb
    keywits :: Set (WitVKey 'Witness)
keywits = forall a b. (a -> b -> a) -> a -> Set b -> a
Set.foldl' Set (WitVKey 'Witness)
-> KeyHash 'Witness -> Set (WitVKey 'Witness)
accum forall a. Set a
Set.empty (forall a. Ord a => Set a -> Set a -> Set a
Set.union Set (KeyHash 'Witness)
necessary Set (KeyHash 'Witness)
sufficient)
      where
        accum :: Set (WitVKey 'Witness)
-> KeyHash 'Witness -> Set (WitVKey 'Witness)
accum Set (WitVKey 'Witness)
ans KeyHash 'Witness
hash = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'Witness
hash Map (KeyHash 'Witness) (KeyPair 'Witness)
keyUniv of
          Just KeyPair 'Witness
keypair -> forall a. Ord a => a -> Set a -> Set a
Set.insert (forall (kr :: KeyRole).
SafeHash EraIndependentTxBody -> KeyPair kr -> WitVKey 'Witness
mkWitnessVKey SafeHash EraIndependentTxBody
bodyhash KeyPair 'Witness
keypair) Set (WitVKey 'Witness)
ans
          Maybe (KeyPair 'Witness)
Nothing -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (forall (a :: KeyRole -> *) (r :: KeyRole) (r' :: KeyRole).
HasKeyRole a =>
a r -> a r'
coerceKeyRole KeyHash 'Witness
hash) Map (KeyHash 'Payment) (Addr, SigningKey)
byronAdUniv of
            Just (AddrBootstrap BootstrapAddress
_, SigningKey
_) -> Set (WitVKey 'Witness)
ans -- Bootstrap witnesses are handled in bootWitsT, so we can ignore them here.
            Maybe (Addr, SigningKey)
_ ->
              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
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
hash Set (KeyHash 'Witness)
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
hash Set (KeyHash 'Witness)
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 ScriptHash -> 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 (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). KeyHash discriminator -> PDoc
pcKeyHash GenDelegPair -> PDoc
pcGenDelegPair Map (KeyHash 'Genesis) GenDelegPair
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 a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era (KeyHash 'Payment)
PayHashR (forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR forall era. Era era => Rep era Addr
AddrR forall era. Rep era SigningKey
SigningKeyR)) Map (KeyHash 'Payment) (Addr, 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
ps)) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript AlonzoEra
ps) Set Language
ans
    accum Set Language
ans (ScriptF Proof era
Babbage (PlutusScript PlutusScript BabbageEra
ps)) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript BabbageEra
ps) Set Language
ans
    accum Set Language
ans (ScriptF Proof era
Conway (PlutusScript PlutusScript ConwayEra
ps)) = forall a. Ord a => a -> Set a -> Set a
Set.insert (forall era. AlonzoEraScript era => PlutusScript era -> Language
plutusScriptLanguage PlutusScript ConwayEra
ps) Set Language
ans
    accum Set Language
ans ScriptF era
_ = Set Language
ans

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

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

getUtxoCoinT ::
  Reflect era =>
  Term era TxIn ->
  Term era (Map TxIn (TxOutF era)) ->
  Target era Coin
getUtxoCoinT :: forall era.
Reflect era =>
Term era TxIn
-> Term era (Map TxIn (TxOutF era)) -> Target era Coin
getUtxoCoinT Term era TxIn
feeinput Term era (Map TxIn (TxOutF era))
spending = forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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
feeinput forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (TxOutF era))
spending
  where
    getUtxoCoin :: k -> Map k (TxOutF era) -> Coin
getUtxoCoin k
input Map k (TxOutF era)
mp = case 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.
  Proof era ->
  Value era ->
  Value era ->
  Map ScriptHash (Map AssetName Integer)
minusMultiValue :: forall era.
Proof era
-> Value era -> Value era -> Map ScriptHash (Map AssetName Integer)
minusMultiValue Proof era
p Value era
v1 Value era
v2 = case 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 (Map AssetName Integer)
m) -> forall k2 k1 a. Ord k2 => (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeys (\(PolicyID ScriptHash
x) -> ScriptHash
x) Map PolicyID (Map AssetName Integer)
m
  ValueWit era
ValueShelleyToAllegra -> 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 (Map AssetName Integer))
mint
          forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"sumAssets" (\[TxOutF era]
out Map TxIn (TxOutF era)
spend -> forall era.
Proof era
-> Value era -> Value era -> Map ScriptHash (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 (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 (TxOutF era))
spending
               )
       , forall era. Era era => Term era (Maybe Network)
networkID forall era t r. Term era t -> RootTarget era r 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)
inputs
       , forall a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. a -> Either a b
Left forall era. Era era => Term era TxIn
feeTxIn) forall era. Era era => Term era (Set TxIn)
inputs
       , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset forall era. Era era => Term era (Set TxIn)
inputs (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p))
       , -- collateral
         forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint forall era. Era era => Term era (Set TxIn)
inputs forall era. Era era => Term era (Set TxIn)
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)
collateral
       , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset forall era. Era era => Term era (Set TxIn)
collateral (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map TxIn (TxOutF era))
colUtxo)
       , --       , Member (Left colInput) collateral
         Term era (Map TxIn (TxOutF era))
colRestriction forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict forall era. Era era => Term era (Set TxIn)
collateral Term era (Map TxIn (TxOutF era))
colUtxo
       , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> 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 x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL Term era (Map TxIn (TxOutF era))
colRestriction]
       , Term era Coin
tempTotalCol forall a era. Eq a => Term era a -> Term era a -> 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))
prewithdrawal
       , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset Term era (Set (Credential 'Staking))
prewithdrawal (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom Term era (Map (Credential 'Staking) Coin)
nonZeroRewards)
       , if Bool
usGenerateWithdrawals
          then
            forall era. Era era => Term era (Map RewardAccount Coin)
withdrawals
              forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr
                      TestName
"mkRwrdAcnt"
                      ( \Set (Credential 'Staking)
s Map (Credential 'Staking) Coin
r ->
                          forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                            ( forall a b. (a -> b) -> [a] -> [b]
map
                                (\Credential 'Staking
x -> (Network -> Credential 'Staking -> RewardAccount
RewardAccount Network
Testnet Credential 'Staking
x, Map (Credential 'Staking) Coin
r forall k a. Ord k => Map k a -> k -> a
Map.! Credential 'Staking
x))
                                (forall a. Set a -> [a]
Set.toList Set (Credential 'Staking)
s)
                            )
                      )
                      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set (Credential 'Staking))
prewithdrawal
                      forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Map (Credential 'Staking) 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 Coin)
withdrawals
       , Term era (Map (Credential 'Staking) Coin)
nonZeroRewards forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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) 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)
refInputs
       , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset forall era. Era era => Term era (Set TxIn)
refInputs (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom (forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p))
       , forall a era. Ord a => Term era a -> Term era (Set a) -> Pred era
NotMember forall era. Era era => Term era TxIn
feeTxIn forall era. Era era => Term era (Set TxIn)
refInputs
       , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Disjoint forall era. Era era => Term era (Set TxIn)
refInputs forall era. Era era => Term era (Set TxIn)
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))
reqSignerHashes
       , forall a era.
Ord a =>
Term era (Set a) -> Term era (Set a) -> Pred era
Subset forall era. Era era => Term era (Set (KeyHash 'Witness))
reqSignerHashes (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Era era =>
Term era (Map (KeyHash 'Witness) (KeyPair 'Witness))
keymapUniv)
       , forall era. Era era => Term era SlotNo
ttl forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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 (TxOutF era))
spending forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict forall era. Era era => Term era (Set TxIn)
inputs (forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo Proof era
p)
       , forall era c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> Pred era
SumsTo
          (forall a b. b -> Either a b
Right (Integer -> Coin
Coin Integer
1))
          Term era Coin
balanceCoin
          OrdCond
EQL
          [forall x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> Sum era c
ProjMap forall era. Rep era Coin
CoinR forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL Term era (Map TxIn (TxOutF era))
spending, forall c era a. Adds c => Term era (Map a c) -> Sum era c
SumMap forall era. Era era => Term era (Map RewardAccount 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 r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"certsRefunds" forall {era}.
EraTxCert era =>
PParamsF era
-> Map (Credential 'Staking) Coin
-> Map (Credential 'DRepRole) 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) 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) 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 r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"certsDeposits" forall {era} {a}.
EraTxCert era =>
PParamsF era -> Map (KeyHash 'StakePool) 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) PoolParams)
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 r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall era.
EraUTxO era =>
Proof era
-> Target
     era (TxBodyF era -> Map TxIn (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 (TxOutF era))
utxo Proof era
p)
       , forall era. Era era => Term era IsValid
txisvalid forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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 r era t.
(Era era, Typeable r) =>
Term era (Maybe t) -> RootTarget era r t -> [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 TxAuxDataHash)
adHash forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"hashMaybe" (forall era. Reflect era => TxAuxDataF era -> TxAuxDataHash
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 ScriptIntegrityHash
randomWppHash
       , Term era (Maybe ScriptIntegrityHash)
tempWppHash forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era t. Term era t -> Target era (Maybe t)
justTarget Term era ScriptIntegrityHash
randomWppHash
       , Term era Coin
tempTxFee forall era t r. Term era t -> RootTarget era r 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 r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget Term era Coin
tempTxFee Term era (Maybe ScriptIntegrityHash)
tempWppHash (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 r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> Target era (TxF era)
txTarget Term era (TxBodyF era)
tempTxBody Term era (Set BootstrapWitness)
tempBootWits Term era (Set (WitVKey 'Witness))
tempKeyWits
       , -- Compute the real fee, and then recompute the TxBody and the Tx
         forall era. Era era => Term era Coin
txfee forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"finalFee" forall era.
EraUTxO era =>
PParamsF era -> TxF era -> Map TxIn (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 (TxOutF era))
utxo Proof era
p)
       , --  , txbodyterm :<-: txbodyTarget txfee wppHash totalCol
         --  , txterm :<-: txTarget txbodyterm bootWits keyWits
         forall a b t1 era.
Ord a =>
Lens' b t1
-> Rep era t1 -> Term era (Map a b) -> Term era (Map a t1)
ProjM Lens' DRepState Coin
drepDepositL forall era. Rep era Coin
CoinR forall era.
Era era =>
Term era (Map (Credential 'DRepRole) DRepState)
currentDRepState forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era (Map (Credential 'DRepRole) 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 (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 ScriptIntegrityHash)
wppHash
        , forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict (forall b t era. Lens' b t -> Rep era t -> Term era b -> Term era t
Proj forall era.
(ScriptsNeeded era ~ ShelleyScriptsNeeded era) =>
Lens' (ScriptsNeededF era) (Set ScriptHash)
smNeededL (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era ScriptHash
ScriptHashR) forall era. Reflect era => Term era (ScriptsNeededF era)
scriptsNeeded) (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits
        , forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems (forall a b t1 era.
Ord a =>
Lens' b t1
-> Rep era t1 -> Term era (Map a b) -> Term era (Map a t1)
ProjM forall a b. Lens' (a, b) a
fstL forall era. Rep era IsValid
IsValidR (forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict (forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits) forall era.
Reflect era =>
Term era (Map ScriptHash (IsValid, ScriptF era))
plutusUniv)) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era [IsValid]
valids
        , Term era (Set BootstrapWitness)
tempBootWits forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"boots" (forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (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) (Addr, SigningKey))
byronAddrUniv)
        , Term era (Set (KeyHash 'Witness))
necessaryHashes forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Target era (Set (KeyHash 'Witness))
necessaryKeyHashTarget @era Term era (TxBodyF era)
tempTxBody (forall era t. Rep era t -> t -> Term era t
Lit (forall a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) forall a. Set a
Set.empty)
        , Term era (Set (KeyHash 'Witness))
sufficientHashes
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"sufficient" (forall era.
Reflect era =>
Proof era
-> Map ScriptHash (ScriptF era)
-> [TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
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 (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) GenDelegPair)
genDelegs)
        , Term era (Set (WitVKey 'Witness))
tempKeyWits
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget Term era (TxBodyF era)
tempTxBody Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
sufficientHashes forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv
        , forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"boots" (forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (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) (Addr, SigningKey))
byronAddrUniv)
        , forall era. Reflect era => Term era (Set (WitVKey 'Witness))
keyWits
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
sufficientHashes forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv
        , forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget forall era. Era era => Term era Coin
txfee Term era (Maybe ScriptIntegrityHash)
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 r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> Target era (TxF era)
txTarget forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits forall era. Reflect era => Term era (Set (WitVKey 'Witness))
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 b t era. Lens' b t -> Rep era t -> Term era b -> Term era t
Proj forall era.
(ScriptsNeeded era ~ AlonzoScriptsNeeded era) =>
Lens' (ScriptsNeededF era) [(PlutusPurposeF era, ScriptHash)]
acNeededL (forall era a. Rep era a -> Rep era [a]
ListR (forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR (forall era. Era era => Proof era -> Rep era (PlutusPurposeF era)
ScriptPurposeR Proof era
p) forall era. Era era => Rep era ScriptHash
ScriptHashR)) forall era. Reflect era => Term era (ScriptsNeededF era)
scriptsNeeded forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: Term era [(PlutusPurposeF era, ScriptHash)]
acNeeded
        , -- Hashes of scripts that will be run. Not all of these will be in the 'scriptWits'
          Term era (Set ScriptHash)
neededHashSet forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"toSet" (\[(PlutusPurposeF era, ScriptHash)]
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)]
x)) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [(PlutusPurposeF era, ScriptHash)]
acNeeded)
        , -- Only the refAdjusted scripts need to be in the 'scriptWits' but if the refscripts that are
          -- excluded from 'scriptWits' are Timelock scripts, a sufficient set keys must be added to
          -- the sufficient key hashes.
          Term era (Set ScriptHash)
refAdjusted
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"adjust" (forall era.
Proof era
-> Set TxIn
-> Set TxIn
-> Map TxIn (TxOutF era)
-> Set ScriptHash
-> Set ScriptHash
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)
inputs forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era. Era era => Term era (Set TxIn)
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 (TxOutF era))
utxo Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Set ScriptHash)
neededHashSet)
        , -- , scriptWits :=: Restrict refAdjusted (allScriptUniv p)
          forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set ScriptHash)
refAdjusted (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits
        , forall a b era. (Ord a, Eq b) => Term era (Map a b) -> Term era [b]
Elems (forall a b t1 era.
Ord a =>
Lens' b t1
-> Rep era t1 -> Term era (Map a b) -> Term era (Map a t1)
ProjM forall a b. Lens' (a, b) a
fstL forall era. Rep era IsValid
IsValidR (forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set ScriptHash)
neededHashSet forall era.
Reflect era =>
Term era (Map ScriptHash (IsValid, ScriptF era))
plutusUniv)) forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Era era => Term era [IsValid]
valids
        , Term era (Set (PlutusPointerF era))
rdmrPtrs forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall era any.
AlonzoEraScript era =>
Target
  era
  ([(PlutusPurposeF era, ScriptHash)]
   -> Map ScriptHash any -> Set (PlutusPointerF era))
rdmrPtrsT forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era [(PlutusPurposeF era, ScriptHash)]
acNeeded forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ forall era.
Reflect era =>
Term era (Map ScriptHash (IsValid, ScriptF era))
plutusUniv)
        , Term era (Set (PlutusPointerF era))
rdmrPtrs forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall a era b. Ord a => Term era (Map a b) -> Term era (Set a)
Dom forall era.
Reflect era =>
Term era (Map (PlutusPointerF era) (Data era, ExUnits))
redeemers
        , forall era r.
RootTarget era r Bool -> Pred era -> Pred era -> Pred era
If
            (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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 a b. Term era a -> 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 c.
(Era era, Adds c) =>
Direct c -> Term era c -> OrdCond -> [Sum era c] -> 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 x c a era.
Adds c =>
Rep era c -> Lens' x c -> Term era (Map a x) -> 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)
plutusDataHashes
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"plutusDataHashes" forall era.
(AlonzoEraTxOut era, EraTxBody era, AlonzoEraScript era) =>
Map TxIn (TxOutF era)
-> TxBodyF era -> Map ScriptHash (ScriptF era) -> Set DataHash
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 (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 (ScriptF era))
allScriptUniv Proof era
p
                 )
        , forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set DataHash)
plutusDataHashes forall era. Era era => Term era (Map DataHash (Data era))
dataUniv forall a era. Eq a => Term era a -> Term era a -> Pred era
:=: forall era. Reflect era => Term era (Map DataHash (Data era))
dataWits
        , Term era (Set BootstrapWitness)
tempBootWits forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"boots" (forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (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) (Addr, SigningKey))
byronAddrUniv)
        , Term era (Set (KeyHash 'Witness))
necessaryHashes forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Target era (Set (KeyHash 'Witness))
necessaryKeyHashTarget @era Term era (TxBodyF era)
tempTxBody forall era. Era era => Term era (Set (KeyHash 'Witness))
reqSignerHashes
        , Term era (Set (KeyHash 'Witness))
sufficientHashes
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"sufficient" (forall era.
Reflect era =>
Proof era
-> Map ScriptHash (ScriptF era)
-> [TxCertF era]
-> Map (KeyHash 'Genesis) GenDelegPair
-> Set (KeyHash 'Witness)
sufficientKeyHashes Proof era
p)
                    forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ (forall a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set ScriptHash)
neededHashSet (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (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) GenDelegPair)
genDelegs
                 )
        , Term era (Set (WitVKey 'Witness))
tempKeyWits
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget Term era (TxBodyF era)
tempTxBody Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
sufficientHashes forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv
        , forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"boots" (forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era)
-> TxBodyF era
-> Map (KeyHash 'Payment) (Addr, SigningKey)
-> Set BootstrapWitness
bootWitsT Proof era
p) forall era a t. Target era (a -> t) -> Term era a -> Target era t
^$ Term era (Map TxIn (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) (Addr, SigningKey))
byronAddrUniv)
        , forall era. Reflect era => Term era (Set (WitVKey 'Witness))
keyWits
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set (KeyHash 'Witness))
-> Term era (Set (KeyHash 'Witness))
-> Term era (Map ScriptHash (ScriptF era))
-> Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
-> Target era (Set (WitVKey 'Witness))
makeKeyWitnessTarget forall era. Reflect era => Term era (TxBodyF era)
txbodyterm Term era (Set (KeyHash 'Witness))
necessaryHashes Term era (Set (KeyHash 'Witness))
sufficientHashes forall era. Reflect era => Term era (Map ScriptHash (ScriptF era))
scriptWits forall era.
Era era =>
Term era (Map (KeyHash 'Payment) (Addr, SigningKey))
byronAddrUniv
        , -- 'langs' is not computed from the 'scriptWits' because that does not include needed
          -- scripts that are reference scripts, So get the scripts from the neededHashSet
          Term era (Set Language)
langs forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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 a era b.
Ord a =>
Term era (Set a) -> Term era (Map a b) -> Term era (Map a b)
Restrict Term era (Set ScriptHash)
neededHashSet (forall era.
Era era =>
Proof era -> Term era (Map ScriptHash (ScriptF era))
allScriptUniv Proof era
p)))
        , forall era. Era era => Term era (Maybe ScriptIntegrityHash)
wppHash forall era t r. Term era t -> RootTarget era r 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 (Data era1))
-> Target era2 (Maybe ScriptIntegrityHash)
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 (Data era))
dataWits
        , forall era. Era era => Term era Coin
owed
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: ( forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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 r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"extraCol" (\(Coin Integer
suminputs) (Coin Integer
owe) -> (Integer -> Coin
Coin (Integer
owe 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 r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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 a era.
Ord a =>
Direct (Term era a) -> Term era (Set a) -> Pred era
Member (forall a b. b -> Either a b
Right forall era. Era era => Term era Addr
colRetAddr) forall era. Era era => Term era (Set Addr)
addrUniv
        , -- This ( collateralReturn) depends on the Coin in the TxOut being (Coin 1).
          -- The computation of 'owed' and 'extraCol" should ensure this.
          forall era. Era era => Proof era -> Term era (TxOutF era)
collateralReturn Proof era
p
            forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> b)
Constr TestName
"colReturn" (\Addr
ad -> forall era. Proof era -> TxOut era -> TxOutF era
TxOutF Proof era
p (forall era.
(EraTxOut era, HasCallStack) =>
Addr -> Value era -> TxOut era
mkBasicTxOut Addr
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
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 r. Term era t -> RootTarget era r t -> Pred era
:<-: (forall a b era.
TestName -> (a -> b) -> RootTarget era Void (a -> 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 r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era Coin
-> Term era (Maybe ScriptIntegrityHash)
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget forall era. Era era => Term era Coin
txfee forall era. Era era => Term era (Maybe ScriptIntegrityHash)
wppHash forall era. Era era => Term era Coin
totalCol
        , forall era. Reflect era => Term era (TxF era)
txterm forall era t r. Term era t -> RootTarget era r t -> Pred era
:<-: forall era.
Reflect era =>
Term era (TxBodyF era)
-> Term era (Set BootstrapWitness)
-> Term era (Set (WitVKey 'Witness))
-> Target era (TxF era)
txTarget forall era. Reflect era => Term era (TxBodyF era)
txbodyterm forall era. Reflect era => Term era (Set BootstrapWitness)
bootWits forall era. Reflect era => Term era (Set (WitVKey 'Witness))
keyWits
        ]
  where
    spending :: Term era (Map TxIn (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 a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era TxIn
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 (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 a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era TxIn
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 (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 a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era TxIn
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) Coin)
nonZeroRewards = forall era t. Era era => TestName -> Rep era t -> Term era t
var TestName
"nonZeroRewards" (forall a era b.
Ord a =>
Rep era a -> Rep era b -> Rep era (Map a b)
MapR forall era. Era era => Rep era (Credential 'Staking)
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) Coin
-> Map (Credential 'DRepRole) Coin
-> [TxCertF era]
-> Coin
certsRefunds (PParamsF Proof era
_ PParams era
pp) Map (Credential 'Staking) Coin
stakingDepositsx Map (Credential 'DRepRole) Coin
drepDepositsx [TxCertF era]
certsx =
      forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (Credential 'Staking -> Maybe Coin)
-> (Credential 'DRepRole -> 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) Coin
stakingDepositsx)
        (forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map (Credential 'DRepRole) 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) a -> [TxCertF era] -> Coin
certsDeposits (PParamsF Proof era
_ PParams era
pp) Map (KeyHash 'StakePool) a
regpools [TxCertF era]
certsx = Integer -> Coin
Coin (-Integer
n)
      where
        Coin Integer
n = forall era (f :: * -> *).
(EraTxCert era, Foldable f) =>
PParams era
-> (KeyHash 'StakePool -> Bool) -> f (TxCert era) -> Coin
getTotalDepositsTxCerts PParams era
pp (forall k a. Ord k => k -> Map k a -> Bool
`Map.member` Map (KeyHash 'StakePool) 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)]
    acNeeded :: Term era [(PlutusPurposeF era, ScriptHash)]
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 a. Rep era a -> Rep era [a]
ListR (forall era a b. Rep era a -> Rep era b -> Rep era (a, b)
PairR (forall era. Era era => Proof era -> Rep era (PlutusPurposeF era)
ScriptPurposeR Proof era
p) forall era. Era era => Rep era ScriptHash
ScriptHashR)) forall era s t. Access era s t
No
    neededHashSet :: Term era (Set ScriptHash)
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era ScriptHash
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 a era. Ord a => Rep era a -> Rep era (Set a)
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)
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era DataHash
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 ScriptIntegrityHash)
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 t1. Rep era t1 -> Rep era (Maybe t1)
MaybeR forall era. Era era => Rep era ScriptIntegrityHash
ScriptIntegrityHashR) forall era s t. Access era s t
No
    randomWppHash :: Term era ScriptIntegrityHash
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 ScriptIntegrityHash
ScriptIntegrityHashR forall era s t. Access era s t
No
    tempBootWits :: Term era (Set BootstrapWitness)
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR (forall era. Era era => Rep era BootstrapWitness
BootstrapWitnessR @era)) forall era s t. Access era s t
No
    tempKeyWits :: Term era (Set (WitVKey 'Witness))
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR (forall era. Era era => Proof era -> Rep era (WitVKey 'Witness)
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 a era. Ord a => Rep era a -> Rep era (Set a)
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))
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (Credential 'Staking)
CredR) forall era s t. Access era s t
No
    refAdjusted :: Term era (Set ScriptHash)
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era ScriptHash
ScriptHashR) forall era s t. Access era s t
No
    necessaryHashes :: Term era (Set (KeyHash 'Witness))
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Witness)
WitHashR) forall era s t. Access era s t
No
    sufficientHashes :: Term era (Set (KeyHash 'Witness))
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 a era. Ord a => Rep era a -> Rep era (Set a)
SetR forall era. Era era => Rep era (KeyHash 'Witness)
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 (TxOutF era))
utxo forall era. Reflect era => Proof era
reify of
  u :: Term era (Map TxIn (TxOutF era))
u@(Var V era (Map TxIn (TxOutF era))
utxoV) -> do
    TxIn
feeinput <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env forall era. Era era => Term era TxIn
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 (TxOutF era)
utxomap <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map TxIn (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 (TxOutF era))
utxoV (forall k t.
Ord k =>
[(k, Coin)] -> Map k t -> Lens' t Coin -> Map k t
balanceMap [(TxIn
feeinput, Coin
feecoin)] Map TxIn (TxOutF era)
utxomap forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL) Env era
env)
  Term era (Map TxIn (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 (TxOutF era))
other]

-- | Adjust UTxO image of 'collateral' to pay for the collateral fees. Do this by
--   adding 'extraCol' to the TxOuts associated with col inputs
adjustColInput ::
  (HasCallStack, Reflect era) =>
  -- Term era (TxIn ) ->
  -- Term era Coin ->
  -- Term era Coin ->
  Env era ->
  Typed (Gen (Env era))
adjustColInput :: forall era.
(HasCallStack, Reflect era) =>
Env era -> Typed (Gen (Env era))
adjustColInput Env era
env = do
  let utxoterm :: Term era (Map TxIn (TxOutF era))
utxoterm = forall era.
Era era =>
Proof era -> Term era (Map TxIn (TxOutF era))
utxo forall era. Reflect era => Proof era
reify
      utxoV :: V era (Map TxIn (TxOutF era))
utxoV = forall era t. Term era t -> V era t
unVar Term era (Map TxIn (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 (TxOutF era)
utxomap <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env Term era (Map TxIn (TxOutF era))
utxoterm
  Set TxIn
col <- forall era t. Env era -> Term era t -> Typed t
runTerm Env era
env forall era. Era era => Term era (Set TxIn)
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
col) Map TxIn (TxOutF era)
utxomap Coin
extracoin forall era. (HasCallStack, Reflect era) => Lens' (TxOutF era) Coin
outputCoinL of
    Maybe (Map TxIn (TxOutF era))
Nothing -> forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a. a
discard
    Just Map TxIn (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 (TxOutF era))
utxoV Map TxIn (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)
-> Term era Coin
-> Target era (TxBodyF era)
txbodyTarget forall era. Era era => Term era Coin
txfee forall era. Era era => Term era (Maybe ScriptIntegrityHash)
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)
-> Term era (Set (WitVKey 'Witness))
-> 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)
bootWits forall era. Reflect era => Term era (Set (WitVKey 'Witness))
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
proof = Proof ConwayEra
Conway
  (NewEpochState ConwayEra
nes, AlonzoTx ConwayEra
_tx, Env ConwayEra
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
proof
  TestName -> IO ()
putStrLn (forall a. Show a => a -> TestName
show (forall era. Reflect era => Proof era -> NewEpochState era -> PDoc
psNewEpochState Proof ConwayEra
proof NewEpochState ConwayEra
nes))
  Map (KeyHash 'StakePool) PoolParams
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
env forall era.
Era era =>
Term era (Map (KeyHash 'StakePool) PoolParams)
regPools
  Map (Credential 'Staking) (KeyHash 'StakePool)
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
env forall era.
Era era =>
Term era (Map (Credential 'Staking) (KeyHash 'StakePool))
delegations
  Map (Credential 'Staking) 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
env forall era. Era era => Term era (Map (Credential 'Staking) 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) PoolParams
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) (KeyHash 'StakePool)
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) Coin
stak)
  let distr :: PoolDistr
distr =
        SnapShot -> PoolDistr
calculatePoolDistr
          ( Stake
-> VMap VB VB (Credential 'Staking) (KeyHash 'StakePool)
-> VMap VB VB (KeyHash 'StakePool) PoolParams
-> SnapShot
SnapShot
              (VMap VB VP (Credential 'Staking) (CompactForm Coin) -> Stake
Stake (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) 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) (KeyHash 'StakePool)
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) PoolParams
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
distr)
  forall era. Proof era -> Env era -> TestName -> IO ()
goRepl Proof ConwayEra
proof Env ConwayEra
env TestName
""

demoTx :: IO ()
demoTx :: IO ()
demoTx = do
  let proof :: Proof ConwayEra
proof = Proof ConwayEra
Conway
  (LedgerState ConwayEra
ls, AlonzoTx ConwayEra
tx, Env ConwayEra
env) <- 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
proof
  TestName -> IO ()
putStrLn (forall a. Show a => a -> TestName
show (forall era. Proof era -> LedgerState era -> PDoc
pcLedgerState Proof ConwayEra
proof LedgerState ConwayEra
ls))
  TestName -> IO ()
putStrLn (forall a. Show a => a -> TestName
show (forall era. Proof era -> Tx era -> PDoc
pcTx Proof ConwayEra
proof AlonzoTx ConwayEra
tx))
  forall era. Proof era -> Env era -> TestName -> IO ()
goRepl Proof ConwayEra
proof Env ConwayEra
env TestName
""

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

gone :: Gen (IO ())
gone :: Gen (IO ())
gone = do
  TxIx
txIx <- forall a. Arbitrary a => Gen a
arbitrary
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
      sizes :: UnivSize
sizes = forall a. Default a => a
def
  (LedgerState BabbageEra
ledgerstate, AlonzoTx BabbageEra
tx, Env BabbageEra
env) <- forall era.
Reflect era =>
UnivSize -> Proof era -> Gen (LedgerState era, Tx era, Env era)
genTxAndLedger UnivSize
sizes Proof BabbageEra
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
env)
  (PParamsF Proof BabbageEra
_ PParams BabbageEra
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
proof)) Env BabbageEra
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
env forall era. Era era => RootTarget era AccountState AccountState
accountStateT)
  Map TxIn (TxOutF BabbageEra)
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 (TxOutF era))
utxo Proof BabbageEra
proof)) Env BabbageEra
env)
  let lenv :: LedgerEnv BabbageEra
lenv = forall era.
SlotNo
-> Maybe EpochNo
-> TxIx
-> PParams era
-> AccountState
-> Bool
-> LedgerEnv era
LedgerEnv SlotNo
slot forall a. Maybe a
Nothing TxIx
txIx PParams BabbageEra
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
proof (forall sts. (Environment sts, State sts, Signal sts) -> TRC sts
TRC (LedgerEnv BabbageEra
lenv, LedgerState BabbageEra
ledgerstate, AlonzoTx BabbageEra
tx)) of
    Right State (EraRule "LEDGER" BabbageEra)
_ledgerState' -> do
      -- putStrLn (show (pcTx Babbage tx))
      TestName -> IO ()
putStrLn TestName
"SUCCESS"
    Left NonEmpty (PredicateFailure (EraRule "LEDGER" BabbageEra))
errs -> do
      TestName -> IO ()
putStrLn TestName
"FAIL"
      forall a. Show a => a -> IO ()
print forall a b. (a -> b) -> a -> b
$ forall era.
Reflect era =>
Proof era -> Map TxIn (TxOutF era) -> Tx era -> PDoc
pgenTx Proof BabbageEra
proof Map TxIn (TxOutF BabbageEra)
utxo1 AlonzoTx BabbageEra
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))
errs
      forall era. Proof era -> Env era -> TestName -> IO ()
goRepl Proof BabbageEra
Babbage Env BabbageEra
env TestName
""

test :: Maybe Int -> IO ()
test :: Maybe Int -> IO ()
test (Just Int
seed) = 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 (TxOutF era) ->
  TxBodyField era ->
  [(Text, PDoc)]
pgenTxBodyField :: forall era.
Reflect era =>
Proof era
-> Map TxIn (TxOutF era) -> TxBodyField era -> [(Text, PDoc)]
pgenTxBodyField Proof era
proof Map TxIn (TxOutF era)
ut TxBodyField era
x = case TxBodyField era
x of
  Inputs Set TxIn
s -> [(TestName -> Text
pack TestName
"spend inputs", forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map TxIn (TxOutF era)
ut Set TxIn
s))]
  Collateral Set TxIn
s -> [(TestName -> Text
pack TestName
"coll inputs", forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map TxIn (TxOutF era)
ut Set TxIn
s))]
  RefInputs Set TxIn
s -> [(TestName -> Text
pack TestName
"ref inputs", forall era. Reflect era => Map TxIn (TxOutF era) -> PDoc
pcUtxoDoc (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys Map TxIn (TxOutF era)
ut Set TxIn
s))]
  TxBodyField era
other -> forall era. Proof era -> TxBodyField era -> [(Text, PDoc)]
pcTxBodyField Proof era
proof TxBodyField era
other

pgenTxBody ::
  Reflect era => Proof era -> TxBody era -> Map TxIn (TxOutF era) -> PDoc
pgenTxBody :: forall era.
Reflect era =>
Proof era -> TxBody era -> Map TxIn (TxOutF era) -> PDoc
pgenTxBody Proof era
proof TxBody era
txBody Map TxIn (TxOutF era)
ut = Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"TxBody " 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 (TxOutF era) -> TxBodyField era -> [(Text, PDoc)]
pgenTxBodyField Proof era
proof Map TxIn (TxOutF era)
ut) [TxBodyField era]
fields

pgenTxField ::
  forall era.
  Reflect era =>
  Proof era ->
  Map TxIn (TxOutF era) ->
  TxField era ->
  [(Text, PDoc)]
pgenTxField :: forall era.
Reflect era =>
Proof era -> Map TxIn (TxOutF era) -> TxField era -> [(Text, PDoc)]
pgenTxField Proof era
proof Map TxIn (TxOutF era)
ut TxField era
x = case TxField era
x of
  Body TxBody era
b -> [(TestName -> Text
pack TestName
"txbody hash", forall index. SafeHash index -> PDoc
ppSafeHash (forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
b)), (TestName -> Text
pack TestName
"body", forall era.
Reflect era =>
Proof era -> TxBody era -> Map TxIn (TxOutF era) -> PDoc
pgenTxBody Proof era
proof TxBody era
b Map TxIn (TxOutF era)
ut)]
  BodyI [TxBodyField era]
xs -> [(TestName -> Text
pack TestName
"body", Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"TxBody") (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 (TxOutF era) -> TxBodyField era -> [(Text, PDoc)]
pgenTxBodyField Proof era
proof Map TxIn (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 (TxOutF era) -> Tx era -> PDoc
pgenTx :: forall era.
Reflect era =>
Proof era -> Map TxIn (TxOutF era) -> Tx era -> PDoc
pgenTx Proof era
proof Map TxIn (TxOutF era)
ut Tx era
tx = Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"Tx") [(Text, PDoc)]
pairs
  where
    fields :: [TxField era]
fields = 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 (TxOutF era) -> TxField era -> [(Text, PDoc)]
pgenTxField Proof era
proof Map TxIn (TxOutF era)
ut) [TxField era]
fields

pcTxWithUTxO :: Reflect era => Proof era -> UTxO era -> Tx era -> PDoc
pcTxWithUTxO :: forall era. Reflect era => Proof era -> UTxO era -> Tx era -> PDoc
pcTxWithUTxO Proof era
proof (UTxO Map TxIn (TxOut era)
ut) Tx era
tx = Text -> [(Text, PDoc)] -> PDoc
ppRecord (TestName -> Text
pack TestName
"Tx") [(Text, PDoc)]
pairs
  where
    fields :: [TxField era]
fields = 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 (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 (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
-> Maybe EpochNo
-> TxIx
-> PParams era
-> AccountState
-> Bool
-> LedgerEnv era
LedgerEnv SlotNo
slot forall a. Maybe a
Nothing 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
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
Shelley))

demo :: ReplMode -> IO ()
demo :: ReplMode -> IO ()
demo ReplMode
mode = do
  let proof :: Proof BabbageEra
proof = Proof BabbageEra
Babbage
  -- Conway
  -- Alonzo
  -- Mary
  -- Shelley
  let sizes :: UnivSize
sizes = forall a. Default a => a
def
  Subst BabbageEra
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
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
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
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
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
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
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
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
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
proof
      )
  -- rewritten <- snd <$> generate (rewriteGen (1, txBodyPreds sizes proof))
  -- putStrLn (show rewritten)
  (Env BabbageEra
_, 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
proof) Subst BabbageEra
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
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
subst forall era. Env era
emptyEnv
  Env BabbageEra
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
env0
  Env BabbageEra
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
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
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
env2 forall era. Reflect era => Term era (TxF era)
txterm
  -- compute Produced and Consumed
  (TxBodyF Proof BabbageEra
_ TxBody BabbageEra
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
env2)
  CertState BabbageEra
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
env1 forall era.
Era era =>
RootTarget era (CertState era) (CertState era)
certstateT
  (PParamsF Proof BabbageEra
_ PParams BabbageEra
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
proof)) Env BabbageEra
env2)
  Map TxIn (TxOutF BabbageEra)
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 (TxOutF era))
utxo Proof BabbageEra
proof)) Env BabbageEra
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
txb PParams BabbageEra
ppV CertState BabbageEra
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
txb PParams BabbageEra
ppV CertState BabbageEra
certState (forall era. Map TxIn (TxOutF era) -> UTxO era
liftUTxO Map TxIn (TxOutF BabbageEra)
utxoV)))
  forall era. ReplMode -> Proof era -> Env era -> TestName -> IO ()
modeRepl ReplMode
mode Proof BabbageEra
proof Env BabbageEra
env2 TestName
""

demoTest :: TestTree
demoTest :: TestTree
demoTest =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Tests for Tx Stage"
    [ 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
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
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)