Changeset 904


Ignore:
Timestamp:
Jun 8, 2011, 5:53:32 PM (8 years ago)
Author:
sacerdot
Message:

Cleanup.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r903 r904  
    10141014       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
    10151015
    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 in
    1020    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 
    10261016lemma rev_preserves_length:
    10271017 ∀A.∀l. length … (rev A l) = length … l.
Note: See TracChangeset for help on using the changeset viewer.