Time weirdnesses in `plutus-ledger-api` and `cardano-ledger`

The work on PR #233 uncovered strange behaviours of functions from plutus-ledger-api and cardano-ledger with regards to the handling of time intervals.

Introductory example

For context, imagine we have a validator that checks that some transaction happens before a deadline like this:

import qualified Plutus.V1.Ledger.Interval as Interval
import qualified Plutus.V2.Ledger.Contexts as PV2

...    Interval.to deadline `Interval.contains` PV2.txInfoValidRange txi

(Here is the actual line that led to this excursion.)

Here are two expectations I have about this code:

The check succeeds if and only if the last millisecond of the PV2.txInfoValidRange txi is at most deadline.
The PV2.txInfoValidRange txi will contain no millisecond outside the time range covered by the slot range of the Cardano transaction corresponding to txi.

Both of these expectations are violated. Let's start with the first one.

Strange behaviour of `Interval.contains`

Assume PV2.txInfoValidRange txi is of the form Interval (LowerBound a True) (UpperBound b False), that is, a half-open interval $[a,b)$. Since we're talking about a discrete interval milliseconds here, we have $[a,b-1] = [a,b)$. In particular, $[a,b-1]\supseteq[a,b)$.

However, Interval.contains disagrees: Following its implementation, and in particular the Ord instance of UpperBound, and noting that the interval $[a,b-1]$ is represented as Interval (LowerBound a True) (UpperBound (b-1) True), it computes

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.

Strange `txInfoValidRange` for left-unbounded transaction validity ranges

Cardano transactions have a validity range in terms of slots, while the TxInfo presents the validity range as an Interval of milliseconds. For Babbage, the function babbageTxInfo consumes a transaction, whose validity range is described in terms of slots, and produces a TxInfo, which describes the validity range of the transaction as an interval of milliseconds (the txInfoValidRange). Drilling down, the function that does the translation of slot ranges to milliseconds is transVITime.

For most slot intervals, transVITime does what I would expect, but for left-unbounded intervals like ValidityIntervel SNothing (SJust i) I don't understand its behaviour. Depending on some condition on the protocol version (I think?) it'll either return

a right-closed interval ending at the first millisecond of the first slot after i (the else case). I think this behaviour is incorrect, as it violates the expectation 2 from the introduction
a right-open interval ending at this point (the then case). I think this is correct, and it's also the behaviour for all other right-bounded intervals.

Can someone please

validate what I wrote above (I know that I'm seeing this behaviour when I actually run such examples and print the txInfoValidRange, but not whether the functions I'm pointing at acutally are the relevant ones and do what I claim they do), and
explain the reasoning behind this?

The upshot for the introductory example

In combination, the two behaviours I described mean that the two expectations outlined at the beginning are violated, if deadline is the last millisecond of a slot:

If the txInfoValidRange is of the first kind described (right closed, and including the first millisecond of the next slot), the check fails because expectation 2 does not hold. The first millisecond of the next slot after deadline is greater than deadline.
If the txInfoValidRange is of the second kind described (right-open, ending at the first millisecond of the next slot), the check fails because of the problem with Interval.contains. That is, even if the txInfoValidRange is what it should be, the comparison with Interval.to fails, because Interval.to is the closed interval ending at deadline, and txInfoValidRange is the open interval ending at deadline+1.

tweag / cooked-validators