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