Fix build

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) :=

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.

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. }

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

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) :=

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 γ -∗

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 ->

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 γ -∗

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 }}}

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 γ }}}.

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 γ }}}

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 γ }}}

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); 

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Φ".

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 γ }}}.

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 }}}

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.

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);

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' }}}.

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 ->

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) ∗

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) ->

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 :

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 ->

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 >>>

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)