Changeset 2536 for src/joint/lineariseProof.ma
 Timestamp:
 Dec 6, 2012, 1:18:35 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2529 r2536 511 511 retrieve … (sigma_regs … gsss r prf1) a 512 512 = return sigma_beval p p' graph_prog sigma bv prf2. 513 513 514 514 515 record good_state_sigma 515 516 (p : unserialized_params) … … 537 538 pair_reg_move_ ? ? (p' ?) (sigma_regs p p' graph_prog sigma gsss r1 prf1) mv = 538 539 return sigma_regs p p' graph_prog sigma gsss r2 prf2 539 ; allocate_locals_commute :540 ∀ loc, r1, prf1. ∃ prf2.541 allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) =542 sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2543 540 ; save_frame_commute : 544 541 ∀dest,st1,st2,prf1. … … 548 545 ∃prf2. 549 546 save_frame ?? (p' ?) dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2 547 ; allocate_locals_commute : 548 ∀ loc, r1, prf1. ∃ prf2. 549 allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) = 550 sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2 550 551 ; eval_ext_seq_commute : 551 552 let lin_prog ≝ linearise p graph_prog in 552 ∀ stack_sizes.553 ∀ stack_sizes. 553 554 ∀ext,i,fn,st1,st2,prf1. 554 555 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) … … 596 597 return mk_state_pc ? st2' pc' 597 598 }. 599 600 601 602 598 603 599 604 lemma store_commute : … … 1260 1265 1261 1266 lemma is_push_sigma_commute : 1262 ∀ p, p', graph_prog,sigma, gss,st,val,is,prf1,prf2.1263 (is_push (istack … st) val=return is) →1267 ∀ p, p', graph_prog,sigma,is,val,is',prf1,prf2. 1268 (is_push is val=return is') → 1264 1269 ∃prf3. 1265 is_push (istack … (sigma_state p p' graph_prog sigma gss st prf1)) 1266 (sigma_beval p p' graph_prog sigma val prf2) = 1267 return sigma_is p p' graph_prog sigma is prf3. 1268 #p #p' #graph_prog #sigma #gss #st #val #is #prf1 #prf2 #H 1270 is_push (sigma_is p p' graph_prog sigma is prf1) 1271 (sigma_beval p p' graph_prog sigma val prf2) = 1272 return sigma_is p p' graph_prog sigma is' prf3. 1273 #p #p' #graph_prog #sigma * 1274 [  #bv1  #bv1 #bv2 ] #val #is' #prf1 #prf2 1275 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1276 whd in match sigma_beval; normalize nodelta 1277 @opt_safe_elim #val' #EQsigma_val 1269 1278 % 1270 [ @hide_prf 1279 [1,3: @hide_prf % 1280 *: whd in match sigma_is in ⊢ (???%); normalize nodelta 1281 @opt_safe_elim #is'' 1282 ] whd in match sigma_is_opt; normalize nodelta 1283 [2,4: 1284 inversion (sigma_beval_opt ?????) 1285 [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1; 1286 normalize nodelta * #H @H % ] 1287 #bv1' #EQ_bv1' >m_return_bind ] 1288 >EQsigma_val 1289 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1290 whd in match sigma_is; normalize nodelta 1291 @opt_safe_elim #is1 1271 1292 whd in match sigma_is_opt; normalize nodelta 1272 inversion (istack ? ?) in H; 1273 whd in match is_push; normalize nodelta [3: #a #b #_ #ABS whd in ABS : (???%); destruct(ABS)] 1274 [2: #a] #a_spec #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta 1275 inversion (sigma_beval_opt ???? val) [1,3: #ABS >ABS in prf2; * #ABS @⊥ @ABS %] 1276 [2: #val' #_ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)] 1277 #val' #_ 1278 inversion(sigma_beval_opt ???? a) 1279 [2: #val'' #_ >m_return_bind >m_return_bind % #EQ whd in EQ : (??%?); destruct(EQ)] 1280 #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf1))) >a_spec 1281 whd in match sigma_is_opt; normalize nodelta >ABS whd in ⊢ ((?(??%?))→ ?); * 1282 #EQ @EQ % 1283 ] 1284 whd in match sigma_state; normalize nodelta 1285 cut(is_push (istack (make_sem_graph_params p p') st) val=return is) 1286 [ assumption] 1287 #H1 whd in match sigma_is; normalize nodelta 1288 @opt_safe_elim #is1 #is1_spec 1289 whd in match sigma_beval; normalize nodelta 1290 @opt_safe_elim #sigma_val #sigma_val_sepc 1291 @opt_safe_elim #sigma_is #sigma_is_spec 1292 inversion(istack ? st) 1293 [2: #val13:#val1 #val2] 1294 #H2 >H2 in H1; 1295 whd in match is_push; normalize nodelta 1296 #EQ whd in EQ : (??%%); destruct(EQ) 1297 >H2 in is1_spec; whd in match sigma_is_opt; normalize nodelta 1298 #EQ whd in EQ : (??%?); destruct(EQ) 1299 normalize nodelta 1300 whd in match sigma_is_opt in sigma_is_spec; 1301 normalize nodelta in sigma_is_spec; 1302 >sigma_val_sepc in sigma_is_spec; 1303 [ inversion(sigma_beval_opt ???? val1) 1304 [ #ABS #EQ1 whd in EQ1 : (??%%); destruct(EQ1)  #sigma_val1 #H3 >m_return_bind]] 1305 >m_return_bind 1306 #EQ whd in EQ : (??%?); destruct(EQ) [2: %] 1307 >H3 in EQ; 1308 normalize nodelta 1309 #EQ1 whd in EQ1 : (??%%); destruct(EQ1) 1310 normalize nodelta // 1293 [ #H @('bind_inversion H) #bv1'' 1294 >EQ_bv1' #EQ destruct(EQ) ] 1295 whd in ⊢ (??%%→?); #EQ destruct(EQ) % 1311 1296 qed. 1312 1297 … … 1320 1305 be_opaccs op (sigma_beval … prf1) (sigma_beval … prf2) = 1321 1306 return 〈(sigma_beval … prf1'),(sigma_beval … prf2')〉. 1322 #p #p' #graph_prog #sigma #op #val1 #val2 1323 #opaccs1 #opaccs2 #prf1 #prf2 1324 whd in match be_opaccs; normalize nodelta 1325 #H elim(bind_inversion ????? H) H 1326 #x * #x_spec 1327 #H elim(bind_inversion ????? H) H 1328 #y * #y_spec 1329 #H lapply H #H1 normalize in H; elim(opaccs_implementation op x y) in H; 1330 #b1 #b2 #EQ normalize in EQ; destruct(EQ) 1331 % 1332 [whd in match sigma_beval_opt; normalize nodelta % #ABS 1333 whd in ABS : (??%?); destruct(ABS)] 1334 % 1335 [whd in match sigma_beval_opt; normalize nodelta % #ABS 1336 whd in ABS : (??%?); destruct(ABS)] 1307 #p #p' #graph_prog #sigma #op 1308 @bv_pc_other 1309 [ #pc1 #p1 #val2 1310  #val1 #val1_no_pc @bv_pc_other 1311 [ #pc #p  #val2 #val2_no_pc ] 1312 ] 1313 #opaccs1 #opaccs2 1314 #prf1 #prf2 1315 [1,2: [2: #H @('bind_inversion H) #by1 #_ ] 1316 whd in ⊢ (??%%→?); #EQ destruct] 1317 #EQ 1318 >(sigma_bv_no_pc … val1_no_pc) 1319 >(sigma_bv_no_pc … val2_no_pc) 1320 cut (bv_no_pc opaccs1 ∧ bv_no_pc opaccs2) 1321 [ cases val1 in EQ; cases daemon ] * 1322 #H1 #H2 @('bind_inversion EQ) #bt #bt_spec 1323 #H3 @('bind_inversion H3) #bt' 1324 #bt_spec' cases (opaccs eval op bt bt') 1325 #ev_bt #ev_bt' normalize nodelta 1326 #EQ1 whd in EQ1 : (??%%); destruct(EQ1) 1327 % [ whd in match sigma_beval_opt ; normalize nodelta % 1328 #ABS whd in ABS : (??%?); destruct(ABS) ] 1329 % [ whd in match sigma_beval_opt ; normalize nodelta % 1330 #ABS whd in ABS : (??%?); destruct(ABS) ] 1331 >(sigma_bv_no_pc … H1) 1332 >(sigma_bv_no_pc … H2) assumption 1333 qed. 1334 1335 lemma sigma_ptr_commute : 1336 ∀ p, p', graph_prog , sigma , val1, val2, ptr, prf1, prf2. 1337 pointer_of_address 〈val1,val2〉= return ptr → 1338 pointer_of_address 〈sigma_beval p p' graph_prog sigma val1 prf1, 1339 sigma_beval p p' graph_prog sigma val2 prf2〉 = return ptr. 1340 #p #p' #graph_prog #sigma #val1 #val2 #ptr #prf1 #prf2 1337 1341 whd in match sigma_beval; normalize nodelta 1338 1342 @opt_safe_elim #sigma_val1 #sigma_val1_spec 1339 @opt_safe_elim #sigma_val2 #sigma_val2_spec 1340 @opt_safe_elim #sigma_op1 #sigma_op1_spec 1341 @opt_safe_elim #sigma_op2 #sigma_op2_spec 1342 lapply x_spec x_spec lapply sigma_val1_spec sigma_val1_spec 1343 inversion val1 whd in match Byte_of_val; normalize nodelta 1344 [ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)] 1345 [#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)] 1346 #bt_val1 #val1_spec whd in match sigma_beval_opt; normalize nodelta 1347 whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ) 1348 #EQ whd in EQ : (???%); destruct(EQ) 1349 lapply y_spec y_spec lapply sigma_val2_spec sigma_val2_spec 1350 inversion val2 whd in match Byte_of_val; normalize nodelta 1351 [ 1,2,5,6,7: [ 1,2: #_ #_] [3: #a #_ #_] [4,5 : #a #b #_ #_] #ABS whd in ABS : (???%); destruct(ABS)] 1352 [#pt1 #pt2 #a #_ #_ #ABS whd in ABS : (???%); destruct(ABS)] 1353 #bt_val2 #val2_spec whd in match sigma_beval_opt; normalize nodelta 1354 whd in ⊢ ((??%?)→ ?); #EQ destruct(EQ) normalize nodelta 1355 #EQ whd in EQ : (???%); destruct(EQ) 1356 >m_return_bind >m_return_bind 1357 whd in match sigma_beval_opt in sigma_op1_spec; 1358 normalize nodelta in sigma_op1_spec; 1359 whd in sigma_op1_spec : (??%?); destruct(sigma_op1_spec) 1360 whd in match sigma_beval_opt in sigma_op2_spec; 1361 normalize nodelta in sigma_op2_spec; 1362 whd in sigma_op2_spec : (??%?); destruct(sigma_op2_spec) 1363 >H1 % 1364 qed. 1343 @opt_safe_elim #sigma_Val2 #sigma_val2_spec 1344 whd in match pointer_of_address; whd in match pointer_of_bevals; 1345 normalize nodelta cases val1 in sigma_val1_spec; normalize nodelta 1346 [1,2,3,4,5: [ #ptr1 #ptr2 #p  #by  #p] #_ #ABS whd in ABS : (??%%); destruct(ABS) 1347  #ptr2 #p2 whd in match sigma_beval_opt; normalize nodelta 1348 #EQ whd in EQ : (??%%); destruct(EQ) cases val2 in sigma_val2_spec; normalize nodelta 1349 [1,2,3,4,5: [ #ptr1 #ptr2 #p  #by  #p] #_ #ABS whd in ABS : (??%%); destruct(ABS) 1350  #ptr1 #p1 whd in match sigma_beval_opt; normalize nodelta 1351 #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta // 1352  #a #b #_ #ABS whd in ABS : (???%); destruct(ABS) 1353 ] 1354  #a #b #_ #ABS whd in ABS : (???%); destruct(ABS) 1355 ] 1356 skip 1357 qed. 1358 1365 1359 1366 1360 lemma eval_seq_no_pc_sigma_commute : … … 1377 1371 f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) = 1378 1372 return sigma_state … gss st' prf'. 1379 #p #p' #graph_prog #stack_sizes #sigma #gss 1373 #p #p' #graph_prog #stack_sizes #sigma #gss #f 1380 1374 #fn #st #stmt 1381 1375 #st' #prf 1382 whd in match eval_seq_no_pc; 1376 whd in match eval_seq_no_pc; 1383 1377 cases stmt normalize nodelta 1384 1378 [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) %{prf} // 1385  (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) H #H 1386 change with 1387 (pair_reg_move p (joint_closed_internal_function (make_sem_graph_params p p')) 1388 (make_sem_graph_params p p') ??) in H : (??%?); 1389 lapply H H 1390 whd in match pair_reg_move; normalize nodelta #H 1391 elim(bind_inversion ????? H) H #reg * #reg_spec #EQ whd in EQ : (??%%); destruct(EQ) 1379  (* MOVE *) #mv_sig #H 1380 whd in match pair_reg_move; normalize nodelta 1381 @('bind_inversion H) H #reg #reg_spec #EQ whd in EQ : (??%%); destruct(EQ) 1392 1382 elim(pair_reg_move_commute ???????? (proj2 … (proj1 … prf)) reg_spec) 1393 1383 #wf_regs #pm_spec >pm_spec >m_return_bind % [2: %] … … 1399 1389 ] 1400 1390  (* POP *) 1401 #a #H lapply(err_eq_from_io ????? H) H #H elim (bind_inversion ????? H) H 1402 * #val #st1 * #vals_spec #H 1403 change with (acca_store p 1404 (joint_closed_internal_function (make_sem_graph_params p p')) 1405 (make_sem_graph_params p p') a val st1 = ?) in H; 1406 change with (pop (make_sem_graph_params p p') ? = ?) in vals_spec; 1391 #a #H @('bind_inversion H) H 1392 * #val #st1 #vals_spec #H 1407 1393 lapply vals_spec vals_spec 1408 1394 whd in match pop; normalize nodelta … … 1438 1424 ] 1439 1425 #prf' #acca_store_commute %{prf'} 1440 whd in match sigma_state in ⊢ (??(???? (?????(?????%?)?))?);1426 whd in match sigma_state in ⊢ (??(?????(?????%?)?)?); 1441 1427 whd in match sigma_is; normalize nodelta 1442 1428 @opt_safe_elim #int_stack #int_stack_sigma_spec 1443 1429 >is_stack_st_spec in int_stack_sigma_spec; 1444 1430 whd in match sigma_is_opt; normalize nodelta 1445 #IS_SPEC elim(bind_opt_inversion ?????IS_SPEC) IS_SPEC1446 [ #sigma_bv *#sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)1447  #sigma_bv_not_used *#sigma_bv_not_used_spec #IS_SPEC1448 elim(bind_opt_inversion ?????IS_SPEC) IS_SPEC1449 #sigma_bv *#sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]1431 #IS_SPEC @('bind_inversion IS_SPEC) IS_SPEC 1432 [ #sigma_bv #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ) 1433  #sigma_bv_not_used #sigma_bv_not_used_spec #IS_SPEC 1434 @('bind_inversion IS_SPEC) IS_SPEC 1435 #sigma_bv #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)] 1450 1436 normalize nodelta >m_return_bind 1451 @err_eq_to_io <acca_store_commute 1452 whd in match helper_def_store; normalize nodelta 1453 whd in match acca_store; normalize nodelta 1437 <acca_store_commute 1438 whd in match helper_def_store; whd in match acca_store; 1454 1439 whd in match sigma_beval; normalize nodelta 1455 1440 @opt_safe_elim #xx #xx_spec … … 1459 1444 change with (return set_regs (make_sem_lin_params p p') ? 1460 1445 (set_istack (make_sem_lin_params p p') ? ?) = ?); 1461 change with (? = return set_regs ? ?1462 (sigma_state p p' graph_prog sigma gss1463 (set_istack ? (one_is Bv_not_used) st) ?))1464 1446 >(set_istack_sigma_commute ?????? (one_is Bv_not_used) (one_is sigma_bv_not_used) ???) 1465 1447 [2: whd in match sigma_is_opt; normalize nodelta >sigma_bv_not_used_spec … … 1467 1449 ] 1468 1450  (* PUSH *) 1469 #a #H lapply(err_eq_from_io ????? H) H #H elim (bind_inversion ????? H) H 1470 #val * 1471 change with (((acca_arg_retrieve p 1472 (joint_closed_internal_function (make_sem_graph_params p p')) 1473 (make_sem_graph_params p p') st a) = ?) → ?) 1474 #graph_ret_spec 1451 #a #H @('bind_inversion H) H 1452 #val #graph_ret_spec 1475 1453 change with (((push (make_sem_graph_params p p') ? ?) = ?) → ?) 1476 1454 #graph_push_spec … … 1478 1456 #val_wf #acca_arg_retrieve_commute 1479 1457 whd in match push in graph_push_spec; normalize nodelta in graph_push_spec; 1480 elim(bind_inversion ?????graph_push_spec) graph_push_spec1481 #int_stack *#int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ)1458 @('bind_inversion graph_push_spec) graph_push_spec 1459 #int_stack #int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ) 1482 1460 % 1483 1461 [ @hide_prf % [% [% [ @(proj1 … (proj1 … (proj1 … prf))) ]]] … … 1502 1480 whd in match sigma_is_opt; normalize nodelta 1503 1481 inversion(sigma_beval_opt ???? y) 1504 [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf))) 1505 xxxxxxxxxxxxxxxxxx 1506 1507 qed. 1508 1509 lemma eval_statement_no_pc_sigma_commute : 1510 ∀p,p',graph_prog. 1511 let lin_prog ≝ linearise p graph_prog in 1512 ∀stack_sizes. 1513 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 1514 ∀f,fn,st,stmt,st'. 1515 ∀prf : well_formed_state … gss st. 1516 eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 1517 f fn stmt st = return st' → 1518 ∃prf'. 1519 eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes)) 1520 f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt) 1521 (sigma_state … gss st prf) = 1522 return sigma_state … gss st' prf'. 1523 #p #p' #graph_prog #stack_sizes #sigma #gss 1524 #f #fn #st * [* [ #stmt  #a #lbl ] #nxt  * [ #lbl   #fl #called #args ]] 1525 #st' #prf 1526 whd in match eval_statement_no_pc; normalize nodelta 1527 [ @eval_seq_no_pc_sigma_commute 1528 2,3,4: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % 1529  (* tailcall, follow proof of CALL in previous lemma *) 1530 cases daemon 1531 ] 1532 qed. 1533 1534 ======= 1482 [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf))) 1535 1483 whd in match sigma_is_opt; >H normalize nodelta >ABS 1536 1484 whd in ⊢ ((?(??%?))→?); * #h1 @h1 % … … 1542 1490 ] 1543 1491 ] 1544  1545 whd in match helper_def_retrieve in acca_arg_retrieve_commute; 1546 normalize nodelta in acca_arg_retrieve_commute; 1547 whd in match acca_arg_retrieve; normalize nodelta 1548 @err_eq_to_io 1549 change with 1550 ((! v ← (acca_arg_retrieve_ p 1551 (joint_closed_internal_function (make_sem_lin_params p p')) 1552 (make_sem_lin_params p p') 1553 (regs (make_sem_lin_params p p') 1554 (sigma_state p p' graph_prog sigma gss st prf)) 1555 a); 1556 ?)=?) 1557 change with ((! v ← ?; push (make_sem_lin_params p p') ? ?) = ?) 1558 cut((acca_arg_retrieve_ p ? ? ? a) = return sigma_beval p ? ? ? ? val_wf) 1559 [4: assumption     ] #H >H >m_return_bind 1560 whd in match push; normalize nodelta 1561 H elim(is_push_sigma_commute ???????? prf val_wf int_stack_spec) 1562 #wf_is #EQ >EQ >m_return_bind // 1492  change with (acca_arg_retrieve ????? = ?) in acca_arg_retrieve_commute; 1493 >acca_arg_retrieve_commute in ⊢ (??%?); >m_return_bind 1494 elim(is_push_sigma_commute … (proj2 … (proj1 …(proj1 … prf))) val_wf int_stack_spec) 1495 #wf_is #EQ whd in match push; normalize nodelta >EQ % 1563 1496 ] 1564 1497  (*C_ADDRESS*) 1565 #sy 1566 change with ((member ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?)1498 #sy 1499 change with ((member ? ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?) 1567 1500 #sy_prf 1568 1501 change with ((dpl_reg p) → ?) #dpl 1569 1502 change with ((dph_reg p) → ?) #dph 1570 #H lapply(err_eq_from_io ????? H) H1571 1503 change with ((( ! st1 ← dpl_store p 1572 1504 (joint_closed_internal_function (make_sem_graph_params p p')) 1573 (make_sem_graph_params p p')1505 ? 1574 1506 ? 1575 1507 ? … … 1597 1529 change with ((( ! st1 ← ? ; 1598 1530 dph_store p (joint_closed_internal_function (make_sem_graph_params p p')) 1599 (make_sem_graph_params p p')?1531 ? ? 1600 1532 (BVptr 1601 1533 (mk_pointer … … 1617 1549 ? 1618 1550 ) ?) = ?) → ?) 1619 #H elim(bind_inversion ?????H) H1620 #st1 *#dpl_st11551 #H @('bind_inversion H) H 1552 #st1 #dpl_st1 1621 1553 elim(store_commute p p' graph_prog sigma ?? gss (dpl_store_commute … gss) ???? prf ? dpl_st1) 1622 1554 [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); % 1623 1555 #ABS destruct(ABS)] 1624 1556 #wf_st1 whd in match helper_def_store; normalize nodelta 1625 #H elim(bind_inversion ????? H) H #reg1 *#reg1_spec #EQ whd in EQ : (??%%);1557 #H @('bind_inversion H) H #reg1 #reg1_spec #EQ whd in EQ : (??%%); 1626 1558 destruct(EQ) EQ 1627 1559 #dph_st' … … 1630 1562 % #ABS destruct(ABS)] 1631 1563 #wf_st' whd in match helper_def_store; normalize nodelta 1632 #H elim(bind_inversion ????? H) H #reg2 *#reg2_spec #EQ whd in EQ : (??%%);1564 #H @('bind_inversion H) H #reg2 #reg2_spec #EQ whd in EQ : (??%%); 1633 1565 destruct(EQ) EQ %{wf_st'} <e1 1634 1566 whd in match dpl_store; normalize nodelta … … 1676 1608  (*C_OPACCS*) 1677 1609 #op #a #b #arg1 #arg2 1678 #H lapply(err_eq_from_io ????? H) H 1679 #H elim(bind_inversion ????? H) H 1680 #val1 * #val1_spec 1610 #H @('bind_inversion H) H 1611 #val1 #val1_spec 1681 1612 elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf val1_spec) 1682 1613 #wf_val1 #sigma_val1_commute 1683 #H elim(bind_inversion ????? H) H 1684 #val2 * #val2_spec 1614 #H @('bind_inversion H) H #val2 #val2_spec 1685 1615 elim (retrieve_commute p p' graph_prog sigma ?? gss (accb_arg_retrieve_commute … gss)??? prf val2_spec) 1686 1616 #wf_val2 #sigma_val2_commute 1687 #H elim(bind_inversion ?????H) H *1688 #opaccs1 #opaccs2 *#opaccs_spec1617 #H @('bind_inversion H) H * 1618 #opaccs1 #opaccs2 #opaccs_spec 1689 1619 elim(beopaccs_sigma_commute p p' graph_prog sigma ????? wf_val1 wf_val2 opaccs_spec) 1690 1620 #wf_opaccs1 * #wf_opaccs2 #be_opaccs_commute 1691 #H elim(bind_inversion ????? H) H 1692 #st1 * #st1_spec 1621 #H @('bind_inversion H) H #st1 #st1_spec 1693 1622 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_opaccs1 st1_spec) 1694 1623 #wf_st1 #sigma_st1_commute #final_spec … … 1707 1636 whd in match helper_def_store in sigma_st1_commute; 1708 1637 normalize nodelta in sigma_st1_commute; 1709 elim(bind_inversion ?????sigma_st1_commute)1710 #reg1 *#reg1_spec #EQ whd in EQ : (??%%); destruct(EQ)1638 @('bind_inversion sigma_st1_commute) 1639 #reg1 #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1711 1640 whd in match acca_store; normalize nodelta 1712 1641 >reg1_spec >m_return_bind … … 1714 1643 whd in match helper_def_store in sigma_final_commute; 1715 1644 normalize nodelta in sigma_final_commute; 1716 elim(bind_inversion ?????sigma_final_commute)1717 #reg2 *#reg2_spec #EQ whd in EQ : (??%%); destruct(EQ)1645 @('bind_inversion sigma_final_commute) 1646 #reg2 #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ) 1718 1647 whd in match accb_store; normalize nodelta 1719 1648 >reg2_spec >m_return_bind whd in match set_regs; normalize nodelta 1720 1649 >e1 % 1721 1650  (*C_OP1*) 1651 #op #a #arg #H @('bind_inversion H) H #val1 #val1_spec 1652 elim (retrieve_commute p p' graph_prog sigma ?? ? (acca_retrieve_commute … gss) ??? prf val1_spec) 1653 #wf_val1 #sigma_val1_commute #H @('bind_inversion H) #op_val1 #op_val1_spec 1654 cut(∃ wf_opval1. be_op1 op (sigma_beval … wf_val1) = return sigma_beval p p' graph_prog sigma op_val1 wf_opval1) 1655 [ whd in match be_op1 in op_val1_spec; normalize nodelta in op_val1_spec; 1656 @('bind_inversion op_val1_spec) #bt1 #b1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1657 % [ @hide_prf whd in match sigma_beval_opt; normalize nodelta % #ABS whd in ABS : (??%?); 1658 destruct(ABS)] 1659 whd in match Byte_of_val in b1_spec; normalize nodelta in b1_spec; 1660 whd in match sigma_beval; normalize nodelta 1661 @opt_safe_elim #sigma_val1 #sigma_val1_spec 1662 @opt_safe_elim #sigma_op_val1 #sigma_op_val1_spec 1663 cases(val1) in b1_spec op_val1_spec sigma_val1_spec; normalize nodelta 1664 [4: #bt2 #EQ whd in EQ : (???%); destruct(EQ) 1665 whd in match Byte_of_val; normalize nodelta >m_return_bind 1666 #EQ whd in EQ : (??%%); destruct(EQ) 1667 whd in match sigma_beval_opt; normalize nodelta 1668 #EQ whd in EQ : (??%%); destruct(EQ) 1669 whd in match sigma_beval_opt in sigma_op_val1_spec; 1670 normalize nodelta in sigma_op_val1_spec; whd in sigma_op_val1_spec : (??%?); 1671 destruct(sigma_op_val1_spec) // 1672 *: [3: #pt1 #pt2 #p] [4:#p] [5:#pt #p] [6:#pc #p] #ABS whd in ABS : (???%); 1673 destruct(ABS) 1674 ] 1675 ] * #wf_op_val1 #sigma_op_val1_commute #H1 1676 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_op_val1 H1) 1677 #wf_st' #final_commute %{wf_st'} 1678 change with (acca_retrieve ????? = ?) in sigma_val1_commute; 1679 >sigma_val1_commute >m_return_bind >sigma_op_val1_commute >m_return_bind 1680 assumption 1681  (*C_OP2*) 1682 #op #a #arg1 #arg2 #H @('bind_inversion H) H 1683 @bv_pc_other (*val1*) 1684 [ #pc_val1 #part_val1 1685  #val1 #val1_no_pc 1686 ] #val1_spec 1687 #H @('bind_inversion H) H 1688 [ #val2 1689  @bv_pc_other (*val2*) 1690 [ #pc_val2 #part_val2 1691  #val2 #val2_no_pc 1692 ] 1693 ] #val2_spec 1694 #H @('bind_inversion H) H * #val3 #bit1 1695 [1,2: [2: cases val1 [#pt1 #pt2 #p#by#p#pt #p#pc #p] cases op ] 1696 whd in ⊢(??%%→?); #EQ destruct(EQ) ] 1697 #H cut (bv_no_pc val3) 1698 [ lapply H H 1699 whd in match be_op2; normalize nodelta 1700 cases val1 normalize nodelta 1701 [1,7: [2: #pc #p] #ABS whd in ABS : (???%); destruct(ABS) 1702 2,3,5: [ #pt1 #pt2 #p  #p ] cases op normalize nodelta 1703 [1,2,3,4,6,7,8,9,10,12,13,14,15,16,17 : #ABS whd in ABS : (???%); destruct(ABS)] 1704 cases val2 normalize nodelta 1705 [1,2,3,4,5,6,7,8,9,12,13,14,15,16,17,18,21 : 1706 [#ptr1 #ptr2 #p #byte2  #p  #ptr #p  #pc #p    #p #ptr #p  #pc #p    #pt1 #pt2 #p  #bt  #pc #p] 1707 #EQ whd in EQ : (??%%); destruct(EQ) // 1708  #pt3 #pt4 #p1 @if_elim [2: #_ #ABS whd in ABS : (??%%); destruct(ABS)] 1709 #_ @if_elim #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1710  #bt @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)] 1711 #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1712  #p3 @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)] 1713 #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1714  #ptt #part @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)] 1715 #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1716 ] 1717 4,6: [ #bt1  #ptr #p] cases val2 normalize nodelta 1718 [1,3,4,5,7,8,9,10,14: [#pt1 #pt2 #p 1719  #bt2 #H @('bind_inversion H) #bit #bit_spec cases(op2 ? ? ? ? ?) 1720 #x #y normalize nodelta 1721  #p  #pc #part    #ptr #ptr' #p #pc #p] 1722 #EQ whd in EQ : (??%%); destruct(EQ) // 1723 *: [#ptr #p #bt  #p  #ptr #p ] cases op normalize nodelta 1724 [1,2,3,4,5,6,9,10,11,12,16,17,18,19,20,21,22,23,25,26,28,29: 1725 #EQ whd in EQ : (??%%); destruct(EQ) // 1726 7,8,13,14,15: whd in match be_add_sub_byte; normalize nodelta 1727 cases(ptype ?) normalize nodelta [2,4,6,8,10: #ABS whd in ABS : (??%%); destruct(ABS)] 1728 cases p * normalize nodelta #n_part_spec [2,6: #_ #ABS whd in ABS : (??%%); destruct(ABS)] 1729 [1,2,4,5,7 : #H @('bind_inversion H) #bit #bit_spec 1730 @if_elim [1,3,5,7,9: #_ #ABS whd in ABS : (??%%); destruct(ABS)] 1731 #_ elim(op2 ? ? ? ? ?) #a1 #a2 normalize nodelta 1732 #EQ whd in EQ : (??%%); destruct(EQ) // 1733 *: #_ cases(carry ? st) normalize nodelta 1734 [1,2,4,5,7,8 : [1,3,5: #bool ] #ABS whd in ABS : (???%); destruct(ABS)] 1735 #bool #pt #p1 #bitvect @if_elim #_ [2,4,6: #ABS whd in ABS : (???%); destruct(ABS)] 1736 @If_elim [2,4,6: #_ #ABS whd in ABS : (???%); destruct(ABS)] 1737 #proof elim(op2_bytes ?????) #a #b 1738 normalize nodelta #EQ whd in EQ : (???%); destruct(EQ) // 1739 ] 1740 24,30: @if_elim #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1741  cases(ptype ?) normalize nodelta [2: #ABS whd in ABS : (???%); destruct(ABS)] 1742 @if_elim #_ [2: #ABS whd in ABS : (??%%); destruct(ABS)] 1743 #H @('bind_inversion H) #b #_ elim(op2 ?????) #x #y normalize nodelta 1744 #EQ whd in EQ : (??%%); destruct(EQ) // 1745 ] 1746 ] 1747 ] 1748 ] #val3_spec lapply H H #val3_op_spec #H @('bind_inversion H) #st1 1749 #st1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1750 elim(retrieve_commute p p' graph_prog sigma ?? ? (acca_arg_retrieve_commute … gss) ??? prf val1_spec) 1751 #wf_val1 #sigma_val1_commute 1752 elim(retrieve_commute p p' graph_prog sigma ?? ? (snd_arg_retrieve_commute … gss) ??? prf val2_spec) 1753 #wf_val2 #sigma_val2_commute 1754 1755 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf ? st1_spec) 1756 [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta inversion val3 normalize nodelta 1757 [7: #pc #p #H >H in val3_spec; #ABS @⊥ // 1758 *: [#pt1 #pt2 #p#bt#p#pt #p] #_ % #ABS whd in ABS : (??%%); destruct(ABS) 1759 ] 1760 ] 1761 #wf_st1 #sigma_st1_commute 1762 % 1763 [ @hide_prf % [2: @(proj2 … wf_st1)] % [2: @(proj2 … (proj1 … wf_st1))] 1764 % [2:@(proj2 … (proj1 … (proj1 … wf_st1)))] 1765 @(proj1 … (proj1 … (proj1 … wf_st1))) 1766 ] 1767 change with ((acca_arg_retrieve ?????)=?) in sigma_val1_commute; 1768 >sigma_val1_commute >m_return_bind 1769 change with ((snd_arg_retrieve ?????)=?) in sigma_val2_commute; 1770 >sigma_val2_commute >m_return_bind 1771 >(sigma_bv_no_pc … val1_no_pc) >(sigma_bv_no_pc … val2_no_pc) 1772 whd in match sigma_state in ⊢ (??(?????%?)?); normalize nodelta 1773 >val3_op_spec >m_return_bind 1774 change with ((acca_store ??????) = ?) in sigma_st1_commute; 1775 >(sigma_bv_no_pc … val3_spec) in sigma_st1_commute; 1776 #H >H >m_return_bind // 1777  (*C_CLEAR_CARRY*) 1778 #EQ whd in EQ : (??%%); destruct(EQ) 1779 %{prf} // 1780  (*C_SET_CARRY*) 1781 #EQ whd in EQ : (??%%); destruct(EQ) %{prf} // 1782  (*C_LOAD*) 1783 #a #dpl #dph #H @('bind_inversion H) H #val1 #val1_spec 1784 #H @('bind_inversion H) H #val2 #val2_spec 1785 #H @('bind_inversion H) H #ptr #ptr_spec 1786 #H @('bind_inversion H) H #val3 #val3_spec #final_spec 1787 elim(retrieve_commute p p' graph_prog sigma ?? ? (dph_arg_retrieve_commute … gss) ??? prf val1_spec) 1788 #wf_val1 #sigma_val1_commute 1789 elim(retrieve_commute p p' graph_prog sigma ?? ? (dpl_arg_retrieve_commute … gss) ??? prf val2_spec) 1790 #wf_val2 #sigma_val2_commute 1791 lapply(opt_eq_from_res ???? val3_spec) val3_spec #val3_spec 1792 elim(beloadv_sigma_commute p p' graph_prog sigma ???? val3_spec) 1793 [2: @hide_prf @(proj2 … prf)] #wf_val3 #sigma_val3_commute 1794 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_val3 final_spec) 1795 #wf_st' #sigma_st_commute %{wf_st'} 1796 change with (dph_arg_retrieve ????? = ?) in sigma_val1_commute; 1797 >sigma_val1_commute >m_return_bind 1798 change with (dpl_arg_retrieve ????? = ?) in sigma_val2_commute; 1799 >sigma_val2_commute >m_return_bind 1800 >(sigma_ptr_commute p p' graph_prog sigma … ptr_spec) 1801 >m_return_bind >sigma_val3_commute >m_return_bind 1802 change with (acca_store ?????? = ?) in sigma_st_commute; assumption 1803  (*C_STORE*) 1804 #dpl #dph #a #H @('bind_inversion H) H #val1 #val1_spec 1805 #H @('bind_inversion H) H #val2 #val2_spec 1806 #H @('bind_inversion H) H #ptr #ptr_spec 1807 #H @('bind_inversion H) H #val3 #val3_spec 1808 #H @('bind_inversion H) H #mem #mem_spec #EQ whd in EQ : (??%%); destruct(EQ) 1809 elim(retrieve_commute p p' graph_prog sigma ?? ? (dph_arg_retrieve_commute … gss) ??? prf val1_spec) 1810 #wf_val1 #sigma_val1_commute 1811 elim(retrieve_commute p p' graph_prog sigma ?? ? (dpl_arg_retrieve_commute … gss) ??? prf val2_spec) 1812 #wf_val2 #sigma_val2_commute 1813 elim(retrieve_commute p p' graph_prog sigma ?? ? (acca_arg_retrieve_commute … gss) ??? prf val3_spec) 1814 #wf_val3 #sigma_val3_commute 1815 lapply(opt_eq_from_res ???? mem_spec) mem_spec #mem_spec 1816 elim(bestorev_sigma_commute p p' graph_prog sigma ????? wf_val3 mem_spec) 1817 [2: @hide_prf @(proj2 … prf)] 1818 #wf_mem #sigma_mem_commute 1819 % [@hide_prf % [2: @wf_mem] % [2: @(proj2 … (proj1 … prf))] % 1820 [ @(proj1 … (proj1 … (proj1 … prf)))  @(proj2 … (proj1 … (proj1 … prf)))] 1821 ] 1822 change with (dph_arg_retrieve ????? = ?) in sigma_val1_commute; 1823 >sigma_val1_commute >m_return_bind 1824 change with (dpl_arg_retrieve ????? = ?) in sigma_val2_commute; 1825 >sigma_val2_commute >m_return_bind 1826 >(sigma_ptr_commute p p' graph_prog sigma … ptr_spec) 1827 >m_return_bind 1828 change with (acca_arg_retrieve ????? = ?) in sigma_val3_commute; 1829 >sigma_val3_commute >m_return_bind >sigma_mem_commute 1830 >m_return_bind // 1831  (*CALL*) 1832 #f #args #dest 1833 #EQ whd in EQ : (??%%); destruct(EQ) %{prf} // 1834  (*C_EXT*) 1835 #s_ext #H 1836 elim(eval_ext_seq_commute … sigma gss … prf H) 1837 #wf_st' #H1 %{wf_st'} >H1 // 1838 ] 1839 skip 1840 qed. 1841 (* check(save_frame_commute)*) 1722 1842 1723 >>>>>>> .r2528 1843 lemma eval_statement_no_pc_sigma_commute : 1844 ∀p,p',graph_prog. 1845 let lin_prog ≝ linearise p graph_prog in 1846 ∀stack_sizes. 1847 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 1848 ∀f,fn,st,stmt,st'. 1849 ∀prf : well_formed_state … gss st. 1850 eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 1851 f fn stmt st = return st' → 1852 ∃prf'. 1853 eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes)) 1854 f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt) 1855 (sigma_state … gss st prf) = 1856 return sigma_state … gss st' prf'. 1857 #p #p' #graph_prog #stack_sizes #sigma #gss 1858 #f #fn #st * [* [ #stmt  #a #lbl ] #nxt  * [ #lbl   #fl #called #args ]] 1859 #st' #prf 1860 whd in match eval_statement_no_pc; normalize nodelta 1861 [ @eval_seq_no_pc_sigma_commute 1862 *: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % 1863 ] 1864 qed. 1865 1866 1724 1867 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 1725 1868 ex1_intro: ∀ x:A. P x → ex_Type1 A P.
Note: See TracChangeset
for help on using the changeset viewer.