PlutusLedgerApi.V1.Interval.contains is wrong for discrete intervals

[carlhammann]

Summary

Hello!

The problem

I expect contains to check the relation $\supseteq$ on intervals. For discrete intervals, this expectation is violated when comparing (some) open and closed intervals.

For instance, for intervals of integers, $[0,2]=\{0,1,2\}=[0,3)$, and in particular $[0,2]\supseteq[0,3)$, but

Interval (LowerBound (Finite 0) True) (UpperBound (Finite 2) True) 
  `contains` Interval (LowerBound (Finite 0) True) (UpperBound (Finite 3) False)

evaluates to False.

This has confusing consequences when applied to, say, the txInfoValidRange, which is a (discrete) Interval of milliseconds. Here is an example of a validator that checks that a transaction happens before a given deadline. It does so in the obvious way, and is subtly wrong in doing so, due to the behaviour of contains.

The cause

Following the implementation, and in particular the Ord instance of UpperBound, we see that for all integers a and b

Interval (LowerBound a True) (UpperBound (b-1) True) 
   `Interval.contains` Interval (LowerBound a True) (UpperBound b False)
  == (LowerBound a True <= LowerBound a True) && (UpperBound b False <= UpperBound (b-1) True)
  == True                                     && False
  == False

The wrong step here is (UpperBound b False <= UpperBound (b-1) True) == False. It arises because the Ord instance of UpperBound first compares the bounds, and only if they are equal checks whether they are inclusive or not. The wrong assumption it makes is that "if b is bigger than b-1, an interval ending at b cannot be contained in an interval ending at b-1". This holds in the continuous case, but not in the discrete case.

The Ord instance of LowerBound makes the same mistake, mutatis mutandis.

A bonus bug

contains is also wrong when it comes to empty sets. It holds $[0,1]\supseteq\emptyset=[3,2]$, but

Interval (LowerBound (Finite 0) True) (UpperBound (Finite 1) True) 
  `contains` Interval (LowerBound (Finite 3) True) (UpperBound (Finite 2) True)

evaluates to False.

Steps to reproduce the behavior

• Open a repl.
• import Plutus.V1.Ledger.Interval
• Evaluate a few examples like the ones above.

Actual Result

If one reads contains as $\supseteq$, and does the appropriate translations of open and closed intervals, inclusions of the forms

• $[a,b-1]\supseteq[a,b)$
• $[a+1,b]\supseteq(a,b]$
• $[a+1,b-1]\supseteq(a,b)$
• ...

all evaluate to False on Integer.

Expected Result

The inclusions above should all evaluate to True.

Describe the approach you would take to fix this

If I'm not mistaken, there are no uses of Interval a with "continuous" a. Should that be the case, a solution would be to have Interval a be isomorphic to (Maybe a, Maybe b), where every Just denotes an included bound, and Nothing stands for $\pm\infty$.

If there are uses for intervals of "continuous" element types, one could implement a function like containsDiscrete :: (Ord a, Enum a) => Interval a -> Interval a -> Bool to do the right thing in the discrete case. (Edit: Enum is probably not a good idea, since it relies on Int, which may be too small...)

In any case, the problem with empty sets is easy to solve by adding an emptyness check for the second argument to the implementation of contains.

System info

irrelevant

[effectfully]

Thank you very much for such a well-written report. We're already working on the issue.

[effectfully]

@carlhammann, the issue is resolved, thanks again for the fantastic report!

[michaelpj]

Yep, this was gold.

[carlhammann]

Thanks for the kind words, guys!