Using SMT fuel and the normalizer

Using SMT fuel to control fixpoint unrolling

Consider the following program:

module Test

let l1 = [ 0 ]
let l3 = [ 0; 0; 0 ]
let l5 = [ 0; 0; 0; 0; 0 ]

let a1 =
  assert (FStar.List.length l1 = 1)

In order to prove the assertion, the following happens:

• the type list is encoded to z3
• the definition of length is also encoded to z3
• z3 finds a proof that makes the assertion succeed; in effect, this amounts to unfolding the definition of length at the level of the smt-solver (z3).

Naturally, the smt-solver should not infinitely expand definitions; therefore, F★, when encoding proof obligations to z3, includes a notion of "fuel", where each unfolding consumes a unit of fuel, and each inversion consumes a unit of _i_fuel.

For instance, the following will not succeed:

let a3 =
  assert (FStar.List.length (l1 @ l3 @ l5) = 9)

This is because z3 is not allowed to unfold at such a depth by default. If you really need to make the assertion above succeed, you can increase the amount of fuel as follows:

#set-options "--initial_fuel 10 --initial_ifuel 10"

let a3 =
  assert (FStar.List.length (l1 @ l3 @ l5) = 9)

#reset-options

Increasing the fuel is expensive: it means that z3 will explore more, deeper branches in the solving process, which can lead to increased verification times.

Using the F★ normalizer

Such proof obligations should be reduced directly by F★'s normalizer, which is a symbolic evaluator for F★ total terms. The assert_norm construct is the current way we expose this to the user, calling the normalizer before encoding the problem to the SMT solver:

  assert_norm (FStar.List.length (l1 @ l3 @ l5) = 9)

For finer grained control there is also a normalize_term construct that can appear at arbitrary positions in types. For instance, above we could tell F★ that normalization should only be applied to the LHS:

  assert (normalize_term (FStar.List.length (l1 @ l3 @ l5)) = 9)

This says if you can prove normalize_term (FStar.List.length (l1 @ l3 @ l5)) = 9 you can conclude the same thing. F* will normalize the left hand side and be left to prove 9 = 9, which is trivial. Now, if you want to conclude that FStar.List.length (l1 @ l3 @ l5) = 9, you can call the lemma normalize_term_spec (FStar.List.length (l1 @ l3 @ l5)) which establishes that FStar.List.length (l1 @ l3 @ l5) == normalize_term (FStar.List.length (l1 @ l3 @ l5)).