Changeset 835 for src/ASM/AssemblyProof.ma
- Timestamp:
- May 25, 2011, 11:06:59 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r834 r835 160 160 qed. 161 161 162 λticks_of.163 λs.164 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in165 let ticks ≝ ticks_of (program_counter ? s) in166 let s ≝ set_clock ? s (clock ? s + ticks) in167 let s ≝ set_program_counter ? s pc in168 let s ≝169 match instr with170 [ Instruction instr ⇒171 Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)172 | Comment cmt ⇒ Some PseudoStatus s173 | Cost cst ⇒ Some PseudoStatus s174 | 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 in177 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in178 let s ≝ set_8051_sfr ? s SFR_SP new_sp in179 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in180 let s ≝ write_at_stack_pointer ? s pc_bl in181 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in182 let s ≝ set_8051_sfr ? s SFR_SP new_sp in183 let s ≝ write_at_stack_pointer ? s pc_bu in184 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 in189 s.190 [2: % ]191 normalize192 @ I193 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) in203 let ticks ≝ ticks_of (program_counter ? s) in204 let s ≝ set_clock ? s (clock ? s + ticks) in205 let s ≝ set_program_counter ? s pc in206 let s ≝207 match instr with208 [ Instruction instr ⇒209 Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)210 | Comment cmt ⇒ Some PseudoStatus s211 | Cost cst ⇒ Some PseudoStatus s212 | 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 in215 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in216 let s ≝ set_8051_sfr ? s SFR_SP new_sp in217 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in218 let s ≝ write_at_stack_pointer ? s pc_bl in219 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in220 let s ≝ set_8051_sfr ? s SFR_SP new_sp in221 let s ≝ write_at_stack_pointer ? s pc_bu in222 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 in227 s.228 [2: % ]229 normalize230 @ I231 qed.232 162 233 163
Note: See TracChangeset
for help on using the changeset viewer.