Changeset 903 for src

Timestamp:

Jun 8, 2011, 5:53:18 PM (9 years ago)

Author:

sacerdot

Message:

Statement of new main lemma (as axiom).

File:

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

src/ASM/AssemblyProof.ma

@@ -931 +931 @@
     → False.
 
-
+(*
 definition build_maps' ≝
   λpseudo_program.
@@ -986 +986 @@
 qed.
 
-(*
-(*
-notation < "hvbox('let' 〈ident x,ident y〉 ≝ t 'in' s)"
- with precedence 10
-for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
-*)
-
 lemma build_maps_ok:
  ∀p:pseudo_assembly_program.
@@ -1008 +1001 @@
 *)
 
-(*
-lemma list_elim_rev:
- ∀A:Type[0].∀P:list A → Prop.
-  P [ ] → (∀n,l. length l = n → P l →  
-  P [ ] → (∀l,a. P l → P (l@[a])) →
-   ∀l. P l.
- #A #P
-qed.*)
+axiom assembly_ok:
+ ∀program,assembled,costs,labels,datalabels.
+  Some … 〈labels,datalabels〉 = 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,len,assembledi.
+    let 〈pi,newppc〉 ≝ fetch_pseudo_instruction (\snd program) ppc in
+     Some … 〈len,assembledi〉 = assembly_1_pseudoinstruction 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).
+
+lemma fetch_assembly_pseudo:
+ ∀program,ppc,lookup_labels,lookup_datalabels.
+  ∀pi,code_memory,len,assembled,instructions,pc.
+   let expansion ≝ jump_expansion_policy program ppc 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 →
+     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.
+
 
 lemma rev_preserves_length: