Changeset 1576

Timestamp:

Nov 29, 2011, 5:22:37 PM (9 years ago)

Author:

mulligan

Message:

big changes to proofs, just two small cases remain and a few (dubious?) axioms

File:

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

src/ASM/CostsProof.ma

@@ -249 +249 @@
 qed.
 
-axiom current_instruction_cost_non_zero:
+axiom clock_execute_1:
   ∀s: Status.
-    current_instruction_cost s > 0.
-
-lemma le_monotonic_plus:
+    clock … (execute_1 s) = current_instruction_cost s + clock … s.
+
+axiom plus_minus_minus:
   ∀m, n, o: nat.
-    m ≤ n → m + o ≤ n + o.
-  #m #n #o #hyp /2/
-qed.
-
-lemma le_plus_to_minus_l:
+    m - (n + o) = (m - n) - o.
+
+axiom plus_le_le:
   ∀m, n, o: nat.
-    n ≤ o → m ≤ o - n → m + n ≤ o.
-  #m #n #o #le_hyp #hyp
-  generalize in match (le_monotonic_plus m (o - n) n hyp);
-  generalize in match (plus_minus_m_m o n le_hyp);
-  #assm <assm in ⊢ (% → ?); #finished assumption
-qed.
+    m + n ≤ o → n ≤ o.
     
-axiom minus_m_n_gt_o_O_le_n_m:
-  ∀m, n, o.
-    m - n = o → o > 0 → n ≤ m.
-(*  #m #n #o #eq_hyp <eq_hyp in ⊢ (% → ?);
-  normalize in ⊢ (% → ?);
-  >le_monot *)
-
 let rec compute_max_trace_label_label_cost_is_ok
   (cost_labels: BitVectorTrie costlabel 16)
@@ -313 +299 @@
         #the_status #assm
         whd in match eject; normalize nodelta
-        >assm %
+        cases(assm)
+        #eq_hyp #le_hyp
+        >eq_hyp %
       |2:
         cases(execute_1 start_status)
         #the_status #assm
         whd in match eject; normalize nodelta
-        @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status))
-        [1: assumption
-        |2: @(current_instruction_cost_non_zero start_status)
-        ]
+        cases(assm)
+        #eq_hyp #le_hyp
+        assumption
       ]
     |2:
@@ -332 +319 @@
         #the_status #assm
         whd in match eject; normalize nodelta
-        >assm %
+        cases(assm)
+        #eq_hyp #le_hyp
+        >eq_hyp %
       |2:
         cases(execute_1 start_status)
         #the_status #assm
         whd in match eject; normalize nodelta
-        @(minus_m_n_gt_o_O_le_n_m ? ? (current_instruction_cost start_status))
-        [1: assumption
-        |2: @current_instruction_cost_non_zero
-        ]
+        cases(assm)
+        #eq_hyp #le_hyp
+        assumption
       ]
     |3:
@@ -360 +348 @@
         #trace_any_label_eq #trace_any_label_le
         >trace_label_return_eq >trace_any_label_eq
-        >commutative_plus
-        
-        cut ((clock (BitVectorTrie Byte 16) status_after_fun_call
-  -clock (BitVectorTrie Byte 16) status_start_fun_call
-  +current_instruction_cost status_pre_fun_call
-  +(clock (BitVectorTrie Byte 16) status_final
-    -clock (BitVectorTrie Byte 16) status_after_fun_call) =
-          ((clock (BitVectorTrie Byte 16) status_after_fun_call
-            - clock (BitVectorTrie Byte 16) status_start_fun_call)
-          + (clock (BitVectorTrie Byte 16) status_final
-          - clock (BitVectorTrie Byte 16) status_after_fun_call))
-          + current_instruction_cost status_pre_fun_call))
-        [ 1:
-          cases daemon (* XXX: complete me *)
-        | 2:
-          #eq_hyp >eq_hyp
+        cases(is_next)
+        >(clock_execute_1 status_pre_fun_call) in match (clock … (execute_1 status_pre_fun_call));
+        >commutative_plus in match (
+          (current_instruction_cost status_pre_fun_call
+            + clock (BitVectorTrie Byte 16) status_pre_fun_call));
+        >plus_minus_minus
+        <(plus_minus_m_m (clock (BitVectorTrie Byte 16) status_after_fun_call
+  -clock (BitVectorTrie Byte 16) status_pre_fun_call) (current_instruction_cost status_pre_fun_call))
+        [1:
           >plus_minus_rearrangement_1
           [1:
-          |2, 3:
+            %
+          |2:
             assumption
+          |3:
+            generalize in match trace_label_return_le;
+            cases(is_next)
+            >(clock_execute_1 status_pre_fun_call)
+            @plus_le_le
           ]
+        |2:
+          cases daemon (* XXX: todo *)
         ]
       |2:
-        cases daemon (* XXX: complete me *)
+        cases(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
+          status_after_fun_call call_trace)
+        #trace_label_return_eq cases(is_next)
+        >clock_execute_1
+        #trace_label_return_le
+        lapply (plus_le_le … trace_label_return_le)
+        #trace_label_return_le'
+        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
+          status_final final_trace)
+        #trace_any_label_eq #trace_any_label_le
+        @(transitive_le (clock … status_pre_fun_call) (clock … status_after_fun_call) (clock … status_final))
+        assumption
       ]
     |4:
       #end_flag #status_pre #status_init #status_end #is_next
       #trace_any_label #is_other #is_not_costed
-      cases daemon (* XXX: complete me *)
+      change with (
+      let current_instruction_cost ≝ current_instruction_cost status_pre in
+      let tail_trace_cost ≝
+       compute_max_trace_any_label_cost cost_labels end_flag
+        status_init status_end trace_any_label
+      in
+        current_instruction_cost + tail_trace_cost) in ⊢ (?(??%?)?);
+      normalize nodelta;
+      @conj
+      [1:
+        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
+        status_init status_end trace_any_label)
+        #trace_any_label_eq #trace_any_label_le
+        >trace_any_label_eq
+        cases(is_next)
+        >commutative_plus
+        >clock_execute_1
+        >commutative_plus in match ((current_instruction_cost status_pre+clock (BitVectorTrie Byte 16) status_pre));
+        >plus_minus_minus
+        <plus_minus_m_m
+        [1: %
+        |2: cases daemon (* XXX: todo *)
+        ]
+      |2:
+        cases(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
+        status_init status_end trace_any_label)
+        #trace_any_label_eq
+        cases(is_next)
+        >clock_execute_1
+        @plus_le_le
+      ]
     ]
   |3: