Splitting and Splicing Intervals (Part 1)
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)
41: {-@ LIQUID "--short-names" @-} 42: {-@ LIQUID "--exact-data-con" @-} 43: {-@ LIQUID "--no-adt" @-} 44: {-@ LIQUID "--prune-unsorted" @-} 45: {-@ LIQUID "--higherorder" @-} 46: {-@ LIQUID "--no-termination" @-} 47: 48: module Intervals where 49: 50: data Interval = I 51: { from :: Int 52: , to :: Int 53: } deriving ((Show Interval)Show) 54:
Encoding Sets as Intervals¶
The key idea underlying the intervals data structure, is that we can represent sets of integers like:
{ 7, 1, 10, 3, 11, 2, 9, 12, 4}
by first ordering them into a list
[ 1, 2, 3, 4, 7, 9, 10, 11, 12 ]
and then partitioning the list into compact intervals
[ (1, 5), (7, 8), (9, 13) ]
That is,
-
Each interval
(from, to)corresponds to the set{from,from+1,...,to-1}. -
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.
-
An
OrdInterval Nis a list ofIntervalthat are lower-bounded byN, and -
In each sub-list, the head
IntervalvHdprecedes each in the tailvTl.
Legal Intervals¶
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?