Changeset 2839


Ignore:
Timestamp:
Mar 11, 2013, 12:18:05 PM (4 years ago)
Author:
campbell
Message:

Basic structure of RTLabs measurable to structured traces results.

Location:
src/RTLabs
Files:
1 added
1 edited
1 copied

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_partial_traces.ma

    r2800 r2839  
     1
     2(* This deals with the construction of structured traces of finite parts of
     3   RTLabs program executions.  It will be used as part of the whole compiler's
     4   intensional correctness proof.
     5   
     6   It was originally based on RTLabs/RTLabs_traces.ma, which constructs whole
     7   execution structured traces, but dealing with the whole program execution
     8   is unnecessary, it requires classical reasoning for deciding when functions
     9   terminate and it doesn't fit well with some of the other definitions.
     10   
     11   In principle we could clean this up a little by harmonising some of the
     12   definitions with other parts of the development. *)
    113
    214include "RTLabs/RTLabs_abstract.ma".
     
    5062qed.
    5163
    52 (* Before attempting to construct a structured trace, let's show that we can
    53    form flat traces with evidence that they were constructed from an execution.
    54    As with the structured traces, we only consider good traces (i.e., ones
    55    which don't go wrong).
    56    
    57    For now we don't consider I/O. *)
    58 
    59 
    60 coinductive exec_no_io (o:Type[0]) (i:o → Type[0]) : execution state o i → Prop ≝
    61 | noio_stop : ∀a,b,c. exec_no_io o i (e_stop … a b c)
    62 | noio_step : ∀a,b,e. exec_no_io o i e → exec_no_io o i (e_step … a b e)
    63 | noio_wrong : ∀m. exec_no_io o i (e_wrong … m).
    64 
    65 (* add I/O? *)
    66 coinductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
    67 | ft_stop : ∀s. RTLabs_is_final s ≠ None ? → flat_trace o i ge s
     64inductive flat_trace (o:Type[0]) (i:o → Type[0]) (ge:genv) : state → Type[0] ≝
     65| ft_stop : ∀s. flat_trace o i ge s
    6866| ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s.
    6967
    70 let corec make_flat_trace ge s
    71   (NF:RTLabs_is_final s = None ?)
    72   (NW:not_wrong state (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s)))
    73   (H:exec_no_io io_out io_in (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) :
    74   flat_trace io_out io_in ge s ≝
    75 let e ≝ exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s) in
    76 match e return λx. e = x → ? with
    77 [ e_stop tr i s' ⇒ λE. ft_step … s tr s' ? (ft_stop … s' ?)
    78 | e_step tr s' e' ⇒ λE. ft_step … s tr s' ? (make_flat_trace ge s' ???)
    79 | e_wrong m ⇒ λE. ⊥
    80 | e_interact o f ⇒ λE. ⊥
    81 ] (refl ? e).
    82 [ 1,3: whd in E:(??%?); >exec_inf_aux_unfold in E;
    83   cases (eval_statement ge s)
    84   [ 1,4: #O #K whd in ⊢ (??%? → ?); #E destruct
    85   | 2,5: * #tr #s1 whd in ⊢ (??%? → ?);
    86     >(?:is_final ????? = RTLabs_is_final s1) //
    87     lapply (refl ? (RTLabs_is_final s1))
    88     cases (RTLabs_is_final s1) in ⊢ (???% → %);
    89     [ 1,3: #_ whd in ⊢ (??%? → ?); #E destruct %
    90     | #i #_ whd in ⊢ (??%? → ?); #E destruct @refl
    91     | #i #E whd in ⊢ (??%? → ?); #E2 destruct
    92     ]
    93   | *: #m whd in ⊢ (??%? → ?); #E destruct
    94   ]
    95 | whd in E:(??%?); >exec_inf_aux_unfold in E;
    96   cases (eval_statement ge s)
    97   [ #o #K whd in ⊢ (??%? → ?); #E destruct
    98   | * #tr #s1 whd in ⊢ (??%? → ?);
    99     lapply (refl ? (RTLabs_is_final s1))
    100     change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
    101     cases (RTLabs_is_final s1) in ⊢ (???% → %);
    102     [ #F #E whd in E:(??%?); destruct
    103     | #r #F #E whd in E:(??%?); destruct >F % #E destruct
    104     ]
    105   | #m #E whd in E:(??%?); destruct
    106   ]
    107 | whd in E:(??%?); >E in H; #H >exec_inf_aux_unfold in E;
    108   cases (eval_statement ge s)
    109   [ #O #K whd in ⊢ (??%? → ?); #E destruct
    110   | * #tr #s1 whd in ⊢ (??%? → ?);
    111     cases (is_final ?????)
    112     [ whd in ⊢ (??%? → ?); #E
    113       change with (eval_statement ge s1) in E:(??(??????(?????%))?);
    114       destruct
    115       inversion H
    116       [ #a #b #c #E1 destruct
    117       | #trx #sx #ex #H1 #E2 #E3 destruct @H1
    118       | #m #E1 destruct
    119       ]
    120     | #i whd in ⊢ (??%? → ?); #E destruct
    121     ]
    122   | #m whd in ⊢ (??%? → ?); #E destruct
    123   ]
    124 | whd in E:(??%?); >E in NW; #NW >exec_inf_aux_unfold in E;
    125   cases (eval_statement ge s)
    126   [ #O #K whd in ⊢ (??%? → ?); #E destruct
    127   | * #tr #s1 whd in ⊢ (??%? → ?);
    128     cases (is_final ?????)
    129     [ whd in ⊢ (??%? → ?); #E
    130       change with (eval_statement ge s1) in E:(??(??????(?????%))?);
    131       destruct
    132       inversion NW
    133       [ #a #b #c #E1 #_ destruct
    134       | #trx #sx #ex #H1 #E2 #E3 destruct @H1
    135       | #o #k #K #E1 destruct
    136       ]
    137     | #i whd in ⊢ (??%? → ?); #E destruct
    138     ]
    139   | #m whd in ⊢ (??%? → ?); #E destruct
    140   ]
    141 | whd in E:(??%?); >exec_inf_aux_unfold in E;
    142   cases (eval_statement ge s)
    143   [ #o #K whd in ⊢ (??%? → ?); #E destruct
    144   | * #tr #s1 whd in ⊢ (??%? → ?);
    145     lapply (refl ? (RTLabs_is_final s1))
    146     change with (RTLabs_is_final s1) in ⊢ (? → ??(match % with [_⇒?|_⇒?])? → ?);
    147     cases (RTLabs_is_final s1) in ⊢ (???% → %);
    148     [ #F #E whd in E:(??%?); destruct @F
    149     | #r #F #E whd in E:(??%?); destruct
    150     ]
    151   | #m #E whd in E:(??%?); destruct
    152   ]
    153 | whd in E:(??%?); >E in NW; #X inversion X
    154   #A #B #C #D #E destruct
    155 | whd in E:(??%?); >E in H; #H inversion H
    156   #A #B #C try #D try #E destruct
    157 ] qed.
    158 
    159 definition make_whole_flat_trace : ∀p,s.
    160   exec_no_io … (exec_inf … RTLabs_fullexec p) →
    161   not_wrong … (exec_inf … RTLabs_fullexec p) →
    162   make_initial_state ??? p = OK ? s →
    163   flat_trace io_out io_in (make_global … RTLabs_fullexec p) s ≝
    164 λp,s,H,NW,I.
    165 let ge ≝ make_global … p in
    166 let e ≝ exec_inf_aux ?? RTLabs_fullexec ge (Value … 〈E0, s〉) in
    167 match e return λx. e = x → ? with
    168 [ e_stop tr i s' ⇒ λE. ft_stop ?? ge s ?
    169 | e_step _ _ e' ⇒ λE. make_flat_trace ge s ???
    170 | e_wrong m ⇒ λE. ⊥
    171 | e_interact o f ⇒ λE. ⊥
    172 ] (refl ? e).
    173 [ whd in E:(??%?); >exec_inf_aux_unfold in E;
    174   whd in ⊢ (??%? → ?);
    175   change with (RTLabs_is_final s) in ⊢ (??(match % with[_⇒?|_⇒?])? → ?);
    176   cases (RTLabs_is_final s)
    177   [ #E whd in E:(??%?); destruct
    178   | #r #E % #E' destruct
    179   ]
    180 | @(initial_state_is_not_final … I)
    181 | whd in NW:(??%); >I in NW; whd in ⊢ (??% → ?); whd in E:(??%?);
    182   >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ??% → ?); cases (is_final ?????)
    183   [ whd in ⊢ (??%? → ??% → ?); #E #H inversion H
    184     [ #a #b #c #E1 destruct
    185     | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
    186       @H1
    187     | #o #k #K #E1 destruct
    188     ]
    189   | #i whd in ⊢ (??%? → ??% → ?); #E destruct
    190   ]
    191 | whd in H:(???%); >I in H; whd in ⊢ (???% → ?); whd in E:(??%?);
    192   >exec_inf_aux_unfold in E ⊢ %; whd in ⊢ (??%? → ???% → ?); cases (is_final ?????)
    193   [ whd in ⊢ (??%? → ???% → ?); #E #H inversion H
    194     [ #a #b #c #E1 destruct
    195     | #tr1 #s1 #e1 #H1 #E1 #E2 -E2 -I destruct (E1)
    196       @H1
    197     | #m #E1 destruct
    198     ]
    199   | #i whd in ⊢ (??%? → ???% → ?); #E destruct
    200   ]
    201 | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
    202   cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
    203 | whd in E:(??%?); >exec_inf_aux_unfold in E; whd in ⊢ (??%? → ?);
    204   cases (is_final ?????) [2:#i] whd in ⊢ (??%? → ?); #E destruct
    205 ] qed.
     68let rec make_flat_trace ge n s trace s' (EX:exec_steps n … RTLabs_fullexec ge s = return 〈trace,s'〉) on n : flat_trace io_out io_in ge s ≝
     69match n return λn. exec_steps n ????? = ? → ? with
     70[ O ⇒ λ_. ft_stop … s
     71| S m ⇒ λEX'.
     72  match eval_statement ge s return λx. eval_statement ?? = x → ? with
     73  [ Value ts ⇒ λEV. ft_step ??? s (\fst ts) (\snd ts) ? (make_flat_trace ge m (\snd ts) (tail … trace) s' ?)
     74  | _ ⇒ λEV. ⊥
     75  ] (refl ??)
     76] EX.
     77[ cases (exec_steps_S … EX') #_ * #tr' *  #s1 * #tl * * #E #ST #_
     78  change with (eval_statement ??) in ST:(??%?); >EV in ST;
     79  #ST destruct
     80| //
     81| cases (exec_steps_S … EX') #_ * #tr' *  #s1 * #tl * * #E #ST #STEPS
     82  change with (eval_statement ??) in ST:(??%?); >EV in ST;
     83  #ST destruct
     84  @STEPS
     85| cases (exec_steps_S … EX') #_ * #tr' *  #s1 * #tl * * #E #ST #_
     86  change with (eval_statement ??) in ST:(??%?); >EV in ST;
     87  #ST destruct
     88] qed.
     89
     90lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'.
     91  ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉.
     92  Σs1. ∃ST,EX'. make_flat_trace ge (S n) s (hd::trace) s' EX = ft_step ??? s (\snd hd) s1 ST (make_flat_trace ge n s1 trace s' EX').
     93#ge #n #s #hd #trace #s' #EX
     94lapply (refl ? (eval_statement ge s))
     95cases (eval_statement ge s) in ⊢ (???% → ?);
     96[ #o #k | 3: #m ]
     97[ 1,2: #EV @⊥ cases (exec_steps_S … EX) #NF * #tr * #s2 * #tl * * #E1 destruct
     98  change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct
     99] * #tr #s1 #EV
     100%{s1}
     101cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct
     102change with (eval_statement ??) in ⊢ (??%? → ?); >EV in ⊢ (% → ?); #E destruct #EX'
     103%{EV} %{EX'}
     104whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
     105>EV in ⊢ (???% → ??(match % with [_⇒?|_⇒?|_⇒?]?)?);
     106#ST' whd in ⊢ (??%?); %
     107qed.
    206108
    207109(* Need a way to choose whether a called function terminates.  Then,
     
    928830                               myge ? (times 3 (will_return_length ??? trace TM)) →
    929831                               sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with
    930   [ ft_stop st FINAL
     832  [ ft_stop st
    931833      λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥
    932834
     
    14891391@⊥ @(absurd ?? CL) @refl
    14901392qed.
    1491 
     1393(*
    14921394definition termination_oracle ≝ ∀ge,depth,s,trace.
    14931395  inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace).
     
    16371539    ]
    16381540] qed.
    1639 
     1541*)
    16401542lemma simplify_cl : ∀ge,s,c.
    16411543  as_classifier (RTLabs_status ge) s c →
     
    16451547destruct //
    16461548qed.
    1647 
     1549(*
    16481550(* NB: This isn't quite what I'd like.  Ideally, we'd show the existence of
    16491551       a trace_label_diverges value, but I only know how to construct those
     
    17771679    ]
    17781680] qed.
    1779 
     1681*)
    17801682lemma init_state_is : ∀p,s.
    17811683  make_initial_state p = OK ? s →
     
    18281730* #id * #fn // * /2/
    18291731qed.
    1830 
     1732(*
    18311733theorem program_trace_exists :
    18321734  termination_oracle →
     
    18581760| @(proj2 ?? (well_cost_labelled_initial … I WCL))
    18591761] qed.
    1860 
     1762*)
    18611763
    18621764lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge.
     
    19891891[ tlc_base s1 s2 tac CS ⇒ flat_trace_of_any_call … tac
    19901892] EX''.
    1991 
     1893(*
    19921894(* Now reconstruct the flat_trace of a diverging execution.  Note that we need
    19931895   to take care to satisfy the guardedness condition by witnessing the fact that
     
    20851987@flat_traces_are_determined_by_starting_point
    20861988qed.
    2087 
     1989*)
    20881990
    20891991
  • src/RTLabs/RTLabs_traces.ma

    r2760 r2839  
     1
     2(* This file shows that structured traces can be generated for entire executions
     3   of RTLabs programs (given no failure or I/O).  It stands alone; the file
     4   RTLabs/RTLabs_partial_traces.ma contains a finite variant that is used for
     5   the compiler proofs. *)
    16
    27include "RTLabs/RTLabs_abstract.ma".
Note: See TracChangeset for help on using the changeset viewer.