1723 

  1723 lemma s2ss_mkdir: "valid (Mkdir p f inum # s) \<Longrightarrow> s2ss (Mkdir p f inum # s) = (

  1724 

  1724   case (cf2sfile (Mkdir p f inum # s) f) of

  1725 

  1725     Some sf \<Rightarrow> (s2ss s) \<union> {S_dir sf}

  1726   | _       \<Rightarrow> {})"

  1727 apply (frule vt_grant_os, frule vd_cons, clarsimp)

  1728 apply (case_tac "cf2sfile (Mkdir p f inum # s) f")

  1729 apply (drule current_file_has_sfile', simp, simp add:current_files_simps, simp)

  1730 

  1731 apply (simp add:s2ss_def)

  1732 apply (tactic {*my_seteq_tac 1*}, simp)

  1733 apply (case_tac "obj = O_dir f")

  1734 apply (rule disjI1, simp add:co2sobj.simps)

  1735 apply (rule disjI2, rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_simps)

  1736 apply (tactic {*my_setiff_tac 1*}, simp)

  1737 apply (rule_tac x = "O_dir f" in exI, simp add:alive_mkdir co2sobj.simps)

  1738 apply (tactic {*my_setiff_tac 1*})

  1739 apply (case_tac "obj = O_dir f", simp add:is_dir_in_current)

  1740 apply (rule_tac x = obj in exI, simp add:co2sobj_mkdir alive_mkdir)

  1741 done

  1742 

  1743 definition update_s2ss_sfile_link:: "t_state \<Rightarrow> t_static_state \<Rightarrow> t_file \<Rightarrow> t_sfile \<Rightarrow> t_static_state"

  1744 where

  1745  "update_s2ss_sfile_link s ss f sf \<equiv>

  1746     if (\<exists> f'. is_file s f' \<and> f' \<notin> same_inode_files s f \<and> co2sobj s (O_file f') = co2sobj s (O_file f))

  1747        then ss \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}

  1748        else ss - {S_file (cf2sfiles s f) (O_file f \<in> Tainted s)} 

  1749                \<union> {S_file (cf2sfiles s f \<union> {sf}) (O_file f \<in> Tainted s)}"

  1750 

  1751 lemma s2ss_linkhard: "valid (LinkHard p f f' # s) \<Longrightarrow> s2ss (LinkHard p f f' # s) = (

  1752   case (cf2sfile (LinkHard p f f' # s) f') of

  1753     Some sf \<Rightarrow> update_s2ss_sfile_link s (s2ss s) f sf

  1754   | _       \<Rightarrow> {})"

  1755 apply (frule vt_grant_os, frule vd_cons, clarsimp)

  1756 apply (split option.splits)

  1757 apply (rule conjI, rule impI, drule current_file_has_sfile', simp, simp add:current_files_simps)

  1758 apply (rule allI, rule impI)

  1759 

  1760 apply (simp add:update_s2ss_sfile_link_def)

  1761 apply (rule conjI, rule impI, erule exE, erule conjE, erule conjE)

  1762 apply (simp add:s2ss_def)

  1763 apply (tactic {*my_seteq_tac 1*})

  1764 apply (case_tac "obj = O_file f'")

  1765 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted

  1766   same_inode_files_linkhard split:if_splits)

  1767 apply (case_tac "O_file f' \<in> Tainted s")

  1768 apply (drule Tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)

  1769 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1770 apply (rule disjI2, simp, rule_tac x = obj in exI)

  1771 apply (simp add:co2sobj_linkhard alive_linkhard)

  1772 apply (case_tac "fa \<in> same_inode_files s f")

  1773 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted 

  1774   same_inodes_Tainted split:if_splits)

  1775 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)

  1776 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard)

  1777 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)

  1778 apply (rule disjI2, simp, rule_tac x = obj in exI, simp add:co2sobj_linkhard)

  1779 apply (tactic {*my_setiff_tac 1*})

  1780 apply (rule_tac x = "O_file f" in exI)

  1781 apply (frule_tac obj = "O_file f" in co2sobj_linkhard)

  1782 apply (simp add:alive_linkhard)

  1783 apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)

  1784 apply (tactic {*my_setiff_tac 1*})

  1785 apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)

  1786 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1787 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1788 apply (case_tac "fa \<in> same_inode_files s f")

  1789 apply (rule_tac x = "O_file f'a" in exI, simp add:co2sobj_linkhard alive_linkhard)

  1790 apply (rule conjI, rule impI, simp add:is_file_in_current)

  1791 apply (rule impI, simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)

  1792 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1793 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1794 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1795 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1796 

  1797 apply (rule impI)

  1798 apply (simp add:s2ss_def)

  1799 apply (tactic {*my_seteq_tac 1*})

  1800 apply (case_tac "obj = O_file f'", simp)

  1801 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted

  1802   same_inode_files_linkhard split:if_splits)

  1803 apply (case_tac "O_file f' \<in> Tainted s")

  1804 apply (drule Tainted_in_current, simp, simp add:is_file_in_current alive.simps, simp)

  1805 apply (erule_tac obj = obj in co2sobj_some_caseD, simp)

  1806 apply (rule disjI2, rule conjI, rule_tac x = obj in exI)

  1807 apply (simp add:co2sobj_linkhard alive_linkhard)

  1808 apply (rule notI, simp add:co2sobj.simps split:option.splits)

  1809 apply (case_tac "fa \<in> same_inode_files s f")

  1810 apply (rule disjI1, simp add:co2sobj.simps cf2sfiles_linkhard tainted_eq_Tainted 

  1811   same_inodes_Tainted split:if_splits)

  1812 apply (simp, rule disjI2, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_file_simps)

  1813 apply (erule_tac x = fa in allE, rule notI)

  1814 apply (simp add:co2sobj_linkhard is_file_simps)

  1815 apply (simp add:co2sobj.simps tainted_eq_Tainted)

  1816 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard)

  1817 apply (rule notI, simp add:co2sobj.simps split:option.splits)

  1818 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard is_dir_simps)

  1819 apply (rule notI, simp add:co2sobj.simps split:option.splits)

  1820 apply (rule disjI2, simp, rule conjI, rule_tac x = obj in exI, simp add:co2sobj_linkhard)

  1821 apply (rule notI, simp add:co2sobj.simps split:option.splits)

  1822 apply (tactic {*my_setiff_tac 1*})

  1823 apply (rule_tac x = "O_file f" in exI)

  1824 apply (frule_tac obj = "O_file f" in co2sobj_linkhard)

  1825 apply (simp add:alive_linkhard)

  1826 apply (simp add:alive_linkhard same_inode_files_prop9 split:t_object.splits)

  1827 apply (tactic {*my_setiff_tac 1*})

  1828 apply (case_tac "obj = O_file f'", simp add:alive_linkhard is_file_in_current)

  1829 apply (erule_tac obj = obj in co2sobj_some_caseD)

  1830 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1831 apply (case_tac "fa \<in> same_inode_files s f")

  1832 apply (simp add:co2sobj.simps cf2sfiles_prop tainted_eq_Tainted same_inodes_Tainted)

  1833 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1834 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1835 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1836 apply (rule_tac x = obj in exI, simp add:co2sobj_linkhard alive_linkhard)

  1837 done

  1729   s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir

  1841   s2ss_readfile s2ss_writefile s2ss_closefd s2ss_unlink s2ss_rmdir s2ss_linkhard

  1730 

  1842   s2ss

  1843