Changeset 2108
- Timestamp:
- Jun 25, 2012, 2:39:06 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Arithmetic.ma
r2032 r2108 534 534 \snd (half_add n l r). 535 535 536 axiom add_zero: 536 lemma half_add_carry_Sn: 537 ∀n: nat. 538 ∀l: BitVector n. 539 ∀hd: bool. 540 \fst (half_add (S n) (hd:::l) (false:::(zero n))) = 541 andb hd (\fst (half_add n l (zero n))). 542 #n #l elim l 543 [1: 544 #hd normalize cases hd % 545 |2: 546 #n' #hd #tl #inductive_hypothesis #hd' 547 whd in match half_add; normalize nodelta 548 whd in match full_add; normalize nodelta 549 normalize in ⊢ (??%%); cases hd' normalize 550 @pair_elim #c1 #r #c1_r_refl cases c1 % 551 ] 552 qed. 553 554 lemma half_add_zero_carry_false: 555 ∀m: nat. 556 ∀b: BitVector m. 557 \fst (half_add m b (zero m)) = false. 558 #m #b elim b try % 559 #n #hd #tl #inductive_hypothesis 560 change with (false:::(zero ?)) in match (zero ?); 561 >half_add_carry_Sn >inductive_hypothesis cases hd % 562 qed. 563 564 axiom half_add_true_true_carry_true: 565 ∀n: nat. 566 ∀hd, hd': bool. 567 ∀l, r: BitVector n. 568 \fst (half_add (S n) (true:::l) (true:::r)) = true. 569 570 lemma add_Sn_carry_add: 571 ∀n: nat. 572 ∀hd, hd': bool. 573 ∀l, r: BitVector n. 574 add (S n) (hd:::l) (hd':::r) = 575 xorb (xorb hd hd') (\fst (half_add n l r)):::add n l r. 576 #n #hd #hd' #l elim l 577 [1: 578 #r cases hd cases hd' 579 >(BitVector_O … r) normalize % 580 |2: 581 #n' #hd'' #tl #inductive_hypothesis #r 582 cases (BitVector_Sn … r) #hd''' * #tl' #r_refl destruct 583 cases hd cases hd' cases hd'' cases hd''' 584 whd in match (xorb ??); 585 cases daemon 586 ] 587 qed. 588 589 lemma add_zero: 537 590 ∀n: nat. 538 591 ∀l: BitVector n. 539 592 l = add n l (zero …). 593 #n #l elim l try % 594 #n' #hd #tl #inductive_hypothesis 595 change with (false:::zero ?) in match (zero ?); 596 >add_Sn_carry_add >half_add_zero_carry_false 597 cases hd <inductive_hypothesis % 598 qed. 599 600 axiom most_significant_bit_zero: 601 ∀size, m: nat. 602 ∀size_proof: 0 < size. 603 m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false. 604 normalize in size_proof; normalize @le_S_S assumption 605 qed. 606 607 axiom zero_add_head: 608 ∀m: nat. 609 ∀tl, hd. 610 (hd:::add m (zero m) tl) = add (S m) (zero (S m)) (hd:::tl). 611 612 lemma zero_add: 613 ∀m: nat. 614 ∀b: BitVector m. 615 add m (zero m) b = b. 616 #m #b elim b try % 617 #m' #hd #tl #inductive_hypothesis 618 <inductive_hypothesis in ⊢ (???%); 619 >zero_add_head % 620 qed. 621 622 axiom bitvector_of_nat_one_Sm: 623 ∀m: nat. 624 ∃b: BitVector m. 625 bitvector_of_nat (S m) 1 ≃ b @@ [[true]]. 626 627 axiom increment_zero_bitvector_of_nat_1: 628 ∀m: nat. 629 ∀b: BitVector m. 630 increment m b = add m (bitvector_of_nat m 1) b. 540 631 541 632 axiom add_associative: 542 ∀n: nat. 543 ∀l, c, r: BitVector n. 544 add … l (add … c r) = add … (add … l c) r. 633 ∀m: nat. 634 ∀l, c, r: BitVector m. 635 add m l (add m c r) = add m (add m l c) r. 636 637 lemma bitvector_of_nat_aux_buffer: 638 ∀m, n: nat. 639 ∀b: BitVector m. 640 bitvector_of_nat_aux m n b = add m (bitvector_of_nat m n) b. 641 #m #n elim n 642 [1: 643 #b change with (? = add ? (zero …) b) 644 >zero_add % 645 |2: 646 #n' #inductive_hypothesis #b 647 whd in match (bitvector_of_nat_aux ???); 648 >inductive_hypothesis whd in match (bitvector_of_nat ??) in ⊢ (???%); 649 >inductive_hypothesis >increment_zero_bitvector_of_nat_1 650 >increment_zero_bitvector_of_nat_1 <(add_zero m (bitvector_of_nat m 1)) 651 <add_associative % 652 ] 653 qed. 654 655 definition sign_extension: Byte → Word ≝ 656 λc. 657 let b ≝ get_index_v ? 8 c 1 ? in 658 [[ b; b; b; b; b; b; b; b ]] @@ c. 659 normalize 660 repeat (@le_S_S) 661 @le_O_n 662 qed. 663 664 lemma bitvector_of_nat_sign_extension_equivalence: 665 ∀m: nat. 666 ∀size_proof: m < 128. 667 sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m. 668 #m #size_proof whd in ⊢ (??%?); 669 >most_significant_bit_zero 670 [1: 671 elim m 672 [1: 673 % 674 |2: 675 #n' #inductive_hypothesis whd in match bitvector_of_nat; normalize nodelta 676 whd in match (bitvector_of_nat_aux ???); 677 whd in match (bitvector_of_nat_aux ???) in ⊢ (???%); 678 >(bitvector_of_nat_aux_buffer 16 n') 679 cases daemon 680 ] 681 |2: 682 assumption 683 ] 684 qed. 545 685 546 686 axiom add_commutative: -
src/ASM/Assembly.ma
r2101 r2108 604 604 qed. 605 605 606 axiom eq_identifier_eq: 606 axiom eqb_succ_injective_Pos: 607 ∀l, r: Pos. 608 eqb (succ l) (succ r) = true → eqb l r = true. 609 610 lemma eqb_true_to_refl_Pos: 611 ∀l, r: Pos. 612 eqb l r = true → l = r. 613 #l #r @(pos_elim2 … l r) 614 [1: 615 #r cases r 616 [1: 617 #_ % 618 |2,3: 619 #l normalize in ⊢ (% → ?); #absurd destruct(absurd) 620 ] 621 |2: 622 #l cases l 623 [1: 624 normalize in ⊢ (% → ?); #absurd destruct(absurd) 625 |2,3: 626 #l' normalize in ⊢ (% → ?); #absurd destruct(absurd) 627 ] 628 |3: 629 #l #r #inductive_hypothesis #relevant @eq_f 630 @inductive_hypothesis @eqb_succ_injective_Pos 631 assumption 632 ] 633 qed. 634 635 lemma eq_identifier_eq: 607 636 ∀tag: String. 608 637 ∀l. 609 638 ∀r. 610 639 eq_identifier tag l r = true → l = r. 640 #tag #l #r cases l cases r 641 #pos_l #pos_r 642 cases pos_l cases pos_r 643 [1: 644 #_ % 645 |2,3,4,7: 646 #p1_l normalize in ⊢ (% → ?); 647 #absurd destruct(absurd) 648 |5,9: 649 #p1_l #p1_r normalize in ⊢ (% → ?); 650 #relevant 651 >(eqb_true_to_refl_Pos … relevant) % 652 |*: 653 #p_l #p_r normalize in ⊢ (% → ?); 654 #absurd destruct(absurd) 655 ] 656 qed. 611 657 612 658 axiom neq_identifier_neq: … … 614 660 ∀l, r: identifier tag. 615 661 eq_identifier tag l r = false → (l = r → False). 616 662 617 663 (* label_map: identifier ↦ pseudo program counter *) 618 664 definition label_map ≝ identifier_map ASMTag ℕ. -
src/ASM/AssemblyProof.ma
r2078 r2108 1521 1521 let datalabels ≝ construct_datalabels preamble in 1522 1522 let lookup_datalabels ≝ λx. lookup_def … datalabels x (zero …) in 1523 〈assembled,costs'〉 = assembly program length_proofsigma policy →1523 〈assembled,costs'〉 = assembly program sigma policy → 1524 1524 (* costs = costs' ∧ CSC: costs != costs', costs' = sigma costs! *) 1525 1525 let code_memory ≝ load_code_memory assembled in … … 1533 1533 sigma newppc = add … pc (bitvector_of_nat … len). 1534 1534 #program #length_proof #sigma #policy #sigma_policy_witness #assembled #costs' 1535 cases (assembly program length_proof sigma policy) * #assembled' #costs'' 1536 @pair_elim #preamble #instr_list #EQprogram whd in ⊢ (% → %); 1537 @pair_elim #labels #costs #create_label_cost_refl whd in ⊢ (% → %); 1535 @pair_elim #preamble #instr_list #EQprogram 1536 cases (assembly program sigma policy) * #assembled' #costs'' 1537 >EQprogram normalize nodelta 1538 @pair_elim #labels #costs #EQcreate_label_cost_refl normalize nodelta 1538 1539 #assembly_ok #Pair_eq destruct(Pair_eq) whd 1539 #ppc #ppc_ok @pair_elim #pi #newppc #eq_fetch_pseudo_instruction 1540 @pair_elim #len #assembled #eq_assembly_1_pseudoinstruction whd 1541 lapply (assembly_ok ppc ?) [(*CSC: ????? WRONG HERE?*) cases daemon] -assembly_ok 1542 >eq_fetch_pseudo_instruction 1540 #ppc #ppc_ok 1541 @pair_elim #pi #newppc #EQfetch_pseudo_instruction 1542 >EQprogram in sigma_policy_witness; #sigma_policy_witness 1543 lapply (assembly_ok sigma_policy_witness ? ppc ?) 1544 [2: >EQprogram in length_proof; #length_proof; assumption ] try assumption 1545 >EQfetch_pseudo_instruction normalize nodelta 1543 1546 change with ((let 〈len0,assembledi〉 ≝ assembly_1_pseudoinstruction ????? pi in ∀j.∀H:j<|assembledi|.?) → ?) 1544 >(? : assembly_1_pseudoinstruction ????? pi = 〈len,assembled〉) 1545 [2: (*CSC: Provable, isn't it?*) cases daemon 1546 | whd in ⊢ (% → ?); #assembly_ok 1547 % 1547 @pair_elim #len #assembledi #EQassembly_1_pseudo_instruction 1548 letin lookup_labels ≝ (λx.sigma (bitvector_of_nat 16 (lookup_def ASMTag ℕ labels x O))) 1549 letin lookup_datalabels ≝ (λx. lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)) 1550 >(? : assembly_1_pseudoinstruction lookup_labels sigma policy ppc lookup_datalabels pi = 〈len,assembledi〉) 1551 [2: <EQassembly_1_pseudo_instruction % ] 1552 whd in ⊢ (% → ?); #assembly_ok % 1548 1553 [2: (*CSC: Use Jaap's invariant here *) cases daemon 1549 | lapply (load_code_memory_ok assembled' ?) [(*CSC: Jaap?*) cases daemon] 1554 |1: 1555 lapply (load_code_memory_ok assembledi ?) 1556 [1: 1557 lapply sigma_policy_witness whd in match sigma_policy_specification; 1558 normalize nodelta * #_ #relevant 1559 (* XXX: wait for Jaap to propagate the property that program 1560 is less than 2^16. 1561 *) 1562 cases daemon 1563 ] 1550 1564 #load_code_memory_ok 1551 -eq_assembly_1_pseudoinstruction -program -policy -costs'' -labels -preamble -instr_list -costs -pi -newppc 1552 cut (len=|assembled|) [(*CSC: provable before cleaning*) cases daemon] #EQlen 1565 cut (len=|assembledi|) 1566 [1: (*CSC: provable before cleaning *) 1567 cases daemon 1568 ] 1569 #EQlen 1553 1570 (* Nice statement here *) 1554 cut (∀j. ∀H: j < |assembled |.1555 nth_safe Byte j assembled H =1571 cut (∀j. ∀H: j < |assembledi|. 1572 nth_safe Byte j assembledi H = 1556 1573 \snd (next (load_code_memory assembled') 1557 1574 (bitvector_of_nat 16 1558 1575 (nat_of_bitvector … 1559 1576 (add … (sigma ppc) (bitvector_of_nat … j)))))) 1560 [(*CSC: is it provable?*) cases daemon 1561 | -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len 1562 elim assembled 1563 [ #pc #_ whd <add_zero % 1577 [1: 1578 cases daemon 1579 |2: 1580 -assembly_ok -load_code_memory_ok generalize in match (sigma ppc); >EQlen -len 1581 elim assembledi 1582 [1: 1583 #pc #_ whd (* <add_zero % 1564 1584 | #hd #tl #IH #pc #H % 1565 1585 [ lapply (H 0 ?) [ normalize @le_S_S @le_O_n ] whd in ⊢ (??%? → ?); -H #H … … 1572 1592 cases daemon 1573 1593 ] 1574 ] 1594 ] *) cases daemon 1595 ] 1596 cases daemon 1575 1597 qed. 1576 1598 … … 1584 1606 ∀ppc.∀ppc_ok. 1585 1607 let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in 1586 let 〈assembled, costs'〉 ≝ pi1 … (assembly program length_proofsigma policy) in1608 let 〈assembled, costs'〉 ≝ pi1 … (assembly program sigma policy) in 1587 1609 let code_memory ≝ load_code_memory assembled in 1588 1610 let data_labels ≝ construct_datalabels (\fst program) in … … 1600 1622 letin lookup_datalabels ≝ (λx. ?) 1601 1623 @pair_elim #pi #newppc #fetch_pseudo_refl 1602 lapply (assembly_ok 〈preamble, instr_list〉 sigma ?policy sigma_policy_specification_witness assembled costs')1603 normalize nodelta 1624 lapply (assembly_ok 〈preamble, instr_list〉 ? sigma policy sigma_policy_specification_witness assembled costs') 1625 normalize nodelta try assumption 1604 1626 @pair_elim #labels' #costs' #create_label_map_refl' #H 1605 1627 lapply (H (sym_eq … assembled_refl)) -H … … 1668 1690 definition internal_pseudo_address_map ≝ list ((BitVector 8) × (bool × Word)) × (option (bool × Word)). 1669 1691 1692 include alias "ASM/BitVectorTrie.ma". 1693 1694 include "common/AssocList.ma". 1695 1670 1696 axiom low_internal_ram_of_pseudo_low_internal_ram: 1671 1697 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. … … 1673 1699 axiom high_internal_ram_of_pseudo_high_internal_ram: 1674 1700 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 1675 1676 include "common/AssocList.ma".1677 1701 1678 1702 axiom low_internal_ram_of_pseudo_internal_ram_hit: … … 1760 1784 None ? 1761 1785 | _ ⇒ (* TO BE COMPLETED *) Some ? M ]]. 1762 1763 1786 1764 1787 definition next_internal_pseudo_address_map ≝ 1765 1788 λM:internal_pseudo_address_map. 1766 1789 λcm. 1767 λs:PseudoStatus cm. λppc_ok. 1768 next_internal_pseudo_address_map0 ? 1769 (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M cm s. 1790 λaddr_of. 1791 λs:PseudoStatus cm. 1792 λppc_ok. 1793 next_internal_pseudo_address_map0 ? cm addr_of 1794 (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s) ppc_ok)) M s. 1770 1795 1771 1796 definition code_memory_of_pseudo_assembly_program: … … 2295 2320 lemma snd_assembly_1_pseudoinstruction_ok: 2296 2321 ∀program: pseudo_assembly_program. 2322 ∀program_length_proof: |\snd program| < 2^16. 2297 2323 ∀sigma: Word → Word. 2298 2324 ∀policy: Word → bool. … … 2308 2334 let len ≝ \fst (assembly_1_pseudoinstruction lookup_labels sigma policy (*(sigma ppc)*) ppc lookup_datalabels pi) in 2309 2335 sigma (add … ppc (bitvector_of_nat ? 1)) = add … (sigma ppc) (bitvector_of_nat ? len). 2310 #program # sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi2336 #program #program_length_proof #sigma #policy #sigma_policy_specification_witness #ppc #ppc_in_bounds #pi 2311 2337 #lookup_labels #lookup_datalabels 2312 2338 #lookup_labels_refl #lookup_datalabels_refl #fetch_pseudo_refl … … 2316 2342 letin assembled ≝ (\fst (pi1 … (assembly program sigma policy))) 2317 2343 letin costs ≝ (\snd (pi1 … (assembly program sigma policy))) 2318 lapply (assembly_ok program sigma policy sigma_policy_specification_witness assembled costs)2344 lapply (assembly_ok program program_length_proof sigma policy sigma_policy_specification_witness assembled costs) 2319 2345 @pair_elim #preamble #instr_list #program_refl 2320 2346 @pair_elim #labels #costs' #create_label_cost_map_refl … … 2352 2378 2353 2379 (* XXX: easy but tedious *) 2354 axiomassembly1_lt_128:2380 lemma assembly1_lt_128: 2355 2381 ∀i: instruction. 2356 2382 |(assembly1 i)| < 128. 2357 2358 axiom most_significant_bit_zero: 2359 ∀size, m: nat. 2360 ∀size_proof: 0 < size. 2361 m < 2^size → get_index_v bool (S size) (bitvector_of_nat (S size) m) 1 ? = false. 2362 normalize in size_proof; /2/ 2363 qed. 2364 2365 lemma bitvector_of_nat_sign_extension_equivalence: 2366 ∀m: nat. 2367 ∀size_proof: m < 128. 2368 sign_extension … (bitvector_of_nat 8 m) = bitvector_of_nat 16 m. 2369 #m #size_proof whd in ⊢ (??%?); 2370 >most_significant_bit_zero 2371 [1: 2372 cases daemon 2373 |2: 2374 assumption 2375 |3: 2376 // 2383 #i cases i 2384 try (#assm1 #assm2) try #assm1 2385 [8: 2386 cases assm1 2387 try (#assm1 #assm2) try #assm1 2388 whd in match assembly1; normalize nodelta 2389 whd in match assembly_preinstruction; normalize nodelta 2390 try @(subaddressing_mode_elim … assm2) 2391 try @(subaddressing_mode_elim … assm1) try #w try #w' normalize nodelta 2392 [32: 2393 cases assm1 -assm1 #assm1 normalize nodelta 2394 cases assm1 #addr1 #addr2 normalize nodelta 2395 [1: 2396 @(subaddressing_mode_elim … addr2) 2397 |2: 2398 @(subaddressing_mode_elim … addr1) 2399 ] 2400 #w 2401 |35,36,37: 2402 cases assm1 -assm1 #assm1 normalize nodelta 2403 [1,3: 2404 cases assm1 -assm1 #assm1 normalize nodelta 2405 ] 2406 cases assm1 #addr1 #addr2 normalize nodelta 2407 @(subaddressing_mode_elim … addr2) try #w 2408 |49: 2409 cases assm1 -assm1 #assm1 normalize nodelta 2410 [1: 2411 cases assm1 -assm1 #assm1 normalize nodelta 2412 [1: 2413 cases assm1 -assm1 #assm1 normalize nodelta 2414 [1: 2415 cases assm1 -assm1 #assm1 normalize nodelta 2416 [1: 2417 cases assm1 -assm1 #assm1 normalize nodelta 2418 ] 2419 ] 2420 ] 2421 ] 2422 cases assm1 #addr1 #addr2 normalize nodelta 2423 [1,3,4,5: 2424 @(subaddressing_mode_elim … addr2) try #w 2425 |*: 2426 @(subaddressing_mode_elim … addr1) try #w 2427 normalize nodelta 2428 [1,2: 2429 @(subaddressing_mode_elim … addr2) try #w 2430 ] 2431 ] 2432 |50: 2433 cases assm1 -assm1 #assm1 normalize nodelta 2434 cases assm1 #addr1 #addr2 normalize nodelta 2435 [1: 2436 @(subaddressing_mode_elim … addr2) try #w 2437 |2: 2438 @(subaddressing_mode_elim … addr1) try #w 2439 ] 2440 ] 2441 normalize repeat @le_S_S @le_O_n 2377 2442 ] 2378 qed. 2443 whd in match assembly1; normalize nodelta 2444 [6: 2445 normalize repeat @le_S_S @le_O_n 2446 |7: 2447 @(subaddressing_mode_elim … assm2) normalize repeat @le_S_S @le_O_n 2448 |*: 2449 @(subaddressing_mode_elim … assm1) #w normalize nodelta repeat @le_S_S @le_O_n 2450 ] 2451 qed. -
src/ASM/AssemblyProofSplit.ma
r2047 r2108 405 405 include alias "ASM/Vector.ma". 406 406 407 axiom main_lemma_preinstruction: 408 ∀M, M': internal_pseudo_address_map. 409 ∀preamble: preamble. 410 ∀instr_list: list labelled_instruction. 411 ∀cm: pseudo_assembly_program. 412 ∀EQcm: cm = 〈preamble, instr_list〉. 413 ∀sigma: Word → Word. 414 ∀policy: Word → bool. 415 ∀sigma_policy_witness: sigma_policy_specification cm sigma policy. 416 ∀ps: PseudoStatus cm. 417 ∀ppc: Word. 418 ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps. 419 ∀labels: label_map. 420 ∀costs: BitVectorTrie costlabel 16. 421 ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉. 422 ∀newppc: Word. 423 ∀lookup_labels: Identifier → Word. 424 ∀EQlookup_labels: lookup_labels = (λx:Identifier. address_of_word_labels_code_mem instr_list x). 425 ∀lookup_datalabels: Identifier → Word. 426 ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)). 427 ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1). 428 ∀instr: preinstruction Identifier. 429 ∀ticks: nat × nat. 430 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr). 431 ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. 432 ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x). 433 ∀s: PreStatus pseudo_assembly_program cm. 434 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))). 435 ∀P: preinstruction Identifier → PseudoStatus cm → Prop. 436 ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc) 437 (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 438 lookup_datalabels (Instruction instr)))) → 439 next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cm ps = Some internal_pseudo_address_map M' → 440 fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps)) 441 (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → 442 ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) = 443 status_of_pseudo_status M' cm s sigma policy). 444 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). 445 446 (* 407 axiom sub16_with_carry_overflow: 408 ∀left, right, result: BitVector 16. 409 ∀flags: BitVector 3. 410 ∀upper: BitVector 9. 411 ∀lower: BitVector 7. 412 sub_16_with_carry left right false = 〈result, flags〉 → 413 vsplit bool 9 7 result = 〈upper, lower〉 → 414 get_index_v bool 3 flags 2 ? = true → 415 upper = [[true; true; true; true; true; true; true; true; true]]. 416 // 417 qed. 418 447 419 lemma main_lemma_preinstruction: 448 420 ∀M, M': internal_pseudo_address_map. … … 477 449 (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc 478 450 lookup_datalabels (Instruction instr)))) → 479 next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr) M cmps = Some internal_pseudo_address_map M' →451 next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' → 480 452 fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps)) 481 453 (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) → … … 899 871 [31,32: (* DJNZ *) 900 872 (* XXX: work on the right hand side *) 901 >p normalize nodelta 873 >p normalize nodelta >p1 normalize nodelta 902 874 (* XXX: switch to the left hand side *) 903 875 -instr_refl >EQP -P normalize nodelta 904 876 #sigma_increment_commutation #maps_assm #fetch_many_assm 905 877 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm; 906 whd in match (expand_relative_jump ????);907 878 <EQppc in fetch_many_assm; 879 whd in match (short_jump_cond ??); 880 @pair_elim #sj_possible #disp 908 881 @pair_elim #result #flags #sub16_refl 909 882 @pair_elim #upper #lower #vsplit_refl 910 cases (eq_bv ???) normalize nodelta 883 inversion (get_index' bool ???) #get_index_refl' normalize nodelta 884 #sj_possible_pair destruct(sj_possible_pair) 885 >p1 normalize nodelta 911 886 [1,3: 912 887 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1} 913 888 whd in ⊢ (??%?); 889 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm; 890 normalize nodelta in ⊢ (% → ?); #fetch_many_assm 914 891 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?); 915 892 (* XXX: work on the left hand side *) … … 927 904 cases daemon 928 905 |2,4: 906 XXX: here 929 907 >EQppc 930 908 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl -
src/ASM/Interpret.ma
r2062 r2108 3 3 include "ASM/Fetch.ma". 4 4 include "ASM/AbstractStatus.ma". 5 6 definition sign_extension: Byte → Word ≝7 λc.8 let b ≝ get_index_v ? 8 c 1 ? in9 [[ b; b; b; b; b; b; b; b ]] @@ c.10 normalize11 repeat (@le_S_S)12 @le_O_n13 qed.14 5 15 6 lemma execute_1_technical:
Note: See TracChangeset
for help on using the changeset viewer.