9 Nested_Environment |
9 Nested_Environment |
10 "~~/src/HOL/Library/Sublist" |
10 "~~/src/HOL/Library/Sublist" |
11 begin |
11 begin |
12 |
12 |
13 text \<open> |
13 text \<open> |
14 We give a simple mathematical model of the basic structures |
14 We give a simple mathematical model of the basic structures underlying the |
15 underlying the Unix file-system, together with a few fundamental |
15 Unix file-system, together with a few fundamental operations that could be |
16 operations that could be imagined to be performed internally by the |
16 imagined to be performed internally by the Unix kernel. This forms the basis |
17 Unix kernel. This forms the basis for the set of Unix system-calls |
17 for the set of Unix system-calls to be introduced later (see |
18 to be introduced later (see \secref{sec:unix-trans}), which are the |
18 \secref{sec:unix-trans}), which are the actual interface offered to |
19 actual interface offered to processes running in user-space. |
19 processes running in user-space. |
20 |
20 |
21 \medskip Basically, any Unix file is either a \emph{plain file} or a |
21 \<^medskip> |
22 \emph{directory}, consisting of some \emph{content} plus |
22 Basically, any Unix file is either a \<^emph>\<open>plain file\<close> or a \<^emph>\<open>directory\<close>, |
23 \emph{attributes}. The content of a plain file is plain text. The |
23 consisting of some \<^emph>\<open>content\<close> plus \<^emph>\<open>attributes\<close>. The content of a plain |
24 content of a directory is a mapping from names to further |
24 file is plain text. The content of a directory is a mapping from names to |
25 files.\footnote{In fact, this is the only way that names get |
25 further files.\<^footnote>\<open>In fact, this is the only way that names get associated with |
26 associated with files. In Unix files do \emph{not} have a name in |
26 files. In Unix files do \<^emph>\<open>not\<close> have a name in itself. Even more, any number |
27 itself. Even more, any number of names may be associated with the |
27 of names may be associated with the very same file due to \<^emph>\<open>hard links\<close> |
28 very same file due to \emph{hard links} (although this is excluded |
28 (although this is excluded from our model).\<close> Attributes include information |
29 from our model).} Attributes include information to control various |
29 to control various ways to access the file (read, write etc.). |
30 ways to access the file (read, write etc.). |
30 |
31 |
31 Our model will be quite liberal in omitting excessive detail that is easily |
32 Our model will be quite liberal in omitting excessive detail that is |
32 seen to be ``irrelevant'' for the aspects of Unix file-systems to be |
33 easily seen to be ``irrelevant'' for the aspects of Unix |
33 discussed here. First of all, we ignore character and block special files, |
34 file-systems to be discussed here. First of all, we ignore |
34 pipes, sockets, hard links, symbolic links, and mount points. |
35 character and block special files, pipes, sockets, hard links, |
|
36 symbolic links, and mount points. |
|
37 \<close> |
35 \<close> |
38 |
36 |
39 |
37 |
40 subsection \<open>Names\<close> |
38 subsection \<open>Names\<close> |
41 |
39 |
42 text \<open> |
40 text \<open> |
43 User ids and file name components shall be represented by natural |
41 User ids and file name components shall be represented by natural numbers |
44 numbers (without loss of generality). We do not bother about |
42 (without loss of generality). We do not bother about encoding of actual |
45 encoding of actual names (e.g.\ strings), nor a mapping between user |
43 names (e.g.\ strings), nor a mapping between user names and user ids as |
46 names and user ids as would be present in a reality. |
44 would be present in a reality. |
47 \<close> |
45 \<close> |
48 |
46 |
49 type_synonym uid = nat |
47 type_synonym uid = nat |
50 type_synonym name = nat |
48 type_synonym name = nat |
51 type_synonym path = "name list" |
49 type_synonym path = "name list" |
52 |
50 |
53 |
51 |
54 subsection \<open>Attributes\<close> |
52 subsection \<open>Attributes\<close> |
55 |
53 |
56 text \<open> |
54 text \<open> |
57 Unix file attributes mainly consist of \emph{owner} information and |
55 Unix file attributes mainly consist of \<^emph>\<open>owner\<close> information and a number of |
58 a number of \emph{permission} bits which control access for |
56 \<^emph>\<open>permission\<close> bits which control access for ``user'', ``group'', and |
59 ``user'', ``group'', and ``others'' (see the Unix man pages @{text |
57 ``others'' (see the Unix man pages \<open>chmod(2)\<close> and \<open>stat(2)\<close> for more |
60 "chmod(2)"} and @{text "stat(2)"} for more details). |
58 details). |
61 |
59 |
62 \medskip Our model of file permissions only considers the ``others'' |
60 \<^medskip> |
63 part. The ``user'' field may be omitted without loss of overall |
61 Our model of file permissions only considers the ``others'' part. The |
64 generality, since the owner is usually able to change it anyway by |
62 ``user'' field may be omitted without loss of overall generality, since the |
65 performing @{text chmod}.\footnote{The inclined Unix expert may try |
63 owner is usually able to change it anyway by performing \<open>chmod\<close>.\<^footnote>\<open>The |
66 to figure out some exotic arrangements of a real-world Unix |
64 inclined Unix expert may try to figure out some exotic arrangements of a |
67 file-system such that the owner of a file is unable to apply the |
65 real-world Unix file-system such that the owner of a file is unable to apply |
68 @{text chmod} system call.} We omit ``group'' permissions as a |
66 the \<open>chmod\<close> system call.\<close> We omit ``group'' permissions as a genuine |
69 genuine simplification as we just do not intend to discuss a model |
67 simplification as we just do not intend to discuss a model of multiple |
70 of multiple groups and group membership, but pretend that everyone |
68 groups and group membership, but pretend that everyone is member of a single |
71 is member of a single global group.\footnote{A general HOL model of |
69 global group.\<^footnote>\<open>A general HOL model of user group structures and related |
72 user group structures and related issues is given in |
70 issues is given in @{cite "Naraschewski:2001"}.\<close> |
73 @{cite "Naraschewski:2001"}.} |
|
74 \<close> |
71 \<close> |
75 |
72 |
76 datatype perm = |
73 datatype perm = |
77 Readable |
74 Readable |
78 | Writable |
75 | Writable |
79 | Executable -- "(ignored)" |
76 | Executable \<comment> "(ignored)" |
80 |
77 |
81 type_synonym perms = "perm set" |
78 type_synonym perms = "perm set" |
82 |
79 |
83 record att = |
80 record att = |
84 owner :: uid |
81 owner :: uid |
85 others :: perms |
82 others :: perms |
86 |
83 |
87 text \<open> |
84 text \<open> |
88 For plain files @{term Readable} and @{term Writable} specify read |
85 For plain files @{term Readable} and @{term Writable} specify read and write |
89 and write access to the actual content, i.e.\ the string of text |
86 access to the actual content, i.e.\ the string of text stored here. For |
90 stored here. For directories @{term Readable} determines if the set |
87 directories @{term Readable} determines if the set of entry names may be |
91 of entry names may be accessed, and @{term Writable} controls the |
88 accessed, and @{term Writable} controls the ability to create or delete any |
92 ability to create or delete any entries (both plain files or |
89 entries (both plain files or sub-directories). |
93 sub-directories). |
90 |
94 |
91 As another simplification, we ignore the @{term Executable} permission |
95 As another simplification, we ignore the @{term Executable} |
92 altogether. In reality it would indicate executable plain files (also known |
96 permission altogether. In reality it would indicate executable |
93 as ``binaries''), or control actual lookup of directory entries (recall that |
97 plain files (also known as ``binaries''), or control actual lookup |
94 mere directory browsing is controlled via @{term Readable}). Note that the |
98 of directory entries (recall that mere directory browsing is |
95 latter means that in order to perform any file-system operation whatsoever, |
99 controlled via @{term Readable}). Note that the latter means that |
96 all directories encountered on the path would have to grant @{term |
100 in order to perform any file-system operation whatsoever, all |
97 Executable}. We ignore this detail and pretend that all directories give |
101 directories encountered on the path would have to grant @{term |
98 @{term Executable} permission to anybody. |
102 Executable}. We ignore this detail and pretend that all directories |
|
103 give @{term Executable} permission to anybody. |
|
104 \<close> |
99 \<close> |
105 |
100 |
106 |
101 |
107 subsection \<open>Files\<close> |
102 subsection \<open>Files\<close> |
108 |
103 |
109 text \<open> |
104 text \<open> |
110 In order to model the general tree structure of a Unix file-system |
105 In order to model the general tree structure of a Unix file-system we use |
111 we use the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"} |
106 the arbitrarily branching datatype @{typ "('a, 'b, 'c) env"} from the |
112 from the standard library of Isabelle/HOL |
107 standard library of Isabelle/HOL @{cite "Bauer-et-al:2002:HOL-Library"}. |
113 @{cite "Bauer-et-al:2002:HOL-Library"}. This type provides |
108 This type provides constructors @{term Val} and @{term Env} as follows: |
114 constructors @{term Val} and @{term Env} as follows: |
109 |
115 |
110 \<^medskip> |
116 \medskip |
|
117 {\def\isastyleminor{\isastyle} |
111 {\def\isastyleminor{\isastyle} |
118 \begin{tabular}{l} |
112 \begin{tabular}{l} |
119 @{term [source] "Val :: 'a \<Rightarrow> ('a, 'b, 'c) env"} \\ |
113 @{term [source] "Val :: 'a \<Rightarrow> ('a, 'b, 'c) env"} \\ |
120 @{term [source] "Env :: 'b \<Rightarrow> ('c \<Rightarrow> ('a, 'b, 'c) env option) \<Rightarrow> ('a, 'b, 'c) env"} \\ |
114 @{term [source] "Env :: 'b \<Rightarrow> ('c \<Rightarrow> ('a, 'b, 'c) env option) \<Rightarrow> ('a, 'b, 'c) env"} \\ |
121 \end{tabular}} |
115 \end{tabular}} |
122 \medskip |
116 \<^medskip> |
123 |
117 |
124 Here the parameter @{typ 'a} refers to plain values occurring at |
118 Here the parameter @{typ 'a} refers to plain values occurring at leaf |
125 leaf positions, parameter @{typ 'b} to information kept with inner |
119 positions, parameter @{typ 'b} to information kept with inner branch nodes, |
126 branch nodes, and parameter @{typ 'c} to the branching type of the |
120 and parameter @{typ 'c} to the branching type of the tree structure. For our |
127 tree structure. For our purpose we use the type instance with @{typ |
121 purpose we use the type instance with @{typ "att \<times> string"} (representing |
128 "att \<times> string"} (representing plain files), @{typ att} (for |
122 plain files), @{typ att} (for attributes of directory nodes), and @{typ |
129 attributes of directory nodes), and @{typ name} (for the index type |
123 name} (for the index type of directory nodes). |
130 of directory nodes). |
|
131 \<close> |
124 \<close> |
132 |
125 |
133 type_synonym "file" = "(att \<times> string, att, name) env" |
126 type_synonym "file" = "(att \<times> string, att, name) env" |
134 |
127 |
135 text \<open> |
128 text \<open> |
136 \medskip The HOL library also provides @{term lookup} and @{term |
129 \<^medskip> |
137 update} operations for general tree structures with the subsequent |
130 The HOL library also provides @{term lookup} and @{term update} operations |
138 primitive recursive characterizations. |
131 for general tree structures with the subsequent primitive recursive |
139 |
132 characterizations. |
140 \medskip |
133 |
|
134 \<^medskip> |
141 {\def\isastyleminor{\isastyle} |
135 {\def\isastyleminor{\isastyle} |
142 \begin{tabular}{l} |
136 \begin{tabular}{l} |
143 @{term [source] "lookup :: ('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"} \\ |
137 @{term [source] "lookup :: ('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"} \\ |
144 @{term [source] |
138 @{term [source] |
145 "update :: 'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"} \\ |
139 "update :: 'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow> ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"} \\ |
146 \end{tabular}} |
140 \end{tabular}} |
147 |
141 |
148 @{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]} |
142 @{thm [display, indent = 2, eta_contract = false] lookup_eq [no_vars]} |
149 @{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]} |
143 @{thm [display, indent = 2, eta_contract = false] update_eq [no_vars]} |
150 |
144 |
151 Several further properties of these operations are proven in |
145 Several further properties of these operations are proven in @{cite |
152 @{cite "Bauer-et-al:2002:HOL-Library"}. These will be routinely used |
146 "Bauer-et-al:2002:HOL-Library"}. These will be routinely used later on |
153 later on without further notice. |
147 without further notice. |
154 |
148 |
155 \bigskip Apparently, the elements of type @{typ "file"} contain an |
149 \<^bigskip> |
156 @{typ att} component in either case. We now define a few auxiliary |
150 Apparently, the elements of type @{typ "file"} contain an @{typ att} |
157 operations to manipulate this field uniformly, following the |
151 component in either case. We now define a few auxiliary operations to |
158 conventions for record types in Isabelle/HOL |
152 manipulate this field uniformly, following the conventions for record types |
159 @{cite "Nipkow-et-al:2000:HOL"}. |
153 in Isabelle/HOL @{cite "Nipkow-et-al:2000:HOL"}. |
160 \<close> |
154 \<close> |
161 |
155 |
162 definition |
156 definition |
163 "attributes file = |
157 "attributes file = |
164 (case file of |
158 (case file of |
323 | "path_of (Mkdir uid perms path) = path" |
316 | "path_of (Mkdir uid perms path) = path" |
324 | "path_of (Rmdir uid path) = path" |
317 | "path_of (Rmdir uid path) = path" |
325 | "path_of (Readdir uid names path) = path" |
318 | "path_of (Readdir uid names path) = path" |
326 |
319 |
327 text \<open> |
320 text \<open> |
328 \medskip Note that we have omitted explicit @{text Open} and @{text |
321 \<^medskip> |
329 Close} operations, pretending that @{term Read} and @{term Write} |
322 Note that we have omitted explicit \<open>Open\<close> and \<open>Close\<close> operations, pretending |
330 would already take care of this behind the scenes. Thus we have |
323 that @{term Read} and @{term Write} would already take care of this behind |
331 basically treated actual sequences of real system-calls @{text |
324 the scenes. Thus we have basically treated actual sequences of real |
332 "open"}--@{text read}/@{text write}--@{text close} as atomic. |
325 system-calls \<open>open\<close>--\<open>read\<close>/\<open>write\<close>--\<open>close\<close> as atomic. |
333 |
326 |
334 In principle, this could make big a difference in a model with |
327 In principle, this could make big a difference in a model with explicit |
335 explicit concurrent processes. On the other hand, even on a real |
328 concurrent processes. On the other hand, even on a real Unix system the |
336 Unix system the exact scheduling of concurrent @{text "open"} and |
329 exact scheduling of concurrent \<open>open\<close> and \<open>close\<close> operations does \<^emph>\<open>not\<close> |
337 @{text close} operations does \emph{not} directly affect the success |
330 directly affect the success of corresponding \<open>read\<close> or \<open>write\<close>. Unix allows |
338 of corresponding @{text read} or @{text write}. Unix allows several |
331 several processes to have files opened at the same time, even for writing! |
339 processes to have files opened at the same time, even for writing! |
|
340 Certainly, the result from reading the contents later may be hard to |
332 Certainly, the result from reading the contents later may be hard to |
341 predict, but the system-calls involved here will succeed in any |
333 predict, but the system-calls involved here will succeed in any case. |
342 case. |
334 |
343 |
335 \<^bigskip> |
344 \bigskip The operational semantics of system calls is now specified |
336 The operational semantics of system calls is now specified via transitions |
345 via transitions of the file-system configuration. This is expressed |
337 of the file-system configuration. This is expressed as an inductive relation |
346 as an inductive relation (although there is no actual recursion |
338 (although there is no actual recursion involved here). |
347 involved here). |
|
348 \<close> |
339 \<close> |
349 |
340 |
350 inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool" |
341 inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool" |
351 ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100) |
342 ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100) |
352 where |
343 where |
391 "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow> |
382 "access root path uid {Readable} = Some (Env att dir) \<Longrightarrow> |
392 names = dom dir \<Longrightarrow> |
383 names = dom dir \<Longrightarrow> |
393 root \<midarrow>(Readdir uid names path)\<rightarrow> root" |
384 root \<midarrow>(Readdir uid names path)\<rightarrow> root" |
394 |
385 |
395 text \<open> |
386 text \<open> |
396 \medskip Certainly, the above specification is central to the whole |
387 \<^medskip> |
397 formal development. Any of the results to be established later on |
388 Certainly, the above specification is central to the whole formal |
398 are only meaningful to the outside world if this transition system |
389 development. Any of the results to be established later on are only |
399 provides an adequate model of real Unix systems. This kind of |
390 meaningful to the outside world if this transition system provides an |
400 ``reality-check'' of a formal model is the well-known problem of |
391 adequate model of real Unix systems. This kind of ``reality-check'' of a |
401 \emph{validation}. |
392 formal model is the well-known problem of \<^emph>\<open>validation\<close>. |
402 |
393 |
403 If in doubt, one may consider to compare our definition with the |
394 If in doubt, one may consider to compare our definition with the informal |
404 informal specifications given the corresponding Unix man pages, or |
395 specifications given the corresponding Unix man pages, or even peek at an |
405 even peek at an actual implementation such as |
396 actual implementation such as @{cite "Torvalds-et-al:Linux"}. Another common |
406 @{cite "Torvalds-et-al:Linux"}. Another common way to gain confidence |
397 way to gain confidence into the formal model is to run simple simulations |
407 into the formal model is to run simple simulations (see |
398 (see \secref{sec:unix-examples}), and check the results with that of |
408 \secref{sec:unix-examples}), and check the results with that of |
|
409 experiments performed on a real Unix system. |
399 experiments performed on a real Unix system. |
410 \<close> |
400 \<close> |
411 |
401 |
412 |
402 |
413 subsection \<open>Basic properties of single transitions \label{sec:unix-single-trans}\<close> |
403 subsection \<open>Basic properties of single transitions \label{sec:unix-single-trans}\<close> |
414 |
404 |
415 text \<open> |
405 text \<open> |
416 The transition system @{text "root \<midarrow>x\<rightarrow> root'"} defined above |
406 The transition system \<open>root \<midarrow>x\<rightarrow> root'\<close> defined above determines a unique |
417 determines a unique result @{term root'} from given @{term root} and |
407 result @{term root'} from given @{term root} and @{term x} (this is holds |
418 @{term x} (this is holds rather trivially, since there is even only |
408 rather trivially, since there is even only one clause for each operation). |
419 one clause for each operation). This uniqueness statement will |
409 This uniqueness statement will simplify our subsequent development to some |
420 simplify our subsequent development to some extent, since we only |
410 extent, since we only have to reason about a partial function rather than a |
421 have to reason about a partial function rather than a general |
411 general relation. |
422 relation. |
|
423 \<close> |
412 \<close> |
424 |
413 |
425 theorem transition_uniq: |
414 theorem transition_uniq: |
426 assumes root': "root \<midarrow>x\<rightarrow> root'" |
415 assumes root': "root \<midarrow>x\<rightarrow> root'" |
427 and root'': "root \<midarrow>x\<rightarrow> root''" |
416 and root'': "root \<midarrow>x\<rightarrow> root''" |
592 |
578 |
593 |
579 |
594 section \<open>Executable sequences\<close> |
580 section \<open>Executable sequences\<close> |
595 |
581 |
596 text \<open> |
582 text \<open> |
597 An inductively defined relation such as the one of @{text "root \<midarrow>x\<rightarrow> |
583 An inductively defined relation such as the one of \<open>root \<midarrow>x\<rightarrow> root'\<close> (see |
598 root'"} (see \secref{sec:unix-syscall}) has two main aspects. First |
584 \secref{sec:unix-syscall}) has two main aspects. First of all, the resulting |
599 of all, the resulting system admits a certain set of transition |
585 system admits a certain set of transition rules (introductions) as given in |
600 rules (introductions) as given in the specification. Furthermore, |
586 the specification. Furthermore, there is an explicit least-fixed-point |
601 there is an explicit least-fixed-point construction involved, which |
587 construction involved, which results in induction (and case-analysis) rules |
602 results in induction (and case-analysis) rules to eliminate known |
588 to eliminate known transitions in an exhaustive manner. |
603 transitions in an exhaustive manner. |
589 |
604 |
590 \<^medskip> |
605 \medskip Subsequently, we explore our transition system in an |
591 Subsequently, we explore our transition system in an experimental style, |
606 experimental style, mainly using the introduction rules with basic |
592 mainly using the introduction rules with basic algebraic properties of the |
607 algebraic properties of the underlying structures. The technique |
593 underlying structures. The technique closely resembles that of Prolog |
608 closely resembles that of Prolog combined with functional evaluation |
594 combined with functional evaluation in a very simple manner. |
609 in a very simple manner. |
595 |
610 |
596 Just as the ``closed-world assumption'' is left implicit in Prolog, we do |
611 Just as the ``closed-world assumption'' is left implicit in Prolog, |
597 not refer to induction over the whole transition system here. So this is |
612 we do not refer to induction over the whole transition system here. |
598 still purely positive reasoning about possible executions; exhaustive |
613 So this is still purely positive reasoning about possible |
599 reasoning will be employed only later on (see \secref{sec:unix-bogosity}), |
614 executions; exhaustive reasoning will be employed only later on (see |
600 when we shall demonstrate that certain behavior is \<^emph>\<open>not\<close> possible. |
615 \secref{sec:unix-bogosity}), when we shall demonstrate that certain |
|
616 behavior is \emph{not} possible. |
|
617 \<close> |
601 \<close> |
618 |
602 |
619 |
603 |
620 subsection \<open>Possible transitions\<close> |
604 subsection \<open>Possible transitions\<close> |
621 |
605 |
622 text \<open> |
606 text \<open> |
623 Rather obviously, a list of system operations can be executed within |
607 Rather obviously, a list of system operations can be executed within a |
624 a certain state if there is a result state reached by an iterated |
608 certain state if there is a result state reached by an iterated transition. |
625 transition. |
|
626 \<close> |
609 \<close> |
627 |
610 |
628 definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')" |
611 definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')" |
629 |
612 |
630 lemma can_exec_nil: "can_exec root []" |
613 lemma can_exec_nil: "can_exec root []" |
649 case (Cons x xs) |
633 case (Cons x xs) |
650 from \<open>can_exec root ((x # xs) @ [y])\<close> obtain r root'' where |
634 from \<open>can_exec root ((x # xs) @ [y])\<close> obtain r root'' where |
651 x: "root \<midarrow>x\<rightarrow> r" and |
635 x: "root \<midarrow>x\<rightarrow> r" and |
652 xs_y: "r =(xs @ [y])\<Rightarrow> root''" |
636 xs_y: "r =(xs @ [y])\<Rightarrow> root''" |
653 by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq) |
637 by (auto simp add: can_exec_def transitions_nil_eq transitions_cons_eq) |
654 from xs_y Cons.hyps obtain root' r' where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'" |
638 from xs_y Cons.hyps obtain root' r' |
|
639 where xs: "r =xs\<Rightarrow> root'" and y: "root' \<midarrow>y\<rightarrow> r'" |
655 unfolding can_exec_def by blast |
640 unfolding can_exec_def by blast |
656 from x xs have "root =(x # xs)\<Rightarrow> root'" |
641 from x xs have "root =(x # xs)\<Rightarrow> root'" |
657 by (rule transitions.cons) |
642 by (rule transitions.cons) |
658 with y show ?case by blast |
643 with y show ?case by blast |
659 qed |
644 qed |
660 |
645 |
661 |
646 |
662 subsection \<open>Example executions \label{sec:unix-examples}\<close> |
647 subsection \<open>Example executions \label{sec:unix-examples}\<close> |
663 |
648 |
664 text \<open> |
649 text \<open> |
665 We are now ready to perform a few experiments within our formal |
650 We are now ready to perform a few experiments within our formal model of |
666 model of Unix system-calls. The common technique is to alternate |
651 Unix system-calls. The common technique is to alternate introduction rules |
667 introduction rules of the transition system (see |
652 of the transition system (see \secref{sec:unix-trans}), and steps to solve |
668 \secref{sec:unix-trans}), and steps to solve any emerging side |
653 any emerging side conditions using algebraic properties of the underlying |
669 conditions using algebraic properties of the underlying file-system |
654 file-system structures (see \secref{sec:unix-file-system}). |
670 structures (see \secref{sec:unix-file-system}). |
|
671 \<close> |
655 \<close> |
672 |
656 |
673 lemmas eval = access_def init_def |
657 lemmas eval = access_def init_def |
674 |
658 |
675 theorem "u \<in> users \<Longrightarrow> can_exec (init users) |
659 theorem "u \<in> users \<Longrightarrow> can_exec (init users) |
676 [Mkdir u perms [u, name]]" |
660 [Mkdir u perms [u, name]]" |
677 apply (rule can_exec_cons) |
661 apply (rule can_exec_cons) |
678 -- \<open>back-chain @{term can_exec} (of @{term [source] Cons})\<close> |
662 \<comment> \<open>back-chain @{term can_exec} (of @{term [source] Cons})\<close> |
679 apply (rule mkdir) |
663 apply (rule mkdir) |
680 -- \<open>back-chain @{term Mkdir}\<close> |
664 \<comment> \<open>back-chain @{term Mkdir}\<close> |
681 apply (force simp add: eval)+ |
665 apply (force simp add: eval)+ |
682 -- \<open>solve preconditions of @{term Mkdir}\<close> |
666 \<comment> \<open>solve preconditions of @{term Mkdir}\<close> |
683 apply (simp add: eval) |
667 apply (simp add: eval) |
684 -- \<open>peek at resulting dir (optional)\<close> |
668 \<comment> \<open>peek at resulting dir (optional)\<close> |
685 txt \<open>@{subgoals [display]}\<close> |
669 txt \<open>@{subgoals [display]}\<close> |
686 apply (rule can_exec_nil) |
670 apply (rule can_exec_nil) |
687 -- \<open>back-chain @{term can_exec} (of @{term [source] Nil})\<close> |
671 \<comment> \<open>back-chain @{term can_exec} (of @{term [source] Nil})\<close> |
688 done |
672 done |
689 |
673 |
690 text \<open> |
674 text \<open> |
691 By inspecting the result shown just before the final step above, we |
675 By inspecting the result shown just before the final step above, we may gain |
692 may gain confidence that our specification of Unix system-calls |
676 confidence that our specification of Unix system-calls actually makes sense. |
693 actually makes sense. Further common errors are usually exhibited |
677 Further common errors are usually exhibited when preconditions of transition |
694 when preconditions of transition rules fail unexpectedly. |
678 rules fail unexpectedly. |
695 |
679 |
696 \medskip Here are a few further experiments, using the same |
680 \<^medskip> |
697 techniques as before. |
681 Here are a few further experiments, using the same techniques as before. |
698 \<close> |
682 \<close> |
699 |
683 |
700 theorem "u \<in> users \<Longrightarrow> can_exec (init users) |
684 theorem "u \<in> users \<Longrightarrow> can_exec (init users) |
701 [Creat u perms [u, name], |
685 [Creat u perms [u, name], |
702 Unlink u [u, name]]" |
686 Unlink u [u, name]]" |
827 |
810 |
828 definition "bogus_path = [user\<^sub>1, name\<^sub>1, name\<^sub>2]" |
811 definition "bogus_path = [user\<^sub>1, name\<^sub>1, name\<^sub>2]" |
829 |
812 |
830 text \<open> |
813 text \<open> |
831 The @{term bogus} operations are the ones that lead into the uncouth |
814 The @{term bogus} operations are the ones that lead into the uncouth |
832 situation; @{term bogus_path} is the key position within the |
815 situation; @{term bogus_path} is the key position within the file-system |
833 file-system where things go awry. |
816 where things go awry. |
834 \<close> |
817 \<close> |
835 |
818 |
836 |
819 |
837 subsection \<open>Invariance lemmas \label{sec:unix-inv-lemmas}\<close> |
820 subsection \<open>Invariance lemmas \label{sec:unix-inv-lemmas}\<close> |
838 |
821 |
839 text \<open> |
822 text \<open> |
840 The following invariant over the root file-system describes the |
823 The following invariant over the root file-system describes the bogus |
841 bogus situation in an abstract manner: located at a certain @{term |
824 situation in an abstract manner: located at a certain @{term path} within |
842 path} within the file-system is a non-empty directory that is |
825 the file-system is a non-empty directory that is neither owned nor writable |
843 neither owned nor writable by @{term user\<^sub>1}. |
826 by @{term user\<^sub>1}. |
844 \<close> |
827 \<close> |
845 |
828 |
846 definition |
829 definition |
847 "invariant root path = |
830 "invariant root path = |
848 (\<exists>att dir. |
831 (\<exists>att dir. |
849 access root path user\<^sub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> |
832 access root path user\<^sub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> |
850 user\<^sub>1 \<noteq> owner att \<and> |
833 user\<^sub>1 \<noteq> owner att \<and> |
851 access root path user\<^sub>1 {Writable} = None)" |
834 access root path user\<^sub>1 {Writable} = None)" |
852 |
835 |
853 text \<open> |
836 text \<open> |
854 Following the general procedure (see |
837 Following the general procedure (see \secref{sec:unix-inv-procedure}) we |
855 \secref{sec:unix-inv-procedure}) we will now establish the three key |
838 will now establish the three key lemmas required to yield the final result. |
856 lemmas required to yield the final result. |
839 |
857 |
840 \<^enum> The invariant is sufficiently strong to entail the pathological case |
858 \begin{enumerate} |
841 that @{term user\<^sub>1} is unable to remove the (owned) directory at @{term |
859 |
842 "[user\<^sub>1, name\<^sub>1]"}. |
860 \item The invariant is sufficiently strong to entail the |
843 |
861 pathological case that @{term user\<^sub>1} is unable to remove the |
844 \<^enum> The invariant does hold after having executed the @{term bogus} list of |
862 (owned) directory at @{term "[user\<^sub>1, name\<^sub>1]"}. |
845 operations (starting with an initial file-system configuration). |
863 |
846 |
864 \item The invariant does hold after having executed the @{term |
847 \<^enum> The invariant is preserved by any file-system operation performed by |
865 bogus} list of operations (starting with an initial file-system |
848 @{term user\<^sub>1} alone, without any help by other users. |
866 configuration). |
849 |
867 |
850 As the invariant appears both as assumptions and conclusions in the course |
868 \item The invariant is preserved by any file-system operation |
851 of proof, its formulation is rather critical for the whole development to |
869 performed by @{term user\<^sub>1} alone, without any help by other |
852 work out properly. In particular, the third step is very sensitive to the |
870 users. |
853 invariant being either too strong or too weak. Moreover the invariant has to |
871 |
854 be sufficiently abstract, lest the proof become cluttered by confusing |
872 \end{enumerate} |
855 detail. |
873 |
856 |
874 As the invariant appears both as assumptions and conclusions in the |
857 \<^medskip> |
875 course of proof, its formulation is rather critical for the whole |
858 The first two lemmas are technically straight forward --- we just have to |
876 development to work out properly. In particular, the third step is |
859 inspect rather special cases. |
877 very sensitive to the invariant being either too strong or too weak. |
|
878 Moreover the invariant has to be sufficiently abstract, lest the |
|
879 proof become cluttered by confusing detail. |
|
880 |
|
881 \medskip The first two lemmas are technically straight forward --- |
|
882 we just have to inspect rather special cases. |
|
883 \<close> |
860 \<close> |
884 |
861 |
885 lemma cannot_rmdir: |
862 lemma cannot_rmdir: |
886 assumes inv: "invariant root bogus_path" |
863 assumes inv: "invariant root bogus_path" |
887 and rmdir: "root \<midarrow>(Rmdir user\<^sub>1 [user\<^sub>1, name\<^sub>1])\<rightarrow> root'" |
864 and rmdir: "root \<midarrow>(Rmdir user\<^sub>1 [user\<^sub>1, name\<^sub>1])\<rightarrow> root'" |