From 20f5dc7dbaf2a748777e9dad9faeb0a4c6640b9f Mon Sep 17 00:00:00 2001
From: Ike Mulder <ikemulder@hotmail.com>
Date: Fri, 6 Jan 2023 16:39:27 +0100
Subject: [PATCH] Add correspondence to figure 4 file, improve paper_example
 correspondence

---
 _CoqProject                                   |  1 -
 .../diaframe_reloc/correspondence_figure_4.v  | 54 ++++++++++
 .../diaframe_reloc/examples/paper_example.v   | 98 ++++++++-----------
 3 files changed, 93 insertions(+), 60 deletions(-)
 create mode 100644 supplements/diaframe_reloc/correspondence_figure_4.v

diff --git a/_CoqProject b/_CoqProject
index 585f1ff0..f423436f 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,7 +3,6 @@
 # supplements
 -Q supplements/diaframe_heap_lang_examples diaframe.heap_lang.examples
 -Q supplements/diaframe_reloc diaframe.reloc
--Q supplements/diaframe_actris diaframe.actris
 # tutorial
 -Q tutorial diaframe.tutorial
 
diff --git a/supplements/diaframe_reloc/correspondence_figure_4.v b/supplements/diaframe_reloc/correspondence_figure_4.v
new file mode 100644
index 00000000..c55a31cd
--- /dev/null
+++ b/supplements/diaframe_reloc/correspondence_figure_4.v
@@ -0,0 +1,54 @@
+From diaframe.reloc Require Import proof_automation.
+
+
+Section correspondence.
+  Context `{!relocG Σ}.
+
+  Lemma val_Z E (z1 z2 : Z) :
+    (|={E,⊤}=> ⌜z1 = z2⌝) ⊢ 
+    REL #z1 << #z2 @ E : lrel_int.
+  Proof. do 3 iStepS. by iMod "H1" as %->. Qed.
+
+  Lemma val_fun E (v1 v2 : val) A :
+    (|={E,⊤}=> □ (REL v1 #() << v2 #() : A)) ⊢ 
+    REL v1 << v2 @ E : () → A.
+  Proof. do 2 iStepS. iIntros "!>". iMod "H1" as "#H1". iStepsS. Qed.
+
+  Lemma reloc_apply E H (e1 e2 : expr) A B K1 K2 :
+    (□ (H -∗ REL e1 << e2 : A) -∗ |={E}=> H ∗ |={E, ⊤}=> ∀ v1 v2, A v1 v2 -∗ REL (fill K1 $ of_val v1) << (fill K2 $ of_val v2) : B)
+        ⊢ 
+    (□ (H -∗ REL e1 << e2 : A)) -∗ REL (fill K1 e1) << (fill K2 e2) @ E : B.
+  Proof.
+    iStepsS. iSplitL "". iStepsS.
+    solveSteps. iIntros "!>". by iMod "H1".
+  Qed.
+
+  Lemma exec_l X L U f (e1 e2 : expr) K (A : lrel Σ) (E : coPset) :
+    (∀ x : X, {{{ L x }}} e1 @ E {{{ RET (f x); U x }}}) →
+    Atomic WeaklyAtomic e1 →
+    (|={⊤, E}=> ∃ x, L x ∗ ▷ (∀ v, ⌜v = f x⌝ ∗ U x -∗ REL (fill K $ of_val v) << e2 @ E : A)) ⊢
+    REL (fill K e1) << e2 : A.
+  Proof.
+    iStepsS.
+    rewrite refines_eq /refines_def /=.
+    iIntros (j) "Hj".
+    iApply wp_bind.
+    iIntros "!>". iMod "H1" as (?) "[HL HPost]".
+    iApply (x with "HL").
+    do 2 iStepS. iApply ("H3" with "[H4]"); iStepsS.
+  Qed.
+
+  Lemma exec_r X L U f (e1 e2 : expr) K (A : lrel Σ) (E : coPset) :
+    (∀ (x : X) j K', spec_ctx ∗ L x ∗ j ⤇ fill K' e2 ={E}=∗ spec_ctx ∗ U x ∗ j ⤇ (fill K' $ of_val $ f x)) →
+    (|={E}=> ∃ x, L x ∗ (∀ v, ⌜v = f x⌝ ∗ U x -∗ REL e1 << (fill K $ of_val v) @ E : A)) ⊢
+    REL e1 << fill K e2 @ E : A.
+  Proof.
+    iStepsS. iMod "H1". iReIntro "H1".
+    rewrite refines_eq /refines_def /=.
+    do 2 iStepS.
+    iMod (x with "[H3 H1 H4]") as "HR".
+    { iStepsS. rewrite -fill_app. iStepsS. }
+    iReIntro "HR". iApply ("H2" with "[H5]"); first iStepsS.
+    iStepsS. rewrite fill_app. iStepsS.
+  Qed.
+End correspondence.
\ No newline at end of file
diff --git a/supplements/diaframe_reloc/examples/paper_example.v b/supplements/diaframe_reloc/examples/paper_example.v
index c38492ad..66b7f931 100644
--- a/supplements/diaframe_reloc/examples/paper_example.v
+++ b/supplements/diaframe_reloc/examples/paper_example.v
@@ -1,28 +1,9 @@
+From iris.program_logic Require Import atomic.
 From diaframe.reloc Require Import proof_automation symb_exec_logatom backtracking reloc_auto_lob.
 From diaframe.heap_lang Require Import atomic_specs wp_auto_lob.
 From reloc.lib Require Import lock.
 
-From diaframe.lib Require Import own_hints.
-From iris.algebra Require Import auth excl numbers.
-
-
-Definition inc : val := 
-  rec: "f" "l" :=
-    let: "n" := ! "l" in
-    if: CAS "l" "n" ("n" + #1) then
-      "n"
-    else
-      "f" "l".
-
-Section inc_spec.
-Context `{!heapGS Σ}.
-
-Instance inc_spec (l : loc) :
-  SPEC (z : Z), << l ↦ #z >> inc #l << RET #z; l ↦ #(z + 1) >>.
-Proof. iSmash. Qed.
-
-End inc_spec.
-
+(** Example from Fig. 2 in the paper. *)
 Definition fg_incrementer : val :=
   λ: <>, 
     let: "l" := ref #1 in
@@ -54,11 +35,11 @@ Proof.
   iAssert (|={⊤}=> inv (nroot.@"incr") 
       (∃ (n : nat), x ↦ #n ∗ x0 ↦ₛ #n ∗ is_locked_r x1 false))%I 
       with "[-]" as ">#Hinv"; first iStepsS.
-  iSmash.
+  iSmash. (* try replacing [iSmash] with [iStepsS. iApply restore_mask. iStepsS.] *)
 Qed.
 End refinement.
 
-(* above establishes logical refinment, contextual refinement follows: *)
+(* above establishes logical refinement, contextual refinement follows: *)
 Lemma fg_cg_incrementer_ctx_refinement :
   ∅ ⊨ fg_incrementer ≤ctx≤ cg_incrementer : () → () → TNat.
 Proof.
@@ -68,46 +49,45 @@ Proof.
   iApply fg_cg_incrementer_refinement.
 Qed.
 
+(** ⊨ is notation for [ctx_refines]. We display its definition: *)
+Print ctx_refines.
+(** Note that this does not mention anything Diaframe/Iris specific! *)
 
-From iris.program_logic Require Import atomic.
-From iris.heap_lang Require Import proofmode.
+(** Let us see the used axioms of this statement *)
+Print Assumptions fg_cg_incrementer_ctx_refinement.
+(** This shows two used axioms:
+  - [refines_xchg_r], an Admitted lemma in the ReLoC source code. 
+        Issue reported here https://gitlab.mpi-sws.org/iris/reloc/-/issues/11
+        Proposed fix available here https://gitlab.mpi-sws.org/iris/reloc/-/merge_requests/6/diffs
+  - Functional Extensionality, which is used throughout the Autosubst library, which is employed by ReLoC. *)
 
-Definition incr_stateUR := authUR $ optionUR $ exclR natO.
-Class incrStateG Σ := IncrStateG {
-  incrState_inG :> inG Σ incr_stateUR
-}.
-Definition incr_stateΣ := #[ GFunctor incr_stateUR].
 
-Global Instance subG_incrStateΣ {Σ} : subG incr_stateΣ Σ → incrStateG Σ.
-Proof. solve_inG. Qed.
+(** Example from Fig. 5 in the paper. *)
+Definition inc : val := 
+  rec: "f" "l" :=
+    let: "n" := ! "l" in
+    if: CAS "l" "n" ("n" + #1) then
+      "n"
+    else
+      "f" "l".
+
+Section inc_spec.
+Context `{!heapGS Σ}.
 
-Section logatom_spec_incrementer.
-Context `{!heapGS Σ, !incrStateG Σ}.
+Instance inc_spec (l : loc) :
+  SPEC (z : Z), << l ↦ #z >> inc #l << RET #z; l ↦ #(z + 1) >>.
+Proof. iSmash. Qed.
 
-Let Nincr := nroot.@"fg_incr".
+(** Above uses Diaframe's SPEC notation of logical atomicity.
+  This does not trivially unfold to the Iris's logical atomicity. 
+  We thus use it prove a logically atomic triple as defined by Iris. *)
 
-Instance fg_incrementer_spec :
-  SPEC {{ True }} fg_incrementer #() {{ (v : val) γ, RET v;
-    own γ (● Excl' 1) ∗ 
-  (*  □ <<< ∀∀ n : nat, own γ (● Excl' n) >>>
-          v #() @ ↑Nincr
-        <<< own γ (● Excl' (S n)), RET #n >>>  
-    atomic_wp notation is broken, cf https://gitlab.mpi-sws.org/iris/iris/-/issues/473 *)
-    □ atomic_wp (TA := [tele_pair nat]) (TB := [tele]) (v #())%E (↑Nincr)
-      (tele_app $ (λ n, own γ (● Excl' n)))
-      (tele_app $ (λ n, tele_app (TT := TeleO) (own γ (● Excl' (S n)))))
-      (tele_app $ (λ n, tele_app (TT := TeleO) (#n)))
-    }}.
-Proof.
-  iStepsS.
-  iAssert (|={⊤}=> inv Nincr (∃ (n : nat), x ↦ #n ∗ own x0 (◯ Excl' n)))%I with "[-]" as ">#Hinv".
-  { iStepsS. }
-  iStepsS.
-  iMod "H3". iReIntro "H3". iStepS.
-  iAssert (|={∅, ⊤ ∖ ↑Nincr}=> emp -∗ own x5 (◯ Excl' (S x2)) ∗ x4 #x2)%I with "[-]" as ">H5".
-  { iPoseProof (diaframe_close_right with "H6") as "H6". iStepsS. }
-  replace (Z.to_nat (x2 + 1)) with (S x2) by lia.
-  iStepsS.
-Qed.
-End logatom_spec_incrementer.
+Lemma inc_spec_iris (l : loc) :
+  ⊢ atomic_wp (TB := [tele]) (inc #l)%E ∅ 
+    (λᵗ (z : Z), l ↦ #z)%I
+    (λᵗ z, tele_app (TT := [tele]) (l ↦ #(z + 1))%I)
+    (λᵗ z, tele_app (TT := [tele]) #z).
+  (* Parsing notation is broken, but it prints fine. *)
+Proof. iSmash. Qed.
+End inc_spec.
 
-- 
GitLab