Changeset 1574


Ignore:
Timestamp:
Nov 28, 2011, 5:57:47 PM (8 years ago)
Author:
campbell
Message:

A little more progress on traces on RTLabs.

Location:
src
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1565 r1574  
    277277
    278278(* We require that labels appear after branch instructions and at the start of
    279    functions. *)
     279   functions.  The first is required for preciseness, the latter for soundness.
     280   We will make a separate requirement for there to be a finite number of steps
     281   between labels to catch loops for soundness (is this sufficient?). *)
    280282
    281283definition is_cost_label : statement → Prop ≝
     
    321323].
    322324
     325(* Don't need to know that labels break loops because we have termination. *)
     326
     327record make_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
     328  new_state : state;
     329  termination_count : nat;
     330  remainder : flat_trace io_out io_in ge new_state;
     331  terminates : nth_is_return ge termination_count O new_state remainder;
     332  cost_labelled : well_cost_labelled_state new_state;
     333  new_trace : T new_state
     334}.
     335
     336definition replace_new_trace : ∀ge,T1,T2.
     337  ∀r:make_result ge T1. T2 (new_state … r) → make_result ge T2 ≝
     338λge,T1,T2,r,trace.
     339  mk_make_result ge T2
     340    (new_state … r)
     341    (termination_count … r)
     342    (remainder … r)
     343    (terminates … r)
     344    (cost_labelled … r)
     345    trace.
     346
    323347let rec make_label_return n ge s
    324348  (trace: flat_trace io_out io_in ge s)
    325349  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    326   (STATE_COSTLABELLED: well_cost_labelled_state s)
     350  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
     351  (STATEMENT_COSTLABEL: RTLabs_cost s)              (* current statement is a cost label *)
    327352  (TERMINATES: nth_is_return ge n O s trace)
    328   : Σs'.Σremainder:flat_trace io_out io_in ge s'.
    329       trace_label_return (RTLabs_status ge) s s' ≝
    330 ?.
     353  : make_result ge (trace_label_return (RTLabs_status ge) s) ≝
     354
     355  let r ≝ make_label_label n ge s trace ???? in
     356  match new_trace … r with
     357  [ dp ends tll ⇒
     358    match ends return λx. trace_label_label ? x ?? → ? with
     359    [ ends_with_ret ⇒ λtll.
     360        replace_new_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
     361    | doesnt_end_with_ret ⇒ λtll.
     362        let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
     363                   (remainder … r) ??? (terminates … r) in
     364          replace_new_trace … r'
     365            (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
     366    ] tll
     367  ]
     368
     369and make_label_label n ge s
     370  (trace: flat_trace io_out io_in ge s)
     371  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     372  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
     373  (STATEMENT_COSTLABEL: RTLabs_cost s)              (* current statement is a cost label *)
     374  (TERMINATES: nth_is_return ge n O s trace)
     375  : make_result ge (λs'. Σends. trace_label_label (RTLabs_status ge) ends s s') ≝
     376let r ≝ make_any_label n ge s trace ??? in
     377match new_trace … r with
     378[ dp ends tr ⇒
     379  replace_new_trace ??? r
     380    (dp ?? ends (tll_base (RTLabs_status ge) ends s (new_state … r) tr STATEMENT_COSTLABEL))
     381]
     382
     383and make_any_label n ge s
     384  (trace: flat_trace io_out io_in ge s)
     385  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     386  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
     387  (TERMINATES: nth_is_return ge n O s trace)
     388  : make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') ≝
     389match trace return λs,trace. nth_is_return ???? trace → make_result ge (λs'. Σends. trace_any_label (RTLabs_status ge) ends s s') with
     390[ ft_stop st FINAL ⇒ λTERMINATES. ?
     391| ft_step start tr next EV trace' ⇒ λTERMINATES. ?
     392| ft_wrong start m EV ⇒ λTERMINATES. ⊥
     393] TERMINATES.
     394
     395[ //
     396| //
     397| @(trace_label_label_label … tll)
     398| //
     399| //
     400| //
     401| //
     402| //
     403| //
     404| //
     405|
     406|
     407| inversion TERMINATES
     408  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 -TERMINATES destruct
     409  | #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 -TERMINATES destruct
     410  | #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 -TERMINATES destruct
     411  | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 -TERMINATES destruct
     412 
     413(* Now we're in trouble - if we're at the end of the function we don't have the
     414   required guarantee that we can make another step.  In particular, there isn't
     415   one at the end of the program. *)
  • src/common/StructuredTraces.ma

    r1544 r1574  
    131131        ¬ (as_costed S status_pre) →
    132132          trace_any_call S status_pre status_end.
     133
     134let rec trace_any_label_label S s s' f
     135  (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝
     136match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
     137[ tal_base_not_return start final _ _ C ⇒ C
     138| tal_base_return _ _  _ _ ⇒ I
     139| tal_step_call f pre start after final X C RET LR tr' ⇒ trace_any_label_label … tr'
     140| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
     141].
     142
     143lemma trace_label_label_label : ∀S,s,s',f.
     144  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
     145#S #s #s' #f #tr
     146cases tr
     147#f #start #end #tr' #C @(trace_any_label_label … tr')
     148qed.
     149
Note: See TracChangeset for help on using the changeset viewer.