Changeset 3497


Ignore:
Timestamp:
Sep 25, 2014, 3:36:28 PM (5 years ago)
Author:
piccolo
Message:

prova finale statico dinamico

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Vm.ma

    r3496 r3497  
    876876qed.
    877877
     878check labels_pc
     879
     880lemma i_act_in_map :  ∀p,prog,iact,l1,l2.
     881mem ? 〈a_non_functional_label iact,O〉 (labels_pc p prog l1 l2 iact O).
     882#p #instr #iact #l1 #l2 generalize in match O in ⊢ (???%); elim instr
     883[ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???);
     884@mem_append_l2 @IH
     885qed.
     886
    878887lemma static_dynamic : ∀p,p',prog.
    879888∀abs_t : abstract_transition_sys (m … p').∀instr_m : (AssemblerInstr p) → abs_instr … abs_t.
     
    905914]   
    906915lapply Hlabelled lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3
    907 [ * [3: #st] #l #prf #H1 #H2 #k whd in ⊢ (??%? → ?);
     916[ * [3: #st] #l #prf #H1 #k #_ whd in ⊢ (??%? → ?);
    908917  [3: cases prf
    909918  |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in ⊢ (??%% → ?);
     
    987996  [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??);
    988997      >neutral_l assumption
    989    |3: >neutral_r lapply(instr_map_ok … good … good_a1)
    990        [ whd in ⊢ (??%?); @eqb_elim
    991          [ #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;
    992          normalize nodelta >EQi in ⊢ (??%?); %
    993        | assumption
     998   |3,6: [ >neutral_r] lapply(instr_map_ok … good … good_a1)
     999       [1,7: whd in ⊢ (??%?); @eqb_elim
     1000         [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state;
     1001         normalize nodelta [ >EQi in ⊢ (??%?); | >EQi in ⊢ (??%?); ] %
     1002       |2,8: assumption
    9941003       |*:
    9951004       ]
    9961005       normalize in ⊢ (% → ?); #H @H
    997    
    998  
    999    [2: assumption | | assumption | assumption | cases daemon (*TODO*)|
    1000       whd in ⊢ (??%%);
    1001   [1,5: inversion H in ⊢ ?;
    1002     [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
     1006  |5: whd in match get_pc; normalize nodelta >EQpc >(monotonicity_of_block_cost … EQk') //
     1007  |*:  inversion pre_meas in ⊢ ?;
     1008    [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
    10031009    |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
    1004       #EQ1 #EQ2 #EQ3 #EQ4 destruct
     1010      #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
    10051011    |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
    1006       #EQ1 #EQ2 #EQ3 #EQ4 destruct
     1012      #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
    10071013    |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
    1008       * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
     1014      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
    10091015    |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
    1010     ] //
    1011   | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx
    1012     >(rewrite_in_dependent_map … EQx)
    1013  
    1014     whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??);
    1015     >neutral_l @opt_safe_elim #elem #EQget
    1016     cases (static_analisys_ok  … x … (pc … st2) … no_dup … EQmap) //
    1017     #EQ #_ <EQ assumption
    1018   | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
    1019   | %
    1020   | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
    1021     >(monotonicity_of_block_cost … EQk') //
    1022   | @(instr_map_ok … good … EQi … good_a1) /2/
    1023   | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
    1024     #EQ >(rewrite_in_dependent_map … EQ) %
    1025   ]
    1026    
    1027     >rewrite_in_dependent_map [2: @eq_f [2: @eq_f2 [3: % |4: @get_cost_label_append |*:] |*:] |3:]
    1028     xxxxxx
    1029    
    1030     >dependent_map_append
    1031   inversion(emits_labels ??)
    1032   [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 #labels
    1033     >rewrite_in_dependent_map #EQlabels
    1034     >neutral_r check big_op_associative @IH
    1035     >big_op_associative >act_op @IH
    1036   | #f #EQemits normalize nodelta #H
    1037     cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
    1038     #EQ destruct(EQ) >act_op whd in match (append ???); @IH
    1039   ]
    1040   [1,5: inversion H in ⊢ ?;
    1041     [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
    1042     |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
    1043       #EQ1 #EQ2 #EQ3 #EQ4 destruct
    1044     |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
    1045       #EQ1 #EQ2 #EQ3 #EQ4 destruct
    1046     |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
    1047       * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    1048     |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
    1049     ] //
    1050   | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx
    1051     >(rewrite_in_dependent_map … EQx)
    1052  
    1053     whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??);
    1054     >neutral_l @opt_safe_elim #elem #EQget
    1055     cases (static_analisys_ok  … x … (pc … st2) … no_dup … EQmap) //
    1056     #EQ #_ <EQ assumption
    1057   | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
    1058   | %
    1059   | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
    1060     >(monotonicity_of_block_cost … EQk') //
    1061   | @(instr_map_ok … good … EQi … good_a1) /2/
    1062   | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
    1063     #EQ >(rewrite_in_dependent_map … EQ) %
    1064   ]
    1065 ]
    1066        
    1067   ]
    1068  
    1069  
    1070  
    1071   * #i * #EQi inversion(emits_labels …) normalize nodelta
    1072        
    1073      
    1074        >(act_neutral … a1) in H;
    1075      
    1076      
    1077        #H #H1
    1078       cases st2 in prf; -st2 [3: #st2] #prf
    1079       lapply(instr_map_ok … good … prf … rel_fin)
    1080      
    1081        lapply prf *
    1082       #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct
    1083       >act_neutral >act_neutral @(instr_map_ok … good … rel_fin)
    1084      
    1085      
    1086        @opt_safe_elim #k_init
    1087       #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct
    1088       >act_neutral whd in match (big_op ??); >act_op >act_neutral
    1089      
    1090      
    1091        #H >act_neutral whd in prf;
    1092        
    1093         cases l in prf H1 H2;
    1094         [1,4: #f #lbl |2,5: * [2,4: #lbl] |*: * [2,4: #lbl] ] #prf
    1095         ** [normalize in ⊢ (% → ?);
    1096          ⊢ (??%% → ?);
    1097 
    1098  #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ]
    1099   cases st -st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %]
    1100    #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1
    1101    #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption
    1102 | -st1 -st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); *
    1103   [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?);
    1104    (*
    1105     #EQlabels
    1106   #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta
    1107   [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st
    1108     normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    1109     #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption
    1110   | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta
    1111     #H cases(bind_inversion ????? H) -H *
    1112     [ #seq * [|#lbl1]
    1113     | #newpc
    1114     | #cond #newpc #ltrue #lfalse
    1115     | #lin #io #lout
    1116     | #f
    1117     |
    1118     ]
    1119     * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate;
    1120     normalize nodelta >EQfetch >m_return_bind normalize nodelta
    1121     cases(asm_is_io ??) normalize nodelta
    1122     [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct
    1123     |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_
    1124       [3: cases x normalize nodelta
    1125       |6: #H cases(bind_inversion ????? H) -H #y * #_
    1126       ]
    1127     ]
    1128     whd in ⊢ (??%% → ?); #EQ destruct
    1129     [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]]
    1130     >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct
    1131     #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r
    1132     >act_neutral
    1133     @(instr_map_ok … good … EQfetch … good_st_a1) /2/
    1134   ]*)
    1135 | -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H
    1136   #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????);
    1137   whd #costs >dependent_map_append
    1138   (*change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);*) 
    1139   #EQ destruct whd in H2 : (??%?); lapply H2 >H3 in ⊢ (% → ?); -H2
    1140   normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi
    1141   inversion(emits_labels ??)
    1142   [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct  >big_op_associative >act_op @IH
    1143   | #f #EQemits normalize nodelta #H
    1144     cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?);
    1145     #EQ destruct(EQ) >act_op whd in match (append ???); @IH
    1146   ]
    1147   [1,5: inversion H in ⊢ ?;
    1148     [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct
    1149     |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
    1150       #EQ1 #EQ2 #EQ3 #EQ4 destruct
    1151     |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
    1152       #EQ1 #EQ2 #EQ3 #EQ4 destruct
    1153     |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
    1154       * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct
    1155     |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
    1156     ] //
    1157   | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx
    1158     >(rewrite_in_dependent_map … EQx)
    1159  
    1160     whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??);
    1161     >neutral_l @opt_safe_elim #elem #EQget
    1162     cases (static_analisys_ok  … x … (pc … st2) … no_dup … EQmap) //
    1163     #EQ #_ <EQ assumption
    1164   | >neutral_r  @(instr_map_ok … good … EQi … good_a1) /2/
    1165   | %
    1166   | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
    1167     >(monotonicity_of_block_cost … EQk') //
    1168   | @(instr_map_ok … good … EQi … good_a1) /2/
    1169   | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits))
    1170     #EQ >(rewrite_in_dependent_map … EQ) %
    1171   ]
    1172 ]
    1173 qed.
    1174 
    1175 definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝
    1176 λa.match a with
    1177 [ call_act f l ⇒ [a_call l]
    1178 | ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]]
    1179 | cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]]
    1180 ].
    1181 
    1182 definition get_costlabels_of_measurable_trace : ∀S : abstract_status.measurable_trace S → list CostLabel ≝
    1183 λS,t.
    1184  match L_label … t with
    1185  [ None ⇒ [i_act]
    1186  | Some l ⇒ actionlabel_to_costlabel l
    1187  ] @
    1188  get_costlabels_of_trace … (trace … t).
    1189 
    1190 lemma i_act_in_map :  ∀p,prog.
    1191 mem … 〈i_act,O〉 (labels_pc … (instructions p prog) O).
    1192 #p *#instr #n #_ generalize in match O in ⊢ (???%); elim instr
    1193 [ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???);
    1194 @mem_append_l2 @IH
    1195 qed.
    1196 
    1197 
    1198 lemma as_execute_labelled_ok : ∀p,p',prog,c,l,st1,st2.
    1199 eval_vmstate p p' prog st1 = return 〈l,st2〉 → actionlabel_to_costlabel l = [c] →
    1200 ∃n.
    1201 mem … 〈c,n〉 (labels_pc … (instructions p prog) O).
    1202 #p #p' * #instr #endmain #Hendmain #c #l #st1 #st2 #H2 lapply H2 whd in match eval_vmstate; normalize nodelta
    1203 #H cases(bind_inversion ????? H) -H #i * #EQfetch #_
    1204  inversion(emits_labels … i)
    1205  [ #EQemit cases(step_emit … H2) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel;
    1206    normalize nodelta >EQ1 #EQ destruct /2 by ex_intro/
    1207   | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta  >(proj1 … (step_non_emit … EQfetch H2 … EQemit))
    1208     #EQ destruct
    1209  ]
    1210 qed.
    1211  
    1212 
    1213 (*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*)
    1214 theorem static_dynamic_meas : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog.
    1215 ∀abs_t : abstract_transition_sys (m … p').∀instr_m.
    1216 ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1.
    1217 ∀EQmap : static_analisys p ? instr_m mT prog = return map1.
    1218 ∀t : measurable_trace (asm_operational_semantics p p' prog).
    1219 let start_state ≝ match L_pre_state … t with [None ⇒ L_s1 … t | Some x ⇒ x ] in
    1220 ∀a1.rel_galois … good start_state a1 →
    1221 ∀abs_trace.
    1222 abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace …  t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) →
    1223 rel_galois … good (R_s2 … t) (act_abs … abs_t (big_op … abs_trace) a1).
    1224 [2: @hide_prf
    1225     whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf;
    1226     cases(mem_append ???? prf) -prf
    1227     [2: #prf cases(mem_map ????? (labels_of_trace_are_in_code … prf)) *
    1228         #lbl' #pc * #Hmem #EQ destruct   
    1229         >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem))
    1230         @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem))
    1231     | inversion(L_label … t) normalize nodelta [| #lbl'] #EQleft
    1232       [ * [2: *] #EQ destruct >(proj1 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …)))
    1233         @(proj2 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …)))
    1234       | #H lapply(L_init_ok … t) inversion(L_pre_state … t) [ #_ normalize nodelta * #_ >EQleft #EQ destruct]
    1235         #st_pre #EQst_pre normalize nodelta * #l' ** >EQleft #EQ destruct cases l' in H;
    1236         [ #x1 #x2 | * [|#x1] | * [|#x1]] whd in ⊢ (% → %→ ?); * [2,4,6: *] #EQ destruct * * #_
    1237         #H cases(as_execute_labelled_ok … H) [3,6,9:% |*:] #w #EQw
    1238         >(proj1 … (static_analisys_ok … no_dup … EQmap … EQw))
    1239        @(proj2 … (static_analisys_ok … no_dup … EQmap … EQw))
    1240       ]
    1241     ]
    1242 ]
    1243 #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace
    1244 @(static_dynamic …)
    1245 
    1246 xxxxxx
    1247 lapply(static_dynamic … (trace …t) … abs_trace) try //
    1248 
    1249 
     1016    ] //
     1017  ]
     1018 | whd in ⊢ (??%% → ?); #EQ destruct #a1 #good_a1 cases exe_st1_st3 #EQpc_st3 #EQ destruct
     1019   #labels whd in match actionlabel_to_costlabel; normalize nodelta
     1020   whd in match (dependent_map ????); @opt_safe_elim #k_c #EQk_c letin ih_labels ≝ (dependent_map ????)
     1021   change with ([?]@?) in match ([?]@?); #EQ destruct >big_op_associative >act_op @IH try //
     1022   [  inversion pre_meas in ⊢ ?;
     1023     [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
     1024     |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_
     1025      #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
     1026     |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_
     1027      #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
     1028     |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct
     1029      * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct
     1030     |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H *
     1031     ] //
     1032   |  cases(static_analisys_ok … (in_act … prog) … (pc … st3) … EQmap)
     1033      [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ]
     1034      #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption
     1035   |  lapply(instr_map_ok … good … good_a1)
     1036     [1: % | assumption |*:] normalize in ⊢ (% → ?); #H @H
     1037   ]
     1038]
     1039qed.
Note: See TracChangeset for help on using the changeset viewer.