Changeset 2317 for src/ASM/PolicyStep.ma

Timestamp:

Sep 3, 2012, 11:36:43 AM (8 years ago)

Author:

boender

Message:

• small changes to make things compile

File:

• src/ASM/PolicyStep.ma (modified) (1 diff)

src/ASM/PolicyStep.ma

@@ -752 +752 @@
 qed.
 
-(*definition sigma_safe_weak ≝ 
- λprefix:list labelled_instruction.λlabels:label_map.
- λsigma:ppc_pc_map.
- ∀i.i < |prefix| →
- let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment [ ]〉 in
- ∀lbl.is_jump_to instr lbl → 
- let paddr ≝ lookup_def … labels lbl 0 in
- let 〈j,src,dest〉 ≝ 
-   let 〈pc,j〉 ≝ bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉 in
-   let pc_plus_jmp_length ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? (S i)) (\snd sigma) 〈0,short_jump〉)) in
-   let addr ≝ bitvector_of_nat ? (\fst (bvt_lookup … (bitvector_of_nat ? paddr) (\snd sigma) 〈0,short_jump〉)) in
-   〈j,pc_plus_jmp_length,addr〉 in     
- i < paddr → 
- match j with
- [ short_jump ⇒ \fst (short_jump_cond src dest) = true
- | absolute_jump ⇒  \fst (absolute_jump_cond src dest) = true (*∧
-      \fst (short_jump_cond src dest) = false*)
- | long_jump   ⇒ True (* do not talk about long jump *)
- ].*)
-
-(*lemma sigma_safe_weak_sigma_safe:
-  ∀program.∀labels.∀old_sigma.∀sigma.
-  sigma_safe program labels old_sigma sigma →
-  sigma_safe_weak program labels sigma.
- #program #labels #old_sigma #sigma #Hsigma_safe
- #i #Hi lapply (Hsigma_safe i Hi)
- cases (nth i ? program 〈None ?, Comment []〉) #label #instr normalize nodelta
- #Hsigma_safe #dest #Hjump lapply (Hsigma_safe dest Hjump) -Hsigma_safe
- cases (lookup … (bitvector_of_nat 16 i) (\snd sigma) 〈0,short_jump〉) #pc #j
- normalize nodelta #Hsigma_safe #Hle
- >(not_le_to_leb_false … (lt_to_not_le … Hle)) in Hsigma_safe; normalize nodelta
- 
-qed.*)
-
-lemma length_of_is_isize: ∀i.is_jump (Instruction i) → 
-  length_of i = instruction_size_jmplen short_jump (Instruction i).
- #i cases i
- try (#x #y #Hj) try (#x #Hj) try (#Hj) try (cases Hj) try (%)
- try ( @(subaddressing_mode_elim … x) #w )  try (%)
- cases x * #a1 #a2 normalize nodelta
- @(subaddressing_mode_elim … a1) try (#w %)
- @(subaddressing_mode_elim … a2) #w %
-qed.
-
 lemma jump_expansion_step9:
  ∀program : list labelled_instruction.