- Timestamp:
- Jul 25, 2012, 12:12:57 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2247 r2256 480 480 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) ∧ 481 481 ¬assoc_list_exists ?? d (eq_bv 8) (\fst M) 482 | EXT_INDIRECT _ ⇒ true 482 | EXT_INDIRECT e ⇒ 483 let address ≝ bit_address_of_register … s [[false;false;e]] in 484 ¬assoc_list_exists … (false:::address) (eq_bv 8) (\fst M) 483 485 | REGISTER r ⇒ 484 486 let address ≝ bit_address_of_register … s r in … … 679 681 None ? 680 682 | NOP ⇒ Some … M 681 | MOVX addr1 ⇒ Some … M 683 | MOVX addr1 ⇒ 684 match addr1 with 685 [ inl l ⇒ 686 let 〈acc_a, others〉 ≝ l in 687 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 688 let others_ok ≝ addressing_mode_ok T M … s others in 689 if acc_a_ok ∧ others_ok then 690 Some ? M 691 else 692 None ? 693 | inr r ⇒ 694 let 〈others, acc_a〉 ≝ r in 695 let acc_a_ok ≝ addressing_mode_ok T M … s acc_a in 696 let others_ok ≝ addressing_mode_ok T M … s others in 697 if others_ok ∧ acc_a_ok then 698 Some ? M 699 else 700 None ? 701 ] 682 702 | XRL addr1 ⇒ 683 703 match addr1 with -
src/ASM/AssemblyProofSplit.ma
r2247 r2256 123 123 lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr: 124 124 ∀M', cm, status, status', sigma. 125 ∀addr1: [[acc_a; registr; direct; indirect; data ]]. (* XXX: expand as needed *)125 ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) 126 126 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 127 127 addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true → … … 129 129 #M' #cm #status #status' #sigma #addr1 #sfr_refl 130 130 @(subaddressing_mode_elim … addr1) try (#w #_ @I) 131 [1 : #_ @I ]132 #wwhd in ⊢ (??%? → %);131 [1,4: #_ @I ] #w 132 whd in ⊢ (??%? → %); 133 133 inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta 134 [1 :134 [1,3: 135 135 #absurd destruct(absurd) 136 |2 :136 |2,4: 137 137 #_ 138 138 @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl) … … 221 221 ∀M', cm. 222 222 ∀sigma, status, status', b, b'. 223 ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr ]]. (* XXX: expand as needed *)223 ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) 224 224 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 225 225 low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' → … … 275 275 ] 276 276 ] 277 |5,6 :278 #w #_%277 |5,6,7,8: 278 #w try #w' % 279 279 ] 280 280 qed. … … 1935 1935 ] 1936 1936 ] 1937 | *)43: (* MOV *)1937 |43: (* MOV *) 1938 1938 >EQP -P normalize nodelta 1939 1939 inversion addr … … 2121 2121 change with (set_arg_1 ????? = ?) 2122 2122 @set_arg_1_status_of_pseudo_status 2123 >EQs >EQticks <instr_refl >addr_refl try %2124 [1:2123 [1: 2124 >EQs >EQticks <instr_refl >addr_refl 2125 2125 @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq 2126 2126 @(get_arg_1_status_of_pseudo_status … status … M') >status_refl -status_refl try % 2127 2127 @(subaddressing_mode_elim … carry) @I 2128 2128 |2: 2129 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … ps) 2130 [1: 2131 normalize nodelta 2129 >EQs >EQticks <instr_refl >addr_refl % 2130 |3,4: (* XXX: following two cases same proof but Matita is too slow if merged *) 2131 @(pose … (set_clock ????)) #status #status_refl 2132 [1: 2133 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1 … status) try % 2132 2134 |2: 2133 assumption 2134 ] 2135 ] 2136 ] 2137 |44: (* MOVX *) 2135 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … status) try % 2136 ] 2137 >status_refl -status_refl >EQs >EQticks <instr_refl >addr_refl 2138 lapply addressing_mode_ok_assm_1 whd in ⊢ (??%? → ??%?); 2139 @(subaddressing_mode_elim … bit_addr) #w normalize nodelta #relevant assumption 2140 ] 2141 ] 2142 |*)44: (* MOVX *) 2143 >EQP -P normalize nodelta 2144 inversion addr 2145 [1: 2146 #acc_a_others cases acc_a_others #acc_a #others normalize nodelta 2147 #addr_refl 2148 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2149 whd in maps_assm:(??%%); 2150 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 2151 [2: normalize nodelta #absurd destruct(absurd) ] 2152 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 2153 [2: normalize nodelta #absurd destruct(absurd) ] 2154 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 2155 whd in ⊢ (??%?); 2156 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 2157 change with (set_arg_8 ????? = ?) 2158 @set_arg_8_status_of_pseudo_status try % 2159 >EQs >EQticks <instr_refl >addr_refl 2160 [1: 2161 @sym_eq @set_clock_status_of_pseudo_status % 2162 |2: 2163 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 2164 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 2165 |3: 2166 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 2167 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] try % 2168 @(pose … (set_clock ????)) #status #status_refl 2169 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 2170 [1: 2171 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 2172 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 2173 |2: 2174 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 2175 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 2176 ] 2177 ] 2178 |2: 2179 #others_acc_a cases others_acc_a #others #acc_a 2180 #addr_refl 2181 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 2182 whd in maps_assm:(??%%); 2183 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 2184 [2: normalize nodelta #absurd destruct(absurd) ] 2185 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 2186 [2: normalize nodelta #absurd destruct(absurd) ] 2187 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 2188 whd in ⊢ (??%?); 2189 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 2190 change with (set_arg_8 ????? = ?) 2191 @set_arg_8_status_of_pseudo_status 2192 >EQs >EQticks <instr_refl >addr_refl try % 2193 [1: 2194 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1) 2195 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] % 2196 |2: 2197 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1) 2198 [1: 2199 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ 2200 |2,3: 2201 % 2202 |4: 2203 @(pose … (set_clock ????)) #status #status_refl 2204 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 2205 [1: 2206 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_2) 2207 [1: @(subaddressing_mode_elim … acc_a) % ] % 2208 |2: 2209 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_2) 2210 [1: @(subaddressing_mode_elim … acc_a) % ] % 2211 ] 2212 ] 2213 ] 2214 ] 2138 2215 |45: (* SETB *) 2139 2216 >EQP -P normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.