Changeset 2118
- Timestamp:
- Jun 27, 2012, 12:04:27 PM (6 years ago)
- Location:
- src
- Files:
-
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/Clight/labelSimulation.ma
r2107 r2118 1091 1091 1092 1092 1093 1093 inductive steps : trace → execution state io_out io_in → execution state io_out io_in → Prop ≝ 1094 | steps_stop : ∀tr,s,r. steps tr (e_stop … tr s r) (e_stop … tr s r) 1095 | steps_step : ∀tr,s,e. steps tr (e_step … tr s e) e 1096 | steps_steps : ∀tr,s,e,tr',e'. steps tr e e' → steps (tr'⧺tr) (e_step … tr' s e) e'. 1097 1098 coinductive sim_with_labels : execution state io_out io_in → execution state io_out io_in → Prop ≝ 1099 | swl_stop : ∀tr1,tr2,tr2',r,s1,s2,e2. 1100 steps tr2 e2 (e_stop … tr2' r s2) → 1101 trace_with_extra_labels tr1 tr2 → 1102 sim_with_labels (e_stop … tr1 r s1) e2 1103 | swl_steps : ∀tr1,tr2,s1,e1,e2,e2'. 1104 steps tr2 e2 e2' → 1105 trace_with_extra_labels tr1 tr2 → 1106 sim_with_labels e1 e2' → 1107 sim_with_labels (e_step … tr1 s1 e1) e2. 1108 1109 coinductive not_wrong_no_io : execution state io_out io_in → Prop ≝ 1110 | nwni_stop : ∀tr,i,s. not_wrong_no_io (e_stop … tr i s) 1111 | nwni_step : ∀tr,s,e. not_wrong_no_io e → not_wrong_no_io (e_step … tr s e). 1112 1113 lemma not_wrong_init : ∀p. 1114 not_wrong_no_io (exec_inf … clight_fullexec p) → 1115 ∃s. make_initial_state … p = OK ? s. 1116 #p whd in ⊢ (?% → ?); change with (make_initial_state p) in match (make_initial_state ??? p); 1117 cases (make_initial_state p) 1118 [ /2/ 1119 | normalize #m #NW @⊥ 1120 inversion NW #H1 #H2 #H3 #H4 try #H5 destruct 1121 ] qed. 1122 1123 lemma final_related : ∀s1,s2. 1124 state_with_labels s1 s2 → 1125 is_final s1 = is_final s2. 1126 #s1x #s2x * 1127 [ #s1y #s2y * // 1128 | // 1129 ] qed. 1130 1131 lemma plus_not_final : ∀ge,s,tr,s'. 1132 plus ge s tr s' → 1133 is_final s = None ?. 1134 #ge #s0 #tr0 #s0' * 1135 [ #s1 #tr #s2 #EX | #s1 #tr #s2 #tr' #s3 #EX #PL ] 1136 lapply (refl ? (is_final s1)) 1137 cases (is_final s1) in ⊢ (???% → %); 1138 // 1139 #r cases s1 in EX ⊢ %; 1140 #H9 #H10 #H11 try #H12 try #H13 try #H14 try #H15 1141 [ 1,5: whd in H15:(??%?); | 2,6: whd in H14:(??%?); | 3,7: whd in H13:(??%?); | 4,8: whd in H11:(??%?); ] 1142 destruct 1143 normalize in H10; 1144 destruct 1145 qed. 1146 1147 lemma plus_exec : ∀ge,s,tr,s'. 1148 plus ge s tr s' → 1149 is_final s' = None ? → 1150 steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1151 (exec_inf_aux … clight_fullexec ge (exec_step ge s')). 1152 #ge #s0 #tr0 #s0' #P elim P 1153 [ #s1 #tr #s2 #EX #NF >EX >exec_inf_aux_unfold 1154 whd in ⊢ (??%?); 1155 whd in match (is_final ?????); >NF 1156 %2 1157 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #NF 1158 >exec_inf_aux_unfold >EX1 1159 whd in ⊢ (??%?); 1160 whd in match (is_final ?????); >(plus_not_final … P2) 1161 %3 @IH // 1162 ] qed. 1163 1164 lemma plus_exec_final : ∀ge,s,tr,s',r. 1165 plus ge s tr s' → 1166 is_final s' = Some ? r → 1167 ∃tr'. steps tr (exec_inf_aux … clight_fullexec ge (exec_step ge s)) 1168 (e_stop … tr' r s'). 1169 #ge #s0 #tr0 #s0' #r #P elim P 1170 [ #s1 #tr #s2 #EX #F >EX >exec_inf_aux_unfold 1171 %{tr} whd in ⊢ (??%?); 1172 whd in match (is_final ?????); >F 1173 %1 1174 | #s1 #tr #s2 #tr' #s3 #EX1 #P2 #IH #F 1175 cases (IH … F) 1176 #tr' #S' %{tr'} 1177 >exec_inf_aux_unfold >EX1 1178 whd in ⊢ (??%?); 1179 whd in match (is_final ?????); >(plus_not_final … P2) 1180 %3 @S' 1181 ] qed. 1182 1183 let corec build_exec 1184 (ge1,ge2:genv) 1185 (RG:related_globals … label_fundef ge1 ge2) 1186 (s1,s2:state) 1187 (S:state_with_labels s1 s2) 1188 (NW:not_wrong_no_io (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))) 1189 : sim_with_labels (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1)) (exec_inf_aux … clight_fullexec ge2 (exec_step ge2 s2)) ≝ 1190 match NW return λe,NW. exec_inf_aux … clight_fullexec ?? = e → sim_with_labels e ? with 1191 [ nwni_stop tr i s ⇒ ? 1192 | nwni_step tr1 s1' e1 NW1 ⇒ ? 1193 ] (refl ? (exec_inf_aux … clight_fullexec ge1 (exec_step ge1 s1))). 1194 [ #E1 1195 cases (exec_inf_stops_at_final ?? clight_fullexec … E1) 1196 #EX1 #F1 1197 cases (step_with_labels … RG … S EX1) 1198 #tr2 * #s2' * * #PL #TWL #S' 1199 lapply F1 whd in ⊢ (??%? → ?); >(final_related … S') #F2 1200 cases (plus_exec_final ????? PL F2) 1201 #tr2' #S2 1202 @(swl_stop … S2 TWL) 1203 | #E1 1204 cases (extract_step ?? clight_fullexec … E1) 1205 #EX1 #E1' 1206 cases (step_with_labels … RG … S EX1) 1207 #tr2 * #s2' * * #EX2 #TR #S' (*>E1' in NW1 ⊢ %; #NW1*) 1208 @(swl_steps … (plus_exec … EX2 ?)) 1209 [ <(final_related … S') @(exec_e_step_not_final ?? clight_fullexec … E1) 1210 | // 1211 | (* Manual rewrite to prevent guardedness condition getting upset. *) 1212 @(match sym_eq … E1' return λe,E1'. sim_with_labels e ? with [refl ⇒ ?]) 1213 @build_exec // >E1' in NW1; // 1214 ] 1215 ] qed. 1216 1217 lemma initial_state_is_not_final : ∀p,s. 1218 make_initial_state p = OK ? s → 1219 is_final s = None ?. 1220 * #vars #fns #main #s 1221 whd in ⊢ (??%? → ?); letin ge ≝ (make_global ?) #EX 1222 cases (bind_inversion ????? EX) -EX #m * #Em #EX 1223 cases (bind_inversion ????? EX) -EX #b * #Emain #EX 1224 cases (bind_inversion ????? EX) -EX #fd * #Emain' #EX 1225 whd in EX:(??%%); destruct // 1226 qed. 1227 1228 1229 theorem labelling_sim : ∀p. 1230 let e1 ≝ exec_inf … clight_fullexec p in 1231 let e2 ≝ exec_inf … clight_fullexec (clight_label p) in 1232 not_wrong_no_io e1 → 1233 sim_with_labels e1 e2. 1234 #p 1235 #NW 1236 cases (not_wrong_init p NW) 1237 #s1 #I1 1238 cases (initial_state_in_simulation … I1) 1239 #s2 * #I2 1240 1241 whd in match (exec_inf ??? p) in NW ⊢ %; 1242 letin ge1 ≝ (make_global ??? p) in NW ⊢ %; 1243 change with (make_initial_state p) in match (make_initial_state ??? p); 1244 >I1 1245 1246 whd in match (exec_inf ????); 1247 letin ge2 ≝ (make_global ?? clight_fullexec (clight_label p)) 1248 change with (make_initial_state (clight_label p)) in match (make_initial_state ?? clight_fullexec (clight_label p)); 1249 >I2 1250 1251 whd in ⊢ (?% → ? → ?%%); 1252 >exec_inf_aux_unfold 1253 >exec_inf_aux_unfold 1254 whd in ⊢ (?% → ? → ?%%); 1255 whd in match (is_final ?????); 1256 >(initial_state_is_not_final … I1) 1257 whd in match (is_final ?????); 1258 >(initial_state_is_not_final … I2) 1259 whd in ⊢ (?% → ? → ?%%); 1260 1261 #NW #S 1262 @(swl_steps E0 E0) 1263 [ 2: @steps_step | skip | // | @build_exec 1264 [ @transform_program_related | // | inversion NW 1265 [ #tr #i #s #E1 #E2 destruct 1266 | #trX #sX #eX #NWX #E1X #E2X destruct // 1267 ] 1268 ] 1269 ] qed. 1270 1271 1272 -
src/common/SmallstepExec.ma
r1599 r2118 80 80 *) 81 81 82 lemma exec_inf_stops_at_final : ∀O,I,TS,ge,s,s',tr,r. 83 exec_inf_aux O I TS ge (step … ge s) = e_stop … tr r s' → 84 step … ge s = Value … 〈tr, s'〉 ∧ 85 is_final … s' = Some ? r. 86 #O #I #TS #ge #s #s' #tr #r 87 >exec_inf_aux_unfold 88 cases (step … ge s) 89 [ 1,3: normalize #H1 #H2 try #H3 destruct 90 | * #tr' #s'' 91 whd in ⊢ (??%? → ?); 92 lapply (refl ? (is_final … s'')) 93 cases (is_final … s'') in ⊢ (???% → %); 94 [ #_ whd in ⊢ (??%? → ?); #E destruct 95 | #r' #E1 #E2 whd in E2:(??%?); destruct % // 96 ] 97 ] qed. 98 99 lemma extract_step : ∀O,I,TS,ge,s,s',tr,e. 100 exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e → 101 step … ge s = Value … 〈tr,s'〉 ∧ e = exec_inf_aux O I TS ge (step … ge s'). 102 #O #I #TS #ge #s #s' #tr #e 103 >exec_inf_aux_unfold 104 cases (step … s) 105 [ 1,3: normalize #H1 #H2 try #H3 destruct 106 | * #tr' #s'' 107 whd in ⊢ (??%? → ?); 108 cases (is_final … s'') 109 [ #E normalize in E; destruct /2/ 110 | #r #E normalize in E; destruct 111 ] 112 ] qed. 113 114 lemma exec_e_step_not_final : ∀O,I,TS,ge,s,s',tr,e. 115 exec_inf_aux O I TS ge (step … ge s) = e_step … tr s' e → 116 is_final … s' = None ?. 117 #O #I #TS #ge #s #s' #tr #e 118 >exec_inf_aux_unfold 119 cases (step … s) 120 [ 1,3: normalize #H1 #H2 try #H3 destruct 121 | * #tr' #s'' 122 whd in ⊢ (??%? → ?); 123 lapply (refl ? (is_final … s'')) 124 cases (is_final … s'') in ⊢ (???% → %); 125 [ #F whd in ⊢ (??%? → ?); #E destruct @F 126 | #r' #_ #E whd in E:(??%?); destruct 127 ] 128 ] qed. 129 130 131 82 132 record fullexec (outty:Type[0]) (inty:outty → Type[0]) : Type[2] ≝ 83 133 { program : Type[0]
Note: See TracChangeset
for help on using the changeset viewer.