From 3ef64d07f1cc5cc090028e529af0488d9fc6fb51 Mon Sep 17 00:00:00 2001
From: Dragana <dragana.milovancevic@epfl.ch>
Date: Wed, 12 Oct 2022 20:43:47 +0200
Subject: [PATCH] Some examples of equivalence checking

---
 .../benchmarks/equivalence/addHorn.scala      | 29 ++++++++++++
 .../benchmarks/equivalence/factorial.scala    | 26 ++++++++++
 .../benchmarks/equivalence/fibonacci.scala    | 29 ++++++++++++
 .../equivalence/fullAlternation.scala         | 34 ++++++++++++++
 .../equivalence/halfAlternation.scala         | 29 ++++++++++++
 .../benchmarks/equivalence/inlining.scala     | 27 +++++++++++
 .../benchmarks/equivalence/isSorted.scala     | 47 +++++++++++++++++++
 frontends/benchmarks/equivalence/limit1.scala | 27 +++++++++++
 frontends/benchmarks/equivalence/limit2.scala | 25 ++++++++++
 frontends/benchmarks/equivalence/limit3.scala | 29 ++++++++++++
 frontends/benchmarks/equivalence/max.scala    | 38 +++++++++++++++
 frontends/benchmarks/equivalence/pascal.scala | 30 ++++++++++++
 frontends/benchmarks/equivalence/sum.scala    | 25 ++++++++++
 frontends/benchmarks/equivalence/uniq.scala   | 44 +++++++++++++++++
 .../benchmarks/equivalence/unrolling.scala    | 35 ++++++++++++++
 frontends/benchmarks/equivalence/unused.scala | 37 +++++++++++++++
 16 files changed, 511 insertions(+)
 create mode 100644 frontends/benchmarks/equivalence/addHorn.scala
 create mode 100644 frontends/benchmarks/equivalence/factorial.scala
 create mode 100644 frontends/benchmarks/equivalence/fibonacci.scala
 create mode 100644 frontends/benchmarks/equivalence/fullAlternation.scala
 create mode 100644 frontends/benchmarks/equivalence/halfAlternation.scala
 create mode 100644 frontends/benchmarks/equivalence/inlining.scala
 create mode 100644 frontends/benchmarks/equivalence/isSorted.scala
 create mode 100644 frontends/benchmarks/equivalence/limit1.scala
 create mode 100644 frontends/benchmarks/equivalence/limit2.scala
 create mode 100644 frontends/benchmarks/equivalence/limit3.scala
 create mode 100644 frontends/benchmarks/equivalence/max.scala
 create mode 100644 frontends/benchmarks/equivalence/pascal.scala
 create mode 100644 frontends/benchmarks/equivalence/sum.scala
 create mode 100644 frontends/benchmarks/equivalence/uniq.scala
 create mode 100644 frontends/benchmarks/equivalence/unrolling.scala
 create mode 100644 frontends/benchmarks/equivalence/unused.scala

diff --git a/frontends/benchmarks/equivalence/addHorn.scala b/frontends/benchmarks/equivalence/addHorn.scala
new file mode 100644
index 0000000000..a5374ee5ce
--- /dev/null
+++ b/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))
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/factorial.scala b/frontends/benchmarks/equivalence/factorial.scala
new file mode 100644
index 0000000000..10f6632247
--- /dev/null
+++ b/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))
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/fibonacci.scala b/frontends/benchmarks/equivalence/fibonacci.scala
new file mode 100644
index 0000000000..c8067f2169
--- /dev/null
+++ b/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))
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/fullAlternation.scala b/frontends/benchmarks/equivalence/fullAlternation.scala
new file mode 100644
index 0000000000..28e5574e60
--- /dev/null
+++ b/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))
+   
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/halfAlternation.scala b/frontends/benchmarks/equivalence/halfAlternation.scala
new file mode 100644
index 0000000000..778b3965e8
--- /dev/null
+++ b/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))
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/inlining.scala b/frontends/benchmarks/equivalence/inlining.scala
new file mode 100644
index 0000000000..b3523d3568
--- /dev/null
+++ b/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))
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/isSorted.scala b/frontends/benchmarks/equivalence/isSorted.scala
new file mode 100644
index 0000000000..d8811d013d
--- /dev/null
+++ b/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)
+  }
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/limit1.scala b/frontends/benchmarks/equivalence/limit1.scala
new file mode 100644
index 0000000000..4864276ae5
--- /dev/null
+++ b/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))
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/limit2.scala b/frontends/benchmarks/equivalence/limit2.scala
new file mode 100644
index 0000000000..d0059add92
--- /dev/null
+++ b/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))
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/limit3.scala b/frontends/benchmarks/equivalence/limit3.scala
new file mode 100644
index 0000000000..aa8df17eff
--- /dev/null
+++ b/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))
+  
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/max.scala b/frontends/benchmarks/equivalence/max.scala
new file mode 100644
index 0000000000..8d44374969
--- /dev/null
+++ b/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)
+    }
+  }
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/pascal.scala b/frontends/benchmarks/equivalence/pascal.scala
new file mode 100644
index 0000000000..e5f0a980f0
--- /dev/null
+++ b/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))
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/sum.scala b/frontends/benchmarks/equivalence/sum.scala
new file mode 100644
index 0000000000..8cc315001c
--- /dev/null
+++ b/frontends/benchmarks/equivalence/sum.scala
@@ -0,0 +1,25 @@
+// 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 Sum {
+
+  // Fig. 5 - two functions are not in lock-step
+
+  def sum1(n: BigInt): BigInt = 
+    if (n <= 1) n
+    else n + n-1 + sum1(n-2)
+
+  def sum2(n: BigInt): BigInt = 
+    if (n <= 1) n
+    else n + sum2(n-1)
+
+  @traceInduct("")
+  def check_sum(n: BigInt): Unit = {
+  } ensuring(sum1(n) == sum2(n))
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/uniq.scala b/frontends/benchmarks/equivalence/uniq.scala
new file mode 100644
index 0000000000..e2f4aaed1c
--- /dev/null
+++ b/frontends/benchmarks/equivalence/uniq.scala
@@ -0,0 +1,44 @@
+import stainless.annotation._
+import stainless.lang._
+import stainless.collection._
+import stainless.proof._ 
+
+object Uniq {
+
+  def uniqR(lst: List[Int]): List[Int] = {
+
+    def find(lst: List[Int], n: Int): Boolean = lst match {
+      case Nil()        => false
+      case Cons(hd, tl) => (n == hd) || find(tl, n)
+    }
+
+    def unique(l: List[Int], r: List[Int]): List[Int] =
+      l match {
+        case Nil() => r
+        case Cons(hd, tl) =>
+          if (!find(r, hd)) unique(tl, r ++ List(hd))
+          else unique(tl, r)
+      }
+
+    unique(lst, Nil())
+
+  }
+
+  def uniqA(lst: List[Int]): List[Int] = {
+
+    def isin(lst: List[Int], a: Int): Boolean = 
+    lst.foldRight(false){ (e, acc) => (e == a || acc) }
+
+    def distinct(a: List[Int], b: List[Int]): List[Int] =
+      a match {
+        case Nil() => b
+        case Cons(hd, tl) =>
+          if (isin(b, hd)) distinct(tl, b)
+          else distinct(tl, b ++ List[Int](hd))
+      }
+
+    distinct(lst, List())
+
+  }
+
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/unrolling.scala b/frontends/benchmarks/equivalence/unrolling.scala
new file mode 100644
index 0000000000..0f7a1e069a
--- /dev/null
+++ b/frontends/benchmarks/equivalence/unrolling.scala
@@ -0,0 +1,35 @@
+// 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 Unrolling {
+
+  // Fig. 13
+
+  def fact13_1(n: BigInt): BigInt =
+    if (n <= 1) 1 
+    else if (n == 2) 2
+    else if (n == 3) 6
+    else if (n == 4) 24
+    else n * (n-1) * (n-2) * (n-3) * fact13_1(n-4)
+
+  def fact13_2(n: BigInt): BigInt =
+    if (n <= 1) 1 
+    else if (n == 2) 2
+    else if (n == 3) 6
+    else if (n == 4) 24
+    else if (n == 5) 120
+    else if (n == 6) 720
+    else if (n == 7) 5040
+    else if (n == 8) 40320
+    else n * (n-1) * (n-2) * (n-3) * fact13_2(n-4)
+
+  @traceInduct("")
+  def check_fact13(n: BigInt): Unit = {
+  } ensuring(fact13_1(n) == fact13_2(n))
+  
+}
\ No newline at end of file
diff --git a/frontends/benchmarks/equivalence/unused.scala b/frontends/benchmarks/equivalence/unused.scala
new file mode 100644
index 0000000000..89f36078c0
--- /dev/null
+++ b/frontends/benchmarks/equivalence/unused.scala
@@ -0,0 +1,37 @@
+// 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 FibonacciUnused {
+
+  // Fig. 13
+
+  def t1(n: BigInt): BigInt = {
+    if (n < 1) 0
+    else if (n == 1) 1
+    else t1(n - 1) + t1(n - 2)
+  }
+
+  def t2(n: BigInt): BigInt = {
+    if (n < 1) 0
+    else if (n == 1 || n == 2) 1
+    else {
+      var results: BigInt = 0
+      var r1 = t2(n-1)
+      var r2 = t2(n-2)
+      var r3 = t2(n-3)
+      if (n % 2 == 0) results = r2 + r2 + r3
+      else results = r1 + r2
+      results 
+    }
+  }
+
+  @traceInduct("")
+  def check_t(n: BigInt): Unit = {
+  } ensuring(t1(n) == t2(n))
+
+}
\ No newline at end of file