diff --git a/src/program_proof/tulip/base.v b/src/program_proof/tulip/base.v
index d31363d8a..415e1ad61 100644
--- a/src/program_proof/tulip/base.v
+++ b/src/program_proof/tulip/base.v
@@ -22,12 +22,23 @@ Inductive txnres :=
 | ResCommitted (wrs : dbmap)
 | ResAborted.
 
-Definition fstring := {k : byte_string | (length k < (Z.to_nat (2 ^ 64)%Z))%nat }.
+Definition fstring := {k : byte_string | length k < 2 ^ 64 }.
 
 #[local]
 Instance fstring_finite :
   finite.Finite fstring.
-Proof. apply Helpers.finite.list_finite_lt_length. Qed.
+Proof.
+  unfold fstring.
+  set(x:=2 ^ 64).
+  generalize x. clear x. intros y.
+  unshelve refine (finite.surjective_finite (λ x : {k : byte_string | (length k < Z.to_nat y)%nat },
+                                               (proj1_sig x) ↾ _ )).
+  { abstract (destruct x; simpl; lia). }
+  { apply Helpers.finite.list_finite_lt_length. }
+  intros [].
+  unshelve eexists (exist _ _ _); last rewrite sig_eq_pi /= //.
+  simpl. lia.
+Qed.
 
 Definition keys_all : gset byte_string :=
   list_to_set (map proj1_sig (finite.enum fstring)).
@@ -300,8 +311,7 @@ Proof.
   intros Hvk.
   rewrite /valid_key /keys_all in Hvk.
   apply elem_of_list_to_set, elem_of_list_fmap_2 in Hvk.
-  destruct Hvk as ([k Hk] & -> & _).
-  simpl. lia.
+  by destruct Hvk as ([k Hk] & -> & _).
 Qed.
 
 Definition valid_ccommand gid (c : ccommand) :=
diff --git a/src/program_proof/tulip/encode.v b/src/program_proof/tulip/encode.v
index f247b87fb..eacdb221d 100644
--- a/src/program_proof/tulip/encode.v
+++ b/src/program_proof/tulip/encode.v
@@ -1,14 +1,75 @@
 From Perennial.program_proof Require Import grove_prelude.
 From Perennial.program_proof.tulip Require Import base.
 
+Definition encode_string (x : byte_string) : list u8 :=
+  u64_le (U64 (length x)) ++ x.
+
+Definition encode_strings_step (bs : list u8) (x : byte_string) : list u8 :=
+  bs ++ encode_string x.
+
+Definition encode_strings_xlen (xs : list byte_string) : list u8 :=
+  foldl encode_strings_step [] xs.
+
+Definition encode_strings (xs : list byte_string) : list u8 :=
+  u64_le (U64 (length xs)) ++ encode_strings_xlen xs.
+
+Lemma encode_strings_xlen_snoc xs x :
+  encode_strings_xlen (xs ++ [x]) = encode_strings_xlen xs ++ encode_string x.
+Proof.
+  by rewrite /encode_strings_xlen foldl_snoc /encode_strings_step.
+Qed.
+
+Lemma foldl_encode_strings_step_app (bs : list u8) (xs : list byte_string) :
+  foldl encode_strings_step bs xs = bs ++ foldl encode_strings_step [] xs.
+Proof.
+  generalize dependent bs.
+  induction xs as [| x xs IH]; intros bs.
+  { by rewrite /= app_nil_r. }
+  rewrite /= (IH (encode_strings_step bs x)) (IH (encode_strings_step [] x)).
+  rewrite {1 3}/encode_strings_step.
+  by rewrite app_nil_l app_assoc.
+Qed.
+
+Lemma encode_strings_xlen_cons xs x :
+  encode_strings_xlen (x :: xs) = encode_string x ++ encode_strings_xlen xs.
+Proof.
+  rewrite /encode_strings_xlen /= foldl_encode_strings_step_app.
+  by rewrite {1}/encode_strings_step app_nil_l.
+Qed.
+
+Lemma encode_strings_xlen_length_inv xs n :
+  (length (encode_strings_xlen xs) ≤ n)%nat ->
+  (length xs ≤ n)%nat.
+Proof.
+  generalize dependent n.
+  induction xs as [| x xs IH]; intros n; first done.
+  rewrite encode_strings_xlen_cons length_app /=.
+  assert (length (encode_string x) ≠ O).
+  { by destruct (nil_or_length_pos (encode_string x)). }
+  intros Hlen.
+  assert (Hlenxs : (length xs ≤ pred n)%nat).
+  { apply IH. lia. }
+  lia.
+Qed.
+
+Lemma encode_strings_length_inv xs n :
+  (length (encode_strings xs) ≤ n)%nat ->
+  (length xs ≤ n)%nat.
+Proof.
+  rewrite /encode_strings length_app.
+  intros Hn.
+  pose proof (encode_strings_xlen_length_inv xs n) as Hlen.
+  lia.
+Qed.
+
 Definition encode_dbval (x : dbval) : list u8 :=
   match x with
-  | Some v => [U8 1] ++ v
+  | Some v => [U8 1] ++ encode_string v
   | None => [U8 0]
   end.
 
 Definition encode_dbmod (x : dbmod) : list u8 :=
-  x.1 ++ encode_dbval x.2.
+  encode_string x.1 ++ encode_dbval x.2.
 
 Definition encode_dbmods_step (bs : list u8) (x : dbmod) : list u8 :=
   bs ++ encode_dbmod x.
diff --git a/src/program_proof/tulip/inv_group.v b/src/program_proof/tulip/inv_group.v
index 90ef49712..1f85bfe8f 100644
--- a/src/program_proof/tulip/inv_group.v
+++ b/src/program_proof/tulip/inv_group.v
@@ -422,7 +422,7 @@ Section lemma.
     do 2 iNamed "Hgroup".
     pose proof (apply_cmds_dom _ _ _ Hrsm) as Hdom.
     assert (is_Some (hists !! key)) as [h Hh].
-    { rewrite -elem_of_dom. rewrite Hdom. set_solver. }
+    { rewrite -elem_of_dom. set_solver. }
     iDestruct (txn_log_prefix with "Hlog Hloglb") as %Hprefix.
     rewrite /hist_from_log in Hhlb.
     destruct (apply_cmds loglb) as [cmlb histmlb |] eqn:Happly; last done.
@@ -467,14 +467,6 @@ Section lemma.
     iApply (group_inv_witness_repl_hist with "Hloglb Hgroup").
     { pose proof (apply_cmds_dom _ _ _ Happly) as Hdom.
       apply elem_of_dom_2 in Hh.
-      try fast_done;                                                                                                                                                                                    
-        intros; setoid_subst;
-        set_unfold;
-        intros; setoid_subst;
-        try match goal with |- _ ∈ _ => apply dec_stable end.
-        naive_solver eauto.
-
-      naive_solver.
       set_solver.
     }
     { done. }
diff --git a/src/program_proof/tulip/msg.v b/src/program_proof/tulip/msg.v
index a25ad8f17..b4e66ca82 100644
--- a/src/program_proof/tulip/msg.v
+++ b/src/program_proof/tulip/msg.v
@@ -58,7 +58,7 @@ Proof.
 Qed.
 
 Definition encode_read_req_xkind (ts : u64) (key : byte_string) :=
-  u64_le ts ++ key.
+  u64_le ts ++ encode_string key.
 
 Definition encode_read_req (ts : u64) (key : byte_string) (data : list u8) :=
   data = u64_le (U64 100) ++ encode_read_req_xkind ts key.
@@ -215,7 +215,7 @@ Qed.
 
 Definition encode_read_resp_xkind
   (ts rid : u64) (key : byte_string) (ver : dbpver) (slow : bool) :=
-  u64_le ts ++ u64_le rid ++ key ++
+  u64_le ts ++ u64_le rid ++ encode_string key ++
     encode_dbpver ver ++ [if slow then U8 1 else U8 0].
 
 Definition encode_read_resp
diff --git a/src/program_proof/tulip/paxos/msg.v b/src/program_proof/tulip/paxos/msg.v
index 33f713340..a3187d26e 100644
--- a/src/program_proof/tulip/paxos/msg.v
+++ b/src/program_proof/tulip/paxos/msg.v
@@ -36,7 +36,7 @@ Definition encode_request_vote_req (term lsnlc : u64) :=
 
 Definition encode_append_entries_req_xkind
   (term lsnlc lsne : u64) (ents : list byte_string) :=
-  u64_le term ++ u64_le lsnlc ++ u64_le lsne ++ concat ents.
+  u64_le term ++ u64_le lsnlc ++ u64_le lsne ++ encode_strings ents.
 
 Definition encode_append_entries_req
   (term lsnlc lsne : u64) (ents : list byte_string) :=
@@ -78,7 +78,7 @@ Qed.
 
 Definition encode_request_vote_resp_xkind
   (nid term terme : u64) (ents : list byte_string) :=
-  u64_le nid ++ u64_le term ++ u64_le terme ++ concat ents.
+  u64_le nid ++ u64_le term ++ u64_le terme ++ encode_strings ents.
 
 Definition encode_request_vote_resp
   (nid term terme : u64) (ents : list byte_string) :=
diff --git a/src/program_proof/tulip/program/gcoord/gcoord_read.v b/src/program_proof/tulip/program/gcoord/gcoord_read.v
index dfadb5a13..6feeb599d 100644
--- a/src/program_proof/tulip/program/gcoord/gcoord_read.v
+++ b/src/program_proof/tulip/program/gcoord/gcoord_read.v
@@ -7,7 +7,7 @@ Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
   Theorem wp_GroupCoordinator__Read
-    (gcoord : loc) (tsW : u64) (key : string) gid γ :
+    (gcoord : loc) (tsW : u64) (key : byte_string) gid γ :
     let ts := uint.nat tsW in
     safe_read_req gid ts key ->
     is_gcoord gcoord gid γ -∗
diff --git a/src/program_proof/tulip/program/gcoord/gcoord_read_session.v b/src/program_proof/tulip/program/gcoord/gcoord_read_session.v
index c0156aca7..8497d402e 100644
--- a/src/program_proof/tulip/program/gcoord/gcoord_read_session.v
+++ b/src/program_proof/tulip/program/gcoord/gcoord_read_session.v
@@ -7,7 +7,7 @@ Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
   Theorem wp_GroupCoordinator__ReadSession 
-    (gcoord : loc) (rid : u64) (tsW : u64) (key : string) gid γ :
+    (gcoord : loc) (rid : u64) (tsW : u64) (key : byte_string) gid γ :
     let ts := uint.nat tsW in
     rid ∈ rids_all ->
     safe_read_req gid ts key ->
diff --git a/src/program_proof/tulip/program/gcoord/gcoord_send.v b/src/program_proof/tulip/program/gcoord/gcoord_send.v
index d935d3eda..df7d6837d 100644
--- a/src/program_proof/tulip/program/gcoord/gcoord_send.v
+++ b/src/program_proof/tulip/program/gcoord/gcoord_send.v
@@ -74,7 +74,7 @@ Section program.
   Qed.
 
   Theorem wp_GroupCoordinator__SendRead
-    (gcoord : loc) (rid : u64) (ts : u64) (key : string) addrm gid γ :
+    (gcoord : loc) (rid : u64) (ts : u64) (key : byte_string) addrm gid γ :
     safe_read_req gid (uint.nat ts) key ->
     rid ∈ dom addrm ->
     is_gcoord_with_addrm gcoord gid addrm γ -∗
diff --git a/src/program_proof/tulip/program/gcoord/gcoord_wait_until_value_ready.v b/src/program_proof/tulip/program/gcoord/gcoord_wait_until_value_ready.v
index 90eba3149..4c46b6bb1 100644
--- a/src/program_proof/tulip/program/gcoord/gcoord_wait_until_value_ready.v
+++ b/src/program_proof/tulip/program/gcoord/gcoord_wait_until_value_ready.v
@@ -7,7 +7,7 @@ Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
   Theorem wp_GroupCoordinator__WaitUntilValueReady
-    (gcoord : loc) (tsW : u64) (key : string) gid γ :
+    (gcoord : loc) (tsW : u64) (key : byte_string) gid γ :
     let ts := uint.nat tsW in
     is_gcoord gcoord gid γ -∗
     {{{ True }}}
diff --git a/src/program_proof/tulip/program/gcoord/greader_clear_versions.v b/src/program_proof/tulip/program/gcoord/greader_clear_versions.v
index b671178b3..c45144c18 100644
--- a/src/program_proof/tulip/program/gcoord/greader_clear_versions.v
+++ b/src/program_proof/tulip/program/gcoord/greader_clear_versions.v
@@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program.gcoord Require Import greader_repr.
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_GroupReader__clearVersions (grd : loc) (key : string) qreadm ts γ :
+  Theorem wp_GroupReader__clearVersions (grd : loc) (key : byte_string) qreadm ts γ :
     {{{ own_greader_qreadm grd qreadm ts γ }}}
       GroupReader__clearVersions #grd #(LitString key)
     {{{ RET #(); own_greader_qreadm grd (delete key qreadm) ts γ }}}.
diff --git a/src/program_proof/tulip/program/gcoord/greader_pick_latest_value.v b/src/program_proof/tulip/program/gcoord/greader_pick_latest_value.v
index a5035b724..22100e8a3 100644
--- a/src/program_proof/tulip/program/gcoord/greader_pick_latest_value.v
+++ b/src/program_proof/tulip/program/gcoord/greader_pick_latest_value.v
@@ -8,7 +8,7 @@ Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_GroupReader__pickLatestValue (grd : loc) (key : string) qreadm verm ts γ :
+  Theorem wp_GroupReader__pickLatestValue (grd : loc) (key : byte_string) qreadm verm ts γ :
     qreadm !! key = Some verm ->
     cquorum_size rids_all (dom verm) ->
     {{{ own_greader_qreadm grd qreadm ts γ }}}
diff --git a/src/program_proof/tulip/program/gcoord/greader_process_read_result.v b/src/program_proof/tulip/program/gcoord/greader_process_read_result.v
index ec81355fa..7cbc997af 100644
--- a/src/program_proof/tulip/program/gcoord/greader_process_read_result.v
+++ b/src/program_proof/tulip/program/gcoord/greader_process_read_result.v
@@ -10,7 +10,7 @@ Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
   Theorem wp_GroupReader__processReadResult
-    grd (rid : u64) (key : string) (ver : dbpver) (slow : bool) ts γ :
+    grd (rid : u64) (key : byte_string) (ver : dbpver) (slow : bool) ts γ :
     rid ∈ rids_all ->
     fast_or_slow_read γ rid key (uint.nat ver.1) ts ver.2 slow -∗
     {{{ own_greader grd ts γ }}}
diff --git a/src/program_proof/tulip/program/gcoord/greader_read.v b/src/program_proof/tulip/program/gcoord/greader_read.v
index 16f5e0ffe..a81980f20 100644
--- a/src/program_proof/tulip/program/gcoord/greader_read.v
+++ b/src/program_proof/tulip/program/gcoord/greader_read.v
@@ -5,7 +5,7 @@ From Perennial.program_proof.tulip.program.gcoord Require Import greader_repr.
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_GroupReader__read (grd : loc) (key : string) ts γ :
+  Theorem wp_GroupReader__read (grd : loc) (key : byte_string) ts γ :
     {{{ own_greader grd ts γ }}}
       GroupReader__read #grd #(LitString key)
     {{{ (v : dbval) (ok : bool), RET (dbval_to_val v, #ok); 
diff --git a/src/program_proof/tulip/program/gcoord/greader_reset.v b/src/program_proof/tulip/program/gcoord/greader_reset.v
index 9cfc4455b..74ce26521 100644
--- a/src/program_proof/tulip/program/gcoord/greader_reset.v
+++ b/src/program_proof/tulip/program/gcoord/greader_reset.v
@@ -17,10 +17,10 @@ Section program.
     (*@     grd.qreadm = make(map[string]map[uint64]tulip.Version)              @*)
     (*@ }                                                                       @*)
     iNamed "Hgrd".
-    wp_apply (wp_NewMap string dbval).
+    wp_apply (wp_NewMap byte_string dbval).
     iIntros (valuemP') "Hvaluem".
     wp_storeField.
-    wp_apply (wp_NewMap string loc).
+    wp_apply (wp_NewMap byte_string loc).
     iIntros (qreadmP') "Hqreadm".
     wp_storeField.
     iApply "HΦ".
diff --git a/src/program_proof/tulip/program/gcoord/greader_responded.v b/src/program_proof/tulip/program/gcoord/greader_responded.v
index 1a2addc7f..dac9ccede 100644
--- a/src/program_proof/tulip/program/gcoord/greader_responded.v
+++ b/src/program_proof/tulip/program/gcoord/greader_responded.v
@@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program.gcoord Require Import greader_repr.
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_GroupReader__responded (grd : loc) (rid : u64) (key : string) ts γ :
+  Theorem wp_GroupReader__responded (grd : loc) (rid : u64) (key : byte_string) ts γ :
     {{{ own_greader grd ts γ }}}
       GroupReader__responded #grd #rid #(LitString key)
     {{{ (responded : bool), RET #responded; own_greader grd ts γ }}}.
diff --git a/src/program_proof/tulip/program/index/index.v b/src/program_proof/tulip/program/index/index.v
index 4c78921b8..e48b20855 100644
--- a/src/program_proof/tulip/program/index/index.v
+++ b/src/program_proof/tulip/program/index/index.v
@@ -22,7 +22,7 @@ Section program.
       "#HmuP" ∷ readonly (idx ↦[Index :: "mu"] #muP) ∗
       "#Hmu"  ∷ is_lock tulipNS #muP (own_index idx γ α).
 
-  Theorem wp_Index__GetTuple (idx : loc) (key : string) γ α :
+  Theorem wp_Index__GetTuple (idx : loc) (key : byte_string) γ α :
     key ∈ keys_all ->
     is_index idx γ α -∗
     {{{ True }}}
diff --git a/src/program_proof/tulip/program/prelude.v b/src/program_proof/tulip/program/prelude.v
index bc9df88bb..cde056671 100644
--- a/src/program_proof/tulip/program/prelude.v
+++ b/src/program_proof/tulip/program/prelude.v
@@ -49,7 +49,7 @@ Proof.
   refine {|
       to_val := dbmod_to_val;
       from_val := dbmod_from_val;
-      IntoVal_def := ("", None);
+      IntoVal_def := (""%go, None);
     |}.
   intros [k v].
   by destruct v.
diff --git a/src/program_proof/tulip/program/replica/encode.v b/src/program_proof/tulip/program/replica/encode.v
index a0079574f..ea1856aba 100644
--- a/src/program_proof/tulip/program/replica/encode.v
+++ b/src/program_proof/tulip/program/replica/encode.v
@@ -7,7 +7,7 @@ Section encode.
   Context `{!heapGS Σ, !paxos_ghostG Σ}.
 
   Theorem wp_EncodeTxnReadResponse
-    (rid : u64) (ts : u64) (key : string) (ver : dbpver) (slow : bool) :
+    (rid : u64) (ts : u64) (key : byte_string) (ver : dbpver) (slow : bool) :
     {{{ True }}}
       EncodeTxnReadResponse #ts #rid #(LitString key) (dbpver_to_val ver) #slow
     {{{ (dataP : Slice.t) (data : list u8), RET (to_val dataP);
diff --git a/src/program_proof/tulip/program/replica/replica_log.v b/src/program_proof/tulip/program/replica/replica_log.v
index 2ebb1a75d..949952d80 100644
--- a/src/program_proof/tulip/program/replica/replica_log.v
+++ b/src/program_proof/tulip/program/replica/replica_log.v
@@ -6,7 +6,7 @@ From Perennial.program_proof.tulip.program.util Require Import
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_logRead (fname : string) (ts : u64) (key : string) (bs : list u8) :
+  Theorem wp_logRead (fname : byte_string) (ts : u64) (key : byte_string) (bs : list u8) :
     {{{ fname f↦ bs }}}
       logRead #(LitString fname) #ts #(LitString key)
     {{{ (bs' : list u8), RET #(); fname f↦ bs' }}}.
@@ -52,7 +52,7 @@ Section program.
   Qed.
 
   Theorem wp_logValidate
-    (fname : string) (ts : u64) (pwrsP : Slice.t) (pwrs : dbmap) (bs : list u8) :
+    (fname : byte_string) (ts : u64) (pwrsP : Slice.t) (pwrs : dbmap) (bs : list u8) :
     {{{ fname f↦ bs ∗ own_dbmap_in_slice pwrsP pwrs }}}
       logValidate #(LitString fname) #ts (to_val pwrsP) slice.nil
     {{{ (bs' : list u8), RET #(); fname f↦ bs' ∗ own_dbmap_in_slice pwrsP pwrs }}}.
@@ -99,7 +99,7 @@ Section program.
   Qed.
 
   Theorem wp_logFastPrepare
-    (fname : string) (ts : u64) (pwrsP : Slice.t) (pwrs : dbmap) (bs : list u8) :
+    (fname : byte_string) (ts : u64) (pwrsP : Slice.t) (pwrs : dbmap) (bs : list u8) :
     {{{ fname f↦ bs ∗ own_dbmap_in_slice pwrsP pwrs }}}
       logFastPrepare #(LitString fname) #ts (to_val pwrsP) slice.nil
     {{{ (bs' : list u8), RET #(); fname f↦ bs' ∗ own_dbmap_in_slice pwrsP pwrs }}}.
@@ -145,7 +145,7 @@ Section program.
     by iFrame.
   Qed.
 
-  Theorem wp_logAccept (fname : string) (ts : u64) (rank : u64) (dec : bool) (bs : list u8) :
+  Theorem wp_logAccept (fname : byte_string) (ts : u64) (rank : u64) (dec : bool) (bs : list u8) :
     {{{ fname f↦ bs }}}
       logAccept #(LitString fname) #ts #rank #dec
     {{{ (bs' : list u8), RET #(); fname f↦ bs' }}}.
diff --git a/src/program_proof/tulip/program/replica/replica_read.v b/src/program_proof/tulip/program/replica/replica_read.v
index fae667528..38033183e 100644
--- a/src/program_proof/tulip/program/replica/replica_read.v
+++ b/src/program_proof/tulip/program/replica/replica_read.v
@@ -9,7 +9,7 @@ From Perennial.program_proof.tulip.program.index Require Import index.
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_Replica__Read (rp : loc) (tsW : u64) (key : string) gid rid γ :
+  Theorem wp_Replica__Read (rp : loc) (tsW : u64) (key : byte_string) gid rid γ :
     let ts := uint.nat tsW in
     ts ≠ O ->
     key ∈ keys_all ->
diff --git a/src/program_proof/tulip/program/replica/replica_repr.v b/src/program_proof/tulip/program/replica/replica_repr.v
index 071337743..cdb58c3a7 100644
--- a/src/program_proof/tulip/program/replica/replica_repr.v
+++ b/src/program_proof/tulip/program/replica/replica_repr.v
@@ -126,7 +126,7 @@ Section repr.
       "%Hexec"      ∷ ⌜execute_cmds log = LocalState cm histm cpm ptgsm sptsm ptsm psm rkm⌝.
 
   Definition own_replica (rp : loc) (gid rid : u64) γ α : iProp Σ :=
-    ∃ (cloga : dblog) (lsna : u64) (fname : string) (bs : list u8),
+    ∃ (cloga : dblog) (lsna : u64) (fname : byte_string) (bs : list u8),
       "Hrp"        ∷ own_replica_with_cloga_no_lsna rp cloga gid rid γ α ∗
       "Hlsna"      ∷ rp ↦[Replica :: "lsna"] #lsna ∗
       "HfnameP"    ∷ rp ↦[Replica :: "fname"] #(LitString fname) ∗
diff --git a/src/program_proof/tulip/program/replica/start.v b/src/program_proof/tulip/program/replica/start.v
index 55e7b30eb..ac7400d00 100644
--- a/src/program_proof/tulip/program/replica/start.v
+++ b/src/program_proof/tulip/program/replica/start.v
@@ -12,8 +12,8 @@ Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ, !paxos_ghostG Σ}.
 
   Theorem wp_Start
-    (rid : u64) (addr : chan) (fname : string) (addrmpxP : loc) (fnamepx : string)
-    (termc : u64) (terml : u64) (lsnc : u64) (log : list string) (addrmpx : gmap u64 chan)
+    (rid : u64) (addr : chan) (fname : byte_string) (addrmpxP : loc) (fnamepx : byte_string)
+    (termc : u64) (terml : u64) (lsnc : u64) (log : list byte_string) (addrmpx : gmap u64 chan)
     (addrm : gmap u64 chan) gid γ π :
     termc = (W64 0) ->
     terml = (W64 0) ->
diff --git a/src/program_proof/tulip/program/tuple/res.v b/src/program_proof/tulip/program/tuple/res.v
index 3a894250f..d0a64f574 100644
--- a/src/program_proof/tulip/program/tuple/res.v
+++ b/src/program_proof/tulip/program/tuple/res.v
@@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program Require Import prelude.
 Section res.
   Context `{!tulip_ghostG Σ}.
 
-  Definition own_phys_hist_half α (key : string) (hist : dbhist) : iProp Σ :=
+  Definition own_phys_hist_half α (key : byte_string) (hist : dbhist) : iProp Σ :=
     own α {[ key := (to_dfrac_agree (DfracOwn (1 / 2)) hist) ]}.
 
   Lemma phys_hist_update {α k h1 h2} h :
diff --git a/src/program_proof/tulip/program/tuple/tuple.v b/src/program_proof/tulip/program/tuple/tuple.v
index 962f52ae7..a99fc88bc 100644
--- a/src/program_proof/tulip/program/tuple/tuple.v
+++ b/src/program_proof/tulip/program/tuple/tuple.v
@@ -174,7 +174,7 @@ Section program.
       "#Hmu"   ∷ readonly (tuple ↦[Tuple :: "mu"] #muP) ∗
       "#Hlock" ∷ is_lock tulipNS #muP (own_tuple tuple key γ α).
 
-  Theorem wp_Tuple__AppendVersion (tuple : loc) (tsW : u64) (value : string) key hist γ α :
+  Theorem wp_Tuple__AppendVersion (tuple : loc) (tsW : u64) (value : byte_string) key hist γ α :
     let ts := uint.nat tsW in
     let hist' := last_extend ts hist ++ [Some value] in
     (length hist ≤ ts)%nat ->
diff --git a/src/program_proof/tulip/program/txn/proph.v b/src/program_proof/tulip/program/txn/proph.v
index c9b1769ed..fab41d503 100644
--- a/src/program_proof/tulip/program/txn/proph.v
+++ b/src/program_proof/tulip/program/txn/proph.v
@@ -4,7 +4,7 @@ From Perennial.goose_lang.trusted.github_com.mit_pdos.tulip Require Import trust
 Section proph.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Lemma wp_ResolveRead p (tid : u64) (key : string) (ts : nat) :
+  Lemma wp_ResolveRead p (tid : u64) (key : byte_string) (ts : nat) :
     ⊢
     {{{ ⌜uint.nat tid = ts⌝ }}}
     <<< ∀∀ acs, own_txn_proph p acs >>>
diff --git a/src/program_proof/tulip/program/txn/txn_getwrs.v b/src/program_proof/tulip/program/txn/txn_getwrs.v
index 69be52b1f..831e20658 100644
--- a/src/program_proof/tulip/program/txn/txn_getwrs.v
+++ b/src/program_proof/tulip/program/txn/txn_getwrs.v
@@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program.txn Require Import txn_repr txn_key_t
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_Txn__getwrs (txn : loc) (key : string) q wrs :
+  Theorem wp_Txn__getwrs (txn : loc) (key : byte_string) q wrs :
     valid_key key ->
     {{{ own_txn_wrs txn q wrs }}}
       Txn__getwrs #txn #(LitString key)
diff --git a/src/program_proof/tulip/program/txn/txn_key_to_group.v b/src/program_proof/tulip/program/txn/txn_key_to_group.v
index 2a5b9a121..8f14a1719 100644
--- a/src/program_proof/tulip/program/txn/txn_key_to_group.v
+++ b/src/program_proof/tulip/program/txn/txn_key_to_group.v
@@ -6,7 +6,7 @@ Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_Txn__keyToGroup (txn : loc) (key : string) q wrs :
+  Theorem wp_Txn__keyToGroup (txn : loc) (key : byte_string) q wrs :
     valid_key key ->
     {{{ own_txn_wrs txn q wrs }}}
       Txn__keyToGroup #txn #(LitString key)
@@ -30,7 +30,7 @@ Section program.
     rewrite /key_to_group.
     rewrite -size_dom Hdomwrs.
     pose proof size_gids_all as Hszall.
-    set x := String.length key.
+    set x := length key.
     set y := size gids_all.
     apply valid_key_length in Hvk.
     word.
diff --git a/src/program_proof/tulip/program/txn/txn_setwrs.v b/src/program_proof/tulip/program/txn/txn_setwrs.v
index 62d8a4489..e0cab4949 100644
--- a/src/program_proof/tulip/program/txn/txn_setwrs.v
+++ b/src/program_proof/tulip/program/txn/txn_setwrs.v
@@ -4,7 +4,7 @@ From Perennial.program_proof.tulip.program.txn Require Import txn_repr txn_key_t
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-  Theorem wp_Txn__setwrs (txn : loc) (key : string) (value : dbval) wrs :
+  Theorem wp_Txn__setwrs (txn : loc) (key : byte_string) (value : dbval) wrs :
     valid_key key ->
     {{{ own_txn_wrs txn (DfracOwn 1) wrs }}}
       Txn__setwrs #txn #(LitString key) (dbval_to_val value)
diff --git a/src/program_proof/tulip/program/txnlog/txnlog.v b/src/program_proof/tulip/program/txnlog/txnlog.v
index f93815f05..4e9b8fc52 100644
--- a/src/program_proof/tulip/program/txnlog/txnlog.v
+++ b/src/program_proof/tulip/program/txnlog/txnlog.v
@@ -252,7 +252,6 @@ Section program.
       exists (CmdAbort (uint.nat ts)).
       split; first set_solver.
       simpl.
-      rewrite bytes_to_string_to_bytes.
       rewrite /encode_abort_cmd.
       by rewrite w64_to_nat_id.
     }
@@ -335,7 +334,7 @@ Section program.
       apply set_Forall_singleton.
       exists (CmdCommit (uint.nat ts) pwrs).
       split; first set_solver.
-      rewrite /= bytes_to_string_to_bytes -app_assoc.
+      rewrite /= -app_assoc.
       exists (u64_le ts ++ mdata).
       split; first done.
       exists mdata.
@@ -369,8 +368,8 @@ Section program.
   Qed.
 
   Theorem wp_Start
-    (nidme : u64) (termc : u64) (terml : u64) (lsnc : u64) (log : list string)
-    (addrmP : loc) (addrm : gmap u64 chan) (fname : string) gid γ π :
+    (nidme : u64) (termc : u64) (terml : u64) (lsnc : u64) (log : list byte_string)
+    (addrmP : loc) (addrm : gmap u64 chan) (fname : byte_string) gid γ π :
     termc = (W64 0) ->
     terml = (W64 0) ->
     lsnc = (W64 0) ->
diff --git a/src/program_proof/tulip/program/util/decode_string.v b/src/program_proof/tulip/program/util/decode_string.v
index b1ed29898..37a97a36b 100644
--- a/src/program_proof/tulip/program/util/decode_string.v
+++ b/src/program_proof/tulip/program/util/decode_string.v
@@ -4,7 +4,7 @@ From Perennial.program_proof Require Import marshal_stateless_proof.
 Section program.
   Context `{!heapGS Σ, !paxos_ghostG Σ}.
 
-  Theorem wp_DecodeString (bsP : Slice.t) (s : string) (bstail : list u8) :
+  Theorem wp_DecodeString (bsP : Slice.t) (s : byte_string) (bstail : list u8) :
     {{{ own_slice_small bsP byteT (DfracOwn 1) (encode_string s ++ bstail) }}}
       DecodeString (to_val bsP)
     {{{ (dataP : Slice.t), RET (#(LitString s), (to_val dataP));
diff --git a/src/program_proof/tulip/program/util/decode_strings.v b/src/program_proof/tulip/program/util/decode_strings.v
index c73e79b38..3e0ad2e9a 100644
--- a/src/program_proof/tulip/program/util/decode_strings.v
+++ b/src/program_proof/tulip/program/util/decode_strings.v
@@ -5,7 +5,7 @@ From Perennial.program_proof Require Import marshal_stateless_proof.
 Section program.
   Context `{!heapGS Σ, !paxos_ghostG Σ}.
 
-  Theorem wp_DecodeStrings (bsP : Slice.t) (strs : list string) (bstail : list u8) :
+  Theorem wp_DecodeStrings (bsP : Slice.t) (strs : list byte_string) (bstail : list u8) :
     {{{ own_slice_small bsP byteT (DfracOwn 1) (encode_strings strs ++ bstail) }}}
       DecodeStrings (to_val bsP)
     {{{ (strsP : Slice.t) (dataP : Slice.t), RET (to_val strsP, to_val dataP);
diff --git a/src/program_proof/tulip/program/util/encode_string.v b/src/program_proof/tulip/program/util/encode_string.v
index a05cf49f8..82e464120 100644
--- a/src/program_proof/tulip/program/util/encode_string.v
+++ b/src/program_proof/tulip/program/util/encode_string.v
@@ -29,7 +29,7 @@ Section program.
     wp_pures.
     iApply "HΦ".
     iFrame.
-    by rewrite -app_assoc /encode_string string_bytes_length.
+    by rewrite -app_assoc /encode_string.
   Qed.
 
 End program.
diff --git a/src/program_proof/vrsm/apps/closed_proof.v b/src/program_proof/vrsm/apps/closed_proof.v
index 66ec2bb64..ebad04cd5 100644
--- a/src/program_proof/vrsm/apps/closed_proof.v
+++ b/src/program_proof/vrsm/apps/closed_proof.v
@@ -58,7 +58,7 @@ Qed.
 Local Instance subG_ekvΣ {Σ} : subG kv_pbΣ Σ → ekvG Σ.
 Proof. intros. solve_inG. Qed.
 
-Definition replica_fname := "kv.data".
+Definition replica_fname := "kv.data"%go.
 
 (* FIXME: put this in the file that defines ekvΣ? *)
 Opaque ekvΣ.
@@ -147,7 +147,7 @@ Proof.
 
   (* Allocate the kv system used for storing data *)
   iMod (alloc_vkv (ekvParams.mk [dr1Host ; dr2Host ]) [(dconfigHost, dconfigHostPaxos)]
-                  {[ "init"; "a1"; "a2" ]} with "[Hd1 Hd2]") as "[Hdkv Hdconf]"; try (simpl; lia).
+                  {[ "init"; "a1"; "a2" ]}%go with "[Hd1 Hd2]") as "[Hdkv Hdconf]"; try (simpl; lia).
   {
     rewrite /own_chans /=.
     repeat iDestruct (wand_refl (_ ∗ _) with "[$]") as "[? ?]".
@@ -158,7 +158,7 @@ Proof.
 
   (* Allocate the kv system used as a lockservice *)
   iMod (alloc_vkv (ekvParams.mk [lr1Host ; lr2Host ]) [(lconfigHost, lconfigHostPaxos)]
-                  {[ "init"; "a1"; "a2" ]} with "[Hl1 Hl2]") as "[Hlkv Hlconf]"; try (simpl; lia).
+                  {[ "init"; "a1"; "a2" ]}%go with "[Hl1 Hl2]") as "[Hlkv Hlconf]"; try (simpl; lia).
   {
     rewrite /own_chans /=.
     repeat iDestruct (wand_refl (_ ∗ _) with "[$]") as "[? ?]".
@@ -168,21 +168,21 @@ Proof.
   iSimpl in "Hlhost".
 
   (* set up bank *)
-  iAssert (|={⊤}=> is_bank "init" _ _ {[ "a1" ; "a2" ]})%I with "[Hlkvs Hkvs]" as ">#Hbank".
+  iAssert (|={⊤}=> is_bank "init"%go _ _ {[ "a1"%go ; "a2"%go ]})%I with "[Hlkvs Hkvs]" as ">#Hbank".
   {
-    iDestruct (big_sepS_delete _ _ "init" with "Hlkvs") as "(Hinit&Hlkvs)".
+    iDestruct (big_sepS_delete _ _ "init"%go with "Hlkvs") as "(Hinit&Hlkvs)".
     { set_solver. }
     instantiate (2:=Build_lock_names (kv_ptsto γl)).
     rewrite /is_bank.
     iMod (lock_alloc lockN {| kvptsto_lock := kv_ptsto γl |} _ "init" with "[Hinit] [-]") as "$"; last done.
     { iFrame. }
-    iDestruct (big_sepS_delete _ _ "init" with "Hkvs") as "(Hinit&Hkvs)".
+    iDestruct (big_sepS_delete _ _ "init"%go with "Hkvs") as "(Hinit&Hkvs)".
     { set_solver. }
     iLeft.
     instantiate (1:=kv_ptsto γd).
     iFrame.
     iApply (big_sepS_sep).
-    eassert (_ ∖ _ = {[ "a1"; "a2" ]}) as ->.
+    eassert (_ ∖ _ = {[ "a1"; "a2" ]}%go) as ->.
     { set_solver. }
     iFrame.
   }
diff --git a/src/program_proof/vrsm/apps/closed_wpcs.v b/src/program_proof/vrsm/apps/closed_wpcs.v
index ffa63b86a..e53316a12 100644
--- a/src/program_proof/vrsm/apps/closed_wpcs.v
+++ b/src/program_proof/vrsm/apps/closed_wpcs.v
@@ -321,11 +321,11 @@ Lemma wp_makeBankClerk γlk γkv (kvParams1 kvParams2:ekvParams.t):
   {{{
         "#Hhost1" ∷ is_kv_config_hosts (params:=kvParams1) [dconfigHost] γkv ∗
         "#Hhost2" ∷ is_kv_config_hosts (params:=kvParams2) [lconfigHost] γlk ∗
-        "#Hbank" ∷ is_bank "init" (Build_lock_names (kv_ptsto γlk)) (kv_ptsto γkv) {[ "a1"; "a2" ]}
+        "#Hbank" ∷ is_bank "init"%go (Build_lock_names (kv_ptsto γlk)) (kv_ptsto γkv) {[ "a1"%go; "a2"%go ]}
   }}}
     makeBankClerk #()
   {{{
-        (b:loc), RET #b; own_bank_clerk b {[ "a1" ; "a2" ]}
+        (b:loc), RET #b; own_bank_clerk b {[ "a1"%go ; "a2"%go ]}
   }}}
 .
 Proof.
@@ -364,7 +364,7 @@ Definition bank_pre : iProp Σ :=
   ∃ γkv γlk (p1 p2:ekvParams.t),
   "#Hhost1" ∷ is_kv_config_hosts (params:=p1)[dconfigHost] γkv ∗
   "#Hhost2" ∷ is_kv_config_hosts (params:=p2) [lconfigHost] γlk ∗
-  "#Hbank" ∷ is_bank "init" (Build_lock_names (kv_ptsto γlk)) (kv_ptsto γkv) {[ "a1"; "a2" ]}
+  "#Hbank" ∷ is_bank "init"%go (Build_lock_names (kv_ptsto γlk)) (kv_ptsto γkv) {[ "a1"%go; "a2"%go ]}
 .
 
 Lemma wp_bank_transferer_main :
@@ -703,7 +703,7 @@ Lemma alloc_vkv (params:ekvParams.t) configHostPairs allocated `{!ekvG Σ}:
   ={⊤}=∗ (∃ γ,
 
   (* system-wide: allows clients to connect to the system, and gives them ownership of keys *)
-  ([∗ set] k ∈ allocated, kv_ptsto γ k "") ∗
+  ([∗ set] k ∈ allocated, kv_ptsto γ k ""%go) ∗
   is_kv_config_hosts (configHostPairs.*1) γ ∗
 
   (* for each kv replica server:  *)
@@ -729,7 +729,7 @@ Proof.
   iMod (alloc_simplepb_system configHostPairs with "[$Hchan] [$HconfChan]") as (?) "H"; try done.
   iDestruct "H" as "(Hlog & #Hhosts & Hsrvs & HconfSrvs)".
   iFrame "HconfSrvs".
-  iMod (ghost_map_alloc (gset_to_gmap "" allocated)) as (γkv_gn) "[Hauth Hkvs]".
+  iMod (ghost_map_alloc (gset_to_gmap ""%go allocated)) as (γkv_gn) "[Hauth Hkvs]".
   iExists (Build_kv_names _ _).
   rewrite big_sepM_gset_to_gmap.
   iFrame "Hkvs".
diff --git a/src/program_proof/vrsm/apps/vkv/kv_proof.v b/src/program_proof/vrsm/apps/vkv/kv_proof.v
index cc3a52ee8..ccdfc21ee 100644
--- a/src/program_proof/vrsm/apps/vkv/kv_proof.v
+++ b/src/program_proof/vrsm/apps/vkv/kv_proof.v
@@ -66,7 +66,7 @@ Context `{!ekvG Σ}.
    [getOp] doing [default []]. *)
 Definition own_kvs γ ops : iProp Σ :=
   ∃ allocatedKeys,
-  ghost_map_auth γ.(kv_gn) 1 (compute_state ops ∪ gset_to_gmap "" allocatedKeys)
+  ghost_map_auth γ.(kv_gn) 1 (compute_state ops ∪ gset_to_gmap ""%go allocatedKeys)
 .
 
 Definition stateN := nroot .@ "state".
@@ -280,14 +280,13 @@ Proof.
   iIntros (?) "Hck Hsl".
   wp_apply (wp_StringFromBytes with "[$]").
   iIntros "_".
-  simpl. rewrite string_to_bytes_to_string /=.
   rewrite lookup_union in Hlook.
+  simpl.
   destruct (compute_state ops !! key) as [x|]; simpl.
   - simpl in Hlook. rewrite union_Some_l in Hlook.
     injection Hlook as <-.
     iApply "HΦ". repeat iExists _. iFrame "∗#".
-  -
-    rewrite left_id lookup_gset_to_gmap_Some in Hlook.
+  - rewrite left_id lookup_gset_to_gmap_Some in Hlook.
     destruct Hlook as [? ?]; subst.
     iApply "HΦ". repeat iExists _. iFrame "∗#".
 Qed.
@@ -307,7 +306,7 @@ Lemma wp_Clerk__CondPut ck γkv key expect val :
   <<< ∀∀ old_value, kv_ptsto γkv key old_value >>>
     Clerk__CondPut #ck #(str key) #(str expect) #(str val) @ (↑pbN ∪ ↑prophReadN ∪ ↑esmN ∪ ↑stateN)
   <<< kv_ptsto γkv key (if bool_decide (expect = old_value) then val else old_value) >>>
-  {{{ RET #(str (if bool_decide (expect = old_value) then "ok" else "")); own_Clerk ck γkv }}}.
+  {{{ RET #(str (if bool_decide (expect = old_value) then "ok"%go else ""%go)); own_Clerk ck γkv }}}.
 Proof.
   iIntros "%Φ !# Hck Hupd".
   wp_rec.
diff --git a/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v b/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v
index 27bf49cd8..b93f884da 100644
--- a/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v
+++ b/src/program_proof/vrsm/apps/vkv/kv_vsm_proof.v
@@ -13,9 +13,9 @@ From Perennial.algebra Require Import map.
 Section defns.
 
 Inductive kvOp :=
-  | putOp : byte_string → byte_string → kvOp
-  | getOp : byte_string → kvOp
-  | condPutOp : byte_string → byte_string → byte_string → kvOp
+  | putOp (k : byte_string) (v : byte_string) : kvOp
+  | getOp (k : byte_string) : kvOp
+  | condPutOp (k : byte_string) (e : byte_string) (v : byte_string) : kvOp
 .
 
 Definition apply_op (state:gmap byte_string byte_string) (op:kvOp) :=
@@ -504,17 +504,17 @@ Proof.
         iModIntro.
         iIntros.
         rewrite /typed_map.map_insert /= in H0.
-        destruct (decide (k = s0)).
+        destruct (decide (k = k0)).
         { subst. rewrite lookup_insert /= in H0.
           replace (vnum) with (vnum') by word.
           iExists _. by iDestruct "Hintermediate" as "[_ $]".
         }
-        assert (compute_reply (ops ++ [putOp s0 s1]) (getOp k) =
-                  compute_reply (ops) (getOp k)) as Heq; last setoid_rewrite Heq.
+        assert (compute_reply (ops ++ [putOp k v]) (getOp k0) =
+                  compute_reply (ops) (getOp k0)) as Heq; last setoid_rewrite Heq.
         {
           rewrite /compute_reply /= /compute_state.
           rewrite foldl_snoc /=.
-          by rewrite lookup_insert_ne.
+          rewrite lookup_insert_ne //.
         }
         rewrite lookup_insert_ne in H0; last done.
         destruct (decide (uint.nat vnum' <= uint.nat latestVnum)).
@@ -536,7 +536,7 @@ Proof.
       }
       {
         iPureIntro. intros.
-        destruct (decide (k = s0)).
+        destruct (decide (k = k0)).
         { subst.
           by rewrite /typed_map.map_insert lookup_insert /=.
         }
@@ -590,7 +590,7 @@ Proof.
       iSplitL.
       2: {
         iPureIntro. intros.
-        destruct (decide (k = s0)).
+        destruct (decide (k = k0)).
         { subst.
           by rewrite /typed_map.map_insert lookup_insert /=. }
         { rewrite /typed_map.map_insert lookup_insert_ne /=; last done.
@@ -601,13 +601,13 @@ Proof.
       iModIntro.
       iIntros.
       rewrite /typed_map.map_insert /= in H0.
-      destruct (decide (k = s0)).
+      destruct (decide (k = k0)).
       { subst. rewrite lookup_insert /= in H0.
         replace (vnum) with (vnum') by word.
         iExists _. by iDestruct "Hintermediate" as "[_ $]".
       }
-      eassert (compute_reply (ops ++ [_]) (getOp k) =
-                compute_reply (ops) (getOp k)) as Heq; last setoid_rewrite Heq.
+      eassert (compute_reply (ops ++ [_]) (getOp k0) =
+                compute_reply (ops) (getOp k0)) as Heq; last setoid_rewrite Heq.
       {
         rewrite /compute_reply /= /compute_state.
         rewrite foldl_snoc /=. done.
@@ -690,13 +690,13 @@ Proof.
           iModIntro.
           iIntros.
           rewrite /typed_map.map_insert /= in H0.
-          destruct (decide (k = s0)).
+          destruct (decide (k = k0)).
           { subst. rewrite lookup_insert /= in H1.
             replace (vnum) with (vnum') by word.
             iExists _. by iDestruct "Hintermediate" as "[_ $]".
           }
-          eassert (compute_reply (ops ++ [condPutOp s0 _ s2]) (getOp k) =
-                  compute_reply (ops) (getOp k)) as Heq; last setoid_rewrite Heq.
+          eassert (compute_reply (ops ++ [condPutOp k _ _]) (getOp k0) =
+                  compute_reply (ops) (getOp k0)) as Heq; last setoid_rewrite Heq.
           {
             rewrite /compute_reply /= /compute_state.
             rewrite foldl_snoc /=.
@@ -726,7 +726,7 @@ Proof.
         }
         {
           iPureIntro. intros.
-          destruct (decide (k = s0)).
+          destruct (decide (k = k0)).
           { subst.
             by rewrite /typed_map.map_insert lookup_insert /=.
           }
@@ -746,8 +746,6 @@ Proof.
       wp_apply wp_StringToBytes.
       injection Hlookup as <-.
       iIntros (?) "Hreply_sl".
-      assert (default "" (foldl apply_op ∅ ops !! s0) ≠ s1) as Hnot.
-      { intros x. apply Heqb. repeat f_equal. done. }
       iApply "HΦ".
       iSplitL "Hkvs Hkvs_map Hvnums HminVnum Hvnums_map".
       {
@@ -762,7 +760,7 @@ Proof.
           iModIntro.
           iIntros.
           iDestruct "Hintermediate" as "[Hintermediate Hcurst]".
-          assert (compute_state (ops ++ [condPutOp s0 s1 s2])
+          assert (compute_state (ops ++ [condPutOp k e v])
                                 = (compute_state ops)) as Heq.
           { rewrite /compute_state foldl_snoc /=.
             rewrite decide_False; done.
@@ -787,7 +785,7 @@ Proof.
         }
         {
           iPureIntro. intros.
-          specialize (Hle k).
+          specialize (Hle k0).
           word.
         }
       }
@@ -850,7 +848,7 @@ Proof.
   {
     wp_pures. iApply "HΦ". iModIntro.
     apply map_get_true in Hlookup.
-    pose proof (Hle s0) as Hle2.
+    pose proof (Hle k) as Hle2.
     rewrite Hlookup /= in Hle2.
     iSplitR. { word. }
     injection Hkv_lookup as <- ?.
@@ -858,7 +856,7 @@ Proof.
     rewrite /kv_record /compute_reply /= /compute_state /=.
     iSplitL.
     { repeat iExists _; iFrame "∗#%". }
-    iSpecialize ("Hst" $! s0).
+    iSpecialize ("Hst" $! k).
     rewrite Hlookup /=.
     iModIntro. iIntros.
     iApply "Hst".
@@ -869,7 +867,7 @@ Proof.
     wp_loadField. wp_pures. iApply "HΦ". iModIntro.
     apply map_get_false in Hlookup as [Hlookup Hv].
     subst.
-    pose proof (Hle s0) as Hle2.
+    pose proof (Hle k) as Hle2.
     rewrite Hlookup /= in Hle2.
     iSplitR. { word. }
     injection Hkv_lookup as <- ?.
@@ -877,7 +875,7 @@ Proof.
     rewrite /kv_record /compute_reply /= /compute_state /=.
     iSplitL.
     { repeat iExists _; iFrame "∗#%". }
-    iSpecialize ("Hst" $! s0).
+    iSpecialize ("Hst" $! k).
     rewrite Hlookup /=.
     iModIntro. iIntros.
     iApply "Hst".