Changeset 3047


Ignore:
Timestamp:
Mar 31, 2013, 10:01:42 PM (4 years ago)
Author:
campbell
Message:

Switch removal and labelling combined.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/SwitchAndLabel.ma

    r3046 r3047  
    22include "Clight/labelSimulation.ma".
    33
    4 axiom switch_final_related : ∀ge1,s1,s2.
    5   switch_state_sim ge1 s1 s2 →
    6   is_final s1 = is_final s2.
    74
    85lemma after_aux_result : ∀avs,n,s,tr,P.
     
    9087
    9188lemma interactive_switch_step : ∀ge,ge'.
    92   switch_removal_globals ? fundef_switch_removal ge ge' →
     89  related_globals … fundef_switch_removal ge ge' →
    9390  ∀s1,s1',o,k.
    9491  exec_step ge s1 = Interact … o k →
     
    144141let corec build_exec
    145142  (ge1,ge2,ge3:genv)
    146   (SRG:switch_removal_globals ? fundef_switch_removal ge1 ge2)
     143  (SRG:related_globals … fundef_switch_removal ge1 ge2)
    147144  (RG:related_globals_gen … label_fundef ge2 ge3)
    148145  (s1,s2,s3:state)
     
    212209  ]
    213210] qed.
     211
     212theorem switch_and_labelling_sim : ∀p.
     213  let e1 ≝ exec_inf … clight_fullexec p in
     214  let e2 ≝ exec_inf … clight_fullexec (\fst (clight_label (program_switch_removal p))) in
     215  not_wrong state e1 →
     216  sim_with_labels e1 e2.
     217#p letin p' ≝ (program_switch_removal p)
     218#NW
     219cases (not_wrong_init clight_fullexec p NW)
     220whd in ⊢ (% → ??%? → ?); #s1 #I1
     221cases (initial_state_in_switch_simulation … I1)
     222#s' * * change with p' in match (program_switch_removal p); #I' #RG' #S'
     223cases (initial_state_in_simulation … I')
     224#s2 * #I2
     225
     226whd in match (exec_inf ?? clight_fullexec p) in NW ⊢ %;
     227letin ge1 ≝ (make_global ?? clight_fullexec p) in NW ⊢ %;
     228change with (make_initial_state p) in match (make_initial_state ?? clight_fullexec p);
     229>I1
     230
     231whd in match (exec_inf ????);
     232letin ge2 ≝ (make_global ?? clight_fullexec (\fst (clight_label p')))
     233change with (make_initial_state (\fst (clight_label p'))) in match (make_initial_state ?? clight_fullexec (\fst (clight_label p')));
     234>I2
     235
     236whd in ⊢ (??% → ? → ?%%);
     237>exec_inf_aux_unfold
     238>exec_inf_aux_unfold
     239whd in ⊢ (??% → ? → ?%%);
     240whd in match (is_final ?????);
     241>(initial_state_is_not_final … I1)
     242whd in match (is_final ?????);
     243>(initial_state_is_not_final … I2)
     244whd in ⊢ (??% → ? → ?%%);
     245
     246#NW #S
     247@(swl_steps E0 E0)
     248[ 2: @steps_step | skip | // | @(build_exec … RG' … S' S)
     249  [ whd in match ge2; >unfold_clight_label
     250    @transform_program_gen_related
     251  | inversion NW
     252    [ #tr #i #s #E1 #E2 destruct
     253    | #trX #sX #eX #NWX #E1X #E2X destruct //
     254    | #H1 #H2 #H3 #H4 #H5 destruct
     255    ]
     256  ]
     257] qed.
     258
     259
  • src/Clight/switchRemoval.ma

    r3046 r3047  
    429429
    430430let rec program_switch_removal (p : clight_program) : clight_program ≝
    431  let prog_funcs ≝ prog_funct ?? p in
    432  let sf_funcs   ≝ map ?? (λcl_fundef.
    433     let 〈fun_id, fun_def〉 ≝ cl_fundef in
    434     〈fun_id, fundef_switch_removal fun_def〉
    435   ) prog_funcs in
    436  mk_program ??
    437   (prog_vars … p)
    438   sf_funcs
    439   (prog_main … p).
     431  transform_program ??? p (λ_. fundef_switch_removal).
    440432
    441433(* -----------------------------------------------------------------------------
     
    19201912      (Kcall r (\fst (function_switch_removal f)) en' k').
    19211913
    1922 record switch_removal_globals (F:Type[0]) (t:F → F) (ge:genv_t F) (ge':genv_t F) : Prop ≝ {
    1923   rg_find_symbol: ∀s.
    1924     find_symbol ? ge s = find_symbol ? ge' s;
    1925   rg_find_funct_id: ∀v,f,id.
    1926     find_funct_id ? ge v = Some ? 〈f,id〉 →
    1927     find_funct_id ? ge' v = Some ? 〈t f,id〉;
    1928   rg_find_funct_ptr: ∀b,f.
    1929     find_funct_ptr ? ge b = Some ? f →
    1930     find_funct_ptr ? ge' b = Some ? (t f)
    1931 }.
    1932 
    19331914inductive switch_state_sim (ge : genv) : state → state → Prop ≝
    19341915| sws_state :
     
    22142195lemma sim_related_globals : ∀ge,ge',en1,m1,en2,m2,writeable,ext.
    22152196  ∀Hext:sr_memext m1 m2 writeable.
    2216   switch_removal_globals ? fundef_switch_removal ge ge' →
     2197  related_globals … fundef_switch_removal ge ge' →
    22172198  disjoint_extension en1 en2 ext →
    22182199(*  disjoint_extension en1 en2 ext Hext → *)
     
    27502731theorem switch_removal_correction :
    27512732  ∀ge,ge'.
    2752   switch_removal_globals ? fundef_switch_removal ge ge' →
     2733  related_globals … fundef_switch_removal ge ge' →
    27532734  ∀s1,s1',tr,s2.
    27542735  switch_state_sim ge s1 s1' →
     
    32593240   | *: @cthulhu ]
    32603241 | *: @cthulhu ] qed.
     3242
     3243
     3244lemma initial_state_in_switch_simulation : ∀p,s.
     3245  make_initial_state p = OK ? s →
     3246  ∃s'.
     3247    make_initial_state (program_switch_removal p) = OK ? s' ∧
     3248    related_globals … fundef_switch_removal (make_global p) (make_global (program_switch_removal p)) ∧
     3249    switch_state_sim (make_global p) s s'.
     3250* #vars #fns #main #s
     3251whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX
     3252cases (bind_inversion ????? EX) -EX #m * #Em #EX
     3253cases (bind_inversion ????? EX) -EX #b * #Emain #EX
     3254cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX
     3255whd in EX:(??%%); destruct
     3256whd in match (make_initial_state ?);
     3257letin ge' ≝ (make_global ?)
     3258cut (related_globals … fundef_switch_removal ge ge')
     3259[ // ] #RG
     3260lapply (rg_find_funct_ptr … RG … Emain') #FFP
     3261% [2: %
     3262[ %
     3263 [whd in ⊢ (??%?);
     3264  change with (transform_program ??? (mk_program …) (λ_.?)) in match (mk_program ??? (transf_program ????) ?);
     3265  >(init_mem_transf … (mk_program ?? vars fns main)) >Em in ⊢ (??%?);
     3266  whd in ⊢ (??%?); <(rg_find_symbol … RG) >Emain in ⊢ (??%?);
     3267  whd in ⊢ (??%?); >FFP in ⊢ (??%?);
     3268  whd in ⊢ (??%?); @refl
     3269| /3/
     3270] | /3/ ] | skip ]
     3271qed.
     3272
     3273lemma switch_final_related : ∀ge1,s1,s2.
     3274  switch_state_sim ge1 s1 s2 →
     3275  is_final s1 = is_final s2.
     3276#Xge #Xs1 #Xs2 * //
     3277qed.
     3278
  • src/correctness.ma

    r3030 r3047  
    33
    44include "ASM/Interpret2.ma".
    5 
    6 include "Clight/labelSimulation.ma".
    75
    86include "Clight/Clight_classified_system.ma".
     
    7472include "common/ExtraMonads.ma".
    7573
     74include "Clight/SwitchAndLabel.ma".
     75
    7676theorem correct :
    7777  ∀observe.
     
    110110
    111111#NOT_WRONG %
    112 [ cases daemon (* TODO *)
     112[ whd in EQ_front_end:(??%%); destruct
     113  cut (labelled = \fst (clight_label cl_switch_removed))
     114  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
     115  #E >E
     116  @switch_and_labelling_sim @NOT_WRONG
    113117| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
    114118
Note: See TracChangeset for help on using the changeset viewer.