Changeset 902
 Timestamp:
 Jun 8, 2011, 5:28:12 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r901 r902 809 809 qed. 810 810 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 in815 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 #assembled820 #EQ1 #EQ2 generalize in match EQ1 EQ1; generalize in match pc pc; elim instructions821 [ #pc #EQ1 #H whd whd in EQ2:(???%); <EQ1 in EQ2; whd in ⊢ (???% → ?) #EQ2822 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) EQ2; #EQ2a #EQ2b >EQ2b823 whd in ⊢ (% → %) #H >EQ2a <plus_n_O824 (* OK, ARITHMETIC *) cases daemon825  #i #tl #IH #pc #EQ1 whd in EQ2:(???%); <EQ1 in EQ2; whd in ⊢ (???% → ?) #EQ2826 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) EQ2 #EQ2a #EQ2b827 change in EQ2b with (? = ?@flatten …) >EQ2b in IH ⊢ %; assembled; #IH #H828 cases (encoding_check_append … H); H; #H1 #H2 whd829 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) @IH833 [834  @H2835 ]836 ]837 qed.838 811 839 812 (* This establishes the correspondence between pseudo program counters and
Note: See TracChangeset
for help on using the changeset viewer.