Address Celina's and Felipe's comments

rfc/src/rfcs/0012-loop-contracts.md

@@ -1,6 +1,6 @@
 - **Feature Name:** Loop Contracts
-- **Feature Request Issue:** 
-- **RFC PR:** 
+- **Feature Request Issue:** [#3168](https://github.com/model-checking/kani/issues/3168)
+- **RFC PR:** [#3167](https://github.com/model-checking/kani/pull/3167)
 - **Status:** Under Review
 - **Version:** 1
 - **Proof-of-concept:** 
@@ -11,23 +11,22 @@
 
 Loop contracts provide way to safely abstract loops of a program, typically
 in order to accelerate the verification process, and remove the loop unwinding
-bounds. The key idea is to overapproximate the possible set of program states,
+bounds. The key idea is to over-approximate the possible set of program states,
 while still being precise enough to be able to prove the desired property.
 
 ## User Impact
 
 Loop contracts provide an interface for a verified, sound abstraction.
-The goal for specifying loop contracts in the source code is three fold:
+The goal for specifying loop contracts in the source code is two fold:
 
-* Unbounded verification: Currently Kani does not support proving correctness
+* Unbounded verification: Currently, proving correctness
  (i.e. assertions never fail) on programs with unbounded control flow (e.g. 
- loops with dynamic bounds). Kani unrolls all unbounded loops until a few
- iterations and then verifies this unrolled program — it thus provides a much
- weaker guarantee on correctness.
-* Faster CI runs: These contracts, when provided, would also significantly
+ loops with dynamic bounds) Kani requires unwinding loops for a large number of
+ times, which is not always feasible. Loop contracts provide a way to abstract
+ out loops, and hence remove the need for unwinding loops.
+* Faster CI runs: In most cases, the provided contracts would also significantly
  improve Kani's verification time since all loops would be unrolled only to
- a single iteration, as opposed to a small number of iterations which is
- Kani's current behavior.
+ a single iteration.
 
 
 
@@ -38,14 +37,15 @@ interfere with existing functionalities.
 
 ## User Experience
 
-A loop contract specifies the behavior of a loop as a predicate that
-can be checked against the loop implementation, and used to abstract out
+A loop contract specifies the behavior of a loop as a boolean predicate
+(loop invariants clauses) with certain frames conditions (loop modifies clauses)
+that can be checked against the loop implementation, and used to abstract out
 the loop in the verification process.
 
 We illustrate the usage of loop contracts with an example.
 Consider the following program:
 ```rs
-fn main() {
+fn simple_loop() {
  let mut x: u64 = kani::any_where(|i| *i >= 1);
 
  while x > 1{
@@ -55,13 +55,13 @@ fn main() {
  assert!(x == 1);
 }
 ```
-The loop in the `main` function keep subtracting 1 from `x` until `x` is 1.
+The loop in the `simple_loop` function keep subtracting 1 from `x` until `x` is 1.
 However, Kani currently needs to unroll the loop for `u64::MAX` number of times
 to verify the assertion at the end of the program. 
 
 With loop contracts, the user can specify the behavior of the loop as follows:
 ```rs
-fn main() {
+fn simple_loop_with_loop_contracts() {
  let mut x: u64 = kani::any_where(|i| *i >= 1);
 
  #[kani::loop_invariant(x >= 1)]
@@ -88,7 +88,7 @@ the negation of the loop guard. The requirement of satisfying the negation of th
 guard comes from the fact that a path exits the loop must fail the loop guard.
 After the loop is abstracted, the program will be equivalent to the following:
 ```rs
-fn main() {
+fn simple_loop_transformed() {
  let mut x: u64 = kani::any_where(|i| *i >= 1);
 
  x = kani::any(); // Arbitrary program state that
@@ -107,9 +107,9 @@ that they stay unchanged throughout the loop are inductive. In other words, Kani
 only havoc the memory locations that are modified in the loop. This is achieved by
 specifying the `modifies` clause for the loop. For example, the following program:
 ```rs
-fn main() {
+fn simple_loop_two_vars() {
  let mut x: u64 = kani::any_where(|i| *i >= 1);
- let mut y: u64 = kani::any_where(|i| *i >= 1);
+ let mut y: u64 = 1;
 
  #[kani::loop_invariant(x >= 1)]
  #[kani::loop_modifies(x)]
@@ -118,11 +118,13 @@ fn main() {
  };
 
  assert!(x == 1);
+ assert!(y == 1);
 }
 ```
 write to only `x` in the loop, hence the `modifies` clause contains only `x`.
 Then when use the loop contracts to abstract the loop, Kani will only havoc the memory
-location `x` and keep `y` unchanged. 
+location `x` and keep `y` unchanged. Note that if the `modifies` clause contains also
+`y`, Kani will havoc both `x` and `y`, and hence violate the assertion `y == 1`.
 
 
 Kani will also verify if all writing targets in the loop are included in the `modifies`
@@ -132,56 +134,97 @@ clause.
 Note that the `modifies` clause is optional, and Kani will infer the write set if not
 provided.
 
+
+### Proof of termination
+
+ Loop contracts also provide a way to prove the termination of the loop.
+ Without the proof of termination, the loop contracts could lead to a false
+ positive result. For example, consider the following program:
+
+```rs
+fn simple_loop_non_terminating() {
+ let mut x: u64 = kani::any_where(|i| *i >= 1);
+
+ #[kani::loop_invariant(x >= 1)]
+ while true{
+ x = x;
+ };
+
+ assert!(x >= 1);
+}
+```
+After abstracting the loop, the loop will be transformed to no-op, and the assertion
+`x >= 1` will be proved. However, the loop is actually an infinite loop, and the
+assertion will never be reached.
+
+For this reason, Kani will also require the user to provide a `decreases` clause that
+specifies a decreasing expression to prove the termination of the loop. For example, in
+```rs
+fn simple_loop_terminating() {
+ let mut x: u64 = kani::any_where(|i| *i >= 1);
+
+ #[kani::loop_invariant(x >= 1)]
+ #[kani::loop_decreases(x)]
+ while x > 1{
+ x = x - 1;
+ };
+
+ assert!(x >= 1);
+}
+```
+, the `decreases` clause `#[kani::loop_decreases(x)]` specifies that the value of `x`
+decreases at each iteration of the loop, and hence the loop will terminate.
+
+
 ## Detailed Design
 
 
 Kani implements the functionality of loop contracts in three places.
 
-1. Procedural macros `loop_invariant` and `loop_modifies`.
-2. Code generation for builtin functions expanded from the above two macros.
+1. Procedural macros `loop_invariant`, `loop_modifies`, and `loop_decreases`.
+2. Code generation for builtin functions expanded from the above macros.
 3. GOTO-level loop contracts using CBMC's contract language generated in
- `kani-compiler` for `loop-modifies` clauses.
+ `kani-compiler`.
 
-### Procedural macros `loop_invariant` and `loop_modifies`.
+### Procedural macros `loop_invariant`, `loop_modifies`, and `loop_decreases`.
 
 The `loop_invariant` macro perform code generation for the loop invariant clause.
 The generated code consists of two parts: 
-1. a closure definition to wrap the loop invariant, which is an boolean expression.
+1. a closure definition to wrap the loop invariant, which is an Boolean expression.
 2. a call to a builtin function `kani_loop_invariant` at end of the loop.
 
 As an example, in the above program, the following code will be generated for the
 loop invariants clauses:
 
 ```rs
-fn main() {
+fn simple_loop_macro_expanded() {
  let mut x: u64 = kani::any_where(|i| *i >= 1);
 
- let _loop_invariant_closure = || x >= 1;
  while x > 1{
  x = x - 1;
- kani_loop_invariant_begin();
- _loop_invariant_closure()
- kani_loop_invariant_end();
+ kani::kani_loop_invariant_begin_marker();
+ let __kani_loop_invariant: bool = x >= 1;
+ kani::kani_loop_invariant_end_marker();
  };
 
  assert!(x == 1);
 }
 ```
 
-Similarly, we generate a call to the builtin function `kani_loop_modifies` for modifies
+Similarly, we generate calls to the corresponding builtin functions for `modifies` and `decreases`
 clauses.
 
 
 ### Code Generation for Builtin Functions
 
 When generating GOTO program from MIR, Kani will first scan for the placeholder function
-calls `kani_loop_invariant_begin` and `kani_loop_invariant_end` in the MIR. Then Kani
-will generate the corresponding GOTO-level statement expression for all instructions
+calls `kani_loop_invariant_begin_marker` and `kani_loop_invariant_end_marker` in the MIR. 
+Then Kani will generate the corresponding GOTO-level statement expression for all instructions
 between the two placeholder function calls. At last, Kani will add the statement expression
 to the loop latch---the jump back to the loop head.
 
 The artifact `goto-instrument` in CBMC will extract the loop contracts from the named-subs
-of the loop latch, and the apply and prove the extracted loop contracts.
+of the loop latch, and then apply and prove the extracted loop contracts.
 
 Similarly, Kani will add the `modifies` targets into the named-subs of the loop latch for
 CBMC to extract and prove the loop contracts.
@@ -210,24 +253,14 @@ in MIR level.
 
 There are two reasons we prefer the GOTO-level transformation.
 First, `goto-instrument` is a mature tool that can correctly instrument the frame
-condition checking for the transformed loop, which will safe us from reinventing
+condition checking for the transformed loop, which will save us from reinventing
 the error-prone wheel. Second, the loop contracts synthesis tool we developed and
 are developing are all based on GOTO level. Hence, doing the transformation in
 the GOTO level will make the integration of loop contracts with the synthesis tool
 easier.
 
 ## Open questions
 
-<!-- For Developers -->
-
-- The idea of using closure to wrap the loop invariant is a bit hacky. It is not
- clear what behavior of the loop will move the variables in the closure, and hence
- invalidate the closure. Is there a better way to do this?
-<!-- 
-- Is there any part of the design that you expect to resolve through the RFC process?
-- What kind of user feedback do you expect to gather before stabilization? How will this impact your design? 
--->
-
 ## Future possibilities
 
 <!-- For Developers -->