Changeset 2808 for src/joint/lineariseProof.ma
 Timestamp:
 Mar 7, 2013, 6:03:18 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2570 r2808 209 209 definition graph_prog_params ≝ 210 210 λp,p',prog,stack_sizes. 211 mk_prog_params (m ake_sem_graph_params p p') prog stack_sizes.211 mk_prog_params (mk_sem_graph_params p p') prog stack_sizes. 212 212 213 213 definition graph_abstract_status: … … 223 223 definition lin_prog_params ≝ 224 224 λp,p',prog,stack_sizes. 225 mk_prog_params (m ake_sem_lin_params p p') prog stack_sizes.225 mk_prog_params (mk_sem_lin_params p p') prog stack_sizes. 226 226 227 227 definition lin_abstract_status: … … 296 296 ≝ 297 297 λp,p',prog,sigma,pc. 298 let pars ≝ m ake_sem_graph_params p p' in298 let pars ≝ mk_sem_graph_params p p' in 299 299 let ge ≝ globalenv_noinit … prog in 300 300 if eqZb (block_id (pc_block pc)) (1) then (* check for dummy exit pc *) … … 304 304 ! lin_point ← sigma fd (point_of_pc pars pc) ; 305 305 return pc_of_point 306 (m ake_sem_lin_params ? p') (pc_block pc) lin_point.306 (mk_sem_lin_params ? p') (pc_block pc) lin_point. 307 307 308 308 definition well_formed_pc: … … 574 574 (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 575 575 (sigma : sigma_map p graph_prog) : Type[0] ≝ 576 { well_formed_frames : framesT (m ake_sem_graph_params p p') → Prop577 ; sigma_frames : ∀frms.well_formed_frames frms → framesT (m ake_sem_lin_params p p')576 { well_formed_frames : framesT (mk_sem_graph_params p p') → Prop 577 ; sigma_frames : ∀frms.well_formed_frames frms → framesT (mk_sem_lin_params p p') 578 578 ; sigma_empty_frames_commute : 579 579 ∃prf. 580 empty_framesT (m ake_sem_lin_params p p') =581 sigma_frames (empty_framesT (m ake_sem_graph_params p p')) prf582 583 ; well_formed_regs : regsT (m ake_sem_graph_params p p') → Prop584 ; sigma_regs : ∀regs.well_formed_regs regs → regsT (m ake_sem_lin_params p p')580 empty_framesT (mk_sem_lin_params p p') = 581 sigma_frames (empty_framesT (mk_sem_graph_params p p')) prf 582 583 ; well_formed_regs : regsT (mk_sem_graph_params p p') → Prop 584 ; sigma_regs : ∀regs.well_formed_regs regs → regsT (mk_sem_lin_params p p') 585 585 ; sigma_empty_regsT_commute : 586 586 ∀ptr.∃ prf. 587 empty_regsT (m ake_sem_lin_params p p') ptr =588 sigma_regs (empty_regsT (m ake_sem_graph_params p p') ptr) prf587 empty_regsT (mk_sem_lin_params p p') ptr = 588 sigma_regs (empty_regsT (mk_sem_graph_params p p') ptr) prf 589 589 ; sigma_load_sp_commute : 590 590 preserving … res_preserve … … … 593 593 sigma_regs 594 594 (λx.λ_.x) 595 (load_sp (m ake_sem_graph_params p p'))596 (load_sp (m ake_sem_lin_params p p'))595 (load_sp (mk_sem_graph_params p p')) 596 (load_sp (mk_sem_lin_params p p')) 597 597 ; sigma_save_sp_commute : 598 598 ∀reg,ptr,prf1. ∃prf2. 599 save_sp (m ake_sem_lin_params p p') (sigma_regs reg prf1) ptr =600 sigma_regs (save_sp (m ake_sem_graph_params p p') reg ptr) prf2599 save_sp (mk_sem_lin_params p p') (sigma_regs reg prf1) ptr = 600 sigma_regs (save_sp (mk_sem_graph_params p p') reg ptr) prf2 601 601 }. 602 602 … … 605 605 ∀sigma. 606 606 good_sem_state_sigma p p' graph_prog sigma → 607 state (m ake_sem_graph_params p p') → Prop ≝607 state (mk_sem_graph_params p p') → Prop ≝ 608 608 λp,p',graph_prog,sigma,gsss,st. 609 609 well_formed_frames … gsss (st_frms … st) ∧ … … 616 616 ∀sigma. 617 617 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 618 ∀st : state (m ake_sem_graph_params p p').618 ∀st : state (mk_sem_graph_params p p'). 619 619 well_formed_state … gsss st → 620 state (m ake_sem_lin_params p p') ≝620 state (mk_sem_lin_params p p') ≝ 621 621 λp,p',graph_prog,sigma,gsss,st,prf. 622 622 mk_state … … … 694 694 ∀p,p',graph_prog,sigma. 695 695 good_sem_state_sigma p p' graph_prog sigma → 696 state_pc (m ake_sem_graph_params p p') → Prop ≝696 state_pc (mk_sem_graph_params p p') → Prop ≝ 697 697 λp,p',prog,sigma,gsss,st. 698 698 well_formed_pc p p' prog sigma (last_pop … st) ∧ … … 707 707 (* let lin_prog ≝ linearise ? graph_prog in *) 708 708 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 709 ∀s:state_pc (m ake_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *)709 ∀s:state_pc (mk_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) 710 710 well_formed_state_pc p p' graph_prog sigma gsss s → 711 state_pc (m ake_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)711 state_pc (mk_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) 712 712 ≝ 713 713 λp,p',graph_prog,sigma,gsss,s,prf. … … 796 796 (λr.pair_reg_move_ ? ? (p' ?) r mv) 797 797 (λr.pair_reg_move_ ? ? (p' ?) r mv) 798 ; allocate_locals__commute :799 ∀loc, r1, prf1. ∃ prf2.800 allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =801 sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2802 798 ; save_frame_commute : 803 799 ∀dest,fl. … … 1221 1217 (joint_closed_internal_function 1222 1218 (graph_prog_params p p' graph_prog 1223 (stack_sizes_lift (m ake_sem_graph_params p p') (make_sem_lin_params p p')1219 (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') 1224 1220 (linearise_int_fun p) graph_prog stack_sizes)) 1225 1221 (globals 1226 1222 (graph_prog_params p p' graph_prog 1227 (stack_sizes_lift (m ake_sem_graph_params p p') (make_sem_lin_params p p')1223 (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') 1228 1224 (linearise_int_fun p) graph_prog stack_sizes))))) 1229 1225 (ev_genv 1230 1226 (graph_prog_params p p' graph_prog 1231 (stack_sizes_lift (m ake_sem_graph_params p p') (make_sem_lin_params p p')1227 (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') 1232 1228 (linearise_int_fun p) graph_prog stack_sizes))) 1233 (pblock (pc (m ake_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct1229 (pblock (pc (mk_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct 1234 1230 1235 1231 … … 1240 1236 (joint_closed_internal_function 1241 1237 (graph_prog_params p p' graph_prog 1242 (stack_sizes_lift (m ake_sem_graph_params p p') (make_sem_lin_params p p')1238 (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') 1243 1239 (linearise_int_fun p) graph_prog stack_sizes)) 1244 1240 (globals 1245 1241 (graph_prog_params p p' graph_prog 1246 (stack_sizes_lift (m ake_sem_graph_params p p') (make_sem_lin_params p p')1242 (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') 1247 1243 (linearise_int_fun p) graph_prog stack_sizes))))) 1248 1244 (ev_genv 1249 1245 (graph_prog_params p p' graph_prog 1250 (stack_sizes_lift (m ake_sem_graph_params p p') (make_sem_lin_params p p')1246 (stack_sizes_lift (mk_sem_graph_params p p') (mk_sem_lin_params p p') 1251 1247 (linearise_int_fun p) graph_prog stack_sizes))) 1252 (pblock (pc (m ake_sem_graph_params p p') st))) in H;1248 (pblock (pc (mk_sem_graph_params p p') st))) in H; 1253 1249 1254 1250 … … 1358 1354 fetch_internal_function … 1359 1355 (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 → 1360 let pc' ≝ pc_of_point (m ake_sem_graph_params p p') … bl lbl in1356 let pc' ≝ pc_of_point (mk_sem_graph_params p p') … bl lbl in 1361 1357 code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl → 1362 ∃prf'.pc_of_label (m ake_sem_lin_params p p') … (globalenv_noinit … lin_prog)1358 ∃prf'.pc_of_label (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog) 1363 1359 bl lbl = 1364 1360 return sigma_pc p p' graph_prog sigma pc' prf'. … … 1406 1402 ∀prf : well_formed_pc p p' graph_prog sigma pc. 1407 1403 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 → 1408 sigma fn (point_of_pc (m ake_sem_graph_params p p') pc) = return n →1409 point_of_pc (m ake_sem_lin_params p p') (sigma_pc … pc prf) = n.1404 sigma fn (point_of_pc (mk_sem_graph_params p p') pc) = return n → 1405 point_of_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) = n. 1410 1406 #p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma 1411 1407 whd in match sigma_pc; normalize nodelta … … 1431 1427 ∀sigma.good_sigma p graph_prog sigma → 1432 1428 ∀prf : well_formed_pc p p' graph_prog sigma pc. 1433 fetch_statement (m ake_sem_graph_params p p') …1429 fetch_statement (mk_sem_graph_params p p') … 1434 1430 (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → 1435 1431 All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma 1436 (pc_of_point (m ake_sem_graph_params p p') (pc_block pc) lbl).1437 pc_of_label (m ake_sem_lin_params p p') …1432 (pc_of_point (mk_sem_graph_params p p') (pc_block pc) lbl). 1433 pc_of_label (mk_sem_lin_params p p') … 1438 1434 (globalenv_noinit … lin_prog) 1439 1435 (pc_block pc) … … 1444 1440 match s with 1445 1441 [ step_seq x ⇒ 1446 fetch_statement (m ake_sem_lin_params p p') …1442 fetch_statement (mk_sem_lin_params p p') … 1447 1443 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 1448 1444 return 〈f, \fst (linearise_int_fun … fn), 1449 1445 sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ 1450 1446 ∃prf'. 1451 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (m ake_sem_graph_params p p') pc nxt) prf' in1452 let nxt_pc ≝ succ_pc (m ake_sem_lin_params p p') (sigma_pc … pc prf) it in1447 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in 1448 let nxt_pc ≝ succ_pc (mk_sem_lin_params p p') (sigma_pc … pc prf) it in 1453 1449 (nxt_pc = sigma_nxt ∨ 1454 (fetch_statement (m ake_sem_lin_params p p') …1450 (fetch_statement (mk_sem_lin_params p p') … 1455 1451 (globalenv_noinit … lin_prog) nxt_pc = 1456 1452 return 〈f, \fst (linearise_int_fun … fn), 1457 1453 final (mk_lin_params p) … (GOTO … nxt)〉 ∧ 1458 (pc_of_label (m ake_sem_lin_params p p') …1454 (pc_of_label (mk_sem_lin_params p p') … 1459 1455 (globalenv_noinit … lin_prog) 1460 1456 (pc_block pc) … … 1462 1458  COND a ltrue ⇒ 1463 1459 ∃prf'. 1464 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (m ake_sem_graph_params p p') pc nxt) prf' in1460 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (mk_sem_graph_params p p') pc nxt) prf' in 1465 1461 (let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in 1466 (fetch_statement (m ake_sem_lin_params p p') …1462 (fetch_statement (mk_sem_lin_params p p') … 1467 1463 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 1468 1464 return 〈f, \fst (linearise_int_fun … fn), 1469 1465 sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧ 1470 1466 nxt_pc = sigma_nxt)) ∨ 1471 (fetch_statement (m ake_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf)1467 (fetch_statement (mk_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 1472 1468 = 1473 1469 return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ∧ 1474 pc_of_label (m ake_sem_lin_params p p') …1470 pc_of_label (mk_sem_lin_params p p') … 1475 1471 (globalenv_noinit … lin_prog) 1476 1472 (pc_block pc) 1477 1473 nxt = return sigma_nxt) 1478 1474 ] 1479  final z ⇒ fetch_statement (m ake_sem_lin_params p p') …1475  final z ⇒ fetch_statement (mk_sem_lin_params p p') … 1480 1476 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 1481 1477 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … z〉 … … 2180 2176 ∀st,st',f,fn,stmt,nxt.no_call ?? stmt → 2181 2177 ∀prf : well_formed_state_pc … gss st. 2182 fetch_statement (m ake_sem_graph_params p p') …2178 fetch_statement (mk_sem_graph_params p p') … 2183 2179 (globalenv_noinit ? graph_prog) (pc … st) = 2184 2180 return 〈f, fn, sequential … (step_seq (mk_graph_params p) … stmt) nxt〉 → … … 2247 2243 (sigma_state p p' graph_prog sigma gss) 2248 2244 (λx.λ_ : True .x) 2249 (block_of_call (m ake_sem_graph_params p p') …2245 (block_of_call (mk_sem_graph_params p p') … 2250 2246 (globalenv_noinit ? graph_prog) cl) 2251 (block_of_call (m ake_sem_lin_params p p') …2247 (block_of_call (mk_sem_lin_params p p') … 2252 2248 (globalenv_noinit ? (linearise ? graph_prog)) cl). 2253 2249 #p #p' #graph_prog #sigma #gss #cl #st #prf … … 2295 2291 ∃prf. 2296 2292 sigma_pc p p' graph_prog sigma 2297 (pc_of_point (m ake_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf =2298 pc_of_point (m ake_sem_lin_params p p') bl 0.2293 (pc_of_point (mk_sem_graph_params p p') bl (joint_if_entry ?? fn1)) prf = 2294 pc_of_point (mk_sem_lin_params p p') bl 0. 2299 2295 #p #p' #graph_prog #sigma #good #bl #f1 #fn1 #fn1_spec 2300 2296 cases (good fn1) * #entry_in #_ #_ … … 2318 2314 ∀st,st',f,fn,called,args,dest,nxt. 2319 2315 ∀prf : well_formed_state_pc … gss st. 2320 fetch_statement (m ake_sem_graph_params p p') …2316 fetch_statement (mk_sem_graph_params p p') … 2321 2317 (globalenv_noinit ? graph_prog) (pc … st) = 2322 2318 return 〈f, fn, … … 2325 2321 return st' → 2326 2322 (* let st_pc' ≝ mk_state_pc ? st' 2327 (succ_pc (m ake_sem_graph_params p p') …2323 (succ_pc (mk_sem_graph_params p p') … 2328 2324 (pc … st) nxt) in 2329 2325 ∀prf'. 2330 fetch_statement (m ake_sem_lin_params p p') …2326 fetch_statement (mk_sem_lin_params p p') … 2331 2327 (globalenv_noinit … lin_prog) 2332 (succ_pc (m ake_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) =2328 (succ_pc (mk_sem_lin_params p p') (sigma_pc … (pc … st) (proj1 … prf)) it) = 2333 2329 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉 → 2334 pc_of_label (m ake_sem_lin_params p p') ?2330 pc_of_label (mk_sem_lin_params p p') ? 2335 2331 (globalenv_noinit ? (linearise p … graph_prog)) 2336 2332 (pc_block (pc … st)) 2337 2333 nxt = return sigma_pc p p' graph_prog sigma 2338 (succ_pc (m ake_sem_graph_params p p') (pc … st) nxt) prf' →*)2334 (succ_pc (mk_sem_graph_params p p') (pc … st) nxt) prf' →*) 2339 2335 let st2_pre_call ≝ sigma_state_pc … gss st prf in 2340 2336 ∃is_call, is_call'. … … 2432 2428 ∀st,st',f,fn,nxt. 2433 2429 ∀prf : well_formed_state_pc … gss st. 2434 fetch_statement (m ake_sem_graph_params p p') …2430 fetch_statement (mk_sem_graph_params p p') … 2435 2431 (globalenv_noinit ? graph_prog) (pc … st) = 2436 2432 return 〈f, fn, final … (GOTO (mk_graph_params p) … nxt)〉 → … … 2480 2476 ∀st,st',f,fn,a,ltrue,lfalse. 2481 2477 ∀prf : well_formed_state_pc … gss st. 2482 fetch_statement (m ake_sem_graph_params p p') …2478 fetch_statement (mk_sem_graph_params p p') … 2483 2479 (globalenv_noinit ? graph_prog) (pc … st) = 2484 2480 return 〈f, fn, sequential … (COND (mk_graph_params p) … a ltrue) lfalse〉 → … … 2551 2547 ∀st,st',f,fn. 2552 2548 ∀prf : well_formed_state_pc … gss st. 2553 fetch_statement (m ake_sem_graph_params p p') …2549 fetch_statement (mk_sem_graph_params p p') … 2554 2550 (globalenv_noinit ? graph_prog) (pc … st) = 2555 2551 return 〈f, fn, final … (RETURN (mk_graph_params p) … )〉 → … … 2659 2655 ∀st,st',f,fn,fl,called,args. 2660 2656 ∀prf : well_formed_state_pc … gss st. 2661 fetch_statement (m ake_sem_graph_params p p') …2657 fetch_statement (mk_sem_graph_params p p') … 2662 2658 (globalenv_noinit ? graph_prog) (pc … st) = 2663 2659 return 〈f, fn, final … (TAILCALL (mk_graph_params p) … fl called args)〉 → … … 2733 2729 qed. 2734 2730 2735 2736 2737 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝2738 ex1_intro: ∀ x:A. P x → ex_Type1 A P.2739 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)2740 2731 2741 2732 lemma linearise_ok: … … 2744 2735 ∀stack_sizes. 2745 2736 (∀sigma.good_state_sigma p p' graph_prog sigma) → 2746 ex_Type1 … (λR.2737 ∃[1] R. 2747 2738 status_simulation 2748 2739 (graph_abstract_status p p' graph_prog stack_sizes) … … 2768 2759 whd in ⊢ (%→?); 2769 2760 change with 2770 (eval_state (m ake_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?)2761 (eval_state (mk_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?) 2771 2762 #EQeval 2772 2763 @('bind_inversion EQeval)
Note: See TracChangeset
for help on using the changeset viewer.