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
     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\<^sub>1 \<Longrightarrow> l \<turnstile> c\<^sub>2 \<Longrightarrow> l \<turnstile> c\<^sub>1;;c\<^sub>2"  |
    13 If:
    14   "\<lbrakk> max (sec b) l \<turnstile> c\<^sub>1;  max (sec b) l \<turnstile> c\<^sub>2 \<rbrakk>
    15    \<Longrightarrow> l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>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\<^sub>1;;c\<^sub>2"  "l \<turnstile> IF b THEN c\<^sub>1 ELSE c\<^sub>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 max.cobounded2 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 max.cobounded2 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 max.cobounded2)
    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 `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
    93   obtain t' where t': "(c1, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
    94     using IfTrue.IH[OF anti_mono[OF `sec b \<turnstile> c1`] `s = t (\<le> l)`] 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 `0 \<turnstile> IF b THEN c1 ELSE c2` by auto
   120   obtain t' where t': "(c2, t) \<Rightarrow> t'" "s' = t' (\<le> l)"
   121     using IfFalse.IH[OF anti_mono[OF `sec b \<turnstile> c2`] `s = t (\<le> l)`] 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 `0 \<turnstile> WHILE b DO c` by auto
   155   from WhileTrue.IH(1)[OF this `s = t (\<le> l)`]
   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\<^sub>1 \<Longrightarrow> l \<turnstile>' c\<^sub>2 \<Longrightarrow> l \<turnstile>' c\<^sub>1;;c\<^sub>2"  |
   180 If':
   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"  |
   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 sec_type_sec_type': 
   188   "l \<turnstile> c \<Longrightarrow> l \<turnstile>' c"
   189 apply(induction rule: sec_type.induct)
   190 apply (metis Skip')
   191 apply (metis Assign')
   192 apply (metis Seq')
   193 apply (metis max.commute max.absorb_iff2 nat_le_linear If' anti_mono')
   194 by (metis While')
   195 
   196 
   197 lemma sec_type'_sec_type:
   198   "l \<turnstile>' c \<Longrightarrow> l \<turnstile> c"
   199 apply(induction rule: sec_type'.induct)
   200 apply (metis Skip)
   201 apply (metis Assign)
   202 apply (metis Seq)
   203 apply (metis max.absorb2 If)
   204 apply (metis While)
   205 by (metis anti_mono)
   206 
   207 corollary sec_type_eq: "l \<turnstile> c \<longleftrightarrow> l \<turnstile>' c"
   208 by (metis sec_type'_sec_type sec_type_sec_type')
   209 
   210 end