From 744a9606bbc0c65365525adc1cc65f171f64f48b Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Sat, 11 Dec 2021 15:34:34 +0100
Subject: [PATCH] Incorporate the `Xchg` operation

---
 theories/logic/compatibility.v          | 19 ++++++
 theories/logic/proofmode/spec_tactics.v | 45 ++++++++++++++
 theories/logic/proofmode/tactics.v      | 80 +++++++++++++++++++++++++
 theories/logic/rules.v                  | 26 ++++++++
 theories/logic/spec_rules.v             | 31 ++++++++++
 theories/tests/proofmode_tests.v        | 24 ++++++++
 theories/typing/fundamental.v           | 13 ++++
 theories/typing/types.v                 |  1 +
 8 files changed, 239 insertions(+)

diff --git a/theories/logic/compatibility.v b/theories/logic/compatibility.v
index 7acf8e5..2258c62 100644
--- a/theories/logic/compatibility.v
+++ b/theories/logic/compatibility.v
@@ -93,6 +93,25 @@ Section compatibility.
     value_case.
   Qed.
 
+  Lemma refines_xchg e1 e2 e1' e2' A :
+    (REL e1 << e1' : ref A) -âˆ—
+    (REL e2 << e2' : A) -âˆ—
+    REL Xchg e1 e2 << Xchg e1' e2' : A.
+  Proof.
+    iIntros "IH1 IH2".
+    rel_bind_ap e2 e2' "IH2" w w' "IH2".
+    rel_bind_ap e1 e1' "IH1" v v' "IH1".
+    iDestruct "IH1" as (l l') "(% & % & Hinv)"; simplify_eq/=.
+    rel_xchg_l_atomic.
+    iInv (relocN .@ "ref" .@ (l,l')) as (v v') "[Hv1 [>Hv2 #Hv]]" "Hclose".
+    iModIntro. iExists _; iFrame "Hv1".
+    iNext. iIntros "Hw1".
+    rel_xchg_r.
+    iMod ("Hclose" with "[Hw1 Hv2 IH2]").
+    { iNext; iExists _, _; simpl; iFrame. }
+    value_case.
+  Qed.
+
   Lemma refines_load e e' A :
     (REL e << e' : ref A) -âˆ—
     REL !e << !e' : A.
diff --git a/theories/logic/proofmode/spec_tactics.v b/theories/logic/proofmode/spec_tactics.v
index 3559799..87daee7 100644
--- a/theories/logic/proofmode/spec_tactics.v
+++ b/theories/logic/proofmode/spec_tactics.v
@@ -190,6 +190,51 @@ Tactic Notation "tp_store" constr(j) :=
   |iAssumptionCore || fail "tp_store: cannot find '? â†¦â‚› ?'"
   |pm_reduce (* new goal *)].
 
+
+Lemma tac_tp_xchg `{relocG Î£} k Î”1 Î”2 E1 i1 i2 K' e (l : loc) e' e2 v' v Q :
+  (âˆ€ P, ElimModal True false false (|={E1}=> P) P Q Q) â†’
+  nclose specN âŠ† E1 â†’
+  envs_lookup_delete false i1 Î”1 = Some (false, refines_right k e, Î”2)%I â†’
+  e = fill K' (Xchg (# l) e') â†’
+  IntoVal e' v â†’
+  (* re-compose the expression and the evaluation context *)
+  envs_lookup i2 Î”2 = Some (false, l â†¦â‚› v')%I â†’
+  e2 = fill K' (of_val v') â†’
+  match envs_simple_replace i2 false
+     (Esnoc (Esnoc Enil i1 (refines_right k e2)) i2 (l â†¦â‚› v)) Î”2 with
+  | None => False
+  | Some Î”3 => envs_entails Î”3 Q
+  end â†’
+  envs_entails Î”1 Q.
+Proof.
+  rewrite /IntoVal.
+  rewrite envs_entails_eq. intros ??? -> <- ? -> HQ.
+  rewrite envs_lookup_delete_sound //; simpl.
+  destruct (envs_simple_replace _ _ _ _) as [Î”3|] eqn:HÎ”3; last done.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id.
+  rewrite !assoc -(assoc _ spec_ctx).
+  rewrite -fill_app step_xchg // fill_app.
+  rewrite -[Q]elim_modal //.
+  apply bi.sep_mono_r.
+  apply bi.wand_intro_l.
+  rewrite (comm _ _ (l â†¦â‚› v)%I). simpl.
+  rewrite assoc. rewrite (comm _ spec_ctx (l â†¦â‚› _)%I).
+  by rewrite bi.wand_elim_r.
+Qed.
+
+Tactic Notation "tp_xchg" constr(j) :=
+  iStartProof;
+  eapply (tac_tp_store j);
+  [iSolveTC || fail "tp_store: cannot eliminate modality in the goal"
+  |solve_ndisj || fail "tp_store: cannot prove 'nclose specN âŠ† ?'"
+  |iAssumptionCore || fail "tp_store: cannot find '" j " ' RHS"
+  |tp_bind_helper
+  |iSolveTC || fail "tp_store: cannot convert the argument to a value"
+  |iAssumptionCore || fail "tp_store: cannot find '? â†¦â‚› ?'"
+  |simpl; reflexivity || fail "tp_store: this should not happen"
+  |pm_reduce (* new goal *)].
+
 (* *)
 (* DF: *)
 (* If [envs_lookup i1 Î”1 = Some (p, spec_ctx Ï)] and *)
diff --git a/theories/logic/proofmode/tactics.v b/theories/logic/proofmode/tactics.v
index 4b87c06..8d70e8f 100644
--- a/theories/logic/proofmode/tactics.v
+++ b/theories/logic/proofmode/tactics.v
@@ -348,6 +348,86 @@ Tactic Notation "rel_store_r" :=
   |reflexivity
   |rel_finish  (** new goal *)].
 
+(** Xchg *)
+Lemma tac_rel_xchg_l_simpl `{!relocG Î£} K â„¶1 â„¶2 â„¶3 i1 (l : loc) v e' v' e t eres A :
+  e = fill K (Xchg (# l) e') â†’
+  IntoVal e' v' â†’
+  MaybeIntoLaterNEnvs 1 â„¶1 â„¶2 â†’
+  envs_lookup i1 â„¶2 = Some (false, l â†¦ v)%I â†’
+  envs_simple_replace i1 false (Esnoc Enil i1 (l â†¦ v')) â„¶2 = Some â„¶3 â†’
+  eres = fill K (of_val v) â†’
+  envs_entails â„¶3 (refines âŠ¤ eres t A) â†’
+  envs_entails â„¶1 (refines âŠ¤ e t A).
+Proof.
+  rewrite envs_entails_eq. intros ?????? Hg.
+  subst e eres.
+  rewrite into_laterN_env_sound envs_simple_replace_sound //; simpl.
+  rewrite bi.later_sep.
+  rewrite right_id.
+  rewrite -(refines_xchg_l K âŠ¤ l).
+  rewrite -fupd_intro.
+  rewrite -(bi.exist_intro v).
+  by rewrite Hg.
+Qed.
+
+Lemma tac_rel_xchg_r `{!relocG Î£} K â„¶1 â„¶2 i1 E (l : loc) v e' v' e t eres A :
+  e = fill K (Xchg (# l) e') â†’
+  IntoVal e' v' â†’
+  nclose specN âŠ† E â†’
+  envs_lookup i1 â„¶1 = Some (false, l â†¦â‚› v)%I â†’
+  envs_simple_replace i1 false (Esnoc Enil i1 (l â†¦â‚› v')) â„¶1 = Some â„¶2 â†’
+  eres = fill K (of_val v) â†’
+  envs_entails â„¶2 (refines E t eres A) â†’
+  envs_entails â„¶1 (refines E t e A).
+Proof.
+  rewrite envs_entails_eq. intros ?????? Hg.
+  subst e eres.
+  rewrite envs_simple_replace_sound //; simpl.
+  rewrite right_id.
+  rewrite (refines_xchg_r E K) //.
+  rewrite Hg.
+  apply bi.wand_elim_l.
+Qed.
+
+Tactic Notation "rel_xchg_l" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l â†¦ _)%I) => l end in
+    iAssumptionCore || fail "rel_xchg_l: cannot find" l "â†¦â‚› ?" in
+  rel_pures_l;
+  first
+    [rel_reshape_cont_l ltac:(fun K e' =>
+       eapply (tac_rel_xchg_l_simpl K);
+       [reflexivity (** e = fill K (#l <- e') *)
+       |iSolveTC    (** e' is a value *)
+       |idtac..])
+    |fail 1 "rel_xchg_l: cannot find 'Xchg'"];
+  (* the remaining goals are from tac_rel_xchg_l (except for the first one, which has already been solved by this point) *)
+  [iSolveTC        (** IntoLaters *)
+  |solve_mapsto ()
+  |pm_reflexivity || fail "rel_xchg_l: this should not happen O-:"
+  |reflexivity
+  |rel_finish  (** new goal *)].
+
+Tactic Notation "rel_xchg_l_atomic" := rel_apply_l refines_xchg_l.
+
+Tactic Notation "rel_xchg_r" :=
+  let solve_mapsto _ :=
+    let l := match goal with |- _ = Some (_, (?l â†¦â‚› _)%I) => l end in
+    iAssumptionCore || fail "rel_xchg_r: cannot find" l "â†¦â‚› ?" in
+  rel_pures_r;
+  first
+    [rel_reshape_cont_r ltac:(fun K e' =>
+       eapply (tac_rel_xchg_r K);
+       [reflexivity|iSolveTC|idtac..])
+    |fail 1 "rel_xchg_r: cannot find 'Xchg'"];
+  (* the remaining goals are from tac_rel_xchg_r (except for the first one, which has already been solved by this point) *)
+  [solve_ndisj || fail "rel_xchg_r: cannot prove 'nclose specN âŠ† ?'"
+  |solve_mapsto ()
+  |pm_reflexivity || fail "rel_xchg_r: this should not happen O-:"
+  |reflexivity
+  |rel_finish  (** new goal *)].
+
+
 (** Alloc *)
 Tactic Notation "rel_alloc_l_atomic" := rel_apply_l refines_alloc_l.
 
diff --git a/theories/logic/rules.v b/theories/logic/rules.v
index 7f9ab5a..4c942ea 100644
--- a/theories/logic/rules.v
+++ b/theories/logic/rules.v
@@ -183,6 +183,20 @@ Section rules.
     iModIntro. iExists _. iFrame. by iApply "Hlog".
   Qed.
 
+  Lemma refines_xchg_r E K l e1 v1 v t A :
+    nclose specN âŠ† E â†’
+    IntoVal e1 v1 â†’
+    l â†¦â‚› v -âˆ—
+    (l â†¦â‚› v1 -âˆ— REL t << fill K (of_val v) @ E : A)
+    -âˆ— REL t << fill K (Xchg #l e1) @ E : A.
+  Proof.
+    rewrite /IntoVal. iIntros (?<-) "Hl Hlog".
+    iApply refines_step_r.
+    iIntros (k) "Hk".
+    admit.
+  Admitted.
+
+
   Lemma refines_cmpxchg_fail_r E K l e1 e2 v1 v2 v t A :
     nclose specN âŠ† E â†’
     IntoVal e1 v1 â†’
@@ -369,6 +383,18 @@ Section rules.
     iApply (wp_store _ _ _ _ v' with "Hl"); auto.
   Qed.
 
+  Lemma refines_xchg_l K E l e v' t A :
+    IntoVal e v' â†’
+    (|={âŠ¤,E}=> âˆƒ v, â–· l â†¦ v âˆ—
+      â–·(l â†¦ v' -âˆ— REL fill K (of_val v) << t @ E : A))
+    -âˆ— REL fill K (Xchg #l e) << t : A.
+  Proof.
+    iIntros (<-) "Hlog".
+    iApply refines_atomic_l; auto.
+    iMod "Hlog" as (v) "[Hl Hlog]". iModIntro.
+    iApply (wp_xchg _ _ _ _ v' with "Hl"); auto.
+  Qed.
+
   Lemma refines_cmpxchg_l K E l e1 e2 v1 v2 t A :
     IntoVal e1 v1 â†’
     IntoVal e2 v2 â†’
diff --git a/theories/logic/spec_rules.v b/theories/logic/spec_rules.v
index 66c8947..6dd9138 100644
--- a/theories/logic/spec_rules.v
+++ b/theories/logic/spec_rules.v
@@ -211,6 +211,37 @@ Section rules.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
 
+  Lemma step_xchg E j K l e (v v' : val) :
+    IntoVal e v â†’
+    nclose specN âŠ† E â†’
+    spec_ctx âˆ— j â¤‡ fill K (Xchg #l e) âˆ— l â†¦â‚› v'
+    ={E}=âˆ— spec_ctx âˆ— j â¤‡ fill K (of_val v') âˆ— l â†¦â‚› v.
+  Proof.
+    iIntros (<-?) "(#Hinv & Hj & Hl)". iFrame "Hinv".
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
+    iDestruct "Hinv" as (Ï) "Hinv".
+    rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
+    iInv specN as (tp Ïƒ) ">[Hown %]" "Hclose".
+    iDestruct (own_valid_2 with "Hown Hj")
+      as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
+    iDestruct (own_valid_2 with "Hown Hl")
+      as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
+    iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
+    { by eapply auth_update, prod_local_update_1, singleton_local_update,
+        (exclusive_local_update _ (Excl (fill K (of_val v')))). }
+    iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
+    { eapply auth_update, prod_local_update_2.
+      apply: singleton_local_update.
+      { by rewrite /to_heap lookup_fmap Hl. }
+      apply: (exclusive_local_update _
+        (1%Qp, to_agree (Some v : leibnizO (option val)))).
+      apply: pair_exclusive_l. done. }
+    iFrame "Hj Hl". iApply "Hclose". iNext.
+    iExists (<[j:=fill K (of_val v')]> tp), (state_upd_heap <[l:=Some v]> Ïƒ).
+    rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
+    eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
+  Qed.
+
   (** CmpXchg & FAA *)
   Lemma step_cmpxchg_fail E j K l q v' e1 v1 e2 v2 :
     IntoVal e1 v1 â†’
diff --git a/theories/tests/proofmode_tests.v b/theories/tests/proofmode_tests.v
index 911cd66..46d66de 100644
--- a/theories/tests/proofmode_tests.v
+++ b/theories/tests/proofmode_tests.v
@@ -91,5 +91,29 @@ Proof.
   rel_values.
 Qed.
 
+
+Lemma test_xchg_1 l1 l2 (v1 v2 : val) (A : lrel Î£) :
+  l1 â†¦ v1 -âˆ—
+  l2 â†¦â‚› v2 -âˆ—
+  (l1 â†¦ #3 -âˆ— l2 â†¦â‚› #3 -âˆ— A v1 v2) -âˆ—
+  REL Xchg #l1 #3 << Xchg #l2 #3 : A.
+Proof.
+  iIntros "Hl1 Hl2 H".
+  rel_xchg_l. rel_xchg_r. rel_values.
+  iModIntro. iApply ("H" with "Hl1 Hl2").
+Qed.
+
+Lemma test_xchg_2 l1 l2 (v1 v2 : val) (A : lrel Î£) :
+  l1 â†¦ v1 -âˆ—
+  l2 â†¦â‚› v2 -âˆ—
+  (l1 â†¦ #3 -âˆ— l2 â†¦â‚› #3 -âˆ— A v1 v2) -âˆ—
+  REL Xchg #l1 #3 << (let: "x" := !#l2 in #l2 <- #3;; "x") : A.
+Proof.
+  iIntros "Hl1 Hl2 H".
+  rel_xchg_l. rel_load_r. rel_pures_r.
+  rel_store_r. rel_pures_r. rel_values.
+  iModIntro. iApply ("H" with "Hl1 Hl2").
+Qed.
+
 End test.
 
diff --git a/theories/typing/fundamental.v b/theories/typing/fundamental.v
index f4c96c7..ca43dc0 100644
--- a/theories/typing/fundamental.v
+++ b/theories/typing/fundamental.v
@@ -264,6 +264,18 @@ Section fundamental.
     - by iApply "IH2".
   Qed.
 
+  Lemma bin_log_related_xchg Î” Î“ e1 e2 e1' e2' Ï„ :
+    ({Î”;Î“} âŠ¨ e1 â‰¤logâ‰¤ e1' : TRef Ï„) -âˆ—
+    ({Î”;Î“} âŠ¨ e2 â‰¤logâ‰¤ e2' : Ï„) -âˆ—
+    {Î”;Î“} âŠ¨ Xchg e1 e2 â‰¤logâ‰¤ Xchg e1' e2' : Ï„.
+  Proof.
+    iIntros "IH1 IH2".
+    intro_clause.
+    iApply (refines_xchg with "[IH1] [IH2]").
+    - by iApply "IH1".
+    - by iApply "IH2".
+  Qed.
+
   Lemma bin_log_related_FAA Î” Î“ e1 e2 e1' e2' :
     ({Î”;Î“} âŠ¨ e1 â‰¤logâ‰¤ e1' : TRef TNat) -âˆ—
     ({Î”;Î“} âŠ¨ e2 â‰¤logâ‰¤ e2' : TNat) -âˆ—
@@ -574,6 +586,7 @@ Section fundamental.
       + iApply bin_log_related_alloc; by iApply fundamental.
       + iApply bin_log_related_load; by iApply fundamental.
       + iApply bin_log_related_store; by iApply fundamental.
+      + iApply bin_log_related_xchg; by iApply fundamental.
       + iApply bin_log_related_FAA; eauto;
           by iApply fundamental.
       + iApply bin_log_related_CmpXchg; eauto;
diff --git a/theories/typing/types.v b/theories/typing/types.v
index 17a8508..b312953 100644
--- a/theories/typing/types.v
+++ b/theories/typing/types.v
@@ -199,6 +199,7 @@ Inductive typed : stringmap type â†’ expr â†’ type â†’ Prop :=
   | TAlloc Î“ e Ï„ : Î“ âŠ¢â‚œ e : Ï„ â†’ Î“ âŠ¢â‚œ Alloc e : ref Ï„
   | TLoad Î“ e Ï„ : Î“ âŠ¢â‚œ e : ref Ï„ â†’ Î“ âŠ¢â‚œ Load e : Ï„
   | TStore Î“ e e' Ï„ : Î“ âŠ¢â‚œ e : ref Ï„ â†’ Î“ âŠ¢â‚œ e' : Ï„ â†’ Î“ âŠ¢â‚œ Store e e' : ()
+  | TXchg Î“ e e' Ï„ : Î“ âŠ¢â‚œ e : ref Ï„ â†’ Î“ âŠ¢â‚œ e' : Ï„ â†’ Î“ âŠ¢â‚œ Xchg e e' : Ï„
   | TFAA Î“ e1 e2 :
      Î“ âŠ¢â‚œ e1 : ref TNat â†’
      Î“ âŠ¢â‚œ e2 : TNat â†’
-- 
GitLab