Changeset 2543

Ignore:
Timestamp:
Dec 7, 2012, 11:35:19 AM (9 years ago)
Message:

finished stmt_at_sigma_commute

File:
1 edited

Unmodified
Added
Removed
• src/joint/lineariseProof.ma

 r2536 return sigma_regs p p' graph_prog sigma gsss r2 prf2 ; save_frame_commute : ∀dest,st1,st2,prf1. save_frame ?? (p' ?) dest st1 = return st2 → ∀b,dest,st1,st2,prf1. save_frame ?? (p' ?) b dest st1 = return st2 → let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1)) (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in ∃prf2. save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2 save_frame ?? (p' ?) b dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2 ; allocate_locals_commute : ∀ loc, r1, prf1. ∃ prf2. stmt_at … graph_code lbl = return stmt → stmt_at ?? lin_code pt = return graph_to_lin_statement … stmt ∧ All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧ match stmt with [ final stmt ⇒ True | sequential stmt nxt ⇒ (sigma nxt = Some ? (S pt) ∨ (stmt_at ?? lin_code (S pt) = return final (mk_lin_params p) … (GOTO … nxt))) [ final s' ⇒ stmt_at … lin_code pt = Some ? (final … s') | sequential s' nxt ⇒ match s' with [ step_seq _ ⇒ (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧ ((sigma nxt = Some ? (S pt)) ∨ (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt))) | COND a ltrue ⇒ (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S pt)) ∨ (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt)) ] | FCOND abs _ _ _ ⇒ Ⓧabs ]. #p #globals #graph_code #entry #lin_code #lbl #pt #sigma * #_ #lin_stmt_spec #prf elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 *** #EQstmt_at elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 ** #stmt1_spec #All_succs_in #next_spec #EQstmt_at_graph_stmt #stmt >EQstmt_at whd in ⊢ (??%%→?); #EQ destruct(EQ) % [ % assumption ] cases stmt in next_spec; -stmt normalize nodelta [2: // ] #stmt #nxt whd in match opt_All; whd in match stmt_implicit_label; normalize nodelta // #stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ) % [assumption] // qed. fetch_statement (make_sem_graph_params p p') … (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), graph_to_lin_statement … stmt〉 ∧ All ? (λlbl.well_formed_pc p p' graph_prog sigma (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl)) (stmt_explicit_labels … stmt) ∧ (stmt_explicit_labels … stmt) ∧ match stmt with [ sequential stmt nxt ⇒ ∃prf'. let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) nxt_pc = return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) | final stmt ⇒ True [  sequential s nxt ⇒ match s with [ step_seq x ⇒ fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ ∃prf'. let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) nxt_pc = return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) | COND a ltrue ⇒ (∃ prf'. let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in (fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧ nxt_pc = sigma_nxt)) ∨ fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 ] | final z ⇒   fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = return 〈f, \fst (linearise_int_fun … fn), final  (mk_lin_params p) … z〉 | FCOND abs _ _ _ ⇒ Ⓧabs ]. #p #p' #graph_prog #pc #f #fn #stmt #sigma #good elim (good fn) * #_ #all_labels_in #good_local #wfprf #H elim (fetch_statement_inv … H) #fetchfn #graph_stmt whd in match fetch_statement; normalize nodelta >sigma_pblock_eq_lemma #p #p' #graph_prog #pc #f #fn #stmt #sigma #good elim (good fn) * #_ #all_labels_in #good_local #wfprf #H elim (fetch_statement_inv … H) #fetchfn #graph_stmt whd in match well_formed_pc in wfprf; normalize nodelta in wfprf; inversion(sigma_pc_opt p p' graph_prog sigma pc) [#ABS @⊥ >ABS in wfprf; * #H @H %] #lin_pc #lin_pc_spec whd in match sigma_pc_opt in lin_pc_spec; normalize nodelta in lin_pc_spec; @('bind_inversion lin_pc_spec) * #id #graph_fun >fetchfn #EQ whd in EQ : (??%?); destruct(EQ) #H @('bind_inversion H) -H #lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ) lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt) [@lin_pt_spec|] * #H1 #H2 % [ -H2 @(All_mp … (All_append_r … H1)) #lab #lab_spec whd in match well_formed_pc; normalize nodelta whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind whd in match point_of_pc; whd in match pc_of_point; normalize nodelta >point_of_offset_of_point cases(sigma graph_fun lab) in lab_spec; [* #ABS @⊥ @ABS %] #linear_pt #_ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS) ] lapply H2 cases (stmt) in H1; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta #all_labels_spec #H3 whd in match fetch_statement; normalize nodelta >sigma_pblock_eq_lemma >(fetch_internal_function_transf … fetchfn) >m_return_bind whd in match sigma_pc; normalize nodelta @opt_safe_elim #lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta >fetchfn in ⊢ (%→?); >m_return_bind inversion (sigma ??) [ #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ] #lin_pt #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ) cases (stmt_at_sigma_commute … (good fn) … EQsigma … graph_stmt) * #H1 #H2 #H3 % [ % ] [ whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >H1 % | @(All_mp … (All_append_r … H2)) #lbl #prf' whd whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind >point_of_pc_of_point >(opt_to_opt_safe … prf') % normalize #ABS destruct(ABS) | cases stmt in H2 H3; normalize nodelta [2: // ] -stmt #stmt #nxt * #next_in #_ #nxt_spec % [ @hide_prf whd % | @opt_safe_elim #pc' ] >graph_succ_pc whd in ⊢ (??%?→?); >fetchfn normalize nodelta >point_of_pc_of_point >(opt_to_opt_safe … next_in) whd in ⊢ (??%?→?); #EQ destruct(EQ) cases nxt_spec [ #EQsigma_nxt %1 whd in match (succ_pc ???); whd in match point_of_pc; normalize nodelta >point_of_offset_of_point lapply next_in >EQsigma_nxt #N % | #EQstmt_at_nxt %2 whd in match (succ_pc ???); >(fetch_internal_function_transf … fetchfn) >m_return_bind whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >point_of_offset_of_point whd in match (point_of_succ ???); >EQstmt_at_nxt % ] ] qed. [ % [ whd in match point_of_pc; whd in match sigma_pc; normalize nodelta @opt_safe_elim #linear_pc whd in match sigma_pc_opt; normalize nodelta >lin_pc_spec #EQ destruct(EQ) >point_of_offset_of_point >(proj1 … H3) >m_return_bind // | % [ @hide_prf whd in match well_formed_pc; whd in match sigma_pc_opt; normalize nodelta lapply fetchfn whd in match fetch_internal_function; normalize nodelta #H4 @('bind_inversion H4) #x #x_spec >x_spec >m_return_bind #EQ >EQ >m_return_bind whd in match pc_of_point; whd in match succ_pc; whd in match point_of_pc; whd in match pc_of_point; normalize nodelta >point_of_offset_of_point cases(proj2 … H3)[ #EQ >EQ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)] lapply all_labels_spec #Z lapply(All_nth ? ? 0 ? Z nxt) whd in match stmt_labels; normalize nodelta #Z1 normalize in Z1; lapply(Z1 ?) [%] inversion(sigma ??) [#_ #ABS @⊥ elim ABS #ABS @ABS %] #sn #sigma_graph_f_spec >sigma_graph_f_spec #_ #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS) | cases(proj2 … H3) [ #Z %1 whd in match sigma_pc; normalize nodelta @opt_safe_elim #pc1 whd in match sigma_pc_opt; normalize nodelta >lin_pc_spec #EQ destruct(EQ) @opt_safe_elim #pc2 >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta whd in match pc_of_point; normalize nodelta >point_of_offset_of_point >Z >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; whd in match point_of_succ; normalize nodelta >point_of_offset_of_point % | #Z %2 lapply fetchfn whd in match fetch_internal_function; normalize nodelta #H @('bind_inversion H) -H * #x1 #x2 #x_spec lapply(fetch_function_transf ???? graph_prog (λglobals.transf_fundef ??(λf_in.\fst (linearise_int_fun p globals f_in))) ?? ? x_spec) #HH HH >m_return_bind cases x2 normalize nodelta [#g_fun | #xxx] #EQ whd in EQ : (??%%); destruct(EQ) >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta whd in match pc_of_point; normalize nodelta  >point_of_offset_of_point whd in match sigma_pc; normalize nodelta @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >Z >m_return_bind % ] ] ] | cases H3 [ * #Z1 #Z2 %1 % [ @hide_prf  whd in match well_formed_pc; normalize nodelta whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta whd in match pc_of_point; normalize nodelta >point_of_offset_of_point >Z2 >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS) ] % [ whd in match sigma_pc; normalize nodelta @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >Z1 >m_return_bind % | whd in match sigma_pc; normalize nodelta @opt_safe_elim #line_pc @opt_safe_elim #line_succ_pc whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta  >point_of_offset_of_point >Z2 >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) whd in match pc_of_point; whd in match point_of_pc; normalize nodelta >point_of_offset_of_point % ] | #Z %2 whd in match sigma_pc; normalize nodelta >fetchfn >m_return_bind @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >Z >m_return_bind % ] | whd in match sigma_pc; normalize nodelta @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta  >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point >H3 >m_return_bind % ] qed. lemma point_of_pc_sigma_commute : #res #_ #H lapply (res_eq_from_opt ??? H) -H cases daemon (*#H elim (bind_inversion ????? H) in ⊢ ?; * #f #stmt * whd in ⊢ (??%?→?);*) #H  @('bind_inversion H) -H * #f #stmt whd in match fetch_statement; normalize nodelta #H @('bind_inversion H) -H * #id #int_f whd in match fetch_internal_function; normalize nodelta #H @('bind_inversion H) -H * #id1 #int_f1 whd in match fetch_function; normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #id2 whd in match symbol_for_block; normalize nodelta whd in match option_map; normalize nodelta cases (find ?? (symbols ? ?) ?) normalize nodelta [1,3: #ABS destruct(ABS)] #sy_bl #EQ destruct(EQ) #H @('bind_inversion H) -H #int_f2 whd in match find_funct_ptr; normalize nodelta cases(block_region (pc_block (pc ? ?))) normalize nodelta [1,3: #ABS destruct(ABS)] cases(block_id (pc_block (pc ??))) normalize nodelta [1,2,4,5: [2,4: #pos] #ABS destruct(ABS)] #pos #int_f2_spec #EQ whd in EQ : (??%?); destruct(EQ) cases int_f1 in int_f2_spec; normalize nodelta [2,4: #ext_f #_ #ABS whd in ABS : (???%); destruct(ABS)] #int_f3 #int_f3_spec #EQ whd in EQ : (??%%); destruct(EQ) #H @('bind_inversion H) -H #stmt1 #H lapply(opt_eq_from_res ???? H) -H #stmt1_spec #EQ whd in EQ : (??%%); destruct(EQ) cases (stmt) in stmt1_spec; normalize nodelta [1,3,4,6: [1,3: #js #jsucc #_ | 2,4: #a #b #c #d #_] #ABS whd in ABS : (???%); destruct(ABS)] #fin_step #fin_step_spec cases (fin_step) in fin_step_spec; normalize nodelta [1,3,4,6: [1,3: #l #_|2,4: #a #b #c #_] #ABS whd in ABS : (???%); destruct(ABS)] #STMT_SPEC #H @('bind_inversion H) -H #state_pc #state_pc_sepc #H @('bind_inversion H) -H #succ_pc whd in match next_of_pc; normalize nodelta #H @('bind_inversion H) -H * #id4 #int_f4 whd in match fetch_statement; normalize nodelta #H @('bind_inversion H) -H * #id5 #int_f5 whd in match fetch_internal_function; normalize nodelta #H @('bind_inversion H) -H * #id6 #int_f6 whd in match fetch_function; normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #id7 whd in match symbol_for_block; normalize nodelta whd in match option_map; normalize nodelta cases(find ? ? ? ?) normalize nodelta [1,3: #ABS destruct(ABS)] #sy_bl1 #EQ destruct(EQ) #H @('bind_inversion H) -H #int_f7 whd in match find_funct_ptr; normalize nodelta cases(block_region (pc_block ?)) normalize nodelta [1,3: #ABS destruct(ABS)] cases(block_id ?) normalize nodelta [1,2,4,5: [2,4:#p] #ABS destruct(ABS)] #pos1 #int_f7_spec #EQ whd in EQ : (??%?); destruct(EQ) cases (int_f6) in int_f7_spec; normalize nodelta [2,4: #ext_fun #_ #ABS whd in ABS : (???%); destruct(ABS)] #int_f8 #int_f8_spec #EQ whd in EQ : (??%%); destruct(EQ) #H @('bind_inversion H) -H #stmt2 #H lapply(opt_eq_from_res ???? H) -H #stmt2_spec #EQ whd in EQ : (??%%); destruct(EQ) cases int_f4 in stmt2_spec; normalize nodelta [2,3,5,6: xxxxxxxxxxxxxx qed.
Note: See TracChangeset for help on using the changeset viewer.