Changeset 2501
 Timestamp:
 Nov 29, 2012, 10:12:48 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2495 r2501 200 200 qed. 201 201 202 lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false. 203 ** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed. 204 205 axiom mem_ext_eq : 206 ∀m1,m2 : mem. 207 (∀b.let bc1 ≝ blocks m1 b in 208 let bc2 ≝ blocks m2 b in 209 low bc1 = low bc2 ∧ high bc1 = high bc2 ∧ 210 ∀z.contents bc1 z = contents bc2 z) → 211 nextblock m1 = nextblock m2 → m1 = m2. 212 202 213 lemma beloadv_sigma_commute: 203 214 ∀p,p',graph_prog,sigma,m,ptr,bv,prf1. … … 207 218 return sigma_beval p p' graph_prog sigma bv prf2. 208 219 #p #p' #graph_prog #sigma #m #ptr #bv #prf1 209 whd in match beloadv in ⊢ (%→?); normalize nodelta 210 whd in match do_if_in_bounds in ⊢ (%→?); normalize nodelta 211 @Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)] 212 #block_id_ok 213 @Zleb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)] 214 #zh 215 @Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)] 216 #zl #EQ whd in EQ : (???%); destruct(EQ) 217 % [ @(prf1 ?? block_id_ok zh zl) ] 218 whd in match beloadv; normalize nodelta 219 whd in match do_if_in_bounds; normalize nodelta 220 @Zltb_elim_Type0 normalize nodelta [2: * #ABS @⊥ @ABS assumption] 221 #block_id_lin_ok 222 @Zleb_elim_Type0 normalize nodelta 223 [ 224  * #ABS @⊥ @ABS whd in match sigma_mem; normalize nodelta 220 whd in match beloadv; 221 whd in match do_if_in_bounds; 222 whd in match sigma_mem; 223 normalize nodelta 224 @If_elim #block_ok >block_ok normalize nodelta 225 [2: whd in ⊢ (???%→?); #ABS destruct(ABS) ] 226 @If_elim #H 227 [ elim (andb_true … H) 228 #H1 #H2 229 whd in match sigma_beval; normalize nodelta 230 @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta 231 whd in ⊢ (???%→?); #EQ' destruct 232 >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe 233  elim (andb_false … H) H #H >H 234 [2: >commutative_andb ] normalize nodelta 235 whd in ⊢ (???%→?); #ABS destruct(ABS) 236 ] 237 qed. 225 238 226 239 lemma bestorev_sigma_commute : 227 240 ∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2. 228 241 bestorev m ptr bv = return m' → 229 ∃prf3. 242 ∃prf3. 230 243 bestorev (sigma_mem p p' graph_prog sigma m prf1) 231 244 ptr … … 233 246 = 234 247 return (sigma_mem p p' graph_prog sigma m' prf3). 235 cases daemon qed. 248 #p #p' #graph_prog #sigma #m #ptr #bv #m' #prf1 #prf2 249 whd in match bestorev; 250 whd in match do_if_in_bounds; 251 whd in match sigma_mem; 252 whd in match update_block; 253 normalize nodelta 254 @If_elim #block_ok >block_ok normalize nodelta 255 [2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)] 256 @Zleb_elim_Type0 #H1 257 [ @Zltb_elim_Type0 #H2 ] 258 [2,3: #ABS normalize in ABS; destruct(ABS) ] 259 normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ) 260 % 261 [2: whd in ⊢ (???%); 262 cut (∀X,a,b.a = b → Some X a = Some X b) [ // ] 263 #aux @aux 264 @mem_ext_eq [2: % ] 265 #b @if_elim 266 [2: #B 267 @If_elim #prf1 @If_elim #prf2 268 [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ] 269 whd in match low_bound; whd in match high_bound; 270 normalize nodelta 271 cut (Not (bool_to_Prop (eq_block b (pblock ptr)))) 272 [ % #ABS >ABS in B; * ] 273 B #B % [ >B %% ] #z 274 @If_elim #prf3 275 @If_elim #prf4 276 [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ 4: % ] 277 whd in match sigma_beval in ⊢ (??%%); normalize nodelta 278 @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; 279 >EQ2 #EQ destruct(EQ) % 280  #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ] 281 #EQ destruct(EQ) 282 @If_elim whd in match low_bound; whd in match high_bound; 283 normalize nodelta 284 [2: >block_ok * #ABS elim (ABS I) ] 285 #prf3 % [ >B %% ] 286 #z whd in match update; normalize nodelta 287 @eqZb_elim normalize nodelta #prf4 288 [2: @If_elim #prf5 @If_elim #prf6 289 [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ 4: % ] 290 whd in match sigma_beval in ⊢ (??%%); normalize nodelta 291 @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; 292 normalize nodelta >(eqZb_false … prf4) >EQ2 293 #EQ destruct(EQ) % 294  @If_elim #prf5 295 [2: >B in prf5; normalize nodelta 296 >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ] 297 whd in match sigma_beval in ⊢ (??%%); normalize nodelta 298 @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; 299 normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) % 300 ] 301 ] 302  whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta 303 @eq_block_elim #H normalize nodelta destruct 304 #h2 #h3 whd in match update; normalize nodelta 305 [ @eqZb_elim #H destruct normalize nodelta [ assumption ]] 306 @prf1 assumption 307 ] 308 qed. 236 309 237 310 record good_sem_state_sigma … … 330 403 qed. 331 404 *) 332 405 definition sigma_pc : 333 406 ∀p,p',graph_prog. 334 407 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → … … 450 523 451 524 ; acca_store__commute : helper_def_store__commute … gsss acca_store_ 452 453 525 ; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_ 454 526 ; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_ 527 ; accb_store_commute : helper_def_store__commute … gsss accb_store_ 528 ; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_ 529 ; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_ 530 ; dpl_store_commute : helper_def_store__commute … gsss dpl_store_ 531 ; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_ 532 ; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_ 533 ; dph_store_commute : helper_def_store__commute … gsss dph_store_ 534 ; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_ 535 ; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_ 536 ; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_ 537 ; pair_reg_move_commute : ∀mv,r1,r2,prf1. 538 pair_reg_move_ ? ? (p' ?) r1 mv = return r2 → 539 ∃prf2 . 540 pair_reg_move_ ? ? (p' ?) (sigma_regs p p' graph_prog sigma gsss r1 prf1) mv = 541 return sigma_regs p p' graph_prog sigma gsss r2 prf2 542 ; allocate_locals_commute : 543 ∀ loc, r1, prf1. ∃ prf2. 544 allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) = 545 sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2 546 ; save_frame_commute : 547 ∀dest,st1,st2,prf1. 548 save_frame ?? (p' ?) dest st1 = return st2 → 549 let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1)) 550 (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in 551 ∃prf2. 552 save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2 553 ; eval_ext_seq_commute : 554 let lin_prog ≝ linearise p graph_prog in 555 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 556 let stack_sizes' ≝ 557 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 558 ? graph_prog stack_sizes in 559 ∀ext,fn,st1,st2,prf1. 560 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 561 ext fn st1 = return st2 → 562 ∃prf2. 563 eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 564 ext (sigma_function_name … fn) (sigma_state p p' graph_prog sigma gsss st1 prf1) = 565 return sigma_state p p' graph_prog sigma gsss st2 prf2 566 ; setup_call_commute : 567 ∀ n , parsT, call_args , st1 , st2 , prf1. 568 setup_call ?? (p' ?) n parsT call_args st1 = return st2 → 569 ∃prf2. 570 setup_call ?? (p' ?) n parsT call_args (sigma_state p p' graph_prog sigma gsss st1 prf1) = 571 return (sigma_state p p' graph_prog sigma gsss st2 prf2) 572 ; fetch_external_args_commute : (* TO BE CHECKED *) 573 ∀ex_fun,st1,prf1,call_args. 574 fetch_external_args ?? (p' ?) ex_fun st1 call_args = 575 fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args 576 ; set_result_commute : 577 ∀ l , call_dest , st1 , st2 , prf1. 578 set_result ?? (p' ?) l call_dest st1 = return st2 → 579 ∃prf2. 580 set_result ?? (p' ?) l call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = 581 return (sigma_state p p' graph_prog sigma gsss st2 prf2) 582 ; read_result_commute : 583 let lin_prog ≝ linearise p graph_prog in 584 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 585 let stack_sizes' ≝ 586 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 587 ? graph_prog stack_sizes in 588 ∀call_dest , st1 , prf1, l1. 589 read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 590 call_dest st1 = return l1 → 591 ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?. 592 read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 593 call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = return opt_safe … prf 594 ; pop_frame_commute : 595 let lin_prog ≝ linearise p graph_prog in 596 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 597 let stack_sizes' ≝ 598 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 599 ? graph_prog stack_sizes in 600 ∀ st1 , prf1, curr_id ,st2. 601 pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 602 curr_id st1 = return st2 → 603 ∃prf2. 604 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in 605 let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in 606 pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 607 (sigma_function_name p graph_prog curr_id) (sigma_state p p' graph_prog sigma gsss st1 prf1) = 608 return mk_state_pc ? st2' pc' 455 609 }. 456 610 … … 467 621 (sigma_beval p p' graph_prog sigma bv prf1') 468 622 (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2. 469 cases daemon qed. 623 #p #p' #graph_prog #sigma #X #store #gsss #H #a #bv #st #st #prf1 #prf2 624 whd in match helper_def_store; normalize nodelta 625 #H1 elim(bind_inversion ????? H1) H1 #graph_reg * #store_spec 626 #EQ whd in EQ : (??%%); destruct(EQ) 627 elim(H a bv ?? (proj2 … (proj1 … prf1)) prf2 store_spec) 628 #wf_graph_reg #store_spec1 % 629 [ % [ % ] [%] ] 630 [ @(proj1 … (proj1 … (proj1 … prf1))) 631  @(proj2 … (proj1 … (proj1 … prf1))) 632  @wf_graph_reg 633  @(proj2 … prf1) 634 ] >store_spec1 >m_return_bind % 635 qed. 636 637 470 638 471 639 lemma retrieve_commute : … … 480 648 helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a = 481 649 return sigma_beval p p' graph_prog sigma bv prf2. 482 cases daemon qed. 650 #p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #bv #prf1 651 whd in match helper_def_retrieve; normalize nodelta 652 #retrieve_spec elim(H … (proj2 … (proj1 … prf1)) … retrieve_spec) 653 #wf_bv #retrieve_spec1 %{wf_bv} >retrieve_spec1 % 654 qed. 483 655 484 656 (* … … 495 667 λp,p',graph_prog,sigma. 496 668 λgss : good_state_sigma p p' graph_prog sigma. 497 store_commute … gss (acca_store__commute … gss). *)669 store_commute … gss (acca_store__commute … gss). 498 670 499 671 … … 525 697 526 698 #p #p' # 527 (* 528 ; acca_store_wf : ∀a,bv,st,st'. 529 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → 530 acca_store ?? (p' ?) a bv st = return st' → 531 well_formed_state st → well_formed_state st' 532 533 ; acca_retrieve_wf : ∀a,st,bv. 534 acca_retrieve ?? (p' ?) st a = return bv → 535 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 536 537 ; acca_arg_retrieve_ok : 538 ∀a,st,bv,prf1,prf2. 539 acca_arg_retrieve ?? (p' ?) st a = return bv → 540 acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 541 return sigma_beval p p' graph_prog sigma bv prf2 542 ; acca_arg_retrieve_wf : ∀a,st,bv. 543 acca_arg_retrieve ?? (p' ?) st a = return bv → 544 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 545 546 ; accb_store_ok : 547 ∀a,bv,bv',st,st',prf1,prf2. 548 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 549 accb_store ?? (p' ?) a bv st = return st' → 550 accb_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 551 ; accb_store_wf : ∀a,bv,bv',st,st'. 552 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 553 accb_store ?? (p' ?) a bv st = return st' → 554 well_formed_state st → well_formed_state st' 555 556 ; accb_retrieve_ok : 557 ∀a,st,bv,prf1,prf2. 558 accb_retrieve ?? (p' ?) st a = return bv → 559 accb_retrieve ?? (p' ?) (sigma_state st prf1) a = 560 return sigma_beval p p' graph_prog sigma bv prf2 561 ; accb_retrieve_wf : ∀a,st,bv. 562 accb_retrieve ?? (p' ?) st a = return bv → 563 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 564 565 ; accb_arg_retrieve_ok : 566 ∀a,st,bv,prf1,prf2. 567 acca_arg_retrieve ?? (p' ?) st a = return bv → 568 acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 569 return sigma_beval p p' graph_prog sigma bv prf2 570 ; accb_arg_retrieve_wf : ∀a,st,bv. 571 accb_arg_retrieve ?? (p' ?) st a = return bv → 572 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 573 574 575 ; dpl_store_ok : 576 ∀a,bv,bv',st,st',prf1,prf2. 577 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 578 dpl_store ?? (p' ?) a bv st = return st' → 579 dpl_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 580 ; dpl_store_wf : ∀a,bv,bv',st,st'. 581 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 582 dpl_store ?? (p' ?) a bv st = return st' → 583 well_formed_state st → well_formed_state st' 584 585 ; dpl_retrieve_ok : 586 ∀a,st,bv,prf1,prf2. 587 dpl_retrieve ?? (p' ?) st a = return bv → 588 dpl_retrieve ?? (p' ?) (sigma_state st prf1) a = 589 return sigma_beval p p' graph_prog sigma bv prf2 590 ; dpl_retrieve_wf : ∀a,st,bv. 591 dpl_retrieve ?? (p' ?) st a = return bv → 592 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 593 594 ; dpl_arg_retrieve_ok : 595 ∀a,st,bv,prf1,prf2. 596 acca_arg_retrieve ?? (p' ?) st a = return bv → 597 acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 598 return sigma_beval p p' graph_prog sigma bv prf2 599 ; dpl_arg_retrieve_wf : ∀a,st,bv. 600 dpl_arg_retrieve ?? (p' ?) st a = return bv → 601 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 602 603 604 ; dph_store_ok : 605 ∀a,bv,bv',st,st',prf1,prf2. 606 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 607 dph_store ?? (p' ?) a bv st = return st' → 608 dph_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 609 ; dph_store_wf : ∀a,bv,bv',st,st'. 610 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 611 dph_store ?? (p' ?) a bv st = return st' → 612 well_formed_state st → well_formed_state st' 613 614 ; dph_retrieve_ok : 615 ∀a,st,bv,prf1,prf2. 616 dph_retrieve ?? (p' ?) st a = return bv → 617 dph_retrieve ?? (p' ?) (sigma_state st prf1) a = 618 return sigma_beval p p' graph_prog sigma bv prf2 619 ; dph_retrieve_wf : ∀a,st,bv. 620 dph_retrieve ?? (p' ?) st a = return bv → 621 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 622 623 ; dph_arg_retrieve_ok : 624 ∀a,st,bv,prf1,prf2. 625 acca_arg_retrieve ?? (p' ?) st a = return bv → 626 acca_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 627 return sigma_beval p p' graph_prog sigma bv prf2 628 ; dph_arg_retrieve_wf : ∀a,st,bv. 629 dph_arg_retrieve ?? (p' ?) st a = return bv → 630 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 631 632 633 ; snd_arg_retrieve_ok : 634 ∀a,st,bv,prf1,prf2. 635 snd_arg_retrieve ?? (p' ?) st a = return bv → 636 snd_arg_retrieve ?? (p' ?) (sigma_state st prf1) a = 637 return sigma_beval p p' graph_prog sigma bv prf2 638 ; snd_arg_retrieve_wf : ∀a,st,bv. 639 snd_arg_retrieve ?? (p' ?) st a = return bv → 640 well_formed_state st → sigma_beval_opt p p' graph_prog sigma bv ≠ None ? 641 642 ; pair_reg_move_ok : 643 ∀mv,st1,st2,prf1,prf2. 644 pair_reg_move ?? (p' ?) st1 mv = return st2 → 645 pair_reg_move ?? (p' ?) (sigma_state st1 prf1) mv = 646 return sigma_state st2 prf2 647 ; pair_reg_move_wf : 648 ∀mv,st1,st2. 649 pair_reg_move ?? (p' ?) st1 mv = return st2 → 650 well_formed_state st1 → well_formed_state st2 651 652 ; allocate_locals_ok : 653 ∀l,st1,prf1,prf2. 654 allocate_locals ?? (p' ?) l (sigma_state st1 prf1) = 655 sigma_state (allocate_locals ?? (p' ?) l st1) prf2 656 ; allocate_locals_wf : 657 ∀l,st1. 658 well_formed_state st1 → 659 well_formed_state (allocate_locals ?? (p' ?) l st1) 660 661 ; save_frame_ok : 662 ∀dest,st1,st2,prf1,prf2. 663 save_frame ?? (p' ?) dest st1 = return st2 → 664 let st1' ≝ mk_state_pc … (sigma_state st1 (proj2 … prf1)) 665 (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in 666 save_frame ?? (p' ?) dest st1' = return sigma_state st2 prf2 667 ; save_frame_wf : 668 ∀dest,st1,st2. 669 save_frame ?? (p' ?) dest st1 = return st2 → 670 (well_formed_pc p p' graph_prog sigma (pc … st1) ∧ 671 well_formed_state st1) → well_formed_state st2 672 673 ; eval_ext_seq_ok : 674 let lin_prog ≝ linearise p graph_prog in 675 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 676 let stack_sizes' ≝ 677 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 678 ? graph_prog stack_sizes in 679 ∀ext,fn,st1,st2,prf1,prf2. 680 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 681 ext fn st1 = return st2 → 682 eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 683 ext (sigma_function_name … fn) (sigma_state st1 prf1) = return sigma_state st2 prf2 684 ; eval_ext_seq_wf : 685 let lin_prog ≝ linearise p graph_prog in 686 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 687 let stack_sizes' ≝ 688 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 689 ? graph_prog stack_sizes in 690 ∀ext,fn,st1,st2. 691 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 692 ext fn st1 = return st2 → 693 well_formed_state st1 → well_formed_state st2 694 695 ; setup_call_ok : 696 ∀ n , parsT, call_args , st1 , st2 , prf1, prf2. 697 setup_call ?? (p' ?) n parsT call_args st1 = return st2 → 698 setup_call ?? (p' ?) n parsT call_args (sigma_state st1 prf1) = 699 return (sigma_state st2 prf2) 700 ; setup_call_wf : 701 ∀ n , parsT, call_args , st1 , st2. 702 setup_call ?? (p' ?) n parsT call_args st1 = return st2 → 703 well_formed_state st1 → well_formed_state st2 704 705 ; fetch_external_args_ok : (* TO BE CHECKED *) 706 ∀ex_fun,st1,prf1,call_args. 707 fetch_external_args ?? (p' ?) ex_fun st1 call_args = 708 fetch_external_args ?? (p' ?) ex_fun (sigma_state st1 prf1) call_args 709 ; fetch_external_args_wf : 710 ∀ex_fun,st1,call_args. 711 well_formed_state st1 → ∃ l. 712 fetch_external_args ?? (p' ?) ex_fun st1 call_args = OK ? l 713 714 ; set_result_ok : 715 ∀ l , call_dest , st1 , st2 , prf1 , prf2 . 716 set_result ?? (p' ?) l call_dest st1 = return st2 → 717 set_result ?? (p' ?) l call_dest (sigma_state st1 prf1) = 718 return (sigma_state st2 prf2) 719 ; set_result_wf : 720 ∀ l , call_dest , st1 , st2 . 721 set_result ?? (p' ?) l call_dest st1 = return st2 → 722 well_formed_state st1 → well_formed_state st2 723 724 ; read_result_ok : 725 let lin_prog ≝ linearise p graph_prog in 726 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 727 let stack_sizes' ≝ 728 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 729 ? graph_prog stack_sizes in 730 ∀call_dest , st1 , prf1, l1. 731 read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 732 call_dest st1 = return l1 → 733 ∀prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?. 734 read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 735 call_dest (sigma_state st1 prf1) = return opt_safe … prf 736 ; read_result_wf : 737 let lin_prog ≝ linearise p graph_prog in 738 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 739 let stack_sizes' ≝ 740 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 741 ? graph_prog stack_sizes in 742 ∀call_dest , st1 , l1. 743 read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 744 call_dest st1 = return l1 → 745 well_formed_state st1 → 746 m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ? 747 748 ; pop_frame_ok : 749 let lin_prog ≝ linearise p graph_prog in 750 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 751 let stack_sizes' ≝ 752 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 753 ? graph_prog stack_sizes in 754 ∀ st1 , prf1, curr_id ,st2, prf2. 755 pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 756 curr_id st1 = return st2 → 757 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in 758 let st2' ≝ sigma_state (st_no_pc ? st2) (proj2 … prf2) in 759 pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 760 (sigma_function_name p graph_prog curr_id) (sigma_state st1 prf1) = 761 return mk_state_pc ? st2' pc' 762 ; pop_frame_wf : 763 let lin_prog ≝ linearise p graph_prog in 764 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 765 let stack_sizes' ≝ 766 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 767 ? graph_prog stack_sizes in 768 ∀ st1, curr_id ,st2. 769 pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 770 curr_id st1 = return st2 → 771 well_formed_state st1 → well_formed_pc p p' graph_prog sigma (pc ? st2) ∧ 772 well_formed_state (st_no_pc ? st2) 773 }. 699 *) 774 700 775 701 (* restano: … … 785 711 ; pop_frame: ∀globals.∀ge : genv_gen F globals. 786 712 (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars) 787 *)788 713 *) 789 714 … … 1207 1132 ∀sigma.∀gss : good_state_sigma … graph_prog sigma. 1208 1133 ∀fn,st,stmt,st'. 1209 ∀prf : well_formed_state … gss st. ∀prf'.1134 ∀prf : well_formed_state … gss st. 1210 1135 eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes')) 1211 1136 fn st stmt = return st' → 1137 ∃prf'. 1212 1138 eval_seq_no_pc ?? (ev_genv … (lin_prog_params … lin_prog stack_sizes)) 1213 1139 (sigma_function_name … fn) (sigma_state … gss st prf) stmt = … … 1215 1141 #p #p' #graph_prog #stack_sizes #sigma #gss 1216 1142 #fn #st #stmt 1217 #st' #prf #prf'1143 #st' #prf 1218 1144 whd in match eval_seq_no_pc; 1219 1145 cases stmt normalize nodelta 1220 [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) //1146 [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) %{prf} // 1221 1147  (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) H #H 1222 >(pair_reg_move_ok ?????????? H) [%  skip] 1148 change with 1149 (pair_reg_move p (joint_closed_internal_function (make_sem_graph_params p p')) 1150 (make_sem_graph_params p p') ??) in H : (??%?); 1151 lapply H H 1152 whd in match pair_reg_move; normalize nodelta #H 1153 elim(bind_inversion ????? H) H #reg * #reg_spec #EQ whd in EQ : (??%%); destruct(EQ) 1154 elim(pair_reg_move_commute ???????? (proj2 … (proj1 … prf)) reg_spec) 1155 #wf_regs #pm_spec >pm_spec >m_return_bind % [2: %] 1156 % [ 2: @(proj2 … prf) 1157  % [2: assumption] % 1158 [ @(proj1 … (proj1 … (proj1 … prf))) 1159  @(proj2 … (proj1 … (proj1 … prf))) 1160 ] 1161 ] 1223 1162  (* POP *) 1224 1163 #a #H lapply(err_eq_from_io ????? H) H #H elim (bind_inversion ????? H) H 1225 1164 * #val #st1 * #vals_spec #H 1165 change with (acca_store p 1166 (joint_closed_internal_function (make_sem_graph_params p p')) 1167 (make_sem_graph_params p p') a val st1 = ?) in H; 1168 change with (pop (make_sem_graph_params p p') ? = ?) in vals_spec; 1169 lapply vals_spec vals_spec 1170 whd in match pop; normalize nodelta 1171 whd in match is_pop; normalize nodelta 1172 lapply(proj2 … (proj1 … (proj1 … prf))) #wf_is 1173 inversion (istack (make_sem_graph_params p p') st) normalize nodelta 1174 [#_ #ABS normalize in ABS; destruct(ABS)] 1175 [ #Bv  #Bv_not_used #Bv] #is_stack_st_spec >m_return_bind 1176 #EQ whd in EQ : (??%%); destruct(EQ) 1177 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ?????? H) 1178 [ 2,5: @hide_prf >is_stack_st_spec in wf_is; #wf_is 1179 whd in match sigma_is_opt in wf_is; normalize nodelta in wf_is; 1180 inversion(sigma_beval_opt ?????) 1181 [1,3 : #EQ >EQ in wf_is; whd in ⊢ ((?(??%?)) → ?); * #ABS @⊥ @ABS // 1182 inversion(sigma_beval_opt ?????) normalize nodelta 1183 [ #bev % 1184  #bev #bev_s >bev_s in ABS; normalize nodelta 1185 #ABS @⊥ @ABS normalize % 1186 ] 1187 ] 1188 [#H1 #H2 % #ABS destruct(ABS)  #H1 #H2 % #ABS destruct(ABS)] 1189 ] 1190 [ 2,4: @hide_prf % [2,4 : @(proj2 … prf)] % [2,4 : @(proj2 … (proj1 … prf))] 1191 % [1,3 : @(proj1 … (proj1 … (proj1 … prf)))] 1192 whd in match sigma_is_opt; normalize nodelta 1193 [ whd in ⊢ (? (??%?)); % #ABS destruct(ABS)] 1194 >is_stack_st_spec in wf_is; 1195 whd in match sigma_is_opt; normalize nodelta 1196 cases(sigma_beval_opt ?????) 1197 [ normalize * #ABS @⊥ @ABS % 1198  #bev #_ normalize % #ABS destruct(ABS) 1199 ] 1200 ] 1201 #prf' #acca_store_commute %{prf'} 1202 whd in match sigma_state in ⊢ (??(????(?????(?????%?)?))?); 1203 whd in match sigma_is; normalize nodelta 1204 @opt_safe_elim #int_stack #int_stack_sigma_spec 1205 >is_stack_st_spec in int_stack_sigma_spec; 1206 whd in match sigma_is_opt; normalize nodelta 1207 #IS_SPEC elim(bind_opt_inversion ????? IS_SPEC) IS_SPEC 1208 [ #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ) 1209  #sigma_bv_not_used * #sigma_bv_not_used_spec #IS_SPEC 1210 elim(bind_opt_inversion ????? IS_SPEC) IS_SPEC 1211 #sigma_bv * #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)] 1212 normalize nodelta >m_return_bind 1213 1214 1215 1216 #INUTILE #H <H 1217 1218 1219 1220 inversion(istack ??) normalize nodelta [ 1221 whd in match (istack ??); 1222 whd in match sigma_state in ⊢ (??%?); normalize nodelta 1223 acca_store p(joint_closed_internal_function 1224 (make_sem_lin_params p p')) 1225 (make_sem_lin_params p p') a v st1 1226 =return sigma_state p p' graph_prog sigma gss st' prf') 1227 1228 1229 1226 1230 cut(well_formed_state … gss st1) [ cases daemon (* to be added to gss *) ] 1227 1231 #wf_st1 … … 1239 1243 cases (istack ? (sigma_state … st prf)) normalize nodelta 1240 1244 1241 lapply (acca_store_ ok?????????????? H)1245 lapply (acca_store_ ???????????????????????? H) 1242 1246 1243 1247
Note: See TracChangeset
for help on using the changeset viewer.