Changeset 1534 for src/ASM/Interpret.ma
 Timestamp:
 Nov 23, 2011, 10:36:34 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Interpret.ma
r1533 r1534 122 122 123 123 lemma set_flags_ignores_clock: 124 ∀M,s,f1,f2,f3. clock M s ≤clock … (set_flags … s f1 f2 f3).124 ∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3). 125 125 // 126 126 qed. … … 132 132 qed. 133 133 134 example set_program_counter_ignores_clock: 135 ∀M: Type[0]. 136 ∀s: PreStatus M. 137 ∀pc: Word. 138 clock M (set_program_counter … s pc) = clock … s. 139 #M #s #pc % 140 qed. 141 142 example set_low_internal_ram_ignores_clock: 143 ∀M: Type[0]. 144 ∀s: PreStatus M. 145 ∀ram: BitVectorTrie Byte 7. 146 clock … (set_low_internal_ram … s ram) = clock … s. 147 #M #s #ram % 148 qed. 149 150 example set_8051_sfr_ignores_clock: 151 ∀M: Type[0]. 152 ∀s: PreStatus M. 153 ∀sfr: SFR8051. 154 ∀v: Byte. 155 clock … (set_8051_sfr ? s sfr v) = clock … s. 156 #M #s #sfr #v % 157 qed. 158 159 axiom set_arg_8_ignores_clock: 160 ∀M: Type[0]. 161 ∀s: PreStatus M. 162 ∀arg. 163 ∀val. 164 clock M (set_arg_8 … s arg val) = clock … s. 165 166 example clock_set_clock: 167 ∀M: Type[0]. 168 ∀s: PreStatus M. 169 ∀v. 170 clock … (set_clock … s v) = v. 171 #M #s #v % 172 qed. 173 134 174 lemma tech_clocks_le: 135 175 ∀M,s.∀t:Σs'. clock M s ≤ clock M s'. clock … s ≤ clock … t. … … 140 180 ∀ticks: nat × nat. 141 181 ∀A, M: Type[0]. (A → PreStatus M → Word) → preinstruction A → 142 ∀s:PreStatus M. Σs':PreStatus M. clock …s ≤ clock … s' ≝182 ∀s:PreStatus M. Σs': PreStatus M. clock M s ≤ clock … s' ≝ 143 183 λticks. 144 184 λA, M: Type[0]. … … 148 188 let add_ticks1 ≝ λs: PreStatus M.set_clock … s (\fst ticks + clock … s) in 149 189 let add_ticks2 ≝ λs: PreStatus M.set_clock … s (\snd ticks + clock … s) in 150 match instr with190 match instr return λx. Σs': PreStatus M. clock … s ≤ clock … s' with 151 191 [ ADD addr1 addr2 ⇒ 152 192 let s ≝ add_ticks1 s in … … 222 262 let 〈addr1, addr2〉 ≝ l' in 223 263 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 224 set_arg_8 ? s addr1 xor_val264 eject … (set_arg_8 ? s addr1 xor_val) 225 265  inr r ⇒ 226 266 let 〈addr1, addr2〉 ≝ r in 227 267 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ? s true addr2) in 228 set_arg_8 ? s addr1 xor_val268 eject … (set_arg_8 ? s addr1 xor_val) 229 269 ] 230 270  INC addr ⇒ 231 let s' ≝ add_ticks1 s in232 271 match addr return λx. bool_to_Prop (is_in … [[ acc_a; 233 272 registr; 234 273 direct; 235 274 indirect; 236 dptr ]] x) → Σs' .clock … s ≤ clock … s' with275 dptr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with 237 276 [ ACC_A ⇒ λacc_a: True. 277 let s' ≝ add_ticks1 s in 238 278 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true ACC_A) (bitvector_of_nat 8 1) in 239 279 eject … (set_arg_8 ? s' ACC_A result) 240 280  REGISTER r ⇒ λregister: True. 281 let s' ≝ add_ticks1 s in 241 282 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (REGISTER r)) (bitvector_of_nat 8 1) in 242 283 eject … (set_arg_8 ? s' (REGISTER r) result) 243 284  DIRECT d ⇒ λdirect: True. 285 let s' ≝ add_ticks1 s in 244 286 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (DIRECT d)) (bitvector_of_nat 8 1) in 245 287 eject … (set_arg_8 ? s' (DIRECT d) result) 246 288  INDIRECT i ⇒ λindirect: True. 289 let s' ≝ add_ticks1 s in 247 290 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ? s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 248 291 eject … (set_arg_8 ? s' (INDIRECT i) result) 249 292  DPTR ⇒ λdptr: True. 293 let s' ≝ add_ticks1 s in 250 294 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ? s' SFR_DPL) (bitvector_of_nat 8 1) in 251 295 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ? s' SFR_DPH) (zero 8) carry in 252 296 let s ≝ set_8051_sfr ? s' SFR_DPL bl in 253 set_8051_sfr ? s' SFR_DPH bu297 eject … (set_8051_sfr ? s' SFR_DPH bu) 254 298  _ ⇒ λother: False. ⊥ 255 299 ] (subaddressing_modein … addr) 300  NOP ⇒ 301 let s ≝ add_ticks2 s in 302 s 256 303  DEC addr ⇒ 257 304 let s ≝ add_ticks1 s in 258 305 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ? s true addr) (bitvector_of_nat 8 1) false in 259 set_arg_8 ? s addr result306 eject … (set_arg_8 ? s addr result) 260 307  MUL addr1 addr2 ⇒ 261 308 let s ≝ add_ticks1 s in … … 267 314 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 268 315 let s ≝ set_8051_sfr ? s SFR_ACC_A low in 269 set_8051_sfr ? s SFR_ACC_B high316 eject … (set_8051_sfr ? s SFR_ACC_B high) 270 317  DIV addr1 addr2 ⇒ 271 318 let s ≝ add_ticks1 s in … … 279 326 let s ≝ set_8051_sfr ? s SFR_ACC_A q in 280 327 let s ≝ set_8051_sfr ? s SFR_ACC_B r in 281 set_flags ? s false (None Bit) false328 eject … (set_flags ? s false (None Bit) false) 282 329 ] 283 330  DA addr ⇒ 284 331 let s ≝ add_ticks1 s in 285 let 〈 acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in332 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_ACC_A) in 286 333 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ? s) then 287 334 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ? s SFR_ACC_A) (bitvector_of_nat 8 6) false in … … 298 345 s 299 346  CLR addr ⇒ 300 let s ≝ add_ticks1 s in 301 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 302 [ ACC_A ⇒ λacc_a: True. set_arg_8 ? s ACC_A (zero 8) 303  CARRY ⇒ λcarry: True. set_arg_1 ? s CARRY false 304  BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 ? s (BIT_ADDR b) false 347 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with 348 [ ACC_A ⇒ λacc_a: True. 349 let s ≝ add_ticks1 s in 350 eject … (set_arg_8 ? s ACC_A (zero 8)) 351  CARRY ⇒ λcarry: True. 352 let s ≝ add_ticks1 s in 353 eject … (set_arg_1 ? s CARRY false) 354  BIT_ADDR b ⇒ λbit_addr: True. 355 let s ≝ add_ticks1 s in 356 eject … (set_arg_1 ? s (BIT_ADDR b) false) 305 357  _ ⇒ λother: False. ⊥ 306 358 ] (subaddressing_modein … addr) 307 359  CPL addr ⇒ 308 let s ≝ add_ticks1 s in 309 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with 360 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with 310 361 [ ACC_A ⇒ λacc_a: True. 362 let s ≝ add_ticks1 s in 311 363 let old_acc ≝ get_8051_sfr ? s SFR_ACC_A in 312 364 let new_acc ≝ negation_bv ? old_acc in 313 set_8051_sfr ? s SFR_ACC_A new_acc365 eject … (set_8051_sfr ? s SFR_ACC_A new_acc) 314 366  CARRY ⇒ λcarry: True. 367 let s ≝ add_ticks1 s in 315 368 let old_cy_flag ≝ get_arg_1 ? s CARRY true in 316 369 let new_cy_flag ≝ ¬old_cy_flag in 317 set_arg_1 ? s CARRY new_cy_flag370 eject … (set_arg_1 ? s CARRY new_cy_flag) 318 371  BIT_ADDR b ⇒ λbit_addr: True. 372 let s ≝ add_ticks1 s in 319 373 let old_bit ≝ get_arg_1 ? s (BIT_ADDR b) true in 320 374 let new_bit ≝ ¬old_bit in 321 set_arg_1 ? s (BIT_ADDR b) new_bit375 eject … (set_arg_1 ? s (BIT_ADDR b) new_bit) 322 376  _ ⇒ λother: False. ? 323 377 ] (subaddressing_modein … addr) … … 358 412 set_8051_sfr ? s SFR_ACC_A new_acc 359 413  PUSH addr ⇒ 360 let s ≝ add_ticks1 s in 361 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with 414 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus M. clock … s ≤ clock … s' with 362 415 [ DIRECT d ⇒ λdirect: True. 416 let s ≝ add_ticks1 s in 363 417 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 364 418 let s ≝ set_8051_sfr ? s SFR_SP new_sp in … … 386 440 let s ≝ set_8051_sfr ? s SFR_ACC_A new_acc in 387 441 set_arg_8 ? s addr2 new_arg 442  _ ⇒ ? 443 ]. 388 444  RET ⇒ 389 445 let s ≝ add_ticks1 s in … … 412 468 [ inl l ⇒ 413 469 let 〈addr1, addr2〉 ≝ l in 414 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)470 eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 415 471  inr r ⇒ 416 472 let 〈addr1, addr2〉 ≝ r in 417 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)473 eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 418 474 ] 419 475  MOV addr ⇒ … … 430 486 [ inl l'''' ⇒ 431 487 let 〈addr1, addr2〉 ≝ l'''' in 432 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)488 eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 433 489  inr r'''' ⇒ 434 490 let 〈addr1, addr2〉 ≝ r'''' in 435 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)491 eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 436 492 ] 437 493  inr r''' ⇒ 438 494 let 〈addr1, addr2〉 ≝ r''' in 439 set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)495 eject … (set_arg_8 ? s addr1 (get_arg_8 ? s false addr2)) 440 496 ] 441 497  inr r'' ⇒ 442 498 let 〈addr1, addr2〉 ≝ r'' in 443 set_arg_16 ? s (get_arg_16 ? s addr2) addr1499 eject … (set_arg_16 ? s (get_arg_16 ? s addr2) addr1) 444 500 ] 445 501  inr r ⇒ 446 502 let 〈addr1, addr2〉 ≝ r in 447 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)503 eject … (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)) 448 504 ] 449 505  inr r ⇒ 450 506 let 〈addr1, addr2〉 ≝ r in 451 set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)507 eject … (set_arg_1 ? s addr1 (get_arg_1 ? s addr2 false)) 452 508 ] 453 509  JC addr ⇒ 454 510 if get_cy_flag ? s then 455 let s ≝ add_ticks1 s in456 set_program_counter ? s (addr_of addr s)511 let s ≝ add_ticks1 s in 512 set_program_counter ? s (addr_of addr s) 457 513 else 458 let s ≝ add_ticks2 s in459 s514 let s ≝ add_ticks2 s in 515 s 460 516  JNC addr ⇒ 461 517 if ¬(get_cy_flag ? s) then 462 518 let s ≝ add_ticks1 s in 463 set_program_counter ? s (addr_of addr s)519 eject … (set_program_counter ? s (addr_of addr s)) 464 520 else 465 521 let s ≝ add_ticks2 s in … … 510 566 let s ≝ add_ticks1 s in 511 567 let s ≝ set_program_counter ? s (addr_of addr2 s) in 512 set_flags ? s new_cy (None ?) (get_ov_flag ? s)568 eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 513 569 else 514 570 let s ≝ add_ticks2 s in 515 (set_flags ? s new_cy (None ?) (get_ov_flag ? s))571 eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 516 572  inr r' ⇒ 517 573 let 〈addr1, addr2'〉 ≝ r' in … … 521 577 let s ≝ add_ticks1 s in 522 578 let s ≝ set_program_counter ? s (addr_of addr2 s) in 523 set_flags ? s new_cy (None ?) (get_ov_flag ? s)579 eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 524 580 else 525 581 let s ≝ add_ticks2 s in 526 (set_flags ? s new_cy (None ?) (get_ov_flag ? s))582 eject … (set_flags ? s new_cy (None ?) (get_ov_flag ? s)) 527 583 ] 528 584  DJNZ addr1 addr2 ⇒ … … 535 591 let s ≝ add_ticks2 s in 536 592 s 537  NOP ⇒538 let s ≝ add_ticks2 s in539 s540 593 ]. (*14s*) 541 try assumption (*20s*)594 (* try assumption (*20s*) 542 595 try % (*6s*) 543 596 try ( 544 597 @ (execute_1_technical … (subaddressing_modein …)) 545 598 @ I 546 ) (*34s*) 547 [1,2,3: /by/ (*41s*) 599 ) (*34s*) *) 600 [9: normalize nodelta <set_flags_ignores_clock >set_8051_sfr_ignores_clock 601 >clock_set_clock // 602 32,34: cases l #either normalize nodelta cases either 603 #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock 604 >clock_set_clock // 605 36,48: cases addr #either normalize nodelta cases either 606 #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock 607 >clock_set_clock // (* XXX: change addr to l *) 608 44: cases l2 #either normalize nodelta 609 [2: cases either #addr1 #addr2 normalize nodelta >set_arg_8_ignores_clock 610 >clock_set_clock // 611 1: cases either #addr cases addr #addr1 #addr2 normalize nodelta 612 >set_arg_8_ignores_clock >clock_set_clock // 613 ] (* XXX: change l2 to l *) 614 5: cases (sub_8_with_carry (get_arg_8 M s1 true addr) (bitvector_of_nat 8 1) false) 615 #result #flags normalize nodelta >set_arg_8_ignores_clock >clock_set_clock // 616 37: cases addr 617 20,21,30,31: (* XXX: segfault here *) 618 1,2,3: /by/ (*41s*) 548 619 4,6,7,8,10,11,12,13,14,15: /by/ (*6s*) 549 620 16,17,18,19,22,23,24,25,26,27,28,29: /by/ (*9s*) 550 621 33,35,39,41,43,54,55,56: /by/ (*6s*) 551 57: <set_args_8_ignores_clock /by/ (*0.5s ??*) 552 (* 31,32,34,36,44,48 facili *) 622 57,58,59,60,61: <set_args_8_ignores_clock /by/ (*0.5s ??*) 553 623 (* 5,9,20,21,30,37,38,40,42,45,46,47,49,50,51,52,53: ??? *) 554 624 *:cases daemon] … … 603 673 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 604 674 [ ADDR11 a ⇒ λaddr11: True. 605 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in675 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 606 676 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 607 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in677 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 608 678 let s ≝ write_at_stack_pointer ? s pc_bl in 609 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in679 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 610 680 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 611 681 let s ≝ write_at_stack_pointer ? s pc_bu in 612 let 〈thr, eig〉 ≝ split ? 3 8 a in613 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in682 let 〈thr, eig〉 ≝ split ? 3 8 a in 683 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 614 684 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 615 685 set_program_counter ? s new_addr … … 620 690 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 621 691 [ ADDR16 a ⇒ λaddr16: True. 622 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in692 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 623 693 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 624 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in694 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 625 695 let s ≝ write_at_stack_pointer ? s pc_bl in 626 let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in696 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in 627 697 let s ≝ set_8051_sfr ? s SFR_SP new_sp in 628 698 let s ≝ write_at_stack_pointer ? s pc_bu in … … 636 706 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 637 707 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 638 let new_addr ≝ \snd (half_add ? dptr big_acc)in708 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in 639 709 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 640 710 set_8051_sfr ? s SFR_ACC_A result 641 711  ACC_PC ⇒ λacc_pc: True. 642 712 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 643 let inc_pc ≝ \snd (half_add ? (program_counter ? s) (bitvector_of_nat 16 1)) in713 let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in 644 714 (* DPM: Under specified: does the carry from PC incrementation affect the *) 645 715 (* addition of the PC with the DPTR? At the moment, no. *) 646 716 let s ≝ set_program_counter ? s inc_pc in 647 let new_addr ≝ \snd (half_add ? inc_pc big_acc)in717 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 648 718 let result ≝ lookup ? ? new_addr (code_memory ? s) (zero ?) in 649 719 set_8051_sfr ? s SFR_ACC_A result … … 654 724 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in 655 725 let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in 656 let jmp_addr ≝ \snd (half_add ? big_acc dptr)in657 let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr)in726 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 727 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in 658 728 set_program_counter ? s new_pc 659 729  LJMP addr ⇒ … … 668 738 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 669 739 [ RELATIVE r ⇒ λrelative: True. 670 let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in740 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in 671 741 set_program_counter ? s new_pc 672 742  _ ⇒ λother: False. ⊥ … … 676 746 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':Status. clock … s0 ≤ clock … s' with 677 747 [ ADDR11 a ⇒ λaddr11: True. 678 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in679 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in748 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in 749 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 680 750 let bit ≝ get_index' ? O ? nl in 681 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in751 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 682 752 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 683 let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr)in753 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in 684 754 set_program_counter ? s new_pc 685 755  _ ⇒ λother: False. ⊥ 686 756 ] (subaddressing_modein … addr) 757 ]. 758 try assumption 759 try ( 760 normalize 761 repeat (@ (le_S_S)) 762 @ (le_O_n) 763 ) 764 try ( 765 @ (execute_1_technical … (subaddressing_modein …)) 766 @ I 767 ) 768 try ( 769 normalize 770 @ I 771 ) 687 772 ]. (*5s*) 688 773 try assumption (*12s*)
Note: See TracChangeset
for help on using the changeset viewer.