simple.v 11.1 KB
Newer Older
1
2
(** A simpler simulation relation that hides most of the physical state,
except for the call ID stack.
3
4
5
Useful whenever the resources we own are strong enough to carry us from step to step.

When your goal is simple, to make it stateful just do [intros σs σt].
6
To go the other direction, [apply sim_simplify NEW_POST]. Then you will likely
7
8
9
want to clean some stuff from your context.
*)

Ralf Jung's avatar
Ralf Jung committed
10
11
From stbor.sim Require Export body instance.
From stbor.sim Require Import refl_step.
12

Hai Dang's avatar
Hai Dang committed
13
14
15
Definition fun_post_simple
  initial_call_id_stack (r: resUR) (n: nat) vs (css: call_id_stack) vt cst :=
  ( c, cst = c::initial_call_id_stack  end_call_sat r c) 
16
  rrel vrel r vs vt.
17
18
19
20
21
22
23

Definition sim_simple fs ft r n es css et cst
  (Φ : resUR  nat  result  call_id_stack  result  call_id_stack  Prop) : Prop :=
   σs σt, σs.(scs) = css  σt.(scs) = cst 
    r { n , fs , ft } ( es , σs )  ( et , σt ) :
    (λ r n vs' σs' vt' σt', Φ r n vs' σs'.(scs) vt' σt'.(scs)).

Ralf Jung's avatar
Ralf Jung committed
24
Notation "r ⊨ˢ{ n , fs , ft } ( es , css ) ≥ ( et , cst ) : Φ" :=
25
  (sim_simple fs ft r n%nat es%E css et%E cst Φ)
26
  (at level 70, es, et at next level,
27
28
   format "'[hv' r  '/' ⊨ˢ{ n , fs , ft }  '/  ' '[ ' ( es ,  css ) ']'  '/' ≥  '/  ' '[ ' ( et ,  cst ) ']'  '/' :  Φ ']'").

Ralf Jung's avatar
Ralf Jung committed
29
30
31
Section simple.
Implicit Types Φ: resUR  nat  result  call_id_stack  result  call_id_stack  Prop.

32
33
34
35
36
37
38
39
40
(* FIXME: does this [apply]? *)
Lemma sim_simplify
  (Φnew: resUR  nat  result  call_id_stack  result  call_id_stack  Prop)
  (Φ: resUR  nat  result  state  result  state  Prop)
  r n fs ft es σs et σt :
  ( r n vs σs vt σt, Φnew r n vs σs.(scs) vt σt.(scs)  Φ r n vs σs vt σt) 
  r ⊨ˢ{ n , fs , ft } (es, σs.(scs))  (et, σt.(scs)) : Φnew 
  r { n , fs , ft } (es, σs)  (et, σt) : Φ.
Proof.
Ralf Jung's avatar
Ralf Jung committed
41
  intros HΦ HH. eapply sim_local_body_post_mono; last exact: HH.
42
43
  apply HΦ.
Qed.
44
45
46
47
48
49
50
51
52
53
54
55
Lemma sim_simplify'
  (Φnew: resUR  nat  result  call_id_stack  result  call_id_stack  Prop)
  (Φ: resUR  nat  result  state  result  state  Prop)
  r n fs ft es σs et σt css cst :
  ( r n vs σs vt σt, Φnew r n vs σs.(scs) vt σt.(scs)  Φ r n vs σs vt σt) 
  σs.(scs) = css 
  σt.(scs) = cst 
  r ⊨ˢ{ n , fs , ft } (es, css)  (et, cst) : Φnew 
  r { n , fs , ft } (es, σs)  (et, σt) : Φ.
Proof.
  intros HΦ <-<-. eapply sim_simplify. done.
Qed.
56

Ralf Jung's avatar
Ralf Jung committed
57
58
59
60
61
62
63
64
65
Lemma sim_simple_frame_core Φ r n fs ft es css et cst :
  r ⊨ˢ{ n , fs , ft }
    (es, css)  (et, cst)
  : (λ r' n' es' css' et' cst', Φ (core r  r') n' es' css' et' cst') 
  r ⊨ˢ{ n , fs , ft } (es, css)  (et, cst) : Φ.
Proof.
  intros Hold σs σt <-<-. eapply sim_body_frame_core. auto.
Qed.

Ralf Jung's avatar
Ralf Jung committed
66
67
68
69
70
71
72
73
74
75
Lemma sim_simple_post_mono Φ1 Φ2 r n fs ft es css et cst :
  Φ1 <6= Φ2 
  r ⊨ˢ{ n , fs , ft } (es, css)  (et, cst) : Φ1 
  r ⊨ˢ{ n , fs , ft } (es, css)  (et, cst) : Φ2.
Proof.
  intros HΦ Hold σs σt <-<-.
  eapply sim_local_body_post_mono; last exact: Hold.
  auto.
Qed.

Ralf Jung's avatar
Ralf Jung committed
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
Lemma sim_simple_valid_pre fs ft r n es css et cst Φ :
  (valid r  r ⊨ˢ{n,fs,ft} (es, css)  (et, cst) : Φ) 
  r ⊨ˢ{n,fs,ft} (es, css)  (et, cst) : Φ.
Proof.
  intros Hold σs σt <-<-.
  eapply sim_body_valid=>Hval.
  eapply sim_local_body_post_mono, Hold; done.
Qed.

Lemma sim_simple_valid_post fs ft r n es css et cst Φ :
  (r ⊨ˢ{n,fs,ft}
    (es, css)  (et, cst)
  : (λ r' n' es' css' et' cst', valid r'  Φ r' n' es' css' et' cst')) 
  r ⊨ˢ{n,fs,ft} (es, css)  (et, cst) : Φ.
Proof.
  intros Hold σs σt <-<-.
  eapply sim_body_valid=>Hval.
  eapply sim_local_body_post_mono, Hold; done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
96
97
98
99
100
101
102
103
Lemma sim_simple_viewshift r2 r1 fs ft n es css et cst Φ :
  r1 |==> r2 
  r2 ⊨ˢ{n,fs,ft} (es, css)  (et, cst) : Φ 
  r1 ⊨ˢ{n,fs,ft} (es, css)  (et, cst) : Φ.
Proof.
  intros Hvs Hold σs σt <-<-. eapply viewshift_sim_local_body, Hold; done.
Qed.

104
(** Simple proof for a function taking one argument. *)
Ralf Jung's avatar
Ralf Jung committed
105
(* TODO: make the two call stacks the same? *)
Ralf Jung's avatar
Ralf Jung committed
106
Lemma sim_fun_simple1 n (esf etf: function) :
Ralf Jung's avatar
Ralf Jung committed
107
108
  length (esf.(fun_args)) = 1%nat 
  length (etf.(fun_args)) = 1%nat 
Ralf Jung's avatar
Ralf Jung committed
109
110
  ( fs ft rf es css et cst vs vt,
    sim_local_funs_lookup fs ft 
111
    vrel rf vs vt 
Ralf Jung's avatar
Ralf Jung committed
112
113
    subst_l (esf.(fun_args)) [Val vs] (esf.(fun_body)) = Some es 
    subst_l (etf.(fun_args)) [Val vt] (etf.(fun_body)) = Some et 
114
    rf ⊨ˢ{n,fs,ft} (InitCall es, css)  (InitCall et, cst) : fun_post_simple cst) 
Ralf Jung's avatar
Ralf Jung committed
115
  ⊨ᶠ esf  etf.
116
Proof.
Ralf Jung's avatar
Ralf Jung committed
117
  intros Hls Hlt HH fs ft Hlook rf es et vls vlt σs σt FREL SUBSTs SUBSTt. exists n.
118
119
120
121
  move:(subst_l_is_Some_length _ _ _ _ SUBSTs) (subst_l_is_Some_length _ _ _ _ SUBSTt).
  rewrite Hls Hlt.
  destruct vls as [|vs []]; [done| |done].
  destruct vlt as [|vt []]; [done| |done].
122
  inversion FREL as [|???? RREL]. intros _ _. simplify_eq.
123
124
  eapply sim_simplify; last by eapply HH. done.
Qed.
125

Ralf Jung's avatar
Ralf Jung committed
126
127
128
129
130
131
132
133
134
135
136
137
138
139
Lemma sim_simple_bind fs ft
  (Ks: list (ectxi_language.ectx_item (bor_ectxi_lang fs)))
  (Kt: list (ectxi_language.ectx_item (bor_ectxi_lang ft)))
  es et r n css cst Φ :
  r ⊨ˢ{n,fs,ft} (es, css)  (et, cst)
    : (λ r' n' es' css' et' cst',
        r' ⊨ˢ{n',fs,ft} (fill Ks es', css')  (fill Kt et', cst') : Φ) 
  r ⊨ˢ{n,fs,ft} (fill Ks es, css)  (fill Kt et, cst) : Φ.
Proof.
  intros HH σs σt <-<-. apply sim_body_bind.
  eapply sim_local_body_post_mono; last exact: HH.
  clear. simpl. intros r n vs σs vt σt HH. exact: HH.
Qed.

140
141
Lemma sim_simple_val fs ft r n (vs vt: value) css cst Φ :
  Φ r n vs css vt cst 
Hai Dang's avatar
Hai Dang committed
142
  r ⊨ˢ{n,fs,ft} (vs, css)  (vt, cst) : Φ.
143
144
145
146
147
148
Proof.
  intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ vs vt). done.
Qed.

Lemma sim_simple_place fs ft r n ls lt ts tt tys tyt css cst Φ :
  Φ r n (PlaceR ls ts tys) css (PlaceR lt tt tyt) cst 
Hai Dang's avatar
Hai Dang committed
149
  r ⊨ˢ{n,fs,ft} (Place ls ts tys, css)  (Place lt tt tyt, cst) : Φ.
150
151
152
153
Proof.
  intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)). done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
154
(** * Administrative *)
155
156
157
158
159
160
161
162
163
164
Lemma sim_simple_init_call fs ft r n es css et cst Φ :
  ( c: call_id,
    let r' := res_callState c (csOwned ) in
    r  r' ⊨ˢ{n,fs,ft} (es, c::cst)  (et, c::cst) : Φ) 
  r ⊨ˢ{n,fs,ft} (InitCall es, css)  (InitCall et, cst) : Φ.
Proof.
  intros HH σs σt <-<-. apply sim_body_init_call=>/= ?.
  apply HH; done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
165
166
(* [Val <$> _] in the goal makes this not work with [apply], but
we'd need tactic support for anything better. *)
167
Lemma sim_simple_call n' rls rlt rv fs ft r r' n fid css cst Φ :
168
  sim_local_funs_lookup fs ft 
169
  Forall2 (rrel vrel rv) rls rlt 
Ralf Jung's avatar
Ralf Jung committed
170
  r  r'  rv 
171
172
173
174
  ( rret vs vt vls vlt,
    rls = ValR <$> vls  rlt = ValR <$> vlt 
    vrel rret vs vt 
    r'  rret ⊨ˢ{n',fs,ft} (Val vs, css)  (Val vt, cst) : Φ) 
Ralf Jung's avatar
Ralf Jung committed
175
  r ⊨ˢ{n,fs,ft}
176
    (Call #[ScFnPtr fid] (of_result <$> rls), css)  (Call #[ScFnPtr fid] (of_result <$> rlt), cst) : Φ.
Ralf Jung's avatar
Ralf Jung committed
177
Proof.
Ralf Jung's avatar
Ralf Jung committed
178
179
  intros Hfns Hrel Hres HH σs σt <-<-. rewrite Hres.
  apply: sim_body_step_over_call.
Ralf Jung's avatar
Ralf Jung committed
180
  - done.
Hai Dang's avatar
Hai Dang committed
181
  - done.
Ralf Jung's avatar
Ralf Jung committed
182
  - intros. exists n'. eapply sim_body_res_proper; last apply: HH; try done.
Hai Dang's avatar
Hai Dang committed
183
Qed.
Ralf Jung's avatar
Ralf Jung committed
184

Ralf Jung's avatar
Ralf Jung committed
185
(** * Memory *)
186
Lemma sim_simple_alloc_local fs ft r n T css cst Φ :
187
  ( (l: loc) (tg: nat),
Ralf Jung's avatar
Ralf Jung committed
188
    let r' := res_mapsto l (tsize T)  (init_stack (Tagged tg)) in
189
    Φ (r  r') n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst) 
190
191
  r ⊨ˢ{n,fs,ft} (Alloc T, css)  (Alloc T, cst) : Φ.
Proof.
Ralf Jung's avatar
Ralf Jung committed
192
  intros HH σs σt <-<-. apply sim_body_alloc_local=>/=. exact: HH.
193
194
Qed.

Ralf Jung's avatar
Ralf Jung committed
195
196
Lemma sim_simple_write_local fs ft r r' n l tg ty v v' css cst Φ :
  tsize ty = 1%nat 
Ralf Jung's avatar
Ralf Jung committed
197
198
  r  r'  res_mapsto l 1 v' (init_stack (Tagged tg)) 
  ( s, v = [s]  Φ (r'  res_mapsto l 1 s (init_stack (Tagged tg))) n (ValR [%S]) css (ValR [%S]) cst) 
199
  r ⊨ˢ{n,fs,ft}
Ralf Jung's avatar
Ralf Jung committed
200
    (Place l (Tagged tg) ty <- #v, css)  (Place l (Tagged tg) ty <- #v, cst)
201
  : Φ.
Hai Dang's avatar
Hai Dang committed
202
Proof. intros Hty Hres HH σs σt <-<-. eapply sim_body_write_local_1; eauto. Qed.
203

Ralf Jung's avatar
Ralf Jung committed
204
Lemma sim_simple_retag_local fs ft r r' r'' rs n l s' s tg m ty css cst Φ :
Ralf Jung's avatar
Ralf Jung committed
205
  r  r'  res_mapsto l 1 s (init_stack (Tagged tg)) 
Ralf Jung's avatar
Ralf Jung committed
206
207
  arel rs s' s 
  r'  r''  rs 
Ralf Jung's avatar
Ralf Jung committed
208
  ( l_inner tg_inner hplt,
Ralf Jung's avatar
Ralf Jung committed
209
    let s_new := ScPtr l_inner (Tagged tg_inner) in
Ralf Jung's avatar
Ralf Jung committed
210
211
212
213
214
    let tk := match m with Mutable => tkUnique | Immutable => tkPub end in
    match m with 
    | Mutable => is_Some (hplt !! l_inner)
    | Immutable => if is_freeze ty then is_Some (hplt !! l_inner) else True
    end 
Ralf Jung's avatar
Ralf Jung committed
215
    Φ (r''  rs  res_mapsto l 1 s_new (init_stack (Tagged tg))  res_tag tg_inner tk hplt) n (ValR [%S]) css (ValR [%S]) cst) 
Ralf Jung's avatar
Ralf Jung committed
216
217
218
219
220
221
222
223
  r ⊨ˢ{n,fs,ft}
    (Retag (Place l (Tagged tg) (Reference (RefPtr m) ty)) Default, css)
  
    (Retag (Place l (Tagged tg) (Reference (RefPtr m) ty)) Default, cst)
  : Φ.
Proof.
Admitted.

Ralf Jung's avatar
Ralf Jung committed
224
(** * Pure *)
Ralf Jung's avatar
Ralf Jung committed
225
226
227
228
229
230
Lemma sim_simple_let fs ft r n x (vs1 vt1: expr) es2 et2 css cst Φ :
  terminal vs1  terminal vt1 
  r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css)  (subst' x vt1 et2, cst) : Φ 
  r ⊨ˢ{n,fs,ft} (let: x := vs1 in es2, css)  ((let: x := vt1 in et2), cst) : Φ.
Proof. intros ?? HH σs σt <-<-. apply sim_body_let; eauto. Qed.

Ralf Jung's avatar
Ralf Jung committed
231
Lemma sim_simple_let_val fs ft r n x (vs1 vt1: value) es2 et2 css cst Φ :
232
  r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css)  (subst' x vt1 et2, cst) : Φ 
Ralf Jung's avatar
Ralf Jung committed
233
234
235
236
  r ⊨ˢ{n,fs,ft} (let: x := vs1 in es2, css)  ((let: x := vt1 in et2), cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_let; eauto. Qed.

Lemma sim_simple_let_place fs ft r n x ls lt ts tt tys tyt es2 et2 css cst Φ :
237
  r ⊨ˢ{n,fs,ft} (subst' x (Place ls ts tys) es2, css)  (subst' x (Place lt tt tyt) et2, cst) : Φ 
Ralf Jung's avatar
Ralf Jung committed
238
239
240
  r ⊨ˢ{n,fs,ft} (let: x := Place ls ts tys in es2, css)  ((let: x := Place lt tt tyt in et2), cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_let; eauto. Qed.

Hai Dang's avatar
Hai Dang committed
241
242
243
244
Lemma sim_simple_ref fs ft r n (pl: result) css cst Φ :
  ( l t T, pl = PlaceR l t T 
    Φ r n (ValR [ScPtr l t]) css (ValR [ScPtr l t]) cst) 
  r ⊨ˢ{n,fs,ft} ((& pl)%E, css)  ((& pl)%E, cst) : Φ.
Ralf Jung's avatar
Ralf Jung committed
245
246
Proof. intros HH σs σt <-<-. apply sim_body_ref; eauto. Qed.

Hai Dang's avatar
Hai Dang committed
247
248
249
250
251
Lemma sim_simple_deref fs ft r n (rf: result) T css cst Φ :
  ( l t, rf = ValR [ScPtr l t] 
    Φ r n (PlaceR l t T) css (PlaceR l t T) cst) 
  r ⊨ˢ{n,fs,ft} (Deref rf T, css)  (Deref rf T, cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_deref; eauto. Qed.
Ralf Jung's avatar
Ralf Jung committed
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269

Lemma sim_simple_var fs ft r n css cst var Φ :
  r ⊨ˢ{n,fs,ft} (Var var, css)  (Var var, cst) : Φ.
Proof. intros σs σt <-<-. apply sim_body_var; eauto. Qed.

Lemma sim_simple_proj fs ft r n (v i: result) css cst Φ :
  ( vi vv iv, v = ValR vv  i = ValR [ScInt iv] 
    vv !! (Z.to_nat iv) = Some vi  0  iv 
    Φ r n (ValR [vi]) css (ValR [vi]) cst) 
  r ⊨ˢ{n,fs,ft} (Proj v i, css)  (Proj v i, cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_proj; eauto. Qed.

Lemma sim_simple_conc fs ft r n (r1 r2: result) css cst Φ :
  ( v1 v2, r1 = ValR v1  r2 = ValR v2 
    Φ r n (ValR (v1 ++ v2)) css (ValR (v1 ++ v2)) cst) 
  r ⊨ˢ{n,fs,ft} (Conc r1 r2, css)  (Conc r1 r2, cst) : Φ.
Proof. intros HH σs σt <-<-. apply sim_body_conc; eauto. Qed.

270
End simple.