Changeset 924 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 9, 2011, 4:14:54 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

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

src/ASM/AssemblyProof.ma

@@ -1369 +1369 @@
     bitvector_of_nat n (nat_of_bitvector n v) = v.
 
+axiom assembly_ok_to_expand_pseudo_instruction_ok:
+ ∀program,assembled,costs.
+  Some … 〈assembled,costs〉 = assembly program →
+   ∀ppc.
+    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 ppc program in
+    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
+     ∃instructions.
+      Some ? instructions = expand_pseudo_instruction lookup_labels lookup_datalabels (sigma program ppc) expansion pi.
+
 lemma fetch_assembly_pseudo2:
  ∀program,assembled,costs,labels.
   Some … 〈labels,costs〉 = build_maps program →
   Some … 〈assembled,costs〉 = assembly program →
-   ∀ppc,instructions.
+   ∀ppc.
     let code_memory ≝ load_code_memory assembled in
     let preamble ≝ \fst program in
@@ -1381 +1395 @@
     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 (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
+     ∃instructions.
+      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
+ generalize in match (assembly_ok_to_expand_pseudo_instruction_ok program assembled costs ASSEMBLY ppc)
  letin code_memory ≝ (load_code_memory assembled)
  letin preamble ≝ (\fst program)
@@ -1389 +1405 @@
  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
+ whd in ⊢ (% → %)
  generalize in match (assembly_ok … BUILD_MAPS ASSEMBLY ppc)
  cases (fetch_pseudo_instruction (\snd program) ppc) #pi #newppc
@@ -1395 +1411 @@
   (λ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:(∀_.∀_.???% → ?);
+ whd in ⊢ ((∀_.∀_.∀_.∀_.%) → (∀_.∀_.%) → % → %) #H1 #H2 * #instructions #EXPAND
+ whd in H1:(∀_.∀_.∀_.∀_.? → ???% → ?) H2:(∀_.∀_.???% → ?);
  normalize nodelta in EXPAND; (* HERE *)
  generalize in match (λlen, assembled.H1 len assembled instructions (nat_of_bitvector … (sigma program ppc))) -H1; #H1
@@ -1404 +1420 @@
  cases (H2 ?? (refl …)) -H2; #K1 #K2 >K2
  generalize in match (H1 ?? (refl …) (refl …) ?) -H1;
-  [ #K3 @K3 | @K1 ]
+  [ #K3 % [2: % [% | @K3]] | @K1 ]
 qed.
 
@@ -1615 +1631 @@
  whd in match (\snd 〈final_pc,assembled〉) in H;
  -s s'' labels costs final_ppc final_pc;
+ (* NICE STATEMENT HERE *)