Context Navigation

source: C-semantics/CexecIO.ma @ 226

Last change on this file since 226 was 225, checked in by campbell, 10 years ago
Missing case in cast.
File size: 39.0 KB

Line
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 bool_of_val_3 : ∀v:val. ∀ty:type. res (Σr:bool. bool_of_val v ty (of_bool r)) ≝
41	λv,ty. match v in val with
42	[ Vint i ⇒ match ty with
43	[ Tint _ _ ⇒ Some ? (OK ? (¬eq i zero))
44	\| Tpointer _ _ ⇒ Some ? (OK ? (¬eq i zero))
45	\| _ ⇒ Some ? (Error ?)
46	]
47	\| Vfloat f ⇒ match ty with
48	[ Tfloat _ ⇒ Some ? (OK ? (¬Fcmp Ceq f Fzero))
49	\| _ ⇒ Some ? (Error ?)
50	]
51	\| Vptr _ _ _ ⇒ match ty with
52	[ Tint _ _ ⇒ Some ? (OK ? true)
53	\| Tpointer _ _ ⇒ Some ? (OK ? true)
54	\| _ ⇒ Some ? (Error ?)
55	]
56	\| _ ⇒ Some ? (Error ?)
57	]. nwhd; //;
58	##[ ##1,2: nlapply (eq_spec c0 zero); nelim (eq c0 zero);
59	##[ ##1,3: #e; nrewrite > e; napply bool_of_val_false; //;
60	##\| ##2,4: #ne; napply bool_of_val_true; /2/;
61	##]
62	##\| nelim (eq_dec c0 Fzero);
63	##[ #e; nrewrite > e; nrewrite > (Feq_zero_true …); napply bool_of_val_false; //;
64	##\| #ne; nrewrite > (Feq_zero_false …); //; napply bool_of_val_true; /2/;
65	##]
66	##\| ##4,5: napply bool_of_val_true; //
67	##] nqed.
68
69	ndefinition err_eq ≝ λA,P. λx:res (sigma A P). λy:A.
70	match x with [ Error ⇒ False \| OK x' ⇒
71	match x' with [ sig_intro x'' _ ⇒ x'' = y ]].
72	(* TODO: can I write a coercion for the above? *)
73
74	(* Same as before, except we have to use a slightly different "equality". *)
75
76	nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ err_eq ?? (bool_of_val_3 v ty) b.
77	#v ty r H; nelim H; #v t H'; nelim H';
78	##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
79	##\| #p b i i0 s; @ true; @; //
80	##\| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
81	##\| #p b i p0 t0; @ true; @; //
82	##\| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
83	##\| #i s; @ false; @; //; (nwhd; nrewrite > (eq_true …); //;)
84	##\| #p t; @ false; @; //; (nwhd; nrewrite > (eq_true …); //;)
85	##\| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
86	##]
87	nqed.
88
89	(* Prove a few minor results to make proof obligations easy. *)
90
91	nlemma bind_assoc_r: ∀A,B,C,e,f,g.
92	bind B C (bind A B e f) g = bind A C e (λx.bind B C (f x) g).
93	#A B C e f g; ncases e; nnormalize; //; nqed.
94
95	nlemma bind_OK: ∀A,B,P,e,f.
96	(∀v. e = OK A v → match f v with [ Error ⇒ True \| OK v' ⇒ P v' ]) →
97	match bind A B e f with [ Error ⇒ True \| OK v ⇒ P v ].
98	#A B P e f; nelim e; /2/; nqed.
99
100	nlemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (sigma A P). ∀f:sigma A P → res B.
101	(∀v:A. ∀p:P v. match f (sig_intro A P v p) with [ Error ⇒ True \| OK v' ⇒ P' v'] ) →
102	match bind (sigma A P) B e f with [ Error ⇒ True \| OK v' ⇒ P' v' ].
103	#A B P P' e f; nelim e;
104	##[ #v0; nelim v0; #v Hv IH; napply IH;
105	##\| #_; napply I;
106	##] nqed.
107
108	nlemma bind2_OK: ∀A,B,C,P,e,f.
109	(∀v1,v2. e = OK ? 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True \| OK v' ⇒ P v' ]) →
110	match bind2 A B C e f with [ Error ⇒ True \| OK v ⇒ P v ].
111	#A B C P e f; nelim e; //; #v; ncases v; /2/; nqed.
112
113	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.
114	(∀v1:A.∀v2:B. P 〈v1,v2〉 → match f v1 v2 with [ Error ⇒ True \| OK v' ⇒ P' v'] ) →
115	match bind2 A B C e f with [ Error ⇒ True \| OK v' ⇒ P' v' ].
116	#A B C P P' e f; nelim e; //;
117	#v0; nelim v0; #v; nelim v; #v1 v2 Hv IH; napply IH; //; nqed.
118
119	nlemma reinject: ∀A. ∀P,P':A → Prop. ∀e:res (sigma A P').
120	(∀v:A. err_eq A P' e v → P' v → P v) →
121	match err_eject A P' e with [ Error ⇒ True \| OK v' ⇒ P v' ].
122	#A P P' e; ncases e; //;
123	#v0; nelim v0; #v Pv' IH; /2/;
124	nqed.
125
126	nlemma bool_val_distinct: Vtrue ≠ Vfalse.
127	@; #H; nwhd in H:(??%%); ndestruct; napply (absurd ? e0 one_not_zero);
128	nqed.
129
130	nlemma bool_of: ∀v,ty,b. bool_of_val v ty (of_bool b) →
131	if b then is_true v ty else is_false v ty.
132	#v ty b; ncases b; #H; ninversion H; #v' ty' H' ev et ev; //;
133	napply False_ind; napply (absurd ? ev ?);
134	##[ ##2: napply sym_neq ##] napply bool_val_distinct;
135	nqed.
136
137	ndefinition opt_to_res ≝ λA.λv:option A. match v with [ None ⇒ Error A \| Some v ⇒ OK A v ].
138	nlemma opt_OK: ∀A,P,e.
139	(∀v. e = Some ? v → P v) →
140	match opt_to_res A e with [ Error ⇒ True \| OK v ⇒ P v ].
141	#A P e; nelim e; /2/;
142	nqed.
143
144	nlemma opt_bind_OK: ∀A,B,P,e,f.
145	(∀v. e = Some A v → match f v with [ Error ⇒ True \| OK v' ⇒ P v' ]) →
146	match bind A B (opt_to_res A e) f with [ Error ⇒ True \| OK v ⇒ P v ].
147	#A B P e f; nelim e; nnormalize; /2/; nqed.
148
149	nlemma extract_subset_pair: ∀A,B,C,P. ∀e:{e:A×B \| P e}. ∀Q:A→B→res C. ∀R:C→Prop.
150	(∀a,b. eject ?? e = 〈a,b〉 → P 〈a,b〉 → match Q a b with [ OK v ⇒ R v \| Error ⇒ True]) →
151	match match eject ?? e with [ mk_pair a b ⇒ Q a b ] with [ OK v ⇒ R v \| Error ⇒ True ].
152	#A B C P e Q R; ncases e; #e'; ncases e'; nnormalize;
153	##[ #H; napply (False_ind … H);
154	##\| #e''; ncases e''; #a b Pab H; nnormalize; /2/;
155	##] nqed.
156
157	(*
158	nremark err_later: ∀A,B. ∀e:res A. match e with [ Error ⇒ Error B \| OK v ⇒ Error B ] = Error B.
159	#A B e; ncases e; //; nqed.
160	*)
161
162	nlet rec try_cast_null (m:mem) (i:int) (ty:type) (ty':type) on i : res (Σv':val. cast m (Vint i) ty ty' v') ≝
163	match eq i zero with
164	[ true ⇒
165	match ty with
166	[ Tint _ _ ⇒
167	match ty' with
168	[ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
169	\| Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
170	\| Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
171	\| _ ⇒ Some ? (Error ?)
172	]
173	\| Tpointer _ _ ⇒
174	match ty' with
175	[ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
176	\| Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
177	\| Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
178	\| _ ⇒ Some ? (Error ?)
179	]
180	\| Tarray _ _ _ ⇒
181	match ty' with
182	[ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
183	\| Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
184	\| Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
185	\| _ ⇒ Some ? (Error ?)
186	]
187	\| Tfunction _ _ ⇒
188	match ty' with
189	[ Tpointer _ _ ⇒ Some ? (OK ? (Vint i))
190	\| Tarray _ _ _ ⇒ Some ? (OK ? (Vint i))
191	\| Tfunction _ _ ⇒ Some ? (OK ? (Vint i))
192	\| _ ⇒ Some ? (Error ?)
193	]
194	\| _ ⇒ Some ? (Error ?)
195	]
196	\| false ⇒ Some ? (Error ?)
197	]. nwhd; //; nlapply (eq_spec i zero); nrewrite > c0; #e; nrewrite > e;
198	##[ ##1,2,3: napply cast_ip_z ##\| ##*: napply cast_pp_z ##] //; nqed.
199
200	ndefinition ms_eq_dec : ∀s1,s2:memory_space. (s1 = s2) + (s1 ≠ s2).
201	#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
202
203	ndefinition exec_cast : ∀m:mem. ∀v:val. ∀ty:type. ∀ty':type. res (Σv':val. cast m v ty ty' v') ≝
204	λm:mem. λv:val. λty:type. λty':type.
205	match v with
206	[ Vint i ⇒
207	match ty with
208	[ Tint sz1 si1 ⇒
209	match ty' with
210	[ Tint sz2 si2 ⇒ Some ? (OK ? (Vint (cast_int_int sz2 si2 i)))
211	\| Tfloat sz2 ⇒ Some ? (OK ? (Vfloat (cast_float_float sz2 (cast_int_float si1 i))))
212	\| Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
213	\| Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
214	\| Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
215	\| _ ⇒ Some ? (Error ?)
216	]
217	\| Tpointer _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
218	\| Tarray _ _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
219	\| Tfunction _ _ ⇒ Some (res val) (do r ← try_cast_null m i ty ty'; OK val r)
220	\| _ ⇒ Some ? (Error ?)
221	]
222	\| Vfloat f ⇒
223	match ty with
224	[ Tfloat sz ⇒
225	match ty' with
226	[ Tint sz' si' ⇒ Some ? (OK ? (Vint (cast_int_int sz' si' (cast_float_int si' f))))
227	\| Tfloat sz' ⇒ Some ? (OK ? (Vfloat (cast_float_float sz' f)))
228	\| _ ⇒ Some ? (Error ?)
229	]
230	\| _ ⇒ Some ? (Error ?)
231	]
232	\| Vptr p b ofs ⇒
233	Some ? (
234	do s ← match ty with [ Tpointer s _ ⇒ OK ? s \| Tarray s _ _ ⇒ OK ? s \| Tfunction _ _ ⇒ OK ? Code \| _ ⇒ Error ? ];
235	do u ← match ms_eq_dec p s with [ inl _ ⇒ OK ? something \| inr _ ⇒ Error ? ];
236	do s' ← match ty' with
237	[ Tpointer s _ ⇒ OK ? s \| Tarray s _ _ ⇒ OK ? s \| Tfunction _ _ ⇒ OK ? Code
238	\| _ ⇒ Error ? ];
239	if is_pointer_compat (block_space m b) s'
240	then OK ? (Vptr s' b ofs)
241	else Error ?)
242	\| _ ⇒ Some ? (Error ?)
243	]. nwhd; //;
244	##[ ##1,2,3,4,5,6: napply sig_bind_OK; #v'; #H; ndestruct; napply H;
245	##\| napply bind_OK; #s es;
246	ncut (type_space ty s);
247	##[ ncases ty in es ⊢ %;
248	##[ #e; ##\| ##3,9: #a e; ##\| ##2,4,6,7,8: #a b e; ##\| #a b c e; ##] nwhd in e:(??%?); ndestruct; //;
249	##\| #Hty;
250	napply bind_OK; #u1 eeq;
251	napply bind_OK; #s' es';
252	ncut (type_space ty' s');
253	##[ ncases ty' in es' ⊢ %; ##[ #e; ##\| ##3,9: #a e; ##\| ##2,4,6,7,8: #a b e; ##\| #a b c e; ##]
254	nwhd in e:(??%?); ndestruct; //;
255	##\| #Hty';
256	ncut (s = c0). nelim (ms_eq_dec c0 s) in eeq; //; nnormalize; #_; #e; ndestruct.
257	#e; nrewrite < e;
258	nwhd in match (is_pointer_compat ??) in ⊢ %;
259	ncases (pointer_compat_dec (block_space m c1) s'); #Hcompat;
260	nwhd; /2/;
261	##]
262	##]
263	##] nqed.
264
265	ndefinition load_value_of_type' ≝
266	λty,m,l. match l with [ mk_pair pl ofs ⇒ match pl with [ mk_pair psp loc ⇒
267	load_value_of_type ty m psp loc ofs ] ].
268
269	(* To make the evaluation of bare lvalue expressions invoke exec_lvalue with
270	a structurally smaller value, we break out the surrounding Expr constructor
271	and use exec_lvalue'. *)
272
273	nlet rec exec_expr (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:val×trace. eval_expr ge en m e (\fst r) (\snd r)) ≝
274	match e with
275	[ Expr e' ty ⇒
276	match e' with
277	[ Econst_int i ⇒ Some ? (OK ? 〈Vint i, E0〉)
278	\| Econst_float f ⇒ Some ? (OK ? 〈Vfloat f, E0〉)
279	\| Evar _ ⇒ Some ? (
280	do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
281	do v ← opt_to_res ? (load_value_of_type' ty m l);
282	OK ? 〈v,tr〉)
283	\| Ederef _ ⇒ Some ? (
284	do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
285	do v ← opt_to_res ? (load_value_of_type' ty m l);
286	OK ? 〈v,tr〉)
287	\| Efield _ _ ⇒ Some ? (
288	do 〈l,tr〉 ← exec_lvalue' ge en m e' ty;
289	do v ← opt_to_res ? (load_value_of_type' ty m l);
290	OK ? 〈v,tr〉)
291	\| Eaddrof a ⇒ Some ? (
292	do 〈plo,tr〉 ← exec_lvalue ge en m a;
293	OK ? 〈match plo with [ mk_pair pl ofs ⇒ match pl with [ mk_pair pcl loc ⇒ Vptr pcl loc ofs ] ], tr〉)
294	\| Esizeof ty' ⇒ Some ? (OK ? 〈Vint (repr (sizeof ty')), E0〉)
295	\| Eunop op a ⇒ Some ? (
296	do 〈v1,tr〉 ← exec_expr ge en m a;
297	do v ← opt_to_res ? (sem_unary_operation op v1 (typeof a));
298	OK ? 〈v,tr〉)
299	\| Ebinop op a1 a2 ⇒ Some ? (
300	do 〈v1,tr1〉 ← exec_expr ge en m a1;
301	do 〈v2,tr2〉 ← exec_expr ge en m a2;
302	do v ← opt_to_res ? (sem_binary_operation op v1 (typeof a1) v2 (typeof a2) m);
303	OK ? 〈v,tr1⧺tr2〉)
304	\| Econdition a1 a2 a3 ⇒ Some ? (
305	do 〈v,tr1〉 ← exec_expr ge en m a1;
306	do b ← bool_of_val_3 v (typeof a1);
307	do 〈v',tr2〉 ← match b return λ_.res (val×trace) with
308	[ true ⇒ (exec_expr ge en m a2)
309	\| false ⇒ (exec_expr ge en m a3) ];
310	OK ? 〈v',tr1⧺tr2〉)
311	(* if b then exec_expr ge en m a2 else exec_expr ge en m a3)*)
312	\| Eorbool a1 a2 ⇒ Some ? (
313	do 〈v1,tr1〉 ← exec_expr ge en m a1;
314	do b1 ← bool_of_val_3 v1 (typeof a1);
315	match b1 return λ_.res (val×trace) with [ true ⇒ OK ? 〈Vtrue,tr1〉 \| false ⇒
316	do 〈v2,tr2〉 ← exec_expr ge en m a2;
317	do b2 ← bool_of_val_3 v2 (typeof a2);
318	OK ? 〈of_bool b2, tr1⧺tr2〉 ])
319	\| Eandbool a1 a2 ⇒ Some ? (
320	do 〈v1,tr1〉 ← exec_expr ge en m a1;
321	do b1 ← bool_of_val_3 v1 (typeof a1);
322	match b1 return λ_.res (val×trace) with [ true ⇒
323	do 〈v2,tr2〉 ← exec_expr ge en m a2;
324	do b2 ← bool_of_val_3 v2 (typeof a2);
325	OK ? 〈of_bool b2, tr1⧺tr2〉
326	\| false ⇒ OK ? 〈Vfalse,tr1〉 ])
327	\| Ecast ty' a ⇒ Some ? (
328	do 〈v,tr〉 ← exec_expr ge en m a;
329	do v' ← exec_cast m v (typeof a) ty';
330	OK ? 〈(* XXX *)sig_eject ?? v',tr〉)
331	\| Ecost l a ⇒ Some ? (
332	do 〈v,tr〉 ← exec_expr ge en m a;
333	OK ? 〈v,tr⧺(Echarge l)〉)
334	]
335	]
336	and exec_lvalue' (ge:genv) (en:env) (m:mem) (e':expr_descr) (ty:type) on e' : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m (Expr e' ty) (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
337	match e' with
338	[ Evar id ⇒
339	match (get … id en) with
340	[ None ⇒ Some ? (do 〈sp,l〉 ← opt_to_res ? (find_symbol ? ? ge id); OK ? 〈〈〈sp,l〉,zero〉,E0〉) (* global *)
341	\| Some loc ⇒ Some ? (OK ? 〈〈〈Any,loc〉,zero〉,E0〉) (* local *)
342	]
343	\| Ederef a ⇒ Some ? (
344	do 〈v,tr〉 ← exec_expr ge en m a;
345	match v with
346	[ Vptr sp l ofs ⇒ OK ? 〈〈〈sp,l〉,ofs〉,tr〉
347	\| _ ⇒ Error ?
348	])
349	\| Efield a i ⇒
350	match (typeof a) with
351	[ Tstruct id fList ⇒ Some ? (
352	do 〈plofs,tr〉 ← exec_lvalue ge en m a;
353	do delta ← field_offset i fList;
354	OK ? 〈〈\fst plofs,add (\snd plofs) (repr delta)〉,tr〉)
355	\| Tunion id fList ⇒ Some ? (
356	do 〈plofs,tr〉 ← exec_lvalue ge en m a;
357	OK ? 〈plofs,tr〉)
358	\| _ ⇒ Some ? (Error ?)
359	]
360	\| _ ⇒ Some ? (Error ?)
361	]
362	and exec_lvalue (ge:genv) (en:env) (m:mem) (e:expr) on e : res (Σr:memory_space × block × int × trace. eval_lvalue ge en m e (\fst (\fst (\fst r))) (\snd (\fst (\fst r))) (\snd (\fst r)) (\snd r)) ≝
363	match e with [ Expr e' ty ⇒ exec_lvalue' ge en m e' ty ].
364	nwhd;
365	##[ ##1,2: //
366	##\| ##3,4:
367	napply sig_bind2_OK; nrewrite > c4; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
368	napply opt_bind_OK; #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … H ev);
369	##\| napply sig_bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
370	nwhd; napply eval_Eaddrof; //;
371	##\| napply sig_bind2_OK; #v1 tr Hv1;
372	napply opt_bind_OK; #v ev;
373	napply (eval_Eunop … Hv1 ev);
374	##\| napply sig_bind2_OK; #v1 tr1 Hv1;
375	napply sig_bind2_OK; #v2 tr2 Hv2;
376	napply opt_bind_OK; #v ev;
377	napply (eval_Ebinop … Hv1 Hv2 ev);
378	##\| napply sig_bind2_OK; #v tr Hv;
379	napply sig_bind_OK; #v' Hv';
380	napply (eval_Ecast … Hv Hv');
381	##\| napply sig_bind2_OK; #vb tr1 Hvb;
382	napply sig_bind_OK; #b;
383	ncases b; #Hb; napply sig_bind2_OK; #v tr Hv;
384	##[ napply (eval_Econdition_true … Hvb ? Hv); napply (bool_of ??? Hb);
385	##\| napply (eval_Econdition_false … Hvb ? Hv); napply (bool_of ??? Hb);
386	##]
387	##\| napply sig_bind2_OK; #v1 tr1 Hv1;
388	napply sig_bind_OK; #b1; ncases b1; #Hb1;
389	##[ napply sig_bind2_OK; #v2 tr2 Hv2;
390	napply sig_bind_OK; #b2 Hb2;
391	napply (eval_Eandbool_2 … Hv1 … Hv2);
392	##[ napply (bool_of … Hb1); ##\| napply Hb2; ##]
393	##\| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
394	##]
395	##\| napply sig_bind2_OK; #v1 tr1 Hv1;
396	napply sig_bind_OK; #b1; ncases b1; #Hb1;
397	##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
398	##\| napply sig_bind2_OK; #v2 tr2 Hv2;
399	napply sig_bind_OK; #b2 Hb2;
400	napply (eval_Eorbool_2 … Hv1 … Hv2);
401	##[ napply (bool_of … Hb1); ##\| napply Hb2; ##]
402	##]
403	##\| //
404	##\| napply sig_bind2_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs tr H;
405	napply opt_bind_OK; #v ev; napply (eval_Elvalue … H ev);
406	##\| napply sig_bind2_OK; #v tr1 H; napply (eval_Ecost … H);
407	##\| //
408	##\| //
409	##\| napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/;
410	##\| napply (eval_Evar_local … c3);
411	##\| napply sig_bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
412	napply eval_Ederef; //
413	##\| ##20,21,22,23,24,25,26,27,28,29,30,31,32,33: //
414	##\| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
415	napply bind_OK; #delta Hdelta;
416	napply (eval_Efield_struct … H c5 Hdelta);
417	##\| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
418	napply (eval_Efield_union … H c5);
419	##\| //
420	##\| //
421	##] nqed.
422
423	(* TODO: Can we do this sensibly with a map combinator? *)
424	nlet rec exec_exprlist (ge:genv) (e:env) (m:mem) (l:list expr) on l : res (Σvltr:list val×trace. eval_exprlist ge e m l (\fst vltr) (\snd vltr)) ≝
425	match l with
426	[ nil ⇒ Some ? (OK ? 〈nil val, E0〉)
427	\| cons e1 es ⇒ Some ? (
428	do 〈v,tr1〉 ← exec_expr ge e m e1;
429	do 〈vs,tr2〉 ← exec_exprlist ge e m es;
430	OK ? 〈cons val v vs, tr1⧺tr2〉)
431	]. nwhd; //;
432	napply sig_bind2_OK; #v tr1 Hv;
433	napply sig_bind2_OK; #vs tr2 Hvs;
434	nwhd; napply eval_Econs; //;
435	nqed.
436
437	(* Don't really want to use subset rather than sigma here, but can't be bothered
438	with another set of coercions. XXX: why do I have to get the recursive
439	call's property manually? *)
440
441	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) } ≝
442	match l with
443	[ nil ⇒ Some ? 〈en, m〉
444	\| cons h vars ⇒
445	match h with [ mk_pair id ty ⇒
446	match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒
447	match exec_alloc_variables (set … id b1 en) m1 vars with
448	[ sig_intro r p ⇒ r ]
449	]]]. nwhd;
450	##[ //;
451	##\| nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1);
452	#H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
453	napply (alloc_variables_cons … IH); /2/;
454	nqed.
455
456	(* TODO: can we establish that length params = length vs in advance? *)
457	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) ≝
458	match params with
459	[ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) \| cons _ _ ⇒ Some ? (Error ?) ]
460	\| cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
461	match vs with
462	[ nil ⇒ Some ? (Error ?)
463	\| cons v1 vl ⇒ Some ? (
464	do b ← opt_to_res ? (get … id e);
465	do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);
466	err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
467	]
468	] ].
469	nwhd; //;
470	napply opt_bind_OK; #b eb;
471	napply opt_bind_OK; #m1 em1;
472	napply reinject; #m2 em2 Hm2;
473	napply (bind_parameters_cons … eb em1 Hm2);
474	nqed.
475
476	ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
477	λt. match t with
478	[ Tvoid ⇒ Some ? (Error ?)
479	\| _ ⇒ Some ? (OK ??)
480	]. nwhd; //; @; #H; ndestruct; nqed.
481
482	ninductive decide : Type ≝
483	\| dy : decide \| dn : decide.
484
485	ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P \| dn ⇒ ¬P ]).P + ¬P.
486	#P d;ncases d;/2/; nqed.
487
488	ncoercion decide_inject :
489	∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P \| dn ⇒ ¬P ]).P + ¬P ≝ dodecide
490	on d:decide to ? + (¬?).
491
492	ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P \| dn ⇒ True ]).res P.
493	#P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##\| napply Error ##] nqed.
494
495	ncoercion decide_inject2 :
496	∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P \| dn ⇒ True ]).res P ≝ dodecide2
497	on d:decide to res ?.
498
499	alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
500	alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
501	ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
502	#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
503	ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
504	#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
505	ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
506	#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
507
508	nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
509	match t1 with
510	[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy \| _ ⇒ dn ]
511	\| 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 ]
512	\| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy \| _ ⇒ dn ] \| _ ⇒ dn ]
513	\| Tpointer s t ⇒ match t2 with [ Tpointer s' t' ⇒
514	match ms_eq_dec s s' with [ inl _ ⇒
515	match assert_type_eq t t' with [ OK _ ⇒ dy \| _ ⇒ dn ] \| _ ⇒ dn ] \| _ ⇒ dn ]
516	\| Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒
517	match ms_eq_dec s s' with [ inl _ ⇒
518	match assert_type_eq t t' with [ OK _ ⇒
519	match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy \| inr _ ⇒ dn ] \| _ ⇒ dn ] \| _ ⇒ dn ] \| _ ⇒ dn ]
520	\| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒
521	match assert_type_eq t t' with [ OK _ ⇒ dy \| _ ⇒ dn ] \| _ ⇒ dn ] \| _ ⇒ dn ]
522	\| Tstruct i fl ⇒
523	match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
524	match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy \| _ ⇒ dn ] \| inr _ ⇒ dn ] \| _ ⇒ dn ]
525	\| Tunion i fl ⇒
526	match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
527	match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy \| _ ⇒ dn ] \| _ ⇒ dn ] \| _ ⇒ dn ]
528	\| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy \| inr _ ⇒ dn ] \| _ ⇒ dn ]
529	]
530	and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝
531	match tl1 with
532	[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy \| _ ⇒ dn ]
533	\| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn \| Tcons t2 ts2 ⇒
534	match assert_type_eq t1 t2 with [ OK _ ⇒
535	match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy \| _ ⇒ dn ] \| _ ⇒ dn ] ]
536	]
537	and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝
538	match fl1 with
539	[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy \| _ ⇒ dn ]
540	\| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn \| Fcons i2 t2 fs2 ⇒
541	match ident_eq i1 i2 with [ inl _ ⇒
542	match assert_type_eq t1 t2 with [ OK _ ⇒
543	match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy \| _ ⇒ dn ]
544	\| _ ⇒ dn ] \| _ ⇒ dn ] ]
545	].
546	(* A poor man's clear, otherwise automation picks up recursive calls without
547	checking that the argument is smaller. *)
548	ngeneralize in assert_type_eq;
549	ngeneralize in assert_typelist_eq;
550	ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //;
551	(* XXX: I have no idea why the first // didn't catch these. *)
552	//; //; //; //; //; //; //; //; //;
553	nqed.
554
555	nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
556	match k with
557	[ Kstop ⇒ dy
558	\| Kcall _ _ _ _ ⇒ dy
559	\| _ ⇒ dn
560	]. nwhd; //; @; #H; nelim H; nqed.
561
562	nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝
563	match s with
564	[ Sskip ⇒ dy
565	\| _ ⇒ dn
566	].
567	##[ //;
568	##\| ##*: @; #H; ndestruct;
569	##] nqed.
570
571	(* IO monad *)
572
573	(* Interactions are function calls that return a value and do not change
574	the rest of the Clight program's state. *)
575	ndefinition io_out ≝ (ident × (list eventval)).
576
577	ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝
578	λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res).
579
580	ndefinition ret: ∀T. T → (IO eventval io_out T) ≝
581	λT,x.(Value ?? T x).
582
583	(* Checking types of values given to / received from an external function call. *)
584
585	ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
586	λev,ty.
587	match ty with
588	[ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) \| _ ⇒ Some ? (Error ?) ]
589	\| Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) \| _ ⇒ Some ? (Error ?) ]
590	\| _ ⇒ Some ? (Error ?)
591	]. nwhd; //; nqed.
592
593	ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v) ≝
594	λv,ty.
595	match ty with
596	[ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) \| _ ⇒ Some ? (Error ?) ]
597	\| Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) \| _ ⇒ Some ? (Error ?) ]
598	\| _ ⇒ Some ? (Error ?)
599	]. nwhd; //; nqed.
600
601	nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝
602	match vs with
603	[ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) \| _ ⇒ Some ? (Error ?) ]
604	\| cons v vt ⇒
605	match tys with
606	[ nil ⇒ Some ? (Error ?)
607	\| cons ty tyt ⇒ Some ? (
608	do ev ← check_eventval' v ty;
609	do evt ← check_eventval_list vt tyt;
610	OK ? ((sig_eject ?? ev)::evt))
611	]
612	]. nwhd; //;
613	napply sig_bind_OK; #ev Hev;
614	napply sig_bind_OK; #evt Hevt;
615	nnormalize; /2/;
616	nqed.
617
618	(* execution *)
619
620	ndefinition store_value_of_type' ≝
621	λty,m,l,v.
622	match l with [ mk_pair pl ofs ⇒
623	match pl with [ mk_pair pcl loc ⇒
624	store_value_of_type ty m pcl loc ofs v ] ].
625
626	nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
627	match st with
628	[ State f s k e m ⇒
629	match s with
630	[ Sassign a1 a2 ⇒ Some ? (
631	! 〈l,tr1〉 ← exec_lvalue ge e m a1;
632	! 〈v2,tr2〉 ← exec_expr ge e m a2;
633	! m' ← store_value_of_type' (typeof a1) m l v2;
634	ret ? 〈tr1⧺tr2, State f Sskip k e m'〉)
635	\| Scall lhs a al ⇒ Some ? (
636	! 〈vf,tr2〉 ← exec_expr ge e m a;
637	! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
638	! fd ← find_funct ? ? ge vf;
639	! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));
640	(*
641	! k' ← match lhs with
642	[ None ⇒ ret ? (Kcall (None ?) f e k)
643	\| Some lhs' ⇒
644	! locofs ← exec_lvalue ge e m lhs';
645	ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
646	];
647	ret ? 〈E0, Callstate fd vargs k' m〉)
648	*)
649	match lhs with
650	[ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
651	\| Some lhs' ⇒
652	! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
653	ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
654	])
655	\| Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉)
656	\| Sskip ⇒
657	match k with
658	[ Kseq s k' ⇒ Some ? (ret ? 〈E0, State f s k' e m〉)
659	\| Kstop ⇒
660	match fn_return f with
661	[ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
662	\| _ ⇒ Some ? (Wrong ???)
663	]
664	\| Kcall _ _ _ _ ⇒
665	match fn_return f with
666	[ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
667	\| _ ⇒ Some ? (Wrong ???)
668	]
669	\| Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
670	\| Kdowhile a s' k' ⇒ Some ? (
671	! 〈v,tr〉 ← exec_expr ge e m a;
672	! b ← bool_of_val_3 v (typeof a);
673	match b with
674	[ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
675	\| false ⇒ ret ? 〈tr, State f Sskip k' e m〉
676	])
677	\| Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
678	\| Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
679	\| Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
680	\| _ ⇒ Some ? (Wrong ???)
681	]
682	\| Scontinue ⇒
683	match k with
684	[ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
685	\| Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
686	\| Kdowhile a s' k' ⇒ Some ? (
687	! 〈v,tr〉 ← exec_expr ge e m a;
688	! b ← bool_of_val_3 v (typeof a);
689	match b with
690	[ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
691	\| false ⇒ ret ? 〈tr, State f Sskip k' e m〉
692	])
693	\| Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
694	\| Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
695	\| _ ⇒ Some ? (Wrong ???)
696	]
697	\| Sbreak ⇒
698	match k with
699	[ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Sbreak k' e m〉)
700	\| Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
701	\| Kdowhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
702	\| Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
703	\| Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
704	\| _ ⇒ Some ? (Wrong ???)
705	]
706	\| Sifthenelse a s1 s2 ⇒ Some ? (
707	! 〈v,tr〉 ← exec_expr ge e m a;
708	! b ← bool_of_val_3 v (typeof a);
709	ret ? 〈tr, State f (if b then s1 else s2) k e m〉)
710	\| Swhile a s' ⇒ Some ? (
711	! 〈v,tr〉 ← exec_expr ge e m a;
712	! b ← bool_of_val_3 v (typeof a);
713	ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
714	else State f Sskip k e m〉)
715	\| Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉)
716	\| Sfor a1 a2 a3 s' ⇒
717	match is_Sskip a1 with
718	[ inl _ ⇒ Some ? (
719	! 〈v,tr〉 ← exec_expr ge e m a2;
720	! b ← bool_of_val_3 v (typeof a2);
721	ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
722	\| inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
723	]
724	\| Sreturn a_opt ⇒
725	match a_opt with
726	[ None ⇒ match fn_return f with
727	[ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
728	\| _ ⇒ Some ? (Wrong ???)
729	]
730	\| Some a ⇒ Some ? (
731	! u ← is_not_void (fn_return f);
732	! 〈v,tr〉 ← exec_expr ge e m a;
733	ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
734	]
735	\| Sswitch a sl ⇒ Some ? (
736	! 〈v,tr〉 ← exec_expr ge e m a;
737	match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
738	\| _ ⇒ Wrong ??? ])
739	\| Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
740	\| Sgoto lbl ⇒
741	match find_label lbl (fn_body f) (call_cont k) with
742	[ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ]
743	\| None ⇒ Some ? (Wrong ???)
744	]
745	\| Scost lbl s' ⇒ Some ? (ret ? 〈Echarge lbl, State f s' k e m〉)
746	]
747	\| Callstate f0 vargs k m ⇒
748	match f0 with
749	[ Internal f ⇒ Some ? (
750	match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
751	! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
752	ret ? 〈E0, State f (fn_body f) k e m2〉
753	])
754	\| External f argtys retty ⇒ Some ? (
755	! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
756	! evres ← do_io f evargs;
757	! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty));
758	ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
759	]
760	\| Returnstate res k m ⇒
761	match k with
762	[ Kcall r f e k' ⇒
763	match r with
764	[ None ⇒
765	match res with
766	[ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉)
767	\| _ ⇒ Some ? (Wrong ???)
768	]
769	\| Some r' ⇒
770	match r' with [ mk_pair l ty ⇒
771	Some ? (
772	! m' ← store_value_of_type' ty m l res;
773	ret ? 〈E0, (State f Sskip k' e m')〉)
774	]
775	]
776	\| _ ⇒ Some ? (Wrong ???)
777	]
778	]. nwhd; //;
779	##[ nrewrite > c7; napply step_skip_call; //; napply c8;
780	##\| napply step_skip_or_continue_while; @; //;
781	##\| napply sig_bindIO2_OK; #v tr Hv;
782	napply sig_bindIO_OK; #b; ncases b; #Hb;
783	##[ napply (step_skip_or_continue_dowhile_true … Hv);
784	##[ @; // ##\| napply (bool_of … Hb); ##]
785	##\| napply (step_skip_or_continue_dowhile_false … Hv);
786	##[ @; // ##\| napply (bool_of … Hb); ##]
787	##]
788	##\| napply step_skip_or_continue_for2; @; //;
789	##\| napply step_skip_break_switch; @; //;
790	##\| nrewrite > c11; napply step_skip_call; //; napply c12;
791	##\| napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
792	napply sig_bindIO2_OK; #v2 tr2 Hv2;
793	napply opt_bindIO_OK; #m' em';
794	nwhd; napply (step_assign … Hlval Hv2 em');
795	##\| napply sig_bindIO2_OK; #vf tr1 Hvf;
796	napply sig_bindIO2_OK; #vargs tr2 Hvargs;
797	napply opt_bindIO_OK; #fd efd;
798	napply bindIO_OK; #ety;
799	ncases c6; nwhd;
800	##[ napply (step_call_none … Hvf Hvargs efd ety);
801	##\| #lhs';
802	napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
803	nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
804	##]
805	##\| napply sig_bindIO2_OK; #v tr Hv;
806	napply sig_bindIO_OK; #b; ncases b; #Hb;
807	##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb);
808	##\| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
809	##]
810	##\| napply sig_bindIO2_OK; #v tr Hv;
811	napply sig_bindIO_OK; #b; ncases b; #Hb;
812	##[ napply (step_while_true … Hv); napply (bool_of … Hb);
813	##\| napply (step_while_false … Hv); napply (bool_of … Hb);
814	##]
815	##\| nrewrite > c11;
816	napply sig_bindIO2_OK; #v tr Hv;
817	napply sig_bindIO_OK; #b; ncases b; #Hb;
818	##[ napply (step_for_true … Hv); napply (bool_of … Hb);
819	##\| napply (step_for_false … Hv); napply (bool_of … Hb);
820	##]
821	##\| napply step_for_start; //;
822	##\| napply step_skip_break_switch; @2; //;
823	##\| napply step_skip_or_continue_while; @2; //;
824	##\| napply sig_bindIO2_OK; #v tr Hv;
825	napply sig_bindIO_OK; #b; ncases b; #Hb;
826	##[ napply (step_skip_or_continue_dowhile_true … Hv);
827	##[ @2; // ##\| napply (bool_of … Hb); ##]
828	##\| napply (step_skip_or_continue_dowhile_false … Hv);
829	##[ @2; // ##\| napply (bool_of … Hb); ##]
830	##]
831	##\| napply step_skip_or_continue_for2; @2; //
832	##\| napply step_return_0; napply c9;
833	##\| napply sig_bindIO_OK; #u Hnotvoid;
834	napply sig_bindIO2_OK; #v tr Hv;
835	nwhd; napply (step_return_1 … Hnotvoid Hv);
836	##\| napply sig_bindIO2_OK; #v; ncases v; //; #n tr Hv;
837	napply step_switch; //;
838	##\| napply step_goto; nrewrite < c12; napply c9;
839	##\| napply extract_subset_pair_io; #e m1 ealloc Halloc;
840	napply sig_bindIO_OK; #m2 Hbind;
841	nwhd; napply (step_internal_function … Halloc Hbind);
842	##\| napply sig_bindIO_OK; #evs Hevs;
843	napply bindIO_OK; #eres;
844	napply sig_bindIO_OK; #res Hres;
845	nwhd; napply step_external_function; @; ##[ napply Hevs; ##\| napply Hres; ##]
846	##\| ncases c11; #x; ncases x; #pcl b ofs;
847	napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
848	##]
849	nqed.
850
851	nlet rec make_initial_state (p:program) : IO eventval io_out (Σs:state. initial_state p s) ≝
852	let ge ≝ globalenv Genv ?? p in
853	let m0 ≝ init_mem Genv ?? p in
854	Some ? (
855	! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p);
856	! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something \| inr _ ⇒ None ? ]);
857	! f ← find_funct_ptr ? ? ge b;
858	ret ? (Callstate f (nil ?) Kstop m0)).
859	nwhd;
860	napply opt_bindIO2_OK; #sp b esb;
861	napply opt_bindIO_OK; #u ecode;
862	napply opt_bindIO_OK; #f ef;
863	ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
864	nwhd; napply (initial_state_intro … esb ef);
865	nqed.
866
867	ndefinition is_final_state : ∀st:state. (∃r. final_state st r) + (¬∃r. final_state st r).
868	#st; nelim st;
869	##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
870	##\| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
871	##\| #v k m; ncases k;
872	##[ ncases v;
873	##[ ##2: #i; @1; @ i; //;
874	##\| ##1: @2; @; *; #r H; ninversion H; #i m e; ndestruct;
875	##\| #f; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
876	##\| #pcl b of; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
877	##]
878	##\| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
879	##\| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
880	##\| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
881	##\| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
882	##]
883	##] nqed.
884
885	nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
886	IO eventval io_out (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
887	match is_final_state s with
888	[ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
889	\| inr _ ⇒
890	match n with
891	[ O ⇒ Some ? (ret ? 〈E0, s〉)
892	\| S n' ⇒ Some ? (
893	! 〈t,s'〉 ← exec_step ge s;
894	(* ! 〈t,s'〉 ← match s with
895	[ 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)) ]
896	\| 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)) ]
897	\| Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
898	] ;*)
899	! 〈t',s''〉 ← match s' with
900	[ 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)) ]
901	\| 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)) ]
902	\| Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
903	] ;
904	(* ! 〈t',s''〉 ← exec_steps n' ge s';*)
905	ret ? 〈t ⧺ t',s''〉)
906	]
907	]. nwhd; /2/;
908	napply sig_bindIO2_OK; #t s'; ncases s'; ##[ #f st k e m; ##\| #fd args k m; ##\| #r k m; ##]
909	nwhd in ⊢ (? → ?????(??????%?));
910	ncases m; #mc mn mp; #H1;
911	nwhd in ⊢ (?????(??????%?));
912	napply sig_bindIO2_OK; #t' s'' IH;
913	nwhd; napply (star_step … IH); //;
914	nqed.
915	(*
916	nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) :
917	res (trace×state) ≝
918	match is_final_state s with
919	[ inl _ ⇒ OK ? 〈E0, s〉
920	\| inr _ ⇒
921	match n with
922	[ O ⇒ OK ? 〈E0, s〉
923	\| S n' ⇒
924	〈t,s'〉 ← exec_step ge s;
925	〈t',s''〉 ← exec_steps_without_proof n' ge s';
926	OK ? 〈t ⧺ t',s''〉
927	]
928	].
929	*)
930
931	(* A (possibly non-terminating) execution. *)
932	ncoinductive execution : Type ≝
933	\| e_stop : trace → state → execution
934	\| e_step : trace → state → execution → execution
935	\| e_wrong : execution
936	\| e_interact : io_out → (eventval → execution) → execution.
937
938	nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝
939	match s with
940	[ Wrong ⇒ e_wrong
941	\| Value v ⇒ match v with [ mk_pair t s' ⇒
942	match is_final_state s' with
943	[ inl _ ⇒ e_stop t s'
944	\| inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
945	\| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
946	].
947
948	ndefinition exec_inf : program → execution ≝
949	λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,sig_eject ?? s〉).
950

Note: See TracBrowser for help on using the repository browser.

Download in other formats:

Original Format