source: C-semantics/CexecIOcomplete.ma @ 239

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

More work on soundness and completeness of executable Clight semantics.

File size: 21.7 KB
Line 
1include "CexecIO.ma".
2include "Plogic/connectives.ma".
3
4ndefinition yields : ∀A,P. res (Σx:A. P x) → A → Prop ≝
5λA,P,e,v. match e with [ OK v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False].
6
7(* This tells us that some execution of e results in v.
8   (There may be many possible executions due to I/O, but we're trying to prove
9   that one particular one exists corresponding to a derivation in the inductive
10   semantics.) *)
11nlet rec yieldsIO (A:Type) (P:A → Prop) (e:IO eventval io_out (Σx:A. P x)) (v:A) on e : Prop ≝
12match e with
13[ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ]
14| Interact _ k ⇒ ∃r.yieldsIO A P (k r) v
15| _ ⇒ False].
16
17nlemma is_pointer_compat_true: ∀m,b,sp.
18  pointer_compat (block_space m b) sp →
19  is_pointer_compat (block_space m b) sp = true.
20#m b sp H; nwhd in ⊢ (??%?);
21nelim (pointer_compat_dec (block_space m b) sp);
22##[ //
23##| #H'; napply False_ind; napply (absurd … H H');
24##] nqed.
25
26nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???.
27##[ #s; ncases s; napply refl;
28##| ##skip
29##] nqed.
30
31notation < "vbox( e break ↓ break e')" with precedence 99 for @{'yields ${e} ${e'}}.
32interpretation "yields" 'yields e e' = (yields ?? e e').
33interpretation "yields IO" 'yields e e' = (yieldsIO ?? e e').
34
35ntheorem is_det: ∀p,s,s'.
36initial_state p s → initial_state p s' → s = s'.
37#p s s' H1 H2;
38ninversion H1; #b1 f1 e11 e12 e13;
39ninversion H2; #b2 f2 e21 e22 e23;
40nrewrite > e11 in e21;
41#e1; nrewrite > (?:b1 = b2) in e12;
42##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1);
43  ##[ //;
44  ##| ndestruct (e2) skip (e22 e23); //;
45  ##]
46##| ndestruct (e1) skip (e11); //
47##] nqed.
48
49nlet rec yieldsIObare (A:Type) (a:IO eventval io_out A) (v':A) on a : Prop ≝
50match a with [ Value v ⇒ v' = v | Interact _ k ⇒ ∃r.yieldsIObare A (k r) v' | _ ⇒ False ].
51
52nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
53yieldsIObare A a v' →
54yieldsIO A P (io_inject eventval io_out A (λx.P x) (Some ? a) p) v'.
55#A P a; nelim a;
56##[ #a k IH v' p H; nwhd in H ⊢ %; nelim H; #r H'; @ r; napply IH; napply H';
57##| #v v' p H; napply H;
58##| #a b; *;
59##] nqed.
60
61
62ntheorem the_initial_state:
63  ∀p,s. initial_state p s → yieldsIO ?? (make_initial_state p) s.
64#p s; ncases p; #fns main globs H;
65napply remove_io_sig;
66ninversion H;
67#b f e1 e2 e3;
68nrewrite > e1;
69nwhd in ⊢ (??%?);
70nrewrite > e2;
71nwhd; napply refl;
72nqed.
73
74ndefinition yieldsbare ≝ λA.λa:res A.λv':A.
75match a with [ OK v ⇒ v' = v | _ ⇒ False ].
76
77nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
78yieldsbare A a v' →
79yields A P (err_inject A (λx.P x) (Some ? a) p) v'.
80#A P a; ncases a;
81##[ #v v' p H; napply H;
82##| #a b; *;
83##] nqed.
84
85nlemma cast_complete: ∀m,v,ty,ty',v'.
86  cast m v ty ty' v' → yields ?? (exec_cast m v ty ty') v'.
87#m v ty ty' v' H;
88nelim H;
89##[ #m i sz1 sz2 sg1 sg2; napply refl;
90##| #m f sz szi sg; napply refl;
91##| #m i sz sz' sg; napply refl;
92##| #m f sz sz'; napply refl;
93##| #m sp sp' ty ty' b ofs H1 H2 H3; napply remove_res_sig;
94    nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##]
95    nwhd in ⊢ (??%?);
96    ##[ ##1,2: nrewrite > (ms_eq_dec_true …); nwhd in ⊢ (??%?); ##]
97    nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ##| ##2,5,8: #sp2 ty2 n2 ##| ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##]
98    #H3; nwhd in ⊢ (??%?);
99    nrewrite > (is_pointer_compat_true …); //;
100##| #m sz si ty'' H; ncases H; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #args rty ##] napply refl;
101##| #m t t' H H'; ncases H; ncases H'; //;
102##] nqed.
103
104nlemma yields_eq: ∀A,P,e,v. yields A P e v → ∃p. e = OK ? (sig_intro … v p).
105#A P e v; ncases e;
106##[ #vp; ncases vp; #v' p H; nwhd in H; nrewrite > H; @ p; napply refl;
107##| *;
108##] nqed.
109
110(* Use to narrow down the choice of expression to just the lvalues. *)
111nlemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop.
112  eval_lvalue ge env m (Expr e ty) sp l ofs tr →
113  (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) →
114  P e.
115#ge env m e ty sp l ofs tr P H; napply (eval_lvalue_inv_ind … H);
116##[ #id l ty e1 e2 e3 e4 e5 e6; ndestruct; //
117##| #id sp l ty e1 e2 e3 e4 e5 e6 e7; ndestruct; //
118##| #e ty sp l ofs tr H e1 e2 e3 e4 e5; ndestruct; //
119##| #e id ty sp l ofs id' fs d tr H e1 e2;(* bogus? *) #_; #e3 e4 e5 e6 e7; ndestruct; //
120##| #e id ty sp l ofs id' fs tr H e1;(* bogus? *) #_; #e2 e3 e4 e5 e6; ndestruct; //
121##] nqed.
122
123nlemma bool_of_val_3_complete : ∀v,ty,r. bool_of_val v ty r → ∃b. r = of_bool b ∧ yields ?? (bool_of_val_3 v ty) b.
124#v ty r H; nelim H; #v t H'; nelim H';
125  ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
126  ##| #p b i i0 s; @ true; @; //
127  ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //;
128  ##| #p b i p0 t0; @ true; @; //
129  ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //;
130  ##| #i s; @ false; @; //;
131  ##| #p t; @ false; @; //;
132  ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //;
133  ##]
134nqed.
135
136nlemma bool_of_true: ∀v,ty. is_true v ty → yields ?? (bool_of_val_3 v ty) true.
137#v ty H; nelim H;
138  ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //;
139  ##| #p b i i0 s; //
140  ##| #i p t ne; nwhd; nrewrite > (eq_false … ne); //;
141  ##| #p b i p0 t0; //
142  ##| #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //;
143  ##]
144nqed.
145
146nlemma bool_of_false: ∀v,ty. is_false v ty → yields ?? (bool_of_val_3 v ty) false.
147#v ty H; nelim H;
148  ##[ #i s; //;
149  ##| #p t; //;
150  ##| #s; nwhd; nrewrite > (Feq_zero_true …); //;
151  ##]
152nqed.
153
154nremark eq_to_jmeq: ∀A. ∀a,b:A. a = b → a ≃ b.
155#A a b H; nrewrite > H; //; nqed.
156
157nlemma dep_option_rewrite: ∀A,B:Type. ∀e:option A. ∀r:B. ∀P:B → Prop. ∀Q:e ≃ None A → res (Σx:B. P x). ∀R:∀v. e ≃ Some A v → res (Σx:B. P x). ∀h: e = None A.
158 yields ?? (Q (eq_to_jmeq ??? h)) r →
159 yields ?? ((match e return λe'.e ≃ e' → ? with [ None ⇒ λp.Q p | Some v ⇒ λp.R v p ]) (refl_jmeq (option A) e)) r.
160#A B e; ncases e;
161##[ #r P Q R h; nwhd in ⊢ (? → ???%?);
162napply (streicherKjmeq ?? (λe. yields ?? (Q e) r → yields ?? (Q (refl_jmeq (option A) (None A))) r));
163//;
164##| #v r P Q R h; ndestruct (h);
165##] nqed.
166
167nlemma expr_lvalue_complete: ∀ge,env,m.
168(∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) ∧
169(∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)).
170#ge env m;
171napply (combined_expr_lvalue_ind ge env m
172  (λe,v,tr,H. yields ?? (exec_expr ge env m e) (〈v,tr〉))
173  (λe,sp,l,off,tr,H. yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉)));
174##[ #i ty; napply refl;
175##| #f ty; napply refl;
176##| #e ty sp l off v tr H1 H2; napply (lvalue_expr … H1);
177    ##[ #id ##| #e' ##| #e' id ##] #H3;
178    nelim (yields_eq ???? H3);
179    #p3 e3; napply remove_res_sig; nwhd in ⊢ (??%?); nwhd in e3:(??%?); nrewrite > e3;
180    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
181##| #e ty sp l off tr H1 H2;
182    nelim (yields_eq ???? H2); ncases e; #e' ty';
183    #p2 e2; napply remove_res_sig; nrewrite > e2;
184    napply refl;
185##| #ty' ty; napply refl;
186##| #op e ty v1 v tr H1 H2 H3; napply remove_res_sig;
187    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3;
188    nwhd in ⊢ (??%?); nrewrite > H2; napply refl;
189##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; napply remove_res_sig;
190    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
191    nwhd in ⊢ (??%?);
192    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
193    nwhd in ⊢ (??%?);
194    nrewrite > e3; napply refl;
195##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig;
196    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
197    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
198    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
199    napply refl;
200##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig;
201    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
202    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
203    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5;
204    napply refl;
205##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig;
206    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
207    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
208    napply refl;   
209##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig;
210    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?);
211    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
212    nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?);
213    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
214    nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb;
215    napply refl;   
216##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig;
217    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
218    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
219    napply refl;   
220##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig;
221    nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?);
222    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
223    nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?);
224    nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb;
225    nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb;
226    napply refl;
227##| #e ty ty' v1 v tr H1 H2 H3; napply remove_res_sig;
228    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
229    nelim (yields_eq ???? (cast_complete … H2)); #p2 e2; nrewrite > e2;
230    napply refl;
231##| #e ty v l tr H1 H2; napply remove_res_sig;
232    nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
233    napply refl;
234  (* lvalues *)
235 
236 
237 (* FIXME: next two cases produce type checking failures at nqed. *)
238##| napply daemon (*#id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*)
239##|napply daemon; (*#id sp l ty e1 e2; nwhd in ⊢ (???%?); napply (dep_option_rewrite ??????? e1);
240    nrewrite > e2; napply refl;*)
241##| #e ty sp l ofs tr H1 H2; napply remove_res_sig;
242    nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
243    napply refl;
244##| (* careful!  Make sure we do the H2 rewrite before unfolding, or we end up
245       in trouble because there's an equality proof floating around. *)
246    #e i ty sp l ofs id fList delta tr H1 H2 H3 H4; ncases e in H2 H4 ⊢ %;
247    #e' ty' H2; nwhd in H2:(??%?); nrewrite > H2; #H4; napply remove_res_sig;
248    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?);
249    nrewrite > H3; napply refl;
250##| #e i ty sp l ofs id fList tr; ncases e; #e' ty' H1 H2;
251    nwhd in H2:(??%?); nrewrite > H2; #H3; napply remove_res_sig;
252    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; napply refl;
253##] nqed.
254
255ntheorem expr_complete:  ∀ge,env,m.
256 ∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉).
257#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
258
259ntheorem exprlist_complete: ∀ge,env,m,es,vs,tr.
260  eval_exprlist ge env m es vs tr → yields ?? (exec_exprlist ge env m es) (〈vs,tr〉).
261#ge env m es vs tr H; nelim H;
262##[ napply refl;
263##| #e et v vt tr trt H1 H2 H3; napply remove_res_sig;
264    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
265    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
266    napply refl;
267##] nqed.
268
269ntheorem lvalue_complete: ∀ge,env,m.
270 ∀e,sp,l,off,tr. eval_lvalue ge env m e sp l off tr → yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉).
271#ge env m; nelim (expr_lvalue_complete ge env m); /2/; nqed.
272
273nlet rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝
274match l with
275[ Tnil ⇒ True
276| Tcons h t ⇒ P h ∧ P_typelist P t
277].
278
279nlet rec type_ind2l
280  (P:type → Prop) (Q:typelist → Prop)
281  (vo:P Tvoid)
282  (it:∀i,s. P (Tint i s))
283  (fl:∀f. P (Tfloat f))
284  (pt:∀s,t. P t → P (Tpointer s t))
285  (ar:∀s,t,n. P t → P (Tarray s t n))
286  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
287  (st:∀i,fl. P (Tstruct i fl))
288  (un:∀i,fl. P (Tunion i fl))
289  (cp:∀i. P (Tcomp_ptr i))
290  (nl:Q Tnil)
291  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
292 (t:type) on t : P t ≝
293  match t return λt'.P t' with
294  [ Tvoid ⇒ vo
295  | Tint i s ⇒ it i s
296  | Tfloat s ⇒ fl s
297  | Tpointer s t' ⇒ pt s t' (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
298  | Tarray s t' n ⇒ ar s t' n (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
299  | Tfunction tl t' ⇒ fn tl t' (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl) (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t')
300  | Tstruct i fs ⇒ st i fs
301  | Tunion i fs ⇒ un i fs
302  | Tcomp_ptr i ⇒ cp i
303  ]
304and typelist_ind2l
305  (P:type → Prop) (Q:typelist → Prop)
306  (vo:P Tvoid)
307  (it:∀i,s. P (Tint i s))
308  (fl:∀f. P (Tfloat f))
309  (pt:∀s,t. P t → P (Tpointer s t))
310  (ar:∀s,t,n. P t → P (Tarray s t n))
311  (fn:∀tl,t. Q tl → P t → P (Tfunction tl t))
312  (st:∀i,fl. P (Tstruct i fl))
313  (un:∀i,fl. P (Tunion i fl))
314  (cp:∀i. P (Tcomp_ptr i))
315  (nl:Q Tnil)
316  (cs:∀t,tl. P t → Q tl → Q (Tcons t tl))
317  (ts:typelist) on ts : Q ts ≝
318  match ts return λts'.Q ts' with
319  [ Tnil ⇒ nl
320  | Tcons t tl ⇒ cs t tl (type_ind2l P Q vo it fl pt ar fn st un cp nl cs t)
321                     (typelist_ind2l P Q vo it fl pt ar fn st un cp nl cs tl)
322  ].
323
324naxiom assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
325(*nlemma assert_type_eq_true: ∀t. ∃p.assert_type_eq t t = OK ? p.
326#t; napply (type_ind2l ? (λtl. ∃p.assert_typelist_eq tl tl = OK ? p) … t);
327##[ @ (refl ??); // ##| #sz si; ncases sz; ncases si; @ (refl ??); //;
328##| #sz; ncases sz; @ ?; //;
329##| #sp ty IH; ncases sp; nwhd in ⊢ (??(λ_.??%?)); nelim IH; #p IH; nrewrite > IH; @ ?; //;
330##| #sp ty n IH; ncases sp; nwhd in ⊢ (??(λ_.??%?)); nelim IH; #p IH; nrewrite > IH;
331    nwhd in ⊢ (??(λ_.??%?)); ncases (decidable_eq_Z_Type n n);
332    ##[ ##1,3,5,7,9,11: #H; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
333    ##| ##*: #H; napply False_ind; /2/;
334    ##]
335##| #tys ty IH1 IH2; @ ?;
336    ##[ ##2: nwhd in ⊢ (??%?); nelim IH1; #p1 e1;
337    nrewrite > e1; nwhd in ⊢ (??%?);
338    nelim IH2;
339    *)
340
341nlemma is_not_void_true: ∀f. ¬fn_return f = Tvoid → ∃p. is_not_void (fn_return f) = OK ? p.
342#f; ncases f; #ty; #_; #_; #_; ncases ty;
343##[ #H; napply False_ind; /2/;
344##| #sz sg e; @ ?; //; ##| #sz e; @ ?; // ##| #sp ty e; @ ?; // ##| #sp ty n e; @ ?; // ##|
345    #tys ty e; @ ?; // ##| #id fs e; @ ?; // ##| #id fs e; @ ?; // ##| #id e; @ ?; // ##]
346nqed.
347
348nlemma alloc_vars_complete: ∀env,m,l,env',m'.
349  alloc_variables env m l env' m' →
350  ∃p.exec_alloc_variables env m l = sig_intro ?? (Some ? 〈env', m'〉) p.
351#env m l env' m' H; nelim H;
352##[ #env'' m''; @ ?; nwhd; //;
353##| #env1 m1 id ty l1 m2 loc m3 env2 H1 H2 H3;
354    nwhd in H1:(??%?) ⊢ (??(λ_.??%?));
355    ndestruct (H1);
356    nelim H3; #p3 e3; nrewrite > e3; nwhd in ⊢ (??(λ_.??%?)); @ ?; //;
357##] nqed.
358
359nlemma bind_params_complete: ∀e,m,params,vs,m2.
360  bind_parameters e m params vs m2 →
361  yields ?? (exec_bind_parameters e m params vs) m2.
362#e m params vs m2 H; nelim H;
363##[ //;
364##| #env1 m1 id ty l v tl loc m2 m3 H1 H2 H3 H4;
365    napply remove_res_sig;
366    nrewrite > H1; nwhd in ⊢ (??%?);
367    nrewrite > H2; nwhd in ⊢ (??%?);
368    nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4;
369    napply refl;
370##] nqed.
371
372nlemma eventval_match_complete: ∀ev,ty,v.
373  eventval_match ev ty v → yields ?? (check_eventval ev ty) v.
374#ev ty v H; nelim H; //; nqed.
375
376nlemma eventval_match_complete': ∀ev,ty,v.
377  eventval_match ev ty v → yields ?? (check_eventval' v ty) ev.
378#ev ty v H; nelim H; //; nqed.
379
380nlemma eventval_list_match_complete: ∀vs,tys,evs.
381  eventval_list_match evs tys vs → yields ?? (check_eventval_list vs tys) evs.
382#vs tys evs H; nelim H;
383##[ //
384##| #e etl ty tytl v vtl H1 H2 H3; napply remove_res_sig;
385    nelim (yields_eq ???? (eventval_match_complete' … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
386    nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
387    napply refl;
388##] nqed.   
389
390
391ntheorem step_complete: ∀ge,s,tr,s'.
392  step ge s tr s' → yieldsIO ?? (exec_step ge s) 〈tr,s'〉.
393#ge s tr s' H; nelim H;
394##[ #f e e1 k e2 m sp loc ofs v m' tr1 tr2 H1 H2 H3; napply remove_io_sig;
395    nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
396    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
397    nrewrite > H3; napply refl;
398##| #f e eargs k ef m vf vargs f' tr1 tr2 H1 H2 H3 H4; napply remove_io_sig;
399    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
400    nelim (yields_eq ???? (exprlist_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
401    nrewrite > H3; nwhd in ⊢ (??%?);
402    nrewrite > H4; nelim (assert_type_eq_true (typeof e)); #pty ety; nrewrite > ety;
403    napply refl;
404##| #f el ef eargs k env m sp loc ofs vf vargs f' tr1 tr2 tr3 H1 H2 H3 H4 H5; napply remove_io_sig;
405    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
406    nelim (yields_eq ???? (exprlist_complete … H3)); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?);
407    nrewrite > H4; nwhd in ⊢ (??%?);
408    nrewrite > H5; nelim (assert_type_eq_true (typeof ef)); #pty ety; nrewrite > ety;
409    nwhd in ⊢ (??%?);
410    nelim (yields_eq ???? (lvalue_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
411    napply refl;
412##| #f s1 s2 k env m; napply refl
413##| ##5,6,7: #f s k env m; napply refl
414##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
415    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
416    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
417    napply refl
418##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
419    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
420    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
421    napply refl
422##| #f e s k env m v tr H1 H2; napply remove_io_sig;
423    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
424    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
425    napply refl
426##| #f e s k env m v tr H1 H2; napply remove_io_sig;
427    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
428    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
429    napply refl
430##| #f s1 e s2 k env m H; ncases H; #es1; nrewrite > es1; napply refl;
431##| ##13,14: #f e s k env m; napply refl
432##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig;
433    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
434    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
435    napply refl
436##| #f s1 e s2 k env m v tr; *; #es1; nrewrite > es1; #H1 H2; napply remove_io_sig;
437    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
438    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
439    napply refl
440##| #f e s k env m; napply refl;
441##| #f s1 e s2 s3 k env m nskip; nwhd in ⊢ (???%?); ncases (is_Sskip s1);
442    ##[ #H; napply False_ind; /2/;
443    ##| #H; napply remove_io_sig; napply refl ##]
444##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
445    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
446    nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2;
447    napply refl;
448##| #f e s1 s2 k env m v tr H1 H2; napply remove_io_sig;
449    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
450    nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2;
451    napply refl;
452##| #f s1 e s2 s3 k env m; *; #es1; nrewrite > es1; napply refl;
453##| ##22,23: #f e s1 s2 k env m; napply refl;
454##| napply daemon (* FIXME: rewrite causes failure at nqed  #f k env m H; nwhd in ⊢ (???%?); nrewrite > H; napply refl;*)
455##| #f e k env m v tr H1 H2; napply remove_io_sig;
456    nelim (is_not_void_true f H1); #pf ef; nrewrite > ef; nwhd in ⊢ (??%?);
457    nelim (yields_eq ???? (expr_complete … H2)); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?);
458    napply refl;
459##| #f k env m; ncases k;
460    ##[ #H1 H2; napply daemon (* FIXME nwhd in ⊢ (???%?); nrewrite > H2; napply refl; *)
461    ##| #s' k'; nwhd in ⊢ (% → ?); *;
462    ##| ##3,4: #e' s' k'; nwhd in ⊢ (% → ?); *;
463    ##| ##5,6: #e' s1' s2' k'; nwhd in ⊢ (% → ?); *;
464    ##| #k'; nwhd in ⊢ (% → ?); *;
465    ##| #r f' env' k' H1 H2; napply daemon (* FIXME typing error at nqed nwhd in ⊢ (???%?); nrewrite > H2; napply refl *)
466    ##]
467##| #f e s k env m i tr H1; napply remove_io_sig;
468    nelim (yields_eq ???? (expr_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
469    napply refl
470##| #f s k env m; napply daemon (* FIXME *; #es; nrewrite > es; napply refl;*)
471##| #f k env m; napply refl
472##| #f l s k env m; napply refl
473##| #f l k env m s k' H1; napply daemon(* FIXME nwhd in ⊢ (???%?); nrewrite > H1; napply refl; *)
474##| #f args k m1 env m2 m3 H1 H2; napply remove_io_sig;
475    nelim (alloc_vars_complete … H1); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
476    nelim (yields_eq ???? (bind_params_complete … H2)); #p2 e2; nrewrite > e2;
477    napply refl;
478##| #id tys rty args k m rv tr H; napply remove_io_sig;
479    ninversion H; #f' args' rv' eargs erv H1 H2 e1 e2 e3 e4; nrewrite < e1 in H1 H2;
480    #H1 H2;
481    nelim (yields_eq ???? (eventval_list_match_complete … H1)); #p1 e1; nrewrite > e1; nwhd in ⊢ (??%?);
482    nwhd; @ erv; nwhd in ⊢ (??%?);
483    nelim (yields_eq ???? (eventval_match_complete … H2)); #p2 e2; nrewrite > e2; napply refl
484##| #v f env k m; nwhd in ⊢ (???%?); napply daemon (* FIXME: inductive semantics allows any value ?! *)
485##| #v f env k m1 m2 sp loc ofs ty H; napply remove_io_sig;
486    nrewrite > H; napply refl
487##| #f l s k env m; napply refl
488##] nqed.
489 
Note: See TracBrowser for help on using the repository browser.