Sliding admit verification style

One surprising aspect of F★ verification is that SMT verification errors are not reported in order. Consider a big function whose post-condition fails to verify. One natural reflex would be to insert an assert in the body of the function to perform some sanity checks.

val difficult_function: input -> o:output{conjunct1 i o /\ conjunct2 io}

let difficult_function i =
  ... stuff ...
  assert (something that should hold true here);
  ... more stuff ...

You may, at this stage, get an error that talks about the post-condition only. However, you SHALL NOT assume that your assert succeeded, because the underlying Z3 encoding does not preserve ordering of verification conditions. Instead, use the "sliding admit" technique.

The sliding admit trick

When faced with a big function with a difficult post-condition that itself may make multiple calls to other functions with pre-conditions the following is a somewhat interactive way to make incremental progress:

val difficult_function: input -> o:output{conjunct1 i o /\ conjunct2 io}

let difficult_function i =
  let t1 = function1 i in
  let t2 = function2 i t1 in
  ...

  let o = tn in
  o

Instead of searching through the whole function to determine which pre-condition or part of the post-condition is failing, you can put an admit what you believe would still succeed, e.g.,

let difficult_function i =
  let t1 = function1 i in
  admit()

If at that point you can already express parts of the post-condition, you can also express them using assert, e.g.,

let difficult_function i =
  let t1 = function1 i in
  assert(conjunct1 i t1);
  admit()

Moving your way forward by sliding the admit() down through the function. In the emacs fstar-mode you can achieve this having two new lines after the admit() and using C-c C-n.

JP: or, you put the cursor right after the admit() and use C-c C-<Enter>.

Pitfalls with using admits

Sometimes it is convenient to admit certain definitions in a program/proof while you work on the rest. For example, you could have

let f (x:t) : s = admit()
let g (x:t) : s * s = f x, f x

etc.

Don't do that, especially if f is a Pure or Ghost computation. If you do, then F* will encode this function to the SMT solver literally as let f x = Prims.admit(), which will allow you to later prove:

let f_is_constant (x y:t) : Lemma (f x == f y) = ()

Which is probably not what you wanted.

Instead, it is safer to use

assume
val f (x:t) : s
let g (x:t) = f x, f x

In this case, f is encoded to the SMT solver as an uninterpreted function, which is most likely what you really want.