Mercurial Mercurial > hg > selinux / comparison
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Init_prop.thy
changeset 6 8779d321cc2e
parent 4 e9c5594d5963
child 7 f27882976251
equal deleted inserted replaced
5:0c209a3e2647 6:8779d321cc2e 
   271 apply (erule_tac x = f' in allE, simp)
 
   271 apply (erule_tac x = f' in allE, simp)
 
   272 by (case_tac f', simp_all add:no_junior_def)
 
   272 by (case_tac f', simp_all add:no_junior_def)
 
   273 
   273 
   274 lemma same_inode_nil_prop:
 
   274 lemma same_inode_nil_prop:
 
   275   "same_inode_files [] f = init_same_inode_files f"
 
   275   "same_inode_files [] f = init_same_inode_files f"
 
   276 by (simp add:same_inode_files_def init_same_inode_files_def)
 
   276 by (simp add:same_inode_files_def init_same_inode_files_def is_file_nil)
 
   277 
   277 
   278 lemma init_same_inode_prop1:
 
   278 lemma init_same_inode_prop1:
 
   279   "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"
 
   279   "f \<in> init_files \<Longrightarrow> \<forall> f' \<in> init_same_inode_files f. f' \<in> init_files"
 
   280 apply (simp add:init_same_inode_files_def)
 
   280 apply (simp add:init_same_inode_files_def)
 
   281 apply (drule init_files_prop3)
 
   281 apply (drule init_files_prop3)
 
   282 apply (auto simp:init_files_prop1)
 
   282 apply (auto simp:init_files_prop1)
 
   283 done
 
   283 done
 
       
   284 
       
   285 lemma init_same_inode_prop2:
 
       
   286   "\<lbrakk>f' \<in> init_same_inode_files f; f \<in> init_files\<rbrakk> \<Longrightarrow> f' \<in> init_files"
 
       
   287 by (drule init_same_inode_prop1, simp)
 
       
   288 
       
   289 lemma init_same_inode_prop3:
 
       
   290   "f' \<in> init_same_inode_files f \<Longrightarrow> f \<in> init_same_inode_files f'"
 
       
   291 by (auto simp add:init_same_inode_files_def is_init_file_def split:if_splits)
 
       
   292 
       
   293 lemma init_same_inode_prop4:
 
       
   294   "\<lbrakk>f' \<in> init_same_inode_files f; f' \<in> init_files\<rbrakk> \<Longrightarrow> f \<in> init_files"
 
       
   295 apply (drule init_same_inode_prop3)
 
       
   296 by (simp add:init_same_inode_prop2)
 
   284 
   297 
   285 end
 
   298 end
 
   286 
   299 
   287 context flask begin
 
   300 context flask begin
 
   288 
   301 
   556 lemma sroot_valid:
 
   569 lemma sroot_valid:
 
   557   "init_cf2sfile [] = Some sroot"
 
   570   "init_cf2sfile [] = Some sroot"
 
   558 by (simp add:init_cf2sfile_def)
 
   571 by (simp add:init_cf2sfile_def)
 
   559 
   572 
   560 lemma sroot_valid':
 
   573 lemma sroot_valid':
 
   561   "cf2sfile s [] False = Some sroot"
 
   574   "cf2sfile s [] = Some sroot"
 
   562 by (simp add:cf2sfile_def)  
   575 by (simp add:cf2sfile_def)  
   563 
   576 
   564 lemma init_sectxt_prop:
 
   577 lemma init_sectxt_prop:
 
   565   "sectxt_of_obj [] obj = init_sectxt_of_obj obj"
 
   578   "sectxt_of_obj [] obj = init_sectxt_of_obj obj"
 
   566 apply (auto simp:init_sectxt_of_obj_def sectxt_of_obj_def split:option.splits)
 
   579 apply (auto simp:init_sectxt_of_obj_def sectxt_of_obj_def split:option.splits)
 
   644   "q \<in> init_msgqs \<Longrightarrow> \<exists> sq. init_cq2smsgq q = Some sq"
 
   657   "q \<in> init_msgqs \<Longrightarrow> \<exists> sq. init_cq2smsgq q = Some sq"
 
   645 apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)
 
   658 apply (frule init_msgq_has_ctxt, erule exE, drule init_cqm2sms_has_sms, erule exE)
 
   646 apply (simp add:init_cq2smsgq_def)
 
   659 apply (simp add:init_cq2smsgq_def)
 
   647 by (case_tac sec, simp+)
 
   660 by (case_tac sec, simp+)
 
   648 
   661 
   649 lemma cf2sfile_nil_prop1:
 
   662 lemma cf2sfile_nil_prop:
 
   650   "f \<in> init_files \<Longrightarrow> cf2sfile [] f (is_init_file f) = init_cf2sfile f"
 
   663   "f \<in> init_files \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 
   651 apply (case_tac f)
 
   664 apply (case_tac f)
 
   652 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
 
   665 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
 
   653 apply (rule notI, drule root_is_init_dir', simp)
 
       
   654 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
 
   666 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
 
   655 apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits
 
   667 apply (auto simp:is_init_file_def is_init_dir_def is_file_nil split:option.splits t_inode_tag.splits 
   656             dest:init_file_has_inum inof_has_file_tag)
 
   668             dest:init_file_has_inum inof_has_file_tag)
 
   657 done
 
   669 done
 
   658 
       
   659 
   670 
   660 lemma init_sec_file_dir:
 
   671 lemma init_sec_file_dir:
 
   661   "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False"
 
   672   "\<lbrakk>init_sectxt_of_obj (O_file f) = Some x; init_sectxt_of_obj (O_dir f) = Some y\<rbrakk> \<Longrightarrow> False"
 
   662 apply (drule init_sectxt_prop2)+
 
   673 apply (drule init_sectxt_prop2)+
 
   663 apply (auto intro:init_file_dir_conflict)
 
   674 apply (auto intro:init_file_dir_conflict)
 
   664 done
 
   675 done
 
   665 
   676 
   666 lemma cf2sfile_nil_prop2:
 
       
   667   "f \<in> init_files \<Longrightarrow> cf2sfile [] f (\<not> is_init_file f) = None"
 
       
   668 apply (case_tac f)
 
       
   669 apply (simp add:init_sectxt_prop cf2sfile_def init_cf2sfile_def)
 
       
   670 apply (rule notI, drule root_is_init_dir', simp)
 
       
   671 apply (auto simp:init_sectxt_prop cf2sfile_def init_cf2sfile_def split:option.splits dest!:init_has_ctxt')
 
       
   672 apply (auto simp:is_init_file_def is_init_dir_def split:option.splits t_inode_tag.splits
 
       
   673             dest:init_file_has_inum inof_has_file_tag init_sec_file_dir)
 
       
   674 done
 
       
   675 
       
   676 lemma cf2sfile_nil_prop:
 
       
   677   "f \<in> init_files \<Longrightarrow> cf2sfile [] f = (\<lambda> b. if (b = is_init_file f) then init_cf2sfile f else None)"
 
       
   678 apply (frule cf2sfile_nil_prop1, frule cf2sfile_nil_prop2)
 
       
   679 by (rule ext, auto split:if_splits)
 
       
   680 
       
   681 lemma cf2sfile_nil_prop3:
 
   677 lemma cf2sfile_nil_prop3:
 
   682   "is_init_file f \<Longrightarrow> cf2sfile [] f True = init_cf2sfile f"
 
   678   "is_init_file f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 
   683 by (simp add:is_init_file_prop1 cf2sfile_nil_prop)
 
   679 by (simp add:is_init_file_prop1 cf2sfile_nil_prop)
 
   684 
   680 
   685 lemma cf2sfile_nil_prop4:
 
   681 lemma cf2sfile_nil_prop4:
 
   686   "is_init_dir f \<Longrightarrow> cf2sfile [] f False = init_cf2sfile f"
 
   682   "is_init_dir f \<Longrightarrow> cf2sfile [] f = init_cf2sfile f"
 
   687 apply (frule init_file_dir_conflict2)
 
   683 apply (frule init_file_dir_conflict2)
 
   688 by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop)
 
   684 by (simp add:is_init_file_prop1 is_init_dir_prop1 cf2sfile_nil_prop)
 
   689 
   685 
   690 lemma cfs2sfiles_nil_prop:
 
   686 lemma cfs2sfiles_nil_prop:
 
   691   "\<forall> f \<in> fs. f \<in> init_files \<Longrightarrow> cfs2sfiles [] fs = init_cfs2sfiles fs"
 
   687   "f \<in> init_files \<Longrightarrow> cf2sfiles [] f = init_cf2sfiles f"
 
   692 apply (simp add:cfs2sfiles_def init_cfs2sfiles_def)
 
   688 apply (simp add:cf2sfiles_def init_cf2sfiles_def)
 
   693 apply (rule set_eqI, rule iffI, auto simp:cf2sfile_nil_prop split:if_splits)
 
   689 apply (rule set_eqI, rule iffI, auto split:if_splits)
 
       
   690 apply (rule_tac x = f' in bexI, simp add:same_inode_nil_prop cf2sfile_nil_prop)
 
       
   691 apply (drule init_same_inode_prop2, simp)
 
       
   692 apply (simp add:cf2sfile_nil_prop)
 
       
   693 apply (simp add:same_inode_nil_prop)
 
       
   694 apply (rule_tac x = f' in bexI)
 
       
   695 apply (drule init_same_inode_prop2, simp)
 
       
   696 apply ( simp add:same_inode_nil_prop cf2sfile_nil_prop)
 
       
   697 apply (simp add:same_inode_nil_prop)
 
   694 done
 
   698 done
 
   695 
   699 
   696 lemma cfd2sfd_nil_prop:
 
   700 lemma cfd2sfd_nil_prop:
 
   697   "init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd"
 
   701   "init_file_of_proc_fd p fd = Some f \<Longrightarrow> cfd2sfd [] p fd = init_cfd2sfd p fd"
 
   698 apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def)
 
   702 apply (simp add:cfd2sfd_def init_sectxt_prop init_cfd2sfd_def)
 
   760                      same_inode_nil_prop  cm2smsg_nil_prop 
   764                      same_inode_nil_prop  cm2smsg_nil_prop 
   761             dest:init_same_inode_prop1 
   765             dest:init_same_inode_prop1 
   762                split:option.splits)
 
   766                split:option.splits)
 
   763 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
 
   767 apply (rule_tac x = list in exI, simp add:init_same_inode_files_def)
 
   764 apply (simp add:init_files_props)
 
   768 apply (simp add:init_files_props)
 
   765 apply (auto simp:is_dir_nil is_file_nil dest:init_file_dir_conflict)
 
   769 apply (auto simp:is_dir_nil is_file_nil init_files_prop4 dest:init_file_dir_conflict)
 
   766 done
 
   770 done
 
   767 
   771 
   768 lemma s2ss_nil_prop:
 
   772 lemma s2ss_nil_prop:
 
   769   "s2ss [] = init_static_state"
 
   773   "s2ss [] = init_static_state"
 
   770 using co2sobj_nil_prop init_alive_prop
 
   774 using co2sobj_nil_prop init_alive_prop
selinux