evmap.v 4.65 KB
 Zhen Zhang committed Oct 19, 2016 1 ``````(* evmap.v -- generalized heap-like monoid composite *) `````` Zhen Zhang committed Oct 11, 2016 2 3 4 5 6 ``````From iris.program_logic Require Export invariants weakestpre. From iris.algebra Require Export auth frac gmap dec_agree. From iris.proofmode Require Import tactics. Section evmap. `````` Zhen Zhang committed Oct 19, 2016 7 `````` Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}. `````` Zhen Zhang committed Oct 11, 2016 8 9 10 11 12 13 14 15 16 `````` 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. `````` Zhen Zhang committed Oct 19, 2016 17 `````` (* Some basic supporting lemmas *) `````` Zhen Zhang committed Oct 11, 2016 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 `````` 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))}. `````` Zhen Zhang committed Oct 19, 2016 52 `````` (* Evidence that k immutably maps to some fixed v *) `````` Zhen Zhang committed Oct 11, 2016 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 `````` 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. Lemma evmap_alloc γm m k v q: m !! k = None → ✓ q → own γm (● m) ⊢ |=r=> own γm (● (<[ k := (q, DecAgree v) ]> m) ⋅ ◯ {[ k := (q, DecAgree v) ]}). Proof. iIntros (??) "Hm". iDestruct (own_update with "Hm") as "?"; last by iAssumption. apply auth_update_alloc. apply alloc_singleton_local_update=>//. Qed. 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 p x agy: m !! hd = Some (p, 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. `````` Zhen Zhang committed Oct 19, 2016 96 97 98 99 100 101 102 103 104 105 106 `````` 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. `````` Zhen Zhang committed Oct 11, 2016 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 `````` Lemma evmap_frag_agree_split γm p q1 q2 (a1 a2: A): own γm (◯ {[p := (q1, DecAgree a1)]}) ★ own γm (◯ {[p := (q2, DecAgree 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 := (q1, DecAgree a1)]} {[p := (q2, 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.``````