Sliding admit verification style

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

Note: F★ is not guaranteed to return SMT failures in order! So, if you do:

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

then you SHALL NOT assume that your assert succeeded. That's precisely why you have to use the "sliding admit" technique.