update dependencies; use local definition of to_heap

opam

@@ -9,6 +9,6 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/reloc"]
 depends: [
-  "coq-iris" { (= "dev.2020-09-30.0.fe735a96") | (= "dev") }
+  "coq-iris" { (= "dev.2020-10-13.1.5558d66d") | (= "dev") }
   "coq-autosubst" { = "dev.coq86" }
 ]

theories/logic/adequacy.v

@@ -26,13 +26,13 @@ Lemma refines_adequate Σ `{relocPreG Σ}
 Proof.
   intros HA Hlog.
   eapply (heap_adequacy Σ _); iIntros (Hinv) "_".
-  iMod (own_alloc (● (to_tpool [e'], to_gen_heap (heap σ))
+  iMod (own_alloc (● (to_tpool [e'], to_heap (heap σ))
     ⋅ ◯ ((to_tpool [e'] : tpoolUR, ∅) : cfgUR)))
     as (γc) "[Hcfg1 Hcfg2]".
   { apply auth_both_valid_discrete. split=>//.
     - apply prod_included. split=>///=.
       apply: ucmra_unit_least.
-    - split=>//. apply to_tpool_valid. apply to_gen_heap_valid. }
+    - split=>//. apply to_tpool_valid. apply to_heap_valid. }
   set (Hcfg := RelocG _ _ (CFGSG _ _ γc)).
   iMod (inv_alloc specN _ (spec_inv ([e'], σ)) with "[Hcfg1]") as "#Hcfg".
   { iNext. iExists [e'], σ. eauto. }

theories/logic/spec_ra.v

@@ -12,8 +12,10 @@ Definition relocN := nroot .@ "reloc".
 Definition specN := relocN .@ "spec".
 
 (** The CMRA for the heap of the specification. *)
+Definition heapUR (L V : Type) `{Countable L} : ucmraT :=
+  gmapUR L (prodR fracR (agreeR (leibnizO V))).
 Definition tpoolUR : ucmraT := gmapUR nat (exclR exprO).
-Definition cfgUR := prodUR tpoolUR (gen_heapUR loc (option val)).
+Definition cfgUR := prodUR tpoolUR (heapUR loc (option val)).
 
 (** The CMRA for the thread pool. *)
 Class cfgSG Σ := CFGSG { cfg_inG :> inG Σ (authR cfgUR); cfg_name : gname }.
@@ -22,6 +24,8 @@ Class relocG Σ := RelocG {
   relocG_cfgG :> cfgSG Σ;
 }.
 
+Definition to_heap {L V} `{Countable L} : gmap L V → heapUR L V :=
+  fmap (λ v, (1%Qp, to_agree (v : leibnizO V))).
 Definition to_tpool (tp : list expr) : tpoolUR := Excl <$> (map_seq 0 tp).
 
 Section definitionsS.
@@ -44,7 +48,7 @@ Section definitionsS.
   Definition mkstate (σ : gmap loc (option val)) (κs : gset proph_id) :=
     {| heap := σ; used_proph_id := κs |}.
   Definition spec_inv ρ : iProp Σ :=
-    (∃ tp σ, own cfg_name (● (to_tpool tp, to_gen_heap (heap σ)))
+    (∃ tp σ, own cfg_name (● (to_tpool tp, to_heap (heap σ)))
                  ∗ ⌜rtc erased_step ρ (tp,σ)⌝)%I.
   Definition spec_ctx : iProp Σ :=
     (∃ ρ, inv specN (spec_inv ρ))%I.
@@ -122,6 +126,30 @@ Section conversions.
   Proof. rewrite tpool_lookup. by move=> /tpool_singleton_included=> ->. Qed.
 End conversions.
 
+Section to_heap.
+  Context (L V : Type) `{Countable L}.
+  Implicit Types σ : gmap L V.
+  Implicit Types m : gmap L gname.
+
+  Lemma lookup_to_heap_None σ l : σ !! l = None → to_heap σ !! l = None.
+  Proof. by rewrite /to_heap lookup_fmap=> ->. Qed.
+  Lemma to_heap_insert l v σ :
+    to_heap (<[l:=v]> σ) = <[l:=(1%Qp, to_agree (v:leibnizO V))]> (to_heap σ).
+  Proof. by rewrite /to_heap fmap_insert. Qed.
+
+  Lemma heap_singleton_included σ l q v :
+    {[l := (q, to_agree v)]} ≼ to_heap σ → σ !! l = Some v.
+  Proof.
+    rewrite singleton_included_l=> -[[q' av] []].
+    rewrite /to_heap lookup_fmap fmap_Some_equiv => -[v' [Hl [/= -> ->]]].
+    move=> /Some_pair_included_total_2 [_] /to_agree_included /leibniz_equiv_iff -> //.
+  Qed.
+
+  Lemma to_heap_valid σ : ✓ to_heap σ.
+  Proof. intros l. rewrite lookup_fmap. by case (σ !! l). Qed.
+
+End to_heap.  
+
 Section mapsto.
   Context `{cfgSG Σ}.
 

theories/logic/spec_rules.v

@@ -160,11 +160,11 @@ Section rules.
     iMod (own_update with "Hown") as "[Hown Hl]".
     { eapply auth_update_alloc, prod_local_update_2,
         (alloc_singleton_local_update _ l (1%Qp,to_agree (Some v : leibnizO _))); last done.
-      by apply lookup_to_gen_heap_None. }
+      by apply lookup_to_heap_None. }
     rewrite heapS_mapsto_eq /heapS_mapsto_def /=.
     iExists l. iFrame "Hj Hl". iApply "Hclose". iNext.
     iExists (<[j:=fill K (# l)]> tp), (state_upd_heap <[l:=Some v]> σ).
-    rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
+    rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto.
     rewrite -state_init_heap_singleton. eapply AllocNS; first by lia.
     intros. assert (i = 0) as -> by lia. by rewrite loc_add_0.
@@ -183,7 +183,7 @@ Section rules.
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[? ?%gen_heap_singleton_included]%prod_included ?]%auth_both_valid_discrete.
+      as %[[? ?%heap_singleton_included]%prod_included ?]%auth_both_valid_discrete.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (of_val v)))). }
@@ -207,20 +207,20 @@ Section rules.
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
+      as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K #()))). }
     iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
     { eapply auth_update, prod_local_update_2.
       apply: singleton_local_update.
-      { by rewrite /to_gen_heap lookup_fmap Hl. }
+      { by rewrite /to_heap lookup_fmap Hl. }
       apply: (exclusive_local_update _
         (1%Qp, to_agree (Some v : leibnizO (option val)))).
       apply: pair_exclusive_l. done. }
     iFrame "Hj Hl". iApply "Hclose". iNext.
     iExists (<[j:=fill K #()]> tp), (state_upd_heap <[l:=Some v]> σ).
-    rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
+    rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
   Qed.
 
@@ -241,7 +241,7 @@ Section rules.
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_both_valid_discrete.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ ?%gen_heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
+      as %[[_ ?%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (_, #false)%V))). }
@@ -268,20 +268,20 @@ Section rules.
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
+      as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (_, #true)%V))). }
     iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
     { eapply auth_update, prod_local_update_2.
       apply: singleton_local_update.
-      { by rewrite /to_gen_heap lookup_fmap Hl. }
+      { by rewrite /to_heap lookup_fmap Hl. }
       apply: (exclusive_local_update _
         (1%Qp, to_agree (Some v2 : leibnizO (option val)))).
       apply: pair_exclusive_l. done. }
     iFrame "Hj Hl". iApply "Hclose". iNext.
     iExists (<[j:=fill K (_, #true)%V]> tp), (state_upd_heap <[l:=Some v2]> σ).
-    rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
+    rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. econstructor; eauto.
     rewrite bool_decide_true //.
   Qed.
@@ -299,20 +299,20 @@ Section rules.
     iDestruct (own_valid_2 with "Hown Hj")
       as %[[?%tpool_singleton_included' _]%prod_included _]%auth_both_valid_discrete.
     iDestruct (own_valid_2 with "Hown Hl")
-      as %[[_ Hl%gen_heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
+      as %[[_ Hl%heap_singleton_included]%prod_included _]%auth_both_valid_discrete.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1, singleton_local_update,
         (exclusive_local_update _ (Excl (fill K (# i1)))). }
     iMod (own_update_2 with "Hown Hl") as "[Hown Hl]".
     { eapply auth_update, prod_local_update_2.
       apply: singleton_local_update.
-      { by rewrite /to_gen_heap lookup_fmap Hl. }
+      { by rewrite /to_heap lookup_fmap Hl. }
       apply: (exclusive_local_update _
         (1%Qp, to_agree (Some #(i1+i2) : leibnizO (option val)))).
       apply: pair_exclusive_l. done. }
     iFrame "Hj Hl". iApply "Hclose". iNext.
     iExists (<[j:=fill K (# i1)]> tp), (state_upd_heap <[l:=Some #(i1+i2)]> σ).
-    rewrite to_gen_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
+    rewrite to_heap_insert to_tpool_insert'; last eauto. iFrame. iPureIntro.
     eapply rtc_r, step_insert_no_fork; eauto. simpl. econstructor; eauto.
   Qed.