1100 lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve |
1100 lemmas cph2spshs_simps = cph2spshs_attach cph2spshs_detach cph2spshs_deleteshm cph2spshs_clone cph2spshs_execve |
1101 cph2spshs_exit cph2spshs_kill cph2spshs_other |
1101 cph2spshs_exit cph2spshs_kill cph2spshs_other |
1102 |
1102 |
1103 (******** cp2sproc simpset *********) |
1103 (******** cp2sproc simpset *********) |
1104 |
1104 |
1105 lemma cp2sproc_nil: "p \<in> init_processes \<Longrightarrow> cp2sproc [] p = SInit p" |
1105 lemma not_init_intro_proc: (*???*) |
1106 apply (simp add:cp2sproc_def) |
1106 "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> deleted (O_proc p) s \<or> p \<notin> init_procs" |
1107 by (simp add:cp2sproc_def index_of_proc.simps) |
1107 using not_deleted_init_proc by auto |
1108 |
1108 |
1109 lemma cp2sproc_nil': "p \<in> current_procs [] \<Longrightarrow> cp2sproc [] p = SInit p" |
1109 lemma not_init_intro_proc': (*???*) |
1110 by (simp add:cp2sproc_nil current_procs.simps) |
1110 "\<lbrakk>p \<notin> current_procs s; valid s\<rbrakk> \<Longrightarrow> \<not> (\<not> deleted (O_proc p) s \<and> p \<in> init_procs)" |
1111 |
1111 using not_deleted_init_proc by auto |
1112 lemma cp2sproc_clone: "cp2sproc (Clone p p' # \<tau>) p'' = ( |
1112 |
1113 if (p'' = p') then SCrea (Suc (length \<tau>)) |
1113 lemma cp2sproc_clone: |
1114 else cp2sproc \<tau> p'' )" |
1114 "valid (Clone p p' fds shms # s) \<Longrightarrow> cp2sproc (Clone p p' fds shms # s) = (cp2sproc s) (p' := |
1115 by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps) |
1115 case (sectxt_of_obj s (O_proc p)) of |
1116 |
1116 Some sec \<Rightarrow> Some (Created, sec, |
1117 lemma cp2sproc_other: "\<forall> p p'. e \<noteq> Clone p p' \<Longrightarrow> cp2sproc (e # \<tau>) p'' = cp2sproc \<tau> p''" |
1117 {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, |
|
1118 {(sh, flag) | h sh flag. h \<in> shms \<and> ch2sshm s h = Some sh \<and> flag_of_proc_shm s p h = Some flag}) |
|
1119 | _ \<Rightarrow> None)" |
|
1120 apply (frule cph2spshs_clone, frule cpfd2sfds_clone) |
|
1121 apply (frule vd_cons, frule vt_grant_os, simp only:os_grant.simps) |
|
1122 apply ((erule exE| erule conjE)+, frule not_init_intro_proc, simp, rule ext, case_tac "x = p'", simp) |
|
1123 apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec' |
|
1124 dest:current_proc_has_sec split:option.splits if_splits) |
|
1125 done |
|
1126 |
|
1127 lemma cp2sproc_other: |
|
1128 "\<lbrakk>valid (e # s); |
|
1129 \<forall> p f flags fd opt. e \<noteq> Open p f flags fd opt; |
|
1130 \<forall> p fd. e \<noteq> CloseFd p fd; |
|
1131 \<forall> p h flag. e \<noteq> Attach p h flag; |
|
1132 \<forall> p h. e \<noteq> Detach p h; |
|
1133 \<forall> p h. e \<noteq> DeleteShM p h; |
|
1134 \<forall> p p' fds shms. e \<noteq> Clone p p' fds shms; |
|
1135 \<forall> p f fds. e \<noteq> Execve p f fds; |
|
1136 \<forall> p p'. e \<noteq> Kill p p'; |
|
1137 \<forall> p. e \<noteq> Exit p\<rbrakk> \<Longrightarrow> cp2sproc (e # s) = cp2sproc s" |
|
1138 apply (frule cph2spshs_other, simp+, frule cpfd2sfds_other, simp+) |
|
1139 apply (frule vt_grant_os, frule vd_cons, rule ext, case_tac e, simp_all) |
|
1140 apply (auto simp:cp2sproc_def sectxt_of_obj_simps dest!:current_has_sec' |
|
1141 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1142 done |
|
1143 |
|
1144 lemma cp2sproc_open: |
|
1145 "valid (Open p f flags fd opt # s) \<Longrightarrow> |
|
1146 cp2sproc (Open p f flags fd opt # s) = (cp2sproc s) (p := |
|
1147 case (sectxt_of_obj s (O_proc p), sectxt_of_obj (Open p f flags fd opt # s) (O_fd p fd), |
|
1148 cf2sfile (Open p f flags fd opt # s) f) of |
|
1149 (Some sec, Some fdsec, Some sf) \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) |
|
1150 then Init p else Created, sec, |
|
1151 (cpfd2sfds s p) \<union> {(fdsec, flags, sf)}, cph2spshs s p) |
|
1152 | _ \<Rightarrow> None)" |
|
1153 apply (frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp) |
|
1154 apply (frule cpfd2sfds_open, frule vt_grant_os, frule vd_cons, rule ext) |
|
1155 apply (case_tac "x = p") |
|
1156 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
|
1157 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current |
|
1158 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1159 done |
|
1160 |
|
1161 lemma cp2sproc_closefd: |
|
1162 "valid (CloseFd p fd # s) \<Longrightarrow> |
|
1163 cp2sproc (CloseFd p fd # s) = (cp2sproc s) (p := |
|
1164 if (fd \<in> proc_file_fds s p) |
|
1165 then (case (cfd2sfd s p fd) of |
|
1166 Some sfd \<Rightarrow> (if (\<exists> fd' f'. fd' \<noteq> fd \<and> file_of_proc_fd s p fd' = Some f' \<and> cfd2sfd s p fd' = Some sfd) |
|
1167 then cp2sproc s p |
|
1168 else (case (sectxt_of_obj s (O_proc p)) of |
|
1169 Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) |
|
1170 then Init p else Created, |
|
1171 sec, cpfd2sfds s p - {sfd}, cph2spshs s p) |
|
1172 | _ \<Rightarrow> None)) |
|
1173 | _ \<Rightarrow> cp2sproc s p) |
|
1174 else cp2sproc s p)" |
|
1175 apply (frule cpfd2sfds_closefd, frule cph2spshs_other, simp, simp, simp, simp, simp, simp, simp) |
|
1176 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
1177 apply (case_tac "x = p") |
|
1178 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
|
1179 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current |
|
1180 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1181 done |
|
1182 |
|
1183 lemma cp2sproc_attach: |
|
1184 "valid (Attach p h flag # s) \<Longrightarrow> |
|
1185 cp2sproc (Attach p h flag # s) = (cp2sproc s) (p := |
|
1186 (case (ch2sshm s h) of |
|
1187 Some sh \<Rightarrow> (case (sectxt_of_obj s (O_proc p)) of |
|
1188 Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) |
|
1189 then Init p else Created, |
|
1190 sec, cpfd2sfds s p, cph2spshs s p \<union> {(sh, flag)}) |
|
1191 | _ \<Rightarrow> None) |
|
1192 | _ \<Rightarrow> cp2sproc s p) )" |
|
1193 apply (frule cph2spshs_attach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp) |
|
1194 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
1195 apply (case_tac "x = p") |
|
1196 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
|
1197 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current |
|
1198 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1199 done |
|
1200 |
|
1201 lemma cp2sproc_detach: |
|
1202 "valid (Detach p h # s) \<Longrightarrow> |
|
1203 cp2sproc (Detach p h # s) = (cp2sproc s) (p := |
|
1204 (case (ch2sshm s h, flag_of_proc_shm s p h) of |
|
1205 (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p,flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh) |
|
1206 then cp2sproc s p |
|
1207 else (case (sectxt_of_obj s (O_proc p)) of |
|
1208 Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) |
|
1209 then Init p else Created, sec, |
|
1210 cpfd2sfds s p, cph2spshs s p - {(sh, flag)}) |
|
1211 | None \<Rightarrow> None) |
|
1212 | _ \<Rightarrow> cp2sproc s p) )" |
|
1213 apply (frule cph2spshs_detach, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp) |
|
1214 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
1215 apply (case_tac "x = p") |
|
1216 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
|
1217 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current |
|
1218 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1219 done |
|
1220 |
|
1221 lemma cp2sproc_deleteshm: |
|
1222 "valid (DeleteShM p h # s) \<Longrightarrow> |
|
1223 cp2sproc (DeleteShM p h # s) = (\<lambda> p'. |
|
1224 (case (ch2sshm s h, flag_of_proc_shm s p' h) of |
|
1225 (Some sh, Some flag) \<Rightarrow> if (\<exists> h'. h' \<noteq> h \<and> (p', flag) \<in> procs_of_shm s h' \<and> ch2sshm s h' = Some sh) |
|
1226 then cp2sproc s p' |
|
1227 else (case (sectxt_of_obj s (O_proc p')) of |
|
1228 Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p') s \<and> p' \<in> init_procs) |
|
1229 then Init p' else Created, sec, |
|
1230 cpfd2sfds s p', cph2spshs s p' - {(sh, flag)}) |
|
1231 | None \<Rightarrow> None) |
|
1232 | _ \<Rightarrow> cp2sproc s p') )" |
|
1233 apply (frule cph2spshs_deleteshm, frule cpfd2sfds_other, simp, simp, simp, simp, simp, simp) |
|
1234 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
1235 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
|
1236 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current |
|
1237 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1238 done |
|
1239 |
|
1240 lemma cp2sproc_execve: |
|
1241 "valid (Execve p f fds # s) \<Longrightarrow> |
|
1242 cp2sproc (Execve p f fds # s) = (cp2sproc s) (p := |
|
1243 (case (sectxt_of_obj (Execve p f fds # s) (O_proc p)) of |
|
1244 Some sec \<Rightarrow> Some (if (\<not> deleted (O_proc p) s \<and> p \<in> init_procs) then Init p else Created, sec, |
|
1245 {sfd. \<exists> fd \<in> fds. \<exists> f. file_of_proc_fd s p fd = Some f \<and> cfd2sfd s p fd = Some sfd}, {}) |
|
1246 | _ \<Rightarrow> None) )" |
|
1247 apply (frule cph2spshs_execve, frule cpfd2sfds_execve) |
|
1248 apply (frule vt_grant_os, frule vd_cons, rule ext) |
|
1249 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
|
1250 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current |
|
1251 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1252 done |
|
1253 |
|
1254 lemma cp2sproc_kill: |
|
1255 "\<lbrakk>valid (Kill p p' # s); p'' \<noteq> p'\<rbrakk> \<Longrightarrow> |
|
1256 cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''" |
|
1257 apply (frule cph2spshs_kill, frule cpfd2sfds_kill) |
|
1258 apply (frule vt_grant_os, frule vd_cons) |
|
1259 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
|
1260 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current |
|
1261 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1262 done |
|
1263 |
|
1264 lemma cp2sproc_kill': |
|
1265 "\<lbrakk>valid (Kill p p' # s); p'' \<in> current_procs (Kill p p' # s)\<rbrakk> \<Longrightarrow> |
|
1266 cp2sproc (Kill p p' # s) p'' = (cp2sproc s) p''" |
|
1267 by (drule_tac p'' = p'' in cp2sproc_kill, simp+) |
|
1268 |
|
1269 lemma cp2sproc_exit: |
|
1270 "\<lbrakk>valid (Exit p # s); p' \<noteq> p\<rbrakk> \<Longrightarrow> |
|
1271 cp2sproc (Exit p # s) p' = (cp2sproc s) p'" |
|
1272 apply (frule cph2spshs_exit, frule cpfd2sfds_exit) |
|
1273 apply (frule vt_grant_os, frule vd_cons) |
|
1274 apply (auto simp:cp2sproc_def sectxt_of_obj_simps current_files_simps |
|
1275 dest!:current_has_sec' dest!:current_file_has_sfile' dest:is_file_in_current is_dir_in_current |
|
1276 dest:current_proc_has_sec not_deleted_init_proc split:option.splits if_splits) |
|
1277 done |
|
1278 |
|
1279 lemma cp2sproc_exit': |
|
1280 "\<lbrakk>valid (Exit p # s); p' \<in> current_procs (Exit p # s)\<rbrakk> \<Longrightarrow> |
|
1281 cp2sproc (Exit p # s) p' = (cp2sproc s) p'" |
|
1282 by (drule_tac p'= p' in cp2sproc_exit, simp+) |
|
1283 |
|
1284 lemmas cp2sproc_simps = cp2sproc_open cp2sproc_closefd cp2sproc_attach cp2sproc_detach cp2sproc_deleteshm |
|
1285 cp2sproc_clone cp2sproc_execve cp2sproc_kill cp2sproc_exit cp2sproc_other |
|
1286 |
|
1287 (********************* cm2smsg simpset ***********************) |
|
1288 |
|
1289 lemma cm2smsg_other: "\<lbrakk>valid (e # s); \<forall> p q m. e \<noteq> SendMsg p q m\<rbrakk> \<Longrightarrow> cm2smsg (e # s) = cm2smsg s" |
|
1290 apply (frule vt_grant_os, frule vd_cons, rule ext, rule ext) |
1118 apply (case_tac e) |
1291 apply (case_tac e) |
1119 by (auto simp:cp2sproc_def index_of_proc.simps d2s_aux.simps) |
1292 apply (auto simp:cm2smsg_def sectxt_of_obj_simps split:option.splits if_splits) |
1120 |
|
1121 lemmas cp2sproc_simps = cp2sproc_nil cp2sproc_nil' cp2sproc_clone cp2sproc_other |
|
1122 |
|
1123 (********************* cm2smsg simpset ***********************) |
|
1124 |
|
1125 lemma cm2smsg_nil: "m \<in> init_msgs \<Longrightarrow> cm2smsg [] m = SInit m" |
|
1126 by (simp add:cm2smsg_def index_of_msg.simps) |
|
1127 |
|
1128 lemma cm2smsg_nil': "m \<in> current_msgs [] \<Longrightarrow> cm2smsg [] m = SInit m" |
|
1129 by (simp add:cm2smsg_nil current_msgs.simps) |
|
1130 |
|
1131 lemma cm2smsg_createmsg: "cm2smsg (CreateMsg p m # \<tau>) m' = (if (m' = m) then SCrea (Suc (length \<tau>)) else cm2smsg \<tau> m')" |
|
1132 by (simp add:cm2smsg_def index_of_msg.simps d2s_aux.simps) |
|
1133 |
|
1134 lemma cm2smsg_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" |
|
1135 apply (case_tac e) |
|
1136 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) |
|
1137 |
1293 |
1138 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
1294 lemmas cm2smsg_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
|
1295 |
|
1296 |
|
1297 |
|
1298 (********************* cq2smsgq simpset ***********************) |
|
1299 |
|
1300 lemma cq2smsgq_other: "\<forall> p m. e \<noteq> CreateMsg p m \<Longrightarrow> cm2smsg (e # \<tau>) m' = cm2smsg \<tau> m'" |
|
1301 apply (case_tac e) |
|
1302 by (auto simp:cm2smsg_def index_of_msg.simps d2s_aux.simps) |
|
1303 |
|
1304 lemmas cq2smsgq_simps = cm2smsg_nil cm2smsg_nil' cm2smsg_createmsg cm2smsg_other |
|
1305 |
1139 |
1306 |
1140 |
1307 |
1141 |
1308 |
1142 end |
1309 end |
1143 |
1310 |