Changeset 1579 for src/ASM/CostsProof.ma

Timestamp:

Dec 1, 2011, 2:11:37 PM (8 years ago)

Author:

mulligan

Message:

Finished proof with simpler statement, making everything a lot nicer

File:

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

src/ASM/CostsProof.ma

@@ -249 +249 @@
 qed.
 
-axiom clock_execute_1:
-  ∀s: Status.
-    clock … (execute_1 s) = current_instruction_cost s + clock … s.
-
-axiom plus_le_le:
+lemma m_le_plus_n_m:
+  ∀m, n: nat.
+    m ≤ n + m.
+  #m #n //
+qed.
+
+lemma n_plus_m_le_o_to_m_le_o:
   ∀m, n, o: nat.
-    m + n ≤ o → n ≤ o.
+    n + m ≤ o → m ≤ o.
+  #m #n #o #assm /2 by le_plus_b/
+qed.
+
+lemma m_minus_n_plus_o_m_minus_n_minus_o:
+  ∀m, n, o: nat.
+    m - (n + o) = m - n - o.
+  #m #n #o /2 by /
+qed.
+
+let rec compute_max_trace_label_label_cost_is_ok
+  (cost_labels: BitVectorTrie costlabel 16)
+   (trace_ends_flag: trace_ends_with_ret)
+    (start_status: Status) (final_status: Status)
+      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
+        start_status final_status) on the_trace:
+          clock … final_status = (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
+and compute_max_trace_any_label_cost_is_ok
+  (cost_labels: BitVectorTrie costlabel 16)
+  (trace_ends_flag: trace_ends_with_ret)
+   (start_status: Status) (final_status: Status)
+     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
+       on the_trace:
+         clock … final_status = (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace) + (clock … start_status) ≝ ?
+and compute_max_trace_label_return_cost_is_ok
+  (cost_labels: BitVectorTrie costlabel 16)
+  (start_status: Status) (final_status: Status)
+    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
+      on the_trace:
+        clock … final_status = (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace) + clock … start_status ≝ ?.
+  [1:
+    cases the_trace
+    #ends_flag #start_status #end_status #any_label_trace #is_costed
+    normalize @compute_max_trace_any_label_cost_is_ok
+  |2:
+    cases the_trace
+    [1,2:
+      #start_status #final_status #is_next #is_not_return try (#is_costed)
+      change with (current_instruction_cost start_status) in ⊢ (???(?%?));
+      cases(is_next)
+      cases(execute_1 start_status)
+      whd in match eject; normalize nodelta;
+      #the_status #assm >assm %
+    |3:
+      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
+      #status_final #is_next #is_call #is_after_return #call_trace #final_trace
+      change with (
+      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
+      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
+      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
+        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (???(?%?));
+      normalize nodelta;
+      >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
+          status_final final_trace)
+      >(compute_max_trace_label_return_cost_is_ok cost_labels status_start_fun_call
+        status_after_fun_call call_trace)
+      cases(is_next) in match (clock … status_start_fun_call);
+      cases(execute_1 status_pre_fun_call);
+      #the_status
+      whd in match eject; normalize nodelta;
+      #assm >assm
+      <associative_plus in ⊢ (??%?);
+      <commutative_plus in match (
+        compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
+          + compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace);
+      >associative_plus in ⊢ (??%?);
+      <commutative_plus in match (
+        compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace
+          + (current_instruction_cost status_pre_fun_call
+              + clock (BitVectorTrie Byte 16) status_pre_fun_call));
+      >associative_plus in ⊢ (??%?);
+      <commutative_plus in match (
+         clock (BitVectorTrie Byte 16) status_pre_fun_call
+           + compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final final_trace);
+      <(associative_plus (
+         (compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call call_trace)))
+      <associative_plus in ⊢ (??%?); %
+    |4:
+      #end_flag #status_pre #status_init #status_end #is_next
+      #trace_any_label #is_other #is_not_costed
+      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;
+      >(compute_max_trace_any_label_cost_is_ok cost_labels end_flag
+         status_init status_end trace_any_label)
+      cases(is_next) in match (clock … status_init);
+      cases(execute_1 status_pre)
+      #the_status whd in match eject; normalize nodelta;
+      #assm >assm <associative_plus in ⊢ (??%?);
+      >commutative_plus in match (
+        compute_max_trace_any_label_cost cost_labels end_flag status_init status_end trace_any_label
+          + current_instruction_cost status_pre);
+      %
+    ]
+  |3:
+    cases the_trace
+    [1:
+      #status_before #status_after #trace_to_lift
+      normalize @compute_max_trace_label_label_cost_is_ok
+    |2:
+      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
+      normalize
+      >(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
+      >(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
+      <associative_plus in ⊢ (??%?);
+      >commutative_plus in match (
+        compute_max_trace_label_return_cost cost_labels status_labelled status_final ret_trace
+          + compute_max_trace_label_label_cost cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
+      %
+    ]
+  ].
+qed.
     
 let rec compute_max_trace_label_label_cost_is_ok
@@ -291 +409 @@
       cases(is_next)
       @conj
+      cases(execute_1 start_status)
+      #the_status #assm
+      whd in match eject; normalize nodelta
+      >assm
       [1:
-        cases(execute_1 start_status)
-        #the_status #assm
-        whd in match eject; normalize nodelta
-        cases(assm)
-        #eq_hyp #le_hyp
-        >eq_hyp %
+        @minus_plus_m_m
       |2:
-        cases(execute_1 start_status)
-        #the_status #assm
-        whd in match eject; normalize nodelta
-        cases(assm)
-        #eq_hyp #le_hyp
-        assumption
+        @m_le_plus_n_m
       ]
     |2:
@@ -311 +423 @@
       cases(is_next)
       @conj
+      cases(execute_1 start_status)
+      #the_status #assm
+      whd in match eject; normalize nodelta
+      >assm
       [1:
-        cases(execute_1 start_status)
+        @minus_plus_m_m
+      |2:
+        @m_le_plus_n_m
+      ]
+    |3:
+      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
+      #status_final #is_next #is_call #is_after_return #call_trace #final_trace
+      change with (
+      let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in
+      let call_trace_cost ≝ compute_max_trace_label_return_cost … call_trace in
+      let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag … final_trace in
+        call_trace_cost + current_instruction_cost + final_trace_cost) in ⊢ (?(??%?)?);
+      normalize nodelta;
+      @conj
+      [1:
+        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 #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
+        >trace_any_label_eq >trace_label_return_eq
+        cases(is_next)
+        cases(execute_1 status_pre_fun_call)
         #the_status #assm
-        whd in match eject; normalize nodelta
-        cases(assm)
-        #eq_hyp #le_hyp
-        >eq_hyp %
+        whd in match eject; normalize nodelta;
+        >assm >commutative_plus in match
+          (current_instruction_cost status_pre_fun_call
+            + clock (BitVectorTrie Byte 16) status_pre_fun_call);
+        >m_minus_n_plus_o_m_minus_n_minus_o
+        <(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
+          lapply(transitive_le
+            (clock … status_pre_fun_call)
+            (clock … status_start_fun_call)
+            (clock … status_after_fun_call) ? trace_label_return_le)
+          [1,3:
+            cases(is_next)
+            cases(execute_1 status_pre_fun_call)
+            whd in match eject; normalize nodelta;
+            #the_new_status #assm >assm @m_le_plus_n_m
+          |2,4:
+            #assm assumption
+          ]
+        |2:
+          cases(is_next)
+          assumption
       |2:
-        cases(execute_1 start_status)
+        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(compute_max_trace_any_label_cost_is_ok cost_labels end_flag status_after_fun_call
+          status_final final_trace)
+        #trace_any_label_eq cases(is_next)
+        cases(execute_1 status_pre_fun_call)
         #the_status #assm
-        whd in match eject; normalize nodelta
-        cases(assm)
-        #eq_hyp #le_hyp
+        whd in match eject; normalize nodelta;
+        >assm #after_final_le #pre_after_le
+        lapply(n_plus_m_le_o_to_m_le_o
+          (clock … status_pre_fun_call)
+          (current_instruction_cost status_pre_fun_call)
+          (clock … status_after_fun_call) pre_after_le);
+        #pre_after_le'
+        @(transitive_le
+          (clock … status_pre_fun_call)
+          (clock … status_after_fun_call)
+          (clock … status_final))
         assumption
       ]
-    |3:
+    |*: cases daemon (* XXX: for now
       #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
       #status_final #is_next #is_call #is_after_return #call_trace #final_trace
@@ -414 +589 @@
         >clock_execute_1
         @plus_le_le
-      ]
+      ]*)
     ]
   |3: