{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Cardano.Ledger.Generic.AggPropTests where

import Cardano.Ledger.Alonzo.Tx (IsValid (..))
import Cardano.Ledger.Coin (Coin (..))
import Cardano.Ledger.Core
import Cardano.Ledger.Shelley.LedgerState (
  DState (..),
  EpochState (..),
  LedgerState (..),
  NewEpochState (..),
  PState (..),
  UTxOState (..),
 )
import Cardano.Ledger.Shelley.Rules.Reports (synopsisCoinMap)
import Cardano.Ledger.State (EraCertState (..), UTxO (..))
import Cardano.Ledger.UMap (UView (RewDepUView), depositMap, domain, fromCompact, sumDepositUView)
import Cardano.Ledger.Val ((<+>))
import Control.State.Transition (STS (..))
import Data.Default (Default (def))
import Data.Foldable as F (foldl')
import qualified Data.Map as Map
import qualified Data.Set as Set
import Lens.Micro ((^.))
import qualified Prettyprinter as Pretty
import Test.Cardano.Ledger.Binary.TreeDiff (ansiDocToString, diffExpr)
import Test.Cardano.Ledger.Generic.Functions (
  getBody,
  getCollateralInputs,
  getCollateralOutputs,
  getInputs,
  getOutputs,
  isValid',
 )
import Test.Cardano.Ledger.Generic.GenState (GenSize (..), initStableFields)
import Test.Cardano.Ledger.Generic.MockChain (MOCKCHAIN, MockBlock (..), MockChainState (..))
import Test.Cardano.Ledger.Generic.Proof (
  Proof (..),
  Reflect (..),
  Some (..),
  preBabbage,
  unReflect,
 )
import Test.Cardano.Ledger.Generic.Trace (Gen1, genTrace, testPropMax)
import Test.Control.State.Transition.Trace (
  SourceSignalTarget (..),
  Trace (..),
  TraceOrder (..),
  firstAndLastState,
  sourceSignalTargets,
  traceSignals,
 )
import Test.Control.State.Transition.Trace.Generator.QuickCheck (HasTrace (..))
import Test.QuickCheck
import Test.Tasty
import Test.Tasty.QuickCheck (testProperty)

-- ============================================================

aggProp ::
  agg -> (agg -> Signal sts -> agg) -> (State sts -> State sts -> agg -> prop) -> Trace sts -> prop
aggProp :: forall agg sts prop.
agg
-> (agg -> Signal sts -> agg)
-> (State sts -> State sts -> agg -> prop)
-> Trace sts
-> prop
aggProp agg
agg0 agg -> Signal sts -> agg
aggregate State sts -> State sts -> agg -> prop
test Trace sts
trace = State sts -> State sts -> agg -> prop
test State sts
firstState State sts
lastState ((agg -> Signal sts -> agg) -> agg -> [Signal sts] -> agg
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
F.foldl' agg -> Signal sts -> agg
aggregate agg
agg0 [Signal sts]
sigs)
  where
    sigs :: [Signal sts]
sigs = TraceOrder -> Trace sts -> [Signal sts]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace sts
trace
    (State sts
firstState, State sts
lastState) = Trace sts -> (State sts, State sts)
forall s. Trace s -> (State s, State s)
firstAndLastState Trace sts
trace

-- | The aggregate sizes of (outputs - inputs) is consistent with the change in size of the UTxO.
--   Be carefull to choose the correct outputs and inputs, depending on if the Tx validates.
consistentUtxoSizeProp :: EraTx era => Proof era -> Trace (MOCKCHAIN era) -> Property
consistentUtxoSizeProp :: forall era.
EraTx era =>
Proof era -> Trace (MOCKCHAIN era) -> Property
consistentUtxoSizeProp Proof era
proof Trace (MOCKCHAIN era)
trace = Int
-> (Int -> Signal (MOCKCHAIN era) -> Int)
-> (State (MOCKCHAIN era)
    -> State (MOCKCHAIN era) -> Int -> Property)
-> Trace (MOCKCHAIN era)
-> Property
forall agg sts prop.
agg
-> (agg -> Signal sts -> agg)
-> (State sts -> State sts -> agg -> prop)
-> Trace sts
-> prop
aggProp Int
agg0 Int -> Signal (MOCKCHAIN era) -> Int
Int -> MockBlock era -> Int
aggregate State (MOCKCHAIN era) -> State (MOCKCHAIN era) -> Int -> Property
MockChainState era -> MockChainState era -> Int -> Property
forall {era} {era}.
MockChainState era -> MockChainState era -> Int -> Property
makeprop Trace (MOCKCHAIN era)
trace
  where
    agg0 :: Int
agg0 = Int
0
    aggregate :: Int -> MockBlock era -> Int
aggregate Int
count (MockBlock KeyHash 'StakePool
_ SlotNo
_ StrictSeq (Tx era)
txs) = (Int -> Tx era -> Int) -> Int -> StrictSeq (Tx era) -> Int
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' Int -> Tx era -> Int
aggTx Int
count StrictSeq (Tx era)
txs
    aggTx :: Int -> Tx era -> Int
aggTx Int
count Tx era
tx =
      Int
count
        Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ( if Bool
valid
              then StrictSeq (TxOut era) -> Int
forall a. StrictSeq a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Proof era -> TxBody era -> StrictSeq (TxOut era)
forall era.
EraTxBody era =>
Proof era -> TxBody era -> StrictSeq (TxOut era)
getOutputs Proof era
proof TxBody era
body) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Set TxIn -> Int
forall a. Set a -> Int
Set.size (Proof era -> TxBody era -> Set TxIn
forall era. EraTxBody era => Proof era -> TxBody era -> Set TxIn
getInputs Proof era
proof TxBody era
body)
              else [TxOut era] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Proof era -> TxBody era -> [TxOut era]
forall era. Proof era -> TxBody era -> [TxOut era]
getCollateralOutputs Proof era
proof TxBody era
body) Int -> Int -> Int
forall a. Num a => a -> a -> a
- Set TxIn -> Int
forall a. Set a -> Int
Set.size (Proof era -> TxBody era -> Set TxIn
forall era. Proof era -> TxBody era -> Set TxIn
getCollateralInputs Proof era
proof TxBody era
body)
          )
      where
        body :: TxBody era
body = Proof era -> Tx era -> TxBody era
forall era. EraTx era => Proof era -> Tx era -> TxBody era
getBody Proof era
proof Tx era
tx
        IsValid Bool
valid = Proof era -> Tx era -> IsValid
forall era. Proof era -> Tx era -> IsValid
isValid' Proof era
proof Tx era
tx
    makeprop :: MockChainState era -> MockChainState era -> Int -> Property
makeprop MockChainState era
firstSt MockChainState era
lastSt Int
n = MockChainState era -> Int
forall era. MockChainState era -> Int
getUtxoSize MockChainState era
firstSt Int -> Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== MockChainState era -> Int
forall era. MockChainState era -> Int
getUtxoSize MockChainState era
lastSt Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n
    getUtxoSize :: MockChainState era -> Int
    getUtxoSize :: forall era. MockChainState era -> Int
getUtxoSize MockChainState era
state = (Map TxIn (TxOut era) -> Int
forall k a. Map k a -> Int
Map.size (Map TxIn (TxOut era) -> Int)
-> (MockChainState era -> Map TxIn (TxOut era))
-> MockChainState era
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxO era -> Map TxIn (TxOut era)
forall era. UTxO era -> Map TxIn (TxOut era)
unUTxO (UTxO era -> Map TxIn (TxOut era))
-> (MockChainState era -> UTxO era)
-> MockChainState era
-> Map TxIn (TxOut era)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UTxOState era -> UTxO era
forall era. UTxOState era -> UTxO era
utxosUtxo (UTxOState era -> UTxO era)
-> (MockChainState era -> UTxOState era)
-> MockChainState era
-> UTxO era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. LedgerState era -> UTxOState era
forall era. LedgerState era -> UTxOState era
lsUTxOState (LedgerState era -> UTxOState era)
-> (MockChainState era -> LedgerState era)
-> MockChainState 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)
-> (MockChainState era -> EpochState era)
-> MockChainState 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)
-> (MockChainState era -> NewEpochState era)
-> MockChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes) MockChainState era
state

aggUTxO ::
  forall era.
  ( HasTrace (MOCKCHAIN era) (Gen1 era)
  , Reflect era
  ) =>
  Proof era ->
  Gen Property
aggUTxO :: forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), Reflect era) =>
Proof era -> Gen Property
aggUTxO Proof era
proof = do
  Trace (MOCKCHAIN era)
trace1 <- Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
proof Int
100 (GenSize
forall a. Default a => a
def {blocksizeMax = 4, slotDelta = (6, 12)}) GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
  Property -> Gen Property
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Property -> Gen Property) -> Property -> Gen Property
forall a b. (a -> b) -> a -> b
$ Proof era -> Trace (MOCKCHAIN era) -> Property
forall era.
EraTx era =>
Proof era -> Trace (MOCKCHAIN era) -> Property
consistentUtxoSizeProp Proof era
proof Trace (MOCKCHAIN era)
trace1

aggTests :: TestTree
aggTests :: TestTree
aggTests =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"tests, aggregating Tx's over a Trace."
    [ Int -> TestName -> Gen Property -> TestTree
forall prop. Testable prop => Int -> TestName -> prop -> TestTree
testPropMax Int
30 TestName
"UTxO size in Babbage" (Proof BabbageEra -> Gen Property
forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), Reflect era) =>
Proof era -> Gen Property
aggUTxO Proof BabbageEra
Babbage)
    , Int -> TestName -> Gen Property -> TestTree
forall prop. Testable prop => Int -> TestName -> prop -> TestTree
testPropMax Int
30 TestName
"UTxO size in Alonzo" (Proof AlonzoEra -> Gen Property
forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), Reflect era) =>
Proof era -> Gen Property
aggUTxO Proof AlonzoEra
Alonzo)
    , Int -> TestName -> Gen Property -> TestTree
forall prop. Testable prop => Int -> TestName -> prop -> TestTree
testPropMax Int
30 TestName
"UTxO size in Mary" (Proof MaryEra -> Gen Property
forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), Reflect era) =>
Proof era -> Gen Property
aggUTxO Proof MaryEra
Mary)
    ]

-- ===============================================================

-- TODO. An analog of   Test.Cardano.Ledger.Shelley.Rules.TestChain(forAllChainTrace)
-- We will add additional analogs (ledgerTraceFromBlock, poolTraceFromBlock) soon,
-- and then redo the tests in that module in the Generic fashion
forAllChainTrace ::
  (Testable prop, Reflect era) => Proof era -> Int -> (Trace (MOCKCHAIN era) -> prop) -> Property
forAllChainTrace :: forall prop era.
(Testable prop, Reflect era) =>
Proof era -> Int -> (Trace (MOCKCHAIN era) -> prop) -> Property
forAllChainTrace p :: Proof era
p@Proof era
Conway Int
n Trace (MOCKCHAIN era) -> prop
propf =
  Gen prop -> Property
forall prop. Testable prop => prop -> Property
property (Gen prop -> Property) -> Gen prop -> Property
forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf (Trace (MOCKCHAIN era) -> prop)
-> Gen (Trace (MOCKCHAIN era)) -> Gen prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
p Int
n (GenSize
forall a. Default a => a
def {blocksizeMax = 4, slotDelta = (6, 12)}) GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Babbage Int
n Trace (MOCKCHAIN era) -> prop
propf =
  Gen prop -> Property
forall prop. Testable prop => prop -> Property
property (Gen prop -> Property) -> Gen prop -> Property
forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf (Trace (MOCKCHAIN era) -> prop)
-> Gen (Trace (MOCKCHAIN era)) -> Gen prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
p Int
n (GenSize
forall a. Default a => a
def {blocksizeMax = 4, slotDelta = (6, 12)}) GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Alonzo Int
n Trace (MOCKCHAIN era) -> prop
propf =
  Gen prop -> Property
forall prop. Testable prop => prop -> Property
property (Gen prop -> Property) -> Gen prop -> Property
forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf (Trace (MOCKCHAIN era) -> prop)
-> Gen (Trace (MOCKCHAIN era)) -> Gen prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
p Int
n (GenSize
forall a. Default a => a
def {blocksizeMax = 4, slotDelta = (6, 12)}) GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Mary Int
n Trace (MOCKCHAIN era) -> prop
propf =
  Gen prop -> Property
forall prop. Testable prop => prop -> Property
property (Gen prop -> Property) -> Gen prop -> Property
forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf (Trace (MOCKCHAIN era) -> prop)
-> Gen (Trace (MOCKCHAIN era)) -> Gen prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
p Int
n (GenSize
forall a. Default a => a
def {blocksizeMax = 4, slotDelta = (6, 12)}) GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Allegra Int
n Trace (MOCKCHAIN era) -> prop
propf =
  Gen prop -> Property
forall prop. Testable prop => prop -> Property
property (Gen prop -> Property) -> Gen prop -> Property
forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf (Trace (MOCKCHAIN era) -> prop)
-> Gen (Trace (MOCKCHAIN era)) -> Gen prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
p Int
n (GenSize
forall a. Default a => a
def {blocksizeMax = 4, slotDelta = (6, 12)}) GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Shelley Int
n Trace (MOCKCHAIN era) -> prop
propf =
  Gen prop -> Property
forall prop. Testable prop => prop -> Property
property (Gen prop -> Property) -> Gen prop -> Property
forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf (Trace (MOCKCHAIN era) -> prop)
-> Gen (Trace (MOCKCHAIN era)) -> Gen prop
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
forall era.
(Reflect era, HasTrace (MOCKCHAIN era) (Gen1 era)) =>
Proof era
-> Int -> GenSize -> GenRS era () -> Gen (Trace (MOCKCHAIN era))
genTrace Proof era
p Int
n (GenSize
forall a. Default a => a
def {blocksizeMax = 4, slotDelta = (6, 12)}) GenRS era ()
forall era. Reflect era => GenRS era ()
initStableFields

-- ===========================================================

-- | Check that the sum of Key Deposits and the Pool Depoits are equal to the utxosDeposits
depositInvariant ::
  EraCertState era =>
  SourceSignalTarget (MOCKCHAIN era) ->
  Property
depositInvariant :: forall era.
EraCertState era =>
SourceSignalTarget (MOCKCHAIN era) -> Property
depositInvariant SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (MOCKCHAIN era)
mockChainSt} =
  let LedgerState {lsUTxOState :: forall era. LedgerState era -> UTxOState era
lsUTxOState = UTxOState era
utxost, lsCertState :: forall era. LedgerState era -> CertState era
lsCertState = CertState era
certState} = (EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (MockChainState era -> EpochState era)
-> MockChainState 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)
-> (MockChainState era -> NewEpochState era)
-> MockChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes) State (MOCKCHAIN era)
MockChainState era
mockChainSt
      -- TODO handle VState
      pstate :: PState era
pstate = CertState era
certState CertState era
-> Getting (PState era) (CertState era) (PState era) -> PState era
forall s a. s -> Getting a s a -> a
^. Getting (PState era) (CertState era) (PState era)
forall era. EraCertState era => Lens' (CertState era) (PState era)
Lens' (CertState era) (PState era)
certPStateL
      dstate :: DState era
dstate = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
      allDeposits :: Coin
allDeposits = UTxOState era -> Coin
forall era. UTxOState era -> Coin
utxosDeposited UTxOState era
utxost
      sumCoin :: Map k Coin -> Coin
sumCoin Map k Coin
m = (Coin -> Coin -> Coin) -> Coin -> Map k Coin -> Coin
forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
(<+>) (Integer -> Coin
Coin Integer
0) Map k Coin
m
      keyDeposits :: Coin
keyDeposits = CompactForm Coin -> Coin
forall a. Compactible a => CompactForm a -> a
fromCompact (CompactForm Coin -> Coin) -> CompactForm Coin -> Coin
forall a b. (a -> b) -> a -> b
$ UView (Credential 'Staking) RDPair -> CompactForm Coin
forall k. UView k RDPair -> CompactForm Coin
sumDepositUView (UMap -> UView (Credential 'Staking) RDPair
RewDepUView (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dstate))
      poolDeposits :: Coin
poolDeposits = Map (KeyHash 'StakePool) Coin -> Coin
forall {k}. Map k Coin -> Coin
sumCoin (PState era -> Map (KeyHash 'StakePool) Coin
forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits PState era
pstate)
   in TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
        ( Doc AnsiStyle -> TestName
ansiDocToString (Doc AnsiStyle -> TestName)
-> ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle]
-> TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
Pretty.vsep ([Doc AnsiStyle] -> TestName) -> [Doc AnsiStyle] -> TestName
forall a b. (a -> b) -> a -> b
$
            [ Doc AnsiStyle
"Deposit invariant fails:"
            , Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
Pretty.indent Int
2 (Doc AnsiStyle -> Doc AnsiStyle)
-> ([TestName] -> Doc AnsiStyle) -> [TestName] -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
Pretty.vsep ([Doc AnsiStyle] -> Doc AnsiStyle)
-> ([TestName] -> [Doc AnsiStyle]) -> [TestName] -> Doc AnsiStyle
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TestName -> Doc AnsiStyle) -> [TestName] -> [Doc AnsiStyle]
forall a b. (a -> b) -> [a] -> [b]
map TestName -> Doc AnsiStyle
forall ann. TestName -> Doc ann
forall a ann. Pretty a => a -> Doc ann
Pretty.pretty ([TestName] -> Doc AnsiStyle) -> [TestName] -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$
                [ TestName
"All deposits = " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Coin -> TestName
forall a. Show a => a -> TestName
show Coin
allDeposits
                , TestName
"Key deposits = " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Maybe (Map (Credential 'Staking) Coin) -> TestName
forall k. Maybe (Map k Coin) -> TestName
synopsisCoinMap (Map (Credential 'Staking) Coin
-> Maybe (Map (Credential 'Staking) Coin)
forall a. a -> Maybe a
Just (UMap -> Map (Credential 'Staking) Coin
depositMap (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dstate)))
                , TestName
"Pool deposits = " TestName -> TestName -> TestName
forall a. [a] -> [a] -> [a]
++ Maybe (Map (KeyHash 'StakePool) Coin) -> TestName
forall k. Maybe (Map k Coin) -> TestName
synopsisCoinMap (Map (KeyHash 'StakePool) Coin
-> Maybe (Map (KeyHash 'StakePool) Coin)
forall a. a -> Maybe a
Just (PState era -> Map (KeyHash 'StakePool) Coin
forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits PState era
pstate))
                ]
            ]
        )
        (Coin
allDeposits Coin -> Coin -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Coin
keyDeposits Coin -> Coin -> Coin
forall t. Val t => t -> t -> t
<+> Coin
poolDeposits)

rewardDepositDomainInvariant ::
  EraCertState era =>
  SourceSignalTarget (MOCKCHAIN era) ->
  Property
rewardDepositDomainInvariant :: forall era.
EraCertState era =>
SourceSignalTarget (MOCKCHAIN era) -> Property
rewardDepositDomainInvariant SourceSignalTarget {source :: forall a. SourceSignalTarget a -> State a
source = State (MOCKCHAIN era)
mockChainSt} =
  let LedgerState {lsCertState :: forall era. LedgerState era -> CertState era
lsCertState = CertState era
certState} = (EpochState era -> LedgerState era
forall era. EpochState era -> LedgerState era
esLState (EpochState era -> LedgerState era)
-> (MockChainState era -> EpochState era)
-> MockChainState 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)
-> (MockChainState era -> NewEpochState era)
-> MockChainState era
-> EpochState era
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MockChainState era -> NewEpochState era
forall era. MockChainState era -> NewEpochState era
mcsNes) State (MOCKCHAIN era)
MockChainState era
mockChainSt
      -- TODO VState
      dstate :: DState era
dstate = CertState era
certState CertState era
-> Getting (DState era) (CertState era) (DState era) -> DState era
forall s a. s -> Getting a s a -> a
^. Getting (DState era) (CertState era) (DState era)
forall era. EraCertState era => Lens' (CertState era) (DState era)
Lens' (CertState era) (DState era)
certDStateL
      rewardDomain :: Set (Credential 'Staking)
rewardDomain = UView (Credential 'Staking) RDPair -> Set (Credential 'Staking)
forall k v. UView k v -> Set k
domain (UMap -> UView (Credential 'Staking) RDPair
RewDepUView (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dstate))
      depositDomain :: Set (Credential 'Staking)
depositDomain = Map (Credential 'Staking) Coin -> Set (Credential 'Staking)
forall k a. Map k a -> Set k
Map.keysSet (UMap -> Map (Credential 'Staking) Coin
depositMap (DState era -> UMap
forall era. DState era -> UMap
dsUnified DState era
dstate))
   in TestName -> Property -> Property
forall prop. Testable prop => TestName -> prop -> Property
counterexample
        ( Doc AnsiStyle -> TestName
ansiDocToString (Doc AnsiStyle -> TestName)
-> ([Doc AnsiStyle] -> Doc AnsiStyle)
-> [Doc AnsiStyle]
-> TestName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Doc AnsiStyle] -> Doc AnsiStyle
forall ann. [Doc ann] -> Doc ann
Pretty.vsep ([Doc AnsiStyle] -> TestName) -> [Doc AnsiStyle] -> TestName
forall a b. (a -> b) -> a -> b
$
            [ Doc AnsiStyle
"Reward-Deposit domain invariant fails:"
            , Int -> Doc AnsiStyle -> Doc AnsiStyle
forall ann. Int -> Doc ann -> Doc ann
Pretty.indent Int
2 (Doc AnsiStyle -> Doc AnsiStyle) -> Doc AnsiStyle -> Doc AnsiStyle
forall a b. (a -> b) -> a -> b
$ Set (Credential 'Staking)
-> Set (Credential 'Staking) -> Doc AnsiStyle
forall a. ToExpr a => a -> a -> Doc AnsiStyle
diffExpr Set (Credential 'Staking)
rewardDomain Set (Credential 'Staking)
depositDomain
            ]
        )
        (Set (Credential 'Staking)
rewardDomain Set (Credential 'Staking) -> Set (Credential 'Staking) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Set (Credential 'Staking)
depositDomain)

itemPropToTraceProp ::
  (SourceSignalTarget (MOCKCHAIN era) -> Property) -> Trace (MOCKCHAIN era) -> Property
itemPropToTraceProp :: forall era.
(SourceSignalTarget (MOCKCHAIN era) -> Property)
-> Trace (MOCKCHAIN era) -> Property
itemPropToTraceProp SourceSignalTarget (MOCKCHAIN era) -> Property
f Trace (MOCKCHAIN era)
trace1 = [Property] -> Property
forall prop. Testable prop => [prop] -> Property
conjoin ((SourceSignalTarget (MOCKCHAIN era) -> Property)
-> [SourceSignalTarget (MOCKCHAIN era)] -> [Property]
forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (MOCKCHAIN era) -> Property
f (Trace (MOCKCHAIN era) -> [SourceSignalTarget (MOCKCHAIN era)]
forall a. Trace a -> [SourceSignalTarget a]
sourceSignalTargets Trace (MOCKCHAIN era)
trace1))

depositEra :: forall era. Reflect era => Proof era -> TestTree
depositEra :: forall era. Reflect era => Proof era -> TestTree
depositEra Proof era
proof =
  TestName -> [TestTree] -> TestTree
testGroup
    (Proof era -> TestName
forall a. Show a => a -> TestName
show Proof era
proof)
    [ TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
        TestName
"Deposits = KeyDeposits + PoolDeposits"
        (Proof era -> Int -> (Trace (MOCKCHAIN era) -> Property) -> Property
forall prop era.
(Testable prop, Reflect era) =>
Proof era -> Int -> (Trace (MOCKCHAIN era) -> prop) -> Property
forAllChainTrace Proof era
proof Int
10 ((SourceSignalTarget (MOCKCHAIN era) -> Property)
-> Trace (MOCKCHAIN era) -> Property
forall era.
(SourceSignalTarget (MOCKCHAIN era) -> Property)
-> Trace (MOCKCHAIN era) -> Property
itemPropToTraceProp (forall era.
EraCertState era =>
SourceSignalTarget (MOCKCHAIN era) -> Property
depositInvariant @era)))
    , TestName -> Property -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty
        TestName
"Reward domain = Deposit domain"
        (Proof era -> Int -> (Trace (MOCKCHAIN era) -> Property) -> Property
forall prop era.
(Testable prop, Reflect era) =>
Proof era -> Int -> (Trace (MOCKCHAIN era) -> prop) -> Property
forAllChainTrace Proof era
proof Int
10 ((SourceSignalTarget (MOCKCHAIN era) -> Property)
-> Trace (MOCKCHAIN era) -> Property
forall era.
(SourceSignalTarget (MOCKCHAIN era) -> Property)
-> Trace (MOCKCHAIN era) -> Property
itemPropToTraceProp (forall era.
EraCertState era =>
SourceSignalTarget (MOCKCHAIN era) -> Property
rewardDepositDomainInvariant @era)))
    ]

-- | Build a TestTree that tests 'f' at all the Eras listed in 'ps'
testEras :: String -> [Some Proof] -> (forall era. Reflect era => Proof era -> TestTree) -> TestTree
testEras :: TestName
-> [Some Proof]
-> (forall era. Reflect era => Proof era -> TestTree)
-> TestTree
testEras TestName
message [Some Proof]
ps forall era. Reflect era => Proof era -> TestTree
f = TestName -> [TestTree] -> TestTree
testGroup TestName
message ([Some Proof] -> [TestTree]
applyF [Some Proof]
ps)
  where
    applyF :: [Some Proof] -> [TestTree]
applyF [] = []
    applyF (Some Proof i
e : [Some Proof]
more) = (Reflect i => Proof i -> TestTree) -> Proof i -> TestTree
forall era a. (Reflect era => Proof era -> a) -> Proof era -> a
unReflect Reflect i => Proof i -> TestTree
Proof i -> TestTree
forall era. Reflect era => Proof era -> TestTree
f Proof i
e TestTree -> [TestTree] -> [TestTree]
forall a. a -> [a] -> [a]
: [Some Proof] -> [TestTree]
applyF [Some Proof]
more

depositTests :: TestTree
depositTests :: TestTree
depositTests = TestName
-> [Some Proof]
-> (forall era. Reflect era => Proof era -> TestTree)
-> TestTree
testEras TestName
"deposit invariants" [Some Proof]
preBabbage Proof era -> TestTree
forall era. Reflect era => Proof era -> TestTree
depositEra