Changeset 2551
 Timestamp:
 Dec 10, 2012, 8:11:35 PM (8 years ago)
 Location:
 src/joint
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2548 r2551 18 18 include "joint/semanticsUtils.ma". 19 19 20 axiom globalenv_no_minus_one : 21 ∀F,V,i,p. 22 find_funct_ptr … (globalenv F V i p) (mk_block Code (1)) = None ?. 23 24 lemma fetch_internal_function_no_minus_one : 25 ∀F,V,i,p,bl. 26 block_id (pi1 … bl) = 1 → 27 fetch_internal_function … (globalenv (λvars.fundef (F vars)) V i p) 28 bl = Error … [MSG BadFunction]. 29 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct 30 whd in match fetch_internal_function; 31 whd in match fetch_function; normalize nodelta 32 >globalenv_no_minus_one 33 cases (symbol_for_block ???) normalize // 34 qed. 35 20 36 lemma bind_option_inversion_star: 21 37 ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B. … … 224 240 joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) → 225 241 label → option ℕ. 226 242 227 243 definition sigma_pc_opt: 228 244 ∀p,p'.∀graph_prog. … … 233 249 let pars ≝ make_sem_graph_params p p' in 234 250 let ge ≝ globalenv_noinit … prog in 235 ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ; 236 ! lin_point ← sigma fd (point_of_pc pars pc) ; 237 return pc_of_point 238 (make_sem_lin_params ? p') (pc_block pc) lin_point. 251 if eqZb (block_id (pc_block pc)) (1) then (* check for dummy exit pc *) 252 return pc 253 else 254 ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ; 255 ! lin_point ← sigma fd (point_of_pc pars pc) ; 256 return pc_of_point 257 (make_sem_lin_params ? p') (pc_block pc) lin_point. 239 258 240 259 definition well_formed_pc: … … 448 467 % 449 468 [2: whd in ⊢ (???%); 450 cut (∀X,a,b.a = b → Some X a = Some X b) [ // ] 451 #aux @aux 469 @eq_f 452 470 @mem_ext_eq [2: % ] 453 471 #b @if_elim … … 724 742 (eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 725 743 ext i (\fst (linearise_int_fun … fn))) 726 }.727 (* TO BE ADAPTED AS ABOVE728 744 ; setup_call_commute : 729 ∀ n , parsT, call_args , st1 , st2 , prf1. 730 setup_call ?? (p' ?) n parsT call_args st1 = return st2 → 731 ∃prf2. 732 setup_call ?? (p' ?) n parsT call_args (sigma_state p p' graph_prog sigma gsss st1 prf1) = 733 return (sigma_state p p' graph_prog sigma gsss st2 prf2) 745 ∀ n , parsT, call_args. 746 preserving … res_preserve … 747 (sigma_state … gsss) 748 (sigma_state … gsss) 749 (setup_call ?? (p' ?) n parsT call_args) 750 (setup_call ?? (p' ?) n parsT call_args) 734 751 ; fetch_external_args_commute : (* TO BE CHECKED *) 735 752 ∀ex_fun,st1,prf1,call_args. … … 737 754 fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args 738 755 ; set_result_commute : 739 ∀ l , call_dest , st1 , st2 , prf1. 740 set_result ?? (p' ?) l call_dest st1 = return st2 → 741 ∃prf2. 742 set_result ?? (p' ?) l call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = 743 return (sigma_state p p' graph_prog sigma gsss st2 prf2) 756 ∀ l , call_dest. 757 preserving … res_preserve … 758 (sigma_state … gsss) 759 (sigma_state … gsss) 760 (set_result ?? (p' ?) l call_dest) 761 (set_result ?? (p' ?) l call_dest) 744 762 ; read_result_commute : 745 763 let lin_prog ≝ linearise p graph_prog in 746 764 ∀stack_sizes. 747 ∀call_dest , st1 , prf1, l1. 748 read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 749 call_dest st1 = return l1 → 750 ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?. 751 read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 752 call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = return opt_safe … prf 765 ∀call_dest. 766 preserving … res_preserve … 767 (sigma_state … gsss) 768 (λl,prf.opt_safe ? (m_list_map … (sigma_beval_opt p p' graph_prog sigma) l) prf) 769 (read_result ?? (p' ?) ? (ev_genv (graph_prog_params … graph_prog stack_sizes)) 770 call_dest) 771 (read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 772 call_dest) 753 773 ; pop_frame_commute : 754 774 let lin_prog ≝ linearise p graph_prog in 755 ∀stack_sizes. 756 ∀ st1 , prf1, curr_id , curr_fn ,st2. 757 pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 758 curr_id curr_fn st1 = return st2 → 759 ∃prf2. 760 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in 761 let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in 762 pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 763 curr_id (\fst (linearise_int_fun … curr_fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) = 764 return mk_state_pc ? st2' pc' 775 ∀stack_sizes, curr_id , curr_fn. 776 preserving … res_preserve … 777 (sigma_state … gsss) 778 (λst : state_pc ?.λprf. 779 mk_state_pc … 780 (sigma_state … gsss st (proj2 ?? prf)) 781 (sigma_pc p p' graph_prog sigma (pc … st) (proj1 ?? prf))) 782 (pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 783 curr_id curr_fn) 784 (pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 785 curr_id (\fst (linearise_int_fun … curr_fn))) 765 786 }. 766 *)767 768 769 770 771 787 772 788 lemma store_commute : … … 855 871 @prog_if_of_function_transform % qed. 856 872 *) 857 lemma sigma_pblock_eq_lemma:873 lemma pc_block_sigma_commute : 858 874 ∀p,p',graph_prog. 859 875 let lin_prog ≝ linearise p graph_prog in … … 863 879 pc_block pc. 864 880 #p #p' #graph_prog #sigma #pc #prf 865 whd in match sigma_pc; normalize nodelta 866 @opt_safe_elim #x #H @('bind_inversion H) H * #i #fn #_ 867 #H @('bind_inversion H) H #n #_ whd in ⊢ (??%?→?); 881 whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta 882 @opt_safe_elim #x 883 @if_elim #_ 884 [2: #H @('bind_inversion H) H * #i #fn #_ 885 #H @('bind_inversion H) H #n #_ ] 886 whd in ⊢ (??%?→?); 868 887 #EQ destruct % 869 888 qed. … … 1111 1130 ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma. 1112 1131 good_local_sigma p globals graph_code entry lin_code sigma → 1132 code_closed … lin_code → 1113 1133 sigma lbl = return pt → 1114 1134 ∀stmt. … … 1123 1143 (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧ 1124 1144 ((sigma nxt = Some ? (S pt)) ∨ 1125 (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt))) 1145 (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt) ∧ 1146 point_of_label … lin_code nxt = sigma nxt) ) 1126 1147  COND a ltrue ⇒ 1127 1148 (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧ 1128 1149 sigma nxt = Some ? (S pt)) ∨ 1129 (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt)) 1150 (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt) ∧ 1151 point_of_label … lin_code nxt = sigma nxt) 1130 1152 ] 1131 1153  FCOND abs _ _ _ ⇒ Ⓧabs 1132 1154 ]. 1133 1155 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma 1134 * #_ #lin_stmt_spec#prf1156 ** #_ #all_labels_in #lin_stmt_spec #lin_code_closed #prf 1135 1157 elim (lin_stmt_spec … prf) lin_stmt_spec #stmt1 ** #stmt1_spec 1136 1158 #All_succs_in #next_spec 1137 1159 #stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ) 1138 1160 % [assumption] 1139 // 1161 cases stmt in next_spec; stmt 1162 [ * [ #s  #a #lbl ] #nxt  #s  * ] 1163 normalize nodelta 1164 [ * #H #G %{H} 1165 cases G G #G 1166 [ %1{G} ] 1167  * [ #H %1{H} ] #G 1168  // 1169 ] %2 %{G} 1170 lapply (refl … (point_of_label … lin_code nxt)) 1171 change with (If ? then with prf do ? else ?) in ⊢ (???%→?); 1172 @If_elim <(lin_code_has_label … (mk_lin_params p)) 1173 [1,3: #_ #EQ >EQ >(all_labels_in … EQ) % ] 1174 * #H cases (H ?) H 1175 lapply (lin_code_closed … G) ** [2: #_ * ] // 1140 1176 qed. 1141 1177 … … 1198 1234 @opt_safe_elim #pc' 1199 1235 ] 1200 whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind 1201 >point_of_pc_of_point 1202 >EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) % 1236 whd in match sigma_pc_opt; normalize nodelta 1237 @eqZb_elim #Hbl normalize nodelta 1238 [1,3: >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; 1239 *: >fetchfn >m_return_bind 1240 >point_of_pc_of_point 1241 >EQsigma 1242 ] whd in ⊢ (??%%→?); #EQ destruct(EQ) % 1203 1243 ] 1204 1244 qed. … … 1215 1255 qed. 1216 1256 1257 lemma point_of_pc_sigma_commute : 1258 ∀p,p',graph_prog. 1259 let lin_prog ≝ linearise p graph_prog in 1260 ∀sigma,pc,f,fn,n. 1261 ∀prf : well_formed_pc p p' graph_prog sigma pc. 1262 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 → 1263 sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n → 1264 point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n. 1265 #p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma 1266 whd in match sigma_pc; normalize nodelta 1267 @opt_safe_elim #pc' whd in match sigma_pc_opt; 1268 normalize nodelta @eqZb_elim #Hbl 1269 [ >(fetch_internal_function_no_minus_one … Hbl) in EQfetch; 1270 whd in ⊢ (???%→?); #ABS destruct(ABS) ] 1271 >EQfetch >m_return_bind >EQsigma 1272 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1273 @point_of_offset_of_point 1274 qed. 1275 1217 1276 lemma graph_succ_pc : 1218 1277 ∀p,p'.let pars ≝ make_sem_graph_params p p' in … … 1229 1288 fetch_statement (make_sem_graph_params p p') … 1230 1289 (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → 1231 All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma1290 (* All ? (λlbl.∃prf:well_formed_pc p p' graph_prog sigma 1232 1291 (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl). 1233 1292 pc_of_label (make_sem_lin_params p p') … … … 1235 1294 (pc_block pc) 1236 1295 lbl = return sigma_pc … prf) 1237 (stmt_explicit_labels … stmt) ∧ 1296 (stmt_explicit_labels … stmt) ∧ *) 1238 1297 match stmt with 1239 1298 [ sequential s nxt ⇒ … … 1284 1343 inversion(sigma_pc_opt p p' graph_prog sigma pc) 1285 1344 [#ABS @⊥ >ABS in wfprf; * #H @H %] 1286 #lin_pc #lin_pc_spec 1287 whd in match sigma_pc_opt in lin_pc_spec; normalize nodelta in lin_pc_spec; 1288 @('bind_inversion lin_pc_spec) * #id #graph_fun >fetchfn 1289 #EQ whd in EQ : (??%?); destruct(EQ) #H @('bind_inversion H) H 1345 #lin_pc 1346 whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta in ⊢ (%→?); 1347 @eqZb_elim #Hbl 1348 [ >(fetch_internal_function_no_minus_one … Hbl) in fetchfn; #ABS destruct(ABS) ] 1349 normalize nodelta >fetchfn >m_return_bind 1350 #H @('bind_inversion H) H 1290 1351 #lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ) 1291 lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt) 1292 [@lin_pt_spec] * #H1 #H2 % 1293 [ H2 @(All_mp … (All_append_r H1) #lab #lab_spec 1294 whd in match well_formed_pc; normalize nodelta 1295 whd in match sigma_pc_opt; normalize nodelta >fetchfn 1296 >m_return_bind whd in match point_of_pc; whd in match pc_of_point; 1297 normalize nodelta >point_of_offset_of_point 1298 cases(sigma graph_fun lab) in lab_spec; [* #ABS @⊥ @ABS %] 1299 #linear_pt #_ >m_return_bind whd in ⊢ (?(??%?)); 1300 % #ABS destruct(ABS) 1301 ] lapply H2 1352 lapply(stmt_at_sigma_commute ???????? (good fn) ??? graph_stmt) 1353 [@lin_pt_spec@(pi2 … (\fst (linearise_int_fun … fn)))] * #H1 (* #H2 % 1354 [ @In_All 1355 #lab #lab_in 1356 lapply (All_In ??? lab H1 ?) 1357 [ @Exists_append_r assumption ] 1358 inversion (sigma graph_fun lab) [#_ * #ABS @⊥ @ABS %] 1359 #lin_pt #EQsigma #_ 1360 % 1361 [ @hide_prf whd % 1362  whd in match sigma_pc; normalize nodelta 1363 @opt_safe_elim #pc_lin 1364 ] whd in match sigma_pc_opt; 1365 normalize nodelta >(eqZb_false … Hbl) >fetchfn normalize nodelta 1366 >m_return_bind >point_of_pc_of_point >EQsigma 1367 #EQ whd in EQ : (??%?); destruct(EQ) 1368 whd in match pc_of_label; normalize nodelta 1369 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1370 inversion (point_of_label ????) 1371 [2: #lin_pt' #EQ lapply (all_labels_in … EQ) >EQsigma 1372 #EQ' destruct % ] 1373 change with (If ? then with prf do ? else ? = ? → ?) 1374 @If_elim <(lin_code_has_label … (mk_lin_params p)) 1375 [ #_ whd in ⊢ (??%?→?); #EQ destruct ] 1376 #ABS cases (absurd ?? ABS) 1377 lapply (pi2 … (\fst (linearise_int_fun … graph_fun)) … ) 1378 [2: 1379 normalize nodelta 1380 1381 >m_return_bind whd in ⊢ (?(??%?)); 1382 % #ABS destruct(ABS) 1383 1384 >(eqZb_false … Hbl) normalize nodelta >fetchfn 1385 >m_return_bind >point_of_pc_of_point inversion(sigma graph_fun lab) in lab_spec; 1386 [ #_ * #ABS @⊥ @ABS %] #linear_pt #linear_pt_spec #_ >m_return_bind 1387 whd in match pc_of_label; normalize nodelta 1388 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1389 1390 ] lapply H2 *) 1302 1391 cases (stmt) in H1; [ * [ #s  #a #ltrue ] #nxt  #s  * ] normalize nodelta 1303 1392 #all_labels_spec #H3 whd in match fetch_statement; normalize nodelta 1304 > sigma_pblock_eq_lemma1393 >pc_block_sigma_commute 1305 1394 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1395 >(point_of_pc_sigma_commute … fetchfn lin_pt_spec) 1306 1396 [ % 1307 [ whd in match point_of_pc; whd in match sigma_pc; normalize nodelta 1308 @opt_safe_elim #linear_pc whd in match sigma_pc_opt; normalize nodelta 1309 >lin_pc_spec #EQ destruct(EQ) >point_of_offset_of_point 1310 >(proj1 … H3) >m_return_bind // 1311  1312 % 1313 [ @hide_prf whd in match well_formed_pc; whd in match sigma_pc_opt; 1314 normalize nodelta lapply fetchfn 1315 whd in match fetch_internal_function; normalize nodelta 1316 #H4 @('bind_inversion H4) #x #x_spec 1317 >x_spec >m_return_bind #EQ >EQ >m_return_bind 1318 whd in match pc_of_point; whd in match succ_pc; whd in match point_of_pc; 1319 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1320 cases(proj2 … H3)[ #EQ >EQ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)] 1321 cases all_labels_spec #Z #_ #sn 1322 whd in match (point_of_succ ???); 1323 >(opt_to_opt_safe … Z) % #ABS whd in ABS : (??%?); destruct(ABS) 1324  cases(proj2 … H3) 1325 [ #Z %1 whd in match sigma_pc; normalize nodelta 1326 @opt_safe_elim #pc1 whd in match sigma_pc_opt; normalize nodelta 1327 >lin_pc_spec #EQ destruct(EQ) 1328 @opt_safe_elim #pc2 >fetchfn >m_return_bind >graph_succ_pc 1329 >point_of_pc_of_point 1330 >Z >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) 1331 whd in match succ_pc; 1332 whd in match point_of_pc; whd in match point_of_succ; normalize nodelta 1397 [ >(proj1 … H3) % 1398  % [ @hide_prf % 1399  change with (opt_safe ???) in match (sigma_pc ???? (succ_pc ???) ?); 1400 @opt_safe_elim #pc1 1401 ] whd in match sigma_pc_opt; 1402 normalize nodelta >(eqZb_false … Hbl) >fetchfn 1403 >m_return_bind 1404 >graph_succ_pc >point_of_pc_of_point 1405 cases(proj2 … H3) 1406 [1,3: #EQ >EQ 1407 *: * cases all_labels_spec #Z #_ #sn 1408 >(opt_to_opt_safe … Z) #EQpoint_of_label 1409 ] whd in ⊢ (??%?→?); #EQ destruct(EQ) 1410 [ %1 1411 whd in match (point_of_succ ???) ; 1412 whd in match point_of_pc; normalize nodelta 1413 whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta 1414 @opt_safe_elim >(eqZb_false … Hbl) >fetchfn >m_return_bind 1415 >lin_pt_spec #pc' whd in ⊢ (??%%→?); #EQ destruct(EQ) 1416 whd in match succ_pc; whd in match point_of_pc; normalize nodelta 1333 1417 >point_of_offset_of_point % 1334  #Z %2 lapply fetchfn whd in match fetch_internal_function; normalize nodelta 1335 #H @('bind_inversion H) H * #x1 #x2 #x_spec 1336 lapply(fetch_function_transf ???? graph_prog 1337 (λglobals.transf_fundef ??(λf_in.\fst (linearise_int_fun p globals f_in))) ?? ? x_spec) 1338 #HH 1339 <sigma_pblock_eq_lemma in HH; [2:@wfprf] #HH >HH >m_return_bind 1340 cases x2 normalize nodelta [#g_fun  #xxx] #EQ whd in EQ : (??%%); destruct(EQ) 1341 >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta 1342 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1343 whd in match sigma_pc; normalize nodelta 1344 @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta 1345 >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); 1346 destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1347 >Z >m_return_bind % 1348 ] 1418  %2 whd in match (pc_block ?); >pc_block_sigma_commute 1419 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1420 whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta 1421 @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta 1422 #pc_lin >fetchfn >m_return_bind >lin_pt_spec >m_return_bind 1423 whd in match pc_of_point; normalize nodelta #EQ whd in EQ : (??%?); destruct 1424 whd in match point_of_pc; whd in match succ_pc; normalize nodelta 1425 whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1426 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1427 >sn >m_return_bind % [%] whd in match pc_of_label; normalize nodelta 1428 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1429 >EQpoint_of_label % 1430 ] 1431 ] 1432  % [ @hide_prf % whd in match sigma_pc_opt; normalize nodelta 1433 >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); >fetchfn 1434 >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta 1435 whd in match pc_of_point; whd in match point_of_pc; normalize nodelta 1436 >point_of_offset_of_point cases all_labels_spec #H >(opt_to_opt_safe … H) #_ 1437 >m_return_bind #ABS whd in ABS : (??%?); destruct(ABS)] 1438 cases H3 * #nxt_spec #point_of_lab_spec >nxt_spec >m_return_bind 1439 [%1 % [%] whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta 1440 @opt_safe_elim #lin_pc1 @opt_safe_elim #lin_pc2 1441 >(eqZb_false … Hbl) normalize nodelta >fetchfn >m_return_bind 1442 >m_return_bind in ⊢ (? → % → ?); whd in match point_of_pc; whd in match succ_pc; 1443 normalize nodelta whd in match pc_of_point; whd in match point_of_pc; normalize nodelta 1444 >point_of_offset_of_point >point_of_lab_spec >m_return_bind #EQ 1445 whd in EQ : (??%?); destruct(EQ) >lin_pt_spec >m_return_bind #EQ 1446 whd in EQ : (??%?); destruct(EQ) >point_of_offset_of_point % 1447 %2 >m_return_bind >nxt_spec >m_return_bind %[%] whd in match pc_of_label; 1448 normalize nodelta >(fetch_internal_function_transf … fetchfn) 1449 >m_return_bind >point_of_lab_spec cases all_labels_spec #H #INUTILE 1450 >(opt_to_opt_safe … H) in ⊢ (??%?); >m_return_bind 1451 normalize in ⊢ (??%?); 1452 whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta 1453 @opt_safe_elim >(eqZb_false … Hbl) normalize nodelta whd in match (pc_block ?); 1454 >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; 1455 normalize nodelta whd in match point_of_pc; whd in match pc_of_point; 1456 normalize nodelta >point_of_offset_of_point cases (sigma fn nxt) in H; 1457 [ * #ABS @⊥ @ABS %] #linear_point * #INUTILE1 #linear_pc >m_return_bind 1458 #EQ whd in EQ : (??%?); destruct(EQ) normalize nodelta % 1349 1459 ] 1350 ] 1351  cases H3 1352 [ * #Z1 #Z2 %1 % [ @hide_prf whd in match well_formed_pc; 1353 whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind 1354 >graph_succ_pc >point_of_pc_of_point 1355 >Z2 % #ABS whd in ABS : (??%?); destruct(ABS) 1356 ] % 1357 [ whd in match sigma_pc; normalize nodelta 1358 @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta 1359 >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); 1360 destruct(EQ) whd in match point_of_pc; normalize nodelta 1361 >point_of_offset_of_point >Z1 >m_return_bind % 1362  whd in match sigma_pc; normalize nodelta 1363 @opt_safe_elim #line_pc 1364 @opt_safe_elim #line_succ_pc whd in match sigma_pc_opt; normalize nodelta 1365 >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; 1366 normalize nodelta >point_of_offset_of_point >Z2 >m_return_bind 1367 #EQ whd in EQ : (??%?); destruct(EQ) >m_return_bind >lin_pt_spec >m_return_bind 1368 #EQ whd in EQ : (??%?); destruct(EQ) whd in match pc_of_point; whd in match point_of_pc; 1369 normalize nodelta >point_of_offset_of_point % 1370 ] 1371  #Z %2 whd in match sigma_pc; normalize nodelta >fetchfn >m_return_bind 1372 @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta 1373 >fetchfn >m_return_bind >lin_pt_spec >m_return_bind 1374 #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta 1375 >point_of_offset_of_point >Z >m_return_bind % 1376 ] 1377  whd in match sigma_pc; normalize nodelta @opt_safe_elim 1378 #line_pc whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind 1379 >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) 1380 whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1381 >H3 >m_return_bind % 1382 ] 1383 qed. 1384 1385 lemma point_of_pc_sigma_commute : 1386 ∀p,p',graph_prog. 1387 let lin_prog ≝ linearise p graph_prog in 1388 ∀sigma,pc,f,fn,n. 1389 ∀prf : well_formed_pc p p' graph_prog sigma pc. 1390 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 → 1391 sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n → 1392 point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n. 1393 #p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma 1394 whd in match sigma_pc; normalize nodelta 1395 @opt_safe_elim #pc' whd in match sigma_pc_opt; 1396 normalize nodelta >EQfetch >m_return_bind >EQsigma 1397 whd in ⊢ (??%?→?); #EQ destruct(EQ) 1398 @point_of_offset_of_point 1399 qed. 1460  >H3 >m_return_bind % 1461 ] 1462 qed. 1463 1464 1465 lemma res_eq_from_opt : ∀A,m,a. 1466 res_to_opt A m = return a → m = return a. 1467 #A #m #a cases m #x normalize #EQ destruct(EQ) % 1468 qed. 1469 1400 1470 1401 1471 definition linearise_status_rel: … … 1403 1473 let lin_prog ≝ linearise p graph_prog in 1404 1474 ∀stack_sizes. 1405 ∀sigma ,gss.1475 ∀sigma. ∀ gss : good_state_sigma p p' graph_prog sigma. 1406 1476 good_sigma p graph_prog sigma → 1407 1477 status_rel … … 1418 1488 (* sim_final ≝ *) ?. 1419 1489 #st1 #st2 * #prf #EQ2 1420 % 1490 % [2: cases daemon] 1491 >EQ2 1421 1492 whd in ⊢ (%→%); 1422 1493 #H lapply (opt_to_opt_safe … H) 1423 @opt_safe_elim H 1424 #res #_ 1425 #H cases daemon (* 1494 @opt_safe_elim H #res #_ whd in match is_final; normalize nodelta 1495 #H lapply(res_eq_from_opt ??? H) H 1426 1496 #H @('bind_inversion H) H 1427 * #f #stmt 1428 whd in match fetch_statement; normalize nodelta 1429 #H @('bind_inversion H) H * 1430 #id #int_f 1431 whd in match fetch_internal_function; normalize nodelta 1432 #H @('bind_inversion H) H * #id1 #int_f1 1433 whd in match fetch_function; normalize nodelta 1434 #H lapply(opt_eq_from_res ???? H) H 1435 #H @('bind_inversion H) H #id2 1436 whd in match symbol_for_block; normalize nodelta 1437 whd in match option_map; normalize nodelta 1438 cases (find ?? (symbols ? ?) ?) normalize nodelta 1439 [1,3: #ABS destruct(ABS)] #sy_bl #EQ destruct(EQ) 1440 #H @('bind_inversion H) H #int_f2 whd in match find_funct_ptr; 1441 normalize nodelta cases(block_region (pc_block (pc ? ?))) 1442 normalize nodelta [1,3: #ABS destruct(ABS)] 1443 cases(block_id (pc_block (pc ??))) normalize nodelta 1444 [1,2,4,5: [2,4: #pos] #ABS destruct(ABS)] 1445 #pos #int_f2_spec #EQ whd in EQ : (??%?); destruct(EQ) 1446 cases int_f1 in int_f2_spec; normalize nodelta 1447 [2,4: #ext_f #_ #ABS whd in ABS : (???%); destruct(ABS)] 1448 #int_f3 #int_f3_spec #EQ whd in EQ : (??%%); destruct(EQ) 1449 #H @('bind_inversion H) H #stmt1 #H lapply(opt_eq_from_res ???? H) H 1450 #stmt1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1451 cases (stmt) in stmt1_spec; normalize nodelta 1452 [1,3,4,6: [1,3: #js #jsucc #_  2,4: #a #b #c #d #_] #ABS whd in ABS : (???%); 1453 destruct(ABS)] 1454 #fin_step #fin_step_spec cases (fin_step) in fin_step_spec; normalize nodelta 1455 [1,3,4,6: [1,3: #l #_2,4: #a #b #c #_] #ABS whd in ABS : (???%); destruct(ABS)] 1456 #STMT_SPEC #H @('bind_inversion H) H #state_pc #state_pc_sepc 1457 #H @('bind_inversion H) H #succ_pc whd in match next_of_pc; normalize nodelta 1458 #H @('bind_inversion H) H * #id4 #int_f4 whd in match fetch_statement; normalize nodelta 1459 #H @('bind_inversion H) H * #id5 #int_f5 whd in match fetch_internal_function; normalize nodelta 1460 #H @('bind_inversion H) H * #id6 #int_f6 whd in match fetch_function; normalize nodelta 1461 #H lapply(opt_eq_from_res ???? H) H #H @('bind_inversion H) H #id7 1462 whd in match symbol_for_block; normalize nodelta whd in match option_map; normalize nodelta 1463 cases(find ? ? ? ?) normalize nodelta [1,3: #ABS destruct(ABS)] 1464 #sy_bl1 #EQ destruct(EQ) #H @('bind_inversion H) H #int_f7 1465 whd in match find_funct_ptr; normalize nodelta 1466 cases(block_region (pc_block ?)) normalize nodelta [1,3: #ABS destruct(ABS)] 1467 cases(block_id ?) normalize nodelta [1,2,4,5: [2,4:#p] #ABS destruct(ABS)] 1468 #pos1 #int_f7_spec #EQ whd in EQ : (??%?); destruct(EQ) cases (int_f6) in int_f7_spec; 1469 normalize nodelta [2,4: #ext_fun #_ #ABS whd in ABS : (???%); destruct(ABS)] 1470 #int_f8 #int_f8_spec #EQ whd in EQ : (??%%); destruct(EQ) 1471 #H @('bind_inversion H) H #stmt2 #H lapply(opt_eq_from_res ???? H) H 1472 #stmt2_spec #EQ whd in EQ : (??%%); destruct(EQ) 1473 cases int_f4 in stmt2_spec; normalize nodelta 1474 [2,3,5,6: 1475 1476 xxxxxxxxxxxxxx 1477 *) 1497 ** #id #int_f #stmt 1498 #stmt_spec lapply(fetch_statement_sigma_commute ???????? good (proj1 … prf) stmt_spec) 1499 cases stmt in stmt_spec; stmt normalize nodelta 1500 [1,3: [ #a #b #_ #a #b #c #d #e] #_ #ABS whd in ABS : (???%); destruct(ABS)] 1501 #fin_step cases(fin_step) fin_step normalize nodelta 1502 [1,3: [#l #a #b #c] #_ #_ #ABS whd in ABS: (???%); destruct(ABS)] 1503 #fetch_graph_spec #fetch_lin_spec 1504 #H >fetch_lin_spec >m_return_bind normalize nodelta 1505 @('bind_inversion H) H #state_pc #state_pc_spec 1506 elim(pop_frame_commute 1507 p p' graph_prog sigma gss ? id int_f ? (hide_prf … (proj2 … prf)) … state_pc_spec) 1508 #wf_state_pc normalize nodelta #sigma_state_pc_commute >sigma_state_pc_commute 1509 >m_return_bind @eq_program_counter_elim normalize nodelta 1510 [2: #_ #EQ whd in EQ : (???%); destruct(EQ)] #state_pc_spec #H 1511 @eq_program_counter_elim normalize nodelta 1512 [2: * #ABS @⊥ @ABS whd in match sigma_pc; whd in match sigma_pc_opt; normalize nodelta 1513 @opt_safe_elim #next_pc @eqZb_elim normalize nodelta >state_pc_spec 1514 [2: * #ABS1 @⊥ @ABS1 normalize %] #_ #EQ whd in EQ : (??%?); destruct(EQ) % 1515  #_ @('bind_inversion H) H #list_val #list_val_spec 1516 elim(read_result_commute p p' graph_prog sigma gss ? ? ? ? ? list_val_spec) 1517 [2: @hide_prf @(proj2 … prf)] #wf_lm #EQ >EQ EQ >m_return_bind 1518 whd in match Word_of_list_beval in ⊢ (% → ?); normalize nodelta 1519 #H @('bind_inversion H) H * #b1 #l1 #b1_l1_spec #H 1520 cases list_val in list_val_spec wf_lm b1_l1_spec; list_val normalize nodelta 1521 [ #_ #l #ABS whd in ABS : (???%); destruct(ABS)] 1522 #b2 #l2 #b2_l2_spec #wf_b2_l2 #H1 @('bind_inversion H1) H1 1523 #bt whd in match Byte_of_val; normalize nodelta 1524 cases (b2) in b2_l2_spec wf_b2_l2; b2 normalize nodelta 1525 [1,2,3,5,6,7: [#a #b #c  #p  #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (???%); destruct(ABS)] 1526 #by #by_l2_spec #wf_by_l2 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); 1527 destruct(EQ) @('bind_inversion H) H * #by1 #l3 1528 cases l1 in by_l2_spec wf_by_l2; l1 normalize nodelta [ #_ #a #ABS whd in ABS : (???%); destruct(ABS)] 1529 #val #l1 #b1_val_l1_spec #wf_b1_val_l1 #H @('bind_inversion H) H #by1 1530 cases val in b1_val_l1_spec wf_b1_val_l1; val 1531 [1,2,3,5,6,7: [#a #b #c  #p  #p #p'] #a #b [6: #_ #a] whd in match Byte_of_val; normalize nodelta 1532 #ABS whd in ABS : (???%); destruct(ABS)] 1533 #by2 #b1_by2_l1_spec #wf_b1_by2_l1 whd in match Byte_of_val; normalize nodelta 1534 #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ) 1535 #H @('bind_inversion H) H * #by2 #l2 1536 cases(l3) in b1_by2_l1_spec wf_b1_by2_l1; l3 normalize nodelta 1537 [#_ #a #ABS whd in ABS : (???%); destruct(ABS)] 1538 #val #l1 #b1_by1_val_l1_spec #wf_b1_by1_val_l1 #H @('bind_inversion H) H 1539 #by3 cases val in b1_by1_val_l1_spec wf_b1_by1_val_l1; val normalize nodelta 1540 [1,2,3,5,6,7: [#a #b #c  #p  #p #p'] #a #b [6: #_ #a] #ABS whd in ABS : (??%%); destruct(ABS)] 1541 #by3 #b1_by1_by3_l1_spec #wf_b1_by1_by3_l1 #EQ whd in EQ : (???%); destruct(EQ) 1542 #EQ whd in EQ : (???%); destruct(EQ) #H @('bind_inversion H) H * 1543 #by3 #l1 cases l2 in b1_by1_by3_l1_spec wf_b1_by1_by3_l1; l2 normalize nodelta 1544 [#_ #a #ABS whd in ABS : (???%); destruct(ABS)] 1545 #val #l2 #_ #wf_b1_by1_by2_val #H @('bind_inversion H) H #by4 1546 cases val in wf_b1_by1_by2_val; val normalize nodelta 1547 [1,2,3,5,6,7: [ #a #b #c #p  #p #p'#p #pa] #a #ABS whd in ABS : (???%); destruct(ABS)] 1548 #by5 #wf_list #EQ whd in EQ : (???%); destruct(EQ) #EQ whd in EQ : (???%); destruct(EQ) cases l1 in wf_list; l1 normalize nodelta [2: #val #l #a #ABS whd in ABS : (???%); destruct(ABS)] 1549 #wf_list #EQ whd in EQ : (???%); destruct(EQ) 1550 @opt_safe_elim #l #H normalize in H; destruct(H) normalize % #ABS destruct(ABS) 1478 1551 qed. 1479 1552 
src/joint/semantics.ma
r2537 r2551 619 619 [ RETURN ⇒ 620 620 do st' ← pop_frame … ge id fn st; 621 ! nxt ← next_of_pc … ge (pc … st') ; 622 let pc' ≝ succ_pc … (pc … st') nxt in 623 if eq_program_counter pc' exit then 624 do vals ← read_result … ge (joint_if_result … fn) st ; 625 Word_of_list_beval vals 621 if eq_program_counter (pc … st') exit then 622 do vals ← read_result … ge (joint_if_result … fn) st ; 623 Word_of_list_beval vals 626 624 else 627 Error ? [ ]625 Error ? [ ] 628 626  _ ⇒ Error ? [ ] 629 627 ]
Note: See TracChangeset
for help on using the changeset viewer.