 Timestamp:
 Dec 4, 2012, 9:05:52 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2507 r2528 360 360 λp,p',graph_prog,sigma,gsss,st,prf. 361 361 mk_state … 362 (sigma_frames … gsss (st_frms … st) (proj1 … (proj1 … (proj1 … prf))))363 (sigma_is p p' graph_prog sigma (istack … st) (proj2 … (proj1 … (proj1 … prf))))362 (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?) 363 (sigma_is p p' graph_prog sigma (istack … st) ?) 364 364 (carry … st) 365 (sigma_regs … gsss (regs … st) (proj2 … (proj1 … prf))) 366 (sigma_mem p p' graph_prog sigma (m … st) (proj2 … prf)). 365 (sigma_regs … gsss (regs … st) ?) 366 (sigma_mem p p' graph_prog sigma (m … st) ?). 367 @hide_prf 368 [ @(proj1 … (proj1 … (proj1 … prf)))  @(proj2 … (proj1 … (proj1 … prf))) 369  @(proj2 … (proj1 … prf))  @(proj2 … prf)] 370 qed. 367 371 368 372 … … 1140 1144 cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %] 1141 1145 #EQ >EQ // 1146 qed. 1147 1148 lemma is_push_sigma_commute : 1149 ∀ p, p', graph_prog,sigma,gss,st,val,is,prf1,prf2. 1150 (is_push (istack … st) val=return is) → 1151 ∃prf3. 1152 is_push (istack … (sigma_state p p' graph_prog sigma gss st prf1)) 1153 (sigma_beval p p' graph_prog sigma val prf2) = 1154 return sigma_is p p' graph_prog sigma is prf3. 1155 #p #p' #graph_prog #sigma #gss #st #val #is #prf1 #prf2 #H 1156 % 1157 [ @hide_prf 1158 whd in match sigma_is_opt; normalize nodelta 1159 inversion (istack ? ?) in H; 1160 whd in match is_push; normalize nodelta [3: #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)] 1161 [2: #a] #a_spec #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta 1162 inversion (sigma_beval_opt ???? val) [1,3: #ABS >ABS in prf2; * #ABS @⊥ @ABS %] 1163 [2: #val' #_ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)] 1164 #val' #_ 1165 inversion(sigma_beval_opt ???? a) 1166 [2: #val'' #_ >m_return_bind >m_return_bind % #EQ whd in EQ : (??%?); destruct(EQ)] 1167 #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf1))) >a_spec 1168 whd in match sigma_is_opt; normalize nodelta >ABS whd in ⊢ ((?(??%?))→ ?); * 1169 #EQ @EQ % 1170 ] 1171 whd in match sigma_state; normalize nodelta 1172 cut(is_push (istack (make_sem_graph_params p p') st) val=return is) 1173 [ assumption] 1174 #H1 whd in match sigma_is; normalize nodelta 1175 @opt_safe_elim #is1 #is1_spec 1176 whd in match sigma_beval; normalize nodelta 1177 @opt_safe_elim #sigma_val #sigma_val_sepc 1178 @opt_safe_elim #sigma_is #sigma_is_spec 1179 inversion(istack ? st) 1180 [2: #val13:#val1 #val2] 1181 #H2 >H2 in H1; 1182 whd in match is_push; normalize nodelta 1183 #EQ whd in EQ : (??%%); destruct(EQ) 1184 >H2 in is1_spec; whd in match sigma_is_opt; normalize nodelta 1185 #EQ whd in EQ : (??%?); destruct(EQ) 1186 normalize nodelta 1187 whd in match sigma_is_opt in sigma_is_spec; 1188 normalize nodelta in sigma_is_spec; 1189 >sigma_val_sepc in sigma_is_spec; 1190 [ inversion(sigma_beval_opt ???? val1) 1191 [ #ABS #EQ1 whd in EQ1 : (??%%); destruct(EQ1)  #sigma_val1 #H3 >m_return_bind]] 1192 >m_return_bind 1193 #EQ whd in EQ : (??%?); destruct(EQ) [2: %] 1194 >H3 in EQ; 1195 normalize nodelta 1196 #EQ1 whd in EQ1 : (??%%); destruct(EQ1) 1197 normalize nodelta // 1198 qed. 1199 1200 lemma beopaccs_sigma_commute : 1201 ∀p,p',graph_prog,sigma,op,val1,val2,opaccs1,opaccs2. 1202 ∀ prf1 : sigma_beval_opt p p' graph_prog sigma val1 ≠ None ?. 1203 ∀ prf2 : sigma_beval_opt p p' graph_prog sigma val2 ≠ None ?. 1204 be_opaccs op val1 val2=return 〈opaccs1,opaccs2〉 → 1205 ∃ prf1' : sigma_beval_opt p p' graph_prog sigma opaccs1 ≠ None ?. 1206 ∃ prf2' : sigma_beval_opt p p' graph_prog sigma opaccs2 ≠ None ?. 1207 be_opaccs op (sigma_beval … prf1) (sigma_beval … prf2) = 1208 return 〈(sigma_beval … prf1'),(sigma_beval … prf2')〉. 1209 #p #p' #graph_prog #sigma #op #val1 #val2 1210 #opaccs1 #opaccs2 #prf1 #prf2 1211 whd in match be_opaccs; normalize nodelta 1212 #H elim(bind_inversion ????? H) H 1213 #x * #x_spec 1214 #H elim(bind_inversion ????? H) H 1215 #y * #y_spec 1216 #H lapply H #H1 normalize in H; elim(opaccs_implementation op x y) in H; 1217 #b1 #b2 #EQ normalize in EQ; destruct(EQ) 1218 % 1219 [whd in match sigma_beval_opt; normalize nodelta % #ABS 1220 whd in ABS : (??%?); destruct(ABS)] 1221 % 1222 [whd in match sigma_beval_opt; normalize nodelta % #ABS 1223 whd in ABS : (??%?); destruct(ABS)] 1224 whd in match sigma_beval; normalize nodelta 1225 @opt_safe_elim #sigma_val1 #sigma_val1_spec 1226 @opt_safe_elim #sigma_val2 #sigma_val2_spec 1227 @opt_safe_elim #sigma_op1 #sigma_op1_spec 1228 @opt_safe_elim #sigma_op2 #sigma_op2_spec 1229 lapply x_spec x_spec lapply sigma_val1_spec sigma_val1_spec 1230 inversion val1 whd in match Byte_of_val; normalize nodelta 1231 [ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)] 1232 [#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)] 1233 #bt_val1 #val1_spec whd in match sigma_beval_opt; normalize nodelta 1234 whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ) 1235 #EQ whd in EQ : (???%); destruct(EQ) 1236 lapply y_spec y_spec lapply sigma_val2_spec sigma_val2_spec 1237 inversion val2 whd in match Byte_of_val; normalize nodelta 1238 [ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)] 1239 [#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)] 1240 #bt_val2 #val2_spec whd in match sigma_beval_opt; normalize nodelta 1241 whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ) normalize nodelta 1242 #EQ whd in EQ : (???%); destruct(EQ) 1243 >m_return_bind >m_return_bind 1244 whd in match sigma_beval_opt in sigma_op1_spec; 1245 normalize nodelta in sigma_op1_spec; 1246 whd in sigma_op1_spec : (??%?); destruct(sigma_op1_spec) 1247 whd in match sigma_beval_opt in sigma_op2_spec; 1248 normalize nodelta in sigma_op2_spec; 1249 whd in sigma_op2_spec : (??%?); destruct(sigma_op2_spec) 1250 >H1 % 1142 1251 qed. 1143 1252 … … 1284 1393 inversion(sigma_beval_opt ???? y) 1285 1394 [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf))) 1286 xxxxxxxxxxxxxxxxxx 1287 1288 qed. 1289 1395 whd in match sigma_is_opt; >H normalize nodelta >ABS 1396 whd in ⊢ ((?(??%?))→?); * #h1 @h1 % 1397  #sigma_y #H >m_return_bind 1398 cases (sigma_beval_opt ? ? ? ? x) in val_wf; [ * #ABS @⊥ @ABS %] 1399 #sigma_y' #_ >m_return_bind whd in ⊢ (?(??%?)); % #H destruct(H) 1400 ] 1401  #a1 #a2 #_ #EQ whd in EQ : (???%); destruct(EQ) 1402 ] 1403 ] 1404  1405 whd in match helper_def_retrieve in acca_arg_retrieve_commute; 1406 normalize nodelta in acca_arg_retrieve_commute; 1407 whd in match acca_arg_retrieve; normalize nodelta 1408 @err_eq_to_io 1409 change with 1410 ((! v ← (acca_arg_retrieve_ p 1411 (joint_closed_internal_function (make_sem_lin_params p p')) 1412 (make_sem_lin_params p p') 1413 (regs (make_sem_lin_params p p') 1414 (sigma_state p p' graph_prog sigma gss st prf)) 1415 a); 1416 ?)=?) 1417 change with ((! v ← ?; push (make_sem_lin_params p p') ? ?) = ?) 1418 cut((acca_arg_retrieve_ p ? ? ? a) = return sigma_beval p ? ? ? ? val_wf) 1419 [4: assumption     ] #H >H >m_return_bind 1420 whd in match push; normalize nodelta 1421 H elim(is_push_sigma_commute ???????? prf val_wf int_stack_spec) 1422 #wf_is #EQ >EQ >m_return_bind // 1423 ] 1424  (*C_ADDRESS*) 1425 #sy 1426 change with ((member ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?) 1427 #sy_prf 1428 change with ((dpl_reg p) → ?) #dpl 1429 change with ((dph_reg p) → ?) #dph 1430 #H lapply(err_eq_from_io ????? H) H 1431 change with ((( ! st1 ← dpl_store p 1432 (joint_closed_internal_function (make_sem_graph_params p p')) 1433 (make_sem_graph_params p p') 1434 ? 1435 ? 1436 ? ; ? ) = ?) → ?) 1437 change with ((( ! st1 ← dpl_store ???? 1438 (BVptr 1439 (mk_pointer 1440 (opt_safe block 1441 (find_symbol 1442 (fundef 1443 (joint_closed_internal_function 1444 (make_sem_graph_params p p') 1445 ? 1446 ) 1447 ) 1448 (globalenv_noinit ? graph_prog) 1449 ? 1450 ) 1451 ? 1452 ) 1453 ? 1454 ) 1455 ? 1456 ) ? ; ?) = ?) → ?) 1457 change with ((( ! st1 ← ? ; 1458 dph_store p (joint_closed_internal_function (make_sem_graph_params p p')) 1459 (make_sem_graph_params p p') ? 1460 (BVptr 1461 (mk_pointer 1462 (opt_safe block 1463 (find_symbol 1464 (fundef 1465 (joint_closed_internal_function 1466 (make_sem_graph_params p p') 1467 ? 1468 ) 1469 ) 1470 (globalenv_noinit ? graph_prog) 1471 ? 1472 ) 1473 ? 1474 ) 1475 ? 1476 ) 1477 ? 1478 ) ?) = ?) → ?) 1479 #H elim(bind_inversion ????? H) H 1480 #st1 * #dpl_st1 1481 elim(store_commute p p' graph_prog sigma ?? gss (dpl_store_commute … gss) ???? prf ? dpl_st1) 1482 [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); % 1483 #ABS destruct(ABS)] 1484 #wf_st1 whd in match helper_def_store; normalize nodelta 1485 #H elim(bind_inversion ????? H) H #reg1 * #reg1_spec #EQ whd in EQ : (??%%); 1486 destruct(EQ) EQ 1487 #dph_st' 1488 elim(store_commute p p' graph_prog sigma ?? gss (dph_store_commute … gss) ???? wf_st1 ? dph_st') 1489 [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); 1490 % #ABS destruct(ABS)] 1491 #wf_st' whd in match helper_def_store; normalize nodelta 1492 #H elim(bind_inversion ????? H) H #reg2 * #reg2_spec #EQ whd in EQ : (??%%); 1493 destruct(EQ) EQ %{wf_st'} <e1 1494 whd in match dpl_store; normalize nodelta 1495 whd in match sigma_beval in reg1_spec; normalize nodelta in reg1_spec; 1496 whd in match sigma_beval_opt in reg1_spec; normalize nodelta in reg1_spec; 1497 lapply reg1_spec reg1_spec @opt_safe_elim #x #EQ whd in EQ : (??%?); 1498 destruct(EQ) @opt_safe_elim #block_graph #block_graph_spec 1499 #reg1_spec @opt_safe_elim #block_lin #block_lin_spec 1500 cut(find_symbol 1501 (fundef 1502 (joint_closed_internal_function 1503 (make_sem_lin_params p p') 1504 (prog_var_names (joint_function (mk_lin_params p)) ℕ (linearise … graph_prog)) 1505 ) 1506 ) 1507 (globalenv_noinit (joint_function (mk_lin_params p)) (linearise … graph_prog)) 1508 sy 1509 = 1510 find_symbol 1511 (fundef 1512 (joint_closed_internal_function 1513 (make_sem_graph_params p p') 1514 (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog) 1515 ) 1516 ) 1517 (globalenv_noinit (joint_function (mk_graph_params p)) graph_prog) 1518 sy) 1519 [ @find_symbol_transf] 1520 #find_sym_EQ >find_sym_EQ in block_lin_spec; >block_graph_spec 1521 #EQ destruct(EQ) >reg1_spec >m_return_bind 1522 whd in match dph_store; normalize nodelta 1523 lapply reg2_spec reg2_spec 1524 whd in match sigma_beval; normalize nodelta 1525 @opt_safe_elim #y 1526 whd in match sigma_beval_opt; normalize nodelta 1527 whd in ⊢((??%?)→?); #EQ destruct(EQ) 1528 @opt_safe_elim #graph_block >block_graph_spec 1529 #EQ destruct(EQ) #reg2_spec 1530 cut(sigma_state p p' graph_prog sigma gss st1 wf_st1 = 1531 (set_regs (lin_prog_params p p' (linearise p graph_prog) stack_sizes) 1532 reg1 (sigma_state p p' graph_prog sigma gss st prf))) 1533 [whd in match set_regs; normalize nodelta >e0 %] 1534 #sigma_st1_spec <sigma_st1_spec >reg2_spec 1535 >m_return_bind % 1536  (*C_OPACCS*) 1537 #op #a #b #arg1 #arg2 1538 #H lapply(err_eq_from_io ????? H) H 1539 #H elim(bind_inversion ????? H) H 1540 #val1 * #val1_spec 1541 elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf val1_spec) 1542 #wf_val1 #sigma_val1_commute 1543 #H elim(bind_inversion ????? H) H 1544 #val2 * #val2_spec 1545 elim (retrieve_commute p p' graph_prog sigma ?? gss (accb_arg_retrieve_commute … gss)??? prf val2_spec) 1546 #wf_val2 #sigma_val2_commute 1547 #H elim(bind_inversion ????? H) H * 1548 #opaccs1 #opaccs2 * #opaccs_spec 1549 elim(beopaccs_sigma_commute p p' graph_prog sigma ????? wf_val1 wf_val2 opaccs_spec) 1550 #wf_opaccs1 * #wf_opaccs2 #be_opaccs_commute 1551 #H elim(bind_inversion ????? H) H 1552 #st1 * #st1_spec 1553 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_opaccs1 st1_spec) 1554 #wf_st1 #sigma_st1_commute #final_spec 1555 elim(store_commute p p' graph_prog sigma ?? gss (accb_store_commute … gss) ???? wf_st1 wf_opaccs2 final_spec) 1556 #wf_st' #sigma_final_commute 1557 %{wf_st'} 1558 whd in match helper_def_retrieve in sigma_val1_commute; 1559 normalize nodelta in sigma_val1_commute; 1560 whd in match acca_arg_retrieve; normalize nodelta 1561 >sigma_val1_commute >m_return_bind 1562 whd in match helper_def_retrieve in sigma_val2_commute; 1563 normalize nodelta in sigma_val2_commute; 1564 whd in match accb_arg_retrieve; normalize nodelta 1565 >sigma_val2_commute >m_return_bind 1566 >be_opaccs_commute >m_return_bind 1567 whd in match helper_def_store in sigma_st1_commute; 1568 normalize nodelta in sigma_st1_commute; 1569 elim(bind_inversion ????? sigma_st1_commute) 1570 #reg1 * #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1571 whd in match acca_store; normalize nodelta 1572 >reg1_spec >m_return_bind 1573 whd in match set_regs; normalize nodelta >e0 1574 whd in match helper_def_store in sigma_final_commute; 1575 normalize nodelta in sigma_final_commute; 1576 elim(bind_inversion ????? sigma_final_commute) 1577 #reg2 * #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ) 1578 whd in match accb_store; normalize nodelta 1579 >reg2_spec >m_return_bind whd in match set_regs; normalize nodelta 1580 >e1 % 1581  (*C_OP1*) 1582 1290 1583 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 1291 1584 ex1_intro: ∀ x:A. P x → ex_Type1 A P.
Note: See TracChangeset
for help on using the changeset viewer.