--- a/all_sobj_prop.thy Thu Jun 13 07:01:39 2013 -0400
+++ b/all_sobj_prop.thy Thu Jun 13 22:15:32 2013 +0800
@@ -248,8 +248,10 @@
by (auto split:option.splits if_splits simp:obj2sobj.simps
dest:current_proc_has_sproc)
have "obj2sobj (e # s) (IPC i) \<in> all_sobjs" using ev vs_cons sproc os
- apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
- apply (rule ai_cipc) using SP sproc rc ev by auto
+ apply (auto simp:obj2sobj.simps split:option.splits)
+ apply (drule_tac obj = "IPC i" in not_deleted_imp_exists, simp+)
+ using SP sproc rc ev
+ by (auto intro:ai_cipc)
with True show ?thesis by simp
next
case False
@@ -271,7 +273,7 @@
by (auto split:option.splits if_splits simp:obj2sobj.simps
dest:current_proc_has_sproc)
have "obj2sobj (e # s) (Proc p) \<in> all_sobjs" using ev vs_cons sproc os
- apply (auto simp:obj2sobj.simps ni_init_deled split:option.splits)
+ apply (auto simp:obj2sobj.simps split:option.splits)
apply (rule ap_crole) using SP sproc rc ev srproc by auto
with True show ?thesis by simp
next
@@ -652,7 +654,7 @@
have valid: "valid (e # \<tau>)"
proof-
have "os_grant \<tau> e"
- using ev tau expab by (simp)
+ using ev tau expab by (simp add:ni_notin_curi)
moreover have "rc_grant \<tau> e"
using ev tau ai'_cipc(3) SPab
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1179,7 +1181,7 @@
have valid: "valid (e # \<tau>)"
proof-
have "os_grant \<tau> e"
- using ev tau expab by (simp)
+ using ev tau expab by (simp add:ni_notin_curi)
moreover have "rc_grant \<tau> e"
using ev tau ai'_cipc(3) SPab
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1305,7 +1307,7 @@
have valid: "valid (e#\<tau>)"
proof-
have "os_grant \<tau> e"
- using ev tau exp by (simp)
+ using ev tau exp by (simp add:np_notin_curp)
moreover have "rc_grant \<tau> e"
using ev tau ap'_crole(3) SPab
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1420,7 +1422,7 @@
have valid: "valid (e#\<tau>)"
proof-
have "os_grant \<tau> e"
- using ev tau exp ap'_chown(3) by (simp)
+ using ev tau exp ap'_chown(3) by (simp add:np_notin_curp)
moreover have "rc_grant \<tau> e"
using ev tau ap'_chown(5) SPab
by (auto simp:cp2sproc.simps obj2sobj.simps pct_def clone_type_unchange
@@ -1927,7 +1929,7 @@
have valid: "valid (e # \<tau>)"
proof-
have "os_grant \<tau> e"
- using ev tau expab by (simp)
+ using ev tau expab by (simp add:ni_notin_curi)
moreover have "rc_grant \<tau> e"
using ev tau ai'_cipc(3) SPab
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
--- a/del_vs_del_s.thy Thu Jun 13 07:01:39 2013 -0400
+++ b/del_vs_del_s.thy Thu Jun 13 22:15:32 2013 +0800
@@ -135,7 +135,7 @@
from initp fstdel vs' have "source_proc s' p = Some p"
apply (induct s', simp)
apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)
- by (case_tac a, auto dest:not_deleted_imp_exists simp:np_notin_curp)
+ by (case_tac a, auto dest:not_deleted_imp_exists)
with exp initp vs' obtain r fr pt u
where SP: "obj2sobj s' (Proc p) = SProc (r,fr,pt,u) (Some p)"
apply (frule_tac current_proc_has_sobj, simp)
--- a/obj2sobj_prop.thy Thu Jun 13 07:01:39 2013 -0400
+++ b/obj2sobj_prop.thy Thu Jun 13 22:15:32 2013 +0800
@@ -601,8 +601,7 @@
"\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; \<not> deleted (IPC i) (e#s)\<rbrakk>
\<Longrightarrow> obj2sobj (e#s) (IPC i) = SIPC si sri"
apply (frule valid_cons, frule valid_os, case_tac e)
-by (auto simp:ni_init_deled ni_notin_curi split:option.splits
- dest!:current_proc_has_role')
+by (auto split:option.splits dest!:current_proc_has_role')
lemma obj2sobj_ipc_remains_cons':
"\<lbrakk>valid (e#s); i \<in> current_ipcs s; obj2sobj s (IPC i) = SIPC si sri; no_del_event (e#s)\<rbrakk>
--- a/os_rc.thy Thu Jun 13 07:01:39 2013 -0400
+++ b/os_rc.thy Thu Jun 13 22:15:32 2013 +0800
@@ -274,6 +274,35 @@
apply (induct s) defer apply (case_tac a)
using init_finite by auto
+end
+
+context tainting_s_complete begin
+
+lemma init_notin_curf_deleted:
+ "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma init_notin_curi_deleted:
+ "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma init_notin_curp_deleted:
+ "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"
+by (induct s, simp, case_tac a, auto)
+
+lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
+by (induct f, auto split:if_splits)
+
+lemma source_proc_in_init:
+ "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"
+apply (induct s arbitrary:p, simp split:if_splits)
+apply (frule valid_os, frule valid_cons, case_tac a)
+by (auto split:if_splits)
+
+end
+
+context tainting_s_sound begin
+
(*** properties of new-proc new-ipc ... ***)
lemma nn_notin_aux: "finite s \<Longrightarrow> \<forall> a \<in> s. Max s \<ge> a "
@@ -299,22 +328,6 @@
lemma ni_notin_curi': "new_ipc \<tau> \<in> current_ipcs \<tau> \<Longrightarrow> False"
by (simp add:ni_notin_curi)
-end
-
-context tainting_s_complete begin
-
-lemma init_notin_curf_deleted:
- "\<lbrakk>f \<notin> current_files s; f \<in> init_files\<rbrakk> \<Longrightarrow> deleted (File f) s"
-by (induct s, simp, case_tac a, auto)
-
-lemma init_notin_curi_deleted:
- "\<lbrakk>i \<notin> current_ipcs s; i \<in> init_ipcs\<rbrakk> \<Longrightarrow> deleted (IPC i) s"
-by (induct s, simp, case_tac a, auto)
-
-lemma init_notin_curp_deleted:
- "\<lbrakk>p \<notin> current_procs s; p \<in> init_processes\<rbrakk> \<Longrightarrow> deleted (Proc p) s"
-by (induct s, simp, case_tac a, auto)
-
lemma ni_init_deled: "new_ipc s \<in> init_ipcs \<Longrightarrow> deleted (IPC (new_ipc s)) s"
using ni_notin_curi[where \<tau> = s]
by (drule_tac init_notin_curi_deleted, simp+)
@@ -323,18 +336,6 @@
using np_notin_curp[where \<tau> = s]
by (drule_tac init_notin_curp_deleted, simp+)
-lemma source_dir_in_init: "source_dir s f = Some sd \<Longrightarrow> sd \<in> init_files"
-by (induct f, auto split:if_splits)
-
-lemma source_proc_in_init:
- "\<lbrakk>source_proc s p = Some p'; p \<in> current_procs s; valid s\<rbrakk> \<Longrightarrow> p' \<in> init_processes"
-apply (induct s arbitrary:p, simp split:if_splits)
-apply (frule valid_os, frule valid_cons, case_tac a)
-by (auto simp:np_notin_curp split:if_splits)
-
-end
-
-context tainting_s_sound begin
lemma len_fname_all: "length (fname_all_a len) = len"
by (induct len, auto simp:fname_all_a.simps)
@@ -366,7 +367,7 @@
lemma clone_event_no_limit:
"\<lbrakk>p \<in> current_procs \<tau>; valid \<tau>\<rbrakk> \<Longrightarrow> valid (Clone p (new_proc \<tau>) # \<tau>)"
apply (rule vs_step)
-apply (auto intro:clone_no_limit split:option.splits
+apply (auto intro:clone_no_limit split:option.splits dest!:np_notin_curp'
dest:current_proc_has_role current_proc_has_type)
done
--- a/rc_theory.thy Thu Jun 13 07:01:39 2013 -0400
+++ b/rc_theory.thy Thu Jun 13 22:15:32 2013 +0800
@@ -463,21 +463,6 @@
(Some r, Some t) \<Rightarrow> (r, Proc_type t, DELETE) \<in> compatible
| _ \<Rightarrow> False )"
-
-(**** OS' job: checking resources existence & grant new resource ****)
-
-definition next_nat :: "nat set \<Rightarrow> nat"
-where
- "next_nat ps = (Max ps) + 1"
-
-definition new_proc :: "t_state \<Rightarrow> t_process"
-where
- "new_proc \<tau> = next_nat (current_procs \<tau>)"
-
-definition new_ipc :: "t_state \<Rightarrow> t_ipc"
-where
- "new_ipc \<tau> = next_nat (current_ipcs \<tau>)"
-
(* new file pathname is user-defined, so os just check if its unexistence *)
fun os_grant :: "t_state \<Rightarrow> t_event \<Rightarrow> bool"
where
@@ -487,10 +472,10 @@
| "os_grant \<tau> (ReadFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
| "os_grant \<tau> (WriteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau>)"
| "os_grant \<tau> (ChangeOwner p u)= (p \<in> current_procs \<tau> \<and> u \<in> init_users)"
-| "os_grant \<tau> (CreateIPC p i) = (p \<in> current_procs \<tau> \<and> i = new_ipc \<tau>)"
+| "os_grant \<tau> (CreateIPC p i) = (p \<in> current_procs \<tau> \<and> i \<notin> current_ipcs \<tau>)" (* i = new_ipc \<tau> *)
| "os_grant \<tau> (Send p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
| "os_grant \<tau> (Recv p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
-| "os_grant \<tau> (Clone p p') = (p \<in> current_procs \<tau> \<and> p' = new_proc \<tau>)"
+| "os_grant \<tau> (Clone p p') = (p \<in> current_procs \<tau> \<and> p' \<notin> current_procs \<tau>)" (* p' = new_proc \<tau> *)
| "os_grant \<tau> (Kill p p') = (p \<in> current_procs \<tau> \<and> p' \<in> current_procs \<tau>)"
| "os_grant \<tau> (DeleteFile p f) = (p \<in> current_procs \<tau> \<and> f \<in> current_files \<tau> \<and> \<not> (\<exists>fn. fn # f \<in> current_files \<tau>))"
| "os_grant \<tau> (DeleteIPC p i) = (p \<in> current_procs \<tau> \<and> i \<in> current_ipcs \<tau>)"
@@ -961,7 +946,19 @@
"initp_intact_but s (SProc sp (Some p)) = initp_intact_butp s p"
| "initp_intact_but s _ = initp_intact s"
-(*** how to generating new valid pathname for examples of CreateFile ***)
+(*** how to generating new valid pathname for examples of new_proc, new_ipc and new_file as CreateFile ***)
+
+definition next_nat :: "nat set \<Rightarrow> nat"
+where
+ "next_nat ps = (Max ps) + 1"
+
+definition new_proc :: "t_state \<Rightarrow> t_process"
+where
+ "new_proc \<tau> = next_nat (current_procs \<tau>)"
+
+definition new_ipc :: "t_state \<Rightarrow> t_ipc"
+where
+ "new_ipc \<tau> = next_nat (current_ipcs \<tau>)"
definition all_fname_under_dir:: "t_file \<Rightarrow> t_state \<Rightarrow> t_fname set"
where
--- a/sound_defs_prop.thy Thu Jun 13 07:01:39 2013 -0400
+++ b/sound_defs_prop.thy Thu Jun 13 22:15:32 2013 +0800
@@ -137,8 +137,9 @@
apply (frule no_del_event_cons_D, drule_tac obj = "Proc pa" and s = s in nodel_imp_exists, simp)
apply (subgoal_tac "pa \<noteq> new_proc s") defer apply (rule notI,simp add:np_notin_curp)
apply (rotate_tac 6, erule_tac x = pa in allE, case_tac e)
-apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps
+apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps dest:nodel_imp_exists[where obj = "Proc pa"]
split:option.splits dest!:current_proc_has_sproc')
+apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+
done
lemma initp_intact_I_exec:
@@ -191,6 +192,7 @@
apply (erule_tac x = p in allE, case_tac e)
apply (auto simp:cp2sproc_simps' simp del:cp2sproc.simps
split:option.splits dest!:current_proc_has_sproc')
+apply (drule_tac obj = "Proc nat2" in nodel_imp_exists, simp, simp)+
done
end
--- a/source_prop.thy Thu Jun 13 07:01:39 2013 -0400
+++ b/source_prop.thy Thu Jun 13 22:15:32 2013 +0800
@@ -23,7 +23,7 @@
"\<lbrakk>p \<in> init_processes; \<not> deleted (Proc p) s; valid s\<rbrakk> \<Longrightarrow> source_proc s p = Some p"
apply (induct s, simp)
apply (frule valid_cons, frule valid_os, frule not_deleted_cons_D, simp)
-apply (case_tac a, auto simp:np_notin_curp dest:not_deleted_imp_exists)
+apply (case_tac a, auto dest:not_deleted_imp_exists)
done
lemma init_proc_keeps_source:
--- a/tainted_vs_tainted_s.thy Thu Jun 13 07:01:39 2013 -0400
+++ b/tainted_vs_tainted_s.thy Thu Jun 13 22:15:32 2013 +0800
@@ -105,7 +105,7 @@
with p2 have TP: "SProc (r,fr,pt,u) (source_proc s p) \<in> tainted_s"
by (auto simp:obj2sobj.simps cp2sproc.simps)
show ?case using p3 sproc os rc TP
- by (auto simp:ni_init_deled obj2sobj.simps cp2sproc.simps
+ by (auto simp:obj2sobj.simps cp2sproc.simps dest:not_deleted_imp_exists
split:option.splits intro!:ts_cipc)
next
case (t_read f s p)
@@ -211,9 +211,8 @@
next
case (IPC i)
have "obj2sobj (e # s) (IPC i) = obj2sobj s (IPC i)" using p5 t_remain(3,4) os IPC
- by (case_tac e, auto simp:ni_init_deled ni_notin_curi obj2sobj.simps
- split:option.splits
- dest!:current_proc_has_role')
+ by (case_tac e, auto simp:obj2sobj.simps dest:not_deleted_imp_exists
+ split:option.splits dest!:current_proc_has_role')
with IPC t_remain(2) show ?thesis by simp
next
case (Proc p)
@@ -298,7 +297,7 @@
have "\<lbrakk>\<forall> f. e \<noteq> Execute p f; \<forall> r. e \<noteq> ChangeRole p r; \<forall> u. e \<noteq> ChangeOwner p u\<rbrakk>
\<Longrightarrow> obj2sobj (e # s) (Proc p) \<in> tainted_s"
using t_remain(2,3,4) os p5 Proc
- by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps np_notin_curp
+ by (case_tac e, auto simp add:obj2sobj.simps cp2sproc_simps dest:not_deleted_imp_exists
simp del:cp2sproc.simps split:option.splits)
ultimately show ?thesis using Proc
by (case_tac e, auto simp del:obj2sobj.simps)
@@ -588,7 +587,7 @@
have valid: "valid (e # s)"
proof-
have "os_grant s e"
- using ev exp by (simp)
+ using ev exp by (simp add:ni_notin_curi)
moreover have "rc_grant s e"
using ev ts'_cipc(3) SP
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
@@ -1141,7 +1140,7 @@
have valid: "valid (e # s)"
proof-
have "os_grant s e"
- using ev exp by (simp)
+ using ev exp by (simp add:ni_notin_curi)
moreover have "rc_grant s e"
using ev ts'_cipc(3) SP
by (auto simp:cp2sproc.simps obj2sobj.simps split:option.splits)
