Ignore:
Timestamp:
Jul 30, 2012, 11:44:50 PM (8 years ago)
Author:
sacerdot
Message:
  1. Bug fixed in the semantics of PUSH (no indirection performed)
  2. Proved write_at_stack_pointer_status_of_pseudo_status
  3. PUSH case of main lemma almost done
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProofSplit.ma

    r2278 r2279  
    1818include alias "ASM/Vector.ma".
    1919include "ASM/Test.ma".
     20include "ASM/Test2.ma".
    2021
    2122(*CSC: move elsewhere*)
     
    365366              set_8051_sfr … s SFR_ACC_A new_acc
    366367        | PUSH addr ⇒ λinstr_refl.
    367             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → ? with
    368               [ DIRECT d ⇒ λdirect: True. λEQaddr.
    369                 let s ≝ add_ticks1 s in
    370                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    371                 let s ≝ set_8051_sfr … s SFR_SP new_sp in
    372                   write_at_stack_pointer … s d
    373               | _ ⇒ λother: False. ⊥
    374               ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
     368            let s ≝ add_ticks1 s in
     369            let new_sp ≝ add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     370            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     371             write_at_stack_pointer … s (get_arg_8 … s false addr)
    375372        | POP addr ⇒ λinstr_refl.
    376373            let s ≝ add_ticks1 s in
     
    19411938    |*:
    19421939      >EQs >EQticks <instr_refl
    1943       cases daemon (* XXX: write_at_stack_pointer_status_of_pseudo_status *)
     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      ]
    19441962    ]
    19451963  |43: (* POP *)
Note: See TracChangeset for help on using the changeset viewer.