Theory LocallySoundModeUse

(*
Title: SIFUM-Type-Systems
Authors: Sylvia Grewe, Heiko Mantel, Daniel Schoepe
*)
section ‹Type System for Ensuring Locally Sound Use of Modes›

theory LocallySoundModeUse
imports Main Security Language
begin

subsection ‹Typing Rules›

locale sifum_modes = sifum_lang ev⇩A ev⇩B  +
  sifum_security dma Stop eval⇩w
  for ev⇩A :: "('Var, 'Val) Mem ⇒ 'AExp ⇒ 'Val"
  and ev⇩B :: "('Var, 'Val) Mem ⇒ 'BExp ⇒ bool"

context sifum_modes
begin

abbreviation eval_abv_modes :: "(_, 'Var, 'Val) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
  (infixl ‹↝› 70)
  where
  "x ↝ y ≡ (x, y) ∈ eval⇩w"

fun update_annos :: "'Var Mds ⇒ 'Var ModeUpd list ⇒ 'Var Mds"
(infix ‹⊕› 140)
  where
  "update_annos mds [] = mds" |
  "update_annos mds (a # as) = update_annos (update_modes a mds) as"

fun annotate :: "('Var, 'AExp, 'BExp) Stmt ⇒ 'Var ModeUpd list ⇒ ('Var, 'AExp, 'BExp) Stmt"
(infix ‹⊗› 140)
  where
  "annotate c [] = c" |
  "annotate c (a # as) = (annotate c as)@[a]"

inductive mode_type :: "'Var Mds ⇒
  ('Var, 'AExp, 'BExp) Stmt ⇒
  'Var Mds ⇒ bool" (‹⊢ _ { _ } _›)
  where
  skip: "⊢ mds { Skip ⊗ annos } (mds ⊕ annos)" |
  assign: "⟦ x ∉ mds GuarNoWrite ; aexp_vars e ∩ mds GuarNoRead = {} ⟧ ⟹
  ⊢ mds { (x ← e) ⊗ annos } (mds ⊕ annos)" |
  if_: "⟦ ⊢ (mds ⊕ annos) { c⇩1 } mds'' ;
          ⊢ (mds ⊕ annos) { c⇩2 } mds'' ;
          bexp_vars e ∩ mds GuarNoRead = {} ⟧ ⟹
        ⊢ mds { If e c⇩1 c⇩2 ⊗ annos } mds''" |
  while: "⟦ mds' = mds ⊕ annos ; ⊢ mds' { c } mds' ; bexp_vars e ∩ mds' GuarNoRead = {} ⟧ ⟹
  ⊢ mds { While e c ⊗ annos } mds'" |
  seq: "⟦ ⊢ mds { c⇩1 } mds' ; ⊢ mds' { c⇩2 } mds'' ⟧ ⟹ ⊢ mds { c⇩1 ;; c⇩2 } mds''" |
  sub: "⟦ ⊢ mds⇩2 { c } mds⇩2' ; mds⇩1 ≤ mds⇩2 ; mds⇩2' ≤ mds⇩1' ⟧ ⟹
  ⊢ mds⇩1 { c } mds⇩1'"

subsection ‹Soundness of the Type System›

(* Special case for evaluation with an empty context *)
lemma cxt_eval:
  "⟦ ⟨cxt_to_stmt [] c, mds, mem⟩ ↝ ⟨cxt_to_stmt [] c', mds', mem'⟩ ⟧ ⟹
  ⟨c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩"
  by auto

lemma update_preserves_le:
  "mds⇩1 ≤ mds⇩2 ⟹ (mds⇩1 ⊕ annos) ≤ (mds⇩2 ⊕ annos)"
proof (induct annos arbitrary: mds⇩1 mds⇩2)
  case Nil
  thus ?case by simp
next
  case (Cons a annos mds⇩1 mds⇩2)
  hence "update_modes a mds⇩1 ≤ update_modes a mds⇩2"
    by (case_tac a, auto simp: le_fun_def)
  with Cons show ?case
    by auto
qed

(* Annotations do not affect doesnt_read and doesnt_modify: *)
lemma doesnt_read_annos:
  "doesnt_read c x ⟹ doesnt_read (c ⊗ annos) x"
  unfolding doesnt_read_def
  apply clarify
  apply (induct annos)
   apply simp
   apply (metis (lifting))
  apply auto
  apply (rule cxt_eval)
  apply (rule eval⇩w.decl)
  by (metis cxt_eval eval⇩w.decl upd_elim)

lemma doesnt_modify_annos:
  "doesnt_modify c x ⟹ doesnt_modify (c ⊗ annos) x"
  unfolding doesnt_modify_def
  apply auto
  apply (induct annos)
   apply simp
  apply auto
  by (metis (lifting) upd_elim)

(* The following part contains some lemmas about evaluation of
   commands annotated using ⊗ and characterisations of loc_reach for
   commands. *)

lemma stop_loc_reach:
  "⟦ ⟨c', mds', mem'⟩ ∈ loc_reach ⟨Stop, mds, mem⟩ ⟧ ⟹
  c' = Stop ∧ mds' = mds"
  apply (induct rule: loc_reach.induct)
  by (auto simp: stop_no_eval)

lemma stop_doesnt_access:
  "doesnt_modify Stop x ∧ doesnt_read Stop x"
  unfolding doesnt_modify_def and doesnt_read_def
  using stop_no_eval
  by auto

lemma skip_eval_step:
  "⟨Skip ⊗ annos, mds, mem⟩ ↝ ⟨Stop, mds ⊕ annos, mem⟩"
  apply (induct annos arbitrary: mds)
   apply simp
   apply (metis cxt_to_stmt.simps(1) eval⇩w.unannotated eval⇩w_simple.skip)
  apply simp
  apply (insert eval⇩w.decl)
  apply (rule cxt_eval)
  apply (rule eval⇩w.decl)
  by auto

lemma skip_eval_elim:
  "⟦ ⟨Skip ⊗ annos, mds, mem⟩ ↝ ⟨c', mds', mem'⟩ ⟧ ⟹ c' = Stop ∧ mds' = mds ⊕ annos ∧ mem' = mem"
  apply (rule ccontr)
  apply (insert skip_eval_step deterministic)
  apply clarify
  apply auto
    by metis+

lemma skip_doesnt_read:
  "doesnt_read (Skip ⊗ annos) x"
  apply (rule doesnt_read_annos)
  apply (auto simp: doesnt_read_def)
  by (metis annotate.simps(1) skip_elim skip_eval_step)

lemma skip_doesnt_write:
  "doesnt_modify (Skip ⊗ annos) x"
  apply (rule doesnt_modify_annos)
  apply (auto simp: doesnt_modify_def)
  by (metis skip_elim)

lemma skip_loc_reach:
  "⟦ ⟨c', mds', mem'⟩ ∈ loc_reach ⟨Skip ⊗ annos, mds, mem⟩ ⟧ ⟹
  (c' = Stop ∧ mds' = (mds ⊕ annos)) ∨ (c' = Skip ⊗ annos ∧ mds' = mds)"
  apply (induct rule: loc_reach.induct)
    apply (metis fst_conv snd_conv)
   apply (metis skip_eval_elim stop_no_eval)
  by metis

lemma skip_doesnt_access:
  "⟦ lc ∈ loc_reach ⟨Skip ⊗ annos, mds, mem⟩ ; lc = ⟨c', mds', mem'⟩ ⟧ ⟹ doesnt_read c' x ∧ doesnt_modify c' x"
  apply (subgoal_tac "(c' = Stop ∧ mds' = (mds ⊕ annos)) ∨ (c' = Skip ⊗ annos ∧ mds' = mds)")
   apply (rule conjI, erule disjE)
     apply (simp add: doesnt_read_def stop_no_eval)
    apply (metis (lifting) annotate.simps skip_doesnt_read)
   apply (erule disjE)
    apply (simp add: doesnt_modify_def stop_no_eval)
   apply (metis (lifting) annotate.simps skip_doesnt_write)
  by (metis skip_loc_reach)

lemma assign_doesnt_modify:
  "⟦ x ≠ y ⟧ ⟹ doesnt_modify ((x ← e) ⊗ annos) y"
  apply (rule doesnt_modify_annos)
  apply (simp add: doesnt_modify_def)
  by (metis assign_elim fun_upd_apply)

lemma assign_annos_eval:
  "⟨(x ← e) ⊗ annos, mds, mem⟩ ↝ ⟨Stop, mds ⊕ annos, mem (x := ev⇩A mem e)⟩"
  apply (induct annos arbitrary: mds)
   apply (simp only: annotate.simps update_annos.simps)
   apply (rule cxt_eval)
   apply (rule eval⇩w.unannotated)
   apply (rule eval⇩w_simple.assign)
  apply (rule cxt_eval)
  apply (simp del: cxt_to_stmt.simps)
  apply (rule eval⇩w.decl)
  by auto

lemma assign_annos_eval_elim:
  "⟦ ⟨(x ← e) ⊗ annos, mds, mem⟩ ↝ ⟨c', mds', mem'⟩ ⟧ ⟹
  c' = Stop ∧ mds' = mds ⊕ annos"
  apply (rule ccontr)
  apply (insert deterministic assign_annos_eval)
  apply auto
   apply (metis (lifting))
  by metis

lemma mem_upd_commute:
  "⟦ x ≠ y ⟧ ⟹ mem (x := v⇩1, y := v⇩2) = mem (y := v⇩2, x := v⇩1)"
  by (metis fun_upd_twist)

lemma assign_doesnt_read:
  "⟦ y ∉ aexp_vars e ⟧ ⟹ doesnt_read ((x ← e) ⊗ annos) y"
  apply (rule doesnt_read_annos)
proof (cases "x = y")
  assume "y ∉ aexp_vars e"
    and [simp]: "x = y"
  show "doesnt_read (x ← e) y"
    unfolding doesnt_read_def
    apply (rule allI)+
    apply (rename_tac mds mem c' mds' mem')
    apply (rule impI)
    apply (subgoal_tac "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)")
     apply simp
     apply (rule disjI2)
     apply clarify
     apply (rule cxt_eval)
     apply (rule eval⇩w.unannotated)
     apply simp
     apply (metis (opaque_lifting, no_types) ‹x = y› ‹y ∉ aexp_vars e› eval⇩w_simple.assign eval_vars_det⇩A fun_upd_apply fun_upd_upd)
    by (metis assign_elim)
next
  assume asms: "y ∉ aexp_vars e" "x ≠ y"
  show "doesnt_read (x ← e) y"
    unfolding doesnt_read_def
    apply (rule allI)+
    apply (rename_tac mds mem c' mds' mem')
    apply (rule impI)
    apply (subgoal_tac "c' = Stop ∧ mds' = mds ∧ mem' = mem (x := ev⇩A mem e)")
     apply simp
     apply (rule disjI1)
     apply (insert asms)
     apply clarify
     apply (subgoal_tac "mem (x := ev⇩A mem e, y := v) = mem (y := v, x := ev⇩A mem e)")
      apply simp
      apply (rule cxt_eval)
      apply (rule eval⇩w.unannotated)
      apply (metis eval⇩w_simple.assign eval_vars_det⇩A fun_upd_apply)
     apply (metis mem_upd_commute)
    by (metis assign_elim)
qed

lemma assign_loc_reach:
  "⟦ ⟨c', mds', mem'⟩ ∈ loc_reach ⟨(x ← e) ⊗ annos, mds, mem⟩ ⟧ ⟹
  (c' = Stop ∧ mds' = (mds ⊕ annos)) ∨ (c' = (x ← e) ⊗ annos ∧ mds' = mds)"
  apply (induct rule: loc_reach.induct)
    apply simp_all
  by (metis assign_annos_eval_elim stop_no_eval)

lemma if_doesnt_modify:
  "doesnt_modify (If e c⇩1 c⇩2 ⊗ annos) x"
  apply (rule doesnt_modify_annos)
  by (auto simp: doesnt_modify_def)

lemma vars_eval⇩B:
  "x ∉ bexp_vars e ⟹ ev⇩B mem e = ev⇩B (mem (x := v)) e"
  by (metis (lifting) eval_vars_det⇩B fun_upd_other)

lemma if_doesnt_read:
  "x ∉ bexp_vars e ⟹ doesnt_read (If e c⇩1 c⇩2 ⊗ annos) x"
  apply (rule doesnt_read_annos)
  apply (auto simp: doesnt_read_def)
  apply (rename_tac mds mem c' mds' mem' v va)
  apply (case_tac "ev⇩B mem e")
   apply (subgoal_tac "c' = c⇩1 ∧ mds' = mds ∧ mem' = mem")
    apply auto
   apply (rule cxt_eval)
   apply (rule eval⇩w.unannotated)
   apply (rule eval⇩w_simple.if_true)
   apply (metis (lifting) vars_eval⇩B)
  apply (subgoal_tac "c' = c⇩2 ∧ mds' = mds ∧ mem' = mem")
   apply auto
  apply (rule cxt_eval)
  apply (rule eval⇩w.unannotated)
  apply (rule eval⇩w_simple.if_false)
  by (metis (lifting) vars_eval⇩B)

lemma if_eval_true:
  "⟦ ev⇩B mem e ⟧ ⟹
  ⟨If e c⇩1 c⇩2 ⊗ annos, mds, mem⟩ ↝ ⟨c⇩1, mds ⊕ annos, mem⟩"
  apply (induct annos arbitrary: mds)
   apply simp
   apply (metis cxt_eval eval⇩w.unannotated eval⇩w_simple.if_true)
  by (metis annotate.simps(2) cxt_eval eval⇩w.decl update_annos.simps(2))

lemma if_eval_false:
  "⟦ ¬ ev⇩B mem e ⟧ ⟹
  ⟨If e c⇩1 c⇩2 ⊗ annos, mds, mem⟩ ↝ ⟨c⇩2, mds ⊕ annos, mem⟩"
  apply (induct annos arbitrary: mds)
   apply simp
   apply (metis cxt_eval eval⇩w.unannotated eval⇩w_simple.if_false)
  by (metis annotate.simps(2) cxt_eval eval⇩w.decl update_annos.simps(2))

lemma if_eval_elim:
  "⟦ ⟨If e c⇩1 c⇩2 ⊗ annos, mds, mem⟩ ↝ ⟨c', mds', mem'⟩ ⟧ ⟹
  ((c' = c⇩1 ∧ ev⇩B mem e) ∨ (c' = c⇩2 ∧ ¬ ev⇩B mem e)) ∧ mds' = mds ⊕ annos ∧ mem' = mem"
  apply (rule ccontr)
  apply (cases "ev⇩B mem e")
   apply (insert if_eval_true deterministic)
   apply (metis prod.inject)
  by (metis prod.inject if_eval_false deterministic)

lemma if_eval_elim':
  "⟦ ⟨If e c⇩1 c⇩2, mds, mem⟩ ↝ ⟨c', mds', mem'⟩ ⟧ ⟹
  ((c' = c⇩1 ∧ ev⇩B mem e) ∨ (c' = c⇩2 ∧ ¬ ev⇩B mem e)) ∧ mds' = mds ∧ mem' = mem"
  using if_eval_elim [where annos = "[]"]
  by auto

lemma loc_reach_refl':
  "⟨c, mds, mem⟩ ∈ loc_reach ⟨c, mds, mem⟩"
  apply (subgoal_tac "∃ lc. lc ∈ loc_reach lc ∧ lc = ⟨c, mds, mem⟩")
   apply blast
  by (metis loc_reach.refl fst_conv snd_conv)

lemma if_loc_reach:
  "⟦ ⟨c', mds', mem'⟩ ∈ loc_reach ⟨If e c⇩1 c⇩2 ⊗ annos, mds, mem⟩ ⟧ ⟹
  (c' = If e c⇩1 c⇩2 ⊗ annos ∧ mds' = mds) ∨
  (∃ mem''. ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩1, mds ⊕ annos, mem''⟩) ∨
  (∃ mem''. ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩2, mds ⊕ annos, mem''⟩)"
  apply (induct rule: loc_reach.induct)
    apply (metis fst_conv snd_conv)
   apply (erule disjE)
    apply (erule conjE)
    apply simp
    apply (drule if_eval_elim)
    apply (erule conjE)+
    apply (erule disjE)
     apply (erule conjE)
     apply simp
     apply (metis loc_reach_refl')
    apply (metis loc_reach_refl')
   apply (metis loc_reach.step)
  by (metis loc_reach.mem_diff)

lemma if_loc_reach':
  "⟦ ⟨c', mds', mem'⟩ ∈ loc_reach ⟨If e c⇩1 c⇩2, mds, mem⟩ ⟧ ⟹
  (c' = If e c⇩1 c⇩2 ∧ mds' = mds) ∨
  (∃ mem''. ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩1, mds, mem''⟩) ∨
  (∃ mem''. ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩2, mds, mem''⟩)"
  using if_loc_reach [where annos = "[]"]
  by simp

lemma seq_loc_reach:
  "⟦ ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩1 ;; c⇩2, mds, mem⟩ ⟧ ⟹
  (∃ c''. c' = c'' ;; c⇩2 ∧ ⟨c'', mds', mem'⟩ ∈ loc_reach ⟨c⇩1, mds, mem⟩) ∨
  (∃ c'' mds'' mem''. ⟨Stop, mds'', mem''⟩ ∈ loc_reach ⟨c⇩1, mds, mem⟩ ∧ 
                      ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩2, mds'', mem''⟩)"
  apply (induct rule: loc_reach.induct)
    apply simp
    apply (metis  loc_reach_refl')
   apply simp
   apply (metis (no_types) loc_reach.step loc_reach_refl' seq_elim seq_stop_elim)
  by (metis (lifting) loc_reach.mem_diff)

lemma seq_doesnt_read:
  "⟦ doesnt_read c x ⟧ ⟹ doesnt_read (c ;; c') x"
  apply (auto simp: doesnt_read_def)
  apply (rename_tac mds mem c'a mds' mem' v va)
  apply (case_tac "c = Stop")
   apply auto
   apply (subgoal_tac "c'a = c' ∧ mds' = mds ∧ mem' = mem")
    apply simp
    apply (metis cxt_eval eval⇩w.unannotated eval⇩w_simple.seq_stop)
   apply (metis (lifting) seq_stop_elim)
  by (metis (lifting, no_types) eval⇩w.seq seq_elim)

lemma seq_doesnt_modify:
  "⟦ doesnt_modify c x ⟧ ⟹ doesnt_modify (c ;; c') x"
  apply (auto simp: doesnt_modify_def)
  apply (case_tac "c = Stop")
   apply auto
   apply (metis (lifting) seq_stop_elim)
  by (metis (no_types) seq_elim)

inductive_cases seq_stop_elim': "⟨Stop ;; c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩"

lemma seq_stop_elim: "⟨Stop ;; c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩ ⟹
  c' = c ∧ mds' = mds ∧ mem' = mem"
  apply (erule seq_stop_elim')
    apply (metis eval⇩w.unannotated seq_stop_elim)
   apply (metis eval⇩w.seq seq_stop_elim)
  by (metis (lifting) Stmt.simps(28) Stmt.simps(34) cxt_seq_elim)

lemma seq_split:
  "⟦ ⟨Stop, mds', mem'⟩ ∈ loc_reach ⟨c⇩1 ;; c⇩2, mds, mem⟩ ⟧ ⟹
  ∃ mds'' mem''. ⟨Stop, mds'', mem''⟩ ∈ loc_reach ⟨c⇩1, mds, mem⟩ ∧
                 ⟨Stop, mds', mem'⟩ ∈ loc_reach ⟨c⇩2, mds'', mem''⟩"
  apply (drule seq_loc_reach)
  by (metis Stmt.simps(41))

lemma while_eval:
  "⟨While e c ⊗ annos, mds, mem⟩ ↝ ⟨(If e (c ;; While e c) Stop), mds ⊕ annos, mem⟩"
  apply (induct annos arbitrary: mds)
   apply simp
   apply (rule cxt_eval)
   apply (rule eval⇩w.unannotated)
   apply (metis (lifting) eval⇩w_simple.while)
  apply simp
  by (metis cxt_eval eval⇩w.decl)

lemma while_eval':
  "⟨While e c, mds, mem⟩ ↝ ⟨If e (c ;; While e c) Stop, mds, mem⟩"
  using while_eval [where annos = "[]"]
  by auto

lemma while_eval_elim:
  "⟦ ⟨While e c ⊗ annos, mds, mem⟩ ↝ ⟨c', mds', mem'⟩ ⟧ ⟹
   (c' = If e (c ;; While e c) Stop ∧ mds' = mds ⊕ annos ∧ mem' = mem)"
  apply (rule ccontr)
  apply (insert while_eval deterministic)
  by blast

lemma while_eval_elim':
  "⟦ ⟨While e c, mds, mem⟩ ↝ ⟨c', mds', mem'⟩ ⟧ ⟹
   (c' = If e (c ;; While e c) Stop ∧ mds' = mds ∧ mem' = mem)"
  using while_eval_elim [where annos = "[]"]
  by auto

lemma while_doesnt_read:
  "⟦ x ∉ bexp_vars e ⟧ ⟹ doesnt_read (While e c ⊗ annos) x"
  unfolding doesnt_read_def
  using while_eval while_eval_elim
  by metis

lemma while_doesnt_modify:
  "doesnt_modify (While e c ⊗ annos) x"
  unfolding doesnt_modify_def
  using while_eval_elim
  by metis

(* TODO: try to find a better solution to this: *)
lemma disjE3:
  "⟦ A ∨ B ∨ C ; A ⟹ P ; B ⟹ P ; C ⟹ P ⟧ ⟹ P"
  by auto

lemma disjE5:
  "⟦ A ∨ B ∨ C ∨ D ∨ E ; A ⟹ P ; B ⟹ P ; C ⟹ P ; D ⟹ P ; E ⟹ P ⟧ ⟹ P"
  by auto

lemma if_doesnt_read':
  "x ∉ bexp_vars e ⟹ doesnt_read (If e c⇩1 c⇩2) x"
  using if_doesnt_read [where annos = "[]"]
  by auto

theorem mode_type_sound:
  assumes typeable: "⊢ mds⇩1 { c } mds⇩1'"
  assumes mode_le: "mds⇩2 ≤ mds⇩1"
  shows "∀ mem. (⟨Stop, mds⇩2', mem'⟩ ∈ loc_reach ⟨c, mds⇩2, mem⟩ ⟶ mds⇩2' ≤ mds⇩1') ∧ 
                locally_sound_mode_use ⟨c, mds⇩2, mem⟩"
  using typeable mode_le
proof (induct arbitrary: mds⇩2 mds⇩2' mem' mem rule: mode_type.induct)
  case (skip mds annos)
  thus ?case
    apply auto
     apply (metis (lifting) skip_eval_step skip_loc_reach stop_no_eval update_preserves_le)
    apply (simp add: locally_sound_mode_use_def)
    by (metis annotate.simps skip_doesnt_access)
next
  case (assign x mds e annos)
  hence "∀ mem. locally_sound_mode_use ⟨(x ← e) ⊗ annos, mds⇩2, mem⟩"
    unfolding locally_sound_mode_use_def
  proof (clarify)
    fix mem c' mds' mem' y
    assume asm: "⟨c', mds', mem'⟩ ∈ loc_reach ⟨(x ← e) ⊗ annos, mds⇩2, mem⟩"
    hence "c' = (x ← e) ⊗ annos ∧ mds' = mds⇩2 ∨ c' = Stop ∧ mds' = mds⇩2 ⊕ annos"
      using assign_loc_reach by blast
    thus "(y ∈ mds' GuarNoRead ⟶ doesnt_read c' y) ∧
          (y ∈ mds' GuarNoWrite ⟶ doesnt_modify c' y)"
    proof
      assume "c' = (x ← e) ⊗ annos ∧ mds' = mds⇩2"
      thus ?thesis
      proof (auto)
        assume "y ∈ mds⇩2 GuarNoRead"
        hence "y ∉ aexp_vars e"
          by (metis IntD2 IntI assign.hyps(2) assign.prems empty_iff inf_apply le_iff_inf)
        with assign_doesnt_read show "doesnt_read ((x ← e) ⊗ annos) y"
          by blast
      next
        assume "y ∈ mds⇩2 GuarNoWrite"
        hence "x ≠ y"
          by (metis assign.hyps(1) assign.prems in_mono le_fun_def)
        with assign_doesnt_modify show "doesnt_modify ((x ← e) ⊗ annos) y"
          by blast
      qed
    next
      assume "c' = Stop ∧ mds' = mds⇩2 ⊕ annos"
      with stop_doesnt_access show ?thesis by blast
    qed
  qed
  thus ?case
    apply auto
    by (metis assign.prems assign_annos_eval assign_loc_reach stop_no_eval update_preserves_le)
next
  case (if_ mds annos c⇩1 mds'' c⇩2 e)
    let ?c = "(If e c⇩1 c⇩2) ⊗ annos"
  from if_ have modes_le': "mds⇩2 ⊕ annos ≤ mds ⊕ annos"
    by (metis (lifting) update_preserves_le)
  from if_ show ?case
    apply (simp add: locally_sound_mode_use_def)
    apply clarify
    apply (rule conjI)
     apply clarify
     prefer 2
     apply clarify
  proof -
    fix mem
    assume "⟨Stop, mds⇩2', mem'⟩ ∈ loc_reach ⟨If e c⇩1 c⇩2 ⊗ annos, mds⇩2, mem⟩"
    with modes_le' and if_ show "mds⇩2' ≤ mds''"
      by (metis if_eval_false if_eval_true if_loc_reach stop_no_eval)
  next
    fix mem c' mds' mem' x
    assume "⟨c', mds', mem'⟩ ∈ loc_reach ⟨If e c⇩1 c⇩2 ⊗ annos, mds⇩2, mem⟩"
    hence "(c' = If e c⇩1 c⇩2 ⊗ annos ∧ mds' = mds⇩2) ∨
           (∃ mem''. ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩1, mds⇩2 ⊕ annos, mem''⟩) ∨
           (∃ mem''. ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩2, mds⇩2 ⊕ annos, mem''⟩)"
      using if_loc_reach by blast
    thus "(x ∈ mds' GuarNoRead ⟶ doesnt_read c' x) ∧
          (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)"
    proof
      assume "c' = If e c⇩1 c⇩2 ⊗ annos ∧ mds' = mds⇩2"
      thus ?thesis
      proof (auto)
        assume "x ∈ mds⇩2 GuarNoRead"
        with ‹bexp_vars e ∩ mds GuarNoRead = {}› and ‹mds⇩2 ≤ mds› have "x ∉ bexp_vars e"
          by (metis IntD2 disjoint_iff_not_equal inf_fun_def le_iff_inf)
        thus "doesnt_read (If e c⇩1 c⇩2 ⊗ annos) x"
          using if_doesnt_read by blast
      next
        assume "x ∈ mds⇩2 GuarNoWrite"
        thus "doesnt_modify (If e c⇩1 c⇩2 ⊗ annos) x"
          using if_doesnt_modify by blast
      qed
    next
      assume "(∃mem''. ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩1, mds⇩2 ⊕ annos, mem''⟩) ∨
              (∃mem''. ⟨c', mds', mem'⟩ ∈ loc_reach ⟨c⇩2, mds⇩2 ⊕ annos, mem''⟩)"
      with if_ show ?thesis
        by (metis locally_sound_mode_use_def modes_le')
    qed
  qed
next
  case (while mdsa mds annos c e)
  hence "mds⇩2 ⊕ annos ≤ mds ⊕ annos"
    by (metis (lifting) update_preserves_le)
  have while_loc_reach: "⋀ c' mds' mem' mem.
  ⟨c', mds', mem'⟩ ∈ loc_reach ⟨While e c ⊗ annos, mds⇩2, mem⟩ ⟹
  c' = While e c ⊗ annos ∧ mds' = mds⇩2 ∨
  c' = While e c ∧ mds' ≤ mdsa ∨
  c' = Stmt.If e (c ;; While e c) Stop ∧ mds' ≤ mdsa ∨
  c' = Stop ∧ mds' ≤ mdsa ∨
  (∃c'' mem'' mds⇩3.
      c' = c'' ;; While e c ∧
      mds⇩3 ≤ mdsa ∧ ⟨c'', mds', mem'⟩ ∈ loc_reach ⟨c, mds⇩3, mem''⟩)"
  proof -
    fix mem c' mds' mem'
    assume "⟨c', mds', mem'⟩ ∈ loc_reach ⟨While e c ⊗ annos, mds⇩2, mem⟩"
    thus "?thesis c' mds' mem' mem"
      apply (induct rule: loc_reach.induct)
        apply simp_all
       apply (erule disjE)
        apply simp
        apply (metis ‹mds⇩2 ⊕ annos ≤ mds ⊕ annos› while.hyps(1) while_eval_elim)
       apply (erule disjE)
        apply (metis while_eval_elim')
       apply (erule disjE)
        apply simp
        apply (metis if_eval_elim' loc_reach_refl')
       apply (erule disjE)
        apply (metis stop_no_eval)
       apply (erule exE)
       apply (rename_tac c' mds' mem' c'' mds'' mem'' c''a)
       apply (case_tac "c''a = Stop")
        apply (insert while.hyps(3))
        apply (metis seq_stop_elim while.hyps(3))
       apply (metis loc_reach.step seq_elim)
      by (metis (full_types) loc_reach.mem_diff)
  qed
  from while show ?case
  proof (auto)
    fix mem
    assume "⟨Stop, mds⇩2', mem'⟩ ∈ loc_reach ⟨While e c ⊗ annos, mds⇩2, mem⟩"
    thus "mds⇩2' ≤ mds ⊕ annos"
      by (metis Stmt.distinct(35) stop_no_eval while.hyps(1) while_eval while_loc_reach)
  next
    fix mem
    from while have "bexp_vars e ∩ (mds⇩2 ⊕ annos) GuarNoRead = {}"
      by (metis (lifting, no_types) Int_empty_right Int_left_commute ‹mds⇩2 ⊕ annos ≤ mds ⊕ annos› inf_fun_def le_iff_inf)
    show "locally_sound_mode_use ⟨While e c ⊗ annos, mds⇩2, mem⟩"
      unfolding locally_sound_mode_use_def
      apply (rule allI)+
      apply (rule impI)
    proof -
      fix c' mds' mem'
      define lc where "lc = ⟨While e c ⊗ annos, mds⇩2, mem⟩"
      assume "⟨c', mds', mem'⟩ ∈ loc_reach lc"
      thus "∀ x. (x ∈ mds' GuarNoRead ⟶ doesnt_read c' x) ∧
                 (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)"
        apply (simp add: lc_def)
        apply (drule while_loc_reach)
        apply (erule disjE5)
      proof (auto del: conjI)
        fix x
        show "(x ∈ mds⇩2 GuarNoRead ⟶ doesnt_read (While e c ⊗ annos) x) ∧
              (x ∈ mds⇩2 GuarNoWrite ⟶ doesnt_modify (While e c ⊗ annos) x)"
          unfolding doesnt_read_def and doesnt_modify_def
          using while_eval and while_eval_elim
          by blast
      next
        fix x
        assume "mds' ≤ mdsa"
        let ?c' = "If e (c ;; While e c) Stop"
        have "x ∈ mds' GuarNoRead ⟶ doesnt_read ?c' x"
          apply clarify
          apply (rule if_doesnt_read')
          by (metis IntI ‹mds' ≤ mdsa› empty_iff le_fun_def rev_subsetD while.hyps(1) while.hyps(4))
        moreover
        have "x ∈ mds' GuarNoWrite ⟶ doesnt_modify ?c' x"
          by (metis annotate.simps(1) if_doesnt_modify)
        ultimately show "(x ∈ mds' GuarNoRead ⟶ doesnt_read ?c' x) ∧
                         (x ∈ mds' GuarNoWrite ⟶ doesnt_modify ?c' x)" ..
      next
        fix x
        assume "mds' ≤ mdsa"
        show "(x ∈ mds' GuarNoRead ⟶ doesnt_read Stop x) ∧
              (x ∈ mds' GuarNoWrite ⟶ doesnt_modify Stop x)"
          by (metis stop_doesnt_access)
      next
        fix c'' x mem'' mds⇩3
        assume "mds⇩3 ≤ mdsa"
        assume "⟨c'', mds', mem'⟩ ∈ loc_reach ⟨c, mds⇩3, mem''⟩"
        thus "(x ∈ mds' GuarNoRead ⟶ doesnt_read (c'' ;; While e c) x) ∧
              (x ∈ mds' GuarNoWrite ⟶ doesnt_modify (c'' ;; While e c) x)"
          apply auto
           apply (rule seq_doesnt_read)
           apply (insert while(3))
           apply (metis ‹mds⇩3 ≤ mdsa› locally_sound_mode_use_def while.hyps(1))
          apply (rule seq_doesnt_modify)
          by (metis ‹mds⇩3 ≤ mdsa› locally_sound_mode_use_def while.hyps(1))
      next
        fix x
        assume "mds' ≤ mdsa"
        show "(x ∈ mds' GuarNoRead ⟶ doesnt_read (While e c) x) ∧
              (x ∈ mds' GuarNoWrite ⟶ doesnt_modify (While e c) x)"
          unfolding doesnt_read_def and doesnt_modify_def
          using while_eval' and while_eval_elim'
          by blast
      qed
    qed
  qed
next
  case (seq mds c⇩1 mds' c⇩2 mds'')
  thus ?case
  proof (auto)
    fix mem
    assume "⟨Stop, mds⇩2', mem'⟩ ∈ loc_reach ⟨c⇩1 ;; c⇩2, mds⇩2, mem⟩"
    then obtain mds⇩2'' mem'' where "⟨Stop, mds⇩2'', mem''⟩ ∈ loc_reach ⟨c⇩1, mds⇩2, mem⟩" and
      "⟨Stop, mds⇩2', mem'⟩ ∈ loc_reach ⟨c⇩2, mds⇩2'', mem''⟩"
      using seq_split by blast
    thus "mds⇩2' ≤ mds''"
      using seq by blast
  next
    fix mem
    from seq show "locally_sound_mode_use ⟨c⇩1 ;; c⇩2, mds⇩2, mem⟩"
      apply (simp add: locally_sound_mode_use_def)
      apply clarify
      apply (drule seq_loc_reach)
      apply (erule disjE)
       apply (metis seq_doesnt_modify seq_doesnt_read)
      by metis
  qed
next
  case (sub mds⇩2'' c mds⇩2' mds⇩1 mds⇩1' c⇩1)
  thus ?case
    apply auto
    by (metis (opaque_lifting, no_types) inf_absorb2 le_infI1)
qed

end

end