Theory LocallySoundModeUse

(*
TiTitle: Value-Dependent SIFUM-Type-Systems
Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
(Based on the SIFUM-Type-Systems AFP entry, whose authors
 are: Sylvia Grewe, Heiko Mantel, Daniel Schoepe)
*)
section ‹Type System for Ensuring Locally Sound Use of Modes›

theory LocallySoundModeUse
imports Security Language
begin

subsection ‹Typing Rules›

locale sifum_modes = 
  sifum_lang_no_dma ev⇩A ev⇩B aexp_vars bexp_vars + sifum_security dma 𝒞_vars 𝒞 eval⇩w undefined
  for ev⇩A :: "('Var, 'Val) Mem ⇒ 'AExp ⇒ 'Val"
  and ev⇩B :: "('Var, 'Val) Mem ⇒ 'BExp ⇒ bool"
  and aexp_vars :: "'AExp ⇒ 'Var set"
  and bexp_vars :: "'BExp ⇒ 'Var set"
  and dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
  and 𝒞_vars :: "'Var ⇒ 'Var set"
  and 𝒞 :: "'Var set"

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 ∪ mds GuarNoReadOrWrite ; aexp_vars e ∩ mds GuarNoReadOrWrite = {};
             ∀v. (x ∈ 𝒞_vars v ⟶ v ∉ mds GuarNoWrite ∪ mds GuarNoReadOrWrite) ∧
                 (𝒞_vars v ∩ aexp_vars e ≠ {} ⟶ v ∉ mds GuarNoReadOrWrite)⟧ ⟹
  ⊢ mds { (x ← e) ⊗ annos } (mds ⊕ annos)" |
  if_: "⟦ ⊢ (mds ⊕ annos) { c⇩1 } mds'' ;
          ⊢ (mds ⊕ annos) { c⇩2 } mds'' ;
          bexp_vars e ∩ mds GuarNoReadOrWrite = {};
          ∀ v. 𝒞_vars v ∩ bexp_vars e ≠ {} ⟶ v ∉ mds GuarNoReadOrWrite⟧ ⟹
        ⊢ mds { If e c⇩1 c⇩2 ⊗ annos } mds''" |
  while: "⟦ mds' = mds ⊕ annos ; ⊢ mds' { c } mds' ; bexp_vars e ∩ mds' GuarNoReadOrWrite = {};
            ∀ v. 𝒞_vars v ∩ bexp_vars e ≠ {} ⟶ v ∉ mds' GuarNoReadOrWrite⟧ ⟹
  ⊢ 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_or_modify c x ⟹ doesnt_read_or_modify (c ⊗ annos) x"
  unfolding doesnt_read_or_modify_def doesnt_read_or_modify_vars_def
  apply clarify
  apply (induct annos)
   apply simp
   apply (metis (lifting))
  apply clarsimp
  apply (rule cxt_eval)
  apply (rule eval⇩w.decl)
  apply (metis cxt_eval eval⇩w.decl upd_elim)+
  done

lemma doesnt_modify_annos:
  "doesnt_modify c x ⟹ doesnt_modify (c ⊗ annos) x"
  unfolding doesnt_modify_def
  apply clarsimp
   apply (induct annos)
    apply simp 
   by (metis annotate.simps(2) 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_or_modify Stop x"
  unfolding doesnt_modify_def and doesnt_read_or_modify_def doesnt_read_or_modify_vars_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 clarsimp
    by metis+

lemma skip_doesnt_read:
  "doesnt_read_or_modify (Skip ⊗ annos) x"
  apply (rule doesnt_read_annos)
  apply (clarsimp simp: doesnt_read_or_modify_def doesnt_read_or_modify_vars_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 (clarsimp 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_or_modify 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_or_modify_def doesnt_read_or_modify_vars_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; x ∉ 𝒞_vars 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 dma_𝒞_vars)
  
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 clarsimp
  by (metis (lifting))

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 ≠ x; y ∉ aexp_vars e; x ∉ 𝒞_vars y; 𝒞_vars y ∩ aexp_vars e = {} ⟧ ⟹ doesnt_read_or_modify ((x ← e) ⊗ annos) y"
  apply (rule doesnt_read_annos)
proof -
  assume  "y ≠ x"
          "y ∉ aexp_vars e"
          "x ∉ 𝒞_vars y"
          "𝒞_vars y ∩ aexp_vars e = {}"
  thus "doesnt_read_or_modify (x ← e) y"
    unfolding doesnt_read_or_modify_def doesnt_read_or_modify_vars_def
    apply -
    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 clarify
     apply (rule conjI)
      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)
     apply clarify
     apply (rename_tac va v)
     apply (subgoal_tac "mem (x := ev⇩A mem e, va := v) = mem (va := v, x := ev⇩A mem e)")
      apply simp
      apply (rule cxt_eval)
      apply (rule eval⇩w.unannotated)
      apply (subgoal_tac "va ∉ aexp_vars e")
       apply (metis eval⇩w_simple.assign eval_vars_det⇩A fun_upd_apply)
      apply blast
     apply (metis mem_upd_commute)
    apply (metis assign_elim)
    done
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 ⟹ 𝒞_vars x ∩ bexp_vars e = {} ⟹ doesnt_read_or_modify (If e c⇩1 c⇩2 ⊗ annos) x"
  apply (rule doesnt_read_annos)
  apply (clarsimp simp: doesnt_read_or_modify_def doesnt_read_or_modify_vars_def, safe)
   apply (rename_tac mds mem c' mds' mem' v)
   apply (case_tac "ev⇩B mem e")
    apply (subgoal_tac "c' = c⇩1 ∧ mds' = mds ∧ mem' = mem")
     prefer 2
     apply auto[1]
    apply clarsimp
    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")
    prefer 2
    apply auto[1]
   apply clarsimp
   apply (rule cxt_eval)
   apply (rule eval⇩w.unannotated)
   apply (rule eval⇩w_simple.if_false)
   apply (metis (lifting) vars_eval⇩B)
  apply (rename_tac mds mem c' mds' mem' va v)
  apply (case_tac "ev⇩B mem e")
   apply (subgoal_tac "c' = c⇩1 ∧ mds' = mds ∧ mem' = mem")
    prefer 2
    apply auto[1]
   apply clarsimp
   apply (rule cxt_eval)
   apply (rule eval⇩w.unannotated)
   apply (rule eval⇩w_simple.if_true)
   apply (subgoal_tac "va ∉ bexp_vars e")
    apply (metis (lifting) vars_eval⇩B)
   apply blast
  apply (subgoal_tac "c' = c⇩2 ∧ mds' = mds ∧ mem' = mem")
   prefer 2
   apply auto[1]
  apply clarsimp
  apply (rule cxt_eval)
  apply (rule eval⇩w.unannotated)
  apply (rule eval⇩w_simple.if_false)
  apply (subgoal_tac "va ∉ bexp_vars e")
   apply (metis (lifting) vars_eval⇩B)
  apply blast
  done
  
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 blast
  using if_eval_false deterministic
  by blast

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_or_modify c x ⟧ ⟹ doesnt_read_or_modify (c ;; c') x"
  apply (clarsimp simp: doesnt_read_or_modify_def doesnt_read_or_modify_vars_def | safe)+
   apply (rename_tac mds mem c'a mds' mem' v)
   apply (case_tac "c = Stop")
    apply clarsimp
    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)
   apply (metis (lifting, no_types) eval⇩w.seq seq_elim)
  apply (rename_tac mds mem c'a mds' mem' va v)
  apply (case_tac "c = Stop")
   apply clarsimp
   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)
  apply (metis (lifting, no_types) eval⇩w.seq seq_elim)
  done
  
lemma seq_doesnt_modify:
  "⟦ doesnt_modify c x ⟧ ⟹ doesnt_modify (c ;; c') x"
  apply (clarsimp simp: doesnt_modify_def | safe)+
   apply (case_tac "c = Stop")
    apply clarsimp
    apply (metis (lifting) seq_stop_elim)
   apply (metis (no_types) seq_elim)
  apply (case_tac "c = Stop")
   apply clarsimp
   apply (metis (lifting) seq_stop_elim)
  apply (metis (no_types) seq_elim)
  done
  
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(34) Stmt.simps(42) 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(49))

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_or_modify (While e c ⊗ annos) x"
  unfolding doesnt_read_or_modify_def doesnt_read_or_modify_vars_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 ⟹ 𝒞_vars x ∩ bexp_vars e = {} ⟹ doesnt_read_or_modify (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 (clarsimp, intro conjI)
     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' GuarNoReadOrWrite ⟶ doesnt_read_or_modify c' y) ∧
          (y ∈ mds' GuarNoWrite ⟶ doesnt_modify c' y)"
    proof
      assume "c' = (x ← e) ⊗ annos ∧ mds' = mds⇩2"
      thus ?thesis
      proof (safe)
        assume nin: "y ∈ mds⇩2 GuarNoReadOrWrite"
        hence nin: "y ∈ mds GuarNoReadOrWrite"
          using assign.prems unfolding le_fun_def by blast
        hence "y ∉ aexp_vars e"
          by (metis IntD2 IntI assign.hyps(2) assign.prems empty_iff inf_apply le_iff_inf)
        moreover from nin assign.hyps(3) have "𝒞_vars y ∩ aexp_vars e = {}"
          by (meson contra_subsetD)
        moreover from nin assign.hyps have "x ∉ 𝒞_vars y ∧ x ≠ y"
          by blast
        ultimately show "doesnt_read_or_modify ((x ← e) ⊗ annos) y"
          using assign_doesnt_read
          by fastforce
      next
        assume "y ∈ mds⇩2 GuarNoWrite"
        hence nin: "y ∈ mds GuarNoWrite"
          using assign.prems unfolding le_fun_def by blast
        hence "x ≠ y ∧ x ∉ 𝒞_vars y"
          using assign by blast
        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 clarsimp
    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' GuarNoReadOrWrite ⟶ doesnt_read_or_modify 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 (safe)
        assume "x ∈ mds⇩2 GuarNoReadOrWrite"
        hence nin: "x ∈ mds GuarNoReadOrWrite"
          using if_ unfolding le_fun_def by auto
        with ‹bexp_vars e ∩ mds GuarNoReadOrWrite = {}› have "x ∉ bexp_vars e"
          by (metis IntD2 disjoint_iff_not_equal)
        moreover from if_(6) nin have "𝒞_vars x ∩ bexp_vars e = {}"
          by blast
        ultimately show "doesnt_read_or_modify (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 (safe)
    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) Stmt.distinct(43) annotate.elims update_annos.simps(1) while.hyps(1) while.prems while_loc_reach)
  next
    fix mem
    from while have a: "bexp_vars e ∩ (mds⇩2 ⊕ annos) GuarNoReadOrWrite = {}"
      by (metis (lifting, no_types) Int_empty_right Int_left_commute ‹mds⇩2 ⊕ annos ≤ mds ⊕ annos› inf_fun_def le_iff_inf)
    from while have b: "∀v.  𝒞_vars v ∩ bexp_vars e ≠ {} ⟶ v ∉ (mds⇩2 ⊕ annos) GuarNoReadOrWrite"
      by (meson ‹mds⇩2 ⊕ annos ≤ mds ⊕ annos› le_fun_def subsetCE)    
    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' GuarNoReadOrWrite ⟶ doesnt_read_or_modify c' x) ∧
                 (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)"
        apply (simp add: lc_def)
        apply (drule while_loc_reach)
        apply (rule allI)
        apply (erule disjE5)
      proof (clarsimp)
        fix x
        show "(x ∈ mds⇩2 GuarNoReadOrWrite ⟶ doesnt_read_or_modify (While e c ⊗ annos) x) ∧
              (x ∈ mds⇩2 GuarNoWrite ⟶ doesnt_modify (While e c ⊗ annos) x)"
          unfolding doesnt_read_or_modify_def doesnt_read_or_modify_vars_def and doesnt_modify_def
          using while_eval and while_eval_elim
          by blast
      next
        fix x
        assume a: "c' = Stmt.If e (c ;; While e c) Stop ∧ mds' ≤ mdsa"
        hence "mds' ≤ mdsa" by blast
        let ?c' = "If e (c ;; While e c) Stop"
        have "x ∈ mds' GuarNoReadOrWrite ⟶ doesnt_read_or_modify ?c' x"
          apply clarify
          apply (rule if_doesnt_read')
           apply (metis IntI ‹mds' ≤ mdsa› empty_iff le_fun_def rev_subsetD while.hyps(1) while.hyps(4))
          by (metis IntI ‹mds' ≤ mdsa› empty_iff le_fun_def rev_subsetD while.hyps(1) while.hyps(5))
        moreover
        have "x ∈ mds' GuarNoWrite ⟶ doesnt_modify ?c' x"
          by (metis annotate.simps(1) if_doesnt_modify)
        ultimately show "(x ∈ mds' GuarNoReadOrWrite ⟶ doesnt_read_or_modify c' x) ∧
                         (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)"
          using a by simp 
      next
        fix x
        assume "c' = Stop ∧ mds' ≤ mdsa"
        thus "(x ∈ mds' GuarNoReadOrWrite ⟶ doesnt_read_or_modify c' x) ∧
              (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)"
          by (simp, metis stop_doesnt_access)
      next
        fix x
        assume "∃c'' mem'' mds⇩3.
            c' = c'' ;; While e c ∧
            mds⇩3 ≤ mdsa ∧
            ⟨c'', mds', mem'⟩
            ∈ loc_reach ⟨c, mds⇩3, mem''⟩"
        from this obtain
         c'' mem'' mds⇩3
        where "mds⇩3 ≤ mdsa" and [simp]: "c' = c'' ;; While e c"
        and "⟨c'', mds', mem'⟩ ∈ loc_reach ⟨c, mds⇩3, mem''⟩" by blast
        thus "(x ∈ mds' GuarNoReadOrWrite ⟶ doesnt_read_or_modify c' x) ∧
              (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)"
          apply (clarsimp, safe)
           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 "c' = While e c ∧ mds' ≤ mdsa"
        thus "(x ∈ mds' GuarNoReadOrWrite ⟶ doesnt_read_or_modify c' x) ∧
              (x ∈ mds' GuarNoWrite ⟶ doesnt_modify c' x)"
          unfolding doesnt_read_or_modify_def doesnt_read_or_modify_vars_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 (safe)
    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 clarsimp
    by (metis (opaque_lifting, no_types) inf_absorb2 le_infI1)
qed

end

end