refl_mem_step.v 63.1 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 286

(** Copy *)
Hai Dang's avatar
Hai Dang committed
287 288 289 290 291 292 293
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 α' 
294 295
      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
296
      vrel ((* r   *) r') vs vt  Φ (r  r') n (ValR vs) σs' (ValR vt) σt') 
Hai Dang's avatar
Hai Dang committed
297
  r {n,fs,ft} (Copy pl, σs)  (Copy pl, σt) : Φ.
298
Proof.
Hai Dang's avatar
Hai Dang committed
299 300
  intros POST. pfold. intros NT. intros.
  have WSAT1 := WSAT. (* backup *)
Hai Dang's avatar
Hai Dang committed
301 302

  (* making a step *)
Hai Dang's avatar
Hai Dang committed
303
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
304 305
  split; [|done|].
  { right.
Hai Dang's avatar
Hai Dang committed
306
    destruct (NT (Copy pl) σs) as [[]|[es' [σs' STEPS]]];
307
      [done..|].
Hai Dang's avatar
Hai Dang committed
308 309 310 311 312 313 314
    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. }
315 316 317
    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
318 319 320 321 322 323 324
  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. }
325
  set σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc).
Hai Dang's avatar
Hai Dang committed
326
  have STEPS: (Copy (Place l t T), σs) ~{fs}~> ((#vs)%E, σs').
327
  { by eapply (head_step_fill_tstep _ []), copy_head_step'. }
Hai Dang's avatar
Hai Dang committed
328 329 330 331 332 333 334

  (* 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 *)
335 336
  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
337
  { destruct SREL as (Eqst & Eqnp & Eqcs & Eqnc & PRIV).
338 339 340 341 342 343 344
    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
345 346 347 348
    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 _].
349
    rewrite Eqlt in HLLt.
Hai Dang's avatar
Hai Dang committed
350 351 352 353 354 355 356 357 358 359 360 361 362 363
    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 *)
364 365 366
  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
367
    split; last split; last split; last split; last split.
368 369 370
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
Hai Dang's avatar
Hai Dang committed
371
    - intros t1 k h Eqt. specialize (PINV t1 k h Eqt) as [Lt PI]. simpl.
Hai Dang's avatar
Hai Dang committed
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
      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
409 410 411 412 413
        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
414 415 416 417 418 419 420 421 422 423 424 425
      + 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
426
    - intros c cs Eqc. specialize (CINV _ _ Eqc). simpl.
Hai Dang's avatar
Hai Dang committed
427 428 429 430
      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).
431 432 433
      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
434
    - rewrite /srel /=. by destruct SREL as (?&?&?&?&?). }
435
  left.
Hai Dang's avatar
Hai Dang committed
436
  apply: sim_body_result. intros. eapply POST; eauto.
Hai Dang's avatar
Hai Dang committed
437
Qed.
438 439 440

(** Write *)

Hai Dang's avatar
Hai Dang committed
441 442 443 444 445 446 447 448 449 450 451 452 453 454
(** 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
455
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
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

  (* 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
484
  destruct ARELp as (_ & _ & ARELp). simpl in RRELv.
Hai Dang's avatar
Hai Dang committed
485 486 487 488

  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
489
    split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
490 491 492 493
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
    - (* tmap_inv *)
Hai Dang's avatar
Hai Dang committed
494 495 496
      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
497 498 499 500 501

      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
502
        rewrite EQL in NEql.
503
        destruct (write_mem_lookup l v σs.(shp)) as [_ EQ2].
Hai Dang's avatar
Hai Dang committed
504 505 506
        destruct k1;
          rewrite /= (EQ _ NEql) Eql; rewrite -EQL in NEql; rewrite (EQ2 _ NEql);
          by apply PINV. }
Hai Dang's avatar
Hai Dang committed
507

Hai Dang's avatar
Hai Dang committed
508 509
      (* l1 is written to *)
      subst l1.
Hai Dang's avatar
Hai Dang committed
510
      (* invoke PINV for t *)
Hai Dang's avatar
Hai Dang committed
511 512 513 514 515 516 517 518 519 520 521 522
      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
523
      destruct k1.
Hai Dang's avatar
Hai Dang committed
524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545
      + (* 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
546 547 548 549 550 551 552 553
        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
554
        eapply (access1_write_remove_incompatible_head _ t t1 _ _ _ ND); [done..|].
Hai Dang's avatar
Hai Dang committed
555 556
        intros ?. subst t. move : Eqt.
        destruct ARELp as [h ARELp]. rewrite lookup_op ARELp.
Hai Dang's avatar
Hai Dang committed
557 558 559 560 561 562 563 564
        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
565

Hai Dang's avatar
Hai Dang committed
566
        (* k1 is Public => t1 is for SRO, and must also have been popped,
Hai Dang's avatar
Hai Dang committed
567 568 569 570 571 572 573 574 575 576 577 578 579
          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
580
      clear -Eqα' CINV VALID.
Hai Dang's avatar
Hai Dang committed
581
      destruct CINV as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
582 583 584
      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
585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609
      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
610
        specialize (PV _ InD1'). by rewrite /pub_loc EqO Eql. }
Hai Dang's avatar
Hai Dang committed
611 612 613 614 615 616
  left.
  apply: sim_body_result.
  intros. simpl. by eapply POST.
Qed.


Hai Dang's avatar
Hai Dang committed
617 618
(** 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 Φ :
619
  tsize T = 1%nat 
Hai Dang's avatar
Hai Dang committed
620
  r  r'  res_tag t k h0 
Hai Dang's avatar
Hai Dang committed
621
  (k = tkLocal  vs = vt  k = tkUnique  vrel r' vs vt) 
Hai Dang's avatar
Hai Dang committed
622 623 624 625 626
  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
627
    Φ (r'  res_tag t k (<[l := (ss,st)]>h0)) n (ValR [%S]) σs' (ValR [%S]) σt') 
628
  r {n,fs,ft}
Hai Dang's avatar
Hai Dang committed
629
    (Place l (Tagged t) T <- #vs, σs)  (Place l (Tagged t) T <- #vt, σt) : Φ.
630
Proof.
Hai Dang's avatar
Hai Dang committed
631
  intros LenT Eqr CASE' IS POST. pfold.
632
  intros NT. intros.
Hai Dang's avatar
Hai Dang committed
633
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
634 635

  (* inversion step *)
Hai Dang's avatar
Hai Dang committed
636
  split; [|done|].
637 638
  { right.
    edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
Hai Dang's avatar
Hai Dang committed
639 640 641 642
    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.
643 644 645
    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
646 647
           (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
648
    - destruct CASE' as [[]|[? VREL]]; [by subst vs|].
Hai Dang's avatar
Hai Dang committed
649
      by rewrite -(vrel_length _ _ _ VREL).
Hai Dang's avatar
Hai Dang committed
650
    - destruct CASE' as [[]|[? VREL]]; [by subst vs|].
Hai Dang's avatar
Hai Dang committed
651
      by apply (vrel_tag_included _ _ _ _ VREL). }
652
  constructor 1. intros.
Hai Dang's avatar
Hai Dang committed
653
  destruct (tstep_write_inv _ (PlaceR _ _ _) (ValR _) _ _ _ STEPT)
Hai Dang's avatar
Hai Dang committed
654
      as (?&?&?&?& α' & EqH & EqH' & ? & Eqα' & EqD & IN & EQLt & ?).
Hai Dang's avatar
Hai Dang committed
655
  symmetry in EqH, EqH'. simplify_eq.
Hai Dang's avatar
Hai Dang committed
656 657 658
  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
659
  assert ( ss, vs = [ss]  (k = tkLocal  ss = st  k = tkUnique  arel r' ss st))
Hai Dang's avatar
Hai Dang committed
660
    as (ss & ? & CASE).
Hai Dang's avatar
Hai Dang committed
661
  { destruct CASE' as [[]|[? VREL]]; [subst vs|].
Hai Dang's avatar
Hai Dang committed
662 663 664 665 666 667
    - 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
668 669 670 671 672 673 674 675 676 677 678 679
  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
680
    exfalso. move : HLtrf.
Hai Dang's avatar
Hai Dang committed
681 682 683 684 685 686 687 688
    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
689 690 691 692 693 694 695 696 697
  { 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
698
  destruct IS as [[ss' st'] Eqs0].
Hai Dang's avatar
Hai Dang committed
699

Hai Dang's avatar
Hai Dang committed
700 701 702
  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
703 704
    as (it & Eqpit & Eqti & HDi & Eqhp); [by rewrite lookup_fmap Eqs0 |].

705
  have ?: α' = σt.(sst).
Hai Dang's avatar
Hai Dang committed
706 707
  { move : Eqα'.
    rewrite LenT /= /memory_written /= shift_loc_0_nat Eqstk /= ACC1 /=.
Hai Dang's avatar
Hai Dang committed
708 709
    destruct (tag_unique_head_access σt.(scs) stk (Tagged t)
                it.(protector) AccessWrite) as [ns Eqss].
Hai Dang's avatar
Hai Dang committed
710 711 712 713 714 715 716 717
    - 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. }
718

Hai Dang's avatar
Hai Dang committed
719 720 721
  (* 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').
722 723
  { 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
724 725
    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
726
    - destruct CASE as [[]|[ AREL']]; [by subst ss|].
Hai Dang's avatar
Hai Dang committed
727 728
      eapply vrel_tag_included; [|eauto]. by constructor.
    - rewrite LenT //. }
729

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

Hai Dang's avatar
Hai Dang committed
733
  exists (#[])%V, σs', (r'  res_tag t k (<[l:=(st,st)]> h0)), n.
734 735
  split; last split.
  { left. by constructor 1. }
Hai Dang's avatar
Hai Dang committed
736 737 738
  { rewrite cmra_assoc.
    have VALID' :  (r_f  r'  res_tag t k (<[l:=(st,st)]> h0)).
    { move : VALID. rewrite Eqr cmra_assoc => VALID.
Hai Dang's avatar
Hai Dang committed
739
      apply (local_update_discrete_valid_frame _ _ _ VALID).
Hai Dang's avatar
Hai Dang committed
740
      by apply res_tag_uniq_local_update. }
Hai Dang's avatar
Hai Dang committed
741

Hai Dang's avatar
Hai Dang committed
742
    split; last split; last split; last split; last split.
743 744
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
Hai Dang's avatar
Hai Dang committed
745
    - done.
Hai Dang's avatar
Hai Dang committed
746 747 748 749

    (* tmap_inv *)
    - intros t1 k1 h1 HL1. simpl.
      case (decide (t1 = t)) => ?; [subst t1|].
Hai Dang's avatar
Hai Dang committed
750
      + specialize (PINV _ _ _ HLtrf) as [? PINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
751
        move : HL1. rewrite HLtr'.
Hai Dang's avatar
Hai Dang committed
752
        intros [Eq1%leibniz_equiv_iff Eq2]%Some_equiv_inj. simpl in Eq1, Eq2.
Hai Dang's avatar
Hai Dang committed
753 754
        have ?: k1 = k. { destruct k, k1; inversion Eq1; done. }
        subst k1. clear Eq1.
Hai Dang's avatar
Hai Dang committed
755
        intros l1 ss1 st1. rewrite -Eq2 lookup_fmap.
Hai Dang's avatar
Hai Dang committed
756 757
        case (decide (l1 = l)) => ?; [subst l1|].
        * rewrite lookup_insert. intros Eq%Some_equiv_inj%to_agree_inj.
Hai Dang's avatar
Hai Dang committed
758 759 760 761 762
          symmetry in Eq. simplify_eq.
          rewrite 2!lookup_insert. intros PRE. do 2 (split; [done|]).
          specialize (PINV l ss' st'). rewrite lookup_fmap Eqs0 in PINV.
          specialize (PINV ltac:(done)).
          destruct CASE as [[]|[]]; subst k; by apply PINV.
Hai Dang's avatar
Hai Dang committed
763
        * rewrite lookup_insert_ne // -lookup_fmap.
Hai Dang's avatar
Hai Dang committed
764
          intros Eq. specialize (PINV _ _ _ Eq).
765
          setoid_rewrite lookup_insert_ne; [|done..].
Hai Dang's avatar
Hai Dang committed
766
          destruct Lk; by subst k.
Hai Dang's avatar
Hai Dang committed
767

Hai Dang's avatar
Hai Dang committed
768
      + have HL': (r_f  r).(rtm) !! t1  Some (to_tgkR k1, h1).
Hai Dang's avatar
Hai Dang committed
769
        { rewrite Eqr cmra_assoc. move: HL1.
Hai Dang's avatar
Hai Dang committed
770 771
          rewrite lookup_op res_tag_lookup_ne //.
          rewrite (lookup_op _ (res_tag _ _ _).(rtm)) res_tag_lookup_ne //. }
Hai Dang's avatar
Hai Dang committed
772
        specialize (PINV _ _ _ HL') as [? PINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
773
        intros l1 ss1 st1 Eqs1. specialize (PINV _ _ _ Eqs1).
Hai Dang's avatar
Hai Dang committed
774
        case (decide (l1 = l)) => [?|NEQ];
Hai Dang's avatar
Hai Dang committed
775
          [subst l1; rewrite lookup_insert|rewrite lookup_insert_ne //].
Hai Dang's avatar
Hai Dang committed
776 777
        * intros PRE.
          destruct PINV as [Eqs' [? HD]]. { by destruct k1. }
Hai Dang's avatar
Hai Dang committed
778 779 780
          (* t1  t, t is top of stack(l), t1 is top or SRO in stack (l).
            This cannot happen. *)
          exfalso.
Hai Dang's avatar
Hai Dang committed
781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800
          have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
          destruct k1; simpl in *.
          { rewrite Eqstk in HD. simplify_eq.
            eapply (access1_write_remove_incompatible_head _ (Tagged t) t1 _ _ _ ND);
              eauto.
            - by exists None, [].
            - by inversion 1.
            - by left. }
          { destruct HD as (stk1 & Eqstk1 & opro & HD).
            rewrite Eqstk1 in Eqstk. simplify_eq.
            eapply (access1_write_remove_incompatible_head _ (Tagged t) t1 _ _ _ ND);
              eauto.
            - by inversion 1.
            - destruct HD as [? HD]. rewrite HD. by left. }
          { destruct HD as (stk1 & Eqstk1 & HD).
            rewrite Eqstk1 in Eqstk. simplify_eq.
            destruct PRE as (stk1 & pm & opro & Eqstk & In1 & ?).
            rewrite Eqstk in Eqstk1. simplify_eq.
            eapply (access1_write_remove_incompatible_active_SRO _
                      (Tagged t) t1 _ _ _ ND); eauto. }
Hai Dang's avatar
Hai Dang committed
801

802
        * setoid_rewrite lookup_insert_ne; [|done]. by apply PINV.
Hai Dang's avatar
Hai Dang committed
803 804

    (* cmap_inv *)
Hai Dang's avatar
Hai Dang committed
805 806 807 808
    - intros c Ts. rewrite -EQrcm. intros Eqcm.
      move : CINV. rewrite Eqr cmra_assoc => CINV.
      specialize (CINV _ _ Eqcm) as [Inc CINV]. split; [done|].
      intros t1 L Int. by specialize (CINV _ _ Int) as [Ltt CINV].
Hai Dang's avatar
Hai Dang committed
809 810

    (* srel *)
Hai Dang's avatar
Hai Dang committed
811 812 813
    - destruct SREL as (?&?&?&?& REL). do 4 (split; [done|]).
      simpl. intros l1 Inl1.
      case (decide (l1 = l)) => ?; [subst l1|].
Hai Dang's avatar
Hai Dang committed
814
      + destruct CASE as [[]|[? AREL]]; subst k.
Hai Dang's avatar
Hai Dang committed
815
        * (* Local => Private *)
Hai Dang's avatar
Hai Dang committed
816 817 818 819
          right. eexists t, _, _. split; last split.
          { by rewrite HLtr'. }
          { rewrite lookup_fmap lookup_insert. by eexists. }
          { by left. }
Hai Dang's avatar
Hai Dang committed
820 821
        * (* Unique => Public *)
          left. intros st1. simpl. rewrite lookup_insert.
822
          intros Eq. symmetry in Eq. simplify_eq. exists st.
Hai Dang's avatar
Hai Dang committed
823 824
          rewrite lookup_insert. split; [done|].
          eapply arel_mono; [apply VALID'|..|exact AREL].
Hai Dang's avatar
Hai Dang committed
825
          etrans; [apply cmra_included_r|].
Hai Dang's avatar
Hai Dang committed
826
          apply cmra_included_l.
Hai Dang's avatar
Hai Dang committed
827 828
      + move : Inl1. rewrite dom_insert elem_of_union elem_of_singleton.
        intros [?|Inl1]; [done|].
Hai Dang's avatar
Hai Dang committed
829 830
        specialize (REL _ Inl1) as [PB|[t1 PV]]; [left|right].
        * move : PB.
Hai Dang's avatar
Hai Dang committed
831
          rewrite Eqr cmra_assoc /pub_loc /= lookup_insert_ne; [|done].
Hai Dang's avatar
Hai Dang committed
832 833
          intros PB st1 Eqst. specialize (PB _ Eqst) as (ss1 & Eqss & AREL).
          exists ss1. split; [by rewrite lookup_insert_ne|].
Hai Dang's avatar
Hai Dang committed
834 835 836
          move : AREL. by apply arel_res_tag_overwrite.
        * exists t1. move : PV. rewrite Eqr cmra_assoc /priv_loc.
          intros (k' & h & Eqh & InL& PV).
Hai Dang's avatar
Hai Dang committed
837
          case (decide (t1 = t)) => ?; [subst t|].
Hai Dang's avatar
Hai Dang committed
838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854
          { exists k. eexists. rewrite HLtr'. split; [eauto|].
            move : HLtrf. rewrite Eqr cmra_assoc. rewrite Eqh.
            intros [Eqk'%leibniz_equiv_iff Eqh']%Some_equiv_inj.
            simpl in Eqk', Eqh'.
            have ?: k' = k. { destruct k', k; inversion Eqk'; done. }
            subst k'. clear Eqk'.
            split.
            { rewrite lookup_fmap lookup_insert_ne //.
              destruct InL as [? InL]. move : (Eqh' l1).
              rewrite InL lookup_fmap.
              destruct (h0 !! l1) eqn:Eq0; rewrite Eq0;
                [by eexists|by inversion 1]. }
            destruct PV as [|(? & c & Tc & L & PV & ? & Inh)]; [by left|right].
            split; [done|].
            exists c, Tc, L. by rewrite -EQrcm. }
          { exists k', h. setoid_rewrite EQrcm.
            split; [|split; [done|destruct PV as [PB|PV]]].
Hai Dang's avatar
Hai Dang committed
855
            - move : Eqh.
Hai Dang's avatar
Hai Dang committed
856 857 858
              rewrite lookup_op res_tag_lookup_ne; [|done].
              rewrite (lookup_op _ (res_tag _ _ _).(rtm)) res_tag_lookup_ne //.
            - left. move : PB. done.
Hai Dang's avatar
Hai Dang committed
859
            - by right. }
Hai Dang's avatar
Hai Dang committed
860
  }
Hai Dang's avatar
Hai Dang committed
861 862

  left. apply: sim_body_result.
Hai Dang's avatar
Hai Dang committed
863
  intros. simpl. by apply POST.
Hai Dang's avatar
Hai Dang committed
864
Qed.
865

Hai Dang's avatar
Hai Dang committed
866
(** Writing to local of size 1 *)
Hai Dang's avatar
Hai Dang committed
867
Lemma sim_body_write_local_1 fs ft r r' n l tg T v v' σs σt Φ :
Hai Dang's avatar
Hai Dang committed
868
  tsize T = 1%nat 
Hai Dang's avatar
Hai Dang committed
869
  r  r'  res_loc l [v'] tg 
Hai Dang's avatar
Hai Dang committed
870 871 872 873
  ( s, v = [s] 
    let σs' := mkState (<[l := s]> σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in
    let σt' := mkState (<[l := s]> σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in
    Φ (r'  res_loc l [(s,s)] tg) n
Hai Dang's avatar
Hai Dang committed
874 875
      (ValR [%S]) σs' (ValR [%S]) σt') 
  r {n,fs,ft}
Hai Dang's avatar
Hai Dang committed
876
    (Place l (Tagged tg) T <- #v, σs)  (Place l (Tagged tg) T <- #v, σt) : Φ.
Hai Dang's avatar
Hai Dang committed
877 878 879
Proof.
  intros LenT Eqr POST.
  eapply sim_body_write_unique_local_1; [done| |by left|..].
Hai Dang's avatar
Hai Dang committed
880
  - rewrite Eqr /res_loc; eauto.
Hai Dang's avatar
Hai Dang committed
881 882 883 884
  - rewrite lookup_insert. by eexists.
  - intros. rewrite insert_insert insert_empty. naive_solver.
Qed.

Hai Dang's avatar
Hai Dang committed
885
(** Writing to owned (unique) location *)
Hai Dang's avatar
Hai Dang committed
886 887
Lemma sim_body_write_unique_1
  fs ft (r r' r'' rs: resUR) n l h tg T s σs σt Φ:
Ralf Jung's avatar
Ralf Jung committed
888 889
  tsize T = 1%nat 
  r  r'  res_tag tg tkUnique h 
Ralf Jung's avatar
Ralf Jung committed
890
  is_Some (h !! l) 
Ralf Jung's avatar
Ralf Jung committed
891 892
  arel rs s s  (* assuming to-write values are related *)
  r'  r''  rs 
Hai Dang's avatar
Hai Dang committed
893 894 895
  (let σs' := mkState (write_mem l [s] σs.(shp)) σs.(sst) σs.(scs) σs.(snp) σs.(snc) in
   let σt' := mkState (write_mem l [s] σt.(shp)) σt.(sst) σt.(scs) σt.(snp) σt.(snc) in
    tag_on_top σt'.(sst) l tg 
Hai Dang's avatar
Hai Dang committed
896
    Φ (r'  res_tag tg tkUnique (<[l:=(s,s)]> h)) n (ValR []%S) σs' (ValR []%S) σt') 
Ralf Jung's avatar
Ralf Jung committed
897 898 899
  r {n,fs,ft}
    (Place l (Tagged tg) T <- #[s], σs)  (Place l (Tagged tg) T <- #[s], σt) : Φ.
Proof.