Changeset 2115


Ignore:
Timestamp:
Jun 27, 2012, 1:59:47 AM (5 years ago)
Author:
sacerdot
Message:

Old commented out code removed

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r2113 r2115  
    12091209  >fetch_pseudo_refl in H1; #assm @assm assumption
    12101210qed.
    1211 
    1212 (* OLD?
    1213 definition assembly_specification:
    1214   ∀assembly_program: pseudo_assembly_program.
    1215   ∀code_mem: BitVectorTrie Byte 16. Prop ≝
    1216   λpseudo_assembly_program.
    1217   λcode_mem.
    1218     ∀pc: Word.
    1219       let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in
    1220       let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in
    1221       let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in
    1222       let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in
    1223       let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program
    1224        (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in
    1225       match pre_assembled with
    1226        [ None ⇒ True
    1227        | Some pc_code ⇒
    1228           let 〈new_pc,code〉 ≝ pc_code in
    1229            encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ].
    1230 
    1231 axiom assembly_meets_specification:
    1232   ∀pseudo_assembly_program.
    1233     match assembly pseudo_assembly_program with
    1234     [ None ⇒ True
    1235     | Some code_mem_cost ⇒
    1236       let 〈code_mem, cost〉 ≝ code_mem_cost in
    1237         assembly_specification pseudo_assembly_program (load_code_memory code_mem)
    1238     ].
    1239 (*
    1240   # PROGRAM
    1241   [ cases PROGRAM
    1242     # PREAMBLE
    1243     # INSTR_LIST
    1244     elim INSTR_LIST
    1245     [ whd
    1246       whd in ⊢ (∀_. %)
    1247       # PC
    1248       whd
    1249     | # INSTR
    1250       # INSTR_LIST_TL
    1251       # H
    1252       whd
    1253       whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])
    1254     ]
    1255   | cases not_implemented
    1256   ] *)
    1257 *)
    12581211
    12591212(* XXX: changed this type.  Bool specifies whether byte is first or second
Note: See TracChangeset for help on using the changeset viewer.