Changeset 1927
 Timestamp:
 May 9, 2012, 1:05:21 PM (8 years ago)
 Location:
 src
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1924 r1927 63 63 ] 64 64  LCALL addr ⇒ 65 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with 65 nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ 66 nat_of_bitvector … program_counter' < total_program_size 67 (*match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Prop with 66 68 [ ADDR16 addr ⇒ λaddr16: True. 67 69 reachable_program_counter code_memory total_program_size addr ∧ … … 69 71 nat_of_bitvector … program_counter' < total_program_size 70 72  _ ⇒ λother: False. ⊥ 71 ] (subaddressing_modein … addr) 73 ] (subaddressing_modein … addr) *) 72 74  ACALL addr ⇒ 73 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with 75 nat_of_bitvector … program_counter < nat_of_bitvector … program_counter' ∧ 76 nat_of_bitvector … program_counter' < total_program_size 77 (* match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Prop with 74 78 [ ADDR11 addr ⇒ λaddr11: True. 75 79 let 〈pc_bu, pc_bl〉 ≝ split … 8 8 program_counter' in … … 81 85 nat_of_bitvector … program_counter' < total_program_size 82 86  _ ⇒ λother: False. ⊥ 83 ] (subaddressing_modein … addr) 87 ] (subaddressing_modein … addr) *) 84 88  AJMP addr ⇒ 85 89 let jump_target ≝ compute_target_of_unconditional_jump program_counter' instruction in … … 98 102 nat_of_bitvector … program_counter' < total_program_size 99 103 ]. 100 cases other 101 qed. 102 103 definition current_instruction_ is_labelled≝104 (* cases other 105 qed. *) 106 107 definition current_instruction_label ≝ 104 108 λcode_memory. 105 109 λcost_labels: BitVectorTrie costlabel 16. 106 110 λs: Status code_memory. 107 111 let pc ≝ program_counter … code_memory s in 108 match lookup_opt … pc cost_labels with 109 [ None ⇒ False 110  _ ⇒ True 111 ]. 112 lookup_opt … pc cost_labels. 112 113 113 114 definition next_instruction_properly_relates_program_counters ≝ … … 159 160 (program_counter …) 160 161 (λs,class. ASM_classify … s = class) 161 (current_instruction_ is_labelled …cost_labels)162 (current_instruction_label code_memory cost_labels) 162 163 (next_instruction_properly_relates_program_counters code_memory) 163 164 ?. … … 373 374 try (#assm1 #absurd destruct(absurd) @I) 374 375 try (#absurd destruct(absurd) @I) 375 [1:376 (* [1: 376 377 #addr #_ 377 378 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] … … 385 386 3: 386 387 #addr #_ * 387 ] 388 # relevant #pc_tps_assm'388 ] *) 389 #_ #_ * #relevant #pc_tps_assm' 389 390 whd cases reachable_program_counter_witness * #n 390 391 #Some_assm #_ % try assumption … … 553 554 #new_pc @ltn_to_ltO 554 555 ] 556 qed. 557 558 lemma not_Some_neq_None_to_False: 559 ∀a: Type[0]. 560 ∀e: a. 561 ¬ (Some a e ≠ None a) → False. 562 #a #e #absurd cases absurd absurd 563 #absurd @absurd @nmk absurd 564 #absurd destruct(absurd) 555 565 qed. 556 566 … … 612 622 generalize in match costed_assm; 613 623 generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels)); 624 whd in match (as_label ??); 614 625 generalize in match (lookup_opt … (program_counter … (execute_1 … status_pre)) cost_labels) 615 in ⊢ (??%? → ?(match % with [ _ ⇒ ?  _ ⇒ ? ])→ ?);626 in ⊢ (??%? → % → ?); 616 627 #lookup_assm cases lookup_assm 617 628 [1: … … 642 653 ] 643 654 2: 644 #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm normalize nodelta 645 #absurd cases absurd #absurd cases(absurd I) 655 #costlabel #Some_lookup_opt_assm <Some_lookup_opt_assm 656 #absurd 657 cases (not_Some_neq_None_to_False ?? absurd) 646 658 ] 647 659 1: … … 654 666 generalize in match costed_assm; 655 667 generalize in match (refl … (lookup_opt … (program_counter … (execute_1 … status_start)) cost_labels)); 668 whd in match (as_label ??); 656 669 generalize in match (lookup_opt … (program_counter … (execute_1 code_memory' status_start)) cost_labels) 657 in ⊢ (??%? → (match % with [ _ ⇒ ?  _ ⇒ ? ])→ ?);670 in ⊢ (??%? → % → ?); 658 671 #lookup_assm cases lookup_assm 659 672 [1: 660 #None_lookup_opt_assm normalize nodelta >None_lookup_opt_assm661 #absurd cases absurd673 #None_lookup_opt_assm 674 #absurd @⊥ cases absurd absurd #absurd @absurd % 662 675 2: 663 676 #costlabel #Some_lookup_opt_assm normalize nodelta #ignore … … 841 854 generalize in match costed_assm; 842 855 generalize in match (refl … (lookup_opt … (program_counter … status_final) cost_labels)); 856 whd in match (as_label ??); 843 857 generalize in match (lookup_opt … (program_counter … status_final) cost_labels) 844 in ⊢ (??%? → (match % with [ _ ⇒ ?  _ ⇒ ? ])→ ?);858 in ⊢ (??%? → % → ?); 845 859 #lookup_assm cases lookup_assm 846 860 [1: 847 861 #None_lookup_opt normalize nodelta #absurd cases absurd 862 absurd #absurd @⊥ @absurd % 848 863 2: 849 864 #costlabel #Some_lookup_opt normalize nodelta #ignore … … 876 891 generalize in match costed_assm; 877 892 generalize in match (refl … (lookup_opt … (program_counter … status_after_fun_call) cost_labels)); 893 whd in match (as_label ??); 878 894 generalize in match (lookup_opt … (program_counter … status_after_fun_call) cost_labels) 879 in ⊢ (??%? → ?(match % with [ _ ⇒ ?  _ ⇒ ? ])→ ?);895 in ⊢ (??%? → % → ?); 880 896 #lookup_assm cases lookup_assm 881 897 [1: … … 899 915 ] 900 916 2: 901 #cost_label #Some_lookup_opt_assm normalize nodelta#absurd902 cases absurd #absurd cases (absurd I)917 #cost_label #Some_lookup_opt_assm #absurd 918 cases (not_Some_neq_None_to_False ?? absurd) 903 919 ] 904 920 ] … … 1121 1137 ] 1122 1138 block_cost' 1123 [32: 1124 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1125 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1126 <FETCH normalize nodelta <instr normalize nodelta 1127 @(subaddressing_mode_elim … [[addr16]] … [[addr16]]) [1: // ] #new_addr 1128 * * * * #n' 1129 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1130 % 1131 [1: 1132 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1133 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1134 >(le_to_leb_true … program_counter_lt') % 1135 2: 1136 assumption 1137 ] 1138 33: 1139 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1140 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1141 <FETCH normalize nodelta <instr normalize nodelta 1142 @(subaddressing_mode_elim … [[addr11]] … [[addr11]]) [1: // ] #new_addr 1143 cases (split … 8 8 program_counter'') #pc_bu #pc_bl normalize nodelta 1144 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 1145 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta * * * * #n' 1146 #_ #_ #program_counter_lt' #program_counter_lt_tps' 1147 % 1148 [1: 1149 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1150 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1151 >(le_to_leb_true … program_counter_lt') % 1152 2: 1153 assumption 1154 ] 1155 27,28: 1156 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1157 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1158 <FETCH normalize nodelta <instr normalize nodelta * 1159 #program_counter_lt' #program_counter_lt_tps' % 1160 [1,3: 1161 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1162 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1163 >(le_to_leb_true … program_counter_lt') % 1164 2,4: 1165 assumption 1166 ] 1167 1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20,21,22,23,24,25,26: 1168 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1169 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1170 <FETCH normalize nodelta <real_instruction_refl <instr normalize nodelta * 1171 #program_counter_lt' #program_counter_lt_tps' % 1172 try assumption 1173 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1174 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1175 >(le_to_leb_true … program_counter_lt') % 1176 29,30,31: (* XXX: unconditional jumps *) 1139 [29,30,31: (* XXX: unconditional jumps *) 1177 1140 normalize nodelta 1178 1141 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1179 1142 lapply (good_program_witness program_counter' reachable_program_counter_witness) 1180 1143 <FETCH normalize nodelta <instr normalize nodelta #assm assumption 1144 *: 1145 cases reachable_program_counter_witness * #n #fetch_n_hyp #lt_hyp 1146 lapply(good_program_witness program_counter' reachable_program_counter_witness) 1147 <FETCH normalize nodelta destruct normalize nodelta 1148 * #program_counter_lt' #program_counter_lt_tps' 1149 % try assumption 1150 %{(S n)} whd in ⊢ (???%); <fetch_n_hyp normalize nodelta 1151 <FETCH normalize nodelta whd in match ltb; normalize nodelta 1152 >(le_to_leb_true … program_counter_lt') % 1181 1153 ] 1182 1154 qed. 
src/ASM/CostsProof.ma
r1923 r1927 287 287 let pc ≝ program_counter ? cm initial in 288 288 let label ≝ 289 match lookup_opt … pc cost_labels return λx: option ?. match x with [None ⇒ False  Some _ ⇒ True]→ costlabel with289 match lookup_opt … pc cost_labels return λx: option ?. x ≠ None … → costlabel with 290 290 [ None ⇒ λabs. ⊥ 291 291  Some l ⇒ λ_. l ] labelled_proof in … … 326 326 labelled_cost @ return_cost 327 327 ]. 328 [ %{pc} whd in match label; generalize in match labelled_proof; whd in ⊢ (% → ?); 329 cases (lookup_opt costlabel … pc cost_labels) normalize 330 [ #abs cases abs  // ] 331  // ] 328 [1: 329 %{pc} whd in match label; generalize in match labelled_proof; whd in ⊢ (% → ?); 330 whd in match (as_costed ??); whd in match (as_label ??); normalize nodelta 331 cases (lookup_opt costlabel … (program_counter … initial) cost_labels) 332 normalize 333 [ #abs cases abs #absurd @⊥ @absurd %  // ] 334  cases abs #absurd @absurd % ] 332 335 qed. 333 336 … … 687 690 generalize in match (tech_cost_of_label0 ? ? ? ? ? ?); 688 691 normalize in match (nth_safe ? ? ? ?); 689 whd in costed_assm; lapply costed_assm 692 whd in costed_assm; lapply costed_assm whd in match (as_label ??); 690 693 inversion (lookup_opt ? ? (program_counter … cm start_status) cost_labels) 691 694 [1: 692 #_ #absurd cases absurd695 #_ #absurd @⊥ cases absurd #absurd @absurd % 693 696 2: 694 697 normalize nodelta #cost_label #Some_assm #_ #p 
src/common/StructuredTraces.ma
r1926 r1927 14 14 15 15 record abstract_status : Type[1] ≝ 16 { as_status :> Type[0] 16 { 17 as_status :> Type[0] 17 18 ; as_execute : as_status → as_status → Prop 18 19 ; as_pc : DeqSet … … 122 123 ]. 123 124 125 definition as_trace_any_label_length': 126 ∀S: abstract_status. 127 ∀trace_ends_flag: trace_ends_with_ret. 128 ∀start_status: S. 129 ∀final_status: S. 130 ∀the_trace: trace_any_label S trace_ends_flag start_status final_status. 131 nat ≝ 132 λS: abstract_status. 133 λtrace_ends_flag: trace_ends_with_ret. 134 λstart_status: S. 135 λfinal_status: S. 136 λthe_trace: trace_any_label S trace_ends_flag start_status final_status. 137 tal_pc_list … the_trace. 138 124 139 let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝ 125 140 match tlr with … … 140 155 bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧ 141 156 tal_unrepeating … tl 157  tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace 142 158  _ ⇒ True 143 159 ]. … … 204 220 λS,st1,st2,tr.match tr with 205 221 [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf» 206 ]. 207 222 ]. 223 208 224 coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝ 209 225  tld_step:
Note: See TracChangeset
for help on using the changeset viewer.