Changeset 1935 for src/common


Ignore:
Timestamp:
May 10, 2012, 5:13:34 PM (8 years ago)
Author:
mulligan
Message:

Generalized some lemma in ASM/CostsProof.ma to work on abstract statuses, moving the abstract version in to common/StructuredTraces.ma. Ported rest of proof in ASM/CostsProof.ma to use new, generalized lemma.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/StructuredTraces.ma

    r1927 r1935  
    44include "common/CostLabel.ma".
    55include "utilities/option.ma".
    6 include "basics/lists/listb.ma".
    76include "ASM/Util.ma".
    8 
    9 inductive status_class : Type[0] ≝
    10 | cl_return : status_class
    11 | cl_jump   : status_class
    12 | cl_call   : status_class
    13 | cl_other : status_class.
     7include "ASM/Interpret.ma".
    148
    159record abstract_status : Type[1] ≝
     
    2418  ; as_final: as_status → Prop
    2519}.
     20
     21definition ASM_abstract_status: ∀code_memory. BitVectorTrie costlabel 16 → abstract_status ≝
     22  λcode_memory.
     23  λcost_labels.
     24    mk_abstract_status
     25      (Status code_memory)
     26      (λs,s'. (execute_1 … s) = s')
     27      word_deqset
     28      (program_counter …)
     29      (λs,class. ASM_classify … s = class)
     30      (current_instruction_label code_memory cost_labels)
     31      (next_instruction_properly_relates_program_counters code_memory)
     32      ?.
     33  cases daemon (* XXX: is final predicate *)
     34qed.
    2635
    2736(* temporary alias for backward compatibility *)
     
    432441    tal_rel … tl1 tal2 (* <- this makes it many to many *)
    433442  ].
     443
     444include "ASM/BitVectorTrie.ma".
     445include "ASM/Status.ma".
     446include "ASM/Fetch.ma".
     447
     448let rec as_compute_cost_trace_label_label
     449  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
     450    (start_status: S) (final_status: S)
     451      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
     452        on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
     453  match the_trace with
     454  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
     455      let label ≝
     456        match as_label … initial return λx: option costlabel. x ≠ None costlabel → ? with
     457        [ None ⇒ λabs. ⊥
     458        | Some l ⇒ λ_. l
     459        ] labelled_proof
     460      in
     461        (mk_Sig … label ?)::as_compute_cost_trace_any_label S ends_flag initial final given_trace
     462  ]
     463and as_compute_cost_trace_any_label
     464  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
     465    (start_status: S) (final_status: S)
     466      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
     467        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
     468  match the_trace with
     469  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
     470  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
     471      as_compute_cost_trace_label_return … call_trace
     472  | tal_base_return the_status _ _ _ ⇒ [ ]
     473  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
     474    _ _ _ call_trace _ final_trace ⇒
     475    let call_cost_trace ≝ as_compute_cost_trace_label_return … call_trace in
     476    let final_cost_trace ≝ as_compute_cost_trace_any_label … end_flag … final_trace in
     477        call_cost_trace @ final_cost_trace
     478  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
     479      as_compute_cost_trace_any_label … tail_trace
     480  ]
     481and as_compute_cost_trace_label_return
     482  (S: abstract_status)
     483    (start_status: S) (final_status: S)
     484      (the_trace: trace_label_return S start_status final_status)
     485        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
     486  match the_trace with
     487  [ tlr_base before after trace_to_lift ⇒
     488      as_compute_cost_trace_label_label … trace_to_lift
     489  | tlr_step initial labelled final labelled_trace ret_trace ⇒
     490    let labelled_cost ≝ as_compute_cost_trace_label_label … doesnt_end_with_ret … labelled_trace in
     491    let return_cost ≝ as_compute_cost_trace_label_return … ret_trace in
     492        labelled_cost @ return_cost
     493  ].
     494  [2:
     495    cases abs -abs #abs @abs %
     496  |1:
     497    %{initial} whd in match label;
     498    generalize in match labelled_proof; whd in ⊢ (% → ?);
     499    cases (as_label S initial)
     500    [1:
     501      #absurd @⊥ cases absurd -absurd #absurd @absurd %
     502    |2:
     503      #costlabel normalize nodelta #_ %
     504    ]
     505  ]
     506qed.
Note: See TracChangeset for help on using the changeset viewer.