Changeset 2285
 Timestamp:
 Aug 2, 2012, 1:58:14 PM (7 years ago)
 Location:
 src/ASM
 Files:

 3 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProofSplit.ma
r2284 r2285 2394 2394 *: >EQs /demod nohyps/ >add_commutative % ] 2395 2395 43: (* POP *) 2396 cases daemon 2396 *: cases daemon ] 2397 >EQP P normalize nodelta lapply instr_refl 2398 @(subaddressing_mode_elim … addr) #w #instr_refl normalize nodelta 2399 #sigma_increment_commutation 2400 whd in ⊢ (??%? → ?); 2401 @vsplit_elim #bit_one #seven_bits 2402 cases (Vector_Sn … bit_one) #bitone * #empty >(Vector_O … empty) #H >H bit_one 2403 cases bitone #bit_one_seven_bits_refl normalize nodelta 2404 [ @eq_bv_elim #seven_bits_refl normalize nodelta 2405 [2: inversion (lookup_from_internal_ram ??) normalize nodelta 2406 [2: #x #_ #abs destruct(abs)] #lookup_from_internal_ram_refl]] 2407 @Some_Some_elim #Mrefl <Mrefl M' #fetch_many_assm %{1} 2408 whd in ⊢ (??%?); 2409 <(fetch_many_singleton … fetch_many_assm) fetch_many_assm 2410 whd in match execute_1_0; normalize nodelta 2411 whd in match execute_1_preinstruction; normalize nodelta 2412 @(pair_replace ?????????? p) >p normalize nodelta 2413 >bit_one_seven_bits_refl 2414 [1,3,5: <p @eq_f3 try % 2415 @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … s) try % 2416 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl try % 2417 @eq_f2 try % @(subaddressing_mode_elim … addr) #y % 2418 2: @set_arg_8_status_of_pseudo_status try % 2419 [1: @set_8051_sfr_status_of_pseudo_status try % 2420 @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl try % 2421 @eq_f2 try % @(subaddressing_mode_elim … addr) #y % 2422  whd in ⊢ (??%?); 2423 inversion (sfr_of_Byte ?) normalize nodelta 2424 [ #sfr_of_Byte_refl (*CSC: needs >read_at_stack_pointer_set_clock*) cases daemon 2425  * normalize nodelta * #sfr_of_Byte_refl 2426 [18: @⊥ @(absurd ?? seven_bits_refl) >bit_one_seven_bits_refl 2427 @eq_sfr_of_Byte_accA_to_eq assumption 2428 *: change with (read_at_stack_pointer ??? = ?) 2429 cases daemon (*CSC: needs >read_at_stack_pointer_set_clock*)]]] 2430 3: 2431 4: 2432 XXX 2433 ] 2397 2434 44: 2398 2435 >EQP P normalize nodelta 
src/ASM/StatusProofs.ma
r2272 r2285 68 68 lemma get_8051_sfr_set_program_counter: 69 69 ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s. 70 // 71 qed. 72 73 lemma get_8051_sfr_set_clock: 74 ∀T,cm,s,pc. get_8051_sfr T cm (set_clock … s pc) = get_8051_sfr … s. 70 75 // 71 76 qed. 
src/ASM/StatusProofsSplit.ma
r2274 r2285 64 64 c. 65 65 // 66 qed.67 68 lemma get_8051_sfr_set_clock:69 ∀M: Type[0].70 ∀cm: M.71 ∀s: PreStatus M cm.72 ∀sfr: SFR8051.73 ∀t: Time.74 get_8051_sfr M cm (set_clock M cm s t) sfr =75 get_8051_sfr M cm s sfr.76 #M #cm #s #sfr #t %77 qed.78 79 lemma get_8051_sfr_set_program_counter:80 ∀M: Type[0].81 ∀cm: M.82 ∀s: PreStatus M cm.83 ∀pc: Word.84 get_8051_sfr M cm (set_program_counter M cm s pc) =85 get_8051_sfr M cm s.86 #M #cm #s #pc %87 66 qed. 88 67
Note: See TracChangeset
for help on using the changeset viewer.