evmap.v 4.65 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
(* evmap.v -- generalized heap-like monoid composite *)
Zhen Zhang's avatar
Zhen Zhang committed
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's avatar
Zhen Zhang committed
7
  Context (K A: Type) (Q: cmraT) `{Countable K, EqDecision A}.
Zhen Zhang's avatar
Zhen Zhang committed
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's avatar
Zhen Zhang committed
17
  (* Some basic supporting lemmas *)
Zhen Zhang's avatar
Zhen Zhang committed
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's avatar
Zhen Zhang committed
52
  (* Evidence that k immutably maps to some fixed v *)
Zhen Zhang's avatar
Zhen Zhang committed
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's avatar
Zhen Zhang committed
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's avatar
Zhen Zhang committed
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.