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