Changeset 2317
 Timestamp:
 Sep 3, 2012, 11:36:43 AM (7 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2316 r2317 566 566 ] 567 567  @(equal_compact_unsafe_compact ? Fp) 568 [ lapply (jump_pc_equal program (2*(program))) >Feq >Geq normalize nodelta 569 #H @H #i #Hi 568 [1,2: 569 [1: lapply (jump_pc_equal program (2*(program))) >Feq >Geq normalize nodelta 570 #H @H ] 571 #i #Hi 570 572 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉))) 571 [ #Hj whd in match (jump_expansion_internal program (S (2*program))) in Geq; (*85s*)573 [1,3: #Hj whd in match (jump_expansion_internal program (S (2*program))) in Geq; (*85s*) 572 574 >Feq in Geq; normalize nodelta cases Fno_ch 573 [ normalize nodelta #Heq575 [1,3: normalize nodelta #Heq 574 576 >(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) % 575  normalize nodelta cases (jump_expansion_step ???)577 2,4: normalize nodelta cases (jump_expansion_step ???) 576 578 #x cases x x #stch #sto normalize nodelta cases sto 577 [ normalize nodelta #_ #X destruct (X)578  sto #stp normalize nodelta #Hst #Heq579 [1,3: normalize nodelta #_ #X destruct (X) 580 2,4: sto #stp normalize nodelta #Hst #Heq 579 581 <(Some_eq ??? (proj2 ?? (pair_destruct ?????? (pi1_eq ???? Heq)))) 580 582 lapply (proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hst)))) i (le_S_to_le … Hi)) 581 lapply (Hfull i Hi ?) [ >Hj %]583 lapply (Hfull i Hi ?) [1,3: >Hj %] 582 584 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd Fp) 〈0,short_jump〉) 583 585 #fp #fj #Hfj >Hfj normalize nodelta 584 586 cases (bvt_lookup … (bitvector_of_nat ? i) (\snd stp) 〈0,short_jump〉) 585 587 #stp #stj cases stj normalize nodelta 586 [1,2 : #H cases H #H2 cases H2 destruct (H2)587 3 : #_ @refl588 [1,2,4,5: #H cases H #H2 cases H2 destruct (H2) 589 3,6: #_ @refl 588 590 ] 589 ] 590 ] 591  #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2:>Hj %] 592 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2:>Hj] % 591 ] 593 592 ] 594  cases daemon (* true, but have to add to properties in some way *)595  @(proj2 ?? (proj1 ?? HGp))593 2,4: #Hj >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HGp))) i Hi ?) [2,4:>Hj %] 594 >(proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? HFp))) i Hi ?) [2,4:>Hj] % 596 595 ] 597 ] 598  @(proj2 ?? HGp) 596  cases daemon (* true, but have to add to properties in some way *) 597  cases daemon 598  @(proj2 ?? (proj1 ?? HGp)) 599 599 ] 600 600 ] 601  @(proj2 ?? HGp) 602 ] 601 603 ] 602 604 ] 603  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 604 #x cases x x #nch #npol normalize nodelta #Hnpol 605 #x cases x x #Sch #Spol normalize nodelta #HSpol 606 cases npol in Hnpol; cases Spol in HSpol; 607 [ #Hnpol #HSpol %1 // 608 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // 609 #H destruct (H) 610 4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m 611 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 612 #x1 #x2 613 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 614 #y1 #y2 normalize nodelta 615 @dec_eq_jump_length 616 ] 617 ] 605 ] 606  #n cases (jump_expansion_internal program n) cases (jump_expansion_internal program (S n)) 607 #x cases x x #nch #npol normalize nodelta #Hnpol 608 #x cases x x #Sch #Spol normalize nodelta #HSpol 609 cases npol in Hnpol; cases Spol in HSpol; 610 [ #Hnpol #HSpol %1 // 611 2,3: #x #Hnpol #HSpol %2 @nmk whd in match (policy_equal_opt ???); // 612 #H destruct (H) 613 4: #np #Hnp #Sp #HSp whd in match (policy_equal_opt ???); @dec_bounded_forall #m 614 cases (bvt_lookup ?? (bitvector_of_nat 16 m) ? 〈0,short_jump〉) 615 #x1 #x2 616 cases (bvt_lookup ?? (bitvector_of_nat ? m) ? 〈0,short_jump〉) 617 #y1 #y2 normalize nodelta 618 @dec_eq_jump_length 619 ] 620 ] 618 621 qed. 619 622 
src/ASM/PolicyStep.ma
r2316 r2317 752 752 qed. 753 753 754 (*definition sigma_safe_weak ≝755 λprefix:list labelled_instruction.λlabels:label_map.756 λsigma:ppc_pc_map.757 ∀i.i < prefix →758 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in759 ∀lbl.is_jump_to instr lbl →760 let paddr ≝ lookup_def … labels lbl 0 in761 let 〈j,src,dest〉 ≝762 let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in763 let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in764 let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in765 〈j,pc_plus_jmp_length,addr〉 in766 i < paddr →767 match j with768 [ short_jump ⇒ \fst (short_jump_cond src dest) = true769  absolute_jump ⇒ \fst (absolute_jump_cond src dest) = true (*∧770 \fst (short_jump_cond src dest) = false*)771  long_jump ⇒ True (* do not talk about long jump *)772 ].*)773 774 (*lemma sigma_safe_weak_sigma_safe:775 ∀program.∀labels.∀old_sigma.∀sigma.776 sigma_safe program labels old_sigma sigma →777 sigma_safe_weak program labels sigma.778 #program #labels #old_sigma #sigma #Hsigma_safe779 #i #Hi lapply (Hsigma_safe i Hi)780 cases (nth i ? program 〈None ?, Comment []〉) #label #instr normalize nodelta781 #Hsigma_safe #dest #Hjump lapply (Hsigma_safe dest Hjump) Hsigma_safe782 cases (lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) #pc #j783 normalize nodelta #Hsigma_safe #Hle784 >(not_le_to_leb_false … (lt_to_not_le … Hle)) in Hsigma_safe; normalize nodelta785 786 qed.*)787 788 lemma length_of_is_isize: ∀i.is_jump (Instruction i) →789 length_of i = instruction_size_jmplen short_jump (Instruction i).790 #i cases i791 try (#x #y #Hj) try (#x #Hj) try (#Hj) try (cases Hj) try (%)792 try ( @(subaddressing_mode_elim … x) #w ) try (%)793 cases x * #a1 #a2 normalize nodelta794 @(subaddressing_mode_elim … a1) try (#w %)795 @(subaddressing_mode_elim … a2) #w %796 qed.797 798 754 lemma jump_expansion_step9: 799 755 ∀program : list labelled_instruction.
Note: See TracChangeset
for help on using the changeset viewer.