 Timestamp:
 Feb 8, 2013, 11:49:55 AM (8 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Policy.ma
r2318 r2652 312 312 lemma measure_full: ∀program.∀policy. 313 313 measure_int program policy 0 = 2*program → ∀i.i<program → 314 is_jump (\snd (nth i ? program 〈None ?,Comment []〉)) →314 is_jump (\snd (nth i ? program 〈None ?,Comment EmptyString〉)) → 315 315 (\snd (bvt_lookup ?? (bitvector_of_nat ? i) (\snd policy) 〈0,short_jump〉)) = long_jump. 316 316 #program #policy elim program in ⊢ (% → ∀i.% → ? → %); … … 570 570 #H @H ] 571 571 #i #Hi 572 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))572 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉))) 573 573 [1,3: #Hj whd in match (jump_expansion_internal program (S (2*program))) in Geq; (*85s*) 574 574 >Feq in Geq; normalize nodelta cases Fno_ch … … 675 675  #ppc #ppc_ok normalize nodelta 676 676 >(?:\fst (fetch_pseudo_instruction (pi1 … (\snd program)) ppc ppc_ok) = 677 \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment []〉))677 \snd (nth (nat_of_bitvector … ppc) ? (\snd program) 〈None ?, Comment EmptyString〉)) 678 678 [2: whd in match fetch_pseudo_instruction; normalize nodelta 679 >(nth_safe_nth … 〈None ?, Comment []〉)680 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment []〉)679 >(nth_safe_nth … 〈None ?, Comment EmptyString〉) 680 cases (nth (nat_of_bitvector ? ppc) ? (\snd program) 〈None ?, Comment EmptyString〉) 681 681 #lbl #ins % ] 682 682 lapply (Hfpol3 ? (nat_of_bitvector ? ppc) ppc_ok) … … 750 750 >Hxpc in Hpcompact; >HSxpc whd in match create_label_map; #H 751 751 @(plus_equals_zero (2^16)) whd in match fetch_pseudo_instruction; 752 normalize nodelta >(nth_safe_nth … 〈None ?, Comment []〉)753 cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment []〉) in H;752 normalize nodelta >(nth_safe_nth … 〈None ?, Comment EmptyString〉) 753 cases (nth (nat_of_bitvector ? ppc') ? (\snd program) 〈None ?, Comment EmptyString〉) in H; 754 754 #lbl #ins normalize nodelta #X @sym_eq @X 755 755 ] 
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 ⊢ (??%?); 
src/ASM/PolicyStep.ma
r2317 r2652 927 927 elim (le_to_or_lt_eq … (le_S_S_to_le … Hi)) Hi #Hi 928 928 [ >nth_append_first [2: @Hi] lapply (Hsigma_safe i Hi) 929 inversion (nth i ? prefix 〈None ?, Comment []〉) #lbl #ins #Heq normalize nodelta929 inversion (nth i ? prefix 〈None ?, Comment EmptyString〉) #lbl #ins #Heq normalize nodelta 930 930 #Hsafe #dest #Hjump lapply (Hsafe dest Hjump) Hsafe 931 931 inversion (leb (lookup_def … labels dest 0) i) #Hle normalize nodelta … … 1201 1201 [ (* USE: policy_jump_equal → added = 0 (from fold) *) 1202 1202 @(proj2 ?? (proj1 ?? (proj1 ?? (proj1 ?? (proj1 ?? Hind))))) #i #Hi 1203 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment []〉)))1203 inversion (is_jump (\snd (nth i ? program 〈None ?, Comment EmptyString〉))) 1204 1204 [ #Hj 1205 1205 (* USE: policy_increase (from fold) *)
Note: See TracChangeset
for help on using the changeset viewer.