From 441b849f2146bd72a4f73bf4b83fc1b9593578b0 Mon Sep 17 00:00:00 2001 From: Michael Peyton Jones Date: Wed, 8 Mar 2023 09:49:28 +0000 Subject: [PATCH] PLT-1611: Fix Interval for discrete intervals (#5190) * PLT-1611: Fix Interval for discrete intervals `Interval` was not in a good place. It violated a bunch of laws. The first thing this PR does is add a bunch more tests: - Generic tests for the typeclasses that `Interval` has instances of. - Some specific tests that test that finite intervals behave the same as sets of consecutive numbers. The latter gives us a "semantic" test that lets us check whether our operations on intervals are doing the right thing with respect to a model - in this case the model is the set of values that fall into the inteval. Then we need to actually fix `Interval`. The most straightforward solution I could see is just to restrict most of its operations to intervals on enumerable types. That lets us turn non-inclusive bounds into inclusive bounds, which simplifies things a lot. Without that information, we can't easily even tell if e.g. an interval is empty or not. Arguably we should just have never had non-inclusive bounds in the first place and it's unnecessary generality. However, I think changing that now would be more disruptive than it is worth. Fixes #5185 * Review comments * Add tests for closed boolean intervals --- ...63021_michael.peyton-jones_fix_interval.md | 3 + plutus-ledger-api/plutus-ledger-api.cabal | 8 +- .../src/PlutusLedgerApi/V1/Interval.hs | 189 +++++++++++++----- plutus-ledger-api/test/Spec/Interval.hs | 161 +++++++++++++-- plutus-tx/plutus-tx.cabal | 10 +- plutus-tx/src/PlutusTx/Enum.hs | 10 +- plutus-tx/testlib/Hedgehog/Laws/Common.hs | 75 +++++++ plutus-tx/testlib/Hedgehog/Laws/Eq.hs | 15 ++ plutus-tx/testlib/Hedgehog/Laws/Lattice.hs | 58 ++++++ plutus-tx/testlib/Hedgehog/Laws/Ord.hs | 23 +++ 10 files changed, 477 insertions(+), 75 deletions(-) create mode 100644 plutus-ledger-api/changelog.d/20230302_163021_michael.peyton-jones_fix_interval.md create mode 100644 plutus-tx/testlib/Hedgehog/Laws/Common.hs create mode 100644 plutus-tx/testlib/Hedgehog/Laws/Eq.hs create mode 100644 plutus-tx/testlib/Hedgehog/Laws/Lattice.hs create mode 100644 plutus-tx/testlib/Hedgehog/Laws/Ord.hs diff --git a/plutus-ledger-api/changelog.d/20230302_163021_michael.peyton-jones_fix_interval.md b/plutus-ledger-api/changelog.d/20230302_163021_michael.peyton-jones_fix_interval.md new file mode 100644 index 00000000000..30d2d3d3d4f --- /dev/null +++ b/plutus-ledger-api/changelog.d/20230302_163021_michael.peyton-jones_fix_interval.md @@ -0,0 +1,3 @@ +### Fixed + +- Fixed numerous bugs in the behaviour of `Interval`s with open endpoints. diff --git a/plutus-ledger-api/plutus-ledger-api.cabal b/plutus-ledger-api/plutus-ledger-api.cabal index 8664f777d17..da3d1076e09 100644 --- a/plutus-ledger-api/plutus-ledger-api.cabal +++ b/plutus-ledger-api/plutus-ledger-api.cabal @@ -138,7 +138,7 @@ test-suite plutus-ledger-api-test build-depends: , barbies - , base >=4.9 && <5 + , base >=4.9 && <5 , bytestring , containers , extra @@ -146,9 +146,9 @@ test-suite plutus-ledger-api-test , lens , mtl , nothunks - , plutus-core ^>=1.2 - , plutus-ledger-api ^>=1.2 - , plutus-ledger-api-testlib ^>=1.2 + , plutus-core ^>=1.2 + , plutus-ledger-api:{plutus-ledger-api, plutus-ledger-api-testlib} ^>=1.2 + , plutus-tx:plutus-tx-testlib ^>=1.2 , tasty , tasty-hedgehog , tasty-hunit diff --git a/plutus-ledger-api/src/PlutusLedgerApi/V1/Interval.hs b/plutus-ledger-api/src/PlutusLedgerApi/V1/Interval.hs index dc36c7fd3d5..5a46ba6a029 100644 --- a/plutus-ledger-api/src/PlutusLedgerApi/V1/Interval.hs +++ b/plutus-ledger-api/src/PlutusLedgerApi/V1/Interval.hs @@ -41,9 +41,12 @@ import Prelude qualified as Haskell import Prettyprinter (Pretty (pretty), comma, (<+>)) import PlutusTx qualified +import PlutusTx.Eq as PlutusTx import PlutusTx.Lift (makeLift) +import PlutusTx.Ord as PlutusTx import PlutusTx.Prelude +-- See Note [Enumerable Intervals] {- | An interval of @a@s. The interval may be either closed or open at either end, meaning @@ -51,11 +54,16 @@ that the endpoints may or may not be included in the interval. The interval can also be unbounded on either side. -The 'Haskell.Eq'uality of two intervals is specified as the canonical, structural equality and not -the equality of the elements of their two underlying sets; the same holds for 'Haskell.Ord'. +The 'Eq' instance gives equality of the intervals, not structural equality. +There is no 'Ord' instance, but 'contains' gives a partial order. + +Note that some of the functions on `Interval` rely on `Enum` in order to +handle non-inclusive endpoints. For this reason, it may not be safe to +use `Interval`s with non-inclusive endpoints on types whose `Enum` +instances have partial methods. -} data Interval a = Interval { ivFrom :: LowerBound a, ivTo :: UpperBound a } - deriving stock (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic) + deriving stock (Haskell.Show, Generic) deriving anyclass (NFData) instance Functor Interval where @@ -66,7 +74,7 @@ instance Pretty a => Pretty (Interval a) where -- | A set extended with a positive and negative infinity. data Extended a = NegInf | Finite a | PosInf - deriving stock (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic) + deriving stock (Haskell.Show, Generic) deriving anyclass (NFData) instance Functor Extended where @@ -79,14 +87,30 @@ instance Pretty a => Pretty (Extended a) where pretty PosInf = pretty "+∞" pretty (Finite a) = pretty a +-- See Note [Enumerable Intervals] -- | Whether a bound is inclusive or not. type Closure = Bool -- | The upper bound of an interval. data UpperBound a = UpperBound (Extended a) Closure - deriving stock (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic) + deriving stock (Haskell.Show, Generic) deriving anyclass (NFData) +-- | For an enumerable type, turn an upper bound into a single inclusive +-- bounding value. +-- +-- Since the type is enumerable, non-inclusive bounds are equivalent +-- to inclusive bounds on the predecessor. +-- +-- See Note [Enumerable Intervals] +inclusiveUpperBound :: Enum a => UpperBound a -> Extended a +-- already inclusive +inclusiveUpperBound (UpperBound v True) = v +-- take pred +inclusiveUpperBound (UpperBound (Finite x) False) = Finite $ pred x +-- an infinity: inclusive/non-inclusive makes no difference +inclusiveUpperBound (UpperBound v False) = v + instance Functor UpperBound where fmap f (UpperBound e c) = UpperBound (f <$> e) c @@ -98,9 +122,24 @@ instance Pretty a => Pretty (UpperBound a) where -- | The lower bound of an interval. data LowerBound a = LowerBound (Extended a) Closure - deriving stock (Haskell.Eq, Haskell.Ord, Haskell.Show, Generic) + deriving stock (Haskell.Show, Generic) deriving anyclass (NFData) +-- | For an enumerable type, turn an lower bound into a single inclusive +-- bounding value. +-- +-- Since the type is enumerable, non-inclusive bounds are equivalent +-- to inclusive bounds on the successor. +-- +-- See Note [Enumerable Intervals] +inclusiveLowerBound :: Enum a => LowerBound a -> Extended a +-- already inclusive +inclusiveLowerBound (LowerBound v True) = v +-- take succ +inclusiveLowerBound (LowerBound (Finite x) False) = Finite $ succ x +-- an infinity: inclusive/non-inclusive makes no difference +inclusiveLowerBound (LowerBound v False) = v + instance Functor LowerBound where fmap f (LowerBound e c) = LowerBound (f <$> e) c @@ -127,6 +166,9 @@ instance Eq a => Eq (Extended a) where Finite l == Finite r = l == r _ == _ = False +instance Eq a => Haskell.Eq (Extended a) where + (==) = (PlutusTx.==) + instance Ord a => Ord (Extended a) where {-# INLINABLE compare #-} NegInf `compare` NegInf = EQ @@ -137,31 +179,40 @@ instance Ord a => Ord (Extended a) where PosInf `compare` _ = GT Finite l `compare` Finite r = l `compare` r -instance Eq a => Eq (UpperBound a) where +instance Ord a => Haskell.Ord (Extended a) where + compare = PlutusTx.compare + +-- See Note [Enumerable Intervals] +instance (Enum a, Eq a) => Eq (UpperBound a) where {-# INLINABLE (==) #-} - UpperBound v1 in1 == UpperBound v2 in2 = v1 == v2 && in1 == in2 + b1 == b2 = inclusiveUpperBound b1 == inclusiveUpperBound b2 -instance Ord a => Ord (UpperBound a) where +instance (Enum a, Eq a) => Haskell.Eq (UpperBound a) where + (==) = (PlutusTx.==) + +-- See Note [Enumerable Intervals] +instance (Enum a, Ord a) => Ord (UpperBound a) where {-# INLINABLE compare #-} - UpperBound v1 in1 `compare` UpperBound v2 in2 = case v1 `compare` v2 of - LT -> LT - GT -> GT - -- A closed upper bound is bigger than an open upper bound. This corresponds - -- to the normal order on Bool. - EQ -> in1 `compare` in2 - -instance Eq a => Eq (LowerBound a) where + b1 `compare` b2 = inclusiveUpperBound b1 `compare` inclusiveUpperBound b2 + +instance (Enum a, Ord a) => Haskell.Ord (UpperBound a) where + compare = PlutusTx.compare + +-- See Note [Enumerable Intervals] +instance (Enum a, Eq a) => Eq (LowerBound a) where {-# INLINABLE (==) #-} - LowerBound v1 in1 == LowerBound v2 in2 = v1 == v2 && in1 == in2 + b1 == b2 = inclusiveLowerBound b1 == inclusiveLowerBound b2 -instance Ord a => Ord (LowerBound a) where +instance (Enum a, Eq a) => Haskell.Eq (LowerBound a) where + (==) = (PlutusTx.==) + +-- See Note [Enumerable Intervals] +instance (Enum a, Ord a) => Ord (LowerBound a) where {-# INLINABLE compare #-} - LowerBound v1 in1 `compare` LowerBound v2 in2 = case v1 `compare` v2 of - LT -> LT - GT -> GT - -- An open lower bound is bigger than a closed lower bound. This corresponds - -- to the *reverse* of the normal order on Bool. - EQ -> in2 `compare` in1 + b1 `compare` b2 = inclusiveLowerBound b1 `compare` inclusiveLowerBound b2 + +instance (Enum a, Ord a) => Haskell.Ord (LowerBound a) where + compare = PlutusTx.compare {-# INLINABLE strictUpperBound #-} {- | Construct a strict upper bound from a value. @@ -195,25 +246,38 @@ The resulting bound includes all values that are equal or smaller than the input upperBound :: a -> UpperBound a upperBound a = UpperBound (Finite a) True -instance Ord a => JoinSemiLattice (Interval a) where +-- See Note [Enumerable Intervals] +instance (Enum a, Ord a) => JoinSemiLattice (Interval a) where {-# INLINABLE (\/) #-} (\/) = hull -instance Ord a => BoundedJoinSemiLattice (Interval a) where +-- See Note [Enumerable Intervals] +instance (Enum a, Ord a) => BoundedJoinSemiLattice (Interval a) where {-# INLINABLE bottom #-} bottom = never -instance Ord a => MeetSemiLattice (Interval a) where +-- See Note [Enumerable Intervals] +instance (Enum a, Ord a) => MeetSemiLattice (Interval a) where {-# INLINABLE (/\) #-} (/\) = intersection -instance Ord a => BoundedMeetSemiLattice (Interval a) where +-- See Note [Enumerable Intervals] +instance (Enum a, Ord a) => BoundedMeetSemiLattice (Interval a) where {-# INLINABLE top #-} top = always -instance Eq a => Eq (Interval a) where +-- See Note [Enumerable Intervals] +instance (Enum a, Ord a) => Eq (Interval a) where {-# INLINABLE (==) #-} - l == r = ivFrom l == ivFrom r && ivTo l == ivTo r + -- Degenerate case: both the intervals are empty. + -- There can be many empty intervals, so we check for this case + -- explicitly + iv1 == iv2 | isEmpty iv1 && isEmpty iv2 = True + (Interval lb1 ub1) == (Interval lb2 ub2) = lb1 == lb2 && ub1 == ub2 + +instance (Enum a, Ord a) => Haskell.Eq (Interval a) where + {-# INLINABLE (==) #-} + (==) = (PlutusTx.==) {-# INLINABLE interval #-} -- | @interval a b@ includes all values that are greater than or equal to @a@ @@ -255,7 +319,7 @@ never = Interval (LowerBound PosInf True) (UpperBound NegInf True) {-# INLINABLE member #-} -- | Check whether a value is in an interval. -member :: Ord a => a -> Interval a -> Bool +member :: (Enum a, Ord a) => a -> Interval a -> Bool member a i = i `contains` singleton a {-# INLINABLE overlaps #-} @@ -267,12 +331,12 @@ overlaps l r = not $ isEmpty (l `intersection` r) {-# INLINABLE intersection #-} -- | 'intersection a b' is the largest interval that is contained in 'a' and in -- 'b', if it exists. -intersection :: Ord a => Interval a -> Interval a -> Interval a +intersection :: (Enum a, Ord a) => Interval a -> Interval a -> Interval a intersection (Interval l1 h1) (Interval l2 h2) = Interval (max l1 l2) (min h1 h2) {-# INLINABLE hull #-} -- | 'hull a b' is the smallest interval containing 'a' and 'b'. -hull :: Ord a => Interval a -> Interval a -> Interval a +hull :: (Enum a, Ord a) => Interval a -> Interval a -> Interval a hull (Interval l1 h1) (Interval l2 h2) = Interval (min l1 l2) (max h1 h2) {-# INLINABLE contains #-} @@ -280,33 +344,56 @@ hull (Interval l1 h1) (Interval l2 h2) = Interval (min l1 l2) (max h1 h2) @a@. That is, @a `contains` b@ if for every entry @s@, if @member s b@ then @member s a@. -} -contains :: Ord a => Interval a -> Interval a -> Bool +contains :: (Enum a, Ord a) => Interval a -> Interval a -> Bool +-- Everything contains the empty interval +contains _ i2 | isEmpty i2 = True +-- Nothing is contained in the empty interval (except the empty interval, +-- which is already handled) +contains i1 _ | isEmpty i1 = False +-- Otherwise we check the endpoints. This doesn't work for empty intervals, +-- hence the cases above. contains (Interval l1 h1) (Interval l2 h2) = l1 <= l2 && h2 <= h1 {-# INLINABLE isEmpty #-} -{- | Check if an 'Interval' is empty. - -There can be many empty intervals, given a set of values. -Two 'Interval's being empty does not imply that they are `Haskell.Eq`ual to each other. --} +{- | Check if an 'Interval' is empty. -} isEmpty :: (Enum a, Ord a) => Interval a -> Bool -isEmpty (Interval (LowerBound v1 in1) (UpperBound v2 in2)) = case v1 `compare` v2 of - LT -> if openInterval then checkEnds v1 v2 else False +isEmpty (Interval lb ub) = case inclusiveLowerBound lb `compare` inclusiveUpperBound ub of + -- We have at least two possible values, the lower bound and the upper bound + LT -> False + -- We have one possible value, the lower bound/upper bound + EQ -> False + -- We have no possible values GT -> True - EQ -> not (in1 && in2) - where - openInterval = in1 == False && in2 == False - -- | We check two finite ends to figure out if there are elements between them. - -- If there are no elements then the interval is empty (#3467). - checkEnds (Finite v1') (Finite v2') = succ v1' == v2' - checkEnds _ _ = False {-# INLINABLE before #-} -- | Check if a value is earlier than the beginning of an 'Interval'. -before :: Ord a => a -> Interval a -> Bool +before :: (Enum a, Ord a) => a -> Interval a -> Bool before h (Interval f _) = lowerBound h < f {-# INLINABLE after #-} -- | Check if a value is later than the end of an 'Interval'. -after :: Ord a => a -> Interval a -> Bool +after :: (Enum a , Ord a) => a -> Interval a -> Bool after h (Interval _ t) = upperBound h > t + +{- Note [Enumerable Intervals] +The 'Interval' type is set up to handle open intervals, where we have non-inclusive +bounds. These are only meaningful for orders where there do not exist (computable) +joins and meets over all elements greater or less than an element. + +If those do exist, we can eliminate non-inclusive bounds in favour of inclusive bounds. +For example, in the integers, (x, y) is equivalent to [x+1, y-1], because +x+1 = sup { z | z > x} and y-1 = inf { z | z < y }. + +Checking equality, containment etc. of intervals with non-inclusive bounds is +tricky. For example, to know if (x, y) is empty, we need to know if there is a +value between x and y. We don't have a typeclass for that! + +In practice, most of the intervals we care about are enumerable (have 'Enum' +instances). We assume that `pred` and `succ` calculate the infima/suprema described +above, and so we can turn non-inclusive bounds into inclusive bounds, which +makes things much easier. The downside is that some of the `Enum` instances have +partial implementations, which means that, e.g. `isEmpty (False, True]` will +throw. + +The upshot of this is that many functions in this module require 'Enum'. +-} diff --git a/plutus-ledger-api/test/Spec/Interval.hs b/plutus-ledger-api/test/Spec/Interval.hs index 45e724ea43e..601e07a2465 100644 --- a/plutus-ledger-api/test/Spec/Interval.hs +++ b/plutus-ledger-api/test/Spec/Interval.hs @@ -6,15 +6,55 @@ module Spec.Interval where import Data.List (sort) +import Data.Maybe (fromJust) +import Data.Set qualified as Set import Hedgehog (Property, forAll, property) import Hedgehog qualified import Hedgehog.Gen qualified as Gen +import Hedgehog.Laws.Eq +import Hedgehog.Laws.Lattice +import Hedgehog.Laws.Ord import Hedgehog.Range qualified as Range import PlutusLedgerApi.V1.Interval qualified as Interval +import PlutusPrelude (reoption) import Test.Tasty (TestTree, testGroup) -import Test.Tasty.Hedgehog (testPropertyNamed) +import Test.Tasty.Hedgehog (testProperty) import Test.Tasty.HUnit (assertBool, testCase) +-- TODO: maybe bias towards generating non-empty intervals? + +genExtended :: Bool -> Hedgehog.Gen a -> Hedgehog.Gen (Interval.Extended a) +genExtended finite g = + if finite + then Interval.Finite <$> g + else Gen.choice [ Interval.Finite <$> g, pure Interval.NegInf, pure Interval.PosInf ] + +genLowerBound :: Bool -> Bool -> Hedgehog.Gen a -> Hedgehog.Gen (Interval.LowerBound a) +genLowerBound finite closedOnly g = do + bound <- genExtended finite g + closure <- if closedOnly then pure True else Gen.bool + pure $ Interval.LowerBound bound closure + +genUpperBound :: Bool -> Bool -> Hedgehog.Gen a -> Hedgehog.Gen (Interval.UpperBound a) +genUpperBound finite closedOnly g = do + bound <- genExtended finite g + closure <- if closedOnly then pure True else Gen.bool + pure $ Interval.UpperBound bound closure + +genInterval :: Bool -> Bool -> Hedgehog.Gen a -> Hedgehog.Gen (Interval.Interval a) +genInterval finite closedOnly g = Interval.Interval <$> genLowerBound finite closedOnly g <*> genUpperBound finite closedOnly g + +genFiniteIntegerInterval :: Hedgehog.Gen (Interval.Interval Integer) +genFiniteIntegerInterval = genInterval True False (Gen.integral (toInteger <$> Range.linear @Int 0 100)) + +genIntegerInterval :: Hedgehog.Gen (Interval.Interval Integer) +genIntegerInterval = genInterval False False (Gen.integral (toInteger <$> Range.linear @Int 0 100)) + +genBooleanInterval :: Hedgehog.Gen (Interval.Interval Bool) +genBooleanInterval = genInterval False True Gen.bool + +-- Unit tests + alwaysIsNotEmpty :: TestTree alwaysIsNotEmpty = testCase "always is not empty" $ @@ -37,6 +77,8 @@ openOverlaps = b = Interval.Interval (Interval.strictLowerBound 4) (Interval.strictUpperBound 6) :: Interval.Interval Integer in assertBool "overlaps" (not $ Interval.overlaps a b) +-- Property tests + intvlIsEmpty :: Property intvlIsEmpty = property $ do (i1, i2) <- forAll $ (,) <$> Gen.integral (toInteger <$> Range.linearBounded @Int) <*> Gen.integral (toInteger <$> Range.linearBounded @Int) @@ -62,17 +104,6 @@ intvlIntersection = property $ do Hedgehog.assert $ intersec == inner Hedgehog.assert $ intersec2 == common -intvlIntersectionWithAlwaysNever :: Property -intvlIntersectionWithAlwaysNever = property $ do - (i1, i2) <- forAll $ (,) <$> Gen.integral (toInteger <$> Range.linearBounded @Int) <*> Gen.integral (toInteger <$> Range.linearBounded @Int) - let (from, to) = (min i1 i2, max i1 i2) - i = Interval.interval from to - e = Interval.interval to from - - Hedgehog.assert $ Interval.never == i `Interval.intersection` Interval.never - Hedgehog.assert $ i == i `Interval.intersection` Interval.always - Hedgehog.assert $ e == e `Interval.intersection` i - intvlOverlaps :: Property intvlOverlaps = property $ do (i1, i2) <- forAll $ (,) <$> Gen.integral (toInteger <$> Range.linearBounded @Int) <*> Gen.integral (toInteger <$> Range.linearBounded @Int) @@ -83,16 +114,112 @@ intvlOverlaps = property $ do Hedgehog.assert $ Interval.always `Interval.overlaps` i Hedgehog.assert $ not $ Interval.never `Interval.overlaps` i +{- Set model tests + +We can give a semantic model for a finite (inded small), discrete interval in terms of the set of +values that are in the interval. We can easily perform many operations at the semantic level, including +equality, intersection, etc. This allows us to check that our implementation of intervals is +implementing the semantically correct behaviour. +-} + +lowerBoundToValue :: Enum a => Interval.LowerBound a -> Maybe a +lowerBoundToValue (Interval.LowerBound (Interval.Finite b) inclusive) = Just $ if inclusive then b else succ b +lowerBoundToValue _ = Nothing + +upperBoundToValue :: Enum a => Interval.UpperBound a -> Maybe a +upperBoundToValue (Interval.UpperBound (Interval.Finite b) inclusive) = Just $ if inclusive then b else pred b +upperBoundToValue _ = Nothing + +intervalToSet :: (Ord a, Enum a) => Interval.Interval a -> Maybe (Set.Set a) +intervalToSet (Interval.Interval lb ub) = Set.fromList <$> (enumFromTo <$> lowerBoundToValue lb <*> upperBoundToValue ub) + +setToInterval :: Set.Set a -> Interval.Interval a +setToInterval st | Set.null st = Interval.Interval (Interval.LowerBound Interval.PosInf True) (Interval.UpperBound Interval.NegInf True) +setToInterval st = Interval.Interval (Interval.LowerBound (Interval.Finite (Set.findMin st)) True) (Interval.UpperBound (Interval.Finite (Set.findMax st)) True) + +prop_intervalSetTripping :: Property +prop_intervalSetTripping = property $ do + ivl <- forAll genFiniteIntegerInterval + Hedgehog.tripping ivl (fromJust . intervalToSet) (Just . setToInterval) + +prop_intervalSetEquals :: Property +prop_intervalSetEquals = property $ do + ivl1 <- forAll genFiniteIntegerInterval + ivl2 <- forAll genFiniteIntegerInterval + s1 <- reoption $ intervalToSet ivl1 + s2 <- reoption $ intervalToSet ivl2 + Hedgehog.annotateShow s1 + Hedgehog.annotateShow s2 + let + c1 = ivl1 == ivl2 + c2 = s2 == s1 + Hedgehog.cover 10 "True" $ c1 + Hedgehog.cover 10 "False" $ not c1 + c1 Hedgehog.=== c2 + +prop_intervalSetContains :: Property +prop_intervalSetContains = property $ do + ivl1 <- forAll genFiniteIntegerInterval + ivl2 <- forAll genFiniteIntegerInterval + s1 <- reoption $ intervalToSet ivl1 + s2 <- reoption $ intervalToSet ivl2 + Hedgehog.annotateShow s1 + Hedgehog.annotateShow s2 + let + c1 = ivl1 `Interval.contains` ivl2 + c2 = s2 `Set.isSubsetOf` s1 + Hedgehog.cover 30 "True" $ c1 + Hedgehog.cover 30 "False" $ not c1 + c1 Hedgehog.=== c2 + +prop_intervalSetIntersection :: Property +prop_intervalSetIntersection = property $ do + ivl1 <- forAll genFiniteIntegerInterval + ivl2 <- forAll genFiniteIntegerInterval + let iv3 = ivl1 `Interval.intersection` ivl2 + s0 <- reoption $ intervalToSet iv3 + + s1 <- reoption $ intervalToSet ivl1 + s2 <- reoption $ intervalToSet ivl2 + let s3 = s1 `Set.intersection` s2 + + -- Just need some coverage of the interesting case + Hedgehog.cover 5 "Non-trivial" $ not $ Set.null s3 + + Hedgehog.annotateShow s0 + Hedgehog.annotateShow s1 + Hedgehog.annotateShow s2 + Hedgehog.annotateShow s3 + + s0 Hedgehog.=== s3 + tests :: TestTree tests = testGroup - "plutus-ledger-api-interval" + "Interval" [ neverIsEmpty , alwaysIsNotEmpty , openIsEmpty , openOverlaps - , testPropertyNamed "interval intersection" "intvIntersection" intvlIntersection - , testPropertyNamed "interval intersection with always/never" "intvlIntersectionWithAlwaysNever" intvlIntersectionWithAlwaysNever - , testPropertyNamed "interval isEmpty" "intvlIsEmpty" intvlIsEmpty - , testPropertyNamed "interval overlaps" "intvlOverlaps" intvlOverlaps + , testGroup "laws for integer intervals" + [ eqLaws genIntegerInterval + , partialOrderLaws genIntegerInterval Interval.contains + , boundedLatticeLaws genIntegerInterval + ] + , testGroup "laws for boolean intervals" + [ eqLaws genBooleanInterval + , partialOrderLaws genBooleanInterval Interval.contains + , boundedLatticeLaws genBooleanInterval + ] + , testGroup "properties" + [ testProperty "intersection" intvlIntersection + , testProperty "isEmpty" intvlIsEmpty + , testProperty "overlaps" intvlOverlaps + ] + , testGroup "set model" + [ testProperty "tripping" prop_intervalSetTripping + , testProperty "equals" prop_intervalSetEquals + , testProperty "contains" prop_intervalSetContains + , testProperty "intersection" prop_intervalSetIntersection + ] ] diff --git a/plutus-tx/plutus-tx.cabal b/plutus-tx/plutus-tx.cabal index 74a25d8b34e..73bf9085488 100644 --- a/plutus-tx/plutus-tx.cabal +++ b/plutus-tx/plutus-tx.cabal @@ -119,11 +119,18 @@ library plutus-tx-testlib import: lang visibility: public hs-source-dirs: testlib - exposed-modules: PlutusTx.Test + exposed-modules: + Hedgehog.Laws.Common + Hedgehog.Laws.Eq + Hedgehog.Laws.Lattice + Hedgehog.Laws.Ord + PlutusTx.Test + build-depends: , base >=4.9 && <5 , filepath , flat <0.5 + , hedgehog , lens , mtl , plutus-core:{plutus-core, plutus-core-testlib, plutus-ir} ^>=1.2 @@ -131,6 +138,7 @@ library plutus-tx-testlib , prettyprinter , tagged , tasty + , tasty-hedgehog , text test-suite plutus-tx-test diff --git a/plutus-tx/src/PlutusTx/Enum.hs b/plutus-tx/src/PlutusTx/Enum.hs index 0d17e1dbd45..4da575559f2 100644 --- a/plutus-tx/src/PlutusTx/Enum.hs +++ b/plutus-tx/src/PlutusTx/Enum.hs @@ -12,9 +12,15 @@ import PlutusTx.Trace -- | Class 'Enum' defines operations on sequentially ordered types. class Enum a where - -- | the successor of a value. For numeric types, 'succ' adds 1. + -- | The successor of a value. For numeric types, 'succ' adds 1. + -- + -- For types that implement 'Ord', @succ x@ should be the least element + -- that is greater than @x@, and 'error' if there is none. succ :: a -> a - -- | the predecessor of a value. For numeric types, 'pred' subtracts 1. + -- | The predecessor of a value. For numeric types, 'pred' subtracts 1. + -- + -- For types that implement 'Ord', @pred x@ should be the greatest element + -- that is less than @x@, and 'error' if there is none. pred :: a -> a -- | Convert from an 'Integer'. toEnum :: Integer -> a diff --git a/plutus-tx/testlib/Hedgehog/Laws/Common.hs b/plutus-tx/testlib/Hedgehog/Laws/Common.hs new file mode 100644 index 00000000000..a195c060b6d --- /dev/null +++ b/plutus-tx/testlib/Hedgehog/Laws/Common.hs @@ -0,0 +1,75 @@ +{-# LANGUAGE OverloadedStrings #-} +module Hedgehog.Laws.Common where + +import Hedgehog (Property, cover, forAll, property) +import Hedgehog qualified +import Prelude + +implies :: Bool -> Bool -> Bool +implies x y = not x || y + +prop_idempotent :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> a) -> Property +prop_idempotent g op = property $ do + x <- forAll g + x `op` x Hedgehog.=== x + +prop_commutative :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> a) -> Property +prop_commutative g op = property $ do + x <- forAll g + y <- forAll g + cover 10 "different" $ x /= y + cover 5 "same" $ x == y + x `op` y Hedgehog.=== y `op` x + +prop_associative :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> a) -> Property +prop_associative g op = property $ do + x <- forAll g + y <- forAll g + z <- forAll g + cover 10 "different" $ x /= y && y /= z + cover 5 "same" $ x == y || y == z || z == x + (x `op` y) `op` z Hedgehog.=== x `op` (y `op` z) + +prop_unit :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> a) -> a -> Property +prop_unit g op unit = property $ do + x <- forAll g + cover 10 "different" $ x /= unit + x `op` unit Hedgehog.=== x + +prop_reflexive :: (Show a) => Hedgehog.Gen a -> (a -> a -> Bool) -> Property +prop_reflexive g op = property $ do + x <- forAll g + x `op` x Hedgehog.=== True + +prop_symmetric :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> Bool) -> Property +prop_symmetric g op = property $ do + x <- forAll g + y <- forAll g + cover 10 "different" $ x /= y + cover 5 "same" $ x == y + x `op` y Hedgehog.=== y `op` x + +prop_transitive :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> Bool) -> Property +prop_transitive g op = property $ do + x <- forAll g + y <- forAll g + z <- forAll g + cover 10 "different" $ x /= y && y /= z + cover 5 "same" $ x == y || y == z || z == x + Hedgehog.assert $ (x `op` y && y `op` z) `implies` (x `op` z) + +prop_antisymmetric :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> Bool) -> Property +prop_antisymmetric g op = property $ do + x <- forAll g + y <- forAll g + cover 10 "different" $ x /= y + cover 5 "same" $ x == y + Hedgehog.assert $ (x `op` y && y `op` x) `implies` (x == y) + +prop_total :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> Bool) -> Property +prop_total g op = property $ do + x <- forAll g + y <- forAll g + cover 10 "different" $ x /= y + cover 5 "same" $ x == y + Hedgehog.assert $ x `op` y || y `op` x diff --git a/plutus-tx/testlib/Hedgehog/Laws/Eq.hs b/plutus-tx/testlib/Hedgehog/Laws/Eq.hs new file mode 100644 index 00000000000..585ef525522 --- /dev/null +++ b/plutus-tx/testlib/Hedgehog/Laws/Eq.hs @@ -0,0 +1,15 @@ +{-# LANGUAGE OverloadedStrings #-} +module Hedgehog.Laws.Eq where + +import Hedgehog qualified +import Hedgehog.Laws.Common +import Prelude +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +eqLaws :: (Show a, Eq a) => Hedgehog.Gen a -> TestTree +eqLaws g = testGroup "equivalence relation laws" + [ testProperty "reflexive" (prop_reflexive g (==)) + , testProperty "symmetric" (prop_symmetric g (==)) + , testProperty "transitive" (prop_transitive g (==)) + ] diff --git a/plutus-tx/testlib/Hedgehog/Laws/Lattice.hs b/plutus-tx/testlib/Hedgehog/Laws/Lattice.hs new file mode 100644 index 00000000000..37b263140e3 --- /dev/null +++ b/plutus-tx/testlib/Hedgehog/Laws/Lattice.hs @@ -0,0 +1,58 @@ +{-# LANGUAGE OverloadedStrings #-} +module Hedgehog.Laws.Lattice where + +import Hedgehog (Property, cover, forAll, property) +import Hedgehog qualified +import Hedgehog.Laws.Common +import PlutusTx.Lattice +import Prelude +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +joinLatticeLaws :: (Show a, Eq a, JoinSemiLattice a) => Hedgehog.Gen a -> TestTree +joinLatticeLaws g = testGroup "join semilattice laws" + [ testProperty "idempotent" (prop_idempotent g (\/)) + , testProperty "commutative" (prop_commutative g (\/)) + , testProperty "associative" (prop_associative g (\/)) + ] + +boundedJoinLatticeLaws :: (Show a, Eq a, BoundedJoinSemiLattice a) => Hedgehog.Gen a -> TestTree +boundedJoinLatticeLaws g = testGroup "bounded join semilattice laws" + [ joinLatticeLaws g + , testProperty "unit" (prop_unit g (\/) bottom) + ] + +meetLatticeLaws :: (Show a, Eq a, MeetSemiLattice a) => Hedgehog.Gen a -> TestTree +meetLatticeLaws g = testGroup "meet semilattice laws" + [ testProperty "idempotent" (prop_idempotent g (/\)) + , testProperty "commutative" (prop_commutative g (/\)) + , testProperty "associative" (prop_associative g (/\)) + ] + +boundedMeetLatticeLaws :: (Show a, Eq a, BoundedMeetSemiLattice a) => Hedgehog.Gen a -> TestTree +boundedMeetLatticeLaws g = testGroup "bounded meet semilattice laws" + [ meetLatticeLaws g + , testProperty "unit" (prop_unit g (/\) top) + ] + +prop_latticeAbsorb :: (Show a, Eq a, Lattice a) => Hedgehog.Gen a -> Property +prop_latticeAbsorb g = property $ do + x <- forAll g + y <- forAll g + cover 10 "different" $ x /= y + x \/ (x /\ y) Hedgehog.=== x + x /\ (x \/ y) Hedgehog.=== x + +latticeLaws :: (Show a, Eq a, Lattice a) => Hedgehog.Gen a -> TestTree +latticeLaws g = testGroup "lattice laws" + [ joinLatticeLaws g + , meetLatticeLaws g + , testProperty "absorption" (prop_latticeAbsorb g) + ] + +boundedLatticeLaws :: (Show a, Eq a, BoundedLattice a) => Hedgehog.Gen a -> TestTree +boundedLatticeLaws g = testGroup "bounded lattice laws" + [ boundedJoinLatticeLaws g + , boundedMeetLatticeLaws g + , testProperty "absorption" (prop_latticeAbsorb g) + ] diff --git a/plutus-tx/testlib/Hedgehog/Laws/Ord.hs b/plutus-tx/testlib/Hedgehog/Laws/Ord.hs new file mode 100644 index 00000000000..543fd22e284 --- /dev/null +++ b/plutus-tx/testlib/Hedgehog/Laws/Ord.hs @@ -0,0 +1,23 @@ +{-# LANGUAGE OverloadedStrings #-} +module Hedgehog.Laws.Ord where + +import Hedgehog qualified +import Hedgehog.Laws.Common +import Prelude +import Test.Tasty (TestTree, testGroup) +import Test.Tasty.Hedgehog (testProperty) + +-- There is no typeclass for this, sadly +partialOrderLaws :: (Show a, Eq a) => Hedgehog.Gen a -> (a -> a -> Bool) -> TestTree +partialOrderLaws g op = testGroup "partial ordering laws" + [ testProperty "reflexive" (prop_reflexive g op) + , testProperty "transitive" (prop_transitive g op) + , testProperty "antisymmetric" (prop_antisymmetric g op) + ] + +ordLaws :: (Show a, Ord a) => Hedgehog.Gen a -> TestTree +ordLaws g = testGroup "total ordering laws" + [ partialOrderLaws g (<=) + , testProperty "total" (prop_total g (<=)) + ] +