refl_mem_step.v 78.2 KB
Newer Older
1 2 3
From iris.algebra Require Import local_updates.

From stbor.lang Require Import steps_progress steps_inversion steps_retag.
4
From stbor.sim Require Export instance body invariant_access.
5 6 7

Set Default Proof Using "Type".

Ralf Jung's avatar
Ralf Jung committed
8 9
Section mem.
Implicit Types Φ: resUR  nat  result  state  result  state  Prop.
10 11 12

(** MEM STEP -----------------------------------------------------------------*)

Hai Dang's avatar
Hai Dang committed
13 14 15
Lemma wsat_tmap_nxtp r σs σt :
  wsat r σs σt  r.(rtm) !! σt.(snp) = None.
Proof.
Hai Dang's avatar
Hai Dang committed
16
  intros (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
17 18
  destruct (r.(rtm) !! σt.(snp)) as [[k h]|] eqn:Eqr; [|done].
  exfalso.
Hai Dang's avatar
Hai Dang committed
19
  move : (proj1 VALID σt.(snp)). rewrite Eqr.
Hai Dang's avatar
Hai Dang committed
20 21 22 23
  intros [[k' Eqk']%tagKindR_valid VALh]. simpl in Eqk', VALh. subst k.
  destruct (PINV σt.(snp) k' h) as [Lt _]; [by rewrite Eqr|]. lia.
Qed.

24 25 26 27 28 29 30 31 32
Lemma sim_body_alloc_local fs ft r n T σs σt Φ :
  let l := (fresh_block σt.(shp), 0) in
  let t := (Tagged σt.(snp)) in
  let σs' := mkState (init_mem l (tsize T) σs.(shp))
                     (init_stacks σs.(sst) l (tsize T) t) σs.(scs)
                     (S σs.(snp)) σs.(snc) in
  let σt' := mkState (init_mem l (tsize T) σt.(shp))
                     (init_stacks σt.(sst) l (tsize T) t) σt.(scs)
                     (S σt.(snp)) σt.(snc) in
Hai Dang's avatar
Hai Dang committed
33
  let vst := repeat (%S, %S) (tsize T) in
Hai Dang's avatar
Hai Dang committed
34
  let r' : resUR := res_loc l vst σt.(snp) in
Hai Dang's avatar
Hai Dang committed
35
  Φ (r  r') n (PlaceR l t T) σs' (PlaceR l t T) σt' 
36 37
  r {n,fs,ft} (Alloc T, σs)  (Alloc T, σt) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
38
  intros l t σs' σt' vst r' POST.
39 40 41
  pfold. intros NT. intros.
  have EqDOM := wsat_heap_dom _ _ _ WSAT.
  have EqFRESH := fresh_block_equiv _ _ EqDOM.
Hai Dang's avatar
Hai Dang committed
42
  have HNP := wsat_tmap_nxtp _ _ _ WSAT.
Hai Dang's avatar
Hai Dang committed
43
  have HEQr': (r_f  r  r').(rtm) !! snp σt 
Hai Dang's avatar
Hai Dang committed
44 45 46
      Some (to_tgkR tkLocal, to_hplR (write_hpl l vst )).
  { rewrite lookup_op HNP left_id lookup_insert //. }
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
47
  destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&REL).
48 49 50 51 52 53 54 55 56
  have Eqlst: l = (fresh_block σs.(shp), 0). { by rewrite /l EqFRESH. }
  split; [|done|].
  { right. do 2 eexists. by eapply (head_step_fill_tstep _ []), alloc_head_step. }
  constructor 1. intros ? σt1 STEPT.
  destruct (tstep_alloc_inv _ _ _ _ _ STEPT) as [? Eqσt'].
  rewrite -/σt' in Eqσt'. subst et' σt1.
  have STEPS: (Alloc T, σs) ~{fs}~> (Place l t T, σs').
  { subst l σs' t. rewrite Eqlst -Eqnp.
    eapply (head_step_fill_tstep _ []),  alloc_head_step. }
Hai Dang's avatar
Hai Dang committed
57
  eexists _, σs', (r  r'), n. split; last split.
58
  { left. by apply tc_once. }
Hai Dang's avatar
Hai Dang committed
59
  { have Eqrcm: (r_f  r  r').(rcm)  (r_f  r).(rcm)
Hai Dang's avatar
Hai Dang committed
60
      by rewrite /rcm /= right_id.
Hai Dang's avatar
Hai Dang committed
61
    have VALID':  (r_f  r  r').
62
    { apply (local_update_discrete_valid_frame _ ε r'); [by rewrite right_id|].
Hai Dang's avatar
Hai Dang committed
63
      rewrite /= right_id -cmra_assoc cmra_assoc.
Hai Dang's avatar
Hai Dang committed
64
      by apply res_tag_alloc_local_update. }
Hai Dang's avatar
Hai Dang committed
65
    rewrite cmra_assoc.
66 67 68 69
    destruct (init_mem_lookup l (tsize T) σt.(shp)) as [HLmt1 HLmt2].
    destruct (init_mem_lookup l (tsize T) σs.(shp)) as [HLms1 HLms2].
    destruct (init_stacks_lookup σt.(sst) l (tsize T) t) as [HLst1 HLst2].
    destruct (init_stacks_lookup σs.(sst) l (tsize T) t) as [HLss1 HLss2].
Hai Dang's avatar
Hai Dang committed
70
    split; last split; last split; last split; last split.
71 72 73
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
Hai Dang's avatar
Hai Dang committed
74
    - intros t1 k1 h1. subst σt'; simpl.
Hai Dang's avatar
Hai Dang committed
75
      case (decide (t1 = σt.(snp))) => ?; [subst t1|].
Hai Dang's avatar
Hai Dang committed
76 77 78
      + intros Eqh1. split; [simpl; lia|].
        move : Eqh1. rewrite HEQr'.
        intros [Eqk1 Eqh1]%Some_equiv_inj. simpl in Eqk1, Eqh1.
Hai Dang's avatar
Hai Dang committed
79 80
        intros l1 ss1 st1. rewrite -Eqh1 /to_hplR lookup_fmap.
        destruct (write_hpl_lookup_case l vst  l1)
Hai Dang's avatar
Hai Dang committed
81 82 83 84
          as [(i & Lti & ? & Eql1)|(NEQl1 & Eql1)].
        * subst l1. rewrite Eql1. rewrite repeat_length in Lti.
          rewrite (repeat_lookup_lt_length _ _ _ Lti) /=.
          intros ?%Some_equiv_inj%to_agree_inj. simplify_eq.
Hai Dang's avatar
Hai Dang committed
85 86 87 88 89
          rewrite (HLmt1 _ Lti) (HLms1 _ Lti).
          intros INVPR. do 2 (split; [done|]). destruct k1.
          { by rewrite /= (HLst1 _ Lti). }
          { move : INVPR. simpl. naive_solver. }
          { by inversion Eqk1. }
Hai Dang's avatar
Hai Dang committed
90 91
        * rewrite Eql1 lookup_empty. inversion 1.
      + intros Eqh'.
Hai Dang's avatar
Hai Dang committed
92
        have Eqh1: (r_f  r).(rtm) !! t1  Some (to_tgkR k1, h1).
Hai Dang's avatar
Hai Dang committed
93
        { move : Eqh'. rewrite lookup_op lookup_insert_ne // right_id //. }
Hai Dang's avatar
Hai Dang committed
94
        specialize (PINV _ _ _ Eqh1) as [? PINV]. split; [simpl; lia|].
Hai Dang's avatar
Hai Dang committed
95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120
        intros l1 ss1 st1 Eqs1. specialize (PINV _ _ _ Eqs1).
        destruct k1.
        { intros _. specialize (PINV I) as (Eqss1 & Eqst1 & IP).
          have NEQl1 :  i : nat, (i < tsize T)%nat  l1  l + i.
          { intros i Lt Eql1. subst l1.
            apply (is_fresh_block σt.(shp) i). by eapply elem_of_dom_2. }
          by rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1). }
        { intros (stk & pm & opro & Eqstk & Instk & ND).
          destruct (init_stacks_lookup_case _ _ _ _ _ _ Eqstk)
            as [[Eql1 NEQl1]|(i & (? & Lti) & Eql1)].
          - rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1).
            apply PINV. by exists stk, pm, opro.
          - subst l1.
            have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id.
            have Eq2 := HLst1 _ Lti'. rewrite Z2Nat.id // Eqstk in Eq2.
            simplify_eq. apply elem_of_list_singleton in Instk. simplify_eq. }
        (* TODO: duplicated proof *)
        { intros (stk & pm & opro & Eqstk & Instk & ND).
          destruct (init_stacks_lookup_case _ _ _ _ _ _ Eqstk)
            as [[Eql1 NEQl1]|(i & (? & Lti) & Eql1)].
          - rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1).
            apply PINV. by exists stk, pm, opro.
          - subst l1.
            have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id.
            have Eq2 := HLst1 _ Lti'. rewrite Z2Nat.id // Eqstk in Eq2.
            simplify_eq. apply elem_of_list_singleton in Instk. simplify_eq. }
121
    - intros c cs. subst σt'. rewrite Eqrcm /=. intros Eqc.
Hai Dang's avatar
Hai Dang committed
122
      specialize (CINV _ _ Eqc) as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
123 124
      intros t1 tls1 [Ltc Ht]%CINV. split; [lia|].
      intros l1 Inl1.
Hai Dang's avatar
Hai Dang committed
125
      case (decide (t1 = σt.(snp))) => ?; [subst t1|]; [lia|].
Hai Dang's avatar
Hai Dang committed
126
      specialize (Ht _  Inl1) as (stk1 & pm1 & Eql1 & Eqp).
Hai Dang's avatar
Hai Dang committed
127 128 129 130 131 132
      destruct (init_stacks_lookup_case_2 _ l (tsize T) t _ _ Eql1)
        as [[EQ NEQ1]|(i & (? & Lti) & ? & EQ)].
      + rewrite EQ. clear -Eqp. naive_solver.
      + exfalso. subst l1.
        apply (is_fresh_block σt.(shp) i). rewrite (state_wf_dom _ WFT).
        by eapply elem_of_dom_2.
Hai Dang's avatar
Hai Dang committed
133
    - subst σt'. split; last split; last split; last split; [|simpl; auto..|].
Hai Dang's avatar
Hai Dang committed
134 135 136 137 138 139 140 141 142 143 144
      { by rewrite /= Eqst. } simpl.
      intros l1 [s1 HL1]%elem_of_dom.
      destruct (init_mem_lookup_case _ _ _ _ _ HL1)
        as [[Eqs1 NEQ]|(i & (? & Lti) & Eql)].
      + have InD1 : l1  dom (gset loc) σt.(shp) by eapply elem_of_dom_2.
        specialize (HLmt2 _ NEQ). specialize (HLms2 _ NEQ).
        specialize (REL _ InD1) as [PB|[t' PV]]; [left|right].
        * rewrite /pub_loc /= HLmt2 HLms2.
          intros st1 Eqst1. destruct (PB _ Eqst1) as [ss [Eqss AREL]].
          exists ss. split; [done|]. eapply arel_mono; [done| |eauto].
          apply cmra_included_l.
Hai Dang's avatar
Hai Dang committed
145 146 147 148
        * destruct PV as (k' & h' & Eqh' & Inh' & Eqt').
          exists t', k', h'. setoid_rewrite Eqrcm. split; last split; [|done..].
          destruct Eqt' as [|[]]; subst k'.
          { apply tmap_lookup_op_l_local_equiv; [apply VALID'|done]. }
Hai Dang's avatar
Hai Dang committed
149
          { apply tmap_lookup_op_l_uniq_equiv; [apply VALID'|done]. }
Hai Dang's avatar
Hai Dang committed
150
      + right. exists σt.(snp), tkLocal. subst l1. eexists.
Hai Dang's avatar
Hai Dang committed
151 152
        have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id.
        split; last split.
Hai Dang's avatar
Hai Dang committed
153
        * rewrite HEQr'; eauto.
Hai Dang's avatar
Hai Dang committed
154 155 156 157
        * destruct (write_hpl_is_Some l vst  (Z.to_nat i)) as [? EQ].
          { by rewrite repeat_length. }
          { rewrite Z2Nat.id // in EQ. rewrite lookup_fmap EQ. by eexists. }
        * by left. }
158
  left.
Ralf Jung's avatar
Ralf Jung committed
159
  apply: sim_body_result. intros.
160
  apply POST; eauto.
Hai Dang's avatar
Hai Dang committed
161
Qed.
Hai Dang's avatar
Hai Dang committed
162

Hai Dang's avatar
Hai Dang committed
163
Lemma sim_body_alloc_public fs ft r n T σs σt Φ :
Hai Dang's avatar
Hai Dang committed
164 165 166 167
  let l := (fresh_block σt.(shp), 0) in
  let t := (Tagged σt.(snp)) in
  let σs' := mkState (init_mem l (tsize T) σs.(shp))
                     (init_stacks σs.(sst) l (tsize T) t) σs.(scs)
168
                     (S σs.(snp)) σs.(snc) in
Hai Dang's avatar
Hai Dang committed
169 170
  let σt' := mkState (init_mem l (tsize T) σt.(shp))
                     (init_stacks σt.(sst) l (tsize T) t) σt.(scs)
171
                     (S σt.(snp)) σt.(snc) in
Hai Dang's avatar
Hai Dang committed
172 173
  let r' : resUR := res_tag σt.(snp) tkPub  in
  Φ (r  r') n (PlaceR l t T) σs' (PlaceR l t T) σt' 
174 175
  r {n,fs,ft} (Alloc T, σs)  (Alloc T, σt) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
176
  intros l t σs' σt' r' POST.
177 178 179
  pfold. intros NT. intros.
  have EqDOM := wsat_heap_dom _ _ _ WSAT.
  have EqFRESH := fresh_block_equiv _ _ EqDOM.
Hai Dang's avatar
Hai Dang committed
180
  have HNP := wsat_tmap_nxtp _ _ _ WSAT.
Hai Dang's avatar
Hai Dang committed
181
  have HEQr': (r_f  r  r').(rtm) !! snp σt  Some (to_tgkR tkPub, to_hplR ).
Hai Dang's avatar
Hai Dang committed
182
  { rewrite lookup_op HNP left_id res_tag_lookup //. }
Hai Dang's avatar
Hai Dang committed
183
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
184 185
  destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&REL).
  have Eqlst: l = (fresh_block σs.(shp), 0). { by rewrite /l EqFRESH. }
186 187 188 189 190
  split; [|done|].
  { right. do 2 eexists. by eapply (head_step_fill_tstep _ []), alloc_head_step. }
  constructor 1. intros ? σt1 STEPT.
  destruct (tstep_alloc_inv _ _ _ _ _ STEPT) as [? Eqσt'].
  rewrite -/σt' in Eqσt'. subst et' σt1.
Hai Dang's avatar
Hai Dang committed
191 192 193 194
  have STEPS: (Alloc T, σs) ~{fs}~> (Place l t T, σs').
  { subst l σs' t. rewrite Eqlst -Eqnp.
    eapply (head_step_fill_tstep _ []),  alloc_head_step. }
  eexists _, σs', (r  r'), n. split; last split.
195
  { left. by apply tc_once. }
Hai Dang's avatar
Hai Dang committed
196 197
  { have Eqrcm: (r_f  r  r').(rcm)  (r_f  r).(rcm)
      by rewrite /rcm /= right_id.
198 199
    have VALID':  (r_f  r  r').
    { apply (local_update_discrete_valid_frame _ ε r'); [by rewrite right_id|].
Hai Dang's avatar
Hai Dang committed
200 201
      rewrite /= right_id -cmra_assoc cmra_assoc.
      by apply res_tag_alloc_local_update. }
202
    rewrite cmra_assoc.
Hai Dang's avatar
Hai Dang committed
203 204 205 206
    destruct (init_mem_lookup l (tsize T) σt.(shp)) as [HLmt1 HLmt2].
    destruct (init_mem_lookup l (tsize T) σs.(shp)) as [HLms1 HLms2].
    destruct (init_stacks_lookup σt.(sst) l (tsize T) t) as [HLst1 HLst2].
    destruct (init_stacks_lookup σs.(sst) l (tsize T) t) as [HLss1 HLss2].
Hai Dang's avatar
Hai Dang committed
207
    split; last split; last split; last split; last split.
208 209 210
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
Hai Dang's avatar
Hai Dang committed
211 212 213 214 215
    - intros t1 k1 h1. subst σt'; simpl.
      case (decide (t1 = σt.(snp))) => ?; [subst t1|].
      + intros Eqh1. split; [simpl; lia|].
        move : Eqh1. rewrite HEQr'.
        intros [Eqk1 Eqh1]%Some_equiv_inj. simpl in Eqk1, Eqh1.
Hai Dang's avatar
Hai Dang committed
216
        intros l1 ss1 st1. rewrite -Eqh1 lookup_fmap lookup_empty. by inversion 1.
Hai Dang's avatar
Hai Dang committed
217
      + intros Eqh'.
Hai Dang's avatar
Hai Dang committed
218
        have Eqh1: (r_f  r).(rtm) !! t1  Some (to_tgkR k1, h1).
Hai Dang's avatar
Hai Dang committed
219
        { move : Eqh'. rewrite lookup_op lookup_insert_ne // right_id //. }
Hai Dang's avatar
Hai Dang committed
220
        specialize (PINV _ _ _ Eqh1) as [? PINV]. split; [simpl; lia|].
Hai Dang's avatar
Hai Dang committed
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
        intros l1 ss1 st1 Eqs1.
        specialize (PINV _ _ _ Eqs1). destruct k1.
        { intros _. specialize (PINV I) as (Eqss1 & Eqst1 & IP).
          have NEQl1 :  i : nat, (i < tsize T)%nat  l1  l + i.
          { intros i Lt Eql1. subst l1.
            apply (is_fresh_block σt.(shp) i). by eapply elem_of_dom_2. }
          by rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1). }
        { intros (stk & pm & opro & Eqstk & Instk & ND).
          destruct (init_stacks_lookup_case _ _ _ _ _ _ Eqstk)
            as [[Eql1 NEQl1]|(i & (? & Lti) & Eql1)].
          - rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1).
            apply PINV. by exists stk, pm, opro.
          - subst l1.
            have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id.
            have Eq2 := HLst1 _ Lti'. rewrite Z2Nat.id // Eqstk in Eq2.
            simplify_eq. apply elem_of_list_singleton in Instk. simplify_eq. }
        (* TODO: duplicated proof *)
        { intros (stk & pm & opro & Eqstk & Instk & ND).
          destruct (init_stacks_lookup_case _ _ _ _ _ _ Eqstk)
            as [[Eql1 NEQl1]|(i & (? & Lti) & Eql1)].
          - rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1).
            apply PINV. by exists stk, pm, opro.
          - subst l1.
            have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id.
            have Eq2 := HLst1 _ Lti'. rewrite Z2Nat.id // Eqstk in Eq2.
            simplify_eq. apply elem_of_list_singleton in Instk. simplify_eq. }
Hai Dang's avatar
Hai Dang committed
247
    - intros c cs. subst σt'. rewrite Eqrcm /=. intros Eqc.
Hai Dang's avatar
Hai Dang committed
248
      specialize (CINV _ _ Eqc) as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
249 250
      intros t1 tls1 [Ltc Ht]%CINV. split; [lia|].
      intros l1 Inl1.
Hai Dang's avatar
Hai Dang committed
251
      case (decide (t1 = σt.(snp))) => ?; [subst t1|]; [lia|].
Hai Dang's avatar
Hai Dang committed
252
      specialize (Ht _  Inl1) as (stk1 & pm1 & Eql1 & Eqp).
Hai Dang's avatar
Hai Dang committed
253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270
      destruct (init_stacks_lookup_case_2 _ l (tsize T) t _ _ Eql1)
        as [[EQ NEQ1]|(i & (? & Lti) & ? & EQ)].
      + rewrite EQ. clear -Eqp. naive_solver.
      + exfalso. subst l1.
        apply (is_fresh_block σt.(shp) i). rewrite (state_wf_dom _ WFT).
        by eapply elem_of_dom_2.
    - subst σt'. split; last split; last split; last split; [|simpl;auto..|].
      { by rewrite /= Eqst. } simpl.
      intros l1 [s1 HL1]%elem_of_dom.
      destruct (init_mem_lookup_case _ _ _ _ _ HL1)
        as [[Eqs1 NEQ]|(i & (? & Lti) & Eql)].
      + have InD1 : l1  dom (gset loc) σt.(shp) by eapply elem_of_dom_2.
        specialize (HLmt2 _ NEQ). specialize (HLms2 _ NEQ).
        specialize (REL _ InD1) as [PB|[t' PV]]; [left|right].
        * rewrite /pub_loc /= HLmt2 HLms2.
          intros st1 Eqst1. destruct (PB _ Eqst1) as [ss [Eqss AREL]].
          exists ss. split; [done|]. eapply arel_mono; [done| |eauto].
          apply cmra_included_l.
Hai Dang's avatar
Hai Dang committed
271 272 273 274
        * destruct PV as (k' & h' & Eqh' & Inh' & Eqt').
          exists t', k', h'. setoid_rewrite Eqrcm. split; last split; [|done..].
          destruct Eqt' as [|[]]; subst k'.
          { apply tmap_lookup_op_l_local_equiv; [apply VALID'|done]. }
Hai Dang's avatar
Hai Dang committed
275
          { apply tmap_lookup_op_l_uniq_equiv; [apply VALID'|done]. }
Hai Dang's avatar
Hai Dang committed
276 277 278 279
      + left. subst l1. intros st. simpl.
        have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id.
        specialize (HLmt1 _ Lti'). rewrite Z2Nat.id // in HLmt1.
        specialize (HLms1 _ Lti'). rewrite Z2Nat.id // in HLms1.
Hai Dang's avatar
Hai Dang committed
280
        rewrite HLmt1 HLms1. inversion 1. subst st. by exists ScPoison. }
281
  left.
Ralf Jung's avatar
Ralf Jung committed
282
  apply: sim_body_result. intros.
Hai Dang's avatar
Hai Dang committed
283
  apply POST; eauto.
Hai Dang's avatar
Hai Dang committed
284
Qed.
285

Hai Dang's avatar
Hai Dang committed
286
(** Free *)
Hai Dang's avatar
Hai Dang committed
287
Lemma sim_body_free_public fs ft r n (pl: result) σs σt Φ
Hai Dang's avatar
Hai Dang committed
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 327 328 329 330 331 332 333 334 335 336 337 338 339 340 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 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423
  (RREL: rrel r pl pl) :
  ( l t T,
    pl = PlaceR l t T 
    ( m, is_Some (σs.(shp) !! (l + m))  0  m < tsize T) 
    ( m, is_Some (σt.(shp) !! (l + m))  0  m < tsize T) 
     α', memory_deallocated σt.(sst) σt.(scs) l t (tsize T) = Some α' 
      let σs' := mkState (free_mem l (tsize T) σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
      let σt' := mkState (free_mem l (tsize T) σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
      Φ r n (ValR [%S]) σs' (ValR [%S]) σt') 
  r {n,fs,ft} (Free pl, σs)  (Free pl, σt) : Φ.
Proof.
  intros POST. pfold. intros NT. intros.
  have WSAT1 := WSAT. (* backup *)

  (* making a step *)
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
  split; [|done|].
  { right.
    destruct (NT (Free pl) σs) as [[]|[es' [σs' STEPS]]];
      [done..|].
    destruct (tstep_free_inv _ _ _ _ _ STEPS)
      as (l&t&T & α' & EqH & ? & Eqh & Eqα' & ?). symmetry in EqH. simplify_eq.
    have Eqh' : ( m, is_Some (σt.(shp) !! (l + m))  0  m < tsize T).
    { intros m. rewrite -(Eqh m). rewrite -2!(elem_of_dom (D:=gset loc)).
      rewrite (wsat_heap_dom _ _ _ WSAT1) //. }
    have Eqα'2: memory_deallocated σt.(sst) σt.(scs) l t (tsize T) = Some α'.
    { destruct SREL as (Eqst&?&Eqcs&?). by rewrite -Eqst -Eqcs. }
    exists (#[%S])%E, (mkState (free_mem l (tsize T) σt.(shp)) α'
                                σt.(scs) σt.(snp) σt.(snc)).
    by eapply (head_step_fill_tstep _ []), dealloc_head_step'. }

  constructor 1. intros.
  destruct (tstep_free_inv _ _ _ _ _ STEPT)
    as (l&t&T& α' & EqH & ? & Eqh & Eqα' & ?). symmetry in EqH. simplify_eq.
  have Eqh' : ( m, is_Some (σs.(shp) !! (l + m))  0  m < tsize T).
    { intros m. rewrite -(Eqh m). rewrite -2!(elem_of_dom (D:=gset loc)).
      rewrite (wsat_heap_dom _ _ _ WSAT1) //. }
  have Eqα'2: memory_deallocated σs.(sst) σs.(scs) l t (tsize T) = Some α'.
  { destruct SREL as (Eqst&?&Eqcs&?). by rewrite Eqst Eqcs. }
  set σs' := mkState (free_mem l (tsize T) σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc).
  have STEPS: (Free (Place l t T), σs) ~{fs}~> ((#[%S])%E, σs').
  { by eapply (head_step_fill_tstep _ []), dealloc_head_step'. }

  (* unfolding rrel for place *)
  simpl in RREL. destruct RREL as [VREL _].
  inversion VREL as [|???? AREL U]; subst; simplify_eq. clear U VREL.
  destruct AREL as (_ & _ & AREL).

  (* reestablishing WSAT *)
  destruct (free_mem_lookup l (tsize T) σt.(shp)) as [Hmst1 Hmst2].
  destruct (free_mem_lookup l (tsize T) σs.(shp)) as [Hmss1 Hmss2].

  exists (#[%S])%E, σs', r, n. split; last split.
  { left. by constructor 1. }
  { split; last split; last split; last split; last split.
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
    - intros t' k' h' Eqt'.
      specialize (PINV _ _ _ Eqt') as [? PINV].
      split; [done|]. intros l1 ss1 st1 Eql1.
      specialize (PINV _ _ _ Eql1).
      destruct k'; simpl in *.
      + specialize (PINV I) as (Eqst & Eqss & HTOP). intros _.
        destruct (free_mem_lookup_case l1 l (tsize T) σt.(shp))
          as [[NEql Eql]|(i & Lti & ? & Eql)].
        * destruct (for_each_dealloc_lookup _ _ _ _ _ Eqα') as [_ EQ2].
          rewrite Eql (Hmss2 _ NEql) (EQ2 _ NEql) //.
        * subst l1. exfalso.
          destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
          destruct Lti as [Lei Lti].
          destruct (EQ1 (Z.to_nat i)) as (stk1 & stk' & Eqstk & EqN & DA).
          { rewrite -(Nat2Z.id (tsize T)). by apply Z2Nat.inj_lt; lia. }
          rewrite Z2Nat.id // in Eqstk. rewrite Eqstk in HTOP. simplify_eq.
          move : DA. clear -AREL Eqt'.
          destruct (dealloc1 (init_stack (Tagged t')) t σt.(scs))
            eqn:Eqd; [|done]. intros _.
          destruct (dealloc1_singleton_Some (mkItem Unique (Tagged t') None)
                      t σt.(scs)) as [Eqt _]. { by eexists. }
          simpl in Eqt. subst t. move : Eqt'.
          destruct AREL as [h AREL]. rewrite lookup_op AREL.
          by apply tagKindR_local_exclusive_r.
      + intros (stk1 & pm & opro & Eqstk1 & ?).
        destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Eqα' _ _ Eqstk1)
          as [NEQ EQ].
        destruct PINV as [Eqst [Eqss PO]].
        { by exists stk1, pm, opro. }
        destruct PO as (stk' & Eqstk' & PO).
        rewrite Eqstk' in EQ. simplify_eq. split; last split.
        * by rewrite Hmst2.
        * by rewrite Hmss2.
        * by exists stk1.
      + intros (stk1 & pm & opro & Eqstk1 & ?).
        destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Eqα' _ _ Eqstk1)
          as [NEQ EQ].
        destruct PINV as [Eqst [Eqss PO]].
        { by exists stk1, pm, opro. }
        destruct PO as (stk' & Eqstk' & PO).
        rewrite Eqstk' in EQ. simplify_eq. split; last split.
        * by rewrite Hmst2.
        * by rewrite Hmss2.
        * by exists stk1.
    - intros c Tc Eqc. specialize (CINV _ _ Eqc) as [? CINV].
      split; [done|]. intros tc L InL. specialize (CINV _ _ InL) as [? CINV].
      split; [done|]. intros l1 Inl1.
      specialize (CINV _ Inl1). simpl.
      destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 EQ2].
      (* from Eqα', l1 cannot be in l because it is protected by c,
        so α' !! l1 = σt.(sst) !! l1. *)
      destruct (block_case l l1 (tsize T)) as [NEql|(i & [Lei Lti] & Eql)].
      + rewrite EQ2 //.
      + exfalso. clear EQ2.
        subst l1. destruct CINV as (stk & pm & Eqstk & Instk & ?).
        specialize (EQ1 (Z.to_nat i)) as (stk1 & stk' & Eqstk').
        { rewrite -(Nat2Z.id (tsize T)). by apply Z2Nat.inj_lt; lia. }
        rewrite Z2Nat.id // in Eqstk'.
        destruct Eqstk' as (Eqstk1 & Eqstk' & DA).
        rewrite Eqstk1 in Eqstk. simplify_eq.
        move : DA. destruct (dealloc1 stk t σt.(scs)) eqn:Eqd; [|done].
        intros _.
        destruct (dealloc1_Some stk t σt.(scs)) as (it & Eqit & ? & FA & GR).
        { by eexists. }
        rewrite ->Forall_forall in FA. apply (FA _ Instk).
        rewrite /is_active_protector /= /is_active bool_decide_true //.
    - rewrite /srel /=. destruct SREL as (?&?&?&?&PB).
      do 4 (split; [done|]).
      intros l1 Inl1.
      destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [_ EQ2].
      destruct (free_mem_dom _ _ _ _ Inl1) as (InD & NEql & EqM).
      specialize (EQ2 _ NEql).
      destruct (PB _ InD) as [PP|PV]; [left|by right].
      intros ?. simpl. rewrite (Hmst2 _ NEql) (Hmss2 _ NEql). by apply PP. }
  left.
  apply: sim_body_result. intros. eapply POST; eauto.
Qed.

Hai Dang's avatar
Hai Dang committed
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 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595
(** Freeing to unique/local *)
(* This one deallocates [l] with [tsize T] and tag [t]. It also deallocates
  the logical resource [res_tag t k h0]. In general, we can require that any
  locations in [h0] be included in [T]. Here, we prove a simple lemma where
  [h0] is a singleton of [l] and [tsize T] = 1 *)
Lemma sim_body_free_unique_local_1 fs ft r r' n l t k T s σs σt Φ :
  tsize T = 1%nat 
  r  r'  res_tag t k {[l := s]} 
  (k = tkLocal  k = tkUnique) 
  (* is_Some (h0 !! l)  *)
  (is_Some (σs.(shp) !! l)  is_Some (σt.(shp) !! l) 
     α', memory_deallocated σt.(sst) σt.(scs) l (Tagged t) (tsize T) = Some α' 
      let σs' := mkState (free_mem l (tsize T) σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
      let σt' := mkState (free_mem l (tsize T) σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
      Φ r' n (ValR [%S]) σs' (ValR [%S]) σt') 
  r {n,fs,ft}
    (Free (Place l (Tagged t) T), σs)  (Free (Place l (Tagged t) T), σt) : Φ.
Proof.
  intros EqT Eqr UNIQ POST. pfold. intros NT. intros.
  have WSAT1 := WSAT. (* backup *)

  (* making a step *)
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
  split; [|done|].
  { right.
    destruct (NT (Free (Place l (Tagged t) T)) σs) as [[]|[es' [σs' STEPS]]];
      [done..|].
    destruct (tstep_free_inv _ (PlaceR _ _ _) _ _ _ STEPS)
      as (l'&t'&T' & α' & EqH & ? & Eqh & Eqα' & ?). symmetry in EqH. simplify_eq.
    have Eqh' : ( m, is_Some (σt.(shp) !! (l + m))  0  m < tsize T).
    { intros m. rewrite -(Eqh m). rewrite -2!(elem_of_dom (D:=gset loc)).
      rewrite (wsat_heap_dom _ _ _ WSAT1) //. }
    have Eqα'2: memory_deallocated σt.(sst) σt.(scs) l (Tagged t) (tsize T) = Some α'.
    { destruct SREL as (Eqst&?&Eqcs&?). by rewrite -Eqst -Eqcs. }
    exists (#[%S])%E, (mkState (free_mem l (tsize T) σt.(shp)) α'
                                σt.(scs) σt.(snp) σt.(snc)).
    by eapply (head_step_fill_tstep _ []), dealloc_head_step'. }

  constructor 1. intros.
  destruct (tstep_free_inv _ (PlaceR _ _ _) _ _ _ STEPT)
    as (l'&t'&T'& α' & EqH & ? & Eqh & Eqα' & ?). symmetry in EqH. simplify_eq.
  have Eqh' : ( m, is_Some (σs.(shp) !! (l + m))  0  m < tsize T).
    { intros m. rewrite -(Eqh m). rewrite -2!(elem_of_dom (D:=gset loc)).
      rewrite (wsat_heap_dom _ _ _ WSAT1) //. }
  have Eqα'2: memory_deallocated σs.(sst) σs.(scs) l (Tagged t) (tsize T) = Some α'.
  { destruct SREL as (Eqst&?&Eqcs&?). by rewrite Eqst Eqcs. }
  set σs' := mkState (free_mem l (tsize T) σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc).
  have STEPS: (Free (Place l (Tagged t) T), σs) ~{fs}~> ((#[%S])%E, σs').
  { by eapply (head_step_fill_tstep _ []), dealloc_head_step'. }

  (* reestablishing WSAT *)
  destruct (free_mem_lookup l (tsize T) σt.(shp)) as [Hmst1 Hmst2].
  destruct (free_mem_lookup l (tsize T) σs.(shp)) as [Hmss1 Hmss2].

  have HNrf: (r_f  r').(rtm) !! t = None.
  { destruct ((r_f  r').(rtm) !! t) eqn:Eqt; [|done].
    exfalso. move : VALID. rewrite Eqr cmra_assoc => VALID.
    move : (proj1 VALID t). rewrite lookup_op Eqt res_tag_lookup.
    intros VAL. apply exclusive_Some_r in VAL; [done|].
    destruct UNIQ; subst k; apply _. }
  have Eqrcm: (r_f  r').(rcm)  (r_f  r).(rcm).
      { rewrite Eqr /= right_id //. }

  exists (#[%S])%E, σs', r', n. split; last split.
  { left. by constructor 1. }
  { split; last split; last split; last split; last split.
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - apply (local_update_discrete_valid_frame r_f _ _ VALID).
      rewrite Eqr cmra_assoc.
      by apply res_tag_uniq_dealloc_local_update_r.
    - intros t' k' h' Eqt'.
      have ?: (t'  t).
      { intros ?. subst t'. rewrite HNrf in Eqt'. inversion Eqt'. }
      have Eqt: (r_f  r).(rtm) !! t'  Some (to_tgkR k', h').
      { rewrite Eqr cmra_assoc lookup_op Eqt' res_tag_lookup_ne //. }
      specialize (PINV _ _ _ Eqt) as [? PINV].
      split; [done|]. intros l1 ss1 st1 Eql1.
      specialize (PINV _ _ _ Eql1).
      destruct k'; simpl in *.
      + specialize (PINV I) as (Eqst & Eqss & HTOP). intros _.
        destruct (free_mem_lookup_case l1 l (tsize T) σt.(shp))
          as [[NEql Eql]|(i & Lti & ? & Eql)].
        * destruct (for_each_dealloc_lookup _ _ _ _ _ Eqα') as [_ EQ2].
          rewrite Eql (Hmss2 _ NEql) (EQ2 _ NEql) //.
        * subst l1. exfalso.
          destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
          destruct Lti as [Lei Lti].
          destruct (EQ1 (Z.to_nat i)) as (stk1 & stk' & Eqstk & EqN & DA).
          { rewrite -(Nat2Z.id (tsize T)). by apply Z2Nat.inj_lt; lia. }
          rewrite Z2Nat.id // in Eqstk. rewrite Eqstk in HTOP. simplify_eq.
          move : DA.
          destruct (dealloc1 (init_stack (Tagged t')) (Tagged t) σt.(scs))
            eqn:Eqd; [|done]. intros _.
          destruct (dealloc1_singleton_Some (mkItem Unique (Tagged t') None)
                      (Tagged t) σt.(scs)) as [Eqt1 _]. { by eexists. }
          simpl in Eqt1. by simplify_eq.
      + intros (stk1 & pm & opro & Eqstk1 & ?).
        destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Eqα' _ _ Eqstk1)
          as [NEQ EQ].
        destruct PINV as [Eqst [Eqss PO]].
        { by exists stk1, pm, opro. }
        destruct PO as (stk' & Eqstk' & PO).
        rewrite Eqstk' in EQ. simplify_eq. split; last split.
        * by rewrite Hmst2.
        * by rewrite Hmss2.
        * by exists stk1.
      + intros (stk1 & pm & opro & Eqstk1 & ?).
        destruct (for_each_dealloc_lookup_Some _ _ _ _ _ Eqα' _ _ Eqstk1)
          as [NEQ EQ].
        destruct PINV as [Eqst [Eqss PO]].
        { by exists stk1, pm, opro. }
        destruct PO as (stk' & Eqstk' & PO).
        rewrite Eqstk' in EQ. simplify_eq. split; last split.
        * by rewrite Hmst2.
        * by rewrite Hmss2.
        * by exists stk1.
    - intros c Tc Eqc. rewrite ->Eqrcm in Eqc.
      specialize (CINV _ _ Eqc) as [? CINV].
      split; [done|]. intros tc L InL. specialize (CINV _ _ InL) as [? CINV].
      split; [done|]. intros l1 Inl1.
      specialize (CINV _ Inl1). simpl.
      destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 EQ2].
      (* from Eqα', l1 cannot be in l because it is protected by c,
        so α' !! l1 = σt.(sst) !! l1. *)
      destruct (block_case l l1 (tsize T)) as [NEql|(i & [Lei Lti] & Eql)].
      + rewrite EQ2 //.
      + exfalso. clear EQ2.
        subst l1. destruct CINV as (stk & pm & Eqstk & Instk & ?).
        specialize (EQ1 (Z.to_nat i)) as (stk1 & stk' & Eqstk').
        { rewrite -(Nat2Z.id (tsize T)). by apply Z2Nat.inj_lt; lia. }
        rewrite Z2Nat.id // in Eqstk'.
        destruct Eqstk' as (Eqstk1 & Eqstk' & DA).
        rewrite Eqstk1 in Eqstk. simplify_eq.
        move : DA. destruct (dealloc1 stk (Tagged t) σt.(scs)) eqn:Eqd; [|done].
        intros _.
        destruct (dealloc1_Some stk (Tagged t) σt.(scs)) as (it & Eqit & ? & FA & GR).
        { by eexists. }
        rewrite ->Forall_forall in FA. apply (FA _ Instk).
        rewrite /is_active_protector /= /is_active bool_decide_true //.
    - rewrite /srel /=. destruct SREL as (?&?&?&?&PB).
      do 4 (split; [done|]).
      intros l1 Inl1.
      destruct (for_each_true_lookup_case_2 _ _ _ _ _ Eqα') as [_ EQ2].
      destruct (free_mem_dom _ _ _ _ Inl1) as (InD & NEql & EqM).
      specialize (EQ2 _ NEql).
      destruct (PB _ InD) as [PP|PV]; [left|right].
      + intros st. simpl. rewrite (Hmst2 _ NEql) (Hmss2 _ NEql).
        intros Eqst. specialize (PP _ Eqst) as (ss & ? & AREL).
        exists ss. split; [done|].
        move : AREL. rewrite Eqr cmra_assoc. by apply arel_res_tag_dealloc.
      + destruct PV as (t' & k' & h' & Eqt' & IS & PV).
        case (decide (t' = t)) => NEq; [subst t'|].
        * exfalso.
          have Eqh0: h'  to_hplR {[l := s]}.
          { move : Eqt'.
            rewrite Eqr cmra_assoc lookup_op HNrf res_tag_lookup left_id.
            by intros [_ ?]%Some_equiv_inj. }
          destruct IS as [? IS]. move : (Eqh0 l1).
          rewrite IS lookup_fmap lookup_insert_ne.
          { rewrite lookup_empty /=. by inversion 1. }
          { intros ?. subst l1.
            apply (NEql O); [rewrite EqT; lia|by rewrite shift_loc_0]. }
        * exists t', k', h'. split; last split; [|done|by setoid_rewrite Eqrcm].
          move : Eqt'.
          by rewrite Eqr cmra_assoc lookup_op res_tag_lookup_ne // right_id. }
  left.
  apply: sim_body_result. intros. eapply POST; eauto.
  - move : (Eqh' 0). rewrite shift_loc_0 EqT. intros Eq1. rewrite Eq1. lia.
  - move : (Eqh 0). rewrite shift_loc_0 EqT. intros Eq1. rewrite Eq1. lia.
Qed.

596
(** Copy *)
Hai Dang's avatar
Hai Dang committed
597 598 599 600 601 602 603
Lemma sim_body_copy_public fs ft r n (pl: result) σs σt Φ
  (RREL: rrel r pl pl) :
  ( l t T vs vt r',
    pl = PlaceR l t T 
    read_mem l (tsize T) σs.(shp) = Some vs 
    read_mem l (tsize T) σt.(shp) = Some vt 
     α', memory_read σt.(sst) σt.(scs) l t (tsize T) = Some α' 
604 605
      let σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc) in
      let σt' := mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc) in
Hai Dang's avatar
Hai Dang committed
606
      vrel ((* r   *) r') vs vt  Φ (r  r') n (ValR vs) σs' (ValR vt) σt') 
Hai Dang's avatar
Hai Dang committed
607
  r {n,fs,ft} (Copy pl, σs)  (Copy pl, σt) : Φ.
608
Proof.
Hai Dang's avatar
Hai Dang committed
609 610
  intros POST. pfold. intros NT. intros.
  have WSAT1 := WSAT. (* backup *)
Hai Dang's avatar
Hai Dang committed
611 612

  (* making a step *)
Hai Dang's avatar
Hai Dang committed
613
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
614 615
  split; [|done|].
  { right.
Hai Dang's avatar
Hai Dang committed
616
    destruct (NT (Copy pl) σs) as [[]|[es' [σs' STEPS]]];
617
      [done..|].
Hai Dang's avatar
Hai Dang committed
618 619 620 621 622 623 624
    destruct (tstep_copy_inv _ _ _ _ _ STEPS)
      as (l&t&T& vs & α' & EqH & ? & Eqvs & Eqα' & ?). symmetry in EqH. simplify_eq.
    destruct (read_mem_is_Some l (tsize T) σt.(shp)) as [vt Eqvt].
    { intros m. rewrite (srel_heap_dom _ _ _ WFS WFT SREL).
      apply (read_mem_is_Some' l (tsize T) σs.(shp)). by eexists. }
    have Eqα'2: memory_read σt.(sst) σt.(scs) l t (tsize T) = Some α'.
    { destruct SREL as (Eqst&?&Eqcs&?). by rewrite -Eqst -Eqcs. }
625 626 627
    exists (#vt)%E, (mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc)).
    by eapply (head_step_fill_tstep _ []), copy_head_step'. }
  constructor 1. intros.
Hai Dang's avatar
Hai Dang committed
628 629 630 631 632 633 634
  destruct (tstep_copy_inv _ _ _ _ _ STEPT)
    as (l&t&T& vt & α' & EqH & ? & Eqvt & Eqα' & ?). symmetry in EqH. simplify_eq.
  destruct (read_mem_is_Some l (tsize T) σs.(shp)) as [vs Eqvs].
  { intros m. rewrite -(srel_heap_dom _ _ _ WFS WFT SREL).
    apply (read_mem_is_Some' l (tsize T) σt.(shp)). by eexists. }
  have Eqα'2: memory_read σs.(sst) σs.(scs) l t (tsize T) = Some α'.
  { destruct SREL as (Eqst&?&Eqcs&?). by rewrite Eqst Eqcs. }
635
  set σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc).
Hai Dang's avatar
Hai Dang committed
636
  have STEPS: (Copy (Place l t T), σs) ~{fs}~> ((#vs)%E, σs').
637
  { by eapply (head_step_fill_tstep _ []), copy_head_step'. }
Hai Dang's avatar
Hai Dang committed
638 639 640 641 642 643 644

  (* unfolding rrel for place *)
  simpl in RREL. destruct RREL as [VREL _].
  inversion VREL as [|???? AREL U]; subst; simplify_eq. clear U VREL.
  destruct AREL as (_ & _ & AREL).

  (* returned values must be related *)
645 646
  have CORE : (r_f  r)  r_f  r  core (r_f  r) by rewrite cmra_core_r.
  assert (VREL': vrel (core (r_f  r)) vs vt).
Hai Dang's avatar
Hai Dang committed
647
  { destruct SREL as (Eqst & Eqnp & Eqcs & Eqnc & PRIV).
648 649 650 651 652 653 654
    destruct (read_mem_values _ _ _ _ Eqvs) as [Eqls HLs].
    destruct (read_mem_values _ _ _ _ Eqvt) as [Eqlt HLt].
    apply Forall2_same_length_lookup. split; [by rewrite Eqls Eqlt|].
    intros i ss st Hss Hst.
    have HLLs := lookup_lt_Some _ _ _ Hss. have HLLt := lookup_lt_Some _ _ _ Hst.
    rewrite -Eqls in HLs. specialize (HLs _ HLLs). rewrite Hss in HLs.
    rewrite -Eqlt in HLt. specialize (HLt _ HLLt). rewrite Hst in HLt.
Hai Dang's avatar
Hai Dang committed
655 656 657 658
    have InD: (l + i)  dom (gset loc) σt.(shp) by eapply elem_of_dom_2.
    specialize (PRIV _ InD).

    destruct (for_each_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
659
    rewrite Eqlt in HLLt.
Hai Dang's avatar
Hai Dang committed
660 661 662 663 664 665 666 667 668 669 670 671 672 673
    specialize (EQ1 _ HLLt) as (stk & stk' & Eqstk & Eqstk' & ACC).
    have ISA: is_Some (access1 stk AccessRead t (scs σt)).
    { move : ACC. case access1; [by eexists|done]. }

    destruct PRIV as [PB|[t' PRIV]]; last first.
    { destruct (priv_pub_access_UB _ _ _ _ _ _ _ _ Eqstk ISA WSAT1 PRIV).
      destruct t; [|done]. destruct AREL as [h Eqh].
      apply (tmap_lookup_op_r_equiv_pub r_f.(rtm)) in Eqh as [h1 Eqh1];
        [|apply VALID]. by exists (h1  h). }

    specialize (PB _ HLt) as [ss1 [Eqss1 AREL1]].
    rewrite Eqss1 in HLs. simplify_eq. by apply arel_persistent. }

  (* reestablishing WSAT *)
674 675 676
  exists (Val vs), σs', (r  (core (r_f  r))), n. split; last split.
  { left. by constructor 1. }
  { rewrite cmra_assoc -CORE.
Hai Dang's avatar
Hai Dang committed
677
    split; last split; last split; last split; last split.
678 679 680
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
Hai Dang's avatar
Hai Dang committed
681
    - intros t1 k h Eqt. specialize (PINV t1 k h Eqt) as [Lt PI]. simpl.
Hai Dang's avatar
Hai Dang committed
682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717 718
      split; [done|]. intros l' ss' st' Eqh TPRE.
      have SUB := for_each_access1 _ _ _ _ _ _ _ Eqα'.
      specialize (PI _ _ _ Eqh) as [Eql' [? HTOP]].
      { move : TPRE.
        destruct k; [done|..];
          intros (stk' & pm & opro & Eqstk' & In' & NDIS);
          specialize (SUB _ _ Eqstk') as (stk & Eqstk & SUB & ?);
          destruct (SUB _ In') as (it2 & In2 & Eqt2 & Eqp2 & NDIS2);
          simpl in *; exists stk, pm, opro.
        - split; last split; [done| |done].
          rewrite /= Eqt2 Eqp2 -NDIS2 //. by destruct it2.
        - split; last split; [done| |done].
          rewrite Eqt2 Eqp2 -NDIS2 //. by destruct it2. }
      do 2 (split; [done|]). move : TPRE.
      destruct k; simpl.
      + intros _.
        destruct (for_each_access1_lookup_inv _ _ _ _ _ _ _ Eqα' _ _ HTOP)
        as (stk2 & Eq2 & LOR).
        destruct LOR as [[n' ACC1]|LOR]; [|by rewrite LOR].
        destruct (local_access_eq _ _ _ _ _ _ _ _ _ _ _ HTOP ACC1 WSAT1 Eqt)
          as [? Eqstk2].
        { destruct (h !! l') eqn:Eql2; rewrite Eql2; [by eexists|].
          by inversion Eqh. }
        { by rewrite Eq2 Eqstk2. }
      + intros (stk' & pm & opro & Eqstk' & In' & NDIS).
        exists stk'. split; [done|].
        specialize (SUB _ _ Eqstk') as (stk & Eqstk & SUB & _).
        destruct HTOP as (stk1 & Eqstk1 & HTOP).
        rewrite Eqstk1 in Eqstk. simplify_eq.
        destruct (for_each_lookup_case _ _ _ _ _ Eqα' _ _ _ Eqstk1 Eqstk')
          as [?|[MR _]]; [by subst|].
        clear -In' MR HTOP Eqstk1 WFT NDIS.
        destruct (access1 stk AccessRead t σt.(scs)) as [[n stk1]|] eqn:Eqstk';
          [|done]. simpl in MR. simplify_eq.
        destruct (state_wf_stack_item _ WFT _ _ Eqstk1) as [? ND].
        destruct HTOP as [opro1 HTOP].
        exists opro1. eapply access1_head_preserving; eauto.
Hai Dang's avatar
Hai Dang committed
719 720 721 722 723
        have In1 : mkItem Unique (Tagged t1) opro1  stk.
        { destruct HTOP as [? HTOP]. rewrite HTOP. by left. }
        have EQ :=
          access1_read_eq _ _ _ _ _ _ _ _ ND Eqstk' In1 In' NDIS eq_refl eq_refl.
        by simplify_eq.
Hai Dang's avatar
Hai Dang committed
724 725 726 727 728 729 730 731 732 733 734 735
      + intros (stk' & pm & opro & Eqstk' & In' & NDIS).
        exists stk'. split; [done|].
        specialize (SUB _ _ Eqstk') as (stk & Eqstk & SUB & _).
        destruct HTOP as (stk1 & Eqstk1 & HTOP).
        rewrite Eqstk1 in Eqstk. simplify_eq.
        destruct (for_each_lookup_case _ _ _ _ _ Eqα' _ _ _ Eqstk1 Eqstk')
          as [?|[MR _]]; [by subst|].
        clear -In' MR HTOP Eqstk1 WFT NDIS.
        destruct (access1 stk AccessRead t σt.(scs)) as [[n stk1]|] eqn:Eqstk';
          [|done]. simpl in MR. simplify_eq.
        destruct (state_wf_stack_item _ WFT _ _ Eqstk1).
        move : Eqstk' HTOP. eapply access1_active_SRO_preserving; eauto.
Hai Dang's avatar
Hai Dang committed
736
    - intros c cs Eqc. specialize (CINV _ _ Eqc). simpl.
Hai Dang's avatar
Hai Dang committed
737 738 739 740
      clear -Eqα' CINV. destruct CINV as [IN CINV]. split; [done|].
      intros t1 L EqL. specialize (CINV _ _ EqL) as [? CINV]. split; [done|].
      intros l' InL.
      specialize (CINV _ InL) as (stk' & pm' & Eqstk' & Instk' & NDIS).
741 742 743
      destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
        as [stk [Eqstk AS]].
      exists stk, pm'. split; last split; [done| |done]. by apply AS.
Hai Dang's avatar
Hai Dang committed
744
    - rewrite /srel /=. by destruct SREL as (?&?&?&?&?). }
745
  left.
Hai Dang's avatar
Hai Dang committed
746
  apply: sim_body_result. intros. eapply POST; eauto.
Hai Dang's avatar
Hai Dang committed
747
Qed.
748 749 750

(** Write *)

Hai Dang's avatar
Hai Dang committed
751 752 753 754 755 756 757 758 759 760 761 762 763 764
(** For writing to public locations. *)
Lemma sim_body_write_public
  fs ft (r: resUR) n (pl vl: result) σs σt Φ
  (RRELp: rrel r pl pl) (RRELv: rrel r vl vl) :
  ( l t T v α',
    pl = PlaceR l t T  vl = ValR v 
    memory_written σt.(sst) σt.(scs) l t (tsize T) = Some α' 
    let σs' := mkState (write_mem l v σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc) in
    let σt' := mkState (write_mem l v σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc) in
    Φ r n (ValR []%S) σs' (ValR []%S) σt' : Prop) 
  r {n,fs,ft} (pl <- vl, σs)  (pl <- vl, σt) : Φ.
Proof.
  intros POST. pfold. intros NT. intros.
  have WSAT1 := WSAT.
Hai Dang's avatar
Hai Dang committed
765
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
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

  (* make a step *)
  split; [|done|].
  { right.
    edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
    destruct (tstep_write_inv _ _ _ _ _ _ STEPS)
      as (l&t&T&v& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQL & ?).
    symmetry in EqH, EqH'. simplify_eq.
    setoid_rewrite <-(srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
    destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
    rewrite Eqst Eqcs in Eqα'. rewrite EQL in EqD. rewrite Eqnp in IN.
    exists (#[])%V,
           (mkState (write_mem l v σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc)).
    eapply (head_step_fill_tstep _ []), write_head_step'; eauto. }
  constructor 1. intros.
  destruct (tstep_write_inv _ _ _ _ _ _ STEPT)
      as (l&t&T&v& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQL & ?).
  symmetry in EqH, EqH'. simplify_eq.
  set σs' := mkState (write_mem l v σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc).
  have STEPS: ((Place l t T <- v)%E, σs) ~{fs}~> ((#[])%V, σs').
  { setoid_rewrite (srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
    destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
    rewrite -Eqst -Eqcs in Eqα'. rewrite EQL in EqD. rewrite -Eqnp in IN.
    eapply (head_step_fill_tstep _ []), write_head_step'; eauto. }

  (* unfolding rrel for place *)
  simpl in RRELp. destruct RRELp as [VREL _].
  inversion VREL as [|???? ARELp U]; subst; simplify_eq. clear U VREL.
Hai Dang's avatar
Hai Dang committed
794
  destruct ARELp as (_ & _ & ARELp). simpl in RRELv.
Hai Dang's avatar
Hai Dang committed
795 796 797 798

  exists (#[])%V, σs', r, n. split; last split.
  { left. by constructor 1. }
  { destruct (for_each_lookup _ _ _ _ _ Eqα') as [EQ1 _].
Hai Dang's avatar
Hai Dang committed
799
    split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
800 801 802 803
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
    - (* tmap_inv *)
Hai Dang's avatar
Hai Dang committed
804 805 806
      intros t1 k1 h1 Eqt. specialize (PINV _ _ _ Eqt) as [Ltt1 PINV].
      split; [done|]. intros l1 ss st Eqh1.
      specialize (PINV _ _ _ Eqh1).
Hai Dang's avatar
Hai Dang committed
807 808 809 810 811

      destruct (write_mem_lookup_case l v σt.(shp) l1)
          as [[i [Lti [Eqi Eqmi]]]|[NEql Eql]]; last first.
      { (* l1 is NOT written to *)
        destruct (for_each_lookup _ _ _ _ _ Eqα') as [_ [_ EQ]].
Hai Dang's avatar
Hai Dang committed
812
        rewrite EQL in NEql.
813
        destruct (write_mem_lookup l v σs.(shp)) as [_ EQ2].
Hai Dang's avatar
Hai Dang committed
814 815 816
        destruct k1;
          rewrite /= (EQ _ NEql) Eql; rewrite -EQL in NEql; rewrite (EQ2 _ NEql);
          by apply PINV. }
Hai Dang's avatar
Hai Dang committed
817

Hai Dang's avatar
Hai Dang committed
818 819
      (* l1 is written to *)
      subst l1.
Hai Dang's avatar
Hai Dang committed
820
      (* invoke PINV for t *)
Hai Dang's avatar
Hai Dang committed
821 822 823 824 825 826 827 828 829 830 831 832
      have SUB := for_each_access1 _ _ _ _ _ _ _ Eqα'.
      intros PRE.
      destruct PINV as [Eql' [Eql2 HTOP]].
      { destruct k1; [done|..];
          destruct PRE as (stk1 & pm & opro & Eqstk1 & In1 & NDIS);
          simpl in Eqstk1;
          specialize (SUB _ _ Eqstk1) as (stk & Eqstk & SUB & ?);
          destruct (SUB _ In1) as (it2 & In2 & Eqt2 & Eqp2 & NDIS2); simpl in *;
          specialize (NDIS2 NDIS);
          exists stk, pm, opro; (split; [done|]);
          rewrite /= Eqt2 Eqp2 -{1}NDIS2; by destruct it2. }

Hai Dang's avatar
Hai Dang committed
833
      destruct k1.
Hai Dang's avatar
Hai Dang committed
834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855
      + (* k1 is Local  Tagged t1  t, writing with t must have popped t1
            from top, contradicting In1. *)
        exfalso. simpl in *.
        rewrite EQL in Lti.
        specialize (EQ1 _ _ Lti HTOP) as (stk' & Eqstk' & ACC).
        destruct (access1 (init_stack (Tagged t1)) AccessWrite t σt.(scs))
          as [[n1 stk1]|] eqn:ACC1; [|done]. simpl in ACC. simplify_eq.
        specialize (access1_in_stack _ _ _ _ _ _ ACC1)
            as (it1 & In1%elem_of_list_singleton & Eqit & _). subst it1 t.
        move : Eqt. simpl in ARELp. destruct ARELp as [h ARELp].
        rewrite lookup_op ARELp.
        by apply tagKindR_local_exclusive_r.

      + destruct PRE as (stk1 & pm & opro & Eqstk1 & In1 & NDIS);
          simpl in Eqstk1;
          specialize (SUB _ _ Eqstk1) as (stk & Eqstk & _).
        destruct HTOP as (stk' & Eq' & HTOP).
        have ?: stk' = stk. { rewrite Eqstk in Eq'. by inversion Eq'. }
        subst stk'. clear Eq'.

        (* k1 is Unique  Tagged t1  t, writing with t must have popped t1
            from top, contradicting In1. *)
Hai Dang's avatar
Hai Dang committed
856 857 858 859 860 861 862 863
        exfalso.
        rewrite EQL in Lti. destruct (EQ1 _ _ Lti Eqstk) as [ss' [Eq' EQ3]].
        have ?: ss' = stk1. { rewrite Eqstk1 in Eq'. by inversion Eq'. }
        subst ss'. clear Eq'. move : EQ3.
        case access1 as [[n1 stk2]|] eqn:EQ4; [|done].
        simpl. intros ?. simplify_eq.
        have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
        move : In1.
Hai Dang's avatar
Hai Dang committed
864
        eapply (access1_write_remove_incompatible_head _ t t1 _ _ _ ND); [done..|].
Hai Dang's avatar
Hai Dang committed
865 866
        intros ?. subst t. move : Eqt.
        destruct ARELp as [h ARELp]. rewrite lookup_op ARELp.
Hai Dang's avatar
Hai Dang committed
867 868 869 870 871 872 873 874
        by apply tagKindR_uniq_exclusive_r.

      + destruct PRE as (stk1 & pm & opro & Eqstk1 & In1 & NDIS);
          simpl in Eqstk1;
          specialize (SUB _ _ Eqstk1) as (stk & Eqstk & _).
        destruct HTOP as (stk' & Eq' & HTOP).
        have ?: stk' = stk. { rewrite Eqstk in Eq'. by inversion Eq'. }
        subst stk'. clear Eq'.
Hai Dang's avatar
Hai Dang committed
875

Hai Dang's avatar
Hai Dang committed
876
        (* k1 is Public => t1 is for SRO, and must also have been popped,
Hai Dang's avatar
Hai Dang committed
877 878 879 880 881 882 883 884 885 886 887 888 889
          contradicting In1. *)
        exfalso.
        rewrite EQL in Lti. destruct (EQ1 _ _ Lti Eqstk) as [ss' [Eq' EQ3]].
        have ?: ss' = stk1. { rewrite Eqstk1 in Eq'. by inversion Eq'. }
        subst ss'. clear Eq'. move : EQ3.
        case access1 as [[n2 stk2]|] eqn:EQ4; [|done].
        simpl. intros ?. simplify_eq.
        have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
        move : In1.
        eapply (access1_write_remove_incompatible_active_SRO _ t t1 _ _ _ ND); eauto.

    - (* cmap_inv : make sure tags in the new resource are still on top *)
      intros c cs Eqc. simpl. specialize (CINV _ _ Eqc).
Hai Dang's avatar
Hai Dang committed
890
      clear -Eqα' CINV VALID.
Hai Dang's avatar
Hai Dang committed
891
      destruct CINV as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
892 893 894
      intros t1 L EqL. specialize (CINV _ _ EqL) as [? CINV]. split; [done|].
      intros l' InL.
      destruct (CINV _ InL) as (stk' & pm' & Eqstk' & Instk' & NDIS).
Hai Dang's avatar
Hai Dang committed
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
      destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
        as [stk [Eqstk AS]].
      exists stk, pm'. split; last split; [done|by apply AS|done].

    - (* srel *)
      rewrite /srel /=. destruct SREL as (?&?&?&?&PV).
      split; last split; last split; last split; [done..|].
      intros l1 InD1.
      destruct (write_mem_lookup l v σs.(shp)) as [EqN EqO].
      destruct (write_mem_lookup_case l v σt.(shp) l1)
        as [[i [Lti [Eqi Eqmi]]]|[NEql Eql]].
      + subst l1. specialize (EqN _ Lti). (* rewrite EqN. *)
        have InD := (EqD _ Lti). specialize (PV _ InD).
        destruct (lookup_lt_is_Some_2 _ _ Lti) as [s Eqs].
        (* (l + i) was written to *)
        left. intros st. simpl. intros Eqst.
        have ?: st = s. { rewrite Eqmi Eqs in Eqst. by inversion Eqst. }
        subst st. exists s. rewrite EqN. split; [done|].
        (* we know that the values written must be publicly related *)
        apply (arel_mono r _ VALID).
        { apply cmra_included_r. }
        { by apply (Forall2_lookup_lr _ _ _ _ _ _ RRELv Eqs). }
      + specialize (EqO _ NEql).
        have InD1': l1  dom (gset loc) σt.(shp)
          by rewrite elem_of_dom -Eql -(elem_of_dom (D:=gset loc)).
Hai Dang's avatar
Hai Dang committed
920
        specialize (PV _ InD1'). by rewrite /pub_loc EqO Eql. }
Hai Dang's avatar
Hai Dang committed
921 922 923 924 925 926
  left.
  apply: sim_body_result.
  intros. simpl. by eapply POST.
Qed.


Hai Dang's avatar
Hai Dang committed
927 928
(** Writing to unique/local of size 1 *)
Lemma sim_body_write_unique_local_1 fs ft r r' n l t k T vs vt h0 σs σt Φ :
929
  tsize T = 1%nat 
Hai Dang's avatar
Hai Dang committed
930
  r  r'  res_tag t k h0 
Hai Dang's avatar
Hai Dang committed
931
  (k = tkLocal  vs = vt  k = tkUnique  vrel r' vs vt) 
Hai Dang's avatar
Hai Dang committed
932 933 934 935 936
  is_Some (h0 !! l) 
  ( ss st, vs = [ss]  vt = [st] 
    let σs' := mkState (<[l := ss]> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in
    let σt' := mkState (<[l := st]> σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in
    tag_on_top σt'.(sst) l t 
Hai Dang's avatar
Hai Dang committed
937
    Φ (r'  res_tag t k (<[l := (ss,st)]>h0)) n (ValR [%S]) σs' (ValR [%S]) σt') 
938
  r {n,fs,ft}
Hai Dang's avatar
Hai Dang committed
939
    (Place l (Tagged t) T <- #vs, σs)  (Place l (Tagged t) T <- #vt, σt) : Φ.
940
Proof.
Hai Dang's avatar
Hai Dang committed
941
  intros LenT Eqr CASE' IS POST. pfold.
942
  intros NT. intros.
Hai Dang's avatar
Hai Dang committed
943
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
944 945

  (* inversion step *)
Hai Dang's avatar
Hai Dang committed
946
  split; [|done|].
947 948
  { right.
    edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
Hai Dang's avatar
Hai Dang committed
949 950 951 952
    destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPS)
      as (?&?&?&?& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQL & ?).
    symmetry in EqH, EqH'. simplify_eq.
    setoid_rewrite <-(srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
953 954 955
    destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
    rewrite Eqst Eqcs in Eqα'. rewrite Eqnp in IN. rewrite EQL in EqD.
    exists (#[])%V,
Hai Dang's avatar
Hai Dang committed
956 957
           (mkState (write_mem l vt σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc)).
    eapply (head_step_fill_tstep _ []), write_head_step'; eauto.
Hai Dang's avatar
Hai Dang committed
958
    - destruct CASE' as [[]|[? VREL]]; [by subst vs|].
Hai Dang's avatar
Hai Dang committed
959
      by rewrite -(vrel_length _ _ _ VREL).
Hai Dang's avatar
Hai Dang committed
960
    - destruct CASE' as [[]|[? VREL]]; [by subst vs|].
Hai Dang's avatar
Hai Dang committed
961
      by apply (vrel_tag_included _ _ _ _ VREL). }
962
  constructor 1. intros.
Hai Dang's avatar
Hai Dang committed
963
  destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPT)
Hai Dang's avatar
Hai Dang committed
964
      as (?&?&?&?& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQLt & ?).
Hai Dang's avatar
Hai Dang committed
965
  symmetry in EqH, EqH'. simplify_eq.
Hai Dang's avatar
Hai Dang committed
966 967 968
  assert ( st, vt = [st]) as [st ?].
  { rewrite LenT in EQLt. destruct vt as [|st vt]; [simpl in EQLt; lia|].
    exists st. destruct vt; [done|simpl in EQLt; lia]. } subst vt.
Hai Dang's avatar
Hai Dang committed
969
  assert ( ss, vs = [ss]  (k = tkLocal  ss = st  k = tkUnique  arel r' ss st))
Hai Dang's avatar
Hai Dang committed
970
    as (ss & ? & CASE).
Hai Dang's avatar
Hai Dang committed
971
  { destruct CASE' as [[]|[? VREL]]; [subst vs|].
Hai Dang's avatar
Hai Dang committed
972 973 974 975 976 977
    - naive_solver.
    - inversion VREL as [|ss ??? AREL VREL']; simplify_eq.
      inversion VREL'. subst. naive_solver. } subst vs. clear CASE' EQLt.

  (* some lookup properties *)
  have VALIDr := cmra_valid_op_r _ _ VALID. rewrite ->Eqr in VALIDr.
Hai Dang's avatar
Hai Dang committed
978 979 980 981 982 983 984 985 986 987 988 989
  have HLtr: r.(rtm) !! t  Some (to_tgkR k, to_agree <$> h0).
  { rewrite Eqr. destruct CASE as [[]|[]]; subst k.
    - eapply tmap_lookup_op_local_included;
        [apply VALIDr|apply cmra_included_r|]. rewrite res_tag_lookup //.
    - eapply tmap_lookup_op_uniq_included;
        [apply VALIDr|apply cmra_included_r|]. rewrite res_tag_lookup //. }
  have HLtrf: (r_f  r).(rtm) !! t  Some (to_tgkR k, to_agree <$> h0).
  { destruct CASE as [[]|[]]; subst k.
    - apply tmap_lookup_op_r_local_equiv; [apply VALID|done].
    - apply tmap_lookup_op_r_uniq_equiv; [apply VALID|done]. }
  have HLNt: (r_f  r').(rtm) !! t = None.
  { destruct ((r_f  r').(rtm) !! t) as [ls|] eqn:Eqls; [|done].
Hai Dang's avatar
Hai Dang committed
990
    exfalso. move : HLtrf.
Hai Dang's avatar
Hai Dang committed
991 992 993 994 995 996 997 998
    rewrite Eqr cmra_assoc lookup_op Eqls res_tag_lookup.
    destruct CASE as [[]|[]]; subst k.
    - apply tagKindR_exclusive_local_heaplet.
    - apply tagKindR_exclusive_heaplet. }
  have EQrcm : (r_f  r'  res_tag t k h0).(rcm) 
               (r_f  r'  res_tag t k (<[l := (ss,st)]>h0)).(rcm) by done.
  have HLtr': (r_f  r'  res_tag t k (<[l := (ss,st)]>h0)).(rtm) !! t 
                  Some (to_tgkR k, to_agree <$> (<[l := (ss,st)]>h0)).
Hai Dang's avatar
Hai Dang committed
999 1000 1001 1002 1003 1004 1005 1006 1007
  { rewrite lookup_op HLNt left_id res_tag_lookup //. }

  (* Unique: stack unchanged *)
  destruct (for_each_lookup_case_2 _ _ _ _ _ Eqα') as [EQ1 _].
  specialize (EQ1 O) as (stk & stk' & Eqstk & Eqstk' & ACC1); [rewrite LenT; lia|].
  rewrite shift_loc_0_nat in Eqstk, Eqstk'.
  move : ACC1. case access1 as [[n1 stk1]|] eqn:ACC1; [|done].
  simpl. intros Eqs1. symmetry in Eqs1. simplify_eq.

Hai Dang's avatar
Hai Dang committed
1008
  destruct IS as [[ss' st'] Eqs0].
Hai Dang's avatar
Hai Dang committed
1009

Hai Dang's avatar
Hai Dang committed
1010 1011 1012
  have Lk : k = tkLocal  k = tkUnique by (destruct CASE as [[]|[]]; [left|right]).
  destruct (local_unique_access_head _ _ _ _ _ _ _ _ _ ss' st' k (to_agree <$> h0)
             WFT Lk Eqstk ACC1 PINV HLtrf)
Hai Dang's avatar
Hai Dang committed
1013 1014
    as (it & Eqpit & Eqti & HDi & Eqhp); [by rewrite lookup_fmap Eqs0 |].

1015
  have ?: α' = σt.(sst).
Hai Dang's avatar
Hai Dang committed
1016 1017
  { move : Eqα'.
    rewrite LenT /= /memory_written /= shift_loc_0_nat Eqstk /= ACC1 /=.
Hai Dang's avatar
Hai Dang committed
1018 1019
    destruct (tag_unique_head_access σt.(scs) stk (Tagged t)
                it.(protector) AccessWrite) as [ns Eqss].
Hai Dang's avatar
Hai Dang committed
1020 1021 1022 1023 1024 1025 1026 1027
    - destruct HDi as [stk' Eq']. exists stk'. rewrite Eq'. f_equal.
      rewrite -Eqpit -Eqti. by destruct it.
    - rewrite ACC1 in Eqss. simplify_eq. rewrite insert_id //. by inversion 1. }
  subst α'. rewrite Eqstk in Eqstk'. symmetry in Eqstk'. simplify_eq.

  have TOT: tag_on_top σt.(sst) l t.
  { destruct HDi as [stk' Eqstk'].
    rewrite /tag_on_top Eqstk Eqstk' /= -Eqpit -Eqti. destruct it. by eexists. }
1028

Hai Dang's avatar
Hai Dang committed
1029 1030 1031
  (* source step *)
  set σs' := mkState (<[l := ss]> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc).
  have STEPS: ((Place l (Tagged t) T <- #[ss])%E, σs) ~{fs}~> ((#[])%V, σs').
1032 1033
  { setoid_rewrite (srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
    destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
Hai Dang's avatar
Hai Dang committed
1034 1035
    rewrite -Eqst -Eqcs in Eqα'. rewrite -Eqnp in IN.
    eapply (head_step_fill_tstep _ []), write_head_step'; eauto.
Hai Dang's avatar
Hai Dang committed
1036
    - destruct CASE as [[]|[ AREL']]; [by subst ss|].
Hai Dang's avatar
Hai Dang committed
1037 1038
      eapply vrel_tag_included; [|eauto]. by constructor.
    - rewrite LenT //. }
1039

1040
  have ?: ss = st.
Hai Dang's avatar
Hai Dang committed
1041
  { destruct CASE as [[]|[]]; [done|]. by eapply arel_eq. } subst ss.
1042

Hai Dang's avatar
Hai Dang committed
1043
  exists (#[])%V, σs', (r'  res_tag t k (<[l:=(st,st)]> h0)), n.
1044 1045