Merge pull request #351 from mtzguido/slice_array_pts_to

ArrayPtr/Slice: expose pts_to, make instance transparent

lib/pulse/lib/Pulse.Lib.ArrayPtr.fst

@@ -26,10 +26,8 @@ type ptr t = {
 let base a = a.base
 let offset a = SZ.v a.offset
 
-instance has_pts_to_array_ptr t = {
-  pts_to = (fun s #p v ->
-    A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v)
-}
+let pts_to s #p v =
+  A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
 
 ghost fn unfold_pts_to #t (s: ptr t) #p v
   requires pts_to s #p v

lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti

@@ -35,7 +35,17 @@ val ptr ([@@@strictly_positive] elt: Type0) : Type0
 val base #t (p: ptr t) : GTot (A.array t)
 val offset #t (p: ptr t) : GTot nat
 
-instance val has_pts_to_array_ptr (t: Type) : has_pts_to (ptr t) (Seq.seq t)
+val pts_to
+  (#t:Type)
+  (s:ptr t)
+  (#[exact (`1.0R)] p:perm)
+  (v : Seq.seq t)
+  : slprop
+
+[@@pulse_unfold]
+instance has_pts_to_array_ptr (t: Type) : has_pts_to (ptr t) (Seq.seq t) = {
+  pts_to = (fun s #p v -> pts_to s #p v);
+}
 
 val pts_to_timeless (#a:Type) (x:ptr a) (p:perm) (s:Seq.seq a)
   : Lemma (timeless (pts_to x #p s))

lib/pulse/lib/Pulse.Lib.Slice.Util.fst

@@ -220,19 +220,19 @@ inline_for_extraction
 fn arrayptr_to_slice_intro_trade
   (#t: Type) (a: AP.ptr t) (#p: perm) (alen: SZ.t) (#v: Ghost.erased (Seq.seq t))
   requires
-    (pts_to a #p v ** pure (SZ.v alen == Seq.length v))
+    (AP.pts_to a #p v ** pure (SZ.v alen == Seq.length v))
   returns s: slice t
   ensures
     (pts_to s #p v **
       trade
         (pts_to s #p v)
-        (pts_to a #p v)
+        (AP.pts_to a #p v)
     )
 {
   let s = arrayptr_to_slice_intro a alen;
   ghost fn aux (_: unit)
     requires arrayptr_to_slice a s ** pts_to s #p v
-    ensures pts_to a #p v
+    ensures AP.pts_to a #p v
   {
     arrayptr_to_slice_elim s
   };
@@ -247,16 +247,16 @@ requires
   (pts_to s #p v)
 returns a: AP.ptr t
 ensures
-  (pts_to a #p v **
+  (AP.pts_to a #p v **
     trade
-      (pts_to a #p v)
+      (AP.pts_to a #p v)
       (pts_to s #p v)
   )
 {
   pts_to_len s;
   let a = slice_to_arrayptr_intro s;
   ghost fn aux (_: unit)
-    requires slice_to_arrayptr s a ** pts_to a #p v
+    requires slice_to_arrayptr s a ** AP.pts_to a #p v
     ensures pts_to s #p v
   {
     slice_to_arrayptr_elim a;

lib/pulse/lib/Pulse.Lib.Slice.fst

@@ -27,28 +27,26 @@ type slice t = {
 
 let len s = s.len
 
-let has_pts_to_slice t = {
-  pts_to = (fun s #p v ->
-    pts_to s.elt #p v **
-    pure (Seq.length v == SZ.v s.len))
-}
+let pts_to (#t:Type) (s:slice t) (#p:perm) (v : Seq.seq t) =
+  pts_to s.elt #p v **
+  pure (Seq.length v == SZ.v s.len)
 
 ghost fn unfold_pts_to #t (s: slice t) #p v
   requires pts_to s #p v
-  ensures pts_to s.elt #p v **
+  ensures AP.pts_to s.elt #p v **
     pure (Seq.length v == SZ.v s.len)
 {
   rewrite pts_to s #p v as
-    pts_to s.elt #p v **
+    AP.pts_to s.elt #p v **
     pure (Seq.length v == SZ.v s.len)
 }
 
 ghost fn fold_pts_to #t (s: slice t) #p v
-  requires pts_to s.elt #p v **
+  requires AP.pts_to s.elt #p v **
     pure (Seq.length v == SZ.v s.len)
   ensures pts_to s #p v
 {
-  rewrite pts_to s.elt #p v **
+  rewrite AP.pts_to s.elt #p v **
       pure (Seq.length v == SZ.v s.len)
     as pts_to s #p v;
 }
@@ -104,7 +102,7 @@ let arrayptr_to_slice
 fn arrayptr_to_slice_intro
   (#t: Type) (a: AP.ptr t) (#p: perm) (alen: SZ.t) (#v: Ghost.erased (Seq.seq t))
   requires
-    (pts_to a #p v ** pure (SZ.v alen == Seq.length v))
+    (AP.pts_to a #p v ** pure (SZ.v alen == Seq.length v))
   returns s: slice t
   ensures
     (pts_to s #p v ** arrayptr_to_slice a s)
@@ -124,7 +122,7 @@ fn arrayptr_to_slice_elim
 requires
   (pts_to s #p v ** arrayptr_to_slice a s)
 ensures
-  (pts_to a #p v)
+  (AP.pts_to a #p v)
 {
   unfold (arrayptr_to_slice a s);
   unfold_pts_to s #p v;
@@ -140,7 +138,7 @@ requires
   (pts_to s #p v)
 returns a: AP.ptr t
 ensures
-  (pts_to a #p v ** slice_to_arrayptr s a)
+  (AP.pts_to a #p v ** slice_to_arrayptr s a)
 {
   unfold_pts_to s #p v;
   fold (slice_to_arrayptr s s.elt);
@@ -151,7 +149,7 @@ ghost
 fn slice_to_arrayptr_elim
   (#t: Type) (a: AP.ptr t) (#p: perm) (#v: Seq.seq t) (#s: slice t)
 requires
-  (pts_to a #p v ** slice_to_arrayptr s a ** pure (Seq.length v == SZ.v (len s)))
+  (AP.pts_to a #p v ** slice_to_arrayptr s a ** pure (Seq.length v == SZ.v (len s)))
 ensures
   (pts_to s #p v)
 {

lib/pulse/lib/Pulse.Lib.Slice.fsti

@@ -24,7 +24,12 @@ val slice ([@@@strictly_positive] elt: Type0) : Type0
 
 val len (#t: Type) : slice t -> SZ.t
 
-instance val has_pts_to_slice (t: Type u#0) : has_pts_to (slice t) (Seq.seq t)
+val pts_to (#t:Type) (s:slice t) (#[exact (`1.0R)] p:perm) (v : Seq.seq t) : slprop
+
+[@@pulse_unfold]
+instance has_pts_to_slice (t: Type u#0) : has_pts_to (slice t) (Seq.seq t) = {
+  pts_to = (fun s #p v -> pts_to s #p v);
+}
 
 val pts_to_timeless (#a:Type) (x:slice a) (p:perm) (s:Seq.seq a)
   : Lemma (timeless (pts_to x #p s))
@@ -57,12 +62,12 @@ val arrayptr_to_slice
 : slprop
 
 val arrayptr_to_slice_intro (#t: Type) (a: AP.ptr t) (#p: perm) (alen: SZ.t) (#v: Ghost.erased (Seq.seq t)) : stt (slice t)
-    (pts_to a #p v ** pure (SZ.v alen == Seq.length v))
+    (AP.pts_to a #p v ** pure (SZ.v alen == Seq.length v))
     (fun s -> pts_to s #p v ** arrayptr_to_slice a s)
 
 val arrayptr_to_slice_elim (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: AP.ptr t) : stt_ghost unit emp_inames
     (pts_to s #p v ** arrayptr_to_slice a s)
-    (fun _ -> pts_to a #p v)
+    (fun _ -> AP.pts_to a #p v)
 
 val slice_to_arrayptr
   (#t: Type)
@@ -72,10 +77,10 @@ val slice_to_arrayptr
 
 val slice_to_arrayptr_intro (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (AP.ptr t)
     (pts_to s #p v)
-    (fun a -> pts_to a #p v ** slice_to_arrayptr s a)
+    (fun a -> AP.pts_to a #p v ** slice_to_arrayptr s a)
 
 val slice_to_arrayptr_elim (#t: Type) (a: AP.ptr t) (#p: perm) (#v: Seq.seq t) (#s: slice t) : stt_ghost unit emp_inames
-    (pts_to a #p v ** slice_to_arrayptr s a ** pure (Seq.length v == SZ.v (len s)))
+    (AP.pts_to a #p v ** slice_to_arrayptr s a ** pure (Seq.length v == SZ.v (len s)))
     (fun _ -> pts_to s #p v)
 
 (* END C only *)

test/Example.Slice.fst

@@ -19,6 +19,7 @@ open Pulse
 open Pulse.Lib.Trade
 open Pulse.Lib.Slice.Util
 module A = Pulse.Lib.Array
+open Pulse { pts_to } (* restore pts_to, shadowed by Pulse.Lib.Slice.Util *)
 
 fn test (arr: A.array UInt8.t)
     requires pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy; 5uy]