invariant.v 11.3 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
From stbor.lang Require Export defs steps_wf.
Hai Dang's avatar
Hai Dang committed
2
3
4
5
From stbor.sim Require Export cmra.

Set Default Proof Using "Type".

Hai Dang's avatar
Hai Dang committed
6
7
8
9
10
11
12
Instance dom_proper `{Countable K} {A : cmraT} :
  Proper (() ==> ()) (dom (M:=gmap K A) (gset K)).
Proof.
  intros m1 m2 Eq. apply elem_of_equiv. intros i.
  by rewrite !elem_of_dom Eq.
Qed.

13
14
(* TODO: define viewshift *)

Hai Dang's avatar
Hai Dang committed
15
16
17
(** Public scalar relation *)
Definition arel (r: resUR) (s1 s2: scalar) : Prop :=
  match s1, s2 with
Hai Dang's avatar
Hai Dang committed
18
  | ScPoison, ScPoison => True
Hai Dang's avatar
Hai Dang committed
19
20
21
22
23
24
  | ScInt n1, ScInt n2 => n1 = n2
  | ScFnPtr n1, ScFnPtr n2 => n1 = n2
  | ScPtr l1 tg1, ScPtr l2 tg2 =>
      l1 = l2  tg1 = tg2 
      match tg1 with
      | Untagged => True
Hai Dang's avatar
Hai Dang committed
25
      | Tagged t =>  h, r.(rtm) !! t  Some (to_tagKindR tkPub, h)
Hai Dang's avatar
Hai Dang committed
26
27
28
29
      end
  | _, _ => False
  end.

Hai Dang's avatar
Hai Dang committed
30
31
Definition tmap_inv (r: resUR) (σ: state) : Prop :=
   (t: ptr_id) (k: tag_kind) h, r.(rtm) !! t  Some (to_tagKindR k, h) 
Hai Dang's avatar
Hai Dang committed
32
33
34
35
36
37
38
39
40
41
42
43
44
45
    (t < σ.(snp))%nat 
     (l: loc) (s: scalar),
      h !! l  Some (to_agree s) 
       (stk: stack), σ.(sst) !! l = Some stk 
         pm opro, mkItem pm (Tagged t) opro  stk  pm  Disabled 
          (* as long as the tag [t] is in the stack [stk] (Disabled is
            considered not in), then its heaplet [h] agree with the state [σ] *)
          σ.(shp) !! l = Some s 
          (* If [k] is Unique, then [t] must be Unique at the top of [stk].
            Otherwise if [k] is Pub, then [t] can be among the top SRO items. *)
          match k with
          | tkUnique =>  stk', stk = mkItem Unique (Tagged t) opro :: stk'
          | tkPub => t  active_SRO stk
          end.
Hai Dang's avatar
Hai Dang committed
46
47

Definition cmap_inv (r: resUR) (σ: state) : Prop :=
Hai Dang's avatar
Hai Dang committed
48
   (c: call_id) (cs: callStateR), r.(rcm) !! c  Some cs 
Hai Dang's avatar
Hai Dang committed
49
50
51
52
53
54
  match cs with
  (* if c is a private call id *)
  | Cinl (Excl T) =>
      c  σ.(scs) 
      (* for any tag [t] owned by c *)
       (t: ptr_id), t  T 
Hai Dang's avatar
Hai Dang committed
55
        (t < σ.(snp))%nat 
Hai Dang's avatar
Hai Dang committed
56
57
58
59
60
61
62
        (* that protects the heaplet [h] *)
         k h, r.(rtm) !! t  Some (k, h) 
          (* if [l] is in that heaplet [h] *)
           (l: loc), l  dom (gset loc) h 
            (* then a c-protector must be in the stack of l *)
             stk pm, σ.(sst) !! l = Some stk 
              mkItem pm (Tagged t) (Some c)  stk  pm  Disabled
Hai Dang's avatar
Hai Dang committed
63
  (* if c is a public call id *)
Hai Dang's avatar
Hai Dang committed
64
  | Cinr _ => (c < σ.(snc))%nat
Hai Dang's avatar
Hai Dang committed
65
66
67
  | _ => False
  end.

Hai Dang's avatar
Hai Dang committed
68
Definition lmap_inv (r: resUR) (σs σt: state) : Prop :=
Hai Dang's avatar
Hai Dang committed
69
70
71
   (l: loc) t,
    (r.(rlm) !! l: optionR tagR)  Some (to_tagR t) 
    (t < σt.(snp))%nat 
Hai Dang's avatar
Hai Dang committed
72
    σt.(sst) !! l = Some (init_stack (Tagged t)) 
Hai Dang's avatar
Hai Dang committed
73
    σt.(shp) !! l = σs.(shp) !! l.
Hai Dang's avatar
Hai Dang committed
74

Hai Dang's avatar
Hai Dang committed
75
76
77
(* [l] is private w.r.t to some tag [t] if [t] is uniquely owned and protected
  by some call id [c] and [l] is in [t]'s heaplet [h]. *)
Definition priv_loc (r: resUR) (l: loc) (t: ptr_id) :=
Hai Dang's avatar
Hai Dang committed
78
79
80
81
   h, r.(rtm) !! t  Some (to_tagKindR tkUnique, h) 
  ((* local *) (r.(rlm) !! l: optionR tagR)  Some (to_tagR t) 
   (* protected *)  (c: call_id) (T: gset ptr_id),
      r.(rcm) !! c  Some (to_callStateR $ csOwned T)  t  T  l  dom (gset loc) h).
Hai Dang's avatar
Hai Dang committed
82

Hai Dang's avatar
Hai Dang committed
83
84
85
Definition pub_loc (r: resUR) (l: loc) (σs σt: state) :=
   st, σt.(shp) !! l = Some st   ss, σs.(shp) !! l = Some ss  arel r ss st.

Hai Dang's avatar
Hai Dang committed
86
87
88
89
(** State relation *)
Definition srel (r: resUR) (σs σt: state) : Prop :=
  σs.(sst) = σt.(sst)  σs.(snp) = σt.(snp) 
  σs.(scs) = σt.(scs)  σs.(snc) = σt.(snc) 
Hai Dang's avatar
Hai Dang committed
90
   (l: loc), l  dom (gset loc) σt.(shp) 
Hai Dang's avatar
Hai Dang committed
91
    pub_loc r l σs σt  ( (t: ptr_id), priv_loc r l t).
Hai Dang's avatar
Hai Dang committed
92
93

Definition wsat (r: resUR) (σs σt: state) : Prop :=
Hai Dang's avatar
Hai Dang committed
94
  (* Wellformedness *)
Hai Dang's avatar
Hai Dang committed
95
  Wf σs  Wf σt   r 
96
  (* Invariants *)
Hai Dang's avatar
Hai Dang committed
97
  tmap_inv r σt  cmap_inv r σt  srel r σs σt  lmap_inv r σs σt.
Hai Dang's avatar
Hai Dang committed
98
99
100
101

(** Value relation for function arguments/return values *)
(* Values passed among functions are public *)
Definition vrel (r: resUR) (v1 v2: value) := Forall2 (arel r) v1 v2.
102

Hai Dang's avatar
Hai Dang committed
103
(** Condition for resource before EndCall *)
Hai Dang's avatar
Hai Dang committed
104
105
106
(* The call id [c] to be end must not have any privately protected locations. *)
Definition end_call_sat (r: resUR) (c: call_id) : Prop :=
  r.(rcm) !! c  Some (to_callStateR csPub).
Hai Dang's avatar
Hai Dang committed
107

Ralf Jung's avatar
Ralf Jung committed
108
109
110
111
112
113
114
115
116
117
118
119
Lemma res_end_call_sat r c :
   r  res_callState c csPub  r  end_call_sat r c.
Proof.
  intros Hval [r' EQ]. rewrite /end_call_sat EQ.
  destruct r' as [[tmap' cmap'] lmap'].
  rewrite /res_callState. rewrite !pair_op /= /rcm /=.
  apply cmap_lookup_op_l_equiv_pub; last by rewrite lookup_insert.
  destruct r as [[tmap cmap] lmap].
  destruct EQ as [[EQt EQc] EQl]. simplify_eq/=.
  apply Hval.
Qed.

Hai Dang's avatar
Hai Dang committed
120
Definition init_res : resUR := ((ε, {[O := to_callStateR csPub]}), ε).
Hai Dang's avatar
Hai Dang committed
121
Lemma wsat_init_state : wsat init_res init_state init_state.
Hai Dang's avatar
Hai Dang committed
122
Proof.
Hai Dang's avatar
Hai Dang committed
123
  split; last split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
124
125
  - apply wf_init_state.
  - apply wf_init_state.
Hai Dang's avatar
Hai Dang committed
126
  - split; [|done]. split; [done|]. intros ?; simpl. destruct i.
Hai Dang's avatar
Hai Dang committed
127
128
    + rewrite lookup_singleton //.
    + rewrite lookup_singleton_ne //.
Hai Dang's avatar
Hai Dang committed
129
  - intros ??? HL. exfalso. move : HL. rewrite /= lookup_empty. by inversion 1.
Hai Dang's avatar
Hai Dang committed
130
131
  - intros ??. simpl. destruct c.
    + rewrite lookup_singleton. intros Eq%Some_equiv_inj.
Hai Dang's avatar
Hai Dang committed
132
133
      destruct cs as [[]| |]; [..|lia|]; by inversion Eq.
    + rewrite lookup_singleton_ne //. by inversion 1.
Hai Dang's avatar
Hai Dang committed
134
135
  - do 4 (split; [done|]). intros l. rewrite /= dom_empty. set_solver.
  - intros ?? HL. exfalso. move : HL. rewrite /= lookup_empty. by inversion 1.
Hai Dang's avatar
Hai Dang committed
136
137
Qed.

Ralf Jung's avatar
Ralf Jung committed
138
139
140
141
142
143
144
145
Lemma arel_ptr l tg :
  arel (res_tag tg tkPub ) (ScPtr l (Tagged tg)) (ScPtr l (Tagged tg)).
Proof.
  simpl. do 2 (split; first done).
  exists . rewrite /res_tag /rtm /=.
  rewrite lookup_insert fmap_empty. done.
Qed.

Hai Dang's avatar
Hai Dang committed
146
147
148
149
150
151
152
153
154
155
156
157
158
159
Lemma arel_eq (r: resUR) (s1 s2: scalar) :
  arel r s1 s2  s1 = s2.
Proof. destruct s1 as [| |? []|], s2 as [| |? []|]; simpl; try done; naive_solver. Qed.

Lemma vrel_eq (r: resUR) (v1 v2: value) :
  vrel r v1 v2  v1 = v2.
Proof.
  revert v2. induction v1 as [|s1 v1 IH]; intros v2 FA.
  { apply Forall2_nil_inv_l in FA. by subst. }
  destruct v2 as [|s2 v2]. { by apply Forall2_nil_inv_r in FA. }
  apply Forall2_cons_inv in FA as [Eq1 Eq2].
  f_equal. by apply (arel_eq _ _ _ Eq1). by apply IH.
Qed.

Hai Dang's avatar
Hai Dang committed
160
161
162
163
164
165
166
167
Lemma arel_mono (r1 r2 : resUR) (VAL:  r2) :
  r1  r2   s1 s2, arel r1 s1 s2  arel r2 s1 s2.
Proof.
  intros Le s1 s2. rewrite /arel.
  destruct s1 as [| |l1 t1|], s2 as [| |l2 t2|]; auto.
  intros [Eql [Eqt PV]]. subst. repeat split.
  destruct t2 as [t2|]; [|done].
  destruct PV as [h HL].
Hai Dang's avatar
Hai Dang committed
168
169
170
  have HL1: Some (to_tagKindR tkPub, h)  r2.(rtm) !! t2.
  { rewrite -HL. apply lookup_included, prod_included.
    by apply prod_included in Le as []. }
Hai Dang's avatar
Hai Dang committed
171
172
173
174
175
176
177
  apply option_included in HL1 as [?|[th1 [[tk2 h2] [? [Eq1 INCL]]]]]; [done|].
  simplify_eq. exists h2. rewrite Eq1 (_: tk2  to_tagKindR tkPub) //.
  apply tag_kind_incl_eq; [done|].
  move : INCL => [[/=<- _//]|/prod_included [/= /csum_included Eq _]].
  - apply csum_included. naive_solver.
  - have VL2:  tk2.
    { apply (pair_valid tk2 h2). rewrite -pair_valid.
Hai Dang's avatar
Hai Dang committed
178
      apply (lookup_valid_Some r2.(rtm) t2); [apply VAL|]. by rewrite Eq1. }
Hai Dang's avatar
Hai Dang committed
179
    destruct Eq as [|[|Eq]]; [by subst|naive_solver|].
Hai Dang's avatar
Hai Dang committed
180
    destruct Eq as [?[[][? [? ?]]]]. simplify_eq.
Hai Dang's avatar
Hai Dang committed
181
182
183
184
185
186
187
    apply csum_included. naive_solver.
Qed.

Lemma vrel_mono (r1 r2 : resUR) (VAL:  r2) :
  r1  r2   v1 v2, vrel r1 v1 v2  vrel r2 v1 v2.
Proof. intros Le v1 v2 VREL. by apply (Forall2_impl _ _ _ _ VREL), arel_mono. Qed.

Hai Dang's avatar
Hai Dang committed
188
189
190
Lemma priv_loc_mono (r1 r2 : resUR) (VAL:  r2) :
  r1  r2   l t, priv_loc r1 l t  priv_loc r2 l t.
Proof.
Hai Dang's avatar
Hai Dang committed
191
  intros LE l t (h & Eqh & PRIV).
Hai Dang's avatar
Hai Dang committed
192
193
  do 2 (apply prod_included in LE as [LE ]).
  do 2 (apply pair_valid in VAL as [VAL ]).
Hai Dang's avatar
Hai Dang committed
194
195
196
197
198
  exists h. split.
  { by apply (tmap_lookup_op_unique_included r1.(rtm)). }
  destruct PRIV as [|(c & T & ? & ?)]; [left|right].
  - by eapply lmap_lookup_op_included.
  - exists c, T. split; [|done]. by apply (cmap_lookup_op_unique_included r1.(rcm)).
Hai Dang's avatar
Hai Dang committed
199
200
Qed.

Hai Dang's avatar
Hai Dang committed
201
Instance tmap_inv_proper : Proper (() ==> (=) ==> iff) tmap_inv.
Hai Dang's avatar
Hai Dang committed
202
Proof.
Hai Dang's avatar
Hai Dang committed
203
  intros r1 r2 [[Eqt Eqc] Eqm] ? σ ?. subst. rewrite /tmap_inv.
Hai Dang's avatar
Hai Dang committed
204
  by setoid_rewrite Eqt.
Hai Dang's avatar
Hai Dang committed
205
206
207
208
Qed.

Instance cmap_inv_proper : Proper (() ==> (=) ==> iff) cmap_inv.
Proof.
Hai Dang's avatar
Hai Dang committed
209
  intros r1 r2 [[Eqt Eqc] Eqm]  ? σ ?. subst. rewrite /cmap_inv.
Hai Dang's avatar
Hai Dang committed
210
211
212
213
  setoid_rewrite Eqc.
  split; intros EQ ?? Eq; specialize (EQ _ _ Eq);
    destruct cs as [[]| |]; eauto;
    [by setoid_rewrite <- Eqt|by setoid_rewrite Eqt].
Hai Dang's avatar
Hai Dang committed
214
215
216
Qed.

Instance arel_proper : Proper (() ==> (=) ==> (=) ==> iff) arel.
Hai Dang's avatar
Hai Dang committed
217
Proof. rewrite /arel. solve_proper. Qed.
Hai Dang's avatar
Hai Dang committed
218
219

Instance priv_loc_proper : Proper (() ==> (=) ==> (=) ==> iff) priv_loc.
Hai Dang's avatar
Hai Dang committed
220
221
222
223
Proof. rewrite /priv_loc. solve_proper. Qed.

Instance pub_loc_proper : Proper (() ==> (=) ==> (=) ==> (=) ==> iff) pub_loc.
Proof. rewrite /pub_loc. intros ???Eq?????????. subst. by setoid_rewrite Eq. Qed.
Hai Dang's avatar
Hai Dang committed
224
225
226
227

Instance srel_proper : Proper (() ==> (=) ==> (=) ==> iff) srel.
Proof.
  intros r1 r2 Eqr ??????. subst. rewrite /srel.
Hai Dang's avatar
Hai Dang committed
228
  split; move => [-> [-> [-> [->]]]]; by setoid_rewrite Eqr.
Hai Dang's avatar
Hai Dang committed
229
230
Qed.

Hai Dang's avatar
Hai Dang committed
231
232
233
Instance lmap_inv_proper  : Proper (() ==> (=) ==> (=) ==> iff) lmap_inv.
Proof. intros r1 r2 Eqr ??????. subst. rewrite /lmap_inv. by setoid_rewrite Eqr. Qed.

Hai Dang's avatar
Hai Dang committed
234
235
Instance wsat_proper : Proper (() ==> (=) ==> (=) ==> iff) wsat.
Proof. solve_proper. Qed.
Hai Dang's avatar
Hai Dang committed
236
237

Lemma cinv_lookup_in (r: resUR) (σ: state) c cs:
Hai Dang's avatar
Hai Dang committed
238
  Wf σ  cmap_inv r σ  r.(rcm) !! c  Some cs  (c < σ.(snc))%nat.
Hai Dang's avatar
Hai Dang committed
239
240
241
242
243
244
245
Proof.
  intros WF CINV EQ. specialize (CINV c cs EQ).
  destruct cs as [[]| |]; [|done..].
  destruct CINV. by apply WF.
Qed.

Lemma cinv_lookup_in_eq (r: resUR) (σ: state) c cs:
Hai Dang's avatar
Hai Dang committed
246
  Wf σ  cmap_inv r σ  r.(rcm) !! c = Some cs  (c < σ.(snc))%nat.
Hai Dang's avatar
Hai Dang committed
247
248
249
Proof.
  intros WF CINV EQ. eapply cinv_lookup_in; eauto. by rewrite EQ.
Qed.
Hai Dang's avatar
Hai Dang committed
250
251
252
253
254
255
256

Lemma srel_heap_dom r σs σt :
  Wf σs  Wf σt  srel r σs σt  dom (gset loc) σt.(shp)  dom (gset loc) σs.(shp).
Proof.
  intros WFS WFT (EQS&?).
  rewrite (state_wf_dom _ WFS) (state_wf_dom _ WFT) EQS //.
Qed.
Hai Dang's avatar
Hai Dang committed
257
258
259

Lemma wsat_heap_dom r σs σt :
  wsat r σs σt  dom (gset loc) σt.(shp)  dom (gset loc) σs.(shp).
Hai Dang's avatar
Hai Dang committed
260
Proof. intros (?&?&?&?&?&?&?). by eapply srel_heap_dom. Qed.
Ralf Jung's avatar
Ralf Jung committed
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289

Lemma arel_persistent r a1 a2 :
  arel r a1 a2  arel (core r) a1 a2.
Proof.
  destruct a1, a2; try done. simpl.
  destruct tg; last done.
  intros (<- & <- & [h Hlk]).
  split; first done. split; first done.
  exists (core h). move: Hlk.
  destruct r as [[tmap cmap] lmap].
  change (core (tmap, cmap, lmap)) with (core tmap, core cmap, core lmap).
  rewrite /rtm /=. rewrite lookup_core=>->.
  rewrite /core /core' /=.
  rewrite {1}/pcore /cmra_pcore /=. rewrite /prod_pcore //.
Qed.

Lemma vrel_persistent r v1 v2 :
  vrel r v1 v2  vrel (core r) v1 v2.
Proof.
  rewrite /vrel=>Hrel. eapply Forall2_impl; first done.
  eauto using arel_persistent.
Qed.

Lemma vrel_list_persistent r vl1 vl2 :
  Forall2 (vrel r) vl1 vl2  Forall2 (vrel (core r)) vl1 vl2.
Proof.
  intros Hrel. eapply Forall2_impl; first done.
  eauto using vrel_persistent.
Qed.
Hai Dang's avatar
Hai Dang committed
290
291
292
293
294
295
296
297
298
299
300
301

Lemma arel_res_mapsto_overwrite_1  r l t v1 v2 ss st :
  arel (r  res_mapsto l [v1] t) ss st  arel (r  res_mapsto l [v2] t) ss st.
Proof.
  destruct ss as [| |? [t1|]|], st as [| |? []|]; simpl; auto; [|naive_solver].
  intros (?&?& h & Eqh). do 2 (split; [done|]).
  case (decide (t1 = t)) => ?; [subst t1|].
  - exfalso. move : Eqh. rewrite lookup_op res_mapsto_tlookup.
    apply tagKindR_exclusive.
  - exists h. move : Eqh.
    by do 2 (rewrite lookup_op res_mapsto_tlookup_ne; [|done]).
Qed.