Changeset 2285


Ignore:
Timestamp:
Aug 2, 2012, 1:58:14 PM (7 years ago)
Author:
sacerdot
Message:
  1. duplicated code erased
  2. POP case finished up to lemmas on read_at_stack_pointer
Location:
src/ASM
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2284 r2285  
    23942394    |*: >EQs /demod nohyps/ >add_commutative % ]
    23952395  |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    ]
    23972434  |44:
    23982435    >EQP -P normalize nodelta
  • src/ASM/StatusProofs.ma

    r2272 r2285  
    6868lemma get_8051_sfr_set_program_counter:
    6969 ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s.
     70 //
     71qed.
     72
     73lemma get_8051_sfr_set_clock:
     74 ∀T,cm,s,pc. get_8051_sfr T cm (set_clock … s pc) = get_8051_sfr … s.
    7075 //
    7176qed.
  • src/ASM/StatusProofsSplit.ma

    r2274 r2285  
    6464        c.
    6565  //
    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 %
    8766qed.
    8867
Note: See TracChangeset for help on using the changeset viewer.