Changeset 835 for src/ASM/AssemblyProof.ma

Timestamp:

May 25, 2011, 11:06:59 AM (10 years ago)

Author:

sacerdot

Message:

Old experiments removed.

File:

• src/ASM/AssemblyProof.ma (modified) (1 diff)

src/ASM/AssemblyProof.ma

@@ -160 +160 @@
 qed.
 
-  λticks_of.
-  λs.
-  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
-  let ticks ≝ ticks_of (program_counter ? s) in
-  let s ≝ set_clock ? s (clock ? s + ticks) in
-  let s ≝ set_program_counter ? s pc in
-  let s ≝
-    match instr with
-    [ Instruction instr ⇒
-       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
-    | Comment cmt ⇒ Some PseudoStatus s
-    | Cost cst ⇒ Some PseudoStatus s
-    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
-    | Call call ⇒
-      let a ≝ address_of_word_labels s call in
-      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
-      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
-      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
-      let s ≝ write_at_stack_pointer ? s pc_bl in
-      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
-      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
-      let s ≝ write_at_stack_pointer ? s pc_bu in
-        Some PseudoStatus (set_program_counter ? s a)
-    | Mov dptr ident ⇒
-       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
-    ]
-  in
-    s.
-  [2: % ]
-  normalize
-  @ I
-qed.
-
-
-
-definition execute_1_pseudo_instruction': (Word → nat) → ∀ps:PseudoStatus.
- {{ ps':PseudoStatus | code_memory … ps = code_memory … ps' }
-≝
-  λticks_of.
-  λs.
-  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s) in
-  let ticks ≝ ticks_of (program_counter ? s) in
-  let s ≝ set_clock ? s (clock ? s + ticks) in
-  let s ≝ set_program_counter ? s pc in
-  let s ≝
-    match instr with
-    [ Instruction instr ⇒
-       Some PseudoStatus (execute_1_preinstruction … (λx, y. address_of_word_labels y x) instr s)
-    | Comment cmt ⇒ Some PseudoStatus s
-    | Cost cst ⇒ Some PseudoStatus s
-    | Jmp jmp ⇒ Some PseudoStatus (set_program_counter ? s (address_of_word_labels s jmp))
-    | Call call ⇒
-      let a ≝ address_of_word_labels s call in
-      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
-      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
-      let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ? s) in
-      let s ≝ write_at_stack_pointer ? s pc_bl in
-      let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ? s SFR_SP) (bitvector_of_nat 8 1) in
-      let s ≝ set_8051_sfr ? s SFR_SP new_sp in
-      let s ≝ write_at_stack_pointer ? s pc_bu in
-        Some PseudoStatus (set_program_counter ? s a)
-    | Mov dptr ident ⇒
-       Some PseudoStatus (set_arg_16 ? s (get_arg_16 ? s (DATA16 (address_of_word_labels s ident))) dptr)
-    ]
-  in
-    s.
-  [2: % ]
-  normalize
-  @ I
-qed.