Changeset 1909 for src/ASM/ASMCosts.ma
 Timestamp:
 Apr 27, 2012, 10:59:03 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1907 r1909 110 110 cases other 111 111 qed. 112 113 lemma is_a_decidable:114 ∀hd.115 ∀element.116 is_a hd element = true ∨ is_a hd element = false.117 #hd #element //118 qed.119 120 lemma mem_decidable:121 ∀n: nat.122 ∀v: Vector addressing_mode_tag n.123 ∀element: addressing_mode_tag.124 mem … eq_a n v element = true ∨125 mem … eq_a … v element = false.126 #n #v #element //127 qed.128 129 lemma eq_a_elim:130 ∀tag.131 ∀hd.132 ∀P: bool → Prop.133 (tag = hd → P (true)) →134 (tag ≠ hd → P (false)) →135 P (eq_a tag hd).136 #tag #hd #P137 cases tag138 cases hd139 #true_hyp #false_hyp140 try @false_hyp141 try @true_hyp142 try %143 #absurd destruct(absurd)144 qed.145 146 lemma is_a_true_to_is_in:147 ∀n: nat.148 ∀x: addressing_mode.149 ∀tag: addressing_mode_tag.150 ∀supervector: Vector addressing_mode_tag n.151 mem addressing_mode_tag eq_a n supervector tag →152 is_a tag x = true →153 is_in … supervector x.154 #n #x #tag #supervector155 elim supervector156 [1:157 #absurd cases absurd158 2:159 #n' #hd #tl #inductive_hypothesis160 whd in match (mem … eq_a (S n') (hd:::tl) tag);161 @eq_a_elim normalize nodelta162 [1:163 #tag_hd_eq #irrelevant164 whd in match (is_in (S n') (hd:::tl) x);165 <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta166 @I167 2:168 #tag_hd_neq169 whd in match (is_in (S n') (hd:::tl) x);170 change with (171 mem … eq_a n' tl tag)172 in match (fold_right … n' ? false tl);173 #mem_hyp #is_a_hyp174 cases(is_a hd x)175 [1:176 normalize nodelta //177 2:178 normalize nodelta179 @inductive_hypothesis assumption180 ]181 ]182 ]183 qed.184 185 lemma is_in_subvector_is_in_supervector:186 ∀m, n: nat.187 ∀subvector: Vector addressing_mode_tag m.188 ∀supervector: Vector addressing_mode_tag n.189 ∀element: addressing_mode.190 subvector_with … eq_a subvector supervector →191 is_in m subvector element → is_in n supervector element.192 #m #n #subvector #supervector #element193 elim subvector194 [1:195 #subvector_with_proof #is_in_proof196 cases is_in_proof197 2:198 #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof199 whd in match (is_in … (hd':::tl') element);200 cases (is_a_decidable hd' element)201 [1:202 #is_a_true >is_a_true203 #irrelevant204 whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof;205 @(is_a_true_to_is_in … is_a_true)206 lapply(subvector_with_proof)207 cases(mem … eq_a n supervector hd') //208 2:209 #is_a_false >is_a_false normalize nodelta210 #assm211 @inductive_hypothesis212 [1:213 generalize in match subvector_with_proof;214 whd in match (subvector_with … eq_a (hd':::tl') supervector);215 cases(mem_decidable n supervector hd')216 [1:217 #mem_true >mem_true normalize nodelta218 #assm assumption219 2:220 #mem_false >mem_false #absurd221 cases absurd222 ]223 2:224 assumption225 ]226 ]227 ]228 qed.229 230 let rec member_addressing_mode_tag231 (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag)232 on v: Prop ≝233 match v with234 [ VEmpty ⇒ False235  VCons n' hd tl ⇒236 bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a237 ].238 239 let rec subaddressing_mode_elim_type240 (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m)241 (Q: addressing_mode → T → Prop)242 (p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T)243 (p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T)244 (p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T)245 (p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T)246 (p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T)247 (p_acc_a: is_in m fixed_v ACC_A → T)248 (p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T)249 (p_acc_b: is_in m fixed_v ACC_B → T)250 (p_dptr: is_in m fixed_v DPTR → T)251 (p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T)252 (p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T)253 (p_acc_dptr: is_in m fixed_v ACC_DPTR → T)254 (p_acc_pc: is_in m fixed_v ACC_PC → T)255 (p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T)256 (p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T)257 (p_carry: is_in m fixed_v CARRY → T)258 (p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T)259 (p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T)260 (p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T)261 (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v)262 on v: Prop ≝263 match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with264 [ VEmpty ⇒ λm_refl. λv_refl.265 ∀addr: addressing_mode. ∀p: is_in m fixed_v addr.266 Q addr (267 match addr return λx: addressing_mode. is_in … fixed_v x → T with268 [ ADDR11 x ⇒ p_addr11 x269  ADDR16 x ⇒ p_addr16 x270  DIRECT x ⇒ p_direct x271  INDIRECT x ⇒ p_indirect x272  EXT_INDIRECT x ⇒ p_ext_indirect x273  ACC_A ⇒ p_acc_a274  REGISTER x ⇒ p_register x275  ACC_B ⇒ p_acc_b276  DPTR ⇒ p_dptr277  DATA x ⇒ p_data x278  DATA16 x ⇒ p_data16 x279  ACC_DPTR ⇒ p_acc_dptr280  ACC_PC ⇒ p_acc_pc281  EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr282  INDIRECT_DPTR ⇒ p_indirect_dptr283  CARRY ⇒ p_carry284  BIT_ADDR x ⇒ p_bit_addr x285  N_BIT_ADDR x ⇒ p_n_bit_addr x286  RELATIVE x ⇒ p_relative x287 ] p)288  VCons n' hd tl ⇒ λm_refl. λv_refl.289 let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11290 p_addr16 p_direct p_indirect p_ext_indirect p_acc_a291 p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr292 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry293 p_bit_addr p_n_bit_addr p_relative n' tl ?294 in295 match hd return λa: addressing_mode_tag. a = hd → ? with296 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call297  addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call298  direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call299  indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call300  ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call301  acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call302  registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call303  acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call304  dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call305  data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call306  data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call307  acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call308  acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call309  ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call310  indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call311  carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call312  bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call313  n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call314  relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call315 ] (refl … hd)316 ] (refl … n) (refl_jmeq … v).317 [20:318 generalize in match proof; destruct319 whd in match (subvector_with … eq_a (hd:::tl) fixed_v);320 cases (mem … eq_a m fixed_v hd) normalize nodelta321 [1:322 whd in match (subvector_with … eq_a tl fixed_v);323 #assm assumption324 2:325 normalize in ⊢ (% → ?);326 #absurd cases absurd327 ]328 ]329 @(is_in_subvector_is_in_supervector … proof)330 destruct @I331 qed.332 333 (* XXX: todo *)334 lemma subaddressing_mode_elim':335 ∀T: Type[2].336 ∀n: nat.337 ∀o: nat.338 ∀v1: Vector addressing_mode_tag n.339 ∀v2: Vector addressing_mode_tag o.340 ∀Q: addressing_mode → T → Prop.341 ∀fixed_v: Vector addressing_mode_tag (n + o).342 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.343 ∀fixed_v_proof: fixed_v = v1 @@ v2.344 ∀subaddressing_mode_proof.345 subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7346 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof.347 #T #n #o #v1 #v2348 elim v1 cases v2349 [1:350 #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10351 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof352 #subaddressing_mode_proof destruct normalize353 #addr #absurd cases absurd354 2:355 #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10356 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof357 destruct normalize in match ([[]]@@hd:::tl);358 ]359 cases daemon360 qed.361 362 (* XXX: todo *)363 lemma subaddressing_mode_elim:364 ∀T: Type[2].365 ∀m: nat.366 ∀n: nat.367 ∀Q: addressing_mode → T → Prop.368 ∀fixed_v: Vector addressing_mode_tag m.369 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19.370 ∀v: Vector addressing_mode_tag n.371 ∀proof.372 subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7373 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.374 #T #m #n #Q #fixed_v375 elim fixed_v376 [1:377 #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13378 #P14 #P15 #P16 #P17 #P18 #P19 #v #proof379 normalize380 2:381 ]382 cases daemon383 qed.384 112 385 113 definition current_instruction_is_labelled ≝ … … 496 224 qed. 497 225 226 (* 498 227 (* XXX: indexing bug *) 499 228 lemma fetch_twice_fetch_execute_1: … … 508 237 * #_ #classify_assm' @classify_assm' assumption 509 238 qed. 239 *) 510 240 511 241 lemma reachable_program_counter_to_0_lt_total_program_size: … … 685 415 whd in match current_instruction0 in classifier_assm; normalize nodelta in classifier_assm; 686 416 <FETCH in classifier_assm; >classify_assm #absurd destruct(absurd) 687 qed. 417 qed. *) 688 418 689 419 lemma trace_compute_paid_trace_cl_jump: … … 998 728  ACALL addr ⇒ λinstr. 999 729 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ? 1000  AJMP addr ⇒ λinstr. ticks 730  AJMP addr ⇒ λinstr. 731 ticks + block_cost' code_memory' ? program_size' total_program_size cost_labels ? good_program_witness false ? 1001 732  LCALL addr ⇒ λinstr. 1002 733 ticks + block_cost' code_memory' program_counter'' program_size' total_program_size cost_labels ? good_program_witness false ?
Note: See TracChangeset
for help on using the changeset viewer.