fundamental_binary.v

From iris_logrel.logrel Require Export logrel_binary.
From iris_logrel.logrel.proofmode Require Export tactics_rel tactics_threadpool.

Section fundamental.
Context `{logrelG Σ}.
Notation D := (prodC valC valC -n> iProp Σ).
Implicit Types e : expr.
Implicit Types Δ : listC D.
Hint Resolve to_of_val.

Section masked.
  Variable (E : coPset).

  Local Ltac value_case :=
    iApply (related_ret ⊤);
    iApply interp_ret; [solve_to_val..|];
    simpl; eauto.

  Local Ltac value_case' := iApply wp_value; [cbn; rewrite ?to_of_val; trivial|]; repeat iModIntro.

  Local Tactic Notation "rel_bind_ap" uconstr(e1) uconstr(e2) constr(IH) ident(v) ident(w) constr(Hv):=
    rel_bind_l e1;
    rel_bind_r e2;
    iApply (related_bind with IH);
    iIntros ([v w]) Hv; simpl.

  (* Old tactic *)
  Local Tactic Notation "smart_bind" ident(j) uconstr(e) uconstr(e') constr(IH) ident(v) ident(w) constr(Hv):=
    try (iModIntro);
    wp_bind e;
    tp_bind j e';
    iSpecialize (IH with "Hs [HΓ] Hj"); eauto;
    iApply fupd_wp; iApply (fupd_mask_mono _); auto;
    iMod IH as IH; iModIntro;
    iApply (wp_wand with IH);
    iIntros (v);
    let vh := iFresh in
    iIntros vh;
    try (iMod vh);
    iDestruct vh as (w) (String.append "[Hj " (String.append Hv " ]")); simpl.

  Lemma bin_log_related_var Δ Γ x τ :
    Γ !! x = Some τ →
    {E,E;Δ;Γ} ⊨ Var x ≤log≤ Var x : τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (? vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj".
    iDestruct (interp_env_Some_l with "HΓ") as ([v v']) "[Hvv' ?]"; first done.
    iDestruct "Hvv'" as %Hvv'.
    cbn-[env_subst].
    rewrite (env_subst_lookup (snd <$> vvs) x v'); last first.
    { rewrite lookup_fmap. by rewrite Hvv'. } 
    rewrite (env_subst_lookup _ x v); last first.
    { rewrite lookup_fmap. by rewrite Hvv'. } 
    iModIntro. value_case'; eauto.
  Qed.

  Lemma bin_log_related_unit Δ Γ : {E,E;Δ;Γ} ⊨ #() ≤log≤ #() : TUnit.
  Proof.
    value_case.
  Qed.

  Lemma bin_log_related_nat Δ Γ (n : nat) : {E,E;Δ;Γ} ⊨ # n ≤log≤ # n : TNat.
  Proof.
    value_case.
  Qed.

  Lemma bin_log_related_bool Δ Γ (b : bool) : {E,E;Δ;Γ} ⊨ # b ≤log≤ # b : TBool.
  Proof.
    value_case.
  Qed.

  Lemma bin_log_related_pair Δ Γ e1 e2 e1' e2' τ1 τ2 :
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ1 -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ2 -∗
    {E,E;Δ;Γ} ⊨ Pair e1 e2 ≤log≤ Pair e1' e2' : TProd τ1 τ2.
  Proof.
    iIntros "IH1 IH2".
    rel_bind_ap e1 e1' "IH1" v1 v1' "Hvv1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "Hvv2".
    value_case.
    iExists _, _; eauto.
    iSplit; simpl; eauto.  auto. 
  Qed.

  Lemma bin_log_related_fst Δ Γ e e' τ1 τ2 :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TProd τ1 τ2 -∗
    {E,E;Δ;Γ} ⊨ Fst e ≤log≤ Fst e' : τ1.
  Proof.
    iIntros (?) "IH".
    rel_bind_ap e e' "IH" v w "IH".
    iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]". simplify_eq/=.
    rel_proj_l.
    rel_proj_r.
    value_case.
  Qed.

  Lemma bin_log_related_snd Δ Γ e e' τ1 τ2 :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TProd τ1 τ2 -∗
    {E,E;Δ;Γ} ⊨ Snd e ≤log≤ Snd e' : τ2.
  Proof.
    iIntros (?) "IH".
    rel_bind_ap e e' "IH" v w "IH".
    iDestruct "IH" as ([v1 v2] [w1 w2]) "[% [IHw IHw']]". simplify_eq/=.
    rel_proj_l.
    rel_proj_r.
    value_case.
  Qed.

  Lemma bin_log_related_app Δ Γ e1 e2 e1' e2' τ1 τ2 :
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow τ1 τ2 -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ1 -∗
    {E,E;Δ;Γ} ⊨ App e1 e2 ≤log≤ App e1' e2' :  τ2.
  Proof.
    iIntros "IH1 IH2".
    rel_bind_ap e1 e1' "IH1" f f' "Hff".
    rel_bind_ap e2 e2' "IH2" v v' "Hvv".
    iSpecialize ("Hff" with "Hvv"). simpl.
    by iApply related_ret.
  Qed.

  Lemma bin_log_related_rec Δ (Γ : stringmap type) (f x : binder) (e e' : expr) τ1 τ2 :
    Closed (x :b: f :b: dom _ Γ) e →
    Closed (x :b: f :b: dom _ Γ) e' →
    □ ({E,E;Δ;<[x:=τ1]>(<[f:=TArrow τ1 τ2]>Γ)} ⊨ e ≤log≤ e' : τ2) -∗
    {E,E;Δ;Γ} ⊨ Rec f x e ≤log≤ Rec f x e' : TArrow τ1 τ2.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (??) "#Ht".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=". cbn.
    iDestruct (interp_env_dom with "HΓ") as %Hdom.
    (* TODO: how to get rid of/ simplify those proofs? *)
    assert (Closed (x :b: f :b: ∅)
              (subst_p (delete f (delete x (fst <$> vvs))) e)).
    { eapply subst_p_closes; eauto.
      rewrite ?dom_delete_binder Hdom.
      rewrite dom_fmap.
      destruct x as [|x], f as [|f]; cbn-[union difference].
      + set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union.
        set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union.
        set_solver.
      + rewrite ?(right_id ∅ union).
        rewrite (comm union {[x]} {[f]}) !assoc.
        rewrite difference_union.
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
        rewrite difference_union.
        set_solver. }
    assert (Closed (x :b: f :b: ∅)
              (subst_p (delete f (delete x (snd <$> vvs))) e')).
    { eapply subst_p_closes; eauto.
      rewrite ?dom_delete_binder Hdom.
      rewrite dom_fmap.
      destruct x as [|x], f as [|f]; cbn-[union difference].
      + set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union.
        set_solver.
      + rewrite difference_empty.
        rewrite assoc. rewrite difference_union.
        set_solver.
      + rewrite ?(right_id ∅ union).
        rewrite (comm union {[x]} {[f]}) !assoc.
        rewrite difference_union.
        rewrite -!assoc (comm union {[f]} {[x]}) !assoc.
        rewrite difference_union.
        set_solver.
    }
    iModIntro. value_case'; eauto.
    { rewrite decide_left; eauto. }
    iExists (RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e')). iIntros "{$Hj} !#".
    iLöb as "IH". iIntros ([v v']) "#Hiv". simpl. iIntros (j' K') "Hj".
    iModIntro. simpl.
    iApply (wp_rec _ f x (subst_p _ e)); eauto 2 using to_of_val. iNext.
    iApply fupd_wp.
    tp_rec j'.
    pose (vvs':=(<[x:=(v,v')]>(<[f:=(RecV f x (subst_p (delete f (delete x (fst <$> vvs))) e), RecV f x (subst_p (delete f (delete x (snd <$> vvs))) e'))]>vvs))).
    iAssert (interp_env (<[x:=τ1]> (<[f:=TArrow τ1 τ2]> Γ)) ⊤ ⊤ Δ vvs') as "#HΓ'".
    { unfold vvs'. destruct f as [|f], x as [|x]; cbn; eauto;
      rewrite -?interp_env_cons -?Hdom; eauto. }
    iSpecialize ("Ht" with "Hs [HΓ']"); eauto.
    iSpecialize ("Ht" $! j' K').
    rewrite {2}/vvs' /env_subst.
    rewrite !fmap_insert' /=.
    rewrite subst_p_insert.
    rewrite !subst_p_insert /=.
    unfold env_subst in *.
    erewrite !subst_p_delete; auto. (* TODO: [auto] solve the [Closed] goal, but [solve_closed] does not *)
    rewrite !(delete_commute_binder _ x f).
    iApply (fupd_mask_mono E); auto.
    iApply ("Ht" with "Hj").
  Qed.

  Lemma bin_log_related_injl Δ Γ e e' τ1 τ2 :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ1 -∗
    {E,E;Δ;Γ} ⊨ InjL e ≤log≤ InjL e' : (TSum τ1 τ2).
  Proof.
    iIntros (?) "IH".
    rel_bind_ap e e' "IH" v v' "Hvv".
    value_case.
    iLeft. iExists (_,_); eauto.
  Qed.

  Lemma bin_log_related_injr Δ Γ e e' τ1 τ2 :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ2 -∗
    {E,E;Δ;Γ} ⊨ InjR e ≤log≤ InjR e' : TSum τ1 τ2.
  Proof.
    iIntros (?) "IH".
    rel_bind_ap e e' "IH" v v' "Hvv".
    value_case.
    iRight. iExists (_,_); eauto.
  Qed.

  Lemma bin_log_related_case Δ Γ e0 e1 e2 e0' e1' e2' τ1 τ2 τ3 :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e0 ≤log≤ e0' : TSum τ1 τ2 -∗
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TArrow τ1 τ3 -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TArrow τ2 τ3 -∗
    {E,E;Δ;Γ} ⊨ Case e0 e1 e2 ≤log≤ Case e0' e1' e2' : τ3.
  Proof.
    iIntros (?) "IH1 IH2 IH3".
    rel_bind_ap e0 e0' "IH1" v0 v0' "IH1".
    iDestruct "IH1" as "[Hiv|Hiv]";
    iDestruct "Hiv" as ([w w']) "[% #Hw]"; simplify_eq/=;
      rel_case_l; rel_case_r.
    - iApply (bin_log_related_app with "IH2").
      value_case.
    - iApply (bin_log_related_app with "IH3").
      value_case.
  Qed.

  Lemma bin_log_related_if Δ Γ e0 e1 e2 e0' e1' e2' τ :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e0 ≤log≤ e0' : TBool -∗
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : τ -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ -∗
    {E,E;Δ;Γ} ⊨ If e0 e1 e2 ≤log≤ If e0' e1' e2' : τ.
  Proof.
    iIntros (?) "IH1 IH2 IH3".
    rel_bind_ap e0 e0' "IH1" v0 v0' "IH1".
    iDestruct "IH1" as ([]) "[% %]"; simplify_eq/=;
      rel_if_l; rel_if_r; iAssumption.
  Qed.

  Lemma bin_log_related_nat_binop Δ Γ op e1 e2 e1' e2' τ :
    ↑ logrelN ⊆ E →
    binop_nat_res_type op = Some τ →
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TNat -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TNat -∗
    {E,E;Δ;Γ} ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : τ.
  Proof.
    iIntros (? Hopτ) "IH1 IH2".
    rel_bind_ap e1 e1' "IH1" v1 v1' "IH1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "IH2".
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
    destruct (binop_nat_typed_safe op n n' _ Hopτ) as [v' Hopv'].
    rel_op_l; eauto.
    rel_op_r; eauto.
    value_case.
    destruct op; simpl in Hopv'; simplify_eq/=; try destruct eq_nat_dec; try destruct le_dec;
      try destruct lt_dec; eauto.
  Qed.

  Lemma bin_log_related_bool_binop Δ Γ op e1 e2 e1' e2' τ :
    ↑ logrelN ⊆ E →
    binop_bool_res_type op = Some τ →
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TBool -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : TBool -∗
    {E,E;Δ;Γ} ⊨ BinOp op e1 e2 ≤log≤ BinOp op e1' e2' : τ.
  Proof.
    iIntros (? Hopτ) "IH1 IH2".
    rel_bind_ap e1 e1' "IH1" v1 v1' "IH1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "IH2".
    iDestruct "IH1" as (n) "[% %]"; simplify_eq/=.
    iDestruct "IH2" as (n') "[% %]"; simplify_eq/=.
    destruct (binop_bool_typed_safe op n n' _ Hopτ) as [v' Hopv'].
    rel_op_l; eauto.
    rel_op_r; eauto.
    value_case.
    destruct op; simpl in Hopv'; simplify_eq/=; eauto.
  Qed.

  Lemma bin_log_related_tlam Δ Γ e e' τ :
    Closed (dom _ Γ) e →
    Closed (dom _ Γ) e' →
    ↑ logrelN ⊆ E →
    (∀ (τi : D), ⌜∀ ww, PersistentP (τi ww)⌝ → □ ({E,E;(τi::Δ);Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨ e ≤log≤ e' : τ)) -∗
    {E,E;Δ;Γ} ⊨ TLam e ≤log≤ TLam e' : TForall τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (???) "#IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    iDestruct (interp_env_dom with "HΓ") as %Hdom.
    assert (Closed ∅ (env_subst (fst <$> vvs) e)).
    { eapply subst_p_closes; eauto. rewrite dom_fmap Hdom. rewrite right_id. reflexivity. }
    assert (Closed ∅ (env_subst (snd <$> vvs) e')).
    { eapply subst_p_closes; eauto. rewrite dom_fmap Hdom. rewrite right_id. reflexivity. }
    value_case'. rewrite decide_left; eauto.
    iExists (TLamV (env_subst (snd <$> vvs) e')). cbn.
    iFrame "Hj". iAlways.
    iIntros (τi ? j' K') "Hv /=".
    iApply wp_tlam; eauto. iModIntro; iNext; iApply fupd_wp.
    tp_tlam j'; eauto.
    iSpecialize ("IH" $! τi with "[] Hs [HΓ]"); auto.
    { by rewrite interp_env_ren. }
    iSpecialize ("IH" with "Hv").
    iApply (fupd_mask_mono E); eauto.
  Qed.

  Lemma bin_log_related_tapp' Δ Γ e e' τ τ' :
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TForall τ -∗
    {E,E;Δ;Γ} ⊨ TApp e ≤log≤ TApp e' : τ.[τ'/].
  Proof.
    iIntros "IH".
    rel_bind_ap e e' "IH" v v' "IH".
    iSpecialize ("IH" $! (interp ⊤ ⊤ τ' Δ) with "[#]"); [iPureIntro; apply _|].
    iApply (related_ret ⊤).
    iApply (interp_expr_subst Δ τ τ' (TApp v, TApp v')  with "IH").
  Qed.

  Lemma bin_log_related_tapp (τi : D) Δ Γ e e' τ :
    (∀ ww, PersistentP (τi ww)) →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TForall τ -∗
    {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨ TApp e ≤log≤ TApp e' : τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    wp_bind (env_subst _ e).
    tp_bind j (env_subst _ e').
    iSpecialize ("IH" with "Hs [HΓ] Hj").
    { by rewrite interp_env_ren. }
    iMod "IH" as "IH /=". iModIntro.
    iApply (wp_wand with "IH").
    iIntros (v). iDestruct 1 as (v') "[Hj #IH]".
    iSpecialize ("IH" $! τi with "[]"); auto.
    unfold interp_expr.
    iMod ("IH" with "Hj") as "IH /=".
    done.
  Qed.

  Lemma bin_log_related_fold Δ Γ e e' τ :
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ.[(TRec τ)/] -∗
    {E,E;Δ;Γ} ⊨ Fold e ≤log≤ Fold e' : TRec τ.
  Proof.
    iIntros "IH".
    rel_bind_ap e e' "IH" v v' "IH".
    value_case.
    rewrite fixpoint_unfold /= -interp_subst.
    iExists (_, _); eauto.
  Qed.

  Lemma bin_log_related_unfold Δ Γ e e' τ :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TRec τ -∗
    {E,E;Δ;Γ} ⊨ Unfold e ≤log≤ Unfold e' : τ.[(TRec τ)/].
  Proof.
    iIntros (?) "IH".
    rel_bind_ap e e' "IH" v v' "IH".
    rewrite /= fixpoint_unfold /=.
    change (fixpoint _) with (interp ⊤ ⊤ (TRec τ) Δ).
    iDestruct "IH" as ([w w']) "#[% Hiz]"; simplify_eq/=.
    rel_unfold_l.
    rel_unfold_r.
    value_case. by rewrite -interp_subst.
  Qed.

  Lemma bin_log_related_pack' Δ Γ e e' τ τ' :
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ.[τ'/] -∗
    {E,E;Δ;Γ} ⊨ Pack e ≤log≤ Pack e' : TExists τ.
  Proof.
    iIntros "IH".
    rel_bind_ap e e' "IH" v v' "#IH".
    value_case.
    iExists (v, v'). simpl; iSplit; eauto.
    iExists (⟦ τ' ⟧ Δ).
    iSplit; eauto. iPureIntro. apply _.
    by rewrite interp_subst.
  Qed.

  Lemma bin_log_related_pack (τi : D) Δ Γ e e' τ :
    (∀ ww, PersistentP (τi ww)) →
    {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨ e ≤log≤ e' : τ -∗
    {E,E;Δ;Γ} ⊨ Pack e ≤log≤ Pack e' : TExists τ.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    wp_bind (env_subst _ e).
    tp_bind j (env_subst _ e').
    iSpecialize ("IH" with "Hs [HΓ] Hj").
    { by rewrite interp_env_ren. }
    iMod "IH" as "IH /=". iModIntro.
    iApply (wp_wand with "IH").
    iIntros (v). iDestruct 1 as (v') "[Hj #IH]".
    value_case'.
    iExists (PackV v'). simpl. iFrame.
    iExists (v, v'). simpl; iSplit; eauto.
  Qed.

  Lemma bin_log_related_unpack Δ Γ e1 e1' e2 e2' τ τ2
    (Hmasked : ↑ logrelN ⊆ E) :
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : TExists τ -∗
    (∀ τi : D, ⌜∀ ww, PersistentP (τi ww)⌝ →
      {E,E;τi::Δ;Autosubst_Classes.subst (ren (+1)) <$> Γ} ⊨
        e2 ≤log≤ e2' : TArrow τ (Autosubst_Classes.subst (ren (+1)) τ2)) -∗
    {E,E;Δ;Γ} ⊨ Unpack e1 e2 ≤log≤ Unpack e1' e2' : τ2.
  Proof.
    rewrite bin_log_related_eq.
    iIntros "IH1 IH2".
    iIntros (vvs ρ) "#Hs #HΓ"; iIntros (j K) "Hj /=".
    smart_bind j (env_subst _ e1) (env_subst _ e1') "IH1" v v' "IH1".
    iDestruct "IH1" as ([w w']) "[% #Hτi]"; simplify_eq/=.
    iDestruct "Hτi" as (τi) "[% #Hτi]"; simplify_eq/=.
    iApply wp_pack; eauto. iNext.
    iApply fupd_wp.
    tp_pack j; eauto. iModIntro.
    iSpecialize ("IH2" $! τi with "[] Hs [HΓ]"); auto.
    { by rewrite interp_env_ren. }
    tp_bind j (env_subst (snd <$> vvs) e2').
    iApply fupd_wp. iApply (fupd_mask_mono E); eauto.
    iMod ("IH2" with "Hj") as "IH2". simpl.
    wp_bind (env_subst (fst <$> vvs) e2).
    iApply (wp_wand with "IH2"). iModIntro.
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
    iSpecialize ("Hvv'" $! (w,w') with "Hτi Hj"). simpl.
    iMod "Hvv'".
    iApply (wp_wand with "Hvv'"). clear v v'.
    iIntros (v). iDestruct 1 as (v') "[Hj #Hvv']".
    rewrite (interp_weaken [] [τi] Δ _ _ τ2) /=.
    eauto.
  Qed.

  Lemma bin_log_related_fork Δ Γ e e' :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : TUnit -∗
    {E,E;Δ;Γ} ⊨ Fork e ≤log≤ Fork e' : TUnit.
  Proof.
    rewrite bin_log_related_eq.
    iIntros (?) "IH".
    iIntros (vvs ρ) "#Hs HΓ"; iIntros (j K) "Hj /=".
    tp_fork j as i "Hi". fold subst_p.  iModIntro.
    iApply wp_fork. fold subst_p. iNext. iSplitL "Hj".
    - iExists #(); eauto.
    - iSpecialize ("IH" with "Hs HΓ").
      iSpecialize ("IH" $! i []). simpl.
      iSpecialize ("IH" with "Hi").
      iApply fupd_wp. iApply (fupd_mask_mono E); eauto.
      iMod "IH". iApply (wp_wand with "IH"). eauto.
  Qed.

  Lemma bin_log_related_alloc Δ Γ e e' τ :
    ↑ logrelN ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : τ -∗
    {E,E;Δ;Γ} ⊨ Alloc e ≤log≤ Alloc e' : Tref τ.
  Proof.
    iIntros (?) "IH".
    rel_bind_ap e e' "IH" v v' "IH".
    rel_alloc_l as l "Hl".
    rel_alloc_r as k "Hk".
    iMod (inv_alloc (logN .@ (l,k)) _ (∃ w : val * val,
      l ↦ᵢ w.1 ∗ k ↦ₛ w.2 ∗ interp _ _ τ Δ w)%I with "[Hl Hk IH]") as "HN"; eauto.
    { iNext. iExists (v, v'); simpl; iFrame. }
    rel_vals.
    iExists (l, k). eauto.
  Qed.

  Lemma bin_log_related_load Δ Γ e e' τ :
    ↑logrelN  ⊆ E →
    {E,E;Δ;Γ} ⊨ e ≤log≤ e' : (Tref τ) -∗
    {E,E;Δ;Γ} ⊨ Load e ≤log≤ Load e' : τ.
  Proof.
    iIntros (?) "IH".
    rel_bind_ap e e' "IH" v v' "IH".
    iDestruct "IH" as ([l l']) "[% Hinv]"; simplify_eq/=.
    rel_load_l_atomic.
    iInv (logN .@ (l,l')) as ([w w']) "[Hw1 [>Hw2 #Hw]]" "Hclose"; simpl.
    iModIntro. iExists _; iFrame "Hw1".
    iNext. iIntros "Hw1".
    rel_load_r.
    iMod ("Hclose" with "[Hw1 Hw2]").
    { iNext. iExists (w,w'); by iFrame. }
    rel_vals; eauto.
  Qed.

  Lemma bin_log_related_store Δ Γ e1 e2 e1' e2' τ :
    ↑logrelN  ⊆ E →
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : (Tref τ) -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ -∗
    {E,E;Δ;Γ} ⊨ Store e1 e2 ≤log≤ Store e1' e2' : TUnit.
  Proof.
    iIntros (?) "IH1 IH2".
    rel_bind_ap e1 e1' "IH1" v v' "IH1".
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
    rel_bind_ap e2 e2' "IH2" w w' "IH2".
    rel_store_l_atomic.
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
    iModIntro. iExists _; iFrame "Hv1".
    iNext. iIntros "Hw1".
    rel_store_r.
    iMod ("Hclose" with "[Hw1 Hv2 IH2]").
    { iNext; iExists (_, _); simpl; iFrame. }
    by rel_vals.
  Qed.

  Lemma bin_log_related_CAS Δ Γ e1 e2 e3 e1' e2' e3' τ
    (HEqτ : EqType τ) :
    ↑logrelN  ⊆ E →
    {E,E;Δ;Γ} ⊨ e1 ≤log≤ e1' : Tref τ -∗
    {E,E;Δ;Γ} ⊨ e2 ≤log≤ e2' : τ -∗
    {E,E;Δ;Γ} ⊨ e3 ≤log≤ e3' : τ -∗
    {E,E;Δ;Γ} ⊨ CAS e1 e2 e3 ≤log≤ CAS e1' e2' e3' : TBool.
  Proof.
    iIntros (?) "IH1 IH2 IH3".
    rel_bind_ap e1 e1' "IH1" v1 v1' "#IH1".
    rel_bind_ap e2 e2' "IH2" v2 v2' "#IH2".
    rel_bind_ap e3 e3' "IH3" v3 v3' "#IH3".
    iDestruct "IH1" as ([l l']) "[% Hinv]"; simplify_eq/=.
    rel_cas_l_atomic.
    iInv (logN .@ (l,l')) as ([v v']) "[Hv1 [>Hv2 #Hv]]" "Hclose".
    iPoseProof ("Hv") as "Hv' /=".
    rewrite {2}[interp _ _ τ Δ (v, v')]interp_EqType_agree; trivial.
    iMod "Hv'" as %Hv'; subst.
    iModIntro. iExists _; iFrame. simpl.
    destruct (decide (v' = v2)) as [|Hneq]; subst.
    - iSplitR; first by (iIntros (?); contradiction).
      iIntros (?). iNext. iIntros "Hv1".
      iApply fupd_logrel'.
      iAssert (▷ ⌜v2 = v2'⌝)%I with "[IH2]" as ">%".
      { rewrite ?interp_EqType_agree; trivial. }
      iModIntro.
      rel_cas_suc_r.
      iMod ("Hclose" with "[-]").
      { iNext; iExists (_, _); by iFrame. }
      rel_vals; eauto.
    - iSplitL; last by (iIntros (?); congruence).
      iIntros (?). iNext. iIntros "Hv1".
      iApply fupd_logrel'.
      iAssert (▷ ⌜v' ≠ v2'⌝)%I as ">%".
      { rewrite ?interp_EqType_agree; trivial. iSimplifyEq. auto. }
      iModIntro.
      rel_cas_fail_r.
      iMod ("Hclose" with "[-]").
      { iNext; iExists (_, _); by iFrame. }
      rel_vals; eauto.
  Qed.

  Theorem binary_fundamental_masked Δ Γ e τ :
    ↑logrelN ⊆ E →
    Γ ⊢ₜ e : τ → ({E,E;Δ;Γ} ⊨ e ≤log≤ e : τ)%I.
  Proof.
    intros HlogN Ht. iInduction Ht as [] "IH" forall (Δ).
    - by iApply bin_log_related_var.
    - iApply bin_log_related_unit.
    - by iApply bin_log_related_nat.
    - by iApply bin_log_related_bool.
    - by iApply (bin_log_related_nat_binop with "[]").
    - by iApply (bin_log_related_bool_binop with "[]").
    - by iApply (bin_log_related_pair with "[]").
    - by iApply bin_log_related_fst.
    - by iApply bin_log_related_snd.
    - by iApply bin_log_related_injl.
    - by iApply bin_log_related_injr.
    - by iApply (bin_log_related_case with "[] []").
    - by iApply (bin_log_related_if with "[] []").
    - assert (Closed (x :b: f :b: dom (gset string) Γ) e).
      { apply typed_X_closed in Ht.
        rewrite !dom_insert_binder in Ht.
        revert Ht. destruct x,f; cbn-[union];
        (* TODO: why is simple rewriting is not sufficient here? *)
        erewrite ?(left_id ∅); eauto.
        all: apply _. }
      iApply (bin_log_related_rec with "[]"); eauto.
    - by iApply (bin_log_related_app with "[] []").
    - assert (Closed (dom _ Γ) e).
      { apply typed_X_closed in Ht.
        pose (K:=(dom_fmap (Autosubst_Classes.subst (ren (+1))) Γ)).
        fold_leibniz. by rewrite -K. }
      iApply bin_log_related_tlam; eauto.
    - by iApply bin_log_related_tapp'.
    - by iApply bin_log_related_fold.
    - by iApply bin_log_related_unfold.
    - by iApply bin_log_related_pack'.
    - iApply (bin_log_related_unpack with "[]"); eauto.
    - by iApply bin_log_related_fork.
    - by iApply bin_log_related_alloc.
    - by iApply bin_log_related_load.
    - by iApply (bin_log_related_store with "[]").
    - by iApply (bin_log_related_CAS with "[] []").
  Qed.
End masked.

Theorem binary_fundamental Δ Γ e τ :
  Γ ⊢ₜ e : τ → ({⊤,⊤;Δ;Γ} ⊨ e ≤log≤ e : τ)%I.
Proof. by eapply binary_fundamental_masked. Qed.

End fundamental.