Merge branch 'main' into sam/minitrait

epfl-lara · Dec 12, 2024 · e511ba9 · e511ba9
2 parents 4d8b7cb + 997f69f
commit e511ba9
Show file tree

Hide file tree

Showing 157 changed files with 3,071 additions and 884 deletions.
diff --git a/.github/workflows/bolts-CI.yml b/.github/workflows/bolts-CI.yml
@@ -0,0 +1,50 @@
+name: Bolts CI
+on:
+  pull_request:
+  push:
+    branches:
+      - main
+jobs:
+  tests:
+    if: github.event.pull_request.draft == false
+    runs-on: [self-hosted, linux]
+    env:
+      # define Java options for both official sbt and sbt-extras
+      JAVA_OPTS: -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M 
+      JVM_OPTS:  -Dsbt.io.implicit.relative.glob.conversion=allow -Xss512M -Xms1024M -Xmx12G -XX:MaxMetaspaceSize=2G -XX:+UseCodeCacheFlushing -XX:ReservedCodeCacheSize=768M 
+      JAVA_OPTS_TMP_DIR: /tmp/tmp_${{ github.run_id }}_${{ github.run_attempt }}
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+      with:
+        submodules: recursive
+    - name: Setup JDK
+      uses: actions/setup-java@v4
+      with:
+        distribution: temurin
+        java-version: 17
+    - name: Setup java options
+      run: |
+          echo "JAVA_OPTS=$JAVA_OPTS -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV" && \
+          echo "JVM_OPTS=$JVM_OPTS -Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV" && \
+          echo "SBT_OPTS=-Djava.io.tmpdir=$JAVA_OPTS_TMP_DIR --sbt-dir $JAVA_OPTS_TMP_DIR" >> "$GITHUB_ENV"
+    - name: Creating temp folder
+      run: rm -rf $JAVA_OPTS_TMP_DIR && mkdir -p $JAVA_OPTS_TMP_DIR && chmod 777 $JAVA_OPTS_TMP_DIR
+    - name: Install stainless and solvers
+      run: ./install_stainless_and_solvers.sh $GITHUB_WORKSPACE/.local/bin $GITHUB_WORKSPACE/.local && echo "PATH=$GITHUB_WORKSPACE/.local/bin:$PATH" >> "$GITHUB_ENV"
+    - name: Add stainless to PATH
+      run: echo "$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin" >> $GITHUB_PATH && echo "PATH=$GITHUB_WORKSPACE/.local/stainless/frontends/dotty/target/universal/stage/bin:$PATH" >> "$GITHUB_ENV"
+    - name: Test stainless availability
+      run: stainless-dotty --version
+    - name: Add solvers to PATH
+      run: echo "$GITHUB_WORKSPACE/.local/bin" >> $GITHUB_PATH
+    - name: Test solvers availability
+      run: cvc5 --version && z3 --version && cvc4 --version
+    - name: Bolts Tests
+      run: ./run-tests.sh --admit-vcs
+  fail_if_pull_request_is_draft:
+    if: github.event.pull_request.draft == true
+    runs-on: [self-hosted, linux]
+    steps:
+    - name: Fails in order to indicate that pull request needs to be marked as ready to review and tests workflows need to pass.
+      run: exit 1
diff --git a/README.md b/README.md
@@ -1,3 +1,5 @@
+[![Build Status](https://github.com/epfl-lara/bolts/actions/workflows/bolts-CI.yml/badge.svg?branch=main)](https://github.com/epfl-lara/bolts/actions/workflows/bolts-CI.yml/?branch=main)
+
 # Bolts: Stainless Verified Scala
 
 This repository showcases examples of code verified using

diff --git a/WIP/Huffman-looping.scala b/WIP/Huffman-looping.scala
@@ -28,7 +28,7 @@ object Huffman {
           case Fork(left, right) => left.chars ++ right.chars
           case Leaf(char, weight) => Set(char)
         }
-      } ensuring(res => res != Set.empty[Char])
+      }.ensuring(res => res != Set.empty[Char])
     }
     case class Fork(left: CodeTree, right: CodeTree) extends CodeTree
     case class Leaf(char: Char, weight: BigInt) extends CodeTree

diff --git a/WIP/LambdaEvaluator/ExplicitSubstitution.scala b/WIP/LambdaEvaluator/ExplicitSubstitution.scala
@@ -55,8 +55,8 @@ object ExplicitSubstitution {
         require(size >= 0 && size == s.size && s.unique == s)
         decreases(size)
         if (size == 0) n else
-        if (s contains n) newVar(s - n, n + 1, size - 1) else n
-    } ensuring{ res => !(s contains res) }
+        if (s.contains(n)) newVar(s - n, n + 1, size - 1) else n
+    }.ensuring( res => !(s.contains(res)) )
 
 
     //propagates a substitution down
@@ -69,7 +69,7 @@ object ExplicitSubstitution {
             case App(f, arg) => App(eval(ApplySubst(f, e.s)), eval(ApplySubst(arg, e.s)))
             case Abs(x, body) =>
                 if (x != e.s.x) {
-                    if (fv(e.s.m) contains x) {
+                    if (fv(e.s.m).contains(x)) {
                         val set = (fv(e.s.m) ++ fv(body)).unique
                         val newX = newVar(set, x + 1, set.size)
                         Abs(newX, ApplySubst(ApplySubst(body, Subst(x, Var(newX))), e.s))
@@ -107,10 +107,10 @@ object ExplicitSubstitution {
             case _ => Some(t)
         }
 
-    } ensuring { res => (res match {
+    }.ensuring( res => (res match {
         case Some(r) => isValue(r)
         case None() => true
-    })}
+    }))
 
 
     //evaluates, but also find all the beta reduction to be made
@@ -148,10 +148,10 @@ object ExplicitSubstitution {
             case _ => Some(t)
         }
 
-    } ensuring { res => (res match {
+    }.ensuring( res => (res match {
         case Some(r) => isReduced(r) && noSubst(r)
         case None() => true
-    })}
+    }))
 
 
     //checks if two terms are alpha equivalent (that is, equal upon renaming of the bound variables)
@@ -168,7 +168,7 @@ object ExplicitSubstitution {
                 case _ => false
             }
             case Abs(x, body) => t2 match {
-                case Abs(x2, body2) => if (x == x2) alphaEquivalent(body, body2) else !(fv(body2) contains x) && alphaEquivalent(body, eval(ApplySubst(body2, Subst(x2, Var(x)))))
+                case Abs(x2, body2) => if (x == x2) alphaEquivalent(body, body2) else !(fv(body2).contains(x)) && alphaEquivalent(body, eval(ApplySubst(body2, Subst(x2, Var(x)))))
                 case _ => false
             }
             case _ => false
@@ -179,64 +179,64 @@ object ExplicitSubstitution {
         require(noSubst(t))
 
         alphaEquivalent(t, t)
-    } holds
+    }.holds
 
 
     def unique(t1: Term, t2: Term, s: Subst, n: BigInt) = {
         require(n > 0 && t1 == t2)
 
         loopingEval(ApplySubst(t1, s), n) == loopingEval(ApplySubst(t2, s), n)
-    } holds
+    }.holds
 
     def unique2(t1: Term, t2: Term, s1: Term, s2: Term, n: BigInt, x: BigInt) = {
         require(n > 0 && t1 == t2 && s1 == s2)
 
         loopingEval(ApplySubst(t1, Subst(x, s1)), n) == loopingEval(ApplySubst(t2, Subst(x, s2)), n)
-    } holds
+    }.holds
 
     def substitutionLemma(t: Term, s1: Subst, s2: Subst) = {
-        require(noSubst(t) && noSubst(s1.m) && noSubst(s2.m) && !((fv(s2.m) ++ fv(t)) contains s1.x) && s1.x != s2.x)
+        require(noSubst(t) && noSubst(s1.m) && noSubst(s2.m) && !((fv(s2.m) ++ fv(t)).contains(s1.x)) && s1.x != s2.x)
 
         eval(ApplySubst(eval(ApplySubst(t, s1)), s2)) == eval(ApplySubst(eval(ApplySubst(t, s2)), Subst(s1.x, eval(ApplySubst(s1.m, s2)))))
-    } holds
+    }.holds
 
     //λx.x((λy.yy)x)x = λx.x(xx)x
     def example1 = {
         loopingStrongEval(Abs(0, App(App(Var(0), App(Abs(1, App(Var(1), Var(1))), Var(0))), Var(0))), 20) match {
             case Some(t) => t == Abs(0, App(App(Var(0), App(Var(0), Var(0))), Var(0)))
             case _ => false
         }
-    } holds
+    }.holds
 
     //(λxyz.zyx)aa(λpq.q) = a
     def example2 = {
         loopingEval(App(App(App(Abs(0, Abs(1, Abs(2, App(App(Var(2), Var(1)), Var(0))))), Var(5)), Var(5)), Abs(3, Abs(4, Var(3)))), 20) match {
             case Some(t) => t == Var(5)
             case _ => false
         }
-    } holds
+    }.holds
 
     //λx.y [y:x] = λz.x
     def captureAvoidingTest = {
        loopingStrongEval(ApplySubst(Abs(0, Var(1)), Subst(1, Var(0))), 50) match {
             case Some(t) => alphaEquivalent(t, Abs(1, Var(0)))
             case _ => false
        }
-    } holds
+    }.holds
 
 
 //=================================================
 
     def powerN(f: Term, M: Term, n: BigInt): Term = {
         require(n >= 0 && noSubst(f) && noSubst(M))
         if (n == 0) M else App(f, powerN(f, M, n - 1))
-    } ensuring{ res => noSubst(res) }
+    }.ensuring(res => noSubst(res) )
 
     //encoding of integers using the church technic
     def churchN(n: BigInt) = {
         require(n >= 0)
         Abs(0, Abs(5, powerN(Var(0), Var(5), n)))
-    } ensuring { res => noSubst(res) }
+    }.ensuring( res => noSubst(res) )
 
 
     val Aplus = Abs(0, Abs(1, Abs(2, Abs(3, App(App(Var(0), Var(2)), App(App(Var(1), Var(2)), Var(3)))))))
@@ -247,14 +247,14 @@ object ExplicitSubstitution {
             case Some(t) => alphaEquivalent(t, churchN(7))
             case _ => false
         }
-    } holds
+    }.holds
 
     def testMult = {
         loopingStrongEval(App(App(Astar, churchN(2)), churchN(3)), 80) match {
             case Some(t) => t == churchN(6)
             case _ => false
         }
-    } holds
+    }.holds
 
 
 //=================================================
@@ -276,38 +276,38 @@ object ExplicitSubstitution {
             case Some(t) => t == Var(10)
             case _ => false
         }
-    } holds
+    }.holds
 
     //False x y = y
     def falseTest = {
         loopingEval(App(App(False, Var(10)), Var(11)), 20) match {
             case Some(t) => t == Var(11)
             case _ => false
         }
-    } holds
+    }.holds
 
     //Cons(x, y) z (λp. p._1) = x
     def listTest = {
         loopingEval(App(App(Cons(Var(10), Var(11)), Var(12)), True), 20) match {
             case Some(t) => t == Var(10)
             case _ => false
         }
-    } holds
+    }.holds
 
     //Pair(x, y)._1 = x
     def testPair1 = {
         loopingEval(_1(Pair(Var(30), Var(31))), 20) match {
             case Some(t) => t == Var(30)
             case _ => false
         }
-    } holds
+    }.holds
 
     //Pair(x, y)._2 = y
     def testPair2 = {
         loopingEval(_2(Pair(Var(30), Var(31))), 20) match {
             case Some(t) => t == Var(31)
             case _ => false
         }
-    } holds
+    }.holds
 
 }