source: src/correctness.ma @ 3104

Last change on this file since 3104 was 3096, checked in by tranquil, 7 years ago

preliminary work on closing correctness.ma

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
18definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
19λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
20
21let rec foldl_exists_aux (A,B:Type[0]) (l,l':list B) (f:A → ∀b:B. Exists … (λx.x=b) l → A) (a:A) on l' : (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A ≝
22match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
23[ nil ⇒ λ_. a
24| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
25].
26[ %1 %
27| #b #H' @H %2 @H'
28] qed.
29
30definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝
31λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).
32
33lemma Exists_lift : ∀A,P,Q,l.
34  (∀x. P x → Q x) →
35  Exists A P l →
36  Exists A Q l.
37#A #P #Q #l elim l
38[ //
39| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
40] qed.
41
42include "RTLabs/MeasurableToStructured.ma".
43include "common/ExtraMonads.ma".
44
45definition exec_cost_of_trace : (costlabel → ℕ) → list intensional_event → nat ≝
46λcostmap,itrace.
47  let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
48  Σ_{l ∈ ctrace}(costmap l).
49
50definition 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
55lemma 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
64whd in OBS:(??%%); destruct
65%{s1} %{s2}
66whd in ⊢ (?(??%?)(??%?)); >INIT
67whd in ⊢ (?(??%?)(??%?)); >EXEC1 >(exec_steps_join … EXEC1 EXEC2)
68whd in ⊢ (?(??%?)(??%?));
69% [ % | >int_trace_append' @breakup_pair @breakup_pair % ]
70qed.
71
72lemma 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
79lemma 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
85cases (obs_exec_steps_with_obs … OBS) #s1 * #s2 * #EXEC1 #EXEC2
86whd in ⊢ (??%? → ??%? → ?); >EXEC1 >EXEC2
87whd in ⊢ (??%% → ??%% → ?); #C1 #C2 destruct
88>filter_map_append >bigsum_append >commutative_plus @sym_eq @minus_plus_m_m
89qed.
90
91include "common/AssocList.ma".
92
93definition lookup_stack_cost : stack_cost_model → ident → option nat ≝
94 λstack_cost,id.
95  assoc_list_lookup ?? id (eq_identifier …) stack_cost.
96
97definition simulates ≝
98  λp: compiler_output.
99  let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in
100  ∀m1,m2.
101   measurable Clight_pcs (c_labelled_clight … p) m1 m2
102    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
103  ∀c1,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 →
106  ∃n1,n2.
107   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
108   observables (OC_preclassified_system (c_labelled_object_code … p))
109    (c_labelled_object_code … p) n1 n2
110  ∧
111   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
112
113include "Clight/SwitchAndLabel.ma".
114
115include "common/FEMeasurable.ma".
116include "Clight/SimplifyCastsMeasurable.ma".
117include "Clight/toCminorMeasurable.ma".
118include "Cminor/toRTLabsCorrectness.ma".
119
120(* atm they are all axioms *)
121include "RTLabs/RTLabsExecToTrace.ma".
122include "RTLabs/RTLabsToRTLAxiom.ma".
123include "RTL/RTL_separate_to_overflow.ma".
124include "RTL/RTL_overflow_to_unique.ma".
125include "RTL/RTLToERTLAxiom.ma".
126include "ERTL/ERTLToLTLAxiom.ma".
127include "LTL/LTLToLINAxiom.ma".
128include "LIN/LINToASMAxiom.ma".
129include "ASM/AssemblyAxiom.ma".
130
131lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max.
132  measurable pcs p m1 m2 stack_cost max →
133  ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉.
134#pcs #p #m1 #m2 #stack_cost #max
135* #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_
136% [2: % [2:
137  whd in ⊢ (??%?); >INIT in ⊢ (??%?);
138  whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?);
139  whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?);
140  whd in ⊢ (??%?); @breakup_pair %
141| skip ]| skip ]
142qed.
143
144theorem correct :
145  ∀observe.
146  ∀input_program,output.
147  compile observe input_program = return output →
148  not_wrong … (exec_inf … clight_fullexec input_program) →
149  sim_with_labels
150   (exec_inf … clight_fullexec input_program)
151   (exec_inf … clight_fullexec (c_labelled_clight … output))
152  ∧
153  simulates output.
154#observe #p_in #out
155#H @('bind_inversion H) -H
156** #init_cost #labelled #p_rtlabs #EQ_front_end
157#H @('bind_inversion H) -H
158** #p_asm #stack_costs #globals_size
159#H @('bind_inversion H) -H
160#p_asm'
161#H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm
162whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
163#H @('bind_inversion H) -H
164#p_loc #EQ_assembler
165whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
166
167whd in EQ_front_end:(??%?);
168letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
169lapply (refl ? (clight_label cl_switch_removed))
170cases (clight_label ?) in ⊢ (???% → %); #cl_labelled #init_cost' #CL_LABELLED
171whd in ⊢ (??%? → ?);
172letin cl_simplified ≝ (simplify_program ?)
173#H @('bind_inversion H) -H #cminor #CMINOR
174#H @('bind_inversion H) -H #WCL #_
175#H @('bind_inversion H) -H #INJ #_
176letin rtlabs ≝ (cminor_to_rtlabs cminor)
177#EQ_front_end
178
179#NOT_WRONG %
180[ whd in EQ_front_end:(??%%); destruct
181  cut (labelled = \fst (clight_label cl_switch_removed))
182  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
183  #E >E
184  @switch_and_labelling_sim @NOT_WRONG
185| cut (labelled = cl_labelled) [ whd in EQ_front_end:(??%%); destruct % ]
186  #El >El
187  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
188  cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
189  >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2
190  cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
191  #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; -m1 -m2
192  cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas)
193  #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2
194  cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas)
195  #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
196  #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
197  #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
198  >OBS -ra_meas
199  cases (produce_rtlabs_flat_trace … ra_exec_prefix)
200  #ra_init * #ra_init_ok * #ra_ft #EQ_ra_pref_obs
201  letin p_rtl ≝ (rtlabs_to_rtl init_cost (cminor_to_rtlabs cminor))
202  letin p_ertl ≝ (rtl_to_ertl p_rtl)
203  letin p_ltl ≝ (\fst (\fst (ertl_to_ltl compute_fixpoint colour_graph p_ertl)))
204  letin p_lin ≝ (ltl_to_lin p_ltl)
205  letin stack_sizes ≝ (lookup_stack_cost (\snd (\fst
206    (ertl_to_ltl compute_fixpoint colour_graph p_ertl))))
207  cases (RTLabsToRTL_ok stack_sizes init_cost … ra_init_ok)
208  [2: cases daemon ]
209  #rtl_init * #rtl_init_ok * #R_ra_rtl #simul_ra_rtl
210  cases (status_simulation_produce_ft_and_tlr … ra_ft ra_tlr simul_ra_rtl)
211  change with (state_pc RTL_semantics_separate) in rtl_init;
212  change with (state_pc RTL_semantics_separate → ?)
213  #rtl_st2 * change with (state_pc RTL_semantics_separate → ?)
214  #rtl_st3 * change with (state_pc RTL_semantics_separate → ?)
215  #rtl_st4 * #rtl_ft * #rtl_tlr * #rtl_taaf ** #_ -rtl_st4
216  #rtl_ft_ok #rtl_tlr_ok
217  cases (RTL_separate_to_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
218    rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
219  [2,3: cases daemon (* good stack usage, consequence of ra_max *) ]
220  #rtl_ft' * #rtl_tlr' * #rtl_ft_ok' #rtl_tlr_ok'
221  cases (RTL_separate_to_unique_ok stack_sizes p_rtl rtl_init rtl_init_ok)
222  #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
223  cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
224  #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
225  #rtl_ft_ok'' #rtl_tlr_ok''
226  cases (RTLToERTL_ok stack_sizes p_rtl rtl_init' rtl_init_ok'')
227  #ertl_init * #ertl_init_ok * #R_rtl_ertl #simul_rtl_ertl
228  cases (status_simulation_produce_ft_and_tlr … rtl_ft'' rtl_tlr'' simul_rtl_ertl)
229  #ertl_st2 * #ertl_st3 * #ertl_st4 * #ertl_ft * #ertl_tlr * #ertl_taaf ** #_ -ertl_st4
230  #ertl_ft_ok #ertl_tlr_ok
231  lapply (ERTLToLTL_ok compute_fixpoint colour_graph p_ertl)
232  @pair_elim' @pair_elim' #aux cases (aux ertl_init ertl_init_ok) -aux
233  #ltl_init * #ltl_init_ok * #R_ertl_ltl #simul_ertl_ltl
234  cases (status_simulation_produce_ft_and_tlr … ertl_ft ertl_tlr simul_ertl_ltl)
235  #ltl_st2 * #ltl_st3 * #ltl_st4 * #ltl_ft * #ltl_tlr * #ltl_taaf ** #_ -ltl_st4
236  #ltl_ft_ok #ltl_tlr_ok
237  cases (LTLToLIN_ok stack_sizes p_ltl ltl_init ltl_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
242  @('bind_inversion EQ_assembler) ** #sigma #pol #sigma_pol_ok -EQ_assembler
243  #EQ lapply (opt_eq_from_res ???? EQ) #jump_expansion_ok -EQ
244  whd in ⊢ (??%%→?); #EQ
245  cut (p_loc = assembly p_asm' (λx.sigma x) (λx.pol x))
246  [ -EQ_ra_pref_obs -ra_obs' -ra_exec_prefix -ltl_init_ok -jump_expansion_ok
247    -rtl_init -rtl_ft'' -ltl_ft -lin_init -ltl_init -ertl_init -rtl_init'
248    -El destruct(EQ) % ] #EQ_p_loc -EQ
249   
250  @@@@
251   
252  cases (LINToASM_ok stack_sizes p_lin p_asm' sigma pol EQ_lin_to_asm lin_init lin_init_ok)
253  #lin_init * #lin_init_ok * #R_ltl_lin #simul_ltl_lin
254  cases (status_simulation_produce_ft_and_tlr … ltl_ft ltl_tlr simul_ltl_lin)
255  #lin_st2 * #lin_st3 * #lin_st4 * #lin_ft * #lin_tlr * #lin_taaf ** #_ -lin_st4
256  #lin_ft_ok #lin_tlr_ok
257 
258 
259 
260 
261  #rtl_init' * #rtl_init_ok'' * #R_rtl #simul_rtl
262  cases (status_simulation_produce_ft_and_tlr … rtl_ft' rtl_tlr' simul_rtl)
263  #rtl_st2' * #rtl_st3' * #rtl_st4' * #rtl_ft'' * #rtl_tlr'' * #rtl_taaf ** #_ -rtl_st4'
264  #rtl_ft_ok'' #rtl_tlr_ok''
265 
266 
267  [2: @rtl_init_ok
268  RTL_overflow_produce_ft_and_tlr stack_sizes p_rtl fn
269    rtl_init rtl_st2 rtl_st3 rtl_ft rtl_tlr ??)
270  )
271  #aux lapply (aux rtl_init rtl_st2 rtl_st3) -aux #aux
272  lapply (aux rtl_ft rtl_tlr) ??)
273  cases (RTLToERTL_ok stack_sizes init_cost … ra_init_ok)
274 
275  [5:
276  cut (∀p : rtlabs_program.∀n : ℕ.∀st,tr.
277    exec_steps_with_obs RTLabs_ext_pcs p n = return 〈st, tr〉 →
278   
279  (* So, we have for RTLabs:
280     ra_exec_prefix - after [ra_m1] steps we get to [ra_s1] with observables [prefix],
281     ra_tlr         - structured trace from [ra_s1] to some [ra_s2],
282     ra_unrepeating - PCs don't repeat locally in [ra_tlr]
283     ra_obs'        - the observables from [ra_tlr] are [subtrace]
284     ra_max         - the stack bound is respected in [prefix@subtrace]
285   *)
286
287
288(* Old, semiformal cut
289cut (∀n,s1,s2,obs1,obs2.
290          exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
291            ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2.
292            tlr_observables … tlr (function_of … s1) = obs2 →
293            (* maybe instead of function_of the called id can rather be obtained from execution? *)
294     ∃m,p,s_fin.
295   observables (OC_preclassified_system (c_labelled_object_code … p))
296    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
297    *)
298     
299             
300             
Note: See TracBrowser for help on using the repository browser.