Changeset 2594 for src/Clight/memoryInjections.ma
 Timestamp:
 Jan 29, 2013, 8:28:44 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/memoryInjections.ma
r2588 r2594 98 98 (* Lemmas related to freeing memory and pointer validity. *) 99 99 (*  *) 100 (*101 lemma nextblock_free_ok : ∀m,b. nextblock m = nextblock (free m b).102 * #contents #next #posnext * #rg #id103 normalize @refl104 qed.105 106 lemma low_bound_free_ok : ∀m,b,ptr.107 b ≠ (pblock ptr) →108 Zleb (low_bound (free m b) (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) =109 Zleb (low_bound m (pblock ptr)) (Z_of_unsigned_bitvector offset_size (offv (poff ptr))).110 * #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize111 cases prg cases brg normalize nodelta try //112 @(eqZb_elim pid bid)113 [ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??)))114  2,4: #_ #_ @refl115 ] qed.116 117 lemma high_bound_free_ok : ∀m,b,ptr.118 b ≠ (pblock ptr) →119 Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound (free m b) (pblock ptr)) =120 Zleb (Z_of_unsigned_bitvector offset_size (offv (poff ptr))) (high_bound m (pblock ptr)).121 * #contents #next #nextpos * #brg #bid * * #prg #pid #poff normalize122 cases prg cases brg normalize nodelta try //123 @(eqZb_elim pid bid)124 [ 1,3: #Heq >Heq * #Habsurd @(False_ind … (Habsurd (refl ??)))125  2,4: #_ #_ @refl126 ] qed.127 128 lemma valid_pointer_free_ok : ∀b : block. ∀m,ptr.129 valid_pointer m ptr = true →130 pblock ptr ≠ b →131 valid_pointer (free m b) ptr = true.132 * #br #bid * #contents #next #posnext * * #pbr #pbid #poff133 normalize134 @(eqZb_elim pbid bid)135 [ 1: #Heqid >Heqid cases pbr cases br normalize136 [ 1,4: #_ * #Habsurd @(False_ind … (Habsurd (refl ??))) ]137 cases (Zltb bid next) normalize nodelta138 [ 2,4: #Habsurd destruct (Habsurd) ]139 //140  2: #Hneqid cases pbr cases br normalize try // ]141 qed.142 143 lemma valid_pointer_free_list_ok : ∀blocks : list block. ∀m,ptr.144 valid_pointer m ptr = true →145 ¬ mem ? (pblock ptr) blocks →146 valid_pointer (free_list m blocks) ptr = true.147 #blocks148 elim blocks149 [ 1: #m #ptr normalize #H #_ @H150  2: #b #tl #Hind #m #ptr #Hvalid151 whd in match (mem block (pblock ptr) ?);152 >free_list_cons * #Hguard153 @valid_pointer_free_ok154 [ 2: % #Heq @Hguard %1 @Heq ]155 @Hind156 [ 1: @Hvalid157  2: % #Hmem @Hguard %2 @Hmem ]158 ] qed. *)159 160 100 161 101 lemma valid_pointer_ok_free : ∀b : block. ∀m,ptr. … … 367 307 (high_bound m b) + (Zoo delta) < Z_two_power_nat 16 368 308 ]. 369 309 370 310 371 311 (* Adapted from Compcert's Memory *) … … 381 321 (* block_is_empty m b1' ∨ *) 382 322 high_bound m b1 + (Zoo delta1) ≤ low_bound m b2 + (Zoo delta2) ∨ 383 high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) 323 high_bound m b2 + (Zoo delta2) ≤ low_bound m b1 + (Zoo delta1) ∨ 324 block_is_empty m b1 ∨ 325 block_is_empty m b2 384 326  inr Hneq ⇒ True 385 327 ]. … … 393 335 mi_inj : load_sim_ptr E m1 m2; 394 336 (* Invalid blocks are not mapped *) 395 (* mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; *)337 mi_freeblock : ∀b. ¬ (valid_block m1 b) → E b = None ?; 396 338 (* Valid pointers are mapped to valid pointers *) 397 339 mi_valid_pointers : ∀p,p'. … … 427 369 definition empty_injection : memory_inj (λx. None ?) empty empty. 428 370 % 429 [ 1: whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hptr_trans #Hload 430 normalize in Hptr_trans; destruct 431  2: * #b #o #p' #_ normalize #Habsurd destruct 432  3: #b #b' #off #Habsurd destruct 433  4: #b #b' #o' #Habsurd destruct 434  5: whd #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct 435  6: #b whd @I 371 [ whd #b1 #off1 #b2 #off2 #ty #v1 #Hvalid #Hptr_trans #Hload 372 normalize in Hptr_trans; destruct 373  #b #H @refl 374  * #b #o #p' #_ normalize #Habsurd destruct 375  #b #b' #off #Habsurd destruct 376  #b #b' #o' #Habsurd destruct 377  whd #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 destruct 378  #b whd @I 436 379 ] qed. 437 380 … … 709 652 @Hload 710 653  4,5: whd in match (load_value_of_type ????) in Hload ⊢ %; @Hload ] 654  @(mi_freeblock … Hmemory_inj) 711 655  #p #p' #Hvalid #Hptr_trans lapply (mi_valid_pointers … Hmemory_inj p p' Hvalid Hptr_trans) 712 656 elim m2 in Halloc; #contentmap #nextblock #Hnextblock … … 744 688 try assumption ] 745 689 ] qed. 746 (*747  @(eq_block_elim … new_block B)748 [ 2: #H cases m2 in Halloc Hinbounds; #contents #nextblock #notnull749 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)750 >unfold_high_bound in Himpl ⊢ %;751 whd in ⊢ (% → % → %);752 >unfold_low_bound >unfold_high_bound753 whd in match (update_block ?????); >eq_block_b_b754 normalize nodelta * #HA #HB755 >unfold_high_bound756 whd in match (update_block ?????) in ⊢ (% → %);757 >(not_eq_block … (sym_neq ??? H)) normalize nodelta758 try //759  (* absurd case *) #Heq destruct (Heq)760 lapply (Hguard ?? (refl ??)) #Hvalid761 (* hence new_block ≠ B *)762 cases m2 in Halloc Hvalid; #contents #nextblock #notnull763 whd in ⊢ ((??%?) → ?); #Heq destruct (Heq)764 whd in ⊢ (% → ?); #Habsurd765 lapply (irreflexive_Zlt nextblock) *766 #H @False_ind @H @Habsurd767 ]768 ]769 ]770 qed. *)771 690 772 691 … … 786 705 memory_inj E m1' m2. 787 706 788 (* Embed a fresh block inside an unmapped portion of the target 789 block. *)707 (* Embed a fresh block inside an unmapped portion of the target block. 708 * This is the equivalent of lemma 45 for Leroy&Blazy. *) 790 709 axiom alloc_memory_inj_m1_to_m2 : 791 710 ∀E:embedding. … … 829 748 830 749 (* lemma 47 of L&B *) 750 751 lemma free_loadn_sim_ptr_m2 : 752 ∀sz,m,b,b',o,res. 753 b ≠ b' → 754 loadn m (mk_pointer b' o) sz = Some ? res → 755 loadn (free m b) (mk_pointer b' o) sz = Some ? res. 756 #sz 757 elim sz 758 [ normalize // 759  #sz' #Hind #m #b #b' #o #res #Hneq whd in ⊢ ((??%?) → (??%?)); 760 #H cases (some_inversion ????? H) H #beres * 761 #Hbeloadv #Hloadn 762 lapply (beloadv_free_beloadv2 m b ??? Hbeloadv) 763 [ @sym_neq @Hneq ] 764 #Hbeloadv' >Hbeloadv' normalize nodelta 765 cases (some_inversion ????? Hloadn) Hloadn #bevals * #Hloadn 766 #Heq destruct (Heq) 767 >(Hind … Hneq Hloadn) normalize nodelta @refl 768 ] qed. 769 831 770 lemma free_load_sim_ptr_m2 : 832 771 ∀E:embedding. … … 844 783 normalize %{(Vptr (mk_pointer b2 off2))} @conj try @refl 845 784 %4 @Htrans ] 846 #Hload <Hfree 847 (* routine *) 848 @cthulhu 849 qed. 785 lapply Htrans Htrans lapply Hsim Hsim lapply Hfree Hfree 786 cases m2 #contents2 #next2 #Hnext2 787 whd in ⊢ ((??%?) → ?); #Hm2' destruct 788 #Hsim #Htrans 789 cases (some_inversion ????? Htrans) * #b2' #off2' * #Hembed normalize nodelta 790 #Heq destruct (Heq) #Hload 791 lapply (Hsim … Hvalid … Htrans … Hload) 792 * #v2' * #Hload_before_free #Hvalue_eq 793 @(eq_block_elim … b2 b) 794 [ 1,3,5: #Heq destruct 795 lapply (Hunmapped b1 off2' Hembed) * 796 [ 1,3,5: #Hnot_valid lapply (valid_pointer_to_Prop … Hvalid) 797 Hvalid whd in match (valid_block ??) in Hnot_valid; 798 * * #Hvalid #_ #_ @False_ind 799 cases Hnot_valid #H @H @Hvalid 800  *: whd in ⊢ (% → ?); #Hempty 801 lapply (valid_pointer_to_Prop … Hvalid) 802 Hvalid * * #_ #Hlow #Hhigh 803 cut ((low_bound m1 b1 < high_bound m1 b1)) 804 [ 1,3,5: /2 by Zle_to_Zlt_to_Zlt, Zlt_to_Zle_to_Zlt/ ] 805 #Hnonempty @False_ind Hlow Hhigh 806 lapply (Zlt_to_Zle_to_Zlt … Hnonempty Hempty) 807 #H cases (irreflexive_Zlt (low_bound m1 b1)) #H' @H' @H ] 808  *: #Hneq %{v2'} @conj try assumption 809 whd in match (load_value_of_type ????) in Hload_before_free:(??%?) ⊢ (??%?); 810 cases (some_inversion ????? Hload_before_free) Hload_before_free 811 #bevals * #Hloadn #Heq 812 >(free_loadn_sim_ptr_m2 … Hloadn) normalize nodelta 813 try assumption @sym_neq @Hneq 814 ] qed. 850 815 851 816 lemma free_block_is_empty : … … 864 829 qed. 865 830 831 lemma high_bound_freed_block : 832 ∀m,b. high_bound (free m b) b = OZ. 833 #m #b normalize 834 cases (block_region b) normalize 835 >eqZb_z_z normalize @refl 836 qed. 837 838 lemma low_bound_freed_block : 839 ∀m,b. low_bound (free m b) b = (pos one). 840 #m #b normalize 841 cases (block_region b) normalize 842 >eqZb_z_z normalize @refl 843 qed. 844 866 845 (* Lemma 49 in Leroy&Blazy *) 867 axiomfree_non_aliasing_m1 :846 lemma free_non_aliasing_m1 : 868 847 ∀E:embedding. 869 848 ∀m1,m2,m1'. … … 873 852 (* The proof proceeds by a first case analysis to see wether b lives in the 874 853 same world as the nonaliasing blocks (if not : trivial), in this case 875 we proceed by a case analysis on the nonaliasing hypothesis in memory_inj. *) 876 854 we proceed to a second case analysis on the nonaliasing hypothesis in 855 memory_inj. *) 856 #E #m1 #m2 #m1' #Hinj #b #Hfree 857 whd 858 #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq 859 #Hembed1 #Hembed2 860 cases (block_decidable_eq ??) normalize nodelta 861 [ 2: try // ] 862 #Hblocks_eq destruct (Hblocks_eq) 863 lapply Hembed1 Hembed1 864 lapply Hembed2 Hembed2 865 generalize in match b2'; 866 #target #Hembed2 #Hembed1 867 lapply (mi_nonalias … Hinj … Hneq Hembed1 Hembed2) 868 cases (block_decidable_eq ??) 869 [ 2: * #Habsurd @False_ind @Habsurd @refl ] #Hrefl 870 normalize nodelta <Hfree 871 @(eq_block_elim … b1 b) 872 [ #Heq destruct (Heq) #Hcase 873 %1 %2 whd 874 >high_bound_freed_block >low_bound_freed_block 875 // 876  #Hneq1 @(eq_block_elim … b2 b) 877 [ #Heq destruct (Heq) #Hcase 878 %2 whd 879 >high_bound_freed_block >low_bound_freed_block 880 // ] ] 881 #Hneq2 882 >unfold_high_bound >unfold_high_bound >unfold_high_bound >unfold_high_bound 883 >unfold_low_bound >unfold_low_bound >unfold_low_bound >unfold_low_bound 884 <(high_free_eq … Hneq1) <(high_free_eq … Hneq2) 885 <(low_free_eq … Hneq1) <(low_free_eq … Hneq2) 886 * 887 [ 2: #H %2 whd >unfold_high_bound >unfold_low_bound 888 <(low_free_eq … Hneq2) <(high_free_eq … Hneq2) @H ] 889 * 890 [ 2: #H %1%2 whd >unfold_high_bound >unfold_low_bound 891 <(low_free_eq … Hneq1) <(high_free_eq … Hneq1) @H ] 892 * #H 893 [ %1 %1 %1 @H 894  %1 %1 %2 @H ] 895 qed. 877 896 878 897 (* Extending lemma 46 and 49 to memory injections *) … … 885 904 #E #m1 #m2 #m1' #Hinj #b #Hfree 886 905 cases Hinj 887 #Hload_sim #H valid #Hnodangling #Hregion #Hnonalias #Himplementable906 #Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himplementable 888 907 % try assumption 889 908 [ @(free_load_sim_ptr_m1 … Hload_sim … Hfree) 909  #bb #Hnot_valid lapply (Hfreeblock bb) #HA @HA % #HB 910 cases Hnot_valid #HC @HC <Hfree @HB 890 911  #p #p' #Hvalid_m1' #Hptr_translation @(Hvalid p p' ? Hptr_translation) 891 912 <Hfree in Hvalid_m1'; @valid_free_to_valid … … 908 929 normalize nodelta try @conj try // % try // 909 930 ] 910 ] qed. 911 912 (* 913 #b0 #b' #o' #Hembed lapply (Himplementable b0 b' o' Hembed) * 914 #HA #HB @conj try // 915 cases m1 in Hfree HA; #contents1 #nextblock1 #Hpos1 916 whd in ⊢ ((??%%) → ? → ?); #Heq destruct (Heq) 917 whd in ⊢ (% → %); * 918 whd in match (low_bound ??) in ⊢ (% → % → %); 919 whd in match (high_bound ??) in ⊢ (% → % → %); #HA #HB 920 @(eq_block_elim … b0 b) 921 [ #H whd in match (update_block ?????); >H >eq_block_b_b @conj 922 normalize nodelta 923 normalize @conj try // 924  #H whd in match (update_block ?????); >(not_eq_block … H) @conj 925 try // ] ] 926 qed.*) 927 928 (* Lifting lemma 47 to memory injs *) 931 ] qed. 932 933 (* Lifting lemma 47 to memory injs  note that we require a much stronger condition 934 * on the freed block : no block of m1 can map to it. Not even an invalid block or 935 * an empty one. 936 * XXX this lemma is not given in Leroy&Blazy, and unless future developments requires 937 * it I will comment it out. XXX *) 929 938 lemma free_memory_inj_m2 : 930 939 ∀E:embedding. … … 932 941 memory_inj E m1 m2 → 933 942 ∀b. free m2 b = m2' → 934 (∀b1,delta. E b1 = Some ? 〈b, delta〉 → ¬ (valid_block m1 b1) ∨ block_is_empty m1 b1) → 943 (∀b1,delta. E b1 = Some ? 〈b, delta〉 → 944 (¬ (valid_block m1 b1)) ∨ block_is_empty m1 b1) → 935 945 memory_inj E m1 m2'. 936 #E #m1 #m2 #m2' #Hinj #b #Hfree #b 1_not_mapped946 #E #m1 #m2 #m2' #Hinj #b #Hfree #b_not_mapped 937 947 % cases Hinj try // 938 #Hload_sim #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl 939 [ (* We succed performing a load from m1. Case analysis: if byvalue, cannot map to freed block [b] 940 (otherwise contradiction), hence simulation proceeds through Hinj. 941 If not byvalue, then simulation proceeds without examining the contents of the memory *) 942 @cthulhu 943  #p #p' #Hvalid #Hptr_trans 944 (* We now through Hinj that valid_pointer m2 p'=true, 945 if (pblock p') = b then using b1_not_mapped and Hptr_trans we 946 know that the original pointer must be either invalid or empty, 947 hence contradiction with Hvalid 948 if (pblock p') ≠ b then straightforward simulation *) 949 @cthulhu 950  #bb #b' #o' #Hembed 951 lapply (Hnodangling bb b' o' Hembed) #Hvalid_before_free 952 (* cf case above *) 953 @cthulhu 948 #Hload_sim #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl 949 [ @(free_load_sim_ptr_m2 … Hload_sim … Hfree) #b1 #delta #Hembed 950 @(b_not_mapped … b1 delta Hembed) 951  @Hfreeblock 952  * #bp #op #p' #Hp_valid #Hptr_trans 953 @(eq_block_elim … (pblock p') b) 954 [ #Heq lapply (Hvalid … Hp_valid Hptr_trans) #Hp_valid' destruct (Heq) 955 cases (some_inversion ????? Hptr_trans) 956 * #bp' #op' * #Hembed normalize nodelta #Heq destruct (Heq) 957 cases (b_not_mapped … Hembed) 958 [ #Hnot_valid lapply (Hfreeblock … Hnot_valid) >Hembed #Habsurd destruct (Habsurd) 959  #Hempty @False_ind lapply (valid_pointer_to_Prop … Hp_valid) * * #_ 960 whd in Hempty; #Hle #Hlt 961 lapply (Zlt_to_Zle_to_Zlt … Hlt Hempty) #Hlt2 962 lapply (Zlt_to_Zle_to_Zlt … Hlt2 Hle) #Hlt3 963 @(absurd … Hlt3 (irreflexive_Zlt ?)) ] 964  #Hneq lapply (Hvalid … Hp_valid Hptr_trans) <Hfree #HA 965 @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … HA) HA * * 966 #HA #HB #HC @conj try @conj try assumption 967 [ >unfold_low_bound <(low_free_eq m2 ?? Hneq) @HB 968  >unfold_high_bound <(high_free_eq m2 ?? Hneq) @HC ] 969 ] 970  #bb #b' #o' #Hembed 971 lapply (Hnodangling … Hembed) <Hfree // 954 972  @Hregion 955 973  #bb lapply (Himpl bb) … … 964 982 #H [ 1,3,5: destruct (H) normalize nodelta try // 965 983 @conj try // 966  *: normalize nodelta cases HBLO try // ] 984  *: normalize nodelta cases HBLO try // ] 967 985 ] qed. 968 986 … … 978 996 free_list m1 blocklist = m1' → 979 997 memory_inj E m1' m2'. 980 (* nothing particular here, application of various lemmas and induction over blocklist. *) 981 @cthulhu 982 qed. 998 #E #m1 #m2 #m1' #m2' #Hinj #blocklist #b2 #Hnot_mapped #Hfree2 #Hfree_list 999 cut (memory_inj E m1' m2) 1000 [ <Hfree_list Hfree_list 1001 Hnot_mapped 1002 lapply Hinj Hinj 1003 lapply m1 m1 1004 elim blocklist 1005 [ #m1 #Hinj @Hinj 1006  #hd #tl #Hind #m1 #Hinj 1007 @(free_memory_inj_m1 ? (free_list m1 tl) ? (free (free_list m1 tl) hd) ? hd) 1008 try @refl @(Hind … Hinj) 1009 ] 1010 ] 1011 #Hinj' 1012 @(free_memory_inj_m2 … Hinj' … Hfree2) 1013 #b1 #delta #Hembed %2 1014 lapply (Hnot_mapped … Hembed) 1015 lapply Hfree_list Hfree_list 1016 generalize in match m1'; 1017 generalize in match m1; 1018 elim blocklist 1019 [ #m1 #m1' whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) @False_ind 1020  #hd #tl #Hind #m1 #m1' #Hfree_list * 1021 [ #Heq destruct whd 1022 whd in match (free_list ??); 1023 >unfold_high_bound >unfold_low_bound 1024 whd in match (update_block ?????); >eq_block_b_b 1025 normalize nodelta @I 1026  >free_list_cons in Hfree_list; #Hfree_list #H 1027 <Hfree_list whd cases m1 #contents2 #n2 #Hn2 1028 >unfold_high_bound >unfold_low_bound 1029 whd in match (update_block ?????); 1030 @(eq_block_elim … b1 hd) 1031 [ #Heq normalize nodelta @I 1032  #Hneq normalize nodelta @(Hind … (mk_mem contents2 n2 Hn2) … (refl ??) … H) 1033 ] 1034 ] 1035 ] qed. 983 1036 984 1037 (*  *) … … 1232 1285 #E #mA #mB #mC #Hinj #block2 #i #ty #Hout #v #Hstore % 1233 1286 lapply (bestorev_memory_inj_to_load_sim … Hinj … Hout … Hstore) #Hsim try // 1234 cases Hinj #Hsim' #H valid #Hnodangling #Hregion #Hnonalias #Himpl try assumption1287 cases Hinj #Hsim' #Hfreeblock #Hvalid #Hnodangling #Hregion #Hnonalias #Himpl try assumption 1235 1288 [ 1236 1289 #p #p' #Hptr #Hptr_trans lapply (Hvalid p p' Hptr Hptr_trans) #Hvalid … … 1418 1471 (* This lemma is not provable as in CompCert. In the following chunk of text, I'll try to 1419 1472 * explain why, and how we might still be able to prove it given enough time. 1420 I'll be refering to paper by Leroy & Blazy in the J.A.R.1473 I'll be refering to a paper by Leroy & Blazy in the J.A.R. 1421 1474 In CompCert, when storing some data of size S in some location 〈block, offset〉, 1422 1475 what happens is that … … 1428 1481 value fv, the story is the following : 1429 1482 1) the value fv is marshalled into a list of backend values (bytesized) which correspond 1430 to the actual size of the data inmemory. This list is then stored asis at the1483 to the actual size of the data inmemory. 2) This list is then stored asis at the 1431 1484 location 〈block, offset〉. 1432 1485 … … 1522 1575 load_sim_ptr E m1' m2. 1523 1576 #E #m1 #m2 #m1' #Hinj #ty #b #i #v #Hembed #Hstore 1524 cases Hinj #Hsim #H valid #Hnodangling #Hregion_eq #Hnonalias #Himpl1577 cases Hinj #Hsim #Hfreeblock #Hvalid #Hnodangling #Hregion_eq #Hnonalias #Himpl 1525 1578 cases ty in Hstore; 1526 1579 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain … … 1562 1615 #Hload @(Hsim … Hembed' … Hload) 1563 1616 @(load_by_value_success_valid_pointer … Hload) // 1564 ] qed. 1617 ] qed. 1565 1618 1566 1619 lemma store_value_of_type_memory_inj : … … 1574 1627 % 1575 1628 [ 1: @(store_value_of_type_load_sim … Hinj … Hnot_mapped … Hstore) 1576  *: (* writing doesn't alter the bound, straightforward *) @cthulhu ] 1577 qed. (* TODO *) 1629  *: lapply (mem_bounds_after_store_value_of_type … Hstore) 1630 * #H1 #H2 1631 [ #b * #Hnot_valid @(mi_freeblock ??? Hinj) 1632 % #H @Hnot_valid whd in H:% ⊢ %; >H1 @H 1633  #p #p' #Hvalid @(mi_valid_pointers ??? Hinj) 1634 @valid_pointer_of_Prop lapply (valid_pointer_to_Prop … Hvalid) 1635 >H1 cases (H2 (pblock p)) #HA #HB 1636 >unfold_high_bound >unfold_low_bound 1637 >unfold_high_bound >unfold_low_bound 1638 >HA >HB // 1639  @(mi_nodangling … Hinj) 1640  @(mi_region … Hinj) 1641  whd #b1 #b2 #b1' #b2' #delta1 #delta2 #Hneq #Hembed1 #Hembed2 1642 whd in match (block_is_empty ??); 1643 whd in match (block_is_empty m1' b2); 1644 >unfold_high_bound >unfold_low_bound 1645 >unfold_high_bound >unfold_low_bound 1646 cases (H2 b1) #HA #HB 1647 cases (H2 b2) #HC #HD 1648 >HA >HB >HC >HD 1649 @(mi_nonalias ??? Hinj) assumption 1650  #bb whd 1651 lapply (mi_nowrap ??? Hinj bb) whd in ⊢ (% → ?); 1652 cases (E bb) normalize nodelta try // * #bb' #off 1653 normalize nodelta 1654 whd in match (block_implementable_bv ??); 1655 whd in match (block_implementable_bv m2 bb'); 1656 whd in match (block_implementable_bv m1' bb); 1657 >unfold_high_bound >unfold_low_bound 1658 >unfold_high_bound >unfold_low_bound 1659 >unfold_high_bound 1660 cases (H2 bb) #HA #HB 1661 >HA >HB // 1662 ] 1663 ] qed. 1578 1664 1579 1665 (*  *) … … 2251 2337 cases (E bq1) [ 1: #_ #_ #_ normalize nodelta #Habsurd destruct (Habsurd) ] 2252 2338 * #BLOq #DELTAq normalize nodelta 2253 cases (E bp1) [ 1: #_ #_ #_ normalize nodelta#_ #Habsurd destruct (Habsurd) ]2339 cases (E bp1) [ 1: normalize nodelta #_ #_ #_ #_ #Habsurd destruct (Habsurd) ] 2254 2340 * #BLOp #DELTAp normalize nodelta #Hnowrap1 #Hnowrap2 #H #Heq1 #Heq2 destruct 2255 2341 cases op … … 2260 2346 #H 2261 2347 [ 2: #_ >(not_eq_block … H) normalize nodelta %{Vfalse} @conj try @refl %2 2262  4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ] 2348  4: #_ >(not_eq_block … H) normalize nodelta >(not_eq_block … H) normalize nodelta %{Vtrue} @conj try @refl %2 ] 2263 2349 destruct (H) generalize in match BLOq in Hnowrap1 Hnowrap2 Hvalid2 Hvalid2' ⊢ %; 2264 2350 #target_block * * #Himplq1 #Himpltarget #Hnowrap_q1 … … 2268 2354 * * #_ #Hlowq #Hhighq * * #_ #Hlowp #Hhighp 2269 2355 >eq_block_b_b normalize nodelta 2356 * 2357 [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind 2358 cases (valid_pointer_to_Prop … Hvalid') * #_ #Hle #Hlt 2359 lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt' 2360 lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl 2361 @(absurd … Hlt_refl (irreflexive_Zlt ?)) ] 2362 * 2363 [ 2,4: whd in ⊢ (% → ?); #Habsurd @False_ind 2364 cases (valid_pointer_to_Prop … Hvalid) * #_ #Hle #Hlt 2365 lapply (Zlt_to_Zle_to_Zlt … Hlt Habsurd) #Hlt' 2366 lapply (Zlt_to_Zle_to_Zlt … Hlt' Hle) #Hlt_refl 2367 @(absurd … Hlt_refl (irreflexive_Zlt ?)) ] 2270 2368 * 2271 2369 #Hdisjoint
Note: See TracChangeset
for help on using the changeset viewer.