Ignore:
Timestamp:
Jun 9, 2011, 11:56:49 AM (9 years ago)
Author:
sacerdot
Message:

Fix for jump_expansion_policy.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r915 r916  
    891891 ∀program,ppc,lookup_labels,lookup_datalabels.
    892892  ∀pi,code_memory,len,assembled,instructions,pc.
    893    let expansion ≝ jump_expansion_policy program ppc in
     893   let expansion ≝ jump_expansion ppc program in
    894894   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
    895895    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
     
    13801380    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
    13811381    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
    1382     let expansion ≝ jump_expansion_policy program ppc in
     1382    let expansion ≝ jump_expansion ppc program in
    13831383    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    13841384     Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
     
    15971597 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ λ_.match % with [ _ ⇒ ? | _ ⇒ ? ]])
    15981598 >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))
    15991601 cases (assembly (code_memory pseudo_assembly_program ps)) [%] * #cm #costs whd
    16001602 change with (execute_1 (set_program_counter ? (set_code_memory ?? ps (load_code_memory (\fst 〈cm,costs〉))) ?) = ?)
    16011603 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.