Ignore:
Timestamp:
Jul 26, 2012, 3:48:31 AM (8 years ago)
Author:
sacerdot
Message:

Commented out code removed.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/ASM/AssemblyProofSplit.ma

    r2262 r2265  
    22492249      cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
    22502250    ]
    2251   |*)43: (* POP *)
     2251  |43: (* POP *)
    22522252    cases daemon
    22532253  |44:
    … …  
    24302430  ]
    24312431qed.
    2432 
    2433 (*
    2434   (* XXX: work on the left hand side *)
    2435   (* XXX: switch to the right hand side *)
    2436   normalize nodelta >EQs -s >EQticks -ticks
    2437   whd in ⊢ (??%%);
    2438   (* XXX: finally, prove the equality using sigma commutation *)
    2439   cases daemon
    2440   |11,12: (* DIV *)
    2441   (* XXX: work on the right hand side *)
    2442   normalize nodelta in p;
    2443   >p normalize nodelta
    2444   (* XXX: switch to the left hand side *)
    2445   -instr_refl >EQP -P normalize nodelta
    2446   #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_refl
    2450   >(?: pose_assm = 0) normalize nodelta
    2451   [2,4:
    2452     <p >pose_refl
    2453     cases daemon
    2454   |1,3:
    2455     (* XXX: switch to the right hand side *)
    2456     >EQs -s >EQticks -ticks
    2457     whd in ⊢ (??%%);
    2458     (* XXX: finally, prove the equality using sigma commutation *)
    2459     @split_eq_status try %
    2460     cases daemon
    2461   ]
    2462   |13,14,15: (* DA *)
    2463   (* XXX: work on the right hand side *)
    2464   >p normalize nodelta
    2465   >p1 normalize nodelta
    2466   try (>p2 normalize nodelta
    2467   try (>p3 normalize nodelta
    2468   try (>p4 normalize nodelta
    2469   try (>p5 normalize nodelta))))
    2470   (* XXX: switch to the left hand side *)
    2471   -instr_refl >EQP -P normalize nodelta
    2472   #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 daemon
    2480   |2,4,6:
    2481     @(if_then_else_replace ???????? p1)
    2482     [1,3,5:
    2483       cases daemon
    2484     |2,4:
    2485       normalize nodelta
    2486       @(pair_replace ?????????? p2)
    2487       [1,3:
    2488         cases daemon
    2489       |2,4:
    2490         normalize nodelta >p3 normalize nodelta
    2491         >p4 normalize nodelta try >p5
    2492       ]
    2493     ]
    2494   (* XXX: switch to the right hand side *)
    2495   normalize nodelta >EQs -s >EQticks -ticks
    2496   whd in ⊢ (??%%);
    2497   (* XXX: finally, prove the equality using sigma commutation *)
    2498   @split_eq_status try %
    2499   cases daemon
    2500   ]
    2501   |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
    2502   (* XXX: work on the right hand side *)
    2503   cases addr #addr' normalize nodelta
    2504   [1,3:
    2505     cases addr' #addr'' normalize nodelta
    2506   ]
    2507   @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
    2508   (* XXX: switch to the left hand side *)
    2509   -instr_refl >EQP -P normalize nodelta
    2510   #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 -ticks
    2516   whd in ⊢ (??%%);
    2517   (* XXX: finally, prove the equality using sigma commutation *)
    2518   cases daemon
    2519   |47: (* MOV *)
    2520   (* XXX: work on the right hand side *)
    2521   cases addr -addr #addr normalize nodelta
    2522   [1:
    2523     cases addr #addr normalize nodelta
    2524     [1:
    2525       cases addr #addr normalize nodelta
    2526       [1:
    2527         cases addr #addr normalize nodelta
    2528         [1:
    2529           cases addr #addr normalize nodelta
    2530         ]
    2531       ]
    2532     ]
    2533   ]
    2534   cases addr #lft #rgt normalize nodelta
    2535   (* XXX: switch to the left hand side *)
    2536   >EQP -P normalize nodelta
    2537   #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 -ticks
    2543   whd in ⊢ (??%%);
    2544   (* XXX: finally, prove the equality using sigma commutation *)
    2545   cases daemon
    2546   ]
    2547 *)
    2548 
    2549 
    2550 (*  [31,32: (* DJNZ *)
    2551   (* XXX: work on the right hand side *)
    2552   >p normalize nodelta >p1 normalize nodelta
    2553   (* XXX: switch to the left hand side *)
    2554   >EQP -P normalize nodelta
    2555   #sigma_increment_commutation #maps_assm #fetch_many_assm
    2556   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 #disp
    2560   @pair_elim #result #flags #sub16_refl
    2561   @pair_elim #upper #lower #vsplit_refl
    2562   inversion (get_index' bool ???) #get_index_refl' normalize nodelta
    2563   #sj_possible_pair destruct(sj_possible_pair)
    2564   >p1 normalize nodelta
    2565   [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_assm
    2569     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 nodelta
    2573     [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
    2574     (* XXX: work on the left hand side *)
    2575     @(pair_replace ?????????? p) normalize nodelta
    2576     [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 assumption
    2582     |2,4:
    2583       >p1 normalize nodelta >EQs
    2584       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_status
    2586        whd in ⊢ (??%%);
    2587       @split_eq_status
    2588       [1,10:
    2589         whd in ⊢ (??%%); >set_arg_8_set_program_counter
    2590         [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    2591         >low_internal_ram_set_program_counter
    2592         [1:
    2593           >low_internal_ram_set_program_counter
    2594           (* XXX: ??? *)
    2595         |2:
    2596           >low_internal_ram_set_clock
    2597           (* XXX: ??? *)
    2598         ]
    2599       |2,11:
    2600         whd in ⊢ (??%%); >set_arg_8_set_program_counter
    2601         [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    2602         >high_internal_ram_set_program_counter
    2603         [1:
    2604           >high_internal_ram_set_program_counter
    2605           (* XXX: ??? *)
    2606         |2:
    2607           >high_internal_ram_set_clock
    2608           (* 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 nodelta
    2617         [1:
    2618           >program_counter_set_program_counter
    2619           >set_arg_8_set_program_counter
    2620           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    2621           >set_clock_set_program_counter >program_counter_set_program_counter
    2622           change with (add ??? = ?)
    2623           (* XXX: ??? *)
    2624         |2:
    2625           >set_arg_8_set_program_counter
    2626           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %]
    2627           >program_counter_set_program_counter
    2628           >set_arg_8_set_program_counter
    2629           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    2630           >set_clock_set_program_counter >program_counter_set_program_counter
    2631           >sigma_increment_commutation <EQppc
    2632           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_counter
    2640           >special_function_registers_8051_set_clock
    2641           >set_arg_8_set_program_counter in ⊢ (???%);
    2642           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    2643           >special_function_registers_8051_set_program_counter
    2644           >set_arg_8_set_program_counter
    2645           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    2646           >special_function_registers_8051_set_program_counter
    2647           @special_function_registers_8051_set_arg_8 assumption
    2648         |2:
    2649           >special_function_registers_8051_set_clock
    2650           >set_arg_8_set_program_counter
    2651           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    2652           >set_arg_8_set_program_counter
    2653           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    2654           >special_function_registers_8051_set_program_counter
    2655           >special_function_registers_8051_set_program_counter
    2656           @special_function_registers_8051_set_arg_8 assumption
    2657         ]
    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_counter
    2663           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    2664           >set_arg_8_set_program_counter
    2665           [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]
    2666           >special_function_registers_8052_set_program_counter
    2667           >special_function_registers_8052_set_program_counter
    2668           @special_function_registers_8052_set_arg_8 assumption
    2669         |2:
    2670           whd in ⊢ (??%%);
    2671           >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
    2672         ]
    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_clock
    2684         >clock_set_program_counter in ⊢ (???%); >clock_set_clock
    2685         >EQticks <instr_refl @eq_f2
    2686         [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 -ticks
    2696     cases (¬ eq_bv ???) normalize nodelta
    2697     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_assm
    2708      
    2709     |9,18,27,36:
    2710       whd in ⊢ (??%%);
    2711       whd in match (ticks_of_instruction ?); <instr_refl
    2712       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 >EQppc
    2720     * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    2721     * @(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_1
    2727     <(?: ? = 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 daemon
    2740       |2,4:
    2741         normalize nodelta
    2742         whd in match (addr_of_relative ????);
    2743         cases (¬ eq_bv ???) normalize nodelta
    2744         >set_clock_mk_Status_commutation
    2745         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_equivalence
    2753           [1,3,5,7:
    2754             >EQintermediate_pc' %
    2755           |*:
    2756             repeat @le_S_S @le_O_n
    2757           ]
    2758         ]
    2759         [1,3: % ]
    2760       ]
    2761     |1,4:
    2762       skip
    2763     ]
    2764     [3,4:
    2765       -status_after_1
    2766       @(pose … (execute_1 ? (mk_PreStatus …)))
    2767       #status_after_1 #EQstatus_after_1
    2768       <(?: ? = 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         skip
    2781       ]
    2782       -status_after_1 whd in ⊢ (??%?);
    2783       (* XXX: switch to the right hand side *)
    2784       normalize nodelta >EQs -s >EQticks -ticks
    2785       normalize nodelta whd in ⊢ (??%%);
    2786     ]
    2787     (* XXX: finally, prove the equality using sigma commutation *)
    2788     @split_eq_status try %
    2789     whd in ⊢ (??%%);
    2790     cases daemon
    2791   ]
    2792   |30: (* CJNE *)
    2793   (* XXX: work on the right hand side *)
    2794   cases addr1 -addr1 #addr1 normalize nodelta
    2795   cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
    2796   (* XXX: switch to the left hand side *)
    2797   >EQP -P normalize nodelta
    2798   #sigma_increment_commutation #maps_assm #fetch_many_assm
    2799 
    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 #disp
    2804   @pair_elim #result #flags #sub16_refl
    2805   @pair_elim #upper #lower #vsplit_refl
    2806   inversion (get_index' bool ???) #get_index_refl' normalize nodelta
    2807   #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
    2808   [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_assm
    2812     whd in ⊢ (??%?);
    2813     <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
    2814     inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
    2815     lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
    2816     @(if_then_else_replace ???????? eq_bv_refl)
    2817     [1,3,5,7:
    2818       cases daemon
    2819     |2,4,6,8:
    2820       (* XXX: switch to the right hand side *)
    2821       normalize nodelta >EQs -s >EQticks -ticks
    2822       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 daemon
    2829         |2,4:
    2830           cases daemon
    2831         ]
    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 >EQppc
    2841     * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    2842     * @(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_1
    2848     <(?: ? = status_after_1)
    2849     [2,5:
    2850       inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
    2851     |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 nodelta
    2859       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_equivalence
    2867         [1,3,5,7:
    2868           >EQintermediate_pc' %
    2869         |*:
    2870           repeat @le_S_S @le_O_n
    2871         ]
    2872       |1,5:
    2873         %
    2874       ]
    2875     |1,4: skip
    2876     ]
    2877     [1,2,3,4:
    2878       -status_after_1
    2879       @(pose … (execute_1 ? (mk_PreStatus …)))
    2880       #status_after_1 #EQstatus_after_1
    2881       <(?: ? = 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         skip
    2893       ]
    2894       -status_after_1 whd in ⊢ (??%?);
    2895       (* XXX: switch to the right hand side *)
    2896       normalize nodelta >EQs -s >EQticks -ticks
    2897       whd in ⊢ (??%%);
    2898     ]
    2899     (* XXX: finally, prove the equality using sigma commutation *)
    2900     @split_eq_status try %
    2901     cases daemon
    2902   ]
    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 nodelta
    2906   (* XXX: switch to the left hand side *)
    2907   >EQP -P normalize nodelta
    2908   #sigma_increment_commutation #maps_assm #fetch_many_assm
    2909  
    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 #disp
    2914   @pair_elim #result #flags #sub16_refl
    2915   @pair_elim #upper #lower #vsplit_refl
    2916   inversion (get_index' bool ???) #get_index_refl' normalize nodelta
    2917   #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
    2918   [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_assm
    2922     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 nodelta
    2926     [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
    2927       cases daemon
    2928     ]
    2929     (* XXX: switch to the right hand side *)
    2930     normalize nodelta >EQs -s >EQticks -ticks
    2931     whd in ⊢ (??%%);
    2932     (* XXX: finally, prove the equality using sigma commutation *)
    2933     @split_eq_status try %
    2934     cases daemon
    2935   |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 >EQppc
    2941     * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
    2942     * @(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_1
    2948     <(?: ? = 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 daemon
    2971       |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
    2972         normalize nodelta
    2973         whd in match (addr_of_relative ????);
    2974         >set_clock_mk_Status_commutation
    2975         [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_equivalence
    2987           [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_n
    2991           ]
    2992         ]
    2993         %
    2994       ]
    2995     |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
    2996       skip
    2997     ]
    2998     -status_after_1
    2999     @(pose … (execute_1 ? (mk_PreStatus …)))
    3000     #status_after_1 #EQstatus_after_1
    3001     <(?: ? = 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       skip
    3028     ]
    3029     -status_after_1 whd in ⊢ (??%?);
    3030     (* XXX: switch to the right hand side *)
    3031     normalize nodelta >EQs -s >EQticks -ticks
    3032     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_commutation
    3037       [5: >program_counter_set_program_counter ]
    3038       >EQaddr_of normalize nodelta
    3039       whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
    3040       >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 @relevant
    3043       whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
    3044       try assumption whd in match instruction_has_label; normalize nodelta
    3045       <instr_refl normalize nodelta %
    3046     |7,15,23,31,45,57,65:
    3047       >set_clock_mk_Status_commutation >program_counter_set_program_counter
    3048       whd in ⊢ (??%?); normalize nodelta
    3049       >EQppc in fetch_many_assm; #fetch_many_assm
    3050       [5:
    3051         >program_counter_set_arg_1 >program_counter_set_program_counter
    3052       ]
    3053       <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
    3054       <bitvector_of_nat_sign_extension_equivalence
    3055       [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_128
    3059         @le_S_S @le_O_n
    3060       ]
    3061     |*:
    3062       cases daemon
    3063     ]
    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 #irrelevant
    3069   try (>p normalize nodelta)
    3070   try (>p1 normalize nodelta)
    3071   (* XXX: switch to the left hand side *)
    3072   >EQP -P normalize nodelta
    3073   #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 #irrelevant
    3086   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 -ticks
    3090   whd in ⊢ (??%%);
    3091   (* XXX: finally, prove the equality using sigma commutation *)
    3092   try @split_eq_status try % whd in ⊢ (??%%);
    3093   cases daemon
    3094   |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 nodelta
    3097   try (>p1 normalize nodelta)
    3098   (* XXX: switch to the left hand side *)
    3099   -instr_refl >EQP -P normalize nodelta
    3100   #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_commutation
    3107     >set_program_counter_mk_Status_commutation >clock_set_program_counter
    3108     cases daemon
    3109   |14,16,18:
    3110     normalize nodelta
    3111     @(pair_replace ?????????? p1)
    3112     [1,3,5:
    3113       >set_clock_mk_Status_commutation
    3114       cases daemon
    3115     ]
    3116   ]
    3117   (* XXX: switch to the right hand side *)
    3118   normalize nodelta >EQs -s >EQticks -ticks
    3119   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.