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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1784 r1805 1403 1403 use the fact that the trace is soundly labelled to achieve this. *) 1404 1404 1405 record remainder_ok (ge:genv) (s:state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ { 1406 ro_well_cost_labelled: well_cost_labelled_state s; 1407 ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t)); 1408 ro_not_undefined: not_wrong … t; 1409 ro_not_final: RTLabs_is_final s = None ? 1410 }. 1411 1405 1412 inductive finite_prefix (ge:genv) : state → Prop ≝ 1406 1413  fp_tal : ∀s,s'. 1407 1414 trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' → 1408 flat_trace io_out io_in ge s' → 1415 ∀t:flat_trace io_out io_in ge s'. 1416 remainder_ok ge s' t → 1409 1417 finite_prefix ge s 1410 1418  fp_tac : ∀s,s'. 1411 1419 trace_any_call (RTLabs_status ge) s s' → 1412 flat_trace io_out io_in ge s' → 1420 ∀t:flat_trace io_out io_in ge s'. 1421 remainder_ok ge s' t → 1413 1422 finite_prefix ge s 1414 1423 . … … 1422 1431 λge,s,s',OTHER,fp. 1423 1432 match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with 1424 [ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf1433 [ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf 1425 1434 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST)) 1426 rem 1427  fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf1428 (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem 1435 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 1429 1438 ]. 1430 1439 … … 1439 1448 λge,s,s1,s',EVAL,CALL,fp. 1440 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 with 1441 [ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf1450 [ fp_tal s' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf 1442 1451 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL) 1443 rem 1444  fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf1452 rem rok 1453  fp_tac s' sf TAC rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf 1445 1454 (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC) 1446 rem 1455 rem rok 1447 1456 ]. 1448 1457 … … 1462 1471 let rec finite_segment ge s n trace 1463 1472 (ORACLE: termination_oracle) 1473 (TRACE_OK: remainder_ok ge s trace) 1464 1474 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1465 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *)1466 (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))1467 (NOT_UNDEFINED: not_wrong … trace)1468 1475 (LABEL_LIMIT: state_bound_on_steps_to_cost s n) 1469 (NOT_FINAL: RTLabs_is_final s = None ?)1470 1476 on n : finite_prefix ge s ≝ 1471 1477 match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with 1472 1478 [ O ⇒ λLABEL_LIMIT. ⊥ 1473 1479  S n' ⇒ 1474 match trace return λs,trace. not_wrong ??? s trace → well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → RTLabs_is_final s = None ?→ state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with1475 [ ft_stop st FINAL ⇒ λ NOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT. ⊥1476  ft_step start tr next EV trace' ⇒ λ NOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT.1480 match trace return λs,trace. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with 1481 [ ft_stop st FINAL ⇒ λTRACE_OK,LABEL_LIMIT. ⊥ 1482  ft_step start tr next EV trace' ⇒ λTRACE_OK,LABEL_LIMIT. 1477 1483 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with 1478 1484 [ cl_other ⇒ λCL. 1485 let TRACE_OK' ≝ ? in 1479 1486 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with 1480 1487 [ true ⇒ λCS. 1481 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' 1488 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK' 1482 1489  false ⇒ λCS. 1483 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ????? in1490 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ? in 1484 1491 fp_add_default ge ?? CL fs ? CS 1485 1492 ] (refl ??) 1486 1493  cl_jump ⇒ λCL. 1487 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' 1494 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' ? 1488 1495  cl_call ⇒ λCL. 1489 1496 match ORACLE ge O next trace' return λ_. finite_prefix ge start with … … 1491 1498 match TERMINATES with [ witness TERMINATES ⇒ 1492 1499 let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in 1500 let TRACE_OK' ≝ ? in 1493 1501 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with 1494 [ 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) 1502 [ 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' 1495 1503  false ⇒ λCS. 1496 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ????? in1504 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ? in 1497 1505 fp_add_terminating_call … fs (new_trace … tlr) ? CS 1498 1506 ] (refl ??) 1499 1507 ] 1500 1508  or_intror NO_TERMINATION ⇒ 1501 fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') 1509 fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') ? 1502 1510 ] 1503 1511  cl_return ⇒ λCL. ⊥ 1504 1512 ] (refl ??) 1505  ft_wrong start m EV ⇒ λ NOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT. ⊥1506 ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION NOT_FINAL1513  ft_wrong start m EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥ 1514 ] TRACE_OK 1507 1515 ] LABEL_LIMIT. 1508 1516 [ cases (state_bound_on_steps_to_cost_zero s) /2/ 1509  @(absurd … NOT_FINALFINAL)1510  @(absurd ?? NO_TERMINATION)1517  @(absurd … (ro_not_final … TRACE_OK) FINAL) 1518  @(absurd ?? (ro_no_termination … TRACE_OK)) 1511 1519 %{0} % @wr_base // 1512  @(well_cost_labelled_jump … EV) // 1513  5,6,7,8,9,10: /2/ 1520  @(well_cost_labelled_jump … EV) /2/ 1521  5,6,8,9,10,11: /3/ 1522  % [ @(well_cost_labelled_state_step … EV) /2/ 1523  @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/ 1524  @(still_not_wrong … EV) /2/ 1525  @(not_return_to_not_final … EV) >CL % #E destruct 1526 ] 1514 1527  /2/ 1515  //1516  @(not_to_not … NO_TERMINATION) * #depth * #TM1 %{depth} %1517 @wr_call //1518 @(will_return_prepend … TERMINATES … TM1)1519 cases (terminates … tlr) //1520  @(will_return_not_wrong … TERMINATES)1521 [ @(still_not_wrong … EV) //1522  cases (terminates … tlr) //1523 ]1524 1528  @(bound_after_call ge … LABEL_LIMIT CL ? CS) 1525 1529 @(RTLabs_after_call … CL EV) @(stack_ok … tlr) 1526  (* By stack preservation we cannot be in the final state *) 1527 inversion (stack_ok … tlr) 1528 [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct 1529  #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 TERMINATES destruct @refl 1530  #s1 #r #S #E1 #E2 #E3 #E4 TERMINATES destruct 1531 cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct 1532 inversion (eval_perserves … EV) 1533 [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 NOT_UNDEFINED NO_TERMINATION destruct ] 1534 #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 NOT_UNDEFINED NO_TERMINATION destruct 1535 inversion S 1536 [ #f #fs0 #m #E1 #E2 #E3 destruct  *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ] 1537 (* state_bound_on_steps_to_cost needs to know about the current stack frame, 1538 so we can use it as a witness that at least one frame exists *) 1539 inversion LABEL_LIMIT 1540 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct 1541  #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct 1542 ] 1543  @(well_cost_labelled_state_step … EV) // 1544  @(well_cost_labelled_call … EV) // 1545  19,20,21: /2/ 1546  @(well_cost_labelled_state_step … EV) // 1547  @(not_to_not … NO_TERMINATION) 1548 * #depth * #TERM %{depth} % @wr_step /2/ 1549  @(still_not_wrong … NOT_UNDEFINED) 1530  % [ /2/ 1531  @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % 1532 @wr_call // 1533 @(will_return_prepend … TERMINATES … TM1) 1534 cases (terminates … tlr) // 1535  @(will_return_not_wrong … TERMINATES) 1536 [ @(still_not_wrong … EV) /2/ 1537  cases (terminates … tlr) // 1538 ] 1539  (* By stack preservation we cannot be in the final state *) 1540 inversion (stack_ok … tlr) 1541 [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct 1542  #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 TERMINATES destruct @refl 1543  #s1 #r #S #E1 #E2 #E3 #E4 TERMINATES destruct 1544 cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct 1545 inversion (eval_perserves … EV) 1546 [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 TRACE_OK destruct ] 1547 #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 TRACE_OK destruct 1548 inversion S 1549 [ #f #fs0 #m #E1 #E2 #E3 destruct  *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ] 1550 (* state_bound_on_steps_to_cost needs to know about the current stack frame, 1551 so we can use it as a witness that at least one frame exists *) 1552 inversion LABEL_LIMIT 1553 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct 1554  #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct 1555 ] 1556 ] 1557  @(well_cost_labelled_state_step … EV) /2/ 1558  @(well_cost_labelled_call … EV) /2/ 1559  % /2/ 1560  18,19,20: /2/ 1550 1561  cases (bound_after_step … LABEL_LIMIT EV ?) 1551 [ * [ #TERMINATES @⊥ @(absurd ?? NO_TERMINATION) %{0} % @wr_step [ %1 // 1562 [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 //  1552 1563 inversion trace' 1553 [ #s0 #FINAL #E1 #E2 destruct @⊥1564 [ #s0 #FINAL #E1 #E2 TRACE_OK' destruct @⊥ 1554 1565 @(absurd ?? FINAL) @(not_return_to_not_final … EV) 1555 1566 % >CL #E destruct 1556  #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct1567  #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 TRACE_OK' destruct 1557 1568 @wr_base // 1558  #H99 #H100 #H101 #H102 #H103 destruct1559 inversion NOT_UNDEFINED1569  #H99 #H100 #H101 #H102 #H103 TRACE_OK' destruct 1570 inversion (ro_not_undefined … TRACE_OK) 1560 1571 [ #H137 #H138 #H139 #H140 #H141 destruct 1561 1572  #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct … … 1572 1583  // 1573 1584 ] 1574  @(not_return_to_not_final … EV) >CL % #E destruct 1575  inversion NOT_UNDEFINED 1585  % [ @(well_cost_labelled_state_step … EV) /2/ 1586  @(not_to_not … (ro_no_termination … TRACE_OK)) 1587 * #depth * #TERM %{depth} % @wr_step /2/ 1588  @(still_not_wrong … (ro_not_undefined … TRACE_OK)) 1589  @(not_return_to_not_final … EV) >CL % #E destruct 1590 ] 1591  inversion (ro_not_undefined … TRACE_OK) 1576 1592 [ #H169 #H170 #H171 #H172 #H173 destruct 1577 1593  #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct … … 1607 1623 (trace: flat_trace io_out io_in ge s) 1608 1624 (ORACLE: termination_oracle) 1625 (TRACE_OK: remainder_ok ge s trace) 1609 1626 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1610 1627 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) 1611 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *)1612 1628 (STATE_SOUNDLY_LABELLED: soundly_labelled_state s) 1613 1629 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 1614 (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace)))1615 (NOT_UNDEFINED: not_wrong … trace)1616 (NOT_FINAL: RTLabs_is_final s = None ?)1617 1630 : ∃T:trace_label_diverges (RTLabs_status ge) s. True ≝ 1618 1631 match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with 1619 1632 [ ex_intro n B ⇒ 1620 match finite_segment ge s n trace ORACLE ENV_COSTLABELLED STATE_COSTLABELLED NO_TERMINATION NOT_UNDEFINED B NOT_FINAL1633 match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED B 1621 1634 return λs.λ_. RTLabs_cost s = true → ∃T:trace_label_diverges (RTLabs_status ge) s. True 1622 1635 with 1623 [ fp_tal s s' T t ⇒ λSTATEMENT_COSTLABEL.1624 match make_label_diverges ge s' t ORACLE ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?????? with1636 [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL. 1637 match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with 1625 1638 [ ex_intro T' _ ⇒ 1626 1639 ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I 1627 1640 ] 1628  fp_tac s s' T t ⇒ λSTATEMENT_COSTLABEL.1629 match t return λs',t. trace_any_call ? s s' → ∃T:trace_label_diverges (RTLabs_status ge) s. True1641  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 1630 1643 with 1631 [ ft_step s' tr next EV t' ⇒ λT .1632 match make_label_diverges ge next t' ORACLE ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?????? with1644 [ ft_step s' tr next EV t' ⇒ λT,tOK. 1645 match make_label_diverges ge next t' ORACLE ? ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with 1633 1646 [ ex_intro T' _ ⇒ 1634 1647 ex_intro ?? (tld_base (RTLabs_status ge) s s' next (tlc_base … T STATEMENT_COSTLABEL) ?? T') ? 1635 1648 ] 1636 1649  _ ⇒ λT. ⊥ 1637 ] T 1650 ] T tOK 1638 1651 ] STATEMENT_COSTLABEL 1639 1652 ]. 1653 [
Note: See TracChangeset
for help on using the changeset viewer.