Slice.subslice

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

@@ -156,7 +156,8 @@ fn gather
     fold_pts_to arr #(p0 +. p1) s0
 }
 
-fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t { SZ.v i <= Seq.length v })
+fn split (#t: Type) (s: ptr 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 s' : ptr t
   ensures
@@ -184,6 +185,36 @@ fn split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.
     s'
 }
 
+ghost fn ghost_split (#t: Type) (s: ptr 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 s' : erased (ptr t)
+  ensures
+    pts_to s #p (Seq.slice v 0 (SZ.v i)) **
+    pts_to (reveal s') #p (Seq.slice v (SZ.v i) (Seq.length v)) **
+    pure (adjacent s (SZ.v i) s')
+{
+    unfold_pts_to s #p v;
+    A.pts_to_range_prop s.base;
+    let s' = {
+        base = s.base;
+        offset = SZ.add s.offset i;
+    };
+    A.pts_to_range_split s.base _ (SZ.v s'.offset) _;
+    with s1. assert A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1;
+    rewrite
+        (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s'.offset) #p s1)
+        as (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + SZ.v i) #p s1);
+    fold_pts_to s #p s1;
+    with s2. assert A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2;
+    rewrite
+        (A.pts_to_range s.base (SZ.v s'.offset) (SZ.v s.offset + Seq.length v) #p s2)
+        as (A.pts_to_range s'.base (SZ.v s'.offset) (SZ.v s'.offset + Seq.length s2) #p s2);
+    fold_pts_to s' #p s2;
+    s'
+}
+
+
 ghost
 fn join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t)
     requires pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2)

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

@@ -106,14 +106,26 @@ val gather
 let adjacent #t (a: ptr t) (sz: nat) (b: ptr t) : prop =
   base a == base b /\ offset a + sz == offset b
 
-val split (#t: Type) (s: ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) (i: SZ.t { SZ.v i <= Seq.length v }) : stt (ptr t)
+val split (#t: Type) (s: ptr t) (#p: perm) (i: SZ.t)
+  (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v })
+  : stt (ptr t)
     (requires pts_to s #p v)
     (ensures fun s' ->
         pts_to s #p (Seq.slice v 0 (SZ.v i)) **
         pts_to s' #p (Seq.slice v (SZ.v i) (Seq.length v)) **
         pure (adjacent s (SZ.v i) s')
     )
 
+val ghost_split (#t: Type) (s: ptr t) (#p: perm) (i: SZ.t)
+  (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v })
+  : stt_ghost (erased (ptr t)) []
+    (requires pts_to s #p v)
+    (ensures fun s' ->
+        pts_to s #p (Seq.slice v 0 (SZ.v i)) **
+        pts_to (reveal s') #p (Seq.slice v (SZ.v i) (Seq.length v)) **
+        pure (adjacent s (SZ.v i) s')
+    )
+
 val join (#t: Type) (s1: ptr t) (#p: perm) (#v1: Seq.seq t) (s2: ptr t) (#v2: Seq.seq t) : stt_ghost unit emp_inames
     (pts_to s1 #p v1 ** pts_to s2 #p v2 ** pure (adjacent s1 (Seq.length v1) s2))
     (fun _ -> pts_to s1 #p (Seq.append v1 v2))

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

@@ -97,3 +97,56 @@ fn split_trade (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased
   intro_trade _ _ _ (split_trade_aux s p v i s1 s2 v1 v2 ());
   S.SlicePair s1 s2
 }
+
+// TODO(GE): fix extraction for inline ghost functions (currently extracts to Obj.magic (fun _ -> ()))
+ghost fn subslice_trade_mut_aux #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 }) (res: slice t) (v': Seq.seq t) ()
+  requires subslice_rest res s 1.0R i j v ** pts_to res v'
+  ensures pts_to s (Seq.slice v 0 (SZ.v i) `Seq.append` v' `Seq.append` Seq.slice v (SZ.v j) (Seq.length v))
+{
+  unfold subslice_rest;
+  join res _ _;
+  join _ _ s;
+  assert pure (
+    Seq.Base.append (Seq.Base.append (Seq.Base.slice v 0 (SZ.v i)) v')
+          (Seq.Base.slice v (SZ.v j) (Seq.Base.length v))
+    `Seq.equal`
+    Seq.Base.append (Seq.Base.slice v 0 (SZ.v i))
+        (Seq.Base.append v' (Seq.Base.slice v (SZ.v j) (Seq.Base.length v))));
+}
+
+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 })
+  requires pts_to s v
+  returns res: slice t
+  ensures pts_to res (Seq.slice v (SZ.v i) (SZ.v j)) **
+    (forall* v'. trade (pts_to res v') (pts_to s (Seq.slice v 0 (SZ.v i) `Seq.append` v' `Seq.append` Seq.slice v (SZ.v j) (Seq.length v))))
+{
+  let res = subslice s i j;
+  intro_forall _ (fun v' -> intro_trade _ _ _ (subslice_trade_mut_aux s i j #v res v'));
+  res
+}
+
+ghost fn subslice_trade_aux #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) (res: slice t) ()
+  requires subslice_rest res s p i j v ** pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j))
+  ensures pts_to s #p v
+{
+  unfold subslice_rest;
+  join res _ _;
+  join _ _ s;
+  assert pure (v `Seq.equal` Seq.append (Seq.slice v 0 (SZ.v i))
+    (Seq.append (Seq.slice v (SZ.v i) (SZ.v j)) (Seq.slice v (SZ.v j) (Seq.length v))));
+}
+
+inline_for_extraction
+noextract
+fn subslice_trade #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v })
+  requires pts_to s #p v
+  returns res: slice t
+  ensures pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)) **
+    trade (pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j))) (pts_to s #p v)
+{
+  let res = subslice s i j;
+  intro_trade _ _ _ (subslice_trade_aux s i j #v res);
+  res
+}

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

@@ -184,7 +184,7 @@ fn split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t)
 {
     unfold_pts_to s #p v;
     Seq.lemma_split v (SZ.v i);
-    let elt' = AP.split s.elt #p #v i;
+    let elt' = AP.split s.elt #p i;
     let s1 = {
         elt = s.elt;
         len = i;
@@ -211,6 +211,27 @@ fn join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2:
     fold_pts_to s #p (Seq.append v1 v2)
 }
 
+fn subslice #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v })
+  requires pts_to s #p v
+  returns res: slice t
+  ensures pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)) ** subslice_rest res s p i j v
+{
+  unfold_pts_to s #p v;
+  let elt' = AP.split s.elt i;
+  let elt'' = AP.ghost_split elt' (SZ.sub j i);
+  let s1 = hide { elt = s.elt; len = i };
+  let s2 = hide { elt = elt'; len = SZ.sub s.len i };
+  fold is_split s s1 s2;
+  let res = hide { elt = elt'; len = SZ.sub j i };
+  let s3 = hide { elt = elt''; len = SZ.sub s.len j };
+  fold is_split s2 res s3;
+  fold_pts_to s1 #p (Seq.slice v 0 (SZ.v i));
+  fold_pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j));
+  fold_pts_to s3 #p (Seq.slice v (SZ.v j) (Seq.length v));
+  fold subslice_rest;
+  ({ elt = elt'; len = SZ.sub j i })
+}
+
 fn copy
   (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t))
 requires

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

@@ -110,6 +110,18 @@ val join (#t: Type) (s1: slice t) (#p: perm) (#v1: Seq.seq t) (s2: slice t) (#v2
     (pts_to s1 #p v1 ** pts_to s2 #p v2 ** is_split s s1 s2)
     (fun _ -> pts_to s #p (Seq.append v1 v2))
 
+(* `subslice_rest r s p i j v` is the resource remaining after taking the subslice `r = s[i..j]` *)
+let subslice_rest #t (r: slice t) (s: slice t) p (i j: SZ.t) (v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) : slprop =
+  exists* s1 s2 s3.
+    is_split s s1 s2 **
+    is_split s2 r s3 **
+    pts_to s1 #p (Seq.slice v 0 (SZ.v i)) **
+    pts_to s3 #p (Seq.slice v (SZ.v j) (Seq.length v))
+
+val subslice #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= SZ.v j /\ SZ.v j <= Seq.length v }) :
+  stt (slice t) (pts_to s #p v)
+    fun res -> pts_to res #p (Seq.slice v (SZ.v i) (SZ.v j)) ** subslice_rest res s p i j v
+
 val copy (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t)) : stt unit
     (exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (len src == len dst))
     (fun _ -> pts_to dst v ** pts_to src #p v)

pulse2rust/src/Pulse2Rust.Extract.fst

@@ -660,6 +660,10 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
   | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::_::i::_)
     when S.string_of_mlpath p = "Pulse.Lib.Slice.split" ->
     mk_method_call (extract_mlexpr g e) "split_at_mut" [extract_mlexpr g i]
+  | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, s::_::a::b::_)
+    when S.string_of_mlpath p = "Pulse.Lib.Slice.subslice" ->
+    let mutb = true in
+    mk_reference_expr true (mk_expr_index (extract_mlexpr g s) (mk_range (Some (extract_mlexpr g a)) RangeLimitsHalfOpen (Some (extract_mlexpr g b))))
   | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, a::_::b::_)
     when S.string_of_mlpath p = "Pulse.Lib.Slice.copy" ->
     mk_method_call (extract_mlexpr g a) "copy_from_slice" [extract_mlexpr g b]

pulse2rust/src/Pulse2Rust.Rust.Syntax.fst

@@ -189,6 +189,13 @@ let mk_cast (e:expr) (ty:typ) : expr =
     expr_cast_type = ty;
   }
 
+let mk_range (s:option expr) (l:range_limits) (e:option expr) : expr =
+  Expr_range {
+    expr_range_start = s;
+    expr_range_limits = l;
+    expr_range_end = e;
+  }
+
 let mk_new_mutex (e:expr) =
   mk_call
     (mk_expr_path ["std"; "sync"; "Mutex"; "new"])

pulse2rust/src/Pulse2Rust.Rust.Syntax.fsti

@@ -112,6 +112,7 @@ and expr =
   | Expr_tuple of list expr
   | Expr_method_call of expr_method_call
   | Expr_cast of expr_cast
+  | Expr_range of expr_range
 
 and expr_bin = {
   expr_bin_left : expr;
@@ -197,6 +198,16 @@ and expr_cast = {
   expr_cast_type : typ;
 }
 
+and expr_range = {
+  expr_range_start: option expr;
+  expr_range_limits: range_limits;
+  expr_range_end: option expr;
+}
+
+and range_limits =
+  | RangeLimitsHalfOpen
+  | RangeLimitsClosed
+
 and local_stmt = {
   local_stmt_pat : option pat;
   local_stmt_init : option expr;
@@ -358,6 +369,7 @@ val mk_expr_tuple (l:list expr) : expr
 val mk_mem_replace (t:typ) (e:expr) (new_v:expr) : expr
 val mk_method_call (receiver:expr) (name:string) (args:list expr) : expr
 val mk_cast (e:expr) (ty:typ) : expr
+val mk_range (s:option expr) (l:range_limits) (e:option expr) : expr
 
 val mk_new_mutex (e:expr) : expr
 val mk_lock_mutex (e:expr) : expr

pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml

@@ -1240,6 +1240,36 @@ and (extract_mlexpr :
           let uu___7 = extract_mlexpr g e1 in
           let uu___8 = let uu___9 = extract_mlexpr g i in [uu___9] in
           Pulse2Rust_Rust_Syntax.mk_method_call uu___7 "split_at_mut" uu___8
+      | FStarC_Extraction_ML_Syntax.MLE_App
+          ({
+             FStarC_Extraction_ML_Syntax.expr =
+               FStarC_Extraction_ML_Syntax.MLE_TApp
+               ({
+                  FStarC_Extraction_ML_Syntax.expr =
+                    FStarC_Extraction_ML_Syntax.MLE_Name p;
+                  FStarC_Extraction_ML_Syntax.mlty = uu___;
+                  FStarC_Extraction_ML_Syntax.loc = uu___1;_},
+                uu___2::[]);
+             FStarC_Extraction_ML_Syntax.mlty = uu___3;
+             FStarC_Extraction_ML_Syntax.loc = uu___4;_},
+           s::uu___5::a::b::uu___6)
+          when
+          let uu___7 = FStarC_Extraction_ML_Syntax.string_of_mlpath p in
+          uu___7 = "Pulse.Lib.Slice.subslice" ->
+          let mutb = true in
+          let uu___7 =
+            let uu___8 = extract_mlexpr g s in
+            let uu___9 =
+              let uu___10 =
+                let uu___11 = extract_mlexpr g a in
+                FStar_Pervasives_Native.Some uu___11 in
+              let uu___11 =
+                let uu___12 = extract_mlexpr g b in
+                FStar_Pervasives_Native.Some uu___12 in
+              Pulse2Rust_Rust_Syntax.mk_range uu___10
+                Pulse2Rust_Rust_Syntax.RangeLimitsHalfOpen uu___11 in
+            Pulse2Rust_Rust_Syntax.mk_expr_index uu___8 uu___9 in
+          Pulse2Rust_Rust_Syntax.mk_reference_expr true uu___7
       | FStarC_Extraction_ML_Syntax.MLE_App
           ({
              FStarC_Extraction_ML_Syntax.expr =

pulse2rust/src/ocaml/generated/Pulse2Rust_Rust_Syntax.ml

@@ -163,6 +163,7 @@ and expr =
   | Expr_tuple of expr Prims.list 
   | Expr_method_call of expr_method_call 
   | Expr_cast of expr_cast 
+  | Expr_range of expr_range 
 and expr_bin =
   {
   expr_bin_left: expr ;
@@ -221,6 +222,14 @@ and expr_method_call =
 and expr_cast = {
   expr_cast_expr: expr ;
   expr_cast_type: typ }
+and expr_range =
+  {
+  expr_range_start: expr FStar_Pervasives_Native.option ;
+  expr_range_limits: range_limits ;
+  expr_range_end: expr FStar_Pervasives_Native.option }
+and range_limits =
+  | RangeLimitsHalfOpen 
+  | RangeLimitsClosed 
 and local_stmt =
   {
   local_stmt_pat: pat FStar_Pervasives_Native.option ;
@@ -406,6 +415,11 @@ let (uu___is_Expr_cast : expr -> Prims.bool) =
     match projectee with | Expr_cast _0 -> true | uu___ -> false
 let (__proj__Expr_cast__item___0 : expr -> expr_cast) =
   fun projectee -> match projectee with | Expr_cast _0 -> _0
+let (uu___is_Expr_range : expr -> Prims.bool) =
+  fun projectee ->
+    match projectee with | Expr_range _0 -> true | uu___ -> false
+let (__proj__Expr_range__item___0 : expr -> expr_range) =
+  fun projectee -> match projectee with | Expr_range _0 -> _0
 let (__proj__Mkexpr_bin__item__expr_bin_left : expr_bin -> expr) =
   fun projectee ->
     match projectee with
@@ -567,6 +581,30 @@ let (__proj__Mkexpr_cast__item__expr_cast_type : expr_cast -> typ) =
   fun projectee ->
     match projectee with
     | { expr_cast_expr; expr_cast_type;_} -> expr_cast_type
+let (__proj__Mkexpr_range__item__expr_range_start :
+  expr_range -> expr FStar_Pervasives_Native.option) =
+  fun projectee ->
+    match projectee with
+    | { expr_range_start; expr_range_limits; expr_range_end;_} ->
+        expr_range_start
+let (__proj__Mkexpr_range__item__expr_range_limits :
+  expr_range -> range_limits) =
+  fun projectee ->
+    match projectee with
+    | { expr_range_start; expr_range_limits; expr_range_end;_} ->
+        expr_range_limits
+let (__proj__Mkexpr_range__item__expr_range_end :
+  expr_range -> expr FStar_Pervasives_Native.option) =
+  fun projectee ->
+    match projectee with
+    | { expr_range_start; expr_range_limits; expr_range_end;_} ->
+        expr_range_end
+let (uu___is_RangeLimitsHalfOpen : range_limits -> Prims.bool) =
+  fun projectee ->
+    match projectee with | RangeLimitsHalfOpen -> true | uu___ -> false
+let (uu___is_RangeLimitsClosed : range_limits -> Prims.bool) =
+  fun projectee ->
+    match projectee with | RangeLimitsClosed -> true | uu___ -> false
 let (__proj__Mklocal_stmt__item__local_stmt_pat :
   local_stmt -> pat FStar_Pervasives_Native.option) =
   fun projectee ->
@@ -1088,6 +1126,15 @@ let (mk_method_call : expr -> Prims.string -> expr Prims.list -> expr) =
           }
 let (mk_cast : expr -> typ -> expr) =
   fun e -> fun ty -> Expr_cast { expr_cast_expr = e; expr_cast_type = ty }
+let (mk_range :
+  expr FStar_Pervasives_Native.option ->
+    range_limits -> expr FStar_Pervasives_Native.option -> expr)
+  =
+  fun s ->
+    fun l ->
+      fun e ->
+        Expr_range
+          { expr_range_start = s; expr_range_limits = l; expr_range_end = e }
 let (mk_new_mutex : expr -> expr) =
   fun e ->
     let uu___ = mk_expr_path ["std"; "sync"; "Mutex"; "new"] in