Changeset 1967


Ignore:
Timestamp:
May 18, 2012, 11:48:36 AM (7 years ago)
Author:
sacerdot
Message:

Mov case completed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r1966 r1967  
    7575  ∀w, w': Word.
    7676  ∀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' #d
    84   cases daemon
     77   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 %
    8585qed.
    8686
     
    173173    |2:
    174174      @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: //
    183177      ]
    184178    ]
    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_status 
    191    
    192    
    193     #fetch_many_assm
    194     >assembly_refl in fetch_many_assm;
    195    
    196     cases (fetch ??) * #instr #newppc' #ticks normalize nodelta
    197     whd in ⊢ (??%?);   
    198    
    199    
    200       #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
    201       #H2
    202       whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
    203       %{1}
    204       lapply H2 -H2 whd in ⊢ (% → ??%?);
    205       cases (fetch ??) * #instr #newppc' #ticks normalize nodelta
    206       * * #H2a #H2b whd in ⊢ (% → ?); #H2c
    207 
    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 nodelta
    214       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; #ARG2
    220        normalize nodelta;
    221        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
    222        #result #flags
    223        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
    224 
    225 *)
    226179
    227180  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
Note: See TracChangeset for help on using the changeset viewer.