source: src/correctness.ma

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

Rebuild prefix traces in back-end's preferred form.

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