Add the verified lexer, including all optimizations, example lexers and JSON example

data-structures/maps/mutablemaps/src/main/scala/benchmark/HashMapBenchmark.scala

@@ -5,15 +5,15 @@ import org.openjdk.jmh.annotations.*
 import scala.collection.mutable.LongMap
 import scala.collection.mutable.HashMap
 import scala.util.Random
-import ch.epfl.map.MutableLongMap
+import com.mutablemaps.map.MutableLongMap
 import stainless.collection.{List => StainlessList}
 import scala.collection.immutable
-import ch.epfl.map.EfficientFill
-import ch.epfl.map.MutableHashMap
-import ch.epfl.map.MutableLongMap
-import ch.epfl.map.Hashable
-import ch.epfl.map.ListMap
-import ch.epfl.map.Ordering
+import com.mutablemaps.map.EfficientFill
+import com.mutablemaps.map.MutableHashMap
+import com.mutablemaps.map.MutableLongMap
+import com.mutablemaps.map.Hashable
+import com.mutablemaps.map.ListMap
+import com.mutablemaps.map.Ordering
 
 
 @State(Scope.Benchmark)
@@ -282,7 +282,7 @@ object HashMapBenchmarkUtilBig {
     mutableMap
   }
 
-  val verifiedHashMapFilledWith2to22Values = {
+  val verifiedHashMapFilledWith2to22Values: MutableHashMap.HashMap[Key, Long] = {
     val mutableMap: MutableHashMap.HashMap[Key, Long] = getVerifiedHashMapEmptyBuffer(16)
     for (k, v) <- random2to22Pairs do mutableMap.update(k, v)
     end for

data-structures/maps/mutablemaps/src/main/scala/benchmark/VerifiedMapBenchmark.scala

@@ -5,14 +5,14 @@ import org.openjdk.jmh.annotations.*
 import scala.collection.mutable.LongMap
 import scala.collection.mutable.HashMap
 import scala.util.Random
-import ch.epfl.map.MutableLongMap
-import ch.epfl.map.MutableLongMapOpti
-import ch.epfl.map.ListLongMap
+import com.mutablemaps.map.MutableLongMap
+import com.mutablemaps.map.MutableLongMapOpti
+import com.mutablemaps.map.ListLongMap
 import stainless.collection.{List => StainlessList}
 import scala.collection.immutable
-import ch.epfl.map.MutableLongMapOpti.LongMapOpti
+import com.mutablemaps.map.MutableLongMapOpti.LongMapOpti
 import benchmark.BenchmarkUtil.getHashMapEmptyBuffer
-import ch.epfl.map.EfficientFill
+import com.mutablemaps.map.EfficientFill
 
 @State(Scope.Benchmark)
 class ArrayFillBenchmark {

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/EfficientFill.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/EfficientFill.scala

@@ -1,7 +1,7 @@
 /** This file contains implementations of a "fill" function for Array, used as benchmark.
   */
 
-package ch.epfl.map
+package com.mutablemaps.map
 
 import MutableLongMap.*
 

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap-onlyCode.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/ListLongMap-onlyCode.scala

@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot Contains only the code of the ListLongMap, without specification nor proof, for line counting purposes.
   */
 
-package ch.epfl.map
+package com.mutablemaps.map
 
 import stainless.annotation._
 import stainless.collection._

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/ListLongMap.scala

@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.map
+package com.mutablemaps.map
 
 import stainless.annotation._
 import stainless.collection._

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/ListMap.scala

@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.map
+package com.mutablemaps.map
 
 import stainless.annotation._
 import stainless.collection._

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/Main.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/Main.scala

@@ -1,26 +1,28 @@
-package ch.epfl.map
+package com.mutablemaps.map
 
-import ch.epfl.map.MutableLongMap
-import ch.epfl.map.ListLongMap
+import com.mutablemaps.map.MutableLongMap
+import com.mutablemaps.map.ListLongMap
 import stainless.collection.List
 import benchmark.BenchmarkUtil.*
 import benchmark.Key
-import ch.epfl.map.MutableHashMap.*
-import ch.epfl.map.MutableLongMap.ValueCellFull
-import ch.epfl.map.MutableLongMap.EmptyCell
+import com.mutablemaps.map.MutableHashMap.*
+import com.mutablemaps.map.MutableLongMap.ValueCellFull
+import com.mutablemaps.map.MutableLongMap.EmptyCell
 import scala.collection.mutable.HashMap
+import stainless.lang.Cell
+import com.mutablemaps.map.MutableLongMap.ValueCell
 object Main {
   def main(args: Array[String]): Unit = {
     // check the number of collisions of each levels:
 
-    val mapFilled = benchmark.HashMapBenchmarkUtilBig.verifiedHashMapFilledWith2to22Values
+    val mapFilled: MutableHashMap.HashMap[Key, Long] = benchmark.HashMapBenchmarkUtilBig.verifiedHashMapFilledWith2to22Values
     println(f"mapFilled.size = ${mapFilled.size}")
     var bucketSizes: HashMap[BigInt, Int] = HashMap()
     var i = 0
     while (i < mapFilled.underlying.v.underlying.v.mask + 1) {
-      val key = mapFilled.underlying.v.underlying.v._keys(i)
+      val key: Long = mapFilled.underlying.v.underlying.v._keys(i)
       if(key != 0 && key != Long.MinValue) {
-        val value = mapFilled.underlying.v.underlying.v._values(i)
+        val value: ValueCell[List[(Key, Long)]] = mapFilled.underlying.v.underlying.v._values(i)
         println(value)
         value match
           case ValueCellFull(v) => bucketSizes(v.size) = bucketSizes.getOrElse(v.size, 0) + 1

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/MutableHashMap.scala

@@ -1,19 +1,31 @@
 /** Author: Samuel Chassot
   */
-package ch.epfl.map
+package com.mutablemaps.map
 
 import stainless.annotation._
 import stainless.collection.{ListMap => ListMapStainless, ListMapLemmas => ListMapLemmasStainless, _}
 import stainless.equations._
-import stainless.lang.{ghost => ghostExpr, _}
-import stainless.proof.check
-import scala.annotation.tailrec
 import stainless.lang.Cell
 import MutableLongMap._
 import LongMapFixedSize.validMask
+import scala.annotation.tailrec
 
-import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
-// import OptimisedChecks.* // Import to remove `ensuring` and `require` from the code for the benchmarks
+// BEGIN uncomment for verification ------------------------------------------
+import stainless.lang.StaticChecks._
+import stainless.lang.{ghost => ghostExpr, _}
+import stainless.proof.check
+// END uncomment for verification --------------------------------------------
+// BEGIN imports for benchmarking -------------------------------------------
+// import stainless.lang.{ghost => _, decreases => _, unfold => _, _}
+// import com.mutablemaps.map.OptimisedChecks.*
+// import Predef.{assert => _, Ensuring => _, require => _}
+
+// @tailrec
+// def dummyMutableHashMap(x: BigInt): BigInt = {
+//   if (x == BigInt(0)) then x
+//   else dummyMutableHashMap(x - BigInt(1))
+// }.ensuring( res => res == BigInt(0))
+// END imports for benchmarking ---------------------------------------------
 
 import MutableMapInterface.MutableMap
 

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/MutableLongMap.scala

@@ -1,20 +1,32 @@
 /** Author: Samuel Chassot
   */
-package ch.epfl.map
+package com.mutablemaps.map
 
 import stainless.annotation._
 import stainless.collection._
 import stainless.equations._
-import stainless.lang.{ghost => ghostExpr, *}
 import stainless.proof.check
-import scala.annotation.tailrec
 import stainless.lang.Cell
-
-import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
-// import OptimisedChecks.* // Import to remove `ensuring` and `require` from the code for the benchmarks
-
+import scala.annotation.tailrec
 import MutableMapInterface.MutLongMap
 
+// BEGIN uncomment for verification ------------------------------------------
+import stainless.lang.StaticChecks._
+import stainless.lang.{ghost => ghostExpr, _}
+import stainless.proof.check
+// END uncomment for verification --------------------------------------------
+// BEGIN imports for benchmarking -------------------------------------------
+// import stainless.lang.{ghost => _, decreases => _, unfold => _, _}
+// import com.mutablemaps.map.OptimisedChecks.*
+// import Predef.{assert => _, Ensuring => _, require => _}
+
+// @tailrec
+// def dummyMutableLongMap(x: BigInt): BigInt = {
+//   if (x == BigInt(0)) then x
+//   else dummyMutableLongMap(x - BigInt(1))
+// }.ensuring( res => res == BigInt(0))
+// END imports for benchmarking ---------------------------------------------
+
 object MutableLongMap {
   import LongMapFixedSize.validMask
 

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMapOpti.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/MutableLongMapOpti.scala

@@ -4,7 +4,7 @@
   *
   * It comes without proof or specification, and is used for benchmarking purposes.
   */
-package ch.epfl.map
+package com.mutablemaps.map
 
 import stainless.annotation._
 import stainless.collection._
@@ -14,8 +14,8 @@ import stainless.proof.check
 import scala.annotation.tailrec
 import stainless.lang.Cell
 
-// import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
-import OptimisedChecks.* // Import to remove `ensuring` and `require` from the code for the benchmarks
+import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
+// import OptimisedChecks.* // Import to remove `ensuring` and `require` from the code for the benchmarks
 
 object MutableLongMapOpti {
   import LongMapFixedSizeOpti.validMask

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/MutableMapsInterface.scala

@@ -1,6 +1,6 @@
 /** Author: Samuel Chassot
   */
-package ch.epfl.map
+package com.mutablemaps.map
 
 import stainless.annotation._
 import stainless.collection._
@@ -10,7 +10,22 @@ import stainless.proof.check
 import scala.annotation.tailrec
 import stainless.lang.Cell
 
-import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
+// BEGIN uncomment for verification ------------------------------------------
+import stainless.lang.StaticChecks._
+import stainless.lang.{ghost => ghostExpr, _}
+import stainless.proof.check
+// END uncomment for verification --------------------------------------------
+// BEGIN imports for benchmarking -------------------------------------------
+// import stainless.lang.{ghost => _, decreases => _, unfold => _, _}
+// import com.ziplex.lexer.OptimisedChecks.*
+// import Predef.{assert => _, Ensuring => _, require => _, ???}
+
+// @tailrec
+// def dummyMMapInterface(x: BigInt): BigInt = {
+//   if (x == BigInt(0)) then x
+//   else dummyMMapInterface(x - BigInt(1))
+// }.ensuring( res => res == BigInt(0))
+// END imports for benchmarking ---------------------------------------------
 
 object MutableMapInterface{
   @mutable
@@ -68,7 +83,7 @@ object MutableMapInterface{
 
   @mutable
   trait MutableMap[K, V] {
-    import ch.epfl.map.ListMap
+    import com.mutablemaps.map.ListMap
     /**
      * Invariant for the datastructure
      */

data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/OptimisedChecks.scala

@@ -0,0 +1,17 @@
+/** Author: Samuel Chassot
+  */
+
+package com.mutablemaps.map
+
+object OptimisedChecks {
+  extension [T](inline value: T) inline def ensuring(condition: T => Boolean): T = value
+  inline def require(inline condition: Boolean): Unit = ()
+  inline def assert(inline condition: Boolean): Unit = ()
+  inline def check(inline condition: Boolean): Unit = ()
+  inline def decreases(inline r1: Any): Unit = ()
+  inline def decreases(inline r1: Any, inline r2: Any): Unit = ()
+  inline def decreases(inline r1: Any, inline r2: Any, inline r3: Any): Unit = ()
+  inline def decreases(inline r1: Any, inline r2: Any, inline r3: Any, inline r4: Any, inline r5: Any): Unit = ()
+  inline def ghostExpr(inline expr: Any): Unit = ()
+  inline def unfold[T](inline expr: T): Unit = ()
+}

data-structures/maps/mutablemaps/src/main/scala/ch/epfl/map/OrderedListMap.scala → data-structures/maps/mutablemaps/src/main/scala/com/mutablemaps/map/OrderedListMap.scala

@@ -1,7 +1,7 @@
 /** Author: Samuel Chassot
   */
 
-package ch.epfl.map
+package com.mutablemaps.map
 
 import stainless.annotation._
 import stainless.collection._

data-structures/maps/mutablemaps/verify.sh

@@ -1,7 +1,7 @@
 stainless-dotty\
- ./src/main/scala/ch/epfl/map/ListMap.scala\
- ./src/main/scala/ch/epfl/map/ListLongMap.scala\
- ./src/main/scala/ch/epfl/map/MutableLongMap.scala\
- ./src/main/scala/ch/epfl/map/MutableHashMap.scala\
- ./src/main/scala/ch/epfl/map/MutableMapsInterface.scala\
+ ./src/main/scala/com/mutablemaps/map/ListMap.scala\
+ ./src/main/scala/com/mutablemaps/map/ListLongMap.scala\
+ ./src/main/scala/com/mutablemaps/map/MutableLongMap.scala\
+ ./src/main/scala/com/mutablemaps/map/MutableHashMap.scala\
+ ./src/main/scala/com/mutablemaps/map/MutableMapsInterface.scala\
   --config-file=stainless.conf -Dparallel=6 $1

data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/ListLongMap.scala

@@ -1 +1 @@
-../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/ListLongMap.scala
+../../../../../../../../maps/mutablemaps/src/main/scala/com/mutablemaps/map/ListLongMap.scala

data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/ListMap.scala

@@ -1 +1 @@
-../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/ListMap.scala
+../../../../../../../../maps/mutablemaps/src/main/scala/com/mutablemaps/map/ListMap.scala

data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableHashMap.scala

@@ -1 +1 @@
-../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/MutableHashMap.scala
+../../../../../../../../maps/mutablemaps/src/main/scala/com/mutablemaps/map/MutableHashMap.scala

data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableLongMap.scala

@@ -1 +1 @@
-../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/MutableLongMap.scala
+../../../../../../../../maps/mutablemaps/src/main/scala/com/mutablemaps/map/MutableLongMap.scala

data-structures/sets/mutablesets/src/main/scala/ch/epfl/map/MutableMapsInterface.scala

@@ -1 +1 @@
-../../../../../../../../maps/mutablemaps/src/main/scala/ch/epfl/map/MutableMapsInterface.scala
+../../../../../../../../maps/mutablemaps/src/main/scala/com/mutablemaps/map/MutableMapsInterface.scala

data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/Main.scala

@@ -1,8 +1,8 @@
 package ch.epfl.set
 
-import ch.epfl.map.MutableLongMap
-import ch.epfl.map.ListLongMap
-import ch.epfl.map.Hashable
+import com.mutablemaps.map.MutableLongMap
+import com.mutablemaps.map.ListLongMap
+import com.mutablemaps.map.Hashable
 import ch.epfl.set.MutableHashSet
 
 object Main {

data-structures/sets/mutablesets/src/main/scala/ch/epfl/set/MutableHashSet.scala

@@ -7,11 +7,11 @@ import stainless.proof.check
 
 import stainless.lang.StaticChecks.* // Comment out when using the OptimisedEnsuring object below
 
-import ch.epfl.map.MutableMapInterface.MutableMap
-import ch.epfl.map.MutableHashMap
-import ch.epfl.map.Hashable
-import ch.epfl.map.ListMap
-import ch.epfl.map.TupleListOpsGenK
+import com.mutablemaps.map.MutableMapInterface.MutableMap
+import com.mutablemaps.map.MutableHashMap
+import com.mutablemaps.map.Hashable
+import com.mutablemaps.map.ListMap
+import com.mutablemaps.map.TupleListOpsGenK
 
 object MutableHashSet {
   /** Helper method to create a new empty HashSet

lexers/regex/verifiedlexer/.gitignore

@@ -34,4 +34,10 @@ metals.sbt
 
 # Stainless plugin
 stainless/
-project/lib
+project/lib
+
+stainless-stack-trace.txt
+
+.venv
+
+**/plots