Formulate a more intuitive definition of contextual refinement

F_mu_ref_conc/context_refinement.v

@@ -188,10 +188,10 @@ Proof.
 Qed.
 
 Definition ctx_refines (Γ : stringmap type)
-    (e e' : expr) (τ : type) := ∀ K thp σ v,
+    (e e' : expr) (τ : type) : Prop := ∀ K thp σ v,
   typed_ctx K Γ τ ∅ TUnit →
   rtc step ([fill_ctx K e], ∅) (of_val v :: thp, σ) →
-  ∃ thp' σ' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', σ').
+  ∃ thp' σ', rtc step ([fill_ctx K e'], ∅) (of_val v :: thp', σ').
 Notation "Γ ⊨ e '≤ctx≤' e' : τ" :=
   (ctx_refines Γ e e' τ) (at level 74, e, e', τ at next level).
 

F_mu_ref_conc/soundness_binary.v

@@ -3,16 +3,36 @@ From iris.algebra Require Import auth frac agree.
 From iris.base_logic Require Import big_op.
 From iris.proofmode Require Import tactics.
 From iris.program_logic Require Import adequacy.
-(* From iris_logrel.F_mu_ref_conc Require Import soundness_unary. *)
+
 Class heapPreIG Σ := HeapPreIG {
   heap_preG_iris :> invPreG Σ;
   heap_preG_heap :> gen_heapPreG loc val Σ
 }.
 
+(* In order to obtain the soundness results (typesafety and
+refinement) we need to generalize the contextual refinement to
+arbitrary types. For types which values we can observe ([obsTy]), it
+is the case that two related values are equal. *)
+Definition obsTy : type -> Prop := fun ty =>
+  match ty with
+  | TUnit | TNat | TBool => True
+  | _ => False
+  end.
+
+Lemma interp_obsTy_eq Σ `{heapIG Σ, cfgSG Σ} (v v' : val) τ :
+  ⟦ τ ⟧ [] (v, v') ⊢ ⌜obsTy τ → v = v'⌝.
+Proof.
+  induction τ; iIntros "HI"; simpl; eauto.
+  - iDestruct "HI" as "[% %]"; subst; eauto.
+  - iDestruct "HI" as (n) "[% %]"; subst; eauto.
+  - iDestruct "HI" as (b) "[% %]"; subst; eauto.
+Qed.
+
 Lemma logrel_adequate Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
     e e' τ σ :
   (∀ `{heapIG Σ, cfgSG Σ}, ∅ ⊨ e ≤log≤ e' : τ) →
-  adequate e σ (λ _, ∃ thp' h v', rtc step ([e'], ∅) (of_val v' :: thp', h)).
+  adequate e σ (λ v, ∃ thp' h v', rtc step ([e'], ∅) (of_val v' :: thp', h) 
+    ∧ (obsTy τ → v = v')).
 Proof.
   intros Hlog.
   eapply (wp_adequacy Σ _); iIntros (Hinv).
@@ -45,6 +65,7 @@ Proof.
     destruct tp as [|? tp']; simplify_eq/=.
     iMod ("Hclose" with "[-]") as "_".
     { iExists (_ :: tp'), σ'. eauto. }
+    iDestruct (interp_obsTy_eq with "Hinterp") as %Hobs.
     iIntros "!> !%"; eauto.
 Qed.
 
@@ -55,7 +76,7 @@ Theorem logrel_typesafety Σ `{heapPreIG Σ, inG Σ (authR cfgUR)} e τ e' thp
   is_Some (to_val e') ∨ reducible e' σ'.
 Proof.
   intros Hlog ??.
-  cut (adequate e σ (λ _, ∃ thp' h v, rtc step ([e], ∅) (of_val v :: thp', h))); first (intros [_ ?]; eauto).
+  cut (adequate e σ (λ v, ∃ thp' h v', rtc step ([e], ∅) (of_val v' :: thp', h) ∧ (obsTy τ → v = v'))); first (intros [_ ?]; eauto).
   eapply logrel_adequate; eauto.
 Qed.
 
@@ -63,10 +84,10 @@ Lemma logrel_simul Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
     e e' τ v thp hp :
   (∀ `{heapIG Σ, cfgSG Σ}, ∅ ⊨ e ≤log≤ e' : τ) →
   rtc step ([e], ∅) (of_val v :: thp, hp) →
-  (∃ thp' hp' v', rtc step ([e'], ∅) (of_val v' :: thp', hp')).
+  (∃ thp' hp' v', rtc step ([e'], ∅) (of_val v' :: thp', hp') ∧ (obsTy τ → v = v')).
 Proof.
   intros Hlog Hsteps.
-  cut (adequate e ∅ (λ _, ∃ thp' h v, rtc step ([e'], ∅) (of_val v :: thp', h))).
+  cut (adequate e ∅ (λ v, ∃ thp' h v', rtc step ([e'], ∅) (of_val v' :: thp', h) ∧ (obsTy τ → v = v'))).
   { destruct 1; naive_solver. }
   eapply logrel_adequate; eauto.
 Qed.
@@ -78,7 +99,11 @@ Lemma logrel_ctxequiv Σ `{heapPreIG Σ, inG Σ (authR cfgUR)}
   (∀ `{heapIG Σ, cfgSG Σ}, Γ ⊨ e ≤log≤ e' : τ) →
   Γ ⊨ e ≤ctx≤ e' : τ.
 Proof.
-  intros He He' Hlog K thp σ v ?. eapply (logrel_simul Σ _)=> ??.
+  intros He He' Hlog K thp σ v ? Hstep.
+  cut (∃ thp' hp' v', rtc step ([fill_ctx K e'], ∅) (of_val v' :: thp', hp') ∧ (obsTy TUnit → v = v')).
+  { naive_solver. }
+  eapply (logrel_simul Σ _); last by apply Hstep.
+  intros ??.
   iApply (bin_log_related_under_typed_ctx _ _ _ _ ∅); eauto.
   iPoseProof (Hlog _ _) as "Hrel". auto.
 Qed.