Improve declaration of implicit binders, and implicit inference for stateful applications about steel HOT 4 CLOSED

Inference of implicit binders

Today, we write:

fn test_read (r:ref U32.t)
             (#n:erased U32.t)
             (#p:perm)
   requires pts_to r p n
   returns x : U32.t
   ensures pts_to r p x

Instead, I propose we write

fn test_read (r:ref U32.t)
   requires pts_to r p 'n
   returns x : U32.t
   ensures pts_to r p x

Note the variables p and 'n are not bound.

• p is an implicitly bound variable
• 'n is an implicitly bound variable of erased type

The goal is to figure out the types of p and 'n and to add
binders for them.

We can do this by generated the type:

r:ref U32.t ->
#p:_ ->
#'n:erased _ ->
stt U32.t (pts_to r p n) (fun x -> pts_to r p x)

getting F* to typecheck the term, filling in the holes. We can
then read it back in the Pulse checker.

It should be possible to mix this with user annotated types. So, one could write something like this too:

fn read_nonzero (r:ref U32.t) (n:erased U32.t { n <> 0 })
   requires pts_to r p n
   returns x : U32.t
   ensures pts_to r p x

DONE

from steel.

Done (#120)

Inference of implicit instantiations

We already solve implicit arguments using the prover to find solutions to existentials. But, this currently relies on the order of implicit binders. We should remove this restriction.

Given an application term e (say f e1 #e2 e3), potentially with some user-annotated implicit instantiations, we have to find the rest.

We ask F* to (lax) check and elaborate e. F* would produce back a term f #t #?u1 e1 #e2 e3 ?u2 etc., where some implicits have been solved, but ?u1 and ?u2 have not been solved yet.

The Pulse checker reads back this term, replacing the unsolved uvars with fresh existential variables and then calls the prover to instantiate them with respect to the current vprop context, as it does today.

from steel.

Make handling of stateful application less syntactic

Currently, we rely on the front-end desugaring to identify stateful application and mark them as such in the AST.

While this works for handling application of top-level functions, it is not properly type-directed, leading to other uses to be awkward to work with, e.g., at higher order, see below.

Instead, let's not rely on the front-end to distinguish stateful applications. Rather, the Pulse typechecker can handle this itself, but computing the type of an application (using F*), then seeing if the computed type is an stt (and if so, instantiating implicit arguments as above), and then computing frames; otherwise handling it as a pure application.

module Test.HigherOrder
open Pulse.Lib.Pervasives

[@@expect_failure]

fn apply (#a:Type0) (#b:Type0) (f:  (a -> stt b emp (fun _ -> emp))) (x:a)
  requires emp
    returns y:b
    ensures emp
{
    f x;
}

let perform (#a:Type0) (#b:Type0) (f: (a -> stt b emp (fun _ -> emp))) (x:a) : stt b emp (fun _ -> emp)=
f x

fn apply (#a:Type0) (#b:Type0) (f:  (a -> stt b emp (fun _ -> emp))) (x:a)
    requires emp
    returns y:b
    ensures emp
{
    perform f x;
}

from steel.

Marking it complete.

from steel.