Merge pull request #523 from mtzguido/tahina_array_updates

Some updates to Pulse.Lib.Array

Author: mtzguido

lib/pulse/lib/Pulse.Lib.Array.Core.fst

@@ -379,20 +379,29 @@ ghost fn pcm_gather u#a (#t: Type u#a) #l
 }
 
 ghost
-fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
-  requires pts_to_mask arr #p s mask
-  ensures pts_to_mask arr #(p /. 2.0R) s mask
-  ensures pts_to_mask arr #(p /. 2.0R) s mask
+fn mask_share_gen u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p (p1: perm) (p2: perm) #mask
+  requires pts_to_mask arr #p s mask ** pure ((p <: real) == p1 +. p2)
+  ensures pts_to_mask arr #p1 s mask
+  ensures pts_to_mask arr #p2 s mask
 {
   loc_get ();
   pts_to_mask_props arr;
   pcm_share
     arr p s mask
-    arr (p /. 2.0R) s mask
-    arr (p /. 2.0R) s mask;
+    arr p1 s mask
+    arr p2 s mask;
   drop_ (loc _);
 }
 
+ghost
+fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
+  requires pts_to_mask arr #p s mask
+  ensures pts_to_mask arr #(p /. 2.0R) s mask
+  ensures pts_to_mask arr #(p /. 2.0R) s mask
+{
+  mask_share_gen arr #s #p (p /. 2.0R) (p /. 2.0R) #mask
+}
+
 [@@allow_ambiguous]
 ghost fn mask_gather u#a (#t: Type u#a) (arr: array t) #p1 #p2 #s1 #s2 #mask1 #mask2
   requires pts_to_mask arr #p1 s1 mask1

lib/pulse/lib/Pulse.Lib.Array.Core.fsti

@@ -124,6 +124,12 @@ fn mask_free u#a (#elt: Type u#a) (a: array elt) (#s: Ghost.erased (Seq.seq elt)
   requires pure (forall i. mask i)
   requires pure (is_full_array a)
 
+ghost
+fn mask_share_gen u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p (p1: perm) (p2: perm) #mask
+  requires pts_to_mask arr #p s mask ** pure ((p <: real) == p1 +. p2)
+  ensures pts_to_mask arr #p1 s mask
+  ensures pts_to_mask arr #p2 s mask
+
 ghost
 fn mask_share u#a (#a: Type u#a) (arr:array a) (#s: Seq.seq a) #p #mask
   requires pts_to_mask arr #p s mask

lib/pulse/lib/Pulse.Lib.Array.fst

@@ -53,7 +53,7 @@ fn compare (#t:eqtype) (l:US.t) (a1 a2:larray t (US.v l)) (#p1 #p2:perm)
   (!i = l)
 }
 
-fn memcpy_l (#t:eqtype) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
+fn memcpy_l (#t:Type0) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
            (#p:perm) (#src0 #dst0:Ghost.erased (Seq.seq t))
   requires pts_to src #p src0 **
            pts_to dst dst0
@@ -89,7 +89,7 @@ fn memcpy_l (#t:eqtype) (l:US.t) (src dst:(a:array t { US.v l <= A.length a }))
 
 
 fn memcpy
-  (#t:eqtype)
+  (#t:Type0)
   (l:SZ.t)
   (src dst:larray t (SZ.v l))
   (#p:perm)

lib/pulse/lib/Pulse.Lib.Array.fsti

@@ -41,7 +41,7 @@ fn compare
      pure (res <==> Seq.equal s1 s2)
 
 fn memcpy_l
-        (#t:eqtype)
+        (#t:Type0)
         (l:SZ.t)
         (src dst:(a:array t { SZ.v l <= length a }))
         (#p:perm)
@@ -54,7 +54,7 @@ fn memcpy_l
                                    (Seq.slice dst0 (SZ.v l) (length dst)))
 
 fn memcpy
-        (#t:eqtype)
+        (#t:Type0)
         (l:SZ.t)
         (src dst:larray t (SZ.v l))
         (#p:perm)