Revising the syntax of vprops in Pulse

Steel.fst.config.json

@@ -19,7 +19,6 @@
     "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/_output/cache"
+    "share/steel/examples/pulse/dice/cbor"
   ]
 }

share/steel/examples/pulse/ArrayTests.fst

@@ -24,7 +24,7 @@ fn compare (#t:eqtype) (#p1 #p2:perm) (l:US.t) (#s1 #s2:elseq t l) (a1 a2:A.larr
 {
   let mut i = 0sz;
   while (let vi = !i; if US.(vi <^ l) { let v1 = a1.(vi); let v2 = a2.(vi); (v1 = v2) } else { false } )
-  invariant b. exists (vi:US.t). ( 
+  invariant b. exists* (vi:US.t). ( 
     R.pts_to i vi **
     A.pts_to a1 #p1 s1 **
     A.pts_to a2 #p2 s2 **
@@ -50,14 +50,14 @@ fn fill_array (#t:Type0) (l:US.t) (a:(a:A.array t{ US.v l == A.length a })) (v:t
               (#s:(s:Ghost.erased (Seq.seq t) { Seq.length s == US.v l }))
    requires (A.pts_to a s)
    ensures 
-      exists (s:Seq.seq t). (
+      exists* (s:Seq.seq t). (
          A.pts_to a s **
          pure (s `Seq.equal` Seq.create (US.v l) v)
       )
 {
    let mut i = 0sz;
    while (let vi = !i; US.(vi <^ l))
-   invariant b. exists (s:Seq.seq t) (vi:US.t). (
+   invariant b. exists* (s:Seq.seq t) (vi:US.t). (
       A.pts_to a s **
       R.pts_to i vi **
       pure ((b == US.(vi <^ l)) /\
@@ -270,7 +270,7 @@ fn sort3 (a:array U32.t)
          (#s:(s:Ghost.erased (Seq.seq U32.t) {Seq.length s == 3}))
    requires (A.pts_to a s)
    ensures 
-      exists s'. (
+      exists* s'. (
          A.pts_to a s' **
          pure (sorted s s')
       )
@@ -330,7 +330,7 @@ fn sort3_alt (a:array U32.t)
              (#s:(s:Ghost.erased (Seq.seq U32.t) {Seq.length s == 3}))
    requires (A.pts_to a s)
    ensures 
-      exists s'. (
+      exists* s'. (
          A.pts_to a s' **
          pure (sorted s s')
       )
@@ -435,7 +435,7 @@ fn test_array_swap
   (#s: Ghost.erased (Seq.seq U32.t))
 requires
   A.pts_to a s ** pure (A.length a == 2)
-ensures exists s' .
+ensures exists* s' .
   A.pts_to a s'
 {
   A.pts_to_len a;

share/steel/examples/pulse/Assert.fst

@@ -7,10 +7,10 @@ fn test_assert (r0 r1: ref nat)
                (#v0:nat)
     requires 
         pts_to r0 #p0 v0 **
-        (exists v1. pts_to r1 #p1 v1)
+        (exists* v1. pts_to r1 #p1 v1)
     ensures
         pts_to r0 #p0 v0 **
-        (exists v1. pts_to r1 #p1 v1)
+        (exists* v1. pts_to r1 #p1 v1)
 {
     //assert_ (pts_to r1 ?p1 ?v1); would be nice to have a version that also binds witnesses
     assert_ (pts_to r0 #p0 (v0 + 0));

share/steel/examples/pulse/AuxPredicate.fst

@@ -82,7 +82,7 @@ fn invar_introduces_ghost_alt (r:R.ref int)
 
   while (let vr = !r; (vr = 0))
   invariant b. 
-    exists v.
+    exists* v.
       R.pts_to r v **
       pure ( (v==0 \/ v == 1) /\ b == (v = 0) )
   {
@@ -96,13 +96,13 @@ fn invar_introduces_ghost_alt (r:R.ref int)
 ```pulse
 fn exists_introduces_ghost (r:R.ref int)
   requires R.pts_to r 0
-  ensures exists v. R.pts_to r v ** pure (v == 0 \/ v == 1)
+  ensures exists* v. R.pts_to r v ** pure (v == 0 \/ v == 1)
 {
   r := 0;
 
   fold (my_inv true r);
 
-  introduce exists b. (my_inv b r) with _; 
+  introduce exists* b. (my_inv b r) with _; 
   // once you hide the witness in the existential
   // you lose knowledge about it, i.e., we do not know that r = 0
   with b. unfold (my_inv b r)

share/steel/examples/pulse/CustomSyntax.fst

@@ -127,11 +127,11 @@ fn if_example (r:ref U32.t)
 ghost
 fn elim_intro_exists2 (r:ref U32.t)
    requires 
-     exists n. pts_to r n
+     exists* n. pts_to r n
    ensures 
-     exists n. pts_to r n
+     exists* n. pts_to r n
 {
-  introduce exists n. pts_to r n with _
+  introduce exists* n. pts_to r n with _
 }
 ```
 
@@ -144,15 +144,15 @@ val read_pred () (#b:erased bool)
 ```pulse
 fn while_test_alt (r:ref U32.t)
   requires 
-    exists b n.
+    exists* b n.
       (pts_to r n  **
        pred b)
   ensures 
-    exists n. (pts_to r n  **
+    exists* n. (pts_to r n  **
               pred false)
 {
   while (read_pred ())
-  invariant b . exists n. (pts_to r n  ** pred b)
+  invariant b . exists* n. (pts_to r n  ** pred b)
   {
     ()
   }
@@ -162,8 +162,8 @@ fn while_test_alt (r:ref U32.t)
 ```pulse
 fn infer_read_ex (r:ref U32.t)
   requires
-    exists n. pts_to r n
-  ensures exists n. pts_to r n
+    exists* n. pts_to r n
+  ensures exists* n. pts_to r n
 {
   let x = !r;
   ()
@@ -173,13 +173,13 @@ fn infer_read_ex (r:ref U32.t)
 
 ```pulse
 fn while_count2 (r:ref U32.t)
-  requires exists (n:U32.t). (pts_to r n)
+  requires exists* (n:U32.t). (pts_to r n)
   ensures (pts_to r 10ul)
 {
   open FStar.UInt32;
   while (let x = !r; (x <> 10ul))
   invariant b. 
-    exists n. (pts_to r n  **
+    exists* n. (pts_to r n  **
           pure (b == (n <> 10ul)))
   {
     let x = !r;
@@ -255,7 +255,7 @@ fn count_local (r:ref int) (n:int)
   let mut i = 0;
   while
     (let m = !i; (m <> n))
-  invariant b. exists m. 
+  invariant b. exists* m. 
     (pts_to i m  **
      pure (b == (m <> n)))
   {
@@ -277,20 +277,20 @@ let zero : nat = 0
 
 ```pulse
 fn sum (r:ref nat) (n:nat)
-   requires exists i. (pts_to r i)
+   requires exists* i. (pts_to r i)
    ensures (pts_to r (sum_spec n))
 {
    let mut i = zero;
    let mut sum = zero;
-   introduce exists b m s. (
+   introduce exists* b m s. (
      pts_to i m  **
      pts_to sum s  **
      pure (s == sum_spec m /\
            b == (m <> n)))
    with (zero <> n);
 
    while (let m = !i; (m <> n))
-   invariant b . exists m s. (
+   invariant b . exists* m s. (
      pts_to i m  **
      pts_to sum s  **
      pure (s == sum_spec m /\
@@ -300,7 +300,7 @@ fn sum (r:ref nat) (n:nat)
      let s = !sum;
      i := (m + 1);
      sum := s + m + 1;
-     introduce exists b m s. (
+     introduce exists* b m s. (
        pts_to i m  **
        pts_to sum s  **
        pure (s == sum_spec m /\
@@ -309,22 +309,22 @@ fn sum (r:ref nat) (n:nat)
    };
    let s = !sum;
    r := s;
-   introduce exists m. (pts_to i m) 
+   introduce exists* m. (pts_to i m) 
    with _;
-   introduce exists s. (pts_to sum s)
+   introduce exists* s. (pts_to sum s)
    with _
 }
 ```
 
 ```pulse
 fn sum2 (r:ref nat) (n:nat)
-   requires exists i. pts_to r i
+   requires exists* i. pts_to r i
    ensures pts_to r (sum_spec n)
 {
    let mut i = zero;
    let mut sum = zero;
    while (let m = !i; (m <> n))
-   invariant b . exists m s.
+   invariant b . exists* m s.
      pts_to i m  **
      pts_to sum s **
      pure (s == sum_spec m /\ b == (m <> n))
@@ -343,16 +343,16 @@ fn sum2 (r:ref nat) (n:nat)
 
 ```pulse
 fn if_then_else_in_specs (r:ref U32.t)
-  requires `@(if true
+  requires (if true
               then pts_to r 0ul
               else pts_to r 1ul)
-  ensures  `@(if true
+  ensures  (if true
               then pts_to r 1ul
               else pts_to r 0ul)
 {
   // need this for typechecking !r on the next line,
   //   with inference of implicits
-  rewrite `@(if true then pts_to r 0ul else pts_to r 1ul)
+  rewrite (if true then pts_to r 0ul else pts_to r 1ul)
        as (pts_to r 0ul);
   let x = !r;
   r := U32.add x 1ul

share/steel/examples/pulse/Demo.MultiplyByRepeatedAddition.fst

@@ -21,7 +21,7 @@ fn mult (x y:nat)
     let mut acc = 0;
     while ((ctr < x))
     invariant b.
-    exists c a.
+    exists* c a.
         pts_to ctr c **
         pts_to acc a **
         pure (a == (c * y) /\
@@ -48,7 +48,7 @@ fn mult32 (x y:U32.t)
     let mut acc = 0ul;
     while ((ctr < x))
     invariant b.
-    exists c a.
+    exists* c a.
         pts_to ctr c **
         pts_to acc a **
         pure (c <= x /\
@@ -75,7 +75,7 @@ fn mult32' (x y:U32.t)
     let mut acc = 0ul;
     while ((ctr <^ x))
     invariant b.
-    exists c a.
+    exists* c a.
         pts_to ctr c **
         pts_to acc a **
         pure (c <=^ x /\

share/steel/examples/pulse/ExistsWitness.fst

@@ -19,8 +19,8 @@ let assume_squash (p:prop) : squash p = assume p
 
 ```pulse
 fn sample (x:R.ref int)
-requires exists p y. R.pts_to x #p y
-ensures exists p y. R.pts_to x #p y ** pure (y == 17)
+requires exists* p y. R.pts_to x #p y
+ensures exists* p y. R.pts_to x #p y ** pure (y == 17)
 {
     let y' = get_witness x;
     assume_squash (y'==17);
@@ -30,8 +30,8 @@ ensures exists p y. R.pts_to x #p y ** pure (y == 17)
 
 ```pulse
 fn sample_ (x:R.ref int) (#p:perm)
-requires exists y. R.pts_to x #p y
-ensures exists y. R.pts_to x #p y ** pure (y == 17)
+requires exists* y. R.pts_to x #p y
+ensures exists* y. R.pts_to x #p y ** pure (y == 17)
 {
     let y = get_witness x;
     assume_squash (y==17);
@@ -41,8 +41,8 @@ ensures exists y. R.pts_to x #p y ** pure (y == 17)
 
 ```pulse
 fn sample2 (x:R.ref int) (#p:perm)
-requires exists y. R.pts_to x #p y
-ensures exists y. R.pts_to x #p y ** pure (y == 17)
+requires exists* y. R.pts_to x #p y
+ensures exists* y. R.pts_to x #p y ** pure (y == 17)
 {
     with (y:erased _).
     assert (R.pts_to x #p y);
@@ -55,7 +55,7 @@ assume val drop (p:vprop) : stt unit p (fun _ -> emp)
 
 ```pulse
 fn sample3 (x0:R.ref int) (x1:R.ref bool) (#p0 #p1:perm)
-requires exists v0 v1. R.pts_to x0 #p0 v0 ** R.pts_to x1 #p1 v1
+requires exists* v0 v1. R.pts_to x0 #p0 v0 ** R.pts_to x1 #p1 v1
 ensures emp
 {
 
@@ -68,7 +68,7 @@ ensures emp
 
 ```pulse
 fn sample4 (x0:R.ref int) (x1:R.ref bool) (#p0 #p1:perm)
-requires exists v0 v1. R.pts_to x0 #p0 v0 ** R.pts_to x1 #p1 v1
+requires exists* v0 v1. R.pts_to x0 #p0 v0 ** R.pts_to x1 #p1 v1
 ensures emp
 {
 
@@ -81,7 +81,7 @@ ensures emp
 
 ```pulse
 fn sample5 (x0:R.ref int) (x1:R.ref bool) (#p0 #p1:perm)
-requires exists v0 v1. R.pts_to x0 #p0 v0 ** R.pts_to x1 #p1 v1
+requires exists* v0 v1. R.pts_to x0 #p0 v0 ** R.pts_to x1 #p1 v1
 ensures emp
 {
 
@@ -96,7 +96,7 @@ ensures emp
 
 ```pulse
 fn sample6 (x0:R.ref int) (x1:R.ref bool)
-requires exists p0 p1 v0 v1. R.pts_to x0 #p0 v0 ** R.pts_to x1 #p1 v1
+requires exists* p0 p1 v0 v1. R.pts_to x0 #p0 v0 ** R.pts_to x1 #p1 v1
 ensures emp
 {
 

share/steel/examples/pulse/ExtractionTest.fst

@@ -38,7 +38,7 @@ fn write10 (x:ref U32.t)
   let mut ctr = 10ul;
   while ((ctr >^ 0ul))
   invariant b.
-    exists n i.
+    exists* n i.
       pts_to x n **
       pts_to ctr i **
       pure (i <=^ 10ul /\ 
@@ -57,13 +57,13 @@ module A = Pulse.Lib.Array
 ```pulse
 fn fill_array (x:array U32.t) (n:SZ.t) (v:U32.t)
   requires A.pts_to x 's ** pure (A.length x == SZ.v n)
-  ensures exists s. A.pts_to x s ** pure (Seq.equal s (Seq.create (SZ.v n) v))
+  ensures exists* s. A.pts_to x s ** pure (Seq.equal s (Seq.create (SZ.v n) v))
 {
   A.pts_to_len x;
   let mut i : SZ.t = 0sz;
   while (SZ.(i `SZ.lt` n))
   invariant b.
-    exists (vi:SZ.t) (s:Seq.seq U32.t).
+    exists* (vi:SZ.t) (s:Seq.seq U32.t).
       pts_to i vi **
       A.pts_to x s **
       pure (SZ.(vi <=^ n) /\

share/steel/examples/pulse/Fibo32.fst

@@ -27,7 +27,7 @@ fn fibo32 (k:U32.t) (_:squash(0ul < k /\ fits #U32.t (fib (v k))))
   let mut j = 1ul;
   let mut ctr = 1ul;
   while (let vctr = !ctr; (vctr < k))
-  invariant b . exists vi vj vctr. (
+  invariant b . exists* vi vj vctr. (
      pts_to i vi **
      pts_to j vj **
      pts_to ctr vctr **