Changeset 901


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

Second main lemma proved.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r897 r901  
    672672 ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
    673673  (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
    674 (*
     674
    675675axiom half_add_SO:
    676676 ∀pc.
    677677 \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
    678678
     679(*
    679680axiom not_eqvb_S:
    680681 ∀pc.
     
    714715  ].
    715716
    716 axiom eq_bv_refl: ∀n,v. eq_bv n v v = true.
     717lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
     718 encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
     719  let intermediate_pc ≝ pc + length … l1 in
     720   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
     721    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
     722 #code_memory #final_pc #l1 elim l1
     723  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
     724  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
     725    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
     726qed.
     727
     728axiom  eq_bv_refl: ∀n,v. eq_bv n v v = true.
    717729
    718730axiom bitvector_3_elim_prop:
     
    722734  P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
    723735
    724 lemma test:
     736axiom fetch_assembly:
    725737  ∀pc,i,code_memory,assembled.
    726738    assembled = assembly1 i →
     
    731743      let 〈instr,pc'〉 ≝ instr_pc in
    732744       (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
    733  #pc #i #code_memory #assembled cases i [8: *]
     745(* #pc #i #code_memory #assembled cases i [8: *]
    734746 [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
    735747 [47,48,49:
     
    755767  69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
    756768 whd >eq_instruction_refl >H4 @eq_bv_refl
    757 qed.
    758  
     769qed. *)
     770
     771let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
     772 match expected with
     773  [ nil ⇒ eq_bv … pc final_pc = true
     774  | cons i tl ⇒
     775     let fetched ≝ fetch code_memory pc in
     776     let 〈instr_pc, ticks〉 ≝ fetched in
     777     let 〈instr,pc'〉 ≝ instr_pc in
     778      eq_instruction instr i = true ∧ fetch_many code_memory final_pc pc' tl].
     779
     780lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
     781 #A #a #b #EQ destruct //
     782qed.
     783
     784lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
     785 #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
     786qed.
     787
     788axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.
     789
     790lemma fetch_assembly_pseudo:
     791 ∀program,ppc,lookup_labels,lookup_datalabels.
     792  ∀pi,code_memory,len,assembled,instructions,pc.
     793   let expansion ≝ jump_expansion_policy program ppc in
     794   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
     795    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
     796     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
     797      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
     798 #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
     799 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
     800 >EQ2a >EQ2b -EQ2a EQ2b;
     801  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
     802  generalize in match pc elim instructions
     803  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
     804  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
     805    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
     806    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
     807    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % //
     808    >(eq_bv_to_eq … K2) @IH @H2 ]
     809qed.
     810
     811lemma 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  ]
     837qed.
     838
    759839(* This establishes the correspondence between pseudo program counters and
    760840   program counters. It is at the heart of the proof. *)
Note: See TracChangeset for help on using the changeset viewer.