steps_retag.v 70.7 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
From stbor.lang Require Export defs steps_foreach steps_list steps_wf steps_progress.
Hai Dang's avatar
Hai Dang committed
2 3 4

Set Default Proof Using "Type".

Hai Dang's avatar
Hai Dang committed
5 6
Definition tag_on_top (stks: stacks) l t pm : Prop :=
   prot, (stks !! l) = head = Some (mkItem pm (Tagged t) prot).
Hai Dang's avatar
Hai Dang committed
7

Hai Dang's avatar
Hai Dang committed
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
(** Active protector preserving *)
Definition active_preserving (cids: call_id_stack) (stk stk': stack) :=
   pm t c, c  cids  mkItem pm t (Some c)  stk  mkItem pm t (Some c)  stk'.

Instance active_preserving_preorder cids : PreOrder (active_preserving cids).
Proof.
  constructor.
  - intros ??. done.
  - intros ??? AS1 AS2 ?????. naive_solver.
Qed.

Lemma active_preserving_app_mono (cids: call_id_stack) (stk1 stk2 stk': stack) :
  active_preserving cids stk1 stk2 
  active_preserving cids (stk1 ++ stk') (stk2 ++ stk').
Proof.
  intros AS pm t c Inc. rewrite 2!elem_of_app.
  specialize (AS pm t c Inc). set_solver.
Qed.

Lemma remove_check_active_preserving cids stk stk' idx:
  remove_check cids stk idx = Some stk'  active_preserving cids stk stk'.
Proof.
  revert idx.
  induction stk as [|it stk IH]; intros idx; simpl.
  { destruct idx; [|done]. intros ??. by simplify_eq. }
  destruct idx as [|idx]; [intros ??; by simplify_eq|].
  case check_protector eqn:Eq; [|done].
  move => /IH AS pm t c IN /elem_of_cons [?|]; [|by apply AS].
  subst it. exfalso. move : Eq.
  by rewrite /check_protector /= /is_active bool_decide_true //.
Qed.

Lemma replace_check'_active_preserving cids acc stk stk':
  replace_check' cids acc stk = Some stk'  active_preserving cids stk stk'.
Proof.
  revert acc.
  induction stk as [|it stk IH]; intros acc; simpl.
  { intros. simplify_eq. by intros ?????%not_elem_of_nil. }
  case decide => ?; [case check_protector eqn:Eq; [|done]|].
  - move => /IH AS pm t c IN /elem_of_cons [?|]; [|by apply AS].
    subst it. exfalso. move : Eq.
    by rewrite /check_protector /= /is_active bool_decide_true //.
  - move => Eq pm t c IN /elem_of_cons [?|].
    + apply (replace_check'_acc_result _ _ _ _ Eq), elem_of_app. right.
      by apply elem_of_list_singleton.
    + by apply (IH _ Eq).
Qed.

Lemma replace_check_active_preserving cids stk stk':
  replace_check cids stk = Some stk'  active_preserving cids stk stk'.
Proof. by apply replace_check'_active_preserving. Qed.

Lemma access1_active_preserving stk stk' kind tg cids n:
  access1 stk kind tg cids = Some (n, stk') 
  active_preserving cids stk stk'.
Proof.
  rewrite /access1. case find_granting as [gip|]; [|done]. simpl.
  destruct kind.
  - case replace_check as [stk1|] eqn:Eq; [|done].
    simpl. intros. simplify_eq.
    rewrite -{1}(take_drop gip.1 stk).
    by apply active_preserving_app_mono, replace_check_active_preserving.
  - case find_first_write_incompatible as [idx|]; [|done]. simpl.
    case remove_check as [stk1|] eqn:Eq; [|done].
    simpl. intros. simplify_eq.
    rewrite -{1}(take_drop gip.1 stk).
    by eapply active_preserving_app_mono, remove_check_active_preserving.
Qed.

Lemma for_each_access1_active_preserving α cids l n tg kind α':
  for_each α l n false
          (λ stk, nstk'  access1 stk kind tg cids; Some nstk'.2) = Some α' 
   l stk, α !! l = Some stk 
   stk', α' !! l = Some stk'  active_preserving cids stk stk'.
Proof.
  intros EQ. destruct (for_each_lookup  _ _ _ _ _ EQ) as [EQ1 [EQ2 EQ3]].
  intros l1 stk1 Eq1.
  case (decide (l1.1 = l.1)) => [Eql|NEql];
    [case (decide (l.2  l1.2 < l.2 + n)) => [[Le Lt]|NIN]|].
  - have Eql2: l1 = l + Z.of_nat (Z.to_nat (l1.2 - l.2)). {
      destruct l, l1. move : Eql Le => /= -> ?.
      rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
    destruct (EQ1 (Z.to_nat (l1.2 - l.2)) stk1)
      as [stk [Eq [[n1 stk'] [Eq' Eq0]]%bind_Some]];
      [rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; lia|by rewrite -Eql2|].
    exists stk. rewrite -Eql2 in Eq. split; [done|]. simpl in Eq0. simplify_eq.
    eapply access1_active_preserving; eauto.
  - rewrite EQ3; [naive_solver|].
    intros i Lt Eq. apply NIN. rewrite Eq /=. lia.
  - rewrite EQ3; [naive_solver|].
    intros i Lt Eq. apply NEql. by rewrite Eq.
Qed.

Hai Dang's avatar
Hai Dang committed
101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123
Lemma for_each_access1_lookup_inv α cids l n tg kind α':
  for_each α l n false
          (λ stk, nstk'  access1 stk kind tg cids; Some nstk'.2) = Some α' 
   l stk, α !! l = Some stk 
   stk', α' !! l = Some stk' 
    (( n', access1 stk kind tg cids = Some (n', stk'))   α' !! l = α !! l).
Proof.
  intros EQ. destruct (for_each_lookup  _ _ _ _ _ EQ) as [EQ1 [EQ2 EQ3]].
  intros l1 stk1 Eq1.
  case (decide (l1.1 = l.1)) => [Eql|NEql];
    [case (decide (l.2  l1.2 < l.2 + n)) => [[Le Lt]|NIN]|].
  - have Eql2: l1 = l + Z.of_nat (Z.to_nat (l1.2 - l.2)). {
      destruct l, l1. move : Eql Le => /= -> ?.
      rewrite /shift_loc /= Z2Nat.id; [|lia]. f_equal. lia. }
    destruct (EQ1 (Z.to_nat (l1.2 - l.2)) stk1)
      as [stk [Eq [[n1 stk'] [Eq' Eq0]]%bind_Some]];
      [rewrite -(Nat2Z.id n) -Z2Nat.inj_lt; lia|by rewrite -Eql2|].
    simpl in Eq0. simplify_eq. rewrite -Eql2 in Eq. naive_solver.
  - rewrite EQ3; [naive_solver|].
    intros i Lt Eq. apply NIN. rewrite Eq /=. lia.
  - rewrite EQ3; [naive_solver|].
    intros i Lt Eq. apply NEql. by rewrite Eq.
Qed.
Hai Dang's avatar
Hai Dang committed
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 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 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 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326

(** Head preserving *)
Definition is_stack_head (it: item) (stk: stack) :=
   stk', stk = it :: stk'.

Lemma sublist_head_preserving t it it' stk stk' :
  stk' `sublist_of` stk 
  it'.(tg) = Tagged t  it.(tg) = Tagged t 
  it'  stk' 
  stack_item_tagged_NoDup stk 
  is_stack_head it stk 
  is_stack_head it stk'.
Proof.
  intros SUB Eqt' Eqt In' ND.
  induction SUB as [|???? IH|???? IH]; [done|..]; intros [stk1 ?]; simplify_eq;
    [by eexists|].
  exfalso. move : ND.
  rewrite /stack_item_tagged_NoDup filter_cons decide_True;
    last by rewrite /is_tagged Eqt.
  rewrite fmap_cons NoDup_cons. intros [NI ?].
  apply NI, elem_of_list_fmap. exists it'. split; [rewrite Eqt' Eqt //|].
  apply elem_of_list_filter. split. by rewrite /is_tagged Eqt'. by rewrite <-SUB.
Qed.

Lemma replace_check'_head_preserving stk stk' acc stk0 cids pm pm' t opro:
  stack_item_tagged_NoDup (acc ++ stk ++ stk0) 
  pm  Disabled 
  mkItem pm (Tagged t) opro  (stk' ++ stk0) 
  replace_check' cids acc stk = Some stk' 
  is_stack_head (mkItem pm' (Tagged t) opro) (acc ++ stk ++ stk0) 
  is_stack_head (mkItem pm' (Tagged t) opro) (stk' ++ stk0).
Proof.
  intros ND NDIS IN. revert acc ND.
  induction stk as [|it stk IH]; simpl; intros acc ND.
  { intros ?. by simplify_eq. }
  case decide => ?; [case check_protector; [|done]|];
    [|move => /IH; rewrite -(app_assoc acc [it] (stk ++ stk0)); naive_solver].
  move => RC.
  rewrite (app_assoc acc [it] (stk ++ stk0)).
  have ND3: stack_item_tagged_NoDup
    ((acc ++ [mkItem Disabled it.(tg) it.(protector)]) ++ stk ++ stk0).
  { move : ND. clear.
    rewrite (app_assoc acc [it]) 2!(Permutation_app_comm acc) -2!app_assoc.
    rewrite /stack_item_tagged_NoDup 2!filter_cons /=.
    case decide => ?; [rewrite decide_True //|rewrite decide_False //]. }
  intros HD. apply (IH _ ND3 RC). clear IH. move : HD.
  destruct acc as [|it1 acc]; last first.
  { simpl in *. move => [? Eq]. inversion Eq. simplify_eq. by eexists. }
  simpl. intros [stk2 Eq]. exfalso. simplify_eq; simpl in *.
  have IN1:= (replace_check'_acc_result _ _ _ _ RC).
  have IN': mkItem Disabled (Tagged t) opro  stk' ++ stk0 by set_solver. clear IN1.
  have ND4 := replace_check'_stack_item_tagged_NoDup_2 _ _ _ _ _ RC ND3.
  have EQ := stack_item_tagged_NoDup_eq _ _ _ _ ND4 IN IN' eq_refl eq_refl.
  by inversion EQ.
Qed.

Lemma replace_check_head_preserving stk stk' stk0 cids pm pm' t opro:
  stack_item_tagged_NoDup (stk ++ stk0) 
  pm  Disabled 
  mkItem pm (Tagged t) opro  (stk' ++ stk0) 
  replace_check cids stk = Some stk' 
  is_stack_head (mkItem pm' (Tagged t) opro) (stk ++ stk0) 
  is_stack_head (mkItem pm' (Tagged t) opro) (stk' ++ stk0).
Proof. intros. eapply replace_check'_head_preserving; eauto. done. Qed.

Lemma access1_head_preserving stk stk' kind tg cids n pm pm' t opro:
  stack_item_tagged_NoDup stk 
  pm  Disabled 
  mkItem pm (Tagged t) opro  stk' 
  access1 stk kind tg cids = Some (n, stk') 
  is_stack_head (mkItem pm' (Tagged t) opro) stk 
  is_stack_head (mkItem pm' (Tagged t) opro) stk'.
Proof.
  intros ND NDIS IN.
  rewrite /access1. case find_granting as [gip|]; [|done]. simpl.
  destruct kind.
  - case replace_check as [stk1|] eqn:Eq; [|done].
    simpl. intros ?. simplify_eq.
    rewrite -{1}(take_drop gip.1 stk). intros HD.
    rewrite -{1}(take_drop gip.1 stk) in ND.
    eapply replace_check_head_preserving; eauto.
  - case find_first_write_incompatible as [idx|]; [|done]. simpl.
    case remove_check as [stk1|] eqn:Eq; [|done].
    simpl. intros ?. simplify_eq.
    have SUB: stk1 ++ drop gip.1 stk `sublist_of` stk.
    { rewrite -{2}(take_drop gip.1 stk). apply sublist_app; [|done].
      move : Eq. apply remove_check_sublist. }
    eapply sublist_head_preserving; eauto. done.
Qed.

(** active_SRO preserving *)
Lemma active_SRO_cons_elem_of t it stk :
  t  active_SRO (it :: stk) 
  it.(perm) = SharedReadOnly  (it.(tg) = Tagged t  t  active_SRO stk).
Proof.
  simpl. destruct it.(perm); [set_solver..| |set_solver].
  case tg => [?|]; [rewrite elem_of_union elem_of_singleton|]; naive_solver.
Qed.

Lemma sublist_active_SRO_preserving t it stk stk' :
  stk' `sublist_of` stk 
  it.(tg) = Tagged t 
  it  stk' 
  stack_item_tagged_NoDup stk 
  t  active_SRO stk  t  active_SRO stk'.
Proof.
  intros SUB Eqt In' ND.
  induction SUB as [|it1 stk1 stk2 ? IH|it1 stk1 stk2 ? IH]; [done|..].
  - intros [? Eq]%active_SRO_cons_elem_of. apply active_SRO_cons_elem_of.
    split; [done|]. destruct Eq as [?|Eq]; [by left|].
    apply elem_of_cons in In' as [?|In'].
    + subst it. rewrite Eqt. by left.
    + right. apply IH; auto. by eapply stack_item_tagged_NoDup_cons_1.
  - intros [? Eq]%active_SRO_cons_elem_of.
    destruct Eq as [Eq|In2].
    + exfalso. move : ND.
      rewrite /stack_item_tagged_NoDup filter_cons decide_True;
        last by rewrite /is_tagged Eq.
      rewrite fmap_cons NoDup_cons. intros [NI ?].
      apply NI, elem_of_list_fmap. exists it. split; [rewrite Eqt Eq //|].
      apply elem_of_list_filter. split. by rewrite /is_tagged Eqt. by rewrite <-SUB.
    + apply IH; auto. by eapply stack_item_tagged_NoDup_cons_1.
Qed.

Lemma active_SRO_tag_eq_elem_of stk1 stk2 t :
  fmap tg stk1 = fmap tg stk2 
  Forall2 (λ pm1 pm2, pm1 = SharedReadOnly  pm2 = SharedReadOnly)
          (fmap perm stk1) (fmap perm stk2) 
  t  active_SRO stk1  t  active_SRO stk2.
Proof.
  revert stk2.
  induction stk1 as [|it stk1 IH]; intros stk2; [simpl; set_solver|].
  destruct stk2 as [|it2 stk2]; [naive_solver|].
  rewrite 4!fmap_cons. inversion 1 as [Eqt].
  inversion 1 as [|???? Eq1 FA]; subst. rewrite 2!active_SRO_cons_elem_of.
  intros [EqSRO Eq]. specialize (Eq1 EqSRO). split; [done|].
  destruct Eq as [Eq|In1].
  - rewrite -Eqt. by left.
  - right. by apply IH.
Qed.

Lemma replace_check'_active_SRO_preserving cids acc stk stk' stk0 t it:
  it.(tg) = Tagged t 
  it  stk' ++ stk0 
  replace_check' cids acc stk = Some stk' 
  stack_item_tagged_NoDup (acc ++ stk ++ stk0) 
  t  active_SRO (acc ++ stk ++ stk0)  t  active_SRO (stk' ++ stk0).
Proof.
  intros Eqt IN. revert acc.
  induction stk as [|it1 stk IH]; simpl; intros acc.
  { intros ?. by simplify_eq. }
  case decide => [EqU|?]; [case check_protector; [|done]|];
    [|move => /IH; rewrite -(app_assoc acc [it1] (stk ++ stk0)); naive_solver].
  move => RC ND.
  rewrite (app_assoc acc [it1] (stk ++ stk0)).
  have ND3: stack_item_tagged_NoDup
    ((acc ++ [mkItem Disabled it1.(tg) it1.(protector)]) ++ stk ++ stk0).
  { move : ND. clear.
    rewrite (app_assoc acc [it1]) 2!(Permutation_app_comm acc) -2!app_assoc.
    rewrite /stack_item_tagged_NoDup 2!filter_cons /=.
    case decide => ?; [rewrite decide_True //|rewrite decide_False //]. }
  intros HD. apply (IH _ RC ND3). clear IH. move : HD.
  apply active_SRO_tag_eq_elem_of.
  - by rewrite !fmap_app /=.
  - rewrite 2!(fmap_app _ _ (stk ++ stk0)).
    apply Forall2_app; [rewrite 2!fmap_app; apply Forall2_app|].
    + by apply Forall_Forall2, Forall_forall.
    + apply Forall2_cons; [|constructor]. by rewrite EqU.
    + by apply Forall_Forall2, Forall_forall.
Qed.

Lemma replace_check_active_SRO_preserving cids stk stk' stk0 it t:
  it.(tg) = Tagged t 
  it  stk' ++ stk0 
  replace_check cids stk = Some stk' 
  stack_item_tagged_NoDup (stk ++ stk0) 
  t  active_SRO (stk ++ stk0)  t  active_SRO (stk' ++ stk0).
Proof. by apply replace_check'_active_SRO_preserving. Qed.

Lemma access1_active_SRO_preserving stk stk' kind tg cids n pm t opro:
  stack_item_tagged_NoDup stk 
  mkItem pm (Tagged t) opro  stk' 
  access1 stk kind tg cids = Some (n, stk') 
  t  active_SRO stk  t  active_SRO stk'.
Proof.
  intros ND IN.
  rewrite /access1. case find_granting as [gip|]; [|done]. simpl.
  destruct kind.
  - case replace_check as [stk1|] eqn:Eq; [|done].
    simpl. intros ?. simplify_eq.
    rewrite -{1}(take_drop gip.1 stk). intros HD.
    rewrite -{1}(take_drop gip.1 stk) in ND.
    eapply replace_check_active_SRO_preserving; eauto. done.
  - case find_first_write_incompatible as [idx|]; [|done]. simpl.
    case remove_check as [stk1|] eqn:Eq; [|done].
    simpl. intros ?. simplify_eq.
    have SUB: stk1 ++ drop gip.1 stk `sublist_of` stk.
    { rewrite -{2}(take_drop gip.1 stk). apply sublist_app; [|done].
      move : Eq. apply remove_check_sublist. }
    eapply sublist_active_SRO_preserving; eauto. done.
Qed.

(** Removing incompatible items *)
Hai Dang's avatar
Hai Dang committed
327

Hai Dang's avatar
Hai Dang committed
328
Lemma find_granting_incompatible_head stk kind t ti idx pm pmi oproi
Hai Dang's avatar
Hai Dang committed
329 330 331 332
  (HD: is_stack_head (mkItem pmi (Tagged t) oproi) stk)
  (NEQ: Tagged t  ti) :
  find_granting stk kind ti = Some (idx, pm) 
  is_stack_head (mkItem pmi (Tagged t) oproi) (take idx stk).
Hai Dang's avatar
Hai Dang committed
333 334 335 336 337 338 339
Proof.
  destruct HD as [stk' Eqi]. rewrite Eqi.
  rewrite /find_granting /= decide_False; last (intros [_ Eq]; by inversion Eq).
  case list_find => [[idx' pm'] /=|//]. intros . simplify_eq. simpl.
  by eexists.
Qed.

Hai Dang's avatar
Hai Dang committed
340
(* Writing *)
Hai Dang's avatar
Hai Dang committed
341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386
Lemma find_first_write_incompatible_head stk pm idx t opro pmi
  (HD: is_stack_head (mkItem pmi t opro) stk)
  (NSRW: pmi  SharedReadWrite) :
  find_first_write_incompatible stk pm = Some idx  (0 < idx)%nat.
Proof.
  set it := (mkItem pmi t opro).
  destruct HD as [stk' Eqi]. rewrite Eqi.
  destruct pm; [..|done|done]; simpl.
  - intros. simplify_eq. lia.
  - rewrite reverse_cons.
    destruct (list_find_elem_of (λ it, it.(perm)  SharedReadWrite)
                (reverse stk' ++ [it]) it) as [[id fnd] Eqf]; [set_solver|done|].
    rewrite Eqf.
    intros. simplify_eq. apply list_find_Some in Eqf as [Eqi ?].
    apply lookup_lt_Some in Eqi.
    rewrite app_length /= reverse_length Nat.add_1_r in Eqi. lia.
Qed.

Lemma remove_check_incompatible_items cids stk stk' stk0 n it i t
  (ND: stack_item_tagged_NoDup (stk ++ stk0)) :
  it.(tg) = Tagged t  stk !! i = Some it  (i < n)%nat 
  remove_check cids stk n = Some stk' 
   it', it'.(tg) = Tagged t  it'  (stk' ++ stk0)  False.
Proof.
  intros Eqt. revert i stk stk0 ND.
  induction n as [|n IH]; simpl; intros i stk stk0 ND Eqit Lt; [lia|].
  destruct stk as [|it' stk]; [done|]. simpl.
  case check_protector; [|done].
  destruct i as [|i].
  - simpl in Eqit. simplify_eq.
    intros SUB%remove_check_sublist it' Eq' IN.
    have SUB': stk' ++ stk0 `sublist_of` stk ++ stk0 by apply sublist_app.
    rewrite -> SUB' in IN.
    clear -ND Eqt Eq' IN.
    move : ND.
    rewrite /stack_item_tagged_NoDup filter_cons decide_True;
            [|by rewrite /is_tagged Eqt].
    rewrite fmap_cons NoDup_cons Eqt -Eq'.
    intros [IN' _]. apply IN'. apply elem_of_list_fmap.
    exists it'. split; [done|]. apply elem_of_list_filter. by rewrite /is_tagged Eq'.
  - apply (IH i); [|done|lia]. by apply stack_item_tagged_NoDup_cons_1 in ND.
Qed.

Lemma access1_write_remove_incompatible_head stk t ti cids n stk'
  (ND: stack_item_tagged_NoDup stk) :
  ( oproi, is_stack_head (mkItem Unique (Tagged ti) oproi) stk) 
Hai Dang's avatar
Hai Dang committed
387 388
  access1 stk AccessWrite t cids = Some (n, stk') 
  Tagged ti  t 
Hai Dang's avatar
Hai Dang committed
389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406
   pm opro, (mkItem pm (Tagged ti) opro)  stk'  False.
Proof.
  intros HD. rewrite /access1.
  case find_granting as [[n' pm']|] eqn:GRANT; [|done]. simpl.
  case find_first_write_incompatible as [idx|] eqn:INC; [|done]. simpl.
  case remove_check as [stk1|] eqn:Eq; [|done].
  simpl. intros ?. simplify_eq.
  intros NEQ. destruct HD as [oproi HD].
  have HD' := find_granting_incompatible_head _ _ _ _ _ _ _ _ HD NEQ GRANT.
  have Gt0 := find_first_write_incompatible_head _ _ _ _ _ _ HD' (ltac:(done)) INC.
  rewrite -{1}(take_drop n stk) in ND.
  intros pm opro.
  have EQH : take n stk !! 0%nat = Some (mkItem Unique (Tagged ti) oproi).
  { destruct HD' as [? Eq']. by rewrite Eq'. }
  eapply (remove_check_incompatible_items _ _ _ _ idx
            (mkItem Unique (Tagged ti) oproi) O ti ND); done.
Qed.

Hai Dang's avatar
Hai Dang committed
407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448
(* Reading *)
Lemma replace_check'_incompatible_items cids acc stk stk' stk0 it t
  (ND: stack_item_tagged_NoDup (acc ++ stk ++ stk0)) :
  it.(tg) = Tagged t  it.(perm) = Unique  it  stk 
  replace_check' cids acc stk = Some stk' 
   it', it'.(tg) = Tagged t  it'  (stk' ++ stk0)  it'.(perm) = Disabled.
Proof.
  intros Eqt IU IN. revert acc ND.
  induction stk as [|it0 stk IH]; simpl; intros acc ND; [set_solver|].
  case decide => ?; [case check_protector; [|done]|]; last first.
  { move => /(IH ltac:(set_solver)).
    rewrite -(app_assoc acc [it0] (stk ++ stk0)).
    intros IH1 it' Eqit' Init'. apply IH1; [done..|]. clear -Init'. set_solver. }
  move => RC.
  have ND3: stack_item_tagged_NoDup
    ((acc ++ [mkItem Disabled it0.(tg) it0.(protector)]) ++ stk ++ stk0).
  { move : ND. clear.
    rewrite (app_assoc acc [it0]) 2!(Permutation_app_comm acc) -2!app_assoc.
    rewrite /stack_item_tagged_NoDup 2!filter_cons /=.
    case decide => ?; [rewrite decide_True //|rewrite decide_False //]. }
  have IN1:= (replace_check'_acc_result _ _ _ _ RC).
  have IN': mkItem Disabled it0.(tg) it0.(protector)  stk' ++ stk0 by set_solver.
  have ND4 := replace_check'_stack_item_tagged_NoDup_2 _ _ _ _ _ RC ND3.
  apply elem_of_cons in IN as [|IN].
  { intros it' Eqt' Init'. subst it0.
    have ? : it' = mkItem Disabled it.(tg) it.(protector).
    { apply (stack_item_tagged_NoDup_eq _ _ _ t ND4 Init' IN' Eqt').
      by rewrite Eqt. }
    by subst it'. }
  apply (IH IN _ ND3 RC).
Qed.

Lemma replace_check_incompatible_items cids stk stk' stk0 it t
  (ND: stack_item_tagged_NoDup (stk ++ stk0)) :
  it.(tg) = Tagged t  it.(perm) = Unique  it  stk 
  replace_check cids stk = Some stk' 
   it', it'.(tg) = Tagged t  it'  (stk' ++ stk0)  it'.(perm) = Disabled.
Proof. intros ????. eapply (replace_check'_incompatible_items _ []); eauto. Qed.

Lemma access1_read_replace_incompatible_head stk t ti cids n stk'
  (ND: stack_item_tagged_NoDup stk) :
  ( oproi, is_stack_head (mkItem Unique (Tagged ti) oproi) stk) 
Hai Dang's avatar
Hai Dang committed
449 450
  access1 stk AccessRead t cids = Some (n, stk') 
  Tagged ti  t 
Hai Dang's avatar
Hai Dang committed
451 452 453 454 455 456 457 458 459 460 461 462 463 464
   pm opro, (mkItem pm (Tagged ti) opro)  stk'  pm = Disabled.
Proof.
  intros HD. rewrite /access1.
  case find_granting as [[n' pm']|] eqn:GRANT; [|done]. simpl.
  case replace_check as [stk1|] eqn:Eq; [|done].
  simpl. intros ?. simplify_eq.
  intros NEQ pm opro. destruct HD as [oproi HD].
  rewrite -{1}(take_drop n stk) in ND.
  eapply (replace_check_incompatible_items _ _ _ _ (mkItem Unique (Tagged ti) oproi) ti ND);
    try done.
  have HD' := find_granting_incompatible_head _ _ _ _ _ _ _ _ HD NEQ GRANT.
  clear -HD'. destruct HD' as [? EqD]. rewrite EqD. by left.
Qed.

Hai Dang's avatar
Hai Dang committed
465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486
Lemma active_SRO_elem_of t stk :
  t  active_SRO stk   i it, stk !! i = Some it  it.(tg) = Tagged t 
  it.(perm) = SharedReadOnly 
   j jt, (j < i)%nat  stk !! j = Some jt  jt.(perm) = SharedReadOnly.
Proof.
  induction stk as [|it' stk IH]; simpl; [set_solver|].
  destruct it'.(perm) eqn:Eqp; [set_solver..| |set_solver].
  destruct it'.(tg) eqn:Eqt;
    [rewrite elem_of_union elem_of_singleton; intros [?|Eq]; [subst|]|].
  - exists O, it'. repeat split; [done..|intros; lia].
  - destruct (IH Eq) as (i & it1 & ? & ? & ? & HL).
    exists (S i), it1. repeat split; [done..|].
    intros j jt Lt. destruct j; simpl.
    + intros. by simplify_eq.
    + apply HL. lia.
  - intros Eq. destruct (IH Eq) as (i & it1 & ? & ? & ? & HL).
    exists (S i), it1. repeat split; [done..|].
    intros j jt Lt. destruct j; simpl.
    + intros. by simplify_eq.
    + apply HL. lia.
Qed.

Hai Dang's avatar
Hai Dang committed
487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503
Lemma active_SRO_elem_of_inv i it t stk :
  stk !! i = Some it  it.(tg) = Tagged t 
  it.(perm) = SharedReadOnly 
  ( j jt, (j < i)%nat  stk !! j = Some jt  jt.(perm) = SharedReadOnly) 
  t  active_SRO stk.
Proof.
  revert i.
  induction stk as [|it' stk IH]; [set_solver|].
  intros [|i]; intros Eq; simpl in Eq.
  { simplify_eq. intros. apply active_SRO_cons_elem_of. split; [done|by left]. }
  intros Eqt SRO PREV.
  apply active_SRO_cons_elem_of.
  have SRO' := PREV O it' ltac:(lia) eq_refl. split; [done|].
  right. apply (IH _ Eq Eqt SRO).
  intros j jt Lt. apply (PREV (S j) jt). lia.
Qed.

Hai Dang's avatar
Hai Dang committed
504 505
Lemma find_granting_incompatible_active_SRO stk t ti idx pm
  (HD: ti  active_SRO stk) :
Hai Dang's avatar
Hai Dang committed
506
  find_granting stk AccessWrite t = Some (idx, pm) 
Hai Dang's avatar
Hai Dang committed
507 508 509 510 511 512
  ti  active_SRO (take idx stk).
Proof.
  revert idx. induction stk as [|it stk IH]; simpl; intros idx; [set_solver|].
  move : HD. rewrite /find_granting /=.
  destruct it.(perm) eqn:Eqp; [set_solver..| |set_solver].
  rewrite decide_False; last (intros [PM _]; by rewrite Eqp in PM).
Hai Dang's avatar
Hai Dang committed
513
  destruct (list_find (matched_grant AccessWrite t) stk)
Hai Dang's avatar
Hai Dang committed
514 515 516 517 518 519 520 521 522 523 524 525
    as [[n' pm']|] eqn:Eql; [|done].
  simpl. intros IN ?. simplify_eq. rewrite /= Eqp. move : IN.
  destruct it.(tg) eqn:Eqt; simpl;
    [rewrite elem_of_union elem_of_singleton; intros [|IN]; [subst|]|]; simpl.
  - set_solver.
  - rewrite elem_of_union. right. apply IH. done. by rewrite /find_granting Eql.
  - intros ?. apply IH. done. by rewrite /find_granting Eql.
Qed.

Lemma find_first_write_incompatible_active_SRO stk pm idx :
  find_first_write_incompatible stk pm = Some idx 
   t, t  active_SRO stk   i it, stk !! i = Some it 
Hai Dang's avatar
Hai Dang committed
526 527 528 529
    it.(perm) = SharedReadOnly 
    it.(tg) = Tagged t  (i < idx)%nat 
    ( (j : nat) (jt : item), (j < i)%nat  stk !! j = Some jt 
        jt.(perm) = SharedReadOnly).
Hai Dang's avatar
Hai Dang committed
530 531 532 533 534 535
Proof.
  intros EF t IN.
  destruct (active_SRO_elem_of _ _ IN) as (i1 & it1 & Eqit1 & Eqt1 & Eqp1 & HL1).
  move  : EF.
  destruct pm; [| |done..].
  { simpl. intros. simplify_eq. exists i1, it1.
Hai Dang's avatar
Hai Dang committed
536
    repeat split; [done..| |done]. by eapply lookup_lt_Some. }
Hai Dang's avatar
Hai Dang committed
537 538 539 540 541 542
  simpl.
  destruct (list_find_elem_of (λ it, it.(perm)  SharedReadWrite) (reverse stk) it1)
    as [[n1 pm1] Eqpm1].
  { rewrite elem_of_reverse. by eapply elem_of_list_lookup_2. }
  { by rewrite Eqp1. }
  rewrite Eqpm1. intros. simplify_eq.
Hai Dang's avatar
Hai Dang committed
543
  exists i1, it1. repeat split; [done..| |done].
Hai Dang's avatar
Hai Dang committed
544 545 546 547 548 549 550 551 552 553 554
  apply list_find_Some_not_earlier in Eqpm1 as (Eqrv & Eqpmv & HLv).
  case (decide (i1 + n1 < length stk)%nat) => [?|]; [lia|].
  rewrite Nat.nlt_ge => GE. exfalso.
  destruct (reserve_lookup _ _ _ Eqit1) as (j & Eqj & Eql).
  have Lt: (j < n1)%nat by lia.
  specialize (HLv _ _ Lt Eqj). rewrite Eqp1 in HLv. by apply HLv.
Qed.

Lemma access1_write_remove_incompatible_active_SRO stk t ti cids n stk'
  (ND: stack_item_tagged_NoDup stk) :
  (ti  active_SRO stk) 
Hai Dang's avatar
Hai Dang committed
555
  access1 stk AccessWrite t cids = Some (n, stk') 
Hai Dang's avatar
Hai Dang committed
556 557 558 559 560 561 562 563 564 565
   pm opro, (mkItem pm (Tagged ti) opro)  stk'  False.
Proof.
  intros HD. rewrite /access1.
  case find_granting as [[n' pm']|] eqn:GRANT; [|done]. simpl.
  case find_first_write_incompatible as [idx|] eqn:INC; [|done]. simpl.
  case remove_check as [stk1|] eqn:Eq; [|done].
  simpl. intros ?. simplify_eq.
  intros NEQ.
  have HD' := find_granting_incompatible_active_SRO _ _ _ _ _ HD GRANT.
  destruct (find_first_write_incompatible_active_SRO _ _ _ INC _ HD')
Hai Dang's avatar
Hai Dang committed
566
    as (i & it & Eqi & Eqp & Eqt & Lt & HL).
Hai Dang's avatar
Hai Dang committed
567 568 569
  rewrite -{1}(take_drop n stk) in ND. intros ?.
  eapply (remove_check_incompatible_items _ _ _ _ idx it i ti ND); eauto.
Qed.
Hai Dang's avatar
Hai Dang committed
570

Hai Dang's avatar
Hai Dang committed
571
Lemma access1_incompatible_head_protector stk t ti kind cids n stk' c :
Hai Dang's avatar
Hai Dang committed
572
  (is_stack_head (mkItem Unique (Tagged t) (Some c)) stk) 
Hai Dang's avatar
Hai Dang committed
573
  c  cids 
Hai Dang's avatar
Hai Dang committed
574 575
  access1 stk kind ti cids = Some (n, stk') 
  ti = Tagged t.
Hai Dang's avatar
Hai Dang committed
576
Proof.
Hai Dang's avatar
Hai Dang committed
577
  intros HD ACTIVE. case (decide (Tagged t = ti)) => NEQ; [done|].
Hai Dang's avatar
Hai Dang committed
578 579 580 581 582
  rewrite /access1.
  case find_granting as [[n' pm']|] eqn:GRANT; [|done]. simpl.
  destruct kind.
  - case replace_check as [stk1|] eqn:Eq; [|done].
    simpl. intros ?. simplify_eq.
Hai Dang's avatar
Hai Dang committed
583
    have HD' := find_granting_incompatible_head _ _ _ _ _ _ _ _ HD NEQ GRANT.
Hai Dang's avatar
Hai Dang committed
584 585 586
    destruct HD' as [stk' Eqs].
    move : Eq.
    rewrite Eqs /replace_check /= /check_protector /= /is_active bool_decide_true //.
Hai Dang's avatar
Hai Dang committed
587
  - have HD' := find_granting_incompatible_head _ _ _ _ _ _ _ _ HD NEQ GRANT.
Hai Dang's avatar
Hai Dang committed
588 589 590 591 592 593 594 595
    case find_first_write_incompatible as [idx|] eqn:INC; [|done]. simpl.
    have NONEZ: (0 < idx)%nat.
    { eapply (find_first_write_incompatible_head _ _ _ _ _ _ HD'); eauto. }
    destruct HD' as [stk2 Eqs].
    rewrite Eqs /=. destruct idx; [lia|].
    rewrite /= /check_protector /= /is_active bool_decide_true //.
Qed.

Hai Dang's avatar
Hai Dang committed
596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627
(* Property of [t] that when used to access [stk], it will not change [stk] *)
Definition stack_preserving_tag
  (stk: stack) (t: ptr_id) (k: access_kind) : Prop :=
   n pm, find_granting stk k (Tagged t) = Some (n, pm) 
    match k with
    | AccessRead =>  it, it  take n stk  it.(perm)  Unique
    | AccessWrite => find_first_write_incompatible (take n stk) pm = Some O
    end.

Lemma stack_preserving_tag_elim stk t kind :
  stack_preserving_tag stk t kind 
   cids,  n stk',
  access1 stk kind (Tagged t) cids = Some (n, stk')  stk' = stk.
Proof.
Abort.

Lemma stack_preserving_tag_intro stk kind t cids n stk' :
  access1 stk kind (Tagged t) cids = Some (n, stk') 
  stack_preserving_tag stk' t kind.
Proof.
Abort.

Lemma stack_preserving_tag_unique_head stk t opro kind :
  is_stack_head (mkItem Unique (Tagged t) opro) stk 
  stack_preserving_tag stk t kind.
Proof.
Abort.

Lemma stack_preserving_tag_active_SRO stk t :
  t  active_SRO stk  stack_preserving_tag stk t AccessRead.
Proof.
Abort.
Hai Dang's avatar
Hai Dang committed
628 629 630


Lemma tag_unique_head_access cids stk t opro kind :
Hai Dang's avatar
Hai Dang committed
631 632
  is_stack_head (mkItem Unique t opro) stk 
   n, access1 stk kind t cids = Some (n, stk).
Hai Dang's avatar
Hai Dang committed
633 634 635
Proof.
  intros [stk1 Eqstk]. 
  rewrite /access1.
Hai Dang's avatar
Hai Dang committed
636 637
  have Eq1: list_find (matched_grant kind t) stk =
    Some (O, mkItem Unique t opro).
Hai Dang's avatar
Hai Dang committed
638 639
  { apply list_find_Some_not_earlier. split; last split.
    rewrite Eqstk //. done. intros; lia. }
Hai Dang's avatar
Hai Dang committed
640
  have Eq2: find_granting stk kind t = Some (O, Unique).
Hai Dang's avatar
Hai Dang committed
641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688
  { rewrite /= /find_granting Eq1 //. }
  rewrite Eq2 /=.
  exists O. by destruct kind.
Qed.

Lemma replace_check'_preserve cids acc stk :
  ( it, it  stk  it.(perm)  Unique) 
  replace_check' cids acc stk = Some (acc ++ stk).
Proof.
  revert acc. induction stk as [|it' stk IH]; intros acc IN.
  { rewrite /= app_nil_r //. }
  rewrite /= decide_False; last by (apply IN; left).
  rewrite (app_assoc acc [it'] stk). apply IH. set_solver.
Qed.

Lemma replace_check_preserve cids stk :
  ( it, it  stk  it.(perm)  Unique) 
  replace_check cids stk = Some stk.
Proof. apply replace_check'_preserve. Qed.

Lemma tag_SRO_top_access cids stk t :
  t  active_SRO stk 
   n, access1 stk AccessRead (Tagged t) cids = Some (n, stk).
Proof.
  intros IN.
  destruct (active_SRO_elem_of _ _ IN) as (i1 & it1 & Eqit1 & Eqt1 & Eqp1 & HL1).
  rewrite /= /access1.
   have Eq1: is_Some (list_find (matched_grant AccessRead (Tagged t)) stk).
  { apply (list_find_elem_of _ _ it1).
    by eapply elem_of_list_lookup_2. by rewrite /matched_grant Eqp1. }
  destruct Eq1 as [[n2 it2] Eq2].
  have Eq3: find_granting stk AccessRead (Tagged t) = Some (n2, it2.(perm)).
  { rewrite /= /find_granting Eq2 //. }
  rewrite Eq3 /=. exists n2.
  rewrite replace_check_preserve.
  - rewrite /= take_drop //.
  - apply list_find_Some_not_earlier in Eq2 as (Eq2 & GR & LT).
    have Lti1: (n2  i1)%nat.
    { case (decide (n2  i1)%nat) => [//|/Nat.nle_gt Lt].
      exfalso. apply (LT _ _ Lt Eqit1). rewrite /matched_grant Eqp1 //. }
    intros it [k Eqk]%elem_of_list_lookup_1.
    have Ltk : (k < n2)%nat.
    { rewrite -(take_length_le stk n2).
      by eapply lookup_lt_Some. apply Nat.lt_le_incl; by eapply lookup_lt_Some. }
    have HL: stk !! k = Some it. { rewrite -(lookup_take _ n2) //. }
    have Ltk2: (k < i1)%nat. { eapply Nat.lt_le_trans; eauto. }
    by rewrite (HL1 _ _ Ltk2 HL).
Qed.
Ralf Jung's avatar
Ralf Jung committed
689 690 691

(** Tag-on-top *)
Lemma tag_on_top_write σ l tg stks :
Hai Dang's avatar
Hai Dang committed
692
  tag_on_top σ.(sst) l tg Unique 
Ralf Jung's avatar
Ralf Jung committed
693
  memory_written (sst σ) (scs σ) l (Tagged tg) 1 = Some stks 
Hai Dang's avatar
Hai Dang committed
694
  tag_on_top stks l tg Unique.
Ralf Jung's avatar
Ralf Jung committed
695 696 697 698 699 700 701 702 703 704
Proof.
  rewrite /memory_written /tag_on_top /= shift_loc_0.
  destruct (sst σ !! l) eqn:Hlk; last done. simpl.
  destruct s as [|it st]; first done. simpl.
  destruct it as [perm tg' prot']. intros [prot ?]; simplify_eq/=.
  edestruct tag_unique_head_access as [n ->].
  { eexists. done. }
  simpl. intros. simplify_eq/=. eexists. rewrite lookup_insert.
  simpl. done.
Qed.
Hai Dang's avatar
Hai Dang committed
705

Hai Dang's avatar
Hai Dang committed
706 707
Lemma tag_on_top_grant_uniq_SRO stk old it cids  stk'
  (UNIQ: it.(perm) = Unique  it.(perm) = SharedReadOnly) :
Hai Dang's avatar
Hai Dang committed
708 709 710 711
  grant stk old it cids = Some stk'  is_stack_head it stk'.
Proof.
  rewrite /grant.
  case find_granting as [gip|]; [|done].
Hai Dang's avatar
Hai Dang committed
712 713 714
  destruct UNIQ as [UNIQ|UNIQ];
  rewrite /= UNIQ /=; (case access1 => [[n1 stk1]/=|//]);
  (destruct stk1; [|case decide => ?]; intros; simplify_eq; by eexists).
Hai Dang's avatar
Hai Dang committed
715 716
Qed.

Hai Dang's avatar
Hai Dang committed
717 718 719 720
Lemma tag_on_top_reborrowN_uniq_SRO α cids l n to tn pm α' pro
  (UNIQ: pm = Unique  pm = SharedReadOnly) :
  reborrowN α cids l n to (Tagged tn) pm pro = Some α' 
   i, (i < n)%nat  tag_on_top α' (l + i) tn pm.
Hai Dang's avatar
Hai Dang committed
721
Proof.
Hai Dang's avatar
Hai Dang committed
722
  intros RB i Lt.
Hai Dang's avatar
Hai Dang committed
723
  destruct (for_each_lookup_case_2 _ _ _ _ _ RB) as [EQ _].
Hai Dang's avatar
Hai Dang committed
724
  specialize (EQ _ Lt) as (stk & stk' & Eq & Eq' & GR).
Hai Dang's avatar
Hai Dang committed
725
  apply tag_on_top_grant_uniq_SRO in GR as [stk1 Eq1]; [|done].
Hai Dang's avatar
Hai Dang committed
726 727
  rewrite /tag_on_top Eq' Eq1 /=. by eexists.
Qed.
Hai Dang's avatar
Hai Dang committed
728

Hai Dang's avatar
Hai Dang committed
729 730 731
Lemma tag_on_top_retag_ref_uniq α cids nxtp l old T pro tn α' nxtp' :
  retag_ref α cids nxtp l old T (UniqueRef false) pro
    = Some (Tagged tn, α', nxtp') 
Hai Dang's avatar
Hai Dang committed
732
   i, (i < tsize T)%nat  tag_on_top α' (l + i) tn Unique.
Hai Dang's avatar
Hai Dang committed
733 734 735 736 737
Proof.
  intros RT i. destruct (tsize T) as [|n] eqn:Eqsz; [lia|].
  rewrite -Eqsz.
  move : RT. rewrite /retag_ref {1}Eqsz /=.
  case reborrowN as [α1|] eqn:RB; [|done]. simpl. intros ?. simplify_eq.
Hai Dang's avatar
Hai Dang committed
738
  eapply tag_on_top_reborrowN_uniq_SRO; eauto.
Hai Dang's avatar
Hai Dang committed
739 740
Qed.

Hai Dang's avatar
Hai Dang committed
741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764
Lemma tag_on_top_retag_ref_shr α cids nxtp l old T pro tn α' nxtp'
  (FRZ: is_freeze T) :
  retag_ref α cids nxtp l old T SharedRef pro
    = Some (Tagged tn, α', nxtp') 
   i, (i < tsize T)%nat  tag_on_top α' (l + i) tn SharedReadOnly.
Proof.
  intros RT i. destruct (tsize T) as [|n] eqn:Eqsz; [lia|].
  rewrite -Eqsz.
  move : RT. rewrite /retag_ref {1}Eqsz /= visit_freeze_sensitive_is_freeze //.
  case reborrowN as [α1|] eqn:RB; [|done]. simpl. intros ?. simplify_eq.
  eapply tag_on_top_reborrowN_uniq_SRO; eauto.
Qed.

Lemma tag_on_top_shr_active_SRO α l t :
  tag_on_top α l t SharedReadOnly 
   stk, α !! l = Some stk  t  active_SRO stk.
Proof.
  intros [pro Eq]. destruct (α !! l) as [stk|]; [|done].
  simpl in Eq. destruct stk as [|it stk']; [done|].
  simpl in Eq. simplify_eq. eexists. split; [done|].
  rewrite /= elem_of_union elem_of_singleton. by left.
Qed.

(* retag *)
Hai Dang's avatar
Hai Dang committed
765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799
Lemma retag_nxtp_change α cids c nxtp l otag ntag rk pk T α' nxtp'
  (TS: (O < tsize T)%nat)
  (RK: match pk with | RawPtr _ => rk = RawRt | _ => True end) :
  retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') 
  nxtp' = S nxtp 
  match ntag with
  | Untagged => True
  | Tagged t => nxtp = t
  end.
Proof.
  assert ( n, tsize T = S n) as [n EqT].
  { destruct (tsize T); [lia|by eexists]. }
  destruct pk as [[]| |]; [| |subst rk|]; rewrite /retag /= /retag_ref EqT;
  (case reborrow as [α1|]; [|done]); simpl; intros; by simplify_eq.
Qed.

Lemma retag_change_case α cids c nxtp l otag ntag rk pk T α' nxtp' :
  retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') 
  tsize T = O  α' = α  nxtp' = nxtp  ntag = otag 
  (O < tsize T)%nat 
    match pk, rk with
    | RawPtr _, RawRt => True
    | RawPtr _, _ => α' = α  nxtp' = nxtp  ntag = otag
    | _, _ => True
    end.
Proof.
  destruct (tsize T) as [|n] eqn:EqT.
  - rewrite /retag /retag_ref EqT /=.
    destruct pk as [[]| |]; [| |destruct rk|]; simpl; intros; simplify_eq;
      by left.
  - rewrite /retag /retag_ref EqT /=.
    destruct pk as [[]| |]; [| |destruct rk|]; simpl; intros; simplify_eq;
      right; (split; [lia|done]).
Qed.

Hai Dang's avatar
Hai Dang committed
800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820
Lemma retag_change_tag α cids c nxtp l otag ntag rk pk T α' nxtp' :
  retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') 
  ntag = otag 
  match ntag with
  | Tagged t => t = nxtp  nxtp' = S nxtp
  | _ => True
  end.
Proof.
  intros RT.
  destruct (retag_change_case _ _ _ _ _ _ _ _ _ _ _ _ RT) as [[?[?[??]]]|[? Eq]].
  - simplify_eq; by left.
  - destruct pk.
    + apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag.
    + destruct rk.
      * left. by destruct Eq as [_ []]; subst.
      * left. by destruct Eq as [_ []]; subst.
      * apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag.
      * left. by destruct Eq as [_ []]; subst.
    + apply retag_nxtp_change in RT as []; [|done..]. right. by destruct ntag.
Qed.

Hai Dang's avatar
Hai Dang committed
821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836
Lemma retag_change_nxtp α cids c nxtp l otag ntag rk pk T α' nxtp' :
  retag α nxtp cids c l otag rk pk T = Some (ntag, α', nxtp') 
  (nxtp  nxtp')%nat.
Proof.
  intros RT.
  destruct (retag_change_case _ _ _ _ _ _ _ _ _ _ _ _ RT) as [[?[?[??]]]|[? Eq]].
  - by simplify_eq.
  - destruct pk.
    + apply retag_nxtp_change in RT as []; [lia|done..].
    + destruct rk.
      * by destruct Eq as [_ [? _]]; subst.
      * by destruct Eq as [_ [? _]]; subst.
      * apply retag_nxtp_change in RT as []; [lia|done..].
      * by destruct Eq as [_ [? _]]; subst.
    + apply retag_nxtp_change in RT as []; [lia|done..].
Qed.
Hai Dang's avatar
Hai Dang committed
837

Hai Dang's avatar
Hai Dang committed
838 839 840 841 842 843 844 845 846 847 848 849
Lemma retag_change_ref_NZST α nxtp cids c l otag rk mut T ntag α' nxtp':
  (O < tsize T)%nat  
  retag α nxtp cids c l otag rk (RefPtr mut) T = Some (ntag, α', nxtp') 
  ntag = Tagged nxtp  nxtp' = S nxtp.
Proof.
  intros ST.
  assert ( n, tsize T = S n) as [n EqT].
  { destruct (tsize T); [lia|by eexists]. }
  destruct mut; rewrite /retag /= /retag_ref EqT;
  (case reborrow as [α1|]; [|done]); simpl; intros; by simplify_eq.
Qed.

Hai Dang's avatar
Hai Dang committed
850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958 959 960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058 1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130 1131 1132 1133 1134 1135 1136 1137 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147
Lemma unsafe_action_stacks_changed
  (f: stacks  _  nat  _  _) α l (last fsz usz: nat) α' ln cn
  (P: option stack  option stack  bool  Prop)
  (HF:  α1 α2 l n b, f α1 l n b = Some α2 
      ( l', ( (i : nat), (i < n)%nat  l'  l + i)  α2 !! l' = α1 !! l') 
      ( (i : nat), (i < n)%nat  P (α1 !! (l + i)) (α2 !! (l + i)) b)):
  unsafe_action f α l last fsz usz = Some (α', (ln, cn)) 
  (last  ln)%nat 
  ( l', ( (i : nat), (last  i < ln)%nat  l'  l + i)  α' !! l' = α !! l') 
  ( (i : nat), (last  i < ln)%nat   b, P (α !! (l + i)) (α' !! (l + i)) b).
Proof.
  rewrite /unsafe_action.
  case f as [α1|] eqn:Eqf1; [simpl|done]. case (f α1) eqn:Eqf2; [simpl|done].
  intros ?. simplify_eq. split; [lia|].
  destruct (HF _ _ _ _ _ Eqf1) as [HF1 Eq1].
  destruct (HF _ _ _ _ _ Eqf2) as [HF2 Eq2]. split.
  { intros ? NEQ. rewrite HF2; last first.
    - intros i Lt.
      rewrite shift_loc_assoc -Nat2Z.inj_add. apply NEQ. lia.
    - rewrite HF1 //.
      intros ??. rewrite shift_loc_assoc -Nat2Z.inj_add. apply NEQ. lia. }
  intros i [Le Lt].
  case (decide (i < last + fsz)%nat) => [Lt1|Ge1].
  - have Le1: (i - last < fsz)%nat by lia.
    have Eql: l + i = l + last + (i - last)%nat.
    { rewrite shift_loc_assoc. f_equal. lia. }
    specialize (Eq1 _ Le1). rewrite -Eql in Eq1. rewrite HF2.
    + by exists true.
    + intros j Ltj.
      rewrite shift_loc_assoc -Nat2Z.inj_add.
      intros ?%shift_loc_inj%Z_of_nat_inj. subst i. lia.
  - apply Nat.nlt_ge in Ge1.
    have Le1: (i - (last + fsz) < usz)%nat by lia.
    have Eql: l + i = l + (last + fsz)%nat + (i - (last + fsz))%nat.
    { rewrite shift_loc_assoc. f_equal. lia. }
    specialize (Eq2 _ Le1). rewrite -Eql in Eq2. rewrite -HF1.
    + by exists false.
    + intros ??. rewrite shift_loc_assoc -Nat2Z.inj_add.
      intros ?%shift_loc_inj%Z_of_nat_inj. subst i. lia.
Qed.


Lemma visit_freeze_sensitive'_stacks_changed l (f: stacks  _  _  _  _)
  α α' last cur T l' c'
  (P: option stack  option stack  bool  Prop) :
  let HF (f: stacks  loc  nat  bool  option stacks) :=
     α1 α2 l n b, f α1 l n b = Some α2 
      ( l', ( (i : nat), (i < n)%nat  l'  l + i)  α2 !! l' = α1 !! l') 
      ( (i : nat), (i < n)%nat  P (α1 !! (l + i)) (α2 !! (l + i)) b) in
  let UC α1 α2 (l: loc) (lo ln: nat) :=
    (lo  ln)%nat 
    ( l', ( (i : nat), (lo  i < ln)%nat  l'  l + i)  α2 !! l' = α1 !! l') 
    ( (i : nat), (lo  i < ln)%nat   b, P (α1 !! (l + i)) (α2 !! (l + i)) b) in
  HF f 
  visit_freeze_sensitive' l f α last cur T = Some (α', (l', c')) 
  UC α α' l last l'.
Proof.
  intros HF UC.
  apply (visit_freeze_sensitive'_elim
    (* general goal P *)
    (λ l f α l1 c1 T oalc,  α' l' c',
      HF f  oalc = Some (α', (l', c'))  UC α α' l l1 l')
    (λ l f _ _ _ Ts1 α l1 c1 Ts2 oalc,  α' l' c',
      HF f  oalc = Some (α', (l', c')) 
          UC α α' l l1 l')); rewrite /HF /UC.
  - clear. intros l f α1 l1 c1 s1 α2 l2 c2 HF ?.
    simplify_eq. split; [done|].
    split; [naive_solver|]. clear. intros i []. lia.
  - clear. intros l f α1 l1 c1 ?? α2 l2 c2 HF ?.
    simplify_eq. split; [done|].
    split; [naive_solver|]. clear. intros i []. lia.
  - (* Unsafe case *)
    clear. intros ?? α l1 c1 ? α2 l2 c2 HF.
    eapply unsafe_action_stacks_changed; eauto.
  - (* Union case *)
    clear. intros ????????? HF0. case is_freeze.
    + intros. simplify_eq. do 2 (split; [done|]).
      clear. intros ? []. lia.
    + intros UN. eapply unsafe_action_stacks_changed; eauto.
  - clear. intros ?????? IH ??? HF. case is_freeze.
    + intros. simplify_eq. do 2 (split; [done|]).
      clear. intros ? []. lia.
    + intros VS. eapply (IH _ _ _ HF); eauto.
  - (* Sum case *)
    clear. intros ????????? HF. case is_freeze.
    + intros. simplify_eq. do 2 (split; [done|]).
      clear. intros ? []. lia.
    + intros UN. eapply unsafe_action_stacks_changed; eauto.
  - clear. intros l f α1 l1 c1 Ts1 α2 l2 c2 α3 l3 c3 HF ?.
    simplify_eq. split; [done|].
    split; [naive_solver|]. clear. intros i []. lia.
  - (* Product case *)
    clear. intros l f α0 l0 c0 Ts1 α2 l2 c2 T Ts2 IH1 IH2 α3 l3 c3 HF.
    case visit_freeze_sensitive' as [alc|] eqn:Eqa; [|done].
    intros VS. destruct alc as [α1 [l1 c1]]. simpl in VS.
    destruct (IH2 α1 l1 c1 HF eq_refl) as [Le2 [IH21 IH22]].
    simpl in IH21, IH22.
    destruct (IH1 (α1, (l1,c1)) α3 l3 c3) as [Le1 [IH11 IH12]];
      [done..|simpl in Le1; split]; [lia|].
    simpl in IH11, IH12.
    split.
    + intros ? NC. rewrite IH11; [rewrite IH21 //|].
      * intros ??. apply NC. lia.
      * intros ??. apply NC. lia.
    + intros i [Le Lt].
      case (decide (l1  i)%nat) => [Gel1|Ltl1].
      * rewrite -IH21; [by apply IH12|].
        intros j [Lej Ltj] ?%shift_loc_inj%Z_of_nat_inj. subst j. lia.
      * apply Nat.nle_gt in Ltl1.
        rewrite IH11; [by apply IH22|].
        intros j [Lej Ltj] ?%shift_loc_inj%Z_of_nat_inj. subst j. lia.
Qed.

Lemma visit_freeze_sensitive_stacks_unchanged l
  (f: stacks  _  _  _  _)
  α α' T
  (P: option stack  option stack  bool  Prop) :
  ( α1 α2 l n b, f α1 l n b = Some α2 
      ( l', ( (i : nat), (i < n)%nat  l'  l + i)  α2 !! l' = α1 !! l') 
      ( (i : nat), (i < n)%nat  P (α1 !! (l + i)) (α2 !! (l + i)) b)) 
  visit_freeze_sensitive l T f α = Some α' 
  ( l', ( (i : nat), (i < tsize T)%nat  l'  l + i)  α' !! l' = α !! l') 
  ( (i : nat), (i < tsize T)%nat   b, P (α !! (l + i)) (α' !! (l + i)) b).
Proof.
  intros HF.
  rewrite /visit_freeze_sensitive.
  case visit_freeze_sensitive' as [[α1 [l1 c1]]|] eqn:Eq; [|done].
  intros Eqf.
  have Eq' := Eq.
  apply visit_freeze_sensitive'_offsets in Eq' as [_ Eq'].
  rewrite 2!Nat.add_0_l in Eq'.
  eapply visit_freeze_sensitive'_stacks_changed in Eq as [_ [EQ1 EQ2]]; [|done].
  specialize (HF _ _ _ _ _ Eqf) as [HF1 HF2].
  split.
  - intros l' NEq. rewrite HF1; last first.
    { intros i Lt. rewrite shift_loc_assoc -Nat2Z.inj_add.
      apply NEq. rewrite -Eq'. lia. }
    rewrite EQ1 //.
    intros i [_ Lti]. apply NEq. rewrite -Eq'. lia.
  - intros i Lt. rewrite -Eq' in Lt.
    case (decide (i < l1)%nat) => [Ltl1|Gel1].
    + rewrite HF1.
      * apply EQ2. split; [lia|done].
      * intros j Ltj. rewrite shift_loc_assoc_nat.
        intros ?%shift_loc_inj%Z_of_nat_inj. subst i. lia.
    + apply Nat.nlt_ge in Gel1. rewrite -EQ1.
      * have Ltc1: (i - l1 < c1)%nat by lia.
        specialize (HF2 _ Ltc1).
        have Eql: l + l1 + (i - l1)%nat = l + i.
        { rewrite shift_loc_assoc_nat. f_equal. lia. }
        rewrite Eql in HF2. by exists true.
      * intros j [_ Ltj] ?%shift_loc_inj%Z_of_nat_inj. subst i. lia.
Qed.

Lemma reborrowN_lookup_case (α1 α2 : stacks) cids l n old new pm protector
  (EQB : reborrowN α1 cids l n old new pm protector = Some α2) :
  ( l', ( (i : nat), (i < n)%nat  l'  l + i)  α2 !! l' = α1 !! l') 
  ( i, (i < n)%nat   stk stk',
    α1 !! (l + i) = Some stk 
    α2 !! (l + i) = Some stk' 
    let item := mkItem pm new protector in
    grant stk old item cids = Some stk').
Proof.
  destruct (for_each_lookup_case_2 _ _ _ _ _ EQB) as [HL1 HL2].
  split; [done|].
  intros i Lt. destruct (HL1 _ Lt) as (stk & stk' & Eq1 & Eq2 & GR).
  naive_solver.
Qed.

Lemma reborrowN_visit_freeze_sensitive_case α α' l T cids old new protector :
  let permB (b: bool) := if b then SharedReadOnly else SharedReadWrite in
  let item (b: bool) := mkItem (permB b) new protector in
  visit_freeze_sensitive l T
        (λ α' l' sz frozen,
          (* If is in Unsafe, use SharedReadWrite, otherwise SharedReadOnly *)
          reborrowN α' cids l' sz old new (permB frozen) protector) α = Some α' 
  ( l', ( (i : nat), (i < tsize T)%nat  l'  l + i)  α' !! l' = α !! l') 
  ( i, (i < tsize T)%nat   stk stk',
    α !! (l + i) = Some stk 
    α' !! (l + i) = Some stk'   b,
    grant stk old (item b) cids = Some stk').
Proof.
  intros permB item VS.
  set P: option stack  option stack  bool  Prop :=
    λ ostk ostk' b,  stk stk', ostk = Some stk  ostk' = Some stk' 
      grant stk old (item b) cids = Some stk'.
  apply (visit_freeze_sensitive_stacks_unchanged _ _ _ _ _ P) in VS.
  - destruct VS as [VS1 VS2]. split; [done|].
    intros i Lt. destruct (VS2 _ Lt) as (b & stk & stk' & Eq1 & Eq2 & Eq3).
    naive_solver.
  - clear. intros α1 α2 l n b [RB1 RB2]%reborrowN_lookup_case.
    split; [done|]. intros i Lt.
    specialize (RB2 _ Lt) as (stk & stk' & Eq1 & Eq2 & Eq3).
    rewrite Eq1 Eq2. exists stk, stk'. naive_solver.
Qed.

Lemma reborrow_Some α α' cids l old T rk new protector :
  reborrow α cids l old T rk new protector = Some α' 
  ( l', ( (i : nat), (i < tsize T)%nat  l'  l + i)  α' !! l' = α !! l') 
  ( i, (i < tsize T)%nat   stk stk',
    α !! (l + i) = Some stk 
    α' !! (l + i) = Some stk' 
    match rk with
    | SharedRef | RawRef false =>
       b : bool, grant stk old
                 (mkItem (if b then SharedReadOnly else SharedReadWrite)
                          new protector) cids = Some stk'
    | UniqueRef false =>
      grant stk old (mkItem Unique new protector) cids = Some stk'
    | UniqueRef true | RawRef true =>
      grant stk old (mkItem SharedReadWrite new protector) cids = Some stk'
    end).
Proof.
  destruct rk as [[]| |[]]; simpl.
  - apply reborrowN_lookup_case.
  - apply reborrowN_lookup_case.
  - apply reborrowN_visit_freeze_sensitive_case.
  - apply reborrowN_lookup_case.
  - apply reborrowN_visit_freeze_sensitive_case.
Qed.

Lemma retag_ref_Some α cids nxtp l old T rk protector new α' nxtp' :
  retag_ref α cids nxtp l old T rk protector = Some (new, α', nxtp') 
  ( l', ( (i : nat), (i < tsize T)%nat  l'  l + i)  α' !! l' = α !! l') 
  ( i, (i < tsize T)%nat   stk stk',
    α !! (l + i) = Some stk 
    α' !! (l + i) = Some stk' 
    match rk with
    | SharedRef | RawRef false =>
       b : bool, grant stk old
                 (mkItem (if b then SharedReadOnly else SharedReadWrite)
                          new protector) cids = Some stk'
    | UniqueRef false =>
      grant stk old (mkItem Unique new protector) cids = Some stk'
    | UniqueRef true | RawRef true =>
      grant stk old (mkItem SharedReadWrite new protector) cids = Some stk'
    end).
Proof.
  rewrite /retag_ref. destruct (tsize T) eqn:EqT.
  - intros. simplify_eq. split; [done|intros; lia].
  - rewrite -EqT. case reborrow as [α1|] eqn:Eq; [|done]. simpl.
    intros. simplify_eq. by apply reborrow_Some.
Qed.

Lemma retag_Some α nxtp c cids l old rk pk T new α' nxtp' :
  retag α nxtp cids c l old rk pk T = Some (new, α', nxtp') 
  ( l', ( (i : nat), (i < tsize T)%nat  l'  l + i)  α' !! l' = α !! l') 
  match pk, rk with
  (* Mutable reference *)
  | RefPtr Mutable, _ =>
      ( i, (i < tsize T)%nat   stk stk',
        α !! (l + i) = Some stk 
        α' !! (l + i) = Some stk' 
        let protector := adding_protector rk c in
        let perm := if (is_two_phase rk) then SharedReadWrite else Unique in
        grant stk old (mkItem perm new protector) cids = Some stk')
  (* Immutable reference *)
  | RefPtr Immutable, _ =>
      ( i, (i < tsize T)%nat   stk stk',
        α !! (l + i) = Some stk 
        α' !! (l + i) = Some stk' 
        let protector := adding_protector rk c in
         b : bool, grant stk old
                   (mkItem (if b then SharedReadOnly else SharedReadWrite)
                            new protector) cids = Some stk')
  (* If is both raw ptr and Raw retagging, no protector *)
  | RawPtr Mutable, RawRt =>
      ( i, (i < tsize T)%nat   stk stk',
        α !! (l + i) = Some stk 
        α' !! (l + i) = Some stk' 
        grant stk old (mkItem SharedReadWrite new None) cids = Some stk')
  | RawPtr Immutable, RawRt =>
      ( i, (i < tsize T)%nat   stk stk',
        α !! (l + i) = Some stk 
        α' !! (l + i) = Some stk' 
         b : bool, grant stk old
                 (mkItem (if b then SharedReadOnly else SharedReadWrite)
                          new None) cids = Some stk')
  (* Box pointer, no protector *)
  | BoxPtr, _ =>
      ( i, (i < tsize T)%nat   stk stk',
        α !! (l + i) = Some stk 
        α' !! (l + i) = Some stk' 
        grant stk old (mkItem Unique new None) cids = Some stk')
  (* Ignore Raw pointer otherwise *)
  | RawPtr _, _ => α' = α  nxtp' = nxtp  new = old
  end.
Proof.
  rewrite /retag. destruct (tsize T) as [|n] eqn:ST.
  { rewrite /retag_ref ST /=.
    destruct pk as [[]|[]|]; [| |destruct rk|destruct rk|]; intros; simplify_eq;
      (split; [done| intros; try done; lia]). }
  rewrite -ST.
  destruct pk as [[]|[]|]; [destruct rk| |destruct rk|destruct rk|];
    try apply retag_ref_Some;
    intros; by simplify_eq.
Qed.

Hai Dang's avatar
Hai Dang committed
1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158
Lemma retag_Some_dom α nxtp c cids l old rk pk T new α' nxtp'
  (RK: match pk with | RawPtr _ => rk = RawRt | _ => True end) :
  retag α nxtp cids c l old rk pk T = Some (new, α', nxtp') 
   i, (i < tsize T)%nat  (l + i)  dom (gset loc) α.
Proof.
  intros RT i Lti. rewrite elem_of_dom.
  destruct (retag_Some _ _ _ _ _ _ _ _ _ _ _ _ RT) as [_ EQ].
  destruct pk as [[]|[]|]; [| |subst rk..|];
    specialize (EQ _ Lti) as (?&?&?&_); by eexists.
Qed.

Hai Dang's avatar
Hai Dang committed
1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319 1320 1321 1322 1323 1324 1325 1326 1327 1328 1329 1330 1331 1332 1333 1334 1335 1336 1337 1338 1339 1340 1341 1342 1343 1344 1345 1346 1347 1348 1349 1350 1351 1352 1353 1354 1355 1356 1357 1358 1359 1360 1361 1362 1363 1364 1365 1366 1367 1368 1369 1370 1371 1372 1373 1374 1375 1376 1377 1378 1379 1380 1381 1382 1383 1384 1385 1386 1387 1388 1389 1390 1391 1392 1393 1394 1395 1396 1397 1398 1399 1400 1401 1402 1403 1404 1405 1406 1407 1408 1409 1410 1411 1412 1413 1414 1415 1416 1417 1418 1419 1420 1421 1422 1423 1424 1425 1426 1427 1428 1429 1430 1431 1432 1433 1434 1435 1436 1437 1438 1439 1440 1441 1442 1443 1444 1445 1446 1447 1448 1449 1450 1451 1452 1453 1454 1455 1456 1457 1458 1459 1460 1461 1462 1463 1464 1465 1466 1467 1468 1469 1470 1471 1472 1473 1474 1475 1476 1477 1478 1479 1480 1481 1482 1483 1484 1485 1486 1487 1488 1489 1490 1491 1492 1493 1494 1495 1496 1497 1498 1499 1500 1501 1502 1503 1504 1505 1506 1507 1508 1509 1510 1511 1512 1513 1514 1515 1516 1517 1518 1519 1520 1521 1522 1523 1524 1525 1526 1527 1528 1529 1530 1531 1532 1533 1534 1535 1536 1537 1538 1539 1540 1541 1542 1543 1544 1545 1546 1547 1548 1549 1550 1551 1552 1553 1554 1555 1556 1557 1558 1559 1560 1561 1562 1563 1564 1565 1566 1567 1568 1569 1570 1571 1572 1573 1574 1575 1576 1577 1578 1579 1580 1581 1582 1583 1584 1585 1586 1587 1588 1589 1590 1591 1592 1593 1594 1595 1596 1597 1598 1599 1600 1601 1602 1603 1604 1605 1606 1607 1608 1609 1610 1611 1612 1613 1614 1615 1616 1617 1618 1619 1620 1621 1622 1623 1624 1625 1626 1627 1628
Lemma grant_singleton_eq (it it': item) old cids stk' :
  grant [it] old it' cids = Some stk' 
  old = it.(tg).
Proof.
  rewrite /grant. case find_granting as [[n p]|] eqn:GR; [simpl|done].
  intros _.
  apply fmap_Some in GR as [[i it1] [FIND ?]]. simplify_eq.
  move : FIND. simpl. case decide => [MT|//]. intros. simplify_eq.
  by destruct MT.
Qed.

Lemma retag_Some_local α nxtp c cids l old rk pk T new α' nxtp' :
  retag α nxtp cids c l old rk pk T = Some (new, α', nxtp') 
   l' t',
    old  (Tagged t') 
    α !! l' = Some (init_stack (Tagged t')) 
    α' !! l' = Some (init_stack (Tagged t')).
Proof.
  intros RT l' t' NEQt Eqstk.
  destruct (retag_Some _ _ _ _ _ _ _ _ _ _ _ _ RT) as [NEQ EQ].
  destruct (block_case l l' (tsize T)) as [?|(i & Lti & ?)].
  { by rewrite NEQ. }
  subst l'.
  destruct pk as [[]|[]|].
  - exfalso. specialize (EQ _ Lti) as (stk & stk' & Eq1 & _ & GR).
    rewrite Eqstk in Eq1. simplify_eq. by apply grant_singleton_eq in GR.
  - exfalso. specialize (EQ _ Lti) as (stk & stk' & Eq1 & _ & b & GR).
    rewrite Eqstk in Eq1. simplify_eq. by apply grant_singleton_eq in GR.
  - destruct rk; try (destruct EQ; by subst α').
    exfalso. specialize (EQ _ Lti) as (stk & stk' & Eq1 & _ & GR).
    rewrite Eqstk in Eq1. simplify_eq. by apply grant_singleton_eq in GR.
  - destruct rk; try (destruct EQ; by subst α').
    exfalso. specialize (EQ _ Lti) as (stk & stk' & Eq1 & _ & b & GR).
    rewrite Eqstk in Eq1. simplify_eq. by apply grant_singleton_eq in GR.
  - exfalso. specialize (EQ _ Lti) as (stk & stk' & Eq1 & _ & GR).
    rewrite Eqstk in Eq1. simplify_eq. by apply grant_singleton_eq in GR.
Qed.

Lemma grant_in_SRW stk old it cids stk' it0
  (SRW: it.(perm) = SharedReadWrite) (NEQ: it  it0) :
  grant stk old it cids = Some stk' 
  it0  stk'  it0  stk.
Proof.
  rewrite /grant. case find_granting as [[n p]|] eqn:FR; [|done].
  rewrite /= SRW.
  case find_first_write_incompatible as [n'|] eqn:FI; [|done].
  rewrite /= => ?. simplify_eq.
  move => /item_insert_dedup_subseteq /elem_of_cons [//|//].
Qed.

Lemma grant_in_non_SRW stk old it cids stk' it0
  (SRW: it.(perm)  SharedReadWrite) (NEQ: it  it0)
  (ND: it0.(perm)  Disabled) :
  grant stk old it cids = Some stk' 
  it0  stk'  it0  stk.
Proof.
  rewrite /grant. case find_granting as [[n p]|] eqn:FR; [|done].
  case it.(perm) eqn:Eqp; [|done|..];
    cbn -[item_insert_dedup];
    (case access1 as [[n' stk1]|] eqn:ACC; [|done]);
    cbn -[item_insert_dedup];
    intros ?; simplify_eq;
    (move => /item_insert_dedup_subseteq /elem_of_cons [//|//]);
    intros IN;
    apply access1_tagged_sublist in ACC;
    specialize (ACC _ IN) as (it2 & IN2 & HT & HPR & HP); specialize (HP ND).
    - have ?: it2 = it0. { destruct it2, it0; simpl in *; by subst. }
      by subst it2.
    - have ?: it2 = it0. { destruct it2, it0; simpl in *; by subst. }
      by subst it2.
    - have ?: it2 = it0. { destruct it2, it0; simpl in *; by subst. }
      by subst it2.
Qed.

Lemma grant_in_preserve stk old it cids stk' it0
  (NEQ: it  it0) (ND: it0.(perm)  Disabled) :
  grant stk old it cids = Some stk' 
  it0  stk'  it0  stk.
Proof.
  case (decide (it.(perm) = SharedReadWrite)) => ?.
  - by apply grant_in_SRW.
  - by apply grant_in_non_SRW.
Qed.

Lemma retag_item_in α nxtp c cids l old rk pk T new α' nxtp' :
  retag α nxtp cids c l old rk pk T = Some (new, α', nxtp') 
   l' stk' t' it',
    α' !! l' = Some stk' 
    it'  stk'  it'.(tg) = Tagged t'  it'.(perm)  Disabled 
    (t' < nxtp)%nat 
     stk, α !! l' = Some stk  it'  stk.
Proof.
  intros RT l' stk' t' it' Eqstk' In' Eqt' ND' Lt'.
  destruct (retag_Some _ _ _ _ _ _ _ _ _ _ _ _ RT) as [NEQ EQ].
  destruct (block_case l l' (tsize T)) as [?|(i & Lti & ?)].
  { rewrite NEQ // in Eqstk'. naive_solver. }
  assert ( sz, tsize T = S sz) as [sz Eqsz].
  { destruct (tsize T); [lia|by eexists]. }
  subst l'.
  move : RT. rewrite /retag /= /retag_ref Eqsz.
  destruct pk as [[]|[]|].
  - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR). simplify_eq.
    case reborrow as [α1|]; [|done]. simpl. intros. simplify_eq.
    exists stk1. split; [done|].
    move : GR In'.
    apply grant_in_preserve; [|done].
    intros ?; subst it'. simpl in Eqt'. simplify_eq. lia.
  - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & b & GR). simplify_eq.
    case reborrow as [α1|]; [|done]. simpl. intros. simplify_eq.
    exists stk1. split; [done|].
    move : GR In'.
    apply grant_in_preserve; [|done].
    intros ?; subst it'. simpl in Eqt'. simplify_eq. lia.
  - destruct rk; [by intros; simplify_eq; naive_solver..|
                  |intros; simplify_eq; naive_solver].
    specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR). simplify_eq.
    case reborrow as [α1|]; [|done]. simpl. intros. simplify_eq.
    exists stk1. split; [done|].
    move : GR In'. apply grant_in_SRW; [done|intros ?; by subst it'].
  - destruct rk; [by intros; simplify_eq; naive_solver..|
                  |intros; simplify_eq; naive_solver].
    specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & b & GR). simplify_eq.
    case reborrow as [α1|]; [|done]. simpl. intros. simplify_eq.
    exists stk1. split; [done|].
    move : GR In'. apply grant_in_preserve; [intros ?; by subst it'|done].
  - specialize (EQ _ Lti) as (stk1 & stk2 & Eq1 & Eq2 & GR). simplify_eq.
    case reborrow as [α1|]; [|done]. simpl. intros. simplify_eq.
    exists stk1. split; [done|].
    move : GR In'.
    apply grant_in_preserve; [|done].
    intros ?; subst it'. simpl in Eqt'. simplify_eq. lia.
Qed.

(* Lemma item_insert_dedup_lookup stk it i (IS: is_Some (stk !! i)):
   j, (item_insert_dedup stk it i) !! j = Some it 
    (j = i  (1  i  j = i - 1)%nat) 
    ( j', (j' < j)%nat  (item_insert_dedup stk it i) !! j' = stk !! j').
Proof.
  destruct i as [|i]; simpl.
  - destruct stk as [|it' stk']; [by destruct IS|]. case decide => [->|?].
    + exists O. naive_solver.
    + exists O. split; [done|]. split;[by left| intros; lia].
  - destruct IS as [it1 Eq1]. rewrite Eq1.
    destruct (stk !! i) as [it2|] eqn:Eq2; last first.
    { apply lookup_ge_None_1 in Eq2. apply lookup_lt_Some in Eq1. lia. }
    case decide => [->|?]; [|case decide => [->|?]].
    + exists i. split; [done|]. rewrite Nat.sub_0_r. split; [right; lia|done].
    + exists (S i). split; [done|]. split; [by left|done].
    + exists (S i). rewrite Nat.sub_0_r. split; last split; [|by left|].
      * rewrite list_lookup_middle // take_length_le //.
        by eapply Nat.lt_le_incl, lookup_lt_Some.
      * intros j' Lt'. rewrite lookup_app_l; [apply lookup_take; lia|].
        rewrite take_length_le //. by eapply Nat.lt_le_incl, lookup_lt_Some.
Qed. *)

Lemma find_granting_Some stk kind bor i pi :
  find_granting stk kind bor = Some (i, pi) 
  is_Some (stk !! i) 
   j jt, (j < i)%nat  stk !! j = Some jt 
  ¬ (grants jt.(perm) kind  jt.(tg) = bor).
Proof.
  move => /fmap_Some [[i' pi'] [/list_find_Some_not_earlier [Eq1 [MG LT]] Eq2]].
  simplify_eq. simpl. split; [by eexists|by apply LT].
Qed.

Lemma item_insert_dedup_new stk new i (NIN: new  stk) (IS: is_Some (stk !! i)):
  item_insert_dedup stk new i = take i stk ++ new :: drop i stk.
Proof.
  destruct i as [|i]; simpl.
  - destruct stk as [|it stk]; [done|]. rewrite decide_False //.
    intros ?. subst. apply NIN. by left.
  - destruct IS as [its Eqs]. rewrite Eqs.
    destruct (stk !! i) as [it|] eqn:Eq; last first.
    { apply lookup_ge_None_1 in Eq. apply lookup_lt_Some in Eqs. lia. }
    rewrite decide_False; last first.
    { intros ?. subst. by eapply NIN, elem_of_list_lookup_2. }
    rewrite decide_False //.
    intros ?. subst. by eapply NIN, elem_of_list_lookup_2.
Qed.

Lemma item_insert_dedup_case stk new i :
   item_insert_dedup stk new i = take i stk ++ new :: drop i stk 
   item_insert_dedup stk new i = stk.
Proof.
  (* intros [it Eqit]. *) destruct i as [|i]; simpl.
  - destruct stk; simpl; [by left|].
    case decide =>?; [subst new|]; [by right|by left].
  - destruct (stk !! S i) eqn: Eqit.
    + have Lt := lookup_lt_Some _ _ _ Eqit.
      destruct (lookup_lt_is_Some_2 stk i) as [it' Eqit']; [lia|].
      rewrite Eqit'.
      case decide => ?; [subst new|]; [by right|].
      case decide => ?; [subst new|]; [by right|by left].
    + destruct (stk !! i) eqn: Eqit'; [|by left].
      case decide => ?; [subst new|]; [by right|by left].
Qed.

Lemma find_first_write_incompatible_le stk p n :
  find_first_write_incompatible stk p = Some n 
  (n  length stk)%nat.
Proof.
  destruct p; simpl; [by intros; simplify_eq| |done..].
  case list_find as [[]|]; intros; simplify_eq; lia.
Qed.

Lemma find_granting_lt stk kind t n p :
  find_granting stk kind t = Some (n, p) 
  (n < length stk)%nat.
Proof.
  intros [[n1 p1] [[Eq%lookup_lt_Some MG]%list_find_Some ?]]%fmap_Some.
  by simplify_eq.
Qed.

Lemma grant_active_SRO_SRW stk old it cids stk' t
  (SRW: it.(perm) = SharedReadWrite):
  grant stk old it cids = Some stk' 
  t  active_SRO stk  t  active_SRO stk'.
Proof.
  rewrite /grant. case find_granting as [[n p]|] eqn:FR; [|done].
  rewrite /= SRW.
  case find_first_write_incompatible as [n'|] eqn:FI; [|done].
  rewrite /= => ?. simplify_eq.
  destruct (item_insert_dedup_case stk it n') as [EQ|EQ]; rewrite EQ; [|done].
  rewrite SRW /= in FR. intros IN.
  have IN' := find_granting_incompatible_active_SRO _ _ _ _ _ IN FR.
  have IN2 := find_first_write_incompatible_active_SRO _ _ _ FI.
  have Ltn := find_granting_lt _ _ _ _ _ FR.
  destruct (IN2 _ IN') as (j & jt & Eqjt & Eqp & Eqt & Lt' & HL).
  have Eqln: length (take n stk) = n by apply take_length_le; lia.
  have Len' := find_first_write_incompatible_le _ _ _ FI. rewrite Eqln in Len'.
  have Eqjt' : stk !! j = Some jt.
  { rewrite lookup_take // in Eqjt. lia. }
  apply (active_SRO_elem_of_inv j jt t); [|done|done|].
  - rewrite lookup_app_l; [by rewrite lookup_take|].
    rewrite take_length_le //. lia.
  - intros k kt Ltk.
    rewrite lookup_app_l; last by (rewrite take_length_le; lia).
    intros Eqkt. apply (HL _ _ Ltk).
    rewrite lookup_take; [|lia].
    rewrite lookup_take in Eqkt; [done|lia].
Qed.

Lemma grant_active_SRO_non_SRW stk old it cids stk' t pm opro
  (ND: stack_item_tagged_NoDup stk)
  (SRW: it.(perm)  SharedReadWrite) (NDIS: it.(perm)  Disabled)
  (IN': mkItem pm (Tagged t) opro  stk')
  (NEqt: it.(tg)  Tagged t) :
  grant stk old it cids = Some stk' 
  t  active_SRO stk  t  active_SRO stk'.
Proof.
  rewrite /grant. case find_granting as [[n p]|] eqn:FR; [|done].
  case it.(perm) eqn:Eqp; [|done|..|done];
    cbn -[item_insert_dedup];
    (case access1 as [[n' stk1]|] eqn:ACC; [|done]);
    cbn -[item_insert_dedup];
    intros ?; simplify_eq.
  - intros Int. exfalso.
    apply (access1_write_remove_incompatible_active_SRO _ _ _ _ _ _ ND
            Int ACC pm opro).
    move : IN' => /item_insert_dedup_subseteq /elem_of_cons [|//].
    intros. by subst it.
  - intros Int.
    have IN'2: mkItem pm (Tagged t) opro  stk1.
    { move : IN' => /item_insert_dedup_subseteq /elem_of_cons [|//].
      intros. by subst it. }
    have IN2:= access1_active_SRO_preserving _ _ _ _ _ _ _ _ _ ND IN'2 ACC Int.
    destruct (item_insert_dedup_case stk1 it 0) as [EQ|EQ]; rewrite EQ //.
    apply active_SRO_cons_elem_of. split; [done|by right].
Qed.

Lemma grant_active_SRO_preserving stk old it cids stk' t pm opro
  (ND: stack_item_tagged_NoDup stk)
  (NDIS: it.(perm)  Disabled)
  (IN': mkItem pm (Tagged t) opro  stk')
  (NEqt: it.(tg)  Tagged t) :
  grant stk old it cids = Some stk' 
  t  active_SRO stk  t  active_SRO stk'.
Proof.
  case (decide (it.(perm) = SharedReadWrite)) => ?.
  - by apply grant_active_SRO_SRW.
  - by eapply grant_active_SRO_non_SRW.
Qed.

Lemma retag_item_active_SRO_preserving α nxtp c cids l old rk pk T new α' nxtp' :
  retag α nxtp cids c l old rk pk T = Some (new, α', nxtp') 
   l' t' stk stk' it',
    stack_item_tagged_NoDup stk 
    α !! l' = Some stk 
    α' !! l' = Some stk' 
    it'  stk  it'  stk' 
    it'.(tg