Some examples of equivalence checking

frontends/benchmarks/equivalence/addHorn.scala

@@ -0,0 +1,29 @@
+// Examples are figures from paper:
+// Automating Regression Verification.
+// https://doi.org/10.1145/2642937.2642987
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object AddHorn {
+
+  def add_horn_1(i: BigInt, j: BigInt): BigInt = {
+    require(i >= 0)
+    if (i == 0) j 
+    else add_horn_1(i-1, j+1)
+  }
+
+  def add_horn_2(i: BigInt, j: BigInt): BigInt = {
+    require(i >= 0)
+    if (i == 0) j 
+    else if (i == 1) j + 1
+    else add_horn_2(i-1, j+1)
+  }
+
+  @traceInduct("")
+  def check_add_horn(i: BigInt, j: BigInt): Unit = {
+    require(i >= 0)
+  } ensuring(add_horn_1(i, j) == add_horn_2(i, j))
+
+}

frontends/benchmarks/equivalence/factorial.scala

@@ -0,0 +1,26 @@
+// Examples are figures from paper:
+// Regression Verification for unbalanced recursive functions
+// https://iew.technion.ac.il/~ofers/publications/fm16.pdf
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object Factorial {
+
+  // Fig. 14
+
+  def fact14_1(n: BigInt): BigInt = 
+    if (n <= 1) 1 
+    else n * fact14_1(n-1)
+
+  def fact14_2(n: BigInt): BigInt =
+    if (n <= 1) 1 
+    else if (n == 10) 3628800
+    else n * fact14_2(n-1)
+
+  @traceInduct("")
+  def check_fact14(n: BigInt): Unit = {
+  } ensuring(fact14_1(n) == fact14_2(n))
+
+}

frontends/benchmarks/equivalence/fibonacci.scala

@@ -0,0 +1,29 @@
+// Examples are figures from paper:
+// Regression verification of unbalanced recursive functions with multiple calls (long version)
+// https://arxiv.org/pdf/2207.14364.pdf
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object Fibonacci {
+
+  // Fig. 4
+
+  def f1(n: BigInt): BigInt = {
+    if (n < 1) 0
+    else if (n <= 2) 1
+    else f1(n-1) + f1(n-2)
+  }
+
+  def f2(n: BigInt): BigInt = {
+    if (n < 1) 0
+    else if (n <= 2) 1
+    else f2(n-2) + f2(n-2) + f2(n-3)
+  }
+
+  @traceInduct("")
+  def check_f(n: BigInt): Unit = {
+  } ensuring(f1(n) == f2(n))
+
+}

frontends/benchmarks/equivalence/fullAlternation.scala

@@ -0,0 +1,34 @@
+// Examples are figures from paper:
+// Regression verification of unbalanced recursive functions with multiple calls (long version)
+// https://arxiv.org/pdf/2207.14364.pdf
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object FullAlternation {
+
+  // Fig. 12
+
+  def m1(n: BigInt, flag: Boolean): BigInt = {
+    if (n < 1) 0
+    else if (n == 1) 1
+    else m1(n - 1, !flag) + m1(n - 2, !flag)
+  }
+
+  def m2(n: BigInt, mode: Boolean): BigInt = {
+    if (n < 1) 0
+    else if (n == 1 || n == 2) 1
+    else {
+      var results: BigInt = 0
+      if (mode) results = m2(n-2, !mode) + m2(n-2, !mode) + m2(n-3, !mode)
+      if (!mode) results = m2(n-1, !mode) + m2(n-2, !mode)
+      results 
+    }
+  }
+
+  @traceInduct("")
+  def check_m(n: BigInt, flag: Boolean): Unit = {
+  } ensuring(m1(n, flag) == m2(n, flag))
+
+}

frontends/benchmarks/equivalence/halfAlternation.scala

@@ -0,0 +1,29 @@
+// Examples are figures from paper:
+// Regression verification of unbalanced recursive functions with multiple calls (long version)
+// https://arxiv.org/pdf/2207.14364.pdf
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object HalfAlternation {
+
+  // Fig. 14
+
+  def h1(n: BigInt): BigInt = {
+    if (n < 1) 0
+    else if (n == 1) 1
+    else h1(n - 1) + h1 (n - 2)
+  }
+
+  def h2(n: BigInt): BigInt = {
+    if (n < 1) 0
+    else if (n == 1) 1
+    else if ((n % 2) == 0) h2(n-1) + h2(n-2)
+    else h2(n-2) + h2(n-2) + h2(n-3)
+  }
+
+  @traceInduct("")
+  def check_h(n: BigInt): Unit = {
+  } ensuring(h1(n) == h2(n))
+}

frontends/benchmarks/equivalence/inlining.scala

@@ -0,0 +1,27 @@
+// Examples are figures from paper:
+// Automating Regression Verification.
+// https://doi.org/10.1145/2642937.2642987
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object Inlining {
+
+  def inlining_1(x: BigInt): BigInt = {
+    if (x > 0) inlining_1(x-1) + BigInt(1)
+    else if (x < 0) 0
+    else x
+  }
+
+  def inlining_2(x: BigInt): BigInt = {
+    if (x > 1) inlining_2(x-2) + BigInt(2)
+    else if (x < 0) 0
+    else x
+  }
+
+  @traceInduct("")
+  def check_inlining(n: BigInt): Unit = {
+  } ensuring(inlining_1(n) == inlining_2(n))
+
+}

frontends/benchmarks/equivalence/isSorted.scala

@@ -0,0 +1,47 @@
+import stainless.annotation._
+import stainless.lang._
+import stainless.collection._
+import stainless.proof._ 
+
+object IsSorted {
+
+  def isSortedR(l: List[Int]): Boolean = {
+    def loop(p: Int, l: List[Int]): Boolean = l match {
+      case Nil() => true
+      case Cons(x, xs) if (p <= x) => loop(x, xs)
+      case _ => false
+    }
+    if (l.isEmpty) true
+    else loop(l.head, l.tail)
+  }
+
+  def isSortedA(l: List[Int]): Boolean = {
+    def leq(cur: Int, next: Int): Boolean = cur < next
+    def iter(l: List[Int]): Boolean =
+      if (l.isEmpty) true
+      else if (l.tail.isEmpty) true
+      else leq(l.head, l.tail.head) && iter(l.tail) 
+    if (l.size < 2) true
+    else l.head <= l.tail.head && iter(l.tail)
+  }
+
+  def isSortedB(l: List[Int]): Boolean = {
+    if (l.isEmpty)
+      true
+    else if (!l.tail.isEmpty && l.head > l.tail.head)
+      false
+    else 
+      isSortedB(l.tail)
+  }
+
+  def isSortedC(l: List[Int]): Boolean = {
+    def chk(l: List[Int], p: Int, a: Boolean): Boolean = {
+      if (l.isEmpty) a
+      else if (l.head < p) false
+      else chk(l.tail, l.head, a)
+    }
+    if (l.isEmpty) true
+    else chk(l, l.head, true)
+  }
+
+}

frontends/benchmarks/equivalence/limit1.scala

@@ -0,0 +1,27 @@
+// Examples are figures from paper:
+// Automating Regression Verification.
+// https://doi.org/10.1145/2642937.2642987
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object Limit1 {
+
+  // REVE does not work -- requires manual unrolling
+
+  def limit1_1(n: BigInt): BigInt = {
+    if (n <= 1) n
+    else n + limit1_1(n-1)
+  }
+
+  def limit1_2(n: BigInt): BigInt = {
+    if (n <= 1) n
+    else n + n-1 + limit1_2(n-2)
+  }
+
+  @traceInduct("")
+  def check_limit1(n: BigInt): Unit = {
+  } ensuring(limit1_1(n) == limit1_2(n))
+
+}

frontends/benchmarks/equivalence/limit2.scala

@@ -0,0 +1,25 @@
+// Examples are figures from paper:
+// Automating Regression Verification.
+// https://doi.org/10.1145/2642937.2642987
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object Limit2 {
+
+  def limit2_1(n: BigInt): BigInt = {
+    if (n <= 0) n
+    else n + limit2_1(n-1)
+  }
+
+  def limit2_2(n: BigInt): BigInt = {
+    if (n <= 1) n
+    else n + limit2_2(n-1)
+  }
+
+  @traceInduct("")
+  def check_limit2(n: BigInt): Unit = {
+  } ensuring(limit2_1(n) == limit2_2(n))
+
+}

frontends/benchmarks/equivalence/limit3.scala

@@ -0,0 +1,29 @@
+// Examples are figures from paper:
+// Automating Regression Verification.
+// https://doi.org/10.1145/2642937.2642987
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object Limit3 {
+
+  def limit3_1(n: BigInt): BigInt = {
+    if (n <= 1) n
+    else n + limit3_1(n-1)
+  }
+
+  def limit3_2(n: BigInt): BigInt = {
+    if (n <= 1) n
+    else {
+      val r = limit3_2(n-1)
+      if (r >= 0) n + r
+      else r
+    }
+  }
+
+  @traceInduct("")
+  def check_limit3(n: BigInt): Unit = {
+  } ensuring(limit3_1(n) == limit3_2(n))
+
+}

frontends/benchmarks/equivalence/max.scala

@@ -0,0 +1,38 @@
+import stainless.annotation._
+import stainless.lang._
+import stainless.collection._
+import stainless.proof._ 
+
+object Max {
+
+  def maxR(lst: List[Int]): Int = {
+    lst match {
+      case Nil()           => -1
+      case Cons(hd, Nil()) => hd
+      case Cons(hd, tl)    => 
+        if (hd > maxR(tl)) hd 
+        else maxR(tl)
+    }
+  } 
+
+  def maxC(l: List[Int]): Int = {
+    l match {
+      case Nil()                => -1
+      case Cons(a, Nil())       => a
+      case Cons(a, Cons(b, tl)) => 
+        if (a > b) maxC(a :: tl) 
+        else maxC(b :: tl)
+    }
+  }
+
+  def maxT(lst: List[Int]): Int = {
+    def bigger(a: Int, b: Int) = 
+      if (a >= b) a else b
+    lst match {
+      case Nil()        => -1
+      case Cons(hd, tl) => 
+        tl.foldLeft(hd)(bigger)
+    }
+  }
+
+}

frontends/benchmarks/equivalence/pascal.scala

@@ -0,0 +1,30 @@
+// Examples are figures from paper:
+// Regression verification of unbalanced recursive functions with multiple calls (long version)
+// https://arxiv.org/pdf/2207.14364.pdf
+
+import stainless.collection._
+import stainless.lang._
+import stainless.annotation._
+
+object Pascal {
+
+  // Fig. 8
+  // RVT times out due to KLEE timing out when trying to prove the base-case
+
+  def p1(n: BigInt, m: BigInt): BigInt = {
+    if (m < 1 || n < 1 || m > n) 0
+    else if (m == 1 || n == 1 || m == n) 1
+    else p1(n-1, m-1) + p1(n-1, m)
+  }
+
+  def p2(n: BigInt, m: BigInt): BigInt = {
+    if (m < 1 || n < 1 || m > n) 0
+    else if (m == 1 || n == 1 || m == n) 1
+    else p2(n-1, m-1) + p2 (n-2 , m-1) + p2 (n-2 , m) 
+  }
+
+  @traceInduct("")
+  def check_p(n: BigInt, m: BigInt): Unit = {
+  } ensuring(p1(n, m) == p2(n, m))
+
+}