Changeset 2115
- Timestamp:
- Jun 27, 2012, 1:59:47 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r2113 r2115 1209 1209 >fetch_pseudo_refl in H1; #assm @assm assumption 1210 1210 qed. 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 in1220 let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in1221 let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in1222 let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in1223 let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program1224 (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in1225 match pre_assembled with1226 [ None ⇒ True1227 | Some pc_code ⇒1228 let 〈new_pc,code〉 ≝ pc_code in1229 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 with1234 [ None ⇒ True1235 | Some code_mem_cost ⇒1236 let 〈code_mem, cost〉 ≝ code_mem_cost in1237 assembly_specification pseudo_assembly_program (load_code_memory code_mem)1238 ].1239 (*1240 # PROGRAM1241 [ cases PROGRAM1242 # PREAMBLE1243 # INSTR_LIST1244 elim INSTR_LIST1245 [ whd1246 whd in ⊢ (∀_. %)1247 # PC1248 whd1249 | # INSTR1250 # INSTR_LIST_TL1251 # H1252 whd1253 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ?])1254 ]1255 | cases not_implemented1256 ] *)1257 *)1258 1211 1259 1212 (* XXX: changed this type. Bool specifies whether byte is first or second
Note: See TracChangeset
for help on using the changeset viewer.