Changeset 2202


Ignore:
Timestamp:
Jul 17, 2012, 6:57:39 PM (5 years ago)
Author:
campbell
Message:

Start defining equivalent executions.

Location:
src
Files:
1 added
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2176 r2202  
    11891189
    11901190lemma not_wrong_init : ∀p.
    1191   not_wrong (exec_inf … clight_fullexec p) →
     1191  not_wrong state (exec_inf … clight_fullexec p) →
    11921192  ∃s. make_initial_state … p = OK ? s.
    1193 #p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
     1193#p whd in ⊢ (??% → ?); change with (make_initial_state p) in match (make_initial_state ??? p);
    11941194cases (make_initial_state p)
    11951195[ /2/
     
    12251225  plus ge s tr s' →
    12261226  is_final s' = None ? →
    1227   steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
    1228            (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
     1227  steps state tr
     1228    (exec_inf_aux … clight_fullexec ge (exec_step ge s))
     1229    (exec_inf_aux … clight_fullexec ge (exec_step ge s')).
    12291230#ge #s0 #tr0 #s0' #P elim P
    12301231[ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold
    1231   whd in ⊢ (??%?);
     1232  whd in ⊢ (???%?);
    12321233  whd in match (is_final ?????); >NF
    12331234  %2
    12341235| #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF
    12351236  >exec_inf_aux_unfold >EX1
    1236   whd in ⊢ (??%?);
     1237  whd in ⊢ (???%?);
    12371238  whd in match (is_final ?????); >(plus_not_final … P2)
    12381239  %3 @IH //
     
    12421243  plus ge s tr s' →
    12431244  is_final s' = Some ? r →
    1244   ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s))
    1245                  (e_stop … tr' r s').
     1245  ∃tr'. steps state tr
     1246          (exec_inf_aux … clight_fullexec ge (exec_step ge s))
     1247          (e_stop … tr' r s').
    12461248#ge #s0 #tr0 #s0' #r #P elim P
    12471249[ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold
    1248   %{tr} whd in ⊢ (??%?);
     1250  %{tr} whd in ⊢ (???%?);
    12491251  whd in match (is_final ?????); >F
    12501252  %1
     
    12531255  #tr' #S' %{tr'}
    12541256  >exec_inf_aux_unfold >EX1
    1255   whd in ⊢ (??%?);
     1257  whd in ⊢ (???%?);
    12561258  whd in match (is_final ?????); >(plus_not_final … P2)
    12571259  %3 @S'
     
    12631265  (s1,s2:state)
    12641266  (S:state_with_labels s1 s2)
    1265   (NW:not_wrong (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
     1267  (NW:not_wrong state (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)))
    12661268: sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝
    12671269match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with
     
    12991301  #i cases (H2 i) #tr1 * #s1' * #K1 * #tr2 * #s2' * * #K2 #TR #S'
    13001302  lapply (NWk i)
    1301   @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (?% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
     1303  @(match sym_eq … K1 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold …) with [refl ⇒ ?]) whd in ⊢ (??% → ?%%); whd in match (is_final ?????); @(match sym_eq … (final_related … S') with [refl ⇒ ?])
    13021304  @(match sym_eq … K2 with [refl ⇒ ?]) @(match sym_eq … (exec_inf_aux_unfold ?? clight_fullexec ge2 …) with [refl ⇒ ?]) whd in ⊢ (? → ??%); whd in match (is_final ?????);
    13031305  cases (is_final s2')
    1304   [ whd in ⊢ (?% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
     1306  [ whd in ⊢ (??% → ?%%); #NW' @(swl_steps … (steps_step …)) // @build_exec //
    13051307    inversion NW'
    13061308    [ #H1 #H2 #H3 #H4 #H5 destruct
     
    13081310    | #H14 #H15 #H16 #H17 #H18 destruct
    13091311    ]
    1310   | #r whd in ⊢ (?% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
     1312  | #r whd in ⊢ (??% → ?%%); #NW' @(swl_stop … (steps_stop …)) //
    13111313  ]
    13121314] qed.
     
    13431345>I2
    13441346
    1345 whd in ⊢ (?% → ? → ?%%);
     1347whd in ⊢ (??% → ? → ?%%);
    13461348>exec_inf_aux_unfold
    13471349>exec_inf_aux_unfold
    1348 whd in ⊢ (?% → ? → ?%%);
     1350whd in ⊢ (??% → ? → ?%%);
    13491351whd in match (is_final ?????);
    13501352>(initial_state_is_not_final … I1)
    13511353whd in match (is_final ?????);
    13521354>(initial_state_is_not_final … I2)
    1353 whd in ⊢ (?% → ? → ?%%);
     1355whd in ⊢ (??% → ? → ?%%);
    13541356
    13551357#NW #S
  • src/Clight/labelSpecification.ma

    r2201 r2202  
    11include "Clight/Cexec.ma".
    22include "Clight/label.ma".
     3include "common/Executions.ma".
    34
    45(* Formalise the notion of a trace with extra cost labels added.  Note that
     
    910| twel_new : ∀c,t1,t2. trace_with_extra_labels t1 t2 → trace_with_extra_labels t1 (EVcost c::t2).
    1011
    11 (* A finite trace is produced by some prefix of an execution. *)
    12 
    13 inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝
    14 | steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r)
    15 | steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e
    16 | steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'.
    17 
    1812(* One execution is simulated by another, but possibly using more steps and
    1913   introducing some cost labels. *)
     
    2115coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝
    2216| swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2.
    23     steps tr2 e2 (e_stop … tr2' r s2) →
     17    steps state tr2 e2 (e_stop … tr2' r s2) →
    2418    trace_with_extra_labels tr1 tr2 →
    2519    sim_with_labels (e_stop … tr1 r s1) e2
    2620| swl_steps : ∀tr1,tr2,s1,e1,e2,e2'.
    27     steps tr2 e2 e2' →
     21    steps state tr2 e2 e2' →
    2822    trace_with_extra_labels tr1 tr2 →
    2923    sim_with_labels e1 e2' →
     
    3327    sim_with_labels (e_interact … o k1) (e_interact … o k2).
    3428
    35 (* We do not consider wrong executions. *)
    36 
    37 coinductive not_wrong : execution state io_out io_in → Prop ≝
    38 | nw_stop : ∀tr,i,s. not_wrong (e_stop … tr i s)
    39 | nw_step : ∀tr,s,e. not_wrong e → not_wrong (e_step … tr s e)
    40 | nw_interact : ∀o,k. (∀i. not_wrong (k i)) → not_wrong (e_interact … o k).
    41 
    4229(* Desired result *)
    4330
     
    4633  let e1 ≝ exec_inf … clight_fullexec p in
    4734  let e2 ≝ exec_inf … clight_fullexec (clight_label p) in
    48   not_wrong e1 →
     35  not_wrong state e1 →
    4936  sim_with_labels e1 e2.
  • src/common/SmallstepExec.ma

    r2145 r2202  
    155155  ].
    156156
    157 (* Some preliminary simulation stuff that's not been used yet.
    158 record execstep' (outty:Type[0]) (inty:outty → Type[0]) : Type[1] ≝
    159 { es0 :> execstep outty inty
    160 ; initial : state ?? es0 → Prop
    161 }.
    162157
    163 
    164 alias symbol "and" (instance 2) = "logical and".
    165 record related_semantics : Type[1] ≝
    166 { output : Type[0]
    167 ; input : output → Type[0]
    168 ; sem1 : execstep' output input
    169 ; sem2 : execstep' output input
    170 ; ge1 : genv ?? sem1
    171 ; ge2 : genv ?? sem2
    172 ; match_states : state ?? sem1 → state ?? sem2 → Prop
    173 ; match_initial_states : ∀st1. (initial ?? sem1) st1 → ∃st2. (initial ?? sem2) st2 ∧ match_states st1 st2
    174 ; match_final_states : ∀st1,st2,r. match_states st1 st2 → (is_final ?? sem1) st1 = Some ? r → (is_final ?? sem2) st2 = Some ? r
    175 }.
    176 
    177 
    178 
    179 record simulation : Type[1] ≝
    180 { sems :> related_semantics
    181 ; sim : ∀st1,st2,t,st1'.
    182         P_io' ?? (trace × (state ?? (sem1 sems))) (λr. r = 〈t,st1'〉) (step ?? (sem1 sems) (ge1 sems) st1) →
    183         match_states sems st1 st2 →
    184         ∃st2':(state ?? (sem2 sems)).(∃n:nat.P_io' ?? (trace × (state ?? (sem2 sems))) (λr. r = 〈t,st2'〉) (repeat n ?? (sem2 sems) (ge2 sems) st2)) ∧
    185           match_states sems st1' st2'
    186 }.
    187 *)
Note: See TracChangeset for help on using the changeset viewer.