Verification Unrolling

The first tool that Imandra makes available in our verification toolbox is recursive function unrolling, a form of bounded model checking backed by Satisfiability Modulo Theories (SMT) solving. This technique is completely automatic, and is in general not influenced by the presence of proved rules or enabled/disabled functions (except with used in conjunction with the simp attribute).

Completeness

For many classes of problems, unrolling is “complete” in various senses. For example, for goals involving only non-recursive functions, algebraic datatypes and linear arithmetic, unrolling will always be able to prove a true goal or refute a false goal in a finite amount of time and space. Moreover, for an even wider class of problems involving recursive functions, datatypes and arithmetic, unrolling is “complete for counterexamples.” This means that if a counterexample to a goal exists, unrolling will in principle always be able to synthesize one. This relies on Imandra’s “fair” strategy for incrementally expanding the “interpretation call-graph” of a goal.

That said, part of the beauty of unrolling is that you don’t need to understand it to apply it!

Strategy

In general, it’s recommended to apply unrolling to a goal before you attempt other methods such as the inductive waterfall (auto). It’s amazing how often seemingly true goals are false due to subtle edge cases, and the ability of unrolling to construct concrete counterexamples can be an invaluable filter on your conjectures.

Examples

To use unrolling, we simply use the verify or instance commands.

Let’s use unrolling to find an instance of two lists of integers, whose sum equals the length of the two lists concatenated. We shall constrain the total length of the two lists to be positive (for fun, at least 10), so we obtain something more interesting than the simple x=[],y=[] solution!

instance
  (fun x y -> List.length (x@y) > 10
    && List.fold_left (+) 0 (x@y) = List.length (x@y))

Imandra was able to find a solution instantly. If you are using ImandraX VSCode extension, you can copy and interact with the solution using “Copy” and “Interact” code actions. Let’s compute with it to better understand it:

module M = struct
  let y = [8456; 7719; 8855; (-18845); 609; 5853; (-4461); 2997; 4679; 1888;
            (-17739)]
  let x = []
end

eval (List.length (M.x@M.y))  (* 11 *)
eval (List.fold_left (+) 0 (M.x@M.y))  (* 11 *)

Unrolling limits

Unrolling works by creating a symbolic call graph for the negation of the goal we’ve asked Imandra to verify (or dually the positive version of the goal in the case of instance), and by iteratively extending this graph with incremental interpretations of recursive functions, up to a given unrolling bound, checking at each step for satisfiability.

The unrolling bound defaults to 100 and can be controlled using the [@@upto <n>] attribute.

If at any step of the unrolling process the negation of our original goal is satisfiable w.r.t. the interpreted approximations of the recursive functions, then Imandra has found a counterexample for our original goal, which has thus been refuted. In this case, Imandra will report it.

If, on the other hand, Imandra is able to prove that there is no counterexample in a manner that is independent of the bound on the approximations, then our original goal is indeed a theorem valid for all possible inputs, and Imandra will report Proved. This can always be done for a wide class of theorems on catamorphisms (e.g., List.fold_right), for example.

Otherwise, if Imandra failed to find a counterexample or proof and stopped unrolling at the unrolling bound, we obtain a weaker result of the form Unknown (verified up to depth k), which effectively means: this may or may not be a theorem, but there are no counterexamples up to depth k. Such bounded results can nevertheless be very useful.

Let’s try to understand in practice how the unrolling bound plays into unrolling. Consider this simple function that recursively decreases an integer until it reaches 0, then returns 1:

let rec f x =
  if x <= 0 then
    1
  else
    f (x - 1)

Let’s verify that for all x < 99, the function will return 1:

verify (fun x -> x < 99 ==> f x = 1)

Proved.

But watch what happens if we ask Imandra to verify this for x < 100, thus exceding the number of recursive calls that Imandra unrolls by default:

verify (fun x -> x < 100 ==> f x = 1)

Validation failed:
(No_proof
   { err =
     Error{ Kind.name = "TacticEvalErr" }:
       Tactic failed: unroll failed to prove goal.
       Result is: (R_unknown { reason = "max number of steps (100) reached" });
     counter_model = None;
     subgoals =
     [
       |----------------------------------------------------------------------
        x < 100 ==> f x =<int> 1
       ];
     sub_anchor = None })

As expected, since the recursion depth needed to prove this exceeds the unrolling bound we set, Imandra could only prove this property up to bound k. This goal is in fact a property that is better suited for verification by induction (indeed, you might try adding the [@@by auto] annotation to the above goal to invoke the Imandra’s inductive waterfall and prove it).

As a minor note, if we reach a local unrolling depth instead of hitting the global one, Imandra will be a bit more positive in its message, telling us that the conjecture has been proved up to the number of steps we’ve specified instead of a weaker “Unknown”:

verify (fun x -> x < 100 ==> f x = 1) [@@upto 100]

Proved up to (N_steps 100).