1 | |
---|
2 | include "Csem.ma". |
---|
3 | |
---|
4 | include "extralib.ma". |
---|
5 | include "IOMonad.ma". |
---|
6 | |
---|
7 | include "Plogic/russell_support.ma". |
---|
8 | |
---|
9 | ndefinition P_to_P_option_res : ∀A:Type[0].∀P:A → CProp[0].option (res A) → CProp[0] ≝ |
---|
10 | λA,P,a.match a with [ None ⇒ False | Some y ⇒ match y return λ_.CProp[0] with [ Error ⇒ True | OK z ⇒ P z ]]. |
---|
11 | |
---|
12 | ndefinition err_inject : ∀A.∀P:A → Prop.∀a:option (res A).∀p:P_to_P_option_res A P a.res (sigma A P) ≝ |
---|
13 | λA.λP:A → Prop.λa:option (res A).λp:P_to_P_option_res A P a. |
---|
14 | (match a return λa'.a=a' → res (sigma A P) with |
---|
15 | [ None ⇒ λe1.? |
---|
16 | | Some b ⇒ λe1.(match b return λb'.b=b' → ? with |
---|
17 | [ Error ⇒ λ_. Error ? |
---|
18 | | OK c ⇒ λe2. OK ? (sig_intro A P c ?) |
---|
19 | ]) (refl ? b) |
---|
20 | ]) (refl ? a). |
---|
21 | ##[ nrewrite > e1 in p; nnormalize; *; |
---|
22 | ##| nrewrite > e1 in p; nrewrite > e2; nnormalize; // |
---|
23 | ##] nqed. |
---|
24 | |
---|
25 | ndefinition err_eject : ∀A.∀P: A → Prop. res (sigma A P) → res A ≝ |
---|
26 | λA,P,a.match a with [ Error ⇒ Error ? | OK b ⇒ |
---|
27 | match b with [ sig_intro w p ⇒ OK ? w] ]. |
---|
28 | |
---|
29 | ndefinition sig_eject : ∀A.∀P: A → Prop. sigma A P → A ≝ |
---|
30 | λA,P,a.match a with [ sig_intro w p ⇒ w]. |
---|
31 | |
---|
32 | ncoercion err_inject : |
---|
33 | ∀A.∀P:A → Prop.∀a.∀p:P_to_P_option_res ? P a.res (sigma A P) ≝ err_inject |
---|
34 | on a:option (res ?) to res (sigma ? ?). |
---|
35 | ncoercion err_eject : ∀A.∀P:A → Prop.∀c:res (sigma A P).res A ≝ err_eject |
---|
36 | on _c:res (sigma ? ?) to res ?. |
---|
37 | ncoercion sig_eject : ∀A.∀P:A → Prop.∀c:sigma A P.A ≝ sig_eject |
---|
38 | on _c:sigma ? ? to ?. |
---|
39 | |
---|
40 | ndefinition P_res: ∀A.∀P:A → Prop.res A → Prop ≝ |
---|
41 | λA,P,a. match a with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
42 | |
---|
43 | ndefinition exec_bool_of_val : ∀v:val. ∀ty:type. res bool ≝ |
---|
44 | λv,ty. match v in val with |
---|
45 | [ Vint i ⇒ match ty with |
---|
46 | [ Tint _ _ ⇒ OK ? (¬eq i zero) |
---|
47 | | Tpointer _ _ ⇒ OK ? (¬eq i zero) |
---|
48 | | _ ⇒ Error ? |
---|
49 | ] |
---|
50 | | Vfloat f ⇒ match ty with |
---|
51 | [ Tfloat _ ⇒ OK ? (¬Fcmp Ceq f Fzero) |
---|
52 | | _ ⇒ Error ? |
---|
53 | ] |
---|
54 | | Vptr _ _ _ ⇒ match ty with |
---|
55 | [ Tint _ _ ⇒ OK ? true |
---|
56 | | Tpointer _ _ ⇒ OK ? true |
---|
57 | | _ ⇒ Error ? |
---|
58 | ] |
---|
59 | | _ ⇒ Error ? |
---|
60 | ]. |
---|
61 | |
---|
62 | nlemma exec_bool_of_val_sound: ∀v,ty,r. |
---|
63 | exec_bool_of_val v ty = OK ? r → bool_of_val v ty (of_bool r). |
---|
64 | #v ty r; |
---|
65 | ncases v; ##[ ##2: #i ##| ##3: #f ##| ##4: #sp b of ##] |
---|
66 | nwhd; ##[ ##4: #H; nwhd in H:(??%?); ndestruct ##] |
---|
67 | ncases ty; ##[ ##2,11,20: #sz sg ##| ##3,12,21: #sz ##| ##4,13,22: #sp ty ##| ##5,14,23: #sp ty n ##| ##6,15,24: #args rty ##| ##7,8,16,17,25,26: #id fs ##| ##9,18,27: #id ##] |
---|
68 | #H; nwhd in H:(??%?); ndestruct; |
---|
69 | ##[ ##1,4: nlapply (eq_spec i zero); nelim (eq i zero); |
---|
70 | ##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //; |
---|
71 | ##| ##2,4: #ne; napply bool_of_val_true; /2/; |
---|
72 | ##] |
---|
73 | ##| ##3: nelim (eq_dec f Fzero); |
---|
74 | ##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //; |
---|
75 | ##| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/; |
---|
76 | ##] |
---|
77 | ##| ##2,5: napply bool_of_val_true; // |
---|
78 | ##] nqed. |
---|
79 | |
---|
80 | nlemma bool_of_val_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ exec_bool_of_val v ty = OK ? b. |
---|
81 | #v ty r H; nelim H; #v t H'; nelim H'; |
---|
82 | ##[ #i is s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //; |
---|
83 | ##| #p b i i0 s; @ true; @; // |
---|
84 | ##| #i p t ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (eq_false … ne); //; |
---|
85 | ##| #p b i p0 t0; @ true; @; // |
---|
86 | ##| #f s ne; @ true; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_false … ne); //; |
---|
87 | ##| #i s; @ false; @; //; |
---|
88 | ##| #p t; @ false; @; //; |
---|
89 | ##| #s; @ false; @; //; nwhd in ⊢ (??%?); nrewrite > (Feq_zero_true …); //; |
---|
90 | ##] |
---|
91 | nqed. |
---|
92 | |
---|
93 | (* Prove a few minor results to make proof obligations easy. *) |
---|
94 | |
---|
95 | nlemma bind_assoc_r: ∀A,B,C,e,f,g. |
---|
96 | bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g). |
---|
97 | #A B C e f g; ncases e; nnormalize; //; nqed. |
---|
98 | |
---|
99 | nlemma bind_OK: ∀A,B,P,e,f. |
---|
100 | (∀v. e = OK A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
101 | match bind A B e f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
102 | #A B P e f; nelim e; /2/; nqed. |
---|
103 | |
---|
104 | nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B. |
---|
105 | (∀v:A. ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True | OK v' ⇒ P' v'] ) → |
---|
106 | match bind (sigma A P) B e f with [ Error ⇒ True | OK v' ⇒ P' v' ]. |
---|
107 | #A B P P' e f; nelim e; |
---|
108 | ##[ #v0; nelim v0; #v Hv IH; napply IH; |
---|
109 | ##| #_; napply I; |
---|
110 | ##] nqed. |
---|
111 | |
---|
112 | nlemma bind2_OK: ∀A,B,C,P,e,f. |
---|
113 | (∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
114 | match bind2 A B C e f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
115 | #A B C P e f; nelim e; //; #v; ncases v; /2/; nqed. |
---|
116 | |
---|
117 | nlemma sig_bind2_OK: ∀A,B,C. ∀P:A×B → Prop. ∀P':C → Prop. ∀e:res (sigma (A×B) P). ∀f:A → B → res C. |
---|
118 | (∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True | OK v' ⇒ P' v'] ) → |
---|
119 | match bind2 A B C e f with [ Error ⇒ True | OK v' ⇒ P' v' ]. |
---|
120 | #A B C P P' e f; nelim e; //; |
---|
121 | #v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed. |
---|
122 | |
---|
123 | nlemma bool_val_distinct: Vtrue ≠ Vfalse. |
---|
124 | @; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero); |
---|
125 | nqed. |
---|
126 | |
---|
127 | nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) → |
---|
128 | if b then is_true v ty else is_false v ty. |
---|
129 | #v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //; |
---|
130 | napply False_ind; napply (absurd ? ev ?); |
---|
131 | ##[ ##2: napply sym_neq ##] napply bool_val_distinct; |
---|
132 | nqed. |
---|
133 | |
---|
134 | ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A | Some v ⇒ OK A v ]. |
---|
135 | nlemma opt_OK: ∀A,P,e. |
---|
136 | (∀v. e = Some ? v → P v) → |
---|
137 | match opt_to_res A e with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
138 | #A P e; nelim e; /2/; |
---|
139 | nqed. |
---|
140 | |
---|
141 | nlemma opt_bind_OK: ∀A,B,P,e,f. |
---|
142 | (∀v. e = Some A v → match f v with [ Error ⇒ True | OK v' ⇒ P v' ]) → |
---|
143 | match bind A B (opt_to_res A e) f with [ Error ⇒ True | OK v ⇒ P v ]. |
---|
144 | #A B P e f; nelim e; nnormalize; /2/; nqed. |
---|
145 | |
---|
146 | nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B | P e}. ∀Q:A→B→res C. ∀R:C→Prop. |
---|
147 | (∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v | Error ⇒ True]) → |
---|
148 | match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v | Error ⇒ True ]. |
---|
149 | #A B C P e Q R; ncases e; #e'; ncases e'; nnormalize; |
---|
150 | ##[ #H; napply (False_ind … H); |
---|
151 | ##| #e''; ncases e''; #a b Pab H; nnormalize; /2/; |
---|
152 | ##] nqed. |
---|
153 | |
---|
154 | (* |
---|
155 | nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B | OK v ⇒ Error B ] = Error B. |
---|
156 | #A B e; ncases e; //; nqed. |
---|
157 | *) |
---|
158 | |
---|
159 | ndefinition try_cast_null : ∀m:mem. ∀i:int. ∀ty:type. ∀ty':type. res val ≝ |
---|
160 | λm:mem. λi:int. λty:type. λty':type. |
---|
161 | match eq i zero with |
---|
162 | [ true ⇒ |
---|
163 | match ty with |
---|
164 | [ Tint _ _ ⇒ |
---|
165 | match ty' with |
---|
166 | [ Tpointer _ _ ⇒ OK ? (Vint i) |
---|
167 | | Tarray _ _ _ ⇒ OK ? (Vint i) |
---|
168 | | Tfunction _ _ ⇒ OK ? (Vint i) |
---|
169 | | _ ⇒ Error ? |
---|
170 | ] |
---|
171 | | Tpointer _ _ ⇒ |
---|
172 | match ty' with |
---|
173 | [ Tpointer _ _ ⇒ OK ? (Vint i) |
---|
174 | | Tarray _ _ _ ⇒ OK ? (Vint i) |
---|
175 | | Tfunction _ _ ⇒ OK ? (Vint i) |
---|
176 | | _ ⇒ Error ? |
---|
177 | ] |
---|
178 | | Tarray _ _ _ ⇒ |
---|
179 | match ty' with |
---|
180 | [ Tpointer _ _ ⇒ OK ? (Vint i) |
---|
181 | | Tarray _ _ _ ⇒ OK ? (Vint i) |
---|
182 | | Tfunction _ _ ⇒ OK ? (Vint i) |
---|
183 | | _ ⇒ Error ? |
---|
184 | ] |
---|
185 | | Tfunction _ _ ⇒ |
---|
186 | match ty' with |
---|
187 | [ Tpointer _ _ ⇒ OK ? (Vint i) |
---|
188 | | Tarray _ _ _ ⇒ OK ? (Vint i) |
---|
189 | | Tfunction _ _ ⇒ OK ? (Vint i) |
---|
190 | | _ ⇒ Error ? |
---|
191 | ] |
---|
192 | | _ ⇒ Error ? |
---|
193 | ] |
---|
194 | | false ⇒ Error ? |
---|
195 | ]. |
---|
196 | |
---|
197 | nlemma try_cast_null_sound: ∀m,i,ty,ty',v'. try_cast_null m i ty ty' = OK ? v' → cast m (Vint i) ty ty' v'. |
---|
198 | #m i ty ty' v'; |
---|
199 | nwhd in ⊢ (??%? → ?); |
---|
200 | nlapply (eq_spec i zero); ncases (eq i zero); |
---|
201 | ##[ #e; nrewrite > e; |
---|
202 | ncases ty; ##[ ##| #sz sg ##| #fs ##| #sp ty ##| #sp ty n ##| #args rty ##| #id fs ##| #id fs ##| #id ##] |
---|
203 | nwhd in ⊢ (??%? → ?); ##[ ##1,3,7,8,9: #H; ndestruct ##] |
---|
204 | ncases ty'; ##[ ##2,11,20,29: #sz' sg' ##| ##3,12,21,30: #sz' ##| ##4,13,22,31: #sp' ty' ##| ##5,14,23,32: #sp' ty' n' ##| ##6,15,24,33: #args' res' ##| ##7,8,16,17,25,26,34,35: #id' fs' ##| ##9,18,27,36: #id' ##] |
---|
205 | nwhd in ⊢ (??%? → ?); #H; ndestruct (H); |
---|
206 | ##[ ##1,5,9: napply cast_ip_z ##| ##*: napply cast_pp_z ##] //; |
---|
207 | ##| #_; nwhd in ⊢ (??%? → ?); #H; ndestruct |
---|
208 | ##] |
---|
209 | nqed. |
---|
210 | |
---|
211 | ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2). |
---|
212 | #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. |
---|
213 | |
---|
214 | ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res val ≝ |
---|
215 | λm:mem. λv:val. λty:type. λty':type. |
---|
216 | match v with |
---|
217 | [ Vint i ⇒ |
---|
218 | match ty with |
---|
219 | [ Tint sz1 si1 ⇒ |
---|
220 | match ty' with |
---|
221 | [ Tint sz2 si2 ⇒ OK ? (Vint (cast_int_int sz2 si2 i)) |
---|
222 | | Tfloat sz2 ⇒ OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))) |
---|
223 | | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r |
---|
224 | | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r |
---|
225 | | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r |
---|
226 | | _ ⇒ Error ? |
---|
227 | ] |
---|
228 | | Tpointer _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r |
---|
229 | | Tarray _ _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r |
---|
230 | | Tfunction _ _ ⇒ do r ← try_cast_null m i ty ty'; OK val r |
---|
231 | | _ ⇒ Error ? |
---|
232 | ] |
---|
233 | | Vfloat f ⇒ |
---|
234 | match ty with |
---|
235 | [ Tfloat sz ⇒ |
---|
236 | match ty' with |
---|
237 | [ Tint sz' si' ⇒ OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f))) |
---|
238 | | Tfloat sz' ⇒ OK ? (Vfloat (cast_float_float sz' f)) |
---|
239 | | _ ⇒ Error ? |
---|
240 | ] |
---|
241 | | _ ⇒ Error ? |
---|
242 | ] |
---|
243 | | Vptr p b ofs ⇒ |
---|
244 | do s ← match ty with [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code | _ ⇒ Error ? ]; |
---|
245 | do u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something | inr _ ⇒ Error ? ]; |
---|
246 | do s' ← match ty' with |
---|
247 | [ Tpointer s _ ⇒ OK ? s | Tarray s _ _ ⇒ OK ? s | Tfunction _ _ ⇒ OK ? Code |
---|
248 | | _ ⇒ Error ? ]; |
---|
249 | if is_pointer_compat (block_space m b) s' |
---|
250 | then OK ? (Vptr s' b ofs) |
---|
251 | else Error ? |
---|
252 | | _ ⇒ Error ? |
---|
253 | ]. |
---|
254 | |
---|
255 | ndefinition exec_cast_sound : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. ∀v':val. exec_cast m v ty ty' = OK ? v' → cast m v ty ty' v'. |
---|
256 | #m v ty ty' v'; |
---|
257 | ncases v; |
---|
258 | ##[ #H; nwhd in H:(??%?); ndestruct; |
---|
259 | ##| #i; ncases ty; |
---|
260 | ##[ #H; nwhd in H:(??%?); ndestruct; |
---|
261 | ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct; |
---|
262 | ##| ##7,8: #a b; #H; nwhd in H:(??%?); ndestruct; |
---|
263 | ##| #sz1 si1; ncases ty'; |
---|
264 | ##[ #H; nwhd in H:(??%?); ndestruct; |
---|
265 | ##| ##3,9: #a; #H; nwhd in H:(??%?); ndestruct; // |
---|
266 | ##| ##2,7,8: #a b; #H; nwhd in H:(??%?); ndestruct; // |
---|
267 | ##| ##4,5,6: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'') |
---|
268 | ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n) |
---|
269 | ##| #args rty; nletin t ≝ (Tfunction args rty) ##] |
---|
270 | nwhd in ⊢ (??%? → ?); |
---|
271 | nlapply (try_cast_null_sound m i (Tint sz1 si1) t v'); |
---|
272 | ncases (try_cast_null m i (Tint sz1 si1) t); |
---|
273 | ##[ ##1,3,5: #v''; #H' e; napply H'; napply e; |
---|
274 | ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H); |
---|
275 | ##] |
---|
276 | ##] |
---|
277 | ##| ##*: ##[ #sp ty''; nletin t ≝ (Tpointer sp ty'') |
---|
278 | ##| #sp ty'' n; nletin t ≝ (Tarray sp ty'' n) |
---|
279 | ##| #args rty; nletin t ≝ (Tfunction args rty) ##] |
---|
280 | nwhd in ⊢ (??%? → ?); |
---|
281 | nlapply (try_cast_null_sound m i t ty' v'); |
---|
282 | ncases (try_cast_null m i t ty'); |
---|
283 | ##[ ##1,3,5: #v''; #H' e; napply H'; napply e; |
---|
284 | ##| ##*: #_; nwhd in ⊢ (??%? → ?); #H; ndestruct (H); |
---|
285 | ##] |
---|
286 | ##] |
---|
287 | ##| #f; ncases ty; ##[ ##3,9: #x; ##| ##2,4,6,7,8: #x y; ##| ##5: #x y z; ##] |
---|
288 | ##[ ncases ty'; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##] |
---|
289 | nwhd in e:(??%?); ndestruct; //; |
---|
290 | ##| ##*: #e; nwhd in e:(??%?); ndestruct |
---|
291 | ##] |
---|
292 | ##| #sp b of; nwhd in ⊢ (??%? → ?); #e; |
---|
293 | nelim (bind_inversion ????? e); #s; *; #es e'; |
---|
294 | nelim (bind_inversion ????? e'); #u; *; #eu e''; |
---|
295 | nelim (bind_inversion ????? e''); #s'; *; #es' e'''; |
---|
296 | ncut (type_space ty s); |
---|
297 | ##[ ncases ty in es:(??%?) ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##] |
---|
298 | nwhd in e:(??%?); ndestruct; //; |
---|
299 | ##| #Hty; |
---|
300 | ncut (type_space ty' s'); |
---|
301 | ##[ ncases ty' in es' ⊢ %; ##[ #e; ##| ##3,9: #a e; ##| ##2,4,6,7,8: #a b e; ##| #a b c e; ##] |
---|
302 | nwhd in e:(??%?); ndestruct; //; |
---|
303 | ##| #Hty'; |
---|
304 | ncut (s = sp). nelim (ms_eq_dec sp s) in eu; //; nnormalize; #_; #e; ndestruct. |
---|
305 | #e; nrewrite < e; |
---|
306 | nwhd in match (is_pointer_compat ??) in e'''; |
---|
307 | ncases (pointer_compat_dec (block_space m b) s') in e'''; #Hcompat e'''; |
---|
308 | nwhd in e''':(??%?); ndestruct (e'''); /2/ |
---|
309 | ##] |
---|
310 | ##] |
---|
311 | ##] nqed. |
---|
312 | |
---|
313 | ndefinition load_value_of_type' ≝ |
---|
314 | λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒ |
---|
315 | load_value_of_type ty m psp loc ofs ] ]. |
---|
316 | |
---|
317 | (* To make the evaluation of bare lvalue expressions invoke exec_lvalue with |
---|
318 | a structurally smaller value, we break out the surrounding Expr constructor |
---|
319 | and use exec_lvalue'. *) |
---|
320 | |
---|
321 | nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (val×trace) ≝ |
---|
322 | match e with |
---|
323 | [ Expr e' ty ⇒ |
---|
324 | match e' with |
---|
325 | [ Econst_int i ⇒ OK ? 〈Vint i, E0〉 |
---|
326 | | Econst_float f ⇒ OK ? 〈Vfloat f, E0〉 |
---|
327 | | Evar _ ⇒ |
---|
328 | do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; |
---|
329 | do v ← opt_to_res ? (load_value_of_type' ty m l); |
---|
330 | OK ? 〈v,tr〉 |
---|
331 | | Ederef _ ⇒ |
---|
332 | do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; |
---|
333 | do v ← opt_to_res ? (load_value_of_type' ty m l); |
---|
334 | OK ? 〈v,tr〉 |
---|
335 | | Efield _ _ ⇒ |
---|
336 | do 〈l,tr〉 ← exec_lvalue' ge en m e' ty; |
---|
337 | do v ← opt_to_res ? (load_value_of_type' ty m l); |
---|
338 | OK ? 〈v,tr〉 |
---|
339 | | Eaddrof a ⇒ |
---|
340 | do 〈plo,tr〉 ← exec_lvalue ge en m a; |
---|
341 | OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉 |
---|
342 | | Esizeof ty' ⇒ OK ? 〈Vint (repr (sizeof ty')), E0〉 |
---|
343 | | Eunop op a ⇒ |
---|
344 | do 〈v1,tr〉 ← exec_expr ge en m a; |
---|
345 | do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a)); |
---|
346 | OK ? 〈v,tr〉 |
---|
347 | | Ebinop op a1 a2 ⇒ |
---|
348 | do 〈v1,tr1〉 ← exec_expr ge en m a1; |
---|
349 | do 〈v2,tr2〉 ← exec_expr ge en m a2; |
---|
350 | do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m); |
---|
351 | OK ? 〈v,tr1⧺tr2〉 |
---|
352 | | Econdition a1 a2 a3 ⇒ |
---|
353 | do 〈v,tr1〉 ← exec_expr ge en m a1; |
---|
354 | do b ← exec_bool_of_val v (typeof a1); |
---|
355 | do 〈v',tr2〉 ← match b return λ_.res (val×trace) with |
---|
356 | [ true ⇒ (exec_expr ge en m a2) |
---|
357 | | false ⇒ (exec_expr ge en m a3) ]; |
---|
358 | OK ? 〈v',tr1⧺tr2〉 |
---|
359 | (* if b then exec_expr ge en m a2 else exec_expr ge en m a3)*) |
---|
360 | | Eorbool a1 a2 ⇒ |
---|
361 | do 〈v1,tr1〉 ← exec_expr ge en m a1; |
---|
362 | do b1 ← exec_bool_of_val v1 (typeof a1); |
---|
363 | match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 | false ⇒ |
---|
364 | do 〈v2,tr2〉 ← exec_expr ge en m a2; |
---|
365 | do b2 ← exec_bool_of_val v2 (typeof a2); |
---|
366 | OK ? 〈of_bool b2, tr1⧺tr2〉 ] |
---|
367 | | Eandbool a1 a2 ⇒ |
---|
368 | do 〈v1,tr1〉 ← exec_expr ge en m a1; |
---|
369 | do b1 ← exec_bool_of_val v1 (typeof a1); |
---|
370 | match b1 return λ_.res (val×trace) with [ true ⇒ |
---|
371 | do 〈v2,tr2〉 ← exec_expr ge en m a2; |
---|
372 | do b2 ← exec_bool_of_val v2 (typeof a2); |
---|
373 | OK ? 〈of_bool b2, tr1⧺tr2〉 |
---|
374 | | false ⇒ OK ? 〈Vfalse,tr1〉 ] |
---|
375 | | Ecast ty' a ⇒ |
---|
376 | do 〈v,tr〉 ← exec_expr ge en m a; |
---|
377 | do v' ← exec_cast m v (typeof a) ty'; |
---|
378 | OK ? 〈v',tr〉 |
---|
379 | | Ecost l a ⇒ |
---|
380 | do 〈v,tr〉 ← exec_expr ge en m a; |
---|
381 | OK ? 〈v,tr⧺(Echarge l)〉 |
---|
382 | ] |
---|
383 | ] |
---|
384 | and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (memory_space × block × int × trace) ≝ |
---|
385 | match e' with |
---|
386 | [ Evar id ⇒ |
---|
387 | match (get … id en) with |
---|
388 | [ None ⇒ do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉 (* global *) |
---|
389 | | Some loc ⇒ OK ? 〈〈〈Any,loc〉,zero〉,E0〉 (* local *) |
---|
390 | ] |
---|
391 | | Ederef a ⇒ |
---|
392 | do 〈v,tr〉 ← exec_expr ge en m a; |
---|
393 | match v with |
---|
394 | [ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉 |
---|
395 | | _ ⇒ Error ? |
---|
396 | ] |
---|
397 | | Efield a i ⇒ |
---|
398 | match (typeof a) with |
---|
399 | [ Tstruct id fList ⇒ |
---|
400 | do 〈plofs,tr〉 ← exec_lvalue ge en m a; |
---|
401 | do delta ← field_offset i fList; |
---|
402 | OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉 |
---|
403 | | Tunion id fList ⇒ |
---|
404 | do 〈plofs,tr〉 ← exec_lvalue ge en m a; |
---|
405 | OK ? 〈plofs,tr〉 |
---|
406 | | _ ⇒ Error ? |
---|
407 | ] |
---|
408 | | _ ⇒ Error ? |
---|
409 | ] |
---|
410 | and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (memory_space × block × int × trace) ≝ |
---|
411 | match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ]. |
---|
412 | |
---|
413 | nlemma P_res_to_P: ∀A,P,e,v. P_res A P e → e = OK A v → P v. |
---|
414 | #A P e v H1 H2; nrewrite > H2 in H1; nwhd in ⊢ (% → ?); //; nqed. |
---|
415 | |
---|
416 | (* We define a special induction principle tailored to the recursive definition |
---|
417 | above. *) |
---|
418 | |
---|
419 | ndefinition is_not_lvalue: expr_descr → Prop ≝ |
---|
420 | λe. match e with [ Evar _ ⇒ False | Ederef _ ⇒ False | Efield _ _ ⇒ False | _ ⇒ True ]. |
---|
421 | |
---|
422 | ndefinition Plvalue ≝ λP:(expr → Prop).λe,ty. |
---|
423 | match e return λ_.Prop with [ Evar _ ⇒ P (Expr e ty) | Ederef _ ⇒ P (Expr e ty) | Efield _ _ ⇒ P (Expr e ty) | _ ⇒ True ]. |
---|
424 | |
---|
425 | nlet rec expr_lvalue_ind |
---|
426 | (P:expr → Prop) |
---|
427 | (Q:expr_descr → type → Prop) |
---|
428 | (ci:∀ty,i.P (Expr (Econst_int i) ty)) |
---|
429 | (cf:∀ty,f.P (Expr (Econst_float f) ty)) |
---|
430 | (lv:∀e,ty. Q e ty → Plvalue P e ty) |
---|
431 | (vr:∀v,ty.Q (Evar v) ty) |
---|
432 | (dr:∀e,ty.P e → Q (Ederef e) ty) |
---|
433 | (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty)) |
---|
434 | (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty)) |
---|
435 | (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty)) |
---|
436 | (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty)) |
---|
437 | (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty)) |
---|
438 | (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty)) |
---|
439 | (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty)) |
---|
440 | (sz:∀ty,ty'. P (Expr (Esizeof ty') ty)) |
---|
441 | (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty) |
---|
442 | (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty)) |
---|
443 | (xx:∀e,ty. is_not_lvalue e → Q e ty) |
---|
444 | (e:expr) on e : P e ≝ |
---|
445 | match e with |
---|
446 | [ Expr e' ty ⇒ |
---|
447 | match e' with |
---|
448 | [ Econst_int i ⇒ ci ty i |
---|
449 | | Econst_float f ⇒ cf ty f |
---|
450 | | Evar v ⇒ lv (Evar v) ty (vr v ty) |
---|
451 | | Ederef e'' ⇒ lv (Ederef e'') ty (dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'')) |
---|
452 | | Eaddrof e'' ⇒ match e'' with [ Expr e0 ty0 ⇒ ao ty e0 ty0 (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e0 ty0) ] |
---|
453 | | Eunop op e'' ⇒ uo ty op e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'') |
---|
454 | | Ebinop op e1 e2 ⇒ bo ty op e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) |
---|
455 | | Ecast ty' e'' ⇒ ca ty ty' e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'') |
---|
456 | | Econdition e1 e2 e3 ⇒ cd ty e1 e2 e3 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e3) |
---|
457 | | Eandbool e1 e2 ⇒ ab ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) |
---|
458 | | Eorbool e1 e2 ⇒ ob ty e1 e2 (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e1) (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e2) |
---|
459 | | Esizeof ty' ⇒ sz ty ty' |
---|
460 | | Efield e'' i ⇒ match e'' with [ Expr ef tyf ⇒ lv (Efield (Expr ef tyf) i) ty (fl ty ef tyf i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx ef tyf)) ] |
---|
461 | | Ecost l e'' ⇒ co ty l e'' (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'') |
---|
462 | ] |
---|
463 | ] |
---|
464 | and lvalue_expr_ind |
---|
465 | (P:expr → Prop) |
---|
466 | (Q:expr_descr → type → Prop) |
---|
467 | (ci:∀ty,i.P (Expr (Econst_int i) ty)) |
---|
468 | (cf:∀ty,f.P (Expr (Econst_float f) ty)) |
---|
469 | (lv:∀e,ty. Q e ty → Plvalue P e ty) |
---|
470 | (vr:∀v,ty.Q (Evar v) ty) |
---|
471 | (dr:∀e,ty.P e → Q (Ederef e) ty) |
---|
472 | (ao:∀ty,e,ty'.Q e ty' → P (Expr (Eaddrof (Expr e ty')) ty)) |
---|
473 | (uo:∀ty,op,e.P e → P (Expr (Eunop op e) ty)) |
---|
474 | (bo:∀ty,op,e1,e2.P e1 → P e2 → P (Expr (Ebinop op e1 e2) ty)) |
---|
475 | (ca:∀ty,ty',e.P e → P (Expr (Ecast ty' e) ty)) |
---|
476 | (cd:∀ty,e1,e2,e3.P e1 → P e2 → P e3 → P (Expr (Econdition e1 e2 e3) ty)) |
---|
477 | (ab:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eandbool e1 e2) ty)) |
---|
478 | (ob:∀ty,e1,e2.P e1 → P e2 → P (Expr (Eorbool e1 e2) ty)) |
---|
479 | (sz:∀ty,ty'. P (Expr (Esizeof ty') ty)) |
---|
480 | (fl:∀ty,e,ty',i. Q e ty' → Q (Efield (Expr e ty') i) ty) |
---|
481 | (co:∀ty,l,e. P e → P (Expr (Ecost l e) ty)) |
---|
482 | (xx:∀e,ty. is_not_lvalue e → Q e ty) |
---|
483 | (e:expr_descr) (ty:type) on e : Q e ty ≝ |
---|
484 | match e return λe0. Q e0 ty with |
---|
485 | [ Evar v ⇒ vr v ty |
---|
486 | | Ederef e'' ⇒ dr e'' ty (expr_lvalue_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'') |
---|
487 | | Efield e' i ⇒ match e' return λe1.Q (Efield e1 i) ty with [ Expr e'' ty'' ⇒ fl ty e'' ty'' i (lvalue_expr_ind P Q ci cf lv vr dr ao uo bo ca cd ab ob sz fl co xx e'' ty'') ] |
---|
488 | | _ ⇒ xx ? ty ? |
---|
489 | ]. nwhd; napply I; nqed. |
---|
490 | |
---|
491 | |
---|
492 | ntheorem exec_expr_sound: ∀ge:genv. ∀en:env. ∀m:mem. ∀e:expr. |
---|
493 | (P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e)). |
---|
494 | #ge en m e; napply (expr_lvalue_ind ? (λe',ty.P_res ? (λr.eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue' ge en m e' ty)) … e); |
---|
495 | ##[ ##1,2: #ty c; nwhd; //; |
---|
496 | (* expressions that are lvalues *) |
---|
497 | ##| #e' ty; ncases e'; //; ##[ #i He' ##| #e He' ##| #e i He' ##] nwhd in He' ⊢ %; |
---|
498 | napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H; |
---|
499 | napply opt_bind_OK; #vl evl; nwhd in evl:(??%?); napply (eval_Elvalue … evl); |
---|
500 | nrewrite > H in He'; #He'; napply He'; |
---|
501 | ##| #v ty; |
---|
502 | nwhd in ⊢ (???%); |
---|
503 | nlapply (refl ? (get ident PTree block v en)); |
---|
504 | ncases (get ident PTree block v en) in ⊢ (???% → %); |
---|
505 | ##[ #eget; napply opt_bind_OK; #sploc; ncases sploc; #sp loc efind; |
---|
506 | nwhd; napply (eval_Evar_global … eget efind); |
---|
507 | ##| #loc eget; napply (eval_Evar_local … eget); |
---|
508 | ##] |
---|
509 | ##| #ty e He; nwhd in ⊢ (???%); |
---|
510 | napply bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd; |
---|
511 | napply eval_Ederef; nrewrite > Hv in He; #He; napply He; |
---|
512 | ##| #ty e'' ty'' He''; napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H; |
---|
513 | nwhd; napply eval_Eaddrof; nrewrite > H in He''; #He''; napply He''; |
---|
514 | ##| #ty op e1 He1; napply bind2_OK; #v1 tr Hv1; |
---|
515 | napply opt_bind_OK; #v ev; |
---|
516 | napply (eval_Eunop … ev); |
---|
517 | nrewrite > Hv1 in He1; #He1; napply He1; |
---|
518 | ##| #ty op e1 e2 He1 He2; |
---|
519 | napply bind2_OK; #v1 tr1 ev1; nrewrite > ev1 in He1; #He1; |
---|
520 | napply bind2_OK; #v2 tr2 ev2; nrewrite > ev2 in He2; #He2; |
---|
521 | napply opt_bind_OK; #v ev; nwhd in He1 He2; nwhd; |
---|
522 | napply (eval_Ebinop … He1 He2 ev); |
---|
523 | ##| #ty ty' e' He'; |
---|
524 | napply bind2_OK; #v tr Hv; nrewrite > Hv in He'; #He'; |
---|
525 | napply bind_OK; #v' ev'; |
---|
526 | napply (eval_Ecast … He' ?); |
---|
527 | /2/; |
---|
528 | ##| #ty e1 e2 e3 He1 He2 He3; |
---|
529 | napply bind2_OK; #vb tr1 Hvb; nrewrite > Hvb in He1; #He1; |
---|
530 | napply bind_OK; #b; |
---|
531 | ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb; |
---|
532 | napply bind2_OK; #v tr Hv; |
---|
533 | ##[ nrewrite > Hv in He2; #He2; nwhd in He2 Hv:(??%?) ⊢%; |
---|
534 | napply (eval_Econdition_true … He1 ? He2); napply (bool_of ??? Hb); |
---|
535 | ##| nrewrite > Hv in He3; #He3; nwhd in He3 Hv:(??%?) ⊢%; |
---|
536 | napply (eval_Econdition_false … He1 ? He3); napply (bool_of ??? Hb); |
---|
537 | ##] |
---|
538 | ##| #ty e1 e2 He1 He2; |
---|
539 | napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1; |
---|
540 | napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1; |
---|
541 | ##[ napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2; |
---|
542 | napply bind_OK; #b2 eb2; |
---|
543 | napply (eval_Eandbool_2 … He1 … He2); |
---|
544 | ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##] |
---|
545 | ##| napply (eval_Eandbool_1 … He1); napply (bool_of … Hb1); |
---|
546 | ##] |
---|
547 | ##| #ty e1 e2 He1 He2; |
---|
548 | napply bind2_OK; #v1 tr1 Hv1; nrewrite > Hv1 in He1; #He1; |
---|
549 | napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1; |
---|
550 | ##[ napply (eval_Eorbool_1 … He1); napply (bool_of … Hb1); |
---|
551 | ##| napply bind2_OK; #v2 tr2 Hv2; nrewrite > Hv2 in He2; #He2; |
---|
552 | napply bind_OK; #b2 eb2; |
---|
553 | napply (eval_Eorbool_2 … He1 … He2); |
---|
554 | ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##] |
---|
555 | ##] |
---|
556 | ##| #ty ty'; nwhd; // |
---|
557 | ##| #ty e' ty' i; ncases ty'; //; |
---|
558 | ##[ #id fs He'; napply bind2_OK; #x; ncases x; #sp l ofs H; |
---|
559 | napply bind_OK; #delta Hdelta; nrewrite > H in He'; #He'; |
---|
560 | napply (eval_Efield_struct … He' (refl ??) Hdelta); |
---|
561 | ##| #id fs He'; napply bind2_OK; #x; ncases x; #sp l ofs H; |
---|
562 | nrewrite > H in He'; #He'; |
---|
563 | napply (eval_Efield_union … He' (refl ??)); |
---|
564 | ##] |
---|
565 | ##| #ty l e' He'; napply bind2_OK; #v tr1 H; nrewrite > H in He'; #He'; |
---|
566 | napply (eval_Ecost … He'); |
---|
567 | (* exec_lvalue fails on non-lvalues. *) |
---|
568 | ##| #e' ty; ncases e'; |
---|
569 | ##[ ##1,2,5,12: #a H ##| ##3,4: #a; * ##| ##13,14: #a b; * ##| ##6,8,10,11: #a b H ##| ##7,9: #a b c H ##] |
---|
570 | napply I; |
---|
571 | ##] nqed. |
---|
572 | |
---|
573 | nlemma addrof_eval_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty. |
---|
574 | eval_expr ge en m (Expr (Eaddrof e) ty) (Vptr sp loc off) tr → |
---|
575 | eval_lvalue ge en m e sp loc off tr. |
---|
576 | #ge en m e sp loc off tr ty H; ninversion H; |
---|
577 | ##[ ##1,2,5: #a b H; napply False_ind; ndestruct (H); |
---|
578 | ##| #a b c d e f g H1 i H2; nrewrite < H2 in H1; #H1; napply False_ind; |
---|
579 | napply (eval_lvalue_inv_ind … H1); |
---|
580 | ##[ #a b c d bad; ndestruct (bad); |
---|
581 | ##| #a b c d e f bad; ndestruct (bad); |
---|
582 | ##| #a b c d e f g bad; ndestruct (bad); |
---|
583 | ##| #a b c d e f g h i j k l m n bad; napply False_ind; ndestruct (bad); |
---|
584 | ##| #a b c d e f g h i j k l bad; ndestruct (bad); |
---|
585 | ##] |
---|
586 | ##| #e' ty' sp' loc' ofs' tr' H e1 e2 e3; ndestruct (e1 e2 e3); napply H; |
---|
587 | ##| #a b c d e f g h i bad; ndestruct (bad); |
---|
588 | ##| #a b c d e f g h i j k l k l bad; ndestruct (bad); |
---|
589 | ##| #a b c d e f g h i j k l m bad; ndestruct (bad); |
---|
590 | ##| #a b c d e f g h i j k l m bad; ndestruct (bad); |
---|
591 | ##| #a b c d e f g h bad; ndestruct (bad); |
---|
592 | ##| #a b c d e f g h i j k l m n bad; ndestruct (bad); |
---|
593 | ##| #a b c d e f g h bad; ndestruct (bad); |
---|
594 | ##| #a b c d e f g h i j k l m n bad; ndestruct (bad); |
---|
595 | ##| #a b c d e f g h i bad; ndestruct (bad); |
---|
596 | ##| #a b c d e f g bad; ndestruct (bad); |
---|
597 | ##] nqed. |
---|
598 | |
---|
599 | nlemma addrof_exec_lvalue: ∀ge,en,m,e,sp,loc,off,tr,ty. |
---|
600 | exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉 → |
---|
601 | exec_expr ge en m (Expr (Eaddrof e) ty) = OK ? 〈Vptr sp loc off, tr〉. |
---|
602 | #ge en m e sp loc off tr ty H; nwhd in ⊢ (??%?); |
---|
603 | nrewrite > H; //; |
---|
604 | nqed. |
---|
605 | |
---|
606 | ntheorem exec_lvalue_sound: ∀ge,en,m,e. |
---|
607 | P_res ? (λr.eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) (exec_lvalue ge en m e). |
---|
608 | #ge en m e; nlapply (refl ? (exec_lvalue ge en m e)); |
---|
609 | ncases (exec_lvalue ge en m e) in ⊢ (???% → %); |
---|
610 | ##[ #x; ncases x; #y; ncases y; #z; ncases z; #sp loc off tr H; nwhd; |
---|
611 | napply (addrof_eval_lvalue … Tvoid); |
---|
612 | nlapply (addrof_exec_lvalue … Tvoid H); #H'; |
---|
613 | nlapply (exec_expr_sound ge en m (Expr (Eaddrof e) Tvoid)); |
---|
614 | nrewrite > H'; #H''; napply H''; |
---|
615 | ##| #_; nwhd; napply I; |
---|
616 | ##] nqed. |
---|
617 | |
---|
618 | (* Plain equality versions of the above *) |
---|
619 | |
---|
620 | ndefinition exec_expr_sound' ≝ λge,en,m,e,v. |
---|
621 | λH:exec_expr ge en m e = OK ? v. |
---|
622 | P_res_to_P ???? (exec_expr_sound ge en m e) H. |
---|
623 | |
---|
624 | ndefinition exec_lvalue_sound' ≝ λge,en,m,e,sp,loc,off,tr. |
---|
625 | λH:exec_lvalue ge en m e = OK ? 〈〈〈sp,loc〉,off〉,tr〉. |
---|
626 | P_res_to_P ???? (exec_lvalue_sound ge en m e) H. |
---|
627 | |
---|
628 | (* TODO: Can we do this sensibly with a map combinator? *) |
---|
629 | nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (list val×trace) ≝ |
---|
630 | match l with |
---|
631 | [ nil ⇒ OK ? 〈nil val, E0〉 |
---|
632 | | cons e1 es ⇒ |
---|
633 | do 〈v,tr1〉 ← exec_expr ge e m e1; |
---|
634 | do 〈vs,tr2〉 ← exec_exprlist ge e m es; |
---|
635 | OK ? 〈cons val v vs, tr1⧺tr2〉 |
---|
636 | ]. |
---|
637 | |
---|
638 | nlemma exec_exprlist_sound: ∀ge,e,m,l. P_res ? (λvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) (exec_exprlist ge e m l). |
---|
639 | #ge e m l; nelim l; |
---|
640 | nwhd; //; |
---|
641 | #e1 es; #IH; |
---|
642 | napply bind2_OK; #v tr1 Hv; |
---|
643 | napply bind2_OK; #vs tr2 Hvs; |
---|
644 | nwhd; napply eval_Econs; |
---|
645 | ##[ napply (P_res_to_P … (exec_expr_sound ge e m e1) Hv); |
---|
646 | ##| napply (P_res_to_P … IH Hvs); |
---|
647 | ##] nqed. |
---|
648 | |
---|
649 | (* Don't really want to use subset rather than sigma here, but can't be bothered |
---|
650 | with *another* set of coercions. XXX: why do I have to get the recursive |
---|
651 | call's property manually? *) |
---|
652 | |
---|
653 | nlet rec exec_alloc_variables (en:env) (m:mem) (l:list (ident × type)) on l : { r:env × mem | alloc_variables en m l (\fst r) (\snd r) } ≝ |
---|
654 | match l with |
---|
655 | [ nil ⇒ Some ? 〈en, m〉 |
---|
656 | | cons h vars ⇒ |
---|
657 | match h with [ mk_pair id ty ⇒ |
---|
658 | match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒ |
---|
659 | match exec_alloc_variables (set … id b1 en) m1 vars with |
---|
660 | [ sig_intro r p ⇒ r ] |
---|
661 | ]]]. nwhd; |
---|
662 | ##[ //; |
---|
663 | ##| nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1); |
---|
664 | #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH; |
---|
665 | napply (alloc_variables_cons … IH); /2/; |
---|
666 | nqed. |
---|
667 | |
---|
668 | (* TODO: can we establish that length params = length vs in advance? *) |
---|
669 | nlet rec exec_bind_parameters (e:env) (m:mem) (params:list (ident × type)) (vs:list val) on params : res (Σm2:mem. bind_parameters e m params vs m2) ≝ |
---|
670 | match params with |
---|
671 | [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ] |
---|
672 | | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒ |
---|
673 | match vs with |
---|
674 | [ nil ⇒ Some ? (Error ?) |
---|
675 | | cons v1 vl ⇒ Some ? ( |
---|
676 | do b ← opt_to_res ? (get … id e); |
---|
677 | do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1); |
---|
678 | err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *) |
---|
679 | ] |
---|
680 | ] ]. |
---|
681 | nwhd; //; |
---|
682 | napply opt_bind_OK; #b eb; |
---|
683 | napply opt_bind_OK; #m1 em1; |
---|
684 | napply sig_bind_OK; #m2 Hm2; |
---|
685 | napply (bind_parameters_cons … eb em1 Hm2); |
---|
686 | nqed. |
---|
687 | |
---|
688 | ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝ |
---|
689 | λt. match t with |
---|
690 | [ Tvoid ⇒ Some ? (Error ?) |
---|
691 | | _ ⇒ Some ? (OK ??) |
---|
692 | ]. nwhd; //; @; #H; ndestruct; nqed. |
---|
693 | |
---|
694 | ninductive decide : Type ≝ |
---|
695 | | dy : decide | dn : decide. |
---|
696 | |
---|
697 | ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P. |
---|
698 | #P d;ncases d;/2/; nqed. |
---|
699 | |
---|
700 | ncoercion decide_inject : |
---|
701 | ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide |
---|
702 | on d:decide to ? + (¬?). |
---|
703 | |
---|
704 | ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P. |
---|
705 | #P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed. |
---|
706 | |
---|
707 | ncoercion decide_inject2 : |
---|
708 | ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2 |
---|
709 | on d:decide to res ?. |
---|
710 | |
---|
711 | alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)". |
---|
712 | alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)". |
---|
713 | ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2). |
---|
714 | #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. |
---|
715 | ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2). |
---|
716 | #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. |
---|
717 | ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2). |
---|
718 | #s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed. |
---|
719 | |
---|
720 | nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝ |
---|
721 | match t1 with |
---|
722 | [ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ] |
---|
723 | | Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz_eq_dec sz sz' with [ inl _ ⇒ match sg_eq_dec sg sg' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
724 | | Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |
---|
725 | | Tpointer s t ⇒ match t2 with [ Tpointer s' t' ⇒ |
---|
726 | match ms_eq_dec s s' with [ inl _ ⇒ |
---|
727 | match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
728 | | Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒ |
---|
729 | match ms_eq_dec s s' with [ inl _ ⇒ |
---|
730 | match assert_type_eq t t' with [ OK _ ⇒ |
---|
731 | match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
732 | | Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒ |
---|
733 | match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
734 | | Tstruct i fl ⇒ |
---|
735 | match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒ |
---|
736 | match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] | _ ⇒ dn ] |
---|
737 | | Tunion i fl ⇒ |
---|
738 | match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒ |
---|
739 | match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] |
---|
740 | | Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] |
---|
741 | ] |
---|
742 | and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝ |
---|
743 | match tl1 with |
---|
744 | [ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ] |
---|
745 | | Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒ |
---|
746 | match assert_type_eq t1 t2 with [ OK _ ⇒ |
---|
747 | match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ] |
---|
748 | ] |
---|
749 | and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝ |
---|
750 | match fl1 with |
---|
751 | [ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ] |
---|
752 | | Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒ |
---|
753 | match ident_eq i1 i2 with [ inl _ ⇒ |
---|
754 | match assert_type_eq t1 t2 with [ OK _ ⇒ |
---|
755 | match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ] |
---|
756 | | _ ⇒ dn ] | _ ⇒ dn ] ] |
---|
757 | ]. |
---|
758 | (* A poor man's clear, otherwise automation picks up recursive calls without |
---|
759 | checking that the argument is smaller. *) |
---|
760 | ngeneralize in assert_type_eq; |
---|
761 | ngeneralize in assert_typelist_eq; |
---|
762 | ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //; |
---|
763 | (* XXX: I have no idea why the first // didn't catch these. *) |
---|
764 | //; //; //; //; //; //; //; //; //; |
---|
765 | nqed. |
---|
766 | |
---|
767 | nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝ |
---|
768 | match k with |
---|
769 | [ Kstop ⇒ dy |
---|
770 | | Kcall _ _ _ _ ⇒ dy |
---|
771 | | _ ⇒ dn |
---|
772 | ]. nwhd; //; @; #H; nelim H; nqed. |
---|
773 | |
---|
774 | nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝ |
---|
775 | match s with |
---|
776 | [ Sskip ⇒ dy |
---|
777 | | _ ⇒ dn |
---|
778 | ]. |
---|
779 | ##[ //; |
---|
780 | ##| ##*: @; #H; ndestruct; |
---|
781 | ##] nqed. |
---|
782 | |
---|
783 | (* IO monad *) |
---|
784 | |
---|
785 | (* Interactions are function calls that return a value and do not change |
---|
786 | the rest of the Clight program's state. *) |
---|
787 | ndefinition io_out ≝ (ident × (list eventval)). |
---|
788 | |
---|
789 | ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝ |
---|
790 | λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res). |
---|
791 | |
---|
792 | ndefinition ret: ∀T. T → (IO eventval io_out T) ≝ |
---|
793 | λT,x.(Value ?? T x). |
---|
794 | |
---|
795 | (* Checking types of values given to / received from an external function call. *) |
---|
796 | |
---|
797 | ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝ |
---|
798 | λev,ty. |
---|
799 | match ty with |
---|
800 | [ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ] |
---|
801 | | Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ] |
---|
802 | | _ ⇒ Some ? (Error ?) |
---|
803 | ]. nwhd; //; nqed. |
---|
804 | |
---|
805 | ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v) ≝ |
---|
806 | λv,ty. |
---|
807 | match ty with |
---|
808 | [ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ] |
---|
809 | | Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ] |
---|
810 | | _ ⇒ Some ? (Error ?) |
---|
811 | ]. nwhd; //; nqed. |
---|
812 | |
---|
813 | nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝ |
---|
814 | match vs with |
---|
815 | [ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) | _ ⇒ Some ? (Error ?) ] |
---|
816 | | cons v vt ⇒ |
---|
817 | match tys with |
---|
818 | [ nil ⇒ Some ? (Error ?) |
---|
819 | | cons ty tyt ⇒ Some ? ( |
---|
820 | do ev ← check_eventval' v ty; |
---|
821 | do evt ← check_eventval_list vt tyt; |
---|
822 | OK ? ((sig_eject ?? ev)::evt)) |
---|
823 | ] |
---|
824 | ]. nwhd; //; |
---|
825 | napply sig_bind_OK; #ev Hev; |
---|
826 | napply sig_bind_OK; #evt Hevt; |
---|
827 | nnormalize; /2/; |
---|
828 | nqed. |
---|
829 | |
---|
830 | (* execution *) |
---|
831 | |
---|
832 | ndefinition store_value_of_type' ≝ |
---|
833 | λty,m,l,v. |
---|
834 | match l with [ mk_pair pl ofs ⇒ |
---|
835 | match pl with [ mk_pair pcl loc ⇒ |
---|
836 | store_value_of_type ty m pcl loc ofs v ] ]. |
---|
837 | |
---|
838 | nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (trace × state)) ≝ |
---|
839 | match st with |
---|
840 | [ State f s k e m ⇒ |
---|
841 | match s with |
---|
842 | [ Sassign a1 a2 ⇒ |
---|
843 | ! 〈l,tr1〉 ← exec_lvalue ge e m a1; |
---|
844 | ! 〈v2,tr2〉 ← exec_expr ge e m a2; |
---|
845 | ! m' ← store_value_of_type' (typeof a1) m l v2; |
---|
846 | ret ? 〈tr1⧺tr2, State f Sskip k e m'〉 |
---|
847 | | Scall lhs a al ⇒ |
---|
848 | ! 〈vf,tr2〉 ← exec_expr ge e m a; |
---|
849 | ! 〈vargs,tr3〉 ← exec_exprlist ge e m al; |
---|
850 | ! fd ← find_funct ? ? ge vf; |
---|
851 | ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a)); |
---|
852 | (* |
---|
853 | ! k' ← match lhs with |
---|
854 | [ None ⇒ ret ? (Kcall (None ?) f e k) |
---|
855 | | Some lhs' ⇒ |
---|
856 | ! locofs ← exec_lvalue ge e m lhs'; |
---|
857 | ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k) |
---|
858 | ]; |
---|
859 | ret ? 〈E0, Callstate fd vargs k' m〉) |
---|
860 | *) |
---|
861 | match lhs with |
---|
862 | [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉 |
---|
863 | | Some lhs' ⇒ |
---|
864 | ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs'; |
---|
865 | ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉 |
---|
866 | ] |
---|
867 | | Ssequence s1 s2 ⇒ ret ? 〈E0, State f s1 (Kseq s2 k) e m〉 |
---|
868 | | Sskip ⇒ |
---|
869 | match k with |
---|
870 | [ Kseq s k' ⇒ ret ? 〈E0, State f s k' e m〉 |
---|
871 | | Kstop ⇒ |
---|
872 | match fn_return f with |
---|
873 | [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉 |
---|
874 | | _ ⇒ Wrong ??? |
---|
875 | ] |
---|
876 | | Kcall _ _ _ _ ⇒ |
---|
877 | match fn_return f with |
---|
878 | [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉 |
---|
879 | | _ ⇒ Wrong ??? |
---|
880 | ] |
---|
881 | | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉 |
---|
882 | | Kdowhile a s' k' ⇒ |
---|
883 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
884 | ! b ← err_to_io … (exec_bool_of_val v (typeof a)); |
---|
885 | match b with |
---|
886 | [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉 |
---|
887 | | false ⇒ ret ? 〈tr, State f Sskip k' e m〉 |
---|
888 | ] |
---|
889 | | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉 |
---|
890 | | Kfor3 a2 a3 s' k' ⇒ ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉 |
---|
891 | | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉 |
---|
892 | | _ ⇒ Wrong ??? |
---|
893 | ] |
---|
894 | | Scontinue ⇒ |
---|
895 | match k with |
---|
896 | [ Kseq s' k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉 |
---|
897 | | Kwhile a s' k' ⇒ ret ? 〈E0, State f (Swhile a s') k' e m〉 |
---|
898 | | Kdowhile a s' k' ⇒ |
---|
899 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
900 | ! b ← err_to_io … (exec_bool_of_val v (typeof a)); |
---|
901 | match b with |
---|
902 | [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉 |
---|
903 | | false ⇒ ret ? 〈tr, State f Sskip k' e m〉 |
---|
904 | ] |
---|
905 | | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉 |
---|
906 | | Kswitch k' ⇒ ret ? 〈E0, State f Scontinue k' e m〉 |
---|
907 | | _ ⇒ Wrong ??? |
---|
908 | ] |
---|
909 | | Sbreak ⇒ |
---|
910 | match k with |
---|
911 | [ Kseq s' k' ⇒ ret ? 〈E0, State f Sbreak k' e m〉 |
---|
912 | | Kwhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉 |
---|
913 | | Kdowhile a s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉 |
---|
914 | | Kfor2 a2 a3 s' k' ⇒ ret ? 〈E0, State f Sskip k' e m〉 |
---|
915 | | Kswitch k' ⇒ ret ? 〈E0, State f Sskip k' e m〉 |
---|
916 | | _ ⇒ Wrong ??? |
---|
917 | ] |
---|
918 | | Sifthenelse a s1 s2 ⇒ |
---|
919 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
920 | ! b ← err_to_io … (exec_bool_of_val v (typeof a)); |
---|
921 | ret ? 〈tr, State f (if b then s1 else s2) k e m〉 |
---|
922 | | Swhile a s' ⇒ |
---|
923 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
924 | ! b ← err_to_io … (exec_bool_of_val v (typeof a)); |
---|
925 | ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m |
---|
926 | else State f Sskip k e m〉 |
---|
927 | | Sdowhile a s' ⇒ ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉 |
---|
928 | | Sfor a1 a2 a3 s' ⇒ |
---|
929 | match is_Sskip a1 with |
---|
930 | [ inl _ ⇒ |
---|
931 | ! 〈v,tr〉 ← exec_expr ge e m a2; |
---|
932 | ! b ← err_to_io … (exec_bool_of_val v (typeof a2)); |
---|
933 | ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉 |
---|
934 | | inr _ ⇒ ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉 |
---|
935 | ] |
---|
936 | | Sreturn a_opt ⇒ |
---|
937 | match a_opt with |
---|
938 | [ None ⇒ match fn_return f with |
---|
939 | [ Tvoid ⇒ ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉 |
---|
940 | | _ ⇒ Wrong ??? |
---|
941 | ] |
---|
942 | | Some a ⇒ |
---|
943 | ! u ← err_to_io_sig … (is_not_void (fn_return f)); |
---|
944 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
945 | ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉 |
---|
946 | ] |
---|
947 | | Sswitch a sl ⇒ |
---|
948 | ! 〈v,tr〉 ← exec_expr ge e m a; |
---|
949 | match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉 |
---|
950 | | _ ⇒ Wrong ??? ] |
---|
951 | | Slabel lbl s' ⇒ ret ? 〈E0, State f s' k e m〉 |
---|
952 | | Sgoto lbl ⇒ |
---|
953 | match find_label lbl (fn_body f) (call_cont k) with |
---|
954 | [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ ret ? 〈E0, State f s' k' e m〉 ] |
---|
955 | | None ⇒ Wrong ??? |
---|
956 | ] |
---|
957 | | Scost lbl s' ⇒ ret ? 〈Echarge lbl, State f s' k e m〉 |
---|
958 | ] |
---|
959 | | Callstate f0 vargs k m ⇒ |
---|
960 | match f0 with |
---|
961 | [ Internal f ⇒ |
---|
962 | match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒ |
---|
963 | ! m2 ← err_to_io_sig … (exec_bind_parameters e m1 (fn_params f) vargs); |
---|
964 | ret ? 〈E0, State f (fn_body f) k e m2〉 |
---|
965 | ] |
---|
966 | | External f argtys retty ⇒ |
---|
967 | ! evargs ← err_to_io_sig … (check_eventval_list vargs (typlist_of_typelist argtys)); |
---|
968 | ! evres ← do_io f evargs; |
---|
969 | ! vres ← err_to_io_sig … (check_eventval evres (proj_sig_res (signature_of_type argtys retty))); |
---|
970 | ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉 |
---|
971 | ] |
---|
972 | | Returnstate res k m ⇒ |
---|
973 | match k with |
---|
974 | [ Kcall r f e k' ⇒ |
---|
975 | match r with |
---|
976 | [ None ⇒ |
---|
977 | match res with |
---|
978 | [ Vundef ⇒ ret ? 〈E0, (State f Sskip k' e m)〉 |
---|
979 | | _ ⇒ Wrong ??? |
---|
980 | ] |
---|
981 | | Some r' ⇒ |
---|
982 | match r' with [ mk_pair l ty ⇒ |
---|
983 | |
---|
984 | ! m' ← store_value_of_type' ty m l res; |
---|
985 | ret ? 〈E0, (State f Sskip k' e m')〉 |
---|
986 | ] |
---|
987 | ] |
---|
988 | | _ ⇒ Wrong ??? |
---|
989 | ] |
---|
990 | ]. |
---|
991 | |
---|
992 | ntheorem exec_step_sound: ∀ge,st. |
---|
993 | P_io ??? (λr. step ge st (\fst r) (\snd r)) (exec_step ge st). |
---|
994 | #ge st; ncases st; |
---|
995 | ##[ #f s k e m; ncases s; |
---|
996 | ##[ ncases k; |
---|
997 | ##[ nwhd in ⊢ (?????%); |
---|
998 | nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %); |
---|
999 | //; #H; nwhd; |
---|
1000 | napply step_skip_call; //; |
---|
1001 | ##| #s' k'; nwhd; //; |
---|
1002 | ##| #ex s' k'; napply step_skip_or_continue_while; @; //; |
---|
1003 | ##| #ex s' k'; |
---|
1004 | napply res_bindIO2_OK; #v tr Hv; |
---|
1005 | nletin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
1006 | nlapply (refl ? bexpr); |
---|
1007 | ncases bexpr in ⊢ (???% → %); |
---|
1008 | ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb; |
---|
1009 | nwhd in ⊢ (?????%); |
---|
1010 | ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv)); |
---|
1011 | ##[ @; // ##| napply (bool_of … Hb); ##] |
---|
1012 | ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv)); |
---|
1013 | ##[ @; // ##| napply (bool_of … Hb); ##] |
---|
1014 | ##] |
---|
1015 | ##| #_; //; |
---|
1016 | ##] |
---|
1017 | ##| #ex s1 s2 k'; napply step_skip_or_continue_for2; @; //; |
---|
1018 | ##| #ex s1 s2 k'; napply step_skip_for3; |
---|
1019 | ##| #k'; napply step_skip_break_switch; @; //; |
---|
1020 | ##| #r f' e' k'; nwhd in ⊢ (?????%); |
---|
1021 | nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %); |
---|
1022 | //; #H; nwhd; |
---|
1023 | napply step_skip_call; //; |
---|
1024 | ##] |
---|
1025 | ##| #ex1 ex2; |
---|
1026 | napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval; |
---|
1027 | napply res_bindIO2_OK; #v2 tr2 Hv2; |
---|
1028 | napply opt_bindIO_OK; #m' em'; |
---|
1029 | nwhd; napply (step_assign … (exec_lvalue_sound' … Hlval) (exec_expr_sound' … Hv2) em'); |
---|
1030 | ##| #lex fex args; |
---|
1031 | napply res_bindIO2_OK; #vf tr1 Hvf0; nlapply (exec_expr_sound' … Hvf0); #Hvf; |
---|
1032 | napply res_bindIO2_OK; #vargs tr2 Hvargs0; nlapply (P_res_to_P ???? (exec_exprlist_sound …) Hvargs0); #Hvargs; |
---|
1033 | napply opt_bindIO_OK; #fd efd; |
---|
1034 | napply bindIO_OK; #ety; |
---|
1035 | ncases lex; nwhd; |
---|
1036 | ##[ napply (step_call_none … Hvf Hvargs efd ety); |
---|
1037 | ##| #lhs'; |
---|
1038 | napply res_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs; |
---|
1039 | nwhd; napply (step_call_some … (exec_lvalue_sound' … Hlocofs) Hvf Hvargs efd ety); |
---|
1040 | ##] |
---|
1041 | ##| #s1 s2; nwhd; //; |
---|
1042 | ##| #ex s1 s2; |
---|
1043 | napply res_bindIO2_OK; #v tr Hv; |
---|
1044 | nletin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
1045 | nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //; |
---|
1046 | #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb; |
---|
1047 | ##[ napply (step_ifthenelse_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb); |
---|
1048 | ##| napply (step_ifthenelse_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb) |
---|
1049 | ##] |
---|
1050 | ##| #ex s'; |
---|
1051 | napply res_bindIO2_OK; #v tr Hv; |
---|
1052 | nletin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
1053 | nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //; |
---|
1054 | #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb; |
---|
1055 | ##[ napply (step_while_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb); |
---|
1056 | ##| napply (step_while_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb); |
---|
1057 | ##] |
---|
1058 | ##| #ex s'; nwhd; //; |
---|
1059 | ##| #s1 ex s2 s3; nwhd in ⊢ (?????%); nelim (is_Sskip s1); #Hs1; nwhd in ⊢ (?????%); |
---|
1060 | ##[ nrewrite > Hs1; |
---|
1061 | napply res_bindIO2_OK; #v tr Hv; |
---|
1062 | nletin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
1063 | nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //; |
---|
1064 | #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb; |
---|
1065 | ##[ napply (step_for_true … (exec_expr_sound' … Hv)); napply (bool_of … Hb); |
---|
1066 | ##| napply (step_for_false … (exec_expr_sound' … Hv)); napply (bool_of … Hb); |
---|
1067 | ##] |
---|
1068 | ##| napply step_for_start; //; |
---|
1069 | ##] |
---|
1070 | ##| nwhd in ⊢ (?????%); ncases k; //; |
---|
1071 | ##[ #s' k'; nwhd; //; |
---|
1072 | ##| #ex s' k'; nwhd; //; |
---|
1073 | ##| #ex s' k'; nwhd; //; |
---|
1074 | ##| #ex s1 s2 k'; nwhd; //; |
---|
1075 | ##| #k'; napply step_skip_break_switch; @2; //; |
---|
1076 | ##] |
---|
1077 | ##| nwhd in ⊢ (?????%); ncases k; //; |
---|
1078 | ##[ #s' k'; nwhd; //; |
---|
1079 | ##| #ex s' k'; nwhd; napply step_skip_or_continue_while; @2; //; |
---|
1080 | ##| #ex s' k'; nwhd; |
---|
1081 | napply res_bindIO2_OK; #v tr Hv; |
---|
1082 | nletin bexpr ≝ (exec_bool_of_val v (typeof ex)); |
---|
1083 | nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //; |
---|
1084 | #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb; |
---|
1085 | ##[ napply (step_skip_or_continue_dowhile_true … (exec_expr_sound' … Hv)); |
---|
1086 | ##[ @2; // ##| napply (bool_of … Hb); ##] |
---|
1087 | ##| napply (step_skip_or_continue_dowhile_false … (exec_expr_sound' … Hv)); |
---|
1088 | ##[ @2; // ##| napply (bool_of … Hb); ##] |
---|
1089 | ##] |
---|
1090 | ##| #ex s1 s2 k'; nwhd; napply step_skip_or_continue_for2; @2; // |
---|
1091 | ##| #k'; nwhd; //; |
---|
1092 | ##] |
---|
1093 | ##| #r; nwhd in ⊢ (?????%); ncases r; |
---|
1094 | ##[ nwhd; nlapply (refl ? (fn_return f)); ncases (fn_return f) in ⊢ (???% → %); //; #H; |
---|
1095 | napply step_return_0; napply H; |
---|
1096 | ##| #ex; napply sig_bindIO_OK; #u Hnotvoid; |
---|
1097 | napply res_bindIO2_OK; #v tr Hv; |
---|
1098 | nwhd; napply (step_return_1 … Hnotvoid (exec_expr_sound' … Hv)); |
---|
1099 | ##] |
---|
1100 | ##| #ex ls; napply res_bindIO2_OK; #v; ncases v; //; #n tr Hv; |
---|
1101 | napply step_switch; napply (exec_expr_sound' … Hv); |
---|
1102 | ##| #l s'; nwhd; //; |
---|
1103 | ##| #l; nwhd in ⊢ (?????%); nlapply (refl ? (find_label l (fn_body f) (call_cont k))); |
---|
1104 | ncases (find_label l (fn_body f) (call_cont k)) in ⊢ (???% → %); //; |
---|
1105 | #sk; ncases sk; #s' k' H; |
---|
1106 | napply (step_goto … H); |
---|
1107 | ##| #l s'; nwhd; //; |
---|
1108 | ##] |
---|
1109 | ##| #f0 vargs k m; nwhd in ⊢ (?????%); ncases f0; |
---|
1110 | ##[ #fn; |
---|
1111 | napply extract_subset_pair_io; #e m1 ealloc Halloc; |
---|
1112 | napply sig_bindIO_OK; #m2 Hbind; |
---|
1113 | nwhd; napply (step_internal_function … Halloc Hbind); |
---|
1114 | ##| #id argtys rty; napply sig_bindIO_OK; #evs Hevs; |
---|
1115 | napply bindIO_OK; #eres; |
---|
1116 | napply sig_bindIO_OK; #res Hres; |
---|
1117 | nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##] |
---|
1118 | ##] |
---|
1119 | ##| #v k' m'; nwhd in ⊢ (?????%); ncases k'; //; |
---|
1120 | #r f e k; nwhd in ⊢ (?????%); ncases r; |
---|
1121 | ##[ ncases v; nwhd; //; |
---|
1122 | ##| #x; ncases x; #y; ncases y; #z; ncases z; #pcl b ofs ty; |
---|
1123 | napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //; |
---|
1124 | ##] |
---|
1125 | ##] |
---|
1126 | nqed. |
---|
1127 | |
---|
1128 | nlet rec make_initial_state (p:program) : IO eventval io_out state ≝ |
---|
1129 | let ge ≝ globalenv Genv ?? p in |
---|
1130 | let m0 ≝ init_mem Genv ?? p in |
---|
1131 | ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p); |
---|
1132 | ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]); |
---|
1133 | ! f ← find_funct_ptr ? ? ge b; |
---|
1134 | ret ? (Callstate f (nil ?) Kstop m0). |
---|
1135 | |
---|
1136 | nlemma make_initial_state_sound : ∀p. P_io ??? (λs.initial_state p s) (make_initial_state p). |
---|
1137 | #p; ncases p; #fns main vars; |
---|
1138 | nwhd in ⊢ (?????%); |
---|
1139 | napply opt_bindIO2_OK; #sp b esb; |
---|
1140 | napply opt_bindIO_OK; #u ecode; |
---|
1141 | napply opt_bindIO_OK; #f ef; |
---|
1142 | ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##] |
---|
1143 | nwhd; napply (initial_state_intro … esb ef); |
---|
1144 | nqed. |
---|
1145 | |
---|
1146 | ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r). |
---|
1147 | #st; nelim st; |
---|
1148 | ##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct; |
---|
1149 | ##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct; |
---|
1150 | ##| #v k m; ncases k; |
---|
1151 | ##[ ncases v; |
---|
1152 | ##[ ##2: #i; @1; @ i; //; |
---|
1153 | ##| ##1: @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
1154 | ##| #f; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
1155 | ##| #pcl b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
1156 | ##] |
---|
1157 | ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
1158 | ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
1159 | ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
1160 | ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct; |
---|
1161 | ##] |
---|
1162 | ##] nqed. |
---|
1163 | |
---|
1164 | nlet rec exec_steps (n:nat) (ge:genv) (s:state) : |
---|
1165 | IO eventval io_out (trace×state) ≝ |
---|
1166 | match is_final_state s with |
---|
1167 | [ inl _ ⇒ ret ? 〈E0, s〉 |
---|
1168 | | inr _ ⇒ |
---|
1169 | match n with |
---|
1170 | [ O ⇒ ret ? 〈E0, s〉 |
---|
1171 | | S n' ⇒ |
---|
1172 | ! 〈t,s'〉 ← exec_step ge s; |
---|
1173 | (* ! 〈t,s'〉 ← match s with |
---|
1174 | [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (State f s k e (mk_mem c n p)) ] |
---|
1175 | | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Callstate fd args k (mk_mem c n p)) ] |
---|
1176 | | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ] |
---|
1177 | ] ;*) |
---|
1178 | ! 〈t',s''〉 ← match s' with |
---|
1179 | [ State f s k e m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (State f s k e (mk_mem c n p)) ] |
---|
1180 | | Callstate fd args k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Callstate fd args k (mk_mem c n p)) ] |
---|
1181 | | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ] |
---|
1182 | ] ; |
---|
1183 | (* ! 〈t',s''〉 ← exec_steps n' ge s';*) |
---|
1184 | ret ? 〈t ⧺ t',s''〉 |
---|
1185 | ] |
---|
1186 | ]. |
---|
1187 | |
---|
1188 | ntheorem exec_steps_sound: ∀ge,n,st. |
---|
1189 | P_io ??? (λts:trace×state. star (mk_transrel ?? step) ge st (\fst ts) (\snd ts)) |
---|
1190 | (exec_steps n ge st). |
---|
1191 | #ge n; nelim n; |
---|
1192 | ##[ #st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H; nwhd; //; |
---|
1193 | ##| #n' IH st; nwhd in ⊢ (?????%); nelim (is_final_state st); #H; |
---|
1194 | ##[ nwhd; //; |
---|
1195 | ##| napply (P_bindIO2_OK ????????? (exec_step_sound …)); #t s'; ncases s'; |
---|
1196 | ##[ #f s k e m; ##| #fd args k m; ##| #r k m; ##] |
---|
1197 | nwhd in ⊢ (? → ?????(??????%?)); |
---|
1198 | ncases m; #mc mn mp; #Hstep; |
---|
1199 | nwhd in ⊢ (?????(??????%?)); |
---|
1200 | napply (P_bindIO2_OK ????????? (IH …)); #t' s'' Hsteps; |
---|
1201 | nwhd; napply (star_step ????????? Hsteps); ##[ ##2,5,8: napply Hstep; ##| ##3,6,9: // ##] |
---|
1202 | ##] |
---|
1203 | nqed. |
---|
1204 | (* |
---|
1205 | nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) : |
---|
1206 | res (trace×state) ≝ |
---|
1207 | match is_final_state s with |
---|
1208 | [ inl _ ⇒ OK ? 〈E0, s〉 |
---|
1209 | | inr _ ⇒ |
---|
1210 | match n with |
---|
1211 | [ O ⇒ OK ? 〈E0, s〉 |
---|
1212 | | S n' ⇒ |
---|
1213 | 〈t,s'〉 ← exec_step ge s; |
---|
1214 | 〈t',s''〉 ← exec_steps_without_proof n' ge s'; |
---|
1215 | OK ? 〈t ⧺ t',s''〉 |
---|
1216 | ] |
---|
1217 | ]. |
---|
1218 | *) |
---|
1219 | |
---|
1220 | |
---|
1221 | |
---|
1222 | (* A (possibly non-terminating) execution. *) |
---|
1223 | ncoinductive execution : Type ≝ |
---|
1224 | | e_stop : trace → int → mem → execution |
---|
1225 | | e_step : trace → state → execution → execution |
---|
1226 | | e_wrong : execution |
---|
1227 | | e_interact : io_out → (eventval → execution) → execution. |
---|
1228 | |
---|
1229 | ndefinition mem_of_state : state → mem ≝ |
---|
1230 | λs.match s with [ State f s k e m ⇒ m | Callstate f a k m ⇒ m | Returnstate r k m ⇒ m ]. |
---|
1231 | |
---|
1232 | (* This definition is slightly awkward because of the need to provide resumptions. |
---|
1233 | It records the last trace/state passed in, then recursively processes the next |
---|
1234 | state. *) |
---|
1235 | |
---|
1236 | nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝ |
---|
1237 | match s with |
---|
1238 | [ Wrong ⇒ e_wrong |
---|
1239 | | Value v ⇒ match v with [ mk_pair t s' ⇒ |
---|
1240 | match is_final_state s' with |
---|
1241 | [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s') |
---|
1242 | | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ] |
---|
1243 | | Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v)) |
---|
1244 | ]. |
---|
1245 | |
---|
1246 | |
---|
1247 | ndefinition exec_inf : program → execution ≝ |
---|
1248 | λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉). |
---|
1249 | |
---|
1250 | nremark execution_cases: ∀e. |
---|
1251 | e = match e with [ e_stop tr r m ⇒ e_stop tr r m | e_step tr s e ⇒ e_step tr s e |
---|
1252 | | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ]. |
---|
1253 | #e; ncases e; //; nqed. |
---|
1254 | |
---|
1255 | nlemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s = |
---|
1256 | match s with |
---|
1257 | [ Wrong ⇒ e_wrong |
---|
1258 | | Value v ⇒ match v with [ mk_pair t s' ⇒ |
---|
1259 | match is_final_state s' with |
---|
1260 | [ inl r ⇒ e_stop t (sig_eject … r) (mem_of_state s') |
---|
1261 | | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ] |
---|
1262 | | Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v)) |
---|
1263 | ]. |
---|
1264 | #ge s; nrewrite > (execution_cases (exec_inf_aux …)); ncases s; |
---|
1265 | ##[ #o k |
---|
1266 | ##| #x; ncases x; #tr s'; ncases s'; |
---|
1267 | ##[ #fn st k env m |
---|
1268 | ##| #fd args k mem |
---|
1269 | ##| #v k mem; (* for final state check *) ncases k; |
---|
1270 | ##[ ncases v; ##[ ##2,3: #v' ##| ##4: #sp loc off ##] |
---|
1271 | ##| #s' k' ##| ##3,4: #e s' k' ##| ##5,6: #e s' s'' k' ##| #k' ##| #a b c d ##] |
---|
1272 | ##] |
---|
1273 | ##| ##] |
---|
1274 | nwhd in ⊢ (??%%); //; |
---|
1275 | nqed. |
---|
1276 | |
---|
1277 | (* Finite number of steps without interaction. *) |
---|
1278 | ninductive execution_steps : trace → execution → execution → Prop ≝ |
---|
1279 | | steps_none : ∀e. execution_steps E0 e e |
---|
1280 | | steps_one : ∀e,e',tr,tr',s. execution_steps tr' e e' → execution_steps (tr⧺tr') (e_step tr s e) e'. |
---|
1281 | |
---|
1282 | nlemma one_step: ∀ge,tr,s,tr',s',e. |
---|
1283 | exec_inf_aux ge (Value ??? 〈tr,s〉) = e_step tr s (e_step tr' s' e) → |
---|
1284 | step ge s tr' s'. |
---|
1285 | #ge tr s tr' s' e; |
---|
1286 | nrewrite > (exec_inf_aux_unfold ge ?); |
---|
1287 | nwhd in ⊢ (??%? → ?); ncases (is_final_state s); |
---|
1288 | ##[ #H E; nwhd in E:(??%?); ndestruct (E); |
---|
1289 | ##| #H E; nwhd in E:(??%?); ndestruct; |
---|
1290 | nrewrite > (exec_inf_aux_unfold ge ?) in e0; |
---|
1291 | nlapply (refl ? (exec_step ge s)); |
---|
1292 | ncases (exec_step ge s) in ⊢ (???% → %); |
---|
1293 | ##[ #i o E1 E2; nwhd in E2:(??%?); ndestruct (E2); |
---|
1294 | ##| #x; ncases x; #tr'' s'' E1 E2; nwhd in E2:(??%?); |
---|
1295 | ncases (is_final_state s'') in E2; |
---|
1296 | #H' E2; nwhd in E2:(??%?); ndestruct (E2); |
---|
1297 | nlapply (exec_step_sound ge s); |
---|
1298 | nrewrite > E1; nwhd in ⊢ (% → ?); |
---|
1299 | #H1; napply H1 |
---|
1300 | ##| #E1 E2; nwhd in E2:(??%?); ndestruct; |
---|
1301 | ##] |
---|
1302 | ##] nqed. |
---|
1303 | |
---|
1304 | (* starting after state s, zero or more steps of execution e reach state s' |
---|
1305 | after which comes e'. *) |
---|
1306 | ninductive execution_isteps : trace → state → execution → state → execution → Prop ≝ |
---|
1307 | | isteps_none : ∀s,e. execution_isteps E0 s e s e |
---|
1308 | | isteps_one : ∀e,e',tr,tr',s,s',s0. |
---|
1309 | execution_isteps tr' s e s' e' → |
---|
1310 | execution_isteps (tr⧺tr') s0 (e_step tr s e) s' e' |
---|
1311 | | isteps_interact : ∀e,e',k,o,i,s,s',s0,tr,tr'. |
---|
1312 | execution_isteps tr' s e s' e' → |
---|
1313 | k i = e_step tr s e → |
---|
1314 | (¬ ∃r.final_state s r) → (* used to avoid showing that k i doesn't end prog *) |
---|
1315 | execution_isteps (tr⧺tr') s0 (e_interact o k) s' e'. |
---|
1316 | |
---|
1317 | nlemma exec_e_step: ∀ge,x,tr,s,e. |
---|
1318 | exec_inf_aux ge x = e_step tr s e → |
---|
1319 | exec_inf_aux ge (exec_step ge s) = e. |
---|
1320 | #ge x tr s e; |
---|
1321 | nrewrite > (exec_inf_aux_unfold …); ncases x; |
---|
1322 | ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct |
---|
1323 | ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?); |
---|
1324 | ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct; |
---|
1325 | napply refl; |
---|
1326 | ##| #EXEC; nwhd in EXEC:(??%?); ndestruct |
---|
1327 | ##] nqed. |
---|
1328 | |
---|
1329 | nlemma exec_e_step_inv: ∀ge,x,tr,s,e. |
---|
1330 | exec_inf_aux ge x = e_step tr s e → |
---|
1331 | x = Value ??? 〈tr,s〉. |
---|
1332 | #ge x tr s e; |
---|
1333 | nrewrite > (exec_inf_aux_unfold …); ncases x; |
---|
1334 | ##[ #o k EXEC; nwhd in EXEC:(??%?); ndestruct |
---|
1335 | ##| #y; ncases y; #tr' s'; nwhd in ⊢ (??%? → ?); |
---|
1336 | ncases (is_final_state s'); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct; |
---|
1337 | napply refl; |
---|
1338 | ##| #EXEC; nwhd in EXEC:(??%?); ndestruct |
---|
1339 | ##] nqed. |
---|
1340 | |
---|
1341 | (* NB: the E0 in the execs are irrelevant. *) |
---|
1342 | nlemma several_steps: ∀ge,tr,e,e',s,s'. |
---|
1343 | execution_isteps tr s e s' e' → |
---|
1344 | exec_inf_aux ge (Value ??? 〈E0,s〉) = e_step E0 s e → |
---|
1345 | star (mk_transrel … step) ge s tr s' ∧ |
---|
1346 | exec_inf_aux ge (Value ??? 〈E0,s'〉) = e_step E0 s' e'. |
---|
1347 | #ge tr0 e0 e0' s0 s0' H; |
---|
1348 | nelim H; |
---|
1349 | ##[ #s e EXEC; @; //; napply EXEC; |
---|
1350 | ##| #e1 e2 tr1 tr2 s1 s2 s3 STEPS IH EXEC; |
---|
1351 | nrewrite > (exec_inf_aux_unfold ge ?) in EXEC; |
---|
1352 | nwhd in ⊢ (??%? → ?); |
---|
1353 | ncases (is_final_state s3); ##[ nwhd in ⊢ (? → ??%? → ?); #FINAL BAD; ndestruct (BAD) ##] |
---|
1354 | #NOTFINAL EXEC; nwhd in EXEC:(??%?); ndestruct; |
---|
1355 | nrewrite > (exec_inf_aux_unfold ge ?) in e3; |
---|
1356 | nlapply (refl ? (exec_step ge s3)); |
---|
1357 | ncases (exec_step ge s3) in ⊢ (???% → %); |
---|
1358 | ##[ #o k E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC'); |
---|
1359 | ##| #x; ncases x; #tr' s' EXEC3; |
---|
1360 | nwhd in ⊢ (??%? → ?); |
---|
1361 | ncases (is_final_state s'); #FINAL' EXEC'; nwhd in EXEC':(??%?); ##[ ndestruct ##] |
---|
1362 | ncut (exec_inf_aux ge (exec_step ge s1) = e1); ##[ ndestruct (EXEC'); napply refl ##] |
---|
1363 | #EXEC''; |
---|
1364 | nlapply (IH ?); |
---|
1365 | ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?); |
---|
1366 | ncases (is_final_state s1); #FINAL1; |
---|
1367 | ##[ napply False_ind; napply (absurd ?? FINAL'); ncases FINAL1; |
---|
1368 | #r' Hr; @ r'; ndestruct (EXEC'); napply Hr; |
---|
1369 | ##| nwhd in ⊢ (??%?); nrewrite < EXEC''; napply refl |
---|
1370 | ##] |
---|
1371 | ##| *; #STARs1s2 EXEC2; @; |
---|
1372 | ##[ nlapply (exec_step_sound ge s3); nrewrite > EXEC3; |
---|
1373 | nwhd in ⊢ (% → ?); #STEP3; ndestruct (EXEC'); |
---|
1374 | napply (star_step (mk_transrel ?? step) … STEP3 STARs1s2); //; |
---|
1375 | ##| napply EXEC2; |
---|
1376 | ##] |
---|
1377 | ##] |
---|
1378 | ##| #E EXEC'; nwhd in EXEC':(??%?); ndestruct (EXEC'); |
---|
1379 | ##] |
---|
1380 | ##| #e e' k o i s s' s0 tr tr' H1 H2 H3 IH; |
---|
1381 | nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%? → ?); |
---|
1382 | ncases (is_final_state s0); #FINAL EXEC; nwhd in EXEC:(??%?); ndestruct; |
---|
1383 | |
---|
1384 | nrewrite > (exec_inf_aux_unfold ge ?) in e1; |
---|
1385 | nlapply (exec_step_sound ge s0); |
---|
1386 | ncases (exec_step ge s0); |
---|
1387 | ##[ #i' k' SOUND E1; nwhd in SOUND E1:(??%?); ndestruct (E1); |
---|
1388 | ##| #x; ncases x; #tr' s'' SOUND; nwhd in ⊢ (??%? → ?); |
---|
1389 | ncases (is_final_state s''); #FINAL'; nwhd in ⊢ (??%? → ?); #EXEC'; |
---|
1390 | ndestruct (EXEC'); |
---|
1391 | ##| #_; nwhd in ⊢ (??%? → ?); #EXEC'; ndestruct (EXEC'); |
---|
1392 | ##] |
---|
1393 | nlapply (IH ?); |
---|
1394 | ##[ nrewrite > (exec_inf_aux_unfold ge ?); nwhd in ⊢ (??%?); |
---|
1395 | ncases (is_final_state s); |
---|
1396 | ##[ #X; ncases X; #r FINAL'; napply False_ind; napply (absurd ?? H3); |
---|
1397 | @ r; napply FINAL' ##] |
---|
1398 | #FINAL'; nwhd in ⊢ (??%?); |
---|
1399 | nrewrite > (exec_e_step … H2); |
---|
1400 | napply refl; |
---|
1401 | ##| *; #STARsTOs' EXECs'; @; |
---|
1402 | ##[ napply (star_step … STARsTOs'); |
---|
1403 | ##[ ##2: nlapply (SOUND i); |
---|
1404 | nrewrite > (exec_e_step_inv … H2); nwhd in ⊢ (% → ?); |
---|
1405 | #STEP; napply STEP; |
---|
1406 | ##| ##skip; |
---|
1407 | ##| napply refl |
---|
1408 | ##] |
---|
1409 | ##| napply EXECs'; |
---|
1410 | ##] |
---|
1411 | ##] |
---|
1412 | ##] nqed. |
---|
1413 | |
---|
1414 | ninductive execution_terminates : trace → state → execution → state → Prop ≝ |
---|
1415 | | terminates : ∀s,s',tr,tr',r,e,m. |
---|
1416 | execution_isteps tr s e s' (e_stop tr' r m) → execution_terminates (tr⧺tr') s e (Returnstate (Vint r) Kstop m). |
---|
1417 | |
---|
1418 | ncoinductive execution_diverging : execution → Prop ≝ |
---|
1419 | | diverging_step : ∀s,e. execution_diverging e → execution_diverging (e_step E0 s e). |
---|
1420 | |
---|
1421 | (* Makes a finite number of interactions (including cost labels) before diverging. *) |
---|
1422 | ninductive execution_diverges : trace → execution → Prop ≝ |
---|
1423 | | diverges_diverging: ∀tr,s,s',e,e'. |
---|
1424 | execution_isteps tr s e s' e' → |
---|
1425 | execution_diverging e' → |
---|
1426 | execution_diverges tr e. |
---|
1427 | |
---|
1428 | (* NB: "reacting" includes hitting a cost label. *) |
---|
1429 | ncoinductive execution_reacts : traceinf → state → execution → Prop ≝ |
---|
1430 | | reacting: ∀tr,tr',s,s',e,e'. execution_reacts tr' s' e' → execution_isteps tr s e s' e' → tr ≠ E0 → execution_reacts (tr⧻tr') s e. |
---|
1431 | |
---|
1432 | ninductive execution_goes_wrong: trace → state → execution → state → Prop ≝ |
---|
1433 | | go_wrong: ∀tr,s,s',e. execution_isteps tr s e s' e_wrong → execution_goes_wrong tr s e s'. |
---|
1434 | |
---|
1435 | ninductive execution_matches_behavior: execution → program_behavior → Prop ≝ |
---|
1436 | | emb_terminates: ∀s,s',e,tr,r. |
---|
1437 | execution_terminates tr s e s' → |
---|
1438 | execution_matches_behavior e (Terminates tr r) |
---|
1439 | | emb_diverges: ∀e,tr. |
---|
1440 | execution_diverges tr e → |
---|
1441 | execution_matches_behavior e (Diverges tr) |
---|
1442 | | emb_reacts: ∀s,e,tr. |
---|
1443 | execution_reacts tr s e → |
---|
1444 | execution_matches_behavior e (Reacts tr) |
---|
1445 | | emb_wrong: ∀e,s,s',tr. |
---|
1446 | execution_goes_wrong tr s e s' → |
---|
1447 | execution_matches_behavior e (Goes_wrong tr). |
---|
1448 | |
---|
1449 | (* We don't morally need the cut, but the proof I tried without it failed the |
---|
1450 | guarded-by-constructors check and it wasn't apparent why. *) |
---|
1451 | |
---|
1452 | nlet corec silent_sound ge s e |
---|
1453 | (H0:execution_diverging e) |
---|
1454 | (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e) |
---|
1455 | : forever_silent (mk_transrel ?? step) … ge s ≝ ?. |
---|
1456 | ncut (∃s2.∃e2.execution_diverging e2 ∧ exec_inf_aux ge (exec_step ge s) = e_step E0 s2 e2); |
---|
1457 | ##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1; |
---|
1458 | nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?); |
---|
1459 | ncases (is_final_state s); #p EXEC; nwhd in EXEC:(??%?); ndestruct; |
---|
1460 | ninversion H1; #s2 e2 H2 EXEC2; |
---|
1461 | @ s2; @ e2; @; //; |
---|
1462 | ##| *; #s2; *; #e2; *; #H2 EXEC2; |
---|
1463 | napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 (e_step E0 s2 e2) ??)); |
---|
1464 | ncut (exec_step ge s = Value ??? 〈E0,s2〉); |
---|
1465 | ##[ ##1,3,5: nrewrite > (exec_inf_aux_unfold …) in EXEC2; nelim (exec_step ge s); |
---|
1466 | ##[ ##1,4,7: #o k IH EXEC2; nwhd in EXEC2:(??%?); ndestruct; |
---|
1467 | ##| ##2,5,8: #x; ncases x; #tr s'; nwhd in ⊢ (??%? → ?); |
---|
1468 | ncases (is_final_state s'); #p' EXEC2; nwhd in EXEC2:(??%?); ndestruct; |
---|
1469 | napply refl; |
---|
1470 | ##| ##3,6,9: #EXEC2; nwhd in EXEC2:(??%?); ndestruct |
---|
1471 | ##] |
---|
1472 | ##| #EXEC1; nlapply (exec_step_sound ge s); nrewrite > EXEC1; nwhd in ⊢ (% → %); // |
---|
1473 | ##| #EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; napply EXEC2; |
---|
1474 | ##| #EXEC1; @; napply H2; |
---|
1475 | ##] |
---|
1476 | ##] |
---|
1477 | nqed. |
---|
1478 | |
---|
1479 | nlemma final_step: ∀ge,tr,r,m,s. |
---|
1480 | exec_inf_aux ge (exec_step ge s) = e_stop tr r m → |
---|
1481 | step ge s tr (Returnstate (Vint r) Kstop m). |
---|
1482 | #ge tr r m s; |
---|
1483 | nrewrite > (exec_inf_aux_unfold …); |
---|
1484 | nlapply (exec_step_sound ge s); |
---|
1485 | ncases (exec_step ge s); |
---|
1486 | ##[ #o k H EXEC; nwhd in EXEC:(??%?); ndestruct |
---|
1487 | ##| #x; ncases x; #tr' s' SOUND; nwhd in ⊢ (??%? → ?); ncases (is_final_state s'); |
---|
1488 | #FINAL EXEC; nwhd in SOUND EXEC:(??%?); ndestruct; |
---|
1489 | ncases FINAL; #r' FINAL'; ninversion FINAL'; |
---|
1490 | #r'' m' E1 E2; ndestruct; |
---|
1491 | napply SOUND; |
---|
1492 | ##| #_; #EXEC; nwhd in EXEC:(??%?); ndestruct |
---|
1493 | ##] nqed. |
---|
1494 | |
---|
1495 | nlemma terminates_sound: ∀ge,tr,s,s',e. |
---|
1496 | execution_terminates tr s e s' → |
---|
1497 | exec_inf_aux ge (Value ??? 〈E0, s〉) = (e_step E0 s e) → |
---|
1498 | ∃r. star (mk_transrel … step) ge s tr s' ∧ final_state s' r. |
---|
1499 | #ge tr0 s0 s0' e0 H; ncases H; |
---|
1500 | #s s' tr tr' r e m ESTEPS EXEC; @r; @; //; |
---|
1501 | ncases (several_steps … ESTEPS EXEC); #STARs' EXECs'; |
---|
1502 | napply (star_right … STARs'); |
---|
1503 | ##[ ##2: napply (final_step ge tr' r m s'); |
---|
1504 | napply (exec_e_step … EXECs'); |
---|
1505 | ##| ##skip |
---|
1506 | ##| napply refl |
---|
1507 | ##] nqed. |
---|
1508 | |
---|
1509 | nlet corec reacts_sound ge tr s e |
---|
1510 | (REACTS:execution_reacts tr s e) |
---|
1511 | (EXEC:exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e) : |
---|
1512 | forever_reactive (mk_transrel … step) ge s tr ≝ ?. |
---|
1513 | ncut (∃s'.∃e'.∃tr'.∃tr''.execution_reacts tr'' s' e' ∧ execution_isteps tr' s e s' e' ∧ tr' ≠ E0 ∧ tr = tr'⧻tr''); |
---|
1514 | ##[ ninversion REACTS; |
---|
1515 | #tr0 tr' s0 s' e0 e' EREACTS ESTEPS REACTED E1 E2 E3; ndestruct (E2 E3); |
---|
1516 | @ s'; @ e'; @ tr0; @ tr'; @; ##[ @; ##[ @; //; ##| napply REACTED ##] ##| napply refl ##] |
---|
1517 | ##| *; #s'; *; #e'; *; #tr'; *; #tr''; |
---|
1518 | *; *; *; #REACTS' ESTEPS REACTED APPTR; |
---|
1519 | (* nrewrite > APPTR;*) |
---|
1520 | napply (match sym_eq ??? APPTR return λx.λ_.forever_reactive (mk_transrel genv state step) ge s x with [ refl ⇒ ? ]); |
---|
1521 | @; |
---|
1522 | ncases (several_steps … ESTEPS EXEC); #STEPS EXEC'; |
---|
1523 | ##[ ##2: napply STEPS; |
---|
1524 | ##| ##skip |
---|
1525 | ##| napply REACTED |
---|
1526 | ##| napply reacts_sound; |
---|
1527 | ##[ ##2: napply REACTS'; |
---|
1528 | ##| ##skip |
---|
1529 | ##| napply EXEC' |
---|
1530 | ##] |
---|
1531 | ##] |
---|
1532 | nqed. |
---|
1533 | |
---|
1534 | (* is/needs completeness... |
---|
1535 | nlemma wrong_sound: ∀ge,tr,s,s',e. |
---|
1536 | execution_goes_wrong tr s e s' → |
---|
1537 | exec_inf_aux ge (Value ??? 〈E0, s〉) = e_step E0 s e → |
---|
1538 | star (mk_transrel … step) ge s tr s' ∧ |
---|
1539 | nostep (mk_transrel … step) ge s' ∧ |
---|
1540 | (¬∃r. final_state s' r). |
---|
1541 | #ge tr0 s0 s0' e0 WRONG; ncases WRONG; |
---|
1542 | #tr s s' e ESTEPS EXEC; |
---|
1543 | ncases (several_steps … ESTEPS EXEC); |
---|
1544 | #STAR EXEC'; |
---|
1545 | *) |
---|
1546 | |
---|
1547 | (* |
---|
1548 | ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b. |
---|
1549 | *) |
---|