Changeset 496 for Deliverables/D3.1/Csemantics/Mem.ma
 Timestamp:
 Feb 11, 2011, 4:45:28 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Mem.ma
r487 r496 40 40 λy.match eqZb y x with [ true ⇒ v  false ⇒ f y ]. 41 41 42 (* Implicit Arguments update [A].*)43 44 42 lemma update_s: 45 43 ∀A: Type[0]. ∀x: Z. ∀v: A. ∀f: Z > A. … … 61 59 //; qed. 62 60 61 definition update_block : ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block → A. block → A ≝ 62 λA,x,v,f. 63 λy.match eq_block y x with [ true ⇒ v  false ⇒ f y ]. 64 65 lemma update_block_s: 66 ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block > A. 67 update_block … x v f x = v. 68 #A * * #ix #v #f whd in ⊢ (??%?); 69 >(eqZb_z_z …) //; 70 qed. 71 72 lemma update_block_o: 73 ∀A: Type[0]. ∀x: block. ∀v: A. ∀f: block > A. ∀y: block. 74 x ≠ y → update_block … x v f y = f y. 75 #A #x #v #f #y #H whd in ⊢ (??%?); 76 @eq_block_elim //; 77 #H2 cases H;#H3 elim (H3 ?);//; 78 qed. 79 80 (* FIXME: workaround for lack of nunfold *) 81 lemma unfold_update_block : ∀A,x,v,f,y. 82 update_block A x v f y = match eq_block y x with [ true ⇒ v  false ⇒ f y ]. 83 //; qed. 84 63 85 64 86 (* * Structure of memory states *) … … 87 109 low: Z; 88 110 high: Z; 89 contents: contentmap; 90 space: region 111 contents: contentmap 91 112 }. 92 113 93 (* A memory state is a mapping from block addresses (represented by [Z]94 integers) to blocks. We also maintain the address of the next114 (* A memory state is a mapping from block addresses (represented by memory 115 regions and integers) to blocks. We also maintain the address of the next 95 116 unallocated block, and a proof that this address is positive. *) 96 117 97 118 record mem : Type[0] ≝ { 98 blocks: Z> block_contents;99 nextblock: block;119 blocks: block > block_contents; 120 nextblock: Z; 100 121 nextblock_pos: OZ < nextblock 101 122 }. … … 195 216 qed. 196 217 197 definition empty_block : Z → Z → region →block_contents ≝198 λlo,hi ,bty.mk_block_contents lo hi (λy. Undef) bty.218 definition empty_block : Z → Z → block_contents ≝ 219 λlo,hi.mk_block_contents lo hi (λy. Undef). 199 220 200 221 definition empty: mem ≝ 201 mk_mem (λx.empty_block OZ OZ Any) (pos one) one_pos.202 203 definition nullptr: block ≝ OZ.222 mk_mem (λx.empty_block OZ OZ) (pos one) one_pos. 223 224 definition nullptr: block ≝ 〈Any,OZ〉. 204 225 205 226 (* Allocation of a fresh block with the given bounds. Return an updated … … 216 237 217 238 definition alloc : mem → Z → Z → region → mem × block ≝ 218 λm,lo,hi, bty.〈mk_mem219 (update … (nextblock m)220 (empty_block lo hi bty)239 λm,lo,hi,r.〈mk_mem 240 (update_block … 〈r,nextblock m〉 241 (empty_block lo hi) 221 242 (blocks m)) 222 243 (Zsucc (nextblock m)) 223 244 (succ_nextblock_pos m), 224 nextblock m〉.245 〈r,nextblock m〉〉. 225 246 226 247 (* Freeing a block. Return the updated memory state where the given … … 231 252 232 253 definition free ≝ 233 λm,b.mk_mem (update … b234 (empty_block OZ OZ Any)254 λm,b.mk_mem (update_block … b 255 (empty_block OZ OZ) 235 256 (blocks m)) 236 257 (nextblock m) … … 252 273 definition high_bound : mem → block → Z ≝ 253 274 λm,b.high (blocks m b). 254 definition block_ space: mem → block → region ≝255 λm,b. space (blocks m b).275 definition block_region: mem → block → region ≝ 276 λm,b.\fst b. (* TODO: should I keep the mem argument for uniformity, or get rid of it? *) 256 277 257 278 (* A block address is valid if it was previously allocated. It remains valid 258 279 even after being freed. *) 259 280 281 (* TODO: should this check for region? *) 260 282 definition valid_block : mem → block → Prop ≝ 261 λm,b. b < nextblock m.283 λm,b.\snd b < nextblock m. 262 284 263 285 (* FIXME: hacks to get around lack of nunfold *) … … 266 288 lemma unfold_high_bound : ∀m,b. high_bound m b = high (blocks m b). 267 289 //; qed. 268 lemma unfold_valid_block : ∀m,b. (valid_block m b) = ( b < nextblock m).290 lemma unfold_valid_block : ∀m,b. (valid_block m b) = (\snd b < nextblock m). 269 291 //; qed. 270 292 … … 564 586 qed. 565 587 *) 566 (* pointer_compat block_ space pointer_space*)588 (* pointer_compat block_region pointer_region *) 567 589 568 590 inductive pointer_compat : region → region → Prop ≝ 569  same_compat : ∀s. pointer_compat s s570  pxdata_compat : pointer_compat PData XData591  same_compat : ∀s. pointer_compat s s 592  pxdata_compat : pointer_compat PData XData 571 593  unspecified_compat : ∀p. pointer_compat Any p 572  universal_compat : ∀b. pointer_compat b Any.594  universal_compat : ∀b. pointer_compat b Any. 573 595 574 596 lemma pointer_compat_dec : ∀b,p. pointer_compat b p + ¬pointer_compat b p. … … 581 603 λb,p. match pointer_compat_dec b p with [ inl _ ⇒ true  inr _ ⇒ false ]. 582 604 583 (* [valid_access m chunk pspb ofs] holds if a memory access (load or store)605 (* [valid_access m chunk r b ofs] holds if a memory access (load or store) 584 606 of the given chunk is possible in [m] at address [b, ofs]. 585 607 This means: … … 587 609  The range of bytes accessed is within the bounds of [b]. 588 610  The offset [ofs] is aligned. 589  The pointer classs [psp] is compatible with the class of [b].611  The pointer representation (i.e., region) [r] is compatible with the class of [b]. 590 612 *) 591 613 592 inductive valid_access (m: mem) (chunk: memory_chunk) ( psp: region) (b: block) (ofs: Z)614 inductive valid_access (m: mem) (chunk: memory_chunk) (r: region) (b: block) (ofs: Z) 593 615 : Prop ≝ 594 616  valid_access_intro: … … 597 619 ofs + size_chunk chunk ≤ high_bound m b → 598 620 (align_chunk chunk ∣ ofs) → 599 pointer_compat (block_ space m b) psp→600 valid_access m chunk pspb ofs.621 pointer_compat (block_region m b) r → 622 valid_access m chunk r b ofs. 601 623 602 624 (* The following function checks whether accessing the given memory chunk … … 605 627 (* XXX: Using + and ¬ instead of Sum and Not causes trouble *) 606 628 let rec in_bounds 607 (m:mem) (chunk:memory_chunk) (psp:region) (b:block) (ofs:Z) on b : 608 Sum (valid_access m chunk psp b ofs) (Not (valid_access m chunk psp b ofs)) ≝ ?. 609 @(Zltb_elim_Type0 b (nextblock m)) #Hnext 610 [ @(Zleb_elim_Type0 (low_bound m b) ofs) #Hlo 611 [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m b)) #Hhi 629 (m:mem) (chunk:memory_chunk) (r:region) (b:block) (ofs:Z) on b : 630 Sum (valid_access m chunk r b ofs) (Not (valid_access m chunk r b ofs)) ≝ ?. 631 cases b #br #bi 632 @(Zltb_elim_Type0 bi (nextblock m)) #Hnext 633 [ @(Zleb_elim_Type0 (low_bound m 〈br,bi〉) ofs) #Hlo 634 [ @(Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m 〈br,bi〉)) #Hhi 612 635 [ elim (dec_dividesZ (align_chunk chunk) ofs); #Hal 613 [ cases (pointer_compat_dec (block_ space m b) psp); #Hcl614 [ %1 % // ]636 [ cases (pointer_compat_dec (block_region m 〈br,bi〉) r); #Hcl 637 [ %1 % // @Hnext ] 615 638 ] 616 639 ] 617 640 ] 618 641 ] 619 %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) // ;642 %2 @nmk *; #Hval #Hlo' #Hhi' #Hal' #Hcl' @(absurd ???) // [ 2: @Hval  3: @Hnext ] 620 643 qed. 621 644 622 645 lemma in_bounds_true: 623 ∀m,chunk, psp,b,ofs. ∀A: Type[0]. ∀a1,a2: A.624 valid_access m chunk pspb ofs >625 (match in_bounds m chunk pspb ofs with646 ∀m,chunk,r,b,ofs. ∀A: Type[0]. ∀a1,a2: A. 647 valid_access m chunk r b ofs > 648 (match in_bounds m chunk r b ofs with 626 649 [ inl _ ⇒ a1  inr _ ⇒ a2 ]) = a1. 627 #m #chunk # psp#b #ofs #A #a1 #a2 #H628 cases (in_bounds m chunk pspb ofs);normalize;#H1650 #m #chunk #r #b #ofs #A #a1 #a2 #H 651 cases (in_bounds m chunk r b ofs);normalize;#H1 629 652 [// 630 653 elim (?:False); @(absurd ? H H1)] 631 654 qed. 632 655 633 (* [valid_pointer] holds if the given block address is valid and the 656 (* [valid_pointer] holds if the given block address is valid (and can be 657 represented in a pointer with the region [r]) and the 634 658 given offset falls within the bounds of the corresponding block. *) 635 659 636 660 definition valid_pointer : mem → region → block → Z → bool ≝ 637 λm, psp,b,ofs. Zltb b(nextblock m) ∧661 λm,r,b,ofs. Zltb (\snd b) (nextblock m) ∧ 638 662 Zleb (low_bound m b) ofs ∧ 639 663 Zltb ofs (high_bound m b) ∧ 640 is_pointer_compat (block_ space m b) psp.641 642 (* [load chunk m b ofs] perform a read in memory state [m], at address664 is_pointer_compat (block_region m b) r. 665 666 (* [load chunk m r b ofs] perform a read in memory state [m], at address 643 667 [b] and offset [ofs]. [None] is returned if the address is invalid 644 or the memory access is out of bounds. *) 668 or the memory access is out of bounds or the address cannot be represented 669 by a pointer with region [r]. *) 645 670 646 671 definition load : memory_chunk → mem → region → block → Z → option val ≝ 647 λchunk,m, psp,b,ofs.648 match in_bounds m chunk pspb ofs with672 λchunk,m,r,b,ofs. 673 match in_bounds m chunk r b ofs with 649 674 [ inl _ ⇒ Some ? (load_result chunk 650 675 (getN (pred_size_chunk chunk) ofs (contents (blocks m b)))) … … 652 677 653 678 lemma load_inv: 654 ∀chunk,m, psp,b,ofs,v.655 load chunk m pspb ofs = Some ? v →656 valid_access m chunk pspb ofs ∧679 ∀chunk,m,r,b,ofs,v. 680 load chunk m r b ofs = Some ? v → 681 valid_access m chunk r b ofs ∧ 657 682 v = load_result chunk 658 683 (getN (pred_size_chunk chunk) ofs (contents (blocks m b))). 659 #chunk #m # psp#b #ofs #v whd in ⊢ (??%? → ?);660 cases (in_bounds m chunk pspb ofs); #Haccess whd in ⊢ ((??%?) → ?); #H684 #chunk #m #r #b #ofs #v whd in ⊢ (??%? → ?); 685 cases (in_bounds m chunk r b ofs); #Haccess whd in ⊢ ((??%?) → ?); #H 661 686 [ % //; destruct; //; 662 687  destruct … … 669 694 let rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝ 670 695 match addr with 671 [ Vptr psp b ofs ⇒ load chunk m pspb (signed ofs)696 [ Vptr r b ofs ⇒ load chunk m r b (signed ofs) 672 697  _ ⇒ None ? ]. 673 698 … … 679 704 let c ≝ (blocks m b) in 680 705 mk_mem 681 (update ? b706 (update_block ? b 682 707 (mk_block_contents (low c) (high c) 683 (setN (pred_size_chunk chunk) ofs v (contents c)) (space c))708 (setN (pred_size_chunk chunk) ofs v (contents c))) 684 709 (blocks m)) 685 710 (nextblock m) 686 711 (nextblock_pos m). 687 712 688 (* [store chunk m b ofs v] perform a write in memory state [m].713 (* [store chunk m r b ofs v] perform a write in memory state [m]. 689 714 Value [v] is stored at address [b] and offset [ofs]. 690 715 Return the updated memory store, or [None] if the address is invalid 691 or the memory access is out of bounds. *) 716 or the memory access is out of bounds or the address cannot be represented 717 by a pointer with region [r]. *) 692 718 693 719 definition store : memory_chunk → mem → region → block → Z → val → option mem ≝ 694 λchunk,m, psp,b,ofs,v.695 match in_bounds m chunk pspb ofs with720 λchunk,m,r,b,ofs,v. 721 match in_bounds m chunk r b ofs with 696 722 [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v) 697 723  inr _ ⇒ None ? ]. 698 724 699 725 lemma store_inv: 700 ∀chunk,m, psp,b,ofs,v,m'.701 store chunk m pspb ofs v = Some ? m' →702 valid_access m chunk pspb ofs ∧726 ∀chunk,m,r,b,ofs,v,m'. 727 store chunk m r b ofs v = Some ? m' → 728 valid_access m chunk r b ofs ∧ 703 729 m' = unchecked_store chunk m b ofs v. 704 #chunk #m # psp#b #ofs #v #m' whd in ⊢ (??%? → ?);730 #chunk #m #r #b #ofs #v #m' whd in ⊢ (??%? → ?); 705 731 (*9*) 706 cases (in_bounds m chunk pspb ofs);#Hv whd in ⊢(??%? → ?);#Heq732 cases (in_bounds m chunk r b ofs);#Hv whd in ⊢(??%? → ?);#Heq 707 733 [% [//destruct;//] 708 734 destruct] … … 715 741 λchunk,m,addr,v. 716 742 match addr with 717 [ Vptr psp b ofs ⇒ store chunk m pspb (signed ofs) v743 [ Vptr r b ofs ⇒ store chunk m r b (signed ofs) v 718 744  _ ⇒ None ? ]. 719 745 … … 729 755 730 756 lemma valid_access_valid_block: 731 ∀m,chunk, psp,b,ofs. valid_access m chunk pspb ofs → valid_block m b.732 #m #chunk # psp#b #ofs #H757 ∀m,chunk,r,b,ofs. valid_access m chunk r b ofs → valid_block m b. 758 #m #chunk #r #b #ofs #H 733 759 elim H;//; 734 760 qed. 735 761 736 762 lemma valid_access_aligned: 737 ∀m,chunk, psp,b,ofs.738 valid_access m chunk pspb ofs → (align_chunk chunk ∣ ofs).739 #m #chunk # psp#b #ofs #H763 ∀m,chunk,r,b,ofs. 764 valid_access m chunk r b ofs → (align_chunk chunk ∣ ofs). 765 #m #chunk #r #b #ofs #H 740 766 elim H;//; 741 767 qed. 742 768 743 769 lemma valid_access_compat: 744 ∀m,chunk1,chunk2, psp,b,ofs.770 ∀m,chunk1,chunk2,r,b,ofs. 745 771 size_chunk chunk1 = size_chunk chunk2 → 746 valid_access m chunk1 pspb ofs →747 valid_access m chunk2 pspb ofs.748 #m #chunk #chunk2 # psp#b #ofs #H1 #H2772 valid_access m chunk1 r b ofs → 773 valid_access m chunk2 r b ofs. 774 #m #chunk #chunk2 #r #b #ofs #H1 #H2 749 775 elim H2;#H3 #H4 #H5 #H6 #H7 750 776 >H1 in H5 #H5 … … 758 784 759 785 theorem valid_access_load: 760 ∀m,chunk, psp,b,ofs.761 valid_access m chunk pspb ofs →762 ∃v. load chunk m pspb ofs = Some ? v.763 #m #chunk # psp#b #ofs #H %786 ∀m,chunk,r,b,ofs. 787 valid_access m chunk r b ofs → 788 ∃v. load chunk m r b ofs = Some ? v. 789 #m #chunk #r #b #ofs #H % 764 790 [2:whd in ⊢ (??%?);@in_bounds_true //; 765 791 skip] … … 767 793 768 794 theorem load_valid_access: 769 ∀m,chunk, psp,b,ofs,v.770 load chunk m pspb ofs = Some ? v →771 valid_access m chunk pspb ofs.772 #m #chunk # psp#b #ofs #v #H795 ∀m,chunk,r,b,ofs,v. 796 load chunk m r b ofs = Some ? v → 797 valid_access m chunk r b ofs. 798 #m #chunk #r #b #ofs #v #H 773 799 cases (load_inv … H);//; 774 800 qed. … … 779 805 780 806 lemma valid_access_store: 781 ∀m1,chunk, psp,b,ofs,v.782 valid_access m1 chunk pspb ofs →783 ∃m2. store chunk m1 pspb ofs v = Some ? m2.784 #m1 #chunk # psp#b #ofs #v #H807 ∀m1,chunk,r,b,ofs,v. 808 valid_access m1 chunk r b ofs → 809 ∃m2. store chunk m1 r b ofs v = Some ? m2. 810 #m1 #chunk #r #b #ofs #v #H 785 811 % 786 812 [2:@in_bounds_true // … … 791 817 792 818 lemma low_bound_store: 793 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →819 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 794 820 ∀b'.low_bound m2 b' = low_bound m1 b'. 795 #chunk #m1 # psp#b #ofs #v #m2 #STORE821 #chunk #m1 #r #b #ofs #v #m2 #STORE 796 822 #b' cases (store_inv … STORE) 797 823 #H1 #H2 >H2 798 824 whd in ⊢ (??(?%?)?) whd in ⊢ (??%?) 799 whd in ⊢ (??(?%)?) lapply (eqZb_to_Prop b' b)800 cases (eqZb b' b)normalize //825 whd in ⊢ (??(?%)?) @eq_block_elim #E 826 normalize // 801 827 qed. 802 828 803 829 lemma nextblock_store : 804 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →830 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 805 831 nextblock m2 = nextblock m1. 806 #chunk #m1 # psp#b #ofs #v #m2 #STORE832 #chunk #m1 #r #b #ofs #v #m2 #STORE 807 833 cases (store_inv … STORE); 808 834 #Hvalid #Heq … … 811 837 812 838 lemma high_bound_store: 813 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →839 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 814 840 ∀b'. high_bound m2 b' = high_bound m1 b'. 815 #chunk #m1 # psp#b #ofs #v #m2 #STORE841 #chunk #m1 #r #b #ofs #v #m2 #STORE 816 842 #b' cases (store_inv … STORE); 817 843 #Hvalid #H 818 844 >H 819 845 whd in ⊢ (??(?%?)?);whd in ⊢ (??%?); 820 whd in ⊢ (??(?%)?); lapply (eqZb_to_Prop b' b);821 cases (eqZb b' b);normalize;//;846 whd in ⊢ (??(?%)?); @eq_block_elim #E 847 normalize;//; 822 848 qed. 823 849 824 850 lemma region_store: 825 ∀chunk,m1,psp,b,ofs,v,m2.store chunk m1 psp b ofs v = Some ? m2 → 826 ∀b'. block_space m2 b' = block_space m1 b'. 827 #chunk #m1 #psp #b #ofs #v #m2 #STORE 828 #b' cases (store_inv … STORE); 829 #Hvalid #H 830 >H 831 whd in ⊢ (??(?%?)?);whd in ⊢ (??%?); 832 whd in ⊢ (??(?%)?);lapply (eqZb_to_Prop b' b); 833 cases (eqZb b' b);normalize;//; 851 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 852 ∀b'. block_region m2 b' = block_region m1 b'. 853 #chunk #m1 #r #b #ofs #v #m2 #STORE 854 * #r #b' // 834 855 qed. 835 856 836 857 lemma store_valid_block_1: 837 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →858 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 838 859 ∀b'. valid_block m1 b' → valid_block m2 b'. 839 #chunk #m1 # psp#b #ofs #v #m2 #STORE860 #chunk #m1 #r #b #ofs #v #m2 #STORE 840 861 #b' whd in ⊢ (% → %);#Hv 841 862 >(nextblock_store … STORE) //; … … 843 864 844 865 lemma store_valid_block_2: 845 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →866 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 846 867 ∀b'. valid_block m2 b' → valid_block m1 b'. 847 #chunk #m1 # psp#b #ofs #v #m2 #STORE868 #chunk #m1 #r #b #ofs #v #m2 #STORE 848 869 #b' whd in ⊢ (%→%); 849 870 >(nextblock_store … STORE) //; … … 853 874 854 875 lemma store_valid_access_1: 855 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →856 ∀chunk', psp',b',ofs'.857 valid_access m1 chunk' psp' b' ofs' → valid_access m2 chunk' psp' b' ofs'.858 #chunk #m1 # psp#b #ofs #v #m2 #STORE859 #chunk' # psp' #b' #ofs'876 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 877 ∀chunk',r',b',ofs'. 878 valid_access m1 chunk' r' b' ofs' → valid_access m2 chunk' r' b' ofs'. 879 #chunk #m1 #r #b #ofs #v #m2 #STORE 880 #chunk' #r' #b' #ofs' 860 881 * Hv; 861 882 #Hvb #Hl #Hr #Halign #Hptr … … 868 889 869 890 lemma store_valid_access_2: 870 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →871 ∀chunk', psp',b',ofs'.872 valid_access m2 chunk' psp' b' ofs' → valid_access m1 chunk' psp' b' ofs'.873 #chunk #m1 # psp#b #ofs #v #m2 #STORE874 #chunk' # psp' #b' #ofs'891 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 892 ∀chunk',r',b',ofs'. 893 valid_access m2 chunk' r' b' ofs' → valid_access m1 chunk' r' b' ofs'. 894 #chunk #m1 #r #b #ofs #v #m2 #STORE 895 #chunk' #r' #b' #ofs' 875 896 * Hv; 876 897 #Hvb #Hl #Hr #Halign #Hcompat … … 883 904 884 905 lemma store_valid_access_3: 885 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →886 valid_access m1 chunk pspb ofs.887 #chunk #m1 # psp#b #ofs #v #m2 #STORE906 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 907 valid_access m1 chunk r b ofs. 908 #chunk #m1 #r #b #ofs #v #m2 #STORE 888 909 cases (store_inv … STORE);//; 889 910 qed. … … 893 914 894 915 lemma load_compat_pointer: 895 ∀chunk,m, psp,psp',b,ofs,v.896 pointer_compat (block_ space m b) psp' →897 load chunk m pspb ofs = Some ? v →898 load chunk m psp' b ofs = Some ? v.899 #chunk #m # psp #psp' #b #ofs #v #Hcompat #LOAD916 ∀chunk,m,r,r',b,ofs,v. 917 pointer_compat (block_region m b) r' → 918 load chunk m r b ofs = Some ? v → 919 load chunk m r' b ofs = Some ? v. 920 #chunk #m #r #r' #b #ofs #v #Hcompat #LOAD 900 921 lapply (load_valid_access … LOAD); #Hvalid 901 cut (valid_access m chunk psp' b ofs);922 cut (valid_access m chunk r' b ofs); 902 923 [ % elim Hvalid; //; 903 924  #Hvalid' … … 910 931 (* Nonessential properties that may require arithmetic 911 932 theorem load_store_similar: 912 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →933 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 913 934 ∀chunk'. 914 935 size_chunk chunk' = size_chunk chunk → 915 load chunk' m2 pspb ofs = Some ? (load_result chunk' v).916 #chunk #m1 # psp#b #ofs #v #m2 #STORE936 load chunk' m2 r b ofs = Some ? (load_result chunk' v). 937 #chunk #m1 #r #b #ofs #v #m2 #STORE 917 938 #chunk' #Hsize cases (store_inv … STORE); 918 939 #Hv #Heq 919 940 whd in ⊢ (??%?); 920 nrewrite > (in_bounds_true m2 chunk' pspb ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))941 nrewrite > (in_bounds_true m2 chunk' r b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b))))) 921 942 (None ?) ?); 922 943 [>Heq … … 934 955 935 956 theorem load_store_same: 936 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →937 load chunk m2 pspb ofs = Some ? (load_result chunk v).938 #chunk #m1 # psp#b #ofs #v #m2 #STORE957 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 958 load chunk m2 r b ofs = Some ? (load_result chunk v). 959 #chunk #m1 #r #b #ofs #v #m2 #STORE 939 960 @load_store_similar //; 940 961 qed. 941 962 942 963 theorem load_store_other: 943 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →944 ∀chunk', psp',b',ofs'.964 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 965 ∀chunk',r',b',ofs'. 945 966 b' ≠ b 946 967 ∨ ofs' + size_chunk chunk' ≤ ofs 947 968 ∨ ofs + size_chunk chunk ≤ ofs' → 948 load chunk' m2 psp' b' ofs' = load chunk' m1 psp' b' ofs'.949 #chunk #m1 # psp#b #ofs #v #m2 #STORE950 #chunk' # psp' #b' #ofs' #H969 load chunk' m2 r' b' ofs' = load chunk' m1 r' b' ofs'. 970 #chunk #m1 #r #b #ofs #v #m2 #STORE 971 #chunk' #r' #b' #ofs' #H 951 972 cases (store_inv … STORE); 952 973 #Hvalid #Heq whd in ⊢ (??%%); 953 cases (in_bounds m1 chunk' psp' b' ofs');954 [#Hvalid1 >(in_bounds_true m2 chunk' psp' b' ofs' ? (Some ? ?) ??)974 cases (in_bounds m1 chunk' r' b' ofs'); 975 [#Hvalid1 >(in_bounds_true m2 chunk' r' b' ofs' ? (Some ? ?) ??) 955 976 [whd in ⊢ (???%); @(eq_f … (Some val)) @(eq_f … (load_result chunk')) 956 977 >Heq whd in ⊢ (??(???(? (? % ?)))?); … … 968 989 #Hneq @ ] 969 990 @(store_valid_access_1 … STORE) //] 970 whd in ⊢ (? → ???%);lapply (in_bounds m2 chunk' psp' b' ofs');991 whd in ⊢ (? → ???%);lapply (in_bounds m2 chunk' r' b' ofs'); 971 992 #H1 cases H1; 972 993 [#H2 #H3 lapply (store_valid_access_2 … STORE … H2);#Hfalse … … 978 999 979 1000 theorem load_store_overlap: 980 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →981 ∀chunk',ofs',v'. load chunk' m2 pspb ofs' = Some ? v' →1001 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 1002 ∀chunk',ofs',v'. load chunk' m2 r b ofs' = Some ? v' → 982 1003 ofs' ≠ ofs → 983 1004 ofs < ofs' + size_chunk chunk' → 984 1005 ofs' < ofs + size_chunk chunk → 985 1006 v' = Vundef. 986 #chunk #m1 # psp#b #ofs #v #m2 #STORE1007 #chunk #m1 #r #b #ofs #v #m2 #STORE 987 1008 #chunk' #ofs' #v' #H 988 1009 #H1 #H2 #H3 … … 1000 1021 1001 1022 theorem load_store_overlap': 1002 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →1023 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 1003 1024 ∀chunk',ofs'. 1004 valid_access m1 chunk' pspb ofs' →1025 valid_access m1 chunk' r b ofs' → 1005 1026 ofs' ≠ ofs → 1006 1027 ofs < ofs' + size_chunk chunk' → 1007 1028 ofs' < ofs + size_chunk chunk → 1008 load chunk' m2 pspb ofs' = Some ? Vundef.1009 #chunk #m1 # psp#b #ofs #v #m2 #STORE1029 load chunk' m2 r b ofs' = Some ? Vundef. 1030 #chunk #m1 #r #b #ofs #v #m2 #STORE 1010 1031 #chunk' #ofs' #Hvalid #H #H1 #H2 1011 cut (∃v'.load chunk' m2 pspb ofs' = Some ? v')1032 cut (∃v'.load chunk' m2 r b ofs' = Some ? v') 1012 1033 [@valid_access_load 1013 1034 @(store_valid_access_1 … STORE) // … … 1018 1039 1019 1040 theorem load_store_mismatch: 1020 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →1041 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 1021 1042 ∀chunk',v'. 1022 load chunk' m2 pspb ofs = Some ? v' →1043 load chunk' m2 r b ofs = Some ? v' → 1023 1044 size_chunk chunk' ≠ size_chunk chunk → 1024 1045 v' = Vundef. 1025 #chunk #m1 # psp#b #ofs #v #m2 #STORE1046 #chunk #m1 #r #b #ofs #v #m2 #STORE 1026 1047 #chunk' #v' #H #H1 1027 1048 cases (store_inv … STORE); … … 1039 1060 1040 1061 theorem load_store_mismatch': 1041 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →1062 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 1042 1063 ∀chunk'. 1043 valid_access m1 chunk' pspb ofs →1064 valid_access m1 chunk' r b ofs → 1044 1065 size_chunk chunk' ≠ size_chunk chunk → 1045 load chunk' m2 pspb ofs = Some ? Vundef.1046 #chunk #m1 # psp#b #ofs #v #m2 #STORE1066 load chunk' m2 r b ofs = Some ? Vundef. 1067 #chunk #m1 #r #b #ofs #v #m2 #STORE 1047 1068 #chunk' #Hvalid #Hsize 1048 cut (∃v'.load chunk' m2 pspb ofs = Some ? v')1069 cut (∃v'.load chunk' m2 r b ofs = Some ? v') 1049 1070 [@(valid_access_load …) 1050 1071 napply … … 1101 1122 1102 1123 theorem load_store_characterization: 1103 ∀chunk,m1, psp,b,ofs,v,m2.store chunk m1 pspb ofs v = Some ? m2 →1104 ∀chunk', psp',b',ofs'.1105 valid_access m1 chunk' psp' b' ofs' →1106 load chunk' m2 psp' b' ofs' =1124 ∀chunk,m1,r,b,ofs,v,m2.store chunk m1 r b ofs v = Some ? m2 → 1125 ∀chunk',r',b',ofs'. 1126 valid_access m1 chunk' r' b' ofs' → 1127 load chunk' m2 r' b' ofs' = 1107 1128 match load_store_classification chunk b ofs chunk' b' ofs' with 1108 1129 [ lsc_similar _ _ _ ⇒ Some ? (load_result chunk' v) 1109  lsc_other _ ⇒ load chunk' m1 psp' b' ofs'1130  lsc_other _ ⇒ load chunk' m1 r' b' ofs' 1110 1131  lsc_overlap _ _ _ _ ⇒ Some ? Vundef 1111 1132  lsc_mismatch _ _ _ ⇒ Some ? Vundef ]. 1112 #chunk #m1 # psp#b #ofs #v #m2 #STORE1113 #chunk' # psp' #b' #ofs' #Hvalid1114 cut (∃v'. load chunk' m2 psp' b' ofs' = Some ? v')1133 #chunk #m1 #r #b #ofs #v #m2 #STORE 1134 #chunk' #r' #b' #ofs' #Hvalid 1135 cut (∃v'. load chunk' m2 r' b' ofs' = Some ? v') 1115 1136 [@valid_access_load 1116 1137 @(store_valid_access_1 … STORE … Hvalid) … … 1118 1139 cases (load_store_classification chunk b ofs chunk' b' ofs') 1119 1140 [#H1 #H2 #H3 whd in ⊢ (???%);<H1 <H2 1120 @(load_compat_pointer … psp)1141 @(load_compat_pointer … r) 1121 1142 [ >(region_store … STORE b) 1122 1143 cases Hvalid; //; … … 1129 1150 #H2 % %{2} //] 1130 1151 #H2 %{2} //] 1131 #H1 #H2 #H3 #H4 lapply (load_compat_pointer … psp… Hx);1152 #H1 #H2 #H3 #H4 lapply (load_compat_pointer … r … Hx); 1132 1153 [ >(region_store … STORE b') 1133 1154 >H1 elim (store_valid_access_3 … STORE); // … … 1137 1158 ] 1138 1159 #H1 #H2 #H3 1139 lapply (load_compat_pointer … psp… Hx);1160 lapply (load_compat_pointer … r … Hx); 1140 1161 [ >(region_store … STORE b') 1141 1162 >H1 elim (store_valid_access_3 … STORE); // … … 1298 1319 lemma class_alloc: 1299 1320 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1300 ∀b'.block_ space m2 b' = if eqZb b' b then bcl else block_spacem1 b'.1321 ∀b'.block_region m2 b' = if eqZb b' b then bcl else block_region m1 b'. 1301 1322 #m1 #lo #hi #bcl #m2 #b #ALLOC 1302 1323 whd in ALLOC:(??%%); destruct; #b' … … 1306 1327 lemma class_alloc_same: 1307 1328 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1308 block_ spacem2 b = bcl.1329 block_region m2 b = bcl. 1309 1330 #m1 #lo #hi #bcl #m2 #b #ALLOC 1310 1331 whd in ALLOC:(??%%); destruct; … … 1314 1335 lemma class_alloc_other: 1315 1336 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1316 ∀b'. valid_block m1 b' → block_ space m2 b' = block_spacem1 b'.1337 ∀b'. valid_block m1 b' → block_region m2 b' = block_region m1 b'. 1317 1338 #m1 #lo #hi #bcl #m2 #b #ALLOC 1318 1339 #b' >(class_alloc … ALLOC b') … … 1325 1346 lemma valid_access_alloc_other: 1326 1347 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1327 ∀chunk, psp,b',ofs.1328 valid_access m1 chunk pspb' ofs →1329 valid_access m2 chunk pspb' ofs.1348 ∀chunk,r,b',ofs. 1349 valid_access m1 chunk r b' ofs → 1350 valid_access m2 chunk r b' ofs. 1330 1351 #m1 #lo #hi #bcl #m2 #b #ALLOC 1331 #chunk # psp#b' #ofs #H1352 #chunk #r #b' #ofs #H 1332 1353 cases H; #Hvalid #Hlow #Hhigh #Halign #Hcompat 1333 1354 % … … 1341 1362 lemma valid_access_alloc_same: 1342 1363 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1343 ∀chunk, psp,ofs.1364 ∀chunk,r,ofs. 1344 1365 lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) → 1345 pointer_compat bcl psp→1346 valid_access m2 chunk pspb ofs.1366 pointer_compat bcl r → 1367 valid_access m2 chunk r b ofs. 1347 1368 #m1 #lo #hi #bcl #m2 #b #ALLOC 1348 #chunk # psp#ofs #Hlo #Hhi #Halign #Hcompat1369 #chunk #r #ofs #Hlo #Hhi #Halign #Hcompat 1349 1370 % 1350 1371 [ napply (valid_new_block … ALLOC) … … 1361 1382 lemma valid_access_alloc_inv: 1362 1383 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1363 ∀chunk, psp,b',ofs.1364 valid_access m2 chunk pspb' ofs →1365 valid_access m1 chunk pspb' ofs ∨1366 (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl psp)).1384 ∀chunk,r,b',ofs. 1385 valid_access m2 chunk r b' ofs → 1386 valid_access m1 chunk r b' ofs ∨ 1387 (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ pointer_compat bcl r)). 1367 1388 #m1 #lo #hi #bcl #m2 #b #ALLOC 1368 #chunk # psp#b' #ofs *;#Hblk #Hlo #Hhi #Hal #Hct1389 #chunk #r #b' #ofs *;#Hblk #Hlo #Hhi #Hal #Hct 1369 1390 elim (valid_block_alloc_inv … ALLOC ? Hblk);#H 1370 1391 [ <H in ALLOC ⊢ % #ALLOC' … … 1382 1403 theorem load_alloc_unchanged: 1383 1404 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 → 1384 ∀chunk, psp,b',ofs.1405 ∀chunk,r,b',ofs. 1385 1406 valid_block m1 b' → 1386 load chunk m2 psp b' ofs = load chunk m1 pspb' ofs.1407 load chunk m2 r b' ofs = load chunk m1 r b' ofs. 1387 1408 #m1 #lo #hi #bcl #m2 #b #ALLOC 1388 #chunk # psp#b' #ofs #H whd in ⊢ (??%%);1389 cases (in_bounds m2 chunk pspb' ofs); #H'1409 #chunk #r #b' #ofs #H whd in ⊢ (??%%); 1410 cases (in_bounds m2 chunk r b' ofs); #H' 1390 1411 [ elim (valid_access_alloc_inv … ALLOC ???? H'); 1391 1412 [ #H'' (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error … … 1400 1421 @False_ind @(absurd ? H) napply (fresh_block_alloc … ALLOC) 1401 1422 ] 1402  cases (in_bounds m1 chunk pspb' ofs); #H'' whd in ⊢ (??%%); //;1423  cases (in_bounds m1 chunk r b' ofs); #H'' whd in ⊢ (??%%); //; 1403 1424 @False_ind @(absurd ? ? H') @(valid_access_alloc_other … ALLOC) // 1404 1425 ] qed. … … 1406 1427 theorem load_alloc_other: 1407 1428 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1408 ∀chunk, psp,b',ofs,v.1409 load chunk m1 pspb' ofs = Some ? v →1410 load chunk m2 pspb' ofs = Some ? v.1429 ∀chunk,r,b',ofs,v. 1430 load chunk m1 r b' ofs = Some ? v → 1431 load chunk m2 r b' ofs = Some ? v. 1411 1432 #m1 #lo #hi #bcl #m2 #b #ALLOC 1412 #chunk # psp#b' #ofs #v #H1433 #chunk #r #b' #ofs #v #H 1413 1434 <H @(load_alloc_unchanged … ALLOC ???) cases (load_valid_access … H); //; 1414 1435 qed. … … 1416 1437 theorem load_alloc_same: 1417 1438 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1418 ∀chunk, psp,ofs,v.1419 load chunk m2 pspb ofs = Some ? v →1439 ∀chunk,r,ofs,v. 1440 load chunk m2 r b ofs = Some ? v → 1420 1441 v = Vundef. 1421 1442 #m1 #lo #hi #bcl #m2 #b #ALLOC 1422 #chunk # psp#ofs #v #H1443 #chunk #r #ofs #v #H 1423 1444 elim (load_inv … H); #H0 #H1 >H1 1424 1445 whd in ALLOC:(??%%); (* XXX destruct; ??? *) @(pairdisc_elim … ALLOC) … … 1431 1452 theorem load_alloc_same': 1432 1453 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1433 ∀chunk, psp,ofs.1454 ∀chunk,r,ofs. 1434 1455 lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) → 1435 pointer_compat bcl psp→1436 load chunk m2 pspb ofs = Some ? Vundef.1456 pointer_compat bcl r → 1457 load chunk m2 r b ofs = Some ? Vundef. 1437 1458 #m1 #lo #hi #bcl #m2 #b #ALLOC 1438 #chunk # psp#ofs #Hlo #Hhi #Hal #Hct1439 cut (∃v. load chunk m2 pspb ofs = Some ? v);1459 #chunk #r #ofs #Hlo #Hhi #Hal #Hct 1460 cut (∃v. load chunk m2 r b ofs = Some ? v); 1440 1461 [ @valid_access_load % //; 1441 1462 [ @(valid_new_block … ALLOC) … … 1504 1525 1505 1526 lemma class_free: 1506 ∀m,bf,b. b ≠ bf → block_ space (free m bf) b = block_spacem b.1527 ∀m,bf,b. b ≠ bf → block_region (free m bf) b = block_region m b. 1507 1528 #m #bf #b #H whd in ⊢ (??%%); whd in ⊢ (??(?(?%?))?); 1508 1529 >(update_o block_contents …) //; @sym_neq //; … … 1510 1531 1511 1532 lemma valid_access_free_1: 1512 ∀m,bf,chunk, psp,b,ofs.1513 valid_access m chunk pspb ofs → b ≠ bf →1514 valid_access (free m bf) chunk pspb ofs.1515 #m #bf #chunk # psp#b #ofs *;#Hval #Hlo #Hhi #Hal #Hcompat #Hneq1533 ∀m,bf,chunk,r,b,ofs. 1534 valid_access m chunk r b ofs → b ≠ bf → 1535 valid_access (free m bf) chunk r b ofs. 1536 #m #bf #chunk #r #b #ofs *;#Hval #Hlo #Hhi #Hal #Hcompat #Hneq 1516 1537 % //; 1517 1538 [ @valid_block_free_1 // … … 1522 1543 1523 1544 lemma valid_access_free_2: 1524 ∀m, psp,bf,chunk,ofs. ¬(valid_access (free m bf) chunk pspbf ofs).1525 #m # psp#bf #chunk #ofs @nmk *; #Hval #Hlo #Hhi #Hal #Hct1545 ∀m,r,bf,chunk,ofs. ¬(valid_access (free m bf) chunk r bf ofs). 1546 #m #r #bf #chunk #ofs @nmk *; #Hval #Hlo #Hhi #Hal #Hct 1526 1547 whd in Hlo:(?%?);whd in Hlo:(?(?(?%?))?); >(update_s block_contents …) in Hlo 1527 1548 whd in Hhi:(??%);whd in Hhi:(??(?(?%?))); >(update_s block_contents …) in Hhi … … 1534 1555 1535 1556 lemma valid_access_free_inv: 1536 ∀m,bf,chunk, psp,b,ofs.1537 valid_access (free m bf) chunk pspb ofs →1538 valid_access m chunk pspb ofs ∧ b ≠ bf.1539 #m #bf #chunk # psp#b #ofs elim (decidable_eq_Z_Type b bf);1557 ∀m,bf,chunk,r,b,ofs. 1558 valid_access (free m bf) chunk r b ofs → 1559 valid_access m chunk r b ofs ∧ b ≠ bf. 1560 #m #bf #chunk #r #b #ofs elim (decidable_eq_Z_Type b bf); 1540 1561 [ #e >e 1541 1562 #H @False_ind @(absurd ? H (valid_access_free_2 …)) … … 1548 1569 1549 1570 theorem load_free: 1550 ∀m,bf,chunk, psp,b,ofs.1571 ∀m,bf,chunk,r,b,ofs. 1551 1572 b ≠ bf → 1552 load chunk (free m bf) psp b ofs = load chunk m pspb ofs.1553 #m #bf #chunk # psp#b #ofs #ne whd in ⊢ (??%%);1554 elim (in_bounds m chunk pspb ofs);1573 load chunk (free m bf) r b ofs = load chunk m r b ofs. 1574 #m #bf #chunk #r #b #ofs #ne whd in ⊢ (??%%); 1575 elim (in_bounds m chunk r b ofs); 1555 1576 [ #Hval whd in ⊢ (???%); >(in_bounds_true ????? (option val) ???) 1556 1577 [ whd in ⊢ (??(??(??(???(?(?%?)))))?); >(update_o block_contents …) //; … … 1558 1579  @valid_access_free_1 //; @ne 1559 1580 ] 1560  elim (in_bounds (free m bf) chunk pspb ofs); (* XXX just // used to work *) [ 2: normalize; //; ]1581  elim (in_bounds (free m bf) chunk r b ofs); (* XXX just // used to work *) [ 2: normalize; //; ] 1561 1582 #H #H' @False_ind @(absurd ? ? H') 1562 1583 elim (valid_access_free_inv …H); //; … … 1586 1607 1587 1608 lemma valid_access_free_list: 1588 ∀chunk, psp,b,ofs,m,bl.1589 valid_access m chunk pspb ofs → ¬in_list ? b bl →1590 valid_access (free_list m bl) chunk pspb ofs.1591 #chunk # psp#b #ofs #m #bl elim bl;1609 ∀chunk,r,b,ofs,m,bl. 1610 valid_access m chunk r b ofs → ¬in_list ? b bl → 1611 valid_access (free_list m bl) chunk r b ofs. 1612 #chunk #r #b #ofs #m #bl elim bl; 1592 1613 [ whd in ⊢ (?→?→(?%????)); // 1593 1614  #h #t #IH #H #notin >(unfold_free_list m h t) @valid_access_free_1 … … 1597 1618 1598 1619 lemma valid_access_free_list_inv: 1599 ∀chunk, psp,b,ofs,m,bl.1600 valid_access (free_list m bl) chunk pspb ofs →1601 ¬in_list ? b bl ∧ valid_access m chunk pspb ofs.1602 #chunk # psp#b #ofs #m #bl elim bl;1620 ∀chunk,r,b,ofs,m,bl. 1621 valid_access (free_list m bl) chunk r b ofs → 1622 ¬in_list ? b bl ∧ valid_access m chunk r b ofs. 1623 #chunk #r #b #ofs #m #bl elim bl; 1603 1624 [ whd in ⊢ ((?%????)→?); #H % // 1604 1625  #h #t #IH >(unfold_free_list m h t) #H … … 1612 1633 1613 1634 lemma valid_pointer_valid_access: 1614 ∀m, psp,b,ofs.1615 valid_pointer m psp b ofs = true ↔ valid_access m Mint8unsigned pspb ofs.1616 #m # psp#b #ofs whd in ⊢ (?(??%?)?); %1635 ∀m,r,b,ofs. 1636 valid_pointer m r b ofs = true ↔ valid_access m Mint8unsigned r b ofs. 1637 #m #r #b #ofs whd in ⊢ (?(??%?)?); % 1617 1638 [ #H 1618 1639 lapply (andb_true_l … H); #H' … … 1627 1648  whd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon 1628 1649  cases ofs; /2/; 1629  whd in H4:(??%?); elim (pointer_compat_dec (block_ space m b) psp) in H4;1650  whd in H4:(??%?); elim (pointer_compat_dec (block_region m b) r) in H4; 1630 1651 [ //;  #Hn #e whd in e:(??%%); destruct ] 1631 1652 ] … … 1634 1655 >(Zle_to_Zleb_true … Hlo) 1635 1656 whd in Hhi:(?(??%)?); >(Zlt_to_Zltb_true … ?) 1636 [ whd in ⊢ (??%?); elim (pointer_compat_dec (block_ space m b) psp);1657 [ whd in ⊢ (??%?); elim (pointer_compat_dec (block_region m b) r); 1637 1658 [ //; 1638 1659  #Hct' @False_ind @(absurd … Hct Hct') … … 1644 1665 1645 1666 theorem valid_pointer_alloc: 1646 ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl, psp. ∀b,b': block. ∀ofs: Z.1667 ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,r. ∀b,b': block. ∀ofs: Z. 1647 1668 alloc m1 lo hi bcl = 〈m2, b'〉 → 1648 valid_pointer m1 pspb ofs = true →1649 valid_pointer m2 pspb ofs = true.1650 #m1 #m2 #lo #hi #bcl # psp#b #b' #ofs #ALLOC #VALID1669 valid_pointer m1 r b ofs = true → 1670 valid_pointer m2 r b ofs = true. 1671 #m1 #m2 #lo #hi #bcl #r #b #b' #ofs #ALLOC #VALID 1651 1672 lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval 1652 1673 @(proj2 ?? (valid_pointer_valid_access ????)) … … 1656 1677 theorem valid_pointer_store: 1657 1678 ∀chunk: memory_chunk. ∀m1,m2: mem. 1658 ∀ psp,psp': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val.1659 store chunk m1 psp' b' ofs' v = Some ? m2 →1660 valid_pointer m1 psp b ofs = true → valid_pointer m2 pspb ofs = true.1661 #chunk #m1 #m2 # psp #psp' #b #b' #ofs #ofs' #v #STORE #VALID1679 ∀r,r': region. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val. 1680 store chunk m1 r' b' ofs' v = Some ? m2 → 1681 valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true. 1682 #chunk #m1 #m2 #r #r' #b #b' #ofs #ofs' #v #STORE #VALID 1662 1683 lapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval 1663 1684 @(proj2 ?? (valid_pointer_valid_access ????)) … … 1715 1736 (* 1716 1737 lemma store_unmapped_inj: ∀val_inj. 1717 ∀mi,m1,m2, psp,b,ofs,v,chunk,m1'.1738 ∀mi,m1,m2,r,b,ofs,v,chunk,m1'. 1718 1739 mem_inj val_inj mi m1 m2 → 1719 1740 mi b = None ? → 1720 store chunk m1 pspb ofs v = Some ? m1' →1741 store chunk m1 r b ofs v = Some ? m1' → 1721 1742 mem_inj val_inj mi m1' m2. 1722 1743 #val_inj 1723 #mi #m1 #m2 # psp#b #ofs #v #chunk #m1' #Hinj #Hmi #Hstore1744 #mi #m1 #m2 #r #b #ofs #v #chunk #m1' #Hinj #Hmi #Hstore 1724 1745 whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload 1725 1746 cut (load chunk0 m1 b1 ofs0 = Some ? v1); … … 1730 1751 1731 1752 lemma store_outside_inj: ∀val_inj. 1732 ∀mi,m1,m2,chunk, psp,b,ofs,v,m2'.1753 ∀mi,m1,m2,chunk,r,b,ofs,v,m2'. 1733 1754 mem_inj val_inj mi m1 m2 → 1734 1755 (∀b',delta. … … 1736 1757 high_bound m1 b' + delta ≤ ofs 1737 1758 ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) → 1738 store chunk m2 pspb ofs v = Some ? m2' →1759 store chunk m2 r b ofs v = Some ? m2' → 1739 1760 mem_inj val_inj mi m1 m2'. 1740 1761 #val_inj 1741 #mi #m1 #m2 #chunk # psp#b #ofs #v #m2' #Hinj #Hbounds #Hstore1762 #mi #m1 #m2 #chunk #r #b #ofs #v #m2' #Hinj #Hbounds #Hstore 1742 1763 whd; #chunk0 #b1 #ofs0 #v1 #b2 #delta #Hmi0 #Hload 1743 1764 lapply (Hinj … Hmi0 Hload);*;#v2 *;#LOAD2 #VINJ … … 2112 2133 ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val. 2113 2134 extends m1 m2 → 2114 load chunk m1 pspb ofs = Some ? v →2115 load chunk m2 pspb ofs = Some ? v.2116 #chunk #m1 #m2 # psp#b #ofs #v2135 load chunk m1 r b ofs = Some ? v → 2136 load chunk m2 r b ofs = Some ? v. 2137 #chunk #m1 #m2 #r #b #ofs #v 2117 2138 *;#Hnext #Hinj #LOAD 2118 2139 lapply (Hinj … LOAD); [ normalize; //  2,3: ] … … 2124 2145 ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val. 2125 2146 extends m1 m2 → 2126 store chunk m1 pspb ofs v = Some ? m1' →2127 ∃m2'. store chunk m2 pspb ofs v = Some ? m2' ∧ extends m1' m2'.2147 store chunk m1 r b ofs v = Some ? m1' → 2148 ∃m2'. store chunk m2 r b ofs v = Some ? m2' ∧ extends m1' m2'. 2128 2149 #chunk #m1 #m2 #m1' #b #ofs #v *;#Hnext #Hinj #STORE1 2129 2150 lapply (store_mapped_inj … Hinj ?? STORE1 ?); … … 2147 2168 extends m1 m2 → 2148 2169 ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs → 2149 store chunk m2 pspb ofs v = Some ? m2' →2170 store chunk m2 r b ofs v = Some ? m2' → 2150 2171 extends m1 m2'. 2151 2172 #chunk #m1 #m2 #m2' #b #ofs #v *;#Hnext #Hinj #Houtside #STORE % … … 2161 2182 theorem valid_pointer_extends: 2162 2183 ∀m1,m2,b,ofs. 2163 extends m1 m2 → valid_pointer m1 pspb ofs = true →2164 valid_pointer m2 pspb ofs = true.2184 extends m1 m2 → valid_pointer m1 r b ofs = true → 2185 valid_pointer m2 r b ofs = true. 2165 2186 #m1 #m2 #b #ofs *;#Hnext #Hinj #VALID 2166 2187 <(Zplus_z_OZ ofs) … … 2192 2213 lemma load_lessdef: 2193 2214 ∀m1,m2,chunk,b,ofs,v1. 2194 lessdef m1 m2 → load chunk m1 pspb ofs = Some ? v1 →2195 ∃v2. load chunk m2 pspb ofs = Some ? v2 ∧ Val_lessdef v1 v2.2215 lessdef m1 m2 → load chunk m1 r b ofs = Some ? v1 → 2216 ∃v2. load chunk m2 r b ofs = Some ? v2 ∧ Val_lessdef v1 v2. 2196 2217 #m1 #m2 #chunk #b #ofs #v1 *;#Hnext #Hinj #LOAD0 2197 2218 lapply (Hinj … LOAD0); [ whd in ⊢ (??%?); //  2,3:##skip ] … … 2217 2238 ∀m1,m2,chunk,b,ofs,v1,v2,m1'. 2218 2239 lessdef m1 m2 → Val_lessdef v1 v2 → 2219 store chunk m1 pspb ofs v1 = Some ? m1' →2220 ∃m2'. store chunk m2 pspb ofs v2 = Some ? m2' ∧ lessdef m1' m2'.2240 store chunk m1 r b ofs v1 = Some ? m1' → 2241 ∃m2'. store chunk m2 r b ofs v2 = Some ? m2' ∧ lessdef m1' m2'. 2221 2242 #m1 #m2 #chunk #b #ofs #v1 #v2 #m1' 2222 2243 *;#Hnext #Hinj #Hvless #STORE0 … … 2309 2330 lemma valid_pointer_lessdef: 2310 2331 ∀m1,m2,b,ofs. 2311 lessdef m1 m2 → valid_pointer m1 psp b ofs = true → valid_pointer m2 pspb ofs = true.2332 lessdef m1 m2 → valid_pointer m1 r b ofs = true → valid_pointer m2 r b ofs = true. 2312 2333 #m1 #m2 #b #ofs *;#Hnext #Hinj #VALID 2313 2334 <(Zplus_z_OZ ofs) @(valid_pointer_inj … Hinj VALID) //; … … 2446 2467 mem_inject f m1 m2 → 2447 2468 valid_pointer m1 b (signed ofs) = true → 2448 val_inject f (Vptr pspb ofs) (Vptr b' ofs') →2469 val_inject f (Vptr r b ofs) (Vptr b' ofs') → 2449 2470 valid_pointer m2 b' (signed ofs') = true. 2450 2471 #f #m1 #m2 #b #ofs #b' #ofs' … … 3494 3515 3495 3516 lemma in_bounds_equiv: 3496 ∀chunk1,chunk2,m, psp,b,ofs.∀A:Type[0].∀a1,a2: A.3517 ∀chunk1,chunk2,m,r,b,ofs.∀A:Type[0].∀a1,a2: A. 3497 3518 size_chunk chunk1 = size_chunk chunk2 → 3498 (match in_bounds m chunk1 pspb ofs with [ inl _ ⇒ a1  inr _ ⇒ a2]) =3499 (match in_bounds m chunk2 pspb ofs with [ inl _ ⇒ a1  inr _ ⇒ a2]).3500 #chunk1 #chunk2 #m # psp#b #ofs #A #a1 #a2 #Hsize3501 elim (in_bounds m chunk1 pspb ofs);3519 (match in_bounds m chunk1 r b ofs with [ inl _ ⇒ a1  inr _ ⇒ a2]) = 3520 (match in_bounds m chunk2 r b ofs with [ inl _ ⇒ a1  inr _ ⇒ a2]). 3521 #chunk1 #chunk2 #m #r #b #ofs #A #a1 #a2 #Hsize 3522 elim (in_bounds m chunk1 r b ofs); 3502 3523 [ #H whd in ⊢ (??%?); >(in_bounds_true … A a1 a2 ?) //; 3503 3524 @valid_access_compat //; 3504  #H whd in ⊢ (??%?); elim (in_bounds m chunk2 pspb ofs); //;3525  #H whd in ⊢ (??%?); elim (in_bounds m chunk2 r b ofs); //; 3505 3526 #H' @False_ind @(absurd ?? H) 3506 3527 @valid_access_compat //; … … 3511 3532 storev Mint8signed m a v = storev Mint8unsigned m a v. 3512 3533 #m #a #v whd in ⊢ (??%%); elim a; //; 3513 # psp#b #ofs whd in ⊢ (??%%);3534 #r #b #ofs whd in ⊢ (??%%); 3514 3535 >(in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???) //; 3515 3536 qed. … … 3519 3540 storev Mint16signed m a v = storev Mint16unsigned m a v. 3520 3541 #m #a #v whd in ⊢ (??%%); elim a; //; 3521 # psp#b #ofs whd in ⊢ (??%%);3542 #r #b #ofs whd in ⊢ (??%%); 3522 3543 >(in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???) //; 3523 3544 qed. … … 3533 3554 loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a). 3534 3555 #m #a whd in ⊢ (??%(????(%))); elim a; //; 3535 # psp#b #ofs whd in ⊢ (??%(????%));3556 #r #b #ofs whd in ⊢ (??%(????%)); 3536 3557 >(in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???) //; 3537 elim (in_bounds m Mint8unsigned pspb (signed ofs)); /2/;3558 elim (in_bounds m Mint8unsigned r b (signed ofs)); /2/; 3538 3559 #H whd in ⊢ (??%%); 3539 3560 elim (getN 0 (signed ofs) (contents (blocks m b)));
Note: See TracChangeset
for help on using the changeset viewer.