Changeset 2652 for src/ASM/PolicyFront.ma
 Timestamp:
 Feb 8, 2013, 11:49:55 AM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyFront.ma
r2318 r2652 20 20 λprefix:list labelled_instruction.λsigma:ppc_pc_map. 21 21 ∀i:ℕ.i < prefix → 22 ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment []〉)) →22 ¬is_jump (\snd (nth i ? prefix 〈None ?, Comment EmptyString〉)) → 23 23 \snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump. 24 24 … … 175 175 [ None ⇒ False 176 176  Some x1 ⇒ let 〈pc1,j1〉 ≝ x1 in 177 pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment []〉))177 pc1 = pc + instruction_size_jmplen j (\snd (nth n ? prefix 〈None ?, Comment EmptyString〉)) 178 178 ] 179 179 ]. … … 193 193 (λppc.bitvector_of_nat ? (\fst (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) 194 194 (λppc.jmpeqb long_jump (\snd (bvt_lookup ?? ppc (\snd sigma) 〈0,short_jump〉))) 195 (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment []〉))195 (bitvector_of_nat ? n) (\snd (nth n ? program 〈None ?, Comment EmptyString〉)) 196 196 ] 197 197 ]. … … 227 227 λprefix:list labelled_instruction.λsigma:ppc_pc_map. 228 228 ∀i.i < prefix → 229 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment []〉 in229 let 〈label,instr〉 ≝ nth i ? prefix 〈None ?, Comment EmptyString〉 in 230 230 (\snd (bvt_lookup … (bitvector_of_nat ? i) (\snd sigma) 〈0,short_jump〉) = short_jump → 231 231 bool_to_Prop (¬is_call instr)) ∧ … … 565 565 definition nec_plus_ultra ≝ 566 566 λprogram:list labelled_instruction.λp:ppc_pc_map. 567 ¬(∀i.i < program → is_jump (\snd (nth i ? program 〈None ?, Comment []〉)) →567 ¬(∀i.i < program → is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉)) → 568 568 \snd (bvt_lookup … (bitvector_of_nat 16 i) (\snd p) 〈0,short_jump〉) = long_jump). 569 569 … … 627 627 type *) 628 628 cut (instruction_size_jmplen jl 629 (\snd (nth i ? program 〈None ?, Comment []〉)) =629 (\snd (nth i ? program 〈None ?, Comment EmptyString〉)) = 630 630 instruction_size … (bitvector_of_nat ? i) 631 (\snd (nth i ? program 〈None ?, Comment []〉)))631 (\snd (nth i ? program 〈None ?, Comment EmptyString〉))) 632 632 [6: #H <H @Hcp_unsafe 633 633 5: whd in match (instruction_size_jmplen ??); … … 635 635 whd in match (assembly_1_pseudoinstruction …); 636 636 whd in match (expand_pseudo_instruction …); 637 normalize nodelta inversion (nth i ? program 〈None ?,Comment []〉) in Hsafe;637 normalize nodelta inversion (nth i ? program 〈None ?,Comment EmptyString〉) in Hsafe; 638 638 #lbl #instr cases instr 639 639 [1: #pi normalize nodelta cases pi … … 696 696 [1,5,9,13,17,21,25,29,33,37,41: 697 697 whd in match fetch_pseudo_instruction; normalize nodelta 698 >(nth_safe_nth … 〈None ?, Comment []〉) >nat_of_bitvector_bitvector_of_nat_inverse698 >(nth_safe_nth … 〈None ?, Comment EmptyString〉) >nat_of_bitvector_bitvector_of_nat_inverse 699 699 [1: >Hnth_eq in ⊢ (??%?); 700 700 3: >Hnth_eq in ⊢ (??%?);
Note: See TracChangeset
for help on using the changeset viewer.