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>.