Changeset 2754 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Mar 1, 2013, 10:26:31 AM (7 years ago)
Author:
sacerdot
Message:
  1. WARNING: I commented out one of James's function used in compiler.ma because it was undefined (partial commit). To be restored.
  2. The type of labelled_object_code programs now has a symbol table, used to generate the intensional events function call/return.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r2671 r2754  
    283283
    284284include alias "ASM/BitVectorTrie.ma".
    285 
    286 (*
    287 let rec compute_cost_trace_label_label
    288   (cm: BitVectorTrie Byte 16)
    289   (cost_labels: BitVectorTrie costlabel 16)
    290    (trace_ends_flag: trace_ends_with_ret)
    291     (start_status: Status cm) (final_status: Status cm)
    292       (the_trace: trace_label_label (ASM_abstract_status cm cost_labels) trace_ends_flag
    293         start_status final_status) on the_trace:
    294          list (Σk:costlabel. ∃pc: Word. lookup_opt … pc cost_labels = Some … k) ≝
    295   match the_trace with
    296   [ tll_base ends_flag initial final given_trace labelled_proof ⇒
    297      let pc ≝ program_counter ? cm initial in
    298      let label ≝
    299       match lookup_opt … pc cost_labels return λx: option ?. x ≠ None … → costlabel with
    300       [ None ⇒ λabs. ⊥
    301       | Some l ⇒ λ_. l ] labelled_proof in
    302       (mk_Sig ?? label ?)::compute_cost_trace_any_label cm cost_labels ends_flag initial final … given_trace
    303   ]
    304 and compute_cost_trace_any_label
    305   (cm: BitVectorTrie Byte 16)
    306   (cost_labels: BitVectorTrie costlabel 16)
    307   (trace_ends_flag: trace_ends_with_ret)
    308    (start_status: Status cm) (final_status: Status cm)
    309      (the_trace: trace_any_label (ASM_abstract_status cm cost_labels) trace_ends_flag start_status final_status)
    310        on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
    311   match the_trace with
    312   [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
    313   | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
    314       compute_cost_trace_label_return … call_trace
    315   | tal_base_return the_status _ _ _ ⇒ [ ]
    316   | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
    317      _ _ _ call_trace _ final_trace ⇒
    318       let call_cost_trace ≝ compute_cost_trace_label_return … call_trace in
    319       let final_cost_trace ≝ compute_cost_trace_any_label cm cost_labels end_flag … final_trace in
    320         call_cost_trace @ final_cost_trace
    321   | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
    322        compute_cost_trace_any_label cm cost_labels end_flag
    323         status_init status_end tail_trace
    324   ]
    325 and compute_cost_trace_label_return
    326   (cm: BitVectorTrie Byte 16)
    327   (cost_labels: BitVectorTrie costlabel 16)
    328   (start_status: Status cm) (final_status: Status cm)
    329     (the_trace: trace_label_return (ASM_abstract_status cm cost_labels) start_status final_status)
    330       on the_trace: list (Σk:costlabel. ∃pc. lookup_opt … pc cost_labels = Some … k) ≝
    331   match the_trace with
    332   [ tlr_base before after trace_to_lift ⇒ compute_cost_trace_label_label cm … trace_to_lift
    333   | tlr_step initial labelled final labelled_trace ret_trace ⇒
    334       let labelled_cost ≝ compute_cost_trace_label_label cm … labelled_trace in
    335       let return_cost ≝ compute_cost_trace_label_return cm … ret_trace in
    336         labelled_cost @ return_cost
    337   ].
    338  [1:
    339   %{pc} whd in match label;  generalize in match labelled_proof; whd in ⊢ (% → ?);
    340    whd in match (as_costed ??); whd in match (as_label ??); normalize nodelta
    341    cases (lookup_opt costlabel … (program_counter … initial) cost_labels)
    342    normalize
    343   [ #abs cases abs #absurd @⊥ @absurd % | // ]
    344  | cases abs #absurd @absurd % ]
    345 qed.
    346 *)
    347 
    348285include alias "arithmetics/nat.ma".
    349286include alias "basics/logic.ma".
    350 
    351287include alias "arithmetics/bigops.ma".
    352288
     
    737673
    738674lemma tech_cost_sum_eq_as_cost :
    739   ∀compiled_code: (list Byte) × (BitVectorTrie costlabel 16).
    740   let cost_labels ≝ \snd compiled_code in
     675  ∀compiled_code: labelled_object_code.
     676  let cost_labels ≝ \fst (\snd compiled_code) in
    741677  ∀cost_labels_injective:
    742678   (∀pc,pc',l.
    743      lookup_opt … pc (\snd  compiled_code) = Some … l
    744      → lookup_opt … pc' (\snd  compiled_code) = Some … l → pc = pc').
    745   let cost_map ≝ compute_costs (\fst compiled_code) (\snd compiled_code) cost_labels_injective in
     679     lookup_opt … pc cost_labels = Some … l
     680     → lookup_opt … pc' cost_labels = Some … l → pc = pc').
     681  let cost_map ≝ compute_costs (\fst compiled_code) (\fst (\snd compiled_code)) cost_labels_injective in
    746682  ∀codom_dom: (∀pc,k. lookup_opt … pc cost_labels = Some … k → present … k).
    747683  ∀trace.
Note: See TracChangeset for help on using the changeset viewer.