Changeset 2928
 Timestamp:
 Mar 21, 2013, 6:26:46 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r2875 r2928 114 114 minus c2 c1 = clock … (execute n2 ? initial_status)  clock … (execute n1 ? initial_status). 115 115 116 include "common/ExtraMonads.ma". 117 116 118 theorem correct' : 117 119 ∀observe. … … 124 126 ∧ 125 127 simulates output. 128 #observe #p_in #out 129 #H @('bind_inversion H) H 130 ** #init_cost #labelled #p_rtlabs #EQ_front_end 131 #H @('bind_inversion H) H 132 ** #p_asm #stack_costs #globals_size 133 #H @('bind_inversion H) H 134 #p_asm' 135 #H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm 136 whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) EQ #EQ destruct(EQ) 137 #H @('bind_inversion H) H 138 #p_loc #EQ_assembler 139 whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) EQ #EQ destruct(EQ) 140 #NOT_WRONG % 141 [ cases daemon (* TODO *) 142  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf 143 144 cut (∀n,s1,s2,obs1,obs2. 145 exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 → 146 ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2. 147 tlr_observables … tlr (function_of … s1) = obs2 → 148 (* maybe instead of function_of the called id can rather be obtained from execution? *) 149 ∃m,p,s_fin. 150 observables (OC_preclassified_system (c_labelled_object_code … p)) 151 (c_labelled_object_code … p) m p = return 〈obs1, obs2〉) 152 153 154 155 126 156 127 157 (* start of old simulates
Note: See TracChangeset
for help on using the changeset viewer.