From e7cc356089a2c7ad89ea9cff403afedefa50a5e2 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 10 Mar 2017 15:04:51 +0100
Subject: [PATCH] Seal off tpool_mapsto and heapS_mapsto to speed up
 unification.

---
 F_mu_ref_conc/rules_binary.v     | 41 +++++++++++++++++++-------------
 F_mu_ref_conc/soundness_binary.v |  4 ++--
 2 files changed, 26 insertions(+), 19 deletions(-)

diff --git a/F_mu_ref_conc/rules_binary.v b/F_mu_ref_conc/rules_binary.v
index 929db3a..5cee1d4 100644
--- a/F_mu_ref_conc/rules_binary.v
+++ b/F_mu_ref_conc/rules_binary.v
@@ -24,24 +24,26 @@ Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
 Section definitionsS.
   Context `{cfgSG Σ, invG Σ}.
 
-  Definition heapS_mapsto (l : loc) (q : Qp) (v: val) : iProp Σ :=
+  Definition heapS_mapsto_def (l : loc) (q : Qp) (v: val) : iProp Σ :=
     own cfg_name (◯ (∅, {[ l := (q, to_agree v) ]})).
+  Definition heapS_mapsto_aux : { x | x = @heapS_mapsto_def }. by eexists. Qed.
+  Definition heapS_mapsto := proj1_sig heapS_mapsto_aux.
+  Definition heapS_mapsto_eq :
+    @heapS_mapsto = @heapS_mapsto_def := proj2_sig heapS_mapsto_aux.
 
-  Definition tpool_mapsto (j : nat) (e: expr) : iProp Σ :=
+  Definition tpool_mapsto_def (j : nat) (e: expr) : iProp Σ :=
     own cfg_name (◯ ({[ j := Excl e ]}, ∅)).
+  Definition tpool_mapsto_aux : { x | x = @tpool_mapsto_def }. by eexists. Qed.
+  Definition tpool_mapsto := proj1_sig tpool_mapsto_aux.
+  Definition tpool_mapsto_eq :
+    @tpool_mapsto = @tpool_mapsto_def := proj2_sig tpool_mapsto_aux.
 
   Definition spec_inv (ρ : cfg lang) : iProp Σ :=
     (∃ tp σ, own cfg_name (● (to_tpool tp, to_gen_heap σ)) 
                  ∗ ⌜rtc step ρ (tp,σ)⌝)%I.
   Definition spec_ctx (ρ : cfg lang) : iProp Σ :=
     inv specN (spec_inv ρ).
-
-  Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
-  Proof. apply _. Qed.
-  Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
-  Proof. apply _. Qed.
 End definitionsS.
-Typeclasses Opaque heapS_mapsto tpool_mapsto.
 
 Notation "l ↦ₛ{ q } v" := (heapS_mapsto l q v)
   (at level 20, q at level 50, format "l  ↦ₛ{ q }  v") : uPred_scope.
@@ -107,7 +109,6 @@ Section conversions.
   Lemma tpool_singleton_included' tp j e :
     {[j := Excl e]} ≼ to_tpool tp → to_tpool tp !! j = Excl' e.
   Proof. rewrite tpool_lookup. by move=> /tpool_singleton_included=> ->. Qed.
-
 End conversions.
 
 Section cfg.
@@ -124,6 +125,11 @@ Section cfg.
   Local Hint Resolve to_tpool_insert'.
   Local Hint Resolve tpool_singleton_included.
 
+  Global Instance heapS_mapsto_timeless l q v : TimelessP (heapS_mapsto l q v).
+  Proof. rewrite heapS_mapsto_eq. apply _. Qed.
+  Global Instance spec_ctx_persistent ρ : PersistentP (spec_ctx ρ).
+  Proof. apply _. Qed.
+
   Lemma step_insert K tp j e σ e' σ' efs :
     tp !! j = Some (fill K e) → head_step e σ e' σ' efs →
     step (tp, σ) (<[j:=fill K e']> tp ++ efs, σ').
@@ -145,7 +151,7 @@ Section cfg.
     nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
   Proof.
-    iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
+    iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
@@ -161,7 +167,7 @@ Section cfg.
     to_val e = Some v → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Alloc e) ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ v.
   Proof.
-    iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx /tpool_mapsto.
+    iIntros (??) "[#Hinv Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     destruct (exist_fresh (dom (gset positive) σ)) as [l Hl%not_elem_of_dom].
     iDestruct (own_valid_2 with "Hown Hj")
@@ -173,7 +179,8 @@ Section cfg.
     { eapply auth_update_alloc, prod_local_update_2,
         (alloc_singleton_local_update _ l (1%Qp,to_agree v)); last done.
       by apply lookup_to_gen_heap_None. }
-    iExists l. rewrite /heapS_mapsto. iFrame "Hj Hl". iApply "Hclose". iNext.
+    iExists l. rewrite heapS_mapsto_eq /heapS_mapsto_def.
+    iFrame "Hj Hl". iApply "Hclose". iNext.
     iExists (<[j:=fill K (Loc l)]> tp), (<[l:=v]>σ).
     rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
@@ -185,7 +192,7 @@ Section cfg.
     ={E}=∗ j ⤇ fill K (of_val v) ∗ l ↦ₛ{q} v.
   Proof.
     iIntros (?) "(#Hinv & Hj & Hl)".
-    rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
@@ -205,7 +212,7 @@ Section cfg.
     ={E}=∗ j ⤇ fill K Unit ∗ l ↦ₛ v.
   Proof.
     iIntros (??) "(#Hinv & Hj & Hl)".
-    rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
@@ -230,7 +237,7 @@ Section cfg.
     ={E}=∗ j ⤇ fill K (#♭ false) ∗ l ↦ₛ{q} v'.
   Proof.
     iIntros (????) "(#Hinv & Hj & Hl)".
-    rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
@@ -251,7 +258,7 @@ Section cfg.
     ={E}=∗ j ⤇ fill K (#♭ true) ∗ l ↦ₛ v2.
   Proof.
     iIntros (????) "(#Hinv & Hj & Hl)"; subst.
-    rewrite /spec_ctx /tpool_mapsto /heapS_mapsto.
+    rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def heapS_mapsto_eq /heapS_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_valid_discrete_2.
@@ -334,7 +341,7 @@ Section cfg.
     nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Fork e) ={E}=∗ ∃ j', j ⤇ fill K Unit ∗ j' ⤇ e.
   Proof.
-    iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
+    iIntros (?) "[#Hspec Hj]". rewrite /spec_ctx tpool_mapsto_eq /tpool_mapsto_def.
     iInv specN as (tp σ) ">[Hown %]" "Hclose".
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
diff --git a/F_mu_ref_conc/soundness_binary.v b/F_mu_ref_conc/soundness_binary.v
index 7b5d417..08fbbf0 100644
--- a/F_mu_ref_conc/soundness_binary.v
+++ b/F_mu_ref_conc/soundness_binary.v
@@ -31,10 +31,10 @@ Proof.
   { iApply (@logrel_binary.interp_env_nil Σ HeapΣ). }
   simpl.
   rewrite empty_env_subst empty_env_subst. iApply ("Hrel" $! 0 []).
-  { rewrite /tpool_mapsto. asimpl. iFrame. }
+  { rewrite tpool_mapsto_eq /tpool_mapsto_def. asimpl. iFrame. }
   iIntros (v1); iDestruct 1 as (v2) "[Hj #Hinterp]".
   iInv specN as (tp σ) ">[Hown Hsteps]" "Hclose"; iDestruct "Hsteps" as %Hsteps'.
-  rewrite /tpool_mapsto /=.
+  rewrite tpool_mapsto_eq /tpool_mapsto_def /=.
   iDestruct (own_valid_2 with "Hown Hj") as %Hvalid.
   move: Hvalid=> /auth_valid_discrete_2
     [/prod_included [/tpool_singleton_included Hv2 _] _].
-- 
GitLab