Pulse re-typechecks postconditions of called functions

[gebner]

Pulse re-typechecks the postconditions of every function that is called. Aside from being a performance issue, this can also cause code to fail in unexpected ways:

// Some proposition that is trivially provable using an SMTPat from FStar.Seq.Base
let tru: prop = Seq.seq_to_list (Seq.seq_of_list ([42])) == [42]
let tru_intro () : Lemma tru = ()

let f (n: nat{tru}) : nat = 42

// The postcondition of `g` now typechecks only if we have facts from FStar.Seq.Base
```pulse
fn g () requires emp returns n:nat ensures pure (f n == 42) {
  42
}
```

#set-options "--using_facts_from '-FStar.Seq'"

let h' () = g () // works

```pulse
fn h () requires emp returns n:nat ensures emp {
  let n = g (); // fails because the *postcondition* of g no longer typechecks
  n
}
```

---

I ran into this issue when calling Pulse.Array.pts_to_range_split, whose postcondition contains a Seq.slice.

        i <= m /\ m <= j /\ j <= length a /\
        Seq.length s == j - i /\
        s1 == Seq.slice s 0 (m - i) /\
        s2 == Seq.slice s (m - i) (Seq.length s) /\
        s == Seq.append s1 s2

Weirdly enough, it started working again once I proved Seq.length s == j - i at the call site. (Even though that should be in scope for the precondition of Seq.slice since it's on the right side of the conjunction.)

[mtzguido]

I think this is coming from a combination of pure elimination + the fact that try_get_non_informative_witness re-typechecks its argument

val try_get_non_informative_witness (g:env) (u:universe) (t:term)
  : T.Tac (option (non_informative_t g u t))

val get_non_informative_witness (g:env) (u:universe) (t:term)
  : T.Tac (non_informative_t g u t)

since it does not take a proof of typing for t, try_get_non_informative just attempts to construct a "witnesser" for the type t, and then check it from scratch

let try_get_non_informative_witness g u t
  : T.Tac (option (non_informative_t g u t))
  = let eopt =
       [...]
    in
    match eopt with
    | None -> None
    | Some e ->
      let tok =
        check_term
          (push_context_no_range g "get_noninformative_witness")
          e
          T.E_Total
          (non_informative_witness_t u t)
      in
      Some tok

This is triggered on every lift from ghost to atomic. Also, since in this example we are calling a function returning a pure, an explicit elimination is inserted, i.e. a call to elim_pure_explicit (f n == 42):

val elim_pure_explicit (p:prop)
: stt_ghost (squash p) (pure p) (fun _ -> emp)

This means the lift is required, and also the fact that squash (f n == 42) is non-informative, which will go via the code above triggering a typechecking for f n again.

I think a fix would be to make try_get_non_informative_witness take a proof of typing for t. The lift should be able to get the derivation for the type from an inversion lemma.