source: src/correctness.ma @ 3022

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

Make a couple of tests monadic for easier inversion.

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