 Timestamp:
 Mar 8, 2012, 12:13:11 PM (8 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1808 r1812 1570 1570 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1571 1571 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) 1572 (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)1573 1572 (LABEL_LIMIT: state_bound_on_steps_to_cost s n) 1574 1573 on n : finite_prefix ge s ≝ … … 1586 1585 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' TRACE_OK' 1587 1586  false ⇒ λCS. 1588 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? ?in1587 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1589 1588 fp_add_default ge ?? CL fs ? CS 1590 1589 ] (refl ??) … … 1600 1599 [ 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' 1601 1600  false ⇒ λCS. 1602 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? ?in1601 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1603 1602 fp_add_terminating_call … fs (new_trace … tlr) ? CS 1604 1603 ] (refl ??) … … 1625 1624 ] 1626 1625  /2/ 1627  @(soundly_labelled_state_preserved … (stack_ok … tlr))1628 @(soundly_labelled_state_step … EV) /2/1629 1626  @(bound_after_call ge … LABEL_LIMIT CL ? CS) 1630 1627 @(RTLabs_after_call … CL EV) @(stack_ok … tlr) … … 1668 1665  @(not_return_to_not_final … EV) >CL % #E destruct 1669 1666 ] 1670  20,21,22: /2/ 1671  @(soundly_labelled_state_step … EV) /2/ 1667  19,20,21: /2/ 1672 1668  cases (bound_after_step … LABEL_LIMIT EV ?) 1673 1669 [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 //  … … 1719 1715 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1720 1716 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) 1721 (STATE_SOUNDLY_LABELLED: soundly_labelled_state s)1722 1717 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 1723 1718 : trace_label_diverges_exists (RTLabs_status ge) s ≝ 1724 match steps_from_sound s STATEMENT_COSTLABEL STATE_SOUNDLY_LABELLEDwith1719 match steps_from_sound s STATEMENT_COSTLABEL (ro_soundly_labelled … TRACE_OK) with 1725 1720 [ ex_intro n B ⇒ 1726 match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED STATE_SOUNDLY_LABELLEDB1721 match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B 1727 1722 return λs.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s 1728 1723 with 1729 1724 [ 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 ? ?in1725 let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1731 1726 tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T' 1732 1727 (* 1733 match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? ?with1728 match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with 1734 1729 [ ex_intro T' _ ⇒ 1735 1730 ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I 1736 1731 ]*) 1737 1732  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 ? ?in1733 let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1739 1734 tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T' 1740 1735 (* 1741 match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? ?with1736 match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with 1742 1737 [ ex_intro T' _ ⇒ 1743 1738 ex_intro ?? (tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T STATEMENT_COSTLABEL) ?? T') ? … … 1745 1740 ] STATEMENT_COSTLABEL 1746 1741 ]. 1747 [ /2/ 1748  @(trace_any_label_label … T) 1742 [ @(trace_any_label_label … T) 1749 1743  %{tr} @EV 1750 1744  @(trace_any_call_call … T) 1751  /2/1752 1745  @(well_cost_labelled_call … EV) // @(trace_any_call_call … T) 1753 1746 ] qed. 1747 1748 let 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 ≝ 1758 match 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 1795 definition 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 (* 1799 theorem 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 1813 letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p) 1814 #NOIO 1815 letin flat_trace ≝ (make_whole_flat_trace p s NOIO I) 1816 whd 1817 @(whole_structured_trace_exists … flat_trace) 1818 // 1819 [ whd 1820 *) 
src/common/StructuredTraces.ma
r1808 r1812 167 167 trace_label_diverges_exists S status_initial. 168 168 169 170 inductive trace_whole_program (S:abstract_status) : S → Type[0] ≝ 171  twp_terminating: 172 ∀status_initial: S. 173 ∀status_start_fun: S. 174 ∀status_final: S. 175 as_classifier S status_initial cl_call → 176 as_execute S status_initial status_start_fun → 177 trace_label_return S status_start_fun status_final → 178 trace_whole_program S status_initial 179  twp_diverges: 180 ∀status_initial: S. 181 ∀status_start_fun: S. 182 as_classifier S status_initial cl_call → 183 as_execute S status_initial status_start_fun → 184 trace_label_diverges S status_start_fun → 185 trace_whole_program S status_initial. 186 187 (* Again, an identical version in Prop for existence proofs. *) 188 inductive trace_whole_program_exists (S:abstract_status) : S → Prop ≝ 189  twp_terminating: 190 ∀status_initial: S. 191 ∀status_start_fun: S. 192 ∀status_final: S. 193 as_classifier S status_initial cl_call → 194 as_execute S status_initial status_start_fun → 195 trace_label_return S status_start_fun status_final → 196 trace_whole_program_exists S status_initial 197  twp_diverges: 198 ∀status_initial: S. 199 ∀status_start_fun: S. 200 as_classifier S status_initial cl_call → 201 as_execute S status_initial status_start_fun → 202 trace_label_diverges_exists S status_start_fun → 203 trace_whole_program_exists S status_initial. 204 205 169 206 let rec trace_any_label_label S s s' f 170 207 (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 ] ≝
Note: See TracChangeset
for help on using the changeset viewer.