Support for close combinator for indexed effects

[aseemr]

This PR adds support for a close combinator for indexed effects.

Why

With some profiling of F* performance on the Pulse checker, we found that F* was creating huge VCs for relatively small TAC functions, resulting in high memory usage and typechecking time.

Adding general support for close combinators for indexed effects, and defining one for TAC, significantly improves the memory consumption and time taken by F* on Pulse checker---upto ~9x memory and ~19x time in some cases.

What does close mean in the context?

Consider typechecking a match expression in F*:

match e1 with
| C x -> e

where x occurs free in e.

To typecheck the branch, F* opens e with x and computes a computation type M a is for it, where is are the effect indices. To compose the computation type with the rest of the function, F* has to ensure that x does not escape ... i.e. weaken M a is so that x does not occur free in the weakened type.

For the result type a, F* ensures this by just checking that x is not free in a, if it is, F* gives an error.

For the effect indices is, F* uses a closing mechanism.

Closing in wp effects

For primitive wp effects, the effect definition defines a close combinator. For example, for the PURE effect, the combinator is defined as follows:

let close (a b:Type) (wp:b -> pure_wp a) : pure_wp a = fun post -> forall (x:b). wp x

When the branch has a primitive wp effect, F* uses such an associated close combinator to close the branch.

Closing in indexed effects

For indexed effects, so far we were following a different approach. Instead of the effect defining a close combinator, we used projector functions applied to the scrutinee to substitute the pattern bound variables.

In the match expression above, for example, in the indices is we substitute x by C? e.

This design was chosen in part to ensure that effect writers provide as few combinators as possible to get the effect going.

The problem

The following code in F*

let (| x, y, z |) = e in
e1

is simply a sugar for:

let r = e in
match r with
| MkTuple3 x y z -> e1

The Pulse checker code is heavily using dependent tuples and pattern matching like this.

When closing x, y, and z in this example, F* substitutes x, for example, by MkTuple3?._1 r. But this is not the whole story: it is actually MkTuple3?._1 #t1 #t2 #t3 r, where t1, t2, and t3 are implicits for the type parameters. For dependent tuples, these implicits are lambda terms (for t2 and t3).

On inspecting the VCs, we found that the bulk of the VC was these projector expressions, with implicits repeated everywhere. This results in huge VCs, high memory consumption, and high cost of passes over the VC.

Support for close combinators for indexed effects

To get around this problem, the PR adds support for custom close combinators for indexed effects, and defines one for TAC:

let tac_close (a b:Type) (wp_f:b -> tac_wp_t a) (f:(x:b -> tac_repr a (wp_f x))) =
  tac_repr a (fun ps post -> forall (x:b). wp_f x ps post)

So now the MkTuple3 example above would result in a VC like forall (x:t1) (y:t2) (z:t3). MkTuple3 #t1 #t2 #t3 x y z == r ==> ... , and thus no duplication in the rest of the VC.

Impact on the Pulse checker

For 3 of the slowest files, memory consumption and time taken (in MB and seconds resp.):

	Memory before	Memory after	Time before	Time after
Pulse.Checker.Bind	6601	743	118.86	6.51
Pulse.Checker.If	3062	774	48.66	7.28
Pulse.Checker.While	2332	838	40.91	9.10

The linear regression slope comparing times 0.27 and memory consumption 0.13.

(Using the runlim scripts and with admit smt queries.)

Mechanics of the close combinator

The wiki page https://github.com/FStarLang/FStar/wiki/Indexed-effects describes how close combinators can be defined.

Combinator shape

The shape of a close combinator looks like:

val close (a b:Type) (is:b -> is_t) (f:(x:a -> M a (is x)) : Type

and the body of the combinator is of the form repr a js, where js are the closed indices.

Combinator soundness

F* checks the soundness of the combinator by checking that:

a:Type, b:Type, (is:b -> is_t), x:b |- subcomp (repr a (is x)) (repr a js)

I.e., forall (x:b), the indices js are a weakening of is x, where the weakening is defined by the effect subcomp combinator.

Applying the combinator

This is a small tweak in existing code for typechecking match. When the branch effect is a primitive wp effect, or an indexed effect with custom close combinator, then we use the combinator to close, else fallback to the substitution-based closing.