- Timestamp:
- Jul 3, 2012, 3:53:32 AM (8 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
-
Assembly.ma (modified) (1 diff)
-
AssemblyProof.ma (modified) (5 diffs)
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.
