{-# 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 Cardano.Ledger.BaseTypes (StrictMaybe (..))
import Cardano.Ledger.Block (
  Block (..),
  bbody,
 )
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 (..),
  UTxOState (..),
  completeRupd,
  curPParamsEpochStateL,
  deltaF,
  deltaR,
  deltaT,
  esLStateL,
  lsCertStateL,
  nesEsL,
  prevPParamsEpochStateL,
  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.Shelley.State
import Cardano.Ledger.UMap (sumRewardsUView)
import qualified Cardano.Ledger.UMap as UM
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.Rules.TestChain (
  TestingLedger,
  forAllChainTrace,
  ledgerTraceFromBlock,
  ledgerTraceFromBlockWithRestrictedUTxO,
  longTraceLen,
 )
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
  , EraStake era
  , TestingLedger era ledger
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  , GovState era ~ ShelleyGovState era
  ) =>
  Int ->
  TestTree
tests :: forall era ledger.
(EraGen era, EraStake era, TestingLedger era ledger,
 ChainProperty era, HasTrace (CHAIN era) (GenEnv MockCrypto era),
 GovState era ~ ShelleyGovState era) =>
Int -> TestTree
tests Int
n =
  TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
TQC.testProperty
    TestName
"total amount of Ada is preserved (Chain)"
    (Property -> Property
forall prop. Testable prop => prop -> Property
noShrinking (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Int -> Property -> Property
forall prop. Testable prop => Int -> prop -> Property
withMaxSuccess Int
n (forall era ledger.
(EraGen era, EraStake era, TestingLedger era ledger,
 ChainProperty era, HasTrace (CHAIN era) (GenEnv MockCrypto era),
 GovState era ~ ShelleyGovState era) =>
Property
adaPreservationProps @era @ledger))

-- | Various preservation properties
adaPreservationProps ::
  forall era ledger.
  ( EraGen era
  , EraStake era
  , TestingLedger era ledger
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  , GovState era ~ ShelleyGovState era
  ) =>
  Property
adaPreservationProps :: forall era ledger.
(EraGen era, EraStake era, TestingLedger era ledger,
 ChainProperty era, HasTrace (CHAIN era) (GenEnv MockCrypto era),
 GovState era ~ ShelleyGovState era) =>
Property
adaPreservationProps =
  forall era prop.
(EraGen era, EraGov era, EraStake era, Testable prop,
 HasTrace (CHAIN era) (GenEnv MockCrypto era)) =>
Word64 -> Constants -> (Trace (CHAIN era) -> prop) -> Property
forAllChainTrace @era Word64
longTraceLen Constants
defaultConstants ((Trace (CHAIN era) -> Property) -> Property)
-> (Trace (CHAIN era) -> Property) -> Property
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 = Trace (CHAIN era) -> [SourceSignalTarget (CHAIN era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (CHAIN era)
tr
        noEpochBoundarySsts :: [SourceSignalTarget (CHAIN era)]
noEpochBoundarySsts = (SourceSignalTarget (CHAIN era) -> Bool)
-> [SourceSignalTarget (CHAIN era)]
-> [SourceSignalTarget (CHAIN era)]
forall a. (a -> Bool) -> [a] -> [a]
filter SourceSignalTarget (CHAIN era) -> Bool
forall era. SourceSignalTarget (CHAIN era) -> Bool
sameEpoch [SourceSignalTarget (CHAIN era)]
ssts
        justBoundarySsts :: [SourceSignalTarget (CHAIN era)]
justBoundarySsts = (SourceSignalTarget (CHAIN era) -> Bool)
-> [SourceSignalTarget (CHAIN era)]
-> [SourceSignalTarget (CHAIN era)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (SourceSignalTarget (CHAIN era) -> Bool)
-> SourceSignalTarget (CHAIN era)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SourceSignalTarget (CHAIN era) -> Bool
forall era. SourceSignalTarget (CHAIN era) -> Bool
sameEpoch) [SourceSignalTarget (CHAIN era)]
ssts

    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property)
-> ([[Property]] -> [Property]) -> [[Property]] -> Property
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Property]] -> [Property]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[Property]] -> Property) -> [[Property]] -> Property
forall a b. (a -> b) -> a -> b
$
      [ -- preservation properties
        (SourceSignalTarget (CHAIN era) -> Int -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Int] -> [Property]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (forall era.
(EraSegWits era, GovState era ~ ShelleyGovState era, EraGov era,
 EraCertState era) =>
SourceSignalTarget (CHAIN era) -> Int -> Property
checkPreservation @era) [SourceSignalTarget (CHAIN era)]
justBoundarySsts [Int
0 ..]
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
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
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseByRewardsPerTx @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
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
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
preserveBalanceRestricted @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
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
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
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
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
SourceSignalTarget (CHAIN era) -> Property
canRestrictUTxO @era @ledger) [SourceSignalTarget (CHAIN era)]
ssts
      , -- well formed deposits
        (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
forall era. SourceSignalTarget (CHAIN era) -> Property
nonNegativeDeposits [SourceSignalTarget (CHAIN era)]
ssts
      , -- non-epoch-boundary preservation properties
        (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
forall era.
EraGen era =>
SourceSignalTarget (CHAIN era) -> Property
checkWithdrawalBound [SourceSignalTarget (CHAIN era)]
noEpochBoundarySsts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
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
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
forall era.
(ChainProperty era, EraGen era) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseWithdrawalsPerBlock [SourceSignalTarget (CHAIN era)]
noEpochBoundarySsts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (CHAIN era) -> Property
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 = KeyHash 'StakePool -> TestName
forall (x :: KeyRole). KeyHash x -> TestName
showKeyHash KeyHash 'StakePool
keyhash TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
extra
  where
    extra :: TestName
extra = case KeyHash 'StakePool -> Map (KeyHash 'StakePool) Coin -> Maybe Coin
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
" (" TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Coin -> TestName
forall a. Show a => a -> TestName
show Coin
coin TestName -> TestName -> TestName
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
  , EraCertState era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Int ->
  Property
checkPreservation :: forall era.
(EraSegWits era, GovState era ~ ShelleyGovState era, EraGov era,
 EraCertState era) =>
SourceSignalTarget (CHAIN era) -> Int -> Property
checkPreservation 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, Signal (CHAIN era)
signal :: Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal} Int
count =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
    ( [TestName] -> TestName
forall a. Monoid a => [a] -> a
mconcat
        ( [ TestName
"\ncount = " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Int -> TestName
forall a. Show a => a -> TestName
show Int
count TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\n"
          , TestName -> AdaPots -> TestName -> AdaPots -> TestName
compareAdaPots TestName
"before" (ChainState era -> AdaPots
forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
ChainState era -> AdaPots
totalAdaPots State (CHAIN era)
ChainState era
source) TestName
"after" (ChainState era -> AdaPots
forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
ChainState era -> AdaPots
totalAdaPots State (CHAIN era)
ChainState era
target)
          , TestName
"\n\nTotal lovelace before block\n"
          , Coin -> TestName
forall a. Show a => a -> TestName
show Coin
sourceTotal
          , TestName
"\n\nTotal lovelace after block\n"
          , Coin -> TestName
forall a. Show a => a -> TestName
show Coin
targetTotal
          , TestName
"\n\nEpoch before block\n"
          , EpochNo -> TestName
forall a. Show a => a -> TestName
show (NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (NewEpochState era -> EpochNo)
-> (State (CHAIN era) -> NewEpochState era)
-> State (CHAIN era)
-> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (CHAIN era) -> NewEpochState era
ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes (State (CHAIN era) -> EpochNo) -> State (CHAIN era) -> EpochNo
forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source)
          , TestName
"\n\nEpoch after block\n"
          , EpochNo -> TestName
forall a. Show a => a -> TestName
show (NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (NewEpochState era -> EpochNo)
-> (State (CHAIN era) -> NewEpochState era)
-> State (CHAIN era)
-> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (CHAIN era) -> NewEpochState era
ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes (State (CHAIN era) -> EpochNo) -> State (CHAIN era) -> EpochNo
forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
target)
          , TestName
"\n\nCurrent protocol parameters\n"
          , PParams era -> TestName
forall a. Show a => a -> TestName
show PParams era
currPP
          , TestName
"\nReward Accounts before update\n"
          , (Credential 'Staking -> TestName)
-> (RDPair -> TestName)
-> Map (Credential 'Staking) RDPair
-> TestName
forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap (Int -> TestName -> TestName
forall a. Int -> [a] -> [a]
take Int
10 (TestName -> TestName)
-> (Credential 'Staking -> TestName)
-> Credential 'Staking
-> TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Credential 'Staking -> TestName
forall (x :: KeyRole). Credential x -> TestName
showCred) RDPair -> TestName
forall a. Show a => a -> TestName
show (UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall k v. UView k v -> Map k v
UM.unUnify UView (Credential 'Staking) RDPair
oldRAs)
          , TestName
"\nReward Accounts after update\n"
          , (Credential 'Staking -> TestName)
-> (RDPair -> TestName)
-> Map (Credential 'Staking) RDPair
-> TestName
forall t1 t2.
(t1 -> TestName) -> (t2 -> TestName) -> Map t1 t2 -> TestName
showMap (Int -> TestName -> TestName
forall a. Int -> [a] -> [a]
take Int
10 (TestName -> TestName)
-> (Credential 'Staking -> TestName)
-> Credential 'Staking
-> TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Credential 'Staking -> TestName
forall (x :: KeyRole). Credential x -> TestName
showCred) RDPair -> TestName
forall a. Show a => a -> TestName
show (UView (Credential 'Staking) RDPair
-> Map (Credential 'Staking) RDPair
forall k v. UView k v -> Map k v
UM.unUnify UView (Credential 'Staking) RDPair
newRAs)
          , TestName
"\nRetiring pools before update\n"
          , (KeyHash 'StakePool -> TestName)
-> (EpochNo -> TestName)
-> Map (KeyHash 'StakePool) EpochNo
-> TestName
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) EpochNo -> TestName
forall a. Show a => a -> TestName
show Map (KeyHash 'StakePool) EpochNo
oldRetire
          , TestName
"\nRetiring pools after update\n"
          , (KeyHash 'StakePool -> TestName)
-> (EpochNo -> TestName)
-> Map (KeyHash 'StakePool) EpochNo
-> TestName
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) EpochNo -> TestName
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 "
          , Coin -> TestName
forall a. Show a => a -> TestName
show (Map (Credential 'Staking) Coin -> Coin
forall m. Monoid m => Map (Credential 'Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
regMirRes)
          , TestName
"\n\nUnregistered Reserves MIR total "
          , Coin -> TestName
forall a. Show a => a -> TestName
show (Map (Credential 'Staking) Coin -> Coin
forall m. Monoid m => Map (Credential 'Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
unRegMirRes)
          , TestName
"\n\nRegistered Treasury MIR total "
          , Coin -> TestName
forall a. Show a => a -> TestName
show (Map (Credential 'Staking) Coin -> Coin
forall m. Monoid m => Map (Credential 'Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
regMirTre)
          , TestName
"\n\nUnregistered Treasury MIR total "
          , Coin -> TestName
forall a. Show a => a -> TestName
show (Map (Credential 'Staking) Coin -> Coin
forall m. Monoid m => Map (Credential 'Staking) m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map (Credential 'Staking) Coin
unRegMirTre)
          , TestName
"\n\nPools Retiring This epoch\n"
          , (KeyHash 'StakePool -> TestName)
-> (EpochNo -> TestName)
-> Map (KeyHash 'StakePool) EpochNo
-> TestName
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)
              EpochNo -> TestName
forall a. Show a => a -> TestName
show
              ((EpochNo -> Bool)
-> Map (KeyHash 'StakePool) EpochNo
-> Map (KeyHash 'StakePool) EpochNo
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter (\EpochNo
e -> EpochNo
e EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
== (NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (NewEpochState era -> EpochNo)
-> (State (CHAIN era) -> NewEpochState era)
-> State (CHAIN era)
-> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (CHAIN era) -> NewEpochState era
ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes (State (CHAIN era) -> EpochNo) -> State (CHAIN era) -> EpochNo
forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
target)) Map (KeyHash 'StakePool) EpochNo
oldRetire)
          ]
            [TestName] -> [TestName] -> [TestName]
forall a. [a] -> [a] -> [a]
++ [TestName]
obligationMsgs
            [TestName] -> [TestName] -> [TestName]
forall a. [a] -> [a] -> [a]
++ [TestName]
rewardUpdateMsgs
            [TestName] -> [TestName] -> [TestName]
forall a. [a] -> [a] -> [a]
++ [TestName
"\n\ntransactions"]
            [TestName] -> [TestName] -> [TestName]
forall a. [a] -> [a] -> [a]
++ [TestName]
txs
        )
    )
    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ Coin
sourceTotal Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Coin
targetTotal
  where
    sourceTotal :: Coin
sourceTotal = ChainState era -> Coin
forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
ChainState era -> Coin
totalAda State (CHAIN era)
ChainState era
source
    targetTotal :: Coin
targetTotal = ChainState era -> Coin
forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
ChainState era -> Coin
totalAda State (CHAIN era)
ChainState era
target

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

    ru' :: StrictMaybe PulsingRewUpdate
ru' = NewEpochState era -> StrictMaybe PulsingRewUpdate
forall era. NewEpochState era -> StrictMaybe PulsingRewUpdate
nesRu (NewEpochState era -> StrictMaybe PulsingRewUpdate)
-> (State (CHAIN era) -> NewEpochState era)
-> State (CHAIN era)
-> StrictMaybe PulsingRewUpdate
forall b c a. (b -> c) -> (a -> b) -> a -> c
. State (CHAIN era) -> NewEpochState era
ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes (State (CHAIN era) -> StrictMaybe PulsingRewUpdate)
-> State (CHAIN era) -> StrictMaybe PulsingRewUpdate
forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source
    lsOld :: LedgerState era
lsOld = EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (State (CHAIN era) -> EpochState era)
-> State (CHAIN era)
-> LedgerState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes (State (CHAIN era) -> LedgerState era)
-> State (CHAIN era) -> LedgerState era
forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
source
    lsNew :: LedgerState era
lsNew = EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (State (CHAIN era) -> EpochState era)
-> State (CHAIN era)
-> LedgerState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes (State (CHAIN era) -> LedgerState era)
-> State (CHAIN era) -> LedgerState era
forall a b. (a -> b) -> a -> b
$ State (CHAIN era)
target
    oldRAs :: UView (Credential 'Staking) RDPair
oldRAs = DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards (DState era -> UView (Credential 'Staking) RDPair)
-> DState era -> UView (Credential 'Staking) RDPair
forall a b. (a -> b) -> a -> b
$ LedgerState era
lsOld LedgerState era
-> Getting (DState era) (LedgerState era) (DState era)
-> DState era
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const (DState era) (CertState era))
-> LedgerState era -> Const (DState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (DState era) (CertState era))
 -> LedgerState era -> Const (DState era) (LedgerState era))
-> ((DState era -> Const (DState era) (DState era))
    -> CertState era -> Const (DState era) (CertState era))
-> Getting (DState era) (LedgerState era) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const (DState era) (DState era))
-> CertState era -> Const (DState era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
    newRAs :: UView (Credential 'Staking) RDPair
newRAs = DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards (DState era -> UView (Credential 'Staking) RDPair)
-> DState era -> UView (Credential 'Staking) RDPair
forall a b. (a -> b) -> a -> b
$ LedgerState era
lsNew LedgerState era
-> Getting (DState era) (LedgerState era) (DState era)
-> DState era
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const (DState era) (CertState era))
-> LedgerState era -> Const (DState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (DState era) (CertState era))
 -> LedgerState era -> Const (DState era) (LedgerState era))
-> ((DState era -> Const (DState era) (DState era))
    -> CertState era -> Const (DState era) (CertState era))
-> Getting (DState era) (LedgerState era) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const (DState era) (DState era))
-> CertState era -> Const (DState era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
    oldCertState :: CertState era
oldCertState = LedgerState era -> CertState era
forall era. LedgerState era -> CertState era
lsCertState LedgerState era
lsOld
    oldRetire :: Map (KeyHash 'StakePool) EpochNo
oldRetire = LedgerState era
lsOld LedgerState era
-> Getting
     (Map (KeyHash 'StakePool) EpochNo)
     (LedgerState era)
     (Map (KeyHash 'StakePool) EpochNo)
-> Map (KeyHash 'StakePool) EpochNo
forall s a. s -> Getting a s a -> a
^. (CertState era
 -> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era))
-> LedgerState era
-> Const (Map (KeyHash 'StakePool) EpochNo) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era))
 -> LedgerState era
 -> Const (Map (KeyHash 'StakePool) EpochNo) (LedgerState era))
-> ((Map (KeyHash 'StakePool) EpochNo
     -> Const
          (Map (KeyHash 'StakePool) EpochNo)
          (Map (KeyHash 'StakePool) EpochNo))
    -> CertState era
    -> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era))
-> Getting
     (Map (KeyHash 'StakePool) EpochNo)
     (LedgerState era)
     (Map (KeyHash 'StakePool) EpochNo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era
 -> Const (Map (KeyHash 'StakePool) EpochNo) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era
  -> Const (Map (KeyHash 'StakePool) EpochNo) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era))
-> ((Map (KeyHash 'StakePool) EpochNo
     -> Const
          (Map (KeyHash 'StakePool) EpochNo)
          (Map (KeyHash 'StakePool) EpochNo))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) EpochNo) (PState era))
-> (Map (KeyHash 'StakePool) EpochNo
    -> Const
         (Map (KeyHash 'StakePool) EpochNo)
         (Map (KeyHash 'StakePool) EpochNo))
-> CertState era
-> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) EpochNo
 -> Const
      (Map (KeyHash 'StakePool) EpochNo)
      (Map (KeyHash 'StakePool) EpochNo))
-> PState era
-> Const (Map (KeyHash 'StakePool) EpochNo) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) EpochNo
 -> f (Map (KeyHash 'StakePool) EpochNo))
-> PState era -> f (PState era)
psRetiringL
    newRetire :: Map (KeyHash 'StakePool) EpochNo
newRetire = LedgerState era
lsNew LedgerState era
-> Getting
     (Map (KeyHash 'StakePool) EpochNo)
     (LedgerState era)
     (Map (KeyHash 'StakePool) EpochNo)
-> Map (KeyHash 'StakePool) EpochNo
forall s a. s -> Getting a s a -> a
^. (CertState era
 -> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era))
-> LedgerState era
-> Const (Map (KeyHash 'StakePool) EpochNo) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era))
 -> LedgerState era
 -> Const (Map (KeyHash 'StakePool) EpochNo) (LedgerState era))
-> ((Map (KeyHash 'StakePool) EpochNo
     -> Const
          (Map (KeyHash 'StakePool) EpochNo)
          (Map (KeyHash 'StakePool) EpochNo))
    -> CertState era
    -> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era))
-> Getting
     (Map (KeyHash 'StakePool) EpochNo)
     (LedgerState era)
     (Map (KeyHash 'StakePool) EpochNo)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era
 -> Const (Map (KeyHash 'StakePool) EpochNo) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era
  -> Const (Map (KeyHash 'StakePool) EpochNo) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era))
-> ((Map (KeyHash 'StakePool) EpochNo
     -> Const
          (Map (KeyHash 'StakePool) EpochNo)
          (Map (KeyHash 'StakePool) EpochNo))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) EpochNo) (PState era))
-> (Map (KeyHash 'StakePool) EpochNo
    -> Const
         (Map (KeyHash 'StakePool) EpochNo)
         (Map (KeyHash 'StakePool) EpochNo))
-> CertState era
-> Const (Map (KeyHash 'StakePool) EpochNo) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) EpochNo
 -> Const
      (Map (KeyHash 'StakePool) EpochNo)
      (Map (KeyHash 'StakePool) EpochNo))
-> PState era
-> Const (Map (KeyHash 'StakePool) EpochNo) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) EpochNo
 -> f (Map (KeyHash 'StakePool) EpochNo))
-> PState era -> f (PState era)
psRetiringL
    oldPoolDeposit :: Map (KeyHash 'StakePool) Coin
oldPoolDeposit = LedgerState era
lsOld LedgerState era
-> Getting
     (Map (KeyHash 'StakePool) Coin)
     (LedgerState era)
     (Map (KeyHash 'StakePool) Coin)
-> Map (KeyHash 'StakePool) Coin
forall s a. s -> Getting a s a -> a
^. (CertState era
 -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> LedgerState era
-> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
 -> LedgerState era
 -> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Const
          (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
    -> CertState era
    -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> Getting
     (Map (KeyHash 'StakePool) Coin)
     (LedgerState era)
     (Map (KeyHash 'StakePool) Coin)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) Coin) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Const
          (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
-> (Map (KeyHash 'StakePool) Coin
    -> Const
         (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
-> CertState era
-> Const (Map (KeyHash 'StakePool) Coin) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) Coin
 -> Const
      (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
-> PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) Coin
 -> f (Map (KeyHash 'StakePool) Coin))
-> PState era -> f (PState era)
psDepositsL
    newPoolDeposit :: Map (KeyHash 'StakePool) Coin
newPoolDeposit = LedgerState era
lsNew LedgerState era
-> Getting
     (Map (KeyHash 'StakePool) Coin)
     (LedgerState era)
     (Map (KeyHash 'StakePool) Coin)
-> Map (KeyHash 'StakePool) Coin
forall s a. s -> Getting a s a -> a
^. (CertState era
 -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> LedgerState era
-> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
 -> LedgerState era
 -> Const (Map (KeyHash 'StakePool) Coin) (LedgerState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Const
          (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
    -> CertState era
    -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> Getting
     (Map (KeyHash 'StakePool) Coin)
     (LedgerState era)
     (Map (KeyHash 'StakePool) Coin)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) Coin) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) Coin) (CertState era))
-> ((Map (KeyHash 'StakePool) Coin
     -> Const
          (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) Coin) (PState era))
-> (Map (KeyHash 'StakePool) Coin
    -> Const
         (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
-> CertState era
-> Const (Map (KeyHash 'StakePool) Coin) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) Coin
 -> Const
      (Map (KeyHash 'StakePool) Coin) (Map (KeyHash 'StakePool) Coin))
-> PState era -> Const (Map (KeyHash 'StakePool) Coin) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) Coin
 -> f (Map (KeyHash 'StakePool) Coin))
-> PState era -> f (PState era)
psDepositsL

    proposal :: Maybe (PParams era)
proposal = ProposedPPUpdates era
-> PParams era -> Word64 -> Maybe (PParams era)
forall era.
EraPParams era =>
ProposedPPUpdates era
-> PParams era -> Word64 -> Maybe (PParams era)
votedFuturePParams (ShelleyGovState era -> ProposedPPUpdates era
forall era. ShelleyGovState era -> ProposedPPUpdates era
sgsCurProposals (ShelleyGovState era -> ProposedPPUpdates era)
-> (UTxOState era -> ShelleyGovState era)
-> UTxOState era
-> ProposedPPUpdates era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOState era -> GovState era
UTxOState era -> ShelleyGovState era
forall era. UTxOState era -> GovState era
utxosGovState (UTxOState era -> ProposedPPUpdates era)
-> UTxOState era -> ProposedPPUpdates era
forall a b. (a -> b) -> a -> b
$ LedgerState era -> UTxOState era
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"
        , PParams era -> TestName
forall a. Show a => a -> TestName
show PParams era
proposal'
        ]

    mir :: InstantaneousRewards
mir = LedgerState era
lsOld LedgerState era
-> Getting
     InstantaneousRewards (LedgerState era) InstantaneousRewards
-> InstantaneousRewards
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const InstantaneousRewards (CertState era))
-> LedgerState era -> Const InstantaneousRewards (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const InstantaneousRewards (CertState era))
 -> LedgerState era -> Const InstantaneousRewards (LedgerState era))
-> ((InstantaneousRewards
     -> Const InstantaneousRewards InstantaneousRewards)
    -> CertState era -> Const InstantaneousRewards (CertState era))
-> Getting
     InstantaneousRewards (LedgerState era) InstantaneousRewards
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const InstantaneousRewards (DState era))
-> CertState era -> Const InstantaneousRewards (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const InstantaneousRewards (DState era))
 -> CertState era -> Const InstantaneousRewards (CertState era))
-> ((InstantaneousRewards
     -> Const InstantaneousRewards InstantaneousRewards)
    -> DState era -> Const InstantaneousRewards (DState era))
-> (InstantaneousRewards
    -> Const InstantaneousRewards InstantaneousRewards)
-> CertState era
-> Const InstantaneousRewards (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (InstantaneousRewards
 -> Const InstantaneousRewards InstantaneousRewards)
-> DState era -> Const InstantaneousRewards (DState era)
forall era (f :: * -> *).
Functor f =>
(InstantaneousRewards -> f InstantaneousRewards)
-> DState era -> f (DState era)
dsIRewardsL
    isRegistered :: Credential 'Staking -> Coin -> Bool
isRegistered Credential 'Staking
kh Coin
_ = Credential 'Staking -> UView (Credential 'Staking) RDPair -> Bool
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) = (Credential 'Staking -> Coin -> Bool)
-> Map (Credential 'Staking) Coin
-> (Map (Credential 'Staking) Coin, Map (Credential 'Staking) Coin)
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) = (Credential 'Staking -> Coin -> Bool)
-> Map (Credential 'Staking) Coin
-> (Map (Credential 'Staking) Coin, Map (Credential 'Staking) Coin)
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) = ShelleyBase (RewardUpdate, Map (Credential 'Staking) (Set Reward))
-> (RewardUpdate, Map (Credential 'Staking) (Set Reward))
forall a. ShelleyBase a -> a
runShelleyBase (PulsingRewUpdate
-> ShelleyBase
     (RewardUpdate, Map (Credential 'Staking) (Set Reward))
completeRupd PulsingRewUpdate
ru'')
            regRewards :: Map (Credential 'Staking) (Set Reward)
regRewards = (Credential 'Staking -> Set Reward -> Bool)
-> Map (Credential 'Staking) (Set Reward)
-> Map (Credential 'Staking) (Set Reward)
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\Credential 'Staking
kh Set Reward
_ -> Credential 'Staking -> UView (Credential 'Staking) RDPair -> Bool
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 "
            , Coin -> TestName
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 "
            , Map (Credential 'Staking) (Set Reward) -> TestName
forall a. Show a => a -> TestName
show (RewardUpdate -> Map (Credential 'Staking) (Set Reward)
rs RewardUpdate
ru)
            , TestName
"\n\nSum of new registered rewards "
            , Coin -> TestName
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 "
            , DeltaCoin -> TestName
forall a. Show a => a -> TestName
show (RewardUpdate -> DeltaCoin
deltaF RewardUpdate
ru)
            , TestName
"\n\nChange in Treasury "
            , DeltaCoin -> TestName
forall a. Show a => a -> TestName
show (RewardUpdate -> DeltaCoin
deltaT RewardUpdate
ru)
            , TestName
"\n\nChange in Reserves "
            , DeltaCoin -> TestName
forall a. Show a => a -> TestName
show (RewardUpdate -> DeltaCoin
deltaR RewardUpdate
ru)
            , TestName
"\n\nNet effect of reward update "
            , DeltaCoin -> TestName
forall a. Show a => a -> TestName
show (DeltaCoin -> TestName) -> DeltaCoin -> TestName
forall a b. (a -> b) -> a -> b
$
                RewardUpdate -> DeltaCoin
deltaT RewardUpdate
ru
                  DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> RewardUpdate -> DeltaCoin
deltaF RewardUpdate
ru
                  DeltaCoin -> DeltaCoin -> DeltaCoin
forall a. Semigroup a => a -> a -> a
<> RewardUpdate -> DeltaCoin
deltaR RewardUpdate
ru
                  DeltaCoin -> DeltaCoin -> DeltaCoin
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' = StrictSeq (Tx era) -> [Tx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (Tx era) -> [Tx era]) -> StrictSeq (Tx era) -> [Tx era]
forall a b. (a -> b) -> a -> b
$ (forall era. EraSegWits era => TxSeq era -> StrictSeq (Tx era)
fromTxSeq @era (TxSeq era -> StrictSeq (Tx era))
-> (Block (BHeader MockCrypto) era -> TxSeq era)
-> Block (BHeader MockCrypto) era
-> StrictSeq (Tx era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Block (BHeader MockCrypto) era -> TxSeq era
forall h era. Block h era -> TxSeq era
bbody) Block (BHeader MockCrypto) era
Signal (CHAIN era)
signal
    txs :: [TestName]
txs = (Tx era -> Int -> TestName) -> [Tx era] -> [Int] -> [TestName]
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 "
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Int -> TestName
forall a. Show a => a -> TestName
show Int
ix
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
" "
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ SafeHash EraIndependentTxBody -> TestName
forall a. Show a => a -> TestName
show (TxBody era -> SafeHash EraIndependentTxBody
forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated (Tx era
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL))
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\nfee :"
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Coin -> TestName
forall a. Show a => a -> TestName
show (Tx era
tx Tx era -> Getting Coin (Tx era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const Coin (TxBody era))
-> Tx era -> Const Coin (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const Coin (TxBody era))
 -> Tx era -> Const Coin (Tx era))
-> ((Coin -> Const Coin Coin)
    -> TxBody era -> Const Coin (TxBody era))
-> Getting Coin (Tx era) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Coin -> Const Coin Coin) -> TxBody era -> Const Coin (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody era) Coin
feeTxBodyL)
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\nwithdrawals:"
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Withdrawals -> TestName
showWithdrawal (Tx era
tx Tx era -> Getting Withdrawals (Tx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const Withdrawals (TxBody era))
-> Tx era -> Const Withdrawals (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const Withdrawals (TxBody era))
 -> Tx era -> Const Withdrawals (Tx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody era -> Const Withdrawals (TxBody era))
-> Getting Withdrawals (Tx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody era -> Const Withdrawals (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL)
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\ncerts:"
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ (TxCert era -> TestName) -> [TxCert era] -> TestName
forall (t :: * -> *) a.
Foldable t =>
(a -> TestName) -> t a -> TestName
showListy ((TestName
"   " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++) (TestName -> TestName)
-> (TxCert era -> TestName) -> TxCert era -> TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxCert era -> TestName
forall a. Show a => a -> TestName
show) (StrictSeq (TxCert era) -> [TxCert era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (TxCert era) -> [TxCert era])
-> StrictSeq (TxCert era) -> [TxCert era]
forall a b. (a -> b) -> a -> b
$ Tx era
tx Tx era
-> Getting
     (StrictSeq (TxCert era)) (Tx era) (StrictSeq (TxCert era))
-> StrictSeq (TxCert era)
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const (StrictSeq (TxCert era)) (TxBody era))
-> Tx era -> Const (StrictSeq (TxCert era)) (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const (StrictSeq (TxCert era)) (TxBody era))
 -> Tx era -> Const (StrictSeq (TxCert era)) (Tx era))
-> ((StrictSeq (TxCert era)
     -> Const (StrictSeq (TxCert era)) (StrictSeq (TxCert era)))
    -> TxBody era -> Const (StrictSeq (TxCert era)) (TxBody era))
-> Getting
     (StrictSeq (TxCert era)) (Tx era) (StrictSeq (TxCert era))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (StrictSeq (TxCert era)
 -> Const (StrictSeq (TxCert era)) (StrictSeq (TxCert era)))
-> TxBody era -> Const (StrictSeq (TxCert era)) (TxBody era)
forall era.
EraTxBody era =>
Lens' (TxBody era) (StrictSeq (TxCert era))
Lens' (TxBody era) (StrictSeq (TxCert era))
certsTxBodyL)
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"total deposits "
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Coin -> TestName
forall a. Show a => a -> TestName
show (PParams era -> CertState era -> TxBody era -> Coin
forall era.
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalDepositsTxBody PParams era
currPP CertState era
oldCertState (Tx era
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL))
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ TestName
"\ntotal refunds "
        TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Coin -> TestName
forall a. Show a => a -> TestName
show (PParams era -> CertState era -> TxBody era -> Coin
forall era.
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalRefundsTxBody PParams era
currPP CertState era
oldCertState (Tx era
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody 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 :: forall a. SourceSignalTarget a -> State a
source :: State (CHAIN era)
source, Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal :: Signal (CHAIN era)
signal, State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target :: State (CHAIN era)
target} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"checkWithdrawalBound" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    Coin
rewardDelta Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Block (BHeader MockCrypto) era -> Coin
forall era. EraGen era => Block (BHeader MockCrypto) era -> Coin
withdrawals Block (BHeader MockCrypto) era
Signal (CHAIN era)
signal
  where
    rewardDelta :: Coin
    rewardDelta :: Coin
rewardDelta =
      CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact
        (UView (Credential 'Staking) RDPair -> CompactForm Coin
forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards (DState era -> UView (Credential 'Staking) RDPair)
-> DState era -> UView (Credential 'Staking) RDPair
forall a b. (a -> b) -> a -> b
$ (ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes State (CHAIN era)
ChainState era
source) NewEpochState era
-> Getting (DState era) (NewEpochState era) (DState era)
-> DState era
forall s a. s -> Getting a s a -> a
^. (EpochState era -> Const (DState era) (EpochState era))
-> NewEpochState era -> Const (DState era) (NewEpochState era)
forall era (f :: * -> *).
Functor f =>
(EpochState era -> f (EpochState era))
-> NewEpochState era -> f (NewEpochState era)
nesEsL ((EpochState era -> Const (DState era) (EpochState era))
 -> NewEpochState era -> Const (DState era) (NewEpochState era))
-> ((DState era -> Const (DState era) (DState era))
    -> EpochState era -> Const (DState era) (EpochState era))
-> Getting (DState era) (NewEpochState era) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LedgerState era -> Const (DState era) (LedgerState era))
-> EpochState era -> Const (DState era) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era -> Const (DState era) (LedgerState era))
 -> EpochState era -> Const (DState era) (EpochState era))
-> ((DState era -> Const (DState era) (DState era))
    -> LedgerState era -> Const (DState era) (LedgerState era))
-> (DState era -> Const (DState era) (DState era))
-> EpochState era
-> Const (DState era) (EpochState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era -> Const (DState era) (CertState era))
-> LedgerState era -> Const (DState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (DState era) (CertState era))
 -> LedgerState era -> Const (DState era) (LedgerState era))
-> ((DState era -> Const (DState era) (DState era))
    -> CertState era -> Const (DState era) (CertState era))
-> (DState era -> Const (DState era) (DState era))
-> LedgerState era
-> Const (DState era) (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const (DState era) (DState era))
-> CertState era -> Const (DState era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL))
        Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact
          (UView (Credential 'Staking) RDPair -> CompactForm Coin
forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards (DState era -> UView (Credential 'Staking) RDPair)
-> DState era -> UView (Credential 'Staking) RDPair
forall a b. (a -> b) -> a -> b
$ (ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes State (CHAIN era)
ChainState era
target) NewEpochState era
-> Getting (DState era) (NewEpochState era) (DState era)
-> DState era
forall s a. s -> Getting a s a -> a
^. (EpochState era -> Const (DState era) (EpochState era))
-> NewEpochState era -> Const (DState era) (NewEpochState era)
forall era (f :: * -> *).
Functor f =>
(EpochState era -> f (EpochState era))
-> NewEpochState era -> f (NewEpochState era)
nesEsL ((EpochState era -> Const (DState era) (EpochState era))
 -> NewEpochState era -> Const (DState era) (NewEpochState era))
-> ((DState era -> Const (DState era) (DState era))
    -> EpochState era -> Const (DState era) (EpochState era))
-> Getting (DState era) (NewEpochState era) (DState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LedgerState era -> Const (DState era) (LedgerState era))
-> EpochState era -> Const (DState era) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era -> Const (DState era) (LedgerState era))
 -> EpochState era -> Const (DState era) (EpochState era))
-> ((DState era -> Const (DState era) (DState era))
    -> LedgerState era -> Const (DState era) (LedgerState era))
-> (DState era -> Const (DState era) (DState era))
-> EpochState era
-> Const (DState era) (EpochState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era -> Const (DState era) (CertState era))
-> LedgerState era -> Const (DState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (DState era) (CertState era))
 -> LedgerState era -> Const (DState era) (LedgerState era))
-> ((DState era -> Const (DState era) (DState era))
    -> CertState era -> Const (DState era) (CertState era))
-> (DState era -> Const (DState era) (DState era))
-> LedgerState era
-> Const (DState era) (LedgerState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const (DState era) (DState era))
-> CertState era -> Const (DState era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL))

-- | 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 :: forall a. SourceSignalTarget a -> State a
source :: State (CHAIN era)
source, Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal :: Signal (CHAIN era)
signal, State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target :: State (CHAIN era)
target} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"utxoDepositsIncreaseByFeesWithdrawals" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    ChainState era -> Coin
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era) =>
ChainState era -> Coin
circulation State (CHAIN era)
ChainState era
target
      Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> ChainState era -> Coin
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era) =>
ChainState era -> Coin
circulation State (CHAIN era)
ChainState era
source
      Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Block (BHeader MockCrypto) era -> Coin
forall era. EraGen era => Block (BHeader MockCrypto) era -> Coin
withdrawals Block (BHeader MockCrypto) era
Signal (CHAIN era)
signal
        Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Trace ledger -> Coin
forall era ledger.
(EraGen era, TestingLedger era ledger) =>
Trace ledger -> Coin
txFees Trace ledger
ledgerTr
  where
    us :: ChainState era -> UTxOState era
us = LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState (LedgerState era -> UTxOState era)
-> (ChainState era -> LedgerState era)
-> ChainState era
-> UTxOState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (ChainState era -> EpochState era)
-> ChainState era
-> LedgerState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
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} = ChainState era -> UTxOState era
forall {era}. ChainState era -> UTxOState era
us ChainState era
chainSt
       in UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO UTxO era
u Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
d
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
ChainState era
source Block (BHeader MockCrypto) era
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 :: forall a. SourceSignalTarget a -> State a
source :: State (CHAIN era)
source, Signal (CHAIN era)
signal :: forall a. SourceSignalTarget a -> Signal a
signal :: Signal (CHAIN era)
signal, State (CHAIN era)
target :: forall a. SourceSignalTarget a -> State a
target :: State (CHAIN era)
target} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
    TestName
"potsSumIncreaseWithdrawalsPerBlock"
    (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ ChainState era -> Coin
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era) =>
ChainState era -> Coin
potsSum State (CHAIN era)
ChainState era
target Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> ChainState era -> Coin
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era) =>
ChainState era -> Coin
potsSum State (CHAIN era)
ChainState era
source Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Block (BHeader MockCrypto) era -> Coin
forall era. EraGen era => Block (BHeader MockCrypto) era -> Coin
withdrawals Block (BHeader MockCrypto) era
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} =
            LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState (LedgerState era -> UTxOState era)
-> (ChainState era -> LedgerState era)
-> ChainState era
-> UTxOState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (ChainState era -> EpochState era)
-> ChainState era
-> LedgerState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes (ChainState era -> UTxOState era)
-> ChainState era -> UTxOState era
forall a b. (a -> b) -> a -> b
$ ChainState era
chainSt
       in UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO UTxO era
u Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
d Coin -> Coin -> Coin
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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"potsSumIncreaseWithdrawalsPerTx" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget ledger -> Property)
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
sumIncreaseWithdrawals ([SourceSignalTarget ledger] -> [Property])
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace ledger -> [SourceSignalTarget ledger]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
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
_
        } =
        Bool -> Property
forall prop. Testable prop => prop -> Property
property (Tx era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
Signal ledger
tx)
          Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. (UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO UTxO era
u' Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
d' Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
f')
            Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> (UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO UTxO era
u Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
d Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
f)
            Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Map RewardAccount Coin -> Coin
forall m. Monoid m => Map RewardAccount m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Withdrawals -> Map RewardAccount Coin
unWithdrawals (Tx era
Signal ledger
tx Tx era -> Getting Withdrawals (Tx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const Withdrawals (TxBody era))
-> Tx era -> Const Withdrawals (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const Withdrawals (TxBody era))
 -> Tx era -> Const Withdrawals (Tx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody era -> Const Withdrawals (TxBody era))
-> Getting Withdrawals (Tx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody era -> Const Withdrawals (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL))

-- | (Utxo + Deposits + Fees) increases by the reward delta
potsSumIncreaseByRewardsPerTx ::
  forall era ledger.
  ( ChainProperty era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
potsSumIncreaseByRewardsPerTx :: forall era ledger.
(ChainProperty 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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"potsSumIncreaseByRewardsPerTx" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget ledger -> Property)
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
forall {a} {era}.
(State a ~ LedgerState era,
 Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraTxOut era, EraCertState era) =>
SourceSignalTarget a -> Property
sumIncreaseRewards ([SourceSignalTarget ledger] -> [Property])
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace ledger -> [SourceSignalTarget ledger]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
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 era
cState1
        , 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
cState2
        } =
        (UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO UTxO era
u' Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
d' Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
f')
          Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> (UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO UTxO era
u Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
d Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
f)
          Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
UM.fromCompact (UView (Credential 'Staking) RDPair -> CompactForm Coin
forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (UMap -> UView (Credential 'Staking) RDPair
UM.RewDepUView (CertState era
cState1 CertState era -> Getting UMap (CertState era) UMap -> UMap
forall s a. s -> Getting a s a -> a
^. (DState era -> Const UMap (DState era))
-> CertState era -> Const UMap (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const UMap (DState era))
 -> CertState era -> Const UMap (CertState era))
-> ((UMap -> Const UMap UMap)
    -> DState era -> Const UMap (DState era))
-> Getting UMap (CertState era) UMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Const UMap UMap) -> DState era -> Const UMap (DState era)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL)))
            Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
UM.fromCompact (UView (Credential 'Staking) RDPair -> CompactForm Coin
forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (UMap -> UView (Credential 'Staking) RDPair
UM.RewDepUView (CertState era
cState2 CertState era -> Getting UMap (CertState era) UMap -> UMap
forall s a. s -> Getting a s a -> a
^. (DState era -> Const UMap (DState era))
-> CertState era -> Const UMap (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const UMap (DState era))
 -> CertState era -> Const UMap (CertState era))
-> ((UMap -> Const UMap UMap)
    -> DState era -> Const UMap (DState era))
-> Getting UMap (CertState era) UMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (UMap -> Const UMap UMap) -> DState era -> Const UMap (DState era)
forall era (f :: * -> *).
Functor f =>
(UMap -> f UMap) -> DState era -> f (DState era)
dsUnifiedL)))

-- | 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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"potsRewardsDecreaseByWithdrawalsPerTx" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget ledger -> Property)
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
forall {a} {era} {era}.
(Signal a ~ Tx era, State a ~ LedgerState era,
 Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 ProtVerIsInBounds
   "at most"
   era
   8
   (OrdCond (CmpNat (ProtVerLow era) 8) 'True 'True 'False),
 Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraGen era, EraCertState era) =>
SourceSignalTarget a -> Property
rewardsDecreaseByWithdrawals ([SourceSignalTarget ledger] -> [Property])
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace ledger -> [SourceSignalTarget ledger]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    rewardsSum :: CertState era -> Coin
rewardsSum CertState era
certState = CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
UM.fromCompact (CompactForm Coin -> Coin)
-> (DState era -> CompactForm Coin) -> DState era -> Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UView (Credential 'Staking) RDPair -> CompactForm Coin
forall k. UView k RDPair -> CompactForm Coin
sumRewardsUView (UView (Credential 'Staking) RDPair -> CompactForm Coin)
-> (DState era -> UView (Credential 'Staking) RDPair)
-> DState era
-> CompactForm Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. DState era -> UView (Credential 'Staking) RDPair
forall era. DState era -> UView (Credential 'Staking) RDPair
rewards (DState era -> Coin) -> DState era -> Coin
forall a b. (a -> b) -> a -> b
$ CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
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 = CertState era -> Coin
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraCertState era) =>
CertState era -> Coin
rewardsSum CertState era
dpstate
            totalRewards' :: Coin
totalRewards' = CertState era -> Coin
forall {era}.
(Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraCertState era) =>
CertState era -> Coin
rewardsSum CertState era
dpstate'
            txWithdrawals :: Coin
txWithdrawals = Map RewardAccount Coin -> Coin
forall m. Monoid m => Map RewardAccount m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Withdrawals -> Map RewardAccount Coin
unWithdrawals (Signal a
tx Signal a
-> Getting Withdrawals (Signal a) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const Withdrawals (TxBody era))
-> Tx era -> Const Withdrawals (Tx era)
(TxBody era -> Const Withdrawals (TxBody era))
-> Signal a -> Const Withdrawals (Signal a)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const Withdrawals (TxBody era))
 -> Signal a -> Const Withdrawals (Signal a))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody era -> Const Withdrawals (TxBody era))
-> Getting Withdrawals (Signal a) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody era -> Const Withdrawals (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL))
         in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
              [ TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"A transaction should not increase the Rewards pot"
                  (Coin
totalRewards Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
totalRewards')
              , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"Withdrawals should be non-negative"
                  (Coin
txWithdrawals Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Coin
Coin Integer
0)
              , TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
                  TestName
"Rewards should increase by withdrawals"
                  (Tx era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
Signal a
tx Bool -> Bool -> Bool
|| Coin
totalRewards Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> Coin
totalRewards' Coin -> Coin -> Bool
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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"preserveBalance" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget ledger -> Property)
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
createdIsConsumed ([SourceSignalTarget ledger] -> [Property])
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace ledger -> [SourceSignalTarget ledger]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
tickedChainSt, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    pp_ :: PParams era
pp_ = (Getting (PParams era) (EpochState era) (PParams era)
-> EpochState era -> PParams era
forall a s. Getting a s a -> s -> a
view Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL (EpochState era -> PParams era)
-> (ChainState era -> EpochState era)
-> ChainState era
-> PParams era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
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'} =
      TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
        TestName
"preserveBalance created /= consumed ... "
        (Property
failedScripts Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. Coin -> Coin -> Property
forall a. (Eq a, ToExpr a) => a -> a -> Property
ediffEq Coin
created Coin
consumed_)
      where
        failedScripts :: Property
failedScripts = Bool -> Property
forall prop. Testable prop => prop -> Property
property (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$ Tx era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
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 = Tx era
Signal ledger
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL
        created :: Coin
created =
          UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO UTxO era
u'
            Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> (TxBody era
txb TxBody era -> Getting Coin (TxBody era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody era) Coin
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody era) Coin
feeTxBodyL)
            Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> PParams era -> CertState era -> TxBody era -> Coin
forall era.
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalDepositsTxBody PParams era
pp_ CertState era
certState TxBody era
txb
        consumed_ :: Coin
consumed_ =
          UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO UTxO era
u
            Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> PParams era -> CertState era -> TxBody era -> Coin
forall era.
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalRefundsTxBody PParams era
pp_ CertState era
certState TxBody era
txb
            Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Map RewardAccount Coin -> Coin
forall m. Monoid m => Map RewardAccount m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Withdrawals -> Map RewardAccount Coin
unWithdrawals (TxBody era
txb TxBody era
-> Getting Withdrawals (TxBody era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody era) Withdrawals
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL))

-- | Preserve balance restricted to TxIns and TxOuts of the Tx
preserveBalanceRestricted ::
  forall era ledger.
  ( ChainProperty era
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
preserveBalanceRestricted :: forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"preserveBalanceRestricted" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget ledger -> Property)
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
createdIsConsumed ([SourceSignalTarget ledger] -> [Property])
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace ledger -> [SourceSignalTarget ledger]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
tickedChainSt, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    pp_ :: PParams era
pp_ = (Getting (PParams era) (EpochState era) (PParams era)
-> EpochState era -> PParams era
forall a s. Getting a s a -> s -> a
view Getting (PParams era) (EpochState era) (PParams era)
forall era. EraGov era => Lens' (EpochState era) (PParams era)
Lens' (EpochState era) (PParams era)
curPParamsEpochStateL (EpochState era -> PParams era)
-> (ChainState era -> EpochState era)
-> ChainState era
-> PParams era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
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 Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Coin
outs
        where
          txb :: TxBody era
txb = Tx era
Signal ledger
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL
          inps :: Coin
inps =
            forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO @era (UTxO era -> Set TxIn -> UTxO era
forall era. UTxO era -> Set TxIn -> UTxO era
txInsFilter UTxO era
utxo (TxBody era
txb TxBody era
-> Getting (Set TxIn) (TxBody era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody era) (Set TxIn)
forall era. EraTxBody era => Lens' (TxBody era) (Set TxIn)
Lens' (TxBody era) (Set TxIn)
inputsTxBodyL))
              Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> PParams era -> CertState era -> TxBody era -> Coin
forall era.
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody era -> Coin
certsTotalRefundsTxBody PParams era
pp_ CertState era
certState TxBody era
txb
              Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Map RewardAccount Coin -> Coin
forall m. Monoid m => Map RewardAccount m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold (Withdrawals -> Map RewardAccount Coin
unWithdrawals (TxBody era
txb TxBody era
-> Getting Withdrawals (TxBody era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody era) Withdrawals
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL))
          outs :: Coin
outs =
            UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO (forall era. EraTxBody era => TxBody era -> UTxO era
txouts @era TxBody era
txb)
              Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> (TxBody era
txb TxBody era -> Getting Coin (TxBody era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody era) Coin
forall era. EraTxBody era => Lens' (TxBody era) Coin
Lens' (TxBody era) Coin
feeTxBodyL)
              Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> PParams era -> CertState era -> TxBody era -> Coin
forall era.
(EraCertState 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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"preserveOutputsTx" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget ledger -> Property)
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget ledger -> Property
outputPreserved ([SourceSignalTarget ledger] -> [Property])
-> [SourceSignalTarget ledger] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace ledger -> [SourceSignalTarget ledger]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTr
  where
    (ChainState era
_, Trace ledger
ledgerTr) = forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
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 (Tx era
Signal ledger
tx Tx era -> Getting (TxBody era) (Tx era) (TxBody era) -> TxBody era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody era) (Tx era) (TxBody era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL)
         in Property -> Property
forall prop. Testable prop => prop -> Property
property (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              Tx era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
Signal ledger
tx
                Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"TxOuts are not a subset of UTxO" (Map TxIn (TxOut era)
outs Map TxIn (TxOut era) -> Map TxIn (TxOut era) -> Bool
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
  , TestingLedger era ledger
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
canRestrictUTxO :: forall era ledger.
(ChainProperty 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} =
  TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample TestName
"canRestrictUTxO" (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ([Property] -> Property) -> [Property] -> Property
forall a b. (a -> b) -> a -> b
$
      (SourceSignalTarget ledger
 -> SourceSignalTarget ledger -> Property)
-> [SourceSignalTarget ledger]
-> [SourceSignalTarget ledger]
-> [Property]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
        SourceSignalTarget ledger -> SourceSignalTarget ledger -> Property
outputPreserved
        (Trace ledger -> [SourceSignalTarget ledger]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTrFull)
        (Trace ledger -> [SourceSignalTarget ledger]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace ledger
ledgerTrRestr)
  where
    (ChainState era
_, Trace ledger
ledgerTrFull) = forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (ChainState era, Trace ledger)
ledgerTraceFromBlock @era @ledger State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    (UTxO Map TxIn (TxOut era)
irrelevantUTxO, Trace ledger
ledgerTrRestr) =
      forall era ledger.
(ChainProperty era, TestingLedger era ledger) =>
ChainState era
-> Block (BHeader MockCrypto) era -> (UTxO era, Trace ledger)
ledgerTraceFromBlockWithRestrictedUTxO @era @ledger State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
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
_} =
        TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
          ([TestName] -> TestName
unlines [TestName
"non-disjoint:", Map TxIn (TxOut era) -> TestName
forall a. Show a => a -> TestName
show Map TxIn (TxOut era)
uRestr, Map TxIn (TxOut era) -> TestName
forall a. Show a => a -> TestName
show Map TxIn (TxOut era)
irrelevantUTxO])
          (Map TxIn (TxOut era)
uRestr Map TxIn (TxOut era) -> Map TxIn (TxOut era) -> Bool
forall k a b. Ord k => Map k a -> Map k b -> Bool
`Map.disjoint` Map TxIn (TxOut era)
irrelevantUTxO)
          Property -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.&&. Map TxIn (TxOut era)
uFull
            Map TxIn (TxOut era) -> Map TxIn (TxOut era) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (Map TxIn (TxOut era)
uRestr Map TxIn (TxOut era)
-> Map TxIn (TxOut era) -> Map TxIn (TxOut era)
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 (Block BHeader MockCrypto
_ TxSeq era
txseq) =
  (Coin -> Tx era -> Coin) -> Coin -> StrictSeq (Tx era) -> Coin
forall b a. (b -> a -> b) -> b -> StrictSeq a -> b
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 (Withdrawals -> Map RewardAccount Coin)
-> Withdrawals -> Map RewardAccount Coin
forall a b. (a -> b) -> a -> b
$ Tx era
tx Tx era -> Getting Withdrawals (Tx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody era -> Const Withdrawals (TxBody era))
-> Tx era -> Const Withdrawals (Tx era)
forall era. EraTx era => Lens' (Tx era) (TxBody era)
Lens' (Tx era) (TxBody era)
bodyTxL ((TxBody era -> Const Withdrawals (TxBody era))
 -> Tx era -> Const Withdrawals (Tx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody era -> Const Withdrawals (TxBody era))
-> Getting Withdrawals (Tx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody era -> Const Withdrawals (TxBody era)
forall era. EraTxBody era => Lens' (TxBody era) Withdrawals
Lens' (TxBody era) Withdrawals
withdrawalsTxBodyL
         in if Tx era -> Bool
forall era. EraGen era => Tx era -> Bool
hasFailedScripts Tx era
tx then Coin
c else Coin
c Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Map RewardAccount Coin -> Coin
forall m. Monoid m => Map RewardAccount m -> m
forall (t :: * -> *) m. (Foldable t, Monoid m) => t m -> m
fold Map RewardAccount Coin
wdrls
    )
    (Integer -> Coin
Coin Integer
0)
    (StrictSeq (Tx era) -> Coin) -> StrictSeq (Tx era) -> Coin
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 =
  (Coin -> SourceSignalTarget ledger -> Coin)
-> Coin -> [SourceSignalTarget ledger] -> Coin
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' Coin -> SourceSignalTarget ledger -> Coin
forall {era} {a}.
(State a ~ LedgerState era, Signal a ~ Tx era,
 ProtVerIsInBounds
   "at most"
   era
   8
   (OrdCond (CmpNat (ProtVerLow era) 8) 'True 'True 'False),
 Assert
   (OrdCond
      (CmpNat (ProtVerLow era) (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerLow era)) 'True 'True 'False)
   (TypeError ...),
 Assert
   (OrdCond (CmpNat 0 (ProtVerHigh era)) 'True 'True 'False)
   (TypeError ...),
 EraGen era) =>
Coin -> SourceSignalTarget a -> Coin
f (Integer -> Coin
Coin Integer
0) (Trace ledger -> [SourceSignalTarget ledger]
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 Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> Tx era -> UTxO era -> Coin
forall era. EraGen era => Tx era -> UTxO era -> Coin
feeOrCollateral Tx era
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 = (NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes) State (CHAIN era)
ChainState era
chainSt
      UTxOState {utxosDeposited :: forall era. UTxOState era -> Coin
utxosDeposited = Coin
d} = (LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState (LedgerState era -> UTxOState era)
-> (EpochState era -> LedgerState era)
-> EpochState era
-> UTxOState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState) EpochState era
es
   in TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"nonNegativeDeposits: " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Coin -> TestName
forall a. Show a => a -> TestName
show Coin
d) (Coin
d Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
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 :: 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} =
  TestName -> Bool -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample (TestName
"feesNonDecreasing: " TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> Coin -> TestName
forall a. Show a => a -> TestName
show (ChainState era -> Coin
forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
ChainState era
source) TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> TestName
" <= " TestName -> TestName -> TestName
forall a. Semigroup a => a -> a -> a
<> Coin -> TestName
forall a. Show a => a -> TestName
show (ChainState era -> Coin
forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
ChainState era
target)) (Bool -> Property) -> Bool -> Property
forall a b. (a -> b) -> a -> b
$
    ChainState era -> Coin
forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
ChainState era
source Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
<= ChainState era -> Coin
forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
ChainState era
target
  where
    fees_ :: ChainState era -> Coin
fees_ ChainState era
chainSt =
      let UTxOState {utxosFees :: forall era. UTxOState era -> Coin
utxosFees = Coin
fees} =
            LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState (LedgerState era -> UTxOState era)
-> (ChainState era -> LedgerState era)
-> ChainState era
-> UTxOState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (ChainState era -> EpochState era)
-> ChainState era
-> LedgerState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewEpochState era -> EpochState era
forall era. NewEpochState era -> EpochState era
nesEs (NewEpochState era -> EpochState era)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes (ChainState era -> UTxOState era)
-> ChainState era -> UTxOState era
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 :: 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} =
  ChainState era -> EpochNo
forall {era}. ChainState era -> EpochNo
epoch State (CHAIN era)
ChainState era
source EpochNo -> EpochNo -> Bool
forall a. Eq a => a -> a -> Bool
== ChainState era -> EpochNo
forall {era}. ChainState era -> EpochNo
epoch State (CHAIN era)
ChainState era
target
  where
    epoch :: ChainState era -> EpochNo
epoch = NewEpochState era -> EpochNo
forall era. NewEpochState era -> EpochNo
nesEL (NewEpochState era -> EpochNo)
-> (ChainState era -> NewEpochState era)
-> ChainState era
-> EpochNo
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes