fundamental_binary.v 24.7 KB
Newer Older
1 2 3
Require Import iris.program_logic.hoare.
Require Import iris.program_logic.lifting.
Require Import iris.algebra.upred_big_op.
4 5 6
Require Import iris_logrel.F_mu_ref_par.lang iris_logrel.F_mu_ref_par.typing
        iris_logrel.F_mu_ref_par.rules iris_logrel.F_mu_ref_par.rules_binary
        iris_logrel.F_mu_ref_par.logrel_binary.
7 8 9 10 11 12 13 14
From iris.program_logic Require Export lifting.
From iris.algebra Require Import upred_big_op frac dec_agree.
From iris.program_logic Require Export invariants ghost_ownership.
From iris.program_logic Require Import ownership auth.
Require Import iris.proofmode.tactics iris.proofmode.invariants.
Import uPred.

Section typed_interp.
15 16
  Context {Σ : gFunctors} {iI : heapIG Σ} {iS : cfgSG Σ}
          {N : namespace}.
17 18 19 20 21 22 23 24 25 26 27 28

  Implicit Types P Q R : iPropG lang Σ.
  Notation "# v" := (of_val v) (at level 20).

  Local Tactic Notation "smart_wp_bind" uconstr(ctx) ident(v) ident(w)
        constr(Hv) uconstr(Hp) :=
    iApply (@wp_bind _ _ _ [ctx]);
    iApply wp_wand_l; iSplitR;
    [|iApply Hp; rewrite fill_app; simpl; repeat iSplitR; trivial];
    iIntros {v} "Htemporary";
    iDestruct "Htemporary" as {w} Hv;
    rewrite fill_app; simpl.
29

30 31 32 33 34 35 36 37 38
  Local Ltac value_case := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|].

  Lemma map_lookup {A B} (l : list A) (f : A  B) k :
    (map f l) !! k = option_map f (l !! k).
  Proof.
    revert k; induction l => k; simpl; trivial.
    destruct k; simpl; trivial.
  Qed.

39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61
  Definition bin_log_related Δ Γ e e' τ
             {HΔ : context_interp_Persistent Δ}
    :=
       vs,
        List.length Γ = List.length vs 
         ρ j K,
          ((heapI_ctx (N .@ 2)  Spec_ctx (N .@ 3) ρ 
                      Π∧ zip_with (λ τ v, @interp Σ iS iI (N .@ 1) τ Δ v) Γ vs
                                   j  (fill K (e'.[env_subst (map snd vs)]))
           )%I)
             WP (e.[env_subst (map fst vs)]) @ 
            {{ λ v,  v', j  (fill K (# v')) 
                            (@interp Σ iS iI (N .@ 1)
                                     τ Δ (v, v')) }}.

  Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" := (bin_log_related Δ Γ e e' τ)
                                       (at level 20) : bin_logrel_scope.

  Local Open Scope bin_logrel_scope.

  Notation "✓✓" := context_interp_Persistent.

  Lemma typed_binary_interp_Pair Δ Γ e1 e2 e1' e2' τ1 τ2 {HΔ : ✓✓ Δ}
62 63
        (IHHtyped1 : Δ  Γ  e1 log e1'  τ1)
        (IHHtyped2 : Δ  Γ  e2 log e2'  τ2)
64 65 66 67 68
    :
      Δ  Γ  Pair e1 e2 log Pair e1' e2'  TProd τ1 τ2.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (PairLCtx e2.[env_subst (map fst vs)]) v v' "[Hv #Hiv]"
69
                  (IHHtyped1 _ _ _ j
70 71
                             (K ++ [PairLCtx e2'.[env_subst (map snd vs)] ])).
    smart_wp_bind (PairRCtx v) w w' "[Hw #Hiw]"
72
                  (IHHtyped2 _ _ _ j (K ++ [(PairRCtx v')])).
73
    value_case. iExists (PairV v' w'); iFrame "Hw".
74
    iExists (v, w), (v', w'); simpl; repeat iSplit; trivial.
75 76 77 78 79
    (* unshelving *)
    Unshelve. all: trivial.
  Qed.

  Lemma typed_binary_interp_Fst Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
80
        (IHHtyped : Δ  Γ  e log e'  (TProd τ1 τ2))
81 82 83 84 85
    :
      Δ  Γ  Fst e log Fst e'  τ1.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (FstCtx) v v' "[Hv #Hiv]"
86
                  (IHHtyped _ _ _ j (K ++ [FstCtx])); cbn.
87 88 89 90 91 92 93 94 95 96 97 98
    iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]".
    inversion H; subst.
    iPvs (step_fst _ _ _ j K (# (w2.1)) (w2.1) (# (w2.2)) (w2.2)
                   _ _ _ with "* -") as "Hw".
    iFrame "Hspec Hv"; trivial.
    iApply wp_fst; eauto using to_of_val; cbn.
    iNext. iExists _; iSplitL; trivial.
    (* unshelving *)
    Unshelve. all: eauto using to_of_val.
  Qed.

  Lemma typed_binary_interp_Snd Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
99
        (IHHtyped : Δ  Γ  e log e'  (TProd τ1 τ2))
100 101 102 103 104
    :
      Δ  Γ  Snd e log Snd e'  τ2.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (SndCtx) v v' "[Hv #Hiv]"
105
                  (IHHtyped _ _ _ j (K ++ [SndCtx])); cbn.
106 107 108 109 110 111 112 113 114 115 116 117
    iDestruct "Hiv" as {w1 w2} "#[% [Hiv2 Hiv3]]".
    inversion H; subst.
    iPvs (step_snd _ _ _ j K (# (w2.1)) (w2.1) (# (w2.2)) (w2.2)
                   _ _ _ with "* -") as "Hw".
    iFrame "Hspec Hv"; trivial.
    iApply wp_snd; eauto using to_of_val; cbn.
    iNext. iExists _; iSplitL; trivial.
    (* unshelving *)
    Unshelve. all: eauto using to_of_val.
  Qed.

  Lemma typed_binary_interp_InjL Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
118
        (IHHtyped : Δ  Γ  e log e'  τ1)
119 120 121 122 123
    :
      Δ  Γ  InjL e log InjL e'  (TSum τ1 τ2).
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (InjLCtx) v v' "[Hv #Hiv]"
124
                  (IHHtyped _ _ _ j (K ++ [InjLCtx])); cbn.
125 126 127 128 129 130 131
    value_case. iExists (InjLV v'); iFrame "Hv".
    iLeft; iExists _; iSplit; [|eauto]; simpl; trivial.
    (* unshelving *)
    Unshelve. all: trivial.
  Qed.

  Lemma typed_binary_interp_InjR Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
132
        (IHHtyped : Δ  Γ  e log e'  τ2)
133 134 135 136 137
    :
      Δ  Γ  InjR e log InjR e'  (TSum τ1 τ2).
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (InjRCtx) v v' "[Hv #Hiv]"
138
                  (IHHtyped _ _ _ j (K ++ [InjRCtx])); cbn.
139 140 141 142 143 144
    value_case. iExists (InjRV v'); iFrame "Hv".
    iRight; iExists _; iSplit; [|eauto]; simpl; trivial.
    (* unshelving *)
    Unshelve. all: trivial.
  Qed.

145 146 147 148 149 150
  Lemma typed_binary_interp_Case Δ Γ (e0 e1 e2 e0' e1' e2' : expr) τ1 τ2 τ3
        {HΔ : ✓✓ Δ}
        (Hclosed2 :  f, e1.[iter (S (List.length Γ)) up f] = e1)
        (Hclosed3 :  f, e2.[iter (S (List.length Γ)) up f] = e2)
        (Hclosed2' :  f, e1'.[iter (S (List.length Γ)) up f] = e1')
        (Hclosed3' :  f, e2'.[iter (S (List.length Γ)) up f] = e2')
151 152 153
        (IHHtyped1 : Δ  Γ  e0 log e0'  TSum τ1 τ2)
        (IHHtyped2 : Δ  τ1 :: Γ  e1 log e1'  τ3)
        (IHHtyped3 : Δ  τ2 :: Γ  e2 log e2'  τ3)
154 155 156 157 158
    :
      Δ  Γ  Case e0 e1 e2 log Case e0' e1' e2'  τ3.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (CaseCtx _ _) v v' "[Hv #Hiv]"
159
                  (IHHtyped1 _ _ _ j (K ++ [CaseCtx _ _])); cbn.
160 161 162 163 164 165 166 167
    iDestruct "Hiv" as "[Hiv|Hiv]".
    + iDestruct "Hiv" as {w} "[% Hw]".
      inversion H; subst.
      iPvs (step_case_inl _ _ _ j K (# (w.2)) (w.2) _ _
                          _ _ with "* -") as "Hz".
      iFrame "Hspec Hv"; trivial.
      iApply wp_case_inl; auto 1 using to_of_val.
      asimpl.
168
      specialize (IHHtyped2 (w::vs)); simpl in IHHtyped2.
169
      erewrite <- ?n_closed_subst_head_simpl in IHHtyped2; eauto;
170 171 172 173 174 175 176 177 178 179
        simpl; try rewrite map_length; eauto with f_equal. iNext.
      iApply IHHtyped2; auto 2.
      iFrame "Hheap Hspec Hw HΓ"; trivial.
    + iDestruct "Hiv" as {w} "[% Hw]".
      inversion H; subst.
      iPvs (step_case_inr _ _ _ j K (# (w.2)) (w.2) _ _
                          _ _ with "* -") as "Hz".
      iFrame "Hspec Hv"; trivial.
      iApply wp_case_inr; auto 1 using to_of_val.
      asimpl.
180
      specialize (IHHtyped3 (w::vs)); simpl in IHHtyped3.
181
      erewrite <- ?n_closed_subst_head_simpl in IHHtyped3; eauto;
182 183 184 185 186 187 188
        simpl; try rewrite map_length; eauto with f_equal. iNext.
      iApply IHHtyped3; auto 2.
      iFrame "Hheap Hspec Hw HΓ"; trivial.
      (* unshelving *)
      Unshelve. all: eauto using to_of_val.
  Qed.

189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230
  Lemma typed_binary_interp_If Δ Γ e0 e1 e2 e0' e1' e2' τ {HΔ : ✓✓ Δ}
        (IHHtyped1 : Δ  Γ  e0 log e0'  TBool)
        (IHHtyped2 : Δ  Γ  e1 log e1'  τ)
        (IHHtyped3 : Δ  Γ  e2 log e2'  τ)
    :
      Δ  Γ  If e0 e1 e2 log If e0' e1' e2'  τ.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (IfCtx _ _) v v' "[Hv #Hiv]"
                  (IHHtyped1 _ _ _ j (K ++ [IfCtx _ _])); cbn.
    iDestruct "Hiv" as {b} "[% %]"; subst; destruct b; simpl.
    + iPvs (step_if_true _ _ _ j K _ _ _ with "* -") as "Hz".
      iFrame "Hspec Hv"; trivial. iApply wp_if_true. iNext.
      iApply IHHtyped2; trivial. iFrame "Hheap Hspec HΓ"; trivial.
    + iPvs (step_if_false _ _ _ j K _ _ _ with "* -") as "Hz".
      iFrame "Hspec Hv"; trivial. iApply wp_if_false. iNext.
      iApply IHHtyped3; trivial. iFrame "Hheap Hspec HΓ"; trivial.
      (* unshelving *)
      Unshelve. all: eauto using to_of_val.
  Qed.

  Lemma typed_binary_interp_nat_bin_op Δ Γ op e1 e2 e1' e2' {HΔ : ✓✓ Δ}
        (IHHtyped1 : Δ  Γ  e1 log e1'  TNat)
        (IHHtyped2 : Δ  Γ  e2 log e2'  TNat)
    :
      Δ  Γ  NBOP op e1 e2 log NBOP op e1' e2'  (NatBinOP_res_type op).
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (NBOPLCtx _ _) v v' "[Hv #Hiv]"
                  (IHHtyped1 _ _ _ j (K ++ [NBOPLCtx _ _])); cbn.
    smart_wp_bind (NBOPRCtx _ _) w w' "[Hw #Hiw]"
                  (IHHtyped2 _ _ _ j (K ++ [NBOPRCtx _ _])); cbn.
    iDestruct "Hiv" as {n} "[% %]"; subst; simpl.
    iDestruct "Hiw" as {n'} "[% %]"; subst; simpl.
    iPvs (step_nat_bin_op _ _ _ j K _ _ _ _ with "* -") as "Hz".
    iFrame "Hspec Hw"; trivial. iApply wp_nat_bin_op. iNext.
    iExists _; iSplitL; eauto.
    destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
      try destruct lt_dec; iExists _; iSplit; trivial.
    (* unshelving *)
    Unshelve. all: eauto using to_of_val.
  Qed.
231

232 233 234
  Lemma typed_binary_interp_Lam Δ Γ (e e' : expr) τ1 τ2 {HΔ : ✓✓ Δ}
        (Hclosed :  f, e.[iter (S (S (List.length Γ))) up f] = e)
        (Hclosed' :  f, e'.[iter (S (S (List.length Γ))) up f] = e')
235
        (IHHtyped : Δ  TArrow τ1 τ2 :: τ1 :: Γ  e log e'  τ2)
236 237 238 239 240
    :
      Δ  Γ  Lam e log Lam e'   TArrow τ1 τ2.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    value_case. iExists (LamV _). iFrame "Htr".
241
    iApply löb. rewrite -always_later. iIntros "#Hlat".
242 243 244 245
    iAlways. iIntros {j' K' v} "[#Hiv Hv]".
    iApply wp_lam; auto 1 using to_of_val. iNext.
    iPvs (step_lam _ _ _ j' K' _ (# (v.2)) (v.2) _ _ with "* -") as "Hz".
    iFrame "Hspec Hv"; trivial.
246 247 248 249
    asimpl.
    specialize (IHHtyped ((LamV e.[upn 2 (env_subst (map fst vs))],
                           LamV e'.[upn 2 (env_subst (map snd vs))])
                            :: v :: vs)). simpl in IHHtyped.
250
    erewrite <- ?n_closed_subst_head_simpl_2 in IHHtyped; eauto; simpl;
251
      try rewrite map_length; auto.
252
    iApply IHHtyped; auto.
253
    repeat iSplitR; trivial. repeat iSplit; trivial.
254 255 256 257 258
    (* unshelving *)
    Unshelve. all: eauto using to_of_val.
  Qed.

  Lemma typed_binary_interp_App Δ Γ e1 e2 e1' e2' τ1 τ2 {HΔ : ✓✓ Δ}
259 260
        (IHHtyped1 : Δ  Γ  e1 log e1'  TArrow τ1 τ2)
        (IHHtyped2 : Δ  Γ  e2 log e2'  τ1)
261 262 263 264 265
    :
      Δ  Γ  App e1 e2 log App e1' e2'   τ2.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (AppLCtx (e2.[env_subst (map fst vs)])) v v' "[Hv #Hiv]"
266
                  (IHHtyped1 _ _ _ j
267 268
                     (K ++ [(AppLCtx (e2'.[env_subst (map snd vs)]))])); cbn.
    smart_wp_bind (AppRCtx v) w w' "[Hw #Hiw]"
269
                  (IHHtyped2 _ _ _ j (K ++ [AppRCtx v'])); cbn.
270
    iApply ("Hiv" $! j K (w, w')); simpl.
271
    iFrame "Hw"; trivial.
272 273 274 275 276
    (* unshelving *)
    Unshelve. all: trivial.
  Qed.

  Lemma typed_binary_interp_TLam Δ Γ e e' τ {HΔ : ✓✓ Δ}
277 278 279
        (IHHtyped :  τi (Hpr: BiVal_to_IProp_Persistent τi),
            (extend_context_interp_fun1 τi Δ)  map (λ t : type, t.[ren (+1)]) Γ
                                               e log e'  τ)
280 281 282 283 284 285 286 287
    :
      Δ  Γ  TLam e log TLam e'   TForall τ.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    value_case. iExists (TLamV _). iFrame "Htr"; simpl.
    iExists (e.[env_subst (map fst vs)], e'.[env_subst (map snd vs)]).
    iSplit; trivial.
    iIntros {τi}; destruct τi as [τi τiPr].
288
    iAlways. iIntros {j' K'} "Hv". simpl.
289 290 291 292 293 294
    iApply IHHtyped; [rewrite map_length; trivial|].
    iFrame "Hheap Hspec Hv".
    rewrite zip_with_context_interp_subst; trivial.
  Qed.

  Lemma typed_binary_interp_TApp Δ Γ e e' τ τ' {HΔ : ✓✓ Δ}
295
        (IHHtyped : Δ  Γ  e log e'  TForall τ)
296 297 298 299 300
    :
      Δ  Γ  TApp e log TApp e'  τ.[τ'/].
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (TAppCtx) v v' "[Hv #Hiv]"
301
                    (IHHtyped _ _ _ j (K ++ [TAppCtx])); cbn.
302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318
    iDestruct "Hiv" as {e''} "[% He'']".
    inversion H; subst.
    iSpecialize ("He''" $! ((interp τ' Δ)  _)); cbn.
    iPvs (step_Tlam _ _ _ j K (e''.2) _ with "* -") as "Hz".
    iFrame "Hspec Hv"; trivial.
    iApply wp_TLam.
    iRevert "He''"; iIntros "#He''". (*To get rid of . Is this the best way?!*)
    iNext.
    iApply wp_wand_l; iSplitR; [|iApply "He''"; auto].
    iIntros {w} "Hw". iDestruct "Hw" as {w'} "[Hw #Hiw]".
    iExists _; iFrame "Hw".
    rewrite -interp_subst; trivial.
    (* unshelving *)
    Unshelve. all: trivial. simpl; typeclasses eauto.
  Qed.

  Lemma typed_binary_interp_Fold Δ Γ e e' τ {HΔ : ✓✓ Δ}
319
        (IHHtyped : Δ  Γ  e log e'  τ.[(TRec τ)/])
320 321 322 323 324 325
    :
      Δ  Γ  Fold e log Fold e'   TRec τ.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    iApply (@wp_bind _ _ _ [FoldCtx]);
      iApply wp_wand_l; iSplitR;
326
        [|iApply (IHHtyped _ _ _ j (K ++ [FoldCtx]));
327
          rewrite fill_app; simpl; repeat iSplitR; trivial].
328 329 330 331 332 333 334 335
    iIntros {v} "Hv"; iDestruct "Hv" as {w} "[Hv #Hiv]";
      rewrite fill_app.
    value_case. iExists (FoldV w); iFrame "Hv".
    rewrite fixpoint_unfold; cbn.
    rewrite -interp_subst; trivial.
    iAlways; iExists (_, _); iSplit; try iNext; trivial.
    (* unshelving *)
    Unshelve. all: trivial.
336 337 338
  Qed.

  Lemma typed_binary_interp_Unfold Δ Γ e e' τ {HΔ : ✓✓ Δ}
339
        (IHHtyped : Δ  Γ  e log e'  TRec τ)
340 341 342 343 344 345
    :
      Δ  Γ  Unfold e log Unfold e'  τ.[(TRec τ)/].
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    iApply (@wp_bind _ _ _ [UnfoldCtx]);
      iApply wp_wand_l; iSplitR;
346
        [|iApply (IHHtyped _ _ _ j (K ++ [UnfoldCtx]));
347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
          rewrite fill_app; simpl; repeat iSplitR; trivial].
    iIntros {v} "Hv". iDestruct "Hv" as {w} "[Hw #Hiw]"; rewrite fill_app.
    simpl. rewrite fixpoint_unfold; simpl.
    iRevert "Hiw"; iIntros "#Hiw". (*To get rid of . Is this the best way?!*)
    change (fixpoint _) with (@interp _ _ _ (N .@ 1) (TRec τ) Δ).
    iDestruct "Hiw" as {z} "[% #Hiz]"; inversion H; subst.
    iPvs (step_Fold _ _ _ j K (# (z.2)) (z.2) _ _ with "* -") as "Hz".
    iFrame "Hspec Hw"; trivial.
    iApply wp_Fold; cbn; auto using to_of_val.
    iNext. iExists _; iFrame "Hz".
    rewrite -interp_subst; destruct z; trivial.
    (* unshelving *)
    Unshelve. all: eauto using to_of_val.
  Qed.

  Lemma typed_binary_interp_Fork Δ Γ e e' {HΔ : ✓✓ Δ}
363
        (IHHtyped : Δ  Γ  e log e'  TUnit)
364 365 366 367 368 369 370 371 372 373 374
    :
      Δ  Γ  Fork e log Fork e'  TUnit.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    iPvs (step_fork _ _ _ j K _ _ with "* -") as "Hz".
    iFrame "Hspec Htr"; trivial.
    iDestruct "Hz" as {j'} "[Hz1 Hz2]".
    iApply wp_fork.
    iSplitL "Hz1".
    + iNext. iExists UnitV; iFrame "Hz1"; iSplit; trivial.
    + iNext. iApply wp_wand_l; iSplitR;
375
               [|iApply (IHHtyped _ _ _ _ [])]; trivial.
376 377 378 379 380 381 382
      * iIntros {w} "Hw"; trivial.
      * iFrame "Hheap Hspec HΓ"; trivial.
    (* unshelving *)
    Unshelve. all: trivial.
  Qed.

  Lemma typed_binary_interp_Alloc Δ Γ e e' τ {HΔ : ✓✓ Δ}
383
        (IHHtyped : Δ  Γ  e log e'  τ)
384 385 386 387 388
    :
      Δ  Γ  Alloc e log Alloc e'  (Tref τ).
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (AllocCtx) v v' "[Hv #Hiv]"
389
                  (IHHtyped _ _ _ j (K ++ [AllocCtx])).
390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424
    iApply wp_atomic; cbn; trivial; [rewrite to_of_val; auto|].
    iPvsIntro.
    iPvs (step_alloc _ _ _ j K (# v') v' _ _ with "* -") as "Hz".
    iFrame "Hspec Hv"; trivial.
    iDestruct "Hz" as {l'} "[Hj Hl']".
    iApply wp_alloc; auto 1 using to_of_val.
    iFrame "Hheap". iNext.
    iIntros {l} "Hl".
    iAssert (( w : val * val, l ↦ᵢ w.1  l' ↦ₛ w.2 
                                 ((@interp _ _ _ (N .@ 1) τ) Δ) w)%I)
      as "Hinv" with "[Hl Hl']".
    { iExists (v, v'); iFrame "Hl Hl' Hiv"; trivial. }
    iPvs (inv_alloc _ with "[Hinv]") as "HN"; eauto 1.
    { iNext; iExact "Hinv". }
    iPvsIntro; iExists (LocV l'); iSplit; [iExact "Hj"|].
    iExists (l, l'); iSplit; trivial.
    (* unshelving *)
    Unshelve. all: eauto using to_of_val.
  Qed.

  Lemma Disjoint_after_dot :  i (l : loc * loc), i  1   N .@ i  N .@ 1 .@ l.
  Proof.
    intros i l h.
    apply ndot_preserve_disjoint_r, ndot_ne_disjoint; auto.
  Qed.

  Ltac SolveDisj i l :=
    let Hneq := fresh "Hneq" in
    let Hdsj := fresh "Hdsj" in
    assert (Hneq : i  1) by omega; set (Hdsj := Disjoint_after_dot i l Hneq);
    clearbody Hdsj; clear Hneq; revert Hdsj;
    generalize (N .@ 1) as S1; generalize (N .@ 2) as S2;
    intros S1 S2 Hsdj; set_solver_ndisj.

  Lemma typed_binary_interp_Load Δ Γ e e' τ {HΔ : ✓✓ Δ}
425
        (IHHtyped : Δ  Γ  e log e'  (Tref τ))
426 427 428 429 430
    :
      Δ  Γ  Load e log Load e'  τ.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (LoadCtx) v v' "[Hv #Hiv]"
431
                  (IHHtyped _ _ _ j (K ++ [LoadCtx])).
432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452
    iDestruct "Hiv" as {l} "[% Hinv]".
    inversion H; subst.
    iApply wp_atomic; cbn; trivial.
    iPvsIntro.
    iInv (N .@ 1 .@ l) as {w} "[Hw1 [Hw2 #Hw3]]".
    iTimeless "Hw2".
    iPvs (step_load _ _ _ j K (l.2) 1 (w.2) _ with "[Hv Hw2]") as "[Hv Hw2]".
    iFrame "Hspec Hv"; trivial.
    iApply (wp_load _ _ _ 1); [|iFrame "Hheap"]; trivial.
    SolveDisj 2 l.
    iNext. iFrame "Hw1". iIntros "Hw1".
    iSplitL "Hw1 Hw2".
    + iNext; iExists w; iFrame "Hw1 Hw2 Hw3"; trivial.
    + iPvsIntro.
      destruct w as [w1 w2]; iExists (w2); iFrame "Hv Hw3"; trivial.
      (* unshelving *)
      Unshelve. all: eauto using to_of_val.
      SolveDisj 3 l.
  Qed.

  Lemma typed_binary_interp_Store Δ Γ e1 e2 e1' e2' τ {HΔ : ✓✓ Δ}
453 454
        (IHHtyped1 : Δ  Γ  e1 log e1'  (Tref τ))
        (IHHtyped2 : Δ  Γ  e2 log e2'  τ)
455 456 457 458 459
    :
      Δ  Γ  Store e1 e2 log Store e1' e2'  TUnit.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (StoreLCtx _) v v' "[Hv #Hiv]"
460
                  (IHHtyped1 _ _ _ j (K ++ [StoreLCtx _])).
461
    smart_wp_bind (StoreRCtx _) w w' "[Hw #Hiw]"
462
                  (IHHtyped2 _ _ _ j (K ++ [StoreRCtx _])).
463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
    iDestruct "Hiv" as {l} "[% Hinv]".
    inversion H; subst.
    iApply wp_atomic; trivial;
      [eapply bool_decide_spec; eauto using to_of_val|].
    iPvsIntro.
    iInv (N .@ 1 .@ l) as {z} "[Hw1 [Hw2 #Hw3]]".
    eapply bool_decide_spec; eauto using to_of_val.
    iTimeless "Hw2".
    iPvs (step_store _ _ _ j K (l.2) (z.2) (# w') w' _ _ with "[Hw Hw2]")
      as "[Hw Hw2]".
    iFrame "Hspec Hw Hw2"; trivial.
    iApply (wp_store (N .@ 2)); auto using to_of_val.
    SolveDisj 2 l.
    iFrame "Hheap Hw1". iNext. iIntros "Hw1".
    iSplitL "Hw1 Hw2".
    + iNext; iExists (w, w'); iFrame "Hw1 Hw2 Hiw"; trivial.
    + iPvsIntro. iExists UnitV; iFrame "Hw" ; iSplit; trivial.
      (* unshelving *)
      Unshelve. all: eauto using to_of_val.
      SolveDisj 3 l.
  Qed.

  Lemma typed_binary_interp_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ {HΔ : ✓✓ Δ}
        (HEqτ : EqType τ)
487 488 489
        (IHHtyped1 : Δ  Γ  e1 log e1'  Tref τ)
        (IHHtyped2 : Δ  Γ  e2 log e2'  τ)
        (IHHtyped3 : Δ  Γ  e3 log e3'  τ)
490
    :
491
      Δ  Γ  CAS e1 e2 e3 log CAS e1' e2' e3'  TBool.
492 493 494
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (CasLCtx _ _) v v' "[Hv #Hiv]"
495
                  (IHHtyped1 _ _ _ j (K ++ [CasLCtx _ _])).
496
    smart_wp_bind (CasMCtx _ _) w w' "[Hw #Hiw]"
497
                  (IHHtyped2 _ _ _ j (K ++ [CasMCtx _ _])).
498
    smart_wp_bind (CasRCtx _ _) u u' "[Hu #Hiu]"
499
                  (IHHtyped3 _ _ _ j (K ++ [CasRCtx _ _])).
500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521
    iDestruct "Hiv" as {l} "[% Hinv]".
    inversion H; subst.
    iApply wp_atomic; trivial;
      [cbn; eauto 10 using to_of_val|].
    iPvsIntro.
    iInv (N .@ 1 .@ l) as {z} "[Hw1 [Hw2 #Hw3]]".
    eapply bool_decide_spec; eauto 10 using to_of_val.
    iTimeless "Hw2".
    destruct z as [z1 z2]; simpl.
    destruct (val_dec_eq z1 w) as [|Hneq]; subst.
    + iPvs (step_cas_suc _ _ _ j K (l.2) (# w') w' z2 (# u') u' _ _ _
            with "[Hu Hw2]") as "[Hw Hw2]"; simpl.
      { iFrame "Hspec Hu Hw2". iNext.
        rewrite ?EqType_related_eq; trivial.
        iDestruct "Hiw" as "%". iDestruct "Hw3" as "%".
        repeat subst; trivial. }
      iApply (wp_cas_suc (N .@ 2)); eauto using to_of_val.
      SolveDisj 2 l.
      iFrame "Hheap Hw1".
      iNext. iIntros "Hw1".
      iSplitL "Hw1 Hw2".
      * iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
522
      * iPvsIntro. iExists (v true); iFrame "Hw". iExists _; iSplit; trivial.
523 524 525 526 527 528 529 530 531 532 533 534
    + iPvs (step_cas_fail _ _ _ j K (l.2) 1 (z2) (# w') w' (# u') u' _ _ _
            with "[Hu Hw2]") as "[Hw Hw2]"; simpl.
      { iFrame "Hspec Hu Hw2". iNext.
        rewrite ?EqType_related_eq; trivial.
        iDestruct "Hiw" as "%". iDestruct "Hw3" as "%".
        repeat subst; trivial. }
      iApply (wp_cas_fail (N .@ 2)); eauto using to_of_val.
      SolveDisj 2 l.
      iFrame "Hheap Hw1".
      iNext. iIntros "Hw1".
      iSplitL "Hw1 Hw2".
      * iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
535
      * iPvsIntro. iExists (v false); iFrame "Hw". iExists _; iSplit; trivial.
536 537 538 539 540
        (* unshelving *)
        Unshelve. all: eauto using to_of_val. all: SolveDisj 3 l.
  Qed.

  Lemma typed_binary_interp Δ Γ e τ {HΔ : context_interp_Persistent Δ}
541
        (Htyped : typed Γ e τ) : Δ  Γ  e log e  τ.
542
  Proof.
543 544
    revert Δ HΔ; induction Htyped; intros Δ HΔ.
    - intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
545 546 547 548 549 550 551 552
      destruct (lookup_lt_is_Some_2 vs x) as [v Hv].
      { by rewrite -Hlen; apply lookup_lt_Some with τ. }
      rewrite /env_subst. repeat rewrite map_lookup. rewrite Hv; simpl.
      value_case.
      iExists _; iFrame "Htr".
      iApply (big_and_elem_of with "HΓ").
      apply elem_of_list_lookup_2 with x.
      rewrite lookup_zip_with; simplify_option_eq; destruct v; trivial.
553 554
    - intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
      value_case. iExists UnitV; iFrame "Htr"; iSplit; trivial.
555 556 557 558 559
    - intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
      value_case. iExists (v _); iFrame "Htr"; iExists _; iSplit; trivial.
    - intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
      value_case. iExists (v _); iFrame "Htr"; iExists _; iSplit; trivial.
    - apply typed_binary_interp_nat_bin_op; trivial.
560 561 562 563 564
    - apply typed_binary_interp_Pair; trivial.
    - eapply typed_binary_interp_Fst; trivial.
    - eapply typed_binary_interp_Snd; trivial.
    - eapply typed_binary_interp_InjL; trivial.
    - eapply typed_binary_interp_InjR; trivial.
565 566
    - eapply typed_binary_interp_Case; eauto;
        match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
567
    - eapply typed_binary_interp_If; eauto.
568 569
    - eapply typed_binary_interp_Lam; eauto;
        match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
570 571 572 573 574 575 576 577 578 579
    - eapply typed_binary_interp_App; trivial.
    - eapply typed_binary_interp_TLam; trivial.
    - eapply typed_binary_interp_TApp; trivial.
    - eapply typed_binary_interp_Fold; trivial.
    - eapply typed_binary_interp_Unfold; trivial.
    - eapply typed_binary_interp_Fork; trivial.
    - eapply typed_binary_interp_Alloc; trivial.
    - eapply typed_binary_interp_Load; trivial.
    - eapply typed_binary_interp_Store; trivial.
    - eapply typed_binary_interp_CAS; eauto.
580 581
  Qed.

582 583 584
End typed_interp.

Notation "Δ ∥ Γ ⊩ e '≤log≤' e' ∷ τ" := (bin_log_related Δ Γ e e' τ)
585 586
                                         (at level 20) : bin_logrel_scope.
Delimit Scope bin_logrel_scope with bin_logrel.