Changeset 2047 for src/ASM/AssemblyProofSplitSplit.ma
 Timestamp:
 Jun 12, 2012, 2:18:16 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplitSplit.ma
r2027 r2047 1 1 include "ASM/AssemblyProofSplit.ma". 2 include "common/LabelledObjects.ma". 3 4 check pseudo_instruction 5 6 definition instruction_has_label ≝ 7 λid: Identifier. 8 λi. 9 match i with 10 [ Jmp j ⇒ j = id 11  Call j ⇒ j = id 12  Instruction instr ⇒ 13 match instr with 14 [ JC j ⇒ j = id 15  JNC j ⇒ j = id 16  JZ j ⇒ j = id 17  JNZ j ⇒ j = id 18  JB _ j ⇒ j = id 19  JBC _ j ⇒ j = id 20  DJNZ _ j ⇒ j = id 21  CJNE _ j ⇒ j = id 22  _ ⇒ False 23 ] 24  _ ⇒ False 25 ]. 26 27 28 definition is_well_labelled_p ≝ 29 λinstr_list. 30 ∀id: Identifier. 31 ∀ppc. 32 ∀i. 33 fetch_pseudo_instruction instr_list ppc = i → 34 instruction_has_label id (\fst i) → 35 occurs_exactly_once ASMTag pseudo_instruction id instr_list. 2 36 3 37 theorem main_thm: 4 38 ∀M, M': internal_pseudo_address_map. 5 39 ∀program: pseudo_assembly_program. 40 ∀is_well_labelled: is_well_labelled_p (\snd program). 6 41 ∀sigma: Word → Word. 7 42 ∀policy: Word → bool. … … 13 48 status_of_pseudo_status M' … 14 49 (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy. 15 #M #M' * #preamble #instr_list # sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds50 #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds 16 51 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 17 52 @(pose … (program_counter ?? ps)) #ppc #EQppc … … 31 66 generalize in match assm1; assm1 assm2 assm3 32 67 normalize nodelta 33 casespi68 inversion pi 34 69 [2,3: 35 #arg 70 #arg #_ 36 71 (* XXX: we first work on sigma_increment_commutation *) 37 72 #sigma_increment_commutation … … 49 84 [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ] 50 85 6: (* Mov *) 51 #arg1 #arg2 86 #arg1 #arg2 #_ 52 87 (* XXX: we first work on sigma_increment_commutation *) 53 88 #sigma_increment_commutation … … 83 118 >set_arg_16_mk_Status_commutation in ⊢ (???%); 84 119 (* here we are *) 85 @split_eq_status //120 @split_eq_status try % 86 121 [1: 87 122 assumption 88 123 2: 89 @special_function_registers_8051_set_arg_16 90 [2: % 91 1: // 92 ] 124 @special_function_registers_8051_set_arg_16 % 93 125 ] 94 126 1: (* Instruction *) 95 pi #instr#EQP #EQnext #fetch_many_assm127 #instr #_ #EQP #EQnext #fetch_many_assm 96 128 @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness 97 129 ps ppc EQppc labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels … … 100 132 (refl …) ? (refl …)) 101 133 try assumption >assembly_refl <EQppc assumption 102 check status_of_pseudo_status103 134 4: 135 #arg1 #pi_refl 136 (* XXX: we first work on sigma_increment_commutation *) 137 whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?); 138 whd in match (expand_pseudo_instruction ??????); 139 (* generalize in match (refl … (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels (Jmp arg1))); 140 whd in match (expand_pseudo_instruction ??????) in ⊢ (??%? → % → ?); *) 141 inversion (sub_16_with_carry ???) #result #flags #sub16_refl normalize nodelta 142 inversion (vsplit ????) #upper #lower #vsplit_refl normalize nodelta 143 inversion (eq_bv ??? ∧ ¬ policy ?) #eq_bv_policy_refl normalize nodelta 144 [2: 145 inversion (vsplit ????) #fst_5_addr #rest_addr #addr_refl normalize nodelta 146 inversion (vsplit ????) #fst_5_pc #rest_pc #pc_refl normalize nodelta 147 cases (eq_bv ??? ∧ ¬ policy ?) normalize nodelta 148 ] 149 #sigma_increment_commutation 150 normalize in sigma_increment_commutation:(???(???(??%))); 151 (* XXX: we work on the maps *) 152 whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm 153 (* XXX: we assume the fetch_many hypothesis *) 154 * #fetch_refl #fetch_many_assm 155 (* XXX: we give the existential *) 156 %{1} 157 (* XXX: work on the left hand side of the equality *) 158 whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc 159 (* XXX: execute fetches some more *) 160 whd in match code_memory_of_pseudo_assembly_program; normalize nodelta 161 whd in fetch_many_assm; 162 >EQassembled in fetch_refl; #fetch_refl <fetch_refl fetch_refl 163 lapply (eq_bv_eq … fetch_many_assm) fetch_many_assm #EQnewpc 164 whd in ⊢ (??%%); 165 (* XXX: now we start to work on the mk_PreStatus equality *) 166 (* XXX: lhs *) 167 (* XXX: rhs *) 168 (* here we are *) 169 @split_eq_status try % /demod nohyps/ 170 [1,3,4: 171 change with (add ???) in match (\snd (half_add ???)); 172 whd in match execute_1_pseudo_instruction0; normalize nodelta 173 /demod nohyps/ >set_clock_set_program_counter 174 >program_counter_set_program_counter 175 whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta 176 lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl 177 normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm 178 [1: 179 address_of_word_labels_assm >EQnewpc >pc_refl normalize nodelta 180 >(pair_destruct_2 ????? (sym_eq … addr_refl)) 181 >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc 182 (* XXX: true but needs lemma about splitting *) 183 cases daemon 184 3: 185 >EQnewpc >pc_refl normalize nodelta 186 >(pair_destruct_2 ????? (sym_eq … addr_refl)) 187 >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc 188 >EQlookup_labels normalize nodelta 189 >address_of_word_labels_assm try % 190 5: 191 >EQnewpc 192 ] 193 @(is_well_labelled_witness … fetch_pseudo_refl) 194 >pi_refl % 195 2: 196 whd in match compute_target_of_unconditional_jump; normalize nodelta 197 >program_counter_set_program_counter 198 cases (vsplit ????) #pc_bu #pc_bl normalize nodelta 199 cases (vsplit ????) #nu #nl normalize nodelta 200 cases (vsplit ????) #relevant1 #relevant2 normalize nodelta 201 change with (add ???) in match (\snd (half_add ???)); >EQnewpc 202 cases daemon 203 3: 204 whd in ⊢ (??%%); 205 /demod nohyps/ 206 cases daemon 207 ] 208 5: (* Call *) 104 209 #arg1 105 210 (* XXX: we first work on sigma_increment_commutation *) … … 119 224 whd in fetch_many_assm; 120 225 >EQassembled in fetch_many_assm; 121 cases (fetch ??) * #instr #newpc # ticks normalize nodelta *226 cases (fetch ??) * #instr #newpc #?ticks normalize nodelta * 122 227 #eq_instr 123 228 #fetch_many_assm whd in fetch_many_assm; … … 145 250 ] 146 251 ] 147 5: cases daemon148 252 ] 149 253 qed.
Note: See TracChangeset
for help on using the changeset viewer.