Changeset 1967
 Timestamp:
 May 18, 2012, 11:48:36 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r1966 r1967 75 75 ∀w, w': Word. 76 76 ∀d, d': [[dptr]]. 77 (∀sfr: SFR8051.78 sfr ≠ SFR_DPH → sfr ≠ SFR_DPL→79 get_8051_sfr M cm s sfr = get_8051_sfr M' cm' s' sfr) →80 w = w' →81 special_function_registers_8051 ?? (set_arg_16 … s w d) =82 special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').83 #M #M' #cm #cm' #s #s' #w #w' #d84 cases daemon77 special_function_registers_8051 ?? s = special_function_registers_8051 … s' → 78 w = w' → 79 special_function_registers_8051 ?? (set_arg_16 … s w d) = 80 special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d'). 81 #M #M' #cm #cm' #s #s' #w #w' 82 @list_addressing_mode_tags_elim_prop try % 83 @list_addressing_mode_tags_elim_prop try % 84 #EQ1 #EQ2 <EQ2 normalize cases (split bool 8 8 w) #b1 #b2 normalize <EQ1 % 85 85 qed. 86 86 … … 173 173 2: 174 174 @special_function_registers_8051_set_arg_16 175 [2: 176 >EQlookup_datalabels % 177 1: 178 * 179 #absurd1 #absurd2 180 try (@⊥ cases absurd1 absurd #absurd1 @absurd1 %) 181 try (@⊥ cases absurd2 absurd #absurd2 @absurd2 %) 182 whd in ⊢ (??%%); cases daemon (* XXX: not nice! manipulation of vectors; true though *) 175 [2: >EQlookup_datalabels % 176 1: // 183 177 ] 184 178 ] 185 186 (*187 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1 whd in ⊢ (??%?);188 whd in match (get_arg_16 ????); whd in match (set_arg_16' ?????);189 190 @split_eq_status191 192 193 #fetch_many_assm194 >assembly_refl in fetch_many_assm;195 196 cases (fetch ??) * #instr #newppc' #ticks normalize nodelta197 whd in ⊢ (??%?);198 199 200 #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;201 #H2202 whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP203 %{1}204 lapply H2 H2 whd in ⊢ (% → ??%?);205 cases (fetch ??) * #instr #newppc' #ticks normalize nodelta206 * * #H2a #H2b whd in ⊢ (% → ?); #H2c207 208 CSC: XXX (I am porting the code below)209 210 whd in match (execute_1_pseudo_instruction0 ?????);211 %{1}212 whd in ⊢ (??%?);213 cases (fetch ??) * #instr #newppc' #ticks normalize nodelta214 whd in ⊢ (??%?);215 216 >H2b >(eq_instruction_to_eq … H2a)217 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?);218 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; whd in ⊢ (???% → ??%?)219 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG2220 normalize nodelta;221 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)]222 #result #flags223 #EQ >EQ EQ; normalize nodelta; >(eq_bv_eq … H2c) %224 225 *)226 179 227 180 4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
Note: See TracChangeset
for help on using the changeset viewer.