Unrolling

Unrolling is ImandraX's bounded model checking engine. It works by systematically expanding recursive function definitions and checking satisfiability modulo ground decision procedures. Unrolling is completely automatic and excels at finding counterexamples.

How unrolling works

When you write verify (fun x -> P x), ImandraX negates the goal (looking for an x where P x is false) and creates a symbolic call graph. It then:

1. Incrementally unfolds recursive function calls, expanding them one level at a time
2. After each expansion, checks satisfiability modulo ground decision procedures (arithmetic, datatypes, congruence closure)
3. Uses reachability literals to track which function calls have been interpreted
4. Selects the next call to expand using unsat-core extraction for efficiency
5. Uses a fair selection strategy, ensuring all calls are eventually expanded

This refinement loop continues until one of three outcomes is reached.

Three possible outcomes

1. Counterexample found

When the solver finds a satisfying assignment to the negated goal, ImandraX reports a concrete counterexample:

verify (fun x -> x * x <> 144)
(* Counterexample (after 2 steps): x = 12 *)

The counterexample is a first-class value you can compute with — see Counterexamples.

2. Theorem proved

When ImandraX proves that no counterexample can exist (regardless of the unrolling bound), the property is established as a theorem:

verify (fun x -> x + 1 > x)
(* Theorem proved *)

This happens when the goal involves only non-recursive functions, algebraic datatypes, and arithmetic — cases where unrolling is complete.

3. Unknown (verified up to a bound)

When unrolling reaches its bound without finding a counterexample or proof, the result is "unknown":

verify (fun xs -> is_sorted xs ==> is_sorted (List.rev xs))
(* Unknown — verified up to depth 100 *)

This means no counterexample exists with inputs "up to depth 100" (roughly, lists up to length 100). To prove the property for all inputs, you need induction — see The Waterfall.

Completeness properties

Unrolling provides strong completeness guarantees for certain problem classes:

• Non-recursive functions + datatypes + linear arithmetic: Unrolling is complete — it will always prove or refute the goal in finite time.
• Recursive functions + datatypes + arithmetic: Unrolling is complete for counterexamples — if a counterexample exists, unrolling will eventually find it (given a large enough bound).

This makes unrolling an excellent first pass: run it before attempting induction. It frequently discovers edge cases that reveal apparently true conjectures are actually false.

Controlling the unrolling bound

The default bound is 100 recursive expansions. You can adjust it:

(* Increase the bound for a specific verification *)
verify ~upto:500 (fun xs -> some_property xs)

For a specific theorem or lemma, use the [@@timeout] attribute to control time rather than depth:

theorem my_theorem x y = deep_property x y
[@@by auto] [@@timeout 60]

Using unrolling as a tactic

The unroll tactic applies unrolling to the current goal within a larger proof:

theorem my_theorem x =
  some_property x
[@@by unroll 100]

Example: Coin change

Unrolling proves this theorem about making change with 3-cent and 5-cent coins completely automatically:

type pocket = {
  num_3s : int;
  num_5s : int;
}
 
let rec mk_change n =
  if n <= 7 then None
  else match n with
  | 8 -> Some { num_3s = 1; num_5s = 1 }
  | 9 -> Some { num_3s = 3; num_5s = 0 }
  | 10 -> Some { num_3s = 0; num_5s = 2 }
  | _ ->
    match mk_change (n - 3) with
    | Some p -> Some { num_3s = p.num_3s + 1; num_5s = p.num_5s }
    | None -> None
 
let eval_pocket = function
  | None -> 0
  | Some p -> 3 * p.num_3s + 5 * p.num_5s
 
theorem coin_completeness n =
  n >= 8 ==> eval_pocket (mk_change n) = n
[@@by auto]

ImandraX proves this using induction with the waterfall, but unrolling plays a key role in checking base cases and validating intermediate steps.

When to use unrolling

• First pass on any conjecture — Let unrolling find counterexamples before you invest effort in a proof
• Non-inductive properties — Properties that don't require induction are often proved by unrolling alone
• Validation — Use unrolling to sanity-check goals before and during induction
• Finding instances — The instance command is powered by unrolling