Support for predicate syntax in Pulse

[nikswamy]

I find it bothersome that we have two different syntaxes for vprops is Pulse.

When one writes a predicate (e.g., a representation predicate for some structure), one uses the the syntax of F*, e.g.,

let ha_val_core (core:ha_core) (h:hash_value_t)
  : vprop
  = A.pts_to core.acc full_perm (fst h) `star`
      exists_ (λ (n:U32.t) →
        pure (U32.v n == snd h) `star`
        pts_to core.ctr full_perm n)

Whereas, in Pulse itself, one would write this as

A.pts_to core.acc full_perm (fst h) **
exists (n:U32.t).
    pure (U32.v n == snd h) **
    pts_to core.ctr full_perm n

What do you think about a convention where all vprops in a Pulse program are written in Pulse-specific syntax.

For instance, rather than using an F* let for ha_val_core, one would write something like

predicate ha_val_core (core:ha_core) (h:hash_value_t) = 
  A.pts_to core.acc full_perm (fst h) **
  exists (n:U32.t).
    pure (U32.v n == snd h) **
    pts_to core.ctr full_perm n

which would elaborate to the original let ha_val_core.

I suppose, if at some point one wanted to write some F* lemmas about ha_val_core, one would eventually confront the fact that this is just an F* term for a vprop. But, if vprops relations are manipulated mainly in Pulse itself, using Pulse ghost functions rather than F* lemmas, then perhaps one wouldn't have to encounter the F* versions very often

[nikswamy]

The syntax of vprops in Pulse and F* now coincide.