Flychecking Pulse?

[JonasAlaif]

In the following snippet

open Pulse.Lib.Pervasives

```pulse
fn cond_lemma
  (#b: bool)
  (#x #y: vprop)
  requires (if b then x else y) ** (pure (not (b)))
  ensures  y
{
  ()
}

fn fold_pre
  (b: bool)
  (y: vprop)
  requires (if b then emp else y)
  ensures  (if b then emp else y)
{
  if not (b) {
    assert (pure (not (b)));
    cond_lemma #b #emp #y;
  } else {
    ()
  }
}
```pulse

I get the error

- Cannot prove:
    match b with
    | true -> emp
    | _ -> y
- In the context:
    emp

If I comment out the assert, the error goes away.

[mtzguido]

Making a note that this is an error from the flycheck: with verification enabled we do not get the error.

[gebner]

I can no longer reproduce this with the recent changes to the matcher. FWIW, the vscode extension now discards errors from the flycheck process if we've already checked the top-level definition using the main process, and errors from the flycheck process are shown as warnings.

[mtzguido]

This PR made this particular issue go away, but this one still shows a spurious error for me (flycheck fails on cond_lemma, normal mode fails on the assert):

```pulse
fn fold_pre
  (b: bool)
  (y: vprop)
  requires (if b then emp else y)
  ensures  (if b then emp else y)
{
  assert (pure False);
  if not (b) {
    assert (pure (not (b)));
    cond_lemma #b #emp #y;
  } else {
    ()
  }
}
```

let _ = assert False

I think FStarLang/FStar#3337 would solve it, at the cost of verifying the Pulse fragment twice (one for each process). Until we maybe add flychecking support to the Pulse checker as we discussed today.

Relabeling this issue.