# Changeset 901

Ignore:
Timestamp:
Jun 8, 2011, 5:27:35 PM (10 years ago)
Message:

Second main lemma proved.

File:
1 edited

Unmodified
Added
Removed
• ## src/ASM/AssemblyProof.ma

 r897 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop. (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v). (* axiom half_add_SO: ∀pc. \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc). (* axiom not_eqvb_S: ∀pc. ]. axiom eq_bv_refl: ∀n,v. eq_bv n v v = true. lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2. encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) → let intermediate_pc ≝ pc + length … l1 in encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧ encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2. #code_memory #final_pc #l1 elim l1 [ #pc #l2 whd in ⊢ (????% → ?) #H half_add_SO in H2; #H2 cases (IH … H2) half_add_SO @K1 ] qed. axiom  eq_bv_refl: ∀n,v. eq_bv n v v = true. axiom bitvector_3_elim_prop: P [[true;true;false]] → P [[true;true;true]] → ∀v. P v. lemma test: axiom fetch_assembly: ∀pc,i,code_memory,assembled. assembled = assembly1 i → let 〈instr,pc'〉 ≝ instr_pc in (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true. #pc #i #code_memory #assembled cases i [8: *] (* #pc #i #code_memory #assembled cases i [8: *] [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]] [47,48,49: 69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: eq_instruction_refl >H4 @eq_bv_refl qed. qed. *) let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝ match expected with [ nil ⇒ eq_bv … pc final_pc = true | cons i tl ⇒ let fetched ≝ fetch code_memory pc in let 〈instr_pc, ticks〉 ≝ fetched in let 〈instr,pc'〉 ≝ instr_pc in eq_instruction instr i = true ∧ fetch_many code_memory final_pc pc' tl]. lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b. #A #a #b #EQ destruct // qed. lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2. #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/ qed. axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2. lemma fetch_assembly_pseudo: ∀program,ppc,lookup_labels,lookup_datalabels. ∀pi,code_memory,len,assembled,instructions,pc. let expansion ≝ jump_expansion_policy program ppc in Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi → Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi → encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions. #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc #EQ1 whd in ⊢ (???% → ?) EQ2a >EQ2b -EQ2a EQ2b; generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc generalize in match pc elim instructions [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd generalize in match (fetch_assembly pc i code_memory … (refl …) H1) cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %) cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % // >(eq_bv_to_eq … K2) @IH @H2 ] qed. lemma fetch_assembly_pseudo: ∀program,ppc,lookup_labels,lookup_datalabels. ∀pc,pi,code_memory,instructions,len,assembled. let expansion ≝ jump_expansion_policy program ppc in Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi → Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi → encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled → fetch_many code_memory len (bitvector_of_nat … pc) instructions. #program #ppc #lookup_labels #lookup_datalabels #pc #pi #code_memory #instructions #len #assembled #EQ1 #EQ2 generalize in match EQ1 -EQ1; generalize in match pc -pc; elim instructions [ #pc #EQ1 #H whd whd in EQ2:(???%); EQ2b whd in ⊢ (% → %) #H >EQ2a EQ2b in IH ⊢ %; -assembled; #IH #H cases (encoding_check_append … H); -H; #H1 #H2 whd generalize in match (fetch_assembly pc i code_memory … (refl …) H1) cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %) cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % // >(eq_bv_to_eq … K2) @IH [ | @H2 ] ] qed. (* This establishes the correspondence between pseudo program counters and program counters. It is at the heart of the proof. *)
Note: See TracChangeset for help on using the changeset viewer.