module Test.Consensus.Shelley.Coherence (tests) where

import           Cardano.Ledger.Alonzo.Scripts (ExUnits, pointWiseExUnits)
import qualified Data.Measure as Measure
import           Data.Word (Word32)
import           Ouroboros.Consensus.Ledger.SupportsMempool (ByteSize32 (..),
                     IgnoringOverflow (..))
import           Ouroboros.Consensus.Shelley.Ledger.Mempool (AlonzoMeasure (..),
                     ConwayMeasure (..), fromExUnits)
import           Test.Cardano.Ledger.Alonzo.Serialisation.Generators ()
import           Test.Tasty
import           Test.Tasty.QuickCheck

tests :: TestTree
tests :: TestTree
tests = TestName -> [TestTree] -> TestTree
testGroup TestName
"Shelley coherences" [
      TestName
-> (Word32 -> Word32 -> ExUnits -> ExUnits -> Property) -> TestTree
forall a. Testable a => TestName -> a -> TestTree
testProperty TestName
"Measure.<= uses pointWiseExUnits (<=)" Word32 -> Word32 -> ExUnits -> ExUnits -> Property
leqCoherence
    ]

-- | 'Measure.<=' and @'pointWiseExUnits' (<=)@ must agree
leqCoherence :: Word32 -> Word32 -> ExUnits -> ExUnits -> Property
leqCoherence :: Word32 -> Word32 -> ExUnits -> ExUnits -> Property
leqCoherence Word32
w1 Word32
w2 ExUnits
eu1 ExUnits
eu2 =
    Bool
actual Bool -> Bool -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Bool
expected
  where
    -- ConwayMeasure is the fullest TxMeasure and mainnet's
    inj :: ExUnits -> ConwayMeasure
inj ExUnits
eu =
        AlonzoMeasure -> IgnoringOverflow ByteSize32 -> ConwayMeasure
ConwayMeasure
          (IgnoringOverflow ByteSize32 -> ExUnits' Natural -> AlonzoMeasure
AlonzoMeasure
             (ByteSize32 -> IgnoringOverflow ByteSize32
forall a. a -> IgnoringOverflow a
IgnoringOverflow (ByteSize32 -> IgnoringOverflow ByteSize32)
-> ByteSize32 -> IgnoringOverflow ByteSize32
forall a b. (a -> b) -> a -> b
$ Word32 -> ByteSize32
ByteSize32 Word32
w1)
             (ExUnits -> ExUnits' Natural
fromExUnits ExUnits
eu)
          )
          (ByteSize32 -> IgnoringOverflow ByteSize32
forall a. a -> IgnoringOverflow a
IgnoringOverflow (ByteSize32 -> IgnoringOverflow ByteSize32)
-> ByteSize32 -> IgnoringOverflow ByteSize32
forall a b. (a -> b) -> a -> b
$ Word32 -> ByteSize32
ByteSize32 Word32
w2)

    actual :: Bool
actual   = ExUnits -> ConwayMeasure
inj ExUnits
eu1 ConwayMeasure -> ConwayMeasure -> Bool
forall a. Measure a => a -> a -> Bool
Measure.<= ExUnits -> ConwayMeasure
inj ExUnits
eu2
    expected :: Bool
expected = (Natural -> Natural -> Bool) -> ExUnits -> ExUnits -> Bool
pointWiseExUnits Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
(<=) ExUnits
eu1 ExUnits
eu2