[1996] | 1 | |
---|
| 2 | include "compiler.ma". |
---|
| 3 | |
---|
| 4 | include "ASM/Interpret2.ma". |
---|
| 5 | |
---|
[2802] | 6 | include "Clight/Clight_classified_system.ma". |
---|
[2322] | 7 | |
---|
[2323] | 8 | (* From measurable on Clight, we will end up with an RTLabs flat trace where |
---|
| 9 | we know that there are some m' and n' such that the prefix in Clight matches |
---|
| 10 | the prefix in RTLabs given by m', the next n steps in Clight are equivalent |
---|
| 11 | to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs |
---|
| 12 | for those n' steps so that we can build a corresponding structured trace. |
---|
| 13 | |
---|
| 14 | "Equivalent" here means, in particular, that the observables will be the same, |
---|
| 15 | and those observables will include the stack space costs. |
---|
| 16 | *) |
---|
| 17 | |
---|
[3021] | 18 | include "RTLabs/MeasurableToStructured.ma". |
---|
[3074] | 19 | include "common/ExtraMonads.ma". |
---|
[2399] | 20 | |
---|
[3074] | 21 | definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝ |
---|
| 22 | λcostmap,itrace. |
---|
[3145] | 23 | let ctrace ≝ costlabels_of_observables itrace in |
---|
[3074] | 24 | Σ_{l ∈ ctrace}(costmap l). |
---|
[2399] | 25 | |
---|
[3074] | 26 | definition clock_after : ∀pcs:preclassified_system. ∀p. nat → (costlabel→ℕ) → res nat ≝ |
---|
| 27 | λC,p,n,costmap. |
---|
| 28 | ! 〈s,itrace〉 ← exec_steps_with_obs C p n; |
---|
| 29 | return exec_cost_of_trace costmap itrace. |
---|
| 30 | |
---|
| 31 | lemma obs_exec_steps_with_obs : ∀pcs,p,m1,m2,obs1,obs2. |
---|
| 32 | observables pcs p m1 m2 = return 〈obs1,obs2〉 → |
---|
| 33 | ∃s1,s2. |
---|
| 34 | exec_steps_with_obs pcs p m1 = return 〈s1,obs1〉 ∧ |
---|
| 35 | exec_steps_with_obs pcs p (m1+m2) = return 〈s2,obs1@obs2〉. |
---|
| 36 | #pcs #p #m1 #m2 #obs1 #obs2 #OBS |
---|
| 37 | @('bind_inversion OBS) -OBS #s0 #INIT #OBS |
---|
| 38 | @('bind_inversion OBS) -OBS * #tr1 #s1 #EXEC1 #OBS |
---|
| 39 | @('bind_inversion OBS) -OBS * #tr2 #s2 #EXEC2 @breakup_pair #OBS |
---|
| 40 | whd in OBS:(??%%); destruct |
---|
| 41 | %{s1} %{s2} |
---|
| 42 | whd in ⊢ (?(??%?)(??%?)); >INIT |
---|
| 43 | whd in ⊢ (?(??%?)(??%?)); >EXEC1 >(exec_steps_join … EXEC1 EXEC2) |
---|
| 44 | whd in ⊢ (?(??%?)(??%?)); |
---|
| 45 | % [ % | >int_trace_append' @breakup_pair @breakup_pair % ] |
---|
| 46 | qed. |
---|
| 47 | |
---|
[3145] | 48 | include "ASM/CostsProof.ma". |
---|
[3074] | 49 | |
---|
| 50 | lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs. |
---|
| 51 | observables pcs p m1 m2 = return 〈obs1,obs2〉 → |
---|
| 52 | clock_after pcs p m1 costs = return c1 → |
---|
| 53 | clock_after pcs p (m1+m2) costs = return c2 → |
---|
| 54 | c2 - c1 = exec_cost_of_trace costs obs2. |
---|
| 55 | #pcs #p #m1 #m2 #obs1 #obs2 #c1 #c2 #costs #OBS |
---|
| 56 | cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2 |
---|
| 57 | whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2 |
---|
| 58 | whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct |
---|
[3145] | 59 | >costlabels_of_observables_append >fold_sum' >commutative_plus @sym_eq @minus_plus_m_m |
---|
[3074] | 60 | qed. |
---|
| 61 | |
---|
[2322] | 62 | definition simulates ≝ |
---|
[2774] | 63 | λp: compiler_output. |
---|
[3003] | 64 | let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in |
---|
[2774] | 65 | ∀m1,m2. |
---|
| 66 | measurable Clight_pcs (c_labelled_clight … p) m1 m2 |
---|
[3145] | 67 | (stack_sizes (c_stack_cost … p)) (c_max_stack … p) → |
---|
[2774] | 68 | ∀c1,c2. |
---|
[3074] | 69 | clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 → |
---|
| 70 | clock_after Clight_pcs (c_labelled_clight … p) (m1+m2) (c_clight_cost_map … p) = OK … c2 → |
---|
[2774] | 71 | ∃n1,n2. |
---|
| 72 | observables Clight_pcs (c_labelled_clight … p) m1 m2 = |
---|
[2875] | 73 | observables (OC_preclassified_system (c_labelled_object_code … p)) |
---|
| 74 | (c_labelled_object_code … p) n1 n2 |
---|
[2774] | 75 | ∧ |
---|
[3145] | 76 | clock ?? (execute (n1 + n2) ? initial_status) = |
---|
| 77 | plus (clock ?? (execute n1 ? initial_status)) (minus c2 c1). |
---|
[2322] | 78 | |
---|
[3047] | 79 | include "Clight/SwitchAndLabel.ma". |
---|
| 80 | |
---|
[3074] | 81 | include "common/FEMeasurable.ma". |
---|
| 82 | include "Clight/SimplifyCastsMeasurable.ma". |
---|
| 83 | include "Clight/toCminorMeasurable.ma". |
---|
| 84 | include "Cminor/toRTLabsCorrectness.ma". |
---|
| 85 | |
---|
[3096] | 86 | (* atm they are all axioms *) |
---|
| 87 | include "RTLabs/RTLabsExecToTrace.ma". |
---|
| 88 | include "RTLabs/RTLabsToRTLAxiom.ma". |
---|
| 89 | include "RTL/RTL_separate_to_overflow.ma". |
---|
| 90 | include "RTL/RTL_overflow_to_unique.ma". |
---|
| 91 | include "RTL/RTLToERTLAxiom.ma". |
---|
| 92 | include "ERTL/ERTLToLTLAxiom.ma". |
---|
| 93 | include "LTL/LTLToLINAxiom.ma". |
---|
| 94 | include "LIN/LINToASMAxiom.ma". |
---|
[3145] | 95 | |
---|
[3096] | 96 | include "ASM/AssemblyAxiom.ma". |
---|
[3145] | 97 | include "ASM/OC_traces_to_exec.ma". |
---|
[3096] | 98 | |
---|
[3074] | 99 | lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max. |
---|
| 100 | measurable pcs p m1 m2 stack_cost max → |
---|
| 101 | ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉. |
---|
| 102 | #pcs #p #m1 #m2 #stack_cost #max |
---|
| 103 | * #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_ |
---|
| 104 | % [2: % [2: |
---|
| 105 | whd in ⊢ (??%?); >INIT in ⊢ (??%?); |
---|
| 106 | whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?); |
---|
| 107 | whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?); |
---|
| 108 | whd in ⊢ (??%?); @breakup_pair % |
---|
| 109 | | skip ]| skip ] |
---|
| 110 | qed. |
---|
| 111 | |
---|
[3145] | 112 | record back_end_preconditions (p_rtlabs : RTLabs_program) |
---|
| 113 | (stacksizes : ident → option ℕ) (max_stack : ℕ) |
---|
| 114 | (prefix, subtrace : list intensional_event) (fn : ident) |
---|
| 115 | : Prop ≝ |
---|
| 116 | { ra_init : RTLabs_status (make_global p_rtlabs) |
---|
| 117 | ; ra_init_ok : make_ext_initial_state p_rtlabs = return ra_init |
---|
| 118 | ; ra_max : |
---|
| 119 | le (maximum (update_stacksize_info stacksizes (mk_stacksize_info 0 0) |
---|
| 120 | (extract_call_ud_from_observables (prefix @ subtrace)))) max_stack |
---|
| 121 | ; ra_ft_tlr : ft_and_tlr (RTLabs_status (make_global p_rtlabs)) |
---|
| 122 | prefix subtrace fn ra_init |
---|
| 123 | }. |
---|
| 124 | |
---|
| 125 | lemma front_end_correct : |
---|
| 126 | ∀observe, input_program, init_cost, labelled, p_rtlabs. |
---|
| 127 | front_end observe input_program = return 〈init_cost, labelled, p_rtlabs〉 → |
---|
| 128 | not_wrong … (exec_inf … clight_fullexec input_program) → |
---|
| 129 | sim_with_labels |
---|
| 130 | (exec_inf … clight_fullexec input_program) |
---|
| 131 | (exec_inf … clight_fullexec labelled) |
---|
| 132 | ∧ |
---|
| 133 | ∀m1,m2,stacksizes,max_stack. |
---|
| 134 | measurable Clight_pcs labelled m1 m2 stacksizes max_stack → |
---|
| 135 | ∃prefix, subtrace, fn. |
---|
| 136 | observables Clight_pcs labelled m1 m2 = return 〈prefix, subtrace〉 ∧ |
---|
| 137 | back_end_preconditions p_rtlabs stacksizes max_stack |
---|
| 138 | prefix subtrace fn. |
---|
| 139 | #observe #p_in #init_cost' #labelled #p_rtlabs #EQ_front_end |
---|
| 140 | whd in EQ_front_end:(??%?); |
---|
| 141 | letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end; |
---|
| 142 | inversion (clight_label cl_switch_removed) |
---|
| 143 | #cl_labelled #init_cost #CL_LABELLED |
---|
| 144 | whd in ⊢ (??%? → ?); |
---|
| 145 | letin cl_simplified ≝ (simplify_program ?) |
---|
| 146 | #H @('bind_inversion H) -H #cminor #CMINOR |
---|
| 147 | #H @('bind_inversion H) -H #WCL #_ |
---|
| 148 | #H @('bind_inversion H) -H #INJ #_ |
---|
| 149 | letin rtlabs ≝ (cminor_to_rtlabs cminor) |
---|
| 150 | whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) |
---|
| 151 | |
---|
| 152 | #NOT_WRONG % |
---|
| 153 | [ cut (cl_labelled = \fst (clight_label cl_switch_removed)) |
---|
| 154 | [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ] |
---|
| 155 | #E >E |
---|
| 156 | @switch_and_labelling_sim @NOT_WRONG |
---|
| 157 | ] |
---|
| 158 | |
---|
| 159 | #m1 #m2 #stacksizes #max_stack #m1_m2_meas |
---|
| 160 | cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS |
---|
| 161 | cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas) |
---|
| 162 | #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; |
---|
| 163 | cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas) |
---|
| 164 | #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2 |
---|
| 165 | cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas) |
---|
| 166 | #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2 |
---|
| 167 | #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS) |
---|
| 168 | #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs' |
---|
| 169 | >OBS -ra_meas |
---|
| 170 | cases (produce_rtlabs_flat_trace … ra_exec_prefix) |
---|
| 171 | #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs |
---|
| 172 | %{prefix} %{subtrace} %{fn} %[%] |
---|
| 173 | %{ra_init_ok ra_max} |
---|
| 174 | %{ra_unrepeating EQ_ra_pref_obs ra_obs'} |
---|
| 175 | (* fn is the current function ... *) cases daemon |
---|
| 176 | qed. |
---|
| 177 | |
---|
| 178 | lemma back_end_correct : |
---|
| 179 | ∀observe,init_cost,p_rtlabs,p_asm,init_cost',stack_m,max_stack,prefix,subtrace,fn. |
---|
| 180 | back_end observe init_cost p_rtlabs = return 〈〈p_asm, init_cost'〉,stack_m,max_stack〉 → |
---|
| 181 | back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn → |
---|
| 182 | init_cost = init_cost' ∧ |
---|
| 183 | ∀sigma,pol. |
---|
| 184 | ft_and_tlr (ASM_status p_asm sigma pol) |
---|
| 185 | prefix subtrace fn |
---|
| 186 | (initialise_status ? p_asm). |
---|
| 187 | #observe #init_cost #p_rtlabs #p_asm' #init_cost #stack_model #max_stack |
---|
| 188 | #prefix #subtrace #fn |
---|
| 189 | #H @('bind_inversion H) -H |
---|
| 190 | #p_asm |
---|
| 191 | #H lapply (opt_eq_from_res ???? H) -H |
---|
| 192 | #EQ_lin_to_asm |
---|
| 193 | #H lapply (sym_eq ??? H) -H |
---|
| 194 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
| 195 | letin p_rtl ≝ (rtlabs_to_rtl init_cost p_rtlabs) |
---|
| 196 | letin p_ertl ≝ (rtl_to_ertl p_rtl) |
---|
| 197 | letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl))) |
---|
| 198 | letin p_lin ≝ (ltl_to_lin p_ltl) |
---|
| 199 | letin stack_model ≝ (\snd (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl))) |
---|
| 200 | letin stack_sizes ≝ (stack_sizes stack_model) |
---|
| 201 | * |
---|
| 202 | #ra_init #ra_init_ok #ra_max #ra_ft_tlr %[%] |
---|
| 203 | #sigma #pol |
---|
| 204 | |
---|
| 205 | cases (RTLabsToRTL_ok stack_model init_cost … ra_init_ok) |
---|
| 206 | [2: @(transitive_stack_cost_model_le … (RTLabsToRTL_monotone_stacksizes init_cost …)) |
---|
| 207 | @(transitive_stack_cost_model_le … (RTLToERTL_monotone_stacksizes …)) |
---|
| 208 | @ERTLToLTL_monotone_stacksizes ] |
---|
| 209 | #rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl |
---|
| 210 | cases (status_simulation_produce_ft_and_tlr … prefix subtrace fn … simul_ra_rtl ra_ft_tlr) |
---|
| 211 | change with (state_pc RTL_semantics_separate) in rtl_init; |
---|
| 212 | change with |
---|
| 213 | (state_pc RTL_semantics_separate → state_pc RTL_semantics_separate → ?) |
---|
| 214 | #rtl_st2 #rtl_st3 #rtl_ft #rtl_tlr #rtl_unrepeating #rtl_ft_ok |
---|
| 215 | #current_is_fn #rtl_tlr_ok |
---|
| 216 | |
---|
| 217 | lapply (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes |
---|
| 218 | p_rtl fn … rtl_ft rtl_tlr ??? rtl_unrepeating) try assumption |
---|
| 219 | [ whd whd in match extract_call_ud_from_ft; whd in match extract_call_ud_from_tlr; |
---|
| 220 | normalize nodelta >rtl_ft_ok >rtl_tlr_ok |
---|
| 221 | <extract_call_ud_from_observables_append assumption |
---|
| 222 | ] |
---|
| 223 | >rtl_ft_ok >rtl_tlr_ok #rtl_ft_tlr |
---|
| 224 | |
---|
| 225 | cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok) |
---|
| 226 | #rtl_init' * #rtl_init_ok' * #R_rtl #simul_rtl |
---|
| 227 | lapply (status_simulation_produce_ft_and_tlr … simul_rtl rtl_ft_tlr) |
---|
| 228 | -rtl_ft_tlr #rtl_ft_tlr -R_rtl -rtl_st2 -rtl_st3 -R_ra_rtl -ra_init -ra_max |
---|
| 229 | |
---|
| 230 | cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok') |
---|
| 231 | #ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl |
---|
| 232 | lapply (status_simulation_produce_ft_and_tlr … simul_rtl_ertl rtl_ft_tlr) |
---|
| 233 | -rtl_init -rtl_init' -R_rtl_ertl #ertl_ft_tlr |
---|
| 234 | |
---|
| 235 | lapply (ERTLToLTL_ok compute_fixpoint colour_graph p_ertl) |
---|
| 236 | @pair_elim' @pair_elim' #aux cases (aux ertl_init ertl_init_ok) -aux |
---|
| 237 | #ltl_init * #ltl_init_ok * #R_ertl_ltl #simul_ertl_ltl |
---|
| 238 | lapply (status_simulation_produce_ft_and_tlr … simul_ertl_ltl ertl_ft_tlr) |
---|
| 239 | -ertl_init -R_ertl_ltl #ltl_ft_tlr |
---|
| 240 | |
---|
| 241 | cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok) |
---|
| 242 | #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin |
---|
| 243 | lapply (status_simulation_produce_ft_and_tlr … simul_ltl_lin ltl_ft_tlr) |
---|
| 244 | -ltl_init -R_ltl_lin #lin_ft_tlr |
---|
| 245 | |
---|
| 246 | cases (LINToASM_ok stack_sizes p_lin p_asm sigma pol EQ_lin_to_asm lin_init lin_init_ok) |
---|
| 247 | #R_lin_asm #simul_lin_asm |
---|
| 248 | @(status_simulation_produce_ft_and_tlr … simul_lin_asm lin_ft_tlr) |
---|
| 249 | qed. |
---|
| 250 | |
---|
| 251 | lemma assembler_correct : |
---|
| 252 | ∀observe,input_program,output_program,prefix,subtrace,fn. |
---|
| 253 | assembler observe input_program = return output_program → |
---|
| 254 | (∀sigma,pol.ft_and_tlr (ASM_status input_program sigma pol) prefix subtrace fn |
---|
| 255 | (initialise_status ? input_program)) → |
---|
| 256 | ft_and_tlr (OC_abstract_status output_program) |
---|
| 257 | prefix subtrace fn (initialise_status ? (cm output_program)). |
---|
| 258 | #observe #p_asm #p_oc #prefix #subtrace #fn |
---|
| 259 | #H @('bind_inversion H) -H ** #sigma #pol normalize nodelta #sigma_pol_ok |
---|
| 260 | #H lapply (opt_eq_from_res ???? H) -H #jump_expansion_ok |
---|
| 261 | whd in ⊢ (??%%→?); #H lapply (sym_eq ??? H) -H #EQ destruct(EQ) |
---|
| 262 | #H lapply (H sigma pol) -H |
---|
| 263 | |
---|
| 264 | cases (assembly_ok p_asm … jump_expansion_ok) |
---|
| 265 | #R_asm_oc #simul_asm_oc |
---|
| 266 | @(status_simulation_produce_ft_and_tlr … simul_asm_oc) |
---|
| 267 | qed. |
---|
| 268 | |
---|
[3030] | 269 | theorem correct : |
---|
[2852] | 270 | ∀observe. |
---|
[2774] | 271 | ∀input_program,output. |
---|
[2852] | 272 | compile observe input_program = return output → |
---|
[2322] | 273 | not_wrong … (exec_inf … clight_fullexec input_program) → |
---|
[2774] | 274 | sim_with_labels |
---|
| 275 | (exec_inf … clight_fullexec input_program) |
---|
| 276 | (exec_inf … clight_fullexec (c_labelled_clight … output)) |
---|
[2322] | 277 | ∧ |
---|
[2774] | 278 | simulates output. |
---|
[2928] | 279 | #observe #p_in #out |
---|
| 280 | #H @('bind_inversion H) -H |
---|
| 281 | ** #init_cost #labelled #p_rtlabs #EQ_front_end |
---|
| 282 | #H @('bind_inversion H) -H |
---|
[3145] | 283 | *** #p_asm' #init_cost' #stack_costs #max_stack #EQ_back_end normalize nodelta |
---|
| 284 | #H @('bind_inversion H) -H #p_oc #EQ_assembler |
---|
| 285 | whd in ⊢ (??%%→?); #EQ destruct(EQ) #NOT_WRONG |
---|
[3022] | 286 | |
---|
[3145] | 287 | cases (front_end_correct … EQ_front_end NOT_WRONG) #H1 #H2 |
---|
| 288 | %{H1} #m1 #m2 #m1_m2_meas |
---|
| 289 | #c1 #c2 #c1_prf #c2_prf |
---|
| 290 | cases (H2 … m1_m2_meas) |
---|
| 291 | #prefix * #subtrace * #fn * #OBS #back_end_pre >OBS |
---|
| 292 | >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2 |
---|
[3022] | 293 | |
---|
[3145] | 294 | cases (back_end_correct … EQ_back_end back_end_pre) #EQ destruct(EQ) |
---|
| 295 | #assembler_pre |
---|
| 296 | cases (assembler_correct … EQ_assembler assembler_pre) |
---|
| 297 | #oc_st2 #oc_st3 #oc_ft #oc_tlr #oc_unrepeating #oc_ft_ok #fn_ok #oc_tlr_ok |
---|
[3115] | 298 | |
---|
[3145] | 299 | %{(ft_length … oc_ft)} |
---|
| 300 | %{(tlr_length … oc_tlr)} |
---|
| 301 | % |
---|
| 302 | [ >(OC_traces_to_observables … fn_ok) >oc_ft_ok >oc_tlr_ok % |
---|
| 303 | | >execute_plus >OC_ft_to_execute >OC_tlr_to_execute |
---|
| 304 | whd in match exec_cost_of_trace; normalize nodelta <oc_tlr_ok |
---|
| 305 | >costlabels_of_observables_trace_label_return_id_irrelevant [2: %{one}] |
---|
| 306 | @(compute_max_trace_label_return_cost_ok_with_trace … oc_unrepeating) |
---|
| 307 | ] |
---|
| 308 | qed. |
---|