diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 72ec8427e..b3242e539 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -54,8 +54,8 @@ jobs:
         id: checkout-karamel
         with:
           path: karamel
-          repository: mtzguido/karamel
-          ref: dev
+          repository: FStarLang/karamel
+          ref: _taramana_mutable_slice
 
       - name: Try fetch built karamel
         id: cache-karamel
diff --git a/lib/pulse/lib/Pulse.Lib.ConstArrayPtr.fst b/lib/pulse/lib/Pulse.Lib.ConstArrayPtr.fst
new file mode 100644
index 000000000..a3f0593e8
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.ConstArrayPtr.fst
@@ -0,0 +1,47 @@
+module Pulse.Lib.ConstArrayPtr
+#lang-pulse
+
+module Trade = Pulse.Lib.Trade.Util
+
+let ptr a = AP.ptr a
+
+let base p = AP.base p
+let offset p = AP.offset p
+
+let has_pts_to_array_ptr t = AP.has_pts_to_array_ptr t
+
+let pts_to_timeless x p s = ()
+
+fn from_arrayptr
+  (#t: Type)
+  (a: AP.ptr t)
+  (#p: perm)
+  (#v: Ghost.erased (Seq.seq t))
+requires
+  pts_to a #p v
+returns s: ptr t
+ensures
+  pts_to s #p v ** Trade.trade (pts_to s #p v) (pts_to a #p v)
+{
+  let s : ptr t = a;
+  Trade.rewrite_with_trade (pts_to a #p v) (pts_to s #p v);
+  s
+}
+
+let is_from_array #t s sz a = AP.is_from_array #t s sz a
+
+let from_array #t a #p #v = AP.from_array #t a #p #v
+
+let to_array #t s a #p #v = AP.to_array #t s a #p #v
+
+let op_Array_Access #t a i #p #s = AP.op_Array_Access #t a i #p #s
+
+let share #a arr #s #p = AP.share #a arr #s #p
+
+let gather #a arr #s0 #s1 #p0 #p1 = AP.gather #a arr #s0 #s1 #p0 #p1
+
+let split #t s #p i #v = AP.split #t s #p i #v
+
+let ghost_split #t s #p i #v = AP.ghost_split #t s #p i #v
+
+let join #t s1 #p #v1 s2 #v2 = AP.join #t s1 #p #v1 s2 #v2
diff --git a/lib/pulse/lib/Pulse.Lib.ConstArrayPtr.fsti b/lib/pulse/lib/Pulse.Lib.ConstArrayPtr.fsti
new file mode 100644
index 000000000..846bbe60e
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.ConstArrayPtr.fsti
@@ -0,0 +1,121 @@
+(*
+   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.ConstArrayPtr
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives
+module SZ = FStar.SizeT
+module A = Pulse.Lib.Array
+module AP = Pulse.Lib.ArrayPtr
+module Trade = Pulse.Lib.Trade
+
+(*
+The `ConstArrayPtr.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 ([@@@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_timeless (#a:Type) (x:ptr a) (p:perm) (s:Seq.seq a)
+  : Lemma (timeless (pts_to x #p s))
+          [SMTPat (timeless (pts_to x #p s))]
+
+val from_arrayptr (#t: Type) (a: AP.ptr t) (#p: perm) (#v: Ghost.erased (Seq.seq t)) : stt (ptr t)
+    (pts_to a #p v)
+    (fun s -> pts_to s #p v ** Trade.trade (pts_to s #p v) (pts_to a #p v))
+
+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)))
+
+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) (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))
diff --git a/lib/pulse/lib/Pulse.Lib.MutableSlice.Util.fst b/lib/pulse/lib/Pulse.Lib.MutableSlice.Util.fst
new file mode 100644
index 000000000..49293f442
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.MutableSlice.Util.fst
@@ -0,0 +1,268 @@
+(*
+   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.MutableSlice.Util
+#lang-pulse
+include Pulse.Lib.Pervasives
+include Pulse.Lib.MutableSlice
+include Pulse.Lib.Trade
+
+module S = Pulse.Lib.MutableSlice
+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: (slice t & slice t)
+  ensures
+    (let (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
+}
+
+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: (slice t & slice t)
+  ensures
+    (let (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 s = append_split input i;
+  match s {
+    Mktuple2 s1 s2 -> {
+      ghost fn aux ()
+        requires S.is_split input s1 s2 ** (pts_to s1 #p v1 ** pts_to s2 #p v2)
+        ensures pts_to input #p (v1 `Seq.append` v2)
+      {
+        S.join s1 s2 input
+      };
+      intro_trade _ _ _ aux;
+      (s1, s2)
+    }
+  }
+}
+
+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: (slice t & slice t)
+  ensures
+    (let (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 v))
+{
+  Seq.lemma_split v (SZ.v i);
+  let s' = S.split s i;
+  match s' {
+    Mktuple2 s1 s2 -> {
+      with v1 v2. assert pts_to s1 #p v1 ** pts_to s2 #p v2;
+      ghost fn aux ()
+        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
+      };
+      intro_trade _ _ _ aux;
+      (s1, s2)
+    }
+  }
+}
+
+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 })
+  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;
+  ghost fn aux (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))));
+  };
+  intro_forall _ (fun v' -> intro_trade _ _ _ (aux v'));
+  res
+}
+
+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;
+  ghost fn aux ()
+    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))));
+  };
+  intro_trade _ _ _ aux;
+  res
+}
+
+(* BEGIN C only (see comment in Pulse.Lib.Slice) *)
+
+module AP = Pulse.Lib.ArrayPtr
+
+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))
+  returns s: slice t
+  ensures
+    (pts_to s #p v **
+      trade
+        (pts_to s #p v)
+        (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
+  {
+    arrayptr_to_slice_elim s
+  };
+  intro_trade _ _ _ aux;
+  s
+}
+
+inline_for_extraction
+fn slice_to_arrayptr_intro_trade
+  (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
+requires
+  (pts_to s #p v)
+returns a: AP.ptr t
+ensures
+  (pts_to a #p v **
+    trade
+      (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
+    ensures pts_to s #p v
+  {
+    slice_to_arrayptr_elim a;
+  };
+  intro_trade _ _ _ aux;
+  a
+}
+
+(* END C only *)
diff --git a/lib/pulse/lib/Pulse.Lib.MutableSlice.fst b/lib/pulse/lib/Pulse.Lib.MutableSlice.fst
new file mode 100644
index 000000000..88878326e
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.MutableSlice.fst
@@ -0,0 +1,342 @@
+(*
+   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.MutableSlice
+#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_timeless 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
+}
+
+let arrayptr_to_slice
+  #t a s
+= pure (s.elt == a)
+
+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))
+  returns s: slice t
+  ensures
+    (pts_to s #p v ** arrayptr_to_slice a s)
+{
+  let s : slice t = {
+    elt = a;
+    len = alen;
+  };
+  fold_pts_to s #p v;
+  fold arrayptr_to_slice a s;
+  s
+}
+
+ghost
+fn arrayptr_to_slice_elim
+  (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: AP.ptr t)
+requires
+  (pts_to s #p v ** arrayptr_to_slice a s)
+ensures
+  (pts_to a #p v)
+{
+  unfold (arrayptr_to_slice a s);
+  unfold_pts_to s #p v;
+}
+
+let slice_to_arrayptr
+  #t s a
+= pure (s.elt == a)
+
+fn slice_to_arrayptr_intro
+  (#t: Type) (s: slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
+requires
+  (pts_to s #p v)
+returns a: AP.ptr t
+ensures
+  (pts_to a #p v ** slice_to_arrayptr s a)
+{
+  unfold_pts_to s #p v;
+  fold (slice_to_arrayptr s s.elt);
+  s.elt
+}
+
+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)))
+ensures
+  (pts_to s #p v)
+{
+  unfold (slice_to_arrayptr s a);
+  fold_pts_to s #p v
+}
+
+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_timeless 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 t & slice t)
+  ensures
+    (let (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 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 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
+    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 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
+  (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.MutableSlice.fsti b/lib/pulse/lib/Pulse.Lib.MutableSlice.fsti
new file mode 100644
index 000000000..d9db128cd
--- /dev/null
+++ b/lib/pulse/lib/Pulse.Lib.MutableSlice.fsti
@@ -0,0 +1,168 @@
+(*
+   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.MutableSlice
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives
+module SZ = FStar.SizeT
+module A = Pulse.Lib.Array
+
+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_timeless (#a:Type) (x:slice a) (p:perm) (s:Seq.seq a)
+  : Lemma (timeless (pts_to x #p s))
+          [SMTPat (timeless (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)
+
+(* BEGIN C only: conversions to/from Pulse.Lib.ArrayPtr. Those are
+   meant to design "clean" C APIs without the need to monomorphize
+   the slice type in the extracted .h file. *)
+
+module AP = Pulse.Lib.ArrayPtr
+
+val arrayptr_to_slice
+  (#t: Type)
+  (a: AP.ptr t)
+  (s: slice t)
+: 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))
+    (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)
+
+val slice_to_arrayptr
+  (#t: Type)
+  (s: slice t)
+  (a: AP.ptr t)
+: slprop
+
+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)
+
+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)))
+    (fun _ -> pts_to s #p v)
+
+(* END C only *)
+
+(* 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_timeless (#t: Type) (s: slice t) (left: slice t) (right: slice t)
+  : Lemma (timeless (is_split s left right))
+          [SMTPat (timeless (is_split s left right))]
+
+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 t & slice t)
+    (requires pts_to s #p v)
+    (ensures fun (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 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))
+
+(* `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)
diff --git a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst
index a5bc8e2d8..dfb94f6ff 100644
--- a/lib/pulse/lib/Pulse.Lib.Slice.Util.fst
+++ b/lib/pulse/lib/Pulse.Lib.Slice.Util.fst
@@ -214,7 +214,7 @@ fn subslice_trade #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v
 
 (* BEGIN C only (see comment in Pulse.Lib.Slice) *)
 
-module AP = Pulse.Lib.ArrayPtr
+module AP = Pulse.Lib.ConstArrayPtr
 
 inline_for_extraction
 fn arrayptr_to_slice_intro_trade
diff --git a/lib/pulse/lib/Pulse.Lib.Slice.fst b/lib/pulse/lib/Pulse.Lib.Slice.fst
index a7a38684f..cf2336111 100644
--- a/lib/pulse/lib/Pulse.Lib.Slice.fst
+++ b/lib/pulse/lib/Pulse.Lib.Slice.fst
@@ -17,7 +17,8 @@
 module Pulse.Lib.Slice
 #lang-pulse
 
-module AP = Pulse.Lib.ArrayPtr
+module AP = Pulse.Lib.ConstArrayPtr
+module Trade = Pulse.Lib.Trade.Util
 
 noeq
 type slice t = {
@@ -159,6 +160,39 @@ ensures
   fold_pts_to s #p v
 }
 
+fn from_mutable_slice
+  (#t: Type) (s: MS.slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
+requires
+  pts_to s #p v
+returns res: slice t
+ensures
+  pts_to res #p v ** Trade.trade (pts_to res #p v) (pts_to s #p v)
+{
+  let len = MS.len s;
+  MS.pts_to_len s;
+  let a = MS.slice_to_arrayptr_intro s;
+  ghost fn aux (_: unit)
+  requires MS.slice_to_arrayptr s a ** pts_to a #p v
+  ensures pts_to s #p v
+  {
+    MS.slice_to_arrayptr_elim a;
+  };
+  Trade.intro _ _ _ aux;
+  let ca = AP.from_arrayptr a;
+  Trade.trans _ _ (pts_to s #p v);
+  let res = arrayptr_to_slice_intro ca len;
+  pts_to_len res;
+  ghost fn aux2 (_: unit)
+  requires arrayptr_to_slice ca res ** pts_to res #p v
+  ensures pts_to ca #p v
+  {
+    arrayptr_to_slice_elim res
+  };
+  Trade.intro _ _ _ aux2;
+  Trade.trans _ _ (pts_to s #p v);
+  res
+}
+
 fn op_Array_Access
         (#t: Type)
         (a: slice t)
@@ -178,22 +212,6 @@ ensures
     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)
@@ -322,21 +340,3 @@ fn subslice #t (s: slice t) #p (i j: SZ.t) (#v: erased (Seq.seq t) { SZ.v i <= S
   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
-  (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
index ba4cfe77b..4c3cfb46b 100644
--- a/lib/pulse/lib/Pulse.Lib.Slice.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Slice.fsti
@@ -19,6 +19,8 @@ open FStar.Tactics.V2
 open Pulse.Lib.Pervasives
 module SZ = FStar.SizeT
 module A = Pulse.Lib.Array
+module Trade = Pulse.Lib.Trade
+module MS = Pulse.Lib.MutableSlice
 
 val slice ([@@@strictly_positive] elt: Type0) : Type0
 
@@ -44,11 +46,11 @@ val to_array (#t: Type) (s: slice t) (#p: perm) (#v: Seq.seq t) (#a: array t) :
     (pts_to s #p v ** is_from_array a s)
     (fun _ -> A.pts_to a #p v)
 
-(* BEGIN C only: conversions to/from Pulse.Lib.ArrayPtr. Those are
+(* BEGIN C only: conversions to/from Pulse.Lib.ConstArrayPtr. Those are
    meant to design "clean" C APIs without the need to monomorphize
    the slice type in the extracted .h file. *)
 
-module AP = Pulse.Lib.ArrayPtr
+module AP = Pulse.Lib.ConstArrayPtr
 
 val arrayptr_to_slice
   (#t: Type)
@@ -80,6 +82,12 @@ val slice_to_arrayptr_elim (#t: Type) (a: AP.ptr t) (#p: perm) (#v: Seq.seq t) (
 
 (* END C only *)
 
+val from_mutable_slice
+  (#t: Type) (s: MS.slice t) (#p: perm) (#v: Ghost.erased (Seq.seq t))
+: stt (slice t)
+  (pts_to s #p v)
+  (fun res -> pts_to res #p v ** Trade.trade (pts_to res #p v) (pts_to s #p v))
+
 (* Written x.(i) *)
 val op_Array_Access
         (#t: Type)
@@ -94,20 +102,6 @@ val op_Array_Access
             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)
@@ -162,7 +156,3 @@ let subslice_rest #t (r: slice t) (s: slice t) p (i j: SZ.t) (v: erased (Seq.seq
 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)
diff --git a/lib/pulse/lib/Pulse.Lib.Sort.Merge.Slice.fst b/lib/pulse/lib/Pulse.Lib.Sort.Merge.Slice.fst
index cd6312c7d..0c8134af7 100644
--- a/lib/pulse/lib/Pulse.Lib.Sort.Merge.Slice.fst
+++ b/lib/pulse/lib/Pulse.Lib.Sort.Merge.Slice.fst
@@ -3,11 +3,11 @@ module Pulse.Lib.Sort.Merge.Slice
 open Pulse.Lib.Pervasives
 include Pulse.Lib.Sort.Base
 include Pulse.Lib.Sort.Merge.Spec
-include Pulse.Lib.Slice.Util
+include Pulse.Lib.MutableSlice.Util
 open Pulse.Lib.Sort.Merge.Common
 
 module SM = Pulse.Lib.SeqMatch.Util
-module S = Pulse.Lib.Slice.Util
+module S = Pulse.Lib.MutableSlice.Util
 module AS = Pulse.Lib.Swap.Slice
 module SZ = FStar.SizeT
 module R = Pulse.Lib.Reference
diff --git a/lib/pulse/lib/Pulse.Lib.Swap.Slice.fsti b/lib/pulse/lib/Pulse.Lib.Swap.Slice.fsti
index e8a4cb8aa..d5736ef68 100644
--- a/lib/pulse/lib/Pulse.Lib.Swap.Slice.fsti
+++ b/lib/pulse/lib/Pulse.Lib.Swap.Slice.fsti
@@ -17,7 +17,7 @@
 module Pulse.Lib.Swap.Slice
 open Pulse.Lib.Pervasives
 module SZ = FStar.SizeT
-module S = Pulse.Lib.Slice
+module S = Pulse.Lib.MutableSlice
 
 inline_for_extraction noextract [@@noextract_to "krml"]
 val slice_swap
diff --git a/pulse2rust/src/Pulse2Rust.Extract.fst b/pulse2rust/src/Pulse2Rust.Extract.fst
index f1f5d14f9..f71c18a0d 100644
--- a/pulse2rust/src/Pulse2Rust.Extract.fst
+++ b/pulse2rust/src/Pulse2Rust.Extract.fst
@@ -185,6 +185,10 @@ let rec extract_mlty (g:env) (t:S.mlty) : typ =
     mk_slice is_mut arg
   | S.MLTY_Named ([arg], p)
     when S.string_of_mlpath p = "Pulse.Lib.Slice.slice" ->
+    let is_mut = false in
+    mk_slice is_mut arg
+  | S.MLTY_Named ([arg], p)
+    when S.string_of_mlpath p = "Pulse.Lib.MutableSlice.slice" ->
     let is_mut = true in
     mk_slice is_mut arg
   | S.MLTY_Named ([arg; _], p)
@@ -612,6 +616,7 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
     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.MutableSlice.op_Array_Access" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.op_Array_Access" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.read_ref" ->
 
@@ -620,7 +625,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.MutableSlice.op_Array_Assignment" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.op_Array_Assignment" ||
          S.string_of_mlpath p = "Pulse.Lib.Vec.write_ref" ->
 
@@ -648,20 +653,30 @@ and extract_mlexpr (g:env) (e:S.mlexpr) : expr =
                    (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" ->
+    when S.string_of_mlpath p = "Pulse.Lib.Slice.from_array"
+     || S.string_of_mlpath p = "Pulse.Lib.MutableSlice.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" ->
+    when S.string_of_mlpath p = "Pulse.Lib.Slice.split"
+    ||  S.string_of_mlpath p = "Pulse.Lib.MutableSlice.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 = false in
+    mk_reference_expr mutb (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}, [_])}, s::_::a::b::_)
+    when S.string_of_mlpath p = "Pulse.Lib.MutableSlice.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))))
+    mk_reference_expr mutb (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" ->
+    when S.string_of_mlpath p = "Pulse.Lib.MutableSlice.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" ->
+    when S.string_of_mlpath p = "Pulse.Lib.Slice.len"
+    || S.string_of_mlpath p = "Pulse.Lib.MutableSlice.len"
+    ->
     mk_method_call (extract_mlexpr g a) "len" []
 
     //
diff --git a/src/extraction/ExtractPulse.fst b/src/extraction/ExtractPulse.fst
index 27a654cfa..253c557c4 100644
--- a/src/extraction/ExtractPulse.fst
+++ b/src/extraction/ExtractPulse.fst
@@ -43,6 +43,11 @@ let pulse_translate_type_without_decay : translate_type_without_decay_t = fun en
      p = "Pulse.Lib.Box.box")
     ->
       TBuf (translate_type_without_decay env arg)
+  | MLTY_Named ([arg], p) when
+    (let p = Syntax.string_of_mlpath p in
+     p = "Pulse.Lib.ConstArrayPtr.ptr")
+    ->
+      TConstBuf (translate_type_without_decay env arg)
   
   | MLTY_Named ([arg; _], p) when Syntax.string_of_mlpath p = "Pulse.Lib.GlobalVar.gvar" ->
       translate_type_without_decay env arg
@@ -128,15 +133,21 @@ let pulse_translate_expr : translate_expr_t = fun env e ->
 
   (* 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" ->
+    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.op_Array_Access"
+    || string_of_mlpath p = "Pulse.Lib.ConstArrayPtr.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" ->
+    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.from_array"
+    || string_of_mlpath p = "Pulse.Lib.ConstArrayPtr.from_array"
+    ->
     translate_expr env x
 
   | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, [ a; _p; i; _w ])
-    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.split" ->
+    when string_of_mlpath p = "Pulse.Lib.ArrayPtr.split"
+    || string_of_mlpath p = "Pulse.Lib.ConstArrayPtr.split"
+    ->
     EBufSub (translate_expr env a, translate_expr env i)
 
   | MLE_App ({ expr = MLE_TApp({ expr = MLE_Name p }, _) }, (e :: i :: v :: _))
diff --git a/test/Example.MutableSlice.fst b/test/Example.MutableSlice.fst
new file mode 100644
index 000000000..a57ef2ef4
--- /dev/null
+++ b/test/Example.MutableSlice.fst
@@ -0,0 +1,56 @@
+(*
+   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.MutableSlice
+#lang-pulse
+open Pulse
+open Pulse.Lib.Trade
+open Pulse.Lib.MutableSlice.Util
+module A = Pulse.Lib.Array
+module UInt8 = FStar.UInt8
+
+fn test (arr: A.array UInt8.t)
+    requires pts_to arr seq![0uy; 1uy; 2uy; 3uy; 4uy; 5uy]
+    returns res: UInt8.t
+    ensures exists* s. pts_to arr s ** pure (s `Seq.equal` seq![0uy; 5uy; 4uy; 5uy; 4uy; 5uy]) {
+  A.pts_to_len arr;
+  let slice = from_array arr 6sz;
+  let s' = split slice 2sz;
+  match s' {
+    Mktuple2 s1 s2 -> {
+      pts_to_len s1;
+      share s2;
+      let s2' = subslice_trade s2 1sz 4sz;
+      let x = s2'.(len s1);
+      s1.(1sz) <- x;
+      elim_trade _ _;
+      gather s2;
+      let s' = split s2 2sz;
+      match s' {
+        Mktuple2 s3 s4 -> {
+          pts_to_len s3;
+          pts_to_len s4;
+          copy s3 s4;
+          let y = s3.(0sz);
+          let z = s4.(0sz);
+          join s3 s4 s2;
+          join s1 s2 slice;
+          to_array slice;
+          (x `UInt8.add` y `UInt8.add` z)
+        }
+      }
+    }
+  }
+}
diff --git a/test/Example.Slice.fst b/test/Example.Slice.fst
index c146ff38e..00df44158 100644
--- a/test/Example.Slice.fst
+++ b/test/Example.Slice.fst
@@ -19,10 +19,12 @@ open Pulse
 open Pulse.Lib.Trade
 open Pulse.Lib.Slice.Util
 module A = Pulse.Lib.Array
+module UInt8 = FStar.UInt8
 
 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; 5uy; 4uy; 5uy; 4uy; 5uy]) {
+    returns res: UInt8.t
+    ensures exists* s. pts_to arr s ** pure (s `Seq.equal` seq![0uy; 1uy; 2uy; 3uy; 4uy; 5uy]) {
   A.pts_to_len arr;
   let slice = from_array arr 6sz;
   let s' = split slice 2sz;
@@ -32,7 +34,6 @@ fn test (arr: A.array UInt8.t)
       share s2;
       let s2' = subslice_trade s2 1sz 4sz;
       let x = s2'.(len s1);
-      s1.(1sz) <- x;
       elim_trade _ _;
       gather s2;
       let s' = split s2 2sz;
@@ -40,10 +41,12 @@ fn test (arr: A.array UInt8.t)
         Mktuple2 s3 s4 -> {
           pts_to_len s3;
           pts_to_len s4;
-          copy s3 s4;
+          let y = s3.(0sz);
+          let z = s4.(0sz);
           join s3 s4 s2;
           join s1 s2 slice;
           to_array slice;
+          (x `UInt8.add` y `UInt8.add` z)
         }
       }
     }
diff --git a/test/Example_MutableSlice.c.expected b/test/Example_MutableSlice.c.expected
new file mode 100644
index 000000000..942ebe6c1
--- /dev/null
+++ b/test/Example_MutableSlice.c.expected
@@ -0,0 +1,87 @@
+/* krml header omitted for test repeatability */
+
+
+#include "Example_MutableSlice.h"
+
+typedef struct slice__uint8_t_s
+{
+  uint8_t *elt;
+  size_t len;
+}
+slice__uint8_t;
+
+static slice__uint8_t from_array__uint8_t(uint8_t *a, size_t alen)
+{
+  uint8_t *ptr = a;
+  return ((slice__uint8_t){ .elt = ptr, .len = alen });
+}
+
+typedef struct __Pulse_Lib_MutableSlice_slice_uint8_t_Pulse_Lib_MutableSlice_slice_uint8_t_s
+{
+  slice__uint8_t fst;
+  slice__uint8_t snd;
+}
+__Pulse_Lib_MutableSlice_slice_uint8_t_Pulse_Lib_MutableSlice_slice_uint8_t;
+
+static __Pulse_Lib_MutableSlice_slice_uint8_t_Pulse_Lib_MutableSlice_slice_uint8_t
+split__uint8_t(slice__uint8_t s, size_t i)
+{
+  uint8_t *elt_ = s.elt + i;
+  slice__uint8_t s1 = { .elt = s.elt, .len = i };
+  slice__uint8_t s2 = { .elt = elt_, .len = s.len - i };
+  return
+    (
+      (__Pulse_Lib_MutableSlice_slice_uint8_t_Pulse_Lib_MutableSlice_slice_uint8_t){
+        .fst = s1,
+        .snd = s2
+      }
+    );
+}
+
+static slice__uint8_t subslice__uint8_t(slice__uint8_t s, size_t i, size_t j)
+{
+  uint8_t *elt_ = s.elt + i;
+  return ((slice__uint8_t){ .elt = elt_, .len = j - i });
+}
+
+static uint8_t op_Array_Access__uint8_t(slice__uint8_t a, size_t i)
+{
+  return a.elt[i];
+}
+
+static size_t len__uint8_t(slice__uint8_t s)
+{
+  return s.len;
+}
+
+static void op_Array_Assignment__uint8_t(slice__uint8_t a, size_t i, uint8_t v)
+{
+  a.elt[i] = v;
+}
+
+static void copy__uint8_t(slice__uint8_t dst, slice__uint8_t src)
+{
+  memcpy(dst.elt, src.elt, src.len * sizeof (uint8_t));
+}
+
+uint8_t Example_MutableSlice_test(uint8_t *arr)
+{
+  slice__uint8_t slice = from_array__uint8_t(arr, (size_t)6U);
+  __Pulse_Lib_MutableSlice_slice_uint8_t_Pulse_Lib_MutableSlice_slice_uint8_t
+  s_ = split__uint8_t(slice, (size_t)2U);
+  slice__uint8_t s1 = s_.fst;
+  slice__uint8_t s2 = s_.snd;
+  slice__uint8_t res = subslice__uint8_t(s2, (size_t)1U, (size_t)4U);
+  slice__uint8_t s2_ = res;
+  uint8_t x = op_Array_Access__uint8_t(s2_, len__uint8_t(s1));
+  op_Array_Assignment__uint8_t(s1, (size_t)1U, x);
+  __Pulse_Lib_MutableSlice_slice_uint8_t_Pulse_Lib_MutableSlice_slice_uint8_t
+  s_1 = split__uint8_t(s2, (size_t)2U);
+  slice__uint8_t s3 = s_1.fst;
+  slice__uint8_t s4 = s_1.snd;
+  copy__uint8_t(s3, s4);
+  uint8_t y = op_Array_Access__uint8_t(s3, (size_t)0U);
+  uint8_t z = op_Array_Access__uint8_t(s4, (size_t)0U);
+  return (uint32_t)x + (uint32_t)y + (uint32_t)z;
+}
+
diff --git a/test/Example_Slice.c.expected b/test/Example_Slice.c.expected
index e8514937f..55fa1e428 100644
--- a/test/Example_Slice.c.expected
+++ b/test/Example_Slice.c.expected
@@ -5,14 +5,14 @@
 
 typedef struct slice__uint8_t_s
 {
-  uint8_t *elt;
+  const uint8_t *elt;
   size_t len;
 }
 slice__uint8_t;
 
 static slice__uint8_t from_array__uint8_t(uint8_t *a, size_t alen)
 {
-  uint8_t *ptr = a;
+  const uint8_t *ptr = a;
   return ((slice__uint8_t){ .elt = ptr, .len = alen });
 }
 
@@ -26,7 +26,7 @@ __Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t;
 static __Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t
 split__uint8_t(slice__uint8_t s, size_t i)
 {
-  uint8_t *elt_ = s.elt + i;
+  const uint8_t *elt_ = s.elt + i;
   slice__uint8_t s1 = { .elt = s.elt, .len = i };
   slice__uint8_t s2 = { .elt = elt_, .len = s.len - i };
   return
@@ -35,7 +35,7 @@ split__uint8_t(slice__uint8_t s, size_t i)
 
 static slice__uint8_t subslice__uint8_t(slice__uint8_t s, size_t i, size_t j)
 {
-  uint8_t *elt_ = s.elt + i;
+  const uint8_t *elt_ = s.elt + i;
   return ((slice__uint8_t){ .elt = elt_, .len = j - i });
 }
 
@@ -49,17 +49,7 @@ static size_t len__uint8_t(slice__uint8_t s)
   return s.len;
 }
 
-static void op_Array_Assignment__uint8_t(slice__uint8_t a, size_t i, uint8_t v)
-{
-  a.elt[i] = v;
-}
-
-static void copy__uint8_t(slice__uint8_t dst, slice__uint8_t src)
-{
-  memcpy(dst.elt, src.elt, src.len * sizeof (uint8_t));
-}
-
-void Example_Slice_test(uint8_t *arr)
+uint8_t Example_Slice_test(uint8_t *arr)
 {
   slice__uint8_t slice = from_array__uint8_t(arr, (size_t)6U);
   __Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t
@@ -69,11 +59,12 @@ void Example_Slice_test(uint8_t *arr)
   slice__uint8_t res = subslice__uint8_t(s2, (size_t)1U, (size_t)4U);
   slice__uint8_t s2_ = res;
   uint8_t x = op_Array_Access__uint8_t(s2_, len__uint8_t(s1));
-  op_Array_Assignment__uint8_t(s1, (size_t)1U, x);
   __Pulse_Lib_Slice_slice_uint8_t_Pulse_Lib_Slice_slice_uint8_t
   s_1 = split__uint8_t(s2, (size_t)2U);
   slice__uint8_t s3 = s_1.fst;
   slice__uint8_t s4 = s_1.snd;
-  copy__uint8_t(s3, s4);
+  uint8_t y = op_Array_Access__uint8_t(s3, (size_t)0U);
+  uint8_t z = op_Array_Access__uint8_t(s4, (size_t)0U);
+  return (uint32_t)x + (uint32_t)y + (uint32_t)z;
 }
 
diff --git a/test/Makefile b/test/Makefile
index 2cb35b63d..f66900171 100644
--- a/test/Makefile
+++ b/test/Makefile
@@ -1,4 +1,4 @@
-SUBDIRS += bug-reports
+# SUBDIRS += bug-reports
 
 PULSE_ROOT ?= ..
 include $(PULSE_ROOT)/mk/test.mk
@@ -15,9 +15,31 @@ $(OUTPUT_DIR)/Example_Hashtable.c: $(addprefix $(OUTPUT_DIR)/,\
 	Pulse_Lib_HashTable_Spec.krml \
 	Pulse_Lib_HashTable.krml)
 
+$(OUTPUT_DIR)/Example_MutableSlice.c: $(addprefix $(OUTPUT_DIR)/,\
+	Pulse_Lib_MutableSlice.krml)
+
 $(OUTPUT_DIR)/Example_Slice.c: $(addprefix $(OUTPUT_DIR)/,\
 	Pulse_Lib_Slice.krml)
 
+$(OUTPUT_DIR)/example/mutableslice.rs: $(addprefix $(OUTPUT_DIR)/,\
+	Example_MutableSlice.krml \
+	Pulse_Lib_MutableSlice.krml)
+
+$(OUTPUT_DIR)/example/slice.rs: $(addprefix $(OUTPUT_DIR)/,\
+	Example_Slice.krml \
+	Pulse_Lib_Slice.krml)
+
 $(OUTPUT_DIR)/Example_Unreachable.c: $(addprefix $(OUTPUT_DIR)/,\
 	FStar_Pervasives.krml \
 	FStar_Pervasives_Native.krml)
+
+$(OUTPUT_DIR)/%.rs:
+	$(call msg, "KRML RS", $(basename $(notdir $@)))
+	$(KRML_EXE) -header=$(PULSE_ROOT)/mk/krmlheader -bundle $(basename $(notdir $<))=* -skip-compilation $+ -fkeep-tuples -tmpdir $(OUTPUT_DIR) -backend rust
+
+$(OUTPUT_DIR)/example/lib%.rlib: $(OUTPUT_DIR)/example/%.rs
+	$(call msg, "RUSTC", $(basename $(notdir $@)))
+	rustc --crate-type=rlib -o $@ $<
+
+__extract: $(OUTPUT_DIR)/example/libslice.rlib
+__extract: $(OUTPUT_DIR)/example/libmutableslice.rlib