Changeset 2115

Timestamp:

Jun 27, 2012, 1:59:47 AM (6 years ago)

Author:

sacerdot

Message:

Old commented out code removed

File:

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

src/ASM/AssemblyProof.ma

@@ -1209 +1209 @@
   >fetch_pseudo_refl in H1; #assm @assm assumption
 qed.
-
-(* OLD?
-definition assembly_specification:
-  ∀assembly_program: pseudo_assembly_program.
-  ∀code_mem: BitVectorTrie Byte 16. Prop ≝
-  λpseudo_assembly_program.
-  λcode_mem.
-    ∀pc: Word.
-      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 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:
-  ∀pseudo_assembly_program.
-    match assembly pseudo_assembly_program with
-    [ None ⇒ True
-    | Some code_mem_cost ⇒
-      let 〈code_mem, cost〉 ≝ code_mem_cost in
-        assembly_specification pseudo_assembly_program (load_code_memory code_mem)
-    ].
-(*
-  # PROGRAM
-  [ cases PROGRAM
-    # PREAMBLE
-    # INSTR_LIST
-    elim INSTR_LIST
-    [ whd
-      whd in ⊢ (∀_. %)
-      # PC
-      whd
-    | # INSTR
-      # INSTR_LIST_TL
-      # H
-      whd
-      whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
-    ]
-  | cases not_implemented
-  ] *)
-*)
 
 (* XXX: changed this type.  Bool specifies whether byte is first or second