Changeset 2172 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jul 10, 2012, 2:39:38 PM (8 years ago)
 File:

 1 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:
Note: See TracChangeset
for help on using the changeset viewer.