Theory Eg1Eg2RefinementSimple

theory Eg1Eg2RefinementSimple
imports Eg1Eg2
begin

context sifum_refinement_eg1_eg2
begin

inductive_set RelS_Eg1Eg2 :: "(
    (((var, aexp, bexp) Stmt × (Mode ⇒ var set)) × (var ⇒ val)) ×
     ((varC, aexpC, bexpC) Stmt × (Mode ⇒ varC set)) × (varC ⇒ val)
    ) set"
where
  acq_mode_rel: "⟦cA = ModeDecl Skip (Acq x SomeMode) ;; cA_tail;
    cC = ModeDecl Skip (Acq (Eg2_varC_of_Eg1 x) SomeMode) ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC AsmNoReadOrWrite);
    ∀mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' ∧
         memA' = memA_of memC' ∧
         memA'' = memA_of memC'' ∧
         (⟨cA, mdsA, memA''⟩A, ⟨Stop ;; cA_tail, mdsA', memA'⟩A) ∈ A.evalw ∧
         (⟨cC, mdsC, memC''⟩C, ⟨Stop ;; cC_tail, mdsC', memC'⟩C) ∈ C.evalw
        )
         ⟶
         (⟨Stop ;; cA_tail, mdsA', memA'⟩A, ⟨Stop ;; cC_tail, mdsC', memC'⟩C) ∈ RelS_Eg1Eg2
    ⟧
    ⟹
    (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" |

  rel_mode_rel: "⟦cA = ModeDecl Skip (Rel x SomeMode);
    cC = ModeDecl Skip (Rel (Eg2_varC_of_Eg1 x) SomeMode);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC AsmNoReadOrWrite);
    ∀mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' ∧
         memA' = memA_of memC' ∧
         memA'' = memA_of memC'' ∧
         (⟨cA, mdsA, memA''⟩A, ⟨Stop, mdsA', memA'⟩A) ∈ A.evalw ∧
         (⟨cC, mdsC, memC''⟩C, ⟨Stop, mdsC', memC'⟩C) ∈ C.evalw
        )
         ⟶
         (⟨Stop, mdsA', memA'⟩A, ⟨Stop, mdsC', memC'⟩C) ∈ RelS_Eg1Eg2
    ⟧
    ⟹
    (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" |

  assign_load_rel: "⟦cA = (x ← aexp.Load y) ;; cA_tail;
    cC = ((Eg2_varC_of_Eg1 x) ← aexpC.Load (Eg2_varC_of_Eg1 y)) ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC AsmNoReadOrWrite);
    ― ‹With this requirement it is possible to establish ‹x ∉ mdsA GuarNoReadOrWrite›.›
    ⌦‹x ≠ y;›
    ― ‹However since we've deemed it reasonable to require ‹x ∉ mdsA GuarNoWrite›,›
    ― ‹it makes little sense not to just require ‹x ∉ mdsA GuarNoReadOrWrite› as well.›
    x ∉ mdsA GuarNoReadOrWrite;
    ― ‹Without this requirement, we would have to prove preservation of ‹doesnt_modify c x››
    ― ‹because ‹x ∈ mdsA GuarNoWrite› holds in the case where ‹memA x = memA y›.›
    ― ‹It makes more sense just to assume a blanket ban on this guarantee for this instruction,›
    ― ‹seeing as it is clearly a write operation to ‹x›.›
    x ∉ mdsA GuarNoWrite;
    ― ‹This command loads from ‹y›, so it makes little sense to guarantee we're not reading it›
    y ∉ mdsA GuarNoReadOrWrite;
    ― ‹Requirements for sound mode use preservation for variables other than ‹x› and ‹y››
    x ∉ 𝒞;
    y ∉ 𝒞;
    ∀mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' ∧
         memA' = memA_of memC' ∧
         memA'' = memA_of memC'' ∧
         (⟨cA, mdsA, memA''⟩A, ⟨Stop ;; cA_tail, mdsA', memA'⟩A) ∈ A.evalw ∧
         (⟨cC, mdsC, memC''⟩C, ⟨Stop ;; cC_tail, mdsC', memC'⟩C) ∈ C.evalw
        )
         ⟶
         (⟨Stop ;; cA_tail, mdsA', memA'⟩A, ⟨Stop ;; cC_tail, mdsC', memC'⟩C) ∈ RelS_Eg1Eg2
    ⟧
    ⟹
    (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" |

  assign_const_rel: "⟦cA = (x ← aexp.Const z) ;; cA_tail;
    cC = ((Eg2_varC_of_Eg1 x) ← aexpC.Const z) ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC AsmNoReadOrWrite);
    x ∉ mdsA GuarNoReadOrWrite;
    x ∉ mdsA GuarNoWrite;
    x ∉ 𝒞;
    ∀mdsA' memA' memA'' mdsC' memC' memC''.
        (
         mdsA' = mdsA_of mdsC' ∧
         memA' = memA_of memC' ∧
         memA'' = memA_of memC'' ∧
         (⟨cA, mdsA, memA''⟩A, ⟨Stop ;; cA_tail, mdsA', memA'⟩A) ∈ A.evalw ∧
         (⟨cC, mdsC, memC''⟩C, ⟨Stop ;; cC_tail, mdsC', memC'⟩C) ∈ C.evalw
        )
         ⟶
         (⟨Stop ;; cA_tail, mdsA', memA'⟩A, ⟨Stop ;; cC_tail, mdsC', memC'⟩C) ∈ RelS_Eg1Eg2
    ⟧
    ⟹
    (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" |

  if_reg_load_rel: "⟦
    cA = (If (Eg1.Eq x 0) cA_then cA_else) ;; cA_tail;
    cC = (regC ← (Load (Eg2_varC_of_Eg1 x))) ;; ((If (Eq regC 0) cC_then cC_else) ;; cC_tail);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC AsmNoReadOrWrite);
    regC ∉ mdsC GuarNoReadOrWrite;
    regC ∉ mdsC GuarNoWrite;
    x ∉ mdsA GuarNoReadOrWrite;
    ― ‹Nope: need to make this one versatile enough to allow ‹c = control_var› for our example›
    ⌦‹x ∉ 𝒞;›
    ∀x'. x ∈ 𝒞_vars x' ⟶ x' ∉ mdsA GuarNoReadOrWrite;
    (∀memA' memC' memA'' memC''.
        (
         memA' = memA_of memC' ∧
         memA'' = memA_of memC'' ∧
         ― ‹The change in ‹memC› does not affect ‹memA››
         memA'' = memA' ∧
         ― ‹The concrete and abstract versions of the bool condition must become consistent›
         evBC memC' (Eq regC 0) = evB memA' (Eg1.Eq x 0) ∧
         (⟨cC, mdsC, memC''⟩C,
          ⟨Stop ;; (If (Eq regC 0) cC_then cC_else) ;; cC_tail, mdsC, memC'⟩C) ∈ C.evalw
        )
         ⟶
         (⟨cA, mdsA, memA''⟩A,
          ⟨Stop ;; (If (Eq regC 0) cC_then cC_else) ;; cC_tail, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2)
    ⟧
    ⟹
    (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" |

  if_reg_stop_rel: "⟦
    cA = (If (Eg1.Eq x 0) cA_then cA_else) ;; cA_tail;
    cC = Stop ;; ((If (Eq regC 0) cC_then cC_else) ;; cC_tail);
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC AsmNoReadOrWrite);
    x ∈ mdsA AsmNoWrite ∧ x ∉ mdsA AsmNoReadOrWrite;
    ― ‹Likely we will need to carry this through to the ‹if_reg_rel› case.›
    evBC memC (Eq regC 0) = evB memA (Eg1.Eq x 0);
    (∀memA' memC' memA'' memC''.
        (
         memA' = memA_of memC' ∧
         memA'' = memA_of memC'' ∧
         ― ‹The change in ‹memC› does not affect ‹memA››
         memA'' = memA' ∧
         ― ‹The concrete and abstract versions of the bool condition must remain consistent›
         evBC memC' (Eq regC 0) = evB memA' (Eg1.Eq x 0) ∧
         evBC memC'' (Eq regC 0) = evB memA'' (Eg1.Eq x 0) ∧
         (⟨cC, mdsC, memC''⟩C,
          ⟨(If (Eq regC 0) cC_then cC_else) ;; cC_tail, mdsC, memC'⟩C) ∈ C.evalw
        )
         ⟶
         (⟨cA, mdsA, memA''⟩A,
          ⟨(If (Eq regC 0) cC_then cC_else) ;; cC_tail, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2)
    ⟧
    ⟹
    (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" |

  if_reg_rel: "⟦
― ‹Is a more generic version possible for an arbitrary ‹bA›?›
    ⌦‹cA = (If bA cA_then cA_else) ;; cA_tail;›
    ⌦‹bA = Eg1.Eq x 0;›  ― ‹‹evB memA bA››
    cA = (If (Eg1.Eq x 0) cA_then cA_else) ;; cA_tail;
    cC = (If (Eq regC 0) cC_then cC_else) ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC AsmNoReadOrWrite);
    x ∈ mdsA AsmNoWrite ∧ x ∉ mdsA AsmNoReadOrWrite;
    ― ‹The concrete and abstract versions of the bool condition must have remained consistent›
    evBC memC (Eq regC 0) = evB memA (Eg1.Eq x 0);
    ― ‹As for ‹if_reg_load_rel››
    regC ∉ mdsC GuarNoReadOrWrite;
    regC ∉ mdsC GuarNoWrite;
    x ∉ mdsA GuarNoReadOrWrite;
    ∀x'. x ∈ 𝒞_vars x' ⟶ x' ∉ mdsA GuarNoReadOrWrite;
    (∀memA' memC' memA'' memC''.
       memA' = memA_of memC' ∧
       memA'' = memA_of memC'' ∧
       evBC memC'' (Eq regC 0) = evB memA'' (Eg1.Eq x 0) ∧
       evBC memC' (Eq regC 0) = evB memA' (Eg1.Eq x 0) ∧
       (⟨cA, mdsA, memA''⟩A,
        ⟨(if (evB memA'' (Eg1.Eq x 0)) then cA_then else cA_else) ;; cA_tail, mdsA, memA'⟩A) ∈ A.evalw ∧
       (⟨cC, mdsC, memC''⟩C,
        ⟨(if (evBC memC'' (Eq regC 0)) then cC_then else cC_else) ;; cC_tail, mdsC, memC'⟩C) ∈ C.evalw
       ⟶
       (⟨(if (evB memA'' (Eg1.Eq x 0)) then cA_then else cA_else) ;; cA_tail, mdsA, memA'⟩A,
        ⟨(if (evBC memC'' (Eq regC 0)) then cC_then else cC_else) ;; cC_tail, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2);
    ― ‹Disallow branching on variables that can potentially be in the high domain›
    x ≠ buffer ∧ x ≠ high_var
    ⟧
    ⟹
    (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" |

  stop_seq_rel: "⟦cA = Stop ;; cA_tail;
    cC = Stop ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (⟨cA_tail, mdsA, memA⟩A, ⟨cC_tail, mdsC, memC⟩C) ∈ RelS_Eg1Eg2⟧
    ⟹
    (⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" |

  stop_rel:
    "(⟨Stop, mdsA_of mdsC, memA_of memC⟩A, ⟨Stop, mdsC, memC⟩C) ∈ RelS_Eg1Eg2"


definition abs_steps' :: "(_,_,_) Stmt ⇒ (_,_,_) Stmt ⇒ nat" where
  "abs_steps' cA cC ≡
    (if (∃x m cA_tail. cA = ((Skip@[x +=m m]) ;; cA_tail)) ∧
        (∃x m cC_tail. cC = ((Skip@[Eg2_varC_of_Eg1 x +=m m]) ;; cC_tail)) then (Suc 0)
     else if (∃ cA_tail cC_tail. cA = (Stop ;; cA_tail) ∧ cC = (Stop ;; cC_tail)) then (Suc 0)
     else if (∃ x thenA elseA tailA thenC elseC tailC.
        cA = (Stmt.If (bexp.Eq x 0) thenA elseA ;; tailA) ∧
        (cC = ((regC ← aexpC.Load (Eg2_varC_of_Eg1 x)) ;; Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC)) ∨
         cC = (Stop ;; Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC))
        then 0
     else (Suc 0))"

fun abs_steps
where
"abs_steps ⟨cA, _, _⟩A ⟨cC, _, _⟩C = abs_steps' cA cC"

lemma closed_others_RelS_Eg1Eg2:
  "closed_others RelS_Eg1Eg2"
unfolding closed_others_def
proof(clarify)
fix cA cC mdsC memC memC'
assume
  in_rel: "(⟨cA, mdsA_of mdsC, memA_of memC⟩A,
    ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" and
  vars: " ∀x. memC x ≠ memC' x ⟶ ¬ var_asm_not_written mdsC x"
and  dmas: "∀x. dmaC memC x ≠ dmaC memC' x ⟶ ¬ var_asm_not_written mdsC x"
from in_rel vars dmas
show "(⟨cA, mdsA_of mdsC, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
  proof (induct rule: RelS_Eg1Eg2.induct)
  case (acq_mode_rel cA x SomeMode tailA cC tailC mdsA mdsC memA memC)
  show "(⟨cA, mdsA, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
    using acq_mode_rel
    by (simp add:RelS_Eg1Eg2.acq_mode_rel)
  next
  case (rel_mode_rel cA x SomeMode cC mdsA mdsC memA memC)
  show "(⟨cA, mdsA, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
    using rel_mode_rel
    by (simp add:RelS_Eg1Eg2.rel_mode_rel)
  next
  case (assign_load_rel cA x y tailA cC tailC mdsA mdsC memA memC)
  show "(⟨cA, mdsA, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
    using assign_load_rel
    by (simp add:RelS_Eg1Eg2.assign_load_rel)
  next
  case (assign_const_rel cA x z tailA cC tailC mdsA mdsC memA memC)
  show "(⟨cA, mdsA, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
    using assign_const_rel
    by (simp add:RelS_Eg1Eg2.assign_const_rel)
  next
  case (if_reg_load_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
  show "(⟨cA, mdsA, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
    using if_reg_load_rel
    by (simp add:RelS_Eg1Eg2.if_reg_load_rel)
  next
  case (if_reg_stop_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
  show "(⟨cA, mdsA, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
    using if_reg_stop_rel
    proof (clarsimp)
      from if_reg_stop_rel.hyps(3,5,6) if_reg_stop_rel.prems(1)
      have regC_untouched: "memC regC = memC' regC" and
        xC_untouched: "memC (Eg2_varC_of_Eg1 x) = memC' (Eg2_varC_of_Eg1 x)" and
        xA_untouched: "memA_of memC x = memA_of memC' x"
        using regC_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC
        by (clarsimp simp:var_asm_not_written_def, blast)+
      with if_reg_stop_rel.hyps
      have conds_still_match: "(memC' regC = 0) = (memA_of memC' x = 0)"
        by simp
      with if_reg_stop_rel RelS_Eg1Eg2.if_reg_stop_rel
      show "(⟨Stmt.If (bexp.Eq x 0) thenA elseA ;; tailA, mdsA_of mdsC, memA_of memC'⟩A,
             ⟨Stop ;; Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC, mdsC, memC'⟩C)
             ∈ RelS_Eg1Eg2"
        by clarsimp
    qed
  next
  case (if_reg_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
  show "(⟨cA, mdsA, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
    using if_reg_rel
    proof (clarsimp)
      from if_reg_rel.hyps(3,5,6) if_reg_rel.prems(1)
      have regC_untouched: "memC regC = memC' regC" and
        xC_untouched: "memC (Eg2_varC_of_Eg1 x) = memC' (Eg2_varC_of_Eg1 x)" and
        xA_untouched: "memA_of memC x = memA_of memC' x"
        using regC_is_not_the_varC_of_anything memA_of_def NoWriteA_implies_NoWriteC
        by (clarsimp simp:var_asm_not_written_def, blast)+
      with if_reg_rel.hyps
      have conds_still_match: "(memC' regC = 0) = (memA_of memC' x = 0)"
        by simp
      show "(⟨Stmt.If (bexp.Eq x 0) thenA elseA ;; tailA, mdsA_of mdsC, memA_of memC'⟩A,
             ⟨Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC, mdsC, memC'⟩C)
             ∈ RelS_Eg1Eg2"
        apply (rule RelS_Eg1Eg2.if_reg_rel, simp+)
            using if_reg_rel apply simp
           using if_reg_rel apply simp
          using conds_still_match apply simp
         using if_reg_rel apply blast+
        done
    qed
  next
  case (stop_seq_rel cA tailA cC tailC mdsA mdsC memA memC)
  show "(⟨cA, mdsA, memA_of memC'⟩A, ⟨cC, mdsC, memC'⟩C) ∈ RelS_Eg1Eg2"
    using stop_seq_rel
    by (simp add:RelS_Eg1Eg2.stop_seq_rel)
  next
  case (stop_rel mdsC memC)
  show ?case by (simp add:RelS_Eg1Eg2.stop_rel)
  qed
qed

lemma preserves_modes_mem_RelS_Eg1Eg2:
  "preserves_modes_mem RelS_Eg1Eg2"
unfolding preserves_modes_mem_def2
proof(clarsimp)
  fix cA mdsA memA cC mdsC memC
  assume in_rel: "(⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2"
  thus "memA = memA_of memC ∧ mdsA = mdsA_of mdsC"
    by (cases rule:RelS_Eg1Eg2.cases, blast+)
qed

(* Just some exploration to see what's likely to be needed *)

lemma mem_twist_other: "z ≠ x ⟹ z ≠ y ⟹ mem (x := mem y, z := v) = mem (z := v, x := (mem (z := v)) y)"
  by (simp add: fun_upd_other fun_upd_twist)

lemma regC_load_helper:
  "xC ≠ Eg2_varC_of_Eg1 x ⟹
   (⟨regC ← aexpC.Load (Eg2_varC_of_Eg1 x), mds, mem(xC := v)⟩C, ⟨Stop, mds, mem
            (xC := v, regC := mem (Eg2_varC_of_Eg1 x))⟩C) =
   (⟨regC ← aexpC.Load (Eg2_varC_of_Eg1 x), mds, mem(xC := v)⟩C, ⟨Stop, mds, mem
            (xC := v, regC := (mem(xC := v)) (Eg2_varC_of_Eg1 x))⟩C)"
  using fun_upd_other by simp

lemma preserves_local_guarantee_compliance_RelS_Eg1Eg2:
  "preserves_local_guarantee_compliance RelS_Eg1Eg2"
proof(clarsimp simp:preserves_local_guarantee_compliance_def2)
  fix cA mdsA memA cC mdsC memC
  assume in_RelS: "(⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" and
    respectsA: "A.respects_own_guarantees (cA, mdsA)"
  thus "conc.respects_own_guarantees (cC, mdsC)"
  unfolding conc.respects_own_guarantees_def conc.doesnt_read_or_modify_def conc.doesnt_read_or_modify_vars_def conc.doesnt_modify_def
  proof(induct rule:RelS_Eg1Eg2.induct)
    case (acq_mode_rel cA x m tailA cC tailC mdsA mdsC memA memC)
      from acq_mode_rel.hyps(2-3)
      show ?case using C.decl_evalw' C.evalw.seq C.seq_decl_elim by fastforce+
    next
    case (rel_mode_rel cA x m cC mdsA mdsC memA memC)
      from rel_mode_rel.hyps(2-3)
      show ?case using C.decl_evalw' C.evalw.seq C.seq_decl_elim by fastforce+
    next
    case (assign_load_rel cA x y tailA cC tailC mdsA mdsC memA memC)
      hence in_RelS: "(⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2"
        by (simp add:RelS_Eg1Eg2.intros(3))

      from assign_load_rel.prems show ?case
      proof (clarify)
        assume respectsA: "A.respects_own_guarantees (cA, mdsA)"
        fix xC
        let ?case_xC = "(xC ∈ snd (cC, mdsC) GuarNoReadOrWrite ⟶
               (∀mds mem c' mds' mem'.
                   (⟨fst (cC, mdsC), mds, mem⟩C, ⟨c', mds', mem'⟩C)
                   ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
                   (∀x∈{xC} ∪ 𝒞_varsC xC.
                       ∀v. (⟨fst (cC, mdsC), mds, mem(x := v)⟩C, ⟨c', mds', mem'(x := v)⟩C)
                           ∈ sifum_lang_no_dma.evalw evAC evBC))) ∧
              (xC ∈ snd (cC, mdsC) GuarNoWrite ⟶
               (∀mds mem c' mds' mem'.
                   (⟨fst (cC, mdsC), mds, mem⟩C, ⟨c', mds', mem'⟩C)
                   ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
                   mem xC = mem' xC ∧ dmaC mem xC = dmaC mem' xC))"

        (* For xC = x, we have to argue that the abstract version of xC must have the same
           guarantees as for xC, which yields contradictions in both cases. *)
        from assign_load_rel(3,6,7) preserves_modes_mem_RelS_Eg1Eg2 has_modeA
        have notGuarNoRW_xC: "xC = Eg2_varC_of_Eg1 x ⟹ xC ∉ mdsC GuarNoReadOrWrite" and
             notGuarNoWrite_xC: "xC = Eg2_varC_of_Eg1 x ⟹ xC ∉ mdsC GuarNoWrite" by clarsimp+

        (* For xC = y, waive doesnt_read_or_modify using ¬ GuarNoRW y from refinement relation,
           and the proof for doesnt_modify is straightforward *)
        from assign_load_rel(3,8) preserves_modes_mem_RelS_Eg1Eg2 has_modeA
        have "xC = Eg2_varC_of_Eg1 y ⟹ xC ∉ mdsC GuarNoReadOrWrite" by clarsimp
        with assign_load_rel(2)
        have "⟦xC = Eg2_varC_of_Eg1 y; Eg2_varC_of_Eg1 x ∉ 𝒞_varsC xC⟧ ⟹ ?case_xC"
          apply clarsimp
          apply(drule C.seq_assign_elim, clarsimp)
          using 𝒞_varsC_def dmaC_def by auto

        (* For all other xC, the proof should be straightforward because cC does not touch xC,
           and we've required that x and y cannot potentially be the control var of xC *)
        moreover have "⟦xC ≠ Eg2_varC_of_Eg1 x; xC ≠ Eg2_varC_of_Eg1 y;
               Eg2_varC_of_Eg1 x ∉ 𝒞_varsC xC; Eg2_varC_of_Eg1 y ∉ 𝒞_varsC xC⟧
              ⟹ ?case_xC"
          using assign_load_rel(2,6) apply safe
             apply(clarsimp, drule C.seq_assign_elim)
             apply(simp add: mem_twist_other C.evalw.seq assign_evalw_loadC del:fun_upd_apply)
            apply(clarsimp, drule C.seq_assign_elim, clarsimp)
            apply(subgoal_tac "xa ≠ Eg2_varC_of_Eg1 x ∧ xa ≠ Eg2_varC_of_Eg1 y")
             apply(simp add: mem_twist_other C.evalw.seq assign_evalw_loadC del:fun_upd_apply)
            apply blast
           apply(clarsimp, drule C.seq_assign_elim, clarsimp)
          apply(clarsimp, drule C.seq_assign_elim)
          using 𝒞_varsC_def dmaC_def by auto

        moreover have "Eg2_varC_of_Eg1 x ∉ 𝒞_varsC xC" and "Eg2_varC_of_Eg1 y ∉ 𝒞_varsC xC"
          using assign_load_rel(9-10) unfolding 𝒞_varsC_def
          by (metis Eg2_varC_of_Eg1.simps(1) A.𝒞_simp empty_iff insert_iff inv_f_eq varC_of_inj)+
        moreover note notGuarNoRW_xC notGuarNoWrite_xC
        moreover have "xC ∉ mdsC GuarNoReadOrWrite ⟹ xC ∉ mdsC GuarNoWrite ⟹ ?case_xC" by auto
        ultimately show ?case_xC by fastforce
      qed
    next
    case (assign_const_rel cA x z tailA cC tailC mdsA mdsC memA memC)
      from assign_const_rel.prems show ?case
      proof (clarify)
        assume respectsA: "A.respects_own_guarantees (cA, mdsA)"
        fix xC
        let ?case_xC = "(xC ∈ snd (cC, mdsC) GuarNoReadOrWrite ⟶
               (∀mds mem c' mds' mem'.
                   (⟨fst (cC, mdsC), mds, mem⟩C, ⟨c', mds', mem'⟩C)
                   ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
                   (∀x∈{xC} ∪ 𝒞_varsC xC.
                       ∀v. (⟨fst (cC, mdsC), mds, mem(x := v)⟩C, ⟨c', mds', mem'(x := v)⟩C)
                           ∈ sifum_lang_no_dma.evalw evAC evBC))) ∧
              (xC ∈ snd (cC, mdsC) GuarNoWrite ⟶
               (∀mds mem c' mds' mem'.
                   (⟨fst (cC, mdsC), mds, mem⟩C, ⟨c', mds', mem'⟩C)
                   ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
                   mem xC = mem' xC ∧ dmaC mem xC = dmaC mem' xC))"
        from assign_const_rel(3,6,7) preserves_modes_mem_RelS_Eg1Eg2 has_modeA
        have notGuarNoRW_xC: "xC = Eg2_varC_of_Eg1 x ⟹ xC ∉ mdsC GuarNoReadOrWrite" and
             notGuarNoWrite_xC: "xC = Eg2_varC_of_Eg1 x ⟹ xC ∉ mdsC GuarNoWrite" by clarsimp+

        moreover have "⟦xC ≠ Eg2_varC_of_Eg1 x; Eg2_varC_of_Eg1 x ∉ 𝒞_varsC xC⟧ ⟹ ?case_xC"
          using assign_const_rel(2,8) apply safe
             apply(clarsimp, drule C.seq_assign_elim)
             apply(simp add: fun_upd_twist C.evalw.seq assign_evalw_constC)
            apply(clarsimp, drule C.seq_assign_elim, clarsimp)
            apply(subgoal_tac "xa ≠ Eg2_varC_of_Eg1 x")
             apply(simp add: fun_upd_twist C.evalw.seq assign_evalw_constC)
            apply blast
           apply(clarsimp, drule C.seq_assign_elim, clarsimp)
          apply(clarsimp, drule C.seq_assign_elim)
          using 𝒞_varsC_def dmaC_def by auto

        moreover have "Eg2_varC_of_Eg1 x ∉ 𝒞_varsC xC"
          using assign_const_rel(8) unfolding 𝒞_varsC_def
          by (metis Eg2_varC_of_Eg1.simps(1) A.𝒞_simp empty_iff insert_iff inv_f_eq varC_of_inj)
        moreover note notGuarNoRW_xC notGuarNoWrite_xC
        moreover have "xC ∉ mdsC GuarNoReadOrWrite ⟹ xC ∉ mdsC GuarNoWrite ⟹ ?case_xC" by auto
        ultimately show ?case_xC by fastforce
      qed
    next
    case (if_reg_load_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
      from if_reg_load_rel.prems show ?case
      proof (clarify)
        assume respectsA: "A.respects_own_guarantees (cA, mdsA)"
        fix xC
        let ?case_xC = "(xC ∈ snd (cC, mdsC) GuarNoReadOrWrite ⟶
               (∀mds mem c' mds' mem'.
                   (⟨fst (cC, mdsC), mds, mem⟩C, ⟨c', mds', mem'⟩C)
                   ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
                   (∀x∈{xC} ∪ 𝒞_varsC xC.
                       ∀v. (⟨fst (cC, mdsC), mds, mem(x := v)⟩C, ⟨c', mds', mem'(x := v)⟩C)
                           ∈ sifum_lang_no_dma.evalw evAC evBC))) ∧
              (xC ∈ snd (cC, mdsC) GuarNoWrite ⟶
               (∀mds mem c' mds' mem'.
                   (⟨fst (cC, mdsC), mds, mem⟩C, ⟨c', mds', mem'⟩C)
                   ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
                   mem xC = mem' xC ∧ dmaC mem xC = dmaC mem' xC))"
        (* For xC = x, waive doesnt_read_or_modify using ¬ GuarNoRW x from refinement relation
           (makes sense because it's being read), then doesnt_modify is straightforward *)
        from if_reg_load_rel(3,8) preserves_modes_mem_RelS_Eg1Eg2 has_modeA
        have "xC = Eg2_varC_of_Eg1 x ⟹ xC ∉ mdsC GuarNoReadOrWrite" by clarsimp
        with if_reg_load_rel(2)
        have "xC = Eg2_varC_of_Eg1 x ⟹ ?case_xC"
          apply clarsimp
          apply(drule C.seq_assign_elim, clarsimp)
          using 𝒞_varsC_def dmaC_def by auto

        moreover from if_reg_load_rel(2)
        have "⟦xC ≠ regC; xC ≠ Eg2_varC_of_Eg1 x; regC ∉ 𝒞_varsC xC;
               Eg2_varC_of_Eg1 x ∈ 𝒞_varsC xC ⟹ xC ∉ mdsC GuarNoReadOrWrite⟧ ⟹ ?case_xC"
          apply safe
             apply(clarsimp, drule C.seq_assign_elim)
             apply(simp add:fun_upd_twist del:fun_upd_apply)
             apply(rule C.evalw.seq, clarsimp)
             apply(simp add:regC_load_helper del:fun_upd_apply)
             apply(rule assign_evalw_loadC)
            apply(clarsimp, drule C.seq_assign_elim)
            apply(simp add:fun_upd_twist del:fun_upd_apply)
            apply(rule C.evalw.seq, clarsimp)
            apply(subgoal_tac "xa ≠ Eg2_varC_of_Eg1 x ∧ xa ≠ regC")
             apply clarsimp
             apply(simp add:fun_upd_twist regC_load_helper assign_evalw_loadC del:fun_upd_apply)
            apply blast
           apply(clarsimp, drule C.seq_assign_elim, clarsimp)
          apply(clarsimp, drule C.seq_assign_elim)
          using 𝒞_varsC_def dmaC_def by auto
        moreover from if_reg_load_rel(3,9)
        have "Eg2_varC_of_Eg1 x ∈ 𝒞_varsC xC ⟹ xC ∉ mdsC GuarNoReadOrWrite"
          by (metis Eg2_varC_of_Eg1.simps(1-2) 𝒞_varsC_def 𝒞_vars_def empty_iff has_modeA insert_iff inv_f_f varC_of_inj)

        (* We waive cases where xC = regC by requiring ¬ GuarNoRW regC and ¬ GuarNoWrite regC
           which makes sense if we consider concrete-only variables like regC to be private.
           Furthermore we establish that regC cannot be a control var.  *)
        moreover have "xC = regC ⟹ ?case_xC"
          using if_reg_load_rel(6-7) by clarsimp
        moreover have "regC ∉ 𝒞_varsC xC"
          using regC_is_not_the_varC_of_anything 𝒞_varsC_def by clarsimp
        ultimately show ?case_xC by fastforce
      qed
    next
    case (if_reg_stop_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
      from if_reg_stop_rel(2) show ?case
        by (metis C.seq_stop_elim C.seq_stop_evalw fst_conv)
    next
    case (if_reg_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
      from if_reg_rel.prems show ?case
      proof (clarify)
        assume respectsA: "A.respects_own_guarantees (cA, mdsA)"
        fix xC
        let ?case_xC = "(xC ∈ snd (cC, mdsC) GuarNoReadOrWrite ⟶
               (∀mds mem c' mds' mem'.
                   (⟨fst (cC, mdsC), mds, mem⟩C, ⟨c', mds', mem'⟩C)
                   ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
                   (∀x∈{xC} ∪ 𝒞_varsC xC.
                       ∀v. (⟨fst (cC, mdsC), mds, mem(x := v)⟩C, ⟨c', mds', mem'(x := v)⟩C)
                           ∈ sifum_lang_no_dma.evalw evAC evBC))) ∧
              (xC ∈ snd (cC, mdsC) GuarNoWrite ⟶
               (∀mds mem c' mds' mem'.
                   (⟨fst (cC, mdsC), mds, mem⟩C, ⟨c', mds', mem'⟩C)
                   ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
                   mem xC = mem' xC ∧ dmaC mem xC = dmaC mem' xC))"
        from if_reg_rel(3,10) preserves_modes_mem_RelS_Eg1Eg2 has_modeA
        have "xC = Eg2_varC_of_Eg1 x ⟹ xC ∉ mdsC GuarNoReadOrWrite" by clarsimp
        with if_reg_rel(2)
        have "xC = Eg2_varC_of_Eg1 x ⟹ ?case_xC"
          apply clarsimp
          apply(drule C.seq_elim, clarsimp)
          using 𝒞_varsC_def dmaC_def by auto
        moreover from if_reg_rel(2)
        have "⟦xC ≠ regC; xC ≠ Eg2_varC_of_Eg1 x; regC ∉ 𝒞_varsC xC;
            Eg2_varC_of_Eg1 x ∈ 𝒞_varsC xC ⟹ xC ∉ mdsC GuarNoReadOrWrite⟧ ⟹ ?case_xC"
          apply safe
             apply(subgoal_tac "(mem(xC := v)) regC = mem regC")
              apply clarsimp
              apply(drule C.seq_elim, clarsimp+)
              apply(erule C.if_elim, clarsimp)
               apply(simp add: if_true_evalwC if_false_evalwC)+
            apply(subgoal_tac "xa ≠ Eg2_varC_of_Eg1 x ∧ xa ≠ regC")
             apply(drule C.seq_elim, clarsimp+)
             apply(erule C.if_elim, clarsimp)
              apply(simp add: if_true_evalwC if_false_evalwC)+
            apply blast
           apply clarsimp
           apply(drule C.seq_elim, clarsimp+)
           apply(erule C.if_elim, clarsimp+)
          apply(drule C.seq_elim, clarsimp+)
          apply(erule C.if_elim, clarsimp+)
          done
        moreover from if_reg_rel(3,11)
        have "Eg2_varC_of_Eg1 x ∈ 𝒞_varsC xC ⟹ xC ∉ mdsC GuarNoReadOrWrite"
          by (metis Eg2_varC_of_Eg1.simps(1-2) 𝒞_varsC_def 𝒞_vars_def empty_iff has_modeA insert_iff inv_f_f varC_of_inj)
        moreover have "xC = regC ⟹ ?case_xC"
          using if_reg_rel(8-9) by clarsimp
        moreover have "regC ∉ 𝒞_varsC xC"
          using regC_is_not_the_varC_of_anything 𝒞_varsC_def by clarsimp
        ultimately show ?case_xC by fastforce
      qed
    next
    case (stop_seq_rel cA tailA cC tailC mdsA mdsC memA memC)
      from stop_seq_rel(2)
      show ?case by (metis C.seq_stop_elim C.seq_stop_evalw fst_conv)
    next
    case stop_rel
      thus ?case by (simp add: C.stop_no_eval)
  qed
qed

definition mdssA_of :: "((varC Mds) list) ⇒ ((var Mds) list)"
where
  "mdssA_of mdssC = map mdsA_of mdssC"

lemma new_vars_private_RelS_Eg1Eg2:
  "sifum_refinement.new_vars_private dmaC C.evalw Eg2_varC_of_Eg1 RelS_Eg1Eg2"
unfolding new_vars_private_def
(* Slightly more intuitive goals without simp converting ∨ to ⟶ *)
proof(clarify)
  fix cA mdsA memA cC mdsC memC cC' mdsC' memC'
  assume in_rel: "(⟨cA, mdsA, memA⟩A, ⟨cC, mdsC, memC⟩C) ∈ RelS_Eg1Eg2" and
      does_eval: "(⟨cC, mdsC, memC⟩C, ⟨cC', mdsC', memC'⟩C) ∈ C.evalw"
  let "?diff_mem vC" = "memC' vC ≠ memC vC"
  let "?diff_dma vC" = "dmaC memC' vC < dmaC memC vC"
  let "?conc_only vC" = "vC ∉ range Eg2_varC_of_Eg1"
  show "(∀vC. (?diff_mem vC ∨ ?diff_dma vC) ∧ ?conc_only vC ⟶ vC ∈ mdsC' AsmNoReadOrWrite) ∧
         mdsC AsmNoReadOrWrite - range Eg2_varC_of_Eg1
         ⊆ mdsC' AsmNoReadOrWrite - range Eg2_varC_of_Eg1" (* not sure what to call this one *)
  using in_rel does_eval
  proof(cases rule:RelS_Eg1Eg2.cases)
  case (acq_mode_rel x SomeMode tailA tailC)
    moreover with does_eval
    have "mdsC' = mdsC (SomeMode := insert (Eg2_varC_of_Eg1 x) (mdsC SomeMode))"
      by (metis (mono_tags) C.seq_decl_elim C.update_modes.simps(1))
    ultimately show ?thesis
      by simp
  next
  case (rel_mode_rel x SomeMode)
    moreover with does_eval
    have "mdsC' = mdsC (SomeMode := {y. y ∈ (mdsC SomeMode) ∧ y ≠ (Eg2_varC_of_Eg1 x)})"
      by (metis (mono_tags) C.upd_elim C.skip_elim C.update_modes.simps(2))
    ultimately show ?thesis
      by auto
  next
  case (assign_load_rel x y tailA tailC)
    with does_eval
    show ?thesis
      by (metis C.assign_elim C.seq_elim Stmt.distinct(14) set_eq_subset)
  next
  case (assign_const_rel x z tailA tailC)
    with does_eval
    show ?thesis
      by (metis C.assign_elim C.seq_elim Stmt.distinct(14) set_eq_subset)
  next
  case (if_reg_load_rel x thenA elseA tailA thenC elseC tailC)
    with does_eval
    show ?thesis
      by (metis C.assign_elim C.seq_elim Stmt.distinct(14) set_eq_subset)
  next
  case (if_reg_stop_rel x thenA elseA tailA thenC elseC tailC)
    with does_eval
    show ?thesis
      by (metis C.seq_stop_elim subset_refl)
  next
  case (if_reg_rel x thenA elseA tailA thenC elseC tailC)
    with does_eval
    have mdsC_unchanged: "mdsC = mdsC'"
      by (metis C.if_elim C.seq_elim Stmt.distinct(50))
    moreover with if_reg_rel(5)
    have "∀vC. (?diff_mem vC ∨ ?diff_dma vC) ∧ ?conc_only vC ⟶ vC ∈ mdsC' AsmNoReadOrWrite"
      by simp
    moreover from mdsC_unchanged
    have "mdsC AsmNoReadOrWrite - range Eg2_varC_of_Eg1 ⊆ mdsC' AsmNoReadOrWrite - range Eg2_varC_of_Eg1"
      by clarify
    ultimately show ?thesis
      by simp
  next
  case (stop_seq_rel tailA tailC)
    with does_eval C.seq_stop_elim
    show ?thesis
      by blast
  next
  case (stop_rel)
    with does_eval C.stop_no_eval have False by simp
    thus ?thesis by simp
  qed
qed

lemma simple_refinement_safe_RelS_Eg1Eg2:
assumes R_low_mds_eq:
  "⋀c mds mem mem'. (⟨c, mds, mem⟩A, ⟨c, mds, mem'⟩A) ∈ Some_R ⟹ A.low_mds_eq mds mem mem'"
shows
  "sifum_refinement.simple_refinement_safe C.evalw Some_R RelS_Eg1Eg2 abs_steps"
unfolding simple_refinement_safe_def
proof(clarsimp)
  fix cA mdsA mem1A mem2A cC mdsC mem1C mem2C
  assume in_R: "(⟨cA, mdsA, mem1A⟩A, ⟨cA, mdsA, mem2A⟩A) ∈ Some_R" and
       in_RelS_1: "(⟨cA, mdsA, mem1A⟩A, ⟨cC, mdsC, mem1C⟩C) ∈ RelS_Eg1Eg2" and
       in_RelS_2: "(⟨cA, mdsA, mem2A⟩A, ⟨cC, mdsC, mem2C⟩C) ∈ RelS_Eg1Eg2"
  show "stopsC ⟨cC, mdsC, mem1C⟩C = stopsC ⟨cC, mdsC, mem2C⟩C ∧
       (∀mds1C' mds2C' mem1C' mem2C' c1C' c2C'.
           (⟨cC, mdsC, mem1C⟩C, ⟨c1C', mds1C', mem1C'⟩C) ∈ C.evalw ∧
           (⟨cC, mdsC, mem2C⟩C, ⟨c2C', mds2C', mem2C'⟩C) ∈ C.evalw  ⟶
           c1C' = c2C' ∧ mds1C' = mds2C')"
  using in_RelS_1 in_RelS_2
  proof(cases rule:RelS_Eg1Eg2.cases)
  case (acq_mode_rel x m tailA tailC)
    let ?mdsC' = "mdsC(m := insert (Eg2_varC_of_Eg1 x) (mdsC m))"
    from acq_mode_rel have
    eval_1: "(⟨cC, mdsC, mem1C⟩C, ⟨Stop ;; tailC, ?mdsC', mem1C⟩C) ∈ C.evalw" and
    eval_2: "(⟨cC, mdsC, mem2C⟩C, ⟨Stop ;; tailC, ?mdsC', mem2C⟩C) ∈ C.evalw"
      by (simp add: C.decl_evalw' C.evalw.seq)+
    thus ?thesis unfolding stopsC_def using C.eval_det by blast
  next
  case (rel_mode_rel x m)
    let ?mdsC' = "mdsC(m := {y. y ∈ (mdsC m) ∧ y ≠ (Eg2_varC_of_Eg1 x)})"
    from rel_mode_rel have
    eval_1: "(⟨cC, mdsC, mem1C⟩C, ⟨Stop, ?mdsC', mem1C⟩C) ∈ C.evalw" and
    eval_2: "(⟨cC, mdsC, mem2C⟩C, ⟨Stop, ?mdsC', mem2C⟩C) ∈ C.evalw"
      by (simp add: C.decl_evalw')+
    thus ?thesis unfolding stopsC_def using C.eval_det by blast
  next
  case (assign_load_rel x y tailA tailC)
    from assign_load_rel have
    eval_1: "(⟨cC, mdsC, mem1C⟩C, ⟨Stop ;; tailC, mdsC,
               mem1C((Eg2_varC_of_Eg1 x) := mem1C (Eg2_varC_of_Eg1 y))⟩C) ∈ C.evalw" and
    eval_2: "(⟨cC, mdsC, mem2C⟩C, ⟨Stop ;; tailC, mdsC,
               mem2C((Eg2_varC_of_Eg1 x) := mem2C (Eg2_varC_of_Eg1 y))⟩C) ∈ C.evalw"
      by (simp add: assign_evalw_loadC C.evalw.seq)+
    thus ?thesis unfolding stopsC_def using C.eval_det by blast
  next
  case (assign_const_rel x z tailA tailC)
    from assign_const_rel have
    eval_1: "(⟨cC, mdsC, mem1C⟩C, ⟨Stop ;; tailC, mdsC,
               mem1C((Eg2_varC_of_Eg1 x) := z)⟩C) ∈ C.evalw" and
    eval_2: "(⟨cC, mdsC, mem2C⟩C, ⟨Stop ;; tailC, mdsC,
               mem2C((Eg2_varC_of_Eg1 x) := z)⟩C) ∈ C.evalw"
      by (simp add: assign_evalw_constC C.evalw.seq)+
    thus ?thesis unfolding stopsC_def using C.eval_det by blast
  next
  case (if_reg_load_rel x thenA elseA tailA thenC elseC tailC)
    from if_reg_load_rel have
    eval_1: "(⟨cC, mdsC, mem1C⟩C, ⟨Stop ;; Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC, mdsC,
               mem1C(regC := mem1C (Eg2_varC_of_Eg1 x))⟩C) ∈ C.evalw" and
    eval_2: "(⟨cC, mdsC, mem2C⟩C, ⟨Stop ;; Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC, mdsC,
               mem2C(regC := mem2C (Eg2_varC_of_Eg1 x))⟩C) ∈ C.evalw"
      by (simp add: assign_evalw_loadC C.evalw.seq)+
    thus ?thesis unfolding stopsC_def using C.eval_det by blast
  next
  case (if_reg_stop_rel x thenA elseA tailA thenC elseC tailC)
    from if_reg_stop_rel have
    eval_1: "(⟨cC, mdsC, mem1C⟩C,
              ⟨Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC, mdsC, mem1C⟩C) ∈ C.evalw" and
    eval_2: "(⟨cC, mdsC, mem2C⟩C,
              ⟨Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC, mdsC, mem2C⟩C) ∈ C.evalw"
      by (simp add: C.seq_stop_evalw)+
    thus ?thesis unfolding stopsC_def using C.eval_det by blast
  next
  case (if_reg_rel x thenA elseA tailA thenC elseC tailC)
    from if_reg_rel have
    eval_1: "(⟨cC, mdsC, mem1C⟩C,
              ⟨(if evBC mem1C (bexpC.Eq regC 0) then thenC else elseC) ;; tailC, mdsC, mem1C⟩C) ∈ C.evalw" and
    eval_2: "(⟨cC, mdsC, mem2C⟩C,
              ⟨(if evBC mem2C (bexpC.Eq regC 0) then thenC else elseC) ;; tailC, mdsC, mem2C⟩C) ∈ C.evalw"
      by (simp add: if_true_evalwC if_false_evalwC)+
    hence stops_eq: "stopsC ⟨cC, mdsC, mem1C⟩C = stopsC ⟨cC, mdsC, mem2C⟩C"
      unfolding stopsC_def by blast
    (* Side-conditions ensure both programs take the same branch *)
    from in_R R_low_mds_eq
    have "A.low_mds_eq mdsA mem1A mem2A" by clarsimp
    with if_reg_rel(6,13) dma_def
    have "evB mem1A (bexp.Eq x 0) = evB mem2A (bexp.Eq x 0)"
      by (simp add:A.low_mds_eq_def)
    with if_reg_rel(1,2,7) in_RelS_2
    have "evBC mem1C (bexpC.Eq regC 0) = evBC mem2C (bexpC.Eq regC 0)"
      apply clarsimp
      by (cases rule:RelS_Eg1Eg2.cases, simp+)
    with if_reg_rel(1,2) eval_1 eval_2 C.eval_det have
      "(∀mds1C' mds2C' mem1C' mem2C' c1C' c2C'.
           (⟨cC, mdsC, mem1C⟩C, ⟨c1C', mds1C', mem1C'⟩C) ∈ sifum_lang_no_dma.evalw evAC evBC ∧
           (⟨cC, mdsC, mem2C⟩C, ⟨c2C', mds2C', mem2C'⟩C) ∈ sifum_lang_no_dma.evalw evAC evBC ⟶
           c1C' = c2C' ∧ mds1C' = mds2C')"
      by (clarsimp, blast)
    thus ?thesis using stops_eq by simp
  next
  case (stop_seq_rel tailA tailC)
    from stop_seq_rel have
    eval_1: "(⟨cC, mdsC, mem1C⟩C, ⟨tailC, mdsC, mem1C⟩C) ∈ C.evalw" and
    eval_2: "(⟨cC, mdsC, mem2C⟩C, ⟨tailC, mdsC, mem2C⟩C) ∈ C.evalw"
      by (simp add: C.seq_stop_evalw)+
    thus ?thesis unfolding stopsC_def using C.eval_det by blast
  next
  case stop_rel
    with C.stop_no_eval have
      stops_1: "stopsC ⟨cC, mdsC, mem1C⟩C" and
      stops_2: "stopsC ⟨cC, mdsC, mem2C⟩C"
      unfolding stopsC_def by simp+
    thus ?thesis unfolding stopsC_def by auto
  qed
qed

lemma induction_RelS_Eg1Eg2:
notes A.update_modes.simps[simp del]
shows
"(⟨c1A, mdsA, mem1A⟩A, ⟨c1C, mdsC, mem1C⟩C) ∈ RelS_Eg1Eg2 ⟹
       (⟨c1C, mdsC, mem1C⟩C, ⟨c1C', mdsC', mem1C'⟩C) ∈ C.evalw ⟹
       ∃c1A' mdsA' mem1A'.
          A.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) ∈ RelS_Eg1Eg2"
proof(induct rule: RelS_Eg1Eg2.induct)
case (acq_mode_rel cA x m tailA cC tailC mdsA mdsC memA memC)
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  let ?c1A' = "Stop ;; tailA"
  from acq_mode_rel(1,2)
  have abs_steps_acq: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  moreover from acq_mode_rel.prems acq_mode_rel(2)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC(m := insert (Eg2_varC_of_Eg1 x) (mdsC m))" and
    mem1C'_def: "mem1C' = memC"
    by (metis (mono_tags) C.seq_decl_elim C.update_modes.simps(1))+
  moreover from mdsC'_def
  have mdsA'_def: "?mdsA' = A.update_modes (x +=m m) (mdsA_of mdsC)"
    unfolding A.update_modes.simps
    by(blast intro: mode_acquire_refinement_helper)
  moreover with mem1C'_def acq_mode_rel A.evalw.seq A.decl_evalw
  have nevalA: "A.neval ⟨cA, mdsA, memA⟩A 1 ⟨?c1A', ?mdsA', ?mem1A'⟩A"
    by clarsimp
  moreover from acq_mode_rel(5)
  have mdsC'_concrete_vars_unwritable:
    "(∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC' AsmNoReadOrWrite)"
    by(auto simp: mdsC'_def)
  moreover with acq_mode_rel(6)[simplified] acq_mode_rel.hyps(4) nevalA c1C'_def
  have in_Rel': "(⟨?c1A', ?mdsA', ?mem1A'⟩A, ⟨c1C', mdsC', mem1C'⟩C) ∈ RelS_Eg1Eg2"
    by (metis A.neval_Suc_simp One_nat_def acq_mode_rel.prems)
  ultimately show ?case
    by (metis (no_types, opaque_lifting) One_nat_def abs_steps.simps n_not_Suc_n)
next
case (rel_mode_rel cA x m cC mdsA mdsC memA memC)
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  let ?c1A' = "Stop"
  from rel_mode_rel(1,2)
  have abs_steps_acq: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  moreover from rel_mode_rel.prems rel_mode_rel(2)
  have c1C'_def: "c1C' = Stop" and
    mdsC'_def: "mdsC' = mdsC(m := {y. y ∈ (mdsC m) ∧ y ≠ (Eg2_varC_of_Eg1 x)})" and
    mem1C'_def: "mem1C' = memC"
    by (metis (mono_tags) C.upd_elim C.skip_elim C.update_modes.simps(2))+
  moreover from mdsC'_def
  have mdsA'_def: "?mdsA' = A.update_modes (x -=m m) (mdsA_of mdsC)"
    unfolding A.update_modes.simps
    by(blast intro: mode_release_refinement_helper)
  moreover with mem1C'_def rel_mode_rel A.evalw.seq A.decl_evalw
  have nevalA: "A.neval ⟨cA, mdsA, memA⟩A 1 ⟨?c1A', ?mdsA', ?mem1A'⟩A"
    by clarsimp
  moreover from rel_mode_rel(5)
  have mdsC'_concrete_vars_unwritable:
    "(∀vC. vC ∉ range Eg2_varC_of_Eg1 ⟶ vC ∈ mdsC' AsmNoReadOrWrite)"
    by(auto simp: mdsC'_def)
  moreover with rel_mode_rel(6)[simplified] rel_mode_rel.hyps(4) nevalA c1C'_def
  have in_Rel': "(⟨?c1A', ?mdsA', ?mem1A'⟩A, ⟨c1C', mdsC', mem1C'⟩C) ∈ RelS_Eg1Eg2"
    by (metis A.neval_Suc_simp One_nat_def rel_mode_rel.prems)
  ultimately show ?case
    by (metis (no_types, opaque_lifting) One_nat_def abs_steps.simps n_not_Suc_n)
next
case (assign_load_rel cA x y tailA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "Stop ;; tailA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from assign_load_rel(1,2)
  have abs_steps_load: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from assign_load_rel.prems assign_load_rel(2)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC((Eg2_varC_of_Eg1 x) := memC (Eg2_varC_of_Eg1 y))"
    using C.seq_elim C.assign_elim C.skip_elim assign_evalw_loadC
    by (metis (no_types, lifting) Stmt.distinct(14))+
  from assign_load_rel(1,3,4) mdsC'_def mem1C'_def
  have evalA: "(⟨cA, mdsA, memA⟩A,⟨?c1A', ?mdsA', ?mem1A'⟩A) ∈ A.evalw" and
    nevalA: "A.neval ⟨cA, mdsA, memA⟩A 1 ⟨?c1A', ?mdsA', ?mem1A'⟩A"
    using A.evalw.seq assign_evalw_loadA mem_assign_refinement_helper_var by simp+
  with assign_load_rel(11)[simplified] assign_load_rel.prems c1C'_def
  have rel': "(⟨?c1A',?mdsA',?mem1A'⟩A,⟨c1C',mdsC',mem1C'⟩C) ∈ RelS_Eg1Eg2"
    using assign_load_rel.hyps(4-5) mdsC'_def by blast
  thus ?case using rel' abs_steps_load nevalA by auto
next
case (assign_const_rel cA x z tailA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "Stop ;; tailA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from assign_const_rel(1,2)
  have abs_steps_const: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from assign_const_rel.prems assign_const_rel(2)
  have c1C'_def: "c1C' = (Stop ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC((Eg2_varC_of_Eg1 x) := z)"
    using C.seq_elim C.assign_elim C.skip_elim assign_evalw_constC
    by (metis (no_types, lifting) Stmt.distinct(14))+
  from assign_const_rel(1,3,4) mdsC'_def mem1C'_def
  have evalA: "(⟨cA, mdsA, memA⟩A,⟨?c1A', ?mdsA', ?mem1A'⟩A) ∈ A.evalw" and
    nevalA: "A.neval ⟨cA, mdsA, memA⟩A 1 ⟨?c1A', ?mdsA', ?mem1A'⟩A"
    using A.evalw.seq assign_evalw_constA mem_assign_refinement_helper_const by simp+
  with assign_const_rel(9)[simplified] assign_const_rel.prems c1C'_def
  have rel': "(⟨?c1A',?mdsA',?mem1A'⟩A,⟨c1C',mdsC',mem1C'⟩C) ∈ RelS_Eg1Eg2"
    using assign_const_rel.hyps(4) by blast
  thus ?case using rel' abs_steps_const nevalA by auto
next
case (if_reg_load_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_reg_load_rel.hyps(1,2)
  have abs_steps_if_reg_load: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_reg_load_rel.prems if_reg_load_rel(2)
  have c1C'_def: "c1C' = (Stop ;; If (Eq regC 0) thenC elseC ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC(regC := memC (Eg2_varC_of_Eg1 x))"
    using C.seq_elim C.assign_elim C.skip_elim assign_evalw_loadC
    by (metis (no_types, lifting) Stmt.distinct(14))+
  from if_reg_load_rel(1-4) mdsC'_def mem1C'_def
  have nevalA: "A.neval ⟨cA, mdsA, memA⟩A 0 ⟨?c1A', ?mdsA', ?mem1A'⟩A" and
    memA_unchanged: "?mem1A' = memA"
    using regC_not_visible_abs conc_only_var_assign_not_visible_abs A.neval.intros(1) by simp+
  with if_reg_load_rel c1C'_def mdsC'_def mem1C'_def
  have rel': "(⟨?c1A',?mdsA',?mem1A'⟩A,⟨c1C',mdsC',mem1C'⟩C) ∈ RelS_Eg1Eg2"
    apply clarsimp
    apply(erule_tac x=mem1C' in allE)
    apply(erule_tac impE)
     apply(rule_tac x=memC in exI)
     apply(rule conjI)
      apply(clarsimp)
     apply(rule conjI)
      apply clarsimp
      apply (simp add: memA_of_def)
     using if_reg_load_rel.prems memA_of_def apply blast
    apply clarsimp
    done
  show ?case using rel' abs_steps_if_reg_load nevalA by auto
next
case (if_reg_stop_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
  let ?c1A' = "cA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_reg_stop_rel.hyps(1,2)
  have abs_steps_if_reg_stop: "(abs_steps' cA cC) = 0"
    by (simp add:abs_steps'_def)
  from if_reg_stop_rel.prems if_reg_stop_rel(2)
  have c1C'_def: "c1C' = (If (Eq regC 0) thenC elseC ;; tailC)" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by simp+
  from if_reg_stop_rel(1-4) mdsC'_def mem1C'_def
  have nevalA: "A.neval ⟨cA, mdsA, memA⟩A 0 ⟨?c1A', ?mdsA', ?mem1A'⟩A" and
    memA_unchanged: "?mem1A' = memA"
    using regC_not_visible_abs conc_only_var_assign_not_visible_abs A.neval.intros(1) by simp+
  with if_reg_stop_rel c1C'_def mdsC'_def mem1C'_def
  have rel': "(⟨?c1A',?mdsA',?mem1A'⟩A,⟨c1C',mdsC',mem1C'⟩C) ∈ RelS_Eg1Eg2" by blast
  show ?case using rel' abs_steps_if_reg_stop nevalA by auto
next
case (if_reg_rel cA x thenA elseA tailA cC thenC elseC tailC mdsA mdsC memA memC)
  let ?c1A' = "if (evB memA (bexp.Eq x 0)) then (thenA ;; tailA) else (elseA ;; tailA)"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from if_reg_rel(1) if_reg_rel(2)
  have abs_steps_if_reg: "(abs_steps' cA cC) = Suc 0"
    by (simp add:abs_steps'_def)
  from if_reg_rel.prems if_reg_rel(2)
  have c1C'_def: "c1C' = (if (evBC memC (bexpC.Eq regC 0)) then (thenC ;; tailC) else (elseC ;; tailC))" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    apply simp_all
    by (drule C.seq_elim, simp, erule exE, clarsimp, erule C.if_elim, clarsimp+)+
  from if_reg_rel(1,3,4) mdsC'_def mem1C'_def
  have evalA: "(⟨cA, mdsA, memA⟩A, ⟨?c1A', ?mdsA', ?mem1A'⟩A) ∈ A.evalw"
    using if_seq_evalw_helperA A.if_evalw by presburger
  hence nevalA: "A.neval ⟨cA, mdsA, memA⟩A (abs_steps' cA cC) ⟨?c1A', ?mdsA', ?mem1A'⟩A"
    using abs_steps_if_reg by (simp only:A.neval_Suc_simp)
  from if_reg_rel(3,4,7,12) if_reg_rel.prems c1C'_def mdsC'_def mem1C'_def evalA
  have rel': "(⟨?c1A',?mdsA',?mem1A'⟩A, ⟨c1C',mdsC',mem1C'⟩C) ∈ RelS_Eg1Eg2"
    by (clarify, presburger)
  show ?case using rel' abs_steps_if_reg nevalA by auto
next
case (stop_seq_rel cA tailA cC tailC mdsA mdsC memA memC)
  let ?c1A' = "tailA"
  let ?mdsA' = "mdsA_of mdsC'"
  let ?mem1A' = "memA_of mem1C'"
  from stop_seq_rel(1,2)
  have abs_steps_stop: "(abs_steps' cA cC) = 1"
    by (simp add:abs_steps'_def)
  from stop_seq_rel
  have c1C'_def: "c1C' = tailC" and
    mdsC'_def: "mdsC' = mdsC" and
    mem1C'_def: "mem1C' = memC"
    using C.seq_stop_elim by auto
  hence
    nevalA: "A.neval ⟨cA, mdsA, memA⟩A 1 ⟨?c1A', ?mdsA', ?mem1A'⟩A" and
    rel': "(⟨?c1A', ?mdsA', ?mem1A'⟩A, ⟨c1C', mdsC', mem1C'⟩C) ∈ RelS_Eg1Eg2"
    using stop_seq_rel A.seq_stop_evalw by auto
  thus ?case using abs_steps_stop by auto
next
case stop_rel
  with C.stop_no_eval have False by simp
  thus ?case by simp
qed

definition
  mds0 :: "Mode ⇒ varC set"
where
  "mds0 ≡ λm. case m of AsmNoReadOrWrite ⇒ {regC} | _ ⇒ {}"

lemma read_buffer_assign_temp_onwards_RelS:
  "(⟨(temp ← aexp.Const 0) ;; (Skip@[temp -=m AsmNoReadOrWrite]),
         mdsA_of ((case_Mode {regC} {} {} {}) (AsmNoWrite := {control_varC},
                  AsmNoReadOrWrite := {tempC, regC})),
         memA_of memC⟩A,
        ⟨(tempC ← aexpC.Const 0) ;; (Skip@[tempC -=m AsmNoReadOrWrite]),
                  (case_Mode {regC} {} {} {}) (AsmNoWrite := {control_varC},
                  AsmNoReadOrWrite := {tempC, regC}),
                  memC⟩C) ∈ RelS_Eg1Eg2"
  (* Assign temp (Const 0) ;; *)
  apply(rule assign_const_rel, simp+)
   apply(clarsimp simp: regC_the_only_concrete_only_var doesnt_have_mode)+
  apply(drule C.seq_assign_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)
  (* ModeDecl Skip (Rel temp AsmNoReadOrWrite)" *)
  apply(rule rel_mode_rel, simp+)
   apply(clarsimp simp: regC_the_only_concrete_only_var)+
  apply(rule stop_rel)
  done

lemma read_buffer_RelS:
  "(⟨A.read_buffer, mdsA_of mds0, memA_of memC⟩A, ⟨C.read_bufferC, mds0, memC⟩C) ∈ RelS_Eg1Eg2"
  unfolding A.read_buffer_def C.read_bufferC_def mds0_def
  (* ModeDecl Skip (Acq buffer AsmNoWrite) ;; *)
  apply(rule acq_mode_rel, simp+)
   apply(clarsimp simp: regC_the_only_concrete_only_var)+
  apply(drule C.seq_decl_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)
  (* ModeDecl Skip (Acq temp AsmNoReadOrWrite) ;; *)
  apply(rule acq_mode_rel, simp+)
   apply(clarsimp simp: regC_the_only_concrete_only_var)+
  apply(drule C.seq_decl_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)
  (* Assign temp (Load buffer) ;; *)
  apply(rule assign_load_rel, simp+)
   apply(clarsimp simp: regC_the_only_concrete_only_var doesnt_have_mode)+
  apply(drule C.seq_assign_elim, clarsimp)
  apply(rule stop_seq_rel, simp+)
  (* If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp)) ;; *)
  apply(rule if_reg_load_rel, simp+)
   apply(clarsimp simp: regC_the_only_concrete_only_var doesnt_have_mode)+
  apply(drule C.seq_assign_elim, clarsimp)
  apply(rule if_reg_stop_rel, simp+)
     apply(clarsimp simp: regC_the_only_concrete_only_var)
    using has_modeA NoRWA_implies_NoRWC apply fastforce
   apply(clarsimp simp: has_modeA)+
  apply(rule if_reg_rel, simp+)
     apply(clarsimp simp: regC_the_only_concrete_only_var has_modeA doesnt_have_mode)+
   apply(rule conjI)
    (* (Assign low_var (Load temp)) ;; *)
    apply clarsimp
    apply(rule assign_load_rel, simp+)
     apply(clarsimp simp: regC_the_only_concrete_only_var doesnt_have_mode)+
     apply(drule C.seq_assign_elim, clarsimp)
    apply(rule stop_seq_rel, simp+)
    apply(rule read_buffer_assign_temp_onwards_RelS)
   (* (Assign high_var (Load temp)) ;; *)
   apply clarsimp
   apply(rule assign_load_rel, simp+)
    apply(clarsimp simp: regC_the_only_concrete_only_var doesnt_have_mode)+
    apply(drule C.seq_assign_elim, clarsimp)
   apply(rule stop_seq_rel, simp+)
   apply(rule read_buffer_assign_temp_onwards_RelS)
  apply simp
  done

lemma control_var_visible:
  "control_varC ∈ range Eg2_varC_of_Eg1"
  apply(unfold Eg2_varC_of_Eg1_def)
  apply(rule_tac x=control_var in range_eqI)
  apply clarsimp
  done

lemma mdss_A_of_mds0:
  "mdss = mdsA_of mds0"
  apply(rule preserves_modes_mem_mdsA_simp)
  apply clarsimp
  apply(case_tac m)
     unfolding mdss_def mds0_def mdsA_of_def
     apply(clarsimp simp: regC_not_visible_abs control_var_visible)+
  done

lemma A_of_mds0_is_mdss:
  "mdsA_of mds0 = mdss"
  by (simp add: mdss_A_of_mds0)

(* using the bisimulation established by the type system *)

lemma RelS_Eg1Eg2_secure_refinement_simple_ℛ:
  "secure_refinement_simple (A.ℛ Γ 𝒮 P) RelS_Eg1Eg2 abs_steps"
  apply(unfold secure_refinement_simple_def)
  apply(rule conjI)
   apply(rule closed_others_RelS_Eg1Eg2)
  apply(rule conjI)
   apply(rule preserves_modes_mem_RelS_Eg1Eg2)
  apply(rule conjI)
   apply(rule new_vars_private_RelS_Eg1Eg2)
  apply(rule conjI)
   apply(rule simple_refinement_safe_RelS_Eg1Eg2)
   using A.ℛ_to_ℛ3 A.ℛ3_mem_eq apply fast
  apply(rule conjI)
   apply(rule bisim_simple_ℛ)
  apply safe
  apply(drule (1) induction_RelS_Eg1Eg2, clarify)
  done

lemma RelS_Eg1Eg2_secure_refinement_ℛ:
  "secure_refinement (A.ℛ Γ 𝒮 P) RelS_Eg1Eg2 ℐsimple"
  apply(rule secure_refinement_simpler)
  apply(rule secure_refinement_simple)
  apply(rule RelS_Eg1Eg2_secure_refinement_simple_ℛ)
  done

lemma strong_low_bisim_mm_RC_of_RelS_ℛ:
  "conc.strong_low_bisim_mm (RC_of (A.ℛ Γ 𝒮 P) RelS_Eg1Eg2 ℐsimple)"
  apply(rule RC_of_strong_low_bisim_mm)
    apply(rule A.ℛ_bisim)
   apply(rule RelS_Eg1Eg2_secure_refinement_ℛ)
  apply(simp add: sym_def ℐsimple_def)
  done

lemma read_bufferC_secure:
  "conc.low_mds_eq mds0 mem1 mem2 ⟹ ∃ Γ' 𝒮' P'.
   (⟨C.read_bufferC, mds0, mem1⟩C, ⟨C.read_bufferC, mds0, mem2⟩C) ∈ (RC_of (A.ℛ Γ' 𝒮' P') RelS_Eg1Eg2 ℐsimple)"
  apply(insert A.read_buffer_typed[OF HOL.refl HOL.refl HOL.refl])
  apply clarsimp
  apply(rule_tac x=Γ' in exI)
  apply(rule_tac x=a in exI)
  apply(rule_tac x=b in exI)
  apply(rule_tac x=x in exI)
  apply(clarsimp simp: RC_of_def)
  apply(rule_tac x=A.read_buffer in exI)
  apply(rule_tac x="mdsA_of mds0" in exI)
  apply(rule_tac x="memA_of mem1" in exI)
  apply(rule conjI)
   apply(rule read_buffer_RelS)
  apply(rule_tac x=A.read_buffer in exI)
  apply(rule_tac x="mdsA_of mds0" in exI)
  apply(rule_tac x="memA_of mem2" in exI)
  apply(rule conjI)
   apply(rule read_buffer_RelS)
  apply(simp add: A_of_mds0_is_mdss ℐsimple_def)
  apply(drule low_mds_eq_from_conc_to_abs)
  apply(rule A.Typed_in_ℛ, simp)
      unfolding A.tyenv_wellformed_def apply safe
       unfolding A.mds_consistent_def apply clarsimp
      unfolding A.types_wellformed_def mdss_def apply simp
     unfolding A.types_stable_def apply simp
    apply clarsimp
    (* should be easy: low_mds_eq and low var ⟶ equal mem var *)
    unfolding A.low_mds_eq_def apply clarsimp
    apply(rename_tac v, erule_tac x=v in allE)
    apply clarsimp
    apply safe
     apply(clarsimp simp: mdsA_of_def mds0_def)
     apply(rename_tac xb, case_tac xb, simp_all)
    apply(case_tac v, clarsimp)
       unfolding dma_def mds0_def mdsA_of_def pred_def
       using regC_not_visible_abs apply auto[4]
   using A.pred_def apply clarsimp
  using A.pred_def apply clarsimp
  done

lemma "conc.com_sifum_secure (C.read_bufferC, mds0)"
  unfolding conc.com_sifum_secure_def conc.low_indistinguishable_def
  apply clarify
  apply(drule_tac read_bufferC_secure)
  apply(erule exE)+
  apply(rule conc.mm_equiv_intro)
   apply(rule_tac Γ=Γ' and 𝒮=𝒮' and P=P' in strong_low_bisim_mm_RC_of_RelS_ℛ)
  by simp

end

end