Prove txn begin

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

@@ -54,6 +54,10 @@ Definition getTimestamp: val :=
 Definition Txn__begin: val :=
   rec: "Txn__begin" "txn" :=
     struct.storeF Txn "ts" "txn" (getTimestamp (struct.loadF Txn "sid" "txn"));;
+    #().
+
+Definition Txn__attach: val :=
+  rec: "Txn__attach" "txn" :=
     MapIter (struct.loadF Txn "gcoords" "txn") (λ: <> "gcoord",
       gcoord.GroupCoordinator__Attach "gcoord" (struct.loadF Txn "ts" "txn"));;
     #().
@@ -204,6 +208,7 @@ Definition Txn__Delete: val :=
 Definition Txn__Run: val :=
   rec: "Txn__Run" "txn" "body" :=
     Txn__begin "txn";;
+    Txn__attach "txn";;
     let: "cmt" := "body" "txn" in
     (if: (~ "cmt")
     then

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

@@ -0,0 +1,56 @@
+From Perennial.program_proof.tulip.program Require Import prelude.
+From Perennial.program_proof.tulip.program.txn Require Import txn_repr.
+From Perennial.program_proof.tulip.program.gcoord Require Import
+  gcoord_repr gcoord_attach.
+
+Section program.
+  Context `{!heapGS Σ, !tulip_ghostG Σ}.
+
+  Theorem wp_Txn__attach (txn : loc) ts γ :
+    {{{ ([∗ set] gid ∈ gids_all, own_txn_client_token γ ts gid) ∗ own_txn_init txn ts γ }}}
+      Txn__attach #txn
+    {{{ RET #(); own_txn_init txn ts γ }}}.
+  Proof.
+    iIntros (Φ) "[Hctks Htxn] HΦ".
+    wp_rec.
+
+    (*@ func (txn *Txn) attach() {                                              @*)
+    (*@     for _, gcoord := range(txn.gcoords) {                               @*)
+    (*@         gcoord.Attach(txn.ts)                                           @*)
+    (*@     }                                                                   @*)
+    (*@ }                                                                       @*)
+    do 2 iNamed "Htxn". iNamed "Hgcoords".
+    wp_loadField.
+    set P := (λ (mx : gmap u64 loc),
+                "Hts"   ∷ own_txn_ts txn ts ∗
+                "Hctks" ∷ [∗ set] gid ∈ gids_all ∖ (dom mx), own_txn_client_token γ ts gid)%I.
+    wp_apply (wp_MapIter_fold _ _ _ P with "Hgcoords [$Hts Hctks]").
+    { subst P. simpl. by rewrite dom_empty_L difference_empty_L. }
+    { clear Φ.
+      iIntros (m g p Φ) "!> [HP %Hp] HΦ".
+      destruct Hp as [Hnotin Hin].
+      iNamed "HP". iNamed "Hts".
+      wp_loadField.
+      iDestruct (big_sepS_delete _ _ g with "Hctks") as "[Hctk Hctks]".
+      { apply not_elem_of_dom_2 in Hnotin.
+        apply elem_of_dom_2 in Hin.
+        set_solver.
+      }
+      iDestruct (big_sepM_lookup with "Hgcoordsabs") as "Hgcoordabs".
+      { apply Hin. }
+      wp_apply (wp_GroupCoordinator__Attach with "Hgcoordabs [Hctk]").
+      { by rewrite Htsword. }
+      iApply "HΦ".
+      iFrame "∗ %".
+      by rewrite dom_insert_L difference_difference_l_L union_comm_L.
+    }
+    iIntros "[Hgcoords HP]".
+    iNamed "HP".
+    wp_pures.
+    iApply "HΦ".
+    iAssert (own_txn_gcoords txn γ)%I with "[Hgcoords HgcoordsP]" as "Hgcoords".
+    { by iFrame "∗ # %". }
+    by iFrame "∗ # %".
+  Qed.
+
+End program.

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

@@ -4,18 +4,59 @@ From Perennial.program_proof.tulip.program.txn Require Import txn_repr.
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
 
+  Theorem wp_getTimestamp (sid : u64) γ :
+    ⊢
+    {{{ True }}}
+    <<< ∀∀ (ts : nat), own_largest_ts γ ts >>>
+      getTimestamp #sid @ ↑tsNS
+    <<< ∃∃ (ts' : nat), own_largest_ts γ ts' ∗ ⌜(ts < ts')%nat⌝ >>>
+    {{{ (tid : u64), RET #tid; ⌜uint.nat tid = ts'⌝ }}}.
+  Proof.
+    iIntros (Φ) "!> _ HAU".
+    wp_rec.
+
+    (*@ func getTimestamp(sid uint64) uint64 {                                  @*)
+    (*@     ts := trusted_time.GetTime()                                        @*)
+    (*@                                                                         @*)
+    (*@     n := params.N_TXN_SITES                                             @*)
+    (*@     tid := std.SumAssumeNoOverflow(ts, n) / n * n + sid                 @*)
+    (*@                                                                         @*)
+    (*@     for trusted_time.GetTime() <= tid {                                 @*)
+    (*@     }                                                                   @*)
+    (*@                                                                         @*)
+    (*@     return tid                                                          @*)
+    (*@ }                                                                       @*)
+  Admitted.
+
   Theorem wp_Txn__begin (txn : loc) γ :
     ⊢ {{{ own_txn_uninit txn γ }}}
       <<< ∀∀ (ts : nat), own_largest_ts γ ts >>>
         Txn__begin #txn @ ↑tsNS
       <<< ∃∃ (ts' : nat), own_largest_ts γ ts' ∗ ⌜(ts < ts')%nat⌝ >>>
       {{{ RET #(); own_txn_init txn ts' γ }}}.
   Proof.
+    iIntros (Φ) "!> Htxn HAU".
+    wp_rec.
+
     (*@ func (txn *Txn) begin() {                                               @*)
-    (*@     // TODO                                                             @*)
-    (*@     // Ghost action: Linearize.                                         @*)
-    (*@     txn.ts = GetTS()                                                    @*)
-    (*@ }                                                                       @*)
-  Admitted.
+    (*@     txn.ts = getTimestamp(txn.sid)                                      @*)
+    (*@                                                                         @*)
+    do 2 iNamed "Htxn". iNamed "Hsid".
+    wp_loadField.
+    wp_apply (wp_getTimestamp).
+    iNamed "Hts".
+    iMod "HAU" as (ts) "[Hts HAU]".
+    iFrame "Hts".
+    iIntros "!>" (ts') "[Hts %Hts]".
+    iMod ("HAU" with "[$Hts]") as "HΦ"; first done.
+    iModIntro.
+    iIntros (tidW HtidW).
+    wp_storeField.
+    iApply "HΦ".
+    iAssert (own_txn_ts txn ts')%I with "[$HtsW]" as "Hts"; first done.
+    iFrame "∗ #".
+    iPureIntro.
+    rewrite /valid_ts. word.
+  Qed.
 
 End program.

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

@@ -49,9 +49,15 @@ Section repr.
       "#Hgcoordsabs" ∷ ([∗ map] gid ↦ gcoord ∈ gcoords, is_gcoord gcoord gid γ) ∗
       "%Hdomgcoords" ∷ ⌜dom gcoords = gids_all⌝.
 
+  Definition own_txn_sid txn : iProp Σ :=
+    ∃ (sid : u64),
+      (* TODO: sid token *)
+      "HsidP" ∷ txn ↦[Txn :: "sid"] #sid.
+
   Definition own_txn_internal txn tid γ : iProp Σ :=
     ∃ (proph : proph_id),
       "Hts"      ∷ own_txn_ts txn tid ∗
+      "Hsid"     ∷ own_txn_sid txn ∗
       "Hwrs"     ∷ own_txn_wrs txn (DfracOwn 1) ∅ ∗
       "Hgcoords" ∷ own_txn_gcoords txn γ ∗
       "Hptgs"    ∷ own_txn_ptgs txn [] ∗
@@ -68,6 +74,7 @@ Section repr.
   Definition own_txn txn tid rds γ τ : iProp Σ :=
     ∃ (proph : proph_id) wrs,
       "Htxn"     ∷ own_txn_ts txn tid ∗
+      "Hsid"     ∷ own_txn_sid txn ∗
       "Hwrs"     ∷ own_txn_wrs txn (DfracOwn 1) wrs ∗
       "Hgcoords" ∷ own_txn_gcoords txn γ ∗
       "Hptgs"    ∷ own_txn_ptgs txn [] ∗
@@ -87,6 +94,7 @@ Section repr.
     Definition own_txn_stable txn tid rds wrs γ τ : iProp Σ :=
     ∃ (proph : proph_id),
       "Htxn"     ∷ own_txn_ts txn tid ∗
+      "Hsid"     ∷ own_txn_sid txn ∗
       (* diff from [own_txn] *)
       "Hwrs"     ∷ own_txn_wrs txn DfracDiscarded wrs ∗
       "Hgcoords" ∷ own_txn_gcoords txn γ ∗
@@ -105,6 +113,7 @@ Section repr.
   Definition own_txn_prepared txn tid rds wrs γ τ : iProp Σ :=
     ∃ (proph : proph_id) ptgs,
       "Htxn"     ∷ own_txn_ts txn tid ∗
+      "Hsid"     ∷ own_txn_sid txn ∗
       "Hwrs"     ∷ own_txn_wrs txn DfracDiscarded wrs ∗
       "Hgcoords" ∷ own_txn_gcoords txn γ ∗
       (* diff from [own_txn_stable] *)

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

@@ -1,7 +1,8 @@
 From Perennial.program_proof.tulip.invariance Require Import linearize preprepare.
 From Perennial.program_proof.tulip.program Require Import prelude.
 From Perennial.program_proof.tulip.program.txn Require Import
-  res txn_repr txn_begin txn_cancel txn_prepare txn_reset txn_abort txn_commit.
+  res txn_repr txn_begin txn_attach txn_cancel txn_prepare
+  txn_reset txn_abort txn_commit.
 
 Section program.
   Context `{!heapGS Σ, !tulip_ghostG Σ}.
@@ -76,13 +77,17 @@ Section program.
       (* Allocate transaction local view [txnmap_ptstos τ r]. *)
       iMod (txnmap_alloc rds) as (τ) "[Htxnmap Htxnpts]".
       iIntros "!> Htxn".
+      wp_pures.
+      wp_apply (wp_Txn__attach with "[$Hclients $Htxn]").
+      iIntros "Htxn".
       iAssert (own_txn txn tid rds γ τ)%I with "[Htxn Htxnmap]" as "Htxn".
       { iClear "Hinv". do 2 iNamed "Htxn".
         iExists _, ∅.
         rewrite map_empty_union.
         by iFrame "∗ # %".
       }
 
+
       (*@     cmt := body(txn)                                                    @*)
       (*@                                                                         @*)
       wp_apply ("Hbody" with "[$Htxn $Htxnpts]"); first done.
@@ -207,6 +212,8 @@ Section program.
       (* Allocate transaction local view [txnmap_ptstos τ r]. *)
       iMod (txnmap_alloc rds) as (τ) "[Htxnmap Htxnpts]".
       iIntros "!> Htxn".
+      wp_apply (wp_Txn__attach with "[$Hclients $Htxn]").
+      iIntros "Htxn".
       iAssert (own_txn txn tid rds γ τ)%I with "[Htxn Htxnmap]" as "Htxn".
       { do 2 iNamed "Htxn".
         iExists _, ∅.