Changeset 2173 for src/ASM/AssemblyProofSplit.ma
 Timestamp:
 Jul 10, 2012, 5:29:32 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2172 r2173 19 19 include alias "ASM/Vector.ma". 20 20 include "ASM/Test.ma". 21 22 lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map: 23 ∀M, cm, ps, sigma, x. 24 ∀addr1: [[acc_a]]. 25 addressing_mode_ok pseudo_assembly_program M cm ps addr1=true → 26 map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x. 27 #M #cm #ps #sigma #x #addr1 28 @(subaddressing_mode_elim … addr1) 29 whd in ⊢ (??%? → ??%?); 30 cases (\snd M) 31 [1: 32 // 33 2: 34 #upper_lower #address normalize nodelta #absurd 35 destruct(absurd) 36 ] 37 qed. 21 38 22 39 lemma main_lemma_preinstruction: … … 477 494 try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*) 478 495 whd in match execute_1_preinstruction; normalize nodelta 479 [31,32: (* DJNZ *) 496 497 (* [31,32: (* DJNZ *) 480 498 (* XXX: work on the right hand side *) 481 499 >p normalize nodelta >p1 normalize nodelta … … 1049 1067 (* XXX: finally, prove the equality using sigma commutation *) 1050 1068 try @split_eq_status try % 1051 cases daemon 1052 10,42,43,44,45,49,52,56: (* MUL *) 1069 cases daemon *) 1070 [42,43,44,45,49,52,56: 1071 10: (* MUL *) 1053 1072 (* XXX: work on the right hand side *) 1054 1073 (* XXX: switch to the left hand side *) 1055 instr_refl>EQP P normalize nodelta1074 >EQP P normalize nodelta 1056 1075 #sigma_increment_commutation #maps_assm #fetch_many_assm %{1} 1076 whd in maps_assm:(??%%); 1077 inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1 1078 [2: normalize nodelta #absurd destruct(absurd) ] 1079 inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2 1080 [2: normalize nodelta #absurd destruct(absurd) ] 1081 normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl) 1057 1082 whd in ⊢ (??%?); 1058 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm whd in ⊢ (??%?); 1083 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm >EQs >EQticks <instr_refl 1084 change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status 1085 [2: 1086 whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f 1087 @sym_eq 1088 [1: 1089 @(get_8051_sfr_status_of_pseudo_status … policy) 1090 cases daemon (* XXX: need a lemma *) 1091 2: 1092 @(get_8051_sfr_status_of_pseudo_status M' … policy) 1093 @sym_eq @set_clock_status_of_pseudo_status [2: % ] 1094 @sym_eq @set_program_counter_status_of_pseudo_status % 1095 ] 1096 ] 1097 @sym_eq @set_8051_sfr_status_of_pseudo_status 1098 [2: 1099 >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1) 1100 @eq_f @eq_f2 try % @eq_f2 @eq_f 1101 @sym_eq 1102 [1: 1103 @(get_8051_sfr_status_of_pseudo_status … policy) 1104 cases daemon (* XXX: needs a lemma *) 1105 2: 1106 @(get_8051_sfr_status_of_pseudo_status M' … policy) 1107 @sym_eq @set_clock_status_of_pseudo_status [2: % ] 1108 @sym_eq @set_program_counter_status_of_pseudo_status % 1109 ] 1110 ] 1111 @sym_eq @set_clock_status_of_pseudo_status 1112 [2: 1113 @eq_f % 1114 ] 1115 @sym_eq @set_program_counter_status_of_pseudo_status % 1116 1059 1117 (* XXX: work on the left hand side *) 1060 1118 (* XXX: switch to the right hand side *)
Note: See TracChangeset
for help on using the changeset viewer.