add iFM24 benchmarks (#1554)

Will the CI run these as tests? Merging in any case; they are great examples.

frontends/benchmarks/equivalence/adjlist/AdjList.scala

@@ -0,0 +1,41 @@
+/* Copyright 2009-2024 EPFL, Lausanne */
+
+import stainless.lang._
+import stainless.collection._
+
+object AdjList:
+
+  def validAdjListM(adjList: Array[List[Int]], N: Int, pos: Int): Boolean =
+    require(N >= 1 && pos >= 0 && pos <= N && N == adjList.length)
+    decreases(pos)
+    if pos == 0 then
+      true
+    else
+      validListM(adjList(pos - 1), N) && validAdjListM(adjList, N, pos - 1)
+
+  def validListM(list: List[Int], N: Int): Boolean =
+    require(N >= 1)
+    list match
+      case Nil() =>
+        true
+      case Cons(h, t) =>
+        h >= 0 && h < N && validListM(t, N)
+
+
+  def validAdjList(adjList: Array[List[Int]], N: Int, pos: Int): Boolean =
+    require(N >= 1 && pos >= 0 && pos <= N && N == adjList.length)
+    decreases(pos)
+    if (pos == 0) then
+      true
+    else if (validAdjList(adjList, N, pos - 1)) then
+      validList(N, adjList(pos - 1))
+    else
+      false
+
+  def validList(N: Int, l: List[Int]): Boolean =
+    require(N >= 1)
+    l match
+      case Cons(h, t) if (h >= 0 && h < N) =>
+        validList(N, t)
+      case _ =>
+        l.size == 0

frontends/benchmarks/equivalence/adjlist/test_conf.json

@@ -0,0 +1,23 @@
+{
+  "models": [
+    "AdjList.validAdjListM"
+  ],
+  "comparefuns": [
+    "AdjList.validAdjList"
+  ],
+  "outcome": {
+    "equivalent": [
+      {
+        "model": "AdjList.validAdjListM",
+        "functions": [
+          "AdjList.validAdjList"
+        ]
+      }
+    ],
+    "unequivalent": [],
+    "unsafe": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
+    "wrong": []
+  }
+}

frontends/benchmarks/equivalence/arrayContent/ArrayContent.scala

@@ -0,0 +1,20 @@
+/* Copyright 2009-2024 EPFL, Lausanne */
+
+import stainless.lang._
+
+object ArrayContent:
+
+  val MAX = 100000
+
+  def arrayContentM(a: Array[BigInt], n: Int) : Set[BigInt] =
+    require(n >= 0 && n <= a.length && a.length <= MAX)
+    decreases(n)
+    if n == 0 then Set.empty[BigInt]
+    else arrayContentM(a, n-1) ++ Set(a(n-1))
+
+
+  def arrayContent(a: Array[BigInt], n: Int) : Set[BigInt] =
+    require(n >= 0 && n <= a.length && a.length <= MAX)
+    decreases(n)
+    if n == 0 then Set.empty[BigInt]
+    else Set(a(n-1)) ++ arrayContent(a, n-1)

frontends/benchmarks/equivalence/arrayContent/test_conf.json

@@ -0,0 +1,23 @@
+{
+  "models": [
+    "ArrayContent.arrayContentM"
+  ],
+  "comparefuns": [
+    "ArrayContent.arrayContent"
+  ],
+  "outcome": {
+    "equivalent": [
+      {
+        "model": "ArrayContent.arrayContentM",
+        "functions": [
+          "ArrayContent.arrayContent"
+        ]
+      }
+    ],
+    "unequivalent": [],
+    "unsafe": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
+    "wrong": []
+  }
+}

frontends/benchmarks/equivalence/arrayHeap/ArrayHeap.scala

@@ -0,0 +1,71 @@
+/* Copyright 2009-2024 EPFL, Lausanne */
+
+import stainless.lang._
+
+object ArrayHeap:
+
+  val MAX = 100000
+
+  def childrenAreHeapsM(a: Array[Int], N: Int, i: Int): Boolean =
+    require(i >= 0 && i < N && N <= a.length && N <= MAX)
+    val l = leftM(i)
+    val r = rightM(i)
+    if (l < N && r < N) then
+      isHeapM(a, N, l) && isHeapM(a, N, r)
+    else if (l < N) then
+      isHeapM(a, N, l)
+    else
+      true
+
+  def isHeapM(a: Array[Int], N: Int, i: Int) : Boolean =
+    require(i >= 0 && i < N && N <= a.length && N <= MAX)
+    decreases(N - i)
+    val l = leftM(i)
+    val r = rightM(i)
+    val isHeapL = l < N && isHeapM(a, N, l)
+    val isHeapR = r < N && isHeapM(a, N, r)
+    if (l < N && a(l) > a(i)) then
+      false
+    else if (r < N && a(r) > a(i)) then
+      false
+    else if (r < i) then
+      isHeapL && isHeapR
+    else if (l < i) then
+      isHeapL
+    else
+      true
+
+
+  def leftM(i: Int) : Int =
+    require(0 <= i && i < MAX)
+    2 * i + 1
+
+  def rightM(i: Int) : Int =
+    require(0 <= i && i < MAX)
+    2 * i + 2
+
+
+  def childrenAreHeaps(a: Array[Int], N: Int, i: Int): Boolean =
+    require(i >= 0 && i < N && N <= a.length && N <= MAX)
+    if (2 * i + 1 < N && 2 * i + 2 < N) then
+      isHeap(a, N, 2 * i + 1) && isHeap(a, N, 2 * i + 2)
+    else if (2 * i + 1 < N) then
+      isHeap(a, N, 2 * i + 1)
+    else
+      true
+
+  def isHeap(a: Array[Int], N: Int, i: Int) : Boolean =
+    require(i >= 0 && i < N && N <= a.length && N <= MAX)
+    decreases(N - i)
+    val l = 2 * i + 1
+    val r = 2 * i + 2
+    if (2 * i + 1 < N && a(2 * i + 1) > a(i)) then
+      false
+    else if (2 * i + 2 < N && a(r) > a(i)) then
+      false
+    else if (2 * i + 2 < i) then
+      isHeap(a, N, 2 * i + 2) && isHeap(a, N, 2 * i + 1)
+    else if (2 * i + 1 < i) then
+      isHeap(a, N, 2 * i + 1)
+    else
+      true

frontends/benchmarks/equivalence/arrayHeap/test_conf.json

@@ -0,0 +1,23 @@
+{
+  "models": [
+    "ArrayHeap.childrenAreHeapsM"
+  ],
+  "comparefuns": [
+    "ArrayHeap.childrenAreHeaps"
+  ],
+  "outcome": {
+    "equivalent": [
+      {
+        "model": "ArrayHeap.childrenAreHeapsM",
+        "functions": [
+          "ArrayHeap.childrenAreHeaps"
+        ]
+      }
+    ],
+    "unequivalent": [],
+    "unsafe": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
+    "wrong": []
+  }
+}

frontends/benchmarks/equivalence/arrayIncreasing/ArrayIncreasing.scala

@@ -0,0 +1,23 @@
+/* Copyright 2009-2024 EPFL, Lausanne */
+
+import stainless.lang._
+
+object ArrayIncreasing:
+
+  def validLengthIncreasingM(a:Array[Array[Int]], N:Int, M:Int, k: Int): Boolean =
+    require(N > 0 && N == a.length && M > 0 && k >= 0 && k <= N)
+    decreases(N - k)
+    if (k == N) then
+      true
+    else
+      a(k).length == M && validLengthIncreasingM(a, N, M, succM(k))
+
+  def succM(n: Int) =
+    require(n < Int.MaxValue)
+    n + 1
+
+
+  def validLengthIncreasing(a:Array[Array[Int]], N:Int, M:Int, k: Int): Boolean =
+    require(N > 0 && N == a.length && M > 0 && k >= 0 && k <= N)
+    decreases(N - k)
+    (k == N) || a(k).length == M && validLengthIncreasing(a, N, M, k + 1)

frontends/benchmarks/equivalence/arrayIncreasing/test_conf.json

@@ -0,0 +1,23 @@
+{
+  "models": [
+    "ArrayIncreasing.validLengthIncreasingM"
+  ],
+  "comparefuns": [
+    "ArrayIncreasing.validLengthIncreasing"
+  ],
+  "outcome": {
+    "equivalent": [
+      {
+        "model": "ArrayIncreasing.validLengthIncreasingM",
+        "functions": [
+          "ArrayIncreasing.validLengthIncreasing"
+        ]
+      }
+    ],
+    "unequivalent": [],
+    "unsafe": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
+    "wrong": []
+  }
+}

frontends/benchmarks/equivalence/finiteStreams/FiniteStreams.scala

@@ -0,0 +1,36 @@
+/* Copyright 2009-2024 EPFL, Lausanne */
+
+import stainless._
+import lang._
+import annotation._
+
+object FiniteStream:
+
+  sealed abstract class Stream:
+    def rank = {
+      this match
+        case SCons(_, _, sz) if (sz > 0) => sz
+        case _                           => BigInt(0)
+    } ensuring(_ >= 0)
+  case class SCons(x: BigInt, tailFun: () => Stream, sz: BigInt) extends Stream
+  case class SNil() extends Stream
+
+  def finiteM(s: Stream): Boolean =
+    decreases(s.rank)
+    s match
+      case SCons(_, tfun, sz) if tfun().rank >= sz =>
+        false
+      case SCons(_, tfun, sz) =>
+        finiteM(tfun())
+      case _ =>
+        true
+
+
+  def finite(stream: Stream): Boolean =
+    decreases(stream.rank)
+    stream match
+      case SCons(_, tfun, sz) =>
+        val tail = tfun()
+        tail.rank < sz && finite(tail)
+      case SNil() =>
+        true

frontends/benchmarks/equivalence/finiteStreams/test_conf.json

@@ -0,0 +1,23 @@
+{
+  "models": [
+    "FiniteStream.finiteM"
+  ],
+  "comparefuns": [
+    "FiniteStream.finite"
+  ],
+  "outcome": {
+    "equivalent": [
+      {
+        "model": "FiniteStream.finiteM",
+        "functions": [
+          "FiniteStream.finite"
+        ]
+      }
+    ],
+    "unequivalent": [],
+    "unsafe": [],
+    "unknownSafety": [],
+    "unknownEquivalence": [],
+    "wrong": []
+  }
+}

frontends/benchmarks/equivalence/maxHeapify/MaxHeapify.scala

@@ -0,0 +1,62 @@
+/* Copyright 2009-2024 EPFL, Lausanne */
+
+import stainless.lang._
+
+object MayHeapify:
+
+  val MAX = 100000
+
+  def maxHeapifyM(a: Array[Int], N: Int, i: Int): Unit =
+    require(i >= 0 && i < N && N <= a.length && N <= MAX)
+    decreases(N - i)
+    val l = leftM(i)
+    val r = rightM(i)
+    val largest =
+      if l < N && a(l) > a(i) then
+        l
+      else
+        i
+    val largest2 =
+      if r < N && a(r) > a(largest) then
+        r
+      else
+        largest
+    if largest2 != i then
+        val temp = a(i)
+        a(i) = a(largest2)
+        a(largest2) = temp
+        maxHeapifyM(a, N, largest2)
+
+  def leftM(i: Int) : Int =
+    require(0 <= i && i < MAX)
+    2 * i + 1
+
+  def rightM(i: Int) : Int =
+    require(0 <= i && i < MAX)
+    2 * i + 2
+
+
+  def maxHeapify(a: Array[Int], N: Int, i: Int): Unit =
+    require(i >= 0 && i < N && N <= a.length && N <= MAX)
+    decreases(N - i)
+    val l = 2 * i + 1
+    val r = 2 * i + 2
+    val largest =
+      if l < N && a(l) > a(i) then
+        l
+      else
+        i
+    val largest2 =
+      if r < N && a(r) > a(largest) then
+        r
+      else
+        largest
+    if largest2 != i then
+      swap(i, largest2, a, N)
+      maxHeapify(a, N, largest2)
+
+  def swap(a: Int, b: Int, array: Array[Int], N: Int): Unit =
+    require(a >= 0 && a < N && b >= 0 && b < N && N <= array.length && N <= MAX)
+    val temp = array(a)
+    array(a) = array(b)
+    array(b) = temp