Changeset 2143 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jul 2, 2012, 11:37:34 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2142 r2143 340 340 qed. 341 341 342 lemma m_lt_1_to_m_refl_0: 343 ∀m: nat. 344 m < 1 → m = 0. 345 #m cases m try (#irrelevant %) 346 #m' whd in ⊢ (% → ?); #relevant 347 lapply (le_S_S_to_le … relevant) 348 change with (? < ? → ?) relevant #relevant 349 cases (lt_to_not_zero … relevant) 350 qed. 351 342 352 (*CSC: move elsewhere*) 343 353 axiom lt_to_lt_nat_of_bitvector_add: 344 ∀n,v,m1,m2.345 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 →346 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) <347 nat_of_bitvector n (add n v (bitvector_of_nat n m2)).354 ∀n,v,m1,m2. 355 m2 < 2^n → nat_of_bitvector n v + m2 < 2^n → m1 < m2 → 356 nat_of_bitvector n (add n v (bitvector_of_nat n m1)) < 357 nat_of_bitvector n (add n v (bitvector_of_nat n m2)). 348 358 349 359 (* This is a trivial consequence of fetch_assembly_pseudo + load_code_memory_ok. *) … … 645 655 (external_ram … ps) 646 656 pc 647 (s pecial_function_registers_8051 … ps)657 (sfr_8051_of_pseudo_sfr_8051 M (special_function_registers_8051 … ps) sigma) 648 658 (special_function_registers_8052 … ps) 649 659 (p1_latch … ps) … … 764 774 *) 765 775 776 (* XXX: check values returned for conditional jumps below! *) 766 777 definition ticks_of0: 767 778 ∀p:pseudo_assembly_program. … … 775 786 [ Instruction instr ⇒ 776 787 match instr with 777 [ JC lbl ⇒ ? (* 778 match pol lookup_labels ppc with 779 [ short_jump ⇒ 〈2, 2〉 780  absolute_jump ⇒ ? 781  long_jump ⇒ 〈4, 4〉 782 ] *) 783  JNC lbl ⇒ ? (* 784 match pol lookup_labels ppc with 785 [ short_jump ⇒ 〈2, 2〉 786  absolute_jump ⇒ ? 787  long_jump ⇒ 〈4, 4〉 788 ] *) 789  JB bit lbl ⇒ ? (* 790 match pol lookup_labels ppc with 791 [ short_jump ⇒ 〈2, 2〉 792  absolute_jump ⇒ ? 793  long_jump ⇒ 〈4, 4〉 794 ] *) 795  JNB bit lbl ⇒ ? (* 796 match pol lookup_labels ppc with 797 [ short_jump ⇒ 〈2, 2〉 798  absolute_jump ⇒ ? 799  long_jump ⇒ 〈4, 4〉 800 ] *) 801  JBC bit lbl ⇒ ? (* 802 match pol lookup_labels ppc with 803 [ short_jump ⇒ 〈2, 2〉 804  absolute_jump ⇒ ? 805  long_jump ⇒ 〈4, 4〉 806 ] *) 807  JZ lbl ⇒ ? (* 808 match pol lookup_labels ppc with 809 [ short_jump ⇒ 〈2, 2〉 810  absolute_jump ⇒ ? 811  long_jump ⇒ 〈4, 4〉 812 ] *) 813  JNZ lbl ⇒ ? (* 814 match pol lookup_labels ppc with 815 [ short_jump ⇒ 〈2, 2〉 816  absolute_jump ⇒ ? 817  long_jump ⇒ 〈4, 4〉 818 ] *) 819  CJNE arg lbl ⇒ ? (* 820 match pol lookup_labels ppc with 821 [ short_jump ⇒ 〈2, 2〉 822  absolute_jump ⇒ ? 823  long_jump ⇒ 〈4, 4〉 824 ] *) 825  DJNZ arg lbl ⇒ ? (* 826 match pol lookup_labels ppc with 827 [ short_jump ⇒ 〈2, 2〉 828  absolute_jump ⇒ ? 829  long_jump ⇒ 〈4, 4〉 830 ] *) 788 [ JC lbl ⇒ 789 if policy ppc then 790 〈4, 4〉 791 else 792 〈2, 2〉 793  JNC lbl ⇒ 794 if policy ppc then 795 〈4, 4〉 796 else 797 〈2, 2〉 798  JB bit lbl ⇒ 799 if policy ppc then 800 〈4, 4〉 801 else 802 〈2, 2〉 803  JNB bit lbl ⇒ 804 if policy ppc then 805 〈4, 4〉 806 else 807 〈2, 2〉 808  JBC bit lbl ⇒ 809 if policy ppc then 810 〈4, 4〉 811 else 812 〈2, 2〉 813  JZ lbl ⇒ 814 if policy ppc then 815 〈4, 4〉 816 else 817 〈2, 2〉 818  JNZ lbl ⇒ 819 if policy ppc then 820 〈4, 4〉 821 else 822 〈2, 2〉 823  CJNE arg lbl ⇒ 824 if policy ppc then 825 〈4, 4〉 826 else 827 〈2, 2〉 828  DJNZ arg lbl ⇒ 829 if policy ppc then 830 〈4, 4〉 831 else 832 〈2, 2〉 831 833  ADD arg1 arg2 ⇒ 832 834 let ticks ≝ ticks_of_instruction (ADD ? arg1 arg2) in … … 916 918  Comment comment ⇒ 〈0, 0〉 917 919  Cost cost ⇒ 〈0, 0〉 918  Jmp jmp ⇒ 〈2, 2〉 919  Call call ⇒ 〈2, 2〉 920  Jmp jmp ⇒ 921 if policy ppc then 922 〈4, 4〉 923 else 924 〈2, 2〉 925  Call call ⇒ 926 if policy ppc then 927 〈4, 4〉 928 else 929 〈2, 2〉 920 930  Mov dptr tgt ⇒ 〈2, 2〉 921 931 ]. 922 cases daemon923 qed.924 932 925 933 definition ticks_of:
Note: See TracChangeset
for help on using the changeset viewer.