diff --git a/labs/lab1/project.scala b/labs/lab1/project.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a6c0d57a67e77dce935488b8573ad37cd9f9a121
--- /dev/null
+++ b/labs/lab1/project.scala
@@ -0,0 +1,4 @@
+//> using scala "3.5.0"
+//> using jar "stainless-library_2.13-0.9.8.1.jar"
+//> using dep "org.scalameta::munit::1.0.2"
+//> using options "-Wconf:msg=not.*?exhaustive:s,msg=pattern.*?specialized:s"
\ No newline at end of file
diff --git a/labs/lab1/src/BooleanAlgebra.scala b/labs/lab1/src/BooleanAlgebra.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bd7f6b765a8cb12018b2205d6d4ea0ded7ffb5d6
--- /dev/null
+++ b/labs/lab1/src/BooleanAlgebra.scala
@@ -0,0 +1,81 @@
+
+object BooleanAlgebra {
+
+
+ // AST for boolean formulas
+
+ sealed trait Formula {
+ infix def &&(rhs: Formula): Formula = And(this, rhs)
+ infix def ||(rhs: Formula): Formula = Or(this, rhs)
+ infix def ==>(rhs: Formula): Formula = Implies(this, rhs)
+ def unary_! : Formula = Not(this)
+
+ override def toString(): String = this match {
+ case Var(id) => s"x($id)"
+ case And(lhs, rhs) => s"($lhs && $rhs)"
+ case Or(lhs, rhs) => s"($lhs || $rhs)"
+ case Implies(lhs, rhs) => s"($lhs ==> $rhs)"
+ case Not(f) => s"!$f"
+ case True => "True"
+ case False => "False"
+ }
+ }
+ def x(i: Int): Formula = Var(i)
+
+ case class Var(id: Int) extends Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case object True extends Formula
+ case object False extends Formula
+
+
+
+ // Evaluation of boolean formulas
+
+ def eval(f: Formula, env: Int => Boolean): Boolean = ??? // TODO
+
+ // Substitution of boolean formulas
+ def substitute(f: Formula, env: Int => Formula): Formula = ??? // TODO
+
+ // Negation normal form
+
+ def nnf(f: Formula): Formula = ??? // TODO
+
+ def variables(f: Formula): Set[Int] = ??? // TODO
+
+ def validity(f: Formula): Boolean = ??? // TODO
+
+ // And-Inverter Graphs representation
+ // (https://en.wikipedia.org/wiki/And-inverter_graph)
+
+
+ sealed trait AIG_Formula{
+ infix def &&(rhs: AIG_Formula): AIG_Formula = AIG_Node(this, rhs, true)
+ infix def ↑(rhs: AIG_Formula): AIG_Formula = AIG_Node(this, rhs, false)
+
+ override def toString(): String = this match {
+ case AIG_Var(id, true) => s"y($id)"
+ case AIG_Var(id, false) => s"!y($id)"
+ case AIG_Node(lhs, rhs, true) => s"($lhs && $rhs)"
+ case AIG_Node(lhs, rhs, false) => s"($lhs ↑ $rhs)"
+ }
+ }
+ def y(id: Int) = AIG_Var(id, true)
+
+ case class AIG_Var(id: Int, polarity: Boolean) extends AIG_Formula {
+ infix def unary_! = AIG_Var(id, !polarity)
+ }
+ case class AIG_Node(lhs: AIG_Formula, rhs: AIG_Formula, polarity: Boolean ) extends AIG_Formula
+
+ def AIG_eval(f: AIG_Formula, env: Int => Boolean): Boolean = ??? // TODO
+
+ def AIG_variables(f: AIG_Formula): Set[Int] = ??? // TODO
+
+ def AIG_validity(f: AIG_Formula): Boolean = ??? // TODO
+
+ def formulaToAIG(f: Formula): AIG_Formula = ??? // TODO
+
+
+}
\ No newline at end of file
diff --git a/labs/lab1/src/Sublist.scala b/labs/lab1/src/Sublist.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a041f6d3cff6623b4d440406662a4d53515d1d27
--- /dev/null
+++ b/labs/lab1/src/Sublist.scala
@@ -0,0 +1,125 @@
+
+import stainless.lang._
+import stainless.collection._
+import stainless.annotation._
+
+/*
+ * The definition of List and its operations can be found here:
+ * https://github.com/epfl-lara/stainless/blob/64a09dbc58d0a41e49e7dffbbd44b234c4d2da59/frontends/library/stainless/collection/List.scala
+ * You should not need them, but you can find some lemmas on List here:
+ * https://github.com/epfl-lara/stainless/blob/64a09dbc58d0a41e49e7dffbbd44b234c4d2da59/frontends/library/stainless/collection/ListSpecs.scala
+ */
+
+def sublist[T](l1: List[T], l2: List[T]): Boolean = {
+ (l1, l2) match {
+ case (Nil(), _) => true
+ case (_, Nil()) => false
+ case (Cons(x, xs), Cons(y, ys)) => (x == y && sublist(xs, ys)) || sublist(l1, ys)
+ }
+}
+
+@extern
+@main
+def main(): Unit = {
+ def example(lhs: List[Int], rhs: List[Int]): Unit = {
+ println(s"${lhs.toScala.mkString("<", ",", ">")} ⊑ ${rhs.toScala.mkString("<", ",", ">")} = ${sublist(lhs, rhs)}")
+ }
+
+ example(List(0, 2), List(0, 1, 2))
+ example(List(0, 0, 2), List(0, 2))
+ example(List(1, 0), List(0, 0, 1))
+ example(List(10, 5, 25), List(70, 10, 11, 8, 5, 25, 22))
+ example(List(25, 11, 53, 38), List(15, 25, 11, 8, 53, 22, 38))
+}
+
+object SublistSpecs {
+
+ /* forall l, sublist(l, l) */
+ def reflexivity[T](l: List[T]): Unit = {
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ sublist(l, l)
+ )
+
+ def leftTail[T](l1: List[T], l2: List[T]): Unit = {
+ require(!l1.isEmpty && sublist(l1, l2))
+
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ sublist(l1.tail, l2)
+ )
+
+ def tails[T](l1: List[T], l2: List[T]): Unit = {
+ require(!l1.isEmpty && !l2.isEmpty && l1.head == l2.head && sublist(l1, l2))
+
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ sublist(l1.tail, l2.tail)
+ )
+
+ /* forall l1 l2 l3, sublist(l1, l2) /\ sublist(l2, l3) ==> sublist(l1, l3) */
+ def transitivity[T](l1: List[T], l2: List[T], l3: List[T]): Unit = {
+ require(sublist(l1, l2) && sublist(l2, l3))
+
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ sublist(l1, l3)
+ )
+
+ def lengthHomomorphism[T](l1: List[T], l2: List[T]): Unit = {
+ require(sublist(l1, l2))
+
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ l1.length <= l2.length
+ )
+
+ def biggerSublist[T](l1: List[T], l2: List[T]): Unit = {
+ require(sublist(l1, l2) && l1.length >= l2.length)
+
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ l1 == l2
+ )
+
+ def antisymmetry[T](l1: List[T], l2: List[T]): Unit = {
+ require(sublist(l1, l2) && sublist(l2, l1))
+
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ l1 == l2
+ )
+
+ /*
+ * ++ is the list concatenation operator.
+ * It is defined here:
+ * https://github.com/epfl-lara/stainless/blob/64a09dbc58d0a41e49e7dffbbd44b234c4d2da59/frontends/library/stainless/collection/List.scala#L46
+ */
+ def extendRight[T](l1: List[T], l2: List[T]): Unit = {
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ sublist(l1, l1 ++ l2)
+ )
+
+ def extendLeft[T](l1: List[T], l2: List[T]): Unit = {
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ sublist(l2, l1 ++ l2)
+ )
+
+ def prepend[T](l: List[T], l1: List[T], l2: List[T]): Unit = {
+ require(sublist(l1, l2))
+
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ sublist(l ++ l1, l ++ l2)
+ )
+
+ def append[T](l1: List[T], l2: List[T], l: List[T]): Unit = {
+ require(sublist(l1, l2))
+
+ /* TODO: Prove me */
+ }.ensuring(_ =>
+ sublist(l1 ++ l, l2 ++ l)
+ )
+}
diff --git a/labs/lab1/test/Tests.scala b/labs/lab1/test/Tests.scala
new file mode 100644
index 0000000000000000000000000000000000000000..acdbb9b23733316b7ccbbb8378cfb89adba774f8
--- /dev/null
+++ b/labs/lab1/test/Tests.scala
@@ -0,0 +1,137 @@
+import munit.{FunSuite, Tag}
+
+import BooleanAlgebra.*
+
+class Tests extends FunSuite {
+
+
+ test("eval") {
+ def env = (id: Int) => id%2 == 0
+
+ assertEquals(eval(True, env), true)
+ assertEquals(eval(False, env), false)
+ assertEquals(eval(x(0), env), true)
+ assertEquals(eval(x(1), env), false)
+ assertEquals(eval(x(0) && x(1), env), false)
+ assertEquals(eval(x(0) || x(1), env), true)
+ assertEquals(eval(x(0) ==> x(1), env), false)
+ assertEquals(eval(!x(1), env), true)
+ assertEquals(eval((!x(0) && x(1)) || (x(2) && x(3) || x(4)) ==> (x(0) && !x(1)), env), true)
+ }
+
+ test("substitute") {
+ def env(id: Int): Formula =
+ if id == 0 then Var(10)
+ else if id == 1 then Var(11)
+ else if id % 2 == 0 then env(id/2) && !env(id/2 - 1)
+ else !env((id-1)/2) || env((id-1)/2 - 1)
+
+ assertEquals(substitute(x(0), id => x(id+1)), x(1))
+ assertEquals(substitute(x(0) && x(1), id => x(id+1)), x(1) && x(2))
+ assertEquals(substitute(x(0) || x(1), id => x(id+1)), x(1) || x(2))
+ assertEquals(substitute(!x(0), id => x(id+1)), !x(1))
+ assertEquals(substitute(x(0) ==> x(1), id => x(id+1)), x(1) ==> x(2))
+ assertEquals(substitute((!x(0) && x(1)) || (x(2) && x(3) || x(4)) ==> (x(0) && !x(1)), id => x(id+1)),
+ (!x(1) && x(2)) || (x(3) && x(4) || x(5)) ==> (x(1) && !x(2)))
+ assertEquals(substitute((!x(0) && x(1)) || (x(2) && x(3) || x(4)) ==> (x(0) && !x(1)), env),
+ ((!x(10) && x(11)) || ((((x(11) && !x(10)) && (!x(11) || x(10))) || ((x(11) && !x(10)) && !x(11))) ==> (x(10) && !x(11)))))
+
+ }
+
+ test("nnf") {
+ assertEquals(nnf(!True), False)
+ assertEquals(nnf(!False), True)
+ assertEquals(nnf(x(0)), x(0))
+ assertEquals(nnf(!(x(0) && x(1))), !x(0) || !x(1))
+ assertEquals(nnf(!(x(0) || x(1))), !x(0) && !x(1))
+ assertEquals(nnf(!(x(0) ==> x(1))), x(0) && !x(1))
+ assertEquals(nnf((x(0) ==> x(1))), !x(0) || x(1))
+ assertEquals(nnf(!(!x(0))), x(0))
+ assertEquals(nnf((!x(0) && x(1)) || ((x(2) && x(3) || x(4)) ==> (x(0) && !x(1)))),
+ (!x(0) && x(1)) || (((!x(2) || !x(3)) && !x(4)) || (x(0) && !x(1))))
+ }
+
+ test("variables") {
+ assertEquals(variables(True), Set())
+ assertEquals(variables(False), Set())
+ assertEquals(variables(x(0)), Set(0))
+ assertEquals(variables(x(0) && x(1)), Set(0, 1))
+ assertEquals(variables(x(0) || x(1)), Set(0, 1))
+ assertEquals(variables(x(0) ==> x(1)), Set(0, 1))
+ assertEquals(variables(!(x(0) && x(1))), Set(0, 1))
+ assertEquals(variables(!x(0)), Set(0))
+ assertEquals(variables((!x(0) && x(1)) || ((x(2) && x(3) || x(4)) ==> (x(0) && !x(1)))), Set(0, 1, 2, 3, 4))
+ }
+
+ test("validity") {
+ assertEquals(validity(True), true)
+ assertEquals(validity(False), false)
+ assertEquals(validity(x(0)), false)
+ assertEquals(validity(x(0) && !x(0)), false)
+ assertEquals(validity(x(0) || !x(0)), true)
+ assertEquals(validity(False || (x(0) ==> x(0))), true)
+ assertEquals(validity(x(0) ==> !x(0)), false)
+ assertEquals(validity(x(1) ==> (x(0) ==> x(1))), true)
+ assertEquals(validity((x(0) ==> x(1)) ==> (x(1) ==> !x(0))), false)
+ assertEquals(validity((!x(0) && x(1)) || ((x(2) && x(3) || x(4)) ==> (x(0) && !x(1)))), false)
+ assertEquals(validity(((x(0) ==> x(1)) && (x(1) ==> x(2))) ==> (x(0) ==> x(2))), true)
+ }
+
+ test("AIG_eval") {
+ def env = (id: Int) => id%2 == 0
+ assertEquals(AIG_eval(!y(0), env), false)
+ assertEquals(AIG_eval(y(0) ↑ y(1), env), true)
+ assertEquals(AIG_eval(y(0) ↑ y(1), env), true)
+ assertEquals(AIG_eval(y(0) && y(0), env), true)
+ assertEquals(AIG_eval(y(1) && y(1), env), false)
+ assertEquals(AIG_eval(y(0) ↑ y(0), env), false)
+ assertEquals(AIG_eval(y(1) ↑ y(1), env), true)
+ assertEquals(AIG_eval((y(0) ↑ y(1)) ↑ ((!y(2) && y(3) && !y(4)) ↑ !y(5)), env), false)
+ }
+
+ test("AIG_variables") {
+ assertEquals(AIG_variables(y(0)), Set(0))
+ assertEquals(AIG_variables(y(0) ↑ y(1)), Set(0, 1))
+ assertEquals(AIG_variables(y(0) && y(0)), Set(0))
+ assertEquals(AIG_variables(!y(1) ↑ y(1)), Set(1))
+ assertEquals(AIG_variables((y(0) ↑ y(1)) ↑ ((!y(2) && y(0) && !y(4)) ↑ !y(2))), Set(0, 1, 2, 4))
+ }
+
+ test("AIG_validity") {
+ //correct test cases with &&, !, ↑
+ assertEquals(AIG_validity(y(0) ↑ !y(0)), true)
+ assertEquals(AIG_validity(y(0) ↑ y(1)), false)
+ assertEquals(AIG_validity(y(0) ↑ y(0)), false)
+ assertEquals(AIG_validity((y(1) ↑ (y(0) && !y(1)))), true)
+ assertEquals(AIG_validity(((y(0) ↑ !y(1)) ↑ (y(1) && y(0)))), false)
+ assertEquals(AIG_validity((!y(0) ↑ y(1)) ↑ (((y(2) ↑ y(3)) ↑ !y(4)) && (y(0) ↑ !y(1)))), false)
+ assertEquals(AIG_validity((((y(0) ↑ !y(1)) && (y(1) ↑ !y(2))) ↑ (y(0) && !y(2)))), true)
+ }
+
+ test("formulaToAIG") {
+ inline def assertCorrectAIG(f: Formula): Unit =
+ val aigf = formulaToAIG(f)
+ (variables(f) ++ AIG_variables(aigf)).subsets().foreach(subset =>
+ assertEquals(eval(f, subset.contains),AIG_eval(aigf, subset.contains))
+ )
+ assertCorrectAIG(True)
+ assertCorrectAIG(False)
+ assertCorrectAIG(x(0))
+ assertCorrectAIG(x(0) && x(1))
+ assertCorrectAIG(x(0) || x(1))
+ assertCorrectAIG(x(0) ==> x(1))
+ assertCorrectAIG(!(x(0) && x(1)))
+ assertCorrectAIG(!(x(0) || x(1)))
+ assertCorrectAIG(!(x(0) ==> x(1)))
+ assertCorrectAIG(!x(1))
+ assertCorrectAIG((!x(0) && x(1)) || (x(2) && x(3) || x(4)) ==> (x(0) && !x(1)))
+ assertCorrectAIG((x(0) ==> x(1)) && (x(1) ==> x(2)) && (x(0) ==> x(2)))
+ assertCorrectAIG((x(0) ==> x(1)) || (x(1) ==> x(2)) || (x(0) ==> x(2)))
+ assertCorrectAIG((x(0) ==> x(1)) && !(x(1) ==> x(2) || x(3) || x(4) || x(5)) && (x(0) ==> x(2)))
+ assertCorrectAIG((x(0) ==> x(1)) || (x(1) ==> x(2) && x(3) && x(4) && !x(5)) || (x(0) ==> x(2)))
+
+
+ }
+
+
+}
\ No newline at end of file