Changeset 1969
 Timestamp:
 May 18, 2012, 6:14:01 PM (7 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1967 r1969 85 85 qed. 86 86 87 lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P. 88 #P #A #a #abs destruct 89 qed. 87 90 88 91 theorem main_thm: … … 157 160 >(eq_instruction_to_eq … eq_instr) instr whd in ⊢ (??%?); 158 161 (* XXX: now we start to work on the mk_PreStatus equality *) 162 (* XXX: lhs *) 159 163 change with (set_arg_16 ????? = ?) 160 164 >set_program_counter_mk_Status_commutation 161 165 >set_clock_mk_Status_commutation 162 166 >set_arg_16_mk_Status_commutation 163 167 (* XXX: rhs *) 164 168 change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??) 165 169 >set_program_counter_mk_Status_commutation 166 170 >set_clock_mk_Status_commutation 167 171 >set_arg_16_mk_Status_commutation in ⊢ (???%); 168 169 172 (* here we are *) 170 173 @split_eq_status // 171 174 [1: … … 177 180 ] 178 181 ] 182 1: (* Instruction *) pi; * 183 [1,2,3: (* ADD, ADDC, SUBB *) 184 @list_addressing_mode_tags_elim_prop try % whd 185 @list_addressing_mode_tags_elim_prop try % whd #arg 186 (* XXX: we first work on sigma_increment_commutation *) 187 #sigma_increment_commutation 188 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 189 (* XXX: we work on the maps *) 190 whd in ⊢ (??%? → ?); 191 try (change with (if ? then ? else ? = ? → ?) 192 cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta) 193 #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm 194 (* XXX: we assume the fetch_many hypothesis *) 195 #fetch_many_assm 196 (* XXX: we give the existential *) 197 %{1} 198 whd in match (execute_1_pseudo_instruction0 ?????); 199 (* XXX: work on the left hand side of the equality *) 200 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 201 (* XXX: execute fetches some more *) 202 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 203 whd in fetch_many_assm; 204 >EQassembled in fetch_many_assm; 205 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * * 206 #eq_instr #EQticks whd in EQticks:(???%); >EQticks 207 #fetch_many_assm whd in fetch_many_assm; 208 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 209 >(eq_instruction_to_eq … eq_instr) instr whd in ⊢ (??%?); 210 [ @(pose … (execute_1_preinstruction' ???????)) 211 #lhs whd in ⊢ (???% → ?); #EQlhs 212 @(pose … (execute_1_preinstruction' ???????)) 213 #rhs whd in ⊢ (???% → ?); #EQrhs 214 215 CSC: delirium 216 217 >EQlhs EQlhs >EQrhs EQrhs 218 cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%%); 219 220 lapply (refl ? (execute_1_preinstruction' ???????)); 221 [ whd in match (execute_1_preinstruction' ???????); 222 223 whd in ⊢ (??%?); 224 [ whd in ⊢ (??(???%)%); 225 whd in match (execute_1_preinstruction' ???????); 226 cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%?); 227 @pair_elim #result #flags #Heq1 228 whd in match execute_1_preinstruction'; normalize nodelta 229 (* XXX: now we start to work on the mk_PreStatus equality *) 230 whd in ⊢ (??%?); 231 232 233 234 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 235 (* XXX: we take up the hypotheses *) 236 #sigma_increment_commutation #next_map_assm #fetch_many_assm 237 (* XXX: we give the existential *) 238 %{1} 239 whd in match (execute_1_pseudo_instruction0 ?????); 240 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 241 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 242 (* XXX: fetching of the instruction *) 243 whd in fetch_many_assm; 244 >EQassembled in fetch_many_assm; 245 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * * 246 #eq_instr #EQticks whd in EQticks:(???%); >EQticks 247 #fetch_many_assm whd in fetch_many_assm; 248 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 249 >(eq_instruction_to_eq … eq_instr) instr 250 (* XXX: now we start to work on the mk_PreStatus equality *) 251 whd in ⊢ (??%?); 252 check execute_1_preinstruction 253 254 255 #MAP #H1 #H2 #EQ %[1,3,5:@1] 256 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 257 change in ⊢ (? → ??%?) with (execute_1_0 ??) 258 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 259 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 260 >H2b >(eq_instruction_to_eq … H2a) 261 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; MAP; 262 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; 263 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG2 264 normalize nodelta; #MAP; 265 [1: change in ⊢ (? → %) with 266 ((let 〈result,flags〉 ≝ 267 add_8_with_carry 268 (get_arg_8 ? ps false ACC_A) 269 (get_arg_8 ? 270 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps))) 271 false (DIRECT ARG2)) 272 ? in ?) = ?) 273 [2,3: %] 274 change in ⊢ (???% → ?) with 275 (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?) 276 >get_arg_8_set_clock 277 [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ? 278 [2,4: #abs @⊥ normalize in abs; destruct (abs) 279 *:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)] 280 [ change in ⊢ (? → %) with 281 ((let 〈result,flags〉 ≝ 282 add_8_with_carry 283 (get_arg_8 ? ps false ACC_A) 284 (get_arg_8 ? 285 (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps))) 286 false (DIRECT ARG2)) 287 ? in ?) = ?) 288 >get_arg_8_set_low_internal_ram 289 290 cases (add_8_with_carry ???) 291 292 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 293 #result #flags 294 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) % 295 179 296 180 297 4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?); … … 192 309 whd in ⊢ (??(match ?%? with [_ ⇒ ?])?) 193 310 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX % 194 6: (* Mov *) #arg1 #arg2195 #H1 #H2 #EQ %[@1]196 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)197 change in ⊢ (? → ??%?) with (execute_1_0 ??)198 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;199 * * #H2a #H2b whd in ⊢ (% → ?) #H2c200 >H2b >(eq_instruction_to_eq … H2a)201 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?);202 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; whd in ⊢ (???% → ??%?)203 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG2204 normalize nodelta;205 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)]206 #result #flags207 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) %208 311 5: (* Call *) #label #MAP 209 312 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP; 
src/ASM/Interpret.ma
r1964 r1969 882 882 program_counter. 883 883 884 definition addr_of_relative ≝ 885 λM,cm. λx:[[relative]]. λs: PreStatus M cm. 886 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 887 [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r) 888  _ ⇒ λabsd. ⊥ 889 ] (subaddressing_modein … x). 890 @absd 891 qed. 892 884 893 definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat. 885 894 Σs': Status cm. … … 894 903 match instr return λx. x = instr → Σs:?.? with 895 904 [ RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … 896 (λx. λs. 897 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 898 [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r) 899  _ ⇒ λabsd. ⊥ 900 ] (subaddressing_modein … x)) instr' s 905 (addr_of_relative … cm) instr' s 901 906  MOVC addr1 addr2 ⇒ λinstr_refl. 902 907 let s ≝ set_clock ?? s (ticks + clock … s) in … … 971 976 [1,2,3,4,5,6,7,8: 972 977 normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS % 973 try // (*CSC: Veeery slow*)978 try // 974 979 s destruct(INSTR_PC) <instr_refl whd 975 980 try (#absurd normalize in absurd; try destruct(absurd) try %) %
Note: See TracChangeset
for help on using the changeset viewer.