Changeset 3030 for src/correctness.ma
 Timestamp:
 Mar 29, 2013, 12:09:07 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r3022 r3030 5 5 6 6 include "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_labels16 (exec_inf … clight_fullexec input_program)17 (exec_inf … clight_fullexec (c_labelled_clight … output))18 ∧19 True (* TODO *).20 21 #observe #input_program #output22 #COMPILE23 #NOT_WRONG24 cases (bind_inversion ????? COMPILE) COMPILE * * #init_cost #labelled' #rtlabs_program * #FRONTEND #COMPILE25 cases (bind_inversion ????? COMPILE) COMPILE #lobject_code' * #ASSEMBLER #COMPILE26 whd in COMPILE:(??%%); destruct27 cases (bind_inversion ????? FRONTEND) FRONTEND #cminor_program * #CMINOR #FRONTEND28 whd in FRONTEND:(??%%); destruct29 30 %31 [ (* Needs switch removal too, now32 @labelling_sim @NOT_WRONG33 *) cases daemon34  @I35 ] qed.36 37 7 38 8 include "Clight/Clight_classified_system.ma". … … 104 74 include "common/ExtraMonads.ma". 105 75 106 theorem correct ':76 theorem correct : 107 77 ∀observe. 108 78 ∀input_program,output. … … 127 97 whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) EQ #EQ destruct(EQ) 128 98 129 @('bind_inversion EQ_front_end) #cminor #CMINOR 99 whd in EQ_front_end:(??%?); 100 letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end; 101 lapply (refl ? (clight_label cl_switch_removed)) 102 cases (clight_label ?) in ⊢ (???% → %); #cl_labelled #init_cost' #CL_LABELLED 103 whd in ⊢ (??%? → ?); 104 letin cl_simplified ≝ (simplify_program ?) 105 #H @('bind_inversion H) H #cminor #CMINOR 130 106 #H @('bind_inversion H) H #WCL #_ 131 107 #H @('bind_inversion H) H #INJ #_ 132 #EQ_front_end' 108 letin rtlabs ≝ (cminor_to_rtlabs cminor) 109 #EQ_front_end 133 110 134 111 #NOT_WRONG % 135 [ destructcases daemon (* TODO *)112 [ cases daemon (* TODO *) 136 113  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf 137 114
Note: See TracChangeset
for help on using the changeset viewer.