How can I define an AVL tree in Stainless?

[mingyang91]

I am having difficulty defining an AVL tree using Stainless. In Liquid Haskell, I can define AVL using the following code:

-- | Trees with value less than X
{-@ type AVLL a X = AVL {v:a | v < X}  @-}

-- | Trees with value greater than X
{-@ type AVLR a X = AVL {v:a | X < v}  @-}

{-@ data AVL a = Leaf
               | Node { key :: a
                      , l   :: AVLL a key
                      , r   :: {v:AVLR a key | isBal l v 1}
                      , ah  :: {v:Nat        | isReal v l r}
                      }                                  @-}

But migrating to stainless is difficult, as shown in the following code:

enum BST[V: Ord]: // Can't put Ord typeclass in there
  case Empty()
  case Node(left: BST[V], data: V, right: BST[V], h: BigInt)

  require(
    this match
      case Empty() => true
      case Node(l, v, r, _) =>
        l.value.forall(Ord[V].lessThan(_, v))
          && r.value.forall(Ord[V].greaterThan(_, v))
  )

and this code.

enum BST[V <: Ordering[V]]
// illegal cyclic type reference: lower bound Ordering[V] of type V refers back to the type itself

How can I define an AVL tree in Stainless?

[mario-bucev]

Hello! One way to include the Ord typeclass is to have it as a field in BST:

import stainless.*
import stainless.collection.*
import stainless.algebra.*

sealed abstract class BST[V]:
  val ord: TotalOrder[V] // here

  // unbalanced invariant, which should be put before and after each operation method
  // (having it in a require causes an unfortunate crash)
  def valid: Boolean =
    this match
      case Empty(_) => true
      case Node(l, v, r, _, _) =>
        l.values.forall(ord.compare(_, v) < 0)
          && r.values.forall(ord.compare(_, v) > 0)

  def values: List[V] =
    this match
      case Empty(_) => Nil()
      case Node(l, v, r, _, _) => l.values ++ List(v) ++ r.values

  def insert(v: V): BST[V] = {
    require(valid)
    // ...
  }.ensuring(_.valid)

case class Empty[V](override val ord: TotalOrder[V]) extends BST[V]
case class Node[V](left: BST[V], data: V, right: BST[V], h: BigInt, override val ord: TotalOrder[V]) extends BST[V]

In this example, I'm using stainless.algebra.{Eq, PartialOrder, TotalOrder} from here (which should be included explicitly when invoking Stainless). Hope this helps! If not, please do not hesitate to comment further :)

[mingyang91]

Thank you for you response, I will try later.

By the way, the first idea that came to mind was to use invariant to constrain it is ordered, because it is very simple - just left < value < right. But I was not successful because of the below reason.

Then I tried to add require and ensuring into every operator, as you suggested. But I have a question - if I want to achieve the best form, is it necessary to modify the AVL constructor to private and only expose wrapped operators (e.g. insert/delete/contains)?

[mario-bucev]

Then I tried to add require and ensuring into every operator, as you suggested. But I have a question - if I want to achieve the best form, is it necessary to modify the AVL constructor to private and only expose wrapped operators (e.g. insert/delete/contains)?

If I'm understanding correctly, it's not really required for correctness, it's just that the user may construct an AVL tree that is not valid and won't be able to call operations that require validity. But this idea is nice to prevent "accidental" construction and avoid the user later confusion!

[romac]

@mario-bucev Does it also crash when adding @invariant to valid and removing the pre/post-conditions?

sealed abstract class BST[V]:
  val ord: TotalOrder[V]

  @invariant
  def valid: Boolean = // ...

  def insert(v: V): BST[V] = {
    // ...
  }
}

[mario-bucev]

Alas no, I get the same crash. It seems to be that the invariant FunDef is not expecting a type parameter while it is being fed one (maybe some interaction with TypeEncoding?)

[mingyang91]

How do I use the stainless.algebra? I tried to follow the documentation and added it to sbt as follows:

stainlessExtraDeps ++= Seq(
  "ch.epfl.lara" %% "stainless-algebra" % "0.1.2" cross(CrossVersion.for3Use2_13),
)

Then I ran sbt stainless-algebra/packageSrc to get the sources jar and put it into the stainless folder, but it did not work. I noticed that the source jar is only 253 bytes:

ll stainless/ch/epfl/lara/stainless-algebra_2.13/0.1.2
total 24
-rw-r--r--@ 1 mingyang  staff   253B May 11 23:32 stainless-algebra_2.13-0.1.2-sources.jar
-rw-r--r--@ 1 mingyang  staff   281B May 11 23:25 stainless-algebra_2.13-0.1.2.jar
-rw-r--r--@ 1 mingyang  staff   1.5K May 11 23:26 stainless-algebra_2.13-0.1.2.pom

[mario-bucev]

Good catch! It's indeed not packaged... We'll fix this for the next release, but in the meantime here is a correctly packaged archive stainless-algebra_2.13.zip (that should replace the incorrectly packaged one).

[vkuncak]

If you are checking how to do balanced trees in Stainless, maybe you should check the previous working examples https://github.com/epfl-lara/bolts/tree/master/data-structures/trees