Ignore:
Timestamp:
Mar 16, 2013, 9:08:18 PM (7 years ago)
Author:
campbell
Message:

Some progress on showing that the change to structured traces preserves
observables.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_partial_traces.ma

    r2840 r2894  
    106106#ST' whd in ⊢ (??%?); %
    107107qed.
     108
     109let rec length_flat_trace O I ge s (t:flat_trace O I ge s) on t : nat ≝
     110match t with
     111[ ft_stop _ ⇒ 0
     112| ft_step _ _ _ _ t' ⇒ S (length_flat_trace … t')
     113].
    108114
    109115
     
    633639] qed.
    634640
     641(* Measure the number of steps in the structured trace so that we know it's the
     642   same execution that we started with.  TODO: move  *)
     643let rec length_tlr (S:abstract_status) s1 s2 (tlr:trace_label_return S s1 s2) on tlr : nat ≝
     644match tlr with
     645[ tlr_base _ _ tll ⇒ length_tll … tll
     646| tlr_step _ _ _ tll tlr' ⇒ length_tll … tll + length_tlr … tlr'
     647]
     648and length_tll (S:abstract_status) e s1 s2 (tll:trace_label_label S e s1 s2) on tll : nat ≝
     649match tll with
     650[ tll_base _ _ _ tal _ ⇒ length_tal … tal
     651]
     652and length_tal (AS:abstract_status) e s1 s2 (tal:trace_any_label AS e s1 s2) on tal : nat ≝
     653match tal with
     654[ tal_base_not_return _ _ _ _ _ ⇒ 1
     655| tal_base_return _ _ _ _ ⇒ 1
     656| tal_base_call _ _ _ _ _ _ tlr _ ⇒ S (length_tlr … tlr)
     657| tal_base_tailcall _ _ _ _ _ tlr ⇒ S (length_tlr … tlr)
     658| tal_step_call _ _ _ _ _ _ _ _ tlr _ tal' ⇒ S (length_tlr … tlr + length_tal … tal')
     659| tal_step_default _ _ _ _ _ tal' _ _ ⇒ S (length_tal … tal')
     660].
     661
     662
     663
    635664(* Don't need to know that labels break loops because we have termination. *)
    636665
     
    641670  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
    642671  (original_terminates: will_return ge depth start full)
    643   (T:RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
     672  (T:RTLabs_ext_state ge → Type[0]) (length:∀s. T s → nat) (limit:nat) : Type[0] ≝
    644673{
    645674  new_state : RTLabs_ext_state ge;
     
    647676  cost_labelled : well_cost_labelled_state new_state;
    648677  new_trace : T new_state;
     678  tr_length : plus (length … new_trace) (length_flat_trace … remainder) = length_flat_trace … full;
    649679  stack_ok : stack_preserved ge ends start new_state;
    650680  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
     
    661691  (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start)
    662692  (original_terminates: will_return ge depth start full)
    663   (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝
     693  (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0])
     694  (length:∀e,s. T e s → nat)
     695  (limit:nat) : Type[0] ≝
    664696{
    665697  ends : trace_ends_with_ret;
    666   trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit
     698  trace_res :> trace_result ge depth ends start full original_terminates (T ends) (length ends) limit
    667699}.
    668700
     
    671703   the size of the termination proof might need to be relaxed, too. *)
    672704
    673 definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
    674   ∀r:trace_result ge d e s1 t1 TM1 T1 l1.
     705definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2. l2 ≥ l1 →
     706  ∀r:trace_result ge d e s1 t1 TM1 T1 ln1 l1.
    675707    will_return_end … TM1 = will_return_end … TM2 →
    676     T2 (new_state … r) →
     708    ∀trace:T2 (new_state … r).
     709    ln2 (new_state … r) trace + length_flat_trace … (remainder … r) = length_flat_trace … t2 →
    677710    stack_preserved ge e s2 (new_state … r) →
    678     trace_result ge d e s2 t2 TM2 T2 l2 ≝
    679 λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
    680   mk_trace_result ge d e s2 t2 TM2 T2 l2
     711    trace_result ge d e s2 t2 TM2 T2 ln2 l2 ≝
     712λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2,lGE,r,TME,trace,LN,SP.
     713  mk_trace_result ge d e s2 t2 TM2 T2 ln2 l2
    681714    (new_state … r)
    682715    (remainder … r)
    683716    (cost_labelled … r)
    684717    trace
     718    LN
    685719    SP
    686720    ?
     
    691725cases e in r ⊢ %;
    692726[ <TME -TME * cases d in TM1 TM2 ⊢ %;
    693   [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS
    694   | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
     727  [ #TM1 #TM2 #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %); #TMS @TMS
     728  | #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %); * #TMa * #L1 #TME
    695729    %{TMa} % // @(transitive_le … lGE) @L1
    696730  ]
    697 | <TME -TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %);
     731| <TME -TME * #ns #rem #WCLS #T1NS #LN1 #SP whd in ⊢ (% → %);
    698732   * #TMa * #L1 #TME
    699733    %{TMa} % // @(transitive_le … lGE) @L1
    700734] qed.
    701735
    702 definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →
    703   ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1.
     736definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2. l2 ≥ l1 →
     737  ∀r:sub_trace_result ge d s1 t1 TM1 T1 ln1 l1.
    704738    will_return_end … TM1 = will_return_end … TM2 →
    705     T2 (ends … r) (new_state … r) →
     739    ∀trace:T2 (ends … r) (new_state … r).
     740    ? (*XXX matita infers this, but won't check it ?! *) + length_flat_trace … (remainder … r) = length_flat_trace ???? t2 →
    706741    stack_preserved ge (ends … r) s2 (new_state … r) →
    707     sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
    708 λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
    709   mk_sub_trace_result ge d s2 t2 TM2 T2 l2
     742    sub_trace_result ge d s2 t2 TM2 T2 ln2 l2 ≝
     743λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,ln1,ln2,l1,l2,lGE,r,TME,trace,LN,SP.
     744  mk_sub_trace_result ge d s2 t2 TM2 T2 ln2 l2
    710745    (ends … r)
    711     (replace_trace … lGE … r TME trace SP).
     746    (replace_trace … lGE … r TME trace LN SP).
    712747
    713748(* Small syntax hack to avoid ambiguous input problems. *)
    714749definition myge : nat → nat → Prop ≝ ge.
     750
     751lemma crappyhack : ∀tlr,rem1,tr,tal,rem2:nat.
     752  tlr+rem1 = tr → tal + rem2 = rem1 → S (tlr + tal) + rem2 = S tr.
     753#tlr #rem1 #tr #tal #rem2 #E1 #E2 destruct <associative_plus %
     754qed.
    715755
    716756let rec make_label_return ge depth (s:RTLabs_ext_state ge)
     
    724764  on TIME : trace_result ge depth ends_with_ret s trace TERMINATES
    725765              (trace_label_return (RTLabs_status ge) s)
    726               (will_return_length … TERMINATES) ≝
     766              (length_tlr (RTLabs_status ge) s)
     767              (will_return_length … TERMINATES) ≝
    727768             
    728769match TIME return λTIME. TIME ≥ ? → ? with
     
    737778            TERMINATES
    738779            TIME ? in
    739   match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? →
    740                             trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
     780  match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) (length_tll (RTLabs_status ge) x s) ? →
     781                            trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) ? (will_return_length … TERMINATES) with
    741782  [ ends_with_ret ⇒ λr.
    742       replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
     783      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) ? (stack_ok … r)
    743784  | doesnt_end_with_ret ⇒ λr.
    744785      let r' ≝ make_label_return ge depth (new_state … r)
     
    749790        replace_trace … r' ?
    750791          (tlr_step (RTLabs_status ge) s (new_state … r)
    751             (new_state … r') (new_trace … r) (new_trace … r')) ?
     792            (new_state … r') (new_trace … r) (new_trace … r')) ??
    752793  ] (trace_res … r)
    753794
     
    765806  on TIME : sub_trace_result ge depth s trace TERMINATES
    766807              (λends. trace_label_label (RTLabs_status ge) ends s)
     808              (λends. length_tll (RTLabs_status ge) ends s)
    767809              (will_return_length … TERMINATES) ≝
    768810             
     
    773815let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
    774816  replace_sub_trace … r ?
    775     (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)
     817    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) ? (stack_ok … r)
    776818
    777819] TERMINATES_IN_TIME
     
    787829  on TIME : sub_trace_result ge depth s0 trace TERMINATES
    788830              (λends. trace_any_label (RTLabs_status ge) ends s0)
     831              (λends. length_tal (RTLabs_status ge) ends s0)
    789832              (will_return_length … TERMINATES) ≝
    790833
    791834match TIME return λTIME. TIME ≥ ? → ? with
    792835[ O ⇒ λTERMINATES_IN_TIME. ⊥
    793 | S TIME ⇒ λTERMINATES_IN_TIME.
     836| S TIME ⇒ λTERMINATES_IN_TIME. 
    794837  match s0 return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s.
    795838                                      well_cost_labelled_state s →
    796839                                      ∀TM:will_return ??? trace.
    797840                                      myge ? (times 3 (will_return_length ??? trace TM)) →
    798                                       sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM)
     841                                      sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (λends. length_tal (RTLabs_status ge) ends s) (will_return_length … TM)
    799842  with [ mk_RTLabs_ext_state s stk mtc0 ⇒ λtrace.
    800843  match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk.
     
    802845                               ∀TM:will_return ??? trace.
    803846                               myge ? (times 3 (will_return_length ??? trace TM)) →
    804                                sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with
     847                               sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (λends. length_tal (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with
    805848  [ ft_stop st ⇒
    806849      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
     
    809852    let start' ≝ mk_RTLabs_ext_state ge start stk mtc in
    810853    let next' ≝ next_state ? start' ?? EV in
    811     match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     854    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    812855    [ cl_other ⇒ λCL.
    813         match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     856        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    814857        (* We're about to run into a label. *)
    815858        [ true ⇒ λCS.
    816             mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
     859            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ?
    817860              doesnt_end_with_ret
    818861              (mk_trace_result ge … next' trace' ?
    819                 (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ??)
     862                (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ???)
    820863        (* An ordinary step, keep going. *)
    821864        | false ⇒ λCS.
    822865            let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
    823                 replace_sub_trace ????????????? r ?
     866                replace_sub_trace ??????????????? r ?
    824867                  (tal_step_default (RTLabs_status ge) (ends … r)
    825                      start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ?
     868                     start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ??
    826869        ] (refl ??)
    827870       
    828871    | cl_jump ⇒ λCL.
    829         mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
     872        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ?
    830873          doesnt_end_with_ret
    831874          (mk_trace_result ge … next' trace' ?
    832             (tal_base_not_return (RTLabs_status ge) start' next' ???) ??)
     875            (tal_base_not_return (RTLabs_status ge) start' next' ???) ???)
    833876           
    834877    | cl_call ⇒ λCL.
    835878        let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
    836         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
     879        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 ?) (λends. length_tal (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    837880        (* We're about to run into a label, use base case for call *)
    838881        [ true ⇒ λCS.
    839             mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
     882            mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ?
    840883            doesnt_end_with_ret
    841884            (mk_trace_result ge …
    842885              (tal_base_call (RTLabs_status ge) start' next' (new_state … r)
    843                 ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??)
     886                ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ???)
    844887        (* otherwise use step case *)
    845888        | false ⇒ λCS.
     
    850893              (tal_step_call (RTLabs_status ge) (ends … r')
    851894                start' next' (new_state … r) (new_state … r') ? CL ?
    852                 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ?
     895                (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ??
    853896        ] (refl ??)
    854897
    855898    | cl_return ⇒ λCL.
    856         mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ?
     899        mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') (λends. length_tal (RTLabs_status ge) ends start') ?
    857900          ends_with_ret
    858           (mk_trace_result ge ???????
     901          (mk_trace_result ge ????????
    859902            next'
    860903            trace'
    861904            ?
    862905            (tal_base_return (RTLabs_status ge) start' next' ? CL)
     906            ?
    863907            ?
    864908            ?)
     
    872916| //
    873917| //
    874 | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT)
    875 | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
     918| @(tr_length … r)
     919| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #GT #_ @(le_S_to_le … GT)
     920| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #_ #EEQ //
     921| <(tr_length … r) <(tr_length … r') @associative_plus
    876922| @(stack_preserved_join … (stack_ok … r)) //
    877923| @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r))
    878 | cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
     924| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 * #LT #_
    879925  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    880926  @(transitive_le …  (3*(will_return_length … TERMINATES)))
     
    888934| //
    889935| @(proj1 … (RTLabs_costed …)) //
     936| @(tr_length … r)
    890937| @le_S_S_to_le @TERMINATES_IN_TIME
    891938| @(wrl_nonzero … TERMINATES_IN_TIME)
     
    900947| @(will_return_return … CL TERMINATES)
    901948| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     949| %
    902950| %{tr} %{EV} @refl
    903951| @(well_cost_labelled_state_step  … EV) //
    904952| whd @(will_return_notfn … TERMINATES) %2 @CL
    905953| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     954| %
    906955| %{tr} %{EV} %
    907956| %1 whd @CL
    908957| @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) //
    909958| @(well_cost_labelled_state_step  … EV) //
    910 | whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
     959| whd cases (terminates ????????? r) #TMr * #LTr #EQr %{TMr} %
    911960  [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES)
    912961    #TMx * #LT' #_ @LT'
     
    915964  ]
    916965| @(stack_preserved_step ge start' ?? CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
     966| whd in ⊢ (???%); <(tr_length … r) %
    917967| %{tr} %{EV} %
    918968| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
    919969| @(cost_labelled … r)
    920970| skip
    921 | cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le
     971| cases r #ns #rm #WS #TLR #SP #LN * #TM * #LT #_ @le_S_to_le
    922972  @(transitive_lt … LT)
    923973  cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT'
    924 | cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
     974| cases r #ns #rm #WS #TLR #SP #LN * #TM * #_ #EQ <EQ
    925975  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
    926976| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
    927977| %{tr} %{EV} %
     978| @(crappyhack ????? (tr_length … r) (tr_length … r'))
    928979| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
    929980| @(cost_labelled … r)
    930 | cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
     981| cases r #H72 #H73 #H74 #H75 #HX #LN * #HY * #GT #H78
    931982  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    932983  cases (will_return_call … TERMINATES) in GT;
     
    947998| whd @(will_return_notfn … TERMINATES) %1 @CL
    948999| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
     1000| %
    9491001| %{tr} %{EV} %
    9501002| %2 whd @CL
     
    9541006| @CL
    9551007| %{tr} %{EV} %
     1008| whd in ⊢ (??%%); @eq_f @(tr_length … r)
    9561009| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    9571010| @(well_cost_labelled_state_step  … EV) //
     
    9711024  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    9721025  (TERMINATES: will_return ge depth s trace)
    973   : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
     1026  : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (length_tlr (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
    9741027make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
    9751028  (2 + 3 * will_return_length … TERMINATES) ?.
Note: See TracChangeset for help on using the changeset viewer.