Merge pull request #263 from FStarLang/_taramana_slice_ghost_split

Add ghost slice splitting

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

@@ -99,6 +99,69 @@ fn split_trade (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased
   }
 }
 
+ghost fn ghost_append_split (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t)
+    (#v1: (Seq.seq t) { SZ.v i == Seq.length v1 })
+    (#v2: (Seq.seq t))
+  requires pts_to s #p (v1 `Seq.append` v2)
+  returns res: Ghost.erased (slice t & slice t)
+  ensures
+    (
+      pts_to (fst res) #p v1 **
+      pts_to (snd res) #p v2 **
+      S.is_split s (fst res) (snd res)
+    )
+{
+  assert pure (v1 `Seq.equal` Seq.slice (Seq.append v1 v2) 0 (SZ.v i));
+  assert pure (v2 `Seq.equal` Seq.slice (Seq.append v1 v2) (SZ.v i) (Seq.length v1 + Seq.length v2));
+  S.ghost_split s i
+}
+
+ghost fn ghost_append_split_trade (#t: Type) (input: S.slice t) (#p: perm) (i: SZ.t)
+    (#v1: (Seq.seq t) { SZ.v i == Seq.length v1 })
+    (#v2: (Seq.seq t))
+  requires pts_to input #p (v1 `Seq.append` v2)
+  returns res: Ghost.erased (slice t & slice t)
+  ensures
+    (
+      pts_to (fst res) #p v1 ** pts_to (snd res) #p v2 **
+      trade (pts_to (fst res) #p v1 ** pts_to (snd res) #p v2)
+        (pts_to input #p (v1 `Seq.append` v2)))
+{
+  let res = ghost_append_split input i;
+      ghost fn aux ()
+        requires S.is_split input (fst res) (snd res) ** (pts_to (fst res) #p v1 ** pts_to (snd res) #p v2)
+        ensures pts_to input #p (v1 `Seq.append` v2)
+      {
+        S.join (fst res) (snd res) input
+      };
+      intro_trade _ _ _ aux;
+      res
+}
+
+ghost fn ghost_split_trade (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v: (Seq.seq t) { SZ.v i <= Seq.length v })
+  requires pts_to s #p v
+  returns res: Ghost.erased (slice t & slice t)
+  ensures
+    (
+      let v1 = Seq.slice v 0 (SZ.v i) in
+      let v2 = Seq.slice v (SZ.v i) (Seq.length v) in
+      pts_to (fst res) #p v1 ** pts_to (snd res) #p v2 **
+      trade (pts_to (fst res) #p v1 ** pts_to (snd res) #p v2)
+        (pts_to s #p v))
+{
+  Seq.lemma_split v (SZ.v i);
+  let s' = S.ghost_split s i;
+      with v1 v2. assert pts_to (fst s') #p v1 ** pts_to (snd s') #p v2;
+      ghost fn aux ()
+        requires S.is_split s (fst s') (snd s') ** (pts_to (fst s') #p v1 ** pts_to (snd s') #p v2)
+        ensures pts_to s #p v
+      {
+        S.join (fst s') (snd s') s
+      };
+      intro_trade _ _ _ aux;
+      s'
+}
+
 inline_for_extraction
 noextract
 fn subslice_trade_mut #t (s: slice t) (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v })

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

@@ -199,6 +199,35 @@ fn split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t)
     (s1, s2)
 }
 
+ghost
+fn ghost_split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t)
+    (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v })
+  requires pts_to s #p v
+  returns res : Ghost.erased (slice t & slice t)
+  ensures
+    (
+    pts_to (fst res) #p (Seq.slice v 0 (SZ.v i)) **
+    pts_to (snd res) #p (Seq.slice v (SZ.v i) (Seq.length v)) **
+    is_split s (fst res) (snd res)
+  )
+{
+    unfold_pts_to s #p v;
+    Seq.lemma_split v (SZ.v i);
+    let elt' = AP.ghost_split s.elt #p i;
+    let s1 = {
+        elt = s.elt;
+        len = i;
+    };
+    fold_pts_to s1 #p (Seq.slice v 0 (SZ.v i));
+    let s2 = {
+        elt = elt';
+        len = s.len `SZ.sub` i;
+    };
+    fold_pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v));
+    fold (is_split s s1 s2);
+    (s1, s2)
+}
+
 ghost
 fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (s: slice t)
     requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s s1 s2

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

@@ -104,6 +104,13 @@ val split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.se
       pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)) **
       is_split s s1 s2)
 
+val ghost_split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) : stt_ghost (Ghost.erased (slice t & slice t)) emp_inames
+    (requires pts_to s #p v)
+    (ensures fun res ->
+      pts_to (fst res) #p (Seq.slice v 0 (SZ.v i)) **
+      pts_to (snd res) #p (Seq.slice v (SZ.v i) (Seq.length v)) **
+      is_split s (fst res) (snd res))
+
 val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2: Seq.seq t) (s: slice t) : stt_ghost unit emp_inames
     (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s s1 s2)
     (fun _ -> pts_to s #p (Seq.append v1 v2))