logrel_binary.v 10.2 KB
Newer Older
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37
From stdpp Require Import tactics.
From iris.proofmode Require Import tactics.
From iris.program_logic Require Export weakestpre.
From iris.base_logic Require Export big_op invariants.
From iris.algebra Require Import list.
From iris_logrel.logrel Require Export semtypes.
Import uPred.

Section bin_log_def.
  Context `{logrelG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).

  Definition interp_env (Γ : stringmap type) (E1 E2 : coPset)
      (Δ : listC D) (vvs : stringmap (val * val)) : iProp Σ :=
    (dom _ Γ = dom _ vvs 
     [ map] x  τvv  (map_zip Γ vvs), interp E1 E2 (fst τvv) Δ (snd τvv))%I.

  Global Instance interp_env_persistent Γ E1 E2 Δ vvs :
    PersistentP (interp_env Γ E1 E2 Δ vvs) := _.

  (* TODO: get rid of the box before interp_env? *)
  Definition bin_log_related_def (E1 E2 : coPset)
      (Δ : list D) (Γ : stringmap type)
      (e e' : expr) (τ : type) : iProp Σ := ( (vvs : stringmap (val * val)) ρ,
    spec_ctx ρ -
     interp_env Γ   Δ vvs 
    - interp_expr E1 E2 (interp   τ) Δ
             (env_subst (fst <$> vvs) e, env_subst (snd <$> vvs) e'))%I.
  Definition bin_log_related_aux : seal bin_log_related_def. Proof. by eexists. Qed.
  Definition bin_log_related := unseal bin_log_related_aux.
  Definition bin_log_related_eq : bin_log_related = bin_log_related_def :=
    seal_eq bin_log_related_aux.
End bin_log_def.

Notation "⟦ Γ ⟧*" := (interp_env Γ).

Notation "'{' E1 ',' E2 ';' Δ ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
38 39 40
  (bin_log_related E1 E2 Δ Γ e%E e'%E τ)
  (at level 74, E1,E2, e, e', τ at next level,
   format "'[hv' '{' E1 ',' E2 ';' Δ ';' Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
41
Notation "'{' E1 ',' E2 ';' Γ '}' ⊨ e '≤log≤' e' : τ" :=
42 43 44
  ( Δ, bin_log_related E1 E2 Δ Γ e%E e'%E τ)%I
  (at level 74, E1,E2, e, e', τ at next level,
   format "'[hv' '{' E1 ',' E2 ';' Γ '}'  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
45
Notation "Γ ⊨ e '≤log≤' e' : τ" :=
46 47 48
  ( Δ, bin_log_related   Δ Γ e%E e'%E τ)%I
  (at level 74, e, e', τ at next level,
   format "'[hv' Γ  ⊨  '/  ' e  '/' '≤log≤'  '/  ' e'  :  τ ']'").
49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201

(** [interp_env] properties *)
Section interp_env_facts.
  Context `{logrelG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types τi : D.
  Implicit Types Δ : listC D.

  Lemma interp_env_dom Δ Γ E1 E2 vvs : interp_env Γ E1 E2 Δ vvs  dom _ Γ = dom _ vvs.
  Proof. by iIntros "[% ?]". Qed.

  Lemma interp_env_Some_l Δ Γ E1 E2 vvs x τ :
    Γ !! x = Some τ  interp_env Γ E1 E2 Δ vvs   vv, vvs !! x = Some vv  interp E1 E2 τ Δ vv.
  Proof.
    iIntros (Hτ) "[Hdom HΓ]"; iDestruct "Hdom" as %Hdom.
    destruct (elem_of_dom vvs x) as [[v Hv] ].
    { rewrite -Hdom. apply elem_of_dom. by exists τ. }
    assert (map_zip Γ vvs !! x = Some (τ, v)) as Hτv.
    { rewrite map_lookup_zip_with.
      by rewrite Hτ /= Hv /=. }    
    iExists v; iSplit. done.    
    iApply (big_sepM_lookup _ _ _ _ Hτv with "HΓ").
  Qed.

  Lemma interp_env_nil Δ E1 E2 : True  interp_env  E1 E2 Δ .
  Proof.
    iIntros ""; iSplit. 
    - iPureIntro. unfold_leibniz. by rewrite ?dom_empty.
    - rewrite map_zip_with_empty. auto.
  Qed.

  Lemma interp_env_cons (Δ : list D) (Γ : stringmap type)
     (vvs : stringmap (val * val)) E1 E2 (τ : type) (vv : val * val) (x : string) :
    interp E1 E2 τ Δ vv  interp_env Γ E1 E2 Δ vvs 
     interp_env (<[x:=τ]> Γ) E1 E2 Δ (<[x:=vv]> vvs).
  Proof.
    iIntros "[Hτ [Hdom HΓ]]". iDestruct "Hdom" as %Hdom. iSplit.
    - iPureIntro. by rewrite !dom_insert_L Hdom. (* TODO: RK: look at why this is so slow *)
    - rewrite -(map_insert_zip_with pair Γ vvs x (τ,vv)); auto.
      rewrite -insert_delete.
      rewrite big_sepM_insert; last by rewrite lookup_delete.
      iFrame "Hτ".
      iApply (big_sepM_mono _ _ (map_zip Γ vvs) with "HΓ").
      { apply delete_subseteq. }
      done.
  Qed.

  Lemma interp_env_cons_bi (Δ : list D) (Γ : stringmap type) (vvs : stringmap (val * val)) E1 E2 (τ : type) (vv : val * val) (x : string) :
    x  dom (gset string) Γ 
    x  dom (gset string) vvs 
    interp_env (<[x:=τ]> Γ) E1 E2 Δ (<[x:=vv]> vvs) ⊣⊢ interp E1 E2 τ Δ vv  interp_env Γ E1 E2 Δ vvs.
  Proof.
    intros Hx1 Hx2.
    rewrite /interp_env /= (assoc _ ( _  _ _)) -(comm _ (_ = _)%I) -assoc.
    apply sep_proper; [apply pure_proper|].
    - unfold_leibniz. rewrite ?dom_insert.
      split. 
      + intros Hd y. destruct (Hd y) as [Hd1 Hd2].
        split; intro Hy.
        * destruct (elem_of_union {[x]} (dom (gset string) Γ) y) as [Hy1 Hy2].
          pose (Hy2':=Hd1 (Hy2 (or_intror Hy))).
          destruct (decide (x = y)) as [?|neq]; subst.
          { exfalso. by apply Hx1. }
          apply elem_of_union in Hy2'.
          destruct Hy2' as [F | ?]; auto.
          exfalso. apply neq. symmetry.
          (* what the hell am i even doing here TODO *)
          apply (and_rec (fun x1 _ => x1 F) (elem_of_singleton y x)).
        * destruct (elem_of_union {[x]} (dom (gset string) vvs) y) as [Hy1 Hy2 ].
          pose (Hy2':=Hd2 (Hy2 (or_intror Hy))).
          destruct (decide (x = y)) as [?|neq]; subst.
          { exfalso. by apply Hx2. }
          apply elem_of_union in Hy2'.
          destruct Hy2' as [F | ?]; auto.
          exfalso. apply neq. symmetry.
          apply (and_rec (fun x1 _ => x1 F) (elem_of_singleton y x)).
      + intros Heq. fold_leibniz. by f_equal.
    - rewrite -(map_insert_zip_with _ _ _ _ (τ, vv)); auto.
      rewrite big_sepM_insert /=; auto.
      apply not_elem_of_dom in Hx1.
      apply not_elem_of_dom in Hx2.
      unfold map_zip. erewrite lookup_merge.
      by rewrite Hx1 /=. 
      by compute.
  Qed.

  Lemma interp_env_ren Δ (Γ : stringmap type) E1 E2 (vvs : stringmap (val * val)) (τi : D) :
    interp_env (Autosubst_Classes.subst (ren (+1)) <$> Γ) E1 E2 (τi :: Δ) vvs
               ⊣⊢
    interp_env Γ E1 E2 Δ vvs.
  Proof.
    apply sep_proper; [apply pure_proper|].
    - unfold_leibniz. by rewrite dom_fmap. 
    - rewrite map_zip_with_fmap_1. 
      rewrite map_zip_with_map_zip.
      generalize (map_zip Γ vvs).
      apply map_ind. 
      + rewrite fmap_empty. done.
      + intros i [σ ww] m Hm IH.
        rewrite fmap_insert.
        rewrite ?big_sepM_insert /=; auto; last first.
        { rewrite lookup_fmap. rewrite Hm. done. }
        rewrite IH. apply sep_proper; auto.
        apply (interp_weaken [] [τi] Δ).
  Qed.
End interp_env_facts.

(** Properties of the relational interpretation *)
Section related_facts.
  Context `{logrelG Σ}.
  Notation D := (prodC valC valC -n> iProp Σ).
  Implicit Types τi : D.
  Implicit Types Δ : listC D.

  (* We need this to be able to open and closed invariants in front of logrels *)
  Lemma fupd_logrel E1 E2 Δ Γ e e' τ :
    ((|={E1,E2}=> ({E2,E2;Δ;Γ}  e log e' : τ))
     - {E1,E2;Δ;Γ}  e log e' : τ)%I.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "H".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    iMod "H".
    iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
  Qed.

  Lemma fupd_logrel' E1 E2 Δ Γ e e' τ :
    ((|={E1}=> ({E1,E2;Δ;Γ}  e log e' : τ))
     - {E1,E2;Δ;Γ}  e log e' : τ)%I.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "H".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    iMod "H".
    iSpecialize ("H" with "Hs [HΓ] Hj"); eauto.
  Qed.

  Global Instance elim_modal_logrel E1 E2 Δ Γ e e' P τ :
   ElimModal (|={E1,E2}=> P) P
     ({E1,E2;Δ;Γ}  e log e' : τ) ({E2,E2;Δ;Γ}  e log e' : τ) | 10.
  Proof.
    iIntros "[HP HI]". iApply fupd_logrel.
    iMod "HP". iApply ("HI" with "HP").
  Qed.

  Global Instance elim_modal_logrel' E1 E2 Δ Γ e e' P τ :
   ElimModal (|={E1}=> P) P
     ({E1,E2;Δ;Γ}  e log e' : τ) ({E1,E2;Δ;Γ}  e log e' : τ) | 0.
  Proof.
    iIntros "[HP HI]". iApply fupd_logrel'.
    iMod "HP". iApply ("HI" with "HP").
  Qed.

Dan Frumin's avatar
Cleanup  
Dan Frumin committed
202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219
  Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 τ :
    {,;Δ;Γ}  e1 log e2 : τ -
    {,;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$>Γ}  e1 log e2 : τ.[ren (+1)].
  Proof.
    rewrite bin_log_related_eq /bin_log_related_def.
    iIntros "Hlog" (vvs ρ) "#Hs #HΓ".
    iSpecialize ("Hlog" $! vvs with "Hs [HΓ]").
    { by rewrite interp_env_ren. }
    unfold interp_expr.
    iIntros (j K) "Hj /=".
    iMod ("Hlog" with "Hj") as "Hlog".
    iApply (wp_mono with "Hlog").
    iIntros (v). simpl.
    iDestruct 1 as (v') "[Hj Hτ]".
    iExists v'. iFrame.
    by rewrite -interp_ren.
  Qed.

220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266
End related_facts.

(** Monadic-like operations on logrel *)
Section monadic.
  Context `{logrelG Σ}.

  Lemma related_ret E1 E2 Δ Γ e1 e2 τ `{Closed  e1} `{Closed  e2} :
    interp_expr E1 E1  τ  Δ (e1,e2) - {E2,E2;Δ;Γ}  e1 log e2 : τ%I.
  Proof.
    iIntros "Hτ".
    rewrite bin_log_related_eq /bin_log_related_def.
    iIntros (vvs ρ) "#Hs #HΓ".
    rewrite /env_subst !Closed_subst_p_id.
    iIntros (j K) "Hj /=". iModIntro.
    iApply fupd_wp. iApply (fupd_mask_mono E1); auto.
    by iMod ("Hτ" with "Hj") as "Hτ".
  Qed.

  Lemma related_bind E Δ Γ (e1 e2 : expr) (τ τ' : type) (K K' : list ectx_item) :
    ({E,E;Δ;Γ}  e1 log e2 : τ) -
    ( vv,  τ  Δ vv - {E,E;Δ;Γ}  fill K (of_val (vv.1)) log fill K' (of_val (vv.2)) : τ') -
    ({E,E;Δ;Γ}  fill K e1 log fill K' e2 : τ').
  Proof.
    iIntros "Hm Hf".
    rewrite bin_log_related_eq /bin_log_related_def.
    iIntros (vvs ρ) "#Hs #HΓ".
    iIntros (j L) "Hj /=".
    iSpecialize ("Hm" with "Hs HΓ").
    rewrite /env_subst !fill_subst -fill_app.
    iMod ("Hm" with "Hj") as "Hm /=".
    iModIntro.
    iApply wp_bind.
    iApply (wp_wand with "Hm").
    iIntros (v1). iDestruct 1 as (v2) "[Hj Hvv]".
    rewrite fill_app.
    replace (of_val v1) with (subst_p (fst <$> vvs) (of_val v1))
      by (apply Closed_subst_p_id; done).
    replace (of_val v2) with (subst_p (snd <$> vvs) (of_val v2))
      by (apply Closed_subst_p_id; done).
    rewrite -!fill_subst.
    iApply fupd_wp. iApply (fupd_mask_mono E); eauto.
    iMod ("Hf" with "Hvv Hs HΓ Hj") as "Hf /=".
    done.
  Qed.
End monadic.

Typeclasses Opaque interp_env.