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