Changeset 890 for src

Timestamp:

Jun 7, 2011, 2:56:39 AM (10 years ago)

Author:

sacerdot

Message:

Better statement, begin of uniform proof.

File:

• src/ASM/AssemblyProof.ma (modified) (3 diffs)

src/ASM/AssemblyProof.ma

@@ -698 +698 @@
 qed.
 
+let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
+                       (encoding: list Byte) on encoding: Prop ≝
+  match encoding with
+  [ nil ⇒ final_pc = pc
+  | cons hd tl ⇒
+    let 〈new_pc, byte〉 ≝ next code_memory pc in
+      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
+  ].
+
+axiom eq_bv_refl: ∀n,v. eq_bv n v v = true.
+
+(*
 lemma test:
   ∀pc,i.
@@ -705 +717 @@
       let 〈instr_pc, ticks〉 ≝ fetched in
         eq_instruction (\fst instr_pc)) i = true.
- #pc #i cases i #arg try #arg2 whd in ⊢ (??%?)
+*)
+lemma test:
+  ∀pc,i,code_memory.
+      let assembled ≝ assembly1 i in
+      let len ≝ length … assembled in
+      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
+      let fetched ≝ fetch code_memory (bitvector_of_nat … pc) in
+      let 〈instr_pc, ticks〉 ≝ fetched in
+      let 〈instr,pc'〉 ≝ instr_pc in
+       (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
+ #pc #i #code_memory cases i [8: *]
+ [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
+ [47,48,49: |*: #arg @(list_addressing_mode_tags_elim_prop … arg) whd try % -arg
+  [2,3,5,7,10,12,16,17,18,21,25,26,27,30,31,32,37,38,39,40,41,42,43,44,45,48,51,58,
+   59,60,63,64,65,66,67: #ARG]
+ [1: #arg2 @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2
+ 
+ [7: #arg2]
+ 
+  whd
+ [ @(list_addressing_mode_tags_elim_prop … arg) whd try %
+   @(list_addressing_mode_tags_elim_prop … arg2) whd try %
+   * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
+   whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 >eq_instruction_refl @eq_bv_refl
+ |6: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
+   * #H1 * #H2 #H3 whd in H3; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
+   whd in ⊢ match ??% with [_ ⇒ ?] <H1 whd <H2 <H3 >eq_instruction_refl @eq_bv_refl
+ |7: @(list_addressing_mode_tags_elim_prop … arg) whd try %
+   * #H1 #H2 whd in H2; whd change in ⊢ match % with [_ ⇒ ?] with (fetch0 ??)
+ |3,5: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
+   
+   @split_elim
+
+  
+   whd in ⊢ (??%?)
    [2,4: @(list_addressing_mode_tags_elim_prop … arg) whd try % #XX
          whd in ⊢ (??(match ? (? ? %) ? with [ _ ⇒ ?] ?)?)
@@ -1297 +1343 @@
  |   
 
-let rec encoding_check (code_memory: BitVectorTrie Byte 16) (pc: Word) (final_pc: Word)
-                       (encoding: list Byte) on encoding: Prop ≝
-  match encoding with
-  [ nil ⇒ final_pc = pc
-  | cons hd tl ⇒
-    let 〈new_pc, byte〉 ≝ next code_memory pc in
-      hd = byte ∧ encoding_check code_memory new_pc final_pc tl
-  ].
-
 definition assembly_specification:
   ∀assembly_program: pseudo_assembly_program.