source: src/correctness.ma @ 3051

Last change on this file since 3051 was 3047, checked in by campbell, 7 years ago

Switch removal and labelling combined.

File size: 7.0 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".
43
44definition clight_clock_after : ∀p:clight_program. nat → (costlabel→ℕ) → res nat ≝
45λp,n,costmap.
46  ! 〈s,itrace〉 ← exec_steps_with_obs Clight_pcs p n;
47  let ctrace ≝ filter_map … (λi. match i with [IEVcost cl ⇒ Some … cl | _ ⇒ None ? ]) itrace in
48  return Σ_{l ∈ ctrace}(costmap l).
49
50include "common/AssocList.ma".
51
52definition lookup_stack_cost : stack_cost_model → ident → option nat ≝
53 λstack_cost,id.
54  assoc_list_lookup ?? id (eq_identifier …) stack_cost.
55
56definition simulates ≝
57  λp: compiler_output.
58  let initial_status ≝ initialise_status … (cm (c_labelled_object_code … p)) in
59  ∀m1,m2.
60   measurable Clight_pcs (c_labelled_clight … p) m1 m2
61    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
62  ∀c1,c2.
63   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = OK … c1 →
64   clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = OK … c2 →
65  ∃n1,n2.
66   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
67   observables (OC_preclassified_system (c_labelled_object_code … p))
68    (c_labelled_object_code … p) n1 n2
69  ∧
70   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
71
72include "common/ExtraMonads.ma".
73
74include "Clight/SwitchAndLabel.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[ whd in EQ_front_end:(??%%); destruct
113  cut (labelled = \fst (clight_label cl_switch_removed))
114  [ cases (clight_label ?) in CL_LABELLED ⊢ %; // ]
115  #E >E
116  @switch_and_labelling_sim @NOT_WRONG
117| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
118
119cut (∀n,s1,s2,obs1,obs2.
120          exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
121            ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2.
122            tlr_observables … tlr (function_of … s1) = obs2 →
123            (* maybe instead of function_of the called id can rather be obtained from execution? *)
124     ∃m,p,s_fin.
125   observables (OC_preclassified_system (c_labelled_object_code … p))
126    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
127   
128     
129             
130             
131 
132(* start of old simulates 
133
134(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
135   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
136   according to the [stack_cost] function. *)
137axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
138axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
139
140
141  let cl_trace ≝ exec_inf … clight_fullexec labelled in
142  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
143  not_wrong ? cl_trace →
144  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
145  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
146
147*)
148
149(* TODO
150
151
152∀input_program.
153! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
154
155exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
156
157
158
159exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
160(* Should we be lifting labels in some way here? *)
161
162
163
164∀i,f : clight_status.
165  Clight_labelled i →
166  Clight_labelled f →
167∀mx,time.
168  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
169  will_return O O mx time f trace →
170  mx < max_allowed_stack →
171∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
172  time = clock f' - clock i'.
173
174
175∀s,flat.
176let ge ≝ (globalenvs … labelled) in
177subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
178RTLabs_cost s = true →
179∀WR : will_return ge 0 s flat.
180let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
181let labels_rtlabs ≝ flat_label_trace … flat WR in
182∃!initial,final,structured_trace_asm.
183  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
184  clock … code_memory … final = clock … code_memory … initial +
185     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
186
187
188
189What is ≃l?  Must show that "labelled" does everything that
190"input_program" does, without getting lost in some
191non-terminating loop part way.
192
193*)
194
Note: See TracBrowser for help on using the repository browser.