Changeset 1697 for src/ASM

Timestamp:

Feb 15, 2012, 6:02:22 PM (8 years ago)

Author:

mulligan

Message:

important bug found

File:

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

src/ASM/ASMCosts.ma

@@ -497 +497 @@
 qed.
 
-(* XXX: indexing bug re-emerges! *)
-example fetch_half_add:
-  ∀code_memory: BitVectorTrie Byte 16.
-  ∀cost_labels: BitVectorTrie costlabel 16.
-  ∀the_status : ASM_abstract_status code_memory cost_labels.
-    \snd (\fst (fetch code_memory (program_counter … the_status))) =
-      \snd (half_add 16 (program_counter … the_status)
-        (bitvector_of_nat … (\snd (fetch code_memory (program_counter … the_status))))).
-  cases daemon
-qed.
-
-axiom half_add_minus_right:
-  ∀size : nat.
-  ∀left : BitVector size.
-  ∀right: nat.
-  nat_of_bitvector … (\snd (half_add … left (bitvector_of_nat … right))) -
-    nat_of_bitvector … left = right.
-
 lemma minus_plus_cancel:
   ∀m, n : nat.
@@ -529 +511 @@
       program_counter … (execute_1 … start_status).
   cases daemon
-qed. (*
-  #code_memory #start_status
-  whd in match (execute_1 code_memory start_status);
-  whd in match (execute_1' code_memory start_status); normalize nodelta
-  cases (fetch code_memory (program_counter … start_status)) #instruction_pc #ticks
-  cases instruction_pc #instruction #pc normalize nodelta *)
+qed.
 
 lemma reachable_program_counter_to_0_lt_total_program_size:
@@ -1468 +1445 @@
 qed.
 
+lemma present_add_hit:
+  ∀tag, a, map, k, v.
+    present tag a (add tag a map k v) k.
+  #tag #a #map #k #v
+  whd >lookup_add_hit
+  % #absurd destruct
+qed.
+
+lemma present_add_miss:
+  ∀tag, a, map, k, k', v.
+    k' ≠ k → present tag a map k' → present tag a (add tag a map k v) k'.
+  #tag #a #map #k #k' #v #neq_assm #present_assm
+  whd >lookup_add_miss assumption
+qed.
+
 let rec traverse_code_internal
   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
@@ -1478 +1470 @@
         on program_size:
           Σcost_map: identifier_map CostTag nat.
+            (∀pc,k. nat_of_bitvector … program_counter < nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
               ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
@@ -1483 +1476 @@
   match program_size with
   [ O ⇒ empty_map …
-  | S program_size ⇒
-    let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in
-    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size ? good_program_witness in
+  | S program_size' ⇒ pi1 …
+  
+    (let 〈instruction, new_program_counter, ticks〉 ≝ fetch … code_memory program_counter in
+    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter fixed_program_size program_size' ? good_program_witness in
     match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
-    [ None ⇒ λlookup_refl. cost_mapping
+    [ None ⇒ λlookup_refl. pi1 … cost_mapping
     | Some lbl ⇒ λlookup_refl.
       let cost ≝ block_cost code_memory program_counter fixed_program_size cost_labels ? good_program_witness in
         add … cost_mapping lbl cost
-    ] (refl … (lookup_opt … program_counter cost_labels))
+    ] (refl … (lookup_opt … program_counter cost_labels)))
   ].
-  [3:
+  [2:
+    @pi2
+  |4:
     @(reachable_program_counter_witness lbl)
     assumption
-  |4:
+  |3:
     assumption
   |1:
-    #k #k_pres
-    @⊥ normalize in k_pres; /2/
-  |2:
-    #k #k_pres
-    @(eq_identifier_elim … k lbl)
+    %
     [1:
-      #eq_assm %{program_counter} #lookup_opt_assm
-      %{(reachable_program_counter_witness …)} try assumption
-      >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
+      #pc #k #absurd1 #absurd2
+      @⊥ lapply(lt_to_not_le … absurd1) #absurd
+      cases absurd #absurd @absurd
+      @(transitive_le … absurd2) @le_S @le_n
     |2:
-      #neq_assm 
-      cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
-      cases (ind_hyp k ?)
-      [2:
-        @(present_add_present … present_assm) assumption
-      |1:
-        #program_counter' #ind_hyp' %{program_counter'}
-        #relevant cases (ind_hyp' relevant) #reachable_witness'
-        #ind_hyp'' %{reachable_witness'} >ind_hyp''
-        @sym_eq @lookup_present_add_miss assumption
+      #k #k_pres
+      @⊥ normalize in k_pres; /2/
+    ]
+  |5:
+    %
+    [2:
+      #k #k_pres
+      @(eq_identifier_elim … k lbl)
+      [1:
+        #eq_assm %{program_counter} #lookup_opt_assm
+        %{(reachable_program_counter_witness …)} try assumption
+        >eq_assm in k_pres ⊢ (???%); #k_pres >lookup_present_add_hit %
+      |2:
+        #neq_assm 
+        cases cost_mapping in k_pres; #cost_mapping' #ind_hyp #present_assm
+        cases ind_hyp #_ #relevant cases (relevant k ?)
+        [2:
+          @(present_add_present … present_assm) assumption
+        |1:
+          #program_counter' #ind_hyp' %{program_counter'}
+          #relevant cases (ind_hyp' relevant) #reachable_witness'
+          #ind_hyp'' %{reachable_witness'} >ind_hyp''
+          @sym_eq @lookup_present_add_miss assumption
+        ]
       ]
-    ]
+    |1:
+      #pc #k #H1 #H2 #lookup_opt_assm @(eq_identifier_elim … k lbl)
+      [1:
+        #eq_assm >eq_assm
+        cases cost_mapping #cost_mapping' * #ind_hyp #_
+        @present_add_hit 
+      |2:
+        #neq_assm @present_add_miss try assumption
+        cases cost_mapping #cost_mapping' * #ind_hyp #_
+        cases daemon (* XXX: !!! *)
+      ]
+    ]
+  |6:
   ]
 qed.