-
Notifications
You must be signed in to change notification settings - Fork 0
/
mono_list.v
198 lines (174 loc) · 7.89 KB
/
mono_list.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
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
52
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
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
(* https://gitlab.mpi-sws.org/iris/iris/-/blob/master/iris_unstable/base_logic/mono_list.v *)
(** This file is still experimental. See its tracking issue
https://gitlab.mpi-sws.org/iris/iris/-/issues/439 for details on remaining
issues before stabilization. *)
(** Ghost state for a append-only list, wrapping the [mono_listR] RA. This
provides three assertions:
- an authoritative proposition [mono_list_auth_own γ q l] for the authoritative
list [l]
- a persistent assertion [mono_list_lb_own γ l] witnessing that the authoritative
list is at least [l]
- a persistent assertion [mono_list_idx_own γ i a] witnessing that the index [i]
is [a] in the authoritative list.
The key rules are [mono_list_lb_own_valid], which asserts that an auth at [l]
and a lower-bound at [l'] imply that [l' `prefix_of` l], and [mono_list_update],
which allows one to grow the auth element by appending only. At any time the
auth list can be "snapshotted" with [mono_list_lb_own_get] to produce a
persistent lower-bound. *)
From iris.proofmode Require Import tactics.
From iris.algebra.lib Require Import mono_list.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export own.
From iris.prelude Require Import options.
Class mono_listG (A : Type) Σ :=
MonoListG { mono_list_inG : inG Σ (mono_listR (leibnizO A)) }.
Local Existing Instance mono_list_inG.
Definition mono_listΣ (A : Type) : gFunctors :=
#[GFunctor (mono_listR (leibnizO A))].
Global Instance subG_mono_listΣ {A Σ} :
subG (mono_listΣ A) Σ → (mono_listG A) Σ.
Proof. solve_inG. Qed.
Local Definition mono_list_auth_own_def `{!mono_listG A Σ}
(γ : gname) (q : Qp) (l : list A) : iProp Σ :=
own γ (●ML{#q} (l : listO (leibnizO A))).
Local Definition mono_list_auth_own_aux : seal (@mono_list_auth_own_def).
Proof. by eexists. Qed.
Definition mono_list_auth_own := mono_list_auth_own_aux.(unseal).
Local Definition mono_list_auth_own_unseal :
@mono_list_auth_own = @mono_list_auth_own_def := mono_list_auth_own_aux.(seal_eq).
Global Arguments mono_list_auth_own {A Σ _} γ q l.
Local Definition mono_list_lb_own_def `{!mono_listG A Σ}
(γ : gname) (l : list A) : iProp Σ :=
own γ (◯ML (l : listO (leibnizO A))).
Local Definition mono_list_lb_own_aux : seal (@mono_list_lb_own_def).
Proof. by eexists. Qed.
Definition mono_list_lb_own := mono_list_lb_own_aux.(unseal).
Local Definition mono_list_lb_own_unseal :
@mono_list_lb_own = @mono_list_lb_own_def := mono_list_lb_own_aux.(seal_eq).
Global Arguments mono_list_lb_own {A Σ _} γ l.
Definition mono_list_idx_own `{!mono_listG A Σ}
(γ : gname) (i : nat) (a : A) : iProp Σ :=
∃ l : list A, ⌜ l !! i = Some a ⌝ ∗ mono_list_lb_own γ l.
Local Ltac unseal := rewrite
/mono_list_idx_own ?mono_list_auth_own_unseal /mono_list_auth_own_def
?mono_list_lb_own_unseal /mono_list_lb_own_def.
Section mono_list_own.
Context `{!mono_listG A Σ}.
Implicit Types (l : list A) (i : nat) (a : A).
Global Instance mono_list_auth_own_timeless γ q l : Timeless (mono_list_auth_own γ q l).
Proof. unseal. apply _. Qed.
Global Instance mono_list_lb_own_timeless γ l : Timeless (mono_list_lb_own γ l).
Proof. unseal. apply _. Qed.
Global Instance mono_list_lb_own_persistent γ l : Persistent (mono_list_lb_own γ l).
Proof. unseal. apply _. Qed.
Global Instance mono_list_idx_own_timeless γ i a :
Timeless (mono_list_idx_own γ i a) := _.
Global Instance mono_list_idx_own_persistent γ i a :
Persistent (mono_list_idx_own γ i a) := _.
Global Instance mono_list_auth_own_fractional γ l :
Fractional (λ q, mono_list_auth_own γ q l).
Proof. unseal. intros p q. by rewrite -own_op -mono_list_auth_dfrac_op. Qed.
Global Instance mono_list_auth_own_as_fractional γ q l :
AsFractional (mono_list_auth_own γ q l) (λ q, mono_list_auth_own γ q l) q.
Proof. split; [auto|apply _]. Qed.
Lemma mono_list_auth_own_agree γ q1 q2 l1 l2 :
mono_list_auth_own γ q1 l1 -∗
mono_list_auth_own γ q2 l2 -∗
⌜(q1 + q2 ≤ 1)%Qp ∧ l1 = l2⌝.
Proof.
unseal. iIntros "H1 H2".
by iCombine "H1 H2" gives %?%mono_list_auth_dfrac_op_valid_L.
Qed.
Lemma mono_list_auth_own_exclusive γ l1 l2 :
mono_list_auth_own γ 1 l1 -∗ mono_list_auth_own γ 1 l2 -∗ False.
Proof.
iIntros "H1 H2".
iDestruct (mono_list_auth_own_agree with "H1 H2") as %[]; done.
Qed.
Lemma mono_list_auth_lb_valid γ q l1 l2 :
mono_list_auth_own γ q l1 -∗
mono_list_lb_own γ l2 -∗
⌜ (q ≤ 1)%Qp ∧ l2 `prefix_of` l1 ⌝.
Proof.
unseal. iIntros "Hauth Hlb".
by iCombine "Hauth Hlb" gives %?%mono_list_both_dfrac_valid_L.
Qed.
Lemma mono_list_auth_lb_lookup i γ q l1 l2 :
i < length l2 →
mono_list_auth_own γ q l1 -∗
mono_list_lb_own γ l2 -∗
⌜ l1 !! i = l2 !! i ⌝.
Proof.
iIntros (Hi) "Hauth Hlb".
iDestruct (mono_list_auth_lb_valid with "Hauth Hlb") as "[_ %Pref]".
assert (is_Some (l2 !! i)) as [v Hv] by by rewrite lookup_lt_is_Some.
rewrite Hv. eapply prefix_lookup_Some in Pref; eauto.
Qed.
Lemma mono_list_lb_valid γ l1 l2 :
mono_list_lb_own γ l1 -∗
mono_list_lb_own γ l2 -∗
⌜ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 ⌝.
Proof.
unseal. iIntros "H1 H2".
by iCombine "H1 H2" gives %?%mono_list_lb_op_valid_L.
Qed.
Lemma mono_list_lb_lookup i γ l1 l2 :
i < length l1 → i < length l2 →
mono_list_lb_own γ l1 -∗
mono_list_lb_own γ l2 -∗
⌜ l1 !! i = l2 !! i ⌝.
Proof.
iIntros (Hi1 Hi2) "H1 H2".
assert (is_Some (l1 !! i)) as [v1 Hv1] by by rewrite lookup_lt_is_Some.
assert (is_Some (l2 !! i)) as [v2 Hv2] by by rewrite lookup_lt_is_Some.
iDestruct (mono_list_lb_valid with "H1 H2") as "[%Pref|%Pref]";
eapply prefix_lookup_Some in Pref; eauto; rewrite Pref.
- by rewrite Hv1.
- by rewrite Hv2.
Qed.
Lemma mono_list_idx_agree γ i a1 a2 :
mono_list_idx_own γ i a1 -∗ mono_list_idx_own γ i a2 -∗ ⌜ a1 = a2 ⌝.
Proof.
iDestruct 1 as (l1 Hl1) "H1". iDestruct 1 as (l2 Hl2) "H2".
iDestruct (mono_list_lb_valid with "H1 H2") as %Hpre.
iPureIntro.
destruct Hpre as [Hpre|Hpre]; eapply prefix_lookup_Some in Hpre; eauto; congruence.
Qed.
Lemma mono_list_auth_idx_lookup γ q l i a :
mono_list_auth_own γ q l -∗ mono_list_idx_own γ i a -∗ ⌜ l !! i = Some a ⌝.
Proof.
iIntros "Hauth". iDestruct 1 as (l1 Hl1) "Hl1".
iDestruct (mono_list_auth_lb_valid with "Hauth Hl1") as %[_ Hpre].
iPureIntro.
eapply prefix_lookup_Some in Hpre; eauto; congruence.
Qed.
Lemma mono_list_lb_own_get γ q l :
mono_list_auth_own γ q l -∗ mono_list_lb_own γ l.
Proof. intros. unseal. by iApply own_mono; apply mono_list_included. Qed.
Lemma mono_list_lb_own_le {γ l} l' :
l' `prefix_of` l →
mono_list_lb_own γ l -∗ mono_list_lb_own γ l'.
Proof. unseal. intros. by iApply own_mono; apply mono_list_lb_mono. Qed.
Lemma mono_list_idx_own_get {γ l} i a :
l !! i = Some a →
mono_list_lb_own γ l -∗ mono_list_idx_own γ i a.
Proof. iIntros (Hli) "Hl". iExists l. by iFrame. Qed.
Lemma mono_list_own_alloc l :
⊢ |==> ∃ γ, mono_list_auth_own γ 1 l ∗ mono_list_lb_own γ l.
Proof.
unseal. setoid_rewrite <- own_op. by apply own_alloc, mono_list_both_valid_L.
Qed.
Lemma mono_list_auth_own_update {γ l} l' :
l `prefix_of` l' →
mono_list_auth_own γ 1 l ==∗ mono_list_auth_own γ 1 l' ∗ mono_list_lb_own γ l'.
Proof.
iIntros (?) "Hauth".
iAssert (mono_list_auth_own γ 1 l') with "[> Hauth]" as "Hauth".
{ unseal. iApply (own_update with "Hauth"). by apply mono_list_update. }
iModIntro. iSplit; [done|]. by iApply mono_list_lb_own_get.
Qed.
Lemma mono_list_auth_own_update_app {γ l} l' :
mono_list_auth_own γ 1 l ==∗
mono_list_auth_own γ 1 (l ++ l') ∗ mono_list_lb_own γ (l ++ l').
Proof. by apply mono_list_auth_own_update, prefix_app_r. Qed.
End mono_list_own.