refl_mem_step.v 86.9 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
        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)
Hai Dang's avatar
Hai Dang committed
104
            as [[Eql1 NEQl1]|(i & Lti & Eql1)].
Hai Dang's avatar
Hai Dang committed
105 106 107
          - rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1).
            apply PINV. by exists stk, pm, opro.
          - subst l1.
Hai Dang's avatar
Hai Dang committed
108
            have Eq2 := HLst1 _ Lti. rewrite Eqstk in Eq2.
Hai Dang's avatar
Hai Dang committed
109 110 111 112
            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)
Hai Dang's avatar
Hai Dang committed
113
            as [[Eql1 NEQl1]|(i & Lti & Eql1)].
Hai Dang's avatar
Hai Dang committed
114 115 116
          - rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1).
            apply PINV. by exists stk, pm, opro.
          - subst l1.
Hai Dang's avatar
Hai Dang committed
117
            have Eq2 := HLst1 _ Lti. rewrite Eqstk in Eq2.
Hai Dang's avatar
Hai Dang committed
118
            simplify_eq. apply elem_of_list_singleton in Instk. simplify_eq. }
119
    - intros c cs. subst σt'. rewrite Eqrcm /=. intros Eqc.
Hai Dang's avatar
Hai Dang committed
120
      specialize (CINV _ _ Eqc) as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
121 122
      intros t1 tls1 [Ltc Ht]%CINV. split; [lia|].
      intros l1 Inl1.
Hai Dang's avatar
Hai Dang committed
123
      case (decide (t1 = σt.(snp))) => ?; [subst t1|]; [lia|].
Hai Dang's avatar
Hai Dang committed
124
      specialize (Ht _  Inl1) as (stk1 & pm1 & Eql1 & Eqp).
Hai Dang's avatar
Hai Dang committed
125
      destruct (init_stacks_lookup_case_2 _ l (tsize T) t _ _ Eql1)
Hai Dang's avatar
Hai Dang committed
126
        as [[EQ NEQ1]|(i & Lti & ? & EQ)].
Hai Dang's avatar
Hai Dang committed
127 128 129 130
      + 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
131
    - subst σt'. split; last split; last split; last split; [|simpl; auto..|].
Hai Dang's avatar
Hai Dang committed
132 133 134
      { by rewrite /= Eqst. } simpl.
      intros l1 [s1 HL1]%elem_of_dom.
      destruct (init_mem_lookup_case _ _ _ _ _ HL1)
Hai Dang's avatar
Hai Dang committed
135
        as [[Eqs1 NEQ]|(i & Lti & Eql)].
Hai Dang's avatar
Hai Dang committed
136 137 138 139 140 141 142
      + 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
143 144 145 146
        * 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
147
          { apply tmap_lookup_op_l_uniq_equiv; [apply VALID'|done]. }
Hai Dang's avatar
Hai Dang committed
148
      + right. exists σt.(snp), tkLocal. subst l1. eexists.
Hai Dang's avatar
Hai Dang committed
149
        split; last split.
Hai Dang's avatar
Hai Dang committed
150
        * rewrite HEQr'; eauto.
Hai Dang's avatar
Hai Dang committed
151
        * destruct (write_hpl_is_Some l vst  i) as [? EQ].
Hai Dang's avatar
Hai Dang committed
152
          { by rewrite repeat_length. }
Hai Dang's avatar
Hai Dang committed
153
          { rewrite lookup_fmap EQ. by eexists. }
Hai Dang's avatar
Hai Dang committed
154
        * by left. }
155
  left.
Ralf Jung's avatar
Ralf Jung committed
156
  apply: sim_body_result. intros.
157
  apply POST; eauto.
Hai Dang's avatar
Hai Dang committed
158
Qed.
Hai Dang's avatar
Hai Dang committed
159

Hai Dang's avatar
Hai Dang committed
160
Lemma sim_body_alloc_public fs ft r n T σs σt Φ :
Hai Dang's avatar
Hai Dang committed
161 162 163 164
  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)
165
                     (S σs.(snp)) σs.(snc) in
Hai Dang's avatar
Hai Dang committed
166 167
  let σt' := mkState (init_mem l (tsize T) σt.(shp))
                     (init_stacks σt.(sst) l (tsize T) t) σt.(scs)
168
                     (S σt.(snp)) σt.(snc) in
Hai Dang's avatar
Hai Dang committed
169 170
  let r' : resUR := res_tag σt.(snp) tkPub  in
  Φ (r  r') n (PlaceR l t T) σs' (PlaceR l t T) σt' 
171 172
  r {n,fs,ft} (Alloc T, σs)  (Alloc T, σt) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
173
  intros l t σs' σt' r' POST.
174 175 176
  pfold. intros NT. intros.
  have EqDOM := wsat_heap_dom _ _ _ WSAT.
  have EqFRESH := fresh_block_equiv _ _ EqDOM.
Hai Dang's avatar
Hai Dang committed
177
  have HNP := wsat_tmap_nxtp _ _ _ WSAT.
Hai Dang's avatar
Hai Dang committed
178
  have HEQr': (r_f  r  r').(rtm) !! snp σt  Some (to_tgkR tkPub, to_hplR ).
Hai Dang's avatar
Hai Dang committed
179
  { rewrite lookup_op HNP left_id res_tag_lookup //. }
Hai Dang's avatar
Hai Dang committed
180
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
181 182
  destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&REL).
  have Eqlst: l = (fresh_block σs.(shp), 0). { by rewrite /l EqFRESH. }
183 184 185 186 187
  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
188 189 190 191
  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.
192
  { left. by apply tc_once. }
Hai Dang's avatar
Hai Dang committed
193 194
  { have Eqrcm: (r_f  r  r').(rcm)  (r_f  r).(rcm)
      by rewrite /rcm /= right_id.
195 196
    have VALID':  (r_f  r  r').
    { apply (local_update_discrete_valid_frame _ ε r'); [by rewrite right_id|].
Hai Dang's avatar
Hai Dang committed
197 198
      rewrite /= right_id -cmra_assoc cmra_assoc.
      by apply res_tag_alloc_local_update. }
199
    rewrite cmra_assoc.
Hai Dang's avatar
Hai Dang committed
200 201 202 203
    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
204
    split; last split; last split; last split; last split.
205 206 207
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
Hai Dang's avatar
Hai Dang committed
208 209 210 211 212
    - 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
213
        intros l1 ss1 st1. rewrite -Eqh1 lookup_fmap lookup_empty. by inversion 1.
Hai Dang's avatar
Hai Dang committed
214
      + intros Eqh'.
Hai Dang's avatar
Hai Dang committed
215
        have Eqh1: (r_f  r).(rtm) !! t1  Some (to_tgkR k1, h1).
Hai Dang's avatar
Hai Dang committed
216
        { move : Eqh'. rewrite lookup_op lookup_insert_ne // right_id //. }
Hai Dang's avatar
Hai Dang committed
217
        specialize (PINV _ _ _ Eqh1) as [? PINV]. split; [simpl; lia|].
Hai Dang's avatar
Hai Dang committed
218 219 220 221 222 223 224 225 226
        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)
Hai Dang's avatar
Hai Dang committed
227
            as [[Eql1 NEQl1]|(i & Lti & Eql1)].
Hai Dang's avatar
Hai Dang committed
228 229 230
          - rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1).
            apply PINV. by exists stk, pm, opro.
          - subst l1.
Hai Dang's avatar
Hai Dang committed
231
            have Eq2 := HLst1 _ Lti. rewrite Eqstk in Eq2.
Hai Dang's avatar
Hai Dang committed
232 233 234 235
            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)
Hai Dang's avatar
Hai Dang committed
236
            as [[Eql1 NEQl1]|(i & Lti & Eql1)].
Hai Dang's avatar
Hai Dang committed
237 238 239
          - rewrite /= (HLmt2 _ NEQl1) (HLms2 _ NEQl1) (HLst2 _ NEQl1).
            apply PINV. by exists stk, pm, opro.
          - subst l1.
Hai Dang's avatar
Hai Dang committed
240
            have Eq2 := HLst1 _ Lti. rewrite Eqstk in Eq2.
Hai Dang's avatar
Hai Dang committed
241
            simplify_eq. apply elem_of_list_singleton in Instk. simplify_eq. }
Hai Dang's avatar
Hai Dang committed
242
    - intros c cs. subst σt'. rewrite Eqrcm /=. intros Eqc.
Hai Dang's avatar
Hai Dang committed
243
      specialize (CINV _ _ Eqc) as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
244 245
      intros t1 tls1 [Ltc Ht]%CINV. split; [lia|].
      intros l1 Inl1.
Hai Dang's avatar
Hai Dang committed
246
      case (decide (t1 = σt.(snp))) => ?; [subst t1|]; [lia|].
Hai Dang's avatar
Hai Dang committed
247
      specialize (Ht _  Inl1) as (stk1 & pm1 & Eql1 & Eqp).
Hai Dang's avatar
Hai Dang committed
248
      destruct (init_stacks_lookup_case_2 _ l (tsize T) t _ _ Eql1)
Hai Dang's avatar
Hai Dang committed
249
        as [[EQ NEQ1]|(i & Lti & ? & EQ)].
Hai Dang's avatar
Hai Dang committed
250 251 252 253 254 255 256 257
      + 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)
Hai Dang's avatar
Hai Dang committed
258
        as [[Eqs1 NEQ]|(i & Lti & Eql)].
Hai Dang's avatar
Hai Dang committed
259 260 261 262 263 264 265
      + 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
266 267 268 269
        * 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
270
          { apply tmap_lookup_op_l_uniq_equiv; [apply VALID'|done]. }
Hai Dang's avatar
Hai Dang committed
271
      + left. subst l1. intros st. simpl.
Hai Dang's avatar
Hai Dang committed
272
        specialize (HLmt1 _ Lti). specialize (HLms1 _ Lti).
Hai Dang's avatar
Hai Dang committed
273
        rewrite HLmt1 HLms1. inversion 1. subst st. by exists ScPoison. }
274
  left.
Ralf Jung's avatar
Ralf Jung committed
275
  apply: sim_body_result. intros.
Hai Dang's avatar
Hai Dang committed
276
  apply POST; eauto.
Hai Dang's avatar
Hai Dang committed
277
Qed.
278

Hai Dang's avatar
Hai Dang committed
279
(** Free *)
Hai Dang's avatar
Hai Dang committed
280
Lemma sim_body_free_public fs ft r n (pl: result) σs σt Φ
Hai Dang's avatar
Hai Dang committed
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 327 328 329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350
  (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 _].
Hai Dang's avatar
Hai Dang committed
351 352
          destruct (EQ1 _ Lti) as (stk1 & stk' & Eqstk & EqN & DA).
          rewrite Eqstk in HTOP. simplify_eq.
Hai Dang's avatar
Hai Dang committed
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
          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. *)
Hai Dang's avatar
Hai Dang committed
388
      destruct (block_case l l1 (tsize T)) as [NEql|(i & Lti & Eql)].
Hai Dang's avatar
Hai Dang committed
389 390 391
      + rewrite EQ2 //.
      + exfalso. clear EQ2.
        subst l1. destruct CINV as (stk & pm & Eqstk & Instk & ?).
Hai Dang's avatar
Hai Dang committed
392
        specialize (EQ1 _ Lti) as (stk1 & stk' & Eqstk1 & Eqstk' & DA).
Hai Dang's avatar
Hai Dang committed
393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411
        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
412
(** Freeing unique/local *)
Hai Dang's avatar
Hai Dang committed
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 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
(* 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 (σ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 _].
Hai Dang's avatar
Hai Dang committed
498 499
          destruct (EQ1 _ Lti) as (stk1 & stk' & Eqstk & EqN & DA).
          rewrite Eqstk in HTOP. simplify_eq.
Hai Dang's avatar
Hai Dang committed
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
          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. *)
Hai Dang's avatar
Hai Dang committed
534
      destruct (block_case l l1 (tsize T)) as [NEql|(i & Lti & Eql)].
Hai Dang's avatar
Hai Dang committed
535 536 537
      + rewrite EQ2 //.
      + exfalso. clear EQ2.
        subst l1. destruct CINV as (stk & pm & Eqstk & Instk & ?).
Hai Dang's avatar
Hai Dang committed
538
        specialize (EQ1 _ Lti) as (stk1 & stk' & Eqstk1 & Eqstk' & DA).
Hai Dang's avatar
Hai Dang committed
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
        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.

578
(** Copy *)
Hai Dang's avatar
Hai Dang committed
579 580 581 582 583 584 585
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 α' 
586 587
      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
588
      vrel ((* r   *) r') vs vt  Φ (r  r') n (ValR vs) σs' (ValR vt) σt') 
Hai Dang's avatar
Hai Dang committed
589
  r {n,fs,ft} (Copy pl, σs)  (Copy pl, σt) : Φ.
590
Proof.
Hai Dang's avatar
Hai Dang committed
591 592
  intros POST. pfold. intros NT. intros.
  have WSAT1 := WSAT. (* backup *)
Hai Dang's avatar
Hai Dang committed
593 594

  (* making a step *)
Hai Dang's avatar
Hai Dang committed
595
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
596 597
  split; [|done|].
  { right.
Hai Dang's avatar
Hai Dang committed
598
    destruct (NT (Copy pl) σs) as [[]|[es' [σs' STEPS]]];
599
      [done..|].
Hai Dang's avatar
Hai Dang committed
600 601 602 603 604 605 606
    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. }
607 608 609
    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
610 611 612 613 614 615 616
  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. }
617
  set σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc).
Hai Dang's avatar
Hai Dang committed
618
  have STEPS: (Copy (Place l t T), σs) ~{fs}~> ((#vs)%E, σs').
619
  { by eapply (head_step_fill_tstep _ []), copy_head_step'. }
Hai Dang's avatar
Hai Dang committed
620 621 622 623 624 625 626

  (* 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 *)
627 628
  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
629
  { destruct SREL as (Eqst & Eqnp & Eqcs & Eqnc & PRIV).
630 631 632 633 634 635 636
    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
637 638 639 640
    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 _].
641
    rewrite Eqlt in HLLt.
Hai Dang's avatar
Hai Dang committed
642 643 644 645 646 647 648 649 650 651 652 653 654 655
    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 *)
656 657 658
  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
659
    split; last split; last split; last split; last split.
660 661 662
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
Hai Dang's avatar
Hai Dang committed
663
    - intros t1 k h Eqt. specialize (PINV t1 k h Eqt) as [Lt PI]. simpl.
Hai Dang's avatar
Hai Dang committed
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 689 690 691 692 693 694 695 696 697 698 699 700
      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
701 702 703 704 705
        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
706 707 708 709 710 711 712 713 714 715 716 717
      + 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
718
    - intros c cs Eqc. specialize (CINV _ _ Eqc). simpl.
Hai Dang's avatar
Hai Dang committed
719 720 721 722
      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).
723 724 725
      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
726
    - rewrite /srel /=. by destruct SREL as (?&?&?&?&?). }
727
  left.
Hai Dang's avatar
Hai Dang committed
728
  apply: sim_body_result. intros. eapply POST; eauto.
Hai Dang's avatar
Hai Dang committed
729
Qed.
730 731 732

(** Write *)

Hai Dang's avatar
Hai Dang committed
733 734 735 736 737 738 739 740 741 742 743 744 745 746
(** 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
747
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775

  (* 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
776
  destruct ARELp as (_ & _ & ARELp). simpl in RRELv.
Hai Dang's avatar
Hai Dang committed
777 778 779 780

  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
781
    split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
782 783 784 785
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
    - (* tmap_inv *)
Hai Dang's avatar
Hai Dang committed
786 787 788
      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
789 790 791 792 793

      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
794
        rewrite EQL in NEql.
795
        destruct (write_mem_lookup l v σs.(shp)) as [_ EQ2].
Hai Dang's avatar
Hai Dang committed
796 797 798
        destruct k1;
          rewrite /= (EQ _ NEql) Eql; rewrite -EQL in NEql; rewrite (EQ2 _ NEql);
          by apply PINV. }
Hai Dang's avatar
Hai Dang committed
799

Hai Dang's avatar
Hai Dang committed
800 801
      (* l1 is written to *)
      subst l1.
Hai Dang's avatar
Hai Dang committed
802
      (* invoke PINV for t *)
Hai Dang's avatar
Hai Dang committed
803 804 805 806 807 808 809 810 811 812 813 814
      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
815
      destruct k1.
Hai Dang's avatar
Hai Dang committed
816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837
      + (* 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
838 839 840 841 842 843 844 845
        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
846
        eapply (access1_write_remove_incompatible_head _ t t1 _ _ _ ND); [done..|].
Hai Dang's avatar
Hai Dang committed
847 848
        intros ?. subst t. move : Eqt.
        destruct ARELp as [h ARELp]. rewrite lookup_op ARELp.
Hai Dang's avatar
Hai Dang committed
849 850 851 852 853 854 855 856
        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
857

Hai Dang's avatar
Hai Dang committed
858
        (* k1 is Public => t1 is for SRO, and must also have been popped,
Hai Dang's avatar
Hai Dang committed
859 860 861 862 863 864 865 866 867 868 869 870 871
          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
872
      clear -Eqα' CINV VALID.
Hai Dang's avatar
Hai Dang committed
873
      destruct CINV as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
874 875 876
      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
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
      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
902
        specialize (PV _ InD1'). by rewrite /pub_loc EqO Eql. }
Hai Dang's avatar
Hai Dang committed
903 904 905 906 907 908
  left.
  apply: sim_body_result.
  intros. simpl. by eapply POST.
Qed.


Hai Dang's avatar
Hai Dang committed
909 910
(** 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 Φ :
911
  tsize T = 1%nat 
Hai Dang's avatar
Hai Dang committed
912
  r  r'  res_tag t k h0 
Hai Dang's avatar
Hai Dang committed
913
  (k = tkLocal  vs = vt  k = tkUnique  vrel r' vs vt) 
Hai Dang's avatar
Hai Dang committed
914 915 916 917
  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
Hai Dang's avatar
Hai Dang committed
918
    tag_on_top σt'.(sst) l t Unique 
Hai Dang's avatar
Hai Dang committed
919
    Φ (r'  res_tag t k (<[l := (ss,st)]>h0)) n (ValR [%S]) σs' (ValR [%S]) σt') 
920
  r {n,fs,ft}
Hai Dang's avatar
Hai Dang committed
921
    (Place l (Tagged t) T <- #vs, σs)  (Place l (Tagged t) T <- #vt, σt) : Φ.
922
Proof.
Hai Dang's avatar
Hai Dang committed
923
  intros LenT Eqr CASE' IS POST. pfold.
924
  intros NT. intros.
Hai Dang's avatar
Hai Dang committed
925
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
926 927

  (* inversion step *)
Hai Dang's avatar
Hai Dang committed
928
  split; [|done|].
929 930
  { right.
    edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
Hai Dang's avatar
Hai Dang committed
931 932 933 934
    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.
935 936 937
    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
938 939
           (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
940
    - destruct CASE' as [[]|[? VREL]]; [by subst vs|].
Hai Dang's avatar
Hai Dang committed
941
      by rewrite -(vrel_length _ _ _ VREL).
Hai Dang's avatar
Hai Dang committed
942
    - destruct CASE' as [[]|[? VREL]]; [by subst vs|].
Hai Dang's avatar
Hai Dang committed
943
      by apply (vrel_tag_included _ _ _ _ VREL). }
944
  constructor 1. intros.
Hai Dang's avatar
Hai Dang committed
945
  destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPT)
Hai Dang's avatar
Hai Dang committed
946
      as (?&?&?&?& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQLt & ?).
Hai Dang's avatar
Hai Dang committed
947
  symmetry in EqH, EqH'. simplify_eq.
Hai Dang's avatar
Hai Dang committed
948 949 950
  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
951
  assert ( ss, vs = [ss]  (k = tkLocal  ss = st  k = tkUnique  arel r' ss st))
Hai Dang's avatar
Hai Dang committed
952
    as (ss & ? & CASE).
Hai Dang's avatar
Hai Dang committed
953
  { destruct CASE' as [[]|[? VREL]]; [subst vs|].
Hai Dang's avatar
Hai Dang committed
954 955 956 957 958 959
    - 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
960 961 962 963 964 965 966 967 968 969 970 971
  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
972
    exfalso. move : HLtrf.
Hai Dang's avatar
Hai Dang committed
973 974 975 976 977 978 979 980
    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
981 982 983 984 985 986 987 988 989
  { 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
990
  destruct IS as [[ss' st'] Eqs0].
Hai Dang's avatar
Hai Dang committed
991

Hai Dang's avatar
Hai Dang committed
992 993 994
  have Lk : k = tkLocal  k = tkUnique by (destruct CASE as [[]|[]]; [left|right]).
  destruct (local_unique_access_head _ _