source: C-semantics/CexecIO.ma @ 250

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

Begin separating soundness from executable semantics.

File size: 47.4 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
416nlemma exec_expr_sound_0: ∀ge:genv. ∀en:env. ∀m:mem.
417(∀e,ty. P_res ? (λx.eval_lvalue ge en m (Expr e ty) (\fst (\fst (\fst x))) (\snd (\fst (\fst x))) (\snd (\fst x)) (\snd x)) (exec_lvalue' ge en m e ty)) →
418∀e:expr. P_res ? (λx.eval_expr ge en m e (\fst x) (\snd x)) (exec_expr ge en m e).
419#ge en m lvalue_sound e; ncases e; #e' ty; ncases e';
420##[ ##1,2: #c; nwhd; //;
421##| ##3,4: #z; nwhd in ⊢ (???%);
422    napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
423    napply opt_bind_OK;  #v ev; nwhd in ev:(??%?); napply (eval_Elvalue … ev);
424    napply (P_res_to_P … (lvalue_sound ??) H);
425##| #e''; napply bind2_OK; #x; ncases x; #y; ncases y; #sp loc ofs tr H;
426    nwhd; napply eval_Eaddrof; ncases e'' in H ⊢ %; #e0 ty0 H; napply (P_res_to_P … (lvalue_sound ??) H);
427##| #op e1; napply bind2_OK; #v1 tr Hv1;
428    napply opt_bind_OK; #v ev;
429    napply (eval_Eunop … ev);
430##| napply sig_bind2_OK; #v1 tr1 Hv1;
431    napply sig_bind2_OK; #v2 tr2 Hv2;
432    napply opt_bind_OK; #v ev;
433    napply (eval_Ebinop … Hv1 Hv2 ev);
434##| napply sig_bind2_OK; #v tr Hv;
435    napply bind_OK; #v' ev';
436    napply (eval_Ecast … Hv ?);
437    /2/;
438##| napply sig_bind2_OK; #vb tr1 Hvb;
439    napply bind_OK; #b;
440    ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
441    napply sig_bind2_OK; #v tr Hv;
442    ##[ napply (eval_Econdition_true … Hvb ? Hv);  napply (bool_of ??? Hb);
443    ##| napply (eval_Econdition_false … Hvb ? Hv);  napply (bool_of ??? Hb);
444    ##]
445##| napply sig_bind2_OK; #v1 tr1 Hv1;
446    napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
447    ##[ napply sig_bind2_OK; #v2 tr2 Hv2;
448        napply bind_OK; #b2 eb2;
449        napply (eval_Eandbool_2 … Hv1 … Hv2);
450        ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
451    ##| napply (eval_Eandbool_1 … Hv1); napply (bool_of … Hb1);
452    ##]
453##| napply sig_bind2_OK; #v1 tr1 Hv1;
454    napply bind_OK; #b1; ncases b1; #eb1; nlapply (exec_bool_of_val_sound … eb1); #Hb1;
455    ##[ napply (eval_Eorbool_1 … Hv1); napply (bool_of … Hb1);
456    ##| napply sig_bind2_OK; #v2 tr2 Hv2;
457        napply bind_OK; #b2 eb2;
458        napply (eval_Eorbool_2 … Hv1 … Hv2);
459        ##[ napply (bool_of … Hb1); ##| napply (exec_bool_of_val_sound … eb2); ##]
460    ##]
461##| //
462##| napply sig_bind2_OK; nrewrite > c5; #x; ncases x; #y; ncases y; #sp l ofs tr H;
463    napply opt_bind_OK; #v ev; napply (eval_Elvalue … H ev);
464##| napply sig_bind2_OK; #v tr1 H; napply (eval_Ecost … H);
465##| //
466##| //
467##| napply opt_bind_OK; #sl; ncases sl; #sp l el; napply eval_Evar_global; /2/;
468##| napply (eval_Evar_local … c3);
469##| napply sig_bind2_OK; #v; ncases v; //; #sp l ofs tr Hv; nwhd;
470    napply eval_Ederef; //
471##| ##20,21,22,23,24,25,26,27,28,29,30,31,32,33: //
472##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
473    napply bind_OK; #delta Hdelta;
474    napply (eval_Efield_struct … H c5 Hdelta);
475##| napply sig_bind2_OK; #x; ncases x; #sp l ofs H;
476    napply (eval_Efield_union … H c5);
477##| //
478##| //
479##] nqed.
480and 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)) ≝
481and 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)) ≝
482
483(* TODO: Can we do this sensibly with a map combinator? *)
484nlet 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)) ≝
485match l with
486[ nil ⇒ Some ? (OK ? 〈nil val, E0〉)
487| cons e1 es ⇒ Some ? (
488  do 〈v,tr1〉 ← exec_expr ge e m e1;
489  do 〈vs,tr2〉 ← exec_exprlist ge e m es;
490  OK ? 〈cons val v vs, tr1⧺tr2〉)
491]. nwhd; //;
492napply sig_bind2_OK; #v tr1 Hv;
493napply sig_bind2_OK; #vs tr2 Hvs;
494nwhd; napply eval_Econs; //;
495nqed.
496
497(* Don't really want to use subset rather than sigma here, but can't be bothered
498   with *another* set of coercions. XXX: why do I have to get the recursive
499   call's property manually? *)
500
501nlet 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) } ≝
502match l with
503[ nil ⇒ Some ? 〈en, m〉
504| cons h vars ⇒
505  match h with [ mk_pair id ty ⇒
506    match alloc m 0 (sizeof ty) Any with [ mk_pair m1 b1 ⇒
507      match exec_alloc_variables (set … id b1 en) m1 vars with
508      [ sig_intro r p ⇒ r ]
509]]]. nwhd;
510##[ //;
511##| nelim (exec_alloc_variables (set ident ? ? c3 c7 en) c6 c1);
512    #H; nelim H; //; #H0; nelim H0; nnormalize; #en' m' IH;
513napply (alloc_variables_cons … IH); /2/;
514nqed.
515
516(* TODO: can we establish that length params = length vs in advance? *)
517nlet 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) ≝
518  match params with
519  [ nil ⇒ match vs with [ nil ⇒ Some ? (OK ? m) | cons _ _ ⇒ Some ? (Error ?) ]
520  | cons idty params' ⇒ match idty with [ mk_pair id ty ⇒
521      match vs with
522      [ nil ⇒ Some ? (Error ?)
523      | cons v1 vl ⇒ Some ? (
524          do b ← opt_to_res ? (get … id e);
525          do m1 ← opt_to_res ? (store_value_of_type ty m Any b zero v1);
526          err_eject ?? (exec_bind_parameters e m1 params' vl)) (* FIXME: don't want to have to eject here *)
527      ]
528  ] ].
529nwhd; //;
530napply opt_bind_OK; #b eb;
531napply opt_bind_OK; #m1 em1;
532napply sig_bind_OK; #m2 Hm2;
533napply (bind_parameters_cons … eb em1 Hm2);
534nqed.
535
536ndefinition is_not_void : ∀t:type. res (Σu:unit. t ≠ Tvoid) ≝
537λt. match t with
538[ Tvoid ⇒ Some ? (Error ?)
539| _ ⇒ Some ? (OK ??)
540]. nwhd; //; @; #H; ndestruct; nqed.
541
542ninductive decide : Type ≝
543| dy : decide | dn : decide.
544
545ndefinition dodecide : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P.
546#P d;ncases d;/2/; nqed.
547
548ncoercion decide_inject :
549  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ ¬P ]).P + ¬P ≝ dodecide
550  on d:decide to ? + (¬?).
551
552ndefinition dodecide2 : ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P.
553#P d; ncases d; nnormalize; #p; ##[ napply (OK ? p); ##| napply Error ##] nqed.
554
555ncoercion decide_inject2 :
556  ∀P:Prop.∀d.∀p:(match d with [ dy ⇒ P | dn ⇒ True ]).res P ≝ dodecide2
557  on d:decide to res ?.
558
559alias id "Tint" = "cic:/matita/c-semantics/Csyntax/type.con(0,2,0)".
560alias id "Tfloat" = "cic:/matita/c-semantics/Csyntax/type.con(0,3,0)".
561ndefinition sz_eq_dec : ∀s1,s2:intsize. (s1 = s2) + (s1 ≠ s2).
562#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
563ndefinition sg_eq_dec : ∀s1,s2:signedness. (s1 = s2) + (s1 ≠ s2).
564#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
565ndefinition fs_eq_dec : ∀s1,s2:floatsize. (s1 = s2) + (s1 ≠ s2).
566#s1; ncases s1; #s2; ncases s2; /2/; @2; @; #H; ndestruct; nqed.
567
568nlet rec assert_type_eq (t1,t2:type) : res (t1 = t2) ≝
569match t1 with
570[ Tvoid ⇒ match t2 with [ Tvoid ⇒ dy | _ ⇒ dn ]
571| 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 ]
572| Tfloat f ⇒ match t2 with [ Tfloat f' ⇒ match fs_eq_dec f f' with [ inl _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ]
573| Tpointer s t ⇒ match t2 with [ Tpointer s' t' ⇒
574    match ms_eq_dec s s' with [ inl _ ⇒
575      match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
576| Tarray s t n ⇒ match t2 with [ Tarray s' t' n' ⇒
577    match ms_eq_dec s s' with [ inl _ ⇒
578      match assert_type_eq t t' with [ OK _ ⇒
579        match decidable_eq_Z_Type n n' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
580| Tfunction tl t ⇒ match t2 with [ Tfunction tl' t' ⇒ match assert_typelist_eq tl tl' with [ OK _ ⇒
581    match assert_type_eq t t' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] | _ ⇒ dn ]
582| Tstruct i fl ⇒
583    match t2 with [ Tstruct i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
584      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | inr _ ⇒ dn ] |  _ ⇒ dn ]
585| Tunion i fl ⇒
586    match t2 with [ Tunion i' fl' ⇒ match ident_eq i i' with [ inl _ ⇒
587      match assert_fieldlist_eq fl fl' with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] |  _ ⇒ dn ]
588| Tcomp_ptr i ⇒ match t2 with [ Tcomp_ptr i' ⇒ match ident_eq i i' with [ inl _ ⇒ dy | inr _ ⇒ dn ] | _ ⇒ dn ]
589]
590and assert_typelist_eq (tl1,tl2:typelist) : res (tl1 = tl2) ≝
591match tl1 with
592[ Tnil ⇒ match tl2 with [ Tnil ⇒ dy | _ ⇒ dn ]
593| Tcons t1 ts1 ⇒ match tl2 with [ Tnil ⇒ dn | Tcons t2 ts2 ⇒
594    match assert_type_eq t1 t2 with [ OK _ ⇒
595      match assert_typelist_eq ts1 ts2 with [ OK _ ⇒ dy | _ ⇒ dn ] | _ ⇒ dn ] ]
596]
597and assert_fieldlist_eq (fl1,fl2:fieldlist) : res (fl1 = fl2) ≝
598match fl1 with
599[ Fnil ⇒ match fl2 with [ Fnil ⇒ dy | _ ⇒ dn ]
600| Fcons i1 t1 fs1 ⇒ match fl2 with [ Fnil ⇒ dn | Fcons i2 t2 fs2 ⇒
601    match ident_eq i1 i2 with [ inl _ ⇒
602      match assert_type_eq t1 t2 with [ OK _ ⇒
603        match assert_fieldlist_eq fs1 fs2 with [ OK _ ⇒ dy | _ ⇒ dn ]
604        | _ ⇒ dn ] | _ ⇒ dn ] ]
605].
606(* A poor man's clear, otherwise automation picks up recursive calls without
607   checking that the argument is smaller. *)
608ngeneralize in assert_type_eq;
609ngeneralize in assert_typelist_eq;
610ngeneralize in assert_fieldlist_eq; #avoid1; #_; #avoid2; #_; #avoid3; #_; nwhd; //;
611(* XXX: I have no idea why the first // didn't catch these. *)
612//; //; //; //; //; //; //; //; //;
613nqed.
614
615nlet rec is_is_call_cont (k:cont) : (is_call_cont k) + (¬is_call_cont k) ≝
616match k with
617[ Kstop ⇒ dy
618| Kcall _ _ _ _ ⇒ dy
619| _ ⇒ dn
620]. nwhd; //; @; #H; nelim H; nqed.
621
622nlet rec is_Sskip (s:statement) : (s = Sskip) + (s ≠ Sskip) ≝
623match s with
624[ Sskip ⇒ dy
625| _ ⇒ dn
626].
627##[ //;
628##| ##*: @; #H; ndestruct;
629##] nqed.
630
631(* IO monad *)
632
633(* Interactions are function calls that return a value and do not change
634   the rest of the Clight program's state. *)
635ndefinition io_out ≝ (ident × (list eventval)).
636
637ndefinition do_io : ident → list eventval → IO eventval io_out eventval ≝
638λfn,args. Interact ?? eventval 〈fn,args〉 (λres. Value ?? eventval res).
639
640ndefinition ret: ∀T. T → (IO eventval io_out T) ≝
641λT,x.(Value ?? T x).
642
643(* Checking types of values given to / received from an external function call. *)
644
645ndefinition check_eventval : ∀ev:eventval. ∀ty:typ. res (Σv:val. eventval_match ev ty v) ≝
646λev,ty.
647match ty with
648[ Tint ⇒ match ev with [ EVint i ⇒ Some ? (OK ? (Vint i)) | _ ⇒ Some ? (Error ?) ]
649| Tfloat ⇒ match ev with [ EVfloat f ⇒ Some ? (OK ? (Vfloat f)) | _ ⇒ Some ? (Error ?) ]
650| _ ⇒ Some ? (Error ?)
651]. nwhd; //; nqed.
652
653ndefinition check_eventval' : ∀v:val. ∀ty:typ. res (Σev:eventval. eventval_match ev ty v) ≝
654λv,ty.
655match ty with
656[ Tint ⇒ match v with [ Vint i ⇒ Some ? (OK ? (EVint i)) | _ ⇒ Some ? (Error ?) ]
657| Tfloat ⇒ match v with [ Vfloat f ⇒ Some ? (OK ? (EVfloat f)) | _ ⇒ Some ? (Error ?) ]
658| _ ⇒ Some ? (Error ?)
659]. nwhd; //; nqed.
660
661nlet rec check_eventval_list (vs: list val) (tys: list typ) : res (Σevs:list eventval. eventval_list_match evs tys vs) ≝
662match vs with
663[ nil ⇒ match tys with [ nil ⇒ Some ? (OK ? (nil ?)) | _ ⇒ Some ? (Error ?) ]
664| cons v vt ⇒
665  match tys with
666  [ nil ⇒ Some ? (Error ?)
667  | cons ty tyt ⇒ Some ? (
668    do ev ← check_eventval' v ty;
669    do evt ← check_eventval_list vt tyt;
670    OK ? ((sig_eject ?? ev)::evt))
671  ]
672]. nwhd; //;
673napply sig_bind_OK; #ev Hev;
674napply sig_bind_OK; #evt Hevt;
675nnormalize; /2/;
676nqed.
677
678(* execution *)
679
680ndefinition store_value_of_type' ≝
681λty,m,l,v.
682match l with [ mk_pair pl ofs ⇒
683  match pl with [ mk_pair pcl loc ⇒
684    store_value_of_type ty m pcl loc ofs v ] ].
685
686nlet rec exec_step (ge:genv) (st:state) on st : (IO eventval io_out (Σr:trace × state. step ge st (\fst r) (\snd r))) ≝
687match st with
688[ State f s k e m ⇒
689  match s with
690  [ Sassign a1 a2 ⇒ Some ? (
691    ! 〈l,tr1〉 ← exec_lvalue ge e m a1;
692    ! 〈v2,tr2〉 ← exec_expr ge e m a2;
693    ! m' ← store_value_of_type' (typeof a1) m l v2;
694    ret ? 〈tr1⧺tr2, State f Sskip k e m'〉)
695  | Scall lhs a al ⇒ Some ? (
696    ! 〈vf,tr2〉 ← exec_expr ge e m a;
697    ! 〈vargs,tr3〉 ← exec_exprlist ge e m al;
698    ! fd ← find_funct ? ? ge vf;
699    ! p ← err_to_io … (assert_type_eq (type_of_fundef fd) (typeof a));
700(*
701    ! k' ← match lhs with
702         [ None ⇒ ret ? (Kcall (None ?) f e k)
703         | Some lhs' ⇒
704           ! locofs ← exec_lvalue ge e m lhs';
705           ret ? (Kcall (Some ? 〈sig_eject ?? locofs, typeof lhs'〉) f e k)
706         ];
707    ret ? 〈E0, Callstate fd vargs k' m〉)
708*)
709    match lhs with
710         [ None ⇒ ret ? 〈tr2⧺tr3, Callstate fd vargs (Kcall (None ?) f e k) m〉
711         | Some lhs' ⇒
712           ! 〈locofs,tr1〉 ← exec_lvalue ge e m lhs';
713           ret ? 〈tr1⧺tr2⧺tr3, Callstate fd vargs (Kcall (Some ? 〈locofs, typeof lhs'〉) f e k) m〉
714         ])
715  | Ssequence s1 s2 ⇒ Some ? (ret ? 〈E0, State f s1 (Kseq s2 k) e m〉)
716  | Sskip ⇒
717      match k with
718      [ Kseq s k' ⇒ Some ? (ret ? 〈E0, State  f s k' e m〉)
719      | Kstop ⇒
720          match fn_return f with
721          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
722          | _ ⇒ Some ? (Wrong ???)
723          ]
724      | Kcall _ _ _ _ ⇒
725          match fn_return f with
726          [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef k (free_list m (blocks_of_env e))〉)
727          | _ ⇒ Some ? (Wrong ???)
728          ]
729      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
730      | Kdowhile a s' k' ⇒ Some ? (
731          ! 〈v,tr〉 ← exec_expr ge e m a;
732          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
733          match b with
734          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
735          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
736          ])
737      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
738      | Kfor3 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f (Sfor Sskip a2 a3 s') k' e m〉)
739      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
740      | _ ⇒ Some ? (Wrong ???)
741      ]
742  | Scontinue ⇒
743      match k with
744      [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
745      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f (Swhile a s') k' e m〉)
746      | Kdowhile a s' k' ⇒ Some ? (
747          ! 〈v,tr〉 ← exec_expr ge e m a;
748          ! b ← err_to_io … (exec_bool_of_val v (typeof a));
749          match b with
750          [ true ⇒ ret ? 〈tr, State f (Sdowhile a s') k' e m〉
751          | false ⇒ ret ? 〈tr, State f Sskip k' e m〉
752          ])
753      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f a3 (Kfor3 a2 a3 s' k') e m〉)
754      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Scontinue k' e m〉)
755      | _ ⇒ Some ? (Wrong ???)
756      ]
757  | Sbreak ⇒
758      match k with
759      [ Kseq s' k' ⇒ Some ? (ret ? 〈E0, State f Sbreak k' e m〉)
760      | Kwhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
761      | Kdowhile a s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
762      | Kfor2 a2 a3 s' k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
763      | Kswitch k' ⇒ Some ? (ret ? 〈E0, State f Sskip k' e m〉)
764      | _ ⇒ Some ? (Wrong ???)
765      ]
766  | Sifthenelse a s1 s2 ⇒ Some ? (
767      ! 〈v,tr〉 ← exec_expr ge e m a;
768      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
769      ret ? 〈tr, State f (if b then s1 else s2) k e m〉)
770  | Swhile a s' ⇒ Some ? (
771      ! 〈v,tr〉 ← exec_expr ge e m a;
772      ! b ← err_to_io … (exec_bool_of_val v (typeof a));
773      ret ? 〈tr, if b then State f s' (Kwhile a s' k) e m
774                      else State f Sskip k e m〉)
775  | Sdowhile a s' ⇒ Some ? (ret ? 〈E0, State f s' (Kdowhile a s' k) e m〉)
776  | Sfor a1 a2 a3 s' ⇒
777      match is_Sskip a1 with
778      [ inl _ ⇒ Some ? (
779          ! 〈v,tr〉 ← exec_expr ge e m a2;
780          ! b ← err_to_io … (exec_bool_of_val v (typeof a2));
781          ret ? 〈tr, State f (if b then s' else Sskip) (if b then (Kfor2 a2 a3 s' k) else k) e m〉)
782      | inr _ ⇒ Some ? (ret ? 〈E0, State f a1 (Kseq (Sfor Sskip a2 a3 s') k) e m〉)
783      ]
784  | Sreturn a_opt ⇒
785    match a_opt with
786    [ None ⇒ match fn_return f with
787      [ Tvoid ⇒ Some ? (ret ? 〈E0, Returnstate Vundef (call_cont k) (free_list m (blocks_of_env e))〉)
788      | _ ⇒ Some ? (Wrong ???)
789      ]
790    | Some a ⇒ Some ? (
791        ! u ← is_not_void (fn_return f);
792        ! 〈v,tr〉 ← exec_expr ge e m a;
793        ret ? 〈tr, Returnstate v (call_cont k) (free_list m (blocks_of_env e))〉)
794    ]
795  | Sswitch a sl ⇒ Some ? (
796      ! 〈v,tr〉 ← exec_expr ge e m a;
797      match v with [ Vint n ⇒ ret ? 〈tr, State f (seq_of_labeled_statement (select_switch n sl)) (Kswitch k) e m〉
798                   | _ ⇒ Wrong ??? ])
799  | Slabel lbl s' ⇒ Some ? (ret ? 〈E0, State f s' k e m〉)
800  | Sgoto lbl ⇒
801      match find_label lbl (fn_body f) (call_cont k) with
802      [ Some sk' ⇒ match sk' with [ mk_pair s' k' ⇒ Some ? (ret ? 〈E0, State f s' k' e m〉) ]
803      | None ⇒ Some ? (Wrong ???)
804      ]
805  | Scost lbl s' ⇒ Some ? (ret ? 〈Echarge lbl, State f s' k e m〉)
806  ]
807| Callstate f0 vargs k m ⇒
808  match f0 with
809  [ Internal f ⇒ Some ? (
810    match exec_alloc_variables empty_env m ((fn_params f) @ (fn_vars f)) with [ mk_pair e m1 ⇒
811      ! m2 ← exec_bind_parameters e m1 (fn_params f) vargs;
812      ret ? 〈E0, State f (fn_body f) k e m2〉
813    ])
814  | External f argtys retty ⇒ Some ? (
815      ! evargs ← check_eventval_list vargs (typlist_of_typelist argtys);
816      ! evres ← do_io f evargs;
817      ! vres ← check_eventval evres (proj_sig_res (signature_of_type argtys retty));
818      ret ? 〈(Eextcall f evargs evres), Returnstate vres k m〉)
819  ]
820| Returnstate res k m ⇒
821  match k with
822  [ Kcall r f e k' ⇒
823    match r with
824    [ None ⇒
825      match res with
826      [ Vundef ⇒ Some ? (ret ? 〈E0, (State f Sskip k' e m)〉)
827      | _ ⇒ Some ? (Wrong ???)
828      ]
829    | Some r' ⇒
830      match r' with [ mk_pair l ty ⇒
831        Some ? (
832          ! m' ← store_value_of_type' ty m l res;
833          ret ? 〈E0, (State f Sskip k' e m')〉)
834      ]
835    ]
836  | _ ⇒ Some ? (Wrong ???)
837  ]
838]. nwhd; //;
839##[ nrewrite > c7; napply step_skip_call; //; napply c8;
840##| napply step_skip_or_continue_while; @; //;
841##| napply sig_bindIO2_OK; #v tr Hv;
842    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
843    nlapply (refl ? bexpr);
844    ncases bexpr in ⊢ (???% → %);
845    ##[ #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
846        nwhd in ⊢ (?????%);
847        ##[ napply (step_skip_or_continue_dowhile_true … Hv);
848          ##[ @; // ##| napply (bool_of … Hb); ##]
849        ##| napply (step_skip_or_continue_dowhile_false … Hv);
850          ##[ @; // ##| napply (bool_of … Hb); ##]
851        ##]
852    ##| #_; //;
853    ##]
854##| napply step_skip_or_continue_for2; @; //;
855##| napply step_skip_break_switch; @; //;
856##| nrewrite > c11; napply step_skip_call; //; napply c12;
857##| napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr1 Hlval;
858    napply sig_bindIO2_OK; #v2 tr2 Hv2;
859    napply opt_bindIO_OK; #m' em';
860    nwhd; napply (step_assign … Hlval Hv2 em');
861##| napply sig_bindIO2_OK; #vf tr1 Hvf;
862    napply sig_bindIO2_OK; #vargs tr2 Hvargs;
863    napply opt_bindIO_OK; #fd efd;
864    napply bindIO_OK; #ety;
865    ncases c6; nwhd;
866    ##[ napply (step_call_none … Hvf Hvargs efd ety);
867    ##| #lhs';
868        napply sig_bindIO2_OK; #x; ncases x; #y; ncases y; #pcl loc ofs tr3 Hlocofs;
869        nwhd; napply (step_call_some … Hlocofs Hvf Hvargs efd ety);
870    ##]
871##| napply sig_bindIO2_OK; #v tr Hv;
872    nletin bexpr ≝ (exec_bool_of_val v (typeof c6));
873    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
874    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
875    ##[ napply (step_ifthenelse_true … Hv); napply (bool_of … Hb);
876    ##| napply (step_ifthenelse_false … Hv); napply (bool_of … Hb)
877    ##]
878##| napply sig_bindIO2_OK; #v tr Hv;
879    nletin bexpr ≝ (exec_bool_of_val v (typeof c6));
880    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
881    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
882    ##[ napply (step_while_true … Hv); napply (bool_of … Hb);
883    ##| napply (step_while_false … Hv); napply (bool_of … Hb);
884    ##]
885##| nrewrite > c11;
886    napply sig_bindIO2_OK; #v tr Hv;
887    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
888    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
889    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
890    ##[ napply (step_for_true … Hv); napply (bool_of … Hb);
891    ##| napply (step_for_false … Hv); napply (bool_of … Hb);
892    ##]
893##| napply step_for_start; //;
894##| napply step_skip_break_switch; @2; //;
895##| napply step_skip_or_continue_while; @2; //;
896##| napply sig_bindIO2_OK; #v tr Hv;
897    nletin bexpr ≝ (exec_bool_of_val v (typeof c7));
898    nlapply (refl ? bexpr); ncases bexpr in ⊢ (???% → %); //;
899    #b; ncases b; #eb; nlapply (exec_bool_of_val_sound … eb); #Hb;
900    ##[ napply (step_skip_or_continue_dowhile_true … Hv);
901      ##[ @2; // ##| napply (bool_of … Hb); ##]
902    ##| napply (step_skip_or_continue_dowhile_false … Hv);
903      ##[ @2; // ##| napply (bool_of … Hb); ##]
904    ##]
905##| napply step_skip_or_continue_for2; @2; //
906##| napply step_return_0; napply c9;
907##| napply sig_bindIO_OK; #u Hnotvoid;
908    napply sig_bindIO2_OK; #v tr Hv;
909    nwhd; napply (step_return_1 … Hnotvoid Hv);
910##| napply sig_bindIO2_OK; #v; ncases v; //; #n tr Hv;
911    napply step_switch; //;
912##| napply step_goto; nrewrite < c12; napply c9;
913##| napply extract_subset_pair_io; #e m1 ealloc Halloc;
914    napply sig_bindIO_OK; #m2 Hbind;
915    nwhd; napply (step_internal_function … Halloc Hbind);
916##| napply sig_bindIO_OK; #evs Hevs;
917    napply bindIO_OK; #eres;
918    napply sig_bindIO_OK; #res Hres;
919    nwhd; napply step_external_function; @; ##[ napply Hevs; ##| napply Hres; ##] 
920##| ncases c11; #x; ncases x; #pcl b ofs;
921    napply opt_bindIO_OK; #m' em'; napply step_returnstate_1; nwhd in em':(??%?); //;
922##]
923nqed.
924
925nlet rec make_initial_state (p:program) : IO eventval io_out state ≝
926  let ge ≝ globalenv Genv ?? p in
927  let m0 ≝ init_mem Genv ?? p in
928    ! 〈sp,b〉 ← find_symbol ? ? ge (prog_main ?? p);
929    ! u ← opt_to_io … (match ms_eq_dec sp Code with [ inl _ ⇒ Some ? something | inr _ ⇒ None ? ]);
930    ! f ← find_funct_ptr ? ? ge b;
931    ret ? (Callstate f (nil ?) Kstop m0).
932
933nlemma make_initial_state_sound : ∀p. P_io ??? (λs.initial_state p s) (make_initial_state p).
934#p; ncases p; #fns main vars;
935nwhd in ⊢ (?????%);
936napply opt_bindIO2_OK; #sp b esb;
937napply opt_bindIO_OK; #u ecode;
938napply opt_bindIO_OK; #f ef;
939ncases sp in esb ecode; #esb ecode; nwhd in ecode:(??%%); ##[ ##1,2,3,4,5: ndestruct (ecode); ##]
940nwhd; napply (initial_state_intro … esb ef);
941nqed.
942
943ndefinition is_final_state : ∀st:state. (Σr. final_state st r) + (¬∃r. final_state st r).
944#st; nelim st;
945##[ #f s k e m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
946##| #f l k m; @2; @;*; #r H; ninversion H; #i m e; ndestruct;
947##| #v k m; ncases k;
948  ##[ ncases v;
949    ##[ ##2: #i; @1; @ i; //;
950    ##| ##1: @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
951    ##| #f; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
952    ##| #pcl b of; @2; @; *;   #r H; ninversion H; #i m e; ndestruct;
953    ##]
954  ##| #a b; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
955  ##| ##3,4: #a b c; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
956  ##| ##5,6,8: #a b c d; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
957  ##| #a; @2; @; *; #r H; ninversion H; #i m e; ndestruct;
958  ##]
959##] nqed.
960
961nlet rec exec_steps (n:nat) (ge:genv) (s:state) :
962 IO eventval io_out (Σts:trace×state. star (mk_transrel ?? step) ge s (\fst ts) (\snd ts)) ≝
963match is_final_state s with
964[ inl _ ⇒ Some ? (ret ? 〈E0, s〉)
965| inr _ ⇒
966  match n with
967  [ O ⇒ Some ? (ret ? 〈E0, s〉)
968  | S n' ⇒ Some ? (
969      ! 〈t,s'〉 ← exec_step ge s;
970(*      ! 〈t,s'〉 ← match s with
971                 [ 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)) ]
972                 | 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)) ]
973                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_step ge (Returnstate r k (mk_mem c n p)) ]
974                 ] ;*)
975      ! 〈t',s''〉 ← match s' with
976                 [ 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)) ]
977                 | 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)) ]
978                 | Returnstate r k m ⇒ match m with [ mk_mem c n p ⇒ exec_steps n' ge (Returnstate r k (mk_mem c n p)) ]
979                 ] ;
980(*      ! 〈t',s''〉 ← exec_steps n' ge s';*)
981      ret ? 〈t ⧺ t',s''〉)
982  ]
983]. nwhd; /2/;
984napply sig_bindIO2_OK; #t s'; ncases s'; ##[ #f st k e m; ##| #fd args k m; ##| #r k m; ##]
985nwhd in ⊢ (? → ?????(??????%?));
986ncases m; #mc mn mp; #H1;
987nwhd in ⊢ (?????(??????%?));
988napply sig_bindIO2_OK; #t' s'' IH;
989nwhd; napply (star_step … IH); //;
990nqed.
991(*
992nlet rec exec_steps_without_proof (n:nat) (ge:genv) (s:state) :
993 res (trace×state) ≝
994match is_final_state s with
995[ inl _ ⇒ OK ? 〈E0, s〉
996| inr _ ⇒
997  match n with
998  [ O ⇒ OK ? 〈E0, s〉
999  | S n' ⇒
1000      〈t,s'〉 ← exec_step ge s;
1001      〈t',s''〉 ← exec_steps_without_proof n' ge s';
1002      OK ? 〈t ⧺ t',s''〉
1003  ]
1004].
1005*)
1006
1007(* A (possibly non-terminating) execution. *)
1008ncoinductive execution : Type ≝
1009| e_stop : trace → int → execution
1010| e_step : trace → state → execution → execution
1011| e_wrong : execution
1012| e_interact : io_out → (eventval → execution) → execution.
1013
1014nlet corec exec_inf_aux (ge:genv) (s:IO eventval io_out (trace×state)) : execution ≝
1015match s with
1016[ Wrong ⇒ e_wrong
1017| Value v ⇒ match v with [ mk_pair t s' ⇒
1018    match is_final_state s' with
1019    [ inl r ⇒ e_stop t (sig_eject … r)
1020    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
1021| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
1022].
1023
1024
1025ndefinition exec_inf : program → execution ≝
1026λp. exec_inf_aux (globalenv Genv ?? p) (! s ← make_initial_state p; ret ? 〈E0,s〉).
1027
1028nremark execution_cases: ∀e.
1029 e = match e with [ e_stop tr r ⇒ e_stop tr r | e_step tr s e ⇒ e_step tr s e
1030 | e_wrong ⇒ e_wrong | e_interact o k ⇒ e_interact o k ].
1031#e; ncases e; //; nqed.
1032
1033nlemma exec_inf_aux_unfold: ∀ge,s. exec_inf_aux ge s =
1034match s with
1035[ Wrong ⇒ e_wrong
1036| Value v ⇒ match v with [ mk_pair t s' ⇒
1037    match is_final_state s' with
1038    [ inl r ⇒ e_stop t (sig_eject … r)
1039    | inr _ ⇒ e_step t s' (exec_inf_aux ge (exec_step ge s')) ] ]
1040| Interact out k' ⇒ e_interact out (λv. exec_inf_aux ge (k' v))
1041].
1042#ge s; nrewrite > (execution_cases (exec_inf_aux …)); ncases s;
1043##[ #o k
1044##| #x; ncases x; #tr s'; ncases s';
1045  ##[ #fn st k env m
1046  ##| #fd args k mem
1047  ##| #v k mem; (* for final state check *) ncases k;
1048    ##[ ncases v; ##[ ##2,3: #v' ##| ##4: #sp loc off ##]
1049    ##| #s' k' ##| ##3,4: #e s' k' ##| ##5,6: #e s' s'' k' ##| #k' ##| #a b c d ##]
1050  ##]
1051##| ##]
1052nwhd in ⊢ (??%%); //;
1053nqed.
1054
1055(* Finite number of steps without interaction. *)
1056ninductive execution_steps : trace → execution → execution → Prop ≝
1057| steps_none : ∀e. execution_steps E0 e e
1058| steps_one : ∀e,e',tr,tr',s. execution_steps tr' e e' → execution_steps (tr⧺tr') (e_step tr s e) e'.
1059
1060(* Finite number of steps allowing interaction. *)
1061ninductive execution_isteps : trace → execution → execution → Prop ≝
1062| isteps_none : ∀e. execution_isteps E0 e e
1063| isteps_step : ∀e,e',tr,tr',s. execution_isteps tr e e' → execution_isteps (tr⧺tr') (e_step tr s e) e'
1064| isteps_interact : ∀k,o,i,e',tr. execution_isteps tr (k i) e' → execution_isteps tr (e_interact o k) e'.
1065
1066ninductive execution_terminates : trace → int → execution → Prop ≝
1067| terminates : ∀tr,tr',r,e. execution_isteps tr e (e_stop tr' r) → execution_terminates (tr⧺tr') r e.
1068
1069ncoinductive execution_diverging : execution → Prop ≝
1070| diverging_step : ∀s,e. execution_diverging e → execution_diverging (e_step E0 s e).
1071
1072(* Makes a finite number of interactions (including cost labels) before diverging. *)
1073ninductive execution_diverges : trace → execution → Prop ≝
1074| diverges_diverging: ∀tr,e,e'.
1075    execution_isteps tr e e' →
1076    execution_diverging e' →
1077    execution_diverges tr e.
1078
1079(* NB: "reacting" includes hitting a cost label. *)
1080ncoinductive execution_reacts : traceinf → execution → Prop ≝
1081| reacting: ∀tr,tr',e,e'. execution_reacts tr' e' → execution_isteps tr e e' → tr ≠ E0 → execution_reacts (tr⧻tr') e.
1082
1083ninductive execution_goes_wrong: trace → execution → Prop ≝
1084| go_wrong: ∀tr,e. execution_isteps tr e e_wrong → execution_goes_wrong tr e.
1085
1086ninductive execution_matches_behavior: execution → program_behavior → Prop ≝
1087| emb_terminates: ∀e,tr,r.
1088    execution_terminates tr r e →
1089    execution_matches_behavior e (Terminates tr r)
1090| emb_diverges: ∀e,tr.
1091    execution_diverges tr e →
1092    execution_matches_behavior e (Diverges tr)
1093| emb_reacts: ∀e,tr.
1094    execution_reacts tr e →
1095    execution_matches_behavior e (Reacts tr)
1096| emb_wrong: ∀e,tr.
1097    execution_goes_wrong tr e →
1098    execution_matches_behavior e (Goes_wrong tr).
1099
1100(* We don't morally need the cut, but the proof I tried without it failed the
1101   guarded-by-constructors check and it wasn't apparent why. *)
1102
1103nlet corec silent_sound ge s e
1104  (H0:execution_diverging e)
1105  (EXEC:exec_inf_aux ge (Value ??? 〈E0,s〉) = e)
1106  : forever_silent (mk_transrel ?? step) … ge s ≝ ?.
1107ncut (∃s2.∃e2.execution_diverging e2 ∧ exec_inf_aux ge (exec_step ge s) = e_step E0 s2 e2);
1108##[ ncases H0 in EXEC ⊢ %; #s1 e1 H1;
1109    nrewrite > (exec_inf_aux_unfold …); nwhd in ⊢ (??%? → ?);
1110    ncases (is_final_state s); #p EXEC; nwhd in EXEC:(??%?); ndestruct;
1111    ninversion H1; #s2 e2 H2 EXEC2;
1112    @ s2; @ e2; @; //;
1113##| *; #s2; *; #e2; *; #H2 EXEC2;
1114    napply (forever_silent_intro (mk_transrel ?? step) … ge s s2 ? (silent_sound ge s2 (e_step E0 s2 e2) ??));
1115    ncut (∃p.exec_step ge s = Value ??? (sig_intro ?? 〈E0,s2〉 p));
1116    ##[ ##1,3,5: nrewrite > (exec_inf_aux_unfold …) in EXEC2; nelim (exec_step ge s);
1117      ##[ ##1,4,7: #o k IH EXEC2; nwhd in EXEC2:(??%?); ndestruct;
1118      ##| ##2,5,8: #x; ncases x; #y; ncases y; #tr' s' p; nwhd in ⊢ (??%? → ?);
1119          ncases (is_final_state s'); #p' EXEC2; nwhd in EXEC2:(??%?); ndestruct;
1120          @ p; napply refl;
1121      ##| ##3,6,9: #EXEC2; nwhd in EXEC2:(??%?); ndestruct
1122      ##]
1123    ##| *; #p EXEC1; napply p
1124    ##| *; #p EXEC1; nrewrite > EXEC1 in EXEC2; #EXEC2; nwhd in EXEC2:(??(??%)?); napply EXEC2;
1125    ##| *; #p EXEC1; @; napply H2;
1126    ##]
1127##]
1128nqed.
1129
1130(*
1131ntheorem exec_inf_sound: ∀p. ∃b.execution_matches_behavior (exec_inf p) b ∧ exec_program p b.
1132*)
Note: See TracBrowser for help on using the repository browser.