source: src/correctness.ma @ 3145

Last change on this file since 3145 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 12.4 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 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
48include "ASM/CostsProof.ma".
49
50lemma 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
56cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2
57whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2
58whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct
59>costlabels_of_observables_append >fold_sum' >commutative_plus @sym_eq @minus_plus_m_m
60qed.
61
62definition simulates ≝
63  λp: compiler_output.
64  let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in
65  ∀m1,m2.
66   measurable Clight_pcs (c_labelled_clight … p) m1 m2
67    (stack_sizes (c_stack_cost … p)) (c_max_stack … p) →
68  ∀c1,c2.
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 →
71  ∃n1,n2.
72   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
73   observables (OC_preclassified_system (c_labelled_object_code … p))
74    (c_labelled_object_code … p) n1 n2
75  ∧
76   clock ?? (execute (n1 + n2) ? initial_status) =
77    plus (clock ?? (execute n1 ? initial_status)) (minus c2 c1).
78
79include "Clight/SwitchAndLabel.ma".
80
81include "common/FEMeasurable.ma".
82include "Clight/SimplifyCastsMeasurable.ma".
83include "Clight/toCminorMeasurable.ma".
84include "Cminor/toRTLabsCorrectness.ma".
85
86(* atm they are all axioms *)
87include "RTLabs/RTLabsExecToTrace.ma".
88include "RTLabs/RTLabsToRTLAxiom.ma".
89include "RTL/RTL_separate_to_overflow.ma".
90include "RTL/RTL_overflow_to_unique.ma".
91include "RTL/RTLToERTLAxiom.ma".
92include "ERTL/ERTLToLTLAxiom.ma".
93include "LTL/LTLToLINAxiom.ma".
94include "LIN/LINToASMAxiom.ma".
95
96include "ASM/AssemblyAxiom.ma".
97include "ASM/OC_traces_to_exec.ma".
98
99lemma 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 ]
110qed.
111
112record 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
125lemma front_end_correct :
126∀observe, input_program, init_cost, labelled, p_rtlabs.
127front_end observe input_program = return 〈init_cost, labelled, p_rtlabs〉 →
128not_wrong … (exec_inf … clight_fullexec input_program) →
129sim_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
140whd in EQ_front_end:(??%?);
141letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
142inversion (clight_label cl_switch_removed)
143#cl_labelled #init_cost #CL_LABELLED
144whd in ⊢ (??%? → ?);
145letin 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 #_
149letin rtlabs ≝ (cminor_to_rtlabs cminor)
150whd 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
160cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
161cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
162#simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %;
163cases (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
165cases (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
170cases (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
176qed.
177
178lemma back_end_correct :
179∀observe,init_cost,p_rtlabs,p_asm,init_cost',stack_m,max_stack,prefix,subtrace,fn.
180back_end observe init_cost p_rtlabs = return 〈〈p_asm, init_cost'〉,stack_m,max_stack〉 →
181back_end_preconditions p_rtlabs (stack_sizes stack_m) max_stack prefix subtrace fn →
182init_cost = init_cost' ∧
183∀sigma,pol.
184ft_and_tlr (ASM_status p_asm sigma pol)
185prefix 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
194whd in ⊢ (??%%→?); #EQ destruct(EQ)
195letin p_rtl ≝ (rtlabs_to_rtl init_cost p_rtlabs)
196letin p_ertl ≝ (rtl_to_ertl p_rtl)
197letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
198letin p_lin ≝ (ltl_to_lin p_ltl)
199letin stack_model ≝ (\snd (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
200letin stack_sizes ≝ (stack_sizes stack_model)
201*
202#ra_init #ra_init_ok #ra_max #ra_ft_tlr %[%]
203#sigma #pol
204
205cases (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
210cases (status_simulation_produce_ft_and_tlr … prefix subtrace fn … simul_ra_rtl ra_ft_tlr)
211change with (state_pc RTL_semantics_separate) in rtl_init;
212change 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
217lapply (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
225cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok)
226#rtl_init' * #rtl_init_ok' * #R_rtl #simul_rtl
227lapply (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
230cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok')
231#ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl
232lapply (status_simulation_produce_ft_and_tlr … simul_rtl_ertl rtl_ft_tlr)
233-rtl_init -rtl_init' -R_rtl_ertl #ertl_ft_tlr
234
235lapply (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
238lapply (status_simulation_produce_ft_and_tlr … simul_ertl_ltl ertl_ft_tlr)
239-ertl_init -R_ertl_ltl #ltl_ft_tlr
240
241cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_init_ok)
242#lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
243lapply (status_simulation_produce_ft_and_tlr … simul_ltl_lin ltl_ft_tlr)
244-ltl_init -R_ltl_lin #lin_ft_tlr
245
246cases (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)
249qed.
250
251lemma assembler_correct :
252∀observe,input_program,output_program,prefix,subtrace,fn.
253assembler 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)) →
256ft_and_tlr (OC_abstract_status output_program)
257prefix 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
261whd in ⊢ (??%%→?); #H lapply (sym_eq ??? H) -H #EQ destruct(EQ)
262#H lapply (H sigma pol) -H
263
264cases (assembly_ok p_asm … jump_expansion_ok)
265#R_asm_oc #simul_asm_oc
266@(status_simulation_produce_ft_and_tlr … simul_asm_oc)
267qed.
268
269theorem correct :
270  ∀observe.
271  ∀input_program,output.
272  compile observe input_program = return output →
273  not_wrong … (exec_inf … clight_fullexec input_program) →
274  sim_with_labels
275   (exec_inf … clight_fullexec input_program)
276   (exec_inf … clight_fullexec (c_labelled_clight … output))
277  ∧
278  simulates output.
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
283*** #p_asm' #init_cost' #stack_costs #max_stack #EQ_back_end normalize nodelta
284#H @('bind_inversion H) -H #p_oc #EQ_assembler
285whd in ⊢ (??%%→?); #EQ destruct(EQ) #NOT_WRONG
286
287cases (front_end_correct … EQ_front_end NOT_WRONG) #H1 #H2
288%{H1} #m1 #m2 #m1_m2_meas
289#c1 #c2 #c1_prf #c2_prf
290cases (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
293
294cases (back_end_correct … EQ_back_end back_end_pre) #EQ destruct(EQ)
295#assembler_pre
296cases (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
298
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]
308qed.
Note: See TracBrowser for help on using the repository browser.