src/HOL/Unix/Unix.thy
author wenzelm
Sat Sep 17 14:02:31 2005 +0200 (2005-09-17)
changeset 17455 151e76f0e3c7
parent 17146 67e9b86ed211
child 18372 2bffdf62fe7f
permissions -rw-r--r--
tuned document;
wenzelm@10966
     1
(*  Title:      HOL/Unix/Unix.thy
wenzelm@10966
     2
    ID:         $Id$
wenzelm@10966
     3
    Author:     Markus Wenzel, TU Muenchen
wenzelm@10966
     4
*)
wenzelm@10966
     5
wenzelm@10966
     6
header {* Unix file-systems \label{sec:unix-file-system} *}
wenzelm@10966
     7
wenzelm@17455
     8
theory Unix
wenzelm@17455
     9
imports Nested_Environment List_Prefix
wenzelm@17455
    10
begin
wenzelm@10966
    11
wenzelm@10966
    12
text {*
wenzelm@10966
    13
  We give a simple mathematical model of the basic structures
wenzelm@10966
    14
  underlying the Unix file-system, together with a few fundamental
wenzelm@10966
    15
  operations that could be imagined to be performed internally by the
wenzelm@10966
    16
  Unix kernel.  This forms the basis for the set of Unix system-calls
wenzelm@10966
    17
  to be introduced later (see \secref{sec:unix-trans}), which are the
wenzelm@10966
    18
  actual interface offered to processes running in user-space.
wenzelm@10966
    19
wenzelm@10966
    20
  \medskip Basically, any Unix file is either a \emph{plain file} or a
wenzelm@10966
    21
  \emph{directory}, consisting of some \emph{content} plus
wenzelm@10966
    22
  \emph{attributes}.  The content of a plain file is plain text.  The
wenzelm@10966
    23
  content of a directory is a mapping from names to further
wenzelm@10966
    24
  files.\footnote{In fact, this is the only way that names get
wenzelm@10966
    25
  associated with files.  In Unix files do \emph{not} have a name in
wenzelm@10966
    26
  itself.  Even more, any number of names may be associated with the
wenzelm@10966
    27
  very same file due to \emph{hard links} (although this is excluded
wenzelm@10966
    28
  from our model).}  Attributes include information to control various
wenzelm@10966
    29
  ways to access the file (read, write etc.).
wenzelm@10966
    30
wenzelm@10966
    31
  Our model will be quite liberal in omitting excessive detail that is
wenzelm@10966
    32
  easily seen to be ``irrelevant'' for the aspects of Unix
wenzelm@10966
    33
  file-systems to be discussed here.  First of all, we ignore
wenzelm@10966
    34
  character and block special files, pipes, sockets, hard links,
wenzelm@10966
    35
  symbolic links, and mount points.
wenzelm@10966
    36
*}
wenzelm@10966
    37
wenzelm@10966
    38
wenzelm@10966
    39
subsection {* Names *}
wenzelm@10966
    40
wenzelm@10966
    41
text {*
wenzelm@10966
    42
  User ids and file name components shall be represented by natural
wenzelm@10966
    43
  numbers (without loss of generality).  We do not bother about
wenzelm@10966
    44
  encoding of actual names (e.g.\ strings), nor a mapping between user
wenzelm@10966
    45
  names and user ids as would be present in a reality.
wenzelm@10966
    46
*}
wenzelm@10966
    47
wenzelm@10966
    48
types
wenzelm@10966
    49
  uid = nat
wenzelm@10966
    50
  name = nat
wenzelm@10966
    51
  path = "name list"
wenzelm@10966
    52
wenzelm@10966
    53
wenzelm@10966
    54
subsection {* Attributes *}
wenzelm@10966
    55
wenzelm@10966
    56
text {*
wenzelm@10966
    57
  Unix file attributes mainly consist of \emph{owner} information and
wenzelm@10966
    58
  a number of \emph{permission} bits which control access for
wenzelm@10966
    59
  ``user'', ``group'', and ``others'' (see the Unix man pages @{text
wenzelm@10966
    60
  "chmod(2)"} and @{text "stat(2)"} for more details).
wenzelm@10966
    61
wenzelm@10966
    62
  \medskip Our model of file permissions only considers the ``others''
wenzelm@10966
    63
  part.  The ``user'' field may be omitted without loss of overall
wenzelm@10966
    64
  generality, since the owner is usually able to change it anyway by
wenzelm@10966
    65
  performing @{text chmod}.\footnote{The inclined Unix expert may try
wenzelm@10966
    66
  to figure out some exotic arrangements of a real-world Unix
wenzelm@10966
    67
  file-system such that the owner of a file is unable to apply the
wenzelm@10966
    68
  @{text chmod} system call.}  We omit ``group'' permissions as a
wenzelm@10966
    69
  genuine simplification as we just do not intend to discuss a model
wenzelm@10966
    70
  of multiple groups and group membership, but pretend that everyone
wenzelm@10966
    71
  is member of a single global group.\footnote{A general HOL model of
wenzelm@10966
    72
  user group structures and related issues is given in
wenzelm@10966
    73
  \cite{Naraschewski:2001}.}
wenzelm@10966
    74
*}
wenzelm@10966
    75
wenzelm@10966
    76
datatype perm =
wenzelm@10966
    77
    Readable
wenzelm@10966
    78
  | Writable
wenzelm@10966
    79
  | Executable    -- "(ignored)"
wenzelm@10966
    80
wenzelm@10966
    81
types perms = "perm set"
wenzelm@10966
    82
wenzelm@10966
    83
record att =
wenzelm@10966
    84
  owner :: uid
wenzelm@10966
    85
  others :: perms
wenzelm@10966
    86
wenzelm@10966
    87
text {*
wenzelm@10966
    88
  For plain files @{term Readable} and @{term Writable} specify read
wenzelm@10966
    89
  and write access to the actual content, i.e.\ the string of text
wenzelm@10966
    90
  stored here.  For directories @{term Readable} determines if the set
wenzelm@10966
    91
  of entry names may be accessed, and @{term Writable} controls the
wenzelm@10966
    92
  ability to create or delete any entries (both plain files or
wenzelm@10966
    93
  sub-directories).
wenzelm@10966
    94
wenzelm@10966
    95
  As another simplification, we ignore the @{term Executable}
wenzelm@10966
    96
  permission altogether.  In reality it would indicate executable
wenzelm@10966
    97
  plain files (also known as ``binaries''), or control actual lookup
wenzelm@10966
    98
  of directory entries (recall that mere directory browsing is
wenzelm@10966
    99
  controlled via @{term Readable}).  Note that the latter means that
wenzelm@10966
   100
  in order to perform any file-system operation whatsoever, all
wenzelm@10966
   101
  directories encountered on the path would have to grant @{term
wenzelm@10966
   102
  Executable}.  We ignore this detail and pretend that all directories
wenzelm@10966
   103
  give @{term Executable} permission to anybody.
wenzelm@10966
   104
*}
wenzelm@10966
   105
wenzelm@10966
   106
wenzelm@10966
   107
subsection {* Files *}
wenzelm@10966
   108
wenzelm@10966
   109
text {*
wenzelm@10966
   110
  In order to model the general tree structure of a Unix file-system
wenzelm@10966
   111
  we use the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"}
wenzelm@10966
   112
  from the standard library of Isabelle/HOL
wenzelm@13380
   113
  \cite{Bauer-et-al:2002:HOL-Library}.  This type provides
wenzelm@10966
   114
  constructors @{term Val} and @{term Env} as follows:
wenzelm@10966
   115
wenzelm@10966
   116
  \medskip
wenzelm@10966
   117
  {\def\isastyleminor{\isastyle}
wenzelm@10966
   118
  \begin{tabular}{l}
wenzelm@10966
   119
  @{term [source] "Val :: 'a \<Rightarrow> ('a, 'b, 'c) env"} \\
wenzelm@10966
   120
  @{term [source] "Env :: 'b \<Rightarrow> ('c \<Rightarrow> ('a, 'b, 'c) env option) \<Rightarrow> ('a, 'b, 'c) env"} \\
wenzelm@10966
   121
  \end{tabular}}
wenzelm@10966
   122
  \medskip
wenzelm@10966
   123
wenzelm@10966
   124
  Here the parameter @{typ 'a} refers to plain values occurring at
wenzelm@10966
   125
  leaf positions, parameter @{typ 'b} to information kept with inner
wenzelm@10966
   126
  branch nodes, and parameter @{typ 'c} to the branching type of the
wenzelm@10966
   127
  tree structure.  For our purpose we use the type instance with @{typ
wenzelm@10966
   128
  "att \<times> string"} (representing plain files), @{typ att} (for
wenzelm@10966
   129
  attributes of directory nodes), and @{typ name} (for the index type
wenzelm@10966
   130
  of directory nodes).
wenzelm@10966
   131
*}
wenzelm@10966
   132
wenzelm@10966
   133
types
berghofe@17146
   134
  "file" = "(att \<times> string, att, name) env"
wenzelm@10966
   135
wenzelm@10966
   136
text {*
wenzelm@10966
   137
  \medskip The HOL library also provides @{term lookup} and @{term
wenzelm@10966
   138
  update} operations for general tree structures with the subsequent
wenzelm@10966
   139
  primitive recursive characterizations.
wenzelm@10966
   140
wenzelm@10966
   141
  \medskip
wenzelm@10966
   142
  {\def\isastyleminor{\isastyle}
wenzelm@10966
   143
  \begin{tabular}{l}
wenzelm@10966
   144
  @{term [source] "lookup :: ('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"} \\
wenzelm@10966
   145
  @{term [source]
wenzelm@10966
   146
  "update :: 'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"} \\
wenzelm@10966
   147
  \end{tabular}}
wenzelm@10966
   148
wenzelm@10966
   149
  @{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]}
wenzelm@10966
   150
  @{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]}
wenzelm@10966
   151
wenzelm@10966
   152
  Several further properties of these operations are proven in
wenzelm@13380
   153
  \cite{Bauer-et-al:2002:HOL-Library}.  These will be routinely used
wenzelm@10966
   154
  later on without further notice.
wenzelm@10966
   155
berghofe@17146
   156
  \bigskip Apparently, the elements of type @{typ "file"} contain an
wenzelm@10966
   157
  @{typ att} component in either case.  We now define a few auxiliary
wenzelm@10966
   158
  operations to manipulate this field uniformly, following the
wenzelm@10966
   159
  conventions for record types in Isabelle/HOL
wenzelm@10966
   160
  \cite{Nipkow-et-al:2000:HOL}.
wenzelm@10966
   161
*}
wenzelm@10966
   162
wenzelm@10966
   163
constdefs
wenzelm@10966
   164
  attributes :: "file \<Rightarrow> att"
wenzelm@10966
   165
  "attributes file \<equiv>
wenzelm@10966
   166
    (case file of
wenzelm@10966
   167
      Val (att, text) \<Rightarrow> att
wenzelm@10966
   168
    | Env att dir \<Rightarrow> att)"
wenzelm@10966
   169
wenzelm@10966
   170
  attributes_update :: "att \<Rightarrow> file \<Rightarrow> file"
wenzelm@10966
   171
  "attributes_update att file \<equiv>
wenzelm@10966
   172
    (case file of
wenzelm@10966
   173
      Val (att', text) \<Rightarrow> Val (att, text)
wenzelm@10966
   174
    | Env att' dir \<Rightarrow> Env att dir)"
wenzelm@10966
   175
wenzelm@10966
   176
lemma [simp]: "attributes (Val (att, text)) = att"
wenzelm@10966
   177
  by (simp add: attributes_def)
wenzelm@10966
   178
wenzelm@10966
   179
lemma [simp]: "attributes (Env att dir) = att"
wenzelm@10966
   180
  by (simp add: attributes_def)
wenzelm@10966
   181
wenzelm@10966
   182
lemma [simp]: "attributes (file \<lparr>attributes := att\<rparr>) = att"
berghofe@17146
   183
  by (cases "file") (simp_all add: attributes_def attributes_update_def
wenzelm@10966
   184
    split_tupled_all)
wenzelm@10966
   185
wenzelm@10966
   186
lemma [simp]: "(Val (att, text)) \<lparr>attributes := att'\<rparr> = Val (att', text)"
wenzelm@10966
   187
  by (simp add: attributes_update_def)
wenzelm@10966
   188
wenzelm@10966
   189
lemma [simp]: "(Env att dir) \<lparr>attributes := att'\<rparr> = Env att' dir"
wenzelm@10966
   190
  by (simp add: attributes_update_def)
wenzelm@10966
   191
wenzelm@10966
   192
wenzelm@10966
   193
subsection {* Initial file-systems *}
wenzelm@10966
   194
wenzelm@10966
   195
text {*
wenzelm@10966
   196
  Given a set of \emph{known users} a file-system shall be initialized
wenzelm@10966
   197
  by providing an empty home directory for each user, with read-only
wenzelm@10966
   198
  access for everyone else.  (Note that we may directly use the user
wenzelm@10966
   199
  id as home directory name, since both types have been identified.)
wenzelm@10966
   200
  Certainly, the very root directory is owned by the super user (who
wenzelm@10966
   201
  has user id 0).
wenzelm@10966
   202
*}
wenzelm@10966
   203
wenzelm@10966
   204
constdefs
wenzelm@10966
   205
  init :: "uid set \<Rightarrow> file"
wenzelm@10966
   206
  "init users \<equiv>
wenzelm@10966
   207
    Env \<lparr>owner = 0, others = {Readable}\<rparr>
wenzelm@10966
   208
      (\<lambda>u. if u \<in> users then Some (Env \<lparr>owner = u, others = {Readable}\<rparr> empty)
wenzelm@10966
   209
        else None)"
wenzelm@10966
   210
wenzelm@10966
   211
wenzelm@10966
   212
subsection {* Accessing file-systems *}
wenzelm@10966
   213
wenzelm@10966
   214
text {*
wenzelm@10966
   215
  The main internal file-system operation is access of a file by a
wenzelm@10966
   216
  user, requesting a certain set of permissions.  The resulting @{typ
wenzelm@10966
   217
  "file option"} indicates if a file had been present at the
wenzelm@10966
   218
  corresponding @{typ path} and if access was granted according to the
wenzelm@10966
   219
  permissions recorded within the file-system.
wenzelm@10966
   220
wenzelm@10966
   221
  Note that by the rules of Unix file-system security (e.g.\
wenzelm@10966
   222
  \cite{Tanenbaum:1992}) both the super-user and owner may always
wenzelm@10966
   223
  access a file unconditionally (in our simplified model).
wenzelm@10966
   224
*}
wenzelm@10966
   225
wenzelm@10966
   226
constdefs
wenzelm@10966
   227
  access :: "file \<Rightarrow> path \<Rightarrow> uid \<Rightarrow> perms \<Rightarrow> file option"
wenzelm@10966
   228
  "access root path uid perms \<equiv>
wenzelm@10966
   229
    (case lookup root path of
wenzelm@10966
   230
      None \<Rightarrow> None
wenzelm@10966
   231
    | Some file \<Rightarrow>
wenzelm@10966
   232
        if uid = 0
wenzelm@10966
   233
          \<or> uid = owner (attributes file)
wenzelm@10966
   234
          \<or> perms \<subseteq> others (attributes file)
wenzelm@10966
   235
        then Some file
wenzelm@10966
   236
        else None)"
wenzelm@10966
   237
wenzelm@10966
   238
text {*
wenzelm@10966
   239
  \medskip Successful access to a certain file is the main
wenzelm@10966
   240
  prerequisite for system-calls to be applicable (cf.\
wenzelm@10966
   241
  \secref{sec:unix-trans}).  Any modification of the file-system is
wenzelm@10966
   242
  then performed using the basic @{term update} operation.
wenzelm@10966
   243
wenzelm@10966
   244
  \medskip We see that @{term access} is just a wrapper for the basic
wenzelm@10966
   245
  @{term lookup} function, with additional checking of
wenzelm@10966
   246
  attributes. Subsequently we establish a few auxiliary facts that
wenzelm@10966
   247
  stem from the primitive @{term lookup} used within @{term access}.
wenzelm@10966
   248
*}
wenzelm@10966
   249
wenzelm@10966
   250
lemma access_empty_lookup: "access root path uid {} = lookup root path"
wenzelm@10966
   251
  by (simp add: access_def split: option.splits)
wenzelm@10966
   252
wenzelm@10966
   253
lemma access_some_lookup:
wenzelm@10966
   254
  "access root path uid perms = Some file \<Longrightarrow>
wenzelm@10966
   255
    lookup root path = Some file"
wenzelm@10966
   256
  by (simp add: access_def split: option.splits if_splits)
wenzelm@10966
   257
wenzelm@10966
   258
lemma access_update_other: "path' \<parallel> path \<Longrightarrow>
wenzelm@10966
   259
  access (update path' opt root) path uid perms = access root path uid perms"
wenzelm@10966
   260
proof -
wenzelm@10966
   261
  assume "path' \<parallel> path"
wenzelm@10966
   262
  then obtain y z xs ys zs where
wenzelm@11072
   263
      "y \<noteq> z" and "path' = xs @ y # ys" and "path = xs @ z # zs"
wenzelm@10966
   264
    by (blast dest: parallel_decomp)
wenzelm@10966
   265
  hence "lookup (update path' opt root) path = lookup root path"
wenzelm@10966
   266
    by (blast intro: lookup_update_other)
wenzelm@10966
   267
  thus ?thesis by (simp only: access_def)
wenzelm@10966
   268
qed
wenzelm@10966
   269
wenzelm@10966
   270
wenzelm@10966
   271
section {* File-system transitions \label{sec:unix-trans} *}
wenzelm@10966
   272
wenzelm@10966
   273
subsection {* Unix system calls \label{sec:unix-syscall} *}
wenzelm@10966
   274
wenzelm@10966
   275
text {*
wenzelm@10966
   276
  According to established operating system design (cf.\
wenzelm@10966
   277
  \cite{Tanenbaum:1992}) user space processes may only initiate system
wenzelm@10966
   278
  operations by a fixed set of \emph{system-calls}.  This enables the
wenzelm@10966
   279
  kernel to enforce certain security policies in the first
wenzelm@10966
   280
  place.\footnote{Incidently, this is the very same principle employed
wenzelm@10966
   281
  by any ``LCF-style'' theorem proving system according to Milner's
wenzelm@10966
   282
  principle of ``correctness by construction'', such as Isabelle/HOL
wenzelm@10966
   283
  itself.}
wenzelm@10966
   284
wenzelm@10966
   285
  \medskip In our model of Unix we give a fixed datatype @{text
wenzelm@10966
   286
  operation} for the syntax of system-calls, together with an
wenzelm@10966
   287
  inductive definition of file-system state transitions of the form
wenzelm@10966
   288
  @{text "root \<midarrow>x\<rightarrow> root'"} for the operational semantics.
wenzelm@10966
   289
*}
wenzelm@10966
   290
wenzelm@10966
   291
datatype operation =
wenzelm@10966
   292
    Read uid string path
wenzelm@10966
   293
  | Write uid string path
wenzelm@10966
   294
  | Chmod uid perms path
wenzelm@10966
   295
  | Creat uid perms path
wenzelm@10966
   296
  | Unlink uid path
wenzelm@10966
   297
  | Mkdir uid perms path
wenzelm@10966
   298
  | Rmdir uid path
wenzelm@10966
   299
  | Readdir uid "name set" path
wenzelm@10966
   300
wenzelm@10966
   301
text {*
wenzelm@10966
   302
  The @{typ uid} field of an operation corresponds to the
wenzelm@10966
   303
  \emph{effective user id} of the underlying process, although our
wenzelm@10966
   304
  model never mentions processes explicitly.  The other parameters are
wenzelm@10966
   305
  provided as arguments by the caller; the @{term path} one is common
wenzelm@10966
   306
  to all kinds of system-calls.
wenzelm@10966
   307
*}
wenzelm@10966
   308
wenzelm@10966
   309
consts
wenzelm@10966
   310
  uid_of :: "operation \<Rightarrow> uid"
wenzelm@10966
   311
primrec
wenzelm@10966
   312
  "uid_of (Read uid text path) = uid"
wenzelm@10966
   313
  "uid_of (Write uid text path) = uid"
wenzelm@10966
   314
  "uid_of (Chmod uid perms path) = uid"
wenzelm@10966
   315
  "uid_of (Creat uid perms path) = uid"
wenzelm@10966
   316
  "uid_of (Unlink uid path) = uid"
wenzelm@10966
   317
  "uid_of (Mkdir uid path perms) = uid"
wenzelm@10966
   318
  "uid_of (Rmdir uid path) = uid"
wenzelm@10966
   319
  "uid_of (Readdir uid names path) = uid"
wenzelm@10966
   320
wenzelm@10966
   321
consts
wenzelm@10966
   322
  path_of :: "operation \<Rightarrow> path"
wenzelm@10966
   323
primrec
wenzelm@10966
   324
  "path_of (Read uid text path) = path"
wenzelm@10966
   325
  "path_of (Write uid text path) = path"
wenzelm@10966
   326
  "path_of (Chmod uid perms path) = path"
wenzelm@10966
   327
  "path_of (Creat uid perms path) = path"
wenzelm@10966
   328
  "path_of (Unlink uid path) = path"
wenzelm@10966
   329
  "path_of (Mkdir uid perms path) = path"
wenzelm@10966
   330
  "path_of (Rmdir uid path) = path"
wenzelm@10966
   331
  "path_of (Readdir uid names path) = path"
wenzelm@10966
   332
wenzelm@10966
   333
text {*
wenzelm@10966
   334
  \medskip Note that we have omitted explicit @{text Open} and @{text
wenzelm@10966
   335
  Close} operations, pretending that @{term Read} and @{term Write}
wenzelm@10966
   336
  would already take care of this behind the scenes.  Thus we have
wenzelm@10966
   337
  basically treated actual sequences of real system-calls @{text
wenzelm@13380
   338
  "open"}--@{text read}/@{text write}--@{text close} as atomic.
wenzelm@10966
   339
wenzelm@10966
   340
  In principle, this could make big a difference in a model with
wenzelm@10966
   341
  explicit concurrent processes.  On the other hand, even on a real
wenzelm@13380
   342
  Unix system the exact scheduling of concurrent @{text "open"} and
wenzelm@10966
   343
  @{text close} operations does \emph{not} directly affect the success
wenzelm@10966
   344
  of corresponding @{text read} or @{text write}.  Unix allows several
wenzelm@10966
   345
  processes to have files opened at the same time, even for writing!
wenzelm@10966
   346
  Certainly, the result from reading the contents later may be hard to
wenzelm@10966
   347
  predict, but the system-calls involved here will succeed in any
wenzelm@10966
   348
  case.
wenzelm@10966
   349
wenzelm@10966
   350
  \bigskip The operational semantics of system calls is now specified
wenzelm@10966
   351
  via transitions of the file-system configuration.  This is expressed
wenzelm@10966
   352
  as an inductive relation (although there is no actual recursion
wenzelm@10966
   353
  involved here).
wenzelm@10966
   354
*}
wenzelm@10966
   355
wenzelm@10966
   356
consts
wenzelm@10966
   357
  transition :: "(file \<times> operation \<times> file) set"
wenzelm@10966
   358
wenzelm@10966
   359
syntax
wenzelm@10966
   360
  "_transition" :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool"
wenzelm@10966
   361
  ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100)
wenzelm@10966
   362
translations
wenzelm@10966
   363
  "root \<midarrow>x\<rightarrow> root'" \<rightleftharpoons> "(root, x, root') \<in> transition"
wenzelm@10966
   364
wenzelm@10966
   365
inductive transition
wenzelm@10966
   366
  intros
wenzelm@10966
   367
wenzelm@10966
   368
  read:
wenzelm@10966
   369
    "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow>
wenzelm@10966
   370
      root \<midarrow>(Read uid text path)\<rightarrow> root"
wenzelm@10966
   371
  write:
wenzelm@10966
   372
    "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow>
wenzelm@10966
   373
      root \<midarrow>(Write uid text path)\<rightarrow> update path (Some (Val (att, text))) root"
wenzelm@10966
   374
wenzelm@10966
   375
  chmod:
wenzelm@10966
   376
    "access root path uid {} = Some file \<Longrightarrow>
wenzelm@10966
   377
      uid = 0 \<or> uid = owner (attributes file) \<Longrightarrow>
wenzelm@10966
   378
      root \<midarrow>(Chmod uid perms path)\<rightarrow> update path
wenzelm@10966
   379
        (Some (file \<lparr>attributes := attributes file \<lparr>others := perms\<rparr>\<rparr>)) root"
wenzelm@10966
   380
wenzelm@10966
   381
  creat:
wenzelm@10966
   382
    "path = parent_path @ [name] \<Longrightarrow>
wenzelm@10966
   383
      access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
wenzelm@10966
   384
      access root path uid {} = None \<Longrightarrow>
wenzelm@10966
   385
      root \<midarrow>(Creat uid perms path)\<rightarrow> update path
wenzelm@10966
   386
        (Some (Val (\<lparr>owner = uid, others = perms\<rparr>, []))) root"
wenzelm@10966
   387
  unlink:
wenzelm@10966
   388
    "path = parent_path @ [name] \<Longrightarrow>
wenzelm@10966
   389
      access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
wenzelm@10966
   390
      access root path uid {} = Some (Val plain) \<Longrightarrow>
wenzelm@10966
   391
      root \<midarrow>(Unlink uid path)\<rightarrow> update path None root"
wenzelm@10966
   392
wenzelm@10966
   393
  mkdir:
wenzelm@10966
   394
    "path = parent_path @ [name] \<Longrightarrow>
wenzelm@10966
   395
      access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
wenzelm@10966
   396
      access root path uid {} = None \<Longrightarrow>
wenzelm@10966
   397
      root \<midarrow>(Mkdir uid perms path)\<rightarrow> update path
wenzelm@10966
   398
        (Some (Env \<lparr>owner = uid, others = perms\<rparr> empty)) root"
wenzelm@10966
   399
  rmdir:
wenzelm@10966
   400
    "path = parent_path @ [name] \<Longrightarrow>
wenzelm@10966
   401
      access root parent_path uid {Writable} = Some (Env att parent) \<Longrightarrow>
wenzelm@10966
   402
      access root path uid {} = Some (Env att' empty) \<Longrightarrow>
wenzelm@10966
   403
      root \<midarrow>(Rmdir uid path)\<rightarrow> update path None root"
wenzelm@10966
   404
wenzelm@10966
   405
  readdir:
wenzelm@10966
   406
    "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow>
wenzelm@10966
   407
      names = dom dir \<Longrightarrow>
wenzelm@10966
   408
      root \<midarrow>(Readdir uid names path)\<rightarrow> root"
wenzelm@10966
   409
wenzelm@10966
   410
text {*
wenzelm@10966
   411
  \medskip Certainly, the above specification is central to the whole
wenzelm@10966
   412
  formal development.  Any of the results to be established later on
wenzelm@10966
   413
  are only meaningful to the outside world if this transition system
wenzelm@10966
   414
  provides an adequate model of real Unix systems.  This kind of
wenzelm@10966
   415
  ``reality-check'' of a formal model is the well-known problem of
wenzelm@10966
   416
  \emph{validation}.
wenzelm@10966
   417
wenzelm@10966
   418
  If in doubt, one may consider to compare our definition with the
wenzelm@10966
   419
  informal specifications given the corresponding Unix man pages, or
wenzelm@10966
   420
  even peek at an actual implementation such as
wenzelm@10966
   421
  \cite{Torvalds-et-al:Linux}.  Another common way to gain confidence
wenzelm@10966
   422
  into the formal model is to run simple simulations (see
wenzelm@10966
   423
  \secref{sec:unix-examples}), and check the results with that of
wenzelm@10966
   424
  experiments performed on a real Unix system.
wenzelm@10966
   425
*}
wenzelm@10966
   426
wenzelm@10966
   427
wenzelm@10966
   428
subsection {* Basic properties of single transitions \label{sec:unix-single-trans} *}
wenzelm@10966
   429
wenzelm@10966
   430
text {*
wenzelm@10966
   431
  The transition system @{text "root \<midarrow>x\<rightarrow> root'"} defined above
wenzelm@10966
   432
  determines a unique result @{term root'} from given @{term root} and
wenzelm@10966
   433
  @{term x} (this is holds rather trivially, since there is even only
wenzelm@10966
   434
  one clause for each operation).  This uniqueness statement will
wenzelm@10966
   435
  simplify our subsequent development to some extent, since we only
wenzelm@10966
   436
  have to reason about a partial function rather than a general
wenzelm@10966
   437
  relation.
wenzelm@10966
   438
*}
wenzelm@10966
   439
wenzelm@10966
   440
theorem transition_uniq: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root \<midarrow>x\<rightarrow> root'' \<Longrightarrow> root' = root''"
wenzelm@10966
   441
proof -
wenzelm@10966
   442
  assume root: "root \<midarrow>x\<rightarrow> root'"
wenzelm@10966
   443
  assume "root \<midarrow>x\<rightarrow> root''"
wenzelm@10966
   444
  thus "root' = root''"
wenzelm@10966
   445
  proof cases
wenzelm@10966
   446
    case read
wenzelm@10966
   447
    with root show ?thesis by cases auto
wenzelm@10966
   448
  next
wenzelm@10966
   449
    case write
wenzelm@10966
   450
    with root show ?thesis by cases auto
wenzelm@10966
   451
  next
wenzelm@10966
   452
    case chmod
wenzelm@10966
   453
    with root show ?thesis by cases auto
wenzelm@10966
   454
  next
wenzelm@10966
   455
    case creat
wenzelm@10966
   456
    with root show ?thesis by cases auto
wenzelm@10966
   457
  next
wenzelm@10966
   458
    case unlink
wenzelm@10966
   459
    with root show ?thesis by cases auto
wenzelm@10966
   460
  next
wenzelm@10966
   461
    case mkdir
wenzelm@10966
   462
    with root show ?thesis by cases auto
wenzelm@10966
   463
  next
wenzelm@10966
   464
    case rmdir
wenzelm@10966
   465
    with root show ?thesis by cases auto
wenzelm@10966
   466
  next
wenzelm@10966
   467
    case readdir
wenzelm@17455
   468
    with root show ?thesis by cases fastsimp+
wenzelm@10966
   469
  qed
wenzelm@10966
   470
qed
wenzelm@10966
   471
wenzelm@10966
   472
text {*
wenzelm@10966
   473
  \medskip Apparently, file-system transitions are \emph{type-safe} in
wenzelm@10966
   474
  the sense that the result of transforming an actual directory yields
wenzelm@10966
   475
  again a directory.
wenzelm@10966
   476
*}
wenzelm@10966
   477
wenzelm@10966
   478
theorem transition_type_safe:
wenzelm@10966
   479
  "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> \<exists>att dir. root = Env att dir
wenzelm@10966
   480
    \<Longrightarrow> \<exists>att dir. root' = Env att dir"
wenzelm@10966
   481
proof -
wenzelm@10966
   482
  assume tr: "root \<midarrow>x\<rightarrow> root'"
wenzelm@10966
   483
  assume inv: "\<exists>att dir. root = Env att dir"
wenzelm@10966
   484
  show ?thesis
wenzelm@10966
   485
  proof (cases "path_of x")
wenzelm@10966
   486
    case Nil
wenzelm@10966
   487
    with tr inv show ?thesis
wenzelm@10966
   488
      by cases (auto simp add: access_def split: if_splits)
wenzelm@10966
   489
  next
wenzelm@10966
   490
    case Cons
wenzelm@10966
   491
    from tr obtain opt where
wenzelm@10966
   492
        "root' = root \<or> root' = update (path_of x) opt root"
wenzelm@10966
   493
      by cases auto
wenzelm@10966
   494
    with inv Cons show ?thesis
wenzelm@10966
   495
      by (auto simp add: update_eq split: list.splits)
wenzelm@10966
   496
  qed
wenzelm@10966
   497
qed
wenzelm@10966
   498
wenzelm@10966
   499
text {*
wenzelm@10966
   500
  The previous result may be seen as the most basic invariant on the
wenzelm@10966
   501
  file-system state that is enforced by any proper kernel
wenzelm@10966
   502
  implementation.  So user processes --- being bound to the
wenzelm@10966
   503
  system-call interface --- may never mess up a file-system such that
wenzelm@10966
   504
  the root becomes a plain file instead of a directory, which would be
wenzelm@10966
   505
  a strange situation indeed.
wenzelm@10966
   506
*}
wenzelm@10966
   507
wenzelm@10966
   508
wenzelm@10966
   509
subsection {* Iterated transitions *}
wenzelm@10966
   510
wenzelm@10966
   511
text {*
wenzelm@10966
   512
  Iterated system transitions via finite sequences of system
wenzelm@10966
   513
  operations are modeled inductively as follows.  In a sense, this
wenzelm@10966
   514
  relation describes the cumulative effect of the sequence of
wenzelm@10966
   515
  system-calls issued by a number of running processes over a finite
wenzelm@10966
   516
  amount of time.
wenzelm@10966
   517
*}
wenzelm@10966
   518
wenzelm@10966
   519
consts
wenzelm@10966
   520
  transitions :: "(file \<times> operation list \<times> file) set"
wenzelm@10966
   521
wenzelm@10966
   522
syntax
wenzelm@10966
   523
  "_transitions" :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool"
wenzelm@10966
   524
  ("_ =_\<Rightarrow> _" [90, 1000, 90] 100)
wenzelm@10966
   525
translations
wenzelm@10966
   526
  "root =xs\<Rightarrow> root'" \<rightleftharpoons> "(root, xs, root') \<in> transitions"
wenzelm@10966
   527
wenzelm@10966
   528
inductive transitions
wenzelm@10966
   529
  intros
wenzelm@10966
   530
    nil: "root =[]\<Rightarrow> root"
wenzelm@10966
   531
    cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''"
wenzelm@10966
   532
wenzelm@10966
   533
text {*
wenzelm@10966
   534
  \medskip We establish a few basic facts relating iterated
wenzelm@10966
   535
  transitions with single ones, according to the recursive structure
wenzelm@10966
   536
  of lists.
wenzelm@10966
   537
*}
wenzelm@10966
   538
wenzelm@10966
   539
lemma transitions_nil_eq: "root =[]\<Rightarrow> root' = (root = root')"
wenzelm@10966
   540
proof
wenzelm@10966
   541
  assume "root =[]\<Rightarrow> root'"
wenzelm@10966
   542
  thus "root = root'" by cases simp_all
wenzelm@10966
   543
next
wenzelm@10966
   544
  assume "root = root'"
wenzelm@10966
   545
  thus "root =[]\<Rightarrow> root'" by (simp only: transitions.nil)
wenzelm@10966
   546
qed
wenzelm@10966
   547
wenzelm@10966
   548
lemma transitions_cons_eq:
wenzelm@10966
   549
  "root =(x # xs)\<Rightarrow> root'' = (\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root'')"
wenzelm@10966
   550
proof
wenzelm@10966
   551
  assume "root =(x # xs)\<Rightarrow> root''"
wenzelm@10966
   552
  thus "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
wenzelm@10966
   553
    by cases auto
wenzelm@10966
   554
next
wenzelm@10966
   555
  assume "\<exists>root'. root \<midarrow>x\<rightarrow> root' \<and> root' =xs\<Rightarrow> root''"
wenzelm@10966
   556
  thus "root =(x # xs)\<Rightarrow> root''"
wenzelm@10966
   557
    by (blast intro: transitions.cons)
wenzelm@10966
   558
qed
wenzelm@10966
   559
wenzelm@10966
   560
text {*
wenzelm@10966
   561
  The next two rules show how to ``destruct'' known transition
wenzelm@10966
   562
  sequences.  Note that the second one actually relies on the
wenzelm@10966
   563
  uniqueness property of the basic transition system (see
wenzelm@10966
   564
  \secref{sec:unix-single-trans}).
wenzelm@10966
   565
*}
wenzelm@10966
   566
wenzelm@10966
   567
lemma transitions_nilD: "root =[]\<Rightarrow> root' \<Longrightarrow> root' = root"
wenzelm@10966
   568
  by (simp add: transitions_nil_eq)
wenzelm@10966
   569
wenzelm@10966
   570
lemma transitions_consD:
wenzelm@10966
   571
  "root =(x # xs)\<Rightarrow> root'' \<Longrightarrow> root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root''"
wenzelm@10966
   572
proof -
wenzelm@10966
   573
  assume "root =(x # xs)\<Rightarrow> root''"
wenzelm@10966
   574
  then obtain r' where r': "root \<midarrow>x\<rightarrow> r'" and root'': "r' =xs\<Rightarrow> root''"
wenzelm@10966
   575
    by cases simp_all
wenzelm@10966
   576
  assume "root \<midarrow>x\<rightarrow> root'"
wenzelm@10966
   577
  with r' have "r' = root'" by (rule transition_uniq)
wenzelm@10966
   578
  with root'' show "root' =xs\<Rightarrow> root''" by simp
wenzelm@10966
   579
qed
wenzelm@10966
   580
wenzelm@10966
   581
text {*
wenzelm@10966
   582
  \medskip The following fact shows how an invariant @{term Q} of
wenzelm@10966
   583
  single transitions with property @{term P} may be transferred to
wenzelm@10966
   584
  iterated transitions.  The proof is rather obvious by rule induction
wenzelm@10966
   585
  over the definition of @{term "root =xs\<Rightarrow> root'"}.
wenzelm@10966
   586
*}
wenzelm@10966
   587
wenzelm@10966
   588
lemma transitions_invariant:
wenzelm@10966
   589
  "(\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r') \<Longrightarrow>
wenzelm@10966
   590
    root =xs\<Rightarrow> root' \<Longrightarrow> Q root \<Longrightarrow> \<forall>x \<in> set xs. P x \<Longrightarrow> Q root'"
wenzelm@10966
   591
proof -
wenzelm@10966
   592
  assume r: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r'"
wenzelm@10966
   593
  assume "root =xs\<Rightarrow> root'"
wenzelm@10966
   594
  thus "Q root \<Longrightarrow> (\<forall>x \<in> set xs. P x) \<Longrightarrow> Q root'" (is "PROP ?P root xs root'")
wenzelm@11809
   595
  proof (induct root xs root')
wenzelm@10966
   596
    fix root assume "Q root"
wenzelm@10966
   597
    thus "Q root" .
wenzelm@10966
   598
  next
wenzelm@10966
   599
    fix root root' root'' and x xs
wenzelm@10966
   600
    assume root': "root \<midarrow>x\<rightarrow> root'"
wenzelm@10966
   601
    assume hyp: "PROP ?P root' xs root''"
wenzelm@10966
   602
    assume Q: "Q root"
wenzelm@10966
   603
    assume P: "\<forall>x \<in> set (x # xs). P x"
wenzelm@10966
   604
    hence "P x" by simp
wenzelm@10966
   605
    with root' Q have Q': "Q root'" by (rule r)
wenzelm@10966
   606
    from P have "\<forall>x \<in> set xs. P x" by simp
wenzelm@10966
   607
    with Q' show "Q root''" by (rule hyp)
wenzelm@10966
   608
  qed
wenzelm@10966
   609
qed
wenzelm@10966
   610
wenzelm@10966
   611
text {*
wenzelm@10966
   612
  As an example of applying the previous result, we transfer the basic
wenzelm@10966
   613
  type-safety property (see \secref{sec:unix-single-trans}) from
wenzelm@10966
   614
  single transitions to iterated ones, which is a rather obvious
wenzelm@10966
   615
  result indeed.
wenzelm@10966
   616
*}
wenzelm@10966
   617
wenzelm@10966
   618
theorem transitions_type_safe:
wenzelm@16670
   619
  assumes "root =xs\<Rightarrow> root'"
wenzelm@16670
   620
    and "\<exists>att dir. root = Env att dir"
wenzelm@16670
   621
  shows "\<exists>att dir. root' = Env att dir"
wenzelm@16670
   622
  using transition_type_safe and prems
wenzelm@16670
   623
proof (rule transitions_invariant)
wenzelm@16670
   624
  show "\<forall>x \<in> set xs. True" by blast
wenzelm@10966
   625
qed
wenzelm@10966
   626
wenzelm@10966
   627
wenzelm@10966
   628
section {* Executable sequences *}
wenzelm@10966
   629
wenzelm@10966
   630
text {*
wenzelm@17455
   631
  An inductively defined relation such as the one of @{text "root \<midarrow>x\<rightarrow>
wenzelm@17455
   632
  root'"} (see \secref{sec:unix-syscall}) has two main aspects.  First
wenzelm@17455
   633
  of all, the resulting system admits a certain set of transition
wenzelm@17455
   634
  rules (introductions) as given in the specification.  Furthermore,
wenzelm@17455
   635
  there is an explicit least-fixed-point construction involved, which
wenzelm@17455
   636
  results in induction (and case-analysis) rules to eliminate known
wenzelm@17455
   637
  transitions in an exhaustive manner.
wenzelm@10966
   638
wenzelm@10966
   639
  \medskip Subsequently, we explore our transition system in an
wenzelm@10966
   640
  experimental style, mainly using the introduction rules with basic
wenzelm@10966
   641
  algebraic properties of the underlying structures.  The technique
wenzelm@10966
   642
  closely resembles that of Prolog combined with functional evaluation
wenzelm@10966
   643
  in a very simple manner.
wenzelm@10966
   644
wenzelm@10966
   645
  Just as the ``closed-world assumption'' is left implicit in Prolog,
wenzelm@10966
   646
  we do not refer to induction over the whole transition system here.
wenzelm@10966
   647
  So this is still purely positive reasoning about possible
wenzelm@10966
   648
  executions; exhaustive reasoning will be employed only later on (see
wenzelm@10966
   649
  \secref{sec:unix-bogosity}), when we shall demonstrate that certain
wenzelm@10966
   650
  behavior is \emph{not} possible.
wenzelm@10966
   651
*}
wenzelm@10966
   652
wenzelm@10966
   653
wenzelm@10966
   654
subsection {* Possible transitions *}
wenzelm@10966
   655
wenzelm@10966
   656
text {*
wenzelm@10966
   657
  Rather obviously, a list of system operations can be executed within
wenzelm@10966
   658
  a certain state if there is a result state reached by an iterated
wenzelm@10966
   659
  transition.
wenzelm@10966
   660
*}
wenzelm@10966
   661
wenzelm@10966
   662
constdefs
wenzelm@10966
   663
  can_exec :: "file \<Rightarrow> operation list \<Rightarrow> bool"
wenzelm@10966
   664
  "can_exec root xs \<equiv> \<exists>root'. root =xs\<Rightarrow> root'"
wenzelm@10966
   665
wenzelm@10966
   666
lemma can_exec_nil: "can_exec root []"
wenzelm@10966
   667
  by (unfold can_exec_def) (blast intro: transitions.intros)
wenzelm@10966
   668
wenzelm@10966
   669
lemma can_exec_cons:
wenzelm@10966
   670
    "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> can_exec root' xs \<Longrightarrow> can_exec root (x # xs)"
wenzelm@10966
   671
  by (unfold can_exec_def) (blast intro: transitions.intros)
wenzelm@10966
   672
wenzelm@10966
   673
text {*
wenzelm@10966
   674
  \medskip In case that we already know that a certain sequence can be
wenzelm@10966
   675
  executed we may destruct it backwardly into individual transitions.
wenzelm@10966
   676
*}
wenzelm@10966
   677
wenzelm@10966
   678
lemma can_exec_snocD: "\<And>root. can_exec root (xs @ [y])
wenzelm@10966
   679
    \<Longrightarrow> \<exists>root' root''. root =xs\<Rightarrow> root' \<and> root' \<midarrow>y\<rightarrow> root''"
wenzelm@10966
   680
  (is "PROP ?P xs" is "\<And>root. ?A root xs \<Longrightarrow> ?C root xs")
wenzelm@10966
   681
proof (induct xs)
wenzelm@10966
   682
  fix root
wenzelm@10966
   683
  {
wenzelm@10966
   684
    assume "?A root []"
wenzelm@10966
   685
    thus "?C root []"
wenzelm@10966
   686
      by (simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
wenzelm@10966
   687
  next
wenzelm@10966
   688
    fix x xs
wenzelm@10966
   689
    assume hyp: "PROP ?P xs"
wenzelm@10966
   690
    assume asm: "?A root (x # xs)"
wenzelm@10966
   691
    show "?C root (x # xs)"
wenzelm@10966
   692
    proof -
wenzelm@10966
   693
      from asm obtain r root'' where x: "root \<midarrow>x\<rightarrow> r" and
wenzelm@10966
   694
          xs_y: "r =(xs @ [y])\<Rightarrow> root''"
wenzelm@10966
   695
        by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq)
wenzelm@10966
   696
      from xs_y hyp obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'"
wenzelm@11758
   697
        by (unfold can_exec_def) blast
wenzelm@10966
   698
      from x xs have "root =(x # xs)\<Rightarrow> root'"
wenzelm@10966
   699
        by (rule transitions.cons)
wenzelm@10966
   700
      with y show ?thesis by blast
wenzelm@10966
   701
    qed
wenzelm@10966
   702
  }
wenzelm@10966
   703
qed
wenzelm@10966
   704
wenzelm@10966
   705
wenzelm@10966
   706
subsection {* Example executions \label{sec:unix-examples} *}
wenzelm@10966
   707
wenzelm@10966
   708
text {*
wenzelm@10966
   709
  We are now ready to perform a few experiments within our formal
wenzelm@10966
   710
  model of Unix system-calls.  The common technique is to alternate
wenzelm@10966
   711
  introduction rules of the transition system (see
wenzelm@10966
   712
  \secref{sec:unix-trans}), and steps to solve any emerging side
wenzelm@10966
   713
  conditions using algebraic properties of the underlying file-system
wenzelm@10966
   714
  structures (see \secref{sec:unix-file-system}).
wenzelm@10966
   715
*}
wenzelm@10966
   716
wenzelm@10966
   717
lemmas eval = access_def init_def
wenzelm@10966
   718
wenzelm@10966
   719
theorem "u \<in> users \<Longrightarrow> can_exec (init users)
wenzelm@10966
   720
    [Mkdir u perms [u, name]]"
wenzelm@10966
   721
  apply (rule can_exec_cons)
wenzelm@10966
   722
    -- {* back-chain @{term can_exec} (of @{term [source] Cons}) *}
wenzelm@10966
   723
  apply (rule mkdir)
wenzelm@10966
   724
    -- {* back-chain @{term Mkdir} *}
wenzelm@10966
   725
  apply (force simp add: eval)+
wenzelm@10966
   726
    -- {* solve preconditions of @{term Mkdir} *}
wenzelm@10966
   727
  apply (simp add: eval)
wenzelm@10966
   728
    -- {* peek at resulting dir (optional) *}
wenzelm@10966
   729
  txt {* @{subgoals [display]} *}
wenzelm@10966
   730
  apply (rule can_exec_nil)
wenzelm@10966
   731
    -- {* back-chain @{term can_exec} (of @{term [source] Nil}) *}
wenzelm@10966
   732
  done
wenzelm@10966
   733
wenzelm@10966
   734
text {*
wenzelm@10966
   735
  By inspecting the result shown just before the final step above, we
wenzelm@10966
   736
  may gain confidence that our specification of Unix system-calls
wenzelm@10966
   737
  actually makes sense.  Further common errors are usually exhibited
wenzelm@10966
   738
  when preconditions of transition rules fail unexpectedly.
wenzelm@10966
   739
wenzelm@10966
   740
  \medskip Here are a few further experiments, using the same
wenzelm@10966
   741
  techniques as before.
wenzelm@10966
   742
*}
wenzelm@10966
   743
wenzelm@10966
   744
theorem "u \<in> users \<Longrightarrow> can_exec (init users)
wenzelm@10966
   745
   [Creat u perms [u, name],
wenzelm@10966
   746
    Unlink u [u, name]]"
wenzelm@10966
   747
  apply (rule can_exec_cons)
wenzelm@10966
   748
  apply (rule creat)
wenzelm@10966
   749
  apply (force simp add: eval)+
wenzelm@10966
   750
  apply (simp add: eval)
wenzelm@10966
   751
  apply (rule can_exec_cons)
wenzelm@10966
   752
  apply (rule unlink)
wenzelm@10966
   753
  apply (force simp add: eval)+
wenzelm@10966
   754
  apply (simp add: eval)
wenzelm@10966
   755
  txt {* peek at result: @{subgoals [display]} *}
wenzelm@10966
   756
  apply (rule can_exec_nil)
wenzelm@10966
   757
  done
wenzelm@10966
   758
wenzelm@17455
   759
theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow>
wenzelm@17455
   760
  Readable \<in> perms\<^isub>2 \<Longrightarrow> name\<^isub>3 \<noteq> name\<^isub>4 \<Longrightarrow>
wenzelm@10966
   761
  can_exec (init users)
wenzelm@17455
   762
   [Mkdir u perms\<^isub>1 [u, name\<^isub>1],
wenzelm@17455
   763
    Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2],
wenzelm@17455
   764
    Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
wenzelm@17455
   765
    Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>4],
wenzelm@17455
   766
    Readdir u {name\<^isub>3, name\<^isub>4} [u, name\<^isub>1, name\<^isub>2]]"
wenzelm@10966
   767
  apply (rule can_exec_cons, rule transition.intros,
wenzelm@10966
   768
    (force simp add: eval)+, (simp add: eval)?)+
wenzelm@10966
   769
  txt {* peek at result: @{subgoals [display]} *}
wenzelm@10966
   770
  apply (rule can_exec_nil)
wenzelm@10966
   771
  done
wenzelm@10966
   772
wenzelm@17455
   773
theorem "u \<in> users \<Longrightarrow> Writable \<in> perms\<^isub>1 \<Longrightarrow> Readable \<in> perms\<^isub>3 \<Longrightarrow>
wenzelm@10966
   774
  can_exec (init users)
wenzelm@17455
   775
   [Mkdir u perms\<^isub>1 [u, name\<^isub>1],
wenzelm@17455
   776
    Mkdir u' perms\<^isub>2 [u, name\<^isub>1, name\<^isub>2],
wenzelm@17455
   777
    Creat u' perms\<^isub>3 [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
wenzelm@17455
   778
    Write u' ''foo'' [u, name\<^isub>1, name\<^isub>2, name\<^isub>3],
wenzelm@17455
   779
    Read u ''foo'' [u, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
wenzelm@10966
   780
  apply (rule can_exec_cons, rule transition.intros,
wenzelm@10966
   781
    (force simp add: eval)+, (simp add: eval)?)+
wenzelm@10966
   782
  txt {* peek at result: @{subgoals [display]} *}
wenzelm@10966
   783
  apply (rule can_exec_nil)
wenzelm@10966
   784
  done
wenzelm@10966
   785
wenzelm@10966
   786
wenzelm@10966
   787
section {* Odd effects --- treated formally \label{sec:unix-bogosity} *}
wenzelm@10966
   788
wenzelm@10966
   789
text {*
wenzelm@10966
   790
  We are now ready to give a completely formal treatment of the
wenzelm@10966
   791
  slightly odd situation discussed in the introduction (see
wenzelm@10966
   792
  \secref{sec:unix-intro}): the file-system can easily reach a state
wenzelm@10966
   793
  where a user is unable to remove his very own directory, because it
wenzelm@10966
   794
  is still populated by items placed there by another user in an
wenzelm@10966
   795
  uncouth manner.
wenzelm@10966
   796
*}
wenzelm@10966
   797
wenzelm@10966
   798
subsection {* The general procedure \label{sec:unix-inv-procedure} *}
wenzelm@10966
   799
wenzelm@10966
   800
text {*
wenzelm@10966
   801
  The following theorem expresses the general procedure we are
wenzelm@10966
   802
  following to achieve the main result.
wenzelm@10966
   803
*}
wenzelm@10966
   804
wenzelm@10966
   805
theorem general_procedure:
wenzelm@10966
   806
  "(\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False) \<Longrightarrow>
wenzelm@10966
   807
    (\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root) \<Longrightarrow>
wenzelm@10966
   808
    (\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow>  P x \<Longrightarrow> Q r') \<Longrightarrow>
wenzelm@10966
   809
    init users =bs\<Rightarrow> root \<Longrightarrow>
wenzelm@10966
   810
      \<not> (\<exists>xs. (\<forall>x \<in> set xs. P x) \<and> can_exec root (xs @ [y]))"
wenzelm@10966
   811
proof -
wenzelm@10966
   812
  assume cannot_y: "\<And>r r'. Q r \<Longrightarrow> r \<midarrow>y\<rightarrow> r' \<Longrightarrow> False"
wenzelm@10966
   813
  assume init_inv: "\<And>root. init users =bs\<Rightarrow> root \<Longrightarrow> Q root"
wenzelm@10966
   814
  assume preserve_inv: "\<And>r x r'. r \<midarrow>x\<rightarrow> r' \<Longrightarrow> Q r \<Longrightarrow> P x \<Longrightarrow> Q r'"
wenzelm@10966
   815
  assume init_result: "init users =bs\<Rightarrow> root"
wenzelm@10966
   816
  {
wenzelm@10966
   817
    fix xs
wenzelm@10966
   818
    assume Ps: "\<forall>x \<in> set xs. P x"
wenzelm@10966
   819
    assume can_exec: "can_exec root (xs @ [y])"
wenzelm@10966
   820
    then obtain root' root'' where
wenzelm@10966
   821
        xs: "root =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> root''"
wenzelm@10966
   822
      by (blast dest: can_exec_snocD)
wenzelm@10966
   823
    from init_result have "Q root" by (rule init_inv)
wenzelm@10966
   824
    from preserve_inv xs this Ps have "Q root'"
wenzelm@10966
   825
      by (rule transitions_invariant)
wenzelm@10966
   826
    from this y have False by (rule cannot_y)
wenzelm@10966
   827
  }
wenzelm@10966
   828
  thus ?thesis by blast
wenzelm@10966
   829
qed
wenzelm@10966
   830
wenzelm@10966
   831
text {*
wenzelm@10966
   832
  Here @{prop "P x"} refers to the restriction on file-system
wenzelm@10966
   833
  operations that are admitted after having reached the critical
wenzelm@10966
   834
  configuration; according to the problem specification this will
wenzelm@17455
   835
  become @{prop "uid_of x = user\<^isub>1"} later on.  Furthermore,
wenzelm@17455
   836
  @{term y} refers to the operations we claim to be impossible to
wenzelm@17455
   837
  perform afterwards, we will take @{term Rmdir} later.  Moreover
wenzelm@17455
   838
  @{term Q} is a suitable (auxiliary) invariant over the file-system;
wenzelm@17455
   839
  choosing @{term Q} adequately is very important to make the proof
wenzelm@17455
   840
  work (see \secref{sec:unix-inv-lemmas}).
wenzelm@10966
   841
*}
wenzelm@10966
   842
wenzelm@10966
   843
wenzelm@12079
   844
subsection {* The particular situation *}
wenzelm@10966
   845
wenzelm@10966
   846
text {*
wenzelm@10966
   847
  We introduce a few global declarations and axioms to describe our
wenzelm@12079
   848
  particular situation considered here.  Thus we avoid excessive use
wenzelm@12079
   849
  of local parameters in the subsequent development.
wenzelm@10966
   850
*}
wenzelm@10966
   851
wenzelm@12079
   852
locale situation =
wenzelm@12079
   853
  fixes users :: "uid set"
wenzelm@17455
   854
    and user\<^isub>1 :: uid
wenzelm@17455
   855
    and user\<^isub>2 :: uid
wenzelm@17455
   856
    and name\<^isub>1 :: name
wenzelm@17455
   857
    and name\<^isub>2 :: name
wenzelm@17455
   858
    and name\<^isub>3 :: name
wenzelm@17455
   859
    and perms\<^isub>1 :: perms
wenzelm@17455
   860
    and perms\<^isub>2 :: perms
wenzelm@17455
   861
  assumes user\<^isub>1_known: "user\<^isub>1 \<in> users"
wenzelm@17455
   862
    and user\<^isub>1_not_root: "user\<^isub>1 \<noteq> 0"
wenzelm@17455
   863
    and users_neq: "user\<^isub>1 \<noteq> user\<^isub>2"
wenzelm@17455
   864
    and perms\<^isub>1_writable: "Writable \<in> perms\<^isub>1"
wenzelm@17455
   865
    and perms\<^isub>2_not_writable: "Writable \<notin> perms\<^isub>2"
wenzelm@17455
   866
  notes facts = user\<^isub>1_known user\<^isub>1_not_root users_neq
wenzelm@17455
   867
    perms\<^isub>1_writable perms\<^isub>2_not_writable
wenzelm@10966
   868
wenzelm@12079
   869
  fixes bogus :: "operation list"
wenzelm@12079
   870
    and bogus_path :: path
wenzelm@12079
   871
  defines "bogus \<equiv>
wenzelm@17455
   872
     [Mkdir user\<^isub>1 perms\<^isub>1 [user\<^isub>1, name\<^isub>1],
wenzelm@17455
   873
      Mkdir user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2],
wenzelm@17455
   874
      Creat user\<^isub>2 perms\<^isub>2 [user\<^isub>1, name\<^isub>1, name\<^isub>2, name\<^isub>3]]"
wenzelm@17455
   875
    and "bogus_path \<equiv> [user\<^isub>1, name\<^isub>1, name\<^isub>2]"
wenzelm@10966
   876
wenzelm@10966
   877
text {*
wenzelm@12079
   878
  The @{term bogus} operations are the ones that lead into the uncouth
wenzelm@12079
   879
  situation; @{term bogus_path} is the key position within the
wenzelm@12079
   880
  file-system where things go awry.
wenzelm@10966
   881
*}
wenzelm@10966
   882
wenzelm@10966
   883
wenzelm@10966
   884
subsection {* Invariance lemmas \label{sec:unix-inv-lemmas} *}
wenzelm@10966
   885
wenzelm@10966
   886
text {*
wenzelm@10966
   887
  The following invariant over the root file-system describes the
wenzelm@10966
   888
  bogus situation in an abstract manner: located at a certain @{term
wenzelm@10966
   889
  path} within the file-system is a non-empty directory that is
wenzelm@17455
   890
  neither owned and nor writable by @{term user\<^isub>1}.
wenzelm@10966
   891
*}
wenzelm@10966
   892
wenzelm@12079
   893
locale invariant = situation +
wenzelm@12079
   894
  fixes invariant :: "file \<Rightarrow> path \<Rightarrow> bool"
wenzelm@12079
   895
  defines "invariant root path \<equiv>
wenzelm@10966
   896
    (\<exists>att dir.
wenzelm@17455
   897
      access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and>
wenzelm@17455
   898
      user\<^isub>1 \<noteq> owner att \<and>
wenzelm@17455
   899
      access root path user\<^isub>1 {Writable} = None)"
wenzelm@10966
   900
wenzelm@10966
   901
text {*
wenzelm@10966
   902
  Following the general procedure (see
wenzelm@17455
   903
  \secref{sec:unix-inv-procedure}) we will now establish the three key
wenzelm@17455
   904
  lemmas required to yield the final result.
wenzelm@10966
   905
wenzelm@10966
   906
  \begin{enumerate}
wenzelm@10966
   907
wenzelm@10966
   908
  \item The invariant is sufficiently strong to entail the
wenzelm@17455
   909
  pathological case that @{term user\<^isub>1} is unable to remove the
wenzelm@17455
   910
  (owned) directory at @{term "[user\<^isub>1, name\<^isub>1]"}.
wenzelm@10966
   911
wenzelm@10966
   912
  \item The invariant does hold after having executed the @{term
wenzelm@10966
   913
  bogus} list of operations (starting with an initial file-system
wenzelm@10966
   914
  configuration).
wenzelm@10966
   915
wenzelm@10966
   916
  \item The invariant is preserved by any file-system operation
wenzelm@17455
   917
  performed by @{term user\<^isub>1} alone, without any help by other
wenzelm@17455
   918
  users.
wenzelm@10966
   919
wenzelm@10966
   920
  \end{enumerate}
wenzelm@10966
   921
wenzelm@10966
   922
  As the invariant appears both as assumptions and conclusions in the
wenzelm@10966
   923
  course of proof, its formulation is rather critical for the whole
wenzelm@10966
   924
  development to work out properly.  In particular, the third step is
wenzelm@10966
   925
  very sensitive to the invariant being either too strong or too weak.
wenzelm@10966
   926
  Moreover the invariant has to be sufficiently abstract, lest the
wenzelm@10966
   927
  proof become cluttered by confusing detail.
wenzelm@10966
   928
wenzelm@10966
   929
  \medskip The first two lemmas are technically straight forward ---
wenzelm@10966
   930
  we just have to inspect rather special cases.
wenzelm@10966
   931
*}
wenzelm@10966
   932
wenzelm@12079
   933
lemma (in invariant)
wenzelm@12079
   934
  cannot_rmdir: "invariant root bogus_path \<Longrightarrow>
wenzelm@17455
   935
    root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root' \<Longrightarrow> False"
wenzelm@10966
   936
proof -
wenzelm@10966
   937
  assume "invariant root bogus_path"
wenzelm@17455
   938
  then obtain "file" where "access root bogus_path user\<^isub>1 {} = Some file"
wenzelm@10966
   939
    by (unfold invariant_def) blast
wenzelm@10966
   940
  moreover
wenzelm@17455
   941
  assume "root \<midarrow>(Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1])\<rightarrow> root'"
wenzelm@10966
   942
  then obtain att where
wenzelm@17455
   943
      "access root [user\<^isub>1, name\<^isub>1] user\<^isub>1 {} = Some (Env att empty)"
wenzelm@10966
   944
    by cases auto
wenzelm@17455
   945
  hence "access root ([user\<^isub>1, name\<^isub>1] @ [name\<^isub>2]) user\<^isub>1 {} = empty name\<^isub>2"
wenzelm@10966
   946
    by (simp only: access_empty_lookup lookup_append_some) simp
wenzelm@10966
   947
  ultimately show False by (simp add: bogus_path_def)
wenzelm@10966
   948
qed
wenzelm@10966
   949
wenzelm@12079
   950
lemma (in invariant)
wenzelm@12079
   951
  init_invariant: "init users =bogus\<Rightarrow> root \<Longrightarrow> invariant root bogus_path"
wenzelm@10966
   952
proof -
wenzelm@12079
   953
  note eval = facts access_def init_def
wenzelm@11549
   954
  case rule_context thus ?thesis
wenzelm@10966
   955
    apply (unfold bogus_def bogus_path_def)
wenzelm@10966
   956
    apply (drule transitions_consD, rule transition.intros,
wenzelm@10966
   957
      (force simp add: eval)+, (simp add: eval)?)+
wenzelm@10966
   958
      -- "evaluate all operations"
wenzelm@10966
   959
    apply (drule transitions_nilD)
wenzelm@10966
   960
      -- "reach final result"
wenzelm@10966
   961
    apply (simp add: invariant_def eval)
wenzelm@10966
   962
      -- "check the invariant"
wenzelm@10966
   963
    done
wenzelm@10966
   964
qed
wenzelm@10966
   965
wenzelm@10966
   966
text {*
wenzelm@10966
   967
  \medskip At last we are left with the main effort to show that the
wenzelm@10966
   968
  ``bogosity'' invariant is preserved by any file-system operation
wenzelm@17455
   969
  performed by @{term user\<^isub>1} alone.  Note that this holds for
wenzelm@17455
   970
  any @{term path} given, the particular @{term bogus_path} is not
wenzelm@10966
   971
  required here.
wenzelm@11004
   972
*}
wenzelm@10966
   973
wenzelm@12079
   974
lemma (in invariant)
wenzelm@12079
   975
  preserve_invariant: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow>
wenzelm@17455
   976
    invariant root path \<Longrightarrow> uid_of x = user\<^isub>1 \<Longrightarrow> invariant root' path"
wenzelm@10966
   977
proof -
wenzelm@10966
   978
  assume tr: "root \<midarrow>x\<rightarrow> root'"
wenzelm@10966
   979
  assume inv: "invariant root path"
wenzelm@17455
   980
  assume uid: "uid_of x = user\<^isub>1"
wenzelm@10966
   981
wenzelm@10966
   982
  from inv obtain att dir where
wenzelm@17455
   983
      inv1: "access root path user\<^isub>1 {} = Some (Env att dir)" and
wenzelm@10966
   984
      inv2: "dir \<noteq> empty" and
wenzelm@17455
   985
      inv3: "user\<^isub>1 \<noteq> owner att" and
wenzelm@17455
   986
      inv4: "access root path user\<^isub>1 {Writable} = None"
wenzelm@10966
   987
    by (auto simp add: invariant_def)
wenzelm@10966
   988
wenzelm@10966
   989
  from inv1 have lookup: "lookup root path = Some (Env att dir)"
wenzelm@10966
   990
    by (simp only: access_empty_lookup)
wenzelm@10966
   991
wenzelm@17455
   992
  from inv1 inv3 inv4 and user\<^isub>1_not_root
wenzelm@10966
   993
  have not_writable: "Writable \<notin> others att"
wenzelm@10966
   994
    by (auto simp add: access_def split: option.splits if_splits)
wenzelm@10966
   995
wenzelm@10966
   996
  show ?thesis
wenzelm@10966
   997
  proof cases
wenzelm@10966
   998
    assume "root' = root"
wenzelm@10966
   999
    with inv show "invariant root' path" by (simp only:)
wenzelm@10966
  1000
  next
wenzelm@10966
  1001
    assume changed: "root' \<noteq> root"
wenzelm@10966
  1002
    with tr obtain opt where root': "root' = update (path_of x) opt root"
wenzelm@10966
  1003
      by cases auto
wenzelm@10966
  1004
    show ?thesis
wenzelm@10966
  1005
    proof (rule prefix_cases)
wenzelm@10966
  1006
      assume "path_of x \<parallel> path"
wenzelm@10966
  1007
      with inv root'
wenzelm@17455
  1008
      have "\<And>perms. access root' path user\<^isub>1 perms = access root path user\<^isub>1 perms"
wenzelm@10966
  1009
        by (simp only: access_update_other)
wenzelm@10966
  1010
      with inv show "invariant root' path"
wenzelm@10966
  1011
        by (simp only: invariant_def)
wenzelm@10966
  1012
    next
wenzelm@10966
  1013
      assume "path_of x \<le> path"
wenzelm@10966
  1014
      then obtain ys where path: "path = path_of x @ ys" ..
wenzelm@10966
  1015
wenzelm@10966
  1016
      show ?thesis
wenzelm@10966
  1017
      proof (cases ys)
wenzelm@10966
  1018
        assume "ys = []"
wenzelm@17455
  1019
        with tr uid inv2 inv3 lookup changed path and user\<^isub>1_not_root
wenzelm@10966
  1020
        have False
wenzelm@10966
  1021
          by cases (auto simp add: access_empty_lookup dest: access_some_lookup)
wenzelm@10966
  1022
        thus ?thesis ..
wenzelm@10966
  1023
      next
wenzelm@10966
  1024
        fix z zs assume ys: "ys = z # zs"
wenzelm@10966
  1025
        have "lookup root' path = lookup root path"
wenzelm@10966
  1026
        proof -
wenzelm@10966
  1027
          from inv2 lookup path ys
wenzelm@10966
  1028
          have look: "lookup root (path_of x @ z # zs) = Some (Env att dir)"
wenzelm@10966
  1029
            by (simp only:)
wenzelm@10966
  1030
          then obtain att' dir' file' where
wenzelm@10966
  1031
              look': "lookup root (path_of x) = Some (Env att' dir')" and
wenzelm@10966
  1032
              dir': "dir' z = Some file'" and
wenzelm@10966
  1033
              file': "lookup file' zs = Some (Env att dir)"
wenzelm@10966
  1034
            by (blast dest: lookup_some_upper)
wenzelm@10966
  1035
wenzelm@10966
  1036
          from tr uid changed look' dir' obtain att'' where
wenzelm@10966
  1037
              look'': "lookup root' (path_of x) = Some (Env att'' dir')"
wenzelm@10966
  1038
            by cases (auto simp add: access_empty_lookup lookup_update_some
wenzelm@10966
  1039
              dest: access_some_lookup)
wenzelm@10966
  1040
          with dir' file' have "lookup root' (path_of x @ z # zs) =
wenzelm@10966
  1041
              Some (Env att dir)"
wenzelm@10966
  1042
            by (simp add: lookup_append_some)
wenzelm@10966
  1043
          with look path ys show ?thesis
wenzelm@10966
  1044
            by simp
wenzelm@10966
  1045
        qed
wenzelm@10966
  1046
        with inv show "invariant root' path"
wenzelm@10966
  1047
          by (simp only: invariant_def access_def)
wenzelm@10966
  1048
      qed
wenzelm@10966
  1049
    next
wenzelm@10966
  1050
      assume "path < path_of x"
wenzelm@10966
  1051
      then obtain y ys where path: "path_of x = path @ y # ys" ..
wenzelm@10966
  1052
wenzelm@10966
  1053
      obtain dir' where
wenzelm@10966
  1054
        lookup': "lookup root' path = Some (Env att dir')" and
wenzelm@10966
  1055
        inv2': "dir' \<noteq> empty"
wenzelm@10966
  1056
      proof (cases ys)
wenzelm@10966
  1057
        assume "ys = []"
wenzelm@10966
  1058
        with path have parent: "path_of x = path @ [y]" by simp
berghofe@17146
  1059
        with tr uid inv4 changed obtain "file" where
wenzelm@10966
  1060
            "root' = update (path_of x) (Some file) root"
wenzelm@10966
  1061
          by cases auto
wenzelm@10979
  1062
        with lookup parent have "lookup root' path = Some (Env att (dir(y\<mapsto>file)))"
wenzelm@10966
  1063
          by (simp only: update_append_some update_cons_nil_env)
wenzelm@10966
  1064
        moreover have "dir(y\<mapsto>file) \<noteq> empty" by simp
wenzelm@10966
  1065
        ultimately show ?thesis ..
wenzelm@10966
  1066
      next
wenzelm@10966
  1067
        fix z zs assume ys: "ys = z # zs"
wenzelm@10966
  1068
        with lookup root' path
wenzelm@10966
  1069
        have "lookup root' path = Some (update (y # ys) opt (Env att dir))"
wenzelm@10966
  1070
          by (simp only: update_append_some)
wenzelm@10966
  1071
        also obtain file' where
wenzelm@10966
  1072
          "update (y # ys) opt (Env att dir) = Env att (dir(y\<mapsto>file'))"
wenzelm@10966
  1073
        proof -
wenzelm@10966
  1074
          have "dir y \<noteq> None"
wenzelm@10966
  1075
          proof -
wenzelm@10966
  1076
            have "dir y = lookup (Env att dir) [y]"
wenzelm@10966
  1077
              by (simp split: option.splits)
wenzelm@10966
  1078
            also from lookup have "\<dots> = lookup root (path @ [y])"
wenzelm@10966
  1079
              by (simp only: lookup_append_some)
wenzelm@10966
  1080
            also have "\<dots> \<noteq> None"
wenzelm@10966
  1081
            proof -
wenzelm@10966
  1082
              from ys obtain us u where rev_ys: "ys = us @ [u]"
berghofe@13601
  1083
                by (cases ys rule: rev_cases) fastsimp+
wenzelm@10966
  1084
              with tr path
wenzelm@10966
  1085
              have "lookup root ((path @ [y]) @ (us @ [u])) \<noteq> None \<or>
wenzelm@10966
  1086
                  lookup root ((path @ [y]) @ us) \<noteq> None"
wenzelm@10966
  1087
                by cases (auto dest: access_some_lookup)
wenzelm@10966
  1088
              thus ?thesis by (blast dest!: lookup_some_append)
wenzelm@10966
  1089
            qed
wenzelm@10966
  1090
            finally show ?thesis .
wenzelm@10966
  1091
          qed
wenzelm@10966
  1092
          with ys show ?thesis
wenzelm@10966
  1093
            by (insert that, auto simp add: update_cons_cons_env)
wenzelm@10966
  1094
        qed
wenzelm@10966
  1095
        also have "dir(y\<mapsto>file') \<noteq> empty" by simp
wenzelm@10966
  1096
        ultimately show ?thesis ..
wenzelm@10966
  1097
      qed
wenzelm@10966
  1098
wenzelm@17455
  1099
      from lookup' have inv1': "access root' path user\<^isub>1 {} = Some (Env att dir')"
wenzelm@10966
  1100
        by (simp only: access_empty_lookup)
wenzelm@10966
  1101
wenzelm@17455
  1102
      from inv3 lookup' and not_writable user\<^isub>1_not_root
wenzelm@17455
  1103
      have "access root' path user\<^isub>1 {Writable} = None"
wenzelm@10966
  1104
        by (simp add: access_def)
wenzelm@10966
  1105
      with inv1' inv2' inv3 show ?thesis by (unfold invariant_def) blast
wenzelm@10966
  1106
    qed
wenzelm@10966
  1107
  qed
wenzelm@10966
  1108
qed
wenzelm@10966
  1109
wenzelm@10966
  1110
wenzelm@10966
  1111
subsection {* Putting it all together \label{sec:unix-main-result} *}
wenzelm@10966
  1112
wenzelm@10966
  1113
text {*
wenzelm@10966
  1114
  The main result is now imminent, just by composing the three
wenzelm@10966
  1115
  invariance lemmas (see \secref{sec:unix-inv-lemmas}) according the the
wenzelm@10966
  1116
  overall procedure (see \secref{sec:unix-inv-procedure}).
wenzelm@10966
  1117
*}
wenzelm@10966
  1118
wenzelm@13380
  1119
corollary result:
wenzelm@13380
  1120
  includes invariant
wenzelm@13380
  1121
  assumes bogus: "init users =bogus\<Rightarrow> root"
wenzelm@17455
  1122
  shows "\<not> (\<exists>xs. (\<forall>x \<in> set xs. uid_of x = user\<^isub>1) \<and>
wenzelm@17455
  1123
    can_exec root (xs @ [Rmdir user\<^isub>1 [user\<^isub>1, name\<^isub>1]]))"
wenzelm@10966
  1124
proof -
wenzelm@13380
  1125
  from cannot_rmdir init_invariant preserve_invariant
wenzelm@13380
  1126
    and bogus show ?thesis by (rule general_procedure)
wenzelm@10966
  1127
qed
wenzelm@10966
  1128
wenzelm@13380
  1129
text {*
wenzelm@13380
  1130
  So this is our final result:
wenzelm@13380
  1131
wenzelm@17455
  1132
  @{thm [display, show_question_marks = false] result [OF
wenzelm@17455
  1133
  invariant.intro, OF situation.intro]}
wenzelm@13380
  1134
*}
wenzelm@13380
  1135
wenzelm@10966
  1136
end