 Timestamp:
 Jul 26, 2012, 10:43:55 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplitSplit.ma
r2264 r2266 37 37 <(vsplit_ok … (sym_eq … vsplit_v2_refl)) 38 38 >(eq_bv_eq … relevant) % 39 qed. 40 41 lemma ticks_of_instruction_AJMP: 42 ∀address. ticks_of_instruction (AJMP (ADDR11 address)) = 2. 43 try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ 44 @(bitvector_3_elim_prop … vl) % 45 qed. 46 47 lemma ticks_of_instruction_ACALL: 48 ∀address. ticks_of_instruction (ACALL (ADDR11 address)) = 2. 49 try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ 50 @(bitvector_3_elim_prop … vl) % 39 51 qed. 40 52 … … 144 156 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 145 157 whd in match (expand_pseudo_instruction ??????); 158 whd in match (ticks_of0 ??????); 146 159 inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta 147 160 inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta … … 165 178 >EQassembled in fetch_refl; #fetch_refl <fetch_refl 166 179 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 167 whd in ⊢ (??%%); 168 (* XXX: now we start to work on the mk_PreStatus equality *) 169 (* XXX: lhs *) 170 (* XXX: rhs *) 171 (* here we are *) 172 @split_eq_status try % /demod nohyps/ 173 [1,3,4: 174 change with (add ???) in match (\snd (half_add ???)); 175 whd in match execute_1_pseudo_instruction0; normalize nodelta 176 /demod nohyps/ >set_clock_set_program_counter 177 >program_counter_set_program_counter 178 whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta 179 lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl 180 normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm 181 [1: 182 >EQnewpc 183 inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta 184 @sym_eq 185 >EQlookup_labels in mjc_refl; #mjc_refl 186 @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl)) 187 >(andb_true_l … mj_possible_refl) @I 188 3: 189 >EQlookup_labels normalize nodelta % 190 5: 191 >EQnewpc 192 inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta 193 @sym_eq 180 change with (set_program_counter ???? = 181 status_of_pseudo_status ?? (set_program_counter ????) ??) 182 @set_program_counter_status_of_pseudo_status 183 [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try % 184 [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try % 185 @sigma_increment_commutation 186  @eq_f2 try % @ticks_of_instruction_AJMP ]] 187 whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels; 188 normalize nodelta 189 [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta 190 >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl 191 @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl)) 192 [2: >(andb_true_l … mj_possible_refl) % 193  <vsplit_refl @eq_f <EQnewpc % ] 194  >EQlookup_labels >create_label_cost_refl % 195  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta 196 >create_label_cost_refl 194 197 >EQlookup_labels in sjc_refl; #sjc_refl 195 198 >(pair_destruct_2 ????? (sym_eq … half_add_refl)) 196 @(short_jump_cond_ok ???? (sym_eq … sjc_refl))197 >(andb_true_l … sj_possible_refl) @I198 ]199 whd in is_well_labelled_witness;200 @(is_well_labelled_witness ? ppc ppc_in_bounds pi)201 try (>fetch_pseudo_refl %)202 >pi_refl %203 2:204 whd in ⊢ (??(?%%)%);205 cases (bitvector_11_cases address)206 * * * * * * #b4 * #b5207 * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl208 normalize in match (fetch ??); <plus_n_Sm @eq_f209 @commutative_plus199 >(short_jump_cond_ok ???? (sym_eq … sjc_refl)) 200 [2: >(andb_true_l … sj_possible_refl) % 201  >EQnewpc % ]] 202 5: (* Call *) 203 #arg1 #pi_refl 204 (* XXX: we first work on sigma_increment_commutation *) 205 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 206 whd in match (expand_pseudo_instruction ??????); 207 whd in match (ticks_of0 ??????); 208 inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta 209 inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta 210 [2: 211 inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta 212 inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta 210 213 ] 211 5: (* Call *) 214 #sigma_increment_commutation 215 normalize in sigma_increment_commutation:(???(???(??%))); 216 (* XXX: we work on the maps *) 217 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 218 (* XXX: we assume the fetch_many hypothesis *) 219 * #fetch_refl #fetch_many_assm 220 (* XXX: we give the existential *) 221 %{1} 222 (* XXX: work on the left hand side of the equality *) 223 whd in ⊢ (??%?); whd in match (program_counter ???); 224 (* XXX: execute fetches some more *) 225 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 226 whd in fetch_many_assm; 227 >EQassembled in fetch_refl; #fetch_refl <fetch_refl 228 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 229 change with (set_program_counter ???? = 230 status_of_pseudo_status ?? (set_program_counter ????) ??) 231 @set_program_counter_status_of_pseudo_status 232 [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try % 233 [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try % 234 @sigma_increment_commutation 235  @eq_f2 try % @ticks_of_instruction_AJMP ]] 236 whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels; 237 normalize nodelta 238 [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta 239 >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl 240 @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl)) 241 [2: >(andb_true_l … mj_possible_refl) % 242  <vsplit_refl @eq_f <EQnewpc % ] 243  >EQlookup_labels >create_label_cost_refl % 244  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta 245 >create_label_cost_refl 246 >EQlookup_labels in sjc_refl; #sjc_refl 247 >(pair_destruct_2 ????? (sym_eq … half_add_refl)) 248 >(short_jump_cond_ok ???? (sym_eq … sjc_refl)) 249 [2: >(andb_true_l … sj_possible_refl) % 250  >EQnewpc % ]] 251 252 253 254 255 256 257 258 259 260 261 262 212 263 #arg1 #pi_refl 213 264 (* XXX: we first work on sigma_increment_commutation *)
Note: See TracChangeset
for help on using the changeset viewer.