{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module Test.Cardano.Ledger.Generic.ApplyTx where

import Cardano.Ledger.Address (RewardAccount (..), Withdrawals (..))
import Cardano.Ledger.Alonzo.Scripts (ExUnits (ExUnits))
import Cardano.Ledger.Alonzo.Tx (AlonzoTx (..), IsValid (..))
import Cardano.Ledger.BaseTypes (ProtVer (..), TxIx, mkTxIxPartial, natVersion)
import Cardano.Ledger.Coin (Coin (..), addDeltaCoin)
import Cardano.Ledger.Core
import Cardano.Ledger.Plutus.Data (Data (..))
import Cardano.Ledger.Plutus.Language (Language (PlutusV1))
import Cardano.Ledger.PoolParams (PoolParams (..))
import Cardano.Ledger.SafeHash (SafeHash, hashAnnotated)
import Cardano.Ledger.Shelley.API (Credential, KeyRole (Staking))
import Cardano.Ledger.Shelley.Rewards (aggregateRewards)
import Cardano.Ledger.Shelley.TxCert (ShelleyDelegCert (..), ShelleyTxCert (..))
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
import Cardano.Ledger.UTxO (UTxO (..))
import Cardano.Ledger.Val (Val ((<+>), (<->)), inject)
import Cardano.Slotting.Slot (EpochNo (..), SlotNo (..))
import Control.Iterate.Exp (dom, (∈))
import Control.Iterate.SetAlgebra (eval)
import Data.Foldable (fold, toList)
import qualified Data.List as List
import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe.Strict (StrictMaybe (..))
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Stack (HasCallStack)
import Lens.Micro
import qualified PlutusLedgerApi.V1 as PV1
import Test.Cardano.Ledger.Core.KeyPair (mkWitnessVKey)
import Test.Cardano.Ledger.Examples.STSTestUtils (
  initUTxO,
  mkGenesisTxIn,
  mkTxDats,
  someAddr,
  someKeys,
 )
import Test.Cardano.Ledger.Generic.Fields (
  PParamsField (..),
  TxBodyField (..),
  TxField (..),
  TxOutField (..),
  WitnessesField (..),
  abstractTx,
  abstractTxBody,
 )
import Test.Cardano.Ledger.Generic.Functions (
  createRUpdNonPulsing',
  getBody,
  getOutputs,
  txInBalance,
 )
import Test.Cardano.Ledger.Generic.GenState (PlutusPurposeTag (..), mkRedeemersFromTags)
import Test.Cardano.Ledger.Generic.ModelState (
  Model,
  ModelNewEpochState (..),
  mNewEpochStateZero,
  pcModelNewEpochState,
 )
import Test.Cardano.Ledger.Generic.PrettyCore (pcCredential, pcTx)
import Test.Cardano.Ledger.Generic.Proof hiding (lift)
import Test.Cardano.Ledger.Generic.Scriptic (Scriptic (never))
import Test.Cardano.Ledger.Generic.Updaters (
  newPParams,
  newScriptIntegrityHash,
  newTx,
  newTxBody,
  newTxOut,
 )
import Test.Cardano.Ledger.Plutus (zeroTestingCostModels)
import Test.Cardano.Ledger.Shelley.Rewards (RewardUpdateOld (deltaFOld), rsOld)
import Test.Cardano.Ledger.Shelley.Utils (epochFromSlotNo)

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

defaultPPs :: [PParamsField era]
defaultPPs :: forall era. [PParamsField era]
defaultPPs =
  [ forall era. CostModels -> PParamsField era
Costmdls forall a b. (a -> b) -> a -> b
$ HasCallStack => [Language] -> CostModels
zeroTestingCostModels [Language
PlutusV1]
  , forall era. Natural -> PParamsField era
MaxValSize Natural
1000000000
  , forall era. ExUnits -> PParamsField era
MaxTxExUnits forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> ExUnits
ExUnits Natural
1000000 Natural
1000000
  , forall era. ExUnits -> PParamsField era
MaxBlockExUnits forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> ExUnits
ExUnits Natural
1000000 Natural
1000000
  , forall era. ProtVer -> PParamsField era
ProtocolVersion forall a b. (a -> b) -> a -> b
$ Version -> Natural -> ProtVer
ProtVer (forall (v :: Natural).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @5) Natural
0
  , forall era. Coin -> PParamsField era
KeyDeposit (Integer -> Coin
Coin Integer
2)
  , forall era. Coin -> PParamsField era
PoolDeposit (Integer -> Coin
Coin Integer
5)
  , forall era. Natural -> PParamsField era
CollateralPercentage Natural
100
  ]

pparams :: EraPParams era => Proof era -> PParams era
pparams :: forall era. EraPParams era => Proof era -> PParams era
pparams Proof era
pf = forall era.
EraPParams era =>
Proof era -> [PParamsField era] -> PParams era
newPParams Proof era
pf forall era. [PParamsField era]
defaultPPs

hasValid :: [TxField era] -> Maybe Bool
hasValid :: forall era. [TxField era] -> Maybe Bool
hasValid [] = forall a. Maybe a
Nothing
hasValid (Valid (IsValid Bool
b) : [TxField era]
_) = forall a. a -> Maybe a
Just Bool
b
hasValid (TxField era
_ : [TxField era]
fs) = forall era. [TxField era] -> Maybe Bool
hasValid [TxField era]
fs

applyTx :: Reflect era => Proof era -> Int -> SlotNo -> Model era -> Tx era -> Model era
applyTx :: forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> Model era -> Tx era -> Model era
applyTx Proof era
proof Int
count SlotNo
slot Model era
model Tx era
tx = Model era
ans
  where
    transactionEpoch :: EpochNo
transactionEpoch = SlotNo -> EpochNo
epochFromSlotNo SlotNo
slot
    modelEpoch :: EpochNo
modelEpoch = forall era. ModelNewEpochState era -> EpochNo
mEL Model era
model
    epochAccurateModel :: Model era
epochAccurateModel = forall era.
Proof era -> EpochNo -> EpochNo -> Model era -> Model era
epochBoundary Proof era
proof EpochNo
transactionEpoch EpochNo
modelEpoch Model era
model
    txbody :: TxBody era
txbody = forall era. EraTx era => Proof era -> Tx era -> TxBody era
getBody Proof era
proof Tx era
tx
    outputs :: StrictSeq (TxOut era)
outputs = forall era.
EraTxBody era =>
Proof era -> TxBody era -> StrictSeq (TxOut era)
getOutputs Proof era
proof TxBody era
txbody
    fields :: [TxField era]
fields = forall era. Proof era -> Tx era -> [TxField era]
abstractTx Proof era
proof Tx era
tx
    nextTxIx :: TxIx
nextTxIx = HasCallStack => Integer -> TxIx
mkTxIxPartial (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (t :: * -> *) a. Foldable t => t a -> Int
length StrictSeq (TxOut era)
outputs)) -- When IsValid is false, ColRet will get this TxIx
    ans :: Model era
ans = case forall era. [TxField era] -> Maybe Bool
hasValid [TxField era]
fields of
      Maybe Bool
Nothing -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxField era -> Model era
applyTxSimple Proof era
proof Int
count) Model era
epochAccurateModel [TxField era]
fields
      Just Bool
True -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxField era -> Model era
applyTxSimple Proof era
proof Int
count) Model era
epochAccurateModel [TxField era]
fields
      Just Bool
False -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall era.
Reflect era =>
Proof era -> Int -> TxIx -> Model era -> TxField era -> Model era
applyTxFail Proof era
proof Int
count TxIx
nextTxIx) Model era
epochAccurateModel [TxField era]
fields

epochBoundary :: forall era. Proof era -> EpochNo -> EpochNo -> Model era -> Model era
epochBoundary :: forall era.
Proof era -> EpochNo -> EpochNo -> Model era -> Model era
epochBoundary Proof era
proof EpochNo
transactionEpoch EpochNo
modelEpoch Model era
model =
  if EpochNo
transactionEpoch forall a. Ord a => a -> a -> Bool
> EpochNo
modelEpoch
    then
      forall era.
RewardUpdateOld (EraCrypto era) -> Model era -> Model era
applyRUpd RewardUpdateOld (EraCrypto era)
ru forall a b. (a -> b) -> a -> b
$
        Model era
model
          { mEL :: EpochNo
mEL = EpochNo
transactionEpoch
          }
    else Model era
model
  where
    ru :: RewardUpdateOld (EraCrypto era)
ru = forall era.
Proof era -> Model era -> RewardUpdateOld (EraCrypto era)
createRUpdNonPulsing' Proof era
proof Model era
model

applyTxSimple :: Reflect era => Proof era -> Int -> Model era -> TxField era -> Model era
applyTxSimple :: forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxField era -> Model era
applyTxSimple Proof era
proof Int
count Model era
model TxField era
field = case TxField era
field of
  Body TxBody era
body1 -> forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxBody era -> Model era
applyTxBody Proof era
proof Int
count Model era
model TxBody era
body1
  BodyI [TxBodyField era]
fs -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxBodyField era -> Model era
applyField Proof era
proof Int
count) Model era
model [TxBodyField era]
fs
  TxWits TxWits era
_ -> Model era
model
  WitnessesI [WitnessesField era]
_ -> Model era
model
  AuxData StrictMaybe (TxAuxData era)
_ -> Model era
model
  Valid IsValid
_ -> Model era
model

applyTxBody :: Reflect era => Proof era -> Int -> Model era -> TxBody era -> Model era
applyTxBody :: forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxBody era -> Model era
applyTxBody Proof era
proof Int
count Model era
model TxBody era
tx = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxBodyField era -> Model era
applyField Proof era
proof Int
count) Model era
model (forall era. Proof era -> TxBody era -> [TxBodyField era]
abstractTxBody Proof era
proof TxBody era
tx)

applyField :: Reflect era => Proof era -> Int -> Model era -> TxBodyField era -> Model era
applyField :: forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxBodyField era -> Model era
applyField Proof era
proof Int
count Model era
model TxBodyField era
field = case TxBodyField era
field of
  Inputs Set (TxIn (EraCrypto era))
txins -> Model era
model {mUTxO :: Map (TxIn (EraCrypto era)) (TxOut era)
mUTxO = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys (forall era.
ModelNewEpochState era -> Map (TxIn (EraCrypto era)) (TxOut era)
mUTxO Model era
model) Set (TxIn (EraCrypto era))
txins}
  Outputs StrictSeq (TxOut era)
seqo -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
count (forall era.
ModelNewEpochState era -> Map Int (TxId (EraCrypto era))
mIndex Model era
model) of
    Maybe (TxId StandardCrypto)
Nothing -> forall a. HasCallStack => [Char] -> a
error ([Char]
"Output not found phase1: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (forall era.
ModelNewEpochState era -> Map Int (TxId (EraCrypto era))
mIndex Model era
model))
    Just (TxId SafeHash StandardCrypto EraIndependentTxBody
hash) -> Model era
model {mUTxO :: Map (TxIn (EraCrypto era)) (TxOut era)
mUTxO = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map (TxIn (EraCrypto era)) (TxOut era)
newstuff (forall era.
ModelNewEpochState era -> Map (TxIn (EraCrypto era)) (TxOut era)
mUTxO Model era
model)}
      where
        newstuff :: Map (TxIn (EraCrypto era)) (TxOut era)
newstuff = forall era.
SafeHash (EraCrypto era) EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map (TxIn (EraCrypto era)) (TxOut era)
additions SafeHash StandardCrypto EraIndependentTxBody
hash forall a. Bounded a => a
minBound (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxOut era)
seqo)
  Txfee Coin
coin -> Model era
model {mFees :: Coin
mFees = Coin
coin forall t. Val t => t -> t -> t
<+> forall era. ModelNewEpochState era -> Coin
mFees Model era
model}
  Certs StrictSeq (TxCert era)
seqc -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' forall era. Reflect era => Model era -> TxCert era -> Model era
applyCert Model era
model (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxCert era)
seqc)
  Withdrawals' (Withdrawals Map (RewardAcnt (EraCrypto era)) Coin
m) -> forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' (forall era.
Proof era
-> Model era -> RewardAccount (EraCrypto era) -> Coin -> Model era
applyWithdrawals Proof era
proof) Model era
model Map (RewardAcnt (EraCrypto era)) Coin
m
  TxBodyField era
_other -> Model era
model

applyWithdrawals :: Proof era -> Model era -> RewardAccount (EraCrypto era) -> Coin -> Model era
applyWithdrawals :: forall era.
Proof era
-> Model era -> RewardAccount (EraCrypto era) -> Coin -> Model era
applyWithdrawals Proof era
_proof Model era
model (RewardAccount Network
_network Credential 'Staking (EraCrypto era)
cred) Coin
coin =
  Model era
model {mRewards :: Map (Credential 'Staking (EraCrypto era)) Coin
mRewards = forall k a. Ord k => (a -> a) -> k -> Map k a -> Map k a
Map.adjust (forall t. Val t => t -> t -> t
<-> Coin
coin) Credential 'Staking (EraCrypto era)
cred (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mRewards Model era
model)}

applyCert :: forall era. Reflect era => Model era -> TxCert era -> Model era
applyCert :: forall era. Reflect era => Model era -> TxCert era -> Model era
applyCert = case forall era. Reflect era => Proof era
reify @era of
  Proof era
Shelley -> forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Mary -> forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Allegra -> forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Alonzo -> forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Babbage -> forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Conway -> forall a. HasCallStack => [Char] -> a
error [Char]
"applyCert, not yet in Conway"

applyShelleyCert :: forall era. EraPParams era => Model era -> ShelleyTxCert era -> Model era
applyShelleyCert :: forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert Model era
model ShelleyTxCert era
dcert = case ShelleyTxCert era
dcert of
  ShelleyTxCertDelegCert (ShelleyRegCert Credential 'Staking (EraCrypto era)
x) ->
    Model era
model
      { mRewards :: Map (Credential 'Staking (EraCrypto era)) Coin
mRewards = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Credential 'Staking (EraCrypto era)
x (Integer -> Coin
Coin Integer
0) (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mRewards Model era
model)
      , mKeyDeposits :: Map (Credential 'Staking (EraCrypto era)) Coin
mKeyDeposits = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Credential 'Staking (EraCrypto era)
x (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppKeyDepositL) (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mKeyDeposits Model era
model)
      , mDeposited :: Coin
mDeposited = forall era. ModelNewEpochState era -> Coin
mDeposited Model era
model forall t. Val t => t -> t -> t
<+> PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppKeyDepositL
      }
    where
      pp :: PParams era
pp = forall era. ModelNewEpochState era -> PParams era
mPParams Model era
model
  ShelleyTxCertDelegCert (ShelleyUnRegCert Credential 'Staking (EraCrypto era)
x) -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Credential 'Staking (EraCrypto era)
x (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mRewards Model era
model) of
    Maybe Coin
Nothing -> forall a. HasCallStack => [Char] -> a
error ([Char]
"DeRegKey not in rewards: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> [Char]
show (forall (keyrole :: KeyRole) c. Credential keyrole c -> PDoc
pcCredential Credential 'Staking (EraCrypto era)
x))
    Just (Coin Integer
0) ->
      Model era
model
        { mRewards :: Map (Credential 'Staking (EraCrypto era)) Coin
mRewards = forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Credential 'Staking (EraCrypto era)
x (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mRewards Model era
model)
        , mKeyDeposits :: Map (Credential 'Staking (EraCrypto era)) Coin
mKeyDeposits = forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Credential 'Staking (EraCrypto era)
x (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mKeyDeposits Model era
model)
        , mDeposited :: Coin
mDeposited = forall era. ModelNewEpochState era -> Coin
mDeposited Model era
model forall t. Val t => t -> t -> t
<-> Coin
keyDeposit
        }
      where
        keyDeposit :: Coin
keyDeposit = forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault forall a. Monoid a => a
mempty Credential 'Staking (EraCrypto era)
x (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mKeyDeposits Model era
model)
    Just (Coin Integer
_n) -> forall a. HasCallStack => [Char] -> a
error [Char]
"DeRegKey with non-zero balance"
  ShelleyTxCertDelegCert (ShelleyDelegCert Credential 'Staking (EraCrypto era)
cred KeyHash 'StakePool (EraCrypto era)
hash) ->
    Model era
model {mDelegations :: Map
  (Credential 'Staking (EraCrypto era))
  (KeyHash 'StakePool (EraCrypto era))
mDelegations = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Credential 'Staking (EraCrypto era)
cred KeyHash 'StakePool (EraCrypto era)
hash (forall era.
ModelNewEpochState era
-> Map
     (Credential 'Staking (EraCrypto era))
     (KeyHash 'StakePool (EraCrypto era))
mDelegations Model era
model)}
  ShelleyTxCertPool (RegPool PoolParams (EraCrypto era)
poolparams) ->
    Model era
model
      { mPoolParams :: Map
  (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
mPoolParams = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'StakePool (EraCrypto era)
hk PoolParams (EraCrypto era)
poolparams (forall era.
ModelNewEpochState era
-> Map
     (KeyHash 'StakePool (EraCrypto era)) (PoolParams (EraCrypto era))
mPoolParams Model era
model)
      , mDeposited :: Coin
mDeposited =
          if forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash 'StakePool (EraCrypto era)
hk (forall era.
ModelNewEpochState era
-> Map (KeyHash 'StakePool (EraCrypto era)) Coin
mPoolDeposits Model era
model)
            then forall era. ModelNewEpochState era -> Coin
mDeposited Model era
model
            else forall era. ModelNewEpochState era -> Coin
mDeposited Model era
model forall t. Val t => t -> t -> t
<+> PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppPoolDepositL
      , mPoolDeposits :: Map (KeyHash 'StakePool (EraCrypto era)) Coin
mPoolDeposits -- Only add if it isn't already there
        =
          if forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash 'StakePool (EraCrypto era)
hk (forall era.
ModelNewEpochState era
-> Map (KeyHash 'StakePool (EraCrypto era)) Coin
mPoolDeposits Model era
model)
            then forall era.
ModelNewEpochState era
-> Map (KeyHash 'StakePool (EraCrypto era)) Coin
mPoolDeposits Model era
model
            else forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'StakePool (EraCrypto era)
hk (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppPoolDepositL) (forall era.
ModelNewEpochState era
-> Map (KeyHash 'StakePool (EraCrypto era)) Coin
mPoolDeposits Model era
model)
      }
    where
      hk :: KeyHash 'StakePool (EraCrypto era)
hk = forall c. PoolParams c -> KeyHash 'StakePool c
ppId PoolParams (EraCrypto era)
poolparams
      pp :: PParams era
pp = forall era. ModelNewEpochState era -> PParams era
mPParams Model era
model
  ShelleyTxCertPool (RetirePool KeyHash 'StakePool (EraCrypto era)
keyhash EpochNo
epoch) ->
    Model era
model
      { mRetiring :: Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
mRetiring = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'StakePool (EraCrypto era)
keyhash EpochNo
epoch (forall era.
ModelNewEpochState era
-> Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
mRetiring Model era
model)
      , mDeposited :: Coin
mDeposited = forall era. ModelNewEpochState era -> Coin
mDeposited Model era
model forall t. Val t => t -> t -> t
<-> PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) Coin
ppPoolDepositL
      }
    where
      pp :: PParams era
pp = forall era. ModelNewEpochState era -> PParams era
mPParams Model era
model
  ShelleyTxCertGenesisDeleg GenesisDelegCert (EraCrypto era)
_ -> Model era
model
  ShelleyTxCertMir MIRCert (EraCrypto era)
_ -> Model era
model

-- =========================================================
-- What to do if the second phase does not validatate.
-- Process and use Collateral to pay fees

data CollInfo era = CollInfo
  { forall era. CollInfo era -> Coin
ciBal :: Coin -- Balance of all the collateral inputs
  , forall era. CollInfo era -> Coin
ciRet :: Coin -- Coin amount of the collateral return output
  , forall era. CollInfo era -> Set (TxIn (EraCrypto era))
ciDelset :: Set (TxIn (EraCrypto era)) -- The set of inputs to delete from the UTxO
  , forall era. CollInfo era -> Map (TxIn (EraCrypto era)) (TxOut era)
ciAddmap :: Map (TxIn (EraCrypto era)) (TxOut era) -- Things to Add to the UTxO
  }

emptyCollInfo :: CollInfo era
emptyCollInfo :: forall era. CollInfo era
emptyCollInfo = forall era.
Coin
-> Coin
-> Set (TxIn (EraCrypto era))
-> Map (TxIn (EraCrypto era)) (TxOut era)
-> CollInfo era
CollInfo (Integer -> Coin
Coin Integer
0) (Integer -> Coin
Coin Integer
0) forall a. Set a
Set.empty forall k a. Map k a
Map.empty

-- | Collect information about how to process Collateral, in a second phase failure.
collInfo ::
  (Reflect era, HasCallStack) =>
  Int ->
  TxIx ->
  Model era ->
  CollInfo era ->
  TxBodyField era ->
  CollInfo era
collInfo :: forall era.
(Reflect era, HasCallStack) =>
Int
-> TxIx
-> Model era
-> CollInfo era
-> TxBodyField era
-> CollInfo era
collInfo Int
count TxIx
firstTxIx Model era
model CollInfo era
info TxBodyField era
field = case TxBodyField era
field of
  CollateralReturn StrictMaybe (TxOut era)
SNothing -> CollInfo era
info
  CollateralReturn (SJust TxOut era
txout) ->
    case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
count (forall era.
ModelNewEpochState era -> Map Int (TxId (EraCrypto era))
mIndex Model era
model) of
      Maybe (TxId StandardCrypto)
Nothing -> forall a. HasCallStack => [Char] -> a
error ([Char]
"Output not found phase2: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show (Int
count, forall era.
ModelNewEpochState era -> Map Int (TxId (EraCrypto era))
mIndex Model era
model))
      Just (TxId SafeHash StandardCrypto EraIndependentTxBody
hash) ->
        CollInfo era
info
          { ciRet :: Coin
ciRet = TxOut era
txout forall s a. s -> Getting a s a -> a
^. forall era. (HasCallStack, EraTxOut era) => Lens' (TxOut era) Coin
coinTxOutL
          , ciAddmap :: Map (TxIn (EraCrypto era)) (TxOut era)
ciAddmap = Map (TxIn (EraCrypto era)) (TxOut era)
newstuff
          }
        where
          newstuff :: Map (TxIn (EraCrypto era)) (TxOut era)
newstuff = forall era.
SafeHash (EraCrypto era) EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map (TxIn (EraCrypto era)) (TxOut era)
additions SafeHash StandardCrypto EraIndependentTxBody
hash TxIx
firstTxIx [TxOut era
txout]
  Collateral Set (TxIn (EraCrypto era))
inputs ->
    CollInfo era
info
      { ciDelset :: Set (TxIn (EraCrypto era))
ciDelset = Set (TxIn (EraCrypto era))
inputs
      , ciBal :: Coin
ciBal = forall era.
EraTxOut era =>
Set (TxIn (EraCrypto era)) -> MUtxo era -> Coin
txInBalance Set (TxIn (EraCrypto era))
inputs (forall era.
ModelNewEpochState era -> Map (TxIn (EraCrypto era)) (TxOut era)
mUTxO Model era
model)
      }
  TxBodyField era
_ -> CollInfo era
info

updateInfo :: CollInfo era -> Model era -> Model era
updateInfo :: forall era. CollInfo era -> Model era -> Model era
updateInfo CollInfo era
info Model era
m =
  Model era
m
    { mUTxO :: Map (TxIn (EraCrypto era)) (TxOut era)
mUTxO = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (forall era. CollInfo era -> Map (TxIn (EraCrypto era)) (TxOut era)
ciAddmap CollInfo era
info) (forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys (forall era.
ModelNewEpochState era -> Map (TxIn (EraCrypto era)) (TxOut era)
mUTxO Model era
m) (forall era. CollInfo era -> Set (TxIn (EraCrypto era))
ciDelset CollInfo era
info))
    , mFees :: Coin
mFees = forall era. ModelNewEpochState era -> Coin
mFees Model era
m forall t. Val t => t -> t -> t
<+> forall era. CollInfo era -> Coin
ciBal CollInfo era
info forall t. Val t => t -> t -> t
<-> forall era. CollInfo era -> Coin
ciRet CollInfo era
info
    }

applyTxFail :: Reflect era => Proof era -> Int -> TxIx -> Model era -> TxField era -> Model era
applyTxFail :: forall era.
Reflect era =>
Proof era -> Int -> TxIx -> Model era -> TxField era -> Model era
applyTxFail Proof era
proof Int
count TxIx
nextTxIx Model era
model TxField era
field = case TxField era
field of
  Body TxBody era
body2 -> forall era. CollInfo era -> Model era -> Model era
updateInfo CollInfo era
info Model era
model
    where
      info :: CollInfo era
info = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall era.
(Reflect era, HasCallStack) =>
Int
-> TxIx
-> Model era
-> CollInfo era
-> TxBodyField era
-> CollInfo era
collInfo Int
count TxIx
nextTxIx Model era
model) forall era. CollInfo era
emptyCollInfo (forall era. Proof era -> TxBody era -> [TxBodyField era]
abstractTxBody Proof era
proof TxBody era
body2)
  BodyI [TxBodyField era]
fs -> forall era. CollInfo era -> Model era -> Model era
updateInfo CollInfo era
info Model era
model
    where
      info :: CollInfo era
info = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (forall era.
(Reflect era, HasCallStack) =>
Int
-> TxIx
-> Model era
-> CollInfo era
-> TxBodyField era
-> CollInfo era
collInfo Int
count TxIx
nextTxIx Model era
model) forall era. CollInfo era
emptyCollInfo [TxBodyField era]
fs
  TxWits TxWits era
_ -> Model era
model
  WitnessesI [WitnessesField era]
_ -> Model era
model
  AuxData StrictMaybe (TxAuxData era)
_ -> Model era
model
  Valid IsValid
_ -> Model era
model

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

additions ::
  SafeHash (EraCrypto era) EraIndependentTxBody ->
  TxIx ->
  [TxOut era] ->
  Map (TxIn (EraCrypto era)) (TxOut era)
additions :: forall era.
SafeHash (EraCrypto era) EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map (TxIn (EraCrypto era)) (TxOut era)
additions SafeHash (EraCrypto era) EraIndependentTxBody
bodyhash TxIx
firstTxIx [TxOut era]
outputs =
  forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (forall c. TxId c -> TxIx -> TxIn c
TxIn (forall c. SafeHash c EraIndependentTxBody -> TxId c
TxId SafeHash (EraCrypto era) EraIndependentTxBody
bodyhash) TxIx
idx, TxOut era
out)
    | (TxOut era
out, TxIx
idx) <- forall a b. [a] -> [b] -> [(a, b)]
zip [TxOut era]
outputs [TxIx
firstTxIx ..]
    ]

-- | This is a template of how we might create unit tests that run both the real STS rules
--   and the model to see that they agree. 'collateralOutputTx' and 'initUTxO' are from
--   the BabbageFeatures.hs unit test file.
go :: IO ()
go :: IO ()
go = do
  let proof :: Proof (BabbageEra StandardCrypto)
proof = Proof (BabbageEra StandardCrypto)
Babbage
      tx :: AlonzoTx (BabbageEra StandardCrypto)
tx = (forall era.
(Scriptic era, EraTx era, GoodCrypto (EraCrypto era)) =>
Proof era -> Tx era
notValidatingTx Proof (BabbageEra StandardCrypto)
proof) {isValid :: IsValid
isValid = Bool -> IsValid
IsValid Bool
False}
      allinputs :: Set (TxIn (EraCrypto (BabbageEra StandardCrypto)))
allinputs = BabbageTxBody (BabbageEra StandardCrypto)
txbody forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
SimpleGetter (TxBody era) (Set (TxIn (EraCrypto era)))
allInputsTxBodyF
      txbody :: TxBody (BabbageEra StandardCrypto)
txbody = forall era. AlonzoTx era -> TxBody era
body AlonzoTx (BabbageEra StandardCrypto)
tx
      doc :: PDoc
doc = forall era. Proof era -> Tx era -> PDoc
pcTx Proof (BabbageEra StandardCrypto)
proof AlonzoTx (BabbageEra StandardCrypto)
tx
      model1 :: ModelNewEpochState (BabbageEra StandardCrypto)
model1 =
        (forall era. Reflect era => ModelNewEpochState era
mNewEpochStateZero @(BabbageEra StandardCrypto))
          { mUTxO :: Map
  (TxIn (EraCrypto (BabbageEra StandardCrypto)))
  (TxOut (BabbageEra StandardCrypto))
mUTxO = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys (forall era. UTxO era -> Map (TxIn (EraCrypto era)) (TxOut era)
unUTxO (forall era.
(EraTxOut era, PostShelley era) =>
Proof era -> UTxO era
initUTxO Proof (BabbageEra StandardCrypto)
proof)) Set (TxIn StandardCrypto)
allinputs
          , mCount :: Int
mCount = Int
0
          , mFees :: Coin
mFees = Integer -> Coin
Coin Integer
10
          , mIndex :: Map Int (TxId (EraCrypto (BabbageEra StandardCrypto)))
mIndex = forall k a. k -> a -> Map k a
Map.singleton Int
0 (forall c. SafeHash c EraIndependentTxBody -> TxId c
TxId (forall x index c.
(HashAnnotated x index c, HashAlgorithm (HASH c)) =>
x -> SafeHash c index
hashAnnotated BabbageTxBody (BabbageEra StandardCrypto)
txbody))
          }
      model2 :: ModelNewEpochState (BabbageEra StandardCrypto)
model2 = forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> Model era -> Tx era -> Model era
applyTx Proof (BabbageEra StandardCrypto)
proof Int
0 (Word64 -> SlotNo
SlotNo Word64
0) ModelNewEpochState (BabbageEra StandardCrypto)
model1 AlonzoTx (BabbageEra StandardCrypto)
tx
  forall a. Show a => a -> IO ()
print (forall era.
Reflect era =>
Proof era -> ModelNewEpochState era -> PDoc
pcModelNewEpochState Proof (BabbageEra StandardCrypto)
proof ModelNewEpochState (BabbageEra StandardCrypto)
model1)
  forall a. Show a => a -> IO ()
print PDoc
doc
  forall a. Show a => a -> IO ()
print (forall era.
Reflect era =>
Proof era -> ModelNewEpochState era -> PDoc
pcModelNewEpochState Proof (BabbageEra StandardCrypto)
proof ModelNewEpochState (BabbageEra StandardCrypto)
model2)

filterRewards ::
  EraPParams era =>
  PParams era ->
  Map (Credential 'Staking (EraCrypto era)) (Set (Reward (EraCrypto era))) ->
  ( Map (Credential 'Staking (EraCrypto era)) (Set (Reward (EraCrypto era)))
  , Map (Credential 'Staking (EraCrypto era)) (Set (Reward (EraCrypto era)))
  )
filterRewards :: forall era.
EraPParams era =>
PParams era
-> Map
     (Credential 'Staking (EraCrypto era))
     (Set (Reward (EraCrypto era)))
-> (Map
      (Credential 'Staking (EraCrypto era))
      (Set (Reward (EraCrypto era))),
    Map
      (Credential 'Staking (EraCrypto era))
      (Set (Reward (EraCrypto era))))
filterRewards PParams era
pp Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
rewards =
  if ProtVer -> Version
pvMajor (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL) forall a. Ord a => a -> a -> Bool
> forall (v :: Natural).
(KnownNat v, MinVersion <= v, v <= MaxVersion) =>
Version
natVersion @2
    then (Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
rewards, forall k a. Map k a
Map.empty)
    else
      let mp :: Map
  (Credential 'Staking (EraCrypto era))
  (Reward (EraCrypto era), Set (Reward (EraCrypto era)))
mp = forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall a. Set a -> (a, Set a)
Set.deleteFindMin Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
rewards
       in (forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (forall a. a -> Set a
Set.singleton forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) Map
  (Credential 'Staking (EraCrypto era))
  (Reward (EraCrypto era), Set (Reward (EraCrypto era)))
mp, forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> Bool
Set.null) forall a b. (a -> b) -> a -> b
$ forall a b k. (a -> b) -> Map k a -> Map k b
Map.map forall a b. (a, b) -> b
snd Map
  (Credential 'Staking (EraCrypto era))
  (Reward (EraCrypto era), Set (Reward (EraCrypto era)))
mp)

filterAllRewards ::
  EraPParams era =>
  Map (Credential 'Staking (EraCrypto era)) (Set (Reward (EraCrypto era))) ->
  Model era ->
  ( Map (Credential 'Staking (EraCrypto era)) (Set (Reward (EraCrypto era)))
  , Map (Credential 'Staking (EraCrypto era)) (Set (Reward (EraCrypto era)))
  , Set (Credential 'Staking (EraCrypto era))
  , Coin
  )
filterAllRewards :: forall era.
EraPParams era =>
Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
-> Model era
-> (Map
      (Credential 'Staking (EraCrypto era))
      (Set (Reward (EraCrypto era))),
    Map
      (Credential 'Staking (EraCrypto era))
      (Set (Reward (EraCrypto era))),
    Set (Credential 'Staking (EraCrypto era)), Coin)
filterAllRewards Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
rs' Model era
m =
  (Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
registered, Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
eraIgnored, Set (Credential 'Staking (EraCrypto era))
unregistered, Coin
totalUnregistered)
  where
    pp :: PParams era
pp = forall era. ModelNewEpochState era -> PParams era
mPParams Model era
m
    (Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
regRU, Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
unregRU) =
      forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
        (\Credential 'Staking (EraCrypto era)
k Set (Reward (EraCrypto era))
_ -> forall s t. Embed s t => Exp t -> s
eval (Credential 'Staking (EraCrypto era)
k forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mRewards Model era
m)))
        Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
rs'
    totalUnregistered :: Coin
totalUnregistered = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall a b. (a -> b) -> a -> b
$ forall c.
ProtVer
-> Map (Credential 'Staking c) (Set (Reward c))
-> Map (Credential 'Staking c) Coin
aggregateRewards (PParams era
pp forall s a. s -> Getting a s a -> a
^. forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL) Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
unregRU
    unregistered :: Set (Credential 'Staking (EraCrypto era))
unregistered = forall k a. Map k a -> Set k
Map.keysSet Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
unregRU

    (Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
registered, Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
eraIgnored) = forall era.
EraPParams era =>
PParams era
-> Map
     (Credential 'Staking (EraCrypto era))
     (Set (Reward (EraCrypto era)))
-> (Map
      (Credential 'Staking (EraCrypto era))
      (Set (Reward (EraCrypto era))),
    Map
      (Credential 'Staking (EraCrypto era))
      (Set (Reward (EraCrypto era))))
filterRewards PParams era
pp Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
regRU

applyRUpd ::
  forall era.
  RewardUpdateOld (EraCrypto era) ->
  Model era ->
  Model era
applyRUpd :: forall era.
RewardUpdateOld (EraCrypto era) -> Model era -> Model era
applyRUpd RewardUpdateOld (EraCrypto era)
ru Model era
m =
  Model era
m
    { mFees :: Coin
mFees = forall era. ModelNewEpochState era -> Coin
mFees Model era
m Coin -> DeltaCoin -> Coin
`addDeltaCoin` forall c. RewardUpdateOld c -> DeltaCoin
deltaFOld @(EraCrypto era) RewardUpdateOld (EraCrypto era)
ru
    , mRewards :: Map (Credential 'Staking (EraCrypto era)) Coin
mRewards = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith forall a. Semigroup a => a -> a -> a
(<>) (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking (EraCrypto era)) Coin
mRewards Model era
m) (forall c. RewardUpdateOld c -> Map (Credential 'Staking c) Coin
rsOld RewardUpdateOld (EraCrypto era)
ru)
    }

notValidatingTx ::
  ( Scriptic era
  , EraTx era
  , GoodCrypto (EraCrypto era)
  ) =>
  Proof era ->
  Tx era
notValidatingTx :: forall era.
(Scriptic era, EraTx era, GoodCrypto (EraCrypto era)) =>
Proof era -> Tx era
notValidatingTx Proof era
pf =
  forall era. Proof era -> [TxField era] -> Tx era
newTx
    Proof era
pf
    [ forall era. TxBody era -> TxField era
Body TxBody era
notValidatingBody
    , forall era. [WitnessesField era] -> TxField era
WitnessesI
        [ forall era.
Era era =>
[WitVKey 'Witness (EraCrypto era)] -> WitnessesField era
AddrWits' [forall c (kr :: KeyRole).
(Crypto c, DSignable c (Hash (HASH c) EraIndependentTxBody)) =>
SafeHash c EraIndependentTxBody
-> KeyPair kr c -> WitVKey 'Witness c
mkWitnessVKey (forall x index c.
(HashAnnotated x index c, HashAlgorithm (HASH c)) =>
x -> SafeHash c index
hashAnnotated TxBody era
notValidatingBody) (forall era.
Era era =>
Proof era -> KeyPair 'Payment (EraCrypto era)
someKeys Proof era
pf)]
        , forall era. EraScript era => [Script era] -> WitnessesField era
ScriptWits' [forall era. Scriptic era => Natural -> Proof era -> Script era
never Natural
0 Proof era
pf]
        , forall era. Era era => [Data era] -> WitnessesField era
DataWits' [forall era. Era era => Data -> Data era
Data (Integer -> Data
PV1.I Integer
0)]
        , forall era. Redeemers era -> WitnessesField era
RdmrWits Redeemers era
redeemers
        ]
    ]
  where
    notValidatingBody :: TxBody era
notValidatingBody =
      forall era.
EraTxBody era =>
Proof era -> [TxBodyField era] -> TxBody era
newTxBody
        Proof era
pf
        [ forall era. [TxIn (EraCrypto era)] -> TxBodyField era
Inputs' [forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
2]
        , forall era. [TxIn (EraCrypto era)] -> TxBodyField era
Collateral' [forall c.
(HashAlgorithm (HASH c), HasCallStack) =>
Integer -> TxIn c
mkGenesisTxIn Integer
12]
        , forall era. [TxOut era] -> TxBodyField era
Outputs' [forall era. Era era => Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [forall era. Addr (EraCrypto era) -> TxOutField era
Address (forall era. Era era => Proof era -> Addr (EraCrypto era)
someAddr Proof era
pf), forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
2995)]]
        , forall era. Coin -> TxBodyField era
Txfee (Integer -> Coin
Coin Integer
5)
        , forall era.
StrictMaybe (ScriptIntegrityHash (EraCrypto era))
-> TxBodyField era
WppHash (forall era.
Proof era
-> PParams era
-> [Language]
-> Redeemers era
-> TxDats era
-> StrictMaybe (ScriptIntegrityHash (EraCrypto era))
newScriptIntegrityHash Proof era
pf (forall era. EraPParams era => Proof era -> PParams era
pparams Proof era
pf) [Language
PlutusV1] Redeemers era
redeemers (forall era. Era era => Data era -> TxDats era
mkTxDats (forall era. Era era => Data -> Data era
Data (Integer -> Data
PV1.I Integer
0))))
        ]
    redeemers :: Redeemers era
redeemers =
      forall era.
Proof era
-> [((PlutusPurposeTag, Word32), (Data era, ExUnits))]
-> Redeemers era
mkRedeemersFromTags Proof era
pf [((PlutusPurposeTag
Spending, Word32
0), (forall era. Era era => Data -> Data era
Data (Integer -> Data
PV1.I Integer
1), Natural -> Natural -> ExUnits
ExUnits Natural
5000 Natural
5000))]