Reorganize the rules in rules.v

theories/logrel/logrel_binary.v

@@ -222,24 +222,6 @@ Section related_facts.
     by iMod "HL".
   Qed.
 
-  Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 (τ : type) :
-    {Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗
-    {τi::Δ;⤉Γ} ⊨ 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.
-
 End related_facts.
 
 (** Monadic-like operations on logrel *)

theories/logrel/rules.v

@@ -12,19 +12,9 @@ Section properties.
   Implicit Types Δ : listC D.
   Hint Resolve to_of_val.
 
-  (** * Lemmas to show that binary logical model is closed under
-  (forward) reductions. *)
-  
-  Lemma bin_log_related_val Δ Γ E e e' τ v v' :
-    to_val e = Some v →
-    to_val e' = Some v' →
-    (|={E}=> ⟦ τ ⟧ Δ (v, v')) ⊢ {E;Δ;Γ} ⊨ e ≤log≤ e' : τ.
-  Proof.
-    iIntros (He He') "Hτ".
-    iMod "Hτ" as "Hτ".
-    rewrite (interp_ret E); eauto.
-    by rewrite -related_ret.
-  Qed.
+  (** * Primitive rules *)
+
+  (** [fupd_logrel] is defined in [logrel_binary.v] *)
 
   Lemma bin_log_related_arrow_val Δ Γ E (f x f' x' : binder) (e e' eb eb' : expr) (τ τ' : type) :
     e = (rec: f x := eb)%E →
@@ -48,7 +38,7 @@ Section properties.
     iExists (RecV f' x' eb').
     iFrame "Hj". iAlways. iIntros ([v1 v2]) "Hvv".
     iSpecialize ("H" $! v1 v2 with "Hvv Hs []").
-    { iAlways. iApply "HΓ". }    
+    { iAlways. iApply "HΓ". }
     assert (Closed ∅ ((rec: f x := eb) v1)).
     { unfold Closed in *. simpl.
       intros. split_and?; auto. apply of_val_closed. }
@@ -58,21 +48,22 @@ Section properties.
     rewrite /env_subst. rewrite !Closed_subst_p_id. done.
   Qed.
 
-  Lemma bin_log_related_arrow Δ Γ E (f x f' x' : binder) (f1 f2 eb eb' : expr) (τ τ' : type) :
-    f1 = (rec: f x := eb)%E →
-    f2 = (rec: f' x' := eb')%E →
-    Closed ∅ f1 →
-    Closed ∅ f2 →
-    □(∀ (v1 v2 : val), □ ({Δ;Γ} ⊨ v1 ≤log≤ v2 : τ) -∗
-      {Δ;Γ} ⊨ f1 v1 ≤log≤ f2 v2 : τ') -∗
-    {E;Δ;Γ} ⊨ f1 ≤log≤ f2 : TArrow τ τ'.
+  Lemma bin_log_related_weaken_2 τi Δ Γ e1 e2 (τ : type) :
+    {Δ;Γ} ⊨ e1 ≤log≤ e2 : τ -∗
+    {τi::Δ;⤉Γ} ⊨ e1 ≤log≤ e2 : τ.[ren (+1)].
   Proof.
-    iIntros (????) "#H".
-    iApply bin_log_related_arrow_val; eauto.
-    iAlways. iIntros (v1 v2) "#Hvv".
-    iApply "H". iAlways.
-    iApply (related_ret ⊤).
-    by iApply interp_ret.
+    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.
 
   Lemma bin_log_related_spec_ctx Δ Γ E1 E2 e e' τ ℶ :
@@ -96,9 +87,22 @@ Section properties.
     iApply (Hp with "Hctx Hρ").
   Qed.
 
-  (** ** Reductions on the left *)
-  (** *** Lifting of the pure reductions *)
-  Lemma bin_log_pure_l Δ (Γ : stringmap type) (E : coPset) 
+  (** ** Monadic rules *)
+  (* TODO this is not actually primitive; insert the monadic rules here *)
+  Lemma bin_log_related_val Δ Γ E e e' τ v v' :
+    to_val e = Some v →
+    to_val e' = Some v' →
+    (|={E}=> ⟦ τ ⟧ Δ (v, v')) ⊢ {E;Δ;Γ} ⊨ e ≤log≤ e' : τ.
+  Proof.
+    iIntros (He He') "Hτ".
+    iMod "Hτ" as "Hτ".
+    rewrite (interp_ret E); eauto.
+    by rewrite -related_ret.
+  Qed.
+
+  (** ** Forward reductions on the LHS *)
+
+  Lemma bin_log_pure_l Δ (Γ : stringmap type) (E : coPset)
     (K' : list ectx_item) (e e' t : expr) (τ : type)
     (Hsafe' : ∀ σ, reducible e σ)
     (Hdet' : ∀ σ1 e2 σ2 efs, prim_step e σ1 e2 σ2 efs -> σ1=σ2 /\ e'=e2 /\ efs = []) :
@@ -127,7 +131,7 @@ Section properties.
     iModIntro. iNext. iModIntro. simpl; iSplitL; last done.
     iSpecialize ("IH" with "Hs [HΓ] Hj"); auto. simpl.
     rewrite /env_subst fill_subst.
-    iApply wp_bind_inv. 
+    iApply wp_bind_inv.
     iApply fupd_wp. by iApply (fupd_mask_mono E).
   Qed.
 
@@ -147,9 +151,9 @@ Section properties.
     assert (to_val (subst_p (fst <$> vvs) e) = None) as Hval.
     { destruct (Hsafe ∅) as [e2 [σ2 [efs Hs]]].
       by eapply language.val_stuck. }
-    iApply (wp_bind (subst_ctx _ K')). 
-    iMod ("IH" with "Hs [HΓ] Hj") as "IH"; auto. 
-    iModIntro.    
+    iApply (wp_bind (subst_ctx _ K')).
+    iMod ("IH" with "Hs [HΓ] Hj") as "IH"; auto.
+    iModIntro.
     iApply wp_lift_pure_det_step; eauto.
     { apply subst_p_det; eauto.
       - intros σ. destruct (Hsafe' σ) as (e2' & σ2' & efs & Hsafez).
@@ -162,136 +166,7 @@ Section properties.
     rewrite /env_subst fill_subst /=.
     by iApply wp_bind_inv.
   Qed.
- 
-  (* TODO: I have to 'refine' here for some reason *)
-  Local Ltac solve_red H :=
-    iApply (bin_log_pure_l with H); auto;
-    [ intros; apply pure_exec_safe 
-    | intros ???? Hst;
-      refine (@pure_exec_puredet F_mu_ref_conc_lang _ _ _ _ _ _ _ _ _ Hst)
-    ]; eauto.
-  Local Ltac solve_red_masked H :=
-    iApply (bin_log_pure_masked_l with H); auto;
-    [ intros; apply pure_exec_safe 
-    | intros ???? Hst;
-      refine (@pure_exec_puredet F_mu_ref_conc_lang _ _ _ _ _ _ _ _ _ Hst)
-    ]; eauto.
-
-  Lemma bin_log_related_fst_l Δ Γ E K v1 v2 e τ :
-   ▷ ({E;Δ;Γ} ⊨ fill K (of_val v1) ≤log≤ e : τ)
-   ⊢ {E;Δ;Γ} ⊨ fill K (Fst (Pair (of_val v1) (of_val v2))) ≤log≤ e : τ.
-  Proof.
-    iIntros "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_snd_l Δ Γ E K v1 v2 e τ :
-   ▷ ({E;Δ;Γ} ⊨ (fill K (of_val v2)) ≤log≤ e : τ)
-   ⊢ {E;Δ;Γ} ⊨ (fill K (Snd (Pair (of_val v1) (of_val v2)))) ≤log≤ e : τ.
-  Proof.
-    iIntros "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_rec_l Δ Γ E K (f x : binder) e e' v t τ
-   (Hclosed : Closed (x :b: f :b: ∅) e) :
-   (to_val e' = Some v) →
-   ▷ ({E;Δ;Γ} ⊨ (fill K (subst' f (Rec f x e) (subst' x e' e))) ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ (fill K (App (Rec f x e) e')) ≤log≤ t : τ.
-  Proof.
-    iIntros (?) "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_tlam_l Δ Γ E K e t τ
-   (Hclosed : Closed ∅ e) :
-   ▷ ({E;Δ;Γ} ⊨ fill K e ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ (fill K (TApp (TLam e))) ≤log≤ t : τ.
-  Proof.
-    iIntros "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_fold_l Δ Γ E K e v t τ :
-   (to_val e = Some v) →
-   ▷ ({E;Δ;Γ} ⊨ fill K e ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ (fill K (Unfold (Fold e))) ≤log≤ t : τ.
-  Proof.
-    iIntros (?) "Hlog".
-    solve_red "Hlog".
-  Qed.
-  
-  Lemma bin_log_related_pack_l Δ Γ E K e e' v t τ :
-   to_val e = Some v →
-   ▷ ({E;Δ;Γ} ⊨ fill K (App e' e) ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ fill K (Unpack (Pack e) e') ≤log≤ t : τ.
-  Proof.
-    iIntros (?) "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_case_inl_l Δ Γ E K e v e1 e2 t τ :
-   to_val e = Some v →
-   ▷ ({E;Δ;Γ} ⊨ fill K (App e1 e) ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ fill K (Case (InjL e) e1 e2) ≤log≤ t : τ.
-  Proof.
-    iIntros (?) "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_case_inr_l Δ Γ E K e v e1 e2 t τ :
-   to_val e = Some v →
-   ▷ ({E;Δ;Γ} ⊨ fill K (App e2 e) ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ fill K (Case (InjR e) e1 e2) ≤log≤ t : τ.
-  Proof.
-    iIntros (?) "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_if_true_l Δ Γ E K e1 e2 t τ :
-   ▷ ({E;Δ;Γ} ⊨ fill K e1 ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ fill K (If #true e1 e2) ≤log≤ t : τ.
-  Proof.
-    iIntros "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_if_true_masked_l Δ Γ E1 E2 K e1 e2 t τ :
-   ({E1,E2;Δ;Γ} ⊨ fill K e1 ≤log≤ t : τ)
-   ⊢ {E1,E2;Δ;Γ} ⊨ fill K (If #true e1 e2) ≤log≤ t : τ.
-  Proof.
-    iIntros "Hlog".
-    solve_red_masked "Hlog".
-  Qed.
-
-  Lemma bin_log_related_if_false_l Δ Γ E K e1 e2 t τ :
-   ▷ ({E;Δ;Γ} ⊨ fill K e2 ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ (fill K (If #false e1 e2)) ≤log≤ t : τ.
-  Proof.
-    iIntros "Hlog".
-    solve_red "Hlog".
-  Qed.
-
-  Lemma bin_log_related_if_false_masked_l Δ Γ E1 E2 K e1 e2 t τ :
-   ({E1,E2;Δ;Γ} ⊨ fill K e2 ≤log≤ t : τ)
-   ⊢ {E1,E2;Δ;Γ} ⊨ (fill K (If #false e1 e2)) ≤log≤ t : τ.
-  Proof.
-    iIntros "Hlog".
-    solve_red_masked "Hlog".
-  Qed.
-
-  Lemma bin_log_related_binop_l Δ Γ E K op e1 e2 v1 v2 v t τ :
-    to_val e1 = Some v1 →
-    to_val e2 = Some v2 →
-    binop_eval op v1 v2 = Some v →
-   ▷ ({E;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ t : τ)
-   ⊢ {E;Δ;Γ} ⊨ (fill K (BinOp op e1 e2)) ≤log≤ t : τ.
-  Proof.
-    iIntros (???) "Hlog".
-    solve_red "Hlog".
-  Qed.
 
-  (** *** Stateful reductions *)
   Lemma bin_log_related_wp_l Δ Γ E K e1 e2 τ
    (Hclosed1 : Closed ∅ e1) :
    (WP e1 @ E {{ v,
@@ -337,217 +212,314 @@ Section properties.
     by iMod "Hlog".
   Qed.
 
-  Lemma bin_log_related_step_atomic_l {A} (Φ : A → val → iProp Σ) Δ Γ E1 E2 K e1 e2 τ
-    (Hatomic : Atomic e1)
-    (Hclosed1 : Closed ∅ e1) :
-    (|={E1,E2}=> ∃ a : A, WP e1 @ E2 {{ v, Φ a v }} ∗
-    (∀ v, Φ a v -∗ {E2,E1;Δ;Γ} ⊨ fill K (of_val v) ≤log≤ e2 : τ)) -∗
-    {E1;Δ;Γ} ⊨ fill K e1 ≤log≤ e2 : τ.
-  Proof.
-    iIntros "Hlog".
-    iApply bin_log_related_wp_atomic_l; auto.
-    iMod "Hlog" as (a) "[He Hlog]". iModIntro.
-    iApply (wp_wand with "He").
-    iIntros (v) "HΦ".
-    iApply ("Hlog" with "HΦ").
-  Qed.
-
-  (* TODO: simplify this monstrosity *)
-  Ltac rewrite_closed :=
-    try (let F := fresh in
-      intro F); simpl;
-       repeat match goal with
-        | [ |- Closed ∅ _] => rewrite /Closed; cbn
-        | [ |- Is_true (is_closed ∅ (of_val ?v))] => eapply of_val_closed
-        | [ |- Is_true (is_closed _ _ && is_closed _ _)]
-          => split_and?        
-        | [Hval : to_val ?e = Some ?v |- context[is_closed ∅ ?e] ] 
-          => rewrite -?(of_to_val e v Hval); eauto
-        | [Hval : to_val ?e = Some ?v |- Is_true (is_closed ∅ ?e) ]
-          => rewrite -?(of_to_val e v Hval); eauto
-        | [Hcl : Closed ∅ ?e |- context[env_subst _ ?e]]
-          => rewrite /env_subst Closed_subst_p_id
-        | [Hcl : Closed ∅ ?e |- context[subst_p _ ?e]]
-          => rewrite Closed_subst_p_id
-        end;
-      try done.
+  (** ** Forward reductions on the RHS *)
 
-  Lemma bin_log_related_fork_l Δ Γ E1 E2 K (e t : expr) (τ : type)
-   (Hclosed : Closed ∅ e) :
-   (|={E1,E2}=> ▷ (WP e {{ _, True }}) ∗
-    {E2,E1;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ) -∗
-   {E1;Δ;Γ} ⊨ fill K (Fork e) ≤log≤ t : τ.
+  Lemma bin_log_pure_r Δ Γ E1 E2 K' e e' t τ
+    (Hspec : nclose specN ⊆ E1) :
+    (∀ σ, prim_step e σ e' σ []) →
+    {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K' e' : τ
+    ⊢ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K' e : τ.
   Proof.
-    iIntros "Hlog".
-    iApply bin_log_related_wp_atomic_l; auto.
-    iMod "Hlog" as "[Hsafe Hlog]". iModIntro.
-    iApply wp_fork. iNext. by iFrame "Hsafe".
+    rewrite bin_log_related_eq /bin_log_related_def.
+    iIntros (Hstep) "Hlog".
+    iIntros (vvs ρ) "#Hs #HΓ".
+    iIntros (j K) "Hj /=".
+    assert (Hsafe : ∀ σ, prim_step (subst_p (snd <$> vvs) e) σ (subst_p (snd <$> vvs) e') σ []).
+    { intros.
+      rewrite -(fmap_nil (subst_p (snd <$> vvs))).
+      by apply subst_p_prim_step. }
+    rewrite /env_subst fill_subst -fill_app.
+    iMod (step_pure _ _ _ _ (subst_p _ e) (env_subst (snd <$> vvs) e') with "[Hs Hj]") as "Hj"; eauto.
+    rewrite fill_app -fill_subst.
+    iDestruct ("Hlog" with "Hs [HΓ] Hj") as "Hlog"; auto.
   Qed.
 
-  Lemma bin_log_related_alloc_l Δ Γ E1 E2 K e v t τ
-    (Heval : to_val e = Some v) :
-    (|={E1,E2}=> ▷ (∀ l : loc, l ↦ᵢ v -∗
-           {E2,E1;Δ;Γ} ⊨ fill K (# l) ≤log≤ t : τ))%I
-    -∗ {E1;Δ;Γ} ⊨ fill K (ref e) ≤log≤ t : τ.
+  (* TODO: This is not described as a primitive rule in the appendix *)
+  Lemma bin_log_related_step_r Φ Δ Γ E1 E2 K' e1 e2 τ
+    (Hclosed2 : Closed ∅ e2) :
+    (∀ ρ j K, spec_ctx ρ -∗ (j ⤇ fill K e2 ={E1}=∗ ∃ v, j ⤇ fill K (of_val v)
+                  ∗ Φ v)) -∗
+    (∀ v, Φ v -∗ {E1,E2;Δ;Γ} ⊨ e1 ≤log≤ fill K' (of_val v) : τ) -∗
+    {E1,E2;Δ;Γ} ⊨ e1 ≤log≤ fill K' e2 : τ.
   Proof.
-    iIntros "Hlog".
-    iApply bin_log_related_wp_atomic_l; auto.
-    iMod "Hlog". iModIntro. 
-    iApply (wp_alloc _ _ v); auto.
+    rewrite bin_log_related_eq.
+    iIntros "He Hlog".
+    iIntros (vvs ρ) "#Hs #HΓ". iIntros (j K) "Hj /=".
+    rewrite /env_subst fill_subst /= -fill_app.
+    rewrite !Closed_subst_p_id.
+    iMod ("He" $! ρ j with "Hs Hj") as (v) "[Hj Hv]".
+    iSpecialize ("Hlog" $! v with "Hv Hs [HΓ]"); first by iFrame.
+    rewrite /env_subst fill_app fill_subst.
+    rewrite of_val_subst_p /=.
+    iSpecialize ("Hlog" with "Hj"); simpl.
+    done.
   Qed.
 
-  Lemma bin_log_related_alloc_l' Δ Γ E K e v t τ
+  Lemma bin_log_related_alloc_r Δ Γ E1 E2 K e v t τ
+    (Hmasked : nclose specN ⊆ E1)
     (Heval : to_val e = Some v) :
-    ▷ (∀ (l : loc), l ↦ᵢ v -∗ {E;Δ;Γ} ⊨ fill K (# l) ≤log≤ t : τ)%I
-    -∗ {E;Δ;Γ} ⊨ fill K (ref e) ≤log≤ t : τ.
+    (∀ l : loc, l ↦ₛ v -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #l : τ)%I
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Alloc e) : τ.
   Proof.
     iIntros "Hlog".
-    iApply (bin_log_related_alloc_l); auto. assumption.
+    pose (Φ := (fun w => ∃ l : loc, ⌜w = (# l)⌝ ∗ l ↦ₛ v)%I).
+    iApply (bin_log_related_step_r Φ with "[]").
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      tp_alloc j as l "Hl". iExists (# l).
+      iFrame. iExists l. eauto. }
+    iIntros (v') "He'". iDestruct "He'" as (l) "[% Hl]". subst.
+    iApply "Hlog".
+    done.
   Qed.
 
-  Lemma bin_log_related_load_l Δ Γ E1 E2 K l q t τ :
-    (|={E1,E2}=> ∃ v',
-      ▷(l ↦ᵢ{q} v') ∗
-      ▷(l ↦ᵢ{q} v' -∗ ({ E2,E1;Δ;Γ } ⊨ fill K (of_val v') ≤log≤ t : τ)))%I
-    -∗ {E1;Δ;Γ} ⊨ fill K (! #l) ≤log≤ t : τ.
+  Lemma bin_log_related_load_r Δ Γ E1 E2 K l q v' t τ
+    (Hmasked : nclose specN ⊆ E1) :
+    l ↦ₛ{q} v' -∗
+    (l ↦ₛ{q} v' -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (of_val v') : τ)
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Load (# l)) : τ.
   Proof.
-    iIntros "Hlog".
-    iApply bin_log_related_wp_atomic_l; auto.
-    iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
-    iApply (wp_load with "Hl"); auto.
+    iIntros "Hl Hlog".
+    pose (Φ := (fun w => ⌜w = v'⌝ ∗ l ↦ₛ{q} v')%I).
+    iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=". iExists v'.
+      tp_load j.
+      iFrame. eauto. }
+    iIntros (v) "[% Hl]"; subst.
+    iApply "Hlog".
+    done.
   Qed.
 
-  Lemma bin_log_related_load_l' Δ Γ E1 K l q v' t τ :
-    ▷ l ↦ᵢ{q} v' -∗
-    ▷ (l ↦ᵢ{q} v' -∗ ({E1;Δ;Γ} ⊨ fill K (of_val v') ≤log≤ t : τ))
-    -∗ {E1;Δ;Γ} ⊨ fill K !#l ≤log≤ t : τ.
-  Proof.
-    iIntros "Hl Hlog".
-    iApply (bin_log_related_load_l); auto.
-    iExists v'.
-    iModIntro.
-    by iFrame.
-  Qed.
-
-  Lemma bin_log_related_store_l Δ Γ E1 E2 K l e v' t τ :
+  Lemma bin_log_related_store_r Δ Γ E1 E2 K l e v v' t τ
+    (Hmasked : nclose specN ⊆ E1) :
     to_val e = Some v' →
-    (|={E1,E2}=> ∃ v, ▷ l ↦ᵢ v ∗
-      ▷(l ↦ᵢ v' -∗ {E2,E1;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ))
-    -∗ {E1;Δ;Γ} ⊨ fill K (#l <- e) ≤log≤ t : τ.
-  Proof.
-    iIntros (?) "Hlog".
-    iApply bin_log_related_wp_atomic_l; auto.
-    iMod "Hlog" as (v) "[Hl Hlog]". iModIntro.
-    iApply (wp_store _ _ _ _ v' with "Hl"); auto.
-  Qed.    
-
-  Lemma bin_log_related_store_l' Δ Γ E K l e v v' t τ :
-    (to_val e = Some v') →
-    ▷ (l ↦ᵢ v) -∗
-    ▷ (l ↦ᵢ v' -∗ {E;Δ;Γ} ⊨ fill K #() ≤log≤ t : τ)
-    -∗ {E;Δ;Γ} ⊨ fill K (#l <- e) ≤log≤ t : τ.
+    l ↦ₛ v -∗
+    (l ↦ₛ v' -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#()) : τ)
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (#l <- e) : τ.
   Proof.
     iIntros (?) "Hl Hlog".
-    iApply (bin_log_related_store_l _ _ _ _ _ l e v'); auto.
-    iModIntro. iExists v. iFrame.
+    pose (Φ := (fun w => ⌜w = #()⌝ ∗ l ↦ₛ v')%I).
+    iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=". iExists #().
+      tp_store j.
+      iFrame. eauto. }
+    iIntros (w) "[% Hl]"; subst.
+    iApply "Hlog".
+    done.
   Qed.
 
-  Lemma bin_log_related_cas_l Δ Γ E1 E2 K l e1 e2 v1 v2 t τ :
+  Lemma bin_log_related_cas_fail_r Δ Γ E1 E2 K l e1 e2 v1 v2 v t τ :
+    nclose specN ⊆ E1 →
     to_val e1 = Some v1 →
     to_val e2 = Some v2 →
-    (|={E1,E2}=> ∃ v', ▷ l ↦ᵢ v' ∗ 
-     (⌜v' ≠ v1⌝ -∗ ▷ (l ↦ᵢ v' -∗ {E2,E1;Δ;Γ} ⊨ fill K #false ≤log≤ t : τ)) ∧
-     (⌜v' = v1⌝ -∗ ▷ (l ↦ᵢ v2 -∗ {E2,E1;Δ;Γ} ⊨ fill K #true ≤log≤ t : τ)))
-    -∗ {E1;Δ;Γ} ⊨ fill K (CAS #l e1 e2) ≤log≤ t : τ.
+    v ≠ v1 →
+    l ↦ₛ v -∗
+    (l ↦ₛ v -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #false : τ)
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (CAS #l e1 e2) : τ.
   Proof.
-    iIntros (??) "Hlog".
-    iApply bin_log_related_wp_atomic_l; auto.
-    iMod "Hlog" as (v') "[Hl Hlog]". iModIntro.
-    destruct (decide (v' = v1)).
-    - (* CAS successful *) subst.
-      iApply (wp_cas_suc with "Hl"); eauto.
-      iDestruct "Hlog" as "[_ Hlog]".
-      iSpecialize ("Hlog" with "[]"); eauto.
-    - (* CAS failed *)
-      iApply (wp_cas_fail with "Hl"); eauto.
-      iDestruct "Hlog" as "[Hlog _]".
-      iSpecialize ("Hlog" with "[]"); eauto.
+    iIntros (????) "Hl Hlog".
+    pose (Φ := (fun (w : val) => ⌜w = #false⌝ ∗ l ↦ₛ v)%I).
+    iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      tp_cas_fail j; auto.
+      iExists #false. simpl.
+      iFrame. eauto. }
+    iIntros (w) "[% Hl]"; subst.
+    iApply "Hlog".
+    done.
   Qed.
 
-  Lemma bin_log_related_cas_fail_l Δ Γ E1 E2 K l e1 e2 v1 v2 t τ :
+  Lemma bin_log_related_cas_suc_r Δ Γ E1 E2 K l e1 e2 v1 v2 v t τ :
+    nclose specN ⊆ E1 →
     to_val e1 = Some v1 →
     to_val e2 = Some v2 →
-    (|={E1,E2}=> ∃ v', ▷ l ↦ᵢ v' ∗ ⌜v' ≠ v1⌝ ∗
-     (l ↦ᵢ v' -∗ {E2,E1;Δ;Γ} ⊨ fill K #false ≤log≤ t : τ))
-    -∗ {E1;Δ;Γ} ⊨ fill K (CAS #l e1 e2) ≤log≤ t : τ.
+    v = v1 →
+    l ↦ₛ v -∗
+    (l ↦ₛ v2 -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #true : τ)
+    -∗ {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (CAS #l e1 e2) : τ.
   Proof.
-    iIntros (??) "Hlog".
-    iApply bin_log_related_wp_atomic_l; auto.
-    iMod "Hlog" as (v') "[Hl [% Hlog]]". iModIntro. 
-    iApply (wp_cas_fail with "Hl"); eauto.
+    iIntros (????) "Hl Hlog".
+    pose (Φ := (fun w => ⌜w = #true⌝ ∗ l ↦ₛ v2)%I).
+    iApply (bin_log_related_step_r Φ with "[Hl]"); eauto.
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      tp_cas_suc j; auto.
+      iExists #true. simpl.
+      iFrame. eauto. }
+    iIntros (w) "[% Hl]"; subst.
+    iApply "Hlog".
+    done.
   Qed.
-  
-  Lemma bin_log_related_cas_fail_l' Δ Γ E K l e1 e2 v1 v2 v' t τ :
-    (to_val e1 = Some v1) →
-    (to_val e2 = Some v2) →
-    (v' ≠ v1) →
-    ▷ (l ↦ᵢ v') -∗
-    (l ↦ᵢ v' -∗ {E;Δ;Γ} ⊨ fill K #false ≤log≤ t : τ)
-    -∗ {E;Δ;Γ} ⊨ fill K (CAS #l e1 e2) ≤log≤ t : τ.
+
+  Lemma bin_log_related_fork_r Δ Γ E1 E2 K (e t : expr) (τ : type)
+   (Hmasked : nclose specN ⊆ E1)
+   (Hclosed : Closed ∅ e) :
+   (∀ i, i ⤇ e -∗
+     {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K #() : τ) -∗
+   {E1,E2;Δ;Γ} ⊨ t ≤log≤ fill K (Fork e) : τ.
   Proof.
-    iIntros (???) "Hl Hlog".
-    iApply bin_log_related_cas_fail_l; eauto.
-    iModIntro. iExists v'. iFrame "Hl Hlog". eauto.
+    iIntros "Hlog".
+    pose (Φ := (fun (v : val) => ∃ i, i ⤇ e ∗ ⌜v = #()⌝%V)%I).
+    iApply (bin_log_related_step_r Φ with "[]"); cbv[Φ].
+    { iIntros (ρ j K') "#Hspec Hj".
+      tp_fork j as i "Hi".
+      iModIntro. iExists #(). iFrame. eauto.
+    }
+    iIntros (v). iDestruct 1 as (i) "[Hi %]"; subst.
+    by iApply "Hlog".
   Qed.
 
-  Lemma bin_log_related_cas_suc_l Δ Γ E1 E2 K l e1 e2 v1 v2 t τ :
-    (to_val e1 = Some v1) →
-    (to_val e2 = Some v2) →
-    (|={E1,E2}=> ▷ (l ↦ᵢ v1) ∗
-     (l ↦ᵢ v2 -∗ {E2,E1;Δ;Γ} ⊨ fill K #true ≤log≤ t : τ))
-    -∗ {E1;Δ;Γ} ⊨ fill K (CAS #l e1 e2) ≤log≤ t : τ.
-  Proof.  
-    iIntros (??) "Hlog".
-    iApply bin_log_related_wp_atomic_l; auto.
-    iMod "Hlog" as "[Hl Hlog]". iModIntro. 
-    iApply (wp_cas_suc with "Hl"); eauto.
+  (** [bin_log_related_var] is in [fundamental_binary.v] *)
+  (** [bin_log_related_rec] is in [fundamental_binary.v] *)
+  (** [bin_log_related_tlam] is in [fundamental_binary.v] *)
+  (** [bin_log_related_tapp] is in [fundamental_binary.v] *)
+  (** [bin_log_related_pack] is in [fundamental_binary.v] *)
+  (** [bin_log_related_unpack] is in [fundamental_binary.v] *)
+  (** [bin_log_related_fork] is in [fundamental_binary.v] *)
+
+  (* -------------------------------------------------- *)
+  (* -------------------------------------------------- *)
+  (** * Derived rules *)
+  (** Derived compatibility rules are in [fundamental_binary.v] *)
+  (* -------------------------------------------------- *)
+  (* -------------------------------------------------- *)
+
+  Lemma bin_log_related_arrow Δ Γ E (f x f' x' : binder) (f1 f2 eb eb' : expr) (τ τ' : type) :
+    f1 = (rec: f x := eb)%E →
+    f2 = (rec: f' x' := eb')%E →
+    Closed ∅ f1 →
+    Closed ∅ f2 →
+    □(∀ (v1 v2 : val), □ ({Δ;Γ} ⊨ v1 ≤log≤ v2 : τ) -∗
+      {Δ;Γ} ⊨ f1 v1 ≤log≤ f2 v2 : τ') -∗
+    {E;Δ;Γ} ⊨ f1 ≤log≤ f2 : TArrow τ τ'.
+  Proof.
+    iIntros (????) "#H".
+    iApply bin_log_related_arrow_val; eauto.
+    iAlways. iIntros (v1 v2) "#Hvv".
+    iApply "H". iAlways.
+    iApply (related_ret ⊤).
+    by iApply interp_ret.
   Qed.
 
-  Lemma bin_log_related_cas_suc_l' Δ Γ E K l e1 e2 v1 v2 v' t τ :
-    to_val e1 = Some v1 →
-    to_val e2 = Some v2 →
-    v' = v1 →
-    ▷ l ↦ᵢ v' -∗
-    (l ↦ᵢ v2 -∗ {E;Δ;Γ} ⊨ fill K #true ≤log≤ t : τ)
-    -∗ {E;Δ;Γ} ⊨ fill K (CAS (# l) e1 e2) ≤log≤ t : τ.
+  (** ** (Pure) reductions on the left *)
+
+  (* TODO: I have to 'refine' here for some reason *)
+  Local Ltac solve_red H :=
+    iApply (bin_log_pure_l with H); auto;
+    [ intros; apply pure_exec_safe
+    | intros ???? Hst;
+      refine (@pure_exec_puredet F_mu_ref_conc_lang _ _ _ _ _ _ _ _ _ Hst)
+    ]; eauto.
+  Local Ltac solve_red_masked H :=
+    iApply (bin_log_pure_masked_l with H); auto;
+    [ intros; apply pure_exec_safe
+    | intros ???? Hst;
+      refine (@pure_exec_puredet F_mu_ref_conc_lang _ _ _ _ _ _ _ _ _ Hst)
+    ]; eauto.
+
+  Lemma bin_log_related_rec_l Δ Γ E K (f x : binder) e e' v t τ
+   (Hclosed : Closed (x :b: f :b: ∅) e) :
+   (to_val e' = Some v) →
+   ▷ ({E;Δ;Γ} ⊨ (fill K (subst' f (Rec f x e) (subst' x e' e))) ≤log≤ t : τ)
+   ⊢ {E;Δ;Γ} ⊨ (fill K (App (Rec f x e) e')) ≤log≤ t : τ.