Changeset 921


Ignore:
Timestamp:
Jun 9, 2011, 3:21:27 PM (8 years ago)
Author:
mulligan
Message:

resolved conflict, fixed bugs

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/AssemblyProof.ma

    r919 r921  
    892892  ∀pi,code_memory,len,assembled,instructions,pc.
    893893   let expansion ≝ jump_expansion ppc program in
    894    Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
    895     Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
     894   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
     895    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) lookup_labels lookup_datalabels pi →
    896896     encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … (pc + len)) assembled →
    897897      fetch_many code_memory (bitvector_of_nat … (pc + len)) (bitvector_of_nat … pc) instructions.
    898898 #program #ppc #lookup_labels #lookup_datalabels #pi #code_memory #len #assembled #instructions #pc
    899  #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
     899 #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
     900 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
    900901 >EQ2a >EQ2b -EQ2a EQ2b;
    901902  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
     
    908909    >(eq_bv_to_eq … K2) @IH @H2 ]
    909910qed.
    910 
    911911
    912912(* This establishes the correspondence between pseudo program counters and
     
    923923         let 〈program_counter, sigma_map〉 ≝ pc_map in
    924924         let 〈label, i〉 ≝ i in
    925           match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
     925          match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
    926926           [ None ⇒ None ?
    927927           | Some pc_ignore ⇒
     
    10201020
    10211021axiom tech_pc_sigma0_append:
    1022  ∀preamble,instr_list,prefix,label,i,pc',code,pc,costs,costs'.
     1022 ∀preamble,instr_list,prefix,label,i,pc',code,ppc,pc,costs,costs'.
    10231023  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
    1024    construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
     1024   construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
    10251025    tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉.
    10261026
    10271027axiom tech_pc_sigma0_append_None:
    1028  ∀preamble,instr_list,prefix,i,pc,costs.
     1028 ∀preamble,instr_list,prefix,i,ppc,pc,costs.
    10291029  Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
    1030    construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
     1030   construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
    10311031    → False.
    10321032
     
    13611361   ∀ppc,len,assembledi.
    13621362    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1363     (* BUG HERE: WE SHOULD PASS BOTH ppc (FOR THE POLICY) AND (sigma program ppc) FOR THE OFFSETS *)
    1364      Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
     1363     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
    13651364      encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
    13661365       sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
     
    13821381    let expansion ≝ jump_expansion ppc program in
    13831382    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
    1384      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
     1383     Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi →
    13851384      fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
    13861385 #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc #instructions
     
    13981397 whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?)
    13991398 #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
    1400  <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
     1399 normalize nodelta in EXPAND; (* HERE *)
     1400 generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
     1401 >bitvector_of_nat_nat_of_bitvector in H1; #H1
     1402 <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
    14011403 #H1 #H2
    14021404 cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
    1403  generalize in match (H1 ??? (nat_of_bitvector … (sigma program ppc)) (refl …) (refl …) ?) -H1;
    1404   [ #K3 >bitvector_of_nat_nat_of_bitvector in K3; #R @R
    1405   | >bitvector_of_nat_nat_of_bitvector @K1 ]
     1405 generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
     1406  [ #K3 @K3 | @K1 ]
    14061407qed.
    14071408
Note: See TracChangeset for help on using the changeset viewer.