Verification Conditions Bloat

[shaolintl]

Email from Nik:

A major source of worry in F* is that it produces VC terms that are
enormous. Often, this is the result of needless bloat, the result of
tweaking the VC generation endlessly, while testing on some random program.
The result is that even programs like:

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

produces a VC like this:

(pure_bind_wp .\test.fst(3,11-3,37) unit unit

(pure_bind_wp .\test.fst(3,23-3,37) Type unit

(pure_bind_wp .\test.fst(3,23-3,37) Type Type

(pure_bind_wp
.\test.fst(3,24-3,31) int Type

(pure_bind_wp
.\test.fst(3,24-3,31) int int

(pure_null_wp int)

(fun
uu___ ->

(pure_assume_p int

(eq2 uu___@0 (op_Subtraction 1 1))

(pure_return int uu___@0))))

(fun x ->
(pure_bind_wp .\test.fst(3,35-3,36) int Type

(pure_return int 0)

(fun y -> (pure_null_wp Type)))))

(fun uu___ -> (pure_assume_p Type

(eq2
uu___@0 (eq2 (op_Subtraction 1 1) 0))

(pure_return Type uu___@0))))

(fun p ->

(fun p ->

(l_and ( (eq2 (op_Subtraction 1 1) 0))

(l_Forall (fun x ->

(l_imp ((fun
uu___ -> (eq2 (op_Subtraction 1 1) 0)) x@0)

(p@1
x@0))))))))

(fun uu___ -> (pure_assume_p unit (eq2 uu___@0 (assert (eq2
(op_Subtraction 1 1) 0)))

(pure_return unit uu___@0))))

After normalization it gets simplified a little, but there is still a LOT of
bloat here.

It would be great if someone could build a catalog of small programs that
exercise a variety of F* features (basic assertions, assert_norm, match,
termination checks, refinement subtyping, sub-effecting, …).

A good catalog would first exercise each of these features in isolation, and
then also some of their combinations.

For each such program in this catalog, it would be great to have a
description of the kind of VC one would expect, in comparison with the kind
of VC that is actually generated.

For example, for this little program, I would hope to just generate the VC:

pure_assert_p unit (1 – 1 == 0) (pure_null_wp unit)

As we get more experience with it, we could also try to describe the reasons
(e.g., in terms of specific code fragments in the compiler) responsible for
introducing this bloat.

In a way, the fact that F* is able to perform the way it does even in the
presence of this bloat is kind of amazing to me. If it were tuned to
generate leaner, more minimalistic terms, I think we will likely see massive
performance boosts, both in F* itself and also in terms of what Z3
eventually needs to process.

[cpitclaudel]

It would be great if someone could build a catalog of small programs that
exercise a variety of F* features (basic assertions, assert_norm, match,
termination checks, refinement subtyping, sub-effecting, …).

Such a catalog would also form a nice collection of examples for F*'s docs.

[shaolintl]

The catalog will be generated in
https://github.com/FStarLang/FStar/wiki/Catalog-of-Verification-Conditions

[shaolintl]

In order to get the VC, run fstar with the --log_queries and look at the ;;;;;;;;;query string which marks the beginning of the query (after all of the context definitions).

[krpcannon]

Notes are on:
https://github.com/FStarLang/FStar/wiki/Optimizing-the-Generation-of-Verification-Conditions
Also, I am not able to reproduce Nik's exact result.

[aseemr]

This issue is quite open and with no plans towards addressing it. Closing it until we decide to revisit.