Changeset 2547 for src/joint/lineariseProof.ma
 Timestamp:
 Dec 7, 2012, 8:37:51 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/lineariseProof.ma
r2543 r2547 17 17 include "joint/Traces.ma". 18 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)). 19 143 20 144 definition graph_prog_params ≝ … … 156 280 sigma_is_opt p p' graph_prog sigma is ≠ None ? → internal_stack ≝ 157 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. 158 299 159 300 lemma sigma_is_pop_commute : 160 ∀p,p',graph_prog,sigma,is ,bv,is'.301 ∀p,p',graph_prog,sigma,is. 161 302 ∀prf : sigma_is_opt p p' graph_prog sigma is ≠ None ?. 162 is_pop is = return 〈bv, is'〉 → 163 ∃prf' : sigma_beval_opt p p' graph_prog sigma bv ≠ None ?. 164 ∃prf'' : sigma_is_opt p p' graph_prog sigma is' ≠ None ?. 165 is_pop (sigma_is … prf) = return 〈sigma_beval … prf', sigma_is … prf''〉. 166 cases daemon qed. 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. *) 167 352 168 353 definition well_formed_mem : … … 211 396 nextblock m1 = nextblock m2 → m1 = m2. 212 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 213 401 lemma beloadv_sigma_commute: 214 ∀p,p',graph_prog,sigma,m,ptr,bv,prf1. 215 beloadv m ptr = return bv → 216 ∃ prf2. 217 beloadv (sigma_mem p p' graph_prog sigma m prf1) ptr = 218 return sigma_beval p p' graph_prog sigma bv prf2. 219 #p #p' #graph_prog #sigma #m #ptr #bv #prf1 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 220 409 whd in match beloadv; 221 410 whd in match do_if_in_bounds; … … 238 427 239 428 lemma bestorev_sigma_commute : 240 ∀p,p',graph_prog,sigma,m,ptr,bv,m',prf1,prf2. 241 bestorev m ptr bv = return m' → 242 ∃prf3. 243 bestorev (sigma_mem p p' graph_prog sigma m prf1) 244 ptr 245 (sigma_beval p p' graph_prog sigma bv prf2) 246 = 247 return (sigma_mem p p' graph_prog sigma m' prf3). 248 #p #p' #graph_prog #sigma #m #ptr #bv #m' #prf1 #prf2 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' 249 437 whd in match bestorev; 250 438 whd in match do_if_in_bounds; … … 326 514 sigma_regs (empty_regsT (make_sem_graph_params p p') ptr) prf 327 515 ; sigma_load_sp_commute : 328 ∀reg,ptr. 329 load_sp (make_sem_graph_params p p') reg = return ptr → 330 ∃prf. 331 load_sp (make_sem_lin_params p p') (sigma_regs reg prf) = return ptr 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')) 332 523 ; sigma_save_sp_commute : 333 524 ∀reg,ptr,prf1. ∃prf2. … … 361 552 (sigma_regs … gsss (regs … st) ?) 362 553 (sigma_mem p p' graph_prog sigma (m … st) ?). 363 @hide_prf 364 [ @(proj1 … (proj1 … (proj1 … prf)))  @(proj2 … (proj1 … (proj1 … prf))) 365  @(proj2 … (proj1 … prf))  @(proj2 … prf)] 554 @hide_prf cases prf ** // 366 555 qed. 367 556 … … 455 644 cases daemon qed. 456 645 457 (*458 inductive isMember (A : Type[0]) (x : A) : list A → Prop ≝459  isMemberHead : ∀ tl.isMember A x (x :: tl)460  isMemberTail : ∀ y,tl .isMember A x tl → isMember A x (y :: tl).461 (*462 definition lift_f_tail : ∀ A,B : Type[0]. ∀ l ,tl : list A. ∀y : A . l = y ::tl →463 (∀ x : A. isMember A x l → B) → ∀ x : A. isMember A x tl → B.464 #A #B #l #tl #y #l_spec #f #x #tl_member @f [//]465 @(isMemberTail ? x y l tl l_spec tl_member)466 qed.467 *)468 469 let rec ext_map (A,B : Type[0]) (l : list A) (f : ∀ x : A. isMember A x l → B) on l : list B ≝470 match l with [ nil ⇒ λprf : l = nil ?.nil ?471  cons x tl ⇒ λprf : l = cons ? x tl.472 f x ? :: ext_map ?? tl (λy,prf'.f y ?)473 ] (refl …).474 @hide_prf475 >prf476 [ %1477  %2 assumption478 ] qed.479 (f x (isMemberHead A x l tl prf)) ::480 ext_map A B tl (lift_f_tail A B l tl x prf f) ]481 (refl ? l).482 *)483 484 646 definition helper_def_store__commute : 485 647 ∀p,p',graph_prog,sigma. … … 491 653 Prop ≝ 492 654 λp,p',graph_prog,sigma,X,gsss,store. 493 ∀a : X ?.∀bv,r,r',prf1,prf1'.494 store … a bv r = return r' →495 ∃prf2.496 store ??? a497 (s igma_beval p p' graph_prog sigma bv prf1')498 (s igma_regs ???? gsss r prf1) = return sigma_regs … gsss r' prf2.499 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 500 662 definition helper_def_retrieve__commute : 501 663 ∀p,p',graph_prog,sigma. … … 506 668 Prop ≝ 507 669 λp,p',graph_prog,sigma,X,gsss,retrieve. 508 ∀a : X p. ∀r,bv,prf1.509 retrieve … r a = return bv →510 ∃prf2.511 retrieve … (sigma_regs … gsss r prf1) a512 = return sigma_beval p p' graph_prog sigma bv prf2.513 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). 514 676 515 677 record good_state_sigma … … 533 695 ; dph_arg_retrieve_commute : helper_def_retrieve__commute … gsss dph_arg_retrieve_ 534 696 ; snd_arg_retrieve_commute : helper_def_retrieve__commute … gsss snd_arg_retrieve_ 535 ; pair_reg_move_commute : ∀mv,r1,r2,prf1. 536 pair_reg_move_ ? ? (p' ?) r1 mv = return r2 → 537 ∃prf2 . 538 pair_reg_move_ ? ? (p' ?) (sigma_regs p p' graph_prog sigma gsss r1 prf1) mv = 539 return sigma_regs p p' graph_prog sigma gsss r2 prf2 540 ; save_frame_commute : 541 ∀b,dest,st1,st2,prf1. 542 save_frame ?? (p' ?) b dest st1 = return st2 → 543 let st1' ≝ mk_state_pc … (sigma_state p p' graph_prog sigma gsss st1 (proj2 … prf1)) 544 (sigma_pc p p' graph_prog sigma (pc … st1) (proj1 … prf1)) in 545 ∃prf2. 546 save_frame ?? (p' ?) b dest st1' = return sigma_state p p' graph_prog sigma gsss st2 prf2 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) 547 701 ; allocate_locals_commute : 548 ∀ 702 ∀loc, r1, prf1. ∃ prf2. 549 703 allocate_locals_ ? ? (p' ?) loc (sigma_regs p p' graph_prog sigma gsss r1 prf1) = 550 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) 551 715 ; eval_ext_seq_commute : 552 716 let lin_prog ≝ linearise p graph_prog in 553 717 ∀ stack_sizes. 554 ∀ext,i,fn,st1,st2,prf1. 555 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 556 ext i fn st1 = return st2 → 557 ∃prf2. 558 eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 559 ext i (\fst (linearise_int_fun … fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) = 560 return sigma_state p p' graph_prog sigma gsss st2 prf2 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 561 728 ; setup_call_commute : 562 729 ∀ n , parsT, call_args , st1 , st2 , prf1. … … 597 764 return mk_state_pc ? st2' pc' 598 765 }. 766 *) 599 767 600 768 … … 606 774 ∀X : ? → Type[0]. 607 775 ∀store. 608 ∀gsss : good_s em_state_sigma p p' graph_prog sigma.776 ∀gsss : good_state_sigma p p' graph_prog sigma. 609 777 ∀H : helper_def_store__commute … gsss store. 610 ∀a : X p.∀bv,st,st',prf1,prf1'. 611 helper_def_store ? store … a bv st = return st' → 612 ∃prf2. 613 helper_def_store ? store … a 614 (sigma_beval p p' graph_prog sigma bv prf1') 615 (sigma_state … gsss st prf1) = return sigma_state … gsss st' prf2. 616 #p #p' #graph_prog #sigma #X #store #gsss #H #a #bv #st #st #prf1 #prf2 617 whd in match helper_def_store; normalize nodelta 618 #H1 elim(bind_inversion ????? H1) H1 #graph_reg * #store_spec 619 #EQ whd in EQ : (??%%); destruct(EQ) 620 elim(H a bv ?? (proj2 … (proj1 … prf1)) prf2 store_spec) 621 #wf_graph_reg #store_spec1 % 622 [ % [ % ] [%] ] 623 [ @(proj1 … (proj1 … (proj1 … prf1))) 624  @(proj2 … (proj1 … (proj1 … prf1))) 625  @wf_graph_reg 626  @(proj2 … prf1) 627 ] >store_spec1 >m_return_bind % 628 qed. 629 630 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. 631 791 632 792 lemma retrieve_commute : … … 636 796 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 637 797 ∀H : helper_def_retrieve__commute … gsss retrieve. 638 ∀a : X p .∀st,bv,prf1. 639 helper_def_retrieve ? retrieve … st a = return bv → 640 ∃prf2. 641 helper_def_retrieve ? retrieve … (sigma_state … gsss st prf1) a = 642 return sigma_beval p p' graph_prog sigma bv prf2. 643 #p #p' #graph_prog #sigma #X #retrieve #gsss #H #a #st #bv #prf1 644 whd in match helper_def_retrieve; normalize nodelta 645 #retrieve_spec elim(H … (proj2 … (proj1 … prf1)) … retrieve_spec) 646 #wf_bv #retrieve_spec1 %{wf_bv} >retrieve_spec1 % 647 qed. 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. 648 805 649 806 (* … … 686 843 *) 687 844 688 lemma res_eq_from_opt :689 ∀A,m,v.res_to_opt A m = return v → m = return v.690 #A * #x #v normalize #EQ destruct % qed.691 692 845 (* 693 846 lemma if_of_function_commute: … … 702 855 @prog_if_of_function_transform % qed. 703 856 *) 704 lemma bind_option_inversion_star:705 ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B.706 (∀x.f = Some … x → g x = Some … y → P) →707 (! x ← f ; g x = Some … y) → P.708 #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed.709 710 interpretation "option bind inversion" 'bind_inversion =711 (bind_option_inversion_star ???????).712 713 857 lemma sigma_pblock_eq_lemma : 714 858 ∀p,p',graph_prog. … … 720 864 #p #p' #graph_prog #sigma #pc #prf 721 865 whd in match sigma_pc; normalize nodelta 722 @opt_safe_elim #x @'bind_inversion* #i #fn #_723 @'bind_inversion#n #_ whd in ⊢ (??%?→?);866 @opt_safe_elim #x #H @('bind_inversion H) H * #i #fn #_ 867 #H @('bind_inversion H) H #n #_ whd in ⊢ (??%?→?); 724 868 #EQ destruct % 725 869 qed. … … 881 1025 whd in match fetch_function; normalize nodelta 882 1026 #H lapply (opt_eq_from_res ???? H) H 883 @'bind_inversion#id #eq_symbol_for_block884 @'bind_inversion#fd #eq_find_funct1027 #H @('bind_inversion H) H #id #eq_symbol_for_block 1028 #H @('bind_inversion H) H #fd #eq_find_funct 885 1029 whd in ⊢ (??%?→?); #EQ destruct(EQ) 886 1030 >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind 887 >(find_funct_ptr_transf A B … eq_find_funct) >m_return_bind % 888 qed. 889 890 lemma bind_inversion_star : ∀X,Y.∀P : Prop. 891 ∀m : res X.∀f : X → res Y.∀v : Y. 892 (∀x. m = return x → f x = return v → P) → 893 ! x ← m ; f x = return v → P. 894 #X #Y #P #m #f #v #H #G 895 elim (bind_inversion ????? G) #x * @H qed. 896 897 interpretation "res bind inversion" 'bind_inversion = 898 (bind_inversion_star ???????). 1031 >(find_funct_ptr_transf A B … eq_find_funct) % 1032 qed. 899 1033 900 1034 lemma fetch_internal_function_transf : … … 909 1043 #A #B #prog #trans #bl #i #f 910 1044 whd in match fetch_internal_function; normalize nodelta 911 @'bind_inversion* #id * #fd normalize nodelta #EQfetch1045 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch 912 1046 whd in ⊢ (??%%→?); #EQ destruct(EQ) 913 1047 >(fetch_function_transf … EQfetch) % … … 1005 1139 // 1006 1140 qed. 1007 1141 1008 1142 (* 1009 1143 … … 1038 1172 1039 1173 lemma pc_of_label_sigma_commute : 1040 ∀p,p',graph_prog, pc,lbl,i,fn.1174 ∀p,p',graph_prog,bl,lbl,i,fn. 1041 1175 let lin_prog ≝ linearise ? graph_prog in 1042 1176 ∀sigma.good_sigma p graph_prog sigma → 1043 ∀prf : well_formed_pc p p' graph_prog sigma pc.1044 1177 fetch_internal_function … 1045 (globalenv_noinit … graph_prog) (pc_block pc)= return 〈i, fn〉 →1046 let pc' ≝ pc_of_point (make_sem_graph_params p p') … (pc_block pc)lbl in1178 (globalenv_noinit … graph_prog) bl = return 〈i, fn〉 → 1179 let pc' ≝ pc_of_point (make_sem_graph_params p p') … bl lbl in 1047 1180 code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl → 1048 1181 ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) 1049 (pc_block (sigma_pc … pc prf))lbl =1182 bl lbl = 1050 1183 return sigma_pc p p' graph_prog sigma pc' prf'. 1051 #p #p' #graph_prog # pc#lbl #i #fn1184 #p #p' #graph_prog #bl #lbl #i #fn 1052 1185 #sigma #good cases (good fn) good * #_ #all_labels_in 1053 #good # prf #fetchfn >lin_code_has_label #lbl_in1186 #good #fetchfn >lin_code_has_label #lbl_in 1054 1187 whd in match pc_of_label; normalize nodelta 1055 >sigma_pblock_eq_lemma1056 1188 > (fetch_internal_function_transf … fetchfn) >m_return_bind 1057 1189 inversion (point_of_label ????) … … 1099 1231 All ? (λlbl.well_formed_pc p p' graph_prog sigma 1100 1232 (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl)) 1101 (stmt_ explicit_labels … stmt) ∧1233 (stmt_labels … stmt) ∧ 1102 1234 match stmt with 1103 1235 [ sequential s nxt ⇒ … … 1145 1277 lapply(stmt_at_sigma_commute ???????? (good graph_fun) ?? graph_stmt) 1146 1278 [@lin_pt_spec] * #H1 #H2 % 1147 [ H2 @(All_mp … (All_append_r … H1)) #lab #lab_spec1279 [ H2 @(All_mp … H1) #lab #lab_spec 1148 1280 whd in match well_formed_pc; normalize nodelta 1149 1281 whd in match sigma_pc_opt; normalize nodelta >fetchfn … … 1173 1305 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1174 1306 cases(proj2 … H3)[ #EQ >EQ >m_return_bind whd in ⊢ (?(??%?)); % #ABS destruct(ABS)] 1175 lapply all_labels_spec #Z 1176 lapply(All_nth ? ? 0 ? Z nxt) whd in match stmt_labels; normalize nodelta 1177 #Z1 normalize in Z1; lapply(Z1 ?) [%] inversion(sigma ??) 1178 [#_ #ABS @⊥ elim ABS #ABS @ABS %] #sn #sigma_graph_f_spec >sigma_graph_f_spec 1179 #_ #_ >m_return_bind % #ABS 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) 1180 1310  cases(proj2 … H3) 1181 1311 [ #Z %1 whd in match sigma_pc; normalize nodelta 1182 1312 @opt_safe_elim #pc1 whd in match sigma_pc_opt; normalize nodelta 1183 1313 >lin_pc_spec #EQ destruct(EQ) 1184 @opt_safe_elim #pc2 >fetchfn >m_return_bind 1185 whd in match point_of_pc; whd in match succ_pc; normalize nodelta 1186 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1314 @opt_safe_elim #pc2 >fetchfn >m_return_bind >graph_succ_pc 1315 >point_of_pc_of_point 1187 1316 >Z >m_return_bind #EQ whd in EQ : (??%?); destruct(EQ) 1317 whd in match succ_pc; 1188 1318 whd in match point_of_pc; whd in match point_of_succ; normalize nodelta 1189 1319 >point_of_offset_of_point % … … 1206 1336 ] 1207 1337  cases H3 1208 [ * #Z1 #Z2 %1 % [ @hide_prf whd in match well_formed_pc; normalize nodelta1338 [ * #Z1 #Z2 %1 % [ @hide_prf whd in match well_formed_pc; 1209 1339 whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind 1210 whd in match point_of_pc; whd in match succ_pc; normalize nodelta 1211 whd in match pc_of_point; normalize nodelta >point_of_offset_of_point 1212 >Z2 >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS) 1340 >graph_succ_pc >point_of_pc_of_point 1341 >Z2 % #ABS whd in ABS : (??%?); destruct(ABS) 1213 1342 ] % 1214 1343 [ whd in match sigma_pc; normalize nodelta … … 1280 1409 @opt_safe_elim H 1281 1410 #res #_ 1282 #H lapply (res_eq_from_opt ??? H) H1411 #H 1283 1412 #H @('bind_inversion H) H 1284 1413 * #f #stmt … … 1335 1464 qed. 1336 1465 1337 lemma IO_bind_inversion:1338 ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.1339 (∀x.f = return x → g x = return y → P) →1340 (! x ← f ; g x = return y) → P.1341 #O #I #A #B #P #f #g #y cases f normalize1342 [ #o #f #_ #H destruct1343  #a #G #H @(G ? (refl …) H)1344  #e #_ #H destruct1345 ] qed.1346 1347 interpretation "IO bind inversion" 'bind_inversion =1348 (IO_bind_inversion ?????????).1349 1350 lemma err_eq_from_io : ∀O,I,X,m,v.1351 err_to_io O I X m = return v → m = return v.1352 #O #I #X * #x #v normalize #EQ destruct % qed.1353 1354 lemma err_eq_to_io : ∀O,I,X,m,v.1355 m = return v → err_to_io O I X m = return v.1356 #O #I #X #m #v #H >H //1357 qed.1358 1359 1466 lemma set_istack_sigma_commute : 1360 ∀p,p',graph_prog,sigma,gss,st,is,sigma_is,prf1,prf2. 1361 sigma_is_opt p p' graph_prog sigma is = return sigma_is → 1362 set_istack ? sigma_is (sigma_state p p' graph_prog sigma gss st prf1) = 1363 sigma_state ???? gss (set_istack ? is st) prf2. 1364 #p #p' #graph_prog #sigma #gss #st #is #sigmais #prf1 #prf2 #H 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 1365 1473 whd in match set_istack; normalize nodelta 1366 1474 whd in match sigma_state; normalize nodelta … … 1369 1477 cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %] 1370 1478 #EQ >EQ // 1371 qed. 1479 qed.*) 1372 1480 1373 1481 (* this should make things easier for ops using memory (where pc cant happen) *) … … 1391 1499 qed. 1392 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 1393 1507 lemma is_push_sigma_commute : 1394 ∀ p, p', graph_prog,sigma ,is,val,is',prf1,prf2.1395 (is_push is val=return is') → 1396 ∃prf3. 1397 is_push (sigma_is p p' graph_prog sigma is prf1) 1398 (sigma_ beval p p' graph_prog sigma val prf2) =1399 return sigma_is p p' graph_prog sigma is' prf3.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. 1400 1514 #p #p' #graph_prog #sigma * 1401 [  #bv1  #bv1 #bv2 ] #val # is' #prf1 #prf21515 [  #bv1  #bv1 #bv2 ] #val #prf1 #prf2 #is' 1402 1516 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1403 1517 whd in match sigma_beval; normalize nodelta … … 1423 1537 qed. 1424 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 1425 1551 lemma beopaccs_sigma_commute : 1426 ∀p,p',graph_prog,sigma,op,val1,val2,opaccs1,opaccs2. 1427 ∀ prf1 : sigma_beval_opt p p' graph_prog sigma val1 ≠ None ?. 1428 ∀ prf2 : sigma_beval_opt p p' graph_prog sigma val2 ≠ None ?. 1429 be_opaccs op val1 val2=return 〈opaccs1,opaccs2〉 → 1430 ∃ prf1' : sigma_beval_opt p p' graph_prog sigma opaccs1 ≠ None ?. 1431 ∃ prf2' : sigma_beval_opt p p' graph_prog sigma opaccs2 ≠ None ?. 1432 be_opaccs op (sigma_beval … prf1) (sigma_beval … prf2) = 1433 return 〈(sigma_beval … prf1'),(sigma_beval … prf2')〉. 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). 1434 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 1435 1615 @bv_pc_other 1436 [ #pc1 #p1 #val2 1437  #val1 #val1_no_pc @bv_pc_other 1438 [ #pc #p  #val2 #val2_no_pc ] 1439 ] 1440 #opaccs1 #opaccs2 1441 #prf1 #prf2 1442 [1,2: [2: #H @('bind_inversion H) #by1 #_ ] 1443 whd in ⊢ (??%%→?); #EQ destruct] 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) ] 1444 1629 #EQ 1445 >(sigma_bv_no_pc … val1_no_pc) 1446 >(sigma_bv_no_pc … val2_no_pc) 1447 cut (bv_no_pc opaccs1 ∧ bv_no_pc opaccs2) 1448 [ cases val1 in EQ; cases daemon ] * 1449 #H1 #H2 @('bind_inversion EQ) #bt #bt_spec 1450 #H3 @('bind_inversion H3) #bt' 1451 #bt_spec' cases (opaccs eval op bt bt') 1452 #ev_bt #ev_bt' normalize nodelta 1453 #EQ1 whd in EQ1 : (??%%); destruct(EQ1) 1454 % [ whd in match sigma_beval_opt ; normalize nodelta % 1455 #ABS whd in ABS : (??%?); destruct(ABS) ] 1456 % [ whd in match sigma_beval_opt ; normalize nodelta % 1457 #ABS whd in ABS : (??%?); destruct(ABS) ] 1458 >(sigma_bv_no_pc … H1) 1459 >(sigma_bv_no_pc … H2) assumption 1460 qed. 1461 1462 lemma sigma_ptr_commute : 1463 ∀ p, p', graph_prog , sigma , val1, val2, ptr, prf1, prf2. 1464 pointer_of_address 〈val1,val2〉= return ptr → 1465 pointer_of_address 〈sigma_beval p p' graph_prog sigma val1 prf1, 1466 sigma_beval p p' graph_prog sigma val2 prf2〉 = return ptr. 1467 #p #p' #graph_prog #sigma #val1 #val2 #ptr #prf1 #prf2 1468 whd in match sigma_beval; normalize nodelta 1469 @opt_safe_elim #sigma_val1 #sigma_val1_spec 1470 @opt_safe_elim #sigma_Val2 #sigma_val2_spec 1471 whd in match pointer_of_address; whd in match pointer_of_bevals; 1472 normalize nodelta cases val1 in sigma_val1_spec; normalize nodelta 1473 [1,2,3,4,5: [ #ptr1 #ptr2 #p  #by  #p] #_ #ABS whd in ABS : (??%%); destruct(ABS) 1474  #ptr2 #p2 whd in match sigma_beval_opt; normalize nodelta 1475 #EQ whd in EQ : (??%%); destruct(EQ) cases val2 in sigma_val2_spec; normalize nodelta 1476 [1,2,3,4,5: [ #ptr1 #ptr2 #p  #by  #p] #_ #ABS whd in ABS : (??%%); destruct(ABS) 1477  #ptr1 #p1 whd in match sigma_beval_opt; normalize nodelta 1478 #EQ whd in EQ : (??%%); destruct(EQ) normalize nodelta // 1479  #a #b #_ #ABS whd in ABS : (???%); destruct(ABS) 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' 1480 1656 ] 1481  #a #b #_ #ABS whd in ABS : (???%); destruct(ABS) 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 ] 1482 1682 ] 1483 skip 1484 qed. 1485 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. 1486 1744 1487 1745 lemma eval_seq_no_pc_sigma_commute : … … 1490 1748 ∀stack_sizes. 1491 1749 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 1492 ∀f,fn,st ,stmt,st'.1493 ∀prf : well_formed_state … gss st.1494 eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))1495 f fn stmt st = return st' →1496 ∃prf'.1497 eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))1498 f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) =1499 return sigma_state … gss st' prf'.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). 1500 1758 #p #p' #graph_prog #stack_sizes #sigma #gss #f 1501 #fn #st #stmt 1502 #st' #prf 1759 #fn #stmt 1503 1760 whd in match eval_seq_no_pc; 1504 1761 cases stmt normalize nodelta 1505 [1,2: (* COMMENT, COST_LABEL *) #_ #EQ whd in EQ : (??%%); destruct(EQ) %{prf} // 1506  (* MOVE *) #mv_sig #H 1507 whd in match pair_reg_move; normalize nodelta 1508 @('bind_inversion H) H #reg #reg_spec #EQ whd in EQ : (??%%); destruct(EQ) 1509 elim(pair_reg_move_commute ???????? (proj2 … (proj1 … prf)) reg_spec) 1510 #wf_regs #pm_spec >pm_spec >m_return_bind % [2: %] 1511 % [ 2: @(proj2 … prf) 1512  % [2: assumption] % 1513 [ @(proj1 … (proj1 … (proj1 … prf))) 1514  @(proj2 … (proj1 … (proj1 … prf))) 1515 ] 1516 ] 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 ] 1517 1768  (* POP *) 1518 #a #H @('bind_inversion H) H 1519 * #val #st1 #vals_spec #H 1520 lapply vals_spec vals_spec 1521 whd in match pop; normalize nodelta 1522 whd in match is_pop; normalize nodelta 1523 lapply(proj2 … (proj1 … (proj1 … prf))) #wf_is 1524 inversion (istack (make_sem_graph_params p p') st) normalize nodelta 1525 [#_ #ABS normalize in ABS; destruct(ABS)] 1526 [ #Bv  #Bv_not_used #Bv] #is_stack_st_spec >m_return_bind 1527 #EQ whd in EQ : (??%%); destruct(EQ) 1528 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ?????? H) 1529 [ 2,5: @hide_prf >is_stack_st_spec in wf_is; #wf_is 1530 whd in match sigma_is_opt in wf_is; normalize nodelta in wf_is; 1531 inversion(sigma_beval_opt ?????) 1532 [1,3 : #EQ >EQ in wf_is; whd in ⊢ ((?(??%?)) → ?); * #ABS @⊥ @ABS // 1533 inversion(sigma_beval_opt ?????) normalize nodelta 1534 [ #bev % 1535  #bev #bev_s >bev_s in ABS; normalize nodelta 1536 #ABS @⊥ @ABS normalize % 1537 ] 1538 ] 1539 [#H1 #H2 % #ABS destruct(ABS)  #H1 #H2 % #ABS destruct(ABS)] 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 1540 1776 ] 1541 [ 2,4: @hide_prf % [2,4 : @(proj2 … prf)] % [2,4 : @(proj2 … (proj1 … prf))]1542 % [1,3 : @(proj1 … (proj1 … (proj1 … prf)))]1543 whd in match sigma_is_opt; normalize nodelta1544 [ whd in ⊢ (? (??%?)); % #ABS destruct(ABS)]1545 >is_stack_st_spec in wf_is;1546 whd in match sigma_is_opt; normalize nodelta1547 cases(sigma_beval_opt ?????)1548 [ normalize * #ABS @⊥ @ABS %1549  #bev #_ normalize % #ABS destruct(ABS)1550 ]1551 ]1552 #prf' #acca_store_commute %{prf'}1553 whd in match sigma_state in ⊢ (??(?????(?????%?)?)?);1554 whd in match sigma_is; normalize nodelta1555 @opt_safe_elim #int_stack #int_stack_sigma_spec1556 >is_stack_st_spec in int_stack_sigma_spec;1557 whd in match sigma_is_opt; normalize nodelta1558 #IS_SPEC @('bind_inversion IS_SPEC) IS_SPEC1559 [ #sigma_bv #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)1560  #sigma_bv_not_used #sigma_bv_not_used_spec #IS_SPEC1561 @('bind_inversion IS_SPEC) IS_SPEC1562 #sigma_bv #sigma_bv_spec #EQ whd in EQ : (??%%); destruct(EQ)]1563 normalize nodelta >m_return_bind1564 <acca_store_commute1565 whd in match helper_def_store; whd in match acca_store;1566 whd in match sigma_beval; normalize nodelta1567 @opt_safe_elim #xx #xx_spec1568 [ >xx_spec in sigma_bv_spec; #EQ destruct(EQ) //1569  cut(xx =sigma_bv) [>xx_spec in sigma_bv_spec; #EQ destruct(EQ) %]1570 #EQ >EQ @m_bind_ext_eq #reg1571 change with (return set_regs (make_sem_lin_params p p') ?1572 (set_istack (make_sem_lin_params p p') ? ?) = ?);1573 >(set_istack_sigma_commute ?????? (one_is Bv_not_used) (one_is sigma_bv_not_used) ???)1574 [2: whd in match sigma_is_opt; normalize nodelta >sigma_bv_not_used_spec1575 >m_return_bind whd in ⊢ (??%%); %  % ]1576 ]1577 1777  (* PUSH *) 1578 #a #H @('bind_inversion H) H 1579 #val #graph_ret_spec 1580 change with (((push (make_sem_graph_params p p') ? ?) = ?) → ?) 1581 #graph_push_spec 1582 elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf graph_ret_spec) 1583 #val_wf #acca_arg_retrieve_commute 1584 whd in match push in graph_push_spec; normalize nodelta in graph_push_spec; 1585 @('bind_inversion graph_push_spec) graph_push_spec 1586 #int_stack #int_stack_spec #EQ whd in EQ : (??%%); destruct(EQ) 1587 % 1588 [ @hide_prf % [% [% [ @(proj1 … (proj1 … (proj1 … prf))) ]]] 1589 [2: @(proj2 … (proj1 … prf))] [2: @(proj2 … prf)] 1590 lapply int_stack_spec int_stack_spec 1591 cases int_stack 1592 [ whd in match is_push; normalize nodelta 1593 cases(istack ? ?) normalize nodelta 1594 [2: #x ] [3: #x #y] #EQ whd in EQ : (??%%); destruct(EQ) 1595 2,3: [#x  #y #x ] whd in match is_push; normalize nodelta 1596 inversion(istack ? ?) normalize nodelta 1597 [ #_ #EQ whd in EQ : (??%%); destruct(EQ) 1598 whd in match sigma_is_opt; normalize nodelta 1599 inversion(sigma_beval_opt ?????) 1600 [ #EQ @⊥ elim val_wf #H @H // 1601  #z #_ >m_return_bind % #ABS whd in ABS : (??%?); destruct(ABS) 1602 ] 1603  #x #_ #ABS whd in ABS : (??%%); destruct(ABS) 1604  #x #y #_ #ABS whd in ABS : (???%); destruct(ABS) 1605  #_ #ABS whd in ABS : (??%%); destruct(ABS) 1606  #z #H #EQ whd in EQ : (??%%); destruct(EQ) 1607 whd in match sigma_is_opt; normalize nodelta 1608 inversion(sigma_beval_opt ???? y) 1609 [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf))) 1610 whd in match sigma_is_opt; >H normalize nodelta >ABS 1611 whd in ⊢ ((?(??%?))→?); * #h1 @h1 % 1612  #sigma_y #H >m_return_bind 1613 cases (sigma_beval_opt ? ? ? ? x) in val_wf; [ * #ABS @⊥ @ABS %] 1614 #sigma_y' #_ >m_return_bind whd in ⊢ (?(??%?)); % #H destruct(H) 1615 ] 1616  #a1 #a2 #_ #EQ whd in EQ : (???%); destruct(EQ) 1617 ] 1618 ] 1619  change with (acca_arg_retrieve ????? = ?) in acca_arg_retrieve_commute; 1620 >acca_arg_retrieve_commute in ⊢ (??%?); >m_return_bind 1621 elim(is_push_sigma_commute … (proj2 … (proj1 …(proj1 … prf))) val_wf int_stack_spec) 1622 #wf_is #EQ whd in match push; normalize nodelta >EQ % 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 ] 1623 1786 ] 1624 1787  (*C_ADDRESS*) … … 1628 1791 change with ((dpl_reg p) → ?) #dpl 1629 1792 change with ((dph_reg p) → ?) #dph 1630 change with ((( ! st1 ← dpl_store p 1631 (joint_closed_internal_function (make_sem_graph_params p p')) 1632 ? 1633 ? 1634 ? 1635 ? ; ? ) = ?) → ?) 1636 change with ((( ! st1 ← dpl_store ???? 1637 (BVptr 1638 (mk_pointer 1639 (opt_safe block 1640 (find_symbol 1641 (fundef 1642 (joint_closed_internal_function 1643 (make_sem_graph_params p p') 1644 ? 1645 ) 1646 ) 1647 (globalenv_noinit ? graph_prog) 1648 ? 1649 ) 1650 ? 1651 ) 1652 ? 1653 ) 1654 ? 1655 ) ? ; ?) = ?) → ?) 1656 change with ((( ! st1 ← ? ; 1657 dph_store p (joint_closed_internal_function (make_sem_graph_params p p')) 1658 ? ? 1659 (BVptr 1660 (mk_pointer 1661 (opt_safe block 1662 (find_symbol 1663 (fundef 1664 (joint_closed_internal_function 1665 (make_sem_graph_params p p') 1666 ? 1667 ) 1668 ) 1669 (globalenv_noinit ? graph_prog) 1670 ? 1671 ) 1672 ? 1673 ) 1674 ? 1675 ) 1676 ? 1677 ) ?) = ?) → ?) 1678 #H @('bind_inversion H) H 1679 #st1 #dpl_st1 1680 elim(store_commute p p' graph_prog sigma ?? gss (dpl_store_commute … gss) ???? prf ? dpl_st1) 1681 [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); % 1682 #ABS destruct(ABS)] 1683 #wf_st1 whd in match helper_def_store; normalize nodelta 1684 #H @('bind_inversion H) H #reg1 #reg1_spec #EQ whd in EQ : (??%%); 1685 destruct(EQ) EQ 1686 #dph_st' 1687 elim(store_commute p p' graph_prog sigma ?? gss (dph_store_commute … gss) ???? wf_st1 ? dph_st') 1688 [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta whd in ⊢ (?(??%?)); 1689 % #ABS destruct(ABS)] 1690 #wf_st' whd in match helper_def_store; normalize nodelta 1691 #H @('bind_inversion H) H #reg2 #reg2_spec #EQ whd in EQ : (??%%); 1692 destruct(EQ) EQ %{wf_st'} <e1 1693 whd in match dpl_store; normalize nodelta 1694 whd in match sigma_beval in reg1_spec; normalize nodelta in reg1_spec; 1695 whd in match sigma_beval_opt in reg1_spec; normalize nodelta in reg1_spec; 1696 lapply reg1_spec reg1_spec @opt_safe_elim #x #EQ whd in EQ : (??%?); 1697 destruct(EQ) @opt_safe_elim #block_graph #block_graph_spec 1698 #reg1_spec @opt_safe_elim #block_lin #block_lin_spec 1699 cut(find_symbol 1700 (fundef 1701 (joint_closed_internal_function 1702 (make_sem_lin_params p p') 1703 (prog_var_names (joint_function (mk_lin_params p)) ℕ (linearise … graph_prog)) 1704 ) 1705 ) 1706 (globalenv_noinit (joint_function (mk_lin_params p)) (linearise … graph_prog)) 1707 sy 1708 = 1709 find_symbol 1710 (fundef 1711 (joint_closed_internal_function 1712 (make_sem_graph_params p p') 1713 (prog_var_names (joint_function (mk_graph_params p)) ℕ graph_prog) 1714 ) 1715 ) 1716 (globalenv_noinit (joint_function (mk_graph_params p)) graph_prog) 1717 sy) 1718 [ @find_symbol_transf] 1719 #find_sym_EQ >find_sym_EQ in block_lin_spec; >block_graph_spec 1720 #EQ destruct(EQ) >reg1_spec >m_return_bind 1721 whd in match dph_store; normalize nodelta 1722 lapply reg2_spec reg2_spec 1723 whd in match sigma_beval; normalize nodelta 1724 @opt_safe_elim #y 1725 whd in match sigma_beval_opt; normalize nodelta 1726 whd in ⊢((??%?)→?); #EQ destruct(EQ) 1727 @opt_safe_elim #graph_block >block_graph_spec 1728 #EQ destruct(EQ) #reg2_spec 1729 cut(sigma_state p p' graph_prog sigma gss st1 wf_st1 = 1730 (set_regs (lin_prog_params p p' (linearise p graph_prog) stack_sizes) 1731 reg1 (sigma_state p p' graph_prog sigma gss st prf))) 1732 [whd in match set_regs; normalize nodelta >e0 %] 1733 #sigma_st1_spec <sigma_st1_spec >reg2_spec 1734 >m_return_bind % 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 % 1735 1809  (*C_OPACCS*) 1736 #op #a #b #arg1 #arg2 1737 #H @('bind_inversion H) H 1738 #val1 #val1_spec 1739 elim (retrieve_commute p p' graph_prog sigma ?? gss (acca_arg_retrieve_commute … gss)??? prf val1_spec) 1740 #wf_val1 #sigma_val1_commute 1741 #H @('bind_inversion H) H #val2 #val2_spec 1742 elim (retrieve_commute p p' graph_prog sigma ?? gss (accb_arg_retrieve_commute … gss)??? prf val2_spec) 1743 #wf_val2 #sigma_val2_commute 1744 #H @('bind_inversion H) H * 1745 #opaccs1 #opaccs2 #opaccs_spec 1746 elim(beopaccs_sigma_commute p p' graph_prog sigma ????? wf_val1 wf_val2 opaccs_spec) 1747 #wf_opaccs1 * #wf_opaccs2 #be_opaccs_commute 1748 #H @('bind_inversion H) H #st1 #st1_spec 1749 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_opaccs1 st1_spec) 1750 #wf_st1 #sigma_st1_commute #final_spec 1751 elim(store_commute p p' graph_prog sigma ?? gss (accb_store_commute … gss) ???? wf_st1 wf_opaccs2 final_spec) 1752 #wf_st' #sigma_final_commute 1753 %{wf_st'} 1754 whd in match helper_def_retrieve in sigma_val1_commute; 1755 normalize nodelta in sigma_val1_commute; 1756 whd in match acca_arg_retrieve; normalize nodelta 1757 >sigma_val1_commute >m_return_bind 1758 whd in match helper_def_retrieve in sigma_val2_commute; 1759 normalize nodelta in sigma_val2_commute; 1760 whd in match accb_arg_retrieve; normalize nodelta 1761 >sigma_val2_commute >m_return_bind 1762 >be_opaccs_commute >m_return_bind 1763 whd in match helper_def_store in sigma_st1_commute; 1764 normalize nodelta in sigma_st1_commute; 1765 @('bind_inversion sigma_st1_commute) 1766 #reg1 #reg1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1767 whd in match acca_store; normalize nodelta 1768 >reg1_spec >m_return_bind 1769 whd in match set_regs; normalize nodelta >e0 1770 whd in match helper_def_store in sigma_final_commute; 1771 normalize nodelta in sigma_final_commute; 1772 @('bind_inversion sigma_final_commute) 1773 #reg2 #reg2_spec #EQ whd in EQ : (??%%); destruct(EQ) 1774 whd in match accb_store; normalize nodelta 1775 >reg2_spec >m_return_bind whd in match set_regs; normalize nodelta 1776 >e1 % 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 1777 1829  (*C_OP1*) 1778 #op #a #arg #H @('bind_inversion H) H #val1 #val1_spec 1779 elim (retrieve_commute p p' graph_prog sigma ?? ? (acca_retrieve_commute … gss) ??? prf val1_spec) 1780 #wf_val1 #sigma_val1_commute #H @('bind_inversion H) #op_val1 #op_val1_spec 1781 cut(∃ wf_opval1. be_op1 op (sigma_beval … wf_val1) = return sigma_beval p p' graph_prog sigma op_val1 wf_opval1) 1782 [ whd in match be_op1 in op_val1_spec; normalize nodelta in op_val1_spec; 1783 @('bind_inversion op_val1_spec) #bt1 #b1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1784 % [ @hide_prf whd in match sigma_beval_opt; normalize nodelta % #ABS whd in ABS : (??%?); 1785 destruct(ABS)] 1786 whd in match Byte_of_val in b1_spec; normalize nodelta in b1_spec; 1787 whd in match sigma_beval; normalize nodelta 1788 @opt_safe_elim #sigma_val1 #sigma_val1_spec 1789 @opt_safe_elim #sigma_op_val1 #sigma_op_val1_spec 1790 cases(val1) in b1_spec op_val1_spec sigma_val1_spec; normalize nodelta 1791 [4: #bt2 #EQ whd in EQ : (???%); destruct(EQ) 1792 whd in match Byte_of_val; normalize nodelta >m_return_bind 1793 #EQ whd in EQ : (??%%); destruct(EQ) 1794 whd in match sigma_beval_opt; normalize nodelta 1795 #EQ whd in EQ : (??%%); destruct(EQ) 1796 whd in match sigma_beval_opt in sigma_op_val1_spec; 1797 normalize nodelta in sigma_op_val1_spec; whd in sigma_op_val1_spec : (??%?); 1798 destruct(sigma_op_val1_spec) // 1799 *: [3: #pt1 #pt2 #p] [4:#p] [5:#pt #p] [6:#pc #p] #ABS whd in ABS : (???%); 1800 destruct(ABS) 1801 ] 1802 ] * #wf_op_val1 #sigma_op_val1_commute #H1 1803 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_op_val1 H1) 1804 #wf_st' #final_commute %{wf_st'} 1805 change with (acca_retrieve ????? = ?) in sigma_val1_commute; 1806 >sigma_val1_commute >m_return_bind >sigma_op_val1_commute >m_return_bind 1807 assumption 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 1808 1839  (*C_OP2*) 1809 #op #a #arg1 #arg2 #H @('bind_inversion H) H 1810 @bv_pc_other (*val1*) 1811 [ #pc_val1 #part_val1 1812  #val1 #val1_no_pc 1813 ] #val1_spec 1814 #H @('bind_inversion H) H 1815 [ #val2 1816  @bv_pc_other (*val2*) 1817 [ #pc_val2 #part_val2 1818  #val2 #val2_no_pc 1819 ] 1820 ] #val2_spec 1821 #H @('bind_inversion H) H * #val3 #bit1 1822 [1,2: [2: cases val1 [#pt1 #pt2 #p#by#p#pt #p#pc #p] cases op ] 1823 whd in ⊢(??%%→?); #EQ destruct(EQ) ] 1824 #H cut (bv_no_pc val3) 1825 [ lapply H H 1826 whd in match be_op2; normalize nodelta 1827 cases val1 normalize nodelta 1828 [1,7: [2: #pc #p] #ABS whd in ABS : (???%); destruct(ABS) 1829 2,3,5: [ #pt1 #pt2 #p  #p ] cases op normalize nodelta 1830 [1,2,3,4,6,7,8,9,10,12,13,14,15,16,17 : #ABS whd in ABS : (???%); destruct(ABS)] 1831 cases val2 normalize nodelta 1832 [1,2,3,4,5,6,7,8,9,12,13,14,15,16,17,18,21 : 1833 [#ptr1 #ptr2 #p #byte2  #p  #ptr #p  #pc #p    #p #ptr #p  #pc #p    #pt1 #pt2 #p  #bt  #pc #p] 1834 #EQ whd in EQ : (??%%); destruct(EQ) // 1835  #pt3 #pt4 #p1 @if_elim [2: #_ #ABS whd in ABS : (??%%); destruct(ABS)] 1836 #_ @if_elim #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1837  #bt @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)] 1838 #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1839  #p3 @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)] 1840 #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1841  #ptt #part @if_elim [2: #_ #ABS whd in ABS : (???%); destruct(ABS)] 1842 #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1843 ] 1844 4,6: [ #bt1  #ptr #p] cases val2 normalize nodelta 1845 [1,3,4,5,7,8,9,10,14: [#pt1 #pt2 #p 1846  #bt2 #H @('bind_inversion H) #bit #bit_spec cases(op2 ? ? ? ? ?) 1847 #x #y normalize nodelta 1848  #p  #pc #part    #ptr #ptr' #p #pc #p] 1849 #EQ whd in EQ : (??%%); destruct(EQ) // 1850 *: [#ptr #p #bt  #p  #ptr #p ] cases op normalize nodelta 1851 [1,2,3,4,5,6,9,10,11,12,16,17,18,19,20,21,22,23,25,26,28,29: 1852 #EQ whd in EQ : (??%%); destruct(EQ) // 1853 7,8,13,14,15: whd in match be_add_sub_byte; normalize nodelta 1854 cases(ptype ?) normalize nodelta [2,4,6,8,10: #ABS whd in ABS : (??%%); destruct(ABS)] 1855 cases p * normalize nodelta #n_part_spec [2,6: #_ #ABS whd in ABS : (??%%); destruct(ABS)] 1856 [1,2,4,5,7 : #H @('bind_inversion H) #bit #bit_spec 1857 @if_elim [1,3,5,7,9: #_ #ABS whd in ABS : (??%%); destruct(ABS)] 1858 #_ elim(op2 ? ? ? ? ?) #a1 #a2 normalize nodelta 1859 #EQ whd in EQ : (??%%); destruct(EQ) // 1860 *: #_ cases(carry ? st) normalize nodelta 1861 [1,2,4,5,7,8 : [1,3,5: #bool ] #ABS whd in ABS : (???%); destruct(ABS)] 1862 #bool #pt #p1 #bitvect @if_elim #_ [2,4,6: #ABS whd in ABS : (???%); destruct(ABS)] 1863 @If_elim [2,4,6: #_ #ABS whd in ABS : (???%); destruct(ABS)] 1864 #proof elim(op2_bytes ?????) #a #b 1865 normalize nodelta #EQ whd in EQ : (???%); destruct(EQ) // 1866 ] 1867 24,30: @if_elim #_ #EQ whd in EQ : (??%%); destruct(EQ) // 1868  cases(ptype ?) normalize nodelta [2: #ABS whd in ABS : (???%); destruct(ABS)] 1869 @if_elim #_ [2: #ABS whd in ABS : (??%%); destruct(ABS)] 1870 #H @('bind_inversion H) #b #_ elim(op2 ?????) #x #y normalize nodelta 1871 #EQ whd in EQ : (??%%); destruct(EQ) // 1872 ] 1873 ] 1874 ] 1875 ] #val3_spec lapply H H #val3_op_spec #H @('bind_inversion H) #st1 1876 #st1_spec #EQ whd in EQ : (??%%); destruct(EQ) 1877 elim(retrieve_commute p p' graph_prog sigma ?? ? (acca_arg_retrieve_commute … gss) ??? prf val1_spec) 1878 #wf_val1 #sigma_val1_commute 1879 elim(retrieve_commute p p' graph_prog sigma ?? ? (snd_arg_retrieve_commute … gss) ??? prf val2_spec) 1880 #wf_val2 #sigma_val2_commute 1881 1882 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf ? st1_spec) 1883 [2: @hide_prf whd in match sigma_beval_opt; normalize nodelta inversion val3 normalize nodelta 1884 [7: #pc #p #H >H in val3_spec; #ABS @⊥ // 1885 *: [#pt1 #pt2 #p#bt#p#pt #p] #_ % #ABS whd in ABS : (??%%); destruct(ABS) 1886 ] 1887 ] 1888 #wf_st1 #sigma_st1_commute 1889 % 1890 [ @hide_prf % [2: @(proj2 … wf_st1)] % [2: @(proj2 … (proj1 … wf_st1))] 1891 % [2:@(proj2 … (proj1 … (proj1 … wf_st1)))] 1892 @(proj1 … (proj1 … (proj1 … wf_st1))) 1893 ] 1894 change with ((acca_arg_retrieve ?????)=?) in sigma_val1_commute; 1895 >sigma_val1_commute >m_return_bind 1896 change with ((snd_arg_retrieve ?????)=?) in sigma_val2_commute; 1897 >sigma_val2_commute >m_return_bind 1898 >(sigma_bv_no_pc … val1_no_pc) >(sigma_bv_no_pc … val2_no_pc) 1899 whd in match sigma_state in ⊢ (??(?????%?)?); normalize nodelta 1900 >val3_op_spec >m_return_bind 1901 change with ((acca_store ??????) = ?) in sigma_st1_commute; 1902 >(sigma_bv_no_pc … val3_spec) in sigma_st1_commute; 1903 #H >H >m_return_bind // 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 1904 1855  (*C_CLEAR_CARRY*) 1905 #EQ whd in EQ : (??%%); destruct(EQ) 1906 %{prf} // 1856 #st #prf @mfr_return 1907 1857  (*C_SET_CARRY*) 1908 # EQ whd in EQ : (??%%); destruct(EQ) %{prf} //1858 #st #prf @mfr_return 1909 1859  (*C_LOAD*) 1910 #a #dpl #dph #H @('bind_inversion H) H #val1 #val1_spec 1911 #H @('bind_inversion H) H #val2 #val2_spec 1912 #H @('bind_inversion H) H #ptr #ptr_spec 1913 #H @('bind_inversion H) H #val3 #val3_spec #final_spec 1914 elim(retrieve_commute p p' graph_prog sigma ?? ? (dph_arg_retrieve_commute … gss) ??? prf val1_spec) 1915 #wf_val1 #sigma_val1_commute 1916 elim(retrieve_commute p p' graph_prog sigma ?? ? (dpl_arg_retrieve_commute … gss) ??? prf val2_spec) 1917 #wf_val2 #sigma_val2_commute 1918 lapply(opt_eq_from_res ???? val3_spec) val3_spec #val3_spec 1919 elim(beloadv_sigma_commute p p' graph_prog sigma ???? val3_spec) 1920 [2: @hide_prf @(proj2 … prf)] #wf_val3 #sigma_val3_commute 1921 elim(store_commute p p' graph_prog sigma ?? gss (acca_store__commute … gss) ???? prf wf_val3 final_spec) 1922 #wf_st' #sigma_st_commute %{wf_st'} 1923 change with (dph_arg_retrieve ????? = ?) in sigma_val1_commute; 1924 >sigma_val1_commute >m_return_bind 1925 change with (dpl_arg_retrieve ????? = ?) in sigma_val2_commute; 1926 >sigma_val2_commute >m_return_bind 1927 >(sigma_ptr_commute p p' graph_prog sigma … ptr_spec) 1928 >m_return_bind >sigma_val3_commute >m_return_bind 1929 change with (acca_store ?????? = ?) in sigma_st_commute; assumption 1930  (*C_STORE*) 1931 #dpl #dph #a #H @('bind_inversion H) H #val1 #val1_spec 1932 #H @('bind_inversion H) H #val2 #val2_spec 1933 #H @('bind_inversion H) H #ptr #ptr_spec 1934 #H @('bind_inversion H) H #val3 #val3_spec 1935 #H @('bind_inversion H) H #mem #mem_spec #EQ whd in EQ : (??%%); destruct(EQ) 1936 elim(retrieve_commute p p' graph_prog sigma ?? ? (dph_arg_retrieve_commute … gss) ??? prf val1_spec) 1937 #wf_val1 #sigma_val1_commute 1938 elim(retrieve_commute p p' graph_prog sigma ?? ? (dpl_arg_retrieve_commute … gss) ??? prf val2_spec) 1939 #wf_val2 #sigma_val2_commute 1940 elim(retrieve_commute p p' graph_prog sigma ?? ? (acca_arg_retrieve_commute … gss) ??? prf val3_spec) 1941 #wf_val3 #sigma_val3_commute 1942 lapply(opt_eq_from_res ???? mem_spec) mem_spec #mem_spec 1943 elim(bestorev_sigma_commute p p' graph_prog sigma ????? wf_val3 mem_spec) 1944 [2: @hide_prf @(proj2 … prf)] 1945 #wf_mem #sigma_mem_commute 1946 % [@hide_prf % [2: @wf_mem] % [2: @(proj2 … (proj1 … prf))] % 1947 [ @(proj1 … (proj1 … (proj1 … prf)))  @(proj2 … (proj1 … (proj1 … prf)))] 1948 ] 1949 change with (dph_arg_retrieve ????? = ?) in sigma_val1_commute; 1950 >sigma_val1_commute >m_return_bind 1951 change with (dpl_arg_retrieve ????? = ?) in sigma_val2_commute; 1952 >sigma_val2_commute >m_return_bind 1953 >(sigma_ptr_commute p p' graph_prog sigma … ptr_spec) 1954 >m_return_bind 1955 change with (acca_arg_retrieve ????? = ?) in sigma_val3_commute; 1956 >sigma_val3_commute >m_return_bind >sigma_mem_commute 1957 >m_return_bind // 1958  (*CALL*) 1959 #f #args #dest 1960 #EQ whd in EQ : (??%%); destruct(EQ) %{prf} // 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 1961 1896  (*C_EXT*) 1962 #s_ext #H 1963 elim(eval_ext_seq_commute … sigma gss … prf H) 1964 #wf_st' #H1 %{wf_st'} >H1 // 1897 #s_ext #st #prf @eval_ext_seq_commute 1965 1898 ] 1966 skip1967 1899 qed. 1968 (* check(save_frame_commute)*)1969 1970 lemma eval_statement_no_pc_sigma_commute :1971 ∀p,p',graph_prog.1972 let lin_prog ≝ linearise p graph_prog in1973 ∀stack_sizes.1974 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma.1975 ∀f,fn,st,stmt,st'.1976 ∀prf : well_formed_state … gss st.1977 eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes))1978 f fn stmt st = return st' →1979 ∃prf'.1980 eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes))1981 f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt)1982 (sigma_state … gss st prf) =1983 return sigma_state … gss st' prf'.1984 #p #p' #graph_prog #stack_sizes #sigma #gss1985 #f #fn #st * [* [ #stmt  #a #lbl ] #nxt  * [ #lbl   #fl #called #args ]]1986 #st' #prf1987 whd in match eval_statement_no_pc; normalize nodelta1988 [ @eval_seq_no_pc_sigma_commute1989 *: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} %1990 ]1991 qed.1992 1993 1900 1994 1901 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ … … 2034 1941 * #wf_prf #st2_EQ 2035 1942 2036 cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt) 2037 * #EQfetch_stmt' #all_labels_in 2038 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 2039 1961 letin lin_prog ≝ (linearise … graph_prog) 2040 1962 lapply (refl … (eval_state … (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2)) 2041 1963 whd in match eval_state in ⊢ (???%→?); 2042 1964 >st2_EQ in ⊢ (???%→?); normalize nodelta 2043 >EQfetch_stmt' in ⊢ (%→?); >m_return_bind in ⊢ (???%→?); 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 2044 2052 cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?; 2045 2053 #wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?); … … 2049 2057 normalize nodelta 2050 2058 2051 cases stmt in ex ex_advance; stmt whd in match graph_to_lin_statement;2052 2059 normalize nodelta 2053 2060 [ whd in match joint_classify_step; @cond_call_other
Note: See TracChangeset
for help on using the changeset viewer.