Changeset 1561 for src/ASM

Timestamp:

Nov 25, 2011, 1:13:15 PM (10 years ago)

Author:

sacerdot

Message:

More dependent types to accomodate the statement.

File:

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

src/ASM/CostsProof.ma

@@ -3 +3 @@
 include "ASM/Status.ma".
 include "common/StructuredTraces.ma".
-
-definition current_instruction ≝
-  λs: Status.
-  let pc ≝ program_counter … s in
-  \fst (\fst (fetch … (code_memory … s) pc)).
-
-definition ASM_classify: Status → status_class ≝
- λs.
-  match current_instruction s with
-   [ RealInstruction pre ⇒
-     match pre with 
-      [ RET ⇒ cl_return
-      | JZ _ ⇒ cl_jump
-      | JNZ _ ⇒ cl_jump
-      | JC _ ⇒ cl_jump
-      | JNC _ ⇒ cl_jump
-      | JB _ _ ⇒ cl_jump
-      | JNB _ _ ⇒ cl_jump
-      | JBC _ _ ⇒ cl_jump
-      | CJNE _ _ ⇒ cl_jump
-      | DJNZ _ _ ⇒ cl_jump
-      | _ ⇒ cl_other
-      ]
-   | ACALL _ ⇒ cl_call
-   | LCALL _ ⇒ cl_call
-   | JMP _ ⇒ cl_call
-   | AJMP _ ⇒ cl_jump
-   | LJMP _ ⇒ cl_jump
-   | SJMP _ ⇒ cl_jump
-   | _ ⇒ cl_other
-   ].
-
-definition current_instruction_is_labelled ≝
-  λcost_labels: BitVectorTrie costlabel 16.
-  λs: Status.
-  let pc ≝ program_counter … s in
-    match lookup_opt … pc cost_labels with
-    [ None ⇒ False
-    | _    ⇒ True
-    ].
-
-definition label_of_current_instruction:
- BitVectorTrie costlabel 16 → Status → list costlabel
- ≝
-  λcost_labels,s.
-  let pc ≝ program_counter … s in
-    match lookup_opt … pc cost_labels with
-    [ None ⇒ []
-    | Some l ⇒ [l]
-    ].
-
-definition next_instruction_properly_relates_program_counters ≝
-  λbefore: Status.
-  λafter : Status.
-  let size ≝ current_instruction_cost before in
-  let pc_before ≝ program_counter … before in
-  let pc_after ≝ program_counter … after in
-  let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in
-    sum = pc_after.
-
-definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
- λcost_labels.
-  mk_abstract_status
-   Status
-   (λs,s'. eject … (execute_1 s) = s')
-   (λs,class. ASM_classify s = class)
-   (current_instruction_is_labelled cost_labels)
-   next_instruction_properly_relates_program_counters.
 
 (*
@@ -290 +222 @@
 include alias "arithmetics/nat.ma".
 
-(*
+(*Useless now?
 lemma minus_m_n_minus_minus_plus_1:
   ∀m, n: nat.
@@ -297 +229 @@
  /3 by lt_plus_to_minus_r, plus_minus/
 qed.
-*)
 
 lemma plus_minus_rearrangement_1:
@@ -314 +245 @@
     (m - n) + (n - o) = m - o.
  /2 by plus_minus_rearrangement_1/
-qed.
+qed.*)
 
 (*
@@ -345 +276 @@
     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
-      normalize nodelta;
-      change with (
-        let current_instruction_cost ≝ current_instruction_cost start_status in 
-        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels start_fun_call after_fun_call call_trace in 
-        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag after_fun_call final final_trace in 
-        call_trace_cost+current_instruction_cost+final_trace_cost
-      ) in ⊢ (??%?);
-    |2:
-      #start_status #final_status #is_next #is_return
-    |3:
-      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
-      #status_final #is_next #is_call #is_after_return #fun_call_trace #after_fun_call_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 cost_labels status_start_fun_call status_after_fun_call fun_call_trace in 
-        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final after_fun_call_trace in 
-          call_trace_cost+current_instruction_cost+final_trace_cost) in ⊢ (??%?);
-      normalize nodelta;
-      >compute_max_trace_label_return_cost_is_ok
-      >compute_max_trace_any_label_cost_is_ok
-    |4:
-    ]
   |3:
     cases the_trace
@@ -379 +285 @@
       normalize >compute_max_trace_label_label_cost_is_ok
       >compute_max_trace_label_return_cost_is_ok
-      >plus_minus_rearrangement_1
-      [1: %
-      |2:
-      |3:
-      ]
     ]
   ].
@@ -536 +437 @@
     (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: list costlabel ≝
+        start_status final_status) on the_trace:
+         list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
   match the_trace with
   [ tll_base ends_flag initial final given_trace labelled_proof ⇒
@@ -544 +446 @@
       [ None ⇒ λabs. ⊥
       | Some l ⇒ λ_. l ] labelled_proof in
-     label::compute_cost_trace_any_label … given_trace
+     (dp … label ?)::compute_cost_trace_any_label … given_trace
   ]
 and compute_cost_trace_any_label
@@ -551 +453 @@
    (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: list costlabel ≝
+       on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
   match the_trace with
   [ tal_base_not_return the_status _ _ _ _ ⇒ []
@@ -568 +470 @@
   (start_status: Status) (final_status: Status)
     (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
-      on the_trace: list costlabel ≝
+      on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
   match the_trace with
   [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label … trace_to_lift
@@ -576 +478 @@
         labelled_cost @ return_cost
   ].
-//
+ [ %{pc} whd in match label;  generalize in match labelled_proof; whd in ⊢ (% → ?);
+  cases (lookup_opt costlabel … pc cost_labels) normalize
+  [ #abs cases abs | // ]
+ | // ]
 qed.
 
@@ -595 +500 @@
    start_status final_status the_trace.
 
-include "arithmetics/bigops.ma".
-
-lemma foo:
+(* To be moved elsewhere*)
+lemma le_S_n_m_to_le_n_m: ∀n,m. S n ≤ m → n ≤ m.
+ #n #m #H change with (pred (S n) ≤ m) @(transitive_le ? (S n)) //
+qed.
+
+(* Here I would like to use arithmetics/bigops.ma, but it requires the
+   function f to be total on nat, which is not the case here *)
+let rec bigplus0 (b:nat) (f: ∀n:nat. n < b → nat) (n:nat) on n ≝
+  match n return λn.n < b → nat with
+   [ O ⇒ λ_. 0
+   | S k ⇒ λH. f k ? + bigplus0 b f k ?
+   ].
+ @(le_S_n_m_to_le_n_m … H)
+qed.
+
+definition bigplus ≝
+ λn,f.
+ match n return λx. x = n → nat with
+ [ O ⇒ λ_. 0
+ | S m ⇒ λH. bigplus0 n f m ? ] (refl … n).
+ //
+qed.
+
+lemma compute_max_trace_label_return_cost_ok_with_trace:
  ∀cost_labels: BitVectorTrie costlabel 16.
- ∀cost_labels_inv: identifier_map CostTag Word.
+ ∀cost_map: identifier_map CostTag nat.
  ∀initial,final.
  ∀trace: trace_label_return (ASM_abstract_status cost_labels) initial final.
-  let dummy ≝ an_identifier ? one in
+ ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … cost_map k).
+ ∀dom_codom:(∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
+   block_cost (code_memory … initial) cost_labels pc 2^16 =
+   lookup_present … k_pres).
   let ctrace ≝ compute_cost_trace_label_return … trace in
   compute_max_trace_label_return_cost … trace =
-   \big [ plus, 0 ]_{ i < |ctrace| }
-    (block_cost (code_memory … initial) cost_labels
-     (lookup_present … cost_labels_inv (nth i ? ctrace dummy) ?) 2^16).
- [2: cases daemon (* ALL LABELS MUST BE PRESENT *)
- | #cost_labels #cost_labels_inv #initial #final #trace
-   letin dummy ≝ (an_identifier CostTag one) normalize nodelta
-   whd in match 
+   bigplus (|ctrace|) (λi,H.lookup_present … cost_map (nth_safe ? i ctrace H) ?).
+ [2: cases (nth_safe … i ctrace H) normalize #id * #id_pc #K
+   lapply (codom_dom … K) #k_pres //
+ | #cost_labels #costmap #initial #final #trace #codom_dom #dom_codom normalize nodelta
+   whd in match
 
 lemma