- Timestamp:
- Jun 28, 2012, 6:47:26 PM (9 years ago)
- Location:
- src/ASM
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProofSplit.ma
r2139 r2140 403 403 status_of_pseudo_status M' cm s sigma policy). 404 404 P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s). 405 (* XXX: takes about 45 minutes to type check! *) 405 406 #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy 406 407 #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels -
src/ASM/AssemblyProofSplitSplit.ma
r2139 r2140 150 150 |6: 151 151 >assembly_refl assumption 152 |7: 153 <EQassembled assumption 152 154 ] 153 155 |4: (* Jmp *) … … 264 266 cases daemon 265 267 |3: 266 whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl 267 >EQlookup_labels normalize nodelta 268 @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl normalize nodelta 269 <EQnewpc @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta 270 #relevant 271 lapply pc_bu_bl_refl' -pc_bu_bl_refl' 272 >program_counter_set_8051_sfr >set_clock_set_program_counter 273 >program_counter_set_program_counter >fst_5_rest_pc_refl 274 cut(fst_5_addr = fst_5_pc) 275 [1: 276 cases daemon (* XXX: !! *) 277 |2: 278 #relevant2 >relevant2 268 lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta 269 change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??); 270 #relevant <(relevant arg1) 271 [2: 272 @(is_well_labelled_witness … ppc_in_bounds pi) 273 [1: 274 >fetch_pseudo_refl % 275 |2: 276 >pi_refl % 277 ] 278 |1: 279 whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl 280 >EQlookup_labels normalize nodelta 281 @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl 282 >fst_5_rest_refl normalize nodelta 283 @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta 284 #pair_true_refl destruct(pair_true_refl) 285 <EQnewpc in fst_5_rest_pc_refl; 286 lapply pc_bu_bl_refl' -pc_bu_bl_refl' 287 >program_counter_set_8051_sfr >set_clock_set_program_counter 288 >program_counter_set_program_counter #relevant2 289 <(vsplit_ok ?????? (sym_eq … relevant2)) 279 290 <(vsplit_ok ?????? (sym_eq … fiv_thr_refl')) 280 #relevant3 281 lapply(vsplit_ok ?????? (sym_eq … relevant3)) 282 >(vector_associative_append bool 5 3 8) #relevant4 283 cut(fiv = fst_5_pc ∧ thr'@@pc_bl' = rest_pc) 291 >(vector_associative_append bool 5 3 8) #relevant3 292 >(? : fiv = fst_5_addr) 284 293 [1: 285 cases daemon (* XXX: !! *)294 % 286 295 |2: 287 * #relevant5 #relevant6 >relevant5 288 >(vector_associative_append bool 5 3 8) @eq_f 289 destruct(relevant) 290 <(vsplit_ok ?????? (sym_eq … thr_eig_refl)) @eq_f 296 cases daemon 291 297 ] 292 ] *)298 ] 293 299 |4: 294 300 >set_program_counter_mk_Status_commutation in ⊢ (???%); … … 308 314 [1: // 309 315 |2: 310 normalize in match (assembly1 ?); >thr_eig_refl311 @(bitvector_3_elim_prop … thr) %316 normalize in match (assembly1 ?); 317 @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 offset))) % 312 318 |3: 313 319 #fetch_2_refl >fetch_2_refl >commutative_plus % 314 320 ] 321 ] 322 |2: 323 @(pair_replace ????? carry new_sp ??? carry_new_sp_refl) 324 try /demod nohyps/ [1: %] 325 @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl' 326 @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl') 327 try /demod nohyps/ [1: %] 328 @split_eq_status try /demod nohyps/ try % 329 [1: 330 cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl)) 331 [1: 332 >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) /demod nohyps/ 333 >set_clock_set_program_counter >program_counter_set_program_counter 334 >add_commutative >EQnewpc @eq_f @sym_eq @(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl)) 335 |2: 336 #relevant cases daemon 337 (* XXX: need axioms *) 338 ] 315 339 |2: 340 cases daemon (* XXX: need axioms from assembly.ma *) 341 |3: 342 change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??); 343 lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta 344 #relevant <(relevant arg1) 345 [1: 346 >EQlookup_labels % 347 |2: 348 @(is_well_labelled_witness … ppc_in_bounds pi) 349 [1: 350 >fetch_pseudo_refl % 351 |2: 352 >pi_refl % 353 ] 354 ] 355 |4: 356 >set_program_counter_mk_Status_commutation in ⊢ (???%); 357 >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%); 358 (* XXX: require set_8051_sfr_write_at_stack_pointer and 359 special_function_registers_8051_set_8051_sfr 360 *) 361 cases daemon 362 |5,6,7: 363 >set_program_counter_mk_Status_commutation in ⊢ (???%); 364 (* XXX: similar to above but for 8052 365 *) 366 cases daemon 316 367 ] 317 368 ] 318 369 ] 319 ]320 370 qed.
Note: See TracChangeset
for help on using the changeset viewer.