From 42e45f5a54bdfa81c067f7d9394324326a025fc0 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 10 Jun 2021 17:58:41 +0200
Subject: [PATCH] proof of log_rel_adequacy (not quite closed yet)

---
 theories/logic/satisfiable.v            |  7 +++++
 theories/simplang/behavior.v            |  2 +-
 theories/simplang/gen_adequacy.v        |  4 +--
 theories/simplang/gen_log_rel.v         | 37 +++++++++++++++----------
 theories/simplang/parallel_subst.v      | 15 +++++++++-
 theories/simplang/simple_inv/adequacy.v | 31 ++++++++++++++++++---
 theories/simplang/simple_inv/refl.v     | 34 +++++++++++++++++++++++
 theories/simulation/slsls.v             | 17 ++++++++++++
 8 files changed, 124 insertions(+), 23 deletions(-)

diff --git a/theories/logic/satisfiable.v b/theories/logic/satisfiable.v
index 777674f7..7214f68c 100644
--- a/theories/logic/satisfiable.v
+++ b/theories/logic/satisfiable.v
@@ -115,6 +115,13 @@ Proof.
   - intros X Φ [x [Hv [a HΦ]]]; eauto.
 Qed.
 
+Lemma isat_intro {M} (P : uPred M) : (⊢ P) → isat P.
+Proof.
+  intros HP. exists ε. split; first by apply ucmra_unit_validN.
+  apply HP; first by apply ucmra_unit_validN.
+  uPred.unseal. done.
+Qed.
+
 Lemma isat_later_false {M}: isat ((▷ False)%I: uPred M) → False.
 Proof.
   unfold isat; uPred.unseal; intros [x [_ HF]].
diff --git a/theories/simplang/behavior.v b/theories/simplang/behavior.v
index d3d25d3f..0d13148d 100644
--- a/theories/simplang/behavior.v
+++ b/theories/simplang/behavior.v
@@ -37,8 +37,8 @@ Section ctx_rel.
       <hole> will be the function argument. *)
   Definition gen_ctx_rel (e_t e_s : expr) :=
     ∀ (C : ctx) (fname x : string) (p : prog),
+      map_Forall (λ _ K, gen_ectx_wf expr_head_wf K ∧ free_vars_ectx K = ∅) p →
       gen_ctx_wf expr_head_wf C →
-      map_Forall (const (gen_ectx_wf expr_head_wf)) p →
       free_vars (fill_ctx C e_t) ∪ free_vars (fill_ctx C e_s) ⊆ {[x]} →
       beh_rel (<[fname := (λ: x, fill_ctx C e_t)%E]> p) (<[fname := (λ: x, fill_ctx C e_s)%E]> p).
 
diff --git a/theories/simplang/gen_adequacy.v b/theories/simplang/gen_adequacy.v
index 1cb52d78..a189cd08 100644
--- a/theories/simplang/gen_adequacy.v
+++ b/theories/simplang/gen_adequacy.v
@@ -14,8 +14,8 @@ Section adequacy.
     ) →
     beh_rel p_t p_s.
   Proof.
-    intros Hsat. eapply (slsls_adequacy (sat:=isat)).
-    intros σ_t σ_s. eapply sat_bupd, sat_mono, Hsat. clear Hsat.
+    intros Hrel. eapply (slsls_adequacy (sat:=isat)).
+    intros σ_t σ_s. eapply sat_bupd, sat_mono, Hrel. clear Hrel.
     iIntros "Hprog_rel".
     iMod sheap_init as (HsheapGS) "Hinit".
     iMod ("Hprog_rel" $! HsheapGS) as (HsheapInv loc_rel) "(Hinv & Hunit & Hobs & Hprog_rel)".
diff --git a/theories/simplang/gen_log_rel.v b/theories/simplang/gen_log_rel.v
index 04df2322..9d34cd4d 100644
--- a/theories/simplang/gen_log_rel.v
+++ b/theories/simplang/gen_log_rel.v
@@ -71,18 +71,25 @@ Section open_rel.
       thread_own π -∗
       subst_map (fst <$> map) e_t ⪯{π} subst_map (snd <$> map) e_s {{ λ v_t v_s, thread_own π ∗ val_rel v_t v_s }}.
 
+  Lemma gen_log_rel_closed_1 e_t e_s π :
+    free_vars e_t ∪ free_vars e_s = ∅ →
+    gen_log_rel e_t e_s ⊢
+      thread_own π -∗ e_t ⪯{π} e_s {{ λ v_t v_s, thread_own π ∗ val_rel v_t v_s }}.
+  Proof.
+    iIntros (Hclosed) "#Hrel". iSpecialize ("Hrel" $! π ∅).
+    rewrite ->!fmap_empty, ->!subst_map_empty.
+    rewrite Hclosed. iApply "Hrel". by iApply subst_map_rel_empty.
+  Qed.
+
   Lemma gen_log_rel_closed e_t e_s :
-    free_vars e_t = ∅ →
-    free_vars e_s = ∅ →
-    gen_log_rel e_t e_s ⊣⊢ (□ ∀ π, thread_own π -∗ e_t ⪯{π} e_s {{ λ v_t v_s, thread_own π ∗ val_rel v_t v_s }}).
+    free_vars e_t ∪ free_vars e_s = ∅ →
+    gen_log_rel e_t e_s ⊣⊢
+      (□ ∀ π, thread_own π -∗ e_t ⪯{π} e_s {{ λ v_t v_s, thread_own π ∗ val_rel v_t v_s }}).
   Proof.
-    intros Hclosed_t Hclosed_s. iSplit.
-    - iIntros "#Hrel !#" (π). iSpecialize ("Hrel" $! π ∅).
-      rewrite ->!fmap_empty, ->!subst_map_empty.
-      rewrite Hclosed_t Hclosed_s [∅ ∪ _]left_id_L.
-      iApply "Hrel". by iApply subst_map_rel_empty.
-    - iIntros "#Hsim" (π xs) "!# Hxs".
-      rewrite !subst_map_closed //.
+    intros Hclosed. iSplit.
+    { iIntros "#Hrel !#" (π). iApply gen_log_rel_closed_1; done. }
+    iIntros "#Hsim" (π xs) "!# Hxs".
+    rewrite !subst_map_closed //; set_solver.
   Qed.
 
   (** Substitute away a single variable in an [gen_log_rel].
@@ -166,7 +173,7 @@ Section log_rel_structural.
      ([∗list] e_t';e_s' ∈ head_t.2; head_s.2, log_rel e_t' e_s') -∗
      log_rel e_t e_s).
 
-  Theorem log_rel_structural_refl e :
+  Theorem gen_log_rel_refl e :
     log_rel_structural →
     gen_expr_wf expr_head_wf e →
     ⊢ log_rel e e.
@@ -179,7 +186,7 @@ Section log_rel_structural.
     all: naive_solver.
   Qed.
 
-  Theorem log_rel_ectx K e_t e_s :
+  Theorem gen_log_rel_ectx K e_t e_s :
     log_rel_structural →
     gen_ectx_wf expr_head_wf K →
     log_rel e_t e_s -∗
@@ -193,11 +200,11 @@ Section log_rel_structural.
     destruct Ki; simpl; iApply He => //=; iFrame "IH".
     all: move: Hiwf; rewrite /= ?Forall_cons ?Forall_nil => Hiwf.
     all: repeat iSplit; try done.
-    all: iApply log_rel_structural_refl; [done|].
+    all: iApply gen_log_rel_refl; [done|].
     all: naive_solver.
   Qed.
 
-  Theorem log_rel_ctx C e_t e_s :
+  Theorem gen_log_rel_ctx C e_t e_s :
     log_rel_structural →
     gen_ctx_wf expr_head_wf C →
     log_rel e_t e_s -∗
@@ -211,7 +218,7 @@ Section log_rel_structural.
     destruct Ci; simpl; iApply He => //=; iFrame "IH".
     all: move: Hiwf; rewrite /= ?Forall_cons ?Forall_nil => Hiwf.
     all: repeat iSplit; try done.
-    all: iApply log_rel_structural_refl; [done|].
+    all: iApply gen_log_rel_refl; [done|].
     all: naive_solver.
   Qed.
 End log_rel_structural.
diff --git a/theories/simplang/parallel_subst.v b/theories/simplang/parallel_subst.v
index 68f950ae..5fcc6d18 100644
--- a/theories/simplang/parallel_subst.v
+++ b/theories/simplang/parallel_subst.v
@@ -1,5 +1,5 @@
 From stdpp Require Export gmap.
-From simuliris.simplang Require Import lang.
+From simuliris.simplang Require Import lang notation.
 
 (** * Parallel substitution for SimpLang *)
 (** Definitions and proofs mostly yoinked from https://gitlab.mpi-sws.org/FP/stacked-borrows/-/blob/master/theories/lang/subst_map.v *)
@@ -118,6 +118,10 @@ Fixpoint free_vars (e : expr) : gset string :=
      free_vars e0 ∪ free_vars e1 ∪ free_vars e2
   end.
 
+(* Just fill with any value, it does not make a difference. *)
+Definition free_vars_ectx (K : ectx) : gset string :=
+  free_vars (fill K #()).
+
 Local Lemma binder_delete_eq x y (xs1 xs2 : gmap string val) :
   (if y is BNamed s then s ≠ x → xs1 !! x = xs2 !! x else xs1 !! x = xs2 !! x) →
   binder_delete y xs1 !! x = binder_delete y xs2 !! x.
@@ -171,3 +175,12 @@ Lemma free_vars_subst x v e :
 Proof.
   induction e=>/=; repeat case_decide; set_solver.
 Qed.
+
+Lemma free_vars_fill K e :
+  free_vars (fill K e) = free_vars_ectx K ∪ free_vars e.
+Proof.
+  revert e. induction K as [|Ki K] using rev_ind; intros e; simpl.
+  { simpl. rewrite /free_vars_ectx /= left_id_L. done. }
+  rewrite /free_vars_ectx !fill_app /=. destruct Ki; simpl.
+  all: rewrite !IHK; set_solver+.
+Qed.
diff --git a/theories/simplang/simple_inv/adequacy.v b/theories/simplang/simple_inv/adequacy.v
index 0fb451f2..73cda553 100644
--- a/theories/simplang/simple_inv/adequacy.v
+++ b/theories/simplang/simple_inv/adequacy.v
@@ -6,7 +6,7 @@ From iris.base_logic.lib Require Import gset_bij.
 From simuliris.logic Require Import satisfiable.
 From simuliris.simulation Require Import slsls global_sim.
 From simuliris.simplang Require Import proofmode tactics.
-From simuliris.simplang Require Import gen_adequacy behavior wf parallel_subst.
+From simuliris.simplang Require Import gen_adequacy behavior wf parallel_subst gen_refl.
 From simuliris.simplang.simple_inv Require Import inv refl.
 
 (** Instantiate our notion of contextual refinement. *)
@@ -23,7 +23,7 @@ Global Instance subG_sbijΣ Σ :
   subG simpleΣ Σ → simpleGpreS Σ.
 Proof. solve_inG. Qed.
 
-Lemma prog_rel_adequacy `{!simpleGpreS Σ} p_t p_s :
+Lemma prog_rel_adequacy `{!simpleGpreS Σ} (p_t p_s : prog) :
   isat (∀ `(simpleGS Σ), prog_rel p_t p_s) →
   beh_rel p_t p_s.
 Proof.
@@ -45,5 +45,28 @@ Theorem log_rel_adequacy `{!simpleGpreS Σ} e_t e_s :
   isat (∀ `(simpleGS Σ), log_rel e_t e_s) →
   ctx_rel e_t e_s.
 Proof.
-  (* TODO *)
-Abort.
+  intros Hrel C fname x p Hpwf HCwf Hvars.
+  apply prog_rel_adequacy. eapply sat_mono, Hrel. clear Hrel.
+  iIntros "#Hrel" (?) "!# %f %K_s %π".
+  iSpecialize ("Hrel" $! _).
+  destruct (decide (f = fname)) as [->|Hne].
+  - (* FIXME: wtf, why does it need a type annotation here?!? *)
+    rewrite !(lookup_insert (M:=gmap _)).
+    iIntros ([= <-]). iExists _. iSplitR; first done.
+    (* TODO Factor this into a general lemma? *)
+    iIntros (v_t v_s) "#Hval /=".
+    iApply log_rel_closed_1.
+    { simpl. set_solver. }
+    iApply log_rel_let.
+    { iApply log_rel_val. done. }
+    iApply log_rel_ctx; done.
+  - rewrite !(lookup_insert_ne (M:=gmap _)) //.
+    iIntros (Hf). rename K_s into K. iExists K. iSplit; first done.
+    specialize (Hpwf _ _ Hf). destruct Hpwf as [HKwf HKclosed].
+    (* TODO Factor this into a lemma? *)
+    iIntros (v_t v_s) "#Hval /=".
+    iApply log_rel_closed_1.
+    { rewrite !free_vars_fill HKclosed. set_solver+. }
+    iApply log_rel_ectx; first done.
+    iApply log_rel_val; done.
+Qed.
diff --git a/theories/simplang/simple_inv/refl.v b/theories/simplang/simple_inv/refl.v
index 46fb280d..90e4b01e 100644
--- a/theories/simplang/simple_inv/refl.v
+++ b/theories/simplang/simple_inv/refl.v
@@ -13,6 +13,10 @@ Definition expr_head_wf (e : expr_head) : Prop :=
   | _ => True
   end.
 
+Notation expr_wf := (gen_expr_wf expr_head_wf).
+Notation ectx_wf := (gen_ectx_wf expr_head_wf).
+Notation ctx_wf := (gen_ctx_wf expr_head_wf).
+
 Section refl.
   Context `{!simpleGS Σ}.
 
@@ -55,4 +59,34 @@ Section refl.
       iIntros (???????) "Hl Hv Hcont". iApply (sim_bij_store with "Hl Hv"). by iApply "Hcont".
   Qed.
 
+  Corollary log_rel_refl e :
+    expr_wf e →
+    ⊢ log_rel e e.
+  Proof.
+    intros ?. iApply gen_log_rel_refl; first by apply simple_log_rel_structural. done.
+  Qed.
+
+  Corollary log_rel_ctx C e_t e_s :
+    ctx_wf C →
+    log_rel e_t e_s -∗ log_rel (fill_ctx C e_t) (fill_ctx C e_s).
+  Proof.
+    intros ?. iApply gen_log_rel_ctx; first by apply simple_log_rel_structural. done.
+  Qed.
+
+  Corollary log_rel_ectx K e_t e_s :
+    ectx_wf K →
+    log_rel e_t e_s -∗ log_rel (fill K e_t) (fill K e_s).
+  Proof.
+    intros ?. iApply gen_log_rel_ectx; first by apply simple_log_rel_structural. done.
+  Qed.
+
+  Lemma log_rel_closed_1 e_t e_s π :
+    free_vars e_t ∪ free_vars e_s = ∅ →
+    log_rel e_t e_s ⊢ e_t ⪯{π} e_s {{ λ v_t v_s, val_rel v_t v_s }}.
+  Proof.
+    iIntros (?) "#Hrel".
+    iApply sim_mono; last iApply (gen_log_rel_closed_1 with "Hrel"); [|done..].
+    iIntros (v_t v_s) "[_ $]".
+  Qed.
+
 End refl.
diff --git a/theories/simulation/slsls.v b/theories/simulation/slsls.v
index 3a12f49c..9601275d 100644
--- a/theories/simulation/slsls.v
+++ b/theories/simulation/slsls.v
@@ -891,6 +891,23 @@ Section fix_lang.
       by iPureIntro.
   Qed.
 
+  (** Simulations on evaluation contexts *)
+  Lemma sim_ectx_mono Φ Φ' π :
+    (∀ v_t v_s, Φ v_t v_s -∗ Φ' v_t v_s) -∗
+    ∀ E_s E_t, sim_ectx π E_t E_s Φ -∗ sim_ectx π E_t E_s Φ'.
+  Proof.
+    iIntros "Hmon" (E_s E_t) "HE %v_t %v_s Hv".
+    iApply (sim_mono with "Hmon"). iApply "HE". done.
+  Qed.
+
+  Lemma sim_expr_ectx_mono Φ Φ' π :
+    (∀ v_t v_s, Φ v_t v_s -∗ Φ' v_t v_s) -∗
+    ∀ E_s E_t, sim_expr_ectx π E_t E_s Φ -∗ sim_expr_ectx π E_t E_s Φ'.
+  Proof.
+    iIntros "Hmon" (E_s E_t) "HE %v_t %v_s Hv".
+    iApply (sim_expr_mono with "Hmon"). iApply "HE". done.
+  Qed.
+
   (** ** source_red judgment *)
   (** source_red allows to focus the reasoning on the source value
     (while being able to switch back and forth to the full simulation at any point) *)
-- 
GitLab