Prove key to group

Author: yunshengtw

external/Goose/github_com/mit_pdos/tulip/txn.v

@@ -71,21 +71,21 @@ Definition Txn__resetwrs: val :=
     struct.storeF Txn "wrsp" "txn" (NewMap stringT (struct.t tulip.Value) #());;
     #().
 
-Definition KeyToGroup: val :=
-  rec: "KeyToGroup" "key" :=
-    (StringLength "key") `rem` #2.
+Definition Txn__keyToGroup: val :=
+  rec: "Txn__keyToGroup" "txn" "key" :=
+    (StringLength "key") `rem` (MapLen (struct.loadF Txn "wrs" "txn")).
 
 Definition Txn__setwrs: val :=
   rec: "Txn__setwrs" "txn" "key" "value" :=
-    let: "gid" := KeyToGroup "key" in
+    let: "gid" := Txn__keyToGroup "txn" "key" in
     let: "pwrs" := Fst (MapGet (struct.loadF Txn "wrs" "txn") "gid") in
     MapInsert "pwrs" "key" "value";;
     MapInsert (struct.loadF Txn "wrsp" "txn") "key" "value";;
     #().
 
 Definition Txn__getwrs: val :=
   rec: "Txn__getwrs" "txn" "key" :=
-    let: "gid" := KeyToGroup "key" in
+    let: "gid" := Txn__keyToGroup "txn" "key" in
     let: "pwrs" := Fst (MapGet (struct.loadF Txn "wrs" "txn") "gid") in
     let: ("v", "ok") := MapGet "pwrs" "key" in
     ("v", "ok").
@@ -177,7 +177,7 @@ Definition Txn__Read: val :=
     (if: "hit"
     then ("vlocal", #true)
     else
-      let: "gid" := KeyToGroup "key" in
+      let: "gid" := Txn__keyToGroup "txn" "key" in
       let: "gcoord" := Fst (MapGet (struct.loadF Txn "gcoords" "txn") "gid") in
       let: ("v", "ok") := gcoord.GroupCoordinator__Read "gcoord" (struct.loadF Txn "ts" "txn") "key" in
       (if: (~ "ok")

src/program_proof/rsm/pure/fin_sets.v

@@ -15,4 +15,9 @@ Section fin_set.
     filter P X ⊆ filter Q X.
   Proof. set_solver. Qed.
 
+  Lemma filter_subseteq_mono X Y (P : A -> Prop) `{!∀ x, Decision (P x)} :
+    X ⊆ Y ->
+    filter P X ⊆ filter P Y.
+  Proof. set_solver. Qed.
+
 End fin_set.

src/program_proof/tulip/base.v

@@ -4,6 +4,8 @@ From Perennial.base_logic Require Import ghost_map mono_nat saved_prop.
 From Perennial.program_proof Require Import grove_prelude.
 From Perennial.Helpers Require finite.
 
+Local Ltac Zify.zify_post_hook ::= Z.div_mod_to_equations.
+
 Definition dbkey := string.
 Definition dbval := option string.
 Definition dbhist := list dbval.
@@ -46,7 +48,7 @@ Definition txnst_to_u64 (s : txnst) :=
 Definition gids_all : gset u64 := list_to_set (fmap W64 (seqZ 0 2)).
 
 Lemma size_gids_all :
-  size gids_all < 2 ^ 64 - 1.
+  0 < size gids_all < 2 ^ 64 - 1.
 Proof.
   rewrite /gids_all size_list_to_set; last first.
   { apply seq_U64_NoDup; lia. }
@@ -160,8 +162,8 @@ Qed.
 Definition dblog := list ccommand.
 
 (** Converting keys to group IDs. *)
-Definition key_to_group (key : dbkey) : u64.
-Admitted.
+Definition key_to_group (key : dbkey) : u64 :=
+  String.length key `mod` size gids_all.
 
 (** Participant groups. *)
 Definition ptgroups (keys : gset dbkey) : gset u64 :=
@@ -185,7 +187,14 @@ Definition valid_pwrs (gid : u64) (pwrs : dbmap) :=
 
 Lemma elem_of_key_to_group key :
   key_to_group key ∈ gids_all.
-Admitted.
+Proof.
+  rewrite /key_to_group /gids_all.
+  rewrite size_list_to_set; last first.
+  { apply seq_U64_NoDup; lia. }
+  rewrite length_fmap length_seqZ.
+  apply elem_of_list_to_set, elem_of_list_fmap_1, elem_of_seqZ.
+  lia.
+Qed.
 
 Lemma elem_of_key_to_group_ptgroups key keys :
   key ∈ keys ->
@@ -284,6 +293,16 @@ Definition valid_wrs (wrs : dbmap) := dom wrs ⊆ keys_all.
 
 Definition valid_key (key : dbkey) := key ∈ keys_all.
 
+Lemma valid_key_length key :
+  valid_key key ->
+  String.length key < 2 ^ 64.
+Proof.
+  intros Hvk.
+  rewrite /valid_key /keys_all in Hvk.
+  apply elem_of_list_to_set, elem_of_list_fmap_2 in Hvk.
+  by destruct Hvk as ([k Hk] & -> & _).
+Qed.
+
 Definition valid_ccommand gid (c : ccommand) :=
   match c with
   | CmdCommit ts pwrs => valid_ts ts ∧ valid_pwrs gid pwrs

src/program_proof/tulip/inv_group.v

@@ -1,5 +1,5 @@
 From Perennial.program_proof Require Import grove_prelude.
-From Perennial.program_proof.rsm.pure Require Import list quorum fin_maps.
+From Perennial.program_proof.rsm.pure Require Import list quorum fin_maps fin_sets.
 From Perennial.program_proof.tulip Require Import base cmd res stability.
 
 Lemma tpls_group_keys_group_dom gid tpls :
@@ -447,7 +447,13 @@ Section lemma.
       iPureIntro.
       split; first done.
       rewrite /valid_pwrs Hwg wrs_group_keys_group_dom.
-      set_solver.
+      rewrite /valid_wrs in Hvw.
+      rewrite /keys_group.
+      (* [set_solver] is able to solve this directly when [key_to_group] is
+      admitted, but is unable to solve this after it is defined, so we apply an
+      additional lemma [filter_subseteq_mono]. *)
+      (* set_solver. *)
+      by apply filter_subseteq_mono.
     }
     { by iDestruct "Hsafec" as "[_ %Hvts]". }
   Qed.

src/program_proof/tulip/program/txn/key_to_group.v

@@ -5,11 +5,12 @@ Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
   Theorem wp_Txn__Delete txn tid key rds γ τ :
+    valid_key key ->
     {{{ own_txn txn tid rds γ τ ∗ (∃ vprev, txnmap_ptsto τ key vprev) }}}
       Txn__Delete #txn #(LitString key)
     {{{ RET #(); own_txn txn tid rds γ τ ∗ txnmap_ptsto τ key None }}}.
   Proof.
-    iIntros (Φ) "[Htxn [%v Hpt]] HΦ".
+    iIntros (Hvk Φ) "[Htxn [%v Hpt]] HΦ".
     wp_rec.
 
     (*@ func (txn *Txn) Delete(key string) {                                    @*)
@@ -21,6 +22,7 @@ Section program.
     iNamed "Htxn".
     wp_pures.
     wp_apply (wp_Txn__setwrs _ _ None with "Hwrs").
+    { apply Hvk. }
     iIntros "Hwrs".
     wp_pures.
     iApply "HΦ".

src/program_proof/tulip/program/txn/txn_delete.v

@@ -1,25 +1,27 @@
 From Perennial.program_proof.tulip.program Require Import prelude.
-From Perennial.program_proof.tulip.program.txn Require Import txn_repr key_to_group.
+From Perennial.program_proof.tulip.program.txn Require Import txn_repr txn_key_to_group.
 
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
-    Theorem wp_Txn__getwrs (txn : loc) (key : string) q wrs :
+  Theorem wp_Txn__getwrs (txn : loc) (key : string) q wrs :
+    valid_key key ->
     {{{ own_txn_wrs txn q wrs }}}
       Txn__getwrs #txn #(LitString key)
     {{{ (v : dbval) (ok : bool), RET (dbval_to_val v, #ok);
         own_txn_wrs txn q wrs ∗ ⌜wrs !! key = if ok then Some v else None⌝
     }}}.
   Proof.
-    iIntros (Φ) "Hwrs HΦ".
+    iIntros (Hvk Φ) "Hwrs HΦ".
     wp_rec.
 
     (*@ func (txn *Txn) getwrs(key string) (Value, bool) {                      @*)
     (*@     gid := KeyToGroup(key)                                              @*)
     (*@     pwrs := txn.wrs[gid]                                                @*)
     (*@                                                                         @*)
-    wp_apply wp_KeyToGroup.
-    iIntros (gid Hgid).
+    wp_apply (wp_Txn__keyToGroup with "Hwrs").
+    { apply Hvk. }
+    iIntros (gid) "[Hwrs %Hgid]".
     do 2 iNamed "Hwrs".
     wp_loadField.
     wp_apply (wp_MapGet with "HpwrsmP").

src/program_proof/tulip/program/txn/txn_getwrs.v

@@ -0,0 +1,39 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.txn Require Import txn_repr.
+
+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 :
+    valid_key key ->
+    {{{ own_txn_wrs txn q wrs }}}
+      Txn__keyToGroup #txn #(LitString key)
+    {{{ (gid : u64), RET #gid; own_txn_wrs txn q wrs ∗ ⌜key_to_group key = gid⌝ }}}.
+  Proof.
+    iIntros (Hvk Φ) "Htxn HΦ".
+    wp_rec.
+
+    (*@ func (txn *Txn) keyToGroup(key string) uint64 {                         @*)
+    (*@     return uint64(len(key)) % uint64(len(txn.gcoords))                  @*)
+    (*@ }                                                                       @*)
+    iNamed "Htxn".
+    wp_loadField.
+    iNamed "Hwrs".
+    wp_apply (wp_MapLen with "HpwrsmP").
+    iIntros "[%Hnoof HpwrsmP]".
+    wp_pures.
+    iApply "HΦ".
+    iFrame "∗ %".
+    iPureIntro.
+    rewrite /key_to_group.
+    rewrite -size_dom Hdomwrs.
+    pose proof size_gids_all as Hszall.
+    set x := String.length key.
+    set y := size gids_all.
+    apply valid_key_length in Hvk.
+    word.
+  Qed.
+
+End program.

src/program_proof/tulip/program/txn/txn_key_to_group.v

@@ -1,7 +1,7 @@
 From Perennial.program_proof.tulip.invariance Require Import read.
 From Perennial.program_proof.tulip.program Require Import prelude.
 From Perennial.program_proof.tulip.program.txn Require Import
-  res txn_repr txn_getwrs proph key_to_group.
+  res txn_repr txn_getwrs proph txn_key_to_group.
 From Perennial.program_proof.tulip.program.gcoord Require Import gcoord_read.
 
 Section program.
@@ -26,6 +26,7 @@ Section program.
     (*@                                                                         @*)
     iNamed "Htxn".
     wp_apply (wp_Txn__getwrs with "Hwrs").
+    { apply Hvk. }
     iIntros (vlocal ok) "[Hwrs %Hv]".
     iDestruct (txnmap_lookup with "Htxnmap Hpt") as %Hvalue.
     wp_if_destruct.
@@ -43,8 +44,9 @@ Section program.
     (*@     gcoord := txn.gcoords[gid]                                          @*)
     (*@     v, ok := gcoord.Read(txn.ts, key)                                   @*)
     (*@                                                                         @*)
-    wp_apply wp_KeyToGroup.
-    iIntros (gid Hgid).
+    wp_apply (wp_Txn__keyToGroup with "Hwrs").
+    { apply Hvk. }
+    iIntros (gid) "[Hwrs %Hgid]".
     iNamed "Hgcoords".
     wp_loadField.
     wp_apply (wp_MapGet with "Hgcoords").

src/program_proof/tulip/program/txn/txn_read.v

@@ -1,23 +1,25 @@
 From Perennial.program_proof.tulip.program Require Import prelude.
-From Perennial.program_proof.tulip.program.txn Require Import txn_repr key_to_group.
+From Perennial.program_proof.tulip.program.txn Require Import txn_repr txn_key_to_group.
 
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
   Theorem wp_Txn__setwrs (txn : loc) (key : string) (value : dbval) wrs :
+    valid_key key ->
     {{{ own_txn_wrs txn (DfracOwn 1) wrs }}}
       Txn__setwrs #txn #(LitString key) (dbval_to_val value)
     {{{ RET #(); own_txn_wrs txn (DfracOwn 1) (<[key := value]> wrs) }}}.
   Proof.
-    iIntros (Φ) "Hwrs HΦ".
+    iIntros (Hvk Φ) "Hwrs HΦ".
     wp_rec.
 
     (*@ func (txn *Txn) setwrs(key string, value Value) {                       @*)
     (*@     gid := KeyToGroup(key)                                              @*)
     (*@     pwrs := txn.wrs[gid]                                                @*)
     (*@                                                                         @*)
-    wp_apply wp_KeyToGroup.
-    iIntros (gid Hgid).
+    wp_apply (wp_Txn__keyToGroup with "Hwrs").
+    { apply Hvk. }
+    iIntros (gid) "[Hwrs %Hgid]".
     do 2 iNamed "Hwrs".
     wp_loadField.
     wp_apply (wp_MapGet with "HpwrsmP").