Splitting and Splicing Intervals (Part 1)

Posted by Ranjit Jhala Dec 15, 2017


Joachim Breitner wrote a cool post describing a library for representing sets of integers as sorted lists of intervals, and how they were able to formally verify the code by translating it to Coq using their nifty new tool.

  • First, lets just see how plain refinement types let us specify the key “goodness” invariant, and check it automatically.

  • Next, we’ll see how LH’s new “type-level computation” abilities let us specify and check “correctness”, and even better, understand why the code works.

(Click here to demo)

Ribbons

Encoding Sets as Intervals

The key idea underlying the intervals data structure, is that we can represent sets of integers like:

by first ordering them into a list

and then partitioning the list into compact intervals

That is,

  1. Each interval (from, to) corresponds to the set {from,from+1,...,to-1}.

  2. Ordering ensures there is a canonical representation that simplifies interval operations.

Making Illegal Intervals Unrepresentable

We require that the list of intervals be “sorted, non-empty, disjoint and non-adjacent”. Lets follow the slogan of make-illegal-values-unrepresentable to see how we can encode the legality constraints with refinements.

A Single Interval

We can ensure that each interval is non-empty by refining the data type for a single interval to specify that the to field must be strictly bigger than the from field:

104: {-@ data Interval = I
105:       { from :: Int
106:       , to   :: {v: Int | from < v }
107:       }
108:   @-}

Now, LH will ensure that we can only construct legal, non-empty Intervals

115: IntervalgoodItv = {v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 10 20
116: IntervalbadItv  = {v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 20 10     -- ILLEGAL: empty interval!

Many Intervals

We can represent arbitrary sets as a list of Intervals:

124: data Intervals = Intervals { itvs :: [Interval] }

The plain Haskell type doesn’t have enough teeth to enforce legality, specifically, to ensure ordering and the absence of overlaps. Refinements to the rescue!

First, we specify a lower-bounded Interval as:

134: {-@ type LbItv N = {v:Interval | N <= from v} @-}

Intuitively, an LbItv n is one that starts (at or) after n.

Next, we use the above to define an ordered list of lower-bounded intervals:

143: {-@ type OrdItvs N = [LbItv N]<{\vHd vTl -> to vHd <= from vTl}> @-}

The signature above uses an abstract-refinement to capture the legality requirements.

  1. An OrdInterval N is a list of Interval that are lower-bounded by N, and

  2. In each sub-list, the head Interval vHd precedes each in the tail vTl.

We can now describe legal Intervals simply as:

161: {-@ data Intervals = Intervals { itvs :: OrdItvs 0 } @-}

LH will now ensure that illegal Intervals are not representable.

167: IntervalsgoodItvs  = {v : x1:[{v : Interval | 0 <= Intervals.from v}] -> {v : Intervals | Intervals.itvs v == x1
                                                                     && lqdc##$select v == x1
                                                                     && v == Intervals.Intervals x1} | v == Intervals.Intervals}Intervals [{v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 1 5, {v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 7 8, {v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 9 13]  -- LEGAL
168: 
169: IntervalsbadItvs1  = {v : x1:[{v : Interval | 0 <= Intervals.from v}] -> {v : Intervals | Intervals.itvs v == x1
                                                                     && lqdc##$select v == x1
                                                                     && v == Intervals.Intervals x1} | v == Intervals.Intervals}Intervals [{v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 1 7, {v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 5 8]          -- ILLEGAL: overlap!
170: IntervalsbadItvs2  = {v : x1:[{v : Interval | 0 <= Intervals.from v}] -> {v : Intervals | Intervals.itvs v == x1
                                                                     && lqdc##$select v == x1
                                                                     && v == Intervals.Intervals x1} | v == Intervals.Intervals}Intervals [{v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 1 5, {v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 9 13, {v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I 7 8]  -- ILLEGAL: disorder!

Do the types really capture the legality requirements? In the original code, Breitner described goodness as a recursively defined predicate that takes an additional lower bound lb and returns True iff the representation was legal:

180: goodLIs :: Int -> [Interval] -> Bool
181: x1:{v : Int | v >= 0} -> [{v : Interval | x1 <= Intervals.from v}] -> {v : Bool | v}goodLIs _ []              = True
182: goodLIs lb ((I f t) : is) = Boollb x1:Int -> x2:Int -> {v : Bool | v <=> x1 <= x2}<= f {v : x1:Bool -> x2:Bool -> {v : Bool | v <=> x1
                                             && x2} | v == GHC.Classes.&&}&& {v : Bool | v <=> f < t}f x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< t {v : x1:Bool -> x2:Bool -> {v : Bool | v <=> x1
                                             && x2} | v == GHC.Classes.&&}&& x1:{v : Int | v >= 0} -> [{v : Interval | x1 <= Intervals.from v}] -> {v : Bool | v}goodLIs t is

We can check that our type-based representation is indeed legit by checking that goodLIs returns True whenever it is called with a valid of OrdItvs:

190: {-@ goodLIs :: lb:Nat -> is:OrdItvs lb -> {v : Bool | v } @-}

Algorithms on Intervals

We represent legality as a type, but is that good for? After all, we could, as seen above, just as well have written a predicate goodLIs? The payoff comes when it comes to using the Intervals e.g. to implement various set operations.

For example, here’s the code for intersecting two sets, each represented as intervals. We’ve made exactly one change to the function implemented by Breitner: we added the extra lower-bound parameter lb to the recursive go to make clear that the function takes two OrdItvs lb and returns an OrdItvs lb.

210: intersect :: Intervals -> Intervals -> Intervals
211: Intervals -> Intervals -> Intervalsintersect (Intervals is1) (Intervals is2) = {v : x1:[{v : Interval | 0 <= Intervals.from v}] -> {v : Intervals | Intervals.itvs v == x1
                                                                     && lqdc##$select v == x1
                                                                     && v == Intervals.Intervals x1} | v == Intervals.Intervals}Intervals ({v : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] | v == go}go 0 is1 is2)
212:   where
213:     {-@ go :: lb:Int -> OrdItvs lb -> OrdItvs lb -> OrdItvs lb @-}
214:     x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go _ _ [] = []
215:     go _ [] _ = []
216:     go lb (i1@(I f1 t1) : is1) (i2@(I f2 t2) : is2)
217:       -- reorder for symmetry
218:       | {v : Bool | v <=> t1 < t2}t1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< t2   = x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go lb (i2:is2) (i1:is1)
219:       -- disjoint
220:       | {v : Bool | v <=> f1 >= t2}f1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 >= x2}>= t2  = x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go lb (i1:is1) is2
221:       -- subset
222:       | {v : Bool | v <=> t1 == t2}t1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 == x2}== t2  = {v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I f' t2 : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go t2 is1 is2
223:       -- overlapping
224:       | {v : Bool | v <=> f2 < f1}f2 x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< f1   = ({v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I f' t2 : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go t2 ({v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I t2 t1 : is1) is2)
225:       | otherwise = x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go lb ({v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I f2 t1 : is1) (i2:is2)
226:       where {v : Int | v == (if f1 > f2 then f1 else f2)}f'    = x1:Int -> x2:Int -> {v : Int | v == (if x1 > x2 then x1 else x2)}max f1 f2

Internal vs External Verification

By representing legality internally as a refinement type, as opposed to externally as predicate (goodLIs) we have exposed enough information about the structure of the values that LH can automatically chomp through the above code to guarantee that we haven’t messed up the invariants.

To appreciate the payoff, compare to the effort needed to verify legality using the external representation used in the hs-to-coq proof.

The same principle and simplification benefits apply to both the union

245: union :: Intervals -> Intervals -> Intervals
246: Intervals -> Intervals -> Intervalsunion (Intervals is1) (Intervals is2) = {v : x1:[{v : Interval | 0 <= Intervals.from v}] -> {v : Intervals | Intervals.itvs v == x1
                                                                     && lqdc##$select v == x1
                                                                     && v == Intervals.Intervals x1} | v == Intervals.Intervals}Intervals ({v : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] | v == go}go 0 is1 is2)
247:   where
248:     {-@ go :: lb:Int -> OrdItvs lb -> OrdItvs lb -> OrdItvs lb @-}
249:     x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go _ [Interval]is [] = is
250:     go _ [] is = is
251:     go lb (i1@(I f1 t1) : is1) (i2@(I f2 t2) : is2)
252:       -- reorder for symmetry
253:       | {v : Bool | v <=> t1 < t2}t1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 < x2}< t2 = x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go lb (i2:is2) (i1:is1)
254:       -- disjoint
255:       | {v : Bool | v <=> f1 > t2}f1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 > x2}> t2 = i2 : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go t2 (i1:is1) is2
256:       -- overlapping
257:       | otherwise  = x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go lb ( ({v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I f' t1) : is1) is2
258:       where
259:         {v : Int | v == (if f1 < f2 then f1 else f2)}f' = x1:Int -> x2:Int -> {v : Int | v == (if x1 < x2 then x1 else x2)}min f1 f2

and the subtract functions too:

265: subtract :: Intervals -> Intervals -> Intervals
266: Intervals -> Intervals -> Intervalssubtract (Intervals is1) (Intervals is2) = {v : x1:[{v : Interval | 0 <= Intervals.from v}] -> {v : Intervals | Intervals.itvs v == x1
                                                                     && lqdc##$select v == x1
                                                                     && v == Intervals.Intervals x1} | v == Intervals.Intervals}Intervals ({v : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] | v == go}go 0 is1 is2)
267:   where
268:     {-@ go :: lb:Int -> OrdItvs lb -> OrdItvs lb -> OrdItvs lb @-}
269:     x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go _ [Interval]is [] = is
270:     go _ [] _  = []
271:     go lb (i1@(I f1 t1) : is1) (i2@(I f2 t2) : is2)
272:       -- i2 past i1
273:       | {v : Bool | v <=> t1 <= f2}t1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 <= x2}<= f2  = (i1 : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go t1 is1 (i2:is2))
274:       -- i1 past i2
275:       | {v : Bool | v <=> t2 <= f1}t2 x1:Int -> x2:Int -> {v : Bool | v <=> x1 <= x2}<= f1  = (x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go lb (i1:is1) is2)
276:       -- i1 contained in i2
277:       | {v : Bool | v <=> f2 <= f1}f2 x1:Int -> x2:Int -> {v : Bool | v <=> x1 <= x2}<= f1, {v : Bool | v <=> t1 <= t2}t1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 <= x2}<= t2 = x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go lb is1 (i2:is2)
278:       -- i2 covers beginning of i1
279:       | {v : Bool | v <=> f2 <= f1}f2 x1:Int -> x2:Int -> {v : Bool | v <=> x1 <= x2}<= f1 = x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go t2 ({v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I t2 t1 : is1) is2
280:       -- -- i2 covers end of i1
281:       | {v : Bool | v <=> t1 <= t2}t1 x1:Int -> x2:Int -> {v : Bool | v <=> x1 <= x2}<= t2 = (({v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I f1 f2) : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go f2 is1 (i2:is2))
282:       -- i2 in the middle of i1
283:       | otherwise = ({v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I f1 f2 : x1:Int -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}] -> [{v : Interval | x1 <= Intervals.from v}]go f2 ({v : x1:Int -> x2:{v : Int | x1 < v} -> {v : Interval | Intervals.to v == x2
                                                        && Intervals.from v == x1
                                                        && lqdc##$select v == x2
                                                        && lqdc##$select v == x1
                                                        && v == Intervals.I x1 x2} | v == Intervals.I}I t2 t1 : is1) is2)

both of which require non-trivial proofs in the external style. (Of course, its possible those proofs can be simplified.)

Summing Up (and Looking Ahead)

I hope the above example illustrates why “making illegal states” unrepresentable is a great principle for engineering code and proofs.

That said, notice that with hs-to-coq, Breitner was able to go far beyond the above legality requirement: he was able to specify and verify the far more important (and difficult) property that the above is a correct implementation of a Set library.

Is it even possible, let alone easier to do that with LH?