theory Flask

imports Main Flask_type OS_type_def File_renaming 

begin

(****** Policy-language-level rule match/auxiliary functions ******)

fun patt_match :: "'a patt \<Rightarrow> 'a \<Rightarrow> bool"

where

  "patt_match (Single x) y = (x = y)"

| "patt_match (Set s)    x = (x \<in> s)"

| "patt_match (Tilde s)  x = (x \<notin> s)"

| "patt_match Asterisk   x = True"

(* match a target with a patt, but including the SELF special 

 * patt_match_self patt target source 

 *)

fun patt_match_self :: "(type_t patt) target_with_self_t \<Rightarrow> type_t \<Rightarrow> type_t \<Rightarrow> bool"

where

  "patt_match_self Self                  tt st = (tt = st)"

| "patt_match_self (Not_self (Single p)) tt st = (tt = p)"

| "patt_match_self (Not_self (Set p))    tt st = (tt \<in> p)"

| "patt_match_self (Not_self (Tilde p))  tt st = (tt \<notin> p)"

| "patt_match_self (Not_self Asterisk)   tt st = True"

(* list lookup: find the first one *)

fun lookup :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a option"

where

  "lookup [] P = None"

| "lookup (x # xs) P = (if (P x) then Some x else lookup xs P)"

(* list member: if exists an element satisfy predicate P *)

fun member :: "'a list \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool"

where

  "member [] P = False"

| "member (x # xs) P = (if (P x) then True else member xs P)"

(******* socket related aux functions ********)

fun is_remote_request :: "t_event \<Rightarrow> bool"    

where

  "is_remote_request (Accept p fd addr port fd' i)  = True"

| "is_remote_request (Connect p fd addr)   = True"

| "is_remote_request (SendSock p fd) = True"

| "is_remote_request (RecvSock p fd) = True"

| "is_remote_request e         = False"

fun ip_of_addr:: "t_sock_addr \<Rightarrow> t_inet_addr"

where

  "ip_of_addr (INET_ADDR saddr sport) = saddr"

fun port_of_addr:: "t_sock_addr \<Rightarrow> t_socket_port"

where

  "port_of_addr (INET_ADDR saddr sport) = sport"

fun after_bind:: "t_sock_state option \<Rightarrow> bool"

where

  "after_bind None = False"

| "after_bind (Some SS_create) = False"

| "after_bind _= True" (* after bind , it should have local addr *)

fun after_conacc:: "t_sock_state option \<Rightarrow> bool"

where

  "after_conacc None = False"

| "after_conacc (Some SS_create) = False"

| "after_conacc (Some SS_bind) = False"

| "after_conacc (Some SS_listen) = False"

| "after_conacc _ = True"  (* after connect or accept, it should have remote addr *)

(* inet_addr_compare addr1 addr2 \<equiv> addr1 \<le> addr2; but in \<le>'s def,there is a \<exists>, is not a function*)

fun subnet_addr :: "t_inet_addr \<Rightarrow> t_inet_addr \<Rightarrow> bool"

where

  "subnet_addr []     addr   = True"

| "subnet_addr (x#xs) []     = False"

| "subnet_addr (x#xs) (y#ys) = ((x = y) \<and> subnet_addr xs ys)"

definition port_in_range :: "t_socket_port \<Rightarrow> t_socket_port \<Rightarrow> t_socket_port \<Rightarrow> bool"

where

  "port_in_range minp maxp p \<equiv> ((p < maxp \<or> p = maxp) \<and> (p > minp \<or> p = minp))"

(* initial value of initiate state constrains aux function *)

definition bidirect_in_init :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b option) \<Rightarrow> bool"

where

  "bidirect_in_init S f \<equiv>  (\<forall> a. a \<in> S \<longrightarrow> (\<exists> b. f a = Some b)) \<and> 

                           (\<forall> a b. f a = Some b \<longrightarrow> a \<in> S)" 

fun is_file_itag :: "t_inode_tag \<Rightarrow> bool"

where

  "is_file_itag Tag_FILE = True"

| "is_file_itag tag      = False"

fun is_dir_itag :: "t_inode_tag \<Rightarrow> bool"

where

  "is_dir_itag Tag_DIR = True"

| "is_dir_itag tag     = False"

fun is_file_dir_itag :: "t_inode_tag \<Rightarrow> bool"

where

  "is_file_dir_itag Tag_FILE = True"

| "is_file_dir_itag Tag_DIR  = True"

| "is_file_dir_itag tag      = False"

fun is_tcp_itag :: "t_inode_tag \<Rightarrow> bool"

where

  "is_tcp_itag Tag_TCP_SOCK = True"

| "is_tcp_itag tag      = False"

fun is_udp_itag :: "t_inode_tag \<Rightarrow> bool"

where

  "is_udp_itag Tag_UDP_SOCK = True"

| "is_udp_itag tag     = False"

fun is_sock_itag :: "t_inode_tag \<Rightarrow> bool"

where

  "is_sock_itag Tag_TCP_SOCK = True"

| "is_sock_itag Tag_UDP_SOCK = True"

| "is_sock_itag tag          = False"

locale init = 

  fixes 

      init_files :: "t_file set"

  and init_procs :: "t_process set"

  and init_nodes :: "t_node set"

  and init_sockets :: "t_socket set"

  and init_users :: "user_t set"

  and init_file_of_proc_fd ::   "t_process \<Rightarrow> t_fd \<rightharpoonup> t_file"

  and init_fds_of_proc ::       "t_process \<Rightarrow> t_fd set"

  and init_oflags_of_proc_fd::  "t_process \<Rightarrow> t_fd \<rightharpoonup> t_open_flags"

  and init_inum_of_file ::      "t_file \<rightharpoonup> t_inode_num"

  and init_inum_of_socket::     "t_socket  \<rightharpoonup> t_inode_num" 

  and init_itag_of_inum::       "t_inode_num \<rightharpoonup> t_inode_tag"

  and init_files_hung_by_del :: "t_file set"

(*

  and init_file_at_writing_by:: "t_file \<Rightarrow> (t_process \<times> t_fd) set"

*)

  and init_socket_state ::      "t_socket \<rightharpoonup> t_sock_state"

  and init_msgqs :: "t_msgq set"

  and init_msgs_of_queue:: "t_msgq \<Rightarrow> t_msg list"

  and init_shms :: "t_shm set"

  and init_procs_of_shm :: "t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set" 

  assumes

      parent_file_in_init: "\<And> f pf. \<lbrakk>parent f = Some pf; f \<in> init_files\<rbrakk> \<Longrightarrow> pf \<in> init_files"

  and root_is_dir: "\<exists> i. init_inum_of_file [] = Some i \<and> init_itag_of_inum i = Some Tag_DIR"

  and init_file_has_inum:  "\<And> f. f \<in> init_files \<Longrightarrow> \<exists> im. init_inum_of_file f = Some im"

  and inof_has_file_tag:   "\<And> f im. init_inum_of_file f = Some im \<Longrightarrow> f \<in> init_files \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_file_dir_itag tag)"

  and init_file_no_son:    "\<And> f im. \<lbrakk>init_inum_of_file f = Some im; init_itag_of_inum im = Some Tag_FILE\<rbrakk> \<Longrightarrow> \<not> (\<exists> f' \<in> init_files. parent f' = Some f)"

  and init_parentf_is_dir: "\<And> f pf im. \<lbrakk>parent f = Some pf; f \<in> init_files; init_inum_of_file pf = Some im\<rbrakk> \<Longrightarrow> init_itag_of_inum im = Some Tag_DIR"

  and init_files_hung_valid:   "\<And> f. f \<in> init_files_hung_by_del \<Longrightarrow> f \<in> init_files \<and> (\<exists> p fd. init_file_of_proc_fd p fd = Some f)"

  and init_files_hung_valid':  "\<And> f im. \<lbrakk>f \<in> init_files_hung_by_del; init_inum_of_file f = Some im\<rbrakk> \<Longrightarrow> 

                                         init_itag_of_inum im = Some Tag_FILE \<or> (init_itag_of_inum im = Some Tag_DIR \<and> \<not> (\<exists> f'. f' \<in> init_files \<and> f \<prec> f'))"

  and init_procfds_valid:      "\<And> p fd. fd \<in> init_fds_of_proc p \<Longrightarrow> p \<in> init_procs \<and> ((\<exists> f \<in> init_files. init_file_of_proc_fd p fd = Some f) \<or> (p, fd) \<in> init_sockets)"

  and init_filefd_valid:       "\<And> p fd f. init_file_of_proc_fd p fd = Some f \<Longrightarrow> fd \<in> init_fds_of_proc p \<and> (\<exists> im. init_inum_of_file f = Some im \<and> init_itag_of_inum im = Some Tag_FILE) \<and> p \<in> init_procs \<and> (\<exists> flags. init_oflags_of_proc_fd p fd = Some flags)"

  and init_fileflag_valid:     "\<And> p fd flags. init_oflags_of_proc_fd p fd = Some flags \<Longrightarrow> \<exists> f. init_file_of_proc_fd p fd = Some f"

  and init_procs_has_shm:      "\<And> p h flag. (p,flag) \<in> init_procs_of_shm h \<Longrightarrow> p \<in> init_procs \<and> h \<in> init_shms"

  and init_msgs_distinct:      "\<And> q. distinct (init_msgs_of_queue q)"

  and init_socket_has_inode:   "\<And> p fd. (p, fd) \<in> init_sockets \<Longrightarrow> \<exists> im. init_inum_of_socket (p, fd) = Some im \<and> p \<in> init_procs \<and> fd \<in> init_fds_of_proc p"

  and inos_has_sock_tag:  "\<And> s im. init_inum_of_socket s = Some im \<Longrightarrow> s \<in> init_sockets \<and> (\<exists> tag. init_itag_of_inum im = Some tag \<and> is_sock_itag tag)"

(*

  and init_netobj_has_state:   "bidirect_in_init init_netobjs init_netobj_state"

  and init_netobj_has_socktype:"bidirect_in_init init_netobjs init_netobj_socktype"

  and init_netobj_has_laddr:   "\<And> s. after_bind (init_netobj_state s) \<Longrightarrow> init_netobj_localaddr s \<noteq> None"

  and init_netobj_has_raddr:   "\<And> s. after_conacc (init_netobj_state s) \<Longrightarrow> init_netobj_remoteaddr s \<noteq> None"

*)

  and init_finite_sets:   "finite init_files \<and> finite init_procs \<and> (\<forall> p. finite (init_fds_of_proc p)) \<and> finite init_shms \<and> finite init_msgqs \<and> finite init_users" 

begin 

definition is_init_file:: "t_file \<Rightarrow> bool"

where

  "is_init_file f \<equiv> (case (init_inum_of_file f) of

                       Some i \<Rightarrow> (case (init_itag_of_inum i) of

                                    Some Tag_FILE \<Rightarrow> True

                                  | _             \<Rightarrow> False)

                     | _      \<Rightarrow> False)"

definition is_init_dir:: "t_file \<Rightarrow> bool"

where

  "is_init_dir f \<equiv> (case (init_inum_of_file f) of

                      Some i \<Rightarrow> (case (init_itag_of_inum i) of

                                   Some Tag_DIR \<Rightarrow> True

                                 | _            \<Rightarrow> False)

                    | _      \<Rightarrow> False)"

definition is_init_tcp_sock:: "t_socket \<Rightarrow> bool"

where

  "is_init_tcp_sock s \<equiv> (case (init_inum_of_socket s) of

                           Some i \<Rightarrow> (case (init_itag_of_inum i) of

                                        Some Tag_TCP_SOCK \<Rightarrow> True

                                      | _                 \<Rightarrow> False)

                         | _      \<Rightarrow> False)"

definition is_init_udp_sock:: "t_socket \<Rightarrow> bool"

where

  "is_init_udp_sock s \<equiv> (case (init_inum_of_socket s) of

                           Some i \<Rightarrow> (case (init_itag_of_inum i) of

                                        Some Tag_UDP_SOCK \<Rightarrow> True

                                      | _                 \<Rightarrow> False)

                         | _      \<Rightarrow> False)"

fun init_alive :: "t_object \<Rightarrow> bool"

where

  "init_alive (O_proc p)     = (p \<in> init_procs)"

| "init_alive (O_file f)     = (is_init_file f)"

| "init_alive (O_dir  f)     = (is_init_dir  f)"

| "init_alive (O_fd p fd)    = (fd \<in> init_fds_of_proc p)"

| "init_alive (O_node n)     = (n \<in> init_nodes)"

| "init_alive (O_tcp_sock k) = (is_init_tcp_sock k)"

| "init_alive (O_udp_sock k) = (is_init_udp_sock k)"

| "init_alive (O_shm  h)     = (h \<in> init_shms)"

| "init_alive (O_msgq q)     = (q \<in> init_msgqs)"

| "init_alive (O_msg q m)    = (m \<in> set (init_msgs_of_queue q) \<and> q \<in> init_msgqs)"

(************ system listeners, event-related ***********)

fun file_of_proc_fd ::  "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_file option"

where

  "file_of_proc_fd [] p' fd' = (init_file_of_proc_fd p' fd')"

| "file_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' = 

     (if (p' = p \<and> fd = fd') then Some f else file_of_proc_fd \<tau> p' fd')"

| "file_of_proc_fd (CloseFd p fd # \<tau>) p' fd' = 

     (if (p = p' \<and> fd = fd') then None else file_of_proc_fd \<tau> p' fd')"

(*deleted: if (f\<^isub>3 \<preceq> f\<^isub>1) then None else *)

(*

| "file_of_proc_fd (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) p' fd = 

     (case (file_of_proc_fd \<tau> p' fd) of

        Some f\<^isub>1 \<Rightarrow> (if (f\<^isub>2 \<preceq> f\<^isub>1) then Some (file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1) 

                    else Some f\<^isub>1)

      | None    \<Rightarrow> None )"

*)

| "file_of_proc_fd (Execve p f fds # \<tau>) p' fd = 

     (if (p' = p \<and> fd \<in> fds) then file_of_proc_fd \<tau> p fd 

      else if (p' = p) then None

      else file_of_proc_fd \<tau> p' fd) "

| "file_of_proc_fd (Clone p p' fds shms # \<tau>) p'' fd = 

     (if (p'' = p' \<and> fd \<in> fds) then file_of_proc_fd \<tau> p fd

      else if (p'' = p') then None

      else file_of_proc_fd \<tau> p'' fd)"

| "file_of_proc_fd (Kill p\<^isub> p\<^isub>' # \<tau>) p'' fd = 

     (if (p'' = p\<^isub>') then None else file_of_proc_fd \<tau> p'' fd)"

| "file_of_proc_fd (Exit p # \<tau>) p' fd = 

     (if (p = p') then None else file_of_proc_fd \<tau> p' fd)"

| "file_of_proc_fd (_ # \<tau>) p fd = file_of_proc_fd \<tau> p fd"

definition proc_fd_of_file :: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set"

where

  "proc_fd_of_file \<tau> f = {(p, fd) | p fd. file_of_proc_fd \<tau> p fd = Some f}"

(****** files and directories ******)

fun files_hung_by_del :: "t_state \<Rightarrow> t_file set"

where

  "files_hung_by_del [] = init_files_hung_by_del"

| "files_hung_by_del (UnLink p f # \<tau>) = (

     if (proc_fd_of_file \<tau> f = {}) then files_hung_by_del \<tau> 

     else insert f (files_hung_by_del \<tau>))"

(* | files_hung_by_del (Rmdir p f) is not need, for open can only apply to file not dir *)

| "files_hung_by_del (CloseFd p fd # \<tau>) = (

     case (file_of_proc_fd \<tau> p fd) of

       Some f \<Rightarrow> (if (proc_fd_of_file \<tau> f = {(p, fd)}) 

                  then files_hung_by_del \<tau> - {f}

                  else files_hung_by_del \<tau>)

     | None   \<Rightarrow> files_hung_by_del \<tau>            )"

(*

| "files_hung_by_del (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = {file_after_rename f\<^isub>2 f\<^isub>3 f\<^isub>1| f\<^isub>1. f\<^isub>1 \<in> files_hung_by_del \<tau>}" (* for rename(2) does not infect on fd of the file, see man -S 2 rename *)

*)

| "files_hung_by_del (e # \<tau>) = files_hung_by_del \<tau>"

declare files_hung_by_del.simps [simp del]

fun inum_of_file :: "t_state \<Rightarrow> (t_file \<rightharpoonup> t_inode_num)"

where

  "inum_of_file [] = init_inum_of_file"

| "inum_of_file (Open p f flags fd (Some inum) # \<tau>) = (inum_of_file \<tau>) (f := Some inum)" 

| "inum_of_file (CloseFd p fd # \<tau>) = (

     case (file_of_proc_fd \<tau> p fd) of

       Some f \<Rightarrow> ( if ((proc_fd_of_file \<tau> f = {(p, fd)}) \<and> (f \<in> files_hung_by_del \<tau>)) 

                   then (inum_of_file \<tau>) (f := None)

                   else inum_of_file \<tau> )

     | _      \<Rightarrow> (inum_of_file \<tau>)    )"

| "inum_of_file (UnLink p f # \<tau>) = (

     if (proc_fd_of_file \<tau> f = {}) 

     then (inum_of_file \<tau>) (f := None)

     else inum_of_file \<tau>            )" 

| "inum_of_file (Rmdir p f # \<tau>) = (

     if (proc_fd_of_file \<tau> f = {}) 

     then (inum_of_file \<tau>) (f := None)

     else inum_of_file \<tau>          )" 

| "inum_of_file (Mkdir p f ino # \<tau>) = (inum_of_file \<tau>) (f:=  Some ino)"

| "inum_of_file (LinkHard p f\<^isub>1 f\<^isub>2 # \<tau>) = (inum_of_file \<tau>) (f\<^isub>2 := inum_of_file \<tau> f\<^isub>1)"

(*

| "inum_of_file (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) = (\<lambda> f. 

     if (f\<^isub>2 \<preceq> f) then None

     else if (f\<^isub>3 \<preceq> f) then inum_of_file \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f)

     else inum_of_file \<tau> f         )"

*)

| "inum_of_file (e # \<tau>) = inum_of_file \<tau>" 

definition current_files :: "t_state \<Rightarrow> t_file set"

where

  "current_files \<tau> = {f. \<exists> i. inum_of_file \<tau> f = Some i}" 

definition has_same_inode :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file \<Rightarrow> bool"

where 

  "has_same_inode \<tau> fa fb = 

     (\<exists>i. inum_of_file \<tau> fa = Some i \<and> inum_of_file \<tau> fb = Some i)"

fun inum_of_socket :: "t_state \<Rightarrow> (t_socket \<rightharpoonup> t_inode_num)"

where

  "inum_of_socket [] = init_inum_of_socket"

| "inum_of_socket (CloseFd p fd # \<tau>) = 

     (inum_of_socket \<tau>) ((p, fd):= None)"

| "inum_of_socket (CreateSock p af st fd ino # \<tau>) = 

     (inum_of_socket \<tau>) ((p, fd) := Some ino)"

| "inum_of_socket (Accept p fd addr lport' fd' ino # \<tau>) = 

     (inum_of_socket \<tau>) ((p, fd') := Some ino)"

| "inum_of_socket (Clone p p' fds shms # \<tau>) = 

     (\<lambda> (p'', fd). if (p'' = p' \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd) 

                   else if (p'' = p') then None

                   else inum_of_socket \<tau> (p'',fd))" 

| "inum_of_socket (Execve p f fds # \<tau>) = 

     (\<lambda> (p', fd). if (p' = p \<and> fd \<in> fds) then inum_of_socket \<tau> (p, fd)

                  else if (p' = p) then None

                  else inum_of_socket \<tau> (p', fd))"

| "inum_of_socket (Kill p\<^isub>1 p\<^isub>2 # \<tau>) = 

     (\<lambda> (p, fd). if (p = p\<^isub>2) then None else inum_of_socket \<tau> (p, fd) )"

| "inum_of_socket (Exit p # \<tau>) = 

     (\<lambda> (p', fd). if (p' = p) then None else inum_of_socket \<tau> (p', fd))"

| "inum_of_socket (_ # \<tau>) = inum_of_socket \<tau>" 

definition current_sockets :: "t_state \<Rightarrow> t_socket set"

where

  "current_sockets \<tau> = {s. \<exists> i. inum_of_socket \<tau> s = Some i}"

(* experimentary: for the delete obj's (file or socket) inode num, it is unnecessary for itag_of_inum to be NONE, cause this is the situation blocked by inum_of_file / inum_of_socket !!! *)  

(* delete a file, just recycle its inode num, but not destroy its inode \<dots>, so it is irrelative to these events, like closeFd, Rmdir, UnLink \<dots>*)

fun itag_of_inum :: "t_state \<Rightarrow> (t_inode_num \<rightharpoonup> t_inode_tag)"

where

  "itag_of_inum [] = init_itag_of_inum"

| "itag_of_inum (Open p f flags fd (Some ino) # \<tau>) = (itag_of_inum \<tau>) (ino := Some Tag_FILE)"

| "itag_of_inum (Mkdir p f ino # \<tau>) = (itag_of_inum \<tau>) (ino := Some Tag_DIR)" 

| "itag_of_inum (CreateSock p af st fd ino # \<tau>) = 

     (case st of 

        STREAM \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)

      | DGRAM  \<Rightarrow> (itag_of_inum \<tau>) (ino := Some Tag_UDP_SOCK) )"

| "itag_of_inum (Accept p fd addr lport' fd' ino # \<tau>) = 

     (itag_of_inum \<tau>) (ino := Some Tag_TCP_SOCK)"

| "itag_of_inum (_ # \<tau>) = itag_of_inum \<tau>"  (* may be sth wrong with nettemp representing addr \<times> netdev in statical analysis ??? *)

definition is_file:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"

where

  "is_file \<tau> f \<equiv> (case (inum_of_file \<tau> f) of

                    Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of

                                 Some Tag_FILE \<Rightarrow> True

                               | _             \<Rightarrow> False)

                  | _      \<Rightarrow> False)"

definition is_dir:: "t_state \<Rightarrow> t_file \<Rightarrow> bool"

where

  "is_dir \<tau> f \<equiv> (case (inum_of_file \<tau> f) of

                    Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of

                                 Some Tag_DIR \<Rightarrow> True

                               | _            \<Rightarrow> False)

                  | _      \<Rightarrow> False)"

definition dir_is_empty :: "t_state \<Rightarrow> t_file \<Rightarrow> bool"

where

  "dir_is_empty \<tau> f \<equiv> is_dir \<tau> f \<and> \<not> (\<exists> f'. f' \<in> current_files \<tau> \<and> f \<prec> f')"

definition is_tcp_sock :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"

where

  "is_tcp_sock \<tau> s \<equiv> (case (inum_of_socket \<tau> s) of

                        Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of

                                     Some Tag_TCP_SOCK \<Rightarrow> True

                                   | _                 \<Rightarrow> False)

                      | _      \<Rightarrow> False)"

definition is_udp_sock :: "t_state \<Rightarrow> t_socket \<Rightarrow> bool"

where

  "is_udp_sock \<tau> s \<equiv> (case (inum_of_socket \<tau> s) of

                        Some i \<Rightarrow> (case (itag_of_inum \<tau> i) of

                                     Some Tag_UDP_SOCK \<Rightarrow> True

                                   | _                 \<Rightarrow> False)

                      | _      \<Rightarrow> False)"

fun current_procs :: "t_state \<Rightarrow> t_process set"

where

  "current_procs [] = init_procs"

| "current_procs (Clone p p' fds shms # \<tau>) = (insert p' (current_procs \<tau>))"

| "current_procs (Exit p # \<tau>) = (current_procs \<tau> - {p})"

| "current_procs (Kill p p' # \<tau>) = (current_procs \<tau> - {p'})"

| "current_procs (_ # \<tau>) = current_procs \<tau>" 

fun current_proc_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set" 

where  

  "current_proc_fds [] = init_fds_of_proc"

| "current_proc_fds (Open p f flags fd iopt # \<tau>) = 

     (current_proc_fds \<tau>) (p:= insert fd (current_proc_fds \<tau> p))"

| "current_proc_fds (CreateSock p sf st newfd newi # \<tau>) =

     (current_proc_fds \<tau>) (p:= insert newfd (current_proc_fds \<tau> p))" 

| "current_proc_fds (Accept p fd raddr port fd' ino # \<tau>) = 

     (current_proc_fds \<tau>) (p:= insert fd' (current_proc_fds \<tau> p))"

| "current_proc_fds (CloseFd p fd # \<tau>) = 

     (current_proc_fds \<tau>) (p:= (current_proc_fds \<tau> p) - {fd})"

| "current_proc_fds (Clone p p' fds shms # \<tau>) = 

     (current_proc_fds \<tau>) (p':= fds)"

| "current_proc_fds (Execve p f fds # \<tau>) = 

     (current_proc_fds \<tau>) (p:= fds)"

| "current_proc_fds (Exit p # \<tau>) = (current_proc_fds \<tau>) (p := {})"

| "current_proc_fds (Kill p p' # \<tau>) = (current_proc_fds \<tau>) (p' := {})"

| "current_proc_fds (_ # \<tau>) = current_proc_fds \<tau>"

fun current_shms :: "t_state \<Rightarrow> t_shm set"

where

  "current_shms [] = init_shms"

| "current_shms (CreateShM p newshm # \<tau>) = insert newshm (current_shms \<tau>)"

| "current_shms (DeleteShM p s # \<tau>) = (current_shms \<tau>) - {s}"

| "current_shms (e # \<tau>) = current_shms \<tau> "

fun procs_of_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> (t_process \<times> t_shm_attach_flag) set"

where

  "procs_of_shm [] = init_procs_of_shm"

| "procs_of_shm (CreateShM p h # \<tau>) = 

    (procs_of_shm \<tau>) (h := {})"  (* creator may not be the sharer of the shm *)

| "procs_of_shm (Attach p h flag # \<tau>) = 

    (procs_of_shm \<tau>) (h := insert (p, flag) (procs_of_shm \<tau> h))"

| "procs_of_shm (Detach p h # \<tau>) =

    (procs_of_shm \<tau>) (h := (procs_of_shm \<tau> h) - {(p,flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"

| "procs_of_shm (DeleteShM p h # \<tau>) = (procs_of_shm \<tau>) (h := {})"

| "procs_of_shm (Clone p p' fds shms # \<tau>) = 

    (\<lambda> h. if (h \<in> shms) 

          then (procs_of_shm \<tau> h) \<union> {(p', flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h}

          else procs_of_shm \<tau> h)"

| "procs_of_shm (Execve p f fds # \<tau>) = 

    (\<lambda> h. procs_of_shm \<tau> h - {(p, flag). \<exists> flag. (p, flag) \<in> procs_of_shm \<tau> h})"

| "procs_of_shm (e # \<tau>)          = procs_of_shm \<tau>"

definition info_flow_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

where

  "info_flow_shm \<tau> from to \<equiv> (from = to) \<or> (\<exists> h \<in> current_shms \<tau>. \<exists> toflag. 

    (((from, SHM_RDWR) \<in> procs_of_shm \<tau> h) \<and> ((to, toflag) \<in> procs_of_shm \<tau> h)))"

fun current_msgqs :: "t_state \<Rightarrow> t_msg set"

where

  "current_msgqs [] = init_msgqs"

| "current_msgqs (CreateMsgq p q # \<tau>) = insert q (current_msgqs \<tau>)"

| "current_msgqs (RemoveMsgq p q # \<tau>) = (current_msgqs \<tau>) - {q}"

| "current_msgqs (_ # \<tau>) = current_msgqs \<tau>"

fun msgs_of_queue :: "t_state \<Rightarrow> t_msgq \<Rightarrow> t_msg list"

where

  "msgs_of_queue [] = init_msgs_of_queue"

| "msgs_of_queue (CreateMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])"

| "msgs_of_queue (SendMsg p q m  # \<tau>) = (msgs_of_queue \<tau>)(q := msgs_of_queue \<tau> q @ [m])"

| "msgs_of_queue (RecvMsg p q m  # \<tau>) = (msgs_of_queue \<tau>)(q := tl (msgs_of_queue \<tau> q))"

| "msgs_of_queue (RemoveMsgq p q # \<tau>) = (msgs_of_queue \<tau>)(q := [])" 

| "msgs_of_queue (_ # \<tau>) = msgs_of_queue \<tau>"         

definition current_file_inums :: "t_state \<Rightarrow> t_inode_num set"

where

  "current_file_inums \<tau> \<equiv> {im. \<exists> f. inum_of_file \<tau> f = Some im}"

definition current_sock_inums :: "t_state \<Rightarrow> t_inode_num set"

where

  "current_sock_inums \<tau> = {im. \<exists> s. inum_of_socket \<tau> s = Some im}"

definition current_inode_nums :: "t_state \<Rightarrow> nat set"

where

  "current_inode_nums \<tau> = current_file_inums \<tau> \<union> current_sock_inums \<tau>"

fun flags_of_proc_fd :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd \<Rightarrow> t_open_flags option"

where

  "flags_of_proc_fd [] p fd = init_oflags_of_proc_fd p fd" 

| "flags_of_proc_fd (Open p f flags fd iopt # \<tau>) p' fd' = 

     (if (p = p' \<and> fd = fd') then Some flags else flags_of_proc_fd \<tau> p' fd')"

| "flags_of_proc_fd (CloseFd p fd # \<tau>) p' fd' = 

     (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"

| "flags_of_proc_fd (CreateSock p af st fd ino # \<tau>) p' fd' = 

     (if (p = p' \<and> fd = fd') then None else flags_of_proc_fd \<tau> p' fd')"

| "flags_of_proc_fd (Accept p fd addr lport' fd' ino # \<tau>) p' fd'' = 

     (if (p = p' \<and> fd' = fd'') then None else flags_of_proc_fd \<tau> p' fd'')"

| "flags_of_proc_fd (Clone p p' fds shms # \<tau>) p'' fd = 

     (if (p' = p'' \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p'' fd)"  

| "flags_of_proc_fd (Execve p f fds # \<tau>) p' fd = 

     (if (p' = p \<and> fd \<in> fds) then flags_of_proc_fd \<tau> p fd else flags_of_proc_fd \<tau> p' fd)"

| "flags_of_proc_fd (Kill p\<^isub>1 p\<^isub>2 # \<tau>) p fd = 

     (if (p = p\<^isub>2) then None else flags_of_proc_fd \<tau> p fd)"

| "flags_of_proc_fd (Exit p # \<tau>) p' fd' = 

     (if (p = p') then None else flags_of_proc_fd \<tau> p' fd')"

| "flags_of_proc_fd (e # \<tau>) p fd = flags_of_proc_fd \<tau> p fd" 

(* 

fun file_at_writing_by:: "t_state \<Rightarrow> t_file \<Rightarrow> (t_process \<times> t_fd) set"

where

  "file_at_writing_by [] f = init_file_at_writing_by f"  

| "file_at_writing_by (Open p f flags fd (Some inum) # \<tau>) f' = (

     if (f' = f) 

     then ( if (is_write_flag flags) 

            then {(p, fd)}

            else {} )

     else file_at_writing_by \<tau> f'                              )"

| "file_at_writing_by (Open p f flags fd None # \<tau>) f' = (

     if (f' = f \<and> is_write_flag flags) 

     then insert (p, fd) (file_at_writing_by \<tau> f) 

     else file_at_writing_by \<tau> f'                       )"

| "file_at_writing_by (Mkdir p f inum # \<tau>) f' = 

     (if (f' = f) then {} else file_at_writing_by \<tau> f')"

| "file_at_writing_by (LinkHard p f f' # \<tau>) f'' = 

     (if (f'' = f') then file_at_writing_by \<tau> f else file_at_writing_by \<tau> f'')"

| "file_at_writing_by (Rename p f\<^isub>2 f\<^isub>3 # \<tau>) f = (

     if (f\<^isub>3 \<preceq> f) then file_at_writing_by \<tau> (file_before_rename f\<^isub>2 f\<^isub>3 f)

     else file_at_writing_by \<tau> f               )"

| "file_at_writing_by (CloseFd p fd # \<tau>) f =