Changeset 2018


Ignore:
Timestamp:
Jun 5, 2012, 5:49:09 PM (5 years ago)
Author:
mulligan
Message:

CJNE case a complete mess.

Location:
src/ASM
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2017 r2018  
    860860  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
    861861  whd in match execute_1_preinstruction; normalize nodelta
    862   [4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
     862  [30: (* CJNE *)
     863  (* XXX: work on the right hand side *)
     864  cases addr1 -addr1 #addr1 normalize nodelta
     865  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
     866  (* XXX: switch to the left hand side *)
     867  >EQP -P normalize nodelta
     868  #sigma_increment_commutation #maps_assm #fetch_many_assm
     869
     870  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     871  whd in match (expand_relative_jump ????);
     872  <EQppc in fetch_many_assm;
     873  @pair_elim #result #flags #sub16_refl
     874  @pair_elim #upper #lower #split_refl
     875  inversion (eq_bv ???) #upper_split_refl normalize nodelta
     876  [1,3:
     877    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     878    whd in ⊢ (??%?);
     879    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     880    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
     881    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
     882    @(if_then_else_replace ???????? eq_bv_refl)
     883    [1,3,5,7:
     884      cases daemon
     885    |2,4,6,8:
     886      (* XXX: switch to the right hand side *)
     887      normalize nodelta >EQs -s >EQticks -ticks
     888      whd in ⊢ (??%%);
     889      (* XXX: finally, prove the equality using sigma commutation *)
     890      @split_eq_status try %
     891      [3,7,11,15:
     892        whd in ⊢ (??%?);
     893        [1,3:
     894          cases daemon
     895        |2,4:
     896          cases daemon
     897        ]
     898      ]
     899      cases daemon (* XXX *)
     900    ]
     901  |2,4:
     902    >EQppc
     903    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     904    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     905    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     906    #fetch_many_assm whd in fetch_many_assm; %{2}
     907    change with (execute_1 ?? = ?)
     908    @(pose … (execute_1 ? (status_of_pseudo_status …)))
     909    #status_after_1 #EQstatus_after_1
     910    <(?: ? = status_after_1)
     911    [3,6:
     912      >EQstatus_after_1 in ⊢ (???%);
     913      whd in ⊢ (???%);
     914      [1: <fetch_refl in ⊢ (???%);
     915      |2: <fetch_refl in ⊢ (???%);
     916      ]
     917      whd in ⊢ (???%);
     918      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
     919      whd in ⊢ (???%);
     920      whd in match (addr_of_relative ????);
     921      change with (add ???) in match (\snd (half_add ???));
     922      >set_clock_set_program_counter in ⊢ (???%);
     923      >program_counter_set_program_counter in ⊢ (???%);
     924      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
     925      [2,4,6,8:
     926        >bitvector_of_nat_sign_extension_equivalence
     927        [1,3,5,7:
     928          >EQintermediate_pc' %
     929        |*:
     930          repeat @le_S_S @le_O_n
     931        ]
     932      ]
     933      [1,3: % ]
     934    ]
     935  ]
     936  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
     937  (* XXX: work on the right hand side *)
     938  >p normalize nodelta
     939  (* XXX: switch to the left hand side *)
     940  -instr_refl >EQP -P normalize nodelta
     941  #sigma_increment_commutation #maps_assm #fetch_many_assm
     942 
     943  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
     944  whd in match (expand_relative_jump ????);
     945  <EQppc in fetch_many_assm;
     946  @pair_elim #result #flags #sub16_refl
     947  @pair_elim #upper #lower #split_refl
     948  cases (eq_bv ???) normalize nodelta
     949  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     950    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
     951    whd in ⊢ (??%?);
     952    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
     953    (* XXX: work on the left hand side *)
     954    @(if_then_else_replace ???????? p) normalize nodelta
     955    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     956      cases daemon
     957    ]
     958    (* XXX: switch to the right hand side *)
     959    normalize nodelta >EQs -s >EQticks -ticks
     960    whd in ⊢ (??%%);
     961    (* XXX: finally, prove the equality using sigma commutation *)
     962    @split_eq_status try %
     963    cases daemon
     964  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     965    >EQppc
     966    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
     967    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
     968    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
     969    #fetch_many_assm whd in fetch_many_assm; %{2}
     970    change with (execute_1 ?? = ?)
     971    @(pose … (execute_1 ? (status_of_pseudo_status …)))
     972    #status_after_1 #EQstatus_after_1
     973    <(?: ? = status_after_1)
     974    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
     975      >EQstatus_after_1 in ⊢ (???%);
     976      whd in ⊢ (???%);
     977      [1: <fetch_refl in ⊢ (???%);
     978      |2: <fetch_refl in ⊢ (???%);
     979      |3: <fetch_refl in ⊢ (???%);
     980      |4: <fetch_refl in ⊢ (???%);
     981      |5: <fetch_refl in ⊢ (???%);
     982      |6: <fetch_refl in ⊢ (???%);
     983      |7: <fetch_refl in ⊢ (???%);
     984      |8: <fetch_refl in ⊢ (???%);
     985      |9: <fetch_refl in ⊢ (???%);
     986      |10: <fetch_refl in ⊢ (???%);
     987      |11: <fetch_refl in ⊢ (???%);
     988      |12: <fetch_refl in ⊢ (???%);
     989      |13: <fetch_refl in ⊢ (???%);
     990      |14: <fetch_refl in ⊢ (???%);
     991      ]
     992      whd in ⊢ (???%);
     993      @(if_then_else_replace ???????? p)
     994      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     995        cases daemon
     996      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     997        normalize nodelta
     998        whd in match (addr_of_relative ????);
     999        >set_clock_mk_Status_commutation
     1000        [9,10:
     1001          (* XXX: demodulation not working in this case *)
     1002          >program_counter_set_arg_1 in ⊢ (???%);
     1003          >program_counter_set_program_counter in ⊢ (???%);
     1004        |*:
     1005          /demod/
     1006        ]
     1007        whd in ⊢ (???%);
     1008        change with (add ???) in match (\snd (half_add ???));
     1009        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
     1010        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
     1011          >bitvector_of_nat_sign_extension_equivalence
     1012          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
     1013            >EQintermediate_pc' %
     1014          |*:
     1015            repeat @le_S_S @le_O_n
     1016          ]
     1017        ]
     1018        %
     1019      ]
     1020    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
     1021      skip
     1022    ]
     1023    -status_after_1
     1024    @(pose … (execute_1 ? (mk_PreStatus …)))
     1025    #status_after_1 #EQstatus_after_1
     1026    <(?: ? = status_after_1)
     1027    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
     1028      >EQstatus_after_1 in ⊢ (???%);
     1029      whd in ⊢ (???%);
     1030      (* XXX: matita bug with patterns across multiple goals *)
     1031      [1: <fetch_refl'' in ⊢ (???%);
     1032      |2: <fetch_refl' in ⊢ (???%);
     1033      |3: <fetch_refl'' in ⊢ (???%);
     1034      |4: <fetch_refl' in ⊢ (???%);
     1035      |5: <fetch_refl'' in ⊢ (???%);
     1036      |6: <fetch_refl' in ⊢ (???%);
     1037      |7: <fetch_refl'' in ⊢ (???%);
     1038      |8: <fetch_refl' in ⊢ (???%);
     1039      |9: <fetch_refl'' in ⊢ (???%);
     1040      |10: <fetch_refl' in ⊢ (???%);
     1041      |11: <fetch_refl'' in ⊢ (???%);
     1042      |12: <fetch_refl' in ⊢ (???%);
     1043      |13: <fetch_refl'' in ⊢ (???%);
     1044      |14: <fetch_refl' in ⊢ (???%);
     1045      ]
     1046      whd in ⊢ (???%);
     1047      [9,10:
     1048      |*:
     1049        /demod/
     1050      ] %
     1051    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
     1052      skip
     1053    ]
     1054    -status_after_1 whd in ⊢ (??%?);
     1055    (* XXX: switch to the right hand side *)
     1056    normalize nodelta >EQs -s >EQticks -ticks
     1057    whd in ⊢ (??%%);
     1058    (* XXX: finally, prove the equality using sigma commutation *)
     1059    @split_eq_status try %
     1060    [3,11,19,27,36,53,61:
     1061      >program_counter_set_program_counter >set_clock_mk_Status_commutation
     1062      [5: >program_counter_set_program_counter ]
     1063      >EQaddr_of normalize nodelta
     1064      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
     1065      >EQcm %
     1066    |7,15,23,31,45,57,65:
     1067      >set_clock_mk_Status_commutation >program_counter_set_program_counter
     1068      whd in ⊢ (??%?); normalize nodelta
     1069      >EQppc in fetch_many_assm; #fetch_many_assm
     1070      [5:
     1071        >program_counter_set_arg_1 >program_counter_set_program_counter
     1072      ]
     1073      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
     1074      <bitvector_of_nat_sign_extension_equivalence
     1075      [1,3,5,7,9,11,13:
     1076        whd in ⊢ (???%); cases (half_add ???) normalize //
     1077      |2,4,6,8,10,12,14:
     1078        @assembly1_lt_128
     1079        @le_S_S @le_O_n
     1080      ]
     1081    |*:
     1082      cases daemon
     1083    ]
     1084  ]
     1085  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
    8631086  (* XXX: work on the right hand side *)
    8641087  lapply (subaddressing_modein ???)
     
    10581281  (* XXX: finally, prove the equality using sigma commutation *)
    10591282  cases daemon
    1060   |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
    1061   (* XXX: work on the right hand side *)
    1062   >p normalize nodelta
    1063   (* XXX: switch to the left hand side *)
    1064   -instr_refl >EQP -P normalize nodelta
    1065   #sigma_increment_commutation #maps_assm #fetch_many_assm
    1066  
    1067   whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    1068   whd in match (expand_relative_jump ????);
    1069   <EQppc in fetch_many_assm;
    1070   @pair_elim #result #flags #sub16_refl
    1071   @pair_elim #upper #lower #split_refl
    1072   cases (eq_bv ???) normalize nodelta
    1073   [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1074     >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    1075     whd in ⊢ (??%?);
    1076     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    1077     (* XXX: work on the left hand side *)
    1078     @(if_then_else_replace ???????? p) normalize nodelta
    1079     [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1080       cases daemon
    1081     ]
    1082     (* XXX: switch to the right hand side *)
    1083     normalize nodelta >EQs -s >EQticks -ticks
    1084     whd in ⊢ (??%%);
    1085     (* XXX: finally, prove the equality using sigma commutation *)
    1086     @split_eq_status try %
    1087     cases daemon
    1088   |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1089     >EQppc
    1090     * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    1091     * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    1092     * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    1093     #fetch_many_assm whd in fetch_many_assm; %{2}
    1094     change with (execute_1 ?? = ?)
    1095     @(pose … (execute_1 ? (status_of_pseudo_status …)))
    1096     #status_after_1 #EQstatus_after_1
    1097     <(?: ? = status_after_1)
    1098     [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
    1099       >EQstatus_after_1 in ⊢ (???%);
    1100       whd in ⊢ (???%);
    1101       [1: <fetch_refl in ⊢ (???%);
    1102       |2: <fetch_refl in ⊢ (???%);
    1103       |3: <fetch_refl in ⊢ (???%);
    1104       |4: <fetch_refl in ⊢ (???%);
    1105       |5: <fetch_refl in ⊢ (???%);
    1106       |6: <fetch_refl in ⊢ (???%);
    1107       |7: <fetch_refl in ⊢ (???%);
    1108       |8: <fetch_refl in ⊢ (???%);
    1109       |9: <fetch_refl in ⊢ (???%);
    1110       |10: <fetch_refl in ⊢ (???%);
    1111       |11: <fetch_refl in ⊢ (???%);
    1112       |12: <fetch_refl in ⊢ (???%);
    1113       |13: <fetch_refl in ⊢ (???%);
    1114       |14: <fetch_refl in ⊢ (???%);
    1115       ]
    1116       whd in ⊢ (???%);
    1117       @(if_then_else_replace ???????? p)
    1118       [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1119         cases daemon
    1120       |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1121         normalize nodelta
    1122         whd in match (addr_of_relative ????);
    1123         >set_clock_mk_Status_commutation
    1124         [9,10:
    1125           (* XXX: demodulation not working in this case *)
    1126           >program_counter_set_arg_1 in ⊢ (???%);
    1127           >program_counter_set_program_counter in ⊢ (???%);
    1128         |*:
    1129           /demod/
    1130         ]
    1131         whd in ⊢ (???%);
    1132         change with (add ???) in match (\snd (half_add ???));
    1133         >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    1134         [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1135           >bitvector_of_nat_sign_extension_equivalence
    1136           [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1137             >EQintermediate_pc' %
    1138           |*:
    1139             repeat @le_S_S @le_O_n
    1140           ]
    1141         ]
    1142         %
    1143       ]
    1144     |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
    1145       skip
    1146     ]
    1147     -status_after_1
    1148     @(pose … (execute_1 ? (mk_PreStatus …)))
    1149     #status_after_1 #EQstatus_after_1
    1150     <(?: ? = status_after_1)
    1151     [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
    1152       >EQstatus_after_1 in ⊢ (???%);
    1153       whd in ⊢ (???%);
    1154       (* XXX: matita bug with patterns across multiple goals *)
    1155       [1: <fetch_refl'' in ⊢ (???%);
    1156       |2: <fetch_refl' in ⊢ (???%);
    1157       |3: <fetch_refl'' in ⊢ (???%);
    1158       |4: <fetch_refl' in ⊢ (???%);
    1159       |5: <fetch_refl'' in ⊢ (???%);
    1160       |6: <fetch_refl' in ⊢ (???%);
    1161       |7: <fetch_refl'' in ⊢ (???%);
    1162       |8: <fetch_refl' in ⊢ (???%);
    1163       |9: <fetch_refl'' in ⊢ (???%);
    1164       |10: <fetch_refl' in ⊢ (???%);
    1165       |11: <fetch_refl'' in ⊢ (???%);
    1166       |12: <fetch_refl' in ⊢ (???%);
    1167       |13: <fetch_refl'' in ⊢ (???%);
    1168       |14: <fetch_refl' in ⊢ (???%);
    1169       ]
    1170       whd in ⊢ (???%);
    1171       [9,10:
    1172       |*:
    1173         /demod/
    1174       ] %
    1175     |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
    1176       skip
    1177     ]
    1178     -status_after_1 whd in ⊢ (??%?);
    1179     (* XXX: switch to the right hand side *)
    1180     normalize nodelta >EQs -s >EQticks -ticks
    1181     whd in ⊢ (??%%);
    1182     (* XXX: finally, prove the equality using sigma commutation *)
    1183     @split_eq_status try %
    1184     [3,11,19,27,36,53,61:
    1185       >program_counter_set_program_counter >set_clock_mk_Status_commutation
    1186       [5: >program_counter_set_program_counter ]
    1187       >EQaddr_of normalize nodelta
    1188       whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
    1189       >EQcm %
    1190     |7,15,23,31,45,57,65:
    1191       >set_clock_mk_Status_commutation >program_counter_set_program_counter
    1192       whd in ⊢ (??%?); normalize nodelta
    1193       >EQppc in fetch_many_assm; #fetch_many_assm
    1194       [5:
    1195         >program_counter_set_arg_1 >program_counter_set_program_counter
    1196       ]
    1197       <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
    1198       <bitvector_of_nat_sign_extension_equivalence
    1199       [1,3,5,7,9,11,13:
    1200         whd in ⊢ (???%); cases (half_add ???) normalize //
    1201       |2,4,6,8,10,12,14:
    1202         @assembly1_lt_128
    1203         @le_S_S @le_O_n
    1204       ]
    1205     |*:
    1206       cases daemon
    1207     ]
    1208   ]
    1209   |30: (* CJNE *)
    1210   cases addr1 * #addr1_l #addr1_r normalize nodelta
    1211   (* XXX: work on the right hand side *)
    1212   (* XXX: switch to the left hand side *)
    1213   -instr_refl >EQP -P normalize nodelta
    1214   #sigma_increment_commutation #maps_assm #fetch_many_assm
    1215 
    1216   whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
    1217   whd in match (expand_relative_jump ????);
    1218   <EQppc in fetch_many_assm;
    1219   @pair_elim #result #flags #sub16_refl
    1220   @pair_elim #upper #lower #split_refl
    1221   cases (eq_bv ???) normalize nodelta
    1222   [1,3:
    1223     >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
    1224     whd in ⊢ (??%?);
    1225     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    1226     (* XXX: work on the left hand side *)
    1227     inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
    1228     lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
    1229     @(if_then_else_replace ???????? eq_bv_refl)
    1230     [1,3,5,7:
    1231       cases daemon
    1232     |*:
    1233       (* XXX: switch to the right hand side *)
    1234       normalize nodelta >EQs -s >EQticks -ticks
    1235       whd in ⊢ (??%%);
    1236       (* XXX: finally, prove the equality using sigma commutation *)
    1237       @split_eq_status try %
    1238       cases daemon
    1239     ]
    1240   |2,4:
    1241     >EQppc
    1242     * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    1243     * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
    1244     * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
    1245     #fetch_many_assm whd in fetch_many_assm; %{2}
    1246     change with (execute_1 ?? = ?)
    1247     @(pose … (execute_1 ? (status_of_pseudo_status …)))
    1248     #status_after_1 #EQstatus_after_1
    1249     <(?: ? = status_after_1)
    1250     [3,6:
    1251       >EQstatus_after_1 in ⊢ (???%);
    1252       whd in ⊢ (???%);
    1253       [1:
    1254         <fetch_refl in ⊢ (???%);
    1255       |2:
    1256         <fetch_refl in ⊢ (???%);
    1257       ]
    1258       whd in ⊢ (???%);
    1259       cases (¬ eq_bv ???) normalize nodelta
    1260       whd in match (addr_of_relative ????);
    1261       >set_clock_mk_Status_commutation
    1262       whd in ⊢ (???%);
    1263         [9,10:
    1264           (* XXX: demodulation not working in this case *)
    1265           >program_counter_set_arg_1 in ⊢ (???%);
    1266           >program_counter_set_program_counter in ⊢ (???%);
    1267         |*:
    1268           /demod/
    1269         ]
    1270         whd in ⊢ (???%);
    1271         change with (add ???) in match (\snd (half_add ???));
    1272         >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
    1273         [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    1274           >bitvector_of_nat_sign_extension_equivalence
    1275           [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    1276             >EQintermediate_pc' %
    1277           |*:
    1278             repeat @le_S_S @le_O_n
    1279           ]
    1280         ]
    1281         %
    1282     ]
    1283      
    12841283  ]
    12851284]
  • src/ASM/Policy.ma

    r2008 r2018  
    341341    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd old_sigma) 〈0,short_jump〉)
    342342                    + added in
    343     if leb (addr - \fst inc_sigma) 126
     343    if leb (addr - \fst inc_sigma) 129
    344344    then short_jump
    345345    else long_jump
    346346  else
    347347    let addr ≝ \fst (bvt_lookup … (bitvector_of_nat 16 paddr) (\snd inc_sigma) 〈0,short_jump〉) in
    348     if leb (\fst inc_sigma - addr) 129
     348    if leb (\fst inc_sigma - addr) 125
    349349    then short_jump
    350350    else long_jump.
Note: See TracChangeset for help on using the changeset viewer.