right_step.v 6 KB
Newer Older
Hai Dang's avatar
Hai Dang committed
1
2
3
From iris.algebra Require Import local_updates.

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 body.
Hai Dang's avatar
Hai Dang committed
5
6
7

Set Default Proof Using "Type".

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

Lemma sim_body_let_r fs ft r n x es et1 et2 vt1 σs σt Φ :
  IntoResult et1 vt1 
  r {n,fs,ft} (es, σs)  (subst' x et1 et2, σt) : Φ 
  r {S n,fs,ft} (es, σs)  (let: x := et1 in et2, σt) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
16
17
18
19
20
21
22
23
24
25
26
  intros TT%into_result_terminal CONT. pfold.
  intros NT r_f WSAT. split; [|done|].
  { right. do 2 eexists. eapply (head_step_fill_tstep _ []).
    econstructor 1. eapply LetBS; eauto. }
  constructor 1. intros.
  destruct (tstep_let_inv _ _ _ _ _ _ _ TT STEPT). subst et' σt'.
  exists es, σs, r, n. split; last split.
  - right. split; [lia|done].
  - done.
  - by left.
Qed.
Ralf Jung's avatar
Ralf Jung committed
27
28
29
30
31
32

Lemma sim_body_deref_r fs ft r n es (rs: result) l t T σs σt Φ :
  IntoResult es rs 
  (Φ r n rs σs (PlaceR l t T) σt) 
  r {S n,fs,ft} (es, σs)  (Deref #[ScPtr l t] T, σt) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
33
34
35
36
37
38
39
40
41
42
43
44
45
  intros TS POST. pfold.
  intros NT r_f WSAT. split; [|done|].
  { right. exists (Place l t T), σt.
    eapply (head_step_fill_tstep _ []). econstructor; econstructor. }
  constructor 1. intros.
  destruct (tstep_deref_inv _ (ValR _) _ _ _ _ STEPT) as (l' & t' & ? & ? & ?).
  simplify_eq.
  exists es, σs, r, n. split; last split.
  - right. split; [lia|done].
  - done.
  - left. apply : sim_body_result.
    intros. by eapply POST.
Qed.
Ralf Jung's avatar
Ralf Jung committed
46

Hai Dang's avatar
Hai Dang committed
47
48
49
50

Lemma sim_body_copy_local_unique_r
  fs ft (r r': resUR) (h: heaplet) n (l: loc) t k T (ss st: scalar) es σs σt Φ
  (LU: k = tkLocal  k = tkUnique) :
Ralf Jung's avatar
Ralf Jung committed
51
  tsize T = 1%nat 
Hai Dang's avatar
Hai Dang committed
52
  tag_on_top σt.(sst) l t Unique 
Hai Dang's avatar
Hai Dang committed
53
  r  r'  res_tag t k h 
Hai Dang's avatar
Hai Dang committed
54
55
  h !! l = Some (ss, st) 
  (r {n,fs,ft} (es, σs)  (#[st], σt) : Φ : Prop) 
Hai Dang's avatar
Hai Dang committed
56
  r {S n,fs,ft} (es, σs)  (Copy (Place l (Tagged t) T), σt) : Φ.
Hai Dang's avatar
Hai Dang committed
57
Proof.
Hai Dang's avatar
Hai Dang committed
58
59
  intros LenT TOP Eqr Eqs CONT. pfold.
  intros NT r_f WSAT. have WSAT1 := WSAT.
Ralf Jung's avatar
Ralf Jung committed
60

Hai Dang's avatar
Hai Dang committed
61
  destruct WSAT as (WFS & WFT & VALID & PINV & CINV & SREL).
Hai Dang's avatar
Hai Dang committed
62
63
64

  (* some lookup properties *)
  have VALIDr := cmra_valid_op_r _ _ VALID. rewrite ->Eqr in VALIDr.
Hai Dang's avatar
Hai Dang committed
65
66
67
68
69
70
71
72
73
74
  have HLtr: r.(rtm) !! t  Some (to_tgkR k, to_agree <$> h).
  { rewrite Eqr. destruct LU; 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 <$> h).
  { destruct LU; subst k.
    - apply tmap_lookup_op_r_local_equiv; [apply VALID|done].
    - apply tmap_lookup_op_r_uniq_equiv; [apply VALID|done]. }
Hai Dang's avatar
Hai Dang committed
75
76
77
78
79
80

  (* we can make the read in tgt because tag_on_top *)
  destruct TOP as [opro TOP].
  destruct (σt.(sst) !! l) as [stk|] eqn:Eqstk; [|done]. simpl in TOP.

  specialize (PINV _ _ _ HLtrf) as [Lt PINV].
Hai Dang's avatar
Hai Dang committed
81
  specialize (PINV l ss st). rewrite lookup_fmap Eqs in PINV.
Hai Dang's avatar
Hai Dang committed
82
83
84
85
  specialize (PINV ltac:(done)) as [Eqss [? HD]].
  { simpl. destruct LU; subst k; [done|].
    exists stk, Unique, opro. split; last split; [done| |done].
    destruct stk; [done|]. simpl in TOP. simplify_eq. by left. }
Hai Dang's avatar
Hai Dang committed
86
87

  destruct (tag_unique_head_access σt.(scs) stk (Tagged t) opro AccessRead)
Hai Dang's avatar
Hai Dang committed
88
89
      as [ns Eqstk'].
  { destruct stk; [done|]. simpl in TOP. simplify_eq. by eexists. }
Hai Dang's avatar
Hai Dang committed
90
91
92

  have Eqα : memory_read σt.(sst) σt.(scs) l (Tagged t) (tsize T) = Some σt.(sst).
  { rewrite LenT /memory_read /= shift_loc_0_nat Eqstk /= Eqstk' /= insert_id //. }
Hai Dang's avatar
Hai Dang committed
93
  have READ: read_mem l (tsize T) σt.(shp) = Some [st].
Hai Dang's avatar
Hai Dang committed
94
95
  { rewrite LenT read_mem_equation_1 /= Eqss //. }

Hai Dang's avatar
Hai Dang committed
96
  have STEPT: (Copy (Place l (Tagged t) T), σt) ~{ft}~> ((#[st])%E, σt).
Hai Dang's avatar
Hai Dang committed
97
98
99
100
101
102
103
104
105
106
107
108
109
110
  { destruct σt.
    eapply (head_step_fill_tstep _ []); eapply copy_head_step'; eauto. }

  split; [right; by do 2 eexists|done|].
  constructor 1. intros et' σt' STEPT'.
  destruct (tstep_copy_inv _ (PlaceR _ _ _) _ _ _ STEPT')
      as (l1&t1&T1& vs1 & α1 & EqH & ? & Eqvs & Eqα' & ?).
  symmetry in EqH. simplify_eq.
  have Eqσt: mkState σt.(shp) σt.(sst) σt.(scs) σt.(snp) σt.(snc) = σt
    by destruct σt. rewrite Eqσt. rewrite Eqσt in STEPT'. clear Eqσt.
  exists es, σs, r, n. split; last split; [|done|].
  - right. split; [lia|done].
  - by left.
Qed.
Hai Dang's avatar
Hai Dang committed
111

Hai Dang's avatar
Hai Dang committed
112
113
114
Lemma sim_body_copy_unique_r
  fs ft (r r': resUR) (h: heaplet) n (l: loc) t T (ss st: scalar) es σs σt Φ :
  tsize T = 1%nat 
Hai Dang's avatar
Hai Dang committed
115
  tag_on_top σt.(sst) l t Unique 
Hai Dang's avatar
Hai Dang committed
116
117
118
119
120
121
  r  r'  res_tag t tkUnique h 
  h !! l = Some (ss, st) 
  (r {n,fs,ft} (es, σs)  (#[st], σt) : Φ : Prop) 
  r {S n,fs,ft} (es, σs)  (Copy (Place l (Tagged t) T), σt) : Φ.
Proof. apply sim_body_copy_local_unique_r. by right. Qed.

Hai Dang's avatar
Hai Dang committed
122
Lemma vsP_res_mapsto_tag_on_top (r: resUR) l t s σs σt :
Hai Dang's avatar
Hai Dang committed
123
  (r  res_loc l [s] t) ={σs,σt}=> (λ _ _ σt, tag_on_top σt.(sst) l t Unique : Prop).
Hai Dang's avatar
Hai Dang committed
124
125
Proof.
  intros r_f. rewrite cmra_assoc.
Hai Dang's avatar
Hai Dang committed
126
127
128
129
130
  intros (WFS & WFT & VALID & PINV & CINV & SREL).
  have Hrf: (r_f  r  res_loc l [s] t).(rtm) !! t 
    Some (to_tgkR tkLocal, to_hplR (write_hpl l [s] )).
  { move : (proj1 VALID t).
    rewrite lookup_op res_tag_lookup.
Hai Dang's avatar
Hai Dang committed
131
    intros Eq%exclusive_Some_r. by rewrite Eq left_id. apply _. }
Hai Dang's avatar
Hai Dang committed
132
133
134
135
136
  specialize (PINV _ _ _ Hrf) as [? PINV]. destruct s as [ss st].
  specialize (PINV l ss st) as (Eq1 & Eq2 & PO); [|done|].
  { by rewrite lookup_fmap /= lookup_insert. }
  simpl in PO.
  rewrite /tag_on_top PO /=. by eexists.
Hai Dang's avatar
Hai Dang committed
137
138
Qed.

Hai Dang's avatar
Hai Dang committed
139
Lemma sim_body_copy_local_r fs ft r r' n l t ty ss st es σs σt Φ :
Ralf Jung's avatar
Ralf Jung committed
140
  tsize ty = 1%nat 
Hai Dang's avatar
Hai Dang committed
141
  r  r'  res_loc l [(ss, st)] t 
Hai Dang's avatar
Hai Dang committed
142
  (r {n,fs,ft} (es, σs)  (#[st], σt) : Φ) 
Ralf Jung's avatar
Ralf Jung committed
143
  r {S n,fs,ft}
Hai Dang's avatar
Hai Dang committed
144
    (es, σs)  (Copy (Place l (Tagged t) ty), σt)
Ralf Jung's avatar
Ralf Jung committed
145
146
  : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
147
148
  intros Hty Hr. rewrite Hr. intros CONT.
  eapply viewshiftP_sim_local_body; [apply vsP_res_mapsto_tag_on_top|].
Hai Dang's avatar
Hai Dang committed
149
150
151
152
  simpl. intros TOP. move : CONT.
  eapply (sim_body_copy_local_unique_r _ _ _ r'); [by left|..] ; eauto.
  - by instantiate (1:= (write_hpl l [(ss, st)] )).
  - by rewrite lookup_insert.
Hai Dang's avatar
Hai Dang committed
153
Qed.
Ralf Jung's avatar
Ralf Jung committed
154

Ralf Jung's avatar
Ralf Jung committed
155
End right.