Optimizing the Generation of Verification Conditions

Overview

F* generates unnecessary VC. This page will try to summarize these cases on simple examples per issue 966.

Given the program

let test = assert ((1 - 1) == 0)

it translates to the VC is Bloat1

For:

let test = assert (normalize_term (length ([0] @ [0] @ [0; 0])) = 4)

we have VC

Given the program:

let test x = match x with
| [] -> 0
| x::xs -> 1

The generated VCs are Bloat2

Given the program:

let test x = if (x > 0) then 1 else -1

The generated VCs are Bloat4

The classical factorial total function

let nat = x:int{x>=0}

val factorial: nat -> Tot nat

let rec factorial n =
        if n = 0 then 1 else Prims.op_Multiply n (factorial (n - 1))

generates this VC query, and this one without type annotation.

For:

val incr : r:ref int -> St unit

let incr r = r := !r + 1

We have VC