FStar.Pure.Break: add a utility to "break away" the VC of the continuation

[mtzguido]

While stabilizing some queries in HACL*, I wrote something similar for the STATE effect

let break () : STATE unit (fun p h -> spinoff (squash (p () h))) = ()

This worked very well to cause a VC to be split at points chosen by the programmer, to make verification more stable. In my case:

let mk_bn_to_bytes_be #t is_known_len len b res =
  push_frame ();
  if is_known_len then begin
    [@inline_let] let numb = size (numbytes t) in
    [@inline_let] let bnLen = blocks len numb in
    [@inline_let] let tmpLen = numb *! bnLen in
    let tmp = create tmpLen (u8 0) in
    if tmpLen =. len then begin
      LowStar.Ignore.ignore tmp;
      bn_to_bytes_be_ bnLen b res end
    else begin
      break(); // !!!!!!
      bn_to_bytes_be_ bnLen b tmp;
      copy res (sub tmp (tmpLen -! len) len) end end
  else begin
    [@inline_let] let numb = size (numbytes t) in
    let bnLen = blocks len numb in
    let tmpLen = numb *! bnLen in
    let tmp = create tmpLen (u8 0) in
    bn_to_bytes_be_ bnLen b tmp;
    copy res (sub tmp (tmpLen -! len) len) end;
  pop_frame ()

That single break stabilizes this proof to pass --quake 10, with an rlimit of 50, while before it had an rlimit of 250 and was still flaky.

Now, I could just say that's a common pattern/trick and document it, but for Pure it is considerably harder to do because we need to prove monotonicity of the effect. This PR is my best attempt, with a small modification in Pervasives to expose that spinoff p is really equal to p.

The interface file is not really clean, but I don't know if I can do better... the postprocess_with is there to ensure that break_wp really is fun p -> spinoff (squash (p ())), so it shouldn't add any unexpected indirection or overhead.

[mtzguido]

tests/ide failing for some reason

{"kind":"response","query-id":"2.86","status":"failure","response":[{"level":"error","number":217,"message":"  - Tactic left uninstantiated unification variable ?208 of type Type0 (reason = \"flex-flex quasi:\tlhs=Instantiating implicit argument in application\trhs=apply arg\")\n","ranges":[{"fname":"FStar.Calc.fsti","beg":[91,52],"end":[91,62]}]}]}