source: src/correctness.ma @ 2938

Last change on this file since 2938 was 2928, checked in by tranquil, 8 years ago

some sketches about correctness proof

File size: 7.6 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
74definition measure_clock : ∀x:execution_prefix Clight_state. ((Σl:costlabel.in_execution_prefix x l)→ℕ) → nat ≝
75λx,costmap. foldl_exists … x
76 (λclock,trs,H.
77    foldl_exists … (\fst trs) (λclock,ev. match ev return λev. Exists … (λx. x=ev) ? → nat with [ EVcost l ⇒ λH'. clock + costmap «l,?» | _ ⇒ λ_. clock ]) clock)
78 0.
79whd @(Exists_lift … H) * #tr1 #s1 #E destruct @(Exists_lift … H') #ev1 #E @E
80qed.
81
82definition clight_clock_after : ∀p:clight_program. nat → ((Σl:costlabel.in_clight_program p l)→ℕ) → option nat ≝
83λp,n,costmap.
84  let x ≝ exec_inf … clight_fullexec p in
85  match split_trace … x n with
86  [ Some traces ⇒
87    Some ? (measure_clock (\fst traces) (λl.costmap «l,?»))
88  | None ⇒ None ?
89  ].
90cases daemon
91qed.
92
93include "common/AssocList.ma".
94
95definition lookup_stack_cost : stack_cost_model → ident → nat ≝
96 λstack_cost,id.
97  match assoc_list_lookup ?? id (eq_identifier …) stack_cost with
98  [ None ⇒ 0 | Some n ⇒ n ].
99
100definition simulates ≝
101  λp: compiler_output.
102  let initial_status ≝ initialise_status … (load_code_memory (oc (c_labelled_object_code … p))) in
103  ∀m1,m2.
104   measurable Clight_pcs (c_labelled_clight … p) m1 m2
105    (lookup_stack_cost (c_stack_cost … p)) (c_max_stack … p) →
106  ∀c1,c2.
107   clight_clock_after (c_labelled_clight … p) m1 (c_clight_cost_map … p) = Some ? c1 →
108   clight_clock_after (c_labelled_clight … p) m2 (c_clight_cost_map … p) = Some ? c2 →
109  ∃n1,n2.
110   observables Clight_pcs (c_labelled_clight … p) m1 m2 =
111   observables (OC_preclassified_system (c_labelled_object_code … p))
112    (c_labelled_object_code … p) n1 n2
113  ∧
114   minus c2 c1 = clock … (execute n2 ? initial_status) - clock … (execute n1 ? initial_status).
115
116include "common/ExtraMonads.ma".
117
118theorem correct' :
119  ∀observe.
120  ∀input_program,output.
121  compile observe input_program = return output →
122  not_wrong … (exec_inf … clight_fullexec input_program) →
123  sim_with_labels
124   (exec_inf … clight_fullexec input_program)
125   (exec_inf … clight_fullexec (c_labelled_clight … output))
126  ∧
127  simulates output.
128#observe #p_in #out
129#H @('bind_inversion H) -H
130** #init_cost #labelled #p_rtlabs #EQ_front_end
131#H @('bind_inversion H) -H
132** #p_asm #stack_costs #globals_size
133#H @('bind_inversion H) -H
134#p_asm'
135#H lapply (opt_eq_from_res ???? H) #EQ_lin_to_asm
136whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
137#H @('bind_inversion H) -H
138#p_loc #EQ_assembler
139whd in ⊢ (??%%→?); #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ)
140#NOT_WRONG %
141[ cases daemon (* TODO *)
142| #m1 #m2 #m1_m2_meas #c1 #c2 #c1_prf #c2_prf
143
144cut (∀n,s1,s2,obs1,obs2.
145          exec_with_observables_n n (RTLabs_init_state p_rtlabs) = return 〈obs1, s1〉 →
146            ∀tlr : trace_label_return (RTLabs_status p_rtlabs) s1 s2.
147            tlr_observables … tlr (function_of … s1) = obs2 →
148            (* maybe instead of function_of the called id can rather be obtained from execution? *)
149     ∃m,p,s_fin.
150   observables (OC_preclassified_system (c_labelled_object_code … p))
151    (c_labelled_object_code … p) m p = return 〈obs1, obs2〉)
152   
153     
154             
155             
156 
157(* start of old simulates 
158
159(* [nth_state_of_with_stack state stack_cost stack_bound exec n] returns [Some s] iff after
160   [n] steps of [exec] we have reached [s] without exceeding the [stack_bound]
161   according to the [stack_cost] function. *)
162axiom nth_state_of_with_stack : ∀state. (state → nat) → nat → execution state io_out io_in → nat → option state.
163axiom nth_state_of : ∀state. execution state io_out io_in → nat → option state.
164
165
166  let cl_trace ≝ exec_inf … clight_fullexec labelled in
167  let asm_trace ≝ exec_inf … ASM_fullexec object_code in
168  not_wrong ? cl_trace →
169  ∀n,s. nth_state_of_with_stack ? stack_cost stack_bound cl_trace n = Some ? s →
170  𝚺m,s'. nth_state_of ? asm_trace m = Some ? s' ∧ s ≃ s'
171
172*)
173
174(* TODO
175
176
177∀input_program.
178! 〈object_code,costlabel_map,labelled,cost_map〉 ← compile input_program
179
180exec_inf … clight_fullexec input_program ≃l exec_inf … clight_fullexec labelled
181
182
183
184exec_inf … clight_fullexec labelled ≈ exec_inf … ASM_fullexec object_code
185(* Should we be lifting labels in some way here? *)
186
187
188
189∀i,f : clight_status.
190  Clight_labelled i →
191  Clight_labelled f →
192∀mx,time.
193  let trace ≝ exec_inf_aux … clight_fullexec labelled i in
194  will_return O O mx time f trace →
195  mx < max_allowed_stack →
196∃!i',f'. i ≃ i' ∧ f ≃ f' ∧ i' 8051~> f' ∧
197  time = clock f' - clock i'.
198
199
200∀s,flat.
201let ge ≝ (globalenvs … labelled) in
202subtrace_of (exec_inf … RTLabs_fullexec labelled) flat →
203RTLabs_cost s = true →
204∀WR : will_return ge 0 s flat.
205let structured_trace_rtlabs ≝ make_label_return' ge 0 s flat ??? WR in
206let labels_rtlabs ≝ flat_label_trace … flat WR in
207∃!initial,final,structured_trace_asm.
208  structured_trace_rtlabs ≈ structured_trace_asm ∧ 
209  clock … code_memory … final = clock … code_memory … initial +
210     (Σ_{i < |labels_rtlabs|} (cost_map (match nth i labels_rtlabs with [ Some k ⇒ k | None ⇒ 0 ])).
211
212
213
214What is ≃l?  Must show that "labelled" does everything that
215"input_program" does, without getting lost in some
216non-terminating loop part way.
217
218*)
219
Note: See TracBrowser for help on using the repository browser.