Changeset 3237
 Timestamp:
 Apr 30, 2013, 7:02:53 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/toCminorCorrectness.ma
r3178 r3237 1812 1812 qed. 1813 1813 1814 lemma Zlt_to_not_Zle : ∀x,y:Z. x < y → y ≰ x. 1815 * [2,3: #p] * [2,3,5,6:#q] /2/ 1816 @lt_to_not_le 1817 qed. 1818 1819 lemma Zlt_to_Zleb_false : ∀x,y:Z. x < y → Zleb y x = false. 1820 #x #y #H 1821 lapply (Zleb_true_to_Zle y x) cases (Zleb ??) // #H' 1822 @⊥ @(absurd … (H' (refl ??))) 1823 @(Zlt_to_not_Zle … H) 1824 qed. 1825 1826 1827 lemma alloc_region : ∀m,l,h,m',b. 1828 alloc m l h = 〈m',b〉 → 1829 block_region b = XData. 1830 * #ct #n #nO #l #h #m' #b #A whd in A:(??%%); destruct 1831 whd in ⊢ (??%?); 1832 >(Zlt_to_Zleb_false … nO) % 1833 qed. 1834 1835 lemma alloc_other_high_bound : ∀m,l,h,m',b,b'. 1836 b ≠ b' → 1837 alloc m l h = 〈m',b〉 → 1838 high_bound m b' = high_bound m' b'. 1839 * #contents #next #next_ok #l #h #m' #b #b' #NE #ALLOC 1840 whd in ALLOC:(??%%); destruct 1841 whd in ⊢ (??%%); 1842 >update_block_o // 1843 qed. 1844 1845 lemma alloc_other_low_bound : ∀m,l,h,m',b,b'. 1846 b ≠ b' → 1847 alloc m l h = 〈m',b〉 → 1848 low_bound m b' = low_bound m' b'. 1849 * #contents #next #next_ok #l #h #m' #b #b' #NE #ALLOC 1850 whd in ALLOC:(??%%); destruct 1851 whd in ⊢ (??%%); 1852 >update_block_o // 1853 qed. 1854 1855 lemma alloc_vars_env : ∀v,L,env,m,env',m'. 1856 All ? (λia. v ≠ \fst ia) L → 1857 exec_alloc_variables env m L = 〈env',m'〉 → 1858 lookup … env v = lookup … env' v. 1859 #v #L elim L 1860 [ #env #m #env' #m' #_ #A whd in A:(??%%); destruct % 1861  * #id #ty #tl #IH 1862 #env #m #env' #m' * #NE #D whd in ⊢ (??%% → ?); 1863 cases (alloc ???) #m1 #b1 #A 1864 <(IH … A) 1865 >(lookup_add_miss … env v id) /2/ 1866 ] qed. 1867 1868 lemma embedding_compatible_trans : ∀E1,E2,E3. 1869 embedding_compatible E1 E2 → 1870 embedding_compatible E2 E3 → 1871 embedding_compatible E1 E3. 1872 #E1 #E2 #E3 #C1 #C2 #v 1873 cases (C1 v) 1874 [ /2/ 1875  #E >E @C2 1876 ] qed. 1814 1877 1815 1878 (* This roughly corresponds to lemma 69 of Leroy and Blazy *) 1816 (* 1879 1817 1880 lemma alloc_vars_rel : ∀vartypes, cl_m, cm_m, stacksize, cm_m1, cm_frame. 1818 1881 ∀Em. memory_inj Em cl_m cm_m → … … 1820 1883 alloc cm_m O (Z_of_nat stacksize) = 〈cm_m1,cm_frame〉 → 1821 1884 ∀L, cl_env, cl_m1. 1885 distinct_env … L → 1822 1886 exec_alloc_variables empty_env cl_m L = 〈cl_env,cl_m1〉 → 1823 1887 (∀v,ty. Exists … (λx.x = 〈v,ty〉) L → ∃c. lookup' vartypes v = return 〈c,ty〉 ∧ … … 1835 1899 lookup' vartypes v = return 〈c,t〉 ∧ 1836 1900 match c with 1837 [ Local ⇒ Em' b = None ?1901 [ Local ⇒ True (*Em' b = None ?*) 1838 1902  Stack off ⇒ Em' b = Some ? 〈cm_frame, offset_of_Z (Z_of_nat off)〉 1839 1903  Global _ ⇒ False 1840 1904 ]. 1841 1905 #vartypes #cl_m #cm_m #stacksize #cm_m1 #cm_frame #Em #Inj #stack_ok #cm_alloc #L 1906 (* Deal with Cminor allocation *) 1842 1907 cut (block_implementable_bv cm_m1 cm_frame) 1843 1908 [ whd >(alloc_low_bound … cm_alloc) >(alloc_high_bound … cm_alloc) % % // … … 1845 1910 lapply (alloc_memory_inj_m2 … Inj cm_alloc cm_bi) 1846 1911 lapply (alloc_valid_new_block … cm_alloc) #cm_frame_valid 1912 1913 (* Generalise *) 1847 1914 cut (∀b:block. ∀delta':offset. 1848 1915 Em b=Some (block×offset) 〈cm_frame,delta'〉 → 1849 ∀v,off,ty. lookup' vartypes v = OK ? 〈Stack off, ty〉 → 1916 ∀v,off,ty. 1917 Exists … (λx.x = 〈v,ty〉) L → 1918 lookup' vartypes v = OK ? 〈Stack off, ty〉 → 1850 1919 high_bound cl_m b+Zoo delta'≤O+Zoo (offset_of_Z off) 1851 1920 ∨ sizeof ty+Zoo (offset_of_Z off)≤low_bound cl_m b+Zoo delta') 1852 1921 [ #b #delta' #E @⊥ lapply (mi_nodangling … Inj … E) #V 1853 1922 @(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 1923 generalize in match Em; Em 1924 generalize in match cl_m; cl_m generalize in match empty_env; 1925 1926 elim L 1927 [ #cl_env #cl_m #Em #_ #Inj #cl_env' #cl_m1 #_ #cl_alloc 1857 1928 whd in cl_alloc:(??%%); destruct #H 1858 1929 %{Em} % [ % [ @Inj  // ]  #v * ] 1859 1930  * #v #ty #tl #IH 1860 #cl_env # Em #Hexisting #Inj #cl_env' #cl_m11931 #cl_env #cl_m #Em #Hexisting #Inj #cl_env' #cl_m1 * #Hdistinct #Hdistinct' 1861 1932 whd in ⊢ (??%? → ?); @pair_elim #cl_m2 #cl_b #cl_alloc #cl_alloc' #H 1862 1933 cases (H v ty ?) [2: %1 % ] * 1863 1934 [ #r * #L * 1864 1935  #off * #L * * #off_low #off_high #other 1936 cut (off < Z_two_power_nat 16) 1937 [ @(Zlt_to_Zle_to_Zlt ? (sizeof ty + off)) 1938 [ <eq_plus_Zplus @lt_to_Zlt whd in ⊢ (??%); /2/ 1939  @(transitive_Zle … stacksize) [ <eq_plus_Zplus @le_to_Zle @off_high  /2/ ] 1940 ] 1941 ] #off_repr 1865 1942 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) 1943 [ #b #delta' #NE #E @(Hexisting … E … L) % % 1867 1944  cases (alloc_properties … cm_alloc) #_ #U #i #LOW #HIGH @U 1868 1945 [ /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)  // ] 1946  @(transitive_Zle … HIGH) >(unZoo … off_repr) 1947 <eq_plus_Zplus /2/ 1948 ] 1949  >(unZoo … off_repr) 1950 <eq_plus_Zplus >(alloc_high_bound … cm_alloc) @le_to_Zle @off_high 1951  >(alloc_low_bound … cm_alloc) // 1952  >(alloc_high_bound … cl_alloc) >(unZoo … off_repr) 1953 @(Zle_to_Zlt_to_Zlt … stack_ok) <eq_plus_Zplus @le_to_Zle @off_high 1954  >(alloc_region … cl_alloc) >(alloc_region … cm_alloc) % 1955  % [ >(alloc_low_bound … cl_alloc) % // 1956  >(alloc_high_bound … cl_alloc) % [ @le_to_Zle //  @(Zle_to_Zlt_to_Zlt … stack_ok) @le_to_Zle /2/ ] 1957 ] 1958  #Inj' lapply (IH … Inj' … cl_alloc' ?) 1959 [ #v' #ty' #EX @(H v' ty') %2 @EX 1960  @Hdistinct' 1961  #b #delta' @eq_block_elim 1962 [ #E1 #E2 whd in E2:(??%?); destruct #v' #off' #ty' #EX #L 1963 cases (other … L) 1964 [ #LE %2 >(unZoo … off_repr) >unZoo 1965 [ >(alloc_low_bound … cl_alloc) <eq_plus_Zplus <eq_plus_Zplus @le_to_Zle >commutative_plus @LE 1966  @(Zle_to_Zlt_to_Zlt … off_repr) @le_to_Zle /2/ 1967 ] 1968  #LE %1 >(unZoo … off_repr) >unZoo 1969 [ >(alloc_high_bound … cl_alloc) >sym_Zplus <eq_plus_Zplus <eq_plus_Zplus @le_to_Zle @LE 1970  cases (H v' ty') 1971 [ #c >L * #E whd in E:(??%%); destruct 1972 * * #_ #LE' #_ 1973 @(Zle_to_Zlt_to_Zlt … stack_ok) @le_to_Zle /2/ 1974  %2 assumption 1975 ] 1976 ] 1977  cases (Exists_All … EX Hdistinct) * #v'' #ty'' * #E destruct // 1874 1978 ] 1979  #NE #EM #v' #off' #ty' #EX 1980 <(alloc_other_high_bound … NE cl_alloc) <(alloc_other_low_bound … NE cl_alloc) 1981 @(Hexisting b delta' EM v' off' ty' ?) 1982 %2 assumption 1875 1983 ] 1984  * #Em' * * #Inj' #compat' #H' 1985 %{Em'} % [ % 1986 [ @Inj' 1987  #b' cases (compat' b') 1988 [ @eq_block_elim [ #E destruct #E whd in E:(??%%); destruct 1989  #NE #E whd in E:(??%%); %1 @E 1990 ] 1991  @eq_block_elim 1992 [ #E destruct #_ %1 @(mi_freeblock … Inj) @(new_block_invalid_before_alloc … cl_alloc) 1993  #NE #E whd in E:(??%%); %2 @E 1994 ] 1995 ] 1996 ] #v' * 1997 [ #E destruct %{cl_b} %{(Stack off)} %{ty} % [ % 1998 [ <(alloc_vars_env … cl_alloc') // @Hdistinct 1999  assumption 2000 ] whd lapply (compat' cl_b) >eq_block_b_b * 2001 #E whd in E:(??%%); [ destruct  <E % ] 2002 ] 2003  @H' 2004 ] 2005 ] 2006 ] 2007 ] 2008  * #L * 2009 cases (alloc_memory_inj_m1 … Inj cl_alloc) 2010 #Inj2 #compat2 2011 cases (IH … Inj2 … cl_alloc' ?) 2012 [ #Em' * * #Inj' #compat' #H' 2013 %{Em'} % [ % 2014 [ @Inj' 2015  /2/ 2016 ] #v' * 2017 [ #E destruct %{cl_b} %{Local} %{ty} % [ % 2018 [ <(alloc_vars_env … cl_alloc') // @Hdistinct 2019  assumption 2020 ] whd % 2021 ] 2022  @H' 2023 ] 1876 2024 ] 1877  >unZoo 1878 [ <eq_plus_Zplus >(alloc_high_bound … cm_alloc) 1879 *) 2025  #b #delta' @eq_block_elim 2026 [ #E destruct #E whd in E:(??%%); destruct 2027  #NE #EM #v' #off' #ty' #EX 2028 <(alloc_other_high_bound … NE cl_alloc) <(alloc_other_low_bound … NE cl_alloc) 2029 @(Hexisting b delta' EM v' off' ty' ?) 2030 %2 assumption 2031 ] 2032  @Hdistinct' 2033  #v' #ty' #EX @H %2 assumption 2034 ] 2035 ] 2036 ] qed. 2037 1880 2038 (* 1881 2039 lemma lset_inclusion_Exists : … … 1921 2079 subtrace corresponding to a measurable Clight subtrace. 1922 2080 *) 1923 (* WIP 2081 (* WIP *) 1924 2082 include "common/ExtraMonads.ma". 2083 2084 (* TODO: move *) 2085 lemma distinct_env_irr : ∀tag,A,B,l,f. 2086 distinct_env tag B (map ?? (λv.〈\fst v, f (\snd v)〉) l) → 2087 distinct_env tag A l. 2088 #tag #A #B #l #f elim l 2089 [ // 2090  * #id #a #tl #IH 2091 * #H1 #H2 % 2092 [ IH H2 elim tl in H1 ⊢ %; 2093 [ // 2094  * #id' #a' #tl' #IH * #NE #TL % /2/ 2095 ] 2096  @IH assumption 2097 ] 2098 ] qed. 2099 2100 lemma distinct_snoc : ∀tag,A,id,a,l. 2101 All ? (λia.id≠\fst ia) l → 2102 distinct_env tag A l → 2103 distinct_env tag A (l@[〈id,a〉]). 2104 #tag #A #id #a #l elim l 2105 [ #_ #_ % % 2106  * #id' #a' #tl #IH * #NE #TL * #D1 #D2 % 2107 [ @All_append [ assumption  % [ /2/  % ] ] 2108  @IH [ @TL  @D2 ] 2109 ] 2110 ] qed. 2111 2112 lemma distinct_env_sym : ∀tag,A,l1,l2. 2113 distinct_env tag A (l1@l2) → 2114 distinct_env tag A (l2@l1). 2115 #tag #A #l1 elim l1 2116 [ // 2117  * #id #a #tl #IH #l2 * #D1 #D2 >append_cons @IH 2118 <associative_append @distinct_snoc // 2119 ] qed. 2120 2121 2122 2123 lemma Exist_sym : ∀tag,A,L,id. 2124 Exists (identifier tag × A) (λx. \fst x = id) L ↔ Exists ? (λx. id = \fst x) L. 2125 #tag #A #L #id elim L 2126 [ /2/ 2127  * #id' #a #tl #IH % 2128 [ * [ #E %1 >E %  #H %2 @(proj1 … IH) @H ] 2129  * [ #E %1 >E %  #H %2 @(proj2 … IH) @H ] 2130 ] 2131 ] qed. 2132 2133 lemma Exists_unpair : ∀tag,A,L,id,a. 2134 Exists (identifier tag × A) (λx. x = 〈id,a〉) L → Exists ? (λx. \fst x = id) L. 2135 #tag #A #L #id #a elim L 2136 [ * 2137  * #id' #a' #tl #IH * [ #E destruct %1 %  #H %2 @IH @H ] 2138 ] qed. 2139 2140 lemma characterise_vars_lookup : ∀globals,f,vartypes,stacksize,id,ty. 2141 characterise_vars globals f = 〈vartypes, stacksize〉 → 2142 distinct_env … (fn_params f @ fn_vars f) → 2143 Exists ? (λx. x = 〈id,ty〉) (fn_params f @ fn_vars f) → 2144 ∃c. match c with [Global _ ⇒ False  _ ⇒ True] ∧ lookup' vartypes id = OK ? 〈c,ty〉. 2145 #globals * #ret #args #vars #body 2146 whd in match (characterise_vars ??); elim (args@vars) 2147 [ #vartypes #stacksize #id #ty #_ #_ * 2148  * #hd #ty #tl #IH 2149 #vartypes #stacksize #id #ty' 2150 whd in match (foldr ?????); 2151 cases (foldr ? (Prod ??) ???) in IH ⊢ %; 2152 #vartypes' #stackspace' #IH 2153 whd in ⊢ (??(match % with [_⇒?])? → ?); 2154 cases (orb ??) 2155 #E whd in E:(??%?); * #D1 #D2 destruct * 2156 [ #E destruct %{(Stack stackspace')} % [ % ] 2157 whd in match (lookup' ??); >lookup_add_hit // 2158  3: #E destruct %{Local} % [ % ] 2159 whd in match (lookup' ??); >lookup_add_hit // 2160  2,4: #TL cases (IH … (refl ??) D2 TL) #c * #C #LC 2161 %{c} %{C} 2162 whd in match (lookup' ??) in LC ⊢ %; >lookup_add_miss try @LC 2163 elim tl in D1 TL; 2164 [1,3: #_ * 2165 *: * #id' #ty' #tl' #IH * #NE #D' * 2166 [1,3: #E destruct /2/ 2167 *: @IH @D' 2168 ] 2169 ] 2170 ] 2171 ] qed. 2172 2173 (* For showing that binding and storing parameters in memory works. 2174 2175 lemma bind_and_store_equiv : ∀cl_ge,cm_ge,INV,cl_f,cm_f,cl_env,cm_env,cl_args,cm_args,cl_m1,cl_m2,cm_m,stackptr,Em,vartypes,lbls,uv,cl_s,s,fgens,s1,Is. 2176 All2 … (λcl,cm.value_eq Em cl cm) cl_args cm_args → 2177 exec_bind_parameters cl_env cl_m1 (fn_params cl_f) cl_args = return cl_m2 → 2178 f_params cm_f = map ?? (λv.〈\fst v, typ_of_type (\snd v)〉) (fn_params cl_f) → 2179 alloc_params vartypes lbls cl_s uv DoNotConvert (opttyp_of_type (fn_return cl_f)) (fn_params cl_f) s = return «〈fgens, s1〉, Is» → 2180 memory_inj Em cl_m1 cm_m → 2181 ∃cm_en,Hcm_args_present. 2182 bind_params cm_args (f_params cm_f) = return «cm_en, Hcm_args_present» ∧ 2183 memory_matching Em cl_ge cm_ge cl_m2 cm_m cl_env cm_env INV stackptr vartypes ∧ 2184 ∀fInv,Inv,kInv,st. ∃n. 2185 after_n_steps n ?? (pcs_exec cm_pre) cm_ge (State cm_f s1 cm_env fInv Inv cm_m stackptr Kend kInv st) (λs.cminor_normal s) (λtr,s'. 2186 tr = E0 ∧ 2187 match s' with 2188 [ State f' code en _ _ m sp' k' kInv' st' ⇒ 2189 memory_inj Em cl_m2 m ∧ 2190 f' = cm_f ∧ code = s1 ∧ en = cm_env ∧ sp' = stackptr ∧ k' = Kend ∧ st' = st 2191  _ ⇒ False 2192 ]). 2193 2194 (* Call simulation, not yet complete. *) 1925 2195 1926 2196 lemma clight_cminor_call : … … 1947 2217  #g #g' #INV #cl_k #cm_k #cm_st #cl_f #cm_f #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize #stmt_univ #tmpenv #Htmpenv #Em #HEm_tmp #CHAR #ALLOC #INJ #MATCH #HEm_fn #HEm_env #CONT 1948 2218 #CL whd in CL:(??%?); destruct 1949  #g #g' #INV #cl_k #cm_st #cl_fd #cm_fd #fblock #target_type #cl_env #cl_m #cm_env #cm_m #fid #Hfind_cl #Hfind_cm #tmpenv #CONT #Em #I NJ#HEm_fn #cl_args #cm_args #Hargs2219  #g #g' #INV #cl_k #cm_st #cl_fd #cm_fd #fblock #target_type #cl_env #cl_m #cm_env #cm_m #fid #Hfind_cl #Hfind_cm #tmpenv #CONT #Em #Inj #HEm_fn #cl_args #cm_args #Hargs 1950 2220 #CL #s2 #tr2 #s3 #tr3 #STEP1 #STEP2 #CS2 1951 2221 … … 1992 2262 1993 2263 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» ∧ 2264 @pair_elim #cm_m1 #cm_frame #cm_alloc 2026 2265 2027 2266 cut (distinct_env … (fn_params cl_f @ fn_vars cl_f)) 2267 [ whd in match cm_vars in D; <map_append in D; <associative_append 2268 #D lapply (distinct_env_sym … D) <associative_append #D2 2269 lapply (distinct_env_append_l … D2) #D3 2270 lapply (distinct_env_sym … D3) >map_append #D4 2271 @(distinct_env_irr … D4) ] #cl_distinct 2272 lapply (alloc_vars_rel vartypes ????? Em Inj ? cm_alloc ??? cl_distinct (sym_eq … ALLOC) ?) 2273 [ #v #ty #EX 2274 cases (characterise_vars_lookup … (sym_eq … Hcharacterise) cl_distinct EX) 2275 * 2276 [ #r * * 2277  #off * #_ #L %{(Stack off)} %{L} 2278 whd % 2279 [ % // >commutative_plus @(characterise_vars_in_range … (sym_eq … Hcharacterise) … L) 2280  @(characterise_vars_disjoint … (sym_eq … Hcharacterise) … L) 2281 ] 2282  * #_ #L %{Local} %{L} % 2283 ] 2284  (* FIXME *) cases daemon 2285 ] 2286 * #Em' * * #Inj' #compat' #alloc_ok 2287 2028 2288 *) 2029 2289 2030 (* 2031 lemma clight_cminor_call_return : 2032 ∀g1, g2. 2033 ∀INV:clight_cminor_inv g1 g2. 2034 ∀s1,s1'. 2035 clight_cminor_rel g1 g2 INV s1 s1' → 2036 match Clight_classify s1 with 2037 [ cl_call ⇒ true 2038  cl_return ⇒ true 2039  _ ⇒ false ] → 2040 ∀s2,tr. step … (pcs_exec cl_pre) g1 s1 = Value … 〈tr, s2〉 → 2041 ∃m. after_n_steps m ?? (pcs_exec cm_pre) g2 s1' (λs.cminor_normal s) (λtr',s2'. 2042 tr = tr' ∧ 2043 clight_cminor_rel g1 g2 INV s2 s2' ∧ 2044 (m = 0 → lex_lt (measure_Clight s2) (measure_Clight s1)) 2045 ). 2046 #g1 #g2 #INV #s1 #s1' #Hstate_rel #Hclight_class 2047 inversion Hstate_rel 2048 [ 1: (* normal *) 2049 #cl_ge #cm_ge #INV' #cl_s 2050 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 2051 #alloc_type #cl_env #cl_m #cm_env #cm_m #stackptr #stacksize 2052 (* introduce everything *) 2053 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 2054 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2055 #flag #Htrans_inv #Htrans_stmt #Hincl #HA #HB #HC 2056 #HE #HF #HG #HI #HJ #HK 2057 @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2 2058 destruct (H1 H2) 2059 @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5 2060 destruct (H3 H4 H5) 2061 @False_ind @Hclight_class 2062  5: 2063 #cl_ge #cm_ge #INV' #cl_s 2064 #cm_s #cl_k #cm_k #cm_st #cl_f #cm_f #rettyp 2065 #alloc_type #cl_k #cm_k #sz #sg #cl_ty #cl_cond_desc #cl_body #entry_lab #exit_lab 2066 #cm_cond #cm_body #cm_stack #rettyp' #kInv 2067 (* introduce everything *) 2068 #fInv #sInv #kInv #Htarget_type #func_univ #Hfresh_globals #Hfresh_function #Htranslate_function 2069 #stmt_univ #stmt_univ' #lbl_univ #lbl_univ' #lbls 2070 #lbl1 #lbl2 #Em #Htmp_vars #Hcharac #Hexec #Hinj #Hmatching #Hem #Hframe #Hcond_tr 2071 #Htransl #Hex1 #Hex2 #Htransinv #Hmklabs #Htranstmt #Hincl 2072 #Hlabdecl #Hinv1 #Hinv2 #Hfindlab 2073 @(jmeq_absorb ?????) #H1 @(jmeq_absorb ?????) #H2 2074 destruct (H1 H2) 2075 @(jmeq_absorb ?????) #H3 @(jmeq_absorb ?????) #H4 @(jmeq_absorb ?????) #H5 2076 destruct (H3 H4 H5) 2077 @False_ind @Hclight_class 2078  2: 2079 #cl_ge #cm_ge #INV' #cl_f #cm_f #cl_k #cm_k #alloc_type 2080 #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #stacksize 2081 #stmt_univ #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp 2082 #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel 2083 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2084 destruct (HA HB) 2085 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE #_ 2086 destruct (HC HD HE) 2087 inversion Hcont_rel 2088 [ #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kcl_env #kcm_env #kalloc_type #kstack #Hkstack 2089 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2090 destruct (HA HB) 2091 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 2092 destruct (HC HD HE) 2093 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 2094 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL 2095 destruct (HF HG HH HI HJ HK HL) #_ 2096 #s2 #tr 2097 whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) 2098  (* Kseq *) 2099 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_s #kcm_s 2100 #kcl_env #kcm_env #kcl_k' #kcm_k' #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbls #kflag 2101 * * * * #kHstmt_inv #kHlabels_translated #kHtmps_preserved 2102 #kHreturn_ok #kHlabel_wf #kHeq_translate #kHlabel_inclusion #kHcont_rel #_ 2103 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2104 destruct (HA HB) 2105 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 2106 destruct (HC HD HE) 2107 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH @(jmeq_absorb ?????) #HI 2108 @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK @(jmeq_absorb ?????) #HL 2109 destruct (HF HG HH HI HJ HK HL) #_ 2110 #s2 #tr 2111 whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) 2112  (* *) 2113 #kcl_ge #kcm_ge #kINV #kcl_f #kcm_f #ktarget_type #kstack #kalloc_type #kcl_env #kcm_env 2114 #kcl_k' #kcm_k' #ksz #ksg #kcl_ty #kcl_cond_desc #kcl_body #kHeq_ty #kcm_cond #kcm_body 2115 #kentry #kexit #kstmt_univ #kstmt_univ' #klbl_univ #klbl_univ' #klbl_univ'' 2116 #klbls #kHtranslate_inv #kHexpr_vars #kHtranslate_expr #kfInv #kHlabel_declared 2117 #kHinv #kHmklabels #kHeq_translate #kHlabel_inclusion #kHfind_label 2118 (* 2119 * * * * #kHentry_declared * * * * 2120 * * * #kHcond_vars_declared #Hnoise #Hnoise' #Hnoise'' 2121 #kHcont_inv #kHmklabels #kHeq_translate 2122 #kHfind_label *) #kHcont_rel #_ 2123 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2124 destruct (HA HB) 2125 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 2126 destruct (HC HD HE) 2127 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 2128 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 2129 @(jmeq_absorb ?????) #HL 2130 destruct (HF HG HH HI HJ HK HL) #_ 2131 #s2 #tr 2132 whd in ⊢ ((??%?) → ?); #Habsurd destruct (Habsurd) 2133 ] 2134  3: 2135 #cl_ge #cm_ge #INV' #alloc_type 2136 #cl_env #cl_m #cm_env #cm_m #cm_st #stackptr #func_univ 2137 #cl_f #cm_f #Hglobals_fresh #Hfundef_fresh 2138 #rettyp #cl_k #cm_k #fblock * 2139 #Hrettyp #Hfind_funct_cl #Hfind_func_cm #Htranslate_function #Hcont_rel 2140 #fun_id #cl_retval #cm_retval #sInv #fInv #kInv #cl_args #cm_args 2141 @(jmeq_absorb ?????) #HA @(jmeq_absorb ?????) #HB 2142 destruct (HA HB) 2143 @(jmeq_absorb ?????) #HC @(jmeq_absorb ?????) #HD @(jmeq_absorb ?????) #HE 2144 destruct (HC HD HE) #_ 2145 #s2 #tr whd in ⊢ ((??%?) → ?); 2146 @(match (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f)) 2147 return λx. (x = (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f))) → ? 2148 with 2149 [ mk_Prod new_cl_env cl_m_alloc ⇒ ? 2150 ] (refl ? (exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f)))) 2151 #Hexec_alloc_variables normalize nodelta 2152 #Hstep 2153 cases (bindIO_inversion ??????? Hstep) Hstep 2154 #cl_m_init * #Hexec_bind_parameters 2155 whd in ⊢ ((??%%) → ?); #Heq destruct (Heq) 2156 %{1} whd whd in ⊢ (??%?); 2157 (* Alloc big chunk of data of size (f_stacksize cm_f) *) 2158 @(match (alloc cm_m 0 (f_stacksize cm_f)) 2159 return λx. (alloc cm_m 0 (f_stacksize cm_f) = x) → ? 2160 with 2161 [ mk_Prod new_cm_mem new_cm_stackptr ⇒ ? 2162 ] (refl ? (alloc cm_m 0 (f_stacksize cm_f)))) 2163 #H_cm_alloc normalize nodelta 2164 (* Initialise CM /parameters/ *) 2165 2166 2167 %{(S (times 3 (fn_vars)))} Hclight_class 2168 lapply (exec_alloc_bind_params_same_length … Hexec_bind_parameters) 2169 elim cl_args in Hstate_rel Hexec_alloc; 2170 [ #Hstate_rel whd in ⊢ ((??%%) → ?); 2171 2172 whd in match (exec_bind_parameters ????); 2173 2174 exec_alloc_variables empty_env cl_m (fn_params cl_f@fn_vars cl_f) = 〈cl_env, cl_m'〉 2175 2176 2177 lapply (let_prod_as_inversion ?????? Hstep) 2178 @(jmeq_absorb ?????) #HF @(jmeq_absorb ?????) #HG @(jmeq_absorb ?????) #HH 2179 @(jmeq_absorb ?????) #HI @(jmeq_absorb ?????) #HJ @(jmeq_absorb ?????) #HK 2180 @(jmeq_absorb ?????) #HL 2181 destruct (HF HG HH HI HJ HK HL) #_ 2182 #s2 #tr 2183 2184 2185 #Em #Htmp_vars_well_allocated #Halloc_hyp #Hcl_env_hyp 2186 #Hinjection #Hmatching #HEm_fn_id #Hframe_spec #Hcont_rel 2187 ] qed. *) 2290 2188 2291 2189 2292 lemma clight_cminor_normal :
Note: See TracChangeset
for help on using the changeset viewer.