 Timestamp:
 Apr 27, 2012, 10:59:03 AM (8 years ago)
 Location:
 src/ASM
 Files:

 2 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 ? 
src/ASM/Interpret.ma
r1710 r1909 144 144  LCALL _ ⇒ cl_call 145 145  JMP _ ⇒ cl_call 146  AJMP _ ⇒ cl_ jump147  LJMP _ ⇒ cl_ jump148  SJMP _ ⇒ cl_ jump146  AJMP _ ⇒ cl_other 147  LJMP _ ⇒ cl_other 148  SJMP _ ⇒ cl_other 149 149  _ ⇒ cl_other 150 150 ]. … … 609 609 discriminator Prod. 610 610 611 definition compute_target_of_unconditional_jump: 612 ∀program_counter: Word. 613 ∀i: instruction. 614 Word ≝ 615 λprogram_counter. 616 λi. 617 match i with 618 [ LJMP addr ⇒ 619 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with 620 [ ADDR16 a ⇒ λaddr16: True. a 621  _ ⇒ λother: False. ⊥ 622 ] (subaddressing_modein … addr) 623  SJMP addr ⇒ 624 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with 625 [ RELATIVE r ⇒ λrelative: True. 626 let 〈carry, new_pc〉 ≝ half_add ? program_counter (sign_extension r) in 627 new_pc 628  _ ⇒ λother: False. ⊥ 629 ] (subaddressing_modein … addr) 630  AJMP addr ⇒ 631 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 632 [ ADDR11 a ⇒ λaddr11: True. 633 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 program_counter in 634 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 635 let bit ≝ get_index' ? O ? nl in 636 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 637 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 638 let 〈carry, new_pc〉 ≝ half_add ? program_counter new_addr in 639 new_pc 640  _ ⇒ λother: False. ⊥ 641 ] (subaddressing_modein … addr) 642  _ ⇒ zero ? 643 ]. 644 // 645 qed. 646 647 definition is_unconditional_jump: 648 instruction → bool ≝ 649 λi: instruction. 650 match i with 651 [ LJMP _ ⇒ true 652  SJMP _ ⇒ true 653  AJMP _ ⇒ true 654  _ ⇒ false 655 ]. 656 657 let rec member_addressing_mode_tag 658 (n: nat) (v: Vector addressing_mode_tag n) (a: addressing_mode_tag) 659 on v: Prop ≝ 660 match v with 661 [ VEmpty ⇒ False 662  VCons n' hd tl ⇒ 663 bool_to_Prop (eq_a hd a) ∨ member_addressing_mode_tag n' tl a 664 ]. 665 666 lemma is_a_decidable: 667 ∀hd. 668 ∀element. 669 is_a hd element = true ∨ is_a hd element = false. 670 #hd #element // 671 qed. 672 673 lemma mem_decidable: 674 ∀n: nat. 675 ∀v: Vector addressing_mode_tag n. 676 ∀element: addressing_mode_tag. 677 mem … eq_a n v element = true ∨ 678 mem … eq_a … v element = false. 679 #n #v #element // 680 qed. 681 682 lemma eq_a_elim: 683 ∀tag. 684 ∀hd. 685 ∀P: bool → Prop. 686 (tag = hd → P (true)) → 687 (tag ≠ hd → P (false)) → 688 P (eq_a tag hd). 689 #tag #hd #P 690 cases tag 691 cases hd 692 #true_hyp #false_hyp 693 try @false_hyp 694 try @true_hyp 695 try % 696 #absurd destruct(absurd) 697 qed. 698 699 lemma is_a_true_to_is_in: 700 ∀n: nat. 701 ∀x: addressing_mode. 702 ∀tag: addressing_mode_tag. 703 ∀supervector: Vector addressing_mode_tag n. 704 mem addressing_mode_tag eq_a n supervector tag → 705 is_a tag x = true → 706 is_in … supervector x. 707 #n #x #tag #supervector 708 elim supervector 709 [1: 710 #absurd cases absurd 711 2: 712 #n' #hd #tl #inductive_hypothesis 713 whd in match (mem … eq_a (S n') (hd:::tl) tag); 714 @eq_a_elim normalize nodelta 715 [1: 716 #tag_hd_eq #irrelevant 717 whd in match (is_in (S n') (hd:::tl) x); 718 <tag_hd_eq #is_a_hyp >is_a_hyp normalize nodelta 719 @I 720 2: 721 #tag_hd_neq 722 whd in match (is_in (S n') (hd:::tl) x); 723 change with ( 724 mem … eq_a n' tl tag) 725 in match (fold_right … n' ? false tl); 726 #mem_hyp #is_a_hyp 727 cases(is_a hd x) 728 [1: 729 normalize nodelta // 730 2: 731 normalize nodelta 732 @inductive_hypothesis assumption 733 ] 734 ] 735 ] 736 qed. 737 738 lemma is_in_subvector_is_in_supervector: 739 ∀m, n: nat. 740 ∀subvector: Vector addressing_mode_tag m. 741 ∀supervector: Vector addressing_mode_tag n. 742 ∀element: addressing_mode. 743 subvector_with … eq_a subvector supervector → 744 is_in m subvector element → is_in n supervector element. 745 #m #n #subvector #supervector #element 746 elim subvector 747 [1: 748 #subvector_with_proof #is_in_proof 749 cases is_in_proof 750 2: 751 #n' #hd' #tl' #inductive_hypothesis #subvector_with_proof 752 whd in match (is_in … (hd':::tl') element); 753 cases (is_a_decidable hd' element) 754 [1: 755 #is_a_true >is_a_true 756 #irrelevant 757 whd in match (subvector_with … eq_a (hd':::tl') supervector) in subvector_with_proof; 758 @(is_a_true_to_is_in … is_a_true) 759 lapply(subvector_with_proof) 760 cases(mem … eq_a n supervector hd') // 761 2: 762 #is_a_false >is_a_false normalize nodelta 763 #assm 764 @inductive_hypothesis 765 [1: 766 generalize in match subvector_with_proof; 767 whd in match (subvector_with … eq_a (hd':::tl') supervector); 768 cases(mem_decidable n supervector hd') 769 [1: 770 #mem_true >mem_true normalize nodelta 771 #assm assumption 772 2: 773 #mem_false >mem_false #absurd 774 cases absurd 775 ] 776 2: 777 assumption 778 ] 779 ] 780 ] 781 qed. 782 783 let rec subaddressing_mode_elim_type 784 (T: Type[2]) (m: nat) (fixed_v: Vector addressing_mode_tag m) 785 (Q: addressing_mode → T → Prop) 786 (p_addr11: ∀w: Word11. is_in m fixed_v (ADDR11 w) → T) 787 (p_addr16: ∀w: Word. is_in m fixed_v (ADDR16 w) → T) 788 (p_direct: ∀w: Byte. is_in m fixed_v (DIRECT w) → T) 789 (p_indirect: ∀w: Bit. is_in m fixed_v (INDIRECT w) → T) 790 (p_ext_indirect: ∀w: Bit. is_in m fixed_v (EXT_INDIRECT w) → T) 791 (p_acc_a: is_in m fixed_v ACC_A → T) 792 (p_register: ∀w: BitVector 3. is_in m fixed_v (REGISTER w) → T) 793 (p_acc_b: is_in m fixed_v ACC_B → T) 794 (p_dptr: is_in m fixed_v DPTR → T) 795 (p_data: ∀w: Byte. is_in m fixed_v (DATA w) → T) 796 (p_data16: ∀w: Word. is_in m fixed_v (DATA16 w) → T) 797 (p_acc_dptr: is_in m fixed_v ACC_DPTR → T) 798 (p_acc_pc: is_in m fixed_v ACC_PC → T) 799 (p_ext_indirect_dptr: is_in m fixed_v EXT_INDIRECT_DPTR → T) 800 (p_indirect_dptr: is_in m fixed_v INDIRECT_DPTR → T) 801 (p_carry: is_in m fixed_v CARRY → T) 802 (p_bit_addr: ∀w: Byte. is_in m fixed_v (BIT_ADDR w) → T) 803 (p_n_bit_addr: ∀w: Byte. is_in m fixed_v (N_BIT_ADDR w) → T) 804 (p_relative: ∀w: Byte. is_in m fixed_v (RELATIVE w) → T) 805 (n: nat) (v: Vector addressing_mode_tag n) (proof: subvector_with … eq_a v fixed_v) 806 on v: Prop ≝ 807 match v return λo: nat. λv': Vector addressing_mode_tag o. o = n → v ≃ v' → ? with 808 [ VEmpty ⇒ λm_refl. λv_refl. 809 ∀addr: addressing_mode. ∀p: is_in m fixed_v addr. 810 Q addr ( 811 match addr return λx: addressing_mode. is_in … fixed_v x → T with 812 [ ADDR11 x ⇒ p_addr11 x 813  ADDR16 x ⇒ p_addr16 x 814  DIRECT x ⇒ p_direct x 815  INDIRECT x ⇒ p_indirect x 816  EXT_INDIRECT x ⇒ p_ext_indirect x 817  ACC_A ⇒ p_acc_a 818  REGISTER x ⇒ p_register x 819  ACC_B ⇒ p_acc_b 820  DPTR ⇒ p_dptr 821  DATA x ⇒ p_data x 822  DATA16 x ⇒ p_data16 x 823  ACC_DPTR ⇒ p_acc_dptr 824  ACC_PC ⇒ p_acc_pc 825  EXT_INDIRECT_DPTR ⇒ p_ext_indirect_dptr 826  INDIRECT_DPTR ⇒ p_indirect_dptr 827  CARRY ⇒ p_carry 828  BIT_ADDR x ⇒ p_bit_addr x 829  N_BIT_ADDR x ⇒ p_n_bit_addr x 830  RELATIVE x ⇒ p_relative x 831 ] p) 832  VCons n' hd tl ⇒ λm_refl. λv_refl. 833 let tail_call ≝ subaddressing_mode_elim_type T m fixed_v Q p_addr11 834 p_addr16 p_direct p_indirect p_ext_indirect p_acc_a 835 p_register p_acc_b p_dptr p_data p_data16 p_acc_dptr 836 p_acc_pc p_ext_indirect_dptr p_indirect_dptr p_carry 837 p_bit_addr p_n_bit_addr p_relative n' tl ? 838 in 839 match hd return λa: addressing_mode_tag. a = hd → ? with 840 [ addr11 ⇒ λhd_refl. (∀w. Q (ADDR11 w) (p_addr11 w ?)) → tail_call 841  addr16 ⇒ λhd_refl. (∀w. Q (ADDR16 w) (p_addr16 w ?)) → tail_call 842  direct ⇒ λhd_refl. (∀w. Q (DIRECT w) (p_direct w ?)) → tail_call 843  indirect ⇒ λhd_refl. (∀w. Q (INDIRECT w) (p_indirect w ?)) → tail_call 844  ext_indirect ⇒ λhd_refl. (∀w. Q (EXT_INDIRECT w) (p_ext_indirect w ?)) → tail_call 845  acc_a ⇒ λhd_refl. (Q ACC_A (p_acc_a ?)) → tail_call 846  registr ⇒ λhd_refl. (∀w. Q (REGISTER w) (p_register w ?)) → tail_call 847  acc_b ⇒ λhd_refl. (Q ACC_A (p_acc_b ?)) → tail_call 848  dptr ⇒ λhd_refl. (Q DPTR (p_dptr ?)) → tail_call 849  data ⇒ λhd_refl. (∀w. Q (DATA w) (p_data w ?)) → tail_call 850  data16 ⇒ λhd_refl. (∀w. Q (DATA16 w) (p_data16 w ?)) → tail_call 851  acc_dptr ⇒ λhd_refl. (Q ACC_DPTR (p_acc_dptr ?)) → tail_call 852  acc_pc ⇒ λhd_refl. (Q ACC_PC (p_acc_pc ?)) → tail_call 853  ext_indirect_dptr ⇒ λhd_refl. (Q EXT_INDIRECT_DPTR (p_ext_indirect_dptr ?)) → tail_call 854  indirect_dptr ⇒ λhd_refl. (Q INDIRECT_DPTR (p_indirect_dptr ?)) → tail_call 855  carry ⇒ λhd_refl. (Q CARRY (p_carry ?)) → tail_call 856  bit_addr ⇒ λhd_refl. (∀w. Q (BIT_ADDR w) (p_bit_addr w ?)) → tail_call 857  n_bit_addr ⇒ λhd_refl. (∀w. Q (N_BIT_ADDR w) (p_n_bit_addr w ?)) → tail_call 858  relative ⇒ λhd_refl. (∀w. Q (RELATIVE w) (p_relative w ?)) → tail_call 859 ] (refl … hd) 860 ] (refl … n) (refl_jmeq … v). 861 [20: 862 generalize in match proof; destruct 863 whd in match (subvector_with … eq_a (hd:::tl) fixed_v); 864 cases (mem … eq_a m fixed_v hd) normalize nodelta 865 [1: 866 whd in match (subvector_with … eq_a tl fixed_v); 867 #assm assumption 868 2: 869 normalize in ⊢ (% → ?); 870 #absurd cases absurd 871 ] 872 ] 873 @(is_in_subvector_is_in_supervector … proof) 874 destruct @I 875 qed. 876 877 (* XXX: todo *) 878 lemma subaddressing_mode_elim': 879 ∀T: Type[2]. 880 ∀n: nat. 881 ∀o: nat. 882 ∀v1: Vector addressing_mode_tag n. 883 ∀v2: Vector addressing_mode_tag o. 884 ∀Q: addressing_mode → T → Prop. 885 ∀fixed_v: Vector addressing_mode_tag (n + o). 886 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 887 ∀fixed_v_proof: fixed_v = v1 @@ v2. 888 ∀subaddressing_mode_proof. 889 subaddressing_mode_elim_type T (n + o) fixed_v Q P1 P2 P3 P4 P5 P6 P7 890 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 (n + o) (v1 @@ v2) subaddressing_mode_proof. 891 #T #n #o #v1 #v2 892 elim v1 cases v2 893 [1: 894 #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 895 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof 896 #subaddressing_mode_proof destruct normalize 897 #addr #absurd cases absurd 898 2: 899 #n' #hd #tl #Q #fixed_v #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 900 #P11 #P12 #P13 #P14 #P15 #P16 #P17 #P18 #P19 #fixed_v_proof 901 destruct normalize in match ([[]]@@hd:::tl); 902 ] 903 cases daemon 904 qed. 905 906 (* XXX: todo *) 907 lemma subaddressing_mode_elim: 908 ∀T: Type[2]. 909 ∀m: nat. 910 ∀n: nat. 911 ∀Q: addressing_mode → T → Prop. 912 ∀fixed_v: Vector addressing_mode_tag m. 913 ∀P1,P2,P3,P4,P5,P6,P7,P8,P9,P10,P11,P12,P13,P14,P15,P16,P17,P18,P19. 914 ∀v: Vector addressing_mode_tag n. 915 ∀proof. 916 subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7 917 P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof. 918 #T #m #n #Q #fixed_v 919 elim fixed_v 920 [1: 921 #P1 #P2 #P3 #P4 #P5 #P6 #P7 #P8 #P9 #P10 #P11 #P12 #P13 922 #P14 #P15 #P16 #P17 #P18 #P19 #v #proof 923 normalize 924 2: 925 ] 926 cases daemon 927 qed. 928 611 929 definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat. 612 930 Σs': Status cm. 613 931 And (clock ?? s' = \snd current + clock … s) 614 (ASM_classify0 (\fst (\fst current)) = cl_other → 615 program_counter ? ? s' = \snd (\fst current)) ≝ 932 (if is_unconditional_jump (\fst (\fst current)) then 933 program_counter ? ? s' = 934 compute_target_of_unconditional_jump (\snd (\fst current)) (\fst (\fst current)) 935 else 936 (ASM_classify0 (\fst (\fst current)) = cl_other → 937 program_counter ? ? s' = \snd (\fst current))) ≝ 616 938 λcm,s0,instr_pc_ticks. 617 939 let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in … … 651 973 set_program_counter … s new_pc 652 974  LJMP addr ⇒ λinstr_refl. 975 let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in 653 976 let s ≝ set_clock ?? s (ticks + clock … s) in 654 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with 655 [ ADDR16 a ⇒ λaddr16: True. 656 set_program_counter … s a 657  _ ⇒ λother: False. ⊥ 658 ] (subaddressing_modein … addr) 977 set_program_counter … s new_pc 659 978  SJMP addr ⇒ λinstr_refl. 979 let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in 660 980 let s ≝ set_clock ?? s (ticks + clock … s) in 661 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with 662 [ RELATIVE r ⇒ λrelative: True. 663 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in 664 set_program_counter … s new_pc 665  _ ⇒ λother: False. ⊥ 666 ] (subaddressing_modein … addr) 981 set_program_counter … s new_pc 667 982  AJMP addr ⇒ λinstr_refl. 983 let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in 668 984 let s ≝ set_clock ?? s (ticks + clock … s) in 669 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 670 [ ADDR11 a ⇒ λaddr11: True. 671 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 672 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 673 let bit ≝ get_index' ? O ? nl in 674 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 675 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 676 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) new_addr in 677 set_program_counter … s new_pc 678  _ ⇒ λother: False. ⊥ 679 ] (subaddressing_modein … addr) 985 set_program_counter … s new_pc 680 986  ACALL addr ⇒ λinstr_refl. 681 987 let s ≝ set_clock ?? s (ticks + clock … s) in … … 714 1020 normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS % 715 1021 try // 716 destruct(INSTR_PC) <instr_refl 717 #absurd normalize in absurd; try destruct(absurd) try%1022 destruct(INSTR_PC) <instr_refl whd 1023 try (#absurd normalize in absurd; try destruct(absurd) try %) % 718 1024 9: 719 1025 cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?? … … 728 1034 destruct(INSTR_PC_TICKS) % 729 1035 2: 730 #classify_assm clock_proof >classify_proof classify_proof 1036 clock_proof <INSTR_PC_TICKS normalize nodelta 1037 cut(\fst instr_pc = instr ∧ \snd instr_pc = pc) 731 1038 [1: 732 normalize nodelta normalize <INSTR_PC_TICKS 733 destruct(INSTR_PC) % 1039 destruct(INSTR_PC) /2/ 734 1040 2: 735 <classify_assm <INSTR_PC_TICKS destruct <e0 % 736 ] 1041 * #hyp1 #hyp2 >hyp1 normalize nodelta 1042 <instr_refl normalize nodelta #hyp >classify_proof classify_proof 1043 try assumption >hyp2 % 737 1044 ] 738 1045 ] … … 745 1052 definition execute_1': ∀cm.∀s:Status cm. 746 1053 Σs':Status cm. 747 And (clock ?? s' = current_instruction_cost cm s + clock … s) 748 (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … s') ≝ 1054 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 1055 And (clock ?? s' = current_instruction_cost cm s + clock … s) 1056 (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then 1057 program_counter ? ? s' = 1058 compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks)) 1059 else 1060 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1061 program_counter ? ? s' = \snd (\fst instr_pc_ticks))) ≝ 749 1062 λcm. λs: Status cm. 750 1063 let instr_pc_ticks ≝ fetch cm (program_counter … s) in … … 756 1069 2: 757 1070 cases(execute_1_0 cm s instr_pc_ticks) 758 #the_status * #_ #classify_assm #classify_assm' 759 lapply(classify_assm ?) 760 [1: 761 change with ( 762 ASM_classify cm s = cl_other 763 ) 764 assumption 765 2: 766 #program_counter_refl >program_counter_refl % 767 ] 1071 #the_status * #_ #classify_assm 1072 assumption 768 1073 ] 769 1074 qed. … … 772 1077 773 1078 lemma execute_1_ok: ∀cm.∀s. 774 (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧ 775 (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)). 776 #cm #s whd in match execute_1; normalize nodelta @pi2 1079 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 1080 (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧ 1081 (if is_unconditional_jump (\fst (\fst instr_pc_ticks)) then 1082 program_counter ? cm (execute_1 cm s) = 1083 compute_target_of_unconditional_jump (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks)) 1084 else 1085 (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other → 1086 (program_counter ? cm (execute_1 cm s)) = \snd (\fst instr_pc_ticks))) 1087 (* (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *). 1088 #cm #s normalize nodelta 1089 whd in match execute_1; normalize nodelta @pi2 777 1090 qed. (*x Andrea: indexing takes ages here *) 778 1091
Note: See TracChangeset
for help on using the changeset viewer.