Changeset 1709 for src/ASM/ASMCosts.ma

Timestamp:

Feb 17, 2012, 11:52:36 AM (8 years ago)

Author:

mulligan

Message:

Changes to the execution of the MOVC instruction

File:

• src/ASM/ASMCosts.ma (modified) (4 diffs)

src/ASM/ASMCosts.ma

@@ -331 +331 @@
 qed.
 
+(* XXX: todo *)
 lemma subaddressing_mode_elim':
   ∀T: Type[2].
@@ -349 +350 @@
 qed.
 
+(* XXX: todo *)
 axiom subaddressing_mode_elim:
   ∀T: Type[2].
@@ -360 +362 @@
     subaddressing_mode_elim_type T m fixed_v Q P1 P2 P3 P4 P5 P6 P7
       P8 P9 P10 P11 P12 P13 P14 P15 P16 P17 P18 P19 n v proof.
-
-definition current_instruction0 ≝
-  λcode_memory: BitVectorTrie Byte 16.
-  λprogram_counter: Word.
-    \fst (\fst (fetch … code_memory program_counter)).
-
-definition current_instruction ≝
-  λcode_memory.
-  λs: Status code_memory.
-    current_instruction0 code_memory (program_counter … s).
-
-definition ASM_classify0: instruction → status_class ≝
-  λi: instruction.
-  match i with
-   [ RealInstruction pre ⇒
-     match pre with
-      [ RET ⇒ cl_return
-      | JZ _ ⇒ cl_jump
-      | JNZ _ ⇒ cl_jump
-      | JC _ ⇒ cl_jump
-      | JNC _ ⇒ cl_jump
-      | JB _ _ ⇒ cl_jump
-      | JNB _ _ ⇒ cl_jump
-      | JBC _ _ ⇒ cl_jump
-      | CJNE _ _ ⇒ cl_jump
-      | DJNZ _ _ ⇒ cl_jump
-      | _ ⇒ cl_other
-      ]
-   | ACALL _ ⇒ cl_call
-   | LCALL _ ⇒ cl_call
-   | JMP _ ⇒ cl_call
-   | AJMP _ ⇒ cl_jump
-   | LJMP _ ⇒ cl_jump
-   | SJMP _ ⇒ cl_jump
-   | _ ⇒ cl_other
-   ].
-
-definition ASM_classify: ∀code_memory. Status code_memory → status_class ≝
-  λcode_memory.
-  λs: Status code_memory.
-    ASM_classify0 (current_instruction … s).
 
 definition current_instruction_is_labelled ≝
@@ -505 +466 @@
 
 (* XXX: indexing bug *)
-example fetch_twice_fetch_execute_1:
+lemma fetch_twice_fetch_execute_1:
   ∀code_memory: BitVectorTrie Byte 16.
   ∀start_status: Status code_memory.
+    ASM_classify code_memory start_status = cl_other →
     \snd (\fst (fetch code_memory (program_counter … start_status))) =
       program_counter … (execute_1 … start_status).
-  cases daemon
-qed.
+  #code_memory #start_status #classify_assm
+  whd in match execute_1; normalize nodelta
+  whd in match execute_1'; normalize nodelta
+  whd in match execute_1_0; normalize nodelta
+  generalize in match (refl … (fetch code_memory
+    (program_counter (BitVectorTrie Byte 16) code_memory start_status)));
+  cases (fetch code_memory
+    (program_counter (BitVectorTrie Byte 16) code_memory start_status)) in ⊢ (??%? → ?);
+  #instr_pc #ticks #fetch_rewrite <fetch_rewrite
+  cases 
+qed-.
 
 lemma reachable_program_counter_to_0_lt_total_program_size: