source: src/correctness.ma @ 3041

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

Break up front-end for correctness proof.
Use let rec to prevent labelling function from unfolding.

File size: 6.8 KB
Line 
1
2include "compiler.ma".
3
4include "ASM/Interpret2.ma".
5
6include "Clight/labelSimulation.ma".
7
8include "Clight/Clight_classified_system.ma".
9
10(* From measurable on Clight, we will end up with an RTLabs flat trace where
11   we know that there are some m' and n' such that the prefix in Clight matches
12   the prefix in RTLabs given by m', the next n steps in Clight are equivalent
13   to the n' steps in RTLabs, and we have a suitable "will_return" for RTLabs
14   for those n' steps so that we can build a corresponding structured trace.
15   
16   "Equivalent" here means, in particular, that the observables will be the same,
17   and those observables will include the stack space costs.
18 *)
19
20definition in_execution_prefix : execution_prefix Clight_state → costlabel → Prop ≝
21λx,l. Exists … (λtrs. Exists … (λev. ev = EVcost l) (\fst trs)) x.
22
23let 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 ≝
24match l' return λl'. (∀b. Exists … (λx.x=b) l' → Exists … (λx.x=b) l) → A with
25[ nil ⇒ λ_. a
26| cons h t ⇒ λH. foldl_exists_aux A B l t f (f a h (H …)) ?
27].
28[ %1 %
29| #b #H' @H %2 @H'
30] qed.
31
32definition foldl_exists : ∀A,B:Type[0]. ∀l:list B. (A → ∀b:B. Exists … (λx. x = b ) l → A) → A → A ≝
33λA,B,l,f,a.  foldl_exists_aux A B l l f a (λb,H. H).
34
35lemma Exists_lift : ∀A,P,Q,l.
36  (∀x. P x → Q x) →
37  Exists A P l →
38  Exists A Q l.
39#A #P #Q #l elim l
40[ //
41| #h #t #IH #H * [ #H' %1 @H @H' | #H' %2 @IH /2/ ]
42] qed.
43
44include "RTLabs/MeasurableToStructured.ma".
45
46definition clight_clock_after : ∀p:clight_program. nat → (costlabel→ℕ) → res nat ≝
47λp,n,costmap.
48  ! 〈s,itrace〉 ← exec_steps_with_obs Clight_pcs p n;
49  let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
50  return Σ_{l ∈ ctrace}(costmap l).
51
52include "common/AssocList.ma".
53
54definition lookup_stack_cost : stack_cost_model → ident → option nat ≝
55 λstack_cost,id.
56  assoc_list_lookup ?? id (eq_identifier …) stack_cost.
57
58definition simulates ≝
59  λp: compiler_output.
60  let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in
61  ∀m1,m2.
62   measurable Clight_pcs (c_labelled_clight … p) m1 m2
63    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
64  ∀c1,c2.
65   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
66   clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = OK … c2 →
67  ∃n1,n2.
68   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
69   observables (OC_preclassified_system (c_labelled_object_code … p))
70    (c_labelled_object_code … p) n1 n2
71  ∧
72   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
73
74include "common/ExtraMonads.ma".
75
76theorem correct :
77  ∀observe.
78  ∀input_program,output.
79  compile observe input_program = return output →
80  not_wrong … (exec_inf … clight_fullexec input_program) →
81  sim_with_labels
82   (exec_inf … clight_fullexec input_program)
83   (exec_inf … clight_fullexec (c_labelled_clight … output))
84  ∧
85  simulates output.
86#observe #p_in #out
87#H @('bind_inversion H) -H
88** #init_cost #labelled #p_rtlabs #EQ_front_end
89#H @('bind_inversion H) -H
90** #p_asm #stack_costs #globals_size
91#H @('bind_inversion H) -H
92#p_asm'
93#H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm
94whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
95#H @('bind_inversion H) -H
96#p_loc #EQ_assembler
97whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
98
99whd in EQ_front_end:(??%?);
100letin cl_switch_removed ≝ (program_switch_removal p_in) in EQ_front_end;
101lapply (refl ? (clight_label cl_switch_removed))
102cases (clight_label ?) in ⊢ (???% → %); #cl_labelled #init_cost' #CL_LABELLED
103whd in ⊢ (??%? → ?);
104letin cl_simplified ≝ (simplify_program ?)
105#H @('bind_inversion H) -H #cminor #CMINOR
106#H @('bind_inversion H) -H #WCL #_
107#H @('bind_inversion H) -H #INJ #_
108letin rtlabs ≝ (cminor_to_rtlabs cminor)
109#EQ_front_end
110
111#NOT_WRONG %
112[ cases daemon (* TODO *)
113| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
114
115cut (∀n,s1,s2,obs1,obs2.
116          exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
117            ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2.
118            tlr_observables … tlr (function_of … s1) = obs2 →
119            (* maybe instead of function_of the called id can rather be obtained from execution? *)
120     ∃m,p,s_fin.
121   observables (OC_preclassified_system (c_labelled_object_code … p))
122    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
123   
124     
125             
126             
127 
128(* start of old simulates 
129
130(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
131   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
132   according to the [stack_cost] function. *)
133axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
134axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
135
136
137  let cl_trace ≝ exec_inf … clight_fullexec labelled in
138  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
139  not_wrong ? cl_trace →
140  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
141  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
142
143*)
144
145(* TODO
146
147
148∀input_program.
149! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
150
151exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
152
153
154
155exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
156(* Should we be lifting labels in some way here? *)
157
158
159
160∀i,f : clight_status.
161  Clight_labelled i →
162  Clight_labelled f →
163∀mx,time.
164  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
165  will_return O O mx time f trace →
166  mx < max_allowed_stack →
167∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
168  time = clock f' - clock i'.
169
170
171∀s,flat.
172let ge ≝ (globalenvs … labelled) in
173subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
174RTLabs_cost s = true →
175∀WR : will_return ge 0 s flat.
176let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
177let labels_rtlabs ≝ flat_label_trace … flat WR in
178∃!initial,final,structured_trace_asm.
179  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
180  clock … code_memory … final = clock … code_memory … initial +
181     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
182
183
184
185What is ≃l?  Must show that "labelled" does everything that
186"input_program" does, without getting lost in some
187non-terminating loop part way.
188
189*)
190
Note: See TracBrowser for help on using the repository browser.