author | haftmann |
Fri, 22 Mar 2019 19:18:08 +0000 | |
changeset 69946 | 494934c30f38 |
parent 69597 | ff784d5a5bfb |
permissions | -rw-r--r-- |
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
1 |
subsection "Termination-Sensitive Systems" |
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
2 |
|
43158 | 3 |
theory Sec_TypingT imports Sec_Type_Expr |
4 |
begin |
|
5 |
||
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
6 |
subsubsection "A Syntax Directed System" |
43158 | 7 |
|
8 |
inductive sec_type :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile> _)" [0,0] 50) where |
|
9 |
Skip: |
|
10 |
"l \<turnstile> SKIP" | |
|
11 |
Assign: |
|
50342 | 12 |
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile> x ::= a" | |
47818 | 13 |
Seq: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52382
diff
changeset
|
14 |
"l \<turnstile> c\<^sub>1 \<Longrightarrow> l \<turnstile> c\<^sub>2 \<Longrightarrow> l \<turnstile> c\<^sub>1;;c\<^sub>2" | |
43158 | 15 |
If: |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52382
diff
changeset
|
16 |
"\<lbrakk> max (sec b) l \<turnstile> c\<^sub>1; max (sec b) l \<turnstile> c\<^sub>2 \<rbrakk> |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52382
diff
changeset
|
17 |
\<Longrightarrow> l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2" | |
43158 | 18 |
While: |
50342 | 19 |
"sec b = 0 \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> 0 \<turnstile> WHILE b DO c" |
43158 | 20 |
|
21 |
code_pred (expected_modes: i => i => bool) sec_type . |
|
22 |
||
23 |
inductive_cases [elim!]: |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52382
diff
changeset
|
24 |
"l \<turnstile> x ::= a" "l \<turnstile> c\<^sub>1;;c\<^sub>2" "l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>2" "l \<turnstile> WHILE b DO c" |
43158 | 25 |
|
26 |
||
27 |
lemma anti_mono: "l \<turnstile> c \<Longrightarrow> l' \<le> l \<Longrightarrow> l' \<turnstile> c" |
|
45015 | 28 |
apply(induction arbitrary: l' rule: sec_type.induct) |
43158 | 29 |
apply (metis sec_type.intros(1)) |
30 |
apply (metis le_trans sec_type.intros(2)) |
|
31 |
apply (metis sec_type.intros(3)) |
|
32 |
apply (metis If le_refl sup_mono sup_nat_def) |
|
33 |
by (metis While le_0_eq) |
|
34 |
||
35 |
||
36 |
lemma confinement: "(c,s) \<Rightarrow> t \<Longrightarrow> l \<turnstile> c \<Longrightarrow> s = t (< l)" |
|
45015 | 37 |
proof(induction rule: big_step_induct) |
43158 | 38 |
case Skip thus ?case by simp |
39 |
next |
|
40 |
case Assign thus ?case by auto |
|
41 |
next |
|
47818 | 42 |
case Seq thus ?case by auto |
43158 | 43 |
next |
44 |
case (IfTrue b s c1) |
|
50342 | 45 |
hence "max (sec b) l \<turnstile> c1" by auto |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
53015
diff
changeset
|
46 |
hence "l \<turnstile> c1" by (metis max.cobounded2 anti_mono) |
45015 | 47 |
thus ?case using IfTrue.IH by metis |
43158 | 48 |
next |
49 |
case (IfFalse b s c2) |
|
50342 | 50 |
hence "max (sec b) l \<turnstile> c2" by auto |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
53015
diff
changeset
|
51 |
hence "l \<turnstile> c2" by (metis max.cobounded2 anti_mono) |
45015 | 52 |
thus ?case using IfFalse.IH by metis |
43158 | 53 |
next |
54 |
case WhileFalse thus ?case by auto |
|
55 |
next |
|
56 |
case (WhileTrue b s1 c) |
|
57 |
hence "l \<turnstile> c" by auto |
|
58 |
thus ?case using WhileTrue by metis |
|
59 |
qed |
|
60 |
||
61 |
lemma termi_if_non0: "l \<turnstile> c \<Longrightarrow> l \<noteq> 0 \<Longrightarrow> \<exists> t. (c,s) \<Rightarrow> t" |
|
45015 | 62 |
apply(induction arbitrary: s rule: sec_type.induct) |
43158 | 63 |
apply (metis big_step.Skip) |
64 |
apply (metis big_step.Assign) |
|
47818 | 65 |
apply (metis big_step.Seq) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
53015
diff
changeset
|
66 |
apply (metis IfFalse IfTrue le0 le_antisym max.cobounded2) |
43158 | 67 |
apply simp |
68 |
done |
|
69 |
||
70 |
theorem noninterference: "(c,s) \<Rightarrow> s' \<Longrightarrow> 0 \<turnstile> c \<Longrightarrow> s = t (\<le> l) |
|
71 |
\<Longrightarrow> \<exists> t'. (c,t) \<Rightarrow> t' \<and> s' = t' (\<le> l)" |
|
45015 | 72 |
proof(induction arbitrary: t rule: big_step_induct) |
43158 | 73 |
case Skip thus ?case by auto |
74 |
next |
|
75 |
case (Assign x a s) |
|
67406 | 76 |
have "sec x >= sec a" using \<open>0 \<turnstile> x ::= a\<close> by auto |
43158 | 77 |
have "(x ::= a,t) \<Rightarrow> t(x := aval a t)" by auto |
78 |
moreover |
|
79 |
have "s(x := aval a s) = t(x := aval a t) (\<le> l)" |
|
80 |
proof auto |
|
81 |
assume "sec x \<le> l" |
|
67406 | 82 |
with \<open>sec x \<ge> sec a\<close> have "sec a \<le> l" by arith |
43158 | 83 |
thus "aval a s = aval a t" |
67406 | 84 |
by (rule aval_eq_if_eq_le[OF \<open>s = t (\<le> l)\<close>]) |
43158 | 85 |
next |
86 |
fix y assume "y \<noteq> x" "sec y \<le> l" |
|
67406 | 87 |
thus "s y = t y" using \<open>s = t (\<le> l)\<close> by simp |
43158 | 88 |
qed |
89 |
ultimately show ?case by blast |
|
90 |
next |
|
47818 | 91 |
case Seq thus ?case by blast |
43158 | 92 |
next |
93 |
case (IfTrue b s c1 s' c2) |
|
67406 | 94 |
have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using \<open>0 \<turnstile> IF b THEN c1 ELSE c2\<close> by auto |
43158 | 95 |
obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
67406 | 96 |
using IfTrue.IH[OF anti_mono[OF \<open>sec b \<turnstile> c1\<close>] \<open>s = t (\<le> l)\<close>] by blast |
43158 | 97 |
show ?case |
98 |
proof cases |
|
50342 | 99 |
assume "sec b \<le> l" |
67406 | 100 |
hence "s = t (\<le> sec b)" using \<open>s = t (\<le> l)\<close> by auto |
101 |
hence "bval b t" using \<open>bval b s\<close> by(simp add: bval_eq_if_eq_le) |
|
43158 | 102 |
thus ?thesis by (metis t' big_step.IfTrue) |
103 |
next |
|
50342 | 104 |
assume "\<not> sec b \<le> l" |
105 |
hence 0: "sec b \<noteq> 0" by arith |
|
106 |
have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2" |
|
67406 | 107 |
by(rule sec_type.intros)(simp_all add: \<open>sec b \<turnstile> c1\<close> \<open>sec b \<turnstile> c2\<close>) |
108 |
from confinement[OF big_step.IfTrue[OF IfTrue(1,2)] 1] \<open>\<not> sec b \<le> l\<close> |
|
43158 | 109 |
have "s = s' (\<le> l)" by auto |
110 |
moreover |
|
111 |
from termi_if_non0[OF 1 0, of t] obtain t' where |
|
63539 | 112 |
t': "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" .. |
43158 | 113 |
moreover |
67406 | 114 |
from confinement[OF t' 1] \<open>\<not> sec b \<le> l\<close> |
43158 | 115 |
have "t = t' (\<le> l)" by auto |
116 |
ultimately |
|
67406 | 117 |
show ?case using \<open>s = t (\<le> l)\<close> by auto |
43158 | 118 |
qed |
119 |
next |
|
120 |
case (IfFalse b s c2 s' c1) |
|
67406 | 121 |
have "sec b \<turnstile> c1" "sec b \<turnstile> c2" using \<open>0 \<turnstile> IF b THEN c1 ELSE c2\<close> by auto |
43158 | 122 |
obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)" |
67406 | 123 |
using IfFalse.IH[OF anti_mono[OF \<open>sec b \<turnstile> c2\<close>] \<open>s = t (\<le> l)\<close>] by blast |
43158 | 124 |
show ?case |
125 |
proof cases |
|
50342 | 126 |
assume "sec b \<le> l" |
67406 | 127 |
hence "s = t (\<le> sec b)" using \<open>s = t (\<le> l)\<close> by auto |
128 |
hence "\<not> bval b t" using \<open>\<not> bval b s\<close> by(simp add: bval_eq_if_eq_le) |
|
43158 | 129 |
thus ?thesis by (metis t' big_step.IfFalse) |
130 |
next |
|
50342 | 131 |
assume "\<not> sec b \<le> l" |
132 |
hence 0: "sec b \<noteq> 0" by arith |
|
133 |
have 1: "sec b \<turnstile> IF b THEN c1 ELSE c2" |
|
67406 | 134 |
by(rule sec_type.intros)(simp_all add: \<open>sec b \<turnstile> c1\<close> \<open>sec b \<turnstile> c2\<close>) |
135 |
from confinement[OF big_step.IfFalse[OF IfFalse(1,2)] 1] \<open>\<not> sec b \<le> l\<close> |
|
43158 | 136 |
have "s = s' (\<le> l)" by auto |
137 |
moreover |
|
138 |
from termi_if_non0[OF 1 0, of t] obtain t' where |
|
63539 | 139 |
t': "(IF b THEN c1 ELSE c2,t) \<Rightarrow> t'" .. |
43158 | 140 |
moreover |
67406 | 141 |
from confinement[OF t' 1] \<open>\<not> sec b \<le> l\<close> |
43158 | 142 |
have "t = t' (\<le> l)" by auto |
143 |
ultimately |
|
67406 | 144 |
show ?case using \<open>s = t (\<le> l)\<close> by auto |
43158 | 145 |
qed |
146 |
next |
|
147 |
case (WhileFalse b s c) |
|
50342 | 148 |
hence [simp]: "sec b = 0" by auto |
67406 | 149 |
have "s = t (\<le> sec b)" using \<open>s = t (\<le> l)\<close> by auto |
150 |
hence "\<not> bval b t" using \<open>\<not> bval b s\<close> by (metis bval_eq_if_eq_le le_refl) |
|
43158 | 151 |
with WhileFalse.prems(2) show ?case by auto |
152 |
next |
|
153 |
case (WhileTrue b s c s'' s') |
|
154 |
let ?w = "WHILE b DO c" |
|
67406 | 155 |
from \<open>0 \<turnstile> ?w\<close> have [simp]: "sec b = 0" by auto |
156 |
have "0 \<turnstile> c" using \<open>0 \<turnstile> WHILE b DO c\<close> by auto |
|
157 |
from WhileTrue.IH(1)[OF this \<open>s = t (\<le> l)\<close>] |
|
43158 | 158 |
obtain t'' where "(c,t) \<Rightarrow> t''" and "s'' = t'' (\<le>l)" by blast |
67406 | 159 |
from WhileTrue.IH(2)[OF \<open>0 \<turnstile> ?w\<close> this(2)] |
43158 | 160 |
obtain t' where "(?w,t'') \<Rightarrow> t'" and "s' = t' (\<le>l)" by blast |
67406 | 161 |
from \<open>bval b s\<close> have "bval b t" |
162 |
using bval_eq_if_eq_le[OF \<open>s = t (\<le>l)\<close>] by auto |
|
43158 | 163 |
show ?case |
67406 | 164 |
using big_step.WhileTrue[OF \<open>bval b t\<close> \<open>(c,t) \<Rightarrow> t''\<close> \<open>(?w,t'') \<Rightarrow> t'\<close>] |
165 |
by (metis \<open>s' = t' (\<le> l)\<close>) |
|
43158 | 166 |
qed |
167 |
||
68776
403dd13cf6e9
avoid session qualification because no tex is generated when used;
nipkow
parents:
67406
diff
changeset
|
168 |
subsubsection "The Standard System" |
43158 | 169 |
|
69597 | 170 |
text\<open>The predicate \<^prop>\<open>l \<turnstile> c\<close> is nicely intuitive and executable. The |
43158 | 171 |
standard formulation, however, is slightly different, replacing the maximum |
172 |
computation by an antimonotonicity rule. We introduce the standard system now |
|
67406 | 173 |
and show the equivalence with our formulation.\<close> |
43158 | 174 |
|
175 |
inductive sec_type' :: "nat \<Rightarrow> com \<Rightarrow> bool" ("(_/ \<turnstile>'' _)" [0,0] 50) where |
|
176 |
Skip': |
|
177 |
"l \<turnstile>' SKIP" | |
|
178 |
Assign': |
|
50342 | 179 |
"\<lbrakk> sec x \<ge> sec a; sec x \<ge> l \<rbrakk> \<Longrightarrow> l \<turnstile>' x ::= a" | |
47818 | 180 |
Seq': |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52382
diff
changeset
|
181 |
"l \<turnstile>' c\<^sub>1 \<Longrightarrow> l \<turnstile>' c\<^sub>2 \<Longrightarrow> l \<turnstile>' c\<^sub>1;;c\<^sub>2" | |
43158 | 182 |
If': |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
52382
diff
changeset
|
183 |
"\<lbrakk> sec b \<le> l; l \<turnstile>' c\<^sub>1; l \<turnstile>' c\<^sub>2 \<rbrakk> \<Longrightarrow> l \<turnstile>' IF b THEN c\<^sub>1 ELSE c\<^sub>2" | |
43158 | 184 |
While': |
50342 | 185 |
"\<lbrakk> sec b = 0; 0 \<turnstile>' c \<rbrakk> \<Longrightarrow> 0 \<turnstile>' WHILE b DO c" | |
43158 | 186 |
anti_mono': |
187 |
"\<lbrakk> l \<turnstile>' c; l' \<le> l \<rbrakk> \<Longrightarrow> l' \<turnstile>' c" |
|
188 |
||
51456 | 189 |
lemma sec_type_sec_type': |
190 |
"l \<turnstile> c \<Longrightarrow> l \<turnstile>' c" |
|
45015 | 191 |
apply(induction rule: sec_type.induct) |
43158 | 192 |
apply (metis Skip') |
193 |
apply (metis Assign') |
|
47818 | 194 |
apply (metis Seq') |
54864
a064732223ad
abolished slightly odd global lattice interpretation for min/max
haftmann
parents:
54863
diff
changeset
|
195 |
apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono') |
43158 | 196 |
by (metis While') |
197 |
||
198 |
||
51456 | 199 |
lemma sec_type'_sec_type: |
200 |
"l \<turnstile>' c \<Longrightarrow> l \<turnstile> c" |
|
45015 | 201 |
apply(induction rule: sec_type'.induct) |
43158 | 202 |
apply (metis Skip) |
203 |
apply (metis Assign) |
|
47818 | 204 |
apply (metis Seq) |
54863
82acc20ded73
prefer more canonical names for lemmas on min/max
haftmann
parents:
53015
diff
changeset
|
205 |
apply (metis max.absorb2 If) |
43158 | 206 |
apply (metis While) |
207 |
by (metis anti_mono) |
|
208 |
||
51456 | 209 |
corollary sec_type_eq: "l \<turnstile> c \<longleftrightarrow> l \<turnstile>' c" |
210 |
by (metis sec_type'_sec_type sec_type_sec_type') |
|
211 |
||
43158 | 212 |
end |