mk_sync -> lat

sync.v

@@ -83,8 +83,151 @@ Section proof.
     iFrame.
     by wp_seq.
   Qed.
+
+  (* a general way to get atomic triple from mk_styc *)
+
+  Definition atomic_triple' {A: Type}
+             (ϕ: A → iProp Σ)
+             (β: A → A → val → iProp Σ)
+             (Ei Eo: coPset)
+             (e: expr) : iProp Σ :=
+    (∀ P Q, (P ={Eo, Ei}=> ∃ g g',
+                                ϕ g ★
+                                (∀ v, β g g' v ={Ei, Eo}=★ Q v)
+            ) -★ {{ P }} e @ ⊤ {{ Q }})%I.
+  
 End proof.
 
+From iris.algebra Require Import dec_agree frac.
+From iris.program_logic Require Import auth.
+
+Definition pcas_R := authR (optionUR (prodR fracR (dec_agreeR (val * val)))).
+
+Class pcasG Σ := PcasG { pcas_tokG :> inG Σ pcas_R }.
+Definition pcasΣ : gFunctors := #[GFunctor (constRF pcas_R)].
+
+Section atomic_pair.
+  Context `{!heapG Σ, !lockG Σ, !pcasG Σ} (N : namespace).
+  
+  Definition pcas_seq : val :=
+    λ: "l1" "l2" "a" "b",
+       if: !"l1" = "a"
+         then if: !"l2" = "a"
+                then "l1" <- "b";; "l2" <- "b";; #true
+                else #false
+         else #false.
+
+  Lemma pcas_seq_spec (l1 l2: loc) (a b x1 x2: val):
+    ∀ (Φ: val → iProp Σ),
+      heapN ⊥ N →
+      heap_ctx ★ l1 ↦ x1 ★ l2 ↦ x2 ★
+      (■ (x1 = a ∧ x2 = a) -★ l1 ↦ b -★ l2 ↦ b -★ Φ #true)%I ★
+      (■ (¬ (x1 = a ∧ x2 = a)) -★ l1 ↦ x1 -★ l2 ↦ x2 -★ Φ #false)%I
+      ⊢ WP pcas_seq #l1 #l2 a b {{ Φ }}.
+  Proof.
+    iIntros (Φ HN) "(#Hh & Hl1 & Hl2 & HΦ1 & HΦ2)".
+    wp_seq. repeat wp_let.
+    wp_load.
+    wp_op=>[?|Hx1na].
+    - subst.
+      wp_if. wp_load.
+      wp_op=>[?|Hx2na]. subst.
+      + wp_if. wp_store. wp_store.
+        iAssert (■ (a = a ∧ a = a))%I as "Ha"; first by auto.
+        iApply ("HΦ1" with "Ha Hl1 Hl2").
+      + wp_if.
+        iAssert (■ ¬ (a = a ∧ x2 = a))%I as "Ha".
+        { iPureIntro. move=>[_ Heq]//. }
+        iApply ("HΦ2" with "Ha Hl1 Hl2").
+    - subst.
+      wp_if.
+        iAssert (■ ¬ (x1 = a ∧ x2 = a))%I as "Ha".
+        { iPureIntro. move=>[_ Heq]//. }
+        iApply ("HΦ2" with "Ha Hl1 Hl2").
+  Qed.
+
+  Definition mk_pcas : val :=
+    λ: "x1" "x2",
+       let: "l1" := ref "x1" in
+       let: "l2" := ref "x2" in
+       let: "lk" := newlock #() in
+       λ: "a" "b",
+          acquire "lk";;
+          let: "v" := pcas_seq "l1" "l2" "a" "b" in
+          release "lk";;
+          "v".
+
+  Definition gFullR (x1 x2: val) : pcas_R := ● Some ((1/2)%Qp, DecAgree (x1, x2)).
+  Definition gFragR (x1 x2: val) : pcas_R := ◯ Some ((1/2)%Qp, DecAgree (x1, x2)).
+
+  Definition gFull (x1 x2: val) γ: iProp Σ := own γ (gFullR x1 x2).
+  Definition gFrag (x1 x2: val) γ :iProp Σ := own γ (gFragR x1 x2).
+
+  Definition β (x1 x2 x1' x2' v a b: val) : iProp Σ :=
+    ((v = #true  ∧ x1 = a ∧ x2 = a ∧ x1' = b ∧ x2' = b) ∨
+     (v = #false ∧ x1 = a ∧ x2 = a ∧ x1' = b ∧ x2' = b))%I.
+  
+  Definition is_pcas γ (f: val) (Ei Eo: coPset) : iProp Σ :=
+    (∀ (a b: val) (Q: val → iProp Σ),
+      (∀ x1 x2 x1' x2' (r: val),
+         (True ={Ei, Eo}=> gFrag x1 x2 γ) ★
+         (gFrag x1' x2' γ ★ β x1 x2 x1' x2' r a b ={Eo, Ei}=> Q r)) -★ WP f a b {{ Q }})%I.
+
+  Lemma pcas_atomic_spec (x10 x20: val): (* let's fix Eo as ⊤, and Ei as heapN *)
+    heapN ⊥ N →
+    heap_ctx
+    ⊢ WP mk_pcas x10 x20 {{ f, ∃ γ, □ is_pcas γ f (⊤ ∖ nclose N) heapN }}.
+  Proof.
+    iIntros (HN) "#Hh". repeat wp_let.
+    wp_alloc l1 as "Hl1". wp_let.
+    wp_alloc l2 as "Hl2". iVs (own_alloc (gFullR x10 x20 ⋅ gFragR x10 x20)) as (γ) "Hγ"; first by done.
+    iDestruct (own_op with "Hγ") as "[Hfull Hfrag]".
+    iAssert (∃ x1 x2, l1 ↦ x1 ★ l2 ↦ x2 ★ gFull x1 x2 γ)%I with "[-Hfrag]" as "HR".
+    { iExists x10, x20. by iFrame. }
+    wp_let.
+    wp_bind (newlock _). iApply newlock_spec=>//.
+    iFrame "Hh".
+    iFrame "HR".
+    iIntros (lk γ') "#Hlk".
+    wp_let.
+    iClear "Hfrag". (* HFrag should be handled to user? *) 
+    iVsIntro. iExists γ. iAlways.
+    rewrite /is_pcas.
+    iIntros (a b Q) "H".
+    repeat wp_let.
+    wp_bind (acquire _).
+    iApply acquire_spec.
+    iFrame "Hlk". iIntros "Hlked Hls".
+    iDestruct "Hls" as (x1 x2) "(Hl1 & Hl2 & HFulla)".
+    wp_seq. repeat wp_let.
+    wp_load.
+    destruct (decide (x1 = a)).
+    - subst. wp_op=>[_|]//.
+      wp_if. wp_load.
+      destruct (decide (x2 = a)).
+      + subst. wp_op=>[_|]//.
+        wp_if. wp_store.
+        wp_store. wp_let.
+        wp_let.
+        iDestruct ("H" $! a a b b #true) as "[Hvs1 Hvs2]".
+        rewrite /is_lock.
+        iDestruct "Hlk" as (l) "(% & _ & % & Hinv)".
+        iInv N as ([]) ">[Hl _]" "Hclose".
+        * iVs ("Hvs1" with "[]") as "Hfraga"; first by auto.
+          subst. wp_store.
+          iAssert (β a a b b #true a b) as "Hβ".
+          { iLeft. eauto. }
+          iAssert (gFrag a a γ ★ gFull a a γ -★ gFrag b b γ ★ gFull b b γ)%I as "H".
+          { admit. }
+          iDestruct ("H" with "[Hfraga HFulla]") as "[HFragb HFullb]"; first by iFrame.
+          iVs ("Hvs2" with "[HFragb Hβ]"); first by iFrame.
+          rewrite /lock_inv.
+          iVsIntro. iVs ("Hclose" with "[-~]").
+          { iNext. iExists false.
+            iFrame. iExists b, b. by iFrame. }
+          iVsIntro. wp_seq. done.
+Admitted.
+
 Section sync_atomic.
   Context `{!heapG Σ, !lockG Σ} (N : namespace) {A: Type}.