Changeset 2226 for src/RTLabs


Ignore:
Timestamp:
Jul 20, 2012, 6:36:34 PM (7 years ago)
Author:
campbell
Message:

Whole program proof.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/CostSpec.ma

    r2218 r2226  
    7676
    7777definition well_cost_labelled_program : RTLabs_program → Prop ≝
    78   λp. All ? (λx. let 〈id,fd〉 ≝ x in
    79                  match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | _ ⇒ True]) (prog_funct … p).
     78  λp. All ? (λx. match \snd x with [ Internal fn ⇒
     79    well_cost_labelled_fn fn ∧ soundly_labelled_fn fn
     80  | _ ⇒ True]) (prog_funct … p).
    8081
    8182
  • src/RTLabs/Traces.ma

    r2224 r2226  
    19421942] qed.
    19431943
     1944lemma well_cost_labelled_initial : ∀p,s.
     1945  make_initial_state p = OK ? s →
     1946  well_cost_labelled_program p →
     1947  well_cost_labelled_state s ∧ soundly_labelled_state s.
     1948#p #s
     1949@bind_ok #m #Em
     1950@bind_ok #b #Eb
     1951@bind_ok #f #Ef
     1952#E destruct
     1953whd in ⊢ (% → %);
     1954#WCL
     1955@(find_funct_ptr_All ??????? Ef)
     1956@(All_mp … WCL)
     1957* #id * /3/ #fn * #W #S % [ /2/ | whd % // @S ]
     1958qed.
     1959
     1960lemma well_cost_labelled_make_global : ∀p.
     1961  well_cost_labelled_program p →
     1962  well_cost_labelled_ge (make_global p) ∧ soundly_labelled_ge (make_global p).
     1963#p whd in ⊢ (% → ?%%);
     1964#WCL %
     1965#b #f #FFP
     1966[ @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ well_cost_labelled_fn f | _ ⇒ True]) FFP)
     1967| @(find_funct_ptr_All ?????? (λf. match f with [ Internal f ⇒ soundly_labelled_fn f | _ ⇒ True]) FFP)
     1968] @(All_mp … WCL)
     1969* #id * #fn // * /2/
     1970qed.
     1971
    19441972theorem program_trace_exists :
    19451973  termination_oracle →
    19461974  ∀p:RTLabs_program.
     1975  well_cost_labelled_program p →
    19471976  ∀s:state.
    19481977  ∀I: make_initial_state p = OK ? s.
     
    19571986  trace_whole_program_exists (RTLabs_status (make_global p)) (Ras_state_initial p s I).
    19581987
    1959 #ORACLE #p #s #I
     1988#ORACLE #p #WCL #s #I
    19601989letin plain_trace ≝ (exec_inf io_out io_in RTLabs_fullexec p)
    19611990#NOIO #NW
     
    19631992whd
    19641993@(whole_structured_trace_exists (make_global p) p ? ORACLE)
    1965 [ 3: @flat_trace | 4: @I
    1966 | *: cases daemon
     1994[ @(proj1 … (well_cost_labelled_make_global … WCL))
     1995| @(proj2 … (well_cost_labelled_make_global … WCL))
     1996| @flat_trace
     1997| @I
     1998| @(proj1 ?? (well_cost_labelled_initial … I WCL))
     1999| @(proj2 ?? (well_cost_labelled_initial … I WCL))
    19672000] qed.
    19682001
Note: See TracChangeset for help on using the changeset viewer.