{-# 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 = forall a. HasCallStack => a
undefined

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

aHeader :: BlockHeader
aHeader :: BlockHeader
aHeader =
  BlockHeader
    { _bhPrevHash :: Hash
_bhPrevHash = forall a. HasCallStack => a
undefined :: Hash
    , _bhSlot :: Slot
_bhSlot = forall a. HasCallStack => a
undefined :: Slot
    , _bhIssuer :: VKey
_bhIssuer = forall a. HasCallStack => a
undefined :: VKey
    , _bhSig :: Sig Hash
_bhSig = forall a. HasCallStack => a
undefined :: Sig Hash
    , _bhUtxoHash :: Hash
_bhUtxoHash = forall a. HasCallStack => a
undefined :: Hash
    , _bhDlgHash :: Hash
_bhDlgHash = forall a. HasCallStack => a
undefined :: Hash
    , _bhUpdHash :: Hash
_bhUpdHash = 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] forall a. [a]
outs) forall a. [a]
wits

aBody :: BlockBody
aBody :: BlockBody
aBody =
  BlockBody
    { _bDCerts :: [DCert]
_bDCerts = []
    , _bUtxo :: [Tx]
_bUtxo = [Tx
aTxWits, Tx
aTxWits]
    , _bUpdProp :: Maybe UProp
_bUpdProp = 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 =
  forall a. HasTypeReps a => a -> Seq TypeRep
typeReps BlockHeader
aHeader
    forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= forall a. [a] -> Seq a
Seq.fromList
      [ forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: BlockHeader)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Hash)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Hash)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Hash)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Hash)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Slot)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Word64)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: VKey)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Owner)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Natural)
      , forall a. Typeable a => a -> TypeRep
typeOf (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 =
  forall a. HasTypeReps a => a -> Seq TypeRep
typeReps BlockBody
aBody
    forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= forall a. [a] -> Seq a
Seq.fromList
      [ forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: BlockBody)
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: [DCert])
      , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: [Tx])
      ]
      forall a. Seq a -> Seq a -> Seq a
>< forall a. HasTypeReps a => a -> Seq TypeRep
typeReps Tx
aTxWits
      forall a. Seq a -> Seq a -> Seq a
>< forall a. HasTypeReps a => a -> Seq TypeRep
typeReps Tx
aTxWits
      forall a. Seq a -> Seq a -> Seq a
>< forall a. [a] -> Seq a
Seq.fromList
        [ forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Maybe UProp)
        , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: [Vote])
        , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: ProtVer)
        , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Natural)
        , forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Natural)
        , forall a. Typeable a => a -> TypeRep
typeOf (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 =
  forall a. HasTypeReps a => a -> Seq TypeRep
typeReps Block
aBlock
    forall a. (Eq a, Show a, HasCallStack) => a -> a -> Assertion
@?= forall a. Typeable a => a -> TypeRep
typeOf (forall a. HasCallStack => a
undefined :: Block)
      forall a. a -> Seq a -> Seq a
<| forall a. HasTypeReps a => a -> Seq TypeRep
typeReps BlockHeader
aHeader
      forall a. Seq a -> Seq a -> Seq a
>< 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 = forall k a. k -> a -> Map k a
Map.singleton (forall a. Typeable a => a -> TypeRep
typeOf (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
        forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @DCert) Block
b forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall (t :: * -> *) a. Foldable t => t a -> Size
length (BlockBody -> [DCert]
_bDCerts BlockBody
body_)
        forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @Tx) Block
b forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall (t :: * -> *) a. Foldable t => t a -> Size
length (BlockBody -> [Tx]
_bUtxo BlockBody
body_)
        forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @Vote) Block
b forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall (t :: * -> *) a. Foldable t => t a -> Size
length (BlockBody -> [Vote]
_bUpdVotes BlockBody
body_)
        forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @UProp) Block
b forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== forall (t :: * -> *) a. Foldable t => t a -> Size
length (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.
        forall (m :: * -> *) a b.
(MonadTest m, Show a, Show b, HasCallStack) =>
a -> (a -> b -> Bool) -> b -> m ()
diff
          (forall b a. b -> (a -> b) -> Maybe a -> b
maybe Size
0 (forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall (t :: * -> *) a. Foldable t => t a -> Size
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Set a -> [a]
Set.toList forall b c a. (b -> c) -> (a -> b) -> a -> c
. UProp -> Set TestName
_upSTags) (BlockBody -> Maybe UProp
_bUpdProp BlockBody
body_))
          forall a. Ord a => a -> a -> Bool
(<=)
          (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
        forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @BlockHeader) Block
b forall (m :: * -> *) a.
(MonadTest m, Eq a, Show a, HasCallStack) =>
a -> a -> m ()
=== Size
1
        -- BlockBody appears only once
        forall a. HasTypeReps a => Map TypeRep Size -> a -> Size
abstractSize (forall a. Typeable a => Map TypeRep Size
mkCost @BlockBody) Block
b 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 forall a b. (a -> b) -> a -> b
$
    HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
      Trace CHAIN
tr <- 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 = forall s. TraceOrder -> Trace s -> [Signal s]
traceSignals TraceOrder
OldestFirst Trace CHAIN
tr :: [Block]
      forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ 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
    ]