source: src/correctness.ma @ 3115

Last change on this file since 3115 was 3115, checked in by campbell, 7 years ago

Clean up some left-over lemmas and move comment back into place.

File size: 11.2 KB
RevLine 
[1996]1
2include "compiler.ma".
3
4include "ASM/Interpret2.ma".
5
[2802]6include "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]18include "RTLabs/MeasurableToStructured.ma".
[3074]19include "common/ExtraMonads.ma".
[2399]20
[3074]21definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝
22λcostmap,itrace.
[3021]23  let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
[3074]24  Σ_{l ∈ ctrace}(costmap l).
[2399]25
[3074]26definition 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
31lemma 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
40whd in OBS:(??%%); destruct
41%{s1} %{s2}
42whd in ⊢ (?(??%?)(??%?)); >INIT
43whd in ⊢ (?(??%?)(??%?)); >EXEC1 >(exec_steps_join … EXEC1 EXEC2)
44whd in ⊢ (?(??%?)(??%?));
45% [ % | >int_trace_append' @breakup_pair @breakup_pair % ]
46qed.
47
48lemma bigsum_append : ∀A,l1,l2. ∀f:A → ℕ.
49  (Σ_{l ∈ (l1@l2)}(f l)) = (Σ_{l ∈ l1}(f l)) + (Σ_{l ∈ l2}(f l)).
50#A #l1 elim l1
51[ #l2 #f %
52| #h #tl #IH #l2 #f whd in ⊢ (??%(?%?)); >IH //
53] qed.
54
55lemma clock_diff_eq_obs : ∀pcs,p,m1,m2,obs1,obs2,c1,c2,costs.
56  observables pcs p m1 m2 = return 〈obs1,obs2〉 →
57  clock_after pcs p m1 costs = return c1 →
58  clock_after pcs p (m1+m2) costs = return c2 →
59  c2 - c1 = exec_cost_of_trace costs obs2.
60#pcs #p #m1 #m2 #obs1 #obs2 #c1 #c2 #costs #OBS
61cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2
62whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2
63whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct
[3096]64>filter_map_append >bigsum_append >commutative_plus @sym_eq @minus_plus_m_m
[3074]65qed.
66
[2774]67include "common/AssocList.ma".
68
[3003]69definition lookup_stack_cost : stack_cost_model → ident → option nat ≝
[2774]70 λstack_cost,id.
[3003]71  assoc_list_lookup ?? id (eq_identifier …) stack_cost.
[2774]72
[2322]73definition simulates ≝
[2774]74  λp: compiler_output.
[3003]75  let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in
[2774]76  ∀m1,m2.
77   measurable Clight_pcs (c_labelled_clight … p) m1 m2
78    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
79  ∀c1,c2.
[3074]80   clock_after Clight_pcs (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
81   clock_after Clight_pcs (c_labelled_clight … p) (m1+m2) (c_clight_cost_map … p) = OK … c2 →
[2774]82  ∃n1,n2.
83   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
[2875]84   observables (OC_preclassified_system (c_labelled_object_code … p))
85    (c_labelled_object_code … p) n1 n2
[2774]86  ∧
[2765]87   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
[2322]88
[3047]89include "Clight/SwitchAndLabel.ma".
90
[3074]91include "common/FEMeasurable.ma".
92include "Clight/SimplifyCastsMeasurable.ma".
93include "Clight/toCminorMeasurable.ma".
94include "Cminor/toRTLabsCorrectness.ma".
95
[3096]96(* atm they are all axioms *)
97include "RTLabs/RTLabsExecToTrace.ma".
98include "RTLabs/RTLabsToRTLAxiom.ma".
99include "RTL/RTL_separate_to_overflow.ma".
100include "RTL/RTL_overflow_to_unique.ma".
101include "RTL/RTLToERTLAxiom.ma".
102include "ERTL/ERTLToLTLAxiom.ma".
103include "LTL/LTLToLINAxiom.ma".
104include "LIN/LINToASMAxiom.ma".
105include "ASM/AssemblyAxiom.ma".
106
[3074]107lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max.
108  measurable pcs p m1 m2 stack_cost max →
109  ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉.
110#pcs #p #m1 #m2 #stack_cost #max
111* #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_
112% [2: % [2:
113  whd in ⊢ (??%?); >INIT in ⊢ (??%?);
114  whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?);
115  whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?);
116  whd in ⊢ (??%?); @breakup_pair %
117| skip ]| skip ]
118qed.
119
[3030]120theorem correct :
[2852]121  ∀observe.
[2774]122  ∀input_program,output.
[2852]123  compile observe input_program = return output →
[2322]124  not_wrong … (exec_inf … clight_fullexec input_program) →
[2774]125  sim_with_labels
126   (exec_inf … clight_fullexec input_program)
127   (exec_inf … clight_fullexec (c_labelled_clight … output))
[2322]128  ∧
[2774]129  simulates output.
[2928]130#observe #p_in #out
131#H @('bind_inversion H) -H
132** #init_cost #labelled #p_rtlabs #EQ_front_end
133#H @('bind_inversion H) -H
134** #p_asm #stack_costs #globals_size
135#H @('bind_inversion H) -H
136#p_asm'
137#H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm
138whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
139#H @('bind_inversion H) -H
140#p_loc #EQ_assembler
141whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
[3022]142
[3030]143whd in EQ_front_end:(??%?);
144letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
145lapply (refl ? (clight_label cl_switch_removed))
146cases (clight_label ?) in ⊢ (???% → %); #cl_labelled #init_cost' #CL_LABELLED
147whd in ⊢ (??%? → ?);
148letin cl_simplified ≝ (simplify_program ?)
149#H @('bind_inversion H) -H #cminor #CMINOR
[3022]150#H @('bind_inversion H) -H #WCL #_
151#H @('bind_inversion H) -H #INJ #_
[3030]152letin rtlabs ≝ (cminor_to_rtlabs cminor)
153#EQ_front_end
[3022]154
[2928]155#NOT_WRONG %
[3047]156[ whd in EQ_front_end:(??%%); destruct
157  cut (labelled = \fst (clight_label cl_switch_removed))
158  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
159  #E >E
160  @switch_and_labelling_sim @NOT_WRONG
[3074]161| cut (labelled = cl_labelled) [ whd in EQ_front_end:(??%%); destruct % ]
162  #El >El
163  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
164  cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
165  >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2
166  cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
167  #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; -m1 -m2
168  cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas)
169  #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2
170  cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas)
171  #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
172  #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
173  #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
174  >OBS -ra_meas
[3115]175   
176  (* So, after the front-end we have for RTLabs:
177     ra_exec_prefix - after [ra_m1] steps we get to [ra_s1] with observables [prefix],
178     ra_tlr         - structured trace from [ra_s1] to some [ra_s2],
179     ra_unrepeating - PCs don't repeat locally in [ra_tlr]
180     ra_obs'        - the observables from [ra_tlr] are [subtrace]
181     ra_max         - the stack bound is respected in [prefix@subtrace]
182   *)
183
[3096]184  cases (produce_rtlabs_flat_trace … ra_exec_prefix)
185  #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
186  letin p_rtl ≝ (rtlabs_to_rtl init_cost (cminor_to_rtlabs cminor))
187  letin p_ertl ≝ (rtl_to_ertl p_rtl)
188  letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
189  letin p_lin ≝ (ltl_to_lin p_ltl)
190  letin stack_sizes ≝ (lookup_stack_cost (\snd (\fst
191    (ertl_to_ltl compute_fixpoint colour_graph p_ertl))))
192  cases (RTLabsToRTL_ok stack_sizes init_cost … ra_init_ok)
193  [2: cases daemon ]
194  #rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl
195  cases (status_simulation_produce_ft_and_tlr … ra_ft ra_tlr simul_ra_rtl)
196  change with (state_pc RTL_semantics_separate) in rtl_init;
197  change with (state_pc RTL_semantics_separate → ?)
198  #rtl_st2 * change with (state_pc RTL_semantics_separate → ?)
199  #rtl_st3 * change with (state_pc RTL_semantics_separate → ?)
200  #rtl_st4 * #rtl_ft * #rtl_tlr * #rtl_taaf ** #_ -rtl_st4
201  #rtl_ft_ok #rtl_tlr_ok
202  cases (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
203    rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
204  [2,3: cases daemon (* good stack usage, consequence of ra_max *) ]
205  #rtl_ft' * #rtl_tlr' * #rtl_ft_ok' #rtl_tlr_ok'
206  cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok)
207  #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
208  cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
209  #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
210  #rtl_ft_ok'' #rtl_tlr_ok''
211  cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok'')
212  #ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl
213  cases (status_simulation_produce_ft_and_tlr … rtl_ft'' rtl_tlr'' simul_rtl_ertl)
214  #ertl_st2 * #ertl_st3 * #ertl_st4 * #ertl_ft * #ertl_tlr * #ertl_taaf ** #_ -ertl_st4
215  #ertl_ft_ok #ertl_tlr_ok
216  lapply (ERTLToLTL_ok compute_fixpoint colour_graph p_ertl)
217  @pair_elim' @pair_elim' #aux cases (aux ertl_init ertl_init_ok) -aux
218  #ltl_init * #ltl_init_ok * #R_ertl_ltl #simul_ertl_ltl
219  cases (status_simulation_produce_ft_and_tlr … ertl_ft ertl_tlr simul_ertl_ltl)
220  #ltl_st2 * #ltl_st3 * #ltl_st4 * #ltl_ft * #ltl_tlr * #ltl_taaf ** #_ -ltl_st4
221  #ltl_ft_ok #ltl_tlr_ok
222  cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok)
223  #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
224  cases (status_simulation_produce_ft_and_tlr … ltl_ft ltl_tlr simul_ltl_lin)
225  #lin_st2 * #lin_st3 * #lin_st4 * #lin_ft * #lin_tlr * #lin_taaf ** #_ -lin_st4
226  #lin_ft_ok #lin_tlr_ok
227  @('bind_inversion EQ_assembler) ** #sigma #pol #sigma_pol_ok -EQ_assembler
228  #EQ lapply (opt_eq_from_res ???? EQ) #jump_expansion_ok -EQ
229  whd in ⊢ (??%%→?); #EQ
230  cut (p_loc = assembly p_asm' (λx.sigma x) (λx.pol x))
231  [ -EQ_ra_pref_obs -ra_obs' -ra_exec_prefix -ltl_init_ok -jump_expansion_ok
232    -rtl_init -rtl_ft'' -ltl_ft -lin_init -ltl_init -ertl_init -rtl_init'
233    -El destruct(EQ) % ] #EQ_p_loc -EQ
234   
235  @@@@
236   
237  cases (LINToASM_ok stack_sizes p_lin p_asm' sigma pol EQ_lin_to_asm lin_init lin_init_ok)
238  #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
239  cases (status_simulation_produce_ft_and_tlr … ltl_ft ltl_tlr simul_ltl_lin)
240  #lin_st2 * #lin_st3 * #lin_st4 * #lin_ft * #lin_tlr * #lin_taaf ** #_ -lin_st4
241  #lin_ft_ok #lin_tlr_ok
[3074]242 
[3096]243 
244 
245 
246  #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
247  cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
248  #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
249  #rtl_ft_ok'' #rtl_tlr_ok''
250 
251 
252  [2: @rtl_init_ok
253  RTL_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
254    rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
255  )
256  #aux lapply (aux rtl_init rtl_st2 rtl_st3) -aux #aux
257  lapply (aux rtl_ft rtl_tlr) ??)
258  cases (RTLToERTL_ok stack_sizes init_cost … ra_init_ok)
259 
260  [5:
261  cut (∀p : rtlabs_program.∀n : ℕ.∀st,tr.
262    exec_steps_with_obs RTLabs_ext_pcs p n = return 〈st, tr〉 →
[2928]263
264     
265             
266             
Note: See TracBrowser for help on using the repository browser.