Changeset 2588 for src/Clight/memoryInjections.ma
 Timestamp:
 Jan 23, 2013, 2:38:06 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/memoryInjections.ma
r2578 r2588 464 464 qed. 465 465 466 lemma value_eq_int_inversion' : 467 ∀E,sz,i,v. value_eq E v (Vint sz i) → v = (Vint sz i). 468 #E #sz #i #v #Heq inversion Heq 469 [ 1: #_ #Habsurd destruct (Habsurd) 470  2: #sz #i #Heq #Heq' #_ @refl 471  3: #_ #Habsurd destruct (Habsurd) 472  4: #p1 #p2 #Heq #Heqv #Heqv2 #_ destruct ] 473 qed. 474 466 475 lemma value_eq_null_inversion : 467 476 ∀E,v. value_eq E Vnull v → v = Vnull. 468 477 #E #v #Heq inversion Heq // 469 478 #p1 #p2 #Htranslate #Habsurd lapply (jmeq_to_eq ??? Habsurd) 479 #Habsurd' destruct 480 qed. 481 482 lemma value_eq_null_inversion' : 483 ∀E,v. value_eq E v Vnull → v = Vnull. 484 #E #v #Heq inversion Heq // 485 #p1 #p2 #Htranslate #_ #Habsurd lapply (jmeq_to_eq ??? Habsurd) 470 486 #Habsurd' destruct 471 487 qed. … … 1733 1749 (* value_eq lifts to subtraction *) 1734 1750 lemma sub_value_eq : 1735 ∀E,v1,v2,v1',v2',ty1,ty2 .1751 ∀E,v1,v2,v1',v2',ty1,ty2,target. 1736 1752 value_eq E v1 v2 → 1737 1753 value_eq E v1' v2' → 1738 ∀r1. (sem_sub v1 ty1 v1' ty2 =Some val r1→1739 ∃r2:val.sem_sub v2 ty1 v2' ty2 =Some val r2∧value_eq E r1 r2).1740 #E #v1 #v2 #v1' #v2' #ty1 #ty2 # Hvalue_eq1 #Hvalue_eq2 #r11754 ∀r1. (sem_sub v1 ty1 v1' ty2 target=Some val r1→ 1755 ∃r2:val.sem_sub v2 ty1 v2' ty2 target=Some val r2∧value_eq E r1 r2). 1756 #E #v1 #v2 #v1' #v2' #ty1 #ty2 #target #Hvalue_eq1 #Hvalue_eq2 #r1 1741 1757 @(value_eq_inversion E … Hvalue_eq1) 1742 1758 [  #sz #i  3:  4: #p1 #p2 #Hembed ] 1743 [ 1: whd in match (sem_sub ???? ); normalize nodelta1759 [ 1: whd in match (sem_sub ?????); normalize nodelta 1744 1760 cases (classify_sub ty1 ty2) normalize nodelta 1745 1761 [ #sz #sg  #n #ty #sz #sg  #n #sz #sg #ty #ty1' #ty2' ] 1746 1762 #Habsurd destruct (Habsurd) 1747  2: whd in match (sem_sub ???? ); whd in match (sem_sub????); normalize nodelta1763  2: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta 1748 1764 cases (classify_sub ty1 ty2) normalize nodelta 1749 1765 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] … … 1756 1772  2: #Heq destruct (Heq) normalize nodelta 1757 1773 #Heq destruct (Heq) 1758 /3 by ex_intro, conj, vint_eq/ 1774 /3 by ex_intro, conj, vint_eq/ 1759 1775 ] 1760 1776 (* 3: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta … … 1767 1783 #Heq destruct (Heq) 1768 1784 /3 by ex_intro, conj, vfloat_eq/ *) 1769  3: whd in match (sem_sub ???? ); whd in match (sem_sub????); normalize nodelta1785  3: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta 1770 1786 cases (classify_sub ty1 ty2) normalize nodelta 1771 1787 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] … … 1776 1792 [ 1: @eq_bv_elim [ 1: normalize nodelta #Heq1 #Heq2 destruct /3 by ex_intro, conj, vnull_eq/ 1777 1793  2: #_ normalize nodelta #Habsurd destruct (Habsurd) ] 1778  2: #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ] 1779  4: whd in match (sem_sub ????); whd in match (sem_sub ????); normalize nodelta 1794  2: cases target 1795 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1796  #structname #fieldspec  #unionname #fieldspec  #id ] 1797 normalize nodelta 1798 #Heq destruct (Heq) /3 by ex_intro, conj, vnull_eq/ ] 1799  4: whd in match (sem_sub ?????); whd in match (sem_sub ?????); normalize nodelta 1780 1800 cases (classify_sub ty1 ty2) normalize nodelta 1781 1801 [ 1: #tsz #tsg  2: #tn #ty #tsz #tsg  3: #tn #tsz #tsg #ty  4: #ty1' #ty2' ] … … 1810 1830 cases (eqb (sizeof tsg) O) normalize nodelta 1811 1831 [ 1: #Habsurd destruct (Habsurd) 1812  2: >(sub_offset_translation 32 off1 off1' dest_off) 1813 cases (division_u 31 1814 (sub_offset 32 (offset_plus off1 dest_off) (offset_plus off1' dest_off)) 1815 (repr (sizeof tsg))) 1832  2: cases target 1833 [  #sz #sg  #ptr_ty  #array_ty #array_sz  #domain #codomain 1834  #structname #fieldspec  #unionname #fieldspec  #id ] 1835 normalize nodelta 1836 #Heq destruct (Heq) 1837 <(sub_offset_translation 32 off1 off1' dest_off) 1838 cases (division_u ? 1839 (sub_offset ? off1 off1') 1840 (repr (sizeof tsg))) in Heq; 1816 1841 [ 1: normalize nodelta #Habsurd destruct (Habsurd) 1817  2: #r1' normalize nodelta #Heq2 destruct (Heq2)1842  2: #r1' cases sg normalize nodelta #Heq2 destruct (Heq2) 1818 1843 /3 by ex_intro, conj, vint_eq/ ] 1819 1844 ] ] ] 1820 1845 ] qed. 1821 1822 1846 1823 1847 lemma mul_value_eq : … … 2089 2113 ] qed. 2090 2114 2091 (* /!\ Warning TODO Warning /!\ *)2092 2093 2115 (* Note that x and y are bounded below and above, similarly for the shifted offsets. 2094 2116 This is enough to prove that there is no "wraparoundtheend" problem, 2095 2117 /provided we know that the block bounds are implementable by 2^16 bitvectors/. 2096 We axiomatize it for now. Notice that this axiom is in fact not provable and implies False. 2097 In order to be true, we need to prove that the (x+delta) and (y+delta) do not overflow. 2098 This is provable from the fact that the original pointers in which the offsets reside are "valid". 2099 This in turn is ensured by the memory injection. 2100 /DO NOT USE IT ELSEWHERE, this is just a temporary stopgap./ *) 2118 We axiomatize it for now. *) 2101 2119 axiom cmp_offset_translation : 2102 2120 ∀op,delta,x,y.
Note: See TracChangeset
for help on using the changeset viewer.