Changeset 3118
 Timestamp:
 Apr 10, 2013, 6:45:40 PM (4 years ago)
 Files:

 2 added
 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/StatusSimulationHelper.ma
r3050 r3118 140 140 return res. 141 141 142 lemma partial_inj_sigma : 142 143 144 145 lemma partial_inj_sigma_label : 143 146 ∀p_in,p_out,prog,stack_size,init,init_regs. 144 147 ∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2. … … 199 202 [2,3: @⊥ [ >Hbl in Hbl1;  >Hbl1 in Hbl;] #H @H % 4: %] 200 203 whd in match (offset_of_point ??) in EQpt2; 201 <EQpt1 in EQpt2; #H lapply(partial_inj_sigma … (sym_eq ??? H))204 <EQpt1 in EQpt2; #H lapply(partial_inj_sigma_label … (sym_eq ??? H)) 202 205 [ >EQpt1 % #EQ prog destruct(EQ)] whd in match point_of_pc; normalize nodelta 203 206 whd in match (point_of_offset ??); whd in match (point_of_offset ??); … … 246 249 #EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H) 247 250 qed. 251 252 lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params. 253 ∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl. 254 In ? (stmt_labels p ? stmt) lbl→ 255 fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 → 256 pc' = pc_of_point p (pc_block pc) lbl → 257 ∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉. 258 #p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch 259 cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt 260 #EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) * 261 cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?) 262 [3: * cases lbl #x #y cases(decidable_eq_pos … x y) 263 [#EQ destruct % %  * #H %2 % #H1 @H destruct %] 264  whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct 265 whd in match code_has_label; whd in match code_has_point; normalize nodelta 266 inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'} 267 whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind 268 >point_of_pc_of_point >EQstmt' % 269  #H lapply(In_all ??? H) H cases(Exists_append … Hlbl) 270 [ cases stmt [ #step #nxt  #fin  *] whd in match stmt_implicit_label; 271 normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_ 272 whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta 273 inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'} 274 whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind 275 >point_of_pc_of_point >EQstmt' % 276  #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H % 277 ] 278 ] 279 qed. 280 281 282 lemma fetch_stmt_ok_nxt_ok : ∀p : sem_graph_params. 283 ∀prog : joint_program p.∀stack_size,f,fn,stmt,bl,pt,nxt. 284 fetch_internal_function … (joint_globalenv p prog stack_size) bl = 285 return 〈f,fn〉→ 286 stmt_at p … (joint_if_code … fn) pt = return sequential p ? stmt nxt → 287 ∃stmt'. 288 stmt_at p … (joint_if_code … fn) nxt = return stmt'. 289 #p #prog #stack_size #f #fn #stmt #bl #pt #nxt #EQfn #EQstmt 290 cases(fetch_stmt_ok_succ_ok … 291 prog stack_size f fn (sequential p … stmt nxt) (pc_of_point p bl pt) 292 (pc_of_point p bl nxt) nxt ???) 293 [ #stmt' #H cases(fetch_statement_inv … H) H #_ >point_of_pc_of_point normalize nodelta 294 #EQstmt' %{stmt'} assumption 295  whd in match stmt_labels; normalize nodelta % % 296  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind 297 >point_of_pc_of_point >EQstmt % 298  % 299 ] 300 qed. 301 248 302 249 303 lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs. … … 260 314 [ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt 261 315  S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧ 262 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt 316 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt 263 317 ]. 264 318 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn … … 288 342 whd in match (length ??); #EQn whd in match (length ??); normalize nodelta] 289 343 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq 290 >m_return_bind >EQfn >m_return_bind inversion(find ????)291 [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta344 >m_return_bind >EQfn >m_return_bind inversion(find ????) 345 [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta 292 346 @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind 293 >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length; 294 normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 295 whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit 296 >m_return_bind cases stmt1 in EQfind; stmt1 297 [1,4,7,10,13: #j_step1 #nxt1 2,5,8,11,14: #fin1 *: *] #EQfind normalize nodelta 298 cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *] 299 [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 *: * #pre_instr1 #instr1 ] 300 >m_return_bind cases pre_instr1 pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl] 301 whd in match (length ??); normalize nodelta 302 [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] #EQ #_ >EQ %] 303 whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *] 304 #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] 305 #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥ 306 cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) ** 307 #H #_ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 308 whd in match code_has_point; normalize nodelta >EQstmt @I 347 >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length; 348 normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 349 whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit 350 >m_return_bind cases stmt1 in EQfind; stmt1 351 [1,4,7,10,13: #j_step1 #nxt1 2,5,8,11,14: #fin1 *: *] #EQfind normalize nodelta 352 cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *] 353 [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 *: * #pre_instr1 #instr1 ] 354 >m_return_bind cases pre_instr1 pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl] 355 whd in match (length ??); normalize nodelta 356 [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] 357 #EQ #_ >EQ %] 358 whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *] 359 #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] 360 #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥ 361 cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) 362 ** #H #_ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 363 whd in match code_has_point; normalize nodelta >EQstmt @I 309 364 *: cases syntax_spec syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *] 310 365 cases pre pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?); … … 374 429 qed. 375 430 431 definition stmt_get_next : ∀p,globals.joint_statement p globals → option (succ p) ≝ 432 λp,globals,stmt. 433 match stmt with 434 [sequential stmt nxt ⇒ Some ? nxt 435  _ ⇒ None ? 436 ]. 437 438 439 definition sigma_next : ∀p_in,p_out : sem_graph_params. 440 joint_program p_in → (ident → option ℕ) → 441 (∀globals.joint_closed_internal_function p_in globals 442 →bound_b_graph_translate_data p_in p_out globals) → 443 (block → list register) → lbl_funct_type → regs_funct_type → 444 block → label → option label ≝ 445 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched. 446 ! bl ← code_block_of_block bl ; 447 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … 448 (joint_globalenv p_in prog stack_size) bl); 449 ! 〈res,s〉 ← 450 find ?? (joint_if_code ?? fn) 451 (λlbl.λstmt.match stmt_get_next … stmt with 452 [ None ⇒ false 453  Some nxt ⇒ 454 match preamble_length … prog stack_size init init_regs f_regs bl lbl with 455 [ None ⇒ false 456  Some n ⇒ match nth_opt ? n ((f_lbls bl lbl) @ [nxt]) with 457 [ None ⇒ false 458  Some x ⇒ eq_identifier … searched x 459 ] 460 ] 461 ]); 462 stmt_get_next … s. 463 376 464 lemma fetch_statement_sigma_stored_pc : 377 465 ∀p_in,p_out,prog,stack_sizes, … … 386 474 match stmt with 387 475 [ sequential step nxt ⇒ 388 ∃step_block. bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step) 476 ∃step_block : step_block p_out (prog_names … trans_prog). 477 bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step) 389 478 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧ 390 479 ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 391 480 init_regs f_lbls f_regs pc' = pc ∧ 392 ∃fn',nxt' .481 ∃fn',nxt',l1,l2. 393 482 fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' = 394 483 if not_emptyb … (added_prologue … data) ∧ 395 484 eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn) 396 then return 〈f,fn',sequential ?? (NOOP …) nxt'〉 397 else return 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉 485 then OK ? 〈f,fn',sequential ?? (NOOP …) nxt'〉 486 else OK ? 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉 ∧ 487 seq_list_in_code p_out (prog_names … trans_prog) (joint_if_code … fn') (point_of_pc p_out pc) 488 (map_eval … (\fst (\fst step_block)) (point_of_pc p_out pc')) 489 l1 (point_of_pc p_out pc') 490 ∧ seq_list_in_code p_out ? (joint_if_code … fn') nxt' (\snd step_block) l2 nxt 491 ∧ sigma_next p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc_block pc) nxt' = return nxt 398 492  final fin ⇒ 399 493 ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin) … … 407 501 ]. 408 502 #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt 409 #good #Hbl #EQfetch 410 lapply(b_graph_transform_program_fetch_statement … good pc f fn ?) 411 [2: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta 412 #H cases(H EQfetch) H *:] 413 #data * #t_fn ** #EQt_fn #Hinit #H %{data} >Hinit %{(refl …)} cases stmt in EQfetch H; 414 [ #step #nxt  #fin  *] normalize nodelta #EQfetch stmt 503 #good #Hbl #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta 504 #EQstmt 505 lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn) 506 @eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) H 507 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H 508 lapply(H … EQstmt) H normalize nodelta #H #_ %{data} >Hinit %{(refl …)} 509 EQfetch cases stmt in EQstmt H; 510 [ #step #nxt  #fin  *] normalize nodelta #EQstmt stmt 415 511 [ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta 416 512 [ @eq_identifier_elim #EQentry normalize nodelta ] ] … … 423 519 *: #Hregs #syntax_spec 424 520 ] 425 cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt426 521 [ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt; 427 522 cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ) … … 436 531 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 437 532 5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind 438 normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} 533 normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} %{[ ]} %{[ ]} 439 534 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 440 >EQt_stmt >m_return_bind @eq_identifier_elim [#_ %] * #H @⊥ @H % 535 >EQt_stmt >m_return_bind % 536 [ % [ % [ @eq_identifier_elim [#_ %] * #H @⊥ @H %  %{(refl …) (refl …)}]  %{(refl …) (refl …)}]] 537 whd in match sigma_next; normalize nodelta >code_block_of_block_eq 538 >m_return_bind >EQfn >m_return_bind inversion(find ????) 539 [ #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta 540 >EQpreamble normalize nodelta >EQentry >e0 normalize nodelta 541 @eq_identifier_elim [#_ *] * #H #_ @H %] 542 * #lbl1 #stmt1 #EQfind >m_return_bind lapply(find_predicate ?????? EQfind) 543 inversion(stmt_get_next … stmt1) [#_ *] #nxt1 #EQnxt1 normalize nodelta 544 inversion(preamble_length ?????????) [#_ *] #m whd in match preamble_length; 545 normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 546 whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind 547 >Hinit >m_return_bind cases stmt1 in EQfind; [#j_step #succ  #fin  *] 548 #EQfind normalize nodelta cases(bind_instantiate ???) 549 [1,3: whd in ⊢ (??%% → ?); #EQ destruct] #bl1 >m_return_bind whd in ⊢ (??%? → ?); 550 #EQ destruct(EQ) inversion(nth_opt ???) [1,3: #_ *] #lbl2 #EQlbl2 normalize nodelta 551 @eq_identifier_elim [2,4: #_ *] #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 552 cases(Exists_append … (nth_opt_Exists ???? EQlbl2)) [2,4: * [2,4: *] #EQ >EQ #_ %] 553 #H @⊥ cases(Exists_All … H (fresh_labs lbl1)) #x * #EQ destruct(EQ) ** H #H #_ 554 @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 555 whd in match code_has_point; normalize nodelta 556 cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt2 #EQ >EQ @I 441 557 2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)} 442 558 6,7,8: %{pc} … … 452 568 #EQmid #EQpre whd in ⊢ (% → ?); 453 569 [1,2,3,4: * #nxt1 *] #EQt_stmt 454 [1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2}] 455 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 456 @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?); 457 #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind 458 normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; pre 459 [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); 460 #EQ destruct(EQ)] 461 [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid; 462 [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct] 463 * #mid * #rest ** #EQ destruct(EQ)] 464 [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 465 [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: %] @eq_identifier_elim [2: #_ %] 466 #EQ <EQ in EQentry; * #H @⊥ @H %] 467 * #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??); 468 whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt; 469 lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1 470 >nth_opt_append_r [2,4,6: %] cut(restrest=O) [1,3,5: cases(rest) //] 471 #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 EQ2 EQ1 472 [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt [2: >point_of_pc_of_point %] 473 @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_ 474 >point_of_pc_of_point %] 475 destruct(EQ3) >point_of_pc_of_point >EQt_stmt % 476 qed. 570 [1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2} %{l1} %{l2} %] 571 [1,3,5,7,9,10: whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 572 @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?); 573 #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind 574 normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; pre 575 [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); 576 #EQ destruct(EQ)] 577 [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid; 578 [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct] 579 * #mid * #rest ** #EQ destruct(EQ)] 580 [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 581 [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: % [ %{(refl …)} %{(refl …) (refl …)} ] assumption] 582 @eq_identifier_elim [2: #_ % [ %{(refl …)} %{(refl …) (refl …)}  assumption] ] 583 #EQ <EQ in EQentry; * #H @⊥ @H %] 584 * #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??); 585 whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt; 586 lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1 587 >nth_opt_append_r [2,4,6: %] cut(restrest=O) [1,3,5: cases(rest) //] 588 #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 EQ2 EQ1 589 [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt 590 [2: >point_of_pc_of_point % [%{(refl …)} whd %{mid'} %{rest} % [2: assumption] % [2: assumption] %] 591 assumption] 592 @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_ >point_of_pc_of_point % 593 [ %{(refl …)} whd %{mid'} %{rest} % [ %{(refl …)} assumption ] assumption  assumption ] ] 594 destruct(EQ3) >point_of_pc_of_point >EQt_stmt %] 595 whd in match sigma_next; normalize nodelta >code_block_of_block_eq >m_return_bind 596 >EQfn >m_return_bind inversion(find ????) 597 [1,3,5,7: #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta >EQpreamble 598 normalize nodelta cases post in Hregs EQpost; 599 [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) @('bind_inversion EQpreamble) 600 #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn 601 >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta 602 >Hregs >m_return_bind cases pre in EQpre Hregs; 603 [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct 604 2,4: #fst #remaining] * 605 [1,2: #lab1 * #rest ** #EQ destruct(EQ) * #nxt' * #EQpc change with nxt' in ⊢ (??%? → ?); 606 #EQ destruct(EQ) #Hrest #Hregs whd in match (length ??); whd in ⊢ (??%? → ?); 607 #EQ destruct(EQ) whd in EQmid : (??%%); destruct(EQmid) >e0 608 lapply(seq_list_in_code_length … Hrest) >length_map #EQ >EQ 609 >nth_opt_append_r 610 [2,4: >length_append whd in match (length ? [mid1]); 611 whd in match (length ? [ ]); cases(rest) //] 612 >length_append whd in match (length ? [mid1]); whd in match (length ? [ ]); 613 cut(S (rest)  (rest + 1) = O) 614 [1,3: cases(rest) // #m normalize cases m // #m1 normalize nodelta 615 cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ] 616 #EQ1 >EQ1 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % 617 *: #EQ1 #EQ2 destruct(EQ1 EQ2) #EQregs #_ whd in EQmid : (??%%); destruct(EQmid) 618 >e0 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % 619 ] 620 *: #fst #rems #Hregs * #lab1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQmid2 621 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest @('bind_inversion EQpreamble) 622 #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn 623 >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta 624 >Hregs >m_return_bind cases pre in EQpre Hregs; 625 [1,3,6,8: [3,4: #x #y] #_ #_ whd in ⊢ (??%? → ?); whd in match (length ??); 626 #EQ destruct2,4: #hd1 #tl1] * 627 [1,2: #lab1 * #rest1 ** #EQ destruct(EQ) * #nxt1 * #EQpc 628 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest1 #Hregs 629 whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) 630 *: #EQ1 #EQ2 destruct(EQ1 EQ2) #Hregs #_ 631 ] 632 whd in EQmid : (??%%); destruct(EQmid) >e0 normalize nodelta 633 [3,4: @eq_identifier_elim [1,3: #_ *] * #H #_ @H %] 634 lapply(seq_list_in_code_length … EQrest1) >length_map #EQ >EQ 635 >nth_opt_append_l [2,4: >length_append whd in match (length ? (mid1::?)); 636 whd in match (length ? (mid2::rest)); cases(rest1) //] >append_cons 637 >append_cons >nth_opt_append_l 638 [2,4: >length_append >length_append whd in match (length ? [ ? ]); 639 whd in match (length ? [ ]); cases(rest1) // ] 640 >nth_opt_append_r 641 [2,4: >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]); 642 cases(rest1) // ] 643 >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]); 644 cut(S(rest1)  (rest1+1) = 0) 645 [1,3: cases(rest1) // #m normalize cases m // #m1 normalize nodelta 646 cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ] #EQ1 >EQ1 647 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % 648 ] 649 *: * #lab2 * [1,4,7,10: #j_step #nxt1 2,5,8,11: #fin1 *: *] #EQfind 650 lapply(find_predicate ?????? EQfind) normalize nodelta [5,6,7,8: *] 651 cases(preamble_length ?????????) normalize nodelta [1,3,5,7: *] #n 652 inversion(nth_opt ???) normalize nodelta [1,3,5,7: #_ *] #lab1 #EQlab1 653 @eq_identifier_elim [2,4,6,8: #_ *] #EQ destruct(EQ) 654 cases(Exists_append … (nth_opt_Exists ???? EQlab1)) 655 [2,4,6,8: * [2,4,6,8: *] #EQ destruct(EQ) cases post in Hregs EQpost; 656 [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) #_ %] #hd1 #tl1 #Hregs * 657 #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * #EQt_lab1 658 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3 659 @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq 660 whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt 661 >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs 662 >m_return_bind cases pre in Hregs EQpre; 663 [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); 664 #EQ destruct(EQ) 2,4: #hd1 #tl1] #Hregs * 665 [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc 666 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4 667 whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ 668 *: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_ 669 ] 670 whd in EQmid : (??%%); destruct(EQmid) @⊥ lapply(fresh_labs (point_of_pc p_in pc)) 671 >e0 672 [1,2: #H cases(append_All … H) #_ * #_ *** H #H #_ #_ @H 673 *: *** #H #_ #_ @H 674 ] 675 @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 676 whd in match code_has_point; normalize nodelta 677 cases(fetch_stmt_ok_nxt_ok … EQfn (find_lookup ?????? EQfind)) 678 #stmt' #EQstmt' >EQstmt' @I 679 *: #Hlab2 cases post in Hregs EQpost; 680 [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) 681 cases(Exists_All … Hlab2 (fresh_labs lab2)) #x * #EQ destruct(EQ) ** #H 682 @⊥ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 683 whd in match code_has_point; normalize nodelta 684 cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt' #EQstmt' >EQstmt' @I 685 *: #hd1 #tl1 #Hregs * #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * 686 #EQt_lab1 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3 687 @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq 688 whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt 689 >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs 690 >m_return_bind cases pre in Hregs EQpre; 691 [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); 692 #EQ destruct(EQ) 693 2,4: #hd1 #tl1] 694 #Hregs * 695 [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc 696 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4 697 whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ 698 *: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_ 699 ] 700 whd in EQmid : (??%%); destruct(EQmid) cases(pp_labs) #_ #H 701 lapply(H lab2 (point_of_pc p_in pc) lab1 ? ?) 702 [3,6,9,12: #EQ destruct(EQ) whd in match (stmt_at ????) in EQstmt; 703 >(find_lookup ?????? EQfind) in EQstmt; #EQ destruct(EQ) % 704 1,4,7,10: >e0 [3,4: whd in match (memb ???); @eqb_elim 705 [2,4: * #H @⊥ @H %] #_ @I] >memb_append_l2 [1,3: @I] 706 whd in match (memb ???); @if_elim [1,3: #_ %] #_ 707 whd in match (memb ???); @eqb_elim [1,3: #_ %] * #H1 @⊥ @H1 % 708 *: @Exists_memb assumption 709 ] 710 ] 711 ] 712 ] 713 qed. 714 477 715 478 716 definition make_is_relation_from_beval : (beval → beval → Prop) → … … 595 833 qed. 596 834 835 lemma fetch_internal_function_no_zero : 836 ∀p,prog,stack_size,bl. 837 block_id (pi1 … bl) = 0 → 838 fetch_internal_function … (joint_globalenv p prog stack_size) bl = 839 Error ? [MSG BadFunction]. 840 #p #prg #stack_size #bl #Hbl whd in match fetch_internal_function; 841 whd in match fetch_function; normalize nodelta @eqZb_elim 842 [ >Hbl #EQ @⊥ cases(not_eq_OZ_neg one) #H @H assumption ] 843 #_ normalize nodelta cases(symbol_for_block ???) [%] #id >m_return_bind 844 cases bl in Hbl; * #id #prf #EQ destruct(EQ) 845 change with (mk_block OZ) in match (mk_block ?); 846 cut(find_funct_ptr 847 (fundef (joint_closed_internal_function p (prog_names p prg))) 848 (joint_globalenv p prg stack_size) (mk_block OZ) = None ?) [%] 849 #EQ >EQ % 850 qed. 851 852 lemma next_of_call_pc_ok : ∀P_in,P_out : sem_graph_params. 853 ∀init,prog,stack_sizes,init_regs,f_lbls,f_regs. 854 b_graph_transform_program_props P_in P_out stack_sizes 855 init prog init_regs f_lbls f_regs → 856 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 857 ∀bl :Σb.block_region b =Code.block_id bl ≠ 1 → 858 ∀f,fn. 859 fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl = 860 return 〈f,fn〉 → 861 (∀id,args,dest,lbl. 862 bind_new_P' ?? 863 (λregs1.λdata.bind_new_P' ?? 864 (λregs2.λblp. 865 ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') 866 (f_step … data lbl (CALL P_in ? id args dest))) 867 (init ? fn)) → 868 gen_preserving ?? gen_res_preserve ???? 869 (λpc1,pc2 : Σpc.pc_block pc = bl. 870 sigma_stored_pc P_in P_out prog stack_sizes init 871 init_regs f_lbls f_regs pc2 = pc1) 872 (λn1,n2.sigma_next P_in P_out prog stack_sizes init init_regs f_lbls f_regs bl n2 = return n1) 873 (next_of_call_pc P_in … (joint_globalenv P_in prog stack_sizes)) 874 (next_of_call_pc P_out … (joint_globalenv P_out trans_prog stack_sizes)). 875 #p_in #p_out #init #prog #stack_sizes #init_regs #f_lbls #f_regs #good #bl #Hbl 876 #f #fn #EQfn #Hcall #pc1 #pc2 #Hpc1pc2 #lbl1 #H @('bind_inversion H) H ** #f1 #fn1 * 877 [ * [#c #id #args #dest  #r #lb  #seq ] #nxt  #fin  *] 878 whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) >EQfn >m_return_bind 879 #H @('bind_inversion H) H #stmt #H lapply(opt_eq_from_res ???? H) H 880 #EQstmt whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) 881 cases(fetch_statement_sigma_stored_pc … pc1 f1 fn1 … good …) 882 [3: >(pi2 ?? pc1) assumption 883 4: whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) in ⊢ (??%?); 884 >EQfn in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >EQstmt in ⊢ (??%?); % 2:] 885 #data * #Hdata normalize nodelta * #st_bl * #Hst_bl * #pc' * #EQpc' * #t_fn 886 * #nxt1 * #l1 * #l2 *** #EQt_fetch #_ #_ #nxt1rel %{nxt1} % [2: <(pi2 ?? pc1) assumption] 887 whd in match next_of_call_pc; normalize nodelta <EQpc' in Hpc1pc2; 888 #H lapply(sym_eq ??? H) H whd in match sigma_stored_pc; normalize nodelta 889 inversion(sigma_pc_opt ?????????) 890 [ #ABS @⊥ whd in match sigma_stored_pc in EQpc'; normalize nodelta in EQpc'; 891 >ABS in EQpc'; normalize nodelta #EQ <(pi2 ?? pc1) in EQfn; 892 >fetch_internal_function_no_zero [2: <EQ %] whd in ⊢ (???% → ?); #EQ1 destruct(EQ1) ] 893 #sigma_pc' #EQsigma_pc' normalize nodelta inversion(sigma_pc_opt ?????????) 894 [ #_ normalize nodelta #EQ destruct(EQ) @⊥ lapply EQt_fetch @if_elim #_ #EQf 895 cases(fetch_statement_inv … EQf) >fetch_internal_function_no_zero [1,3: #EQ destruct] 896 >(pc_block_eq p_in p_out prog stack_sizes init init_regs f_lbls f_regs) 897 [1,3: whd in match sigma_stored_pc; normalize nodelta >EQsigma_pc' % 898 *: >EQsigma_pc' % #EQ destruct 899 ] 900 ] 901 #pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQsigma_pc' in EQpc3; #H 902 lapply(sym_eq ??? H) H #EQp lapply(sigma_stored_pc_inj … EQp) [>EQsigma_pc' % #EQ destruct] 903 #EQ destruct(EQ) >EQt_fetch @eq_identifier_elim 904 [ #EQ1 >EQ1 in EQstmt; cases(entry_is_cost … (pi2 ?? fn1)) #nxt2 * #c #ABS >ABS #EQ1 destruct(EQ1) ] 905 #_ cases(not_emptyb ??) normalize nodelta >m_return_bind normalize nodelta 906 lapply(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hst_bl) 907 (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hdata) 908 (Hcall id args dest (point_of_pc p_in pc1)))) 909 #H cases(H (point_of_pc p_in pc2)) #id' * #args' * #dest' #EQ >EQ % 910 qed. 597 911 598 912 definition joint_state_relation ≝ … … 600 914 601 915 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop. 602 603 916 604 917 record good_state_relation (P_in : sem_graph_params) … … 697 1010 ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧ 698 1011 bool_of_beval … bv' = return b 699 (*let st2_pre_mid ≝ mk_state_pc P_out st2_pre_mid_no_pc700 (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in701 let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in702 eval_statement_advance P_out (prog_var_names … trans_prog)703 (joint_globalenv P_out trans_prog stack_sizes) f t_fn704 (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'*)705 1012 ) (f_step … data (point_of_pc P_in (pc … st1)) cond) 706 1013 ) (init ? fn) … … 732 1039 ) (f_step … data (point_of_pc P_in (pc … st1)) seq) 733 1040 ) (init ? fn) 1041 ; call_is_call :∀f,fn,bl. 1042 fetch_internal_function … 1043 (joint_globalenv P_in prog stack_sizes) bl = return 〈f,fn〉 → 1044 ∀id,args,dest,lbl. 1045 bind_new_P' ?? 1046 (λregs1.λdata.bind_new_P' ?? 1047 (λregs2.λblp. 1048 ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') 1049 (f_step … data lbl (CALL P_in ? id args dest))) 1050 (init ? fn) 734 1051 ; cost_commutation : 735 1052 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in … … 740 1057 return 〈f, fn, sequential ?? (COST_LABEL ?? c) nxt〉 → 741 1058 st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2 1059 ; return_commutation : 1060 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1061 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 1062 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 1063 ∀f,fn. 1064 block_id … (pc_block (pc … st1)) ≠ 1 → 1065 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 1066 return 〈f, fn, final P_in ? (RETURN …)〉 → 1067 ∀n. stack_sizes f = return n → 1068 let curr_ret ≝ joint_if_result … fn in 1069 ∀st_pop,pc_pop. 1070 pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret 1071 (st_no_pc … st1) = return 〈st_pop,pc_pop〉 → 1072 ∀nxt.∀f1,fn1,id,args,dest. 1073 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop = 1074 return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 → 1075 st_rel st1 st2 → 1076 ∀t_fn. 1077 fetch_internal_function … 1078 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 1079 return 〈f,t_fn〉 → 1080 bind_new_P' ?? 1081 (λregs1.λdata. 1082 bind_new_P' ?? 1083 (λregs2.λblp. 1084 \snd blp = (RETURN …) ∧ 1085 ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 1086 (\fst blp) (st_no_pc … st2)= return st_fin ∧ 1087 ∃t_st_pop,t_pc_pop. 1088 pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f 1089 (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧ 1090 sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs 1091 t_pc_pop = pc_pop ∧ 1092 if eqZb (block_id (pc_block pc_pop)) (1) then 1093 st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) 1094 (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*) 1095 else 1096 bind_new_P' ?? 1097 (λregs4.λdata1. 1098 bind_new_P' ?? 1099 (λregs3.λblp1. 1100 ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 1101 (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧ 1102 st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) 1103 (decrement_stack_usage ? n st_pop) st2' 1104 ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest)) 1105 ) (init ? fn1) 1106 ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …)) 1107 ) (init ? fn) 1108 ; call_commutation : 1109 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1110 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 1111 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 1112 ∀f,fn,id,arg,dest,nxt. 1113 block_id … (pc_block (pc … st1)) ≠ 1 → 1114 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 1115 return 〈f, fn, sequential P_in ? (CALL P_in ? id arg dest) nxt〉 → 1116 ∀bl. 1117 block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1) 1118 = return bl → 1119 ∀f1,fn1. 1120 fetch_internal_function … 1121 (joint_globalenv P_in prog stack_sizes) bl = return 〈f1,fn1〉 → 1122 ∀st1_pre. 1123 save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre → 1124 ∀n.stack_sizes f1 = return n → 1125 ∀st1'. 1126 setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' → 1127 st_rel st1 st2 → 1128 ∀t_fn. 1129 fetch_internal_function … 1130 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 1131 return 〈f,t_fn〉 → 1132 ∀t_fn1. 1133 fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl = 1134 return 〈f1,t_fn1〉 → 1135 bind_new_P' ?? 1136 (λregs1.λdata. 1137 bind_new_P' ?? 1138 (λregs2.λblp. 1139 ∀mid,id',arg',dest',nxt1. 1140 stmt_at P_out … (joint_if_code ?? t_fn) mid 1141 = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→ 1142 ((\snd (\fst blp)) mid) = (CALL P_out ? id' arg' dest') → 1143 ∃st2_pre_call. 1144 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 1145 (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) = return st2_pre_call ∧ 1146 block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id' 1147 st2_pre_call = return bl ∧ 1148 ∃st2_pre. 1149 save_frame … P_out (kind_of_call P_out id') dest' 1150 (mk_state_pc ? st2_pre_call (pc_of_point P_out (pc_block(pc … st2)) mid) 1151 (last_pop … st2)) = return st2_pre ∧ 1152 ∃st2_after_call. 1153 setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre 1154 = return st2_after_call ∧ 1155 bind_new_P' ?? 1156 (λregs11.λdata1. 1157 ∃st2'. 1158 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 1159 (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) = 1160 return st2' ∧ 1161 st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1)) 1162 (increment_stack_usage P_in n st1') st2' 1163 1164 ) (init ? fn1) 1165 ) 1166 (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest)) 1167 ) (init ? fn) 742 1168 }. 743 1169 744 lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params. 1170 definition JointStatusSimulation : 1171 ∀p_in,p_out : sem_graph_params. 1172 ∀ prog.∀stack_sizes. 1173 ∀ f_lbls, f_regs. ∀init_regs.∀init.∀st_no_pc_rel,st_rel. 1174 good_state_relation p_in p_out prog stack_sizes init init_regs f_lbls f_regs 1175 st_no_pc_rel st_rel → 1176 let trans_prog ≝ b_graph_transform_program p_in p_out init prog in 1177 status_rel (joint_abstract_status (mk_prog_params p_in prog stack_sizes)) 1178 (joint_abstract_status (mk_prog_params p_out trans_prog stack_sizes)) ≝ 1179 λp_in,p_out,prog,stack_sizes,f_lbls,f_regs,init_regs,init,st_no_pc_rel,st_rel,good. 1180 mk_status_rel ?? 1181 (* sem_rel ≝ *) (λs1 : (joint_abstract_status (mk_prog_params p_in ??)). 1182 λs2 : (joint_abstract_status (mk_prog_params p_out ??)).st_rel s1 s2) 1183 (* call_rel ≝ *) 1184 (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call 1185 .λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call 1186 .pc ? s1 = 1187 sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)). 1188 1189 (* 1190 lemma fetch_stmt_ok_succs_ok : ∀p : sem_graph_params. 745 1191 ∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl. 746 1192 In ? (stmt_labels p ? stmt) lbl→ … … 770 1216 ] 771 1217 qed. 772 1218 *) 773 1219 774 1220 … … 1125 1571 qed. 1126 1572 1127 (* 1573 lemma next_of_call_pc_error : ∀pars.∀prog. ∀stack_size,pc. 1574 block_id (pi1 … (pc_block pc)) = 0→ 1575 next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size)) 1576 pc = Error ? [MSG BadFunction]. 1577 #pars #prg #init #pc #EQ whd in match next_of_call_pc; normalize nodelta 1578 whd in match fetch_statement; normalize nodelta 1579 >fetch_internal_function_no_zero // 1580 qed. 1581 1582 lemma next_of_call_pc_inv : ∀pars.∀prog. ∀stack_size. 1583 ∀pc,nxt. 1584 next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size)) pc 1585 = return nxt → 1586 ∃id,fn,c_id,c_args,c_dest. 1587 fetch_statement pars 1588 … (ev_genv … (mk_prog_params pars prog stack_size)) pc = 1589 return 〈id,fn, sequential ? ?(CALL pars ? c_id c_args c_dest) nxt〉. 1590 #pars #prog #init #pc #nxt whd in match next_of_call_pc; normalize nodelta 1591 #H @('bind_inversion H) H ** #id #fn * 1592 [ *[ #c  #c_id #c_arg #c_dest  #reg #lbl  #seq ] #prox  #fin  #H #r #l #l ] 1593 #EQfetch normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1594 %{id} %{fn} %{c_id} %{c_arg} %{c_dest} assumption 1595 qed. 1596 1597 lemma stored_pc_inj : 1598 ∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'. 1599 sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? → 1600 sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc = 1601 sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc' → 1602 pc = pc'. 1603 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H 1604 whd in match sigma_stored_pc; normalize nodelta 1605 inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1 1606 normalize nodelta inversion(sigma_pc_opt ?????????) 1607 [ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1; whd in match sigma_pc_opt; 1608 normalize nodelta @eqZb_elim 1609 [ #ABS1 whd in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ABS1 : (??%%); destruct] 1610 #Hbl normalize nodelta #H @('bind_inversion H) H #lbl whd in match sigma_label; 1611 normalize nodelta >code_block_of_block_eq >m_return_bind 1612 >fetch_internal_function_no_zero [ whd in ⊢ (??%% → ?); #EQ destruct(EQ)] 1613 >(pc_block_eq … H) whd in match sigma_stored_pc; normalize nodelta >EQpc1 % 1614 ] 1615 #pc2 #EQpc2 normalize nodelta #EQ destruct(EQ) 1616 @(sigma_stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs …) 1617 [ assumption] >EQpc1 >EQpc2 % 1618 qed. 1619 1620 1621 1622 1623 1128 1624 lemma eval_return_ok : 1129 1625 ∀ P_in , P_out: sem_graph_params. … … 1131 1627 ∀stack_sizes. 1132 1628 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 1133 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.1134 1629 ∀st_no_pc_rel,st_rel. 1135 1630 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 1136 1631 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1137 1632 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 1138 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good1139 st_no_pc_rel st_rel →1140 ∀st1,st1' : 1633 ∀good : good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 1634 st_no_pc_rel st_rel. 1635 ∀st1,st1' : joint_abstract_status prog_pars_in. 1141 1636 ∀st2 : joint_abstract_status prog_pars_out. 1142 1637 ∀f. 1143 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog). 1144 *) 1145 1638 ∀fn : joint_closed_internal_function P_in ?. 1639 block_id … (pc_block (pc … st1)) ≠ 1 → 1640 st_rel st1 st2 → 1641 fetch_statement P_in … 1642 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 1643 return 〈f, fn,final P_in ? (RETURN …)〉 → 1644 eval_state P_in … (ev_genv … prog_pars_in) 1645 st1 = return st1' → 1646 ∃st2_ret,st2_after_ret,st2' : joint_abstract_status prog_pars_out. 1647 ∃taa2 : trace_any_any … st2 st2_ret. 1648 ∃taa2' : trace_any_any_free … st2_after_ret st2'. 1649 (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ 1650 as_classifier … st2_ret cl_return ∧ 1651 as_execute … st2_ret st2_after_ret ∧ st_rel st1' st2' ∧ 1652 ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret. 1653 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel 1654 #st_rel #good #st1 #st1' #st2 #f #fn #Hbl #Rst1st2 #EQfetch 1655 whd in match eval_state; normalize nodelta >EQfetch >m_return_bind 1656 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 1657 whd in match eval_statement_advance; whd in match eval_return; normalize nodelta 1658 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H #ssize 1659 #H lapply(opt_eq_from_res ???? H) H change with (stack_size f) in ⊢ (??%? → ?); 1660 #EQssize #H @('bind_inversion H) H * #st_pop #pc_pop #EQpop #H @('bind_inversion H) 1661 H #next_of_call #EQnext_of_call whd in ⊢ (??%% → ?); whd in match next; 1662 whd in match set_last_pop; whd in match set_pc; normalize nodelta #EQ destruct(EQ) 1663 lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?) 1664 [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta 1665 #H cases(H EQfetch) H *:] 1666 #data * #t_fn ** #EQt_fn >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; 1667 #EQt_fn #Hinit normalize nodelta ** #pre #fin_s * #Hregs * #pre * #mid 1668 ** #EQmid #EQpre whd in ⊢ (% → ?); #EQt_stmt 1669 cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall 1670 <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs 1671 cases(bind_new_bind_new_instantiates … Hregs (bind_new_bind_new_instantiates … Hinit 1672 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall … 1673 Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop 1674 ** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta 1675 [ #sem_rel (*premain case TODO *) cases daemon ] 1676 cases(fetch_statement_sigma_stored_pc … good … Hbl_pcpop … EQcall) #data1 * #Hinit1 1677 normalize nodelta *** #pre_c #instr_c #post_c * #Hregs1 * #pc1 * destruct(EQt_pc_pop) 1678 whd in match sigma_stored_pc in ⊢ (% → ?); normalize nodelta 1679 inversion(sigma_pc_opt ???????? t_pc_pop) 1680 [ #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero [#EQ destruct(EQ)] 1681 whd in match sigma_stored_pc; normalize nodelta >ABS %] 1682 #pc2 #EQpc2 normalize nodelta inversion(sigma_pc_opt ?????????) 1683 [ #_ normalize nodelta #EQ destruct(EQ) cases(fetch_statement_inv … EQcall) 1684 >fetch_internal_function_no_zero [2: whd in match sigma_stored_pc; normalize nodelta >EQpc2 %] 1685 #EQ destruct(EQ) ] 1686 #pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQpc2 in EQpc3; #H lapply(sym_eq ??? H) H #H 1687 lapply(sigma_stored_pc_inj … H) [ >EQpc2 % #EQ destruct] #EQ destruct(EQ) * #t_fn1 * #nxt1 1688 * #pre * #post @eq_identifier_elim 1689 [ #EQentry cases(entry_is_cost … (pi2 ?? fn1)) #nxt1 * #c <EQentry #ABS 1690 cases(fetch_statement_inv … EQcall) #_ normalize nodelta >ABS #EQ destruct(EQ) ] 1691 #_ cut(∀x : bool.andb x false = false) [* %] #EQ >EQ EQ normalize nodelta *** 1692 cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1) 1693 (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1) 1694 ((call_is_call … good … (proj1 … (fetch_statement_inv … EQcall))) id args dest ?)) (point_of_pc p_in pc1)) 1695 #id' * #args' * #dest' #EQ >EQ EQ #EQt_call #EQpre_c #EQpost_c #EQnxt1 #H 1696 cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1) 1697 (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1) H)) 1698 H #st2' * #EQst2' #fin_sem_rel 1699 %{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))} 1700 %{(next p_out nxt1 1701 (set_last_pop p_out (decrement_stack_usage ? ssize t_st_pop) pc1))} 1702 %{(mk_state_pc ? st2' (pc_of_point p_out (pc_block pc1) next_of_call) pc1)} 1703 %{((taaf_to_taa … 1704 (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))} 1705 [ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); whd in match (as_label ??); 1706 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 1707 >point_of_pc_of_point >EQt_stmt >m_return_bind normalize nodelta * #H @H % ] 1708 letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog) 1709 lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size) ??????????) 1710 [11: * #taaf * #_ #prf %{taaf} 1711 3: change with (pc_block pc1) in match (pc_block ?); 1712 @(proj1 … (fetch_statement_inv … EQt_call)) 1713 2: whd in match next; whd in match succ_pc; whd in match set_pc; 1714 whd in match point_of_pc; normalize nodelta whd in match pc_of_point; 1715 normalize nodelta >point_of_offset_of_point in ⊢ (????%???); 1716 whd in match (point_of_succ ???); @EQpost_c 1717 1: assumption 1718 *: 1719 ] 1720 % 1721 [ % 1722 [ % 1723 [ % 1724 [ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *] 1725 #hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) * 1726 #succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ) 1727 #EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??); 1728 whd in match (as_pc_of ??); whd in match (point_of_succ ???); 1729 change with (pc_block pc1) in match (pc_block ?); 1730 whd in match fetch_statement; normalize nodelta 1731 >(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind 1732 whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1733 >EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt; 1734 normalize nodelta * #H @H % ] 1735 ] 1736 whd [ whd in match (as_classify ??);  whd in match eval_state; normalize nodelta] 1737 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 1738 >point_of_pc_of_point >EQt_stmt [%] >m_return_bind whd in match eval_statement_no_pc; 1739 normalize nodelta >m_return_bind whd in match eval_statement_advance; 1740 whd in match eval_return; normalize nodelta whd in match (stack_sizes ????); 1741 >EQssize >m_return_bind >EQt_pop >m_return_bind whd in match next_of_call_pc; 1742 normalize nodelta >EQt_call >m_return_bind % 1743  whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct] 1744 whd in match (point_of_succ ???); @(st_rel_def … good) 1745 [3: change with (pc_block pc1) in match (pc_block ?); 1746 lapply(proj1 ?? (fetch_statement_inv … EQcall)) <pc_block_eq in ⊢ (% → ?); 1747 [2: >EQpc2 % #EQ destruct] #H @H 1748 1,2: 1749  <pc_block_eq in fin_sem_rel; [2: >EQpc2 % #EQ destruct] #H @H 1750  % 1751 ] 1752 ] 1753 ] 1754 whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i 1755 #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call 1756 whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQpc1_pc_s1_pre #EQsucc_pc 1757 whd in ⊢ (% → ?); #EQpc_s1_pre >EQpc_s1_pre in EQfetch_call; #EQfetch_call 1758 cases(fetch_statement_sigma_stored_pc … good … EQfetch_call) 1759 [2: <EQpc_s1_pre % #ABS elim Hbl_pcpop #H @H H >EQpc1_pc_s1_pre assumption ] 1760 #data2 * #EQdata2 normalize nodelta * #bl2 * #EQbl2 * #pc3 * #EQstored 1761 lapply(stored_pc_inj … (sym_eq ??? EQstored)) 1762 [ % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero 1763 [ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS % ] 1764 #EQ destruct(EQ) * #fn' * #nxt'' * #l1 * #l2 @eq_identifier_elim 1765 [ #EQentry cases(fetch_statement_inv … EQfetch_call) #_ >EQentry normalize nodelta 1766 cases(entry_is_cost … (pi2 ?? calling)) #nxt1 * #c #EQ >EQ #EQ1 destruct] 1767 #_ cut(∀b : bool.andb b false = false) [ * //] #EQ >EQ EQ normalize nodelta 1768 *** #EQt_fetch_call #_ #_ #EQnxt' whd >EQt_fetch_call normalize nodelta 1769 cut(? : Prop) 1770 [3: whd in match (last_pop ??); #H %{H} 1771 2: @(stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs … ) 1772 [ % #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero 1773 [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS % ] 1774 >EQpc1_pc_s1_pre assumption 1775 ] 1776 destruct(H) 1777 cut(nxt'' = nxt1) [2: #EQ destruct whd in ⊢ (??%%); % ] 1778 cut(nxt' = next_of_call) 1779 [ lapply EQsucc_pc whd in match (succ_pc); normalize nodelta 1780 whd in match (point_of_succ ???); whd in match (point_of_succ ???); 1781 whd in ⊢ (??%% → ?); cases next_of_call #x cases nxt' #y 1782 whd in match (offset_of_point ??); whd in match (offset_of_point ??); 1783 #EQ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct(EQ) % ] 1784 #EQ destruct(EQ) >EQcall in EQfetch_call; >EQt_call in EQt_fetch_call; 1785 whd in ⊢ (? → ??%? → ?); #EQ1 #EQ2 lapply(eq_to_jmeq ??? EQ1) EQ1 #EQ1 destruct(EQ1) % 1786 qed. 1787 1788 1789 theorem joint_correctness : ∀p_in,p_out : sem_graph_params. 1790 ∀prog : joint_program p_in.∀stack_size : ident → option ℕ. 1791 ∀init : (∀globals.joint_closed_internal_function p_in globals → 1792 bound_b_graph_translate_data p_in p_out globals). 1793 ∀init_regs : block → list register.∀f_lbls : lbl_funct_type. 1794 ∀f_regs : regs_funct_type.∀st_no_pc_rel : joint_state_relation p_in p_out. 1795 ∀st_rel : joint_state_pc_relation p_in p_out. 1796 good_state_relation p_in p_out prog stack_size init init_regs 1797 f_lbls f_regs st_no_pc_rel st_rel → 1798 let trans_prog ≝ b_graph_transform_program … init prog in 1799 ∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in → 1800 ∃init_out.make_initial_state (mk_prog_params p_out trans_prog stack_size) = OK ? init_out ∧ 1801 ∃[1] R. 1802 status_simulation_with_init 1803 (joint_abstract_status (mk_prog_params p_in prog stack_size)) 1804 (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)) 1805 R init_in init_out. 1806 cases daemon 1807 qed. 1808 1809
Note: See TracChangeset
for help on using the changeset viewer.