Changeset 2269
- Timestamp:
- Jul 26, 2012, 3:29:15 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplitSplit.ma
r2267 r2269 51 51 qed. 52 52 53 (*CSC: move elsewhere*) 54 lemma bv_append_eq_to_eq: 55 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m. 56 v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4. 57 #A #n #v1 elim v1 58 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %% 59 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2 60 #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ] 61 qed. 62 53 63 theorem main_thm: 54 64 ∀M, M': internal_pseudo_address_map. … … 102 112 %{0} 103 113 whd in match execute_1_pseudo_instruction0; normalize nodelta 104 change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ??? 105 whd in match (execute_1_pseudo_instruction0 ?????); 106 (* XXX: work on the left hand side of the equality *) 107 whd in ⊢ (??%?); 108 @split_eq_status try % 109 /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *) 114 change with (status_of_pseudo_status ????? = ?) 115 whd in ⊢ (??%%); @split_eq_status try % 116 [ >set_clock_set_program_counter ] 117 >program_counter_set_program_counter >sigma_increment_commutation @add_zero 110 118 |6: (* Mov *) 111 119 #arg1 #arg2 #_ … … 206 214 whd in match (expand_pseudo_instruction ??????); 207 215 whd in match (execute_1_pseudo_instruction0 ?????); 216 whd in match (ticks_of0 ??????); 208 217 inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta 209 218 inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta … … 231 240 [1: 232 241 @(pair_replace ????? carry new_sp ??? carry_new_sp_refl) 233 [ @eq_f2 try % 234 cases daemon (*CSC*) 242 [ @eq_f2 try % @sym_eq 243 @(pose … (set_clock ????)) #status #status_refl @sym_eq >status_refl 244 /demod nohyps/ 245 (*CSC: mess with get_8051_sfr_set_program_counter + missing high level lemmas*) 246 cut (∀A,B:Type[0]. ∀f,g:A → B. ∀a:A. f=g → f a = g a) [#A #B #f #f #a * %] #eq_fun 247 >(eq_fun ???? ? (get_8051_sfr_set_program_counter (BitVectorTrie Byte 16) … SFR_SP …)) 248 >(eq_fun ???? ? (get_8051_sfr_set_program_counter pseudo_assembly_program … SFR_SP …)) 249 whd in match get_8051_sfr; normalize nodelta whd in match status_of_pseudo_status; 250 normalize nodelta whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta 251 cases accM try % normalize nodelta #ul #addr cases (vsplit bool ???) 252 normalize nodelta #v1 #v2 cases (eq_upper_lower ul upper) normalize nodelta 253 >get_index_v_set_index_miss try % #abs normalize in abs; destruct(abs) 235 254 ] whd in ⊢ (??%?); 236 255 @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl' 237 256 @(pair_replace ????? ?? ??? carry_new_sp_refl') 238 [ @eq_f2 try % 239 cases daemon (*CSC*) 257 [ @eq_f2 try % @sym_eq 258 @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq 259 @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try % 260 @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*) 240 261 ] 241 262 whd in ⊢ (??%?); … … 243 264 change with (set_program_counter ???? = ?) 244 265 @set_program_counter_status_of_pseudo_status 245 [2: @sym_eq cases daemon (* @write_at_stack_pointer_status_of_pseudo_status try %266 [2: @sym_eq cases daemon (*CSC: missing @write_at_stack_pointer_status_of_pseudo_status try % 246 267 [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try % 247 268 @sigma_increment_commutation … … 263 284 [1: <fst_5_rest_refl whd in match address_of_word_labels; normalize nodelta 264 285 >create_label_cost_refl % 265 |2: 266 cases daemon (*CSC: make a lemma here!*)267 ]286 |2: cases (bv_append_eq_to_eq … relevant3) #H #_ >H 287 cases (conjunction_true … aj_possible_refl) #K #_ @sym_eq 288 @eq_bv_eq assumption ] 268 289 | @(pair_replace ????? carry new_sp ??? carry_new_sp_refl) 269 [ @eq_f2 try % cases daemon ] 290 [ @eq_f2 try % 291 @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq 292 @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) 293 >status_refl -status_refl try % 294 @sym_eq @set_clock_status_of_pseudo_status try % 295 @sym_eq @set_program_counter_status_of_pseudo_status try % assumption ] 270 296 @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl' 271 297 @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl') 272 [ @eq_f2 try % cases daemon ] 298 [ @eq_f2 try % @sym_eq 299 @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq 300 @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try % 301 @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*) ] 273 302 change with (set_program_counter ???? = ?) 274 303 @set_program_counter_status_of_pseudo_status … … 284 313 >program_counter_set_8051_sfr >set_clock_set_program_counter 285 314 >program_counter_set_program_counter assumption ] #sigma_pc_bu_pc_bl_refl 286 @sym_eq 315 @sym_eq (*CSC: write_at_stack_pointer_status_of_pseudo_status*) 287 316 cases daemon 288 317 ]
Note: See TracChangeset
for help on using the changeset viewer.