Changeset 1577
 Timestamp:
 Nov 30, 2011, 5:32:52 PM (8 years ago)
 Location:
 src/ASM
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CostsProof.ma
r1576 r1577 252 252 ∀s: Status. 253 253 clock … (execute_1 s) = current_instruction_cost s + clock … s. 254 255 axiom plus_minus_minus:256 ∀m, n, o: nat.257 m  (n + o) = (m  n)  o.258 254 259 255 axiom plus_le_le: … … 353 349 (current_instruction_cost status_pre_fun_call 354 350 + clock (BitVectorTrie Byte 16) status_pre_fun_call)); 355 >plus_minus_minus351 <minus_plus 356 352 <(plus_minus_m_m (clock (BitVectorTrie Byte 16) status_after_fun_call 357 353 clock (BitVectorTrie Byte 16) status_pre_fun_call) (current_instruction_cost status_pre_fun_call)) … … 406 402 >clock_execute_1 407 403 >commutative_plus in match ((current_instruction_cost status_pre+clock (BitVectorTrie Byte 16) status_pre)); 408 >plus_minus_minus404 <minus_plus 409 405 <plus_minus_m_m 410 406 [1: % 
src/ASM/Interpret.ma
r1575 r1577 166 166 167 167 definition execute_1_preinstruction: 168 ∀ticks: nat × nat. 169 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → 170 ∀s:PreStatus M. 171 Σs': PreStatus M. 172 And 173 (Or (clock … s'  clock … s = \fst ticks) 174 (clock … s'  clock … s = \snd ticks)) 175 (clock … s ≤ clock … s') 176 ≝ 177 λticks. 178 λA, M: Type[0]. 179 λaddr_of: A → (PreStatus M) → Word. 180 λinstr: preinstruction A. 181 λs: PreStatus M. 182 let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in 183 let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in 184 match instr return λx. 185 Σs': PreStatus M. 186 And 187 (Or (clock … s'  clock … s = \fst ticks) 188 (clock … s'  clock … s = \snd ticks)) 189 (clock … s ≤ clock … s') with 168 ∀ticks: nat × nat. 169 ∀a, m: Type[0]. (a → PreStatus m → Word) → preinstruction a → 170 ∀s: PreStatus m. 171 Σs': PreStatus m. 172 Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) ≝ 173 λticks: nat × nat. 174 λa, m: Type[0]. 175 λaddr_of: a → PreStatus m → Word. 176 λinstr: preinstruction a. 177 λs: PreStatus m. 178 let add_ticks1 ≝ λs: PreStatus m. set_clock … s (\fst ticks + clock … s) in 179 let add_ticks2 ≝ λs: PreStatus m. set_clock … s (\snd ticks + clock … s) in 180 match instr return λx. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with 190 181 [ ADD addr1 addr2 ⇒ 191 182 let s ≝ add_ticks1 s in … … 225 216 let 〈addr1, addr2〉 ≝ l' in 226 217 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 227 set_arg_8 ? s addr1 and_val218 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val) 228 219  inr r ⇒ 229 220 let 〈addr1, addr2〉 ≝ r in 230 221 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 231 set_arg_8 ? s addr1 and_val222 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 and_val) 232 223 ] 233 224  inr r ⇒ 234 225 let 〈addr1, addr2〉 ≝ r in 235 226 let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ? s addr2 true) in 236 set_flags ? s and_val (None ?) (get_ov_flag ? s)227 eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s and_val (None ?) (get_ov_flag ? s)) 237 228 ] 238 229  ORL addr ⇒ … … 240 231 match addr with 241 232 [ inl l ⇒ 242 match l with233 match l return λ_. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with 243 234 [ inl l' ⇒ 244 235 let 〈addr1, addr2〉 ≝ l' in 245 236 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 246 set_arg_8 ? s addr1 or_val237 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val) 247 238  inr r ⇒ 248 239 let 〈addr1, addr2〉 ≝ r in 249 240 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 250 set_arg_8 ? s addr1 or_val241 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 or_val) 251 242 ] 252 243  inr r ⇒ 253 244 let 〈addr1, addr2〉 ≝ r in 254 245 let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ? s addr2 true) in 255 set_flags ? s or_val (None ?) (get_ov_flag ? s)246 eject (PreStatus m) (λx. clock … s = clock … x) (set_flags ? s or_val (None ?) (get_ov_flag ? s)) 256 247 ] 257 248  XRL addr ⇒ … … 261 252 let 〈addr1, addr2〉 ≝ l' in 262 253 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 263 eject …(set_arg_8 ? s addr1 xor_val)254 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val) 264 255  inr r ⇒ 265 256 let 〈addr1, addr2〉 ≝ r in 266 257 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 267 eject …(set_arg_8 ? s addr1 xor_val)258 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 xor_val) 268 259 ] 269 260  INC addr ⇒ 270 match addr 271 return 272 λx. bool_to_Prop 273 (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → 274 Σs': PreStatus M. 275 And 276 (Or (clock … s'  clock … s = \fst ticks) 277 (clock … s'  clock … s = \snd ticks)) 278 (clock … s ≤ clock … s') 279 with 261 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with 280 262 [ ACC_A ⇒ λacc_a: True. 281 263 let s' ≝ add_ticks1 s in 282 264 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in 283 eject …(set_arg_8 ? s' ACC_A result)265 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' ACC_A result) 284 266  REGISTER r ⇒ λregister: True. 285 267 let s' ≝ add_ticks1 s in 286 268 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in 287 eject …(set_arg_8 ? s' (REGISTER r) result)269 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (REGISTER r) result) 288 270  DIRECT d ⇒ λdirect: True. 289 271 let s' ≝ add_ticks1 s in 290 272 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in 291 eject …(set_arg_8 ? s' (DIRECT d) result)273 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (DIRECT d) result) 292 274  INDIRECT i ⇒ λindirect: True. 293 275 let s' ≝ add_ticks1 s in 294 276 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 295 eject …(set_arg_8 ? s' (INDIRECT i) result)277 eject (PreStatus m) (λx. clock … s' = clock … x) (set_arg_8 ? s' (INDIRECT i) result) 296 278  DPTR ⇒ λdptr: True. 297 279 let s' ≝ add_ticks1 s in … … 299 281 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in 300 282 let s ≝ set_8051_sfr ? s' SFR_DPL bl in 301 eject …(set_8051_sfr ? s' SFR_DPH bu)283 eject (PreStatus m) (λx. clock … s' = clock … x) (set_8051_sfr ? s' SFR_DPH bu) 302 284  _ ⇒ λother: False. ⊥ 303 285 ] (subaddressing_modein … addr) … … 308 290 let s ≝ add_ticks1 s in 309 291 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in 310 eject …(set_arg_8 ? s addr result)292 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr result) 311 293  MUL addr1 addr2 ⇒ 312 294 let s ≝ add_ticks1 s in … … 318 300 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 319 301 let s ≝ set_8051_sfr ? s SFR_ACC_A low in 320 eject … (set_8051_sfr ? s SFR_ACC_B high)302 set_8051_sfr ? s SFR_ACC_B high 321 303  DIV addr1 addr2 ⇒ 322 304 let s ≝ add_ticks1 s in … … 330 312 let s ≝ set_8051_sfr ? s SFR_ACC_A q in 331 313 let s ≝ set_8051_sfr ? s SFR_ACC_B r in 332 eject … (set_flags ? s false (None Bit) false)314 set_flags ? s false (None Bit) false 333 315 ] 334 316  DA addr ⇒ … … 349 331 s 350 332  CLR addr ⇒ 351 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → 352 Σs': PreStatus M. 353 And 354 (Or (clock … s'  clock … s = \fst ticks) 355 (clock … s'  clock … s = \snd ticks)) 356 (clock … s ≤ clock … s') with 333 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with 357 334 [ ACC_A ⇒ λacc_a: True. 358 335 let s ≝ add_ticks1 s in 359 eject …(set_arg_8 ? s ACC_A (zero 8))336 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s ACC_A (zero 8)) 360 337  CARRY ⇒ λcarry: True. 361 338 let s ≝ add_ticks1 s in 362 eject …(set_arg_1 ? s CARRY false)339 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY false) 363 340  BIT_ADDR b ⇒ λbit_addr: True. 364 341 let s ≝ add_ticks1 s in 365 eject …(set_arg_1 ? s (BIT_ADDR b) false)342 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) false) 366 343  _ ⇒ λother: False. ⊥ 367 344 ] (subaddressing_modein … addr) 368 345  CPL addr ⇒ 369 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → 370 Σs': PreStatus M. 371 And 372 (Or (clock … s'  clock … s = \fst ticks) 373 (clock … s'  clock … s = \snd ticks)) 374 (clock … s ≤ clock … s') with 346 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with 375 347 [ ACC_A ⇒ λacc_a: True. 376 348 let s ≝ add_ticks1 s in 377 349 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 378 350 let new_acc ≝ negation_bv ? old_acc in 379 eject …(set_8051_sfr ? s SFR_ACC_A new_acc)351 eject (PreStatus m) (λx. clock … s = clock … x) (set_8051_sfr ? s SFR_ACC_A new_acc) 380 352  CARRY ⇒ λcarry: True. 381 353 let s ≝ add_ticks1 s in 382 354 let old_cy_flag ≝ get_arg_1 ? s CARRY true in 383 355 let new_cy_flag ≝ ¬old_cy_flag in 384 eject …(set_arg_1 ? s CARRY new_cy_flag)356 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s CARRY new_cy_flag) 385 357  BIT_ADDR b ⇒ λbit_addr: True. 386 358 let s ≝ add_ticks1 s in 387 359 let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in 388 360 let new_bit ≝ ¬old_bit in 389 eject …(set_arg_1 ? s (BIT_ADDR b) new_bit)361 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s (BIT_ADDR b) new_bit) 390 362  _ ⇒ λother: False. ? 391 363 ] (subaddressing_modein … addr) … … 426 398 set_8051_sfr ? s SFR_ACC_A new_acc 427 399  PUSH addr ⇒ 428 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → 429 Σs': PreStatus M. 430 And 431 (Or (clock … s'  clock … s = \fst ticks) 432 (clock … s'  clock … s = \snd ticks)) 433 (clock … s ≤ clock … s') with 400 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock … s) with 434 401 [ DIRECT d ⇒ λdirect: True. 435 402 let s ≝ add_ticks1 s in … … 450 417 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 451 418 let s ≝ set_8051_sfr ? s SFR_ACC_A old_addr in 452 eject …(set_arg_8 ? s addr2 old_acc)419 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr2 old_acc) 453 420  XCHD addr1 addr2 ⇒ 454 421 let s ≝ add_ticks1 s in … … 485 452 [ inl l ⇒ 486 453 let 〈addr1, addr2〉 ≝ l in 487 eject …(set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))454 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 488 455  inr r ⇒ 489 456 let 〈addr1, addr2〉 ≝ r in 490 eject …(set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))457 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 491 458 ] 492 459  MOV addr ⇒ … … 503 470 [ inl l'''' ⇒ 504 471 let 〈addr1, addr2〉 ≝ l'''' in 505 eject …(set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))472 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 506 473  inr r'''' ⇒ 507 474 let 〈addr1, addr2〉 ≝ r'''' in 508 eject …(set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))475 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 509 476 ] 510 477  inr r''' ⇒ 511 478 let 〈addr1, addr2〉 ≝ r''' in 512 eject …(set_arg_8 ? s addr1 (get_arg_8 ? s false addr2))479 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 513 480 ] 514 481  inr r'' ⇒ 515 482 let 〈addr1, addr2〉 ≝ r'' in 516 eject …(set_arg_16 ? s (get_arg_16 ? s addr2) addr1)483 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_16 ? s (get_arg_16 ? s addr2) addr1) 517 484 ] 518 485  inr r ⇒ 519 486 let 〈addr1, addr2〉 ≝ r in 520 eject …(set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))487 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)) 521 488 ] 522 489  inr r ⇒ 523 490 let 〈addr1, addr2〉 ≝ r in 524 eject …(set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false))491 eject (PreStatus m) (λx. clock … s = clock … x) (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)) 525 492 ] 526 493  JC addr ⇒ … … 534 501 if ¬(get_cy_flag ? s) then 535 502 let s ≝ add_ticks1 s in 536 eject … (set_program_counter ? s (addr_of addr s))503 set_program_counter ? s (addr_of addr s) 537 504 else 538 505 let s ≝ add_ticks2 s in … … 583 550 let s ≝ add_ticks1 s in 584 551 let s ≝ set_program_counter ? s (addr_of addr2 s) in 585 eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))552 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 586 553 else 587 554 let s ≝ add_ticks2 s in 588 eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))555 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 589 556  inr r' ⇒ 590 557 let 〈addr1, addr2'〉 ≝ r' in … … 594 561 let s ≝ add_ticks1 s in 595 562 let s ≝ set_program_counter ? s (addr_of addr2 s) in 596 eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))563 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 597 564 else 598 565 let s ≝ add_ticks2 s in 599 eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s))566 set_flags ? s new_cy (None ?) (get_ov_flag ? s) 600 567 ] 601 568  DJNZ addr1 addr2 ⇒ … … 609 576 s 610 577 ]. (*15s*) 578 try (destruct(other)) 611 579 try assumption (*20s*) 612 580 try % (*6s*) … … 615 583 @ I 616 584 ) (*66s*) 617 try @le_n 618 [ /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ /2 by or_introl/ 619  /demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ // 620 *: cases daemon (* XXX: easy? *) ] 585 try (<set_arg_8_ignores_clock normalize nodelta /demod/ %) 586 try (/demod/ normalize nodelta <set_arg_8_ignores_clock /demod/ %) 587 try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock /demod/ %) 588 try (normalize nodelta <set_flags_ignores_clock /demod/ %) 589 try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %) 590 try (/demod/ normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock @commutative_plus) 591 try (/demod/ normalize nodelta >clock_set_clock @commutative_plus) 592 (* XXX: weird open goals here *) 593 (* [14: normalize nodelta <set_arg_8_ignores_clock /demod/ normalize nodelta 594 try (normalize nodelta /demod/ %) 595 try (/demod/ normalize nodelta >clock_set_clock >set_arg_1_ignores_clock @commutative_plus) 596 597 try (normalize nodelta >set_8051_sfr_ignores_clock >set_8051_sfr_ignores_clock >clock_set_clock %)*) 598 cases daemon 621 599 qed. 622 600 … … 632 610 #nu #nl normalize nodelta; 633 611 cases(get_index_v bool 4 nu O (le_S_S O 3 (le_O_n 3))) 634 [ normalize nodelta; % 635  normalize nodelta; % 636 ] 612 normalize nodelta; % 637 613 qed. 638 614 639 615 definition execute_1_0: ∀s: Status. ∀current:instruction × Word × nat. 640 Σs': Status. And (clock … s'  clock … s = \snd current) (clock … s ≤ clock … s')≝616 Σs': Status. clock … s' = \snd current + clock … s ≝ 641 617 λs0,instr_pc_ticks. 642 618 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in 643 619 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 644 620 let s ≝ set_program_counter ? s0 pc in 645 match instr return λ_. Σs': Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s')with621 match instr return λ_. Σs': Status. clock … s' = ticks + clock … s0 with 646 622 [ RealInstruction instr ⇒ eject … (execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ? 647 623 (λx. λs. … … 652 628  MOVC addr1 addr2 ⇒ 653 629 let s ≝ set_clock ? s (ticks + clock ? s) in 654 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → 655 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 630 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with 656 631 [ ACC_DPTR ⇒ λacc_dptr: True. 657 632 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in … … 680 655  LJMP addr ⇒ 681 656 let s ≝ set_clock ? s (ticks + clock ? s) in 682 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → 683 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 657 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with 684 658 [ ADDR16 a ⇒ λaddr16: True. 685 659 set_program_counter ? s a … … 688 662  SJMP addr ⇒ 689 663 let s ≝ set_clock ? s (ticks + clock ? s) in 690 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → 691 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 664 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with 692 665 [ RELATIVE r ⇒ λrelative: True. 693 666 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in … … 697 670  AJMP addr ⇒ 698 671 let s ≝ set_clock ? s (ticks + clock ? s) in 699 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → 700 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 672 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with 701 673 [ ADDR11 a ⇒ λaddr11: True. 702 674 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in … … 711 683  ACALL addr ⇒ 712 684 let s ≝ set_clock ? s (ticks + clock ? s) in 713 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → 714 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 685 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with 715 686 [ ADDR11 a ⇒ λaddr11: True. 716 687 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in … … 729 700  LCALL addr ⇒ 730 701 let s ≝ set_clock ? s (ticks + clock ? s) in 731 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → 732 Σs':Status. And (clock … s'  clock … s0 = ticks) (clock … s0 ≤ clock … s') with 702 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status. clock … s' = ticks + clock … s0 with 733 703 [ ADDR16 a ⇒ λaddr16: True. 734 704 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in … … 743 713 ] (subaddressing_modein … addr) 744 714 ]. (*10s*) 745 cases daemon (* XXX: problem with russell here *) 715 try (cases(other)) 716 [2: normalize nodelta 717 >set_program_counter_ignores_clock 718 >write_at_stack_pointer_ignores_clock 719 >set_8051_sfr_ignores_clock 720 >write_at_stack_pointer_ignores_clock 721 >set_8051_sfr_ignores_clock >clock_set_clock 722 >set_program_counter_ignores_clock % 723 *: cases daemon 724 ] 746 725 (* 747 726 [*:try assumption] … … 772 751 773 752 definition execute_1: ∀s:Status. 774 Σs':Status. And (clock … s'  clock … s = current_instruction_cost s) (clock … s ≤ clock … s')≝753 Σs':Status. clock … s' = current_instruction_cost s + clock … s ≝ 775 754 λs: Status. 776 755 let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ? s) in … … 810 789 s. 811 790 normalize 812 @ 791 @I 813 792 qed. 814 793
Note: See TracChangeset
for help on using the changeset viewer.