Changeset 1712


Ignore:
Timestamp:
Feb 21, 2012, 11:58:07 AM (8 years ago)
Author:
campbell
Message:

Show that constructing an RTLabs structure trace really does use a prefix of the flat trace.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1707 r1712  
    8888[ #H105 #H106 #H107 #H108 #H109 destruct
    8989| #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct //
     90] qed.
     91
     92inductive flat_trace_prefix (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s,s'. flat_trace o i ge s → flat_trace o i ge s' → Prop ≝
     93| ftp_refl : ∀s,t. flat_trace_prefix o i ge s s t t
     94| ftp_step : ∀s1,tr,s2,s3,t2,t3,EV.
     95    flat_trace_prefix o i ge s2 s3 t2 t3 →
     96    flat_trace_prefix o i ge s1 s3 (ft_step o i ge s1 tr s2 EV t2) t3
     97.
     98
     99lemma concatenate_flat_trace_prefix : ∀o,i,ge,s1,s2,s3,t1,t2,t3.
     100  flat_trace_prefix o i ge s1 s2 t1 t2 →
     101  flat_trace_prefix o i ge s2 s3 t2 t3 →
     102  flat_trace_prefix o i ge s1 s3 t1 t3.
     103#o #i #ge #s1 #s2 #s3 #t1 #t2 #t3 #p1 elim p1
     104[ //
     105| #s1' #tr #s2' #s3' #t2' #t3' #EV #p2 #IH #p3
     106  %2 /2/
    90107] qed.
    91108
     
    596613   termination.  Note that we keep a proof that our upper bound on the length
    597614   of the termination proof is respected. *)
    598 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
     615record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (full:flat_trace io_out io_in ge start) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
    599616  new_state : state;
    600617  remainder : flat_trace io_out io_in ge new_state;
     618  is_remainder : flat_trace_prefix … full remainder;
    601619  cost_labelled : well_cost_labelled_state new_state;
    602620  new_trace : T new_state;
     
    610628(* The same with a flag indicating whether the function returned, as opposed to
    611629   encountering a label. *)
    612 record sub_trace_result (ge:genv) (depth:nat) (start:state) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
     630record sub_trace_result (ge:genv) (depth:nat) (start:state) (full:flat_trace io_out io_in ge start) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
    613631  ends : trace_ends_with_ret;
    614   trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) ends start (T ends) limit
     632  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) ends start full (T ends) limit
    615633}.
    616634
     
    619637   the size of the termination proof might need to be relaxed, too. *)
    620638
    621 definition replace_trace : ∀ge,d,e1,e2,s1,s2,T1,T2,l1,l2. l2 ≥ l1 →
    622   ∀r:trace_result ge d e1 s1 T1 l1. T2 (new_state … r) → stack_preserved e2 s2 (new_state … r) → trace_result ge d e2 s2 T2 l2 ≝
    623 λge,d,e1,e2,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP.
    624   mk_trace_result ge d e2 s2 T2 l2
     639definition replace_trace : ∀ge,d,e1,e2,s1,s2,t1,t2,T1,T2,l1,l2. l2 ≥ l1 →
     640  ∀r:trace_result ge d e1 s1 t1 T1 l1.
     641    (∀s,t. flat_trace_prefix … s1 s t1 t → flat_trace_prefix … s2 s t2 t) →
     642    T2 (new_state … r) →
     643    stack_preserved e2 s2 (new_state … r) →
     644    trace_result ge d e2 s2 t2 T2 l2 ≝
     645λge,d,e1,e2,s1,s2,t1,t2,T1,T2,l1,l2,lGE,r,PRE,trace,SP.
     646  mk_trace_result ge d e2 s2 t2 T2 l2
    625647    (new_state … r)
    626648    (remainder … r)
     649    (PRE ?? (is_remainder ??????? r))
    627650    (cost_labelled … r)
    628651    trace
     
    630653    (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
    631654                        match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with
    632      [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ?????? r))
    633 . @(transitive_le … lGE) @(pi2 … TM) qed.
    634 
    635 definition replace_sub_trace : ∀ge,d,s1,s2,T1,T2,l1,l2. l2 ≥ l1 →
    636   ∀r:sub_trace_result ge d s1 T1 l1. T2 (ends … r) (new_state … r) → stack_preserved (ends … r) s2 (new_state … r) → sub_trace_result ge d s2 T2 l2 ≝
    637 λge,d,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP.
    638   mk_sub_trace_result ge d s2 T2 l2
     655     [O ⇒ λ_. I | _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ??????? r))
     656.
     657@(transitive_le … lGE) @(pi2 … TM) qed.
     658
     659definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,T1,T2,l1,l2. l2 ≥ l1 →
     660  ∀r:sub_trace_result ge d s1 t1 T1 l1.
     661    (∀s,t. flat_trace_prefix … s1 s t1 t → flat_trace_prefix … s2 s t2 t) →
     662    T2 (ends … r) (new_state … r) →
     663    stack_preserved (ends … r) s2 (new_state … r) →
     664    sub_trace_result ge d s2 t2 T2 l2 ≝
     665λge,d,s1,s2,t1,t2,T1,T2,l1,l2,lGE,r,PRE,trace,SP.
     666  mk_sub_trace_result ge d s2 t2 T2 l2
    639667    (ends … r)
    640     (replace_trace … lGE … r trace SP).
     668    (replace_trace … lGE … r PRE trace SP).
    641669
    642670(* Small syntax hack to avoid ambiguous input problems. *)
     
    651679  (TIME: nat)
    652680  (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES))))
    653   on TIME : trace_result ge depth ends_with_ret s
     681  on TIME : trace_result ge depth ends_with_ret s trace
    654682              (trace_label_return (RTLabs_status ge) s)
    655683              (will_return_length … TERMINATES) ≝
     
    666694            TERMINATES
    667695            TIME ? in
    668   match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) x s (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
     696  match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) x s trace (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s trace (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with
    669697  [ ends_with_ret ⇒ λr.
    670       replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
     698      replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)
    671699  | doesnt_end_with_ret ⇒ λr.
    672700      let r' ≝ make_label_return ge depth (new_state … r)
     
    675703                 (cost_labelled … r) ?
    676704                 (pi1 … (terminates … r)) TIME ? in
    677         replace_trace … r'
     705        replace_trace … r' ?
    678706          (tlr_step (RTLabs_status ge) s (new_state … r)
    679707            (new_state … r') (new_trace … r) (new_trace … r')) ?
     
    691719  (TIME: nat)
    692720  (TERMINATES_IN_TIME:  myge TIME (plus 1 (times 3 (will_return_length … TERMINATES))))
    693   on TIME : sub_trace_result ge depth s
     721  on TIME : sub_trace_result ge depth s trace
    694722              (λends. trace_label_label (RTLabs_status ge) ends s)
    695723              (will_return_length … TERMINATES) ≝
     
    700728
    701729let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
    702   replace_sub_trace … r
     730  replace_sub_trace … r ?
    703731    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r)
    704732
     
    713741  (TIME: nat)
    714742  (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES)))
    715   on TIME : sub_trace_result ge depth s
     743  on TIME : sub_trace_result ge depth s trace
    716744              (λends. trace_any_label (RTLabs_status ge) ends s)
    717745              (will_return_length … TERMINATES) ≝
     
    721749| S TIME ⇒ λTERMINATES_IN_TIME.
    722750
    723   match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth s (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
     751  match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth s trace (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with
    724752  [ ft_stop st FINAL ⇒
    725753      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
    726754
    727755  | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME.
    728     match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
     756    match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with
    729757    [ cl_other ⇒ λCL.
    730         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
     758        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
    731759        (* We're about to run into a label. *)
    732760        [ true ⇒ λCS.
    733             mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
     761            mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?
    734762              doesnt_end_with_ret
    735               (mk_trace_result ge … next trace' ?
     763              (mk_trace_result ge … next trace' ??
    736764                (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??)
    737765        (* An ordinary step, keep going. *)
    738766        | false ⇒ λCS.
    739767            let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in
    740                 replace_sub_trace … r
     768                replace_sub_trace … r ?
    741769                  (tal_step_default (RTLabs_status ge) (ends … r)
    742770                     start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ?
     
    744772       
    745773    | cl_jump ⇒ λCL.
    746         mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
     774        mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?
    747775          doesnt_end_with_ret
    748           (mk_trace_result ge ????? next trace' ?
     776          (mk_trace_result ge ?????? next trace' ??
    749777            (tal_base_not_return (RTLabs_status ge) start next ???) ??)
    750778           
    751779    | cl_call ⇒ λCL.
    752780        let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in
    753         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
     781        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
    754782        (* We're about to run into a label, use base case for call *)
    755783        [ true ⇒ λCS.
    756             mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
     784            mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?
    757785            doesnt_end_with_ret
    758             (replace_trace … r
     786            (replace_trace … r ?
    759787              (tal_base_call (RTLabs_status ge) start next (new_state … r)
    760788                ? CL ? (new_trace … r) CS) ?)
     
    764792                       (new_state … r) (remainder … r) ENV_COSTLABELLED ?
    765793                       (pi1 … (terminates … r)) TIME ? in
    766             replace_sub_trace … r'
     794            replace_sub_trace … r' ?
    767795              (tal_step_call (RTLabs_status ge) (ends … r')
    768796                start next (new_state … r) (new_state … r') ? CL ?
     
    771799
    772800    | cl_return ⇒ λCL.
    773         mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?
     801        mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?
    774802          ends_with_ret
    775           (mk_trace_result ge ?????
     803          (mk_trace_result ge ??????
    776804            next
    777805            trace'
     806            ?
    778807            ?
    779808            (tal_base_return (RTLabs_status ge) start next ? CL)
     
    789818[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
    790819| //
    791 | cases r #H1 #H2 #H3 #H4 #H5 * #H6 @le_S_to_le
     820| //
     821| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 @le_S_to_le
     822| #s0 #t @concatenate_flat_trace_prefix @(is_remainder … r)
    792823| @(stack_preserved_join … (stack_ok … r)) //
    793824| @(trace_label_label_label … (new_trace … r))
    794 | cases r #H1 #H2 #H3 #H4 #H5 * #H6 #LT
     825| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 #LT
    795826  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    796827  @(transitive_le …  (3*(will_return_length … TERMINATES)))
     
    802833| cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
    803834| @le_n
     835| //
    804836| @le_S_S_to_le @TERMINATES_IN_TIME
    805837| @(wrl_nonzero … TERMINATES_IN_TIME)
     
    810842| %{tr} @EV
    811843| @(well_cost_labelled_state_step  … EV) //
     844| %2 %1
    812845| whd @(will_return_notfn … TERMINATES) %2 @CL
    813846| @stack_preserved_step /2/
     
    816849| @(well_cost_labelled_jump … EV) //
    817850| @(well_cost_labelled_state_step  … EV) //
     851| %2 %1
    818852| @(stack_preserved_call … EV (stack_ok … r)) //
    819853| %{tr} @EV
    820854| @RTLabs_after_call //
     855| #s0 #t #p %2 @p
    821856| cases (will_return_call … TERMINATES) #H @le_S_to_le
    822 | cases r #H1 #H2 #H3 #H4 #H5 * #H6
     857| cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7
    823858  cases (will_return_call … CL TERMINATES)
    824859  #TM #X #Y @le_S_to_le @(transitive_lt … Y X)
     860| #s0 #t #p1 %2 @(concatenate_flat_trace_prefix … p1) @(is_remainder … r)
    825861| @RTLabs_after_call //
    826862| %{tr} @EV
    827863| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
    828864| @(cost_labelled … r)
    829 | cases r #H72 #H73 #H74 #H75 #HX * #H76 #H78
     865| cases r #H72 #H73 #H74 #H75 #HX #HY * #H76 #H78
    830866  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    831867  cases (will_return_call … TERMINATES) in H78;
     
    848884| %2 whd @CL
    849885| @(well_cost_labelled_state_step  … EV) //
     886| %2 %1
    850887| cases (will_return_notfn … TERMINATES) #TM @le_S_to_le
     888| #s0 #t #p %2 @p
    851889| @CL
    852890| %{tr} @EV
     
    874912  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    875913  (TERMINATES: will_return ge depth s trace)
    876   : trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
     914  : trace_result ge depth ends_with_ret s trace (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝
    877915make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES
    878916  (2 + 3 * will_return_length … TERMINATES) ?.
Note: See TracChangeset for help on using the changeset viewer.