Changeset 3178 for src/Clight/toCminorCorrectness.ma
 Timestamp:
 Apr 25, 2013, 6:03:24 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r3170 r3178 1747 1747 #A #B #C * #a #b #Q #x normalize #E1 %{a} %{b} % try @refl @E1 qed. 1748 1748 1749 lemma pair_as_elim: 1750 ∀A,B,C: Type[0]. 1751 ∀p. 1752 ∀T: ∀a:A. ∀b:B. 〈a,b〉 = p → C. 1753 ∀P: A×B → C → Prop. 1754 (∀lft, rgt. ∀E:〈lft,rgt〉 = p. P 〈lft,rgt〉 (T lft rgt E)) → 1755 P p (let 〈lft, rgt〉 as E ≝ p in T lft rgt E). 1756 #A #B #C * /2/ 1757 qed. 1758 1759 (* TODO: move *) 1760 lemma alloc_low_bound : ∀m,l,h,m',b. 1761 alloc m l h = 〈m',b〉 → 1762 low_bound m' b = l. 1763 * #contents #next #next_ok #l #h #m' #b #E 1764 whd in E:(??%%); destruct 1765 whd in ⊢ (??%?); >update_block_s 1766 % 1767 qed. 1768 1769 lemma alloc_high_bound : ∀m,l,h,m',b. 1770 alloc m l h = 〈m',b〉 → 1771 high_bound m' b = h. 1772 * #contents #next #next_ok #l #h #m' #b #E 1773 whd in E:(??%%); destruct 1774 whd in ⊢ (??%?); >update_block_s 1775 % 1776 qed. 1777 1778 (* Weaker version of Zlt_to_Zle *) 1779 lemma Zlt_Zle : ∀x,y:Z. x < y → x ≤ y. 1780 #x #y #H 1781 @(transitive_Zle … (Zsucc_le x)) @Zlt_to_Zle @H 1782 qed. 1783 1784 axiom unZoo : ∀off:Z. 1785 off < Z_two_power_nat 16 → 1786 Zoo (offset_of_Z off) = off. 1787 1788 lemma le_to_Zle : ∀x,y:nat. le x y → Zle x y. 1789 #x #y #H @(le_ind ????? H) 1790 [ // 1791  #m #H1 #H2 >Zsucc_pos @(transitive_Zle … (Zsucc_le m)) assumption 1792 ] qed. 1793 1794 lemma lt_to_Zlt : ∀x,y:nat. lt x y → Zlt x y. 1795 #x #y whd in ⊢ (% → ?); #H 1796 <(Zpred_Zsucc x) @Zle_to_Zlt 1797 <Zsucc_pos 1798 @le_to_Zle assumption 1799 qed. 1800 1801 lemma Zlt_Zsucc : ∀z:Z. z < Zsucc z. 1802 /2/ 1803 qed. 1804 1805 lemma Zle_Zlt_Zsucc : ∀x,y:Z. x ≤ y → x < Zsucc y. 1806 /2/ 1807 qed. 1808 1809 theorem Zle_to_Zlt_to_Zlt: ∀n,m,p:Z. n ≤ m → m < p → n < p. 1810 #n #m #p #Hle #Hlt lapply (Zlt_to_Zle … Hlt) 1811 @Zlt_to_Zle_to_Zlt @Zle_Zlt_Zsucc assumption 1812 qed. 1813 1814 1815 (* This roughly corresponds to lemma 69 of Leroy and Blazy *) 1816 (* 1817 lemma alloc_vars_rel : ∀vartypes, cl_m, cm_m, stacksize, cm_m1, cm_frame. 1818 ∀Em. memory_inj Em cl_m cm_m → 1819 Z_of_nat stacksize < Z_two_power_nat 16 → 1820 alloc cm_m O (Z_of_nat stacksize) = 〈cm_m1,cm_frame〉 → 1821 ∀L, cl_env, cl_m1. 1822 exec_alloc_variables empty_env cl_m L = 〈cl_env,cl_m1〉 → 1823 (∀v,ty. Exists … (λx.x = 〈v,ty〉) L → ∃c. lookup' vartypes v = return 〈c,ty〉 ∧ 1824 match c with 1825 [ Local ⇒ True 1826  Stack off ⇒ 1827 le O off ∧ le (sizeof ty + off) stacksize ∧ 1828 (∀v',off',t'. v≠v' → lookup' vartypes v' = return 〈Stack off',t'〉 → le (off' + sizeof t') off ∨ le (off + sizeof ty) off') 1829  Global _ ⇒ False 1830 ]) → 1831 ∃Em'. memory_inj Em' cl_m1 cm_m1 ∧ 1832 embedding_compatible Em Em' ∧ 1833 ∀v. Exists … (λx.\fst x = v) L → 1834 ∃b,c,t. lookup … cl_env v = Some ? b ∧ 1835 lookup' vartypes v = return 〈c,t〉 ∧ 1836 match c with 1837 [ Local ⇒ Em' b = None ? 1838  Stack off ⇒ Em' b = Some ? 〈cm_frame, offset_of_Z (Z_of_nat off)〉 1839  Global _ ⇒ False 1840 ]. 1841 #vartypes #cl_m #cm_m #stacksize #cm_m1 #cm_frame #Em #Inj #stack_ok #cm_alloc #L 1842 cut (block_implementable_bv cm_m1 cm_frame) 1843 [ whd >(alloc_low_bound … cm_alloc) >(alloc_high_bound … cm_alloc) % % // 1844 cases stacksize // ] #cm_bi 1845 lapply (alloc_memory_inj_m2 … Inj cm_alloc cm_bi) 1846 lapply (alloc_valid_new_block … cm_alloc) #cm_frame_valid 1847 cut (∀b:block. ∀delta':offset. 1848 Em b=Some (block×offset) 〈cm_frame,delta'〉 → 1849 ∀v,off,ty. lookup' vartypes v = OK ? 〈Stack off, ty〉 → 1850 high_bound cl_m b+Zoo delta'≤O+Zoo (offset_of_Z off) 1851 ∨ sizeof ty+Zoo (offset_of_Z off)≤low_bound cl_m b+Zoo delta') 1852 [ #b #delta' #E @⊥ lapply (mi_nodangling … Inj … E) #V 1853 @(absurd … V) @(new_block_invalid_before_alloc … cm_alloc) ] 1854 1855 generalize in match Em; Em generalize in match empty_env; elim L 1856 [ #cl_env #Em #_ #Inj #cl_env' #cl_m1 #cl_alloc 1857 whd in cl_alloc:(??%%); destruct #H 1858 %{Em} % [ % [ @Inj  // ]  #v * ] 1859  * #v #ty #tl #IH 1860 #cl_env #Em #Hexisting #Inj #cl_env' #cl_m1 1861 whd in ⊢ (??%? → ?); @pair_elim #cl_m2 #cl_b #cl_alloc #cl_alloc' #H 1862 cases (H v ty ?) [2: %1 % ] * 1863 [ #r * #L * 1864  #off * #L * * #off_low #off_high #other 1865 lapply (alloc_memory_inj_m1_to_m2 … (offset_of_Z off) cm_frame_valid … cm_bi … cl_alloc … Inj) 1866 [ #b #delta' #NE #E @(Hexisting … E … L) 1867  cases (alloc_properties … cm_alloc) #_ #U #i #LOW #HIGH @U 1868 [ /2/ 1869  @(transitive_Zle … HIGH) >unZoo 1870 [ <eq_plus_Zplus /2/ 1871  @(Zlt_to_Zle_to_Zlt ? (sizeof ty + off)) 1872 [ <eq_plus_Zplus @lt_to_Zlt whd in ⊢ (??%); /2/ 1873  @(transitive_Zlt … stacksize) [ <eq_plus_Zplus @(lt_to_Zlt … off_high)  // ] 1874 ] 1875 ] 1876 ] 1877  >unZoo 1878 [ <eq_plus_Zplus >(alloc_high_bound … cm_alloc) 1879 *) 1749 1880 (* 1750 1881 lemma lset_inclusion_Exists : … … 1790 1921 subtrace corresponding to a measurable Clight subtrace. 1791 1922 *) 1792 (* WIP 1923 (* WIP 1924 include "common/ExtraMonads.ma". 1925 1793 1926 lemma clight_cminor_call : 1794 1927 ∀g,g'. … … 1831 1964 whd in STEP1:(??%%); destruct ] 1832 1965 cl_fd 1966 (* and the Cminor one must be Internal *) 1967 @('bind_inversion Htranslate) #cm_f #Htranslate' #E 1968 whd in E:(??%%); destruct 1969 1970 (* Invert function translation *) 1971 (* NB: if you want to examine the proof state in here, you probably want to 1972 turn off the pretty printer  it doesn't cope well with a large proof 1973 term. *) 1974 @('bind_inversion Htranslate') * * #lbls #Ilbls #ul #Hbuild_label_env 1975 whd in ⊢ (??%? → ?); 1976 @pair_as_elim #vartypes #stacksize #Hcharacterise 1977 letin uv ≝ (mk_tmpgen ?? [ ] ??) #H 1978 @('bind_inversion H) H #s0 #Htranslate_statement #H 1979 @('bind_inversion H) H * * #fgens #s1 #Is #Halloc_params 1980 letin cm_params ≝ (map ??? (fn_params cl_f)) 1981 whd in ⊢ (??%? → ?); 1982 letin cm_vars ≝ (map ??? (?@fn_vars cl_f)) #H 1983 @('bind_inversion H) H #D #Hcheck_distinct_env 1984 whd in ⊢ (??%% → ?); generalize in ⊢ (??(??(???????%))? → ?); 1985 (* It's safe to use the pretty printer again. *) 1986 #cm_Sinv #H destruct 1833 1987 1834 1988 (* Invert Clight STEP1 *) … … 1836 1990 cases (bindIO_inversion ??????? STEP1) STEP1 #cl_m2 * #BIND #STEP1 1837 1991 whd in STEP1:(??%%); destruct 1992 1993 whd whd in ⊢ (??%?); 1994 @pair_elim #cm_m1 #cm_frame #CM_ALLOC 1995 1996 (〈vartypes,stacksize〉=characterise_vars (globals g g' INV) cl_f) 1997 We need to build an extended memory injection to reflect the new allocations; 1998 then the bind functions put the correct local variables in; 1999 then after execution the appropriate number of Cminor steps the stored values 2000 match. 2001 2002 Oh, and there are the locals too. 2003 2004 2005 alloc_memory_inj_m2 shows that embedding is fine after the Cminor alloc 2006 2007 ∀Em. memory_inj Em cl_m cm_m → 2008 (∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) → 2009 exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env,cl_m1〉 → 2010 alloc cm_m O (f_stacksize cm_f) = 〈cm_m1,cm_frame〉 → 2011 ∃Em'. 2012 memory_inj Em' cl_m1 cm_m1 ∧ 2013 (∀b. block_region b = Code → Em' b = Some ? 〈b,zero_offset〉) ∧ 2014 (∀v,v'. value_eq Em v v' → value_eq Em' v v') ∧ 2015 (∀b1.∀delta. Em' b1=Some ? 〈cm_frame,delta〉 → 2016 mem block b1 (blocks_of_env cl_env)). 2017 2018 ∀b. Em b = Em' b ∨ (Em b = None ? ∧ ∃off. Em' b = Some ? 〈cm_frame,off〉). 2019 2020 2021 translate_function func_univ (globals … INV) cl_f H1 H2 = return cm_f → 2022 All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args → 2023 exec_bind_parameters cl_env cl_m1 (fn_params cl_f) cl_args = return cl_m2 → 2024 ∃cm_en,Hcm_args_present. 2025 bind_params cm_args (f_params cm_f) = return «cm_en, Hcm_args_present» ∧ 2026 2027 1838 2028 *) 1839 2029
Note: See TracChangeset
for help on using the changeset viewer.