Changeset 902


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

Cleanup.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r901 r902  
    809809qed.
    810810
    811 lemma fetch_assembly_pseudo:
    812  ∀program,ppc,lookup_labels,lookup_datalabels.
    813   ∀pc,pi,code_memory,instructions,len,assembled.
    814    let expansion ≝ jump_expansion_policy program ppc in
    815    Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
    816     Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
    817      encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    818       fetch_many code_memory len (bitvector_of_nat … pc) instructions.
    819  #program #ppc #lookup_labels #lookup_datalabels #pc #pi #code_memory #instructions #len #assembled
    820  #EQ1 #EQ2 generalize in match EQ1 -EQ1; generalize in match pc -pc; elim instructions
    821   [ #pc #EQ1 #H whd whd in EQ2:(???%); <EQ1 in EQ2; whd in ⊢ (???% → ?) #EQ2
    822     cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b >EQ2b
    823     whd in ⊢ (% → %) #H >EQ2a <plus_n_O
    824     (* OK, ARITHMETIC *) cases daemon
    825    | #i #tl #IH #pc #EQ1 whd in EQ2:(???%); <EQ1 in EQ2; whd in ⊢ (???% → ?) #EQ2
    826     cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2 #EQ2a #EQ2b
    827     change in EQ2b with (? = ?@flatten …) >EQ2b in IH ⊢ %; -assembled; #IH #H
    828     cases (encoding_check_append … H); -H; #H1 #H2 whd
    829     generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
    830     cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
    831     cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % //
    832     >(eq_bv_to_eq … K2) @IH
    833      [
    834      | @H2
    835      ]
    836   ]
    837 qed.
    838811
    839812(* This establishes the correspondence between pseudo program counters and
Note: See TracChangeset for help on using the changeset viewer.