Simplify and update

- evmap is dropped
- per-item invariant is implemented with inv-in-inv
- peritem.v is simplified by proving an ad-hoc iter spec
- update to latest iris
- related fixes

_CoqProject

@@ -7,6 +7,5 @@ theories/flat.v
 theories/atomic_sync.v
 theories/treiber.v
 theories/misc.v
-theories/evmap.v
 theories/peritem.v
 theories/atomic_pcas.v

opam.pins

-coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 766dbcd2415df9256f197dc562a0a15f9b0ddeac
+coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2e3a9be08487e50bfc4bba911da6a11a4b715d36

theories/evmap.v

-(* evmap.v -- generalized heap-like monoid composite *)
-From iris.base_logic Require Export invariants.
-From iris.program_logic Require Export weakestpre.
-From iris.algebra Require Export auth frac gmap.
-From iris.algebra Require deprecated.
-From iris.proofmode Require Import tactics.
-
-Export deprecated.dec_agree.
-(* Porting this to algebra.agree does not really work well because the
-   map from K to (Q * agree A) is part of the interface of this file.
-   This file should either be ditched or raised to a higher level
-   of abstraction, i.e., work on a map from K to A and use fmap
-   for the thing that's owned. *)
-
-Section evmap.
-  Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}.
-  Definition evkR := prodR Q (dec_agreeR A).
-  Definition evmapR := gmapUR K evkR.
-  Definition evidenceR := authR evmapR.
-  Class evidenceG Σ := EvidenceG { evidence_G :> inG Σ evidenceR }.
-  Definition evidenceΣ : gFunctors := #[ GFunctor (constRF evidenceR) ].
-
-  Instance subG_evidenceΣ {Σ} : subG evidenceΣ Σ → evidenceG Σ.
-  Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
-
-  (* Some basic supporting lemmas *)
-  Lemma map_agree_eq m m' (hd: K) (p q: Q) (x y: A):
-    m !! hd = Some (p, DecAgree y) →
-    m = {[hd := (q, DecAgree x)]} ⋅ m' → x = y.
-  Proof.
-    intros H1 H2.
-    destruct (decide (x = y)) as [->|Hneq]=>//.
-    exfalso.
-    subst. rewrite lookup_op lookup_singleton in H1.
-    destruct (m' !! hd) as [[b [c|]]|] eqn:Heqn; rewrite Heqn in H1; inversion H1=>//.
-    destruct (decide (x = c)) as [->|Hneq3]=>//.
-    - rewrite dec_agree_idemp in H3. by inversion H3.
-    - rewrite dec_agree_ne in H3=>//.
-  Qed.
-
-  Lemma map_agree_somebot m m' (hd: K) (p q: Q) (x: A):
-    m !! hd = Some (p, DecAgreeBot) → m' !! hd = None →
-    m = {[hd := (q, DecAgree x)]} ⋅ m' → False.
-  Proof.
-    intros H1 H2 H3. subst. rewrite lookup_op lookup_singleton in H1.
-    destruct (m' !! hd) as [[b [c|]]|] eqn:Heqn; rewrite Heqn in H1; inversion H1=>//.
-  Qed.
-
-  Lemma map_agree_none m m' (hd: K) (q: Q) (x: A):
-    m !! hd = None → m = {[hd := (q, DecAgree x)]} ⋅ m' → False.
-  Proof.
-    intros H1 H2. subst. rewrite lookup_op lookup_singleton in H1.
-    destruct (m' !! hd)=>//.
-  Qed.
-End evmap.
-
-Section evmapR.
-  Context (K A: Type) `{Countable K, EqDecision A}.
-  Context `{!inG Σ (authR (evmapR K A unitR))}.
-
-  (* Evidence that k immutably maps to some fixed v *)
-  Definition ev γm (k : K) (v: A) := own γm (◯ {[ k := ((), DecAgree v) ]})%I.
-
-  Global Instance persistent_ev γm k v : PersistentP (ev γm k v).
-  Proof. apply _. Qed.
-
-  (* Alloc a new mapsto *)
-  Lemma evmap_alloc γm m k v:
-    m !! k = None →
-    own γm (● m) ⊢ |==> own γm (● (<[ k := ((), DecAgree v) ]> m) ⋅ ◯ {[ k := ((), DecAgree v) ]}).
-  Proof.
-    iIntros (?) "Hm".
-    iDestruct (own_update with "Hm") as "?"; last by iAssumption.
-    apply auth_update_alloc. apply alloc_singleton_local_update=>//.
-  Qed.
-  
-  (* Some other supporting lemmas *)
-  Lemma map_agree_none' γm (m: evmapR K A unitR) hd x:
-    m !! hd = None →
-    own γm (● m) ∗ ev γm hd x ⊢ False.
-  Proof.
-    iIntros (?) "[Hom Hev]".
-    iCombine "Hom" "Hev" as "Hauth".
-    iDestruct (own_valid with "Hauth") as %Hvalid. iPureIntro.
-    apply auth_valid_discrete_2 in Hvalid as [[af Compose%leibniz_equiv_iff] Valid].
-    eapply (map_agree_none _ _ _ m)=>//.
-  Qed.
-
-  Lemma map_agree_eq' γm m hd x agy:
-    m !! hd = Some ((), agy) →
-    ev γm hd x ∗ own γm (● m) ⊢ ⌜DecAgree x = agy⌝.
-  Proof.
-    iIntros (?) "[#Hev Hom]".
-    iCombine "Hom" "Hev" as "Hauth".
-    iDestruct (own_valid γm (● m ⋅ ◯ {[hd := (_, DecAgree x)]})
-               with "[Hauth]") as %Hvalid=>//.
-    apply auth_valid_discrete_2 in Hvalid as [[af Compose%leibniz_equiv_iff] Valid].
-    destruct agy as [y|].
-    - iDestruct "Hauth" as "[? ?]". iFrame.
-      iPureIntro. apply f_equal.
-      eapply (map_agree_eq _ _ _ m)=>//.
-    - iAssert (✓ m)%I as "H"=>//. rewrite (gmap_validI m).
-      iDestruct ("H" $! hd) as "%".
-      exfalso. subst. rewrite H0 in H1.
-      by destruct H1 as [? ?].
-  Qed.
-
-  (* Evidence is the witness of membership *)
-  Lemma ev_map_witness γm m hd x:
-    ev γm hd x ∗ own γm (● m) ⊢ ⌜m !! hd = Some (∅, DecAgree x)⌝.
-  Proof.
-    iIntros "[#Hev Hom]".
-    destruct (m !! hd) as [[[] agy]|] eqn:Heqn.
-    - iDestruct (map_agree_eq' with "[-]") as %H'=>//; first by iFrame. by subst.
-    - iExFalso. iApply map_agree_none'=>//. by iFrame.
-  Qed.
-  
-  (* Two evidences coincides *)
-  Lemma evmap_frag_agree_split γm p (a1 a2: A):
-    ev γm p a1 ∗ ev γm p a2 ⊢ ⌜a1 = a2⌝.
-  Proof.
-    iIntros "[Ho Ho']".
-    destruct (decide (a1 = a2)) as [->|Hneq].
-    - by iFrame.
-    - iCombine "Ho" "Ho'" as "Ho".
-      rewrite -(@auth_frag_op (evmapR K A unitR) {[p := (_, DecAgree a1)]} {[p := (_, DecAgree a2)]}).
-      iDestruct (own_valid with "Ho") as %Hvalid.
-      exfalso. rewrite op_singleton in Hvalid.
-      apply auth_valid_discrete in Hvalid. simpl in Hvalid.
-      apply singleton_valid in Hvalid.
-      destruct Hvalid as [_ Hvalid].
-      apply dec_agree_op_inv in Hvalid. inversion Hvalid. subst. auto.
-  Qed.
-End evmapR.

theories/peritem.v

 From iris.program_logic Require Export weakestpre.
 From iris.heap_lang Require Export lang.
 From iris.heap_lang Require Import proofmode notation.
+From iris.proofmode Require Import tactics.
 From iris.algebra Require Import frac auth gmap csum.
 From iris.base_logic Require Import big_op.
-From iris_atomic Require Export treiber misc evmap.
+From iris_atomic Require Export treiber misc.
+From iris.base_logic.lib Require Import invariants namespaces.
 
 Section defs.
-  Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
+  Context `{heapG Σ} (N: namespace).
   Context (R: val → iProp Σ) `{∀ x, TimelessP (R x)}.
 
-  Definition allocated hd := (∃ q v, hd ↦{q} v)%I.
-
-  Definition evs (γ: gname) := ev loc val γ.
-
-  Fixpoint is_list' (γ: gname) (hd: loc) (xs: list val) : iProp Σ :=
+  Fixpoint is_list_R (hd: loc) (xs: list val) : iProp Σ :=
     match xs with
     | [] => (∃ q, hd ↦{ q } NONEV)%I
-    | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ∗ evs γ hd x ∗ is_list' γ hd' xs)%I
+    | x :: xs => (∃ (hd': loc) q, hd ↦{q} SOMEV (x, #hd') ∗ inv N (R x) ∗ is_list_R hd' xs)%I
     end.
 
-  Lemma in_list' γ x xs:
-    ∀ hd, x ∈ xs →
-          is_list' γ hd xs
-          ⊢ ∃ (hd' hd'': loc) q, hd' ↦{q} SOMEV (x, #hd'') ∗ evs γ hd' x.
-  Proof.
-    induction xs as [|x' xs' IHxs'].
-    - intros ? Hin. inversion Hin.
-    - intros hd Hin. destruct (decide (x = x')) as [->|Hneq].
-      + iIntros "Hls". simpl.
-        iDestruct "Hls" as (hd' q) "(? & ? & ?)".
-        iExists hd, hd', q. iFrame.
-      + assert (x ∈ xs') as Hin'; first set_solver.
-        iIntros "Hls". simpl.
-        iDestruct "Hls" as (hd' q) "(? & ? & ?)".
-        iApply IHxs'=>//.
-  Qed.
-
-  Definition perR' hd v v' := (⌜v = ((∅: unitR), DecAgree v')⌝ ∗ R v' ∗ allocated hd)%I.
-  Definition perR  hd v := (∃ v', perR' hd v v')%I.
-  
-  Definition allR γ := (∃ m : evmapR loc val unitR, own γ (● m) ∗ [∗ map] hd ↦ v ∈ m, perR hd v)%I.
+  Definition is_bag_R xs s := (∃ hd: loc, s ↦ #hd ∗ is_list_R hd xs)%I.
 
-  Definition is_stack' γ xs s :=
-    (∃ hd: loc, s ↦ #hd ∗ is_list' γ hd xs ∗ allR γ)%I.
-
-  Global Instance is_list'_timeless γ hd xs: TimelessP (is_list' γ hd xs).
-  Proof. generalize hd. induction xs; apply _. Qed.
-
-  Global Instance is_stack'_timeless γ xs s: TimelessP (is_stack' γ xs s).
-  Proof. apply _. Qed.
-
-  Lemma dup_is_list' γ : ∀ xs hd,
-    is_list' γ hd xs ⊢ |==> is_list' γ hd xs ∗ is_list' γ hd xs.
+  Lemma dup_is_list_R : ∀ xs hd,
+    is_list_R hd xs ⊢ |==> is_list_R hd xs ∗ is_list_R hd xs.
   Proof.
     induction xs as [|y xs' IHxs'].
     - iIntros (hd) "Hs".
       simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
     - iIntros (hd) "Hs". simpl.
-      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hev & Hs')".
+      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & #Hinv & Hs')".
       iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
       iModIntro. iSplitL "Hhd Hs1"; iExists hd', (q / 2)%Qp; by iFrame.
   Qed.
-
-  Lemma extract_is_list γ : ∀ xs hd,
-    is_list' γ hd xs ⊢ |==> is_list' γ hd xs ∗ is_list hd xs.
-  Proof.
-    induction xs as [|y xs' IHxs'].
-    - iIntros (hd) "Hs".
-      simpl. iDestruct "Hs" as (q) "[Hhd Hhd']". iSplitL "Hhd"; eauto.
-    - iIntros (hd) "Hs". simpl.
-      iDestruct "Hs" as (hd' q) "([Hhd Hhd'] & Hev & Hs')".
-      iDestruct (IHxs' with "[Hs']") as ">[Hs1 Hs2]"; first by iFrame.
-      iModIntro. iSplitL "Hhd Hs1 Hev"; iExists hd', (q / 2)%Qp; by iFrame.
-  Qed.
-
-  Definition f_spec γ (xs: list val) (s: loc) (f: val) (Rf RI: iProp Σ) :=
-    (* Rf, RI is some frame *)
-    ∀ Φ (x: val),
-      inv N ((∃ xs, is_stack' γ xs s) ∗ RI) ∗ (∃ hd, evs γ hd x) ∗
-      Rf ∗ (Rf -∗ Φ #())
-      ⊢ WP f x {{ Φ }}.
 End defs.
 
 Section proofs.
-  Context `{heapG Σ, !evidenceG loc val unitR Σ} (N: namespace).
+  Context `{heapG Σ} (N: namespace).
   Context (R: val → iProp Σ).
 
-Lemma new_stack_spec' Φ RI:
-    RI ∗ (∀ γ s : loc, inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) -∗ Φ #s)
-    ⊢ WP new_stack #() {{ Φ }}.
+  Definition bag_inv s: iProp Σ := inv N (∃ xs, is_bag_R N R xs s)%I.
+
+  Lemma new_bag_spec:
+    {{{ True }}} new_stack #() {{{ s, RET #s; bag_inv s }}}.
   Proof.
-    iIntros "(HR & HΦ)". iApply wp_fupd.
-    iMod (own_alloc (● (∅: evmapR loc val unitR) ⋅ ◯ ∅)) as (γ) "[Hm Hm']".
-    { apply auth_valid_discrete_2. done. }
+    iIntros (Φ) "HΦ". iApply wp_fupd.
     wp_seq. wp_bind (ref NONE)%E. wp_alloc l as "Hl".
     wp_alloc s as "Hs".
-    iAssert ((∃ xs : list val, is_stack' R γ xs s) ∗ RI)%I with "[-HΦ Hm']" as "Hinv".
-    { iFrame. iExists [], l. iFrame. simpl. iSplitL "Hl".
-      - eauto.
-      - iExists ∅. iSplitL. iFrame. by iApply (big_sepM_empty (fun hd v => perR R hd v)). }
-    iMod (inv_alloc N _ ((∃ xs : list val, is_stack' R γ xs s) ∗ RI)%I with "[-HΦ Hm']") as "#?"; first eauto.
-    by iApply "HΦ".
-  Qed.
-    
-  Lemma iter_spec Φ γ s (Rf RI: iProp Σ):
-    ∀ xs hd (f: expr) (f': val),
-      f_spec N R γ xs s f' Rf RI → to_val f = Some f' →
-      inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) ∗
-      is_list' γ hd xs ∗ Rf ∗ (Rf -∗ Φ #())
-      ⊢ WP (iter #hd) f {{ v, Φ v }}.
-  Proof.
-    induction xs as [|x xs' IHxs'].
-    - simpl. iIntros (hd f f' ? ?) "(#? & Hxs1 & HRf & HΦ)".
-      iDestruct "Hxs1" as (q) "Hhd".
-      wp_rec. wp_value. wp_let. wp_load. wp_match. by iApply "HΦ".
-    - simpl. iIntros (hd f f' Hf ?) "(#? & Hxs1 & HRf & HΦ)".
-      iDestruct "Hxs1" as (hd2 q) "(Hhd & Hev & Hhd2)".
-      wp_rec. wp_value. wp_let. wp_load. wp_match. wp_proj.
-      wp_bind (f' _). iApply Hf=>//. iFrame "#".
-      iSplitL "Hev"; first eauto. iFrame. iIntros "HRf".
-      wp_seq. wp_proj. iApply (IHxs' with "[-]")=>//.
-      + apply to_of_val.
-      + iFrame "#". by iFrame.
+    iAssert ((∃ xs, is_bag_R N R xs s))%I with "[-HΦ]" as "Hxs".
+    { iFrame. iExists [], l.
+      iFrame. simpl. eauto. }
+    iMod (inv_alloc N _ (∃ xs : list val, is_bag_R N R xs s)%I with "[-HΦ]") as "#?"; first eauto.
+    iApply "HΦ". iFrame "#".
   Qed.
   
-  Lemma push_spec Φ γ (s: loc) (x: val) RI:
-    R x ∗ inv N ((∃ xs, is_stack' R γ xs s) ∗ RI) ∗ ((∃ hd, evs γ hd x) -∗ Φ #())
-    ⊢ WP push #s x {{ Φ }}.
+  Lemma push_spec (s: loc) (x: val):
+    {{{ R x ∗ bag_inv s }}} push #s x {{{ RET #() ; inv N (R x) }}}.
   Proof.
-    iIntros "(HRx & #? & HΦ)".
-    iDestruct (push_atomic_spec s x) as "Hpush"=>//.
-    iSpecialize ("Hpush" $! (R x) (fun ret => (∃ hd, evs γ hd x) ∗ ⌜ret = #()⌝)%I with "[]").
-    - iIntros "!# Rx".
-      (* open the invariant *)
-      iInv N as "[IH1 ?]" "Hclose".
-      iDestruct "IH1" as (xs hd) "[>Hs [>Hxs HR]]".
-      iDestruct (extract_is_list with "[Hxs]") as ">[Hxs Hxs']"; first by iFrame.
-      iDestruct (dup_is_list with "[Hxs']") as "[Hxs'1 Hxs'2]"; first by iFrame.
-      (* mask magic *)
-      iMod (fupd_intro_mask' (⊤ ∖ nclose N) ∅) as "Hvs"; first set_solver.
-      iModIntro. iExists (xs, hd).
-      iFrame "Hs Hxs'1". iSplit.
-      + (* provide a way to rollback *)
-        iIntros "[Hs Hl']".
-        iMod "Hvs". iMod ("Hclose" with "[-Rx]"); last done.
-        { iNext. iFrame. iExists xs. iExists hd. by iFrame. }
-      + (* provide a way to commit *)
-        iIntros (v) "Hs".
-        iDestruct "Hs" as (hd') "[% [Hs [[Hhd'1 Hhd'2] Hxs']]]". subst.
-        iMod "Hvs".
-        iDestruct "HR" as (m) "[>Hom HRm]".
-        destruct (m !! hd') eqn:Heqn.
-        * iDestruct (big_sepM_delete_later (perR R) m with "HRm") as "[Hx ?]"=>//.
-          iDestruct "Hx" as (?) "(_ & _ & >Hhd'')".
-          iCombine "Hhd'1" "Hhd'2" as "Hhd".
-          iDestruct "Hhd''" as (q v) "Hhd''". iExFalso.
-          iApply (bogus_heap hd' 1%Qp q); first apply Qp_not_plus_q_ge_1.
-          iFrame "#". iFrame.
-        * iAssert (evs γ hd' x ∗ ▷ (allR R γ))%I
-                  with ">[Rx Hom HRm Hhd'1]" as "[#Hox ?]".
-          {
-            iDestruct (evmap_alloc _ _ _ m with "[Hom]") as ">[Hom Hox]"=>//.
-            iDestruct (big_sepM_insert_later (perR R) m) as "H"=>//.
-            iSplitL "Hox".
-            { rewrite /evs /ev. eauto. }
-            iExists (<[hd' := ((), DecAgree x)]> m).
-            iFrame. iApply "H". iFrame. iExists x.
-            iFrame. rewrite /allocated. iSplitR "Hhd'1"; auto.
-          }
-          iMod ("Hclose" with "[-]").
-          { iNext. iFrame. iExists (x::xs).
-            iExists hd'. iFrame.
-            iExists hd, (1/2)%Qp. by iFrame.
-          }
-        iModIntro. iSplitL; last auto. by iExists hd'.
-    - iApply wp_wand_r. iSplitL "HRx Hpush".
-      + by iApply "Hpush".
-      + iIntros (?) "[? %]". subst.
-        by iApply "HΦ".
+    iIntros (Φ) "(HRx & #?) HΦ".
+    iLöb as "IH". wp_rec. wp_let.
+    wp_bind (! _)%E.
+    iInv N as "H1" "Hclose".
+    iDestruct "H1" as (xs hd) "[>Hs H1]".
+    wp_load. iMod ("Hclose" with "[Hs H1]").
+    { iNext. iFrame. iExists xs, hd. iFrame. }
+    iModIntro. wp_let. wp_alloc l as "Hl".
+    wp_let. wp_bind (CAS _ _ _)%E.
+    iInv N as "H1" "Hclose".
+    iDestruct "H1" as (xs' hd') "[>Hs H1]".
+    destruct (decide (hd = hd')) as [->|Hneq].
+    - wp_cas_suc.
+      iMod (inv_alloc N _ (R x) with "[HRx]") as "#HRx"; first eauto.
+      iMod ("Hclose" with "[Hs Hl H1]").
+      { iNext. iFrame. iExists (x::xs'), l.
+        iFrame. simpl. iExists hd', 1%Qp. iFrame.
+        by iFrame "#". }
+      iModIntro. wp_if. by iApply "HΦ".
+    - wp_cas_fail.
+      iMod ("Hclose" with "[Hs H1]").
+      { iNext. iFrame. iExists (xs'), hd'. iFrame. }
+      iModIntro. wp_if. iApply ("IH" with "HRx").
+      by iNext.
   Qed.
 
 End proofs.