diff --git a/lib/pulse/lib/Pulse.Lib.Array.Core.fst b/lib/pulse/lib/Pulse.Lib.Array.Core.fst
index 822d0d067..6dd3ff41c 100644
--- a/lib/pulse/lib/Pulse.Lib.Array.Core.fst
+++ b/lib/pulse/lib/Pulse.Lib.Array.Core.fst
@@ -362,7 +362,6 @@ ensures post
   free arr  
 }
 
-```pulse
 ghost
 fn pts_to_range_share
   (#a:Type)
@@ -378,9 +377,7 @@ fn pts_to_range_share
   fold (pts_to_range arr l r #(p /. 2.0R) s);
   fold (pts_to_range arr l r #(p /. 2.0R) s);
 }
-```
 
-```pulse
 ghost
 fn pts_to_range_gather
   (#a:Type)
@@ -396,7 +393,6 @@ fn pts_to_range_gather
   H.pts_to_range_gather arr;
   fold (pts_to_range arr l r #(p0 +. p1) s0)
 }
-```
 
 
 (* this is universe-polymorphic in ret_t; so can't define it in Pulse yet *)
diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst
new file mode 100644
index 000000000..11afa6347
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fst
@@ -0,0 +1,232 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Lib.ArrayPtr
+#lang-pulse
+
+noeq
+type ptr t = {
+    base: A.array t;
+    offset: (offset: SZ.t { SZ.v offset <= A.length base})
+}
+
+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)
+}
+
+ghost fn unfold_pts_to #t (s: ptr t) #p v
+  requires pts_to s #p v
+  ensures A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
+{
+  rewrite pts_to s #p v as
+    A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
+}
+
+ghost fn fold_pts_to #t (s: ptr t) #p v
+  requires A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
+  ensures pts_to s #p v
+{
+  rewrite
+    A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v
+    as pts_to s #p v
+}
+
+let pts_to_is_slprop2 x p s = ()
+
+let is_from_array s sz a =
+    pure (sz == A.length a /\ s.base == a)
+
+fn from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
+    requires A.pts_to a #p v
+    returns s: ptr t
+    ensures pts_to s #p v ** is_from_array s (Seq.length v) a
+{
+    A.pts_to_len a;
+    let res = {
+        base = a;
+        offset = 0sz;
+    };
+    fold (is_from_array res (Seq.length v) a);
+    A.pts_to_range_intro a p v;
+    rewrite (A.pts_to_range a 0 (A.length a) #p v)
+        as (A.pts_to_range res.base (SZ.v res.offset) (SZ.v res.offset + Seq.length v) #p v);
+    fold_pts_to res #p v;
+    res
+}
+
+ghost
+fn to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#v: Seq.seq t)
+    requires pts_to s #p v ** is_from_array s (Seq.length v) a
+    ensures A.pts_to a #p v
+{
+    unfold is_from_array s (Seq.length v) a;
+    unfold_pts_to s #p v;
+    A.pts_to_range_prop s.base;
+    rewrite (A.pts_to_range s.base (SZ.v s.offset) (SZ.v s.offset + Seq.length v) #p v)
+        as (A.pts_to_range a 0 (A.length a) #p v);
+    A.pts_to_range_elim a _ _;
+}
+
+fn op_Array_Access
+        (#t: Type)
+        (a: ptr t)
+        (i: SZ.t)
+        (#p: perm)
+        (#s: Ghost.erased (Seq.seq t))
+   requires
+     pts_to a #p s ** pure (SZ.v i < Seq.length s)
+   returns res: t
+   ensures
+            pts_to a #p s **
+            pure (
+              SZ.v i < Seq.length s /\
+              res == Seq.index s (SZ.v i))
+{
+    unfold_pts_to a #p s;
+    A.pts_to_range_prop a.base;
+    let res = A.pts_to_range_index a.base (SZ.add a.offset i);
+    fold_pts_to a #p s;
+    res
+}
+
+fn op_Array_Assignment
+        (#t: Type)
+        (a: ptr t)
+        (i: SZ.t)
+        (v: t)
+        (#s: Ghost.erased (Seq.seq t))
+   requires
+     pts_to a s ** pure (SZ.v i < Seq.length s)
+   ensures exists* s' .
+            pts_to a s' **
+            pure (SZ.v i < Seq.length s /\
+              s' == Seq.upd s (SZ.v i) v
+            )
+{
+    unfold_pts_to a s;
+    A.pts_to_range_prop a.base;
+    let res = A.pts_to_range_upd a.base (SZ.add a.offset i) v;
+    fold_pts_to a (Seq.upd s (SZ.v i) v);
+}
+
+ghost
+fn share
+  (#a:Type)
+  (arr:ptr a)
+  (#s:Ghost.erased (Seq.seq a))
+  (#p:perm)
+  requires pts_to arr #p s
+  ensures pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s
+{
+    unfold_pts_to arr #p s;
+    A.pts_to_range_share arr.base;
+    fold_pts_to arr #(p /. 2.0R) s;
+    fold_pts_to arr #(p /. 2.0R) s;    
+}
+
+ghost
+fn gather
+  (#a:Type)
+  (arr:ptr a)
+  (#s0 #s1:Ghost.erased (Seq.seq a))
+  (#p0 #p1:perm)
+  requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 ** pure (Seq.length s0 == Seq.length s1)
+  ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1)
+{
+    unfold_pts_to arr #p0 s0;
+    unfold_pts_to arr #p1 s1;
+    A.pts_to_range_gather arr.base;
+    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 })
+  requires pts_to s #p v
+  returns s' : ptr t
+  ensures
+    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')
+{
+    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)
+    ensures pts_to s1 #p (Seq.append v1 v2)
+{
+    unfold_pts_to s1 #p v1;
+    unfold_pts_to s2 #p v2;
+    rewrite (A.pts_to_range s2.base (SZ.v s2.offset) (SZ.v s2.offset + Seq.length v2) #p v2)
+        as (A.pts_to_range s1.base (SZ.v s1.offset + Seq.length v1) (SZ.v s1.offset + Seq.length v1 + Seq.length v2) #p v2);
+    A.pts_to_range_join s1.base (SZ.v s1.offset) (SZ.v s1.offset + Seq.length v1) (SZ.v s1.offset + Seq.length v1 + Seq.length v2);
+    fold_pts_to s1 #p (Seq.append v1 v2)
+}
+
+module R = Pulse.Lib.Reference
+
+fn memcpy
+    (#t:Type0) (#p0:perm)
+    (src:ptr t) (idx_src: SZ.t)
+    (dst:ptr t) (idx_dst: SZ.t)
+    (len: SZ.t)
+    (#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 })
+    (#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 })
+  requires pts_to src #p0 s0 ** pts_to dst s1
+  ensures pts_to src #p0 s0 **
+    pts_to dst (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1))
+{
+  let mut i = 0sz;
+  while (let vi = !i; SZ.lt vi len)
+    invariant b. exists* s1' vi.
+      R.pts_to i vi **
+      pts_to src #p0 s0 **
+      pts_to dst s1' **
+      pure (b == SZ.lt vi len /\ SZ.lte vi len /\
+        Seq.length s1' == Seq.length s1 /\
+        forall (j:nat). j < Seq.length s1' ==>
+          Seq.index s1' j == (if j < SZ.v vi then Seq.index s0 j else Seq.index s1 j))
+  {
+    let vi = !i;
+    let x = src.(vi);
+    dst.(vi) <- x;
+    i := SZ.add vi 1sz;
+  };
+  with s1'. assert pts_to dst s1';
+  assert pure (s1' `Seq.equal`
+    (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1)))
+}
diff --git a/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti
new file mode 100644
index 000000000..3e308be45
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.ArrayPtr.fsti
@@ -0,0 +1,130 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Lib.ArrayPtr
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives
+module SZ = FStar.SizeT
+module A = Pulse.Lib.Array
+
+(*
+The `ArrayPtr.ptr t` type in this module cannot be extracted to Rust
+because of the `split` operation, which assumes that the same pointer
+can point to either the large subarray or its sub-subarray, depending on the permission.
+Rust slices have the length baked in, so they cannot support this operation
+without modifying the pointer.
+
+Use `Pulse.Lib.Slice.slice` instead when possible.
+*)
+
+val ptr : 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_is_slprop2 (#a:Type) (x:ptr a) (p:perm) (s:Seq.seq a)
+  : Lemma (is_slprop2 (pts_to x #p s))
+          [SMTPat (is_slprop2 (pts_to x #p s))]
+
+val is_from_array (#t: Type) (s: ptr t) (sz: nat) (a: A.array t) : slprop
+
+val from_array (#t: Type) (a: A.array t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (ptr t)
+    (A.pts_to a #p v)
+    (fun s -> pts_to s #p v ** is_from_array s (Seq.length v) a)
+
+val to_array (#t: Type) (s: ptr t) (a: array t) (#p: perm) (#v: Seq.seq t) : stt_ghost unit emp_inames
+    (pts_to s #p v ** is_from_array s (Seq.length v) a)
+    (fun _ -> A.pts_to a #p v)
+
+(* Written x.(i) *)
+val op_Array_Access
+        (#t: Type)
+        (a: ptr t)
+        (i: SZ.t)
+        (#p: perm)
+        (#s: Ghost.erased (Seq.seq t))
+  : stt t
+        (requires
+            pts_to a #p s ** pure (SZ.v i < Seq.length s))
+        (ensures fun res ->
+            pts_to a #p s **
+            pure (
+              SZ.v i < Seq.length s /\
+              res == Seq.index s (SZ.v i)))
+
+(* Written a.(i) <- v *)
+val op_Array_Assignment
+        (#t: Type)
+        (a: ptr t)
+        (i: SZ.t)
+        (v: t)
+        (#s: Ghost.erased (Seq.seq t))
+  : stt unit
+        (requires
+            pts_to a s ** pure (SZ.v i < Seq.length s))
+        (ensures fun res -> exists* s' .
+            pts_to a s' **
+            pure (SZ.v i < Seq.length s /\
+              s' == Seq.upd s (SZ.v i) v
+            ))
+
+val share
+  (#a:Type)
+  (arr:ptr a)
+  (#s:Ghost.erased (Seq.seq a))
+  (#p:perm)
+: stt_ghost unit emp_inames
+      (requires pts_to arr #p s)
+      (ensures fun _ -> pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s)
+
+[@@allow_ambiguous]
+val gather
+  (#a:Type)
+  (arr:ptr a)
+  (#s0 #s1:Ghost.erased (Seq.seq a))
+  (#p0 #p1:perm)
+: stt_ghost unit emp_inames
+      (requires pts_to arr #p0 s0 ** pts_to arr #p1 s1 ** pure (Seq.length s0 == Seq.length s1))
+      (ensures fun _ -> pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1))
+
+
+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)
+    (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 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))
+
+val memcpy
+    (#t:Type0) (#p0:perm)
+    (src:ptr t) (idx_src: SZ.t)
+    (dst:ptr t) (idx_dst: SZ.t)
+    (len: SZ.t)
+    (#s0:Ghost.erased (Seq.seq t) { SZ.v idx_src + SZ.v len <= Seq.length s0 })
+    (#s1:Ghost.erased (Seq.seq t) { SZ.v idx_dst + SZ.v len <= Seq.length s1 })
+  : stt unit
+    (pts_to src #p0 s0 ** pts_to dst s1)
+    (fun _ -> pts_to src #p0 s0 ** pts_to dst (Seq.slice s0 0 (SZ.v len) `Seq.append` Seq.slice s1 (SZ.v len) (Seq.length s1)))
diff --git a/lib/pulse/lib/Pulse.Lib.HigherArray.fst b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
index 1247c6e07..d468a2af1 100644
--- a/lib/pulse/lib/Pulse.Lib.HigherArray.fst
+++ b/lib/pulse/lib/Pulse.Lib.HigherArray.fst
@@ -904,7 +904,6 @@ ensures
 
 let pts_to_range_upd = pts_to_range_upd'
 
-```pulse
 ghost
 fn pts_to_range_share
   (#a:Type)
@@ -922,9 +921,7 @@ fn pts_to_range_share
   pts_to_range_intro_ij arr (p /. 2.0R) s l r ();
   pts_to_range_intro_ij arr (p /. 2.0R) s l r ();
 }
-```
 
-```pulse
 ghost
 fn pts_to_range_gather
   (#a:Type)
@@ -942,4 +939,3 @@ fn pts_to_range_gather
   gather (array_slice arr l r);
   fold (pts_to_range arr l r #(p0 +. p1) s0)
 }
-```
diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst
new file mode 100644
index 000000000..9155f4a0b
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst
@@ -0,0 +1,99 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Lib.Slice.Util
+#lang-pulse
+include Pulse.Lib.Pervasives
+include Pulse.Lib.Slice
+include Pulse.Lib.Trade
+
+module S = Pulse.Lib.Slice
+module SZ = FStar.SizeT
+
+inline_for_extraction
+noextract
+fn append_split (#t: Type) (s: S.slice t) (#p: perm) (i: SZ.t)
+    (#v1: Ghost.erased (Seq.seq t) { SZ.v i == Seq.length v1 })
+    (#v2: Ghost.erased (Seq.seq t))
+  requires pts_to s #p (v1 `Seq.append` v2)
+  returns res: S.slice_pair t
+  ensures
+    (let S.SlicePair s1 s2 = res in
+      pts_to s1 #p v1 **
+      pts_to s2 #p v2 **
+      S.is_split s s1 s2)
+{
+  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.split s i
+}
+
+ghost
+fn append_split_trade_aux
+  (#t: Type) (input: S.slice t) (p: perm) (v1 v2: (Seq.seq t)) (i: SZ.t) (input1 input2: S.slice t) (_: unit)
+    requires S.is_split input input1 input2 ** (pts_to input1 #p v1 ** pts_to input2 #p v2)
+    ensures pts_to input #p (v1 `Seq.append` v2)
+{
+  S.join input1 input2 input
+}
+
+inline_for_extraction
+noextract
+fn append_split_trade (#t: Type) (input: S.slice t) (#p: perm) (i: SZ.t)
+    (#v1: Ghost.erased (Seq.seq t) { SZ.v i == Seq.length v1 })
+    (#v2: Ghost.erased (Seq.seq t))
+  requires pts_to input #p (v1 `Seq.append` v2)
+  returns res: S.slice_pair t
+  ensures
+    (let SlicePair s1 s2 = res in
+      pts_to s1 #p v1 ** pts_to s2 #p v2 **
+      trade (pts_to s1 #p v1 ** pts_to s2 #p v2)
+        (pts_to input #p (v1 `Seq.append` v2)))
+{
+  let SlicePair s1 s2 = append_split input i;
+  intro_trade _ _ _ (append_split_trade_aux input p v1 v2 i s1 s2);
+  SlicePair s1 s2
+}
+
+ghost
+fn split_trade_aux
+  (#t: Type) (s: S.slice t) (p: perm) (v: Seq.seq t) (i: SZ.t)
+  (s1 s2: S.slice t) (v1 v2: Seq.seq t) (hyp: squash (v == Seq.append v1 v2)) (_: unit)
+    requires (S.is_split s s1 s2 ** (pts_to s1 #p v1 ** pts_to s2 #p v2))
+    ensures (pts_to s #p v)
+{
+  S.join s1 s2 s
+}
+
+inline_for_extraction
+noextract
+fn split_trade (#t: Type) (s: 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: S.slice_pair t
+  ensures
+    (let SlicePair s1 s2 = res in
+      let v1 = Seq.slice v 0 (SZ.v i) in
+      let v2 = Seq.slice v (SZ.v i) (Seq.length v) in
+      pts_to s1 #p v1 ** pts_to s2 #p v2 **
+      trade (pts_to s1 #p v1 ** pts_to s2 #p v2)
+        (pts_to s #p (v1 `Seq.append` v2)))
+{
+  Seq.lemma_split v (SZ.v i);
+  let SlicePair s1 s2 = S.split s i;
+  with v1 v2. assert pts_to s1 #p v1 ** pts_to s2 #p v2;
+  intro_trade _ _ _ (split_trade_aux s p v i s1 s2 v1 v2 ());
+  S.SlicePair s1 s2
+}
diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst
new file mode 100644
index 000000000..85486df77
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.Slice.fst
@@ -0,0 +1,230 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Lib.Slice
+#lang-pulse
+
+module AP = Pulse.Lib.ArrayPtr
+
+noeq
+type slice t = {
+    elt: AP.ptr t;
+    len: SZ.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))
+}
+
+ghost fn unfold_pts_to #t (s: slice t) #p v
+  requires pts_to s #p v
+  ensures 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 **
+    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 **
+    pure (Seq.length v == SZ.v s.len)
+  ensures pts_to s #p v
+{
+  rewrite pts_to s.elt #p v **
+      pure (Seq.length v == SZ.v s.len)
+    as pts_to s #p v;
+}
+
+let pts_to_is_slprop2 x p v = ()
+
+ghost
+fn pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t)
+  requires pts_to s #p v
+  ensures pts_to s #p v ** pure (Seq.length v == SZ.v (len s))
+{
+    unfold_pts_to s #p v;
+    fold_pts_to s #p v
+}
+
+let is_from_array a s =
+  AP.is_from_array s.elt (SZ.v s.len) a
+
+fn from_array (#t: Type) (a: array t) (#p: perm) (alen: SZ.t)
+    (#v: Ghost.erased (Seq.seq t) { SZ.v alen == A.length a })
+  requires A.pts_to a #p v
+  returns s: (slice t)
+  ensures 
+    pts_to s #p v **
+    is_from_array a s
+{
+    A.pts_to_len a;
+    let ptr = AP.from_array a;
+    let res : slice t = {
+        elt = ptr;
+        len = alen;
+    };
+    fold_pts_to res #p v;
+    fold is_from_array a res;
+    res
+}
+
+ghost
+fn to_array
+    (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t)
+requires    (pts_to s #p v ** is_from_array a s)
+ensures    (A.pts_to a #p v)
+{
+    unfold_pts_to s #p v;
+    unfold is_from_array a s;
+    AP.to_array s.elt a
+}
+
+fn op_Array_Access
+        (#t: Type)
+        (a: slice t)
+        (i: SZ.t)
+        (#p: perm)
+        (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s})
+        requires
+            pts_to a #p s
+returns res : t
+ensures
+            pts_to a #p s **
+            pure (res == Seq.index s (SZ.v i))
+{
+    unfold_pts_to a #p s;
+    let res = AP.op_Array_Access a.elt i;
+    fold_pts_to a #p s;
+    res
+}
+
+fn op_Array_Assignment
+        (#t: Type)
+        (a: slice t)
+        (i: SZ.t)
+        (v: t)
+        (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s})
+        requires
+            pts_to a s
+        ensures
+            pts_to a (Seq.upd s (SZ.v i) v)
+{
+    unfold_pts_to a s;
+    AP.op_Array_Assignment a.elt i v;
+    fold_pts_to a (Seq.upd s (SZ.v i) v)
+}
+
+ghost
+fn share
+  (#a:Type)
+  (arr:slice a)
+  (#s:Ghost.erased (Seq.seq a))
+  (#p:perm)
+requires
+    pts_to arr #p s
+ensures pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s
+{
+    unfold_pts_to arr #p s;
+    AP.share arr.elt;
+    fold_pts_to arr #(p /. 2.0R) s;
+    fold_pts_to arr #(p /. 2.0R) s
+}
+
+ghost
+fn gather
+  (#a:Type)
+  (arr:slice a)
+  (#s0 #s1:Ghost.erased (Seq.seq a))
+  (#p0 #p1:perm)
+requires pts_to arr #p0 s0 ** pts_to arr #p1 s1
+ensures pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1)
+{
+    unfold_pts_to arr #p0 s0;
+    unfold_pts_to arr #p1 s1;
+    AP.gather arr.elt;
+    fold_pts_to arr #(p0 +. p1) s0
+}
+
+let is_split #t s s1 s2 =
+    pure (
+        s1.elt == s.elt /\
+        AP.adjacent s1.elt (SZ.v s1.len) s2.elt /\
+        SZ.v s.len == SZ.v s1.len + SZ.v s2.len
+    )
+
+let is_split_is_slprop2 s s1 s2 = ()
+
+fn 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 : slice_pair t
+  ensures
+    (let SlicePair s1 s2 = res in
+    pts_to s1 #p (Seq.slice v 0 (SZ.v i)) **
+    pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)) **
+    is_split s s1 s2)
+{
+    unfold_pts_to s #p v;
+    Seq.lemma_split v (SZ.v i);
+    let elt' = AP.split s.elt #p #v 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 `SlicePair` 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
+    ensures pts_to s #p (Seq.append v1 v2)
+{
+    unfold (is_split s s1 s2);
+    unfold_pts_to s1 #p v1;
+    unfold_pts_to s2 #p v2;
+    AP.join s1.elt s2.elt;
+    fold_pts_to s #p (Seq.append v1 v2)
+}
+
+fn copy
+  (#t: Type) (dst: slice t) (#p: perm) (src: slice t) (#v: Ghost.erased (Seq.seq t))
+requires
+  (exists* v_dst . pts_to dst v_dst ** pts_to src #p v ** pure (len src == len dst))
+ensures
+  (pts_to dst v ** pts_to src #p v)
+{
+  with v_dst . assert (pts_to dst v_dst);
+  unfold_pts_to dst v_dst;
+  unfold_pts_to src #p v;
+  AP.memcpy src.elt 0sz dst.elt 0sz src.len;
+  fold_pts_to src #p v;
+  assert pure (v `Seq.equal`
+    Seq.append (Seq.slice v 0 (SZ.v src.len))
+      (Seq.slice v_dst (SZ.v src.len) (Seq.length v_dst)));
+  fold_pts_to dst v
+}
diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Slice.fsti
new file mode 100644
index 000000000..b7fc4794b
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti
@@ -0,0 +1,115 @@
+(*
+   Copyright 2024 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+
+module Pulse.Lib.Slice
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives
+module SZ = FStar.SizeT
+module A = Pulse.Lib.Array
+
+val slice : 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_is_slprop2 (#a:Type) (x:slice a) (p:perm) (s:Seq.seq a)
+  : Lemma (is_slprop2 (pts_to x #p s))
+          [SMTPat (is_slprop2 (pts_to x #p s))]
+
+val pts_to_len (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) : stt_ghost unit emp_inames
+    (pts_to s #p v)
+    (fun _ -> pts_to s #p v ** pure (Seq.length v == SZ.v (len s)))
+
+val is_from_array (#t: Type) (a: array t) (s: slice t) : slprop
+
+val from_array (#t: Type) (a: array t) (#p: perm) (alen: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v alen == A.length a }) : stt (slice t)
+    (A.pts_to a #p v)
+    (fun s -> pts_to s #p v ** is_from_array a s)
+
+val to_array (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t) : stt_ghost unit emp_inames
+    (pts_to s #p v ** is_from_array a s)
+    (fun _ -> A.pts_to a #p v)
+
+(* Written x.(i) *)
+val op_Array_Access
+        (#t: Type)
+        (a: slice t)
+        (i: SZ.t)
+        (#p: perm)
+        (#s: Ghost.erased (Seq.seq t){SZ.v i < Seq.length s})
+  : stt t
+        (requires
+            pts_to a #p s)
+        (ensures fun res ->
+            pts_to a #p s **
+            pure (res == Seq.index s (SZ.v i)))
+
+
+(* Written a.(i) <- v *)
+val op_Array_Assignment
+        (#t: Type)
+        (a: slice t)
+        (i: SZ.t)
+        (v: t)
+        (#s: Ghost.erased (Seq.seq t) {SZ.v i < Seq.length s})
+  : stt unit
+        (requires
+            pts_to a s)
+        (ensures fun res ->
+            pts_to a (Seq.upd s (SZ.v i) v))
+
+val share
+  (#a:Type)
+  (arr:slice a)
+  (#s:Ghost.erased (Seq.seq a))
+  (#p:perm)
+: stt_ghost unit emp_inames
+      (requires pts_to arr #p s)
+      (ensures fun _ -> pts_to arr #(p /. 2.0R) s ** pts_to arr #(p /. 2.0R) s)
+
+[@@allow_ambiguous]
+val gather
+  (#a:Type)
+  (arr:slice a)
+  (#s0 #s1:Ghost.erased (Seq.seq a))
+  (#p0 #p1:perm)
+: stt_ghost unit emp_inames
+      (requires pts_to arr #p0 s0 ** pts_to arr #p1 s1)
+      (ensures fun _ -> pts_to arr #(p0 +. p1) s0 ** pure (s0 == s1))
+
+val is_split (#t: Type) (s: slice t) (left: slice t) (right: slice t) : slprop
+
+val is_split_is_slprop2 (#t: Type) (s: slice t) (left: slice t) (right: slice t)
+  : Lemma (is_slprop2 (is_split s left right))
+          [SMTPat (is_slprop2 (is_split s left right))]
+
+noeq type slice_pair (t: Type) = | SlicePair: (fst: slice t) -> (snd: slice t) -> slice_pair t
+
+val split (#t: Type) (s: slice t) (#p: perm) (i: SZ.t) (#v: Ghost.erased (Seq.seq t) { SZ.v i <= Seq.length v }) : stt (slice_pair t)
+    (requires pts_to s #p v)
+    (ensures fun (SlicePair s1 s2) ->
+      pts_to s1 #p (Seq.slice v 0 (SZ.v i)) **
+      pts_to s2 #p (Seq.slice v (SZ.v i) (Seq.length v)) **
+      is_split s s1 s2)
+
+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))
+
+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)
diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst
index 35abfe4f9..2ca88e832 100644
--- a/pulse2rust/src/Pulse2Rust.Extract.fst
+++ b/pulse2rust/src/Pulse2Rust.Extract.fst
@@ -183,6 +183,10 @@ let rec extract_mlty (g:env) (t:S.mlty) : typ =
     when S.string_of_mlpath p = "Pulse.Lib.Array.Core.array" ->
     let is_mut = true in
     mk_slice is_mut arg
+  | S.MLTY_Named ([arg], p)
+    when S.string_of_mlpath p = "Pulse.Lib.Slice.slice" ->
+    let is_mut = true in
+    mk_slice is_mut arg
   | S.MLTY_Named ([arg; _], p)
     when S.string_of_mlpath p = "Pulse.Lib.Array.Core.larray" ->
     let is_mut = true in
@@ -402,6 +406,10 @@ let rec extract_mlpattern_to_pat (g:env) (p:S.mlpattern) : env & pat =
     let g, ps = fold_left_map extract_mlpattern_to_pat g ps in
     g,
     mk_pat_tuple ps
+  | S.MLP_CTor (p, ps) when snd p = "SlicePair" ->
+    let g, ps = fold_left_map extract_mlpattern_to_pat g ps in
+    g,
+    mk_pat_tuple ps
   | S.MLP_CTor (p, ps) ->
     let g, ps = fold_left_map extract_mlpattern_to_pat g ps in
     let path =
@@ -610,6 +618,7 @@ 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.Array.Core.op_Array_Access" ||
          S.string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_index" ||
+         S.string_of_mlpath p = "Pulse.Lib.Slice.op_Array_Access" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.op_Array_Access" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.read_ref" ->
 
@@ -618,6 +627,7 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
   | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e1::e2::e3::_)
     when S.string_of_mlpath p = "Pulse.Lib.Array.Core.op_Array_Assignment" ||
          S.string_of_mlpath p = "Pulse.Lib.Array.Core.pts_to_range_upd" ||
+         S.string_of_mlpath p = "Pulse.Lib.Slice.op_Array_Assignment" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.op_Array_Assignment" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.write_ref" ->
 
@@ -644,6 +654,18 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
                    (extract_mlexpr g e_r)
                    (extract_mlexpr g e_x)
 
+  | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, e::_)
+    when S.string_of_mlpath p = "Pulse.Lib.Slice.from_array" ->
+    extract_mlexpr g e
+  | 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}, [_])}, 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]
+  | S.MLE_App ({expr=S.MLE_TApp ({expr=S.MLE_Name p}, [_])}, [a])
+    when S.string_of_mlpath p = "Pulse.Lib.Slice.len" ->
+    mk_method_call (extract_mlexpr g a) "len" []
 
     //
     // vec_as_array e extracted to &mut e
diff --git a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml
index ebff33497..3a8a53f53 100644
--- a/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml
+++ b/pulse2rust/src/ocaml/generated/Pulse2Rust_Extract.ml
@@ -238,6 +238,10 @@ let rec (extract_mlty :
           let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in
           uu___ = "Pulse.Lib.Array.Core.array" ->
           let is_mut = true in mk_slice is_mut arg
+      | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when
+          let uu___ = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+          uu___ = "Pulse.Lib.Slice.slice" ->
+          let is_mut = true in mk_slice is_mut arg
       | FStar_Extraction_ML_Syntax.MLTY_Named (arg::uu___::[], p) when
           let uu___1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
           uu___1 = "Pulse.Lib.Array.Core.larray" ->
@@ -577,6 +581,14 @@ let rec (extract_mlpattern_to_pat :
            | (g1, ps1) ->
                let uu___1 = Pulse2Rust_Rust_Syntax.mk_pat_tuple ps1 in
                (g1, uu___1))
+      | FStar_Extraction_ML_Syntax.MLP_CTor (p1, ps) when
+          (FStar_Pervasives_Native.snd p1) = "SlicePair" ->
+          let uu___ =
+            FStar_Compiler_List.fold_left_map extract_mlpattern_to_pat g ps in
+          (match uu___ with
+           | (g1, ps1) ->
+               let uu___1 = Pulse2Rust_Rust_Syntax.mk_pat_tuple ps1 in
+               (g1, uu___1))
       | FStar_Extraction_ML_Syntax.MLP_CTor (p1, ps) ->
           let uu___ =
             FStar_Compiler_List.fold_left_map extract_mlpattern_to_pat g ps in
@@ -1091,10 +1103,13 @@ and (extract_mlexpr :
              FStar_Extraction_ML_Syntax.loc = uu___4;_},
            e1::i::uu___5)
           when
-          (((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-             uu___6 = "Pulse.Lib.Array.Core.op_Array_Access") ||
+          ((((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+              uu___6 = "Pulse.Lib.Array.Core.op_Array_Access") ||
+               (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+                uu___6 = "Pulse.Lib.Array.Core.pts_to_range_index"))
+              ||
               (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-               uu___6 = "Pulse.Lib.Array.Core.pts_to_range_index"))
+               uu___6 = "Pulse.Lib.Slice.op_Array_Access"))
              ||
              (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
               uu___6 = "Pulse.Lib.Vec.op_Array_Access"))
@@ -1119,10 +1134,13 @@ and (extract_mlexpr :
              FStar_Extraction_ML_Syntax.loc = uu___4;_},
            e1::e2::e3::uu___5)
           when
-          (((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-             uu___6 = "Pulse.Lib.Array.Core.op_Array_Assignment") ||
+          ((((let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+              uu___6 = "Pulse.Lib.Array.Core.op_Array_Assignment") ||
+               (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+                uu___6 = "Pulse.Lib.Array.Core.pts_to_range_upd"))
+              ||
               (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-               uu___6 = "Pulse.Lib.Array.Core.pts_to_range_upd"))
+               uu___6 = "Pulse.Lib.Slice.op_Array_Assignment"))
              ||
              (let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
               uu___6 = "Pulse.Lib.Vec.op_Array_Assignment"))
@@ -1183,6 +1201,79 @@ and (extract_mlexpr :
           let uu___6 = extract_mlexpr g e_r in
           let uu___7 = extract_mlexpr g e_x in
           Pulse2Rust_Rust_Syntax.mk_mem_replace uu___5 uu___6 uu___7
+      | FStar_Extraction_ML_Syntax.MLE_App
+          ({
+             FStar_Extraction_ML_Syntax.expr =
+               FStar_Extraction_ML_Syntax.MLE_TApp
+               ({
+                  FStar_Extraction_ML_Syntax.expr =
+                    FStar_Extraction_ML_Syntax.MLE_Name p;
+                  FStar_Extraction_ML_Syntax.mlty = uu___;
+                  FStar_Extraction_ML_Syntax.loc = uu___1;_},
+                uu___2::[]);
+             FStar_Extraction_ML_Syntax.mlty = uu___3;
+             FStar_Extraction_ML_Syntax.loc = uu___4;_},
+           e1::uu___5)
+          when
+          let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+          uu___6 = "Pulse.Lib.Slice.from_array" -> extract_mlexpr g e1
+      | FStar_Extraction_ML_Syntax.MLE_App
+          ({
+             FStar_Extraction_ML_Syntax.expr =
+               FStar_Extraction_ML_Syntax.MLE_TApp
+               ({
+                  FStar_Extraction_ML_Syntax.expr =
+                    FStar_Extraction_ML_Syntax.MLE_Name p;
+                  FStar_Extraction_ML_Syntax.mlty = uu___;
+                  FStar_Extraction_ML_Syntax.loc = uu___1;_},
+                uu___2::[]);
+             FStar_Extraction_ML_Syntax.mlty = uu___3;
+             FStar_Extraction_ML_Syntax.loc = uu___4;_},
+           e1::uu___5::i::uu___6)
+          when
+          let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+          uu___7 = "Pulse.Lib.Slice.split" ->
+          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
+      | FStar_Extraction_ML_Syntax.MLE_App
+          ({
+             FStar_Extraction_ML_Syntax.expr =
+               FStar_Extraction_ML_Syntax.MLE_TApp
+               ({
+                  FStar_Extraction_ML_Syntax.expr =
+                    FStar_Extraction_ML_Syntax.MLE_Name p;
+                  FStar_Extraction_ML_Syntax.mlty = uu___;
+                  FStar_Extraction_ML_Syntax.loc = uu___1;_},
+                uu___2::[]);
+             FStar_Extraction_ML_Syntax.mlty = uu___3;
+             FStar_Extraction_ML_Syntax.loc = uu___4;_},
+           a::uu___5::b::uu___6)
+          when
+          let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+          uu___7 = "Pulse.Lib.Slice.copy" ->
+          let uu___7 = extract_mlexpr g a in
+          let uu___8 = let uu___9 = extract_mlexpr g b in [uu___9] in
+          Pulse2Rust_Rust_Syntax.mk_method_call uu___7 "copy_from_slice"
+            uu___8
+      | FStar_Extraction_ML_Syntax.MLE_App
+          ({
+             FStar_Extraction_ML_Syntax.expr =
+               FStar_Extraction_ML_Syntax.MLE_TApp
+               ({
+                  FStar_Extraction_ML_Syntax.expr =
+                    FStar_Extraction_ML_Syntax.MLE_Name p;
+                  FStar_Extraction_ML_Syntax.mlty = uu___;
+                  FStar_Extraction_ML_Syntax.loc = uu___1;_},
+                uu___2::[]);
+             FStar_Extraction_ML_Syntax.mlty = uu___3;
+             FStar_Extraction_ML_Syntax.loc = uu___4;_},
+           a::[])
+          when
+          let uu___5 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+          uu___5 = "Pulse.Lib.Slice.len" ->
+          let uu___5 = extract_mlexpr g a in
+          Pulse2Rust_Rust_Syntax.mk_method_call uu___5 "len" []
       | FStar_Extraction_ML_Syntax.MLE_App
           ({
              FStar_Extraction_ML_Syntax.expr =
diff --git a/pulse2rust/tests/Makefile b/pulse2rust/tests/Makefile
index fd2b02dc1..74fd26498 100644
--- a/pulse2rust/tests/Makefile
+++ b/pulse2rust/tests/Makefile
@@ -1,7 +1,7 @@
 PULSE_HOME ?= ../..
 PULSE_EXAMPLES_ROOT ?= $(PULSE_HOME)/share/pulse/examples
 
-SRC_DIRS := $(addprefix $(PULSE_EXAMPLES_ROOT)/,by-example dice/external dice/external/hacl dice/external/l0 dice/dpe dice/engine dice/l0)
+SRC_DIRS := $(addprefix $(PULSE_EXAMPLES_ROOT)/,. by-example dice/external dice/external/hacl dice/external/l0 dice/dpe dice/engine dice/l0)
 ifneq (,$(wildcard $(PULSE_EXAMPLES_ROOT)/dice/_output/cache))
 SRC_DIRS += $(PULSE_EXAMPLES_ROOT)/dice/_output/cache
 endif
@@ -16,9 +16,11 @@ CACHE_DIRECTORY := $(OUTPUT_DIRECTORY)/cache
 FSTAR_OPTIONS += --warn_error -342 --cmi
 
 MAIN=../main.exe
-RUST_SRC_DIR=./src/
+RUST_SRC_DIR=src
+RUST_OUT_DIR=out
 DPE_OUTPUT_DIR=../dpe/src/generated
 
+.PHONY: all
 all: test dpe
 
 include $(PULSE_HOME)/share/pulse/Makefile.include
@@ -60,35 +62,46 @@ FSTAR_DEP_OPTIONS=--extract '* -FStar.Tactics -FStar.Reflection -Pulse +Pulse.Cl
 # files. If so, then this %.ast rule will be generic and can move to
 # share/pulse/Makefile.include-base.
 
-%.ast:
+$(OUTPUT_DIRECTORY)/%.ast:
 		$(FSTAR) --admit_smt_queries true --codegen Extension $(subst .ast,.fst, $(subst _,., $(notdir $@))) --extract_module $(basename $(subst .ast,.fst, $(subst _,., $(notdir $@))))
 
-pulsetutorial-array.rs: PulseTutorial_Array.ast
-	$(MAIN) -odir $(RUST_SRC_DIR) $(addprefix $(OUTPUT_DIRECTORY)/, $^)
+$(RUST_SRC_DIR)/pulsetutorial_array.rs: $(OUTPUT_DIRECTORY)/PulseTutorial_Array.ast
+	$(MAIN) -odir $(RUST_SRC_DIR) $+
 
-pulsetutorial-loops.rs: PulseTutorial_Loops.ast
-	$(MAIN) -odir $(RUST_SRC_DIR) $(addprefix $(OUTPUT_DIRECTORY)/, $^)
+$(RUST_SRC_DIR)/pulsetutorial_loops.rs: $(OUTPUT_DIRECTORY)/PulseTutorial_Loops.ast
+	$(MAIN) -odir $(RUST_SRC_DIR) $+
 
-pulsetutorial-algorithms.rs: PulseTutorial_Algorithms.ast
-	$(MAIN) -odir $(RUST_SRC_DIR) $(addprefix $(OUTPUT_DIRECTORY)/, $^)
+$(RUST_SRC_DIR)/pulsetutorial_algorithms.rs: $(OUTPUT_DIRECTORY)/PulseTutorial_Algorithms.ast
+	$(MAIN) -odir $(RUST_SRC_DIR) $+
 
-DPE_FILES = EngineTypes.ast \
-  EngineCore.ast \
+$(RUST_SRC_DIR)/example_slice.rs: $(OUTPUT_DIRECTORY)/Example_Slice.ast
+	$(MAIN) -odir $(RUST_SRC_DIR) $+
+
+%.rlib: %.rs
+	rustc --crate-type rlib -o $@ $+
+
+DPE_FILES = $(addprefix $(OUTPUT_DIRECTORY)/, \
+	EngineTypes.ast \
+	EngineCore.ast \
 	HACL.ast \
 	L0Types.ast \
 	Pulse_Lib_HashTable_Type.ast \
 	Pulse_Lib_HashTable_Spec.ast \
 	Pulse_Lib_HashTable.ast \
 	DPETypes.ast \
-	DPE.ast
+	DPE.ast \
+)
 
 DPE_LIB = L0Core,Pulse.Lib.Array,FStar.SizeT,EverCrypt.HMAC,EverCrypt.Hash.Incremental,EverCrypt.Ed25519,EverCrypt.AutoConfig2,Spec.Hash.Definitions
 
+.PHONY: dpe.rs
 dpe.rs: $(DPE_FILES)
-	$(MAIN) -odir $(DPE_OUTPUT_DIR)/ -lib $(DPE_LIB) $(addprefix $(OUTPUT_DIRECTORY)/, $^)
+	$(MAIN) -odir $(DPE_OUTPUT_DIR)/ -lib $(DPE_LIB) $^
 
-all-rs: pulsetutorial-loops.rs pulsetutorial-algorithms.rs
+.PHONY: all-rs
+all-rs: $(addprefix $(RUST_SRC_DIR)/, pulsetutorial_loops.rlib pulsetutorial_algorithms.rs pulsetutorial_array.rs example_slice.rlib)
 
+.PHONY: test
 test: all-rs
 	cargo test
 
@@ -96,6 +109,7 @@ test: all-rs
 external:
 	../dpe/gen-rust-bindings.sh
 
+.PHONY: dpe
 dpe: dpe.rs external
 	cd ../dpe && cargo build && cd -
 	$(MAKE) -C ../dpe -f c.Makefile
diff --git a/pulse2rust/tests/src/.gitignore b/pulse2rust/tests/src/.gitignore
new file mode 100644
index 000000000..e9e98e15f
--- /dev/null
+++ b/pulse2rust/tests/src/.gitignore
@@ -0,0 +1 @@
+*.rlib
diff --git a/pulse2rust/tests/src/example_slice.rs b/pulse2rust/tests/src/example_slice.rs
new file mode 100644
index 000000000..17fde9346
--- /dev/null
+++ b/pulse2rust/tests/src/example_slice.rs
@@ -0,0 +1,21 @@
+////
+////
+//// This file is generated by the Pulse2Rust tool
+////
+////
+
+pub fn test(arr: &mut [u8]) -> () {
+    let slice = arr;
+    let _letpattern = slice.split_at_mut(2);
+    match _letpattern {
+        (mut s1, mut s2) => {
+            let x = s2[s1.len()];
+            s1[1] = x;
+            let _letpattern1 = s2.split_at_mut(2);
+            match _letpattern1 {
+                (mut s3, mut s4) => s3.copy_from_slice(s4),
+            }
+        }
+    }
+}
+
diff --git a/pulse2rust/tests/src/pulsetutorial_array.rs b/pulse2rust/tests/src/pulsetutorial_array.rs
new file mode 100644
index 000000000..abbc90465
--- /dev/null
+++ b/pulse2rust/tests/src/pulsetutorial_array.rs
@@ -0,0 +1,94 @@
+////
+////
+//// This file is generated by the Pulse2Rust tool
+////
+////
+
+pub fn read_i<T: Copy>(arr: &mut [T], p: (), s: (), i: usize) -> T {
+    arr[i]
+}
+pub fn write_i<T>(arr: &mut [T], s: (), x: T, i: usize) -> () {
+    arr[i] = x;
+}
+pub fn compare<T: PartialEq + Copy>(
+    p1: (),
+    p2: (),
+    a1: &mut [T],
+    a2: &mut [T],
+    l: usize,
+    __s1: (),
+    __s2: (),
+) -> bool {
+    let mut i = 0;
+    while {
+        let vi = i;
+        if vi < l {
+            let v1 = a1[vi];
+            let v2 = a2[vi];
+            v1 == v2
+        } else {
+            false
+        }
+    } {
+        let vi = i;
+        i = vi + 1;
+    }
+    let vi = i;
+    let res = vi == l;
+    let i1 = res;
+    i1
+}
+pub fn copy<T: Copy>(
+    a1: &mut [T],
+    a2: &mut [T],
+    l: usize,
+    p2: (),
+    __s1: (),
+    __s2: (),
+) -> () {
+    let mut i = 0;
+    while {
+        let vi = i;
+        vi < l
+    } {
+        let vi = i;
+        let v = a2[vi];
+        a1[vi] = v;
+        i = vi + 1;
+    }
+}
+pub fn copy2<T: Copy>(
+    a1: &mut [T],
+    a2: &mut [T],
+    l: usize,
+    p2: (),
+    __s1: (),
+    __s2: (),
+) -> () {
+    let mut i = 0;
+    while {
+        let vi = i;
+        vi < l
+    } {
+        let vi = i;
+        let v = a2[vi];
+        a1[vi] = v;
+        i = vi + 1;
+    }
+}
+pub fn compare_stack_arrays(uu___: ()) -> () {
+    let a1 = &mut [0; 2];
+    let a2 = &mut [0; 2];
+    let b = super::pulsetutorial_array::compare((), (), a1, a2, 2, (), ());
+}
+pub fn heap_arrays(uu___: ()) -> std::vec::Vec<i64> {
+    let mut a1 = vec![0; 2];
+    let mut a2 = vec![0; 2];
+    drop(a1);
+    a2
+}
+pub fn copy_app(mut v: std::vec::Vec<i64>) -> () {
+    let a = &mut [0; 2];
+    super::pulsetutorial_array::copy2(&mut v, a, 2, (), (), ())
+}
+
diff --git a/share/pulse/examples/Example.Slice.fst b/share/pulse/examples/Example.Slice.fst
new file mode 100644
index 000000000..ded284bfe
--- /dev/null
+++ b/share/pulse/examples/Example.Slice.fst
@@ -0,0 +1,40 @@
+(*
+   Copyright 2023 Microsoft Research
+
+   Licensed under the Apache License, Version 2.0 (the "License");
+   you may not use this file except in compliance with the License.
+   You may obtain a copy of the License at
+
+       http://www.apache.org/licenses/LICENSE-2.0
+
+   Unless required by applicable law or agreed to in writing, software
+   distributed under the License is distributed on an "AS IS" BASIS,
+   WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+   See the License for the specific language governing permissions and
+   limitations under the License.
+*)
+module Example.Slice
+#lang-pulse
+open Pulse
+open Pulse.Lib.Slice
+module A = Pulse.Lib.Array
+
+fn test (arr: A.array UInt8.t)
+    requires pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy; 5uy]
+    ensures exists* s. pts_to arr s ** pure (s `Seq.equal` seq![0uy; 4uy; 4uy; 5uy; 4uy; 5uy]) {
+  A.pts_to_len arr;
+  let slice = from_array arr 6sz;
+  let SlicePair s1 s2 = split slice 2sz;
+  pts_to_len s1;
+  share s2;
+  let x = s2.(len s1);
+  s1.(1sz) <- x;
+  gather s2;
+  let SlicePair s3 s4 = split s2 2sz;
+  pts_to_len s3;
+  pts_to_len s4;
+  copy s3 s4;
+  join s3 s4 s2;
+  join s1 s2 slice;
+  to_array slice;
+}
\ No newline at end of file
diff --git a/share/pulse/examples/Makefile b/share/pulse/examples/Makefile
index 0f0e17787..0bfc8aabf 100755
--- a/share/pulse/examples/Makefile
+++ b/share/pulse/examples/Makefile
@@ -20,6 +20,9 @@ $(OUTPUT_DIRECTORY)/Example_Hashtable.c: $(addprefix $(OUTPUT_DIRECTORY)/,\
 	Pulse_Lib_Vec.krml \
 	Pulse_Lib_HashTable_Type.krml Pulse_Lib_HashTable_Spec.krml Pulse_Lib_HashTable.krml)
 
+$(OUTPUT_DIRECTORY)/Example_Slice.c: $(addprefix $(OUTPUT_DIRECTORY)/,\
+	Pulse_Lib_Slice.krml)
+
 $(OUTPUT_DIRECTORY)/Example_Unreachable.c: $(addprefix $(OUTPUT_DIRECTORY)/,FStar_Pervasives.krml FStar_Pervasives_Native.krml)
 
 $(OUTPUT_DIRECTORY)/%.c: $(EXTRA_KRML_DEPS) $(OUTPUT_DIRECTORY)/%.krml
@@ -31,6 +34,8 @@ extract: $(OUTPUT_DIRECTORY)/ExtractionTest.ml
 .PHONY: extract_unreachable
 extract_unreachable: $(OUTPUT_DIRECTORY)/Example_Unreachable.ml
 
+EXTRACT_C_FILES = $(addprefix $(OUTPUT_DIRECTORY)/,ExtractionTest.c PulsePointStruct.c Bug166.c Example_Unreachable.c Example_Hashtable.c Example_Slice.c)
+
 ifneq (,$(KRML_HOME))
 test-dpe-c: dice
 	+$(MAKE) -C dice test-c
@@ -38,38 +43,24 @@ test-dpe-c: dice
 test-cbor: dice
 	+$(MAKE) -C dice/cbor
 
-extract_c: $(OUTPUT_DIRECTORY)/ExtractionTest.c
-
-extract_pulse_c: $(OUTPUT_DIRECTORY)/PulsePointStruct.c
-
-extract_c_bug166: $(OUTPUT_DIRECTORY)/Bug166.c
-
-extract_c_unreachable: $(OUTPUT_DIRECTORY)/Example_Unreachable.c
-
-extract_c_hashtable: $(OUTPUT_DIRECTORY)/Example_Hashtable.c
-
 else
 test-dpe-c:
 
 test-cbor:
 
-extract_c:
-
-extract_pulse_c:
-
-extract_c_bug166:
-
-extract_c_unreachable:
+EXTRACT_C_FILES =
 
 endif
 
-test: test-cbor extract extract_pulse_c extract_c extract_c_bug166 test-dpe-c test-error-messages extract_c_unreachable extract_c_hashtable
+extract_c: $(EXTRACT_C_FILES)
+
+test: test-cbor extract extract_pulse_c extract_c test-dpe-c test-error-messages
 
 test-error-messages:
 	+$(MAKE) -C bug-reports/error-messages
 
 .PHONY: test-dpe-c test-error-messages
 
-.PHONY: extract_pulse_c extract_c extract_c_bug166 extract_c_unreachable extract_c_hashtable
+.PHONY: extract_pulse_c extract_c
 
 .PHONY: test test-cbor test-cbor-raw
diff --git a/share/pulse/examples/bug-reports/Bug166.fst b/share/pulse/examples/bug-reports/Bug166.fst
index 38f3e08c8..fa08771e3 100644
--- a/share/pulse/examples/bug-reports/Bug166.fst
+++ b/share/pulse/examples/bug-reports/Bug166.fst
@@ -1,8 +1,8 @@
 module Bug166
 open Pulse
+#lang-pulse
 
 inline_for_extraction noextract
-```pulse
 fn h ()
   requires emp
   returns  x : int
@@ -10,5 +10,4 @@ fn h ()
 {
   42
 }
-```
 let h2 = h
\ No newline at end of file
diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst
index 64a944ce9..484ce3004 100644
--- a/src/extraction/ExtractPulse.fst
+++ b/src/extraction/ExtractPulse.fst
@@ -41,6 +41,7 @@ let pulse_translate_type_without_decay : translate_type_without_decay_t = fun en
     (let p = Syntax.string_of_mlpath p in
      p = "Pulse.Lib.Reference.ref" ||
      p = "Pulse.Lib.Array.Core.array" ||
+     p = "Pulse.Lib.ArrayPtr.ptr" ||
      p = "Pulse.Lib.Vec.vec" ||
      p = "Pulse.Lib.Box.box")
     ->
@@ -118,6 +119,28 @@ let pulse_translate_expr : translate_expr_t = fun env e ->
     when string_of_mlpath p = "Pulse.Lib.Array.Core.free" ->
     EBufFree (cb x)
 
+  (* Pulse array pointers (ArrayPtr, as an underlying C extraction for slices *)
+  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ e; i; _p; _w ])
+    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Access" ->
+    EBufRead (translate_expr env e, translate_expr env i)
+
+  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ x; _p; _w ])
+    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.from_array" ->
+    translate_expr env x
+
+  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ a; _p; _w; i ])
+    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.split" ->
+    EBufSub (translate_expr env a, translate_expr env i)
+
+  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, (e :: i :: v :: _))
+    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Assignment" ->
+    EBufWrite (translate_expr env e, translate_expr env i, translate_expr env v)
+
+  | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ _; e1; e2; e3; e4; e5; _; _ ])
+    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.memcpy" ->
+    EBufBlit (translate_expr env e1, translate_expr env e2, translate_expr env e3, translate_expr env e4, translate_expr env e5)
+
+
   (* Pulse control, while etc *)
   | MLE_App ({expr=MLE_Name p}, [{expr=MLE_Fun (_, test)}; {expr=MLE_Fun(_, body)}])
     when (string_of_mlpath p = "Pulse.Lib.Dv.while_") ->
diff --git a/src/ocaml/plugin/generated/ExtractPulse.ml b/src/ocaml/plugin/generated/ExtractPulse.ml
index 2382123d6..678fe03e1 100644
--- a/src/ocaml/plugin/generated/ExtractPulse.ml
+++ b/src/ocaml/plugin/generated/ExtractPulse.ml
@@ -28,8 +28,9 @@ let (pulse_translate_type_without_decay :
       match t with
       | FStar_Extraction_ML_Syntax.MLTY_Named (arg::[], p) when
           let p1 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
-          (((p1 = "Pulse.Lib.Reference.ref") ||
-              (p1 = "Pulse.Lib.Array.Core.array"))
+          ((((p1 = "Pulse.Lib.Reference.ref") ||
+               (p1 = "Pulse.Lib.Array.Core.array"))
+              || (p1 = "Pulse.Lib.ArrayPtr.ptr"))
              || (p1 = "Pulse.Lib.Vec.vec"))
             || (p1 = "Pulse.Lib.Box.box")
           ->
@@ -404,6 +405,111 @@ let (pulse_translate_expr : FStar_Extraction_Krml.translate_expr_t) =
            let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
            uu___6 = "Pulse.Lib.Array.Core.free" ->
            let uu___6 = cb x in FStar_Extraction_Krml.EBufFree uu___6
+       | FStar_Extraction_ML_Syntax.MLE_App
+           ({
+              FStar_Extraction_ML_Syntax.expr =
+                FStar_Extraction_ML_Syntax.MLE_TApp
+                ({
+                   FStar_Extraction_ML_Syntax.expr =
+                     FStar_Extraction_ML_Syntax.MLE_Name p;
+                   FStar_Extraction_ML_Syntax.mlty = uu___1;
+                   FStar_Extraction_ML_Syntax.loc = uu___2;_},
+                 uu___3);
+              FStar_Extraction_ML_Syntax.mlty = uu___4;
+              FStar_Extraction_ML_Syntax.loc = uu___5;_},
+            e2::i::_p::_w::[])
+           when
+           let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+           uu___6 = "Pulse.Lib.ArrayPtr.op_Array_Access" ->
+           let uu___6 =
+             let uu___7 = FStar_Extraction_Krml.translate_expr env e2 in
+             let uu___8 = FStar_Extraction_Krml.translate_expr env i in
+             (uu___7, uu___8) in
+           FStar_Extraction_Krml.EBufRead uu___6
+       | FStar_Extraction_ML_Syntax.MLE_App
+           ({
+              FStar_Extraction_ML_Syntax.expr =
+                FStar_Extraction_ML_Syntax.MLE_TApp
+                ({
+                   FStar_Extraction_ML_Syntax.expr =
+                     FStar_Extraction_ML_Syntax.MLE_Name p;
+                   FStar_Extraction_ML_Syntax.mlty = uu___1;
+                   FStar_Extraction_ML_Syntax.loc = uu___2;_},
+                 uu___3);
+              FStar_Extraction_ML_Syntax.mlty = uu___4;
+              FStar_Extraction_ML_Syntax.loc = uu___5;_},
+            x::_p::_w::[])
+           when
+           let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+           uu___6 = "Pulse.Lib.ArrayPtr.from_array" ->
+           FStar_Extraction_Krml.translate_expr env x
+       | FStar_Extraction_ML_Syntax.MLE_App
+           ({
+              FStar_Extraction_ML_Syntax.expr =
+                FStar_Extraction_ML_Syntax.MLE_TApp
+                ({
+                   FStar_Extraction_ML_Syntax.expr =
+                     FStar_Extraction_ML_Syntax.MLE_Name p;
+                   FStar_Extraction_ML_Syntax.mlty = uu___1;
+                   FStar_Extraction_ML_Syntax.loc = uu___2;_},
+                 uu___3);
+              FStar_Extraction_ML_Syntax.mlty = uu___4;
+              FStar_Extraction_ML_Syntax.loc = uu___5;_},
+            a::_p::_w::i::[])
+           when
+           let uu___6 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+           uu___6 = "Pulse.Lib.ArrayPtr.split" ->
+           let uu___6 =
+             let uu___7 = FStar_Extraction_Krml.translate_expr env a in
+             let uu___8 = FStar_Extraction_Krml.translate_expr env i in
+             (uu___7, uu___8) in
+           FStar_Extraction_Krml.EBufSub uu___6
+       | FStar_Extraction_ML_Syntax.MLE_App
+           ({
+              FStar_Extraction_ML_Syntax.expr =
+                FStar_Extraction_ML_Syntax.MLE_TApp
+                ({
+                   FStar_Extraction_ML_Syntax.expr =
+                     FStar_Extraction_ML_Syntax.MLE_Name p;
+                   FStar_Extraction_ML_Syntax.mlty = uu___1;
+                   FStar_Extraction_ML_Syntax.loc = uu___2;_},
+                 uu___3);
+              FStar_Extraction_ML_Syntax.mlty = uu___4;
+              FStar_Extraction_ML_Syntax.loc = uu___5;_},
+            e2::i::v::uu___6)
+           when
+           let uu___7 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+           uu___7 = "Pulse.Lib.ArrayPtr.op_Array_Assignment" ->
+           let uu___7 =
+             let uu___8 = FStar_Extraction_Krml.translate_expr env e2 in
+             let uu___9 = FStar_Extraction_Krml.translate_expr env i in
+             let uu___10 = FStar_Extraction_Krml.translate_expr env v in
+             (uu___8, uu___9, uu___10) in
+           FStar_Extraction_Krml.EBufWrite uu___7
+       | FStar_Extraction_ML_Syntax.MLE_App
+           ({
+              FStar_Extraction_ML_Syntax.expr =
+                FStar_Extraction_ML_Syntax.MLE_TApp
+                ({
+                   FStar_Extraction_ML_Syntax.expr =
+                     FStar_Extraction_ML_Syntax.MLE_Name p;
+                   FStar_Extraction_ML_Syntax.mlty = uu___1;
+                   FStar_Extraction_ML_Syntax.loc = uu___2;_},
+                 uu___3);
+              FStar_Extraction_ML_Syntax.mlty = uu___4;
+              FStar_Extraction_ML_Syntax.loc = uu___5;_},
+            uu___6::e11::e2::e3::e4::e5::uu___7::uu___8::[])
+           when
+           let uu___9 = FStar_Extraction_ML_Syntax.string_of_mlpath p in
+           uu___9 = "Pulse.Lib.ArrayPtr.memcpy" ->
+           let uu___9 =
+             let uu___10 = FStar_Extraction_Krml.translate_expr env e11 in
+             let uu___11 = FStar_Extraction_Krml.translate_expr env e2 in
+             let uu___12 = FStar_Extraction_Krml.translate_expr env e3 in
+             let uu___13 = FStar_Extraction_Krml.translate_expr env e4 in
+             let uu___14 = FStar_Extraction_Krml.translate_expr env e5 in
+             (uu___10, uu___11, uu___12, uu___13, uu___14) in
+           FStar_Extraction_Krml.EBufBlit uu___9
        | FStar_Extraction_ML_Syntax.MLE_App
            ({
               FStar_Extraction_ML_Syntax.expr =