-
Notifications
You must be signed in to change notification settings - Fork 11
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Time weirdnesses in plutus-ledger-api
and cardano-ledger
#309
Comments
With regard to the second problem, @ak3n has kindly pointed me to this issue on |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
The work on PR #233 uncovered strange behaviours of functions from
plutus-ledger-api
andcardano-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:
(Here is the actual line that led to this excursion.)
Here are two expectations I have about this code:
PV2.txInfoValidRange txi
is at mostdeadline
.PV2.txInfoValidRange txi
will contain no millisecond outside the time range covered by the slot range of the Cardano transaction corresponding totxi
.Both of these expectations are violated. Let's start with the first one.
Strange behaviour of
Interval.contains
Assume$[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)$ .
PV2.txInfoValidRange txi
is of the formInterval (LowerBound a True) (UpperBound b False)
, that is, a half-open intervalHowever,$[a,b-1]$ is represented as
Interval.contains
disagrees: Following its implementation, and in particular theOrd
instance ofUpperBound
, and noting that the intervalInterval (LowerBound a True) (UpperBound (b-1) True)
, it computesThe wrong step here is
(UpperBound b False <= UpperBound (b-1) True) == False
. It arises because theOrd
instance ofUpperBound
first compares the bounds, and only if they are equal checks whether they are inclusive or not. The wrong assumption it makes is that "ifb
is bigger thanb-1
, an interval ending atb
cannot be contained in an interval ending atb-1
". This holds in the continuous case, but not in the discrete case.Strange
txInfoValidRange
for left-unbounded transaction validity rangesCardano transactions have a validity range in terms of slots, while the
TxInfo
presents the validity range as anInterval
of milliseconds. For Babbage, the functionbabbageTxInfo
consumes a transaction, whose validity range is described in terms of slots, and produces aTxInfo
, which describes the validity range of the transaction as an interval of milliseconds (thetxInfoValidRange
). Drilling down, the function that does the translation of slot ranges to milliseconds istransVITime
.For most slot intervals,
transVITime
does what I would expect, but for left-unbounded intervals likeValidityIntervel SNothing (SJust i)
I don't understand its behaviour. Depending on some condition on the protocol version (I think?) it'll either returni
(theelse
case). I think this behaviour is incorrect, as it violates the expectation 2 from the introductionthen
case). I think this is correct, and it's also the behaviour for all other right-bounded intervals.Can someone please
txInfoValidRange
, but not whether the functions I'm pointing at acutally are the relevant ones and do what I claim they do), andThe 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: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 afterdeadline
is greater thandeadline
.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 withInterval.contains
. That is, even if thetxInfoValidRange
is what it should be, the comparison withInterval.to
fails, becauseInterval.to
is the closed interval ending atdeadline
, andtxInfoValidRange
is the open interval ending atdeadline+1
.The text was updated successfully, but these errors were encountered: