Theory CompositionalRefinement

(*
Title: Value-Dependent SIFUM Refinement
Authors: Toby Murray, Robert Sison
*)
theory CompositionalRefinement
imports Dependent_SIFUM_Type_Systems.Compositionality
begin


lemma inj_card_le: 
  "inj (f::'a ⇒ 'b) ⟹ finite (UNIV::'b set) ⟹ card (UNIV::'a set) ≤ card (UNIV::'b set)"
  by (blast intro: card_inj_on_le)

text ‹
  We define a generic locale for capturing refinement between an abstract and a concrete
  program. We then define and prove sufficient, conditions that preserve local security
  from the abstract to the concrete program.

  Below we define a second locale that is more restrictive than this one. Specifically, this
  one allows the concrete program to have extra variables not present in the abstract one.
  These variables might be used, for instance, to implement a runtime stack that was implicit
  in the semantics of the abstract program; or as temporary storage for expression evaluation
  that may (appear to be) atomic in the abstract semantics.

  The simpler locale below forbids extra variables in the concrete program, making the
  necessary conditions for preservation of local security simpler.
›
locale sifum_refinement = 
  abs: sifum_security dmaA 𝒞_varsA 𝒞A evalA some_val +
  conc: sifum_security dmaC 𝒞_varsC 𝒞C evalC some_val
  for dmaA :: "('VarA,'Val) Mem ⇒ 'VarA ⇒ Sec"
  and dmaC :: "('VarC,'Val) Mem ⇒ 'VarC ⇒ Sec"
  and 𝒞_varsA :: "'VarA ⇒ 'VarA set"
  and 𝒞_varsC :: "'VarC ⇒ 'VarC set"
  and 𝒞A :: "'VarA set"
  and 𝒞C :: "'VarC set"
  and evalA :: "('ComA, 'VarA, 'Val) LocalConf rel"
  and evalC :: "('ComC, 'VarC, 'Val) LocalConf rel"
  and some_val :: "'Val" +
  fixes varC_of :: "'VarA ⇒ 'VarC"
  assumes varC_of_inj: "inj varC_of" 
  assumes dma_consistent:
    "dmaA (λxA. memC (varC_of xA)) xA = dmaC memC (varC_of xA)"
  assumes 𝒞_vars_consistent:
    "(varC_of ` 𝒞_varsA xA) = 𝒞_varsC (varC_of xA)"
  (* we make the (reasonable IMHO) assumption that the only control variables
     are user-declared and so that the compiler won't introduce new ones. *)
  assumes control_vars_are_A_vars:
    "𝒞C = varC_of ` 𝒞A"

section "General Compositional Refinement"

text ‹
  The type of state relations between the abstract and compiled components.
  The job of a certifying compiler will be to exhibit one of these for each
  component it compiles. Below we'll define the conditions that such a
  relation needs to satisfy to give compositional refinement.
›
type_synonym ('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation = 
   "(('ComA, 'VarA, 'Val) LocalConf × ('ComC, 'VarC, 'Val) LocalConf) set"

context sifum_refinement begin

abbreviation 
  conf_abvA :: "'ComA ⇒ 'VarA Mds ⇒ ('VarA, 'Val) Mem ⇒ (_,_,_) LocalConf"
  ("⟨_, _, _⟩A" [0, 0, 0] 1000)
where
  "⟨ c, mds, mem ⟩A ≡ ((c, mds), mem)"

abbreviation 
  conf_abvC :: "'ComC ⇒ 'VarC Mds ⇒ ('VarC, 'Val) Mem ⇒ (_,_,_) LocalConf"
  ("⟨_, _, _⟩C" [0, 0, 0] 1000)
where
  "⟨ c, mds, mem ⟩C ≡ ((c, mds), mem)"

abbreviation 
  eval_abvA :: "('ComA, 'VarA, 'Val) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
  (infixl "↝A" 70)
 where
  "x ↝A y ≡ (x, y) ∈ evalA"

abbreviation 
  eval_abvC :: "('ComC, 'VarC, 'Val) LocalConf ⇒ (_, _, _) LocalConf ⇒ bool"
  (infixl "↝C" 70)
where
  "x ↝C y ≡ (x, y) ∈ evalC"

definition
  preserves_modes_mem :: "('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation ⇒ bool"
where
  "preserves_modes_mem ℛ ≡ 
  (∀ cA mdsA memA cC mdsC memC. (⟨ cA, mdsA, memA ⟩A, ⟨ cC, mdsC, memC ⟩C) ∈ ℛ ⟶
      (∀xA. (memA xA) = (memC (varC_of xA))) ∧
      (∀m. varC_of ` mdsA m = (range varC_of) ∩ mdsC m))"

definition
  memA_of :: "('VarC, 'Val) Mem ⇒ ('VarA, 'Val) Mem"
where
  "memA_of memC ≡  (λxA. (memC (varC_of xA)))"
  
definition
  mdsA_of :: "'VarC Mds ⇒ 'VarA Mds"
where
  "mdsA_of mdsC ≡ (λ m. (inv varC_of) ` (range varC_of ∩ mdsC m))"

lemma low_mds_eq_from_conc_to_abs:
  "conc.low_mds_eq mds mem mem' ⟹ abs.low_mds_eq (mdsA_of mds) (memA_of mem) (memA_of mem')"
  apply(clarsimp simp: abs.low_mds_eq_def conc.low_mds_eq_def memA_of_def mdsA_of_def)
  using varC_of_inj 
  by (metis IntI control_vars_are_A_vars dma_consistent image_eqI inv_f_f rangeI)

definition
  varA_of :: "'VarC ⇒ 'VarA"
where
  "varA_of ≡ inv varC_of"

lemma preserves_modes_mem_memA_simp:
  "(∀xA. (memA xA) = (memC (varC_of xA))) ⟹
      memA = memA_of memC"
  unfolding memA_of_def by blast


lemma preserves_modes_mem_mdsA_simp:
  "(∀m. varC_of ` mdsA m = range (varC_of) ∩ mdsC m) ⟹
      mdsA = mdsA_of mdsC"
  unfolding mdsA_of_def
  apply(rule ext)
  apply(drule_tac x=m in spec)
  apply(rule equalityI)
   apply clarsimp
   apply(rename_tac xA)
   apply(drule equalityD1)
   apply(drule_tac c="varC_of xA" in subsetD)
    apply blast
   unfolding image_def
   apply clarsimp
   apply(rule_tac x="varC_of xA" in bexI)
    apply(rule sym)
    apply(rule inv_f_f[OF varC_of_inj])
   apply(drule inj_onD[OF varC_of_inj])
   apply blast+
  apply clarsimp
  apply(rename_tac xA)
  apply(simp add: inv_f_f[OF varC_of_inj])
  apply(drule equalityD2)
  apply(drule_tac c="varC_of xA" in subsetD)
   apply blast
  apply clarsimp
  apply(drule inj_onD[OF varC_of_inj])
  apply blast+
  done

text ‹
  This version might be more useful. Not sure yet.
›
lemma preserves_modes_mem_def2:
  "preserves_modes_mem ℛ =
  (∀ cA mdsA memA cC mdsC memC. (⟨ cA, mdsA, memA ⟩A, ⟨ cC, mdsC, memC ⟩C) ∈ ℛ ⟶
      memA = memA_of memC ∧
      mdsA = mdsA_of mdsC)"
  unfolding preserves_modes_mem_def
  apply(rule iffI)
   apply(blast dest: preserves_modes_mem_memA_simp preserves_modes_mem_mdsA_simp)
  apply safe
     apply(elim allE impE, assumption, elim conjE)
     apply(simp add: memA_of_def)
    apply blast
   apply clarsimp
   apply(rename_tac xA)
   apply(elim allE impE, assumption, elim conjE)
   apply clarsimp
   apply(clarsimp simp: mdsA_of_def image_def)
   apply(simp add: inv_f_f[OF varC_of_inj])
  apply clarsimp
  apply(rename_tac xA)
  apply(rule imageI)
  apply(elim allE impE, assumption, elim conjE)
  apply(clarsimp simp: mdsA_of_def)
  apply(subst image_def)
  apply clarify
  apply(rule_tac x="varC_of xA" in bexI)
   apply(simp add: inv_f_f[OF varC_of_inj])
  apply blast
  done

definition
  closed_others :: "('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation ⇒ bool"
where
  "closed_others ℛ ≡ 
  (∀ cA cC mdsC memC memC'. (⟨ cA, mdsA_of mdsC, memA_of memC ⟩A, ⟨ cC, mdsC, memC ⟩C) ∈ ℛ ⟶
   (∀x. memC x ≠ memC' x ⟶ ¬ var_asm_not_written mdsC x) ⟶
   (∀x. dmaC memC x ≠ dmaC memC' x ⟶ ¬ var_asm_not_written mdsC x) ⟶
         (⟨ cA, mdsA_of mdsC, memA_of memC' ⟩A, ⟨ cC, mdsC, memC' ⟩C) ∈ ℛ)"

definition
  stopsC :: "('ComC, 'VarC, 'Val) LocalConf ⇒ bool"
where
  "stopsC c ≡ ∀c'. ¬ (c ↝C c')"

lemmas neval_induct = abs.neval.induct[consumes 1, case_names Zero Suc]

(* FIXME: move to Security.thy or similar *)
lemma strong_low_bisim_neval':
  "abs.neval c1 n cn ⟹ (c1,c1') ∈ ℛA ⟹ snd (fst c1) = snd (fst c1') ⟹ abs.strong_low_bisim_mm ℛA ⟹
  ∃cn'. abs.neval c1' n cn' ∧ (cn,cn') ∈ ℛA ∧ snd (fst cn) = snd (fst (cn'))"
proof(induct  arbitrary: c1' rule: neval_induct)
  case (Zero c1 cn)
   hence "abs.neval c1' 0 c1' ∧ (cn, c1') ∈ ℛA ∧ snd (fst cn) = snd (fst c1')"
     by(blast intro: abs.neval.intros(1))
   thus ?case by blast
next
  case (Suc lc0 lc1 n lcn lc0')
  obtain c0 mds0 mem0 
  where [simp]: "lc0 = ⟨c0, mds0, mem0⟩A" by (case_tac lc0, auto)
  obtain c1 mds1 mem1 
  where [simp]: "lc1 = ⟨c1, mds1, mem1⟩A" by (case_tac lc1, auto)
  from ‹snd (fst lc0) = snd (fst lc0')› obtain c0' mem0'
  where [simp]: "lc0' = ⟨c0', mds0, mem0'⟩A" by (case_tac lc0', auto)
  
  from ‹(lc0, lc0') ∈ ℛA›[simplified] ‹lc0 ↝A lc1›[simplified] ‹abs.strong_low_bisim_mm ℛA›
  obtain c1' mem1' where a: "⟨c0',mds0, mem0'⟩A ↝A ⟨c1',mds1, mem1'⟩A" and 
          b: "(⟨c1,mds1,mem1⟩A,⟨c1',mds1, mem1'⟩A) ∈ ℛA"
    unfolding abs.strong_low_bisim_mm_def
    by blast

  from this Suc.hyps Suc(6) obtain lcS' where "abs.neval ⟨c1',mds1,mem1'⟩A n lcS'" and "(lcn, lcS') ∈ ℛA" and "snd (fst lcn) = snd (fst lcS')"
    by force
  with Suc this a b show ?case by(fastforce intro: abs.neval.intros(2))
qed

lemma strong_low_bisim_neval:
  "abs.neval ⟨c1,mds1,mem1⟩A n ⟨cn,mdsn,memn⟩A ⟹ (⟨c1,mds1,mem1⟩A,⟨c1',mds1,mem1'⟩A) ∈ ℛA ⟹ abs.strong_low_bisim_mm ℛA ⟹
  ∃cn' memn'. abs.neval ⟨c1',mds1,mem1'⟩A n ⟨cn',mdsn,memn'⟩A ∧ (⟨cn,mdsn,memn⟩A,⟨cn',mdsn,memn'⟩A) ∈ ℛA"
  by(drule strong_low_bisim_neval', simp+)

lemma in_ℛ_dma':
  assumes preserves: "preserves_modes_mem ℛ"
  assumes in_ℛ: "(⟨cA,mdsA,memA⟩A,⟨cC,mdsC,memC⟩C) ∈ ℛ"
  shows  "dmaA memA xA = dmaC memC (varC_of xA)"
proof -
  from assms have
    mdsA_def: "mdsA = mdsA_of mdsC" and  
    memA_def: "memA = memA_of memC"
    unfolding preserves_modes_mem_def2 by blast+
  
  have "dmaA (memA_of memC) xA = dmaC memC (varC_of xA)"
    unfolding memA_of_def
    by(rule dma_consistent)
  
  thus ?thesis
    by(simp add: memA_def)
qed

lemma in_ℛ_dma:
  assumes preserves: "preserves_modes_mem ℛ"
  assumes in_ℛ: "(⟨cA,mdsA,memA⟩A,⟨cC,mdsC,memC⟩C) ∈ ℛ"
  shows  "dmaA memA = (dmaC memC ∘ varC_of)"
  unfolding o_def
  using assms by(blast intro: in_ℛ_dma')


definition
  new_vars_private ::  "('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation ⇒ bool"
where
  "new_vars_private ℛ ≡
  (∀ c1A mdsA mem1A c1C mdsC mem1C. 
   (⟨ c1A, mdsA, mem1A ⟩A, ⟨ c1C, mdsC, mem1C ⟩C) ∈ ℛ ⟶
    (∀ c1C' mdsC' mem1C'. ⟨ c1C, mdsC, mem1C ⟩C ↝C ⟨ c1C', mdsC', mem1C' ⟩C ⟶
     (∀vC. (mem1C' vC ≠ mem1C vC ∨ dmaC mem1C' vC < dmaC mem1C vC) ∧ vC ∉ range varC_of ⟶ vC ∈ mdsC' AsmNoReadOrWrite) ∧
     (mdsC AsmNoReadOrWrite - (range varC_of)) ⊆ (mdsC' AsmNoReadOrWrite - (range varC_of))))"

lemma not_less_eq_is_greater_Sec:
  "(¬ a ≤ (b::Sec)) = (a > b)"
  unfolding less_Sec_def less_eq_Sec_def using Sec.exhaust by blast

lemma doesnt_have_mode:
  "(x ∉ mdsA_of mdsC m) = (varC_of x ∉ mdsC m)"
  apply(clarsimp simp: mdsA_of_def image_def)
  apply(rule iffI)
   apply clarsimp
   apply(drule_tac x="varC_of x" in bspec)
    apply blast
   apply(simp add: inv_f_f[OF varC_of_inj])
  apply(clarify)
  apply(simp add: inv_f_f[OF varC_of_inj])
  done

lemma new_vars_private_does_the_thing:
  assumes nice: "new_vars_private ℛ"
  assumes in_ℛ1: "(⟨ c1A, mdsA_of mdsC, memA_of mem1C ⟩A, ⟨ c1C, mdsC, mem1C ⟩C) ∈ ℛ"
  assumes in_ℛ2: "(⟨ c2A, mdsA_of mdsC, memA_of mem2C ⟩A, ⟨ c2C, mdsC, mem2C ⟩C) ∈ ℛ"
  assumes step1C: "⟨ c1C, mdsC, mem1C ⟩C ↝C ⟨ c1C', mdsC', mem1C' ⟩C"
  assumes step2C: "⟨ c2C, mdsC, mem2C ⟩C ↝C ⟨ c2C', mdsC', mem2C' ⟩C"
  assumes low_mds_eqC: "conc.low_mds_eq mdsC mem1C mem2C"
  assumes low_mds_eqA': "abs.low_mds_eq (mdsA_of mdsC') (memA_of mem1C') (memA_of mem2C')" 
  shows "conc.low_mds_eq mdsC' mem1C' mem2C'"
  unfolding conc.low_mds_eq_def
proof(clarify)
  let ?mem1A = "memA_of mem1C"
  let ?mem2A = "memA_of mem2C"
  let ?mem1A' = "memA_of mem1C'"
  let ?mem2A' = "memA_of mem2C'"
  let ?mdsA = "mdsA_of mdsC"
  let ?mdsA' = "mdsA_of mdsC'"
  fix xC
  assume is_LowC': "dmaC mem1C' xC = Low"
  assume is_readableC': "xC ∈ 𝒞C ∨ xC ∉ mdsC' AsmNoReadOrWrite"
  show "mem1C' xC = mem2C' xC"
  proof(cases "dmaC mem1C' xC ≥ dmaC mem1C xC ∧ mem1C' xC = mem1C xC ∧ mem2C' xC = mem2C xC ∧ (xC ∈ mdsC AsmNoReadOrWrite ⟶ xC ∈ mdsC' AsmNoReadOrWrite)")
    assume easy: "dmaC mem1C' xC ≥ dmaC mem1C xC ∧ mem1C' xC = mem1C xC ∧ mem2C' xC = mem2C xC ∧ (xC ∈ mdsC AsmNoReadOrWrite ⟶ xC ∈ mdsC' AsmNoReadOrWrite)"
    with is_LowC' have is_LowC: "dmaC mem1C xC = Low" by (simp add: less_eq_Sec_def)
    from easy is_readableC' have is_readableC: "xC ∈ 𝒞C ∨ xC ∉ mdsC AsmNoReadOrWrite" by blast
    from is_LowC is_readableC low_mds_eqC have "mem1C xC = mem2C xC"
      unfolding conc.low_mds_eq_def by blast
    with easy show ?thesis by metis
  next
    assume a: "¬ (dmaC mem1C xC ≤ dmaC mem1C' xC ∧
       mem1C' xC = mem1C xC ∧
       mem2C' xC = mem2C xC ∧ (xC ∈ mdsC AsmNoReadOrWrite ⟶ xC ∈ mdsC' AsmNoReadOrWrite))"
    hence a_disj: "(dmaC mem1C xC > dmaC mem1C' xC ∨
       mem1C' xC ≠ mem1C xC ∨
       mem2C' xC ≠ mem2C xC ∨ (xC ∈ mdsC AsmNoReadOrWrite ∧ xC ∉ mdsC' AsmNoReadOrWrite))"
       using not_less_eq_is_greater_Sec by blast
    show "mem1C' xC = mem2C' xC"
    proof(cases "xC ∈ range varC_of")
      assume C_only_var: "xC ∉ range varC_of"
      with in_ℛ1 step1C nice
      have "(mem1C' xC ≠ mem1C xC ∨ dmaC mem1C' xC < dmaC mem1C xC) ⟶ xC ∈ mdsC' AsmNoReadOrWrite"
        unfolding new_vars_private_def  by blast
      moreover from C_only_var in_ℛ2 step2C nice have "(mem2C' xC ≠ mem2C xC) ⟶ xC ∈ mdsC' AsmNoReadOrWrite"
        unfolding new_vars_private_def by blast
      moreover from C_only_var in_ℛ1 step1C nice have "xC ∈ mdsC AsmNoReadOrWrite ⟶ xC ∈ mdsC' AsmNoReadOrWrite" unfolding new_vars_private_def by blast
      moreover from C_only_var is_readableC' have "xC ∉ mdsC' AsmNoReadOrWrite"
        using control_vars_are_A_vars by blast
      ultimately have False using a_disj by blast
      thus ?thesis by blast
    next
      assume in_valC_of: "xC ∈ range varC_of"
      from this obtain xA where xC_def: "xC = varC_of xA" by blast
      from is_LowC' have is_LowA': "dmaA ?mem1A' xA = Low"
        using dma_consistent unfolding memA_of_def xC_def by force
      from is_readableC' have is_readableA': "xA ∈ 𝒞A ∨ xA ∉ ?mdsA' AsmNoReadOrWrite"
        using control_vars_are_A_vars xC_def doesnt_have_mode[symmetric] varC_of_inj inj_image_mem_iff by fast
      with is_LowA' low_mds_eqA' have xA_eq': "?mem1A' xA = ?mem2A' xA" 
        unfolding abs.low_mds_eq_def by blast
      thus ?thesis by(simp add: memA_of_def xC_def)
    qed
  qed
qed

  
text ‹
  Perhaps surprisingly, we don't necessarily 
  care whether the refinement preserves
  termination or divergence behaviour from the source to the target program.
  It can do whatever it likes, so long as it transforms two source programs
  that are low bisimilar (i.e. perform the same low actions at the 
  same time), into two target ones that perform the same low actions at the
  same time.

  Having the concrete step correspond to zero abstract ones is like expanding
  abstract code out (think e.g. of side-effect free expression evaluation).
  Having the concrete step correspond to more than one abstract step is
  like optimising out abstract code. But importantly, the optimisation needs
  to look the same for abstract-bisimilar code.

  Additionally, we allow the instantiation of this theory to supply
  an arbitrary predicate that can be used to restrict our consideration to
  pairs of concrete steps that correspond to each other in terms of progress.
  This is particularly important for distinguishing between multiple concrete
  steps derived from the expansion of a single abstract step.
›
definition
  secure_refinement :: "('ComA, 'VarA, 'Val) LocalConf rel ⇒ ('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation ⇒ 
                          ('ComC, 'VarC, 'Val) LocalConf rel ⇒ bool"
where
  "secure_refinement ℛA ℛ P ≡
  closed_others ℛ ∧
  preserves_modes_mem ℛ ∧
  new_vars_private ℛ ∧
  conc.closed_glob_consistent P ∧
  (∀ c1A mdsA mem1A c1C mdsC mem1C. 
   (⟨ c1A, mdsA, mem1A ⟩A, ⟨ c1C, mdsC, mem1C ⟩C) ∈ ℛ ⟶
    (∀ c1C' mdsC' mem1C'. ⟨ c1C, mdsC, mem1C ⟩C ↝C ⟨ c1C', mdsC', mem1C' ⟩C ⟶
     (∃ n c1A' mdsA' mem1A'. abs.neval ⟨ c1A, mdsA, mem1A ⟩A n ⟨ c1A', mdsA', mem1A' ⟩A ∧
                   (⟨ c1A', mdsA', mem1A' ⟩A, ⟨ c1C', mdsC', mem1C' ⟩C) ∈ ℛ ∧
       (∀c2A mem2A c2C mem2C c2A' mem2A'. 
         (⟨ c1A, mdsA, mem1A ⟩A, ⟨ c2A, mdsA, mem2A ⟩A) ∈ ℛA ∧
         (⟨ c2A, mdsA, mem2A ⟩A, ⟨ c2C, mdsC, mem2C ⟩C) ∈ ℛ ∧
         (⟨ c1C, mdsC, mem1C ⟩C, ⟨ c2C, mdsC, mem2C ⟩C) ∈ P ∧
         abs.neval ⟨ c2A, mdsA, mem2A ⟩A n ⟨ c2A', mdsA', mem2A' ⟩A  ⟶
           (∃ c2C' mem2C'. ⟨ c2C, mdsC, mem2C ⟩C ↝C ⟨ c2C', mdsC', mem2C' ⟩C ∧
                   (⟨ c2A', mdsA', mem2A' ⟩A, ⟨ c2C', mdsC', mem2C' ⟩C) ∈ ℛ ∧
                   (⟨ c1C', mdsC', mem1C' ⟩C, ⟨ c2C', mdsC', mem2C' ⟩C) ∈ P)))))"

lemma preserves_modes_memD:
  "⟦preserves_modes_mem ℛ; (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ ℛ⟧ ⟹ memA = memA_of memC ∧ mdsA = mdsA_of mdsC"
  using preserves_modes_mem_def2 by blast

lemma secure_refinement_def2:
  "secure_refinement ℛA ℛ P ≡
  closed_others ℛ ∧
  preserves_modes_mem ℛ ∧
  new_vars_private ℛ ∧
  conc.closed_glob_consistent P ∧
  (∀ c1A c1C mdsC mem1C. 
   (⟨ c1A, mdsA_of mdsC, memA_of mem1C ⟩A, ⟨ c1C, mdsC, mem1C ⟩C) ∈ ℛ ⟶
    (∀ c1C' mdsC' mem1C'. ⟨ c1C, mdsC, mem1C ⟩C ↝C ⟨ c1C', mdsC', mem1C' ⟩C ⟶
     (∃ n c1A'. abs.neval ⟨ c1A, mdsA_of mdsC, memA_of mem1C ⟩A n ⟨ c1A', mdsA_of mdsC', memA_of mem1C' ⟩A ∧
                   (⟨ c1A', mdsA_of mdsC', memA_of mem1C' ⟩A, ⟨ c1C', mdsC', mem1C' ⟩C) ∈ ℛ ∧
       (∀c2A c2C mem2C c2A' mem2A'. 
         (⟨ c1A, mdsA_of mdsC, memA_of mem1C ⟩A, ⟨ c2A, mdsA_of mdsC, memA_of mem2C ⟩A) ∈ ℛA ∧
         (⟨ c2A, mdsA_of mdsC, memA_of mem2C ⟩A, ⟨ c2C, mdsC, mem2C ⟩C) ∈ ℛ ∧
         (⟨ c1C, mdsC, mem1C ⟩C, ⟨ c2C, mdsC, mem2C ⟩C) ∈ P ∧
         abs.neval ⟨ c2A, mdsA_of mdsC, memA_of mem2C ⟩A n ⟨ c2A', mdsA_of mdsC', mem2A' ⟩A  ⟶
           (∃ c2C' mem2C'. ⟨ c2C, mdsC, mem2C ⟩C ↝C ⟨ c2C', mdsC', mem2C' ⟩C ∧
                   (⟨ c2A', mdsA_of mdsC', mem2A' ⟩A, ⟨ c2C', mdsC', mem2C' ⟩C) ∈ ℛ ∧
                   (⟨ c1C', mdsC', mem1C' ⟩C, ⟨ c2C', mdsC', mem2C' ⟩C) ∈ P)))))"
  apply(rule eq_reflection)
  unfolding secure_refinement_def
  apply(rule conj_cong)
   apply(fastforce)
  apply(rule conj_cong)
   apply(fastforce)
  apply(rule conj_cong)
   apply(fastforce)
  apply(rule conj_cong, fastforce)
  apply(rule iffI)
   apply(intro allI conjI impI)
   apply((drule spec)+,erule (1) impE)
   apply((drule spec)+,erule (1) impE)
   using preserves_modes_memD apply metis
  apply(intro allI conjI impI)
  apply(frule (1) preserves_modes_memD, clarify)
  apply((drule spec)+,erule (1) impE)
  apply((drule spec)+,erule (1) impE)
  using preserves_modes_memD apply metis
  done

lemma extra_vars_are_not_control_vars:
  "x ∉ range varC_of ⟹ x ∉ 𝒞C"
  proof(erule contrapos_nn)
    assume "x ∈ 𝒞C"
    from this obtain xA where "x = varC_of xA"
      using control_vars_are_A_vars by blast
    thus "x ∈ range varC_of" by blast
  qed

definition
  RC_of :: 
 "((('ComA × (Mode ⇒ 'VarA set)) × ('VarA ⇒ 'Val)) ×
    ('ComA × (Mode ⇒ 'VarA set)) × ('VarA ⇒ 'Val)) set ⇒ 
  ('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation ⇒
  ((('ComC × (Mode ⇒ 'VarC set)) × ('VarC ⇒ 'Val)) ×
    ('ComC × (Mode ⇒ 'VarC set)) × ('VarC ⇒ 'Val)) set ⇒
  ((('ComC × (Mode ⇒ 'VarC set)) × ('VarC ⇒ 'Val)) ×
    ('ComC × (Mode ⇒ 'VarC set)) × ('VarC ⇒ 'Val)) set"
where
  "RC_of ℛA ℛ P ≡ {(x,y). ∃xA yA. (xA,x) ∈ ℛ ∧ (yA,y) ∈ ℛ ∧ (xA,yA) ∈ ℛA ∧
     snd (fst x) = snd (fst y) ― ‹TODO: annoying to have to say› ∧
     conc.low_mds_eq (snd (fst x)) (snd x) (snd y) ∧
     (x,y) ∈ P}"

lemma abs_low_mds_eq_dmaC_eq:
  assumes "abs.low_mds_eq (mdsA_of mds) (memA_of mem1C)  (memA_of mem2C)"
  shows "dmaC mem1C = dmaC mem2C"
  proof(rule conc.dma_𝒞, rule ballI)
    fix xC
    assume "xC ∈ 𝒞C"
    from this obtain xA where "varC_of xA = xC" and "xA ∈ 𝒞A" using control_vars_are_A_vars by blast
    from assms ‹xA ∈ 𝒞A› have "(memA_of mem1C) xA = (memA_of mem2C) xA"
      unfolding abs.low_mds_eq_def
      using abs.𝒞_Low by blast
    thus "(mem1C xC) = (mem2C xC)"
      using ‹varC_of xA = xC› unfolding memA_of_def by blast
  qed

lemma RC_ofD:
  assumes rr: "secure_refinement ℛA ℛ P"
  assumes in_R: "(⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC', mem2C⟩C) ∈ RC_of ℛA ℛ P"
  shows
   "(∃c1A c2A.  (⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ ∧
             (⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ ∧
             (⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A) ∈ ℛA) ∧
    (mdsC' = mdsC) ∧
    conc.low_mds_eq mdsC mem1C mem2C ∧
    (⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC', mem2C⟩C) ∈ P"
  proof -
  have ℛ_preserves_modes_mem: "preserves_modes_mem ℛ"
    using rr unfolding secure_refinement_def by blast

  from in_R obtain c1A mds1A mem1A c2A mds2A mem2A where
  in_ℛ1: "(⟨c1A, mds1A, mem1A⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ" and
  in_ℛ2: "(⟨c2A, mds2A, mem2A⟩A, ⟨c2C, mdsC', mem2C⟩C) ∈ ℛ" and
  in_ℛA: "(⟨c1A, mds1A, mem1A⟩A, ⟨c2A, mds2A, mem2A⟩A) ∈ ℛA" and
  pred_holds: "(⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ P" and
  mds_eq: "mdsC = mdsC'" and
  mds_eq: "conc.low_mds_eq mdsC mem1C mem2C"
    unfolding RC_of_def by force+
  
  from this ℛ_preserves_modes_mem[simplified preserves_modes_mem_def2, rule_format, OF in_ℛ1] ℛ_preserves_modes_mem[simplified preserves_modes_mem_def2, rule_format, OF in_ℛ2]
    show ?thesis by blast
qed

lemma RC_ofI:
   "(⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ ⟹
    (⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ ⟹
    (⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A) ∈ ℛA ⟹
    conc.low_mds_eq mdsC mem1C mem2C ⟹
    (⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ P ⟹
     (⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ RC_of ℛA ℛ P"
  unfolding RC_of_def by fastforce

lemma RC_of_sym:
  assumes "sym ℛA"
  assumes P_sym: "sym P"
  assumes rr: "secure_refinement ℛA ℛ P"
  assumes mm: 
    "⋀c1 mds mem1 c2 mds mem2. (⟨c1, mds, mem1⟩A, ⟨c2, mds, mem2⟩A) ∈ ℛA ⟹
    abs.low_mds_eq mds mem1 mem2"
  shows "sym (RC_of ℛA ℛ P)"
proof(rule symI, clarify)
  fix c1C mdsC mem1C  c2C mdsC' mem2C
  assume in_RC_of: "(⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC', mem2C⟩C) ∈ RC_of ℛA ℛ P"
  from in_RC_of obtain c1A c2A where
  junk:
  "(⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ ∧
   (⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ ∧
   (⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A) ∈ ℛA ∧
    (mdsC' = mdsC) ∧ conc.low_mds_eq mdsC mem1C mem2C ∧
    (⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ P"
    using rr RC_ofD by fastforce+
  hence dma_eq: "dmaC mem1C = dmaC mem2C"
    using abs_low_mds_eq_dmaC_eq[OF mm] by blast
  with junk have junk':
  "(⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ ∧
   (⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ ∧
   (⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A, ⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A) ∈ ℛA ∧
    (mdsC' = mdsC) ∧
   conc.low_mds_eq mdsC' mem2C mem1C ∧
   (⟨c2C, mdsC, mem2C⟩C, ⟨c1C, mdsC, mem1C⟩C) ∈ P"
    using ‹sym ℛA› P_sym unfolding sym_def using conc.low_mds_eq_sym by metis
   thus "(⟨c2C, mdsC', mem2C⟩C, ⟨c1C, mdsC, mem1C⟩C) ∈ RC_of ℛA ℛ P"
   using RC_ofI by auto
qed

lemma RC_of_simp:
  assumes rr: "secure_refinement ℛA ℛ P"
  shows "(⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ RC_of ℛA ℛ P =
   ((∃c1A c2A.  (⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ ∧
             (⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ ∧
             (⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A) ∈ ℛA) ∧
    conc.low_mds_eq mdsC mem1C mem2C ∧
    (⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ P)"
  using assms by(blast dest: RC_ofD intro: RC_ofI)

definition
  AA_of :: "('VarC,'Val) adaptation ⇒ ('VarA,'Val) adaptation"
where
  "AA_of A ≡ λxA. case A (varC_of xA) of None ⇒ None |
                  Some (v,v') ⇒ Some (v,v')"

lemma var_writableA:
  "¬ var_asm_not_written mdsC (varC_of x) ⟹ ¬ var_asm_not_written (mdsA_of mdsC) x"
  apply(simp add: var_asm_not_written_def mdsA_of_def)
  apply(auto simp: inv_f_f[OF varC_of_inj])
  done

lemma AA_asm_mem:
  assumes AC_asm_mem: "∀x. case AC x of None ⇒ True
           | Some (v, v') ⇒
               mem1C x ≠ v ∨ mem2C x ≠ v' ⟶ ¬ var_asm_not_written mdsC x"
  shows "case (AA_of AC) x of None ⇒ True
           | Some (v, v') ⇒
               (memA_of mem1C) x ≠ v ∨ (memA_of mem2C) x ≠ v' ⟶ ¬ var_asm_not_written (mdsA_of mdsC) x"
  apply(split option.splits, simp, intro allI impI)
  proof -
    fix v v'
    assume AA_not_None: "AA_of AC x = Some (v, v')"
    assume AA_updates_x: "memA_of mem1C x = v ⟶ memA_of mem2C x ≠ v'"
    from AA_not_None have
      AC_not_None: "AC (varC_of x) = Some (v, v')"
      unfolding AA_of_def by (auto split: option.splits)

    from AA_updates_x  have
      AC_updates_x: "mem1C (varC_of x) ≠ v ∨ mem2C (varC_of x) ≠ v'"
      unfolding memA_of_def by fastforce

    from AC_not_None AC_updates_x AC_asm_mem have
      "¬ var_asm_not_written mdsC (varC_of x)" by (auto split: option.splits)

    thus "¬ var_asm_not_written (mdsA_of mdsC) x"
      by(rule var_writableA)
  qed

lemma dmaA_adaptation_eq:
  "dmaA ((memA_of mem1C) [∥1 AA_of AC]) xA = dmaC (mem1C [∥1 AC]) (varC_of xA)"
  apply(subst dma_consistent[folded memA_of_def, symmetric])
  apply(rule_tac x=xA in fun_cong)
  apply(rule_tac f="dmaA" in arg_cong)
  apply(rule ext)
  apply(clarsimp simp: apply_adaptation_def AA_of_def memA_of_def split: option.splits)
  done

  
lemma AA_asm_dma:
  assumes AC_asm_dma: "∀x. dmaC (mem1C [∥1 AC]) x ≠ dmaC mem1C x ⟶ ¬ var_asm_not_written mdsC x"
  shows "dmaA ((memA_of mem1C) [∥1 (AA_of AC)]) xA ≠ dmaA (memA_of mem1C) xA ⟶ ¬ var_asm_not_written (mdsA_of mdsC) xA"
proof(intro impI)
  assume AA_updates_dma: "dmaA ((memA_of mem1C) [∥1 AA_of AC]) xA ≠ dmaA (memA_of mem1C) xA"
 
  with dma_consistent[folded memA_of_def] dmaA_adaptation_eq
  have "dmaC (mem1C [∥1 AC]) (varC_of xA) ≠ dmaC mem1C (varC_of xA)" by(metis)

  with AC_asm_dma have "¬ var_asm_not_written mdsC (varC_of xA)" by blast

  thus " ¬ var_asm_not_written (mdsA_of mdsC) xA" by (rule  var_writableA)
qed

lemma varC_of_in_𝒞C: 
  assumes "xA ∈ 𝒞A"
  shows "varC_of xA ∈ 𝒞C"
proof -
  from assms obtain yA where "xA ∈ 𝒞_varsA yA"
  unfolding abs.𝒞_def by blast

  hence "varC_of xA ∈ 𝒞_varsC (varC_of yA)"
    using 𝒞_vars_consistent by blast

  thus ?thesis using conc.𝒞_def by blast
qed

lemma doesnt_have_modeC:
  "x ∉ mdsA_of mdsC m ⟹ varC_of x ∉ mdsC m"
  by(simp add: doesnt_have_mode)

lemma has_modeA: "varC_of x ∈ mdsC m ⟹ x ∈ mdsA_of mdsC m"
  using doesnt_have_modeC
  by fastforce

lemma AA_sec:
  assumes AC_sec: "∀x. dmaC (mem1C [∥1 AC]) x = Low ∧ (x ∉ mdsC AsmNoReadOrWrite ∨ x ∈ 𝒞C) ⟶
           mem1C [∥1 AC] x = mem2C [∥2 AC] x"
  shows "dmaA ((memA_of mem1C) [∥1 AA_of AC]) x = Low ∧ (x ∉ mdsA_of mdsC AsmNoReadOrWrite ∨ x ∈ 𝒞A) ⟶
           (memA_of mem1C) [∥1 AA_of AC] x = (memA_of mem2C) [∥2 AA_of AC] x"
proof(clarify)
  assume x_is_Low: "dmaA ((memA_of mem1C) [∥1 AA_of AC]) x = Low"
  assume x_is_readable: "x ∉ mdsA_of mdsC AsmNoReadOrWrite ∨ x ∈ 𝒞A"
    
  from x_is_Low have x_is_LowC: "dmaC (mem1C [∥1 AC]) (varC_of x) = Low"
    using dmaA_adaptation_eq by simp
  from x_is_readable have "varC_of x ∉ mdsC AsmNoReadOrWrite ∨ varC_of x ∈ 𝒞C"
    using doesnt_have_modeC  varC_of_in_𝒞C by blast
  with AC_sec x_is_LowC have "mem1C [∥1 AC] (varC_of x) = mem2C [∥2 AC] (varC_of x)"
    by blast
  thus "(memA_of mem1C) [∥1 AA_of AC] x = (memA_of mem2C) [∥2 AA_of AC] x"
    by(auto simp: memA_of_def apply_adaptation_def AA_of_def split: option.splits)
qed

lemma apply_adaptationA:
  "(memA_of mem1C) [∥1 AA_of AC] = memA_of (mem1C [∥1 AC])"
  "(memA_of mem1C) [∥2 AA_of AC] = memA_of (mem1C [∥2 AC])"
  by(auto simp: memA_of_def AA_of_def apply_adaptation_def split: option.splits)

 
lemma RC_of_closed_glob_consistent:
  assumes mm: 
    "⋀c1 mds mem1 c2 mds mem2. (⟨c1, mds, mem1⟩A, ⟨c2, mds, mem2⟩A) ∈ ℛA ⟹
    abs.low_mds_eq mds mem1 mem2"
  assumes cgc: "abs.closed_glob_consistent ℛA"
  assumes rr: "secure_refinement ℛA ℛ P"
  shows "conc.closed_glob_consistent (RC_of ℛA ℛ P)"
  unfolding conc.closed_glob_consistent_def
proof(clarify)
  fix c1C mdsC mem1C c2C mem2C AC
  assume "(⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ RC_of ℛA ℛ P"
  from this rr obtain c1A c2A where
       in_ℛA:  "(⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A) ∈ ℛA" and
       in_ℛ1:  "(⟨c1A, mdsA_of mdsC, memA_of mem1C⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ" and
       in_ℛ2:  "(⟨c2A, mdsA_of mdsC, memA_of mem2C⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ"
         and
       mds_eq: "conc.low_mds_eq mdsC mem1C mem2C"
         and
       P: "(⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ P"
      by (blast dest: RC_ofD)
  assume AC_asm_mem: "∀x. case AC x of None ⇒ True
                                   | Some (v, v') ⇒
                                      mem1C x ≠ v ∨ mem2C x ≠ v' ⟶ ¬ var_asm_not_written mdsC x"
  hence AA_asm_mem: "∀x. case (AA_of AC) x of None ⇒ True
                                           | Some (v, v') ⇒
               (memA_of mem1C) x ≠ v ∨ (memA_of mem2C) x ≠ v' ⟶ ¬ var_asm_not_written (mdsA_of mdsC) x"
    by(metis AA_asm_mem)

  assume AC_asm_dma: "∀x. dmaC (mem1C [∥1 AC]) x ≠ dmaC mem1C x ⟶ ¬ var_asm_not_written mdsC x"
  hence AA_asm_dma: "∀xA. dmaA ((memA_of mem1C) [∥1 (AA_of AC)]) xA ≠ dmaA (memA_of mem1C) xA ⟶ ¬ var_asm_not_written (mdsA_of mdsC) xA"
    by(metis AA_asm_dma)

  assume AC_sec: "∀x. dmaC (mem1C [∥1 AC]) x = Low ∧ (x ∉ mdsC AsmNoReadOrWrite ∨ x ∈ 𝒞C) ⟶
         mem1C [∥1 AC] x = mem2C [∥2 AC] x"
  hence AA_sec: "∀x. dmaA ((memA_of mem1C) [∥1 AA_of AC]) x = Low ∧ (x ∉ mdsA_of mdsC AsmNoReadOrWrite ∨ x ∈ 𝒞A) ⟶
         (memA_of mem1C) [∥1 AA_of AC] x = (memA_of mem2C) [∥2 AA_of AC] x"
    by(metis AA_sec)
    
  from rr have others: "closed_others ℛ"
    unfolding secure_refinement_def by blast
  from rr have P_cgc: "conc.closed_glob_consistent P"
    unfolding secure_refinement_def by blast
  let ?mem1C' = "(mem1C [∥1 AC])" and
      ?mem2C' = "(mem2C [∥2 AC])" and
      ?mem1A = "(memA_of mem1C)" and
      ?mem2A = "(memA_of mem2C)" and
      ?mem1A' = "(memA_of mem1C) [∥1 AA_of AC]" and
      ?mem2A' = "(memA_of mem2C) [∥2 AA_of AC]"

  have mem'_simps: 
    "?mem1A' = memA_of ?mem1C'" 
    "?mem2A' = memA_of ?mem2C'" by(simp add: apply_adaptationA)+

  from cgc in_ℛA AA_asm_mem AA_asm_dma AA_sec have
    in_ℛA': "(⟨c1A, mdsA_of mdsC, (memA_of mem1C) [∥1 AA_of AC]⟩A, ⟨c2A, mdsA_of mdsC, (memA_of mem2C) [∥2 AA_of AC]⟩A) ∈ ℛA" unfolding abs.closed_glob_consistent_def by blast

  from AC_asm_mem AC_asm_dma have 
    AC_asm_mem1': "∀x. mem1C x ≠ ?mem1C' x ⟶ ¬ var_asm_not_written mdsC x" and
    AC_asm_dma1': "∀x. dmaC mem1C x ≠ dmaC ?mem1C' x ⟶ ¬ var_asm_not_written mdsC x"
    unfolding apply_adaptation_def by(force split: option.splits)+

  from AC_asm_mem have
    AC_asm_mem2': "∀x. mem2C x ≠ ?mem2C' x ⟶ ¬ var_asm_not_written mdsC x"
    unfolding apply_adaptation_def by(force split: option.splits)

  from in_ℛ1 AC_asm_mem1' AC_asm_dma1' others have
    in_ℛ1':  "(⟨c1A, mdsA_of mdsC, ?mem1A'⟩A, ⟨c1C, mdsC, ?mem1C'⟩C) ∈ ℛ"
    unfolding closed_others_def mem'_simps by blast

  from mm[OF in_ℛA] have 
    dmaC_eq: "dmaC mem1C = dmaC mem2C" by(rule abs_low_mds_eq_dmaC_eq)
  have dmaC_eq': "dmaC ?mem1C' = dmaC ?mem2C'"
    apply(rule abs_low_mds_eq_dmaC_eq[OF mm])
    apply(simp add: mem'_simps[symmetric])
    by(rule in_ℛA')
  from dmaC_eq dmaC_eq' AC_asm_dma1' have
    AC_asm_dma2': "∀x. dmaC mem2C x ≠ dmaC ?mem2C' x ⟶ ¬ var_asm_not_written mdsC x"
    by simp

  from in_ℛ2  AC_asm_mem2' AC_asm_dma2' others have
    in_ℛ2':  "(⟨c2A, mdsA_of mdsC, ?mem2A'⟩A, ⟨c2C, mdsC, ?mem2C'⟩C) ∈ ℛ"
    unfolding closed_others_def mem'_simps by blast

  have mds_eq': "conc.low_mds_eq mdsC ?mem1C' ?mem2C'" 
    using AC_sec unfolding conc.low_mds_eq_def by blast
   
 from P P_cgc AC_asm_mem AC_asm_dma AC_sec have P': "(⟨c1C, mdsC, ?mem1C'⟩C, ⟨c2C, mdsC, ?mem2C'⟩C) ∈ P"
   unfolding conc.closed_glob_consistent_def by blast 
  from in_ℛA' in_ℛ1' in_ℛ2' mem'_simps RC_ofI mds_eq' P' show
  "(⟨c1C, mdsC, ?mem1C'⟩C, ⟨c2C, mdsC, ?mem2C'⟩C) ∈ RC_of ℛA ℛ P"
    by(metis)
qed

lemma RC_of_local_preservation:
  assumes rr: "secure_refinement ℛA ℛ P"
  assumes bisim: "abs.strong_low_bisim_mm ℛA"
  assumes in_RC_of: "(⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ RC_of ℛA ℛ P"
  assumes step1C: "⟨c1C, mdsC, mem1C⟩C ↝C ⟨c1C', mdsC', mem1C'⟩C"
  shows "∃c2C' mem2C'.
          ⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C ∧
          (⟨c1C', mdsC', mem1C'⟩C, ⟨c2C', mdsC', mem2C'⟩C) ∈ RC_of ℛA ℛ P"
proof -
  from rr in_RC_of have
    P: "(⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ P"
      by(blast dest: RC_ofD)

  let ?mdsA = "mdsA_of mdsC" and
      ?mem1A = "memA_of mem1C" and
      ?mem2A = "memA_of mem2C" and
      ?mdsA' = "mdsA_of mdsC'" and
      ?mem1A' = "memA_of mem1C'"

  from rr in_RC_of obtain c1A c2A where
    in_ℛ1: "(⟨c1A, ?mdsA, ?mem1A⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ" and
    in_ℛ2: "(⟨c2A, ?mdsA, ?mem2A⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ" and
    in_ℛA: "(⟨c1A, ?mdsA, ?mem1A⟩A, ⟨c2A, ?mdsA, ?mem2A⟩A) ∈ ℛA" and
    low_mds_mdsC: "conc.low_mds_eq mdsC mem1C mem2C"
    by(blast dest: RC_ofD)+

  from rr in_ℛ1 in_ℛA in_ℛ2 step1C obtain n c1A' where
     a: "(abs.neval ⟨ c1A, ?mdsA, ?mem1A ⟩A n ⟨ c1A', ?mdsA', ?mem1A' ⟩A ∧
         (⟨ c1A', ?mdsA', ?mem1A' ⟩A, ⟨ c1C', mdsC', mem1C' ⟩C) ∈ ℛ ∧
       (∀c2A' mem2A'. 
         (⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ P ∧
         abs.neval ⟨ c2A, ?mdsA, ?mem2A ⟩A n ⟨ c2A', ?mdsA', mem2A' ⟩A  ⟶
           (∃ c2C' mem2C'. ⟨ c2C, mdsC, mem2C ⟩C ↝C ⟨ c2C', mdsC', mem2C' ⟩C ∧
                   (⟨ c2A', ?mdsA', mem2A' ⟩A, ⟨ c2C', mdsC', mem2C' ⟩C) ∈ ℛ ∧
                   (⟨c1C', mdsC', mem1C'⟩C, ⟨c2C', mdsC', mem2C'⟩C) ∈ P)))"
  unfolding secure_refinement_def2
    by metis

  show ?thesis
  proof -
    from a have neval1A: "abs.neval ⟨c1A, ?mdsA, ?mem1A⟩A n ⟨c1A', ?mdsA', ?mem1A'⟩A" and
                in_ℛ1': "(⟨c1A', ?mdsA', ?mem1A'⟩A, ⟨c1C', mdsC', mem1C'⟩C) ∈ ℛ"
           by blast+
    from  strong_low_bisim_neval[OF neval1A  in_ℛA bisim] obtain c2A' mem2A' where
      neval2A: "abs.neval ⟨c2A, ?mdsA, ?mem2A⟩A n ⟨c2A', ?mdsA', mem2A'⟩A" and
      in_ℛA'_help: "(⟨c1A', ?mdsA', ?mem1A'⟩A, ⟨c2A', ?mdsA', mem2A'⟩A) ∈ ℛA"
      unfolding abs.strong_low_bisim_mm_def
      by blast

    from a in_ℛA in_ℛ2 neval2A P obtain c2C' mem2C' where
          step2C: "⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C" and
          in_ℛ2'_help: "(⟨c2A', ?mdsA', mem2A'⟩A, ⟨c2C', mdsC', mem2C'⟩C) ∈ ℛ" and
          P': "(⟨c1C', mdsC', mem1C'⟩C, ⟨c2C', mdsC', mem2C'⟩C) ∈ P"
      by blast

    let ?mem2A' = "memA_of mem2C'"
    from in_ℛ2'_help rr preserves_modes_memD have "mem2A' = ?mem2A'" 
      unfolding secure_refinement_def by metis
    with in_ℛ2'_help in_ℛA'_help have 
      in_ℛ2': "(⟨c2A', ?mdsA', ?mem2A'⟩A, ⟨c2C', mdsC', mem2C'⟩C) ∈ ℛ" and
      in_ℛA': "(⟨c1A', ?mdsA', ?mem1A'⟩A, ⟨c2A', ?mdsA', ?mem2A'⟩A) ∈ ℛA"
      by simp+

    have "conc.low_mds_eq mdsC' mem1C' mem2C'"
      apply(rule new_vars_private_does_the_thing[where ℛ=ℛ, OF _ in_ℛ1 in_ℛ2 step1C step2C low_mds_mdsC])
       using rr apply(fastforce simp: secure_refinement_def)
      using in_ℛA' bisim unfolding abs.strong_low_bisim_mm_def by blast

    with step2C in_ℛ1' in_ℛ2' in_ℛA' in_ℛ2' P' show ?thesis
      by(blast intro: RC_ofI)
  qed
qed
  
text ‹
  Security of the concrete system should follow straightforwardly from
  security of the abstract one, via the compositionality theorem, presuming
  that the compiler also preserves the sound use of modes.
›
lemma RC_of_strong_low_bisim_mm:
  assumes abs: "abs.strong_low_bisim_mm ℛA"
  assumes rr: "secure_refinement ℛA ℛ P"
  assumes P_sym: "sym P"
  shows "conc.strong_low_bisim_mm (RC_of ℛA ℛ P)"
  unfolding conc.strong_low_bisim_mm_def
  apply(intro conjI)
    apply(rule RC_of_sym)
    using abs rr P_sym unfolding abs.strong_low_bisim_mm_def apply blast+
   apply(rule RC_of_closed_glob_consistent)
    using abs unfolding abs.strong_low_bisim_mm_def apply blast+
   using rr apply blast
  apply safe
   apply(fastforce simp: RC_of_def)
  apply(rule RC_of_local_preservation)
     apply(rule rr)
    apply(rule abs)
   apply assumption+
  done

section "A Simpler Proof Principle for General Compositional Refinement"

text ‹
  Here we make use of the fact that the source language we are working
  in is assumed deterministic. This allows us to invert the direction
  of refinement and thereby to derive a simpler condition for secure
  compositional refinement.
  
  The simpler condition rests on an ordinary definition of refinement,
  and has the user prove separately that the coupling invariant @{term P}
  is self-preserving. This allows proofs about coupling invariant properties
  to be disentangled from the proof of refinement itself.
›
  
text ‹
  Given a  bisimulation @{term ℛA}, this definition captures the essence of the extra
  requirements on a refinement relation~@{term ℛ} needed to ensure that the refined program is
  also secure. These requirements are essentially that:
  \begin{enumerate}
    \item The enabledness of the compiled code depends only on Low abstract data;
    \item The length of the abstract program to which a single step of the concrete program
          corresponds depends only on Low abstract data;
    \item The coupling invariant is maintained.
  \end{enumerate}
  
  The second requirement we express via the parameter~@{term abs_steps} that, given an
  abstract and corresponding concrete configuration, yields the number of execution steps of
  the abstract configuration to which a single step of the concrete configuration corresponds.
  
  Note that a more specialised version of this definition, fixing the coupling
  invariant @{term P} to be the one that relates all configurations with
  identical programs and mode states, appeared in Murray et al., CSF 2016.
  Here we generalise the theory to support a wider class of coupling invariants.
›
definition
  simpler_refinement_safe 
where
  "simpler_refinement_safe ℛA ℛ P abs_steps ≡ 
  ∀c1A mdsA mem1A c2A mem2A c1C mdsC mem1C c2C mem2C. (⟨c1A,mdsA,mem1A⟩A,⟨c2A,mdsA,mem2A⟩A) ∈ ℛA ∧ 
      (⟨c1A,mdsA,mem1A⟩A,⟨c1C, mdsC, mem1C⟩C) ∈ ℛ ∧ (⟨c2A,mdsA,mem2A⟩A,⟨c2C, mdsC, mem2C⟩C) ∈ ℛ ∧
       (⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C) ∈ P  ⟶
           (stopsC ⟨c1C, mdsC, mem1C⟩C = stopsC ⟨c2C, mdsC, mem2C⟩C) ∧
           (abs_steps ⟨c1A,mdsA,mem1A⟩A ⟨c1C, mdsC, mem1C⟩C = abs_steps ⟨c2A,mdsA,mem2A⟩A ⟨c2C, mdsC, mem2C⟩C) ∧
           (∀mds1C' mds2C' mem1C' mem2C' c1C' c2C'. ⟨c1C, mdsC, mem1C⟩C ↝C ⟨c1C', mds1C', mem1C'⟩C  ∧
                                          ⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mds2C', mem2C'⟩C ⟶
                                          (⟨c1C', mds1C', mem1C'⟩C, ⟨c2C', mds2C', mem2C'⟩C) ∈ P ∧
                                          mds1C' = mds2C')"

definition
  secure_refinement_simpler
where
  "secure_refinement_simpler ℛA ℛ P abs_steps ≡
  closed_others ℛ ∧
  preserves_modes_mem ℛ ∧
  new_vars_private ℛ ∧
  simpler_refinement_safe ℛA ℛ P abs_steps ∧
  conc.closed_glob_consistent P ∧
  (∀ c1A mdsA mem1A c1C mdsC mem1C. 
   (⟨ c1A, mdsA, mem1A ⟩A, ⟨ c1C, mdsC, mem1C ⟩C) ∈ ℛ ⟶
    (∀ c1C' mdsC' mem1C'. ⟨ c1C, mdsC, mem1C ⟩C ↝C ⟨ c1C', mdsC', mem1C' ⟩C ⟶
     (∃ c1A' mdsA' mem1A'. abs.neval ⟨ c1A, mdsA, mem1A ⟩A (abs_steps ⟨c1A,mdsA,mem1A⟩A ⟨c1C,mdsC,mem1C⟩C) ⟨ c1A', mdsA', mem1A' ⟩A ∧
                   (⟨ c1A', mdsA', mem1A' ⟩A, ⟨ c1C', mdsC', mem1C' ⟩C) ∈ ℛ)))"
    
lemma secure_refinement_simpler:
  assumes rrs: "secure_refinement_simpler ℛA ℛ P abs_steps"
  shows "secure_refinement ℛA ℛ P"
  unfolding secure_refinement_def
proof(safe)
  from rrs show "closed_others ℛ"
    unfolding secure_refinement_simpler_def by blast
next
  from rrs show "preserves_modes_mem ℛ"
    unfolding secure_refinement_simpler_def by blast
next
  from rrs show "new_vars_private ℛ"
    unfolding secure_refinement_simpler_def by blast
next
  fix c1A mdsA mem1A c1C mdsC mem1C c1C' mdsC' mem1C'
  let ?n = "abs_steps ⟨c1A,mdsA,mem1A⟩A ⟨c1C,mdsC,mem1C⟩C"
  assume in_ℛ1: "(⟨c1A, mdsA, mem1A⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ"
     and eval1C: "⟨c1C, mdsC, mem1C⟩C ↝C ⟨c1C', mdsC', mem1C'⟩C"
  with rrs obtain c1A' mdsA' mem1A' where
    neval1: "abs.neval ⟨ c1A, mdsA, mem1A ⟩A ?n ⟨ c1A', mdsA', mem1A' ⟩A" and
    in_ℛ1': "(⟨ c1A', mdsA', mem1A' ⟩A, ⟨ c1C', mdsC', mem1C' ⟩C) ∈ ℛ"
    unfolding secure_refinement_simpler_def by metis
  have "(∀c2A mem2A c2C mem2C c2A' mem2A'.
                (⟨c1A, mdsA, mem1A⟩A, ⟨c2A, mdsA, mem2A⟩A) ∈ ℛA ∧
                (⟨c2A, mdsA, mem2A⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ ∧
                (⟨c1C, mdsC, mem1C⟩C,⟨c2C, mdsC, mem2C⟩C) ∈ P ∧ abs.neval ⟨c2A, mdsA, mem2A⟩A ?n ⟨c2A', mdsA', mem2A'⟩A ⟶
                (∃c2C' mem2C'.
                    ⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C ∧
                    (⟨c2A', mdsA', mem2A'⟩A, ⟨c2C', mdsC', mem2C'⟩C) ∈ ℛ ∧ 
                    (⟨c1C', mdsC', mem1C'⟩C,⟨c2C', mdsC', mem2C'⟩C) ∈ P))"
  proof(clarsimp)
    fix c2A mem2A c2C mem2C c2A' mem2A'
    assume 
    in_ℛA: "(⟨c1A, mdsA, mem1A⟩A, ⟨c2A, mdsA, mem2A⟩A) ∈ ℛA" and 
    in_ℛ2: "(⟨c2A, mdsA, mem2A⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ" and
    neval2: "abs.neval ⟨c2A, mdsA, mem2A⟩A ?n ⟨c2A', mdsA', mem2A'⟩A" and
    in_P: "(⟨c1C, mdsC, mem1C⟩C,⟨c2C, mdsC, mem2C⟩C) ∈ P"
    have "∀c2C' mem2C'. ⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C ⟶ (⟨c2A', mdsA', mem2A'⟩A, ⟨c2C', mdsC', mem2C'⟩C) ∈ ℛ ∧ (⟨c1C', mdsC', mem1C'⟩C, ⟨c2C', mdsC', mem2C'⟩C) ∈ P"
    proof(clarify)
      fix c2C' mem2C'
      assume eval2C: "⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C"
      from in_ℛ2 eval2C in_P rrs obtain
      c2A'' mdsA'' mem2A'' where 
      neval2': "abs.neval ⟨ c2A, mdsA, mem2A ⟩A (abs_steps ⟨c2A,mdsA,mem2A⟩A ⟨c2C,mdsC,mem2C⟩C) ⟨ c2A'', mdsA'', mem2A'' ⟩A" and
      in_ℛ2': "(⟨ c2A'', mdsA'', mem2A'' ⟩A, ⟨ c2C', mdsC', mem2C' ⟩C) ∈ ℛ"
        unfolding secure_refinement_simpler_def by blast
      let ?n' = "(abs_steps ⟨c2A,mdsA,mem2A⟩A ⟨c2C,mdsC,mem2C⟩C)"
      from rrs have pe: "simpler_refinement_safe ℛA ℛ P abs_steps"
        unfolding secure_refinement_simpler_def by blast
      with in_ℛA in_ℛ1 in_ℛ2 in_P
      have "?n' = ?n"
        unfolding simpler_refinement_safe_def by fastforce
      with neval2 neval2' abs.neval_det 
      have [simp]: "c2A'' = c2A'"  and [simp]: "mdsA'' = mdsA'" and [simp]: "mem2A'' = mem2A'"
        by auto
      from in_ℛ2' have in_ℛ2': "(⟨c2A', mdsA', mem2A'⟩A, ⟨c2C', mdsC', mem2C'⟩C) ∈ ℛ" by simp
      from eval1C eval2C in_P have 
      in_P': "(⟨c1C', mdsC', mem1C'⟩C,⟨c2C', mdsC', mem2C'⟩C) ∈ P"
        using rrs unfolding secure_refinement_simpler_def
                            simpler_refinement_safe_def
        using in_ℛA in_ℛ1 in_ℛ2 in_P by auto
      with in_ℛ2'
      show "(⟨c2A', mdsA', mem2A'⟩A, ⟨c2C', mdsC', mem2C'⟩C) ∈ ℛ ∧
       (⟨c1C', mdsC', mem1C'⟩C, ⟨c2C', mdsC', mem2C'⟩C) ∈ P" by blast
    qed
    moreover have "∃c2C' mem2C'. ⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C"
    proof -
      from rrs have pe: "simpler_refinement_safe ℛA ℛ P abs_steps"
        unfolding secure_refinement_simpler_def by blast
      with in_ℛA in_ℛ1 in_ℛ2 in_P have "stopsC  ⟨c1C, mdsC, mem1C⟩C = stopsC  ⟨c2C, mdsC, mem2C⟩C"
        unfolding simpler_refinement_safe_def by blast
      moreover from eval1C have "¬ stopsC  ⟨c1C, mdsC, mem1C⟩C"
        unfolding stopsC_def by blast
      ultimately have "¬ stopsC  ⟨c2C, mdsC, mem2C⟩C"
        by simp          
      from this obtain c2C' mdsC'' mem2C'' where eval2C': "⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C',mdsC'',mem2C''⟩C"
        unfolding stopsC_def by auto
      with pe eval1C in_ℛA in_ℛ1 in_ℛ2 in_P have in_P': "(⟨c1C',mdsC', mem1C'⟩C, ⟨c2C',mdsC'', mem2C''⟩C) ∈ P"
                                             and [simp]: "mdsC'' = mdsC'"
        unfolding simpler_refinement_safe_def  by blast+
      from in_P' eval2C'
      show "∃c2C' mem2C'. ⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C"
        by fastforce
      qed
    ultimately show 
    "∃c2C' mem2C'.
     ⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C ∧ (⟨c2A', mdsA', mem2A'⟩A, ⟨c2C', mdsC', mem2C'⟩C) ∈ ℛ ∧ (⟨c1C', mdsC', mem1C'⟩C,
           ⟨c2C', mdsC', mem2C'⟩C)
          ∈ P"
      by blast
  qed
  with neval1 in_ℛ1 in_ℛ1' 
  show "∃n c1A' mdsA' mem1A'.
            abs.neval ⟨c1A, mdsA, mem1A⟩A n ⟨c1A', mdsA', mem1A'⟩A ∧
            (⟨c1A', mdsA', mem1A'⟩A, ⟨c1C', mdsC', mem1C'⟩C) ∈ ℛ ∧
            (∀c2A mem2A c2C mem2C c2A' mem2A'.
                (⟨c1A, mdsA, mem1A⟩A, ⟨c2A, mdsA, mem2A⟩A) ∈ ℛA ∧
                (⟨c2A, mdsA, mem2A⟩A, ⟨c2C, mdsC, mem2C⟩C) ∈ ℛ ∧
                (⟨c1C, mdsC, mem1C⟩C, ⟨c2C, mdsC, mem2C⟩C)
                ∈ P ∧
                abs.neval ⟨c2A, mdsA, mem2A⟩A n ⟨c2A', mdsA', mem2A'⟩A ⟶
                (∃c2C' mem2C'.
                    ⟨c2C, mdsC, mem2C⟩C ↝C ⟨c2C', mdsC', mem2C'⟩C ∧
                    (⟨c2A', mdsA', mem2A'⟩A, ⟨c2C', mdsC', mem2C'⟩C) ∈ ℛ ∧
                    (⟨c1C', mdsC', mem1C'⟩C, ⟨c2C', mdsC', mem2C'⟩C)
                    ∈ P))"
    by auto
next
  show "conc.closed_glob_consistent P"
    using rrs unfolding secure_refinement_simpler_def by blast
qed

section "Simple Bisimulations and Simple Refinement"

text ‹
  We derive the theory of simple refinements from Murray et al. CSF 2016 from the above
  \emph{simpler} theory of secure refinement.
›

definition
   bisim_simple
where
  "bisim_simple ℛA ≡ ∀c1A mds mem1A c2A mem2A. (⟨c1A,mds,mem1A⟩A,⟨c2A,mds,mem2A⟩A) ∈ ℛA ⟶ 
                                              c1A = c2A"
definition
  simple_refinement_safe
where
  "simple_refinement_safe ℛA ℛ abs_steps ≡ 
  ∀cA mdsA mem1A mem2A cC mdsC mem1C mem2C. (⟨cA,mdsA,mem1A⟩A,⟨cA,mdsA,mem2A⟩A) ∈ ℛA ∧ 
      (⟨cA,mdsA,mem1A⟩A,⟨cC, mdsC, mem1C⟩C) ∈ ℛ ∧ (⟨cA,mdsA,mem2A⟩A,⟨cC, mdsC, mem2C⟩C) ∈ ℛ ⟶
           (stopsC ⟨cC, mdsC, mem1C⟩C = stopsC ⟨cC, mdsC, mem2C⟩C) ∧
           (abs_steps ⟨cA,mdsA,mem1A⟩A ⟨cC, mdsC, mem1C⟩C = abs_steps ⟨cA,mdsA,mem2A⟩A ⟨cC, mdsC, mem2C⟩C) ∧
           (∀mds1C' mds2C' mem1C' mem2C' c1C' c2C'. ⟨cC, mdsC, mem1C⟩C ↝C ⟨c1C', mds1C', mem1C'⟩C  ∧
                                          ⟨cC, mdsC, mem2C⟩C ↝C ⟨c2C', mds2C', mem2C'⟩C ⟶
                                          c1C' = c2C' ∧ mds1C' = mds2C')"

definition
  secure_refinement_simple
where
  "secure_refinement_simple ℛA ℛ abs_steps ≡
  closed_others ℛ ∧
  preserves_modes_mem ℛ ∧
  new_vars_private ℛ ∧
  simple_refinement_safe ℛA ℛ abs_steps ∧
  bisim_simple ℛA ∧
  (∀ c1A mdsA mem1A c1C mdsC mem1C. 
   (⟨ c1A, mdsA, mem1A ⟩A, ⟨ c1C, mdsC, mem1C ⟩C) ∈ ℛ ⟶
    (∀ c1C' mdsC' mem1C'. ⟨ c1C, mdsC, mem1C ⟩C ↝C ⟨ c1C', mdsC', mem1C' ⟩C ⟶
     (∃ c1A' mdsA' mem1A'. abs.neval ⟨ c1A, mdsA, mem1A ⟩A (abs_steps ⟨c1A,mdsA,mem1A⟩A ⟨c1C,mdsC,mem1C⟩C) ⟨ c1A', mdsA', mem1A' ⟩A ∧
                   (⟨ c1A', mdsA', mem1A' ⟩A, ⟨ c1C', mdsC', mem1C' ⟩C) ∈ ℛ)))"

definition
  ℐsimple
where
  "ℐsimple ≡ {(⟨c,mds,mem⟩C,⟨c',mds',mem'⟩C)| c mds mem c' mds' mem'. c = c'}"

lemma ℐsimple_closed_glob_consistent:
  "conc.closed_glob_consistent ℐsimple"
  by(auto simp: conc.closed_glob_consistent_def ℐsimple_def)
  
lemma secure_refinement_simple:
  assumes srs: "secure_refinement_simple ℛA ℛ abs_steps"
  shows "secure_refinement_simpler ℛA ℛ ℐsimple abs_steps"
unfolding secure_refinement_simpler_def
proof(safe | clarsimp)+
  from srs show "closed_others ℛ"
  unfolding secure_refinement_simple_def by blast
next
  from srs show "preserves_modes_mem ℛ"
  unfolding secure_refinement_simple_def by blast
next
  from srs show "new_vars_private ℛ"
  unfolding secure_refinement_simple_def by blast
next
  show "conc.closed_glob_consistent ℐsimple" by (rule ℐsimple_closed_glob_consistent)
next
  from srs have safe: "simple_refinement_safe ℛA ℛ abs_steps"
  unfolding secure_refinement_simple_def by blast
  from srs have simple: "bisim_simple ℛA"
  unfolding secure_refinement_simple_def by fastforce
  
  from safe simple show "simpler_refinement_safe ℛA ℛ ℐsimple abs_steps"
  by(fastforce simp: simpler_refinement_safe_def ℐsimple_def simple_refinement_safe_def bisim_simple_def)
next
  fix c1A mdsA mem1A c1C mdsC mem1C c1C' mdsC' mem1C'
  show " (⟨c1A, mdsA, mem1A⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ ℛ ⟹
       ⟨c1C, mdsC, mem1C⟩C ↝C ⟨c1C', mdsC', mem1C'⟩C ⟹
       ∃c1A' mdsA' mem1A'.
          abs.neval ⟨c1A, mdsA, mem1A⟩A (abs_steps ⟨c1A, mdsA, mem1A⟩A ⟨c1C, mdsC, mem1C⟩C)
           ⟨c1A', mdsA', mem1A'⟩A ∧
          (⟨c1A', mdsA', mem1A'⟩A, ⟨c1C', mdsC', mem1C'⟩C) ∈ ℛ"
    using srs unfolding secure_refinement_simple_def by blast
qed
  
section "Sound Mode Use Preservation"

text ‹
  Prove that
  \begin{quote}
  acquiring a mode on the concrete version of an abstract
      variable~@{term x}, and then mapping the new concrete mode state to the
      corresponding abstract mode state,
  \end{quote}
   is equivalent to
   \begin{quote}
      first mapping the initial concrete mode
      state to its corresponding abstract mode state and then acquiring the mode
      on the abstract variable~@{term x}.
   \end{quote}

   This lemma essentially justifies why a concrete program doing
   @{term "Acq (varC_of x) SomeMode"}
   is a the right way to implement the abstract program doing
   @{term "Acq x SomeMode"}.
›

(* FIXME: There might be better names for these *)
lemma mode_acquire_refinement_helper:
  "mdsA_of (mdsC(SomeMode := insert (varC_of x) (mdsC SomeMode))) =
   (mdsA_of mdsC)(SomeMode := insert x (mdsA_of mdsC SomeMode))"
  apply(clarsimp simp: mdsA_of_def)
  apply(rule ext)
  apply(force simp: image_def inv_f_f[OF varC_of_inj])
  done

lemma mode_release_refinement_helper:
  "mdsA_of (mdsC(SomeMode := {y ∈ mdsC SomeMode. y ≠ (varC_of x)})) =
   (mdsA_of mdsC)(SomeMode := {y ∈ (mdsA_of mdsC SomeMode). y ≠ x})"
  apply(clarsimp simp: mdsA_of_def)
  apply(rule ext)
  apply (force simp: image_def inv_f_f[OF varC_of_inj])
  done

definition
  preserves_locally_sound_mode_use :: "('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation ⇒ bool"
where
  "preserves_locally_sound_mode_use ℛ ≡
   ∀lcA lcC.
      (abs.locally_sound_mode_use lcA ∧ (lcA, lcC) ∈ ℛ ⟶
      conc.locally_sound_mode_use lcC)"

lemma secure_refinement_loc_reach:
  assumes rr: "secure_refinement ℛA ℛ P"
  assumes in_ℛ:  "(⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ ℛ"
  assumes loc_reachC: "⟨cC', mdsC', memC'⟩C ∈ conc.loc_reach ⟨cC, mdsC, memC⟩C"
  shows "∃cA' mdsA' memA'.
      (⟨cA', mdsA', memA'⟩A, ⟨cC', mdsC', memC'⟩C) ∈ ℛ ∧
      ⟨cA', mdsA', memA'⟩A ∈ abs.loc_reach ⟨cA, mdsA, memA⟩A"
using loc_reachC proof(induct rule: conc.loc_reach.induct)
  case (refl) show ?case
    using in_ℛ abs.loc_reach.refl by force
next
  case (step cC' mdsC' memC' cC'' mdsC'' memC'')
  from step(2) obtain cA' mdsA' memA' where 
    in_ℛ': "(⟨cA', mdsA', memA'⟩A, ⟨cC', mdsC', memC'⟩C) ∈ ℛ" and 
    loc_reachA: "⟨cA', mdsA', memA'⟩A ∈ abs.loc_reach ⟨cA, mdsA, memA⟩A "
    by blast
  from rr in_ℛ' step(3)
  obtain n cA'' mdsA'' memA'' where 
    nevalA: "abs.neval ⟨ cA', mdsA', memA' ⟩A n ⟨ cA'', mdsA'', memA'' ⟩A" and
    in_ℛ'': "(⟨ cA'', mdsA'', memA'' ⟩A, ⟨ cC'', mdsC'', memC'' ⟩C) ∈ ℛ"
    unfolding secure_refinement_def by blast
  from nevalA loc_reachA have "⟨cA'', mdsA'', memA''⟩A ∈ abs.loc_reach ⟨cA, mdsA, memA⟩A"
    using abs.neval_loc_reach
    by blast
  with in_ℛ'' show ?case by blast
next
  case (mem_diff cC' mdsC' memC' memC'')
  from mem_diff(2) obtain cA' mdsA' memA' where 
    in_ℛ': "(⟨cA', mdsA', memA'⟩A, ⟨cC', mdsC', memC'⟩C) ∈ ℛ" and 
    loc_reachA: "⟨cA', mdsA', memA'⟩A ∈ abs.loc_reach ⟨cA, mdsA, memA⟩A "
    by blast
  from rr have mm: "preserves_modes_mem ℛ" and co: "closed_others ℛ"
    unfolding secure_refinement_def by blast+
  from preserves_modes_memD[OF mm in_ℛ'] have 
    memA'_def: "memA' = memA_of memC'" and mdsA'_def: "mdsA' = mdsA_of mdsC'"
    by simp+
  hence in_ℛ': "(⟨cA', mdsA_of mdsC', memA_of memC'⟩A, ⟨cC', mdsC', memC'⟩C) ∈ ℛ"
   and loc_reachA: "(⟨cA', mdsA_of mdsC', memA_of memC'⟩A) ∈ abs.loc_reach ⟨cA, mdsA, memA⟩A"
    using in_ℛ' loc_reachA by simp+
  with mem_diff(3) co
  have "(⟨cA', mdsA_of mdsC', memA_of memC''⟩A, ⟨cC', mdsC', memC''⟩C) ∈ ℛ"
    unfolding closed_others_def by blast
  moreover have "⟨cA', mdsA_of mdsC', memA_of memC''⟩A ∈ abs.loc_reach ⟨cA, mdsA, memA⟩A"
    apply(rule abs.loc_reach.mem_diff)
     apply(rule loc_reachA)
    using mem_diff(3)
    using calculation in_ℛ' in_ℛ_dma' memA_of_def mm var_writableA by fastforce 
  ultimately show ?case by blast
qed

definition preserves_local_guarantee_compliance ::
  "('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation ⇒ bool"
where
  "preserves_local_guarantee_compliance ℛ ≡
    ∀cmA memA cmC memC.
      abs.respects_own_guarantees cmA ∧
      ((cmA, memA), (cmC, memC)) ∈ ℛ ⟶
        conc.respects_own_guarantees cmC"

lemma preserves_local_guarantee_compliance_def2:
  "preserves_local_guarantee_compliance ℛ ≡
    ∀cA mdsA memA cC mdsC memC.
      abs.respects_own_guarantees (cA, mdsA) ∧
      (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ ℛ ⟶
        conc.respects_own_guarantees (cC, mdsC)"
  unfolding preserves_local_guarantee_compliance_def
  by simp

(* This lemma proves it is sufficient to require a refinement relation to preserve
   guarantee compliance to ensure that it also preserves locally sound mode use.
  TODO: Should preserves_guarantee_compliance become part of secure_refinement's requirements? *)
lemma locally_sound_mode_use_preservation:
  assumes rr: "secure_refinement ℛA ℛ P"
  assumes preserves_guarantee_compliance: "preserves_local_guarantee_compliance ℛ"
  shows "preserves_locally_sound_mode_use ℛ"
  unfolding preserves_locally_sound_mode_use_def
proof(clarsimp)
  fix cA mdsA memA cC mdsC memC
  assume locally_soundA: "abs.locally_sound_mode_use ⟨cA, mdsA, memA⟩A" and
         in_ℛ: "(⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ ℛ"
 
  show "conc.locally_sound_mode_use ⟨cC, mdsC, memC⟩C"
    unfolding conc.locally_sound_mode_use_def2
    proof(clarsimp)
      fix cC' mdsC' memC'
      assume loc_reachC: "⟨cC', mdsC', memC'⟩C ∈ conc.loc_reach ⟨cC, mdsC, memC⟩C"

      from rr in_ℛ loc_reachC
      obtain cA' mdsA' memA' where
        in_ℛ': "(⟨cA', mdsA', memA'⟩A, ⟨cC', mdsC', memC'⟩C) ∈ ℛ" and
        loc_reachA: "⟨cA', mdsA', memA'⟩A ∈ abs.loc_reach ⟨cA, mdsA, memA⟩A"
        using secure_refinement_loc_reach by blast

      from locally_soundA loc_reachA
      have respects_guaranteesA': "abs.respects_own_guarantees (cA', mdsA')"
        unfolding abs.locally_sound_mode_use_def2 by auto

      with preserves_guarantee_compliance in_ℛ'
      show "conc.respects_own_guarantees (cC', mdsC')"
        unfolding preserves_local_guarantee_compliance_def by blast
    qed
qed

end

section "Refinement without changing the Memory Model"

text ‹
  Here we define a locale which restricts the refinement to be between an abstract and
  concrete programs that share identical memory models: i,e. have the same set of variables.
  This allows us to derive simpler versions of the conditions that are likely to be easier
  to work with for initial experimentation.
›
locale sifum_refinement_same_mem = 
  abs: sifum_security dma 𝒞_vars 𝒞 evalA some_val +
  conc: sifum_security dma 𝒞_vars 𝒞 evalC some_val
  for dma :: "('Var,'Val) Mem ⇒ 'Var ⇒ Sec"
  and 𝒞_vars :: "'Var ⇒ 'Var set"
  and 𝒞 :: "'Var set"
  and evalA :: "('ComA, 'Var, 'Val) LocalConf rel"
  and evalC :: "('ComC, 'Var, 'Val) LocalConf rel"
  and some_val :: "'Val" 

sublocale sifum_refinement_same_mem ⊆ 
          gen_refine: sifum_refinement dma dma 𝒞_vars 𝒞_vars 𝒞 𝒞 evalA evalC some_val id
  by(unfold_locales, simp_all)

context sifum_refinement_same_mem begin

lemma [simp]:
  "gen_refine.new_vars_private ℛ"
  unfolding gen_refine.new_vars_private_def
  by simp

definition
  preserves_modes_mem :: "('ComA, 'Var, 'Val, 'ComC, 'Var) state_relation ⇒ bool"
where
  "preserves_modes_mem ℛ ≡ 
  (∀ cA mdsA memA cC mdsC memC. (⟨ cA, mdsA, memA ⟩A, ⟨ cC, mdsC, memC ⟩C) ∈ ℛ ⟶
      memA = memC ∧ mdsA = mdsC)"


definition
  closed_others :: "('ComA, 'Var, 'Val, 'ComC, 'Var) state_relation ⇒ bool"
where
  "closed_others ℛ ≡ 
  (∀ cA mds mem cC mem'. (⟨ cA, mds, mem ⟩A, ⟨ cC, mds, mem ⟩C) ∈ ℛ ⟶
   (∀x. mem x ≠ mem' x ⟶ ¬ var_asm_not_written mds x) ⟶
   (∀x. dma mem x ≠ dma mem' x ⟶ ¬ var_asm_not_written mds x) ⟶
         (⟨ cA, mds, mem' ⟩A, ⟨ cC, mds, mem' ⟩C) ∈ ℛ)"

lemma [simp]:
  "gen_refine.mdsA_of x = x"
  by(simp add: gen_refine.mdsA_of_def)

lemma [simp]:
  "gen_refine.memA_of x = x"
  by(simp add: gen_refine.memA_of_def)

lemma [simp]:
  "preserves_modes_mem ℛ ⟹
  gen_refine.closed_others ℛ = closed_others ℛ"
  unfolding closed_others_def
            gen_refine.closed_others_def
            preserves_modes_mem_def
  by auto

lemma [simp]:
  "gen_refine.preserves_modes_mem ℛ = preserves_modes_mem ℛ"
  unfolding gen_refine.preserves_modes_mem_def2 preserves_modes_mem_def
  by simp

definition
  secure_refinement :: "('ComA, 'Var, 'Val) LocalConf rel ⇒ ('ComA, 'Var, 'Val, 'ComC, 'Var) state_relation ⇒ 
                          ('ComC, 'Var, 'Val) LocalConf rel ⇒ bool"
where
  "secure_refinement ℛA ℛ P ≡
  closed_others ℛ ∧
  preserves_modes_mem ℛ ∧
  conc.closed_glob_consistent P ∧
  (∀ c1A mds mem1 c1C. 
   (⟨ c1A, mds, mem1 ⟩A, ⟨ c1C, mds, mem1 ⟩C) ∈ ℛ ⟶
    (∀ c1C' mds' mem1'. ⟨ c1C, mds, mem1 ⟩C ↝C ⟨ c1C', mds', mem1' ⟩C ⟶
     (∃ n c1A'. abs.neval ⟨ c1A, mds, mem1 ⟩A n ⟨ c1A', mds', mem1' ⟩A ∧
                   (⟨ c1A', mds', mem1' ⟩A, ⟨ c1C', mds', mem1' ⟩C) ∈ ℛ ∧
       (∀c2A mem2 c2C c2A' mem2'. 
         (⟨ c1A, mds, mem1 ⟩A, ⟨ c2A, mds, mem2 ⟩A) ∈ ℛA ∧
         (⟨ c2A, mds, mem2 ⟩A, ⟨ c2C, mds, mem2 ⟩C) ∈ ℛ ∧
         (⟨c1C, mds, mem1⟩C, ⟨c2C, mds, mem2⟩C) ∈ P  ∧
         abs.neval ⟨ c2A, mds, mem2 ⟩A n ⟨ c2A', mds', mem2' ⟩A  ⟶
           (∃ c2C' . ⟨ c2C, mds, mem2 ⟩C ↝C ⟨ c2C', mds', mem2' ⟩C ∧
                   (⟨ c2A', mds', mem2' ⟩A, ⟨ c2C', mds', mem2' ⟩C) ∈ ℛ ∧
                   (⟨c1C', mds', mem1'⟩C, ⟨c2C', mds', mem2'⟩C) ∈ P )))))"

lemma preserves_modes_memD:
  "preserves_modes_mem ℛ ⟹
(⟨ cA, mdsA, memA ⟩A, ⟨ cC, mdsC, memC ⟩C) ∈ ℛ ⟹
      memA = memC ∧ mdsA = mdsC"
  by(auto simp: preserves_modes_mem_def)

lemma [simp]:
  "gen_refine.secure_refinement ℛA ℛ P = secure_refinement ℛA ℛ P"
  unfolding gen_refine.secure_refinement_def secure_refinement_def
  apply safe
         apply fastforce
        apply fastforce
       defer
       apply fastforce
      apply fastforce
     apply fastforce
    defer
   apply ((drule spec)+, erule (1) impE)
   apply ((drule spec)+, erule (1) impE)
   apply (clarify)
   apply(rename_tac  n c1A' mdsA' mem1A')
   apply(rule_tac x=n in exI)
   apply(rule_tac x=c1A' in exI)
   apply(fastforce dest: preserves_modes_memD)
  apply (frule (1) preserves_modes_memD)
  apply clarify
  apply ((drule spec)+, erule (1) impE)
  apply ((drule spec)+, erule (1) impE)
  apply clarify
  apply(blast dest: preserves_modes_memD)
  done
  
lemma RC_of_strong_low_bisim_mm:
  assumes abs: "abs.strong_low_bisim_mm ℛA"
  assumes rr: "secure_refinement ℛA ℛ P"
  assumes P_sym: "sym P"
  shows "conc.strong_low_bisim_mm (gen_refine.RC_of ℛA ℛ P)"
  using abs rr gen_refine.RC_of_strong_low_bisim_mm[OF _ _ P_sym]
  by simp

end

context sifum_refinement begin
lemma use_secure_refinement_helper:
  "secure_refinement ℛA ℛ P ⟹
   ((cmA,memA),(cmC,memC)) ∈ ℛ ⟹ (cmC,memC) ↝C (cmC',memC') ⟹
   (∃cmA' memA' n. abs.neval (cmA,memA) n (cmA',memA') ∧
                 ((cmA',memA'), (cmC',memC')) ∈ ℛ)"
  apply(case_tac cmA, case_tac cmC)
  apply clarsimp
  apply(clarsimp simp: secure_refinement_def)
  by (metis surjective_pairing)
  
lemma closed_othersD:
  "closed_others ℛ ⟹
   (⟨cA, mdsA_of mdsC, memA_of memC⟩A, ⟨cC, mdsC, memC⟩C) ∈ ℛ ⟹
   (⋀x. memC' x ≠ memC x ∨ dmaC memC' x ≠ dmaC memC x ⟹ ¬ var_asm_not_written mdsC x) ⟹
   (⟨cA, mdsA_of mdsC, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ ℛ"
   unfolding closed_others_def
   by auto
end

record ('a, 'Val, 'VarC, 'ComC, 'VarA, 'ComA) componentwise_refinement =
  priv_mem :: "'VarC set" (* private variables *)
  ℛA_rel :: "('ComA, 'VarA, 'Val) LocalConf rel" (* abstract bisimulation *)
  ℛ_rel :: "('ComA, 'VarA, 'Val, 'ComC, 'VarC) state_relation" (* refinement relation *)
  P_rel :: "('ComC, 'VarC, 'Val) LocalConf rel"

section "Whole System Refinement"

text ‹
  A locale to capture componentwise refinement of an entire system.
›
locale sifum_refinement_sys = 
  sifum_refinement dmaA dmaC 𝒞_varsA 𝒞_varsC 𝒞A 𝒞C evalA evalC some_val varC_of
  for dmaA :: "('VarA,'Val) Mem ⇒ 'VarA ⇒ Sec"
  and dmaC :: "('VarC,'Val) Mem ⇒ 'VarC ⇒ Sec"
  and 𝒞_varsA :: "'VarA ⇒ 'VarA set"
  and 𝒞_varsC :: "'VarC ⇒ 'VarC set"
  and 𝒞A :: "'VarA set"
  and 𝒞C :: "'VarC set"
  and evalA :: "('ComA, 'VarA, 'Val) LocalConf rel"
  and evalC :: "('ComC, 'VarC, 'Val) LocalConf rel"
  and some_val :: "'Val"
  and varC_of :: "'VarA ⇒ 'VarC" +
  fixes cms :: "('a::wellorder, 'Val, 'VarC, 'ComC, 'VarA, 'ComA) componentwise_refinement list" 
  fixes priv_memC :: "'VarC set list"
  defines priv_memC_def: "priv_memC ≡ map priv_mem cms"
  assumes priv_mem_disjoint: "i < length cms ⟹ j < length cms ⟹ i ≠ j ⟹ priv_memC ! i ∩ priv_memC ! j = {}"
  assumes new_vars_priv: "- range varC_of = ⋃ (set priv_memC)"
  assumes new_privs_preserved: "⟨c, mds, mem⟩C ↝C ⟨c', mds', mem'⟩C ⟹ x ∉ range varC_of ⟹
                                 (x ∈ mds m) = (x ∈ mds' m)"
  assumes secure_refinements: 
    "i < length cms ⟹ secure_refinement (ℛA_rel (cms ! i)) (ℛ_rel (cms ! i)) (P_rel (cms ! i))"
  assumes local_guarantee_preservation:
    "i < length cms ⟹ preserves_local_guarantee_compliance (ℛ_rel (cms ! i))"
  assumes bisims:
    "i < length cms ⟹ abs.strong_low_bisim_mm (ℛA_rel (cms ! i))"
  assumes Ps_sym:
    "⋀a b. i < length cms ⟹ sym (P_rel (cms ! i))"
  assumes Ps_refl_on_low_mds_eq:
    "i < length cms ⟹ conc.low_mds_eq mdsC memC memC' ⟹ (⟨cC, mdsC, memC⟩C, ⟨cC, mdsC, memC'⟩C) ∈ (P_rel (cms ! i))" 

(* FIXME: move to a parent theory? *)
context sifum_security begin
lemma neval_modifies_helper:
  assumes nevaln: "neval lcn m lcn'"
  assumes lcn_def: "lcn = (cms ! n, mem)"
  assumes lcn'_def: "lcn' = (cmn', mem')"
  assumes len: "n < length cms"
  assumes modified: "mem x ≠ mem' x ∨ dma mem x ≠ dma mem' x"
  shows "∃k cmn'' mem'' cmn''' mem'''. k < m ∧ neval (cms ! n,mem) k (cmn'',mem'') ∧
                           (cmn'',mem'') ↝ (cmn''', mem''') ∧
                           (mem'' x ≠ mem''' x ∨ dma mem'' x ≠ dma mem''' x)"
using nevaln lcn_def lcn'_def modified len
proof(induct arbitrary: cms cmn' mem mem' rule: neval.induct)
  case (neval_0 lcn lcn')
    from neval_0 show ?case by simp
  next
  case (neval_S_n lcn lcn'' m lcn')
  obtain cmn'' mem'' where lcn''_def: "lcn'' = (cmn'', mem'')" by fastforce
  show ?case
  proof(cases "mem x ≠ mem'' x ∨ dma mem x ≠ dma mem'' x")    
    assume a: "mem x ≠ mem'' x ∨ dma mem x ≠ dma mem'' x"
    let ?k = "0::nat"
    let ?cmn'' = "cms ! n"
    let ?mem'' = "mem"
    have "?k < Suc m ∧
    neval (cms ! n, mem) ?k (?cmn'', ?mem'') ∧
    (?cmn'', ?mem'') ↝ (cmn'', mem'') ∧ (?mem'' x ≠ mem'' x ∨
    dma ?mem'' x ≠ dma mem'' x)"
      apply (rule conjI, simp add: neval.neval_0)+
      apply (simp only: a)
      by (simp add: neval_S_n(1)[simplified neval_S_n lcn''_def])
    thus ?case by blast
  next
    assume a: "¬ (mem x ≠ mem'' x ∨ dma mem x ≠ dma mem'' x)"
    hence unchanged: "mem'' x = mem x ∧ dma mem'' x = dma mem x"
      by (blast intro: sym)
    define cms'' where "cms'' = cms[n := cmn'']"
    have len'': "n < length cms''"
      by(simp add: cms''_def neval_S_n)
    hence lcn''_def2: "lcn'' = (cms'' ! n, mem'')"
      by(simp add: lcn''_def cms''_def)
    from
    neval_S_n(3)[OF lcn''_def2 neval_S_n(5), simplified unchanged neval_S_n len'']
    obtain k cmn''' mem''' cmn'''' mem'''' where
      hyp:    "k < m ∧
          neval (cms'' ! n, mem'') k (cmn''', mem''') ∧
          (cmn''', mem''') ↝ (cmn'''', mem'''') ∧
          (mem''' x ≠ mem'''' x ∨ dma mem''' x ≠ dma mem'''' x)"
      by blast
    have "neval (cms ! n, mem) (Suc k) (cmn''', mem''')"           
      apply(rule neval.neval_S_n)  
       prefer 2
       using hyp apply fastforce 
      apply(simp add: cms''_def neval_S_n)
      by(rule neval_S_n(1)[simplified neval_S_n lcn''_def])
    moreover have "Suc k < Suc m" using hyp by auto
    ultimately show ?case using hyp by fastforce
  qed
qed

lemma neval_sched_Nil [simp]:
  "(cms, mem) →⇘[]⇙ (cms, mem)"
  by simp
  
lemma reachable_mode_states_refl:
  "map snd cms ∈ reachable_mode_states (cms, mem)"
  apply(clarsimp simp: reachable_mode_states_def)
  using neval_sched_Nil by blast
  
lemma neval_reachable_mode_states:
  assumes neval: "neval lc n lc'"
  assumes lc_def: "lc = (cms ! k, mem)" 
  assumes len: "k < length cms"
  shows "map snd (cms[k := (fst lc')]) ∈ reachable_mode_states (cms, mem)"
using neval lc_def len proof(induct arbitrary: cms mem rule: neval.induct)
case (neval_0 x y)
  thus ?case
  apply simp
  apply(drule sym, simp add: len reachable_mode_states_refl)
  done
next
case (neval_S_n x y n z)
  define cms' where "cms' = cms[k := fst y]"
  define mem' where "mem' = snd y"
  have y_def: "y = (cms' ! k, mem')"
    by(simp add: cms'_def mem'_def neval_S_n)
  moreover have len': "k < length cms'"
    by(simp add: cms'_def neval_S_n)
  ultimately have hyp: "map snd (cms'[k := fst z]) ∈ reachable_mode_states (cms', mem')"
    using neval_S_n by metis
  have "map snd (cms'[k := fst z]) = map snd (cms[k := fst z])"
    unfolding cms'_def
    by simp
  moreover have "(cms, mem) ↝⇘k⇙ (cms', mem')"
    using meval_intro neval_S_n y_def cms'_def mem'_def len' by fastforce 
  ultimately show ?case
  using reachable_modes_subset subsetD hyp by fastforce
qed


lemma meval_sched_sound_mode_use:
  "sound_mode_use gc ⟹ meval_sched sched gc gc' ⟹ sound_mode_use gc'"
proof(induct rule: meval_sched.induct)
case (1 gc)
  thus ?case by simp
next
case (2 n ns gc gc')
  from 2(3) obtain gc'' where "meval_abv gc n gc''" and a: "meval_sched ns gc'' gc'" by force
  with 2(2) sound_modes_invariant have b: "sound_mode_use gc''" by (metis surjective_pairing)
  show ?case by (rule 2(1)[OF b a])
qed

lemma neval_meval:
  "neval lcn k lcn' ⟹ n < length cms ⟹ lcn = (cms ! n,mem) ⟹ lcn' = (cmn', mem') ⟹
  meval_sched (replicate k n) (cms,mem) (cms[n := cmn'],mem')"
proof(induct arbitrary: cms mem cmn' mem' rule: neval.induct)
case (neval_0 lcn lcn')  
  thus ?case by fastforce
next
case (neval_S_n lcn lcn'' k lcn')
  define cms'' where [simp]: "cms'' = cms[n := fst lcn'']"
  define mem'' where [simp]: "mem'' = snd lcn''"
  have len'' [simp]: "n < length cms''" by(simp add: neval_S_n(4))
  have lcn''_def: "lcn'' = (cms'' ! n, mem'')" using len'' by simp
  have hyp: "(cms'', mem'') →⇘replicate k n⇙ (cms''[n := cmn'], mem')"
    by (rule neval_S_n(3)[OF len'' lcn''_def neval_S_n(6)])
  have meval: "(cms, mem) ↝⇘n⇙ (cms'', mem'')"
    using cms''_def neval_S_n.hyps(1) neval_S_n.prems(1) neval_S_n.prems(2) by fastforce
  from hyp meval show ?case
    by fastforce
qed

lemma meval_sched_app:
  "meval_sched as gc gc' ⟹ meval_sched bs gc' gc'' ⟹ meval_sched (as@bs) gc gc''"
proof(induct as arbitrary: gc gc' bs)
case Nil thus ?case by simp
next
case (Cons a as)
  from Cons(2) 
  obtain gc''' where a: "meval_abv gc a gc'''" and as: "meval_sched as gc''' gc'" by force
  from Cons(1)[OF as Cons(3)] a
  have "gc →⇘a # (as @ bs)⇙ gc''"
    by (metis meval_sched.simps)
  thus ?case by simp
qed

end

context sifum_refinement_sys begin

lemma conc_respects_priv:
  assumes xnin: "xC ∉ range varC_of"
  assumes modifiedC: "memC xC ≠ memC' xC ∨ dmaC memC xC ≠ dmaC memC' xC"
  assumes evalC: "(cmsC ! n, memC) ↝C (cmCn', memC')"
  assumes in_ℛn: "((cmsA ! n, memA), cmsC ! n, memC) ∈ ℛn"
  assumes preserves: "preserves_local_guarantee_compliance ℛn"
  assumes sound_mode_useA: "abs.sound_mode_use (cmsA, memA)"
  assumes nlen: "n < length cms"
  assumes len_eq: "length cmsA = length cms"
  assumes len_eq': "length cmsC = length cms"
  shows "xC ∉ (snd (cmsC ! n)) GuarNoWrite ∧ xC ∉ (snd (cmsC ! n)) GuarNoReadOrWrite"
proof -
  from sound_mode_useA have "abs.respects_own_guarantees (cmsA ! n)"
    using nlen len_eq abs.locally_sound_respects_guarantees 
    unfolding abs.sound_mode_use_def list_all_length
    by fastforce
  with in_ℛn have 1: "conc.respects_own_guarantees (cmsC ! n)"
    using preserves
    unfolding preserves_local_guarantee_compliance_def
    by metis
  with evalC modifiedC have 2: "¬ conc.doesnt_modify (fst (cmsC ! n)) xC"
    unfolding conc.doesnt_modify_def
    by (metis surjective_pairing)
  then have "¬ conc.doesnt_read_or_modify (fst (cmsC ! n)) xC"
    using conc.doesnt_read_or_modify_doesnt_modify by metis
  with 1 2 show ?thesis
    unfolding conc.respects_own_guarantees_def 
    by metis
qed

lemma modified_variables_are_not_assumed_not_written:
  fixes cmsA memA cmsC memC cmCn' memC' ℛn cmAn' memA' mA ℛi
  assumes sound_mode_useA: "abs.sound_mode_use (cmsA, memA)"
  assumes pmmn: "preserves_modes_mem ℛn"
  assumes in_ℛn: "((cmsA ! n, memA), (cmsC ! n, memC)) ∈ ℛn"
  assumes pmmi: "preserves_modes_mem ℛi"
  assumes in_ℛi: "((cmsA ! i, memA), (cmsC ! i, memC)) ∈ ℛi"
  assumes nlen: "n < length cms"
  assumes lenA: "length cmsA = length cms"
  assumes lenC: "length cmsC = length cms"
  assumes priv_is_asm_priv: "⋀i. i < length cms ⟹ priv_memC ! i ⊆ snd (cmsC ! i) AsmNoReadOrWrite"
  assumes priv_is_guar_priv: "⋀i j. i < length cms ⟹ j < length cms ⟹ i ≠ j ⟹ priv_memC ! i ⊆ snd (cmsC ! j) GuarNoReadOrWrite"
  assumes new_asms_only_for_priv: "⋀i. i < length cms ⟹ 
                                           (snd (cmsC ! i) AsmNoReadOrWrite ∪ snd (cmsC ! i) AsmNoWrite) ∩ (- range varC_of) ⊆ priv_memC ! i"
  assumes evalCn: "(cmsC ! n,memC) ↝C (cmCn', memC')"
  assumes nevalAn: "abs.neval (cmsA ! n,memA) mA (cmAn', memA')"
  assumes in_ℛn': "((cmAn', memA'), (cmCn', memC')) ∈ ℛn"
  assumes modifiedC: "memC xC ≠ memC' xC ∨ dmaC memC xC ≠ dmaC memC' xC"
  assumes neq: "i ≠ n"
  assumes ilen: "i < length cms"
  assumes preserves: "preserves_local_guarantee_compliance ℛn"
  shows "¬ var_asm_not_written (snd (cmsC ! i)) xC"
proof(cases "xC ∈ range varC_of")
  assume "xC ∈ range varC_of"
  from this obtain xA where xC_def: "xC = varC_of xA" by blast
  obtain cAn mdsAn where [simp]: "cmsA ! n = (cAn, mdsAn)" by fastforce
  obtain cCn mdsCn where [simp]: "cmsC ! n = (cCn, mdsCn)" by fastforce
  obtain cCn' mdsCn' where [simp]: "cmCn' = (cCn', mdsCn')" by fastforce
  obtain cAn' mdsAn' where [simp]: "cmAn' = (cAn', mdsAn')" by fastforce

  from in_ℛn pmmn have [simp]: "memA = memA_of memC" and [simp]: "mdsAn = mdsA_of mdsCn"
    using preserves_modes_memD by auto
  from in_ℛn' pmmn have [simp]: "memA' = memA_of memC'" and [simp]: "mdsAn' = mdsA_of mdsCn'"
    using preserves_modes_memD by auto
  
  from modifiedC dma_consistent have 
    modifiedA: "memA xA ≠ memA' xA ∨ dmaA memA xA ≠ dmaA memA' xA"
    by (simp add: memA_of_def xC_def)
    
  from lenA nlen have nlenA: "n < length cmsA" by simp
  from lenA ilen have ilenA: "i < length cmsA" by simp

  from abs.neval_modifies_helper[OF nevalAn HOL.refl HOL.refl nlenA modifiedA]
  obtain kA cmAn'' memA'' cmAn''' memA''' 
  where "kA < mA" 
    and nevalAn'': "abs.neval (cmsA ! n, memA) kA (cmAn'', memA'')"
    and evalAn'': "(cmAn'', memA'') ↝A (cmAn''', memA''')"
    and modifiedA'': "(memA'' xA ≠ memA''' xA ∨ dmaA memA'' xA ≠ dmaA memA''' xA)" by blast
  let ?cAn'' = "fst cmAn''"
  let ?mdsAn'' = "snd cmAn''"
  from evalAn'' modifiedA'' have modifiesA'': "¬ abs.doesnt_modify ?cAn'' xA"
    unfolding abs.doesnt_modify_def
    by (metis surjective_pairing)
  have loc_reachA'': "(cmAn'', memA'') ∈ abs.loc_reach (cmsA ! n, memA)"
    apply(rule abs.neval_loc_reach)
     apply(rule nevalAn'')
    using abs.loc_reach.refl by simp
  have locally_sound_mode_useAn: "abs.locally_sound_mode_use  (cmsA ! n, memA)"
    using sound_mode_useA nlenA
    unfolding abs.sound_mode_use_def
    using list_all_length by fastforce
  from modifiesA'' loc_reachA'' locally_sound_mode_useAn abs.doesnt_read_or_modify_doesnt_modify
  have no_guarAn: "xA ∉ ?mdsAn'' GuarNoReadOrWrite ∧ xA ∉ ?mdsAn'' GuarNoWrite"
    unfolding abs.locally_sound_mode_use_def
    by (metis surjective_pairing)
  let ?mdssA'' = "map snd (cmsA[n := fst (cmAn'',memA'')])"
  have "?mdssA'' ∈ abs.reachable_mode_states (cmsA, memA)"
    apply(rule abs.neval_reachable_mode_states)
      apply(rule nevalAn'')
     apply(rule HOL.refl)
    by(rule nlenA)
  hence compat: "abs.compatible_modes ?mdssA''"
    using sound_mode_useA
    by(simp add: abs.globally_sound_mode_use_def)
  have n: "?mdssA'' ! n = ?mdsAn''"
    by(simp add: nlenA)
  let ?mdsAi = "snd (cmsA ! i)"
  have i: "?mdssA'' ! i = ?mdsAi"
    apply(simp add: ilenA)
    by(metis nth_list_update_neq neq)
  from nlenA have nlenA'': "n < length ?mdssA''" by simp
  from ilenA have ilenA'': "i < length ?mdssA''" by simp
  with compat n i nlenA'' ilenA'' no_guarAn neq
  have no_asmAi: "xA ∉ ?mdsAi AsmNoWrite ∧ xA ∉ ?mdsAi AsmNoReadOrWrite"
    unfolding abs.compatible_modes_def
    by metis

  obtain cAi mdsAi where [simp]: "cmsA ! i = (cAi, mdsAi)" by fastforce
  obtain cCi mdsCi where [simp]: "cmsC ! i = (cCi, mdsCi)" by fastforce

  from in_ℛi pmmi have [simp]: "mdsAi = mdsA_of mdsCi"
    using preserves_modes_memD by auto
  have [simp]: "?mdsAi = mdsAi" by simp
  from no_asmAi have no_asmCi: "xC ∉ mdsCi AsmNoWrite ∧ xC ∉ mdsCi AsmNoReadOrWrite"
    using xC_def mdsA_of_def
    using doesnt_have_mode by auto
  thus ?thesis
    unfolding var_asm_not_written_def
    by simp
next
  let ?mdsCn = "snd (cmsC ! n)"
  let ?mdsCi = "snd (cmsC ! i)"

  assume new_var: "xC ∉ range varC_of"
  from conc_respects_priv[OF new_var modifiedC evalCn in_ℛn preserves sound_mode_useA nlen lenA lenC] 
  have "xC ∉ ?mdsCn GuarNoWrite ∧ xC ∉ ?mdsCn GuarNoReadOrWrite" .
  with priv_is_guar_priv nlen ilen neq
  have "xC ∉ priv_memC ! i"
    by blast
  with new_var new_asms_only_for_priv ilen
  have "xC ∉ ?mdsCi AsmNoReadOrWrite ∪ ?mdsCi AsmNoWrite"
    by blast
  thus ?thesis
    unfolding var_asm_not_written_def
    by simp
qed

definition
  priv_is_asm_priv :: "'VarC Mds list ⇒ bool"
where
  "priv_is_asm_priv mdssC ≡  ∀i < length cms. priv_memC ! i ⊆ (mdssC ! i) AsmNoReadOrWrite"

definition
  priv_is_guar_priv :: "'VarC Mds list ⇒ bool"
where
  "priv_is_guar_priv mdssC ≡ 
    ∀i < length cms. (∀j < length cms. i ≠ j ⟶ priv_memC ! i ⊆ (mdssC ! j) GuarNoReadOrWrite)"
 
definition
  new_asms_only_for_priv :: "'VarC Mds list ⇒ bool"
where
  "new_asms_only_for_priv mdssC ≡ 
    ∀ i < length cms. 
      ((mdssC ! i) AsmNoReadOrWrite ∪ (mdssC ! i) AsmNoWrite) ∩ (- range varC_of) ⊆ priv_memC ! i"

definition
  new_asms_NoReadOrWrite_only :: "'VarC Mds list ⇒ bool"
where
  "new_asms_NoReadOrWrite_only mdssC ≡ 
    ∀ i < length cms. 
      (mdssC ! i) AsmNoWrite ∩ (- range varC_of) = {}"

definition
  modes_respect_priv :: "'VarC Mds list ⇒ bool"
where
  "modes_respect_priv mdssC  ≡ priv_is_asm_priv mdssC ∧ priv_is_guar_priv mdssC ∧
                               new_asms_only_for_priv mdssC ∧
                               new_asms_NoReadOrWrite_only mdssC"

definition
  ignores_old_vars :: "('VarC Mds list ⇒ bool) ⇒ bool"
where
  "ignores_old_vars P ≡ ∀mdss mdss'. length mdss = length mdss' ∧ length mdss' = length cms ⟶ 
    (map (λx m. x m ∩ (- range varC_of)) mdss) = (map (λx m. x m ∩ (- range varC_of)) mdss') ⟶ 
  P mdss = P mdss'"

lemma ignores_old_vars_conj:
  assumes Rdef: "(⋀x. R x = (P x ∧ Q x))"
  assumes iP: "ignores_old_vars P" 
  assumes iQ: "ignores_old_vars Q" 
  shows "ignores_old_vars R"
  unfolding ignores_old_vars_def
  apply(simp add: Rdef)
  apply(intro impI allI)
  apply(rule conj_cong)
   apply(erule (1) iP[unfolded ignores_old_vars_def, rule_format])
  apply(erule (1) iQ[unfolded ignores_old_vars_def, rule_format])
  done

  
lemma nth_map_eq': 
  "length xs = length ys ⟹ map f xs = map g ys ⟹ i < length xs ⟹ f (xs ! i) = g (ys ! i)"  
  apply(induct xs ys rule: list_induct2)
   apply simp
  apply(case_tac i)
   apply force
  by (metis length_map nth_map)

lemma nth_map_eq: 
  "map f xs = map g ys ⟹ i < length xs ⟹ f (xs ! i) = g (ys ! i)"
  apply(rule nth_map_eq')
    apply(erule map_eq_imp_length_eq)
   apply assumption+
  done

lemma nth_in_Union_over_set: 
  "i < length xs ⟹ xs ! i ⊆ ⋃(set xs)"
  by (simp add: Union_upper)

lemma priv_are_new_vars: 
  "x ∈ priv_memC ! i ⟹ i < length cms ⟹ x ∉ range varC_of"
  using new_vars_priv nth_in_Union_over_set subsetD
  using priv_memC_def by fastforce
  
lemma priv_is_asm_priv_ignores_old_vars:
  "ignores_old_vars priv_is_asm_priv"
  apply(clarsimp simp: ignores_old_vars_def priv_is_asm_priv_def)
  apply(rule all_cong)
  apply(drule nth_map_eq)
   apply simp
  apply(blast dest: priv_are_new_vars fun_cong)
  done
  
lemma priv_is_guar_priv_ignores_old_vars:
  "ignores_old_vars priv_is_guar_priv"
  apply(clarsimp simp: ignores_old_vars_def priv_is_guar_priv_def)
  apply(rule all_cong)
  apply(rule all_cong)
  apply(rule imp_cong)
   apply(rule HOL.refl)
  apply(frule nth_map_eq)
   apply simp
  apply(drule_tac i=j in nth_map_eq)
   apply simp
  apply(blast dest: priv_are_new_vars fun_cong)
  done

lemma new_asms_only_for_priv_ignores_old_vars:
  "ignores_old_vars new_asms_only_for_priv"
  apply(clarsimp simp: ignores_old_vars_def new_asms_only_for_priv_def)
  apply(rule all_cong)
  apply(drule nth_map_eq)
   apply simp
  apply(blast dest: priv_are_new_vars fun_cong)
  done

lemma new_asms_NoReadOrWrite_only_ignores_old_vars:
  "ignores_old_vars new_asms_NoReadOrWrite_only"
  apply(clarsimp simp: ignores_old_vars_def new_asms_NoReadOrWrite_only_def)
  apply(rule all_cong)
  apply(drule nth_map_eq)
   apply simp
  apply(blast dest: priv_are_new_vars fun_cong)
  done
  
lemma modes_respect_priv_ignores_old_vars:
   "ignores_old_vars modes_respect_priv"
   apply(rule ignores_old_vars_conj)
     apply(subst modes_respect_priv_def)
     apply(rule HOL.refl)
    apply(rule priv_is_asm_priv_ignores_old_vars)
   apply(rule ignores_old_vars_conj)
    apply(rule HOL.refl)
   apply(rule priv_is_guar_priv_ignores_old_vars)
  apply(rule ignores_old_vars_conj)
    apply(rule HOL.refl)
   apply(rule new_asms_only_for_priv_ignores_old_vars)
  apply(rule new_asms_NoReadOrWrite_only_ignores_old_vars)
  done
  
lemma ignores_old_varsD:
  "ignores_old_vars P ⟹ length mdss = length mdss' ⟹ length mdss' = length cms ⟹
  (map (λx m. x m ∩ (- range varC_of)) mdss) = (map (λx m. x m ∩ (- range varC_of)) mdss') ⟹ 
  P mdss = P mdss'"
  unfolding ignores_old_vars_def
  by force
  
lemma new_privs_preserved':
  "⟨c, mds, mem⟩C ↝C ⟨c', mds', mem'⟩C ⟹ (mds m ∩ (- range varC_of)) = (mds' m ∩ (- range varC_of))"
  using new_privs_preserved by blast

lemma map_nth_eq:
  "length xs = length ys ⟹ (⋀i. i < length xs ⟹ f (xs ! i) = g (ys ! i)) ⟹
  map f xs = map g ys"
  apply(induct xs ys rule: list_induct2)
   apply simp
  apply force
  done
  
lemma ignores_old_vars_conc_meval:
  assumes ignores: "ignores_old_vars P"
  assumes meval:  "conc.meval_abv gcC n gcC'"
  assumes len_eq: "length (fst gcC) = length cms"
  shows "P (map snd (fst gcC)) = P (map snd (fst gcC'))"
proof -
  obtain cmsC memC where [simp]: "gcC = (cmsC, memC)" by fastforce
  obtain cmsC' memC' where [simp]: "gcC' = (cmsC', memC')" by fastforce
  from meval obtain cmn' memC' where
    evalCn: "(cmsC ! n, memC) ↝C (cmn', memC')" and len: "n < length cmsC" and cmsC'_def: "cmsC' = cmsC[n := cmn']"
    using conc.meval.cases by fastforce
  have
    "P (map snd cmsC) = P (map snd cmsC')"
    apply(rule ignores_old_varsD[OF ignores])
      apply(simp add: cmsC'_def)
     using len_eq apply (simp add: cmsC'_def)
    apply(rule map_nth_eq)
     apply (simp add: cmsC'_def)
    apply(case_tac "i = n")
     apply simp
     apply(rule ext)
     apply(simp add: cmsC'_def)
     using evalCn new_privs_preserved' apply(metis surjective_pairing)
    by (simp add: cmsC'_def)
  thus ?thesis by simp
qed

lemma ignores_old_vars_conc_meval_sched:
  assumes ignores: "ignores_old_vars P"
  assumes meval_sched:  "conc.meval_sched sched gcC gcC'"
  assumes len_eq: "length (fst gcC) = length cms"
  shows "P (map snd (fst gcC)) = P (map snd (fst gcC'))"
using meval_sched len_eq proof(induct rule: conc.meval_sched.induct)
  case (1 gc gc')
  thus ?case by simp
next
  case (2 n ns gc gc')
  from 2(2) obtain gc'' where b: "conc.meval_abv gc n gc''" and a: "conc.meval_sched ns gc'' gc'" by force
  with 2 have "length (fst gc'') = length cms"
    using conc.meval.cases 
    by (metis length_list_update surjective_pairing)
  with 2 a b show ?case
  using ignores_old_vars_conc_meval ignores by metis 
qed

lemma meval_sched_modes_respect_priv:
  "conc.meval_sched sched gcC gcC' ⟹   length (fst gcC) = length cms ⟹
  modes_respect_priv (map snd (fst gcC)) ⟹
  modes_respect_priv (map snd (fst gcC'))"
  by(blast dest!: ignores_old_vars_conc_meval_sched[OF modes_respect_priv_ignores_old_vars])

lemma meval_modes_respect_priv:
  "conc.meval_abv gcC n gcC' ⟹   length (fst gcC) = length cms ⟹
  modes_respect_priv (map snd (fst gcC)) ⟹
  modes_respect_priv (map snd (fst gcC'))"
  by(blast dest!: ignores_old_vars_conc_meval[OF modes_respect_priv_ignores_old_vars])
  
(* I think this lemma would guarantee globally sound mode use for all of the
  varC_of variables. It should also hold for all of the non varC_of variables by
  the locale assumptions above *)
lemma traces_refinement:
  "⋀gcC gcC' schedC gcA. conc.meval_sched schedC gcC gcC' ⟹
    length (fst gcA) = length cms ⟹ length (fst gcC) = length cms  ⟹
    (⋀i. i < length cms ⟹ ((fst gcA ! i, snd gcA), (fst gcC ! i, snd gcC)) ∈ ℛ_rel (cms ! i)) ⟹
    abs.sound_mode_use gcA ⟹ modes_respect_priv (map snd (fst gcC)) ⟹
   ∃schedA gcA'. abs.meval_sched schedA gcA gcA' ∧
          (∀i. i < length cms ⟶ ((fst gcA' ! i, snd gcA'), (fst gcC' ! i, snd gcC')) ∈ ℛ_rel (cms ! i)) ∧
          abs.sound_mode_use gcA'"
proof -
  fix gcC gcC' schedC gcA
  assume mevalC: "conc.meval_sched schedC gcC gcC'"
     and len_eq [simp]: "length (fst gcA) = length cms"
     and len_eq'[simp]: "length (fst gcC) = length cms"
     and in_ℛ: "(⋀i. i < length cms ⟹ ((fst gcA ! i, snd gcA), (fst gcC ! i, snd gcC)) ∈ ℛ_rel (cms ! i))"
     and sound_mode_useA: "abs.sound_mode_use gcA"
     and modes_respect_priv: "modes_respect_priv (map snd (fst gcC))"
  thus
    "∃schedA gcA'. abs.meval_sched schedA gcA gcA' ∧
          (∀i. i < length cms ⟶ ((fst gcA' ! i, snd gcA'), (fst gcC' ! i, snd gcC')) ∈ ℛ_rel (cms ! i)) ∧
          abs.sound_mode_use gcA'"
  proof(induct  arbitrary: gcA rule: conc.meval_sched.induct)
  case (1 cmsC cmsC')
    from 1(1) have cmsC'_def [simp]: "cmsC' = cmsC" by simp
    with 1 have "abs.meval_sched [] gcA gcA ∧
    (∀i<length cms.
        ((fst gcA ! i, snd gcA), fst cmsC' ! i, snd cmsC') ∈ ℛ_rel (cms ! i)) ∧
        abs.sound_mode_use gcA"
      by simp
    thus ?case by blast
  next
  case (2 n ns gcC gcc')
    obtain cmsC memC where gcC_def [simp]: "gcC = (cmsC, memC)" by force
    obtain cmsA memA where gcA_def [simp]: "gcA = (cmsA, memA)" by force
    from 2(2) gcC_def obtain cmsC'' memC'' where
      mevalC: "((cmsC,memC), n, (cmsC'',memC'')) ∈ conc.meval" and 
      meval_schedC: "conc.meval_sched ns (cmsC'',memC'') gcc'" 
      by force
  
    let ?cmCn = "cmsC ! n"
    let ?cmAn = "cmsA ! n"
    let ?ℛn = "ℛ_rel (cms ! n)"
    from mevalC obtain cmCn'' where
      evalCn: "(?cmCn, memC) ↝C (cmCn'', memC'')" and
      len: "n < length cmsC" and
      cmsC''_def: "cmsC'' = cmsC [n := cmCn'']" by (blast elim: conc.meval.cases)
    from len have len [simp]: "n < length cms" by (simp add: 2[simplified])
    from cmsC''_def 2 have 
      len_cmsC'' [simp]: "length cmsC'' = length cms" by simp
    from 2 len have 
      in_ℛn: "((?cmAn,memA), (?cmCn,memC)) ∈ ?ℛn"
      by simp
    
    with evalCn use_secure_refinement_helper[OF secure_refinements[OF len]]  
    obtain cmAn'' memA'' mA where
      nevalAn: "abs.neval (?cmAn, memA) mA (cmAn'', memA'')" and
      in_ℛn'': "((cmAn'',memA''),(cmCn'',memC'')) ∈ ?ℛn"
      by blast+
      
    define cmsA'' where "cmsA'' = cmsA [n := cmAn'']" 
    define gcA'' where [simp]: "gcA'' = (cmsA'', memA'')"
    have len_cmsA'' [simp]: "length cmsA'' = length cms" by(simp add: cmsA''_def 2[simplified])
  
    have in_ℛ'': "(⋀i. i < length cms ⟹ ((cmsA'' ! i, memA''), cmsC'' ! i, memC'') ∈ ℛ_rel (cms ! i))"
    proof -
      fix i
      assume "i < length cms"
      show "?thesis i"
      proof(cases "i = n")
        assume "i = n"
        hence "cmsA'' ! i = cmAn''"
          using cmsA''_def len_cmsA'' len by simp
        moreover from ‹i = n› have "cmsC'' ! i = cmCn''"
          using cmsC''_def len_cmsC'' len by simp
        ultimately  show ?thesis 
          using in_ℛn'' ‹i = n›
          by simp
      next
        obtain cAi mdsAi where cmsAi_def [simp]: "(cmsA ! i) = (cAi, mdsAi)" by fastforce 
        obtain cCi mdsCi where cmsCi_def [simp]: "(cmsC ! i) = (cCi, mdsCi)" by fastforce 
        hence mdsCi_def: "mdsCi = snd (cmsC ! i)" by simp
        
        from 2(5) ‹i < length cms› have 
          in_ℛi: "((cmsA ! i,memA), (cmsC ! i,memC)) ∈ ℛ_rel (cms ! i)"
          by force
          
        from in_ℛn'' secure_refinements len preserves_modes_memD
        have memA''_def [simp]: "memA'' = memA_of memC''"
          unfolding secure_refinement_def
          by (metis surjective_pairing)
          
        from in_ℛi secure_refinements  ‹i < length cms› preserves_modes_memD
             cmsAi_def cmsCi_def
        have memA_def [simp]: "memA = memA_of memC" and
             mdsAi_def [simp]: "mdsAi = mdsA_of mdsCi"
          unfolding secure_refinement_def
          by metis+
          
        assume "i ≠ n"
        hence "cmsA'' ! i = cmsA ! i"
          using cmsA''_def len_cmsA'' len by simp
        moreover from ‹i ≠ n› have "cmsC'' ! i = cmsC ! i"
          using cmsC''_def len_cmsC'' len by simp
        ultimately  show ?thesis 
        
          using 2(5)[of i] ‹i ≠ n› ‹i < length cms›
          apply simp
          apply(rule closed_othersD)
            apply(rule secure_refinements[OF ‹i < length cms›, unfolded secure_refinement_def, THEN conjunct1])
           apply assumption
          apply(simp only: mdsCi_def)  
          apply(rule_tac ℛn="ℛ_rel (cms ! n)"  and ℛi="ℛ_rel (cms ! i)" in modified_variables_are_not_assumed_not_written)
                           apply(rule 2(6)[unfolded gcA_def])
                          using secure_refinements len secure_refinement_def apply blast
                         apply(rule in_ℛn)
                        using secure_refinements secure_refinement_def apply blast
                       apply(rule in_ℛi)
                      apply(rule len)
                      using 2 apply simp
                    using 2 apply simp
                   using 2(7) unfolding modes_respect_priv_def priv_is_asm_priv_def gcC_def 
                   using "2.prems"(3) apply auto[1]
                  using 2(7) unfolding modes_respect_priv_def priv_is_guar_priv_def gcC_def 
                  using "2.prems"(3) apply auto[1]
                 using 2(7) unfolding modes_respect_priv_def new_asms_only_for_priv_def gcC_def 
                 using "2.prems"(3) apply auto[1]
                apply(rule evalCn)
               apply(rule nevalAn)
              apply(rule in_ℛn'')
             apply fastforce
            apply assumption
           apply assumption
          apply(rule local_guarantee_preservation)
          by simp
      qed
    qed
  
    have meval_schedA: "abs.meval_sched (replicate mA n) gcA (cmsA'', memA'')"
      apply(simp add: cmsA''_def)
      apply(rule abs.neval_meval[OF _ _ HOL.refl HOL.refl])
       apply(rule nevalAn)
      using "2.prems"(2) by auto
  
    have sound_mode_useA'': "abs.sound_mode_use (cmsA'', memA'')"
      apply(rule abs.meval_sched_sound_mode_use)
       apply(rule 2(6))
      by(rule meval_schedA)
   
    have respects'': "modes_respect_priv (map snd cmsC'')"
      apply(rule meval_modes_respect_priv[where gcC'="(cmsC'',memC'')", simplified])
        apply(rule mevalC)
       using "2.prems"(3) gcC_def apply blast
      using 2 by simp

    from respects'' 2(1)[OF meval_schedC, where gcA7 = gcA''] in_ℛ'' sound_mode_useA''
    obtain schedA gcA' 
    where  meval_schedA'': "abs.meval_sched schedA gcA'' gcA'" and
           in_ℛ': "(∀i<length cms. ((fst gcA' ! i, snd gcA'), fst gcc' ! i, snd gcc') ∈ ℛ_rel (cms ! i))" and
           sound_mode_useA': "abs.sound_mode_use  gcA'" by fastforce
    define final_schedA where "final_schedA = (replicate mA n) @ schedA"
    have meval_final_schedA: "abs.meval_sched final_schedA gcA gcA'"
      using meval_schedA'' meval_schedA abs.meval_sched_app final_schedA_def gcA''_def by blast
    
    from meval_final_schedA in_ℛ' sound_mode_useA'
    show ?case by blast
  qed
qed

end

context sifum_security begin

definition
  restrict_modes :: "'Var Mds list ⇒ 'Var set ⇒ 'Var Mds list"
where
  "restrict_modes mdss X ≡ map (λmds m. mds m ∩ X) mdss"

lemma restrict_modes_length [simp]:
  "length (restrict_modes mdss X) = length mdss"
  by(auto simp: restrict_modes_def)
  
lemma compatible_modes_by_case_distinction:
  assumes compat_X: "compatible_modes (restrict_modes mdss X)"
  assumes compat_compX: "compatible_modes (restrict_modes mdss (-X ))"
  shows "compatible_modes mdss"
unfolding compatible_modes_def
proof(safe)
  fix i x j
  assume ilen: "i < length mdss"
  assume jlen: "j < length mdss"
  assume neq: "j ≠ i"
  assume asm: "x ∈ (mdss ! i) AsmNoReadOrWrite"
  show "x ∈ (mdss ! j) GuarNoReadOrWrite"
  proof(cases "x ∈ X")
    assume xin: "x ∈ X"
    let ?mdssX = "restrict_modes mdss X"
    from asm xin have "x ∈ (?mdssX ! i) AsmNoReadOrWrite"
      unfolding restrict_modes_def
      using ilen by auto
    
    with compat_X jlen ilen neq 
    have "x ∈ (?mdssX ! j) GuarNoReadOrWrite"
      unfolding compatible_modes_def
      by auto
    with xin jlen show ?thesis
      unfolding restrict_modes_def by auto
  next
    assume xnin: "x ∉ X"
    let ?mdssX = "restrict_modes mdss (- X)"
    from asm xnin have "x ∈ (?mdssX ! i) AsmNoReadOrWrite"
      unfolding restrict_modes_def
      using ilen by auto
    
    with compat_compX jlen ilen neq 
    have "x ∈ (?mdssX ! j) GuarNoReadOrWrite"
      unfolding compatible_modes_def
      by auto
    with xnin jlen show ?thesis
      unfolding restrict_modes_def by auto
  qed
next
  fix i x j
  assume ilen: "i < length mdss"
  assume jlen: "j < length mdss"
  assume neq: "j ≠ i"
  assume asm: "x ∈ (mdss ! i) AsmNoWrite"
  show "x ∈ (mdss ! j) GuarNoWrite"
  proof(cases "x ∈ X")
    assume xin: "x ∈ X"
    let ?mdssX = "restrict_modes mdss X"
    from asm xin have "x ∈ (?mdssX ! i) AsmNoWrite"
      unfolding restrict_modes_def
      using ilen by auto
    
    with compat_X jlen ilen neq 
    have "x ∈ (?mdssX ! j) GuarNoWrite"
      unfolding compatible_modes_def
      by auto
    with xin jlen show ?thesis
      unfolding restrict_modes_def by auto
  next
    assume xnin: "x ∉ X"
    let ?mdssX = "restrict_modes mdss (- X)"
    from asm xnin have "x ∈ (?mdssX ! i) AsmNoWrite"
      unfolding restrict_modes_def
      using ilen by auto
    
    with compat_compX jlen ilen neq 
    have "x ∈ (?mdssX ! j) GuarNoWrite"
      unfolding compatible_modes_def
      by auto
    with xnin jlen show ?thesis
      unfolding restrict_modes_def by auto
  qed
qed

lemma in_restrict_modesD:
  "i < length mdss ⟹ x ∈ ((restrict_modes mdss X) ! i) m ⟹ x ∈ X ∧ x ∈ (mdss ! i) m"
  by(auto simp: restrict_modes_def)

lemma in_restrict_modesI:
  "i < length mdss ⟹ x ∈ X ⟹ x ∈ (mdss ! i) m ⟹ x ∈ ((restrict_modes mdss X) ! i) m "
  by(auto simp: restrict_modes_def)
  
lemma meval_sched_length:
  "meval_sched sched gc gc' ⟹ length (fst gc') = length (fst gc)"
  apply(induct sched arbitrary: gc gc')
  by auto
  
  
end

context sifum_refinement_sys begin

lemma compatible_modes_old_vars:
  assumes compatible_modesA: "abs.compatible_modes (map snd cmsA)" 
  assumes lenA: "length cmsA = length cms"
  assumes lenC: "length cmsC = length cms"
  assumes in_ℛ: "(∀i<length cms. ((cmsA ! i, memA), cmsC ! i, memC) ∈ ℛ_rel (cms ! i))"
  shows "conc.compatible_modes (conc.restrict_modes (map snd cmsC) (range varC_of))"
unfolding conc.compatible_modes_def
proof(clarsimp)
  fix i x
  assume i_len: "i < length cmsC"
  let ?cms = "cms ! i" and
      ?cA = "fst (cmsA ! i)" and ?mdsA = "snd (cmsA ! i)" and
      ?cC = "fst (cmsC ! i)" and ?mdsC = "snd (cmsC ! i)"

  from in_ℛ i_len lenC
  have in_ℛ_i: "((cmsA ! i, memA), cmsC ! i, memC) ∈ ℛ_rel ?cms" by simp

  from i_len have "i < length (map snd cmsC)" by simp
  hence m_x_range: "⋀m. x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! i) m ⟹ x ∈ range varC_of ∧ x ∈ (map snd cmsC ! i) m"
    using conc.in_restrict_modesD i_len by blast+
  hence m_xC_i: "⋀m. x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! i) m ⟹ x ∈ ?mdsC m"
    by (simp add: i_len)

  from secure_refinements i_len lenC
  have "secure_refinement (ℛA_rel ?cms) (ℛ_rel ?cms) (P_rel ?cms)" by simp
  hence preserves_modes_mem_ℛ_i: "preserves_modes_mem (ℛ_rel ?cms)"
    unfolding secure_refinement_def by simp

  from in_ℛ_i have "(⟨?cA, ?mdsA, memA⟩A, ⟨?cC, ?mdsC, memC⟩C) ∈ ℛ_rel ?cms" by clarsimp
  with preserves_modes_mem_ℛ_i
  have "(∀xA. memA xA = memC (varC_of xA)) ∧ (∀m. varC_of ` ?mdsA m = range varC_of ∩ ?mdsC m)"
    unfolding preserves_modes_mem_def by blast
  with m_xC_i have m_xA: "⋀m. x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! i) m ⟹ varA_of x ∈ ?mdsA m"
    unfolding varA_of_def using m_x_range inj_image_mem_iff varC_of_inj by fastforce

  show "(x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! i) AsmNoReadOrWrite ⟶
          (∀j<length cmsC. j ≠ i ⟶
            x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! j) GuarNoReadOrWrite)) ∧
        (x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! i) AsmNoWrite ⟶
          (∀j<length cmsC. j ≠ i ⟶
            x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! j) GuarNoWrite))"
    proof(safe)
      fix j
      assume AsmNoRW_xC: "x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! i) AsmNoReadOrWrite" and
        j_len: "j < length cmsC" and
        j_not_i: "j ≠ i"
      let ?cms' = "cms ! j" and
          ?cA' = "fst (cmsA ! j)" and ?mdsA' = "snd (cmsA ! j)" and
          ?cC' = "fst (cmsC ! j)" and ?mdsC' = "snd (cmsC ! j)"

      from AsmNoRW_xC m_x_range
      have x_range: "x ∈ range varC_of" by simp

      from AsmNoRW_xC m_xA
      have "varA_of x ∈ ?mdsA AsmNoReadOrWrite" by simp
      with compatible_modesA
      have GuarNoRW_xA: "varA_of x ∈ ?mdsA' GuarNoReadOrWrite"
        unfolding abs.compatible_modes_def using i_len lenA lenC j_len j_not_i by clarsimp

      from in_ℛ j_len lenC
      have in_ℛ_j: "((cmsA ! j, memA), cmsC ! j, memC) ∈ ℛ_rel ?cms'" by simp

      from j_len have j_len': "j < length (map snd cmsC)" by simp

      from secure_refinements j_len lenC
      have "secure_refinement (ℛA_rel ?cms') (ℛ_rel ?cms') (P_rel ?cms')" by simp
      hence preserves_modes_mem_ℛ_j: "preserves_modes_mem (ℛ_rel ?cms')"
        unfolding secure_refinement_def by simp

      from in_ℛ_j have "(⟨?cA', ?mdsA', memA⟩A, ⟨?cC', ?mdsC', memC⟩C) ∈ ℛ_rel ?cms'" by clarsimp
      with preserves_modes_mem_ℛ_j
      have "(∀xA. memA xA = memC (varC_of xA)) ∧ (∀m. varC_of ` ?mdsA' m = range varC_of ∩ ?mdsC' m)"
        unfolding preserves_modes_mem_def by blast

      with GuarNoRW_xA j_len j_len' mdsA_of_def x_range conc.in_restrict_modesI varC_of_inj
      show "x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! j) GuarNoReadOrWrite"
        unfolding varA_of_def
        by (metis (no_types, lifting) doesnt_have_mode f_inv_into_f image_inv_f_f nth_map)
    next
      (* This argument is identical to that for AsmNoReadOrWrite *)
      fix j
      assume AsmNoWrite_xC: "x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! i) AsmNoWrite" and
        j_len: "j < length cmsC" and
        j_not_i: "j ≠ i"
      let ?cms' = "cms ! j" and
          ?cA' = "fst (cmsA ! j)" and ?mdsA' = "snd (cmsA ! j)" and
          ?cC' = "fst (cmsC ! j)" and ?mdsC' = "snd (cmsC ! j)"

      from AsmNoWrite_xC m_x_range
      have x_range: "x ∈ range varC_of" by simp

      from AsmNoWrite_xC m_xA
      have "varA_of x ∈ ?mdsA AsmNoWrite" by simp
      with compatible_modesA
      have GuarNoWrite_xA: "varA_of x ∈ ?mdsA' GuarNoWrite"
        unfolding abs.compatible_modes_def using i_len lenA lenC j_len j_not_i by clarsimp

      from in_ℛ j_len lenC
      have in_ℛ_j: "((cmsA ! j, memA), cmsC ! j, memC) ∈ ℛ_rel ?cms'" by simp

      from j_len have j_len': "j < length (map snd cmsC)" by simp

      from secure_refinements j_len lenC
      have "secure_refinement (ℛA_rel ?cms') (ℛ_rel ?cms') (P_rel ?cms')" by simp
      hence preserves_modes_mem_ℛ_j: "preserves_modes_mem (ℛ_rel ?cms')"
        unfolding secure_refinement_def by simp

      from in_ℛ_j have "(⟨?cA', ?mdsA', memA⟩A, ⟨?cC', ?mdsC', memC⟩C) ∈ ℛ_rel ?cms'" by clarsimp
      with preserves_modes_mem_ℛ_j
      have "(∀xA. memA xA = memC (varC_of xA)) ∧ (∀m. varC_of ` ?mdsA' m = range varC_of ∩ ?mdsC' m)"
        unfolding preserves_modes_mem_def by blast

      with GuarNoWrite_xA j_len j_len' mdsA_of_def x_range conc.in_restrict_modesI varC_of_inj
      show "x ∈ (conc.restrict_modes (map snd cmsC) (range varC_of) ! j) GuarNoWrite"
        unfolding varA_of_def
        by (metis (no_types, lifting) doesnt_have_mode f_inv_into_f image_inv_f_f nth_map)
    qed
qed

lemma compatible_modes_new_vars:
  "length mdss = length cms ⟹ modes_respect_priv mdss ⟹ conc.compatible_modes (conc.restrict_modes mdss (- range varC_of))"
unfolding conc.compatible_modes_def
proof(safe)
  let ?X = "- range varC_of"
  let ?mdssX = "conc.restrict_modes mdss ?X"
  assume respect: "modes_respect_priv mdss"
  assume len_eq: "length mdss = length cms"
  fix i xC j
  assume ilen: "i < length ?mdssX"
  assume jlen: "j < length ?mdssX"
  assume neq: "j ≠ i"
  assume asmX: "xC ∈ (?mdssX ! i) AsmNoWrite"
  from conc.in_restrict_modesD ilen asmX conc.restrict_modes_length have 
    xin: "xC ∈ ?X" and
    asm: "xC ∈ (mdss ! i) AsmNoWrite" by metis+
  from asm have "False"
    using respect xin ilen conc.restrict_modes_length len_eq
    unfolding modes_respect_priv_def new_asms_NoReadOrWrite_only_def
    by force
  thus "xC ∈ (?mdssX ! j) GuarNoWrite" by blast
next
  let ?X = "- range varC_of"
  let ?mdssX = "conc.restrict_modes mdss ?X"
  assume respect: "modes_respect_priv mdss"
  assume len_eq: "length mdss = length cms"
  fix i xC j
  assume ilen: "i < length ?mdssX"
  assume jlen: "j < length ?mdssX"
  assume neq: "j ≠ i"
  assume asmX: "xC ∈ (?mdssX ! i) AsmNoReadOrWrite"
  from conc.in_restrict_modesD ilen asmX conc.restrict_modes_length have 
    xin: "xC ∈ ?X" and
    asm: "xC ∈ (mdss ! i) AsmNoReadOrWrite" by metis+
  from respect asm xin ilen conc.restrict_modes_length len_eq have
    "xC ∈ priv_memC ! i"
    unfolding modes_respect_priv_def new_asms_only_for_priv_def
    by force
  with respect ilen jlen neq conc.restrict_modes_length len_eq have
    "xC ∈ (mdss ! j) GuarNoReadOrWrite"
    unfolding modes_respect_priv_def priv_is_guar_priv_def
    by force
  with jlen xin conc.in_restrict_modesI show
    "xC ∈ (?mdssX ! j) GuarNoReadOrWrite" by force
qed

    
lemma sound_mode_use_preservation:
  "⋀gcC gcA. 
    length (fst gcA) = length cms ⟹ length (fst gcC) = length cms  ⟹
    (⋀i. i < length cms ⟹ ((fst gcA ! i, snd gcA), (fst gcC ! i, snd gcC)) ∈ ℛ_rel (cms ! i)) ⟹
    abs.sound_mode_use gcA ⟹ modes_respect_priv (map snd (fst gcC)) ⟹
    conc.sound_mode_use gcC"
proof -
  fix gcC gcA
  assume len_eq [simp]: "length (fst gcA) = length cms"
     and len_eq'[simp]: "length (fst gcC) = length cms"
     and in_ℛ: "(⋀i. i < length cms ⟹ ((fst gcA ! i, snd gcA), (fst gcC ! i, snd gcC)) ∈ ℛ_rel (cms ! i))"
     and sound_mode_useA: "abs.sound_mode_use gcA"
     and modes_respect_priv: "modes_respect_priv (map snd (fst gcC))"
  have "conc.globally_sound_mode_use gcC"
  unfolding conc.globally_sound_mode_use_def
  proof(clarsimp)
    fix mdssC'
    assume in_reachable_modes: "mdssC' ∈ conc.reachable_mode_states gcC"
    from this obtain cmsC' memC' schedC where
      meval_schedC: "conc.meval_sched schedC gcC (cmsC', memC')" and
      mdssC'_def: "mdssC' = map snd cmsC'"
      unfolding conc.reachable_mode_states_def by blast
    from traces_refinement[OF meval_schedC, OF len_eq len_eq' in_ℛ sound_mode_useA modes_respect_priv] 
    obtain schedA gcA' cmsA' memA' where gcA'_def [simp]: "gcA' = (cmsA', memA')"  and
      meval_schedA: "abs.meval_sched schedA gcA gcA'" and
      in_ℛ: "(∀i<length cms.
              ((cmsA' ! i, memA'), cmsC' ! i, memC') ∈ ℛ_rel (cms ! i))"
      and sound_mode_useA': "abs.sound_mode_use gcA'"
        by fastforce
    let ?mdssA' = "map snd cmsA'"
    have "?mdssA' ∈ abs.reachable_mode_states gcA"
      unfolding abs.reachable_mode_states_def
      using meval_schedA by fastforce
    hence compatible_modesA': "abs.compatible_modes ?mdssA'"
      using sound_mode_useA unfolding abs.sound_mode_use_def abs.globally_sound_mode_use_def
      by fastforce
    let ?X = "range varC_of"
    show "conc.compatible_modes mdssC'"
    proof(rule conc.compatible_modes_by_case_distinction[where X="?X"])
      show "conc.compatible_modes (conc.restrict_modes mdssC' ?X)"
        apply(simp add: mdssC'_def)
        apply(rule compatible_modes_old_vars[OF _ _ _ in_ℛ])
          apply(rule compatible_modesA')
         using len_eq abs.meval_sched_length[OF meval_schedA] gcA'_def apply simp
        using len_eq' conc.meval_sched_length[OF meval_schedC] by simp
    next
      show "conc.compatible_modes (conc.restrict_modes mdssC' (- ?X))"
        apply(rule compatible_modes_new_vars)
         using len_eq' conc.meval_sched_length[OF meval_schedC] mdssC'_def apply simp
        apply(simp add: mdssC'_def)
        apply(rule meval_sched_modes_respect_priv[OF meval_schedC, simplified])
        using modes_respect_priv by simp
    qed
  qed
  
  moreover have "list_all (λ cm. conc.locally_sound_mode_use (cm, (snd gcC))) (fst gcC)"
  unfolding list_all_length
  proof(clarify)
    fix i
    assume "i < length (fst gcC)"
    hence len: "i < length cms" by simp
    have preserves: "preserves_locally_sound_mode_use (ℛ_rel (cms ! i))"
      apply(rule locally_sound_mode_use_preservation)
       using secure_refinements len apply blast
      using local_guarantee_preservation len by blast
    have "abs.locally_sound_mode_use (fst gcA ! i, snd gcA)"
      using sound_mode_useA ‹i < length cms› len_eq
      unfolding abs.sound_mode_use_def list_all_length
      by (simp add: case_prod_unfold)
    
    from this in_ℛ[OF len] preserves[unfolded preserves_locally_sound_mode_use_def]
    show "conc.locally_sound_mode_use (fst gcC ! i, snd gcC)"
      by blast
  qed
      
  ultimately show "?thesis gcC gcA" unfolding conc.sound_mode_use_def 
  by (simp add: case_prod_unfold)
qed     
      
lemma refined_prog_secure:
  assumes lenA [simp]: "length cmsC = length cms"
  assumes lenC [simp]: "length cmsA = length cms"
  assumes in_ℛ: "(⋀i memC. i < length cms ⟹  ((cmsA ! i,memA_of memC),(cmsC ! i, memC)) ∈ ℛ_rel (cms ! i))"
  assumes in_ℛA: "(⋀i memC memC'. ⟦i < length cms; conc.low_mds_eq (snd (cmsC ! i)) memC memC'⟧
       ⟹ ((cmsA ! i, memA_of memC), (cmsA ! i, memA_of memC')) ∈ ℛA_rel (cms ! i))"
  assumes sound_mode_useA: "(⋀ memA.  abs.sound_mode_use (cmsA, memA))"
  assumes modes_respect_priv: "modes_respect_priv (map snd cmsC)"
  shows "conc.prog_sifum_secure_cont cmsC"
  apply(rule conc.sifum_compositionality_cont)
   apply(clarsimp simp: list_all_length)
   apply(clarsimp simp: conc.com_sifum_secure_def conc.low_indistinguishable_def)
   apply(rule conc.mm_equiv.intros)
    apply(rule RC_of_strong_low_bisim_mm)
      apply(fastforce intro: bisims)
     apply(fastforce intro: secure_refinements)
    apply(fastforce simp: Ps_sym)
   apply(clarsimp simp: RC_of_def)
   apply(rename_tac i cC mdsC memC memC')
   apply(rule_tac x="fst (cmsA ! i)" in exI)
   apply(rule_tac x="snd (cmsA ! i)" in exI)
   apply(rule_tac x="memA_of memC" in exI)
   apply(rule conjI)
    using in_ℛ apply fastforce
   apply(rule_tac x="fst (cmsA ! i)" in exI)
   apply(rule_tac x="snd (cmsA ! i)" in exI)
   apply(rule_tac x="memA_of memC'" in exI)
   apply(rule conjI)
    using in_ℛ apply fastforce
   apply(fastforce simp: in_ℛA Ps_refl_on_low_mds_eq)
  apply(clarify)
  apply(rename_tac memC)
  apply(rule_tac gcA="(cmsA,memA_of memC)" in sound_mode_use_preservation)
      apply simp
     apply simp
    using in_ℛ apply fastforce
   apply(rule sound_mode_useA)
  apply clarsimp
  by(rule modes_respect_priv)

lemma refined_prog_secure':
  assumes lenA [simp]: "length cmsC = length cms"
  assumes lenC [simp]: "length cmsA = length cms"
  assumes in_ℛ: "(⋀i memC. i < length cms ⟹ ((cmsA ! i,memA_of memC),(cmsC ! i, memC)) ∈ ℛ_rel (cms ! i))"
  assumes in_ℛA: "(⋀i memA memA'. ⟦i < length cms;  abs.low_mds_eq (snd (cmsA ! i)) memA memA'⟧
       ⟹ ((cmsA ! i, memA), (cmsA ! i, memA')) ∈ ℛA_rel (cms ! i))"
  assumes sound_mode_useA: "(⋀ memA.  abs.sound_mode_use (cmsA, memA))"
  assumes modes_respect_priv: "modes_respect_priv (map snd cmsC)"
  shows "conc.prog_sifum_secure_cont cmsC"
  apply(rule refined_prog_secure)
       apply(rule lenA)
      apply(rule lenC)
     apply(blast intro: in_ℛ)
    apply(rule in_ℛA)
     apply assumption
    apply(subgoal_tac "snd (cmsA ! i) = mdsA_of (snd (cmsC ! i))")
     using low_mds_eq_from_conc_to_abs apply fastforce
    apply(rule_tac ℛ1="ℛ_rel (cms ! i)" and cA1="fst (cmsA ! i)" and cC1="fst (cmsC ! i)" in preserves_modes_memD[THEN conjunct2])
     using secure_refinements unfolding secure_refinement_def apply fast
    apply clarsimp
    using in_ℛ apply fastforce
   apply(blast intro: sound_mode_useA)
  by(rule modes_respect_priv)
    
end
  
context sifum_security begin

definition
  reachable_mems :: "('Com × (Mode ⇒ 'Var set)) list ⇒ ('Var,'Val) Mem ⇒ ('Var,'Val) Mem set"
where
  "reachable_mems cms mem ≡ {mem'. ∃sched cms'. meval_sched sched (cms,mem) (cms',mem')}"

lemma reachable_mems_refl:
  "mem ∈ reachable_mems cms mem"
  apply(clarsimp simp: reachable_mems_def)
  apply(rule_tac x="[]" in exI)
  apply fastforce
  done
  
end

context sifum_refinement_sys begin

lemma reachable_mems_refinement:
  assumes sys_nonempty: "length cms > 0"
  assumes lenA [simp]: "length cmsC = length cms"
  assumes lenC [simp]: "length cmsA = length cms"
  assumes in_ℛ: "(⋀i memC. i < length cms ⟹ ((cmsA ! i,memA_of memC),(cmsC ! i, memC)) ∈ ℛ_rel (cms ! i))"
  assumes sound_mode_useA: "(⋀ memA. abs.sound_mode_use (cmsA, memA))"
  assumes modes_respect_priv: "modes_respect_priv (map snd cmsC)"
  assumes reachableC: "memC' ∈ conc.reachable_mems cmsC memC"
  shows "memA_of memC' ∈ abs.reachable_mems cmsA (memA_of memC)"
proof -
  from reachableC obtain schedC cmsC' where
    meval_schedC: "conc.meval_sched schedC (cmsC, memC) (cmsC', memC')"
    by (fastforce simp: conc.reachable_mems_def)
  
  let ?memA = "memA_of memC"
  
  have sound_mode_useA: "abs.sound_mode_use (cmsA, ?memA)"  
    by(rule sound_mode_useA)

  from traces_refinement[where gcA="(cmsA,?memA)", OF meval_schedC, OF _ _ _ sound_mode_useA]
       in_ℛ[of _ memC]
       modes_respect_priv
  obtain schedA cmsA' memA' where
    meval_schedA: "abs.meval_sched schedA (cmsA, ?memA) (cmsA', memA')" and
    in_ℛ': "(∀i<length cms.
               ((cmsA' ! i, memA'), cmsC' ! i, memC') ∈ ℛ_rel (cms ! i))"
    by fastforce
  hence reachableA: "memA' ∈ abs.reachable_mems cmsA ?memA"
    by(fastforce simp: abs.reachable_mems_def)
  from sys_nonempty obtain i where ilen: "i < length cms" by blast
  let ?ℛi = "ℛ_rel (cms ! i)"
  from ilen secure_refinements have "preserves_modes_mem ?ℛi"
    unfolding secure_refinement_def by blast
  from ilen in_ℛ' preserves_modes_memD[OF this] have
    memA'_def: "memA' = memA_of memC'"
    by(metis surjective_pairing)
  with reachableA show ?thesis by simp
qed

end

end