Commit 535a2fc5 by Ralf Jung

### FAILED: port evmap to dec_agree

parent a50a88fc
 coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 766dbcd2415df9256f197dc562a0a15f9b0ddeac coq-iris https://gitlab.mpi-sws.org/FP/iris-coq a953a68d9b9f30f8aa4e0e36811b9175f3f2ea58
 (* 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.algebra Require Export auth frac agree gmap. From iris.proofmode Require Import tactics. Export deprecated.dec_agree. Section evmap. Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}. Definition evkR := prodR Q (dec_agreeR A). Canonical AC := leibnizC A. Definition evkR := prodR Q (agreeR AC). Definition evmapR := gmapUR K evkR. Definition evidenceR := authR evmapR. Class evidenceG Σ := EvidenceG { evidence_G :> inG Σ evidenceR }. ... ... @@ -20,32 +18,31 @@ Section evmap. (* 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. m !! hd ≡ Some (p, to_agree y) → m ≡ {[hd := (q, to_agree 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=>//. intros H1 H2. unfold_leibniz. eapply to_agree_included. assert ({[hd := (q, to_agree x)]} !! hd ≼ m !! hd) as Hincl. { apply lookup_included. exists m'. done. } move: Hincl. rewrite lookup_singleton H1. move /Some_included=>[[/= _ ->]|/prod_included [_ ?]] //. 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. m = {[hd := (q, to_agree 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. m !! hd = None → m ≡ {[hd := (q, to_agree x)]} ⋅ m' → False. Proof. intros H1 H2. subst. rewrite lookup_op lookup_singleton in H1. destruct (m' !! hd)=>//. intros H1 H2. move:(H2 hd). rewrite H1 lookup_op lookup_singleton. case: (m' !! hd)=>[?|]//=; intros XX; inversion XX. Qed. End evmap. ... ... @@ -54,7 +51,7 @@ Section evmapR. 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. Definition ev γm (k : K) (v: A) := own γm (◯ {[ k := ((), to_agree v) ]})%I. Global Instance persistent_ev γm k v : PersistentP (ev γm k v). Proof. apply _. Qed. ... ... @@ -62,7 +59,7 @@ Section evmapR. (* 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) ]}). own γm (● m) ⊢ |==> own γm (● (<[ k := ((), to_agree v) ]> m) ⋅ ◯ {[ k := ((), to_agree v) ]}). Proof. iIntros (?) "Hm". iDestruct (own_update with "Hm") as "?"; last by iAssumption. ... ... @@ -77,36 +74,34 @@ Section evmapR. 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)=>//. apply auth_valid_discrete_2 in Hvalid as [[af Compose] 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⌝. ev γm hd x ∗ own γm (● m) ⊢ ⌜to_agree x ≡ agy⌝. Proof. iIntros (?) "[#Hev Hom]". iCombine "Hom" "Hev" as "Hauth". iDestruct (own_valid γm (● m ⋅ ◯ {[hd := (_, DecAgree x)]}) iDestruct (own_valid γm (● m ⋅ ◯ {[hd := (_, to_agree 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 [? ?]. apply auth_valid_discrete_2 in Hvalid as [[af Compose] Valid]. iDestruct "Hauth" as "[? ?]". iPureIntro. edestruct (to_agree_uninj agy) as [y Heq]. - move:(Valid hd). rewrite H0=>-[??] //. - rewrite -Heq. f_equiv. eapply (map_agree_eq _ _ _ m)=>//. by rewrite Heq H0. 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)⌝. ev γm hd x ∗ own γm (● m) ⊢ ⌜m !! hd ≡ Some (∅, to_agree x)⌝. Proof. iIntros "[#Hev Hom]". destruct (m !! hd) as [[[] agy]|] eqn:Heqn. - iDestruct (map_agree_eq' with "[-]") as %H'=>//; first by iFrame. by subst. - iDestruct (map_agree_eq' with "[-]") as %H'=>//; first by iFrame. iPureIntro. by rewrite H'. - iExFalso. iApply map_agree_none'=>//. by iFrame. Qed. ... ... @@ -118,12 +113,12 @@ Section evmapR. 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)]}). rewrite -(@auth_frag_op (evmapR K A unitR) {[p := (_, to_agree a1)]} {[p := (_, to_agree 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. apply agree_op_inv in Hvalid. apply (inj to_agree) in Hvalid. by fold_leibniz. Qed. End evmapR.
 ... ... @@ -158,7 +158,7 @@ Section proof. iDestruct (evmap_alloc _ _ _ m p (γx, γ1, γ3, γ4, γq) with "[Hm]") as ">[Hm1 #Hm2]"=>//. iDestruct "Hl" as "[Hl1 Hl2]". iMod ("Hclose" with "[HRm Hm1 Hl1 Hrs]"). + iNext. iFrame. iExists (<[p := (∅, DecAgree (γx, γ1, γ3, γ4, γq))]> m). iFrame. + iNext. iFrame. iExists (<[p := (∅, to_agree (γx, γ1, γ3, γ4, γq))]> m). iFrame. iDestruct (big_sepM_insert _ m with "[-]") as "H"=>//. iSplitL "Hl1"; last by iAssumption. eauto. + iDestruct (own_update with "Hx") as ">[Hx1 Hx2]"; first by apply pair_l_frac_op_1'. ... ... @@ -193,8 +193,12 @@ Section proof. iDestruct "HRs" as (m) "[>Hom HRs]". (* acccess *) iDestruct (ev_map_witness _ _ _ m with "[Hev Hom]") as %H'; first by iFrame. case Hlk:(m !! xhd)=>[xx|]; last first. { rewrite Hlk in H'. inversion H'. } iDestruct (big_sepM_delete_later (perR _) m with "HRs") as "[Hp HRm]"=>//. iDestruct "Hp" as (v') "[>% [Hpinv' >Hahd]]". inversion H. subst. rewrite Hlk in H'. iDestruct "Hp" as (v') "[>% [Hpinv' >Hahd]]". inversion H'. subst. destruct H2 as [_ H2]. apply (inj to_agree) in H2. fold_leibniz. subst. iDestruct "Hpinv'" as (ts p'') "[>% [>#Hevm [Hp | [Hp | [Hp | Hp]]]]]"; subst. + iDestruct "Hp" as (y) "(>Hp & Hs)". wp_load. iMod ("Hclose" with "[-Hor HR Hev HΦ']"). ... ... @@ -228,10 +232,14 @@ Section proof. iDestruct "Hs" as (xs'' hd''') "[>Hhd [>Hxs HRs]]". iDestruct "HRs" as (m') "[>Hom HRs]". iDestruct (ev_map_witness _ _ _ m' with "[Hevm Hom]") as %?; first by iFrame. case Hlk':(m' !! xhd)=>[xx|]; last first. { rewrite Hlk' in H. inversion H. } iDestruct (big_sepM_delete_later (perR _) m' with "HRs") as "[Hp HRm]"=>//. iDestruct "Hp" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H1. subst. rewrite Hlk' in H. iDestruct "Hp" as (v'') "[>% [Hpinv' >Hhd'']]". inversion H. subst. destruct H3 as [_ H3]. apply (inj to_agree) in H3. fold_leibniz. subst. iDestruct "Hpinv'" as ([[[[γx' γ1'] γ3'] γ4'] γq'] p'''') "[>% [>#Hevm2 Hps]]". inversion H2. subst. inversion H0. subst. destruct (decide (γ1 = γ1' ∧ γx = γx' ∧ γ3 = γ3' ∧ γ4 = γ4' ∧ γq = γq')) as [[? [? [? [? ?]]]]|Hneq]; subst. { ... ...
 ... ... @@ -36,7 +36,7 @@ Section defs. iApply IHxs'=>//. Qed. Definition perR' hd v v' := (⌜v = ((∅: unitR), DecAgree v')⌝ ∗ R v' ∗ allocated hd)%I. Definition perR' hd v v' := (⌜v = ((∅: unitR), to_agree 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. ... ... @@ -164,7 +164,7 @@ Lemma new_stack_spec' Φ RI: iDestruct (big_sepM_insert_later (perR R) m) as "H"=>//. iSplitL "Hox". { rewrite /evs /ev. eauto. } iExists (<[hd' := ((), DecAgree x)]> m). iExists (<[hd' := ((), to_agree x)]> m). iFrame. iApply "H". iFrame. iExists x. iFrame. rewrite /allocated. iSplitR "Hhd'1"; auto. } ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!