Changeset 2105 for src/common/Globalenvs.ma
 Timestamp:
 Jun 21, 2012, 5:21:04 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/Globalenvs.ma
r2010 r2105 202 202 definition globalenv_noinit: ∀F. ∀p:program F nat. genv_t (F (prog_var_names … p)) ≝ 203 203 λF,p. 204 \fst (globalenv_allocmem F nat (λn.[Init_space n]) p).204 globalenv F nat (λn.[Init_space n]) p. 205 205 206 206 (* Return the initial memory state for the given program. *) … … 242 242 ] qed. 243 243 244 245 lemma vars_irrelevant_to_find_funct_ptr : ∀F,V,init,b,vars,ge,m. 246 find_funct_ptr F (\fst (add_globals F V init 〈ge,m〉 vars)) b = find_funct_ptr F ge b. 247 #F #V #init * * // * // #blk 248 whd in ⊢ (? → ? → ? → ??%%); 249 #vars elim vars 250 [ #ge #m % 251  * * #id #r #v #tl #IH #ge #m 252 whd in match (add_globals ?????); 253 whd in ⊢ (??(???(??(???(????%?))))?); 254 cases (alloc ????) #m' #b 255 whd in ⊢ (??(???(??(???(????%?))))?); 256 >IH cases ge #fnmap #nextblock #symmap 257 whd in ⊢ (??(???%)?); 258 % 259 ] qed. 260 261 lemma matching_globals_get_same_blocks : ∀A,B,V,W,initV,initW. 262 ∀P:(ident × region × V) → (ident × region × W) → Prop. 263 (∀v,w. P v w → \fst v = \fst w ∧ size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → 264 ∀vars,ge,ge',m,vars'. 265 symbols ? ge = symbols … ge' → 266 All2 … P vars vars' → 267 symbols … (\fst (add_globals A V initV 〈ge,m〉 vars)) = symbols … (\fst (add_globals B W initW 〈ge',m〉 vars')). 268 #A #B #V #W #initV #initW #P #varsOK 269 #vars elim vars 270 [ #ge #ge' #m * [ #E #_ @E  #h #t #_ * ] 271  * * #id #r #v #tl #IH #ge #ge' #m * [ #_ * ] 272 * * #id' #r' #w #tl' #E * #p #TL 273 whd in match (add_globals A ????); 274 change with (add_globals A ????) in match (foldl ?????); 275 whd in match (add_globals B ????); 276 change with (add_globals B ????) in match (foldl (genv_t B × mem) ????); 277 cases (varsOK … p) #E1 #E2 278 destruct >E2 cases (alloc ????) #m' #b 279 @IH // 280 whd in match (add_symbol ????); 281 whd in match (add_symbol ????); 282 >E % 283 ] qed. 284 285 lemma pre_matching_fns_get_same_blocks : ∀A,B,P. 286 (∀f,g. P f g → \fst f = \fst g) → 287 ∀fns,fns'. 288 All2 … P fns fns' → 289 let ge ≝ add_functs A (empty ?) fns in 290 let ge' ≝ add_functs B (empty ?) fns' in 291 nextfunction … ge = nextfunction … ge' ∧ symbols … ge = symbols … ge'. 292 #A #B #P #fnOK #fns elim fns 293 [ * [ #_ % %  #h #t * ] 294  * #id #f #tl #IH * [ * ] 295 * #id' #g #tl' * #p lapply (fnOK … p) #E destruct #H 296 whd in match (add_functs ???); 297 change with (add_functs ???) in match (foldr ?????); 298 whd in match (add_functs B ??); 299 change with (add_functs ???) in match (foldr (ident × B) ????); 300 cases (IH tl' H) #E1 #E2 301 % [ >E1 %  >E1 >E2 % ] 302 ] qed. 303 304 lemma matching_fns_get_same_blocks : ∀A,B,P. 305 (∀f,g. P f g → \fst f = \fst g) → 306 ∀fns,fns'. 307 All2 … P fns fns' → 308 let ge ≝ add_functs A (empty ?) fns in 309 let ge' ≝ add_functs B (empty ?) fns' in 310 symbols … ge = symbols … ge'. 311 #A #B #P #fnOK #fns #fns' #p @(proj2 … (pre_matching_fns_get_same_blocks … p)) @fnOK 312 qed. 244 313 245 314 (* … … 318 387 and operations over global environments. *) 319 388 320 find_funct_ptr_transf:321 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.322 ∀b: block. ∀f: A.323 find_funct_ptr ? (globalenv ?? p) b = Some ? f →324 find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? (transf f);325 find_funct_transf:326 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.327 ∀v: val. ∀f: A.328 find_funct ? (globalenv ?? p) v = Some ? f →329 find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? (transf f);330 find_symbol_transf:331 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V.332 ∀s: ident.333 find_symbol ? (globalenv ?? (transform_program … transf p)) s =334 find_symbol ? (globalenv ?? p) s;335 389 init_mem_transf: 336 390 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. … … 434 488 (* * Commutation properties between matching between programs 435 489 and operations over global environments. *) 490 *) *) 491 492 (* First, show that nextfunction only depends on the number of functions: *) 493 494 let rec nat_plus_pos (n:nat) (p:Pos) : Pos ≝ 495 match n with 496 [ O ⇒ p 497  S m ⇒ succ (nat_plus_pos m p) 498 ]. 499 500 lemma nextfunction_length : ∀A,l,ge. 501 nextfunction A (add_functs … ge l) = nat_plus_pos (l) (nextfunction A ge). 502 #A #l elim l // #h #t #IH #ge 503 whd in ⊢ (??%%); >IH // 504 qed. 505 506 (* Now link functions in related programs, but without dealing with the type 507 casts yet. *) 508 509 lemma find_funct_ptr_All2 : ∀A,B,V,W,b,p,f,initV,initW,p',P. 510 find_funct_ptr … (globalenv A V initV p) b = Some ? f → 511 All2 ?? (λx,y. P (\snd x) (\snd y)) (prog_funct ?? p) (prog_funct … p') → 512 ∃f'. find_funct_ptr … (globalenv B W initW p') b = Some ? f' ∧ P f f'. 513 #A #B #V #W #b * #vars #fns #main #f #initV #initW * #vars' #fns' #main' #P 514 cases b * * [ 2,3,5,6,8,9,11,12,14,15,17,18: #bp ] 515 [ 12:  *: #F whd in F:(??%?); destruct ] 516 >vars_irrelevant_to_find_funct_ptr 517 >vars_irrelevant_to_find_funct_ptr 518 letin varnames ≝ (map ??? vars) 519 cut (lookup_opt (A varnames) bp (functions ? (add_functs ? (empty ?) [ ])) = None ?) 520 // 521 cut (nextfunction (A varnames) (empty ?) = nextfunction (B (map … (λx.\fst (\fst x)) vars')) (empty ?)) 522 // 523 generalize in match (empty ?); 524 generalize in match (empty ?); 525 generalize in match fns'; 526 elim fns 527 [ #fns' #ge' #ge #_ #F1 #FFP @⊥ normalize in FFP; >F1 in FFP; #E destruct 528  * #id #fn #tl #IH #fns' #ge' #ge #NF #F1 whd in ⊢ (??%? → ?); 529 whd in match (functions ??); 530 change with (add_functs ???) in match (foldr ?????); 531 cases (decidable_eq_pos bp (nextfunction … (add_functs ? ge tl))) 532 [ #E destruct >lookup_opt_insert_hit #E destruct 533 cases fns' [ * ] 534 * #id' #fn' #tl' * #M #Mtl 535 %{fn'} % // whd in ⊢ (??%?); 536 whd in match (functions ??); 537 change with (add_functs ???) in match (foldr ???? tl'); 538 >nextfunction_length >nextfunction_length <NF >(All2_length … Mtl) 539 >lookup_opt_insert_hit @refl 540  #NE >lookup_opt_insert_miss // 541 #FFP cases fns' [ * ] * #id' #fn' #tl' * #M #Mtl 542 cases (IH ?????? Mtl) 543 [ #fn'' * #FFP' #P' %{fn''} % [ whd in ⊢ (??%?); >lookup_opt_insert_miss [2: >nextfunction_length <NF <(All2_length … Mtl) <nextfunction_length @NE ] @FFP'  @P' ] 544  skip 545  4: @NF 546  skip 547  // 548  @FFP 549 ] 550 ] 551 ] qed. 552 553 discriminator Prod. 554 555 (* Now prove the full version. *) 556 557 lemma find_funct_ptr_match: 558 ∀M:matching.∀initV,initW. 559 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 560 ∀MATCH:match_program … M p p'. 561 ∀b: block. ∀f: m_A M (prog_var_names … p). 562 find_funct_ptr … (globalenv … initV p) b = Some ? f → 563 ∃tf : m_B M (prog_var_names … p'). 564 find_funct_ptr … (globalenv … initW p') b = Some ? tf ∧ match_fundef M ? f (tf⌈m_B M ? ↦ m_B M (prog_var_names … p)⌉). 565 [ 2: >(matching_vars … (mp_vars … MATCH)) % ] 566 * #A #B #V #W #match_fn #match_var #initV #initW 567 #p #p' * #Mvars #Mfn #Mmain 568 #b #f #FFP 569 @(find_funct_ptr_All2 A B V W ??????? FFP) 570 lapply (matching_vars … (mk_matching A B V W match_fn match_var) … Mvars) 571 #E 572 @(All2_mp … Mfn) 573 * #id #f * #id' #f' 574 <E in f' ⊢ %; #f' Mmain b Mfn Mvars initV initW E 575 normalize #H @(match_funct_entry_inv … H) // 576 qed. 577 578 lemma 579 find_funct_ptr_transf_partial2: 580 ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W. 581 ∀p: program A V. ∀p': program B W. 582 transform_partial_program2 … p transf_fun transf_var = OK ? p' → 583 ∀b: block. ∀f: A ?. 584 find_funct_ptr ? (globalenv … iV p) b = Some ? f → 585 ∃f'. 586 find_funct_ptr ? (globalenv … iW p') b = Some ? f' ∧ transf_fun ? f ≃ OK ? f'. 587 #A #B #V #W #iV #iW #tf #tv #p #p' #TPP2 #b #f #FFP 588 cases (find_funct_ptr_match … (transform_partial_program2_match … TPP2) … FFP) 589 [2: @iW 590  #f' * #FFP' generalize in ⊢ (???(??(match % with [_⇒?])) → ?); #E 591 #TF %{f'} % // 592 FFP TPP2 FFP' >TF TF >E in f' ⊢ %; #f' % 593 qed. 594 595 lemma match_funct_entry_id : ∀M,vs,vs',f,g. 596 match_funct_entry M vs vs' f g → \fst f = \fst g. 597 #M #vs #vs' #f #g * // 598 qed. 599 600 lemma 601 find_symbol_match: 602 ∀M:matching. 603 ∀initV,initW. (∀v,w. match_var_entry M v w → size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → 604 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 605 match_program … M p p' → 606 ∀s: ident. 607 find_symbol ? (globalenv … initW p') s = find_symbol ? (globalenv … initV p) s. 608 * #A #B #V #W #match_fun #match_var #initV #initW #initsize 609 * #vars #fns #main * #vars' #fns' #main' * #Mvars #Mfns #Mmain #s 610 whd in ⊢ (??%%); 611 @sym_eq 612 @(eq_f ??(λx. lookup SymbolTag block x s)) 613 whd in match (globalenv ????); whd in match (globalenv_allocmem ????); 614 whd in match (globalenv ????); whd in match (globalenv_allocmem ????); 615 change with (add_globals ?????) in match (foldl ?????); 616 change with (add_globals ?????) in match (foldl ? (ident×region×V) ???); 617 @(matching_globals_get_same_blocks … Mvars) 618 [ * #idr #v * #idr' #w #MVE % [ inversion MVE #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct %  @(initsize … MVE) ] 619  @(matching_fns_get_same_blocks … Mfns) 620 #f #g @match_funct_entry_id 621 ] qed. 622 623 lemma 624 find_symbol_transf_partial2: 625 ∀A,B,V,W,iV,iW. ∀transf_fun: (∀vs. A vs → res (B vs)). ∀transf_var: V → res W. 626 (∀v,w. transf_var v = OK ? w → size_init_data_list (iV v) = size_init_data_list (iW w)) → 627 ∀p: program A V. ∀p': program B W. 628 transform_partial_program2 … p transf_fun transf_var = OK ? p' → 629 ∀s: ident. 630 find_symbol ? (globalenv … iW p') s = find_symbol ? (globalenv … iV p) s. 631 #A #B #V #W #iV #iW #tf #tv #sizeOK #p #p' #TPP2 #s 632 @(find_symbol_match … (transform_partial_program2_match … TPP2)) 633 #v0 #w0 * #id #r #v #w @sizeOK 634 qed. 635 636 lemma 637 find_funct_ptr_transf: 638 ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). 639 ∀b: block. ∀f: A ?. 640 find_funct_ptr ? (globalenv … iV p) b = Some ? f → 641 find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = Some ? (transf … f). 642 #A #B #V #iV * #vars #fns #main #tf #b #f #FFP 643 cases (find_funct_ptr_match … (transform_program_match … tf ?) … FFP) 644 [ 2: @iV 645  #f' * #FFP' 646 generalize in match (matching_vars ????); 647 whd in match (prog_var_names ???); whd in match (prog_vars ???); 648 #E >(K ?? E) whd in ⊢ (??%% → ?); #E' >FFP' >E' % 649 ] qed. 650 651 lemma 652 find_funct_transf: 653 ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. 654 ∀v: val. ∀f: A ?. 655 find_funct ? (globalenv … iV p) v = Some ? f → 656 find_funct ? (globalenv … iV (transform_program … p transf)) v = Some ? (transf ? f). 657 #A #B #V #iV #tf #p #v #f #FF 658 cases (find_funct_find_funct_ptr ???? FF) 659 #r * #b * #pc * #E destruct #FFP 660 change with (find_funct_ptr ???) in ⊢ (??%?); 661 @(find_funct_ptr_transf A B V iV p tf b f FFP) (* XXX Matita seems to require too much detail here *) 662 qed. 663 664 lemma 665 find_symbol_transf: 666 ∀A,B,V,iV. ∀transf: (∀vs. A vs → B vs). ∀p: program A V. 667 ∀s: ident. 668 find_symbol ? (globalenv … iV (transform_program … p transf)) s = 669 find_symbol ? (globalenv … iV p) s. 670 #A #B #V #iV #tf #p @(find_symbol_match … (transform_program_match … tf ?)) 671 #v0 #w0 * // 672 qed. 673 674 (* Package up transform_program results nicely. *) 675 676 record related_globals (A,B:Type[0]) (t: A → B) (ge:genv_t A) (ge':genv_t B) : Prop ≝ { 677 rg_find_symbol: ∀s. 678 find_symbol … ge s = find_symbol … ge' s; 679 rg_find_funct: ∀v,f. 680 find_funct … ge v = Some ? f → 681 find_funct … ge' v = Some ? (t f); 682 rg_find_funct_ptr: ∀b,f. 683 find_funct_ptr … ge b = Some ? f → 684 find_funct_ptr … ge' b = Some ? (t f) 685 }. 686 687 theorem transform_program_related : ∀A,B,V,init,p. ∀tf:∀vs. A vs → B vs. 688 related_globals (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (transform_program A B V p tf)). 689 #A #B #V #iV #p #tf % 690 [ #s @sym_eq @(find_symbol_transf A B V iV tf p) 691  @(find_funct_transf A B V iV tf p) 692  @(find_funct_ptr_transf A B V iV p tf) 693 ] qed. 694 695 696 (* 436 697 437 698 find_funct_ptr_match: … … 475 736 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 476 737 match_program … match_fun match_var p p' → 477 init_mem ?? p' = init_mem ?? p*) *)738 init_mem ?? p' = init_mem ?? p*) 478 739 479 740 (*
Note: See TracChangeset
for help on using the changeset viewer.