Changeset 2129 for src/ASM/AssemblyProofSplitSplit.ma
 Timestamp:
 Jun 27, 2012, 7:14:32 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplitSplit.ma
r2127 r2129 38 38 >(eq_bv_eq … relevant) % 39 39 qed. 40 40 41 41 theorem main_thm: 42 42 ∀M, M': internal_pseudo_address_map. 43 43 ∀program: pseudo_assembly_program. 44 ∀program_in_bounds: \snd program ≤ 2^16. 45 ∀addr_of: Identifier → PreStatus pseudo_assembly_program program → BitVector 16. 44 46 ∀is_well_labelled: is_well_labelled_p (\snd program). 45 47 ∀sigma: Word → Word. … … 48 50 ∀ps: PseudoStatus program. 49 51 ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < \snd program. 50 next_internal_pseudo_address_map M program ps program_counter_in_bounds = Some … M' →52 next_internal_pseudo_address_map M program addr_of ps program_counter_in_bounds = Some … M' → 51 53 ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) = 52 54 status_of_pseudo_status M' … 53 55 (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy. 54 #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps 55 letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds 56 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 57 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?; 58 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta 59 @pair_elim #assembled #costs' #assembly_refl normalize nodelta 60 lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled 61 @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta 62 @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels 63 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 64 whd in match execute_1_pseudo_instruction; normalize nodelta 65 whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta 66 lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc 67 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?) 68 [1: >fetch_pseudo_refl % 2: skip ] 69 #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3; 70 generalize in match assm1; assm1 assm2 assm3 71 normalize nodelta 72 inversion pi 73 [2,3: 74 #arg #_ 75 (* XXX: we first work on sigma_increment_commutation *) 76 #sigma_increment_commutation 77 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 78 (* XXX: we work on the maps *) 79 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 80 (* XXX: we assume the fetch_many hypothesis *) 81 #fetch_many_assm 82 (* XXX: we give the existential *) 83 %{0} 84 whd in match (execute_1_pseudo_instruction0 ?????); 85 (* XXX: work on the left hand side of the equality *) 86 whd in ⊢ (??%?); 87 @split_eq_status try % 88 /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) 89 6: (* Mov *) 90 #arg1 #arg2 #_ 91 (* XXX: we first work on sigma_increment_commutation *) 92 #sigma_increment_commutation 93 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 94 (* XXX: we work on the maps *) 95 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 96 (* XXX: we assume the fetch_many hypothesis *) 97 #fetch_many_assm 98 (* XXX: we give the existential *) 99 %{1} 100 whd in match (execute_1_pseudo_instruction0 ?????); 101 (* XXX: work on the left hand side of the equality *) 102 whd in ⊢ (??%?); whd in match (program_counter ???); 103 (* XXX: execute fetches some more *) 104 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 105 whd in fetch_many_assm; 106 >EQassembled in fetch_many_assm; 107 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * 108 #eq_instr 109 #fetch_many_assm whd in fetch_many_assm; 110 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 111 destruct whd in ⊢ (??%?); 112 (* XXX: now we start to work on the mk_PreStatus equality *) 113 (* XXX: lhs *) 114 change with (set_arg_16 ????? = ?) 115 >set_program_counter_mk_Status_commutation 116 >set_clock_mk_Status_commutation 117 >set_arg_16_mk_Status_commutation 118 (* XXX: rhs *) 119 change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%); 120 >set_program_counter_mk_Status_commutation 121 >set_clock_mk_Status_commutation 122 >set_arg_16_mk_Status_commutation in ⊢ (???%); 123 (* here we are *) 124 @split_eq_status try % 125 [1: 126 assumption 127 2: 128 @special_function_registers_8051_set_arg_16 % 129 ] 130 1: (* Instruction *) 131 #instr #_ #EQP #EQnext #fetch_many_assm 132 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness 133 ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels 134 EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …) 135 (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1))) 136 (refl …) ? (refl …)) 137 try assumption try % >assembly_refl assumption 138 4: (* Jmp *) 139 #arg1 #pi_refl 140 (* XXX: we first work on sigma_increment_commutation *) 141 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 142 whd in match (expand_pseudo_instruction ??????); 143 inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta 144 inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta 145 [2: 146 inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta 147 inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta 148 ] 149 #sigma_increment_commutation 150 normalize in sigma_increment_commutation:(???(???(??%))); 151 (* XXX: we work on the maps *) 152 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 153 (* XXX: we assume the fetch_many hypothesis *) 154 * #fetch_refl #fetch_many_assm 155 (* XXX: we give the existential *) 156 %{1} 157 (* XXX: work on the left hand side of the equality *) 158 whd in ⊢ (??%?); whd in match (program_counter ???); 159 (* XXX: execute fetches some more *) 160 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 161 whd in fetch_many_assm; 162 >EQassembled in fetch_refl; #fetch_refl <fetch_refl 163 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 164 whd in ⊢ (??%%); 165 (* XXX: now we start to work on the mk_PreStatus equality *) 166 (* XXX: lhs *) 167 (* XXX: rhs *) 168 (* here we are *) 169 @split_eq_status try % /demod nohyps/ 170 [1,3,4: 171 change with (add ???) in match (\snd (half_add ???)); 172 whd in match execute_1_pseudo_instruction0; normalize nodelta 173 /demod nohyps/ >set_clock_set_program_counter 174 >program_counter_set_program_counter 175 whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta 176 lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl 177 normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm 56 #M #M' * #preamble #instr_list #program_in_bounds #addr_of 57 #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps 58 letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds 59 change with (next_internal_pseudo_address_map0 ?????? = ? → ?) 60 generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?; 61 @pair_elim #labels #costs #create_label_cost_refl normalize nodelta 62 @pair_elim #assembled #costs' #assembly_refl normalize nodelta 63 lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled 64 @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta 65 @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels 66 @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels 67 whd in match execute_1_pseudo_instruction; normalize nodelta 68 whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta 69 lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc 70 lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?) 71 [1: >fetch_pseudo_refl % 2: skip 3: assumption ] 72 #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3; 73 generalize in match assm1; assm1 assm2 assm3 74 normalize nodelta 75 inversion pi 76 [(*2,3: 77 #arg #_ 78 (* XXX: we first work on sigma_increment_commutation *) 79 #sigma_increment_commutation 80 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 81 (* XXX: we work on the maps *) 82 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 83 (* XXX: we assume the fetch_many hypothesis *) 84 #fetch_many_assm 85 (* XXX: we give the existential *) 86 %{0} 87 whd in match (execute_1_pseudo_instruction0 ?????); 88 (* XXX: work on the left hand side of the equality *) 89 whd in ⊢ (??%?); 90 @split_eq_status try % 91 /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) 92 6: (* Mov *) 93 #arg1 #arg2 #_ 94 (* XXX: we first work on sigma_increment_commutation *) 95 #sigma_increment_commutation 96 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 97 (* XXX: we work on the maps *) 98 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 99 (* XXX: we assume the fetch_many hypothesis *) 100 #fetch_many_assm 101 (* XXX: we give the existential *) 102 %{1} 103 whd in match (execute_1_pseudo_instruction0 ?????); 104 (* XXX: work on the left hand side of the equality *) 105 whd in ⊢ (??%?); whd in match (program_counter ???); 106 (* XXX: execute fetches some more *) 107 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 108 whd in fetch_many_assm; 109 >EQassembled in fetch_many_assm; 110 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * 111 #eq_instr 112 #fetch_many_assm whd in fetch_many_assm; 113 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 114 destruct whd in ⊢ (??%?); 115 (* XXX: now we start to work on the mk_PreStatus equality *) 116 (* XXX: lhs *) 117 change with (set_arg_16 ????? = ?) 118 >set_program_counter_mk_Status_commutation 119 >set_clock_mk_Status_commutation 120 >set_arg_16_mk_Status_commutation 121 (* XXX: rhs *) 122 change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%); 123 >set_program_counter_mk_Status_commutation 124 >set_clock_mk_Status_commutation 125 >set_arg_16_mk_Status_commutation in ⊢ (???%); 126 (* here we are *) 127 @split_eq_status try % 178 128 [1: 179 >EQnewpc 180 inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta 181 @sym_eq >address_of_word_labels_assm 129 assumption 130 2: 131 @special_function_registers_8051_set_arg_16 % 132 ] 133 1: (* Instruction *) 134 #instr #_ #EQP #EQnext #fetch_many_assm 135 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness 136 ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels 137 EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …) 138 (λx:Identifier. λy:PreStatus pseudo_assembly_program 〈preamble, instr_list〉. address_of_word_labels 〈preamble, instr_list〉 x) (refl …) (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1))) 139 (refl …) ? (refl …)) 140 try assumption try % >assembly_refl assumption 141 4: (* Jmp *) 142 #arg1 #pi_refl 143 (* XXX: we first work on sigma_increment_commutation *) 144 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 145 whd in match (expand_pseudo_instruction ??????); 146 inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta 147 inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta 148 [2: 149 inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta 150 inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta 151 ] 152 #sigma_increment_commutation 153 normalize in sigma_increment_commutation:(???(???(??%))); 154 (* XXX: we work on the maps *) 155 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 156 (* XXX: we assume the fetch_many hypothesis *) 157 * #fetch_refl #fetch_many_assm 158 (* XXX: we give the existential *) 159 %{1} 160 (* XXX: work on the left hand side of the equality *) 161 whd in ⊢ (??%?); whd in match (program_counter ???); 162 (* XXX: execute fetches some more *) 163 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 164 whd in fetch_many_assm; 165 >EQassembled in fetch_refl; #fetch_refl <fetch_refl 166 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 182 181 [1: 183 >EQlookup_labels in mjc_refl; #mjc_refl 184 @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl)) 185 >(andb_true_l … mj_possible_refl) @I 182 >EQnewpc 183 inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta 184 @sym_eq >address_of_word_labels_assm 185 [1: 186 >EQlookup_labels in mjc_refl; #mjc_refl 187 @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl)) 188 >(andb_true_l … mj_possible_refl) @I 189 ] 190 3: 191 >EQlookup_labels normalize nodelta 192 >address_of_word_labels_assm try % 193 5: 194 >EQnewpc 195 inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta 196 @sym_eq >address_of_word_labels_assm 197 [1: 198 >EQlookup_labels in sjc_refl; #sjc_refl 199 >(pair_destruct_2 ????? (sym_eq … half_add_refl)) 200 @(short_jump_cond_ok ???? (sym_eq … sjc_refl)) 201 >(andb_true_l … sj_possible_refl) @I 202 ] 186 203 ] 187 3: 188 >EQlookup_labels normalize nodelta 189 >address_of_word_labels_assm try % 190 5: 191 >EQnewpc 192 inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta 193 @sym_eq >address_of_word_labels_assm 194 [1: 195 >EQlookup_labels in sjc_refl; #sjc_refl 196 >(pair_destruct_2 ????? (sym_eq … half_add_refl)) 197 @(short_jump_cond_ok ???? (sym_eq … sjc_refl)) 198 >(andb_true_l … sj_possible_refl) @I 204 @(is_well_labelled_witness … fetch_pseudo_refl) 205 >pi_refl % 206 2: 207 whd in ⊢ (??(?%%)%); 208 cases (bitvector_11_cases address) 209 * * * * * * #b4 * #b5 210 * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl 211 normalize in match (fetch ??); <plus_n_Sm @eq_f 212 @commutative_plus 213 ] 214 *)5: (* Call *) 215 #arg1 #pi_refl 216 (* XXX: we first work on sigma_increment_commutation *) 217 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 218 whd in match (expand_pseudo_instruction ??????); 219 whd in match (execute_1_pseudo_instruction0 ?????); 220 inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta 221 inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta 222 @pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) carry_new_sp_refl #carry_new_sp_refl 223 @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) pc_bu_bl_refl #pc_bu_bl_refl 224 @pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') carry_new_sp_refl' #carry_new_sp_refl' 225 #sigma_increment_commutation 226 normalize in sigma_increment_commutation:(???(???(??%))); 227 (* XXX: we work on the maps *) 228 whd in ⊢ (??%? → ?); 229 @pair_elim #callM #accM #Mrefl 230 @Some_Some_elim #map_refl_assm <map_refl_assm 231 (* XXX: we assume the fetch_many hypothesis *) 232 * #fetch_refl #fetch_many_assm 233 (* XXX: we give the existential *) 234 %{1} 235 (* XXX: work on the left hand side of the equality *) 236 whd in ⊢ (??%?); whd in match (program_counter ???); 237 (* XXX: execute fetches some more *) 238 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 239 whd in fetch_many_assm; 240 >EQassembled in fetch_refl; #fetch_refl <fetch_refl 241 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 242 whd in ⊢ (??(???%)?); normalize in match (length ? (assembly1 …)); 243 normalize in match (length ? (assembly1 …)) in EQnewpc; 244 normalize nodelta 245 [1: 246 @(pair_replace ????? carry new_sp ??? carry_new_sp_refl) 247 try /demod nohyps/ [1: %] 248 @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl' 249 @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl') 250 try /demod nohyps/ [1: %] 251 @pair_elim #thr #eig #thr_eig_refl 252 @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%); 253 @split_eq_status try /demod nohyps/ try % 254 [1,2: 255 (* XXX: need the commented out axioms from AssemblyProof.ma *) 256 cases daemon 257 3: 258 >program_counter_set_program_counter 259 whd in ajc_refl:(??%?); lapply ajc_refl ajc_refl map_refl_assm Mrefl 260 >EQlookup_labels normalize nodelta 261 @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl normalize nodelta 262 <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta 263 #relevant >fst_5_rest_refl 264 check absolute_jump_cond 265 <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) 266 lapply pc_bu_bl_refl' pc_bu_bl_refl' 267 >program_counter_set_8051_sfr >set_clock_set_program_counter 268 >program_counter_set_program_counter >fst_5_rest_pc_refl 269 cut(fst_5_addr = fst_5_pc) 270 [1: 271 cases daemon (* XXX: !! *) 272 2: 273 #relevant2 >relevant2 274 <(vsplit_ok ?????? (sym_eq … fiv_thr_refl')) 275 #relevant3 276 lapply(vsplit_ok ?????? (sym_eq … relevant3)) 277 >(vector_associative_append bool 5 3 8) #relevant4 278 cut(fiv = fst_5_pc ∧ thr'@@pc_bl' = rest_pc) 279 [1: 280 cases daemon (* XXX: !! *) 281 2: 282 * #relevant5 #relevant6 >relevant5 283 >(vector_associative_append bool 5 3 8) @eq_f 284 destruct(relevant) 285 <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f 286 ] 287 ] 288 4: 289 >set_program_counter_mk_Status_commutation in ⊢ (???%); 290 >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%); 291 (* XXX: require set_8051_sfr_write_at_stack_pointer and 292 special_function_registers_8051_set_8051_sfr 293 *) 294 cases daemon 295 5,6,7: 296 >set_program_counter_mk_Status_commutation in ⊢ (???%); 297 (* XXX: similar to above but for 8052 298 *) 299 cases daemon 300 8: 301 whd in match (ticks_of_instruction ?); 302 cut(\snd (fetch (load_code_memory (assembly1 (ACALL (ADDR11 offset)))) (zero 16)) = 2) 303 [1: // 304 2: 305 normalize in match (assembly1 ?); >thr_eig_refl 306 @(bitvector_3_elim_prop … thr) % 307 3: 308 #fetch_2_refl >fetch_2_refl >commutative_plus % 309 ] 310 2: 199 311 ] 200 ]201 @(is_well_labelled_witness … 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_plus210 ]211 5: (* Call *)212 #arg1 #_213 (* XXX: we first work on sigma_increment_commutation *)214 #sigma_increment_commutation215 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;216 (* XXX: we work on the maps *)217 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm218 (* XXX: we assume the fetch_many hypothesis *)219 #fetch_many_assm220 (* XXX: we give the existential *)221 %{1}222 whd in match (execute_1_pseudo_instruction0 ?????);223 (* XXX: work on the left hand side of the equality *)224 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc225 (* XXX: execute fetches some more *)226 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta227 whd in fetch_many_assm;228 >EQassembled in fetch_many_assm;229 cases (fetch ??) * #instr #newpc #?ticks normalize nodelta *230 #eq_instr231 #fetch_many_assm whd in fetch_many_assm;232 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc233 destruct whd in ⊢ (??%?);234 (* XXX: now we start to work on the mk_PreStatus equality *)235 (* XXX: lhs *)236 change with (set_arg_16 ????? = ?)237 >set_program_counter_mk_Status_commutation238 >set_clock_mk_Status_commutation239 >set_arg_16_mk_Status_commutation240 (* XXX: rhs *)241 change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);242 >set_program_counter_mk_Status_commutation243 >set_clock_mk_Status_commutation244 >set_arg_16_mk_Status_commutation in ⊢ (???%);245 (* here we are *)246 @split_eq_status //247 [1:248 assumption249 2:250 @special_function_registers_8051_set_arg_16251 [2: %252 1: //253 312 ] 254 313 ]
Note: See TracChangeset
for help on using the changeset viewer.