Use inlineOnce instead of inline for opaque functions (#55)

epfl-lara · Nov 15, 2022 · 7e487c5 · 7e487c5
1 parent 3f4df34
commit 7e487c5
Show file tree

Hide file tree

Showing 6 changed files with 17 additions and 8 deletions.
diff --git a/WIP/SLOW/longmap/StrictlyOrderedLongListMap.scala b/WIP/SLOW/longmap/StrictlyOrderedLongListMap.scala
@@ -398,6 +398,7 @@ object TupleListOps {
 
   @opaque
   def lemmaAddExistingKeyPreservesSize[B](l: List[(Long, B)], key: Long, value: B): Unit = {
+    decreases(l)
     require(invariantList(l))
     require(containsKey(l, key))
 
@@ -679,7 +680,7 @@ object ListMapLongKeyLemmas {
   }.ensuring(_ => (lm + (a -> b))(a0) == lm(a0))
 
   @opaque
-  @inline
+  @inlineOnce
   def addStillContains[B](lm: ListMapLongKey[B], a: Long, b: B, a0: Long): Unit = {
     require(lm.contains(a0))
 

diff --git a/WIP/SLOW/longmap/stainless.conf b/WIP/SLOW/longmap/stainless.conf
@@ -3,7 +3,7 @@
 # options listed by `stainless --help`
 
 vc-cache            = true
-debug               = [] #["verification"]
+#debug               = ["verification"]
 timeout             = 20
 check-models        = false
 print-ids           = false
@@ -15,4 +15,5 @@ strict-arithmetic   = false
 # solvers             = "smt-z3,no-inc:smt-z3:z3-master tactic.default_tactic=smt sat.euf=true"
 solvers             = "smt-cvc4,smt-z3,no-inc:smt-z3:z3 tactic.default_tactic=smt sat.euf=true"
 check-measures      = yes
-infer-measures      = true
+infer-measures      = false
+no-colors           = true
diff --git a/data-structures/sorted-array/SortedArray.scala b/data-structures/sorted-array/SortedArray.scala
@@ -123,7 +123,7 @@ object SortedArray {
     isSortedRange(array, order, i2, j2)
   )
 
-  @pure @opaque @ghostAnnot @inline
+  @pure @opaque @ghostAnnot @inlineOnce
   def arrayGetSameIndex2[@mutable T](array: Array[T], i: Int, j: Int): Unit = {
     require(0 <= i && i < array.length - 1 && i == j)
 

diff --git a/qoi/stainless.conf b/qoi/stainless.conf
@@ -3,4 +3,5 @@ timeout = 300
 strict-arithmetic = false
 batched = true
 solvers = "smt-cvc4,smt-z3,no-inc:smt-z3:z3 tactic.default_tactic=smt sat.euf=true"
-infer-measures = false
+infer-measures = false
+no-colors = true
diff --git a/qoi/verified/common.scala b/qoi/verified/common.scala
@@ -377,7 +377,7 @@ object common {
   @opaque
   @inlineOnce
   def arraysEqAtIndex[T](arr1: Array[T], arr2: Array[T], from: Long, until: Long, at: Long): Unit = {
-    decreases(until - at)
+    decreases(until - from)
     require(arr1.length == arr2.length)
     require(0 <= from && from <= until && until <= arr1.length)
     require(arraysEq(arr1, arr2, from, until))

diff --git a/qoi/verified/encoder.scala b/qoi/verified/encoder.scala
@@ -678,6 +678,7 @@ object encoder {
         assert(decoded1.pxPos + chan <= decoded1.pixels.length)
         assert(outPos1 < outPos2 && outPos2 <= bytes.length - Padding)
         assert(pixels.length == w * h * chan)
+        assert(pxPos % chan == 0)
         assert(decoder.pxPosInv(decoded1.pxPos))
         val (ix2, pix2, decIter2) = decoder.decodeLoopPure(decoded1.index, decoded1.pixels, decIter1.px, outPos1, outPos2, decoded1.pxPos)
         assert(decIter2.pxPos == decoded2.pxPos)
@@ -782,11 +783,16 @@ object encoder {
       assert(pxPosInv(pxPos))
       unfold(pxPosInv(pxPos))
       check(pxPos % chan == 0)
-      check(pixels.length % chan == 0) // Slow (~75)
+
+      modMultLemma(w, h, chan)
+      assert((w * h * chan) % chan == 0)
+      assert(pixels.length == w * h * chan)
+      check(pixels.length % chan == 0)
+
       check(samePixels(pixels, px, pxPos, chan))
       check(arraysEq(bytesPre, bytes, 0, outPos0))
       check(rangesInv(index.length, bytes.length, run1, outPos2, pxPos))
-      check(positionsIneqInv(run1, outPos2, pxPos + chan)) // Slow (~45s)
+      check(positionsIneqInv(run1, outPos2, pxPos + chan))
       check(pxPosInv(decoded.pxPos))
       check(newDecoded.pxPos + chan * run1 == pxPos + chan)
       check((outPos0 == outPos2) ==> (decoded == newDecoded && run1 == run0 + 1 && px == pxPrev))