Changeset 1806 for src/RTLabs
 Timestamp:
 Mar 5, 2012, 12:38:26 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1805 r1806 424 424  #s #tr #s' #d #t1 #CL #NW #E normalize in E; destruct 425 425 inversion NW [ #H1 #H2 #H3 #H4 #H5 destruct  #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 destruct // ] 426 ] qed. 427 428 429 lemma will_return_lower : ∀ge,d,s,t. 430 will_return ge d s t → 431 ∀d'. d' ≤ d → 432 will_return ge d' s t. 433 #ge #d0 #s0 #t0 #TM elim TM 434 [ #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE % /2/ 435  #s #tr #s' #d #EX #tr #CL #TM1 #IH #d' #LE %2 // @IH /2/ 436  #s #tr #s' #d #EX #tr #CL #TM1 #IH * 437 [ #LE @wr_base // 438  #d' #LE %3 // @IH /2/ 439 ] 440  #s #tr #s' #EX #tr #CL * 441 [ #_ @wr_base // 442  #d' #LE @⊥ /2/ 443 ] 426 444 ] qed. 427 445 … … 1398 1416 ] 1399 1417 ] qed. 1400 1418 1419 1420 1421 1422 definition soundly_labelled_fn : internal_function → Prop ≝ 1423 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n. 1424 1425 definition soundly_labelled_ge : genv → Prop ≝ 1426 λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f. 1427 1428 definition soundly_labelled_state : state → Prop ≝ 1429 λs. match s with 1430 [ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs 1431  Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn  External _ ⇒ True ] ∧ 1432 All ? (λf. soundly_labelled_fn (func f)) fs 1433  Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs 1434  Finalstate _ ⇒ True 1435 ]. 1436 1437 lemma steps_from_sound : ∀s. 1438 RTLabs_cost s = true → 1439 soundly_labelled_state s → 1440 ∃n. state_bound_on_steps_to_cost s n. 1441 * [ #f #fs #m #CS  #a #b #c #d #e #E normalize in E; destruct  #a #b #c #d #E normalize in E; destruct  #a #E normalize in E; destruct ] 1442 whd in ⊢ (% → ?); * #SLF #_ 1443 cases (SLF (next f) (next_ok f)) #n #B1 1444 %{n} % @B1 1445 qed. 1446 1447 lemma soundly_labelled_state_step : ∀ge,s,tr,s'. 1448 soundly_labelled_ge ge → 1449 eval_statement ge s = Value ??? 〈tr,s'〉 → 1450 soundly_labelled_state s → 1451 soundly_labelled_state s'. 1452 #ge #s #tr #s' #ENV #EV #S 1453 inversion (eval_perserves … EV) 1454 [ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct 1455 whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S 1456  #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct 1457 whd in S ⊢ %; % 1458 [ cases fd in FFP ⊢ %; // #fn #FFP @ENV // 1459  inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S 1460 ] 1461  #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct 1462 whd in S ⊢ %; @S 1463  #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct 1464 whd in S ⊢ %; cases S // 1465  #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct 1466 whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S 1467  #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I 1468 ] qed. 1469 1470 lemma soundly_labelled_state_preserved : ∀s,s'. 1471 stack_preserved ends_with_ret s s' → 1472 soundly_labelled_state s → 1473 soundly_labelled_state s'. 1474 #s0 #s0' #SP inversion SP 1475 [ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct 1476  #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct 1477 inversion S1 1478 [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct 1479 * #_ #S whd in S; 1480 inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 1481 destruct @S 1482  #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S 1483 inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 1484 destruct @S 1485  #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S 1486 inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 1487 destruct @S 1488 ] 1489  // 1490  // 1491 ] qed. 1492 1401 1493 (* When constructing an infinite trace, we need to be able to grab the finite 1402 1494 portion of the trace for the next [trace_label_diverges] constructor. We … … 1405 1497 record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ { 1406 1498 ro_well_cost_labelled: well_cost_labelled_state s; 1499 ro_soundly_labelled: soundly_labelled_state s; 1407 1500 ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t)); 1408 1501 ro_not_undefined: not_wrong … t; … … 1416 1509 remainder_ok ge s' t → 1417 1510 finite_prefix ge s 1418  fp_tac : ∀s,s'. 1419 trace_any_call (RTLabs_status ge) s s' → 1420 ∀t:flat_trace io_out io_in ge s'. 1421 remainder_ok ge s' t → 1422 finite_prefix ge s 1511  fp_tac : ∀s1,s2,s3,tr. 1512 trace_any_call (RTLabs_status ge) s1 s2 → 1513 well_cost_labelled_state s2 → 1514 eval_statement ge s2 = Value ??? 〈tr,s3〉 → 1515 ∀t:flat_trace io_out io_in ge s3. 1516 remainder_ok ge s3 t → 1517 finite_prefix ge s1 1423 1518 . 1424 1519 … … 1434 1529 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST)) 1435 1530 rem rok 1436  fp_tac s' sf TAC rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s sf 1437 (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem rok 1531  fp_tac s1 s2 s3 tr TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 tr 1532 (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) 1533 WCL2 EV rem rok 1438 1534 ]. 1439 1535 1440 definition fp_add_terminating_call : ∀ge,s,s1,s' .1536 definition fp_add_terminating_call : ∀ge,s,s1,s''. 1441 1537 (∃t. eval_statement ge s = Value ??? 〈t,s1〉) → 1442 1538 ∀CALL:RTLabs_classify s = cl_call. 1443 finite_prefix ge s' →1444 trace_label_return (RTLabs_status ge) s1 s' →1445 as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' →1446 RTLabs_cost s' = false →1539 finite_prefix ge s'' → 1540 trace_label_return (RTLabs_status ge) s1 s'' → 1541 as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s'' → 1542 RTLabs_cost s'' = false → 1447 1543 finite_prefix ge s ≝ 1448 λge,s,s1,s' ,EVAL,CALL,fp.1449 match fp return λs' .λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → RTLabs_cost s' = false → finite_prefix ge s with1450 [ fp_tal s' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf1451 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)1544 λge,s,s1,s'',EVAL,CALL,fp. 1545 match fp return λs''.λ_. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with 1546 [ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf 1547 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL) 1452 1548 rem rok 1453  fp_tac s' sf TAC rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf1454 (tac_step_call (RTLabs_status ge) s s' sfs1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC)1455 rem rok1549  fp_tac s'' s2 s3 tr TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 tr 1550 (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC) 1551 WCL2 EV rem rok 1456 1552 ]. 1457 1553 … … 1473 1569 (TRACE_OK: remainder_ok ge s trace) 1474 1570 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1571 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) 1572 (STATE_SOUNDLY_LABELLED: soundly_labelled_state s) 1475 1573 (LABEL_LIMIT: state_bound_on_steps_to_cost s n) 1476 1574 on n : finite_prefix ge s ≝ … … 1488 1586 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK' 1489 1587  false ⇒ λCS. 1490 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ? in1588 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in 1491 1589 fp_add_default ge ?? CL fs ? CS 1492 1590 ] (refl ??) … … 1502 1600 [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr) TRACE_OK' 1503 1601  false ⇒ λCS. 1504 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ? in1602 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in 1505 1603 fp_add_terminating_call … fs (new_trace … tlr) ? CS 1506 1604 ] (refl ??) 1507 1605 ] 1508 1606  or_intror NO_TERMINATION ⇒ 1509 fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace')?1607 fp_tac ????? (tac_base (RTLabs_status ge) start CL) ? EV trace' ? 1510 1608 ] 1511 1609  cl_return ⇒ λCL. ⊥ … … 1521 1619  5,6,8,9,10,11: /3/ 1522 1620  % [ @(well_cost_labelled_state_step … EV) /2/ 1621  @(soundly_labelled_state_step … EV) /2/ 1523 1622  @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/ 1524 1623  @(still_not_wrong … EV) /2/ … … 1526 1625 ] 1527 1626  /2/ 1627  @(soundly_labelled_state_preserved … (stack_ok … tlr)) 1628 @(soundly_labelled_state_step … EV) /2/ 1528 1629  @(bound_after_call ge … LABEL_LIMIT CL ? CS) 1529 1630 @(RTLabs_after_call … CL EV) @(stack_ok … tlr) 1530 1631  % [ /2/ 1632  @(soundly_labelled_state_preserved … (stack_ok … tlr)) 1633 @(soundly_labelled_state_step … EV) /2/ 1531 1634  @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % 1532 1635 @wr_call // … … 1557 1660  @(well_cost_labelled_state_step … EV) /2/ 1558 1661  @(well_cost_labelled_call … EV) /2/ 1559  % /2/ 1560  18,19,20: /2/ 1662  /2/ 1663  % [ @(well_cost_labelled_state_step … EV) /2/ 1664  @(soundly_labelled_state_step … EV) /2/ 1665  @(not_to_not … NO_TERMINATION) * #depth * #TM % 1666 @(will_return_lower … TM) // 1667  @(still_not_wrong … EV) /2/ 1668  @(not_return_to_not_final … EV) >CL % #E destruct 1669 ] 1670  20,21,22: /2/ 1671  @(soundly_labelled_state_step … EV) /2/ 1561 1672  cases (bound_after_step … LABEL_LIMIT EV ?) 1562 1673 [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 //  … … 1584 1695 ] 1585 1696  % [ @(well_cost_labelled_state_step … EV) /2/ 1697  @(soundly_labelled_state_step … EV) /2/ 1586 1698  @(not_to_not … (ro_no_termination … TRACE_OK)) 1587 1699 * #depth * #TERM %{depth} % @wr_step /2/ … … 1595 1707 ] qed. 1596 1708 1597 definition soundly_labelled_fn : internal_function → Prop ≝ 1598 λf. ∀l. present … (f_graph f) l → ∃n. bound_on_steps_to_cost1 (f_graph f) l n. 1599 1600 definition soundly_labelled_ge : genv → Prop ≝ 1601 λge. ∀b,f. find_funct_ptr ?? ge b = Some ? (Internal ? f) → soundly_labelled_fn f. 1602 1603 definition soundly_labelled_state : state → Prop ≝ 1604 λs. match s with 1605 [ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs 1606  Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn  External _ ⇒ True ] ∧ 1607 All ? (λf. soundly_labelled_fn (func f)) fs 1608  Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs 1609  Finalstate _ ⇒ True 1610 ]. 1611 1612 lemma steps_from_sound : ∀s. 1613 RTLabs_cost s = true → 1614 soundly_labelled_state s → 1615 ∃n. state_bound_on_steps_to_cost s n. 1616 * [ #f #fs #m #CS  #a #b #c #d #e #E normalize in E; destruct  #a #b #c #d #E normalize in E; destruct  #a #E normalize in E; destruct ] 1617 whd in ⊢ (% → ?); * #SLF #_ 1618 cases (SLF (next f) (next_ok f)) #n #B1 1619 %{n} % @B1 1620 qed. 1709 (* FIXME: 1710 1711 This isn't going to work in this form: the existential isn't the coinductive 1712 type, so this isn't technically a cofixpoint. Try to return just the 1713 structured trace won't either, because the termination oracle is in Prop. 1714 1715 Not sure how to get out of this situation... 1716 *) 1621 1717 1622 1718 let corec make_label_diverges ge s … … 1631 1727 match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with 1632 1728 [ ex_intro n B ⇒ 1633 match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED B1729 match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED STATE_SOUNDLY_LABELLED B 1634 1730 return λs.λ_. RTLabs_cost s = true → ∃T:trace_label_diverges (RTLabs_status ge) s. True 1635 1731 with … … 1639 1735 ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I 1640 1736 ] 1641  fp_tac s s' T t tOK ⇒ λSTATEMENT_COSTLABEL. 1642 match t return λs',t. trace_any_call ? s s' → remainder_ok ge s' t → ∃T:trace_label_diverges (RTLabs_status ge) s. True 1643 with 1644 [ ft_step s' tr next EV t' ⇒ λT,tOK. 1645 match make_label_diverges ge next t' ORACLE ? ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with 1646 [ ex_intro T' _ ⇒ 1647 ex_intro ?? (tld_base (RTLabs_status ge) s s' next (tlc_base … T STATEMENT_COSTLABEL) ?? T') ? 1648 ] 1649  _ ⇒ λT. ⊥ 1650 ] T tOK 1737  fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL. 1738 match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with 1739 [ ex_intro T' _ ⇒ 1740 ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ? 1741 ] 1651 1742 ] STATEMENT_COSTLABEL 1652 1743 ]. 1653 [ 1744 [ /2/ 1745  @(trace_any_label_label … T) 1746  @(trace_any_call_call … T) 1747  %{tr} @EV 1748  @I 1749  /2/ 1750  @(well_cost_labelled_call … EV) // @(trace_any_call_call … T) 1751 ] (* XXX fails, see above. *) qed.
Note: See TracChangeset
for help on using the changeset viewer.