Ignore:
Timestamp:
May 24, 2011, 11:19:53 PM (8 years ago)
Author:
sacerdot
Message:

Bug fixed to make the file compile.
But the type of the assembly function is no more right.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r832 r833  
    7979           (clock … ps)) ].
    8080
     81(* RUSSEL **)
     82
     83include "basics/jmeq.ma".
     84
     85definition inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ λA,P,a,p. dp … a p.
     86definition eject : ∀A.∀P: A → Prop.(Σx:A.P x) → A ≝ λA,P,c.match c with [ dp w p ⇒ w].
     87
     88coercion inject : ∀A.∀P:A → Prop.∀a.∀p:P a.Σx:A.P x ≝ inject on a:? to Σx:?.?.
     89coercion eject : ∀A.∀P:A → Prop.∀c:Σx:A.P x.A ≝ eject on _c:Σx:?.? to ?.
     90
     91(* END RUSSELL **)
     92
     93definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
     94 Σps':PseudoStatus.(code_memory … ps = code_memory … ps')
     95
     96  λticks_of.
     97  λs.
     98  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
     99  let ticks ≝ ticks_of (program_counter ? s) in
     100  let s ≝ set_clock ? s (clock ? s + ticks) in
     101  let s ≝ set_program_counter ? s pc in
     102  let s ≝
     103    match instr with
     104    [ Instruction instr ⇒
     105       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
     106    | Comment cmt ⇒ Some PseudoStatus s
     107    | Cost cst ⇒ Some PseudoStatus s
     108    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
     109    | Call call ⇒
     110      let a ≝ address_of_word_labels s call in
     111      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     112      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     113      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     114      let s ≝ write_at_stack_pointer ? s pc_bl in
     115      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     116      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     117      let s ≝ write_at_stack_pointer ? s pc_bu in
     118        Some PseudoStatus (set_program_counter ? s a)
     119    | Mov dptr ident ⇒
     120       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
     121    ]
     122  in
     123    s.
     124 [
     125 |2,3,4: %
     126 | whd % 
     127
     128  λticks_of.
     129  λs.
     130  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
     131  let ticks ≝ ticks_of (program_counter ? s) in
     132  let s ≝ set_clock ? s (clock ? s + ticks) in
     133  let s ≝ set_program_counter ? s pc in
     134  let s ≝
     135    match instr with
     136    [ Instruction instr ⇒
     137       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
     138    | Comment cmt ⇒ Some PseudoStatus s
     139    | Cost cst ⇒ Some PseudoStatus s
     140    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
     141    | Call call ⇒
     142      let a ≝ address_of_word_labels s call in
     143      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     144      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     145      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     146      let s ≝ write_at_stack_pointer ? s pc_bl in
     147      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     148      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     149      let s ≝ write_at_stack_pointer ? s pc_bu in
     150        Some PseudoStatus (set_program_counter ? s a)
     151    | Mov dptr ident ⇒
     152       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
     153    ]
     154  in
     155    s.
     156  [2: % ]
     157  normalize
     158  @ I
     159qed.
     160
     161
     162
     163definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
     164 {{ ps':PseudoStatus | code_memory … ps = code_memory … ps' }
     165
     166  λticks_of.
     167  λs.
     168  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
     169  let ticks ≝ ticks_of (program_counter ? s) in
     170  let s ≝ set_clock ? s (clock ? s + ticks) in
     171  let s ≝ set_program_counter ? s pc in
     172  let s ≝
     173    match instr with
     174    [ Instruction instr ⇒
     175       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
     176    | Comment cmt ⇒ Some PseudoStatus s
     177    | Cost cst ⇒ Some PseudoStatus s
     178    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
     179    | Call call ⇒
     180      let a ≝ address_of_word_labels s call 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 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
     184      let s ≝ write_at_stack_pointer ? s pc_bl in
     185      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
     186      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
     187      let s ≝ write_at_stack_pointer ? s pc_bu in
     188        Some PseudoStatus (set_program_counter ? s a)
     189    | Mov dptr ident ⇒
     190       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
     191    ]
     192  in
     193    s.
     194  [2: % ]
     195  normalize
     196  @ I
     197qed.
     198
     199
    81200
    82201lemma execute_code_memory_unchanged:
     
    94213       cases (split ????) #z1 #z2 %
    95214     | #a1 whd in ⊢ (??? (??%)) cases a1 #x #H whd in ⊢ (??? (??%)) cases x
     215       [ #x1 whd in ⊢ (??? (??%))
    96216     | *: cases not_implemented
    97217     ]
Note: See TracChangeset for help on using the changeset viewer.