 Timestamp:
 Jul 18, 2012, 2:56:12 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r2197 r2209 473 473 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 474 474  INDIRECT i ⇒ 475 let d ≝ get_register … s [[false;false;i]] in 476 ¬(assoc_list_exists ?? d (eq_bv 8) (\fst M)) 475 let d ≝ get_register … s [[false;false;i]] in 476 let address ≝ bit_address_of_register … s [[false;false;i]] in 477 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧ 478 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 477 479  EXT_INDIRECT _ ⇒ true 478 480  REGISTER r ⇒ 
src/ASM/AssemblyProofSplit.ma
r2207 r2209 98 98 qed. 99 99 100 lemma lookup_low_internal_ram_false:101 ∀cm: pseudo_assembly_program.102 ∀status.103 ∀b, b': BitVector 7.104 b = b' →105 lookup … b (low_internal_ram … cm status) (zero 8) = false:::b'.106 #cm * #low_internal_ram #high_internal_ram #external_ram #program_counter107 #sfr_8051 #sfr_8052 #p1_latch #p3_latch #clock #b #b' #b_refl108 cases daemon (* XXX: cannot eliminate, case analyse or invert the BitVectorTrie *)109 qed.110 111 100 lemma sfr_psw_eq_to_bit_address_of_register_eq: 112 101 ∀A: Type[0]. … … 148 137 #_ 149 138 @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl) 150 whd in match get_register; normalize nodelta 151 cases w whd in ⊢ (??%%); @lookup_low_internal_ram_false 152 @sfr_psw_eq_to_bit_address_of_register_eq assumption (* XXX: dubious *) 139 <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try % assumption 153 140 ] 154 141 qed. 155 (* XXX: indirect case false above *)156 142 143 lemma not_b_c_to_b_not_c: 144 ∀b, c: bool. 145 (¬b) = c → b = (¬c). 146 // 147 qed. 148 (* XXX: move above elsewhere *) 149 150 lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map: 151 ∀M. 152 ∀sigma. 153 ∀sfr8051. 154 ∀b. 155 sfr8051 ≠ SFR_ACC_A → 156 map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b. 157 #M #sigma * #b 158 [18: 159 #relevant cases (absurd … (refl ??) relevant) 160 ] 161 #_ % 162 qed. 163 164 lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map: 165 ∀M. 166 ∀sigma: Word → Word. 167 ∀w: BitVector 8. 168 ∀b. 169 w ≠ bitvector_of_nat … 224 → 170 map_address_Byte_using_internal_pseudo_address_map M sigma w b = b. 171 #M #sigma #w #b #w_neq_assm 172 whd in ⊢ (??%?); inversion (sfr_of_Byte ?) 173 [1: 174 #sfr_of_Byte_refl % 175 2: 176 * #sfr8051 #sfr_of_Byte_refl normalize nodelta try % 177 @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map % 178 #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl 179 @(absurd ?? w_neq_assm) 180 lapply sfr_of_Byte_refl b sfr_of_Byte_refl relevant w_neq_assm sfr8051 sigma 181 whd in match sfr_of_Byte; normalize nodelta 182 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 183 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 184 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 185 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 186 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 187 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 188 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 189 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 190 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 191 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 192 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 193 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 194 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 195 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 196 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 197 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 198 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 199 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 200 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 201 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 202 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 203 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 204 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 205 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 206 @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ] 207 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 208 #absurd destruct(absurd) 209 qed. 210 211 lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map: 212 ∀M, sigma, w, b. 213 assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst M) = false → 214 map_internal_ram_address_using_pseudo_address_map M sigma w b = b. 215 #M #sigma #w #b #assoc_list_exists_assm 216 whd in ⊢ (??%?); 217 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) % 218 qed. 219 157 220 lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2: 158 221 ∀M', cm. … … 184 247 normalize nodelta % 185 248 4: 186 #_ 249 #assoc_list_exists_assm lapply (not_b_c_to_b_not_c … assoc_list_exists_assm) 250 assoc_list_exists_assm #assoc_list_exists_assm 187 251 <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl) 188 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_ refl)252 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) 189 253 normalize nodelta % 190 254 ] 191 255 3: 192 256 #w whd in ⊢ (??%? → ??%?); 193 cases daemon (* XXX: ??? *) 257 @eq_bv_elim #eq_bv_refl normalize nodelta 258 [1: 259 #assoc_list_exists_assm cases (conjunction_true … assoc_list_exists_assm) 260 #assoc_list_exists_refl #eq_accumulator_refl 261 >eq_bv_refl change with (map_address_Byte_using_internal_pseudo_address_map M' sigma (bitvector_of_nat 8 224) b = b) 262 whd in ⊢ (??%?); >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_refl) 263 % 264 2: 265 #assoc_list_exists_assm 266 @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta 267 cases (Vector_Sn … bit_one) #bit * #tl >(Vector_O … tl) #bit_one_refl >bit_one_refl 268 <head_head' inversion bit #bit_refl normalize nodelta 269 >bit_one_refl in bit_one_seven_bits_refl; >bit_refl #w_refl normalize in w_refl; 270 [1: 271 @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map <w_refl assumption 272 2: 273 @assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map 274 <w_refl @(not_b_c_to_b_not_c … assoc_list_exists_assm) 275 ] 276 ] 194 277 5,6: 195 278 #w #_ % … … 700 783 change with (set_arg_8 ????? = ?) 701 784 @set_arg_8_status_of_pseudo_status try % 702 [ @sym_eq @set_clock_status_of_pseudo_status 703 [ @sym_eq >EQs @set_program_counter_status_of_pseudo_status % 704  >EQs >EQticks <instr_refl >addr_refl @eq_f2 % 705 ] 706  @(subaddressing_mode_elim … acc_a) @I 707  >EQs >EQticks <instr_refl >addr_refl 785 >EQs >EQticks <instr_refl >addr_refl 786 [1: 787 @sym_eq @set_clock_status_of_pseudo_status 788 [1: 789 @sym_eq @set_program_counter_status_of_pseudo_status % 790 2: 791 @eq_f2 % 792 ] 793 2: 794 @(subaddressing_mode_elim … acc_a) @I 795 3: 708 796 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 709 797 [1: 710 798 @(subaddressing_mode_elim … acc_a) % 711 2:712 %713 3:714 %715 799 4: 716 800 @eq_f2 … … 719 803 [1: 720 804 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 721 [1: 722 @(subaddressing_mode_elim … acc_a) % 723 *: 724 % 725 ] 805 [1: @(subaddressing_mode_elim … acc_a) % *: % ] 726 806 3: 727 807 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 728 [1: 729 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ 730 *: 731 % 732 ] 808 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ *: % ] 733 809 2: 734 810 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 735 [1: 736 @(subaddressing_mode_elim … acc_a) % 737 2: 738 % 739 ] 811 [1: @(subaddressing_mode_elim … acc_a) % 2: % ] 740 812 4: 741 813 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 742 [1: 743 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ 744 *: 745 % 746 ] 814 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ *: % ] 747 815 ] 816 *: 817 % 748 818 ] 749 819 ]
Note: See TracChangeset
for help on using the changeset viewer.