Changeset 1625
 Timestamp:
 Dec 16, 2011, 6:35:45 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/ASMCosts.ma
r1624 r1625 187 187 qed. 188 188 189 axiom is_in_subvector_is_in_supervector: 190 ∀m, n: nat. 191 ∀subvector: Vector addressing_mode_tag m. 192 ∀supervector: Vector addressing_mode_tag n. 193 ∀element: addressing_mode. 194 subvector_with … eq_a subvector supervector → 195 is_in m subvector element → is_in n supervector element. 196 189 197 let rec member_addressing_mode_tag 190 198 (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) … … 197 205 198 206 let rec subaddressing_mode_elim_type 199 (T: Type[2]) ( n: nat) (v: Vector addressing_mode_tag n)207 (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m) 200 208 (Q: addressing_mode → T → Prop) 201 on v: 202 (∀w: Word11. is_in n v (ADDR11 w) → T) → 203 (∀w: Word. is_in n v (ADDR16 w) → T) → 204 (∀w: Byte. is_in n v (DIRECT w) → T) → 205 (∀w: Bit. is_in n v (INDIRECT w) → T) → 206 (∀w: Bit. is_in n v (EXT_INDIRECT w) → T) → 207 ( is_in n v ACC_A → T) → 208 (∀w: BitVector 3. is_in n v (REGISTER w) → T) → 209 ( is_in n v ACC_B → T) → 210 ( is_in n v DPTR → T) → 211 (∀w: Byte. is_in n v (DATA w) → T) → 212 (∀w: Word. is_in n v (DATA16 w) → T) → 213 ( is_in n v ACC_DPTR → T) → 214 ( is_in n v ACC_PC → T) → 215 ( is_in n v EXT_INDIRECT_DPTR → T) → 216 ( is_in n v INDIRECT_DPTR → T) → 217 ( is_in n v CARRY → T) → 218 (∀w: Byte. is_in n v (BIT_ADDR w) → T) → 219 (∀w: Byte. is_in n v (N_BIT_ADDR w) → T) → 220 (∀w: Byte. is_in n v (RELATIVE w) → T) → Prop ≝ 221 match v return λm: nat. λv': Vector addressing_mode_tag m. m = n → v ≃ v' → ? with 209 (p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T) 210 (p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T) 211 (p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T) 212 (p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T) 213 (p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T) 214 (p_acc_a: is_in m fixed_v ACC_A → T) 215 (p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T) 216 (p_acc_b: is_in m fixed_v ACC_B → T) 217 (p_dptr: is_in m fixed_v DPTR → T) 218 (p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T) 219 (p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T) 220 (p_acc_dptr: is_in m fixed_v ACC_DPTR → T) 221 (p_acc_pc: is_in m fixed_v ACC_PC → T) 222 (p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T) 223 (p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T) 224 (p_carry: is_in m fixed_v CARRY → T) 225 (p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T) 226 (p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T) 227 (p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T) 228 (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) 229 on v: Prop ≝ 230 match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with 222 231 [ VEmpty ⇒ λm_refl. λv_refl. 223 λp_addr11. λp_addr16. λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. 224 λp_register. λp_acc_b. λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. 225 λp_ext_indirect_dptr. λp_indirect_dptr. λp_carry. λp_bit_addr. 226 λp_n_bit_addr. λp_relative. 227 ∀addr. ∀p: is_in … v addr. 232 ∀addr: addressing_mode. ∀p: is_in m fixed_v addr. 228 233 Q addr ( 229 match addr return λx: addressing_mode. is_in … v x → T with234 match addr return λx: addressing_mode. is_in … fixed_v x → T with 230 235 [ ADDR11 x ⇒ p_addr11 x 231 236  ADDR16 x ⇒ p_addr16 x … … 249 254 ] p) 250 255  VCons n' hd tl ⇒ λm_refl. λv_refl. 251 λp_addr11. λp_addr16: (∀w: Word. is_in n v (ADDR16 w) → T). 252 λp_direct. λp_indirect. λp_ext_indirect. λp_acc_a. λp_register. λp_acc_b. 253 λp_dptr. λp_data. λp_data16. λp_acc_dptr. λp_acc_pc. λp_ext_indirect_dptr. 254 λp_indirect_dptr. λp_carry. λp_bit_addr. λp_n_bit_addr. λp_relative. 255 let tail_call ≝ subaddressing_mode_elim_type T n' tl Q (? p_addr11) 256 (? p_addr16) (? p_direct) (? p_indirect) (? p_ext_indirect) (? p_acc_a) 257 (? p_register) (? p_acc_b) (? p_dptr) (? p_data) (? p_data16) (? p_acc_dptr) 258 (? p_acc_pc) (? p_ext_indirect_dptr) (? p_indirect_dptr) (? p_carry) 259 (? p_bit_addr) (? p_n_bit_addr) (? p_relative) 256 let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11 257 p_addr16 p_direct p_indirect p_ext_indirect p_acc_a 258 p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 259 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry 260 p_bit_addr p_n_bit_addr p_relative n' tl ? 260 261 in 261 262 match hd return λa: addressing_mode_tag. a = hd → ? with … … 281 282 ] (refl … hd) 282 283 ] (refl … n) (refl_jmeq … v). 283 try (#_ #w1 try #w2)284 284 [20: 285 destruct @p_addr11 try assumption 286 @is_in_tail_to_is_in_cons_hd_tl assumption 287 21: 288 destruct @p_addr16 try assumption 289 @is_in_tail_to_is_in_cons_hd_tl assumption 290 22: 291 destruct @p_direct try assumption 292 @is_in_tail_to_is_in_cons_hd_tl assumption 293 23: 294 destruct @p_indirect try assumption 295 @is_in_tail_to_is_in_cons_hd_tl assumption 296 24: 297 destruct @p_ext_indirect try assumption 298 @is_in_tail_to_is_in_cons_hd_tl assumption 299 25: 300 destruct @p_acc_a try assumption 301 @is_in_tail_to_is_in_cons_hd_tl assumption 302 26: 303 destruct @p_register try assumption 304 @is_in_tail_to_is_in_cons_hd_tl assumption 305 27: 306 destruct @p_acc_b try assumption 307 @is_in_tail_to_is_in_cons_hd_tl assumption 308 28: 309 destruct @p_dptr try assumption 310 @is_in_tail_to_is_in_cons_hd_tl assumption 311 29: 312 destruct @p_data try assumption 313 @is_in_tail_to_is_in_cons_hd_tl assumption 314 30: 315 destruct @p_data16 try assumption 316 @is_in_tail_to_is_in_cons_hd_tl assumption 317 31: 318 destruct @p_acc_dptr try assumption 319 @is_in_tail_to_is_in_cons_hd_tl assumption 320 32: 321 destruct @p_acc_pc try assumption 322 @is_in_tail_to_is_in_cons_hd_tl assumption 323 33: 324 destruct @p_ext_indirect_dptr try assumption 325 @is_in_tail_to_is_in_cons_hd_tl assumption 326 34: 327 destruct @p_indirect_dptr try assumption 328 @is_in_tail_to_is_in_cons_hd_tl assumption 329 35: 330 destruct @p_carry try assumption 331 @is_in_tail_to_is_in_cons_hd_tl assumption 332 36: 333 destruct @p_bit_addr try assumption 334 @is_in_tail_to_is_in_cons_hd_tl assumption 335 37: 336 destruct @p_n_bit_addr try assumption 337 @is_in_tail_to_is_in_cons_hd_tl assumption 338 38: 339 destruct @p_relative try assumption 340 @is_in_tail_to_is_in_cons_hd_tl assumption 341 *: 342 tail_call destruct @I 343 ] 285 generalize in match proof; destruct 286 whd in match (subvector_with … eq_a (hd:::tl) fixed_v); 287 cases (mem … eq_a m fixed_v hd) normalize nodelta 288 [1: 289 whd in match (subvector_with … eq_a tl fixed_v); 290 #assm assumption 291 2: 292 normalize in ⊢ (% → ?); 293 #absurd cases absurd 294 ] 295 ] 296 @(is_in_subvector_is_in_supervector n m v fixed_v … proof) 297 destruct @I 344 298 qed. 345 299 346 axiom subaddressing_mode_elim:300 lemma subaddressing_mode_elim': 347 301 ∀T: Type[2]. 348 ∀ n: nat.349 ∀ v: Vector addressing_mode_tag n.302 ∀m: nat. 303 ∀fixed_v: Vector addressing_mode_tag m. 350 304 ∀Q: addressing_mode → T → Prop. 351 305 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 352 subaddressing_mode_elim_type T n v Q P1 P2 P3 P4 P5 P6 P7 353 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19. 306 ∀n: nat. 307 308 ∀v: Vector addressing_mode_tag n. 309 ∀proof. 310 subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7 311 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. 312 #T #m #fixed_v #Q #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #n #v 313 elim v 314 [ #proof normalize 315 316 qed. 354 317 355 318 (* … … 454 417 cases FETCH normalize nodelta 455 418 cases instr normalize nodelta 456 @(subaddressing_mode_elim Prop 1 [[ addr11 ]]) try // 457 [2: normalize // #new_addr 419 @(subaddressing_mode_elim … [[ addr11 ]]) #new_addr 420 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 421 cases (split … 3 8 new_addr) #thr #eig normalize nodelta 422 cases (split … 5 3 pc_bu) #fiv #thr' normalize nodelta 423 #assm cases assm #ignore 424 whd in match good_program_counter; normalize nodelta * #n * * 425 #program_counter_eq' #program_counter_lt_total_program_size 426 #fetch_n_leq_program_counter' 427 @(transitive_le 428 total_program_size 429 ((S program_size') + nat_of_bitvector … program_counter) 430 (program_size' + nat_of_bitvector … program_counter') recursive_case) 431 whd in ⊢ (?%?); 432 change with ( 433 program_size' + (nat_of_bitvector … program_counter) < 434 program_size' + (nat_of_bitvector … program_counter')) 435 @lt_n_o_to_plus_m_n_lt_plus_m_o 436 >(fetch_program_counter_n_technical code_memory program_counter 437 program_counter' instruction ticks n) 438 /2 by pair_destruct_2/ 439 7: 440 generalize in match good_program_witness; 441 whd in match good_program; normalize nodelta 442 cases FETCH normalize nodelta 443 cases instr normalize nodelta 444 @(subaddressing_mode_elim … [[ acc_dptr; acc_pc ]]) #new_addr 458 445 cases (split … 8 8 program_counter') #pc_bu #pc_bl normalize nodelta 459 446 cases (split … 3 8 new_addr) #thr #eig normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.