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 | lemma bind_option_inversion_star: |
---|
21 | ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B. |
---|
22 | (∀x.f = Some … x → g x = Some … y → P) → |
---|
23 | (! x ← f ; g x = Some … y) → P. |
---|
24 | #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed. |
---|
25 | |
---|
26 | interpretation "option bind inversion" 'bind_inversion = |
---|
27 | (bind_option_inversion_star ???????). |
---|
28 | |
---|
29 | lemma bind_inversion_star : ∀X,Y.∀P : Prop. |
---|
30 | ∀m : res X.∀f : X → res Y.∀v : Y. |
---|
31 | (∀x. m = return x → f x = return v → P) → |
---|
32 | ! x ← m ; f x = return v → P. |
---|
33 | #X #Y #P #m #f #v #H #G |
---|
34 | elim (bind_inversion ????? G) #x * @H qed. |
---|
35 | |
---|
36 | interpretation "res bind inversion" 'bind_inversion = |
---|
37 | (bind_inversion_star ???????). |
---|
38 | |
---|
39 | lemma IO_bind_inversion: |
---|
40 | ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. |
---|
41 | (∀x.f = return x → g x = return y → P) → |
---|
42 | (! x ← f ; g x = return y) → P. |
---|
43 | #O #I #A #B #P #f #g #y cases f normalize |
---|
44 | [ #o #f #_ #H destruct |
---|
45 | | #a #G #H @(G ? (refl …) H) |
---|
46 | | #e #_ #H destruct |
---|
47 | ] qed. |
---|
48 | |
---|
49 | interpretation "IO bind inversion" 'bind_inversion = |
---|
50 | (IO_bind_inversion ?????????). |
---|
51 | |
---|
52 | record MonadFunctRel (M1 : Monad) (M2 : Monad) : Type[1] ≝ |
---|
53 | { m_frel :6> ∀X,Y.∀P : X → Prop.(∀x.P x → Y) → (M1 X → M2 Y → Prop) |
---|
54 | ; mfr_return : ∀X,Y,P,F,x,prf.m_frel X Y P F (return x) (return (F x prf)) |
---|
55 | ; mfr_bind : ∀X,Y,Z,W,P,Q,F,G,m,n. |
---|
56 | m_frel X Y P F m n → ∀f,g.(∀x,prf.m_frel Z W Q G (f x) (g (F x prf))) → |
---|
57 | m_frel ?? Q G (m_bind … m f) (m_bind … n g) |
---|
58 | ; m_frel_ext : ∀X,Y,P,F,G.(∀x,prf1,prf2.F x prf1 = G x prf2) → ∀u,v.m_frel X Y P F u v → m_frel X Y P G u v |
---|
59 | }. |
---|
60 | |
---|
61 | (*definition IO_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ |
---|
62 | λO,I.mk_MonadFunctRel ?? |
---|
63 | (λX,Y,F,m,n.∀x.m = return x → n = return F x) |
---|
64 | ???. |
---|
65 | [ #X #Y #F #x #y whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
66 | | #X #Y #Z #W #F #G * |
---|
67 | [ #o #f | #u | #e ] #n #H #f #g #K #x |
---|
68 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
69 | >(H ? (refl …)) @K @EQ |
---|
70 | | #X #Y #P #Q #H #z #w #G #x #EQ >(G … EQ) >H % |
---|
71 | ] |
---|
72 | qed.*) |
---|
73 | |
---|
74 | definition res_preserve : MonadFunctRel Res Res ≝ |
---|
75 | mk_MonadFunctRel ?? |
---|
76 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
---|
77 | ???. |
---|
78 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
---|
79 | | #X #Y #Z #W #P #Q #F #G * |
---|
80 | [ #u | #e ] #n #H #f #g #K #x |
---|
81 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
82 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
---|
83 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
---|
84 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
---|
85 | ] |
---|
86 | qed. |
---|
87 | |
---|
88 | definition opt_preserve : MonadFunctRel Option Option ≝ |
---|
89 | mk_MonadFunctRel ?? |
---|
90 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
---|
91 | ???. |
---|
92 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
---|
93 | | #X #Y #Z #W #P #Q #F #G * |
---|
94 | [ | #u ] #n #H #f #g #K #x |
---|
95 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
96 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
---|
97 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
---|
98 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
---|
99 | ] |
---|
100 | qed. |
---|
101 | |
---|
102 | definition io_preserve : ∀O,I.MonadFunctRel (IOMonad O I) (IOMonad O I) ≝ |
---|
103 | λO,I.mk_MonadFunctRel ?? |
---|
104 | (λX,Y,P,F,m,n.∀x.m = return x → ∃prf.n = return F x prf) |
---|
105 | ???. |
---|
106 | [ #X #Y #P #F #x #prf #x' whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % |
---|
107 | | #X #Y #Z #W #P #Q #F #G * |
---|
108 | [ #o #f | #u | #e ] #n #H #f #g #K #x |
---|
109 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
110 | cases (H ? (refl …)) #prf #L >L @(K ? prf ? EQ) |
---|
111 | | #X #Y #P #F #G #H #u #v #K #x #EQ |
---|
112 | cases (K … EQ) #prf #EQ' %{prf} >EQ' >H try % |
---|
113 | ] |
---|
114 | qed. |
---|
115 | |
---|
116 | definition preserving ≝ |
---|
117 | λM1,M2.λFR : MonadFunctRel M1 M2. |
---|
118 | λX,Y,A,B : Type[0]. |
---|
119 | λP : X → Prop. |
---|
120 | λQ : A → Prop. |
---|
121 | λF : ∀x : X.P x → Y. |
---|
122 | λG : ∀a : A.Q a → B. |
---|
123 | λf : X → M1 A. |
---|
124 | λg : Y → M2 B. |
---|
125 | ∀x,prf. |
---|
126 | FR … G |
---|
127 | (f x) (g (F x prf)). |
---|
128 | |
---|
129 | definition preserving2 ≝ |
---|
130 | λM1,M2.λFR : MonadFunctRel M1 M2. |
---|
131 | λX,Y,Z,W,A,B : Type[0]. |
---|
132 | λP : X → Prop. |
---|
133 | λQ : Y → Prop. |
---|
134 | λR : A → Prop. |
---|
135 | λF : ∀x : X.P x → Z. |
---|
136 | λG : ∀y : Y.Q y → W. |
---|
137 | λH : ∀a : A.R a → B. |
---|
138 | λf : X → Y → M1 A. |
---|
139 | λg : Z → W → M2 B. |
---|
140 | ∀x,y,prf1,prf2. |
---|
141 | FR … H |
---|
142 | (f x y) (g (F x prf1) (G y prf2)). |
---|
143 | |
---|
144 | definition graph_prog_params ≝ |
---|
145 | λp,p',prog,stack_sizes. |
---|
146 | mk_prog_params (make_sem_graph_params p p') prog stack_sizes. |
---|
147 | |
---|
148 | definition graph_abstract_status: |
---|
149 | ∀p:unserialized_params. |
---|
150 | (∀F.sem_unserialized_params p F) → |
---|
151 | ∀prog : joint_program (mk_graph_params p). |
---|
152 | (ident → option ℕ) → |
---|
153 | abstract_status |
---|
154 | ≝ |
---|
155 | λp,p',prog,stack_sizes. |
---|
156 | joint_abstract_status (graph_prog_params ? p' prog stack_sizes). |
---|
157 | |
---|
158 | definition lin_prog_params ≝ |
---|
159 | λp,p',prog,stack_sizes. |
---|
160 | mk_prog_params (make_sem_lin_params p p') prog stack_sizes. |
---|
161 | |
---|
162 | definition lin_abstract_status: |
---|
163 | ∀p:unserialized_params. |
---|
164 | (∀F.sem_unserialized_params p F) → |
---|
165 | ∀prog : joint_program (mk_lin_params p). |
---|
166 | (ident → option ℕ) → |
---|
167 | abstract_status |
---|
168 | ≝ |
---|
169 | λp,p',prog,stack_sizes. |
---|
170 | joint_abstract_status (lin_prog_params ? p' prog stack_sizes). |
---|
171 | |
---|
172 | (* |
---|
173 | axiom P : |
---|
174 | ∀A,B,prog.A (prog_var_names (λvars.fundef (A vars)) B prog) → Prop. |
---|
175 | |
---|
176 | check (λpars.let pars' ≝ make_global pars in λx :joint_closed_internal_function pars' (globals pars'). P … x) |
---|
177 | (* |
---|
178 | unification hint 0 ≔ p, prog, stack_sizes ; |
---|
179 | pars ≟ mk_prog_params p prog stack_sizes , |
---|
180 | pars' ≟ make_global pars, |
---|
181 | A ≟ λvars.joint_closed_internal_function p vars, |
---|
182 | B ≟ ℕ |
---|
183 | ⊢ |
---|
184 | A (prog_var_names (λvars.fundef (A vars)) B prog) ≡ |
---|
185 | joint_closed_internal_function pars' (globals pars'). |
---|
186 | *) |
---|
187 | axiom T : ∀A,B,prog.genv_t (fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog))) → Prop. |
---|
188 | (*axiom Q : ∀A,B,init,prog. |
---|
189 | T … (globalenv (λvars:list ident.fundef (A vars)) B |
---|
190 | init prog) → Prop. |
---|
191 | |
---|
192 | lemma pippo : |
---|
193 | ∀p,p',prog,stack_sizes. |
---|
194 | let pars ≝ graph_prog_params p p' prog stack_sizes in |
---|
195 | let ge ≝ ev_genv pars in T ?? prog ge → Prop. |
---|
196 | |
---|
197 | #H1 #H2 #H3 #H4 |
---|
198 | #H5 |
---|
199 | whd in match (ev_genv ?) in H5; |
---|
200 | whd in match (globalenv_noinit) in H5; normalize nodelta in H5; |
---|
201 | whd in match (prog ?) in H5; |
---|
202 | whd in match (joint_function ?) in H5; |
---|
203 | @(Q … H5) |
---|
204 | λx:T ??? ge.Q ???? x) |
---|
205 | *) |
---|
206 | axiom Q : ∀A,B,init,prog,i. |
---|
207 | is_internal_function |
---|
208 | (A |
---|
209 | (prog_var_names (λvars:list ident.fundef (A vars)) B |
---|
210 | prog)) |
---|
211 | (globalenv (λvars:list ident.fundef (A vars)) B |
---|
212 | init prog) |
---|
213 | i → Prop. |
---|
214 | |
---|
215 | check |
---|
216 | (λp,p',prog,stack_sizes,i. |
---|
217 | let pars ≝ graph_prog_params p p' prog stack_sizes in |
---|
218 | let ge ≝ ev_genv pars in |
---|
219 | λx:is_internal_function (joint_closed_internal_function pars (globals pars)) |
---|
220 | ge i.Q ??? prog ? x) |
---|
221 | *) |
---|
222 | |
---|
223 | definition sigma_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p). |
---|
224 | joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) → |
---|
225 | label → option ℕ. |
---|
226 | |
---|
227 | definition sigma_pc_opt: |
---|
228 | ∀p,p'.∀graph_prog. |
---|
229 | sigma_map p graph_prog → |
---|
230 | program_counter → option program_counter |
---|
231 | ≝ |
---|
232 | λp,p',prog,sigma,pc. |
---|
233 | let pars ≝ make_sem_graph_params p p' in |
---|
234 | let ge ≝ globalenv_noinit … prog in |
---|
235 | ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ; |
---|
236 | ! lin_point ← sigma fd (point_of_pc pars pc) ; |
---|
237 | return pc_of_point |
---|
238 | (make_sem_lin_params ? p') (pc_block pc) lin_point. |
---|
239 | |
---|
240 | definition well_formed_pc: |
---|
241 | ∀p,p',graph_prog. |
---|
242 | sigma_map p graph_prog → |
---|
243 | program_counter → Prop |
---|
244 | ≝ |
---|
245 | λp,p',prog,sigma,pc. |
---|
246 | sigma_pc_opt p p' prog sigma pc |
---|
247 | ≠ None …. |
---|
248 | |
---|
249 | definition sigma_beval_opt : |
---|
250 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
251 | sigma_map p graph_prog → |
---|
252 | beval → option beval ≝ |
---|
253 | λp,p',graph_prog,sigma,bv. |
---|
254 | match bv with |
---|
255 | [ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt p p' graph_prog sigma pc ; return BVpc pc' prt |
---|
256 | | _ ⇒ return bv |
---|
257 | ]. |
---|
258 | |
---|
259 | definition sigma_beval : |
---|
260 | ∀p,p',graph_prog,sigma,bv. |
---|
261 | sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝ |
---|
262 | λp,p',graph_prog,sigma,bv.opt_safe …. |
---|
263 | |
---|
264 | definition sigma_is_opt : |
---|
265 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
266 | sigma_map p graph_prog → |
---|
267 | internal_stack → option internal_stack ≝ |
---|
268 | λp,p',graph_prog,sigma,is. |
---|
269 | match is with |
---|
270 | [ empty_is ⇒ return empty_is |
---|
271 | | one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv' |
---|
272 | | both_is bv1 bv2 ⇒ |
---|
273 | ! bv1' ← sigma_beval_opt p p' … sigma bv1 ; |
---|
274 | ! bv2' ← sigma_beval_opt p p' … sigma bv2 ; |
---|
275 | return both_is bv1' bv2' |
---|
276 | ]. |
---|
277 | |
---|
278 | definition sigma_is : |
---|
279 | ∀p,p',graph_prog,sigma,is. |
---|
280 | sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝ |
---|
281 | λp,p',graph_prog,sigma,is.opt_safe …. |
---|
282 | |
---|
283 | lemma sigma_is_empty : ∀p,p',graph_prog,sigma. |
---|
284 | ∀prf.sigma_is p p' graph_prog sigma empty_is prf = empty_is. |
---|
285 | #p #p' #graph_prog #sigma #prf whd in match sigma_is; normalize nodelta |
---|
286 | @opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. |
---|
287 | |
---|
288 | lemma res_preserve_error : ∀X,Y,P,F,e,n.res_preserve X Y P F (Error … e) n. |
---|
289 | #X #Y #P #F #e #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
---|
290 | |
---|
291 | lemma mfr_return_eq : ∀M1,M2.∀FR : MonadFunctRel M1 M2. |
---|
292 | ∀X,Y,P,F,v,n. |
---|
293 | ∀prf.n = return F v prf → |
---|
294 | FR X Y P F (return v) n. |
---|
295 | #M1 #M2 #FR #X #Y #P #F #v #n #prf #EQ >EQ @mfr_return qed. |
---|
296 | |
---|
297 | lemma opt_safe_eq : ∀A,m,x,prf.m = Some A x → opt_safe A m prf = x. |
---|
298 | #A #m #x #prf @opt_safe_elim #x' #EQ >EQ #EQ' destruct % qed. |
---|
299 | |
---|
300 | lemma sigma_is_pop_commute : |
---|
301 | ∀p,p',graph_prog,sigma,is. |
---|
302 | ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?. |
---|
303 | res_preserve … |
---|
304 | (λpr.sigma_beval_opt p p' graph_prog sigma (\fst pr) ≠ None ? ∧ |
---|
305 | sigma_is_opt p p' graph_prog sigma (\snd pr) ≠ None ?) |
---|
306 | (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉) |
---|
307 | (is_pop is) (is_pop (sigma_is … prf)). |
---|
308 | #p #p' #graph_prog #sigma * [|#bv1|#bv1 #bv2] #prf |
---|
309 | [ @res_preserve_error |
---|
310 | |*: |
---|
311 | whd in match sigma_is in ⊢ (?????????%); normalize nodelta |
---|
312 | @opt_safe_elim #is' |
---|
313 | #H @('bind_inversion H) -H #bv1' #EQ1 |
---|
314 | [2: #H @('bind_inversion H) -H #bv2' #EQ2 ] |
---|
315 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
316 | @mfr_return_eq |
---|
317 | [1,3: @hide_prf %% |
---|
318 | |*: whd in match sigma_beval; whd in match sigma_is; |
---|
319 | normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is'' |
---|
320 | ] |
---|
321 | [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ] |
---|
322 | whd in ⊢ (??%%→?); #EQ destruct(EQ) ] |
---|
323 | [1,3: >EQ2 |*: >EQ1 ] #EQ' destruct(EQ') % |
---|
324 | ] |
---|
325 | qed. |
---|
326 | |
---|
327 | (* lemma opt_to_res_preserve : ∀X,Y.∀P : X → Y → Prop.∀e,u,v. |
---|
328 | opt_preserve P u v → res_preserve P (opt_to_res … e u) (opt_to_res … e v). |
---|
329 | #X #Y #P #e #u #v #H #x #EQ lapply (opt_eq_from_res ???? EQ) -EQ #EQ |
---|
330 | lapply (H … EQ) cases v [ * ] #y #K @K qed. |
---|
331 | |
---|
332 | lemma err_eq_from_io : ∀O,I,X,m,v. |
---|
333 | err_to_io O I X m = return v → m = return v. |
---|
334 | #O #I #X * #x #v normalize #EQ destruct % qed. |
---|
335 | |
---|
336 | lemma res_to_io_preserve : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v. |
---|
337 | res_preserve P u v → IO_preserve O I P u v. |
---|
338 | #X #Y #P #O #I #u #v #H #x #EQ lapply (err_eq_from_io ????? EQ) -EQ #EQ |
---|
339 | lapply (H … EQ) cases v [2: #e * ] #y #K @K qed. |
---|
340 | |
---|
341 | lemma preserve_opt_to_res : ∀X,Y.∀P : X → Y → Prop.∀e,u,v. |
---|
342 | res_preserve P (opt_to_res … e u) (opt_to_res … e v) → opt_preserve P u v. |
---|
343 | #X #Y #P #e #u #v #H #x #EQ |
---|
344 | lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [ * ] |
---|
345 | #y #K @K qed. |
---|
346 | |
---|
347 | lemma preserve_res_to_io : ∀X,Y.∀P : X → Y → Prop.∀O,I,u,v. |
---|
348 | IO_preserve O I P (err_to_io … u) (err_to_io … v) → res_preserve P u v. |
---|
349 | #X #Y #P #O #I #u #v #H #x #EQ |
---|
350 | lapply (H x) >EQ -H #H lapply (H (refl …)) cases v [2: #e * ] |
---|
351 | #y #K @K qed. *) |
---|
352 | |
---|
353 | definition well_formed_mem : |
---|
354 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
355 | sigma_map p graph_prog → |
---|
356 | bemem → Prop ≝ |
---|
357 | λp,p',graph_prog,sigma,m. |
---|
358 | ∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b → |
---|
359 | sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?. |
---|
360 | |
---|
361 | definition sigma_mem : |
---|
362 | ∀p,p',graph_prog,sigma,m. |
---|
363 | well_formed_mem p p' graph_prog sigma m → |
---|
364 | bemem ≝ |
---|
365 | λp,p',graph_prog,sigma,m,prf. |
---|
366 | mk_mem |
---|
367 | (λb. |
---|
368 | If Zltb (block_id b) (nextblock m) then with prf' do |
---|
369 | let l ≝ low_bound m b in |
---|
370 | let h ≝ high_bound m b in |
---|
371 | mk_block_contents l h |
---|
372 | (λz.If Zleb l z ∧ Zltb z h then with prf'' do |
---|
373 | sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ? |
---|
374 | else BVundef) |
---|
375 | else empty_block OZ OZ) |
---|
376 | (nextblock m) |
---|
377 | (nextblock_pos m). |
---|
378 | @hide_prf |
---|
379 | lapply prf'' lapply prf' -prf' -prf'' |
---|
380 | @Zltb_elim_Type0 [2: #_ * ] |
---|
381 | #bid_ok * |
---|
382 | @Zleb_elim_Type0 [2: #_ * ] |
---|
383 | @Zltb_elim_Type0 [2: #_ #_ * ] |
---|
384 | #zh #zl * @(prf … bid_ok zl zh) |
---|
385 | qed. |
---|
386 | |
---|
387 | lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false. |
---|
388 | ** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed. |
---|
389 | |
---|
390 | axiom mem_ext_eq : |
---|
391 | ∀m1,m2 : mem. |
---|
392 | (∀b.let bc1 ≝ blocks m1 b in |
---|
393 | let bc2 ≝ blocks m2 b in |
---|
394 | low bc1 = low bc2 ∧ high bc1 = high bc2 ∧ |
---|
395 | ∀z.contents bc1 z = contents bc2 z) → |
---|
396 | nextblock m1 = nextblock m2 → m1 = m2. |
---|
397 | |
---|
398 | lemma opt_preserve_none : ∀X,Y,P,F,n.opt_preserve X Y P F (None ?) n. |
---|
399 | #X #Y #P #F #n #x whd in ⊢ (??%%→?); #EQ destruct(EQ) qed. |
---|
400 | |
---|
401 | lemma beloadv_sigma_commute: |
---|
402 | ∀p,p',graph_prog,sigma,ptr. |
---|
403 | preserving … opt_preserve … |
---|
404 | (sigma_mem p p' graph_prog sigma) |
---|
405 | (sigma_beval p p' graph_prog sigma) |
---|
406 | (λm.beloadv m ptr) |
---|
407 | (λm.beloadv m ptr). |
---|
408 | #p #p' #graph_prog #sigma #ptr #m #prf #bv |
---|
409 | whd in match beloadv; |
---|
410 | whd in match do_if_in_bounds; |
---|
411 | whd in match sigma_mem; |
---|
412 | normalize nodelta |
---|
413 | @If_elim #block_ok >block_ok normalize nodelta |
---|
414 | [2: whd in ⊢ (???%→?); #ABS destruct(ABS) ] |
---|
415 | @If_elim #H |
---|
416 | [ elim (andb_true … H) |
---|
417 | #H1 #H2 |
---|
418 | whd in match sigma_beval; normalize nodelta |
---|
419 | @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta |
---|
420 | whd in ⊢ (???%→?); #EQ' destruct |
---|
421 | >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe |
---|
422 | | elim (andb_false … H) -H #H >H |
---|
423 | [2: >commutative_andb ] normalize nodelta |
---|
424 | whd in ⊢ (???%→?); #ABS destruct(ABS) |
---|
425 | ] |
---|
426 | qed. |
---|
427 | |
---|
428 | lemma bestorev_sigma_commute : |
---|
429 | ∀p,p',graph_prog,sigma,ptr. |
---|
430 | preserving2 ?? opt_preserve … |
---|
431 | (sigma_mem p p' graph_prog sigma) |
---|
432 | (sigma_beval p p' graph_prog sigma) |
---|
433 | (sigma_mem p p' graph_prog sigma) |
---|
434 | (λm.bestorev m ptr) |
---|
435 | (λm.bestorev m ptr). |
---|
436 | #p #p' #graph_prog #sigma #ptr #m #bv #prf1 #prf2 #m' |
---|
437 | whd in match bestorev; |
---|
438 | whd in match do_if_in_bounds; |
---|
439 | whd in match sigma_mem; |
---|
440 | whd in match update_block; |
---|
441 | normalize nodelta |
---|
442 | @If_elim #block_ok >block_ok normalize nodelta |
---|
443 | [2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)] |
---|
444 | @Zleb_elim_Type0 #H1 |
---|
445 | [ @Zltb_elim_Type0 #H2 ] |
---|
446 | [2,3: #ABS normalize in ABS; destruct(ABS) ] |
---|
447 | normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ) |
---|
448 | % |
---|
449 | [2: whd in ⊢ (???%); |
---|
450 | cut (∀X,a,b.a = b → Some X a = Some X b) [ // ] |
---|
451 | #aux @aux |
---|
452 | @mem_ext_eq [2: % ] |
---|
453 | #b @if_elim |
---|
454 | [2: #B |
---|
455 | @If_elim #prf1 @If_elim #prf2 |
---|
456 | [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ] |
---|
457 | whd in match low_bound; whd in match high_bound; |
---|
458 | normalize nodelta |
---|
459 | cut (Not (bool_to_Prop (eq_block b (pblock ptr)))) |
---|
460 | [ % #ABS >ABS in B; * ] |
---|
461 | -B #B % [ >B %% ] #z |
---|
462 | @If_elim #prf3 |
---|
463 | @If_elim #prf4 |
---|
464 | [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ] |
---|
465 | whd in match sigma_beval in ⊢ (??%%); normalize nodelta |
---|
466 | @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; |
---|
467 | >EQ2 #EQ destruct(EQ) % |
---|
468 | | #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ] |
---|
469 | #EQ destruct(EQ) |
---|
470 | @If_elim whd in match low_bound; whd in match high_bound; |
---|
471 | normalize nodelta |
---|
472 | [2: >block_ok * #ABS elim (ABS I) ] |
---|
473 | #prf3 % [ >B %% ] |
---|
474 | #z whd in match update; normalize nodelta |
---|
475 | @eqZb_elim normalize nodelta #prf4 |
---|
476 | [2: @If_elim #prf5 @If_elim #prf6 |
---|
477 | [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ] |
---|
478 | whd in match sigma_beval in ⊢ (??%%); normalize nodelta |
---|
479 | @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; |
---|
480 | normalize nodelta >(eqZb_false … prf4) >EQ2 |
---|
481 | #EQ destruct(EQ) % |
---|
482 | | @If_elim #prf5 |
---|
483 | [2: >B in prf5; normalize nodelta |
---|
484 | >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ] |
---|
485 | whd in match sigma_beval in ⊢ (??%%); normalize nodelta |
---|
486 | @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1; |
---|
487 | normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) % |
---|
488 | ] |
---|
489 | ] |
---|
490 | | whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta |
---|
491 | @eq_block_elim #H normalize nodelta destruct |
---|
492 | #h2 #h3 whd in match update; normalize nodelta |
---|
493 | [ @eqZb_elim #H destruct normalize nodelta [ assumption ]] |
---|
494 | @prf1 assumption |
---|
495 | ] |
---|
496 | qed. |
---|
497 | |
---|
498 | record good_sem_state_sigma |
---|
499 | (p : unserialized_params) |
---|
500 | (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) |
---|
501 | (sigma : sigma_map p graph_prog) : Type[0] ≝ |
---|
502 | { well_formed_frames : framesT (make_sem_graph_params p p') → Prop |
---|
503 | ; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p') |
---|
504 | ; sigma_empty_frames_commute : |
---|
505 | ∃prf. |
---|
506 | empty_framesT (make_sem_lin_params p p') = |
---|
507 | sigma_frames (empty_framesT (make_sem_graph_params p p')) prf |
---|
508 | |
---|
509 | ; well_formed_regs : regsT (make_sem_graph_params p p') → Prop |
---|
510 | ; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p') |
---|
511 | ; sigma_empty_regsT_commute : |
---|
512 | ∀ptr.∃ prf. |
---|
513 | empty_regsT (make_sem_lin_params p p') ptr = |
---|
514 | sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf |
---|
515 | ; sigma_load_sp_commute : |
---|
516 | preserving … res_preserve … |
---|
517 | (λ_.True) |
---|
518 | … |
---|
519 | sigma_regs |
---|
520 | (λx.λ_.x) |
---|
521 | (load_sp (make_sem_graph_params p p')) |
---|
522 | (load_sp (make_sem_lin_params p p')) |
---|
523 | ; sigma_save_sp_commute : |
---|
524 | ∀reg,ptr,prf1. ∃prf2. |
---|
525 | save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr = |
---|
526 | sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2 |
---|
527 | }. |
---|
528 | |
---|
529 | definition well_formed_state : |
---|
530 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
531 | ∀sigma. |
---|
532 | good_sem_state_sigma p p' graph_prog sigma → |
---|
533 | state (make_sem_graph_params p p') → Prop ≝ |
---|
534 | λp,p',graph_prog,sigma,gsss,st. |
---|
535 | well_formed_frames … gsss (st_frms … st) ∧ |
---|
536 | sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧ |
---|
537 | well_formed_regs … gsss (regs … st) ∧ |
---|
538 | well_formed_mem p p' graph_prog sigma (m … st). |
---|
539 | |
---|
540 | definition sigma_state : |
---|
541 | ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). |
---|
542 | ∀sigma. |
---|
543 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
544 | ∀st : state (make_sem_graph_params p p'). |
---|
545 | well_formed_state … gsss st → |
---|
546 | state (make_sem_lin_params p p') ≝ |
---|
547 | λp,p',graph_prog,sigma,gsss,st,prf. |
---|
548 | mk_state … |
---|
549 | (sigma_frames p p' graph_prog sigma gsss (st_frms … st) ?) |
---|
550 | (sigma_is p p' graph_prog sigma (istack … st) ?) |
---|
551 | (carry … st) |
---|
552 | (sigma_regs … gsss (regs … st) ?) |
---|
553 | (sigma_mem p p' graph_prog sigma (m … st) ?). |
---|
554 | @hide_prf cases prf ** // |
---|
555 | qed. |
---|
556 | |
---|
557 | |
---|
558 | (* |
---|
559 | lemma sigma_is_pop_wf : |
---|
560 | ∀p,p',graph_prog,sigma,is,bv,is'. |
---|
561 | is_pop is = return 〈bv, is'〉 → |
---|
562 | sigma_is_opt p p' graph_prog sigma is ≠ None ? → |
---|
563 | sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧ |
---|
564 | sigma_is_opt p p' graph_prog sigma is' ≠ None ?. |
---|
565 | cases daemon qed. |
---|
566 | *) |
---|
567 | |
---|
568 | (* |
---|
569 | lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?. |
---|
570 | [ #p #s #st #prf |
---|
571 | whd in match sigma_pc_of_status; normalize nodelta |
---|
572 | @opt_safe_elim |
---|
573 | #n |
---|
574 | lapply (refl … (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
575 | (ev_genv p) (pblock (pc p st)))) |
---|
576 | elim (int_funct_of_block (joint_closed_internal_function p) (globals p) |
---|
577 | (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%); |
---|
578 | [ #_ #ABS normalize in ABS; destruct(ABS) ] |
---|
579 | #f #EQ >m_return_bind |
---|
580 | *) |
---|
581 | |
---|
582 | |
---|
583 | (* |
---|
584 | lemma wf_status_to_wf_pc : |
---|
585 | ∀p,p',graph_prog,stack_sizes. |
---|
586 | ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → |
---|
587 | code_point (mk_graph_params p) → option ℕ). |
---|
588 | ∀st. |
---|
589 | well_formed_status p p' graph_prog stack_sizes sigma st → |
---|
590 | well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st). |
---|
591 | #p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H |
---|
592 | qed. |
---|
593 | *) |
---|
594 | definition sigma_pc : |
---|
595 | ∀p,p',graph_prog. |
---|
596 | ∀sigma. |
---|
597 | ∀pc. |
---|
598 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
599 | program_counter ≝ |
---|
600 | λp,p',graph_prog,sigma,st.opt_safe …. |
---|
601 | |
---|
602 | lemma sigma_pc_ok: |
---|
603 | ∀p,p',graph_prog. |
---|
604 | ∀sigma. |
---|
605 | ∀pc. |
---|
606 | ∀prf:well_formed_pc p p' graph_prog sigma pc. |
---|
607 | sigma_pc_opt p p' graph_prog sigma pc = |
---|
608 | Some … (sigma_pc p p' graph_prog sigma pc prf). |
---|
609 | #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed. |
---|
610 | |
---|
611 | definition well_formed_state_pc : |
---|
612 | ∀p,p',graph_prog,sigma. |
---|
613 | good_sem_state_sigma p p' graph_prog sigma → |
---|
614 | state_pc (make_sem_graph_params p p') → Prop ≝ |
---|
615 | λp,p',prog,sigma,gsss,st. |
---|
616 | well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st. |
---|
617 | |
---|
618 | definition sigma_state_pc : |
---|
619 | ∀p. |
---|
620 | ∀p':∀F.sem_unserialized_params p F. |
---|
621 | ∀graph_prog. |
---|
622 | ∀sigma. |
---|
623 | (* let lin_prog ≝ linearise ? graph_prog in *) |
---|
624 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
625 | ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) |
---|
626 | well_formed_state_pc p p' graph_prog sigma gsss s → |
---|
627 | state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) |
---|
628 | ≝ |
---|
629 | λp,p',graph_prog,sigma,gsss,s,prf. |
---|
630 | let pc' ≝ sigma_pc … (proj1 … prf) in |
---|
631 | let st' ≝ sigma_state … (proj2 … prf) in |
---|
632 | mk_state_pc ? st' pc'. |
---|
633 | (* |
---|
634 | definition sigma_function_name : |
---|
635 | ∀p,graph_prog. |
---|
636 | let lin_prog ≝ linearise p graph_prog in |
---|
637 | (Σf.is_internal_function_of_program … graph_prog f) → |
---|
638 | (Σf.is_internal_function_of_program … lin_prog f) ≝ |
---|
639 | λp,graph_prog,f.«f, if_propagate … (pi2 … f)». |
---|
640 | *) |
---|
641 | lemma m_list_map_All_ok : |
---|
642 | ∀M : MonadProps.∀X,Y,f,l. |
---|
643 | All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'. |
---|
644 | cases daemon qed. |
---|
645 | |
---|
646 | definition helper_def_store__commute : |
---|
647 | ∀p,p',graph_prog,sigma. |
---|
648 | ∀X : ? → Type[0]. |
---|
649 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
650 | ∀store : ∀p,F.∀p' : sem_unserialized_params p F. |
---|
651 | X p → beval → regsT p' → |
---|
652 | res (regsT p'). |
---|
653 | Prop ≝ |
---|
654 | λp,p',graph_prog,sigma,X,gsss,store. |
---|
655 | ∀a : X p.preserving2 … res_preserve … |
---|
656 | (sigma_beval p p' graph_prog sigma) |
---|
657 | (sigma_regs … gsss) |
---|
658 | (sigma_regs … gsss) |
---|
659 | (store … a) |
---|
660 | (store … a). |
---|
661 | |
---|
662 | definition helper_def_retrieve__commute : |
---|
663 | ∀p,p',graph_prog,sigma. |
---|
664 | ∀X : ? → Type[0]. |
---|
665 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
666 | ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F. |
---|
667 | regsT p' → X p → res beval. |
---|
668 | Prop ≝ |
---|
669 | λp,p',graph_prog,sigma,X,gsss,retrieve. |
---|
670 | ∀a : X p. |
---|
671 | preserving … res_preserve … |
---|
672 | (sigma_regs … gsss) |
---|
673 | (sigma_beval p p' graph_prog sigma) |
---|
674 | (λr.retrieve … r a) |
---|
675 | (λr.retrieve … r a). |
---|
676 | |
---|
677 | record good_state_sigma |
---|
678 | (p : unserialized_params) |
---|
679 | (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) |
---|
680 | (sigma : sigma_map p graph_prog) |
---|
681 | : Type[0] ≝ |
---|
682 | { gsss :> good_sem_state_sigma p p' graph_prog sigma |
---|
683 | |
---|
684 | ; acca_store__commute : helper_def_store__commute … gsss acca_store_ |
---|
685 | ; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_ |
---|
686 | ; acca_arg_retrieve_commute : helper_def_retrieve__commute … gsss acca_arg_retrieve_ |
---|
687 | ; accb_store_commute : helper_def_store__commute … gsss accb_store_ |
---|
688 | ; accb_retrieve_commute : helper_def_retrieve__commute … gsss accb_retrieve_ |
---|
689 | ; accb_arg_retrieve_commute : helper_def_retrieve__commute … gsss accb_arg_retrieve_ |
---|
690 | ; dpl_store_commute : helper_def_store__commute … gsss dpl_store_ |
---|
691 | ; dpl_retrieve_commute : helper_def_retrieve__commute … gsss dpl_retrieve_ |
---|
692 | ; dpl_arg_retrieve_commute : helper_def_retrieve__commute … gsss dpl_arg_retrieve_ |
---|
693 | ; dph_store_commute : helper_def_store__commute … gsss dph_store_ |
---|
694 | ; dph_retrieve_commute : helper_def_retrieve__commute … gsss dph_retrieve_ |
---|
695 | ; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_ |
---|
696 | ; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_ |
---|
697 | ; pair_reg_move_commute : ∀mv. |
---|
698 | preserving … res_preserve … (sigma_regs … gsss) (sigma_regs … gsss) |
---|
699 | (λr.pair_reg_move_ ? ? (p' ?) r mv) |
---|
700 | (λr.pair_reg_move_ ? ? (p' ?) r mv) |
---|
701 | ; allocate_locals_commute : |
---|
702 | ∀loc, r1, prf1. ∃ prf2. |
---|
703 | allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) = |
---|
704 | sigma_regs p p' graph_prog sigma gsss (allocate_locals_ ? ? (p' ?) loc r1) prf2 |
---|
705 | ; save_frame_commute : |
---|
706 | ∀dest,fl. |
---|
707 | preserving … res_preserve … |
---|
708 | (λst : state_pc ?.λprf. |
---|
709 | mk_state_pc … |
---|
710 | (sigma_state … gsss st (proj2 ?? prf)) |
---|
711 | (sigma_pc p p' graph_prog sigma (pc … st) (proj1 ?? prf))) |
---|
712 | (sigma_state … gsss) |
---|
713 | (save_frame ?? (p' ?) fl dest) |
---|
714 | (save_frame ?? (p' ?) fl dest) |
---|
715 | ; eval_ext_seq_commute : |
---|
716 | let lin_prog ≝ linearise p graph_prog in |
---|
717 | ∀ stack_sizes. |
---|
718 | ∀ext,i,fn. |
---|
719 | preserving … res_preserve … |
---|
720 | (sigma_state … gsss) |
---|
721 | (sigma_state … gsss) |
---|
722 | (eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) |
---|
723 | ext i fn) |
---|
724 | (eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) |
---|
725 | ext i (\fst (linearise_int_fun … fn))) |
---|
726 | }. |
---|
727 | (* TO BE ADAPTED AS ABOVE |
---|
728 | ; setup_call_commute : |
---|
729 | ∀ n , parsT, call_args , st1 , st2 , prf1. |
---|
730 | setup_call ?? (p' ?) n parsT call_args st1 = return st2 → |
---|
731 | ∃prf2. |
---|
732 | setup_call ?? (p' ?) n parsT call_args (sigma_state p p' graph_prog sigma gsss st1 prf1) = |
---|
733 | return (sigma_state p p' graph_prog sigma gsss st2 prf2) |
---|
734 | ; fetch_external_args_commute : (* TO BE CHECKED *) |
---|
735 | ∀ex_fun,st1,prf1,call_args. |
---|
736 | fetch_external_args ?? (p' ?) ex_fun st1 call_args = |
---|
737 | fetch_external_args ?? (p' ?) ex_fun (sigma_state p p' graph_prog sigma gsss st1 prf1) call_args |
---|
738 | ; set_result_commute : |
---|
739 | ∀ l , call_dest , st1 , st2 , prf1. |
---|
740 | set_result ?? (p' ?) l call_dest st1 = return st2 → |
---|
741 | ∃prf2. |
---|
742 | set_result ?? (p' ?) l call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = |
---|
743 | return (sigma_state p p' graph_prog sigma gsss st2 prf2) |
---|
744 | ; read_result_commute : |
---|
745 | let lin_prog ≝ linearise p graph_prog in |
---|
746 | ∀stack_sizes. |
---|
747 | ∀call_dest , st1 , prf1, l1. |
---|
748 | read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) |
---|
749 | call_dest st1 = return l1 → |
---|
750 | ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?. |
---|
751 | read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) |
---|
752 | call_dest (sigma_state p p' graph_prog sigma gsss st1 prf1) = return opt_safe … prf |
---|
753 | ; pop_frame_commute : |
---|
754 | let lin_prog ≝ linearise p graph_prog in |
---|
755 | ∀stack_sizes. |
---|
756 | ∀ st1 , prf1, curr_id , curr_fn ,st2. |
---|
757 | pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) |
---|
758 | curr_id curr_fn st1 = return st2 → |
---|
759 | ∃prf2. |
---|
760 | let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in |
---|
761 | let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in |
---|
762 | pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) |
---|
763 | curr_id (\fst (linearise_int_fun … curr_fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) = |
---|
764 | return mk_state_pc ? st2' pc' |
---|
765 | }. |
---|
766 | *) |
---|
767 | |
---|
768 | |
---|
769 | |
---|
770 | |
---|
771 | |
---|
772 | lemma store_commute : |
---|
773 | ∀p,p',graph_prog,sigma. |
---|
774 | ∀X : ? → Type[0]. |
---|
775 | ∀store. |
---|
776 | ∀gsss : good_state_sigma p p' graph_prog sigma. |
---|
777 | ∀H : helper_def_store__commute … gsss store. |
---|
778 | ∀a : X p. |
---|
779 | preserving2 … res_preserve … |
---|
780 | (sigma_beval p p' graph_prog sigma) |
---|
781 | (sigma_state … gsss) |
---|
782 | (sigma_state … gsss) |
---|
783 | (helper_def_store ? store … a) |
---|
784 | (helper_def_store ? store … a). |
---|
785 | #p #p' #graph_prog #sigma #X #store #gsss #H #a |
---|
786 | #bv #st #prf1 #prf2 |
---|
787 | @(mfr_bind … (sigma_regs … gsss)) [@H] |
---|
788 | #r #prf3 @mfr_return cases st in prf2; |
---|
789 | #frms #is #carry #r' #m *** #H1 #H2 #H3 #H4 %{H4} % [%{H1 H2}] assumption |
---|
790 | qed. |
---|
791 | |
---|
792 | lemma retrieve_commute : |
---|
793 | ∀p,p',graph_prog,sigma. |
---|
794 | ∀X : ? → Type[0]. |
---|
795 | ∀retrieve. |
---|
796 | ∀gsss : good_sem_state_sigma p p' graph_prog sigma. |
---|
797 | ∀H : helper_def_retrieve__commute … gsss retrieve. |
---|
798 | ∀a : X p . |
---|
799 | preserving … res_preserve … |
---|
800 | (sigma_state … gsss) |
---|
801 | (sigma_beval p p' graph_prog sigma) |
---|
802 | (λst.helper_def_retrieve ? retrieve … st a) |
---|
803 | (λst.helper_def_retrieve ? retrieve … st a). |
---|
804 | #p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #prf @H qed. |
---|
805 | |
---|
806 | (* |
---|
807 | definition acca_store_commute : |
---|
808 | ∀p,p',graph_prog,sigma. |
---|
809 | ∀gss : good_state_sigma p p' graph_prog sigma. |
---|
810 | ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'. |
---|
811 | acca_store … a bv st = return st' → |
---|
812 | ∃prf2. |
---|
813 | acca_store … a |
---|
814 | (sigma_beval p p' graph_prog sigma bv prf1') |
---|
815 | (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 |
---|
816 | ≝ |
---|
817 | λp,p',graph_prog,sigma. |
---|
818 | λgss : good_state_sigma p p' graph_prog sigma. |
---|
819 | store_commute … gss (acca_store__commute … gss). |
---|
820 | |
---|
821 | *) |
---|
822 | |
---|
823 | (* restano: |
---|
824 | ; setup_call : nat → paramsT … uns_pars → call_args uns_pars → |
---|
825 | state st_pars → res (state st_pars) |
---|
826 | ; fetch_external_args: external_function → state st_pars → call_args … uns_pars → |
---|
827 | res (list val) |
---|
828 | ; set_result: list val → call_dest uns_pars → state st_pars → res (state st_pars) |
---|
829 | |
---|
830 | (* from now on, parameters that use the type of functions *) |
---|
831 | ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) |
---|
832 | (* change of pc must be left to *_flow execution *) |
---|
833 | ; pop_frame: ∀globals.∀ge : genv_gen F globals. |
---|
834 | (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars) |
---|
835 | *) |
---|
836 | |
---|
837 | (* |
---|
838 | lemma sigma_pc_commute: |
---|
839 | ∀p,p',graph_prog,sigma,gss,st. |
---|
840 | ∀prf : well_formed_state_pc p p' graph_prog sigma gss st. |
---|
841 | sigma_pc … (pc ? st) (proj1 … prf) = |
---|
842 | pc ? (sigma_state_pc … st prf). // qed. |
---|
843 | *) |
---|
844 | |
---|
845 | (* |
---|
846 | lemma if_of_function_commute: |
---|
847 | ∀p. |
---|
848 | ∀graph_prog : joint_program (mk_graph_params p). |
---|
849 | ∀graph_fun : Σi.is_internal_function_of_program … graph_prog i. |
---|
850 | let graph_fd ≝ if_of_function … graph_fun in |
---|
851 | let lin_fun ≝ sigma_function_name … graph_fun in |
---|
852 | let lin_fd ≝ if_of_function … lin_fun in |
---|
853 | lin_fd = \fst (linearise_int_fun ?? graph_fd). |
---|
854 | #p #graph_prog #graph_fun whd |
---|
855 | @prog_if_of_function_transform % qed. |
---|
856 | *) |
---|
857 | lemma sigma_pblock_eq_lemma : |
---|
858 | ∀p,p',graph_prog. |
---|
859 | let lin_prog ≝ linearise p graph_prog in |
---|
860 | ∀sigma,pc. |
---|
861 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
862 | pc_block (sigma_pc ? p' graph_prog sigma pc prf) = |
---|
863 | pc_block pc. |
---|
864 | #p #p' #graph_prog #sigma #pc #prf |
---|
865 | whd in match sigma_pc; normalize nodelta |
---|
866 | @opt_safe_elim #x #H @('bind_inversion H) -H * #i #fn #_ |
---|
867 | #H @('bind_inversion H) -H #n #_ whd in ⊢ (??%?→?); |
---|
868 | #EQ destruct % |
---|
869 | qed. |
---|
870 | |
---|
871 | (* |
---|
872 | lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B. |
---|
873 | (! x ← m ; g x) ≠ None ? → m ≠ None ?. |
---|
874 | #A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize |
---|
875 | [ #abs elim abs -abs #abs @abs % |
---|
876 | | #abs elim abs -abs #abs #v @abs % |
---|
877 | ] |
---|
878 | qed. |
---|
879 | |
---|
880 | lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A. |
---|
881 | ∀ b : B .∀ f : A → B. ∀g : B → option C. |
---|
882 | g (match m with [None ⇒ b | Some x ⇒ f x])≠ None ? → g b = None ? → m ≠ None ?. |
---|
883 | #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 |
---|
884 | qed. |
---|
885 | *) |
---|
886 | |
---|
887 | (* |
---|
888 | lemma funct_of_block_transf : |
---|
889 | ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. |
---|
890 | ∀transf : ∀vars. A vars → B vars. ∀bl,f,prf. |
---|
891 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
892 | funct_of_block … (globalenv_noinit … progr) bl = return f → |
---|
893 | funct_of_block … (globalenv_noinit … progr') bl = return «pi1 … f,prf». |
---|
894 | #A #B #progr #transf #bl #f #prf whd |
---|
895 | whd in match funct_of_block in ⊢ (%→?); normalize nodelta |
---|
896 | cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. |
---|
897 | ∀o.∀prf : Q o. |
---|
898 | ∀f1,f2. |
---|
899 | (∀x,prf.P (f1 x prf)) → (∀prf.P(f2 prf)) → |
---|
900 | P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) |
---|
901 | [ #A #B #Q #P * /2/ ] #aux |
---|
902 | @aux [2: #_ change with (?=Some ??→?) #ABS destruct(ABS) ] |
---|
903 | #fd #EQfind whd in ⊢ (??%%→?); |
---|
904 | generalize in ⊢ (??(??(????%))?→?); #e #EQ destruct(EQ) |
---|
905 | whd in match funct_of_block; normalize nodelta |
---|
906 | @aux [ # fd' ] |
---|
907 | [2: >(find_funct_ptr_transf … EQfind) #ABS destruct(ABS) ] |
---|
908 | #prf' cases daemon qed. |
---|
909 | |
---|
910 | lemma description_of_function_transf : |
---|
911 | ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. |
---|
912 | ∀transf : ∀vars. A vars → B vars. |
---|
913 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
914 | ∀f_out,prf. |
---|
915 | description_of_function … |
---|
916 | (globalenv_noinit … progr') f_out = |
---|
917 | transf_fundef … (transf ?) (description_of_function … (globalenv_noinit … progr) |
---|
918 | «pi1 … f_out, prf»). |
---|
919 | #A #B #progr #transf #f_out #prf |
---|
920 | whd in match description_of_function in ⊢ (???%); |
---|
921 | normalize nodelta |
---|
922 | cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop. |
---|
923 | ∀o.∀prf : Q o. |
---|
924 | ∀f1,f2. |
---|
925 | (∀x,prf.o = Some ? x → P (f1 x prf)) → (∀prf.o = None ? → P(f2 prf)) → |
---|
926 | P (match o return λx.Q x → B with [ Some x ⇒ f1 x | None ⇒ f2 ] prf)) |
---|
927 | [ #A #B #Q #P * /2/ ] #aux |
---|
928 | @aux |
---|
929 | [ #fd' ] * #fd #EQ destruct (EQ) |
---|
930 | inversion (find_symbol ???) [ #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] |
---|
931 | #bl #EQfind >m_return_bind #EQfindf |
---|
932 | whd in match description_of_function; normalize nodelta |
---|
933 | @aux |
---|
934 | [ #fdo' ] * #fdo #EQ destruct (EQ) |
---|
935 | >find_symbol_transf >EQfind >m_return_bind |
---|
936 | >(find_funct_ptr_transf … EQfindf) #EQ destruct(EQ) % |
---|
937 | qed. |
---|
938 | |
---|
939 | |
---|
940 | lemma match_int_fun : |
---|
941 | ∀A,B : Type[0].∀P : B → Prop. |
---|
942 | ∀Q : fundef A → Prop. |
---|
943 | ∀m : fundef A. |
---|
944 | ∀f1 : ∀fd.Q (Internal \ldots fd) → B. |
---|
945 | ∀f2 : ∀fd.Q (External … fd) → B. |
---|
946 | ∀prf : Q m. |
---|
947 | (∀fd,prf.P (f1 fd prf)) → |
---|
948 | (∀fd,prf.P (f2 fd prf)) → |
---|
949 | P (match m |
---|
950 | return λx.Q x → ? |
---|
951 | with |
---|
952 | [ Internal fd ⇒ f1 fd |
---|
953 | | External fd ⇒ f2 fd |
---|
954 | ] prf). |
---|
955 | #A #B #P #Q * // qed. |
---|
956 | (*) |
---|
957 | lemma match_int_fun : |
---|
958 | ∀A,B : Type[0].∀P : B → Prop. |
---|
959 | ∀m : fundef A. |
---|
960 | ∀f1 : ∀fd.m = Internal … fd → B. |
---|
961 | ∀f2 : ∀fd.m = External … fd → B. |
---|
962 | (∀fd,prf.P (f1 fd prf)) → |
---|
963 | (∀fd,prf.P (f2 fd prf)) → |
---|
964 | P (match m |
---|
965 | return λx.m = x → ? |
---|
966 | with |
---|
967 | [ Internal fd ⇒ f1 fd |
---|
968 | | External fd ⇒ f2 fd |
---|
969 | ] (refl …)). |
---|
970 | #A #B #P * // qed. |
---|
971 | *) |
---|
972 | (* |
---|
973 | lemma prova : |
---|
974 | ∀ A.∀progr : program (λvars. fundef (A vars)) ℕ. |
---|
975 | ∀ M : fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) ℕ progr)). |
---|
976 | ∀ f,g,prf1. |
---|
977 | match M return λx.M = x → option (Σi.is_internal_function_of_program ?? progr i) with |
---|
978 | [Internal fn ⇒ λ prf.return «g,prf1 fn prf» | |
---|
979 | External fn ⇒ λprf.None ? ] (refl ? M) = return f → |
---|
980 | ∃ fn. ∃ prf : M = Internal ? fn . f = «g, prf1 fn prf». |
---|
981 | #H1 #H2 #H3 #H4 #H5 #H6 |
---|
982 | @match_int_fun |
---|
983 | #fd #EQ #EQ' whd in EQ' : (??%%); destruct |
---|
984 | %[|%[| % ]] qed. |
---|
985 | *) |
---|
986 | |
---|
987 | lemma int_funct_of_block_transf: |
---|
988 | ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ. |
---|
989 | ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf. |
---|
990 | let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in |
---|
991 | int_funct_of_block ? (globalenv_noinit … progr) bl = return f → |
---|
992 | int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf». |
---|
993 | #A #B #progr #transf #bl #f #prf |
---|
994 | whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta |
---|
995 | @'bind_inversion #x #x_spec |
---|
996 | @match_int_fun [2: #fd #_ #ABS destruct(ABS) ] |
---|
997 | #fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ) |
---|
998 | whd in match int_funct_of_block; normalize nodelta |
---|
999 | >(funct_of_block_transf … (internal_function_is_function … prf) … x_spec) |
---|
1000 | >m_return_bind |
---|
1001 | @match_int_fun #fd' #prf' [ % ] |
---|
1002 | @⊥ cases x in prf EQdescr prf'; -x #x #x_prf #prf #EQdescr |
---|
1003 | >(description_of_function_transf) [2: @x_prf ] |
---|
1004 | >EQdescr whd in ⊢ (??%%→?); #ABS destruct qed. |
---|
1005 | *) |
---|
1006 | |
---|
1007 | axiom symbol_for_block_transf : |
---|
1008 | ∀A,B,V,init.∀prog_in : program A V. |
---|
1009 | ∀trans : ∀vars.A vars → B vars. |
---|
1010 | let prog_out ≝ transform_program … prog_in trans in |
---|
1011 | ∀bl, i. |
---|
1012 | symbol_for_block … (globalenv … init prog_in) bl = Some ? i → |
---|
1013 | symbol_for_block … (globalenv … init prog_out) bl = Some ? i. |
---|
1014 | |
---|
1015 | lemma fetch_function_transf : |
---|
1016 | ∀A,B,V,init.∀prog_in : program A V. |
---|
1017 | ∀trans : ∀vars.A vars → B vars. |
---|
1018 | let prog_out ≝ transform_program … prog_in trans in |
---|
1019 | ∀bl,i,f. |
---|
1020 | fetch_function … (globalenv … init prog_in) bl = |
---|
1021 | return 〈i, f〉 |
---|
1022 | → fetch_function … (globalenv … init prog_out) bl = |
---|
1023 | return 〈i, trans … f〉. |
---|
1024 | #A #B #V #init #prog_in #trans #bl #i #f |
---|
1025 | whd in match fetch_function; normalize nodelta |
---|
1026 | #H lapply (opt_eq_from_res ???? H) -H |
---|
1027 | #H @('bind_inversion H) -H #id #eq_symbol_for_block |
---|
1028 | #H @('bind_inversion H) -H #fd #eq_find_funct |
---|
1029 | whd in ⊢ (??%?→?); #EQ destruct(EQ) |
---|
1030 | >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind |
---|
1031 | >(find_funct_ptr_transf A B … eq_find_funct) % |
---|
1032 | qed. |
---|
1033 | |
---|
1034 | lemma fetch_internal_function_transf : |
---|
1035 | ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ. |
---|
1036 | ∀trans : ∀vars.A vars → B vars. |
---|
1037 | let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in |
---|
1038 | ∀bl,i,f. |
---|
1039 | fetch_internal_function … (globalenv_noinit … prog_in) bl = |
---|
1040 | return 〈i, f〉 |
---|
1041 | → fetch_internal_function … (globalenv_noinit … prog_out) bl = |
---|
1042 | return 〈i, trans … f〉. |
---|
1043 | #A #B #prog #trans #bl #i #f |
---|
1044 | whd in match fetch_internal_function; normalize nodelta |
---|
1045 | #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch |
---|
1046 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
1047 | >(fetch_function_transf … EQfetch) % |
---|
1048 | qed. |
---|
1049 | |
---|
1050 | (* |
---|
1051 | #H elim (bind_opt_inversion ????? H) -H |
---|
1052 | #x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta |
---|
1053 | @match_opt_prf_elim |
---|
1054 | #H #H1 whd in H : (??%?); |
---|
1055 | cases ( find_funct_ptr |
---|
1056 | (fundef |
---|
1057 | (joint_closed_internal_function |
---|
1058 | (graph_prog_params p p' graph_prog |
---|
1059 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
1060 | (linearise_int_fun p) graph_prog stack_sizes)) |
---|
1061 | (globals |
---|
1062 | (graph_prog_params p p' graph_prog |
---|
1063 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
1064 | (linearise_int_fun p) graph_prog stack_sizes))))) |
---|
1065 | (ev_genv |
---|
1066 | (graph_prog_params p p' graph_prog |
---|
1067 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
1068 | (linearise_int_fun p) graph_prog stack_sizes))) |
---|
1069 | (pblock (pc (make_sem_graph_params p p') st))) in H; [ 2: normalize #abs destruct |
---|
1070 | |
---|
1071 | |
---|
1072 | normalize nodelta |
---|
1073 | #H #H1 |
---|
1074 | cases ( find_funct_ptr |
---|
1075 | (fundef |
---|
1076 | (joint_closed_internal_function |
---|
1077 | (graph_prog_params p p' graph_prog |
---|
1078 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
1079 | (linearise_int_fun p) graph_prog stack_sizes)) |
---|
1080 | (globals |
---|
1081 | (graph_prog_params p p' graph_prog |
---|
1082 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
1083 | (linearise_int_fun p) graph_prog stack_sizes))))) |
---|
1084 | (ev_genv |
---|
1085 | (graph_prog_params p p' graph_prog |
---|
1086 | (stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') |
---|
1087 | (linearise_int_fun p) graph_prog stack_sizes))) |
---|
1088 | (pblock (pc (make_sem_graph_params p p') st))) in H; |
---|
1089 | |
---|
1090 | |
---|
1091 | check find_funct_ptr_transf |
---|
1092 | whd in match int_funct_of_block; normalize nodelta |
---|
1093 | #H elim (bind_inversion ????? H) |
---|
1094 | |
---|
1095 | .. sigma_int_funct_of_block |
---|
1096 | |
---|
1097 | |
---|
1098 | |
---|
1099 | whd in match int_funct_of_block; normalize nodelta |
---|
1100 | elim (bind_inversion ????? H) |
---|
1101 | whd in match int_funct_of_block; normalize nodelta |
---|
1102 | #H elim (bind_inversion ????? H) -H #fn * |
---|
1103 | #H lapply (opt_eq_from_res ???? H) -H |
---|
1104 | #H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H) |
---|
1105 | -H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%); |
---|
1106 | destruct // |
---|
1107 | cases daemon |
---|
1108 | qed. *) |
---|
1109 | |
---|
1110 | lemma stmt_at_sigma_commute: |
---|
1111 | ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma. |
---|
1112 | good_local_sigma p globals graph_code entry lin_code sigma → |
---|
1113 | sigma lbl = return pt → |
---|
1114 | ∀stmt. |
---|
1115 | stmt_at … graph_code |
---|
1116 | lbl = return stmt → |
---|
1117 | All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧ |
---|
1118 | match stmt with |
---|
1119 | [ final s' ⇒ stmt_at … lin_code pt = Some ? (final … s') |
---|
1120 | | sequential s' nxt ⇒ |
---|
1121 | match s' with |
---|
1122 | [ step_seq _ ⇒ |
---|
1123 | (stmt_at … lin_code pt = Some ? (sequential … s' it)) ∧ |
---|
1124 | ((sigma nxt = Some ? (S pt)) ∨ |
---|
1125 | (stmt_at … lin_code (S pt) = Some ? (GOTO … nxt))) |
---|
1126 | | COND a ltrue ⇒ |
---|
1127 | (stmt_at … lin_code pt = Some ? (sequential … s' it) ∧ |
---|
1128 | sigma nxt = Some ? (S pt)) ∨ |
---|
1129 | (stmt_at … lin_code pt = Some ? (FCOND … I a ltrue nxt)) |
---|
1130 | ] |
---|
1131 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
1132 | ]. |
---|
1133 | #p #globals #graph_code #entry #lin_code #lbl #pt #sigma |
---|
1134 | * #_ #lin_stmt_spec #prf |
---|
1135 | elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 ** #stmt1_spec |
---|
1136 | #All_succs_in #next_spec |
---|
1137 | #stmt >stmt1_spec #EQ whd in EQ : (???%); destruct(EQ) |
---|
1138 | % [assumption] |
---|
1139 | // |
---|
1140 | qed. |
---|
1141 | |
---|
1142 | (* |
---|
1143 | |
---|
1144 | >(if_of_function_commute … graph_fun) |
---|
1145 | |
---|
1146 | check opt_Exists |
---|
1147 | check linearise_int_fun |
---|
1148 | check |
---|
1149 | whd in match (stmt_at ????); |
---|
1150 | whd in match (stmt_at ????); |
---|
1151 | cases (linearise_code_spec … p' graph_prog graph_fun |
---|
1152 | (joint_if_entry … graph_fun)) |
---|
1153 | * #lin_code_closed #sigma_entry_is_zero #sigma_spec |
---|
1154 | lapply (sigma_spec |
---|
1155 | (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) |
---|
1156 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ] |
---|
1157 | -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok |
---|
1158 | whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; |
---|
1159 | inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] |
---|
1160 | * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ |
---|
1161 | #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm |
---|
1162 | <sigma_pc_commute >lin_lookup_ok // *) |
---|
1163 | |
---|
1164 | definition good_sigma : |
---|
1165 | ∀p.∀graph_prog : joint_program (mk_graph_params p). |
---|
1166 | (joint_closed_internal_function ? (prog_var_names … graph_prog) → |
---|
1167 | label → option ℕ) → Prop ≝ |
---|
1168 | λp,graph_prog,sigma. |
---|
1169 | ∀fn : joint_closed_internal_function (mk_graph_params p) ?. |
---|
1170 | good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn) |
---|
1171 | (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn). |
---|
1172 | |
---|
1173 | lemma pc_of_label_sigma_commute : |
---|
1174 | ∀p,p',graph_prog,bl,lbl,i,fn. |
---|
1175 | let lin_prog ≝ linearise ? graph_prog in |
---|
1176 | ∀sigma.good_sigma p graph_prog sigma → |
---|
1177 | fetch_internal_function … |
---|
1178 | (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 → |
---|
1179 | let pc' ≝ pc_of_point (make_sem_graph_params p p') … bl lbl in |
---|
1180 | code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl → |
---|
1181 | ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) |
---|
1182 | bl lbl = |
---|
1183 | return sigma_pc p p' graph_prog sigma pc' prf'. |
---|
1184 | #p #p' #graph_prog #bl #lbl #i #fn |
---|
1185 | #sigma #good cases (good fn) -good * #_ #all_labels_in |
---|
1186 | #good #fetchfn >lin_code_has_label #lbl_in |
---|
1187 | whd in match pc_of_label; normalize nodelta |
---|
1188 | > (fetch_internal_function_transf … fetchfn) >m_return_bind |
---|
1189 | inversion (point_of_label ????) |
---|
1190 | [ (* |
---|
1191 | change with (If ? then with prf do ? else ? = ? → ?) |
---|
1192 | @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ] |
---|
1193 | *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS) |
---|
1194 | | #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind |
---|
1195 | % |
---|
1196 | [ @hide_prf whd % |
---|
1197 | | whd in match sigma_pc; normalize nodelta |
---|
1198 | @opt_safe_elim #pc' |
---|
1199 | ] |
---|
1200 | whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind |
---|
1201 | >point_of_pc_of_point |
---|
1202 | >EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) % |
---|
1203 | ] |
---|
1204 | qed. |
---|
1205 | |
---|
1206 | lemma graph_pc_of_label : |
---|
1207 | ∀p,p'.let pars ≝ make_sem_graph_params p p' in |
---|
1208 | ∀globals,ge,bl,i_fn,lbl. |
---|
1209 | fetch_internal_function ? ge bl = return i_fn → |
---|
1210 | pc_of_label pars globals ge bl lbl = |
---|
1211 | OK ? (pc_of_point pars bl lbl). |
---|
1212 | #p #p' #globals #ge #bl #fn #lbl #fetchfn |
---|
1213 | whd in match pc_of_label; normalize nodelta |
---|
1214 | >fetchfn % |
---|
1215 | qed. |
---|
1216 | |
---|
1217 | lemma graph_succ_pc : |
---|
1218 | ∀p,p'.let pars ≝ make_sem_graph_params p p' in |
---|
1219 | ∀pc,lbl. |
---|
1220 | succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl. |
---|
1221 | normalize // |
---|
1222 | qed. |
---|
1223 | |
---|
1224 | lemma fetch_statement_sigma_commute: |
---|
1225 | ∀p,p',graph_prog,pc,f,fn,stmt. |
---|
1226 | let lin_prog ≝ linearise ? graph_prog in |
---|
1227 | ∀sigma.good_sigma p graph_prog sigma → |
---|
1228 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
1229 | fetch_statement (make_sem_graph_params p p') … |
---|
1230 | (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → |
---|
1231 | All ? (λlbl.well_formed_pc p p' graph_prog sigma |
---|
1232 | (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl)) |
---|
1233 | (stmt_labels … stmt) ∧ |
---|
1234 | match stmt with |
---|
1235 | [ sequential s nxt ⇒ |
---|
1236 | match s with |
---|
1237 | [ step_seq x ⇒ |
---|
1238 | fetch_statement (make_sem_lin_params p p') … |
---|
1239 | (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = |
---|
1240 | return 〈f, \fst (linearise_int_fun … fn), |
---|
1241 | sequential (mk_lin_params p) … (step_seq … x ) it〉 ∧ |
---|
1242 | ∃prf'. |
---|
1243 | let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in |
---|
1244 | let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in |
---|
1245 | (nxt_pc = sigma_nxt ∨ fetch_statement (make_sem_lin_params p p') … |
---|
1246 | (globalenv_noinit … lin_prog) nxt_pc = |
---|
1247 | return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) |
---|
1248 | | COND a ltrue ⇒ |
---|
1249 | (∃ prf'. |
---|
1250 | let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in |
---|
1251 | let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in |
---|
1252 | (fetch_statement (make_sem_lin_params p p') … |
---|
1253 | (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = |
---|
1254 | return 〈f, \fst (linearise_int_fun … fn), |
---|
1255 | sequential (mk_lin_params p) … (COND … a ltrue) it〉 ∧ |
---|
1256 | nxt_pc = sigma_nxt)) ∨ |
---|
1257 | fetch_statement (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) (sigma_pc … pc prf) |
---|
1258 | = |
---|
1259 | return 〈f, \fst (linearise_int_fun … fn), FCOND (mk_lin_params p) … I a ltrue nxt〉 |
---|
1260 | ] |
---|
1261 | | final z ⇒ fetch_statement (make_sem_lin_params p p') … |
---|
1262 | (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = |
---|
1263 | return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … z〉 |
---|
1264 | | FCOND abs _ _ _ ⇒ Ⓧabs |
---|
1265 | ]. |
---|
1266 | #p #p' #graph_prog #pc #f #fn #stmt #sigma |
---|
1267 | #good elim (good fn) * #_ #all_labels_in #good_local #wfprf |
---|
1268 | #H elim (fetch_statement_inv … H) #fetchfn #graph_stmt |
---|
1269 | whd in match well_formed_pc in wfprf; normalize nodelta in wfprf; |
---|
1270 | inversion(sigma_pc_opt p p' graph_prog sigma pc) |
---|
1271 | [#ABS @⊥ >ABS in wfprf; * #H @H %] |
---|
1272 | #lin_pc #lin_pc_spec |
---|
1273 | whd in match sigma_pc_opt in lin_pc_spec; normalize nodelta in lin_pc_spec; |
---|
1274 | @('bind_inversion lin_pc_spec) * #id #graph_fun >fetchfn |
---|
1275 | #EQ whd in EQ : (??%?); destruct(EQ) #H @('bind_inversion H) -H |
---|
1276 | #lin_pt #lin_pt_spec #EQ whd in EQ : (??%?); destruct(EQ) |
---|
1277 | lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt) |
---|
1278 | [@lin_pt_spec|] * #H1 #H2 % |
---|
1279 | [ -H2 @(All_mp … H1) #lab #lab_spec |
---|
1280 | whd in match well_formed_pc; normalize nodelta |
---|
1281 | whd in match sigma_pc_opt; normalize nodelta >fetchfn |
---|
1282 | >m_return_bind whd in match point_of_pc; whd in match pc_of_point; |
---|
1283 | normalize nodelta >point_of_offset_of_point |
---|
1284 | cases(sigma graph_fun lab) in lab_spec; [* #ABS @⊥ @ABS %] |
---|
1285 | #linear_pt #_ >m_return_bind whd in ⊢ (?(??%?)); |
---|
1286 | % #ABS destruct(ABS) |
---|
1287 | ] lapply H2 |
---|
1288 | cases (stmt) in H1; [ * [ #s | #a #ltrue ] #nxt | #s | * ] normalize nodelta |
---|
1289 | #all_labels_spec #H3 whd in match fetch_statement; normalize nodelta |
---|
1290 | >sigma_pblock_eq_lemma |
---|
1291 | >(fetch_internal_function_transf … fetchfn) >m_return_bind |
---|
1292 | [ % |
---|
1293 | [ whd in match point_of_pc; whd in match sigma_pc; normalize nodelta |
---|
1294 | @opt_safe_elim #linear_pc whd in match sigma_pc_opt; normalize nodelta |
---|
1295 | >lin_pc_spec #EQ destruct(EQ) >point_of_offset_of_point |
---|
1296 | >(proj1 … H3) >m_return_bind // |
---|
1297 | | |
---|
1298 | % |
---|
1299 | [ @hide_prf whd in match well_formed_pc; whd in match sigma_pc_opt; |
---|
1300 | normalize nodelta lapply fetchfn |
---|
1301 | whd in match fetch_internal_function; normalize nodelta |
---|
1302 | #H4 @('bind_inversion H4) #x #x_spec |
---|
1303 | >x_spec >m_return_bind #EQ >EQ >m_return_bind |
---|
1304 | whd in match pc_of_point; whd in match succ_pc; whd in match point_of_pc; |
---|
1305 | whd in match pc_of_point; normalize nodelta >point_of_offset_of_point |
---|
1306 | cases(proj2 … H3)[ #EQ >EQ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)] |
---|
1307 | cases all_labels_spec #Z #_ #sn |
---|
1308 | whd in match (point_of_succ ???); |
---|
1309 | >(opt_to_opt_safe … Z) % #ABS whd in ABS : (??%?); destruct(ABS) |
---|
1310 | | cases(proj2 … H3) |
---|
1311 | [ #Z %1 whd in match sigma_pc; normalize nodelta |
---|
1312 | @opt_safe_elim #pc1 whd in match sigma_pc_opt; normalize nodelta |
---|
1313 | >lin_pc_spec #EQ destruct(EQ) |
---|
1314 | @opt_safe_elim #pc2 >fetchfn >m_return_bind >graph_succ_pc |
---|
1315 | >point_of_pc_of_point |
---|
1316 | >Z >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) |
---|
1317 | whd in match succ_pc; |
---|
1318 | whd in match point_of_pc; whd in match point_of_succ; normalize nodelta |
---|
1319 | >point_of_offset_of_point % |
---|
1320 | | #Z %2 lapply fetchfn whd in match fetch_internal_function; normalize nodelta |
---|
1321 | #H @('bind_inversion H) -H * #x1 #x2 #x_spec |
---|
1322 | lapply(fetch_function_transf ???? graph_prog |
---|
1323 | (λglobals.transf_fundef ??(λf_in.\fst (linearise_int_fun p globals f_in))) ?? ? x_spec) |
---|
1324 | #HH |
---|
1325 | <sigma_pblock_eq_lemma in HH; [2:@wfprf|||||] #HH >HH >m_return_bind |
---|
1326 | cases x2 normalize nodelta [#g_fun | #xxx] #EQ whd in EQ : (??%%); destruct(EQ) |
---|
1327 | >m_return_bind whd in match point_of_pc; whd in match succ_pc; normalize nodelta |
---|
1328 | whd in match pc_of_point; normalize nodelta >point_of_offset_of_point |
---|
1329 | whd in match sigma_pc; normalize nodelta |
---|
1330 | @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta |
---|
1331 | >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); |
---|
1332 | destruct(EQ) whd in match point_of_pc; normalize nodelta >point_of_offset_of_point |
---|
1333 | >Z >m_return_bind % |
---|
1334 | ] |
---|
1335 | ] |
---|
1336 | ] |
---|
1337 | | cases H3 |
---|
1338 | [ * #Z1 #Z2 %1 % [ @hide_prf whd in match well_formed_pc; |
---|
1339 | whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind |
---|
1340 | >graph_succ_pc >point_of_pc_of_point |
---|
1341 | >Z2 % #ABS whd in ABS : (??%?); destruct(ABS) |
---|
1342 | ] % |
---|
1343 | [ whd in match sigma_pc; normalize nodelta |
---|
1344 | @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta |
---|
1345 | >fetchfn >m_return_bind >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); |
---|
1346 | destruct(EQ) whd in match point_of_pc; normalize nodelta |
---|
1347 | >point_of_offset_of_point >Z1 >m_return_bind % |
---|
1348 | | whd in match sigma_pc; normalize nodelta |
---|
1349 | @opt_safe_elim #line_pc |
---|
1350 | @opt_safe_elim #line_succ_pc whd in match sigma_pc_opt; normalize nodelta |
---|
1351 | >fetchfn >m_return_bind whd in match point_of_pc; whd in match succ_pc; |
---|
1352 | normalize nodelta >point_of_offset_of_point >Z2 >m_return_bind |
---|
1353 | #EQ whd in EQ : (??%?); destruct(EQ) >m_return_bind >lin_pt_spec >m_return_bind |
---|
1354 | #EQ whd in EQ : (??%?); destruct(EQ) whd in match pc_of_point; whd in match point_of_pc; |
---|
1355 | normalize nodelta >point_of_offset_of_point % |
---|
1356 | ] |
---|
1357 | | #Z %2 whd in match sigma_pc; normalize nodelta >fetchfn >m_return_bind |
---|
1358 | @opt_safe_elim #line_pc whd in match sigma_pc_opt; normalize nodelta |
---|
1359 | >fetchfn >m_return_bind >lin_pt_spec >m_return_bind |
---|
1360 | #EQ whd in EQ : (??%?); destruct(EQ) whd in match point_of_pc; normalize nodelta |
---|
1361 | >point_of_offset_of_point >Z >m_return_bind % |
---|
1362 | ] |
---|
1363 | | whd in match sigma_pc; normalize nodelta @opt_safe_elim |
---|
1364 | #line_pc whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind |
---|
1365 | >lin_pt_spec >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) |
---|
1366 | whd in match point_of_pc; normalize nodelta >point_of_offset_of_point |
---|
1367 | >H3 >m_return_bind % |
---|
1368 | ] |
---|
1369 | qed. |
---|
1370 | |
---|
1371 | lemma point_of_pc_sigma_commute : |
---|
1372 | ∀p,p',graph_prog. |
---|
1373 | let lin_prog ≝ linearise p graph_prog in |
---|
1374 | ∀sigma,pc,f,fn,n. |
---|
1375 | ∀prf : well_formed_pc p p' graph_prog sigma pc. |
---|
1376 | fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 → |
---|
1377 | sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n → |
---|
1378 | point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n. |
---|
1379 | #p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma |
---|
1380 | whd in match sigma_pc; normalize nodelta |
---|
1381 | @opt_safe_elim #pc' whd in match sigma_pc_opt; |
---|
1382 | normalize nodelta >EQfetch >m_return_bind >EQsigma |
---|
1383 | whd in ⊢ (??%?→?); #EQ destruct(EQ) |
---|
1384 | @point_of_offset_of_point |
---|
1385 | qed. |
---|
1386 | |
---|
1387 | definition linearise_status_rel: |
---|
1388 | ∀p,p',graph_prog. |
---|
1389 | let lin_prog ≝ linearise p graph_prog in |
---|
1390 | ∀stack_sizes. |
---|
1391 | ∀sigma,gss. |
---|
1392 | good_sigma p graph_prog sigma → |
---|
1393 | status_rel |
---|
1394 | (graph_abstract_status p p' graph_prog stack_sizes) |
---|
1395 | (lin_abstract_status p p' lin_prog stack_sizes) |
---|
1396 | ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good. |
---|
1397 | mk_status_rel … |
---|
1398 | (* sem_rel ≝ *) (λs1,s2. |
---|
1399 | ∃prf: well_formed_state_pc p p' graph_prog sigma gss s1. |
---|
1400 | s2 = sigma_state_pc … s1 prf) |
---|
1401 | (* call_rel ≝ *) (λs1,s2. |
---|
1402 | ∃prf:well_formed_state_pc p p' graph_prog sigma gss s1. |
---|
1403 | pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf)) |
---|
1404 | (* sim_final ≝ *) ?. |
---|
1405 | #st1 #st2 * #prf #EQ2 |
---|
1406 | % |
---|
1407 | whd in ⊢ (%→%); |
---|
1408 | #H lapply (opt_to_opt_safe … H) |
---|
1409 | @opt_safe_elim -H |
---|
1410 | #res #_ |
---|
1411 | #H |
---|
1412 | #H @('bind_inversion H) -H |
---|
1413 | * #f #stmt |
---|
1414 | whd in match fetch_statement; normalize nodelta |
---|
1415 | #H @('bind_inversion H) -H * |
---|
1416 | #id #int_f |
---|
1417 | whd in match fetch_internal_function; normalize nodelta |
---|
1418 | #H @('bind_inversion H) -H * #id1 #int_f1 |
---|
1419 | whd in match fetch_function; normalize nodelta |
---|
1420 | #H lapply(opt_eq_from_res ???? H) -H |
---|
1421 | #H @('bind_inversion H) -H #id2 |
---|
1422 | whd in match symbol_for_block; normalize nodelta |
---|
1423 | whd in match option_map; normalize nodelta |
---|
1424 | cases (find ?? (symbols ? ?) ?) normalize nodelta |
---|
1425 | [1,3: #ABS destruct(ABS)] #sy_bl #EQ destruct(EQ) |
---|
1426 | #H @('bind_inversion H) -H #int_f2 whd in match find_funct_ptr; |
---|
1427 | normalize nodelta cases(block_region (pc_block (pc ? ?))) |
---|
1428 | normalize nodelta [1,3: #ABS destruct(ABS)] |
---|
1429 | cases(block_id (pc_block (pc ??))) normalize nodelta |
---|
1430 | [1,2,4,5: [2,4: #pos] #ABS destruct(ABS)] |
---|
1431 | #pos #int_f2_spec #EQ whd in EQ : (??%?); destruct(EQ) |
---|
1432 | cases int_f1 in int_f2_spec; normalize nodelta |
---|
1433 | [2,4: #ext_f #_ #ABS whd in ABS : (???%); destruct(ABS)] |
---|
1434 | #int_f3 #int_f3_spec #EQ whd in EQ : (??%%); destruct(EQ) |
---|
1435 | #H @('bind_inversion H) -H #stmt1 #H lapply(opt_eq_from_res ???? H) -H |
---|
1436 | #stmt1_spec #EQ whd in EQ : (??%%); destruct(EQ) |
---|
1437 | cases (stmt) in stmt1_spec; normalize nodelta |
---|
1438 | [1,3,4,6: [1,3: #js #jsucc #_ | 2,4: #a #b #c #d #_] #ABS whd in ABS : (???%); |
---|
1439 | destruct(ABS)] |
---|
1440 | #fin_step #fin_step_spec cases (fin_step) in fin_step_spec; normalize nodelta |
---|
1441 | [1,3,4,6: [1,3: #l #_|2,4: #a #b #c #_] #ABS whd in ABS : (???%); destruct(ABS)] |
---|
1442 | #STMT_SPEC #H @('bind_inversion H) -H #state_pc #state_pc_sepc |
---|
1443 | #H @('bind_inversion H) -H #succ_pc whd in match next_of_pc; normalize nodelta |
---|
1444 | #H @('bind_inversion H) -H * #id4 #int_f4 whd in match fetch_statement; normalize nodelta |
---|
1445 | #H @('bind_inversion H) -H * #id5 #int_f5 whd in match fetch_internal_function; normalize nodelta |
---|
1446 | #H @('bind_inversion H) -H * #id6 #int_f6 whd in match fetch_function; normalize nodelta |
---|
1447 | #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #id7 |
---|
1448 | whd in match symbol_for_block; normalize nodelta whd in match option_map; normalize nodelta |
---|
1449 | cases(find ? ? ? ?) normalize nodelta [1,3: #ABS destruct(ABS)] |
---|
1450 | #sy_bl1 #EQ destruct(EQ) #H @('bind_inversion H) -H #int_f7 |
---|
1451 | whd in match find_funct_ptr; normalize nodelta |
---|
1452 | cases(block_region (pc_block ?)) normalize nodelta [1,3: #ABS destruct(ABS)] |
---|
1453 | cases(block_id ?) normalize nodelta [1,2,4,5: [2,4:#p] #ABS destruct(ABS)] |
---|
1454 | #pos1 #int_f7_spec #EQ whd in EQ : (??%?); destruct(EQ) cases (int_f6) in int_f7_spec; |
---|
1455 | normalize nodelta [2,4: #ext_fun #_ #ABS whd in ABS : (???%); destruct(ABS)] |
---|
1456 | #int_f8 #int_f8_spec #EQ whd in EQ : (??%%); destruct(EQ) |
---|
1457 | #H @('bind_inversion H) -H #stmt2 #H lapply(opt_eq_from_res ???? H) -H |
---|
1458 | #stmt2_spec #EQ whd in EQ : (??%%); destruct(EQ) |
---|
1459 | cases int_f4 in stmt2_spec; normalize nodelta |
---|
1460 | [2,3,5,6: |
---|
1461 | |
---|
1462 | xxxxxxxxxxxxxx |
---|
1463 | |
---|
1464 | qed. |
---|
1465 | |
---|
1466 | lemma set_istack_sigma_commute : |
---|
1467 | ∀p,p',graph_prog,sigma,gss,st,is,prf1,prf2,prf3. |
---|
1468 | set_istack ? (sigma_is p p' graph_prog sigma is prf1) (sigma_state p p' graph_prog sigma gss st prf2) = |
---|
1469 | sigma_state ???? gss (set_istack ? is st) prf3. |
---|
1470 | #p #p' #graph_prog #sigma #gss * |
---|
1471 | #frms #is' #carry #r #m #is #prf1 #prf2 #prf3 % qed. |
---|
1472 | (* #st #is #sigmais #prf1 #prf2 #H |
---|
1473 | whd in match set_istack; normalize nodelta |
---|
1474 | whd in match sigma_state; normalize nodelta |
---|
1475 | whd in match sigma_is; normalize nodelta |
---|
1476 | @opt_safe_elim #x #H1 |
---|
1477 | cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %] |
---|
1478 | #EQ >EQ // |
---|
1479 | qed.*) |
---|
1480 | |
---|
1481 | (* this should make things easier for ops using memory (where pc cant happen) *) |
---|
1482 | definition bv_no_pc : beval → Prop ≝ |
---|
1483 | λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ]. |
---|
1484 | |
---|
1485 | lemma bv_pc_other : |
---|
1486 | ∀P : beval → Prop. |
---|
1487 | (∀pc,p.P (BVpc pc p)) → |
---|
1488 | (∀bv.bv_no_pc bv → P bv) → |
---|
1489 | ∀bv.P bv. |
---|
1490 | #P #H1 #H2 * /2/ qed. |
---|
1491 | |
---|
1492 | lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf. |
---|
1493 | bv_no_pc bv → |
---|
1494 | sigma_beval p p' graph_prog sigma bv prf = bv. |
---|
1495 | #p #p' #graph_prog #sigma * |
---|
1496 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] |
---|
1497 | #prf * whd in match sigma_beval; normalize nodelta |
---|
1498 | @opt_safe_elim #bv' normalize #EQ destruct(EQ) % |
---|
1499 | qed. |
---|
1500 | |
---|
1501 | lemma bv_no_pc_wf : ∀p,p',graph_prog,sigma,bv. |
---|
1502 | bv_no_pc bv → sigma_beval_opt p p' graph_prog sigma bv ≠ None ?. |
---|
1503 | #p #p' #graph_prog #sigma * |
---|
1504 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] * |
---|
1505 | % whd in ⊢ (??%?→?); #ABS destruct(ABS) qed. |
---|
1506 | |
---|
1507 | lemma is_push_sigma_commute : |
---|
1508 | ∀ p, p', graph_prog,sigma. |
---|
1509 | preserving2 … res_preserve … |
---|
1510 | (sigma_is p p' graph_prog sigma) |
---|
1511 | (sigma_beval p p' graph_prog sigma) |
---|
1512 | (sigma_is p p' graph_prog sigma) |
---|
1513 | is_push is_push. |
---|
1514 | #p #p' #graph_prog #sigma * |
---|
1515 | [ | #bv1 | #bv1 #bv2 ] #val #prf1 #prf2 #is' |
---|
1516 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
1517 | whd in match sigma_beval; normalize nodelta |
---|
1518 | @opt_safe_elim #val' #EQsigma_val |
---|
1519 | % |
---|
1520 | [1,3: @hide_prf % |
---|
1521 | |*: whd in match sigma_is in ⊢ (???%); normalize nodelta |
---|
1522 | @opt_safe_elim #is'' |
---|
1523 | ] whd in match sigma_is_opt; normalize nodelta |
---|
1524 | [2,4: |
---|
1525 | inversion (sigma_beval_opt ?????) |
---|
1526 | [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1; |
---|
1527 | normalize nodelta * #H @H % ] |
---|
1528 | #bv1' #EQ_bv1' >m_return_bind ] |
---|
1529 | >EQsigma_val |
---|
1530 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
1531 | whd in match sigma_is; normalize nodelta |
---|
1532 | @opt_safe_elim #is1 |
---|
1533 | whd in match sigma_is_opt; normalize nodelta |
---|
1534 | [ #H @('bind_inversion H) #bv1'' |
---|
1535 | >EQ_bv1' #EQ destruct(EQ) ] |
---|
1536 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
1537 | qed. |
---|
1538 | |
---|
1539 | lemma byte_of_val_inv : |
---|
1540 | ∀e,bv,v.Byte_of_val e bv = return v → bv = BVByte v. |
---|
1541 | #e * |
---|
1542 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] #v |
---|
1543 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. |
---|
1544 | |
---|
1545 | lemma bit_of_val_inv : |
---|
1546 | ∀e,bb,v.Bit_of_val e bb = return v → bb = BBbit v. |
---|
1547 | #e * |
---|
1548 | [ #b || #b #ptr #p #o ] #v |
---|
1549 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. |
---|
1550 | |
---|
1551 | lemma beopaccs_sigma_commute : |
---|
1552 | ∀p,p',graph_prog,sigma,op. |
---|
1553 | preserving2 … res_preserve … |
---|
1554 | (sigma_beval p p' graph_prog sigma) |
---|
1555 | (sigma_beval p p' graph_prog sigma) |
---|
1556 | (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf), |
---|
1557 | sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉) |
---|
1558 | (be_opaccs op) (be_opaccs op). |
---|
1559 | #p #p' #graph_prog #sigma #op |
---|
1560 | #bv1 #bv2 #prf1 #prf2 |
---|
1561 | @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] |
---|
1562 | [2: #by1 * @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] |
---|
1563 | [2: #by2 * cases (opaccs ????) #by1' #by2' |
---|
1564 | @mfr_return %% whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
1565 | ] |
---|
1566 | ] |
---|
1567 | #v #EQ %{I} |
---|
1568 | >sigma_bv_no_pc try assumption |
---|
1569 | >(byte_of_val_inv … EQ) % |
---|
1570 | qed. |
---|
1571 | |
---|
1572 | lemma beop1_sigma_commute : |
---|
1573 | ∀p,p',graph_prog,sigma,op. |
---|
1574 | preserving … res_preserve … |
---|
1575 | (sigma_beval p p' graph_prog sigma) |
---|
1576 | (sigma_beval p p' graph_prog sigma) |
---|
1577 | (be_op1 op) (be_op1 op). |
---|
1578 | #p #p' #graph_prog #sigma #op |
---|
1579 | #bv #prf |
---|
1580 | @mfr_bind [ @(λ_.True) | @(λx.λ_.x) ] |
---|
1581 | [2: #by * @mfr_return % whd in ⊢ (??%%→?); #EQ destruct(EQ) ] |
---|
1582 | #v #EQ %{I} >sigma_bv_no_pc try assumption |
---|
1583 | >(byte_of_val_inv … EQ) % |
---|
1584 | qed. |
---|
1585 | |
---|
1586 | |
---|
1587 | lemma sigma_ptr_commute : |
---|
1588 | ∀ p, p', graph_prog , sigma. |
---|
1589 | preserving … res_preserve … |
---|
1590 | (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) (proj1 ?? prf), |
---|
1591 | sigma_beval p p' graph_prog sigma (\snd pr) (proj2 ?? prf)〉) |
---|
1592 | (λx.λ_ : True.x) |
---|
1593 | pointer_of_address pointer_of_address. |
---|
1594 | #p #p' #graph_prog #sigma * #val1 #val2 * #prf1 #prf2 |
---|
1595 | #ptr whd in ⊢ (??%?→?); |
---|
1596 | cases val1 in prf1; |
---|
1597 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr1 #p1 | #pc #p ] |
---|
1598 | #prf1 whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
1599 | cases val2 in prf2 EQ; |
---|
1600 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr2 #p2 | #pc #p ] |
---|
1601 | #prf2 normalize nodelta #EQ destruct(EQ) |
---|
1602 | %{I} |
---|
1603 | >sigma_bv_no_pc [2: %] |
---|
1604 | >sigma_bv_no_pc [2: %] @EQ |
---|
1605 | qed. |
---|
1606 | |
---|
1607 | lemma beop2_sigma_commute : |
---|
1608 | ∀p,p',graph_prog,sigma,carry,op. |
---|
1609 | preserving2 … res_preserve … |
---|
1610 | (sigma_beval p p' graph_prog sigma) |
---|
1611 | (sigma_beval p p' graph_prog sigma) |
---|
1612 | (λpr,prf.〈sigma_beval p p' graph_prog sigma (\fst pr) prf, \snd pr〉) |
---|
1613 | (be_op2 carry op) (be_op2 carry op). |
---|
1614 | #p #p' #graph_prog #sigma #carry #op |
---|
1615 | @bv_pc_other |
---|
1616 | [ #pc1 #p1 #bv2 |
---|
1617 | | #bv1 #bv1_no_pc |
---|
1618 | @bv_pc_other |
---|
1619 | [ #pc2 #p2 |
---|
1620 | | #bv2 #bv2_no_pc |
---|
1621 | ] |
---|
1622 | ] #prf1 #prf2 |
---|
1623 | * #res #carry' |
---|
1624 | [1,2: |
---|
1625 | [2: cases bv1 in prf1; |
---|
1626 | [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] #prf1 ] |
---|
1627 | whd in ⊢ (??%%→?); |
---|
1628 | #EQ destruct(EQ) ] |
---|
1629 | #EQ |
---|
1630 | cut (bv_no_pc res) |
---|
1631 | [ -prf1 -prf2 |
---|
1632 | cases bv1 in bv1_no_pc EQ; |
---|
1633 | [|| #ptr11 #ptr12 #p1 | #by1 | #p1 | #ptr1 #p1 | #pc1 #p1 ] * |
---|
1634 | cases bv2 in bv2_no_pc; |
---|
1635 | [3,10,17,24,31,38: #ptr21 #ptr22 #p2 |
---|
1636 | |4,11,18,25,32,39: #by2 |
---|
1637 | |5,12,19,26,33,40: #p2 |
---|
1638 | |6,13,20,27,34,41: #ptr2 #p2 |
---|
1639 | |7,14,21,28,35,42: #pc2 #p2 |
---|
1640 | ] * |
---|
1641 | cases op |
---|
1642 | whd in match be_op2; whd in ⊢ (???%→?); |
---|
1643 | normalize nodelta |
---|
1644 | #EQ destruct(EQ) try % |
---|
1645 | try (whd in EQ : (??%?); destruct(EQ) %) |
---|
1646 | lapply EQ -EQ |
---|
1647 | [ @if_elim #_ [ @if_elim #_ ] whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
1648 | |2,12,13,16,18: @if_elim #_ whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
1649 | |3,4,5,6,7,8: #H @('bind_inversion H) #bit #EQ |
---|
1650 | cases (op2 eval bit ???) #res' #bit' |
---|
1651 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
1652 | |17: cases (ptype ptr1) normalize nodelta |
---|
1653 | [ @if_elim #_ |
---|
1654 | [ #H @('bind_inversion H) #bit #EQbit |
---|
1655 | cases (op2 eval bit ???) #res' #bit' |
---|
1656 | ] |
---|
1657 | ] |
---|
1658 | whd in ⊢ (??%%→?); #EQ destruct(EQ) % |
---|
1659 | |*: whd in ⊢ (??%?→?); |
---|
1660 | cases (ptype ?) normalize nodelta |
---|
1661 | try (#EQ destruct(EQ) @I) |
---|
1662 | cases (part_no ?) normalize nodelta |
---|
1663 | try (#n lapply (refl ℕ n) #_) |
---|
1664 | try (#EQ destruct(EQ) @I) |
---|
1665 | try (#H @('bind_inversion H) -H * #EQbit |
---|
1666 | whd in ⊢ (??%%→?);) |
---|
1667 | try (#EQ destruct(EQ) @I) |
---|
1668 | [1,2,4,6,7: cases (op2 eval ????) #res' #bit' whd in ⊢ (??%%→?); |
---|
1669 | #EQ destruct(EQ) @I |
---|
1670 | |*: cases carry normalize nodelta |
---|
1671 | try (#b lapply (refl bool b) #_) |
---|
1672 | try (#ptr lapply (refl pointer ptr) #_ #p #o) |
---|
1673 | try (#EQ destruct(EQ) @I) |
---|
1674 | @if_elim #_ |
---|
1675 | try (#EQ destruct(EQ) @I) |
---|
1676 | @If_elim #prf |
---|
1677 | try (#EQ destruct(EQ) @I) |
---|
1678 | cases (op2_bytes ?????) |
---|
1679 | #res' #bit' whd in ⊢ (??%%→?); |
---|
1680 | #EQ destruct(EQ) @I |
---|
1681 | ] |
---|
1682 | ] |
---|
1683 | ] #res_no_pc |
---|
1684 | %{(bv_no_pc_wf … res_no_pc)} |
---|
1685 | >(sigma_bv_no_pc … bv1_no_pc) |
---|
1686 | >(sigma_bv_no_pc … bv2_no_pc) |
---|
1687 | >(sigma_bv_no_pc … res_no_pc) |
---|
1688 | assumption |
---|
1689 | qed. |
---|
1690 | |
---|
1691 | definition combine_strong : |
---|
1692 | ∀A,B,C,D : Type[0]. |
---|
1693 | ∀P : A → Prop.∀Q : C → Prop. |
---|
1694 | (∀x.P x → B) → (∀x.Q x → D) → |
---|
1695 | (∀pr.(P (\fst pr) ∧ Q (\snd pr)) → B × D) ≝ |
---|
1696 | λA,B,C,D,P,Q,f,g,pr,prf.〈f ? (proj1 … prf), g ? (proj2 … prf)〉. |
---|
1697 | |
---|
1698 | lemma wf_set_regs : ∀p,p',graph_prog,sigma,gss,st,r. |
---|
1699 | well_formed_state p p' graph_prog sigma gss st → |
---|
1700 | well_formed_regs … gss r → |
---|
1701 | well_formed_state … gss (set_regs … r st). |
---|
1702 | #p #p' #graph_prog #sigma #gss #st #r |
---|
1703 | *** #H1 #H2 #_ #H4 #H3 |
---|
1704 | %{H4} %{H3} %{H2} @H1 |
---|
1705 | qed. |
---|
1706 | |
---|
1707 | lemma wf_set_is : ∀p,p',graph_prog,sigma,gss,st,is. |
---|
1708 | well_formed_state p p' graph_prog sigma gss st → |
---|
1709 | sigma_is_opt p p' graph_prog sigma is ≠ None ? → |
---|
1710 | well_formed_state … gss (set_istack … is st). |
---|
1711 | #p #p' #graph_prog #sigma #gss #st #is |
---|
1712 | *** #H1 #H2 #H3 #H4 #H5 |
---|
1713 | %{H4} %{H3} %{H5} @H1 |
---|
1714 | qed. |
---|
1715 | |
---|
1716 | lemma wf_set_m : ∀p,p',graph_prog,sigma,gss,st,m. |
---|
1717 | well_formed_state p p' graph_prog sigma gss st → |
---|
1718 | well_formed_mem p p' graph_prog sigma m → |
---|
1719 | well_formed_state … gss (set_m … m st). |
---|
1720 | #p #p' #graph_prog #sigma #gss #st #m |
---|
1721 | *** #H1 #H2 #H3 #H4 #H5 |
---|
1722 | %{H5} %{H3} %{H2} @H1 |
---|
1723 | qed. |
---|
1724 | |
---|
1725 | lemma opt_to_res_preserve : ∀X,Y,P,F,m,n,e1,e2. |
---|
1726 | opt_preserve X Y P F m n → |
---|
1727 | res_preserve X Y P F (opt_to_res … e1 m) (opt_to_res … e2 n). |
---|
1728 | #X #Y #P #F #m #n #e1 #e2 #H #v #prf |
---|
1729 | cases (H … (opt_eq_from_res ???? prf)) #prf' #EQ %{prf'} |
---|
1730 | >EQ % |
---|
1731 | qed. |
---|
1732 | |
---|
1733 | lemma err_eq_from_io : ∀O,I,X,m,v. |
---|
1734 | err_to_io O I X m = return v → m = return v. |
---|
1735 | #O #I #X * #x #v normalize #EQ destruct % qed. |
---|
1736 | |
---|
1737 | lemma res_to_io_preserve : ∀O,I,X,Y,P,F,m,n. |
---|
1738 | res_preserve X Y P F m n → |
---|
1739 | io_preserve O I X Y P F m n. |
---|
1740 | #O #I #X #Y #P #F #m #n #H #v #prf |
---|
1741 | cases (H … (err_eq_from_io ????? prf)) #prf' #EQ %{prf'} |
---|
1742 | >EQ % |
---|
1743 | qed. |
---|
1744 | |
---|
1745 | lemma eval_seq_no_pc_sigma_commute : |
---|
1746 | ∀p,p',graph_prog. |
---|
1747 | let lin_prog ≝ linearise p graph_prog in |
---|
1748 | ∀stack_sizes. |
---|
1749 | ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. |
---|
1750 | ∀f,fn,stmt. |
---|
1751 | preserving … res_preserve … |
---|
1752 | (sigma_state … gss) |
---|
1753 | (sigma_state … gss) |
---|
1754 | (eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) |
---|
1755 | f fn stmt) |
---|
1756 | (eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes)) |
---|
1757 | f (\fst (linearise_int_fun … fn)) stmt). |
---|
1758 | #p #p' #graph_prog #stack_sizes #sigma #gss #f |
---|
1759 | #fn #stmt |
---|
1760 | whd in match eval_seq_no_pc; |
---|
1761 | cases stmt normalize nodelta |
---|
1762 | [1,2: (* COMMENT, COST_LABEL *) #_ @mfr_return |
---|
1763 | | (* MOVE *) #mv_sig #st #prf' |
---|
1764 | @(mfr_bind … (sigma_regs … gss)) |
---|
1765 | [ @pair_reg_move_commute |
---|
1766 | | #r #prf @mfr_return @wf_set_regs assumption |
---|
1767 | ] |
---|
1768 | | (* POP *) |
---|
1769 | #a #st #prf |
---|
1770 | @(mfr_bind … (combine_strong … (sigma_beval p p' graph_prog sigma) (sigma_state … gss))) |
---|
1771 | [ @(mfr_bind … (sigma_is_pop_commute …)) * #bv #is' * #prf1' #prf2' |
---|
1772 | @mfr_return %{prf1'} @wf_set_is assumption |
---|
1773 | | * #bv #st' * #prf1' #prf2' |
---|
1774 | @mfr_bind [3: @acca_store__commute |*:] |
---|
1775 | #r #prf3' @mfr_return @wf_set_regs assumption |
---|
1776 | ] |
---|
1777 | | (* PUSH *) |
---|
1778 | #a #st #prf |
---|
1779 | @(mfr_bind … (sigma_beval p p' graph_prog sigma)) |
---|
1780 | [ @acca_arg_retrieve_commute |
---|
1781 | | #bv #prf_bv |
---|
1782 | @(mfr_bind … (sigma_is p p' graph_prog sigma)) |
---|
1783 | [ @is_push_sigma_commute |
---|
1784 | | #is #prf_is @mfr_return @wf_set_is assumption |
---|
1785 | ] |
---|
1786 | ] |
---|
1787 | | (*C_ADDRESS*) |
---|
1788 | #sy |
---|
1789 | change with ((member ? ? ? (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog)) → ?) |
---|
1790 | #sy_prf |
---|
1791 | change with ((dpl_reg p) → ?) #dpl |
---|
1792 | change with ((dph_reg p) → ?) #dph |
---|
1793 | #st #prf |
---|
1794 | @(mfr_bind … (sigma_state … gss)) |
---|
1795 | [ @(mfr_bind … (sigma_regs … gss)) |
---|
1796 | [2: #r #prf' @mfr_return @wf_set_regs assumption ] |
---|
1797 | ] |
---|
1798 | @opt_safe_elim #bl #EQbl |
---|
1799 | @opt_safe_elim #bl' |
---|
1800 | >(find_symbol_transf … |
---|
1801 | (λvars.transf_fundef … (λfn.\fst (linearise_int_fun … fn))) graph_prog sy) in ⊢ (%→?); |
---|
1802 | >EQbl in ⊢ (%→?); #EQ destruct(EQ) |
---|
1803 | [ @dpl_store_commute |
---|
1804 | | #st' #st_prf' |
---|
1805 | @mfr_bind [3: @dph_store_commute |*:] |
---|
1806 | [2: #r #prf' @mfr_return @wf_set_regs assumption |
---|
1807 | ] |
---|
1808 | ] @bv_no_pc_wf % |
---|
1809 | | (*C_OPACCS*) |
---|
1810 | #op #a #b #arg1 #arg2 #st #prf |
---|
1811 | @(mfr_bind … (sigma_beval p p' graph_prog sigma)) |
---|
1812 | [ @acca_arg_retrieve_commute ] |
---|
1813 | #bv1 #bv1_prf |
---|
1814 | @(mfr_bind … (sigma_beval p p' graph_prog sigma)) |
---|
1815 | [ @accb_arg_retrieve_commute ] |
---|
1816 | #bv2 #bv2_prf |
---|
1817 | @(mfr_bind … (combine_strong … |
---|
1818 | (sigma_beval p p' graph_prog sigma) |
---|
1819 | (sigma_beval p p' graph_prog sigma))) |
---|
1820 | [ @beopaccs_sigma_commute ] |
---|
1821 | * #res1 #res2 * #res1_prf #res2_prf |
---|
1822 | @(mfr_bind … (sigma_state … gss)) |
---|
1823 | [ @mfr_bind [3: @acca_store__commute |*: ] |
---|
1824 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
1825 | ] |
---|
1826 | #st' #st_prf' |
---|
1827 | @mfr_bind [3: @accb_store_commute |*: ] |
---|
1828 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
1829 | | (*C_OP1*) |
---|
1830 | #op #a #arg #st #prf |
---|
1831 | @(mfr_bind … (sigma_beval p p' graph_prog sigma)) |
---|
1832 | [ @acca_retrieve_commute ] |
---|
1833 | #bv #bv_prf |
---|
1834 | @(mfr_bind … (sigma_beval p p' graph_prog sigma)) |
---|
1835 | [ @beop1_sigma_commute ] |
---|
1836 | #res #res_prf |
---|
1837 | @mfr_bind [3: @acca_store__commute |*: ] |
---|
1838 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
1839 | | (*C_OP2*) |
---|
1840 | #op #a #arg1 #arg2 #st #prf |
---|
1841 | @(mfr_bind … (sigma_beval p p' graph_prog sigma)) |
---|
1842 | [ @acca_arg_retrieve_commute ] |
---|
1843 | #bv1 #bv1_prf |
---|
1844 | @(mfr_bind … (sigma_beval p p' graph_prog sigma)) |
---|
1845 | [ @snd_arg_retrieve_commute ] |
---|
1846 | #bv2 #bv2_prf |
---|
1847 | @mfr_bind |
---|
1848 | [3: @beop2_sigma_commute |*: ] |
---|
1849 | * #res1 #carry' #res1_prf |
---|
1850 | @(mfr_bind … (sigma_state … gss)) |
---|
1851 | [ @mfr_bind [3: @acca_store__commute |*: ] |
---|
1852 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
1853 | ] |
---|
1854 | #st' #st_prf' @mfr_return |
---|
1855 | | (*C_CLEAR_CARRY*) |
---|
1856 | #st #prf @mfr_return |
---|
1857 | | (*C_SET_CARRY*) |
---|
1858 | #st #prf @mfr_return |
---|
1859 | | (*C_LOAD*) |
---|
1860 | #a #dpl #dph #st #prf |
---|
1861 | @mfr_bind [3: @dph_arg_retrieve_commute |*:] |
---|
1862 | #bv1 #bv1_prf |
---|
1863 | @mfr_bind [3: @dpl_arg_retrieve_commute |*:] |
---|
1864 | #bv2 #bv2_prf |
---|
1865 | @mfr_bind [3: @sigma_ptr_commute |*:] |
---|
1866 | [ % assumption ] |
---|
1867 | #ptr * |
---|
1868 | @mfr_bind |
---|
1869 | [3: |
---|
1870 | @opt_to_res_preserve @beloadv_sigma_commute |
---|
1871 | |*:] |
---|
1872 | #res #res_prf |
---|
1873 | @mfr_bind [3: @acca_store__commute |*: ] |
---|
1874 | #r #r_prf @mfr_return @wf_set_regs assumption |
---|
1875 | | (*C_STORE*) |
---|
1876 | #dpl #dph #a #st #prf |
---|
1877 | @mfr_bind [3: @dph_arg_retrieve_commute |*:] |
---|
1878 | #bv1 #bv1_prf |
---|
1879 | @mfr_bind [3: @dpl_arg_retrieve_commute |*:] |
---|
1880 | #bv2 #bv2_prf |
---|
1881 | @mfr_bind [3: @sigma_ptr_commute |*:] |
---|
1882 | [ % assumption ] |
---|
1883 | #ptr * |
---|
1884 | @mfr_bind |
---|
1885 | [3: @acca_arg_retrieve_commute |*:] |
---|
1886 | #res #res_prf |
---|
1887 | @mfr_bind |
---|
1888 | [3: |
---|
1889 | @opt_to_res_preserve @bestorev_sigma_commute |
---|
1890 | |*:] |
---|
1891 | #mem #wf_mem |
---|
1892 | @mfr_return |
---|
1893 | @wf_set_m assumption |
---|
1894 | | (*CALL*) |
---|
1895 | #f #args #dest #st #prf @mfr_return |
---|
1896 | | (*C_EXT*) |
---|
1897 | #s_ext #st #prf @eval_ext_seq_commute |
---|
1898 | ] |
---|
1899 | qed. |
---|
1900 | |
---|
1901 | inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ |
---|
1902 | ex1_intro: ∀ x:A. P x → ex_Type1 A P. |
---|
1903 | (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) |
---|
1904 | |
---|
1905 | lemma linearise_ok: |
---|
1906 | ∀p,p',graph_prog. |
---|
1907 | let lin_prog ≝ linearise ? graph_prog in |
---|
1908 | ∀stack_sizes. |
---|
1909 | (∀sigma.good_state_sigma p p' graph_prog sigma) → |
---|
1910 | ex_Type1 … (λR. |
---|
1911 | status_simulation |
---|
1912 | (graph_abstract_status p p' graph_prog stack_sizes) |
---|
1913 | (lin_abstract_status p p' lin_prog stack_sizes) R). |
---|
1914 | #p #p' #graph_prog |
---|
1915 | letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog) |
---|
1916 | cut (∀fn.good_local_sigma … (sigma fn)) |
---|
1917 | [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:] |
---|
1918 | #good |
---|
1919 | #stack_sizes |
---|
1920 | #gss lapply (gss sigma) -gss #gss |
---|
1921 | %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)} |
---|
1922 | whd in match graph_abstract_status; |
---|
1923 | whd in match lin_abstract_status; |
---|
1924 | whd in match graph_prog_params; |
---|
1925 | whd in match lin_prog_params; |
---|
1926 | normalize nodelta |
---|
1927 | whd |
---|
1928 | whd in ⊢ (%→%→%→?); |
---|
1929 | whd in ⊢ (?(?%)→?(?%)→?(?%)→?); |
---|
1930 | whd in ⊢ (?%→?%→?%→?); |
---|
1931 | #st1 #st1' #st2 |
---|
1932 | whd in ⊢ (%→?); |
---|
1933 | change with |
---|
1934 | (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?) |
---|
1935 | whd in match eval_state in ⊢ (%→?); normalize nodelta |
---|
1936 | @'bind_inversion |
---|
1937 | ** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch_stmt |
---|
1938 | cases (fetch_statement_inv … EQfetch_stmt) #EQfetchfn #_ |
---|
1939 | @'bind_inversion |
---|
1940 | #st1_no_pc' #ex lapply (err_eq_from_io ????? ex) -ex #ex #ex_advance |
---|
1941 | * #wf_prf #st2_EQ |
---|
1942 | |
---|
1943 | cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt) |
---|
1944 | cases stmt in EQfetch_stmt ex ex_advance; -stmt |
---|
1945 | [ @cond_call_other |
---|
1946 | [ #a #ltrue | #f #args #dest | #s #s_no_call ] #nxt | #s | * ] |
---|
1947 | normalize nodelta |
---|
1948 | #EQfetch_stmt |
---|
1949 | whd in match eval_statement_no_pc in ⊢ (%→?); normalize nodelta |
---|
1950 | #ex |
---|
1951 | [| whd in match eval_statement_advance in ⊢ (%→?); |
---|
1952 | whd in match eval_seq_advance in ⊢ (%→?); |
---|
1953 | normalize nodelta |
---|
1954 | | whd in match eval_statement_advance in ⊢ (%→?); |
---|
1955 | normalize nodelta |
---|
1956 | >(no_call_advance (mk_prog_params (make_sem_graph_params p p') |
---|
1957 | graph_prog stack_sizes)) in ⊢ (%→?); try assumption |
---|
1958 | ] |
---|
1959 | #ex_advance |
---|
1960 | #all_labels_in |
---|
1961 | letin lin_prog ≝ (linearise … graph_prog) |
---|
1962 | lapply (refl … (eval_state … (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2)) |
---|
1963 | whd in match eval_state in ⊢ (???%→?); |
---|
1964 | >st2_EQ in ⊢ (???%→?); normalize nodelta |
---|
1965 | [ (* COND *) |
---|
1966 | | (* CALL *) |
---|
1967 | | (* SEQ *) |
---|
1968 | #ex' |
---|
1969 | * #lin_fetch_stmt #next_spec |
---|
1970 | whd in match (as_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
1971 | >EQfetch_stmt in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
1972 | normalize nodelta |
---|
1973 | whd in match joint_classify_step; |
---|
1974 | normalize nodelta |
---|
1975 | >no_call_other in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
1976 | try assumption |
---|
1977 | normalize nodelta |
---|
1978 | >lin_fetch_stmt in ex' : (???%) ⊢ ?; >m_return_bind in ⊢ (???%→?); |
---|
1979 | whd in match eval_statement_no_pc in ⊢ (???%→?); |
---|
1980 | normalize nodelta |
---|
1981 | cases (eval_seq_no_pc_sigma_commute … gss … ex) in ⊢ ?; |
---|
1982 | [2: @hide_prf @(proj2 … wf_prf) ] |
---|
1983 | #st1_no_pc_wf #EQ >EQ in ⊢ (???%→?); -EQ |
---|
1984 | >m_return_bind in ⊢ (???%→?); |
---|
1985 | whd in match eval_statement_advance in ⊢ (%→?); |
---|
1986 | normalize nodelta |
---|
1987 | >(no_call_advance (mk_prog_params (make_sem_lin_params p p') |
---|
1988 | lin_prog stack_sizes)) in ⊢ (%→?); try assumption |
---|
1989 | whd in match (next ???) in ⊢ (%→?); |
---|
1990 | change with (sigma_pc ????? (hide_prf ??)) in match (pc ??) in ⊢ (%→?); |
---|
1991 | #ex' |
---|
1992 | cases next_spec |
---|
1993 | #succ_pc_nxt_wf * |
---|
1994 | [ #succ_pc_commute >succ_pc_commute in ex' ⊢ ?; |
---|
1995 | #ex' |
---|
1996 | % [2: %{(taaf_step … (taa_base …) …)} [2: @ex' ] |*:] |
---|
1997 | whd |
---|
1998 | [ whd in ⊢ (??%?); |
---|
1999 | >lin_fetch_stmt normalize nodelta |
---|
2000 | whd in match joint_classify_step; normalize nodelta |
---|
2001 | @no_call_other assumption |
---|
2002 | | normalize nodelta |
---|
2003 | cut (? : Prop) |
---|
2004 | [3: #H % [ % [ % | @H ]] |*:] |
---|
2005 | [ (* TODO lemma : sem_rel → label_rel *) |
---|
2006 | cases daemon |
---|
2007 | | whd in ex_advance : (??%%); destruct(ex_advance) |
---|
2008 | % [ % assumption | % ] |
---|
2009 | ] |
---|
2010 | ] |
---|
2011 | | #fetch_GOTO |
---|
2012 | cases (all_labels_in) #wf_next #_ |
---|
2013 | cases (pc_of_label_sigma_commute … p' … good … EQfetchfn ?) |
---|
2014 | [2: @nxt |3: cases daemon ] |
---|
2015 | #wf_next' #EQ |
---|
2016 | % [2: %{(taaf_step … (taa_step … (taa_base …) …) …)} |
---|
2017 | [3: @ex' |
---|
2018 | |2: whd |
---|
2019 | whd in match eval_state; normalize nodelta |
---|
2020 | >fetch_GOTO in ⊢ (??%?); >m_return_bind in ⊢ (??%?); |
---|
2021 | >m_return_bind in ⊢ (??%?); |
---|
2022 | whd in match eval_statement_advance; normalize nodelta |
---|
2023 | whd in match goto; normalize nodelta |
---|
2024 | whd in match (pc_block ?); |
---|
2025 | >sigma_pblock_eq_lemma >EQ in ⊢ (??%?); % |
---|
2026 | |7: normalize nodelta |
---|
2027 | cut (? : Prop) |
---|
2028 | [3: #H % [ % [ % | @H ]] |*:] |
---|
2029 | [ (* TODO lemma : sem_rel → label_rel *) |
---|
2030 | cases daemon |
---|
2031 | | whd in ex_advance : (??%%); destruct(ex_advance) |
---|
2032 | % [ % assumption | % ] |
---|
2033 | ] |
---|
2034 | |5: % * #H @H -H whd in ⊢ (??%?); >fetch_GOTO % |
---|
2035 | |4: whd whd in ⊢ (??%?); |
---|
2036 | >lin_fetch_stmt normalize nodelta |
---|
2037 | whd in match joint_classify_step; normalize nodelta |
---|
2038 | @no_call_other assumption |
---|
2039 | |1: whd whd in ⊢ (??%?); |
---|
2040 | >fetch_GOTO normalize nodelta % |
---|
2041 | |*: |
---|
2042 | ] |
---|
2043 | |*: |
---|
2044 | ] |
---|
2045 | ] |
---|
2046 | | (* FIN *) |
---|
2047 | ] |
---|
2048 | |
---|
2049 | #stmt_spec |
---|
2050 | |
---|
2051 | |
---|
2052 | cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?; |
---|
2053 | #wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?); |
---|
2054 | |
---|
2055 | whd in match (as_classify ??) in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
2056 | >EQfetch_stmt in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
2057 | normalize nodelta |
---|
2058 | |
---|
2059 | normalize nodelta |
---|
2060 | [ whd in match joint_classify_step; @cond_call_other |
---|
2061 | [ (* COND *) #a #lbltrue #nxt |
---|
2062 | #ex whd in match eval_statement_advance in ⊢ (%→%→?); normalize nodelta |
---|
2063 | #H @('bind_inversion (err_eq_from_io ????? H)) -H @bv_pc_other |
---|
2064 | [ #bv_pc #p #bv whd in ⊢ (??%%→?); #ABS destruct(ABS) ] |
---|
2065 | #bv #bv_no_pc #EQretrieve |
---|
2066 | cases (retrieve_commute … (acca_retrieve_commute … gss) … wf_st1_no_pc_prf … EQretrieve) |
---|
2067 | #ignore >(sigma_bv_no_pc … bv_no_pc) |
---|
2068 | change with (acca_retrieve ?? (make_sem_lin_params p p') ?? = ? → ?) |
---|
2069 | #EQretrieve' >EQretrieve' in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); |
---|
2070 | #H @('bind_inversion H) -H * normalize nodelta #EQbool_of_bv |
---|
2071 | >EQbool_of_bv in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); normalize nodelta |
---|
2072 | [ whd in match goto; normalize nodelta |
---|
2073 | >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→?); |
---|
2074 | #EQ destruct(EQ) #ex_advance #ex_advance' |
---|
2075 | % [2: %{(tal_base_not_return …)} [3: @ex_advance' |
---|
2076 | | (* CALL *) #f #args #dest #nxt |
---|
2077 | | (* other *) #stmt #no_call #nxt |
---|
2078 | ] normalize nodelta |
---|
2079 | [ #ex |
---|
2080 | #ex_advance #ex_advance' |
---|
2081 | | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
2082 | #H @('bind_inversion H) -H #called_block |
---|
2083 | #H lapply (err_eq_from_io ????? H) -H #EQcalled_block |
---|
2084 | #H @('bind_inversion H) -H * #called * #called_fn |
---|
2085 | #H lapply (err_eq_from_io ????? H) -H #EQcalled |
---|
2086 | normalize nodelta |
---|
2087 | [ #H lapply (err_eq_from_io ????? H) -H ] |
---|
2088 | #H @('bind_inversion H) -H |
---|
2089 | | @('bind_inversion H) ] -H #st1_no_pc'' #save_frame_EQ ] |
---|
2090 | #ex_advance #ex_advance' |
---|
2091 | whd in match joint_classify_seq; normalize nodelta |
---|
2092 | >EQcalled_block in ⊢ (?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); |
---|
2093 | |
---|
2094 | cut (∀p,p',graph_prog,sigma,gss,st,f,bl. |
---|
2095 | ∀prf : well_formed_state p p' graph_prog sigma gss st. |
---|
2096 | block_of_call (make_sem_graph_params p p') ? |
---|
2097 | (globalenv_noinit ? graph_prog) st f = return bl → |
---|
2098 | block_of_call (make_sem_lin_params p p') ? |
---|
2099 | (globalenv_noinit ? (linearise … graph_prog)) |
---|
2100 | (sigma_state … st prf) f = return bl) |
---|
2101 | [1,3: (*TODO lemma *) cases daemon ] #block_of_call_sigma_commute |
---|
2102 | whd in match eval_seq_advance; normalize nodelta |
---|
2103 | >(block_of_call_sigma_commute … EQcalled_block) in ⊢ (???%→?); |
---|
2104 | >m_return_bind in ⊢ (???%→?); |
---|
2105 | >(fetch_function_transf … EQcalled : |
---|
2106 | fetch_function … (globalenv_noinit … lin_prog) called_block = ?) in ⊢ (???%→?); |
---|
2107 | >m_return_bind in ⊢ (???%→?); |
---|
2108 | whd in match (transf_fundef); normalize nodelta |
---|
2109 | |
---|
2110 | |
---|
2111 | #block_of_call_sigma_commute |
---|
2112 | @match_int_fun #called_descr #EQcalled_descr |
---|
2113 | [ #H @('bind_inversion H) -H #st1_frame_saved #EQ_frame_saved ] |
---|
2114 | #ex_advance |
---|
2115 | cut |
---|
2116 | (∀A,B.∀prog : program (λvars.fundef (A vars)) ℕ. |
---|
2117 | ∀trans : ∀vars.A vars → B vars. |
---|
2118 | let prog_out : program (λvars.fundef (B vars)) ℕ ≝ |
---|
2119 | transform_program ??? prog (λvars.transf_fundef … (trans vars)) in |
---|
2120 | ∀i.is_function … (globalenv_noinit … prog) i → |
---|
2121 | is_function … (globalenv_noinit … prog_out) i) [1,3: (* TODO lemma *) cases daemon ] |
---|
2122 | #f_propagate |
---|
2123 | letin sigma_function ≝ (λA,B,prog,trans. |
---|
2124 | λf : Σi.is_function ? (globalenv_noinit ? prog) i. |
---|
2125 | «pi1 ?? f, f_propagate A B prog trans ? (pi2 ?? f)») in ⊢ ?; (* TODO def *) |
---|
2126 | cut (∀p,p',graph_prog. |
---|
2127 | let lin_prog ≝ linearise ? graph_prog in |
---|
2128 | ∀sigma.∀gss : good_state_sigma … graph_prog sigma. |
---|
2129 | ∀f,st,fn. |
---|
2130 | ∀prf : well_formed_state … gss st. |
---|
2131 | function_of_call (make_sem_graph_params p p') … (globalenv_noinit … graph_prog) |
---|
2132 | st f = return fn → |
---|
2133 | function_of_call (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) |
---|
2134 | (sigma_state … gss st prf) f = return sigma_function … fn) |
---|
2135 | [1,3: (* TODO lemma *) cases daemon ] |
---|
2136 | #function_of_call_sigma_commute |
---|
2137 | whd in match joint_classify_step; whd in match joint_classify_seq; |
---|
2138 | normalize nodelta #next_spec |
---|
2139 | >(function_of_call_sigma_commute … EQcalled) in ⊢ (%→?); |
---|
2140 | >m_return_bind in ⊢ (%→?); |
---|
2141 | @match_int_fun |
---|
2142 | [2,3: #EQdescr' lapply EQdescr' |
---|
2143 | >description_of_function_transf in EQdescr'; |
---|
2144 | |
---|
2145 | |
---|
2146 | whd in match sigma_beval; normalize nodelta |
---|
2147 | cases bv |
---|
2148 | [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #bv_pc #p ] |
---|
2149 | whd in match (sigma_beval_opt ?????) in ⊢ (%→%→?); |
---|
2150 | [7: #ignore #_ |
---|
2151 | #ignore whd in match (opt_safe ???) in ⊢ (%→?); #EQretrieve |
---|
2152 | whd in match (bool_of_beval ?) in ⊢ (% → ?); |
---|
2153 | 3: >no_call_advance [2: @no_call] |
---|
2154 | |
---|
2155 | |
---|
2156 | |
---|
2157 | generalize in match wf_pc in ⊢ ?; |
---|
2158 | whd in ⊢ (%→?); |
---|
2159 | inversion (sigma_pc_opt ?????) in ⊢ (%→?); [ #_ * #ABS elim (ABS ?) % ] |
---|
2160 | #lin_pc |
---|
2161 | whd in match (sigma_pc_opt) in ⊢ (%→?); normalize nodelta |
---|
2162 | >EQfunc_of_block in ⊢ (%→?); >m_return_bind in ⊢ (%→?); |
---|
2163 | #H elim (bind_opt_inversion ????? H) in ⊢ ?; -H #lin_pt * |
---|
2164 | #EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) #_ |
---|
2165 | elim (good_local … EQsigma) -good_local |
---|
2166 | #stmt' * |
---|
2167 | change with (stmt_at ?? (joint_if_code ?? graph_fun) ? = ? → ?) |
---|
2168 | >EQstmt_at #EQ lapply (sym_eq ??? EQ) -EQ #EQ destruct(EQ) |
---|
2169 | #H elim (opt_Exists_elim … H) -H * #lbl_opt #lin_stmt normalize nodelta |
---|
2170 | >(prog_if_of_function_transform … fn) in ⊢ (%→?); [2: % ] |
---|
2171 | change with graph_fun in match (if_of_function ?? fn) in ⊢ (%→?); |
---|
2172 | letin lin_fun ≝ (\fst (linearise_int_fun p globals graph_fun)) |
---|
2173 | change with globals in match (prog_var_names ?? graph_prog) in ⊢ (%→?); |
---|
2174 | * |
---|
2175 | #EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec |
---|
2176 | destruct(EQst2) |
---|
2177 | whd in match eval_state in ⊢ (???%→?); normalize nodelta |
---|
2178 | (* resolve classifier *) |
---|
2179 | [ * |
---|
2180 | [ #stmt #nxt |
---|
2181 | whd in match eval_statement in ⊢ (?→%→?); normalize nodelta |
---|
2182 | #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec |
---|
2183 | whd in match (graph_to_lin_statement ???) in ⊢ (%→?); |
---|
2184 | whd in match eval_statement in ⊢ (%→?); normalize nodelta |
---|
2185 | elim (IO_bind_inversion ??????? EQeval) #st1_no_pc * |
---|
2186 | #EQeval_no_pc #EQeval_pc |
---|
2187 | >(eval_seq_no_pc_sigma_commute … EQeval_no_pc) |
---|
2188 | [2: (*TODO lemma eval_seq_no_pc_wf *) @hide_prf cases daemon ] |
---|
2189 | >m_return_bind |
---|
2190 | cases stmt in EQfetch EQeval_no_pc EQeval_pc EQstmt_at EQnth_opt next_spec; |
---|
2191 | [14: #f #args #dest |
---|
2192 | | #c |
---|
2193 | | #lbl |
---|
2194 | | #move_sig |
---|
2195 | | #a |
---|
2196 | | #a |
---|
2197 | | #sy #sy_prf #dpl #dph |
---|
2198 | | #op #a #b #arg1 #arg2 |
---|
2199 | | #op #a #arg |
---|
2200 | | #op #a #arg1 #arg2 |
---|
2201 | || |
---|
2202 | | #a #dpl #dph |
---|
2203 | | #dpl #dph #a |
---|
2204 | | #s_ext |
---|
2205 | ] |
---|
2206 | [ (* CALL *) |
---|
2207 | |(*:*) |
---|
2208 | normalize nodelta |
---|
2209 | #EQfetch #EQeval_no_pc #EQeval_pc #EQstmt_at #EQnth_opt #next_spec |
---|
2210 | whd in match eval_seq_pc; normalize nodelta |
---|
2211 | #ex1 |
---|
2212 | cases next_spec |
---|
2213 | [ #EQnext_sigma |
---|
2214 | %[2: %{(taaf_step … (taa_base …) ex1 ?)} |
---|
2215 | [ cases daemon (* TODO lemma joint_classify_sigma_commute *) ]|] |
---|
2216 | normalize nodelta |
---|
2217 | cut (? : Prop) [3: #R' % [ %{I R'} ] |*:] |
---|
2218 | [ cases daemon (* TODO lemma joint_label_sigma_commute *) |
---|
2219 | | % |
---|
2220 | [ (* TODO lemma well_formed_state_pc_preserve? *) @hide_prf cases daemon |
---|
2221 | | whd in match eval_seq_pc in EQeval_pc; |
---|
2222 | whd in EQeval_pc : (??%%); whd in EQeval_pc : (??(????%)?); |
---|
2223 | destruct (EQeval_pc) |
---|
2224 | whd in ⊢ (??%%); |
---|
2225 | change with (sigma_pc ??????) in match |
---|
2226 | (pc ? (sigma_state_pc ???????)); |
---|
2227 | whd in match (succ_pc ????) in ⊢ (??%%); |
---|
2228 | whd in match (point_of_succ ???) in ⊢ (??%%); |
---|
2229 | >(point_of_pc_sigma_commute … EQfunc_of_block EQsigma) |
---|
2230 | whd in match sigma_pc in ⊢ (???%); |
---|
2231 | whd in match sigma_pc_opt in ⊢ (???%); normalize nodelta |
---|
2232 | @opt_safe_elim #pc' |
---|
2233 | >EQfunc_of_block >m_return_bind |
---|
2234 | whd in match point_of_pc; normalize nodelta |
---|
2235 | >point_of_offset_of_point |
---|
2236 | >EQnext_sigma whd in ⊢ (??%?→?); |
---|
2237 | whd in match pc_of_point; normalize nodelta |
---|
2238 | #EQ destruct(EQ) |
---|
2239 | >sigma_pblock_eq_lemma % |
---|
2240 | ] |
---|
2241 | ] |
---|
2242 | | -next_spec #next_spec |
---|
2243 | % |
---|
2244 | |
---|
2245 | |
---|
2246 | whd in ⊢ (?→???%→?); |
---|
2247 | generalize in ⊢ (??%? → ???(????%) → ?); |*: skip] | #a #lbltrue #next |
---|
2248 | ] #next change with label in next; |
---|
2249 | | * |
---|
2250 | [ #lbl |
---|
2251 | | |
---|
2252 | | #fl #f #args |
---|
2253 | ] |
---|
2254 | ] |
---|
2255 | whd in match eval_statement in ⊢ (?→%→?); normalize nodelta |
---|
2256 | #EQfetch #EQeval #EQstmt_at #EQnth_opt #next_spec |
---|
2257 | normalize nodelta |
---|
2258 | whd in match (graph_to_lin_statement ???) in ⊢ (%→?); |
---|
2259 | whd in match eval_statement in ⊢ (%→?); normalize nodelta |
---|
2260 | [ >m_return_bind in ⊢ (%→?); |
---|
2261 | >m_return_bind in EQeval; |
---|
2262 | |
---|
2263 | |
---|
2264 | |
---|
2265 | (* common for all non-call seq *) |
---|
2266 | >m_return_bind in ⊢ (%→?); |
---|
2267 | whd in ⊢ (??%%→?); #EQ destruct(EQ) |
---|
2268 | >m_return_bind in ⊢ (%→?); |
---|
2269 | |
---|
2270 | |
---|
2271 | #ex1 |
---|
2272 | lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2)) |
---|
2273 | |
---|
2274 | whd in match (point_of_pc ???); |
---|
2275 | whd in match (point_of_succ ???); |
---|
2276 | whd in match sigma_pc in ⊢ (???%); normalize nodelta @opt_safe_elim |
---|
2277 | #pc' #H |
---|
2278 | elim (bind_opt_inversion ????? H) #fn * #EQbl |
---|
2279 | -H #H |
---|
2280 | elim (bind_opt_inversion ????? H) -H #n * #EQsigma whd in ⊢ (??%?→?); |
---|
2281 | #EQ destruct(EQ) |
---|
2282 | whd in match (succ_pc ????); |
---|
2283 | whd in match (point_of_succ ???); |
---|
2284 | change with (point_of_offset ???) in match (point_of_pc ???); |
---|
2285 | >point_of_offset_of_point |
---|
2286 | whd in match sigma_pc; normalize nodelta @opt_safe_elim |
---|
2287 | #pc' whd in match sigma_pc_opt; normalize nodelta |
---|
2288 | |
---|
2289 | |
---|
2290 | |
---|
2291 | whd in match (succ_pc ????); |
---|
2292 | |
---|
2293 | change with next in match (offset_of_point ???) in ⊢ (???%); |
---|
2294 | whd in fetch_statement_spec : (??()%); |
---|
2295 | cases cl in classified_st1_cl; -cl #classified_st1_cl whd |
---|
2296 | [4: |
---|
2297 | >rel_st1_st2 -st2 letin lin_prog ≝ (linearise ? graph_prog) |
---|
2298 | cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ] |
---|
2299 | #sigma_entry_is_zero #sigma_spec |
---|
2300 | lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1))) |
---|
2301 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) |2: skip ] |
---|
2302 | -sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec |
---|
2303 | cases (opt_Exists_elim … sigma_spec) in ⊢ ?; |
---|
2304 | * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved |
---|
2305 | #related_lin_stm_graph_stm |
---|
2306 | |
---|
2307 | inversion (stmt_implicit_label ???) |
---|
2308 | [ whd in match (opt_All ???); #stmt_implicit_spec #_ |
---|
2309 | letin st2_opt' ≝ (eval_state … |
---|
2310 | (ev_genv (lin_prog_params … lin_prog lin_stack_sizes)) |
---|
2311 | (sigma_state_pc … wf_st1)) |
---|
2312 | cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2') |
---|
2313 | [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' |
---|
2314 | normalize nodelta in st2_spec'; -st2_opt' |
---|
2315 | %{st2'} %{(taaf_step … (taa_base …) …)} |
---|
2316 | [ cases daemon (* TODO, together with the previous one? *) |
---|
2317 | | @st2_spec' ] |
---|
2318 | %[%] [%] |
---|
2319 | [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec'; |
---|
2320 | >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec'; |
---|
2321 | >m_return_bind |
---|
2322 | (* Case analysis over the possible statements *) |
---|
2323 | inversion graph_stmt in stmt_implicit_spec; normalize nodelta |
---|
2324 | [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ] |
---|
2325 | XXXXXXXXXX siamo qua, caso GOTO e RETURN |
---|
2326 | | cases daemon (* TODO, after the definition of label_rel, trivial *) ] |
---|
2327 | ] |
---|
2328 | | .... |
---|
2329 | qed. |
---|
2330 | |
---|
2331 | |
---|
2332 | |
---|
2333 | |
---|
2334 | |
---|
2335 | [ * |
---|
2336 | [ * |
---|
2337 | [ letin C_COMMENT ≝ 0 in ⊢ ?; #c |
---|
2338 | | letin C_COST_LABEL ≝ 0 in ⊢ ?; #lbl |
---|
2339 | | letin C_MOVE ≝ 0 in ⊢ ?; #move_sig |
---|
2340 | | letin C_POP ≝ 0 in ⊢ ?; #a |
---|
2341 | | letin C_PUSH ≝ 0 in ⊢ ?; #a |
---|
2342 | | letin C_ADDRESS ≝ 0 in ⊢ ?; #sy #sy_prf #dpl #dph |
---|
2343 | | letin C_OPACCS ≝ 0 in ⊢ ?; #op #a #b #arg1 #arg2 |
---|
2344 | | letin C_OP1 ≝ 0 in ⊢ ?; #op #a #arg |
---|
2345 | | letin C_OP2 ≝ 0 in ⊢ ?; #op #a #arg1 #arg2 |
---|
2346 | | letin C_CLEAR_CARRY ≝ 0 in ⊢ ?; |
---|
2347 | | letin C_SET_CARRY ≝ 0 in ⊢ ?; |
---|
2348 | | letin C_LOAD ≝ 0 in ⊢ ?; #a #dpl #dph |
---|
2349 | | letin C_STORE ≝ 0 in ⊢ ?; #dpl #dph #a |
---|
2350 | | letin C_CALL ≝ 0 in ⊢ ?; #f #args #dest |
---|
2351 | | letin C_EXT ≝ 0 in ⊢ ?; #s_ext |
---|
2352 | ] |
---|
2353 | | letin C_COND ≝ 0 in ⊢ ?; #a #lbltrue |
---|
2354 | ] #next change with label in next; |
---|
2355 | | * |
---|
2356 | [ letin C_GOTO ≝ 0 in ⊢ ?; #lbl |
---|
2357 | | letin C_RETURN ≝ 0 in ⊢ ?; |
---|
2358 | | letin C_TAILCALL ≝ 0 in ⊢ ?; #fl #f #args |
---|
2359 | ] |
---|
2360 | ] |
---|