update iris dep

src/algebra/async.v

@@ -11,11 +11,11 @@ Set Default Proof Using "Type".
 
 Class asyncG Σ (K V: Type) `{Countable K, EqDecision V} := {
   async_listG :> fmlistG (gmap K V) Σ;
-  async_mapG :> inG Σ (gmap_viewR K natO);
+  async_mapG :> inG Σ (gmap_viewR K (agreeR natO));
 }.
 
 Definition asyncΣ K V `{Countable K, EqDecision V} : gFunctors :=
-  #[ fmlistΣ (gmap K V); GFunctor (gmap_viewR K natO) ].
+  #[ fmlistΣ (gmap K V); GFunctor (gmap_viewR K (agreeR natO)) ].
 
 #[global]
 Instance subG_asyncΣ Σ K V `{Countable K, EqDecision V} : subG (asyncΣ K V) Σ → asyncG Σ K V.
@@ -44,9 +44,9 @@ Local Definition is_last σs k i : Prop :=
   ∃ v, lookup_async σs i k = Some v ∧
     ∀ i', i ≤ i' → i' < length (possible σs) → lookup_async σs i' k = Some v.
 Local Definition own_last_auth γ q σs : iProp Σ :=
-  ∃ (last: gmap K nat), ⌜map_Forall (is_last σs) last⌝ ∗ own γ.(async_map) (gmap_view_auth q last).
+  ∃ (last: gmap K nat), ⌜map_Forall (is_last σs) last⌝ ∗ own γ.(async_map) (gmap_view_auth q (to_agree <$> last)).
 Local Definition own_last_frag γ k i : iProp Σ :=
-  own γ.(async_map) (gmap_view_frag k (DfracOwn 1) i).
+  own γ.(async_map) (gmap_view_frag k (DfracOwn 1) (to_agree i)).
 
 (* The possible states in [σs] are tracked in a regular append-only list.
 Additionally, there is a way to control which was the last transaction that changed
@@ -107,7 +107,8 @@ Lemma own_last_frag_conflict γ k i1 i2 :
 Proof.
   rewrite /own_last_frag.
   iIntros "H1 H2".
-  iDestruct (own_valid_2 with "H1 H2") as %Hvalid%gmap_view_frag_op_valid_L.
+  iDestruct (own_valid_2 with "H1 H2") as %Hvalid.
+  apply gmap_view_frag_op_valid in Hvalid.
   iPureIntro.
   destruct Hvalid as [Hdfrac _].
   rewrite dfrac_op_own in Hdfrac.
@@ -148,10 +149,13 @@ Proof.
   - iDestruct 1 as "[H1 H2]".
     iDestruct "H1" as (last1 ?) "H1".
     iDestruct "H2" as (last2 ?) "H2".
-    iDestruct (own_valid_2 with "H1 H2") as %Hvalid%gmap_view_auth_dfrac_op_inv_L.
-    subst.
+    iDestruct (own_valid_2 with "H1 H2") as %Hvalid.
+    apply gmap_view_auth_dfrac_op_inv in Hvalid.
     iCombine "H1 H2" as "H".
-    eauto.
+    rewrite Hvalid.
+    iExists last2. iSplit; first done.
+    rewrite -gmap_view_auth_dfrac_op.
+    iFrame.
 Qed.
 
 Local Lemma lookup_async_insert_ne k k' v' m σs j :
@@ -176,13 +180,20 @@ Local Lemma own_last_shift γ σs k i i' :
 Proof.
   iIntros (Hle Hi') "Halast Hflast".
   iDestruct "Halast" as (last Hlast) "Hmap".
-  iDestruct (own_valid_2 with "Hmap Hflast") as %[_ Hk]%gmap_view_both_valid_L.
+  iDestruct (own_valid_2 with "Hmap Hflast") as %Hk.
+  apply gmap_view_both_valid in Hk. destruct Hk as (_ & _ & Hk).
   iMod (own_update_2 with "Hmap Hflast") as "[Hmap Hflast]".
-  { apply (gmap_view_update _ k i i'). }
+  { apply (gmap_view_replace _ k (to_agree i) (to_agree i')). done. }
   iModIntro. iFrame "Hflast".
+  rewrite -fmap_insert.
   iExists _. iFrame. iPureIntro. intros k' j.
   destruct (decide (k=k')) as [->|Hne].
-  - rewrite lookup_insert=>[=<-]. destruct (Hlast _ _ Hk) as (v & Hv & Htail).
+  - rewrite lookup_insert=>[=<-].
+    assert (last !! k' = Some i) as Hk'.
+    { rewrite lookup_fmap in Hk. apply fmap_Some_equiv in Hk. destruct Hk as (x & Ha & Hb).
+      apply (inj to_agree) in Hb.
+      inversion Hb. done. }
+    destruct (Hlast _ _ Hk') as (v & Hv & Htail).
     exists v. split.
     + apply Htail; lia.
     + intros i'' Hi''. apply Htail. lia.
@@ -226,7 +237,8 @@ Proof.
   iIntros "Halast Hflast". iDestruct "Halast" as (last Hlast) "Hmap".
   assert ((S (length (possible σs)) - 1) = length (possible σs)) as -> by lia.
   iMod (own_update_2 with "Hmap Hflast") as "[Hmap $]".
-  { apply (gmap_view_update _ k _ (length (possible σs))). }
+  { apply (gmap_view_replace _ k _ (to_agree (length (possible σs)))). done. }
+  rewrite -fmap_insert.
   iExists _. iFrame "Hmap". iPureIntro.
   intros k' j. destruct (decide (k = k')) as [<-|Hne].
   - rewrite lookup_insert=>[=<-]. exists v'.
@@ -372,7 +384,11 @@ Proof.
   iClear "Hval".
   iDestruct "Hauth" as "(Halast & Halist & Hflist)".
   iDestruct "Halast" as (last Hlast) "Hmap".
-  iDestruct (own_valid_2 with "Hmap Hlast") as %(_  & _ & Hmap)%gmap_view_both_dfrac_valid_L.
+  iDestruct (own_valid_2 with "Hmap Hlast") as %Hmap.
+  apply gmap_view_both_dfrac_valid_discrete_total in Hmap.
+  destruct Hmap as (v' & _ & _ & Hma & _ & Hmc).
+  rewrite lookup_fmap in Hma. apply fmap_Some in Hma. destruct Hma as (x & Hmap & ->).
+  apply to_agree_included_L in Hmc. subst.
   destruct (Hlast _ _ Hmap) as (v' & Hlookup' & Htail).
   rewrite Hlookup in Hlookup'. injection Hlookup' as [=<-].
   iApply ephemeral_lookup_txn_val; last first.
@@ -469,8 +485,12 @@ Proof.
   { apply prefix_nil. }
   iFrame "Hlb".
   iMod (own_update with "Hmap") as "Hmap".
-  { eapply (gmap_view_alloc_big _ last (DfracOwn 1)); last done.
-    apply map_disjoint_empty_r. }
+  { eapply (gmap_view_alloc_big _ (to_agree <$> last) (DfracOwn 1)). 2: done.
+    1: apply map_disjoint_empty_r.
+    apply map_Forall_lookup. intros i x Ha.
+    rewrite lookup_fmap in Ha. apply fmap_Some in Ha. destruct Ha as (y & _ & ->).
+    done.
+  }
   iDestruct "Hmap" as "[Hmap Hfrag]".
   iModIntro. iSplitR "Hfrag"; first iSplit.
   - iExists last. rewrite right_id. iFrame.
@@ -484,6 +504,7 @@ Proof.
   - iPureIntro. apply Forall_app. split; first done.
     apply Forall_singleton. done.
   - rewrite big_opM_own_1. subst last.
+    rewrite big_sepM_fmap.
     rewrite big_sepM_fmap.
     iApply (big_sepM_impl with "Hfrag"). iIntros "!#" (k v Hk) "Hfrag".
     rewrite app_length /=.

src/algebra/na_heap.v

@@ -28,7 +28,7 @@ Definition na_sizeUR (L: Type) `{Countable L} : ucmra :=
 Class na_heapGS (L V: Type) Σ `{BlockAddr L} := Na_HeapG {
   na_heap_inG :> inG Σ (authR (na_heapUR L V));
   na_size_inG :> inG Σ (authR (na_sizeUR Z));
-  na_meta_inG :> inG Σ (gmap_viewR L gnameO);
+  na_meta_inG :> inG Σ (gmap_viewR L (agreeR gnameO));
   na_meta_data_inG :> inG Σ (reservation_mapR (agreeR positiveO));
   na_heap_name : gname;
   na_size_name : gname;
@@ -42,14 +42,14 @@ Arguments na_meta_name {_ _ _ _ _ _} _ : assert.
 Class na_heapGpreS (L V : Type) (Σ : gFunctors) `{BlockAddr L} := {
   na_heap_preG_inG :> inG Σ (authR (na_heapUR L V));
   na_size_preG_inG :> inG Σ (authR (na_sizeUR Z));
-  na_meta_preG_inG :> inG Σ (gmap_viewR L gnameO);
+  na_meta_preG_inG :> inG Σ (gmap_viewR L (agreeR gnameO));
   na_meta_data_preG_inG :> inG Σ (reservation_mapR (agreeR positiveO));
 }.
 
 Definition na_heapΣ (L V : Type) `{BlockAddr L} : gFunctors := #[
   GFunctor (authR (na_heapUR L V));
   GFunctor (authR (na_sizeUR Z));
-  GFunctor (gmap_viewR L gnameO);
+  GFunctor (gmap_viewR L (agreeR gnameO));
   GFunctor (reservation_mapR (agreeR positiveO))
 ].
 
@@ -115,14 +115,14 @@ Section definitions.
     seal_eq na_block_size_aux.
 
   Definition meta_token_def (l : L) (E : coPset) : iProp Σ :=
-    (∃ γm, own (na_meta_name hG) (gmap_view_frag l DfracDiscarded γm) ∗
+    (∃ γm, own (na_meta_name hG) (gmap_view_frag l DfracDiscarded (to_agree γm)) ∗
            own γm (reservation_map_token E))%I.
   Definition meta_token_aux : seal (@meta_token_def). Proof. by eexists. Qed.
   Definition meta_token := meta_token_aux.(unseal).
   Definition meta_token_eq : @meta_token = @meta_token_def := meta_token_aux.(seal_eq).
 
   Definition meta_def `{Countable A} (l : L) (N : namespace) (x : A) : iProp Σ :=
-    (∃ γm, own (na_meta_name hG) (gmap_view_frag l DfracDiscarded γm) ∗
+    (∃ γm, own (na_meta_name hG) (gmap_view_frag l DfracDiscarded (to_agree γm)) ∗
            own γm (reservation_map_data (positives_flatten N) (to_agree (encode x))))%I.
   Definition meta_aux : seal (@meta_def). Proof. by eexists. Qed.
   Definition meta {A dA cA} := meta_aux.(unseal) A dA cA.
@@ -326,7 +326,8 @@ Section na_heap.
     iDestruct 1 as (γm1) "[#Hγm1 Hm1]". iDestruct 1 as (γm2) "[#Hγm2 Hm2]".
     iAssert ⌜ γm1 = γm2 ⌝%I as %->.
     { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
-      move: Hγ. apply gmap_view_frag_op_valid_L. }
+      apply gmap_view_frag_op_valid in Hγ. destruct Hγ as [Ha Hb].
+      apply to_agree_op_inv_L in Hb. done. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %?%reservation_map_token_valid_op.
     iExists γm2. iFrame "Hγm2". rewrite reservation_map_token_union //. by iSplitL "Hm1".
   Qed.
@@ -351,7 +352,8 @@ Section na_heap.
     iDestruct 1 as (γm1) "[Hγm1 Hm1]"; iDestruct 1 as (γm2) "[Hγm2 Hm2]".
     iAssert ⌜ γm1 = γm2 ⌝%I as %->.
     { iDestruct (own_valid_2 with "Hγm1 Hγm2") as %Hγ; iPureIntro.
-      move: Hγ. apply gmap_view_frag_op_valid_L.  }
+      apply gmap_view_frag_op_valid in Hγ. destruct Hγ as [Ha Hb].
+      apply to_agree_op_inv_L in Hb. done. }
     iDestruct (own_valid_2 with "Hm1 Hm2") as %Hγ; iPureIntro.
     move: Hγ. rewrite -reservation_map_data_op reservation_map_data_valid.
     move=> /to_agree_op_inv_L. naive_solver.
@@ -384,8 +386,8 @@ Section na_heap.
     iMod (own_alloc (reservation_map_token ⊤)) as (γm) "Hγm".
     { apply reservation_map_token_valid. }
     iMod (own_update with "Hm") as "[Hm Hlm]".
-    { eapply (gmap_view_alloc _ l DfracDiscarded); last done.
-      move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
+    { eapply (gmap_view_alloc _ l DfracDiscarded (to_agree _)). 2: done. 2: done.
+      { move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. } }
     iDestruct "Hwf" as %[Hwf1 Hwf2].
     assert (sz !! addr_id l = None).
     {
@@ -402,7 +404,7 @@ Section na_heap.
     iModIntro. rewrite na_heap_pointsto_eq/na_heap_pointsto_def.
     iFrame "Hl".
     iSplitL "Hσ Hm Hsz". (* last by eauto with iFrame. *)
-    { iExists (<[l:=γm]> m), sz.
+    { iExists (<[l:=(to_agree γm)]> m), sz.
       rewrite to_na_heap_insert /block_sizes_wf
               !dom_insert_L Hread //=.
       iFrame; iPureIntro; split_and!.
@@ -432,7 +434,7 @@ Section na_heap.
     iMod (own_alloc (reservation_map_token ⊤)) as (γm) "Hγm".
     { apply reservation_map_token_valid. }
     iMod (own_update with "Hm") as "[Hm Hlm]".
-    { eapply (gmap_view_alloc _ l DfracDiscarded); last done.
+    { eapply (gmap_view_alloc _ l DfracDiscarded (to_agree _)). 2: done. 2: done.
       move: Hσl. rewrite -!(not_elem_of_dom (D:=gset L)). set_solver. }
     iDestruct "Hwf" as %[Hwf1 Hwf2].
     assert (sz !! addr_id l = None).
@@ -449,7 +451,7 @@ Section na_heap.
     iModIntro. rewrite na_heap_pointsto_eq/na_heap_pointsto_def na_block_size_eq/na_block_size_def.
     iFrame "Hl Hszl".
     iSplitL "Hσ Hm Hsz". (* last by eauto with iFrame. *)
-    { iExists (<[l:=γm]> m), (<[addr_id l:=z]> sz).
+    { iExists (<[l:=(to_agree γm)]> m), (<[addr_id l:=z]> sz).
       rewrite to_na_heap_insert to_na_size_insert /block_sizes_wf
               !dom_insert_L Hread //=.
       iFrame; iPureIntro; split_and!.

src/program_proof/mvcc/mvcc_ghost.v

@@ -5,7 +5,7 @@ From Perennial.program_proof.mvcc Require Import mvcc_prelude.
 (* RA definitions. *)
 Local Definition vchainR := mono_listR dbvalO.
 Local Definition key_vchainR := gmapR u64 vchainR.
-Local Definition tidsR := gmap_viewR nat unitO.
+Local Definition tidsR := gmap_viewR nat unitR.
 Local Definition sid_tidsR := gmapR u64 tidsR.
 Local Definition sid_min_tidR := gmapR u64 mono_natR.
 Local Definition sid_ownR := gmapR u64 (exclR unitO).
@@ -350,8 +350,9 @@ Lemma site_active_tids_elem_of γ (sid : u64) tids tid :
 Proof.
   iIntros "Hauth Helem".
   iDestruct (own_valid_2 with "Hauth Helem") as %Hvalid.
-  rewrite singleton_op singleton_valid gmap_view_both_dfrac_valid_L in Hvalid.
-  destruct Hvalid as (_ & _ & Hlookup).
+  rewrite singleton_op singleton_valid in Hvalid.
+  apply gmap_view_both_dfrac_valid_discrete_total in Hvalid.
+  destruct Hvalid as (v' & _ & _ & Hlookup & _ & _).
   apply elem_of_dom_2 in Hlookup.
   rewrite dom_gset_to_gmap in Hlookup.
   done.
@@ -364,8 +365,10 @@ Lemma site_active_tids_agree γ (sid : u64) tids tids' :
 Proof.
   iIntros "Hauth1 Hauth2".
   iDestruct (own_valid_2 with "Hauth1 Hauth2") as %Hvalid.
-  rewrite singleton_op singleton_valid gmap_view_auth_dfrac_op_valid_L in Hvalid.
+  rewrite singleton_op singleton_valid in Hvalid.
+  apply gmap_view_auth_dfrac_op_valid in Hvalid.
   destruct Hvalid as [_ Etids].
+  iPureIntro.
   rewrite -(dom_gset_to_gmap tids ()) -(dom_gset_to_gmap tids' ()).
   by rewrite Etids.
 Qed.
@@ -387,7 +390,7 @@ Proof.
     apply singleton_update.
     rewrite gset_to_gmap_union_singleton.
     (* Q: What's the difference between [apply] (which fails here) and [apply:]? *)
-    apply: gmap_view_alloc; last done.
+    apply: gmap_view_alloc; last done; last done.
     by rewrite lookup_gset_to_gmap_None.
   }
   by iFrame.