 Timestamp:
 Apr 2, 2013, 7:25:22 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/correctness.ma
r3047 r3074 41 41 42 42 include "RTLabs/MeasurableToStructured.ma". 43 44 definition clight_clock_after : ∀p:clight_program. nat → (costlabel→ℕ) → res nat ≝ 45 λp,n,costmap. 46 ! 〈s,itrace〉 ← exec_steps_with_obs Clight_pcs p n; 43 include "common/ExtraMonads.ma". 44 45 definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝ 46 λcostmap,itrace. 47 47 let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl  _ ⇒ None ? ]) itrace in 48 return Σ_{l ∈ ctrace}(costmap l). 48 Σ_{l ∈ ctrace}(costmap l). 49 50 definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝ 51 λC,p,n,costmap. 52 ! 〈s,itrace〉 ← exec_steps_with_obs C p n; 53 return exec_cost_of_trace costmap itrace. 54 55 lemma obs_exec_steps_with_obs : ∀pcs,p,m1,m2,obs1,obs2. 56 observables pcs p m1 m2 = return 〈obs1,obs2〉 → 57 ∃s1,s2. 58 exec_steps_with_obs pcs p m1 = return 〈s1,obs1〉 ∧ 59 exec_steps_with_obs pcs p (m1+m2) = return 〈s2,obs1@obs2〉. 60 #pcs #p #m1 #m2 #obs1 #obs2 #OBS 61 @('bind_inversion OBS) OBS #s0 #INIT #OBS 62 @('bind_inversion OBS) OBS * #tr1 #s1 #EXEC1 #OBS 63 @('bind_inversion OBS) OBS * #tr2 #s2 #EXEC2 @breakup_pair #OBS 64 whd in OBS:(??%%); destruct 65 %{s1} %{s2} 66 whd in ⊢ (?(??%?)(??%?)); >INIT 67 whd in ⊢ (?(??%?)(??%?)); >EXEC1 >(exec_steps_join … EXEC1 EXEC2) 68 whd in ⊢ (?(??%?)(??%?)); 69 % [ %  >int_trace_append' @breakup_pair @breakup_pair % ] 70 qed. 71 72 lemma bigsum_append : ∀A,l1,l2. ∀f:A → ℕ. 73 (Σ_{l ∈ (l1@l2)}(f l)) = (Σ_{l ∈ l1}(f l)) + (Σ_{l ∈ l2}(f l)). 74 #A #l1 elim l1 75 [ #l2 #f % 76  #h #tl #IH #l2 #f whd in ⊢ (??%(?%?)); >IH // 77 ] qed. 78 79 lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs. 80 observables pcs p m1 m2 = return 〈obs1,obs2〉 → 81 clock_after pcs p m1 costs = return c1 → 82 clock_after pcs p (m1+m2) costs = return c2 → 83 c2  c1 = exec_cost_of_trace costs obs2. 84 #pcs #p #m1 #m2 #obs1 #obs2 #c1 #c2 #costs #OBS 85 cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2 86 whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2 87 whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct 88 >filter_map_append >bigsum_append /2/ 89 qed. 49 90 50 91 include "common/AssocList.ma". … … 61 102 (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) → 62 103 ∀c1,c2. 63 cl ight_clock_after(c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →64 cl ight_clock_after (c_labelled_clight … p) m2(c_clight_cost_map … p) = OK … c2 →104 clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 → 105 clock_after Clight_pcs (c_labelled_clight … p) (m1+m2) (c_clight_cost_map … p) = OK … c2 → 65 106 ∃n1,n2. 66 107 observables Clight_pcs (c_labelled_clight … p) m1 m2 = … … 70 111 minus c2 c1 = clock … (execute n2 ? initial_status)  clock … (execute n1 ? initial_status). 71 112 72 include "common/ExtraMonads.ma".73 74 113 include "Clight/SwitchAndLabel.ma". 114 115 include "common/FEMeasurable.ma". 116 include "Clight/SimplifyCastsMeasurable.ma". 117 include "Clight/toCminorMeasurable.ma". 118 include "Cminor/toRTLabsCorrectness.ma". 119 120 lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max. 121 measurable pcs p m1 m2 stack_cost max → 122 ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉. 123 #pcs #p #m1 #m2 #stack_cost #max 124 * #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_ 125 % [2: % [2: 126 whd in ⊢ (??%?); >INIT in ⊢ (??%?); 127 whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?); 128 whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?); 129 whd in ⊢ (??%?); @breakup_pair % 130  skip ] skip ] 131 qed. 75 132 76 133 theorem correct : … … 115 172 #E >E 116 173 @switch_and_labelling_sim @NOT_WRONG 117  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf 118 174  cut (labelled = cl_labelled) [ whd in EQ_front_end:(??%%); destruct % ] 175 #El >El 176 #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf 177 cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS 178 >(clock_diff_eq_obs … OBS c1_prf c2_prf) c1 c2 179 cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas) 180 #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; m1 m2 181 cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas) 182 #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs simp_m1 simp_m2 183 cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas) 184 #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs cm_m1 cm_m2 185 #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS) 186 #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs' 187 >OBS ra_meas 188 189 (* So, we have for RTLabs: 190 ra_exec_prefix  after [ra_m1] steps we get to [ra_s1] with observables [prefix], 191 ra_tlr  structured trace from [ra_s1] to some [ra_s2], 192 ra_unrepeating  PCs don't repeat locally in [ra_tlr] 193 ra_obs'  the observables from [ra_tlr] are [subtrace] 194 ra_max  the stack bound is respected in [prefix@subtrace] 195 *) 196 197 198 (* Old, semiformal cut 119 199 cut (∀n,s1,s2,obs1,obs2. 120 200 exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 → … … 125 205 observables (OC_preclassified_system (c_labelled_object_code … p)) 126 206 (c_labelled_object_code … p) m p = return 〈obs1, obs2〉) 127 207 *) 128 208 129 209 130 210 131 132 (* start of old simulates133 134 (* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after135 [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]136 according to the [stack_cost] function. *)137 axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.138 axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.139 140 141 let cl_trace ≝ exec_inf … clight_fullexec labelled in142 let asm_trace ≝ exec_inf … ASM_fullexec object_code in143 not_wrong ? cl_trace →144 ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →145 𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'146 147 *)148 149 (* TODO150 151 152 ∀input_program.153 ! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program154 155 exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled156 157 ∧158 159 exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code160 (* Should we be lifting labels in some way here? *)161 162 ∧163 164 ∀i,f : clight_status.165 Clight_labelled i →166 Clight_labelled f →167 ∀mx,time.168 let trace ≝ exec_inf_aux … clight_fullexec labelled i in169 will_return O O mx time f trace →170 mx < max_allowed_stack →171 ∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧172 time = clock f'  clock i'.173 174 175 ∀s,flat.176 let ge ≝ (globalenvs … labelled) in177 subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →178 RTLabs_cost s = true →179 ∀WR : will_return ge 0 s flat.180 let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in181 let labels_rtlabs ≝ flat_label_trace … flat WR in182 ∃!initial,final,structured_trace_asm.183 structured_trace_rtlabs ≈ structured_trace_asm ∧184 clock … code_memory … final = clock … code_memory … initial +185 (Σ_{i < labels_rtlabs} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k  None ⇒ 0 ])).186 187 188 189 What is ≃l? Must show that "labelled" does everything that190 "input_program" does, without getting lost in some191 nonterminating loop part way.192 193 *)194
Note: See TracChangeset
for help on using the changeset viewer.