Changeset 3503
Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3502 r3503 1103 1103 1104 1104 definition measurable : 1105 ∀S: abstract_status. ∀s 1,s2,s4 : S. raw_trace … s1 s4→ Prop ≝1106 λS,s 1,s2,s4,t.1105 ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝ 1106 λS,si,s1,s3,sn,t. 1107 1107 pre_measurable_trace … t ∧ 1108 ∃s3:S. ∃t' : raw_trace … s2 s3. ∃l1,l2,prf1,prf2. 1109 t = t_ind ? s1 s2 s4 l1 prf1 … (t' @ (t_ind ? s3 s4 s4 l2 prf2 … (t_base … s4))) 1110 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2. 1111 1108 ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn. 1109 ∃l1,l2,prf1,prf2. 1110 t = ti0 @ t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n)) 1111 ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n. 1112 1113 lemma chop_cons : ∀A : Type[0].∀x : A.∀xs: list A. xs ≠ [ ] → chop … (x :: xs) = x :: (chop … xs). 1114 #A #x * [ #H cases(absurd ?? H) % ] // qed. 1115 1112 1116 (* 1113 1117 lemma measurable_terminated: … … 1117 1121 qed. *) 1118 1122 1123 lemma execute_mem_label_pc :∀p,p',prog.∀st0,st1 :vm_state p p'.∀l1,c1. 1124 actionlabel_to_costlabel l1 = [c1] → 1125 vmstep p p' prog l1 st0 st1 → 1126 mem … 〈c1,pc p p' st1〉 1127 (labels_pc … (instructions … prog) (call_label_fun … prog) 1128 (return_label_fun … prog) (in_act … prog) O). 1119 1129 theorem static_dynamic : 1120 1130 (* Given an assembly program *) … … 1129 1139 (* For every measurable trace whose second state is st1 or, equivalently, 1130 1140 whose first state after the initial labelled transition is st1 *) 1131 ∀s t0,st1,stn. ∀t: raw_trace (asm_operational_semantics … prog) … st0 stn.1132 measurable … s t1… t →1141 ∀si,s1,s2,sn. ∀t: raw_trace (asm_operational_semantics … prog) … si sn. 1142 measurable … s1 s2 … t → 1133 1143 1134 1144 (* Let labels be the costlabels observed in the trace (last one excluded) *) … … 1142 1152 1143 1153 (* Given an abstract state in relation with the second state of the trace *) 1144 ∀a1.R s t1 a1 →1154 ∀a1.R s1 a1 → 1145 1155 1146 1156 (* The final state of the trace is in relation with the one obtained by 1147 1157 applying every semantics in abs_trace. *) 1148 R stn (〚abs_actions〛 a1). 1149 [2: @hide_prf cases daemon 1150  #p #p' #prog #R #mT #map1 #EQmap #st0 #st1 #stn #t #measurable 1151 cases measurable #premeas * #st3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct 1152 #Hl1 #Hl2 #acts #EQacts #a1 #HR 1153 cut (∃act.∃actstl. acts = act::actstl) 1154 [ cases daemon (* usare measurable *) ] 1155 * #act * #actstl #EQacts2 >EQacts2 1156 cut (〚act::actstl〛 a1 = (〚actstl〛 (〚act〛 a1))) 1157 [ cases daemon (* true *) ] 1158 #EQ >EQ EQ >EQacts2 in EQacts; #EQacts 1159 @(static_dynamic_inv … EQmap … (t' @ t_ind … prf2 (t_base …)) … actstl … HR) 1158 R s2 (〚abs_actions〛 a1). 1159 [2: @hide_prf 1160 cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) * 1161 #lbl' #pc * #Hmem #EQ destruct 1162 >(proj1 … (static_analisys_ok … EQmap … Hmem)) 1163 @(proj2 … (static_analisys_ok … EQmap … Hmem)) 1164 ] 1165 #p #p' #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable 1166 cases measurable #premeas * #s0 * #s3 * #ti0 * #t12 * #t3n * #l1 * #l2 * #prf1 * #prf2 1167 **** #EQ destruct #Hl1 #Hl2 #silent_ti0 #silent_t3n #acts cases(actionlabel_ok … Hl1) 1168 #c1 #EQc1 >rewrite_in_dependent_map 1169 [2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … silent_ti0) in ⊢ (??%?); 1170 >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?); 1171 >get_cost_label_of_trace_tind in ⊢ (??%?); 1172 >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?); 1173 >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?); 1174 whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); [2: cases daemon] % 3: 1175 ] 1176 whd in ⊢ (???% → ?); @opt_safe_elim #act #EQact #EQacts2 >EQacts2 1177 >(big_op_associative ? [?]) #a1 >act_op #HR 1178 letin actsl ≝ (dependent_map ????); 1179 @(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR) 1160 1180 [ /6 width=6 by conj, ex_intro/ 1161 1181  cases daemon (* true *) 1162  cases daemon (* true *) 1163  cases daemon (* true *) ]] 1164 qed. 1182  cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] * 1183 [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %); 1184 #st' #EQst' #tr lapply prf2 lapply EQst' EQst' cases tr 1185 [ #st'' #EQ2 >EQ2 * 1186  #st'' #st''' #st'''' #l3 #ABS #_ #EQ2 >EQ2 in ABS; * 1187 ] 1188  #H1 #H2 #_ whd in match get_pc; normalize nodelta 1189 <(proj1 ?? (static_analisys_ok … EQmap …)) 1190 [ normalize in ⊢ (??%%); >neutral_l @EQact 1191  1192  check nth_opt 1193 1194 cases daemon 1195  >rewrite_in_dependent_map 1196 [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?); 1197 >append_nil in ⊢ (??%?); % 3:] 1198 % 1199 ] 1200 qed.
Note: See TracChangeset
for help on using the changeset viewer.