- Timestamp:
- Jun 27, 2012, 7:14:32 PM (7 years ago)
- Location:
- src/ASM
- Files:
-
- 4 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2128 r2129 64 64 let 〈instr, pc', ticks〉 ≝ fetch code_memory pc in 65 65 (eq_instruction instr i ∧ eqb ticks (ticks_of_instruction instr) ∧ eq_bv … pc' pc_plus_len) = true. 66 cases daemon 67 (* XXX: commented out as takes ages to typecheck 66 68 #pc #i #code_memory #assembled cases i [8: *] 67 69 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] … … 83 85 whd in match fetch; normalize nodelta <H1 whd in ⊢ (match % with [ _ ⇒ ? ]); 84 86 [17,18,19,20,21,22,23,24,25,26,32,34,35,36,37,39: <H3] 85 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl 87 try <H2 whd >eq_instruction_refl >H4 @eq_bv_refl *) 86 88 qed. 87 89 … … 936 938 ∀i: instruction. 937 939 |(assembly1 i)| < 128. 940 cases daemon 941 (* XXX: commented out as takes ages to type check 938 942 #i cases i 939 943 try (#assm1 #assm2) try #assm1 … … 1004 1008 @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n 1005 1009 ] 1006 qed. 1010 *) 1011 qed. -
src/ASM/AssemblyProofSplit.ma
r2124 r2129 400 400 status_of_pseudo_status M' cm s sigma policy). 401 401 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). 402 cases daemon (* XXX: commented out as it takes 45 minutes to typecheck *) 403 (* 402 404 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels 403 405 #costs #create_label_cost_refl #newppc … … 1371 1373 (* XXX: finally, prove the equality using sigma commutation *) 1372 1374 cases daemon 1373 ] 1374 qed. 1375 ] *) 1376 qed. -
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 ] -
src/ASM/Interpret.ma
r2124 r2129 1072 1072 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with 1073 1073 [ ADDR11 a ⇒ λaddr11: True. 1074 «let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1075 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1076 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in 1077 let s ≝ write_at_stack_pointer … s pc_bl in 1078 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1079 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1080 let s ≝ write_at_stack_pointer … s pc_bu in 1081 let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in 1082 let new_addr ≝ fiv @@ a in 1083 set_program_counter … s new_addr, ?» 1084 | _ ⇒ λother: False. ⊥ 1085 ] (subaddressing_modein … addr) 1086 | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s 1087 | LCALL addr ⇒ λinstr_refl. 1088 let s ≝ set_clock ?? s (ticks + clock … s) in 1089 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with 1090 [ ADDR16 a ⇒ λaddr16: True. 1091 « 1074 1092 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1075 1093 let s ≝ set_8051_sfr … s SFR_SP new_sp in … … 1079 1097 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1080 1098 let s ≝ write_at_stack_pointer … s pc_bu in 1081 let 〈thr, eig〉 ≝ vsplit ? 3 8 a in 1082 let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in 1083 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 1084 set_program_counter … s new_addr 1085 | _ ⇒ λother: False. ⊥ 1086 ] (subaddressing_modein … addr) 1087 | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s 1088 | LCALL addr ⇒ λinstr_refl. 1089 let s ≝ set_clock ?? s (ticks + clock … s) in 1090 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with 1091 [ ADDR16 a ⇒ λaddr16: True. 1092 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1093 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1094 let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in 1095 let s ≝ write_at_stack_pointer … s pc_bl in 1096 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 1097 let s ≝ set_8051_sfr … s SFR_SP new_sp in 1098 let s ≝ write_at_stack_pointer … s pc_bu in 1099 set_program_counter … s a 1099 set_program_counter … s a, ?» 1100 1100 | _ ⇒ λother: False. ⊥ 1101 1101 ] (subaddressing_modein … addr) … … 1106 1106 try // 1107 1107 -s destruct(INSTR_PC) <instr_refl whd 1108 try (#absurd normalize in absurd; try destruct(absurd) try %) % 1108 try (#absurd normalize in absurd; try destruct(absurd) try %) 1109 @pair_elim #carry #new_sp #carry_new_sp_refl 1110 @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl 1111 @pair_elim #carry' #new_sp' #carry_new_sp_refl' 1112 [2: 1113 /demod nohyps/ % 1114 |1: 1115 cases (vsplit ????) #thr #eig normalize nodelta 1116 cases (vsplit ????) #fiv #thr' normalize nodelta 1117 /demod by clock_set_program_counter/ /demod nohyps/ % 1118 ] 1109 1119 |9: 1110 1120 cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
Note: See TracChangeset
for help on using the changeset viewer.