Change to pre, post condition instead of invariant, private val for t…

…he cache (#98)

* Add cached function to bolts

* change spec to be pre and post condition, and private cache

* opaque valid function, using unfold

---------

Co-authored-by: Viktor Kunčak <vkuncak@users.noreply.github.com>

caching/CachedFunction.scala

@@ -11,14 +11,16 @@ object CachedFunction {
     CachedFunction(f, hashable, MutableHashMap.getEmptyHashMap[I, O](f, hashable))
   }
 
+  @pure @ghost def isImageOf[I, O](f: I => O): ((I, O)) => Boolean = (t) => t._2 == f(t._1) // If we use a lambda, it is rejected for illegal capture of thiss
+
   @ghost
   @inline
   def allValuesAreFunctionOutputs[I, O](
       f: I => O,
       cache: MutableHashMap.HashMap[I, O]
   ): Boolean = {
     require(cache.valid)
-    cache.map.forall((k, v) => v == f(k))
+    cache.map.forall(isImageOf[I, O](f))
   }
 
   @ghost
@@ -41,7 +43,7 @@ object CachedFunction {
         y
       )
       assert(cache.map.toList.contains((x, cache(x))))
-      ListSpecs.forallContained(cache.map.toList, (k, v) => v == f(k), (x, y))
+      ListSpecs.forallContained(cache.map.toList, isImageOf[I, O](f), (x, y))
   }.ensuring (_ => if (cache.contains(x)) then cache(x) == f(x) else true)
 
 }
@@ -51,26 +53,30 @@ final case class CachedFunction[I, O](
     hashable: Hashable[I],
     private val cache: MutableHashMap.HashMap[I, O]
 ) {
-
-  @ghost @opaque
-  def valid: Boolean =
-    cache.valid &&
-    CachedFunction.allValuesAreFunctionOutputs(f, cache)
+  @pure
+  @ghost
+  @opaque
+  def valid: Boolean = cache.valid && CachedFunction.allValuesAreFunctionOutputs(f, cache)
 
   @opaque
   def apply(x: I): O = {
-    require(valid)
-    ghostExpr(unfold(valid))
+    require(this.valid)
+    ghostExpr(unfold(this.valid))
     if cache.contains(x) then
       ghostExpr(CachedFunction.lemmaInMapThenCorrect(f, cache, x, cache(x)))
       cache(x)
     else
       val result = f(x)
+      @ghost val thiss = snapshot(this)
+      ghostExpr(MutableHashMap.lemmaUpdatePreservesForallPairs(cache, x, result, CachedFunction.isImageOf[I, O](f)))
       cache.update(x, result)
       assert(cache.valid)
       assert(CachedFunction.allValuesAreFunctionOutputs(f, cache), "cached value is still function output")
       result
-  }.ensuring { res => res == f(x) && {unfold(valid);valid} }
+  }.ensuring { res =>
+    unfold(this.valid)
+    res == f(x) && this.valid 
+  }
 }
 
 // object IntHashable extends Hashable[Int] {

caching/stainless.conf

@@ -8,7 +8,7 @@ check-models        = false
 print-ids           = false
 print-types         = false
 batched             = true
-strict-arithmetic   = true
+strict-arithmetic   = false
 solvers             = "smt-cvc5,smt-z3,smt-cvc4"
 check-measures      = yes
 infer-measures      = true