Changeset 1971
 Timestamp:
 May 20, 2012, 10:34:31 PM (6 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1969 r1971 88 88 #P #A #a #abs destruct 89 89 qed. 90 91 (* 92 lemma pi1_let_commute: 93 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c. 94 pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t). 95 #A #B #C #P * #a #b * // 96 qed. 97 98 lemma pi1_let_as_commute: 99 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c. 100 pi1 … (let 〈x1,y1〉 as H ≝ c in t) = 101 (let 〈x1,y1〉 as H ≝ c in pi1 … t). 102 #A #B #C #P * #a #b * // 103 qed. 104 *) 105 106 lemma tech_pi1_let_as_commute: 107 ∀A,B,C,P. ∀f. ∀c,c':A × B. 108 ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c. 109 ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c. 110 c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) → 111 pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) = 112 f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)). 113 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/ 114 qed. 115 116 include alias "arithmetics/nat.ma". 117 include alias "basics/logic.ma". 118 include alias "ASM/BitVectorTrie.ma". 119 120 lemma pair_replace: 121 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c=c' → c ≃ 〈a,b〉 → 122 P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b'). 123 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct // 124 qed. 125 126 lemma main_lemma_preinstruction: 127 ∀M,M': internal_pseudo_address_map. 128 ∀preamble : preamble. ∀instr_list : list labelled_instruction. 129 ∀cm: pseudo_assembly_program. 130 ∀EQcm: cm = 〈preamble,instr_list〉. 131 ∀sigma : Word→Word. ∀policy : Word→bool. 132 ∀sigma_policy_witness : sigma_policy_specification cm sigma policy. 133 ∀ps : PseudoStatus cm. 134 ∀ppc : Word. 135 ∀EQppc : ppc=program_counter pseudo_assembly_program cm ps. 136 ∀labels : label_map. 137 ∀costs : BitVectorTrie costlabel 16. 138 ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉. 139 ∀assembled : list Byte. 140 ∀costs' : BitVectorTrie costlabel 16. 141 ∀assembly_refl : assembly 〈preamble,instr_list〉 sigma policy=〈assembled,costs'〉. 142 ∀EQassembled : assembled=\fst (assembly cm sigma policy). 143 ∀newppc : Word. 144 ∀lookup_labels : Identifier→Word. 145 ∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)). 146 ∀lookup_datalabels : identifier ASMTag→Word. 147 ∀ EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). 148 ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1). 149 ∀instr: preinstruction Identifier. 150 ∀ticks. 151 ∀EQticks: ticks = ticks_of0 〈preamble,instr_list〉 sigma policy ppc (Instruction instr). 152 ∀addr_of. 153 ∀EQaddr_of: addr_of = (λx:Identifier 154 .λy:PreStatus pseudo_assembly_program cm 155 .address_of_word_labels cm x). 156 ∀s. 157 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps 158 (add 16 ppc (bitvector_of_nat 16 1))). 159 ∀P. 160 ∀EQP: 161 P = (λs. ∃n:ℕ 162 .execute n 163 (code_memory_of_pseudo_assembly_program cm sigma 164 policy) 165 (status_of_pseudo_status M cm ps sigma policy) 166 =status_of_pseudo_status M' cm s sigma policy). 167 sigma (add 16 ppc (bitvector_of_nat 16 1)) 168 =add 16 (sigma ppc) 169 (bitvector_of_nat 16 170 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 171 lookup_datalabels (Instruction instr)))) 172 →next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) 173 M cm ps 174 =Some internal_pseudo_address_map M' 175 →fetch_many (load_code_memory assembled) 176 (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma ppc) 177 (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels 178 (Instruction instr)) 179 →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm 180 addr_of instr s). 181 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels 182 #costs #create_label_cost_refl #assembled #costs' #assembly_refl #EQassembled #newppc 183 #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr 184 #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP 185 #sigma_increment_commutation #maps_assm #fetch_many_assm 186 letin a ≝ Identifier letin m ≝ pseudo_assembly_program 187 cut (Σxxx:PseudoStatus cm. P (execute_1_preinstruction ticks a m cm addr_of instr s)) 188 [2: * // ] 189 @( 190 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 191 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 192 match instr in preinstruction return λx. x = instr → Σs'.? with 193 [ ADD addr1 addr2 ⇒ λinstr_refl. 194 let s ≝ add_ticks1 s in 195 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 196 (get_arg_8 … s false addr2) false in 197 let cy_flag ≝ get_index' ? O ? flags in 198 let ac_flag ≝ get_index' ? 1 ? flags in 199 let ov_flag ≝ get_index' ? 2 ? flags in 200 let s ≝ set_arg_8 … s ACC_A result in 201 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 202  ADDC addr1 addr2 ⇒ λinstr_refl. 203 let s ≝ add_ticks1 s in 204 let old_cy_flag ≝ get_cy_flag ?? s in 205 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 206 (get_arg_8 … s false addr2) old_cy_flag in 207 let cy_flag ≝ get_index' ? O ? flags in 208 let ac_flag ≝ get_index' ? 1 ? flags in 209 let ov_flag ≝ get_index' ? 2 ? flags in 210 let s ≝ set_arg_8 … s ACC_A result in 211 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 212  SUBB addr1 addr2 ⇒ λinstr_refl. 213 let s ≝ add_ticks1 s in 214 let old_cy_flag ≝ get_cy_flag ?? s in 215 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) 216 (get_arg_8 … s false addr2) old_cy_flag in 217 let cy_flag ≝ get_index' ? O ? flags in 218 let ac_flag ≝ get_index' ? 1 ? flags in 219 let ov_flag ≝ get_index' ? 2 ? flags in 220 let s ≝ set_arg_8 … s ACC_A result in 221 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 222  ANL addr ⇒ λinstr_refl. 223 let s ≝ add_ticks1 s in 224 match addr with 225 [ inl l ⇒ 226 match l with 227 [ inl l' ⇒ 228 let 〈addr1, addr2〉 ≝ l' in 229 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 230 set_arg_8 … s addr1 and_val 231  inr r ⇒ 232 let 〈addr1, addr2〉 ≝ r in 233 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 234 set_arg_8 … s addr1 and_val 235 ] 236  inr r ⇒ 237 let 〈addr1, addr2〉 ≝ r in 238 let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in 239 set_flags … s and_val (None ?) (get_ov_flag ?? s) 240 ] 241  ORL addr ⇒ λinstr_refl. 242 let s ≝ add_ticks1 s in 243 match addr with 244 [ inl l ⇒ 245 match l with 246 [ inl l' ⇒ 247 let 〈addr1, addr2〉 ≝ l' in 248 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 249 set_arg_8 … s addr1 or_val 250  inr r ⇒ 251 let 〈addr1, addr2〉 ≝ r in 252 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 253 set_arg_8 … s addr1 or_val 254 ] 255  inr r ⇒ 256 let 〈addr1, addr2〉 ≝ r in 257 let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in 258 set_flags … s or_val (None ?) (get_ov_flag … s) 259 ] 260  XRL addr ⇒ λinstr_refl. 261 let s ≝ add_ticks1 s in 262 match addr with 263 [ inl l' ⇒ 264 let 〈addr1, addr2〉 ≝ l' in 265 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 266 set_arg_8 … s addr1 xor_val 267  inr r ⇒ 268 let 〈addr1, addr2〉 ≝ r in 269 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 270 set_arg_8 … s addr1 xor_val 271 ] 272  INC addr ⇒ λinstr_refl. 273 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. ? with 274 [ ACC_A ⇒ λacc_a: True. 275 let s' ≝ add_ticks1 s in 276 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 277 set_arg_8 … s' ACC_A result 278  REGISTER r ⇒ λregister: True. 279 let s' ≝ add_ticks1 s in 280 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 281 set_arg_8 … s' (REGISTER r) result 282  DIRECT d ⇒ λdirect: True. 283 let s' ≝ add_ticks1 s in 284 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 285 set_arg_8 … s' (DIRECT d) result 286  INDIRECT i ⇒ λindirect: True. 287 let s' ≝ add_ticks1 s in 288 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 289 set_arg_8 … s' (INDIRECT i) result 290  DPTR ⇒ λdptr: True. 291 let s' ≝ add_ticks1 s in 292 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in 293 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in 294 let s ≝ set_8051_sfr … s' SFR_DPL bl in 295 set_8051_sfr … s' SFR_DPH bu 296  _ ⇒ λother: False. ⊥ 297 ] (subaddressing_modein … addr) 298  NOP ⇒ λinstr_refl. 299 let s ≝ add_ticks2 s in 300 s 301  DEC addr ⇒ λinstr_refl. 302 let s ≝ add_ticks1 s in 303 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in 304 set_arg_8 … s addr result 305  MUL addr1 addr2 ⇒ λinstr_refl. 306 let s ≝ add_ticks1 s in 307 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 308 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 309 let product ≝ acc_a_nat * acc_b_nat in 310 let ov_flag ≝ product ≥ 256 in 311 let low ≝ bitvector_of_nat 8 (product mod 256) in 312 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 313 let s ≝ set_8051_sfr … s SFR_ACC_A low in 314 set_8051_sfr … s SFR_ACC_B high 315  DIV addr1 addr2 ⇒ λinstr_refl. 316 let s ≝ add_ticks1 s in 317 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 318 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 319 match acc_b_nat with 320 [ O ⇒ set_flags … s false (None Bit) true 321  S o ⇒ 322 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 323 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 324 let s ≝ set_8051_sfr … s SFR_ACC_A q in 325 let s ≝ set_8051_sfr … s SFR_ACC_B r in 326 set_flags … s false (None Bit) false 327 ] 328  DA addr ⇒ λinstr_refl. 329 let s ≝ add_ticks1 s in 330 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in 331 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then 332 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in 333 let cy_flag ≝ get_index' ? O ? flags in 334 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in 335 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 336 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 337 let new_acc ≝ nu @@ acc_nl' in 338 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in 339 set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) 340 else 341 s 342 else 343 s 344  CLR addr ⇒ λinstr_refl. 345 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with 346 [ ACC_A ⇒ λacc_a: True. 347 let s ≝ add_ticks1 s in 348 set_arg_8 … s ACC_A (zero 8) 349  CARRY ⇒ λcarry: True. 350 let s ≝ add_ticks1 s in 351 set_arg_1 … s CARRY false 352  BIT_ADDR b ⇒ λbit_addr: True. 353 let s ≝ add_ticks1 s in 354 set_arg_1 … s (BIT_ADDR b) false 355  _ ⇒ λother: False. ⊥ 356 ] (subaddressing_modein … addr) 357  CPL addr ⇒ λinstr_refl. 358 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. ? with 359 [ ACC_A ⇒ λacc_a: True. 360 let s ≝ add_ticks1 s in 361 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 362 let new_acc ≝ negation_bv ? old_acc in 363 set_8051_sfr … s SFR_ACC_A new_acc 364  CARRY ⇒ λcarry: True. 365 let s ≝ add_ticks1 s in 366 let old_cy_flag ≝ get_arg_1 … s CARRY true in 367 let new_cy_flag ≝ ¬old_cy_flag in 368 set_arg_1 … s CARRY new_cy_flag 369  BIT_ADDR b ⇒ λbit_addr: True. 370 let s ≝ add_ticks1 s in 371 let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in 372 let new_bit ≝ ¬old_bit in 373 set_arg_1 … s (BIT_ADDR b) new_bit 374  _ ⇒ λother: False. ? 375 ] (subaddressing_modein … addr) 376  SETB b ⇒ λinstr_refl. 377 let s ≝ add_ticks1 s in 378 set_arg_1 … s b false 379  RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 380 let s ≝ add_ticks1 s in 381 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 382 let new_acc ≝ rotate_left … 1 old_acc in 383 set_8051_sfr … s SFR_ACC_A new_acc 384  RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 385 let s ≝ add_ticks1 s in 386 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 387 let new_acc ≝ rotate_right … 1 old_acc in 388 set_8051_sfr … s SFR_ACC_A new_acc 389  RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 390 let s ≝ add_ticks1 s in 391 let old_cy_flag ≝ get_cy_flag ?? s in 392 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 393 let new_cy_flag ≝ get_index' ? O ? old_acc in 394 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 395 let s ≝ set_arg_1 … s CARRY new_cy_flag in 396 set_8051_sfr … s SFR_ACC_A new_acc 397  RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 398 let s ≝ add_ticks1 s in 399 let old_cy_flag ≝ get_cy_flag ?? s in 400 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 401 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 402 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 403 let s ≝ set_arg_1 … s CARRY new_cy_flag in 404 set_8051_sfr … s SFR_ACC_A new_acc 405  SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 406 let s ≝ add_ticks1 s in 407 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 408 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 409 let new_acc ≝ nl @@ nu in 410 set_8051_sfr … s SFR_ACC_A new_acc 411  PUSH addr ⇒ λinstr_refl. 412 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. ? with 413 [ DIRECT d ⇒ λdirect: True. 414 let s ≝ add_ticks1 s in 415 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 416 let s ≝ set_8051_sfr … s SFR_SP new_sp in 417 write_at_stack_pointer … s d 418  _ ⇒ λother: False. ⊥ 419 ] (subaddressing_modein … addr) 420  POP addr ⇒ λinstr_refl. 421 let s ≝ add_ticks1 s in 422 let contents ≝ read_at_stack_pointer ?? s in 423 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 424 let s ≝ set_8051_sfr … s SFR_SP new_sp in 425 set_arg_8 … s addr contents 426  XCH addr1 addr2 ⇒ λinstr_refl. 427 let s ≝ add_ticks1 s in 428 let old_addr ≝ get_arg_8 … s false addr2 in 429 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 430 let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in 431 set_arg_8 … s addr2 old_acc 432  XCHD addr1 addr2 ⇒ λinstr_refl. 433 let s ≝ add_ticks1 s in 434 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in 435 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in 436 let new_acc ≝ acc_nu @@ arg_nl in 437 let new_arg ≝ arg_nu @@ acc_nl in 438 let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in 439 set_arg_8 … s addr2 new_arg 440  RET ⇒ λinstr_refl. 441 let s ≝ add_ticks1 s in 442 let high_bits ≝ read_at_stack_pointer ?? s in 443 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 444 let s ≝ set_8051_sfr … s SFR_SP new_sp in 445 let low_bits ≝ read_at_stack_pointer ?? s in 446 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 447 let s ≝ set_8051_sfr … s SFR_SP new_sp in 448 let new_pc ≝ high_bits @@ low_bits in 449 set_program_counter … s new_pc 450  RETI ⇒ λinstr_refl. 451 let s ≝ add_ticks1 s in 452 let high_bits ≝ read_at_stack_pointer ?? s in 453 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 454 let s ≝ set_8051_sfr … s SFR_SP new_sp in 455 let low_bits ≝ read_at_stack_pointer ?? s in 456 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 457 let s ≝ set_8051_sfr … s SFR_SP new_sp in 458 let new_pc ≝ high_bits @@ low_bits in 459 set_program_counter … s new_pc 460  MOVX addr ⇒ λinstr_refl. 461 let s ≝ add_ticks1 s in 462 (* DPM: only copies  doesn't affect I/O *) 463 match addr with 464 [ inl l ⇒ 465 let 〈addr1, addr2〉 ≝ l in 466 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 467  inr r ⇒ 468 let 〈addr1, addr2〉 ≝ r in 469 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 470 ] 471  MOV addr ⇒ λinstr_refl. 472 let s ≝ add_ticks1 s in 473 match addr with 474 [ inl l ⇒ 475 match l with 476 [ inl l' ⇒ 477 match l' with 478 [ inl l'' ⇒ 479 match l'' with 480 [ inl l''' ⇒ 481 match l''' with 482 [ inl l'''' ⇒ 483 let 〈addr1, addr2〉 ≝ l'''' in 484 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 485  inr r'''' ⇒ 486 let 〈addr1, addr2〉 ≝ r'''' in 487 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 488 ] 489  inr r''' ⇒ 490 let 〈addr1, addr2〉 ≝ r''' in 491 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 492 ] 493  inr r'' ⇒ 494 let 〈addr1, addr2〉 ≝ r'' in 495 set_arg_16 … s (get_arg_16 … s addr2) addr1 496 ] 497  inr r ⇒ 498 let 〈addr1, addr2〉 ≝ r in 499 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 500 ] 501  inr r ⇒ 502 let 〈addr1, addr2〉 ≝ r in 503 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 504 ] 505  JC addr ⇒ λinstr_refl. 506 if get_cy_flag ?? s then 507 let s ≝ add_ticks1 s in 508 set_program_counter … s (addr_of addr s) 509 else 510 let s ≝ add_ticks2 s in 511 s 512  JNC addr ⇒ λinstr_refl. 513 if ¬(get_cy_flag ?? s) then 514 let s ≝ add_ticks1 s in 515 set_program_counter … s (addr_of addr s) 516 else 517 let s ≝ add_ticks2 s in 518 s 519  JB addr1 addr2 ⇒ λinstr_refl. 520 if get_arg_1 … s addr1 false then 521 let s ≝ add_ticks1 s in 522 set_program_counter … s (addr_of addr2 s) 523 else 524 let s ≝ add_ticks2 s in 525 s 526  JNB addr1 addr2 ⇒ λinstr_refl. 527 if ¬(get_arg_1 … s addr1 false) then 528 let s ≝ add_ticks1 s in 529 set_program_counter … s (addr_of addr2 s) 530 else 531 let s ≝ add_ticks2 s in 532 s 533  JBC addr1 addr2 ⇒ λinstr_refl. 534 let s ≝ set_arg_1 … s addr1 false in 535 if get_arg_1 … s addr1 false then 536 let s ≝ add_ticks1 s in 537 set_program_counter … s (addr_of addr2 s) 538 else 539 let s ≝ add_ticks2 s in 540 s 541  JZ addr ⇒ λinstr_refl. 542 if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then 543 let s ≝ add_ticks1 s in 544 set_program_counter … s (addr_of addr s) 545 else 546 let s ≝ add_ticks2 s in 547 s 548  JNZ addr ⇒ λinstr_refl. 549 if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then 550 let s ≝ add_ticks1 s in 551 set_program_counter … s (addr_of addr s) 552 else 553 let s ≝ add_ticks2 s in 554 s 555  CJNE addr1 addr2 ⇒ λinstr_refl. 556 match addr1 with 557 [ inl l ⇒ 558 let 〈addr1, addr2'〉 ≝ l in 559 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 560 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 561 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 562 let s ≝ add_ticks1 s in 563 let s ≝ set_program_counter … s (addr_of addr2 s) in 564 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 565 else 566 let s ≝ add_ticks2 s in 567 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 568  inr r' ⇒ 569 let 〈addr1, addr2'〉 ≝ r' in 570 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 571 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 572 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 573 let s ≝ add_ticks1 s in 574 let s ≝ set_program_counter … s (addr_of addr2 s) in 575 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 576 else 577 let s ≝ add_ticks2 s in 578 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 579 ] 580  DJNZ addr1 addr2 ⇒ λinstr_refl. 581 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in 582 let s ≝ set_arg_8 … s addr1 result in 583 if ¬(eq_bv ? result (zero 8)) then 584 let s ≝ add_ticks1 s in 585 set_program_counter … s (addr_of addr2 s) 586 else 587 let s ≝ add_ticks2 s in 588 s 589 ] (refl … instr)) 590 try (cases(other)) 591 try assumption (*20s*) 592 try (% @False) (*6s*) (* Bug exploited here to implement solve :*) 593 try ( 594 @(execute_1_technical … (subaddressing_modein …)) 595 @I 596 ) (*66s*) 597 whd in match execute_1_preinstruction; normalize nodelta 598 [1: (* ADD *) 599 >p normalize nodelta 600 >EQP %{1} 601 whd in ⊢ (??%?); 602 (* work on fetch_many *) 603 <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled 604 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 605 whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy)); 606 <EQppc 607 cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * * 608 #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm; 609 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 610 >(eq_instruction_to_eq … eq_instr) instr' whd in ⊢ (??%?); 611 @(pair_replace ?????????? p) 612 [2: normalize nodelta >EQs s >EQticks' ticks' 613 <instr_refl in EQticks; #EQticks >EQticks ticks 614 <instr_refl in sigma_increment_commutation; #sigma_increment_commutation 615 whd in ⊢ (??%%); 616 @split_eq_status 617 try % 618 [3: whd in ⊢ (??%%); >EQnewpc >sigma_increment_commutation % 619 2: whd in ⊢ (??%%); >set_clock_mk_Status_commutation 620 whd in match (set_flags ??????); 621 (* CSC: TO BE COMPLETED *) 622 ] 623  (*>get_arg_8_ok_set_clock*) (*CSC: to be done *) 624 ] 625 626 ] cases daemon 627 qed. 628 (* 629 630 631 @list_addressing_mode_tags_elim_prop try % whd 632 @list_addressing_mode_tags_elim_prop try % whd #arg 633 (* XXX: we first work on sigma_increment_commutation *) 634 #sigma_increment_commutation 635 normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation; 636 (* XXX: we work on the maps *) 637 whd in ⊢ (??%? → ?); 638 try (change with (if ? then ? else ? = ? → ?) 639 cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta) 640 #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm 641 (* XXX: we assume the fetch_many hypothesis *) 642 #fetch_many_assm 643 (* XXX: we give the existential *) 644 %{1} 645 whd in match (execute_1_pseudo_instruction0 ?????); 646 (* XXX: work on the left hand side of the equality *) 647 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 648 (* XXX: execute fetches some more *) 649 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 650 whd in fetch_many_assm; 651 >EQassembled in fetch_many_assm; 652 cases (fetch ??) * #instr #newpc #ticks normalize nodelta * * 653 #eq_instr #EQticks whd in EQticks:(???%); >EQticks 654 #fetch_many_assm whd in fetch_many_assm; 655 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 656 >(eq_instruction_to_eq … eq_instr) instr 657 [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs 658 @(pose … 659 (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy)) 660 #Pl #EQPl 661 cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq 662 lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) XX >EQlhs lhs 663 whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%))); 664 @pair_elim 665 >tech_pi1_let_as_commute 666 667 *) 668 90 669 91 670 theorem main_thm: … … 180 759 ] 181 760 ] 182 1: (* Instruction *) pi; * 761 1: (* Instruction *) pi; #instr 762 @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness 763 … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels … 764 EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …)) 765 4,5: cases daemon 766 ] 767 qed. 768 (* 769 * 183 770 [1,2,3: (* ADD, ADDC, SUBB *) 184 771 @list_addressing_mode_tags_elim_prop try % whd … … 207 794 #fetch_many_assm whd in fetch_many_assm; 208 795 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 209 >(eq_instruction_to_eq … eq_instr) instr whd in ⊢ (??%?); 796 >(eq_instruction_to_eq … eq_instr) instr 797 [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs 798 @(pose … 799 (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy)) 800 #Pl #EQPl 801 cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq 802 lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) XX >EQlhs lhs 803 whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%))); 804 @pair_elim 805 >tech_pi1_let_as_commute 806 807 808 whd in ⊢ (??%?); 210 809 [ @(pose … (execute_1_preinstruction' ???????)) 211 810 #lhs whd in ⊢ (???% → ?); #EQlhs 212 811 @(pose … (execute_1_preinstruction' ???????)) 213 812 #rhs whd in ⊢ (???% → ?); #EQrhs 214 813 814 215 815 CSC: delirium 216 816 … … 573 1173 cases daemon (* EASY CASES TO BE COMPLETED *) 574 1174 qed. 1175 *) 
src/ASM/Interpret.ma
r1969 r1971 112 112 include alias "ASM/BitVectorTrie.ma". 113 113 114 definition execute_1_preinstruction ':114 definition execute_1_preinstruction: 115 115 ∀ticks: nat × nat. 116 116 ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a. 117 ∀s: PreStatus m cm. 118 Σs': PreStatus m cm. 119 And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 120 (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) ≝ 117 ∀s: PreStatus m cm. PreStatus m cm ≝ 121 118 λticks: nat × nat. 122 119 λa, m: Type[0]. λcm. … … 126 123 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 127 124 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 128 match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm. 129 And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 130 (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s) with 125 match instr in preinstruction return λx. x = instr → PreStatus m cm with 131 126 [ ADD addr1 addr2 ⇒ λinstr_refl. 132 127 let s ≝ add_ticks1 s in … … 533 528 @I 534 529 ) (*66s*) 530 qed. 531 532 definition execute_1_preinstruction_ok': 533 ∀ticks: nat × nat. 534 ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a. 535 ∀s: PreStatus m cm. 536 Σs': PreStatus m cm. 537 (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in 538 (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 539 (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝ 540 λticks: nat × nat. 541 λa, m: Type[0]. λcm. 542 λaddr_of: a → PreStatus m cm → Word. 543 λinstr: preinstruction a. 544 λs: PreStatus m cm. 545 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 546 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 547 match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm. 548 ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s)) 549 (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with 550 [ ADD addr1 addr2 ⇒ λinstr_refl. 551 let s ≝ add_ticks1 s in 552 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 553 (get_arg_8 … s false addr2) false in 554 let cy_flag ≝ get_index' ? O ? flags in 555 let ac_flag ≝ get_index' ? 1 ? flags in 556 let ov_flag ≝ get_index' ? 2 ? flags in 557 let s ≝ set_arg_8 … s ACC_A result in 558 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 559  ADDC addr1 addr2 ⇒ λinstr_refl. 560 let s ≝ add_ticks1 s in 561 let old_cy_flag ≝ get_cy_flag ?? s in 562 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 563 (get_arg_8 … s false addr2) old_cy_flag in 564 let cy_flag ≝ get_index' ? O ? flags in 565 let ac_flag ≝ get_index' ? 1 ? flags in 566 let ov_flag ≝ get_index' ? 2 ? flags in 567 let s ≝ set_arg_8 … s ACC_A result in 568 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 569  SUBB addr1 addr2 ⇒ λinstr_refl. 570 let s ≝ add_ticks1 s in 571 let old_cy_flag ≝ get_cy_flag ?? s in 572 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) 573 (get_arg_8 … s false addr2) old_cy_flag in 574 let cy_flag ≝ get_index' ? O ? flags in 575 let ac_flag ≝ get_index' ? 1 ? flags in 576 let ov_flag ≝ get_index' ? 2 ? flags in 577 let s ≝ set_arg_8 … s ACC_A result in 578 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 579  ANL addr ⇒ λinstr_refl. 580 let s ≝ add_ticks1 s in 581 match addr with 582 [ inl l ⇒ 583 match l with 584 [ inl l' ⇒ 585 let 〈addr1, addr2〉 ≝ l' in 586 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 587 set_arg_8 … s addr1 and_val 588  inr r ⇒ 589 let 〈addr1, addr2〉 ≝ r in 590 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 591 set_arg_8 … s addr1 and_val 592 ] 593  inr r ⇒ 594 let 〈addr1, addr2〉 ≝ r in 595 let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in 596 set_flags … s and_val (None ?) (get_ov_flag ?? s) 597 ] 598  ORL addr ⇒ λinstr_refl. 599 let s ≝ add_ticks1 s in 600 match addr with 601 [ inl l ⇒ 602 match l with 603 [ inl l' ⇒ 604 let 〈addr1, addr2〉 ≝ l' in 605 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 606 set_arg_8 … s addr1 or_val 607  inr r ⇒ 608 let 〈addr1, addr2〉 ≝ r in 609 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 610 set_arg_8 … s addr1 or_val 611 ] 612  inr r ⇒ 613 let 〈addr1, addr2〉 ≝ r in 614 let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in 615 set_flags … s or_val (None ?) (get_ov_flag … s) 616 ] 617  XRL addr ⇒ λinstr_refl. 618 let s ≝ add_ticks1 s in 619 match addr with 620 [ inl l' ⇒ 621 let 〈addr1, addr2〉 ≝ l' in 622 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 623 set_arg_8 … s addr1 xor_val 624  inr r ⇒ 625 let 〈addr1, addr2〉 ≝ r in 626 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 627 set_arg_8 … s addr1 xor_val 628 ] 629  INC addr ⇒ λinstr_refl. 630 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with 631 [ ACC_A ⇒ λacc_a: True. λEQaddr. 632 let s' ≝ add_ticks1 s in 633 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 634 set_arg_8 … s' ACC_A result 635  REGISTER r ⇒ λregister: True. λEQaddr. 636 let s' ≝ add_ticks1 s in 637 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 638 set_arg_8 … s' (REGISTER r) result 639  DIRECT d ⇒ λdirect: True. λEQaddr. 640 let s' ≝ add_ticks1 s in 641 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 642 set_arg_8 … s' (DIRECT d) result 643  INDIRECT i ⇒ λindirect: True. λEQaddr. 644 let s' ≝ add_ticks1 s in 645 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 646 set_arg_8 … s' (INDIRECT i) result 647  DPTR ⇒ λdptr: True. λEQaddr. 648 let s' ≝ add_ticks1 s in 649 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in 650 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in 651 let s ≝ set_8051_sfr … s' SFR_DPL bl in 652 set_8051_sfr … s' SFR_DPH bu 653  _ ⇒ λother: False. ⊥ 654 ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr)) 655  NOP ⇒ λinstr_refl. 656 let s ≝ add_ticks2 s in 657 s 658  DEC addr ⇒ λinstr_refl. 659 let s ≝ add_ticks1 s in 660 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in 661 set_arg_8 … s addr result 662  MUL addr1 addr2 ⇒ λinstr_refl. 663 let s ≝ add_ticks1 s in 664 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 665 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 666 let product ≝ acc_a_nat * acc_b_nat in 667 let ov_flag ≝ product ≥ 256 in 668 let low ≝ bitvector_of_nat 8 (product mod 256) in 669 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 670 let s ≝ set_8051_sfr … s SFR_ACC_A low in 671 set_8051_sfr … s SFR_ACC_B high 672  DIV addr1 addr2 ⇒ λinstr_refl. 673 let s ≝ add_ticks1 s in 674 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 675 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 676 match acc_b_nat with 677 [ O ⇒ set_flags … s false (None Bit) true 678  S o ⇒ 679 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 680 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 681 let s ≝ set_8051_sfr … s SFR_ACC_A q in 682 let s ≝ set_8051_sfr … s SFR_ACC_B r in 683 set_flags … s false (None Bit) false 684 ] 685  DA addr ⇒ λinstr_refl. 686 let s ≝ add_ticks1 s in 687 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in 688 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then 689 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in 690 let cy_flag ≝ get_index' ? O ? flags in 691 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in 692 if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then 693 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 694 let new_acc ≝ nu @@ acc_nl' in 695 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in 696 set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) 697 else 698 s 699 else 700 s 701  CLR addr ⇒ λinstr_refl. 702 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with 703 [ ACC_A ⇒ λacc_a: True. λEQaddr. 704 let s ≝ add_ticks1 s in 705 set_arg_8 … s ACC_A (zero 8) 706  CARRY ⇒ λcarry: True. λEQaddr. 707 let s ≝ add_ticks1 s in 708 set_arg_1 … s CARRY false 709  BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. 710 let s ≝ add_ticks1 s in 711 set_arg_1 … s (BIT_ADDR b) false 712  _ ⇒ λother: False. ⊥ 713 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 714  CPL addr ⇒ λinstr_refl. 715 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with 716 [ ACC_A ⇒ λacc_a: True. λEQaddr. 717 let s ≝ add_ticks1 s in 718 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 719 let new_acc ≝ negation_bv ? old_acc in 720 set_8051_sfr … s SFR_ACC_A new_acc 721  CARRY ⇒ λcarry: True. λEQaddr. 722 let s ≝ add_ticks1 s in 723 let old_cy_flag ≝ get_arg_1 … s CARRY true in 724 let new_cy_flag ≝ ¬old_cy_flag in 725 set_arg_1 … s CARRY new_cy_flag 726  BIT_ADDR b ⇒ λbit_addr: True. λEQaddr. 727 let s ≝ add_ticks1 s in 728 let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in 729 let new_bit ≝ ¬old_bit in 730 set_arg_1 … s (BIT_ADDR b) new_bit 731  _ ⇒ λother: False. ? 732 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 733  SETB b ⇒ λinstr_refl. 734 let s ≝ add_ticks1 s in 735 set_arg_1 … s b false 736  RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 737 let s ≝ add_ticks1 s in 738 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 739 let new_acc ≝ rotate_left … 1 old_acc in 740 set_8051_sfr … s SFR_ACC_A new_acc 741  RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 742 let s ≝ add_ticks1 s in 743 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 744 let new_acc ≝ rotate_right … 1 old_acc in 745 set_8051_sfr … s SFR_ACC_A new_acc 746  RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 747 let s ≝ add_ticks1 s in 748 let old_cy_flag ≝ get_cy_flag ?? s in 749 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 750 let new_cy_flag ≝ get_index' ? O ? old_acc in 751 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 752 let s ≝ set_arg_1 … s CARRY new_cy_flag in 753 set_8051_sfr … s SFR_ACC_A new_acc 754  RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 755 let s ≝ add_ticks1 s in 756 let old_cy_flag ≝ get_cy_flag ?? s in 757 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 758 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 759 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 760 let s ≝ set_arg_1 … s CARRY new_cy_flag in 761 set_8051_sfr … s SFR_ACC_A new_acc 762  SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *) 763 let s ≝ add_ticks1 s in 764 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 765 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 766 let new_acc ≝ nl @@ nu in 767 set_8051_sfr … s SFR_ACC_A new_acc 768  PUSH addr ⇒ λinstr_refl. 769 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with 770 [ DIRECT d ⇒ λdirect: True. λEQaddr. 771 let s ≝ add_ticks1 s in 772 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 773 let s ≝ set_8051_sfr … s SFR_SP new_sp in 774 write_at_stack_pointer … s d 775  _ ⇒ λother: False. ⊥ 776 ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr)) 777  POP addr ⇒ λinstr_refl. 778 let s ≝ add_ticks1 s in 779 let contents ≝ read_at_stack_pointer ?? s in 780 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 781 let s ≝ set_8051_sfr … s SFR_SP new_sp in 782 set_arg_8 … s addr contents 783  XCH addr1 addr2 ⇒ λinstr_refl. 784 let s ≝ add_ticks1 s in 785 let old_addr ≝ get_arg_8 … s false addr2 in 786 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 787 let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in 788 set_arg_8 … s addr2 old_acc 789  XCHD addr1 addr2 ⇒ λinstr_refl. 790 let s ≝ add_ticks1 s in 791 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in 792 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in 793 let new_acc ≝ acc_nu @@ arg_nl in 794 let new_arg ≝ arg_nu @@ acc_nl in 795 let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in 796 set_arg_8 … s addr2 new_arg 797  RET ⇒ λinstr_refl. 798 let s ≝ add_ticks1 s in 799 let high_bits ≝ read_at_stack_pointer ?? s in 800 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 801 let s ≝ set_8051_sfr … s SFR_SP new_sp in 802 let low_bits ≝ read_at_stack_pointer ?? s in 803 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 804 let s ≝ set_8051_sfr … s SFR_SP new_sp in 805 let new_pc ≝ high_bits @@ low_bits in 806 set_program_counter … s new_pc 807  RETI ⇒ λinstr_refl. 808 let s ≝ add_ticks1 s in 809 let high_bits ≝ read_at_stack_pointer ?? s in 810 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 811 let s ≝ set_8051_sfr … s SFR_SP new_sp in 812 let low_bits ≝ read_at_stack_pointer ?? s in 813 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 814 let s ≝ set_8051_sfr … s SFR_SP new_sp in 815 let new_pc ≝ high_bits @@ low_bits in 816 set_program_counter … s new_pc 817  MOVX addr ⇒ λinstr_refl. 818 let s ≝ add_ticks1 s in 819 (* DPM: only copies  doesn't affect I/O *) 820 match addr with 821 [ inl l ⇒ 822 let 〈addr1, addr2〉 ≝ l in 823 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 824  inr r ⇒ 825 let 〈addr1, addr2〉 ≝ r in 826 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 827 ] 828  MOV addr ⇒ λinstr_refl. 829 let s ≝ add_ticks1 s in 830 match addr with 831 [ inl l ⇒ 832 match l with 833 [ inl l' ⇒ 834 match l' with 835 [ inl l'' ⇒ 836 match l'' with 837 [ inl l''' ⇒ 838 match l''' with 839 [ inl l'''' ⇒ 840 let 〈addr1, addr2〉 ≝ l'''' in 841 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 842  inr r'''' ⇒ 843 let 〈addr1, addr2〉 ≝ r'''' in 844 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 845 ] 846  inr r''' ⇒ 847 let 〈addr1, addr2〉 ≝ r''' in 848 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 849 ] 850  inr r'' ⇒ 851 let 〈addr1, addr2〉 ≝ r'' in 852 set_arg_16 … s (get_arg_16 … s addr2) addr1 853 ] 854  inr r ⇒ 855 let 〈addr1, addr2〉 ≝ r in 856 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 857 ] 858  inr r ⇒ 859 let 〈addr1, addr2〉 ≝ r in 860 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 861 ] 862  JC addr ⇒ λinstr_refl. 863 if get_cy_flag ?? s then 864 let s ≝ add_ticks1 s in 865 set_program_counter … s (addr_of addr s) 866 else 867 let s ≝ add_ticks2 s in 868 s 869  JNC addr ⇒ λinstr_refl. 870 if ¬(get_cy_flag ?? s) then 871 let s ≝ add_ticks1 s in 872 set_program_counter … s (addr_of addr s) 873 else 874 let s ≝ add_ticks2 s in 875 s 876  JB addr1 addr2 ⇒ λinstr_refl. 877 if get_arg_1 … s addr1 false then 878 let s ≝ add_ticks1 s in 879 set_program_counter … s (addr_of addr2 s) 880 else 881 let s ≝ add_ticks2 s in 882 s 883  JNB addr1 addr2 ⇒ λinstr_refl. 884 if ¬(get_arg_1 … s addr1 false) then 885 let s ≝ add_ticks1 s in 886 set_program_counter … s (addr_of addr2 s) 887 else 888 let s ≝ add_ticks2 s in 889 s 890  JBC addr1 addr2 ⇒ λinstr_refl. 891 let s ≝ set_arg_1 … s addr1 false in 892 if get_arg_1 … s addr1 false then 893 let s ≝ add_ticks1 s in 894 set_program_counter … s (addr_of addr2 s) 895 else 896 let s ≝ add_ticks2 s in 897 s 898  JZ addr ⇒ λinstr_refl. 899 if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then 900 let s ≝ add_ticks1 s in 901 set_program_counter … s (addr_of addr s) 902 else 903 let s ≝ add_ticks2 s in 904 s 905  JNZ addr ⇒ λinstr_refl. 906 if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then 907 let s ≝ add_ticks1 s in 908 set_program_counter … s (addr_of addr s) 909 else 910 let s ≝ add_ticks2 s in 911 s 912  CJNE addr1 addr2 ⇒ λinstr_refl. 913 match addr1 with 914 [ inl l ⇒ 915 let 〈addr1, addr2'〉 ≝ l in 916 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 917 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 918 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 919 let s ≝ add_ticks1 s in 920 let s ≝ set_program_counter … s (addr_of addr2 s) in 921 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 922 else 923 let s ≝ add_ticks2 s in 924 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 925  inr r' ⇒ 926 let 〈addr1, addr2'〉 ≝ r' in 927 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 928 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 929 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 930 let s ≝ add_ticks1 s in 931 let s ≝ set_program_counter … s (addr_of addr2 s) in 932 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 933 else 934 let s ≝ add_ticks2 s in 935 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 936 ] 937  DJNZ addr1 addr2 ⇒ λinstr_refl. 938 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in 939 let s ≝ set_arg_8 … s addr1 result in 940 if ¬(eq_bv ? result (zero 8)) then 941 let s ≝ add_ticks1 s in 942 set_program_counter … s (addr_of addr2 s) 943 else 944 let s ≝ add_ticks2 s in 945 s 946 ] (refl … instr). 947 try (cases(other)) 948 try assumption (*20s*) 949 try (% @False) (*6s*) (* Bug exploited here to implement solve :*) 950 try ( 951 @(execute_1_technical … (subaddressing_modein …)) 952 @I 953 ) (*66s*) 954 whd in match execute_1_preinstruction; 535 955 normalize nodelta % 536 try (<instr_refl change with (cl_jump = cl_other → ?) #absurd destruct(absurd)) 537 try (<instr_refl change with (cl_return = cl_other → ?) #absurd destruct(absurd)) 956 [21,22,23,24: (* DIV *) 957 normalize nodelta in p; 958 7,8,9,10,11,12,13,14,15,16, (* INC *) 959 71,72,73,74,75,76, (* CLR *) 960 77,78,79,80,81,82, (* CPL *) 961 99,100: (* PUSH *) 962 lapply (subaddressing_modein ???) <EQaddr normalize nodelta #b 963 93,94: (* MOV *) 964 cases addr * normalize nodelta 965 [1,2,4,5: * normalize nodelta 966 [1,2,4,5: * normalize nodelta 967 [1,2,4,5: * normalize nodelta 968 [1,2,4,5: * normalize nodelta ]]]] 969 #arg1 #arg2 970 65,66, (* ANL *) 971 67,68, (* ORL *) 972 95,96: (* MOVX*) 973 cases addr * try (change with (? × ? → ?) * normalize nodelta) #addr11 #addr12 normalize nodelta 974 59,60: (* CJNE *) 975 cases addr1 normalize nodelta * #addr11 #addr12 normalize nodelta 976 cases (¬(eq_bv ???)) normalize nodelta 977 69,70: (* XRL *) 978 cases addr normalize nodelta * #addr1 #addr2 normalize nodelta 979 ] 980 try (>p normalize nodelta 981 try (>p1 normalize nodelta 982 try (>p2 normalize nodelta 983 try (>p3 normalize nodelta 984 try (>p4 normalize nodelta 985 try (>p5 normalize nodelta)))))) 986 try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd)) 987 try (change with (cl_return = cl_other → ?) #absurd destruct(absurd)) 538 988 try (@or_introl //) 539 989 try (@or_intror //) 540 #_ /demod/ % 541 qed. 542 543 definition execute_1_preinstruction: 544 ∀ticks: nat × nat. 545 ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a → 546 PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'. 547 990 try (#_ /demod/ %) 991 try (#_ //) 992 [ <set_arg_8_ok @or_introl // 993 *: <set_arg_1_ok @or_introl // ] 994 qed. 995 548 996 lemma execute_1_preinstruction_ok: 549 997 ∀ticks,a,m,cm,f,i,s. … … 551 999 clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧ 552 1000 (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s). 553 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi21001 #ticks #a #m #cm #f #i #s cases (execute_1_preinstruction_ok' ticks a m cm f i s) // 554 1002 qed. 555 1003
Note: See TracChangeset
for help on using the changeset viewer.