1 | (**************************************************************************) |
---|
2 | (* ___ *) |
---|
3 | (* ||M|| *) |
---|
4 | (* ||A|| A project by Andrea Asperti *) |
---|
5 | (* ||T|| *) |
---|
6 | (* ||I|| Developers: *) |
---|
7 | (* ||T|| The HELM team. *) |
---|
8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
9 | (* \ / *) |
---|
10 | (* \ / This file is distributed under the terms of the *) |
---|
11 | (* v GNU General Public License Version 2 *) |
---|
12 | (* *) |
---|
13 | (**************************************************************************) |
---|
14 | |
---|
15 | include "joint/linearise.ma". |
---|
16 | include "common/StatusSimulation.ma". |
---|
17 | include "joint/Traces.ma". |
---|
18 | include "joint/semanticsUtils.ma". |
---|
19 | |
---|
20 | definition graph_prog_params ≝ |
---|
21 | λp,p',prog,stack_sizes. |
---|
22 | mk_prog_params (make_sem_graph_params p p') prog stack_sizes. |
---|
23 | |
---|
24 | definition graph_abstract_status: |
---|
25 | ∀p:unserialized_params. |
---|
26 | (∀F.sem_unserialized_params p F) → |
---|
27 | ∀prog : joint_program (mk_graph_params p). |
---|
28 | ((Σi.is_internal_function_of_program … prog i) → ℕ) → |
---|
29 | abstract_status |
---|
30 | ≝ |
---|
31 | λp,p',prog,stack_sizes. |
---|
32 | joint_abstract_status (graph_prog_params ? p' prog stack_sizes). |
---|
33 | |
---|
34 | definition lin_prog_params ≝ |
---|
35 | λp,p',prog,stack_sizes. |
---|
36 | mk_prog_params (make_sem_lin_params p p') prog stack_sizes. |
---|
37 | |
---|
38 | definition lin_abstract_status: |
---|
39 | ∀p:unserialized_params. |
---|
40 | (∀F.sem_unserialized_params p F) → |
---|
41 | ∀prog : joint_program (mk_lin_params p). |
---|
42 | ((Σi.is_internal_function_of_program … prog i) → ℕ) → |
---|
43 | abstract_status |
---|
44 | ≝ |
---|
45 | λp,p',prog,stack_sizes. |
---|
46 | joint_abstract_status (lin_prog_params ? p' prog stack_sizes). |
---|
47 | |
---|
48 | (* |
---|
49 | axiom P : |
---|
50 | ∀A,B,prog.A (prog_var_names (λvars.fundef (A vars)) B prog) → Prop. |
---|
51 | |
---|
52 | check (λpars.let pars' ≝ make_global pars in λx :joint_closed_internal_function pars' (globals pars'). P … x) |
---|
53 | (* |
---|
54 | unification hint 0 ≔ p, prog, stack_sizes ; |
---|
55 | pars ≟ mk_prog_params p prog stack_sizes , |
---|
56 | pars' ≟ make_global pars, |
---|
57 | A ≟ λvars.joint_closed_internal_function p vars, |
---|
58 | B ≟ ℕ |
---|
59 | ⊢ |
---|
60 | A (prog_var_names (λvars.fundef (A vars)) B prog) ≡ |
---|
61 | joint_closed_internal_function pars' (globals pars'). |
---|
62 | *) |
---|
63 | axiom T : ∀A,B,prog.genv_t (fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog))) → Prop. |
---|
64 | (*axiom Q : ∀A,B,init,prog. |
---|
65 | T … (globalenv (λvars:list ident.fundef (A vars)) B |
---|
66 | init prog) → Prop. |
---|
67 | |
---|
68 | lemma pippo : |
---|
69 | ∀p,p',prog,stack_sizes. |
---|
70 | let pars ≝ graph_prog_params p p' prog stack_sizes in |
---|
71 | let ge ≝ ev_genv pars in T ?? prog ge → Prop. |
---|
72 | |
---|
73 | #H1 #H2 #H3 #H4 |
---|
74 | #H5 |
---|
75 | whd in match (ev_genv ?) in H5; |
---|
76 | whd in match (globalenv_noinit) in H5; normalize nodelta in H5; |
---|
77 | whd in match (prog ?) in H5; |
---|
78 | whd in match (joint_function ?) in H5; |
---|
79 | @(Q … H5) |
---|
80 | λx:T ??? ge.Q ???? x) |
---|
81 | *) |
---|
82 | axiom Q : ∀A,B,init,prog,i. |
---|
83 | is_internal_function |
---|
84 | (A |
---|
85 | (prog_var_names (λvars:list ident.fundef (A vars)) B |
---|
86 | prog)) |
---|
87 | (globalenv (λvars:list ident.fundef (A vars)) B |
---|
88 | init prog) |
---|
89 | i → Prop. |
---|
90 | |
---|
91 | check |
---|
92 | (λp,p',prog,stack_sizes,i. |
---|
93 | let pars ≝ graph_prog_params p p' prog stack_sizes in |
---|
94 | let ge ≝ ev_genv pars in |
---|
95 | λx:is_internal_function (joint_closed_internal_function pars (globals pars)) |
---|
96 | ge i.Q ??? prog ? x) |
---|
97 | *) |
---|
98 | |
---|
99 | definition sigma_pc_opt: |
---|
100 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
101 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
102 | code_point (mk_graph_params p) → option ℕ) → |
---|
103 | program_counter → option program_counter |
---|
104 | ≝ |
---|
105 | λp,p',prog,sigma,pc. |
---|
106 | let pars ≝ make_sem_graph_params p p' in |
---|
107 | let ge ≝ globalenv_noinit … prog in |
---|
108 | ! f ← int_funct_of_block ? ge (pc_block pc) ; |
---|
109 | ! lin_point ← sigma f (point_of_pc ? pars pc) ; |
---|
110 | return pc_of_point ? (make_sem_lin_params ? p') pc lin_point. |
---|
111 | |
---|
112 | definition well_formed_pc: |
---|
113 | ∀p,p',graph_prog. |
---|
114 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
115 | label → option ℕ) → |
---|
116 | program_counter → Prop |
---|
117 | ≝ |
---|
118 | λp,p',prog,sigma,pc. |
---|
119 | sigma_pc_opt p p' prog sigma pc |
---|
120 | ≠ None …. |
---|
121 | |
---|
122 | definition well_formed_status: |
---|
123 | ∀p,p',graph_prog. |
---|
124 | ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
125 | label → option ℕ) → |
---|
126 | state_pc (make_sem_graph_params p p') → Prop ≝ |
---|
127 | λp,p',prog,sigma,st. |
---|
128 | well_formed_pc p p' prog sigma (pc … st) ∧ ?. |
---|
129 | cases daemon (* TODO *) |
---|
130 | qed. |
---|
131 | |
---|
132 | (* |
---|
133 | lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?. |
---|
134 | [ #p #s #st #prf |
---|
135 | whd in match sigma_pc_of_status; normalize nodelta |
---|
136 | @opt_safe_elim |
---|
137 | #n |
---|
138 | lapply (refl … (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
139 | (ev_genv p) (pblock (pc p st)))) |
---|
140 | elim (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
141 | (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%); |
---|
142 | [ #_ #ABS normalize in ABS; destruct(ABS) ] |
---|
143 | #f #EQ >m_return_bind |
---|
144 | *) |
---|
145 | |
---|
146 | |
---|
147 | (* |
---|
148 | lemma wf_status_to_wf_pc : |
---|
149 | ∀p,p',graph_prog,stack_sizes. |
---|
150 | ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
151 | code_point (mk_graph_params p) → option ℕ). |
---|
152 | ∀st. |
---|
153 | well_formed_status p p' graph_prog stack_sizes sigma st → |
---|
154 | well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st). |
---|
155 | #p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H |
---|
156 | qed. |
---|
157 | *) |
---|
158 | definition sigma_pc : |
---|
159 | ∀p,p',graph_prog. |
---|
160 | ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
161 | label → option ℕ). |
---|
162 | ∀pc. |
---|
163 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
164 | program_counter ≝ |
---|
165 | λp,p',graph_prog,sigma,st.opt_safe …. |
---|
166 | |
---|
167 | lemma sigma_pc_of_status_ok: |
---|
168 | ∀p,p',graph_prog. |
---|
169 | ∀sigma. |
---|
170 | ∀pc. |
---|
171 | ∀prf:well_formed_pc p p' graph_prog sigma pc. |
---|
172 | sigma_pc_opt p p' graph_prog sigma pc = |
---|
173 | Some … (sigma_pc p p' graph_prog sigma pc prf). |
---|
174 | #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed. |
---|
175 | |
---|
176 | definition sigma_state : |
---|
177 | ∀p. |
---|
178 | ∀p':∀F.sem_unserialized_params p F. |
---|
179 | ∀graph_prog. |
---|
180 | ∀sigma. |
---|
181 | (* let lin_prog ≝ linearise ? graph_prog in *) |
---|
182 | ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) |
---|
183 | well_formed_status p p' graph_prog sigma s → |
---|
184 | state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) |
---|
185 | ≝ |
---|
186 | λp,p',graph_prog,sigma,s,prf. |
---|
187 | let pc' ≝ sigma_pc … (proj1 … prf) in |
---|
188 | mk_state_pc ? ? pc'. |
---|
189 | cases daemon (* TODO *) qed. |
---|
190 | |
---|
191 | lemma sigma_pc_commute: |
---|
192 | ∀p,p',graph_prog,sigma,st. |
---|
193 | ∀prf : well_formed_status p p' graph_prog sigma st. |
---|
194 | sigma_pc … (pc ? st) (proj1 … prf) = |
---|
195 | pc ? (sigma_state … st prf). |
---|
196 | #p #p' #prog #sigma #st #prf % |
---|
197 | qed. |
---|
198 | |
---|
199 | lemma res_eq_from_opt : |
---|
200 | ∀A,m,v.res_to_opt A m = return v → m = return v. |
---|
201 | #A * #x #v normalize #EQ destruct % qed. |
---|
202 | |
---|
203 | definition sigma_function_name : |
---|
204 | ∀p,graph_prog. |
---|
205 | let lin_prog ≝ linearise p graph_prog in |
---|
206 | (Σf.is_internal_function_of_program … graph_prog f) → |
---|
207 | (Σf.is_internal_function_of_program … lin_prog f) ≝ |
---|
208 | λp,graph_prog,f.«f, if_propagate … (pi2 … f)». |
---|
209 | |
---|
210 | lemma if_of_function_commute: |
---|
211 | ∀p. |
---|
212 | ∀graph_prog : joint_program (mk_graph_params p). |
---|
213 | ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i. |
---|
214 | let graph_fd ≝ if_of_function … graph_fun in |
---|
215 | let lin_fun ≝ sigma_function_name … graph_fun in |
---|
216 | let lin_fd ≝ if_of_function … lin_fun in |
---|
217 | lin_fd = \fst (linearise_int_fun ?? graph_fd). |
---|
218 | #p #graph_prog #graph_fun whd |
---|
219 | @prog_if_of_function_transform % qed. |
---|
220 | |
---|
221 | lemma bind_opt_inversion: |
---|
222 | ∀A,B: Type[0]. ∀f: option A. ∀g: A → option B. ∀y: B. |
---|
223 | (! x ← f ; g x = Some … y) → |
---|
224 | ∃x. (f = Some … x) ∧ (g x = Some … y). |
---|
225 | #A #B #f #g #y cases f normalize |
---|
226 | [ #H destruct (H) |
---|
227 | | #a #e %{a} /2 by conj/ |
---|
228 | ] qed. |
---|
229 | |
---|
230 | lemma sigma_pblock_eq_lemma : |
---|
231 | ∀p,p',graph_prog. |
---|
232 | let lin_prog ≝ linearise p graph_prog in |
---|
233 | ∀sigma,pc. |
---|
234 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
235 | pc_block (sigma_pc ? p' graph_prog sigma pc prf) = |
---|
236 | pc_block pc. |
---|
237 | #p #p' #graph_prog #sigma #pc #prf |
---|
238 | whd in match sigma_pc; normalize nodelta |
---|
239 | @opt_safe_elim #x #x_spec |
---|
240 | whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec; |
---|
241 | normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H |
---|
242 | #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct // |
---|
243 | qed. |
---|
244 | |
---|
245 | (* |
---|
246 | lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B. |
---|
247 | (! x ← m ; g x) ≠ None ? → m ≠ None ?. |
---|
248 | #A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize |
---|
249 | [ #abs elim abs -abs #abs @abs % |
---|
250 | | #abs elim abs -abs #abs #v @abs % |
---|
251 | ] |
---|
252 | qed. |
---|
253 | |
---|
254 | lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A. |
---|
255 | ∀ b : B .∀ f : A → B. ∀g : B → option C. |
---|
256 | g (match m with [None ⇒ b | Some x ⇒ f x])≠ None ? → g b = None ? → m ≠ None ?. |
---|
257 | #A #B #C #m #x #b #f #g #H1 #H2 % #m_eq_none >m_eq_none in H1; normalize #H elim H -H #H @H assumption |
---|
258 | qed. |
---|
259 | *) |
---|
260 | |
---|
261 | lemma funct_of_block_transf : |
---|
262 | ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. |
---|
263 | ∀transf : ∀vars. A vars → B vars. ∀bl,f,prf. |
---|
264 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
265 | funct_of_block … (globalenv_noinit … progr) bl = return f → |
---|
266 | funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf». |
---|
267 | #A #B #progr #transf #bl #f #prf whd |
---|
268 | whd in match funct_of_block in ⊢ (%→?); normalize nodelta |
---|
269 | cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. |
---|
270 | ∀o.∀prf : Q o. |
---|
271 | ∀f1,f2. |
---|
272 | (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) → |
---|
273 | P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) |
---|
274 | [ #A #B #Q #P * /2/ ] #aux |
---|
275 | @aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ] |
---|
276 | #fd #EQfind whd in ⊢ (??%%→?); |
---|
277 | generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ) |
---|
278 | whd in match funct_of_block; normalize nodelta |
---|
279 | @aux [ # fd' ] |
---|
280 | [2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ] |
---|
281 | #prf' cases daemon qed. |
---|
282 | |
---|
283 | lemma description_of_function_transf : |
---|
284 | ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. |
---|
285 | ∀transf : ∀vars. A vars → B vars. |
---|
286 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
287 | ∀f_out,prf. |
---|
288 | description_of_function … |
---|
289 | (globalenv_noinit … progr') f_out = |
---|
290 | transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr) |
---|
291 | «pi1 … f_out, prf»). |
---|
292 | #A #B #progr #transf #f_out #prf |
---|
293 | whd in match description_of_function in ⊢ (???%); |
---|
294 | normalize nodelta |
---|
295 | cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. |
---|
296 | ∀o.∀prf : Q o. |
---|
297 | ∀f1,f2. |
---|
298 | (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) → |
---|
299 | P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) |
---|
300 | [ #A #B #Q #P * /2/ ] #aux |
---|
301 | @aux |
---|
302 | [ #fd' ] * #fd #EQ destruct (EQ) |
---|
303 | inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] |
---|
304 | #bl #EQfind >m_return_bind #EQfindf |
---|
305 | whd in match description_of_function; normalize nodelta |
---|
306 | @aux |
---|
307 | [ #fdo' ] * #fdo #EQ destruct (EQ) |
---|
308 | >find_symbol_transf >EQfind >m_return_bind |
---|
309 | >(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) % |
---|
310 | qed. |
---|
311 | |
---|
312 | |
---|
313 | lemma match_int_fun : |
---|
314 | ∀A,B : Type[0].∀P : B → Prop. |
---|
315 | ∀Q : fundef A → Prop. |
---|
316 | ∀m : fundef A. |
---|
317 | ∀f1 : ∀fd.Q (Internal \ldots fd) → B. |
---|
318 | ∀f2 : ∀fd.Q (External … fd) → B. |
---|
319 | ∀prf : Q m. |
---|
320 | (∀fd,prf.P (f1 fd prf)) → |
---|
321 | (∀fd,prf.P (f2 fd prf)) → |
---|
322 | P (match m |
---|
323 | return λx.Q x → ? |
---|
324 | with |
---|
325 | [ Internal fd ⇒ f1 fd |
---|
326 | | External fd ⇒ f2 fd |
---|
327 | ] prf). |
---|
328 | #A #B #P #Q * // qed. |
---|
329 | (*) |
---|
330 | lemma match_int_fun : |
---|
331 | ∀A,B : Type[0].∀P : B → Prop. |
---|
332 | ∀m : fundef A. |
---|
333 | ∀f1 : ∀fd.m = Internal … fd → B. |
---|
334 | ∀f2 : ∀fd.m = External … fd → B. |
---|
335 | (∀fd,prf.P (f1 fd prf)) → |
---|
336 | (∀fd,prf.P (f2 fd prf)) → |
---|
337 | P (match m |
---|
338 | return λx.m = x → ? |
---|
339 | with |
---|
340 | [ Internal fd ⇒ f1 fd |
---|
341 | | External fd ⇒ f2 fd |
---|
342 | ] (refl …)). |
---|
343 | #A #B #P * // qed. |
---|
344 | *) |
---|
345 | (* |
---|
346 | lemma prova : |
---|
347 | ∀ A.∀progr : program (λvars. fundef (A vars)) ℕ. |
---|
348 | ∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)). |
---|
349 | ∀ f,g,prf1. |
---|
350 | match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with |
---|
351 | [Internal fn ⇒ λ prf.return «g,prf1 fn prf» | |
---|
352 | External fn ⇒ λprf.None ? ] (refl ? M) = return f → |
---|
353 | ∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf». |
---|
354 | #H1 #H2 #H3 #H4 #H5 #H6 |
---|
355 | @match_int_fun |
---|
356 | #fd #EQ #EQ' whd in EQ' : (??%%); destruct |
---|
357 | %[|%[| % ]] qed. |
---|
358 | *) |
---|
359 | |
---|
360 | lemma int_funct_of_block_transf_commute: |
---|
361 | ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ. |
---|
362 | ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf. |
---|
363 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
364 | int_funct_of_block ? (globalenv_noinit … progr) bl = return f → |
---|
365 | int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf». |
---|
366 | #A #B #progr #transf #bl #f #prf |
---|
367 | whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta |
---|
368 | #H |
---|
369 | elim (bind_opt_inversion ??? ?? H) -H #x |
---|
370 | * #x_spec |
---|
371 | @match_int_fun [2: #fd #_ #ABS destruct(ABS) ] |
---|
372 | #fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ) |
---|
373 | whd in match int_funct_of_block; normalize nodelta |
---|
374 | >(funct_of_block_transf … (internal_function_is_function … prf) … x_spec) |
---|
375 | >m_return_bind |
---|
376 | @match_int_fun #fd' #prf' [ % ] |
---|
377 | @⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr |
---|
378 | >(description_of_function_transf) [2: @x_prf ] |
---|
379 | >EQdescr whd in ⊢ (??%%→?); #ABS destruct qed. |
---|
380 | |
---|
381 | |
---|
382 | lemma fetch_function_sigma_commute : |
---|
383 | ∀p,p',graph_prog. |
---|
384 | let lin_prog ≝ linearise p graph_prog in |
---|
385 | ∀sigma,pc_st,f. |
---|
386 | ∀prf : well_formed_pc p p' graph_prog sigma pc_st. |
---|
387 | fetch_function … (globalenv_noinit … graph_prog) pc_st = |
---|
388 | return f |
---|
389 | → fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) = |
---|
390 | return sigma_function_name … f. |
---|
391 | #p #p' #graph_prog #sigma #st #f #prf |
---|
392 | whd in match fetch_function; normalize nodelta |
---|
393 | >(sigma_pblock_eq_lemma … prf) #H |
---|
394 | lapply (opt_eq_from_res ???? H) -H #H |
---|
395 | >(int_funct_of_block_transf_commute ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H) |
---|
396 | // |
---|
397 | qed. |
---|
398 | |
---|
399 | (* |
---|
400 | #H elim (bind_opt_inversion ????? H) -H |
---|
401 | #x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta |
---|
402 | @match_opt_prf_elim |
---|
403 | #H #H1 whd in H : (??%?); |
---|
404 | cases ( find_funct_ptr |
---|
405 | (fundef |
---|
406 | (joint_closed_internal_function |
---|
407 | (graph_prog_params p p' graph_prog |
---|
408 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
409 | (linearise_int_fun p) graph_prog stack_sizes)) |
---|
410 | (globals |
---|
411 | (graph_prog_params p p' graph_prog |
---|
412 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
413 | (linearise_int_fun p) graph_prog stack_sizes))))) |
---|
414 | (ev_genv |
---|
415 | (graph_prog_params p p' graph_prog |
---|
416 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
417 | (linearise_int_fun p) graph_prog stack_sizes))) |
---|
418 | (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct |
---|
419 | |
---|
420 | |
---|
421 | normalize nodelta |
---|
422 | #H #H1 |
---|
423 | cases ( find_funct_ptr |
---|
424 | (fundef |
---|
425 | (joint_closed_internal_function |
---|
426 | (graph_prog_params p p' graph_prog |
---|
427 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
428 | (linearise_int_fun p) graph_prog stack_sizes)) |
---|
429 | (globals |
---|
430 | (graph_prog_params p p' graph_prog |
---|
431 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
432 | (linearise_int_fun p) graph_prog stack_sizes))))) |
---|
433 | (ev_genv |
---|
434 | (graph_prog_params p p' graph_prog |
---|
435 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
436 | (linearise_int_fun p) graph_prog stack_sizes))) |
---|
437 | (pblock (pc (make_sem_graph_params p p') st))) in H; |
---|
438 | |
---|
439 | |
---|
440 | check find_funct_ptr_transf |
---|
441 | whd in match int_funct_of_block; normalize nodelta |
---|
442 | #H elim (bind_inversion ????? H) |
---|
443 | |
---|
444 | .. sigma_int_funct_of_block |
---|
445 | |
---|
446 | |
---|
447 | |
---|
448 | whd in match int_funct_of_block; normalize nodelta |
---|
449 | elim (bind_inversion ????? H) |
---|
450 | whd in match int_funct_of_block; normalize nodelta |
---|
451 | #H elim (bind_inversion ????? H) -H #fn * |
---|
452 | #H lapply (opt_eq_from_res ???? H) -H |
---|
453 | #H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H) |
---|
454 | -H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%); |
---|
455 | destruct // |
---|
456 | cases daemon |
---|
457 | qed. *) |
---|
458 | |
---|
459 | lemma stmt_at_sigma_commute: |
---|
460 | ∀p,graph_prog,graph_fun,lbl,pt. |
---|
461 | let lin_prog ≝ linearise ? graph_prog in |
---|
462 | let lin_fun ≝ sigma_function_name p graph_prog graph_fun in |
---|
463 | ∀sigma.good_sigma p graph_prog sigma → |
---|
464 | sigma graph_fun lbl = return pt → |
---|
465 | ∀stmt. |
---|
466 | stmt_at … |
---|
467 | (joint_if_code ?? (if_of_function ?? graph_fun)) |
---|
468 | lbl = return stmt → |
---|
469 | stmt_at ?? |
---|
470 | (joint_if_code ?? (if_of_function ?? lin_fun)) |
---|
471 | pt = return (graph_to_lin_statement … stmt). |
---|
472 | #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf |
---|
473 | (* |
---|
474 | whd in match (stmt_at ????); |
---|
475 | whd in match (stmt_at ????); |
---|
476 | cases (linearise_code_spec … p' graph_prog graph_fun |
---|
477 | (joint_if_entry … graph_fun)) |
---|
478 | * #lin_code_closed #sigma_entry_is_zero #sigma_spec |
---|
479 | lapply (sigma_spec |
---|
480 | (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) |
---|
481 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ] |
---|
482 | -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok |
---|
483 | whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; |
---|
484 | inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] |
---|
485 | * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ |
---|
486 | #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm |
---|
487 | <sigma_pc_commute >lin_lookup_ok // *) |
---|
488 | cases daemon |
---|
489 | qed. |
---|
490 | |
---|
491 | lemma fetch_statement_sigma_commute: |
---|
492 | ∀p,p',graph_prog,pc,fn,stmt. |
---|
493 | let lin_prog ≝ linearise ? graph_prog in |
---|
494 | ∀sigma.good_sigma p graph_prog sigma → |
---|
495 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
496 | fetch_statement ? (make_sem_graph_params p p') … |
---|
497 | (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 → |
---|
498 | fetch_statement ? (make_sem_lin_params p p') … |
---|
499 | (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = |
---|
500 | return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉. |
---|
501 | #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf |
---|
502 | whd in match fetch_statement; normalize nodelta #H |
---|
503 | cases (bind_inversion ????? H) #id * -H #fetchfn |
---|
504 | >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind |
---|
505 | #H cases (bind_inversion ????? H) #fstmt * -H #H |
---|
506 | lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct |
---|
507 | >(stmt_at_sigma_commute … good … H) [%] |
---|
508 | whd in match sigma_pc; normalize nodelta |
---|
509 | @opt_safe_elim #pc' #H |
---|
510 | cases (bind_opt_inversion ????? H) |
---|
511 | #i * #EQ1 -H #H |
---|
512 | cases (bind_opt_inversion ????? H) |
---|
513 | #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct |
---|
514 | whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point |
---|
515 | lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2 |
---|
516 | qed. |
---|
517 | |
---|
518 | definition linearise_status_rel: |
---|
519 | ∀p,p',graph_prog. |
---|
520 | let lin_prog ≝ linearise p graph_prog in |
---|
521 | ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
522 | let stack_sizes' ≝ |
---|
523 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
524 | ? graph_prog stack_sizes in |
---|
525 | ∀sigma. |
---|
526 | good_sigma p graph_prog sigma → |
---|
527 | status_rel |
---|
528 | (graph_abstract_status p p' graph_prog stack_sizes') |
---|
529 | (lin_abstract_status p p' lin_prog stack_sizes) |
---|
530 | ≝ λp,p',graph_prog,stack_sizes,sigma,good. |
---|
531 | mk_status_rel … |
---|
532 | (* sem_rel ≝ *) (λs1,s2. |
---|
533 | ∃prf: well_formed_status p p' graph_prog sigma s1. |
---|
534 | s2 = sigma_state … s1 prf) |
---|
535 | (* call_rel ≝ *) (λs1,s2. |
---|
536 | ∃prf:well_formed_status p p' graph_prog sigma s1. |
---|
537 | pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf)) |
---|
538 | (* sim_final ≝ *) ?. |
---|
539 | #st1 #st2 * #prf #EQ2 |
---|
540 | % |
---|
541 | whd in ⊢ (%→%); |
---|
542 | #H lapply (opt_to_opt_safe … H) |
---|
543 | @opt_safe_elim -H |
---|
544 | #res #_ |
---|
545 | #H lapply (res_eq_from_opt ??? H) -H |
---|
546 | #H elim (bind_inversion ????? H) |
---|
547 | * #f #stmt * |
---|
548 | whd in ⊢ (??%?→?); |
---|
549 | cases daemon |
---|
550 | qed. |
---|
551 | |
---|
552 | (* To be added to common/Globalenvs, it strenghtens |
---|
553 | find_funct_ptr_transf *) |
---|
554 | (* |
---|
555 | lemma |
---|
556 | find_funct_ptr_transf_eq: |
---|
557 | ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs). |
---|
558 | ∀b: block. |
---|
559 | find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b = |
---|
560 | m_map ??? |
---|
561 | (transf …) |
---|
562 | (find_funct_ptr ? (globalenv … iV p) b). |
---|
563 | #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%); |
---|
564 | [ cases daemon (* TODO in Globalenvs.ma *) |
---|
565 | | #f #H >(find_funct_ptr_transf A B … H) // ] |
---|
566 | qed. |
---|
567 | *) |
---|
568 | |
---|
569 | |
---|
570 | (*lemma fetch_function_sigma_commute: |
---|
571 | ∀p,p',graph_prog,sigma,st1. |
---|
572 | ∀prf:well_formed_status ??? sigma st1. |
---|
573 | let lin_prog ≝ linearise ? graph_prog in |
---|
574 | fetch_function |
---|
575 | (lin_prog_params p p' lin_prog) |
---|
576 | (globals (lin_prog_params p p' lin_prog)) |
---|
577 | (ev_genv (lin_prog_params p p' lin_prog)) |
---|
578 | (pc (lin_prog_params p p' lin_prog) |
---|
579 | (linearise_status_fun p p' graph_prog sigma st1 prf)) |
---|
580 | = |
---|
581 | m_map … |
---|
582 | (linearise_int_fun ??) |
---|
583 | (fetch_function |
---|
584 | (graph_prog_params p p' graph_prog) |
---|
585 | (globals (graph_prog_params p p' graph_prog)) |
---|
586 | (ev_genv (graph_prog_params p p' graph_prog)) |
---|
587 | (pc (graph_prog_params p p' graph_prog) st1)). |
---|
588 | #p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta |
---|
589 | whd in match function_of_block; normalize nodelta |
---|
590 | >(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …) |
---|
591 | cases (find_funct_ptr ???) // * // |
---|
592 | qed. |
---|
593 | *) |
---|
594 | |
---|
595 | lemma IO_bind_inversion: |
---|
596 | ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. |
---|
597 | (! x ← f ; g x = return y) → |
---|
598 | ∃x. (f = return x) ∧ (g x = return y). |
---|
599 | #O #I #A #B #f #g #y cases f normalize |
---|
600 | [ #o #f #H destruct |
---|
601 | | #a #e %{a} /2 by conj/ |
---|
602 | | #m #H destruct (H) |
---|
603 | ] qed. |
---|
604 | |
---|
605 | lemma opt_Exists_elim: |
---|
606 | ∀A:Type[0].∀P:A → Prop. |
---|
607 | ∀o:option A. |
---|
608 | opt_Exists A P o → |
---|
609 | ∃v:A. o = Some … v ∧ P v. |
---|
610 | #A #P * normalize /3/ * |
---|
611 | qed. |
---|
612 | |
---|
613 | inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ |
---|
614 | ex1_intro: ∀ x:A. P x → ex_Type1 A P. |
---|
615 | (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) |
---|
616 | |
---|
617 | lemma err_eq_from_io : ∀O,I,X,m,v. |
---|
618 | err_to_io O I X m = return v → m = return v. |
---|
619 | #O #I #X * #x #v normalize #EQ destruct % qed. |
---|
620 | |
---|
621 | lemma linearise_ok: |
---|
622 | ∀p,p',graph_prog. |
---|
623 | let lin_prog ≝ linearise ? graph_prog in |
---|
624 | ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. |
---|
625 | let graph_stack_sizes ≝ |
---|
626 | stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
627 | ? graph_prog lin_stack_sizes in |
---|
628 | ex_Type1 … (λR. |
---|
629 | status_simulation |
---|
630 | (graph_abstract_status p p' graph_prog graph_stack_sizes) |
---|
631 | (lin_abstract_status p p' lin_prog lin_stack_sizes) R). |
---|
632 | #p #p' #graph_prog |
---|
633 | cases (linearise_spec … graph_prog) #sigma #good |
---|
634 | #lin_stack_sizes |
---|
635 | %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)} |
---|
636 | whd whd in ⊢ (%→%→?); |
---|
637 | change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?) |
---|
638 | #st1 |
---|
639 | change with (∀st1 : state_pc (p' (joint_closed_internal_function (mk_graph_params ?))).?) |
---|
640 | #st1' |
---|
641 | change with (∀st : state_pc (p' (joint_closed_internal_function (mk_lin_params ?))).?) |
---|
642 | #st2 |
---|
643 | #ex * #wfprf #rel_st1_st2 |
---|
644 | whd in ex; |
---|
645 | change with |
---|
646 | (eval_state |
---|
647 | (make_sem_graph_params p p') |
---|
648 | (prog_var_names ?? graph_prog) |
---|
649 | ? |
---|
650 | st1 = ?) in ex; |
---|
651 | whd in match eval_state in ex; |
---|
652 | normalize nodelta in ex; |
---|
653 | cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt |
---|
654 | change with (Σi.is_internal_function_of_program … graph_prog i) in fn; * |
---|
655 | change with (globalenv_noinit ? graph_prog) in |
---|
656 | ⊢ (??(???%?)?→?); |
---|
657 | match (ge ?? (ev_genv ?)) in ⊢ (%→?); |
---|
658 | st1' |
---|
659 | whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
660 | >fetch_statement_spec in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
661 | whd in fetch_statement_spec : (??()%); |
---|
662 | cases cl in classified_st1_cl; -cl #classified_st1_cl whd |
---|
663 | [4: |
---|
664 | >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog) |
---|
665 | cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ] |
---|
666 | #sigma_entry_is_zero #sigma_spec |
---|
667 | lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1))) |
---|
668 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ] |
---|
669 | -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec |
---|
670 | cases (opt_Exists_elim … sigma_spec) in ⊢ ?; |
---|
671 | * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved |
---|
672 | #related_lin_stm_graph_stm |
---|
673 | |
---|
674 | inversion (stmt_implicit_label ???) |
---|
675 | [ whd in match (opt_All ???); #stmt_implicit_spec #_ |
---|
676 | letin st2_opt' ≝ (eval_state … |
---|
677 | (ev_genv (lin_prog_params … lin_prog lin_stack_sizes)) |
---|
678 | (sigma_state … wf_st1)) |
---|
679 | cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2') |
---|
680 | [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' |
---|
681 | normalize nodelta in st2_spec'; -st2_opt' |
---|
682 | %{st2'} %{(taaf_step … (taa_base …) …)} |
---|
683 | [ cases daemon (* TODO, together with the previous one? *) |
---|
684 | | @st2_spec' ] |
---|
685 | %[%] [%] |
---|
686 | [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec'; |
---|
687 | >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec'; |
---|
688 | >m_return_bind |
---|
689 | (* Case analysis over the possible statements *) |
---|
690 | inversion graph_stmt in stmt_implicit_spec; normalize nodelta |
---|
691 | [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ] |
---|
692 | XXXXXXXXXX siamo qua, caso GOTO e RETURN |
---|
693 | | cases daemon (* TODO, after the definition of label_rel, trivial *) ] |
---|
694 | ] |
---|
695 | | .... |
---|
696 | qed. |
---|