Changeset 2276 for src/ASM/AssemblyProofSplit.ma
- Timestamp:
- Jul 30, 2012, 2:36:41 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2273 r2276 56 56 qed. 57 57 58 lemma get_arg_8_status_of_pseudo_status': 59 ∀cm,ps,l. 60 ∀addr:[[ direct ; indirect ; registr ; acc_a ; acc_b ; data ; acc_dptr ; acc_pc ; ext_indirect ; ext_indirect_dptr ]]. 61 ∀M. ∀sigma. ∀policy. ∀s. 62 s = status_of_pseudo_status M cm ps sigma policy → 63 map_address_mode_using_internal_pseudo_address_map_ok1 M cm ps sigma addr → 64 map_address_mode_using_internal_pseudo_address_map_ok2 … M sigma cm ps addr (get_arg_8 … cm ps l addr) 65 = get_arg_8 … ps l addr → 66 get_arg_8 (BitVectorTrie Byte 16) (code_memory_of_pseudo_assembly_program cm sigma policy) 67 s l addr = get_arg_8 … ps l addr. 68 #cm #ps #l #addr #M #sigma #policy #s #H1 #H2 #H3 @get_arg_8_status_of_pseudo_status 69 try assumption % 70 qed. 71 58 72 lemma main_lemma_preinstruction: 59 73 ∀M, M': internal_pseudo_address_map. … … 98 112 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). 99 113 (* XXX: takes about 45 minutes to type check! *) 100 #M#M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy114 ** #low #high #accA #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy 101 115 #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels 102 116 #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels … … 513 527 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 514 528 whd in match execute_1_preinstruction; normalize nodelta 515 [ (*1,2: (* ADD and ADDC *)529 [1,2: (* ADD and ADDC *) 516 530 (* XXX: work on the right hand side *) 517 531 (* XXX: switch to the left hand side *) … … 519 533 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 520 534 whd in maps_assm:(??%%); 521 inversion (a ddressing_mode_ok?????) in maps_assm; #addressing_mode_ok_assm_1535 inversion (assert_data ?????) in maps_assm; #addressing_mode_ok_assm_1 522 536 [2,4: normalize nodelta #absurd destruct(absurd) ] 523 inversion (a ddressing_mode_ok?????) #addressing_mode_ok_assm_2537 inversion (assert_data ?????) #addressing_mode_ok_assm_2 524 538 [2,4: normalize nodelta #absurd destruct(absurd) ] 525 539 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 526 whd in ⊢ (??%?); 527 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl 540 letin M' ≝ (〈low,high,accA〉) 541 whd in ⊢ (??%?); 542 <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm 528 543 whd in ⊢ (??%?); 529 544 normalize nodelta >EQs >EQticks <instr_refl … … 531 546 [1,3: 532 547 @eq_f3 533 [1,2,4,5: 534 @(pose … (set_clock ????)) #status #status_refl 535 @sym_eq @(get_arg_8_status_of_pseudo_status … status … M') >status_refl -status_refl try % 536 [1,5: 548 [1,2,4,5: @(get_arg_8_status_of_pseudo_status' … M') 549 [3,9: 537 550 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr1 … addressing_mode_ok_assm_1) try % 538 551 @(subaddressing_mode_elim … addr1) % 539 | 3,7:552 |6,12: 540 553 @(addressing_mode_ok_to_map_address_mode_using_internal_pseudo_address_map_ok2 … addr2 … addressing_mode_ok_assm_2) try % 541 554 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 542 |2, 6:555 |2,8: 543 556 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr1 … addressing_mode_ok_assm_1) try % 544 557 @(subaddressing_mode_elim … addr1) % 545 | 4,8:558 |5,11: 546 559 @(map_address_mode_using_internal_pseudo_address_map_ok1_addr … addr2 … addressing_mode_ok_assm_2) try % 547 560 @(is_in_subvector_is_in_supervector … (subaddressing_modein …)) % 548 ]561 |*: % ] 549 562 |3: 550 563 % 551 |6: 552 @sym_eq @(get_cy_flag_status_of_pseudo_status M') 553 @sym_eq @set_clock_status_of_pseudo_status % 554 ] 564 |6: @(get_cy_flag_status_of_pseudo_status M') @set_clock_status_of_pseudo_status % ] 555 565 |2,4: 556 #result #flags @sym_eq 557 @set_flags_status_of_pseudo_status try % 558 @sym_eq @set_arg_8_status_of_pseudo_status try % 559 @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) 560 ] 561 |3: (* SUBB *) 566 #result #flags @set_flags_status_of_pseudo_status try % 567 @set_arg_8_status_of_pseudo_status try % 568 @(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)] 569 |(*3: (* SUBB *) 562 570 (* XXX: work on the right hand side *) 563 571 (* XXX: switch to the left hand side *) … … 1131 1139 ] 1132 1140 ] 1133 | *)12: (* JC *)1141 |12: (* JC *) 1134 1142 >EQP -P normalize nodelta 1135 1143 whd in match expand_pseudo_instruction; normalize nodelta … … 1872 1880 @(addressing_mode_ok_to_map_bit_address_mode_using_internal_pseudo_address_map_set_2 … ps ps … b … false (refl …) addressing_mode_ok_assm_1) 1873 1881 ] 1874 |*) 42: (* PUSH *)1882 |*)*)42: (* PUSH *) 1875 1883 >EQP -P normalize nodelta lapply instr_refl 1876 1884 @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta 1877 1885 #sigma_increment_commutation 1878 whd in ⊢ (??%? → ?); inversion M #callM #accM #callM_accM_refl normalize nodelta 1886 whd in ⊢ (??%? → ?); 1887 @vsplit_elim #bit_one #seven_bits 1888 cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H -bit_one 1889 cases bitone #bit_one_seven_bits_refl normalize nodelta 1890 [ @eq_bv_elim #seven_bits_refl normalize nodelta 1891 | inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry] 1892 #lookup_from_internal_ram_refl ] 1879 1893 @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1} 1880 1894 whd in ⊢ (??%?); … … 1883 1897 @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta 1884 1898 @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl)) 1885 [1 :1899 [1,3,5,7: 1886 1900 @eq_f2 try % 1887 1901 @(pose … (set_clock ????)) #status #status_refl 1888 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈callM, accM〉 … status) >status_refl -status_refl try % 1889 @sym_eq @set_clock_status_of_pseudo_status 1890 >EQs >EQticks <instr_refl % 1891 |2: 1902 @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl -status_refl try % 1903 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl % 1904 |*: 1892 1905 >EQs >EQticks <instr_refl 1893 1906 cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
Note: See TracChangeset
for help on using the changeset viewer.