Trying to simplify RTQ for the paper

testcases/lazy-datastructures/RealTimeQueue-new.scala

+import leon.lazyeval._
+import leon.lazyeval.$._
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.instrumentation._
+
+object RealTimeQueue {
+
+  /**
+   * A stream of values of type T
+   */
+  sealed abstract class Stream[T] {
+    @inline
+    def isEmpty: Boolean = {
+      this match {
+        case SNil() => true
+        case _      => false
+      }
+    }
+
+    @inline
+    def isCons: Boolean = {
+      this match {
+        case SCons(_, _) => true
+        case _           => false
+      }
+    }
+
+    def size: BigInt = {
+      this match {
+        case SNil()      => BigInt(0)
+        case SCons(x, t) => 1 + ssize(t)
+      }
+    } ensuring (_ >= 0)
+  }
+  case class SCons[T](x: T, tail: $[Stream[T]]) extends Stream[T]
+  case class SNil[T]() extends Stream[T]
+
+  def ssize[T](l: $[Stream[T]]): BigInt = (l*).size
+
+  def isConcrete[T](l: $[Stream[T]]): Boolean = {
+    l.isEvaluated && (l* match {
+      case SCons(_, tail) =>
+        isConcrete(tail)
+      case _ => true
+    })
+  }
+
+   @invstate
+  def rotate[T](f: $[Stream[T]], r: List[T], a: $[Stream[T]]): Stream[T] = { // doesn't change state
+    require(r.size == ssize(f) + 1 && (firstUneval(f)*).isEmpty)
+    (f.value, r) match {
+      case (SNil(), Cons(y, _)) => //in this case 'y' is the only element in 'r'
+        SCons(y, a)
+      case (SCons(x, tail), Cons(y, r1)) =>
+        val newa: Stream[T] = SCons(y, a)
+        val rot = $(rotate(tail, r1, newa)) //this creates a lazy rotate operation
+        SCons(x, rot)
+    }
+  } ensuring (res => res.size == (f*).size + r.size + (a*).size && res.isCons && // using f*.size instead of ssize seems to speed up verification magically
+                     time <= 30)
+
+  def firstUneval[T](l: $[Stream[T]]): $[Stream[T]] = {
+    if (l.isEvaluated) {
+      l* match {
+        case SCons(_, tail) =>
+          firstUneval(tail)
+        case _ => l
+      }
+    } else
+      l
+  } ensuring (res => //(!(res*).isEmpty || isConcrete(l)) && //if there are no lazy closures then the stream is concrete
+    //((res*).isEmpty || !res.isEvaluated) && // if the return value is not a Nil closure then it would not have been evaluated
+    (res.value match {
+      case SCons(_, tail) =>
+        firstUneval(l) == firstUneval(tail) // after evaluating the firstUneval closure in 'l' we can access the next unevaluated closure
+      case _ => true
+    }))
+
+  case class Queue[T](f: $[Stream[T]], r: List[T], s: $[Stream[T]]) {
+    def isEmpty = (f*).isEmpty
+    def valid = {
+      (firstUneval(f) == firstUneval(s)) &&
+        ssize(s) == ssize(f) - r.size //invariant: |s| = |f| - |r|
+    }
+  }
+  
+  @inline
+  def createQ[T](f: $[Stream[T]], r: List[T], s: $[Stream[T]]) = {
+    s.value match {
+      case SCons(_, tail) => Queue(f, r, tail)
+      case SNil() =>
+        val newa: Stream[T] = SNil()
+        val rotres = $(rotate(f, r, newa))
+        Queue(rotres, Nil(), rotres)
+    }
+  }
+
+  def enqueue[T](x: T, q: Queue[T]): Queue[T] = {
+    require(q.valid)    
+    createQ(q.f, Cons(x, q.r), q.s)
+  } ensuring (res => res.valid && time <= 60)
+
+  def dequeue[T](q: Queue[T]): Queue[T] = {
+    require(!q.isEmpty && q.valid)
+    q.f.value match {
+      case SCons(x, nf) =>
+        createQ(nf, q.r, q.s)
+    }
+  } ensuring(res => res.valid && time <= 120)
+}

testcases/lazy-datastructures/RealTimeQueue.scala

@@ -5,7 +5,6 @@ import leon.annotation._
 import leon.collection._
 import leon.instrumentation._
 
-//TODO: need to automatically check monotonicity of isConcrete
 object RealTimeQueue {
 
   /**
@@ -38,7 +37,6 @@ object RealTimeQueue {
 
   def ssize[T](l: $[Stream[T]]): BigInt = (l*).size
 
-  //@monotonic
   def isConcrete[T](l: $[Stream[T]]): Boolean = {
     l.isEvaluated && (l* match {
       case SCons(_, tail) =>

testcases/orb-testcases/timing/ConstantPropagation.scala

@@ -76,7 +76,7 @@ object ConstantPropagation {
 
   /**
    * Assuming that the functions are ordered from callee to
-   * caller and there is no mutual recursion
+   * caller and there is no mutual recursion, only self recursion
    */
   case class Program(funcs: List[Function])