Changeset 2147
 Timestamp:
 Jul 3, 2012, 3:53:32 AM (5 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Assembly.ma
r2146 r2147 730 730 let 〈len,assembledi〉 ≝ 731 731 assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi in 732 assembledi ≤ assembled ∧ 732 733 ∀j:nat. ∀H: j < assembledi. ∀K. 733 734 nth_safe ? j assembledi H = 
src/ASM/AssemblyProof.ma
r2146 r2147 448 448 lapply (assembly_ok2 ppc ?) try // assembly_ok2 449 449 >eq_fetch_pseudo_instruction 450 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<assembledi.?) → ?)450 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ? ∧ ∀j.∀H:j<assembledi.?) → ?) 451 451 >eq_assembly_1_pseudoinstruction 452 whd in ⊢ (% → ?); #assembly_ok452 whd in ⊢ (% → ?); * #assembly_ok4 #assembly_ok 453 453 % 454 454 [2: >(pair_destruct_2 ????? (sym_eq … eq_fetch_pseudo_instruction)) … … 472 472 [1: #j #H <load_code_memory_ok 473 473 [ @assembly_ok 474  cases assembly_ok3 assembly_ok3 474  cut (0=assembled' → False) 475 [ #abs <abs in assembly_ok4; >EQlen #abs' 476 @(absurd ?? (not_le_Sn_O j)) @(transitive_le … H) assumption ] #NOT_EMPTY 477 cases assembly_ok3 assembly_ok3 475 478 [2: * #_ #EQ2 >EQ2 @lt_nat_of_bitvector ] 476 479 #EQlen_assembled' <EQlen_assembled' … … 483 486 [2: * #EQ1 #EQ2 @⊥ <EQ1 in EQlen_assembled'; 484 487 <add_bitvector_of_nat_Sm >add_commutative 485 >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2 486 whd in ⊢ (??%? → ?); #EQlen_assembled' 487 cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) ] 488 >bitvector_of_nat_inverse_nat_of_bitvector >OK >EQ2 assumption ] 488 489 cases (le_to_or_lt_eq … instr_list_ok) 489 490 [2: #abs @⊥ >abs in EQlen_assembled'; >bitvector_of_nat_exp_zero >sigma_zero 490 whd in ⊢ (??%? → ?); #EQlen_assembled' 491 cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) ] 492 ] 491 assumption ] 493 492 #instr_list_ok' #NO_OVERFLOW 494 493 @(lt_to_le_to_lt … (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))))) … … 509 508 >nat_of_bitvector_add <plus_n_Sm <plus_n_O try assumption 510 509 @(transitive_le … instr_list_ok') @le_S_S assumption 511  * #EQ1 @⊥ >EQ1 in EQlen_assembled'; 512 whd in ⊢ (??%? → ?); #EQlen_assembled' 513 cases daemon (*CSC: need lemma: assembled'=0 → assembled=0 → absurdum *) 514 ] 515 ] 516 (* OLD CODE [ #assembly_ok1' 517 cut (nat_of_bitvector 16 (sigma ppc)+assembled≤assembled') 518 [ cases sigma_policy_witness #_ >EQprogram #sigma_ok 519 cases (sigma_ok … ppc_ok) sigma_ok >eq_fetch_pseudo_instruction 520 whd in match instruction_size; normalize nodelta 521 >create_label_cost_refl 522 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 523 [>eq_assembly_1_pseudoinstruction 2: skip] #OK >OK <EQlen * 524 [ #JAP1 525 cut (nat_of_bitvector … (sigma ppc) + len < 2^16) 526 [cases daemon (*CSC: provable, needs lemma*)] #LT1 527 <(nat_of_bitvector_bitvector_of_nat_inverse 16 len) 528 [2: @(le_to_lt_to_lt … LT1) / by / ] 529 cases assembly_ok3 530 [2: * #_ #abs @⊥ @(absurd … abs (lt_to_not_eq … assembly_ok1')) ] 531 #EQ_sigma_instr_list <EQ_sigma_instr_list 532 <nat_of_bitvector_add 533 [2: >nat_of_bitvector_bitvector_of_nat_inverse try assumption 534 @(transitive_le … LT1) @le_S_S / by / ] 535 <OK XXX 536 537 XXX cases daemon (*CSC: ???*) 538  assembly_ok3 #assembly_ok3 539 <assembly_ok3 540 (*CSC: we have to go by cases here!*) 541 <nat_of_bitvector_add 542 [2: cases daemon ] (*CSC: end of wrong part*) 543 544  545 ] 546 547 548 #JAP1 549 <(nat_of_bitvector_bitvector_of_nat_inverse 16 len) 550 [2: cases daemon ] 551 cases assembly_ok3 552 [2: * #_ #EQ2 cases daemon (*CSC: ???*) 553  assembly_ok3 #assembly_ok3 554 <assembly_ok3 555 (*CSC: we have to go by cases here!*) 556 <nat_of_bitvector_add 557 [2: cases daemon ] (*CSC: end of wrong part*) 558 559 560 cases assembly_ok3 561 [2: * #_ #EQ2 cases daemon (*CSC: ???*) 562  assembly_ok3 #assembly_ok3 563 <assembly_ok3 cases sigma_policy_witness #_ >EQprogram #sigma_ok 564 cases (sigma_ok … ppc_ok) sigma_ok >eq_fetch_pseudo_instruction 565 whd in match instruction_size; normalize nodelta 566 >create_label_cost_refl 567 >fst_assembly_1_pseudoinstruction_insensible_to_lookup_datalabels 568 [>eq_assembly_1_pseudoinstruction 2: skip] #OK #_ <EQlen 569 <(nat_of_bitvector_bitvector_of_nat_inverse 16 len) 570 [2: cases daemon ] 571 <nat_of_bitvector_add 572 [2: cases daemon ] 573 <OK @(monotone_sigma2 … sigma_policy_witness) >EQprogram 574 cases daemon (*CSC: ???*) 575 ] 576  #LE2 577 cut (assembled < 2^16) 578 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) / by /] #LTassembled 579 cut (nat_of_bitvector … (add … (sigma ppc) (bitvector_of_nat … (assembled))) ≤ assembled') 580 [ >nat_of_bitvector_add 581 >nat_of_bitvector_bitvector_of_nat_inverse try assumption 582 @(le_to_lt_to_lt … LE2 assembly_ok1') 583  #LE @(lt_to_le_to_lt … LE) 584 @lt_to_lt_nat_of_bitvector_add 585 [ @(eq_ind ?? (λp.λ_. \snd p < 2^16) ?? eq_assembly_1_pseudoinstruction) 586 / by / 587  @(le_to_lt_to_lt ???? assembly_ok1') @LE2 588  assumption 589 ] 590 ] 591 ] 592  #assembly_ok1' >assembly_ok1' / by / 593 ]*) 510  * #EQ1 @⊥ >EQ1 in EQlen_assembled'; assumption ]]] 594 511 2: 595 512 assembly_ok load_code_memory_ok generalize in match (sigma ppc); >EQlen len … … 604 521 @IH IH #j #LTj lapply (H (S j) ?) [ @le_S_S @LTj ] 605 522 <(nth_safe_prepend … [hd] … LTj) #IH >IH <add_bitvector_of_nat_Sm 606 >add_associative % ]] 607 ]] 523 >add_associative % ]]]] 608 524 qed. 609 525
Note: See TracChangeset
for help on using the changeset viewer.