Changeset 2590 for src/ERTLptr/ERTLtoERTLptrOK.ma
 Timestamp:
 Jan 24, 2013, 7:52:38 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLtoERTLptrOK.ma
r2570 r2590 1 1 2 (**************************************************************************) 2 3 (* ___ *) … … 19 20 include "common/ExtraMonads.ma". 20 21 22 axiom getLocalsFromId : ident → list register. 23 21 24 definition ERTL_status ≝ 22 25 λprog : ertl_program.λstack_sizes. … … 27 30 joint_abstract_status (mk_prog_params ERTLptr_semantics prog stack_sizes). 28 31 29 definition sigma_map ≝ λ prog : ertl _program.30 joint_closed_internal_function ERTL (prog_var_names … prog) → label → option label.32 definition sigma_map ≝ λ prog : ertlptr_program. 33 joint_closed_internal_function ERTLptr (prog_var_names … prog) → label → option label. 31 34 32 35 definition sigma_pc_opt : 33 ∀ prog : ertl _program.36 ∀ prog : ertlptr_program. 34 37 sigma_map prog → program_counter → option program_counter ≝ 35 38 λprog,sigma,pc. … … 43 46 ERTLptr_semantics (pc_block pc) ertl_ptr_point. 44 47 45 definition well_formed_pc ≝ 46 λprog,sigma,pc.sigma_pc_opt prog sigma pc ≠ None ?. 47 48 definition sigma_pc ≝ 49 λprog,sigma,pc.λprf : well_formed_pc prog sigma pc. opt_safe … prf. 50 51 definition sigma_beval _opt:52 ∀prog : ertl _program.48 49 definition sigma_stored_pc ≝ 50 λprog,sigma,pc. match sigma_pc_opt prog sigma pc with 51 [None ⇒ null_pc  Some x ⇒ x]. 52 53 54 definition sigma_beval : 55 ∀prog : ertlptr_program. 53 56 sigma_map prog → 54 beval → optionbeval ≝57 beval → beval ≝ 55 58 λprog,sigma,bv. 56 59 match bv with 57 [ BVpc pc prt ⇒ ! pc' ← sigma_pc_opt prog sigma pc ; return BVpc pc' prt 58  _ ⇒ return bv 60 [ BVpc pc prt ⇒ match sigma_pc_opt prog sigma pc with 61 [None ⇒ BVundef  Some x ⇒ BVpc x prt] 62  _ ⇒ bv 59 63 ]. 60 64 65 (* 61 66 definition sigma_beval : 62 67 ∀prog,sigma,bv. 63 68 sigma_beval_opt prog sigma bv ≠ None ? → beval ≝ 64 69 λprog,sigma,bv.opt_safe …. 65 66 definition sigma_is _opt:67 ∀prog : ertl _program.70 *) 71 definition sigma_is : 72 ∀prog : ertlptr_program. 68 73 sigma_map prog → 69 internal_stack → optioninternal_stack ≝74 internal_stack → internal_stack ≝ 70 75 λprog,sigma,is. 71 76 match is with 72 [ empty_is ⇒ returnempty_is73  one_is bv ⇒ ! bv' ← sigma_beval_opt … sigma bv ; return one_is bv'77 [ empty_is ⇒ empty_is 78  one_is bv ⇒ one_is (sigma_beval prog sigma bv) 74 79  both_is bv1 bv2 ⇒ 75 ! bv1' ← sigma_beval_opt … sigma bv1 ; 76 ! bv2' ← sigma_beval_opt … sigma bv2 ; 77 return both_is bv1' bv2' 80 both_is (sigma_beval prog sigma bv1) (sigma_beval prog sigma bv2) 78 81 ]. 79 82 80 definition sigma_is : 81 ∀prog,sigma,is. 82 sigma_is_opt prog sigma is ≠ None ? → internal_stack ≝ 83 λprog,sigma,is.opt_safe …. 83 lemma sigma_is_empty : ∀prog,sigma. 84 sigma_is prog sigma empty_is = empty_is. 85 #prog #sigma % 86 qed. 87 88 (* 89 lemma sigma_is_pop_commute : 90 ∀prog,sigma,is,bv,is'. 91 is_pop (sigma_is prog sigma is) = 92 return 〈sigma_beval prog sigma bv,sigma_is prog sigma is'〉 → 93 is_pop is = return 〈bv,is'〉. 84 94 85 lemma sigma_is_empty : ∀prog,sigma. 86 ∀prf.sigma_is prog sigma empty_is prf = empty_is. 87 #prog #sigma #prf whd in match sigma_is; normalize nodelta 88 @opt_safe_elim #is' whd in ⊢ (??%%→?); #EQ destruct(EQ) % qed. 89 90 lemma sigma_is_pop_commute : 91 ∀prog,sigma,is. 95 92 96 ∀prf : sigma_is_opt prog sigma is ≠ None ?. 93 97 res_preserve … … … 122 126 ∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b → 123 127 sigma_beval_opt prog sigma (contents (blocks m b) z) ≠ None ?. 124 128 *) 125 129 126 130 127 131 definition sigma_mem : 128 ∀prog,sigma,m. 129 well_formed_mem prog sigma m → 130 bemem ≝ 131 λprog,sigma,m,prf. 132 ∀prog : ertlptr_program . sigma_map prog → bemem → bemem ≝ 133 λprog,sigma,m. 132 134 mk_mem 133 135 (λb. … … 137 139 mk_block_contents l h 138 140 (λz.If Zleb l z ∧ Zltb z h then with prf'' do 139 sigma_beval prog sigma (contents (blocks m b) z) ?141 sigma_beval prog sigma (contents (blocks m b) z) 140 142 else BVundef) 141 143 else empty_block OZ OZ) 142 144 (nextblock m) 143 145 (nextblock_pos m). 146 (* 144 147 @hide_prf 145 148 lapply prf'' lapply prf' prf' prf'' … … 150 153 #zh #zl * @(prf … bid_ok zl zh) 151 154 qed. 152 155 *) 153 156 154 157 (*DOPPIONI DEI CORRISPONDENTI LEMMI IN LINEARISE_PROOF.MA *) 155 lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false.158 (*lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false. 156 159 ** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed. 160 *) 157 161 158 162 axiom mem_ext_eq : … … 163 167 ∀z.contents bc1 z = contents bc2 z) → 164 168 nextblock m1 = nextblock m2 → m1 = m2. 169 170 (* 165 171 166 172 lemma beloadv_sigma_commute: … … 295 301 qed. 296 302 303 lemma ext_map_inf_eq : ∀A , B : Type[0]. 304 ∀ m : positive_map A. 305 ∀ F, F' : (∀a:A.(Σp:Pos. lookup_opt A p m = Some ? a) → B). 306 (∀a',id',id'',prf,prf'. F a' «id',prf» = F' a' «id'',prf'») → 307 map_inf A B m F = map_inf A B m F'. 308 #A #B #m elim m [#F #F' #eqFF' %] * [2:#a] normalize nodelta #l #r #Hl #Hr #F #F' 309 #eqFF' normalize [>(eqFF' a one one (refl ? (Some A a)) (refl ? (Some A a)))] 310 @eq_f2 [1,3: @Hl *: @Hr] #a' #id' #id'' #prf' #prf'' @eqFF' 311 qed. 312 313 314 lemma map_inf_add : ∀ A, B : Type[0]. 315 ∀tag : String. 316 ∀m: identifier_map tag A. 317 ∀F :(∀a:A.(Σid. lookup tag A m id = Some A a) → B). 318 ∀a,id. 319 let m' ≝ (add tag A m id a) in 320 ∀F' :(∀a:A.(Σid. lookup tag A m' id = Some A a) → B). 321 (∀a',id',id'',prf,prf'. F a' «id',prf» = F' a' «id'',prf'») → 322 ∃ prf. 323 map_inf1 A B tag m' F' = 324 add tag B (map_inf1 A B tag m F) id (F' a «id,prf»). 325 #A #B #tag #m #F #a #id normalize nodelta #F' #eqFF' % 326 [@hide_prf @(lookup_add_hit tag A m ? ?)] 327 lapply eqFF' eqFF' lapply F' F' lapply id id lapply a a lapply F F 328 cases m m #m elim m 329 [ #F #a * #id elim id [#F' #eqFF' %] #x #Hx #F' #eqFF' whd in ⊢ (??%%); 330 normalize nodelta @eq_f whd in match insert; normalize nodelta 331 whd in ⊢ (??%%); normalize nodelta @eq_f2 try % 332 lapply(Hx ??) 333 [2,5: #a1 ** #id1 #prf1 @F' [1,3: @a1] 334 [%{(an_identifier tag (p1 id1))} %{(an_identifier tag (p0 id1))}] @prf1 335 1,4: #a' * #id' * #id'' #prf #prf' normalize nodelta @eqFF' 336 *: normalize nodelta whd in ⊢ (??%% → ?); normalize nodelta #EQ destruct(EQ) 337 lapply e0 e0 whd in ⊢ (??%% → ?); normalize nodelta normalize in ⊢ (??(???%?)? → ?); 338 #EQ <EQ % 339 ] 340  #opt_a #l1 #r1 #Hl1 #Hr1 #F #a ** [*: #x] #F' #eqFF' 341 [ normalize @eq_f @eq_f2 @ext_map_inf_eq #a' #id' #id'' #prf' #prf'' >eqFF' [1,4:%*:] 342 *: normalize @eq_f lapply eqFF' eqFF' lapply F' F' lapply F F cases opt_a 343 [2,4: #a1] normalize nodelta #F #F' #eqFF' 344 [3,4: @eq_f2*: >(eqFF' a1 (an_identifier tag one) (an_identifier tag one) 345 (refl (option A) (Some A a1)) (refl (option A) (Some A a1))) 346 @eq_f2] 347 [1,4,5,8: @ext_map_inf_eq #a' #id' #id'' #prf' #prf'' >eqFF' [1,4,7,10:%*:] 348 2,6: lapply (Hr1 ? a (an_identifier tag x) ? ?) 349 *: lapply (Hl1 ? a (an_identifier tag x) ? ?) 350 ] 351 [2,3,6,7,10,11,14,15: #a ** #id #prf [2,4,6,8: @F *: @F'] try @a % 352 [1,3,9,11: % @(p1 id) 5,7,13,15: % @(p0 id) *: @hide_prf <prf %] 353 1,5,9,13: #a * #id' * #id'' #prf #prf' normalize nodelta @eqFF' 354 *: normalize in ⊢ (%→ ?); #EQ destruct(EQ) >e0 % 355 ] 356 ] 357 ] 358 qed. 359 *) 360 361 297 362 inductive id_is_in (A : Type[0]) : Pos → positive_map A → Prop ≝ 298 363  is_in_root : ∀l,r,opt_a. id_is_in A (one) (pm_node … opt_a l r) … … 308 373 [an_id_map p ⇒ id_is_in A x p] 309 374 ]. 310 375 (* 311 376 lemma lookup_map : ∀A,B : Type[0]. 312 377 ∀tag : String. … … 355 420 qed.*) 356 421 422 *) 357 423 358 424 lemma lookup_eq : ∀ A : Type[0]. … … 387 453 qed. 388 454 389 lemma update_lookup_previous : ∀ A : Type[0]. 455 include alias "common/Identifiers.ma". 456 include alias "common/PositiveMap.ma". 457 458 459 lemma p0_neq_one : ∀x: Pos. p0 x ≠ one. 460 #x /3/ 461 qed. 462 463 lemma p1_neq_one : ∀x: Pos. p1 x ≠ one. 464 #x /3/ 465 qed. 466 467 lemma lookup_ok_to_update : ∀ A : Type[0]. 390 468 ∀ tag : String. 391 469 ∀m,m' : identifier_map tag A. ∀id,a. 392 update tag A m id a = return m' ↔ 393 (lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧ 470 (lookup tag A m' id = Some ? a) → lookup tag A m id ≠ None ? → 394 471 (∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧ 395 (id_is_in A tag m id' ↔ id_is_in A tag m' id')). 396 #A #tag * #m * #m' * #id #a % 397 [ whd in ⊢ (??%% → ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct] 398 #m1 #m1_spec #EQ destruct % [%] 399 [ normalize @(update_lookup_opt_same … m1_spec) 400 3: * #id' * #id_spec' normalize % 401 [@(update_lookup_opt_other … m1_spec ??) % #EQ @id_spec' >EQ %] 402 lapply id_spec' lapply m1_spec id_spec' m1_spec 403 (*cases id [*:#x] id normalize*) lapply m' m' lapply id lapply id' id id' 404 elim m [#id' #id #m' cases id [*: #x] normalize #EQ destruct] 405 #opt_a #l #r #Hl #Hr #id' #id #m' cases id [*:#x] id normalize 406 [ cases opt_a [2:#a] normalize #EQ destruct cases id' [#H @⊥ @H %] 407 #x #_ normalize % #H [1,2: %3 *: %2] 408 inversion H #l1 #r1 #opt_a1 409 [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥ 410 [1,2: cut(p1 x ≠ one) [1,3: @(pos_elim … x) /3/] 411 *: cut(p0 x ≠ one) [1,3: @(pos_elim … x) /3/] 412 ] 413 * #H @H >EQ1 // 414 *: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) 415 #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) #_ assumption 416 ] 417 *: inversion(update A x a ?) normalize [1,3: #_ #EQ destruct] #pos_map 418 #pos_map_spec #EQ destruct #id_spec' % #H 419 inversion H #l1 #l2 #opt_a1 420 [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) EQ #EQ 421 #EQ1 lapply(jmeq_to_eq ??? EQ1) EQ1 #EQ1 destruct(EQ1) 422 #H1 % 423 *: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) EQ #EQ 424 #EQ1 lapply(jmeq_to_eq ??? EQ1) EQ1 #EQ1 destruct(EQ1) 425 #H2 try %2 try %3 try assumption 426 [ @(proj1 … (Hr ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %] 427  @(proj2 … (Hr ? ? l2 pos_map_spec ?)) [#EQ1 destruct @id_spec' %] 428  @(proj1 … (Hl ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %] 429  @(proj2 … (Hl ? ? l1 pos_map_spec ?)) [#EQ1 destruct @id_spec' %] 430 ] 431 assumption 432 ] 433 ] 434  % normalize lapply m1_spec lapply id lapply m' id m' elim m 435 [#m' * [*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [*: #x] 436 normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct] 437 inversion (update A x a ?) [1,3: #_ normalize #EQ destruct] 438 #pos_map #EQpos_map normalize #EQ destruct [@Hr@Hl] assumption 439 ] 440  ** normalize in ⊢ (%→%→?); lapply id id lapply m' m' elim m 472 (id_is_in A tag m id' ↔ id_is_in A tag m' id')) → 473 update tag A m id a = return m'. 474 #A #tag * #m * #m' * #id #a 475 normalize in ⊢ (%→%→?); lapply id id lapply m' m' elim m 441 476 [ #m' #id #m_spec' normalize in ⊢ (% → ?); * #EQ @⊥ @EQ %] #opt_a #l #r #Hl #Hr 442 477 #m' * [*: #x] normalize in ⊢ (%→%→?); #m_spec' … … 494 529 ] 495 530 ] 496 ] 497 qed. 531 qed. 532 533 534 lemma update_ok_to_lookup : ∀ A : Type[0]. 535 ∀ tag : String. 536 ∀m,m' : identifier_map tag A. ∀id,a. 537 update tag A m id a = return m' → 538 (lookup tag A m' id = Some ? a) ∧ lookup tag A m id ≠ None ? ∧ 539 (∀ id'. id ≠ id' → (lookup tag A m id' = lookup tag A m' id') ∧ 540 (id_is_in A tag m id' ↔ id_is_in A tag m' id')). 541 #A #tag * #m * #m' * #id #a 542 whd in ⊢ (??%% → ?); inversion(update A ???) normalize nodelta [#_ #ABS destruct] 543 #m1 #m1_spec #EQ destruct % [%] 544 [ normalize @(update_lookup_opt_same … m1_spec) 545 3: * #id' * #id_spec' normalize % 546 [@(update_lookup_opt_other … m1_spec ??) % #EQ @id_spec' >EQ %] 547 lapply id_spec' lapply m1_spec id_spec' m1_spec 548 (*cases id [*:#x] id normalize*) lapply m' m' lapply id lapply id' id id' 549 elim m [#id' #id #m' cases id [*: #x] normalize #EQ destruct] 550 #opt_a #l #r #Hl #Hr #id' #id #m' cases id [*:#x] id normalize 551 [ cases opt_a [2:#a] normalize #EQ destruct cases id' [#H @⊥ @H %] 552 #x #_ normalize % #H [1,2: %3 *: %2] 553 inversion H #l1 #r1 #opt_a1 554 [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥ 555 [1,2: cut(p1 x ≠ one) [1,3: @(pos_elim … x) /3/] 556 *: cut(p0 x ≠ one) [1,3: @(pos_elim … x) /3/] 557 ] 558 * #H @H >EQ1 // 559 *: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) 560 #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1) #_ assumption 561 ] 562 *: inversion(update A x a ?) normalize [1,3: #_ #EQ destruct] #pos_map 563 #pos_map_spec #EQ destruct #id_spec' % #H 564 inversion H #l1 #l2 #opt_a1 565 [1,4,7,10: #EQ lapply(jmeq_to_eq ??? EQ) EQ #EQ 566 #EQ1 lapply(jmeq_to_eq ??? EQ1) EQ1 #EQ1 destruct(EQ1) 567 #H1 % 568 *: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) EQ #EQ 569 #EQ1 lapply(jmeq_to_eq ??? EQ1) EQ1 #EQ1 destruct(EQ1) 570 #H2 try %2 try %3 try assumption 571 [ @(proj1 … (Hr ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %] 572  @(proj2 … (Hr ? ? l2 pos_map_spec ?)) [#EQ1 destruct @id_spec' %] 573  @(proj1 … (Hl ? ? pos_map pos_map_spec ?)) [#EQ1 destruct @id_spec' %] 574  @(proj2 … (Hl ? ? l1 pos_map_spec ?)) [#EQ1 destruct @id_spec' %] 575 ] 576 assumption 577 ] 578 ] 579  % normalize lapply m1_spec lapply id lapply m' id m' elim m 580 [#m' * [*: #x] normalize #EQ destruct] #opt_a #l #r #Hl #Hr #m' * [*: #x] 581 normalize [ cases opt_a [2:#a] normalize #EQ1 #EQ2 destruct] 582 inversion (update A x a ?) [1,3: #_ normalize #EQ destruct] 583 #pos_map #EQpos_map normalize #EQ destruct [@Hr@Hl] assumption 584 ] 585 qed. 586 (* 498 587 499 500 501 (*502 503 504 505 EQ506 lapply H H507 [ lapply l1 l1 elim l508 [#l1 #H lapply (H (an_identifier tag (p0 one)) ?) [% #EQ destruct] *509 normalize in ⊢ (%→?); cases l1 normalize [#_ #_ %] #opt_a #l2 #r2510 #EQ <EQ * #H1 #H2 lapply (H2 ?) [%2 %] #h inversion h #l3 #r3 #opt_a3511 [ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 @⊥ cut(p0 one ≠ one) [@(pos_elim … one) /3/]512 * #H @H >EQ1 //513 *: #pos #H1 #_ #EQ lapply(jmeq_to_eq ??? EQ) #EQ1 destruct(EQ1)514 #EQ lapply(jmeq_to_eq ??? EQ) EQ #EQ1 H destruct(EQ1) #_515 h H2 inversion H1 #l4 #r4 #opt_a4516 [ #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) EQ1 #EQ1 destruct(EQ1)517 *: #pos #H2 #_ #_ #EQ1 lapply(jmeq_to_eq ??? EQ1) EQ1 #EQ1518 destruct(EQ1)519 ]520 ]521 522 EQ1 #EQ1523 [ #_ %524 #opt_a2 #r2 #l2 #H lapply525 526 qed.527 *)528 588 lemma update_lookup_after : ∀ A : Type[0]. 529 589 ∀ tag : String. … … 608 668 qed. 609 669 670 (* 610 671 definition well_formed_register_env : 611 672 ∀prog : ertl_program .∀sigma : (sigma_map prog). … … 613 674 λprog,sigma,psd_reg.∀id,bv. lookup ?? psd_reg id = Some ? bv → 614 675 sigma_beval_opt prog sigma bv ≠ None ?. 615 676 *) 677 *) 678 679 definition map : ∀tag,A,B. identifier_map tag A → (A → B) → identifier_map tag B ≝ 680 λtag,A,B,m,f.match m with 681 [an_id_map p ⇒ an_id_map … (map ?? f p)]. 682 683 lemma lookup_map : ∀A,B : Type[0]. 684 ∀tag : String. 685 ∀m : identifier_map tag A. 686 ∀ f:A → B. 687 ∀ id. 688 lookup tag B (map tag A B m f) id = 689 ! a ← lookup tag A m id; return f a. 690 #A #B #tag * #m #f * #id normalize >lookup_opt_map % 691 qed. 692 693 lemma update_leaf_fail: ∀tag,A,i,v. 694 update tag A (empty_map ??) i v = Error ? [MSG MissingId; CTX … i]. 695 #ta #A ** [*: #x] #v normalize % 696 qed. 697 698 lemma update_def : ∀tag,A,m,i,v. 699 update tag A m i v = 700 match lookup tag A m i with 701 [ Some _ ⇒ OK ? (add tag A m i v) 702  None ⇒ Error ? [MSG MissingId; CTX … i] 703 ]. 704 #tag #A #m #i #v inversion(update tag A m i v) 705 [ #m' #EQm' cases(update_ok_to_lookup ?????? EQm') * #_ 706 #H #_ elim H cases(lookup tag A m i) [#H @⊥ @H %] 707 #x #_ normalize <EQm' lapply EQm' cases i cases m cases m' m m' i 708 normalize #m' #m #i inversion(update A i v m) normalize [#_ #ABS destruct] 709 #m'' #EQm'' #EQ destruct(EQ) @eq_f @eq_f lapply EQm'' EQm'' lapply i i 710 lapply m' m' elim m [#m' * [2,3: #z] normalize #EQ destruct] 711 #opt_a #l #r #Hl #Hr #m' * [2,3: #z] normalize 712 [3: cases opt_a normalize [2: #y] #EQ destruct % 713 *: inversion(update A z v ?) [2,4: #m''] #EQm'' normalize #EQ destruct 714 [<(Hr … EQm'')  <(Hl … EQm'')] % 715 ] 716  #err cases m m cases i i #i #m normalize inversion(update A i v m) [2:#m'] 717 #EQerr normalize #EQ destruct lapply EQerr lapply i elim m 718 [ normalize #x #_ %] #opt_a #l #r #Hl #Hr * [2,3:#z] normalize 719 [3: cases opt_a [2:#w] normalize #EQ destruct % 720 *: inversion(update A z v ?) [2,4: #m'] #EQm' normalize #EQ destruct 721 [lapply(Hr … EQm')  lapply(Hl … EQm')] cases(lookup_opt A z ?) [2,4: #a] 722 normalize #EQ destruct % 723 ] 724 ] 725 qed. 726 727 lemma map_add : ∀tag : String.∀A,B : Type[0].∀ f: A → B.∀m,id,v. 728 map tag A B (add tag A m id v) f = add tag B (map tag A B m f) id (f v). 729 #tag #A #B #f * #m * #id #v normalize @eq_f lapply v v lapply id id elim m 730 [ #id elim id [#v %] #x #IH #id normalize >IH % 731  #opt_a #l #r #Hl #Hr * [2,3: #x #v normalize @eq_f2 %] #v normalize @eq_f2 732 try % [@Hr@Hl] 733 ] 734 qed. 735 736 737 definition restrict : ∀tag.∀A,B. 738 identifier_map tag A → identifier_map tag B → identifier_map tag A ≝ 739 λtag,A,B,m1,m2.an_id_map … 740 (merge A B A (λo,o'.match o' with [None ⇒ None ?  Some _ ⇒ o]) 741 (match m1 with [an_id_map p1 ⇒ p1]) 742 (match m2 with [an_id_map p2 ⇒ p2])). 743 744 interpretation "identifier map restriction" 'intersects a b = (restrict ??? a b). 745 746 unification hint 0 ≔ tag ; R ≟ identifier tag ⊢ list R ≡ list (identifier tag). 747 748 lemma map_update_commute : ∀tag : String.∀A,B : Type[0].∀f : A → B. ∀m,id,v. 749 update tag B (map tag A B m f) id (f v) = 750 !m' ← update tag A m id v; return map tag A B m' f. 751 #tag #A #B #f #m #id #v >update_def >update_def >lookup_map 752 cases (lookup tag A m id) [%] #a >m_return_bind >m_return_bind normalize nodelta 753 whd in ⊢ (???%); @eq_f @sym_eq @map_add 754 qed. 755 756 definition is_leaf ≝ λA.λpm : positive_map A. 757 match pm with [ pm_leaf ⇒ true  _ ⇒ false ]. 758 (* 759 let rec pm_clean A (pm : positive_map A) on pm : positive_map A ≝ 760 match pm with 761 [ pm_leaf ⇒ pm_leaf ? 762  pm_node o l r ⇒ 763 let l' ≝ pm_clean … l in 764 let r' ≝ pm_clean … r in 765 match o with 766 [ Some _ ⇒ pm_node … o l' r' 767  None ⇒ 768 if is_leaf … l' ∧ is_leaf … r' then pm_leaf ? else 769 pm_node … o l' r' 770 ] 771 ]. 772 773 definition clean ≝ λtag,A.λm : identifier_map tag A. 774 match m with [ an_id_map pm ⇒ an_id_map tag A (pm_clean … pm) ]. 775 *) 616 776 617 777 definition sigma_register_env : 618 ∀prog : ertl_program.∀sigma : (sigma_map prog). 619 ∀psd_env : register_env beval. 620 well_formed_register_env prog sigma psd_env → register_env beval ≝ 621 λprog,sigma,psd_env,prf. 622 map_inf1 ?? ? psd_env (λbv,prf1.sigma_beval prog sigma bv ?). 623 @hide_prf @prf cases prf1 #pi1 #H assumption 624 qed. 625 626 778 ∀prog : ertlptr_program.∀sigma : (sigma_map prog). 779 register_env beval → list register → register_env beval ≝ 780 λprog,sigma,psd_env,ids. 781 let m' ≝ map ??? psd_env (λbv.sigma_beval prog sigma bv) in 782 m' ∩ ids. 783 784 (* 627 785 definition well_formed_ertl_psd_env : 628 786 ∀prog : ertl_program. ∀sigma : (sigma_map prog). 629 787 ertl_psd_env → Prop≝ 630 788 λprog,sigma,psd_env.well_formed_register_env prog sigma (psd_regs psd_env). 631 632 definition sigma_ertl_psd_env : 633 ∀prog : ertl_program. ∀ sigma : (sigma_map prog). 634 ∀psd : ertl_psd_env. 635 well_formed_ertl_psd_env prog sigma psd → ertl_psd_env ≝ 636 λprog,sigma,psd_env,prf. 637 mk_ertl_psd_env 638 (sigma_register_env … prf) 639 (need_spilled_no psd_env). 640 789 *) 790 (* 641 791 let rec well_formed_frames 642 792 (prog : ertl_program) (sigma : (sigma_map prog)) … … 646 796  cons a tl ⇒ well_formed_ertl_psd_env prog sigma a ∧ 647 797 well_formed_frames prog sigma tl 648 ]. 649 650 651 let rec sigma_frames (prog : ertl_program) (sigma : (sigma_map prog)) 652 (l : list ertl_psd_env) (prf : well_formed_frames prog sigma l) 653 on l : list ertl_psd_env ≝ 654 (match l with 655 [nil ⇒ λ_ : (l = nil ?) .nil ? 656 cons a tl ⇒ 657 λx : (l = cons ? a tl). 658 (sigma_ertl_psd_env prog sigma a ?):: 659 (sigma_frames prog sigma tl ?) 660 661 ]) (refl ? l). 662 @hide_prf >x in prf; whd in match (well_formed_frames ???); * // 663 qed. 664 798 ]. 799 *) 800 801 802 lemma lookup_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B. 803 ∀i.lookup ?? (a ∩ b) i = if i ∈ b then lookup … a i else None ?. 804 #tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases (lookup_opt B i b) 805 [2: #b] normalize % qed. 806 807 808 (* 809 lemma clean_add : ∀tag,A,m,i,v.clean … (add tag A m i v) = add tag A (clean … m) i v. 810 #tag #A * #m * #i #v normalize @eq_f 811 lapply m m 812 elim i i 813 [ * [%] 814 * [2: #x] #l #r [%] normalize 815 cases (pm_clean A l) normalize // cases (pm_clean A r) // 816 *: #i #IH * normalize 817 [1,3: >IH cases i // ] 818 * [2,4: #x] #l #r normalize 819 [1,2: >IH % ] 820 >IH cases i cases (pm_clean A l) cases (pm_clean A r) normalize // 821 ] 822 qed. 823 824 lemma clean_lookup : ∀tag,A,m,i.lookup … (clean tag A m) i = lookup … m i. 825 #tag #A * #m * #i normalize lapply i i elim m 826 [#i %] * [2: #a] #l #r #Hl #Hr * [2,3,5,6: #x] normalize in ⊢ (???%); 827 [1,3:<Hr2,4:<Hl] normalize try % [3: @if_elim #_ %] 828 cases(pm_clean A l) in Hl; normalize 829 [2: #opt_a1 #l1 #r1 #_ % 830 3: #H cases(pm_clean A r) normalize // 831  #H cases(pm_clean A r) in Hr; normalize // 832  #opt_a1 #l1 #r1 #H cases x normalize // 833 ] 834 qed. 835 836 837 lemma clean_update : ∀tag,A,m,i,v. 838 ! m' ← update tag A m i v; return clean … m' = 839 update tag A (clean … m) i v. 840 #tag #A #m #i #v 841 >update_def >update_def >clean_lookup cases (lookup tag A m i) 842 [ % ] 843 #m' >m_return_bind normalize nodelta >clean_add % 844 qed. 845 *) 846 lemma lookup_eq_id_map : ∀tag : String. ∀ A : Type[0]. 847 ∀m,m' : identifier_map tag A. 848 (∀id. lookup … m id = lookup … m' id 849 ∧ (id_is_in A tag m id ↔ id_is_in A tag m' id)) → m=m'. 850 #tag #A * #m * #m' #H @eq_f @lookup_eq #id lapply(H (an_identifier tag id)) 851 * #H1 #H2 % // assumption 852 qed. 853 854 (* 855 lemma clean_leaf : ∀tag : String . ∀ A : Type[0]. 856 ∀m : identifier_map tag A. (∀ id. lookup … m id = None ?) → 857 clean ?? m = empty_map ??. 858 #tag #A * #m elim m [#_ %] #opt_a #l #r #Hl #Hr #H normalize @eq_f 859 lapply(H (an_identifier tag one)) normalize #EQ >EQ EQ normalize 860 lapply(Hl ?) [2: lapply(Hr ?)] 861 [1,3: * #id [lapply(H (an_identifier tag (p1 id)))  lapply(H (an_identifier tag (p0 id)))] 862 #H assumption 863  normalize #EQ #EQ1 destruct >e0 >e1 normalize % 864 ] 865 qed. 866 *) 867 lemma id_is_in_lookup : ∀tag,A,m,id,v. 868 lookup tag A m id = Some ? v → id_is_in A tag m id. 869 #tag #A * #m * #id #a normalize lapply m m elim id 870 [*: #x #IH] * normalize [1,3,5: #EQ destruct] #opt_a #l #r [ #_ %] #H [%3 %2] 871 @IH assumption 872 qed. 873 (* 874 lemma pm_clean_leaf : ∀ A : Type[0]. 875 ∀m : positive_map A. (∀ id. lookup_opt … id m = None ?) → 876 pm_clean ? m = pm_leaf …. 877 #A #m elim m [ #id %] #opt_a #l #r #Hl #Hr #H normalize lapply(H one) normalize 878 #EQ >EQ normalize >Hl [normalize >Hr [ %]] #id [@(H (p1 id))@(H (p0 id))] 879 qed. 880 881 882 lemma pm_clean_canonic : ∀A,m,n.(∀i.lookup_opt A i m = lookup_opt A i n) → 883 pm_clean ? m = pm_clean ? n. 884 #A #m #n lapply m m elim n 885 [ @pm_clean_leaf ] 886 * [2: #x] #l #r #IHl #IHr * 887 [1,3: #H @sym_eq @pm_clean_leaf #id @sym_eq @H ] #opt #l' #r' #H 888 lapply (H one) normalize in ⊢ (%→?); #EQ destruct 889 whd in ⊢ (??%%); 890 >(IHl l') [1,3: >(IHr r') [1,3 : % ]] #i 891 [1,2: @(H (p1 i)) *: @(H (p0 i)) ] qed. 892 893 894 lemma clean_canonic : ∀tag,A,m,n.(∀i.lookup tag A m i = lookup tag A n i) → 895 clean ?? m = clean ?? n. 896 #tag #A * #m * #n #H normalize @eq_f @pm_clean_canonic #i 897 lapply(H (an_identifier tag i)) 898 normalize // 899 qed. 900 *) 901 lemma update_fail_lookup : ∀tag,A,m,i,v,e.update tag A m i v = Error … e → 902 e = [MSG MissingId; CTX … i] ∧ lookup … m i = None ?. 903 #tag #A #m #i #v #errmsg >update_def cases(lookup tag A m i) [2: #a] normalize 904 #EQ destruct % // 905 qed. 906 907 lemma lookup_hit_update : ∀tag,A,m,i,v.i ∈ m → 908 ∃m'.update tag A m i v = OK ? m'. 909 #tag #A #m #i #v #H % [2: >update_def lapply(in_map_domain … m i) >H * #v #EQ >EQ 910 normalize %] 911 qed. 912 913 lemma lookup_miss_update : ∀tag,A,m,i,v.lookup tag A m i = None ? → 914 update … m i v = Error … [MSG MissingId; CTX … i]. 915 #tag #A #m #i #v #EQ >update_def >EQ normalize % 916 qed. 917 918 lemma update_ok_old_lookup : ∀tag,A,m,i,v,m'.update tag A m i v = OK ? m' → 919 i ∈ m. 920 #tag #A #m #i #v #m' >update_def inversion(lookup tag A m i) [2: #a] #EQ normalize 921 #EQ destruct >EQ normalize @I 922 qed. 923 924 lemma lookup_update_ok : ∀tag,A,m,i,v,m',i'.update tag A m i v = OK ? m' → 925 lookup … m' i' = if eq_identifier ? i' i then Some ? v else lookup … m i'. 926 #tag #A #m #i #v #m' #i' >update_def inversion(lookup tag A m i) [2: #a] #EQ 927 normalize nodelta #EQ1 destruct @eq_identifier_elim 928 [ #H normalize nodelta >H @lookup_add_hit 929  #H normalize nodelta @lookup_add_miss assumption 930 ] 931 qed. 932 933 lemma mem_set_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B. 934 ∀i.i ∈ a ∩ b = (i ∈ a ∧ i ∈ b). 935 #tag #A #B * #a * #b * #i normalize >lookup_opt_merge [2: %] cases(lookup_opt B i b) 936 [2: #a1] normalize [2: @if_elim #_ %] cases(lookup_opt A i a) [2: #a2] normalize % 937 qed. 938 (* 939 lemma merge_eq : ∀A.∀p : positive_map A.∀choice. merge 940 *) 941 lemma add_restrict : ∀tag,A,B.∀a : identifier_map tag A. ∀b : identifier_map tag B. 942 ∀i,v.i∈b → add tag A (a ∩ b) i v = (add tag A a i v) ∩ b. 943 #tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) normalize [#_ *] 944 #v1 #EQv1 * @eq_f lapply EQv1 lapply v1 lapply a lapply b a b v1 elim i normalize 945 [ * normalize [#b #v #EQ destruct] #opt_a #l #r * 946 [#v #EQ destruct normalize %] #opt_b #l1 #r1 #v #EQ destruct normalize cases opt_b 947 normalize [2: #x %] cases(merge A B A ? l1 l) normalize [2: #opt_a2 #l2 #r2 %] 948 cases(merge A B A ? r1 r) // 949 *: #x #IH * [2,4: #opt_b #l1 #r1] #p1 normalize [3,4: #i #EQ destruct] cases p1 p1 950 [2,4: #opt_a #l2 #r2] normalize #v #H cases opt_b [2,4,6,8: #b] normalize 951 [1,2,5,6: <IH try assumption [1,2: cases opt_a [2,4: #a] normalize try %] 952 cases(merge A B A ? l2 l1) normalize // lapply H [1,4: cases r1 *: cases l1] 953 normalize [1,3,5,7,9,11: #EQ destruct] #opt_b4 #l4 #r4 cases x normalize 954 [1,4,7,10,13,16: #EQ destruct normalize // cases(merge A B A ? ? ?) normalize //] 955 #x #H normalize cases(merge A B A ? ? ?) normalize // 956 *: <IH try assumption 957 [1,3: cases(map_opt ? ? ? l1) normalize // lapply H cases r1 normalize 958 [1,3: #EQ destruct] #opt_b2 #l2 #r2 cases x [1,4: //] #x normalize // 959 *: lapply H cases x normalize [2,3,5,6: #y] cases l1 normalize 960 [1,3,5,7,9,11: #EQ destruct] #opt_b2 #l2 #r2 #H // 961 ] 962 ] 963 ] 964 qed. 965 966 lemma update_restrict : ∀tag,A,B.∀a : identifier_map tag A.∀b : identifier_map tag B. 967 ∀i,v.i ∈ b → update ?? (a ∩ b) i v = 968 ! a' ← update ?? a i v ; return a' ∩ b. 969 #tag #A #B #a #b #id #v #H 970 lapply (in_map_domain … b id) >H * #ignore #EQ_lookup_b 971 (*<clean_update*) 972 inversion (update tag A a id v) 973 [2: #e #EQ cases (update_fail_lookup ?????? EQ) #EQ1 #EQ2 destruct 974 >lookup_miss_update [%] 975 >lookup_restrict >H assumption ] 976 #m' #EQ >m_return_bind 977 cases (lookup_hit_update ?? (a∩b) id v ?) 978 [2: >mem_set_restrict >H >(update_ok_old_lookup ?????? EQ) % ] 979 #m'' >update_def >update_def in EQ; >lookup_restrict >H normalize nodelta 980 cases(lookup tag A a id) normalize nodelta [#ABS destruct] #v1 #EQ #EQ'' destruct 981 whd in ⊢ (??%%); @eq_f @add_restrict assumption 982 qed. 983 984 definition sigma_frames : ∀prog : ertlptr_program.sigma_map prog → 985 list (register_env beval × ident) → list (register_env beval × ident) ≝ 986 λprog,sigma,frms.map ?? 987 (λx.〈sigma_register_env prog sigma (\fst x) (getLocalsFromId (\snd x)),\snd x〉) frms. 988 989 (* 665 990 lemma sigma_empty_frames_commute : 666 991 ∀prog : ertl_program. ∀ sigma : (sigma_map prog). … … 688 1013 hw_register_env → Prop ≝ 689 1014 λprog,sigma,regs.sigma_bit_vector_trie_opt prog sigma 6 (reg_env … regs) ≠ None ?. 1015 *) 1016 1017 1018 include "common/BitVectorTrieMap.ma". 690 1019 691 1020 definition sigma_hw_register_env : 692 ∀prog: ertl_program. ∀sigma : (sigma_map prog). 693 ∀h_reg : hw_register_env. well_formed_hw_register_env prog sigma h_reg → 694 hw_register_env ≝ 695 λprog,sigma,h_reg,prf.mk_hw_register_env 696 (opt_safe … prf) (other_bit … h_reg). 697 698 definition well_formed_regs : 699 ∀prog : ertl_program. ∀ sigma : (sigma_map prog). 700 ertl_psd_env×hw_register_env → Prop ≝ 701 λprog,sigma,regs. let 〈x,y〉 ≝ regs in 702 well_formed_ertl_psd_env prog sigma x ∧ well_formed_hw_register_env prog sigma y. 1021 ∀prog: ertlptr_program. ∀sigma : (sigma_map prog). 1022 hw_register_env → hw_register_env ≝ 1023 λprog,sigma,h_reg.mk_hw_register_env 1024 (map ? ? (sigma_beval prog sigma) 6 (reg_env … h_reg)) (other_bit … h_reg). 1025 703 1026 704 1027 definition sigma_regs : 705 ∀prog : ertl_program. ∀sigma : (sigma_map prog). 706 ∀regs: ertl_psd_env×hw_register_env.well_formed_regs prog sigma regs → 707 ertl_psd_env×hw_register_env ≝ 708 λprog,sigma,regs.let 〈x,y〉≝ regs in 709 λprf : well_formed_regs prog sigma 〈x,y〉. 710 〈sigma_ertl_psd_env prog sigma x (proj1 … prf), 711 sigma_hw_register_env prog sigma y (proj2 … prf)〉. 712 1028 ∀prog : ertlptr_program. ∀sigma : (sigma_map prog). 1029 (register_env beval)×hw_register_env→ list register → 1030 (register_env beval)×hw_register_env ≝ 1031 λprog,sigma,regs,ids.let 〈x,y〉≝ regs in 1032 〈sigma_register_env prog sigma x ids, 1033 sigma_hw_register_env prog sigma y〉. 1034 (* 713 1035 lemma sigma_empty_regsT_commute : 714 1036 ∀prog : ertl_program. ∀sigma : (sigma_map prog). … … 746 1068 well_formed_regs prog sigma (regs … st) ∧ 747 1069 well_formed_mem prog sigma (m … st). 1070 *) 748 1071 749 1072 definition sigma_state : 750 ∀prog : ertl _program.1073 ∀prog : ertlptr_program. 751 1074 ∀sigma : sigma_map prog. 752 ∀st : state ERTL_semantics. 753 well_formed_state prog sigma st → 754 state ERTLptr_semantics ≝ 755 λprog,sigma,st,prf. 756 mk_state … 757 (sigma_frames prog sigma (st_frms … st) ?) 758 (sigma_is prog sigma (istack … st) ?) 1075 state ERTLptr_semantics → list register → 1076 state ERTL_semantics ≝ 1077 λprog,sigma,st,ids. 1078 mk_state ? 1079 (sigma_frames prog sigma (st_frms … st)) 1080 (sigma_is prog sigma (istack … st)) 759 1081 (carry … st) 760 (sigma_regs prog sigma (regs … st) ?)761 (sigma_mem prog sigma (m … st) ?).762 @hide_prf cases prf ** // 763 qed. 764 765 definition well_formed_state_pc : 766 ∀prog : ertl_program .∀ sigma : sigma_map prog.767 state_pc ERTL_semantics → Prop ≝ 768 λprog,sigma,st.769 well_formed_pc prog sigma (last_pop … st) ∧ 770 well_formed_state prog sigma st. 1082 (sigma_regs prog sigma (regs … st) ids) 1083 (sigma_mem prog sigma (m … st)). 1084 1085 definition dummy_state : state ERTL_semantics ≝ 1086 mk_state ERTL_semantics 1087 [ ] empty_is BBundef 〈empty_map ? ?,mk_hw_register_env … (Stub …) BBundef〉 empty. 1088 1089 definition dummy_state_pc : state_pc ERTL_semantics ≝ 1090 mk_state_pc ? dummy_state null_pc null_pc. 1091 1092 check fetch_internal_function 771 1093 772 1094 definition sigma_state_pc : 773 ∀prog : ertl_program. ∀sigma : sigma_map prog. 774 ∀ st : state_pc ERTL_semantics. well_formed_state_pc prog sigma st → 775 state_pc ERTLptr_semantics ≝ 776 λprog,sigma,st,prf. 777 mk_state_pc ? (sigma_state … (proj2 … prf)) (pc … st) 778 (sigma_pc … (proj1 … prf)). 779 1095 ∀prog : ertl_program. 1096 let trans_prog ≝ ertl_to_ertlptr prog in 1097 ∀sigma : sigma_map trans_prog. 1098 state_pc ERTLptr_semantics → 1099 state_pc ERTL_semantics ≝ 1100 λprog,sigma,st. 1101 let trans_prog ≝ ertl_to_ertlptr prog in 1102 let ge ≝ globalenv_noinit … prog in 1103 if eqZb (block_id (pc_block (pc … st))) (1) then (* check for dummy pc *) 1104 dummy_state_pc 1105 else 1106 match (fetch_internal_function (joint_closed_internal_function ERTL 1107 (prog_var_names (joint_function ERTL) ℕ prog)) ge (pc_block (pc … st))) with 1108 [OK x ⇒ let 〈i,fd〉 ≝ x in 1109 mk_state_pc ? (sigma_state trans_prog sigma st (joint_if_locals … fd)) 1110 (pc … st) (sigma_stored_pc trans_prog sigma (last_pop … st)) 1111 Error msg ⇒ dummy_state_pc]. 1112 1113 (* 780 1114 lemma reg_store_sigma_commute : 781 1115 ∀ prog : ertl_program. ∀sigma : (sigma_map prog). … … 892 1226 qed. 893 1227 894 895 896 897 1228 lemma ertl_allocate_local_commute : ∀prog : ertl_program. 1229 ∀sigma : sigma_map prog.∀reg,regs,prf1. ∃ prf2. 1230 ertl_allocate_local reg (sigma_regs prog sigma regs prf1) = 1231 sigma_regs prog sigma (ertl_allocate_local reg regs) prf2. 1232 #prog #sigma * #r ** #psd_r #sp #hw_regs #prf1 % 1233 whd in match ertl_allocate_local; normalize nodelta 1234 [ @hide_prf % [2: cases prf1 #_ #x assumption] ] 1235 whd in match set_psd_regs; normalize nodelta 1236 [ whd in match well_formed_ertl_psd_env; whd in match well_formed_register_env; 1237 normalize nodelta * #id #bv cases(decidable_eq_pos id r) 1238 [ #EQ >EQ >lookup_add_hit #EQ1 destruct(EQ1) normalize % #EQ2 destruct 1239  * #EQ 1240 >(lookup_add_miss ?? (psd_r) (an_identifier ? id) (an_identifier RegisterTag r) BVundef ?) 1241 [2: % #EQ1 @EQ destruct %] cases prf1 whd in match well_formed_ertl_psd_env; 1242 whd in match well_formed_register_env; normalize nodelta #H1 #_ #H @H1 1243 [% @idassumption] 1244 ] 1245  whd in match sigma_regs; whd in match sigma_ertl_psd_env; normalize nodelta 1246 @eq_f2 [2: %] @eq_f2 [2: %] whd in match sigma_register_env; normalize nodelta 1247 cases(map_inf_add beval beval RegisterTag psd_r ? BVundef (an_identifier ? r) ? ?) 1248 [ #prf2 #EQ >EQ @eq_f %  1249  #bv #id' #id'' #prf #prf' % 1250 ] 1251 ] 1252 qed. 1253 1254 lemma is_push_sigma_commute : 1255 ∀ prog : ertl_program. ∀ sigma : sigma_map prog. 1256 preserving2 … res_preserve … 1257 (sigma_is prog sigma) 1258 (sigma_beval prog sigma) 1259 (sigma_is prog sigma) 1260 is_push 1261 is_push. 1262 #prog #sigma * 1263 [  #bv1  #bv1 #bv2 ] #val #prf1 #prf2 #is' 1264 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1265 whd in match sigma_beval; normalize nodelta 1266 @opt_safe_elim #val' #EQsigma_val 1267 % 1268 [1,3: @hide_prf % 1269 *: whd in match sigma_is in ⊢ (???%); normalize nodelta 1270 @opt_safe_elim #is'' 1271 ] whd in match sigma_is_opt; normalize nodelta 1272 [2,4: 1273 inversion (sigma_beval_opt ???) 1274 [1,3: #EQ whd in prf1 : (?(??%?)); @⊥ >EQ in prf1; 1275 normalize nodelta * #H @H % ] 1276 #bv1' #EQ_bv1' >m_return_bind ] 1277 >EQsigma_val 1278 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1279 whd in match sigma_is; normalize nodelta 1280 @opt_safe_elim #is1 1281 whd in match sigma_is_opt; normalize nodelta 1282 [ #H @('bind_inversion H) #bv1'' 1283 >EQ_bv1' #EQ destruct(EQ) ] 1284 whd in ⊢ (??%%→?); #EQ destruct(EQ) % 1285 qed. 1286 1287 check internal_stack 1288 check BVpc 1289 1290 definition sigma_is_not_head_opt : ∀ prog : ertl_program. 1291 sigma_map prog → internal_stack → option internal_stack ≝ 1292 λprog,sigma,is. 1293 match is with 1294 [ empty_is ⇒ return empty_is 1295  one_is bv ⇒ return one_is bv 1296  both_is bv1 bv2 ⇒ 1297 ! bv2' ← sigma_beval_opt … sigma bv2 ; 1298 return both_is bv1 bv2' 1299 ]. 1300 1301 1302 lemma ertlptr_save_frame_commute : ∀prog: ertl_program. 1303 ∀sigma : sigma_map prog. ∀kind. 1304 preserving … res_preserve … 1305 (sigma_state_pc prog sigma) 1306 (sigma_state prog sigma) 1307 (ertl_save_frame kind it) 1308 (ertlptr_save_frame kind it). 1309 #prog #sigma * whd in match ertl_save_frame; whd in match ertlptr_save_frame; 1310 normalize nodelta * #st #pc #lp * #wf_lp #wf_st 1311 [2: @mfr_bind 1312 [3: whd in match push_ra; normalize nodelta @mfr_bind 1313 [3: whd in match sigma_state_pc; whd in match push; whd in match sigma_state; 1314 normalize nodelta @mfr_bind 1315 [#is @(sigma_is_not_head_opt prog sigma is ≠ None ?) 1316 #is #prf @(opt_safe … prf) 1317  1318 1319 1320 #x #x_spec @mfr_bind 1321 [ @(λ_.True)  #st * @(sigma_state prog sigma st)  1322 [3: cases kind normalize nodelta whd in match push_ra; normalize nodelta 1323 [ whd in match sigma_state_pc; normalize nodelta #st #st_spec 1324 *) 1325 898 1326 definition ERTLptrStatusSimulation : 899 1327 ∀ prog : ertl_program. 900 1328 let trans_prog ≝ ertl_to_ertlptr prog in 901 1329 ∀stack_sizes. 902 sigma_map prog →1330 sigma_map trans_prog → 903 1331 status_rel (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) ≝ 904 λprog,stack_sizes,sigma.mk_status_rel … 905 (* sem_rel ≝ *) (λ 1332 λprog,stack_sizes,sigma.let trans_prog ≝ ertl_to_ertlptr prog in mk_status_rel ?? 1333 (* sem_rel ≝ *) (λs1:ERTL_status prog stack_sizes 1334 .λs2:ERTLptr_status trans_prog stack_sizes 1335 .s1=sigma_state_pc prog sigma s2) 1336 (* call_rel ≝ *) (λs1:Σs:ERTL_status prog stack_sizes 1337 .as_classifier (ERTL_status prog stack_sizes) s cl_call 1338 .λs2:Σs:ERTLptr_status trans_prog stack_sizes 1339 .as_classifier (ERTLptr_status trans_prog stack_sizes) s cl_call 1340 .pc (mk_prog_params ERTL_semantics prog stack_sizes) s1 1341 =sigma_stored_pc trans_prog sigma 1342 (pc 1343 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_sizes) 1344 s2)) 1345 (* sim_final ≝ *) ?. 1346 cases daemon 1347 qed. 1348 1349 lemma fetch_function_no_minus_one : 1350 ∀F,V,i,p,bl. 1351 block_id (pi1 … bl) = 1 → 1352 fetch_function … (globalenv (λvars.fundef (F vars)) V i p) 1353 bl = Error … [MSG BadFunction]. 1354 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct 1355 whd in match fetch_function; normalize nodelta 1356 >globalenv_no_minus_one 1357 cases (symbol_for_block ???) normalize // 1358 qed. 1359 1360 lemma fetch_function_no_zero : 1361 ∀F,V,i,p,bl. 1362 block_id (pi1 … bl) = 0 → 1363 fetch_function … (globalenv (λvars.fundef (F vars)) V i p) 1364 bl = Error … [MSG BadFunction]. 1365 #F#V#i#p ** #r #id #EQ1 #EQ2 destruct 1366 whd in match fetch_function; normalize nodelta 1367 >globalenv_no_zero 1368 cases (symbol_for_block ???) normalize // 1369 qed. 1370 1371 (*DOPPIONI dei LEMMI in LINEARISE_PROOF*) 1372 lemma symbol_for_block_match: 1373 ∀M:matching.∀initV,initW. 1374 (∀v,w. match_var_entry M v w → 1375 size_init_data_list (initV (\snd v)) = size_init_data_list (initW (\snd w))) → 1376 ∀p: program (m_A M) (m_V M). ∀p': program (m_B M) (m_W M). 1377 ∀MATCH:match_program … M p p'. 1378 ∀b: block. 1379 symbol_for_block … (globalenv … initW p') b = 1380 symbol_for_block … (globalenv … initV p) b. 1381 * #A #B #V #W #match_fn #match_var #initV #initW #H 1382 #p #p' * #Mvars #Mfn #Mmain 1383 #b 1384 whd in match symbol_for_block; normalize nodelta 1385 whd in match globalenv in ⊢ (???%); normalize nodelta 1386 whd in match (globalenv_allocmem ????); 1387 change with (add_globals ?????) in match (foldl ?????); 1388 >(proj1 … (add_globals_match … initW … Mvars)) 1389 [ % *:] 1390 [ * #idr #v * #idr' #w #MVE % 1391 [ inversion MVE 1392 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct % 1393  @(H … MVE) 1394 ] 1395  @(matching_fns_get_same_blocks … Mfn) 1396 #f #g @match_funct_entry_id 1397 ] 1398 qed. 1399 1400 lemma symbol_for_block_transf : 1401 ∀A,B,V,init.∀prog_in : program A V. 1402 ∀trans : ∀vars.A vars → B vars. 1403 let prog_out ≝ transform_program … prog_in trans in 1404 ∀bl. 1405 symbol_for_block … (globalenv … init prog_out) bl = 1406 symbol_for_block … (globalenv … init prog_in) bl. 1407 #A #B #V #iV #p #tf @(symbol_for_block_match … (transform_program_match … tf ?)) 1408 #v0 #w0 * // 1409 qed. 1410 1411 lemma fetch_function_transf : 1412 ∀A,B,V,init.∀prog_in : program A V. 1413 ∀trans : ∀vars.A vars → B vars. 1414 let prog_out ≝ transform_program … prog_in trans in 1415 ∀bl,i,f. 1416 fetch_function … (globalenv … init prog_in) bl = 1417 return 〈i, f〉 1418 → fetch_function … (globalenv … init prog_out) bl = 1419 return 〈i, trans … f〉. 1420 #A #B #V #init #prog_in #trans #bl #i #f 1421 whd in match fetch_function; normalize nodelta 1422 #H lapply (opt_eq_from_res ???? H) H 1423 #H @('bind_inversion H) H #id #eq_symbol_for_block 1424 #H @('bind_inversion H) H #fd #eq_find_funct 1425 whd in ⊢ (??%?→?); #EQ destruct(EQ) 1426 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind 1427 >(find_funct_ptr_transf A B … eq_find_funct) % 1428 qed. 1429 1430 1431 lemma fetch_internal_function_transf : 1432 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ. 1433 ∀trans : ∀vars.A vars → B vars. 1434 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in 1435 ∀bl,i,f. 1436 fetch_internal_function … (globalenv_noinit … prog_in) bl = 1437 return 〈i, f〉 1438 → fetch_internal_function … (globalenv_noinit … prog_out) bl = 1439 return 〈i, trans … f〉. 1440 #A #B #prog #trans #bl #i #f 1441 whd in match fetch_internal_function; normalize nodelta 1442 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch 1443 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1444 >(fetch_function_transf … EQfetch) % 1445 qed. 1446 1447 (* 1448 definition good_local_sigma : 1449 ∀globals. 1450 ∀g:codeT ERTLptr globals. 1451 (Σl.bool_to_Prop (code_has_label … g l)) → 1452 codeT ERTL globals → 1453 (label → option label) → Prop ≝ 1454 λglobals,g,c,sigma. 1455 ∀l,l'.sigma l = Some ? l' → 1456 ∃s. stmt_at … g l = Some ? s ∧ 1457 All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧ 1458 (match s with 1459 [ sequential s' nxt ⇒ 1460 match s' with 1461 [ step_seq _ ⇒ 1462 (stmt_at … c n = Some ? (sequential … s' it)) ∧ 1463 ((sigma nxt = Some ? (S n)) ∨ 1464 (stmt_at … c (S n) = Some ? (GOTO … nxt))) 1465  COND a ltrue ⇒ 1466 (stmt_at … c n = Some ? (sequential … s' it) ∧ sigma nxt = Some ? (S n)) ∨ 1467 (stmt_at … c n = Some ? (FCOND … I a ltrue nxt)) 1468 ] 1469  final s' ⇒ 1470 stmt_at … c n = Some ? (final … s') 1471  FCOND abs _ _ _ ⇒ Ⓧabs 1472 ]). 1473 1474 *) 1475 1476 lemma ps_reg_retrieve_ok : ∀prog : ertlptr_program. 1477 ∀sigma : sigma_map prog. ∀r,restr. 1478 preserving1 ?? res_preserve1 … 1479 (λregs.sigma_regs prog sigma regs restr) 1480 (sigma_beval prog sigma) 1481 (λregs.ps_reg_retrieve regs r) 1482 (λregs.ps_reg_retrieve regs r). 1483 #prog #sigma #r #restr * #psd_r #hw_r whd in match ps_reg_retrieve; 1484 whd in match reg_retrieve; normalize nodelta @opt_to_res_preserve1 1485 whd in match sigma_regs; whd in match sigma_register_env; normalize nodelta 1486 >lookup_restrict @if_elim [2: #_ @opt_preserve_none1] #id_r_in 1487 >(lookup_map ?? RegisterTag ???) #bv #H @('bind_inversion H) H #bv1 1488 #bv1_spec whd in ⊢ (??%? → ?); #EQ destruct %{bv1} % // >bv1_spec % 1489 qed. 1490 1491 lemma hw_reg_retrieve_ok : ∀prog : ertlptr_program. 1492 ∀sigma : sigma_map prog. ∀r,restr. 1493 preserving1 ?? res_preserve1 … 1494 (λregs.sigma_regs prog sigma regs restr) 1495 (sigma_beval prog sigma) 1496 (λregs.hw_reg_retrieve regs r) 1497 (λregs.hw_reg_retrieve regs r). 1498 #prog #sigma #r #restr * #psd_r * #hw_r #b whd in match hw_reg_retrieve; 1499 whd in match hwreg_retrieve; normalize nodelta whd in match sigma_regs; 1500 whd in match sigma_hw_register_env; normalize nodelta 1501 change with (sigma_beval prog sigma BVundef) in ⊢ (???????(??(?????%))?); 1502 #bv >lookup_map whd in ⊢ (???% → ?); #EQ destruct 1503 %{(lookup beval 6 (bitvector_of_register r) hw_r BVundef)} 1504 % // 1505 qed. 1506 1507 1508 lemma ps_reg_store_ok : ∀prog : ertlptr_program. 1509 ∀sigma : sigma_map prog. ∀r,restr. 1510 preserving21 ?? res_preserve1 … 1511 (sigma_beval prog sigma) 1512 (λregs.sigma_regs prog sigma regs restr) 1513 (λregs.sigma_regs prog sigma regs restr) 1514 (ps_reg_store r) 1515 (ps_reg_store r). 1516 #prog #sigma #r #restr whd in match ps_reg_store; normalize nodelta 1517 #bv * #psd_r #hw_r @mfr_bind1 1518 [ @(λr.sigma_register_env prog sigma r restr) 1519  whd in match reg_store; whd in match sigma_regs; normalize nodelta 1520 #x #x_spec lapply(update_ok_to_lookup ?????? x_spec) * * #_ #EQpsd #_ 1521 lapply x_spec x_spec lapply EQpsd EQpsd whd in match sigma_register_env; 1522 normalize nodelta >lookup_restrict @if_elim [2: #_ * #H @⊥ @H %] 1523 #id_in #_ >update_restrict [2: assumption] #H @('bind_inversion H) H 1524 #x0 >map_update_commute #H @('bind_inversion H) H #x1 #x1_spec 1525 whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct %{x1} % // 1526  #x * #psd_r' #hw_r' whd in match sigma_regs; normalize nodelta 1527 whd in ⊢ (???% → ?); #EQ destruct %{〈x,hw_r〉} % // 1528 ] 1529 qed. 1530 1531 1532 lemma hw_reg_store_ok : ∀prog : ertlptr_program. 1533 ∀sigma : sigma_map prog. ∀r,restr. 1534 preserving21 ?? res_preserve1 … 1535 (sigma_beval prog sigma) 1536 (λregs.sigma_regs prog sigma regs restr) 1537 (λregs.sigma_regs prog sigma regs restr) 1538 (hw_reg_store r) 1539 (hw_reg_store r). 1540 #prog #sigma #r #restr whd in match hw_reg_store; normalize nodelta 1541 #bv * #psd_r * #hw_r #b whd in match hwreg_store; whd in match sigma_regs; normalize nodelta 1542 whd in match sigma_hw_register_env; normalize nodelta <insert_map * #psd_r' 1543 * #hw_r' #b' whd in ⊢ (???% → ?); #EQ destruct % [2: % [%] % ] 1544 qed. 1545 1546 1547 lemma ertl_eval_move_ok : ∀prog : ertlptr_program. 1548 ∀sigma : sigma_map prog. ∀ restr,pm. 1549 preserving1 ?? res_preserve1 … 1550 (λregs.sigma_regs prog sigma regs restr) 1551 (λregs.sigma_regs prog sigma regs restr) 1552 (λregs.ertl_eval_move regs pm) 1553 (λregs.ertl_eval_move regs pm). 1554 #prog #sigma #restr * #mv_dst #arg_dst #pm whd in match ertl_eval_move; 1555 normalize nodelta @mfr_bind1 [@(sigma_beval prog sigma) 1556  cases arg_dst normalize nodelta 1557 [2: #b change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?); 1558 @mfr_return1] 1559 * #r normalize nodelta [@ps_reg_retrieve_ok @hw_reg_retrieve_ok] 1560  #bv cases mv_dst #r normalize nodelta [@ps_reg_store_ok  @hw_reg_store_ok] 1561 ] 1562 qed. 1563 1564 lemma ps_arg_retrieve_ok : ∀prog : ertlptr_program. 1565 ∀sigma : sigma_map prog. ∀a,restr. 1566 preserving1 ?? res_preserve1 … 1567 (λregs.sigma_regs prog sigma regs restr) 1568 (sigma_beval prog sigma) 1569 (λregs.ps_arg_retrieve regs a) 1570 (λregs.ps_arg_retrieve regs a). 1571 #prog #sigma #a #restr whd in match ps_arg_retrieve; normalize nodelta cases a a 1572 normalize nodelta [#r  #b ] #regs 1573 [ @ps_reg_retrieve_ok 1574  change with (return sigma_beval prog sigma (BVByte b)) in ⊢ (???????%?); 1575 @mfr_return1 1576 ] 1577 qed. 1578 1579 lemma pop_ok : 1580 ∀prog : ertl_program. 1581 let trans_prog ≝ ertl_to_ertlptr prog in 1582 ∀sigma : sigma_map trans_prog. 1583 ∀stack_size. 1584 ∀fn : (joint_closed_internal_function ERTL (globals (mk_prog_params ERTL_semantics prog stack_size))). 1585 preserving1 ?? res_preserve1 ???? 1586 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 1587 (λx.let 〈bv,st〉 ≝ x in 1588 〈sigma_beval trans_prog sigma bv, 1589 sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn) 〉) 1590 (pop ERTL_semantics) 1591 (pop ERTLptr_semantics). 1592 #prog #sigma #stack_size #fn whd in match pop; normalize nodelta #st @mfr_bind1 1593 [@(λx.let 〈bv,is〉 ≝ x in 1594 〈sigma_beval (ertl_to_ertlptr prog) sigma bv, 1595 sigma_is (ertl_to_ertlptr prog) sigma is 〉) 1596  whd in match is_pop; normalize nodelta whd in match sigma_state; normalize nodelta 1597 cases(istack ? st) normalize nodelta 1598 [@res_preserve_error1 1599 2,3: #bv1 [2: #bv2] * #bv3 #is1 whd in ⊢ (??%% → ?); #EQ destruct 1600 % [2,4: % [1,3: %*: %] *:] 1601 ] 1602  * #bv #is * #bv1 #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] %] 1603 ] 1604 qed. 1605 1606 lemma push_ok : 1607 ∀prog : ertl_program. 1608 let trans_prog ≝ ertl_to_ertlptr prog in 1609 ∀sigma : sigma_map trans_prog. 1610 ∀stack_size. 1611 ∀fn : (joint_closed_internal_function ERTL (globals (mk_prog_params ERTL_semantics prog stack_size))). 1612 preserving21 ?? res_preserve1 … 1613 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 1614 (sigma_beval trans_prog sigma) 1615 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 1616 (push ERTL_semantics) 1617 (push ERTLptr_semantics). 1618 cases daemon 1619 qed. 1620 1621 lemma be_opaccs_ok : 1622 ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1623 ∀ op. 1624 preserving21 ?? res_preserve1 ?????? 1625 (sigma_beval prog sigma) 1626 (sigma_beval prog sigma) 1627 (λx.let 〈bv1,bv2〉 ≝ x in 1628 〈sigma_beval prog sigma bv1, 1629 sigma_beval prog sigma bv2〉) 1630 (be_opaccs op) 1631 (be_opaccs op). 1632 cases daemon 1633 qed. 1634 1635 lemma be_op1_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1636 ∀ op. 1637 preserving1 ?? res_preserve1 … 1638 (sigma_beval prog sigma) 1639 (sigma_beval prog sigma) 1640 (be_op1 op) 1641 (be_op1 op). 1642 cases daemon 1643 qed. 1644 1645 lemma be_op2_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1646 ∀ b,op. 1647 preserving21 ?? res_preserve1 … 1648 (sigma_beval prog sigma) 1649 (sigma_beval prog sigma) 1650 (λx.let 〈bv,b〉≝ x in 〈sigma_beval prog sigma bv,b〉) 1651 (be_op2 b op) 1652 (be_op2 b op). 1653 cases daemon 1654 qed. 1655 1656 lemma pointer_of_address_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1657 preserving1 … res_preserve1 … 1658 (λx.let 〈bv1,bv2〉 ≝ x in〈sigma_beval prog sigma bv1, 1659 sigma_beval prog sigma bv2〉) 1660 (λx.x) 1661 pointer_of_address pointer_of_address. 1662 cases daemon 1663 qed. 1664 1665 lemma beloadv_ok : ∀prog : ertlptr_program. ∀sigma : sigma_map prog. 1666 ∀ptr. 1667 preserving1 … opt_preserve1 … 1668 (sigma_mem prog sigma) 1669 (sigma_beval prog sigma) 1670 (λm.beloadv m ptr) 1671 (λm.beloadv m ptr). 1672 cases daemon 1673 qed. 1674 1675 lemma bestorev_ok : ∀prog : ertlptr_program.∀sigma : sigma_map prog. 1676 ∀ptr. 1677 preserving21 … opt_preserve1 … 1678 (sigma_mem prog sigma) 1679 (sigma_beval prog sigma) 1680 (sigma_mem prog sigma) 1681 (λm.bestorev m ptr) 1682 (λm.bestorev m ptr). 1683 cases daemon 1684 qed. 1685 1686 lemma eval_seq_no_pc_no_call_ok : 1687 ∀prog : ertl_program. 1688 let trans_prog ≝ ertl_to_ertlptr prog in 1689 ∀stack_size.∀sigma : sigma_map trans_prog. 1690 ∀id. ∀fn : (joint_closed_internal_function ??) .∀seq. 1691 preserving1 ?? res_preserve1 ???? 1692 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 1693 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 1694 (eval_seq_no_pc (mk_prog_params ERTL_semantics prog stack_size) 1695 (globals (mk_prog_params ERTL_semantics prog stack_size)) 1696 (ev_genv (mk_prog_params ERTL_semantics prog stack_size)) id fn seq) 1697 (eval_seq_no_pc (mk_prog_params ERTLptr_semantics trans_prog stack_size) 1698 (globals (mk_prog_params ERTLptr_semantics trans_prog stack_size)) 1699 (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size)) id (translate_internal … fn) (translate_step_seq … seq)). 1700 #prog #stack_size #sigma #f #fn * 1701 whd in match eval_seq_no_pc; normalize nodelta 1702 [ #c #st @mfr_return1 1703  #c #st @mfr_return1 1704  #pm #st whd in match pair_reg_move; normalize nodelta 1705 @mfr_bind1 1706 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1707  change with (ertl_eval_move ??) in ⊢ (???????%%); @ertl_eval_move_ok 1708  #regs #st whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1709 ] 1710  #r #st @mfr_bind1 1711 [@(λx.let 〈bv,st〉 ≝ x in 1712 〈sigma_beval (ertl_to_ertlptr prog) sigma bv, 1713 sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn) 〉) 1714  @pop_ok 1715  * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1 1716 [@(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1717  @ps_reg_store_ok 1718  #regs #x whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1719 ] 1720 ] 1721  #r #st @mfr_bind1 1722 [@(λbv.sigma_beval (ertl_to_ertlptr prog) sigma bv) 1723  whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1724  #bv @push_ok 1725 ] 1726  #i 1727 change with (member ? ? ? (((prog_var_names (joint_function ERTL)) ℕ prog)) → ?) 1728 #i_spec 1729 change with ((dpl_reg ERTL) → ?) 1730 #dpl 1731 change with ((dph_reg ERTL) → ?) 1732 #dph #st @mfr_bind1 1733 [@(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn)) 1734  whd in match dpl_store; normalize nodelta @mfr_bind1 1735 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1736  @opt_safe_elim #bl #EQbl 1737 @opt_safe_elim #bl' 1738 >(find_symbol_transf … 1739 (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?); 1740 >EQbl #EQ destruct whd in match sigma_state; normalize nodelta 1741 change with (sigma_beval (ertl_to_ertlptr prog) sigma (BVptr …)) 1742 in ⊢ (???????(?????%?)?); 1743 @ps_reg_store_ok 1744  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1745 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1746 ] 1747  #st1 @opt_safe_elim #bl #EQbl @opt_safe_elim #bl' 1748 >(find_symbol_transf … 1749 (λvars.transf_fundef … (λfn.(translate_internal … fn))) prog i) in ⊢ (%→?); 1750 >EQbl #EQ destruct whd in match dph_store; normalize nodelta @mfr_bind1 1751 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1752  whd in match sigma_state; normalize nodelta 1753 change with (sigma_beval (ertl_to_ertlptr prog) sigma (BVptr …)) 1754 in ⊢ (???????(?????%?)?); 1755 @ps_reg_store_ok 1756  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1757 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1758 ] 1759 ] 1760  #op #a #b #arg1 #arg2 #st @mfr_bind1 1761 [@(sigma_beval (ertl_to_ertlptr prog) sigma) 1762  whd in match acca_arg_retrieve; whd in match sigma_state; normalize nodelta 1763 @ps_arg_retrieve_ok 1764  #bv1 @mfr_bind1 1765 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1766  whd in match accb_arg_retrieve; whd in match sigma_state; normalize nodelta 1767 @ps_arg_retrieve_ok 1768  #bv2 @mfr_bind1 1769 [@(λx.let 〈bv1,bv2〉 ≝ x in 1770 〈sigma_beval (ertl_to_ertlptr prog) sigma bv1, 1771 sigma_beval (ertl_to_ertlptr prog) sigma bv2〉) 1772  @be_opaccs_ok 1773  * #bv3 #bv4 normalize nodelta @mfr_bind1 1774 [ @(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn)) 1775  whd in match acca_store; normalize nodelta @mfr_bind1 1776 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1777  @ps_reg_store_ok 1778  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1779 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1780 ] 1781  #st1 whd in match accb_store; normalize nodelta @mfr_bind1 1782 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1783  whd in match sigma_state; normalize nodelta 1784 @ps_reg_store_ok 1785  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1786 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1787 ] 1788 ] 1789 ] 1790 ] 1791 ] 1792  #op #r1 #r2 #st @mfr_bind1 1793 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1794  whd in match acca_retrieve; normalize nodelta @ps_reg_retrieve_ok 1795  #bv1 @mfr_bind1 1796 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1797  @be_op1_ok 1798  #bv2 whd in match acca_store; normalize nodelta @mfr_bind1 1799 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1800  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 1801  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1802 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1803 ] 1804 ] 1805 ] 1806  #op2 #r1 #r2 #arg #st @mfr_bind1 1807 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1808  whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1809  #bv @mfr_bind1 1810 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1811  whd in match snd_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1812  #bv1 @mfr_bind1 1813 [@(λx.let 〈bv,b〉≝ x in 〈sigma_beval (ertl_to_ertlptr prog) sigma bv,b〉) 1814  @be_op2_ok 1815  * #bv2 #b @mfr_bind1 1816 [ @(λst.sigma_state (ertl_to_ertlptr prog) sigma st (joint_if_locals ERTL ? fn)) 1817  whd in match acca_store; normalize nodelta @mfr_bind1 1818 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1819  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 1820  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1821 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1822 ] 1823  #st1 #st2 whd in match set_carry; whd in match sigma_state; normalize nodelta 1824 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1825 ] 1826 ] 1827 ] 1828 ] 1829  #st whd in match set_carry; whd in match sigma_state; normalize nodelta 1830 #st1 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1831  #st #st1 whd in match set_carry; whd in match sigma_state; normalize nodelta 1832 whd in ⊢ (??%% → ?); #EQ destruct % [2: % [%] % ] 1833  #r1 #dpl #dph #st @mfr_bind1 1834 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1835  whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1836  #bv @mfr_bind1 1837 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1838  whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1839  #bv1 @mfr_bind1 1840 [ @(λx.x) 1841  @(pointer_of_address_ok ? sigma 〈bv1,bv〉) 1842  #ptr @mfr_bind1 1843 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1844  @opt_to_res_preserve1 @beloadv_ok 1845  #bv2 whd in match acca_store; normalize nodelta @mfr_bind1 1846 [ @(λregs.sigma_regs (ertl_to_ertlptr prog) sigma regs (joint_if_locals ERTL ? fn)) 1847  whd in match sigma_state; normalize nodelta @ps_reg_store_ok 1848  #regs #st1 whd in match set_regs; whd in match sigma_state; normalize nodelta; 1849 whd in ⊢(??%% → ?); #EQ destruct % [2: % [%] %] 1850 ] 1851 ] 1852 ] 1853 ] 1854 ] 1855  #dpl #dph #r #st @mfr_bind1 1856 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1857  whd in match dph_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1858  #bv @mfr_bind1 1859 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1860  whd in match dpl_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1861  #bv1 @mfr_bind1 1862 [ @(λx.x) 1863  @(pointer_of_address_ok ? sigma 〈bv1,bv〉) 1864  #ptr @mfr_bind1 1865 [ @(sigma_beval (ertl_to_ertlptr prog) sigma) 1866  whd in match acca_arg_retrieve; normalize nodelta @ps_arg_retrieve_ok 1867  #bv2 @mfr_bind1 1868 [ @(sigma_mem (ertl_to_ertlptr prog) sigma) 1869  @opt_to_res_preserve1 @bestorev_ok 1870  #m #st1 whd in ⊢ (??%% → ?); whd in match set_m; whd in match sigma_state; 1871 normalize nodelta #EQ destruct % [2: % [%] %] 1872 ] 1873 ] 1874 ] 1875 ] 1876 ] 1877  #ext #st cases daemon 1878 ] 1879 qed. 1880 1881 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 1882 ex1_intro: ∀ x:A. P x → ex_Type1 A P. 1883 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) 1884 1885 lemma linearise_ok: 1886 ∀prog. 1887 let trans_prog ≝ ertl_to_ertlptr prog in 1888 ∀stack_sizes. sigma_map trans_prog → 1889 ex_Type1 … (λR. 1890 status_simulation 1891 (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R). 1892 #prog #stack_size #sigma % [@ERTLptrStatusSimulation assumption] 1893 whd in match status_simulation; normalize nodelta 1894 whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta 1895 whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2 1896 whd in match eval_state; normalize nodelta @('bind_inversion) ** #id #fn #stmt 1897 #H lapply (err_eq_from_io ????? H) H #EQfetch @('bind_inversion) #st #EQst 1898 #EQst1' whd in match ERTLptrStatusSimulation; normalize nodelta 1899 #EQsim whd in match joint_abstract_status in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 1900 normalize nodelta whd in match joint_classify; normalize nodelta >EQfetch 1901 >m_return_bind cases stmt in EQst EQst1'; stmt normalize nodelta 1902 [ * [#called #c_arg #c_dest  #reg #lbl  #seq ] #succ_pc  #fin_step  (*FCOND absurd*) cases daemon] 1903 [3: whd in match joint_classify_step; normalize nodelta whd in match eval_statement_no_pc; 1904 normalize nodelta #H1 whd in match eval_statement_advance; normalize nodelta 1905 whd in match set_no_pc; whd in match next; whd in match set_pc; normalize nodelta 1906 #EQtobdest >EQsim in H1; #H1 cases(eval_seq_no_pc_no_call_ok ????????? H1) 1907 [2: cases daemon (*TODO*)] #st' * #st_spec' #st_sim % 1908 [% [ @st' @(pc … st1')  @(last_pop … st1')]] 1909 check taa_base 1910 %{(taaf_step ???? (taa_base … st2) ? ?)} 1911 [(*dalla commutazione del fetch TODO*) cases daemon 1912  whd in match (as_execute ???); whd in match eval_state; normalize nodelta 1913 cases daemon (*dalla commutazione del fetch + st_spec' TODO *) 1914 ] normalize nodelta % [% // cases daemon (*facile TODO *)] whd in match label_rel; 1915 normalize nodelta (*specifica di sigma TODO *) cases daemon 1916  1917 1918 1919 1920 >EQsim in EQfetch; whd in match sigma_state_pc in ⊢ (%→ ?); 1921 whd in match fetch_statement; normalize nodelta #H @('bind_inversion H) H 1922 * #id1 #fn1 whd in match fetch_internal_function; normalize nodelta 1923 #H @('bind_inversion H) H * #id2 #fn2 @if_elim #block_st2_spec 1924 [whd in match dummy_state_pc; whd in match null_pc; normalize nodelta 1925 lapply(fetch_function_no_zero ??????) 1926 [2: @(«mk_block Code OZ,refl region Code»)%@prog7: #EQ >EQ *:] 1927 whd in ⊢ (???% → ?); #ABS destruct] 1928 inversion(fetch_function 1929 (fundef 1930 (joint_closed_internal_function ERTLptr 1931 (prog_var_names (joint_function ERTLptr) ℕ (ertl_to_ertlptr prog)))) 1932 (globalenv_noinit (joint_function ERTLptr) (ertl_to_ertlptr prog)) 1933 (pc_block (pc ERTLptr_semantics st2))) 1934 [2: #err #_ normalize nodelta whd in match dummy_state_pc; whd in match null_pc; normalize nodelta 1935 lapply(fetch_function_no_zero ??????) 1936 [2: @(«mk_block Code OZ,refl region Code»)%@prog7: #EQ >EQ *:] 1937 whd in ⊢ (???% → ?); #ABS destruct] * #id3 #fn3 #EQ lapply(jmeq_to_eq ??? EQ) EQ 1938 #EQffst2 >m_return_bind cases fn3 in EQffst2; fn3 [2: #ext #_ normalize nodelta 1939 whd in match dummy_state_pc; whd in match null_pc; normalize nodelta 1940 lapply(fetch_function_no_zero ??????) 1941 [2: @(«mk_block Code OZ,refl region Code»)%@prog7: #EQ >EQ *:] 1942 whd in ⊢ (???% → ?); #ABS destruct] #fn3 #fn3_spec normalize nodelta 1943 #fn2_spec >(fetch_function_transf ??????????) in fn3_spec; [2: @fn2_spec*:] 1944 cases fn2 in fn2_spec; fn2 #fn2 #fn2_spec whd in match transf_fundef; 1945 normalize nodelta whd in ⊢ (??%? → ?); #EQ destruct whd in ⊢ (??%% → ?); #EQ destruct 1946 #H @('bind_inversion H) H #stmt1 #H lapply(opt_eq_from_res ???? H) H #stmt1_spec 1947 whd in ⊢ (??%% → ?); #EQ destruct cases stmt in stmt1_spec EQst1' EQst; stmt 1948 [* [#called #c_arg #c_dest  #reg #lbl  #seq ] #succ_pc  #fin_step  (*FCOND absurd*) cases daemon] 1949 #stmt_spec whd in match eval_statement_advance; normalize nodelta whd in match eval_call; 1950 normalize nodelta #EQst1' whd in match eval_statement_no_pc; normalize nodelta 1951 [3: #H cases(eval_seq_no_pc_no_call_ok ????????? H) [2: whd in match fetch_internal_function; 1952 normalize nodelta whd in match sigma_state_pc; normalize nodelta @if_elim 1953 [ #H1 >H1 in block_st2_spec; *] #_ whd in match fetch_internal_function; normalize nodelta 1954 >(fetch_function_transf ??????????) [2: @fn2_spec *: ] whd in match transf_fundef; 1955 normalize nodelta >fn2_spec >m_return_bind %] #st3 * #st3_spec #sem_rel 1956 % [ % [ @st3  @(pc … st1')  @(last_pop … st2)]] % [%2 [2: %11:4: whd in match as_classifier; normalize nodelta whd in match (as_classify ??); normalize nodelta 1957 1958 %{(taaf_step … (taa_base …) …) I} 1959 1960 1961 [1,2,4: whd in ⊢ (??%% → ?); #EQ destruct 1962 3: whd in EQst1' : (??%%); whd in match set_no_pc in EQst1'; normalize nodelta in EQst1'; 1963 whd in match sigma_state_pc in EQst1'; normalize nodelta in EQst1'; 1964 >block_st2_spec in EQst1'; @if_elim [ #H >H in block_st2_spec; *] #_ 1965 whd in match fetch_internal_function; normalize nodelta >(fetch_function_transf ??????????) [2: @fn2_spec*:] 1966 >m_return_bind whd in match transf_fundef; normalize nodelta whd in match next; 1967 normalize nodelta whd in match set_pc; normalize nodelta #EQ destruct #H 1968 1969 1970 1971 1972 whd ;in match in EQst1'; 1973 destruct #EQst 1974 #EQst normalize nodelta 1975 [ whd in match joint_classify_step; normalize nodelta 1976 1977 1978 1979 lapply(fetch_function_no_zero ??????) [2: @(«mk_block Code OZ,refl region Code») 1980 2: %  %7: #EQ >EQ *: try assumption 1981 1982 normalize in ⊢ (%→ ?); 1983 normalize in as_ex; 1984 1985 1986
Note: See TracChangeset
for help on using the changeset viewer.