Changeset 2273 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jul 30, 2012, 12:46:19 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2272 r2273 20 20 include "ASM/Test.ma". 21 21 22 lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map: 23 ∀M, cm, ps, sigma, x. 24 ∀addr1: [[acc_a]]. 25 addressing_mode_ok pseudo_assembly_program M cm ps addr1=true → 26 map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x. 27 #M #cm #ps #sigma #x #addr1 28 @(subaddressing_mode_elim … addr1) 29 whd in ⊢ (??%? → ??%?); 30 cases (\snd M) 31 [1: 32 // 33 2: 34 #upper_lower #address normalize nodelta #absurd 35 destruct(absurd) 36 ] 37 qed. 38 39 lemma addressing_mode_ok_to_snd_M_data: 40 ∀M, cm, ps. 41 ∀addr: [[acc_a]]. 42 addressing_mode_ok pseudo_assembly_program M cm ps addr = true → 43 \snd M = data. 44 #M #addr #ps #addr 45 @(subaddressing_mode_elim … addr) 46 whd in ⊢ (??%? → ?); 47 cases (\snd M) normalize nodelta 48 [2: 49 * #address #absurd destruct(absurd) 50 ] 51 #_ % 52 qed. 53 54 lemma assoc_list_exists_true_to_assoc_list_lookup_Some: 55 ∀A, B: Type[0]. 56 ∀e: A. 57 ∀the_list: list (A × B). 58 ∀eq_f: A → A → bool. 59 assoc_list_exists A B e eq_f the_list = true → 60 ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'. 61 #A #B #e #the_list #eq_f elim the_list 62 [1: 63 whd in ⊢ (??%? → ?); #absurd destruct(absurd) 64 2: 65 #hd #tl #inductive_hypothesis 66 whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????); 67 cases (eq_f (\fst hd) e) normalize nodelta 68 [1: 69 #_ %{(\snd hd)} % 70 2: 71 @inductive_hypothesis 72 ] 73 ] 74 qed. 75 76 lemma assoc_list_exists_false_to_assoc_list_lookup_None: 77 ∀A, B: Type[0]. 78 ∀e, e': A. 79 ∀the_list, the_list': list (A × B). 80 ∀eq_f: A → A → bool. 81 e = e' → 82 the_list = the_list' → 83 assoc_list_exists A B e eq_f the_list = false → 84 assoc_list_lookup A B e' eq_f the_list' = None …. 85 #A #B #e #e' #the_list elim the_list 86 [1: 87 #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ % 88 2: 89 #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl 90 whd in ⊢ (??%? → ??%?); <e_refl 91 cases (eq_f (\fst hd) e) normalize nodelta 92 [1: 93 #absurd destruct(absurd) 94 2: 95 >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption 96 ] 97 ] 98 qed. 99 100 lemma sfr_psw_eq_to_bit_address_of_register_eq: 101 ∀A: Type[0]. 102 ∀code_memory: A. 103 ∀status, status', register_address. 104 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 105 bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address. 106 #A #code_memory #status #status' #register_address #sfr_psw_refl 107 whd in match bit_address_of_register; normalize nodelta 108 <sfr_psw_refl % 109 qed. 110 111 lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq: 112 ∀A: Type[0]. 113 ∀code_memory: A. 114 ∀status, status', register_address. 115 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 116 low_internal_ram A code_memory status = low_internal_ram A code_memory status' → 117 get_register A code_memory status register_address = get_register A code_memory status' register_address. 118 #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl 119 whd in match get_register; normalize nodelta <low_internal_ram_refl 120 >(sfr_psw_eq_to_bit_address_of_register_eq … status status') // 121 qed. 122 123 lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr: 124 ∀M', cm, status, status', sigma. 125 ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) 126 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 127 addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true → 128 map_address_mode_using_internal_pseudo_address_map_ok1 M' cm status' sigma addr1. 129 #M' #cm #status #status' #sigma #addr1 #sfr_refl 130 @(subaddressing_mode_elim … addr1) try (#w #_ @I) 131 [1,4: #_ @I ] #w 132 whd in ⊢ (??%? → %); 133 inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta 134 [1,3: 135 #absurd destruct(absurd) 136 2,4: 137 #_ 138 @(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl) 139 <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try % assumption 140 ] 141 qed. 142 22 (*CSC: move elsewhere*) 143 23 lemma not_b_c_to_b_not_c: 144 24 ∀b, c: bool. 145 25 (¬b) = c → b = (¬c). 146 26 // 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 * #b158 [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_assm172 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_refl179 @(absurd ?? w_neq_assm)180 lapply sfr_of_Byte_refl b sfr_of_Byte_refl relevant w_neq_assm sfr8051 sigma181 whd in match sfr_of_Byte; normalize nodelta182 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_assm216 whd in ⊢ (??%?);217 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) %218 qed.219 220 lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2:221 ∀M', cm.222 ∀sigma, status, status', b, b'.223 ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *)224 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW →225 low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' →226 b = b' →227 addressing_mode_ok pseudo_assembly_program M' cm status addr1 = true →228 map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'.229 #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl230 @(subaddressing_mode_elim … addr1)231 [1:232 whd in ⊢ (??%? → ??%?); cases (\snd M')233 [1:234 normalize nodelta #_ %235 2:236 * #address normalize nodelta #absurd destruct(absurd)237 ]238 2,4:239 #w whd in ⊢ (??%? → ??%?);240 inversion (assoc_list_exists ?????) #assoc_list_exists_refl normalize nodelta241 [1,3:242 #absurd destruct(absurd)243 2:244 #_245 <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl)246 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_refl)247 normalize nodelta %248 4: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_assm251 <(sfr_psw_and_low_internal_ram_eq_to_get_register_eq … status status' [[false; false; w]] … sfr_refl low_internal_ram_refl)252 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm)253 normalize nodelta %254 ]255 3:256 #w whd in ⊢ (??%? → ??%?);257 @eq_bv_elim #eq_bv_refl normalize nodelta258 [1:259 #assoc_list_exists_assm cases (conjunction_true … assoc_list_exists_assm)260 #assoc_list_exists_refl #eq_accumulator_refl261 >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_assm266 @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta267 cases (Vector_Sn … bit_one) #bit * #tl >(Vector_O … tl) #bit_one_refl >bit_one_refl268 <head_head' inversion bit #bit_refl normalize nodelta269 >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 assumption272 2:273 @assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map274 <w_refl @(not_b_c_to_b_not_c … assoc_list_exists_assm)275 ]276 ]277 5,6,7,8:278 #w try #w' %279 ]280 qed.281 282 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get:283 ∀M: internal_pseudo_address_map.284 ∀cm: pseudo_assembly_program.285 ∀s: PreStatus pseudo_assembly_program cm.286 ∀sigma: Word → Word.287 ∀addr: [[bit_addr]]. (* XXX: expand as needed *)288 ∀f: bool.289 addressing_mode_ok pseudo_assembly_program M cm s addr = true →290 map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f.291 #M #cm #s #sigma #addr #f292 @(subaddressing_mode_elim … addr) #w293 whd in ⊢ (??%? → %);294 @(vsplit_elim bool ???) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta295 cases (head' bool ??) normalize nodelta296 [1:297 #eq_accumulator_assm whd in ⊢ (??%?);298 cases (sfr_of_Byte ?) try %299 * * normalize nodelta try %300 whd in ⊢ (??%?);301 >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %302 2:303 #assoc_list_exists_assm whd in ⊢ (??%?);304 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) (not_b_c_to_b_not_c … assoc_list_exists_assm)) %305 ]306 qed.307 308 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1:309 ∀M: internal_pseudo_address_map.310 ∀cm: pseudo_assembly_program.311 ∀s, s': PreStatus pseudo_assembly_program cm.312 ∀sigma: Word → Word.313 ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)314 ∀f: bool.315 s = s' →316 addressing_mode_ok pseudo_assembly_program M cm s addr = true →317 map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f.318 #M #cm #s #s' #sigma #addr #f #s_refl <s_refl319 @(subaddressing_mode_elim … addr) [1: #w ]320 whd in ⊢ (??%? → %); [2: #_ @I ]321 inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta322 cases (head' bool ??) normalize nodelta323 [1:324 #eq_accumulator_assm whd in ⊢ (??%?);325 cases (sfr_of_Byte ?) try % * * try % normalize nodelta326 whd in ⊢ (??%?);327 >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %328 2:329 #assoc_list_exists_assm whd in ⊢ (??%?);330 lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) assoc_list_exists_assm #assoc_list_exists_assm331 whd in assoc_list_exists_assm:(???%);332 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %333 ]334 qed.335 336 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2:337 ∀M: internal_pseudo_address_map.338 ∀cm: pseudo_assembly_program.339 ∀s, s': PreStatus pseudo_assembly_program cm.340 ∀sigma: Word → Word.341 ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *)342 ∀f: bool.343 s = s' →344 addressing_mode_ok pseudo_assembly_program M cm s addr = true →345 map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f.346 #M #cm #s #s' #sigma #addr #f #s_refl <s_refl347 @(subaddressing_mode_elim … addr) [1: #w ]348 whd in ⊢ (??%? → %); [2: #_ @I ]349 inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta350 cases (head' bool ??) normalize nodelta351 [1:352 #eq_accumulator_assm whd in ⊢ (??%?);353 cases (sfr_of_Byte ?) try % * * try % normalize nodelta354 whd in ⊢ (??%?);355 >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) %356 2:357 #assoc_list_exists_assm whd in ⊢ (??%?);358 lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) assoc_list_exists_assm #assoc_list_exists_assm359 whd in assoc_list_exists_assm:(???%);360 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) %361 ]362 27 qed. 363 28 … … 371 36 qed. 372 37 38 (*CSC: move elsewhere*) 373 39 lemma conjunction_split: 374 40 ∀l, l', r, r': bool. … … 388 54 #n_refl #s_refl #s_refl' <n_refl <s_refl 389 55 cases n normalize nodelta try % #n' <(s_refl' n') % 390 qed.391 392 axiom insert_low_internal_ram_of_pseudo_low_internal_ram':393 ∀M, M', sigma,cm,s,addr,v,v'.394 (∀addr'.395 ((false:::addr) = addr' →396 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v =397 map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧398 ((false:::addr) ≠ addr' →399 let 〈callM, accM〉 ≝ M in400 let 〈callM', accM'〉 ≝ M' in401 accM = accM' ∧402 assoc_list_lookup … addr' (eq_bv 8) … callM =403 assoc_list_lookup … addr' (eq_bv 8) … callM')) →404 insert Byte 7 addr v'405 (low_internal_ram_of_pseudo_low_internal_ram M'406 (low_internal_ram pseudo_assembly_program cm s)) =407 low_internal_ram_of_pseudo_low_internal_ram M408 (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)).409 410 lemma write_at_stack_pointer_status_of_pseudo_status:411 ∀M, M'.412 ∀cm.413 ∀sigma.414 ∀policy.415 ∀s, s'.416 ∀new_b, new_b'.417 map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' →418 status_of_pseudo_status M cm s sigma policy = s' →419 write_at_stack_pointer ?? s' new_b' =420 status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy.421 #M #M' #cm #sigma #policy #s #s' #new_b #new_b'422 #new_b_refl #s_refl <new_b_refl <s_refl423 whd in match write_at_stack_pointer; normalize nodelta424 @pair_elim #nu #nl #nu_nl_refl normalize nodelta425 @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl))426 [1:427 @eq_f428 whd in match get_8051_sfr; normalize nodelta429 whd in match sfr_8051_index; normalize nodelta430 whd in match status_of_pseudo_status; normalize nodelta431 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta432 cases (\snd M) [2: * #address ] normalize nodelta433 [1,2:434 cases (vsplit bool ???) #high #low normalize nodelta435 whd in match sfr_8051_index; normalize nodelta436 >get_index_v_set_index_miss %437 #absurd destruct(absurd)438 3:439 %440 ]441 2:442 @if_then_else_status_of_pseudo_status try %443 [2:444 @sym_eq <set_low_internal_ram_status_of_pseudo_status445 [1:446 @eq_f2447 [2:448 @insert_low_internal_ram_of_pseudo_low_internal_ram'449 @sym_eq450 [2:451 <set_low_internal_ram_status_of_pseudo_status452 [1:453 @eq_f2454 [2:455 @sym_eq456 >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b')457 [2:458 >new_b_refl459 ]460 ]461 56 qed. 462 57
Note: See TracChangeset
for help on using the changeset viewer.