Changeset 2272 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jul 27, 2012, 5:53:25 PM (7 years ago)
Author:
mulligan
Message:

Changed proof strategy for main lemma after noticed that the current approach would not work with POP, RET, etc. Ported throughout the assembly proof and all the way up to Test.ma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2264 r2272  
    727727                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    728728                let s ≝ set_8051_sfr … s SFR_SP new_sp in
    729                   write_at_stack_pointer … s d
     729                  write_at_stack_pointer ?? s (get_arg_8 ?? s false (DIRECT … d))
    730730              | _ ⇒ λother: False. ⊥
    731731              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
Note: See TracChangeset for help on using the changeset viewer.