Changeset 838 for src/ASM/AssemblyProof.ma

Timestamp:

May 25, 2011, 12:08:24 PM (10 years ago)

Author:

sacerdot

Message:

Restored.

File:

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

src/ASM/AssemblyProof.ma

@@ -11 +11 @@
   ].
 
-(*
+axiom sigma: pseudo_assembly_program → Word → Word.
+
 definition assembly_specification:
-  ∀sigma: Word → Word. ∀assembly_program: pseudo_assembly_program.
+  ∀assembly_program: pseudo_assembly_program.
   ∀code_mem: BitVectorTrie Byte 16. Prop ≝
-  λsigma.
   λpseudo_assembly_program.
   λcode_mem.
@@ -21 +21 @@
       let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
       let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
-      let address_of ≝ ? in
-      let labels ≝ λx. sigma (address_of_word_labels_code_mem instr_list x) in
-      let datalabels ≝ λx. sigma (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
-      let pre_assembled ≝ assembly_1_pseudoinstruction labels datalabels address_of 〈None ?, pre_instr〉 in
-        encoding_check code_mem pc (sigma pre_new_pc) pre_assembled.
-      cases not_implemented
-qed.
+      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
+      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 ].
 
 axiom assembly_meets_specification:
@@ -35 +37 @@
     | Some code_mem_cost ⇒
       let 〈code_mem, cost〉 ≝ code_mem_cost in
-        assembly_specification ? pseudo_assembly_program (load_code_memory code_mem)
+        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
     ].
-cases not_implemented (*
+(*
   # PROGRAM
   [ cases PROGRAM
@@ -55 +57 @@
   | cases not_implemented
   ] *)
-qed.
-*)
-
-axiom sigma: pseudo_assembly_program → Word → Word.
-
-(*
+
 definition status_of_pseudo_status: PseudoStatus → option Status ≝
  λps.
@@ -81 +78 @@
            (p3_latch … ps)
            (clock … ps)) ].
-*)
-
+           
 (* RUSSEL **)