Changeset 239 for Csemantics/CexecIOcomplete.ma
 Timestamp:
 Nov 12, 2010, 7:16:52 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/CexecIOcomplete.ma
r226 r239 4 4 ndefinition yields : ∀A,P. res (Σx:A. P x) → A → Prop ≝ 5 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 *) 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 12 17 nlemma is_pointer_compat_true: ∀m,b,sp. 13 18 pointer_compat (block_space m b) sp → … … 27 32 interpretation "yields" 'yields e e' = (yields ?? e e'). 28 33 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 34 41 35 ntheorem is_det: ∀p,s,s'. … … 53 47 ##] nqed. 54 48 55 n definition yieldsIObare ≝ λA.λa:IO eventval io_out A.λv':A.56 match a with [ Value v ⇒ v' = v  _ ⇒ False ].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 ]. 57 51 58 52 nlemma remove_io_sig: ∀A. ∀P:A → Prop. ∀a,v',p. 59 53 yieldsIObare A a v' → 60 54 yieldsIO A P (io_inject eventval io_out A (λx.P x) (Some ? a) p) v'. 61 #A P a; n casesa;62 ##[ #a b c d; *;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'; 63 57 ## #v v' p H; napply H; 64 58 ## #a b; *; … … 113 107 ## *; 114 108 ##] 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 109 129 110 (* Use to narrow down the choice of expression to just the lvalues. *) … … 184 165 ##] nqed. 185 166 186 nlemma expr_ complete: ∀ge,env,m.167 nlemma expr_lvalue_complete: ∀ge,env,m. 187 168 (∀e,v,tr. eval_expr ge env m e v tr → yields ?? (exec_expr ge env m e) (〈v,tr〉)) ∧ 188 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〉)). … … 255 236 256 237 (* FIXME: next two cases produce type checking failures at nqed. *) 257 ## napply daemon; (*#id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*)238 ## napply daemon (*#id l ty e1; nwhd in ⊢ (???%?); nrewrite > e1; napply refl;*) 258 239 ##napply daemon; (*#id sp l ty e1 e2; nwhd in ⊢ (???%?); napply (dep_option_rewrite ??????? e1); 259 240 nrewrite > e2; napply refl;*) … … 272 253 ##] nqed. 273 254 274 255 ntheorem 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 259 ntheorem 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 269 ntheorem 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 273 nlet rec P_typelist (P:type → Prop) (l:typelist) on l : Prop ≝ 274 match l with 275 [ Tnil ⇒ True 276  Tcons h t ⇒ P h ∧ P_typelist P t 277 ]. 278 279 nlet 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 ] 304 and 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 324 naxiom 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 341 nlemma 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; @ ?; // ##] 346 nqed. 347 348 nlemma 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 359 nlemma 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 372 nlemma 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 376 nlemma 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 380 nlemma 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 391 ntheorem 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 TracChangeset
for help on using the changeset viewer.