Some synthesis stuff

doc/synthesis.rst

@@ -11,57 +11,77 @@ consists of translating these specifications (or expectations) to executable
 programs which realises them.
 
 As we have seen previously, relatively precise specifications of complex
-operations can be written consicely. Synthesis can thus reduce development time
+operations can be written concisely. Synthesis can thus reduce development time
 and allows the user to focus on high-level aspects.
 
 Deductive Synthesis Framework
 -----------------------------
 
-Closing Rules
--------------
+The synthesizer takes a synthesis problem that it extracts from ``choose`` or
+holes (``???``) found in the program. Formally, we define a **synthesis problem** as
 
-Ground
-^^^^^^
+.. math::
 
-This rule applies when the synthesis problem has no input variables. If the
-specification is satisfiable, its model corresponds to a valid solution. We
-rely on SMT solvers to check satisfiability of the formulas. For instance:
+    [[ ~~ \bar{a} ~~ \langle ~~ \Pi \rhd \phi ~~ \rangle ~~  \bar{x} ~~ ]]
+
+
+which carries the following information:
+
+ * a set of input variables :math:`\bar{a}`, initially all variables in scope of the ``choose``,
+ * a set of output variables :math:`\bar{x}`, corresponding to the values to synthesize,
+ * a path-condition :math:`\Pi`, constraining :math:`\bar{a}`,
+ * the specification :math:`\phi` relating input variables to output variables.
+
+The job of the synthesizer is to convert this problem into a solution :math:`[ ~ P ~ | ~ T ~ ]`, which consists of
+
+ * a executable program term :math:`T` (an expression that may contain input variables),
+ * a precondition  :math:`P` under which this program is valid
+
+To illustrate, we consider the following program:
 
 .. code-block:: scala
 
-  choose ((x: Int, y: Int) => x > 42 && y > x)
+  def foo(a: BigInt, b: BigInt): Int = {
+    if (a > b) {
+      choose ( (x: BigInt) => x > a)
+    } else {
+      0
+    }
+  }
 
-can trivially be synthesized by ``(1000, 1001)``.
 
-If the specification turns out to be UNSAT, the synthesis problem is impossible
-and we synthesize it as an ``error`` with a ``false`` precondition.
+From this program, we will extract the following initial synthesis problem:
 
+.. math::
 
-Optimistic Ground
-^^^^^^^^^^^^^^^^^
+    [[ ~~ a, b ~~ \langle ~~ a > b ~ \rhd ~ x > a ~~ \rangle ~~  x ~~ ]]
 
-This rule acts like `Ground`, but without the requirement on the absence of input
-variables. The reasonning is that even though the problem has input variables,
-the solutions might still be a constant expression.
+A possible solution to this problem would be:
 
-`Optimistic Ground` also tries to satisfy the specification, but it also needs
-to validate the resulting model. That is, given a valuation of output
-variables, it checks whether it exists a valuation for input variables such that
-the specification is violated. The model is discarded if such counter-example
-is found. If no counter-example exist, we solve the synthesis problem with the
-corresponding values.
+.. math::
 
-The rule tries at most three times to discover a valid value.
+   [ ~ \top ~ | ~ a + 1 ~ ]
 
-CEGIS
-^^^^^
+To solve this problem, the synthesizer will apply a series of rules which will
+try to either
+
+ 1. Decompose this problem into sub problems, which may be simpler to solve
+ 2. Immediately find a solution
+
+
+This corresponds to an and-or graph of rule applications, which Leon will
+explore.
 
-TEGIS
-^^^^^
 
 Decomposing Rules
 -----------------
 
+Leon defines several rules that decompose a synthesis problem (a ``choose``)
+into sub-problems that may be simpler to solve. Such rules also define a way to
+generate a solution for the original problem, when provided with solutions for
+all of the sub-problems. These rules thus both decompose the problems and
+recompose the solutions. Leon defines several of such decomposing rules:
+
 Equality Split
 ^^^^^^^^^^^^^^
 
@@ -84,7 +104,7 @@ this rule generates two sub-chooses, and combines them as follows:
    }
 
 
-Inequality Split
+Inequalite Split
 ^^^^^^^^^^^^^^^^
 
 Given two input variables `a` and `b` of numeric type, this rule
@@ -139,7 +159,7 @@ substituted by the appropriate case, and combines them as follows:
 Int Induction
 ^^^^^^^^^^^^^
 
-Given an integer (or bigint) variable `a`, the rules performs induction on `a`:
+Given an Int (or BigInt) variable `a`, the rules performs induction on `a`:
 
 .. code-block:: scala
 
@@ -238,14 +258,14 @@ redundancies. We consider two kinds of equivalences:
  1) Simple equivalences: the specification contains  :math:`a = b` at the top
  level.
 
- 2) ADT equialences: the specification contains :math:`l.isInstanceOf[Cons]
+ 2) ADT equivalence the specification contains :math:`l.isInstanceOf[Cons]
  \land h = l.head \land t = l.tail` which entails :math:`l = Cons(h, t)` and
  thus allows us to substitute :math:`l` by :math:`Cons(h, t)`.
 
-Eliminating equivalences prevents explosion of redundant rule instanciations.
+Eliminating equivalences prevents explosion of redundant rule instantiations.
 For instance, if you have four integer variables where three of them are
 equivalent, Leon has 6 ways of applying `Inequality Split`. After
-eliminating equivalences, only one application remains posible.
+eliminating equivalences, only one application remains possible.
 
 Unused Input
 ^^^^^^^^^^^^
@@ -287,3 +307,100 @@ define it.
     DetupleOutput,
     DetupleInput,
     InnerCaseSplit
+
+Closing Rules
+-------------
+
+While decomposing rules split problems in sub-problems, Leon also defines rules
+that are able to directly solve certain synthesis problems. These rules are
+crucial for the synthesis search to terminate efficiently. We define several
+closing rules that apply in different scenarios:
+
+Ground
+^^^^^^
+
+This rule applies when the synthesis problem has no input variables. If the
+specification is satisfiable, its model corresponds to a valid solution. We
+rely on SMT solvers to check satisfiability of the formulas. For instance:
+
+.. code-block:: scala
+
+  choose ((x: Int, y: Int) => x > 42 && y > x)
+
+can trivially be synthesized by ``(1000, 1001)``.
+
+If the specification turns out to be UNSAT, the synthesis problem is impossible
+and we synthesize it as an ``error`` with a ``false`` precondition.
+
+
+Optimistic Ground
+^^^^^^^^^^^^^^^^^
+
+This rule acts like `Ground`, but without the requirement on the absence of input
+variables. The reasoning is that even though the problem has input variables,
+the solutions might still be a constant expression.
+
+`Optimistic Ground` also tries to satisfy the specification, but it also needs
+to validate the resulting model. That is, given a valuation of output
+variables, it checks whether it exists a valuation for input variables such that
+the specification is violated. The model is discarded if such counter-example
+is found. If no counter-example exist, we solve the synthesis problem with the
+corresponding values.
+
+The rule tries at most three times to discover a valid value.
+
+CEGIS
+^^^^^
+
+`CEGIS` stands for Counter-Example-Guided Inductive Synthesis, it explores the
+space of small expressions to find valid solutions. Here we represent the space
+of programs by a tree, where branches are determined by free boolean variables.
+For instance, a tree for small integer operations could be:
+
+.. code-block:: scala
+
+  def res(b, a1, a2) =      if (b1) 0
+                       else if (b2) 1
+                       else if (b3) a1
+                       else if (b4) a2
+                       else if (b5) c1(b, a1, a2) + c2(b, a1, a2)
+                       else         c1(b, a1, a2) * c2(b, a1, a2)
+
+  def c1(b, a1, a2)  =      if (b7) 0
+                       else if (b8) 1
+                       else if (b9) a1
+                       else         a2
+
+  def c2(b, a1, a2)  =      if (b10) 0
+                       else if (b11) 1
+                       else if (b12) a1
+                       else          a2
+
+At a high-level, it consists of the following loop:
+
+ 1. Find one expression and inputs that satisfies the specification:
+    :math:`\exists \bar{b}, a1, a2. spec(a1, a2, res(\bar{b}, a1, a2))`.
+    If this fails, we know that the solution is not in the search space.
+    If this succeeds, we:
+
+ 2. Validate the expression represented by :math:`M_\bar{b}` for all inputs by
+    searching for a counter-example: :math:`\exists a1, a2. \lnot spec(a1, a2, res(M_\bar{b}, a1, a2))`. 
+    If such counter-example exists, start over with (1) with this program
+    excluded. If no counter-example exists we found a valid expression.
+
+The space of expressions our CEGIS rule considers is small expressions of
+bounded depth (3), which contain for each type: a few literals, functions and
+operations returning that type that do not transitively call the function under
+synthesis (to prevent infinite loops), and recursive calls where one argument is
+decreasing.
+
+
+TEGIS
+^^^^^
+
+This rule uses the same search space as `CEGIS` but relies only on tests
+(specified by the user or generated) to validate expressions. It is thus a
+generally faster way of discovering candidate expressions. However, these
+expressions are not guaranteed to be valid since they have only been validated
+by tests. Leon's synthesis framework supports untrusted solutions which trigger
+an end-to-end validation step that relies on verification.