source: src/correctness.ma @ 3095

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

Put some kind of high level proof in for front-end.

File size: 8.3 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 /2/
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
120lemma measurable_observables : ∀pcs,p,m1,m2,stack_cost,max.
121  measurable pcs p m1 m2 stack_cost max →
122  ∃pre,subtrace. observables pcs p m1 m2 = return 〈pre,subtrace〉.
123#pcs #p #m1 #m2 #stack_cost #max
124* #s0 * #prefix * #s1 * #interesting * #s2 * * * * * #INIT #EXEC1 #EXEC2 #_ #_ #_
125% [2: % [2:
126  whd in ⊢ (??%?); >INIT in ⊢ (??%?);
127  whd in ⊢ (??%?); >EXEC1 in ⊢ (??%?);
128  whd in ⊢ (??%?); >EXEC2 in ⊢ (??%?);
129  whd in ⊢ (??%?); @breakup_pair %
130| skip ]| skip ]
131qed.
132
133theorem correct :
134  ∀observe.
135  ∀input_program,output.
136  compile observe input_program = return output →
137  not_wrong … (exec_inf … clight_fullexec input_program) →
138  sim_with_labels
139   (exec_inf … clight_fullexec input_program)
140   (exec_inf … clight_fullexec (c_labelled_clight … output))
141  ∧
142  simulates output.
143#observe #p_in #out
144#H @('bind_inversion H) -H
145** #init_cost #labelled #p_rtlabs #EQ_front_end
146#H @('bind_inversion H) -H
147** #p_asm #stack_costs #globals_size
148#H @('bind_inversion H) -H
149#p_asm'
150#H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm
151whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
152#H @('bind_inversion H) -H
153#p_loc #EQ_assembler
154whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
155
156whd in EQ_front_end:(??%?);
157letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
158lapply (refl ? (clight_label cl_switch_removed))
159cases (clight_label ?) in ⊢ (???% → %); #cl_labelled #init_cost' #CL_LABELLED
160whd in ⊢ (??%? → ?);
161letin cl_simplified ≝ (simplify_program ?)
162#H @('bind_inversion H) -H #cminor #CMINOR
163#H @('bind_inversion H) -H #WCL #_
164#H @('bind_inversion H) -H #INJ #_
165letin rtlabs ≝ (cminor_to_rtlabs cminor)
166#EQ_front_end
167
168#NOT_WRONG %
169[ whd in EQ_front_end:(??%%); destruct
170  cut (labelled = \fst (clight_label cl_switch_removed))
171  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
172  #E >E
173  @switch_and_labelling_sim @NOT_WRONG
174| cut (labelled = cl_labelled) [ whd in EQ_front_end:(??%%); destruct % ]
175  #El >El
176  #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
177  cases (measurable_observables … m1_m2_meas) #prefix * #subtrace #OBS
178  >(clock_diff_eq_obs … OBS c1_prf c2_prf) -c1 -c2
179  cases (measured_subtrace_preserved simplify_measurable_sim … (refl ??) m1_m2_meas)
180  #simp_m1 * #simp_m2 * #simp_meas #simp_obs >simp_obs in OBS ⊢ %; -m1 -m2
181  cases (measured_subtrace_preserved clight_to_cminor_measurable_sim … CMINOR simp_meas)
182  #cm_m1 * #cm_m2 * #cm_meas #cm_obs >cm_obs -simp_m1 -simp_m2
183  cases (measured_subtrace_preserved cminor_rtlabs_meas_sim … (refl ??) cm_meas)
184  #ra_m1 * #ra_m2 * #ra_meas #ra_obs >ra_obs -cm_m1 -cm_m2
185  #OBS cases (measurable_subtraces_are_structured … WCL ra_meas OBS)
186  #ra_s1 * #ra_s2 * #fn * #ra_tlr * * * #ra_exec_prefix #ra_unrepeating #ra_max #ra_obs'
187  >OBS -ra_meas
188 
189  (* So, we have for RTLabs:
190     ra_exec_prefix - after [ra_m1] steps we get to [ra_s1] with observables [prefix],
191     ra_tlr         - structured trace from [ra_s1] to some [ra_s2],
192     ra_unrepeating - PCs don't repeat locally in [ra_tlr]
193     ra_obs'        - the observables from [ra_tlr] are [subtrace]
194     ra_max         - the stack bound is respected in [prefix@subtrace]
195   *)
196
197
198(* Old, semiformal cut
199cut (∀n,s1,s2,obs1,obs2.
200          exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
201            ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2.
202            tlr_observables … tlr (function_of … s1) = obs2 →
203            (* maybe instead of function_of the called id can rather be obtained from execution? *)
204     ∃m,p,s_fin.
205   observables (OC_preclassified_system (c_labelled_object_code … p))
206    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
207    *)
208     
209             
210             
Note: See TracBrowser for help on using the repository browser.