{-# 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 (ShelleyBase, StrictMaybe (..))
import Cardano.Ledger.Block (
  Block (..),
  bbody,
 )
import Cardano.Ledger.Coin
import Cardano.Ledger.Credential
import Cardano.Ledger.Shelley.API (LedgerState)
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 (LedgerEnv, votedFuturePParams)
import Cardano.Ledger.Shelley.Rules.Reports (
  showIR,
  showKeyHash,
  showListy,
  showMap,
  showWithdrawal,
 )
import Cardano.Ledger.Shelley.State
import Cardano.Ledger.Val ((<+>), (<->))
import Cardano.Protocol.TPraos.BHeader (BHeader (..))
import Control.State.Transition.Extended (BaseM, Environment, STS, Signal, State)
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 (
  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.
  ( EraGen era
  , EraStake era
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  , GovState era ~ ShelleyGovState era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , STS (EraRule "LEDGER" era)
  ) =>
  Int ->
  TestTree
tests :: forall era.
(EraGen era, EraStake era, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era),
 GovState era ~ ShelleyGovState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" 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.
(EraGen era, EraStake era, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era),
 GovState era ~ ShelleyGovState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era)) =>
Property
adaPreservationProps @era))

-- | Various preservation properties
adaPreservationProps ::
  forall era.
  ( EraGen era
  , EraStake era
  , ChainProperty era
  , QC.HasTrace (CHAIN era) (GenEnv MockCrypto era)
  , GovState era ~ ShelleyGovState era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , STS (EraRule "LEDGER" era)
  ) =>
  Property
adaPreservationProps :: forall era.
(EraGen era, EraStake era, ChainProperty era,
 HasTrace (CHAIN era) (GenEnv MockCrypto era),
 GovState era ~ ShelleyGovState era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" 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.
(EraBlockBody 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.
(ChainProperty era, EraGen era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseWithdrawalsPerTx @era) [SourceSignalTarget (CHAIN era)]
ssts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(ChainProperty era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
potsSumIncreaseByRewardsPerTx @era) [SourceSignalTarget (CHAIN era)]
ssts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(ChainProperty era, EraGen era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
preserveBalance @era) [SourceSignalTarget (CHAIN era)]
ssts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(ChainProperty era, BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
preserveBalanceRestricted @era) [SourceSignalTarget (CHAIN era)]
ssts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(ChainProperty era, EraGen era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
preserveOutputsTx @era) [SourceSignalTarget (CHAIN era)]
ssts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(EraGen era, ChainProperty era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
potsRewardsDecreaseByWithdrawalsPerTx @era) [SourceSignalTarget (CHAIN era)]
ssts
      , (SourceSignalTarget (CHAIN era) -> Property)
-> [SourceSignalTarget (CHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map (forall era.
(ChainProperty era, Signal (EraRule "LEDGER" era) ~ Tx era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
canRestrictUTxO @era) [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.
(ChainProperty era, EraGen era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
utxoDepositsIncreaseByFeesWithdrawals @era) [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 :: Show a => Map (KeyHash 'StakePool) a -> KeyHash 'StakePool -> String
infoRetire :: forall a.
Show a =>
Map (KeyHash 'StakePool) a -> KeyHash 'StakePool -> TestName
infoRetire Map (KeyHash 'StakePool) a
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) a -> Maybe a
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup KeyHash 'StakePool
keyhash Map (KeyHash 'StakePool) a
deposits of
      Maybe a
Nothing -> TestName
" (?)"
      Just a
coin -> TestName
" (" TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ a -> TestName
forall a. Show a => a -> TestName
show a
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.
  ( EraBlockBody era
  , GovState era ~ ShelleyGovState era
  , EraGov era
  , EraCertState era
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Int ->
  Property
checkPreservation :: forall era.
(EraBlockBody 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"
          , Accounts era -> TestName
forall a. Show a => a -> TestName
show Accounts era
oldAccounts
          , TestName
"\nReward Accounts after update\n"
          , Accounts era -> TestName
forall a. Show a => a -> TestName
show Accounts era
newAccounts
          , 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) (CompactForm Coin)
-> KeyHash 'StakePool -> TestName
forall a.
Show a =>
Map (KeyHash 'StakePool) a -> KeyHash 'StakePool -> TestName
infoRetire Map (KeyHash 'StakePool) (CompactForm 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) (CompactForm Coin)
-> KeyHash 'StakePool -> TestName
forall a.
Show a =>
Map (KeyHash 'StakePool) a -> KeyHash 'StakePool -> TestName
infoRetire Map (KeyHash 'StakePool) (CompactForm 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) (CompactForm Coin)
-> KeyHash 'StakePool -> TestName
forall a.
Show a =>
Map (KeyHash 'StakePool) a -> KeyHash 'StakePool -> TestName
infoRetire Map (KeyHash 'StakePool) (CompactForm 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
    oldAccounts :: Accounts era
oldAccounts = LedgerState era
lsOld LedgerState era
-> Getting (Accounts era) (LedgerState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const (Accounts era) (CertState era))
-> LedgerState era -> Const (Accounts era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (Accounts era) (CertState era))
 -> LedgerState era -> Const (Accounts era) (LedgerState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> CertState era -> Const (Accounts era) (CertState era))
-> Getting (Accounts era) (LedgerState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> (Accounts era -> Const (Accounts era) (Accounts era))
-> CertState era
-> Const (Accounts era) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL
    newAccounts :: Accounts era
newAccounts = LedgerState era
lsNew LedgerState era
-> Getting (Accounts era) (LedgerState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (CertState era -> Const (Accounts era) (CertState era))
-> LedgerState era -> Const (Accounts era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era -> Const (Accounts era) (CertState era))
 -> LedgerState era -> Const (Accounts era) (LedgerState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> CertState era -> Const (Accounts era) (CertState era))
-> Getting (Accounts era) (LedgerState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> (Accounts era -> Const (Accounts era) (Accounts era))
-> CertState era
-> Const (Accounts era) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL
    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) (CompactForm Coin)
oldPoolDeposit = StakePoolState -> CompactForm Coin
spsDeposit (StakePoolState -> CompactForm Coin)
-> Map (KeyHash 'StakePool) StakePoolState
-> Map (KeyHash 'StakePool) (CompactForm Coin)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LedgerState era
lsOld LedgerState era
-> Getting
     (Map (KeyHash 'StakePool) StakePoolState)
     (LedgerState era)
     (Map (KeyHash 'StakePool) StakePoolState)
-> Map (KeyHash 'StakePool) StakePoolState
forall s a. s -> Getting a s a -> a
^. (CertState era
 -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
-> LedgerState era
-> Const
     (Map (KeyHash 'StakePool) StakePoolState) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
 -> LedgerState era
 -> Const
      (Map (KeyHash 'StakePool) StakePoolState) (LedgerState era))
-> ((Map (KeyHash 'StakePool) StakePoolState
     -> Const
          (Map (KeyHash 'StakePool) StakePoolState)
          (Map (KeyHash 'StakePool) StakePoolState))
    -> CertState era
    -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
-> Getting
     (Map (KeyHash 'StakePool) StakePoolState)
     (LedgerState era)
     (Map (KeyHash 'StakePool) StakePoolState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era
 -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era
  -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
-> ((Map (KeyHash 'StakePool) StakePoolState
     -> Const
          (Map (KeyHash 'StakePool) StakePoolState)
          (Map (KeyHash 'StakePool) StakePoolState))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
-> (Map (KeyHash 'StakePool) StakePoolState
    -> Const
         (Map (KeyHash 'StakePool) StakePoolState)
         (Map (KeyHash 'StakePool) StakePoolState))
-> CertState era
-> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) StakePoolState
 -> Const
      (Map (KeyHash 'StakePool) StakePoolState)
      (Map (KeyHash 'StakePool) StakePoolState))
-> PState era
-> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) StakePoolState
 -> f (Map (KeyHash 'StakePool) StakePoolState))
-> PState era -> f (PState era)
psStakePoolsL
    newPoolDeposit :: Map (KeyHash 'StakePool) (CompactForm Coin)
newPoolDeposit = StakePoolState -> CompactForm Coin
spsDeposit (StakePoolState -> CompactForm Coin)
-> Map (KeyHash 'StakePool) StakePoolState
-> Map (KeyHash 'StakePool) (CompactForm Coin)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> LedgerState era
lsNew LedgerState era
-> Getting
     (Map (KeyHash 'StakePool) StakePoolState)
     (LedgerState era)
     (Map (KeyHash 'StakePool) StakePoolState)
-> Map (KeyHash 'StakePool) StakePoolState
forall s a. s -> Getting a s a -> a
^. (CertState era
 -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
-> LedgerState era
-> Const
     (Map (KeyHash 'StakePool) StakePoolState) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL ((CertState era
  -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
 -> LedgerState era
 -> Const
      (Map (KeyHash 'StakePool) StakePoolState) (LedgerState era))
-> ((Map (KeyHash 'StakePool) StakePoolState
     -> Const
          (Map (KeyHash 'StakePool) StakePoolState)
          (Map (KeyHash 'StakePool) StakePoolState))
    -> CertState era
    -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
-> Getting
     (Map (KeyHash 'StakePool) StakePoolState)
     (LedgerState era)
     (Map (KeyHash 'StakePool) StakePoolState)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (PState era
 -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
-> CertState era
-> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL ((PState era
  -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
 -> CertState era
 -> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era))
-> ((Map (KeyHash 'StakePool) StakePoolState
     -> Const
          (Map (KeyHash 'StakePool) StakePoolState)
          (Map (KeyHash 'StakePool) StakePoolState))
    -> PState era
    -> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era))
-> (Map (KeyHash 'StakePool) StakePoolState
    -> Const
         (Map (KeyHash 'StakePool) StakePoolState)
         (Map (KeyHash 'StakePool) StakePoolState))
-> CertState era
-> Const (Map (KeyHash 'StakePool) StakePoolState) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Map (KeyHash 'StakePool) StakePoolState
 -> Const
      (Map (KeyHash 'StakePool) StakePoolState)
      (Map (KeyHash 'StakePool) StakePoolState))
-> PState era
-> Const (Map (KeyHash 'StakePool) StakePoolState) (PState era)
forall era (f :: * -> *).
Functor f =>
(Map (KeyHash 'StakePool) StakePoolState
 -> f (Map (KeyHash 'StakePool) StakePoolState))
-> PState era -> f (PState era)
psStakePoolsL

    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 -> a -> Bool
    isRegistered :: forall a. Credential 'Staking -> a -> Bool
isRegistered Credential 'Staking
cred a
_ = Credential 'Staking -> Accounts era -> Bool
forall era.
EraAccounts era =>
Credential 'Staking -> Accounts era -> Bool
isAccountRegistered Credential 'Staking
cred Accounts era
oldAccounts
    (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
forall a. Credential 'Staking -> a -> 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
forall a. Credential 'Staking -> a -> 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 -> Set Reward -> Bool
forall a. Credential 'Staking -> a -> Bool
isRegistered (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
$ Block (BHeader MockCrypto) era -> BlockBody era
forall h era. Block h era -> BlockBody era
bbody Block (BHeader MockCrypto) era
Signal (CHAIN era)
signal BlockBody era
-> Getting
     (StrictSeq (Tx era)) (BlockBody era) (StrictSeq (Tx era))
-> StrictSeq (Tx era)
forall s a. s -> Getting a s a -> a
^. Getting (StrictSeq (Tx era)) (BlockBody era) (StrictSeq (Tx era))
forall era.
EraBlockBody era =>
Lens' (BlockBody era) (StrictSeq (Tx era))
Lens' (BlockBody era) (StrictSeq (Tx era))
txSeqBlockBodyL
    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 =
      CertState era -> Coin
forall era. EraCertState era => CertState era -> Coin
sumAccountsBalances (ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes State (CHAIN era)
ChainState era
source NewEpochState era
-> Getting (CertState era) (NewEpochState era) (CertState era)
-> CertState era
forall s a. s -> Getting a s a -> a
^. (EpochState era -> Const (CertState era) (EpochState era))
-> NewEpochState era -> Const (CertState era) (NewEpochState era)
forall era (f :: * -> *).
Functor f =>
(EpochState era -> f (EpochState era))
-> NewEpochState era -> f (NewEpochState era)
nesEsL ((EpochState era -> Const (CertState era) (EpochState era))
 -> NewEpochState era -> Const (CertState era) (NewEpochState era))
-> ((CertState era -> Const (CertState era) (CertState era))
    -> EpochState era -> Const (CertState era) (EpochState era))
-> Getting (CertState era) (NewEpochState era) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LedgerState era -> Const (CertState era) (LedgerState era))
-> EpochState era -> Const (CertState era) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era -> Const (CertState era) (LedgerState era))
 -> EpochState era -> Const (CertState era) (EpochState era))
-> ((CertState era -> Const (CertState era) (CertState era))
    -> LedgerState era -> Const (CertState era) (LedgerState era))
-> (CertState era -> Const (CertState era) (CertState era))
-> EpochState era
-> Const (CertState era) (EpochState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era -> Const (CertState era) (CertState era))
-> LedgerState era -> Const (CertState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL)
        Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> CertState era -> Coin
forall era. EraCertState era => CertState era -> Coin
sumAccountsBalances (ChainState era -> NewEpochState era
forall era. ChainState era -> NewEpochState era
chainNes State (CHAIN era)
ChainState era
target NewEpochState era
-> Getting (CertState era) (NewEpochState era) (CertState era)
-> CertState era
forall s a. s -> Getting a s a -> a
^. (EpochState era -> Const (CertState era) (EpochState era))
-> NewEpochState era -> Const (CertState era) (NewEpochState era)
forall era (f :: * -> *).
Functor f =>
(EpochState era -> f (EpochState era))
-> NewEpochState era -> f (NewEpochState era)
nesEsL ((EpochState era -> Const (CertState era) (EpochState era))
 -> NewEpochState era -> Const (CertState era) (NewEpochState era))
-> ((CertState era -> Const (CertState era) (CertState era))
    -> EpochState era -> Const (CertState era) (EpochState era))
-> Getting (CertState era) (NewEpochState era) (CertState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (LedgerState era -> Const (CertState era) (LedgerState era))
-> EpochState era -> Const (CertState era) (EpochState era)
forall era (f :: * -> *).
Functor f =>
(LedgerState era -> f (LedgerState era))
-> EpochState era -> f (EpochState era)
esLStateL ((LedgerState era -> Const (CertState era) (LedgerState era))
 -> EpochState era -> Const (CertState era) (EpochState era))
-> ((CertState era -> Const (CertState era) (CertState era))
    -> LedgerState era -> Const (CertState era) (LedgerState era))
-> (CertState era -> Const (CertState era) (CertState era))
-> EpochState era
-> Const (CertState era) (EpochState era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (CertState era -> Const (CertState era) (CertState era))
-> LedgerState era -> Const (CertState era) (LedgerState era)
forall era (f :: * -> *).
Functor f =>
(CertState era -> f (CertState era))
-> LedgerState era -> f (LedgerState era)
lsCertStateL)

-- | 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.
  ( ChainProperty era
  , EraGen era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
utxoDepositsIncreaseByFeesWithdrawals :: forall era.
(ChainProperty era, EraGen era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
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 (EraRule "LEDGER" era) -> Coin
forall era.
(EraGen era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era) =>
Trace (EraRule "LEDGER" era) -> Coin
txFees Trace (EraRule "LEDGER" era)
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 (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era 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.
  ( ChainProperty era
  , EraGen era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
potsSumIncreaseWithdrawalsPerTx :: forall era.
(ChainProperty era, EraGen era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 STS (EraRule "LEDGER" era)) =>
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 (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
sumIncreaseWithdrawals ([SourceSignalTarget (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
_, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    sumIncreaseWithdrawals :: SourceSignalTarget (EraRule "LEDGER" era) -> Property
    sumIncreaseWithdrawals :: SourceSignalTarget (EraRule "LEDGER" era) -> 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 (EraRule "LEDGER" era)
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 (EraRule "LEDGER" era)
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 (EraRule "LEDGER" 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))

-- | (Utxo + Deposits + Fees) increases by the reward delta
potsSumIncreaseByRewardsPerTx ::
  forall era.
  ( ChainProperty era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
potsSumIncreaseByRewardsPerTx :: forall era.
(ChainProperty era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
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 (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
forall {era} {a}.
(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 (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
_, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era 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
=== CertState era -> Coin
forall era. EraCertState era => CertState era -> Coin
sumAccountsBalances CertState era
cState1 Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<-> CertState era -> Coin
forall era. EraCertState era => CertState era -> Coin
sumAccountsBalances CertState era
cState2

-- | The Rewards pot decreases by the sum of withdrawals in a transaction
potsRewardsDecreaseByWithdrawalsPerTx ::
  forall era.
  ( EraGen era
  , ChainProperty era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
potsRewardsDecreaseByWithdrawalsPerTx :: forall era.
(EraGen era, ChainProperty era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 STS (EraRule "LEDGER" era)) =>
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 (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
forall {era} {era} {a}.
(Signal a ~ Tx era, State a ~ LedgerState 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 ...),
 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 (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
_, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era 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. EraCertState era => CertState era -> Coin
sumAccountsBalances CertState era
dpstate
            totalRewards' :: Coin
totalRewards' = CertState era -> Coin
forall era. EraCertState era => CertState era -> Coin
sumAccountsBalances 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 (Tx era
Signal a
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 [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.
  ( ChainProperty era
  , EraGen era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
preserveBalance :: forall era.
(ChainProperty era, EraGen era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 STS (EraRule "LEDGER" era)) =>
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 (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
createdIsConsumed ([SourceSignalTarget (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
tickedChainSt, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era 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 (EraRule "LEDGER" era) -> Property
createdIsConsumed SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (EraRule "LEDGER" era)
ledgerSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (EraRule "LEDGER" era)
tx, target :: forall a. SourceSignalTarget a -> State a
target = State (EraRule "LEDGER" era)
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 (EraRule "LEDGER" era)
tx
        LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u}) CertState era
certState = State (EraRule "LEDGER" era)
ledgerSt
        LedgerState (UTxOState {utxosUtxo :: forall era. UTxOState era -> UTxO era
utxosUtxo = UTxO era
u'}) CertState era
_ = State (EraRule "LEDGER" era)
ledgerSt'
        txb :: TxBody era
txb = Tx era
Signal (EraRule "LEDGER" 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
        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.
  ( ChainProperty era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
preserveBalanceRestricted :: forall era.
(ChainProperty era, BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
SourceSignalTarget (CHAIN era) -> Property
preserveBalanceRestricted SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (CHAIN era)
chainSt, signal :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} =
  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 (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
createdIsConsumed ([SourceSignalTarget (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
tickedChainSt, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era 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 (EraRule "LEDGER" era) -> 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 (EraRule "LEDGER" era)
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 (EraRule "LEDGER" 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
          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.
  ( ChainProperty era
  , EraGen era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
preserveOutputsTx :: forall era.
(ChainProperty era, EraGen era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 STS (EraRule "LEDGER" era)) =>
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 (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (EraRule "LEDGER" era) -> Property
outputPreserved ([SourceSignalTarget (EraRule "LEDGER" era)] -> [Property])
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> [Property]
forall a b. (a -> b) -> a -> b
$
        Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr
  where
    (ChainState era
_, Trace (EraRule "LEDGER" era)
ledgerTr) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    outputPreserved :: SourceSignalTarget (EraRule "LEDGER" era) -> 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 (EraRule "LEDGER" era)
tx
        } =
        let UTxO Map TxIn (TxOut era)
outs = forall era. EraTxBody era => TxBody era -> UTxO era
txouts @era (Tx era
Signal (EraRule "LEDGER" 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)
         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 (EraRule "LEDGER" era)
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.
  ( ChainProperty era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , BaseM (EraRule "LEDGER" era) ~ ShelleyBase
  , State (EraRule "LEDGER" era) ~ LedgerState era
  , Environment (EraRule "LEDGER" era) ~ LedgerEnv era
  , STS (EraRule "LEDGER" era)
  ) =>
  SourceSignalTarget (CHAIN era) ->
  Property
canRestrictUTxO :: forall era.
(ChainProperty era, Signal (EraRule "LEDGER" era) ~ Tx era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 STS (EraRule "LEDGER" era)) =>
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 (EraRule "LEDGER" era)
 -> SourceSignalTarget (EraRule "LEDGER" era) -> Property)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
-> [SourceSignalTarget (EraRule "LEDGER" era)]
-> [Property]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
        SourceSignalTarget (EraRule "LEDGER" era)
-> SourceSignalTarget (EraRule "LEDGER" era) -> Property
outputPreserved
        (Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTrFull)
        (Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTrRestr)
  where
    (ChainState era
_, Trace (EraRule "LEDGER" era)
ledgerTrFull) = forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (ChainState era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlock @era State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    (UTxO Map TxIn (TxOut era)
irrelevantUTxO, Trace (EraRule "LEDGER" era)
ledgerTrRestr) =
      forall era.
(ChainProperty era, STS (EraRule "LEDGER" era),
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 State (EraRule "LEDGER" era) ~ LedgerState era,
 Signal (EraRule "LEDGER" era) ~ Tx era) =>
ChainState era
-> Block (BHeader MockCrypto) era
-> (UTxO era, Trace (EraRule "LEDGER" era))
ledgerTraceFromBlockWithRestrictedUTxO @era State (CHAIN era)
ChainState era
chainSt Block (BHeader MockCrypto) era
Signal (CHAIN era)
block
    outputPreserved :: SourceSignalTarget (EraRule "LEDGER" era)
-> SourceSignalTarget (EraRule "LEDGER" era) -> 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
_ BlockBody era
blockBody) =
  (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
$ BlockBody era
blockBody BlockBody era
-> Getting
     (StrictSeq (Tx era)) (BlockBody era) (StrictSeq (Tx era))
-> StrictSeq (Tx era)
forall s a. s -> Getting a s a -> a
^. Getting (StrictSeq (Tx era)) (BlockBody era) (StrictSeq (Tx era))
forall era.
EraBlockBody era =>
Lens' (BlockBody era) (StrictSeq (Tx era))
Lens' (BlockBody era) (StrictSeq (Tx era))
txSeqBlockBodyL

txFees ::
  forall era.
  ( EraGen era
  , Signal (EraRule "LEDGER" era) ~ Tx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  ) =>
  Trace (EraRule "LEDGER" era) ->
  Coin
txFees :: forall era.
(EraGen era, Signal (EraRule "LEDGER" era) ~ Tx era,
 State (EraRule "LEDGER" era) ~ LedgerState era) =>
Trace (EraRule "LEDGER" era) -> Coin
txFees Trace (EraRule "LEDGER" era)
ledgerTr =
  (SourceSignalTarget (EraRule "LEDGER" era) -> Coin)
-> [SourceSignalTarget (EraRule "LEDGER" era)] -> Coin
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap
    (\SourceSignalTarget (EraRule "LEDGER" era)
sst -> forall era. EraGen era => Tx era -> UTxO era -> Coin
feeOrCollateral @era (SourceSignalTarget (EraRule "LEDGER" era)
-> Signal (EraRule "LEDGER" era)
forall a. SourceSignalTarget a -> Signal a
signal SourceSignalTarget (EraRule "LEDGER" era)
sst :: Tx era) (SourceSignalTarget (EraRule "LEDGER" era)
-> State (EraRule "LEDGER" era)
forall a. SourceSignalTarget a -> State a
source SourceSignalTarget (EraRule "LEDGER" era)
sst LedgerState era
-> Getting (UTxO era) (LedgerState era) (UTxO era) -> UTxO era
forall s a. s -> Getting a s a -> a
^. Getting (UTxO era) (LedgerState era) (UTxO era)
forall era. Lens' (LedgerState era) (UTxO era)
forall (t :: * -> *) era. CanSetUTxO t => Lens' (t era) (UTxO era)
utxoL :: UTxO era))
    (Trace (EraRule "LEDGER" era)
-> [SourceSignalTarget (EraRule "LEDGER" era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (EraRule "LEDGER" era)
ledgerTr)

-- | 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

sumAccountsBalances :: EraCertState era => CertState era -> Coin
sumAccountsBalances :: forall era. EraCertState era => CertState era -> Coin
sumAccountsBalances CertState era
certState =
  Accounts era -> Coin
forall era. EraAccounts era => Accounts era -> Coin
sumBalancesAccounts (Accounts era -> Coin) -> Accounts era -> Coin
forall a b. (a -> b) -> a -> b
$ CertState era
certState CertState era
-> Getting (Accounts era) (CertState era) (Accounts era)
-> Accounts era
forall s a. s -> Getting a s a -> a
^. (DState era -> Const (Accounts era) (DState era))
-> CertState era -> Const (Accounts era) (CertState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL ((DState era -> Const (Accounts era) (DState era))
 -> CertState era -> Const (Accounts era) (CertState era))
-> ((Accounts era -> Const (Accounts era) (Accounts era))
    -> DState era -> Const (Accounts era) (DState era))
-> Getting (Accounts era) (CertState era) (Accounts era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Accounts era -> Const (Accounts era) (Accounts era))
-> DState era -> Const (Accounts era) (DState era)
forall era. Lens' (DState era) (Accounts era)
forall (t :: * -> *) era.
CanSetAccounts t =>
Lens' (t era) (Accounts era)
accountsL