- Timestamp:
- Jul 25, 2012, 4:52:44 PM (7 years ago)
- File:
-
- 1 edited
-
src/ASM/AssemblyProofSplit.ma (modified) (27 diffs)
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2259 r2260 488 488 ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_labels sigma policy ppc (Instruction instr). 489 489 ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16. 490 ∀EQaddr_of: addr_of = (λ x:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).490 ∀EQaddr_of: addr_of = (λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O)). 491 491 ∀s: PreStatus pseudo_assembly_program cm. 492 492 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))). … … 943 943 |3,7: 944 944 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 945 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 945 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 946 946 |2,6: 947 947 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try % … … 949 949 |4,8: 950 950 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try % 951 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 951 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 952 952 ] 953 953 |3: … … 1580 1580 |3,7: 1581 1581 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1582 [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]1582 [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1583 1583 |2,6: 1584 1584 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) … … 1586 1586 |4,8: 1587 1587 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1588 [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]1588 [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1589 1589 ] 1590 1590 |*: … … 1630 1630 |3,7: 1631 1631 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1632 [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]1632 [1,5: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1633 1633 |2,6: 1634 1634 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) … … 1636 1636 |4,8: 1637 1637 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1638 [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]1638 [1,3: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1639 1639 ] 1640 1640 |*: … … 1699 1699 |3: 1700 1700 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1701 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]1701 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1702 1702 |2: 1703 1703 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) … … 1705 1705 |4: 1706 1706 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1707 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]1707 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1708 1708 ] 1709 1709 |*: … … 1749 1749 |3: 1750 1750 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 1751 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]1751 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1752 1752 |2: 1753 1753 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … direct … addressing_mode_ok_assm_1) … … 1755 1755 |4: 1756 1756 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 1757 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]1757 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 1758 1758 ] 1759 1759 |*: … … 2009 2009 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1) 2010 2010 [1: 2011 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2011 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 2012 2012 |2,3: 2013 2013 % … … 2050 2050 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … direct … addressing_mode_ok_assm_1) 2051 2051 [1: 2052 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2052 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 2053 2053 |2,3: 2054 2054 % … … 2061 2061 |2: 2062 2062 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 2063 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2063 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2064 2064 ] 2065 2065 ] … … 2161 2161 |2: 2162 2162 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … acc_a … addressing_mode_ok_assm_1) 2163 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2163 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2164 2164 |3: 2165 2165 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … acc_a … addressing_mode_ok_assm_1) 2166 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] try %2166 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] try % 2167 2167 @(pose … (set_clock ????)) #status #status_refl 2168 2168 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 2169 2169 [1: 2170 2170 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_2) 2171 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2171 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2172 2172 |2: 2173 2173 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_2) 2174 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2174 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2175 2175 ] 2176 2176 ] … … 2192 2192 [1: 2193 2193 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … others … addressing_mode_ok_assm_1) 2194 [1: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/] %2194 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2195 2195 |2: 2196 2196 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … others … addressing_mode_ok_assm_1) 2197 2197 [1: 2198 /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/2198 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 2199 2199 |2,3: 2200 2200 % … … 2314 2314 [1: 2315 2315 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 2316 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]2316 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2317 2317 |2: 2318 2318 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 2319 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]2319 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2320 2320 ] 2321 2321 |2: 2322 2322 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 2323 2323 [1: 2324 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2324 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 2325 2325 |*: 2326 2326 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta … … 2332 2332 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 2333 2333 [1: 2334 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2334 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 2335 2335 |2: 2336 2336 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta … … 2372 2372 [1: 2373 2373 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) 2374 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]2374 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2375 2375 |2: 2376 2376 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 2377 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) |*: % ]2377 [1: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % 2378 2378 ] 2379 2379 |2: … … 2395 2395 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) 2396 2396 [1: 2397 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2397 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 2398 2398 |2: 2399 2399 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta … … 2405 2405 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 2406 2406 [1: 2407 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) 2407 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 2408 2408 |2: 2409 2409 whd in match get_8051_sfr in ⊢ (???%); normalize nodelta … … 2577 2577 [1,3: 2578 2578 >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1) 2579 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2579 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] 2580 2580 >(get_arg_8_set_program_counter … true addr1) 2581 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2581 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % ] 2582 2582 @get_arg_8_pseudo_addressing_mode_ok assumption 2583 2583 |2,4: … … 2589 2589 [1,10: 2590 2590 whd in ⊢ (??%%); >set_arg_8_set_program_counter 2591 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2591 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] 2592 2592 >low_internal_ram_set_program_counter 2593 2593 [1: … … 2600 2600 |2,11: 2601 2601 whd in ⊢ (??%%); >set_arg_8_set_program_counter 2602 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2602 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] 2603 2603 >high_internal_ram_set_program_counter 2604 2604 [1: … … 2611 2611 |3,12: 2612 2612 whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%); 2613 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2613 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] 2614 2614 >(external_ram_set_arg_8 ??? addr1) 2615 2615 [2,4: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ] % … … 2619 2619 >program_counter_set_program_counter 2620 2620 >set_arg_8_set_program_counter 2621 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2621 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] 2622 2622 >set_clock_set_program_counter >program_counter_set_program_counter 2623 2623 change with (add ??? = ?) … … 2625 2625 |2: 2626 2626 >set_arg_8_set_program_counter 2627 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) ]2627 [2: @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) %] 2628 2628 >program_counter_set_program_counter 2629 2629 >set_arg_8_set_program_counter
Note: See TracChangeset
for help on using the changeset viewer.
