Ignore:
Timestamp:
Jul 31, 2012, 6:08:00 PM (8 years ago)
Author:
sacerdot
Message:

PUSH case almost finished

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2279 r2282  
    11571157      ]
    11581158    ]
    1159   |*)12: (* JC *)
     1159  |12: (* JC *)
    11601160    >EQP -P normalize nodelta
    11611161    whd in match assembly_1_pseudoinstruction; normalize nodelta
     
    19231923    cases bitone #bit_one_seven_bits_refl normalize nodelta
    19241924    [ @eq_bv_elim #seven_bits_refl normalize nodelta
    1925     | inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
     1925    | FUFFA inversion (lookup_from_internal_ram ??) normalize nodelta [2: #addr_entry]
    19261926      #lookup_from_internal_ram_refl ]
    1927     @Some_Some_elim #Mrefl destruct(Mrefl) #fetch_many_assm %{1}
     1927    @Some_Some_elim #Mrefl <Mrefl -M' #fetch_many_assm %{1}
    19281928    whd in ⊢ (??%?);
    19291929    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm
    1930     whd in ⊢ (??%?);
    1931     @pair_elim #carry #new_sp #carry_new_sp_refl normalize nodelta
    1932     @(pair_replace ?????????? (eq_to_jmeq … carry_new_sp_refl))
    1933     [1,3,5,7:
    1934       @eq_f2 try %
    1935       @(pose … (set_clock ????)) #status #status_refl
    1936       @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl -status_refl try %
    1937       @set_clock_status_of_pseudo_status >EQs >EQticks <instr_refl %
    1938     |*:
    1939       >EQs >EQticks <instr_refl
    1940       @(write_at_stack_pointer_status_of_pseudo_status 〈low,high,accA〉)
    1941       [2,4,6,8: @set_8051_sfr_status_of_pseudo_status try %
    1942       | >get_8051_sfr_set_8051_sfr
    1943         cut (new_sp = (add … (get_8051_sfr … ps SFR_SP) (bitvector_of_nat … 1)))
    1944         [ >(pair_destruct_2 ????? (sym_eq … carry_new_sp_refl))
    1945           change with (add ??? = ?); @eq_f2 try %
    1946           cases daemon (*CSC: use @get_8051_sfr_status_of_pseudo_status*) ] #EQnew_sp
    1947         >EQnew_sp
    1948         @internal_pseudo_address_map_equal_up_to_address_overwrite_or_delete_from_internal_ram
    1949        
    1950      
    1951          XXX
    1952         (*CSC: lemma here*)
    1953         cases accA
    1954         whd in match overwrite_or_delete_from_internal_ram; normalize nodelta
    1955         [ whd whd in match delete_from_internal_ram; normalize nodelta
    1956           @pair_elim #bit_one
    1957         |
    1958         ]
    1959       |
    1960       |
    1961       ]
     1930    whd in match execute_1_0; normalize nodelta
     1931    whd in match execute_1_preinstruction; normalize nodelta
     1932    >bit_one_seven_bits_refl
     1933    [ alias id "write_at_stack_pointer_accA" = "cic:/matita/cerco/ASM/Test3/write_at_stack_pointer_accA.def(29)".
     1934      >seven_bits_refl
     1935      @(write_at_stack_pointer_status_of_pseudo_status_accA … 〈low,high,accA〉)
     1936      [ @set_8051_sfr_status_of_pseudo_status >EQs >EQticks <instr_refl @(subaddressing_mode_elim … addr) #y
     1937        try %
     1938        change with (add ??? = ?); @eq_f2 try %
     1939        @(pose … (set_clock ????)) #status #status_refl
     1940        @sym_eq @(get_8051_sfr_status_of_pseudo_status … 〈low,high,accA〉 … status) >status_refl %
     1941      | >EQs /demod nohyps/ >add_commutative % ]
     1942    |
     1943    |
     1944    |
    19621945    ]
    19631946  |43: (* POP *)
Note: See TracChangeset for help on using the changeset viewer.