Changeset 1511 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Nov 16, 2011, 5:35:24 PM (8 years ago)
Author:
mulligan
Message:

proofs, added, changes to execute_1_0 function therefore required to remove excess lets

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r1494 r1511  
    545545          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    546546            [ ADDR11 a ⇒ λaddr11: True.
    547               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     547              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    548548              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    549               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     549              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
     550              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
    550551              let s ≝ write_at_stack_pointer ? s pc_bl in
    551               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     552              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    552553              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    553554              let s ≝ write_at_stack_pointer ? s pc_bu in
    554               let 〈thr, eig〉 ≝ split ? 3 8 a in
    555               let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in
     555              let thr ≝ \fst (split ? 3 8 a) in
     556              let eig ≝ \snd (split ? 3 8 a) in
     557              let fiv ≝ \fst (split ? 5 3 pc_bu) in
     558              let thr' ≝ \snd (split ? 5 3 pc_bu) in
    556559              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    557560                set_program_counter ? s new_addr
     
    562565          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → ? with
    563566            [ ADDR16 a ⇒ λaddr16: True.
    564               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     567              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    565568              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    566               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     569              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
     570              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
    567571              let s ≝ write_at_stack_pointer ? s pc_bl in
    568               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     572              let new_sp ≝ \snd (half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1)) in
    569573              let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    570574              let s ≝ write_at_stack_pointer ? s pc_bu in
     
    596600          let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ? s SFR_DPL) in
    597601          let big_acc ≝ (zero 8) @@ (get_8051_sfr ? s SFR_ACC_A) in
    598           let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in
    599           let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) jmp_addr in
     602          let jmp_addr ≝ \snd (half_add ? big_acc dptr) in
     603          let new_pc ≝ \snd (half_add ? (program_counter ? s) jmp_addr) in
    600604            set_program_counter ? s new_pc
    601605        | LJMP addr ⇒
     
    610614          match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → ? with
    611615            [ RELATIVE r ⇒ λrelative: True.
    612                 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) (sign_extension r) in
     616                let new_pc ≝ \snd (half_add ? (program_counter ? s) (sign_extension r)) in
    613617                  set_program_counter ? s new_pc
    614618            | _ ⇒ λother: False. ⊥
     
    618622          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → ? with
    619623            [ ADDR11 a ⇒ λaddr11: True.
    620               let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    621               let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in
     624              let pc_bu ≝ \fst (split ? 8 8 (program_counter ? s)) in
     625              let pc_bl ≝ \snd (split ? 8 8 (program_counter ? s)) in
     626              let nu ≝ \fst (split ? 4 4 pc_bu) in
     627              let nl ≝ \snd (split ? 4 4 pc_bu) in
    622628              let bit ≝ get_index' ? O ? nl in
    623               let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in
     629              let relevant1 ≝ \fst (split ? 3 8 a) in
     630              let relevant2 ≝ \snd (split ? 3 8 a) in
    624631              let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in
    625               let 〈carry, new_pc〉 ≝ half_add ? (program_counter ? s) new_addr in
     632              let new_pc ≝ \snd (half_add ? (program_counter ? s) new_addr) in
    626633                set_program_counter ? s new_pc
    627634            | _ ⇒ λother: False. ⊥
Note: See TracChangeset for help on using the changeset viewer.