Changeset 846 for src/ASM/AssemblyProof.ma

Timestamp:

May 25, 2011, 6:10:04 PM (10 years ago)

Author:

mulligan

Message:

changes

File:

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

src/ASM/AssemblyProof.ma

@@ -131 +131 @@
   ].
 
-axiom sigma: pseudo_assembly_program → Word → Word.
+axiom sigma': pseudo_assembly_program → Word → Word.
 
 definition assembly_specification:
@@ -141 +141 @@
       let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
       let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
-      let labels ≝ λx. sigma pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
-      let datalabels ≝ λx. sigma pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
+      let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
+      let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
       let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
-       (sigma pseudo_assembly_program pc) labels datalabels pre_instr in
+       (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
       match pre_assembled with
        [ None ⇒ True
        | Some pc_code ⇒
           let 〈new_pc,code〉 ≝ pc_code in
-           encoding_check code_mem pc (sigma pseudo_assembly_program pre_new_pc) code ].
+           encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
 
 axiom assembly_meets_specification:
@@ -185 +185 @@
     | Some p ⇒
        let cm ≝ load_code_memory (\fst p) in
-       let pc ≝ sigma pap (program_counter ? ps) in
+       let pc ≝ sigma' pap (program_counter ? ps) in
         Some …
          (mk_PreStatus (BitVectorTrie Byte 16)
@@ -198 +198 @@
            (p3_latch … ps)
            (clock … ps)) ].
-           
+(*
 definition write_at_stack_pointer':
  ∀M. ∀ps: PreStatus M. Byte → Σps':PreStatus M.(code_memory … ps = code_memory … ps') ≝
@@ -300 +300 @@
     | Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w
     ].
- #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ])
+ #ps #ps' #H whd in ⊢ (mat
+ ch % with [ _ ⇒ ? | _ ⇒ ? ])
  generalize in match (refl … (assembly (code_memory … ps)))
  cases (assembly ?) in ⊢ (???% → %)
   [ #K whd whd in ⊢ (??%?) <H >K %
   | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ]
-qed.
+qed.*)
+
+let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝
+  match encoding with
+  [ nil ⇒ True
+  | cons hd tl ⇒
+    let 〈new_pc, byte〉 ≝ next code_memory pc in
+      hd = byte ∧ encoding_check' code_memory new_pc tl
+  ].
+
+lemma test:
+  ∀i: instruction.
+  ∃pc.
+  let assembled ≝ assembly1 i in
+  let code_memory ≝ load_code_memory assembled in
+  let fetched ≝ fetch code_memory pc in
+  let 〈instr_pc, ticks〉 ≝ fetched in
+    \fst instr_pc = i.
+  # INSTR
+  %
+  [ @ (zero 16)
+  | cases INSTR
+  ].
+
+lemma test:
+  ∀pc: Word.
+  ∀code_memory: BitVectorTrie Byte 16.
+  ∀i: instruction.
+    let assembled ≝ assembly1 i in
+      encoding_check' code_memory pc assembled →
+        let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in
+        let 〈instr, pc〉 ≝ instr_pc in
+          instr = i.
+  # PC # CODE_MEMORY # INSTRUCTION
+  whd
+  whd in ⊢ (? → match % with [ _ ⇒ ? ])
+  cases (next CODE_MEMORY PC)
+  whd
+  # PC1 # V1
+
+
+  cases (fetch CODE_MEMORY PC)
+  # INSTR_PC
+  # TICKS
+  cases (INSTRUCTION)
+  [ # ADDR11
+    # ENCODING_CHECK
+    whd in ENCODING_CHECK;
+    normalize
+    cases (INSTR_PC)
+    # INSTR
+    # PC
+    normalize
+    
+    
+  # ENCODING
+  normalize
+  [ cases INSTR_PC
+    # NEW_INSTRUCTION
+    # PC
+    normalize
+    normalize in ENCODING;
+  | # ASSEMBLED
+    whd
  
 lemma main_thm: