invariant.v 12.4 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.

Hai Dang's avatar
Hai Dang committed
13 14 15
(** Public scalar relation *)
Definition arel (r: resUR) (s1 s2: scalar) : Prop :=
  match s1, s2 with
Hai Dang's avatar
Hai Dang committed
16
  | ScPoison, ScPoison => True
Hai Dang's avatar
Hai Dang committed
17 18 19 20 21 22
  | 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
23
      | Tagged t =>  h, r.(rtm) !! t  Some (to_tgkR tkPub, h)
Hai Dang's avatar
Hai Dang committed
24 25 26 27
      end
  | _, _ => False
  end.

Hai Dang's avatar
Hai Dang committed
28 29 30 31 32 33 34 35 36 37 38 39 40
Definition tmap_inv_pre (k: tag_kind) (t: ptr_id) (l: loc) (σt: state) : Prop :=
  match k with
  | tkLocal => True
  | _ =>
     stk pm opro, σt.(sst) !! l = Some stk 
      mkItem pm (Tagged t) opro  stk  pm  Disabled
  end.

Definition tmap_inv_post (k: tag_kind) (t: ptr_id) (l: loc) (σt: state) : Prop :=
  match k with
  | tkLocal =>
      σt.(sst) !! l = Some (init_stack (Tagged t))
  | tkUnique =>
Hai Dang's avatar
Hai Dang committed
41
       stk, σt.(sst) !! l = Some stk   opro stk',
Hai Dang's avatar
Hai Dang committed
42 43 44 45 46
        stk = mkItem Unique (Tagged t) opro :: stk'
  | tkPub =>
       stk, σt.(sst) !! l = Some stk  t  active_SRO stk
  end.

Hai Dang's avatar
Hai Dang committed
47 48
Definition tmap_inv (r: resUR) (σs σt: state) : Prop :=
   (t: ptr_id) (k: tag_kind) h, r.(rtm) !! t  Some (to_tgkR k, h) 
Hai Dang's avatar
Hai Dang committed
49 50 51 52 53 54 55 56 57 58 59
  (t < σt.(snp))%nat 
   (l: loc) (ss st: scalar),
    h !! l  Some (to_agree (ss, st)) 
    tmap_inv_pre k t l σt 
    (* as long as the tag [t] is in the stack [stk] (Disabled is
      considered not in), then its heaplet [h] agree with the state [σ] *)
    σt.(shp) !! l = Some st 
    σs.(shp) !! l = Some ss 
    (* If [k] ls Local, then the stack is a singleton.
      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. *)
Hai Dang's avatar
Hai Dang committed
60
    tmap_inv_post k t l σt.
Hai Dang's avatar
Hai Dang committed
61 62

Definition cmap_inv (r: resUR) (σ: state) : Prop :=
Hai Dang's avatar
Hai Dang committed
63 64 65 66 67 68 69 70 71 72
   (c: call_id) (T: tag_locs), r.(rcm) !! c  Excl' T 
  c  σ.(scs) 
  (* for any tag [t] owned by [c] *)
   (t: ptr_id) (L : gset loc), T !! t = Some L 
    (t  < σ.(snp))%nat 
    (* and any [l] protected by [t] *)
     l, l  L 
    (* 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
73

Hai Dang's avatar
Hai Dang committed
74 75 76
(* [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
77
   k h, r.(rtm) !! t  Some (to_tgkR k, h)  is_Some (h !! l) 
Hai Dang's avatar
Hai Dang committed
78 79 80 81 82
  ((* local *)
    k = tkLocal 
   (* protector *)
    (k = tkUnique   (c: call_id) T L,
        r.(rcm) !! c  Excl' T  T !! t = Some L  l  L)).
Hai Dang's avatar
Hai Dang committed
83

Hai Dang's avatar
Hai Dang committed
84 85 86
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
87 88 89 90
(** 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
91
   (l: loc), l  dom (gset loc) σt.(shp) 
Hai Dang's avatar
Hai Dang committed
92
    pub_loc r l σs σt  ( (t: ptr_id), priv_loc r l t).
Hai Dang's avatar
Hai Dang committed
93 94

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

(** 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.
103

Hai Dang's avatar
Hai Dang committed
104
(** Condition for resource before EndCall *)
Hai Dang's avatar
Hai Dang committed
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 :=
Hai Dang's avatar
Hai Dang committed
107
  r.(rcm) !! c  Some (Excl ).
Hai Dang's avatar
Hai Dang committed
108

Ralf Jung's avatar
Ralf Jung committed
109
Lemma res_end_call_sat r c :
Hai Dang's avatar
Hai Dang committed
110
   r  res_cs c   r  end_call_sat r c.
Ralf Jung's avatar
Ralf Jung committed
111 112 113
Proof.
  intros Hval [r' EQ]. rewrite /end_call_sat EQ.
  destruct r' as [[tmap' cmap'] lmap'].
Hai Dang's avatar
Hai Dang committed
114 115
  rewrite /res_cs !pair_op /= /rcm /= /to_cmUR fmap_insert fmap_empty insert_empty.
  apply cmap_lookup_op_l_equiv; last by rewrite lookup_insert.
Hai Dang's avatar
Hai Dang committed
116 117
  destruct r as [tmap cmap].
  destruct EQ as [EQt EQc]. simplify_eq/=.
Hai Dang's avatar
Hai Dang committed
118 119
  move : Hval. rewrite /to_cmUR fmap_insert fmap_empty insert_empty.
  intros Hval. apply Hval.
Ralf Jung's avatar
Ralf Jung committed
120 121
Qed.

Hai Dang's avatar
Hai Dang committed
122 123
Definition init_res : resUR := res_cs O .

Hai Dang's avatar
Hai Dang committed
124
Lemma wsat_init_state : wsat init_res init_state init_state.
Hai Dang's avatar
Hai Dang committed
125
Proof.
Hai Dang's avatar
Hai Dang committed
126
  split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
127 128
  - apply wf_init_state.
  - apply wf_init_state.
Hai Dang's avatar
Hai Dang committed
129
  - split; [done|]. intros ?; simpl.
Hai Dang's avatar
Hai Dang committed
130
    rewrite /to_cmUR lookup_fmap. destruct i.
Hai Dang's avatar
Hai Dang committed
131 132
    + rewrite lookup_singleton //.
    + rewrite lookup_singleton_ne //.
Hai Dang's avatar
Hai Dang committed
133
  - intros ??? HL. exfalso. move : HL. rewrite /= lookup_empty. by inversion 1.
Hai Dang's avatar
Hai Dang committed
134 135
  - intros ??. simpl. rewrite /rcm /init_res /= /to_cmUR lookup_fmap.
    destruct c.
Hai Dang's avatar
Hai Dang committed
136
    + rewrite lookup_singleton. intros Eq%Some_equiv_inj. simplify_eq.
Hai Dang's avatar
Hai Dang committed
137
      split; [by rewrite elem_of_list_singleton|]. intros ??. set_solver.
Hai Dang's avatar
Hai Dang committed
138
    + rewrite lookup_singleton_ne //. by inversion 1.
Hai Dang's avatar
Hai Dang committed
139
  - do 4 (split; [done|]). intros l. rewrite /= dom_empty. set_solver.
Hai Dang's avatar
Hai Dang committed
140 141
Qed.

Ralf Jung's avatar
Ralf Jung committed
142 143 144 145 146 147 148 149
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
150 151 152 153 154 155 156 157 158 159 160 161 162 163
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
164 165 166 167 168 169 170 171
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
172
  have HL1: Some (to_tgkR tkPub, h)  r2.(rtm) !! t2.
Hai Dang's avatar
Hai Dang committed
173
  { rewrite -HL. by apply lookup_included, prod_included. }
Hai Dang's avatar
Hai Dang committed
174
  apply option_included in HL1 as [?|[th1 [[tk2 h2] [? [Eq1 INCL]]]]]; [done|].
Hai Dang's avatar
Hai Dang committed
175
  simplify_eq. exists h2. rewrite Eq1 (_: tk2  to_tgkR tkPub) //.
Hai Dang's avatar
Hai Dang committed
176
  apply tagKindR_incl_eq; [done|].
Hai Dang's avatar
Hai Dang committed
177
  move : INCL => [[/=<- _//]|/prod_included [/= /csum_included Eq _]].
Hai Dang's avatar
Hai Dang committed
178 179
  - apply csum_included. right. right. exists (Cinr ()), (Cinr ()).
    do 2 (split; [done|]). apply csum_included. naive_solver.
Hai Dang's avatar
Hai Dang committed
180 181
  - have VL2:  tk2.
    { apply (pair_valid tk2 h2). rewrite -pair_valid.
Hai Dang's avatar
Hai Dang committed
182
      apply (lookup_valid_Some r2.(rtm) t2); [apply VAL|]. by rewrite Eq1. }
Hai Dang's avatar
Hai Dang committed
183
    destruct Eq as [|[|Eq]]; [by subst|naive_solver|].
Hai Dang's avatar
Hai Dang committed
184 185 186 187 188 189
    destruct Eq as [b [[|[]|] [? [? Eq%csum_included]]]]; simplify_eq;
      [naive_solver| |done].
    destruct Eq as [|[|Eq]]; [by subst|naive_solver|].
    apply csum_included.
    right. right. exists (Cinr ()), (Cinr ()).
    do 2 (split; [done|]). apply csum_included. naive_solver.
Hai Dang's avatar
Hai Dang committed
190 191 192 193 194 195
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
196 197 198
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
199
  intros LE l t (k & h & Eqh & Inl & PRIV).
Hai Dang's avatar
Hai Dang committed
200 201
  apply prod_included in LE as [LE ].
  apply pair_valid in VAL as [VAL ].
Hai Dang's avatar
Hai Dang committed
202
  exists k, h. split; last split; [|done|].
Hai Dang's avatar
Hai Dang committed
203 204 205 206 207 208 209
  { destruct PRIV as [|[]]; subst k.
    - by apply (tmap_lookup_op_local_included r1.(rtm)).
    - by apply (tmap_lookup_op_uniq_included r1.(rtm)). }
  destruct PRIV as [|(? & c & T & L & ? & ?)]; [by left|right].
  subst k. split; [done|].
  exists c, T, L. split; [|done].
  by apply (cmap_lookup_op_unique_included r1.(rcm)).
Hai Dang's avatar
Hai Dang committed
210 211
Qed.

212
Instance tmap_inv_proper : Proper (() ==> (=) ==> (=) ==> iff) tmap_inv.
Hai Dang's avatar
Hai Dang committed
213
Proof.
Hai Dang's avatar
Hai Dang committed
214
  intros r1 r2 [Eqt Eqc] ? σ ? ???. subst. rewrite /tmap_inv.
Hai Dang's avatar
Hai Dang committed
215
  by setoid_rewrite Eqt.
Hai Dang's avatar
Hai Dang committed
216 217 218 219
Qed.

Instance cmap_inv_proper : Proper (() ==> (=) ==> iff) cmap_inv.
Proof.
Hai Dang's avatar
Hai Dang committed
220
  intros r1 r2 [Eqt Eqc]  ? σ ?. subst. rewrite /cmap_inv.
Hai Dang's avatar
Hai Dang committed
221
  setoid_rewrite Eqc.
Hai Dang's avatar
Hai Dang committed
222
  split; intros EQ ?? Eq; specialize (EQ _ _ Eq); eauto.
Hai Dang's avatar
Hai Dang committed
223 224 225
Qed.

Instance arel_proper : Proper (() ==> (=) ==> (=) ==> iff) arel.
Hai Dang's avatar
Hai Dang committed
226
Proof. rewrite /arel. solve_proper. Qed.
Hai Dang's avatar
Hai Dang committed
227 228

Instance priv_loc_proper : Proper (() ==> (=) ==> (=) ==> iff) priv_loc.
Hai Dang's avatar
Hai Dang committed
229 230 231 232
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
233 234 235 236

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

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

Hai Dang's avatar
Hai Dang committed
243 244
Lemma cinv_lookup_in (r: resUR) (σ: state) c T:
  Wf σ  cmap_inv r σ  r.(rcm) !! c  Excl' T  (c < σ.(snc))%nat.
Hai Dang's avatar
Hai Dang committed
245
Proof.
Hai Dang's avatar
Hai Dang committed
246 247
  intros WF CINV EQ. specialize (CINV c T EQ).
  destruct CINV. by apply WF.
Hai Dang's avatar
Hai Dang committed
248 249
Qed.

Hai Dang's avatar
Hai Dang committed
250 251
Lemma cinv_lookup_in_eq (r: resUR) (σ: state) c T:
  Wf σ  cmap_inv r σ  r.(rcm) !! c = Excl' T  (c < σ.(snc))%nat.
Hai Dang's avatar
Hai Dang committed
252 253 254
Proof.
  intros WF CINV EQ. eapply cinv_lookup_in; eauto. by rewrite EQ.
Qed.
Hai Dang's avatar
Hai Dang committed
255 256 257 258 259 260 261

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
262 263 264

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
265
Proof. intros (?&?&?&?&?&?&?). by eapply srel_heap_dom. Qed.
Ralf Jung's avatar
Ralf Jung committed
266 267 268 269 270 271 272 273 274

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.
Hai Dang's avatar
Hai Dang committed
275 276
  destruct r as [tmap cmap].
  change (core (tmap, cmap)) with (core tmap, core cmap).
Ralf Jung's avatar
Ralf Jung committed
277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294
  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
295

Hai Dang's avatar
Hai Dang committed
296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312
Lemma vrel_length r vs vt :
  vrel r vs vt  length vs = length vt.
Proof. intros. eapply Forall2_length; eauto. Qed.

Lemma vrel_tag_included r vs vt t:
  vrel r vs vt  vs <<t t  vt <<t t.
Proof.
  intros VREL.
  split; intros IN l1 t1 [i Eqi]%elem_of_list_lookup;
    [destruct (Forall2_lookup_r _ _ _ _ _ VREL Eqi) as (ss & Eqss & AREL)
    |destruct (Forall2_lookup_l _ _ _ _ _ VREL Eqi) as (ss & Eqss & AREL)];
    apply elem_of_list_lookup_2 in Eqss;
    destruct ss as [| |ls ts|]; try done;
    specialize (IN _ _ Eqss);
    destruct t1, ts; try done; naive_solver.
Qed.

Hai Dang's avatar
Hai Dang committed
313 314 315
Lemma arel_res_tag_overwrite r t h1 k2 h2 k ss st
  (UNIQ: k = tkLocal  k = tkUnique) :
  arel (r  res_tag t k h1) ss st 
Hai Dang's avatar
Hai Dang committed
316
  arel (r  res_tag t k2 h2) ss st.
Hai Dang's avatar
Hai Dang committed
317
Proof.
Hai Dang's avatar
Hai Dang committed
318
  destruct ss as [| |? [t1|]|], st as [| |? []|]; auto; [|naive_solver].
Hai Dang's avatar
Hai Dang committed
319 320
  intros (?&?& h & Eqh). do 2 (split; [done|]).
  case (decide (t1 = t)) => ?; [subst t1|].
Hai Dang's avatar
Hai Dang committed
321
  - exfalso. move : Eqh. rewrite lookup_op res_tag_lookup.
Hai Dang's avatar
Hai Dang committed
322 323 324
    destruct UNIQ; subst k.
    + apply tagKindR_local_exclusive_l.
    + apply tagKindR_uniq_exclusive_l.
Hai Dang's avatar
Hai Dang committed
325
  - exists h. move : Eqh.
Hai Dang's avatar
Hai Dang committed
326
    by do 2 (rewrite lookup_op res_tag_lookup_ne; [|done]).
Hai Dang's avatar
Hai Dang committed
327
Qed.
Hai Dang's avatar
Hai Dang committed
328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343

Lemma arel_res_tag_dealloc r t h k ss st
  (UNIQ: k = tkLocal  k = tkUnique) :
  arel (r  res_tag t k h) ss st 
  arel r ss st.
Proof.
  destruct ss as [| |? [t1|]|], st as [| |? []|]; auto; [|naive_solver].
  intros (?&?& h' & Eqh). do 2 (split; [done|]).
  case (decide (t1 = t)) => ?; [subst t1|].
  - exfalso. move : Eqh. rewrite lookup_op res_tag_lookup.
    destruct UNIQ; subst k.
    + apply tagKindR_local_exclusive_l.
    + apply tagKindR_uniq_exclusive_l.
  - exists h'. move : Eqh.
    by rewrite lookup_op res_tag_lookup_ne // right_id.
Qed.