 Timestamp:
 Dec 14, 2012, 12:40:37 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2553 r2555 2147 2147 qed. 2148 2148 2149 lemma block_of_call_sigma_commute : 2150 ∀p,p',graph_prog,sigma. 2151 ∀gss : good_state_sigma p p' graph_prog sigma.∀cl. 2152 preserving … res_preserve … 2153 (sigma_state p p' graph_prog sigma gss) 2154 (λx.λ_ : True .x) 2155 (block_of_call (make_sem_graph_params p p') … 2156 (globalenv_noinit ? graph_prog) cl) 2157 (block_of_call (make_sem_lin_params p p') … 2158 (globalenv_noinit ? (linearise ? graph_prog)) cl). 2159 #p #p' #graph_prog #sigma #gss #cl #st #prf 2160 @mfr_bind 2161 [3: cases cl 2162 [ #id normalize nodelta @opt_to_res_preserve 2163 >(find_symbol_transf … 2164 (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog id) 2165 #s #EQs %{I} >EQs in ⊢ (??%?); % 2166  * #dpl #dph normalize nodelta 2167 @mfr_bind [3: @dpl_arg_retrieve_commute *:] 2168 #bv1 #bv1_prf 2169 @mfr_bind [3: @dph_arg_retrieve_commute *:] 2170 #bv2 #bv2_prf 2171 @(mfr_bind … (λptr.λ_:True.ptr)) 2172 [ lapply bv2_prf lapply bv2 lapply bv1_prf lapply bv1 2173 @bv_pc_other 2174 [ #pc1 #p #bv1_prf #bv2 #bv2_prf @res_preserve_error ] 2175 #bv1 #bv1_no_pc #bv1_prf 2176 @bv_pc_other 2177 [ cases bv1 in bv1_prf; 2178 [#a #b #c #a  #a  #a #b  #a #b ] #bv1_prf 2179 #pc2 #p #bv2_prf @res_preserve_error ] 2180 #bv2 #bv2_no_pc #bv2_prf 2181 >sigma_bv_no_pc try assumption 2182 >sigma_bv_no_pc try assumption 2183 whd #ptr #EQ %{I EQ} 2184 ] #ptr * 2185 @if_elim #_ [ @mfr_return  @res_preserve_error ] % 2186 ] 2187 4: #bl * @opt_to_res_preserve #x #EQ %{I} @EQ 2188 *: 2189 ] 2190 qed. 2191 2192 2149 2193 lemma eval_call_ok : 2150 2194 ∀p,p',graph_prog. 2151 2195 let lin_prog ≝ linearise p graph_prog in 2152 2196 ∀stack_sizes. 2153 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 2197 ∀sigma. good_sigma p graph_prog sigma → 2198 ∀gss : good_state_sigma p p' graph_prog sigma. 2154 2199 ∀st,st',f,fn,called,args,dest,nxt. 2155 2200 ∀prf : well_formed_state_pc … gss st. 2156 fetch_statement (make_sem_ lin_params p p') …2157 (globalenv_noinit ? lin_prog) (pc … (sigma_state_pc … st prf)) =2158 return 〈f, \fst (linearise_int_fun … fn),2159 sequential … (CALL (mk_ lin_params p) … called args dest ) it〉 →2201 fetch_statement (make_sem_graph_params p p') … 2202 (globalenv_noinit ? graph_prog) (pc … st) = 2203 return 〈f, fn, 2204 sequential … (CALL (mk_graph_params p) … called args dest ) nxt〉 → 2160 2205 eval_seq_advance ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 2161 2206 (CALL … called args dest) nxt st = return st' → … … 2181 2226 eval_state … (ev_genv … (lin_prog_params … (linearise … graph_prog) stack_sizes)) 2182 2227 st2_pre_call = return st2_after_call. 2183 cases daemon 2184 qed. 2185 2228 #p #p' #graph_prog #stack_sizes #sigma #good #gss #st #st1 #f #fn 2229 #called #args #dest #nxt #prf #fetch_spec 2230 cases(fetch_statement_sigma_commute … good (proj1 … prf) … fetch_spec) #_ 2231 normalize nodelta * #lin_fetch_spec #_ 2232 whd in match eval_seq_advance; whd in match eval_seq_call; normalize nodelta 2233 @('bind_inversion) #bl #H lapply (err_eq_from_io ????? H) H #bl_spec 2234 @('bind_inversion) * #id #int_f #H lapply (err_eq_from_io ????? H) H 2235 cases int_f int_f [ #fn  #ext_f] #int_f_spec normalize nodelta 2236 [2:#H @('bind_inversion H) H #st' #H #_ @('bind_inversion H) H #vals #_ 2237 @'bind_inversion #vals' #_ whd in ⊢ (??%%→?); #ABS destruct(ABS) ] 2238 #H % 2239 [ @hide_prf 2240 whd in match joint_classify; normalize nodelta >fetch_spec >m_return_bind 2241 normalize nodelta whd in match joint_classify_step; 2242 whd in match joint_classify_seq; normalize nodelta 2243 >bl_spec >m_return_bind >int_f_spec normalize nodelta % 2244  % 2245 [ @hide_prf whd in match joint_classify; normalize nodelta >lin_fetch_spec 2246 >m_return_bind normalize nodelta whd in match joint_classify_step; 2247 whd in match joint_classify_seq; normalize nodelta 2248 cases bl in bl_spec int_f_spec; #reg #reg_prf bl #reg_spec #int_f_spec 2249 cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 2250 reg_spec) 2251 * #EQ >EQ EQ >m_return_bind 2252 lapply(fetch_function_transf ????? 2253 (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????) 2254 [ 2255  @(Internal ? fn) 2256  @id 2257  assumption assumption 2258  2259  2260  % 2261 [@(prog_vars … graph_prog) 2262 @(prog_funct … graph_prog) 2263 @(prog_main … graph_prog) 2264 ] 2265 ] 2266 [>int_f_spec %   ] #EQ >EQ normalize nodelta % 2267  % 2268 [2: % 2269 [ change with ((λx.joint_call_ident (lin_prog_params p p' (linearise p graph_prog) stack_sizes) 2270 (mk_Sig ? ? ? x)) ? = (λx.joint_call_ident ? (mk_Sig ? ? ? x)) ?) 2271 whd in match joint_call_ident in ⊢ (??(%?)?); normalize nodelta in ⊢ (??(%?)?); 2272 whd in match (pc ?); >lin_fetch_spec in ⊢ (??(%?)?); normalize nodelta in ⊢ (??%?); 2273 whd in match joint_call_ident in ⊢ (???(%?)); normalize nodelta in ⊢ (???(%?)); 2274 >fetch_spec in ⊢ (???(%?)); normalize nodelta >bl_spec in ⊢ (???%); 2275 >m_return_bind in ⊢ (???%); 2276  whd in match eval_state; normalize nodelta 2277 >lin_fetch_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2278 whd in match eval_statement_no_pc; normalize nodelta 2279 whd in match eval_seq_no_pc; normalize nodelta 2280 >m_return_bind in ⊢ (??%?); 2281 whd in match eval_statement_advance; whd in match eval_seq_advance; 2282 whd in match eval_seq_call; normalize nodelta 2283 ] 2284 cases(block_of_call_sigma_commute p p' graph_prog sigma gss ?? (proj2 … prf) ? 2285 bl_spec) * #EQ >EQ in ⊢ (??%?); >m_return_bind in ⊢ (??%?); EQ 2286 [ whd in match fetch_internal_function; normalize nodelta >int_f_spec in ⊢ (???%); 2287 >m_return_bind in ⊢ (???%); normalize nodelta ] 2288 lapply(fetch_function_transf ????? 2289 (λvars.transf_fundef … (λf_in.\fst(linearise_int_fun ?? f_in))) ????) 2290 [ 2291  2,12: @(Internal ? fn) 2292  3,13: @id 2293  4,14: assumption assumption 2294  5,15: 2295  6,16: 2296 7,17: % 2297 [1,4: @(prog_vars … graph_prog) 2298 2,5: @(prog_funct … graph_prog) 2299 3,6: @(prog_main … graph_prog) 2300 ] 2301 ] 2302 [1,5: >int_f_spec % *:] #EQ >EQ in ⊢ (??%?); EQ 2303 >m_return_bind in ⊢ (??%?); normalize nodelta [ %] 2304 ] 2305 ] 2306 ] 2307 [2: @hide_prf] 2308 lapply (err_eq_from_io ????? H) H #H @('bind_inversion H) 2309 #st' #st_spec' #H @('bind_inversion H) H #st'' #st_spec'' 2310 whd in ⊢ (??%% → ?); #EQ destruct(EQ) [ % ] 2311 [2,3: elim(save_frame_commute p p' graph_prog sigma gss … prf … st_spec') 2312 #wf_st' #sigma_st_spec' [2: >sigma_st_spec' in ⊢ (??%?); >m_return_bind in ⊢ (??%?);] 2313 lapply st_spec'' st_spec'' whd in match eval_internal_call; normalize nodelta 2314 #H @('bind_inversion H) H #dim_s #dim_s_spec #H 2315 [ >dim_s_spec in ⊢ (??%?); >m_return_bind in ⊢ (??%?);] 2316 elim(bind_inversion ????? H) H #st''' * #st_spec''' 2317 elim(setup_call_commute p p' graph_prog sigma gss … wf_st' … st_spec''') 2318 #wf_st''' #sigma_st_spec''' whd in ⊢ (??%% → ?); 2319 whd in match allocate_locals; whd in match set_regs; normalize nodelta 2320 #EQ destruct(EQ) 2321 ] 2322 [ >sigma_st_spec''' in ⊢ (??%?); >m_return_bind in ⊢ (??%?); 2323 whd in match sigma_state_pc; normalize nodelta 2324 change with (return mk_state_pc (make_sem_lin_params p p') ? ? = ?) 2325 cut(∀A,semp,pc,pc',st,st'.∀ f : ? → A.pc = pc' ∧ st = st' → 2326 f(mk_state_pc semp st pc) = f(mk_state_pc semp st' pc')) 2327 [#A #H1 #H2 #H3 #H4 #H5 #f * #H8 #H9 //] 2328 #APP @APP % 2329 ] 2330 [1,4: [whd in match sigma_pc; normalize nodelta @opt_safe_elim #lin_pc  whd in match well_formed_pc;] 2331 whd in match sigma_pc_opt; normalize nodelta @if_elim 2332 [1,3: @eqZb_elim [2,4: #_ *] #EQbl cases bl in EQbl int_f_spec; * 2333 #reg #pos #reg_prf normalize in ⊢ (% → ?); 2334 #EQbl whd in match fetch_function; normalize nodelta 2335 >EQbl cases(symbol_for_block ???) 2336 [1,3: whd in ⊢ (??%% → ?); #ABS destruct(ABS)] 2337 #id1 >m_return_bind inversion(find_funct_ptr ???) 2338 [1,3:#_ whd in ⊢ (??%% → ?); #ABS destruct(ABS)] 2339 #z lapply(globalenv_no_minus_one ??? graph_prog) [1,3: @(λn.[Init_space n])] 2340 #EQ 2341 change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?) → ?) 2342 change with ((find_funct_ptr ? (globalenv_noinit ? graph_prog) ? = ?)) in EQ; 2343 cases reg in ⊢ (% → ?); 2344 [1,3: whd in match find_funct_ptr; normalize nodelta #ABS destruct(ABS) 2345 2,4: >EQ #ABS destruct(ABS) 2346 ] 2347 2,4: #_ whd in match fetch_internal_function; normalize nodelta 2348 whd in match (pc_block ?); >int_f_spec >m_return_bind 2349 >point_of_pc_of_point lapply(good fn) ** #EQ #_ #_ >EQ EQ 2350 >m_return_bind [2:%] whd in ⊢ (??%? → ?); #EQ destruct(EQ) 2351 % 2352 ] 2353  whd in match sigma_state; normalize nodelta 2354 cut(∀A,semp,fr,fr',is,is',c,c',r,r',m,m'.∀ f : ? → A. 2355 fr = fr' ∧ is = is' ∧ c = c' ∧ r = r' ∧ m = m'→ 2356 f(mk_state semp fr is c r m) = f(mk_state semp fr' is' c' r' m')) 2357 [#A #semp #fr #fr' #is #is' #c #c' #r #r' #m #m' #f **** //] 2358 #APP @APP % [% [% [% [%]]]] // [whd in match sigma_is; normalize nodelta % 3: 2359 whd in match sigma_mem; normalize nodelta %] 2360  % [2: @(proj2 … wf_st')] % [ % [ @(proj1 … (proj1 … (proj1 … wf_st')))  2361 @(proj2 … (proj1 … (proj1 … wf_st')))] ] 2362 ] 2363 [ change with (? = (λx.sigma_regs ? ? ? ? ? (foldr ? ? ? ? x) ?)?) 2364 [ cut((joint_if_locals (lin_prog_params p p' (linearise p graph_prog) stack_sizes) 2365 (globals (lin_prog_params p p' (linearise p graph_prog) stack_sizes)) 2366 (\fst (linearise_int_fun p 2367 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn))) = (joint_if_locals (graph_prog_params p p' graph_prog stack_sizes) 2368 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn)) 2369 [%] #EQ >EQ 2370 elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes) 2371 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn) in ⊢ (??%(?%)); 2372  @hide_prf elim x 2373 ] 2374  @hide_prf elim(joint_if_locals (graph_prog_params p p' graph_prog stack_sizes) 2375 (globals (graph_prog_params p p' graph_prog stack_sizes)) fn) 2376 ] 2377 [3,5: whd in match (foldr ? ? ???); @(proj2 … (proj1 … wf_st')) 2378 4,6: #locs_t #tl_list #wf_regs_tail whd in match (foldr ? ? ???); 2379 elim(allocate_locals_commute p p' graph_prog sigma gss locs_t 2380 ? wf_regs_tail) #wf_regs_locs_t #_ assumption 2381 *: normalize nodelta 2382 [ whd in match (foldr ? ? ???) in ⊢ (??%%); % 2383  #locs_t #tl_list #EQtl whd in match (foldr ?????) in ⊢ (??%%); 2384 >EQtl 2385 lapply(allocate_locals_commute p p' graph_prog sigma gss locs_t 2386 (foldr (localsT ?) (regsT ?) (allocate_locals_ ???) (regs ? st') tl_list) ?) 2387 [2: * #x #H >H % ] 2388 ] 2389 ] 2390 qed. 2391 2186 2392 lemma eval_goto_ok : 2187 lemma eval_tailcall_ok : 2393 lemma eval_tailcall_ok 2394 : 2188 2395 lemma eval_cond_cond_ok : 2189 2396 lemma eval_cond_fcond_ok :
Note: See TracChangeset
for help on using the changeset viewer.