source: C-semantics/CexecIOcomplete.ma @ 226

Last change on this file since 226 was 226, checked in by campbell, 10 years ago

Some incomplete work on completeness of CexecIO wrt Csem.
Features some rather nasty induction principles.

File size: 11.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].
6ndefinition 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(*
9ndefinition yields : ∀A.∀P:A → Prop. res (sigma A P) → A → Prop ≝
10λA,P,e,v. err_eject A P e = OK ? v.
11*)
12nlemma 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 ⊢ (??%?);
16nelim (pointer_compat_dec (block_space m b) sp);
17##[ //
18##| #H'; napply False_ind; napply (absurd … H H');
19##] nqed.
20
21nlemma ms_eq_dec_true: ∀s. ms_eq_dec s s = inl ???.
22##[ #s; ncases s; napply refl;
23##| ##skip
24##] nqed.
25
26notation < "vbox( e break ↓ break e')" with precedence 99 for @{'yields ${e} ${e'}}.
27interpretation "yields" 'yields e e' = (yields ?? e e').
28interpretation "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'})}.*)
31notation < "vbox( e ;: break e' )" with precedence 40 for @{'binde ${e} ${e'}}.
32notation < "vbox( ident v ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v}. ${e'})}.
33notation < "vbox( ident v : ty ← e ;: break e' )" with precedence 40 for @{'binde ${e} (λ${ident v} : ${ty}. ${e'})}.
34interpretation "error monad bind" 'binde e f = (bind ? ? e f).
35(*interpretation "error monad bind" 'bindnat e f = (bind nat nat e f).*)
36
37nlemma 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
41ntheorem is_det: ∀p,s,s'.
42initial_state p s → initial_state p s' → s = s'.
43#p s s' H1 H2;
44ninversion H1; #b1 f1 e11 e12 e13;
45ninversion H2; #b2 f2 e21 e22 e23;
46nrewrite > 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
55ndefinition yieldsIObare ≝ λA.λa:IO eventval io_out A.λv':A.
56match a with [ Value v ⇒ v' = v | _ ⇒ False ].
57
58nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
59yieldsIObare A a v' →
60yieldsIO 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
68ntheorem 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;
71napply remove_io_sig;
72ninversion H;
73#b f e1 e2 e3;
74nrewrite > e1;
75nwhd in ⊢ (??%?);
76nrewrite > e2;
77nwhd; napply refl;
78nqed.
79
80ndefinition yieldsbare ≝ λA.λa:res A.λv':A.
81match a with [ OK v ⇒ v' = v | _ ⇒ False ].
82
83nlemma remove_res_sig: ∀A. ∀P:A → Prop. ∀a,v',p.
84yieldsbare A a v' →
85yields 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
91nlemma 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;
94nelim 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
110nlemma 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(*
116nlemma 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. *)
130nlemma 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
142nlemma 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  ##]
153nqed.
154
155nlemma 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  ##]
163nqed.
164
165nlemma 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  ##]
171nqed.
172
173nremark eq_to_jmeq: ∀A. ∀a,b:A. a = b → a ≃ b.
174#A a b H; nrewrite > H; //; nqed.
175
176nlemma 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 ⊢ (? → ???%?);
181napply (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
186nlemma 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;
190napply (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
Note: See TracBrowser for help on using the repository browser.