Changeset 3498 for LTS


Ignore:
Timestamp:
Sep 25, 2014, 3:49:58 PM (5 years ago)
Author:
sacerdot
Message:

Much nicer statement.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3497 r3498  
    1  include "costs.ma".
     1include "costs.ma".
    22include "basics/lists/list.ma".
    33include "../src/utilities/option.ma".
     
    876876qed.
    877877
    878 check labels_pc
    879 
    880878lemma i_act_in_map :  ∀p,prog,iact,l1,l2.
    881879mem ? 〈a_non_functional_label iact,O〉 (labels_pc p prog l1 l2 iact O).
     
    885883qed.
    886884
    887 lemma static_dynamic : ∀p,p',prog.
    888 ∀abs_t : abstract_transition_sys (m … p').∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
    889 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t
     885notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }.
     886interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x).
     887
     888coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?.
     889
     890lemma static_dynamic :
     891(* Given an assembly program *)
     892∀p,p',prog.
     893
     894(* Given a Galois connection to an abstract transition system *)
     895∀abs_t : abstract_transition_sys (m … p').
     896∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
     897∀R : static_galois … (asm_static_analisys_data … prog …
    890898 (λi.match i with [None ⇒ e …
    891899                  |Some x ⇒ instr_m x
    892                   ])) .∀mT,map1.
    893 ∀EQmap : static_analisys p ? instr_m mT prog = return map1.
    894 ∀st1,st2 : vm_ass_state p p'.
    895 ∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2.
    896 terminated_trace … t →
    897 ∀k.
    898 pre_measurable_trace … t →
    899 block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
    900 ∀a1.rel_galois … good st1 a1 →
    901 ∀labels.
    902 labels = dependent_map CostLabel ? (chop … (get_costlabels_of_trace …  t)) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
    903 rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)).
     900                  ])).
     901
     902(* If the static analysis does not fail *)
     903∀mT,map1. ∀EQmap : static_analisys … instr_m mT prog = return map1.
     904
     905(* For every pre_measurable, terminated trace *)
     906∀st1,st2. ∀t: raw_trace (asm_operational_semantics … prog) … st1 st2.
     907 terminated_trace … t → pre_measurable_trace … t →
     908
     909(* Let k be the statically computed abstract action of the prefix of the trace
     910   up to the first label *)
     911∀k.block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k →
     912
     913(* Given an abstract state in relation with the first state of the trace *)
     914∀a1.R st1 a1 →
     915
     916(* Let labels be the costlabels observed in the trace, excluding the last one *)
     917let labels ≝ chop … (get_costlabels_of_trace …  t) in
     918
     919(* Let abs_actions be the list of statically computed abstract actions
     920   associated to each label in labels. *)
     921∀abs_actions.
     922 abs_actions =
     923  dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
     924
     925(* The final state of the trace is in relation with the one obtained by
     926   first applying k to a1, and then applying every semantics in abs_trace. *)
     927R st2 (〚abs_actions〛 (〚k〛 a1)).
     928
    904929[2: @hide_prf
    905930    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
     
    914939]   
    915940lapply Hlabelled lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
    916 [ * [3: #st] #l #prf #H1 #k #_ whd in ⊢ (??%? → ?);
     941[ * [3: #st] #l #prf #H1 #_ #k whd in ⊢ (??%? → ?);
    917942  [3: cases prf
    918943  |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?);
    919944      lapply(instr_map_ok … good … prf … rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] *
    920945      #EQpc #EQ destruct #H #EQ destruct >act_neutral >act_neutral normalize in H;
    921       <(act_neutral ?? (act_abs ? abs_t) a1) @H
     946      <(act_neutral … (act_abs …) a1) @H
    922947  | @eqb_elim normalize nodelta
    923948    [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels whd in ⊢ (??%% → ?);
     
    974999    ]
    9751000  ]
    976   #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #k #pre_meas whd in ⊢ (??%? → ?);
     1001  #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #pre_meas #k whd in ⊢ (??%? → ?);
    9771002  >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind |3,6: ]
    9781003  >dependent_map_append
Note: See TracChangeset for help on using the changeset viewer.