refl_step.v 62.5 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
2
From iris.algebra Require Import local_updates.

Hai Dang's avatar
Hai Dang committed
3
From stbor.lang Require Import steps_progress steps_inversion steps_retag.
Hai Dang's avatar
Hai Dang committed
4
From stbor.sim Require Export instance.
Hai Dang's avatar
Hai Dang committed
5
6
7

Set Default Proof Using "Type".

Hai Dang's avatar
Hai Dang committed
8
9
(** MEM STEP -----------------------------------------------------------------*)

Hai Dang's avatar
Hai Dang committed
10
11
12
13
14
15
16
17
18
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
19
  let r' : resUR := res_mapsto l ScPoison (init_stack t) in
Hai Dang's avatar
Hai Dang committed
20
21
22
23
  Φ (r  r') n (PlaceR l t T) σs' (PlaceR l t T) σt' : Prop 
  r {n,fs,ft} (Alloc T, σs)  (Alloc T, σt) : Φ.
Proof.
Admitted.
Hai Dang's avatar
Hai Dang committed
24
25

(** Alloc *)
Hai Dang's avatar
Hai Dang committed
26
(* 
Hai Dang's avatar
Hai Dang committed
27
Lemma sim_body_alloc_shared fs ft r n T σs σt Φ :
Hai Dang's avatar
Hai Dang committed
28
29
30
31
32
33
34
35
36
37
38
  let ls := (fresh_block σs.(shp), 0) in
  let lt := (fresh_block σt.(shp), 0) in
  let ts := (Tagged σs.(snp)) in
  let tgt := (Tagged σt.(snp)) in
  let σs' := mkState (init_mem ls (tsize T) σs.(shp))
                     (init_stacks σs.(sst) ls (tsize T) ts) σs.(scs)
                     (S σs.(snp)) σs.(snc) in
  let σt' := mkState (init_mem lt (tsize T) σt.(shp))
                     (init_stacks σt.(sst) lt (tsize T) tgt) σt.(scs)
                     (S σt.(snp)) σt.(snc) in
  let r' : resUR :=
Hai Dang's avatar
Hai Dang committed
39
40
    (({[σt.(snp) := (to_tagKindR tkUnique, to_heapletR $ init_mem lt (tsize T) )]},
        ε), ε) in
Hai Dang's avatar
Hai Dang committed
41
42
  (ls = lt  ts = tgt 
    Φ (r  r') n (PlaceR ls ts T) σs' (PlaceR lt tgt T) σt' : Prop) 
Hai Dang's avatar
Hai Dang committed
43
44
45
46
47
48
  r {n,fs,ft} (Alloc T, σs)  (Alloc T, σt) : Φ.
Proof.
  intros ls lt ts tgt σs' σt' r' POST.
  pfold. intros NT. intros.
  have EqDOM := wsat_heap_dom _ _ _ WSAT.
  have EqFRESH := fresh_block_equiv _ _ EqDOM.
Hai Dang's avatar
Hai Dang committed
49
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
Hai Dang's avatar
Hai Dang committed
50
  have Eqnp : σs.(snp) = σt.(snp). { by destruct SREL as (?&?&?&?). }
Hai Dang's avatar
Hai Dang committed
51
  have Eqlst: ls = lt. { by rewrite /ls /lt EqFRESH. }
Hai Dang's avatar
Hai Dang committed
52
53
54
55
56
57
58
59
60
61
  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 (fresh_block σs.(shp), 0) (Tagged σs.(snp)) T, σs').
  { subst ls σs' ts. eapply (head_step_fill_tstep _ []), alloc_head_step. }
  eexists _, σs', (r  r'), (S n). split; last split.
  { left. by apply tc_once. }
Hai Dang's avatar
Hai Dang committed
62
63
  { have HLF : (r_f  r).(rtm) !! σt.(snp) = None.
    { destruct ((r_f  r).(rtm) !! σt.(snp)) as [[k h]|] eqn:Eqkh; [|done]. exfalso.
Hai Dang's avatar
Hai Dang committed
64
65
66
      destruct (tagKindR_valid k) as [k' Eqk'].
      { apply (Some_valid (k,h)). rewrite -Some_valid -Eqkh. apply VALID. }
      destruct (PINV σt.(snp) k' h) as [Lt _]; [by rewrite Eqkh Eqk'|lia]. }
Hai Dang's avatar
Hai Dang committed
67
68
    have VALID':  (r_f  r  r').
    { apply (local_update_discrete_valid_frame _ ε r'); [by rewrite right_id|].
Hai Dang's avatar
Hai Dang committed
69
70
      do 2 apply prod_local_update_1. rewrite /= right_id.
      rewrite -(cmra_comm _ (r_f.(rtm)  r.(rtm))) -insert_singleton_op //.
Hai Dang's avatar
Hai Dang committed
71
72
73
74
      apply alloc_singleton_local_update; [done|]. split; [done|].
      by apply to_heapletR_valid. }
    have INCL: r_f  r  r_f  r  r' by apply cmra_included_l.
    rewrite cmra_assoc.
Hai Dang's avatar
Hai Dang committed
75
76
77
    destruct (init_mem_lookup ls (tsize T) σs.(shp)) as [HLs1 HLs2].
    destruct (init_mem_lookup lt (tsize T) σt.(shp)) as [HLt1 HLt2].
    split; last split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
78
79
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
Hai Dang's avatar
Hai Dang committed
80
    - done.
Hai Dang's avatar
Hai Dang committed
81
82
83
84
85
86
    - intros t k h. rewrite lookup_op.
      case (decide (t = σt.(snp))) => ?; [subst t|].
      + rewrite /= lookup_insert HLF left_id.
        intros [Eq1 Eq2]%Some_equiv_inj. simpl in Eq1, Eq2. split; [lia|].
        intros l s. rewrite -Eq2. intros Eqs stk Eqstk pm opro Instk NDIS.
        (* l is new memory *)
Hai Dang's avatar
Hai Dang committed
87
88
89
90
91
92
93
94
        apply to_heapletR_lookup in Eqs.
        destruct (init_mem_lookup_empty _ _ _ _ Eqs) as [i [[? Lti] Eql]].
        have Eqi: Z.of_nat (Z.to_nat i) = i by rewrite Z2Nat.id.
        have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Eqi.
        have ?: s = ScPoison.
        { rewrite Eql -Eqi in Eqs.
          rewrite (proj1 (init_mem_lookup lt (tsize T) )) // in Eqs.
          by inversion Eqs. } subst s.
Hai Dang's avatar
Hai Dang committed
95
        have Eqs2 := HLt1 _ Lti'. rewrite Eqi -Eql in Eqs2. split; [done|].
Hai Dang's avatar
Hai Dang committed
96
97
98
99
100
        destruct k; [|by inversion Eq1].
        have Eqstk2 := proj1 (init_stacks_lookup σt.(sst) lt (tsize T) tgt) _ Lti'.
        rewrite Eqi -Eql Eqstk in Eqstk2.
        exists []. move : Instk. inversion Eqstk2.
        rewrite elem_of_list_singleton. by inversion 1.
Hai Dang's avatar
Hai Dang committed
101
102
103
104
105
      + rewrite lookup_insert_ne // right_id. intros Eqkh.
        specialize (PINV t k h Eqkh) as [Lt PINV].
        split. { etrans; [exact Lt|simpl; lia]. }
        intros l s Eqs stk Eqstk pm opro Instk NDIS.
        specialize (PINV l s Eqs).
Hai Dang's avatar
Hai Dang committed
106
        destruct (init_stacks_lookup_case _ _ _ _ _ _ Eqstk)
Hai Dang's avatar
Hai Dang committed
107
108
          as [[EqstkO Lti]|[i [[? Lti] Eql]]].
        * specialize (PINV _ EqstkO _ _ Instk NDIS) as [Eqss PINV].
Hai Dang's avatar
Hai Dang committed
109
          rewrite /= HLt2 //.
Hai Dang's avatar
Hai Dang committed
110
        * exfalso. move : Eqstk. simpl.
Hai Dang's avatar
Hai Dang committed
111
          destruct (init_stacks_lookup σt.(sst) lt (tsize T) tgt) as [EQ _].
Hai Dang's avatar
Hai Dang committed
112
113
114
115
          have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id //.
          specialize (EQ _ Lti'). rewrite Z2Nat.id // in EQ. rewrite Eql EQ.
          intros. inversion Eqstk. clear Eqstk. subst stk.
          move : Instk. rewrite elem_of_list_singleton. by inversion 1.
Hai Dang's avatar
Hai Dang committed
116
    - intros c cs. rewrite /rcm /= right_id => /CINV.
Hai Dang's avatar
Hai Dang committed
117
118
      destruct cs as [[T0|]| |]; [|done..]. intros [InT Eqh].
      split; [done|]. intros t2 InT2. specialize (Eqh t2 InT2) as [Lt2 Eqh].
Hai Dang's avatar
Hai Dang committed
119
      split; [lia|]. intros k2 h2. rewrite lookup_op.
Hai Dang's avatar
Hai Dang committed
120
121
122
123
      case (decide (t2 = σt.(snp))) => ?; [subst t2|]; [exfalso; by lia|].
      rewrite lookup_insert_ne // right_id.
      intros Eqh2 l Inl.
      specialize (Eqh _ _ Eqh2 l Inl) as (stk & pm & Eqsk & Instk).
Hai Dang's avatar
Hai Dang committed
124
      destruct (init_stacks_lookup_case_2 _ lt (tsize T) tgt _ _ Eqsk)
Hai Dang's avatar
Hai Dang committed
125
126
127
128
129
130
        as [[EqO NIn]|[i [[? Lti] [Eqi EqN]]]].
      + exists stk, pm. by rewrite EqO.
      + exfalso. apply (is_fresh_block σt.(shp) i).
        rewrite (state_wf_dom _ WFT). apply elem_of_dom. exists stk.
        rewrite (_: (fresh_block (shp σt), i) = lt + i) //.
        by rewrite -Eqi.
Hai Dang's avatar
Hai Dang committed
131
    - destruct SREL as (Eqst&_&Eqcs&Eqnc&VREL).
Hai Dang's avatar
Hai Dang committed
132
133
      repeat split; simpl; [|auto..|].
      { subst σs' σt' ls lt ts tgt. by rewrite Eqst EqFRESH Eqnp. }
Hai Dang's avatar
Hai Dang committed
134
      intros l st HL.
Hai Dang's avatar
Hai Dang committed
135
136
137
138
139
140
141
142
143
144
      destruct (init_mem_lookup_case _ _ _ _ _ HL) as [[EqO NIn]|[i [[? Lti] Eqi]]].
      + rewrite -Eqlst in NIn. rewrite (HLs2 _ NIn).
        specialize (VREL _ _ EqO) as [[ss [? AREL]]|[t PV]].
        * left. exists ss. split; [done|]. move : AREL. by apply arel_mono.
        * right. exists t. move : PV. by apply priv_loc_mono.
      + left. exists %S.
        have Lti': (Z.to_nat i < tsize T)%nat by rewrite Nat2Z.inj_lt Z2Nat.id //.
        specialize (HLt1 _ Lti').
        rewrite Z2Nat.id // -Eqi HL in HLt1.
        specialize (HLs1 _ Lti'). rewrite -Eqlst in Eqi.
Hai Dang's avatar
Hai Dang committed
145
146
147
148
149
150
151
152
        rewrite Z2Nat.id // -Eqi in HLs1. split; [done|by inversion HLt1].
    - intros ???. rewrite /lmap_inv /= right_id. intros IN.
      specialize (LINV _ _ _ IN) as [Eq1 Eq2].
      have ?:  i : nat, (i < tsize T)%nat  l  lt + i.
      { intros i Lt Eq. apply (is_fresh_block σt.(shp) i), elem_of_dom.
        exists s. rewrite (_ : (fresh_block σt.(shp), Z.of_nat i) = l) //. }
      rewrite HLt2 // HLs2 // Eqlst //. }
  left.
Hai Dang's avatar
Hai Dang committed
153
  apply (sim_body_result _ _ _ _ (PlaceR _ _ T) (PlaceR _ _ T)). intros.
Hai Dang's avatar
Hai Dang committed
154
  apply POST; eauto. by rewrite /ts Eqnp.
Hai Dang's avatar
Hai Dang committed
155
Qed. *)
Hai Dang's avatar
Hai Dang committed
156

Hai Dang's avatar
Hai Dang committed
157
(** Copy *)
Hai Dang's avatar
Hai Dang committed
158
159
Lemma sim_body_copy_public fs ft r n l t Ts Tt σs σt Φ
  (EQS: tsize Ts = tsize Tt)
Hai Dang's avatar
Hai Dang committed
160
161
  (PUBLIC:  (h: heapletR), r.(rtm) !! t  Some (to_tagKindR tkPub, h))
  (SHR:  i, (i < tsize Tt)%nat  r.(rlm) !! (l + i)  Some $ to_locStateR lsShared) :
Hai Dang's avatar
Hai Dang committed
162
  ( vs vt r',
Hai Dang's avatar
Hai Dang committed
163
164
165
166
167
    read_mem l (tsize Ts) σs.(shp) = Some vs 
    read_mem l (tsize Tt) σt.(shp) = Some vt 
     α', memory_read σt.(sst) σt.(scs) l (Tagged t) (tsize Tt) = Some α' 
      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
168
      vrel (r  r') vs vt  Φ (r  r') n (ValR vs) σs' (ValR vt) σt' : Prop) 
Hai Dang's avatar
Hai Dang committed
169
170
  r {n,fs,ft} (Copy (Place l (Tagged t) Ts), σs)  (Copy (Place l (Tagged t) Tt), σt) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
171
172
  intros POST. pfold.
  intros NT. intros.
Hai Dang's avatar
Hai Dang committed
173
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
Hai Dang's avatar
Hai Dang committed
174
175
  split; [|done|].
  { right.
Hai Dang's avatar
Hai Dang committed
176
177
    destruct (NT (Copy (Place l (Tagged t) Ts)) σs) as [[]|[es' [σs' STEPS]]];
      [done..|].
Hai Dang's avatar
Hai Dang committed
178
    destruct (tstep_copy_inv _ _ _ _ _ _ _ STEPS)
Hai Dang's avatar
Hai Dang committed
179
      as (vs & α' & ? & Eqvs & Eqα' & ?). subst es'.
Hai Dang's avatar
Hai Dang committed
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
    destruct (read_mem_is_Some l (tsize Tt) σt.(shp)) as [vt Eqvt].
    { intros m. rewrite (srel_heap_dom _ _ _ WFS WFT SREL) -EQS.
      apply (read_mem_is_Some' l (tsize Ts) σs.(shp)). by eexists. }
    have Eqα'2: memory_read σt.(sst) σt.(scs) l (Tagged t)  (tsize Tt) = Some α'.
    { destruct SREL as (Eqst&?&Eqcs&?). by rewrite -Eqst -Eqcs -EQS. }
    exists (#vt)%E, (mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc)).
    by eapply (head_step_fill_tstep _ []), copy_head_step'. }
  constructor 1. intros.
  destruct (tstep_copy_inv _ _ _ _ _ _ _ STEPT) as (vt & α' & ? & Eqvt & Eqα' & ?).
  subst et'.
  destruct (read_mem_is_Some l (tsize Ts) σs.(shp)) as [vs Eqvs].
  { intros m. rewrite -(srel_heap_dom _ _ _ WFS WFT SREL) EQS.
    apply (read_mem_is_Some' l (tsize Tt) σt.(shp)). by eexists. }
  have Eqα'2: memory_read σs.(sst) σs.(scs) l (Tagged t)  (tsize Ts) = Some α'.
  { destruct SREL as (Eqst&?&Eqcs&?). by rewrite Eqst Eqcs EQS. }
  set σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc).
  have STEPS: (Copy (Place l (Tagged t)  Ts), σs) ~{fs}~> ((#vs)%E, σs').
  { by eapply (head_step_fill_tstep _ []), copy_head_step'. }
  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).
  { destruct PUBLIC as [h PUB].
Hai Dang's avatar
Hai Dang committed
201
    destruct (tmap_lookup_op_r_equiv_pub r_f.(rtm) r.(rtm) t h) as [h0 Eqh0];
Hai Dang's avatar
Hai Dang committed
202
203
204
205
206
      [apply VALID|done|].
    destruct (PINV _ _ _ Eqh0) as [Lt PB].
    destruct SREL as (Eqst & Eqnp & Eqcs & Eqnc & PRIV).
    destruct (read_mem_values _ _ _ _ Eqvs) as [Eqls HLs].
    destruct (read_mem_values _ _ _ _ Eqvt) as [Eqlt HLt].
Hai Dang's avatar
Hai Dang committed
207
    apply Forall2_same_length_lookup. split; [by rewrite Eqls Eqlt|].
Hai Dang's avatar
Hai Dang committed
208
209
210
211
    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
212
213
214
215
216
217
    rewrite -Eqlt in SHR.
    have SHR' := lmap_lookup_op_r _ _ (proj2 VALID) _ _ (SHR _ HLLt).
    specialize (PRIV _ (elem_of_dom_2 _ _ _ HLt) SHR')
      as [PUBl|[t' PV]].
    { destruct (PUBl _ HLt) as [ss' [Eqss' AREL]].
      rewrite HLs in Eqss'. symmetry in Eqss'. simplify_eq. move: AREL.
Hai Dang's avatar
Hai Dang committed
218
219
      destruct ss as [| |l1 [t1|]|], st as [| |l2 [t2|]|]; auto; simpl; [|by intros [?[]]].
      intros [? [? [h' Eqh']]]. simplify_eq. do 2 (split; [done|]).
Hai Dang's avatar
Hai Dang committed
220
      exists h'. by apply tmap_lookup_core_pub. }
Hai Dang's avatar
Hai Dang committed
221
    destruct PV as (c' & T' & h' & Eqci & InT' & Eqh' & Inl).
Hai Dang's avatar
Hai Dang committed
222
223
224
     (* impossible: t' is protected by c' which is still active.
      So t  t' and protected(t',c') is on top of (l + i), so access with t is UB *)
    exfalso.
Hai Dang's avatar
Hai Dang committed
225
226
    have NEQ: t'  t.
    { intros ?. subst t'.
Hai Dang's avatar
Hai Dang committed
227
      apply (tmap_lookup_op_r_equiv_pub r_f.(rtm)) in PUB as [? PUB];
Hai Dang's avatar
Hai Dang committed
228
229
230
        [|by apply VALID].
      rewrite -> PUB in Eqh'. apply Some_equiv_inj in Eqh' as [Eqk' ?].
      inversion Eqk'. }
Hai Dang's avatar
Hai Dang committed
231
232
    specialize (CINV _ _ Eqci) as [Inc' CINV].
    specialize (CINV _ InT') as [Ltt' CINV].
Hai Dang's avatar
Hai Dang committed
233
    specialize (CINV _ _ Eqh' _ Inl) as (stk & pm & Eqstk & Instk & NDIS).
Hai Dang's avatar
Hai Dang committed
234
    specialize (PINV _ _ _ Eqh') as [_ PINV].
Hai Dang's avatar
Hai Dang committed
235
236
237
238
    have VALh' :  h'.
    { apply (Some_valid (to_tagKindR tkUnique,h')).
      rewrite -Some_valid -Eqh'. apply VALID. }
    destruct (heapletR_elem_of_dom _ _ VALh' Inl) as [s Eqs].
Hai Dang's avatar
Hai Dang committed
239
240
    specialize (PINV _ _ Eqs) as [_ PINV].
    specialize (PINV _ Eqstk _ _ Instk NDIS) as (Eqss & HD).
Hai Dang's avatar
Hai Dang committed
241
242
243
244
245
246
    destruct (for_each_lookup _ _ _ _ _ Eqα') as [EQ1 _].
    rewrite Eqlt in HLLt.
    specialize (EQ1 _ _ HLLt Eqstk) as (stk' & Eqstk' & EQ2).
    move : EQ2. case access1 as [[n1 stk1]|] eqn:EQ3; [|done].
    simpl. inversion 1. subst stk1.
    have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
Hai Dang's avatar
Hai Dang committed
247
248
249
250
251
    admit.
  }
  exists (Val vs), σs', (r  (core (r_f  r))), (S n). split; last split.
  { left. by constructor 1. }
  { rewrite cmra_assoc -CORE.
Hai Dang's avatar
Hai Dang committed
252
    split; last split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
253
254
255
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
Hai Dang's avatar
Hai Dang committed
256
257
258
259
    - intros t1 k h Eqt. specialize (PINV t1 k h Eqt) as [Lt PI]. subst σt'. simpl.
      split; [done|]. intros l' s' Eqk'.
      specialize (PI _ _ Eqk') as [? PI]. split; [done|].
      intros stk' Eqstk'.
Hai Dang's avatar
Hai Dang committed
260
261
262
263
      destruct (for_each_access1 _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
        as (stk & Eqstk & SUB & ?).
      intros pm opro In' NDIS.
      destruct (SUB _ In') as (it2 & In2 & Eqt2 & Eqp2 & NDIS2).
Hai Dang's avatar
Hai Dang committed
264
      specialize (PI _ Eqstk it2.(perm) opro) as [Eql' HTOP].
Hai Dang's avatar
Hai Dang committed
265
266
267
268
269
270
271
272
273
274
275
276
277
278
      { simpl in *. rewrite /= Eqt2 Eqp2. by destruct it2. }
      { simpl in *. by rewrite (NDIS2 NDIS). }
      split; [done|].
      destruct (for_each_lookup_case _ _ _ _ _ Eqα' _ _ _ Eqstk Eqstk')
        as [?|[MR _]]; [by subst|]. clear -In' MR HTOP Eqstk WFT NDIS.
      destruct (access1 stk AccessRead (Tagged t) σt.(scs)) as [[n stk1]|] eqn:Eqstk';
        [|done]. simpl in MR. simplify_eq.
      destruct (state_wf_stack_item _ WFT _ _ Eqstk). move : Eqstk' HTOP.
      destruct k.
      + eapply access1_head_preserving; eauto.
      + eapply access1_active_SRO_preserving; eauto.
    - intros c cs Eqc. specialize (CINV _ _ Eqc). subst σt'. simpl.
      clear -Eqα' CINV. destruct cs as [[T|]| |]; [|done..].
      destruct CINV as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
279
280
      intros t1 InT. specialize (CINV _ InT) as [? CINV]. split; [done|].
      intros k h Eqt l' Inh.
Hai Dang's avatar
Hai Dang committed
281
      destruct (CINV _ _ Eqt _ Inh) as (stk' & pm' & Eqstk' & Instk' & NDIS).
Hai Dang's avatar
Hai Dang committed
282
283
      destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
        as [stk [Eqstk AS]].
Hai Dang's avatar
Hai Dang committed
284
      exists stk, pm'. split; last split; [done| |done]. by apply AS.
Hai Dang's avatar
Hai Dang committed
285
286
    - subst σt'. rewrite /srel /=. by destruct SREL as (?&?&?&?&?).
    - intros ??? IN. specialize (LINV _ _ _ IN) as [Eq1 Eq2]. by subst σt'. }
Hai Dang's avatar
Hai Dang committed
287
288
289
290
291
  left.
  apply (sim_body_result _ _ _ _ (ValR vs) (ValR vt)). intros.
  have VREL2: vrel (r  (core (r_f  r))) vs vt.
  { eapply vrel_mono; [done| |exact VREL']. apply cmra_included_r. }
  subst σt'. apply POST; eauto.
Hai Dang's avatar
Hai Dang committed
292
293
Abort.

Hai Dang's avatar
Hai Dang committed
294
Lemma sim_body_copy_raw fs ft r n l tg Ts Tt σs σt Φ
Hai Dang's avatar
Hai Dang committed
295
296
297
298
299
300
301
302
  (EQS: tsize Ts = tsize Tt) :
  ( vs vt,
    read_mem l (tsize Ts) σs.(shp) = Some vs 
    read_mem l (tsize Tt) σt.(shp) = Some vt 
     α', memory_read σt.(sst) σt.(scs) l tg (tsize Tt) = Some α' 
      let σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc) in
      let σt' := mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc) in
      Φ r n (ValR vs) σs' (ValR vt) σt' : Prop) 
Hai Dang's avatar
Hai Dang committed
303
  r {n,fs,ft} (Copy (Place l tg Ts), σs)  (Copy (Place l tg Tt), σt) : Φ.
Hai Dang's avatar
Hai Dang committed
304
305
Proof.
  intros POST. pfold.
Hai Dang's avatar
Hai Dang committed
306
  intros NT. intros.
Hai Dang's avatar
Hai Dang committed
307
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
Hai Dang's avatar
Hai Dang committed
308
309
310
311
312
313
314
315
316
317
318
319
320
  split; [|done|].
  { right.
    destruct (NT (Copy (Place l tg Ts)) σs) as [[]|[es' [σs' STEPS]]]; [done..|].
    destruct (tstep_copy_inv _ _ _ _ _ _ _ STEPS)
      as (vs & α' & ? & Eqvs & Eqα' & ?).
    subst es'.
    destruct (read_mem_is_Some l (tsize Tt) σt.(shp)) as [vt Eqvt].
    { intros m. rewrite (srel_heap_dom _ _ _ WFS WFT SREL) -EQS.
      apply (read_mem_is_Some' l (tsize Ts) σs.(shp)). by eexists. }
    have Eqα'2: memory_read σt.(sst) σt.(scs) l tg (tsize Tt) = Some α'.
    { destruct SREL as (Eqst&?&Eqcs&?). by rewrite -Eqst -Eqcs -EQS. }
    exists (#vt)%E, (mkState σt.(shp) α' σt.(scs) σt.(snp) σt.(snc)).
    by eapply (head_step_fill_tstep _ []), copy_head_step'. }
Hai Dang's avatar
Hai Dang committed
321
  constructor 1. intros.
Hai Dang's avatar
Hai Dang committed
322
323
324
325
326
327
328
329
330
331
332
333
  destruct (tstep_copy_inv _ _ _ _ _ _ _ STEPT) as (vt & α' & ? & Eqvt & Eqα' & ?).
  subst et'.
  destruct (read_mem_is_Some l (tsize Ts) σs.(shp)) as [vs Eqvs].
  { intros m. rewrite -(srel_heap_dom _ _ _ WFS WFT SREL) EQS.
    apply (read_mem_is_Some' l (tsize Tt) σt.(shp)). by eexists. }
  have Eqα'2: memory_read σs.(sst) σs.(scs) l tg (tsize Ts) = Some α'.
  { destruct SREL as (Eqst&?&Eqcs&?). by rewrite Eqst Eqcs EQS. }
  set σs' := mkState σs.(shp) α' σs.(scs) σs.(snp) σs.(snc).
  have STEPS: (Copy (Place l tg Ts), σs) ~{fs}~> ((#vs)%E, σs').
  { by eapply (head_step_fill_tstep _ []), copy_head_step'. }
  exists (Val vs), σs', r, (S n). split; last split.
  { left. by constructor 1. }
Hai Dang's avatar
Hai Dang committed
334
  { split; last split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
335
336
337
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
    - done.
Hai Dang's avatar
Hai Dang committed
338
339
340
    - intros t k h Eqt. specialize (PINV t k h Eqt) as [Lt PI]. subst σt'. simpl.
      split; [done|]. intros l' s' Eqk'. specialize (PI _ _ Eqk') as [? PI].
      split; [done|]. intros stk' Eqstk'.
Hai Dang's avatar
Hai Dang committed
341
342
      destruct (for_each_access1 _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
        as (stk & Eqstk & SUB & ?).
343
344
      intros pm opro In' NDIS.
      destruct (SUB _ In') as (it2 & In2 & Eqt2 & Eqp2 & NDIS2).
Hai Dang's avatar
Hai Dang committed
345
      destruct (PI _ Eqstk it2.(perm) opro) as [Eql' HTOP].
Hai Dang's avatar
Hai Dang committed
346
      { simpl in *. rewrite /= Eqt2 Eqp2. by destruct it2. }
347
      { simpl in *. by rewrite (NDIS2 NDIS). }
Hai Dang's avatar
Hai Dang committed
348
349
      split; [done|].
      destruct (for_each_lookup_case _ _ _ _ _ Eqα' _ _ _ Eqstk Eqstk')
350
        as [?|[MR _]]; [by subst|]. clear -In' MR HTOP Eqstk WFT NDIS.
Hai Dang's avatar
Hai Dang committed
351
352
      destruct (access1 stk AccessRead tg σt.(scs)) as [[n stk1]|] eqn:Eqstk';
        [|done]. simpl in MR. simplify_eq.
Hai Dang's avatar
Hai Dang committed
353
      destruct (state_wf_stack_item _ WFT _ _ Eqstk). move : Eqstk' HTOP.
Hai Dang's avatar
Hai Dang committed
354
      destruct k.
Hai Dang's avatar
Hai Dang committed
355
356
      + eapply access1_head_preserving; eauto.
      + eapply access1_active_SRO_preserving; eauto.
Hai Dang's avatar
Hai Dang committed
357
358
359
    - intros c cs Eqc. specialize (CINV _ _ Eqc). subst σt'. simpl.
      clear -Eqα' CINV. destruct cs as [[T|]| |]; [|done..].
      destruct CINV as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
360
361
      intros t InT. specialize (CINV _ InT) as [? CINV]. split; [done|].
      intros k h Eqt l' Inh.
Hai Dang's avatar
Hai Dang committed
362
      destruct (CINV _ _ Eqt _ Inh) as (stk' & pm' & Eqstk' & Instk' & NDIS).
Hai Dang's avatar
Hai Dang committed
363
364
      destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
        as [stk [Eqstk AS]].
Hai Dang's avatar
Hai Dang committed
365
      exists stk, pm'. split; last split; [done| |done]. by apply AS.
Hai Dang's avatar
Hai Dang committed
366
367
    - subst σt'. rewrite /srel /=. by destruct SREL as (?&?&?&?&?).
    - intros ??? IN. specialize (LINV _ _ _ IN) as [Eq1 Eq2]. by subst σt'. }
Hai Dang's avatar
Hai Dang committed
368
369
370
  left. pfold. split; last first.
  { constructor 1. intros vt' ? STEPT'. exfalso.
    have ?: to_result (Val vt) = None.
Hai Dang's avatar
Hai Dang committed
371
372
373
374
375
376
377
378
379
    { eapply (tstep_reducible_not_result ft _ σt'); eauto. by do 2 eexists. }
    done. }
  { move => ? /= Eqvt'. symmetry in Eqvt'. simplify_eq.
    exists (ValR vs), σs', r, n. split; last split.
    - right. split; [lia|]. eauto.
    - eauto.
    - by apply POST. }
  { left. by eexists. }
Qed.
Hai Dang's avatar
Hai Dang committed
380

Hai Dang's avatar
Hai Dang committed
381
(** Write *)
Hai Dang's avatar
Hai Dang committed
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
Fixpoint write_heaplet (l: loc) (v: value) (h: gmapR loc (agreeR scalarC)) :=
  match v with
  | [] => h
  | s :: v =>
      write_heaplet (l + 1) v (if h !! l then <[l := to_agree s]> h else h)
  end.

(* TODO: move *)
Instance insert_gmap_proper `{Countable K} {A : cmraT} (i: K) :
  Proper (() ==> () ==> ()) (insert (M:=gmap K A) i).
Proof.
  intros m1 m2 Eq a1 a2 Eqa i'. case (decide (i = i')) => [->|?].
  - by rewrite 2!lookup_insert Eq.
  - do 2 (rewrite lookup_insert_ne //).
Qed.

Instance write_heaplet_proper (l: loc) (v: value) :
  Proper (() ==> ()) (write_heaplet l v).
Proof.
  intros h1 h2 Eq. revert l h1 h2 Eq.
  induction v as [|s v IH]; intros l h1 h2 Eq; simpl; [done|].
  apply IH. move : (Eq l).
  destruct (h1 !! l) as [s1|] eqn:Eq1, (h2 !! l) as [s2|] eqn:Eq2; [..|done];
    rewrite Eq1 Eq2; intros Eql; [by rewrite Eq|by inversion Eql..].
Qed.

Lemma write_heaplet_dom (l: loc) (v: value) h :
  dom (gset loc) (write_heaplet l v h)  dom (gset loc) h.
Proof.
  revert l h.
  induction v as [|s v IH]; intros l h; simpl; [done|].
  rewrite IH. destruct (h !! l) eqn:Eq; [|done].
  rewrite dom_map_insert_is_Some //. by eexists.
Qed.

Hai Dang's avatar
Hai Dang committed
417
418
419
420
421
Lemma write_heaplet_empty l v : write_heaplet l v   .
Proof. revert l. induction v as [|?? IH]; [done|]; intros l. apply IH. Qed.

Lemma write_heaplet_valid l v h:
   h   (write_heaplet l v h).
Hai Dang's avatar
Hai Dang committed
422
Proof.
Hai Dang's avatar
Hai Dang committed
423
424
425
  revert l h. induction v as [|s v IH]; intros l h VALID; simpl; [done|].
  apply IH. destruct (h !! l) eqn:Eql; [|done]. by apply insert_valid.
Qed.
Hai Dang's avatar
Hai Dang committed
426

Hai Dang's avatar
Hai Dang committed
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
Lemma write_heaplet_lookup (l: loc) (vl: value) (h: heapletR) :
  ( (i: nat) s, (i < length vl)%nat 
    write_heaplet l vl h !! (l + i)  Some s 
    Some s  to_agree <$> vl !! i) 
  ( (l': loc), ( (i: nat), (i < length vl)%nat  l'  l + i) 
    write_heaplet l vl h !! l'  h !! l').
Proof.
  revert l h. induction vl as [|v vl IH]; move => l h; simpl;
    [split; [intros; by lia|done]|].
  destruct (IH (l + 1) (if h !! l then <[l:=to_agree v]> h else h)) as [IH1 IH2].
  split.
  - intros i s Lt. destruct i as [|i].
    + rewrite shift_loc_0_nat /=. rewrite IH2; [|].
      * destruct (h !! l) eqn:Eql; [by rewrite lookup_insert|].
        rewrite Eql; by inversion 1.
      * move => ? _.
        rewrite shift_loc_assoc -{1}(shift_loc_0 l) => /shift_loc_inj ?. by lia.
    + intros Eq.  rewrite /= -IH1; [eauto|lia|].
      by rewrite shift_loc_assoc -(Nat2Z.inj_add 1).
  - intros l' Lt. rewrite IH2.
    + destruct (h !! l) eqn:Eql; [|done].
      rewrite lookup_insert_ne; [done|].
      move => ?. subst l'. apply (Lt O); [lia|by rewrite shift_loc_0_nat].
    + move => i Lti. rewrite shift_loc_assoc -(Nat2Z.inj_add 1).
      apply Lt. by lia.
Qed.

Lemma sim_body_write_related_values
  fs ft (r: resUR) k0 h0 n l tg Ts Tt v σs σt Φ
Hai Dang's avatar
Hai Dang committed
456
  (EQS: tsize Ts = tsize Tt)
Hai Dang's avatar
Hai Dang committed
457
  (Eqtg: r.(rtm) !! tg = Some (to_tagKindR k0, h0))
Hai Dang's avatar
Hai Dang committed
458
459
  (SHR:  i, (i < tsize Tt)%nat  r.(rlm) !! (l + i)  Some $ to_locStateR lsShared)
  (* assuming to-write values are related *)
Hai Dang's avatar
Hai Dang committed
460
461
  (PUBWRITE:  s, s  v  arel r s s) :
  let r' := if k0 then
Hai Dang's avatar
Hai Dang committed
462
463
            ((<[tg := (to_tagKindR tkUnique,  write_heaplet l v h0)]> r.(rtm),
              r.(rcm)), r.(rlm))
Hai Dang's avatar
Hai Dang committed
464
            else r in
Hai Dang's avatar
Hai Dang committed
465
  ( α', memory_written σt.(sst) σt.(scs) l (Tagged tg) (tsize Tt) = Some α' 
Hai Dang's avatar
Hai Dang committed
466
467
468
    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 ((#[])%V) σs' ((#[]%V)) σt' : Prop) 
Hai Dang's avatar
Hai Dang committed
469
470
  r {n,fs,ft}
    (Place l (Tagged tg) Ts <- #v, σs)  (Place l (Tagged tg) Tt <- #v, σt) : Φ.
Hai Dang's avatar
Hai Dang committed
471
Proof.
Hai Dang's avatar
Hai Dang committed
472
  intros r' POST. pfold.
Hai Dang's avatar
Hai Dang committed
473
  intros NT. intros.
Hai Dang's avatar
Hai Dang committed
474
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
Hai Dang's avatar
Hai Dang committed
475
476
  split; [|done|].
  { right.
Hai Dang's avatar
Hai Dang committed
477
    edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
Hai Dang's avatar
Hai Dang committed
478
479
480
481
482
483
    destruct (tstep_write_inv _ _ _ _ _ _ _ _ STEPS)
      as (α' & ? & Eqα' & EqD & IN & EQL & ?).
    subst es'. setoid_rewrite <-(srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
    destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
    rewrite Eqst Eqcs EQS in Eqα'. rewrite -EQL in EQS.
    rewrite EQS in EqD. rewrite Eqnp in IN.
Hai Dang's avatar
Hai Dang committed
484
485
    exists (#[])%V,
           (mkState (write_mem l v σt.(shp)) α' σt.(scs) σt.(snp) σt.(snc)).
Hai Dang's avatar
Hai Dang committed
486
487
    by eapply (head_step_fill_tstep _ []), write_head_step'. }
  constructor 1. intros.
Hai Dang's avatar
Hai Dang committed
488
489
  destruct (tstep_write_inv _ _ _ _ _ _ _ _ STEPT)
    as (α' & ? & Eqα' & EqD & IN & EQL & ?). subst et'.
Hai Dang's avatar
Hai Dang committed
490
  set σs' := mkState (write_mem l v σs.(shp)) α' σs.(scs) σs.(snp) σs.(snc).
Hai Dang's avatar
Hai Dang committed
491
  have STEPS: ((Place l (Tagged tg) Ts <- v)%E, σs) ~{fs}~> ((#[])%V, σs').
Hai Dang's avatar
Hai Dang committed
492
493
494
495
496
  { setoid_rewrite (srel_heap_dom _ _ _ WFS WFT SREL) in EqD.
    destruct SREL as (Eqst&Eqnp&Eqcs&Eqnc&AREL).
    rewrite -Eqst -Eqcs -EQS in Eqα'. rewrite -EQS in EQL.
    rewrite EQL in EqD. rewrite -Eqnp in IN.
    eapply (head_step_fill_tstep _ []), write_head_step'; eauto. }
Hai Dang's avatar
Hai Dang committed
497
  have HL: if k0 then  kh, r_f.(rtm)  <[tg:=kh]> r.(rtm) = <[tg:=kh]> (r_f.(rtm)  r.(rtm)) else True.
Hai Dang's avatar
Hai Dang committed
498
  { destruct k0; [|done]. intros.
Hai Dang's avatar
Hai Dang committed
499
500
    rewrite (tmap_insert_op_r r_f.(rtm) r.(rtm) tg h0) //. apply VALID. }
  have HL2: if k0 then  (r_f.(rtm)  r.(rtm)) !! tg = Some (to_tagKindR tkUnique, h0) else True.
Hai Dang's avatar
Hai Dang committed
501
  { destruct k0; [|done].
Hai Dang's avatar
Hai Dang committed
502
    by apply (tmap_lookup_op_r _ _ _ _ (proj1 (proj1 VALID)) Eqtg). }
Hai Dang's avatar
Hai Dang committed
503
  exists (#[])%V, σs', r', (S n). split; last split.
Hai Dang's avatar
Hai Dang committed
504
  { left. by constructor 1. }
Hai Dang's avatar
Hai Dang committed
505
  { split; last split; last split; last split; last split; last split.
Hai Dang's avatar
Hai Dang committed
506
507
    - by apply (tstep_wf _ _ _ STEPS WFS).
    - by apply (tstep_wf _ _ _ STEPT WFT).
Hai Dang's avatar
Hai Dang committed
508
    - (* valid *)
Hai Dang's avatar
Hai Dang committed
509
510
      rewrite /r'. destruct k0; [|done]. do 2 (split; [|apply VALID]).
      eapply tmap_valid; eauto; [|apply VALID]. split; [done|].
Hai Dang's avatar
Hai Dang committed
511
      apply write_heaplet_valid.
Hai Dang's avatar
Hai Dang committed
512
      have VL := (proj1 (proj1 (cmra_valid_op_r _ _ VALID)) tg).
Hai Dang's avatar
Hai Dang committed
513
      rewrite Eqtg in VL. apply VL.
Hai Dang's avatar
Hai Dang committed
514
    - (* tmap_inv *)
Hai Dang's avatar
Hai Dang committed
515
      intros t k h Eqt.
Hai Dang's avatar
Hai Dang committed
516
      have Eqttg: t = tg  k0 = tkUnique  k = k0  h  write_heaplet l v h0.
Hai Dang's avatar
Hai Dang committed
517
      { intros. subst t k0. move  : Eqt. rewrite /rtm /= HL lookup_insert.
Hai Dang's avatar
Hai Dang committed
518
        intros [Eq1 Eq2]%Some_equiv_inj.
Hai Dang's avatar
Hai Dang committed
519
520
        simpl in Eq1, Eq2. rewrite Eq2. repeat split; [|done].
        destruct k; [done|inversion Eq1]. }
Hai Dang's avatar
Hai Dang committed
521
      have CASEt : (t = tg  k0 = tkUnique  k = k0  h  write_heaplet l v h0 
Hai Dang's avatar
Hai Dang committed
522
523
                    (r_f  r).(rtm) !! t  Some (to_tagKindR k, h) 
                      (k = tkUnique  t  tg)).
Hai Dang's avatar
Hai Dang committed
524
525
      { move : Eqt. rewrite /r'.
        destruct k0; simpl.
Hai Dang's avatar
Hai Dang committed
526
        - rewrite /rtm /= HL.
Hai Dang's avatar
Hai Dang committed
527
528
529
530
531
532
533
          case (decide (t = tg)) => ?; [subst t|rewrite lookup_insert_ne //].
          + left. by destruct Eqttg.
          + right. naive_solver.
        - case (decide (t = tg)) => ?; [subst t|].
          + intros Eqt. right. split; [done|]. intros ?. subst k.
            move : Eqt. rewrite lookup_op Eqtg. by move => /tagKindR_exclusive_2.
          + right. naive_solver. }
Hai Dang's avatar
Hai Dang committed
534
      split.
Hai Dang's avatar
Hai Dang committed
535
      { subst σt'. simpl. destruct CASEt as [(?&?&?&?Eqh)|[Eqh NEQ]].
Hai Dang's avatar
Hai Dang committed
536
537
        - subst t k k0. apply (PINV tg tkUnique h0). by rewrite HL2.
        - move : Eqh. apply PINV. }
Hai Dang's avatar
Hai Dang committed
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
      intros l' s' Eqk'. split.
      { destruct CASEt as [(?&?&?&?Eqh)|[Eqh NEQ]].
        - subst t k k0. destruct (PINV tg tkUnique h0) as [? PI]; [by rewrite HL2|].
          have InD': l'  dom (gset loc) h.
          { rewrite elem_of_dom.
            destruct (h !! l') eqn:Eql'; rewrite Eql'; [by eexists|by inversion Eqk']. }
          move : InD'. rewrite Eqh write_heaplet_dom elem_of_dom.
          intros [s0 Eqs0].
          have VALS := proj1 (proj1 (cmra_valid_op_r _ _ VALID)) tg. rewrite Eqtg in VALS.
          have VALs0:  s0. { change ( (Some s0)). rewrite -Eqs0. apply VALS. }
          apply to_agree_uninj in VALs0 as [ss0 Eqss0].
          destruct (PI l' ss0) as [? _]; [|done]. by rewrite Eqs0 Eqss0.
        - specialize (PINV _ _ _ Eqh) as [? PINV].
          specialize (PINV _ _ Eqk') as [EQ _]. rewrite /r' /=. by destruct k0. }
      intros stk'. subst σt'. simpl.
Hai Dang's avatar
Hai Dang committed
553
554
555
556
557
      destruct (write_mem_lookup_case l v σt.(shp) l')
          as [[i [Lti [Eqi Eqmi]]]|[NEql Eql]]; last first.
      { (* l' is NOT written to *)
        destruct (for_each_lookup _ _ _ _ _ Eqα') as [_ [_ EQ]].
        rewrite EQL in NEql. rewrite (EQ _ NEql) Eql.
Hai Dang's avatar
Hai Dang committed
558
        destruct CASEt as [(?&?&?&?Eqh)|[Eqh ?]]; [|by apply (PINV t k h Eqh)].
Hai Dang's avatar
Hai Dang committed
559
560
561
562
563
564
        subst t k k0. apply (PINV tg tkUnique h0).
        - by rewrite HL2.
        - move : Eqk'. rewrite Eqh. rewrite -EQL in NEql.
          by rewrite (proj2 (write_heaplet_lookup l v h0) _ NEql). }
      (* l' is written to *)
      intros Eqstk' pm opro In' NDIS. subst l'.
Hai Dang's avatar
Hai Dang committed
565
566
      destruct (for_each_access1 _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
        as (stk & Eqstk & SUB & ?).
Hai Dang's avatar
Hai Dang committed
567
      destruct (SUB _ In') as (it2 & In2 & Eqt2 & Eqp2 & NDIS2). simpl in *.
Hai Dang's avatar
Hai Dang committed
568
      destruct CASEt as [(?&?&?&?Eqh)|[Eqh NEQ]].
Hai Dang's avatar
Hai Dang committed
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
      + (* t = tg *)
        subst t k k0. rewrite -> Eqh in Eqk'. split.
        * have Eqs' := proj1 (write_heaplet_lookup l v h0) _ _ Lti Eqk'.
          rewrite (proj1 (write_mem_lookup l v σt.(shp)) _ Lti).
          destruct (v !! i) as [s''|] eqn: Eq''; [rewrite Eq''|by inversion Eqs'].
          apply Some_equiv_inj, to_agree_inj in Eqs'. by inversion Eqs'.
        * assert ( s0: scalar, h0 !! (l + i)  Some (to_agree s0)) as [s0 Eq0].
          { assert (is_Some (h0 !! (l + i))) as [s0 Eqs0].
            { rewrite -(elem_of_dom (D:=gset loc)) -(write_heaplet_dom l v h0).
              move : Eqk'.
              destruct (write_heaplet l v h0 !! (l + i)) eqn: Eq'';
                rewrite Eq''; [intros _|by inversion 1].
              apply (elem_of_dom_2 _ _ _ Eq''). }
            rewrite Eqs0.
            destruct (to_agree_uninj s0) as [s1 Eq1]; [|by exists s1; rewrite -Eq1].
            apply (lookup_valid_Some h0 (l + i)); [|by rewrite Eqs0].
Hai Dang's avatar
Hai Dang committed
585
            apply (lookup_valid_Some (r_f.(rtm)  r.(rtm)) tg (to_tagKindR tkUnique, h0));
Hai Dang's avatar
Hai Dang committed
586
              [by apply (proj1 VALID)|by rewrite HL2]. }
Hai Dang's avatar
Hai Dang committed
587
588
589
          specialize (PINV tg tkUnique h0) as [Lt PI]; [by rewrite HL2|].
          specialize (PI _ _ Eq0) as [? PI].
          specialize (PI _ Eqstk it2.(perm) opro) as [Eql' HTOP].
Hai Dang's avatar
Hai Dang committed
590
591
592
593
594
595
596
          { rewrite /= Eqt2 Eqp2. by destruct it2. } { by rewrite (NDIS2 NDIS). }
          destruct (for_each_lookup_case _ _ _ _ _ Eqα' _ _ _ Eqstk Eqstk')
            as [?|[MR _]]; [by subst|]. clear -In' MR HTOP Eqstk WFT NDIS.
          destruct (access1 stk AccessWrite (Tagged tg) σt.(scs))
            as [[n stk1]|] eqn:Eqstk'; [|done]. simpl in MR. simplify_eq.
          destruct (state_wf_stack_item _ WFT _ _ Eqstk). move : Eqstk' HTOP.
          eapply access1_head_preserving; eauto.
Hai Dang's avatar
Hai Dang committed
597
      + (* invoke PINV for t *)
Hai Dang's avatar
Hai Dang committed
598
        exfalso. destruct (PINV t k h Eqh) as [Lt PI].
Hai Dang's avatar
Hai Dang committed
599
600
        specialize (PI _ _ Eqk') as [? PI].
        specialize (PI _ Eqstk it2.(perm) opro) as [Eql' HTOP].
Hai Dang's avatar
Hai Dang committed
601
        { rewrite /= Eqt2 Eqp2. by destruct it2. } { by rewrite (NDIS2 NDIS). }
Hai Dang's avatar
Hai Dang committed
602
603
604
        destruct k.
        * (* if k is Unique  t  tg, writing with tg must have popped t
            from top, contradicting In'. *)
Hai Dang's avatar
Hai Dang committed
605
606
607
608
609
          destruct (for_each_lookup _ _ _ _ _ Eqα') as [EQ1 _].
          rewrite EQL in Lti. destruct (EQ1 _ _ Lti Eqstk) as [ss' [Eq' EQ2]].
          have ?: ss' = stk'. { rewrite Eqstk' in Eq'. by inversion Eq'. }
          subst ss'. clear Eq'. move : EQ2. case access1 as [[n1 stk1]|] eqn:EQ3; [|done].
          simpl. intros ?. simplify_eq.
Hai Dang's avatar
Hai Dang committed
610
          specialize (NEQ eq_refl).
Hai Dang's avatar
Hai Dang committed
611
612
613
614
          have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
          move : In'.
          eapply (access1_write_remove_incompatible_head _ tg t _ _ _ ND);
            [by eexists|done..].
Hai Dang's avatar
Hai Dang committed
615
616
        * (* if k is Public => t is for SRO, and must also have been popped,
             contradicting In'. *)
Hai Dang's avatar
Hai Dang committed
617
618
619
620
621
622
623
624
          destruct (for_each_lookup _ _ _ _ _ Eqα') as [EQ1 _].
          rewrite EQL in Lti. destruct (EQ1 _ _ Lti Eqstk) as [ss' [Eq' EQ2]].
          have ?: ss' = stk'. { rewrite Eqstk' in Eq'. by inversion Eq'. }
          subst ss'. clear Eq'. move : EQ2. case access1 as [[n1 stk1]|] eqn:EQ3; [|done].
          simpl. intros ?. simplify_eq.
          have ND := proj2 (state_wf_stack_item _ WFT _ _ Eqstk).
          move : In'.
          eapply (access1_write_remove_incompatible_active_SRO _ tg t _ _ _ ND); eauto.
Hai Dang's avatar
Hai Dang committed
625
626
    - (* cmap_inv : make sure tags in the new resource are still on top *)
      intros c cs Eqc'.
Hai Dang's avatar
Hai Dang committed
627
      have Eqc: (r_f  r).(rcm) !! c  Some cs.
Hai Dang's avatar
Hai Dang committed
628
629
      { move  : Eqc'. rewrite /r'. by destruct k0. }
      specialize (CINV _ _ Eqc). subst σt'. simpl.
Hai Dang's avatar
Hai Dang committed
630
      clear -Eqα' CINV Eqtg VALID HL HL2. destruct cs as [[T|]| |]; [|done..].
Hai Dang's avatar
Hai Dang committed
631
      destruct CINV as [IN CINV]. split; [done|].
Hai Dang's avatar
Hai Dang committed
632
633
      intros t InT. specialize (CINV _ InT) as [? CINV]. split; [done|].
      intros k h.
Hai Dang's avatar
Hai Dang committed
634
635
      (* TODO: duplicated proofs *)
      rewrite /r'. destruct k0.
Hai Dang's avatar
Hai Dang committed
636
      + (* if tg was unique *)
Hai Dang's avatar
Hai Dang committed
637
        rewrite /rtm /= HL.
Hai Dang's avatar
Hai Dang committed
638
639
640
        case (decide (t = tg)) => ?.
        { subst tg. rewrite lookup_insert.
          intros [Eqk Eqh]%Some_equiv_inj. simpl in Eqk, Eqh.
Hai Dang's avatar
Hai Dang committed
641
          have Eqt : (r_f  r).(rtm) !! t  Some (k, h0) by rewrite HL2 -Eqk.
Hai Dang's avatar
Hai Dang committed
642
          intros l'. rewrite -Eqh write_heaplet_dom. intros Inh.
Hai Dang's avatar
Hai Dang committed
643
          destruct (CINV _ _ Eqt _ Inh) as (stk' & pm' & Eqstk' & Instk' & NDIS).
Hai Dang's avatar
Hai Dang committed
644
645
          destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
            as [stk [Eqstk AS]].
Hai Dang's avatar
Hai Dang committed
646
          exists stk, pm'. split; last split; [done|by apply AS|done]. }
Hai Dang's avatar
Hai Dang committed
647
648
        { rewrite lookup_insert_ne //.
          intros Eqt l' Inh.
Hai Dang's avatar
Hai Dang committed
649
          destruct (CINV _ _ Eqt _ Inh) as (stk' & pm' & Eqstk' & Instk' & NDIS).
Hai Dang's avatar
Hai Dang committed
650
651
          destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
            as [stk [Eqstk AS]].
Hai Dang's avatar
Hai Dang committed
652
          exists stk, pm'. split; last split; [done|by apply AS|done]. }
Hai Dang's avatar
Hai Dang committed
653
654
      + (* if tg was public *)
        intros Eqt l' Inh.
Hai Dang's avatar
Hai Dang committed
655
        destruct (CINV _ _ Eqt _ Inh) as (stk' & pm' & Eqstk' & Instk' & NDIS).
Hai Dang's avatar
Hai Dang committed
656
657
        destruct (for_each_access1_active_preserving _ _ _ _ _ _ _ Eqα' _ _ Eqstk')
          as [stk [Eqstk AS]].
Hai Dang's avatar
Hai Dang committed
658
        exists stk, pm'. split; last split; [done|by apply AS|done].
Hai Dang's avatar
Hai Dang committed
659
660
    - (* srel *)
      subst σt'. rewrite /srel /=. destruct SREL as (?&?&?&?&Eq).
Hai Dang's avatar
Hai Dang committed
661
      repeat split; [done..|].
Hai Dang's avatar
Hai Dang committed
662
      intros l1 InD1 Eq1.
Hai Dang's avatar
Hai Dang committed
663
      destruct (write_mem_lookup l v σs.(shp)) as [EqN EqO]. rewrite /r'.
Hai Dang's avatar
Hai Dang committed
664
665
      destruct (write_mem_lookup_case l v σt.(shp) l1)
        as [[i [Lti [Eqi Eqmi]]]|[NEql Eql]].
Hai Dang's avatar
Hai Dang committed
666
667
668
669
      + subst l1. specialize (EqN _ Lti). (* rewrite EqN. *)
        have InD := (EqD _ Lti).
        have Eq1' : (r_f  r).(rlm) !! (l + i)  Some $ to_locStateR lsShared
          by destruct k0. specialize (Eq _ InD Eq1').
Hai Dang's avatar
Hai Dang committed
670
671
672
        destruct (lookup_lt_is_Some_2 _ _ Lti) as [s Eqs].
        destruct k0.
        * (* tg was unique, and (l + i) was written to *)
Hai Dang's avatar
Hai Dang committed
673
674
675
676
          destruct Eq as [PB|[t PV]].
          { 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|].
Hai Dang's avatar
Hai Dang committed
677
678
679
680
681
            move : (PUBWRITE _ (elem_of_list_lookup_2 _ _ _ Eqs)).
            rewrite /arel /=. destruct s as [| |l0 t0|]; [done..| |done].
            intros [? [? Eqt0]]. repeat split; [done..|].
            destruct t0 as [t0|]; [|done].
            repeat split. destruct Eqt0 as [ht0 Eqt0].
Hai Dang's avatar
Hai Dang committed
682
683
684
            destruct (tmap_lookup_op_r_equiv_pub r_f.(rtm) r.(rtm)
                        _ _ (proj1 (proj1 VALID)) Eqt0) as [h' Eq'].
            exists (h'  ht0). rewrite /rtm /= HL lookup_insert_ne //.
Hai Dang's avatar
Hai Dang committed
685
686
687
688
689
690
            intros ?; subst t0. rewrite Eqtg in Eqt0.
            apply Some_equiv_inj in Eqt0 as [Eqt0 _]. inversion Eqt0. }
          { destruct PV as (c & T & h & Eqc & InT & Eqt & Inh).
            right. exists t, c, T.
            case (decide (t = tg)) => ?; [subst t|].
            - exists (write_heaplet l v h0). do 2 (split; [done|]). split.
Hai Dang's avatar
Hai Dang committed
691
692
              by rewrite /rtm /= HL lookup_insert.
              rewrite write_heaplet_dom.
Hai Dang's avatar
Hai Dang committed
693
694
              rewrite HL2 in Eqt. apply Some_equiv_inj in Eqt as [? Eqt].
              simpl in Eqt. by rewrite Eqt.
Hai Dang's avatar
Hai Dang committed
695
            - exists h. rewrite /rtm /= HL. do 2 (split; [done|]).
Hai Dang's avatar
Hai Dang committed
696
697
              rewrite lookup_insert_ne //. }
        * (* tg was public, and (l + i) was written to *)
Hai Dang's avatar
Hai Dang committed
698
699
700
          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|].
Hai Dang's avatar
Hai Dang committed
701
702
703
704
          (* we know that the values written must be publicly related *)
          apply (arel_mono r _ VALID).
          { apply cmra_included_r. }
          { apply PUBWRITE, (elem_of_list_lookup_2 _ _ _ Eqs). }
Hai Dang's avatar
Hai Dang committed
705
706
707
708
709
710
711
712
      + specialize (EqO _ NEql).
        have InD1': l1  dom (gset loc) σt.(shp)
          by rewrite elem_of_dom -Eql -(elem_of_dom (D:=gset loc)).
        have Eq1' : (r_f  r).(rlm) !! l1  Some $ to_locStateR lsShared.
        { move : Eq1. by destruct k0. }
        specialize (Eq _ InD1' Eq1'). rewrite /pub_loc EqO Eql.
        destruct k0; [|done].
        destruct Eq as [PB|[t PV]].
Hai Dang's avatar
Hai Dang committed
713
        * (* tg was unique, and l1 was NOT written to *)
Hai Dang's avatar
Hai Dang committed
714
715
716
          left. intros st Eqst. destruct (PB _ Eqst) as [ss [Eqss AREL]].
          exists ss. split; [done|]. move : AREL. rewrite /arel.
          destruct ss as [| |l0 t0|], st as [| |l3 t3|]; try done.
Hai Dang's avatar
Hai Dang committed
717
718
          intros [? [? Eqt]]. subst l3 t3. repeat split.
          destruct t0 as [t0|]; [|done].
Hai Dang's avatar
Hai Dang committed
719
          destruct Eqt as [h Eqt]. exists h.
Hai Dang's avatar
Hai Dang committed
720
          rewrite /rtm /= HL (lookup_insert_ne _ tg) //.
Hai Dang's avatar
Hai Dang committed
721
722
723
724
725
726
727
          intros ?. subst t0. move : Eqt. rewrite lookup_op Eqtg.
          by apply tagKindR_exclusive.
        * (* tg was public, and l1 was NOT written to *)
          right. destruct PV as (c & T & h & Eqc & InT & Eqt & Inl).
          exists t, c, T. simpl.
          case (decide (t = tg)) => ?; [subst t|].
          { eexists (write_heaplet l v h0).
Hai Dang's avatar
Hai Dang committed
728
            rewrite /rtm /= HL lookup_insert. repeat split; [done..|].
Hai Dang's avatar
Hai Dang committed
729
730
            rewrite lookup_op Eqtg in Eqt.
            by rewrite write_heaplet_dom (tagKindR_exclusive_heaplet _ _ _ Eqt). }
Hai Dang's avatar
Hai Dang committed
731
          { exists h. rewrite /rtm /= HL lookup_insert_ne //. }
Hai Dang's avatar
Hai Dang committed
732
733
734
735
736
737
738
739
740
741
742
    - intros l' s' stk' Eq.
      have Eq' : rlm (r_f  r) !! l'  Some (to_locStateR (lsLocal s' stk')) by destruct k0.
      specialize (LINV _ _ _ Eq').
      subst σt'. rewrite /=.
      destruct (write_mem_lookup l v σs.(shp)) as [_ HLs].
      destruct (write_mem_lookup l v σt.(shp)) as [_ HLt].
      have ?:  i, (i < length v)%nat  l'  l + i.
      { intros i Lti EQ. rewrite EQL in Lti. specialize (SHR _ Lti).
        subst l'. apply (lmap_lookup_op_r r_f.(rlm)) in SHR; [|apply VALID].
        move : Eq'. rewrite SHR. intros Eqv%Some_equiv_inj. inversion Eqv. }
      rewrite HLs // HLt //.
Hai Dang's avatar
Hai Dang committed
743
  }
Hai Dang's avatar
Hai Dang committed
744
  left.
Hai Dang's avatar
Hai Dang committed
745
  eapply (sim_body_result fs ft r' n (ValR [%S]) (ValR [%S])).
Hai Dang's avatar
Hai Dang committed
746
  intros. simpl. subst σt'. by apply POST.
Hai Dang's avatar
Hai Dang committed
747
Qed.
Hai Dang's avatar
Hai Dang committed
748

Hai Dang's avatar
Hai Dang committed
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
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
(** Retag *)

Lemma retag_ref_change_1 h α cids c nxtp x rk mut T h' α' nxtp'
  (N2: rk  TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) :
  retag h α nxtp cids c x rk (Reference (RefPtr mut) T) = Some (h', α', nxtp') 
   l otag, h !! x = Some (ScPtr l otag) 
   rk' new,
    h' = <[x := ScPtr l new]>h 
    retag_ref h α cids nxtp l otag T rk' (adding_protector rk c) =
      Some (new, α', nxtp') 
    rk' = if mut then UniqueRef (is_two_phase rk) else SharedRef.
Proof.
  rewrite retag_equation_2 /=.
  destruct (h !! x) as [[| |l t|]|]; simpl; [done..| |done|done].
  destruct mut; (case retag_ref as [[[t1 α1] n1]|] eqn:Eq => [/=|//]);
    intros; simplify_eq; exists l, t; (split; [done|]);
    eexists; exists t1; done.
Qed.

Lemma retag_ref_change_2
  h α cids c nxtp l otag rk (mut: mutability) T new α' nxtp'
  (TS: (O < tsize T)%nat) (FRZ: is_freeze T) :
  let rk' := if mut then UniqueRef false else SharedRef in
  let opro := (adding_protector rk c) in
  retag_ref h α cids nxtp l otag T rk' opro = Some (new, α', nxtp') 
  nxtp' = S nxtp  new = Tagged nxtp 
  reborrowN α cids l (tsize T) otag (Tagged nxtp)
            (if mut then Unique else SharedReadOnly) opro = Some α'.
Proof.
  intros rk' opro. rewrite /retag_ref. destruct (tsize T) as [|n] eqn:EqT; [lia|].
  destruct mut; simpl; [|rewrite visit_freeze_sensitive_is_freeze //];
    case reborrowN as [α1|] eqn:Eq1 => [/=|//]; intros; simplify_eq; by rewrite -EqT.
Qed.

Lemma retag_ref_change h α cids c nxtp x rk mut T h' α' nxtp'
  (N2: rk  TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) :
  retag h α nxtp cids c x rk (Reference (RefPtr mut) T) = Some (h', α', nxtp') 
   l otag, h !! x = Some (ScPtr l otag) 
    h' = <[x := ScPtr l (Tagged nxtp)]>h 
    nxtp' = S nxtp 
    reborrowN α cids l (tsize T) otag (Tagged nxtp)
            (if mut then Unique else SharedReadOnly) (adding_protector rk c) = Some α'.
Proof.
  intros RT.
  apply retag_ref_change_1 in RT
    as (l & otag & EqL & rk' & new & Eqh & RT &?); [|done..].
  subst. exists l, otag. split; [done|].
  rewrite (_: is_two_phase rk = false) in RT; [|by destruct rk].
  apply retag_ref_change_2 in RT as (?&?&?); [|done..]. by subst new.
Qed.

Lemma retag_ref_reborrowN
  (h: mem) α t cids c x l otg T rk (mut: mutability) α'
  (N2: rk  TwoPhase) (TS: (O < tsize T)%nat) (FRZ: is_freeze T) :
  h !! x = Some (ScPtr l otg) 
  reborrowN α cids l (tsize T) otg (Tagged t)
     (if mut then Unique else SharedReadOnly) (adding_protector rk c) =
     Some α' 
  retag h α t cids c x rk (Reference (RefPtr mut) T) = Some (<[x:=ScPtr l (Tagged t)]> h, α', S t).
Proof.
  intros Eqx RB. rewrite retag_equation_2 Eqx /= /retag_ref.
  destruct (tsize T) eqn:EqT; [lia|].
  rewrite (_: is_two_phase rk = false); [|by destruct rk].
  destruct mut; simpl; [|rewrite visit_freeze_sensitive_is_freeze //]; rewrite EqT RB /= //.
Qed.

Lemma sim_body_retag_default fs ft r n x xtag mut T σs σt Φ
  (TS: (O < tsize T)%nat) (FRZ: is_freeze T) (Eqx: σs.(shp) = σt.(shp)) :
  let Tr := (Reference (RefPtr mut) T) in
  ( c cids hs' αs' nps' ht' αt' npt' (STACK: σt.(scs) = c :: cids),
    retag σt.(shp) σt.(sst) σt.(snp) σt.(scs) c x Default Tr
      = Some (ht', αt', npt') 
    retag σs.(shp) σs.(sst) σs.(snp) σs.(scs) c x Default Tr
      = Some (hs', αs', nps') 
    let σs' := mkState hs' αs' σs.(scs) nps' σs.(snc) in
    let σt' := mkState ht' αt' σt.(scs) npt' σt.(snc) in
      Φ r n ((#[])%V) σs' ((#[]%V)) σt' : Prop) 
  r {n,fs,ft}
    (Retag (Place x xtag Tr) Default, σs) 
    (Retag (Place x xtag Tr) Default, σt) : Φ.
Proof.
  intros Tr POST. pfold. intros NT. intros.
Hai Dang's avatar
Hai Dang committed
831
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
Hai Dang's avatar
Hai Dang committed
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
  split; [|done|].
  { right.
    edestruct NT as [[]|[es' [σs' STEPS]]]; [constructor 1|done|].
    (* inversion retag of src *)
    destruct (tstep_retag_inv _ _ _ _ _ _ _ _ _ STEPS)
      as (c & cids & h' & α' & nxtp' & Eqs & EqT & ? & ?). subst es'.
    apply retag_ref_change in EqT as (l & otg & Eqx' & Eqh' & Eqp' & RB); [|done..].
    subst h' nxtp'. destruct SREL as (Eqst & Eqnp & Eqcs & Eqnc &?).
    rewrite Eqx in Eqx'. rewrite Eqst Eqcs Eqnp in RB. rewrite Eqcs in Eqs.
    (* retag of tgt *)
    exists (#[])%V,
      (mkState (<[x:=ScPtr l (Tagged σt.(snp))]> σt.(shp)) α' σt.(scs) (S σt.(snp)) σt.(snc)).
    eapply (head_step_fill_tstep _ []), retag1_head_step'; [eauto|].
    eapply retag_ref_reborrowN; eauto. }
  constructor 1.
  intros.
  (* inversion retag of tgt *)
  destruct (tstep_retag_inv _ _ _ _ _ _ _ _ _ STEPT)
      as (c & cids & h' & α' & nxtp' & Eqs & EqT & ? & ?). subst et'.
  apply retag_ref_change in EqT as (l & otg & Eqx' & Eqh' & Eqp' & RB); [|done..].
  subst h' nxtp'.
  exists (#[])%V,
      (mkState (<[x:=ScPtr l (Tagged σs.(snp))]> σs.(shp)) α' σs.(scs) (S σs.(snp)) σs.(snc)).
  exists r, n. split; last split.
  { left. apply tc_once.
    destruct SREL as (Eqst & Eqnp & Eqcs & Eqnc &?).
    rewrite -Eqx in Eqx'. rewrite -Eqst -Eqcs -Eqnp in RB. rewrite -Eqcs in Eqs.
    eapply (head_step_fill_tstep _ []), retag1_head_step'; [eauto|].
    eapply retag_ref_reborrowN; eauto. }
  { split.
Abort.

Hai Dang's avatar
Hai Dang committed
864
(** InitCall *)
Hai Dang's avatar
fix let    
Hai Dang committed
865
866
867
Lemma sim_body_init_call fs ft r n es et σs σt Φ :
  let σs' := mkState σs.(shp) σs.(sst) (σs.(snc) :: σs.(scs)) σs.(snp) (S σs.(snc)) in
  let σt' := mkState σt.(shp) σt.(sst) (σt.(snc) :: σt.(scs)) σt.(snp) (S σt.(snc)) in
Ralf Jung's avatar
Ralf Jung committed
868
  let r'  : resUR := res_callState σt.(snc) (csOwned ) in
Hai Dang's avatar
Hai Dang committed
869
870
  r  r' {n,fs,ft} (es, σs')  (et, σt') : Φ 
  r {n,fs,ft} (InitCall es, σs)  (InitCall et, σt) : Φ.
Hai Dang's avatar
fix let    
Hai Dang committed
871
872
Proof.
  intros σs' σt1 r' SIM. pfold.
Hai Dang's avatar
Hai Dang committed
873
  intros NT. intros. split; [|done|].
Hai Dang's avatar
Hai Dang committed
874
  { right. do 2 eexists. by eapply (head_step_fill_tstep _ []), initcall_head_step. }
Hai Dang's avatar
Hai Dang committed
875
  constructor 1. intros.
876
  exists es, σs', (r  r').
Hai Dang's avatar
fix let    
Hai Dang committed
877
  destruct (tstep_init_call_inv _ _ _ _ _ STEPT). subst et' σt'.
878
  have STEPS: (InitCall es, σs) ~{fs}~> (es, σs').
Hai Dang's avatar
fix let    
Hai Dang committed
879
  { by eapply (head_step_fill_tstep _ []), initcall_head_step. }
Hai Dang's avatar
Hai Dang committed
880
881
  have FRESH: (r_f  r).(rcm) !! σt.(snc) = None.
  { destruct ((r_f  r).(rcm) !! σt.(snc)) as [cs|] eqn:Eqcs; [|done].
Hai Dang's avatar
Hai Dang committed
882
883
    exfalso. destruct WSAT as (WFS & WFT & ? & ? & CINV & ?).
    apply (lt_irrefl σt.(snc)), (cinv_lookup_in_eq _ _ _ _ WFT CINV Eqcs). }
Hai Dang's avatar
fix let    
Hai Dang committed
884
  have LOCAL: (r_f  r  ε, ε) ~l~> (r_f  r  r', r').
Hai Dang's avatar
Hai Dang committed
885
  { apply prod_local_update_1, prod_local_update_2.
Hai Dang's avatar
fix let    
Hai Dang committed
886
887
888
889
890
891
    rewrite /= right_id (comm _ (_  _)) -insert_singleton_op //.
    by apply alloc_singleton_local_update. }
  exists n. split; last split; cycle 2.
  { (* sim cont *)  by punfold SIM. }
  { (* STEP src *)  left. by apply tc_once. }
  (* WSAT new *)
Hai Dang's avatar
Hai Dang committed
892
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL & LINV).
Hai Dang's avatar
fix let    
Hai Dang committed
893
  rewrite assoc.
Hai Dang's avatar
Hai Dang committed
894
  split; last split; last split; last split; last split; last split.
Hai Dang's avatar
fix let    
Hai Dang committed
895
896
897
898
899
  { (* WF src *)    by apply (tstep_wf _ _ _ STEPS WFS). }
  { (* WF tgt *)    by apply (tstep_wf _ _ _ STEPT WFT). }
  { (* VALID *)
    apply (local_update_discrete_valid_frame (r_f  r) ε r'); [|done].
    by rewrite right_id. }
Hai Dang's avatar
Hai Dang committed
900
  { (* tmap_inv *)
Hai Dang's avatar
Hai Dang committed
901
902
    move => t k h /=. rewrite /rtm /= right_id. move => /PINV [? PI].
    split; [done|]. intros ???. rewrite right_id. by apply PI. }
Hai Dang's avatar
fix let    
Hai Dang committed
903
904
  { (* cmap_inv *)
    intros c cs.
Hai Dang's avatar
Hai Dang committed
905
    rewrite /rcm /= (comm _ (r_f.(rcm)  r.(rcm))) -insert_singleton_op //.
Hai Dang's avatar
fix let    
Hai Dang committed
906
907
908
909
910
    case (decide (c = σt.(snc))) => [->|NE].
    - rewrite lookup_insert. intros Eqcs%Some_equiv_inj.
      inversion Eqcs as [?? Eq| |]; subst. inversion Eq as [?? Eq2|] ; subst.
      split; [by left|]. intros ? IN. exfalso. move : IN.
      by rewrite -Eq2 elem_of_empty.
Hai Dang's avatar
Hai Dang committed
911
    - rewrite lookup_insert_ne // => /CINV. destruct cs as [[]| |]; [|done|lia|done].
Hai Dang's avatar
Hai Dang committed
912
      intros [? Ht]. split; [by right|].
Hai Dang's avatar
Hai Dang committed
913
      setoid_rewrite (right_id _ _ (r_f.(rtm)  r.(rtm))). naive_solver. }
Hai Dang's avatar
fix let    
Hai Dang committed
914
915
916
  { (* srel *)
    destruct SREL as (?&?&?&?&SREL).
    do 2 (split; [done|]). do 2 (split; [simpl; by f_equal|]).
Hai Dang's avatar
Hai Dang committed
917
918
919
920
921
    move => l InD. rewrite {1}/r' /= right_id => SHR.
    destruct (SREL _ InD SHR) as [PUB|[t [c [T [h [PRI [? ?]]]]]]]; [left|right].
    - move => st /PUB [ss [Eqss AREL]]. exists ss. split; [done|]. move : AREL.
      rewrite /arel /=.
      destruct st, ss as [| |l2 [|]|]; auto.
Hai Dang's avatar
Hai Dang committed
922
923
924
      by setoid_rewrite (right_id _ _ (r_f.(rtm)  r.(rtm))).
    - exists t, c, T, h. rewrite /rtm /= right_id. split; [|done].
      rewrite /rcm /= (comm _ (r_f.(rcm)  r.(rcm))) -insert_singleton_op //.
Hai Dang's avatar
fix let    
Hai Dang committed
925
      rewrite lookup_insert_ne // => Eqc. subst c.
Hai Dang's avatar
Hai Dang committed
926
      apply (lt_irrefl σt.(snc)), (cinv_lookup_in _ _ _ _ WFT CINV PRI). }
Hai Dang's avatar
Hai Dang committed
927
  { intros ???. rewrite /lmap_inv /= right_id. apply LINV. }
Hai Dang's avatar
Hai Dang committed
928
Qed.