Remove some forAlls and simplify configuration. (#92)

* Remove some forAlls and simplify configuration.

* Fix config.

light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/blockchain/BlockchainSystem.scala

@@ -23,7 +23,8 @@ object BlockchainSystem {
       validatorSet.values.forall(_.votingPower.value == 1) &&
         maxPower.isPositive &&
         nextValidatorSet.keys.subsetOf(validatorSet.keys) &&
-        faultChecker.isCorrect(nextValidatorSet, ListSet.empty) && initialCommit.forBlock.isEmpty)
+        faultChecker.isCorrect(nextValidatorSet, ListSet.empty) &&
+        initialCommit.forBlock.isEmpty)
 
     val noFaulty = ListSet.empty[Address]
 

light-client-core/src/main/scala/utils/ListMap.scala

@@ -87,6 +87,7 @@ case class ListMap[A, B](toList: List[(A, B)]) {
 object ListMap {
   def empty[A, B]: ListMap[A, B] = ListMap(List.empty[(A, B)])
 
+  @library
   object lemmas {
 
     @opaque

light-client-core/src/main/scala/utils/ListSet.scala

@@ -34,24 +34,23 @@ case class ListSet[T](toList: List[T]) {
     ListUtils.restOfSetIsSubset(toList, other.toList)
     ListSet(toList -- other.toList)
   }.ensuring(res ⇒
-    forall((elem: T) ⇒ (this.contains(elem) && !other.contains(elem)) == res.contains(elem)) &&
-      (res & other).isEmpty &&
+    (res & other).isEmpty &&
       res.subsetOf(this))
 
   def &(other: ListSet[T]): ListSet[T] = {
     ListSetUtils.listSetIntersection(toList, other.toList)
     ListUtils.listIntersectionLemma(toList, other.toList)
     ListSet(toList & other.toList)
   }.ensuring(res ⇒
-    forall((elem: T) ⇒ (this.contains(elem) && other.contains(elem)) == res.contains(elem)) &&
-      res.subsetOf(this) &&
+    res.subsetOf(this) &&
       res.subsetOf(other))
 
+  @opaque
   def filter(predicate: T ⇒ Boolean): ListSet[T] = {
     ListSetUtils.filteringPreservesPredicate(toList, predicate)
     ListSetUtils.filteringMakesSubset(toList, predicate)
     ListSet(toList.filter(predicate))
-  }.ensuring(res ⇒ res.subsetOf(this))
+  }.ensuring(res ⇒ res.subsetOf(this) && res.toList.forall(predicate))
 
   def size: BigInt = toList.size
   def isEmpty: Boolean = toList.isEmpty
@@ -65,6 +64,7 @@ case class ListSet[T](toList: List[T]) {
 object ListSet {
   def empty[T]: ListSet[T] = ListSet(List.empty[T])
 
+  @library
   object lemmas {
 
     @opaque

light-client-core/src/main/scala/utils/ListUtils.scala

@@ -330,8 +330,7 @@ object ListUtils {
   }.ensuring { _ =>
     val intersection = first & second
     intersection.forall(first.contains) &&
-    intersection.forall(second.contains) &&
-    forall((elem: T) => intersection.contains(elem) == (first.contains(elem) && second.contains(elem)))
+    intersection.forall(second.contains)
   }
 
   @opaque

run.sh

@@ -1,6 +1,6 @@
 #!/bin/bash
 
-stainless-scalac  "$@" --batched --watch --solvers=smt-z3 \
+stainless-scalac  "$@" --watch \
   light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/integration/ModelIntegration.scala \
   light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/types/*.scala \
   light-client-core/src/main/scala/ch/epfl/ognjanovic/stevan/tendermint/verified/light/*.scala \

stainless.conf

@@ -1,12 +1,11 @@
 vc-cache = false
 timeout = 300
+solvers = [smt-z3]
 check-models = true
 print-ids = false
-//debug = [verification]
 batched = true
 no-colors = false
 fail-invalid = false
 infer-measures = true
 check-measures = true
-type-checker = true
-//functions = [setIntersectionLemma]
+type-checker = true