{-# 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.State (UTxO (..))
import Cardano.Ledger.TxIn (TxId (..), TxIn (..))
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 =
  [ CostModels -> PParamsField era
forall era. CostModels -> PParamsField era
Costmdls (CostModels -> PParamsField era) -> CostModels -> PParamsField era
forall a b. (a -> b) -> a -> b
$ HasCallStack => [Language] -> CostModels
[Language] -> CostModels
zeroTestingCostModels [Language
PlutusV1]
  , Natural -> PParamsField era
forall era. Natural -> PParamsField era
MaxValSize Natural
1000000000
  , ExUnits -> PParamsField era
forall era. ExUnits -> PParamsField era
MaxTxExUnits (ExUnits -> PParamsField era) -> ExUnits -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> ExUnits
ExUnits Natural
1000000 Natural
1000000
  , ExUnits -> PParamsField era
forall era. ExUnits -> PParamsField era
MaxBlockExUnits (ExUnits -> PParamsField era) -> ExUnits -> PParamsField era
forall a b. (a -> b) -> a -> b
$ Natural -> Natural -> ExUnits
ExUnits Natural
1000000 Natural
1000000
  , ProtVer -> PParamsField era
forall era. ProtVer -> PParamsField era
ProtocolVersion (ProtVer -> PParamsField era) -> ProtVer -> PParamsField era
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
  , Coin -> PParamsField era
forall era. Coin -> PParamsField era
KeyDeposit (Integer -> Coin
Coin Integer
2)
  , Coin -> PParamsField era
forall era. Coin -> PParamsField era
PoolDeposit (Integer -> Coin
Coin Integer
5)
  , Natural -> PParamsField era
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 = Proof era -> [PParamsField era] -> PParams era
forall era.
EraPParams era =>
Proof era -> [PParamsField era] -> PParams era
newPParams Proof era
pf [PParamsField era]
forall era. [PParamsField era]
defaultPPs

hasValid :: [TxField era] -> Maybe Bool
hasValid :: forall era. [TxField era] -> Maybe Bool
hasValid [] = Maybe Bool
forall a. Maybe a
Nothing
hasValid (Valid (IsValid Bool
b) : [TxField era]
_) = Bool -> Maybe Bool
forall a. a -> Maybe a
Just Bool
b
hasValid (TxField era
_ : [TxField era]
fs) = [TxField era] -> Maybe Bool
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 = Model era -> EpochNo
forall era. ModelNewEpochState era -> EpochNo
mEL Model era
model
    epochAccurateModel :: Model era
epochAccurateModel = Proof era -> EpochNo -> EpochNo -> Model era -> Model era
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 = Proof era -> Tx era -> TxBody era
forall era. EraTx era => Proof era -> Tx era -> TxBody era
getBody Proof era
proof Tx era
tx
    outputs :: StrictSeq (TxOut era)
outputs = Proof era -> TxBody era -> StrictSeq (TxOut era)
forall era.
EraTxBody era =>
Proof era -> TxBody era -> StrictSeq (TxOut era)
getOutputs Proof era
proof TxBody era
txbody
    fields :: [TxField era]
fields = Proof era -> Tx era -> [TxField era]
forall era. Proof era -> Tx era -> [TxField era]
abstractTx Proof era
proof Tx era
tx
    nextTxIx :: TxIx
nextTxIx = HasCallStack => Integer -> TxIx
Integer -> TxIx
mkTxIxPartial (Int -> Integer
forall a b. (Integral a, Num b) => a -> b
fromIntegral (StrictSeq (TxOut era) -> Int
forall a. StrictSeq a -> Int
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 [TxField era] -> Maybe Bool
forall era. [TxField era] -> Maybe Bool
hasValid [TxField era]
fields of
      Maybe Bool
Nothing -> (Model era -> TxField era -> Model era)
-> Model era -> [TxField era] -> Model era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (Proof era -> Int -> Model era -> TxField era -> Model era
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 -> (Model era -> TxField era -> Model era)
-> Model era -> [TxField era] -> Model era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (Proof era -> Int -> Model era -> TxField era -> Model era
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 -> (Model era -> TxField era -> Model era)
-> Model era -> [TxField era] -> Model era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (Proof era -> Int -> TxIx -> Model era -> TxField era -> Model era
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 EpochNo -> EpochNo -> Bool
forall a. Ord a => a -> a -> Bool
> EpochNo
modelEpoch
    then
      RewardUpdateOld -> Model era -> Model era
forall era. RewardUpdateOld -> Model era -> Model era
applyRUpd RewardUpdateOld
ru (Model era -> Model era) -> Model era -> Model era
forall a b. (a -> b) -> a -> b
$
        Model era
model
          { mEL = transactionEpoch
          }
    else Model era
model
  where
    ru :: RewardUpdateOld
ru = Proof era -> Model era -> RewardUpdateOld
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 -> Proof era -> Int -> Model era -> TxBody era -> Model era
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 -> (Model era -> TxBodyField era -> Model era)
-> Model era -> [TxBodyField era] -> Model era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (Proof era -> Int -> Model era -> TxBodyField era -> Model era
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 = (Model era -> TxBodyField era -> Model era)
-> Model era -> [TxBodyField era] -> Model era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (Proof era -> Int -> Model era -> TxBodyField era -> Model era
forall era.
Reflect era =>
Proof era -> Int -> Model era -> TxBodyField era -> Model era
applyField Proof era
proof Int
count) Model era
model (Proof era -> TxBody era -> [TxBodyField era]
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.withoutKeys (mUTxO model) txins}
  Outputs StrictSeq (TxOut era)
seqo -> case Int -> Map Int TxId -> Maybe TxId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
count (Model era -> Map Int TxId
forall era. ModelNewEpochState era -> Map Int TxId
mIndex Model era
model) of
    Maybe TxId
Nothing -> [Char] -> Model era
forall a. HasCallStack => [Char] -> a
error ([Char]
"Output not found phase1: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ Map Int TxId -> [Char]
forall a. Show a => a -> [Char]
show (Model era -> Map Int TxId
forall era. ModelNewEpochState era -> Map Int TxId
mIndex Model era
model))
    Just (TxId SafeHash EraIndependentTxBody
hash) -> Model era
model {mUTxO = Map.union newstuff (mUTxO model)}
      where
        newstuff :: Map TxIn (TxOut era)
newstuff = SafeHash EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map TxIn (TxOut era)
forall era.
SafeHash EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map TxIn (TxOut era)
additions SafeHash EraIndependentTxBody
hash TxIx
forall a. Bounded a => a
minBound (StrictSeq (TxOut era) -> [TxOut era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxOut era)
seqo)
  Txfee Coin
coin -> Model era
model {mFees = coin <+> mFees model}
  Certs StrictSeq (TxCert era)
seqc -> (Model era -> TxCert era -> Model era)
-> Model era -> [TxCert era] -> Model era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' Model era -> TxCert era -> Model era
forall era. Reflect era => Model era -> TxCert era -> Model era
applyCert Model era
model (StrictSeq (TxCert era) -> [TxCert era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList StrictSeq (TxCert era)
seqc)
  Withdrawals' (Withdrawals Map RewardAccount Coin
m) -> (Model era -> RewardAccount -> Coin -> Model era)
-> Model era -> Map RewardAccount Coin -> Model era
forall a k b. (a -> k -> b -> a) -> a -> Map k b -> a
Map.foldlWithKey' (Proof era -> Model era -> RewardAccount -> Coin -> Model era
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.adjust (<-> coin) cred (mRewards 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 -> Model era -> TxCert era -> Model era
Model era -> ShelleyTxCert era -> Model era
forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Mary -> Model era -> TxCert era -> Model era
Model era -> ShelleyTxCert era -> Model era
forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Allegra -> Model era -> TxCert era -> Model era
Model era -> ShelleyTxCert era -> Model era
forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Alonzo -> Model era -> TxCert era -> Model era
Model era -> ShelleyTxCert era -> Model era
forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Babbage -> Model era -> TxCert era -> Model era
Model era -> ShelleyTxCert era -> Model era
forall era.
EraPParams era =>
Model era -> ShelleyTxCert era -> Model era
applyShelleyCert
  Proof era
Conway -> [Char]
-> Model ConwayEra -> ConwayTxCert ConwayEra -> Model ConwayEra
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.insert x (Coin 0) (mRewards model)
      , mKeyDeposits = Map.insert x (pp ^. ppKeyDepositL) (mKeyDeposits model)
      , mDeposited = mDeposited model <+> pp ^. ppKeyDepositL
      }
    where
      pp :: PParams era
pp = Model era -> PParams era
forall era. ModelNewEpochState era -> PParams era
mPParams Model era
model
  ShelleyTxCertDelegCert (ShelleyUnRegCert Credential 'Staking
x) -> case Credential 'Staking -> Map (Credential 'Staking) Coin -> Maybe Coin
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Credential 'Staking
x (Model era -> Map (Credential 'Staking) Coin
forall era.
ModelNewEpochState era -> Map (Credential 'Staking) Coin
mRewards Model era
model) of
    Maybe Coin
Nothing -> [Char] -> Model era
forall a. HasCallStack => [Char] -> a
error ([Char]
"DeRegKey not in rewards: " [Char] -> [Char] -> [Char]
forall a. Semigroup a => a -> a -> a
<> PDoc -> [Char]
forall a. Show a => a -> [Char]
show (Credential 'Staking -> PDoc
forall (keyrole :: KeyRole). Credential keyrole -> PDoc
pcCredential Credential 'Staking
x))
    Just (Coin Integer
0) ->
      Model era
model
        { mRewards = Map.delete x (mRewards model)
        , mKeyDeposits = Map.delete x (mKeyDeposits model)
        , mDeposited = mDeposited model <-> keyDeposit
        }
      where
        keyDeposit :: Coin
keyDeposit = Coin
-> Credential 'Staking -> Map (Credential 'Staking) Coin -> Coin
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault Coin
forall a. Monoid a => a
mempty Credential 'Staking
x (Model era -> Map (Credential 'Staking) Coin
forall era.
ModelNewEpochState era -> Map (Credential 'Staking) Coin
mKeyDeposits Model era
model)
    Just (Coin Integer
_n) -> [Char] -> Model era
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.insert cred hash (mDelegations model)}
  ShelleyTxCertPool (RegPool PoolParams
poolparams) ->
    Model era
model
      { mPoolParams = Map.insert hk poolparams (mPoolParams model)
      , mDeposited =
          if Map.member hk (mPoolDeposits model)
            then mDeposited model
            else mDeposited model <+> pp ^. ppPoolDepositL
      , mPoolDeposits -- Only add if it isn't already there
        =
          if Map.member hk (mPoolDeposits model)
            then mPoolDeposits model
            else Map.insert hk (pp ^. ppPoolDepositL) (mPoolDeposits model)
      }
    where
      hk :: KeyHash 'StakePool
hk = PoolParams -> KeyHash 'StakePool
ppId PoolParams
poolparams
      pp :: PParams era
pp = Model era -> PParams era
forall era. ModelNewEpochState era -> PParams era
mPParams Model era
model
  ShelleyTxCertPool (RetirePool KeyHash 'StakePool
keyhash EpochNo
epoch) ->
    Model era
model
      { mRetiring = Map.insert keyhash epoch (mRetiring model)
      , mDeposited = mDeposited model <-> pp ^. ppPoolDepositL
      }
    where
      pp :: PParams era
pp = Model era -> PParams era
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 = Coin -> Coin -> Set TxIn -> Map TxIn (TxOut era) -> CollInfo era
forall era.
Coin -> Coin -> Set TxIn -> Map TxIn (TxOut era) -> CollInfo era
CollInfo (Integer -> Coin
Coin Integer
0) (Integer -> Coin
Coin Integer
0) Set TxIn
forall a. Set a
Set.empty Map TxIn (TxOut era)
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 Int -> Map Int TxId -> Maybe TxId
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
count (Model era -> Map Int TxId
forall era. ModelNewEpochState era -> Map Int TxId
mIndex Model era
model) of
      Maybe TxId
Nothing -> [Char] -> CollInfo era
forall a. HasCallStack => [Char] -> a
error ([Char]
"Output not found phase2: " [Char] -> [Char] -> [Char]
forall a. [a] -> [a] -> [a]
++ (Int, Map Int TxId) -> [Char]
forall a. Show a => a -> [Char]
show (Int
count, Model era -> Map Int TxId
forall era. ModelNewEpochState era -> Map Int TxId
mIndex Model era
model))
      Just (TxId SafeHash EraIndependentTxBody
hash) ->
        CollInfo era
info
          { ciRet = txout ^. coinTxOutL
          , ciAddmap = newstuff
          }
        where
          newstuff :: Map TxIn (TxOut era)
newstuff = SafeHash EraIndependentTxBody
-> TxIx -> [TxOut era] -> Map TxIn (TxOut era)
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 = inputs
      , ciBal = txInBalance inputs (mUTxO 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.union (ciAddmap info) (Map.withoutKeys (mUTxO m) (ciDelset info))
    , mFees = mFees m <+> ciBal info <-> ciRet 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 -> CollInfo era -> Model era -> Model era
forall era. CollInfo era -> Model era -> Model era
updateInfo CollInfo era
info Model era
model
    where
      info :: CollInfo era
info = (CollInfo era -> TxBodyField era -> CollInfo era)
-> CollInfo era -> [TxBodyField era] -> CollInfo era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (Int
-> TxIx
-> Model era
-> CollInfo era
-> TxBodyField era
-> CollInfo era
forall era.
(Reflect era, HasCallStack) =>
Int
-> TxIx
-> Model era
-> CollInfo era
-> TxBodyField era
-> CollInfo era
collInfo Int
count TxIx
nextTxIx Model era
model) CollInfo era
forall era. CollInfo era
emptyCollInfo (Proof era -> TxBody era -> [TxBodyField era]
forall era. Proof era -> TxBody era -> [TxBodyField era]
abstractTxBody Proof era
proof TxBody era
body2)
  BodyI [TxBodyField era]
fs -> CollInfo era -> Model era -> Model era
forall era. CollInfo era -> Model era -> Model era
updateInfo CollInfo era
info Model era
model
    where
      info :: CollInfo era
info = (CollInfo era -> TxBodyField era -> CollInfo era)
-> CollInfo era -> [TxBodyField era] -> CollInfo era
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
List.foldl' (Int
-> TxIx
-> Model era
-> CollInfo era
-> TxBodyField era
-> CollInfo era
forall era.
(Reflect era, HasCallStack) =>
Int
-> TxIx
-> Model era
-> CollInfo era
-> TxBodyField era
-> CollInfo era
collInfo Int
count TxIx
nextTxIx Model era
model) CollInfo era
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 =
  [(TxIn, TxOut era)] -> Map TxIn (TxOut era)
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) <- [TxOut era] -> [TxIx] -> [(TxOut era, TxIx)]
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 = (Proof BabbageEra -> Tx BabbageEra
forall era. (Scriptic era, EraTx era) => Proof era -> Tx era
notValidatingTx Proof BabbageEra
proof) {isValid = IsValid False}
      allinputs :: Set TxIn
allinputs = TxBody BabbageEra
txbody TxBody BabbageEra
-> Getting (Set TxIn) (TxBody BabbageEra) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody BabbageEra) (Set TxIn)
forall era. EraTxBody era => SimpleGetter (TxBody era) (Set TxIn)
SimpleGetter (TxBody BabbageEra) (Set TxIn)
allInputsTxBodyF
      txbody :: TxBody BabbageEra
txbody = AlonzoTx BabbageEra -> TxBody BabbageEra
forall era. AlonzoTx era -> TxBody era
body AlonzoTx BabbageEra
tx
      doc :: PDoc
doc = Proof BabbageEra -> Tx BabbageEra -> PDoc
forall era. Proof era -> Tx era -> PDoc
pcTx Proof BabbageEra
proof Tx BabbageEra
AlonzoTx BabbageEra
tx
      model1 :: ModelNewEpochState BabbageEra
model1 =
        (forall era. Reflect era => ModelNewEpochState era
mNewEpochStateZero @BabbageEra)
          { mUTxO = Map.restrictKeys (unUTxO (initUTxO proof)) allinputs
          , mCount = 0
          , mFees = Coin 10
          , mIndex = Map.singleton 0 (TxId (hashAnnotated txbody))
          }
      model2 :: ModelNewEpochState BabbageEra
model2 = Proof BabbageEra
-> Int
-> SlotNo
-> ModelNewEpochState BabbageEra
-> Tx BabbageEra
-> ModelNewEpochState BabbageEra
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 Tx BabbageEra
AlonzoTx BabbageEra
tx
  PDoc -> IO ()
forall a. Show a => a -> IO ()
print (Proof BabbageEra -> ModelNewEpochState BabbageEra -> PDoc
forall era.
Reflect era =>
Proof era -> ModelNewEpochState era -> PDoc
pcModelNewEpochState Proof BabbageEra
proof ModelNewEpochState BabbageEra
model1)
  PDoc -> IO ()
forall a. Show a => a -> IO ()
print PDoc
doc
  PDoc -> IO ()
forall a. Show a => a -> IO ()
print (Proof BabbageEra -> ModelNewEpochState BabbageEra -> PDoc
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 PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL) Version -> Version -> Bool
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, Map (Credential 'Staking) (Set Reward)
forall k a. Map k a
Map.empty)
    else
      let mp :: Map (Credential 'Staking) (Reward, Set Reward)
mp = (Set Reward -> (Reward, Set Reward))
-> Map (Credential 'Staking) (Set Reward)
-> Map (Credential 'Staking) (Reward, Set Reward)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Set Reward -> (Reward, Set Reward)
forall a. Set a -> (a, Set a)
Set.deleteFindMin Map (Credential 'Staking) (Set Reward)
rewards
       in (((Reward, Set Reward) -> Set Reward)
-> Map (Credential 'Staking) (Reward, Set Reward)
-> Map (Credential 'Staking) (Set Reward)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Reward -> Set Reward
forall a. a -> Set a
Set.singleton (Reward -> Set Reward)
-> ((Reward, Set Reward) -> Reward)
-> (Reward, Set Reward)
-> Set Reward
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Reward, Set Reward) -> Reward
forall a b. (a, b) -> a
fst) Map (Credential 'Staking) (Reward, Set Reward)
mp, (Set Reward -> Bool)
-> Map (Credential 'Staking) (Set Reward)
-> Map (Credential 'Staking) (Set Reward)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (Bool -> Bool
not (Bool -> Bool) -> (Set Reward -> Bool) -> Set Reward -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set Reward -> Bool
forall a. Set a -> Bool
Set.null) (Map (Credential 'Staking) (Set Reward)
 -> Map (Credential 'Staking) (Set Reward))
-> Map (Credential 'Staking) (Set Reward)
-> Map (Credential 'Staking) (Set Reward)
forall a b. (a -> b) -> a -> b
$ ((Reward, Set Reward) -> Set Reward)
-> Map (Credential 'Staking) (Reward, Set Reward)
-> Map (Credential 'Staking) (Set Reward)
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map (Reward, Set Reward) -> Set Reward
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 = Model era -> PParams era
forall era. ModelNewEpochState era -> PParams era
mPParams Model era
m
    (Map (Credential 'Staking) (Set Reward)
regRU, Map (Credential 'Staking) (Set Reward)
unregRU) =
      (Credential 'Staking -> Set Reward -> Bool)
-> Map (Credential 'Staking) (Set Reward)
-> (Map (Credential 'Staking) (Set Reward),
    Map (Credential 'Staking) (Set Reward))
forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey
        (\Credential 'Staking
k Set Reward
_ -> Exp Bool -> Bool
forall s t. Embed s t => Exp t -> s
eval (Credential 'Staking
k Credential 'Staking
-> Exp (Sett (Credential 'Staking) ()) -> Exp Bool
forall k (g :: * -> * -> *) s.
(Show k, Ord k, Iter g, HasExp s (g k ())) =>
k -> s -> Exp Bool
∈ Map (Credential 'Staking) Coin
-> Exp (Sett (Credential 'Staking) ())
forall k s (f :: * -> * -> *) v.
(Ord k, HasExp s (f k v)) =>
s -> Exp (Sett k ())
dom (Model era -> Map (Credential 'Staking) Coin
forall era.
ModelNewEpochState era -> Map (Credential 'Staking) Coin
mRewards Model era
m)))
        Map (Credential 'Staking) (Set Reward)
rs'
    totalUnregistered :: Coin
totalUnregistered = Map (Credential 'Staking) Coin -> Coin
forall m. Monoid m => Map (Credential 'Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Map (Credential 'Staking) Coin -> Coin)
-> Map (Credential 'Staking) Coin -> Coin
forall a b. (a -> b) -> a -> b
$ ProtVer
-> Map (Credential 'Staking) (Set Reward)
-> Map (Credential 'Staking) Coin
aggregateRewards (PParams era
pp PParams era -> Getting ProtVer (PParams era) ProtVer -> ProtVer
forall s a. s -> Getting a s a -> a
^. Getting ProtVer (PParams era) ProtVer
forall era. EraPParams era => Lens' (PParams era) ProtVer
Lens' (PParams era) ProtVer
ppProtocolVersionL) Map (Credential 'Staking) (Set Reward)
unregRU
    unregistered :: Set (Credential 'Staking)
unregistered = Map (Credential 'Staking) (Set Reward) -> Set (Credential 'Staking)
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) = PParams era
-> Map (Credential 'Staking) (Set Reward)
-> (Map (Credential 'Staking) (Set Reward),
    Map (Credential 'Staking) (Set Reward))
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 = mFees m `addDeltaCoin` deltaFOld ru
    , mRewards = Map.unionWith (<>) (mRewards m) (rsOld 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 =
  Proof era -> [TxField era] -> Tx era
forall era. Proof era -> [TxField era] -> Tx era
newTx
    Proof era
pf
    [ TxBody era -> TxField era
forall era. TxBody era -> TxField era
Body TxBody era
notValidatingBody
    , [WitnessesField era] -> TxField era
forall era. [WitnessesField era] -> TxField era
WitnessesI
        [ [WitVKey 'Witness] -> WitnessesField era
forall era. Era era => [WitVKey 'Witness] -> WitnessesField era
AddrWits' [SafeHash EraIndependentTxBody
-> KeyPair 'Payment -> WitVKey 'Witness
forall (kr :: KeyRole).
SafeHash EraIndependentTxBody -> KeyPair kr -> WitVKey 'Witness
mkWitnessVKey (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated TxBody era
notValidatingBody) (Proof era -> KeyPair 'Payment
forall era. Proof era -> KeyPair 'Payment
someKeys Proof era
pf)]
        , [Script era] -> WitnessesField era
forall era. EraScript era => [Script era] -> WitnessesField era
ScriptWits' [Natural -> Proof era -> Script era
forall era. Scriptic era => Natural -> Proof era -> Script era
never Natural
0 Proof era
pf]
        , [Data era] -> WitnessesField era
forall era. Era era => [Data era] -> WitnessesField era
DataWits' [Data -> Data era
forall era. Era era => Data -> Data era
Data (Integer -> Data
PV1.I Integer
0)]
        , Redeemers era -> WitnessesField era
forall era. Redeemers era -> WitnessesField era
RdmrWits Redeemers era
redeemers
        ]
    ]
  where
    notValidatingBody :: TxBody era
notValidatingBody =
      Proof era -> [TxBodyField era] -> TxBody era
forall era.
EraTxBody era =>
Proof era -> [TxBodyField era] -> TxBody era
newTxBody
        Proof era
pf
        [ [TxIn] -> TxBodyField era
forall era. [TxIn] -> TxBodyField era
Inputs' [HasCallStack => Integer -> TxIn
Integer -> TxIn
mkGenesisTxIn Integer
2]
        , [TxIn] -> TxBodyField era
forall era. [TxIn] -> TxBodyField era
Collateral' [HasCallStack => Integer -> TxIn
Integer -> TxIn
mkGenesisTxIn Integer
12]
        , [TxOut era] -> TxBodyField era
forall era. [TxOut era] -> TxBodyField era
Outputs' [Proof era -> [TxOutField era] -> TxOut era
forall era. Proof era -> [TxOutField era] -> TxOut era
newTxOut Proof era
pf [Addr -> TxOutField era
forall era. Addr -> TxOutField era
Address (Proof era -> Addr
forall era. Proof era -> Addr
someAddr Proof era
pf), Value era -> TxOutField era
forall era. Value era -> TxOutField era
Amount (Coin -> Value era
forall t s. Inject t s => t -> s
inject (Coin -> Value era) -> Coin -> Value era
forall a b. (a -> b) -> a -> b
$ Integer -> Coin
Coin Integer
2995)]]
        , Coin -> TxBodyField era
forall era. Coin -> TxBodyField era
Txfee (Integer -> Coin
Coin Integer
5)
        , StrictMaybe ScriptIntegrityHash -> TxBodyField era
forall era. StrictMaybe ScriptIntegrityHash -> TxBodyField era
WppHash (Proof era
-> PParams era
-> [Language]
-> Redeemers era
-> TxDats era
-> StrictMaybe ScriptIntegrityHash
forall era.
Proof era
-> PParams era
-> [Language]
-> Redeemers era
-> TxDats era
-> StrictMaybe ScriptIntegrityHash
newScriptIntegrityHash Proof era
pf (Proof era -> PParams era
forall era. EraPParams era => Proof era -> PParams era
pparams Proof era
pf) [Language
PlutusV1] Redeemers era
redeemers (Data era -> TxDats era
forall era. Era era => Data era -> TxDats era
mkTxDats (Data -> Data era
forall era. Era era => Data -> Data era
Data (Integer -> Data
PV1.I Integer
0))))
        ]
    redeemers :: Redeemers era
redeemers =
      Proof era
-> [((PlutusPurposeTag, Word32), (Data era, ExUnits))]
-> Redeemers era
forall era.
Proof era
-> [((PlutusPurposeTag, Word32), (Data era, ExUnits))]
-> Redeemers era
mkRedeemersFromTags Proof era
pf [((PlutusPurposeTag
Spending, Word32
0), (Data -> Data era
forall era. Era era => Data -> Data era
Data (Integer -> Data
PV1.I Integer
1), Natural -> Natural -> ExUnits
ExUnits Natural
5000 Natural
5000))]