{-# 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 (
CertState (..),
DState (..),
EpochState (..),
LedgerState (..),
NewEpochState (..),
PState (..),
UTxOState (..),
)
import Cardano.Ledger.Shelley.Rules.Reports (synopsisCoinMap)
import Cardano.Ledger.UMap (UView (RewDepUView), depositMap, domain, fromCompact, sumDepositUView)
import Cardano.Ledger.UTxO (UTxO (..))
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 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 (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 = forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace sts
trace
(State sts
firstState, State sts
lastState) = forall s. Trace s -> (State s, State s)
firstAndLastState Trace sts
trace
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 = forall agg sts prop.
agg
-> (agg -> Signal sts -> agg)
-> (State sts -> State sts -> agg -> prop)
-> Trace sts
-> prop
aggProp Int
agg0 Int -> MockBlock era -> Int
aggregate 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) = 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
forall a. Num a => a -> a -> a
+ ( if Bool
valid
then forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall era.
EraTxBody era =>
Proof era -> TxBody era -> StrictSeq (TxOut era)
getOutputs Proof era
proof TxBody era
body) forall a. Num a => a -> a -> a
- forall a. Set a -> Int
Set.size (forall era. EraTxBody era => Proof era -> TxBody era -> Set TxIn
getInputs Proof era
proof TxBody era
body)
else forall (t :: * -> *) a. Foldable t => t a -> Int
length (forall era. Proof era -> TxBody era -> [TxOut era]
getCollateralOutputs Proof era
proof TxBody era
body) forall a. Num a => a -> a -> a
- forall a. Set a -> Int
Set.size (forall era. Proof era -> TxBody era -> Set TxIn
getCollateralInputs Proof era
proof TxBody era
body)
)
where
body :: TxBody era
body = forall era. EraTx era => Proof era -> Tx era -> TxBody era
getBody Proof era
proof Tx era
tx
IsValid Bool
valid = 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 = forall era. MockChainState era -> Int
getUtxoSize MockChainState era
firstSt forall a. (Eq a, Show a) => a -> a -> Property
=== forall era. MockChainState era -> Int
getUtxoSize MockChainState era
lastSt forall a. Num a => a -> a -> a
- Int
n
getUtxoSize :: MockChainState era -> Int
getUtxoSize :: forall era. MockChainState era -> Int
getUtxoSize MockChainState era
state = (forall k a. Map k a -> Int
Map.size forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. UTxO era -> Map TxIn (TxOut era)
unUTxO forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. UTxOState era -> UTxO era
utxosUtxo forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. LedgerState era -> UTxOState era
lsUTxOState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. 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 <- 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 (forall a. Default a => a
def {blocksizeMax :: Integer
blocksizeMax = Integer
4, slotDelta :: (Word64, Word64)
slotDelta = (Word64
6, Word64
12)}) forall era. Reflect era => GenRS era ()
initStableFields
forall (f :: * -> *) a. Applicative f => a -> f a
pure forall a b. (a -> b) -> a -> b
$ 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."
[ forall prop. Testable prop => Int -> TestName -> prop -> TestTree
testPropMax Int
30 TestName
"UTxO size in Babbage" (forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), Reflect era) =>
Proof era -> Gen Property
aggUTxO Proof BabbageEra
Babbage)
, forall prop. Testable prop => Int -> TestName -> prop -> TestTree
testPropMax Int
30 TestName
"UTxO size in Alonzo" (forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), Reflect era) =>
Proof era -> Gen Property
aggUTxO Proof AlonzoEra
Alonzo)
, forall prop. Testable prop => Int -> TestName -> prop -> TestTree
testPropMax Int
30 TestName
"UTxO size in Mary" (forall era.
(HasTrace (MOCKCHAIN era) (Gen1 era), Reflect era) =>
Proof era -> Gen Property
aggUTxO Proof MaryEra
Mary)
]
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 =
forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall a. Default a => a
def {blocksizeMax :: Integer
blocksizeMax = Integer
4, slotDelta :: (Word64, Word64)
slotDelta = (Word64
6, Word64
12)}) forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Babbage Int
n Trace (MOCKCHAIN era) -> prop
propf =
forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall a. Default a => a
def {blocksizeMax :: Integer
blocksizeMax = Integer
4, slotDelta :: (Word64, Word64)
slotDelta = (Word64
6, Word64
12)}) forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Alonzo Int
n Trace (MOCKCHAIN era) -> prop
propf =
forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall a. Default a => a
def {blocksizeMax :: Integer
blocksizeMax = Integer
4, slotDelta :: (Word64, Word64)
slotDelta = (Word64
6, Word64
12)}) forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Mary Int
n Trace (MOCKCHAIN era) -> prop
propf =
forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall a. Default a => a
def {blocksizeMax :: Integer
blocksizeMax = Integer
4, slotDelta :: (Word64, Word64)
slotDelta = (Word64
6, Word64
12)}) forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Allegra Int
n Trace (MOCKCHAIN era) -> prop
propf =
forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall a. Default a => a
def {blocksizeMax :: Integer
blocksizeMax = Integer
4, slotDelta :: (Word64, Word64)
slotDelta = (Word64
6, Word64
12)}) forall era. Reflect era => GenRS era ()
initStableFields
forAllChainTrace p :: Proof era
p@Proof era
Shelley Int
n Trace (MOCKCHAIN era) -> prop
propf =
forall prop. Testable prop => prop -> Property
property forall a b. (a -> b) -> a -> b
$ Trace (MOCKCHAIN era) -> prop
propf forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 (forall a. Default a => a
def {blocksizeMax :: Integer
blocksizeMax = Integer
4, slotDelta :: (Word64, Word64)
slotDelta = (Word64
6, Word64
12)}) forall era. Reflect era => GenRS era ()
initStableFields
depositInvariant ::
SourceSignalTarget (MOCKCHAIN era) ->
Property
depositInvariant :: forall 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 VState era
_vstate PState era
pstate DState era
dstate} = (forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. MockChainState era -> NewEpochState era
mcsNes) State (MOCKCHAIN era)
mockChainSt
allDeposits :: Coin
allDeposits = forall era. UTxOState era -> Coin
utxosDeposited UTxOState era
utxost
sumCoin :: Map k Coin -> Coin
sumCoin Map k Coin
m = forall a b k. (a -> b -> a) -> a -> Map k b -> a
Map.foldl' forall t. Val t => t -> t -> t
(<+>) (Integer -> Coin
Coin Integer
0) Map k Coin
m
keyDeposits :: Coin
keyDeposits = forall a. Compactible a => CompactForm a -> a
fromCompact forall a b. (a -> b) -> a -> b
$ forall k. UView k RDPair -> CompactForm Coin
sumDepositUView (UMap -> UView (Credential 'Staking) RDPair
RewDepUView (forall era. DState era -> UMap
dsUnified DState era
dstate))
poolDeposits :: Coin
poolDeposits = forall {k}. Map k Coin -> Coin
sumCoin (forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits PState era
pstate)
in forall prop. Testable prop => TestName -> prop -> Property
counterexample
( Doc AnsiStyle -> TestName
ansiDocToString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. [Doc ann] -> Doc ann
Pretty.vsep forall a b. (a -> b) -> a -> b
$
[ Doc AnsiStyle
"Deposit invariant fails:"
, forall ann. Int -> Doc ann -> Doc ann
Pretty.indent Int
2 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. [Doc ann] -> Doc ann
Pretty.vsep forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map forall a ann. Pretty a => a -> Doc ann
Pretty.pretty forall a b. (a -> b) -> a -> b
$
[ TestName
"All deposits = " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> TestName
show Coin
allDeposits
, TestName
"Key deposits = " forall a. [a] -> [a] -> [a]
++ forall k. Maybe (Map k Coin) -> TestName
synopsisCoinMap (forall a. a -> Maybe a
Just (UMap -> Map (Credential 'Staking) Coin
depositMap (forall era. DState era -> UMap
dsUnified DState era
dstate)))
, TestName
"Pool deposits = " forall a. [a] -> [a] -> [a]
++ forall k. Maybe (Map k Coin) -> TestName
synopsisCoinMap (forall a. a -> Maybe a
Just (forall era. PState era -> Map (KeyHash 'StakePool) Coin
psDeposits PState era
pstate))
]
]
)
(Coin
allDeposits forall a. (Eq a, Show a) => a -> a -> Property
=== Coin
keyDeposits forall t. Val t => t -> t -> t
<+> Coin
poolDeposits)
rewardDepositDomainInvariant ::
SourceSignalTarget (MOCKCHAIN era) ->
Property
rewardDepositDomainInvariant :: forall 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 VState era
_ PState era
_ DState era
dstate} = (forall era. EpochState era -> LedgerState era
esLState forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. NewEpochState era -> EpochState era
nesEs forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall era. MockChainState era -> NewEpochState era
mcsNes) State (MOCKCHAIN era)
mockChainSt
rewardDomain :: Set (Credential 'Staking)
rewardDomain = forall k v. UView k v -> Set k
domain (UMap -> UView (Credential 'Staking) RDPair
RewDepUView (forall era. DState era -> UMap
dsUnified DState era
dstate))
depositDomain :: Set (Credential 'Staking)
depositDomain = forall k a. Map k a -> Set k
Map.keysSet (UMap -> Map (Credential 'Staking) Coin
depositMap (forall era. DState era -> UMap
dsUnified DState era
dstate))
in forall prop. Testable prop => TestName -> prop -> Property
counterexample
( Doc AnsiStyle -> TestName
ansiDocToString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall ann. [Doc ann] -> Doc ann
Pretty.vsep forall a b. (a -> b) -> a -> b
$
[ Doc AnsiStyle
"Reward-Deposit domain invariant fails:"
, forall ann. Int -> Doc ann -> Doc ann
Pretty.indent Int
2 forall a b. (a -> b) -> a -> b
$ forall a. ToExpr a => a -> a -> Doc AnsiStyle
diffExpr Set (Credential 'Staking)
rewardDomain Set (Credential 'Staking)
depositDomain
]
)
(Set (Credential 'Staking)
rewardDomain 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 = forall prop. Testable prop => [prop] -> Property
conjoin (forall a b. (a -> b) -> [a] -> [b]
map SourceSignalTarget (MOCKCHAIN era) -> Property
f (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
(forall a. Show a => a -> TestName
show Proof era
proof)
[ forall a. Testable a => TestName -> a -> TestTree
testProperty
TestName
"Deposits = KeyDeposits + PoolDeposits"
(forall prop era.
(Testable prop, Reflect era) =>
Proof era -> Int -> (Trace (MOCKCHAIN era) -> prop) -> Property
forAllChainTrace Proof era
proof Int
10 (forall era.
(SourceSignalTarget (MOCKCHAIN era) -> Property)
-> Trace (MOCKCHAIN era) -> Property
itemPropToTraceProp (forall era. SourceSignalTarget (MOCKCHAIN era) -> Property
depositInvariant @era)))
, forall a. Testable a => TestName -> a -> TestTree
testProperty
TestName
"Reward domain = Deposit domain"
(forall prop era.
(Testable prop, Reflect era) =>
Proof era -> Int -> (Trace (MOCKCHAIN era) -> prop) -> Property
forAllChainTrace Proof era
proof Int
10 (forall era.
(SourceSignalTarget (MOCKCHAIN era) -> Property)
-> Trace (MOCKCHAIN era) -> Property
itemPropToTraceProp (forall era. SourceSignalTarget (MOCKCHAIN era) -> Property
rewardDepositDomainInvariant @era)))
]
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) = forall era a. (Reflect era => Proof era -> a) -> Proof era -> a
unReflect forall era. Reflect era => Proof era -> TestTree
f Proof i
e 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 forall era. Reflect era => Proof era -> TestTree
depositEra