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 | ndefinition yieldsIO : ∀A,P. IO eventval io_out (Σx:A. P x) → A → Prop ≝ |
---|
7 | λA,P,e,v. match e with [ Value v' ⇒ match v' with [ sig_intro v'' _ ⇒ v = v'' ] | _ ⇒ False]. |
---|
8 | (* |
---|
9 | ndefinition yields : ∀A.∀P:A → Prop. res (sigma A P) → A → Prop ≝ |
---|
10 | λA,P,e,v. err_eject A P e = OK ? v. |
---|
11 | *) |
---|
12 | nlemma is_pointer_compat_true: ∀m,b,sp. |
---|
13 | pointer_compat (block_space m b) sp → |
---|
14 | is_pointer_compat (block_space m b) sp = true. |
---|
15 | #m b sp H; nwhd in ⊢ (??%?); |
---|
16 | nelim (pointer_compat_dec (block_space m b) sp); |
---|
17 | ##[ // |
---|
18 | ##| #H'; napply False_ind; napply (absurd … H H'); |
---|
19 | ##] nqed. |
---|
20 | |
---|
21 | nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???. |
---|
22 | ##[ #s; ncases s; napply refl; |
---|
23 | ##| ##skip |
---|
24 | ##] nqed. |
---|
25 | |
---|
26 | notation < "vbox( e break ↓ break e')" with precedence 99 for @{'yields ${e} ${e'}}. |
---|
27 | interpretation "yields" 'yields e e' = (yields ?? e e'). |
---|
28 | interpretation "yields IO" 'yields e e' = (yieldsIO ?? e e'). |
---|
29 | (* |
---|
30 | (*notation < "vbox( ident v ← e;: break e' )" with precedence 40 for @{'bindnat ${e} (\lambda ${ident v} : ${ty}. ${e'})}.*) |
---|
31 | notation < "vbox( e ;: break e' )" with precedence 40 for @{'binde ${e} ${e'}}. |
---|
32 | notation < "vbox( ident v ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v}. ${e'})}. |
---|
33 | notation < "vbox( ident v : ty ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v} : ${ty}. ${e'})}. |
---|
34 | interpretation "error monad bind" 'binde e f = (bind ? ? e f). |
---|
35 | (*interpretation "error monad bind" 'bindnat e f = (bind nat nat e f).*) |
---|
36 | |
---|
37 | nlemma foo: ∀e:res nat. ∀f: nat → res nat. (x ← e;: f x) = OK ? 5. |
---|
38 | *) |
---|
39 | (*interpretation "error monad bind" 'bind e f = (bind ? ? e f).*) |
---|
40 | |
---|
41 | ntheorem is_det: ∀p,s,s'. |
---|
42 | initial_state p s → initial_state p s' → s = s'. |
---|
43 | #p s s' H1 H2; |
---|
44 | ninversion H1; #b1 f1 e11 e12 e13; |
---|
45 | ninversion H2; #b2 f2 e21 e22 e23; |
---|
46 | nrewrite > e11 in e21; |
---|
47 | #e1; nrewrite > (?:b1 = b2) in e12; |
---|
48 | ##[ nrewrite > e22; #e2; nrewrite > (?:f2 = f1); |
---|
49 | ##[ //; |
---|
50 | ##| ndestruct (e2) skip (e22 e23); //; |
---|
51 | ##] |
---|
52 | ##| ndestruct (e1) skip (e11); // |
---|
53 | ##] nqed. |
---|
54 | |
---|
55 | ndefinition yieldsIObare ≝ λA.λa:IO eventval io_out A.λv':A. |
---|
56 | match a with [ Value v ⇒ v' = v | _ ⇒ False ]. |
---|
57 | |
---|
58 | nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p. |
---|
59 | yieldsIObare A a v' → |
---|
60 | yieldsIO A P (io_inject eventval io_out A (λx.P x) (Some ? a) p) v'. |
---|
61 | #A P a; ncases a; |
---|
62 | ##[ #a b c d; *; |
---|
63 | ##| #v v' p H; napply H; |
---|
64 | ##| #a b; *; |
---|
65 | ##] nqed. |
---|
66 | |
---|
67 | |
---|
68 | ntheorem the_initial_state: |
---|
69 | ∀p,s. initial_state p s → yieldsIO ?? (make_initial_state p) s. |
---|
70 | #p s; ncases p; #fns main globs H; |
---|
71 | napply remove_io_sig; |
---|
72 | ninversion H; |
---|
73 | #b f e1 e2 e3; |
---|
74 | nrewrite > e1; |
---|
75 | nwhd in ⊢ (??%?); |
---|
76 | nrewrite > e2; |
---|
77 | nwhd; napply refl; |
---|
78 | nqed. |
---|
79 | |
---|
80 | ndefinition yieldsbare ≝ λA.λa:res A.λv':A. |
---|
81 | match a with [ OK v ⇒ v' = v | _ ⇒ False ]. |
---|
82 | |
---|
83 | nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p. |
---|
84 | yieldsbare A a v' → |
---|
85 | yields A P (err_inject A (λx.P x) (Some ? a) p) v'. |
---|
86 | #A P a; ncases a; |
---|
87 | ##[ #v v' p H; napply H; |
---|
88 | ##| #a b; *; |
---|
89 | ##] nqed. |
---|
90 | |
---|
91 | nlemma cast_complete: ∀m,v,ty,ty',v'. |
---|
92 | cast m v ty ty' v' → yields ?? (exec_cast m v ty ty') v'. |
---|
93 | #m v ty ty' v' H; |
---|
94 | nelim H; |
---|
95 | ##[ #m i sz1 sz2 sg1 sg2; napply refl; |
---|
96 | ##| #m f sz szi sg; napply refl; |
---|
97 | ##| #m i sz sz' sg; napply refl; |
---|
98 | ##| #m f sz sz'; napply refl; |
---|
99 | ##| #m sp sp' ty ty' b ofs H1 H2 H3; napply remove_res_sig; |
---|
100 | nelim H1; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #tys1 ty1; nletin sp1 ≝ Code ##] |
---|
101 | nwhd in ⊢ (??%?); |
---|
102 | ##[ ##1,2: nrewrite > (ms_eq_dec_true …); nwhd in ⊢ (??%?); ##] |
---|
103 | nelim H2 in H3 ⊢ %; ##[ ##1,4,7: #sp2 ty2 ##| ##2,5,8: #sp2 ty2 n2 ##| ##3,6,9: #tys2 ty2; nletin sp2 ≝ Code ##] |
---|
104 | #H3; nwhd in ⊢ (??%?); |
---|
105 | nrewrite > (is_pointer_compat_true …); //; |
---|
106 | ##| #m sz si ty'' H; ncases H; ##[ #sp1 ty1 ##| #sp1 ty1 n1 ##| #args rty ##] napply refl; |
---|
107 | ##| #m t t' H H'; ncases H; ncases H'; //; |
---|
108 | ##] nqed. |
---|
109 | |
---|
110 | nlemma yields_eq: ∀A,P,e,v. yields A P e v → ∃p. e = OK ? (sig_intro … v p). |
---|
111 | #A P e v; ncases e; |
---|
112 | ##[ #vp; ncases vp; #v' p H; nwhd in H; nrewrite > H; @ p; napply refl; |
---|
113 | ##| *; |
---|
114 | ##] nqed. |
---|
115 | (* |
---|
116 | nlemma lvalue_complete_cond: ∀ge,env,m. |
---|
117 | (∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) → |
---|
118 | (∀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〉)). |
---|
119 | #ge env m IH; |
---|
120 | #e sp l off tr H; napply (eval_lvalue_ind … H); |
---|
121 | ##[ #id l ty H1; nwhd in ⊢ (???%?); |
---|
122 | nrewrite > H1; |
---|
123 | napply refl; |
---|
124 | ##| #id sp l ty H1 H2; nwhd in ⊢ (???%?); |
---|
125 | nrewrite > H1; nwhd nodelta in ⊢ (???%?); napply remove_res_sig; |
---|
126 | nrewrite > H2; |
---|
127 | *) |
---|
128 | |
---|
129 | (* Use to narrow down the choice of expression to just the lvalues. *) |
---|
130 | nlemma lvalue_expr: ∀ge,env,m,e,ty,sp,l,ofs,tr. ∀P:expr_descr → Prop. |
---|
131 | eval_lvalue ge env m (Expr e ty) sp l ofs tr → |
---|
132 | (∀id. P (Evar id)) → (∀e'. P (Ederef e')) → (∀e',id. P (Efield e' id)) → |
---|
133 | P e. |
---|
134 | #ge env m e ty sp l ofs tr P H; napply (eval_lvalue_inv_ind … H); |
---|
135 | ##[ #id l ty e1 e2 e3 e4 e5 e6; ndestruct; // |
---|
136 | ##| #id sp l ty e1 e2 e3 e4 e5 e6 e7; ndestruct; // |
---|
137 | ##| #e ty sp l ofs tr H e1 e2 e3 e4 e5; ndestruct; // |
---|
138 | ##| #e id ty sp l ofs id' fs d tr H e1 e2;(* bogus? *) #_; #e3 e4 e5 e6 e7; ndestruct; // |
---|
139 | ##| #e id ty sp l ofs id' fs tr H e1;(* bogus? *) #_; #e2 e3 e4 e5 e6; ndestruct; // |
---|
140 | ##] nqed. |
---|
141 | |
---|
142 | nlemma 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. |
---|
143 | #v ty r H; nelim H; #v t H'; nelim H'; |
---|
144 | ##[ #i is s ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; |
---|
145 | ##| #p b i i0 s; @ true; @; // |
---|
146 | ##| #i p t ne; @ true; @; //; nwhd; nrewrite > (eq_false … ne); //; |
---|
147 | ##| #p b i p0 t0; @ true; @; // |
---|
148 | ##| #f s ne; @ true; @; //; nwhd; nrewrite > (Feq_zero_false … ne); //; |
---|
149 | ##| #i s; @ false; @; //; |
---|
150 | ##| #p t; @ false; @; //; |
---|
151 | ##| #s; @ false; @; //; nwhd; nrewrite > (Feq_zero_true …); //; |
---|
152 | ##] |
---|
153 | nqed. |
---|
154 | |
---|
155 | nlemma bool_of_true: ∀v,ty. is_true v ty → yields ?? (bool_of_val_3 v ty) true. |
---|
156 | #v ty H; nelim H; |
---|
157 | ##[ #i is s ne; nwhd; nrewrite > (eq_false … ne); //; |
---|
158 | ##| #p b i i0 s; // |
---|
159 | ##| #i p t ne; nwhd; nrewrite > (eq_false … ne); //; |
---|
160 | ##| #p b i p0 t0; // |
---|
161 | ##| #f s ne; nwhd; nrewrite > (Feq_zero_false … ne); //; |
---|
162 | ##] |
---|
163 | nqed. |
---|
164 | |
---|
165 | nlemma bool_of_false: ∀v,ty. is_false v ty → yields ?? (bool_of_val_3 v ty) false. |
---|
166 | #v ty H; nelim H; |
---|
167 | ##[ #i s; //; |
---|
168 | ##| #p t; //; |
---|
169 | ##| #s; nwhd; nrewrite > (Feq_zero_true …); //; |
---|
170 | ##] |
---|
171 | nqed. |
---|
172 | |
---|
173 | nremark eq_to_jmeq: ∀A. ∀a,b:A. a = b → a ≃ b. |
---|
174 | #A a b H; nrewrite > H; //; nqed. |
---|
175 | |
---|
176 | 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. |
---|
177 | yields ?? (Q (eq_to_jmeq ??? h)) r → |
---|
178 | yields ?? ((match e return λe'.e ≃ e' → ? with [ None ⇒ λp.Q p | Some v ⇒ λp.R v p ]) (refl_jmeq (option A) e)) r. |
---|
179 | #A B e; ncases e; |
---|
180 | ##[ #r P Q R h; nwhd in ⊢ (? → ???%?); |
---|
181 | napply (streicherKjmeq ?? (λe. yields ?? (Q e) r → yields ?? (Q (refl_jmeq (option A) (None A))) r)); |
---|
182 | //; |
---|
183 | ##| #v r P Q R h; ndestruct (h); |
---|
184 | ##] nqed. |
---|
185 | |
---|
186 | nlemma expr_complete: ∀ge,env,m. |
---|
187 | (∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) ∧ |
---|
188 | (∀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〉)). |
---|
189 | #ge env m; |
---|
190 | napply (combined_expr_lvalue_ind ge env m |
---|
191 | (λe,v,tr,H. yields ?? (exec_expr ge env m e) (〈v,tr〉)) |
---|
192 | (λe,sp,l,off,tr,H. yields ?? (exec_lvalue ge env m e) (〈〈〈sp,l〉,off〉,tr〉))); |
---|
193 | ##[ #i ty; napply refl; |
---|
194 | ##| #f ty; napply refl; |
---|
195 | ##| #e ty sp l off v tr H1 H2; napply (lvalue_expr … H1); |
---|
196 | ##[ #id ##| #e' ##| #e' id ##] #H3; |
---|
197 | nelim (yields_eq ???? H3); |
---|
198 | #p3 e3; napply remove_res_sig; nwhd in ⊢ (??%?); nwhd in e3:(??%?); nrewrite > e3; |
---|
199 | nwhd in ⊢ (??%?); nrewrite > H2; napply refl; |
---|
200 | ##| #e ty sp l off tr H1 H2; |
---|
201 | nelim (yields_eq ???? H2); ncases e; #e' ty'; |
---|
202 | #p2 e2; napply remove_res_sig; nrewrite > e2; |
---|
203 | napply refl; |
---|
204 | ##| #ty' ty; napply refl; |
---|
205 | ##| #op e ty v1 v tr H1 H2 H3; napply remove_res_sig; |
---|
206 | nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; |
---|
207 | nwhd in ⊢ (??%?); nrewrite > H2; napply refl; |
---|
208 | ##| #op e1 e2 ty v1 v2 v tr1 tr2 H1 H2 e3 H4 H5; napply remove_res_sig; |
---|
209 | nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; |
---|
210 | nwhd in ⊢ (??%?); |
---|
211 | nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; |
---|
212 | nwhd in ⊢ (??%?); |
---|
213 | nrewrite > e3; napply refl; |
---|
214 | ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig; |
---|
215 | nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?); |
---|
216 | nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; |
---|
217 | nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; |
---|
218 | napply refl; |
---|
219 | ##| #e1 e2 e3 ty v1 v2 tr1 tr2 H1 H2 H3 H4 H5; napply remove_res_sig; |
---|
220 | nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?); |
---|
221 | nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; |
---|
222 | nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; |
---|
223 | napply refl; |
---|
224 | ##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig; |
---|
225 | nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); |
---|
226 | nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; |
---|
227 | napply refl; |
---|
228 | ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig; |
---|
229 | nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?); |
---|
230 | nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; |
---|
231 | nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?); |
---|
232 | nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb; |
---|
233 | nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb; |
---|
234 | napply refl; |
---|
235 | ##| #e1 e2 ty v1 tr H1 H2 H3; napply remove_res_sig; |
---|
236 | nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); |
---|
237 | nelim (yields_eq ???? (bool_of_false ?? H2)); #p2 e2; nrewrite > e2; |
---|
238 | napply refl; |
---|
239 | ##| #e1 e2 ty v1 v2 v tr1 tr2 H1 H2 H3 H4 H5 H6; napply remove_res_sig; |
---|
240 | nelim (yields_eq ???? H5); #p5 e5; nrewrite > e5; nwhd in ⊢ (??%?); |
---|
241 | nelim (yields_eq ???? (bool_of_true ?? H2)); #p2 e2; nrewrite > e2; |
---|
242 | nelim (yields_eq ???? H6); #p6 e6; nrewrite > e6; nwhd in ⊢ (??%?); |
---|
243 | nelim (bool_of_val_3_complete … H4); #b; *; #evb Hb; |
---|
244 | nelim (yields_eq ???? Hb); #pb eb; nrewrite > eb; nwhd in ⊢ (??%?); nrewrite < evb; |
---|
245 | napply refl; |
---|
246 | ##| #e ty ty' v1 v tr H1 H2 H3; napply remove_res_sig; |
---|
247 | nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; nwhd in ⊢ (??%?); |
---|
248 | nelim (yields_eq ???? (cast_complete … H2)); #p2 e2; nrewrite > e2; |
---|
249 | napply refl; |
---|
250 | ##| #e ty v l tr H1 H2; napply remove_res_sig; |
---|
251 | nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?); |
---|
252 | napply refl; |
---|
253 | (* lvalues *) |
---|
254 | |
---|
255 | |
---|
256 | (* FIXME: next two cases produce type checking failures at nqed. *) |
---|
257 | ##|napply daemon; (* #id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*) |
---|
258 | ##|napply daemon; (*#id sp l ty e1 e2; nwhd in ⊢ (???%?); napply (dep_option_rewrite ??????? e1); |
---|
259 | nrewrite > e2; napply refl;*) |
---|
260 | ##| #e ty sp l ofs tr H1 H2; napply remove_res_sig; |
---|
261 | nelim (yields_eq ???? H2); #p2 e2; nrewrite > e2; nwhd in ⊢ (??%?); |
---|
262 | napply refl; |
---|
263 | ##| (* careful! Make sure we do the H2 rewrite before unfolding, or we end up |
---|
264 | in trouble because there's an equality proof floating around. *) |
---|
265 | #e i ty sp l ofs id fList delta tr H1 H2 H3 H4; ncases e in H2 H4 ⊢ %; |
---|
266 | #e' ty' H2; nwhd in H2:(??%?); nrewrite > H2; #H4; napply remove_res_sig; |
---|
267 | nelim (yields_eq ???? H4); #p4 e4; nrewrite > e4; nwhd in ⊢ (??%?); |
---|
268 | nrewrite > H3; napply refl; |
---|
269 | ##| #e i ty sp l ofs id fList tr; ncases e; #e' ty' H1 H2; |
---|
270 | nwhd in H2:(??%?); nrewrite > H2; #H3; napply remove_res_sig; |
---|
271 | nelim (yields_eq ???? H3); #p3 e3; nrewrite > e3; napply refl; |
---|
272 | ##] nqed. |
---|
273 | |
---|
274 | |
---|