Changeset 904 for src/ASM/AssemblyProof.ma
- Timestamp:
- Jun 8, 2011, 5:53:32 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/AssemblyProof.ma
r903 r904 1014 1014 sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len). 1015 1015 1016 lemma fetch_assembly_pseudo:1017 ∀program,ppc,lookup_labels,lookup_datalabels.1018 ∀pi,code_memory,len,assembled,instructions,pc.1019 let expansion ≝ jump_expansion_policy program ppc in1020 Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →1021 Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →1022 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →1023 fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.1024 1025 1026 1016 lemma rev_preserves_length: 1027 1017 ∀A.∀l. length … (rev A l) = length … l.
Note: See TracChangeset
for help on using the changeset viewer.