Changeset 3499
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3498 r3499 907 907 terminated_trace … t → pre_measurable_trace … t → 908 908 909 (* Let labels be the costlabels observed in the trace, excluding the last one *) 910 let labels ≝ chop … (get_costlabels_of_trace … t) in 911 909 912 (* Let k be the statically computed abstract action of the prefix of the trace 910 913 up to the first label *) 911 914 ∀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) in918 915 919 916 (* Let abs_actions be the list of statically computed abstract actions … … 923 920 dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) → 924 921 922 (* Given an abstract state in relation with the first state of the trace *) 923 ∀a1.R st1 a1 → 924 925 925 (* The final state of the trace is in relation with the one obtained by 926 926 first applying k to a1, and then applying every semantics in abs_trace. *) … … 933 933 @(proj2 … (static_analisys_ok … EQmap … Hmem)) 934 934 ] 935 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * #l1 * #prf1 * #EQ destruct 936 #Hlabelled >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) 935 #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * 936 #l1 * #prf1 * #EQ destruct #Hlabelled 937 >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) 937 938 [2: >get_cost_label_append >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled) 938 #c #EQc >EQc // 939 ] 939 #c #EQc >EQc // ] 940 940 lapply Hlabelled lapply prf1 prf1 lapply l1 l1 elim t1 st3 941 941 [ * [3: #st] #l #prf #H1 #_ #k whd in ⊢ (??%? → ?); 942 942 [3: cases prf 943 2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?); 943 2: whd in ⊢ (??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); #EQlabels 944 #a1 #rel_fin 944 945 lapply(instr_map_ok … good … prf … rel_fin) [ %] cases st2 in prf; st2 [3: #st2] * 945 #EQpc #EQ destruct #H #EQ destruct>act_neutral >act_neutral normalize in H;946 #EQpc #EQ destruct #H >act_neutral >act_neutral normalize in H; 946 947 <(act_neutral … (act_abs …) a1) @H 947 948  @eqb_elim normalize nodelta 948 [ #EQpc whd in ⊢(??%% → ?); #EQ destruct # a1 #good_st_a1 #labels whd in ⊢ (??%% → ?);949 #EQ destruct >act_neutral >act_neutral whd in prf; cases st2 in prf; st2 [3: #st2]949 [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); 950 #EQ destruct #a1 #good_st_a1>act_neutral >act_neutral whd in prf; cases st2 in prf; st2 [3: #st2] 950 951 normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct 951 952 #EQ destruct whd in EQc : (??%%); destruct … … 968 969  969 970 ] 970 * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate ;971 * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate in ⊢ (% → ?); 971 972 normalize nodelta >EQfetch >m_return_bind normalize nodelta 972 973 cases(asm_is_io ??) normalize nodelta … … 979 980 whd in ⊢ (??%% → ?); #EQ destruct [4,8: cases H1 ] 980 981 >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct 981 #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ destruct >neutral_r982 > act_neutral982 whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1 983 >neutral_r >act_neutral 983 984 lapply(instr_map_ok … good … good_st_a1) 984 985 [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta … … 1005 1006 #Hpc normalize nodelta #H cases(bind_inversion ????? H) H #i * #EQi 1006 1007 inversion(emits_labels ??) 1007 [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct # a1 #good_a1 #labels1008 [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #labels 1008 1009 cases(step_emit … EQi … EQemits) 1009 1010 [4: cases exe_st1_st3 #EQ #H @(vm_step_to_eval … H) 2,3:] #c * #EQc #Hc … … 1011 1012 >rewrite_in_dependent_map [2: @EQc 3:] whd in match (dependent_map ????); 1012 1013 @opt_safe_elim #k_c #EQk_c whd in match (dependent_map ????); letin ih_labels ≝ (dependent_map ????) 1013 #EQ destruct >big_op_associative >act_op @IH1014 #EQ destruct #a1 #good_a1 >big_op_associative >act_op @IH 1014 1015  #f #EQemits normalize nodelta #H cases(bind_inversion ????? H) H #k' * #EQk' whd in ⊢ (??%% → ?); 1015 #EQ destruct(EQ) # a1 #good_a1 #labels cases(step_non_emit … EQi… EQemits)1016 #EQ destruct(EQ) #labels cases(step_non_emit … EQi… EQemits) 1016 1017 [4: cases exe_st1_st3 #EQ #H @(vm_step_to_eval … H) 2,3:] #EQl #EQpc 1017 1018 >(rewrite_in_dependent_map ??? []) [2: assumption] whd in match (dependent_map ????); 1018 #EQlabels >act_op @IH1019 #EQlabels #a1 #good_a1 >act_op @IH 1019 1020 ] 1020 1021 try // … … 1041 1042 ] // 1042 1043 ] 1043  whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1cases exe_st1_st3 #EQpc_st3 #EQ destruct1044  whd in ⊢ (??%% → ?); #EQ destruct cases exe_st1_st3 #EQpc_st3 #EQ destruct 1044 1045 #labels whd in match actionlabel_to_costlabel; normalize nodelta 1045 1046 whd in match (dependent_map ????); @opt_safe_elim #k_c #EQk_c letin ih_labels ≝ (dependent_map ????) 1046 change with ([?]@?) in match ([?]@?); #EQ destruct >big_op_associative >act_op @IH try // 1047 change with ([?]@?) in match ([?]@?); #EQ #a1 #good_a1 destruct 1048 >big_op_associative >act_op @IH try // 1047 1049 [ inversion pre_meas in ⊢ ?; 1048 1050 [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct … … 1055 1057 5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * 1056 1058 ] // 1057  cases(static_analisys_ok … (in_act … prog) … (pc … st3) … EQmap) 1059  cases(static_analisys_ok … (in_act … prog) … (pc … st3) … EQmap) 1058 1060 [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ] 1059 1061 #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption
Note: See TracChangeset
for help on using the changeset viewer.