simple.v 7.14 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
From stbor.sim Require Import body instance refl_step.
11

Hai Dang's avatar
Hai Dang committed
12
13
14
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) 
15
16
17
18
19
20
21
22
  vrel_res r vs vt.

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
23
Notation "r ⊨ˢ{ n , fs , ft } ( es , css ) ≥ ( et , cst ) : Φ" :=
24
  (sim_simple fs ft r n%nat es%E css et%E cst Φ)
25
  (at level 70, es, et at next level,
26
27
   format "'[hv' r  '/' ⊨ˢ{ n , fs , ft }  '/  ' '[ ' ( es ,  css ) ']'  '/' ≥  '/  ' '[ ' ( et ,  cst ) ']'  '/' :  Φ ']'").

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

31
32
33
34
35
36
37
38
39
(* 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
40
  intros HΦ HH. eapply sim_local_body_post_mono; last exact: HH.
41
42
  apply HΦ.
Qed.
43

44
45
46
(** Simple proof for a function taking one argument. *)
(* TODO: make the two call stacks the same. *)
Lemma sim_fun_simple1 n fs ft (esf etf: function) :
47
48
  length (esf.(fun_b)) = 1%nat 
  length (etf.(fun_b)) = 1%nat 
49
50
51
52
53
  ( rf es css et cst vs vt,
    vrel rf vs vt 
    subst_l (esf.(fun_b)) [Val vs] (esf.(fun_e)) = Some es 
    subst_l (etf.(fun_b)) [Val vt] (etf.(fun_e)) = Some et 
    rf ⊨ˢ{n,fs,ft} (InitCall es, css)  (InitCall et, cst) : fun_post_simple cst) 
54
  ⊨ᶠ{fs,ft} esf  etf.
55
56
57
58
59
60
61
Proof.
  intros Hls Hlt HH rf es et vls vlt σs σt FREL SUBSTs SUBSTt. exists n.
  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].
  inversion FREL. intros _ _. simplify_eq.
Hai Dang's avatar
Hai Dang committed
62
63
  eapply sim_simplify; last by eapply HH. done.
Qed.
64

Ralf Jung's avatar
Ralf Jung committed
65
66
67
68
69
70
71
72
73
74
75
76
77
78
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.

79
80
81
82
83
84
85
86
87
88
89
90
91
92
Lemma sim_simple_val fs ft r n (vs vt: value) css cst Φ :
  Φ r n vs css vt cst 
  r ⊨ˢ{S n,fs,ft} (vs, css)  (vt, cst) : Φ.
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 
  r ⊨ˢ{S n,fs,ft} (Place ls ts tys, css)  (Place lt tt tyt, cst) : Φ.
Proof.
  intros HH σs σt <-<-. eapply (sim_body_result _ _ _ _ (PlaceR _ _ _) (PlaceR _ _ _)). done.
Qed.

Ralf Jung's avatar
Ralf Jung committed
93
(** * Administrative *)
94
95
96
97
98
99
100
101
102
103
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
104
105
106
(* [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 Φ :
107
  sim_local_funs_lookup fs ft 
Ralf Jung's avatar
Ralf Jung committed
108
109
  Forall2 (vrel rv) vls vlt 
  r  r'  rv 
Ralf Jung's avatar
Ralf Jung committed
110
111
  ( rret vs vt, vrel rret vs vt 
    r'  rret ⊨ˢ{n',fs,ft} (Val vs, css)  (Val vt, cst) : Φ) 
Ralf Jung's avatar
Ralf Jung committed
112
113
114
  r ⊨ˢ{n,fs,ft}
    (Call #[ScFnPtr fid] (Val <$> vls), css)  (Call #[ScFnPtr fid] (Val <$> vlt), cst) : Φ.
Proof.
Hai Dang's avatar
Hai Dang committed
115
  intros Hfns Hrel Hres HH σs σt <-<-.
Ralf Jung's avatar
Ralf Jung committed
116
117
118
  eapply sim_body_res_proper; last apply: sim_body_step_over_call.
  - symmetry. exact: Hres.
  - done.
Hai Dang's avatar
Hai Dang committed
119
  - done.
Ralf Jung's avatar
Ralf Jung committed
120
  - intros. exists n'. eapply sim_body_res_proper; last apply: HH; try done.
Hai Dang's avatar
Hai Dang committed
121
Qed.
Ralf Jung's avatar
Ralf Jung committed
122

Ralf Jung's avatar
Ralf Jung committed
123
(** * Memory *)
124
Lemma sim_simple_alloc_local fs ft r n T css cst Φ :
125
  ( (l: loc) (tg: nat),
Ralf Jung's avatar
Ralf Jung committed
126
    let r' := res_mapsto l (tsize T)  (init_stack (Tagged tg)) in
127
    Φ (r  r') n (PlaceR l (Tagged tg) T) css (PlaceR l (Tagged tg) T) cst) 
128
129
  r ⊨ˢ{n,fs,ft} (Alloc T, css)  (Alloc T, cst) : Φ.
Proof.
Ralf Jung's avatar
Ralf Jung committed
130
  intros HH σs σt <-<-. apply sim_body_alloc_local=>/=. exact: HH.
131
132
Qed.

133
Lemma sim_simple_write_local fs ft r r' n l tg Ts Tt v v' css cst Φ :
Ralf Jung's avatar
Ralf Jung committed
134
135
  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) 
136
137
138
139
140
141
  r ⊨ˢ{n,fs,ft}
    (Place l (Tagged tg) Ts <- #v, css)  (Place l (Tagged tg) Tt <- #v, cst)
  : Φ.
Proof.
Admitted.

Ralf Jung's avatar
Ralf Jung committed
142
Lemma sim_simple_retag_local fs ft r r' r'' rf n l s' s tg m ty css cst Φ :
Ralf Jung's avatar
Ralf Jung committed
143
  r  r'  res_mapsto l 1 s (init_stack (Tagged tg)) 
Ralf Jung's avatar
Ralf Jung committed
144
145
146
147
148
149
150
151
152
  arel rf s' s 
  r'  r''  rf 
  ( l_inner tg_inner hplt,
    let s := ScPtr l_inner (Tagged tg_inner) in
    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
153
    Φ (r'  res_mapsto l 1 s (init_stack (Tagged tg))  res_tag tg_inner tk hplt) n (ValR [%S]) css (ValR [%S]) cst) 
Ralf Jung's avatar
Ralf Jung committed
154
155
156
157
158
159
160
161
  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
162
163
(** * Pure *)
Lemma sim_simple_let_val fs ft r n x (vs1 vt1: value) es2 et2 css cst Φ :
164
  r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css)  (subst' x vt1 et2, cst) : Φ 
Ralf Jung's avatar
Ralf Jung committed
165
166
167
168
  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 Φ :
169
  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
170
171
172
  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.

173
End simple.