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