can we please delete Coq from the universe

_CoqProject

@@ -17,6 +17,7 @@ theories/simulation/global_sim.v
 theories/simulation/fairness_adequacy.v
 theories/simulation/adequacy.v
 theories/simulation/lifting.v
+theories/simulation/log_rel.v
 
 theories/playground/fixpoints.v
 theories/playground/language.v

theories/simplang/lang.v

@@ -1192,10 +1192,6 @@ 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 (Val (LitV LitUnit))).
-
 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.
@@ -1223,16 +1219,6 @@ Proof.
   ].
 Qed.
 
-Lemma subst_map_closed xs e :
-  free_vars e = ∅ →
-  subst_map xs e = e.
-Proof.
-  intros Hclosed.
-  trans (subst_map ∅ e).
-  - apply subst_map_free_vars. rewrite Hclosed. done.
-  - apply subst_map_empty.
-Qed.
-
 Lemma subst_free_vars x v e :
   x ∉ free_vars e →
   subst x v e = e.
@@ -1258,16 +1244,6 @@ Proof.
   - rewrite -subst_subst_map delete_notin // free_vars_subst IH. 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 IH] 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 !IH; set_solver+.
-Qed.
-
-
 (* Proving the mixin *)
 
 Lemma simp_lang_mixin : LanguageMixin of_class to_class empty_ectx ectx_compose fill subst_map free_vars head_step.
@@ -1279,6 +1255,7 @@ Proof.
   - intros p f v ????. split.
     + cbn. inversion 1; subst. eexists _, _. rewrite subst_map_singleton. eauto.
     + intros (x & e & ? & -> & -> & ->). cbn. rewrite subst_map_singleton. by constructor.
+  - eapply subst_map_empty.
   - eapply subst_map_free_vars.
   - done.
   - intros ???. by rewrite -fill_app.

theories/simulation/behavior.v

@@ -24,8 +24,12 @@ Section beh.
     (* safety *)
     (safe p_t (of_call main u) σ_t).
 
-  (** * A more classical definition of 'behavioral refinement', equivalent to the
-      above. *)
+  (** The notion of *contextual* refinement depends on an idea of "contexts" and
+      some form of "well-formedness", so we do not define it in general and
+      instead expect each language to define a suitable one.
+
+  (** * A more classical definition of 'behavioral refinement', equivalent to
+      the above. *)
 
   (** First we define the possible "behaviors" of a program, and which behaviors
       we consider observably related (lifting O to behaviors). *)

theories/simulation/global_sim.v

@@ -4,7 +4,7 @@ From iris.bi Require Import bi.
 From iris.proofmode Require Import tactics.
 From simuliris.logic Require Import fixpoints.
 From simuliris.simulation Require Import relations language.
-From simuliris.simulation Require Export simulation slsls.
+From simuliris.simulation Require Export simulation slsls log_rel.
 From iris.prelude Require Import options.
 Import bi.
 
@@ -20,16 +20,6 @@ Section fix_lang.
     (P_s P_t P: prog Λ)
     (σ_s σ_t σ : state Λ).
 
-  Definition prog_rel P_t P_s : PROP :=
-    (□ ∀ f x_s e_s, ⌜P_s !! f = Some (x_s, e_s)⌝ →
-       ∃ x_t e_t, ⌜P_t !! f = Some (x_t, e_t)⌝ ∗
-         ∀ v_t v_s π, ext_rel π v_t v_s -∗
-           (subst_map {[x_t:=v_t]} e_t) ⪯{π} (subst_map {[x_s:=v_s]} e_s) {{ ext_rel π }})%I.
-  Typeclasses Opaque prog_rel.
-
-  Global Instance prog_rel_persistent P_s P_t : Persistent (prog_rel P_s P_t).
-  Proof. rewrite /prog_rel; apply _. Qed.
-
   Notation expr_rel := (@exprO Λ -d> @exprO Λ -d> PROP).
 
   Global Instance expr_rel_func_ne (F: expr_rel → thread_idO -d> expr_rel) `{Hne: !NonExpansive F}:
@@ -688,7 +678,6 @@ Section fix_lang.
       iApply sim_expr_bind. iDestruct ("Hloc" $! _ _ _ Hdef_s) as (x_f_t' e_f_t') "[% Hectx]".
       replace x_f_t' with x_f_t by naive_solver.
       replace e_f_t' with e_f_t by naive_solver.
-      rewrite /sim_ectx.
       iApply (sim_expr_mono with "[-Hval] [Hval]"); last by iApply "Hectx".
       iIntros (e_t' e_s'). iDestruct 1 as (v_t' v_s' -> ->) "Hval".
       rewrite sim_expr_eq. by iApply "Hcont".
@@ -710,5 +699,3 @@ Section fix_lang.
     iIntros (??) "Hrel". iApply "Hsim". done.
   Qed.
 End fix_lang.
-
-Typeclasses Opaque prog_rel.

theories/simulation/language.v

@@ -20,6 +20,9 @@ Section language_mixin.
   Context (comp_ectx : ectx → ectx → ectx).
   Context (fill : ectx → expr → expr).
 
+  (** Parallel substitution. For defining function calls, "singleton"
+      substitution would be sufficient, but this also lets us define
+      the logical relation. *)
   Context (subst_map : gmap string val → expr → expr).
   Context (free_vars : expr → gset string).
 
@@ -44,9 +47,14 @@ Section language_mixin.
         p !! f = Some (x, e) ∧ e2 = subst_map {[x:=v]} e ∧ σ2 = σ1 ∧ efs = [];
 
     (** Substitution and free variables *)
+    mixin_subst_map_empty e : subst_map ∅ e = e;
+    mixin_subst_map_subst_map xs ys e :
+      subst_map xs (subst_map ys e) = subst_map (ys ∪ xs) e;
     mixin_subst_map_free_vars (xs1 xs2 : gmap string val) (e : expr) :
       (∀ x, x ∈ free_vars e → xs1 !! x = xs2 !! x) →
       subst_map xs1 e = subst_map xs2 e;
+    mixin_free_vars_subst_map xs e :
+      free_vars (subst_map xs e) = free_vars e ∖ (dom _ xs);
 
     (** Evaluation contexts *)
     mixin_fill_empty e : fill empty_ectx e = e;
@@ -168,6 +176,20 @@ Section language.
     ∃ x e, p !! f = Some (x, e) ∧ e2 = subst_map {[x:=v]} e ∧ σ2 = σ1 ∧ efs = nil.
   Proof. apply language_mixin. Qed.
 
+  Lemma subst_map_empty e :
+    subst_map ∅ e = e.
+  Proof. apply language_mixin. Qed.
+  Lemma subst_map_free_vars (xs1 xs2 : gmap string (val Λ)) e :
+    (∀ x, x ∈ free_vars e → xs1 !! x = xs2 !! x) →
+    subst_map xs1 e = subst_map xs2 e.
+  Proof. apply language_mixin. Qed.
+  Lemma subst_map_subst_map xs ys e :
+    subst_map xs (subst_map ys e) = subst_map (ys ∪ xs) e.
+  Proof. apply language_mixin. Qed.
+  Lemma free_vars_subst_map xs e :
+    free_vars (subst_map xs e) = free_vars e ∖ (dom _ xs).
+  Proof. apply language_mixin. Qed.
+
   Lemma fill_empty e : fill empty_ectx e = e.
   Proof. apply language_mixin. Qed.
   Lemma fill_comp K1 K2 e : fill K1 (fill K2 e) = fill (comp_ectx K1 K2) e.
@@ -1005,6 +1027,15 @@ Section language.
     destruct IH as [(-> & ->)|(e''' & σ''' & Hnfs & Hnf)]; eauto 10 using no_forks.
   Qed.
 
+  Lemma subst_map_closed xs e :
+    free_vars e = ∅ →
+    subst_map xs e = e.
+  Proof.
+    intros Hclosed.
+    trans (subst_map ∅ e).
+    - apply subst_map_free_vars. rewrite Hclosed. done.
+    - apply subst_map_empty.
+  Qed.
 
 End language.
 
@@ -1104,4 +1135,5 @@ Section reach_or_stuck.
     - exfalso. apply: Hs. apply: pool_reach_stuck_reach_stuck; [|done]. by apply: fill_reach_stuck.
     - eexists _, _. split; [done|]. apply: pool_safe_no_forks; [done..|]. by apply: fill_no_forks.
   Qed.
+
 End reach_or_stuck.

theories/simulation/log_rel.v

+(** General definition of [prog_rel] on whole programs and [log_rel] on open
+    terms. *)
+
+From stdpp Require Import binders.
+From iris.bi Require Import bi.
+From iris.proofmode Require Import tactics.
+From simuliris.simulation Require Import relations language.
+From simuliris.simulation Require Export simulation slsls.
+From iris.prelude Require Import options.
+Import bi.
+
+Section fix_lang.
+  Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
+  Context {Λ : language}.
+  Context {s : simulirisGS PROP Λ}.
+
+  Set Default Proof Using "Type*".
+
+  Implicit Types
+    (e_s e_t e: expr Λ)
+    (P_s P_t P: prog Λ)
+    (σ_s σ_t σ : state Λ).
+
+  (** Whole-program relation *)
+  Definition prog_rel P_t P_s : PROP :=
+    (□ ∀ f x_s e_s, ⌜P_s !! f = Some (x_s, e_s)⌝ →
+       ∃ x_t e_t, ⌜P_t !! f = Some (x_t, e_t)⌝ ∗
+         ∀ v_t v_s π, ext_rel π v_t v_s -∗
+           (subst_map {[x_t:=v_t]} e_t) ⪯{π} (subst_map {[x_s:=v_s]} e_s) {{ ext_rel π }})%I.
+  Typeclasses Opaque prog_rel.
+
+  Global Instance prog_rel_persistent P_s P_t : Persistent (prog_rel P_s P_t).
+  Proof. rewrite /prog_rel; apply _. Qed.
+
+  
+  (** Relation on "contexts":
+      Well-formed substitutions closing source and target, with [X] denoting the
+      free variables. *)
+  Definition subst_map_rel (X : gset string) (map : gmap string (val Λ * val Λ)) : PROP :=
+    [∗ set] x ∈ X,
+      match map !! x with
+      | Some (v_t, v_s) => val_rel v_t v_s
+      | None => False
+      end.
+
+  Global Instance subst_map_rel_pers X map `{!∀ vt vs, Persistent (val_rel vt vs)} :
+    Persistent (subst_map_rel X map).
+  Proof.
+    rewrite /subst_map_rel. apply big_sepS_persistent=>x.
+    destruct (map !! x) as [[v_t v_s]|]; apply _.
+  Qed.
+
+  Lemma subst_map_rel_lookup {X map} x :
+    x ∈ X →
+    subst_map_rel X map -∗
+    ∃ v_t v_s, ⌜map !! x = Some (v_t, v_s)⌝ ∗ val_rel v_t v_s.
+  Proof.
+    iIntros (Hx) "Hrel".
+    iDestruct (big_sepS_elem_of _ _ x with "Hrel") as "Hrel"; first done.
+    destruct (map !! x) as [[v_t v_s]|]; last done. eauto.
+  Qed.
+
+  Lemma subst_map_rel_weaken X1 X2 map :
+    X2 ⊆ X1 →
+    subst_map_rel X1 map -∗ subst_map_rel X2 map.
+  Proof. iIntros (HX). iApply big_sepS_subseteq. done. Qed.
+
+  Lemma subst_map_rel_singleton X x v_t v_s :
+    X ⊆ {[x]} →
+    val_rel v_t v_s -∗
+    subst_map_rel X {[x:=(v_t, v_s)]}.
+  Proof.
+    iIntros (?) "Hrel".
+    iApply (subst_map_rel_weaken {[x]}); first done.
+    rewrite /subst_map_rel big_sepS_singleton lookup_singleton. done.
+  Qed.
+
+  (* TODO: use [binder_delete], once we can [delete] on [gset]. *)
+  Definition binder_delete_gset (b : binder) (X : gset string) :=
+    match b with BAnon => X | BNamed x => X ∖ {[x]} end.
+
+  Lemma subst_map_rel_insert X x v_t v_s map `{!∀ vt vs, Persistent (val_rel vt vs)} :
+    subst_map_rel (binder_delete_gset x X) map -∗
+    val_rel v_t v_s -∗
+    subst_map_rel X (binder_insert x (v_t, v_s) map).
+  Proof.
+    iIntros "#Hmap #Hval". destruct x as [|x]; first done. simpl.
+    iApply big_sepS_intro. iIntros "!# %x' %Hx'".
+    destruct (decide (x = x')) as [->|Hne].
+    - rewrite lookup_insert. done.
+    - rewrite lookup_insert_ne //.
+      iApply (big_sepS_elem_of with "Hmap"). set_solver.
+  Qed.
+
+  Lemma subst_map_rel_empty map :
+    ⊢ subst_map_rel ∅ map.
+  Proof. iApply big_sepS_empty. done. Qed.
+
+  (** The core "logical relation" of our system:
+      The simulation relation ("expression relation") must hold after applying
+      an arbitrary well-formed closing substitution [map]. *)
+  Definition log_rel e_t e_s : PROP :=
+    □ ∀ π (map : gmap string (val Λ * val Λ)),
+      subst_map_rel (free_vars e_t ∪ free_vars e_s) map -∗
+      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 log_rel_closed_1 e_t e_s π :
+    free_vars e_t ∪ free_vars e_s = ∅ →
+    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 log_rel_closed e_t e_s :
+    free_vars e_t ∪ free_vars e_s = ∅ →
+    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. iSplit.
+    { iIntros "#Hrel !#" (π). iApply log_rel_closed_1; done. }
+    iIntros "#Hsim" (π xs) "!# Hxs".
+    rewrite !subst_map_closed //; set_solver.
+  Qed.
+
+  Lemma log_rel_singleton e_t e_s v_t v_s arg π :
+    free_vars e_t ∪ free_vars e_s ⊆ {[ arg ]} →
+    log_rel e_t e_s -∗
+    val_rel v_t v_s -∗
+    thread_own π -∗ 
+    subst_map {[arg := v_t]} e_t ⪯{π} subst_map {[arg := v_s]} e_s
+      {{ λ v_t v_s, thread_own π ∗ val_rel v_t v_s }}.
+  Proof.
+    iIntros (?) "Hlog Hval Hπ".
+    iDestruct ("Hlog" $! _ {[arg := (v_t, v_s)]} with "[Hval] Hπ") as "Hsim".
+    { by iApply subst_map_rel_singleton. }
+    rewrite !map_fmap_singleton. done.
+  Qed.
+
+  (** Substitute away a single variable in an [log_rel].
+      Use the [log_rel] tactic below to automatically apply this for all free variables. *)
+  Lemma log_rel_subst x e_t e_s `{!∀ vt vs, Persistent (val_rel vt vs)} :
+    x ∈ free_vars e_t ∪ free_vars e_s →
+    (□ ∀ (v_t v_s : val Λ), val_rel v_t v_s -∗
+      log_rel (subst_map {[x:=v_t]} e_t) (subst_map {[x:=v_s]} e_s)) -∗
+    log_rel e_t e_s.
+  Proof.
+    iIntros (Hin) "#Hsim %π %xs !# #Hxs".
+    iDestruct (subst_map_rel_lookup x with "Hxs") as (v_t v_s Hv) "Hrel"; first done.
+    iSpecialize ("Hsim" $! v_t v_s with "Hrel").
+    iSpecialize ("Hsim" $! π (delete x xs) with "[Hxs]").
+    { iApply (subst_map_rel_weaken with "Hxs").
+      rewrite !free_vars_subst_map. set_solver. }
+Set Printing All.
+(* Crazy Delete instance picked right here *)
+
+    rewrite !subst_map_subst_map.
+    rewrite (_ : fst <$> xs = {[x := v_t]} ∪ (fst <$> delete x xs)). ; last first.
+    { trans ((fst <$> {[x := (v_t, v_s)]}) ∪ (fst <$> delete x xs)).
+      - rewrite -map_fmap_union. rewrite -insert_union_singleton_l.
+        rewrite insert_delete. rewrite insert_id //.
+      - rewrite map_fmap_singleton //. }
+    rewrite (_ : snd <$> xs = {[x := v_s]} ∪ (snd <$> delete x xs)); last first.
+    { trans ((snd <$> {[x := (v_t, v_s)]}) ∪ (snd <$> delete x xs)).
+      - rewrite -map_fmap_union. rewrite -insert_union_singleton_l.
+        rewrite insert_delete. rewrite insert_id //.
+      - rewrite map_fmap_singleton //. }
+    done.
+    rewrite insert_id.
+    2:{ rewrite lookup_fmap Hv //. }
+    rewrite insert_id.
+    2:{ rewrite lookup_fmap Hv //. }
+    done.
+  Qed.
+
+End fix_lang.
+
+Typeclasses Opaque prog_rel log_rel.

theories/simulation/simulation.v

@@ -16,10 +16,15 @@ Class simulirisGS (PROP : bi) (Λ : language) := SimulirisGS {
     (∀ σ_s, prim_step P_s e_s σ_s e_s' σ_s []) →
     state_interp P_t σ_t P_s σ_s T -∗
     state_interp P_t σ_t P_s σ_s (<[π:=e_s']>T);
-  (* external function call relation *)
-  ext_rel : thread_id → val Λ → val Λ → PROP;
+  (* value relation *)
+  val_rel : val Λ → val Λ → PROP;
+  (* extra thread ownership that is threaded through *)
+  thread_own : thread_id → PROP;
 }.
 
+Definition ext_rel `{!simulirisGS PROP Λ} (π : thread_id) (v_t v_s : val Λ) : PROP :=
+  thread_own π ∗ val_rel v_t v_s.
+
 Definition progs_are {Λ PROP} `{simulirisGS PROP Λ} (P_t P_s : prog Λ) : PROP :=
   (□ ∀ P_t' P_s' σ_t σ_s T_s, state_interp P_t' σ_t P_s' σ_s T_s → ⌜P_t' = P_t⌝ ∧ ⌜P_s' = P_s⌝)%I.
 #[global]
@@ -65,7 +70,7 @@ Instance expr_equiv {Λ} : Equiv (expr Λ). apply exprO. Defined.
 Definition thread_idO := leibnizO thread_id.
 Instance thread_id_equiv : Equiv thread_id. apply thread_idO. Defined.
 
-(** * SLSLS, Separation Logic Stuttering Local Simulation *)
+(** FXME: get rid of this *)
 Section fix_lang.
   Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
   Context {Λ : language}.
@@ -77,9 +82,6 @@ Section fix_lang.
 
   Definition sim_ectx `{!Sim s} π K_t K_s Φ :=
     (∀ v_t v_s, ext_rel π v_t v_s -∗ sim Φ π (fill K_t (of_val v_t)) (fill K_s (of_val v_s)))%I.
-  Definition sim_expr_ectx `{!SimE s} π K_t K_s Φ :=
-    (∀ v_t v_s, ext_rel π v_t v_s -∗ sim_expr Φ π (fill K_t (of_val v_t)) (fill K_s (of_val v_s)))%I.
 End fix_lang.
 
 Global Arguments sim_ectx : simpl never.
-Global Arguments sim_expr_ectx : simpl never.

theories/simulation/slsls.v

@@ -68,6 +68,7 @@ Qed.
 Notation NonExpansive3 f := (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n) f).
 Notation NonExpansive4 f := (∀ n, Proper (dist n ==> dist n ==> dist n ==> dist n ==> dist n) f).
 
+(** * SLSLS, Separation Logic Stuttering Local Simulation *)
 
 Section fix_lang.
   Context {PROP : bi} `{!BiBUpd PROP, !BiAffine PROP, !BiPureForall PROP}.
@@ -343,10 +344,10 @@ Section fix_lang.
         ⌜e_t = fill K_t (of_call f v_t)⌝ ∗
         ⌜no_forks P_s e_s σ_s (fill K_s' (of_call f v_s)) σ_s'⌝ ∗
         ext_rel π v_t v_s ∗ state_interp P_t σ_t P_s σ_s' (<[π := fill K_s (fill K_s' (of_call f v_s))]> T_s) ∗
-        sim_expr_ectx π K_t K_s' Φ)
+        (∀ v_t v_s, ext_rel π v_t v_s -∗ sim_expr Φ π (fill K_t (of_val v_t)) (fill K_s' (of_val v_s))))
     )%I.
   Proof.
-    rewrite /sim_expr_ectx sim_expr_fixpoint /sim_expr_inner //.
+    rewrite sim_expr_fixpoint /sim_expr_inner //.
   Qed.
 
   (* FIXME: should use [pointwise_relation] *)
@@ -923,14 +924,6 @@ Section fix_lang.
     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) *)