Changeset 2598 for src/Clight/memoryInjections.ma
 Timestamp:
 Jan 31, 2013, 12:56:03 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/memoryInjections.ma
r2594 r2598 579 579 qed. 580 580 581 (* A valid pointer stays valid after an alloc *) 582 (* 583 lemma alloc_valid_pointer_conservation : 584 ∀m,m',z1,z2,r,new_block. 585 alloc m z1 z2 r = 〈m', new_block〉 → 586 ∀p. valid_pointer m p = true → valid_pointer m' p = true. 587 #m #m' #z1 #z2 #r * #new_block #Hregion_eq #Halloc 588 #p #Hvalid @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid) 589 Hvalid lapply Halloc Halloc cases m #cont #next #Hnext 590 whd in ⊢ ((??%%) → ?); 591 #Heq destruct (Heq) * * #Hblock_id 592 >unfold_low_bound >unfold_high_bound 593 >unfold_low_bound >unfold_high_bound 594 whd in match (update_block ?????); 595 whd in match (update_block ?????); 596 #HA #HB % [ % [ /2 by Zlt_to_Zle_to_Zlt/ ] ] 597 @(eq_block_elim … (pblock p) (mk_block r next)) 598 [ 1,3: cases p in Hblock_id; #b #o #H #Heq destruct 599 @False_ind 600 @(absurd … H (irreflexive_Zlt ?)) 601  *: #Hneq normalize nodelta try assumption ] 602 qed.*) 603 604 605 lemma Zle_split : 606 ∀a,b:Z. a ≤ b → a ≠ b → a < b. 607 #a #b elim a elim b try /2/ 608 #p1 #p2 #Hle #Hneq whd 609 @not_eq_to_le_to_lt 610 try // % #Heq destruct cases Hneq #H @H @refl 611 qed. 612 613 lemma alloc_valid_pointer_conservation : 614 ∀m,m',z1,z2,r,new_block. 615 alloc m z1 z2 r=〈m',new_block〉 → 616 ∀p. (pblock p) ≠ (pi1 … new_block) → 617 block_region (pblock p) = block_region (pi1 … new_block) → 618 valid_pointer m' p = true → 619 valid_pointer m p = true. 620 #m #m' #z1 #z2 #r * #new_block #Hregion 621 cases m #cont #next #Hnext 622 whd in ⊢ ((??%%) → ?); 623 #Heq destruct (Heq) * #b #o #Hneq #Hregion #Hvalid 624 @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid) 625 Hvalid 626 * * #Hblock_id 627 >unfold_low_bound >unfold_high_bound 628 >unfold_low_bound >unfold_high_bound 629 whd in match (update_block ?????); 630 whd in match (update_block ?????); 631 >(not_eq_block … Hneq) normalize nodelta 632 #HA #HB % [ % ] try assumption 633 cases b in Hneq Hregion Hblock_id; #r' #id * #Hnext_not_id #Hregion destruct 634 cut (next ≠ id) 635 [ % #H destruct @Hnext_not_id @refl ] 636 #Hneq #Hlt cut (id ≤ next) 637 [ /3 by monotonic_Zle_Zpred, Zlt_to_Zle/ ] 638 #Hle @Zle_split try @Hle @sym_neq @Hneq 639 qed. 640 581 641 (* Allocating a new zone produces a valid block. *) 582 642 lemma alloc_valid_new_block : … … 624 684 625 685 (* Memory allocation in m2 preserves [memory_inj]. 626 * This is lemma 43from Leroy&Blazy. *)686 * This is lemma 66 from Leroy&Blazy. *) 627 687 lemma alloc_memory_inj_m2 : 628 688 ∀E:embedding. … … 693 753 * of the allocation. *) 694 754 755 lemma block_neq_elim : 756 ∀b1,b2. b1 ≠ b2 → 757 (block_id b1 ≠ block_id b2 ∧ block_region b1 = block_region b2) ∨ 758 (block_id b1 = block_id b2 ∧ block_region b1 ≠ block_region b2) ∨ 759 (block_id b1 ≠ block_id b2 ∧ block_region b1 ≠ block_region b2). 760 * #r #id * #r' #id' 761 cases r cases r' 762 @(eqZb_elim … id id') 763 #H1 #H2 764 [ 1,7: destruct @False_ind @(absurd … (refl ??) H2) ] 765 try /4 by or_introl, or_intror, conj/ 766 destruct 767 [ %1 %2 @conj // % #H destruct 768  %2 @conj try @H1 % #H destruct 769  %1 %2 @conj // % #H destruct 770  %2 @conj try @H1 % #H destruct ] 771 qed. 772 695 773 (* Allocating in m1 such that the resulting block has no image in m2 preserves 696 the injection. This is lemma 44for Leroy&Blazy. The proof should proceed as774 the injection. This is lemma 67 for Leroy&Blazy. The proof should proceed as 697 775 in Blazy & Leroy. Careful of using the mi_embedding hypothesis to rule out 698 776 absurd cases. *) 699 axiomalloc_memory_inj_m1 :777 lemma alloc_memory_inj_m1 : 700 778 ∀E:embedding. 701 779 ∀m1,m2,m1',z1,z2,r,new_block. 702 780 ∀H:memory_inj E m1 m2. 703 781 alloc m1 z1 z2 r = 〈m1', new_block〉 → 704 E (pi1 … new_block) = None ? → 705 memory_inj E m1' m2. 782 memory_inj (λx. if eq_block x (pi1 … new_block) then None ? else E x) m1' m2 ∧ 783 embedding_compatible E (λx. if eq_block x (pi1 … new_block) then None ? else E x). 784 @cthulhu 785 qed. (* XXX finish this. *) 786 (* 787 #E #m1 #m2 #m1' #z1 #z2 #r * #new_block #Hregion_eq #Hinj #Halloc 788 cut (E new_block = None ?) 789 [ @(mi_freeblock … Hinj) cases m1 in Hinj Halloc; #contents #next #Hpos #Hinj whd in ⊢ ((??%%) → ?); 790 #Heq destruct (Heq) % #H whd in H; @(absurd … H (irreflexive_Zlt … next)) ] 791 #Hempty % 792 [ 2: whd #b @(eq_block_elim … b new_block) try // #Heq destruct (Heq) >Hempty %1 @refl ] 793 % 794 [ whd #b1 #off1 #b2 #off2 #ty #v1 795 @(eq_block_elim … b1 new_block) 796 [ #Heq destruct #_ whd in ⊢ ((??%?) → ?); >eq_block_b_b normalize nodelta 797 #Habsurd destruct ] 798 #Hneq #Hvalid 799 whd in ⊢ ((??%?) → ?); >(not_eq_block … Hneq) normalize nodelta 800 #Hembed cases (some_inversion ????? Hembed) * #b1' #off' * #Hembed 801 normalize nodelta #Heq destruct (Heq) 802 lapply (block_neq_elim … Hneq) 803 * 804 [ 2: * #Hid_neq #Hregion_neq 805 lapply (alloc_valid_pointer_conservation … Halloc (mk_pointer b1 off1) … Hneq) 806 *) 807 706 808 707 809 (* Embed a fresh block inside an unmapped portion of the target block. 708 * This is the equivalent of lemma 45for Leroy&Blazy. *)810 * This is the equivalent of lemma 68 for Leroy&Blazy. *) 709 811 axiom alloc_memory_inj_m1_to_m2 : 710 812 ∀E:embedding. … … 712 814 ∀z1,z2:Z. 713 815 ∀b2,new_block. 714 ∀delta:offset. 715 ∀H:memory_inj E m1 m2.816 ∀delta:offset. 817 valid_block m2 b2 → 716 818 alloc m1 z1 z2 (block_region b2) = 〈m1', new_block〉 → 717 E (pi1 … new_block) = Some ? 〈b2, delta〉 →718 819 low_bound m2 b2 ≤ z1 + Zoo delta → 719 820 z2 + Zoo delta ≤ high_bound m2 b2 → … … 722 823 high_bound m1 b + (Zoo delta') ≤ z1 + (Zoo delta) ∨ 723 824 z2 + (Zoo delta) ≤ low_bound m1 b + (Zoo delta')) → 724 memory_inj E m1' m2. 825 memory_inj E m1 m2 → 826 memory_inj (λx. if eq_block x (pi1 … new_block) then Some ? 〈b2, delta〉 else E x) m1' m2. 725 827 726 828 (*  *)
Note: See TracChangeset
for help on using the changeset viewer.