From f0560c6109bda6bed273b065a041a38821243ed0 Mon Sep 17 00:00:00 2001
From: Dan Frumin <dfrumin@cs.ru.nl>
Date: Wed, 6 Feb 2019 11:33:55 +0100
Subject: [PATCH] Soundness proof for the logical relation for F_mu_ref_conc

---
 _CoqProject                             |  1 +
 theories/typing/contextual_refinement.v |  2 +
 theories/typing/soundness.v             | 67 +++++++++++++++++++++++++
 3 files changed, 70 insertions(+)
 create mode 100644 theories/typing/soundness.v

diff --git a/_CoqProject b/_CoqProject
index 8f5d9ff..1edebe4 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -15,6 +15,7 @@ theories/typing/types.v
 theories/typing/interp.v
 theories/typing/fundamental.v
 theories/typing/contextual_refinement.v
+theories/typing/soundness.v
 
 theories/tests/tp_tests.v
 theories/tests/proofmode_tests.v
diff --git a/theories/typing/contextual_refinement.v b/theories/typing/contextual_refinement.v
index 29b0195..a43aa9f 100644
--- a/theories/typing/contextual_refinement.v
+++ b/theories/typing/contextual_refinement.v
@@ -1,3 +1,5 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Notion of contextual refinement & proof that it is a precongruence wrt the logical relation *)
 From iris.heap_lang Require Export lang.
 From iris.proofmode Require Import tactics.
 From reloc.typing Require Export types interp fundamental.
diff --git a/theories/typing/soundness.v b/theories/typing/soundness.v
new file mode 100644
index 0000000..8a42f4b
--- /dev/null
+++ b/theories/typing/soundness.v
@@ -0,0 +1,67 @@
+(* ReLoC -- Relational logic for fine-grained concurrency *)
+(** Logical relation is sound w.r.t. the contextual refinement. *)
+From iris.proofmode Require Import tactics.
+From reloc.logic Require Export adequacy.
+From reloc.typing Require Export contextual_refinement.
+
+Lemma logrel_adequate Σ `{relocPreG Σ}
+   e e' τ (σ : state) :
+  (∀ `{relocG Σ} Δ, {⊤;Δ;∅} ⊨ e ≤log≤ e' : τ) →
+  adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h)
+    ∧ (ObsType τ → v = v')).
+Proof.
+  intros Hlog.
+  set (A := λ (HΣ : relocG Σ), interp τ []).
+  eapply (refines_adequate Σ A); last first.
+  - intros HΣ. specialize (Hlog HΣ []).
+    revert Hlog. unfold A, bin_log_related.
+    by rewrite fmap_empty.
+  - intros HΣ v v'. unfold A. iIntros "Hvv".
+    unfold ObsType. cbn.
+    iIntros (HÏ„). by iApply (eq_type_sound with "Hvv").
+Qed.
+
+Theorem logrel_typesafety Σ `{relocPreG Σ} e e' τ thp σ σ' :
+  (∀ `{relocG Σ} Δ, {⊤;Δ;∅} ⊨ e ≤log≤ e : τ) →
+  rtc erased_step ([e], σ) (thp, σ') → e' ∈ thp →
+  is_Some (to_val e') ∨ reducible e' σ'.
+Proof.
+  intros Hlog ??.
+  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e], σ) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))); first (intros [_ ?]; eauto).
+  eapply logrel_adequate; eauto.
+Qed.
+
+Theorem F_mu_ref_conc_typesfety e e' τ σ thp σ' :
+  ∅ ⊢ₜ e : τ →
+  rtc erased_step ([e], σ) (thp, σ') → e' ∈ thp →
+  is_Some (to_val e') ∨ reducible e' σ'.
+Proof.
+  intros.
+  eapply (logrel_typesafety relocΣ); eauto.
+  intros. by apply binary_fundamental.
+Qed.
+
+Lemma logrel_simul Σ `{relocPreG Σ}
+  e e' τ v thp hp σ :
+  (∀ `{relocG Σ} Δ, {⊤;Δ;∅} ⊨ e ≤log≤ e' : τ) →
+  rtc erased_step ([e], σ) (of_val v :: thp, hp) →
+  (∃ thp' hp' v', rtc erased_step ([e'], σ) (of_val v' :: thp', hp') ∧ (ObsType τ → v = v')).
+Proof.
+  intros Hlog Hsteps.
+  cut (adequate NotStuck e σ (λ v _, ∃ thp' h v', rtc erased_step ([e'], σ) (of_val v' :: thp', h) ∧ (ObsType τ → v = v'))).
+  { destruct 1; naive_solver. }
+  eapply logrel_adequate; eauto.
+Qed.
+
+Lemma logrel_ctxequiv Σ `{relocPreG Σ} Γ e e' τ :
+  (∀ `{relocG Σ} Δ, {⊤;Δ;Γ} ⊨ e ≤log≤ e' : τ) →
+  Γ ⊨ e ≤ctx≤ e' : τ.
+Proof.
+  intros Hlog K thp σ₀ σ₁ v τ' ? Htyped Hstep.
+  cut (∃ thp' hp' v', rtc erased_step ([fill_ctx K e'], σ₀) (of_val v' :: thp', hp') ∧ (ObsType τ'  → v = v')).
+  { naive_solver. }
+  eapply (logrel_simul Σ); last by apply Hstep.
+  iIntros (? ?).
+  iApply (bin_log_related_under_typed_ctx with "[]"); eauto.
+  iAlways. iIntros (?). iApply Hlog.
+Qed.
-- 
GitLab