Changeset 846 for src/ASM/AssemblyProof.ma
- Timestamp:
- May 25, 2011, 6:10:04 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r845 r846 131 131 ]. 132 132 133 axiom sigma : pseudo_assembly_program → Word → Word.133 axiom sigma': pseudo_assembly_program → Word → Word. 134 134 135 135 definition assembly_specification: … … 141 141 let 〈preamble, instr_list〉 ≝ pseudo_assembly_program in 142 142 let 〈pre_instr, pre_new_pc〉 ≝ fetch_pseudo_instruction instr_list pc in 143 let labels ≝ λx. sigma pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in144 let datalabels ≝ λx. sigma pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in143 let labels ≝ λx. sigma' pseudo_assembly_program (address_of_word_labels_code_mem instr_list x) in 144 let datalabels ≝ λx. sigma' pseudo_assembly_program (lookup ? ? x (construct_datalabels preamble) (zero ?)) in 145 145 let pre_assembled ≝ assembly_1_pseudoinstruction pseudo_assembly_program 146 (sigma pseudo_assembly_program pc) labels datalabels pre_instr in146 (sigma' pseudo_assembly_program pc) labels datalabels pre_instr in 147 147 match pre_assembled with 148 148 [ None ⇒ True 149 149 | Some pc_code ⇒ 150 150 let 〈new_pc,code〉 ≝ pc_code in 151 encoding_check code_mem pc (sigma pseudo_assembly_program pre_new_pc) code ].151 encoding_check code_mem pc (sigma' pseudo_assembly_program pre_new_pc) code ]. 152 152 153 153 axiom assembly_meets_specification: … … 185 185 | Some p ⇒ 186 186 let cm ≝ load_code_memory (\fst p) in 187 let pc ≝ sigma pap (program_counter ? ps) in187 let pc ≝ sigma' pap (program_counter ? ps) in 188 188 Some … 189 189 (mk_PreStatus (BitVectorTrie Byte 16) … … 198 198 (p3_latch … ps) 199 199 (clock … ps)) ]. 200 200 (* 201 201 definition write_at_stack_pointer': 202 202 ∀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 301 301 ]. 302 #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]) 302 #ps #ps' #H whd in ⊢ (mat 303 ch % with [ _ ⇒ ? | _ ⇒ ? ]) 303 304 generalize in match (refl … (assembly (code_memory … ps))) 304 305 cases (assembly ?) in ⊢ (???% → %) 305 306 [ #K whd whd in ⊢ (??%?) <H >K % 306 307 | #x #K whd whd in ⊢ (?? (λ_.??%?)) <H >K % [2: % ] ] 307 qed. 308 qed.*) 309 310 let rec encoding_check' (code_memory: BitVectorTrie Byte 16) (pc: Word) (encoding: list Byte) on encoding: Prop ≝ 311 match encoding with 312 [ nil ⇒ True 313 | cons hd tl ⇒ 314 let 〈new_pc, byte〉 ≝ next code_memory pc in 315 hd = byte ∧ encoding_check' code_memory new_pc tl 316 ]. 317 318 lemma test: 319 ∀i: instruction. 320 ∃pc. 321 let assembled ≝ assembly1 i in 322 let code_memory ≝ load_code_memory assembled in 323 let fetched ≝ fetch code_memory pc in 324 let 〈instr_pc, ticks〉 ≝ fetched in 325 \fst instr_pc = i. 326 # INSTR 327 % 328 [ @ (zero 16) 329 | cases INSTR 330 ]. 331 332 lemma test: 333 ∀pc: Word. 334 ∀code_memory: BitVectorTrie Byte 16. 335 ∀i: instruction. 336 let assembled ≝ assembly1 i in 337 encoding_check' code_memory pc assembled → 338 let 〈instr_pc, ignore〉 ≝ fetch code_memory pc in 339 let 〈instr, pc〉 ≝ instr_pc in 340 instr = i. 341 # PC # CODE_MEMORY # INSTRUCTION 342 whd 343 whd in ⊢ (? → match % with [ _ ⇒ ? ]) 344 cases (next CODE_MEMORY PC) 345 whd 346 # PC1 # V1 347 348 349 cases (fetch CODE_MEMORY PC) 350 # INSTR_PC 351 # TICKS 352 cases (INSTRUCTION) 353 [ # ADDR11 354 # ENCODING_CHECK 355 whd in ENCODING_CHECK; 356 normalize 357 cases (INSTR_PC) 358 # INSTR 359 # PC 360 normalize 361 362 363 # ENCODING 364 normalize 365 [ cases INSTR_PC 366 # NEW_INSTRUCTION 367 # PC 368 normalize 369 normalize in ENCODING; 370 | # ASSEMBLED 371 whd 308 372 309 373 lemma main_thm:
Note: See TracChangeset
for help on using the changeset viewer.