Update documentation

.buildinfo

@@ -0,0 +1,4 @@
+# Sphinx build info version 1
+# This file hashes the configuration used when building these files. When it is not found, a full rebuild will be done.
+config: 2cca740605cef710b38d3bc90671a0b9
+tags: 645f666f9bcd5a90fca523b33c5a78b7

_sources/casestudies.rst.txt

@@ -0,0 +1,308 @@
+.. _casestudies:
+
+Case Studies
+============
+
+Case Study #1: Proving invariants of actor systems
+--------------------------------------------------
+
+Actor system model
+~~~~~~~~~~~~~~~~~~
+
+Our model is loosely based on the modern definition of object-based actor systems,
+and attempts to provide an idiomatic Scala API in the style of the Akka actor library.
+
+In this framework, each actor is addressed by a reference, through which other actors
+can asynchronously send messages. Each actor has an associated behavior, which holds
+the state of the actor, if any, and determines
+
+a) the operations which will be performed upon receiving a message
+b) what is the next behavior to associate with its reference
+
+A behavior can thus be seen as a data type holding some immutable values representing
+the state, and a method which takes in a message, performs some computation which might
+involve sending messages to other actors, and finally returns a new behavior.
+
+State at the actor level is thus effectively handled in a functional way, by returning
+a new behavior which holds the updated state. An actor system maintains a collection
+of one-way channels (inboxes) between any two actors in the system.
+
+An inbox is an ordered list of messages awaiting delivery, the head of the list being
+the next message to deliver.
+
+The system drives the execution by non-deterministically
+picking a non-empty inbox, taking the first message of the list, and invoking the message
+handler of the behavior associated with the destination reference.
+
+It then collects the messages to send, and appends them to the appropriate inboxes,
+and update the destination actor’s behavior with the behavior returned by the message handler.
+
+Actor system implementation
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Imports
+^^^^^^^
+
+.. code-block:: scala
+
+  import stainless.lang._
+  import stainless.collection._
+  import stainless.annotation._
+
+Message
+^^^^^^^
+
+In our framework, messages are modeled as constructors of the abstract class ``Msg``.
+
+.. code-block:: scala
+
+  abstract class Msg
+
+Actor reference
+^^^^^^^^^^^^^^^
+
+Each actor is associated with a persistent reference, modeled as instances of the case class ``ActorRef``.
+Each reference has a name, and an underlying Akka ``akka.actor.ActorRef``, marked as extern and pure (see Section :doc:`wrap` for more information about extern fields).
+
+.. code-block:: scala
+
+  case class ActorRef(
+    name: String,
+    @extern @pure
+    underlying: akka.actor.ActorRef
+  ) {
+
+    @inline
+    def !(msg: Msg)(implicit ctx: ActorContext): Unit = {
+      ctx.send(this, msg)
+    }
+  }
+
+Actor Context
+^^^^^^^^^^^^^
+
+When a message is delivered to an actor, the latter is provided with a context, which holds a reference to itself, and a mutable list of messages to send. We mark this list as ghost to avoid having to persist in memory the list of all messages sent through the context.
+
+.. code-block:: scala
+
+  case class ActorContext(
+    self: ActorRef,
+    @ghost
+    var toSend: List[(ActorRef, Msg)] = Nil()
+  ) {
+
+    def send(to: ActorRef, msg: Msg): Unit = {
+      toSend = (to, msg) :: toSend
+
+      sendUnderlying(to, msg)
+    }
+
+    @extern @pure
+    private def sendUnderlying(to: ActorRef, msg: Msg): Unit = {
+      to.underlying ! msg
+    }
+  }
+
+Behavior
+^^^^^^^^
+
+A behavior specifies both the current state of an actor, and how this one should process the next incoming message. In our framework, these are modeled as a subclass of the abstract class ``Behavior``, which defines a single abstract method ``processMsg``, to be overridden for each defined behavior.
+
+Using the provided ``ActorContext``, the implementation of the ``processMsg`` method can both access its own reference, and send messages. It is also required to return a new ``Behavior`` for handling subsequent messages.
+
+.. code-block:: scala
+
+  sealed abstract class Behavior {
+    def processMsg(msg: Msg)(implicit ctx: ActorContext): Behavior
+  }
+
+Actor System
+^^^^^^^^^^^^
+
+The state of the actor system at a given point in time is modeled as a case class, holding the behavior associated with each actor reference, and the list of in-flight messages between any two actors.
+
+It provides a ``step`` method which, whengiven two ``ActorRef``, will deliver the next message (if any) in the corresponding channel.
+
+Because the ``ActorSystem`` class is only used to model and prove properties about the underlying actor system, we mark the whole class as ghost in order to drop it from the resulting program.
+
+.. code-block:: scala
+
+  @ghost
+  case class ActorSystem(
+    behaviors: CMap[ActorRef, Behavior],
+    inboxes: CMap[(ActorRef, ActorRef), List[Msg]]
+  ) {
+
+    def step(from: ActorRef, to: ActorRef): ActorSystem = {
+      inboxes(from -> to) match {
+        case Nil() =>
+          this
+
+        case Cons(msg, msgs) =>
+          val (newBehavior, toSend) = deliverMessage(to, msg)
+
+          val newBehaviors = behaviors.updated(to, newBehavior)
+          val newInboxes = toSend.foldLeft(inboxes.updated(from -> to, msgs)) {
+            case (acc, (dest, m)) => acc.updated(to -> dest, m :: acc(to -> dest))
+          }
+
+          ActorSystem(newBehaviors, newInboxes)
+      }
+    }
+
+    private def deliverMessage(actor: ActorRef, msg: Msg): (Behavior, List[(ActorRef, Msg)]) = {
+      val behavior = behaviors(actor)
+
+      val ctx = ActorContext(actor, Nil())
+      val nextBehavior = behavior.processMsg(msg)(ctx)
+
+      (nextBehavior, ctx.toSend)
+    }
+  }
+
+Building a replicated counter
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. code-block:: scala
+
+  @extern
+  def noSender = akka.actor.ActorRef.noSender
+
+  val Primary = ActorRef("primary", noSender)
+  val Backup  = ActorRef("backup", noSender)
+
+  case object Inc extends Msg
+
+  case class Counter(value: BigInt) {
+    require(value >= 0)
+
+    def increment: Counter = Counter(value + 1)
+
+    def <=(that: Counter): Boolean = this.value <= that.value
+  }
+
+  case class PrimBehav(backup: ActorRef, counter: Counter) extends Behavior {
+    require(backup.name == "backup")
+
+    override
+    def processMsg(msg: Msg)(implicit ctx: ActorContext): Behavior = msg match {
+      case Inc =>
+        backup ! Inc
+        PrimBehav(backup, counter.increment)
+
+      case _ => this
+    }
+  }
+
+  case class BackBehav(counter: Counter) extends Behavior {
+
+    override
+    def processMsg(msg: Msg)(implicit ctx: ActorContext): Behavior = msg match {
+      case Inc =>
+        BackBehav(counter.increment)
+
+      case _ => this
+    }
+  }
+
+Proving preservation of an invariant
+^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+
+After having defined an actor system with our framework, one might want to verify that this system preserves some invariant between each step of its execution. That is to say, given an invariant ``inv: ActorSystem → Boolean``, for any ``ActorSystem`` `s` and any two ``ActorRef`` `n` and `m`, if ``inv(s)`` holds, then ``inv(s.step(n, m))`` should hold as well. In other words:
+
+:math:`\forall s: \texttt{ActorSystem}, n, m: \texttt{ActorRef}. \texttt{inv}(s) \implies \texttt{inv}(s.\texttt{step}(n, m))`
+
+We note that, because we are essentially doing a proof by induction over execution steps here, one needs also to ensure the invariant holds for some initial system. We show these two properties below:
+
+.. code-block:: scala
+
+  @ghost
+  def invariant(s: ActorSystem): Boolean = {
+    s.inboxes(Primary -> Primary).isEmpty &&
+    s.inboxes(Backup -> Primary).isEmpty &&
+    s.inboxes(Backup -> Backup).isEmpty &&
+    s.inboxes(Primary -> Backup).forall(_ == Inc) && {
+      (s.behaviors(Primary), s.behaviors(Backup)) match {
+        case (PrimBehav(_, p), BackBehav(b)) =>
+          p.value == b.value + s.inboxes(Primary -> Backup).length
+
+        case _ => false
+      }
+    }
+  }
+
+  @ghost
+  def initialSystem = ActorSystem(
+    behaviors = CMap({
+      case `Primary` => PrimBehav(Counter(0))
+      case `Backup`  => BackBehav(Counter(0))
+    }),
+    inboxes = CMap(_ => List())
+  )
+
+  @ghost
+  def initialInv = invariant(initialSystem).holds
+
+  @ghost
+  def validRef(ref: ActorRef): Boolean = ref == Primary || ref == Backup
+
+  @ghost
+  def theorem(s: ActorSystem, from: ActorRef, to: ActorRef): Boolean = {
+    require(invariant(s) && validRef(from) && validRef(to))
+    val newSystem = s.step(from, to)
+    invariant(newSystem)
+  }.holds
+
+Running the system with Akka
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+.. code-block:: scala
+
+    @ignore
+    class ActorWrapper(initialBehavior: Behavior) extends akka.actor.Actor with akka.actor.ActorLogging {
+
+      private def handler(behavior: Behavior): PartialFunction[Any, Unit] = {
+        case msg: Msg =>
+          val me = ActorRef(context.self.path.name, context.self)
+          val ctx = ActorContext(me, Nil())
+          val newBehavior = behavior.processMsg(msg)(ctx)
+
+          log.info(s"Received: $msg, becoming $newBehavior")
+          context.become(handler(newBehavior), discardOld = true)
+      }
+
+      def receive = handler(initialBehavior)
+    }
+
+.. code-block:: scala
+
+  @ignore
+  def main(args: Array[String]): Unit = {
+    val initCounter = Counter(0)
+
+    val system = akka.actor.ActorSystem("Counter")
+
+    val backupRef = ActorRef(
+      "backup",
+      system.actorOf(
+        akka.actor.Props(new ActorWrapper(BackBehav(initCounter))),
+        name = "backup"
+      )
+    )
+
+    val primaryRef = ActorRef(
+      "primary",
+      system.actorOf(
+        akka.actor.Props(new ActorWrapper(PrimBehav(backupRef, initCounter))),
+        name = "primary"
+      )
+    )
+
+    implicit val ctx = ActorContext(primaryRef, Nil())
+
+    import system.dispatcher
+    import scala.concurrent.duration._
+    system.scheduler.schedule(500.millis, 1000.millis) {
+      primaryRef ! Inc
+    }
+  }

_sources/coq.rst.txt

@@ -0,0 +1,69 @@
+.. _coq:
+
+Translation from Stainless to Coq
+=================================
+
+Initially based on a project done by `Bence Czipó
+<https://github.com/czipobence>`_, this translation is an early experimental
+stage.
+
+The `--coq` option of Stainless replaces the standard verification checker
+(which uses Inox) by a translation to Coq. Each function from the `*.scala` file
+is translated to a Coq file, and obligations corresponding to assertions,
+preconditions, and postconditions are solved using predefined tactics in Coq.
+
+.. _coq-requirements:
+
+Requirements
+------------
+
+- Coq 8.11.2
+- Coq Equations 1.2.2+8.11
+
+These can be installed using `opam
+<https://github.com/ocaml/opam/releases/latest>`_ as explained in the `Equations
+README.md <https://github.com/mattam82/Coq-Equations>`_.
+
+.. _coq-option:
+
+Usage of the Coq option
+-----------------------
+
+First, clone the `Stainless repository
+<https://github.com/epfl-lara/stainless>`_. In the `slc-lib` directory, run
+`./configure` and `make`.
+
+Then, assuming the Stainless binary ``stainless-scalac`` is in your path, run:
+``stainless-scalac --coq File.scala`` on the file of your choice. As an example,
+consider the ``test`` function from the `Arith.scala
+<https://github.com/epfl-lara/stainless/blob/master/frontends/benchmarks/coq/Arith.scala>`_
+file:
+
+.. code-block:: scala
+
+  def test(a: BigInt, b: BigInt, c: BigInt): BigInt = {
+    require(a > b && c > BigInt(0))
+    c + a
+  } ensuring( _ > c + b )
+
+Running ``stainless-scalac --coq frontends/benchmarks/coq/Arith.scala``
+generates the file ``tmp/test.v`` which contains the following Coq definition.
+
+.. code-block:: coq
+
+  Definition test (a: Z) (b: Z) (c: Z) (contractHyp4: (ifthenelse (Z.gtb a b) bool
+          (fun _ => Z.gtb c (0)%Z )
+          (fun _ => false ) = true)) : {x___1: Z | (Z.gtb x___1 (Z.add c b) = true)} :=
+  Z.add c a.
+
+  Fail Next Obligation.
+
+The ``coqc`` executable in run on the file, and the status is reported by
+Stainless. In the translation to Coq, the ``BigInt`` type is encoded as ``Z``.
+The precondition (``require``) is encoded as an extra argument ``contractHyp4``,
+and the postcondition is encoded as a refinement on the return type of `test`.
+Here, the obligation related to the postcondition is solved automatically thanks
+to the obligation tactic defined above in the ``tmp/test.v`` file. The statement
+``Fail Next Obligation.`` then succeeds because all obligations have been solved
+(any command in Coq can be prefixed with ``Fail``, and the resulting command
+succeeds when the original command fails).