aiken/interval

In a eUTxO-based blockchain like Cardano, the management of time can be finicky.

Indeed, in order to maintain a complete determinism in the execution of scripts, it is impossible to introduce a notion of “current time” since the execution would then depend on factor that are external to the transaction itself: the ineluctable stream of time flowing in our universe.

Hence, to work around that, we typically define time intervals, which gives window – a.k.a intervals – within which the transaction can be executed. From within a script, it isn’t possible to know when exactly the script is executed, but we can reason about the interval bounds to validate pieces of logic.

Example

Let’s consider an example and assume an auction with a bidding period over an interval $biddingPeriod = [start_{bid}, end_{bid})$ .

Bidders for the auction must be whitelisted by an administrator before the bidding period starts.
Once the bidding period is over, the auction winner may collect its due by paying the agreed price.

This scenario identifies three periods:

   pre-bidding            bidding            post-bidding
-----------------[-----------------------)----------------->
             start_bid                end_bid

If we call $validityRange = [start_{tx}, end_{tx})$ the validity interval of transactions during each period, we must then have:

In Plutus V3, transaction validity ranges are always semi-open intervals, open in their upper bound.

Pre-bidding: $end_{tx} \lt start_{bid}$

validity_range |> interval.is_entirely_before(start_bid)

Bidding: $validityRange \subseteq biddingPeriod$
```
bidding_period |> interval.includes(validity_range)
```
or alternatively $start_{tx} \geq start_{bid}$ and $end_{tx} \lt end_{bid}$ :
```
and {
  bidding_period |> interval.contains(start_tx),
  bidding_period |> interval.contains(end_tx),
}
```

Post-bidding: $start_{tx} \gt end_{bid}$

validity_range |> interval.is_entirely_after(end_bid)

Types

Interval

A type to represent intervals of values. Interval are inhabited by an integer value representing have a finite lower-bound and/or upper-bound.

This allows to represent all kind of mathematical intervals:

// [1; 10]
let i0: Interval = Interval
  { lower_bound:
      IntervalBound { bound_type: Finite(1), is_inclusive: True }
  , upper_bound:
      IntervalBound { bound_type: Finite(10), is_inclusive: True }
  }

// (20; infinity)
let i1: Interval = Interval
  { lower_bound:
      IntervalBound { bound_type: Finite(20), is_inclusive: False }
  , upper_bound:
      IntervalBound { bound_type: PositiveInfinity, is_inclusive: False }
  }

Constructors

Interval { lower_bound: IntervalBound, upper_bound: IntervalBound }

IntervalBound

An interval bound, either inclusive or exclusive.

Constructors

IntervalBound { bound_type: IntervalBoundType, is_inclusive: Bool }

IntervalBoundType

A type of interval bound. The value for the Finite case typically represents a number of seconds or milliseconds.

Constructors

```
NegativeInfinity
```
```
Finite(Int)
```
```
PositiveInfinity
```

Constants

empty: Interval

Create an empty interval that contains no value.

interval.contains(empty, 0) == False
interval.contains(empty, 1000) == False

everything: Interval

Create an interval that contains every possible values. i.e. $(-∞, +∞)$

interval.contains(everything, 0) == True
interval.contains(everything, 1000) == True

Functions

Constructing

after(lower_bound: Int) -> Interval

Create an interval that includes all values greater than the given bound. i.e $[lower_bound, +∞]$

interval.after(10) == Interval {
  lower_bound: IntervalBound { bound_type: Finite(10), is_inclusive: True },
  upper_bound: IntervalBound { bound_type: PositiveInfinity, is_inclusive: True },
}

entirely_after(lower_bound: Int) -> Interval

Create an interval that includes all values after (and not including) the given bound. i.e $(lower_bound, +∞]$

interval.entirely_after(10) == Interval {
  lower_bound: IntervalBound { bound_type: Finite(10), is_inclusive: False },
  upper_bound: IntervalBound { bound_type: PositiveInfinity, is_inclusive: True },
}

before(upper_bound: Int) -> Interval

Create an interval that includes all values before (and including) the given bound. i.e $(-∞, upper_bound]$

interval.before(100) == Interval {
  lower_bound: IntervalBound { bound_type: NegativeInfinity, is_inclusive: True },
  upper_bound: IntervalBound { bound_type: Finite(100), is_inclusive: True },
}

entirely_before(upper_bound: Int) -> Interval

Create an interval that includes all values before (and not including) the given bound. i.e $(-∞, upper_bound)$

interval.entirely_before(10) == Interval {
  lower_bound: IntervalBound { bound_type: NegativeInfinity, is_inclusive: True },
  upper_bound: IntervalBound { bound_type: Finite(10), is_inclusive: False },
}

between(lower_bound: Int, upper_bound: Int) -> Interval

Create an interval that includes all values between two bounds, including the bounds. i.e. $[lower_bound, upper_bound]$

interval.between(10, 100) == Interval {
  lower_bound: IntervalBound { bound_type: Finite(10), is_inclusive: True },
  upper_bound: IntervalBound { bound_type: Finite(100), is_inclusive: True },
}

entirely_between(lower_bound: Int, upper_bound: Int) -> Interval

Create an interval that includes all values between two bounds, excluding the bounds. i.e. $(lower_bound, upper_bound)$

interval.entirely_between(10, 100) == Interval {
  lower_bound: IntervalBound { bound_type: Finite(10), is_inclusive: False },
  upper_bound: IntervalBound { bound_type: Finite(100), is_inclusive: False },
}

Inspecting

contains(self: Interval, elem: Int) -> Bool

Checks whether an element is contained within the interval.

let iv =
  Interval {
    lower_bound: IntervalBound {
      bound_type: Finite(14),
      is_inclusive: True
    },
    upper_bound: IntervalBound {
      bound_type: Finite(42),
      is_inclusive: False
    },
  }

interval.contains(iv, 25) == True
interval.contains(iv, 0) == False
interval.contains(iv, 14) == True
interval.contains(iv, 42) == False

is_empty(1st_arg: Interval) -> Bool

Tells whether an interval is empty; i.e. that is contains no value.

let iv1 = interval.empty

let iv2 = Interval {
    lower_bound: IntervalBound { bound_type: Finite(0), is_inclusive: False },
    upper_bound: IntervalBound { bound_type: Finite(0), is_inclusive: False },
  }

let iv3 = Interval {
    lower_bound: IntervalBound { bound_type: Finite(0), is_inclusive: False },
    upper_bound: IntervalBound { bound_type: Finite(100), is_inclusive: False },
  }

interval.is_empty(iv1) == True
interval.is_empty(iv2) == True
interval.is_empty(iv3) == False

// Note: Two empty intervals are not necessarily equal.
iv1 != iv2

is_entirely_after(self: Interval, point: Int) -> Bool

Check whether the interval is entirely after a given point.

interval.is_entirely_after(interval.after(10), 5) == True
interval.is_entirely_after(interval.after(10), 10) == False
interval.is_entirely_after(interval.after(10), 15) == False
interval.is_entirely_after(interval.between(10, 20), 30) == False
interval.is_entirely_after(interval.between(10, 20), 5) == True

is_entirely_before(self: Interval, point: Int) -> Bool

Check whether the interval is entirely before a given point.

interval.is_entirely_before(interval.before(10), 15) == True
interval.is_entirely_before(interval.before(10), 10) == False
interval.is_entirely_before(interval.before(10), 5) == False
interval.is_entirely_before(interval.between(10, 20), 30) == True
interval.is_entirely_before(interval.between(10, 20), 5) == False

to_string(self: Interval) -> String

Obtain a human-readable string representation of the interval. Useful for debugging.

Combining

hull(iv1: Interval, iv2: Interval) -> Interval

Computes the smallest interval containing the two given intervals, if any

let iv1 = between(0, 10) // [0, 10]
let iv2 = between(2, 14) // [2, 14]
hull(iv1, iv2) == between(0, 14)

let iv1 = between(5, 10) // [5, 10]
let iv2 = before(0) // [ْ-∞, 0]
hull(iv1, iv2) == before(10)

let iv1 = entirely_after(0) // (0, +∞]
let iv2 = between(10, 42)  // [10, 42]
hull(iv1, iv2) = entirely_after(0)

includes(self: Interval, other: Interval) -> Bool

Checks whether the second interval is fully included in the first.

between(-5, 5)  // [-5, 5]
  |> includes(between(0, 2)) // [0, 2]

between(-5, 5)  // [-5, 5]
  |> includes(entirely_between(-5, 5)) // (-5, 5)

after(0) // [0, +∞]
  |> includes(after(1)) // [1, +∞]

before(-1) // (-∞, -1]
  |> includes(entirely_before(-1)) // [-∞, -1)

intersection(iv1: Interval, iv2: Interval) -> Interval

Computes the largest interval contained in the two given intervals, if any.

let iv1 = interval.between(0, 10) // [0, 10]
let iv2 = interval.between(2, 14) // [2, 14]
interval.intersection(iv1, iv2) == interval.between(2, 10)

let iv1 = interval.entirely_before(10) // [-∞, 10)
let iv2 = interval.entirely_after(0) // (0, +∞]
interval.intersection(iv1, iv2) == interval.entirely_between(0, 10)

let iv1 = interval.between(0, 1) // [0, 1]
let iv2 = interval.between(2, 3) // [2, 3]
interval.intersection(iv1, iv2) |> interval.is_empty