Changeset 2164
 Timestamp:
 Jul 7, 2012, 3:00:44 AM (5 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Test.ma
r2163 r2164 72 72 let mapped ≝ sigma word in 73 73 let 〈high, low〉 ≝ vsplit bool 8 8 mapped in 74 if eq_upper_lower upper_lower upper then 75 high 76 else 77 low 78 ]. 79 80 (*CSC: Taken from AssemblyProofSplit.ma; there named map_lower_internal... *) 81 definition map_internal_ram_address_using_pseudo_address_map: 82 ∀M: internal_pseudo_address_map. (Word → Word) → Byte → Byte → Byte ≝ 83 λM: internal_pseudo_address_map. 84 λsigma: Word → Word. 85 λaddress: Byte. 86 λvalue: Byte. 87 match assoc_list_lookup ?? address (eq_bv …) (\fst M) with 88 [ None ⇒ value 89  Some upper_lower_word ⇒ 90 let 〈upper_lower, word〉 ≝ upper_lower_word in 91 let 〈high, low〉 ≝ vsplit bool 8 8 (sigma word) in 74 92 if eq_upper_lower upper_lower upper then 75 93 high … … 319 337 qed. 320 338 321 check status_of_pseudo_status 322 323 lemma set_low_internal_fram_status_of_pseudo_status: 339 lemma set_low_internal_ram_status_of_pseudo_status: 324 340 ∀cm,sigma,policy,M,s,ram. 325 341 set_low_internal_ram (BitVectorTrie Byte 16) … … 331 347 // 332 348 qed. 349 350 (* Real axiom ATM *) 351 axiom insert_low_internal_ram_of_pseudo_low_internal_ram: 352 ∀M,sigma,cm,s,addr,v,v'. 353 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → 354 insert Byte 7 addr v' 355 (low_internal_ram_of_pseudo_low_internal_ram M 356 (low_internal_ram pseudo_assembly_program cm s)) 357 =low_internal_ram_of_pseudo_low_internal_ram M 358 (insert Byte 7 addr v (low_internal_ram pseudo_assembly_program cm s)). 333 359 334 lemma set_low_internal_fram_status_of_pseudo_status: 335 ∀M,cm,sigma,policy,s,addr,v. 336 insert Byte 7 addr v 360 lemma insert_low_internal_ram_status_of_pseudo_status: 361 ∀M,cm,sigma,policy,s,addr,v,v'. 362 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) v = v' → 363 insert Byte 7 addr v' 337 364 (low_internal_ram (BitVectorTrie Byte 16) 338 365 (code_memory_of_pseudo_assembly_program cm sigma policy) … … 341 368 (insert Byte 7 addr v 342 369 (low_internal_ram pseudo_assembly_program cm s)). 343 #M #cm #sigma #policy #s #addr #v 344 345 346 definition map_address_mode_using_internal_pseudo_address_map ≝ 347 λM,sigma,addr,v. 370 /2 by insert_low_internal_ram_of_pseudo_low_internal_ram/ 371 qed. 372 373 (*CSC: Taken from AssemblyProofSplit *) 374 lemma get_index_v_set_index_miss: 375 ∀T: Type[0]. 376 ∀n, i, j: nat. 377 ∀v: Vector T n. 378 ∀b: T. 379 ∀i_proof: i < n. 380 ∀j_proof: j < n. 381 i ≠ j → 382 get_index_v T n (set_index T n v i b i_proof) j j_proof = 383 get_index_v T n v j j_proof. 384 #T #n #i #j #v lapply i lapply j elim v #i #j 385 [1: 386 #b #i_proof 387 cases (lt_to_not_zero … i_proof) 388 2: 389 #tl #inductive_hypothesis #j' #i' #b #i_proof #j_proof #i_neq_j 390 lapply i_proof lapply i_neq_j cases i' 391 [1: 392 i_neq_j #i_neq_j i_proof #i_proof 393 whd in match (set_index ??????); 394 lapply j_proof lapply i_neq_j cases j' 395 [1: 396 #relevant @⊥ cases relevant relevant #absurd @absurd % 397 2: 398 #j' #_ j_proof #j_proof % 399 ] 400 2: 401 #i' i_neq_j #i_neq_j i_proof #i_proof 402 lapply j_proof lapply i_neq_j cases j' 403 [1: 404 #_ #j_proof % 405 2: 406 #j' #i_neq_j #j_proof 407 @inductive_hypothesis @nmk #relevant 408 cases i_neq_j #absurd @absurd >relevant % 409 ] 410 ] 411 ] 412 qed. 413 414 lemma get_8051_sfr_status_of_pseudo_status: 415 ∀M,cm,s,sigma,policy,sfr. 416 get_8051_sfr … 417 (code_memory_of_pseudo_assembly_program cm sigma policy) 418 (status_of_pseudo_status M cm s sigma policy) sfr = 419 map_address_using_internal_pseudo_address_map M sigma sfr 420 (get_8051_sfr … cm s sfr). 421 #M #cm #s #sigma #policy #sfr whd in ⊢ (??%%); 422 whd in match status_of_pseudo_status; normalize nodelta 423 whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 424 whd in match map_acc_a_using_internal_pseudo_address_map; normalize nodelta 425 cases (\snd M) normalize nodelta [cases sfr %] 426 #map_mem #map_acc @pair_elim #high #low #_ normalize nodelta 427 cases (eq_upper_lower ??) normalize nodelta cases sfr normalize nodelta 428 [18,37: @get_index_v_set_index 429 *: >get_index_v_set_index_miss % normalize #abs destruct] 430 qed. 431 432 lemma bit_address_of_register_status_of_pseudo_status: 433 ∀M,cm,s,sigma,policy,r. 434 bit_address_of_register … 435 (code_memory_of_pseudo_assembly_program cm sigma policy) 436 (status_of_pseudo_status M cm s sigma policy) r = 437 bit_address_of_register … cm s r. 438 #M #cm #s #sigma #policy #r whd in ⊢ (??%%); 439 >get_8051_sfr_status_of_pseudo_status 440 @pair_elim #un #ln #_ 441 @pair_elim #r1 #r0 #_ % 442 qed. 443 444 (*CSC: provable using the axiom in AssemblyProof, but this one seems more 445 primitive *) 446 axiom lookup_low_internal_ram_of_pseudo_low_internal_ram: 447 ∀M,sigma,cm,s,addr. 448 lookup Byte 7 addr 449 (low_internal_ram_of_pseudo_low_internal_ram M 450 (low_internal_ram pseudo_assembly_program cm s)) (zero 8) 451 = 452 map_internal_ram_address_using_pseudo_address_map M sigma (false:::addr) 453 (lookup Byte 7 addr 454 (low_internal_ram pseudo_assembly_program cm s) (zero 8)). 455 456 lemma get_register_status_of_pseudo_status: 457 ∀M,cm,sigma,policy,s,r. 458 get_register … 459 (code_memory_of_pseudo_assembly_program cm sigma policy) 460 (status_of_pseudo_status M cm s sigma policy) r = 461 map_internal_ram_address_using_pseudo_address_map M sigma (false:::bit_address_of_register pseudo_assembly_program cm s r) 462 (get_register … cm s r). 463 #M #cm #sigma #policy #s #r whd in match get_register; normalize nodelta 464 whd in match status_of_pseudo_status; normalize nodelta 465 >bit_address_of_register_status_of_pseudo_status 466 @lookup_low_internal_ram_of_pseudo_low_internal_ram 467 qed. 468 469 definition map_address_mode_using_internal_pseudo_address_map_ok ≝ 470 λM,sigma,cm.λs:PreStatus ? cm.λaddr,v,v'. 348 471 match addr with 349 472 [ DIRECT d ⇒ 350 let 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4d in351 match get_index_v ? ? nu 0 ?with473 let 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit … 1 7 d in 474 match head' … bit_one with 352 475 [ true ⇒ 353 map_address_Byte_using_internal_pseudo_address_map M sigma d v 354  false ⇒ v ] 355  _ ⇒ v ]. 356 // 357 qed. 476 map_address_Byte_using_internal_pseudo_address_map M sigma (true:::seven_bits) v 477  false ⇒ 478 map_internal_ram_address_using_pseudo_address_map M sigma (false:::seven_bits) v ] = v' 479  INDIRECT i ⇒ 480 assoc_list_lookup ?? 481 (false:::bit_address_of_register pseudo_assembly_program cm s [[false; false; i]]) (eq_bv …) (\fst M) = None … ∧ 482 let register ≝ get_register ?? s [[ false; false; i ]] in 483 map_internal_ram_address_using_pseudo_address_map M sigma register v = v' 484  _ ⇒ v = v']. 358 485 359 486 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. ∀addr: [[ direct ; indirect ; registr ; … … 368 495 [ DIRECT d ⇒ 369 496 λdirect: True. 370 let 〈 nu, nl 〉 ≝ vsplit … 4 4 d in 371 let bit_one ≝ get_index_v ? ? nu 0 ? in 372 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in 373 match bit_one with 374 [ true ⇒ set_bit_addressable_sfr ?? s d v 497 let 〈 bit_one, seven_bits 〉 ≝ vsplit ? 1 7 d in 498 match head' … bit_one with 499 [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v 375 500  false ⇒ 376 let memory ≝ insert ? 7 (three_bits @@ nl)v (low_internal_ram ?? s) in501 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in 377 502 set_low_internal_ram ?? s memory 378 503 ] … … 380 505 λindirect: True. 381 506 let register ≝ get_register ?? s [[ false; false; i ]] in 382 let 〈nu, nl〉 ≝ vsplit ? 4 4 register in 383 let bit_1 ≝ get_index_v … nu 0 ? in 384 let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in 385 match bit_1 with 507 let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in 508 match head' … bit_one with 386 509 [ false ⇒ 387 let memory ≝ insert … (three_bits @@ nl)v (low_internal_ram ?? s) in510 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in 388 511 set_low_internal_ram ?? s memory 389 512  true ⇒ 390 let memory ≝ insert … (three_bits @@ nl)v (high_internal_ram ?? s) in513 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in 391 514 set_high_internal_ram ?? s memory 392 515 ] … … 409 532 match other in False with [ ] 410 533 ] (subaddressing_modein … a). 411 // 534 535 (*CSC: move elsewhere*) 536 lemma eq_head': ∀A,n,v. v = head' A n v ::: tail … v. 537 #A #n #v inversion v in ⊢ ?; 538 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) /2/ 539  #m #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ' >EQ' % ] 540 qed. 541 542 (*CSC: move elsewhere*) 543 lemma tail_singleton: ∀A,v. tail A 0 v = [[]]. 544 #A #v inversion v in ⊢ ?; 545 [ #abs @⊥ lapply (jmeq_to_eq ??? abs) #H destruct(H) 546  #n #hd #tl #_ #EQ <(injective_S … EQ) in tl; #tl #EQ1 >EQ1 normalize 547 /2 by jmeq_to_eq/ 548 ] 549 qed. 550 551 (*CSC: move elsewhere*) 552 lemma eq_cons_head_append: 553 ∀A,n.∀hd: Vector A 1. ∀tl: Vector A n. 554 head' A 0 hd:::tl = hd@@tl. 555 #A #n #hd #tl >(eq_head' … hd) >tail_singleton % 412 556 qed. 413 557 … … 417 561 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]]. 418 562 ∀value. Σp: PreStatus ? cm. ∀M. ∀sigma. ∀policy. ∀value'. 419 map_address_mode_using_internal_pseudo_address_map M sigma addr value =value' →563 map_address_mode_using_internal_pseudo_address_map_ok … M sigma cm ps addr value value' → 420 564 set_arg_8 (BitVectorTrie Byte 16) 421 565 (code_memory_of_pseudo_assembly_program cm sigma policy) … … 434 578 [ DIRECT d ⇒ 435 579 λdirect: True. 436 deplet 〈 nu, nl 〉 as vsplit_refl ≝ vsplit … 4 4 d in 437 let bit_one ≝ get_index_v ? ? nu 0 ? in 438 let 〈 ignore, three_bits 〉 ≝ vsplit ? 1 3 nu in 439 match bit_one with 440 [ true ⇒ set_bit_addressable_sfr ?? s d v 580 deplet 〈 bit_one, seven_bits 〉 as vsplit_refl ≝ vsplit ? 1 7 d in 581 match head' … bit_one with 582 [ true ⇒ set_bit_addressable_sfr ?? s (true:::seven_bits) v 441 583  false ⇒ 442 let memory ≝ insert ? 7 (three_bits @@ nl)v (low_internal_ram ?? s) in584 let memory ≝ insert ? 7 seven_bits v (low_internal_ram ?? s) in 443 585 set_low_internal_ram ?? s memory 444 586 ] … … 446 588 λindirect: True. 447 589 let register ≝ get_register ?? s [[ false; false; i ]] in 448 let 〈nu, nl〉 ≝ vsplit ? 4 4 register in 449 let bit_1 ≝ get_index_v … nu 0 ? in 450 let 〈ignore, three_bits〉 ≝ vsplit ? 1 3 nu in 451 match bit_1 with 590 let 〈bit_one, seven_bits〉 ≝ vsplit ? 1 7 register in 591 match head' … bit_one with 452 592 [ false ⇒ 453 let memory ≝ insert … (three_bits @@ nl)v (low_internal_ram ?? s) in593 let memory ≝ insert … seven_bits v (low_internal_ram ?? s) in 454 594 set_low_internal_ram ?? s memory 455 595  true ⇒ 456 let memory ≝ insert … (three_bits @@ nl)v (high_internal_ram ?? s) in596 let memory ≝ insert … seven_bits v (high_internal_ram ?? s) in 457 597 set_high_internal_ram ?? s memory 458 598 ] … … 475 615 match other in False with [ ] 476 616 ] (subaddressing_modein … a)) normalize nodelta 477 [3,6: // ] #M #sigma #policy #v' whd in ⊢ (??%? → ?);617 #M #sigma #policy #v' whd in match map_address_mode_using_internal_pseudo_address_map_ok; normalize nodelta 478 618 [1,2: 479 619 <vsplit_refl normalize nodelta >p normalize nodelta 480 normalize nodelta in p1; >p1 normalize nodelta 481 [ @set_bit_addressable_sfr_status_of_pseudo_status 482  #v_ok <v_ok @set_low_internal_ram_status_of_pseudo_status 483 ] 484 2: 485 qed. 620 [ >(vsplit_ok … vsplit_refl) @set_bit_addressable_sfr_status_of_pseudo_status 621  #v_ok >(insert_low_internal_ram_status_of_pseudo_status … v) // ] 622 3,4: * #EQ1 #EQ2 change with (get_register ????) in match register in p; 623 >get_register_status_of_pseudo_status 624 whd in match map_internal_ram_address_using_pseudo_address_map; normalize nodelta 625 >EQ1 normalize nodelta >p normalize nodelta >p1 normalize nodelta 626 [ 627  >(insert_low_internal_ram_status_of_pseudo_status … v) // <EQ2 628 @eq_f2 try % <(vsplit_ok … (sym_eq … p)) <eq_cons_head_append >p1 % ] 629 qed.
Note: See TracChangeset
for help on using the changeset viewer.