 Timestamp:
 Feb 27, 2012, 2:16:54 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1764 r1765 1447 1447 ]. 1448 1448 1449 lemma not_return_to_not_final : ∀ge,s,tr,s'. 1450 eval_statement ge s = Value ??? 〈tr, s'〉 → 1451 RTLabs_classify s ≠ cl_return → 1452 RTLabs_is_final s' = None ?. 1453 #ge #s #tr #s' #EV 1454 inversion (eval_perserves … EV) // 1455 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL 1456 @⊥ @(absurd ?? CL) @refl 1457 qed. 1458 1449 1459 definition termination_oracle ≝ ∀ge,depth,s,trace. 1450 1460 inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace). … … 1457 1467 (NOT_UNDEFINED: not_wrong … trace) 1458 1468 (LABEL_LIMIT: state_bound_on_steps_to_cost s n) 1469 (NOT_FINAL: RTLabs_is_final s = None ?) 1459 1470 on n : finite_prefix ge s ≝ 1460 1471 match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with 1461 1472 [ O ⇒ λLABEL_LIMIT. ⊥ 1462 1473  S n' ⇒ 1463 match trace return λs,trace. not_wrong ??? s trace → well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with1464 [ ft_stop st FINAL ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION, LABEL_LIMIT. ⊥1465  ft_step start tr next EV trace' ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION, LABEL_LIMIT.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 with 1475 [ 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. 1466 1477 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with 1467 1478 [ cl_other ⇒ λCL. … … 1470 1481 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' 1471 1482  false ⇒ λCS. 1472 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ???? in1483 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ????? in 1473 1484 fp_add_default ge ?? CL fs ? CS 1474 1485 ] (refl ??) … … 1483 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) 1484 1495  false ⇒ λCS. 1485 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ???? in1496 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ????? in 1486 1497 fp_add_terminating_call … fs (new_trace … tlr) ? CS 1487 1498 ] (refl ??) … … 1492 1503  cl_return ⇒ λCL. ⊥ 1493 1504 ] (refl ??) 1494  ft_wrong start m EV ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION, LABEL_LIMIT. ⊥1495 ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION 1505  ft_wrong start m EV ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,NOT_FINAL,LABEL_LIMIT. ⊥ 1506 ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION NOT_FINAL 1496 1507 ] LABEL_LIMIT. 1497 1508 [ cases (state_bound_on_steps_to_cost_zero s) /2/ 1498  (* TODO: how do we know that we're not at the final state? *)1509  @(absurd … NOT_FINAL FINAL) 1499 1510  @(absurd ?? NO_TERMINATION) 1500 1511 %{0} % @wr_base // … … 1513 1524  @(bound_after_call ge … LABEL_LIMIT CL ? CS) 1514 1525 @(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 #H130 #H131 #H133 #H134 #H135 #H136 #H137 #H138 #H139 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 ] 1515 1543  @(well_cost_labelled_state_step … EV) // 1516 1544  @(well_cost_labelled_call … EV) // 1517  1 8,19,20: /2/1545  19,20,21: /2/ 1518 1546  @(well_cost_labelled_state_step … EV) // 1519 1547  @(not_to_not … NO_TERMINATION) … … 1523 1551 [ * [ #TERMINATES @⊥ @(absurd ?? NO_TERMINATION) %{0} % @wr_step [ %1 //  1524 1552 inversion trace' 1525 [ cases daemon (* TODO again *)  #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct 1526 @wr_base // 1553 [ #s0 #FINAL #E1 #E2 destruct @⊥ 1554 @(absurd ?? FINAL) @(not_return_to_not_final … EV) 1555 % >CL #E destruct 1556  #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct 1557 @wr_base // 1527 1558  #H99 #H100 #H101 #H102 #H103 destruct 1528 1559 inversion NOT_UNDEFINED … … 1541 1572  // 1542 1573 ] 1574  @(not_return_to_not_final … EV) >CL % #E destruct 1543 1575  inversion NOT_UNDEFINED 1544 1576 [ #H169 #H170 #H171 #H172 #H173 destruct 1545 1577  #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct 1546 1578 ] 1547 ] cases daemonqed.1579 ] qed. 1548 1580 1549 1581 (*
Note: See TracChangeset
for help on using the changeset viewer.