source: C-semantics/CexecIO.ma @ 189

Last change on this file since 189 was 189, checked in by campbell, 10 years ago

Rework monad notation so that it is displayed well in proof mode.

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