Lemmas for the closure of the binary interpretation under reductions

F_mu_ref_conc/examples/lock.v

 From iris.proofmode Require Import tactics.
 From iris_logrel.F_mu_ref_conc Require Import tactics.
-From iris_logrel.F_mu_ref_conc Require Export rules_binary typing.
+From iris_logrel.F_mu_ref_conc Require Export rules_binary typing fundamental_binary.
 From iris.base_logic Require Import namespaces.
 
 (** [newlock = alloc false] *)
@@ -92,6 +92,25 @@ Section proof.
     by iExists _; iFrame.
   Qed.
 
+  Lemma bin_log_related_newlock_r Γ K t τ :
+    (∀ (l : loc), l ↦ₛ (#♭v false) -∗ Γ ⊨ t ≤log≤ fill K (Loc l) : τ)%I
+    -∗ Γ ⊨ t ≤log≤ fill K newlock : τ.
+  Proof.
+    iIntros "Hlog".
+    pose (Φ := (fun w => ∃ l, ⌜w = (LocV l)⌝ ∗ l ↦ₛ (#♭v false))%I).
+    iApply (bin_log_related_step_r Φ with "[]").
+    { autosubst.  }
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      tp_apply j steps_newlock.
+      iDestruct "Hj" as (l) "[Hj Hl]".
+      iExists (LocV l). simpl. iFrame.
+      iModIntro. iSplitL; eauto. }
+    iIntros (v') "He'". iDestruct "He'" as (l) "[% Hl]". subst.
+    iApply "Hlog".
+    done.
+  Qed.
+
   Global Opaque newlock.
 
   Lemma steps_acquire E ρ j K l :
@@ -106,6 +125,25 @@ Section proof.
     by iFrame.
   Qed.
 
+  Lemma bin_log_related_acquire_r Γ K l t τ :
+    l ↦ₛ (#♭v false) -∗
+    (l ↦ₛ (#♭v true) -∗ Γ ⊨ t ≤log≤ fill K Unit : τ)%I
+    -∗ Γ ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ.
+  Proof.
+    iIntros "Hl Hlog".
+    pose (Φ := (fun w => ⌜w = UnitV⌝ ∗ l ↦ₛ (#♭v true))%I).
+    iApply (bin_log_related_step_r Φ with "[Hl]").
+    { autosubst.  }
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      tp_apply j steps_acquire with "Hl" as "Hl".
+      iExists UnitV. simpl. iFrame.
+      iModIntro. iSplitL; eauto. }
+    iIntros (v') "[% Hl]". subst.
+    iApply "Hlog".
+    done.
+  Qed.
+  
   Global Opaque acquire.
 
   Lemma steps_release E ρ j K l b:
@@ -119,6 +157,25 @@ Section proof.
     by iFrame.
   Qed.
 
+  Lemma bin_log_related_release_r Γ K l t τ b :
+    l ↦ₛ (#♭v b) -∗
+    (l ↦ₛ (#♭v false) -∗ Γ ⊨ t ≤log≤ fill K Unit : τ)%I
+    -∗ Γ ⊨ t ≤log≤ fill K (App release (Loc l)) : τ.
+  Proof.
+    iIntros "Hl Hlog".
+    pose (Φ := (fun w => ⌜w = UnitV⌝ ∗ l ↦ₛ (#♭v false))%I).
+    iApply (bin_log_related_step_r Φ with "[Hl]").
+    { autosubst.  }
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      tp_apply j steps_release with "Hl" as "Hl".
+      iExists UnitV. simpl. iFrame.
+      iModIntro. iSplitL; eauto. }
+    iIntros (v') "[% Hl]". subst.
+    iApply "Hlog".
+    done.
+  Qed.
+
   Global Opaque release.
 
   Lemma steps_with_lock E ρ j K e l P Q v w:
@@ -149,5 +206,39 @@ Section proof.
     by iFrame.
   Qed.
 
+  Lemma bin_log_related_with_lock_r Γ K P Q e v w l t τ :
+    (∀ f, e.[f] = e) (* e is a closed term *) →
+    (∀ f, (of_val v).[f] = of_val v) (* v is a closed term *) →
+    (∀ f, (of_val w).[f] = of_val w) (* w is a closed term *) →
+    (∀ ρ j K', spec_ctx ρ -∗ P -∗ j ⤇ fill K' (App e (of_val w))
+            ={⊤}=∗ j ⤇ fill K' (of_val v) ∗ Q) →
+    P -∗
+    l ↦ₛ (#♭v false) -∗
+    (l ↦ₛ (#♭v false) -∗ Q -∗ Γ ⊨ t ≤log≤ fill K (of_val v) : τ)%I
+    -∗ Γ ⊨ t ≤log≤ fill K (App (with_lock e (Loc l)) (of_val w)) : τ.
+  Proof.
+    iIntros (????) "HP Hl Hlog".
+    pose (Φ := (fun (w: val) => ⌜w = v⌝ ∗ Q ∗ l ↦ₛ (#♭v false))%I).
+    iApply (bin_log_related_step_r Φ with "[HP Hl]").
+    { intros. 
+      replace ((App (with_lock e (Loc l)) (of_val w)).[f])
+      with (App (with_lock e (Loc l)).[f] (of_val w).[f]); auto.
+      rewrite with_lock_closed. 
+      all: repeat lazymatch goal with
+        | [Hcl : ∀ s, ?e.[s] = ?e |- context[?e.[_]]]
+          => rewrite Hcl
+        | [Hcl : ∀ s, ?e = ?e.[s] |- context[?e.[?F]]]
+          => rewrite -(Hcl F)
+        end; try done. }
+    { cbv[Φ].
+      iIntros (ρ j K') "#Hs Hj /=".
+      iMod (steps_with_lock _ _ j K' _ l P Q with "Hs HP Hl Hj")
+           as "[Hj [HQ Hl]]"; auto.
+      iExists v. iFrame.
+      iModIntro. auto. }
+    iIntros (v') "[% [HQ Hl]]". subst.
+    iApply ("Hlog" with "Hl HQ").
+  Qed.
+
   Global Opaque with_lock.
 End proof.

F_mu_ref_conc/lang.v

@@ -355,6 +355,15 @@ Module lang.
   Instance of_val_inj : Inj (=) (=) of_val.
   Proof. by intros ?? Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
+  Lemma binop_eval_closed op a b f :
+  (of_val (binop_eval op a b)).[f] = (of_val (binop_eval op a b)).
+  Proof. 
+    induction op; simpl; eauto;
+    match goal with
+    | |- context[if ?H then _ else _] => destruct H; auto
+    end.
+  Qed.
+  
   Lemma fill_item_val Ki e :
     is_Some (to_val (fill_item Ki e)) → is_Some (to_val e).
   Proof. intros [v ?]. destruct Ki; simplify_option_eq; eauto. Qed.