Changeset 3030 for src/correctness.ma


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.