simple.v 7.65 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

Ralf Jung's avatar
Ralf Jung committed
45
46
47
48
49
50
51
52
53
54
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.

55
56
(** Simple proof for a function taking one argument. *)
(* TODO: make the two call stacks the same. *)
Ralf Jung's avatar
Ralf Jung committed
57
Lemma sim_fun_simple1 n (esf etf: function) :
Ralf Jung's avatar
Ralf Jung committed
58
59
  length (esf.(fun_args)) = 1%nat 
  length (etf.(fun_args)) = 1%nat 
Ralf Jung's avatar
Ralf Jung committed
60
61
  ( fs ft rf es css et cst vs vt,
    sim_local_funs_lookup fs ft 
62
    vrel rf vs vt 
Ralf Jung's avatar
Ralf Jung committed
63
64
    subst_l (esf.(fun_args)) [Val vs] (esf.(fun_body)) = Some es 
    subst_l (etf.(fun_args)) [Val vt] (etf.(fun_body)) = Some et 
65
    rf ⊨ˢ{n,fs,ft} (InitCall es, css)  (InitCall et, cst) : fun_post_simple cst) 
Ralf Jung's avatar
Ralf Jung committed
66
  ⊨ᶠ esf  etf.
67
Proof.
Ralf Jung's avatar
Ralf Jung committed
68
  intros Hls Hlt HH fs ft Hlook rf es et vls vlt σs σt FREL SUBSTs SUBSTt. exists n.
69
70
71
72
  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].
73
  inversion FREL as [|???? RREL]. intros _ _. simplify_eq.
74
75
  eapply sim_simplify; last by eapply HH. done.
Qed.
76

Ralf Jung's avatar
Ralf Jung committed
77
78
79
80
81
82
83
84
85
86
87
88
89
90
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.

91
92
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
93
  r ⊨ˢ{n,fs,ft} (vs, css)  (vt, cst) : Φ.
94
95
96
97
98
99
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
100
  r ⊨ˢ{n,fs,ft} (Place ls ts tys, css)  (Place lt tt tyt, cst) : Φ.
101
102
103
104
Proof.
  intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)). done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
105
(** * Administrative *)
106
107
108
109
110
111
112
113
114
115
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
116
117
118
(* [Val <$> _] in the goal makes this not work with [apply], but
we'd need tactic support for anything better. *)
Lemma sim_simple_call n' vls vlt rv fs ft r r' n fid css cst Φ :
119
  sim_local_funs_lookup fs ft 
Ralf Jung's avatar
Ralf Jung committed
120
121
  Forall2 (vrel rv) vls vlt 
  r  r'  rv 
122
  ( rret vs vt, rrel vrel rret vs vt 
123
    r'  rret ⊨ˢ{n',fs,ft} (of_result vs, css)  (of_result vt, cst) : Φ) 
Ralf Jung's avatar
Ralf Jung committed
124
125
126
  r ⊨ˢ{n,fs,ft}
    (Call #[ScFnPtr fid] (Val <$> vls), css)  (Call #[ScFnPtr fid] (Val <$> vlt), cst) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
127
  intros Hfns Hrel Hres HH σs σt <-<-.
Ralf Jung's avatar
Ralf Jung committed
128
129
130
  eapply sim_body_res_proper; last apply: sim_body_step_over_call.
  - symmetry. exact: Hres.
  - done.
Hai Dang's avatar
Hai Dang committed
131
  - done.
Ralf Jung's avatar
Ralf Jung committed
132
  - intros. exists n'. eapply sim_body_res_proper; last apply: HH; try done.
Hai Dang's avatar
Hai Dang committed
133
Qed.
Ralf Jung's avatar
Ralf Jung committed
134

Ralf Jung's avatar
Ralf Jung committed
135
(** * Memory *)
136
Lemma sim_simple_alloc_local fs ft r n T css cst Φ :
137
  ( (l: loc) (tg: nat),
Ralf Jung's avatar
Ralf Jung committed
138
    let r' := res_mapsto l (tsize T)  (init_stack (Tagged tg)) in
139
    Φ (r  r') n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst) 
140
141
  r ⊨ˢ{n,fs,ft} (Alloc T, css)  (Alloc T, cst) : Φ.
Proof.
Ralf Jung's avatar
Ralf Jung committed
142
  intros HH σs σt <-<-. apply sim_body_alloc_local=>/=. exact: HH.
143
144
Qed.

Ralf Jung's avatar
Ralf Jung committed
145
146
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
147
148
  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) 
149
  r ⊨ˢ{n,fs,ft}
Ralf Jung's avatar
Ralf Jung committed
150
    (Place l (Tagged tg) ty <- #v, css)  (Place l (Tagged tg) ty <- #v, cst)
151
  : Φ.
Hai Dang's avatar
Hai Dang committed
152
Proof. intros Hty Hres HH σs σt <-<-. eapply sim_body_write_local_1; eauto. Qed.
153

Ralf Jung's avatar
Ralf Jung committed
154
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
155
  r  r'  res_mapsto l 1 s (init_stack (Tagged tg)) 
Ralf Jung's avatar
Ralf Jung committed
156
157
  arel rs s' s 
  r'  r''  rs 
Ralf Jung's avatar
Ralf Jung committed
158
  ( l_inner tg_inner hplt,
Ralf Jung's avatar
Ralf Jung committed
159
    let s_new := ScPtr l_inner (Tagged tg_inner) in
Ralf Jung's avatar
Ralf Jung committed
160
161
162
163
164
    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
165
    Φ (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
166
167
168
169
170
171
172
173
  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
174
175
(** * Pure *)
Lemma sim_simple_let_val fs ft r n x (vs1 vt1: value) es2 et2 css cst Φ :
176
  r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css)  (subst' x vt1 et2, cst) : Φ 
Ralf Jung's avatar
Ralf Jung committed
177
178
179
180
  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 Φ :
181
  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
182
183
184
  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.

185
End simple.