Changeset 977 for src/ASM/AssemblyProof.ma

Timestamp:

Jun 16, 2011, 12:12:59 PM (8 years ago)

Author:

sacerdot

Message:

#$%@#$@#$

File:

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

src/ASM/AssemblyProof.ma

@@ -1074 +1074 @@
 qed.
 
+lemma index_of_internal_Some_hit: ∀i,id.
+ ∀instr_list,n.
+  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
+   index_of_internal ? (instruction_matches_identifier id) (instr_list@[〈Some ? id,i〉]) n
+  = |instr_list| + n.
+ #i #id #instr_list elim instr_list
+  [ #n #_ whd in ⊢ (??%%) change with (if eq_bv … id id then ? else ? = ?) >eq_bv_refl %
+  | #hd #tl #IH #n whd in ⊢ (?% → ??%%) cases (instruction_matches_identifier id hd) normalize nodelta;
+    [ >does_not_occur_absurd #abs cases abs | #H applyS (IH (S n)) //]]
+qed.
+
 lemma address_of_word_labels_code_mem_None: ∀i,id,instr_list.
  occurs_exactly_once id (instr_list@[〈None …,i〉]) →
@@ -1089 +1100 @@
  #i #id #id' #instr_list #EQ #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)(??%?))
  >(index_of_internal_Some_miss … H) //
+qed.
+
+lemma address_of_word_labels_code_mem_Some_hit: ∀i,id,instr_list.
+  occurs_exactly_once id (instr_list@[〈Some ? id,i〉]) →
+   address_of_word_labels_code_mem (instr_list@[〈Some … id,i〉]) id
+   = bitvector_of_nat … (|instr_list|).
+ #i #id #instr_list #H whd in ⊢ (??%%) whd in ⊢ (??(??%?)?)
+ >(index_of_internal_Some_hit … H) //
 qed.
 
@@ -1120 +1139 @@
       let 〈ppc',pc_costs〉 ≝ ppc_pc_costs in
       let 〈pc',costs〉 ≝ pc_costs in
+       ppc' = length … pre ∧
        tech_pc_sigma00 pseudo_program pre = Some ? 〈ppc',pc'〉 ∧
        ∀id. occurs_exactly_once id pre →
@@ -1149 +1169 @@
    let 〈pc, costs〉 ≝ pc_costs in
     〈labels, costs〉.
- [3: whd % // #id normalize in ⊢ (% → ?) #abs @⊥ //
- | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2
-   cases construct in p4 #PC #CODE #JMEQ %
-   [ @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
+ [3: whd % [%] // #id normalize in ⊢ (% → ?) #abs @⊥ //
+ | whd generalize in match (sig2 … t) >p >p1 >p2 >p3 * * #IH0 #IH1 #IH2
+   cases construct in p4 #PC #CODE #JMEQ % [%]
+   [ >length_append <IH0 normalize; //
+   | @(tech_pc_sigma00_append_Some … IH1 (jmeq_to_eq … JMEQ))
    | #id normalize nodelta; -labels1; cases label; normalize nodelta
      [ #K <address_of_word_labels_code_mem_None [2:@K] @IH2 //
      | #l #H generalize in match (occurs_exactly_once_Some ???? H) in ⊢ ?;
        generalize in match (refl … (eq_bv ? l id)); cases (eq_bv … l id) in ⊢ (???% → %)
-        [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit
-          
+        [ #EQ #_ <(eq_bv_to_eq … EQ) >lookup_insert_hit >address_of_word_labels_code_mem_Some_hit 
+          <IH0 
         | #EQ change with (occurs_exactly_once ?? → ?) #K >lookup_insert_miss [2: /2/]
           <(address_of_word_labels_code_mem_Some_miss … EQ … H) @IH2 //]]]
- | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 *; #IH1 #IH2 
+ | (* dummy case *) @⊥ generalize in match (sig2 … t) >p >p1 >p2 >p3 * *; #IH0 #IH1 #IH2 
    @(tech_pc_sigma00_append_None … IH1 (jmeq_to_eq ??? p4)) ]
 qed.