Changeset 876
 Timestamp:
 Jun 3, 2011, 4:03:00 PM (9 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r875 r876 439 439 ∀P. instruction_elim P = true → ∀i. P i = true. 440 440 441 definition eq_instruction ≝441 (*definition eq_instruction ≝ 442 442 λi, j: instruction. 443 true. 444 445 let rec list_addressing_mode_tags_elim_prop 446 (n: nat) (l: Vector addressing_mode_tag (S n)) 447 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 448 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 449 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 450 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 451 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 452 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 453 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 454 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 455 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 456 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 457 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 458 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 459 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 460 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 461 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 462 (if is_in ? l direct then ∀x. P (DIRECT x) else True) → 463 (if is_in ? l relative then ∀x. P (RELATIVE x) else True) → 464 (if is_in ? l addr11 then ∀x. P (ADDR11 x) else True) → 465 (if is_in ? l addr16 then ∀x. P (ADDR16 x) else True) → 466 (P: addressing_mode → Prop) (x: l) 467 on l : P x ≝ 468 match l return λx.match x with [O ⇒ λl: Vector … O. bool  S x' ⇒ λl: Vector addressing_mode_tag (S x'). 469 (l → bool) → bool ] with 470 [ VEmpty ⇒ true 471  VCons len hd tl ⇒ λP. 472 let process_hd ≝ 473 match hd return λhd. ∀P: hd:::tl → bool. bool with 474 [ direct ⇒ λP.bitvector_elim 8 (λx. P (DIRECT x)) 475  indirect ⇒ λP.bit_elim (λx. P (INDIRECT x)) 476  ext_indirect ⇒ λP.bit_elim (λx. P (EXT_INDIRECT x)) 477  registr ⇒ λP.bitvector_elim 3 (λx. P (REGISTER x)) 478  acc_a ⇒ λP.P ACC_A 479  acc_b ⇒ λP.P ACC_B 480  dptr ⇒ λP.P DPTR 481  data ⇒ λP.bitvector_elim 8 (λx. P (DATA x)) 482  data16 ⇒ λP.bitvector_elim 16 (λx. P (DATA16 x)) 483  acc_dptr ⇒ λP.P ACC_DPTR 484  acc_pc ⇒ λP.P ACC_PC 485  ext_indirect_dptr ⇒ λP.P EXT_INDIRECT_DPTR 486  indirect_dptr ⇒ λP.P INDIRECT_DPTR 487  carry ⇒ λP.P CARRY 488  bit_addr ⇒ λP.bitvector_elim 8 (λx. P (BIT_ADDR x)) 489  n_bit_addr ⇒ λP.bitvector_elim 8 (λx. P (N_BIT_ADDR x)) 490  relative ⇒ λP.bitvector_elim 8 (λx. P (RELATIVE x)) 491  addr11 ⇒ λP.bitvector_elim 11 (λx. P (ADDR11 x)) 492  addr16 ⇒ λP.bitvector_elim 16 (λx. P (ADDR16 x)) 493 ] 494 in 495 andb (process_hd P) 496 (match len return λx. x = len → bool with 497 [ O ⇒ λprf. true 498  S y ⇒ λprf. list_addressing_mode_tags_elim y ? P ] (refl ? len)) 499 ]. 500 try % 501 [ 2: cases (sym_eq ??? prf); @tl 502  generalize in match H; generalize in match tl; cases prf; 503 (* cases prf in tl H; : ??? WAS WORKING BEFORE *) 504 #tl 505 normalize in ⊢ (∀_: %. ?) 506 # H 507 whd 508 normalize in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?]) 509 cases (is_a hd (subaddressing_modeel y tl H)) whd // ] 510 qed. 443 true.*) 444 axiom eq_instruction: instruction → instruction → bool. 511 445 512 446 (* … … 522 456 ]*) 523 457 458 lemma BitVectorTrie_O: 459 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0. 460 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??)) 461 [ #w #_ %1 %[@w] % 462  #n #l #r #abs @⊥ // 463  #n #EQ %2 >EQ %] 464 qed. 465 466 lemma BitVectorTrie_Sn: 467 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n). 468 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%) 469 [ #m #abs @⊥ // 470  #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] // 471  #m #EQ %2 // ] 472 qed. 473 474 lemma lookup_prepare_trie_for_insertion_hit: 475 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n. 476 lookup … b (prepare_trie_for_insertion … b v) a = v. 477 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize // 478 qed. 479 480 lemma lookup_insert_hit: 481 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n. 482 lookup … b (insert … b v t) a = v. 483 #A #a #v #n #b elim b b n // 484 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t) 485 [ * #l * #r #JMEQ >JMEQ cases hd normalize // 486  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ] 487 qed. 488 489 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool. 490 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) // 491 #n #hd #tl #abs @⊥ // 492 qed. 493 494 lemma BitVector_Sn: ∀n.∀v:BitVector (S n). 495 ∃hd.∃tl.v ≃ VCons bool n hd tl. 496 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))) 497 [ #abs @⊥ // 498  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 499 qed. 500 501 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 502 503 lemma lookup_prepare_trie_for_insertion_miss: 504 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n. 505 (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a. 506 #A #a #v #n #c elim c 507 [ #b >(BitVector_O … b) normalize #abs @⊥ // 508  #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 509 cases hd cases hd' normalize 510 [2,3: #_ cases tl' // 511 *: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]] 512 qed. 513 514 lemma lookup_insert_miss: 515 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n. 516 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a. 517 #A #a #v #n #c elim c c n 518 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF // 519  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ 520 #t cases(BitVectorTrie_Sn … t) 521 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 522 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH // 523  #JMEQ >JMEQ cases hd cases hd' #H normalize in H; 524 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize 525 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]] 526 qed. 527 528 definition load_code_memory_aux ≝ 529 fold_left_i_aux … ( 530 λi, mem, v. 531 insert … (bitvector_of_nat … i) v mem) (Stub Byte 16). 532 533 axiom split_elim: 534 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop. 535 (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). 536 537 axiom half_add_SO: 538 ∀pc. 539 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc). 540 541 axiom not_eqvb_S: 542 ∀pc. 543 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S pc))). 544 545 axiom not_eqvb_SS: 546 ∀pc. 547 (¬eq_bv 16 (bitvector_of_nat 16 pc) (bitvector_of_nat 16 (S (S pc)))). 548 524 549 lemma test: 525 ∀ i.526 527 let code_memory ≝ load_code_memory assembled in528 let fetched ≝ fetch code_memory ?in550 ∀pc,i. 551 (let assembled ≝ assembly1 i in 552 let code_memory ≝ load_code_memory_aux pc assembled in 553 let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in 529 554 let 〈instr_pc, ticks〉 ≝ fetched in 530 555 eq_instruction (\fst instr_pc)) i = true. 531 [#i cases i #arg try #arg2 whd in ⊢ (??%?)532 [2 : whd in ⊢ (??(match ? (? %) ?with [ _ ⇒ ?] ?)?)556 #pc #i cases i #arg try #arg2 whd in ⊢ (??%?) 557 [2,4: whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) 533 558 cases arg #sam cases sam #XX try #PP normalize in PP; try cases PP; 534 whd in ⊢ (??(match ? (? %) ? with [ _ ⇒ ?] ?)?) 559 whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?) try cases PP normalize in XX; 560 [1,2,3,4,5,6,7,8,10,11,12,13,14,15,16,17: cases XX 561 *:@split_elim #b1 #b2 #EQ >EQ EQ; 562 change in ⊢ (??(match % with [ _ ⇒ ?] ?)?) with (fetch0 ??) 563 whd in ⊢ (??(match ??% with [ _ ⇒ ?] ?)?) 564 >lookup_insert_miss // 565 >lookup_insert_miss // 566 >lookup_insert_hit 567 whd in ⊢ (??(match % with [ _ ⇒ ?] ?)?) 568 whd in ⊢ (??%?) whd in ⊢ (??(?%?)?) 569 >half_add_SO >half_add_SO 570 >lookup_insert_miss [2,4: @not_eqvb_S] 571 >lookup_insert_hit >lookup_insert_hit] 572  573 574 575 535 576 536 577 [2: #addr whd in ⊢ (??%?) … … 630 671 qed. 631 672 632 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0].633 634 673 lemma index_of_internal_None: ∀i,id,instr_list,n. 635 674 occurs_exactly_once id (instr_list@[〈None …,i〉]) → … … 665 704 → False. 666 705 667 lemma BitVectorTrie_O:668 ∀A:Type[0].∀v:BitVectorTrie A 0.(∃w. v ≃ Leaf A w) ∨ v ≃ Stub A 0.669 #A #v generalize in match (refl … O) cases v in ⊢ (??%? → (?(??(λ_.?%%??)))(?%%??))670 [ #w #_ %1 %[@w] %671  #n #l #r #abs @⊥ //672  #n #EQ %2 >EQ %]673 qed.674 675 lemma BitVectorTrie_Sn:676 ∀A:Type[0].∀n.∀v:BitVectorTrie A (S n).(∃l,r. v ≃ Node A n l r) ∨ v ≃ Stub A (S n).677 #A #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → (?(??(λ_.??(λ_.?%%??))))%)678 [ #m #abs @⊥ //679  #m #l #r #EQ %1 <(injective_S … EQ) %[@l] %[@r] //680  #m #EQ %2 // ]681 qed.682 683 lemma lookup_prepare_trie_for_insertion_hit:684 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.685 lookup … b (prepare_trie_for_insertion … b v) a = v.686 #A #a #v #n #b elim b // #m #hd #tl #IH cases hd normalize //687 qed.688 689 lemma lookup_insert_hit:690 ∀A:Type[0].∀a,v:A.∀n.∀b:BitVector n.∀t:BitVectorTrie A n.691 lookup … b (insert … b v t) a = v.692 #A #a #v #n #b elim b b n //693 #n #hd #tl #IH #t cases(BitVectorTrie_Sn … t)694 [ * #l * #r #JMEQ >JMEQ cases hd normalize //695  #JMEQ >JMEQ cases hd normalize @lookup_prepare_trie_for_insertion_hit ]696 qed.697 698 lemma BitVector_O: ∀v:BitVector 0. v ≃ VEmpty bool.699 #v generalize in match (refl … 0) cases v in ⊢ (??%? → ?%%??) //700 #n #hd #tl #abs @⊥ //701 qed.702 703 lemma BitVector_Sn: ∀n.∀v:BitVector (S n).704 ∃hd.∃tl.v ≃ VCons bool n hd tl.705 #n #v generalize in match (refl … (S n)) cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??)))706 [ #abs @⊥ //707  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ]708 qed.709 710 lemma lookup_prepare_trie_for_insertion_miss:711 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.712 (notb (eq_bv ? b c)) → lookup … b (prepare_trie_for_insertion … c v) a = a.713 #A #a #v #n #c elim c714 [ #b >(BitVector_O … b) normalize #abs @⊥ //715  #m #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ716 cases hd cases hd' normalize717 [2,3: #_ cases tl' //718 *: change with (bool_to_Prop (notb (eq_bv ???)) → ?) /2/ ]]719 qed.720 721 lemma lookup_insert_miss:722 ∀A:Type[0].∀a,v:A.∀n.∀c,b:BitVector n.∀t:BitVectorTrie A n.723 (notb (eq_bv ? b c)) → lookup … b (insert … c v t) a = lookup … b t a.724 #A #a #v #n #c elim c c n725 [ #b #t #DIFF @⊥ whd in DIFF; >(BitVector_O … b) in DIFF //726  #n #hd #tl #IH #b cases(BitVector_Sn … b) #hd' * #tl' #JMEQ >JMEQ727 #t cases(BitVectorTrie_Sn … t)728 [ * #l * #r #JMEQ >JMEQ cases hd cases hd' #H normalize in H;729 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize // @IH //730  #JMEQ >JMEQ cases hd cases hd' #H normalize in H;731 [1,4: change in H with (bool_to_Prop (notb (eq_bv ???))) ] normalize732 [3,4: cases tl' //  *: @lookup_prepare_trie_for_insertion_miss //]]]733 qed.734 706 735 707 definition build_maps' ≝ 
src/ASM/Fetch.ma
r856 r876 6 6 λpmem: BitVectorTrie Byte 16. 7 7 λpc: Word. 8 let 〈x,res〉 ≝ half_add … pc (bitvector_of_nat 16 (S O)) in 9 〈res, lookup … pc pmem (zero 8)〉. 8 〈\snd (half_add … pc (bitvector_of_nat 16 (S O))), lookup … pc pmem (zero 8)〉. 10 9 11 10 (* timings taken from SIEMENS *) 12 11 13 definition fetch : BitVectorTrie Byte 16 → Word→ instruction × Word × nat ≝12 definition fetch0: BitVectorTrie Byte 16 → Word × Byte → instruction × Word × nat ≝ 14 13 λpmem: BitVectorTrie Byte 16. 15 λpc : Word.16 let 〈pc,v〉 ≝ next pmem pcin14 λpc_v. 15 let 〈pc,v〉 ≝ pc_v in 17 16 let 〈b,v〉 ≝ head … v in if b then 18 17 let 〈b,v〉 ≝ head … v in if b then … … 390 389 %. 391 390 qed. 391 392 definition fetch: BitVectorTrie Byte 16 → Word → instruction × Word × nat ≝ 393 λpmem: BitVectorTrie Byte 16. 394 λpc: Word. 395 fetch0 pmem (next pmem pc).
Note: See TracChangeset
for help on using the changeset viewer.