source: C-semantics/CexecIO.ma @ 388

Last change on this file since 388 was 388, checked in by campbell, 9 years ago

Tidy up some decidability functions.

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