Changeset 2273
- Timestamp:
- Jul 30, 2012, 12:46:19 AM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 4 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 -
src/ASM/AssemblyProofSplitSplit.ma
r2269 r2273 51 51 qed. 52 52 53 (*CSC: move elsewhere*)54 lemma bv_append_eq_to_eq:55 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.56 v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.57 #A #n #v1 elim v158 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%59 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ260 #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]61 qed.62 63 53 theorem main_thm: 64 54 ∀M, M': internal_pseudo_address_map. -
src/ASM/PolicyFront.ma
r2264 r2273 238 238 ] 239 239 ]. 240 240 241 241 (* new safety condition: sigma corresponds to program and resulting program is compact *) 242 242 definition sigma_compact ≝ -
src/ASM/Test.ma
r2272 r2273 301 301 qed. 302 302 303 (*304 303 lemma get_index_v_status_of_pseudo_status: 305 304 ∀M, code_memory, sigma, policy, s, s', sfr. … … 316 315 whd in match status_of_pseudo_status; normalize nodelta 317 316 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 318 inversion (\snd M) try ( #upper_lower #address) #sndM_refl normalize nodelta317 inversion (\snd M) try ( * #upper_lower #address) #sndM_refl normalize nodelta 319 318 [1: 320 319 cases sfr … … 326 325 % 327 326 |2: 327 inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta 328 328 @pair_elim #high #low #high_low_refl normalize nodelta 329 inversion (eq_upper_lower upper_lower upper) #eq_upper_lower_refl normalize nodelta330 329 cases sfr 331 330 [18,37: … … 340 339 ] 341 340 qed. 342 *)343 341 344 342 lemma set_8051_sfr_status_of_pseudo_status: … … 350 348 (set_8051_sfr pseudo_assembly_program code_memory s sfr v) sigma policy. 351 349 #M #code_memory #sigma #policy #s #s' #sfr #v #v' #s_ok #v_ok 352 <s_ok whd in ⊢ (??%%); @split_eq_status try % /2/ 353 qed. 354 355 (* 350 <s_ok whd in ⊢ (??%%); @split_eq_status try % /2 by set_index_status_of_pseudo_status/ 351 qed. 352 353 (*lemma get_8051_sfr_status_of_pseudo_status: 354 ∀M. 355 ∀cm, ps, sigma, policy. 356 ∀sfr. 357 (sfr = SFR_ACC_A → \snd M = None …) → 358 get_8051_sfr (BitVectorTrie Byte 16) 359 (code_memory_of_pseudo_assembly_program cm sigma policy) 360 (status_of_pseudo_status M cm ps sigma policy) sfr = 361 get_8051_sfr pseudo_assembly_program cm ps sfr. 362 #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant 363 [18: >relevant % ] 364 cases sndM try % * #address 365 whd in match get_8051_sfr; 366 whd in match status_of_pseudo_status; normalize nodelta 367 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address 368 cases (eq_upper_lower ??) normalize nodelta 369 @pair_elim #upper #lower #upper_lower_refl 370 @get_index_v_set_index_miss @nmk #relevant 371 normalize in relevant; destruct(relevant) 372 qed.*) 373 356 374 lemma get_8051_sfr_status_of_pseudo_status: 357 375 ∀M, code_memory, sigma, policy, s, s', s'', sfr. … … 365 383 whd in match get_8051_sfr; normalize nodelta 366 384 @get_index_v_status_of_pseudo_status % 367 qed. *)385 qed. 368 386 369 387 lemma get_8052_sfr_status_of_pseudo_status: … … 537 555 (low_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' → 538 556 lookup Byte 7 addr 539 (low_internal_ram_of_pseudo_low_internal_ram M 557 (low_internal_ram_of_pseudo_low_internal_ram M sigma 540 558 (low_internal_ram pseudo_assembly_program cm s)) (zero 8) 541 559 = s'. … … 549 567 (high_internal_ram pseudo_assembly_program cm s) (zero 8)) = s' → 550 568 lookup Byte 7 addr 551 (high_internal_ram_of_pseudo_high_internal_ram M 569 (high_internal_ram_of_pseudo_high_internal_ram M sigma 552 570 (high_internal_ram pseudo_assembly_program cm s)) (zero 8) 553 571 = s'. … … 606 624 definition map_address_mode_using_internal_pseudo_address_map_ok1 ≝ 607 625 λM:internal_pseudo_address_map.λcm.λs:PreStatus ? cm.λsigma. λaddr. 626 let 〈low,high,accA〉 ≝ M in 608 627 match addr with 609 628 [ INDIRECT i ⇒ 610 assoc_list_lookup ??611 ( false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M)= None …629 lookup_opt … 630 (bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) low = None … 612 631 | EXT_INDIRECT e ⇒ 613 assoc_list_lookup ??614 ( false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) (eq_bv …) (\fst M)= None …632 lookup_opt … 633 (bit_address_of_register pseudo_assembly_program cm s [[false; false; e]]) low = None … 615 634 | ACC_DPTR ⇒ 616 635 (* XXX: \snd M = None plus in the very rare case when we are trying to dereference a null (O) pointer … … 697 716 set_low_internal_ram ?? s memory 698 717 ] 718 699 719 | INDIRECT i ⇒ 700 720 λindirect: True. … … 734 754 [ >(vsplit_ok … vsplit_refl) #_ @set_bit_addressable_sfr_status_of_pseudo_status 735 755 | #_ #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] 736 |3,4: #EQ1 #EQ2 change with (get_register ????) in match register in p; 756 |3,4: cases M * -M #low #high #accA normalize nodelta 757 #EQ1 #EQ2 change with (get_register ????) in match register in p; 737 758 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 738 759 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 760 whd in match (lookup_from_internal_ram ??); 739 761 >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta 740 762 [ >(insert_high_internal_ram_status_of_pseudo_status … v) 741 763 | >(insert_low_internal_ram_status_of_pseudo_status … v) ] 742 764 // <EQ2 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 743 |5: #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 765 |5: cases M * -M #low #high #accA normalize nodelta 766 #EQ1 #EQ2 <EQ2 >(get_register_status_of_pseudo_status … (refl …) (refl …)) 744 767 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 768 whd in match lookup_from_internal_ram; normalize nodelta 745 769 >EQ1 normalize nodelta 746 770 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status … … 957 981 #_>p normalize nodelta >p1 normalize nodelta 958 982 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma) % 959 |3,4: 983 |3,4: cases M -M * #low #high #accA 960 984 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …)) 961 985 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 986 whd in match lookup_from_internal_ram; normalize nodelta 962 987 >assoc_list_assm normalize nodelta >p normalize nodelta >p1 normalize nodelta 963 988 [1: 964 @(lookup_high_internal_ram_of_pseudo_high_internal_ram … sigma)989 @(lookup_high_internal_ram_of_pseudo_high_internal_ram … 〈low,high,accA〉 sigma) 965 990 |2: 966 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma)991 @(lookup_low_internal_ram_of_pseudo_low_internal_ram … 〈low,high,accA〉 sigma) 967 992 ] 968 993 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % 969 |5: 994 |5: cases M -M * #low #high #accA 970 995 #assoc_list_assm >(get_register_status_of_pseudo_status … (refl …) (refl …)) 971 996 whd in match map_internal_ram_address_using_pseudo_address_map in ⊢ (??%?); normalize nodelta 997 whd in match lookup_from_internal_ram; normalize nodelta 972 998 >assoc_list_assm normalize nodelta % 973 999 |6,7,8,9: 974 1000 #_ /2 by refl, get_register_status_of_pseudo_status, get_index_v_status_of_pseudo_status/ 975 |10: 1001 |10: cases M -M * #low #high #accA 976 1002 #acc_a_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 977 1003 >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) … … 979 1005 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta 980 1006 >acc_a_assm >p normalize nodelta // 981 |11: 1007 |11: cases M -M * #low #high #accA 982 1008 * #map_acc_a_assm #sigma_assm >(get_8051_sfr_status_of_pseudo_status … (refl …) (refl …)) 983 1009 >(program_counter_status_of_pseudo_status … (refl …) (refl …)) … … 1048 1074 match head' … bit_1 with 1049 1075 [ true ⇒ 1050 let address ≝ nat_of_bitvector … seven_bits in 1051 let d ≝ address ÷ 8 in 1052 let m ≝ address mod 8 in 1053 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1076 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1077 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1054 1078 map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l 1055 1079 | false ⇒ 1056 let address ≝ nat_of_bitvector …seven_bits in1057 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1080 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1081 let address' ≝ [[true; false; false]]@@four_bits in 1058 1082 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1059 1083 map_internal_ram_address_using_pseudo_address_map M sigma 1060 1084 (false:::address') t = t 1061 1085 ] … … 1064 1088 match head' … bit_1 with 1065 1089 [ true ⇒ 1066 let address ≝ nat_of_bitvector … seven_bits in 1067 let d ≝ address ÷ 8 in 1068 let m ≝ address mod 8 in 1069 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1090 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1091 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1070 1092 map_address_Byte_using_internal_pseudo_address_map M sigma trans (get_bit_addressable_sfr pseudo_assembly_program cm s trans l) = get_bit_addressable_sfr … cm s trans l 1071 1093 | false ⇒ 1072 let address ≝ nat_of_bitvector …seven_bits in1073 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1094 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1095 let address' ≝ [[true; false; false]]@@four_bits in 1074 1096 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1075 1097 map_internal_ram_address_using_pseudo_address_map M sigma 1076 1098 (false:::address') t = t 1077 1099 ] … … 1100 1122 match head' … bit_1 with 1101 1123 [ true ⇒ 1102 let address ≝ nat_of_bitvector … seven_bits in 1103 let d ≝ address ÷ 8 in 1104 let m ≝ address mod 8 in 1105 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1124 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1125 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1106 1126 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 1107 get_index_v … sfr m?1127 get_index_v … sfr (nat_of_bitvector … three_bits) ? 1108 1128 | false ⇒ 1109 let address ≝ nat_of_bitvector …seven_bits in1110 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1129 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1130 let address' ≝ [[true; false; false]]@@four_bits in 1111 1131 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1112 get_index_v … t ( modulus address 8) ?1132 get_index_v … t (nat_of_bitvector … three_bits) ? 1113 1133 ] 1114 1134 | N_BIT_ADDR n ⇒ … … 1117 1137 match head' … bit_1 with 1118 1138 [ true ⇒ 1119 let address ≝ nat_of_bitvector … seven_bits in 1120 let d ≝ address ÷ 8 in 1121 let m ≝ address mod 8 in 1122 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1139 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1140 let trans ≝ true:::four_bits @@ [[false; false; false]] in 1123 1141 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 1124 ¬(get_index_v … sfr m?)1142 ¬(get_index_v ?? sfr (nat_of_bitvector … three_bits) ?) 1125 1143 | false ⇒ 1126 let address ≝ nat_of_bitvector …seven_bits in1127 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32)in1144 let 〈four_bits, three_bits〉 ≝ vsplit bool 4 3 seven_bits in 1145 let address' ≝ [[true; false; false]]@@four_bits in 1128 1146 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1129 ¬(get_index_v … t ( modulus address 8) ?)1147 ¬(get_index_v … t (nat_of_bitvector … three_bits) ?) 1130 1148 ] 1131 1149 | CARRY ⇒ λcarry: True. get_cy_flag ?? s … … 1133 1151 match other in False with [ ] 1134 1152 ] (subaddressing_modein … a)) normalize nodelta 1135 try @modulus_less_than1153 [4,5,8,9: //] 1136 1154 #M #sigma #policy #s' #s_refl <s_refl 1137 1155 [1: 1138 1156 #_ >(get_cy_flag_status_of_pseudo_status … (refl …)) % 1139 1157 |2,4: 1140 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1158 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta destruct >p2 1159 normalize nodelta 1141 1160 >(get_bit_addressable_sfr_status_of_pseudo_status … (refl …) (refl …)) #map_address_assm 1142 1161 >map_address_assm % 1143 1162 |3,5: 1144 1163 whd in ⊢ (% → ?); >p normalize nodelta >p1 normalize nodelta 1145 whd in match status_of_pseudo_status; normalize nodelta 1164 whd in match status_of_pseudo_status; normalize nodelta destruct >p2 normalize nodelta 1146 1165 >(lookup_low_internal_ram_of_pseudo_low_internal_ram … sigma … (refl …)) 1147 1166 #map_address_assm >map_address_assm % … … 1167 1186 qed. 1168 1187 1188 (*CSC: daemon 1169 1189 definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝ 1170 1190 λM: internal_pseudo_address_map. … … 1321 1341 cases (set_arg_1_status_of_pseudo_status' cm ps addr b) #_ #relevant 1322 1342 @relevant 1323 qed. 1343 qed.*) 1324 1344 1325 1345 lemma clock_status_of_pseudo_status: … … 1344 1364 qed. 1345 1365 1366 (*CSC: daemon 1346 1367 lemma set_flags_status_of_pseudo_status: 1347 1368 ∀M. … … 1367 1388 [1: 1368 1389 normalize nodelta % 1369 |2: 1370 * #address normalize nodelta 1390 |2: ** #address normalize nodelta 1371 1391 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1372 1392 whd in ⊢ (??%%); cases opt try #opt' normalize nodelta … … 1374 1394 cases daemon 1375 1395 ] 1376 qed. 1396 qed.*) 1377 1397 1378 1398 lemma get_ac_flag_status_of_pseudo_status: … … 1389 1409 whd in match status_of_pseudo_status; normalize nodelta 1390 1410 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1391 cases (\snd M) try % 1392 * normalize nodelta#address1411 cases (\snd M) try % normalize nodelta ** normalize nodelta 1412 #address 1393 1413 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1394 1414 whd in match sfr_8051_index; normalize nodelta … … 1410 1430 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1411 1431 cases (\snd M) try % 1412 * normalize nodelta #address1432 ** normalize nodelta #address 1413 1433 @(vsplit_elim bool ???) #high #low #high_low_refl normalize nodelta 1414 1434 whd in match sfr_8051_index; normalize nodelta … … 1416 1436 qed. 1417 1437 1418 lemma get_8051_sfr_status_of_pseudo_status: 1419 ∀M. 1420 ∀cm, ps, sigma, policy. 1421 ∀sfr. 1422 (sfr = SFR_ACC_A → \snd M = None …) → 1423 get_8051_sfr (BitVectorTrie Byte 16) 1424 (code_memory_of_pseudo_assembly_program cm sigma policy) 1425 (status_of_pseudo_status M cm ps sigma policy) sfr = 1426 get_8051_sfr pseudo_assembly_program cm ps sfr. 1427 #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant 1428 [18: 1429 >relevant % 1430 ] 1431 cases sndM try % * #address 1432 whd in match get_8051_sfr; 1433 whd in match status_of_pseudo_status; normalize nodelta 1434 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta #address 1435 cases (eq_upper_lower ??) normalize nodelta 1436 @pair_elim #upper #lower #upper_lower_refl 1437 @get_index_v_set_index_miss @nmk #relevant 1438 normalize in relevant; destruct(relevant) 1439 qed. 1440 1438 (*CSC: useless? 1441 1439 lemma get_arg_8_pseudo_addressing_mode_ok: 1442 1440 ∀M: internal_pseudo_address_map. … … 1485 1483 |2: 1486 1484 #addressing_mode_ok_refl whd in ⊢ (??%?); 1487 @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (*1485 @pair_elim #nu #nl #nu_nl_refl normalize nodelta XXX cases daemon (* 1488 1486 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta 1489 1487 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta … … 1610 1608 ] 1611 1609 ] 1612 ] *) 1613 qed. 1610 ] 1611 qed.*)*) 1612 1613 lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map: 1614 ∀M, cm, ps, sigma, x. 1615 ∀addr1: [[acc_a]]. 1616 assert_data pseudo_assembly_program M cm ps addr1=true → 1617 map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x. 1618 #M #cm #ps #sigma #x #addr1 1619 @(subaddressing_mode_elim … addr1) 1620 whd in ⊢ (??%? → ??%?); cases M -M * #low #high * [//] 1621 * #upper_lower #address normalize nodelta #absurd destruct(absurd) 1622 qed. 1623 1624 lemma addressing_mode_ok_to_snd_M_data: 1625 ∀M, cm, ps. 1626 ∀addr: [[acc_a]]. 1627 assert_data pseudo_assembly_program M cm ps addr = true → 1628 \snd M = None …. 1629 #M #cm #ps #addr 1630 @(subaddressing_mode_elim … addr) 1631 whd in ⊢ (??%? → ?); cases M * #low #high * normalize nodelta 1632 [ #_ % 1633 | #addr #abs destruct(abs) ] 1634 qed. 1635 1636 (*(*CSC: move elsewhere*) 1637 lemma assoc_list_exists_true_to_assoc_list_lookup_Some: 1638 ∀A, B: Type[0]. 1639 ∀e: A. 1640 ∀the_list: list (A × B). 1641 ∀eq_f: A → A → bool. 1642 assoc_list_exists A B e eq_f the_list = true → 1643 ∃e'. assoc_list_lookup A B e eq_f the_list = Some … e'. 1644 #A #B #e #the_list #eq_f elim the_list 1645 [1: 1646 whd in ⊢ (??%? → ?); #absurd destruct(absurd) 1647 |2: 1648 #hd #tl #inductive_hypothesis 1649 whd in ⊢ (??%? → ?); whd in match (assoc_list_lookup ?????); 1650 cases (eq_f (\fst hd) e) normalize nodelta 1651 [1: 1652 #_ %{(\snd hd)} % 1653 |2: 1654 @inductive_hypothesis 1655 ] 1656 ] 1657 qed. 1658 1659 (*CSC: move elsewhere*) 1660 lemma assoc_list_exists_false_to_assoc_list_lookup_None: 1661 ∀A, B: Type[0]. 1662 ∀e, e': A. 1663 ∀the_list, the_list': list (A × B). 1664 ∀eq_f: A → A → bool. 1665 e = e' → 1666 the_list = the_list' → 1667 assoc_list_exists A B e eq_f the_list = false → 1668 assoc_list_lookup A B e' eq_f the_list' = None …. 1669 #A #B #e #e' #the_list elim the_list 1670 [1: 1671 #the_list' #eq_f #e_refl <e_refl #the_list_refl <the_list_refl #_ % 1672 |2: 1673 #hd #tl #inductive_hypothesis #the_list' #eq_f #e_refl #the_list_refl <the_list_refl 1674 whd in ⊢ (??%? → ??%?); <e_refl 1675 cases (eq_f (\fst hd) e) normalize nodelta 1676 [1: 1677 #absurd destruct(absurd) 1678 |2: 1679 >e_refl in ⊢ (? → %); @inductive_hypothesis try % assumption 1680 ] 1681 ] 1682 qed.*) 1683 1684 lemma sfr_psw_eq_to_bit_address_of_register_eq: 1685 ∀A: Type[0]. 1686 ∀code_memory: A. 1687 ∀status, status', register_address. 1688 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 1689 bit_address_of_register A code_memory status register_address = bit_address_of_register A code_memory status' register_address. 1690 #A #code_memory #status #status' #register_address #sfr_psw_refl 1691 whd in match bit_address_of_register; normalize nodelta 1692 <sfr_psw_refl % 1693 qed. 1694 1695 lemma sfr_psw_and_low_internal_ram_eq_to_get_register_eq: 1696 ∀A: Type[0]. 1697 ∀code_memory: A. 1698 ∀status, status', register_address. 1699 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 1700 low_internal_ram A code_memory status = low_internal_ram A code_memory status' → 1701 get_register A code_memory status register_address = get_register A code_memory status' register_address. 1702 #A #code_memory #status #status' #register_address #sfr_psw_refl #low_internal_ram_refl 1703 whd in match get_register; normalize nodelta <low_internal_ram_refl 1704 >(sfr_psw_eq_to_bit_address_of_register_eq … status status') // 1705 qed. 1706 1707 lemma map_address_mode_using_internal_pseudo_address_map_ok1_addr: 1708 ∀M, cm, status, status', sigma. 1709 ∀addr1: [[acc_a; registr; direct; indirect; data; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) 1710 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 1711 assert_data pseudo_assembly_program M cm status addr1 = true → 1712 map_address_mode_using_internal_pseudo_address_map_ok1 M cm status' sigma addr1. 1713 * * #low #high #accA #cm #status #status' #sigma #addr1 #sfr_refl 1714 @(subaddressing_mode_elim … addr1) try (#w #_ @I) [1,4: #_ @I ] #w 1715 whd in ⊢ (??%? → %); whd in match (data_or_address ?????); 1716 whd in match exists; normalize nodelta 1717 <(sfr_psw_eq_to_bit_address_of_register_eq … status status') try assumption 1718 cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) 1719 qed. 1720 1721 lemma sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map: 1722 ∀M. 1723 ∀sigma. 1724 ∀sfr8051. 1725 ∀b. 1726 sfr8051 ≠ SFR_ACC_A → 1727 map_address_using_internal_pseudo_address_map M sigma sfr8051 b = b. 1728 #M #sigma * #b 1729 [18: 1730 #relevant cases (absurd … (refl ??) relevant) 1731 ] 1732 #_ % 1733 qed. 1734 1735 lemma w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map: 1736 ∀M. 1737 ∀sigma: Word → Word. 1738 ∀w: BitVector 8. 1739 ∀b. 1740 w ≠ bitvector_of_nat … 224 → 1741 map_address_Byte_using_internal_pseudo_address_map M sigma w b = b. 1742 #M #sigma #w #b #w_neq_assm 1743 whd in ⊢ (??%?); inversion (sfr_of_Byte ?) 1744 [1: 1745 #sfr_of_Byte_refl % 1746 |2: 1747 * #sfr8051 #sfr_of_Byte_refl normalize nodelta try % 1748 @sfr8051_neq_acc_a_to_map_address_using_internal_pseudo_address_map % 1749 #relevant >relevant in sfr_of_Byte_refl; #sfr_of_Byte_refl 1750 @(absurd ?? w_neq_assm) 1751 lapply sfr_of_Byte_refl -b -sfr_of_Byte_refl -relevant -w_neq_assm -sfr8051 -sigma 1752 whd in match sfr_of_Byte; normalize nodelta 1753 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1754 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1755 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1756 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1757 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1758 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1759 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1760 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1761 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1762 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1763 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1764 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1765 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1766 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1767 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1768 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1769 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1770 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1771 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1772 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1773 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1774 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1775 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1776 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1777 @eqb_elim #eqb_refl normalize nodelta [1: #_ <eqb_refl >bitvector_of_nat_inverse_nat_of_bitvector % ] 1778 cases (eqb ??) normalize nodelta [1: #absurd destruct(absurd) ] 1779 #absurd destruct(absurd) 1780 qed. 1781 1782 (*lemma assoc_list_exists_false_to_map_internal_ram_address_using_pseudo_address_map: 1783 ∀M, sigma, w, b. 1784 assoc_list_exists Byte (upper_lower×Word) w (eq_bv 8) (\fst M) = false → 1785 map_internal_ram_address_using_pseudo_address_map M sigma w b = b. 1786 #M #sigma #w #b #assoc_list_exists_assm 1787 whd in ⊢ (??%?); 1788 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) … assoc_list_exists_assm) % 1789 qed.*) 1790 1791 lemma addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2: 1792 ∀M', cm. 1793 ∀sigma, status, status', b, b'. 1794 ∀addr1: [[acc_a; registr; direct; indirect; data; bit_addr; ext_indirect; ext_indirect_dptr]]. (* XXX: expand as needed *) 1795 get_8051_sfr … status SFR_PSW = get_8051_sfr … status' SFR_PSW → 1796 low_internal_ram pseudo_assembly_program cm status = low_internal_ram pseudo_assembly_program cm status' → 1797 b = b' → 1798 assert_data pseudo_assembly_program M' cm status addr1 = true → 1799 map_address_mode_using_internal_pseudo_address_map_ok2 pseudo_assembly_program M' sigma cm status' addr1 b = b'. 1800 #M' #cm #sigma #status #status' #b #b' #addr1 #sfr_refl #low_internal_ram_refl #b_refl <b_refl 1801 @(subaddressing_mode_elim … addr1) 1802 [1: 1803 whd in ⊢ (??%? → ??%?); cases M' -M' * #low #high * 1804 [1: 1805 normalize nodelta #_ % 1806 |2: 1807 * #upper_lower #address normalize nodelta #absurd destruct(absurd) 1808 ] 1809 |2: cases M' -M' * #low #high #accA 1810 #w whd in ⊢ (??%? → ??%?); whd in match (lookup_from_internal_ram ??); 1811 <(sfr_psw_eq_to_bit_address_of_register_eq … status status' w … sfr_refl) 1812 cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) 1813 |4: cases M' -M' * #low #high #accA 1814 #w whd in ⊢ (??%? → ??%?); whd in match lookup_from_internal_ram; 1815 whd in match data_or_address; normalize nodelta whd in match exists; normalize nodelta 1816 whd in match get_register; normalize nodelta 1817 <(sfr_psw_eq_to_bit_address_of_register_eq … status status' … sfr_refl) 1818 cases (lookup_opt ????) normalize nodelta [2: #_ #abs destruct(abs)] 1819 <low_internal_ram_refl @vsplit_elim #one #seven #EQone_seven normalize nodelta 1820 cases (head' bool ??) normalize nodelta cases (lookup_opt ????) normalize nodelta 1821 #x try % #abs destruct(abs) 1822 |3: cases M' -M' * #low #high #accA 1823 #w whd in ⊢ (??%? → ??%?); whd in match data_or_address; normalize nodelta 1824 @vsplit_elim #hd #tl #w_refl normalize nodelta 1825 lapply (eq_head' ?? … hd) >(Vector_O … (tail … hd)) 1826 cases (head' bool ??) normalize nodelta 1827 [2: #_ whd in match (map_internal_ram_address_using_pseudo_address_map ????); 1828 whd in match (lookup_from_internal_ram ??); cases (lookup_opt ????); 1829 normalize nodelta // #x #abs destruct(abs) ] #EQhd 1830 >w_refl >EQhd @eq_bv_elim #eq_bv_refl normalize nodelta 1831 [1: cases accA normalize nodelta try (#x #abs destruct(abs)) #_ 1832 normalize in eq_bv_refl; >eq_bv_refl % 1833 |2: #_ @w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map assumption ] 1834 |5,6,7,8: 1835 #w try #w' % 1836 ] 1837 qed. 1838 1839 (*CSC: move elsewhere*) 1840 lemma bv_append_eq_to_eq: 1841 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m. 1842 v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4. 1843 #A #n #v1 elim v1 1844 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %% 1845 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2 1846 #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ] 1847 qed. 1848 1849 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_get: 1850 ∀M: internal_pseudo_address_map. 1851 ∀cm: pseudo_assembly_program. 1852 ∀s: PreStatus pseudo_assembly_program cm. 1853 ∀sigma: Word → Word. 1854 ∀addr: [[bit_addr]]. (* XXX: expand as needed *) 1855 ∀f: bool. 1856 assert_data pseudo_assembly_program M cm s addr = true → 1857 map_bit_address_mode_using_internal_pseudo_address_map_get M cm s sigma addr f. 1858 ** #low #high #accA #cm #s #sigma #addr #f 1859 @(subaddressing_mode_elim … addr) #w 1860 whd in ⊢ (??%? → %); whd in match data_or_address; normalize nodelta 1861 @vsplit_elim #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta 1862 @vsplit_elim #four #three #four_three_refl normalize nodelta 1863 cases (head' bool ??) normalize nodelta 1864 [1: @eq_bv_elim normalize nodelta 1865 [1: #EQfour cases accA normalize nodelta #x [2: #abs destruct(abs)] >EQfour % 1866 |2: #NEQ #_ >w_neq_224_to_map_address_Byte_using_internal_pseudo_address_map 1867 try % normalize #EQ @(absurd ?? NEQ) 1868 cases (bv_append_eq_to_eq … [[true]] [[true]] … EQ) #_ #EQ1 1869 cases (bv_append_eq_to_eq … four [[true;true;false;false]] … EQ1) // ] 1870 |2: whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 1871 whd in match lookup_from_internal_ram; normalize nodelta 1872 cases (lookup_opt ????); normalize nodelta #x try % #abs destruct(abs) ] 1873 qed. 1874 1875 (* 1876 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_1: 1877 ∀M: internal_pseudo_address_map. 1878 ∀cm: pseudo_assembly_program. 1879 ∀s, s': PreStatus pseudo_assembly_program cm. 1880 ∀sigma: Word → Word. 1881 ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *) 1882 ∀f: bool. 1883 s = s' → 1884 addressing_mode_ok pseudo_assembly_program M cm s addr = true → 1885 map_bit_address_mode_using_internal_pseudo_address_map_set_1 M cm s' sigma addr f. 1886 #M #cm #s #s' #sigma #addr #f #s_refl <s_refl 1887 @(subaddressing_mode_elim … addr) [1: #w ] 1888 whd in ⊢ (??%? → %); [2: #_ @I ] 1889 inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta 1890 cases (head' bool ??) normalize nodelta 1891 [1: 1892 #eq_accumulator_assm whd in ⊢ (??%?); 1893 cases (sfr_of_Byte ?) try % * * try % normalize nodelta 1894 whd in ⊢ (??%?); 1895 >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) % 1896 |2: 1897 #assoc_list_exists_assm whd in ⊢ (??%?); 1898 lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm 1899 whd in assoc_list_exists_assm:(???%); 1900 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) % 1901 ] 1902 qed. 1903 1904 lemma addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2: 1905 ∀M: internal_pseudo_address_map. 1906 ∀cm: pseudo_assembly_program. 1907 ∀s, s': PreStatus pseudo_assembly_program cm. 1908 ∀sigma: Word → Word. 1909 ∀addr: [[bit_addr; carry]]. (* XXX: expand as needed *) 1910 ∀f: bool. 1911 s = s' → 1912 addressing_mode_ok pseudo_assembly_program M cm s addr = true → 1913 map_bit_address_mode_using_internal_pseudo_address_map_set_2 M cm s' sigma addr f. 1914 #M #cm #s #s' #sigma #addr #f #s_refl <s_refl 1915 @(subaddressing_mode_elim … addr) [1: #w ] 1916 whd in ⊢ (??%? → %); [2: #_ @I ] 1917 inversion (vsplit bool 1 7 w) #bit_one #seven_bits #bit_one_seven_bits_refl normalize nodelta 1918 cases (head' bool ??) normalize nodelta 1919 [1: 1920 #eq_accumulator_assm whd in ⊢ (??%?); 1921 cases (sfr_of_Byte ?) try % * * try % normalize nodelta 1922 whd in ⊢ (??%?); 1923 >(eq_accumulator_address_map_entry_true_to_eq … eq_accumulator_assm) % 1924 |2: 1925 #assoc_list_exists_assm whd in ⊢ (??%?); 1926 lapply (not_b_c_to_b_not_c ?? assoc_list_exists_assm) -assoc_list_exists_assm #assoc_list_exists_assm 1927 whd in assoc_list_exists_assm:(???%); 1928 >(assoc_list_exists_false_to_assoc_list_lookup_None … (refl …) assoc_list_exists_assm) % 1929 ] 1930 qed.*) 1931 1932 (* 1933 axiom insert_low_internal_ram_of_pseudo_low_internal_ram': 1934 ∀M, M', sigma,cm,s,addr,v,v'. 1935 (∀addr'. 1936 ((false:::addr) = addr' → 1937 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = 1938 map_internal_ram_address_using_pseudo_address_map M' sigma (false:::addr) v') ∧ 1939 ((false:::addr) ≠ addr' → 1940 let 〈callM, accM〉 ≝ M in 1941 let 〈callM', accM'〉 ≝ M' in 1942 accM = accM' ∧ 1943 assoc_list_lookup … addr' (eq_bv 8) … callM = 1944 assoc_list_lookup … addr' (eq_bv 8) … callM')) → 1945 insert Byte 7 addr v' 1946 (low_internal_ram_of_pseudo_low_internal_ram M' 1947 (low_internal_ram pseudo_assembly_program cm s)) = 1948 low_internal_ram_of_pseudo_low_internal_ram M 1949 (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). 1950 *) 1951 1952 (* 1953 lemma write_at_stack_pointer_status_of_pseudo_status: 1954 ∀M, M'. 1955 ∀cm. 1956 ∀sigma. 1957 ∀policy. 1958 ∀s, s'. 1959 ∀new_b, new_b'. 1960 map_internal_ram_address_using_pseudo_address_map M sigma (get_8051_sfr pseudo_assembly_program cm s SFR_SP) new_b = new_b' → 1961 status_of_pseudo_status M cm s sigma policy = s' → 1962 write_at_stack_pointer ?? s' new_b' = 1963 status_of_pseudo_status M' cm (write_at_stack_pointer ? cm s new_b) sigma policy. 1964 #M #M' #cm #sigma #policy #s #s' #new_b #new_b' 1965 #new_b_refl #s_refl <new_b_refl <s_refl 1966 whd in match write_at_stack_pointer; normalize nodelta 1967 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 1968 @(pair_replace ?????????? (eq_to_jmeq … nu_nl_refl)) 1969 [1: 1970 @eq_f 1971 whd in match get_8051_sfr; normalize nodelta 1972 whd in match sfr_8051_index; normalize nodelta 1973 whd in match status_of_pseudo_status; normalize nodelta 1974 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 1975 cases (\snd M) [2: * #address ] normalize nodelta 1976 [1,2: 1977 cases (vsplit bool ???) #high #low normalize nodelta 1978 whd in match sfr_8051_index; normalize nodelta 1979 >get_index_v_set_index_miss % 1980 #absurd destruct(absurd) 1981 |3: 1982 % 1983 ] 1984 |2: 1985 @if_then_else_status_of_pseudo_status try % 1986 [2: 1987 @sym_eq <set_low_internal_ram_status_of_pseudo_status 1988 [1: 1989 @eq_f2 1990 [2: 1991 @insert_low_internal_ram_of_pseudo_low_internal_ram' 1992 @sym_eq 1993 [2: 1994 <set_low_internal_ram_status_of_pseudo_status 1995 [1: 1996 @eq_f2 1997 [2: 1998 @sym_eq 1999 >(insert_low_internal_ram_of_pseudo_low_internal_ram … sigma … new_b') 2000 [2: 2001 >new_b_refl 2002 ] 2003 ] 2004 qed.*)
Note: See TracChangeset
for help on using the changeset viewer.