- Timestamp:
- Jun 9, 2011, 11:56:49 AM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r915 r916 891 891 ∀program,ppc,lookup_labels,lookup_datalabels. 892 892 ∀pi,code_memory,len,assembled,instructions,pc. 893 let expansion ≝ jump_expansion _policy program ppcin893 let expansion ≝ jump_expansion ppc program in 894 894 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi → 895 895 Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi → … … 1380 1380 let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in 1381 1381 let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in 1382 let expansion ≝ jump_expansion _policy program ppcin1382 let expansion ≝ jump_expansion ppc program in 1383 1383 let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in 1384 1384 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi → … … 1597 1597 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]]) 1598 1598 >execute_1_pseudo_instruction_preserves_code_memory 1599 generalize in match (fetch_assembly_pseudo2 (code_memory … ps)) 1600 cases (build_maps (code_memory pseudo_assembly_program ps)) 1599 1601 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd 1600 1602 change with (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) ?) = ?) 1601 1603 change with (? = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ticks_of ps) (load_code_memory (\fst 〈cm,costs〉))) ?) 1604 whd in ⊢ (??%?)
Note: See TracChangeset
for help on using the changeset viewer.