Documentation for decreases clauses

Co-authored-by: Long Pham <[email protected]>

Author: SaswatPadhi

doc/cprover-manual/contracts-decreases.md

@@ -1,3 +1,183 @@
-# Decreases Clause
+# Decreases Clauses
 
-TODO: Document `__CPROVER_decreases`
+A _decreases_ clause specifies a measure that must strictly decrease
+monotonically at every iteration of a loop.
+By demonstrating that the measure
+1. is bounded from below, and
+2. strictly decreases monotonically at each iteration,
+we can prove termination of loops.
+This is because the measure must eventually hit the lower bound
+at which point the loop must terminate,
+since the measure cannot strictly decrease further.
+
+In the scientific literature, this measure is also called a _loop variant_ or _ranking function_.
+Although they can be arbitrary (strict) well-founded relations on arbitrary domains,
+we restrict decreases clauses to (strict) arithmetic inequalities.
+Unlike mathematical integers, arithmetic types in C are all bounded from below.
+Furthermore, unlike mathematical real numbers, floating-point arithmetic types in C are not dense.
+Hence, any strictly decreasing arithmetic expression in C can be used as a decreases clause.
+
+### Syntax
+
+A one-dimensional (1D) decreases clause for a loop is an arithmetic expression `e`
+over the variables visible at the same scope as the loop,
+specified as `__CPROVER_decreases(e)`.
+
+Like invariant clauses, decreases clauses may be specified just after the loop guard.
+An example of a 1D decreases clause is shown below.
+
+```c
+for(int i = 0; i < n; i += 2)
+__CPROVER_loop_invariant(0 <= i && i <= n)
+__CPROVER_decreases(n - i)
+{ ... }
+```
+
+Please see the [invariant clauses](contracts-invariants.md) page
+for more examples on `for` and `do...while` loops.
+
+To help prove termination of more complex loops,
+CBMC also supports multi-dimensional decreases clauses.
+A multi-dimensional decreases clause is an [ordered tuple](https://en.wikipedia.org/wiki/Tuple)
+of arithmetic expressions, specified as `__CPROVER_decreases(e_1, e_2, ..., e_n)`.
+An example of a multi-dimensional decreases clause is given below.
+
+```c
+while(i < n)
+__CPROVER_loop_invariant(0 <= i && i <= n)
+__CPROVER_loop_invariant(0 <= j && j <= n)
+__CPROVER_decreases(n - i, n - j)
+{
+  if (j < n)
+    j++;
+  else
+  {
+    i++;
+    j = 0;
+  }
+}
+```
+
+We extend the strict arithmetic comparison for 1D decreases clauses
+to a strict [lexicographic comparison](https://en.wikipedia.org/wiki/Lexicographic_order)
+for multi-dimensional decreases clauses.
+
+**Important.**
+Like invariant clauses, decreases clauses must be free of side effects,
+for example, mutation of local or global variables.
+
+### Semantics
+
+A decreases clause extends the loop abstraction introduced in the [invariants clause](contracts-invariants.md) document.
+In addition to the inductiveness check asserted at the end of a single arbitrary iteration,
+CBMC would also assert the strict decrement of the measure specified in the decreases clause.
+At a high level, in addition to the assumptions and assertions introduced by the invariant clause,
+a decreases clause expands to three key steps:
+1. At the beginning of the loop body, record the initial value of the measure specified in the decreases clause.
+2. At the end of the loop body, record the final value of the measure specified in the decreases clause.
+3. After the loop iteration, assert that the final value is strictly smaller than the initial one.
+
+For a 1D decreases clause, we use the strict arithmetic comparison (i.e., `<`).
+For a multi-dimensional decreases clause, say `(e_1, ..., e_n)`,
+we extend the strict arithmetic comparison to a strict lexicographic comparison.
+Formally, given two evaluations `(a_1, ..., a_n)` and `(b_1, ..., b_n)`,
+a strict lexicographic comparison, denoted by `(a_1, ..., a_n) ≺ (b_1, ..., b_n)`,
+is defined as the predicate:
+
+```c
+   (a_1 < b_1)
+|| (a_1 == b_1 && a_2 < b_2)
+|| ...
+|| (a_1 == b_1 && ... && a_n < b_n)
+```
+
+where `||` and `&&` are Boolean disjunction and conjunction respectively.
+
+As an example, consider our binary search implementation again,
+this time with a decreases clause annotation to prove its termination:
+
+```c
+int binary_search(int val, int *buf, int size)
+{
+  if(size <= 0 || buf == NULL) return NOT_FOUND;
+
+  long lb = 0, ub = size - 1;
+  long mid = (lb + ub) / 2;
+
+  while(lb <= ub)
+  __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size)
+  __CPROVER_loop_invariant(mid == (lb + ub) / 2L)
+  __CPROVER_decreases(ub - lb)
+  {
+     if(buf[mid] == val) break;
+     if(buf[mid] < val)
+       lb = mid + 1;
+     else
+       ub = mid - 1;
+     mid = (lb + ub) / 2;
+  }
+  return lb > ub ? NOT_FOUND : mid;
+}
+```
+
+The instrumented GOTO program is conceptually similar to the following high-level C program:
+
+```c
+int binary_search(int val, int *buf, int size)
+{
+  if(size <= 0 || buf == NULL) return NOT_FOUND;
+
+  long lb = 0, ub = size - 1;
+  long mid = (lb + ub) / 2;
+
+  /* 1. assert invariant at loop entry */
+  assert(0L <= lb && lb - 1L <= ub && ub < size);
+  assert(mid == (lb + ub) / 2L);
+
+  /* 2. create a non-deterministic state for modified variables */
+  havoc(lb, ub, mid);
+
+  /* 3. establish invariant to model state at an arbitrary iteration */
+  __CPROVER_assume(0L <= lb && lb - 1L <= ub && ub < size)
+  __CPROVER_assume(mid == (lb + ub) / 2L)
+
+  /* 4. perform a single arbitrary iteration (or exit the loop) */
+  if(lb <= ub)
+  {
+    /* 5. declare variables for tracking the loop variant */
+    int old_measure, new_measure;
+
+    /* 6. evaluate the variant at the start of the loop body */
+    old_measure = ub - lb;
+
+    if(buf[mid] == val) break;
+    if(buf[mid] < val)
+      lb = mid + 1;
+    else
+      ub = mid - 1;
+    mid = (lb + ub) / 2;
+
+    /* 7. assert the invariant to establish inductiveness */
+    assert(0L <= lb && lb - 1L <= ub && ub < size);
+    assert(mid == (lb + ub) / 2L);
+
+    /* 8. evaluate the variant at the end of the loop body */
+    new_measure = ub - lb;
+
+    /* 9. assert the decreases clause */
+    assert(new_measure < old_measure);
+
+    /* 10. terminate this symbolic execution path; similar to "exit" */
+    __CPROVER_assume(false);
+  }
+  return lb > ub ? NOT_FOUND : mid;
+}
+```
+
+The instrumented code points (5), (6), (8), and (9) are specific to the decreases clause.
+
+**Important.** 
+Decreases clauses work in conjunction with [loop invariants](contract-invariants.md),
+which model an arbitrary loop iteration at which the decreases clause is checked.
+If a decreases clause is annotated on a loop without an invariant clause,
+then the weakest possible invariant (i.e, `true`) is used to model an arbitrary iteration.

doc/cprover-manual/contracts-invariant.md renamed to doc/cprover-manual/contracts-invariants.md

@@ -1,4 +1,4 @@
-# Invariant Clause
+# Invariant Clauses
 
 An _invariant_ clause specifies a property that must be preserved
 by every iteration of a loop.
@@ -50,7 +50,7 @@ for example, mutation of local or global variables.
 
 ### Semantics
 
-The loop invariant clause expands to several assumptions and assertions:
+A loop invariant clause expands to several assumptions and assertions:
 1. The invariant is _asserted_ just before the first iteration.
 2. The invariant is _assumed_ on a non-deterministic state to model a non-deterministic iteration.
 3. The invariant is finally _asserted_ again to establish its inductiveness.
@@ -77,7 +77,6 @@ int binary_search(int val, int *buf, int size)
   while(lb <= ub)
   __CPROVER_loop_invariant(0L <= lb && lb - 1L <= ub && ub < size)
   __CPROVER_loop_invariant(mid == (lb + ub) / 2L)
-  __CPROVER_decreases(ub - lb)
   {
      if(buf[mid] == val) break;
      if(buf[mid] < val)