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

12
13
14
15
16
17
18
19
20
21
22
Definition fun_post_simple initial_call_id_stack (r: resUR) (n: nat) vs css vt cst :=
  ( c, cst = c::initial_call_id_stack) 
  end_call_sat r (mkState   css 0 0) (mkState   cst 0 0) 
  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
62
63
64
65
66
67
68
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.
  eapply sim_simplify; last by eapply HH.
  intros ?????? (Hhead & Hend & Hrel). split; first done.
  split; last done.
  (* Currently [end_call_sat] still looks at the state, but we should be able to fix that. *)
  admit.
Admitted.

Ralf Jung's avatar
Ralf Jung committed
69
70
71
72
73
74
75
76
77
78
79
80
81
82
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.

83
84
85
86
87
88
89
90
91
92
93
94
95
96
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
97
(** * Administrative *)
98
99
100
101
102
103
104
105
106
107
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
108
109
110
111
112
113
114
115
116
117
118
119
(* [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 Φ :
  Forall2 (vrel rv) vls vlt 
  r  r'  rv 
  ( r' vs vt, vrel r' vs vt 
    r  r' ⊨ˢ{n',fs,ft} (Val vs, css)  (Val vt, cst) : Φ) 
  r ⊨ˢ{n,fs,ft}
    (Call #[ScFnPtr fid] (Val <$> vls), css)  (Call #[ScFnPtr fid] (Val <$> vlt), cst) : Φ.
Proof.
Admitted.

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

130
131
132
133
134
135
136
137
138
Lemma sim_simple_write_local fs ft r r' n l tg Ts Tt v v' css cst Φ :
  r  r'  res_mapsto l v' (init_stack (Tagged tg)) 
  ( s, v = [s]  Φ (r'  res_mapsto l s (init_stack (Tagged tg))) n (ValR [%S]) css (ValR [%S]) cst) 
  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
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
Lemma sim_simple_retag_local fs ft r r' r'' rf n l s' s tg m ty css cst Φ :
  r  r'  res_mapsto l s (init_stack (Tagged tg)) 
  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 
    Φ (r'  res_mapsto l s (init_stack (Tagged tg))  res_tag tg_inner tk hplt) n (ValR [%S]) css (ValR [%S]) cst) 
  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
159
160
(** * Pure *)
Lemma sim_simple_let_val fs ft r n x (vs1 vt1: value) es2 et2 css cst Φ :
161
  r ⊨ˢ{n,fs,ft} (subst' x vs1 es2, css)  (subst' x vt1 et2, cst) : Φ 
Ralf Jung's avatar
Ralf Jung committed
162
163
164
165
  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 Φ :
166
  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
167
168
169
  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.

170
End simple.