using exists*; before simplifying Pulse parser for vprop

Steel.fst.config.json

@@ -19,7 +19,7 @@
     "share/steel/examples/pulse/dice/l0",
     "share/steel/examples/pulse/dice/engine",
     "share/steel/examples/pulse/dice/common",
-    "share/steel/examples/pulse/dice/cbor"
-
+    "share/steel/examples/pulse/dice/cbor",
+    "share/steel/examples/pulse/_output/cache"
   ]
 }

lib/steel/pulse/Pulse.Reflection.Util.fst

@@ -80,8 +80,8 @@ let mk_star (l r:R.term) : R.term =
   pack_ln (Tv_App t (r, Q_Explicit))
 
 let pure_lid = mk_pulse_lib_core_lid "pure"
-let exists_lid = mk_pulse_lib_core_lid "exists_"
-let forall_lid = mk_pulse_lib_core_lid "forall_"
+let exists_lid = mk_pulse_lib_core_lid "op_exists_Star"
+let forall_lid = mk_pulse_lib_core_lid "op_forall_Star"
 let args_of (tms:list R.term) =
   List.Tot.map (fun x -> x, R.Q_Explicit) tms
 

share/steel/examples/pulse/AuxPredicate.fst

@@ -10,10 +10,10 @@ module R = Pulse.Lib.Reference
 // Defining a vprop using F* syntax. We do not yet allow
 // writing Pulse syntax for vprops in predicates 
 let my_inv (b:bool) (r:R.ref int) : vprop
-  = exists_ (fun v -> 
+  = exists* v.
       R.pts_to r v ** 
       pure ( (v==0 \/ v == 1) /\ b == (v = 0) )
-    )
+
 
 
 ```pulse

share/steel/examples/pulse/GhostStateMachine.fst

@@ -56,11 +56,10 @@ noeq
 type locked_state_t = 
 { h:handle_t; 
   ph:pure_handle_t; 
-  lk:lock (exists_ (fun s ->
-      exists_ (fun ps -> 
+  lk:lock (exists* s ps. 
           handle_has_state h s **
           pure_handle_has_state ph ps **
-          pure (states_correspond s ps))));}
+          pure (states_correspond s ps));}
 let mk_locked_st h ph lk = {h; ph; lk;}
 
 assume
@@ -87,11 +86,10 @@ fn init' ()
   fold pure_handle_has_state ph Init;
   fold handle_has_state h CInit;
 
-  let lk = new_lock (exists_ (fun s ->
-                     exists_ (fun ps -> 
+  let lk = new_lock (exists* s ps.
                         handle_has_state h s **
                         pure_handle_has_state ph ps **
-                        pure (states_correspond s ps))));
+                        pure (states_correspond s ps));
 
   let locked_st = mk_locked_st h ph lk;
   rewrite (pure_handle_has_state ph Init)

share/steel/examples/pulse/QuicksortParallel.fst

@@ -120,10 +120,12 @@ let op_Array_Assignment
   (#s0: Ghost.erased (Seq.seq t))
 : stt unit
     (requires A.pts_to_range a l r s0)
-    (ensures fun _ -> (exists_ (fun s -> A.pts_to_range a l r s **
-    pure(
-      Seq.length s0 == r - l /\ s == Seq.upd s0 (SZ.v i - l) v
-    ))))
+    (ensures fun _ -> 
+      exists* s.
+        A.pts_to_range a l r s **
+        pure(
+          Seq.length s0 == r - l /\ s == Seq.upd s0 (SZ.v i - l) v
+        ))
 = pts_to_range_upd a i v #l #r
 
 (** Partitioning **)

share/steel/examples/pulse/ZetaHashAccumulator.fst

@@ -195,7 +195,7 @@ let mk_ha_core acc ctr = { acc; ctr }
 let ha_val_core (core:ha_core) (h:hash_value_t) 
   : vprop
   = A.pts_to core.acc (fst h) **
-    exists_ (λ (n:U32.t) →
+    (exists* (n:U32.t).
       pure (U32.v n == snd h) **
       pts_to core.ctr n)
 
@@ -252,7 +252,7 @@ let mk_ha core tmp dummy = { core; tmp; dummy }
 // A representation predicate for ha, encapsulating an ha_val_core
 let ha_val (h:ha) (s:hash_value_t) =
   ha_val_core h.core s **
-  exists_ (fun (s:Seq.lseq U8.t 32) -> A.pts_to h.tmp s) **
+  (exists* (s:Seq.lseq U8.t 32). A.pts_to h.tmp s) **
   A.pts_to h.dummy (Seq.create 1 0uy)
 
 // A ghost function to package up a ha_val predicate

share/steel/examples/pulse/bug-reports/Bug.SpinLock.fst

@@ -3,12 +3,16 @@ open Pulse.Lib.Pervasives
 module R = Pulse.Lib.Reference
 open Pulse.Lib.SpinLock
 
+let test_fstar (r:R.ref int) =
+  let my_lock = new_lock (exists* v. R.pts_to r v) in
+  ()
+
 ```pulse
 fn lock_ref (r:R.ref int) (#v_:Ghost.erased int)
   requires R.pts_to r v_
   ensures emp
 {
-  let my_lock = new_lock (exists_ (fun v -> R.pts_to r v));
+  let my_lock = new_lock (exists* v. R.pts_to r v);
   ()
 }
 ```
@@ -20,7 +24,7 @@ fn create_and_lock_ref ()
   ensures emp
 {
   let mut r = 0;
-  let my_lock = new_lock (exists_ (fun v -> R.pts_to r v));
+  let my_lock = new_lock (exists* v. R.pts_to r v);
   ()
 }
 ```

share/steel/examples/pulse/bug-reports/DependentTuples.fst

@@ -3,7 +3,7 @@ open Pulse.Lib.Pervasives
 open Pulse.Lib.Reference
 open Pulse.Lib.SpinLock
 
-let exists_n (r:ref nat) : vprop = exists_ (fun n -> pts_to r n)
+let exists_n (r:ref nat) : vprop = exists* n. pts_to r n
 
 type tup_t = r:ref nat & lock (exists_n r)
 let mk_tup r lk : tup_t = (| r, lk |)
@@ -24,7 +24,7 @@ fn tuple ()
   unfold exists_n global_tup._1;  // this unfold affects the type of the dependent 
                                   // tuple, so we lost syntactic equality and the 
                                   // following assertion fails
-  assert (exists_ (fun n -> pts_to global_tup._1 n));
+  assert (`@(exists* n. pts_to global_tup._1 n));
   admit()
 }
 ```
@@ -47,7 +47,7 @@ fn record ()
   acquire global_rec.lk;
   assert (exists_n global_rec.r);
   unfold exists_n global_rec.r;
-  assert (exists_ (fun n -> pts_to global_rec.r n));
+  assert (exists n. pts_to global_rec.r n);
   admit()
 }
 ```

share/steel/examples/pulse/bug-reports/IntroGhost.fst

@@ -9,10 +9,10 @@ module R = Pulse.Lib.Reference
   var outside the loop is not ghost
 *)
 let my_inv (b:bool) (r:R.ref int) : vprop
-  = exists_ (fun v -> 
+  = exists* v.
       R.pts_to r v ** 
       pure ( b == (v = 0) )
-    )
+
 
 [@@expect_failure]
 ```pulse

share/steel/examples/pulse/dice/cbor/CBOR.Pulse.Extern.fsti

@@ -106,13 +106,13 @@ let cbor_read_success_post
   (va: Ghost.erased (Seq.seq U8.t))
   (c: cbor_read_t)
 : Tot vprop
-= exists_ (fun v -> exists_ (fun rem ->
+= exists* v rem.
     raw_data_item_match full_perm c.cbor_read_payload v **
     A.pts_to c.cbor_read_remainder #p rem **
     ((raw_data_item_match full_perm c.cbor_read_payload v ** A.pts_to c.cbor_read_remainder #p rem) @==>
       A.pts_to a #p va) **
     pure (cbor_read_success_postcond va c v rem)
-  ))
+
 
 noextract
 let cbor_read_error_postcond
@@ -164,7 +164,7 @@ let cbor_read_deterministically_encoded_success_post
   (va: Ghost.erased (Seq.seq U8.t))
   (c: cbor_read_t)
 : Tot vprop
-= exists_ (fun v -> exists_ (fun rem ->
+= ((exists* v rem.
     raw_data_item_match full_perm c.cbor_read_payload v **
     A.pts_to c.cbor_read_remainder #p rem **
     ((raw_data_item_match full_perm c.cbor_read_payload v ** A.pts_to c.cbor_read_remainder #p rem) @==>
@@ -264,11 +264,11 @@ val cbor_destr_string
     (raw_data_item_match p c (Ghost.reveal va) ** pure (
       Cbor.String? va
     ))
-    (fun c' -> exists_ (fun vc' -> exists_ (fun p'->
+    (fun c' -> exists* vc' p'.
       A.pts_to c'.cbor_string_payload #p' vc' **
       (A.pts_to c'.cbor_string_payload #p' vc' @==> raw_data_item_match p c (Ghost.reveal va)) **
       pure (cbor_destr_string_post va c'  vc'
-    ))))
+    ))
 
 val cbor_constr_string
   (typ: Cbor.major_type_byte_string_or_text_string)
@@ -280,14 +280,14 @@ val cbor_constr_string
     (A.pts_to a #p va ** pure (
       U64.v len == Seq.length va
     ))
-    (fun c' -> exists_ (fun vc' ->
+    (fun c' -> exists* vc'.
       raw_data_item_match full_perm c' vc' **
       (raw_data_item_match full_perm c' vc' @==>
         A.pts_to a #p va
       ) ** pure (
       U64.v len == Seq.length va /\
       vc' == Cbor.String typ va
-    )))
+    ))
 
 val cbor_constr_array
   (a: A.array cbor)
@@ -300,15 +300,15 @@ val cbor_constr_array
       pure (
         U64.v len == List.Tot.length v'
     ))
-    (fun res -> exists_ (fun vres ->
+    (fun res -> exists* vres.
       raw_data_item_match full_perm res vres **
       (raw_data_item_match full_perm res vres @==>
         (A.pts_to a c' **
           raw_data_item_array_match full_perm c' v')
       ) ** pure (
       U64.v len == List.Tot.length v' /\
       vres == Cbor.Array v'
-    )))
+    ))
 
 let maybe_cbor_array
   (v: Cbor.raw_data_item)
@@ -340,15 +340,15 @@ val cbor_array_index
       Cbor.Array? v /\
       SZ.v i < List.Tot.length (Cbor.Array?.v v)
     ))
-    (fun a' -> exists_ (fun va' ->
+    (fun a' -> exists* va'.
       raw_data_item_match p a' va' **
       (raw_data_item_match p a' va' @==>
         raw_data_item_match p a v) **
       pure (
         Cbor.Array? v /\
         SZ.v i < List.Tot.length (Cbor.Array?.v v) /\
         va' == List.Tot.index (Cbor.Array?.v v) (SZ.v i)
-    )))
+    ))
 
 val cbor_dummy_array_iterator: cbor_array_iterator_t
 
@@ -364,14 +364,14 @@ val cbor_array_iterator_init
   (#v: Ghost.erased Cbor.raw_data_item)
 : stt cbor_array_iterator_t
     (raw_data_item_match p a v)
-    (fun i -> exists_ (fun vi ->
+    (fun i -> exists* vi.
       cbor_array_iterator_match p i vi **
       (cbor_array_iterator_match p i vi @==>
         raw_data_item_match p a v) **
       pure (
         Cbor.Array? v /\
         vi == Cbor.Array?.v v
-    )))
+    ))
 
 val cbor_array_iterator_is_done
   (i: cbor_array_iterator_t)
@@ -392,7 +392,7 @@ val cbor_array_iterator_next
     (R.pts_to pi i ** cbor_array_iterator_match p i l **
       pure (Cons? l)
     )
-    (fun c -> exists_ (fun i' -> exists_ (fun vc -> exists_ (fun vi' ->
+    (fun c -> exists* i' vc vi'.
       R.pts_to pi i' **
       raw_data_item_match p c vc **
       cbor_array_iterator_match p i' vi' **
@@ -401,7 +401,7 @@ val cbor_array_iterator_next
         cbor_array_iterator_match p i l
       ) ** pure (
       Ghost.reveal l == vc :: vi'
-    )))))
+    ))
 
 val cbor_read_array
   (a: cbor)
@@ -419,18 +419,18 @@ val cbor_read_array
           U64.v len == List.Tot.length (Cbor.Array?.v v)
         )
     ))
-    (fun res -> exists_ (fun vres ->
+    (fun res -> exists* vres.
       A.pts_to res vres **
       raw_data_item_array_match p vres (maybe_cbor_array v) **
       ((A.pts_to res vres **
         raw_data_item_array_match p vres (maybe_cbor_array v)) @==> (
         raw_data_item_match p a v **
-        (exists_ (A.pts_to dest #full_perm))
+        (exists* _x. (A.pts_to dest #full_perm _x))
       )) ** pure (
       Cbor.Array? v /\
       U64.v len == A.length dest /\
       U64.v len == A.length res
-    )))
+    ))
 
 let maybe_cbor_tagged_tag
   (v: Cbor.raw_data_item)
@@ -500,15 +500,15 @@ val cbor_constr_map
       pure (
         U64.v len == List.Tot.length v'
     ))
-    (fun res -> exists_ (fun vres ->
+    (fun res -> exists* vres.
       raw_data_item_match full_perm res vres **
       (raw_data_item_match full_perm res vres @==>
         (A.pts_to a c' **
           raw_data_item_map_match full_perm c' v')
       ) ** pure (
       U64.v len == List.Tot.length v' /\
       vres == Cbor.Map v'
-    )))
+    ))
 
 val cbor_map_length
   (a: cbor)
@@ -537,15 +537,15 @@ val cbor_map_iterator_init
   (#v: Ghost.erased Cbor.raw_data_item)
 : stt cbor_map_iterator_t
     (raw_data_item_match p a v ** pure (Cbor.Map? v))
-    (fun i -> exists_ (fun l ->
+    (fun i -> exists* l.
       cbor_map_iterator_match p i l **
       (cbor_map_iterator_match p i l @==>
         raw_data_item_match p a v) **
       pure (
         Cbor.Map? v /\
         l == Cbor.Map?.v v
       )
-    ))
+    )
 
 val cbor_map_iterator_is_done
   (i: cbor_map_iterator_t)
@@ -562,7 +562,7 @@ val cbor_map_iterator_next
   (#i: Ghost.erased cbor_map_iterator_t)
 : stt cbor_map_entry
     (pts_to pi i ** cbor_map_iterator_match p i l ** pure (Cons? l))
-    (fun c -> exists_ (fun i' -> exists_ (fun vc -> exists_ (fun l' ->
+    (fun c -> exists* i' vc l'.
       pts_to pi i' **
       raw_data_item_map_entry_match p c vc **
       cbor_map_iterator_match p i' l' **
@@ -571,7 +571,7 @@ val cbor_map_iterator_next
         cbor_map_iterator_match p i l
       ) **
       pure (Ghost.reveal l == vc :: l')
-    )))))
+    ))
 
 val cbor_get_major_type
   (a: cbor)
@@ -651,7 +651,7 @@ val cbor_write
     ))
     (fun res -> 
       raw_data_item_match p c (Ghost.reveal va) **
-      exists_ (cbor_write_post va c vout out res)
+      (exists* _x. cbor_write_post va c vout out res _x)
     )
 
 val cbor_gather