Changeset 835


Ignore:
Timestamp:
May 25, 2011, 11:06:59 AM (8 years ago)
Author:
sacerdot
Message:

Old experiments removed.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r834 r835  
    160160qed.
    161161
    162   λticks_of.
    163   λs.
    164   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    165   let ticks ≝ ticks_of (program_counter ? s) in
    166   let s ≝ set_clock ? s (clock ? s + ticks) in
    167   let s ≝ set_program_counter ? s pc in
    168   let s ≝
    169     match instr with
    170     [ Instruction instr ⇒
    171        Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
    172     | Comment cmt ⇒ Some PseudoStatus s
    173     | Cost cst ⇒ Some PseudoStatus s
    174     | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
    175     | Call call ⇒
    176       let a ≝ address_of_word_labels s call in
    177       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    178       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    179       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    180       let s ≝ write_at_stack_pointer ? s pc_bl in
    181       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    182       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    183       let s ≝ write_at_stack_pointer ? s pc_bu in
    184         Some PseudoStatus (set_program_counter ? s a)
    185     | Mov dptr ident ⇒
    186        Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
    187     ]
    188   in
    189     s.
    190   [2: % ]
    191   normalize
    192   @ I
    193 qed.
    194 
    195 
    196 
    197 definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
    198  {{ ps':PseudoStatus | code_memory … ps = code_memory … ps' }
    199 
    200   λticks_of.
    201   λs.
    202   let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
    203   let ticks ≝ ticks_of (program_counter ? s) in
    204   let s ≝ set_clock ? s (clock ? s + ticks) in
    205   let s ≝ set_program_counter ? s pc in
    206   let s ≝
    207     match instr with
    208     [ Instruction instr ⇒
    209        Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
    210     | Comment cmt ⇒ Some PseudoStatus s
    211     | Cost cst ⇒ Some PseudoStatus s
    212     | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
    213     | Call call ⇒
    214       let a ≝ address_of_word_labels s call in
    215       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    216       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    217       let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
    218       let s ≝ write_at_stack_pointer ? s pc_bl in
    219       let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
    220       let s ≝ set_8051_sfr ? s SFR_SP new_sp in
    221       let s ≝ write_at_stack_pointer ? s pc_bu in
    222         Some PseudoStatus (set_program_counter ? s a)
    223     | Mov dptr ident ⇒
    224        Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
    225     ]
    226   in
    227     s.
    228   [2: % ]
    229   normalize
    230   @ I
    231 qed.
    232162
    233163
Note: See TracChangeset for help on using the changeset viewer.