Changeset 2129 for src/ASM/Interpret.ma


Ignore:
Timestamp:
Jun 27, 2012, 7:14:32 PM (7 years ago)
Author:
mulligan
Message:

Large changes from today trying to complete the main theorem. Again :(

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Interpret.ma

    r2124 r2129  
    10721072          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
    10731073            [ ADDR11 a ⇒ λaddr11: True.
     1074              «let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1075              let s ≝ set_8051_sfr … s SFR_SP new_sp in
     1076              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
     1077              let s ≝ write_at_stack_pointer … s pc_bl in
     1078              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
     1079              let s ≝ set_8051_sfr … s SFR_SP new_sp in
     1080              let s ≝ write_at_stack_pointer … s pc_bu in
     1081              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
     1082              let new_addr ≝ fiv @@ a in
     1083                set_program_counter … s new_addr, ?»
     1084            | _ ⇒ λother: False. ⊥
     1085            ] (subaddressing_modein … addr)
     1086      | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
     1087      | LCALL addr ⇒ λinstr_refl.
     1088          let s ≝ set_clock ?? s (ticks + clock … s) in
     1089          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
     1090            [ ADDR16 a ⇒ λaddr16: True.
     1091              «
    10741092              let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    10751093              let s ≝ set_8051_sfr … s SFR_SP new_sp in
     
    10791097              let s ≝ set_8051_sfr … s SFR_SP new_sp in
    10801098              let s ≝ write_at_stack_pointer … s pc_bu in
    1081               let 〈thr, eig〉 ≝ vsplit ? 3 8 a in
    1082               let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
    1083               let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    1084                 set_program_counter … s new_addr
    1085             | _ ⇒ λother: False. ⊥
    1086             ] (subaddressing_modein … addr)
    1087       | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
    1088       | LCALL addr ⇒ λinstr_refl.
    1089           let s ≝ set_clock ?? s (ticks + clock … s) in
    1090           match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
    1091             [ ADDR16 a ⇒ λaddr16: True.
    1092               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    1093               let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1094               let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
    1095               let s ≝ write_at_stack_pointer … s pc_bl in
    1096               let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
    1097               let s ≝ set_8051_sfr … s SFR_SP new_sp in
    1098               let s ≝ write_at_stack_pointer … s pc_bu in
    1099                 set_program_counter … s a
     1099                set_program_counter … s a, ?»
    11001100            | _ ⇒ λother: False. ⊥
    11011101            ] (subaddressing_modein … addr)
     
    11061106    try //
    11071107    -s destruct(INSTR_PC) <instr_refl whd
    1108     try (#absurd normalize in absurd; try destruct(absurd) try %) %
     1108    try (#absurd normalize in absurd; try destruct(absurd) try %)
     1109    @pair_elim #carry #new_sp #carry_new_sp_refl
     1110    @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl
     1111    @pair_elim #carry' #new_sp' #carry_new_sp_refl'
     1112    [2:
     1113      /demod nohyps/ %
     1114    |1:
     1115      cases (vsplit ????) #thr #eig normalize nodelta
     1116      cases (vsplit ????) #fiv #thr' normalize nodelta
     1117      /demod by clock_set_program_counter/ /demod nohyps/ %
     1118    ]
    11091119  |9:
    11101120    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
Note: See TracChangeset for help on using the changeset viewer.