Changeset 901 for src

Timestamp:

Jun 8, 2011, 5:27:35 PM (10 years ago)

Author:

sacerdot

Message:

Second main lemma proved.

File:

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

src/ASM/AssemblyProof.ma

@@ -672 +672 @@
  ∀A,l,m,v.∀P: (Vector A l) × (Vector A m) → Prop.
   (∀vl,vm. v = vl@@vm → P 〈vl,vm〉) → P (split A l m v).
-(*
+
 axiom half_add_SO:
  ∀pc.
  \snd (half_add 16 (bitvector_of_nat … pc) (bitvector_of_nat … 1)) = bitvector_of_nat … (S pc).
 
+(*
 axiom not_eqvb_S:
  ∀pc.
@@ -714 +715 @@
   ].
 
-axiom eq_bv_refl: ∀n,v. eq_bv n v v = true.
+lemma encoding_check_append: ∀code_memory,final_pc,l1,pc,l2.
+ encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … final_pc) (l1@l2) →
+  let intermediate_pc ≝ pc + length … l1 in
+   encoding_check code_memory (bitvector_of_nat … pc) (bitvector_of_nat … intermediate_pc) l1 ∧
+    encoding_check code_memory (bitvector_of_nat … intermediate_pc) (bitvector_of_nat … final_pc) l2.
+ #code_memory #final_pc #l1 elim l1
+  [ #pc #l2 whd in ⊢ (????% → ?) #H <plus_n_O whd whd in ⊢ (?%?) /2/
+  | #hd #tl #IH #pc #l2 * #H1 #H2 >half_add_SO in H2; #H2 cases (IH … H2) <plus_n_Sm
+    #K1 #K2 % [2:@K2] whd % // >half_add_SO @K1 ]
+qed.
+
+axiom  eq_bv_refl: ∀n,v. eq_bv n v v = true.
 
 axiom bitvector_3_elim_prop:
@@ -722 +734 @@
   P [[true;true;false]] → P [[true;true;true]] → ∀v. P v.
 
-lemma test:
+axiom fetch_assembly:
   ∀pc,i,code_memory,assembled.
     assembled = assembly1 i →
@@ -731 +743 @@
       let 〈instr,pc'〉 ≝ instr_pc in
        (eq_instruction instr i ∧ eq_bv … pc' (bitvector_of_nat … (pc + len))) = true.
- #pc #i #code_memory #assembled cases i [8: *]
+(* #pc #i #code_memory #assembled cases i [8: *]
  [16,20,29: * * |18,19: * * [1,2,4,5: *] |28: * * [1,2: * [1,2: * [1,2: * [1,2: *]]]]]
  [47,48,49:
@@ -755 +767 @@
   69,70,73,74,78,80,81,84,85,95,98,101,102,103,104,105,106,107,108,109,110: <H2]
  whd >eq_instruction_refl >H4 @eq_bv_refl
-qed.
- 
+qed. *)
+
+let rec fetch_many code_memory final_pc pc expected on expected: Prop ≝
+ match expected with
+  [ nil ⇒ eq_bv … pc final_pc = true
+  | cons i tl ⇒
+     let fetched ≝ fetch code_memory pc in
+     let 〈instr_pc, ticks〉 ≝ fetched in
+     let 〈instr,pc'〉 ≝ instr_pc in
+      eq_instruction instr i = true ∧ fetch_many code_memory final_pc pc' tl].
+
+lemma option_destruct_Some: ∀A,a,b. Some A a = Some A b → a=b.
+ #A #a #b #EQ destruct //
+qed.
+
+lemma pair_destruct: ∀A,B,a1,a2,b1,b2. pair A B a1 a2 = 〈b1,b2〉 → a1=b1 ∧ a2=b2.
+ #A #B #a1 #a2 #b1 #b2 #EQ destruct /2/
+qed. 
+
+axiom eq_bv_to_eq: ∀n.∀v1,v2: BitVector n. eq_bv … v1 v2 = true → v1=v2.
+
+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.
+ #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
+ >EQ2a >EQ2b -EQ2a EQ2b;
+  generalize in match (pc + |flatten … (map … assembly1 instructions)|); #final_pc
+  generalize in match pc elim instructions
+  [ #pc whd in ⊢ (% → %) #H >H @eq_bv_refl
+  | #i #tl #IH #pc #H whd cases (encoding_check_append … H); -H; #H1 #H2 whd
+    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
+    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
+    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % //
+    >(eq_bv_to_eq … K2) @IH @H2 ]
+qed.
+
+lemma fetch_assembly_pseudo:
+ ∀program,ppc,lookup_labels,lookup_datalabels.
+  ∀pc,pi,code_memory,instructions,len,assembled.
+   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 len (bitvector_of_nat … pc) instructions.
+ #program #ppc #lookup_labels #lookup_datalabels #pc #pi #code_memory #instructions #len #assembled
+ #EQ1 #EQ2 generalize in match EQ1 -EQ1; generalize in match pc -pc; elim instructions
+  [ #pc #EQ1 #H whd whd in EQ2:(???%); <EQ1 in EQ2; whd in ⊢ (???% → ?) #EQ2
+    cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2; #EQ2a #EQ2b >EQ2b
+    whd in ⊢ (% → %) #H >EQ2a <plus_n_O
+    (* OK, ARITHMETIC *) cases daemon
+   | #i #tl #IH #pc #EQ1 whd in EQ2:(???%); <EQ1 in EQ2; whd in ⊢ (???% → ?) #EQ2
+    cases (pair_destruct ?????? (option_destruct_Some … EQ2)) -EQ2 #EQ2a #EQ2b
+    change in EQ2b with (? = ?@flatten …) >EQ2b in IH ⊢ %; -assembled; #IH #H
+    cases (encoding_check_append … H); -H; #H1 #H2 whd
+    generalize in match (fetch_assembly pc i code_memory … (refl …) H1)
+    cases (fetch code_memory (bitvector_of_nat … pc)) #newi_pc #ticks whd in ⊢ (% → %)
+    cases newi_pc #newi #newpc whd in ⊢ (% → %) #K cases (conjunction_true … K) -K; #K1 #K2 % //
+    >(eq_bv_to_eq … K2) @IH
+     [ 
+     | @H2
+     ]
+  ]
+qed.
+
 (* This establishes the correspondence between pseudo program counters and
    program counters. It is at the heart of the proof. *)