Changeset 2265 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jul 26, 2012, 3:48:31 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2262 r2265 2249 2249 cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *) 2250 2250 ] 2251  *)43: (* POP *)2251 43: (* POP *) 2252 2252 cases daemon 2253 2253 44: … … 2430 2430 ] 2431 2431 qed. 2432 2433 (*2434 (* XXX: work on the left hand side *)2435 (* XXX: switch to the right hand side *)2436 normalize nodelta >EQs s >EQticks ticks2437 whd in ⊢ (??%%);2438 (* XXX: finally, prove the equality using sigma commutation *)2439 cases daemon2440 11,12: (* DIV *)2441 (* XXX: work on the right hand side *)2442 normalize nodelta in p;2443 >p normalize nodelta2444 (* XXX: switch to the left hand side *)2445 instr_refl >EQP P normalize nodelta2446 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}2447 whd in ⊢ (??%?);2448 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);2449 @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl2450 >(?: pose_assm = 0) normalize nodelta2451 [2,4:2452 <p >pose_refl2453 cases daemon2454 1,3:2455 (* XXX: switch to the right hand side *)2456 >EQs s >EQticks ticks2457 whd in ⊢ (??%%);2458 (* XXX: finally, prove the equality using sigma commutation *)2459 @split_eq_status try %2460 cases daemon2461 ]2462 13,14,15: (* DA *)2463 (* XXX: work on the right hand side *)2464 >p normalize nodelta2465 >p1 normalize nodelta2466 try (>p2 normalize nodelta2467 try (>p3 normalize nodelta2468 try (>p4 normalize nodelta2469 try (>p5 normalize nodelta))))2470 (* XXX: switch to the left hand side *)2471 instr_refl >EQP P normalize nodelta2472 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}2473 whd in ⊢ (??%?);2474 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);2475 (* XXX: work on the left hand side *)2476 @(pair_replace ?????????? p)2477 [1,3,5:2478 /demod/2479 cases daemon2480 2,4,6:2481 @(if_then_else_replace ???????? p1)2482 [1,3,5:2483 cases daemon2484 2,4:2485 normalize nodelta2486 @(pair_replace ?????????? p2)2487 [1,3:2488 cases daemon2489 2,4:2490 normalize nodelta >p3 normalize nodelta2491 >p4 normalize nodelta try >p52492 ]2493 ]2494 (* XXX: switch to the right hand side *)2495 normalize nodelta >EQs s >EQticks ticks2496 whd in ⊢ (??%%);2497 (* XXX: finally, prove the equality using sigma commutation *)2498 @split_eq_status try %2499 cases daemon2500 ]2501 33,34,35,48: (* ANL, ORL, XRL, MOVX *)2502 (* XXX: work on the right hand side *)2503 cases addr #addr' normalize nodelta2504 [1,3:2505 cases addr' #addr'' normalize nodelta2506 ]2507 @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta2508 (* XXX: switch to the left hand side *)2509 instr_refl >EQP P normalize nodelta2510 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}2511 whd in ⊢ (??%?);2512 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);2513 (* XXX: work on the left hand side *)2514 (* XXX: switch to the right hand side *)2515 normalize nodelta >EQs s >EQticks ticks2516 whd in ⊢ (??%%);2517 (* XXX: finally, prove the equality using sigma commutation *)2518 cases daemon2519 47: (* MOV *)2520 (* XXX: work on the right hand side *)2521 cases addr addr #addr normalize nodelta2522 [1:2523 cases addr #addr normalize nodelta2524 [1:2525 cases addr #addr normalize nodelta2526 [1:2527 cases addr #addr normalize nodelta2528 [1:2529 cases addr #addr normalize nodelta2530 ]2531 ]2532 ]2533 ]2534 cases addr #lft #rgt normalize nodelta2535 (* XXX: switch to the left hand side *)2536 >EQP P normalize nodelta2537 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}2538 whd in ⊢ (??%?);2539 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);2540 (* XXX: work on the left hand side *)2541 (* XXX: switch to the right hand side *)2542 normalize nodelta >EQs s >EQticks ticks2543 whd in ⊢ (??%%);2544 (* XXX: finally, prove the equality using sigma commutation *)2545 cases daemon2546 ]2547 *)2548 2549 2550 (* [31,32: (* DJNZ *)2551 (* XXX: work on the right hand side *)2552 >p normalize nodelta >p1 normalize nodelta2553 (* XXX: switch to the left hand side *)2554 >EQP P normalize nodelta2555 #sigma_increment_commutation #maps_assm #fetch_many_assm2556 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;2557 <EQppc in fetch_many_assm;2558 whd in match (short_jump_cond ??);2559 @pair_elim #sj_possible #disp2560 @pair_elim #result #flags #sub16_refl2561 @pair_elim #upper #lower #vsplit_refl2562 inversion (get_index' bool ???) #get_index_refl' normalize nodelta2563 #sj_possible_pair destruct(sj_possible_pair)2564 >p1 normalize nodelta2565 [1,3:2566 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}2567 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;2568 normalize nodelta in ⊢ (% → ?); #fetch_many_assm2569 whd in ⊢ (??%?);2570 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);2571 lapply maps_assm whd in ⊢ (??%? → ?);2572 inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta2573 [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl M'2574 (* XXX: work on the left hand side *)2575 @(pair_replace ?????????? p) normalize nodelta2576 [1,3:2577 >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)2578 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ]2579 >(get_arg_8_set_program_counter … true addr1)2580 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ]2581 @get_arg_8_pseudo_addressing_mode_ok assumption2582 2,4:2583 >p1 normalize nodelta >EQs2584 alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".2585 >set_program_counter_status_of_pseudo_status2586 whd in ⊢ (??%%);2587 @split_eq_status2588 [1,10:2589 whd in ⊢ (??%%); >set_arg_8_set_program_counter2590 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]2591 >low_internal_ram_set_program_counter2592 [1:2593 >low_internal_ram_set_program_counter2594 (* XXX: ??? *)2595 2:2596 >low_internal_ram_set_clock2597 (* XXX: ??? *)2598 ]2599 2,11:2600 whd in ⊢ (??%%); >set_arg_8_set_program_counter2601 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]2602 >high_internal_ram_set_program_counter2603 [1:2604 >high_internal_ram_set_program_counter2605 (* XXX: ??? *)2606 2:2607 >high_internal_ram_set_clock2608 (* XXX: ??? *)2609 ]2610 3,12:2611 whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);2612 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]2613 >(external_ram_set_arg_8 ??? addr1)2614 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] %2615 4,13:2616 whd in ⊢ (??%%); >EQaddr_of normalize nodelta2617 [1:2618 >program_counter_set_program_counter2619 >set_arg_8_set_program_counter2620 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]2621 >set_clock_set_program_counter >program_counter_set_program_counter2622 change with (add ??? = ?)2623 (* XXX: ??? *)2624 2:2625 >set_arg_8_set_program_counter2626 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]2627 >program_counter_set_program_counter2628 >set_arg_8_set_program_counter2629 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2630 >set_clock_set_program_counter >program_counter_set_program_counter2631 >sigma_increment_commutation <EQppc2632 whd in match (assembly_1_pseudoinstruction ??????);2633 whd in match (expand_pseudo_instruction ??????);2634 (* XXX: ??? *)2635 ]2636 5,14:2637 whd in match (special_function_registers_8051 ???);2638 [1:2639 >special_function_registers_8051_set_program_counter2640 >special_function_registers_8051_set_clock2641 >set_arg_8_set_program_counter in ⊢ (???%);2642 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2643 >special_function_registers_8051_set_program_counter2644 >set_arg_8_set_program_counter2645 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2646 >special_function_registers_8051_set_program_counter2647 @special_function_registers_8051_set_arg_8 assumption2648 2:2649 >special_function_registers_8051_set_clock2650 >set_arg_8_set_program_counter2651 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2652 >set_arg_8_set_program_counter2653 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2654 >special_function_registers_8051_set_program_counter2655 >special_function_registers_8051_set_program_counter2656 @special_function_registers_8051_set_arg_8 assumption2657 ]2658 6,15:2659 whd in match (special_function_registers_8052 ???);2660 whd in match (special_function_registers_8052 ???) in ⊢ (???%);2661 [1:2662 >set_arg_8_set_program_counter2663 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2664 >set_arg_8_set_program_counter2665 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2666 >special_function_registers_8052_set_program_counter2667 >special_function_registers_8052_set_program_counter2668 @special_function_registers_8052_set_arg_8 assumption2669 2:2670 whd in ⊢ (??%%);2671 >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption2672 ]2673 (* XXX: we need special_function_registers_8052_set_arg_8 *)2674 7,16:2675 whd in match (p1_latch ???);2676 whd in match (p1_latch ???) in ⊢ (???%);2677 (* XXX: we need p1_latch_8052_set_arg_8 *)2678 8,17:2679 whd in match (p3_latch ???);2680 whd in match (p3_latch ???) in ⊢ (???%);2681 (* XXX: we need p3_latch_8052_set_arg_8 *)2682 9:2683 >clock_set_clock2684 >clock_set_program_counter in ⊢ (???%); >clock_set_clock2685 >EQticks <instr_refl @eq_f22686 [1:2687 whd in ⊢ (??%%); whd in match (ticks_of0 ??????);2688 2:2689 (* XXX: we need clock_set_arg_8 *)2690 ]2691 18:2692 ]2693 ]2694 (* XXX: switch to the right hand side *)2695 normalize nodelta >EQs s >EQticks ticks2696 cases (¬ eq_bv ???) normalize nodelta2697 whd in ⊢ (??%%);2698 (* XXX: finally, prove the equality using sigma commutation *)2699 @split_eq_status try %2700 [1,2,3,19,20,21,28,29,30:2701 cases daemon (* XXX: axioms as above *)2702 4,13,22,31:2703 5,14,23,32:2704 6,15,24,33:2705 7,16,25,34:2706 8,17,26,35:2707 whd in ⊢ (??%%);maps_assm2708 2709 9,18,27,36:2710 whd in ⊢ (??%%);2711 whd in match (ticks_of_instruction ?); <instr_refl2712 cases daemon (* XXX: daemon in ticks_of0 stopping progression *)2713 ]2714 2,4:2715 >(? : eq_v bool 9 eq_b upper (zero 9) = false)2716 [2, 4:2717 cases daemon (* XXX: !!! *)2718 ]2719 normalize nodelta >EQppc2720 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl2721 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'2722 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''2723 #fetch_many_assm whd in fetch_many_assm; %{2}2724 change with (execute_1 ?? = ?)2725 @(pose … (execute_1 ? (status_of_pseudo_status …)))2726 #status_after_1 #EQstatus_after_12727 <(?: ? = status_after_1)2728 [3,6:2729 >EQstatus_after_1 in ⊢ (???%);2730 whd in ⊢ (???%);2731 [1:2732 <fetch_refl in ⊢ (???%);2733 2:2734 <fetch_refl in ⊢ (???%);2735 ]2736 whd in ⊢ (???%);2737 @(pair_replace ?????????? p)2738 [1,3:2739 cases daemon2740 2,4:2741 normalize nodelta2742 whd in match (addr_of_relative ????);2743 cases (¬ eq_bv ???) normalize nodelta2744 >set_clock_mk_Status_commutation2745 whd in ⊢ (???%);2746 change with (add ???) in match (\snd (half_add ???));2747 >set_arg_8_set_program_counter in ⊢ (???%);2748 [2,4,6,8: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2749 >program_counter_set_program_counter in ⊢ (???%);2750 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')2751 [2,4,6,8:2752 >bitvector_of_nat_sign_extension_equivalence2753 [1,3,5,7:2754 >EQintermediate_pc' %2755 *:2756 repeat @le_S_S @le_O_n2757 ]2758 ]2759 [1,3: % ]2760 ]2761 1,4:2762 skip2763 ]2764 [3,4:2765 status_after_12766 @(pose … (execute_1 ? (mk_PreStatus …)))2767 #status_after_1 #EQstatus_after_12768 <(?: ? = status_after_1)2769 [3,6:2770 >EQstatus_after_1 in ⊢ (???%);2771 whd in ⊢ (???%);2772 (* XXX: matita bug with patterns across multiple goals *)2773 [1:2774 <fetch_refl'' in ⊢ (???%);2775 2:2776 <fetch_refl'' in ⊢ (???%);2777 ]2778 [2: % 1: whd in ⊢ (???%); % ]2779 1,4:2780 skip2781 ]2782 status_after_1 whd in ⊢ (??%?);2783 (* XXX: switch to the right hand side *)2784 normalize nodelta >EQs s >EQticks ticks2785 normalize nodelta whd in ⊢ (??%%);2786 ]2787 (* XXX: finally, prove the equality using sigma commutation *)2788 @split_eq_status try %2789 whd in ⊢ (??%%);2790 cases daemon2791 ]2792 30: (* CJNE *)2793 (* XXX: work on the right hand side *)2794 cases addr1 addr1 #addr1 normalize nodelta2795 cases addr1 addr1 #addr1_l #addr1_r normalize nodelta2796 (* XXX: switch to the left hand side *)2797 >EQP P normalize nodelta2798 #sigma_increment_commutation #maps_assm #fetch_many_assm2799 2800 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;2801 <EQppc in fetch_many_assm;2802 whd in match (short_jump_cond ??);2803 @pair_elim #sj_possible #disp2804 @pair_elim #result #flags #sub16_refl2805 @pair_elim #upper #lower #vsplit_refl2806 inversion (get_index' bool ???) #get_index_refl' normalize nodelta2807 #sj_possible_pair destruct(sj_possible_pair) normalize nodelta2808 [1,3:2809 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}2810 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;2811 normalize nodelta in ⊢ (% → ?); #fetch_many_assm2812 whd in ⊢ (??%?);2813 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);2814 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta2815 lapply (refl_to_jmrefl ??? eq_bv_refl) eq_bv_refl #eq_bv_refl2816 @(if_then_else_replace ???????? eq_bv_refl)2817 [1,3,5,7:2818 cases daemon2819 2,4,6,8:2820 (* XXX: switch to the right hand side *)2821 normalize nodelta >EQs s >EQticks ticks2822 whd in ⊢ (??%%);2823 (* XXX: finally, prove the equality using sigma commutation *)2824 @split_eq_status try %2825 [3,7,11,15:2826 whd in ⊢ (??%?);2827 [1,3:2828 cases daemon2829 2,4:2830 cases daemon2831 ]2832 ]2833 cases daemon (* XXX *)2834 ]2835 2,4:2836 >(? : eq_v bool 9 eq_b upper (zero 9) = false)2837 [2, 4:2838 cases daemon (* XXX: !!! *)2839 ]2840 normalize nodelta >EQppc2841 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl2842 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'2843 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''2844 #fetch_many_assm whd in fetch_many_assm; %{2}2845 change with (execute_1 ?? = ?)2846 @(pose … (execute_1 ? (status_of_pseudo_status …)))2847 #status_after_1 #EQstatus_after_12848 <(?: ? = status_after_1)2849 [2,5:2850 inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta2851 3,6:2852 >EQstatus_after_1 in ⊢ (???%);2853 whd in ⊢ (???%);2854 [1: <fetch_refl in ⊢ (???%);2855 2: <fetch_refl in ⊢ (???%);2856 ]2857 whd in ⊢ (???%);2858 inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta2859 whd in ⊢ (???%);2860 whd in match (addr_of_relative ????);2861 change with (add ???) in match (\snd (half_add ???));2862 >set_clock_set_program_counter in ⊢ (???%);2863 >program_counter_set_program_counter in ⊢ (???%);2864 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')2865 [2,4,6,8:2866 >bitvector_of_nat_sign_extension_equivalence2867 [1,3,5,7:2868 >EQintermediate_pc' %2869 *:2870 repeat @le_S_S @le_O_n2871 ]2872 1,5:2873 %2874 ]2875 1,4: skip2876 ]2877 [1,2,3,4:2878 status_after_12879 @(pose … (execute_1 ? (mk_PreStatus …)))2880 #status_after_1 #EQstatus_after_12881 <(?: ? = status_after_1)2882 [3,6,9,12:2883 >EQstatus_after_1 in ⊢ (???%);2884 whd in ⊢ (???%);2885 (* XXX: matita bug with patterns across multiple goals *)2886 [1: <fetch_refl'' in ⊢ (???%);2887 2: <fetch_refl'' in ⊢ (???%);2888 3: <fetch_refl'' in ⊢ (???%);2889 4: <fetch_refl'' in ⊢ (???%);2890 ] %2891 1,4,7,10:2892 skip2893 ]2894 status_after_1 whd in ⊢ (??%?);2895 (* XXX: switch to the right hand side *)2896 normalize nodelta >EQs s >EQticks ticks2897 whd in ⊢ (??%%);2898 ]2899 (* XXX: finally, prove the equality using sigma commutation *)2900 @split_eq_status try %2901 cases daemon2902 ]2903 17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)2904 (* XXX: work on the right hand side *)2905 >p normalize nodelta2906 (* XXX: switch to the left hand side *)2907 >EQP P normalize nodelta2908 #sigma_increment_commutation #maps_assm #fetch_many_assm2909 2910 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;2911 <EQppc in fetch_many_assm;2912 whd in match (short_jump_cond ??);2913 @pair_elim #sj_possible #disp2914 @pair_elim #result #flags #sub16_refl2915 @pair_elim #upper #lower #vsplit_refl2916 inversion (get_index' bool ???) #get_index_refl' normalize nodelta2917 #sj_possible_pair destruct(sj_possible_pair) normalize nodelta2918 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:2919 >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}2920 >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;2921 normalize nodelta in ⊢ (% → ?); #fetch_many_assm2922 whd in ⊢ (??%?);2923 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);2924 (* XXX: work on the left hand side *)2925 @(if_then_else_replace ???????? p) normalize nodelta2926 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:2927 cases daemon2928 ]2929 (* XXX: switch to the right hand side *)2930 normalize nodelta >EQs s >EQticks ticks2931 whd in ⊢ (??%%);2932 (* XXX: finally, prove the equality using sigma commutation *)2933 @split_eq_status try %2934 cases daemon2935 2,4,6,8,10,12,14,16,18,20,22,24,26,28:2936 >(? : eq_v bool 9 eq_b upper (zero 9) = false)2937 [2,4,6,8,10,12,14,16,18,20,22,24,26,28:2938 cases daemon (* XXX: !!! *)2939 ]2940 normalize nodelta >EQppc2941 * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl2942 * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'2943 * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''2944 #fetch_many_assm whd in fetch_many_assm; %{2}2945 change with (execute_1 ?? = ?)2946 @(pose … (execute_1 ? (status_of_pseudo_status …)))2947 #status_after_1 #EQstatus_after_12948 <(?: ? = status_after_1)2949 [3,6,9,12,15,18,21,24,27,30,33,36,39,42:2950 >EQstatus_after_1 in ⊢ (???%);2951 whd in ⊢ (???%);2952 [1: <fetch_refl in ⊢ (???%);2953 2: <fetch_refl in ⊢ (???%);2954 3: <fetch_refl in ⊢ (???%);2955 4: <fetch_refl in ⊢ (???%);2956 5: <fetch_refl in ⊢ (???%);2957 6: <fetch_refl in ⊢ (???%);2958 7: <fetch_refl in ⊢ (???%);2959 8: <fetch_refl in ⊢ (???%);2960 9: <fetch_refl in ⊢ (???%);2961 10: <fetch_refl in ⊢ (???%);2962 11: <fetch_refl in ⊢ (???%);2963 12: <fetch_refl in ⊢ (???%);2964 13: <fetch_refl in ⊢ (???%);2965 14: <fetch_refl in ⊢ (???%);2966 ]2967 whd in ⊢ (???%);2968 @(if_then_else_replace ???????? p)2969 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:2970 cases daemon2971 2,4,6,8,10,12,14,16,18,20,22,24,26,28:2972 normalize nodelta2973 whd in match (addr_of_relative ????);2974 >set_clock_mk_Status_commutation2975 [9,10:2976 (* XXX: demodulation not working in this case *)2977 >program_counter_set_arg_1 in ⊢ (???%);2978 >program_counter_set_program_counter in ⊢ (???%);2979 *:2980 /demod/2981 ]2982 whd in ⊢ (???%);2983 change with (add ???) in match (\snd (half_add ???));2984 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')2985 [2,4,6,8,10,12,14,16,18,20,22,24,26,28:2986 >bitvector_of_nat_sign_extension_equivalence2987 [1,3,5,7,9,11,13,15,17,19,21,23,25,27:2988 >EQintermediate_pc' %2989 *:2990 repeat @le_S_S @le_O_n2991 ]2992 ]2993 %2994 ]2995 1,4,7,10,13,16,19,22,25,28,31,34,37,40:2996 skip2997 ]2998 status_after_12999 @(pose … (execute_1 ? (mk_PreStatus …)))3000 #status_after_1 #EQstatus_after_13001 <(?: ? = status_after_1)3002 [3,6,9,12,15,18,21,24,27,30,33,36,39,42:3003 >EQstatus_after_1 in ⊢ (???%);3004 whd in ⊢ (???%);3005 (* XXX: matita bug with patterns across multiple goals *)3006 [1: <fetch_refl'' in ⊢ (???%);3007 2: <fetch_refl' in ⊢ (???%);3008 3: <fetch_refl'' in ⊢ (???%);3009 4: <fetch_refl' in ⊢ (???%);3010 5: <fetch_refl'' in ⊢ (???%);3011 6: <fetch_refl' in ⊢ (???%);3012 7: <fetch_refl'' in ⊢ (???%);3013 8: <fetch_refl' in ⊢ (???%);3014 9: <fetch_refl'' in ⊢ (???%);3015 10: <fetch_refl' in ⊢ (???%);3016 11: <fetch_refl'' in ⊢ (???%);3017 12: <fetch_refl' in ⊢ (???%);3018 13: <fetch_refl'' in ⊢ (???%);3019 14: <fetch_refl' in ⊢ (???%);3020 ]3021 whd in ⊢ (???%);3022 [9,10:3023 *:3024 /demod/3025 ] %3026 1,4,7,10,13,16,19,22,25,28,31,34,37,40:3027 skip3028 ]3029 status_after_1 whd in ⊢ (??%?);3030 (* XXX: switch to the right hand side *)3031 normalize nodelta >EQs s >EQticks ticks3032 whd in ⊢ (??%%);3033 (* XXX: finally, prove the equality using sigma commutation *)3034 @split_eq_status try %3035 [3,11,19,27,36,53,61:3036 >program_counter_set_program_counter >set_clock_mk_Status_commutation3037 [5: >program_counter_set_program_counter ]3038 >EQaddr_of normalize nodelta3039 whd in ⊢ (??%?); >EQlookup_labels normalize nodelta3040 >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);3041 @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)3042 >create_label_cost_refl normalize nodelta #relevant @relevant3043 whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))3044 try assumption whd in match instruction_has_label; normalize nodelta3045 <instr_refl normalize nodelta %3046 7,15,23,31,45,57,65:3047 >set_clock_mk_Status_commutation >program_counter_set_program_counter3048 whd in ⊢ (??%?); normalize nodelta3049 >EQppc in fetch_many_assm; #fetch_many_assm3050 [5:3051 >program_counter_set_arg_1 >program_counter_set_program_counter3052 ]3053 <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''3054 <bitvector_of_nat_sign_extension_equivalence3055 [1,3,5,7,9,11,13:3056 whd in ⊢ (???%); cases (half_add ???) normalize //3057 2,4,6,8,10,12,14:3058 @assembly1_lt_1283059 @le_S_S @le_O_n3060 ]3061 *:3062 cases daemon3063 ]3064 ]3065 4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)3066 (* XXX: work on the right hand side *)3067 lapply (subaddressing_modein ???)3068 <EQaddr normalize nodelta #irrelevant3069 try (>p normalize nodelta)3070 try (>p1 normalize nodelta)3071 (* XXX: switch to the left hand side *)3072 >EQP P normalize nodelta3073 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}3074 whd in ⊢ (??%?);3075 whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;3076 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);3077 (* XXX: work on the left hand side *)3078 [1,2,3,4,5:3079 generalize in ⊢ (??(???(?%))?);3080 6,7,8,9,10,11:3081 generalize in ⊢ (??(???(?%))?);3082 12:3083 generalize in ⊢ (??(???(?%))?);3084 ]3085 <EQaddr normalize nodelta #irrelevant3086 try @(jmpair_as_replace ?????????? p)3087 [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]3088 (* XXX: switch to the right hand side *)3089 normalize nodelta >EQs s >EQticks ticks3090 whd in ⊢ (??%%);3091 (* XXX: finally, prove the equality using sigma commutation *)3092 try @split_eq_status try % whd in ⊢ (??%%);3093 cases daemon3094 1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI *)3095 (* XXX: work on the right hand side *)3096 >p normalize nodelta3097 try (>p1 normalize nodelta)3098 (* XXX: switch to the left hand side *)3099 instr_refl >EQP P normalize nodelta3100 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}3101 whd in ⊢ (??%?);3102 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?);3103 (* XXX: work on the left hand side *)3104 @(pair_replace ?????????? p)3105 [1,3,5,7,9,11,13,15,17:3106 >set_clock_set_program_counter >set_clock_mk_Status_commutation3107 >set_program_counter_mk_Status_commutation >clock_set_program_counter3108 cases daemon3109 14,16,18:3110 normalize nodelta3111 @(pair_replace ?????????? p1)3112 [1,3,5:3113 >set_clock_mk_Status_commutation3114 cases daemon3115 ]3116 ]3117 (* XXX: switch to the right hand side *)3118 normalize nodelta >EQs s >EQticks ticks3119 whd in ⊢ (??%%);3120 (* XXX: finally, prove the equality using sigma commutation *)3121 try @split_eq_status try %3122 cases daemon *)
Note: See TracChangeset
for help on using the changeset viewer.