Changeset 2571 for src/RTLabs
 Timestamp:
 Jan 8, 2013, 5:46:04 PM (7 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2499 r2571 726 726 qed. 727 727 728 definition lift_classify : ∀s,c. RTLabs_classify s = c → Some ? (RTLabs_classify s) = Some ? c ≝ λs,c,E. eq_f … E. 729 728 730 lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge. 729 731 ∀CL : RTLabs_classify s1 = cl_call. 730 732 as_execute (RTLabs_status ge) s1 s2 → 731 733 stack_preserved ge ends_with_ret s2 s3 → 732 as_after_return (RTLabs_status ge) «s1, CL» s3.734 as_after_return (RTLabs_status ge) «s1,lift_classify … CL» s3. 733 735 #ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23 734 736 cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct … … 838 840 (* Small syntax hack to avoid ambiguous input problems. *) 839 841 definition myge : nat → nat → Prop ≝ ge. 842 843 (* RTLabs_classify isn't exactly as_classifier *) 844 definition lift_cl ≝ eq_f ?? (Some status_class). 840 845 841 846 let rec make_label_return ge depth (s:RTLabs_ext_state ge) … … 958 963 959 964  cl_call ⇒ λCL. 960 let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … CLTERMINATES) TIME ? in965 let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in 961 966 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start' ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 962 967 (* We're about to run into a label, use base case for call *) … … 966 971 (mk_trace_result ge … 967 972 (tal_base_call (RTLabs_status ge) start' next' (new_state … r) 968 ? CL? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)973 ? (lift_cl … CL) ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??) 969 974 (* otherwise use step case *) 970 975  false ⇒ λCS. … … 974 979 replace_sub_trace … r' ? 975 980 (tal_step_call (RTLabs_status ge) (ends … r') 976 start' next' (new_state … r) (new_state … r') ? CL?981 start' next' (new_state … r) (new_state … r') ? (lift_cl … CL) ? 977 982 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ? 978 983 ] (refl ??) … … 981 986 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ? 982 987 ends_with_ret 983 (mk_trace_result ge …988 (mk_trace_result ge ??????? 984 989 next' 985 990 trace' 986 991 ? 987 (tal_base_return (RTLabs_status ge) start' next' ? CL)992 (tal_base_return (RTLabs_status ge) start' next' ? (lift_cl … CL)) 988 993 ? 989 994 ?) 995  cl_tailcall ⇒ λCL. ⊥ 990 996 ] (refl ? (RTLabs_classify start)) 991 997 … … 1029 1035  @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) 1030 1036  %{tr} %{EV} % 1031  %1 whd @ CL1037  %1 whd @(lift_cl … CL) 1032 1038  @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) // 1033 1039  @(well_cost_labelled_state_step … EV) // … … 1062 1068  @(well_cost_labelled_state_step … EV) // 1063 1069  @(well_cost_labelled_call … EV) // 1070  skip 1064 1071  cases (will_return_call … TERMINATES) 1065 1072 #TM * #GT #_ @le_S_S_to_le … … 1067 1074 @(transitive_le … TERMINATES_IN_TIME) 1068 1075 @(monotonic_le_times_r 3 … GT) 1076  @(RTLabs_notail … CL) 1069 1077  whd @(will_return_notfn … TERMINATES) %1 @CL 1070 1078  @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) 1071 1079  %{tr} %{EV} % 1072  %2 whd @ CL1080  %2 whd @(lift_cl … CL) 1073 1081  @(well_cost_labelled_state_step … EV) // 1074 1082  cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT) 1075 1083  cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ 1076  @ CL1084  @(lift_cl … CL) 1077 1085  %{tr} %{EV} % 1078 1086  @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) … … 1265 1273 state_bound_on_steps_to_cost s (S n) → 1266 1274 ∀CL:RTLabs_classify s = cl_call. 1267 as_after_return (RTLabs_status ge) «s, CL» s' →1275 as_after_return (RTLabs_status ge) «s, lift_cl … CL» s' → 1268 1276 RTLabs_cost s' = false → 1269 1277 state_bound_on_steps_to_cost s' n. … … 1452 1460 match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with 1453 1461 [ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf 1454 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER(RTLabs_not_cost … NOT_COST))1462 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST)) 1455 1463 rem rok 1456 1464  fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 1457 (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER(RTLabs_not_cost … NOT_COST))1465 (tac_step_default (RTLabs_status ge) ??? EVAL TAC (lift_cl … OTHER) (RTLabs_not_cost … NOT_COST)) 1458 1466 WCL2 EV rem rok 1459 1467 ]. … … 1464 1472 finite_prefix ge s'' → 1465 1473 trace_label_return (RTLabs_status ge) s1 s'' → 1466 as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL)s'' →1474 as_after_return (RTLabs_status ge) «s, lift_cl … CALL» s'' → 1467 1475 RTLabs_cost s'' = false → 1468 1476 finite_prefix ge s ≝ … … 1470 1478 match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with 1471 1479 [ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf 1472 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALLRET TLR (RTLabs_not_cost … NOT_COST) TAL)1480 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAL) 1473 1481 rem rok 1474 1482  fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 1475 (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALLRET TLR (RTLabs_not_cost … NOT_COST) TAC)1483 (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (lift_cl … CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC) 1476 1484 WCL2 EV rem rok 1477 1485 ]. … … 1525 1533 let TRACE_OK' ≝ ? in 1526 1534 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with 1527 [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? CL? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK'1535 [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? (lift_cl … CL) ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK' 1528 1536  false ⇒ λCS. 1529 1537 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in … … 1532 1540 ] 1533 1541  or_intror NO_TERMINATION ⇒ 1534 fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' CL) ?? trace' ?1542 fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (lift_cl … CL))) ?? trace' ? 1535 1543 ] 1536 1544  cl_return ⇒ λCL. ⊥ 1545  cl_tailcall ⇒ λCL. ⊥ 1537 1546 ] (refl ??) 1538 1547 ] mtc0 … … 1544 1553 %{0} % @wr_base // 1545 1554  @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK)  // ] 1546  %1 @ CL1555  %1 @(lift_cl … CL) 1547 1556  6,9,10,11: /3/ 1548 1557  cases TRACE_OK #H1 #H2 #H3 #H4 … … 1592 1601  @(not_return_to_not_final … EV) >CL % #E destruct 1593 1602 ] 1594  %2 @CL 1603  @(RTLabs_notail … CL) 1604  %2 @(lift_cl … CL) 1595 1605  21,22: %{tr} %{EV} % 1596 1606  cases (bound_after_step … LABEL_LIMIT EV ?) … … 1609 1619  // 1610 1620 ] 1621  cases (bound_after_step … LABEL_LIMIT EV ?) 1622 [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 //  1623 inversion trace' 1624 [ #s0 #FINAL #E1 #E2 TRACE_OK' destruct @⊥ 1625 @(absurd ?? FINAL) @(not_return_to_not_final … EV) 1626 % >CL #E destruct 1627  #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 TRACE_OK' destruct 1628 @wr_base // 1629 ] 1630 ] 1631  >CL #E destruct 1632 ] 1633  // 1634  // 1635 ] 1611 1636  cases TRACE_OK #H1 #H2 #H3 #H4 1612 1637 % [ @(well_cost_labelled_state_step … EV) // … … 1617 1642 ] 1618 1643 ] qed. 1644 1645 lemma simplify_cl : ∀ge,s,c. 1646 as_classifier (RTLabs_status ge) s c → 1647 RTLabs_classify (Ras_state … s) = c. 1648 #ge * #s #S #M #c #CL 1649 whd in CL; whd in CL:(??%?); 1650 destruct // 1651 qed. 1619 1652 1620 1653 (* NB: This isn't quite what I'd like. Ideally, we'd show the existence of … … 1657 1690 [ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T) 1658 1691  @EV 1659  @(trace_any_call_call … T) 1660  cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') // @(trace_any_call_call … T) 1692  cases (trace_any_call_call … T) // #CL cases (RTLabs_notail' … CL) 1693  cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') // 1694 cases (trace_any_call_call … T) #CL 1695 [ @simplify_cl @CL 1696  @⊥ @(RTLabs_notail' … CL) 1697 ] 1661 1698 ] qed. 1662 1699 … … 1721 1758 [ witness TERMINATES ⇒ 1722 1759 let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in 1723 twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) IS_CALL? (new_trace … tlr) ?1760 twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) (lift_cl … IS_CALL) ? (new_trace … tlr) ? 1724 1761 ] 1725 1762  or_intror NO_TERMINATION ⇒ 1726 twp_diverges (RTLabs_status ge) s' next' IS_CALL?1763 twp_diverges (RTLabs_status ge) s' next' (lift_cl … IS_CALL) ? 1727 1764 (make_label_diverges ge next' trace' ORACLE ? 1728 1765 ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?) … … 1921 1958 pft_step … EX' (flat_trace_of_any_label ge ??? tal) 1922 1959 ] 1960  tal_base_tailcall s1 s2 s3 EX CL tlr ⇒ ⊥ 1923 1961 ]. 1924 1962 @(RTLabs_notail' … CL) 1963 qed. 1925 1964 1926 1965 (* We take an extra step so that we can always return a nonempty trace to … … 2076 2115  cl_other ⇒ ∀fn,l. P (rapc_state fn l) 2077 2116  cl_jump ⇒ ∀fn,l. P (rapc_state fn l) 2117  cl_tailcall ⇒ True 2078 2118 ] → P (as_pc_of (RTLabs_status ge) s). 2079 2119 #ge #cl #P * * … … 2086 2126 ] qed. 2087 2127 2128 definition declassify_pc_cl ≝ λge,cl,P,s,s',EX,CL. declassify_pc ge cl P s s' EX (simplify_cl … CL). 2129 2088 2130 lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge. 2089 2131 as_execute (RTLabs_status ge) s s' → … … 2094 2136  cl_other ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l 2095 2137  cl_jump ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l 2138  cl_tailcall ⇒ False 2096 2139 ] . 2097 2140 #ge * #s #s' #EX #CL whd 2098 2141 @(declassify_pc … EX CL) whd 2099 [ #fn %{fn} %  #fn #l %{fn} %{l} %  #caller #callee %{caller} %{callee} %  #fn #l %{fn} %{l} % ]2142 [ #fn %{fn} %  #fn #l %{fn} %{l} %  #caller #callee %{caller} %{callee} %  @I  #fn #l %{fn} %{l} % ] 2100 2143 qed. 2101 2144 … … 2140 2183  #s1 #s2 * #tr * #EX #NX #CL 2141 2184  #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS 2185  #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL) 2142 2186  #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal 2143 2187  #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS … … 2158 2202  #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥ 2159 2203 whd in CL CL'; >CL in CL'; #E destruct 2204  #s1 #s2 #s3 #EX #CL' @⊥ @(RTLabs_notail' … CL') 2160 2205  #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct 2161 2206 whd in CL CL'; >CL in CL'; #E destruct … … 2231 2276 #ge #pre #post #CL #ret #callee #AF 2232 2277 cases pre in CL AF ⊢ %; 2233 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); 2278 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); whd in CL:(??(??%)?); 2234 2279 cases (next_instruction f) in CL; 2235 2280 normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct … … 2288 2333 #l1 #PC1 #G #NCS #IN lapply (memb_single … IN) #E destruct 2289 2334 >(pc_label_eq … PC0 PC1) %1 2335  #s1 #s2 #s3 #EX #CL #tlr #l1 #PC1 #G #NCS #IN @⊥ @(RTLabs_notail' … CL) 2290 2336  #fl #pre #start #after #final #EX #CL #AF #tlr #CS #tal' 2291 2337 #l1 #PC1 #G #NCS whd in ⊢ (?% → ?); @eqb_elim 2292 2338 [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1 2293 2339  #NE #IN 2294 lapply (declassify_pc' … EX CL) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC12340 lapply (declassify_pc' … EX (simplify_cl … CL)) * * [2: #ret ] * #fn2 #PC >PC in PC1; #PC1 2295 2341 [ cases (pc_after_return' … AF PC) #SF #PC' >SF in G; #G 2296 2342 lapply (pc_label_call_eq … PC1) #E destruct … … 2303 2349 [ #E destruct >(pc_label_eq … PC0 PC1) #_ %1 2304 2350  #NE #IN 2305 cases (declassify_state … EX CL)2351 cases (declassify_state … EX (simplify_cl … CL)) 2306 2352 #f * #fs * #m * #S * #M #E destruct 2307 2353 cut (l1 = next f) … … 2310 2356 cases EX #tr * #EV #NX 2311 2357 cases (eval_successor … EV) 2312 [ * #CL' @⊥ cases (tal_return … CL'tal') #EX' * #CL'' * #E1 #E2 destruct2313 lapply (memb_single … IN) @(declassify_pc … EX' CL'') whd2358 [ * #CL' @⊥ cases (tal_return … (lift_cl … CL') tal') #EX' * #CL'' * #E1 #E2 destruct 2359 lapply (memb_single … IN) @(declassify_pc_cl … EX' CL'') whd 2314 2360 #fn #E destruct inversion PC0 #a #b #E1 #E2 #E3 destruct 2315 2361  * #l' * #AS #SC … … 2344 2390 cases (eval_successor … EV) 2345 2391 [ * #CL2 #SC 2346 cases (tal_return … CL2tal) #EX2 * #CL2' * #E1 #E2 destruct2392 cases (tal_return … (lift_cl … CL2) tal) #EX2 * #CL2' * #E1 #E2 destruct 2347 2393 @notb_Prop % whd in match (tal_pc_list ?????); #IN 2348 2394 lapply (memb_single … IN) cases (declassify_state … EX2 CL2) … … 2389 2435 as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4. 2390 2436 #ge * #s1 #S1 #M1 #CL1 2391 cases (rtlabs_call_inv … CL1) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct2437 cases (rtlabs_call_inv … (simplify_cl … CL1)) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct 2392 2438 * #s2 #S2 #M2 #CL2 2393 cases (rtlabs_call_inv … CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct2439 cases (rtlabs_call_inv … (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct 2394 2440 * * [ #f3 #fs3 #m3 #S3 #M3  #a #b #c #d #e #f #g #h *  #a #b #c #d #e #f #g *  #r3 #S3 #M3 ] 2395 2441 * * [ 1,5: #f4 #fs4 #m4 #S4 #M4  2,6: #a #b #c #d #e #f #g #h *  3,7: #a #b #c #d #e #f #g *  4,8: #r4 #S4 #M4 ] … … 2467 2513 #ge #flX #s1X #s2X * 2468 2514 [ #s1 #s2 #EX * 2469 [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥ change with ( RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL in CL'; #CL'destruct2515 [ whd in ⊢ (% → ?); #CL #CS #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct 2470 2516  #CL #CS #CL' @eq_true_to_b @memb_hd 2471 2517 ] 2472  #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = ?) in CL; >CL in CL'; #CL' destruct 2473  #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = cl_call) in CL; >CL in CL'; #CL' destruct 2474  #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (RTLabs_classify (Ras_state ? s1) = cl_call) in CL; >CL in CL'; #CL' destruct 2518  #s1 #s2 #EX #CL whd in CL; #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct 2519  #s1 #s2 #s3 #EX #CL #AF #tlr #CS #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct 2520  #s1 #s2 #s3 #EX #CL @⊥ @(RTLabs_notail' … CL) 2521  #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal #CL' @⊥ change with (Some ? (RTLabs_classify (Ras_state ? s1)) = ?) in CL; >CL' in CL; #CL destruct 2475 2522  #fl #s1 #s2 #s3 #EX #tal #CL #CS #CL' @eq_true_to_b @memb_hd 2476 2523 ] qed. … … 2480 2527 state_fn … pre = state_fn … post. 2481 2528 #ge * #pre #preS #preM * #post #postS #postM #CL #AF 2482 cases (rtlabs_call_inv … CL) #fd * #args * #dst * #fs * #m #E destruct2529 cases (rtlabs_call_inv … (simplify_cl … CL)) #fd * #args * #dst * #fs * #m #E destruct 2483 2530 cases post in postM AF ⊢ %; 2484 2531 [ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF … … 2528 2575 [ #s3 #s4 #EX3 #CL3 #CS4 #FN #IN @⊥ 2529 2576 whd in match (tal_pc_list ?????) in IN; 2530 lapply (memb_single … IN) @(declassify_pc … EX1 CL1) #caller #callee2531 cases CL3 #CL3' @(declassify_pc … EX3 CL3') #fn #l2577 lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee 2578 cases CL3 #CL3' @(declassify_pc_cl … EX3 CL3') #fn #l 2532 2579 #IN' destruct 2533 2580  #s2 #s4 #EX2 #CL2 #FN #IN @⊥ 2534 lapply (memb_single … IN) @(declassify_pc … EX1 CL1) #caller #callee2535 @(declassify_pc … EX2 CL2) whd #fn2581 lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL1) #caller #callee 2582 @(declassify_pc_cl … EX2 CL2) whd #fn 2536 2583 #IN' destruct 2537 2584  #s3 #s3' #s4 #EX3 #CL3 #AF3 #tlr3 #CS4 #FN #IN … … 2539 2586 lapply (pc_after_return_eq … AF1 AF3 E FN) #PC 2540 2587 @⊥ @(absurd ?? CS2) @(eq_pc_cost … CS4) // 2588  #s1 #s2 #s3 #EX #CL #tlr #S1 #IN @⊥ @(RTLabs_notail' … CL) 2541 2589  #fl' #s3 #s3' #s3'' #s4 #EX3 #CL3 #AF3 #tlr3' #CS3'' #tal3'' #FN 2542 2590 whd in ⊢ (?% → ?); @eqb_elim … … 2549 2597 ] 2550 2598  #fl' #s3 #s3' #s4 #EX3 #tal3' #CL3 #CS3' #FN #IN 2551 change with (RTLabs_classify ? = ?) in CL1;2552 change with (RTLabs_classify ? = ?) in CL3;2599 lapply (simplify_cl … CL1) #CL1' 2600 lapply (simplify_cl … CL3) #CL3' 2553 2601 @eq_true_to_b @memb_cons 2554 2602 @(pc_after_call_repeats_aux ge … AF1 CL2 CS2 EX1) 2555 [ >FN cases (state_fn_other … CL3 EX3)2556 [ #CL3' @⊥2557 cases (tal_return … CL3'tal3')2558 #EX3' * #CL3'' * #E1 #E2 destruct2603 [ >FN cases (state_fn_other … CL3' EX3) 2604 [ #CL3'' @⊥ 2605 cases (tal_return … (lift_cl … CL3'') tal3') 2606 #EX3' * #CL3''' * #E1 #E2 destruct 2559 2607 whd in IN:(?%); lapply IN @eqb_elim 2560 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1 >CL3#E destruct2561  #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1 >CL3' #E destruct2608 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct 2609  #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL1' >CL3'' #E destruct 2562 2610 ] 2563 2611  // 2564 2612 ] 2565 2613  lapply IN whd in ⊢ (?% → ?); @eqb_elim 2566 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1 >CL3#E destruct2614 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL1' >CL3' #E destruct 2567 2615  #NE #IN @IN 2568 2616 ] … … 2583 2631 [ #s2 #s4 #EX2 #CL2 #CS #EX1 #AF #CS2 #IN @⊥ 2584 2632 whd in match (tal_pc_list ?????) in IN; 2585 lapply (memb_single … IN) @(declassify_pc … EX1 CL) #caller #callee2586 cases CL2 #CL2' @(declassify_pc … EX2 CL2') #fn #l2633 lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee 2634 cases CL2 #CL2' @(declassify_pc_cl … EX2 CL2') #fn #l 2587 2635 #IN' destruct 2588 2636  #s2 #s4 #EX2 #CL2 #EX1 #AF #CS2 #IN @⊥ 2589 lapply (memb_single … IN) @(declassify_pc … EX1 CL) #caller #callee2590 @(declassify_pc … EX2 CL2) whd #fn2637 lapply (memb_single … IN) @(declassify_pc_cl … EX1 CL) #caller #callee 2638 @(declassify_pc_cl … EX2 CL2) whd #fn 2591 2639 #IN' destruct 2592 2640  #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥ 2593 cases (declassify_state … EX1 CL) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct2594 cases (declassify_state … EX2 CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct2641 cases (declassify_state … EX1 (simplify_cl … CL)) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct 2642 cases (declassify_state … EX2 (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct 2595 2643 cases AF1 2644  #s1 #s2 #s3 #EX #CL #tlr @⊥ @(RTLabs_notail' … CL) 2596 2645  #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥ 2597 cases (declassify_state … EX1 CL) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct2598 cases (declassify_state … EX2 CL2) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct2646 cases (declassify_state … EX1 (simplify_cl … CL)) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct 2647 cases (declassify_state … EX2 (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct 2599 2648 cases AF1 2600 2649  #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN 2601 change with (RTLabs_classify ? = ?) in CL;2602 change with (RTLabs_classify ? = ?) in CL2;2650 lapply (simplify_cl … CL) #CL' 2651 lapply (simplify_cl … CL2) #CL2' 2603 2652 %{s3} %{EX2} %{CL2} %{CS3} %{tal3} % [ % ] 2604 2653 (* Now that we've inverted the first part of the trace, look for the repeat. *) 2605 @(pc_after_call_repeats_aux … CL … AF1 CL2 CS2 EX1)2654 @(pc_after_call_repeats_aux … CL … AF1 CL2' CS2 EX1) 2606 2655 [ >(state_fn_after_return … AF1) 2607 cases (state_fn_other … CL2 EX2)2656 cases (state_fn_other … CL2' EX2) 2608 2657 [ #CL3 @⊥ 2609 cases (tal_return … CL3tal3)2658 cases (tal_return … (lift_cl … CL3) tal3) 2610 2659 #EX3 * #CL3' * #E1 #E2 destruct 2611 change with (RTLabs_classify ? = ?) in CL3';2660 lapply (simplify_cl … CL3') #CL3'' 2612 2661 whd in IN:(?%); lapply IN @eqb_elim 2613 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2#E destruct2614  #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL >CL3' #E destruct2662 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct 2663  #NE #IN lapply (memb_single … IN) #PC lapply (eq_pc_eq_classify … PC) >CL' >CL3'' #E destruct 2615 2664 ] 2616 2665  // 2617 2666 ] 2618 2667  lapply IN whd in ⊢ (?% → ?); @eqb_elim 2619 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL >CL2#E destruct2668 [ #PC #_ lapply (eq_pc_eq_classify … PC) >CL' >CL2' #E destruct 2620 2669  #NE #IN @IN 2621 2670 ] … … 2637 2686 @(absurd ? IN') 2638 2687 @Prop_notb 2639 @no_loops_in_tal assumption2688 @no_loops_in_tal /2/ 2640 2689 qed. 2641 2690 … … 2676 2725  tal_base_return _ _ EX _ ⇒ λS1. soundly_step … GE EX S1 2677 2726  tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. tlr_sound … tlr GE (soundly_step … GE EX S1) 2727  tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥ 2678 2728  tal_step_call _ _ _ _ _ EX _ _ tlr _ tal ⇒ λS1. tal_sound … tal GE (tlr_sound … tlr GE (soundly_step … GE EX S1)) 2679 2729  tal_step_default _ _ _ _ EX tal _ _ ⇒ λS1. tal_sound … tal GE (soundly_step … GE EX S1) 2680 2730 ]. 2731 @(RTLabs_notail' … CL) 2732 qed. 2681 2733 2682 2734 (* And join everything up to show that soundly labelled states give unrepeating … … 2710 2762  tal_base_call _ _ _ EX _ _ tlr _ ⇒ λS1. 2711 2763 tlr_sound_unrepeating … GE tlr (soundly_step … GE EX S1) 2764  tal_base_tailcall _ _ _ _ CL _ ⇒ ⊥ 2712 2765  tal_step_call _ pre start after final EX CL AF tlr _ tal ⇒ λS1. 2713 2766 conj ?? (conj ??? … … 2717 2770 conj ??? (tal_sound_unrepeating … GE tal (soundly_step … GE EX S1)) 2718 2771 ]. 2719 [ @(no_repeats_of_calls … EX AF) [ assumption  2772 [ @(RTLabs_notail' … CL) 2773  @(no_repeats_of_calls … EX AF) [ assumption  2720 2774 @(tlr_sound … tlr) [ assumption  @(soundly_step … GE EX S1) ] ] 2721  @no_loops_in_tal // @ CL2722 ] qed. 2723 2775  @no_loops_in_tal // @simplify_cl @CL 2776 ] qed. 2777 
src/RTLabs/abstract.ma
r2511 r2571 201 201 *) 202 202 203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. RTLabs_classify s =cl_call) → RTLabs_ext_state ge → Prop ≝203 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → RTLabs_ext_state ge → Prop ≝ 204 204 λge,s,s'. 205 205 match s with 206 206 [ mk_Sig s p ⇒ 207 match s return λs. RTLabs_classify s =cl_call → ? with207 match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with 208 208 [ Callstate fd args dst stk m ⇒ 209 209 λ_. match s' with … … 219 219 ] p 220 220 ]. 221 [ whd in H:(?? %?);221 [ whd in H:(??(??%)?); 222 222 cases (next_instruction f) in H; 223 223 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct … … 226 226 ] qed. 227 227 228 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. RTLabs_classify s =cl_call) → ident ≝228 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_ext_state ge. Some ? (RTLabs_classify s) = Some ? cl_call) → ident ≝ 229 229 λge,s. 230 230 match s with 231 231 [ mk_Sig s p ⇒ 232 match s return λs':RTLabs_ext_state ge. RTLabs_classify s' =cl_call → ident with232 match s return λs':RTLabs_ext_state ge. Some ? (RTLabs_classify s') = Some ? cl_call → ident with 233 233 [ mk_RTLabs_ext_state s' stk mtc0 ⇒ 234 match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' =cl_call → ident with234 match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with 235 235 [ Callstate fd _ _ _ _ ⇒ 236 236 match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with … … 243 243 ] p 244 244 ]. 245 [ whd in H:(?? %?);245 [ whd in H:(??(??%)?); 246 246 cases (next_instruction f) in H; 247 247 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct … … 251 251 ] qed. 252 252 253 lemma RTLabs_notail : ∀s. 254 RTLabs_classify s = cl_tailcall → 255 False. 256 * [ #f #fs #m whd in ⊢ (??%? → ?); cases (next_instruction f) ] 257 normalize 258 #a try #b try #c try #d try #e try #g try #h try #i try #j destruct 259 qed. 260 261 (* Roughly corresponding to as_classifier *) 262 lemma RTLabs_notail' : ∀s. 263 Some ? (RTLabs_classify s) = Some ? cl_tailcall → 264 False. 265 #s #E @(RTLabs_notail … s) 266 generalize in match (RTLabs_classify s) in E ⊢ %; 267 #c #E' destruct % 268 qed. 253 269 254 270 definition RTLabs_status : genv → abstract_status ≝ … … 259 275 RTLabs_deqset 260 276 (RTLabs_ext_state_to_pc ge) 261 RTLabs_classify277 (λs. Some ? (RTLabs_classify s)) 262 278 (RTLabs_pc_to_cost_label ge) 263 279 (RTLabs_after_return ge) 264 280 (λs. RTLabs_is_final s ≠ None ?) 265 (RTLabs_call_ident ge). 266 267 281 (RTLabs_call_ident ge) 282 (λs. ⊥). 283 (* No tailcalls here for now. *) 284 cases s @RTLabs_notail' 285 qed. 268 286 269 287 (* Allow us to move between the different notions of when a state is cost
Note: See TracChangeset
for help on using the changeset viewer.