 Timestamp:
 Feb 22, 2013, 11:20:03 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/PolicyStep.ma
r2652 r2714 71 71  <Heq2 >Hi >lookup_insert_miss 72 72 [ >lookup_insert_hit cases instr in Heq1; 73 [2,3,6: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 74 4,5: #x normalize nodelta #Heq1 >nth_append_second try % 73 [2,3,8: #x [3: #y] normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ @refl 74 5,6: #x #y #z normalize nodelta #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) #_ % 75 4,7: #x normalize nodelta #Heq1 >nth_append_second try % 75 76 <minus_n_n #abs cases abs 76 77 1: #pi normalize nodelta >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); … … 146 147 Comment (_:String)⇒None jump_length 147 148 Cost (_:costlabel)⇒None jump_length 149 Jnz _ _ _ ⇒ None ? 150 MovSuccessor _ _ _ ⇒ None ? 148 151 Jmp (j:Identifier)⇒ 149 152 Some jump_length … … 203 206 [ >lookup_insert_hit normalize nodelta 204 207 inversion instr in Heq1; normalize nodelta 205 [4, 5: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length208 [4,7: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 206 209  #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta 207 210 lapply (destination_of_None_to_is_jump_false pi) … … 211 214  #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 212 215 ] 213 2,3,6: #x [3: #y] #Heqi ] 216 5,6: #x #y #z #Heqi 217 2,3,8: #x [3: #y] #Heqi ] 214 218 #Hj <(proj1 ?? (pair_destruct ?????? Hj)) 215 219 lapply (pi2 ?? old_sigma (prefix) ??) try assumption 216 [1,3,5,7 : >prf >nth_append_second try @le_n220 [1,3,5,7,9,11: >prf >nth_append_second try @le_n 217 221 <minus_n_n whd in match (nth ????); >p1 >Heqi 218 222 whd in match is_jump; normalize nodelta try % >Hx % … … 261 265 Comment (_:String)⇒None jump_length 262 266 Cost (_:costlabel)⇒None jump_length 267 Jnz _ _ _ ⇒ None ? 268 MovSuccessor _ _ _ ⇒ None ? 263 269 Jmp (j:Identifier)⇒ 264 270 Some jump_length … … 426 432 >Hpolicy1 427 433 [ cases instr in Heq1 Heq; 428 [2,3,6: #x [3: #y] normalize nodelta #_ #_ % 434 [2,3,8: #x [3: #y] normalize nodelta #_ #_ % 435 5,6: #x #y #z #_ #_ % 429 436 1: #pi normalize nodelta whd in match jump_expansion_step_instruction; 430 437 normalize nodelta cases (destination_of ?) normalize nodelta [#_ #_ %]] … … 575 582 cases (destination_of ?) normalize nodelta 576 583 [ #_ #dest_None  #tgt #dest_Some #_ ]] 584 try (#x #y #z #Heq1 #Hadded #X) 577 585 try (#x #y #Heq1 #Hadded #X) try (#x #Heq1 #Hadded #X) try (#Heq1 #Hadded #X) 578 586 <(proj2 ?? (pair_destruct ?????? Heq1)) >X @plus_left_monotone 579 [1,3,4, 7: @instruction_size_irrelevant try %587 [1,3,4,6,7,9: @instruction_size_irrelevant try % 580 588 whd in match is_jump; normalize nodelta >dest_None % 581 589 *: >(lookup_opt_lookup_hit … EQ 〈0,short_jump〉) in Holdeq; #EQ' … … 718 726 (* USE: sigma_compact_unsafe (from old_sigma) *) 719 727 lapply (proj1 ?? (pi2 ?? old_sigma) (prefix) ?) 720 [1,3,5,7,9,11,13,15 : >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r]728 [1,3,5,7,9,11,13,15,17: >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r] 721 729 lapply Holdeq Holdeq 722 730 inversion (bvt_lookup_opt … (bitvector_of_nat ? (prefix)) (\snd old_sigma)) 723 [1,3,5,7,9,11,13,15 : normalize nodelta #_ #_ #abs cases abs]731 [1,3,5,7,9,11,13,15,17: normalize nodelta #_ #_ #abs cases abs] 724 732 inversion (bvt_lookup_opt … (bitvector_of_nat ? (S (prefix))) (\snd old_sigma)) 725 [1,3,5,7,9,11,13,15: normalize nodelta #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs] 733 normalize nodelta 734 [1,3,5,7,9,11,13,15,17: #_ * #Spc #Sj normalize nodelta #_ #_ #abs cases abs] 726 735 * #Spc #Sj #EQS * #pc #j #Holdeq #EQ normalize nodelta 727 736 #H (* USE: fst p = lookup prefix *) (*CSC: This part of the proof is repeated somewhere else*) … … 729 738 (* USE[pass]: lookup p = lookup old_sigma + added *) 730 739 >Hpolicy2 731 [1,3,4, 7:740 [1,3,4,6,7,9: 732 741 >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; 733 742 Holdeq #EQ <(proj1 ?? (pair_destruct ?????? EQ)) … … 737 746 @plus_right_monotone @instruction_size_irrelevant try % 738 747 whd in match is_jump; normalize nodelta >y % 739 2,5,6 :748 2,5,6,8: 740 749 >(lookup_opt_lookup_hit … EQS 〈0,short_jump〉) >H 741 750 >(lookup_opt_lookup_hit … Holdeq 〈0,short_jump〉) in EQ; #EQ … … 859 868 Comment (_:String)⇒None jump_length 860 869 Cost (_:costlabel)⇒None jump_length 870 Jnz _ _ _ ⇒ None ? 871 MovSuccessor _ _ _ ⇒ None ? 861 872 Jmp (j:Identifier)⇒ 862 873 Some jump_length … … 991 1002 ] 992 1003 normalize nodelta cases instr in Hjump Heq1; 993 [1, 7: #pi normalize nodelta cases pi1004 [1,9: #pi normalize nodelta cases pi 994 1005 try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1) 995 1006 try (cases Hjump) lapply Heq1 Heq1 lapply Hjump Hjump lapply id id 996 2,3,6,8,9,12: #y [3,6: #id] normalize nodelta #abs cases abs 1007 2,3,8,10,11,16: #y [3,6: #id] normalize nodelta #abs cases abs 1008 5,6,13,14: #x #y #z #abs cases abs 997 1009 ] 998 1010 #id #Hjump normalize nodelta #Heq1 … … 1040 1052 #Holdeq >prf >nth_append_second [2: @le_n] <minus_n_n whd in match (nth ????); 1041 1053 >p1 cases instr in Hjump Heq1; 1042 [1, 7: #pi normalize nodelta cases pi1054 [1,9: #pi normalize nodelta cases pi 1043 1055 try (#y #id #Hjump #Heq1) try (#id #Hjump #Heq1) try (#Hjump #Heq1) 1044 1056 try (cases Hjump) lapply Heq1 Heq1 lapply Hjump Hjump lapply id id 1045 2,3,6,8,9,12: #y [3,6: #id] normalize nodelta #abs cases abs 1057 2,3,8,10,11,16: #y [3,6: #id] normalize nodelta #abs cases abs 1058 5,6,13,14: #x #y #z #abs cases abs 1046 1059 ] 1047 1060 #id #Hjump normalize nodelta <Hjump #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1))
Note: See TracChangeset
for help on using the changeset viewer.