Changeset 3030


Ignore:
Timestamp:
Mar 29, 2013, 12:09:07 PM (4 years ago)
Author:
campbell
Message:

Break up front-end for correctness proof.
Use let rec to prevent labelling function from unfolding.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/label.ma

    r3021 r3030  
    280280
    281281
    282 
    283 definition clight_label : clight_program → clight_program × costlabel ≝
    284 λp.
     282(* Use a let rec to prevent premature unfolding in correctness.ma. *)
     283
     284let rec clight_label (p:clight_program) : clight_program × costlabel ≝
    285285  let costgen ≝ new_universe CostTag in
    286286  let 〈init_cost, costgen〉 ≝ fresh … costgen in
    287287  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉.
     288
     289
     290lemma unfold_clight_label : ∀p.
     291  clight_label p =
     292  (let costgen ≝ new_universe CostTag in
     293  let 〈init_cost, costgen〉 ≝ fresh … costgen in
     294  〈\fst (transform_program_gen … costgen p (λ_.label_fundef)), init_cost〉).
     295* //
     296qed.
  • src/Clight/labelSimulation.ma

    r2722 r3030  
    12741274@(swl_steps E0 E0)
    12751275[ 2: @steps_step | skip | // | @build_exec
    1276   [ @transform_program_gen_related | // | inversion NW
     1276  [ whd in match ge2; >unfold_clight_label @transform_program_gen_related
     1277  | //
     1278  | inversion NW
    12771279    [ #tr #i #s #E1 #E2 destruct
    12781280    | #trX #sX #eX #NWX #E1X #E2X destruct //
  • src/correctness.ma

    r3022 r3030  
    55
    66include "Clight/labelSimulation.ma".
    7 
    8 theorem correct :
    9   ∀observe,input_program,output.
    10 (*  ∀lobject_code,labelled,cost_map. *)
    11   compile observe input_program = return output →
    12 
    13   not_wrong … (exec_inf … clight_fullexec input_program) →
    14  
    15   sim_with_labels
    16    (exec_inf … clight_fullexec input_program)
    17    (exec_inf … clight_fullexec (c_labelled_clight … output))
    18   ∧
    19   True (* TODO *).
    20 
    21 #observe #input_program #output
    22 #COMPILE
    23 #NOT_WRONG
    24 cases (bind_inversion ????? COMPILE) -COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE
    25 cases (bind_inversion ????? COMPILE) -COMPILE #lobject_code' * #ASSEMBLER #COMPILE
    26 whd in COMPILE:(??%%); destruct
    27 cases (bind_inversion ????? FRONTEND) -FRONTEND #cminor_program * #CMINOR #FRONTEND
    28 whd in FRONTEND:(??%%); destruct
    29 
    30 %
    31 [ (* Needs switch removal too, now
    32      @labelling_sim @NOT_WRONG
    33    *) cases daemon
    34 | @I
    35 ] qed.
    36 
    377
    388include "Clight/Clight_classified_system.ma".
     
    10474include "common/ExtraMonads.ma".
    10575
    106 theorem correct' :
     76theorem correct :
    10777  ∀observe.
    10878  ∀input_program,output.
     
    12797whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
    12898
    129 @('bind_inversion EQ_front_end) #cminor #CMINOR
     99whd in EQ_front_end:(??%?);
     100letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
     101lapply (refl ? (clight_label cl_switch_removed))
     102cases (clight_label ?) in ⊢ (???% → %); #cl_labelled #init_cost' #CL_LABELLED
     103whd in ⊢ (??%? → ?);
     104letin cl_simplified ≝ (simplify_program ?)
     105#H @('bind_inversion H) -H #cminor #CMINOR
    130106#H @('bind_inversion H) -H #WCL #_
    131107#H @('bind_inversion H) -H #INJ #_
    132 #EQ_front_end'
     108letin rtlabs ≝ (cminor_to_rtlabs cminor)
     109#EQ_front_end
    133110
    134111#NOT_WRONG %
    135 [ destruct cases daemon (* TODO *)
     112[ cases daemon (* TODO *)
    136113| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
    137114
Note: See TracChangeset for help on using the changeset viewer.