General recursion in Pulse

[nikswamy]

• Add support for Dv and general recursion in FStar.Reflection.Typing
• Add a typing rule for Pulse recursion targeting the Dv rule in reflection typing.

[mtzguido]

For Dv recursion, without any termination check, one possibility is having a rule like:

G, f : (a -> Dv b), x:a |- e : Dv b
------------------------------------ [Rec]
G |- (let rec f x = e in f) : a -> Dv b

i.e. the simple 1-argument Dv recursion rule, and use that to get n-ary recursion like this:

G, f : (a -> b -> c -> Dv d), x:a, y:b, z:c |- e : Dv d
-------------------------------------------------------------------- [Lam]
G, f : (a -> b -> c -> Dv d), x:a |- (fun y z -> e) : b -> c -> Dv d
-------------------------------------------------------------------- [Rec]
G |- (let rec f x = fun y z -> e) : a -> Dv (b -> c -> Dv d)

And then use eta expansion to turn this into a a -> b -> c -> Dv d.

[nikswamy]

@mtzguido has added support for general recursion in stt as well as recursion with termination checking for stt_ghost. We also have support for extraction of recursive definitions.

The approach involves introducing a Pulse definition with an additional argument for the recursively bound name and then relying on a regular F* definition to tie that knot. The code that actually ties the knot is admitted currently, but our most recent discussions around this is to expose for stt a pair of coercions as_dv (s:stt a p q) : unit -> Dv (stt' a p q) and from_dv: (unit -> Dv (stt' a p q) -> stt a p q for an abstract type stt'. This should allow us to tie the knot in the general recursion case without needing to prove termination.