Changeset 2317 for src/ASM/PolicyStep.ma
 Timestamp:
 Sep 3, 2012, 11:36:43 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

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.