{-# 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.Core
import Cardano.Ledger.Keys (KeyHash, KeyRole (StakePool))
import Cardano.Ledger.SafeHash (hashAnnotated)
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.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 (EraCrypto era)) 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 c) Coin -> KeyHash 'StakePool c -> String
infoRetire :: forall c.
Map (KeyHash 'StakePool c) Coin -> KeyHash 'StakePool c -> TestName
infoRetire Map (KeyHash 'StakePool c) Coin
deposits KeyHash 'StakePool c
keyhash = forall (c :: KeyRole) x. KeyHash c x -> TestName
showKeyHash KeyHash 'StakePool c
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 c
keyhash Map (KeyHash 'StakePool c) 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) c. Credential x c -> TestName
showCred) forall a. Show a => a -> TestName
show (forall c k v. UView c k v -> Map k v
UM.unUnify UView (EraCrypto era) (Credential 'Staking (EraCrypto era)) 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) c. Credential x c -> TestName
showCred) forall a. Show a => a -> TestName
show (forall c k v. UView c k v -> Map k v
UM.unUnify UView (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
newRAs)
          , TestName
"\nRetiring pools before update\n"
          , forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap (forall c.
Map (KeyHash 'StakePool c) Coin -> KeyHash 'StakePool c -> TestName
infoRetire Map (KeyHash 'StakePool (EraCrypto era)) Coin
oldPoolDeposit) forall a. Show a => a -> TestName
show Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
oldRetire
          , TestName
"\nRetiring pools after update\n"
          , forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap (forall c.
Map (KeyHash 'StakePool c) Coin -> KeyHash 'StakePool c -> TestName
infoRetire Map (KeyHash 'StakePool (EraCrypto era)) Coin
newPoolDeposit) forall a. Show a => a -> TestName
show Map (KeyHash 'StakePool (EraCrypto era)) EpochNo
newRetire
          , TestName
"\nMIR\n"
          , forall c. InstantaneousRewards c -> TestName
showIR InstantaneousRewards (EraCrypto era)
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 (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era)) Coin
unRegMirTre)
          , TestName
"\n\nPools Retiring This epoch\n"
          , forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap
              (forall c.
Map (KeyHash 'StakePool c) Coin -> KeyHash 'StakePool c -> TestName
infoRetire Map (KeyHash 'StakePool (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era))
ru' = forall era.
NewEpochState era -> StrictMaybe (PulsingRewUpdate (EraCrypto era))
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 (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
oldRAs = forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
newRAs = forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 (EraCrypto era)) EpochNo
oldRetire = forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) 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 (EraCrypto era)) EpochNo
newRetire = forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) 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 (EraCrypto era)) Coin
oldPoolDeposit = forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) 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 (EraCrypto era)) Coin
newPoolDeposit = forall era.
PState era -> Map (KeyHash 'StakePool (EraCrypto era)) 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 (EraCrypto era)
mir = forall era. DState era -> InstantaneousRewards (EraCrypto era)
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 (EraCrypto era) -> Coin -> Bool
isRegistered Credential 'Staking (EraCrypto era)
kh Coin
_ = forall k c v. k -> UView c k v -> Bool
UM.member Credential 'Staking (EraCrypto era)
kh UView (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
oldRAs
    (Map (Credential 'Staking (EraCrypto era)) Coin
regMirRes, Map (Credential 'Staking (EraCrypto era)) Coin
unRegMirRes) = forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey Credential 'Staking (EraCrypto era) -> Coin -> Bool
isRegistered (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRReserves InstantaneousRewards (EraCrypto era)
mir)
    (Map (Credential 'Staking (EraCrypto era)) Coin
regMirTre, Map (Credential 'Staking (EraCrypto era)) Coin
unRegMirTre) = forall k a. (k -> a -> Bool) -> Map k a -> (Map k a, Map k a)
Map.partitionWithKey Credential 'Staking (EraCrypto era) -> Coin -> Bool
isRegistered (forall c.
InstantaneousRewards c -> Map (Credential 'Staking c) Coin
iRTreasury InstantaneousRewards (EraCrypto era)
mir)

    rewardUpdateMsgs :: [TestName]
rewardUpdateMsgs = case StrictMaybe (PulsingRewUpdate (EraCrypto era))
ru' of
      StrictMaybe (PulsingRewUpdate (EraCrypto era))
SNothing -> []
      SJust PulsingRewUpdate (EraCrypto era)
ru'' ->
        let (RewardUpdate (EraCrypto era)
ru, Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
_rewevent) = forall a. ShelleyBase a -> a
runShelleyBase (forall c.
PulsingRewUpdate c -> ShelleyBase (RewardUpdate c, RewardEvent c)
completeRupd PulsingRewUpdate (EraCrypto era)
ru'')
            regRewards :: Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
regRewards = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\Credential 'Staking (EraCrypto era)
kh Set (Reward (EraCrypto era))
_ -> forall k c v. k -> UView c k v -> Bool
UM.member Credential 'Staking (EraCrypto era)
kh UView (EraCrypto era) (Credential 'Staking (EraCrypto era)) RDPair
oldRAs) (forall c.
RewardUpdate c -> Map (Credential 'Staking c) (Set (Reward c))
rs RewardUpdate (EraCrypto era)
ru)
         in [ TestName
"\n\nSum of new rewards "
            , forall a. Show a => a -> TestName
show (forall c.
ProtVer -> Map (Credential 'Staking c) (Set (Reward c)) -> Coin
sumRewards ProtVer
prevPP (forall c.
RewardUpdate c -> Map (Credential 'Staking c) (Set (Reward c))
rs RewardUpdate (EraCrypto era)
ru))
            , TestName
"\n\nNew rewards "
            , forall a. Show a => a -> TestName
show (forall c.
RewardUpdate c -> Map (Credential 'Staking c) (Set (Reward c))
rs RewardUpdate (EraCrypto era)
ru)
            , TestName
"\n\nSum of new registered rewards "
            , forall a. Show a => a -> TestName
show (forall c.
ProtVer -> Map (Credential 'Staking c) (Set (Reward c)) -> Coin
sumRewards ProtVer
prevPP Map
  (Credential 'Staking (EraCrypto era))
  (Set (Reward (EraCrypto era)))
regRewards)
            , TestName
"\n\nChange in Fees "
            , forall a. Show a => a -> TestName
show (forall c. RewardUpdate c -> DeltaCoin
deltaF RewardUpdate (EraCrypto era)
ru)
            , TestName
"\n\nChange in Treasury "
            , forall a. Show a => a -> TestName
show (forall c. RewardUpdate c -> DeltaCoin
deltaT RewardUpdate (EraCrypto era)
ru)
            , TestName
"\n\nChange in Reserves "
            , forall a. Show a => a -> TestName
show (forall c. RewardUpdate c -> DeltaCoin
deltaR RewardUpdate (EraCrypto era)
ru)
            , TestName
"\n\nNet effect of reward update "
            , forall a. Show a => a -> TestName
show forall a b. (a -> b) -> a -> b
$
                forall c. RewardUpdate c -> DeltaCoin
deltaT RewardUpdate (EraCrypto era)
ru
                  forall a. Semigroup a => a -> a -> a
<> forall c. RewardUpdate c -> DeltaCoin
deltaF RewardUpdate (EraCrypto era)
ru
                  forall a. Semigroup a => a -> a -> a
<> forall c. RewardUpdate c -> DeltaCoin
deltaR RewardUpdate (EraCrypto era)
ru
                  forall a. Semigroup a => a -> a -> a
<> Coin -> DeltaCoin
toDeltaCoin (forall c.
ProtVer -> Map (Credential 'Staking c) (Set (Reward c)) -> Coin
sumRewards ProtVer
prevPP (forall c.
RewardUpdate c -> Map (Credential 'Staking c) (Set (Reward c))
rs RewardUpdate (EraCrypto era)
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 index c.
(HashAnnotated x index c, HashAlgorithm (HASH c)) =>
x -> SafeHash c index
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]
++ forall c. Withdrawals c -> 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 (EraCrypto era))
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 (EraCrypto era)) era -> Coin
withdrawals Signal (CHAIN era)
signal
  where
    rewardDelta :: Coin
    rewardDelta :: Coin
rewardDelta =
      forall a. Compactible a => CompactForm a -> a
fromCompact
        (forall c k. UView c k RDPair -> CompactForm Coin
sumRewardsUView (forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 c k. UView c k RDPair -> CompactForm Coin
sumRewardsUView (forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era)) 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 (EraCrypto era)) 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 (forall c. Withdrawals c -> Map (RewardAcnt c) 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 (EraCrypto era))
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 (EraCrypto era)) 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 (EraCrypto era)
dsUnified = UMap (EraCrypto era)
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 (EraCrypto era)
dsUnified = UMap (EraCrypto era)
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 c k. UView c k RDPair -> CompactForm Coin
sumRewardsUView (forall c. UMap c -> UView c (Credential 'Staking c) RDPair
UM.RewDepUView UMap (EraCrypto era)
umap1))
            forall t. Val t => t -> t -> t
<-> forall a. Compactible a => CompactForm a -> a
UM.fromCompact (forall c k. UView c k RDPair -> CompactForm Coin
sumRewardsUView (forall c. UMap c -> UView c (Credential 'Staking c) RDPair
UM.RewDepUView UMap (EraCrypto era)
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}.
(Signal a ~ Tx era, State a ~ LedgerState 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 c k. UView c k RDPair -> CompactForm Coin
sumRewardsUView forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era.
DState era
-> UView
     (EraCrypto era) (Credential 'Staking (EraCrypto era)) 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 (EraCrypto era)) 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 (forall c. Withdrawals c -> Map (RewardAcnt c) 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 (EraCrypto era))
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 (EraCrypto era)) 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 (forall c. Withdrawals c -> Map (RewardAcnt c) Coin
unWithdrawals (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Withdrawals (EraCrypto era))
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 (EraCrypto era)) 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 (EraCrypto era)) -> 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 (EraCrypto era)))
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 (forall c. Withdrawals c -> Map (RewardAcnt c) Coin
unWithdrawals (TxBody era
txb forall s a. s -> Getting a s a -> a
^. forall era.
EraTxBody era =>
Lens' (TxBody era) (Withdrawals (EraCrypto era))
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 (EraCrypto era)) 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 (EraCrypto era)) (TxOut era)
utxo}) CertState era
_
        , signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal ledger
tx
        } =
        let UTxO Map (TxIn (EraCrypto era)) (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 (EraCrypto era)) (TxOut era)
outs forall k a. (Ord k, Eq a) => Map k a -> Map k a -> Bool
`Map.isSubmapOf` Map (TxIn (EraCrypto era)) (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 (EraCrypto era)) era
-> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
chainSt Signal (CHAIN era)
block
    (UTxO Map (TxIn (EraCrypto era)) (TxOut era)
irrelevantUTxO, Trace ledger
ledgerTrRestr) =
      forall era ledger.
(ChainProperty era, EraSegWits era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader (EraCrypto era)) 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 (EraCrypto era)) (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 (EraCrypto era)) (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 (EraCrypto era)) (TxOut era)
uRestr, forall a. Show a => a -> TestName
show Map (TxIn (EraCrypto era)) (TxOut era)
irrelevantUTxO])
          (Map (TxIn (EraCrypto era)) (TxOut era)
uRestr forall k a b. Ord k => Map k a -> Map k b -> Bool
`Map.disjoint` Map (TxIn (EraCrypto era)) (TxOut era)
irrelevantUTxO)
          forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Map (TxIn (EraCrypto era)) (TxOut era)
uFull
            forall a. (Eq a, Show a) => a -> a -> Property
=== (Map (TxIn (EraCrypto era)) (TxOut era)
uRestr forall k a. Ord k => Map k a -> Map k a -> Map k a
`Map.union` Map (TxIn (EraCrypto era)) (TxOut era)
irrelevantUTxO)

withdrawals ::
  forall era.
  EraGen era =>
  Block (BHeader (EraCrypto era)) era ->
  Coin
withdrawals :: forall era.
EraGen era =>
Block (BHeader (EraCrypto era)) era -> Coin
withdrawals (UnserialisedBlock BHeader (EraCrypto era)
_ 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 (RewardAcnt (EraCrypto era)) Coin
wdrls = forall c. Withdrawals c -> Map (RewardAcnt c) 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 (EraCrypto era))
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 (RewardAcnt (EraCrypto era)) 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}.
(Signal a ~ Tx era, State a ~ LedgerState 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