source: C-semantics/CexecIOcomplete.ma @ 226

Last change on this file since 226 was 226, checked in by campbell, 9 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.