Generalize some lemmas and an alternative with_lock rule

The new _with_lock rule does not mentioned lower level details of the
relational interpretation.

F_mu_ref_conc/examples/counter.v

@@ -74,6 +74,45 @@ Section CG_Counter.
     by iFrame.
   Qed.
 
+  (* TODO: those should be accompaied by lemmas; preferably so that 
+     [change] does not change too much *)
+  Tactic Notation "rel_bind_l" open_constr(efoc) :=
+    lazymatch goal with
+    | [ |- (_ ⊢ bin_log_related _ _ _ ?e _ _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e'))
+    end.
+  Tactic Notation "rel_bind_r" open_constr(efoc) :=
+    lazymatch goal with
+    | [ |- (_ ⊢ bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+    | [ |- (_ ⊢ bin_log_related _ _ _ _ ?e _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+    end.
+ 
+  Lemma bin_log_related_CG_increment_r Γ K E1 E2 x n t τ :
+    nclose specN ⊆ E1 →
+    x ↦ₛ (#nv n) -∗
+    (x ↦ₛ (#nv (S n)) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K Unit : τ) -∗
+    {E1,E2;Γ} ⊨ t ≤log≤ fill K (App (CG_increment (Loc x)) Unit) : τ.
+  Proof.
+    iIntros (?) "Hx Hlog".
+    unfold CG_increment. simpl.
+    iApply bin_log_related_rec_r; auto. simpl.
+    (* TODO: rel_bind_r (Load (Loc x)) *)
+    change ((Store (Loc x) (BinOp Add (#n 1) (Load (Loc x)))))
+    with (fill [StoreRCtx (LocV x);BinOpRCtx Add (#nv 1)] (Load (Loc x))).
+    rewrite -fill_app.
+    iApply (bin_log_related_load_r with "Hx");auto.
+    iIntros "Hx". rewrite ?fill_app /=.
+    rel_bind_r (BinOp Add _ _).
+    iApply (bin_log_related_binop_r); auto.
+    rewrite fill_app /=.
+    iApply (bin_log_related_store_r with "Hx"); auto.
+  Qed.
+  
   Global Opaque CG_increment.
 
   Lemma CG_locked_increment_to_val x l :
@@ -131,13 +170,10 @@ Section CG_Counter.
     {E1,E2;Γ} ⊨ t ≤log≤ fill K (App (CG_locked_increment (Loc x) (Loc l)) Unit) : τ)%I.
   Proof. 
     iIntros (?) "Hx Hl Hlog".
-    unfold CG_locked_increment.
-    change Unit with (of_val UnitV).
-    iApply (bin_log_related_with_lock_r Γ K E1 E2 (x ↦ₛ (#nv n))%I (x ↦ₛ (#nv S n)) (CG_increment (Loc x)) UnitV UnitV l t τ with "[Hx] [Hl] [Hlog]"); auto.
-    - iIntros (ρ j K') "#Hspec Hx Hj /=".
-      tp_apply j steps_CG_increment with "Hx" as "Hx". iModIntro.
-      iFrame.
-    - iIntros "Hl Hx". iApply ("Hlog" with "Hx Hl").
+    unfold CG_locked_increment.  
+    iApply (bin_log_related_with_lock_r' Γ K E1 E2 (x ↦ₛ (#nv S n)) _ Unit Unit with "[Hx] Hl"); eauto. 
+    - iIntros (K') "Hlog".
+      iApply (bin_log_related_CG_increment_r with "Hx"); auto.
   Qed.
  
   Global Opaque CG_locked_increment.
@@ -259,21 +295,6 @@ Section CG_Counter.
 
   Definition counterN : namespace := nroot .@ "counter".
 
-  (* TODO: those should be accompaied by lemmas; preferably so that 
-     [change] does not change too much *)
-  Ltac rel_bind_l efoc :=
-    lazymatch goal with
-    | [ |- (_ ⊢ bin_log_related _ _ _ ?e _ _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e'))
-    end.
-  Ltac rel_bind_r efoc :=
-    lazymatch goal with
-    | [ |- (_ ⊢ bin_log_related _ _ _ _ ?e _ ) ] =>
-      reshape_expr e ltac:(fun K e' =>
-       unify e' efoc; change e with (fill K e'))
-    end.
-
   Lemma bin_log_related_arrow Γ (e e' : expr) τ τ'
    (Hclosed : ∀ f, e.[upn 2 f] = e)
    (Hclosed' : ∀ f, e'.[upn 2 f] = e') :

F_mu_ref_conc/examples/lock.v

@@ -125,10 +125,11 @@ Section proof.
     by iFrame.
   Qed.
 
-  Lemma bin_log_related_acquire_r Γ K l t τ :
+  Lemma bin_log_related_acquire_r Γ E1 E2 K l t τ
+    (Hspec : nclose specN ⊆ E1) :
     l ↦ₛ (#♭v false) -∗
-    (l ↦ₛ (#♭v true) -∗ Γ ⊨ t ≤log≤ fill K Unit : τ)%I
-    -∗ Γ ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ.
+    (l ↦ₛ (#♭v true) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K Unit : τ)%I
+    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App acquire (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
     pose (Φ := (fun w => ⌜w = UnitV⌝ ∗ l ↦ₛ (#♭v true))%I).
@@ -157,10 +158,11 @@ Section proof.
     by iFrame.
   Qed.
 
-  Lemma bin_log_related_release_r Γ K l t τ b :
+  Lemma bin_log_related_release_r Γ K E1 E2 l t τ b
+    (Hspec : nclose specN ⊆ E1):
     l ↦ₛ (#♭v b) -∗
-    (l ↦ₛ (#♭v false) -∗ Γ ⊨ t ≤log≤ fill K Unit : τ)%I
-    -∗ Γ ⊨ t ≤log≤ fill K (App release (Loc l)) : τ.
+    (l ↦ₛ (#♭v false) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K Unit : τ)%I
+    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App release (Loc l)) : τ.
   Proof.
     iIntros "Hl Hlog".
     pose (Φ := (fun w => ⌜w = UnitV⌝ ∗ l ↦ₛ (#♭v false))%I).
@@ -206,6 +208,75 @@ Section proof.
     by iFrame.
   Qed.
 
+  (* TODO: those should be accompaied by lemmas; preferably so that 
+     [change] does not change too much *)
+  Tactic Notation "rel_bind_l" open_constr(efoc) :=
+    lazymatch goal with
+    | [ |- (_ ⊢ bin_log_related _ _ _ ?e _ _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e'))
+    end.
+  Tactic Notation "rel_bind_r" open_constr(efoc) :=
+    lazymatch goal with
+    | [ |- (_ ⊢ bin_log_related _ _ _ _ (fill _ ?e) _ ) ] =>
+      reshape_expr e ltac:(fun K e' =>
+       unify e' efoc; change e with (fill K e')); try (rewrite -fill_app)
+    end.
+
+  
+  Lemma bin_log_related_with_lock_r' Γ K E1 E2 Q e ev ew v w l t τ :
+    (nclose specN ⊆ E1) →
+    (to_val ev = Some v) →
+    (to_val ew = Some w) →
+    (∀ f, e.[f] = e) (* e is a closed term *) →
+    (∀ f, ev.[f] = ev) (* v is a closed term *) →
+    (∀ f, ew.[f] = ew) (* w is a closed term *) →
+    (∀ K, (Q -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K ev : τ) -∗
+        {E1,E2;Γ} ⊨ t ≤log≤ fill K (App e ew) : τ) -∗
+    l ↦ₛ (#♭v false) -∗
+    (Q -∗ l ↦ₛ (#♭v false) -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K ev : τ)%I
+    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App (with_lock e (Loc l)) ew) : τ.
+  Proof.
+    iIntros (??? Hcle Hclv Hclw) "HA Hl Hlog".
+    unfold with_lock.
+    iApply (bin_log_related_rec_r); eauto.
+    { intro f. simpl.
+      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.
+      done.  }
+    asimpl.
+    rel_bind_r (App acquire (Loc l)).
+    iApply (bin_log_related_acquire_r Γ E1 E2 (K ++ _) l with "Hl"); auto.
+    iIntros "Hl". rewrite fill_app /=.
+    rewrite Hcle Hclw.
+    iApply (bin_log_related_rec_r); eauto.
+    { intro f. simpl.
+      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.
+      done.  }
+    asimpl. rewrite Hcle Hclw.
+    rel_bind_r (App e ew).
+    iApply "HA". iIntros "HQ".
+    rewrite fill_app /=.
+    iApply (bin_log_related_rec_r); eauto.
+    asimpl. rewrite Hclv.
+    rel_bind_r (App release _).
+    iApply (bin_log_related_release_r with "Hl"); eauto.
+    iIntros "Hl".
+    rewrite fill_app /=.
+    iApply (bin_log_related_rec_r); eauto. 
+    rewrite Hclv.
+    iApply ("Hlog" with "HQ Hl").
+  Qed.
+
   Lemma bin_log_related_with_lock_r Γ K E1 E2 P Q e v w l t τ :
     (nclose specN ⊆ E1) →
     (∀ f, e.[f] = e) (* e is a closed term *) →

F_mu_ref_conc/relational_properties.v

@@ -614,12 +614,13 @@ Section properties.
   
   (** ** Reductions on the right *)
   (** Lifting of the pure reductions *)
-  Lemma bin_log_pure_r Γ τ K' e e' t
+  Lemma bin_log_pure_r Γ τ K' E1 E2 e e' t
+    (Hspec : nclose specN ⊆ E1)
     (Hclosed1 : ∀ f, e.[f] = e)
     (Hclosed2 : ∀ f, e'.[f] = e') :
     (∀ σ, head_step e σ e' σ []) →
-    Γ ⊨ t ≤log≤ fill K' e' : τ
-    ⊢ Γ ⊨ t ≤log≤ fill K' e : τ.
+    {E1,E2;Γ} ⊨ t ≤log≤ fill K' e' : τ
+    ⊢ {E1,E2;Γ} ⊨ t ≤log≤ fill K' e : τ.
   Proof.
     iIntros (Hstep) "Hlog".
     iIntros (Δ vvs ρ) "#Hs #HΓ".
@@ -631,12 +632,13 @@ Section properties.
     iDestruct ("Hlog" with "* Hs [HΓ] * Hj") as "Hlog"; auto.    
   Qed.
 
-  Lemma bin_log_related_rec_r Γ K e e' t v' τ
+  Lemma bin_log_related_rec_r Γ K E1 E2 e e' t v' τ
+   (Hspec : nclose specN ⊆ E1)
    (Hclosed : ∀ f, e.[upn 2 f] = e)
    (Hclosed' : ∀ f, e'.[f] = e') :
    (to_val e' = Some v') →
-   Γ ⊨ t ≤log≤ fill K e.[Rec e, e'/] : τ
-   ⊢ Γ ⊨ t ≤log≤ fill K (App (Rec e) e') : τ.
+   {E1,E2;Γ} ⊨ t ≤log≤ fill K e.[Rec e, e'/] : τ
+   ⊢ {E1,E2;Γ} ⊨ t ≤log≤ fill K (App (Rec e) e') : τ.
   Proof.
     iIntros (?) "Hlog".
     iApply (bin_log_pure_r with "Hlog"); auto; intros.
@@ -654,11 +656,12 @@ Section properties.
   (* Lemma bin_log_related_Fold_r Γ K e e' v' τ *)
   (* Lemma bin_log_related_Pack_r Γ K e e' v' τ *)
   
-  Lemma bin_log_related_fst_r Γ K e v1 v2 τ
+  Lemma bin_log_related_fst_r Γ K E1 E2 e v1 v2 τ
+   (Hspec : nclose specN ⊆ E1)
    (Hclosed1 : ∀ f, (of_val v1).[f] = (of_val v1))
    (Hclosed2 : ∀ f, (of_val v2).[f] = (of_val v2)) :
-   Γ ⊨ e ≤log≤ (fill K (of_val v1)) : τ
-   ⊢ Γ ⊨ e ≤log≤ (fill K (Fst (Pair (of_val v1) (of_val v2)))) : τ.
+   {E1,E2;Γ} ⊨ e ≤log≤ (fill K (of_val v1)) : τ
+   ⊢ {E1,E2;Γ} ⊨ e ≤log≤ (fill K (Fst (Pair (of_val v1) (of_val v2)))) : τ.
   Proof.
     iIntros "Hlog".
     iApply (bin_log_pure_r with "Hlog"); auto; intros.
@@ -666,11 +669,12 @@ Section properties.
     { econstructor; eauto. }
   Qed.
 
-  Lemma bin_log_related_snd_r Γ K e v1 v2 τ
+  Lemma bin_log_related_snd_r Γ K E1 E2 e v1 v2 τ
+   (Hspec : nclose specN ⊆ E1)
    (Hclosed1 : ∀ f, (of_val v1).[f] = (of_val v1))
    (Hclosed2 : ∀ f, (of_val v2).[f] = (of_val v2)) :
-   Γ ⊨ e ≤log≤ (fill K (of_val v2)) : τ
-   ⊢ Γ ⊨ e ≤log≤ (fill K (Snd (Pair (of_val v1) (of_val v2)))) : τ.
+   {E1,E2;Γ} ⊨ e ≤log≤ (fill K (of_val v2)) : τ
+   ⊢ {E1,E2;Γ} ⊨ e ≤log≤ (fill K (Snd (Pair (of_val v1) (of_val v2)))) : τ.
   Proof.
     iIntros "Hlog".
     iApply (bin_log_pure_r with "Hlog"); auto; intros.
@@ -682,11 +686,12 @@ Section properties.
   (* Lemma bin_log_related_inl_r Γ K e e' v' τ *)
   (* Lemma bin_log_related_inr_r Γ K e e' v' τ *)
 
-  Lemma bin_log_related_if_true_r Γ K e e1 e2 τ
+  Lemma bin_log_related_if_true_r Γ K E1 E2 e e1 e2 τ
+   (Hspec : nclose specN ⊆ E1)
    (Hclosed1 : ∀ f, e1.[f] = e1)
    (Hclosed2 : ∀ f, e2.[f] = e2) :
-   Γ ⊨ e ≤log≤ (fill K e1) : τ
-   ⊢ Γ ⊨ e ≤log≤ (fill K (If (#♭ true) e1 e2)) : τ.
+   {E1,E2;Γ} ⊨ e ≤log≤ (fill K e1) : τ
+   ⊢ {E1,E2;Γ} ⊨ e ≤log≤ (fill K (If (#♭ true) e1 e2)) : τ.
   Proof.
     iIntros "Hlog".
     iApply (bin_log_pure_r with "Hlog"); auto; intros.
@@ -694,11 +699,12 @@ Section properties.
     { econstructor; eauto. }
   Qed.
 
-  Lemma bin_log_related_if_false_r Γ K e e1 e2 τ
+  Lemma bin_log_related_if_false_r Γ K E1 E2 e e1 e2 τ
+   (Hspec : nclose specN ⊆ E1)
    (Hclosed1 : ∀ f, e1.[f] = e1)
    (Hclosed2 : ∀ f, e2.[f] = e2) :
-   Γ ⊨ e ≤log≤ (fill K e2) : τ
-   ⊢ Γ ⊨ e ≤log≤ (fill K (If (#♭ false) e1 e2)) : τ.
+   {E1,E2;Γ} ⊨ e ≤log≤ (fill K e2) : τ
+   ⊢ {E1,E2;Γ} ⊨ e ≤log≤ (fill K (If (#♭ false) e1 e2)) : τ.
   Proof.
     iIntros "Hlog".
     iApply (bin_log_pure_r with "Hlog"); auto; intros.
@@ -706,9 +712,17 @@ Section properties.
     { econstructor; eauto. }
   Qed.
 
-  (* TODO *)
-  (* Lemma bin_log_related_nat_binop_r Γ K e e1 e2 τ *)
-
+  Lemma bin_log_related_binop_r Γ K E1 E2 op a b t τ
+   (Hspec : nclose specN ⊆ E1)
+   (Hcl : ∀f,(of_val (binop_eval op a b)).[f] = (of_val (binop_eval op a b))) :
+   {E1,E2;Γ} ⊨ t ≤log≤ fill K (of_val (binop_eval op a b)) : τ
+   ⊢ {E1,E2;Γ} ⊨ t ≤log≤ (fill K (BinOp op (#n a) (#n b))) : τ.
+  Proof.
+    iIntros "Hlog".
+    iApply (bin_log_pure_r with "Hlog"); auto; intros.
+    econstructor; eauto.
+  Qed.
+  
   (* TODO difference btween |={⊤}=> and |==>  *)
   (*   note: also can put an update after the quantifier (in addition to the one present *)
   (** Stateful reductions *)
@@ -774,12 +788,13 @@ Section properties.
     done.
   Qed.
 
-  Lemma bin_log_related_store_r Γ K l e v v' t τ
+  Lemma bin_log_related_store_r Γ K E1 E2 l e v v' t τ 
+    (Hmasked : nclose specN ⊆ E1)
     (Hclosed : ∀ f, e.[f] = e) :
     (to_val e = Some v') →
     l ↦ₛ v -∗
-    (l ↦ₛ v' -∗ Γ ⊨ t ≤log≤ fill K Unit : τ)
-    -∗ Γ ⊨ t ≤log≤ fill K (Store (Loc l) e) : τ.
+    (l ↦ₛ v' -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K Unit : τ)
+    -∗ {E1,E2;Γ} ⊨ t ≤log≤ fill K (Store (Loc l) e) : τ.
   Proof.
     iIntros (?) "Hl Hlog".
     pose (Φ := (fun w => ⌜w = UnitV⌝ ∗ l ↦ₛ v')%I).