{-# 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.Credential (Credential)
import Cardano.Ledger.Plutus.Data (Data (..))
import Cardano.Ledger.Plutus.Language (Language (PlutusV1))
import Cardano.Ledger.PoolParams (PoolParams (..))
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 -> Model era -> Model era
applyRUpd RewardUpdateOld
ru forall a b. (a -> b) -> a -> b
$
        Model era
model
          { mEL :: EpochNo
mEL = EpochNo
transactionEpoch
          }
    else Model era
model
  where
    ru :: RewardUpdateOld
ru = forall era. Proof era -> Model era -> RewardUpdateOld
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
txins -> Model era
model {mUTxO :: Map TxIn (TxOut era)
mUTxO = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.withoutKeys (forall era. ModelNewEpochState era -> Map TxIn (TxOut era)
mUTxO Model era
model) Set TxIn
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
mIndex Model era
model) of
    Maybe TxId
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
mIndex Model era
model))
    Just (TxId SafeHash EraIndependentTxBody
hash) -> Model era
model {mUTxO :: Map TxIn (TxOut era)
mUTxO = forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map TxIn (TxOut era)
newstuff (forall era. ModelNewEpochState era -> Map TxIn (TxOut era)
mUTxO Model era
model)}
      where
        newstuff :: Map TxIn (TxOut era)
newstuff = forall era.
SafeHash EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map TxIn (TxOut era)
additions SafeHash 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 RewardAccount Coin
m) -> forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' (forall era.
Proof era -> Model era -> RewardAccount -> Coin -> Model era
applyWithdrawals Proof era
proof) Model era
model Map RewardAccount Coin
m
  TxBodyField era
_other -> Model era
model

applyWithdrawals :: Proof era -> Model era -> RewardAccount -> Coin -> Model era
applyWithdrawals :: forall era.
Proof era -> Model era -> RewardAccount -> Coin -> Model era
applyWithdrawals Proof era
_proof Model era
model (RewardAccount Network
_network Credential 'Staking
cred) Coin
coin =
  Model era
model {mRewards :: Map (Credential 'Staking) 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
cred (forall era.
ModelNewEpochState era -> Map (Credential 'Staking) 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
x) ->
    Model era
model
      { mRewards :: Map (Credential 'Staking) Coin
mRewards = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Credential 'Staking
x (Integer -> Coin
Coin Integer
0) (forall era.
ModelNewEpochState era -> Map (Credential 'Staking) Coin
mRewards Model era
model)
      , mKeyDeposits :: Map (Credential 'Staking) Coin
mKeyDeposits = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Credential 'Staking
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) 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
x) -> case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Credential 'Staking
x (forall era.
ModelNewEpochState era -> Map (Credential 'Staking) 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). Credential keyrole -> PDoc
pcCredential Credential 'Staking
x))
    Just (Coin Integer
0) ->
      Model era
model
        { mRewards :: Map (Credential 'Staking) Coin
mRewards = forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Credential 'Staking
x (forall era.
ModelNewEpochState era -> Map (Credential 'Staking) Coin
mRewards Model era
model)
        , mKeyDeposits :: Map (Credential 'Staking) Coin
mKeyDeposits = forall k a. Ord k => k -> Map k a -> Map k a
Map.delete Credential 'Staking
x (forall era.
ModelNewEpochState era -> Map (Credential 'Staking) 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
x (forall era.
ModelNewEpochState era -> Map (Credential 'Staking) 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
cred KeyHash 'StakePool
hash) ->
    Model era
model {mDelegations :: Map (Credential 'Staking) (KeyHash 'StakePool)
mDelegations = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Credential 'Staking
cred KeyHash 'StakePool
hash (forall era.
ModelNewEpochState era
-> Map (Credential 'Staking) (KeyHash 'StakePool)
mDelegations Model era
model)}
  ShelleyTxCertPool (RegPool PoolParams
poolparams) ->
    Model era
model
      { mPoolParams :: Map (KeyHash 'StakePool) PoolParams
mPoolParams = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'StakePool
hk PoolParams
poolparams (forall era.
ModelNewEpochState era -> Map (KeyHash 'StakePool) PoolParams
mPoolParams Model era
model)
      , mDeposited :: Coin
mDeposited =
          if forall k a. Ord k => k -> Map k a -> Bool
Map.member KeyHash 'StakePool
hk (forall era. ModelNewEpochState era -> Map (KeyHash 'StakePool) 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) 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
hk (forall era. ModelNewEpochState era -> Map (KeyHash 'StakePool) Coin
mPoolDeposits Model era
model)
            then forall era. ModelNewEpochState era -> Map (KeyHash 'StakePool) Coin
mPoolDeposits Model era
model
            else forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'StakePool
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) Coin
mPoolDeposits Model era
model)
      }
    where
      hk :: KeyHash 'StakePool
hk = PoolParams -> KeyHash 'StakePool
ppId PoolParams
poolparams
      pp :: PParams era
pp = forall era. ModelNewEpochState era -> PParams era
mPParams Model era
model
  ShelleyTxCertPool (RetirePool KeyHash 'StakePool
keyhash EpochNo
epoch) ->
    Model era
model
      { mRetiring :: Map (KeyHash 'StakePool) EpochNo
mRetiring = forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert KeyHash 'StakePool
keyhash EpochNo
epoch (forall era.
ModelNewEpochState era -> Map (KeyHash 'StakePool) 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
_ -> Model era
model
  ShelleyTxCertMir MIRCert
_ -> 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
ciDelset :: Set TxIn -- The set of inputs to delete from the UTxO
  , forall era. CollInfo era -> Map TxIn (TxOut era)
ciAddmap :: Map TxIn (TxOut era) -- Things to Add to the UTxO
  }

emptyCollInfo :: CollInfo era
emptyCollInfo :: forall era. CollInfo era
emptyCollInfo = forall era.
Coin -> Coin -> Set TxIn -> Map TxIn (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
mIndex Model era
model) of
      Maybe TxId
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
mIndex Model era
model))
      Just (TxId SafeHash 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 (TxOut era)
ciAddmap = Map TxIn (TxOut era)
newstuff
          }
        where
          newstuff :: Map TxIn (TxOut era)
newstuff = forall era.
SafeHash EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map TxIn (TxOut era)
additions SafeHash EraIndependentTxBody
hash TxIx
firstTxIx [TxOut era
txout]
  Collateral Set TxIn
inputs ->
    CollInfo era
info
      { ciDelset :: Set TxIn
ciDelset = Set TxIn
inputs
      , ciBal :: Coin
ciBal = forall era. EraTxOut era => Set TxIn -> MUtxo era -> Coin
txInBalance Set TxIn
inputs (forall era. ModelNewEpochState era -> Map TxIn (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 (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 (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 (TxOut era)
mUTxO Model era
m) (forall era. CollInfo era -> Set TxIn
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 EraIndependentTxBody ->
  TxIx ->
  [TxOut era] ->
  Map TxIn (TxOut era)
additions :: forall era.
SafeHash EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map TxIn (TxOut era)
additions SafeHash EraIndependentTxBody
bodyhash TxIx
firstTxIx [TxOut era]
outputs =
  forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
    [ (TxId -> TxIx -> TxIn
TxIn (SafeHash EraIndependentTxBody -> TxId
TxId SafeHash 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
proof = Proof BabbageEra
Babbage
      tx :: AlonzoTx BabbageEra
tx = (forall era. (Scriptic era, EraTx era) => Proof era -> Tx era
notValidatingTx Proof BabbageEra
proof) {isValid :: IsValid
isValid = Bool -> IsValid
IsValid Bool
False}
      allinputs :: Set TxIn
allinputs = BabbageTxBody BabbageEra
txbody forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => SimpleGetter (TxBody era) (Set TxIn)
allInputsTxBodyF
      txbody :: TxBody BabbageEra
txbody = forall era. AlonzoTx era -> TxBody era
body AlonzoTx BabbageEra
tx
      doc :: PDoc
doc = forall era. Proof era -> Tx era -> PDoc
pcTx Proof BabbageEra
proof AlonzoTx BabbageEra
tx
      model1 :: ModelNewEpochState BabbageEra
model1 =
        (forall era. Reflect era => ModelNewEpochState era
mNewEpochStateZero @BabbageEra)
          { mUTxO :: Map TxIn (TxOut BabbageEra)
mUTxO = forall k a. Ord k => Map k a -> Set k -> Map k a
Map.restrictKeys (forall era. UTxO era -> Map TxIn (TxOut era)
unUTxO (forall era.
(EraTxOut era, PostShelley era) =>
Proof era -> UTxO era
initUTxO Proof BabbageEra
proof)) Set TxIn
allinputs
          , mCount :: Int
mCount = Int
0
          , mFees :: Coin
mFees = Integer -> Coin
Coin Integer
10
          , mIndex :: Map Int TxId
mIndex = forall k a. k -> a -> Map k a
Map.singleton Int
0 (SafeHash EraIndependentTxBody -> TxId
TxId (forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated BabbageTxBody BabbageEra
txbody))
          }
      model2 :: ModelNewEpochState BabbageEra
model2 = forall era.
Reflect era =>
Proof era -> Int -> SlotNo -> Model era -> Tx era -> Model era
applyTx Proof BabbageEra
proof Int
0 (Word64 -> SlotNo
SlotNo Word64
0) ModelNewEpochState BabbageEra
model1 AlonzoTx BabbageEra
tx
  forall a. Show a => a -> IO ()
print (forall era.
Reflect era =>
Proof era -> ModelNewEpochState era -> PDoc
pcModelNewEpochState Proof BabbageEra
proof ModelNewEpochState BabbageEra
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
proof ModelNewEpochState BabbageEra
model2)

filterRewards ::
  EraPParams era =>
  PParams era ->
  Map (Credential 'Staking) (Set Reward) ->
  ( Map (Credential 'Staking) (Set Reward)
  , Map (Credential 'Staking) (Set Reward)
  )
filterRewards :: forall era.
EraPParams era =>
PParams era
-> Map (Credential 'Staking) (Set Reward)
-> (Map (Credential 'Staking) (Set Reward),
    Map (Credential 'Staking) (Set Reward))
filterRewards PParams era
pp Map (Credential 'Staking) (Set Reward)
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) (Set Reward)
rewards, forall k a. Map k a
Map.empty)
    else
      let mp :: Map (Credential 'Staking) (Reward, Set Reward)
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) (Set Reward)
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) (Reward, Set Reward)
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) (Reward, Set Reward)
mp)

filterAllRewards ::
  EraPParams era =>
  Map (Credential 'Staking) (Set Reward) ->
  Model era ->
  ( Map (Credential 'Staking) (Set Reward)
  , Map (Credential 'Staking) (Set Reward)
  , Set (Credential 'Staking)
  , Coin
  )
filterAllRewards :: forall era.
EraPParams era =>
Map (Credential 'Staking) (Set Reward)
-> Model era
-> (Map (Credential 'Staking) (Set Reward),
    Map (Credential 'Staking) (Set Reward), Set (Credential 'Staking),
    Coin)
filterAllRewards Map (Credential 'Staking) (Set Reward)
rs' Model era
m =
  (Map (Credential 'Staking) (Set Reward)
registered, Map (Credential 'Staking) (Set Reward)
eraIgnored, Set (Credential 'Staking)
unregistered, Coin
totalUnregistered)
  where
    pp :: PParams era
pp = forall era. ModelNewEpochState era -> PParams era
mPParams Model era
m
    (Map (Credential 'Staking) (Set Reward)
regRU, Map (Credential 'Staking) (Set Reward)
unregRU) =
      forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
        (\Credential 'Staking
k Set Reward
_ -> forall s t. Embed s t => Exp t -> s
eval (Credential 'Staking
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) Coin
mRewards Model era
m)))
        Map (Credential 'Staking) (Set Reward)
rs'
    totalUnregistered :: Coin
totalUnregistered = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold forall a b. (a -> b) -> a -> b
$ ProtVer
-> Map (Credential 'Staking) (Set Reward)
-> Map (Credential 'Staking) 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) (Set Reward)
unregRU
    unregistered :: Set (Credential 'Staking)
unregistered = forall k a. Map k a -> Set k
Map.keysSet Map (Credential 'Staking) (Set Reward)
unregRU

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

applyRUpd ::
  forall era.
  RewardUpdateOld ->
  Model era ->
  Model era
applyRUpd :: forall era. RewardUpdateOld -> Model era -> Model era
applyRUpd RewardUpdateOld
ru Model era
m =
  Model era
m
    { mFees :: Coin
mFees = forall era. ModelNewEpochState era -> Coin
mFees Model era
m Coin -> DeltaCoin -> Coin
`addDeltaCoin` RewardUpdateOld -> DeltaCoin
deltaFOld RewardUpdateOld
ru
    , mRewards :: Map (Credential 'Staking) 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) Coin
mRewards Model era
m) (RewardUpdateOld -> Map (Credential 'Staking) Coin
rsOld RewardUpdateOld
ru)
    }

notValidatingTx ::
  ( Scriptic era
  , EraTx era
  ) =>
  Proof era ->
  Tx era
notValidatingTx :: forall era. (Scriptic era, EraTx 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] -> WitnessesField era
AddrWits' [forall (kr :: KeyRole).
SafeHash EraIndependentTxBody -> KeyPair kr -> WitVKey 'Witness
mkWitnessVKey (forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
notValidatingBody) (forall era. Proof era -> KeyPair 'Payment
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] -> TxBodyField era
Inputs' [HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
2]
        , forall era. [TxIn] -> TxBodyField era
Collateral' [HasCallStack => Integer -> TxIn
mkGenesisTxIn Integer
12]
        , forall era. [TxOut era] -> TxBodyField era
Outputs' [forall era. Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [forall era. Addr -> TxOutField era
Address (forall era. Proof era -> Addr
someAddr Proof era
pf), forall era. Value era -> TxOutField era
Amount (forall t s. Inject t s => t -> s
inject forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
2995)]]
        , forall era. Coin -> TxBodyField era
Txfee (Integer -> Coin
Coin Integer
5)
        , forall era. StrictMaybe ScriptIntegrityHash -> TxBodyField era
WppHash (forall era.
Proof era
-> PParams era
-> [Language]
-> Redeemers era
-> TxDats era
-> StrictMaybe ScriptIntegrityHash
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))]