Destruct txn, replica, and group coordinators

src/program_proof/tulip/program/gcoord/gcoord_abort.v

@@ -0,0 +1,68 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.gcoord Require Import
+  gcoord_repr gcoord_register_finalization gcoord_finalized gcoord_send
+  gcoord_get_leader gcoord_change_leader.
+
+Section program.
+  Context `{!heapGS Σ, !tulip_ghostG Σ}.
+
+  Theorem wp_GroupCoordinator__Abort (gcoord : loc) (tsW : u64) gid γ :
+    let ts := uint.nat tsW in
+    safe_abort γ ts -∗
+    is_gcoord gcoord gid γ -∗
+    {{{ True }}}
+      GroupCoordinator__Abort #gcoord #tsW
+    {{{ RET #(); True }}}.
+  Proof.
+    iIntros (ts) "#Habted #Hgcoord".
+    iIntros (Φ) "!> _ HΦ".
+    wp_rec.
+
+    (*@ func (gcoord *GroupCoordinator) Abort(ts uint64) {                      @*)
+    (*@     gcoord.RegisterFinalization(ts)                                     @*)
+    (*@                                                                         @*)
+    wp_apply (wp_GroupCoordinator__RegisterFinalization with "Hgcoord").
+    iNamed "Hgcoord".
+    wp_apply (wp_GroupCoordinator__GetLeader with "Hgcoord").
+    iIntros (leader Hleader).
+    wp_apply wp_ref_to; first by auto.
+    iIntros (leaderP) "HleaderP".
+    wp_pures.
+
+    (*@     var leader = gcoord.GetLeader()                                     @*)
+    (*@     for !gcoord.Finalized(ts) {                                         @*)
+    (*@         gcoord.SendAbort(leader, ts)                                    @*)
+    (*@         primitive.Sleep(params.NS_RESEND_ABORT)                         @*)
+    (*@         // Retry with different leaders until success.                  @*)
+    (*@         leader = gcoord.ChangeLeader()                                  @*)
+    (*@     }                                                                   @*)
+    (*@ }                                                                       @*)
+    set P := (λ _ : bool, ∃ leader' : u64, leaderP ↦[uint64T] #leader' ∗ ⌜leader' ∈ dom addrm⌝)%I.
+    wp_apply (wp_forBreak_cond P with "[] [$HleaderP]"); last first; first 1 last.
+    { done. }
+    { clear Φ.
+      iIntros (Φ) "!> HP HΦ".
+      wp_apply (wp_GroupCoordinator__Finalized with "[]").
+      { iFrame "Hgcoord". }
+      iIntros (finalized) "_".
+      wp_pures.
+      destruct finalized; wp_pures.
+      { by iApply "HΦ". }
+      iDestruct "HP" as (leader') "[HleaderP %Hin]".
+      wp_load.
+      wp_apply (wp_GroupCoordinator__SendAbort with "Habted").
+      { iFrame "Hgcoord". }
+      wp_apply wp_Sleep.
+      wp_apply (wp_GroupCoordinator__ChangeLeader).
+      { iFrame "Hgcoord". }
+      iIntros (leadernew Hleadernew).
+      wp_store.
+      iApply "HΦ".
+      by iFrame.
+    }
+    iIntros "_".
+    wp_pures.
+    by iApply "HΦ".
+  Qed.
+
+End program.

src/program_proof/tulip/program/gcoord/gcoord_attached_with.v

@@ -0,0 +1,62 @@
+From Perennial.program_proof.tulip.invariance Require Import read.
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.gcoord Require Import gcoord_repr.
+
+Section program.
+  Context `{!heapGS Σ, !tulip_ghostG Σ}.
+
+  Theorem wp_GroupCoordinator__attachedWith (gcoord : loc) (tsW : u64) tscur rids gid γ :
+    let ts := uint.nat tsW in
+    {{{ own_gcoord_core gcoord tscur gid rids γ }}}
+      GroupCoordinator__attachedWith #gcoord #tsW
+    {{{ (ok : bool), RET #ok;
+        if ok
+        then own_gcoord_core gcoord ts gid rids γ
+        else own_gcoord_core gcoord tscur gid rids γ
+    }}}.
+  Proof.
+    iIntros (ts Φ) "Hgcoord HΦ".
+    wp_rec.
+
+    (*@ func (gcoord *GroupCoordinator) attachedWith(ts uint64) bool {          @*)
+    (*@     return gcoord.ts == ts                                              @*)
+    (*@ }                                                                       @*)
+    iNamed "Hgcoord".
+    rename tsW into tsargW. iNamed "Hts".
+    wp_loadField.
+    wp_pures.
+    case_bool_decide as Htsarg.
+    { iApply "HΦ". inv Htsarg. by iFrame "∗ # %". }
+    { iApply "HΦ". by iFrame "∗ # %". }
+  Qed.
+
+  Theorem wp_GroupCoordinator__AttachedWith (gcoord : loc) (ts : u64) gid γ :
+    is_gcoord gcoord gid γ -∗
+    {{{ True }}}
+      GroupCoordinator__AttachedWith #gcoord #ts
+    {{{ (attached : bool), RET #attached; True }}}.
+  Proof.
+    iIntros "#Hgcoord" (Φ) "!> _ HΦ".
+    wp_rec.
+
+    (*@ func (gcoord *GroupCoordinator) AttachedWith(ts uint64) bool {          @*)
+    (*@     gcoord.mu.Lock()                                                    @*)
+    (*@     b := gcoord.attachedWith(ts)                                        @*)
+    (*@     gcoord.mu.Unlock()                                                  @*)
+    (*@     return b                                                            @*)
+    (*@ }                                                                       @*)
+    do 2 iNamed "Hgcoord".
+    wp_loadField.
+    wp_apply (wp_Mutex__Lock with "Hlock").
+    iIntros "[Hlocked Hgcoord]".
+    do 2 iNamed "Hgcoord".
+    wp_apply (wp_GroupCoordinator__attachedWith with "Hgcoord").
+    iIntros (b) "Hgcoord".
+    wp_loadField.
+    wp_apply (wp_Mutex__Unlock with "[-HΦ]").
+    { iFrame "Hlock Hlocked". by destruct b; iFrame. }
+    wp_pures.
+    by iApply "HΦ".
+  Qed.
+
+End program.

src/program_proof/tulip/program/gcoord/gcoord_change_leader.v

@@ -0,0 +1,59 @@
+From Perennial.program_proof.tulip.invariance Require Import read.
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.gcoord Require Import gcoord_repr.
+
+Section program.
+  Context `{!heapGS Σ, !tulip_ghostG Σ}.
+
+  Theorem wp_GroupCoordinator__ChangeLeader (gcoord : loc) gid addrm γ :
+    is_gcoord_with_addrm gcoord gid addrm γ -∗
+    {{{ True }}}
+      GroupCoordinator__ChangeLeader #gcoord
+    {{{ (leader : u64), RET #leader; ⌜leader ∈ dom addrm⌝ }}}.
+  Proof.
+    iIntros "#Hgcoord" (Φ) "!> _ HΦ".
+    wp_rec.
+
+    (*@ func (gcoord *GroupCoordinator) ChangeLeader() uint64 {                 @*)
+    (*@     gcoord.mu.Lock()                                                    @*)
+    (*@     leader := (gcoord.leader + 1) % uint64(len(gcoord.addrm))             @*)
+    (*@     gcoord.leader = leader                                              @*)
+    (*@     gcoord.mu.Unlock()                                                  @*)
+    (*@     return leader                                                       @*)
+    (*@ }                                                                       @*)
+    iNamed "Hgcoord".
+    wp_loadField.
+    wp_apply (wp_Mutex__Lock with "Hlock").
+    iIntros "[Hlocked Hgcoord]".
+    do 3 iNamed "Hgcoord". iNamed "Hgfl".
+    iNamed "Haddrm".
+    do 2 wp_loadField.
+    wp_apply wp_slice_len.
+    wp_storeField.
+    iMod (readonly_load with "Hrps") as (q) "Hrpsro".
+    iDestruct (own_slice_small_sz with "Hrpsro") as %Hlenrps.
+    wp_loadField.
+    set idxleader' := word.modu _ _.
+    assert (Hltrps : (uint.nat idxleader' < length rps)%nat).
+    { assert (size (dom addrm) = length rps) as Hszaddrm.
+      { by rewrite Hdomaddrm size_list_to_set. }
+      rewrite word.unsigned_modu_nowrap; [word | lia].
+    }
+    wp_apply (wp_Mutex__Unlock with "[-HΦ Hrpsro]").
+    { iFrame "Hlock Hlocked Hts Hgrd Hgpp Hcomm ∗ %".
+      iPureIntro.
+      rewrite Hdomaddrm size_list_to_set; [lia | done].
+    }
+    wp_pures.
+    wp_loadField.
+    assert (is_Some (rps !! uint.nat idxleader')) as [leader Hlead].
+    { by apply lookup_lt_is_Some. }
+    wp_apply (wp_SliceGet with "[$Hrpsro]").
+    { done. }
+    iIntros "_".
+    iApply "HΦ".
+    apply elem_of_list_lookup_2 in Hlead.
+    by rewrite Hdomaddrm elem_of_list_to_set.
+  Qed.
+
+End program.

src/program_proof/tulip/program/gcoord/gcoord_commit.v

@@ -0,0 +1,73 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.gcoord Require Import
+  gcoord_repr gcoord_register_finalization gcoord_finalized gcoord_send
+  gcoord_get_leader gcoord_change_leader.
+
+Section program.
+  Context `{!heapGS Σ, !tulip_ghostG Σ}.
+
+  Theorem wp_GroupCoordinator__Commit
+    (gcoord : loc) (tsW : u64) (pwrsP : loc) q (pwrs : dbmap) gid γ :
+    let ts := uint.nat tsW in
+    safe_commit γ gid ts pwrs -∗
+    is_gcoord gcoord gid γ -∗
+    {{{ own_map pwrsP q pwrs }}}
+      GroupCoordinator__Commit #gcoord #tsW #pwrsP
+    {{{ RET #(); own_map pwrsP q pwrs }}}.
+  Proof.
+    iIntros (ts) "#Hcmted #Hgcoord".
+    iIntros (Φ) "!> Hpwrs HΦ".
+    wp_rec.
+
+    (*@ func (gcoord *GroupCoordinator) Commit(ts uint64, pwrs tulip.KVMap) {   @*)
+    (*@     gcoord.RegisterFinalization(ts)                                     @*)
+    (*@                                                                         @*)
+    wp_apply (wp_GroupCoordinator__RegisterFinalization with "Hgcoord").
+    iNamed "Hgcoord".
+    wp_apply (wp_GroupCoordinator__GetLeader with "Hgcoord").
+    iIntros (leader Hleader).
+    wp_apply wp_ref_to; first by auto.
+    iIntros (leaderP) "HleaderP".
+    wp_pures.
+
+    (*@     var leader = gcoord.GetLeader()                                     @*)
+    (*@     for !gcoord.Finalized(ts) {                                         @*)
+    (*@         gcoord.SendCommit(leader, ts, pwrs)                             @*)
+    (*@         primitive.Sleep(params.NS_RESEND_COMMIT)                        @*)
+    (*@         // Retry with different leaders until success.                  @*)
+    (*@         leader = gcoord.ChangeLeader()                                  @*)
+    (*@     }                                                                   @*)
+    (*@ }                                                                       @*)
+    set P := (λ _ : bool, ∃ leader' : u64,
+                 "HleaderP"  ∷ leaderP ↦[uint64T] #leader' ∗
+                 "Hpwrs"     ∷ own_map pwrsP q pwrs ∗
+                 "%Hinaddrm" ∷ ⌜leader' ∈ dom addrm⌝)%I.
+    wp_apply (wp_forBreak_cond P with "[] [$Hpwrs $HleaderP]"); last first; first 1 last.
+    { done. }
+    { clear Φ.
+      iIntros (Φ) "!> HP HΦ".
+      wp_apply (wp_GroupCoordinator__Finalized with "[]").
+      { iFrame "Hgcoord". }
+      iIntros (finalized) "_".
+      wp_pures.
+      destruct finalized; wp_pures.
+      { by iApply "HΦ". }
+      iNamed "HP".
+      wp_load.
+      wp_apply (wp_GroupCoordinator__SendCommit with "Hcmted [] Hpwrs").
+      { iFrame "Hgcoord". }
+      iIntros "Hpwrs".
+      wp_apply wp_Sleep.
+      wp_apply (wp_GroupCoordinator__ChangeLeader).
+      { iFrame "Hgcoord". }
+      iIntros (leadernew Hleadernew).
+      wp_store.
+      iApply "HΦ".
+      by iFrame.
+    }
+    iNamed 1.
+    wp_pures.
+    by iApply "HΦ".
+  Qed.
+
+End program.

src/program_proof/tulip/program/gcoord/gcoord_finalized.v

@@ -0,0 +1,37 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.gcoord Require Import gcoord_repr.
+
+Section program.
+  Context `{!heapGS Σ, !tulip_ghostG Σ}.
+
+  Theorem wp_GroupCoordinator__Finalized (gcoord : loc) (tsW : u64) gid γ :
+    is_gcoord gcoord gid γ -∗
+    {{{ True }}}
+      GroupCoordinator__Finalized #gcoord #tsW
+    {{{ (finalized : bool), RET #finalized; True }}}.
+  Proof.
+    iIntros "#Hgcoord" (Φ) "!> _ HΦ".
+    wp_rec.
+
+    (*@ func (gcoord *GroupCoordinator) Finalized(ts uint64) bool {             @*)
+    (*@     gcoord.mu.Lock()                                                    @*)
+    (*@     _, ok := gcoord.tsfinals[ts]                                        @*)
+    (*@     gcoord.mu.Unlock()                                                  @*)
+    (*@     return !ok                                                          @*)
+    (*@ }                                                                       @*)
+    do 2 iNamed "Hgcoord".
+    wp_loadField.
+    wp_apply (wp_Mutex__Lock with "Hlock").
+    iIntros "[Hlocked Hgcoord]".
+    do 3 iNamed "Hgcoord". iNamed "Hgfl".
+    wp_loadField.
+    wp_apply (wp_MapGet with "Htsfinals").
+    iIntros (v ok) "[%Hok Htsfinals]".
+    wp_loadField.
+    wp_apply (wp_Mutex__Unlock with "[-HΦ]").
+    { by iFrame "Hlock Hlocked Hts Hgrd Hgpp Hcomm ∗ %". }
+    wp_pures.
+    by iApply "HΦ".
+  Qed.
+
+End program.

src/program_proof/tulip/program/gcoord/gcoord_get_leader.v

@@ -0,0 +1,48 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.gcoord Require Import gcoord_repr.
+
+Section program.
+  Context `{!heapGS Σ, !tulip_ghostG Σ}.
+
+  Theorem wp_GroupCoordinator__GetLeader (gcoord : loc) gid addrm γ :
+    is_gcoord_with_addrm gcoord gid addrm γ -∗
+    {{{ True }}}
+      GroupCoordinator__GetLeader #gcoord
+    {{{ (leader : u64), RET #leader; ⌜leader ∈ dom addrm⌝ }}}.
+  Proof.
+    iIntros "#Hgcoord" (Φ) "!> _ HΦ".
+    wp_rec.
+
+    (*@ func (gcoord *GroupCoordinator) GetLeader() uint64 {                    @*)
+    (*@     gcoord.mu.Lock()                                                    @*)
+    (*@     leader := gcoord.leader                                             @*)
+    (*@     gcoord.mu.Unlock()                                                  @*)
+    (*@     return leader                                                       @*)
+    (*@ }                                                                       @*)
+    iNamed "Hgcoord".
+    wp_loadField.
+    wp_apply (wp_Mutex__Lock with "Hlock").
+    iIntros "[Hlocked Hgcoord]".
+    do 3 iNamed "Hgcoord". iNamed "Hgfl".
+    do 2 wp_loadField.
+    wp_apply (wp_Mutex__Unlock with "[-HΦ]").
+    { by iFrame "Hlock Hlocked Hts Hgrd Hgpp Hcomm ∗ %". }
+    wp_pures.
+    iNamed "Haddrm".
+    wp_loadField.
+    iMod (readonly_load with "Hrps") as (q) "Hrpsro".
+    assert (is_Some (rps !! uint.nat idxleader)) as [leader Hlead].
+    { apply lookup_lt_is_Some.
+      assert (length rps = size (dom addrm)); last word.
+      by rewrite Hdomaddrm size_list_to_set.
+    }
+    wp_apply (wp_SliceGet with "[$Hrpsro]").
+    { done. }
+    iIntros "_".
+    iApply "HΦ".
+    iPureIntro.
+    apply elem_of_list_lookup_2 in Hlead.
+    by rewrite Hdomaddrm elem_of_list_to_set.
+  Qed.
+
+End program.