Changeset 2840


Ignore:
Timestamp:
Mar 11, 2013, 12:18:26 PM (7 years ago)
Author:
campbell
Message:

Remove irrelevant stuff from RTLabs_partial_traces

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/RTLabs/RTLabs_partial_traces.ma

    r2839 r2840  
    107107qed.
    108108
    109 (* Need a way to choose whether a called function terminates.  Then,
    110      if the initial function terminates we generate a purely inductive structured trace,
    111      otherwise we start generating the coinductive one, and on every function call
    112        use the choice method again to decide whether to step over or keep going.
    113 
    114 Not quite what we need - have to decide on seeing each label whether we will see
    115 another or hit a non-terminating call?
    116 
    117 Also - need the notion of well-labelled in order to break loops.
    118 
    119 
    120 
    121 outline:
    122 
    123  does function terminate?
    124  - yes, get (bound on the number of steps until return), generate finite
    125         structure using bound as termination witness
    126  - no,  get (¬ bound on steps to return), start building infinite trace out of
    127         finite steps.  At calls, check for termination, generate appr. form.
    128 
    129 generating the finite parts:
    130 
    131 We start with the status after the call has been executed; well-labelling tells
    132 us that this is a labelled state.  Now we want to generate a trace_label_return
    133 and also return the remainder of the flat trace.
    134 
    135 *)
    136109
    137110(* [will_return ge depth s trace] says that after a finite number of steps of
    … …  
    1009982 *)
    1010983
    1011 inductive inhabited (T:Type[0]) : Prop ≝
    1012 | witness : T → inhabited T.
    1013984
    1014985
    … …  
    13221293] qed.
    13231294
    1324 (* When constructing an infinite trace, we need to be able to grab the finite
    1325    portion of the trace for the next [trace_label_diverges] constructor.  We
    1326    use the fact that the trace is soundly labelled to achieve this. *)
    1327 
    1328 record remainder_ok (ge:genv) (s:RTLabs_ext_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {
    1329   ro_well_cost_labelled: well_cost_labelled_state s;
    1330   ro_soundly_labelled: soundly_labelled_state s;
    1331   ro_no_termination: Not (∃depth. inhabited (will_return ge depth s t));
    1332   ro_not_final: RTLabs_is_final s = None ?
    1333 }.
    1334 
    1335 inductive finite_prefix (ge:genv) : RTLabs_ext_state ge → Prop ≝
    1336 | fp_tal : ∀s,s':RTLabs_ext_state ge.
    1337            trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' →
    1338            ∀t:flat_trace io_out io_in ge s'.
    1339            remainder_ok ge s' t →
    1340            finite_prefix ge s
    1341 | fp_tac : ∀s1,s2,s3:RTLabs_ext_state ge.
    1342            trace_any_call (RTLabs_status ge) s1 s2 →
    1343            well_cost_labelled_state s2 →
    1344            as_execute (RTLabs_status ge) s2 s3 →
    1345            ∀t:flat_trace io_out io_in ge s3.
    1346            remainder_ok ge s3 t →
    1347            finite_prefix ge s1
    1348 .
    1349 
    1350 definition fp_add_default : ∀ge. ∀s,s':RTLabs_ext_state ge.
    1351   RTLabs_classify s = cl_other →
    1352   finite_prefix ge s' →
    1353   as_execute (RTLabs_status ge) s s' →
    1354   RTLabs_cost s' = false →
    1355   finite_prefix ge s ≝
    1356 λge,s,s',OTHER,fp.
    1357 match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with
    1358 [ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf
    1359     (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST))
    1360     rem rok
    1361 | fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3
    1362     (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST))
    1363     WCL2 EV rem rok
    1364 ].
    1365 
    1366 definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_ext_state ge.
    1367   as_execute (RTLabs_status ge) s s1 →
    1368   ∀CALL:RTLabs_classify s = cl_call.
    1369   finite_prefix ge s'' →
    1370   trace_label_return (RTLabs_status ge) s1 s'' →
    1371   as_after_return (RTLabs_status ge) «s, CALL» s'' →
    1372   RTLabs_cost s'' = false →
    1373   finite_prefix ge s ≝
    1374 λge,s,s1,s'',EVAL,CALL,fp.
    1375 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
    1376 [ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf
    1377     (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL)
    1378     rem rok
    1379 | fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3
    1380     (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL (CALL) RET TLR (RTLabs_not_cost … NOT_COST) TAC)
    1381     WCL2 EV rem rok
    1382 ].
    1383 
    1384 lemma not_return_to_not_final : ∀ge,s,tr,s'.
    1385   eval_statement ge s = Value ??? 〈tr, s'〉 →
    1386   RTLabs_classify s ≠ cl_return →
    1387   RTLabs_is_final s' = None ?.
    1388 #ge #s #tr #s' #EV
    1389 inversion (eval_preserves … EV) //
    1390 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #CL
    1391 @⊥ @(absurd ?? CL) @refl
    1392 qed.
    1393 (*
    1394 definition termination_oracle ≝ ∀ge,depth,s,trace.
    1395   inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
    1396 
    1397 let rec finite_segment ge (s:RTLabs_ext_state ge) n trace
    1398   (ORACLE: termination_oracle)
    1399   (TRACE_OK: remainder_ok ge s trace)
    1400   (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    1401   (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
    1402   (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
    1403   on n : finite_prefix ge s ≝
    1404 match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with
    1405 [ O ⇒ λLABEL_LIMIT. ⊥
    1406 | S n' ⇒
    1407   match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace'.
    1408     match trace' return λs:state.λtrace:flat_trace io_out io_in ge s. ∀mtc:Ras_Fn_Match ge s stk. remainder_ok ge (mk_RTLabs_ext_state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_ext_state ge s ? mtc) with
    1409     [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥
    1410     | ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT.
    1411         let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
    1412         let next' ≝ next_state ge start' next tr EV in
    1413         match RTLabs_classify start return λx. RTLabs_classify start = x → ? with
    1414         [ cl_other ⇒ λCL.
    1415             let TRACE_OK' ≝ ? in
    1416             match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
    1417             [ true ⇒ λCS.
    1418                 fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ((proj1 … (RTLabs_costed ge next')) … CS)) trace' TRACE_OK'
    1419             | false ⇒ λCS.
    1420                 let fs ≝ finite_segment ge next' n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    1421                 fp_add_default ge start' next' CL fs ? CS
    1422             ] (refl ??)
    1423         | cl_jump ⇒ λCL.
    1424             fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ?) trace' ?
    1425         | cl_call ⇒ λCL.
    1426             match ORACLE ge O next trace' return λ_. finite_prefix ge start' with
    1427             [ or_introl TERMINATES ⇒
    1428               match TERMINATES with [ witness TERMINATES ⇒
    1429                 let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in
    1430                 let TRACE_OK' ≝ ? in
    1431                 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with
    1432                 [ 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'
    1433                 | false ⇒ λCS.
    1434                     let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    1435                     fp_add_terminating_call … fs (new_trace … tlr) ? CS
    1436                 ] (refl ??)
    1437               ]
    1438             | or_intror NO_TERMINATION ⇒
    1439                 fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' (or_introl … (CL))) ?? trace' ?
    1440             ]
    1441         | cl_return ⇒ λCL. ⊥
    1442         | cl_tailcall ⇒ λCL. ⊥
    1443         ] (refl ??)
    1444     ] mtc0
    1445   ] trace TRACE_OK
    1446 ] LABEL_LIMIT.
    1447 [ cases (state_bound_on_steps_to_cost_zero s) /2/
    1448 | @(absurd …  (ro_not_final … TRACE_OK) FINAL)
    1449 | @(absurd ?? (ro_no_termination … TRACE_OK))
    1450      %{0} % @wr_base //
    1451 | @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
    1452 | %1 @(CL)
    1453 | 6,9,10,11: /3/
    1454 | cases TRACE_OK #H1 #H2 #H3 #H4
    1455   % [ @(well_cost_labelled_state_step … EV) //
    1456     | @(soundly_labelled_state_step … EV) //
    1457     | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/
    1458     | @(not_return_to_not_final … EV) >CL % #E destruct
    1459     ]
    1460 | @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
    1461 | @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
    1462 | @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS)
    1463   @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
    1464 | % [ /2/
    1465     | @(soundly_labelled_state_preserved … (stack_ok … tlr))
    1466       @(soundly_labelled_state_step … EV) /2/ @(ro_soundly_labelled … TRACE_OK)
    1467     | @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} %
    1468       @wr_call //
    1469       @(will_return_prepend … TERMINATES … TM1)
    1470       cases (terminates … tlr) //
    1471     | (* By stack preservation we cannot be in the final state *)
    1472       inversion (stack_ok … tlr)
    1473       [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
    1474       | #s1 #f #f' #fs #m #fn #S #M #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
    1475       | #s1 #r #M #S #E1 #E2 #E3 #E4 change with (next_state ?????) in E2:(??%??); -TERMINATES destruct -next' -s0
    1476         cases (rtlabs_call_inv … CL) #vf * #fd * #args * #dst * #stk * #m #E destruct
    1477         inversion (eval_preserves … EV)
    1478         [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 try #H124 @⊥ -next destruct ]
    1479         #ge' #vf' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
    1480         inversion S
    1481         [ #f #fs0 #m #fn0 #S0 #M0 #E1 #E2 whd in ⊢ (??%?% → ?); generalize in ⊢ (??(????%)?? → ?); #M'' #E3 #_ destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H1 #H2 #H3 try #H130 try #H4 try #H5 try #H6 [ whd in H6:(??%?%); | whd in H2:(??%?%); ] destruct ]
    1482         (* state_bound_on_steps_to_cost needs to know about the current stack frame,
    1483            so we can use it as a witness that at least one frame exists *)
    1484         inversion LABEL_LIMIT
    1485         #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 try #H151 destruct
    1486       | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 destruct
    1487       ]
    1488     ]
    1489 | @(well_cost_labelled_state_step … EV) /2/ @(ro_well_cost_labelled … TRACE_OK)
    1490 | @(well_cost_labelled_call … EV) [ @(ro_well_cost_labelled … TRACE_OK) | // ]
    1491 | /2/
    1492 | %{tr} %{EV} %
    1493 | cases TRACE_OK #H1 #H2 #H3 #H4
    1494   % [ @(well_cost_labelled_state_step … EV) /2/
    1495     | @(soundly_labelled_state_step … EV) /2/
    1496     | @(not_to_not … NO_TERMINATION) * #depth * #TM %
    1497       @(will_return_lower … TM) //
    1498     | @(not_return_to_not_final … EV) >CL % #E destruct
    1499     ]
    1500 | @(RTLabs_notail … CL)
    1501 | %2 @(CL)
    1502 | 21,22: %{tr} %{EV} %
    1503 | cases (bound_after_step … LABEL_LIMIT EV ?)
    1504   [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
    1505     inversion trace'
    1506     [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
    1507       @(absurd ?? FINAL) @(not_return_to_not_final … EV)
    1508       % >CL #E destruct
    1509     | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
    1510       @wr_base //
    1511     ]
    1512     ]
    1513     | >CL #E destruct
    1514     ]
    1515   | //
    1516   | //
    1517   ]
    1518 | cases (bound_after_step … LABEL_LIMIT EV ?)
    1519   [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
    1520     inversion trace'
    1521     [ #s0 #FINAL #E1 #E2 -TRACE_OK' destruct @⊥
    1522       @(absurd ?? FINAL) @(not_return_to_not_final … EV)
    1523       % >CL #E destruct
    1524     | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 -TRACE_OK' destruct
    1525       @wr_base //
    1526     ]
    1527     ]
    1528     | >CL #E destruct
    1529     ]
    1530   | //
    1531   | //
    1532   ]
    1533 | cases TRACE_OK #H1 #H2 #H3 #H4
    1534   % [ @(well_cost_labelled_state_step … EV) //
    1535     | @(soundly_labelled_state_step … EV) //
    1536     | @(not_to_not … (ro_no_termination … TRACE_OK))
    1537       * #depth * #TERM %{depth} % @wr_step /2/
    1538     | @(not_return_to_not_final … EV) >CL % #E destruct
    1539     ]
    1540 ] qed.
    1541 *)
    15421295lemma simplify_cl : ∀ge,s,c.
    15431296  as_classifier (RTLabs_status ge) s c →
    … …  
    18911644[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
    18921645] EX''.
    1893 (*
    1894 (* Now reconstruct the flat_trace of a diverging execution.  Note that we need
    1895    to take care to satisfy the guardedness condition by witnessing the fact that
    1896    the partial traces are non-empty. *)
    1897 let corec flat_trace_of_label_diverges ge (s:RTLabs_ext_state ge)
    1898   (tr:trace_label_diverges (RTLabs_status ge) s)
    1899 : flat_trace io_out io_in ge s ≝
    1900 match tr return λs:RTLabs_ext_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with
    1901 [ tld_step sx sy tll tld ⇒
    1902   match sy in RTLabs_ext_state return λsy:RTLabs_ext_state ge. trace_label_label (RTLabs_status ge) ? sx sy → trace_label_diverges (RTLabs_status ge) sy → flat_trace io_out io_in ge ? with [ mk_RTLabs_ext_state sy' stk mtc0 ⇒
    1903     λtll.
    1904     match flat_trace_of_label_label ge … tll return λs1,s2:state.λ_:partial_flat_trace io_out io_in ge s1 s2. ∀mtc:Ras_Fn_Match ge s2 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s2 stk mtc) → flat_trace ??? s1 with
    1905     [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
    1906     | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld)
    1907     ] mtc0 ] tll tld
    1908 | tld_base s1 s2 s3 tlc EX CL tld ⇒
    1909   match s3 in RTLabs_ext_state return λs3:RTLabs_ext_state ge. as_execute (RTLabs_status ge) ? s3 → trace_label_diverges (RTLabs_status ge) s3 → flat_trace io_out io_in ge ? with [ mk_RTLabs_ext_state s3' stk mtc0 ⇒
    1910     λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    1911       match flat_trace_of_label_call … tlc EX' return λs1,s3.λ_. ∀mtc:Ras_Fn_Match ge s3 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s3 stk mtc) → flat_trace ??? s1 with
    1912       [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
    1913       | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld)
    1914       ] mtc0
    1915     ]
    1916   ] EX tld
    1917 ]
    1918 (* Helper to keep adding the partial trace without violating the guardedness
    1919    condition. *)
    1920 and add_partial_flat_trace ge (s:state) (s':RTLabs_ext_state ge)
    1921 : partial_flat_trace io_out io_in ge s s' →
    1922   trace_label_diverges (RTLabs_status ge) s' →
    1923   flat_trace io_out io_in ge s ≝
    1924 match s' return λs':RTLabs_ext_state ge. partial_flat_trace io_out io_in ge s s' → trace_label_diverges (RTLabs_status ge) s' → flat_trace io_out io_in ge s with [ mk_RTLabs_ext_state sx stk mtc ⇒
    1925 λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s' ? mtc) → flat_trace io_out io_in ge s with
    1926 [ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr)
    1927 | pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_ext_state ge s3 stk mtc) tr' tr)
    1928 ] mtc ]
    1929 .
    1930 
    1931 
    1932 coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝
    1933 | eft_stop : ∀s,F. equal_flat_traces ge s (ft_stop … F) (ft_stop … F)
    1934 | eft_step : ∀s,tr,s',EX,tr1,tr2. equal_flat_traces ge s' tr1 tr2 → equal_flat_traces ge s (ft_step … EX tr1) (ft_step … s tr s' EX tr2).
    1935 
    1936 let corec flat_traces_are_determined_by_starting_point ge s tr1
    1937 : ∀tr2. equal_flat_traces ge s tr1 tr2 ≝
    1938 match tr1 return λs,tr1. flat_trace ??? s → equal_flat_traces ? s tr1 ? with
    1939 [ ft_stop s F ⇒ λtr2. ?
    1940 | ft_step s1 tr s2 EX0 tr1' ⇒ λtr2.
    1941     match tr2 return λs,tr2. ∀EX:eval_statement ge s = ?. equal_flat_traces ? s (ft_step ??? s ?? EX ?) tr2 with
    1942     [ ft_stop s F ⇒ λEX. ?
    1943     | ft_step s tr' s2' EX' tr2' ⇒ λEX. ?
    1944     ] EX0
    1945 ].
    1946 [ inversion tr2 in tr1 F;
    1947   [ #s #F #_ #_ #tr1 #F' @eft_stop
    1948   | #s1 #tr #s2 #EX #tr' #E #_ #tr'' #F' @⊥ destruct
    1949     cases (final_cannot_move ge … F') #err #Er >Er in EX; #E destruct
    1950   ]
    1951 | @⊥ cases (final_cannot_move ge … F) #err #Er >Er in EX; #E destruct
    1952 | -EX0
    1953   cut (s2 = s2'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
    1954   @(match E return λs2',E. ∀tr2':flat_trace ??? s2'. ∀EX':? = Value ??? 〈?,s2'〉. equal_flat_traces ??? (ft_step ????? s2' EX' tr2') with [ refl ⇒ ? ] tr2' EX')
    1955   -E -EX' -tr2' #tr2' #EX'
    1956   cut (tr = tr'). >EX in EX'; #E destruct @refl. #E (* Can't use destruct due to cofixpoint guardedness check *)
    1957   @(match E return λtr',E. ∀EX':? = Value ??? 〈tr',?〉. equal_flat_traces ??? (ft_step ???? tr' ? EX' ?) with [ refl ⇒ ? ] EX')
    1958   -E -EX' #EX'
    1959     @eft_step @flat_traces_are_determined_by_starting_point
    1960 ] qed.
    1961 
    1962 let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
    1963   (str:trace_label_diverges (RTLabs_status ge) s)
    1964   (tr:flat_trace io_out io_in ge s)
    1965 : equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.
    1966 @flat_traces_are_determined_by_starting_point
    1967 qed.
    1968 
    1969 let rec flat_trace_of_whole_program ge (s:RTLabs_ext_state ge)
    1970   (tr:trace_whole_program (RTLabs_status ge) s)
    1971 on tr : flat_trace io_out io_in ge s ≝
    1972 match tr return λs:RTLabs_ext_state ge.λtr. flat_trace io_out io_in ge s with
    1973 [ twp_terminating s1 s2 sf CL EX tlr F ⇒
    1974     match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    1975       ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F))
    1976     ]
    1977 | twp_diverges s1 s2 CL EX tld ⇒
    1978     match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    1979       ft_step … EX' (flat_trace_of_label_diverges … tld)
    1980     ]
    1981 ].
    1982 
    1983 let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge)
    1984   (str:trace_whole_program (RTLabs_status ge) s)
    1985   (tr:flat_trace io_out io_in ge s)
    1986 : equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
    1987 @flat_traces_are_determined_by_starting_point
    1988 qed.
    1989 *)
    19901646
    19911647
Note: See TracChangeset for help on using the changeset viewer.