Changeset 921 for src

Timestamp:

Jun 9, 2011, 3:21:27 PM (9 years ago)

Author:

mulligan

Message:

resolved conflict, fixed bugs

File:

• src/ASM/AssemblyProof.ma (modified) (7 diffs)

src/ASM/AssemblyProof.ma

@@ -892 +892 @@
   ∀pi,code_memory,len,assembled,instructions,pc.
    let expansion ≝ jump_expansion ppc program 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 →
+   Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (bitvector_of_nat ? pc) expansion pi →
+    Some … 〈len,assembled〉 = assembly_1_pseudoinstruction program ppc (bitvector_of_nat ? pc) 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 ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2 cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
+ #EQ1 whd in ⊢ (???% → ?) <EQ1 whd in ⊢ (???% → ?) #EQ2
+ cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b
  >EQ2a >EQ2b -EQ2a EQ2b;
   generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
@@ -908 +909 @@
     >(eq_bv_to_eq … K2) @IH @H2 ]
 qed.
-
 
 (* This establishes the correspondence between pseudo program counters and
@@ -923 +923 @@
          let 〈program_counter, sigma_map〉 ≝ pc_map in
          let 〈label, i〉 ≝ i in
-          match construct_costs instr_list program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
+          match construct_costs instr_list ppc program_counter (λx. zero ?) (λx. zero ?) (Stub …) i with
            [ None ⇒ None ?
            | Some pc_ignore ⇒
@@ -1020 +1020 @@
 
 axiom tech_pc_sigma0_append:
- ∀preamble,instr_list,prefix,label,i,pc',code,pc,costs,costs'.
+ ∀preamble,instr_list,prefix,label,i,pc',code,ppc,pc,costs,costs'.
   Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
-   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
+   construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = Some … 〈pc',code〉 →
     tech_pc_sigma0 〈preamble,prefix@[〈label,i〉]〉 = Some … 〈pc',costs'〉.
 
 axiom tech_pc_sigma0_append_None:
- ∀preamble,instr_list,prefix,i,pc,costs.
+ ∀preamble,instr_list,prefix,i,ppc,pc,costs.
   Some … 〈pc,costs〉 = tech_pc_sigma0 〈preamble,prefix〉 →
-   construct_costs 〈preamble,instr_list〉 … pc (λx.zero 16) (λx. zero 16) costs i = None …
+   construct_costs 〈preamble,instr_list〉 … ppc pc (λx.zero 16) (λx. zero 16) costs i = None …
     → False.
 
@@ -1361 +1361 @@
    ∀ppc,len,assembledi.
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
-    (* BUG HERE: WE SHOULD PASS BOTH ppc (FOR THE POLICY) AND (sigma program ppc) FOR THE OFFSETS *)
-     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc lookup_labels lookup_datalabels pi →
+     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction program ppc (sigma program ppc) lookup_labels lookup_datalabels pi →
       encoding_check code_memory (sigma program ppc) (bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len)) assembledi ∧
        sigma program newppc = bitvector_of_nat … (nat_of_bitvector … (sigma program ppc) + len).
@@ -1382 +1381 @@
     let expansion ≝ jump_expansion ppc program in
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
-     Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
+     Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi →
       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
  #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc #instructions
@@ -1398 +1397 @@
  whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?)
  #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
- <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
+ normalize nodelta in EXPAND; (* HERE *)
+ generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
+ >bitvector_of_nat_nat_of_bitvector in H1; #H1
+ <EXPAND in H1 H2; whd in ⊢ ((∀_.∀_.? → ???% → ?) → (∀_.∀_.???% → ?) → ?)
  #H1 #H2
  cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
- generalize in match (H1 ??? (nat_of_bitvector … (sigma program ppc)) (refl …) (refl …) ?) -H1;
-  [ #K3 >bitvector_of_nat_nat_of_bitvector in K3; #R @R
-  | >bitvector_of_nat_nat_of_bitvector @K1 ]
+ generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
+  [ #K3 @K3 | @K1 ]
 qed.