source: C-semantics/CexecIO.ma @ 185

Last change on this file since 185 was 175, checked in by campbell, 11 years ago

Add cost labels, with the semantics that the label is added to the
event trace.

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