Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3463 r3464 32 32 { instructions : list (AssemblerInstr p) 33 33 ; endmain : ℕ 34 ; endmain_ok : endmain ≤instructions34 ; endmain_ok : endmain < instructions 35 35 }. 36 36 … … 510 510 qed. 511 511 512 (* 513 lemma labels_pc_bounded : ∀p.∀prog : AssemblerProgram p.∀lbl,pc.∀m. 514 mem ? 〈lbl,pc〉 (labels_pc p (instructions … prog) m) → 515 (m + pc) < ((instructions … prog)). 516 #p * #instr #endmain #_ #H1 #H2 elim instr 517 [ #H3 @⊥ /2/ ] #x #xs #IH #_ #lbl #pc #m whd in match (labels_pc ???); 518 #H cases(mem_append ???? H) H 519 [ whd in match labels_pc_of_instr; normalize nodelta 520 cases x normalize nodelta 521 [ #seq * [#lab] 522  #newpc 523  #cond #newpc #ltrue #lfalse 524  #lin #io #lout 525  #f 526  527 ] 528 normalize [1,3,6,7: *] * [2,4,6: * [2,4:*] ] 529 #EQ destruct 530 *) 531 512 532 unification hint 0 ≔ ; 513 533 X ≟ DEQInitCostLabel … … 592 612 static_analisys p abs_t instr_m mT prog = return map → 593 613 mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) O) → 594 get_map … map lbl = block_cost … prog abs_t instr_m pc (S ((instructions … prog))). 614 get_map … map lbl = 615 block_cost … prog abs_t instr_m pc (S ((instructions … prog))) ∧ 616 block_cost … prog abs_t instr_m pc (S ((instructions … prog))) ≠ None ?. 595 617 #p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta 596 618 whd in match asm_no_duplicates; normalize nodelta lapply (labels_pc ???) … … 600 622 cases(bind_inversion ????? H) H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ 601 623 destruct * 602 [ #EQ destruct >get_set_hit >EQelem % 603  #H >get_set_miss [ @IH //] inversion (? == ?) [2: #_ %] 604 #ABS cases H1 H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb // 605 cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1 624 [ #EQ destruct % [ >get_set_hit >EQelem %  >EQelem % whd in ⊢ (??%% → ?); #EQ destruct] 625  #H % 626 [ >get_set_miss [ @(proj1 … (IH …)) //] inversion (? == ?) [2: #_ %] 627 #ABS cases H1 H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb // 628 cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1 629  @(proj2 … (IH …)) // 630 ] 606 631 ] 607 632 qed. … … 741 766 qed. 742 767 743 744 lemma static_dynamic : ∀p,p',prog.asm_no_duplicates p prog → 768 lemma labels_of_trace_are_in_code : 769 ∀p,p',prog.∀st1,st2 : vm_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. 770 ∀lbl. 771 mem … lbl (get_costlabels_of_trace … t) → 772 mem … (costlab lbl) (map ?? \fst … (labels_pc … (instructions p prog) O)). 773 #p #p' #prog #st1 #st2 #t elim t 774 [ #st #lbl * 775  #st1 #st2 #st3 #l * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????); 776 #H cases(mem_append ???? H) H [2: #H @IH //] 777 lapply(vm_step_to_eval … H2) whd in match eval_vmstate; 778 normalize nodelta #H cases(bind_inversion ????? H) H #i * #EQi #_ 779 inversion(emits_labels … i) 780 [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 * 781 [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct // 782  #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit)) 783 * 784 ] 785 ] 786 qed. 787 788 let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝ 789 (match l return λx.l=x → ? with 790 [ nil ⇒ λ_.nil ? 791  cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?) 792 ])(refl …). 793 [ >prf %%  >prf %2 assumption] 794 qed. 795 796 lemma dependent_map_append : ∀A,B,l1,l2,f. 797 dependent_map A B (l1 @ l2) (λa,prf.f a prf) = 798 (dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)). 799 [2: @hide_prf /2/  3: @hide_prf /2/] 800 #A #B #l1 elim l1 normalize /2/ 801 qed. 802 803 lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f. 804 ∀EQ:l1 = l2. 805 dependent_map A B l1 (λa,prf.f a prf) = 806 dependent_map A B l2 (λa,prf.f a ?). 807 [2: >EQ //  #A #B #l1 #l2 #f #EQ >EQ in f; #f % ] 808 qed. 809 810 811 lemma static_dynamic : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog. 745 812 ∀abs_t : abstract_transition_sys (m … p').∀instr_m. 746 813 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1. 747 static_analisys p ? instr_m mT prog = return map1 → 814 ∀EQmap : static_analisys p ? instr_m mT prog = return map1. 748 815 ∀st1,st2 : vm_state p p'. 749 816 ∀ter : terminated_trace (asm_operational_semantics p p' prog) st2. … … 755 822 let stop_state ≝ match R_post_step … ter with [None ⇒ st2  Some x ⇒ \snd x ] in 756 823 ∀costs. 757 costs = map … (λlbl.(opt_safe … (get_map … map1 lbl) ?)) (get_costlabels_of_trace … t) →824 costs = dependent_map CostLabel ? (get_costlabels_of_trace … t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → 758 825 rel_galois … good stop_state (act_abs … abs_t (big_op … costs) (act_abs … abs_t k a1)). 759 [2: @hide_prf cases daemon] 826 [2: @hide_prf 827 cases(mem_map ????? (labels_of_trace_are_in_code … prf)) * 828 #lbl' #pc * #Hmem #EQ destruct 829 >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem)) 830 @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem)) 831 ] 760 832 #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #ter #t 761 833 lapply ter ter elim t … … 786 858 [4,8: cases H1 [1,3: * *: * #y #EQ destruct]] 787 859 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 788 #a1 #good_st_a1 whd in match ( map ????); #costs #EQ >EQ >neutral_r860 #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r 789 861 >act_neutral 790 862 @(instr_map_ok … good … EQfetch … good_st_a1) /2/ … … 792 864  st1 st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H 793 865 #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????); 794 whd #costs whd in match list_cost_to_list_initcost; normalize nodelta 795 <map_append <map_append 796 change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?); 797 #EQ destruct whd in H2 : (??%?); >H3 in H2; normalize nodelta #H 798 cases(bind_inversion ????? H) H #i * #EQi 866 whd #costs >dependent_map_append 867 (*change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);*) 868 #EQ destruct whd in H2 : (??%?); lapply H2 >H3 in ⊢ (% → ?); H2 869 normalize nodelta #H cases(bind_inversion ????? H) H #i * #EQi 799 870 inversion(emits_labels ??) 800 871 [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct >big_op_associative >act_op @IH … … 813 884 5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 814 885 ] // 815  cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx >EQx 816 whd in match (map ????); whd in match (map ????); whd in match (big_op ??); 817 >neutral_l @opt_safe_elim #elem #EQget <(static_analisys_ok … x … (pc … st2) … EQmap) 818 assumption 886  cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx 887 >(rewrite_in_dependent_map … EQx) 888 889 whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??); 890 >neutral_l @opt_safe_elim #elem #EQget 891 cases (static_analisys_ok … x … (pc … st2) … no_dup … EQmap) // 892 #EQ #_ <EQ assumption 819 893  >neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ 820 894  % … … 822 896 >(monotonicity_of_block_cost … EQk') // 823 897  @(instr_map_ok … good … EQi … good_a1) /2/ 824  >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) % 825 ] 826 ] 827 qed. 828 829 830 831 898  lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) 899 #EQ >(rewrite_in_dependent_map … EQ) % 900 ] 901 ] 902 qed. 903 904 905 906
Note: See TracChangeset
for help on using the changeset viewer.