Changeset 2495
 Timestamp:
 Nov 27, 2012, 5:17:17 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2484 r2495 135 135 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → beval ≝ 136 136 λp,p',graph_prog,sigma,bv.opt_safe …. 137 138 definition sigma_is_opt : 139 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 140 ((Σi.is_internal_function_of_program … graph_prog i) → 141 code_point (mk_graph_params p) → option ℕ) → 142 internal_stack → option internal_stack ≝ 143 λp,p',graph_prog,sigma,is. 144 match is with 145 [ empty_is ⇒ return empty_is 146  one_is bv ⇒ ! bv' ← sigma_beval_opt p p' … sigma bv ; return one_is bv' 147  both_is bv1 bv2 ⇒ 148 ! bv1' ← sigma_beval_opt p p' … sigma bv1 ; 149 ! bv2' ← sigma_beval_opt p p' … sigma bv2 ; 150 return both_is bv1' bv2' 151 ]. 152 153 definition sigma_is : 154 ∀p,p',graph_prog,sigma,is. 155 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝ 156 λp,p',graph_prog,sigma,is.opt_safe …. 157 158 lemma sigma_is_pop_commute : 159 ∀p,p',graph_prog,sigma,is,bv,is'. 160 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?. 161 is_pop is = return 〈bv, is'〉 → 162 ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?. 163 ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?. 164 is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉. 165 cases daemon qed. 166 167 definition well_formed_mem : 168 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 169 ((Σi.is_internal_function_of_program … graph_prog i) → 170 code_point (mk_graph_params p) → option ℕ) → 171 bemem → Prop ≝ 172 λp,p',graph_prog,sigma,m. 173 ∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b → 174 sigma_beval_opt p p' graph_prog sigma (contents (blocks m b) z) ≠ None ?. 175 176 definition sigma_mem : 177 ∀p,p',graph_prog,sigma,m. 178 well_formed_mem p p' graph_prog sigma m → 179 bemem ≝ 180 λp,p',graph_prog,sigma,m,prf. 181 mk_mem 182 (λb. 183 If Zltb (block_id b) (nextblock m) then with prf' do 184 let l ≝ low_bound m b in 185 let h ≝ high_bound m b in 186 mk_block_contents l h 187 (λz.If Zleb l z ∧ Zltb z h then with prf'' do 188 sigma_beval p p' graph_prog sigma (contents (blocks m b) z) ? 189 else BVundef) 190 else empty_block OZ OZ) 191 (nextblock m) 192 (nextblock_pos m). 193 @hide_prf 194 lapply prf'' lapply prf' prf' prf'' 195 @Zltb_elim_Type0 [2: #_ * ] 196 #bid_ok * 197 @Zleb_elim_Type0 [2: #_ * ] 198 @Zltb_elim_Type0 [2: #_ #_ * ] 199 #zh #zl * @(prf … bid_ok zl zh) 200 qed. 201 202 lemma beloadv_sigma_commute: 203 ∀p,p',graph_prog,sigma,m,ptr,bv,prf1. 204 beloadv m ptr = return bv → 205 ∃ prf2. 206 beloadv (sigma_mem p p' graph_prog sigma m prf1) ptr = 207 return sigma_beval p p' graph_prog sigma bv prf2. 208 #p #p' #graph_prog #sigma #m #ptr #bv #prf1 209 whd in match beloadv in ⊢ (%→?); normalize nodelta 210 whd in match do_if_in_bounds in ⊢ (%→?); normalize nodelta 211 @Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)] 212 #block_id_ok 213 @Zleb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)] 214 #zh 215 @Zltb_elim_Type0 normalize nodelta [2: #_ #EQ whd in EQ : (??%%); destruct(EQ)] 216 #zl #EQ whd in EQ : (???%); destruct(EQ) 217 % [ @(prf1 ?? block_id_ok zh zl) ] 218 whd in match beloadv; normalize nodelta 219 whd in match do_if_in_bounds; normalize nodelta 220 @Zltb_elim_Type0 normalize nodelta [2: * #ABS @⊥ @ABS assumption] 221 #block_id_lin_ok 222 @Zleb_elim_Type0 normalize nodelta 223 [ 224  * #ABS @⊥ @ABS whd in match sigma_mem; normalize nodelta 225 226 lemma bestorev_sigma_commute : 227 ∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2. 228 bestorev m ptr bv = return m' → 229 ∃prf3. 230 bestorev (sigma_mem p p' graph_prog sigma m prf1) 231 ptr 232 (sigma_beval p p' graph_prog sigma bv prf2) 233 = 234 return (sigma_mem p p' graph_prog sigma m' prf3). 235 cases daemon qed. 236 237 record good_sem_state_sigma 238 (p : unserialized_params) 239 (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 240 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p)) 241 graph_prog i) → 242 label → option ℕ) : Type[0] ≝ 243 { well_formed_frames : framesT (make_sem_graph_params p p') → Prop 244 ; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p') 245 ; sigma_empty_frames_commute : 246 ∃prf. 247 empty_framesT (make_sem_lin_params p p') = 248 sigma_frames (empty_framesT (make_sem_graph_params p p')) prf 249 250 ; well_formed_regs : regsT (make_sem_graph_params p p') → Prop 251 ; sigma_regs : ∀regs.well_formed_regs regs → regsT (make_sem_lin_params p p') 252 ; sigma_empty_regsT_commute : 253 ∀ptr.∃ prf. 254 empty_regsT (make_sem_lin_params p p') ptr = 255 sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf 256 ; sigma_load_sp_commute : 257 ∀reg,ptr. 258 load_sp (make_sem_graph_params p p') reg = return ptr → 259 ∃prf. 260 load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr 261 ; sigma_save_sp_commute : 262 ∀reg,ptr,prf1. ∃prf2. 263 save_sp (make_sem_lin_params p p') (sigma_regs reg prf1) ptr = 264 sigma_regs (save_sp (make_sem_graph_params p p') reg ptr) prf2 265 }. 266 267 definition well_formed_state : 268 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 269 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 270 code_point (mk_graph_params p) → option ℕ). 271 good_sem_state_sigma p p' graph_prog sigma → 272 state (make_sem_graph_params p p') → Prop ≝ 273 λp,p',graph_prog,sigma,gsss,st. 274 well_formed_frames … gsss (st_frms … st) ∧ 275 sigma_is_opt p p' graph_prog sigma (istack … st) ≠ None ? ∧ 276 well_formed_regs … gsss (regs … st) ∧ 277 well_formed_mem p p' graph_prog sigma (m … st). 278 279 definition sigma_state : 280 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 281 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 282 code_point (mk_graph_params p) → option ℕ). 283 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 284 ∀st : state (make_sem_graph_params p p'). 285 well_formed_state … gsss st → 286 state (make_sem_lin_params p p') ≝ 287 λp,p',graph_prog,sigma,gsss,st,prf. 288 mk_state … 289 (sigma_frames … gsss (st_frms … st) (proj1 … (proj1 … (proj1 … prf)))) 290 (sigma_is p p' graph_prog sigma (istack … st) (proj2 … (proj1 … (proj1 … prf)))) 291 (carry … st) 292 (sigma_regs … gsss (regs … st) (proj2 … (proj1 … prf))) 293 (sigma_mem p p' graph_prog sigma (m … st) (proj2 … prf)). 294 295 296 (* 297 lemma sigma_is_pop_wf : 298 ∀p,p',graph_prog,sigma,is,bv,is'. 299 is_pop is = return 〈bv, is'〉 → 300 sigma_is_opt p p' graph_prog sigma is ≠ None ? → 301 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? ∧ 302 sigma_is_opt p p' graph_prog sigma is' ≠ None ?. 303 cases daemon qed. 304 *) 137 305 138 306 (* … … 180 348 #p #p' #graph_prog #sigma #st #prf @opt_to_opt_safe qed. 181 349 350 definition well_formed_state_pc : 351 ∀p,p',graph_prog,sigma. 352 good_sem_state_sigma p p' graph_prog sigma → 353 state_pc (make_sem_graph_params p p') → Prop ≝ 354 λp,p',prog,sigma,gsss,st. 355 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gsss st. 356 357 definition sigma_state_pc : 358 ∀p. 359 ∀p':∀F.sem_unserialized_params p F. 360 ∀graph_prog. 361 ∀sigma. 362 (* let lin_prog ≝ linearise ? graph_prog in *) 363 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 364 ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) 365 well_formed_state_pc p p' graph_prog sigma gsss s → 366 state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) 367 ≝ 368 λp,p',graph_prog,sigma,gsss,s,prf. 369 let pc' ≝ sigma_pc … (proj1 … prf) in 370 let st' ≝ sigma_state … (proj2 … prf) in 371 mk_state_pc ? st' pc'. 372 182 373 definition sigma_function_name : 183 374 ∀p,graph_prog. … … 187 378 λp,graph_prog,f.«f, if_propagate … (pi2 … f)». 188 379 189 record good_sigma_state (p : unserialized_params) 380 lemma m_list_map_All_ok : 381 ∀M : MonadProps.∀X,Y,f,l. 382 All X (λx.∃y.f x = return y) l → ∃l'.m_list_map M X Y f l = return l'. 383 cases daemon qed. 384 385 (* 386 inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝ 387  isMemberHead : ∀ tl.isMember A x (x :: tl) 388  isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl). 389 (* 390 definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl → 391 (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B. 392 #A #B #l #tl #y #l_spec #f #x #tl_member @f [//] 393 @(isMemberTail ? x y l tl l_spec tl_member) 394 qed. 395 *) 396 397 let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝ 398 match l with [ nil ⇒ λprf : l = nil ?.nil ? 399  cons x tl ⇒ λprf : l = cons ? x tl. 400 f x ? :: ext_map ?? tl (λy,prf'.f y ?) 401 ] (refl …). 402 @hide_prf 403 >prf 404 [ %1 405  %2 assumption 406 ] qed. 407 (f x (isMemberHead A x l tl prf)) :: 408 ext_map A B tl (lift_f_tail A B l tl x prf f) ] 409 (refl ? l). 410 *) 411 412 definition helper_def_store__commute : 413 ∀p,p',graph_prog,sigma. 414 ∀X : ? → Type[0]. 415 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 416 ∀store : ∀p,F.∀p' : sem_unserialized_params p F. 417 X p → beval → regsT p' → 418 res (regsT p'). 419 Prop ≝ 420 λp,p',graph_prog,sigma,X,gsss,store. 421 ∀a : X ?.∀bv,r,r',prf1,prf1'. 422 store … a bv r = return r' → 423 ∃prf2. 424 store ??? a 425 (sigma_beval p p' graph_prog sigma bv prf1') 426 (sigma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2. 427 428 definition helper_def_retrieve__commute : 429 ∀p,p',graph_prog,sigma. 430 ∀X : ? → Type[0]. 431 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 432 ∀retrieve : ∀p,F.∀p' : sem_unserialized_params p F. 433 regsT p' → X p → res beval. 434 Prop ≝ 435 λp,p',graph_prog,sigma,X,gsss,retrieve. 436 ∀a : X p.∀r,bv,prf1. 437 retrieve … r a = return bv → 438 ∃prf2. 439 retrieve … (sigma_regs … gsss r prf1) a 440 = return sigma_beval p p' graph_prog sigma bv prf2. 441 442 record good_state_sigma 443 (p : unserialized_params) 190 444 (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 191 445 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p)) … … 193 447 label → option ℕ) 194 448 : Type[0] ≝ 195 { well_formed_state : state (make_sem_graph_params p p') → Prop 196 ; sigma_state : ∀st.well_formed_state st → state (make_sem_lin_params p p') 197 198 ; acca_store_ok : 199 ∀a,bv,bv',st,st',prf1,prf2. 200 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 449 { gsss :> good_sem_state_sigma p p' graph_prog sigma 450 451 ; acca_store__commute : helper_def_store__commute … gsss acca_store_ 452 453 ; acca_retrieve_commute : helper_def_retrieve__commute … gsss acca_retrieve_ 454 455 }. 456 457 lemma store_commute : 458 ∀p,p',graph_prog,sigma. 459 ∀X : ? → Type[0]. 460 ∀store. 461 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 462 ∀H : helper_def_store__commute … gsss store. 463 ∀a : X p.∀bv,st,st',prf1,prf1'. 464 helper_def_store ? store … a bv st = return st' → 465 ∃prf2. 466 helper_def_store ? store … a 467 (sigma_beval p p' graph_prog sigma bv prf1') 468 (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2. 469 cases daemon qed. 470 471 lemma retrieve_commute : 472 ∀p,p',graph_prog,sigma. 473 ∀X : ? → Type[0]. 474 ∀retrieve. 475 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 476 ∀H : helper_def_retrieve__commute … gsss retrieve. 477 ∀a : X p .∀st,bv,prf1. 478 helper_def_retrieve ? retrieve … st a = return bv → 479 ∃prf2. 480 helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a = 481 return sigma_beval p p' graph_prog sigma bv prf2. 482 cases daemon qed. 483 484 (* 485 definition acca_store_commute : 486 ∀p,p',graph_prog,sigma. 487 ∀gss : good_state_sigma p p' graph_prog sigma. 488 ∀a : acc_a_reg p.∀bv,st,st',prf1,prf1'. 489 acca_store … a bv st = return st' → 490 ∃prf2. 491 acca_store … a 492 (sigma_beval p p' graph_prog sigma bv prf1') 493 (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 494 ≝ 495 λp,p',graph_prog,sigma. 496 λgss : good_state_sigma p p' graph_prog sigma. 497 store_commute … gss (acca_store__commute … gss).*) 498 499 500 lemma acca_store_commute : 501 ∀p,p',graph_prog,sigma. 502 ∀gss : good_state_sigma p p' graph_prog sigma. 503 ∀a,bv,st,st',prf1,prf1'. 201 504 acca_store ?? (p' ?) a bv st = return st' → 202 acca_store … (p' ?) a bv' (sigma_state st prf1) = return sigma_state st' prf2 203 ; acca_store_wf : ∀a,bv,bv',st,st'. 204 sigma_beval_opt p p' graph_prog sigma bv = Some ? bv' → 505 ∃prf2. 506 acca_store ?? (p' ?) a 507 (sigma_beval p p' graph_prog sigma bv prf1') 508 (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝ 509 λp,p',graph_prog,sigma,gss,a,bv.?. 510 * #frms #is #carry #regs #m 511 * #frms' #is' #carry' #regs' #m' 512 *** #frms_ok #is_ok #regs_ok #mem_ok 513 #bv_ok #EQ1 elim (bind_inversion ????? EQ1) 514 #regs'' * EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ) 515 elim (acca_store__commute … gss … EQ1) 516 [ #prf2 #EQ2 517 % [ whd /4 by conj/ ] 518 change with (! r ← ? ; ? = ?) >EQ2 519 whd in match (sigma_state ???????); normalize nodelta 520 >m_return_bind 521 522 523 st,st',prf1,prf2,prf3.?. 524 525 526 #p #p' # 527 (* 528 ; acca_store_wf : ∀a,bv,st,st'. 529 sigma_beval_opt p p' graph_prog sigma bv ≠ None ? → 205 530 acca_store ?? (p' ?) a bv st = return st' → 206 531 well_formed_state st → well_formed_state st' 207 532 208 ; acca_retrieve_ok :209 ∀a,st,bv,prf1,prf2.210 acca_retrieve ?? (p' ?) st a = return bv →211 acca_retrieve ?? (p' ?) (sigma_state st prf1) a =212 return sigma_beval p p' graph_prog sigma bv prf2213 533 ; acca_retrieve_wf : ∀a,st,bv. 214 534 acca_retrieve ?? (p' ?) st a = return bv → … … 373 693 well_formed_state st1 → well_formed_state st2 374 694 695 ; setup_call_ok : 696 ∀ n , parsT, call_args , st1 , st2 , prf1, prf2. 697 setup_call ?? (p' ?) n parsT call_args st1 = return st2 → 698 setup_call ?? (p' ?) n parsT call_args (sigma_state st1 prf1) = 699 return (sigma_state st2 prf2) 700 ; setup_call_wf : 701 ∀ n , parsT, call_args , st1 , st2. 702 setup_call ?? (p' ?) n parsT call_args st1 = return st2 → 703 well_formed_state st1 → well_formed_state st2 704 705 ; fetch_external_args_ok : (* TO BE CHECKED *) 706 ∀ex_fun,st1,prf1,call_args. 707 fetch_external_args ?? (p' ?) ex_fun st1 call_args = 708 fetch_external_args ?? (p' ?) ex_fun (sigma_state st1 prf1) call_args 709 ; fetch_external_args_wf : 710 ∀ex_fun,st1,call_args. 711 well_formed_state st1 → ∃ l. 712 fetch_external_args ?? (p' ?) ex_fun st1 call_args = OK ? l 713 714 ; set_result_ok : 715 ∀ l , call_dest , st1 , st2 , prf1 , prf2 . 716 set_result ?? (p' ?) l call_dest st1 = return st2 → 717 set_result ?? (p' ?) l call_dest (sigma_state st1 prf1) = 718 return (sigma_state st2 prf2) 719 ; set_result_wf : 720 ∀ l , call_dest , st1 , st2 . 721 set_result ?? (p' ?) l call_dest st1 = return st2 → 722 well_formed_state st1 → well_formed_state st2 723 724 ; read_result_ok : 725 let lin_prog ≝ linearise p graph_prog in 726 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 727 let stack_sizes' ≝ 728 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 729 ? graph_prog stack_sizes in 730 ∀call_dest , st1 , prf1, l1. 731 read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 732 call_dest st1 = return l1 → 733 ∀prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?. 734 read_result ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 735 call_dest (sigma_state st1 prf1) = return opt_safe … prf 736 ; read_result_wf : 737 let lin_prog ≝ linearise p graph_prog in 738 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 739 let stack_sizes' ≝ 740 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 741 ? graph_prog stack_sizes in 742 ∀call_dest , st1 , l1. 743 read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 744 call_dest st1 = return l1 → 745 well_formed_state st1 → 746 m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ? 747 748 ; pop_frame_ok : 749 let lin_prog ≝ linearise p graph_prog in 750 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 751 let stack_sizes' ≝ 752 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 753 ? graph_prog stack_sizes in 754 ∀ st1 , prf1, curr_id ,st2, prf2. 755 pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 756 curr_id st1 = return st2 → 757 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in 758 let st2' ≝ sigma_state (st_no_pc ? st2) (proj2 … prf2) in 759 pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 760 (sigma_function_name p graph_prog curr_id) (sigma_state st1 prf1) = 761 return mk_state_pc ? st2' pc' 762 ; pop_frame_wf : 763 let lin_prog ≝ linearise p graph_prog in 764 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 765 let stack_sizes' ≝ 766 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 767 ? graph_prog stack_sizes in 768 ∀ st1, curr_id ,st2. 769 pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 770 curr_id st1 = return st2 → 771 well_formed_state st1 → well_formed_pc p p' graph_prog sigma (pc ? st2) ∧ 772 well_formed_state (st_no_pc ? st2) 375 773 }. 376 774 … … 388 786 (Σi.is_internal_function … ge i) (* current *) → state st_pars → res (state st_pars) 389 787 *) 390 391 definition well_formed_state_pc : 392 ∀p,p',graph_prog,sigma. 393 good_sigma_state p p' graph_prog sigma → 394 state_pc (make_sem_graph_params p p') → Prop ≝ 395 λp,p',prog,sigma,gss,st. 396 well_formed_pc p p' prog sigma (pc … st) ∧ well_formed_state … gss st. 397 398 definition sigma_state_pc : 399 ∀p. 400 ∀p':∀F.sem_unserialized_params p F. 401 ∀graph_prog. 402 ∀sigma. 403 (* let lin_prog ≝ linearise ? graph_prog in *) 404 ∀gss : good_sigma_state p p' graph_prog sigma. 405 ∀s:state_pc (make_sem_graph_params p p'). (* = graph_abstract_status p p' graph_prog stack_sizes *) 406 well_formed_state_pc p p' graph_prog sigma gss s → 407 state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *) 408 ≝ 409 λp,p',graph_prog,sigma,gss,s,prf. 410 let pc' ≝ sigma_pc … (proj1 … prf) in 411 let st' ≝ sigma_state … (proj2 … prf) in 412 mk_state_pc ? st' pc'. 788 *) 413 789 414 790 (* … … 829 1205 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 830 1206 ? graph_prog stack_sizes in 831 ∀sigma.∀gss : good_s igma_state… graph_prog sigma.1207 ∀sigma.∀gss : good_state_sigma … graph_prog sigma. 832 1208 ∀fn,st,stmt,st'. 833 1209 ∀prf : well_formed_state … gss st.∀prf'. … … 840 1216 #fn #st #stmt 841 1217 #st' #prf #prf' 842 cases daemon (*843 1218 whd in match eval_seq_no_pc; 844 1219 cases stmt normalize nodelta 845 [1,2: #_ #EQ whd in EQ : (??%%); destruct(EQ) // 846  #mv_sig whd in match pair_reg_move in ⊢ (%→?); normalize nodelta 1220 [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1221  (* MOVE *) #mv_sig #H lapply(err_eq_from_io ????? H) H #H 1222 >(pair_reg_move_ok ?????????? H) [%  skip] 1223  (* POP *) 1224 #a #H lapply(err_eq_from_io ????? H) H #H elim (bind_inversion ????? H) H 1225 * #val #st1 * #vals_spec #H 1226 cut(well_formed_state … gss st1) [ cases daemon (* to be added to gss *) ] 1227 #wf_st1 1228 lapply(acca_store_wf ????????? H wf_st1) 1229 * #_ #sigma_val_spec 1230 lapply vals_spec vals_spec 1231 whd in match pop; normalize nodelta 1232 #H1 elim (bind_inversion ????? H1) H1 * #g_bev #g_is * #ispop_spec 1233 whd in ⊢ ((??%%) → ?); #EQ (*to be destructed*) 1234 lapply ispop_spec ispop_spec 1235 whd in match is_pop; normalize nodelta 1236 cases (istack ? st) normalize nodelta 1237 [ #ABS whd in ABS : (???%); destruct(ABS) 1238  #one whd in ⊢ ((??%%) → ?); #EQ1 destruct(EQ1) 1239 cases (istack ? (sigma_state … st prf)) normalize nodelta 1240 1241 lapply (acca_store_ok ?????????????? H) 1242 1243 1244 val_spec * #bv #is * #bv_is_spec 1245 #EQ whd in EQ : (??%%); destruct(EQ) 1246 whd in match is_pop in bv_is_spec; normalize nodelta in bv_is_spec; 1247 inversion (istack ? st) in bv_is_spec; 1248 [ #_ normalize nodelta whd in ⊢ ((???%) → ?); #ABS destruct(ABS) 1249  #bv1 #bv1_spec normalize nodelta whd in ⊢ ((??%%) → ?); #EQ destruct(EQ) 1250 lapply(acca_store_wf ????????? H prf) check acca_store_ok check(acca_store_ok ?????????????? H) 1251 1252 @(pair_reg_move_ok ? ? ? ? gss mv_sig st st' ? ?) whd in match pair_reg_move in ⊢ (%→?); normalize nodelta 847 1253 #H 848 ] *)849 1254 qed. 850 1255
Note: See TracChangeset
for help on using the changeset viewer.