- Timestamp:
- Jul 10, 2012, 2:39:38 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2160 r2172 1 include "ASM/AssemblyProof.ma". 2 include alias "arithmetics/nat.ma". 3 include alias "basics/logic.ma". 4 5 lemma set_arg_16_mk_Status_commutation: 6 ∀M: Type[0]. 7 ∀cm: M. 8 ∀s: PreStatus M cm. 9 ∀w: Word. 10 ∀d: [[dptr]]. 11 set_arg_16 M cm s w d = 12 mk_PreStatus M cm 13 (low_internal_ram … s) 14 (high_internal_ram … s) 15 (external_ram … s) 16 (program_counter … s) 17 (special_function_registers_8051 … (set_arg_16 M cm s w d)) 18 (special_function_registers_8052 … s) 19 (p1_latch … s) 20 (p3_latch … s) 21 (clock … s). 22 #M #cm #s #w #d 23 whd in match set_arg_16; normalize nodelta 24 whd in match set_arg_16'; normalize nodelta 25 @(subaddressing_mode_elim … d) 26 cases (vsplit bool 8 8 w) #bu #bl normalize nodelta 27 whd in match set_8051_sfr; normalize nodelta % 28 qed. 29 30 lemma set_program_counter_mk_Status_commutation: 31 ∀M: Type[0]. 32 ∀cm: M. 33 ∀s: PreStatus M cm. 34 ∀w: Word. 35 set_program_counter M cm s w = 36 mk_PreStatus M cm 37 (low_internal_ram … s) 38 (high_internal_ram … s) 39 (external_ram … s) 40 w 41 (special_function_registers_8051 … s) 42 (special_function_registers_8052 … s) 43 (p1_latch … s) 44 (p3_latch … s) 45 (clock … s). 46 // 47 qed. 48 49 lemma set_clock_mk_Status_commutation: 50 ∀M: Type[0]. 51 ∀cm: M. 52 ∀s: PreStatus M cm. 53 ∀c: nat. 54 set_clock M cm s c = 55 mk_PreStatus M cm 56 (low_internal_ram … s) 57 (high_internal_ram … s) 58 (external_ram … s) 59 (program_counter … s) 60 (special_function_registers_8051 … s) 61 (special_function_registers_8052 … s) 62 (p1_latch … s) 63 (p3_latch … s) 64 c. 65 // 66 qed. 67 68 lemma get_8051_sfr_set_clock: 69 ∀M: Type[0]. 70 ∀cm: M. 71 ∀s: PreStatus M cm. 72 ∀sfr: SFR8051. 73 ∀t: Time. 74 get_8051_sfr M cm (set_clock M cm s t) sfr = 75 get_8051_sfr M cm s sfr. 76 #M #cm #s #sfr #t % 77 qed. 78 79 lemma get_8051_sfr_set_program_counter: 80 ∀M: Type[0]. 81 ∀cm: M. 82 ∀s: PreStatus M cm. 83 ∀sfr: SFR8051. 84 ∀pc: Word. 85 get_8051_sfr M cm (set_program_counter M cm s pc) = 86 get_8051_sfr M cm s. 87 #M #cm #s #sfr #pc % 88 qed. 89 90 lemma special_function_registers_8051_set_arg_16: 91 ∀M, M': Type[0]. 92 ∀cm: M. 93 ∀cm': M'. 94 ∀s: PreStatus M cm. 95 ∀s': PreStatus M' cm'. 96 ∀w, w': Word. 97 ∀d, d': [[dptr]]. 98 special_function_registers_8051 ?? s = special_function_registers_8051 … s' → 99 w = w' → 100 special_function_registers_8051 ?? (set_arg_16 … s w d) = 101 special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d'). 102 #M #M' #cm #cm' #s #s' #w #w' 103 #d @(subaddressing_mode_elim … d) 104 #d' @(subaddressing_mode_elim … d') 105 #EQ1 #EQ2 <EQ2 normalize cases (vsplit bool 8 8 w) #b1 #b2 normalize <EQ1 % 106 qed. 107 108 lemma program_counter_set_arg_1: 109 ∀M: Type[0]. 110 ∀cm: M. 111 ∀s: PreStatus M cm. 112 ∀addr: [[bit_addr; carry]]. 113 ∀b: Bit. 114 program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s. 115 #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta 116 #addr #b 117 @(subaddressing_mode_elim … addr) 118 [1: 119 #byte cases (vsplit ????) #nu #nl normalize nodelta 120 cases (vsplit ????) #ignore #three_bits normalize nodelta 121 cases (get_index_v bool ????) normalize nodelta 122 [1: 123 @program_counter_set_bit_addressable_sfr 124 |2: 125 @program_counter_set_low_internal_ram 126 ] 127 |2: 128 cases (vsplit ????) // 129 ] 130 qed. 131 132 lemma get_ov_flag_set_program_counter: 133 ∀M: Type[0]. 134 ∀cm: M. 135 ∀s: PreStatus M cm. 136 ∀pc: Word. 137 get_ov_flag M cm (set_program_counter M cm s pc) = 138 get_ov_flag M cm s. 139 #M #cm #s #pc % 140 qed. 141 142 lemma external_ram_set_program_counter: 143 ∀M: Type[0]. 144 ∀cm: M. 145 ∀s: PreStatus M cm. 146 ∀pc: Word. 147 external_ram M cm (set_program_counter M cm s pc) = 148 external_ram M cm s. 149 #M #cm #s #pc % 150 qed. 151 152 lemma low_internal_ram_set_program_counter: 153 ∀M: Type[0]. 154 ∀cm: M. 155 ∀s: PreStatus M cm. 156 ∀pc: Word. 157 low_internal_ram M cm (set_program_counter M cm s pc) = 158 low_internal_ram M cm s. 159 #M #cm #s #pc % 160 qed. 161 162 lemma high_internal_ram_set_program_counter: 163 ∀M: Type[0]. 164 ∀cm: M. 165 ∀s: PreStatus M cm. 166 ∀pc: Word. 167 high_internal_ram M cm (set_program_counter M cm s pc) = 168 high_internal_ram M cm s. 169 #M #cm #s #pc % 170 qed. 171 172 lemma get_arg_8_set_program_counter: 173 ∀M: Type[0]. 174 ∀cm: M. 175 ∀s: PreStatus M cm. 176 ∀flag: bool. 177 ∀addr: [[direct; indirect; registr; acc_a; acc_b; data; acc_dptr; ext_indirect; ext_indirect_dptr]]. 178 ∀pc: Word. 179 get_arg_8 M cm (set_program_counter M cm s pc) flag addr = 180 get_arg_8 M cm s flag addr. 181 [2,3: 182 cases addr #subaddressing_mode 183 cases subaddressing_mode 184 try (#addr1 whd in ⊢ (% → %);) 185 whd in ⊢ (% → %); // 186 ] 187 #M #cm #s #flag #addr #pc 188 whd in match get_arg_8; normalize nodelta 189 cases addr * 190 try (#addr1 #absurd normalize in absurd; cases absurd @I) 191 try (#absurd normalize in absurd; cases absurd @I) 192 try (#addr1 #addr2) try #addr1 193 normalize nodelta % 194 qed. 195 196 lemma external_ram_set_flags: 197 ∀M: Type[0]. 198 ∀cm: M. 199 ∀s: PreStatus M cm. 200 ∀opt: option Bit. 201 ∀bit1, bit2: Bit. 202 external_ram M cm (set_flags M cm s bit1 opt bit2) = 203 external_ram M cm s. 204 #M #cm #s #opt #bit1 #bit2 % 205 qed. 206 207 lemma low_internal_ram_set_flags: 208 ∀M: Type[0]. 209 ∀cm: M. 210 ∀s: PreStatus M cm. 211 ∀opt: option Bit. 212 ∀bit1, bit2: Bit. 213 low_internal_ram M cm (set_flags M cm s bit1 opt bit2) = 214 low_internal_ram M cm s. 215 #M #cm #s #opt #bit1 #bit2 % 216 qed. 217 218 lemma high_internal_ram_set_flags: 219 ∀M: Type[0]. 220 ∀cm: M. 221 ∀s: PreStatus M cm. 222 ∀opt: option Bit. 223 ∀bit1, bit2: Bit. 224 high_internal_ram M cm (set_flags M cm s bit1 opt bit2) = 225 high_internal_ram M cm s. 226 #M #cm #s #opt #bit1 #bit2 % 227 qed. 228 229 lemma low_internal_ram_set_clock: 230 ∀M: Type[0]. 231 ∀cm: M. 232 ∀s: PreStatus M cm. 233 ∀t: Time. 234 low_internal_ram M cm (set_clock M cm s t) = 235 low_internal_ram M cm s. 236 #M #cm #s #t % 237 qed. 238 239 lemma high_internal_ram_set_clock: 240 ∀M: Type[0]. 241 ∀cm: M. 242 ∀s: PreStatus M cm. 243 ∀t: Time. 244 high_internal_ram M cm (set_clock M cm s t) = 245 high_internal_ram M cm s. 246 #M #cm #s #t % 247 qed. 248 249 lemma external_ram_set_clock: 250 ∀M: Type[0]. 251 ∀cm: M. 252 ∀s: PreStatus M cm. 253 ∀t: Time. 254 external_ram M cm (set_clock M cm s t) = 255 external_ram M cm s. 256 #M #cm #s #t % 257 qed. 258 259 lemma set_8051_sfr_set_program_counter: 260 ∀M: Type[0]. 261 ∀cm: M. 262 ∀s: PreStatus M cm. 263 ∀pc: Word. 264 ∀sfr: SFR8051. 265 ∀v: Byte. 266 set_8051_sfr M cm (set_program_counter M cm s pc) sfr v = 267 set_program_counter M cm (set_8051_sfr M cm s sfr v) pc. 268 #M #cm #s #pc #sfr #v % 269 qed. 270 271 lemma low_internal_ram_set_8051_sfr: 272 ∀M: Type[0]. 273 ∀cm: M. 274 ∀s: PreStatus M cm. 275 ∀sfr: SFR8051. 276 ∀v: Byte. 277 low_internal_ram M cm (set_8051_sfr M cm s sfr v) = 278 low_internal_ram M cm s. 279 #M #cm #s #sfr #v % 280 qed. 281 282 lemma high_internal_ram_set_8051_sfr: 283 ∀M: Type[0]. 284 ∀cm: M. 285 ∀s: PreStatus M cm. 286 ∀sfr: SFR8051. 287 ∀v: Byte. 288 high_internal_ram M cm (set_8051_sfr M cm s sfr v) = 289 high_internal_ram M cm s. 290 #M #cm #s #sfr #v % 291 qed. 292 293 lemma external_ram_set_8051_sfr: 294 ∀M: Type[0]. 295 ∀cm: M. 296 ∀s: PreStatus M cm. 297 ∀sfr: SFR8051. 298 ∀v: Byte. 299 external_ram M cm (set_8051_sfr M cm s sfr v) = 300 external_ram M cm s. 301 #M #cm #s #sfr #v % 302 qed. 303 304 lemma get_arg_8_set_clock: 305 ∀M: Type[0]. 306 ∀cm: M. 307 ∀s: PreStatus M cm. 308 ∀addr. 309 ∀t: Time. 310 get_arg_8 M cm (set_clock M cm s t) addr = 311 get_arg_8 M cm s addr. 312 #M #cm #s #addr #t % 313 qed. 314 315 lemma set_program_counter_set_program_counter: 316 ∀M: Type[0]. 317 ∀cm: M. 318 ∀s: PreStatus M cm. 319 ∀pc: Word. 320 ∀pc': Word. 321 set_program_counter M cm (set_program_counter M cm s pc) pc' = 322 set_program_counter M cm s pc'. 323 #M #cm #s #pc #pc' % 324 qed. 325 326 (* XXX: move elsewhere *) 327 lemma bitvector_8_cases: 328 ∀w: BitVector 8. 329 ∃b0,b1,b2,b3,b4,b5,b6,b7: bool. 330 w ≃ [[b0;b1;b2;b3;b4;b5;b6;b7]]. 331 #w repeat (cases (BitVector_Sn … w) #b0 * #w0 #EQ0 >EQ0 %{b0} -w lapply w0 -w0 #w) 332 >(BitVector_O … w) % 333 qed. 334 335 (* XXX: not true 336 lemma p3_latch_set_arg_8: 337 ∀M: Type[0]. 338 ∀cm: M. 339 ∀s: PreStatus M cm. 340 ∀args. 341 ∀v: Byte. 342 p3_latch M cm (set_arg_8 M cm s args v) = 343 p3_latch M cm s. 344 #M #cm #s #args #v 345 @(subaddressing_mode_elim … args) 346 try #w try % 347 whd in match set_arg_8; normalize nodelta 348 whd in match set_arg_8'; normalize nodelta 349 inversion (vsplit bool ???) #nu #nl #nu_nl_refl normalize nodelta 350 inversion (vsplit bool ???) #ignore #three_bits #ignore_three_bits_refl normalize nodelta 351 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta try % 352 whd in match set_bit_addressable_sfr; normalize nodelta 353 @(bitvector_8_elim_prop … w) 354 *) 355 356 lemma status_of_pseudo_status_does_not_change_8051_sfrs: 357 ∀M: internal_pseudo_address_map. 358 ∀cm: pseudo_assembly_program. 359 ∀s: PreStatus pseudo_assembly_program cm. 360 ∀sigma: Word → Word. 361 ∀policy: Word → bool. 362 \snd M = data → 363 special_function_registers_8051 pseudo_assembly_program cm s = 364 special_function_registers_8051 (BitVectorTrie Byte 16) 365 (code_memory_of_pseudo_assembly_program cm sigma policy) 366 (status_of_pseudo_status M cm s sigma policy). 367 #M #cm #s #sigma #policy #None_proof cases s 368 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 369 whd in match status_of_pseudo_status; normalize nodelta 370 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 371 >None_proof % 372 qed. 373 374 lemma n_lt_19_elim_prop: 375 ∀P: nat → Prop. 376 P 0 → P 1 → P 2 → P 3 → P 4 → P 5 → P 6 → P 7 → P 8 → P 9 → 377 P 10 → P 11 → P 12 → P 13 → P 14 → P 15 → P 16 → P 17 → P 18 → 378 (∀n. n < 19 → P n). 379 #P #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 380 #H15 #H16 #H17 #H18 #H19 #n 381 cases n [1: // ] 382 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 383 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 384 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 385 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 386 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 387 #n' cases n' [1: // ] #n' cases n' [1: // ] #n' cases n' [1: // ] 388 #n' normalize in ⊢ (% → ?); 389 #absurd repeat (lapply (le_S_S_to_le … absurd) #absurd) 390 cases (lt_to_not_zero … absurd) 391 qed. 392 393 lemma get_index_v_set_index_miss: 394 ∀T: Type[0]. 395 ∀n, i, j: nat. 396 ∀v: Vector T n. 397 ∀b: T. 398 ∀i_proof: i < n. 399 ∀j_proof: j < n. 400 i ≠ j → 401 get_index_v T n (set_index T n v i b i_proof) j j_proof = 402 get_index_v T n v j j_proof. 403 #T #n #i #j #v lapply i lapply j elim v #i #j 404 [1: 405 #b #i_proof 406 cases (lt_to_not_zero … i_proof) 407 |2: 408 #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j 409 lapply i_proof lapply i_neq_j cases i' 410 [1: 411 -i_neq_j #i_neq_j -i_proof #i_proof 412 whd in match (set_index ??????); 413 lapply j_proof lapply i_neq_j cases j' 414 [1: 415 #relevant @⊥ cases relevant -relevant #absurd @absurd % 416 |2: 417 #j' #_ -j_proof #j_proof % 418 ] 419 |2: 420 #i' -i_neq_j #i_neq_j -i_proof #i_proof 421 lapply j_proof lapply i_neq_j cases j' 422 [1: 423 #_ #j_proof % 424 |2: 425 #j' #i_neq_j #j_proof 426 @inductive_hypothesis @nmk #relevant 427 cases i_neq_j #absurd @absurd >relevant % 428 ] 429 ] 430 ] 431 qed. 432 433 lemma get_index_v_special_function_registers_8051_not_acc_a: 434 ∀M: internal_pseudo_address_map. 435 ∀cm: pseudo_assembly_program. 436 ∀s: PreStatus pseudo_assembly_program cm. 437 ∀sigma: Word → Word. 438 ∀policy: Word → bool. 439 ∀n: nat. 440 ∀proof: n < 19. 441 n ≠ 17 → 442 (get_index_v Byte 19 443 (special_function_registers_8051 pseudo_assembly_program cm s) n 444 proof = 445 get_index_v Byte 19 446 (special_function_registers_8051 (BitVectorTrie Byte 16) 447 (code_memory_of_pseudo_assembly_program cm sigma policy) 448 (status_of_pseudo_status M cm s sigma policy)) n 449 proof). 450 #M #cm #s #sigma #policy #n #proof lapply proof 451 @(n_lt_19_elim_prop … proof) -proof #proof 452 [18: 453 #absurd @⊥ cases absurd -absurd #absurd @absurd % 454 ] 455 #_ cases s #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 456 whd in match status_of_pseudo_status; normalize nodelta 457 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 458 cases M #left #right cases right normalize nodelta try % 459 -right * #address 460 @pair_elim #high #low #high_low_refl normalize nodelta 461 whd in match sfr_8051_index; normalize nodelta 462 >get_index_v_set_index_miss try % 463 #absurd destruct(absurd) 464 qed. 1 include "ASM/StatusProofsSplit.ma". 465 2 466 3 include alias "arithmetics/nat.ma". … … 473 10 ∀i: instruction. 474 11 fetch_many code_memory final_pc start_pc [i] → 475 〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc. 12 〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory 13 start_pc. 476 14 #code_memory #final_pc #start_pc #i * #new_pc 477 15 #fetch_many_assm whd in fetch_many_assm; … … 479 17 qed. 480 18 481 (* XXX: this needs an extra invariant relating address and word that we look482 up!483 *)484 definition map_lower_internal_ram_address_using_pseudo_address_map:485 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝486 λM: internal_pseudo_address_map.487 λsigma: Word → Word.488 λaddress: Byte.489 λvalue: Byte.490 match assoc_list_lookup ?? address (eq_bv …) (\fst M) with491 [ None ⇒ value492 | Some upper_lower_word ⇒493 let 〈upper_lower, word〉 ≝ upper_lower_word in494 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in495 if eq_upper_lower upper_lower upper then496 high497 else498 low499 ].500 501 lemma get_8051_sfr_status_of_pseudo_status:502 ∀M.503 ∀cm, ps, sigma, policy.504 ∀sfr.505 (sfr = SFR_ACC_A → \snd M = data) →506 get_8051_sfr (BitVectorTrie Byte 16)507 (code_memory_of_pseudo_assembly_program cm sigma policy)508 (status_of_pseudo_status M cm ps sigma policy) sfr =509 get_8051_sfr pseudo_assembly_program cm ps sfr.510 #M #cm #ps #sigma #policy * cases M #fstM #sndM #relevant511 [18:512 >relevant %513 ]514 cases sndM try % * #address515 whd in match get_8051_sfr;516 whd in match status_of_pseudo_status; normalize nodelta517 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta518 @pair_elim #upper #lower #upper_lower_refl519 @get_index_v_set_index_miss @nmk #relevant520 normalize in relevant; destruct(relevant)521 qed.522 523 lemma bitvector_cases_hd_tl:524 ∀n: nat.525 ∀w: BitVector (S n).526 ∃hd: bool. ∃tl: BitVector n.527 w ≃ hd:::tl.528 #n #w cases (BitVector_Sn … w) #hd #relevant %{hd} @relevant529 qed.530 531 lemma external_ram_set_bit_addressable_sfr:532 ∀M: Type[0].533 ∀cm: M.534 ∀ps.535 ∀w.536 ∀result: Byte.537 external_ram M cm538 (set_bit_addressable_sfr M cm ps w result) =539 external_ram M cm ps.540 #M #cm #ps #w #result cases daemon (* XXX: prove this with Russell in Status.ma!541 whd in match set_bit_addressable_sfr; normalize nodelta542 cases (eqb ??) normalize nodelta [1: cases not_implemented ]543 cases (eqb ??) normalize nodelta [1: % ]544 cases (eqb ??) normalize nodelta [1: cases not_implemented ]545 cases (eqb ??) normalize nodelta [1: % ]546 cases (eqb ??) normalize nodelta [1: % ]547 cases (eqb ??) normalize nodelta [1: % ]548 cases (eqb ??) normalize nodelta [1: % ]549 cases (eqb ??) normalize nodelta [1: % ]550 cases (eqb ??) normalize nodelta [1: % ]551 cases (eqb ??) normalize nodelta [1: % ]552 cases (eqb ??) normalize nodelta [1: % ]553 cases (eqb ??) normalize nodelta [1: % ]554 cases (eqb ??) normalize nodelta [1: % ]555 cases (eqb ??) normalize nodelta [1: % ]556 cases (eqb ??) normalize nodelta [1: % ]557 cases (eqb ??) normalize nodelta [1: % ]558 cases (eqb ??) normalize nodelta [1: % ]559 cases (eqb ??) normalize nodelta [1: % ]560 cases (eqb ??) normalize nodelta [1: % ]561 cases (eqb ??) normalize nodelta [1: % ]562 cases (eqb ??) normalize nodelta [1: % ]563 cases (eqb ??) normalize nodelta [1: % ]564 cases (eqb ??) normalize nodelta [1: % ]565 cases (eqb ??) normalize nodelta [1: % ]566 cases (eqb ??) normalize nodelta [1: % ]567 cases (eqb ??) normalize nodelta [1: % ]568 cases not_implemented *)569 qed.570 571 lemma external_ram_set_arg_8:572 ∀M: Type[0].573 ∀cm: M.574 ∀ps.575 ∀addr1: [[direct; indirect; registr; acc_a; acc_b ]].576 ∀result.577 external_ram M cm (set_arg_8 M cm ps addr1 result) =578 external_ram M cm ps.579 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]580 #M #cm #ps #addr1 #result581 @(subaddressing_mode_elim … addr1) try #w try %582 whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)583 [1:584 cases (vsplit bool ???) #nu #nl normalize nodelta585 cases (vsplit bool ???) #ignore #three_bits normalize nodelta586 cases (get_index_v bool ????) normalize nodelta try %587 @external_ram_set_bit_addressable_sfr588 |2:589 cases (vsplit bool ???) #nu #nl normalize nodelta590 cases (vsplit bool ???) #ignore #three_bits normalize nodelta591 cases (get_index_v bool ????) normalize nodelta %592 ]593 qed.594 595 lemma special_function_registers_8051_set_clock:596 ∀M: Type[0].597 ∀cm: M.598 ∀ps.599 ∀t.600 special_function_registers_8051 M cm (set_clock M cm ps t) =601 special_function_registers_8051 M cm ps.602 //603 qed.604 605 lemma get_arg_8_pseudo_addressing_mode_ok:606 ∀M: internal_pseudo_address_map.607 ∀cm: pseudo_assembly_program.608 ∀ps: PreStatus pseudo_assembly_program cm.609 ∀sigma: Word → Word.610 ∀policy: Word → bool.611 ∀addr1: [[registr; direct]].612 addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →613 get_arg_8 (BitVectorTrie Byte 16)614 (code_memory_of_pseudo_assembly_program cm sigma policy)615 (status_of_pseudo_status M cm ps sigma policy) true addr1 =616 get_arg_8 pseudo_assembly_program cm ps true addr1.617 [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]618 #M #cm #ps #sigma #policy #addr1619 @(subaddressing_mode_elim … addr1) #arg whd in ⊢ (? → ???%);620 [1:621 whd in ⊢ (??%? → ??%?);622 whd in match bit_address_of_register; normalize nodelta623 @pair_elim #un #ln #un_ln_refl624 lapply (refl_to_jmrefl ??? un_ln_refl) -un_ln_refl #un_ln_refl625 @(pair_replace ?????????? un_ln_refl)626 [1:627 whd in match get_8051_sfr; normalize nodelta628 whd in match sfr_8051_index; normalize nodelta629 @eq_f <get_index_v_special_function_registers_8051_not_acc_a630 try % #absurd destruct(absurd)631 |2:632 #assembly_mode_ok_refl633 >low_internal_ram_of_pseudo_internal_ram_miss634 [1:635 %636 |2:637 cases (assoc_list_exists ?????) in assembly_mode_ok_refl; normalize nodelta638 #absurd try % @sym_eq assumption639 ]640 ]641 |2:642 #addressing_mode_ok_refl whd in ⊢ (??%?);643 @pair_elim #nu #nl #nu_nl_refl normalize nodelta644 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta645 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta646 [1:647 whd in ⊢ (??%%); normalize nodelta648 cases (eqb ??) normalize nodelta [1: % ]649 cases (eqb ??) normalize nodelta [1: % ]650 cases (eqb ??) normalize nodelta [1: % ]651 cases (eqb ??) normalize nodelta [1: % ]652 cases (eqb ??) normalize nodelta [1:653 @get_8051_sfr_status_of_pseudo_status654 #absurd destruct(absurd)655 ]656 cases (eqb ??) normalize nodelta [1:657 @get_8051_sfr_status_of_pseudo_status658 #absurd destruct(absurd)659 ]660 cases (eqb ??) normalize nodelta [1:661 @get_8051_sfr_status_of_pseudo_status662 #absurd destruct(absurd)663 ]664 cases (eqb ??) normalize nodelta [1:665 @get_8051_sfr_status_of_pseudo_status666 #absurd destruct(absurd)667 ]668 cases (eqb ??) normalize nodelta [1:669 @get_8051_sfr_status_of_pseudo_status670 #absurd destruct(absurd)671 ]672 cases (eqb ??) normalize nodelta [1: % ]673 cases (eqb ??) normalize nodelta [1: % ]674 cases (eqb ??) normalize nodelta [1: % ]675 cases (eqb ??) normalize nodelta [1: % ]676 cases (eqb ??) normalize nodelta [1: % ]677 cases (eqb ??) normalize nodelta [1:678 @get_8051_sfr_status_of_pseudo_status679 #absurd destruct(absurd)680 ]681 cases (eqb ??) normalize nodelta [1:682 @get_8051_sfr_status_of_pseudo_status683 #absurd destruct(absurd)684 ]685 cases (eqb ??) normalize nodelta [1:686 @get_8051_sfr_status_of_pseudo_status687 #absurd destruct(absurd)688 ]689 cases (eqb ??) normalize nodelta [1:690 @get_8051_sfr_status_of_pseudo_status691 #absurd destruct(absurd)692 ]693 cases (eqb ??) normalize nodelta [1:694 @get_8051_sfr_status_of_pseudo_status695 #absurd destruct(absurd)696 ]697 cases (eqb ??) normalize nodelta [1:698 @get_8051_sfr_status_of_pseudo_status699 #absurd destruct(absurd)700 ]701 cases (eqb ??) normalize nodelta [1:702 @get_8051_sfr_status_of_pseudo_status703 #absurd destruct(absurd)704 ]705 cases (eqb ??) normalize nodelta [1:706 @get_8051_sfr_status_of_pseudo_status707 #absurd destruct(absurd)708 ]709 cases (eqb ??) normalize nodelta [1:710 @get_8051_sfr_status_of_pseudo_status711 #absurd destruct(absurd)712 ]713 cases (eqb ??) normalize nodelta [1:714 @get_8051_sfr_status_of_pseudo_status715 #absurd destruct(absurd)716 ]717 inversion (eqb ??) #eqb_refl normalize nodelta [1:718 @get_8051_sfr_status_of_pseudo_status lapply addressing_mode_ok_refl719 whd in ⊢ (??%? → ?); <(eqb_true_to_eq … eqb_refl)720 >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta721 #assoc_list_assm cases (conjunction_true … assoc_list_assm) #_722 #relevant #_ cases (eq_accumulator_address_map_entry_true_to_eq … relevant) %723 ]724 cases (eqb ??) normalize nodelta [1:725 @get_8051_sfr_status_of_pseudo_status726 #absurd destruct(absurd)727 ] %728 |2:729 lapply addressing_mode_ok_refl whd in ⊢ (??%? → ?); #relevant730 whd in match status_of_pseudo_status; normalize nodelta731 >low_internal_ram_of_pseudo_internal_ram_miss try %732 cut(arg = false:::(three_bits@@nl))733 [1:734 <get_index_v_refl735 cut(nu=get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3)):::three_bits)736 [1:737 cut(ignore = [[get_index_v bool 4 nu 0 ?]])738 [1:739 @le_S_S @le_O_n740 |2:741 cut(ignore = \fst (vsplit bool 1 3 nu))742 [1:743 >ignore_three_bits_refl %744 |2:745 #ignore_refl >ignore_refl746 cases (bitvector_cases_hd_tl … nu) #hd * #tl #nu_refl747 >nu_refl %748 ]749 |3:750 #ignore_refl >ignore_refl in ignore_three_bits_refl;751 #relevant lapply (vsplit_ok ?????? (sym_eq … relevant))752 #nu_refl <nu_refl %753 ]754 |2:755 #nu_refl change with (? = (?:::three_bits)@@?) <nu_refl756 @sym_eq @vsplit_ok >nu_nl_refl %757 ]758 |2:759 #arg_refl <arg_refl cases (assoc_list_exists ?????) in relevant;760 normalize nodelta761 [1:762 cases (eq_bv ???) normalize #absurd destruct(absurd)763 |2:764 #_ %765 ]766 ]767 ]768 ]769 qed.770 771 lemma special_function_registers_8051_set_program_counter:772 ∀M: Type[0].773 ∀cm: M.774 ∀ps.775 ∀pc: Word.776 special_function_registers_8051 M cm (set_program_counter M cm ps pc) =777 special_function_registers_8051 M cm ps.778 //779 qed.780 781 lemma special_function_registers_8052_set_program_counter:782 ∀M: Type[0].783 ∀cm: M.784 ∀ps.785 ∀pc: Word.786 special_function_registers_8052 M cm (set_program_counter M cm ps pc) =787 special_function_registers_8052 M cm ps.788 //789 qed.790 791 lemma set_index_set_index_commutation:792 ∀A: Type[0].793 ∀n: nat.794 ∀v: Vector A n.795 ∀m, o: nat.796 ∀m_lt_proof: m < n.797 ∀o_lt_proof: o < n.798 ∀e, f: A.799 m ≠ o →800 set_index A n (set_index A n v o f o_lt_proof) m e m_lt_proof =801 set_index A n (set_index A n v m e m_lt_proof) o f o_lt_proof.802 #A #n #v elim v803 [1:804 #m #o #m_lt_proof805 normalize in m_lt_proof; cases (lt_to_not_zero … m_lt_proof)806 |2:807 #n' #hd #tl #inductive_hypothesis808 #m #o809 cases m cases o810 [1:811 #m_lt_proof #o_lt_proof #e #f #absurd @⊥ cases absurd #relevant812 @relevant %813 |2,3:814 #o' normalize //815 |4:816 #m' #o' #m_lt_proof #o_lt_proof #e #f #o_neq_m_assm817 normalize @eq_f @inductive_hypothesis @nmk #relevant818 >relevant in o_neq_m_assm; #relevant @(absurd ?? relevant) %819 ]820 ]821 qed.822 823 lemma special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051:824 ∀M: internal_pseudo_address_map.825 ∀cm: pseudo_assembly_program.826 ∀ps.827 ∀sigma: Word → Word.828 ∀policy: Word → bool.829 ∀sfr.830 ∀result: Byte.831 eqb (sfr_8051_index sfr) (sfr_8051_index SFR_ACC_A) = false →832 special_function_registers_8051 (BitVectorTrie Byte 16)833 (code_memory_of_pseudo_assembly_program cm sigma policy)834 (set_8051_sfr (BitVectorTrie Byte 16)835 (code_memory_of_pseudo_assembly_program cm sigma policy)836 (status_of_pseudo_status M cm ps sigma policy) sfr result) =837 sfr_8051_of_pseudo_sfr_8051 M838 (special_function_registers_8051 pseudo_assembly_program cm839 (set_8051_sfr pseudo_assembly_program cm ps sfr result)) sigma.840 #M #cm #ps #sigma #policy #sfr #result #sfr_neq_assm841 whd in match (set_8051_sfr ?????);842 cases M #callM * try % #upper_lower #address843 whd in match (special_function_registers_8051 ???);844 whd in match (sfr_8051_of_pseudo_sfr_8051 ???);845 @pair_elim #high #low #high_low_refl normalize nodelta846 cases (eq_upper_lower ??) normalize nodelta847 whd in match (set_8051_sfr ?????);848 @set_index_set_index_commutation @nmk #relevant849 @(absurd ? relevant (eqb_false_to_not_eq ?? sfr_neq_assm))850 qed.851 852 lemma special_function_registers_8051_set_arg_8:853 ∀M: internal_pseudo_address_map.854 ∀cm: pseudo_assembly_program.855 ∀ps.856 ∀sigma: Word → Word.857 ∀policy: Word → bool.858 ∀addr1: [[ registr; direct ]].859 ∀result.860 addressing_mode_ok pseudo_assembly_program M cm ps addr1 = true →861 special_function_registers_8051 (BitVectorTrie Byte 16)862 (code_memory_of_pseudo_assembly_program cm sigma policy)863 (set_arg_8 (BitVectorTrie Byte 16)864 (code_memory_of_pseudo_assembly_program cm sigma policy)865 (status_of_pseudo_status M cm ps sigma policy) addr1 result) =866 sfr_8051_of_pseudo_sfr_8051 M867 (special_function_registers_8051 pseudo_assembly_program cm868 (set_arg_8 pseudo_assembly_program cm ps addr1 result)) sigma.869 cases daemon870 (*871 [2,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]872 #M #cm #ps #sigma #policy #addr1 #result873 @(subaddressing_mode_elim … addr1) #w #addressing_mode_ok_refl try %874 whd in match (set_arg_8 ?????); whd in ⊢ (??(???(???%))?);875 whd in match (set_arg_8 ?????) in ⊢ (???%); whd in ⊢ (???(??(???(???%))?));876 cases (vsplit bool ???) #nu #nl normalize nodelta877 cases (vsplit bool ???) #ignore #three_bits normalize nodelta878 cases (get_index_v bool ????) normalize nodelta try %879 whd in match (set_bit_addressable_sfr ?????); whd in match (set_bit_addressable_sfr ?????) in ⊢ (???%);880 cases (eqb ??) normalize nodelta [1: cases not_implemented ]881 cases (eqb ??) normalize nodelta [1: % ]882 cases (eqb ??) normalize nodelta [1: cases not_implemented ]883 cases (eqb ??) normalize nodelta [1: % ]884 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]885 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]886 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]887 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]888 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]889 cases (eqb ??) normalize nodelta [1: % ]890 cases (eqb ??) normalize nodelta [1: % ]891 cases (eqb ??) normalize nodelta [1: % ]892 cases (eqb ??) normalize nodelta [1: % ]893 cases (eqb ??) normalize nodelta [1: % ]894 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]895 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]896 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]897 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]898 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]899 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]900 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]901 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]902 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]903 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]904 inversion (eqb ??) #eqb_refl normalize nodelta [1:905 whd in addressing_mode_ok_refl:(??%?); <(eqb_true_to_eq … eqb_refl) in addressing_mode_ok_refl;906 >bitvector_of_nat_inverse_nat_of_bitvector >eq_bv_refl normalize nodelta907 #relevant cases (conjunction_true … relevant) #_ #eq_acc_assm908 whd in match (status_of_pseudo_status ?????);909 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta910 >(eq_accumulator_address_map_entry_true_to_eq … eq_acc_assm) normalize nodelta %911 ]912 cases (eqb ??) normalize nodelta [1: @special_function_registers_8051_sfr_8051_of_pseudo_sfr_8051 % ]913 cases not_implemented *)914 qed.915 916 19 include alias "ASM/Vector.ma". 20 include "ASM/Test.ma". 917 21 918 22 lemma main_lemma_preinstruction: -
src/ASM/Status.ma
r2160 r2172 546 546 set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7). 547 547 548 definition get_bit_addressable_sfr ≝ 549 λM: Type[0]. 550 λcode_memory:M. 551 λs: PreStatus M code_memory. 552 λn: nat. 553 λb: BitVector n. 548 549 definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝ 550 λb: Byte. 551 let address ≝ nat_of_bitvector … b in 552 if (eqb address 128) then None ? 553 else if (eqb address 144) then Some … (inl … SFR_P1) 554 else if (eqb address 160) then None ? 555 else if (eqb address 176) then Some … (inl … SFR_P3) 556 else if (eqb address 153) then Some … (inl … SFR_SBUF) 557 else if (eqb address 138) then Some … (inl … SFR_TL0) 558 else if (eqb address 139) then Some … (inl … SFR_TL1) 559 else if (eqb address 140) then Some … (inl … SFR_TH0) 560 else if (eqb address 141) then Some … (inl … SFR_TH1) 561 else if (eqb address 200) then Some … (inr … SFR_T2CON) 562 else if (eqb address 202) then Some … (inr … SFR_RCAP2L) 563 else if (eqb address 203) then Some … (inr … SFR_RCAP2H) 564 else if (eqb address 204) then Some … (inr … SFR_TL2) 565 else if (eqb address 205) then Some … (inr … SFR_TH2) 566 else if (eqb address 135) then Some … (inl … SFR_PCON) 567 else if (eqb address 136) then Some … (inl … SFR_TCON) 568 else if (eqb address 137) then Some … (inl … SFR_TMOD) 569 else if (eqb address 152) then Some … (inl … SFR_SCON) 570 else if (eqb address 168) then Some … (inl … SFR_IE) 571 else if (eqb address 184) then Some … (inl … SFR_IP) 572 else if (eqb address 129) then Some … (inl … SFR_SP) 573 else if (eqb address 130) then Some … (inl … SFR_DPL) 574 else if (eqb address 131) then Some … (inl … SFR_DPH) 575 else if (eqb address 208) then Some … (inl … SFR_PSW) 576 else if (eqb address 224) then Some … (inl … SFR_ACC_A) 577 else if (eqb address 240) then Some … (inl … SFR_ACC_B) 578 else None ?. 579 580 definition get_bit_addressable_sfr: 581 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝ 582 λM: Type[0]. 583 λcode_memory:M. 584 λs: PreStatus M code_memory. 585 λb: Byte. 554 586 λl: bool. 555 let address ≝ nat_of_bitvector … b in 556 if (eqb address 128) then 557 ? 558 else if (eqb address 144) then 587 match sfr_of_Byte b with 588 [ None ⇒ match not_implemented in False with [ ] 589 | Some sfr8051_8052 ⇒ 590 match sfr8051_8052 with 591 [ inl sfr ⇒ 592 match sfr with 593 [ SFR_P1 ⇒ 559 594 if l then 560 (p1_latch ?? s)595 p1_latch … s 561 596 else 562 (get_8051_sfr ?? s SFR_P1) 563 else if (eqb address 160) then 564 ? 565 else if (eqb address 176) then 597 get_8051_sfr … s SFR_P1 598 | SFR_P3 ⇒ 566 599 if l then 567 (p3_latch ?? s)600 p3_latch … s 568 601 else 569 (get_8051_sfr ?? s SFR_P3) 570 else if (eqb address 153) then 571 get_8051_sfr ?? s SFR_SBUF 572 else if (eqb address 138) then 573 get_8051_sfr ?? s SFR_TL0 574 else if (eqb address 139) then 575 get_8051_sfr ?? s SFR_TL1 576 else if (eqb address 140) then 577 get_8051_sfr ?? s SFR_TH0 578 else if (eqb address 141) then 579 get_8051_sfr ?? s SFR_TH1 580 else if (eqb address 200) then 581 get_8052_sfr ?? s SFR_T2CON 582 else if (eqb address 202) then 583 get_8052_sfr ?? s SFR_RCAP2L 584 else if (eqb address 203) then 585 get_8052_sfr ?? s SFR_RCAP2H 586 else if (eqb address 204) then 587 get_8052_sfr ?? s SFR_TL2 588 else if (eqb address 205) then 589 get_8052_sfr ?? s SFR_TH2 590 else if (eqb address 135) then 591 get_8051_sfr ?? s SFR_PCON 592 else if (eqb address 136) then 593 get_8051_sfr ?? s SFR_TCON 594 else if (eqb address 137) then 595 get_8051_sfr ?? s SFR_TMOD 596 else if (eqb address 152) then 597 get_8051_sfr ?? s SFR_SCON 598 else if (eqb address 168) then 599 get_8051_sfr ?? s SFR_IE 600 else if (eqb address 184) then 601 get_8051_sfr ?? s SFR_IP 602 else if (eqb address 129) then 603 get_8051_sfr ?? s SFR_SP 604 else if (eqb address 130) then 605 get_8051_sfr ?? s SFR_DPL 606 else if (eqb address 131) then 607 get_8051_sfr ?? s SFR_DPH 608 else if (eqb address 208) then 609 get_8051_sfr ?? s SFR_PSW 610 else if (eqb address 224) then 611 get_8051_sfr ?? s SFR_ACC_A 612 else if (eqb address 240) then 613 get_8051_sfr ?? s SFR_ACC_B 614 else 615 ?. 616 cases not_implemented 617 qed. 618 619 definition set_bit_addressable_sfr': 620 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → 621 Σs':PreStatus M code_memory. 622 clock … code_memory s = clock … code_memory s' ∧ 623 program_counter … code_memory s = program_counter … code_memory s' ≝ 602 get_8051_sfr … s SFR_P3 603 | _ ⇒ get_8051_sfr … s sfr 604 ] 605 | inr sfr ⇒ get_8052_sfr M code_memory s sfr 606 ] 607 ]. 608 609 definition set_bit_addressable_sfr: 610 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → PreStatus M code_memory ≝ 624 611 λM: Type[0]. 625 612 λcode_memory:M. … … 627 614 λb: Byte. 628 615 λv: Byte. 629 let address ≝ nat_of_bitvector … b in 630 if (eqb address 128) then 631 match not_implemented in False with [ ] 632 else if (eqb address 144) then 633 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 634 let status_2 ≝ set_p1_latch ?? s v in 635 status_2 636 else if (eqb address 160) then 637 match not_implemented in False with [ ] 638 else if (eqb address 176) then 639 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 640 let status_2 ≝ set_p3_latch ?? s v in 641 status_2 642 else if (eqb address 153) then 643 set_8051_sfr ?? s SFR_SBUF v 644 else if (eqb address 138) then 645 set_8051_sfr ?? s SFR_TL0 v 646 else if (eqb address 139) then 647 set_8051_sfr ?? s SFR_TL1 v 648 else if (eqb address 140) then 649 set_8051_sfr ?? s SFR_TH0 v 650 else if (eqb address 141) then 651 set_8051_sfr ?? s SFR_TH1 v 652 else if (eqb address 200) then 653 set_8052_sfr ?? s SFR_T2CON v 654 else if (eqb address 202) then 655 set_8052_sfr ?? s SFR_RCAP2L v 656 else if (eqb address 203) then 657 set_8052_sfr ?? s SFR_RCAP2H v 658 else if (eqb address 204) then 659 set_8052_sfr ?? s SFR_TL2 v 660 else if (eqb address 205) then 661 set_8052_sfr ?? s SFR_TH2 v 662 else if (eqb address 135) then 663 set_8051_sfr ?? s SFR_PCON v 664 else if (eqb address 136) then 665 set_8051_sfr ?? s SFR_TCON v 666 else if (eqb address 137) then 667 set_8051_sfr ?? s SFR_TMOD v 668 else if (eqb address 152) then 669 set_8051_sfr ?? s SFR_SCON v 670 else if (eqb address 168) then 671 set_8051_sfr ?? s SFR_IE v 672 else if (eqb address 184) then 673 set_8051_sfr ?? s SFR_IP v 674 else if (eqb address 129) then 675 set_8051_sfr ?? s SFR_SP v 676 else if (eqb address 130) then 677 set_8051_sfr ?? s SFR_DPL v 678 else if (eqb address 131) then 679 set_8051_sfr ?? s SFR_DPH v 680 else if (eqb address 208) then 681 set_8051_sfr ?? s SFR_PSW v 682 else if (eqb address 224) then 683 set_8051_sfr ?? s SFR_ACC_A v 684 else if (eqb address 240) then 685 set_8051_sfr ?? s SFR_ACC_B v 686 else 687 match not_implemented in False with [ ]. 688 /2 by refl, pair_destruct/ 689 qed. 690 691 definition set_bit_addressable_sfr: 692 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → 693 PreStatus M code_memory ≝ set_bit_addressable_sfr'. 616 match sfr_of_Byte b with 617 [ None ⇒ match not_implemented in False with [ ] 618 | Some sfr8051_8052 ⇒ 619 match sfr8051_8052 with 620 [ inl sfr ⇒ 621 match sfr with 622 [ SFR_P1 ⇒ 623 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 624 set_p1_latch ?? s v 625 | SFR_P3 ⇒ 626 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 627 set_p3_latch ?? s v 628 | _ ⇒ set_8051_sfr ?? s sfr v ] 629 | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]. 694 630 695 631 lemma clock_set_bit_addressable_sfr: … … 697 633 clock … code_memory s = clock … code_memory (set_bit_addressable_sfr M code_memory s b v). 698 634 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 699 cases (set_bit_addressable_sfr' ?????) #s' * // 635 cases (sfr_of_Byte ?) 636 [1: 637 normalize nodelta cases not_implemented 638 |2: 639 * * normalize nodelta % 640 ] 700 641 qed. 701 642 … … 704 645 program_counter … code_memory s = program_counter … code_memory (set_bit_addressable_sfr M code_memory s b v). 705 646 #M #code_memory #s #b #v whd in match (set_bit_addressable_sfr ?????); 706 cases (set_bit_addressable_sfr' ?????) #s' * // 647 cases (sfr_of_Byte ?) 648 [1: 649 normalize nodelta cases not_implemented 650 |2: 651 * * % 652 ] 707 653 qed. 708 654 … … 863 809 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 864 810 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 865 let 〈 carry, address〉 ≝ half_add 16 dptr padded_acc in811 let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in 866 812 lookup ? 16 address (external_ram ?? s) (zero 8) 867 813 | ACC_PC ⇒ … … 872 818 | DIRECT d ⇒ 873 819 λdirect: True. 874 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 d in 875 let bit_one ≝ get_index_v ? ? nu 0 ? in 876 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in 877 match bit_one with 878 [ false ⇒ 879 let address ≝ three_bits @@ nl in 880 lookup ? 7 address (low_internal_ram ?? s) (zero 8) 881 | true ⇒ get_bit_addressable_sfr ?? s 8 d l 882 ] 820 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in 821 match head' … hd with 822 [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l 823 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 824 ] 883 825 | INDIRECT i ⇒ 884 826 λindirect: True. 885 let 〈 nu, nl 〉 ≝ vsplit ? 4 4 (get_register ?? s [[ false; false; i]]) in 886 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 887 let bit_1 ≝ get_index_v ?? bit_one_v O ? in 888 match bit_1 with 889 [ false ⇒ 890 lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8) 891 | true ⇒ 892 lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8) 827 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in 828 match head' … hd with 829 [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …) 830 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …) 893 831 ] 894 832 | _ ⇒ λother. 895 833 match other in False with [ ] 896 834 ] (subaddressing_modein … a). 897 [1,2: 898 normalize 899 repeat (@ le_S_S) 900 @ le_O_n 901 ] 902 qed. 903 904 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; 835 836 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; 905 837 acc_a ; acc_b ; ext_indirect ; 906 ext_indirect_dptr ]]. Byte → Σs':PreStatus M code_memory. 907 clock … code_memory s = clock … code_memory s' ∧ 908 (¬(is_a … direct addr) → p1_latch … code_memory s = p1_latch … code_memory s') ∧ 909 (¬(is_a … direct addr) → p3_latch … code_memory s = p3_latch … code_memory s') ∧ 910 program_counter … code_memory s = program_counter … code_memory s' ∧ 911 (¬(is_a … direct addr) → special_function_registers_8052 … code_memory s = special_function_registers_8052 … code_memory s') ≝ 838 ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝ 912 839 λm, cm, s, a, v. 913 840 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 914 841 acc_a ; acc_b ; ext_indirect ; 915 842 ext_indirect_dptr ]] x) → 916 Σs':PreStatus m cm. ? 917 (*CSC: bug here if one specified the two clock above*) 843 PreStatus m cm 918 844 with 919 845 [ DIRECT d ⇒ 920 846 λdirect: True. 921 let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in 922 let bit_one ≝ get_index_v ? ? nu 0 ? in 923 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in 924 match bit_one with 925 [ true ⇒ set_bit_addressable_sfr ?? s d v 847 let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in 848 match head' … bit_one with 849 [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v 926 850 | false ⇒ 927 let memory ≝ insert ? 7 (three_bits @@ nl)v (low_internal_ram ?? s) in851 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in 928 852 set_low_internal_ram ?? s memory 929 853 ] … … 931 855 λindirect: True. 932 856 let register ≝ get_register ?? s [[ false; false; i ]] in 933 let 〈nu, nl〉 ≝ vsplit ? 4 4 register in 934 let bit_1 ≝ get_index_v … nu 0 ? in 935 let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in 936 match bit_1 with 857 let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in 858 match head' … bit_one with 937 859 [ false ⇒ 938 let memory ≝ insert … (three_bits @@ nl)v (low_internal_ram ?? s) in860 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in 939 861 set_low_internal_ram ?? s memory 940 862 | true ⇒ 941 let memory ≝ insert … (three_bits @@ nl)v (high_internal_ram ?? s) in863 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in 942 864 set_high_internal_ram ?? s memory 943 865 ] … … 960 882 match other in False with [ ] 961 883 ] (subaddressing_modein … a). 962 /6 by conj, False_ind/963 qed.964 965 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝966 set_arg_8'.967 884 968 885 lemma clock_set_arg_8: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). 969 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 970 cases (set_arg_8' ?????) #s' * * * * // 886 cases daemon 971 887 qed. 972 888 973 889 lemma program_counter_set_arg_8: ∀M,cm,s,x,v. program_counter M cm s = program_counter … (set_arg_8 M cm s x v). 974 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 975 cases (set_arg_8' ?????) #s' * * * * // 890 cases daemon 976 891 qed. 977 892 … … 979 894 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 980 895 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 981 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 982 * * * * #_ #relevant #_ #_ #_ @relevant @I 896 cases daemon 983 897 qed. 984 898 … … 986 900 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 987 901 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 988 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 989 * * * * #_ #_ #relevant #_ #_ @relevant @I 902 cases daemon 990 903 qed. 991 904 … … 993 906 [2: /2 by subaddressing_modein, orb_Prop_r/ ] 994 907 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta 995 cases (set_arg_8' ?????) #s' @(subaddressing_mode_elim … x) [1,2,5: #w ] 996 * * * * #_ #_ #_ #_ #relevant @relevant @I 908 cases daemon 997 909 qed. 998 910 … … 1056 968 [ BIT_ADDR b ⇒ 1057 969 λbit_addr: True. 1058 let 〈 nu, nl 〉 ≝ vsplit … 4 4 b in 1059 let bit_1 ≝ get_index_v ? ? nu 0 ? in 1060 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 1061 match bit_1 with 1062 [ true ⇒ 1063 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1064 let d ≝ address ÷ 8 in 1065 let m ≝ address mod 8 in 1066 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1067 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in 1068 get_index_v … sfr m ? 1069 | false ⇒ 1070 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1071 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1072 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1073 get_index_v … t (modulus address 8) ? 1074 ] 970 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in 971 match head' … bit_1 with 972 [ true ⇒ 973 let address ≝ nat_of_bitvector … seven_bits in 974 let d ≝ address ÷ 8 in 975 let m ≝ address mod 8 in 976 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 977 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 978 get_index_v … sfr m ? 979 | false ⇒ 980 let address ≝ nat_of_bitvector … seven_bits in 981 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 982 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 983 get_index_v … t (modulus address 8) ? 984 ] 1075 985 | N_BIT_ADDR n ⇒ 1076 986 λn_bit_addr: True. 1077 let 〈 nu, nl 〉 ≝ vsplit … 4 4 n in 1078 let bit_1 ≝ get_index_v ? ? nu 0 ? in 1079 let 〈 bit_one_v, three_bits 〉 ≝ vsplit ? 1 3 nu in 1080 match bit_1 with 1081 [ true ⇒ 1082 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1083 let d ≝ address ÷ 8 in 1084 let m ≝ address mod 8 in 1085 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1086 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in 1087 ¬(get_index_v … sfr m ?) 1088 | false ⇒ 1089 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1090 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1091 let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1092 ¬(get_index_v … trans (modulus address 8) ?) 1093 ] 987 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in 988 match head' … bit_1 with 989 [ true ⇒ 990 let address ≝ nat_of_bitvector … seven_bits in 991 let d ≝ address ÷ 8 in 992 let m ≝ address mod 8 in 993 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 994 let sfr ≝ get_bit_addressable_sfr ?? s trans l in 995 ¬(get_index_v … sfr m ?) 996 | false ⇒ 997 let address ≝ nat_of_bitvector … seven_bits in 998 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 999 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1000 ¬(get_index_v … t (modulus address 8) ?) 1001 ] 1094 1002 | CARRY ⇒ λcarry: True. get_cy_flag ?? s 1095 1003 | _ ⇒ λother. 1096 1004 match other in False with [ ] 1097 1005 ] (subaddressing_modein … a). 1098 [3,6: 1099 normalize 1100 repeat (@ le_S_S) 1101 @ le_O_n 1102 |1,2,4,5: 1103 @modulus_less_than 1104 ] 1006 @modulus_less_than 1105 1007 qed. 1106 1008 1107 definition set_arg_1 ': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s'≝1009 definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ 1108 1010 λm: Type[0]. 1109 1011 λcm. … … 1111 1013 λa: [[bit_addr; carry]]. 1112 1014 λv: Bit. 1113 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s'with1015 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → ? with 1114 1016 [ BIT_ADDR b ⇒ λbit_addr: True. 1115 let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1116 let bit_1 ≝ get_index_v ?? nu 0 ? in 1117 let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in 1118 match bit_1 return λ_. ? with 1119 [ true ⇒ 1120 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1121 let d ≝ address ÷ 8 in 1122 let m ≝ address mod 8 in 1123 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1124 let sfr ≝ get_bit_addressable_sfr ?? s ? t true in 1125 let new_sfr ≝ set_index … sfr m v ? in 1126 set_bit_addressable_sfr ?? s new_sfr t 1127 | false ⇒ 1128 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1129 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1130 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1131 let n_bit ≝ set_index … t (modulus address 8) v ? in 1132 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1133 set_low_internal_ram ?? s memory 1134 ] 1017 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1018 match head' … bit_1 with 1019 [ true ⇒ 1020 let address ≝ nat_of_bitvector … seven_bits in 1021 let d ≝ address ÷ 8 in 1022 let m ≝ address mod 8 in 1023 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1024 let sfr ≝ get_bit_addressable_sfr … s t true in 1025 let new_sfr ≝ set_index … sfr m v ? in 1026 set_bit_addressable_sfr … s new_sfr t 1027 | false ⇒ 1028 let address ≝ nat_of_bitvector … seven_bits in 1029 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1030 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1031 let n_bit ≝ set_index … t (modulus address 8) v ? in 1032 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1033 set_low_internal_ram … s memory 1034 ] 1135 1035 | CARRY ⇒ 1136 1036 λcarry: True. 1137 let 〈nu, nl〉 ≝ vsplit ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1138 let bit_1 ≝ get_index_v… nu 1 ? in 1139 let bit_2 ≝ get_index_v… nu 2 ? in 1140 let bit_3 ≝ get_index_v… nu 3 ? in 1141 let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in 1037 let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in 1038 let new_psw ≝ v:::seven_bits in 1142 1039 set_8051_sfr ?? s SFR_PSW new_psw 1143 1040 | _ ⇒ … … 1146 1043 [ ] 1147 1044 ] (subaddressing_modein … a). 1148 try (repeat @le_S_S @le_O_n) 1149 /by/ 1150 qed. 1151 1152 definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'. 1045 @modulus_less_than 1046 qed. 1153 1047 1154 1048 lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v). 1155 #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi21049 cases daemon 1156 1050 qed. 1157 1051 -
src/ASM/StatusProofs.ma
r2124 r2172 200 200 #x try (#y #H) try #H whd in H; try cases H try % 201 201 whd in match set_arg_8; normalize nodelta 202 whd in match set_arg_8'; normalize nodelta 203 cases (vsplit bool 4 4 ?) #nu' #nl' normalize nodelta 204 cases (vsplit bool 1 3 nu') #bit1' #ignore' normalize nodelta 205 cases (get_index_v bool 4 nu' 0 ?) normalize nodelta 206 try % cases daemon (*@(set_bit_addressable_sfr_set_program_counter)*) 202 cases (vsplit bool ???) #bit_one #seven_bits normalize nodelta 203 cases (head' bool ??) normalize nodelta 204 try % cases daemon (* XXX: need @(set_bit_addressable_sfr_set_program_counter) *) 207 205 qed. 208 206 … … 349 347 #m #cm #s #addr #byte 350 348 whd in match set_arg_8; normalize nodelta 349 cases daemon (* 351 350 whd in match set_arg_8'; normalize nodelta 352 351 cases addr #subaddressing_modein_proof … … 357 356 cases (vsplit bool 4 4 ?) #nu #nl normalize nodelta 358 357 cases (vsplit bool 1 3 ?) #ignore #three_bits normalize nodelta 359 cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % 358 cases (get_index_v bool 4 nu ? ?) normalize nodelta try /demod/ try % *) 360 359 qed. 361 360 … … 366 365 #m #cm #s #addr #v 367 366 whd in match set_arg_1; normalize nodelta 367 cases daemon (* 368 368 whd in match set_arg_1'; normalize nodelta 369 369 cases addr #subaddressing_modein_proof … … 376 376 cases (get_index_v bool 4 nu ??) normalize nodelta 377 377 (* XXX: try /demod/ try % *) 378 cases daemon 378 cases daemon *) 379 379 qed. 380 380 -
src/ASM/StatusProofsSplit.ma
r2170 r2172 113 113 ∀b: Bit. 114 114 program_counter M cm (set_arg_1 M cm s addr b) = program_counter M cm s. 115 #M #cm #s whd in match set_arg_1; whd in match set_arg_1'; normalize nodelta115 #M #cm #s whd in match set_arg_1; cases daemon (* whd in match set_arg_1'; normalize nodelta 116 116 #addr #b 117 117 @(subaddressing_mode_elim … addr) … … 127 127 |2: 128 128 cases (vsplit ????) // 129 ] 129 ] *) 130 130 qed. 131 131 … … 551 551 #M #cm #ps #addr1 #result 552 552 @(subaddressing_mode_elim … addr1) try #w try % 553 whd in ⊢ (??(???%)?); whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *)553 whd in ⊢ (??(???%)?); cases daemon (*whd in ⊢ (??(???(???%))?); (* XXX: to be understood, slow match *) 554 554 [1: 555 555 cases (vsplit bool ???) #nu #nl normalize nodelta … … 561 561 cases (vsplit bool ???) #ignore #three_bits normalize nodelta 562 562 cases (get_index_v bool ????) normalize nodelta % 563 ] 563 ] *) 564 564 qed. 565 565 … … 612 612 |2: 613 613 #addressing_mode_ok_refl whd in ⊢ (??%?); 614 @pair_elim #nu #nl #nu_nl_refl normalize nodelta 614 @pair_elim #nu #nl #nu_nl_refl normalize nodelta cases daemon (* 615 615 @pair_elim #ignore #three_bits #ignore_three_bits_refl normalize nodelta 616 616 inversion (get_index_v bool ????) #get_index_v_refl normalize nodelta … … 737 737 ] 738 738 ] 739 ] 739 ] *) 740 740 qed. 741 741 -
src/ASM/Test.ma
r2171 r2172 1 (**************************************************************************)2 (* ___ *)3 (* ||M|| *)4 (* ||A|| A project by Andrea Asperti *)5 (* ||T|| *)6 (* ||I|| Developers: *)7 (* ||T|| The HELM team. *)8 (* ||A|| http://helm.cs.unibo.it *)9 (* \ / *)10 (* \ / This file is distributed under the terms of the *)11 (* v GNU General Public License Version 2 *)12 (* *)13 (**************************************************************************)14 15 1 include "ASM/Assembly.ma". 16 2 include "ASM/Interpret.ma". … … 316 302 // 317 303 qed. 318 319 definition sfr_of_Byte: Byte → option (SFR8051 + SFR8052) ≝ 320 λb: Byte. 321 let address ≝ nat_of_bitvector … b in 322 if (eqb address 128) then None ? 323 else if (eqb address 144) then Some … (inl … SFR_P1) 324 else if (eqb address 160) then None ? 325 else if (eqb address 176) then Some … (inl … SFR_P3) 326 else if (eqb address 153) then Some … (inl … SFR_SBUF) 327 else if (eqb address 138) then Some … (inl … SFR_TL0) 328 else if (eqb address 139) then Some … (inl … SFR_TL1) 329 else if (eqb address 140) then Some … (inl … SFR_TH0) 330 else if (eqb address 141) then Some … (inl … SFR_TH1) 331 else if (eqb address 200) then Some … (inr … SFR_T2CON) 332 else if (eqb address 202) then Some … (inr … SFR_RCAP2L) 333 else if (eqb address 203) then Some … (inr … SFR_RCAP2H) 334 else if (eqb address 204) then Some … (inr … SFR_TL2) 335 else if (eqb address 205) then Some … (inr … SFR_TH2) 336 else if (eqb address 135) then Some … (inl … SFR_PCON) 337 else if (eqb address 136) then Some … (inl … SFR_TCON) 338 else if (eqb address 137) then Some … (inl … SFR_TMOD) 339 else if (eqb address 152) then Some … (inl … SFR_SCON) 340 else if (eqb address 168) then Some … (inl … SFR_IE) 341 else if (eqb address 184) then Some … (inl … SFR_IP) 342 else if (eqb address 129) then Some … (inl … SFR_SP) 343 else if (eqb address 130) then Some … (inl … SFR_DPL) 344 else if (eqb address 131) then Some … (inl … SFR_DPH) 345 else if (eqb address 208) then Some … (inl … SFR_PSW) 346 else if (eqb address 224) then Some … (inl … SFR_ACC_A) 347 else if (eqb address 240) then Some … (inl … SFR_ACC_B) 348 else None ?. 349 350 definition set_bit_addressable_sfr: 351 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → Byte → 352 PreStatus M code_memory ≝ 353 λM: Type[0]. 354 λcode_memory:M. 355 λs: PreStatus M code_memory. 356 λb: Byte. 357 λv: Byte. 358 match sfr_of_Byte b with 359 [ None ⇒ match not_implemented in False with [ ] 360 | Some sfr8051_8052 ⇒ 361 match sfr8051_8052 with 362 [ inl sfr ⇒ 363 match sfr with 364 [ SFR_P1 ⇒ 365 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 366 set_p1_latch ?? s v 367 | SFR_P3 ⇒ 368 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 369 set_p3_latch ?? s v 370 | _ ⇒ set_8051_sfr ?? s sfr v ] 371 | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]. 372 304 373 305 definition map_address_Byte_using_internal_pseudo_address_map ≝ 374 306 λM,sigma,d,v. … … 376 308 [ None ⇒ v 377 309 | Some sfr8051_8052 ⇒ 378 match sfr8051_8052 with 379 [ inl sfr ⇒ 380 map_address_using_internal_pseudo_address_map M sigma sfr v 381 | inr _ ⇒ v ]]. 310 match sfr8051_8052 with 311 [ inl sfr ⇒ 312 map_address_using_internal_pseudo_address_map M sigma sfr v 313 | inr _ ⇒ v 314 ] 315 ]. 382 316 383 317 lemma set_bit_addressable_sfr_status_of_pseudo_status': … … 390 324 =status_of_pseudo_status M code_memory 391 325 (set_bit_addressable_sfr pseudo_assembly_program code_memory s d v) sigma policy). 326 whd in match map_address_Byte_using_internal_pseudo_address_map; 392 327 whd in match set_bit_addressable_sfr; 393 whd in match map_address_Byte_using_internal_pseudo_address_map;394 328 normalize nodelta 395 329 @(let M ≝ pseudo_assembly_program in … … 412 346 | _ ⇒ set_8051_sfr ?? s sfr v ] 413 347 | inr sfr ⇒ set_8052_sfr ?? s sfr v ]]) 414 normalize nodelta415 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/416 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta //348 normalize nodelta 349 /2 by refl, set_8051_sfr_status_of_pseudo_status, set_8052_sfr_status_of_pseudo_status/ 350 whd in match map_address_using_internal_pseudo_address_map; normalize nodelta // 417 351 qed. 418 352 … … 610 544 map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A v 611 545 | _ ⇒ v ]. 612 613 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ;614 acc_a ; acc_b ; ext_indirect ;615 ext_indirect_dptr ]]. Byte → PreStatus M code_memory ≝616 λm, cm, s, a, v.617 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;618 acc_a ; acc_b ; ext_indirect ;619 ext_indirect_dptr ]] x) →620 PreStatus m cm621 with622 [ DIRECT d ⇒623 λdirect: True.624 let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in625 match head' … bit_one with626 [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v627 | false ⇒628 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in629 set_low_internal_ram ?? s memory630 ]631 | INDIRECT i ⇒632 λindirect: True.633 let register ≝ get_register ?? s [[ false; false; i ]] in634 let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in635 match head' … bit_one with636 [ false ⇒637 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in638 set_low_internal_ram ?? s memory639 | true ⇒640 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in641 set_high_internal_ram ?? s memory642 ]643 | REGISTER r ⇒ λregister: True. set_register ?? s r v644 | ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v645 | ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v646 | EXT_INDIRECT e ⇒647 λext_indirect: True.648 let address ≝ get_register ?? s [[ false; false; e ]] in649 let padded_address ≝ pad 8 8 address in650 let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in651 set_external_ram ?? s memory652 | EXT_INDIRECT_DPTR ⇒653 λext_indirect_dptr: True.654 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in655 let memory ≝ insert ? 16 address v (external_ram ?? s) in656 set_external_ram ?? s memory657 | _ ⇒658 λother: False.659 match other in False with [ ]660 ] (subaddressing_modein … a).661 546 662 547 (*CSC: move elsewhere*) … … 767 652 >external_ram_status_of_pseudo_status @set_external_ram_status_of_pseudo_status ] 768 653 qed. 769 770 definition get_bit_addressable_sfr:771 ∀M: Type[0]. ∀code_memory: M. ∀s: PreStatus M code_memory. Byte → bool → Byte ≝772 λM: Type[0].773 λcode_memory:M.774 λs: PreStatus M code_memory.775 λb: Byte.776 λl: bool.777 match sfr_of_Byte b with778 [ None ⇒ match not_implemented in False with [ ]779 | Some sfr8051_8052 ⇒780 match sfr8051_8052 with781 [ inl sfr ⇒782 match sfr with783 [ SFR_P1 ⇒784 if l then785 p1_latch … s786 else787 get_8051_sfr … s SFR_P1788 | SFR_P3 ⇒789 if l then790 p3_latch … s791 else792 get_8051_sfr … s SFR_P3793 | _ ⇒ get_8051_sfr … s sfr794 ]795 | inr sfr ⇒ get_8052_sfr M code_memory s sfr796 ]797 ].798 799 definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ;800 acc_a ; acc_b ; data ; acc_dptr ;801 acc_pc ; ext_indirect ;802 ext_indirect_dptr ]] → Byte ≝803 λm, cm, s, l, a.804 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;805 acc_a ; acc_b ; data ; acc_dptr ;806 acc_pc ; ext_indirect ;807 ext_indirect_dptr ]] x) → ? with808 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A809 | ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B810 | DATA d ⇒ λdata: True. d811 | REGISTER r ⇒ λregister: True. get_register ?? s r812 | EXT_INDIRECT_DPTR ⇒813 λext_indirect_dptr: True.814 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in815 lookup ? 16 address (external_ram ?? s) (zero 8)816 | EXT_INDIRECT e ⇒817 λext_indirect: True.818 let address ≝ get_register ?? s [[ false; false; e ]] in819 let padded_address ≝ pad 8 8 address in820 lookup ? 16 padded_address (external_ram ?? s) (zero 8)821 | ACC_DPTR ⇒822 λacc_dptr: True.823 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in824 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in825 let 〈carry, address〉 ≝ half_add 16 dptr padded_acc in826 lookup ? 16 address (external_ram ?? s) (zero 8)827 | ACC_PC ⇒828 λacc_pc: True.829 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in830 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in831 lookup ? 16 address (external_ram ?? s) (zero 8)832 | DIRECT d ⇒833 λdirect: True.834 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 d in835 match head' … hd with836 [ true ⇒ get_bit_addressable_sfr m cm s (true:::seven_bits) l837 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)838 ]839 | INDIRECT i ⇒840 λindirect: True.841 let 〈hd, seven_bits〉 ≝ vsplit bool 1 7 (get_register … s [[false;false;i]]) in842 match head' … hd with843 [ true ⇒ lookup ? 7 seven_bits (high_internal_ram … s) (zero …)844 | false ⇒ lookup ? 7 seven_bits (low_internal_ram … s) (zero …)845 ]846 | _ ⇒ λother.847 match other in False with [ ]848 ] (subaddressing_modein … a).849 654 850 655 lemma p1_latch_status_of_pseudo_status: … … 1081 886 qed. 1082 887 1083 definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] →1084 bool → bool ≝1085 λm, cm, s, a, l.1086 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ;1087 n_bit_addr ;1088 carry ]] x) → ? with1089 [ BIT_ADDR b ⇒1090 λbit_addr: True.1091 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 b in1092 match head' … bit_1 with1093 [ true ⇒1094 let address ≝ nat_of_bitvector … seven_bits in1095 let d ≝ address ÷ 8 in1096 let m ≝ address mod 8 in1097 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in1098 let sfr ≝ get_bit_addressable_sfr ?? s trans l in1099 get_index_v … sfr m ?1100 | false ⇒1101 let address ≝ nat_of_bitvector … seven_bits in1102 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in1103 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in1104 get_index_v … t (modulus address 8) ?1105 ]1106 | N_BIT_ADDR n ⇒1107 λn_bit_addr: True.1108 let 〈bit_1, seven_bits〉 ≝ vsplit … 1 7 n in1109 match head' … bit_1 with1110 [ true ⇒1111 let address ≝ nat_of_bitvector … seven_bits in1112 let d ≝ address ÷ 8 in1113 let m ≝ address mod 8 in1114 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in1115 let sfr ≝ get_bit_addressable_sfr ?? s trans l in1116 ¬(get_index_v … sfr m ?)1117 | false ⇒1118 let address ≝ nat_of_bitvector … seven_bits in1119 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in1120 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in1121 ¬(get_index_v … t (modulus address 8) ?)1122 ]1123 | CARRY ⇒ λcarry: True. get_cy_flag ?? s1124 | _ ⇒ λother.1125 match other in False with [ ]1126 ] (subaddressing_modein … a).1127 @modulus_less_than1128 qed.1129 1130 888 definition map_bit_address_mode_using_internal_pseudo_address_map_get ≝ 1131 889 λM:internal_pseudo_address_map.λcm: pseudo_assembly_program.λs:PreStatus ? cm.λsigma: Word → Word. λaddr. λl. … … 1250 1008 qed. 1251 1009 1252 definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝1253 λm: Type[0].1254 λcm.1255 λs: PreStatus m cm.1256 λa: [[bit_addr; carry]].1257 λv: Bit.1258 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with1259 [ BIT_ADDR b ⇒ λbit_addr: True.1260 let 〈bit_1, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in1261 match head' … bit_1 with1262 [ true ⇒1263 let address ≝ nat_of_bitvector … seven_bits in1264 let d ≝ address ÷ 8 in1265 let m ≝ address mod 8 in1266 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in1267 let sfr ≝ get_bit_addressable_sfr … s t true in1268 let new_sfr ≝ set_index … sfr m v ? in1269 set_bit_addressable_sfr … s new_sfr t1270 | false ⇒1271 let address ≝ nat_of_bitvector … seven_bits in1272 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in1273 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in1274 let n_bit ≝ set_index … t (modulus address 8) v ? in1275 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in1276 set_low_internal_ram … s memory1277 ]1278 | CARRY ⇒1279 λcarry: True.1280 let 〈ignore, seven_bits〉 ≝ vsplit bool 1 7 (get_8051_sfr … s SFR_PSW) in1281 let new_psw ≝ v:::seven_bits in1282 set_8051_sfr ?? s SFR_PSW new_psw1283 | _ ⇒1284 λother: False.1285 match other in False with1286 [ ]1287 ] (subaddressing_modein … a).1288 try (repeat @le_S_S @le_O_n)1289 try @modulus_less_than1290 /by/1291 cases daemon (* XXX: russell type for preservation of clock on set_bit_addressable_sfr *)1292 qed.1293 1294 definition set_arg_1:1295 ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] →1296 Bit → PreStatus M code_memory ≝ set_arg_1'.1297 1298 1010 definition map_bit_address_mode_using_internal_pseudo_address_map_set_1 ≝ 1299 1011 λM: internal_pseudo_address_map. … … 1372 1084 status_of_pseudo_status M cm (set_arg_1 … cm ps addr b) sigma policy. 1373 1085 whd in match set_arg_1; normalize nodelta 1374 whd in match set_arg_1'; normalize nodelta1375 1086 whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_1; normalize nodelta 1376 1087 whd in match map_bit_address_mode_using_internal_pseudo_address_map_set_2; normalize nodelta … … 1433 1144 ] 1434 1145 qed. 1146 1147 lemma clock_status_of_pseudo_status: 1148 ∀M,cm,sigma,policy,s. 1149 clock … 1150 (code_memory_of_pseudo_assembly_program cm sigma policy) 1151 (status_of_pseudo_status M cm s sigma policy) 1152 = clock … cm s. 1153 // 1154 qed. 1155 1156 lemma set_clock_status_of_pseudo_status: 1157 ∀M,cm,sigma,policy,s,v. 1158 set_clock … 1159 (code_memory_of_pseudo_assembly_program cm sigma policy) 1160 (status_of_pseudo_status M cm s sigma policy) v 1161 = status_of_pseudo_status M cm (set_clock … cm s v) sigma policy. 1162 // 1163 qed.
Note: See TracChangeset
for help on using the changeset viewer.