Changeset 1567 for src/ASM

Timestamp:

Nov 25, 2011, 6:17:13 PM (10 years ago)

Author:

mulligan

Message:

more work on big proof, 2.5 cases left

File:

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

src/ASM/CostsProof.ma

@@ -222 +222 @@
 include alias "arithmetics/nat.ma".
 
-(*Useless now?
+(*
 lemma minus_m_n_minus_minus_plus_1:
   ∀m, n: nat.
@@ -229 +229 @@
  /3 by lt_plus_to_minus_r, plus_minus/
 qed.
+*)
 
 lemma plus_minus_rearrangement_1:
@@ -245 +246 @@
     (m - n) + (n - o) = m - o.
  /2 by plus_minus_rearrangement_1/
-qed.*)
-
-(*
+qed.
+
+axiom current_instruction_cost_non_zero:
+  ∀s: Status.
+    current_instruction_cost s > 0.
+    
+axiom minus_m_n_gt_o_0_le_n_m:
+  ∀m, n, o.
+  m - n = o → o > 0 → n ≤ m.
+
 let rec compute_max_trace_label_label_cost_is_ok
-  (cost_labels: BitVectorTrie Byte 16)
+  (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:
-          compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
-            (clock … final_status) - (clock … start_status) ≝ ?
+          And (compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
+            (clock … final_status) - (clock … start_status)) (clock … start_status ≤ clock … final_status) ≝ ?
 and compute_max_trace_any_label_cost_is_ok
-  (cost_labels: BitVectorTrie Byte 16)
+  (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:
-         compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
-           (clock … final_status) - (clock … start_status) ≝ ?
+         (compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
+           (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?
 and compute_max_trace_label_return_cost_is_ok
-  (cost_labels: BitVectorTrie Byte 16)
+  (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:
-        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
-          (clock … final_status) - (clock … start_status) ≝ ?.
+        (compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
+          (clock … final_status) - (clock … start_status)) ∧ (clock … start_status ≤ clock … final_status) ≝ ?.
   [1:
     cases the_trace
@@ -276 +284 @@
     normalize @compute_max_trace_any_label_cost_is_ok
   |2:
+    cases the_trace
+    [1:
+      #start_status #final_status #is_next #is_not_return #is_costed
+      change with (current_instruction_cost start_status) in ⊢ (?(??%?)?);
+      cases(is_next)
+      @conj
+      [1:
+        cases(execute_1 start_status)
+        #the_status #assm
+        whd in match eject; normalize nodelta
+        >assm %
+      |2:
+        cases(execute_1 start_status)
+        #the_status #assm
+        whd in match eject; normalize nodelta
+        @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status))
+        [1: assumption
+        |2: @current_instruction_cost_non_zero
+        ]
+      ]
+    |2:
+      #start_status #final_status #is_next #is_return
+      change with (current_instruction_cost start_status) in ⊢ (?(??%?)?);
+      cases(is_next)
+      @conj
+      [1:
+        cases(execute_1 start_status)
+        #the_status #assm
+        whd in match eject; normalize nodelta
+        >assm %
+      |2:
+        cases(execute_1 start_status)
+        #the_status #assm
+        whd in match eject; normalize nodelta
+        @(minus_m_n_gt_o_0_le_n_m ? ? (current_instruction_cost start_status))
+        [1: assumption
+        |2: @current_instruction_cost_non_zero
+        ]
+      ]
+    |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_label_return_eq >trace_any_label_eq
+        cases daemon (* XXX: complete me *)
+      |2:
+        cases daemon (* XXX: complete me *)
+      ]
+    |4:
+      #end_flag #status_pre #status_init #status_end #is_next
+      #trace_any_label #is_other #is_not_costed
+      cases daemon (* XXX: complete me *)
+    ]
   |3:
     cases the_trace
@@ -283 +357 @@
     |2:
       #status_initial #status_labelled #status_final #labelled_trace #ret_trace
-      normalize >compute_max_trace_label_label_cost_is_ok
-      >compute_max_trace_label_return_cost_is_ok
+      normalize
+      cases(compute_max_trace_label_label_cost_is_ok cost_labels doesnt_end_with_ret status_initial status_labelled labelled_trace);
+      #label_label_trace_equality #label_label_trace_leq
+      cases(compute_max_trace_label_return_cost_is_ok cost_labels status_labelled status_final ret_trace);
+      #label_return_trace_equality #label_return_trace_leq
+      >label_label_trace_equality >label_return_trace_equality
+      @conj
+      [2: @(transitive_le (clock (BitVectorTrie (Vector bool 8) 16) status_initial)
+            (clock (BitVectorTrie Byte 16) status_labelled)
+            (clock (BitVectorTrie (Vector bool 8) 16) status_final))
+      |1: @plus_minus_rearrangement_1
+      ]
+      assumption
     ]
-  ].
-*)
+  ]
+qed.
 
 (* XXX: work below here: *)