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