source: src/correctness.ma @ 3018

Last change on this file since 3018 was 3003, checked in by sacerdot, 7 years ago

Correctness.ma "repaired"

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