Changeset 2608 for src/Clight/memoryInjections.ma
 Timestamp:
 Feb 6, 2013, 1:01:34 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/memoryInjections.ma
r2600 r2608 3 3 include "Clight/frontend_misc.ma". 4 4 5 (* This file contains some definitions and lemmas related to memory injections. 6 Could be useful for the Clight → Cminor. Needs revision: the definitions are7 too lax and allow inconsistent embeddings (more precisely, these embeddings do8 not allow to prove that the semantics for pointer lessthan comparisons is9 conserved). *)10 5 (* This file contains some definitions and lemmas related to memory injections. 6 * The whole development is quite similar to the one described in the article by 7 * Leroy & Blazy in J.A.R., except that in Cerco, we describe data down to the byte 8 * level (similar to the memory model of CompCert v2 but not to the aforementioned 9 * paper). 10 * *) 11 11 12 12 (*  *) … … 29 29 30 30 lemma eqZb_reflexive : ∀x:Z. eqZb x x = true. #x /2/. qed. 31 32 lemma eqZb_symmetric : ∀x,y:Z. eqZb x y = eqZb y x. 33 #x #y @(eqZb_elim … x y) 34 [ * >eqZb_z_z @refl 35  #Hneq >(eqZb_false … (sym_neq ??? Hneq)) @refl ] 36 qed. 31 37 32 38 (*  *) … … 60 66 qed. 61 67 68 62 69 lemma block_eq_dec : ∀a,b:block. a = b ∨ a ≠ b. 63 #a #b @(eq_block_elim … a b) /2/ qed. 70 * #a * #b 71 cases (decidable_eq_Z … a b) 72 [ * %1 @refl 73  #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed. 64 74 65 75 lemma block_decidable_eq : ∀a,b:block. (a = b) + (a ≠ b). 66 * #ra #ida * #rb #idb 67 cases ra cases rb 68 [ 2: %2 % #H destruct 69  3: %2 % #H destruct 70  *: cases (decidable_eq_Z_Type ida idb) 71 [ 1,3: * %1 @refl 72  2,4: #Hneq %2 % #H destruct (H) cases Hneq #H @H @refl ] 73 ] qed. 76 * #a * #b 77 cases (decidable_eq_Z_Type … a b) 78 [ * %1 @refl 79  #Hneq %2 % #H destruct @(absurd … (refl ??) Hneq) ] qed. 74 80 75 81 lemma mem_not_mem_neq : ∀l,elt1,elt2. (mem block elt1 l) → ¬ (mem block elt2 l) → elt1 ≠ elt2. … … 82 88 [ 1: #Heq >Heq /2 by not_to_not/ 83 89  2: #x @x ] 84  2: #Hmem1 cases (mem_dec … block_eq_dec elt2tl)90  2: #Hmem1 cases (mem_dec ? block_eq_dec ? tl) 85 91 [ 1: #Hmem2 % #Helt_eq cases Hr #H @H %2 @Hmem2 86 92  2: #Hmem2 @Hind // … … 103 109 pblock ptr ≠ b → 104 110 valid_pointer (free m b) ptr = true. 105 * #br #bid * #contents #next #posnext * * #pbr#pbid #poff111 * (* #br *) #bid * #contents #next #posnext * * (* #pbr *) #pbid #poff 106 112 normalize 107 113 @(eqZb_elim pbid bid) 108 [ 1: #Heqid >Heqid cases pbr cases br normalize 109 [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ] 114 [ 1: #Heqid >Heqid (* cases pbr cases br normalize *) 110 115 cases (Zltb bid next) normalize nodelta 111 [ 2 ,4: #Habsurd destruct (Habsurd) ]112 //113  2: #Hneqid cases pbr cases br normalizetry // ]116 [ 2: #Habsurd destruct (Habsurd) ] 117 #_ #H @False_ind @(absurd … (refl ??) H) 118  2: #Hneqid (* cases pbr cases br normalize *) try // ] 114 119 qed. 115 120 … … 118 123 whd in match (free ??); @refl qed. 119 124 125 (* 120 126 lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr. 121 127 valid_pointer (free m b) ptr = true → … … 148 154 [ 2: % #Heq @Hguard %2 @Heq 149 155  1: @H % #Heq @Hguard %1 @Heq ] 150 ] qed. 156 ] qed. *) 151 157 152 158 (* An alternative version without the gard on the equality of blocks. *) 159 (* 153 160 lemma valid_pointer_free_ok_alt : ∀b : block. ∀m,ptr. 154 161 valid_pointer (free m b) ptr = true → … … 165 172 ] 166 173  *: #_ #H %2 @conj try @H % #Habsurd destruct (Habsurd) ] 167 ] qed. 174 ] qed. *) 168 175 169 176 (* Well in fact a valid pointer can be valid even after a free. Ah. *) … … 207 214 208 215 (* An embedding is a function from block ids to (blocks × offset). *) 209 definition embedding ≝ Z→ option (block × offset).216 definition embedding ≝ block → option (block × offset). 210 217 211 218 definition offset_plus : offset → offset → offset ≝ … … 224 231 match p with 225 232 [ mk_pointer pblock poff ⇒ 226 match E (block_id pblock)with233 match E pblock with 227 234 [ None ⇒ None ? 228 235  Some loc ⇒ … … 236 243 definition embedding_compatible : embedding → embedding → Prop ≝ 237 244 λE,E'. 238 ∀b:block. E (block_id b)= None ? ∨239 E (block_id b) = E' (block_id b).245 ∀b:block. E b = None ? ∨ 246 E b = E' b. 240 247 241 248 (* We parameterise the "equivalence" relation on values with an embedding. *) … … 258 265 ∀b1,off1,b2,off2,ty,v1. 259 266 valid_block m1 b1 → (* We need this because it is not provable from [load_value_of_type ty m1 b1 off1] when loading byref *) 260 E (block_id b1)= Some ? 〈b2,off2〉 →267 E b1 = Some ? 〈b2,off2〉 → 261 268 load_value_of_type ty m1 b1 off1 = Some ? v1 → 262 269 (∃v2. load_value_of_type ty m2 b2 (offset_plus off1 off2) = Some ? v2 ∧ value_eq E v1 v2). … … 299 306 definition block_in_bounds_if_mapped : embedding → block → mem → mem → Prop ≝ 300 307 λE.λb.λm,m'. 301 match E (block_id b)with308 match E b with 302 309 [ None ⇒ True 303 310  Some loc ⇒ … … 313 320 ∀b1,b2,b1',b2',delta1,delta2. 314 321 b1 ≠ b2 → (* note that two blocks can be different only becuase of this region *) 315 E (block_id b1)= Some ? 〈b1',delta1〉 →316 E (block_id b2)= Some ? 〈b2',delta2〉 →317 (if eq Zb (block_id b1') (block_id b2')then322 E b1 = Some ? 〈b1',delta1〉 → 323 E b2 = Some ? 〈b2',delta2〉 → 324 (if eq_block b1' b2' then 318 325 (* block_is_empty m b1' ∨ *) 319 326 high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ … … 332 339 mi_inj : load_sim_ptr E m1 m2; 333 340 (* Invalid blocks are not mapped *) 334 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E (block_id b)= None ?;341 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; 335 342 (* Valid pointers are mapped to valid pointers *) 336 343 mi_valid_pointers : ∀p,p'. … … 340 347 (* Blocks in the codomain are valid *) 341 348 mi_nodangling : ∀b,b',o'. E b = Some ? 〈b',o'〉 → valid_block m2 b'; 342 (* Regions are preserved *)343 mi_region : ∀b,b',o'. E (block_id b)= Some ? 〈b',o'〉 → block_region b = block_region b';349 (* Regions are preserved  this might be superfluous now ?. *) 350 mi_region : ∀b,b',o'. E b = Some ? 〈b',o'〉 → block_region b = block_region b'; 344 351 (* subblocks do not overlap (nonaliasing property) *) 345 352 mi_nonalias : non_aliasing E m1; … … 468 475 (* If we succeed to load something by value from a 〈b,off〉 location, 469 476 [b] is a valid block. *) 477 (* 470 478 lemma load_by_value_success_valid_block_aux : 471 479 ∀ty,m,b,off,v. … … 487 495 try // #Habsurd destruct (Habsurd) 488 496  *: normalize in Hmode; destruct (Hmode) 489 ] qed. 497 ] qed. *) 490 498 491 499 (* If we succeed in loading some data from a location, then this loc is a valid pointer. *) … … 497 505 Zleb (low_bound m b) (Z_of_unsigned_bitvector ? (offv off)) = true ∧ 498 506 Zltb (Z_of_unsigned_bitvector ? (offv off)) (high_bound m b) = true. 499 #ty #m * #brg#bid #off #v507 #ty #m * (* #brg *) #bid #off #v 500 508 cases ty 501 509 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain … … 509 517 whd in match (beloadv ??); 510 518 cases (Zltb bid (nextblock m)) normalize nodelta 511 cases (Zleb (low (blocks m (mk_block brgbid)))519 cases (Zleb (low (blocks m (mk_block (*brg*) bid))) 512 520 (Z_of_unsigned_bitvector offset_size (offv off))) 513 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block brgbid))))521 cases (Zltb (Z_of_unsigned_bitvector offset_size (offv off)) (high (blocks m (mk_block (*brg*) bid)))) 514 522 normalize nodelta 515 523 #Heq destruct (Heq) … … 567 575 (* A valid block stays valid after an alloc. *) 568 576 lemma alloc_valid_block_conservation : 569 ∀m,m',z1,z2, r,new_block.570 alloc m z1 z2 r= 〈m', new_block〉 →577 ∀m,m',z1,z2,(*r,*)new_block. 578 alloc m z1 z2 (*r*) = 〈m', new_block〉 → 571 579 ∀b. valid_block m b → valid_block m' b. 572 #m #m' #z1 #z2 #r * #b' #Hregion_eq573 elim m #contents #nextblock #Hcorrect whd in match (alloc ??? ?);580 #m #m' #z1 #z2 (* #r*) * #b' (* #Hregion_eq *) 581 elim m #contents #nextblock #Hcorrect whd in match (alloc ???(*?*)); 574 582 #Halloc destruct (Halloc) 575 583 #b whd in match (valid_block ??) in ⊢ (% → %); /2/ … … 609 617 610 618 lemma alloc_valid_pointer_conservation : 611 ∀m,m',z1,z2, r,new_block.612 alloc m z1 z2 r=〈m',new_block〉 →613 ∀p. block_id (pblock p) ≠ block_id (pi1 … new_block)→619 ∀m,m',z1,z2,(*r,*)new_block. 620 alloc m z1 z2 (*r*) = 〈m',new_block〉 → 621 ∀p. (pblock p) ≠ new_block → 614 622 valid_pointer m' p = true → 615 623 valid_pointer m p = true. 616 #m #m' #z1 #z2 #r * #new_block #Hregion624 #m #m' #z1 #z2 (*#r*) #new_block 617 625 cases m #cont #next #Hnext 618 626 whd in ⊢ ((??%%) → ?); … … 625 633 whd in match (update_block ?????); 626 634 whd in match (update_block ?????); 627 cut (b ≠ (mk_block rnext))628 [ @(eq_block_elim … b (mk_block rnext)) #H destruct try //635 cut (b ≠ (mk_block (*r*) next)) 636 [ @(eq_block_elim … b (mk_block (*r*) next)) #H destruct try // 629 637 @False_ind 630 638 @(absurd … (refl ??) Hneq) ] #Hneqb 631 639 >(not_eq_block … Hneqb) normalize nodelta 632 640 #HA #HB % [ % ] try assumption 633 cases b in Hneqb Hneq Hblock_id; #r'#id * #Hnext_not_id #Hneq641 cases b in Hneqb Hneq Hblock_id; (* #r'*) #id * #Hnext_not_id #Hneq 634 642 #Hlt cut (id ≤ next) 635 643 [ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ] 636 #Hle @Zle_split try @Hle @Hneq 644 #Hle @Zle_split try @Hle % #Heq destruct 645 @(absurd … (refl ??) Hneq) 637 646 qed. 638 647 639 648 (* Allocating a new zone produces a valid block. *) 640 649 lemma alloc_valid_new_block : 641 ∀m,m',z1,z2 ,r,new_block.642 alloc m z1 z2 r= 〈m', new_block〉 →650 ∀m,m',z1,z2(*,r*),new_block. 651 alloc m z1 z2 (*r*) = 〈m', new_block〉 → 643 652 valid_block m' new_block. 644 * #contents #nextblock #Hcorrect #m' #z1 #z2 #r * #new_block #Hregion_eq645 whd in match (alloc ??? ?); whd in match (valid_block ??);653 * #contents #nextblock #Hcorrect #m' #z1 #z2 (* #r *) * #new_block (* #Hregion_eq *) 654 whd in match (alloc ???(*?*)); whd in match (valid_block ??); 646 655 #Halloc destruct (Halloc) /2/ 647 656 qed. … … 649 658 (* All data in a valid block is unchanged after an alloc. *) 650 659 lemma alloc_beloadv_conservation : 651 ∀m,m',block,offset,z1,z2, r,new_block.660 ∀m,m',block,offset,z1,z2,(*r,*)new_block. 652 661 valid_block m block → 653 alloc m z1 z2 r= 〈m', new_block〉 →662 alloc m z1 z2 (*r*) = 〈m', new_block〉 → 654 663 beloadv m (mk_pointer block offset) = beloadv m' (mk_pointer block offset). 655 * #contents #next #Hcorrect #m' #block #offset #z1 #z2 #r#new_block #Hvalid #Halloc664 * #contents #next #Hcorrect #m' #block #offset #z1 #z2 (* #r*) #new_block #Hvalid #Halloc 656 665 whd in Halloc:(??%?); destruct (Halloc) 657 666 whd in match (beloadv ??) in ⊢ (??%%); … … 661 670 cut (eqZb (block_id block) next = false) 662 671 [ lapply (Zltb_true_to_Zlt … Hlt) #Hlt' @eqZb_false /2 by not_to_not/ ] #Hneq 663 >Hneq cases (eq_region ??) normalize nodelta@refl672 >Hneq @refl 664 673 qed. 665 674 666 675 (* Lift [alloc_beloadv_conservation] to loadn *) 667 676 lemma alloc_loadn_conservation : 668 ∀m,m',z1,z2, r,new_block.669 alloc m z1 z2 r= 〈m', new_block〉 →677 ∀m,m',z1,z2,(*r,*)new_block. 678 alloc m z1 z2 (*r*) = 〈m', new_block〉 → 670 679 ∀n. ∀block,offset. 671 680 valid_block m block → 672 681 loadn m (mk_pointer block offset) n = loadn m' (mk_pointer block offset) n. 673 #m #m' #z1 #z2 #r#new_block #Halloc #n682 #m #m' #z1 #z2 (*#r*) #new_block #Halloc #n 674 683 elim n try // 675 684 #n' #Hind #block #offset #Hvalid_block … … 682 691 683 692 lemma alloc_load_value_of_type_conservation : 684 ∀m,m',z1,z2 ,r,new_block.685 alloc m z1 z2 r= 〈m', new_block〉 →693 ∀m,m',z1,z2(*,r*),new_block. 694 alloc m z1 z2 (*r*) = 〈m', new_block〉 → 686 695 ∀block,offset. 687 696 valid_block m block → 688 697 ∀ty. load_value_of_type ty m block offset = 689 698 load_value_of_type ty m' block offset. 690 #m #m' #z1 #z2 #r#new_block #Halloc #block #offset #Hvalid699 #m #m' #z1 #z2 (*#r*) #new_block #Halloc #block #offset #Hvalid 691 700 #ty cases ty 692 701 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain … … 701 710 lemma alloc_memory_inj_m2 : 702 711 ∀E:embedding. 703 ∀m1,m2,m2',z1,z2 ,r,new_block.712 ∀m1,m2,m2',z1,z2(*,r*),new_block. 704 713 ∀H:memory_inj E m1 m2. 705 alloc m2 z1 z2 r= 〈m2', new_block〉 →714 alloc m2 z1 z2 (*r*) = 〈m2', new_block〉 → 706 715 block_implementable_bv m2' new_block → 707 716 memory_inj E m1 m2'. 708 #E #m1 #m2 #m2' #z1 #z2 #r * #new_block #Hregion#Hmemory_inj #Halloc #Himpl717 #E #m1 #m2 #m2' #z1 #z2 (*#r*) * #new_block (* #Hregion *) #Hmemory_inj #Halloc #Himpl 709 718 % 710 719 [ whd … … 727 736  #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) 728 737 elim m2 in Halloc; #contentmap #nextblock #Hnextblock 729 elim p' * #br'#bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc)738 elim p' * (*#br'*) #bid' #o' #Halloc whd in Halloc:(??%?) ⊢ ?; destruct (Halloc) 730 739 whd in match (valid_pointer ??) in ⊢ (% → %); 731 740 @Zltb_elim_Type0 732 741 [ 2: normalize #_ #Habsurd destruct (Habsurd) ] 733 #Hbid' cut (Zltb bid' (Zsucc ne xtblock) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ]742 #Hbid' cut (Zltb bid' (Zsucc new_block) = true) [ lapply (Zlt_to_Zltb_true … Hbid') @zlt_succ ] 734 743 #Hbid_succ >Hbid_succ whd in match (low_bound ??) in ⊢ (% → %); 735 744 whd in match (high_bound ??) in ⊢ (% → %); 736 745 whd in match (update_block ?????); 737 746 whd in match (eq_block ??); 738 cut (eqZb bid' ne xtblock = false) [ 1: @eqZb_false /2 by not_to_not/ ]739 #Hbid_neq >Hbid_neq 740 cases (eq_region br' r) normalize #H @H 747 cut (eqZb bid' new_block = false) [ 1: @eqZb_false /2 by not_to_not/ ] 748 #Hbid_neq >Hbid_neq #H @H 749 (* cases (eq_region br' r) normalize #H @H*) 741 750  #b #b' #o' #Hembed lapply (mi_nodangling … Hmemory_inj b b' o' Hembed) #H 742 751 @(alloc_valid_block_conservation … Halloc … H) … … 745 754  #b lapply (mi_nowrap … Hmemory_inj b) 746 755 whd in ⊢ (% → %); 747 lapply (mi_nodangling … Hmemory_inj (block_id b))748 cases (E (block_id b)) normalize nodelta try //756 lapply (mi_nodangling … Hmemory_inj b) 757 cases (E b) normalize nodelta try // 749 758 * #B #OFF normalize nodelta #Hguard 750 759 * * #H1 #H2 #Hinbounds @conj try @conj try assumption 751 @(eq_block_elim … new_blockB)760 @(eq_block_elim … (mk_block new_block) B) 752 761 [ #H <H assumption 753 762  #H cases m2 in Halloc H2; #contents #nextblock #notnull … … 767 776 lemma alloc_memory_inj_m1 : 768 777 ∀E:embedding. 769 ∀m1,m2,m1',z1,z2, r,new_block.778 ∀m1,m2,m1',z1,z2,(*r,*)new_block. 770 779 ∀H:memory_inj E m1 m2. 771 alloc m1 z1 z2 r= 〈m1', new_block〉 →772 memory_inj (λx. if eq Zb (block_id (pi1 … new_block))x then None ? else E x) m1' m2 ∧773 embedding_compatible E (λx. if eq Zb (block_id (pi1 … new_block))x then None ? else E x).774 #E #m1 #m2 #m1' #z1 #z2 #r * #new_block #Hregion_eq#Hinj #Halloc775 cut (E (block_id new_block)= None ?)780 alloc m1 z1 z2 (*r*) = 〈m1', new_block〉 → 781 memory_inj (λx. if eq_block new_block x then None ? else E x) m1' m2 ∧ 782 embedding_compatible E (λx. if eq_block new_block x then None ? else E x). 783 #E #m1 #m2 #m1' #z1 #z2 (* #r*) #new_block (* #Hregion_eq *) #Hinj #Halloc 784 cut (E new_block = None ?) 776 785 [ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?); 777 786 #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ] 778 787 #Hempty 779 788 cut (embedding_compatible E 780 (λx :Z.781 if eq Zb (block_id new_block)x782 then None (block×offset) 783 else E x 784 [ whd #b @(eq Zb_elim … (block_id new_block) (block_id b)) normalize nodelta try // #Heq <Heq %1 @Hempty ]789 (λx. 790 if eq_block new_block x 791 then None (block×offset) 792 else E x)) 793 [ whd #b @(eq_block_elim … new_block b) normalize nodelta try // #Heq <Heq %1 @Hempty ] 785 794 #Hembedding_compatible @conj try assumption 786 795 % 787 796 [ whd #b1 #off1 #b2 #off2 #ty #v1 788 797 @(eq_block_elim … b1 new_block) 789 [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq Zb_z_znormalize nodelta798 [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta 790 799 #Habsurd destruct ] 791 800 #Hneq #Hvalid 792 801 whd in ⊢ ((??%?) → ?); 793 @(eq Zb_elim … (block_id new_block) (block_id b1))802 @(eq_block_elim … new_block b1) 794 803 normalize nodelta 795 804 [ #Heq #Habsurd destruct (Habsurd) ] … … 806 815 %{v2} @conj try assumption 807 816 @(embedding_compatibility_value_eq … Hveq2) assumption 808  #b #Hnot_valid @(eq Zb_elim … (block_id new_block) (block_id b))817  #b #Hnot_valid @(eq_block_elim … new_block b) 809 818 normalize nodelta 810 819 [ #Heq @refl … … 814 823 cases p #b #o cases p' #b' #o' normalize nodelta #Hvalidptr #Hvalid1' 815 824 whd in ⊢ ((??%%) → ?); 816 @(eq Zb_elim … (block_id new_block) (block_id b)) normalize nodelta825 @(eq_block_elim … new_block b) normalize nodelta 817 826 [ #Heq #Habsurd destruct ] 818 827 #Hneq #Hembed … … 820 829 #Hvalid1 821 830 @(Hvalidptr Hvalid1 Hembed) 822  #b #b' #o' @(eq Zb_elim … (block_id new_block)b)831  #b #b' #o' @(eq_block_elim … new_block b) 823 832 [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ] 824 833 normalize nodelta #Henq 825 834 @(mi_nodangling … Hinj) 826  #b #b' #o' @(eq Zb_elim … (block_id new_block) (block_id b))835  #b #b' #o' @(eq_block_elim … new_block b) 827 836 [ #Heq normalize nodelta #Habsurd destruct (Habsurd) ] 828 837 #Hneq @(mi_region … Hinj) 829 838  whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq 830 @(eq Zb_elim … (block_id new_block) (block_id b1))839 @(eq_block_elim … new_block b1) 831 840 normalize nodelta 832 841 [ #Heq #Habsurd destruct (Habsurd) ] 833 842 #Hneq1 #Hembed1 834 @(eq Zb_elim … (block_id new_block) (block_id b2))843 @(eq_block_elim … new_block b2) 835 844 normalize nodelta 836 845 [ #Heq #Habsurd destruct (Habsurd) ] 837 846 #Hneq2 #Hembed2 838 @(eq Zb_elim … (block_id b1') (block_id b2')) normalize nodelta try //847 @(eq_block_elim … b1' b2') normalize nodelta try // 839 848 #Heq 840 849 lapply (mi_nonalias … Hinj … b1 b2 b1' b2' delta1 delta2 Hneq Hembed1 Hembed2) >Heq 841 >eq Zb_z_znormalize nodelta850 >eq_block_b_b normalize nodelta 842 851 cases m1 in Halloc; #contents #next #Hnext 843 852 >unfold_high_bound >unfold_low_bound … … 845 854 >unfold_high_bound >unfold_low_bound 846 855 >unfold_high_bound >unfold_low_bound 847 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 848 cut (eq_block b1 (mk_block r next) = false) 849 [ whd in ⊢ (??%%); 850 >(eqZb_false … (sym_neq ??? Hneq1)) 851 cases (eq_region ??) @refl ] 852 cut (eq_block b2 (mk_block r next) = false) 853 [ whd in ⊢ (??%%); 854 >(eqZb_false … (sym_neq ??? Hneq2)) 855 cases (eq_region ??) @refl ] 856 whd in ⊢ ((??%%) → ?); destruct (Heq) #Heq destruct (Heq) 857 lapply (neq_block_eq_block_false … (sym_neq ??? Hneq1)) 858 lapply (neq_block_eq_block_false … (sym_neq ??? Hneq2)) 856 859 #Heq_block_2 857 860 #Heq_block_1 … … 876 879 >Heq_block_1 >Heq_block_2 @H 877 880 ] 878  #b whd @(eq Zb_elim … (block_id new_block) (block_id b)) normalize nodelta try //881  #b whd @(eq_block_elim … new_block b) normalize nodelta try // 879 882 #Hneq lapply (mi_nowrap … Hinj b) whd in ⊢ (% → ?); 880 cases (E (block_id b)) normalize nodelta try //883 cases (E b) normalize nodelta try // 881 884 * #bb #oo normalize nodelta 882 885 * * * #HA #HB * #HC #HD #HE @conj try @conj … … 892 895 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) try // 893 896 whd in match (update_block ?????); 894 cut (eq_block b (mk_block r next) = false) 895 [ 1,3,5: whd in ⊢ (??%%); 896 >(eqZb_false … (sym_neq ??? Hneq)) 897 cases (eq_region ??) @refl 897 cut (eq_block b (mk_block next) = false) 898 [ 1,3,5: @neq_block_eq_block_false @(sym_neq … Hneq) 898 899  2,4,6: #Heq_block >Heq_block // ] 899 ] qed. 900 901 900 ] qed. 901 902 (* In CompCert, "∀v. value_eq Vundef v" holds. Not in our developments. In order 903 * to prove the equivalent of lemma 68 of L&B, we need to provide an additional 904 * property of the target memory: the /target/ portion of memory we are going to map a block 905 * to must only contains BVundef (whereas in CompCert, the fact that the source block 906 * contains BVundefs is enough to proceed). 907 * 908 * The following definition expresses the fact that a portion of memory [z1; z2] contains only 909 * BVundefs. 910 * Note that the bounds are /inclusive/. We do not check for their validity. *) 911 definition undef_memory_zone : mem → block → Z → Z → Prop ≝ 912 λm,b,z1,z2. 913 ∀i. z1 ≤ i → i ≤ z2 → contents (blocks m b) i = BVundef. 914 915 (* Explictly stating the properties of alloc. *) 916 lemma alloc_properties : 917 ∀m,m',z1,z2(*,r*),b. 918 alloc m z1 z2 (* r *) = 〈m',b〉 → 919 low_bound m' b = z1 ∧ 920 high_bound m' b = z2 ∧ 921 undef_memory_zone m' b z1 z2. 922 #m #m' #z1 #z2 * (* #br *) #bid 923 cases m #contents #next #Hnext 924 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq) 925 >unfold_low_bound >unfold_high_bound 926 @conj try @conj 927 /2 by refl, pair_destruct_2/ 928 whd 929 #i #H1 #H2 whd in match (update_block ?????); 930 >eq_block_b_b normalize nodelta @refl 931 qed. 932 933 (* Embed a fresh block inside an unmapped portion of the target block. 934 * This is the equivalent of lemma 68 of Leroy&Blazy. 935 * Compared to L&B, an additional "undef_memory_zone" proof object must be provided. 936 *) 937 lemma alloc_memory_inj_m1_to_m2 : 938 ∀E:embedding. 939 ∀m1,m2,m1':mem. 940 ∀z1,z2:Z. 941 ∀target,new_block. 942 ∀delta:offset. 943 valid_block m2 target → 944 alloc m1 z1 z2 = 〈m1', new_block〉 → 945 low_bound m2 target ≤ z1 + Zoo delta → 946 z2 + Zoo delta ≤ high_bound m2 target → 947 undef_memory_zone m2 target (z1 + Zoo delta) (z2 + Zoo delta) → 948 (∀b,delta'. b ≠ new_block → 949 E b = Some ? 〈target, delta'〉 → 950 high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨ 951 z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) → 952 memory_inj E m1 m2 → 953 memory_inj (λx. if eq_block new_block x then Some ? 〈target, delta〉 else E x) m1' m2. 954 #E #m1 #m2 #m1' #z1 #z2 (* * #tr *) #tid (* * * #newr *) #newid (* * *) #delta 955 #Hvalid #Halloc #Hlow #Hhigh #Hundef_zone #Hno_interference #Hinj 956 cut (E newid = (None ?)) 957 [ @(mi_freeblock ??? Hinj newid) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj 958 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ] 959 @cthulhu 960 qed. 961 (* 962 #Hnew_not_mapped 963 cut (embedding_compatible E (λx. if eqZb newid x then Some ? 〈mk_block newr tid, delta〉 else E x)) 964 [ whd #b @(eqZb_elim … newid (block_id b)) normalize nodelta try // #Heq <Heq %1 assumption ] 965 #Hembedding_compatible 966 % 967 [ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid' #Hembed #Hload 968 @(eqZb_elim … newid (block_id b1)) 969 [ 2: (* we do not load from the newly allocated block *) 970 #Hneq 971 (* prove that we can equivalently load from the memory before alloc *) 972 cases (some_inversion ????? Hembed) * #target' #delta' 973 >(eqZb_false … Hneq) normalize nodelta 974 * #Hembed #Heq destruct (Heq) 975 cases (valid_pointer_to_Prop … Hvalid') * #Hvalid_block' #Hlow #Hhigh 976 lapply (alloc_valid_block_conservation2 … Halloc … (sym_neq ??? Hneq) Hvalid_block') 977 #Hvalid_block 978 lapply (alloc_load_value_of_type_conservation … Halloc b1 off1 … Hvalid_block ty) 979 #Heq_load <Heq_load in Hload; #Hload 980 lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … (sym_neq ??? Hneq) Hvalid') 981 #Hvalid_ptr 982 lapply (mi_inj … Hinj b1 off1 b2 (offset_plus off1 delta') … Hvalid_ptr … Hload) 983 [ whd in ⊢ (??%?); >Hembed @refl ] 984 (* conclude *) 985 * #v2 * #Hload2 #Hvalue_eq %{v2} @conj 986 [ @Hload2 987  @(embedding_compatibility_value_eq … Hvalue_eq) @Hembedding_compatible ] 988  1: (* we allegedly performed a load from a block with the same id as 989 * the newly allocated block (which by def. of alloc contains only BVundefs) *) 990 #Heq destruct (Heq) 991 whd in Hembed:(??%?); >eqZb_z_z in Hembed; normalize nodelta 992 #Heq_ptr 993 (* cull out all boring cases *) 994 lapply Hload Hload cases ty 995 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 996  #structname #fieldspec  #unionname #fieldspec  #id ] 997 [ 1,6,7: whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) 998  4,5: whd in ⊢ ((??%?) → ?); #Heq destruct (Heq_ptr Heq) 999 %{(Vptr (mk_pointer (mk_block newr tid) (offset_plus off1 delta)))} 1000 @conj 1001 [ 1,3: @refl 1002  *: %4 whd in ⊢ (??%?); >eqZb_z_z @refl ] ] 1003 (* Now: loadbyvalue cases. Outcome is either None or Undef. *) 1004 lapply (load_by_value_after_alloc_undef m1 m1' z1 z2 b1 ?) 1005 [ 1,3,5: 1006 #Hload_eq 1007 [ lapply (Hload_eq (Tint sz sg) (refl ??) off1) 1008  lapply (Hload_eq (Tpointer ptr_ty) (refl ??) off1) 1009  lapply (Hload_eq (Tcomp_ptr id) (refl ??) off1) ] 1010 * 1011 (* None case: absurd *) 1012 [ 2,4,6: >Hload #Habsurd destruct (Habsurd) ] 1013 >Hload #Heq destruct (Heq) %{Vundef} 1014 @conj try // 1015 cut (valid_pointer m2 (mk_pointer b2 (offset_plus off1 delta))=true) 1016 [ 1,3,5: @valid_pointer_of_Prop @conj try @conj 1017 [ 1,4,7: assumption 1018  2,5,8: >unfold_low_bound 1019 lapply (alloc_properties … Halloc) * * 1020 >unfold_low_bound >unfold_high_bound #Hlow #Hhigh #Hundef 1021 lapply (valid_pointer_to_Prop … Hvalid') * * 1022 #Hblock_valid >unfold_low_bound >unfold_high_bound >Hlow >Hhigh 1023 *) 902 1024 903 1025 (* Embed a fresh block inside an unmapped portion of the target block. 904 1026 * This is the equivalent of lemma 68 for Leroy&Blazy. *) 1027 (* 905 1028 axiom alloc_memory_inj_m1_to_m2 : 906 1029 ∀E:embedding. … … 919 1042 memory_inj E m1 m2 → 920 1043 memory_inj (λx. if eqZb (block_id (pi1 … new_block)) x then Some ? 〈b2, delta〉 else E x) m1' m2. 1044 *) 921 1045 922 1046 (*  *) … … 969 1093 load_sim_ptr E m1 m2 → 970 1094 ∀b. free m2 b = m2' → 971 (∀b1,delta. E (block_id b1)= Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) →1095 (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) → 972 1096 load_sim_ptr E m1 m2'. 973 1097 #E #m1 #m2 #m2' #Hsim #b #Hfree #Hunmapped … … 1054 1178 #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq 1055 1179 #Hembed1 #Hembed2 1056 @(eq Zb_elim … (block_id b1') (block_id b2')) normalize nodelta1180 @(eq_block_elim … b1' b2') normalize nodelta 1057 1181 [ 2: try // ] 1058 1182 #Hblocks_eq … … 1060 1184 lapply Hembed1 Hembed1 1061 1185 lapply Hblocks_eq Hblocks_eq 1062 cases b1' #r1' #bid1'1063 cases b2' #r2' #bid2' 1186 (*cases b1' #r1' #bid1' 1187 cases b2' #r2' #bid2' *) 1064 1188 #Heq destruct (Heq) 1065 generalize in match b id2';1189 generalize in match b2'; 1066 1190 #target #Hembed1 #Hembed2 1067 1191 lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2) 1068 >eq Zb_z_znormalize nodelta1192 >eq_block_b_b normalize nodelta 1069 1193 normalize nodelta <Hfree 1070 1194 @(eq_block_elim … b1 b) … … 1112 1236  @(free_non_aliasing_m1 … Hinj … Hfree) 1113 1237  #bb whd lapply (Himplementable bb) whd in ⊢ (% → ?); 1114 cases (E (block_id bb)) normalize nodelta try //1238 cases (E bb) normalize nodelta try // 1115 1239 * #BLO #DELTA normalize nodelta * * #HA #HB #HC @conj try @conj 1116 1240 try // … … 1140 1264 memory_inj E m1 m2 → 1141 1265 ∀b. free m2 b = m2' → 1142 (∀b1,delta. E (block_id b1)= Some ? 〈b, delta〉 →1266 (∀b1,delta. E b1 = Some ? 〈b, delta〉 → 1143 1267 (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 1144 1268 memory_inj E m1 m2'. … … 1171 1295  @Hregion 1172 1296  #bb lapply (Himpl bb) 1173 whd in ⊢ (% → %); cases (E (block_id bb)) normalize nodelta try //1297 whd in ⊢ (% → %); cases (E bb) normalize nodelta try // 1174 1298 * #BLO #OFF normalize nodelta * * destruct (Hfree) 1175 1299 #Hbb #HBLO #Hbound whd in match (free ??); @conj try @conj try @conj try assumption … … 1191 1315 memory_inj E m1 m2 → 1192 1316 ∀blocklist,b2. 1193 (∀b1,delta. E (block_id b1)= Some ? 〈b2, delta〉 → meml ? b1 blocklist) →1317 (∀b1,delta. E b1 = Some ? 〈b2, delta〉 → meml ? b1 blocklist) → 1194 1318 free m2 b2 = m2' → 1195 1319 free_list m1 blocklist = m1' → … … 1253 1377 else false) normalize nodelta 1254 1378 [ 2: #Habsurd destruct (Habsurd) ] 1255 #Heq destruct (Heq) elim rb in Hblock_neq; #rr #rid elim wb #wr #wid1256 cases rr cases wr normalizetry //1257 @(eqZb_elim … rid wid)1258 [ 1,3: #Heq destruct (Heq) >(eqZb_reflexive wid) #Habsurd destruct (Habsurd)]1259 try // 1379 #Heq destruct (Heq) 1380 cases (Zltb (block_id rb) (nextblock mA)) normalize nodelta try // 1381 cut (eqZb (block_id rb) (block_id wb) = false) 1382 [ >eqZb_symmetric @Hblock_neq ] 1383 #Heqzb >Heqzb normalize nodelta @refl 1260 1384 qed. 1261 1385 … … 1327 1451 memory_inj E mA mB → 1328 1452 ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → 1329 ∀b1,delta. E (block_id b1)= Some ? 〈blo,delta〉 →1453 ∀b1,delta. E b1 = Some ? 〈blo,delta〉 → 1330 1454 high_bound mA b1 + Zoo delta < Zoo wo → 1331 1455 ∀ty,off. … … 1405 1529 memory_inj E mA mB → 1406 1530 ∀blo. storen mB (mk_pointer blo wo) l = Some ? mC → 1407 ∀b1,delta. E (block_id b1)= Some ? 〈blo,delta〉 →1531 ∀b1,delta. E b1 = Some ? 〈blo,delta〉 → 1408 1532 Zoo wo < low_bound mA b1 + Zoo delta → 1409 1533 ∀ty,off. … … 1422 1546 ∀block2. ∀i : offset. ∀ty : type. 1423 1547 (∀block1,delta. 1424 E (block_id block1)= Some ? 〈block2, delta〉 →1548 E block1 = Some ? 〈block2, delta〉 → 1425 1549 (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → 1426 1550 ∀v.store_value_of_type ty mB block2 i v = Some ? mC → … … 1478 1602 ∀block2. ∀i : offset. ∀ty : type. 1479 1603 (∀block1,delta. 1480 E (block_id block1)= Some ? 〈block2, delta〉 →1604 E block1 = Some ? 〈block2, delta〉 → 1481 1605 (high_bound mA block1 + (Zoo delta) < (Zoo i)) ∨ (Zoo i + (sizeof ty) ≤ (low_bound mA block1 + (Zoo delta)))) → 1482 1606 ∀v.store_value_of_type ty mB block2 i v = Some ? mC → … … 1508 1632 >(Hnext_eq) try // 1509 1633  #b lapply (mi_nowrap … Hinj b) whd in ⊢ (% → %); 1510 cases (E (block_id b)) try //1634 cases (E b) try // 1511 1635 * #BLO #OFF normalize nodelta * * 1512 1636 #Hb #HBLO #Hbound try @conj try @conj try assumption … … 1526 1650 lemma be_to_fe_value_ptr : 1527 1651 ∀b,o. (be_to_fe_value ASTptr (fe_to_be_values ASTptr (Vptr (mk_pointer b o))) = Vptr (mk_pointer b o)). 1528 #b * #o whd in ⊢ (??%%); normalize cases b #br#bid normalize nodelta1529 cases br normalize nodelta>eqZb_z_z normalize nodelta1652 #b * #o whd in ⊢ (??%%); normalize cases b (* #br *) #bid normalize nodelta 1653 (*cases br normalize nodelta *) >eqZb_z_z normalize nodelta 1530 1654 cases (vsplit_eq bool 7 8 … o) #lhs * #rhs #Heq 1531 1655 <(vsplit_prod … Heq) >eq_v_true normalize nodelta try @refl … … 1570 1694 ∀E,m1,m2. 1571 1695 memory_inj E m1 m2 → 1572 ∀b1,b2,delta. E (block_id b1)= Some ? 〈b2,delta〉 →1696 ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 → 1573 1697 ∀v1,v2. value_eq E v1 v2 → 1574 1698 ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ … … 1639 1763 ∀E,m1,m2. 1640 1764 memory_inj E m1 m2 → 1641 ∀b1,b2,delta. E (block_id b1)= Some ? 〈b2,delta〉 →1765 ∀b1,b2,delta. E b1 = Some ? 〈b2,delta〉 → 1642 1766 ∀v1,v2. value_eq E v1 v2 → 1643 1767 ∀i,m1',ty. storen m1 (mk_pointer b1 i) (fe_to_be_values ty v1) = Some ? m1'→ … … 1662 1786 ∀Hinj:memory_inj E m1 m2. 1663 1787 ∀v1,v2. value_eq E v1 v2 → 1664 ∀b1,b2,delta. E (block_id b1)= Some ? 〈b2, delta〉 →1788 ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → 1665 1789 ∀ty,i,m1'. 1666 1790 ast_typ_consistent_with_value ty v1 → … … 1750 1874 ∀Hinj:memory_inj E m1 m2. 1751 1875 ∀v1,v2. value_eq E v1 v2 → 1752 ∀b1,b2,delta. E (block_id b1)= Some ? 〈b2, delta〉 →1876 ∀b1,b2,delta. E b1 = Some ? 〈b2, delta〉 → 1753 1877 ∀ty,i,m1'. 1754 1878 type_consistent_with_value ty v1 → … … 1770 1894 ∀Hinj:memory_inj E m1 m2. 1771 1895 ∀ty,b,i,v. 1772 E (block_id b)= None ? →1896 E b = None ? → 1773 1897 store_value_of_type ty m1 b i v = Some ? m1' → 1774 1898 load_sim_ptr E m1' m2. … … 1820 1944 ∀Hinj:memory_inj E m1 m2. 1821 1945 ∀ty,b,i,v. 1822 E (block_id b)= None ? →1946 E b = None ? → 1823 1947 store_value_of_type ty m1 b i v = Some ? m1' → 1824 1948 memory_inj E m1' m2. … … 1849 1973  #bb whd 1850 1974 lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?); 1851 cases (E (block_id bb)) normalize nodelta try // * #bb' #off1975 cases (E bb) normalize nodelta try // * #bb' #off 1852 1976 normalize nodelta 1853 1977 whd in match (block_implementable_bv ??); … … 1952 2076 @(ex_intro … (conj … (refl …) ?)) 1953 2077 @vptr_eq whd in match (pointer_translation ??); 1954 cases (E (block_id b1')) in Hembed;2078 cases (E b1') in Hembed; 1955 2079 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 1956 2080  2: * #block #offset normalize nodelta #Heq destruct (Heq) … … 1994 2118 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 1995 2119 elim p1 in Hembed; #b1 #o1 normalize nodelta 1996 cases (E (block_id b1))2120 cases (E b1) 1997 2121 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 1998 2122  2: * #block #offset normalize nodelta #Heq destruct (Heq) … … 2093 2217 @vptr_eq whd in match (pointer_translation ??) in Hembed ⊢ %; 2094 2218 elim p1 in Hembed; #b1 #o1 normalize nodelta 2095 cases (E (block_id b1))2219 cases (E b1) 2096 2220 [ 1: normalize in ⊢ (% → ?); #Habsurd destruct (Habsurd) 2097 2221  2: * #block #offset normalize nodelta #Heq destruct (Heq) … … 2109 2233 elim p1' #b1' #off1' whd in ⊢ (% → % → ?); #Hpblock1_eq destruct (Hpblock1_eq) 2110 2234 whd in ⊢ ((??%?) → (??%?) → ?); 2111 cases (E (block_id b1')) normalize nodelta2235 cases (E b1') normalize nodelta 2112 2236 [ 1: #Habsurd destruct (Habsurd) ] 2113 2237 * #dest_block #dest_off normalize nodelta … … 2515 2639 lapply (mi_nowrap … Hinj bq1) 2516 2640 whd in ⊢ (% → ?); 2517 cases (E (block_id bq1)) normalize nodelta2641 cases (E bq1) normalize nodelta 2518 2642 [ #_ #Habsurd destruct ] 2519 2643 * #BLO #OFF normalize nodelta * * … … 2536 2660 lapply (mi_region … Hinj bq1) 2537 2661 lapply (mi_region … Hinj bp1) 2538 cases (E (block_id bq1)) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ]2662 cases (E bq1) [ 1: #_ #_ #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2539 2663 * #BLOq #DELTAq normalize nodelta 2540 cases (E (block_id bp1)) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ]2664 cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #_ #_ #Habsurd destruct (Habsurd) ] 2541 2665 * #BLOp #DELTAp normalize nodelta #Hregion1 #Hregion2 #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct 2542 2666 lapply (Hregion1 … (refl ??)) lapply (Hregion2 … (refl ??)) Hregion1 Hregion2 … … 2556 2680 lapply (valid_pointer_to_Prop … Hvalid') 2557 2681 * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp 2558 >eq Zb_z_z >eq_block_b_b normalize nodelta2682 >eq_block_b_b normalize nodelta 2559 2683 * 2560 2684 [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind
Note: See TracChangeset
for help on using the changeset viewer.