{-# 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 (..))
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 TopTx 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 TopTx era,
 Environment (EraRule "LEDGER" era) ~ LedgerEnv era,
 BaseM (EraRule "LEDGER" era) ~ ShelleyBase,
 STS (EraRule "LEDGER" era)) =>
Int -> TestTree
tests Int
n =
  String -> Property -> TestTree
forall prop.
(HasCallStack, Testable prop) =>
String -> prop -> TestTree
TQC.testProperty
    String
"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 TopTx 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 TopTx 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 TopTx 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 TopTx 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 TopTx 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 TopTx 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 TopTx 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 TopTx 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 TopTx 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 TopTx 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 TopTx 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 -> String
infoRetire Map (KeyHash StakePool) a
deposits KeyHash StakePool
keyhash = KeyHash StakePool -> String
forall (x :: KeyRole). KeyHash x -> String
showKeyHash KeyHash StakePool
keyhash String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
extra
  where
    extra :: String
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 -> String
" (?)"
      Just a
coin -> String
" (" String -> String -> String
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
coin String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
")"

-- 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 :: forall a. SourceSignalTarget a -> Signal a
signal = Signal (CHAIN era)
block} Int
count =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
    ( [String] -> String
forall a. Monoid a => [a] -> a
mconcat
        ( [ String
"\ncount = " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
count String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\n"
          , String -> AdaPots -> String -> AdaPots -> String
compareAdaPots String
"before" (ChainState era -> AdaPots
forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
ChainState era -> AdaPots
totalAdaPots State (CHAIN era)
ChainState era
source) String
"after" (ChainState era -> AdaPots
forall era.
(EraTxOut era, EraGov era, EraCertState era) =>
ChainState era -> AdaPots
totalAdaPots State (CHAIN era)
ChainState era
target)
          , String
"\n\nTotal lovelace before block\n"
          , Coin -> String
forall a. Show a => a -> String
show Coin
sourceTotal
          , String
"\n\nTotal lovelace after block\n"
          , Coin -> String
forall a. Show a => a -> String
show Coin
targetTotal
          , String
"\n\nEpoch before block\n"
          , EpochNo -> String
forall a. Show a => a -> String
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)
          , String
"\n\nEpoch after block\n"
          , EpochNo -> String
forall a. Show a => a -> String
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)
          , String
"\n\nCurrent protocol parameters\n"
          , PParams era -> String
forall a. Show a => a -> String
show PParams era
currPP
          , String
"\nReward Accounts before update\n"
          , Accounts era -> String
forall a. Show a => a -> String
show Accounts era
oldAccounts
          , String
"\nReward Accounts after update\n"
          , Accounts era -> String
forall a. Show a => a -> String
show Accounts era
newAccounts
          , String
"\nRetiring pools before update\n"
          , (KeyHash StakePool -> String)
-> (EpochNo -> String) -> Map (KeyHash StakePool) EpochNo -> String
forall t1 t2.
(t1 -> String) -> (t2 -> String) -> Map t1 t2 -> String
showMap (Map (KeyHash StakePool) (CompactForm Coin)
-> KeyHash StakePool -> String
forall a.
Show a =>
Map (KeyHash StakePool) a -> KeyHash StakePool -> String
infoRetire Map (KeyHash StakePool) (CompactForm Coin)
oldPoolDeposit) EpochNo -> String
forall a. Show a => a -> String
show Map (KeyHash StakePool) EpochNo
oldRetire
          , String
"\nRetiring pools after update\n"
          , (KeyHash StakePool -> String)
-> (EpochNo -> String) -> Map (KeyHash StakePool) EpochNo -> String
forall t1 t2.
(t1 -> String) -> (t2 -> String) -> Map t1 t2 -> String
showMap (Map (KeyHash StakePool) (CompactForm Coin)
-> KeyHash StakePool -> String
forall a.
Show a =>
Map (KeyHash StakePool) a -> KeyHash StakePool -> String
infoRetire Map (KeyHash StakePool) (CompactForm Coin)
newPoolDeposit) EpochNo -> String
forall a. Show a => a -> String
show Map (KeyHash StakePool) EpochNo
newRetire
          , String
"\nMIR\n"
          , InstantaneousRewards -> String
showIR InstantaneousRewards
mir
          , String
"\n\nRegistered Reserves MIR total "
          , Coin -> String
forall a. Show a => a -> String
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)
          , String
"\n\nUnregistered Reserves MIR total "
          , Coin -> String
forall a. Show a => a -> String
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)
          , String
"\n\nRegistered Treasury MIR total "
          , Coin -> String
forall a. Show a => a -> String
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)
          , String
"\n\nUnregistered Treasury MIR total "
          , Coin -> String
forall a. Show a => a -> String
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)
          , String
"\n\nPools Retiring This epoch\n"
          , (KeyHash StakePool -> String)
-> (EpochNo -> String) -> Map (KeyHash StakePool) EpochNo -> String
forall t1 t2.
(t1 -> String) -> (t2 -> String) -> Map t1 t2 -> String
showMap
              (Map (KeyHash StakePool) (CompactForm Coin)
-> KeyHash StakePool -> String
forall a.
Show a =>
Map (KeyHash StakePool) a -> KeyHash StakePool -> String
infoRetire Map (KeyHash StakePool) (CompactForm Coin)
oldPoolDeposit)
              EpochNo -> String
forall a. Show a => a -> String
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)
          ]
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
obligationMsgs
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
rewardUpdateMsgs
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String
"\n\ntransactions"]
            [String] -> [String] -> [String]
forall a. [a] -> [a] -> [a]
++ [String]
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 :: [String]
obligationMsgs = case Maybe (PParams era)
proposal of
      Maybe (PParams era)
Nothing -> []
      Just PParams era
proposal' ->
        [ String
"\n\nProposed protocol parameter update\n"
        , PParams era -> String
forall a. Show a => a -> String
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 :: [String]
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 [ String
"\n\nSum of new rewards "
            , Coin -> String
forall a. Show a => a -> String
show (ProtVer -> Map (Credential Staking) (Set Reward) -> Coin
sumRewards ProtVer
prevPP (RewardUpdate -> Map (Credential Staking) (Set Reward)
rs RewardUpdate
ru))
            , String
"\n\nNew rewards "
            , Map (Credential Staking) (Set Reward) -> String
forall a. Show a => a -> String
show (RewardUpdate -> Map (Credential Staking) (Set Reward)
rs RewardUpdate
ru)
            , String
"\n\nSum of new registered rewards "
            , Coin -> String
forall a. Show a => a -> String
show (ProtVer -> Map (Credential Staking) (Set Reward) -> Coin
sumRewards ProtVer
prevPP Map (Credential Staking) (Set Reward)
regRewards)
            , String
"\n\nChange in Fees "
            , DeltaCoin -> String
forall a. Show a => a -> String
show (RewardUpdate -> DeltaCoin
deltaF RewardUpdate
ru)
            , String
"\n\nChange in Treasury "
            , DeltaCoin -> String
forall a. Show a => a -> String
show (RewardUpdate -> DeltaCoin
deltaT RewardUpdate
ru)
            , String
"\n\nChange in Reserves "
            , DeltaCoin -> String
forall a. Show a => a -> String
show (RewardUpdate -> DeltaCoin
deltaR RewardUpdate
ru)
            , String
"\n\nNet effect of reward update "
            , DeltaCoin -> String
forall a. Show a => a -> String
show (DeltaCoin -> String) -> DeltaCoin -> String
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 TopTx era]
txs' = StrictSeq (Tx TopTx era) -> [Tx TopTx era]
forall a. StrictSeq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList (StrictSeq (Tx TopTx era) -> [Tx TopTx era])
-> StrictSeq (Tx TopTx era) -> [Tx TopTx era]
forall a b. (a -> b) -> a -> b
$ Block (BHeader MockCrypto) era -> BlockBody era
forall h era. Block h era -> BlockBody era
blockBody Block (BHeader MockCrypto) era
Signal (CHAIN era)
block BlockBody era
-> Getting
     (StrictSeq (Tx TopTx era))
     (BlockBody era)
     (StrictSeq (Tx TopTx era))
-> StrictSeq (Tx TopTx era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (Tx TopTx era))
  (BlockBody era)
  (StrictSeq (Tx TopTx era))
forall era.
EraBlockBody era =>
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
txSeqBlockBodyL
    txs :: [String]
txs = (Tx TopTx era -> Int -> String)
-> [Tx TopTx era] -> [Int] -> [String]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Tx TopTx era -> Int -> String
dispTx [Tx TopTx era]
txs' [Int
0 :: Int ..]

    dispTx :: Tx TopTx era -> Int -> String
dispTx Tx TopTx era
tx Int
ix =
      String
"\n\n******** Transaction "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
ix
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ SafeHash EraIndependentTxBody -> String
forall a. Show a => a -> String
show (forall x i. HashAnnotated x i => x -> SafeHash i
hashAnnotated @_ @EraIndependentTxBody (Tx TopTx era
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL))
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nfee :"
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Coin -> String
forall a. Show a => a -> String
show (Tx TopTx era
tx Tx TopTx era -> Getting Coin (Tx TopTx era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. (TxBody TopTx era -> Const Coin (TxBody TopTx era))
-> Tx TopTx era -> Const Coin (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL ((TxBody TopTx era -> Const Coin (TxBody TopTx era))
 -> Tx TopTx era -> Const Coin (Tx TopTx era))
-> ((Coin -> Const Coin Coin)
    -> TxBody TopTx era -> Const Coin (TxBody TopTx era))
-> Getting Coin (Tx TopTx era) Coin
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Coin -> Const Coin Coin)
-> TxBody TopTx era -> Const Coin (TxBody TopTx era)
forall era. EraTxBody era => Lens' (TxBody TopTx era) Coin
Lens' (TxBody TopTx era) Coin
feeTxBodyL)
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\nwithdrawals:"
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Withdrawals -> String
showWithdrawal (Tx TopTx era
tx Tx TopTx era
-> Getting Withdrawals (Tx TopTx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Tx TopTx era -> Const Withdrawals (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL ((TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
 -> Tx TopTx era -> Const Withdrawals (Tx TopTx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Getting Withdrawals (Tx TopTx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l era) Withdrawals
withdrawalsTxBodyL)
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\ncerts:"
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ (TxCert era -> String) -> [TxCert era] -> String
forall (t :: * -> *) a.
Foldable t =>
(a -> String) -> t a -> String
showListy ((String
"   " String -> String -> String
forall a. [a] -> [a] -> [a]
++) (String -> String)
-> (TxCert era -> String) -> TxCert era -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TxCert era -> String
forall a. Show a => a -> String
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 TopTx era
tx Tx TopTx era
-> Getting
     (StrictSeq (TxCert era)) (Tx TopTx era) (StrictSeq (TxCert era))
-> StrictSeq (TxCert era)
forall s a. s -> Getting a s a -> a
^. (TxBody TopTx era
 -> Const (StrictSeq (TxCert era)) (TxBody TopTx era))
-> Tx TopTx era -> Const (StrictSeq (TxCert era)) (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL ((TxBody TopTx era
  -> Const (StrictSeq (TxCert era)) (TxBody TopTx era))
 -> Tx TopTx era -> Const (StrictSeq (TxCert era)) (Tx TopTx era))
-> ((StrictSeq (TxCert era)
     -> Const (StrictSeq (TxCert era)) (StrictSeq (TxCert era)))
    -> TxBody TopTx era
    -> Const (StrictSeq (TxCert era)) (TxBody TopTx era))
-> Getting
     (StrictSeq (TxCert era)) (Tx TopTx 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 TopTx era
-> Const (StrictSeq (TxCert era)) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (StrictSeq (TxCert era))
forall (l :: TxLevel).
Lens' (TxBody l era) (StrictSeq (TxCert era))
certsTxBodyL)
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"total deposits "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Coin -> String
forall a. Show a => a -> String
show (PParams era -> CertState era -> TxBody TopTx era -> Coin
forall era (t :: TxLevel).
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody t era -> Coin
forall (t :: TxLevel).
EraTxBody era =>
PParams era -> CertState era -> TxBody t era -> Coin
certsTotalDepositsTxBody PParams era
currPP CertState era
oldCertState (Tx TopTx era
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL))
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
"\ntotal refunds "
        String -> String -> String
forall a. [a] -> [a] -> [a]
++ Coin -> String
forall a. Show a => a -> String
show (PParams era -> CertState era -> TxBody TopTx era -> Coin
forall era (t :: TxLevel).
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody t era -> Coin
forall (t :: TxLevel).
EraTxBody era =>
PParams era -> CertState era -> TxBody t era -> Coin
certsTotalRefundsTxBody PParams era
currPP CertState era
oldCertState (Tx TopTx era
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
    String
"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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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 TopTx era -> Bool
forall era. EraGen era => Tx TopTx era -> Bool
hasFailedScripts Tx TopTx 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 TopTx era
Signal (EraRule "LEDGER" era)
tx Tx TopTx era
-> Getting Withdrawals (Tx TopTx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Tx TopTx era -> Const Withdrawals (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL ((TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
 -> Tx TopTx era -> Const Withdrawals (Tx TopTx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Getting Withdrawals (Tx TopTx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l 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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 {a} {era} {era}.
(Signal a ~ Tx TopTx era, State a ~ LedgerState era,
 ProtVerIsInBounds
   "at most"
   era
   11
   (OrdCond (CmpNat (ProtVerLow era) 11) 'True 'True 'False),
 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 TopTx 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 TopTx era
Signal a
tx Tx TopTx era
-> Getting Withdrawals (Tx TopTx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Tx TopTx era -> Const Withdrawals (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL ((TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
 -> Tx TopTx era -> Const Withdrawals (Tx TopTx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Getting Withdrawals (Tx TopTx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l era) Withdrawals
withdrawalsTxBodyL))
         in [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin
              [ String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"A transaction should not increase the Rewards pot"
                  (Coin
totalRewards Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Coin
totalRewards')
              , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"Withdrawals should be non-negative"
                  (Coin
txWithdrawals Coin -> Coin -> Bool
forall a. Ord a => a -> a -> Bool
>= Integer -> Coin
Coin Integer
0)
              , String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                  String
"Rewards should increase by withdrawals"
                  (Tx TopTx era -> Bool
forall era. EraGen era => Tx TopTx era -> Bool
hasFailedScripts Tx TopTx 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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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'} =
      String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
        String
"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 TopTx era -> Bool
forall era. EraGen era => Tx TopTx era -> Bool
hasFailedScripts Tx TopTx 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 TopTx era
txb = Tx TopTx era
Signal (EraRule "LEDGER" era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l 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 TopTx era
txb TxBody TopTx era -> Getting Coin (TxBody TopTx era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody TopTx era) Coin
forall era. EraTxBody era => Lens' (TxBody TopTx era) Coin
Lens' (TxBody TopTx era) Coin
feeTxBodyL)
            Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> PParams era -> CertState era -> TxBody TopTx era -> Coin
forall era (t :: TxLevel).
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody t era -> Coin
forall (t :: TxLevel).
EraTxBody era =>
PParams era -> CertState era -> TxBody t era -> Coin
certsTotalDepositsTxBody PParams era
pp_ CertState era
certState TxBody TopTx 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 TopTx era -> Coin
forall era (t :: TxLevel).
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody t era -> Coin
forall (t :: TxLevel).
EraTxBody era =>
PParams era -> CertState era -> TxBody t era -> Coin
certsTotalRefundsTxBody PParams era
pp_ CertState era
certState TxBody TopTx 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 TopTx era
txb TxBody TopTx era
-> Getting Withdrawals (TxBody TopTx era) Withdrawals
-> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody TopTx era) Withdrawals
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l 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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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 TopTx era
txb = Tx TopTx era
Signal (EraRule "LEDGER" era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l 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 TopTx era
txb TxBody TopTx era
-> Getting (Set TxIn) (TxBody TopTx era) (Set TxIn) -> Set TxIn
forall s a. s -> Getting a s a -> a
^. Getting (Set TxIn) (TxBody TopTx era) (Set TxIn)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) (Set TxIn)
forall (l :: TxLevel). Lens' (TxBody l era) (Set TxIn)
inputsTxBodyL))
              Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> PParams era -> CertState era -> TxBody TopTx era -> Coin
forall era (t :: TxLevel).
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody t era -> Coin
forall (t :: TxLevel).
EraTxBody era =>
PParams era -> CertState era -> TxBody t era -> Coin
certsTotalRefundsTxBody PParams era
pp_ CertState era
certState TxBody TopTx 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 TopTx era
txb TxBody TopTx era
-> Getting Withdrawals (TxBody TopTx era) Withdrawals
-> Withdrawals
forall s a. s -> Getting a s a -> a
^. Getting Withdrawals (TxBody TopTx era) Withdrawals
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l era) Withdrawals
withdrawalsTxBodyL))
          outs :: Coin
outs =
            UTxO era -> Coin
forall era. EraTxOut era => UTxO era -> Coin
sumCoinUTxO (forall era (l :: TxLevel).
EraTxBody era =>
TxBody l era -> UTxO era
txouts @era TxBody TopTx era
txb)
              Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> (TxBody TopTx era
txb TxBody TopTx era -> Getting Coin (TxBody TopTx era) Coin -> Coin
forall s a. s -> Getting a s a -> a
^. Getting Coin (TxBody TopTx era) Coin
forall era. EraTxBody era => Lens' (TxBody TopTx era) Coin
Lens' (TxBody TopTx era) Coin
feeTxBodyL)
              Coin -> Coin -> Coin
forall a. Semigroup a => a -> a -> a
<> PParams era -> CertState era -> TxBody TopTx era -> Coin
forall era (t :: TxLevel).
(EraCertState era, EraTxBody era) =>
PParams era -> CertState era -> TxBody t era -> Coin
forall (t :: TxLevel).
EraTxBody era =>
PParams era -> CertState era -> TxBody t era -> Coin
certsTotalDepositsTxBody PParams era
pp_ CertState era
certState TxBody TopTx 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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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 (l :: TxLevel).
EraTxBody era =>
TxBody l era -> UTxO era
txouts @era (Tx TopTx era
Signal (EraRule "LEDGER" era)
tx Tx TopTx era
-> Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
-> TxBody TopTx era
forall s a. s -> Getting a s a -> a
^. Getting (TxBody TopTx era) (Tx TopTx era) (TxBody TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL)
         in Property -> Property
forall prop. Testable prop => prop -> Property
property (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
              Tx TopTx era -> Bool
forall era. EraGen era => Tx TopTx era -> Bool
hasFailedScripts Tx TopTx era
Signal (EraRule "LEDGER" era)
tx
                Bool -> Property -> Property
forall prop1 prop2.
(Testable prop1, Testable prop2) =>
prop1 -> prop2 -> Property
.||. String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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 TopTx 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} =
  String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample String
"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 TopTx 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 TopTx 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
_} =
        String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
          ([String] -> String
unlines [String
"non-disjoint:", Map TxIn (TxOut era) -> String
forall a. Show a => a -> String
show Map TxIn (TxOut era)
uRestr, Map TxIn (TxOut era) -> String
forall a. Show a => a -> String
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 TopTx era -> Coin)
-> Coin -> StrictSeq (Tx TopTx 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 TopTx 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 TopTx era
tx Tx TopTx era
-> Getting Withdrawals (Tx TopTx era) Withdrawals -> Withdrawals
forall s a. s -> Getting a s a -> a
^. (TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Tx TopTx era -> Const Withdrawals (Tx TopTx era)
forall era (l :: TxLevel).
EraTx era =>
Lens' (Tx l era) (TxBody l era)
forall (l :: TxLevel). Lens' (Tx l era) (TxBody l era)
bodyTxL ((TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
 -> Tx TopTx era -> Const Withdrawals (Tx TopTx era))
-> ((Withdrawals -> Const Withdrawals Withdrawals)
    -> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era))
-> Getting Withdrawals (Tx TopTx era) Withdrawals
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Withdrawals -> Const Withdrawals Withdrawals)
-> TxBody TopTx era -> Const Withdrawals (TxBody TopTx era)
forall era (l :: TxLevel).
EraTxBody era =>
Lens' (TxBody l era) Withdrawals
forall (l :: TxLevel). Lens' (TxBody l era) Withdrawals
withdrawalsTxBodyL
         in if Tx TopTx era -> Bool
forall era. EraGen era => Tx TopTx era -> Bool
hasFailedScripts Tx TopTx 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 TopTx era) -> Coin)
-> StrictSeq (Tx TopTx era) -> Coin
forall a b. (a -> b) -> a -> b
$ BlockBody era
blockBody BlockBody era
-> Getting
     (StrictSeq (Tx TopTx era))
     (BlockBody era)
     (StrictSeq (Tx TopTx era))
-> StrictSeq (Tx TopTx era)
forall s a. s -> Getting a s a -> a
^. Getting
  (StrictSeq (Tx TopTx era))
  (BlockBody era)
  (StrictSeq (Tx TopTx era))
forall era.
EraBlockBody era =>
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
Lens' (BlockBody era) (StrictSeq (Tx TopTx era))
txSeqBlockBodyL

txFees ::
  forall era.
  ( EraGen era
  , Signal (EraRule "LEDGER" era) ~ Tx TopTx era
  , State (EraRule "LEDGER" era) ~ LedgerState era
  ) =>
  Trace (EraRule "LEDGER" era) ->
  Coin
txFees :: forall era.
(EraGen era, Signal (EraRule "LEDGER" era) ~ Tx TopTx 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 TopTx 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 TopTx 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 String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"nonNegativeDeposits: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Coin -> String
forall a. Show a => a -> String
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} =
  String -> Bool -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample (String
"feesNonDecreasing: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Coin -> String
forall a. Show a => a -> String
show (ChainState era -> Coin
forall {era}. ChainState era -> Coin
fees_ State (CHAIN era)
ChainState era
source) String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" <= " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Coin -> String
forall a. Show a => a -> String
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