Changeset 2476
 Timestamp:
 Nov 19, 2012, 6:04:24 PM (9 years ago)
 Location:
 src
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/common/extraGlobalenvs.ma
r2474 r2476 193 193 Σi.is_internal_function_of_program ?? prog i ≝ 194 194 λA,B,init,prog,f.«f, is_internal_function_of_program_ok … (pi2 … f)». 195 196 coercion if_in_prog_from_if_in_global_env nocomposites :197 ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.198 ∀f:Σi.is_internal_function ? (globalenv ?? init prog) i.199 Σi.is_internal_function_of_program ?? prog i ≝200 if_in_global_env_to_if_in_prog201 on _f : Sig ident (λi.is_internal_function ?? i)202 to Sig ident (λi.is_internal_function_of_program ??? i).203 195 204 196 lemma if_propagate : 
src/joint/lineariseProof.ma
r2467 r2476 18 18 include "joint/semanticsUtils.ma". 19 19 20 definition good_local_sigma : 21 ∀p:unserialized_params. 22 ∀p':(∀F.sem_unserialized_params p F). 23 ∀globals. 24 joint_closed_internal_function (mk_graph_params p) globals → 25 (label → option ℕ) → Prop ≝ 26 λp,p',globals,graph_fun,sigma. 27 let lin_fun ≝ linearise_int_fun … graph_fun in 28 let g ≝ joint_if_code ?? (pi1 … graph_fun) in 29 let c ≝ joint_if_code ?? (pi1 … lin_fun) in 30 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). 31 code_closed … c ∧ 32 sigma entry = Some ? 0 ∧ 33 ∀l,n.sigma l = Some ? n → 34 lt n 2^offset_size → 35 ∃s. lookup … g l = Some ? s ∧ 36 opt_Exists ? 37 (λls.let 〈lopt, ts〉 ≝ ls in 38 opt_All ? (eq ? l) lopt ∧ 39 ts = graph_to_lin_statement … s ∧ 40 opt_All ? 41 (λnext.Or (sigma next = Some ? (S n)) 42 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 43 (stmt_implicit_label … s)) (nth_opt … n c). 44 45 axiom prog_if_of_function : 46 ∀p.∀prog : joint_program p. 47 (Σi.is_internal_function_of_program … prog i) → 48 joint_closed_internal_function p (prog_var_names … prog). 49 50 definition if_in_global_env_to_if_in_prog : 51 ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i. 52 Σi.is_internal_function_of_program ? (prog prog_pars) i ≝ 53 λprog_pars,f.pi1 ?? f. 54 @is_internal_function_of_program_ok @(pi2 … f) qed. 55 20 21 lemma ok_is_internal_function_of_program_noinit : 22 ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.∀i. 23 is_internal_function_of_program … prog i → 24 is_internal_function ? (globalenv_noinit ? prog) i ≝ 25 λA,prog.ok_is_internal_function_of_program … prog. 26 27 lemma is_internal_function_of_program_ok_noinit : 28 ∀A.∀prog:program (λvars.fundef (A vars)) ℕ.∀i. 29 is_internal_function ? (globalenv_noinit ? prog) i → 30 is_internal_function_of_program … prog i ≝ 31 λA,prog.is_internal_function_of_program_ok … prog. 32 33 definition if_in_global_env_to_if_in_prog_noinit : 34 ∀A.∀prog:program (λvars.fundef (A vars)) ℕ. 35 (Σi.is_internal_function ? (globalenv_noinit ? prog) i) → 36 Σi.is_internal_function_of_program ?? prog i ≝ 37 λA,prog,f.«f, is_internal_function_of_program_ok_noinit … (pi2 … f)». 38 39 (* 56 40 coercion if_in_prog_from_if_in_global_env nocomposites : 57 ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i. 58 Σi.is_internal_function_of_program ? (prog prog_pars) i ≝ 59 if_in_global_env_to_if_in_prog 60 on _f : Sig ident (λi.is_internal_function ??? i) 61 to Sig ident (λi.is_internal_function_of_program ?? i). 62 63 definition good_sigma : 64 ∀p:unserialized_params. 65 ∀p':(∀F.sem_unserialized_params p F). 66 ∀prog : joint_program (mk_graph_params p). 67 ((Σi.is_internal_function_of_program … prog i) → label → option ℕ) → Prop ≝ 68 λp,p',graph_prog,sigma. 69 ∀i. 70 let graph_fun ≝ prog_if_of_function ?? i in 71 let sigma_local ≝ sigma i in 72 good_local_sigma ? p' ? graph_fun sigma_local. 41 ∀A.∀prog:program (λvars.fundef (A vars)) ℕ. 42 ∀f:Σi.is_internal_function ? (globalenv_noinit ? prog) i. 43 Σi.is_internal_function_of_program ?? prog i ≝ 44 if_in_global_env_to_if_in_prog_noinit 45 on _f : Sig ident (λi.is_internal_function ?? i) 46 to Sig ident (λi.is_internal_function_of_program ??? i). 47 *) 73 48 74 49 definition graph_prog_params ≝ … … 100 75 joint_abstract_status (lin_prog_params ? p' prog stack_sizes). 101 76 77 (* 78 axiom P : 79 ∀A,B,prog.A (prog_var_names (λvars.fundef (A vars)) B prog) → Prop. 80 81 check (λpars.let pars' ≝ make_global pars in λx :joint_closed_internal_function pars' (globals pars'). P … x) 82 (* 83 unification hint 0 ≔ p, prog, stack_sizes ; 84 pars ≟ mk_prog_params p prog stack_sizes , 85 pars' ≟ make_global pars, 86 A ≟ λvars.joint_closed_internal_function p vars, 87 B ≟ ℕ 88 ⊢ 89 A (prog_var_names (λvars.fundef (A vars)) B prog) ≡ 90 joint_closed_internal_function pars' (globals pars'). 91 *) 92 axiom T : ∀A,B,prog.genv_t (fundef (A (prog_var_names (λvars:list ident.fundef (A vars)) B prog))) → Prop. 93 (*axiom Q : ∀A,B,init,prog. 94 T … (globalenv (λvars:list ident.fundef (A vars)) B 95 init prog) → Prop. 96 97 lemma pippo : 98 ∀p,p',prog,stack_sizes. 99 let pars ≝ graph_prog_params p p' prog stack_sizes in 100 let ge ≝ ev_genv pars in T ?? prog ge → Prop. 101 102 #H1 #H2 #H3 #H4 103 #H5 104 whd in match (ev_genv ?) in H5; 105 whd in match (globalenv_noinit) in H5; normalize nodelta in H5; 106 whd in match (prog ?) in H5; 107 whd in match (joint_function ?) in H5; 108 @(Q … H5) 109 λx:T ??? ge.Q ???? x) 110 *) 111 axiom Q : ∀A,B,init,prog,i. 112 is_internal_function 113 (A 114 (prog_var_names (λvars:list ident.fundef (A vars)) B 115 prog)) 116 (globalenv (λvars:list ident.fundef (A vars)) B 117 init prog) 118 i → Prop. 119 120 check 121 (λp,p',prog,stack_sizes,i. 122 let pars ≝ graph_prog_params p p' prog stack_sizes in 123 let ge ≝ ev_genv pars in 124 λx:is_internal_function (joint_closed_internal_function pars (globals pars)) 125 ge i.Q ??? prog ? x) 126 *) 127 102 128 definition sigma_pc_opt: 103 129 ∀p,p',graph_prog,stack_sizes. 104 130 ((Σi.is_internal_function_of_program … graph_prog i) → 105 131 code_point (mk_graph_params p) → option ℕ) → 106 cpointer → option cpointer132 program_counter → option program_counter 107 133 ≝ 108 134 λp,p',prog,stack_sizes,sigma,pc. 109 135 let pars ≝ graph_prog_params p p' prog stack_sizes in 110 136 let ge ≝ ev_genv pars in 111 ! f ← int_funct_of_block ?? ge (pblock pc) ; 112 ! lin_point ← sigma f (point_of_pointer … pars pc) ; 113 res_to_opt … (pointer_of_point ? (make_sem_lin_params ? p') pc lin_point). 137 ! f ← int_funct_of_block ? ge (pc_block pc) ; 138 ! lin_point ← sigma (pi1 … f) (point_of_pc ? pars pc) ; 139 return pc_of_point ? (make_sem_lin_params ? p') pc lin_point. 140 @(is_internal_function_of_program_ok … prog … (pi2 … f)) 141 qed. 114 142 115 143 definition well_formed_pc: … … 117 145 ((Σi.is_internal_function_of_program … graph_prog i) → 118 146 label → option ℕ) → 119 cpointer → Prop147 program_counter → Prop 120 148 ≝ 121 149 λp,p',prog,stack_sizes,sigma,pc. … … 165 193 ∀pc. 166 194 ∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc. 167 cpointer ≝195 program_counter ≝ 168 196 λp,p',graph_prog,stack_sizes,sigma,st.opt_safe …. 169 197 … … 205 233 #A * #x #v normalize #EQ destruct % qed. 206 234 207 lemma if_propagate :208 ∀pars_in, pars_out : sem_params.209 ∀trans : ∀globals.joint_closed_internal_function pars_in globals →210 joint_closed_internal_function pars_out globals.211 ∀prog_in : program (joint_function pars_in) ℕ.212 let prog_out ≝213 transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in214 ∀i.is_internal_function_of_program … prog_in i →215 is_internal_function_of_program … prog_out i.216 cases daemon (* TODO by paolo *) qed.217 218 definition stack_sizes_lift :219 ∀pars_in, pars_out : sem_params.220 ∀trans : ∀globals.joint_closed_internal_function pars_in globals →221 joint_closed_internal_function pars_out globals.222 ∀prog_in : program (joint_function pars_in) ℕ.223 let prog_out ≝224 transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in225 ((Σi.is_internal_function_of_program … prog_out i) → ℕ) →226 ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝227 λpars_in,pars_out,prog_in,trans,stack_sizes.228 λi.stack_sizes «i, if_propagate … (pi2 … i)».229 230 axiom ok_is_internal_function_of_program :231 ∀p.∀prog:joint_program p.∀i.232 is_internal_function_of_program p prog i →233 is_internal_function ?? (globalenv_noinit ? prog) i.234 235 236 235 definition sigma_function_name : 237 236 ∀p,p',graph_prog. … … 244 243 (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝ 245 244 λp,p',graph_prog,lin_stack_sizes,f.pi1 … f. 246 @ok_is_internal_function_of_program 247 @(if_propagate (make_sem_graph_params p p') (make_sem_lin_params p p')) 248 @is_internal_function_of_program_ok 249 @(pi2 … f) 250 qed. 251 245 @(ok_is_internal_function_of_program ??? (linearise … graph_prog) ??) 246 @if_propagate 247 @is_internal_function_of_program_ok [2: @(pi2 … f) ] 248 qed. 252 249 253 250 lemma if_of_function_commute: 254 ∀p,p' ,graph_prog,stack_sizes.255 ∀graph_fun .256 let graph_fd ≝ if_of_function ? ??graph_fun in257 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_funin251 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p).∀stack_sizes. 252 ∀graph_fun,prf. 253 let graph_fd ≝ if_of_function ? (globalenv_noinit … graph_prog) graph_fun in 254 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes «graph_fun, prf» in 258 255 let lin_fd ≝ if_of_function … lin_fun in 259 lin_fd = linearise_int_fun … graph_fd. 260 (* usare match_opt_prf_elim ? *) 261 cases daemon qed. 256 lin_fd = \fst (linearise_int_fun ?? graph_fd). 257 #p #p' #graph_prog #stack_sizes #graph_fun #prf whd 258 (* Old comment? usare match_opt_prf_elim ? *) 259 cases daemon (* Job for Paolo *) qed. 262 260 263 261 lemma bind_opt_inversion: … … 277 275 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 278 276 ? graph_prog lin_stack_sizes in 279 ∀sigma, st.280 ∀prf : well_formed_ status p p' graph_prog graph_stack_sizes sigma st.281 p block (sigma_pc ? p' graph_prog graph_stack_sizes sigma (pc ? st) (proj1 … prf)) =282 p block (pc ? st).283 #p #p' #graph_prog #stack_sizes #sigma # st#prf277 ∀sigma,pc. 278 ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc. 279 pc_block (sigma_pc ? p' graph_prog graph_stack_sizes sigma pc prf) = 280 pc_block pc. 281 #p #p' #graph_prog #stack_sizes #sigma #pc #prf 284 282 whd in match sigma_pc; normalize nodelta 285 283 @opt_safe_elim #x #x_spec 286 whd in x_spec:(??%?); cases (int_funct_of_block ??? ?) in x_spec;284 whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec; 287 285 normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) H 288 #offset * #_ whd in ⊢ (??%? → ?); whd in match pointer_of_point; normalize nodelta 289 cases (opt_to_res ???) [2: #msg #abs normalize in abs; destruct] 290 #offset_lin whd in ⊢ (??%? → ?); #EQ destruct // 291 qed. 286 #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct // 287 qed. 288 289 lemma bind_opt_non_none : ∀A,B : Type[0] . ∀ m : option A . ∀g : A → option B. 290 (! x ← m ; g x) ≠ None ? → m ≠ None ?. 291 #A #B #m #g #H % #m_eq_none cases m >m_eq_none in H; normalize 292 [ #abs elim abs abs #abs @abs % 293  #abs elim abs abs #abs #v @abs % 294 ] 295 qed. 296 297 lemma match_option_non_none : ∀A ,B, C : Type[0]. ∀m : option A. ∀ x : A. 298 ∀ b : B .∀ f : A → B. ∀g : B → option C. 299 g (match m with [None ⇒ b  Some x ⇒ f x])≠ None ? → g b = None ? → m ≠ None ?. 300 #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 301 qed. 302 303 axiom int_funct_of_block_transf_commute: 304 ∀A,B.∀progr: program (λvars. fundef (A vars)) ℕ. 305 ∀transf: ∀vars. A vars → B vars. ∀bl,f,prf. 306 let progr' ≝ transform_program … progr (λvars.transf_fundef … (transf vars)) in 307 int_funct_of_block ? (globalenv_noinit … progr) bl = return f → 308 int_funct_of_block ? (globalenv_noinit … progr') bl = return «pi1 … f,prf». 292 309 293 310 lemma fetch_function_sigma_commute : … … 298 315 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 299 316 ? graph_prog lin_stack_sizes in 300 ∀sigma,st,f. 301 ∀prf : well_formed_status p p' graph_prog graph_stack_sizes sigma st. 302 let pc_st ≝ pc ? st in 317 ∀sigma,pc_st,f. 318 ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc_st. 303 319 fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc_st = 304 320 return f 305 → fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) (sigma_pc … pc_st (proj1 … prf)) = 321 → fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) 322 (sigma_pc … pc_st prf) = 306 323 return sigma_function_name … f. 307 324 #p #p' #graph_prog #stack_sizes #sigma #st #f #prf 308 >(sigma_pc_commute … prf)309 whd in match fetch_function; normalize nodelta 310 >(sigma_pblock_eq_lemma … prf) #H 311 lapply (opt_eq_from_res ???? H) H 312 whd in match int_funct_of_block in ⊢ (%→?); normalize nodelta 313 314 XXXX ENTRARE IN PRF CHE C'E' FUNCT OF BLOCK XXXX 315 325 whd in match fetch_function; normalize nodelta 326 >(sigma_pblock_eq_lemma … prf) #H 327 lapply (opt_eq_from_res ???? H) H #H 328 >(int_funct_of_block_transf_commute ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H) 329 // 330 qed. 331 332 (* 316 333 #H elim (bind_opt_inversion ????? H) H 317 334 #x * whd in match funct_of_block in ⊢ (%→?); normalize nodelta … … 369 386 #H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H) 370 387 H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%); 371 destruct // *)388 destruct // 372 389 cases daemon 373 qed. 390 qed. *) 374 391 375 392 lemma stmt_at_sigma_commute: 376 ∀p,p',graph_prog,stack_sizes,graph_fun, lbl.393 ∀p,p',graph_prog,stack_sizes,graph_fun,prf2,lbl,pt. 377 394 let lin_prog ≝ linearise ? graph_prog in 378 395 let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in 379 ∀sigma.good_sigma p p'graph_prog sigma →380 ∀prf:sigma graph_fun lbl ≠ None ….381 ∃stmt.396 ∀sigma.good_sigma p graph_prog sigma → 397 sigma «pi1 … graph_fun,prf2» lbl = return pt → 398 ∀stmt. 382 399 stmt_at … 383 (joint_if_code ?? (if_of_function ?? ?graph_fun))384 lbl = Some ? stmt ∧385 stmt_at …386 (joint_if_code ?? (if_of_function ?? ?lin_fun))387 (opt_safe … (sigma graph_fun lbl) prf) = Some ?(graph_to_lin_statement … stmt).388 #p #p' #graph_prog #stack_sizes #graph_fun # lbl#sigma #good #prf389 @opt_safe_elim prf #n#prf400 (joint_if_code ?? (if_of_function ?? graph_fun)) 401 lbl = return stmt → 402 stmt_at ?? 403 (joint_if_code ?? (if_of_function ?? lin_fun)) 404 pt = return (graph_to_lin_statement … stmt). 405 #p #p' #graph_prog #stack_sizes #graph_fun #prf2 #lbl #pt #sigma #good #prf 406 #prf 390 407 (* 391 408 whd in match (stmt_at ????); … … 412 429 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 413 430 ? graph_prog lin_stack_sizes in 414 ∀sigma.good_sigma p p'graph_prog sigma →431 ∀sigma.good_sigma p graph_prog sigma → 415 432 ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc. 416 433 fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc = … … 419 436 (sigma_pc … pc prf) = 420 437 return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉. 421 #p #p' #graph_prog #stack_sizes #pc #fn #stmt #good #prf 422 (* @opt_safe_elim prf #n #prf 423 whd in match fetch_statement; normalize nodelta 424 >fetch_function_sigma_commute 425 cases (fetch_function ????) [2://] 426 #graph_fun whd in ⊢ (??%%); 427 whd in ⊢ (???(match % with [ _ ⇒ ?  _ ⇒ ?])); 428 >stm_at_sigma_commute cases (stmt_at ????) // *) 429 cases daemon 438 #p #p' #graph_prog #stack_sizes #pc #fn #stmt #sigma #good #wfprf 439 whd in match fetch_statement; normalize nodelta #H 440 cases (bind_inversion ????? H) #id * H #H 441 >(fetch_function_sigma_commute … wfprf … H) H >m_return_bind 442 #H cases (bind_inversion ????? H) #fstmt * H #H 443 lapply (opt_eq_from_res ???? H) H #H #EQ whd in EQ:(??%%); destruct 444 >(stmt_at_sigma_commute … good … H) 445 [3: @is_internal_function_of_program_ok [2: @(pi2 … fn)] 446 2: cases daemon (* TO BE DONE, COMMUTATION LEMMA NEEDED *) ] 447 % 430 448 qed. 431 449 … … 438 456 ? graph_prog stack_sizes in 439 457 ∀sigma. 440 good_sigma p p'graph_prog sigma →458 good_sigma p graph_prog sigma → 441 459 status_rel 442 460 (graph_abstract_status p p' graph_prog stack_sizes') … … 509 527 qed. 510 528 *) 529 530 lemma IO_bind_inversion: 531 ∀O,I,A,B. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. 532 (! x ← f ; g x = return y) → 533 ∃x. (f = return x) ∧ (g x = return y). 534 #O #I #A #B #f #g #y cases f normalize 535 [ #o #f #H destruct 536  #a #e %{a} /2 by conj/ 537  #m #H destruct (H) 538 ] qed. 539 540 lemma opt_Exists_elim: 541 ∀A:Type[0].∀P:A → Prop. 542 ∀o:option A. 543 opt_Exists A P o → 544 ∃v:A. o = Some … v ∧ P v. 545 #A #P * normalize /3/ * 546 qed. 511 547 512 548 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 513 549 ex1_intro: ∀ x:A. P x → ex_Type1 A P. 514 interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x). 550 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) 551 515 552 516 553 lemma linearise_ok: … … 521 558 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 522 559 ? graph_prog lin_stack_sizes in 523 ∃R.560 ex_Type1 … (λR. 524 561 status_simulation 525 562 (graph_abstract_status p p' graph_prog graph_stack_sizes) 526 (lin_abstract_status p p' lin_prog lin_stack_sizes) R .563 (lin_abstract_status p p' lin_prog lin_stack_sizes) R). 527 564 #p #p' #graph_prog 528 cut (∃sigma.good_sigma p p' graph_prog sigma) 529 [ cases daemon (* TODO by Paolo *) ] * #sigma #good 565 cases (linearise_spec … graph_prog) #sigma #good 530 566 #lin_stack_sizes 531 567 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)} 532 568 whd 533 #st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl 569 #st1 #cl #st1' #st2 #move_st1_st1' * #wf_st1 #rel_st1_st2 #classified_st1_cl 570 whd in move_st1_st1'; whd in match eval_state in move_st1_st1':(??%?); 571 normalize nodelta in move_st1_st1'; 572 cases (IO_bind_inversion ??????? move_st1_st1') * #fn #stmt * 573 #fetch_statement_spec move_st1_st1' #move_st1_st1' 534 574 cases cl in classified_st1_cl; cl #classified_st1_cl whd 535 575 [4: 536 cases rel_st1_st2 rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 st2 537 whd in move_st1_st1'; 538 letin lin_prog ≝ (linearise ? graph_prog) 539 540 cut (joint_closed_internal_function (mk_graph_params p) (globals (graph_prog_params p p' graph_prog))) [cases daemon (*???*)] #graph_fun 541 542 cases (linearise_code_spec … p' graph_prog graph_fun 543 (joint_if_entry … graph_fun)) 544 * #lin_code_closed #sigma_entry_is_zero #sigma_spec 545 lapply (sigma_spec 546 (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … st1))) 547 sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … wf_st1) 2: skip ] 548 sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec whd in sigma_spec; 549 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] 550 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved 576 >rel_st1_st2 st2 letin lin_prog ≝ (linearise ? graph_prog) 577 cases (good (pi1 ?? fn)) [2: cases daemon (* TODO *) ] 578 #sigma_entry_is_zero #sigma_spec 579 lapply (sigma_spec (point_of_pc … (make_sem_graph_params … p') (pc … st1))) 580 sigma_spec #sigma_spec cases (sigma_spec ??) [3: @opt_to_opt_safe cases daemon (* TO REDO *) 2: skip ] 581 sigma_spec #graph_stmt * #graph_lookup_ok #sigma_spec 582 cases (opt_Exists_elim … sigma_spec) in ⊢ ?; 583 * #optlabel #lin_stm * #lin_lookup_ok whd in ⊢ (% → ?); ** #labels_preserved 551 584 #related_lin_stm_graph_stm 585 552 586 inversion (stmt_implicit_label ???) 553 587 [ whd in match (opt_All ???); #stmt_implicit_spec #_ 554 letin st2_opt' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) … 555 (ev_genv (lin_prog_params p p' lin_prog)) 556 (linearise_status_fun … sigma st1 wf_st1)) 557 check st2_opt' 558 cut (∃st2': lin_abstract_status p p' lin_prog. st2_opt' = return st2') 588 letin st2_opt' ≝ (eval_state … 589 (ev_genv (lin_prog_params … lin_prog lin_stack_sizes)) 590 (sigma_state … wf_st1)) 591 cut (∃st2': lin_abstract_status p p' lin_prog lin_stack_sizes. st2_opt' = return st2') 559 592 [cases daemon (* TODO, needs lemma? *)] * #st2' #st2_spec' 560 593 normalize nodelta in st2_spec'; st2_opt' … … 563 596  @st2_spec' ] 564 597 %[%] [%] 565 [ whd 566 whd in st2_spec':(??%?); >fetch_statement_sigma_commute in st2_spec'; 567 whd in move_st1_st1':(??%?); 568 cut (fetch_statement (graph_prog_params p p' graph_prog) (graph_prog_params … graph_prog) … (ev_genv (graph_prog_params … graph_prog)) … (pc … st1) = OK ? 〈graph_fun,graph_stmt〉) 569 [ cases daemon (* TODO once and for all, consequence of graph_lookup_ok *) ] 570 #fetch_statement_ok >fetch_statement_ok in move_st1_st1'; 571 whd in ⊢ (??%? → ??%? → ?); normalize nodelta 598 [ whd whd in match eval_state in st2_spec'; normalize nodelta in st2_spec'; 599 >(fetch_statement_sigma_commute … good … fetch_statement_spec) in st2_spec'; 600 >m_return_bind 601 (* Case analysis over the possible statements *) 572 602 inversion graph_stmt in stmt_implicit_spec; normalize nodelta 573 603 [ #stmt #lbl #_ #abs @⊥ normalize in abs; destruct(abs) ]
Note: See TracChangeset
for help on using the changeset viewer.