Theory Degeneracy

(*  Title:       Information Flow Control via Stateful Intransitive Noninterference in Language IMP
    Author:      Pasquale Noce
                 Senior Staff Firmware Engineer at HID Global, Italy
                 pasquale dot noce dot lavoro at gmail dot com
                 pasquale dot noce at hidglobal dot com
*)

section "Degeneracy to stateless level-based information flow control"

theory Degeneracy
  imports Correctness "HOL-IMP.Sec_TypingT"
begin

text ‹
\null

The goal of this concluding section is to prove the degeneracy of the information flow correctness
notion and the static type system defined in this paper to the classical counterparts addressed in
cite‹"Nipkow23-1"›, section 9.2.6, and formalized in cite‹"Nipkow23-2"› and cite‹"Nipkow23-3"›, in
case of a stateless level-based information flow correctness policy.

First of all, locale @{locale noninterf} is interpreted within the context of the class @{class sec}
defined in cite‹"Nipkow23-2"›, as follows.

  ▪ Parameter @{text dom} is instantiated as function @{text sec}, which also sets the type variable
standing for the type of the domains to @{typ nat}.

  ▪ Parameter @{text interf} is instantiated as the predicate such that for any program state, the
output is @{const True} just in case the former input level may interfere with, namely is not larger
than, the latter one.

  ▪ Parameter @{text state} is instantiated as the empty set, consistently with the fact that the
policy is represented by a single, stateless interference predicate.

Next, the information flow security notion implied by theorem @{thm [source] noninterference} in
cite‹"Nipkow23-3"› is formalized as a predicate @{text secure} taking a program as input. This
notion is then proven to be implied, in the degenerate interpretation described above, by the
information flow correctness notion formalized as predicate @{const [names_short] noninterf.correct} 
(theorem @{text correct_secure}). Particularly:

  ▪ This theorem demands the additional assumption that the @{typ "state set"} @{term A} input to
@{const [names_short] noninterf.correct} is nonempty, since @{const [names_short] noninterf.correct}
is vacuously true for @{prop "A = {}"}.

  ▪ In order for this theorem to hold, predicate @{text secure} needs to slight differ from the
information flow security notion implied by theorem @{thm [source] noninterference}, in that it
requires state @{term t'} to exist if there also exists some variable with a level not larger than
@{term l}, namely if condition @{prop "s = t (≤ l)"} is satisfied \emph{nontrivially} -- actually,
no leakage may arise from two initial states disagreeing on the value of \emph{every} variable. In
fact, predicate @{const [names_short] noninterf.correct} requires a nontrivial configuration
@{term "(c2', t2)"} to exist in case condition @{prop "s1 = t1 (⊆ sources cs s1 x)"} is satisfied
\emph{for some variable} \lstinline{x}.

Finally, the static type system @{const [names_short] noninterf.ctyping2} is proven to be equivalent
to the @{const sec_type} one defined in cite‹"Nipkow23-3"› in the above degenerate interpretation
(theorems @{text ctyping2_sec_type} and @{text sec_type_ctyping2}). The former theorem, which proves
that a \emph{pass} verdict from @{const [names_short] noninterf.ctyping2} implies the issuance of a
\emph{pass} verdict from @{const sec_type} as well, demands the additional assumptions that (a) the
@{typ "state set"} input to @{const [names_short] noninterf.ctyping2} is nonempty, (b) the input
program does not contain any loop with @{term "Bc True"} as boolean condition, and (c) the input
program has undergone \emph{constant folding}, as addressed in cite‹"Nipkow23-1"›, section 3.1.3
for arithmetic expressions and in cite‹"Nipkow23-1"›, section 3.2.1 for boolean expressions. Why?

This need arises from the different ways in which the two type systems handle ``dead'' conditional
branches. Type system @{const sec_type} does not try to detect ``dead'' branches; it simply applies
its full range of information flow security checks to any conditional branch contained in the input
program, even if it actually is a ``dead'' one. On the contrary, type system @{const [names_short]
noninterf.ctyping2} detects ``dead'' branches whenever boolean conditions can be evaluated at
compile time, and applies only a subset of its information flow correctness checks to such branches.

As parameter @{text state} is instantiated as the empty set, boolean conditions containing variables
cannot be evaluated at compile time, yet they can if they only contain constants. Thus, assumption
(a) prevents @{const [names_short] noninterf.ctyping2} from handling the entire input program as a
``dead'' branch, while assumptions (b) and (c) ensure that @{const [names_short] noninterf.ctyping2}
will not detect any ``dead'' conditional branch within the program. On the whole, those assumptions
guarantee that @{const [names_short] noninterf.ctyping2}, like @{const sec_type}, applies its full
range of checks to \emph{any} conditional branch contained in the input program, as required for
theorem @{text ctyping2_sec_type} to hold.
›


subsection "Global context definitions and proofs"

fun cgood :: "com ⇒ bool" where
"cgood (c1;; c2) = (cgood c1 ∧ cgood c2)" |
"cgood (IF _ THEN c1 ELSE c2) = (cgood c1 ∧ cgood c2)" |
"cgood (WHILE b DO c) = (b ≠ Bc True ∧ cgood c)" |
"cgood _ = True"


fun seq :: "com ⇒ com ⇒ com" where
"seq SKIP c = c" |
"seq c SKIP = c" |
"seq c1 c2 = c1;; c2"

fun ifc :: "bexp ⇒ com ⇒ com ⇒ com" where
"ifc (Bc True) c _ = c" |
"ifc (Bc False) _ c = c" |
"ifc b c1 c2 = (if c1 = c2 then c1 else IF b THEN c1 ELSE c2)"

fun while :: "bexp ⇒ com ⇒ com" where
"while (Bc False) _ = SKIP" |
"while b c = WHILE b DO c"

primrec csimp :: "com ⇒ com" where
"csimp SKIP = SKIP" |
"csimp (x ::= a) = x ::= asimp a" |
"csimp (c1;; c2) = seq (csimp c1) (csimp c2)" |
"csimp (IF b THEN c1 ELSE c2) = ifc (bsimp b) (csimp c1) (csimp c2)" |
"csimp (WHILE b DO c) = while (bsimp b) (csimp c)"


lemma not_size:
 "size (not b) ≤ Suc (size b)"
by (induction b rule: not.induct, simp_all)

lemma and_size:
 "size (and b1 b2) ≤ Suc (size b1 + size b2)"
by (induction b1 b2 rule: and.induct, simp_all)

lemma less_size:
 "size (less a1 a2) = 0"
by (induction a1 a2 rule: less.induct, simp_all)

lemma bsimp_size:
 "size (bsimp b) ≤ size b"
by (induction b, auto intro: le_trans not_size and_size simp: less_size)


lemma seq_size:
 "size (seq c1 c2) ≤ Suc (size c1 + size c2)"
by (induction c1 c2 rule: seq.induct, simp_all)

lemma ifc_size:
 "size (ifc b c1 c2) ≤ Suc (size c1 + size c2)"
by (induction b c1 c2 rule: ifc.induct, simp_all)

lemma while_size:
 "size (while b c) ≤ Suc (size c)"
by (induction b c rule: while.induct, simp_all)

lemma csimp_size:
 "size (csimp c) ≤ size c"
by (induction c, auto intro: le_trans seq_size ifc_size while_size)


lemma avars_asimp:
 "avars a = {} ⟹ ∃i. asimp a = N i"
by (induction a, auto)

lemma seq_match [dest!]:
 "seq (csimp c1) (csimp c2) = c1;; c2 ⟹ csimp c1 = c1 ∧ csimp c2 = c2"
by (rule seq.cases [of "(csimp c1, csimp c2)"],
 insert csimp_size [of c1], insert csimp_size [of c2], simp_all)

lemma ifc_match [dest!]:
 "ifc (bsimp b) (csimp c1) (csimp c2) = IF b THEN c1 ELSE c2 ⟹
    bsimp b = b ∧ (∀v. b ≠ Bc v) ∧ csimp c1 = c1 ∧ csimp c2 = c2"
by (insert csimp_size [of c1], insert csimp_size [of c2],
 subgoal_tac "csimp c1 ≠ IF b THEN c1 ELSE c2", auto intro: ifc.cases
 [of "(bsimp b, csimp c1, csimp c2)"] split: if_split_asm)

lemma while_match [dest!]:
 "while (bsimp b) (csimp c) = WHILE b DO c ⟹
    bsimp b = b ∧ b ≠ Bc False ∧ csimp c = c"
by (rule while.cases [of "(bsimp b, csimp c)"], auto)


subsection "Local context definitions and proofs"

context sec
begin


interpretation noninterf "λs. (≤)" sec "{}"
by (unfold_locales, simp)

notation interf_set  ("(_: _ ↝ _)" [51, 51, 51] 50)
notation univ_states_if  ("(Univ? _ _)" [51, 75] 75)
notation atyping  ("(_ ⊨ _ '(⊆ _'))" [51, 51] 50)
notation btyping2_aux  ("(⊫ _ '(⊆ _, _'))" [51] 55)
notation btyping2  ("(⊨ _ '(⊆ _, _'))" [51] 55)
notation ctyping1  ("(⊢ _ '(⊆ _, _'))" [51] 55)
notation ctyping2  ("(_ ⊨ _ '(⊆ _, _'))" [51, 51] 55)


abbreviation eq_le_ext :: "state ⇒ state ⇒ level ⇒ bool"
  ("(_ = _ '(≤ _'))" [51, 51, 0] 50) where
"s = t (≤ l) ≡ s = t (≤ l) ∧ (∃x :: vname. sec x ≤ l)"

definition secure :: "com ⇒ bool" where
"secure c ≡ ∀s s' t l. (c, s) ⇒ s' ∧ s = t (≤ l) ⟶
  (∃t'. (c, t) ⇒ t' ∧ s' = t' (≤ l))"

definition levels :: "config set ⇒ level set" where
"levels U ≡ insert 0 (sec ` ⋃ (snd ` {(B, Y) ∈ U. B ≠ {}}))"


lemma avars_finite:
 "finite (avars a)"
by (induction a, simp_all)

lemma avars_in:
 "n < sec a ⟹ sec a ∈ sec ` avars a"
by (induction a, auto simp: max_def)

lemma avars_sec:
 "x ∈ avars a ⟹ sec x ≤ sec a"
by (induction a, auto)

lemma avars_ub:
 "sec a ≤ l = (∀x ∈ avars a. sec x ≤ l)"
by (induction a, auto)


lemma bvars_finite:
 "finite (bvars b)"
by (induction b, simp_all add: avars_finite)

lemma bvars_in:
 "n < sec b ⟹ sec b ∈ sec ` bvars b"
by (induction b, auto dest!: avars_in simp: max_def)

lemma bvars_sec:
 "x ∈ bvars b ⟹ sec x ≤ sec b"
by (induction b, auto dest: avars_sec)

lemma bvars_ub:
 "sec b ≤ l = (∀x ∈ bvars b. sec x ≤ l)"
by (induction b, auto simp: avars_ub)


lemma levels_insert:
  assumes
    A: "A ≠ {}" and
    B: "finite (levels U)"
  shows "finite (levels (insert (A, bvars b) U)) ∧
    Max (levels (insert (A, bvars b) U)) = max (sec b) (Max (levels U))"
    (is "finite (levels ?U') ∧ ?P")
proof -
  have C: "levels ?U' = sec ` bvars b ∪ levels U"
    using A by (auto simp: image_def levels_def univ_states_if_def)
  hence D: "finite (levels ?U')"
    using B by (simp add: bvars_finite)
  moreover have ?P
  proof (rule Max_eqI [OF D])
    fix l
    assume "l ∈ levels (insert (A, bvars b) U)"
    thus "l ≤ max (sec b) (Max (levels U))"
      using C by (auto dest: Max_ge [OF B] bvars_sec)
  next
    show "max (sec b) (Max (levels U)) ∈ levels (insert (A, bvars b) U)"
      using C by (insert Max_in [OF B],
       fastforce dest: bvars_in simp: max_def not_le levels_def)
  qed
  ultimately show ?thesis ..
qed

lemma sources_le:
 "y ∈ sources cs s x ⟹ sec y ≤ sec x"
and sources_aux_le:
 "y ∈ sources_aux cs s x ⟹ sec y ≤ sec x"
by (induction cs s x and cs s x rule: sources_induct,
 auto split: com_flow.split_asm if_split_asm, fastforce+)


lemma bsimp_btyping2_aux_not [intro]:
 "⟦bsimp b = b ⟹ ∀v. b ≠ Bc v ⟹ ⊫ b (⊆ A, X) = None;
    not (bsimp b) = Not b⟧ ⟹ ⊫ b (⊆ A, X) = None"
by (rule not.cases [of "bsimp b"], auto)

lemma bsimp_btyping2_aux_and [intro]:
  assumes
    A: "⟦bsimp b1 = b1; ∀v. b1 ≠ Bc v⟧ ⟹ ⊫ b1 (⊆ A, X) = None" and
    B: "and (bsimp b1) (bsimp b2) = And b1 b2"
  shows "⊫ b1 (⊆ A, X) = None"
proof -
  {
    assume "bsimp b2 = And b1 b2"
    hence "Bc True = b1"
      by (insert bsimp_size [of b2], simp)
  }
  moreover {
    assume "bsimp b2 = And (Bc True) b2"
    hence False
      by (insert bsimp_size [of b2], simp)
  }
  moreover {
    assume "bsimp b1 = And b1 b2"
    hence False
      by (insert bsimp_size [of b1], simp)
  }
  ultimately have "bsimp b1 = b1 ∧ (∀v. b1 ≠ Bc v)"
    using B by (auto intro: and.cases [of "(bsimp b1, bsimp b2)"])
  thus ?thesis
    using A by simp
qed

lemma bsimp_btyping2_aux_less [elim]:
 "⟦less (asimp a1) (asimp a2) = Less a1 a2;
    avars a1 = {}; avars a2 = {}⟧ ⟹ False"
by (fastforce dest: avars_asimp)

lemma bsimp_btyping2_aux:
 "⟦bsimp b = b; ∀v. b ≠ Bc v⟧ ⟹ ⊫ b (⊆ A, X) = None"
by (induction b, auto split: option.split)

lemma bsimp_btyping2:
 "⟦bsimp b = b; ∀v. b ≠ Bc v⟧ ⟹ ⊨ b (⊆ A, X) = (A, A)"
by (auto dest: bsimp_btyping2_aux [of _ A X] simp: btyping2_def)


lemma csimp_ctyping2_if:
 "⟦⋀U' B B'. U' = U ⟹ B = B1 ⟹ {} = B' ⟹ B1 ≠ {} ⟹ False; s ∈ A;
    ⊨ b (⊆ A, X) = (B1, B2); bsimp b = b; ∀v. b ≠ Bc v⟧ ⟹
  False"
by (drule bsimp_btyping2 [of _ A X], auto)

lemma csimp_ctyping2_while:
 "⟦(if P then Some (B2 ∪ B2', Y) else None) = Some ({}, Z); s ∈ A;
    ⊨ b (⊆ A, X) = (B1, B2); bsimp b = b; b ≠ Bc True; b ≠ Bc False⟧ ⟹
  False"
by (drule bsimp_btyping2 [of _ A X], auto split: if_split_asm)

lemma csimp_ctyping2:
 "⟦(U, v) ⊨ c (⊆ A, X) = Some (B, Y); A ≠ {}; cgood c; csimp c = c⟧ ⟹
    B ≠ {}"
proof (induction "(U, v)" c A X arbitrary: B Y U v rule: ctyping2.induct)
  fix A X B Y U v c1 c2
  show
   "⟦⋀B Y. (U, v) ⊨ c1 (⊆ A, X) = Some (B, Y) ⟹
      A ≠ {} ⟹ cgood c1 ⟹ csimp c1 = c1 ⟹
      B ≠ {};
    ⋀p B Y C Z. (U, v) ⊨ c1 (⊆ A, X) = Some p ⟹
      (B, Y) = p ⟹ (U, v) ⊨ c2 (⊆ B, Y) = Some (C, Z) ⟹
      B ≠ {} ⟹ cgood c2 ⟹ csimp c2 = c2 ⟹
      C ≠ {};
    (U, v) ⊨ c1;; c2 (⊆ A, X) = Some (B, Y);
    A ≠ {}; cgood (c1;; c2);
    csimp (c1;; c2) = c1;; c2⟧ ⟹
      B ≠ {}"
    by (fastforce split: option.split_asm)
next
  fix A X C Y U v b c1 c2
  show
   "⟦⋀U' p B1 B2 C Y.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B1, B2) = p ⟹ (U', v) ⊨ c1 (⊆ B1, X) = Some (C, Y) ⟹
      B1 ≠ {} ⟹ cgood c1 ⟹ csimp c1 = c1 ⟹
      C ≠ {};
    ⋀U' p B1 B2 C Y.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B1, B2) = p ⟹ (U', v) ⊨ c2 (⊆ B2, X) = Some (C, Y) ⟹
      B2 ≠ {} ⟹ cgood c2 ⟹ csimp c2 = c2 ⟹
      C ≠ {};
      (U, v) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (C, Y);
    A ≠ {}; cgood (IF b THEN c1 ELSE c2);
    csimp (IF b THEN c1 ELSE c2) = IF b THEN c1 ELSE c2⟧ ⟹
      C ≠ {}"
    by (auto split: option.split_asm prod.split_asm,
     rule csimp_ctyping2_if)
next
  fix A X B Z U v b c
  show
   "⟦⋀B1 B2 C Y B1' B2' B Z.
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹
      (B1', B2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: sec ` W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B1, X) = Some (B, Z) ⟹
      B1 ≠ {} ⟹ cgood c ⟹ csimp c = c ⟹
      B ≠ {};
    ⋀B1 B2 C Y B1' B2' B Z.
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹
      (B1', B2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: sec ` W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B1', Y) = Some (B, Z) ⟹
      B1' ≠ {} ⟹ cgood c ⟹ csimp c = c ⟹
      B ≠ {};
    (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Z);
    A ≠ {}; cgood (WHILE b DO c);
    csimp (WHILE b DO c) = WHILE b DO c⟧ ⟹
      B ≠ {}"
    by (auto split: option.split_asm prod.split_asm,
     rule csimp_ctyping2_while)
qed (simp_all split: if_split_asm)


theorem correct_secure:
  assumes
    A: "correct c A X" and
    B: "A ≠ {}"
  shows "secure c"
proof -
  {
    fix s s' t l and x :: vname
    assume "(c, s) ⇒ s'"
    then obtain cfs where C: "(c, s) →*{cfs} (SKIP, s')"
      by (auto dest: small_steps_stepsl simp: big_iff_small)
    assume D: "s = t (≤ l)"
    have E: "∀x. sec x ≤ l ⟶ s = t (⊆ sources (flow cfs) s x)"
    proof (rule allI, rule impI)
      fix x :: vname
      assume "sec x ≤ l"
      moreover have "sources (flow cfs) s x ⊆ {y. sec y ≤ sec x}"
        by (rule subsetI, simp, rule sources_le)
      ultimately show "s = t (⊆ sources (flow cfs) s x)"
        using D by auto
    qed
    assume "∀s c1 c2 s1 s2 cfs.
      (c, s) →* (c1, s1) ∧ (c1, s1) →*{cfs} (c2, s2) ⟶
        (∀t1. ∃c2' t2. ∀x.
          s1 = t1 (⊆ sources (flow cfs) s1 x) ⟶
            (c1, t1) →* (c2', t2) ∧ (c2 = SKIP) = (c2' = SKIP) ∧
            s2 x = t2 x)"
    note F = this [rule_format]
    obtain t' where G: "∀x.
      s = t (⊆ sources (flow cfs) s x) ⟶
        (c, t) →* (SKIP, t') ∧ s' x = t' x"
      using F [of s c s cfs SKIP s' t] and C by blast
    assume H: "sec x ≤ l"
    {
      have "s = t (⊆ sources (flow cfs) s x)"
        using E and H by simp
      hence "(c, t) ⇒ t'"
        using G by (simp add: big_iff_small)
    }
    moreover {
      fix x :: vname
      assume "sec x ≤ l"
      hence "s = t (⊆ sources (flow cfs) s x)"
        using E by simp
      hence "s' x = t' x"
        using G by simp
    }
    ultimately have "∃t'. (c, t) ⇒ t' ∧ s' = t' (≤ l)"
      by auto
  }
  with A and B show ?thesis
    by (auto simp: correct_def secure_def split: if_split_asm)
qed


lemma ctyping2_sec_type_assign [elim]:
  assumes
    A: "(if ((∃s. s ∈ Univ? A X) ⟶ (∀y ∈ avars a. sec y ≤ sec x)) ∧
      (∀p ∈ U. ∀B Y. p = (B, Y) ⟶ B = {} ∨ (∀y ∈ Y. sec y ≤ sec x))
      then Some (if x ∈ {} ∧ A ≠ {}
        then if v ⊨ a (⊆ X)
          then ({s(x := aval a s) |s. s ∈ A}, insert x X) else (A, X - {x})
        else (A, Univ?? A X))
      else None) = Some (B, Y)"
      (is "(if (_ ⟶ ?P) ∧ ?Q then _ else _) = _") and
    B: "s ∈ A" and
    C: "finite (levels U)"
  shows "Max (levels U) ⊢ x ::= a"
proof -
  have "?P ∧ ?Q"
    using A and B by (auto simp: univ_states_if_def split: if_split_asm)
  moreover from this have "Max (levels U) ≤ sec x"
    using C by (subst Max_le_iff, auto simp: levels_def, blast)
  ultimately show "Max (levels U) ⊢ x ::= a"
    by (auto intro: Assign simp: avars_ub)
qed

lemma ctyping2_sec_type_seq:
  assumes
    A: "⋀B' s. B = B' ⟹ s ∈ A ⟹ Max (levels U) ⊢ c1" and
    B: "⋀B' B'' C Z s'. B = B' ⟹ B'' = B' ⟹
      (U, v) ⊨ c2 (⊆ B', Y) = Some (C, Z) ⟹
        s' ∈ B' ⟹ Max (levels U) ⊢ c2" and
    C: "(U, v) ⊨ c1 (⊆ A, X) = Some (B, Y)" and
    D: "(U, v) ⊨ c2 (⊆ B, Y) = Some (C, Z)" and
    E: "s ∈ A" and
    F: "cgood c1" and
    G: "csimp c1 = c1"
  shows "Max (levels U) ⊢ c1;; c2"
proof -
  have "Max (levels U) ⊢ c1"
    using A and E by simp
  moreover from C and E and F and G have "B ≠ {}"
    by (erule_tac csimp_ctyping2, blast)
  hence "Max (levels U) ⊢ c2"
    using B and D by blast
  ultimately show ?thesis ..
qed

lemma ctyping2_sec_type_if:
  assumes
    A: "⋀U' B C s. U' = insert (Univ? A X, bvars b) U ⟹
      B = B1 ⟹ C1 = C ⟹ s ∈ B1 ⟹
        finite (levels (insert (Univ? A X, bvars b) U)) ⟹
          Max (levels (insert (Univ? A X, bvars b) U)) ⊢ c1"
      (is "⋀_ _ _ _. _ = ?U' ⟹ _ ⟹ _ ⟹ _ ⟹ _ ⟹ _")
  assumes
    B: "⋀U' B C s. U' = ?U' ⟹ B = B1 ⟹ C2 = C ⟹ s ∈ B2 ⟹
      finite (levels ?U') ⟹ Max (levels ?U') ⊢ c2" and
    C: "⊨ b (⊆ A, X) = (B1, B2)" and
    D: "s ∈ A" and
    E: "bsimp b = b" and
    F: "∀v. b ≠ Bc v" and
    G: "finite (levels U)"
  shows "Max (levels U) ⊢ IF b THEN c1 ELSE c2"
proof -
  from D and G have H: "finite (levels ?U') ∧
    Max (levels ?U') = max (sec b) (Max (levels U))"
    using levels_insert by (auto simp: univ_states_if_def)
  moreover have I: "⊨ b (⊆ A, X) = (A, A)"
    using E and F by (rule bsimp_btyping2)
  hence "Max (levels ?U') ⊢ c1"
    using A and C and D and H by auto
  moreover have "Max (levels ?U') ⊢ c2"
    using B and C and D and H and I by auto
  ultimately show ?thesis
    by (auto intro: If)
qed

lemma ctyping2_sec_type_while:
  assumes
    A: "⋀B C' B' D' s. B = B1 ⟹ C' = C ⟹ B' = B1' ⟹
      ((∃s. s ∈ Univ? A X ∨ s ∈ Univ? C Y) ⟶
        (∀x ∈ bvars b. All ((≤) (sec x)))) ∧
      (∀p ∈ U. case p of (B, W) ⇒ (∃s. s ∈ B) ⟶
        (∀x ∈ W. All ((≤) (sec x)))) ⟹
        D = D' ⟹ s ∈ B1 ⟹ finite (levels {}) ⟹ Max (levels {}) ⊢ c"
      (is "⋀_ _ _ _ _. _ ⟹ _ ⟹ _ ⟹
        ?P ∧ (∀p ∈ _. case p of (_, W) ⇒ _ ⟶ ?Q W) ⟹
          _ ⟹ _ ⟹ _ ⟹ _")
  assumes
    B: "(if ?P ∧ (∀p ∈ U. ∀B W. p = (B, W) ⟶ B = {} ∨ ?Q W)
      then Some (B2 ∪ B2', Univ?? B2 X ∩ Y) else None) = Some (B, Z)"
      (is "(if ?R then _ else _) = _") and
    C: "⊨ b (⊆ A, X) = (B1, B2)" and
    D: "s ∈ A" and
    E: "bsimp b = b" and
    F: "b ≠ Bc False" and
    G: "b ≠ Bc True" and
    H: "finite (levels U)"
  shows "Max (levels U) ⊢ WHILE b DO c"
proof -
  have ?R
    using B by (simp split: if_split_asm)
  hence "sec b ≤ 0"
    using D by (subst bvars_ub, auto simp: univ_states_if_def, fastforce)
  moreover have "⊨ b (⊆ A, X) = (A, A)"
    using E and F and G by (blast intro: bsimp_btyping2)
  hence "0 ⊢ c"
    using A and C and D and `?R` by (fastforce simp: levels_def)
  moreover have "Max (levels U) = 0"
  proof (rule Max_eqI [OF H])
    fix l
    assume "l ∈ levels U"
    thus "l ≤ 0"
      using `?R` by (fastforce simp: levels_def)
  next
    show "0 ∈ levels U"
      by (simp add: levels_def)
  qed
  ultimately show ?thesis
    by (auto intro: While)
qed


theorem ctyping2_sec_type:
 "⟦(U, v) ⊨ c (⊆ A, X) = Some (B, Y);
    s ∈ A; cgood c; csimp c = c; finite (levels U)⟧ ⟹
  Max (levels U) ⊢ c"
proof (induction "(U, v)" c A X arbitrary: B Y U v s rule: ctyping2.induct)
  fix U
  show "Max (levels U) ⊢ SKIP"
    by (rule Skip)
next
  fix A X C Z U v c1 c2 s
  show
   "⟦⋀B Y s. (U, v) ⊨ c1 (⊆ A, X) = Some (B, Y) ⟹
      s ∈ A ⟹ cgood c1 ⟹ csimp c1 = c1 ⟹ finite (levels U) ⟹
      Max (levels U) ⊢ c1;
    ⋀p B Y C Z s. (U, v) ⊨ c1 (⊆ A, X) = Some p ⟹
      (B, Y) = p ⟹ (U, v) ⊨ c2 (⊆ B, Y) = Some (C, Z) ⟹
      s ∈ B ⟹ cgood c2 ⟹ csimp c2 = c2 ⟹ finite (levels U) ⟹
      Max (levels U) ⊢ c2;
    (U, v) ⊨ c1;; c2 (⊆ A, X) = Some (C, Z);
    s ∈ A; cgood (c1;; c2);
    csimp (c1;; c2) = c1;; c2;
    finite (levels U)⟧ ⟹
      Max (levels U) ⊢ c1;; c2"
    by (auto split: option.split_asm, rule ctyping2_sec_type_seq)
next
  fix A X B Y U v b c1 c2 s
  show
   "⟦⋀U' p B1 B2 C Y s.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B1, B2) = p ⟹ (U', v) ⊨ c1 (⊆ B1, X) = Some (C, Y) ⟹
      s ∈ B1 ⟹ cgood c1 ⟹ csimp c1 = c1 ⟹ finite (levels U') ⟹
      Max (levels U') ⊢ c1;
    ⋀U' p B1 B2 C Y s.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B1, B2) = p ⟹ (U', v) ⊨ c2 (⊆ B2, X) = Some (C, Y) ⟹
      s ∈ B2 ⟹ cgood c2 ⟹ csimp c2 = c2 ⟹ finite (levels U') ⟹
      Max (levels U') ⊢ c2;
    (U, v) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (B, Y);
    s ∈ A; cgood (IF b THEN c1 ELSE c2);
    csimp (IF b THEN c1 ELSE c2) = IF b THEN c1 ELSE c2;
    finite (levels U)⟧ ⟹
      Max (levels U) ⊢ IF b THEN c1 ELSE c2"
    by (auto split: option.split_asm prod.split_asm,
     rule ctyping2_sec_type_if)
next
  fix A X B Z U v b c s
  show
   "⟦⋀B1 B2 C Y B1' B2' D Z s.
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹
      (B1', B2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: sec ` W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B1, X) = Some (D, Z) ⟹
      s ∈ B1 ⟹ cgood c ⟹ csimp c = c ⟹ finite (levels {}) ⟹
      Max (levels {}) ⊢ c;
    ⋀B1 B2 C Y B1' B2' D' Z' s.
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹
      (B1', B2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: sec ` W ↝ UNIV ⟹
      ({}, False) ⊨ c (⊆ B1', Y) = Some (D', Z') ⟹
      s ∈ B1' ⟹ cgood c ⟹ csimp c = c ⟹ finite (levels {}) ⟹
      Max (levels {}) ⊢ c;
    (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Z);
    s ∈ A; cgood (WHILE b DO c);
    csimp (WHILE b DO c) = WHILE b DO c;
    finite (levels U)⟧ ⟹
      Max (levels U) ⊢ WHILE b DO c"
    by (auto split: option.split_asm prod.split_asm,
     rule ctyping2_sec_type_while)
qed (auto split: prod.split_asm)


lemma sec_type_ctyping2_if:
  assumes
    A: "⋀U' B1 B2. U' = insert (Univ? A X, bvars b) U ⟹
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
        Max (levels (insert (Univ? A X, bvars b) U)) ⊢ c1 ⟹
          finite (levels (insert (Univ? A X, bvars b) U)) ⟹
      ∃C Y. (insert (Univ? A X, bvars b) U, v) ⊨ c1 (⊆ B1, X) =
        Some (C, Y)"
      (is "⋀_ _ _. _ = ?U' ⟹ _ ⟹ _ ⟹ _ ⟹ _")
  assumes
    B: "⋀U' B1 B2. U' = ?U' ⟹ (B1, B2) = ⊨ b (⊆ A, X) ⟹
      Max (levels ?U') ⊢ c2 ⟹ finite (levels ?U') ⟹
        ∃C Y. (?U', v) ⊨ c2 (⊆ B2, X) = Some (C, Y)" and
    C: "finite (levels U)" and
    D: "max (sec b) (Max (levels U)) ⊢ c1" and
    E: "max (sec b) (Max (levels U)) ⊢ c2"
  shows "∃C Y. (U, v) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (C, Y)"
proof -
  obtain B1 B2 where F: "(B1, B2) = ⊨ b (⊆ A, X)"
    by (cases "⊨ b (⊆ A, X)", simp)
  moreover have "∃C1 C2 Y1 Y2. (?U', v) ⊨ c1 (⊆ B1, X) = Some (C1, Y1) ∧
    (?U', v) ⊨ c2 (⊆ B2, X) = Some (C2, Y2)"
  proof (cases "A = {}")
    case True
    hence "levels ?U' = levels U"
      by (auto simp: levels_def univ_states_if_def)
    moreover have "Max (levels U) ⊢ c1"
      using D by (auto intro: anti_mono)
    moreover have "Max (levels U) ⊢ c2"
      using E by (auto intro: anti_mono)
    ultimately show ?thesis
      using A and B and C and F by simp
  next
    case False
    with C have "finite (levels ?U') ∧
      Max (levels ?U') = max (sec b) (Max (levels U))"
      by (simp add: levels_insert univ_states_if_def)
    thus ?thesis
      using A and B and D and E and F by simp
  qed
  ultimately show ?thesis
    by (auto split: prod.split)
qed

lemma sec_type_ctyping2_while:
  assumes
    A: "⋀B1 B2 C Y B1' B2'. (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹ (B1', B2') = ⊨ b (⊆ C, Y) ⟹
        ((∃s. s ∈ Univ? A X ∨ s ∈ Univ? C Y) ⟶
          (∀x ∈ bvars b. All ((≤) (sec x)))) ∧
        (∀p ∈ U. case p of (B, W) ⇒ (∃s. s ∈ B) ⟶
          (∀x ∈ W. All ((≤) (sec x)))) ⟹
        Max (levels {}) ⊢ c ⟹ finite (levels {}) ⟹
          ∃D Z. ({}, False) ⊨ c (⊆ B1, X) = Some (D, Z)"
      (is "⋀_ _ C Y _ _. _ ⟹ _ ⟹ _ ⟹ ?P C Y ⟹ _ ⟹ _ ⟹ _")
  assumes
    B: "⋀B1 B2 C Y B1' B2'. (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹ (B1', B2') = ⊨ b (⊆ C, Y) ⟹
        ?P C Y ⟹ Max (levels {}) ⊢ c ⟹ finite (levels {}) ⟹
          ∃D Z. ({}, False) ⊨ c (⊆ B1', Y) = Some (D, Z)" and
    C: "finite (levels U)" and
    D: "Max (levels U) = 0" and
    E: "sec b = 0" and
    F: "0 ⊢ c"
  shows "∃B Y. (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Y)"
proof -
  obtain B1 B2 where G: "(B1, B2) = ⊨ b (⊆ A, X)"
    by (cases "⊨ b (⊆ A, X)", simp)
  moreover obtain C Y where H: "(C, Y) = ⊢ c (⊆ B1, X)"
    by (cases "⊢ c (⊆ B1, X)", simp)
  moreover obtain B1' B2' where I: "(B1', B2') = ⊨ b (⊆ C, Y)"
    by (cases "⊨ b (⊆ C, Y)", simp)
  moreover {
    fix l x s B W
    assume J: "(B, W) ∈ U" and K: "x ∈ W" and L: "s ∈ B"
    have "sec x ≤ l"
    proof (rule le_trans, rule Max_ge [OF C])
      show "sec x ∈ levels U"
        using J and K and L by (fastforce simp: levels_def)
    next
      show "Max (levels U) ≤ l"
        using D by simp
    qed
  }
  hence J: "?P C Y"
    using E by (auto dest: bvars_sec)
  ultimately have "∃D D' Z Z'. ({}, False) ⊨ c (⊆ B1, X) = Some (D, Z) ∧
    ({}, False) ⊨ c (⊆ B1', Y) = Some (D', Z')"
    using A and B and F by (force simp: levels_def)
  thus ?thesis
    using G and H and I and J by (auto split: prod.split)
qed


theorem sec_type_ctyping2:
 "⟦Max (levels U) ⊢ c; finite (levels U)⟧ ⟹
    ∃B Y. (U, v) ⊨ c (⊆ A, X) = Some (B, Y)"
proof (induction "(U, v)" c A X arbitrary: U v rule: ctyping2.induct)
  fix A X U v x a
  show "Max (levels U) ⊢ x ::= a ⟹ finite (levels U) ⟹
    ∃B Y. (U, v) ⊨ x ::= a (⊆ A, X) = Some (B, Y)"
    by (fastforce dest: avars_sec simp: levels_def)
next
  fix A X U v b c1 c2
  show
   "⟦⋀U' p B1 B2.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B1, B2) = p ⟹ Max (levels U') ⊢ c1 ⟹ finite (levels U') ⟹
      ∃B Y. (U', v) ⊨ c1 (⊆ B1, X) = Some (B, Y);
    ⋀U' p B1 B2.
      (U', p) = (insert (Univ? A X, bvars b) U, ⊨ b (⊆ A, X)) ⟹
      (B1, B2) = p ⟹ Max (levels U') ⊢ c2 ⟹ finite (levels U') ⟹
      ∃B Y. (U', v) ⊨ c2 (⊆ B2, X) = Some (B, Y);
    Max (levels U) ⊢ IF b THEN c1 ELSE c2; finite (levels U)⟧ ⟹
      ∃B Y. (U, v) ⊨ IF b THEN c1 ELSE c2 (⊆ A, X) = Some (B, Y)"
    by (auto simp del: ctyping2.simps(4), rule sec_type_ctyping2_if)
next
  fix A X U v b c
  show
   "⟦⋀B1 B2 C Y B1' B2'.
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹
      (B1', B2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: sec ` W ↝ UNIV ⟹
      Max (levels {}) ⊢ c ⟹ finite (levels {}) ⟹
      ∃B Z. ({}, False) ⊨ c (⊆ B1, X) = Some (B, Z);
    ⋀B1 B2 C Y B1' B2'.
      (B1, B2) = ⊨ b (⊆ A, X) ⟹
      (C, Y) = ⊢ c (⊆ B1, X) ⟹
      (B1', B2') = ⊨ b (⊆ C, Y) ⟹
      ∀(B, W) ∈ insert (Univ? A X ∪ Univ? C Y, bvars b) U.
        B: sec ` W ↝ UNIV ⟹
      Max (levels {}) ⊢ c ⟹ finite (levels {}) ⟹
      ∃B Z. ({}, False) ⊨ c (⊆ B1', Y) = Some (B, Z);
    Max (levels U) ⊢ WHILE b DO c; finite (levels U)⟧ ⟹
      ∃B Z. (U, v) ⊨ WHILE b DO c (⊆ A, X) = Some (B, Z)"
    by (auto simp del: ctyping2.simps(5), rule sec_type_ctyping2_while)
qed auto

end

end