Changeset 1549 for src/ASM


Ignore:
Timestamp:
Nov 24, 2011, 11:11:30 AM (8 years ago)
Author:
mulligan
Message:

removed cruft from costsproof.ma file so claudio can work in parallel

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1548 r1549  
    306306
    307307let rec compute_max_trace_label_label_cost_is_ok
     308  (cost_labels: BitVectorTrie Byte 16)
     309   (trace_ends_flag: trace_ends_with_ret)
     310    (start_status: Status) (final_status: Status)
     311      (the_trace: trace_label_label (ASM_abstract_status cost_labels) trace_ends_flag
     312        start_status final_status) on the_trace:
     313          compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
     314            (clock … final_status) - (clock … start_status) ≝ ?
     315and compute_max_trace_any_label_cost_is_ok
     316  (cost_labels: BitVectorTrie Byte 16)
     317  (trace_ends_flag: trace_ends_with_ret)
     318   (start_status: Status) (final_status: Status)
     319     (the_trace: trace_any_label (ASM_abstract_status cost_labels) trace_ends_flag start_status final_status)
     320       on the_trace:
     321         compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
     322           (clock … final_status) - (clock … start_status) ≝ ?
     323and compute_max_trace_label_return_cost_is_ok
     324  (cost_labels: BitVectorTrie Byte 16)
     325  (start_status: Status) (final_status: Status)
     326    (the_trace: trace_label_return (ASM_abstract_status cost_labels) start_status final_status)
     327      on the_trace:
     328        compute_max_trace_label_return_cost cost_labels start_status final_status the_trace =
     329          (clock … final_status) - (clock … start_status) ≝ ?.
     330  [1:
     331    cases the_trace
     332    #ends_flag #start_status #end_status #any_label_trace #is_costed
     333    normalize @compute_max_trace_any_label_cost_is_ok
     334  |2:
     335  |3:
     336    cases the_trace
     337    [1:
     338      #status_before #status_after #trace_to_lift
     339      normalize @compute_max_trace_label_label_cost_is_ok
     340    |2:
     341      #status_initial #status_labelled #status_final #labelled_trace #ret_trace
     342      normalize >compute_max_trace_label_label_cost_is_ok
     343      >compute_max_trace_label_return_cost_is_ok
     344    ]
     345  ].
     346
     347(*
     348let rec compute_max_trace_label_label_cost_is_ok
    308349  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
    309350    (start_status: Status) (final_status: Status)
     
    312353        compute_max_trace_label_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    313354          (clock … final_status) - (clock … start_status) ≝ ?
    314 and compute_max_trace_label_label_pre_cost_is_ok
     355and compute_max_trace_any_label_pre_cost_is_ok
    315356  (cost_labels: BitVectorTrie Byte 16) (trace_ends_flag: trace_ends_with_ret)
    316357    (start_status: Status) (final_status: Status)
    317       (the_trace: trace_label_label_pre cost_labels trace_ends_flag start_status final_status)
     358      (the_trace: trace_any_label cost_labels trace_ends_flag start_status final_status)
    318359        on the_trace:
    319           compute_max_trace_label_label_pre_cost cost_labels trace_ends_flag start_status final_status the_trace =
     360          compute_max_trace_any_label_cost cost_labels trace_ends_flag start_status final_status the_trace =
    320361            (clock … final_status) - (clock … start_status) ≝ ?
    321362and compute_max_trace_label_return_cost_is_ok
     
    389430    ]
    390431  ]
    391 qed.
    392        
    393 let rec compute_max_trace_label_ret_cost_is_ok
    394   (cost_labels: BitVectorTrie Byte 16) (start_status: Status) (final_status: Status)
    395     (the_trace: trace_label_return cost_labels start_status final_status)
    396       on the_trace:
    397         compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
    398         (clock … final_status) - (clock … start_status) ≝
    399   match the_trace with
    400   [ tlr_base before after trace_to_lift ⇒ ?
    401   | tlr_step initial pre_fun_call pre_fun_call_trace start_fun_call end_fun_call
    402       fun_call_trace pre_start_fun_call_coherence ⇒ ?
    403   ]
    404 and compute_max_trace_label_label_pre_cost_is_ok
    405   (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
    406     (start_status: Status) (final_status: Status)
    407       (the_trace: trace_label_label_pre cost_labels ends_flag start_status final_status)
    408         on the_trace:
    409           compute_max_trace_label_label_pre_cost cost_labels ends_flag start_status final_status the_trace =
    410             (clock … final_status) - (clock … start_status) ≝
    411   match the_trace with
    412   [ tllp_base_not_return the_status not_return not_jump not_cost_label ⇒ ?
    413   | tllp_base_return the_status is_return ⇒ ?
    414   | tllp_base_jump the_status cost_label is_jump is_cost ⇒ ?
    415   | tllp_step_call end_flag pre_fun_call start_fun_call end_fun_call after_fun_call final
    416       fun_call_trace is_call statuses_related pre_start_fun_call_coherence
    417       end_after_fun_call_coherence after_fun_call_trace ⇒ ?
    418   | tllp_step_default end_flag start initial end initial_end_trace not_call
    419       not_jump not_return not_cost ⇒ ?
    420   ]
    421 and compute_max_trace_label_label_cost_is_ok
    422   (cost_labels: BitVectorTrie Byte 16) (ends_flag: trace_ends_with_ret)
    423     (start_status: Status) (final_status: Status)
    424       (the_trace: trace_label_label cost_labels ends_flag start_status final_status)
    425         on the_trace:
    426           compute_max_trace_label_label_cost cost_labels ends_flag start_status final_status the_trace =
    427             (clock … final_status) - (clock … start_status) ≝
    428   match the_trace with
    429   [ tll_base ends_flag initial final given_trace labelled_proof ⇒ ?
    430   ].
    431   [8: @(compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag initial final given_trace)
    432   |1: @(compute_max_trace_label_label_cost_is_ok cost_labels ends_with_ret before after trace_to_lift)
    433   |4: normalize
    434       @minus_n_n
    435   |3: normalize
    436       @minus_n_n
    437   |5: normalize
    438       @minus_n_n
    439   |6: letin fun_call_cost_ok ≝ (compute_max_trace_label_ret_cost_is_ok cost_labels start_fun_call end_fun_call fun_call_trace)
    440       letin the_trace_cost_ok ≝ (compute_max_trace_label_label_pre_cost_is_ok cost_labels ends_flag start_status final_status the_trace)
    441   |*:
    442   ]
    443 qed.
    444  
    445 lemma compute_max_trace_label_ret_cost_is_ok:
    446   ∀cost_labels: BitVectorTrie Byte 16.
    447   ∀start_status: Status.
    448   ∀final_status: Status.
    449   ∀the_trace: trace_label_return cost_labels start_status final_status.
    450     compute_max_trace_label_ret_cost cost_labels start_status final_status the_trace =
    451       (clock … final_status) - (clock … start_status).
    452   #COST_LABELS #START_STATUS #FINAL_STATUS #THE_TRACE
    453   elim THE_TRACE
    454 
    455 lemma trace_lab_rec_cost_ok:
    456  ∀p: trace_lab_rec.
    457   trace_lab_rec_cost p = Timer (last p) - Timer (first p).
     432qed. *)
     433
     434(* XXX: work below here: *)
    458435
    459436let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
Note: See TracChangeset for help on using the changeset viewer.