Changeset 1812 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Mar 8, 2012, 12:13:11 PM (8 years ago)
Author:
campbell
Message:

Provide a combined type for terminating and non-terminating structured
traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1808 r1812  
    15701570  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    15711571  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
    1572   (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
    15731572  (LABEL_LIMIT: state_bound_on_steps_to_cost s n)
    15741573  on n : finite_prefix ge s ≝
     
    15861585                fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK'
    15871586            | false ⇒ λCS.
    1588                 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
     1587                let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    15891588                fp_add_default ge ?? CL fs ? CS
    15901589            ] (refl ??)
     
    16001599                [ 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'
    16011600                | false ⇒ λCS.
    1602                     let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
     1601                    let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    16031602                    fp_add_terminating_call … fs (new_trace … tlr) ? CS
    16041603                ] (refl ??)
     
    16251624    ]
    16261625| /2/
    1627 | @(soundly_labelled_state_preserved … (stack_ok … tlr))
    1628   @(soundly_labelled_state_step … EV) /2/
    16291626| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
    16301627  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
     
    16681665    | @(not_return_to_not_final … EV) >CL % #E destruct
    16691666    ]
    1670 | 20,21,22: /2/
    1671 | @(soundly_labelled_state_step … EV) /2/
     1667| 19,20,21: /2/
    16721668| cases (bound_after_step … LABEL_LIMIT EV ?)
    16731669  [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 // |
     
    17191715  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    17201716  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
    1721   (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)
    17221717  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    17231718  : trace_label_diverges_exists (RTLabs_status ge) s ≝
    1724 match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLED with
     1719match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with
    17251720[ ex_intro n B ⇒
    1726     match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED STATE_SOUNDLY_LABELLED B
     1721    match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B
    17271722      return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s
    17281723    with
    17291724    [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL.
    1730         let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
     1725        let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    17311726            tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T'
    17321727(*
    1733         match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
     1728        match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
    17341729        [ ex_intro T' _ ⇒
    17351730            ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I
    17361731        ]*)
    17371732    | fp_tac s s2 s3 tr T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.
    1738         let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? in
     1733        let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in
    17391734            tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T'
    17401735(*
    1741         match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?? with
     1736        match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with
    17421737        [ ex_intro T' _ ⇒
    17431738            ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ?
     
    17451740    ] STATEMENT_COSTLABEL
    17461741].
    1747 [ /2/
    1748 | @(trace_any_label_label … T)
     1742[ @(trace_any_label_label … T)
    17491743| %{tr} @EV
    17501744| @(trace_any_call_call … T)
    1751 | /2/
    17521745| @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)
    17531746] qed.
     1747
     1748let rec whole_structured_trace_exists ge s
     1749  (trace: flat_trace io_out io_in ge s)
     1750  (ORACLE: termination_oracle)
     1751  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
     1752  (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge)
     1753  : ∀IS_CALL: RTLabs_classify s = cl_call.
     1754    ∀NOT_WRONG: not_wrong … s trace.
     1755    ∀STATE_COSTLABELLED: well_cost_labelled_state s.
     1756    ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s.
     1757    trace_whole_program_exists (RTLabs_status ge) s ≝
     1758match trace return λs,trace. RTLabs_classify s = cl_call →
     1759                             not_wrong … s trace →
     1760                             well_cost_labelled_state s →
     1761                             soundly_labelled_state s →
     1762                             trace_whole_program_exists (RTLabs_status ge) s with
     1763[ ft_step s tr next EV trace' ⇒ λIS_CALL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.
     1764    match ORACLE ge O next trace' with
     1765    [ or_introl TERMINATES ⇒
     1766        match TERMINATES with
     1767        [ witness TERMINATES ⇒
     1768          let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in
     1769          twp_terminating (RTLabs_status ge) s next (new_state … tlr) IS_CALL ? (new_trace … tlr)
     1770        ]
     1771    | or_intror NO_TERMINATION ⇒
     1772        twp_diverges (RTLabs_status ge) s next IS_CALL ?
     1773         (make_label_diverges ge next trace' ORACLE ?
     1774            ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?)
     1775    ]
     1776| ft_stop st FINAL ⇒ λIS_CALL,NOT_WRONG. ⊥
     1777| ft_wrong start m EV ⇒ λIS_CALL,NOT_WRONG. ⊥
     1778].
     1779[ cases (rtlabs_call_inv … IS_CALL) #fn * #args * #dst * #stk * #m #E destruct
     1780  cases FINAL #E @E @refl
     1781| %{tr} @EV
     1782| @(well_cost_labelled_state_step … EV) //
     1783| @(well_cost_labelled_call … EV) //
     1784| %{tr} @EV
     1785| @(well_cost_labelled_call … EV) //
     1786| % [ @(well_cost_labelled_state_step … EV) //
     1787    | @(soundly_labelled_state_step … EV) //
     1788    | @(not_to_not … NO_TERMINATION) * #d * #TM % /2/
     1789    | @(still_not_wrong … NOT_WRONG)
     1790    | @(not_return_to_not_final … EV) >IS_CALL % #E destruct
     1791    ]
     1792| inversion NOT_WRONG #H29 #H30 #H31 #H32 #H33 try #H35 try #H36 try #H37 destruct
     1793] qed.
     1794
     1795definition well_cost_labelled_program : RTLabs_program → Prop ≝
     1796  λp. All ? (λx. let 〈id,fd〉 ≝ x in
     1797                 match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p).
     1798(*
     1799theorem program_trace_exists :
     1800  termination_oracle →
     1801  ∀p:RTLabs_program.
     1802  ∀s:state.
     1803  ∀I: make_initial_state p = OK ? s.
     1804 
     1805  let plain_trace ≝ exec_inf io_out io_in RTLabs_fullexec p in
     1806 
     1807  ∀NOIO:exec_no_io … plain_trace.
     1808 
     1809  let flat_trace ≝ make_whole_flat_trace p s NOIO I in
     1810 
     1811  trace_whole_program_exists (RTLabs_status (make_global p)) s.
     1812#ORACLE #p #s #I
     1813letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
     1814#NOIO
     1815letin flat_trace ≝ (make_whole_flat_trace p s NOIO I)
     1816whd
     1817@(whole_structured_trace_exists … flat_trace)
     1818//
     1819[ whd
     1820*)
Note: See TracChangeset for help on using the changeset viewer.