- Timestamp:
- Jul 25, 2012, 1:47:01 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2257 r2258 898 898 |3,7: 899 899 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 900 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/900 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 901 901 |2,6: 902 902 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try % … … 904 904 |4,8: 905 905 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try % 906 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/906 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 907 907 ] 908 908 |3: % … … 943 943 >status_refl 944 944 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) 945 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %945 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 946 946 |3: 947 947 >status_refl 948 948 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) 949 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %949 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 950 950 ] 951 951 |2: … … 957 957 >status_refl 958 958 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 959 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %959 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 960 960 |3: 961 961 >status_refl 962 962 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 963 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %963 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 964 964 ] 965 965 |3: … … 986 986 |3: 987 987 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … ps … ACC_A) 988 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] try %988 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try % 989 989 <addressing_mode_ok_assm_1 @(subaddressing_mode_elim … addr1) % 990 990 ] … … 1534 1534 |3,7: 1535 1535 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1536 [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]1536 [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 1537 1537 |2,6: 1538 1538 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) … … 1540 1540 |4,8: 1541 1541 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1542 [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]1542 [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 1543 1543 ] 1544 1544 |*: … … 1584 1584 |3,7: 1585 1585 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1586 [1,5: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]1586 [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 1587 1587 |2,6: 1588 1588 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) … … 1590 1590 |4,8: 1591 1591 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1592 [1,3: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]1592 [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 1593 1593 ] 1594 1594 |*: … … 1653 1653 |3: 1654 1654 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1655 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]1655 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 1656 1656 |2: 1657 1657 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) … … 1659 1659 |4: 1660 1660 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1661 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]1661 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 1662 1662 ] 1663 1663 |*: … … 1703 1703 |3: 1704 1704 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1705 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]1705 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 1706 1706 |2: 1707 1707 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) … … 1709 1709 |4: 1710 1710 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1711 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]1711 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 1712 1712 ] 1713 1713 |*: … … 1983 1983 |2: 1984 1984 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1985 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %1985 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1986 1986 |3: 1987 1987 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1988 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %1988 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1989 1989 ] 1990 1990 ] … … 2007 2007 [1: 2008 2008 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1) 2009 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2009 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2010 2010 |2: 2011 2011 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1) 2012 2012 [1: 2013 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/2013 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2014 2014 |2,3: 2015 2015 % … … 2021 2021 |2: 2022 2022 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others' … addressing_mode_ok_assm_2) 2023 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2023 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2024 2024 |3: 2025 2025 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others' … addressing_mode_ok_assm_2) 2026 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2026 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2027 2027 ] 2028 2028 ] … … 2048 2048 |2: 2049 2049 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) 2050 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2050 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2051 2051 |3: 2052 2052 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 2053 2053 [1: 2054 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/2054 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2055 2055 |2,3: 2056 2056 % … … 2060 2060 [1: 2061 2061 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 2062 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2062 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2063 2063 |2: 2064 2064 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) % … … 2080 2080 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 2081 2081 change with (set_arg_16 ????? = ?) 2082 @set_arg_16_status_of_pseudo_status 2082 @set_arg_16_status_of_pseudo_status try % 2083 2083 >EQs >EQticks <instr_refl >addr_refl 2084 2084 @sym_eq @set_clock_status_of_pseudo_status % … … 2259 2259 [1: 2260 2260 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 2261 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]2261 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 2262 2262 |2: 2263 2263 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 2264 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]2264 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 2265 2265 ] 2266 2266 |2: 2267 2267 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 2268 2268 [1: 2269 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/2269 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2270 2270 |*: 2271 2271 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta … … 2277 2277 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 2278 2278 [1: 2279 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/2279 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2280 2280 |2: 2281 2281 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta … … 2317 2317 [1: 2318 2318 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 2319 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]2319 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 2320 2320 |2: 2321 2321 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 2322 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/|*: % ]2322 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ] 2323 2323 ] 2324 2324 |2: … … 2340 2340 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 2341 2341 [1: 2342 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/2342 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2343 2343 |2: 2344 2344 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta … … 2350 2350 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 2351 2351 [1: 2352 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/2352 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2353 2353 |2: 2354 2354 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta … … 2362 2362 ] 2363 2363 ] 2364 | *)50: (* RET *)2364 |50: (* RET *) 2365 2365 >EQP -P normalize nodelta 2366 2366 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} … … 2415 2415 @set_clock_status_of_pseudo_status % 2416 2416 ] 2417 cases daemon 2417 2418 qed. 2418 2419 … … 2562 2563 [1,3: 2563 2564 >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1) 2564 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2565 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2565 2566 >(get_arg_8_set_program_counter … true addr1) 2566 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2567 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2567 2568 @get_arg_8_pseudo_addressing_mode_ok assumption 2568 2569 |2,4: … … 2574 2575 [1,10: 2575 2576 whd in ⊢ (??%%); >set_arg_8_set_program_counter 2576 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2577 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2577 2578 >low_internal_ram_set_program_counter 2578 2579 [1: … … 2585 2586 |2,11: 2586 2587 whd in ⊢ (??%%); >set_arg_8_set_program_counter 2587 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2588 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2588 2589 >high_internal_ram_set_program_counter 2589 2590 [1: … … 2596 2597 |3,12: 2597 2598 whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%); 2598 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2599 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2599 2600 >(external_ram_set_arg_8 ??? addr1) 2600 [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2601 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2601 2602 |4,13: 2602 2603 whd in ⊢ (??%%); >EQaddr_of normalize nodelta … … 2604 2605 >program_counter_set_program_counter 2605 2606 >set_arg_8_set_program_counter 2606 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2607 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2607 2608 >set_clock_set_program_counter >program_counter_set_program_counter 2608 2609 change with (add ??? = ?) … … 2610 2611 |2: 2611 2612 >set_arg_8_set_program_counter 2612 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2613 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2613 2614 >program_counter_set_program_counter 2614 2615 >set_arg_8_set_program_counter 2615 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2616 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2616 2617 >set_clock_set_program_counter >program_counter_set_program_counter 2617 2618 >sigma_increment_commutation <EQppc … … 2626 2627 >special_function_registers_8051_set_clock 2627 2628 >set_arg_8_set_program_counter in ⊢ (???%); 2628 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2629 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2629 2630 >special_function_registers_8051_set_program_counter 2630 2631 >set_arg_8_set_program_counter 2631 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2632 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2632 2633 >special_function_registers_8051_set_program_counter 2633 2634 @special_function_registers_8051_set_arg_8 assumption … … 2635 2636 >special_function_registers_8051_set_clock 2636 2637 >set_arg_8_set_program_counter 2637 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2638 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2638 2639 >set_arg_8_set_program_counter 2639 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2640 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2640 2641 >special_function_registers_8051_set_program_counter 2641 2642 >special_function_registers_8051_set_program_counter … … 2647 2648 [1: 2648 2649 >set_arg_8_set_program_counter 2649 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2650 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2650 2651 >set_arg_8_set_program_counter 2651 [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2652 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2652 2653 >special_function_registers_8052_set_program_counter 2653 2654 >special_function_registers_8052_set_program_counter … … 2732 2733 change with (add ???) in match (\snd (half_add ???)); 2733 2734 >set_arg_8_set_program_counter in ⊢ (???%); 2734 [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/]2735 [2,4,6,8: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] 2735 2736 >program_counter_set_program_counter in ⊢ (???%); 2736 2737 >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc') -
src/ASM/Test.ma
r2247 r2258 982 982 ∀cm. 983 983 ∀ps. 984 ∀addr : [[dptr]].985 ∀v : Word.984 ∀addr,addr': [[dptr]]. 985 ∀v,v': Word. 986 986 ∀M. ∀sigma. ∀policy. ∀s'. 987 987 status_of_pseudo_status M cm ps sigma policy = s' → 988 v=v' → addr=addr' → 988 989 set_arg_16 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 989 s' v addr=990 s' v' addr' = 990 991 status_of_pseudo_status M cm (set_arg_16 ? cm ps v addr) sigma policy. 991 #cm #ps #addr #v #M #sigma #policy #s' #s_refl <s_refl 992 #cm #ps #addr #addr' #v #v' #M #sigma #policy #s' #s_refl <s_refl #addr_refl 993 <addr_refl #v_refl <v_refl 992 994 @(subaddressing_mode_elim … addr) 993 995 whd in match set_arg_16; normalize nodelta
Note: See TracChangeset
for help on using the changeset viewer.