Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3497 r3498 1 1 include "costs.ma". 2 2 include "basics/lists/list.ma". 3 3 include "../src/utilities/option.ma". … … 876 876 qed. 877 877 878 check labels_pc879 880 878 lemma i_act_in_map : ∀p,prog,iact,l1,l2. 881 879 mem ? 〈a_non_functional_label iact,O〉 (labels_pc p prog l1 l2 iact O). … … 885 883 qed. 886 884 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 885 notation "〚 term 19 C 〛 term 90 A" with precedence 10 for @{ 'sem $C $A }. 886 interpretation "act_abs" 'sem f x = (act ?? (act_abs ??) f x). 887 888 coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?. 889 890 lemma 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 … 890 898 (λi.match i with [None ⇒ e … 891 899 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 *) 917 let 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. *) 927 R st2 (〚abs_actions〛 (〚k〛 a1)). 928 904 929 [2: @hide_prf 905 930 cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) * … … 914 939 ] 915 940 lapply 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 ⊢ (??%? → ?); 917 942 [3: cases prf 918 943 2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?); 919 944 lapply(instr_map_ok … good … prf … rel_fin) [ %] cases st2 in prf; st2 [3: #st2] * 920 945 #EQpc #EQ destruct #H #EQ destruct >act_neutral >act_neutral normalize in H; 921 <(act_neutral ?? (act_abs ? abs_t) a1) @H946 <(act_neutral … (act_abs …) a1) @H 922 947  @eqb_elim normalize nodelta 923 948 [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels whd in ⊢ (??%% → ?); … … 974 999 ] 975 1000 ] 976 #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab # k #pre_measwhd in ⊢ (??%? → ?);1001 #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #pre_meas #k whd in ⊢ (??%? → ?); 977 1002 >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind 3,6: ] 978 1003 >dependent_map_append
Note: See TracChangeset
for help on using the changeset viewer.