{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}

module Test.Cardano.Ledger.Shelley.Rules.AdaPreservation (
  adaPreservationProps,
  tests,
) where

import Test.Cardano.Ledger.Shelley.Rules.TestChain (
  TestingLedger,
  forAllChainTrace,
  ledgerTraceFromBlock,
  ledgerTraceFromBlockWithRestrictedUTxO,
  longTraceLen,
 )

import Cardano.Ledger.BaseTypes (StrictMaybe (..))
import Cardano.Ledger.Block (
  Block (..),
  bbody,
 )
import Cardano.Ledger.CertState (
  CertState (..),
  DState (..),
  certsTotalDepositsTxBody,
  certsTotalRefundsTxBody,
 )
import Cardano.Ledger.Coin
import Cardano.Ledger.Compactible (fromCompact)
import Cardano.Ledger.Shelley.Core
import Cardano.Ledger.Shelley.Internal (compareAdaPots)
import Cardano.Ledger.Shelley.LedgerState (
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  PState (..),
  UTxOState (..),
  completeRupd,
  curPParamsEpochStateL,
  deltaF,
  deltaR,
  deltaT,
  iRReserves,
  iRTreasury,
  prevPParamsEpochStateL,
  rewards,
  rs,
 )
import Cardano.Ledger.Shelley.Rewards (sumRewards)
import Cardano.Ledger.Shelley.Rules (votedFuturePParams)
import Cardano.Ledger.Shelley.Rules.Reports (
  showCred,
  showIR,
  showKeyHash,
  showListy,
  showMap,
  showWithdrawal,
 )
import Cardano.Ledger.UMap (sumRewardsUView)
import qualified Cardano.Ledger.UMap as UM
import Cardano.Ledger.UTxO (UTxO (..), coinBalance, txInsFilter, txouts)
import Cardano.Ledger.Val ((<+>), (<->))
import Cardano.Protocol.TPraos.BHeader (BHeader (..))
import Data.Foldable as F (fold, foldl', toList)
import Data.Map (Map)
import qualified Data.Map.Strict as Map
import Data.TreeDiff.QuickCheck (ediffEq)
import Lens.Micro hiding (ix)
import Lens.Micro.Extras (view)
import Test.Cardano.Ledger.Shelley.ConcreteCryptoTypes (MockCrypto)
import Test.Cardano.Ledger.Shelley.Constants (defaultConstants)
import Test.Cardano.Ledger.Shelley.Generator.Core (GenEnv)
import Test.Cardano.Ledger.Shelley.Generator.EraGen (EraGen (..))
import Test.Cardano.Ledger.Shelley.Generator.ShelleyEraGen ()
import Test.Cardano.Ledger.Shelley.Rules.Chain (CHAIN, ChainState (..), totalAda, totalAdaPots)
import Test.Cardano.Ledger.Shelley.Utils (
  ChainProperty,
  runShelleyBase,
 )
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  Trace (..),
  sourceSignalTargets,
 )
import qualified Test.Control.State.Transition.Trace.Generator.QuickCheck as QC
import Test.QuickCheck (
  Property,
  Testable (..),
  conjoin,
  counterexample,
  noShrinking,
  (.&&.),
  (.||.),
  (===),
 )
import Test.QuickCheck.Property (withMaxSuccess)
import Test.Tasty (TestTree)
import qualified Test.Tasty.QuickCheck as TQC

tests ::
  forall era ledger.
  ( EraGen era
  , TestingLedger era ledger
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv era)
  , GovState era ~ ShelleyGovState era
  ) =>
  Int ->
  TestTree
tests :: forall era ledger.
(EraGen era, TestingLedger era ledger, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv era),
 GovState era ~ ShelleyGovState era) =>
Int -> TestTree
tests Int
n =
  forall a. Testable a => TestName -> a -> TestTree
TQC.testProperty
    TestName
"total amount of Ada is preserved (Chain)"
    (forall prop. Testable prop => prop -> Property
noShrinking forall a b. (a -> b) -> a -> b
$ forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (forall era ledger.
(EraGen era, TestingLedger era ledger, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv era),
 GovState era ~ ShelleyGovState era) =>
Property
adaPreservationProps @era @ledger))

-- | Various preservation properties
adaPreservationProps ::
  forall era ledger.
  ( EraGen era
  , TestingLedger era ledger
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv era)
  , GovState era ~ ShelleyGovState era
  ) =>
  Property
adaPreservationProps :: forall era ledger.
(EraGen era, TestingLedger era ledger, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv era),
 GovState era ~ ShelleyGovState era) =>
Property
adaPreservationProps =
  forall era prop.
(Testable prop, EraGen era, HasTrace (CHAIN era) (GenEnv era),
 EraGov era) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
longTraceLen Constants
defaultConstants forall a b. (a -> b) -> a -> b
$ \Trace (CHAIN era)
tr -> do
    let ssts :: [SourceSignalTarget (CHAIN era)]
        -- In this test, the STS Signal has this definition
        -- Signal(CHAIN era) = Block (BHeader MockCrypto) era
        ssts :: [SourceSignalTarget (CHAIN era)]
ssts = forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr
        noEpochBoundarySsts :: [SourceSignalTarget (CHAIN era)]
noEpochBoundarySsts = forall a. (a -> Bool) -> [a] -> [a]
filter forall era. SourceSignalTarget (CHAIN era) -> Bool
sameEpoch [SourceSignalTarget (CHAIN era)]
ssts
        justBoundarySsts :: [SourceSignalTarget (CHAIN era)]
justBoundarySsts = forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. SourceSignalTarget (CHAIN era) -> Bool
sameEpoch) [SourceSignalTarget (CHAIN era)]
ssts

    forall prop. Testable prop => [prop] -> Property
conjoin forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat forall a b. (a -> b) -> a -> b
$
      [ -- preservation properties
        forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall era.
(EraSegWits era, GovState era ~ ShelleyGovState era, EraGov era) =>
SourceSignalTarget (CHAIN era) -> Int -> Property
checkPreservation @era) [SourceSignalTarget (CHAIN era)]
justBoundarySsts [Int
0 ..]
      , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseWithdrawalsPerTx @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseByRewardsPerTx @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
preserveBalance @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, TestingLedger era ledger, EraSegWits era) =>
SourceSignalTarget (CHAIN era) -> Property
preserveBalanceRestricted @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
preserveOutputsTx @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
potsRewardsDecreaseByWithdrawalsPerTx @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
canRestrictUTxO @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , -- well formed deposits
        forall a b. (a -> b) -> [a] -> [b]
map forall era. SourceSignalTarget (CHAIN era) -> Property
nonNegativeDeposits [SourceSignalTarget (CHAIN era)]
ssts
      , -- non-epoch-boundary preservation properties
        forall a b. (a -> b) -> [a] -> [b]
map forall era.
EraGen era =>
SourceSignalTarget (CHAIN era) -> Property
checkWithdrawalBound [SourceSignalTarget (CHAIN era)]
noEpochBoundarySsts
      , forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
utxoDepositsIncreaseByFeesWithdrawals @era @ledger) [SourceSignalTarget (CHAIN era)]
noEpochBoundarySsts
      , forall a b. (a -> b) -> [a] -> [b]
map forall era.
(ChainProperty era, EraGen era) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseWithdrawalsPerBlock [SourceSignalTarget (CHAIN era)]
noEpochBoundarySsts
      , forall a b. (a -> b) -> [a] -> [b]
map forall era. SourceSignalTarget (CHAIN era) -> Property
feesNonDecreasing [SourceSignalTarget (CHAIN era)]
noEpochBoundarySsts
      ]

infoRetire :: Map (KeyHash 'StakePool) Coin -> KeyHash 'StakePool -> String
infoRetire :: Map (KeyHash 'StakePool) Coin -> KeyHash 'StakePool -> TestName
infoRetire Map (KeyHash 'StakePool) Coin
deposits KeyHash 'StakePool
keyhash = forall (x :: KeyRole). KeyHash x -> TestName
showKeyHash KeyHash 'StakePool
keyhash forall a. [a] -> [a] -> [a]
++ TestName
extra
  where
    extra :: TestName
extra = case forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'StakePool
keyhash Map (KeyHash 'StakePool) Coin
deposits of
      Maybe Coin
Nothing -> TestName
" (?)"
      Just Coin
coin -> TestName
" (" forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Coin
coin forall a. [a] -> [a] -> [a]
++ TestName
")"

-- ADA should be preserved for all state transitions in the generated trace
checkPreservation ::
  forall era.
  ( EraSegWits era
  , GovState era ~ ShelleyGovState era
  , EraGov era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Int ->
  Property
checkPreservation :: forall era.
(EraSegWits era, GovState era ~ ShelleyGovState era, EraGov era) =>
SourceSignalTarget (CHAIN era) -> Int -> Property
checkPreservation SourceSignalTarget {State (CHAIN era)
source :: forall a. SourceSignalTarget a -> State a
source :: State (CHAIN era)
source, State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target :: State (CHAIN era)
target, Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal :: Signal (CHAIN era)
signal} Int
count =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample
    ( forall a. Monoid a => [a] -> a
mconcat
        ( [ TestName
"\ncount = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Int
count forall a. [a] -> [a] -> [a]
++ TestName
"\n"
          , TestName -> AdaPots -> TestName -> AdaPots -> TestName
compareAdaPots TestName
"before" (forall era. (EraTxOut era, EraGov era) => ChainState era -> AdaPots
totalAdaPots State (CHAIN era)
source) TestName
"after" (forall era. (EraTxOut era, EraGov era) => ChainState era -> AdaPots
totalAdaPots State (CHAIN era)
target)
          , TestName
"\n\nTotal lovelace before block\n"
          , forall a. Show a => a -> TestName
show Coin
sourceTotal
          , TestName
"\n\nTotal lovelace after block\n"
          , forall a. Show a => a -> TestName
show Coin
targetTotal
          , TestName
"\n\nEpoch before block\n"
          , forall a. Show a => a -> TestName
show (forall era. NewEpochState era -> EpochNo
nesEL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source)
          , TestName
"\n\nEpoch after block\n"
          , forall a. Show a => a -> TestName
show (forall era. NewEpochState era -> EpochNo
nesEL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
target)
          , TestName
"\n\nCurrent protocol parameters\n"
          , forall a. Show a => a -> TestName
show PParams era
currPP
          , TestName
"\nReward Accounts before update\n"
          , forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap (forall a. Int -> [a] -> [a]
take Int
10 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (x :: KeyRole). Credential x -> TestName
showCred) forall a. Show a => a -> TestName
show (forall k v. UView k v -> Map k v
UM.unUnify UView (Credential 'Staking) RDPair
oldRAs)
          , TestName
"\nReward Accounts after update\n"
          , forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap (forall a. Int -> [a] -> [a]
take Int
10 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (x :: KeyRole). Credential x -> TestName
showCred) forall a. Show a => a -> TestName
show (forall k v. UView k v -> Map k v
UM.unUnify UView (Credential 'Staking) RDPair
newRAs)
          , TestName
"\nRetiring pools before update\n"
          , forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap (Map (KeyHash 'StakePool) Coin -> KeyHash 'StakePool -> TestName
infoRetire Map (KeyHash 'StakePool) Coin
oldPoolDeposit) forall a. Show a => a -> TestName
show Map (KeyHash 'StakePool) EpochNo
oldRetire
          , TestName
"\nRetiring pools after update\n"
          , forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap (Map (KeyHash 'StakePool) Coin -> KeyHash 'StakePool -> TestName
infoRetire Map (KeyHash 'StakePool) Coin
newPoolDeposit) forall a. Show a => a -> TestName
show Map (KeyHash 'StakePool) EpochNo
newRetire
          , TestName
"\nMIR\n"
          , InstantaneousRewards -> TestName
showIR InstantaneousRewards
mir
          , TestName
"\n\nRegistered Reserves MIR total "
          , forall a. Show a => a -> TestName
show (forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
regMirRes)
          , TestName
"\n\nUnregistered Reserves MIR total "
          , forall a. Show a => a -> TestName
show (forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
unRegMirRes)
          , TestName
"\n\nRegistered Treasury MIR total "
          , forall a. Show a => a -> TestName
show (forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
regMirTre)
          , TestName
"\n\nUnregistered Treasury MIR total "
          , forall a. Show a => a -> TestName
show (forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
unRegMirTre)
          , TestName
"\n\nPools Retiring This epoch\n"
          , forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap
              (Map (KeyHash 'StakePool) Coin -> KeyHash 'StakePool -> TestName
infoRetire Map (KeyHash 'StakePool) Coin
oldPoolDeposit)
              forall a. Show a => a -> TestName
show
              (forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\EpochNo
e -> EpochNo
e forall a. Eq a => a -> a -> Bool
== (forall era. NewEpochState era -> EpochNo
nesEL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
target)) Map (KeyHash 'StakePool) EpochNo
oldRetire)
          ]
            forall a. [a] -> [a] -> [a]
++ [TestName]
obligationMsgs
            forall a. [a] -> [a] -> [a]
++ [TestName]
rewardUpdateMsgs
            forall a. [a] -> [a] -> [a]
++ [TestName
"\n\ntransactions"]
            forall a. [a] -> [a] -> [a]
++ [TestName]
txs
        )
    )
    forall a b. (a -> b) -> a -> b
$ Coin
sourceTotal forall a. (Eq a, Show a) => a -> a -> Property
=== Coin
targetTotal
  where
    sourceTotal :: Coin
sourceTotal = forall era. (EraTxOut era, EraGov era) => ChainState era -> Coin
totalAda State (CHAIN era)
source
    targetTotal :: Coin
targetTotal = forall era. (EraTxOut era, EraGov era) => ChainState era -> Coin
totalAda State (CHAIN era)
target

    currPP :: PParams era
currPP = forall a s. Getting a s a -> s -> a
view forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source
    prevPP :: ProtVer
prevPP = forall a s. Getting a s a -> s -> a
view forall era. EraPParams era => Lens' (PParams era) ProtVer
ppProtocolVersionL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a s. Getting a s a -> s -> a
view forall era. EraGov era => Lens' (EpochState era) (PParams era)
prevPParamsEpochStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source

    ru' :: StrictMaybe PulsingRewUpdate
ru' = forall era. NewEpochState era -> StrictMaybe PulsingRewUpdate
nesRu forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source
    lsOld :: LedgerState era
lsOld = forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source
    lsNew :: LedgerState era
lsNew = forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
target
    oldRAs :: UView (Credential 'Staking) RDPair
oldRAs = forall era. DState era -> UView (Credential 'Staking) RDPair
rewards forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall a b. (a -> b) -> a -> b
$ LedgerState era
lsOld
    newRAs :: UView (Credential 'Staking) RDPair
newRAs = forall era. DState era -> UView (Credential 'Staking) RDPair
rewards forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall a b. (a -> b) -> a -> b
$ LedgerState era
lsNew
    oldCertState :: CertState era
oldCertState = forall era. LedgerState era -> CertState era
lsCertState LedgerState era
lsOld
    oldRetire :: Map (KeyHash 'StakePool) EpochNo
oldRetire = forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
psRetiring forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> PState era
certPState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall a b. (a -> b) -> a -> b
$ LedgerState era
lsOld
    newRetire :: Map (KeyHash 'StakePool) EpochNo
newRetire = forall era. PState era -> Map (KeyHash 'StakePool) EpochNo
psRetiring forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> PState era
certPState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall a b. (a -> b) -> a -> b
$ LedgerState era
lsNew
    oldPoolDeposit :: Map (KeyHash 'StakePool) Coin
oldPoolDeposit = forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> PState era
certPState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall a b. (a -> b) -> a -> b
$ LedgerState era
lsOld
    newPoolDeposit :: Map (KeyHash 'StakePool) Coin
newPoolDeposit = forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> PState era
certPState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall a b. (a -> b) -> a -> b
$ LedgerState era
lsNew

    proposal :: Maybe (PParams era)
proposal = forall era.
EraPParams era =>
ProposedPPUpdates era
-> PParams era -> Word64 -> Maybe (PParams era)
votedFuturePParams (forall era. ShelleyGovState era -> ProposedPPUpdates era
sgsCurProposals forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. UTxOState era -> GovState era
utxosGovState forall a b. (a -> b) -> a -> b
$ forall era. LedgerState era -> UTxOState era
lsUTxOState LedgerState era
lsOld) PParams era
currPP Word64
5
    obligationMsgs :: [TestName]
obligationMsgs = case Maybe (PParams era)
proposal of
      Maybe (PParams era)
Nothing -> []
      Just PParams era
proposal' ->
        [ TestName
"\n\nProposed protocol parameter update\n"
        , forall a. Show a => a -> TestName
show PParams era
proposal'
        ]

    mir :: InstantaneousRewards
mir = forall era. DState era -> InstantaneousRewards
dsIRewards forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall a b. (a -> b) -> a -> b
$ LedgerState era
lsOld
    isRegistered :: Credential 'Staking -> Coin -> Bool
isRegistered Credential 'Staking
kh Coin
_ = forall k v. k -> UView k v -> Bool
UM.member Credential 'Staking
kh UView (Credential 'Staking) RDPair
oldRAs
    (Map (Credential 'Staking) Coin
regMirRes, Map (Credential 'Staking) Coin
unRegMirRes) = forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey Credential 'Staking -> Coin -> Bool
isRegistered (InstantaneousRewards -> Map (Credential 'Staking) Coin
iRReserves InstantaneousRewards
mir)
    (Map (Credential 'Staking) Coin
regMirTre, Map (Credential 'Staking) Coin
unRegMirTre) = forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey Credential 'Staking -> Coin -> Bool
isRegistered (InstantaneousRewards -> Map (Credential 'Staking) Coin
iRTreasury InstantaneousRewards
mir)

    rewardUpdateMsgs :: [TestName]
rewardUpdateMsgs = case StrictMaybe PulsingRewUpdate
ru' of
      StrictMaybe PulsingRewUpdate
SNothing -> []
      SJust PulsingRewUpdate
ru'' ->
        let (RewardUpdate
ru, Map (Credential 'Staking) (Set Reward)
_rewevent) = forall a. ShelleyBase a -> a
runShelleyBase (PulsingRewUpdate
-> ShelleyBase
     (RewardUpdate, Map (Credential 'Staking) (Set Reward))
completeRupd PulsingRewUpdate
ru'')
            regRewards :: Map (Credential 'Staking) (Set Reward)
regRewards = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\Credential 'Staking
kh Set Reward
_ -> forall k v. k -> UView k v -> Bool
UM.member Credential 'Staking
kh UView (Credential 'Staking) RDPair
oldRAs) (RewardUpdate -> Map (Credential 'Staking) (Set Reward)
rs RewardUpdate
ru)
         in [ TestName
"\n\nSum of new rewards "
            , forall a. Show a => a -> TestName
show (ProtVer -> Map (Credential 'Staking) (Set Reward) -> Coin
sumRewards ProtVer
prevPP (RewardUpdate -> Map (Credential 'Staking) (Set Reward)
rs RewardUpdate
ru))
            , TestName
"\n\nNew rewards "
            , forall a. Show a => a -> TestName
show (RewardUpdate -> Map (Credential 'Staking) (Set Reward)
rs RewardUpdate
ru)
            , TestName
"\n\nSum of new registered rewards "
            , forall a. Show a => a -> TestName
show (ProtVer -> Map (Credential 'Staking) (Set Reward) -> Coin
sumRewards ProtVer
prevPP Map (Credential 'Staking) (Set Reward)
regRewards)
            , TestName
"\n\nChange in Fees "
            , forall a. Show a => a -> TestName
show (RewardUpdate -> DeltaCoin
deltaF RewardUpdate
ru)
            , TestName
"\n\nChange in Treasury "
            , forall a. Show a => a -> TestName
show (RewardUpdate -> DeltaCoin
deltaT RewardUpdate
ru)
            , TestName
"\n\nChange in Reserves "
            , forall a. Show a => a -> TestName
show (RewardUpdate -> DeltaCoin
deltaR RewardUpdate
ru)
            , TestName
"\n\nNet effect of reward update "
            , forall a. Show a => a -> TestName
show forall a b. (a -> b) -> a -> b
$
                RewardUpdate -> DeltaCoin
deltaT RewardUpdate
ru
                  forall a. Semigroup a => a -> a -> a
<> RewardUpdate -> DeltaCoin
deltaF RewardUpdate
ru
                  forall a. Semigroup a => a -> a -> a
<> RewardUpdate -> DeltaCoin
deltaR RewardUpdate
ru
                  forall a. Semigroup a => a -> a -> a
<> Coin -> DeltaCoin
toDeltaCoin (ProtVer -> Map (Credential 'Staking) (Set Reward) -> Coin
sumRewards ProtVer
prevPP (RewardUpdate -> Map (Credential 'Staking) (Set Reward)
rs RewardUpdate
ru))
            ]

    txs' :: [Tx era]
txs' = forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ (forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq @era forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall h era. Block h era -> TxSeq era
bbody) Signal (CHAIN era)
signal
    txs :: [TestName]
txs = forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Tx era -> Int -> TestName
dispTx [Tx era]
txs' [Int
0 :: Int ..]

    dispTx :: Tx era -> Int -> TestName
dispTx Tx era
tx Int
ix =
      TestName
"\n\n******** Transaction "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Int
ix
        forall a. [a] -> [a] -> [a]
++ TestName
" "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated (Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL))
        forall a. [a] -> [a] -> [a]
++ TestName
"\nfee :"
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL)
        forall a. [a] -> [a] -> [a]
++ TestName
"\nwithdrawals:"
        forall a. [a] -> [a] -> [a]
++ Withdrawals -> TestName
showWithdrawal (Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL)
        forall a. [a] -> [a] -> [a]
++ TestName
"\ncerts:"
        forall a. [a] -> [a] -> [a]
++ forall (t :: * -> *) a.
Foldable t =>
(a -> TestName) -> t a -> TestName
showListy ((TestName
"   " forall a. [a] -> [a] -> [a]
++) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Show a => a -> TestName
show) (forall (t :: * -> *) a. Foldable t => t a -> [a]
toList forall a b. (a -> b) -> a -> b
$ Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL)
        forall a. [a] -> [a] -> [a]
++ TestName
"total deposits "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (forall era.
EraTxBody era =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalDepositsTxBody PParams era
currPP CertState era
oldCertState (Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL))
        forall a. [a] -> [a] -> [a]
++ TestName
"\ntotal refunds "
        forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show (forall era.
EraTxBody era =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalRefundsTxBody PParams era
currPP CertState era
oldCertState (Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL))

-- If we are not at an Epoch Boundary (i.e. epoch source == epoch target)
-- then the total rewards should change only by withdrawals
checkWithdrawalBound ::
  EraGen era => SourceSignalTarget (CHAIN era) -> Property
checkWithdrawalBound :: forall era.
EraGen era =>
SourceSignalTarget (CHAIN era) -> Property
checkWithdrawalBound SourceSignalTarget {State (CHAIN era)
source :: State (CHAIN era)
source :: forall a. SourceSignalTarget a -> State a
source, Signal (CHAIN era)
signal :: Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal, State (CHAIN era)
target :: State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"checkWithdrawalBound" forall a b. (a -> b) -> a -> b
$
    Coin
rewardDelta forall a. (Eq a, Show a) => a -> a -> Property
=== forall era. EraGen era => Block (BHeader MockCrypto) era -> Coin
withdrawals Signal (CHAIN era)
signal
  where
    rewardDelta :: Coin
    rewardDelta :: Coin
rewardDelta =
      forall a. Compactible a => CompactForm a -> a
fromCompact
        (forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (forall era. DState era -> UView (Credential 'Staking) RDPair
rewards forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source))
        forall t. Val t => t -> t -> t
<-> forall a. Compactible a => CompactForm a -> a
fromCompact
          (forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (forall era. DState era -> UView (Credential 'Staking) RDPair
rewards forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> CertState era
lsCertState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
target))

-- | If we are not at an Epoch Boundary, then (Utxo + Deposits)
-- increases by Withdrawals minus Fees (for all transactions in a block)
utxoDepositsIncreaseByFeesWithdrawals ::
  forall era ledger.
  ( ChainProperty era
  , EraGen era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
utxoDepositsIncreaseByFeesWithdrawals :: forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
utxoDepositsIncreaseByFeesWithdrawals SourceSignalTarget {State (CHAIN era)
source :: State (CHAIN era)
source :: forall a. SourceSignalTarget a -> State a
source, Signal (CHAIN era)
signal :: Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal, State (CHAIN era)
target :: State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"utxoDepositsIncreaseByFeesWithdrawals" forall a b. (a -> b) -> a -> b
$
    forall {era}. EraTxOut era => ChainState era -> Coin
circulation State (CHAIN era)
target
      forall t. Val t => t -> t -> t
<-> forall {era}. EraTxOut era => ChainState era -> Coin
circulation State (CHAIN era)
source
      forall a. (Eq a, Show a) => a -> a -> Property
=== forall era. EraGen era => Block (BHeader MockCrypto) era -> Coin
withdrawals Signal (CHAIN era)
signal
        forall t. Val t => t -> t -> t
<-> forall era ledger.
(EraGen era, TestingLedger era ledger) =>
Trace ledger -> Coin
txFees Trace ledger
ledgerTr
  where
    us :: ChainState era -> UTxOState era
us = forall era. LedgerState era -> UTxOState era
lsUTxOState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes
    circulation :: ChainState era -> Coin
circulation ChainState era
chainSt =
      let UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u, utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d} = forall {era}. ChainState era -> UTxOState era
us ChainState era
chainSt
       in forall era. EraTxOut era => UTxO era -> Coin
coinBalance UTxO era
u forall t. Val t => t -> t -> t
<+> Coin
d
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
source Signal (CHAIN era)
signal

-- | If we are not at an Epoch Boundary, then (Utxo + Deposits + Fees)
-- increases by sum of withdrawals for all transactions in a block
potsSumIncreaseWithdrawalsPerBlock ::
  (ChainProperty era, EraGen era) =>
  SourceSignalTarget (CHAIN era) ->
  Property
potsSumIncreaseWithdrawalsPerBlock :: forall era.
(ChainProperty era, EraGen era) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseWithdrawalsPerBlock SourceSignalTarget {State (CHAIN era)
source :: State (CHAIN era)
source :: forall a. SourceSignalTarget a -> State a
source, Signal (CHAIN era)
signal :: Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal, State (CHAIN era)
target :: State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample
    TestName
"potsSumIncreaseWithdrawalsPerBlock"
    forall a b. (a -> b) -> a -> b
$ forall {era}. EraTxOut era => ChainState era -> Coin
potsSum State (CHAIN era)
target forall t. Val t => t -> t -> t
<-> forall {era}. EraTxOut era => ChainState era -> Coin
potsSum State (CHAIN era)
source forall a. (Eq a, Show a) => a -> a -> Property
=== forall era. EraGen era => Block (BHeader MockCrypto) era -> Coin
withdrawals Signal (CHAIN era)
signal
  where
    potsSum :: ChainState era -> Coin
potsSum ChainState era
chainSt =
      let UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u, utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d, utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
f} =
            forall era. LedgerState era -> UTxOState era
lsUTxOState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ ChainState era
chainSt
       in forall era. EraTxOut era => UTxO era -> Coin
coinBalance UTxO era
u forall t. Val t => t -> t -> t
<+> Coin
d forall t. Val t => t -> t -> t
<+> Coin
f

-- | If we are not at an Epoch Boundary, then (Utxo + Deposits + Fees)
-- increases by sum of withdrawals in a transaction
potsSumIncreaseWithdrawalsPerTx ::
  forall era ledger.
  ( ChainProperty era
  , EraGen era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
potsSumIncreaseWithdrawalsPerTx :: forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseWithdrawalsPerTx SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"potsSumIncreaseWithdrawalsPerTx" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
sumIncreaseWithdrawals forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    sumIncreaseWithdrawals :: SourceSignalTarget ledger -> Property
    sumIncreaseWithdrawals :: SourceSignalTarget ledger -> Property
sumIncreaseWithdrawals
      SourceSignalTarget
        { source :: forall a. SourceSignalTarget a -> State a
source = LedgerState UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u, utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d, utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
f} CertState era
_
        , signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal ledger
tx
        , target :: forall a. SourceSignalTarget a -> State a
target = LedgerState UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u', utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d', utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
f'} CertState era
_
        } =
        forall prop. Testable prop => prop -> Property
property (forall era. EraGen era => Tx era -> Bool
hasFailedScripts Signal ledger
tx)
          forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. (forall era. EraTxOut era => UTxO era -> Coin
coinBalance UTxO era
u' forall t. Val t => t -> t -> t
<+> Coin
d' forall t. Val t => t -> t -> t
<+> Coin
f')
            forall t. Val t => t -> t -> t
<-> (forall era. EraTxOut era => UTxO era -> Coin
coinBalance UTxO era
u forall t. Val t => t -> t -> t
<+> Coin
d forall t. Val t => t -> t -> t
<+> Coin
f)
            forall a. (Eq a, Show a) => a -> a -> Property
=== forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Withdrawals -> Map RewardAccount Coin
unWithdrawals (Signal ledger
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL))

-- | (Utxo + Deposits + Fees) increases by the reward delta
potsSumIncreaseByRewardsPerTx ::
  forall era ledger.
  ( ChainProperty era
  , EraSegWits era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
potsSumIncreaseByRewardsPerTx :: forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseByRewardsPerTx SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"potsSumIncreaseByRewardsPerTx" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map forall {a} {era}.
(State a ~ LedgerState era, EraTxOut era) =>
SourceSignalTarget a -> Property
sumIncreaseRewards forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    sumIncreaseRewards :: SourceSignalTarget a -> Property
sumIncreaseRewards
      SourceSignalTarget
        { source :: forall a. SourceSignalTarget a -> State a
source =
          LedgerState
            UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u, utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d, utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
f}
            CertState {certDState :: forall era. CertState era -> DState era
certDState = DState {dsUnified :: forall era. DState era -> UMap
dsUnified = UMap
umap1}}
        , target :: forall a. SourceSignalTarget a -> State a
target =
          LedgerState
            UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u', utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d', utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
f'}
            CertState {certDState :: forall era. CertState era -> DState era
certDState = DState {dsUnified :: forall era. DState era -> UMap
dsUnified = UMap
umap2}}
        } =
        (forall era. EraTxOut era => UTxO era -> Coin
coinBalance UTxO era
u' forall t. Val t => t -> t -> t
<+> Coin
d' forall t. Val t => t -> t -> t
<+> Coin
f')
          forall t. Val t => t -> t -> t
<-> (forall era. EraTxOut era => UTxO era -> Coin
coinBalance UTxO era
u forall t. Val t => t -> t -> t
<+> Coin
d forall t. Val t => t -> t -> t
<+> Coin
f)
          forall a. (Eq a, Show a) => a -> a -> Property
=== forall a. Compactible a => CompactForm a -> a
UM.fromCompact (forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (UMap -> UView (Credential 'Staking) RDPair
UM.RewDepUView UMap
umap1))
            forall t. Val t => t -> t -> t
<-> forall a. Compactible a => CompactForm a -> a
UM.fromCompact (forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (UMap -> UView (Credential 'Staking) RDPair
UM.RewDepUView UMap
umap2))

-- | The Rewards pot decreases by the sum of withdrawals in a transaction
potsRewardsDecreaseByWithdrawalsPerTx ::
  forall era ledger.
  ( ChainProperty era
  , EraGen era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
potsRewardsDecreaseByWithdrawalsPerTx :: forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
potsRewardsDecreaseByWithdrawalsPerTx SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"potsRewardsDecreaseByWithdrawalsPerTx" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map forall {a} {era} {era}.
(State a ~ LedgerState era, Signal a ~ Tx era, EraGen era) =>
SourceSignalTarget a -> Property
rewardsDecreaseByWithdrawals forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    rewardsSum :: CertState era -> Coin
rewardsSum = forall a. Compactible a => CompactForm a -> a
UM.fromCompact forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. DState era -> UView (Credential 'Staking) RDPair
rewards forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. CertState era -> DState era
certDState
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    rewardsDecreaseByWithdrawals :: SourceSignalTarget a -> Property
rewardsDecreaseByWithdrawals
      SourceSignalTarget
        { source :: forall a. SourceSignalTarget a -> State a
source = LedgerState UTxOState era
_ CertState era
dpstate
        , signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal a
tx
        , target :: forall a. SourceSignalTarget a -> State a
target = LedgerState UTxOState era
_ CertState era
dpstate'
        } =
        let totalRewards :: Coin
totalRewards = forall {era}. CertState era -> Coin
rewardsSum CertState era
dpstate
            totalRewards' :: Coin
totalRewards' = forall {era}. CertState era -> Coin
rewardsSum CertState era
dpstate'
            txWithdrawals :: Coin
txWithdrawals = forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Withdrawals -> Map RewardAccount Coin
unWithdrawals (Signal a
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL))
         in forall prop. Testable prop => [prop] -> Property
conjoin
              [ forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"A transaction should not increase the Rewards pot"
                  (Coin
totalRewards forall a. Ord a => a -> a -> Bool
>= Coin
totalRewards')
              , forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"Withdrawals should be non-negative"
                  (Coin
txWithdrawals forall a. Ord a => a -> a -> Bool
>= Integer -> Coin
Coin Integer
0)
              , forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"Rewards should increase by withdrawals"
                  (forall era. EraGen era => Tx era -> Bool
hasFailedScripts Signal a
tx Bool -> Bool -> Bool
|| Coin
totalRewards forall t. Val t => t -> t -> t
<-> Coin
totalRewards' forall a. Eq a => a -> a -> Bool
== Coin
txWithdrawals)
              ]

-- | Preserve the balance in a transaction, i.e., the sum of the consumed value
-- equals the sum of the created value.
preserveBalance ::
  forall era ledger.
  ( ChainProperty era
  , EraGen era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
preserveBalance :: forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
preserveBalance SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"preserveBalance" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
createdIsConsumed forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
tickedChainSt, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    pp_ :: PParams era
pp_ = (forall a s. Getting a s a -> s -> a
view forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
tickedChainSt

    createdIsConsumed :: SourceSignalTarget ledger -> Property
createdIsConsumed SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State ledger
ledgerSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal ledger
tx, target :: forall a. SourceSignalTarget a -> State a
target = State ledger
ledgerSt'} =
      forall prop. Testable prop => TestName -> prop -> Property
counterexample
        TestName
"preserveBalance created /= consumed ... "
        (Property
failedScripts forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. forall a. (Eq a, ToExpr a) => a -> a -> Property
ediffEq Coin
created Coin
consumed_)
      where
        failedScripts :: Property
failedScripts = forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ forall era. EraGen era => Tx era -> Bool
hasFailedScripts Signal ledger
tx
        LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u}) CertState era
certState = State ledger
ledgerSt
        LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u'}) CertState era
_ = State ledger
ledgerSt'
        txb :: TxBody era
txb = Signal ledger
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
        created :: Coin
created =
          forall era. EraTxOut era => UTxO era -> Coin
coinBalance UTxO era
u'
            forall t. Val t => t -> t -> t
<+> (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL)
            forall t. Val t => t -> t -> t
<+> forall era.
EraTxBody era =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalDepositsTxBody PParams era
pp_ CertState era
certState TxBody era
txb
        consumed_ :: Coin
consumed_ =
          forall era. EraTxOut era => UTxO era -> Coin
coinBalance UTxO era
u
            forall t. Val t => t -> t -> t
<+> forall era.
EraTxBody era =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalRefundsTxBody PParams era
pp_ CertState era
certState TxBody era
txb
            forall t. Val t => t -> t -> t
<+> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Withdrawals -> Map RewardAccount Coin
unWithdrawals (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL))

-- | Preserve balance restricted to TxIns and TxOuts of the Tx
preserveBalanceRestricted ::
  forall era ledger.
  ( ChainProperty era
  , TestingLedger era ledger
  , EraSegWits era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
preserveBalanceRestricted :: forall era ledger.
(ChainProperty era, TestingLedger era ledger, EraSegWits era) =>
SourceSignalTarget (CHAIN era) -> Property
preserveBalanceRestricted SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"preserveBalanceRestricted" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
createdIsConsumed forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
tickedChainSt, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    pp_ :: PParams era
pp_ = (forall a s. Getting a s a -> s -> a
view forall era. EraGov era => Lens' (EpochState era) (PParams era)
curPParamsEpochStateL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) ChainState era
tickedChainSt

    createdIsConsumed :: SourceSignalTarget ledger -> Property
createdIsConsumed
      SourceSignalTarget
        { source :: forall a. SourceSignalTarget a -> State a
source = LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
utxo}) CertState era
certState
        , signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal ledger
tx
        } =
        Coin
inps forall a. (Eq a, Show a) => a -> a -> Property
=== Coin
outs
        where
          txb :: TxBody era
txb = Signal ledger
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL
          inps :: Coin
inps =
            forall era. EraTxOut era => UTxO era -> Coin
coinBalance @era (forall era. UTxO era -> Set TxIn -> UTxO era
txInsFilter UTxO era
utxo (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
inputsTxBodyL))
              forall a. Semigroup a => a -> a -> a
<> forall era.
EraTxBody era =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalRefundsTxBody PParams era
pp_ CertState era
certState TxBody era
txb
              forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Withdrawals -> Map RewardAccount Coin
unWithdrawals (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL))
          outs :: Coin
outs =
            forall era. EraTxOut era => UTxO era -> Coin
coinBalance (forall era. EraTxBody era => TxBody era -> UTxO era
txouts @era TxBody era
txb)
              forall a. Semigroup a => a -> a -> a
<> (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era. EraTxBody era => Lens' (TxBody era) Coin
feeTxBodyL)
              forall a. Semigroup a => a -> a -> a
<> forall era.
EraTxBody era =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalDepositsTxBody PParams era
pp_ CertState era
certState TxBody era
txb

preserveOutputsTx ::
  forall era ledger.
  ( ChainProperty era
  , EraGen era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
preserveOutputsTx :: forall era ledger.
(ChainProperty era, EraGen era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
preserveOutputsTx SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"preserveOutputsTx" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
outputPreserved forall a b. (a -> b) -> a -> b
$
        forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    outputPreserved :: SourceSignalTarget ledger -> Property
outputPreserved
      SourceSignalTarget
        { target :: forall a. SourceSignalTarget a -> State a
target = LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO Map TxIn (TxOut era)
utxo}) CertState era
_
        , signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal ledger
tx
        } =
        let UTxO Map TxIn (TxOut era)
outs = forall era. EraTxBody era => TxBody era -> UTxO era
txouts @era (Signal ledger
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL)
         in forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$
              forall era. EraGen era => Tx era -> Bool
hasFailedScripts Signal ledger
tx
                forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"TxOuts are not a subset of UTxO" (Map TxIn (TxOut era)
outs forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
`Map.isSubmapOf` Map TxIn (TxOut era)
utxo)

canRestrictUTxO ::
  forall era ledger.
  ( ChainProperty era
  , EraSegWits era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
canRestrictUTxO :: forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
canRestrictUTxO SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"canRestrictUTxO" forall a b. (a -> b) -> a -> b
$
    forall prop. Testable prop => [prop] -> Property
conjoin forall a b. (a -> b) -> a -> b
$
      forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
        SourceSignalTarget ledger -> SourceSignalTarget ledger -> Property
outputPreserved
        (forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTrFull)
        (forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTrRestr)
  where
    (ChainState era
_, Trace ledger
ledgerTrFull) = forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    (UTxO Map TxIn (TxOut era)
irrelevantUTxO, Trace ledger
ledgerTrRestr) =
      forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (UTxO era, Trace ledger)
ledgerTraceFromBlockWithRestrictedUTxO @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    outputPreserved :: SourceSignalTarget ledger -> SourceSignalTarget ledger -> Property
outputPreserved
      SourceSignalTarget {target :: forall a. SourceSignalTarget a -> State a
target = LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO Map TxIn (TxOut era)
uFull}) CertState era
_}
      SourceSignalTarget {target :: forall a. SourceSignalTarget a -> State a
target = LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO Map TxIn (TxOut era)
uRestr}) CertState era
_} =
        forall prop. Testable prop => TestName -> prop -> Property
counterexample
          ([TestName] -> TestName
unlines [TestName
"non-disjoint:", forall a. Show a => a -> TestName
show Map TxIn (TxOut era)
uRestr, forall a. Show a => a -> TestName
show Map TxIn (TxOut era)
irrelevantUTxO])
          (Map TxIn (TxOut era)
uRestr forall k a b. Ord k => Map k a -> Map k b -> Bool
`Map.disjoint` Map TxIn (TxOut era)
irrelevantUTxO)
          forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Map TxIn (TxOut era)
uFull
            forall a. (Eq a, Show a) => a -> a -> Property
=== (Map TxIn (TxOut era)
uRestr forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map TxIn (TxOut era)
irrelevantUTxO)

withdrawals ::
  forall era.
  EraGen era =>
  Block (BHeader MockCrypto) era ->
  Coin
withdrawals :: forall era. EraGen era => Block (BHeader MockCrypto) era -> Coin
withdrawals (UnserialisedBlock BHeader MockCrypto
_ TxSeq era
txseq) =
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl'
    ( \Coin
c Tx era
tx ->
        let wdrls :: Map RewardAccount Coin
wdrls = Withdrawals -> Map RewardAccount Coin
unWithdrawals forall a b. (a -> b) -> a -> b
$ Tx era
tx forall s a. s -> Getting a s a -> a
^. forall era. EraTx era => Lens' (Tx era) (TxBody era)
bodyTxL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL
         in if forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
tx then Coin
c else Coin
c forall a. Semigroup a => a -> a -> a
<> forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map RewardAccount Coin
wdrls
    )
    (Integer -> Coin
Coin Integer
0)
    forall a b. (a -> b) -> a -> b
$ forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq @era TxSeq era
txseq

txFees ::
  forall era ledger.
  (EraGen era, TestingLedger era ledger) =>
  Trace ledger ->
  Coin
txFees :: forall era ledger.
(EraGen era, TestingLedger era ledger) =>
Trace ledger -> Coin
txFees Trace ledger
ledgerTr =
  forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' forall {a} {era}.
(State a ~ LedgerState era, Signal a ~ Tx era, EraGen era) =>
Coin -> SourceSignalTarget a -> Coin
f (Integer -> Coin
Coin Integer
0) (forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr)
  where
    f :: Coin -> SourceSignalTarget a -> Coin
f
      Coin
c
      SourceSignalTarget
        { source :: forall a. SourceSignalTarget a -> State a
source = LedgerState UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
utxo} CertState era
_
        , signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal a
tx
        } = Coin
c forall a. Semigroup a => a -> a -> a
<> forall era. EraGen era => Tx era -> UTxO era -> Coin
feeOrCollateral Signal a
tx UTxO era
utxo

-- | Check that deposits are always non-negative
nonNegativeDeposits ::
  SourceSignalTarget (CHAIN era) ->
  Property
nonNegativeDeposits :: forall era. SourceSignalTarget (CHAIN era) -> Property
nonNegativeDeposits SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt} =
  let es :: EpochState era
es = (forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes) State (CHAIN era)
chainSt
      UTxOState {utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d} = (forall era. LedgerState era -> UTxOState era
lsUTxOState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState) EpochState era
es
   in forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"nonNegativeDeposits: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Coin
d) (Coin
d forall a. Ord a => a -> a -> Bool
>= forall a. Monoid a => a
mempty)

-- | Checks that the fees are non-decreasing when not at an epoch boundary
feesNonDecreasing ::
  SourceSignalTarget (CHAIN era) ->
  Property
feesNonDecreasing :: forall era. SourceSignalTarget (CHAIN era) -> Property
feesNonDecreasing SourceSignalTarget {State (CHAIN era)
source :: State (CHAIN era)
source :: forall a. SourceSignalTarget a -> State a
source, State (CHAIN era)
target :: State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target} =
  forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"feesNonDecreasing: " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> TestName
show (forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
source) forall a. Semigroup a => a -> a -> a
<> TestName
" <= " forall a. Semigroup a => a -> a -> a
<> forall a. Show a => a -> TestName
show (forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
target)) forall a b. (a -> b) -> a -> b
$
    forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
source forall a. Ord a => a -> a -> Bool
<= forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
target
  where
    fees_ :: ChainState era -> Coin
fees_ ChainState era
chainSt =
      let UTxOState {utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
fees} =
            forall era. LedgerState era -> UTxOState era
lsUTxOState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes forall a b. (a -> b) -> a -> b
$ ChainState era
chainSt
       in Coin
fees

sameEpoch ::
  forall era.
  SourceSignalTarget (CHAIN era) ->
  Bool
sameEpoch :: forall era. SourceSignalTarget (CHAIN era) -> Bool
sameEpoch SourceSignalTarget {State (CHAIN era)
source :: State (CHAIN era)
source :: forall a. SourceSignalTarget a -> State a
source, State (CHAIN era)
target :: State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target} =
  forall {era}. ChainState era -> EpochNo
epoch State (CHAIN era)
source forall a. Eq a => a -> a -> Bool
== forall {era}. ChainState era -> EpochNo
epoch State (CHAIN era)
target
  where
    epoch :: ChainState era -> EpochNo
epoch = forall era. NewEpochState era -> EpochNo
nesEL forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. ChainState era -> NewEpochState era
chainNes