Changeset 1960


Ignore:
Timestamp:
May 16, 2012, 5:24:05 PM (7 years ago)
Author:
campbell
Message:

Update RTLabs structured traces to make minor changes in definitions.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1880 r1960  
    2121].
    2222
     23(* We define a straight "is this a cost label" pair of functions, which is
     24   convenient for most of our uses here (because we can make a hypothesis of
     25   it without naming the label), and a pair which return the label to fit the
     26   definition of abstract_status. *)
     27   
    2328definition is_cost_label : statement → bool ≝
    2429λs. match s with [ St_cost _ _ ⇒ true | _ ⇒ false ].
     
    3136].
    3237
    33 definition RTLabs_status : genv → final_abstract_status ≝
     38definition cost_label_of : statement → option costlabel ≝
     39λs. match s with [ St_cost s _ ⇒ Some ? s | _ ⇒ None ? ].
     40
     41definition RTLabs_cost_label : state → option costlabel ≝
     42λs. match s with
     43[ State f fs m ⇒
     44    cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))
     45| _ ⇒ None ?
     46].
     47
     48(* At the moment we don't need to talk about the program counter, so we just
     49   use unit. *)
     50definition unit_deqset ≝ mk_DeqSet unit (λ_.λ_. true) ?.
     51* * % //
     52qed.
     53
     54definition RTLabs_status : genv → abstract_status ≝
    3455λge.
    35 mk_final_abstract_status
    36   (mk_abstract_status
     56  mk_abstract_status
    3757    state
    3858    (λs,s'. ∃t. eval_statement ge s = Value ??? 〈t,s'〉)
     59    unit_deqset
     60    (λ_. it)
    3961    (λs,c. RTLabs_classify s = c)
    40     (λs. RTLabs_cost s = true)
     62    RTLabs_cost_label
    4163    (λs,s'. match s with
    4264      [ mk_Sig s p ⇒
     
    5173        | _ ⇒ λH.⊥
    5274        ] p
    53       ]))
     75      ])
    5476  (λs. RTLabs_is_final s ≠ None ?).
    55 [ whd in H:(??%?);
     77[ normalize in H; destruct
     78| normalize in H; destruct
     79| whd in H:(??%?);
    5680  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
    5781  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
    58 | normalize in H; destruct
    59 | normalize in H; destruct
     82] qed.
     83
     84(* Allow us to move between the different notions of when a state is cost
     85   labelled. *)
     86
     87lemma RTLabs_costed : ∀ge,s.
     88  RTLabs_cost s = true →
     89  as_costed (RTLabs_status ge) s.
     90#ge *
     91[ * #func #locals #next #nok #b #r #fs #m
     92  whd in ⊢ (??%? → %); whd in ⊢ (? → ?(??%?));
     93  cases (lookup_present ?? (f_graph func) ??) normalize
     94  #A try #B try #C try #D try #E try #F try #G try #H try #G destruct
     95  % #E' destruct
     96| normalize #fd #args #r #fs #m #E destruct
     97| normalize #A #B #C #D #E destruct
     98| normalize #A #B destruct
     99] qed.
     100
     101lemma costed_RTLabs : ∀ge,s.
     102  as_costed (RTLabs_status ge) s →
     103  RTLabs_cost s = true.
     104#ge
     105cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #H
     106*
     107[ * #func #locals #next #nok #b #r #fs #m
     108  whd in ⊢ (% → ??%?); whd in ⊢ (?(??%?) → ?);
     109  cases (lookup_present ?? (f_graph func) ??) normalize //
     110  #A try #B try #C try #D try #E try #F try #G try #I try #J cases (H ?) //
     111| *: normalize #A #B try #C try #D try #E try #F cases (H ?) //
    60112] qed.
    61113
     
    63115  RTLabs_cost s = false →
    64116  ¬ as_costed (RTLabs_status ge) s.
    65 #ge #s #E % whd in ⊢ (% → ?); >E #E' destruct
    66 qed.
     117#ge *
     118[ * #func #locals #next #nok #b #r #fs #m
     119  whd in ⊢ (??%? → ?%); whd in ⊢ (? → ?(?(??%?)));
     120  cases (lookup_present ?? (f_graph func) ??) normalize
     121  #A try #B try #C try #D try #E try #F try #G try #H try #I destruct
     122  % * #J @J @refl
     123| *: normalize #A #B try #C try #D try #E try #F % * #G @G @refl
     124] qed.
    67125
    68126(* Before attempting to construct a structured trace, let's show that we can
     
    550608  >Estmt #LP whd in ⊢ (??%? → ?);
    551609  (* replace with lemma on successors? *)
    552   @bind_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
     610  @bind_res_value #v #Ev @bind_ok * #Eb whd in ⊢ (??%? → ?); #E destruct
    553611  lapply (Hbody (next fr) (next_ok fr))
    554612  generalize in ⊢ (???% → ?);
     
    561619  >Estmt #LP whd in ⊢ (??%? → ?);
    562620  (* replace with lemma on successors? *)
    563   @bind_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
     621  @bind_res_value #a cases a [ | #sz #i | #f | #r | #ptr ]  #Ea whd in ⊢ (??%? → ?);
    564622  [ 2: (* later *)
    565623  | *: #E destruct
     
    598656cases fd
    599657[ #fn whd in ⊢ (??%? → % → ?);
    600   @bind_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any)
     658  @bind_res_value #lcl #Elcl cases (alloc ? m O (f_stacksize fn) Any)
    601659  #m' #b whd in ⊢ (??%? → ?); #E' destruct
    602660  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
     
    703761  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
    704762    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
    705   | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
     763  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_res_value #locals #El #EV
    706764    whd in EV:(??%?); destruct @(sp_finished ? f) //
    707765    cases f //
     
    9461004let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
    9471005  replace_sub_trace … r ?
    948     (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r)
     1006    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) ?) (stack_ok … r)
    9491007
    9501008] TERMINATES_IN_TIME
     
    9781036        match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    9791037        (* We're about to run into a label. *)
    980         [ true ⇒ λCS.
     1038        [ true ⇒ λCS. 
    9811039            mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?
    9821040              doesnt_end_with_ret
    9831041              (mk_trace_result ge … next trace' ?
    984                 (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??)
     1042                (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) ??)
    9851043        (* An ordinary step, keep going. *)
    9861044        | false ⇒ λCS.
     
    10061064            (mk_trace_result ge …
    10071065              (tal_base_call (RTLabs_status ge) start next (new_state … r)
    1008                 ? CL ? (new_trace … r) CS) ??)
     1066                ? CL ? (new_trace … r) (RTLabs_costed … CS)) ??)
    10091067        (* otherwise use step case *)
    10101068        | false ⇒ λCS.
     
    10411099| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ //
    10421100| @(stack_preserved_join … (stack_ok … r)) //
    1043 | @(trace_label_label_label … (new_trace … r))
     1101| @(costed_RTLabs ge) @(trace_label_label_label … (new_trace … r))
    10441102| cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_
    10451103  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
     
    10531111| @le_n
    10541112| //
     1113| @RTLabs_costed //
    10551114| @le_S_S_to_le @TERMINATES_IN_TIME
    10561115| @(wrl_nonzero … TERMINATES_IN_TIME)
     
    10711130| %{tr} @EV
    10721131| %1 whd @CL
    1073 | @(well_cost_labelled_jump … EV) //
     1132| @RTLabs_costed @(well_cost_labelled_jump … EV) //
    10741133| @(well_cost_labelled_state_step  … EV) //
    10751134| whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} %
     
    12361295[ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    12371296| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1238 | #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1239 | #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1240 | #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1241 | #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1242 | #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1243 | #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1244 | #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
    1245 | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
    1246 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
     1297| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     1298| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     1299| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     1300| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     1301| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     1302| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     1303| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % //
     1304| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct %2 cases b [ %{l1} | %{l2} ] % // [ % | %2 %] //
     1305| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
    12471306  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ]
    12481307  whd in ⊢ (??%? → ?);
     
    12521311  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
    12531312  ]
    1254 | #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
     1313| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
    12551314] qed.
    12561315
     
    13281387[ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
    13291388| #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl
    1330 | #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    1331 | #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    1332 | #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    1333 | #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
    1334 | #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
    1335 | #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
    1336 | #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
    1337 | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
    1338 | #r #ls #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev
     1389| #ty #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1390| #ty #ty' #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1391| #ty1 #ty2 #ty' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1392| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #locals' #El whd in ⊢ (??%? → ?); #E destruct @refl
     1393| #ch #r1 #r2 #l  #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #m' #Em whd in ⊢ (??%? → ?); #E destruct @refl
     1394| #id #rs #r #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
     1395| #r #rs #r' #l #LP whd in ⊢ (??%? → ?); @bind_res_value #fv #Efv @bind_ok #fd #Efd @bind_ok #vs #Evs whd in ⊢ (??%? → ?); #E destruct @refl
     1396| #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb whd in ⊢ (??%? → ?); #E destruct @refl
     1397| #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev
    13391398  cases v [ #E normalize in E; destruct | #sz #i | #f #E normalize in E; destruct | #r #E normalize in E; destruct | #p #E normalize in E; destruct ]
    13401399  whd in ⊢ (??%? → ?);
     
    13441403  | #l #El whd in ⊢ (??%? → ?); #E destruct @refl
    13451404  ]
    1346 | #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
     1405| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct @refl
    13471406] qed.
    13481407
     
    15991658            match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
    16001659            [ true ⇒ λCS.
    1601                 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK'
     1660                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed … CS)) trace' TRACE_OK'
    16021661            | false ⇒ λCS.
    16031662                let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
     
    16131672                let TRACE_OK' ≝ ? in
    16141673                match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with
    1615                 [ 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'
     1674                [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) (RTLabs_costed … CS)) (remainder … tlr) TRACE_OK'
    16161675                | false ⇒ λCS.
    16171676                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
     
    16311690| @(absurd ?? (ro_no_termination … TRACE_OK))
    16321691     %{0} % @wr_base //
    1633 | @(well_cost_labelled_jump … EV) /2/
     1692| @RTLabs_costed @(well_cost_labelled_jump … EV) /2/
    16341693| 5,6,8,9,10,11: /3/
    16351694| % [ @(well_cost_labelled_state_step … EV) /2/
     
    17401799    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
    17411800        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    1742             tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T'
     1801            tld_step (RTLabs_status ge) s s' (tll_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) T'
    17431802(*
    17441803        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
     
    17481807    | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
    17491808        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    1750             tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T'
     1809            tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T (RTLabs_costed … STATEMENT_COSTLABEL)) ?? T'
    17511810(*
    17521811        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
     
    17561815    ] STATEMENT_COSTLABEL
    17571816].
    1758 [ @(trace_any_label_label … T)
     1817[ @(costed_RTLabs ge) @(trace_any_label_label … T)
    17591818| %{tr} @EV
    17601819| @(trace_any_call_call … T)
     
    19051964
    19061965(* Extract a flat trace from a structured one. *)
    1907 let rec flatten_trace_label_return ge s s'
     1966let rec flat_trace_of_label_return ge s s'
    19081967  (tr:trace_label_return (RTLabs_status ge) s s')
    19091968on tr :
    19101969  partial_flat_trace io_out io_in ge s s' ≝
    19111970match tr with
    1912 [ tlr_base s1 s2 tll ⇒ flatten_trace_label_label ge ends_with_ret s1 s2 tll
     1971[ tlr_base s1 s2 tll ⇒ flat_trace_of_label_label ge ends_with_ret s1 s2 tll
    19131972| tlr_step s1 s2 s3 tll tlr ⇒
    19141973  append_partial_flat_trace …
    1915     (flatten_trace_label_label ge doesnt_end_with_ret s1 s2 tll)
    1916     (flatten_trace_label_return ge s2 s3 tlr)
     1974    (flat_trace_of_label_label ge doesnt_end_with_ret s1 s2 tll)
     1975    (flat_trace_of_label_return ge s2 s3 tlr)
    19171976]
    1918 and flatten_trace_label_label ge ends s s'
     1977and flat_trace_of_label_label ge ends s s'
    19191978  (tr:trace_label_label (RTLabs_status ge) ends s s')
    19201979on tr :
    19211980  partial_flat_trace io_out io_in ge s s' ≝
    19221981match tr with
    1923 [ tll_base e s1 s2 tal _ ⇒ flatten_trace_any_label ge e s1 s2 tal
     1982[ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal
    19241983]
    1925 and flatten_trace_any_label ge ends s s'
     1984and flat_trace_of_any_label ge ends s s'
    19261985  (tr:trace_any_label (RTLabs_status ge) ends s s')
    19271986on tr :
     
    19351994    pft_base … EX' ]
    19361995| tal_base_call s1 s2 s3 EX CL AR tlr CS ⇒
    1937     let suffix' ≝ flatten_trace_label_return ge ?? tlr in
     1996    let suffix' ≝ flat_trace_of_label_return ge ?? tlr in
    19381997    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    19391998    pft_step … EX' suffix' ]
     
    19422001    pft_step … EX'
    19432002      (append_partial_flat_trace …
    1944         (flatten_trace_label_return ge ?? tlr)
    1945         (flatten_trace_any_label ge ??? tal))
     2003        (flat_trace_of_label_return ge ?? tlr)
     2004        (flat_trace_of_any_label ge ??? tal))
    19462005    ]
    19472006| tal_step_default ends s1 s2 s3 EX tal CL CS ⇒
    19482007    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    1949       pft_step … EX' (flatten_trace_any_label ge ??? tal)
     2008      pft_step … EX' (flat_trace_of_any_label ge ??? tal)
    19502009    ]
    19512010].
     
    19542013(* We take an extra step so that we can always return a non-empty trace to
    19552014   satisfy the guardedness condition in the cofixpoint. *)
    1956 let rec flatten_trace_any_call ge s s' s'' et
     2015let rec flat_trace_of_any_call ge s s' s'' et
    19572016  (tr:trace_any_call (RTLabs_status ge) s s')
    19582017  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
     
    19652024    pft_step … EX'
    19662025      (append_partial_flat_trace …
    1967         (flatten_trace_label_return ge ?? tlr)
    1968         (flatten_trace_any_call ge … tac EX''))
     2026        (flat_trace_of_label_return ge ?? tlr)
     2027        (flat_trace_of_any_call ge … tac EX''))
    19692028    ]
    19702029| tac_step_default s1 s2 s3 EX tal CL CS ⇒ λEX''.
    19712030    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    19722031    pft_step … EX'
    1973      (flatten_trace_any_call ge … tal EX'')
     2032     (flat_trace_of_any_call ge … tal EX'')
    19742033    ]
    19752034] EX''.
    19762035
    1977 let rec flatten_trace_label_call ge s s' s'' et
     2036let rec flat_trace_of_label_call ge s s' s'' et
    19782037  (tr:trace_label_call (RTLabs_status ge) s s')
    19792038  (EX'':eval_statement ge s' = Value … 〈et,s''〉)
     
    19812040  partial_flat_trace io_out io_in ge s s'' ≝
    19822041match tr with
    1983 [ tlc_base s1 s2 tac CS ⇒ flatten_trace_any_call … tac
     2042[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
    19842043] EX''.
    19852044
     
    19872046   to take care to satisfy the guardedness condition by witnessing the fact that
    19882047   the partial traces are non-empty. *)
    1989 let corec flatten_trace_label_diverges ge s
     2048let corec flat_trace_of_label_diverges ge s
    19902049  (tr:trace_label_diverges (RTLabs_status ge) s)
    19912050: flat_trace io_out io_in ge s ≝
    19922051match tr with
    19932052[ tld_step sx sy tll tld ⇒
    1994     match flatten_trace_label_label ge … tll with
    1995     [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flatten_trace_label_diverges ge ? tld)
     2053    match flat_trace_of_label_label ge … tll with
     2054    [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
    19962055    | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld)
    19972056    ] tld
    19982057| tld_base s1 s2 s3 tlc EX CL tld ⇒
    19992058    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    2000       match flatten_trace_label_call … tlc EX' with
    2001       [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flatten_trace_label_diverges ge ? tld)
     2059      match flat_trace_of_label_call … tlc EX' with
     2060      [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld)
    20022061      | pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld)
    20032062      ] tld
     
    20112070: flat_trace io_out io_in ge s ≝
    20122071match ptr with
    2013 [ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flatten_trace_label_diverges ge s' tr)
     2072[ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flat_trace_of_label_diverges ge s' tr)
    20142073| pft_step s1 et s2 s3 EX tr' ⇒ λtr. ft_step … EX (add_partial_flat_trace … tr' tr)
    20152074] tr
     
    20722131  (str:trace_label_diverges (RTLabs_status ge) s)
    20732132  (tr:flat_trace io_out io_in ge s)
    2074 : equal_flat_traces … (flatten_trace_label_diverges … str) tr ≝ ?.
     2133: equal_flat_traces … (flat_trace_of_label_diverges … str) tr ≝ ?.
    20752134@flat_traces_are_determined_by_starting_point
    20762135qed.
    20772136
    2078 let rec flatten_trace_whole_program ge s
     2137let rec flat_trace_of_whole_program ge s
    20792138  (tr:trace_whole_program (RTLabs_status ge) s)
    20802139on tr : flat_trace io_out io_in ge s ≝
     
    20822141[ twp_terminating s1 s2 sf CL EX tlr F ⇒
    20832142    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    2084       ft_step … EX' (partial_to_flat_trace … (flatten_trace_label_return … tlr) (ft_stop … sf F))
     2143      ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … sf F))
    20852144    ]
    20862145| twp_diverges s1 s2 CL EX tld ⇒
    20872146    match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒
    2088       ft_step … EX' (flatten_trace_label_diverges … tld)
     2147      ft_step … EX' (flat_trace_of_label_diverges … tld)
    20892148    ]
    20902149].
     
    20932152  (str:trace_whole_program (RTLabs_status ge) s)
    20942153  (tr:flat_trace io_out io_in ge s)
    2095 : equal_flat_traces … (flatten_trace_whole_program … str) tr ≝ ?.
     2154: equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
    20962155@flat_traces_are_determined_by_starting_point
    20972156qed.
Note: See TracChangeset for help on using the changeset viewer.