Changeset 1831 for src/ASM/ASMCosts.ma

Timestamp:

Mar 13, 2012, 4:13:08 PM (8 years ago)

Author:

mulligan

Message:

small changes to asmcosts file to refactor proof

File:

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

src/ASM/ASMCosts.ma

@@ -1396 +1396 @@
     eqb l r = false → l ≠ r.
 
+axiom le_neq_to_lt:
+  ∀m, n: nat.
+    m ≤ n → m ≠ n → m < n.
+
 let rec traverse_code_internal
   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
@@ -1428 +1432 @@
     ] (refl … (lookup_opt … program_counter cost_labels)))
   ] (refl … program_size).
-  [1:
-    %
+  cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
+  [1,3,5,7,9,11,13:
+  |14:
+    cases daemon (* XXX: russell error here i think *)
+  |2:
+    #_ %
     [1:
       #pc #k #absurd1 #absurd2
@@ -1438 +1446 @@
       @⊥ normalize in k_pres; /2/
     ]
-  |2:
+  |4:
+    #S_assm
     cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
     [1:
-      
+      <NEW_PC' %
     |2:
       #new_program_counter_assm' >new_program_counter_assm'
+      <program_size_invariant <program_size_refl
+      <S_assm normalize <plus_n_Sm %
     ]
-  |3:
+  |6:
+    #_ assumption
+  |8:
+    #_ @(reachable_program_counter_witness lbl)
     assumption
-  |4:
-    @(reachable_program_counter_witness lbl)
-    assumption
+  |10:
+    #S_assm %
+    [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 #_
+        @(ind_hyp … lookup_opt_assm)
+        [1:
+          generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
+            (nat_of_bitvector … pc));
+          #hyp cases hyp
+          [1:
+            #relevant
+            generalize in match (eqb_true_to_refl … relevant);
+            #rewrite_assm <rewrite_assm
+            cases daemon
+            (* XXX: ??? *)
+          |2:
+            #relevant
+            generalize in match (eqb_false_to_not_refl … relevant);
+            #rewrite_assm
+            @⊥
+            cases rewrite_assm #relevant @relevant -relevant
+            -rewrite_assm -relevant -hyp
+            cases daemon
+            (* XXX: ??? *)
+          ]
+        |2:
+          generalize in match H2; <program_size_refl whd in ⊢ (??% → ?);
+          >plus_n_Sm in ⊢ (% → ?);
+          cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
+          [1:
+            <NEW_PC' %
+          |2:
+            #new_program_counter_assm' >new_program_counter_assm'
+            >S_assm #relevant assumption
+          ]
+        ]
+      ]
+    |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
+        ]
+      ]
+    ]
+  |12:
+    #S_assm %
+    [1:
+      #pc #k #H1 #H2 #lookup_opt_assm
+      whd >lookup_opt_assm
+    |2:
+    ]
+  ]
+    
   |5:
     %
@@ -1483 +1568 @@
         @(ind_hyp … lookup_opt_assm) 
         [1:
-          generalize in match (eqb_decidable (nat_of_bitvector … pc)
-            (nat_of_bitvector … new_program_counter'));
+          generalize in match (eqb_decidable (nat_of_bitvector … program_counter)
+            (nat_of_bitvector … pc));
           #hyp cases hyp
           [1:
             #relevant
             generalize in match (eqb_true_to_refl … relevant);
-            #refl_assm >refl_assm @le_n
+            #rewrite_assm <rewrite_assm
           |2:
             #relevant
             generalize in match (eqb_false_to_not_refl … relevant);
-            #refl_assm
-            cases refl_assm #refl_assm
+            #rewrite_assm
+            @⊥
+            cases rewrite_assm #relevant @relevant -relevant
+            -rewrite_assm -relevant -hyp
           ]
           (* XXX: case analysis over pc = new_program_counter' *)