Changeset 2279 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jul 30, 2012, 11:44:50 PM (7 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/Interpret.ma

    r2272 r2279  
    298298              set_8051_sfr … s SFR_ACC_A new_acc
    299299        | PUSH addr ⇒ λinstr_refl.
    300             match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → ? with
    301               [ DIRECT d ⇒ λdirect: True.
    302                 let s ≝ add_ticks1 s in
    303                 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    304                 let s ≝ set_8051_sfr … s SFR_SP new_sp in
    305                   write_at_stack_pointer … s d
    306               | _ ⇒ λother: False. ⊥
    307               ] (subaddressing_modein … addr)
     300            let s ≝ add_ticks1 s in
     301            let new_sp ≝ add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     302            let s ≝ set_8051_sfr … s SFR_SP new_sp in
     303             write_at_stack_pointer … s (get_arg_8 … s false addr)
    308304        | POP addr ⇒ λinstr_refl.
    309305            let s ≝ add_ticks1 s in
Note: See TracChangeset for help on using the changeset viewer.