Changeset 2278 for src/ASM/AssemblyProofSplit.ma
- Timestamp:
- Jul 30, 2012, 6:33:11 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2276 r2278 10 10 ∀i: instruction. 11 11 fetch_many code_memory final_pc start_pc [i] → 12 〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory 13 start_pc. 12 〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory start_pc. 14 13 #code_memory #final_pc #start_pc #i * #new_pc 15 14 #fetch_many_assm whd in fetch_many_assm; … … 68 67 #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status 69 68 try assumption % 69 qed. 70 71 lemma short_jump_cond_ok: 72 ∀v1, v1', v2, v2': Word. 73 ∀is_possible, offset. 74 v1 = v1' → v2 = v2' → 75 〈is_possible, offset〉 = short_jump_cond v1 v2 → 76 is_possible → v2' = add 16 v1' (sign_extension offset). 77 #v1 #v1' #v2 #v2' #is_possible #offset #v1_refl #v2_refl <v1_refl <v2_refl 78 whd in match short_jump_cond; normalize nodelta 79 @pair_elim #result #flags #sub16_refl 80 @pair_elim #upper #lower #vsplit_refl 81 inversion (get_index' bool ???) #get_index_refl normalize nodelta 82 #relevant destruct(relevant) #relevant 83 [1: 84 @(sub_16_to_add_16_8_1 … flags) 85 |2: 86 @(sub_16_to_add_16_8_0 … flags) 87 ] 88 try assumption >sub16_refl 89 <(eq_bv_eq … relevant) 90 >(vsplit_ok … (sym_eq … vsplit_refl)) % 70 91 qed. 71 92 … … 1139 1160 ] 1140 1161 ] 1141 | 12: (* JC *)1162 |*)12: (* JC *) 1142 1163 >EQP -P normalize nodelta 1164 whd in match assembly_1_pseudoinstruction; normalize nodelta 1143 1165 whd in match expand_pseudo_instruction; normalize nodelta 1144 1166 whd in match expand_relative_jump; normalize nodelta 1145 1167 whd in match expand_relative_jump_internal; normalize nodelta 1168 >EQppc in ⊢ (% → ?); 1146 1169 @pair_elim #sj_possible #disp #sj_possible_disp_refl 1147 1170 inversion sj_possible #sj_possible_refl normalize nodelta … … 1156 1179 >EQs >EQticks <instr_refl normalize nodelta 1157 1180 [1: 1158 @(get_cy_flag_status_of_pseudo_status M') % 1159 |2: 1160 @sym_eq @set_program_counter_status_of_pseudo_status 1161 [1: 1162 |2: 1163 @sym_eq @set_clock_status_of_pseudo_status try % 1181 @(get_cy_flag_status_of_pseudo_status 〈low, high, accA〉) % 1182 |2: 1183 @set_program_counter_status_of_pseudo_status 1184 [1: 1185 >EQaddr_of normalize nodelta 1186 whd in match addr_of_relative; normalize nodelta 1187 @(short_jump_cond_ok … sj_possible … (sym_eq ??? sj_possible_disp_refl)) 1188 [1: 1189 @sym_eq whd in ⊢ (??%?); >EQppc % 1190 |2: 1191 >EQlookup_labels % 1192 |3: 1193 >sj_possible_refl @I 1194 ] 1195 |2: 1196 @set_clock_status_of_pseudo_status try % 1164 1197 whd in match ticks_of0; normalize nodelta 1165 1198 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1166 1199 [1: 1167 @eq_f2 try % 1168 >sigma_increment_commutation 1169 lapply sigma_policy_witness whd in match sigma_policy_specification; normalize nodelta 1170 * #sigma_zero_assm #relevant cases (relevant ppc ?) 1171 [1: 1172 -relevant 1173 [2: 1174 >EQcm assumption 1175 |1: 1176 #relevant #_ <EQppc >relevant @eq_f @eq_f @eq_f 1177 >EQlookup_labels >EQcm >create_label_cost_refl @eq_f2 1178 ] 1179 |2: 1180 ] 1200 >EQppc % 1181 1201 |2: 1182 1202 >sj_possible_refl % … … 1184 1204 ] 1185 1205 |3: 1186 ] 1206 @set_clock_status_of_pseudo_status try % @eq_f2 try % 1207 whd in match ticks_of0; normalize nodelta 1208 @(pair_replace ?????????? (eq_to_jmeq … sj_possible_disp_refl)) 1209 [1: 1210 >EQppc % 1211 |2: 1212 >sj_possible_refl % 1213 ] 1214 ] 1215 |2: 1216 #sigma_increment_commutation #maps_assm 1217 whd in maps_assm:(??%?); lapply maps_assm @Some_Some_elim #Mrefl destruct(Mrefl) 1218 whd in ⊢ (% → ?); * #jc_fetch_refl * #sjmp_fetch_refl * #ljmp_fetch_refl 1219 whd in ⊢ (% → ?); #ppc_eq_bv_refl %{2} 1220 @(if_then_else_replace ???????? p) try % normalize nodelta 1221 change with (execute_1 ?? = ?) destruct 1222 whd in ⊢ (??%?); >EQs >EQticks <instr_refl 1223 change with (set_program_counter ???? = ?) 1187 1224 ] 1188 1225 cases daemon
Note: See TracChangeset
for help on using the changeset viewer.