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" 

  and init_flag_of_proc_shm :: "t_process \<Rightarrow> t_shm \<rightharpoonup> t_shm_attach_flag"

*)

  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> (p, fd) \<notin> init_sockets"

  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_flag_of_proc_shm p h = Some flag"

  and init_shmflag_has_proc:   "\<And> p h flag. init_flag_of_proc_shm p h = Some flag \<Longrightarrow> (p, flag) \<in> init_procs_of_shm h"

*)

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

  and init_msgs_valid:         "\<And> m q. m \<in> set (init_msgs_of_queue q) \<Longrightarrow> q \<in> init_msgqs"

  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> init_file_of_proc_fd p fd = None"

  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_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)"

definition init_same_inode_files :: "t_file \<Rightarrow> t_file set"

where

  "init_same_inode_files f \<equiv> if is_init_file f then {f'. init_inum_of_file f = init_inum_of_file f'} else {}"

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 # \<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}"

definition proc_file_fds :: "t_state \<Rightarrow> t_process \<Rightarrow> t_fd set"

where

  "proc_file_fds s p \<equiv> {fd. \<exists> f. file_of_proc_fd s p fd = Some f}"

definition init_proc_file_fds:: "t_process \<Rightarrow> t_fd set"

where

  "init_proc_file_fds p \<equiv> {fd. \<exists> f. init_file_of_proc_fd 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>) = (inum_of_file \<tau>) (f := None)"

| "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}" 

(* 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>"  

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 same_inode_files :: "t_state \<Rightarrow> t_file \<Rightarrow> t_file set"

where

  "same_inode_files s f \<equiv> if is_file s f then {f'. inum_of_file s f = inum_of_file s f'} else {}"

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

where 

  "has_same_inode s fa fb \<equiv> fb \<in> same_inode_files s fa"

*)

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 # \<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}"

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 # \<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 # \<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 flag_of_proc_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_shm \<Rightarrow> t_shm_attach_flag option"

where

  "flag_of_proc_shm [] = init_flag_of_proc_shm"

| "flag_of_proc_shm (Attach p h flag # s) = (\<lambda> p' h'. 

     if (p' = p \<and> h' = h) then Some flag else flag_of_proc_shm s p' h')"

| "flag_of_proc_shm (Detach p h # s) = (\<lambda> p' h'. 

     if (p' = p \<and> h' = h) then None else flag_of_proc_shm s p' h')"

| "flag_of_proc_shm (CreateShM p h # s) = (\<lambda> p' h'. 

     if (h' = h) then None else flag_of_proc_shm s p' h')"

| "flag_of_proc_shm (DeleteShM p h # s) = (\<lambda> p' h'. 

     if (h' = h) then None else flag_of_proc_shm s p' h')"

| "flag_of_proc_shm (Clone p p' fds shms # s) = (\<lambda> p'' h.

     if (p'' = p' \<and> h \<in> shms) then flag_of_proc_shm s p h

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

     else flag_of_proc_shm s p'' h)"

| "flag_of_proc_shm (Execve p f fds # s) = (\<lambda> p' h. 

     if (p' = p) then None else flag_of_proc_shm s p' h)"

| "flag_of_proc_shm (Kill p p' # s) = (\<lambda> p'' h. 

     if (p'' = p') then None else flag_of_proc_shm s p'' h)"

| "flag_of_proc_shm (Exit p # s) = (\<lambda> p' h. 

     if (p' = p) then None else flag_of_proc_shm s p' h)"

| "flag_of_proc_shm (e # s) = flag_of_proc_shm s"

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) | 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) | 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) | flag. (p, flag) \<in> procs_of_shm \<tau> h})"

| "procs_of_shm (Kill p p' # s) = 

    (\<lambda> h. (procs_of_shm s h) - {(p', flag) | flag. (p', flag) \<in> procs_of_shm s h})"

| "procs_of_shm (Exit p # s) = 

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

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

(*

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

where

  "p \<in> current_procs s \<Longrightarrow> info_flow_shm s p p"

| "\<lbrakk>info_flow_shm s p p'; (p', SHM_RDWR) \<in> procs_of_shm s h; (p'', flag) \<in> procs_of_shm s h; p' \<noteq> p''\<rbrakk>

   \<Longrightarrow> info_flow_shm s p p''"

*)

definition one_flow_shm :: "t_state \<Rightarrow> t_shm \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

where

  "one_flow_shm s h from to \<equiv> from \<noteq> to \<and> (from, SHM_RDWR) \<in> procs_of_shm s h \<and> 

                              (\<exists> flag. (to, flag) \<in> procs_of_shm s h)"

fun self_shm :: "t_state \<Rightarrow> t_process \<Rightarrow> t_process \<Rightarrow> bool"

where

  "self_shm s p p' = (p = p' \<and> p' \<in> current_procs s)"

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

where

  "info_flow_shm s from to \<equiv> (self_shm s from to) \<or> (\<exists> h. one_flow_shm s h from to)" 

*)

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))"