Changeset 124 for Csemantics/Mem.ma
 Timestamp:
 Sep 24, 2010, 10:31:32 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Csemantics/Mem.ma
r24 r124 83 83 plus a mapping from byte offsets to contents. *) 84 84 85 ninductive block_class : Type ≝ 86  UnspecifiedB : block_class 87  DataB : block_class 88  IDataB : block_class 89  XDataB : block_class 90  CodeB : block_class. 91 85 92 (* XXX: mkblock *) 86 93 nrecord block_contents : Type[0] ≝ { 87 94 low: Z; 88 95 high: Z; 89 contents: contentmap 96 contents: contentmap; 97 class: block_class 90 98 }. 91 99 … … 184 192 nqed. 185 193 186 ndefinition empty_block : Z → Z → block_c ontents ≝187 λlo,hi .mk_block_contents lo hi (λy. Undef).194 ndefinition empty_block : Z → Z → block_class → block_contents ≝ 195 λlo,hi,bty.mk_block_contents lo hi (λy. Undef) bty. 188 196 189 197 ndefinition empty: mem ≝ 190 mk_mem (λx.empty_block OZ OZ ) (pos one) one_pos.198 mk_mem (λx.empty_block OZ OZ UnspecifiedB) (pos one) one_pos. 191 199 192 200 ndefinition nullptr: block ≝ OZ. … … 204 212 nqed. 205 213 206 ndefinition alloc : mem → Z → Z → mem × block ≝207 λm,lo,hi .〈mk_mem214 ndefinition alloc : mem → Z → Z → block_class → mem × block ≝ 215 λm,lo,hi,bty.〈mk_mem 208 216 (update … (nextblock m) 209 (empty_block lo hi )217 (empty_block lo hi bty) 210 218 (blocks m)) 211 219 (Zsucc (nextblock m)) … … 221 229 ndefinition free ≝ 222 230 λm,b.mk_mem (update … b 223 (empty_block OZ OZ )231 (empty_block OZ OZ UnspecifiedB) 224 232 (blocks m)) 225 233 (nextblock m) … … 241 249 ndefinition high_bound : mem → block → Z ≝ 242 250 λm,b.high (blocks m b). 251 ndefinition blockclass: mem → block → block_class ≝ 252 λm,b.class (blocks m b). 243 253 244 254 (* A block address is valid if it was previously allocated. It remains valid … … 550 560 nqed. 551 561 552 553 (* [valid_access m chunk b ofs] holds if a memory access (load or store) 562 ninductive class_compat : block_class → ptr_class → Prop ≝ 563  data_compat : class_compat DataB Data 564  idata_compat : class_compat IDataB IData 565  xdata_compat : class_compat XDataB XData 566  code_compat : class_compat CodeB Code 567  unspecified_compat : ∀p. class_compat UnspecifiedB p 568  universal_compat : ∀b. class_compat b Universal. 569 570 nlemma class_compat_dec : ∀b,p. class_compat b p + ¬class_compat b p. 571 #b p; ncases b; 572 ##[ ##1: @1; //; 573 ## ##*: ncases p; /2/; @2; @; #H; ninversion H; #e1 e2; ndestruct; #e3; ndestruct; 574 ##] nqed. 575 576 ndefinition is_class_compat : block_class → ptr_class → bool ≝ 577 λb,p. match class_compat_dec b p with [ inl _ ⇒ true  inr _ ⇒ false ]. 578 579 (* [valid_access m chunk pcl b ofs] holds if a memory access (load or store) 554 580 of the given chunk is possible in [m] at address [b, ofs]. 555 581 This means: … … 557 583  The range of bytes accessed is within the bounds of [b]. 558 584  The offset [ofs] is aligned. 585  The pointer classs [pcl] is compatible with the class of [b]. 559 586 *) 560 587 561 ninductive valid_access (m: mem) (chunk: memory_chunk) ( b: block) (ofs: Z)588 ninductive valid_access (m: mem) (chunk: memory_chunk) (pcl: ptr_class) (b: block) (ofs: Z) 562 589 : Prop ≝ 563 590  valid_access_intro: … … 566 593 ofs + size_chunk chunk ≤ high_bound m b → 567 594 (align_chunk chunk ∣ ofs) → 568 valid_access m chunk b ofs. 595 class_compat (blockclass m b) pcl → 596 valid_access m chunk pcl b ofs. 569 597 570 598 (* The following function checks whether accessing the given memory chunk … … 573 601 (* XXX: Using + and ¬ instead of Sum and Not causes trouble *) 574 602 nlet rec in_bounds 575 (m:mem) (chunk:memory_chunk) ( b:block) (ofs:Z) on b :576 Sum (valid_access m chunk b ofs) (Not (valid_access m chunkb ofs)) ≝ ?.603 (m:mem) (chunk:memory_chunk) (pcl:ptr_class) (b:block) (ofs:Z) on b : 604 Sum (valid_access m chunk pcl b ofs) (Not (valid_access m chunk pcl b ofs)) ≝ ?. 577 605 napply (Zltb_elim_Type0 b (nextblock m)); #Hnext; 578 606 ##[ napply (Zleb_elim_Type0 (low_bound m b) ofs); #Hlo; 579 607 ##[ napply (Zleb_elim_Type0 (ofs + size_chunk chunk) (high_bound m b)); #Hhi; 580 608 ##[ nelim (dec_dividesZ (align_chunk chunk) ofs); #Hal; 581 ##[ @1; @; // ##] 609 ##[ ncases (class_compat_dec (blockclass m b) pcl); #Hcl; 610 ##[ @1; @; // ##] 611 ##] 582 612 ##] 583 613 ##] 584 614 ##] 585 @2; napply nmk; *; #Hval; #Hlo'; #Hhi'; #Hal'; napply (absurd ???); //;615 @2; napply nmk; *; #Hval; #Hlo'; #Hhi'; #Hal'; #Hcl'; napply (absurd ???); //; 586 616 nqed. 587 617 588 618 nlemma in_bounds_true: 589 ∀m,chunk, b,ofs. ∀A: Type[0]. ∀a1,a2: A.590 valid_access m chunk b ofs >591 (match in_bounds m chunk b ofs with619 ∀m,chunk,pcl,b,ofs. ∀A: Type[0]. ∀a1,a2: A. 620 valid_access m chunk pcl b ofs > 621 (match in_bounds m chunk pcl b ofs with 592 622 [ inl _ ⇒ a1  inr _ ⇒ a2 ]) = a1. 593 #m ;#chunk;#b;#ofs;#A;#a1;#a2;#H;594 ncases (in_bounds m chunk b ofs);nnormalize;#H1;623 #m chunk pcl b ofs A a1 a2 H; 624 ncases (in_bounds m chunk pcl b ofs);nnormalize;#H1; 595 625 ##[// 596 626 ##nelim (?:False);napply (absurd ? H H1)] … … 600 630 given offset falls within the bounds of the corresponding block. *) 601 631 602 ndefinition valid_pointer : mem → block → Z → bool ≝603 λm, b,ofs. Zltb b (nextblock m) ∧632 ndefinition valid_pointer : mem → ptr_class → block → Z → bool ≝ 633 λm,pcl,b,ofs. Zltb b (nextblock m) ∧ 604 634 Zleb (low_bound m b) ofs ∧ 605 Zltb ofs (high_bound m b). 606 (* XXX: use lebZ etc. 607 ≝ λm,b,ofs.b < nextblock m ∧ 608 low_bound m b ≤ ofs ∧ 609 610 ofs < high_bound m b. *) 635 Zltb ofs (high_bound m b) ∧ 636 is_class_compat (blockclass m b) pcl. 611 637 612 638 (* [load chunk m b ofs] perform a read in memory state [m], at address … … 614 640 or the memory access is out of bounds. *) 615 641 616 ndefinition load : memory_chunk → mem → block → Z → option val ≝617 λchunk,m, b,ofs.618 match in_bounds m chunk b ofs with642 ndefinition load : memory_chunk → mem → ptr_class → block → Z → option val ≝ 643 λchunk,m,pcl,b,ofs. 644 match in_bounds m chunk pcl b ofs with 619 645 [ inl _ ⇒ Some ? (load_result chunk 620 646 (getN (pred_size_chunk chunk) ofs (contents (blocks m b)))) … … 622 648 623 649 nlemma load_inv: 624 ∀chunk,m, b,ofs,v.625 load chunk m b ofs = Some ? v →626 valid_access m chunk b ofs ∧650 ∀chunk,m,pcl,b,ofs,v. 651 load chunk m pcl b ofs = Some ? v → 652 valid_access m chunk pcl b ofs ∧ 627 653 v = load_result chunk 628 654 (getN (pred_size_chunk chunk) ofs (contents (blocks m b))). 629 #chunk ;#m;#b;#ofs;#v;nwhd in ⊢ (??%? → ?);630 ncases (in_bounds m chunk b ofs); #Haccess; nwhd in ⊢ ((??%?) → ?); #H;655 #chunk m pcl b ofs v; nwhd in ⊢ (??%? → ?); 656 ncases (in_bounds m chunk pcl b ofs); #Haccess; nwhd in ⊢ ((??%?) → ?); #H; 631 657 ##[ @;//; ndestruct; //; 632 658 ## ndestruct … … 639 665 nlet rec loadv (chunk:memory_chunk) (m:mem) (addr:val) on addr : option val ≝ 640 666 match addr with 641 [ Vptr b ofs ⇒ load chunk mb (signed ofs)667 [ Vptr pcl b ofs ⇒ load chunk m pcl b (signed ofs) 642 668  _ ⇒ None ? ]. 643 669 … … 651 677 (update ? b 652 678 (mk_block_contents (low c) (high c) 653 (setN (pred_size_chunk chunk) ofs v (contents c)) )679 (setN (pred_size_chunk chunk) ofs v (contents c)) (class c)) 654 680 (blocks m)) 655 681 (nextblock m) … … 661 687 or the memory access is out of bounds. *) 662 688 663 ndefinition store : memory_chunk → mem → block → Z → val → option mem ≝664 λchunk,m, b,ofs,v.665 match in_bounds m chunk b ofs with689 ndefinition store : memory_chunk → mem → ptr_class → block → Z → val → option mem ≝ 690 λchunk,m,pcl,b,ofs,v. 691 match in_bounds m chunk pcl b ofs with 666 692 [ inl _ ⇒ Some ? (unchecked_store chunk m b ofs v) 667 693  inr _ ⇒ None ? ]. 668 694 669 695 nlemma store_inv: 670 ∀chunk,m, b,ofs,v,m'.671 store chunk m b ofs v = Some ? m' →672 valid_access m chunk b ofs ∧696 ∀chunk,m,pcl,b,ofs,v,m'. 697 store chunk m pcl b ofs v = Some ? m' → 698 valid_access m chunk pcl b ofs ∧ 673 699 m' = unchecked_store chunk m b ofs v. 674 #chunk ;#m;#b;#ofs;#v;#m';nwhd in ⊢ (??%? → ?);700 #chunk m pcl b ofs v m'; nwhd in ⊢ (??%? → ?); 675 701 (*9*) 676 ncases (in_bounds m chunk b ofs);#Hv;nwhd in ⊢(??%? → ?);#Heq;702 ncases (in_bounds m chunk pcl b ofs);#Hv;nwhd in ⊢(??%? → ?);#Heq; 677 703 ##[@; ##[//ndestruct;//] 678 704 ##ndestruct] … … 685 711 λchunk,m,addr,v. 686 712 match addr with 687 [ Vptr b ofs ⇒ store chunk mb (signed ofs) v713 [ Vptr pcl b ofs ⇒ store chunk m pcl b (signed ofs) v 688 714  _ ⇒ None ? ]. 689 715 … … 752 778 nqed. 753 779 754 ndefinition block_init_data : list init_data → block_c ontents ≝755 λi_data .mk_block_contents756 OZ (size_init_data_list i_data) (contents_init_data OZ i_data) .757 758 ndefinition alloc_init_data : mem → list init_data → mem × block ≝759 λm,i_data .780 ndefinition block_init_data : list init_data → block_class → block_contents ≝ 781 λi_data,bcl.mk_block_contents 782 OZ (size_init_data_list i_data) (contents_init_data OZ i_data) bcl. 783 784 ndefinition alloc_init_data : mem → list init_data → block_class → mem × block ≝ 785 λm,i_data,bcl. 760 786 〈mk_mem (update ? (nextblock m) 761 (block_init_data i_data )787 (block_init_data i_data bcl) 762 788 (blocks m)) 763 789 (Zsucc (nextblock m)) … … 766 792 767 793 nremark block_init_data_empty: 768 block_init_data [] = empty_block OZ OZ.794 ∀bcl. block_init_data [ ] bcl = empty_block OZ OZ bcl. 769 795 //; 770 796 nqed. … … 781 807 782 808 nlemma valid_access_valid_block: 783 ∀m,chunk, b,ofs. valid_access m chunkb ofs → valid_block m b.784 #m;#chunk;# b;#ofs;#H;809 ∀m,chunk,pcl,b,ofs. valid_access m chunk pcl b ofs → valid_block m b. 810 #m;#chunk;#pcl;#b;#ofs;#H; 785 811 nelim H;//; 786 812 nqed. 787 813 788 814 nlemma valid_access_aligned: 789 ∀m,chunk, b,ofs.790 valid_access m chunk b ofs → (align_chunk chunk ∣ ofs).791 #m;#chunk;# b;#ofs;#H;815 ∀m,chunk,pcl,b,ofs. 816 valid_access m chunk pcl b ofs → (align_chunk chunk ∣ ofs). 817 #m;#chunk;#pcl;#b;#ofs;#H; 792 818 nelim H;//; 793 819 nqed. 794 820 795 821 nlemma valid_access_compat: 796 ∀m,chunk1,chunk2, b,ofs.822 ∀m,chunk1,chunk2,pcl,b,ofs. 797 823 size_chunk chunk1 = size_chunk chunk2 → 798 valid_access m chunk1 b ofs →799 valid_access m chunk2 b ofs.800 #m;#chunk;#chunk2;# b;#ofs;#H1;#H2;801 nelim H2;#H3;#H4;#H5;#H6; 824 valid_access m chunk1 pcl b ofs → 825 valid_access m chunk2 pcl b ofs. 826 #m;#chunk;#chunk2;#pcl;#b;#ofs;#H1;#H2; 827 nelim H2;#H3;#H4;#H5;#H6;#H7; 802 828 nrewrite > H1 in H5;#H5; 803 829 @;//; … … 810 836 811 837 ntheorem valid_access_load: 812 ∀m,chunk, b,ofs.813 valid_access m chunk b ofs →814 ∃v. load chunk m b ofs = Some ? v.815 #m;#chunk;# b;#ofs;#H;@;838 ∀m,chunk,pcl,b,ofs. 839 valid_access m chunk pcl b ofs → 840 ∃v. load chunk m pcl b ofs = Some ? v. 841 #m;#chunk;#pcl;#b;#ofs;#H;@; 816 842 ##[##2:nwhd in ⊢ (??%?);napply in_bounds_true;//; 817 843 ####skip] … … 819 845 820 846 ntheorem load_valid_access: 821 ∀m,chunk, b,ofs,v.822 load chunk m b ofs = Some ? v →823 valid_access m chunk b ofs.824 #m;#chunk;# b;#ofs;#v;#H;847 ∀m,chunk,pcl,b,ofs,v. 848 load chunk m pcl b ofs = Some ? v → 849 valid_access m chunk pcl b ofs. 850 #m;#chunk;#pcl;#b;#ofs;#v;#H; 825 851 ncases (load_inv … H);//; 826 852 nqed. … … 831 857 832 858 nlemma valid_access_store: 833 ∀m1,chunk, b,ofs,v.834 valid_access m1 chunk b ofs →835 ∃m2. store chunk m1 b ofs v = Some ? m2.836 #m1;#chunk;# b;#ofs;#v;#H;859 ∀m1,chunk,pcl,b,ofs,v. 860 valid_access m1 chunk pcl b ofs → 861 ∃m2. store chunk m1 pcl b ofs v = Some ? m2. 862 #m1;#chunk;#pcl;#b;#ofs;#v;#H; 837 863 @; 838 864 ##[##2:napply in_bounds_true;// … … 843 869 844 870 nlemma low_bound_store: 845 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →871 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 846 872 ∀b'.low_bound m2 b' = low_bound m1 b'. 847 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;873 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 848 874 #b';ncases (store_inv … STORE); 849 875 #H1;#H2;nrewrite > H2; … … 854 880 855 881 nlemma nextblock_store : 856 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →882 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 857 883 nextblock m2 = nextblock m1. 858 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;884 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 859 885 ncases (store_inv … STORE); 860 886 #Hvalid;#Heq; … … 863 889 864 890 nlemma high_bound_store: 865 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →891 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 866 892 ∀b'. high_bound m2 b' = high_bound m1 b'. 867 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;893 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 868 894 #b';ncases (store_inv … STORE); 869 895 #Hvalid;#H; … … 874 900 nqed. 875 901 902 nlemma block_class_store: 903 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 904 ∀b'. blockclass m2 b' = blockclass m1 b'. 905 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 906 #b';ncases (store_inv … STORE); 907 #Hvalid;#H; 908 nrewrite > H; 909 nwhd in ⊢ (??(?%?)?);nwhd in ⊢ (??%?); 910 nwhd in ⊢ (??(?%)?);nlapply (eqZb_to_Prop b' b); 911 ncases (eqZb b' b);nnormalize;//; 912 nqed. 913 876 914 nlemma store_valid_block_1: 877 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →915 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 878 916 ∀b'. valid_block m1 b' → valid_block m2 b'. 879 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;917 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 880 918 #b';nwhd in ⊢ (% → %);#Hv; 881 919 nrewrite > (nextblock_store … STORE);//; … … 883 921 884 922 nlemma store_valid_block_2: 885 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →923 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 886 924 ∀b'. valid_block m2 b' → valid_block m1 b'. 887 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;925 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 888 926 #b';nwhd in ⊢ (%→%); 889 927 nrewrite > (nextblock_store … STORE);//; … … 893 931 894 932 nlemma store_valid_access_1: 895 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →896 ∀chunk', b',ofs'.897 valid_access m1 chunk' b' ofs' → valid_access m2 chunk' b' ofs'.898 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;899 #chunk';# b';#ofs';933 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 934 ∀chunk',pcl',b',ofs'. 935 valid_access m1 chunk' pcl' b' ofs' → valid_access m2 chunk' pcl' b' ofs'. 936 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 937 #chunk';#pcl';#b';#ofs'; 900 938 * Hv; 901 #Hvb;#Hl;#Hr;#Halign; 939 #Hvb;#Hl;#Hr;#Halign;#Hptr; 902 940 @;//; 903 941 ##[napply (store_valid_block_1 … STORE);// 904 942 ##nrewrite > (low_bound_store … STORE …);// 905 ##nrewrite > (high_bound_store … STORE …);//] 943 ##nrewrite > (high_bound_store … STORE …);// 944 ##nrewrite > (block_class_store … STORE …);//] 906 945 nqed. 907 946 908 947 nlemma store_valid_access_2: 909 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →910 ∀chunk', b',ofs'.911 valid_access m2 chunk' b' ofs' → valid_access m1 chunk' b' ofs'.912 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;913 #chunk';# b';#ofs';948 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 949 ∀chunk',pcl',b',ofs'. 950 valid_access m2 chunk' pcl' b' ofs' → valid_access m1 chunk' pcl' b' ofs'. 951 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 952 #chunk';#pcl';#b';#ofs'; 914 953 * Hv; 915 #Hvb;#Hl;#Hr;#Halign; 954 #Hvb;#Hl;#Hr;#Halign;#Hcompat; 916 955 @;//; 917 956 ##[napply (store_valid_block_2 … STORE);// 918 957 ##nrewrite < (low_bound_store … STORE …);// 919 ##nrewrite < (high_bound_store … STORE …);//] 958 ##nrewrite < (high_bound_store … STORE …);// 959 ##nrewrite < (block_class_store … STORE …);//] 920 960 nqed. 921 961 922 962 nlemma store_valid_access_3: 923 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →924 valid_access m1 chunk b ofs.925 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;963 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 964 valid_access m1 chunk pcl b ofs. 965 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 926 966 ncases (store_inv … STORE);//; 927 967 nqed. … … 930 970 store_valid_access_3: mem.*) 931 971 972 nlemma load_compat_pointer: 973 ∀chunk,m,pcl,pcl',b,ofs,v. 974 class_compat (blockclass m b) pcl' → 975 load chunk m pcl b ofs = Some ? v → 976 load chunk m pcl' b ofs = Some ? v. 977 #chunk m pcl pcl' b ofs v Hcompat LOAD. 978 nlapply (load_valid_access … LOAD); #Hvalid; 979 ncut (valid_access m chunk pcl' b ofs); 980 ##[ @;nelim Hvalid; //; 981 ## #Hvalid'; 982 nrewrite < LOAD; nwhd in ⊢ (??%%); 983 nrewrite > (in_bounds_true … (option val) ?? Hvalid); 984 nrewrite > (in_bounds_true … (option val) ?? Hvalid'); 985 // 986 ##] nqed. 987 932 988 ntheorem load_store_similar: 933 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →989 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 934 990 ∀chunk'. 935 991 size_chunk chunk' = size_chunk chunk → 936 load chunk' m2 b ofs = Some ? (load_result chunk' v).937 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;992 load chunk' m2 pcl b ofs = Some ? (load_result chunk' v). 993 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 938 994 #chunk';#Hsize;ncases (store_inv … STORE); 939 995 #Hv;#Heq; 940 996 nwhd in ⊢ (??%?); 941 nrewrite > (in_bounds_true m2 chunk' b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b)))))997 nrewrite > (in_bounds_true m2 chunk' pcl b ofs ? (Some ? (load_result chunk' (getN (pred_size_chunk chunk') ofs (contents (blocks m2 b))))) 942 998 (None ?) ?); 943 999 ##[nrewrite > Heq; … … 949 1005 nrewrite > (size_chunk_pred …) in Hsize;#Hsize; 950 1006 napply injective_Z_of_nat;napply (injective_Zplus_r 1);//;##] 951 ##napply (store_valid_access_1 ??????STORE);952 ncases Hv;#H1;#H2;#H3;#H4; @;//;1007 ##napply (store_valid_access_1 … STORE); 1008 ncases Hv;#H1;#H2;#H3;#H4;#H5;@;//; 953 1009 nrewrite > (align_chunk_compat … Hsize);//] 954 1010 nqed. 955 1011 956 1012 ntheorem load_store_same: 957 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →958 load chunk m2 b ofs = Some ? (load_result chunk v).959 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;1013 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 1014 load chunk m2 pcl b ofs = Some ? (load_result chunk v). 1015 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 960 1016 napply load_store_similar;//; 961 1017 nqed. 962 1018 963 1019 ntheorem load_store_other: 964 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →965 ∀chunk', b',ofs'.1020 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 1021 ∀chunk',pcl',b',ofs'. 966 1022 b' ≠ b 967 1023 ∨ ofs' + size_chunk chunk' ≤ ofs 968 1024 ∨ ofs + size_chunk chunk ≤ ofs' → 969 load chunk' m2 b' ofs' = load chunk' m1b' ofs'.970 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;971 #chunk';# b';#ofs';#H;1025 load chunk' m2 pcl' b' ofs' = load chunk' m1 pcl' b' ofs'. 1026 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 1027 #chunk';#pcl';#b';#ofs';#H; 972 1028 ncases (store_inv … STORE); 973 1029 #Hvalid;#Heq;nwhd in ⊢ (??%%); 974 ncases (in_bounds m1 chunk' b' ofs');975 ##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' b' ofs' ? (Some ? ?) ??);1030 ncases (in_bounds m1 chunk' pcl' b' ofs'); 1031 ##[#Hvalid1;nrewrite > (in_bounds_true m2 chunk' pcl' b' ofs' ? (Some ? ?) ??); 976 1032 ##[nwhd in ⊢ (???%);napply eq_f;napply eq_f; 977 1033 nrewrite > Heq;nwhd in ⊢ (??(???(? (? % ?)))?); … … 989 1045 ###Hneq;@ ##] 990 1046 ##napply (store_valid_access_1 … STORE);//##] 991 ##nwhd in ⊢ (? → ???%);nlapply (in_bounds m2 chunk' b' ofs');1047 ##nwhd in ⊢ (? → ???%);nlapply (in_bounds m2 chunk' pcl' b' ofs'); 992 1048 #H1;ncases H1; 993 1049 ##[#H2;#H3;nlapply (store_valid_access_2 … STORE … H2);#Hfalse; … … 999 1055 1000 1056 ntheorem load_store_overlap: 1001 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →1002 ∀chunk',ofs',v'. load chunk' m2 b ofs' = Some ? v' →1057 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 1058 ∀chunk',ofs',v'. load chunk' m2 pcl b ofs' = Some ? v' → 1003 1059 ofs' ≠ ofs → 1004 1060 ofs < ofs' + size_chunk chunk' → 1005 1061 ofs' < ofs + size_chunk chunk → 1006 1062 v' = Vundef. 1007 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;1063 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 1008 1064 #chunk';#ofs';#v';#H; 1009 1065 #H1;#H2;#H3; … … 1021 1077 1022 1078 ntheorem load_store_overlap': 1023 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →1079 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 1024 1080 ∀chunk',ofs'. 1025 valid_access m1 chunk' b ofs' →1081 valid_access m1 chunk' pcl b ofs' → 1026 1082 ofs' ≠ ofs → 1027 1083 ofs < ofs' + size_chunk chunk' → 1028 1084 ofs' < ofs + size_chunk chunk → 1029 load chunk' m2 b ofs' = Some ? Vundef.1030 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;1085 load chunk' m2 pcl b ofs' = Some ? Vundef. 1086 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 1031 1087 #chunk';#ofs';#Hvalid;#H;#H1;#H2; 1032 ncut (∃v'.load chunk' m2 b ofs' = Some ? v')1088 ncut (∃v'.load chunk' m2 pcl b ofs' = Some ? v') 1033 1089 ##[napply valid_access_load; 1034 1090 napply (store_valid_access_1 … STORE);// … … 1039 1095 1040 1096 ntheorem load_store_mismatch: 1041 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →1097 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 1042 1098 ∀chunk',v'. 1043 load chunk' m2 b ofs = Some ? v' →1099 load chunk' m2 pcl b ofs = Some ? v' → 1044 1100 size_chunk chunk' ≠ size_chunk chunk → 1045 1101 v' = Vundef. 1046 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;1102 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 1047 1103 #chunk';#v';#H;#H1; 1048 1104 ncases (store_inv … STORE); … … 1060 1116 1061 1117 ntheorem load_store_mismatch': 1062 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →1118 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 1063 1119 ∀chunk'. 1064 valid_access m1 chunk' b ofs →1120 valid_access m1 chunk' pcl b ofs → 1065 1121 size_chunk chunk' ≠ size_chunk chunk → 1066 load chunk' m2 b ofs = Some ? Vundef.1067 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;1122 load chunk' m2 pcl b ofs = Some ? Vundef. 1123 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 1068 1124 #chunk';#Hvalid;#Hsize; 1069 ncut (∃v'.load chunk' m2 b ofs = Some ? v')1125 ncut (∃v'.load chunk' m2 pcl b ofs = Some ? v') 1070 1126 ##[napply (valid_access_load …); 1071 napply (store_valid_access_1 … STORE);// 1127 napply 1128 (store_valid_access_1 … STORE);// 1072 1129 ##*;#x;#Hx;nrewrite > Hx;napply eq_f; 1073 1130 napply (load_store_mismatch … STORE … Hsize);//;##] … … 1121 1178 1122 1179 ntheorem load_store_characterization: 1123 ∀chunk,m1, b,ofs,v,m2.store chunk m1b ofs v = Some ? m2 →1124 ∀chunk', b',ofs'.1125 valid_access m1 chunk' b' ofs' >1126 load chunk' m2 b' ofs' =1180 ∀chunk,m1,pcl,b,ofs,v,m2.store chunk m1 pcl b ofs v = Some ? m2 → 1181 ∀chunk',pcl',b',ofs'. 1182 valid_access m1 chunk' pcl' b' ofs' → 1183 load chunk' m2 pcl' b' ofs' = 1127 1184 match load_store_classification chunk b ofs chunk' b' ofs' with 1128 [ lsc_similar _ _ _ =>Some ? (load_result chunk' v)1129  lsc_other _ => load chunk' m1b' ofs'1130  lsc_overlap _ _ _ _ =>Some ? Vundef1131  lsc_mismatch _ _ _ =>Some ? Vundef ].1132 #chunk;#m1;# b;#ofs;#v;#m2;#STORE;1133 #chunk';# b';#ofs';#Hvalid;1134 ncut (∃v'. load chunk' m2 b' ofs' = Some ? v')1185 [ lsc_similar _ _ _ ⇒ Some ? (load_result chunk' v) 1186  lsc_other _ ⇒ load chunk' m1 pcl' b' ofs' 1187  lsc_overlap _ _ _ _ ⇒ Some ? Vundef 1188  lsc_mismatch _ _ _ ⇒ Some ? Vundef ]. 1189 #chunk;#m1;#pcl b ofs;#v;#m2;#STORE; 1190 #chunk';#pcl';#b';#ofs';#Hvalid; 1191 ncut (∃v'. load chunk' m2 pcl' b' ofs' = Some ? v') 1135 1192 ##[napply valid_access_load; 1136 1193 napply (store_valid_access_1 … STORE … Hvalid); 1137 1194 ##*;#x;#Hx; 1138 1195 ncases (load_store_classification chunk b ofs chunk' b' ofs') 1139 ##[#H1;#H2;#H3;nrewrite > H1;napply load_store_similar;//; 1196 ##[#H1;#H2;#H3;nwhd in ⊢ (???%);nrewrite < H1;nrewrite < H2; 1197 napply (load_compat_pointer … pcl); 1198 ##[ nrewrite > (block_class_store … STORE b); 1199 ncases Hvalid; //; 1200 ## napply (load_store_similar … STORE);//; 1201 ##] 1140 1202 ###H1;napply (load_store_other … STORE); 1141 1203 ncases H1 … … 1144 1206 ###H2;@;@2;//] 1145 1207 ###H2;@2;//] 1146 ###H1;#H2;#H3;#H4;nrewrite < H1 in Hx; 1147 #Hx;nrewrite > Hx; 1148 napply eq_f;napply (load_store_overlap … STORE … Hx);/2/; 1149 ###H1;#H2;#H3;nrewrite < H1 in Hx; 1150 nrewrite < H2;#Hx;nrewrite > Hx;napply eq_f; 1151 napply (load_store_mismatch … STORE … Hx);/2/] 1208 ###H1;#H2;#H3;#H4; nlapply (load_compat_pointer … pcl … Hx); 1209 ##[ nrewrite > (block_class_store … STORE b'); 1210 nrewrite > H1; nelim (store_valid_access_3 … STORE); // 1211 ## nrewrite < H1 in ⊢ (% → ?);#Hx'; 1212 nrewrite < H1 in Hx;#Hx;nrewrite > Hx; 1213 napply eq_f;napply (load_store_overlap … STORE … Hx');/2/; 1214 ##] 1215 ###H1;#H2;#H3; 1216 nlapply (load_compat_pointer … pcl … Hx); 1217 ##[ nrewrite > (block_class_store … STORE b'); 1218 nrewrite > H1; nelim (store_valid_access_3 … STORE); // 1219 ## nrewrite < H1 in Hx ⊢ %; nrewrite < H2; #Hx Hx'; 1220 nrewrite > Hx;napply eq_f; 1221 napply (load_store_mismatch … STORE … Hx');/2/ 1222 ##] 1223 ##] 1224 1152 1225 ##] 1153 1226 nqed. … … 1183 1256 1184 1257 nlemma nextblock_alloc: 1185 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1258 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1186 1259 nextblock m2 = Zsucc (nextblock m1). 1187 #m1;#lo;#hi;# m2;#b;#ALLOC;1260 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1188 1261 nwhd in ALLOC:(??%%); ndestruct; //; 1189 1262 nqed. 1190 1263 1191 1264 nlemma alloc_result: 1192 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1265 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1193 1266 b = nextblock m1. 1194 #m1;#lo;#hi;# m2;#b;#ALLOC;1267 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1195 1268 nwhd in ALLOC:(??%%); ndestruct; //; 1196 1269 nqed. … … 1198 1271 1199 1272 nlemma valid_block_alloc: 1200 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1273 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1201 1274 ∀b'. valid_block m1 b' → valid_block m2 b'. 1202 #m1;#lo;#hi;# m2;#b;#ALLOC;1275 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1203 1276 #b'; nrewrite > (unfold_valid_block m1 b'); 1204 1277 nrewrite > (unfold_valid_block m2 b'); … … 1208 1281 1209 1282 nlemma fresh_block_alloc: 1210 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1283 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1211 1284 ¬(valid_block m1 b). 1212 #m1;#lo;#hi;# m2;#b;#ALLOC;1285 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1213 1286 nrewrite > (unfold_valid_block m1 b); 1214 1287 nrewrite > (alloc_result … ALLOC); … … 1217 1290 1218 1291 nlemma valid_new_block: 1219 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1292 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1220 1293 valid_block m2 b. 1221 #m1;#lo;#hi;# m2;#b;#ALLOC;1294 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1222 1295 nrewrite > (unfold_valid_block m2 b); 1223 1296 nrewrite > (alloc_result … ALLOC); … … 1231 1304 1232 1305 nlemma valid_block_alloc_inv: 1233 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1306 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1234 1307 ∀b'. valid_block m2 b' → b' = b ∨ valid_block m1 b'. 1235 #m1;#lo;#hi;# m2;#b;#ALLOC;1308 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1236 1309 #b'; 1237 1310 nrewrite > (unfold_valid_block m2 b'); … … 1243 1316 1244 1317 nlemma low_bound_alloc: 1245 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1318 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1246 1319 ∀b'. low_bound m2 b' = if eqZb b' b then lo else low_bound m1 b'. 1247 #m1;#lo;#hi;# m2;#b;#ALLOC;1320 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1248 1321 nwhd in ALLOC:(??%%); ndestruct; #b'; 1249 1322 nrewrite > (unfold_update block_contents ????); … … 1252 1325 1253 1326 nlemma low_bound_alloc_same: 1254 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1327 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1255 1328 low_bound m2 b = lo. 1256 #m1;#lo;#hi;# m2;#b;#ALLOC;1329 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1257 1330 nrewrite > (low_bound_alloc … ALLOC b); 1258 1331 nrewrite > (eqZb_z_z …); … … 1261 1334 1262 1335 nlemma low_bound_alloc_other: 1263 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1336 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1264 1337 ∀b'. valid_block m1 b' → low_bound m2 b' = low_bound m1 b'. 1265 #m1;#lo;#hi;# m2;#b;#ALLOC;1338 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1266 1339 #b'; nrewrite > (low_bound_alloc … ALLOC b'); 1267 1340 napply eqZb_elim; #Hb; … … 1272 1345 1273 1346 nlemma high_bound_alloc: 1274 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1347 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1275 1348 ∀b'. high_bound m2 b' = if eqZb b' b then hi else high_bound m1 b'. 1276 #m1;#lo;#hi;# m2;#b;#ALLOC;1349 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1277 1350 nwhd in ALLOC:(??%%); ndestruct; #b'; 1278 1351 nrewrite > (unfold_update block_contents ????); … … 1281 1354 1282 1355 nlemma high_bound_alloc_same: 1283 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1356 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1284 1357 high_bound m2 b = hi. 1285 #m1;#lo;#hi;# m2;#b;#ALLOC;1358 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1286 1359 nrewrite > (high_bound_alloc … ALLOC b); 1287 1360 nrewrite > (eqZb_z_z …); … … 1290 1363 1291 1364 nlemma high_bound_alloc_other: 1292 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1365 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1293 1366 ∀b'. valid_block m1 b' → high_bound m2 b' = high_bound m1 b'. 1294 #m1;#lo;#hi;# m2;#b;#ALLOC;1367 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1295 1368 #b'; nrewrite > (high_bound_alloc … ALLOC b'); 1296 1369 napply eqZb_elim; #Hb; … … 1300 1373 ##] nqed. 1301 1374 1375 nlemma class_alloc: 1376 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1377 ∀b'.blockclass m2 b' = if eqZb b' b then bcl else blockclass m1 b'. 1378 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1379 nwhd in ALLOC:(??%%); ndestruct; #b'; 1380 ncases (eqZb b' (nextblock m1)); //; 1381 nqed. 1382 1383 nlemma class_alloc_same: 1384 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1385 blockclass m2 b = bcl. 1386 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1387 nwhd in ALLOC:(??%%); ndestruct; 1388 nrewrite > (eqZb_z_z ?); //; 1389 nqed. 1390 1391 nlemma class_alloc_other: 1392 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1393 ∀b'. valid_block m1 b' → blockclass m2 b' = blockclass m1 b'. 1394 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1395 #b'; nrewrite > (class_alloc … ALLOC b'); 1396 napply eqZb_elim; #Hb; 1397 ##[ nrewrite > Hb; #bad; napply False_ind; napply (absurd ? bad); 1398 napply (fresh_block_alloc … ALLOC) 1399 ## // 1400 ##] nqed. 1401 1302 1402 nlemma valid_access_alloc_other: 1303 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1304 ∀chunk, b',ofs.1305 valid_access m1 chunk b' ofs →1306 valid_access m2 chunk b' ofs.1307 #m1;#lo;#hi;# m2;#b;#ALLOC;1308 #chunk;# b';#ofs;#H;1309 ncases H; #Hvalid; #Hlow; #Hhigh;#Halign; 1403 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1404 ∀chunk,pcl,b',ofs. 1405 valid_access m1 chunk pcl b' ofs → 1406 valid_access m2 chunk pcl b' ofs. 1407 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1408 #chunk;#pcl;#b';#ofs;#H; 1409 ncases H; #Hvalid; #Hlow; #Hhigh;#Halign;#Hcompat; 1310 1410 @; 1311 1411 ##[ napply (valid_block_alloc … ALLOC); // … … 1313 1413 ## nrewrite > (high_bound_alloc_other … ALLOC b' Hvalid); // 1314 1414 ## // 1415 ## nrewrite > (class_alloc_other … ALLOC b' Hvalid); //; 1315 1416 ##] nqed. 1316 1417 1317 1418 nlemma valid_access_alloc_same: 1318 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1319 ∀chunk, ofs.1419 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1420 ∀chunk,pcl,ofs. 1320 1421 lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) → 1321 valid_access m2 chunk b ofs. 1322 #m1;#lo;#hi;#m2;#b;#ALLOC; 1323 #chunk;#ofs; #Hlo; #Hhi; #Halign; 1422 class_compat bcl pcl → 1423 valid_access m2 chunk pcl b ofs. 1424 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1425 #chunk;#pcl;#ofs; #Hlo; #Hhi; #Halign; #Hcompat; 1324 1426 @; 1325 1427 ##[ napply (valid_new_block … ALLOC) … … 1327 1429 ## nrewrite > (high_bound_alloc_same … ALLOC); // 1328 1430 ## // 1431 ## nrewrite > (class_alloc_same … ALLOC); // 1329 1432 ##] nqed. 1330 1433 … … 1334 1437 1335 1438 nlemma valid_access_alloc_inv: 1336 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1337 ∀chunk, b',ofs.1338 valid_access m2 chunk b' ofs →1339 valid_access m1 chunk b' ofs ∨1340 (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) )).1341 #m1;#lo;#hi;# m2;#b;#ALLOC;1342 #chunk;# b';#ofs;*;#Hblk;#Hlo;#Hhi;#Hal;1439 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1440 ∀chunk,pcl,b',ofs. 1441 valid_access m2 chunk pcl b' ofs → 1442 valid_access m1 chunk pcl b' ofs ∨ 1443 (b' = b ∧ lo ≤ ofs ∧ (ofs + size_chunk chunk ≤ hi ∧ (align_chunk chunk ∣ ofs) ∧ class_compat bcl pcl)). 1444 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1445 #chunk;#pcl;#b';#ofs;*;#Hblk;#Hlo;#Hhi;#Hal;#Hct; 1343 1446 nelim (valid_block_alloc_inv … ALLOC ? Hblk);#H; 1344 1447 ##[ nrewrite < H in ALLOC ⊢ %; #ALLOC'; 1345 1448 nrewrite > (low_bound_alloc_same … ALLOC') in Hlo; #Hlo'; 1346 1449 nrewrite > (high_bound_alloc_same … ALLOC') in Hhi; #Hhi'; 1347 @2; /4/ 1450 nrewrite > (class_alloc_same … ALLOC') in Hct; #Hct; 1451 @2; /4/; 1348 1452 ## @1;@;//; 1349 1453 ##[ nrewrite > (low_bound_alloc_other … ALLOC ??) in Hlo; // 1350 1454 ## nrewrite > (high_bound_alloc_other … ALLOC ??) in Hhi; // 1455 ## nrewrite > (class_alloc_other … ALLOC ??) in Hct; // 1351 1456 ##] 1352 1457 ##] nqed. 1353 1458 1354 1459 ntheorem load_alloc_unchanged: 1355 ∀m1,lo,hi, m2,b.alloc m1 lohi = 〈m2,b〉 →1356 ∀chunk, b',ofs.1460 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo bcl hi = 〈m2,b〉 → 1461 ∀chunk,pcl,b',ofs. 1357 1462 valid_block m1 b' → 1358 load chunk m2 b' ofs = load chunk m1b' ofs.1359 #m1;#lo;#hi;# m2;#b;#ALLOC;1360 #chunk;# b';#ofs;#H;nwhd in ⊢ (??%%);1361 ncases (in_bounds m2 chunk b' ofs); #H';1362 ##[ nelim (valid_access_alloc_inv … ALLOC ??? H');1463 load chunk m2 pcl b' ofs = load chunk m1 pcl b' ofs. 1464 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1465 #chunk;#pcl;#b';#ofs;#H;nwhd in ⊢ (??%%); 1466 ncases (in_bounds m2 chunk pcl b' ofs); #H'; 1467 ##[ nelim (valid_access_alloc_inv … ALLOC ???? H'); 1363 1468 ##[ #H''; (* XXX: if there's no hint that the result type is an option then the rewrite fails with an odd type error 1364 1469 nrewrite > (in_bounds_true ???? ??? H''); *) nrewrite > (in_bounds_true … ? (option val) ?? H''); 1365 1470 nwhd in ⊢ (??%?); (* XXX: if you do this at the point below the proof term is illtyped. *) 1366 nwhd in ALLOC:(??%%); ndestruct; 1367 nrewrite > (update_o block_contents ?????); 1368 ##[ // ## napply sym_neq; napply (valid_not_valid_diff … H); napply (fresh_block_alloc … );//; ##] 1471 ncut (b' ≠ b); 1472 ##[ napply (valid_not_valid_diff … H); napply (fresh_block_alloc … ALLOC); 1473 ## nwhd in ALLOC:(??%%); ndestruct; 1474 nrewrite > (update_o block_contents ?????); /2/; 1475 ##] 1369 1476 ## *;*;#A;#B;#C; nrewrite < A in ALLOC ⊢ %; #ALLOC; 1370 1477 napply False_ind; napply (absurd ? H); napply (fresh_block_alloc … ALLOC) 1371 1478 ##] 1372 ## ncases (in_bounds m1 chunk b' ofs); #H''; nwhd in ⊢ (??%%); //;1479 ## ncases (in_bounds m1 chunk pcl b' ofs); #H''; nwhd in ⊢ (??%%); //; 1373 1480 napply False_ind; napply (absurd ? ? H'); napply (valid_access_alloc_other … ALLOC); // 1374 1481 ##] nqed. 1375 1482 1376 1483 ntheorem load_alloc_other: 1377 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1378 ∀chunk, b',ofs,v.1379 load chunk m1 b' ofs = Some ? v →1380 load chunk m2 b' ofs = Some ? v.1381 #m1;#lo;#hi;# m2;#b;#ALLOC;1382 #chunk;# b';#ofs;#v;#H;1383 nrewrite < H; napply (load_alloc_unchanged … ALLOC ???); /3/;1484 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1485 ∀chunk,pcl,b',ofs,v. 1486 load chunk m1 pcl b' ofs = Some ? v → 1487 load chunk m2 pcl b' ofs = Some ? v. 1488 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1489 #chunk;#pcl;#b';#ofs;#v;#H; 1490 nrewrite < H; napply (load_alloc_unchanged … ALLOC ???); ncases (load_valid_access … H); //; 1384 1491 nqed. 1385 1492 1386 1493 ntheorem load_alloc_same: 1387 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1388 ∀chunk, ofs,v.1389 load chunk m2 b ofs = Some ? v →1494 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1495 ∀chunk,pcl,ofs,v. 1496 load chunk m2 pcl b ofs = Some ? v → 1390 1497 v = Vundef. 1391 #m1;#lo;#hi;# m2;#b;#ALLOC;1392 #chunk;# ofs;#v;#H;1498 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1499 #chunk;#pcl;#ofs;#v;#H; 1393 1500 nelim (load_inv … H); #H0; #H1; nrewrite > H1; 1394 1501 nwhd in ALLOC:(??%%); (* XXX ndestruct; ??? *) napply (pairdisc_elim … ALLOC); 1395 1502 nwhd in ⊢ (??%% → ?);#e0;nrewrite < e0 in ⊢ (%→?); 1396 1503 nwhd in ⊢ (??%% → ?);#e1; 1397 nrewrite < e1; nrewrite < e0; nrewrite > (update_s ? ? (empty_block lo hi ) ?);1504 nrewrite < e1; nrewrite < e0; nrewrite > (update_s ? ? (empty_block lo hi bcl) ?); 1398 1505 nnormalize; ncases chunk; //; 1399 1506 nqed. 1400 1507 1401 1508 ntheorem load_alloc_same': 1402 ∀m1,lo,hi, m2,b.alloc m1 lo hi= 〈m2,b〉 →1403 ∀chunk, ofs.1509 ∀m1,lo,hi,bcl,m2,b.alloc m1 lo hi bcl = 〈m2,b〉 → 1510 ∀chunk,pcl,ofs. 1404 1511 lo ≤ ofs → ofs + size_chunk chunk ≤ hi → (align_chunk chunk ∣ ofs) → 1405 load chunk m2 b ofs = Some ? Vundef. 1406 #m1;#lo;#hi;#m2;#b;#ALLOC; 1407 #chunk;#ofs;#Hlo;#Hhi;#Hal; 1408 ncut (∃v. load chunk m2 b ofs = Some ? v); 1409 ##[ napply valid_access_load; @; /2/; 1410 ##[ nrewrite > (low_bound_alloc_same … ALLOC); // 1512 class_compat bcl pcl → 1513 load chunk m2 pcl b ofs = Some ? Vundef. 1514 #m1;#lo;#hi;#bcl;#m2;#b;#ALLOC; 1515 #chunk;#pcl;#ofs;#Hlo;#Hhi;#Hal;#Hct; 1516 ncut (∃v. load chunk m2 pcl b ofs = Some ? v); 1517 ##[ napply valid_access_load; @; //; 1518 ##[ napply (valid_new_block … ALLOC); 1519 ## nrewrite > (low_bound_alloc_same … ALLOC); // 1411 1520 ## nrewrite > (high_bound_alloc_same … ALLOC); // 1521 ## nrewrite > (class_alloc_same … ALLOC); // 1412 1522 ##] 1413 1523 ## *; #v;#LOAD; nrewrite > LOAD; napply eq_f; … … 1470 1580 nqed. 1471 1581 1582 nlemma class_free: 1583 ∀m,bf,b. b ≠ bf → blockclass (free m bf) b = blockclass m b. 1584 #m;#bf;#b;#H;nwhd in ⊢ (??%%); nwhd in ⊢ (??(?(?%?))?); 1585 nrewrite > (update_o block_contents …); //; napply sym_neq; //; 1586 nqed. 1587 1472 1588 nlemma valid_access_free_1: 1473 ∀m,bf,chunk, b,ofs.1474 valid_access m chunk b ofs → b ≠ bf →1475 valid_access (free m bf) chunk b ofs.1476 #m;#bf;#chunk;# b;#ofs;*;#Hval;#Hlo;#Hhi;#Hal;#Hneq;1589 ∀m,bf,chunk,pcl,b,ofs. 1590 valid_access m chunk pcl b ofs → b ≠ bf → 1591 valid_access (free m bf) chunk pcl b ofs. 1592 #m;#bf;#chunk;#pcl b ofs;*;#Hval;#Hlo;#Hhi;#Hal;#Hcompat;#Hneq; 1477 1593 @; //; 1478 1594 ##[ napply valid_block_free_1; // 1479 1595 ## nrewrite > (low_bound_free … Hneq); // 1480 1596 ## nrewrite > (high_bound_free … Hneq); // 1597 ## nrewrite > (class_free … Hneq); // 1481 1598 ##] nqed. 1482 1599 1483 1600 nlemma valid_access_free_2: 1484 ∀m, bf,chunk,ofs. ¬(valid_access (free m bf) chunkbf ofs).1485 #m;# bf;#chunk;#ofs; napply nmk; *; #Hval;#Hlo;#Hhi;#Hal;1601 ∀m,pcl,bf,chunk,ofs. ¬(valid_access (free m bf) chunk pcl bf ofs). 1602 #m;#pcl;#bf;#chunk;#ofs; napply nmk; *; #Hval;#Hlo;#Hhi;#Hal;#Hct; 1486 1603 nwhd in Hlo:(?%?);nwhd in Hlo:(?(?(?%?))?); nrewrite > (update_s block_contents …) in Hlo; 1487 1604 nwhd in Hhi:(??%);nwhd in Hhi:(??(?(?%?))); nrewrite > (update_s block_contents …) in Hhi; … … 1494 1611 1495 1612 nlemma valid_access_free_inv: 1496 ∀m,bf,chunk, b,ofs.1497 valid_access (free m bf) chunk b ofs →1498 valid_access m chunk b ofs ∧ b ≠ bf.1499 #m;#bf;#chunk;# b;#ofs; nelim (decidable_eq_Z_Type b bf);1613 ∀m,bf,chunk,pcl,b,ofs. 1614 valid_access (free m bf) chunk pcl b ofs → 1615 valid_access m chunk pcl b ofs ∧ b ≠ bf. 1616 #m;#bf;#chunk;#pcl b ofs; nelim (decidable_eq_Z_Type b bf); 1500 1617 ##[ #e; nrewrite > e; 1501 1618 #H; napply False_ind; napply (absurd ? H (valid_access_free_2 …)); 1502 1619 ## #ne; *; nrewrite > (low_bound_free … ne); 1503 1620 nrewrite > (high_bound_free … ne); 1504 #Hval; #Hlo; #Hhi; #Hal; 1505 @; ##[ @; //; napply (valid_block_free_2 … Hval); ## /2/ ##] 1621 nrewrite > (class_free … ne); 1622 #Hval; #Hlo; #Hhi; #Hal; #Hct; 1623 @; ##[ @; /2/; ## /2/ ##] 1506 1624 ##] nqed. 1507 1625 1508 1626 ntheorem load_free: 1509 ∀m,bf,chunk, b,ofs.1627 ∀m,bf,chunk,pcl,b,ofs. 1510 1628 b ≠ bf → 1511 load chunk (free m bf) b ofs = load chunk mb ofs.1512 #m;#bf;#chunk;# b;#ofs;#ne; nwhd in ⊢ (??%%);1513 nelim (in_bounds m chunk b ofs);1514 ##[ #Hval; nwhd in ⊢ (???%); nrewrite > (in_bounds_true ???? (option val) ???);1629 load chunk (free m bf) pcl b ofs = load chunk m pcl b ofs. 1630 #m;#bf;#chunk;#pcl b ofs;#ne; nwhd in ⊢ (??%%); 1631 nelim (in_bounds m chunk pcl b ofs); 1632 ##[ #Hval; nwhd in ⊢ (???%); nrewrite > (in_bounds_true ????? (option val) ???); 1515 1633 ##[ nwhd in ⊢ (??(??(??(???(?(?%?)))))?); nrewrite > (update_o block_contents …); //; 1516 1634 napply sym_neq; // 1517 1635 ## napply valid_access_free_1; //; napply ne; 1518 1636 ##] 1519 ## nelim (in_bounds (free m bf) chunk b ofs); (* XXX just // used to work *) ##[ ##2: nnormalize; //; ##]1637 ## nelim (in_bounds (free m bf) chunk pcl b ofs); (* XXX just // used to work *) ##[ ##2: nnormalize; //; ##] 1520 1638 #H;#H'; napply False_ind; napply (absurd ? ? H'); 1521 1639 nelim (valid_access_free_inv …H); //; … … 1545 1663 1546 1664 nlemma valid_access_free_list: 1547 ∀chunk, b,ofs,m,bl.1548 valid_access m chunk b ofs → ¬in_list ? b bl →1549 valid_access (free_list m bl) chunk b ofs.1550 #chunk; # b; #ofs; #m; #bl; nelim bl;1551 ##[ nwhd in ⊢ (?→?→(?%??? )); //1665 ∀chunk,pcl,b,ofs,m,bl. 1666 valid_access m chunk pcl b ofs → ¬in_list ? b bl → 1667 valid_access (free_list m bl) chunk pcl b ofs. 1668 #chunk; #pcl b ofs; #m; #bl; nelim bl; 1669 ##[ nwhd in ⊢ (?→?→(?%????)); // 1552 1670 ## #h;#t;#IH;#H;#notin; nrewrite > (unfold_free_list m h t); napply valid_access_free_1; 1553 1671 ##[ napply IH; //; napply (not_to_not ??? notin); #Ht; napply (in_list_cons … Ht) … … 1556 1674 1557 1675 nlemma valid_access_free_list_inv: 1558 ∀chunk, b,ofs,m,bl.1559 valid_access (free_list m bl) chunk b ofs →1560 ¬in_list ? b bl ∧ valid_access m chunk b ofs.1561 #chunk; # b; #ofs; #m; #bl; nelim bl;1562 ##[ nwhd in ⊢ ((?%??? )→?); #H; @; //1676 ∀chunk,pcl,b,ofs,m,bl. 1677 valid_access (free_list m bl) chunk pcl b ofs → 1678 ¬in_list ? b bl ∧ valid_access m chunk pcl b ofs. 1679 #chunk; #pcl b ofs; #m; #bl; nelim bl; 1680 ##[ nwhd in ⊢ ((?%????)→?); #H; @; // 1563 1681 ## #h;#t;#IH; nrewrite > (unfold_free_list m h t); #H; 1564 1682 nelim (valid_access_free_inv … H); #H';#ne; … … 1571 1689 1572 1690 nlemma valid_pointer_valid_access: 1573 ∀m, b,ofs.1574 valid_pointer m b ofs = true ↔ valid_access m Mint8unsignedb ofs.1575 #m;# b;#ofs;nwhd in ⊢ (?(??%?)?); @;1691 ∀m,pcl,b,ofs. 1692 valid_pointer m pcl b ofs = true ↔ valid_access m Mint8unsigned pcl b ofs. 1693 #m;#pcl b ofs;nwhd in ⊢ (?(??%?)?); @; 1576 1694 ##[ #H; 1577 1695 nlapply (andb_true_l … H); #H'; 1578 nlapply (andb_true_l … H'); #H1; 1579 nlapply (andb_true_r … H'); #H2; 1580 nlapply (andb_true_r … H); #H3; 1696 nlapply (andb_true_l … H'); #H''; 1697 nlapply (andb_true_l … H''); #H1; 1698 nlapply (andb_true_r … H''); #H2; 1699 nlapply (andb_true_r … H'); #H3; 1700 nlapply (andb_true_r … H); #H4; 1581 1701 @; 1582 1702 ##[ nrewrite > (unfold_valid_block m b); napply (Zltb_true_to_Zlt … H1) … … 1584 1704 ## nwhd in ⊢ (?(??%)?); (* arith, Zleb_true_to_Zle *) napply daemon 1585 1705 ## ncases ofs; /2/; 1706 ## nwhd in H4:(??%?); nelim (class_compat_dec (blockclass m b) pcl) in H4; 1707 ##[ //; ## #Hn e; nwhd in e:(??%%); ndestruct ##] 1586 1708 ##] 1587 ## *; #Hval;#Hlo;#Hhi;#Hal; 1709 ## *; #Hval;#Hlo;#Hhi;#Hal;#Hct; 1588 1710 nrewrite > (Zlt_to_Zltb_true … Hval); 1589 1711 nrewrite > (Zle_to_Zleb_true … Hlo); 1590 1712 nwhd in Hhi:(?(??%)?); nrewrite > (Zlt_to_Zltb_true … ?); 1591 //; (* arith *) napply daemon 1592 ##] nqed. 1713 ##[ nwhd in ⊢ (??%?); nelim (class_compat_dec (blockclass m b) pcl); 1714 ##[ //; 1715 ## #Hct'; napply False_ind; napply (absurd … Hct Hct'); 1716 ##] 1717 ## (* arith *) napply daemon 1718 ##] 1719 ##] 1720 nqed. 1593 1721 1594 1722 ntheorem valid_pointer_alloc: 1595 ∀m1,m2: mem. ∀lo,hi: Z. ∀b ,b': block. ∀ofs: Z.1596 alloc m1 lo hi = 〈m2, b'〉 →1597 valid_pointer m1 b ofs = true →1598 valid_pointer m2 b ofs = true.1599 #m1;#m2;#lo;#hi;#b ;#b';#ofs;#ALLOC;#VALID;1600 nlapply ((proj1 ?? (valid_pointer_valid_access ??? )) VALID); #Hval;1601 napply (proj2 ?? (valid_pointer_valid_access ??? ));1723 ∀m1,m2: mem. ∀lo,hi: Z. ∀bcl,pcl. ∀b,b': block. ∀ofs: Z. 1724 alloc m1 lo hi bcl = 〈m2, b'〉 → 1725 valid_pointer m1 pcl b ofs = true → 1726 valid_pointer m2 pcl b ofs = true. 1727 #m1;#m2;#lo;#hi;#bcl pcl;#b;#b';#ofs;#ALLOC;#VALID; 1728 nlapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval; 1729 napply (proj2 ?? (valid_pointer_valid_access ????)); 1602 1730 napply (valid_access_alloc_other … ALLOC … Hval); 1603 1731 nqed. 1604 1732 1605 1733 ntheorem valid_pointer_store: 1606 ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val. 1607 store chunk m1 b' ofs' v = Some ? m2 → 1608 valid_pointer m1 b ofs = true → valid_pointer m2 b ofs = true. 1609 #chunk;#m1;#m2;#b;#b';#ofs;#ofs';#v;#STORE;#VALID; 1610 nlapply ((proj1 ?? (valid_pointer_valid_access ???)) VALID); #Hval; 1611 napply (proj2 ?? (valid_pointer_valid_access ???)); 1734 ∀chunk: memory_chunk. ∀m1,m2: mem. 1735 ∀pcl,pcl': ptr_class. ∀b,b': block. ∀ofs,ofs': Z. ∀v: val. 1736 store chunk m1 pcl' b' ofs' v = Some ? m2 → 1737 valid_pointer m1 pcl b ofs = true → valid_pointer m2 pcl b ofs = true. 1738 #chunk;#m1;#m2;#pcl pcl';#b;#b';#ofs;#ofs';#v;#STORE;#VALID; 1739 nlapply ((proj1 ?? (valid_pointer_valid_access ????)) VALID); #Hval; 1740 napply (proj2 ?? (valid_pointer_valid_access ????)); 1612 1741 napply (store_valid_access_1 … STORE … Hval); 1613 1742 nqed. 1614 1743 1615 1744 (* * * Generic injections between memory states. *) 1616 1745 (* 1617 1746 (* Section GENERIC_INJECT. *) 1618 1747 … … 1656 1785 1657 1786 (*Hint Resolve valid_access_inj: mem.*) 1658 1787 *) 1659 1788 (* FIXME: can't use ndestruct below *) 1660 1789 nlemma grumpydestruct : ∀A,v. None A = Some A v → False. 1661 1790 #A;#v;#H;ndestruct; 1662 1791 nqed. 1663 1792 (* 1664 1793 nlemma store_unmapped_inj: ∀val_inj. 1665 ∀mi,m1,m2, b,ofs,v,chunk,m1'.1794 ∀mi,m1,m2,pcl,b,ofs,v,chunk,m1'. 1666 1795 mem_inj val_inj mi m1 m2 → 1667 1796 mi b = None ? → 1668 store chunk m1 b ofs v = Some ? m1' →1797 store chunk m1 pcl b ofs v = Some ? m1' → 1669 1798 mem_inj val_inj mi m1' m2. 1670 1799 #val_inj; 1671 #mi;#m1;#m2;# b;#ofs;#v;#chunk;#m1';#Hinj;#Hmi;#Hstore;1800 #mi;#m1;#m2;#pcl b ofs;#v;#chunk;#m1';#Hinj;#Hmi;#Hstore; 1672 1801 nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload; 1673 1802 ncut (load chunk0 m1 b1 ofs0 = Some ? v1); … … 1678 1807 1679 1808 nlemma store_outside_inj: ∀val_inj. 1680 ∀mi,m1,m2,chunk, b,ofs,v,m2'.1809 ∀mi,m1,m2,chunk,pcl,b,ofs,v,m2'. 1681 1810 mem_inj val_inj mi m1 m2 → 1682 1811 (∀b',delta. … … 1684 1813 high_bound m1 b' + delta ≤ ofs 1685 1814 ∨ ofs + size_chunk chunk ≤ low_bound m1 b' + delta) → 1686 store chunk m2 b ofs v = Some ? m2' →1815 store chunk m2 pcl b ofs v = Some ? m2' → 1687 1816 mem_inj val_inj mi m1 m2'. 1688 1817 #val_inj; 1689 #mi;#m1;#m2;#chunk;# b;#ofs;#v;#m2';#Hinj;#Hbounds;#Hstore;1818 #mi;#m1;#m2;#chunk;#pcl b ofs;#v;#m2';#Hinj;#Hbounds;#Hstore; 1690 1819 nwhd; #chunk0;#b1;#ofs0;#v1;#b2;#delta; #Hmi0; #Hload; 1691 1820 nlapply (Hinj … Hmi0 Hload);*;#v2;*;#LOAD2;#VINJ; … … 1712 1841 (Or (high_bound m b1 + delta1 ≤ low_bound m b2 + delta2) 1713 1842 (high_bound m b2 + delta2 ≤ low_bound m b1 + delta1)). 1714 1843 *) 1715 1844 (* FIXME *) 1716 1845 nlemma grumpydestruct1 : ∀A,x1,x2. Some A x1 = Some A x2 → x1 = x2. … … 1720 1849 #A;#B;#x1;#y1;#x2;#y2;#H;ndestruct;/2/; 1721 1850 nqed. 1722 1851 (* 1723 1852 nlemma store_mapped_inj: ∀val_inj.∀val_inj_undef:∀mi. val_inj mi Vundef Vundef. 1724 1853 ∀mi,m1,m2,b1,ofs,b2,delta,v1,v2,chunk,m1'. … … 2060 2189 ∀chunk: memory_chunk. ∀m1,m2: mem. ∀b: block. ∀ofs: Z. ∀v: val. 2061 2190 extends m1 m2 → 2062 load chunk m1 b ofs = Some ? v →2063 load chunk m2 b ofs = Some ? v.2064 #chunk;#m1;#m2;# b;#ofs;#v;2191 load chunk m1 pcl b ofs = Some ? v → 2192 load chunk m2 pcl b ofs = Some ? v. 2193 #chunk;#m1;#m2;#pcl b ofs;#v; 2065 2194 *;#Hnext;#Hinj;#LOAD; 2066 2195 nlapply (Hinj … LOAD); ##[ nnormalize; // ## ##2,3: ##] … … 2072 2201 ∀chunk: memory_chunk. ∀m1,m2,m1': mem. ∀b: block. ∀ofs: Z. ∀v: val. 2073 2202 extends m1 m2 → 2074 store chunk m1 b ofs v = Some ? m1' →2075 ∃m2'. store chunk m2 b ofs v = Some ? m2' ∧ extends m1' m2'.2203 store chunk m1 pcl b ofs v = Some ? m1' → 2204 ∃m2'. store chunk m2 pcl b ofs v = Some ? m2' ∧ extends m1' m2'. 2076 2205 #chunk;#m1;#m2;#m1';#b;#ofs;#v;*;#Hnext;#Hinj;#STORE1; 2077 2206 nlapply (store_mapped_inj … Hinj ?? STORE1 ?); … … 2095 2224 extends m1 m2 → 2096 2225 ofs + size_chunk chunk ≤ low_bound m1 b ∨ high_bound m1 b ≤ ofs → 2097 store chunk m2 b ofs v = Some ? m2' →2226 store chunk m2 pcl b ofs v = Some ? m2' → 2098 2227 extends m1 m2'. 2099 2228 #chunk;#m1;#m2;#m2';#b;#ofs;#v;*;#Hnext;#Hinj;#Houtside;#STORE; @; … … 2109 2238 ntheorem valid_pointer_extends: 2110 2239 ∀m1,m2,b,ofs. 2111 extends m1 m2 → valid_pointer m1 b ofs = true →2112 valid_pointer m2 b ofs = true.2240 extends m1 m2 → valid_pointer m1 pcl b ofs = true → 2241 valid_pointer m2 pcl b ofs = true. 2113 2242 #m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID; 2114 2243 nrewrite < (Zplus_z_OZ ofs); … … 2140 2269 nlemma load_lessdef: 2141 2270 ∀m1,m2,chunk,b,ofs,v1. 2142 lessdef m1 m2 → load chunk m1 b ofs = Some ? v1 →2143 ∃v2. load chunk m2 b ofs = Some ? v2 ∧ Val_lessdef v1 v2.2271 lessdef m1 m2 → load chunk m1 pcl b ofs = Some ? v1 → 2272 ∃v2. load chunk m2 pcl b ofs = Some ? v2 ∧ Val_lessdef v1 v2. 2144 2273 #m1;#m2;#chunk;#b;#ofs;#v1;*;#Hnext;#Hinj;#LOAD0; 2145 2274 nlapply (Hinj … LOAD0); ##[ nwhd in ⊢ (??%?); // ## ##2,3:##skip ##] … … 2165 2294 ∀m1,m2,chunk,b,ofs,v1,v2,m1'. 2166 2295 lessdef m1 m2 → Val_lessdef v1 v2 → 2167 store chunk m1 b ofs v1 = Some ? m1' →2168 ∃m2'. store chunk m2 b ofs v2 = Some ? m2' ∧ lessdef m1' m2'.2296 store chunk m1 pcl b ofs v1 = Some ? m1' → 2297 ∃m2'. store chunk m2 pcl b ofs v2 = Some ? m2' ∧ lessdef m1' m2'. 2169 2298 #m1;#m2;#chunk;#b;#ofs;#v1;#v2;#m1'; 2170 2299 *;#Hnext;#Hinj;#Hvless;#STORE0; … … 2257 2386 nlemma valid_pointer_lessdef: 2258 2387 ∀m1,m2,b,ofs. 2259 lessdef m1 m2 → valid_pointer m1 b ofs = true → valid_pointer m2b ofs = true.2388 lessdef m1 m2 → valid_pointer m1 pcl b ofs = true → valid_pointer m2 pcl b ofs = true. 2260 2389 #m1;#m2;#b;#ofs;*;#Hnext;#Hinj;#VALID; 2261 2390 nrewrite < (Zplus_z_OZ ofs); napply (valid_pointer_inj … Hinj VALID); //; … … 2394 2523 mem_inject f m1 m2 → 2395 2524 valid_pointer m1 b (signed ofs) = true → 2396 val_inject f (Vptr b ofs) (Vptr b' ofs') →2525 val_inject f (Vptr pcl b ofs) (Vptr b' ofs') → 2397 2526 valid_pointer m2 b' (signed ofs') = true. 2398 2527 #f;#m1;#m2;#b;#ofs;#b';#ofs'; … … 3433 3562 ##] 3434 3563 nqed. 3435 3564 *) 3436 3565 (* ** Relation between signed and unsigned loads and stores *) 3437 3566 … … 3442 3571 3443 3572 nremark in_bounds_equiv: 3444 ∀chunk1,chunk2,m, b,ofs.∀A:Type.∀a1,a2: A.3573 ∀chunk1,chunk2,m,pcl,b,ofs.∀A:Type.∀a1,a2: A. 3445 3574 size_chunk chunk1 = size_chunk chunk2 → 3446 (match in_bounds m chunk1 b ofs with [ inl _ ⇒ a1  inr _ ⇒ a2]) =3447 (match in_bounds m chunk2 b ofs with [ inl _ ⇒ a1  inr _ ⇒ a2]).3448 #chunk1;#chunk2;#m;# b;#ofs;#A;#a1;#a2;#Hsize;3449 nelim (in_bounds m chunk1 b ofs);3575 (match in_bounds m chunk1 pcl b ofs with [ inl _ ⇒ a1  inr _ ⇒ a2]) = 3576 (match in_bounds m chunk2 pcl b ofs with [ inl _ ⇒ a1  inr _ ⇒ a2]). 3577 #chunk1;#chunk2;#m;#pcl b ofs;#A;#a1;#a2;#Hsize; 3578 nelim (in_bounds m chunk1 pcl b ofs); 3450 3579 ##[ #H; nwhd in ⊢ (??%?); nrewrite > (in_bounds_true … A a1 a2 ?); //; 3451 3580 napply valid_access_compat; //; 3452 ## #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 b ofs); //;3581 ## #H; nwhd in ⊢ (??%?); nelim (in_bounds m chunk2 pcl b ofs); //; 3453 3582 #H'; napply False_ind; napply (absurd ?? H); 3454 3583 napply valid_access_compat; //; … … 3459 3588 storev Mint8signed m a v = storev Mint8unsigned m a v. 3460 3589 #m;#a;#v; nwhd in ⊢ (??%%); nelim a; //; 3461 # b;#ofs; nwhd in ⊢ (??%%);3590 #pcl b ofs; nwhd in ⊢ (??%%); 3462 3591 nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option mem) ???); //; 3463 3592 nqed. … … 3467 3596 storev Mint16signed m a v = storev Mint16unsigned m a v. 3468 3597 #m;#a;#v; nwhd in ⊢ (??%%); nelim a; //; 3469 # b;#ofs; nwhd in ⊢ (??%%);3598 #pcl b ofs; nwhd in ⊢ (??%%); 3470 3599 nrewrite > (in_bounds_equiv Mint16signed Mint16unsigned … (option mem) ???); //; 3471 3600 nqed. … … 3480 3609 loadv Mint8signed m a = option_map ?? (sign_ext 8) (loadv Mint8unsigned m a). 3481 3610 #m;#a; nwhd in ⊢ (??%(????(%))); nelim a; //; 3482 # b;#ofs; nwhd in ⊢ (??%(????%));3611 #pcl b ofs; nwhd in ⊢ (??%(????%)); 3483 3612 nrewrite > (in_bounds_equiv Mint8signed Mint8unsigned … (option val) ???); //; 3484 nelim (in_bounds m Mint8unsigned b (signed ofs)); /2/;3613 nelim (in_bounds m Mint8unsigned pcl b (signed ofs)); /2/; 3485 3614 #H; nwhd in ⊢ (??%%); 3486 3615 nelim (getN 0 (signed ofs) (contents (blocks m b)));
Note: See TracChangeset
for help on using the changeset viewer.