diff --git a/src/program_proof/tulip/program/prelude.v b/src/program_proof/tulip/program/prelude.v
index c9092da4b..7b90b471b 100644
--- a/src/program_proof/tulip/program/prelude.v
+++ b/src/program_proof/tulip/program/prelude.v
@@ -28,7 +28,7 @@ Defined.
 
 #[global]
 Instance dbval_into_val_for_type : IntoValForType dbval (boolT * (stringT * unitT)%ht).
-Proof. constructor; [done | done | intros [v |]; by auto]. Defined.
+Proof. by constructor; [| | intros [v |]; auto]. Defined.
 
 Definition dbmod_to_val (x : dbmod) : val :=
   (#(LitString x.1), (dbval_to_val x.2, #())).
@@ -54,6 +54,11 @@ Proof.
   by destruct v.
 Defined.
 
+#[global]
+Instance dbmod_into_val_for_type :
+  IntoValForType dbmod (stringT * (boolT * (stringT * unitT) * unitT)%ht).
+Proof. by constructor; [| | intros [k [s |]]; auto 10]. Defined.
+
 Definition ppsl_to_val (v : ppsl) : val := (#v.1, (#v.2, #())).
 
 Definition ppsl_from_val (v : val) : option ppsl :=
diff --git a/src/program_proof/tulip/program/util/decode_kvmap_into_slice.v b/src/program_proof/tulip/program/util/decode_kvmap_into_slice.v
new file mode 100644
index 000000000..4a563741e
--- /dev/null
+++ b/src/program_proof/tulip/program/util/decode_kvmap_into_slice.v
@@ -0,0 +1,115 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.util Require Import decode_write_entry.
+From Perennial.program_proof Require Import marshal_stateless_proof.
+
+Section program.
+  Context `{!heapGS Σ, !paxos_ghostG Σ}.
+
+  Theorem wp_DecodeKVMapIntoSlice
+    (bsP : Slice.t) (m : dbmap) (mdata : list u8) (bstail : list u8) :
+    encode_dbmap m mdata ->
+    {{{ own_slice_small bsP byteT (DfracOwn 1) (mdata ++ bstail) }}}
+      DecodeKVMapIntoSlice (to_val bsP)
+    {{{ (entsP : Slice.t) (dataP : Slice.t), RET (to_val entsP, to_val dataP); 
+        own_dbmap_in_slice entsP m ∗
+        own_slice_small dataP byteT (DfracOwn 1) bstail
+    }}}.
+  Proof.
+    iIntros (Hmdata Φ) "Hbs HΦ".
+    wp_rec.
+    destruct Hmdata as (xs & Hmdata & Hxs).
+    iDestruct (own_slice_small_sz with "Hbs") as %Hlenbs.
+    assert (Hlenxs : length xs < 2 ^ 64).
+    { rewrite length_app in Hlenbs.
+      assert (Hlen : (length mdata ≤ uint.nat bsP.(Slice.sz))%nat) by lia.
+      rewrite Hmdata in Hlen.
+      apply encode_dbmods_length_inv in Hlen.
+      word.
+    }
+
+    (*@ func DecodeKVMapIntoSlice(bs []byte) ([]tulip.WriteEntry, []byte) {     @*)
+    (*@     n, bs1 := marshal.ReadInt(bs)                                       @*)
+    (*@                                                                         @*)
+    rewrite Hmdata /encode_dbmods -app_assoc.
+    wp_apply (wp_ReadInt with "Hbs").
+    iIntros (p) "Hxs".
+
+    (*@     var data = bs1                                                      @*)
+    (*@     var ents = make([]tulip.WriteEntry, 0, n)                           @*)
+    (*@                                                                         @*)
+    wp_apply wp_ref_to; first done.
+    iIntros (dataP) "HdataP".
+    wp_apply (wp_NewSliceWithCap (V:= dbmod)); first word.
+    iIntros (entsbaseP) "Hents".
+    wp_apply wp_ref_to; first done.
+    iIntros (entsP) "HentsP".
+
+    (*@     var i uint64 = 0                                                    @*)
+    (*@     for i < n {                                                         @*)
+    (*@         x, bsloop := DecodeWriteEntry(data)                             @*)
+    (*@         ents = append(ents, x)                                          @*)
+    (*@         data = bsloop                                                   @*)
+    (*@         i++                                                             @*)
+    (*@     }                                                                   @*)
+    (*@                                                                         @*)
+    wp_apply wp_ref_to; first by auto.
+    iIntros (iP) "HiP".
+    wp_pures.
+    set P := (λ cont : bool, ∃ (i : u64) (p1 p2 : Slice.t),
+                 let remaining := encode_dbmods_xlen (drop (uint.nat i) xs) ++ bstail in
+                 "HdataP"  ∷ dataP ↦[slice.T byteT] p1 ∗
+                 "HentsP"  ∷ entsP ↦[slice.T (struct.t WriteEntry)] p2 ∗
+                 "HiP"     ∷ iP ↦[uint64T] #i ∗
+                 "Hxs"     ∷ own_slice_small p1 byteT (DfracOwn 1) remaining ∗
+                 "Hents"   ∷ own_slice p2 (struct.t WriteEntry) (DfracOwn 1) (take (uint.nat i) xs) ∗
+                 "%Hbound" ∷ ⌜cont || bool_decide (length xs ≤ uint.nat i)%nat⌝)%I.
+    wp_apply (wp_forBreak_cond P with "[] [-HΦ]"); last first; first 1 last.
+    { by iFrame. }
+    { clear Φ.
+      iIntros (Φ) "!> HP HΦ".
+      iNamed "HP".
+      wp_load.
+      wp_pures.
+      rewrite Z_u64; last first.
+      { clear -Hlenxs. lia. }
+      set b := bool_decide _.
+      destruct b eqn:Hb; wp_pures; last first.
+      { iApply "HΦ".
+        iFrame.
+        iPureIntro.
+        subst b.
+        case_bool_decide as Hi; first done.
+        apply bool_decide_pack.
+        lia.
+      }
+      wp_load.
+      subst b. apply bool_decide_eq_true_1 in Hb.
+      assert (is_Some (xs !! uint.nat i)) as [x Hx].
+      { apply lookup_lt_is_Some_2. word. }
+      rewrite (drop_S _ _ _ Hx) encode_dbmods_xlen_cons -app_assoc.
+      wp_apply (wp_DecodeWriteEntry with "Hxs").
+      iIntros (bsloopP) "Hbsloop".
+      wp_load.
+      wp_apply (wp_SliceAppend with "Hents").
+      iIntros (entsP') "Hents".
+      do 2 wp_store. wp_load. wp_store.
+      iApply "HΦ".
+      iFrame "∗ %".
+      rewrite uint_nat_word_add_S; last word.
+      rewrite (take_S_r _ _ _ Hx).
+      by iFrame.
+    }
+    iNamed 1.
+    case_bool_decide as Hi; last done.
+    do 2 wp_load.
+    wp_pures.
+
+    (*@     return ents, data                                                   @*)
+    (*@ }                                                                       @*)
+    iApply "HΦ".
+    rewrite take_ge; last apply Hi.
+    rewrite drop_ge; last apply Hi.
+    by iFrame.
+  Qed.
+
+End program.
diff --git a/src/program_proof/tulip/program/util/encode_kvmap.v b/src/program_proof/tulip/program/util/encode_kvmap.v
new file mode 100644
index 000000000..1a6bda30e
--- /dev/null
+++ b/src/program_proof/tulip/program/util/encode_kvmap.v
@@ -0,0 +1,79 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.util Require Import encode_write_entry.
+From Perennial.program_proof Require Import marshal_stateless_proof.
+
+Section program.
+  Context `{!heapGS Σ, !paxos_ghostG Σ}.
+
+  Theorem wp_EncodeKVMap (bsP : Slice.t) (mP : loc) (bs : list u8) q (m : dbmap) :
+    {{{ own_slice bsP byteT (DfracOwn 1) bs ∗ own_map mP q m }}}
+      EncodeKVMap (to_val bsP) #mP
+    {{{ (dataP : Slice.t) (mdata : list u8), RET (to_val dataP);
+        own_slice dataP byteT (DfracOwn 1) (bs ++ mdata) ∗ own_map mP q m ∗
+        ⌜encode_dbmap m mdata⌝
+    }}}.
+  Proof.
+    iIntros (Φ) "[Hbs Hm] HΦ".
+    wp_rec.
+
+    (*@ func EncodeKVMap(bs []byte, m tulip.KVMap) []byte {                     @*)
+    (*@     var data = marshal.WriteInt(bs, uint64(len(m)))                     @*)
+    (*@                                                                         @*)
+    wp_apply (wp_MapLen with "Hm").
+    iIntros "[%Hszm Hm]".
+    wp_apply (wp_WriteInt with "Hbs").
+    iIntros (p) "Hp".
+    wp_apply wp_ref_to; first done.
+    iIntros (dataP) "HdataP".
+
+    (*@     for k, v := range(m) {                                              @*)
+    (*@         x := tulip.WriteEntry{                                          @*)
+    (*@             Key   : k,                                                  @*)
+    (*@             Value : v,                                                  @*)
+    (*@         }                                                               @*)
+    (*@         data = EncodeWriteEntry(data, x)                                @*)
+    (*@     }                                                                   @*)
+    (*@                                                                         @*)
+    set P := (λ (mx : dbmap), ∃ (px : Slice.t) (ml : list dbmod),
+                 let l := encode_dbmods_xlen ml in
+                "HdataP" ∷ dataP ↦[slice.T byteT] px ∗
+                "Hdata"  ∷ own_slice px byteT (DfracOwn 1) (bs ++ u64_le (W64 (size m)) ++ l) ∗
+                "%Hml"   ∷ ⌜ml ≡ₚ map_to_list mx⌝)%I.
+    wp_apply (wp_MapIter_fold _ _ _ P with "Hm [-HΦ]").
+    { iExists _, []. rewrite map_to_list_empty. by iFrame. }
+    { clear Φ.
+      iIntros (mx k v Φ) "!> [HP %Hk] HΦ".
+      destruct Hk as [Hmxk Hmk].
+      iNamed "HP".
+      wp_load.
+      wp_apply (wp_EncodeWriteEntry _ (k, v) with "Hdata").
+      iIntros (py) "Hdata".
+      wp_store.
+      iApply "HΦ".
+      rewrite -2!(app_assoc _ _ (encode_dbmod (k, v))).
+      iExists _, (ml ++ [(k, v)]).
+      rewrite encode_dbmods_xlen_snoc.
+      iFrame.
+      iPureIntro.
+      rewrite map_to_list_insert; last apply Hmxk.
+      rewrite Hml.
+      symmetry.
+      apply Permutation_cons_append.
+    }
+    iIntros "[Hm HP]".
+    iNamed "HP".
+    wp_load.
+
+    (*@     return data                                                         @*)
+    (*@ }                                                                       @*)
+    iApply "HΦ".
+    iFrame.
+    iPureIntro.
+    exists ml.
+    split; last done.
+    rewrite /encode_dbmods.
+    do 2 f_equal.
+    by rewrite Hml length_map_to_list.
+  Qed.
+
+End program.
diff --git a/src/program_proof/tulip/program/util/encode_kvmap_from_slice.v b/src/program_proof/tulip/program/util/encode_kvmap_from_slice.v
new file mode 100644
index 000000000..e4ca45740
--- /dev/null
+++ b/src/program_proof/tulip/program/util/encode_kvmap_from_slice.v
@@ -0,0 +1,74 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.util Require Import encode_write_entry.
+From Perennial.program_proof Require Import marshal_stateless_proof.
+
+Section program.
+  Context `{!heapGS Σ, !paxos_ghostG Σ}.
+
+  Theorem wp_EncodeKVMapFromSlice (bsP : Slice.t) (xsP : Slice.t) (bs : list u8) (m : dbmap) :
+    {{{ own_slice bsP byteT (DfracOwn 1) bs ∗ own_dbmap_in_slice xsP m }}}
+      EncodeKVMapFromSlice (to_val bsP) (to_val xsP)
+    {{{ (dataP : Slice.t) (mdata : list u8), RET (to_val dataP);
+        own_slice dataP byteT (DfracOwn 1) (bs ++ mdata) ∗
+        own_dbmap_in_slice xsP m ∗
+        ⌜encode_dbmap m mdata⌝
+    }}}.
+  Proof.
+    iIntros (Φ) "[Hbs Hm] HΦ".
+    wp_rec.
+
+    (*@ func EncodeKVMapFromSlice(bs []byte, xs []tulip.WriteEntry) []byte {    @*)
+    (*@     var data = marshal.WriteInt(bs, uint64(len(xs)))                    @*)
+    (*@                                                                         @*)
+    wp_apply wp_slice_len.
+    wp_apply (wp_WriteInt with "Hbs").
+    iIntros (p) "Hp".
+    wp_apply wp_ref_to; first done.
+    iIntros (dataP) "HdataP".
+
+    (*@     for _, x := range(xs) {                                             @*)
+    (*@         data = EncodeWriteEntry(data, x)                                @*)
+    (*@     }                                                                   @*)
+    (*@                                                                         @*)
+    iDestruct "Hm" as (xs) "[Hm %Hxs]".
+    iDestruct (own_slice_small_acc with "Hm") as "[Hm HmC]".
+    iDestruct (own_slice_small_sz with "Hm") as %Hlenm.
+    set nW := xsP.(Slice.sz).
+    set P := (λ (i : u64), ∃ (px : Slice.t),
+                 let l := encode_dbmods_xlen (take (uint.nat i) xs) in
+                "HdataP" ∷ dataP ↦[slice.T byteT] px ∗
+                "Hdata"  ∷ own_slice px byteT (DfracOwn 1) (bs ++ u64_le nW ++ l))%I.
+    wp_apply (wp_forSlice P with "[] [$Hm $Hp $HdataP]"); last first; first 1 last.
+    { clear Φ.
+      iIntros (i x Φ) "!> [HP %Hloop] HΦ".
+      destruct Hloop as [Hi Hx].
+      iNamed "HP".
+      wp_load.
+      wp_apply (wp_EncodeWriteEntry with "Hdata").
+      iIntros (py) "Hpy".
+      wp_store.
+      iApply "HΦ".
+      iFrame.
+      rewrite uint_nat_word_add_S; last word.
+      by rewrite (take_S_r _ _ _ Hx) encode_dbmods_xlen_snoc -app_assoc.
+    }
+    iIntros "[HP Hm]".
+    iNamed "HP".
+    wp_load.
+
+    (*@     return data                                                         @*)
+    (*@ }                                                                       @*)
+    iDestruct ("HmC" with "Hm") as "Hm".
+    iApply "HΦ".
+    iFrame.
+    iPureIntro.
+    split; first done.
+    exists xs.
+    split; last done.
+    subst nW.
+    rewrite -Hlenm firstn_all /encode_dbmods Hlenm.
+    do 2 f_equal.
+    word.
+  Qed.
+
+End program.