Changeset 915 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 9, 2011, 11:30:59 AM (10 years ago)

Author:

mulligan

Message:

finished changes to fetch_assembly_pseudo2

File:

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

src/ASM/AssemblyProof.ma

@@ -1351 +1351 @@
 
 axiom assembly_ok:
- ∀program,assembled,costs,labels,datalabels.
-  Some … 〈labels,datalabels〉 = build_maps program →
+ ∀program,assembled,costs,labels.
+  Some … 〈labels,costs〉 = build_maps program →
   Some … 〈assembled,costs〉 = assembly program →
   let code_memory ≝ load_code_memory assembled in
-  let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in
+  let preamble ≝ \fst program in
+  let datalabels ≝ construct_datalabels preamble in
+  let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
   let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    ∀ppc,len,assembledi.
@@ -1365 +1367 @@
 
 axiom bitvector_of_nat_nat_of_bitvector:
- ∀n,v. bitvector_of_nat n (nat_of_bitvector n v) = v.
+  ∀n,v.
+    bitvector_of_nat n (nat_of_bitvector n v) = v.
 
 lemma fetch_assembly_pseudo2:
- ∀program,assembled,costs,labels,datalabels.
-  Some … 〈labels,datalabels〉 = build_maps program →
+ ∀program,assembled,costs,labels.
+  Some … 〈labels,costs〉 = build_maps program →
   Some … 〈assembled,costs〉 = assembly program →
-  let code_memory ≝ load_code_memory assembled in
-  let lookup_labels ≝ λx. lookup ?? x labels (zero ?) in
-  let lookup_datalabels ≝ λx. lookup ?? x datalabels (zero ?) in
    ∀ppc,instructions.
+    let code_memory ≝ load_code_memory assembled in
+    let preamble ≝ \fst program in
+    let data_labels ≝ construct_datalabels preamble in
+    let lookup_labels ≝ λx. sigma program (address_of_word_labels_code_mem (\snd program) x) in
+    let lookup_datalabels ≝ λx. lookup ? ? x data_labels (zero ?) in
     let expansion ≝ jump_expansion_policy program ppc in
     let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels ppc expansion pi →
       fetch_many code_memory (sigma program newppc) (sigma program ppc) instructions.
- #program #assembled #costs #labels #datalabels #BUILD_MAPS #ASSEMBLY #ppc #instructions whd
+ #program #assembled #costs #labels #BUILD_MAPS #ASSEMBLY #ppc #instructions
+ letin code_memory ≝ (load_code_memory assembled)
+ letin preamble ≝ (\fst program)
+ letin data_labels ≝ (construct_datalabels preamble)
+ letin lookup_labels ≝ (λx. sigma program (address_of_word_labels_code_mem (\snd program) x))
+ letin lookup_datalabels ≝ (λx. lookup ? ? x data_labels (zero ?))
+ whd
  generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
  cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
  generalize in match (fetch_assembly_pseudo program ppc
-  (λx. lookup ?? x labels (zero ?)) (λx. lookup ?? x datalabels (zero ?)) pi
-  (load_code_memory assembled)) 
+  (λx. sigma program (address_of_word_labels_code_mem (\snd program) x)) (λx. lookup ?? x data_labels (zero ?)) pi
+  (load_code_memory assembled));
  whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → ?)
  #H1 #H2 whd #EXPAND whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);