{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Test.Byron.AbstractSize.Properties (testAbstractSize, testProperty) where

import Byron.Spec.Chain.STS.Block (Block (..), BlockBody (..), BlockHeader (..))
import Byron.Spec.Chain.STS.Rule.Chain (CHAIN)
import Byron.Spec.Ledger.Core hiding ((<|))
import Byron.Spec.Ledger.Delegation (DCert)
import Byron.Spec.Ledger.UTxO
import Byron.Spec.Ledger.Update (ProtVer (..), UProp (..), Vote)
import Data.AbstractSize
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map
import Data.Maybe (maybeToList)
import Data.Sequence ((<|), (><))
import qualified Data.Sequence as Seq
import qualified Data.Set as Set
import Data.Typeable (TypeRep, Typeable, typeOf)
import Data.Word (Word64)
import Hedgehog (MonadTest, Property, diff, forAll, property, withTests, (===))
import Hedgehog.Internal.Property (PropertyName (..))
import Numeric.Natural (Natural)
import Test.Control.State.Transition.Generator (trace)
import Test.Control.State.Transition.Trace (TraceOrder (OldestFirst), traceSignals)
import Test.Tasty (TestName, TestTree, testGroup)
import Test.Tasty.HUnit (Assertion, testCase, (@?=))
import Test.Tasty.Hedgehog hiding (testProperty)

-- | testProperty has been deprecated. We make our own version here.
testProperty :: TestName -> Property -> TestTree
testProperty :: TestName -> Property -> TestTree
testProperty TestName
s Property
p = TestName -> PropertyName -> Property -> TestTree
testPropertyNamed TestName
s (TestName -> PropertyName
Hedgehog.Internal.Property.PropertyName TestName
s) Property
p

--------------------------------------------------------------------------------
-- Example typeReps for Block/Header/Body
--------------------------------------------------------------------------------

aTx :: TxBody
aTx :: TxBody
aTx = TxBody
forall a. HasCallStack => a
undefined

aTxId :: TxId
aTxId :: TxId
aTxId = Hash -> TxId
TxId (TxBody -> Hash
forall a. HasHash a => a -> Hash
hash TxBody
aTx)

aHeader :: BlockHeader
aHeader :: BlockHeader
aHeader =
  BlockHeader
    { _bhPrevHash :: Hash
_bhPrevHash = Hash
forall a. HasCallStack => a
undefined :: Hash
    , _bhSlot :: Slot
_bhSlot = Slot
forall a. HasCallStack => a
undefined :: Slot
    , _bhIssuer :: VKey
_bhIssuer = VKey
forall a. HasCallStack => a
undefined :: VKey
    , _bhSig :: Sig Hash
_bhSig = Sig Hash
forall a. HasCallStack => a
undefined :: Sig Hash
    , _bhUtxoHash :: Hash
_bhUtxoHash = Hash
forall a. HasCallStack => a
undefined :: Hash
    , _bhDlgHash :: Hash
_bhDlgHash = Hash
forall a. HasCallStack => a
undefined :: Hash
    , _bhUpdHash :: Hash
_bhUpdHash = Hash
forall a. HasCallStack => a
undefined :: Hash
    }

aTxWits :: Tx
aTxWits :: Tx
aTxWits =
  let (TxIn
in0, TxIn
in1) = (TxId -> Natural -> TxIn
TxIn TxId
aTxId Natural
0, TxId -> Natural -> TxIn
TxIn TxId
aTxId Natural
1)
      outs :: [a]
outs = []
      wits :: [a]
wits = []
   in TxBody -> [Wit] -> Tx
Tx ([TxIn] -> [TxOut] -> TxBody
TxBody [TxIn
in0, TxIn
in1] [TxOut]
forall a. [a]
outs) [Wit]
forall a. [a]
wits

aBody :: BlockBody
aBody :: BlockBody
aBody =
  BlockBody
    { _bDCerts :: [DCert]
_bDCerts = []
    , _bUtxo :: [Tx]
_bUtxo = [Tx
aTxWits, Tx
aTxWits]
    , _bUpdProp :: Maybe UProp
_bUpdProp = Maybe UProp
forall a. Maybe a
Nothing
    , _bUpdVotes :: [Vote]
_bUpdVotes = []
    , _bProtVer :: ProtVer
_bProtVer =
        ProtVer
          { _pvMaj :: Natural
_pvMaj = Natural
0
          , _pvMin :: Natural
_pvMin = Natural
1
          , _pvAlt :: Natural
_pvAlt = Natural
1
          }
    }

aBlock :: Block
aBlock :: Block
aBlock =
  Block
    { _bHeader :: BlockHeader
_bHeader = BlockHeader
aHeader
    , _bBody :: BlockBody
_bBody = BlockBody
aBody
    }

-- | A BlockHeader term has fixed typeReps
exampleTypeRepsBlockHeader :: Assertion
exampleTypeRepsBlockHeader :: Assertion
exampleTypeRepsBlockHeader =
  BlockHeader -> Seq TypeRep
forall a. HasTypeReps a => a -> Seq TypeRep
typeReps BlockHeader
aHeader
    Seq TypeRep -> Seq TypeRep -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= [TypeRep] -> Seq TypeRep
forall a. [a] -> Seq a
Seq.fromList
      [ BlockHeader -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (BlockHeader
forall a. HasCallStack => a
undefined :: BlockHeader)
      , Hash -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Hash
forall a. HasCallStack => a
undefined :: Hash)
      , Hash -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Hash
forall a. HasCallStack => a
undefined :: Hash)
      , Hash -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Hash
forall a. HasCallStack => a
undefined :: Hash)
      , Hash -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Hash
forall a. HasCallStack => a
undefined :: Hash)
      , Slot -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Slot
forall a. HasCallStack => a
undefined :: Slot)
      , Word64 -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Word64
forall a. HasCallStack => a
undefined :: Word64)
      , VKey -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (VKey
forall a. HasCallStack => a
undefined :: VKey)
      , Owner -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Owner
forall a. HasCallStack => a
undefined :: Owner)
      , Natural -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Natural
forall a. HasCallStack => a
undefined :: Natural)
      , Sig Hash -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Sig Hash
forall a. HasCallStack => a
undefined :: Sig Hash)
      ]

-- | A BlockBody has variable typeReps, depending on the collections
-- [DCert], [TxWits], [Vote] and [STag] (in UProp)
--
--   In this example, we can see the repetition of typeReps for 2 TxWits
exampleTypeRepsBlockBody :: Assertion
exampleTypeRepsBlockBody :: Assertion
exampleTypeRepsBlockBody =
  BlockBody -> Seq TypeRep
forall a. HasTypeReps a => a -> Seq TypeRep
typeReps BlockBody
aBody
    Seq TypeRep -> Seq TypeRep -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= [TypeRep] -> Seq TypeRep
forall a. [a] -> Seq a
Seq.fromList
      [ BlockBody -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (BlockBody
forall a. HasCallStack => a
undefined :: BlockBody)
      , [DCert] -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf ([DCert]
forall a. HasCallStack => a
undefined :: [DCert])
      , [Tx] -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf ([Tx]
forall a. HasCallStack => a
undefined :: [Tx])
      ]
      Seq TypeRep -> Seq TypeRep -> Seq TypeRep
forall a. Seq a -> Seq a -> Seq a
>< Tx -> Seq TypeRep
forall a. HasTypeReps a => a -> Seq TypeRep
typeReps Tx
aTxWits
      Seq TypeRep -> Seq TypeRep -> Seq TypeRep
forall a. Seq a -> Seq a -> Seq a
>< Tx -> Seq TypeRep
forall a. HasTypeReps a => a -> Seq TypeRep
typeReps Tx
aTxWits
      Seq TypeRep -> Seq TypeRep -> Seq TypeRep
forall a. Seq a -> Seq a -> Seq a
>< [TypeRep] -> Seq TypeRep
forall a. [a] -> Seq a
Seq.fromList
        [ Maybe UProp -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Maybe UProp
forall a. HasCallStack => a
undefined :: Maybe UProp)
        , [Vote] -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf ([Vote]
forall a. HasCallStack => a
undefined :: [Vote])
        , ProtVer -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (ProtVer
forall a. HasCallStack => a
undefined :: ProtVer)
        , Natural -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Natural
forall a. HasCallStack => a
undefined :: Natural)
        , Natural -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Natural
forall a. HasCallStack => a
undefined :: Natural)
        , Natural -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Natural
forall a. HasCallStack => a
undefined :: Natural)
        ]

-- | The typeReps for a 'Block' is a combination of typeReps for
-- the header and body in the block.
exampleTypeRepsBlock :: Assertion
exampleTypeRepsBlock :: Assertion
exampleTypeRepsBlock =
  Block -> Seq TypeRep
forall a. HasTypeReps a => a -> Seq TypeRep
typeReps Block
aBlock
    Seq TypeRep -> Seq TypeRep -> Assertion
forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= Block -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (Block
forall a. HasCallStack => a
undefined :: Block)
      TypeRep -> Seq TypeRep -> Seq TypeRep
forall a. a -> Seq a -> Seq a
<| BlockHeader -> Seq TypeRep
forall a. HasTypeReps a => a -> Seq TypeRep
typeReps BlockHeader
aHeader
      Seq TypeRep -> Seq TypeRep -> Seq TypeRep
forall a. Seq a -> Seq a -> Seq a
>< BlockBody -> Seq TypeRep
forall a. HasTypeReps a => a -> Seq TypeRep
typeReps BlockBody
aBody

--------------------------------------------------------------------------------
-- Properties of abstractSize for Block/Header/Body
--------------------------------------------------------------------------------

-- | Make a singleton cost of "1" for the given term's type
mkCost :: forall a. Typeable a => Map TypeRep Size
mkCost :: forall a. Typeable a => Map TypeRep Size
mkCost = TypeRep -> Size -> Map TypeRep Size
forall k a. k -> a -> Map k a
Map.singleton (a -> TypeRep
forall a. Typeable a => a -> TypeRep
typeOf (a
forall a. HasCallStack => a
undefined :: a)) Size
1

-- | This property tests that for abstractSize
--   - we should account for each DCert/TxWits/Vote/UProp/STag in a Block Body
--   - the BlockHeader and BlockBody should each be counted only once
propMultipleOfSizesBlock ::
  MonadTest m => Block -> m ()
propMultipleOfSizesBlock :: forall (m :: * -> *). MonadTest m => Block -> m ()
propMultipleOfSizesBlock Block
b =
  let body_ :: BlockBody
body_ = Block -> BlockBody
_bBody Block
b
   in do
        Map TypeRep Size -> Block -> Size
forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @DCert) Block
b Size -> Size -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== [DCert] -> Size
forall a. [a] -> Size
forall (t :: * -> *) a. Foldable t => t a -> Size
length (BlockBody -> [DCert]
_bDCerts BlockBody
body_)
        Map TypeRep Size -> Block -> Size
forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @Tx) Block
b Size -> Size -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== [Tx] -> Size
forall a. [a] -> Size
forall (t :: * -> *) a. Foldable t => t a -> Size
length (BlockBody -> [Tx]
_bUtxo BlockBody
body_)
        Map TypeRep Size -> Block -> Size
forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @Vote) Block
b Size -> Size -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== [Vote] -> Size
forall a. [a] -> Size
forall (t :: * -> *) a. Foldable t => t a -> Size
length (BlockBody -> [Vote]
_bUpdVotes BlockBody
body_)
        Map TypeRep Size -> Block -> Size
forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @UProp) Block
b Size -> Size -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== [UProp] -> Size
forall a. [a] -> Size
forall (t :: * -> *) a. Foldable t => t a -> Size
length (Maybe UProp -> [UProp]
forall a. Maybe a -> [a]
maybeToList (BlockBody -> Maybe UProp
_bUpdProp BlockBody
body_))
        -- A STag is a string, so we need to make sure that all the characters are
        -- accounted for in the size computation. We cannot use equality, since
        -- characters might appear in other parts of the block.
        Size -> (Size -> Size -> Bool) -> Size -> m ()
forall (m :: * -> *) a b.
(MonadTest m, Show a, Show b, HasCallStack) =>
a -> (a -> b -> Bool) -> b -> m ()
diff
          (Size -> (UProp -> Size) -> Maybe UProp -> Size
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Size
0 ([Size] -> Size
forall a. Num a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum ([Size] -> Size) -> (UProp -> [Size]) -> UProp -> Size
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TestName -> Size) -> [TestName] -> [Size]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TestName -> Size
forall a. [a] -> Size
forall (t :: * -> *) a. Foldable t => t a -> Size
length ([TestName] -> [Size]) -> (UProp -> [TestName]) -> UProp -> [Size]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set TestName -> [TestName]
forall a. Set a -> [a]
Set.toList (Set TestName -> [TestName])
-> (UProp -> Set TestName) -> UProp -> [TestName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. UProp -> Set TestName
_upSTags) (BlockBody -> Maybe UProp
_bUpdProp BlockBody
body_))
          Size -> Size -> Bool
forall a. Ord a => a -> a -> Bool
(<=)
          (Map TypeRep Size -> Block -> Size
forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @Char) Block
b)

        -- BlockHeader appears only once
        Map TypeRep Size -> Block -> Size
forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @BlockHeader) Block
b Size -> Size -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== Size
1
        -- BlockBody appears only once
        Map TypeRep Size -> Block -> Size
forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @BlockBody) Block
b Size -> Size -> m ()
forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== Size
1

propBlockAbstractSize :: Property
propBlockAbstractSize :: Property
propBlockAbstractSize =
  TestLimit -> Property -> Property
withTests TestLimit
50 (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$
    HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
      Trace CHAIN
tr <- Gen (Trace CHAIN) -> PropertyT IO (Trace CHAIN)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll (forall s. HasTrace s => BaseEnv s -> Word64 -> Gen (Trace s)
trace @CHAIN () Word64
100)
      let blocks :: [Block]
blocks = TraceOrder -> Trace CHAIN -> [Signal CHAIN]
forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace CHAIN
tr :: [Block]
      (Block -> PropertyT IO ()) -> [Block] -> PropertyT IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Block -> PropertyT IO ()
forall (m :: * -> *). MonadTest m => Block -> m ()
propMultipleOfSizesBlock [Block]
blocks

testAbstractSize :: TestTree
testAbstractSize :: TestTree
testAbstractSize =
  TestName -> [TestTree] -> TestTree
testGroup
    TestName
"Test abstractSize"
    [ TestName -> Assertion -> TestTree
testCase TestName
"AbstractSize - example - BlockHeader" Assertion
exampleTypeRepsBlockHeader
    , TestName -> Assertion -> TestTree
testCase TestName
"AbstractSize - example - BlockBody" Assertion
exampleTypeRepsBlockBody
    , TestName -> Assertion -> TestTree
testCase TestName
"AbstractSize - example - Block" Assertion
exampleTypeRepsBlock
    , TestName -> Property -> TestTree
testProperty TestName
"AbstractSize - Block/Header/Body" Property
propBlockAbstractSize
    ]