Changeset 2543
 Timestamp:
 Dec 7, 2012, 11:35:19 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2536 r2543 539 539 return sigma_regs p p' graph_prog sigma gsss r2 prf2 540 540 ; save_frame_commute : 541 ∀ dest,st1,st2,prf1.542 save_frame ?? (p' ?) dest st1 = return st2 →541 ∀b,dest,st1,st2,prf1. 542 save_frame ?? (p' ?) b dest st1 = return st2 → 543 543 let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1)) 544 544 (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in 545 545 ∃prf2. 546 save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2546 save_frame ?? (p' ?) b dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2 547 547 ; allocate_locals_commute : 548 548 ∀ loc, r1, prf1. ∃ prf2. … … 981 981 stmt_at … graph_code 982 982 lbl = return stmt → 983 stmt_at ?? lin_code984 pt = return graph_to_lin_statement … stmt ∧985 983 All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧ 986 984 match stmt with 987 [ final stmt ⇒ True 988  sequential stmt nxt ⇒ 989 (sigma nxt = Some ? (S pt) ∨ 990 (stmt_at ?? lin_code 991 (S pt) = return final (mk_lin_params p) … (GOTO … nxt))) 985 [ final s' ⇒ stmt_at … lin_code pt = Some ? (final … s') 986  sequential s' nxt ⇒ 987 match s' with 988 [ step_seq _ ⇒ 989 (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧ 990 ((sigma nxt = Some ? (S pt)) ∨ 991 (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt))) 992  COND a ltrue ⇒ 993 (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧ 994 sigma nxt = Some ? (S pt)) ∨ 995 (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt)) 996 ] 997  FCOND abs _ _ _ ⇒ Ⓧabs 992 998 ]. 993 999 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma 994 1000 * #_ #lin_stmt_spec #prf 995 elim (lin_stmt_spec … prf) lin_stmt_spec #stmt1 ** * #EQstmt_at1001 elim (lin_stmt_spec … prf) lin_stmt_spec #stmt1 ** #stmt1_spec 996 1002 #All_succs_in #next_spec 997 #EQstmt_at_graph_stmt 998 #stmt >EQstmt_at 999 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1000 % [ % assumption ] 1001 cases stmt in next_spec; stmt normalize nodelta [2: // ] 1002 #stmt #nxt 1003 whd in match opt_All; 1004 whd in match stmt_implicit_label; 1005 normalize nodelta // 1003 #stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ) 1004 % [assumption] 1005 // 1006 1006 qed. 1007 1007 … … 1097 1097 fetch_statement (make_sem_graph_params p p') … 1098 1098 (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → 1099 fetch_statement (make_sem_lin_params p p') …1100 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) =1101 return 〈f, \fst (linearise_int_fun … fn), graph_to_lin_statement … stmt〉 ∧1102 1099 All ? (λlbl.well_formed_pc p p' graph_prog sigma 1103 1100 (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl)) 1104 (stmt_explicit_labels … stmt) ∧ 1101 (stmt_explicit_labels … stmt) ∧ 1105 1102 match stmt with 1106 [ sequential stmt nxt ⇒ 1107 ∃prf'. 1108 let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in 1109 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 1110 (nxt_pc = sigma_nxt ∨ 1111 fetch_statement (make_sem_lin_params p p') … 1112 (globalenv_noinit … lin_prog) nxt_pc = 1113 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) 1114  final stmt ⇒ True 1103 [ sequential s nxt ⇒ 1104 match s with 1105 [ step_seq x ⇒ 1106 fetch_statement (make_sem_lin_params p p') … 1107 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 1108 return 〈f, \fst (linearise_int_fun … fn), 1109 sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ 1110 ∃prf'. 1111 let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in 1112 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 1113 (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') … 1114 (globalenv_noinit … lin_prog) nxt_pc = 1115 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) 1116  COND a ltrue ⇒ 1117 (∃ prf'. 1118 let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in 1119 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 1120 (fetch_statement (make_sem_lin_params p p') … 1121 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 1122 return 〈f, \fst (linearise_int_fun … fn), 1123 sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧ 1124 nxt_pc = sigma_nxt)) ∨ 1125 fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) 1126 = 1127 return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 1128 ] 1129  final z ⇒ fetch_statement (make_sem_lin_params p p') … 1130 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 1131 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … z〉 1132  FCOND abs _ _ _ ⇒ Ⓧabs 1115 1133 ]. 1116 #p #p' #graph_prog #pc #f #fn #stmt #sigma #good 1117 elim (good fn) * #_ #all_labels_in #good_local #wfprf 1118 #H 1119 elim (fetch_statement_inv … H) 1120 #fetchfn #graph_stmt 1121 whd in match fetch_statement; normalize nodelta 1122 >sigma_pblock_eq_lemma 1134 #p #p' #graph_prog #pc #f #fn #stmt #sigma 1135 #good elim (good fn) * #_ #all_labels_in #good_local #wfprf 1136 #H elim (fetch_statement_inv … H) #fetchfn #graph_stmt 1137 whd in match well_formed_pc in wfprf; normalize nodelta in wfprf; 1138 inversion(sigma_pc_opt p p' graph_prog sigma pc) 1139 [#ABS @⊥ >ABS in wfprf; * #H @H %] 1140 #lin_pc #lin_pc_spec 1141 whd in match sigma_pc_opt in lin_pc_spec; normalize nodelta in lin_pc_spec; 1142 @('bind_inversion lin_pc_spec) * #id #graph_fun >fetchfn 1143 #EQ whd in EQ : (??%?); destruct(EQ) #H @('bind_inversion H) H 1144 #lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ) 1145 lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt) 1146 [@lin_pt_spec] * #H1 #H2 % 1147 [ H2 @(All_mp … (All_append_r … H1)) #lab #lab_spec 1148 whd in match well_formed_pc; normalize nodelta 1149 whd in match sigma_pc_opt; normalize nodelta >fetchfn 1150 >m_return_bind whd in match point_of_pc; whd in match pc_of_point; 1151 normalize nodelta >point_of_offset_of_point 1152 cases(sigma graph_fun lab) in lab_spec; [* #ABS @⊥ @ABS %] 1153 #linear_pt #_ >m_return_bind whd in ⊢ (?(??%?)); 1154 % #ABS destruct(ABS) 1155 ] lapply H2 1156 cases (stmt) in H1; [ * [ #s  #a #ltrue ] #nxt  #s  * ] normalize nodelta 1157 #all_labels_spec #H3 whd in match fetch_statement; normalize nodelta 1158 >sigma_pblock_eq_lemma 1123 1159 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1124 whd in match sigma_pc; normalize nodelta @opt_safe_elim 1125 #lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta 1126 >fetchfn in ⊢ (%→?); >m_return_bind 1127 inversion (sigma ??) 1128 [ #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ] 1129 #lin_pt #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ) 1130 cases (stmt_at_sigma_commute … (good fn) … EQsigma … graph_stmt) * 1131 #H1 #H2 #H3 % [ % ] 1132 [ whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1133 >H1 % 1134  @(All_mp … (All_append_r … H2)) #lbl #prf' 1135 whd whd in match sigma_pc_opt; normalize nodelta 1136 >fetchfn >m_return_bind >point_of_pc_of_point 1137 >(opt_to_opt_safe … prf') % normalize 1138 #ABS destruct(ABS) 1139  cases stmt in H2 H3; normalize nodelta [2: // ] 1140 stmt #stmt #nxt * #next_in #_ #nxt_spec 1141 % 1142 [ @hide_prf whd % 1143  @opt_safe_elim #pc' 1144 ] 1145 >graph_succ_pc whd in ⊢ (??%?→?); 1146 >fetchfn normalize nodelta >point_of_pc_of_point 1147 >(opt_to_opt_safe … next_in) whd in ⊢ (??%?→?); #EQ destruct(EQ) 1148 cases nxt_spec 1149 [ #EQsigma_nxt %1 1150 whd in match (succ_pc ???); whd in match point_of_pc; normalize nodelta 1151 >point_of_offset_of_point lapply next_in >EQsigma_nxt #N % 1152  #EQstmt_at_nxt %2 1153 whd in match (succ_pc ???); 1154 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1155 whd in match point_of_pc; 1156 normalize nodelta >point_of_offset_of_point >point_of_offset_of_point 1157 whd in match (point_of_succ ???); 1158 >EQstmt_at_nxt % 1159 ] 1160 ] 1161 qed. 1160 [ % 1161 [ whd in match point_of_pc; whd in match sigma_pc; normalize nodelta 1162 @opt_safe_elim #linear_pc whd in match sigma_pc_opt; normalize nodelta 1163 >lin_pc_spec #EQ destruct(EQ) >point_of_offset_of_point 1164 >(proj1 … H3) >m_return_bind // 1165  1166 % 1167 [ @hide_prf whd in match well_formed_pc; whd in match sigma_pc_opt; 1168 normalize nodelta lapply fetchfn 1169 whd in match fetch_internal_function; normalize nodelta 1170 #H4 @('bind_inversion H4) #x #x_spec 1171 >x_spec >m_return_bind #EQ >EQ >m_return_bind 1172 whd in match pc_of_point; whd in match succ_pc; whd in match point_of_pc; 1173 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1174 cases(proj2 … H3)[ #EQ >EQ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)] 1175 lapply all_labels_spec #Z 1176 lapply(All_nth ? ? 0 ? Z nxt) whd in match stmt_labels; normalize nodelta 1177 #Z1 normalize in Z1; lapply(Z1 ?) [%] inversion(sigma ??) 1178 [#_ #ABS @⊥ elim ABS #ABS @ABS %] #sn #sigma_graph_f_spec >sigma_graph_f_spec 1179 #_ #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS) 1180  cases(proj2 … H3) 1181 [ #Z %1 whd in match sigma_pc; normalize nodelta 1182 @opt_safe_elim #pc1 whd in match sigma_pc_opt; normalize nodelta 1183 >lin_pc_spec #EQ destruct(EQ) 1184 @opt_safe_elim #pc2 >fetchfn >m_return_bind 1185 whd in match point_of_pc; whd in match succ_pc; normalize nodelta 1186 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1187 >Z >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) 1188 whd in match point_of_pc; whd in match point_of_succ; normalize nodelta 1189 >point_of_offset_of_point % 1190  #Z %2 lapply fetchfn whd in match fetch_internal_function; normalize nodelta 1191 #H @('bind_inversion H) H * #x1 #x2 #x_spec 1192 lapply(fetch_function_transf ???? graph_prog 1193 (λglobals.transf_fundef ??(λf_in.\fst (linearise_int_fun p globals f_in))) ?? ? x_spec) 1194 #HH 1195 <sigma_pblock_eq_lemma in HH; [2:@wfprf] #HH >HH >m_return_bind 1196 cases x2 normalize nodelta [#g_fun  #xxx] #EQ whd in EQ : (??%%); destruct(EQ) 1197 >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta 1198 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1199 whd in match sigma_pc; normalize nodelta 1200 @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta 1201 >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); 1202 destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1203 >Z >m_return_bind % 1204 ] 1205 ] 1206 ] 1207  cases H3 1208 [ * #Z1 #Z2 %1 % [ @hide_prf whd in match well_formed_pc; normalize nodelta 1209 whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind 1210 whd in match point_of_pc; whd in match succ_pc; normalize nodelta 1211 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1212 >Z2 >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS) 1213 ] % 1214 [ whd in match sigma_pc; normalize nodelta 1215 @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta 1216 >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); 1217 destruct(EQ) whd in match point_of_pc; normalize nodelta 1218 >point_of_offset_of_point >Z1 >m_return_bind % 1219  whd in match sigma_pc; normalize nodelta 1220 @opt_safe_elim #line_pc 1221 @opt_safe_elim #line_succ_pc whd in match sigma_pc_opt; normalize nodelta 1222 >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; 1223 normalize nodelta >point_of_offset_of_point >Z2 >m_return_bind 1224 #EQ whd in EQ : (??%?); destruct(EQ) >m_return_bind >lin_pt_spec >m_return_bind 1225 #EQ whd in EQ : (??%?); destruct(EQ) whd in match pc_of_point; whd in match point_of_pc; 1226 normalize nodelta >point_of_offset_of_point % 1227 ] 1228  #Z %2 whd in match sigma_pc; normalize nodelta >fetchfn >m_return_bind 1229 @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta 1230 >fetchfn >m_return_bind >lin_pt_spec >m_return_bind 1231 #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta 1232 >point_of_offset_of_point >Z >m_return_bind % 1233 ] 1234  whd in match sigma_pc; normalize nodelta @opt_safe_elim 1235 #line_pc whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind 1236 >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) 1237 whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1238 >H3 >m_return_bind % 1239 ] 1240 qed. 1162 1241 1163 1242 lemma point_of_pc_sigma_commute : … … 1202 1281 #res #_ 1203 1282 #H lapply (res_eq_from_opt ??? H) H 1204 cases daemon 1205 (*#H elim (bind_inversion ????? H) in ⊢ ?; 1206 * #f #stmt * 1207 whd in ⊢ (??%?→?);*) 1283 #H @('bind_inversion H) H 1284 * #f #stmt 1285 whd in match fetch_statement; normalize nodelta 1286 #H @('bind_inversion H) H * 1287 #id #int_f 1288 whd in match fetch_internal_function; normalize nodelta 1289 #H @('bind_inversion H) H * #id1 #int_f1 1290 whd in match fetch_function; normalize nodelta 1291 #H lapply(opt_eq_from_res ???? H) H 1292 #H @('bind_inversion H) H #id2 1293 whd in match symbol_for_block; normalize nodelta 1294 whd in match option_map; normalize nodelta 1295 cases (find ?? (symbols ? ?) ?) normalize nodelta 1296 [1,3: #ABS destruct(ABS)] #sy_bl #EQ destruct(EQ) 1297 #H @('bind_inversion H) H #int_f2 whd in match find_funct_ptr; 1298 normalize nodelta cases(block_region (pc_block (pc ? ?))) 1299 normalize nodelta [1,3: #ABS destruct(ABS)] 1300 cases(block_id (pc_block (pc ??))) normalize nodelta 1301 [1,2,4,5: [2,4: #pos] #ABS destruct(ABS)] 1302 #pos #int_f2_spec #EQ whd in EQ : (??%?); destruct(EQ) 1303 cases int_f1 in int_f2_spec; normalize nodelta 1304 [2,4: #ext_f #_ #ABS whd in ABS : (???%); destruct(ABS)] 1305 #int_f3 #int_f3_spec #EQ whd in EQ : (??%%); destruct(EQ) 1306 #H @('bind_inversion H) H #stmt1 #H lapply(opt_eq_from_res ???? H) H 1307 #stmt1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1308 cases (stmt) in stmt1_spec; normalize nodelta 1309 [1,3,4,6: [1,3: #js #jsucc #_  2,4: #a #b #c #d #_] #ABS whd in ABS : (???%); 1310 destruct(ABS)] 1311 #fin_step #fin_step_spec cases (fin_step) in fin_step_spec; normalize nodelta 1312 [1,3,4,6: [1,3: #l #_2,4: #a #b #c #_] #ABS whd in ABS : (???%); destruct(ABS)] 1313 #STMT_SPEC #H @('bind_inversion H) H #state_pc #state_pc_sepc 1314 #H @('bind_inversion H) H #succ_pc whd in match next_of_pc; normalize nodelta 1315 #H @('bind_inversion H) H * #id4 #int_f4 whd in match fetch_statement; normalize nodelta 1316 #H @('bind_inversion H) H * #id5 #int_f5 whd in match fetch_internal_function; normalize nodelta 1317 #H @('bind_inversion H) H * #id6 #int_f6 whd in match fetch_function; normalize nodelta 1318 #H lapply(opt_eq_from_res ???? H) H #H @('bind_inversion H) H #id7 1319 whd in match symbol_for_block; normalize nodelta whd in match option_map; normalize nodelta 1320 cases(find ? ? ? ?) normalize nodelta [1,3: #ABS destruct(ABS)] 1321 #sy_bl1 #EQ destruct(EQ) #H @('bind_inversion H) H #int_f7 1322 whd in match find_funct_ptr; normalize nodelta 1323 cases(block_region (pc_block ?)) normalize nodelta [1,3: #ABS destruct(ABS)] 1324 cases(block_id ?) normalize nodelta [1,2,4,5: [2,4:#p] #ABS destruct(ABS)] 1325 #pos1 #int_f7_spec #EQ whd in EQ : (??%?); destruct(EQ) cases (int_f6) in int_f7_spec; 1326 normalize nodelta [2,4: #ext_fun #_ #ABS whd in ABS : (???%); destruct(ABS)] 1327 #int_f8 #int_f8_spec #EQ whd in EQ : (??%%); destruct(EQ) 1328 #H @('bind_inversion H) H #stmt2 #H lapply(opt_eq_from_res ???? H) H 1329 #stmt2_spec #EQ whd in EQ : (??%%); destruct(EQ) 1330 cases int_f4 in stmt2_spec; normalize nodelta 1331 [2,3,5,6: 1332 1333 xxxxxxxxxxxxxx 1334 1208 1335 qed. 1209 1336
Note: See TracChangeset
for help on using the changeset viewer.