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, memAA, cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  RelS_Eg1Eg2" |

  stop_seq_rel: "cA = Stop ;; cA_tail;
    cC = Stop ;; cC_tail;
    mdsA = mdsA_of mdsC;
    memA = memA_of memC;
    (cA_tail, mdsA, memAA, cC_tail, mdsC, memCC)  RelS_Eg1Eg2
    
    (cA, mdsA, memAA, cC, mdsC, memCC)  RelS_Eg1Eg2" |

  stop_rel:
    "(Stop, mdsA_of mdsC, memA_of memCA, Stop, mdsC, memCC)  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 memCA,
    cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  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, memAA, cC, mdsC, memCC)  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, memC, 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, memC, 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, memC, 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, memC, 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, memC, 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, memC, 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, memC, 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, memC, 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, memAA, cC, mdsC, memCC)  RelS_Eg1Eg2" and
      does_eval: "(cC, mdsC, memCC, 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, memA, 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, mem1AA, cA, mdsA, mem2AA)  Some_R" and
       in_RelS_1: "(cA, mdsA, mem1AA, cC, mdsC, mem1CC)  RelS_Eg1Eg2" and
       in_RelS_2: "(cA, mdsA, mem2AA, cC, mdsC, mem2CC)  RelS_Eg1Eg2"
  show "stopsC cC, mdsC, mem1CC = stopsC cC, mdsC, mem2CC 
       (mds1C' mds2C' mem1C' mem2C' c1C' c2C'.
           (cC, mdsC, mem1CC, c1C', mds1C', mem1C'C)  C.evalw 
           (cC, mdsC, mem2CC, 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, mem1CC, Stop ;; tailC, ?mdsC', mem1CC)  C.evalw" and
    eval_2: "(cC, mdsC, mem2CC, Stop ;; tailC, ?mdsC', mem2CC)  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, mem1CC, Stop, ?mdsC', mem1CC)  C.evalw" and
    eval_2: "(cC, mdsC, mem2CC, Stop, ?mdsC', mem2CC)  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, mem1CC, Stop ;; tailC, mdsC,
               mem1C((Eg2_varC_of_Eg1 x) := mem1C (Eg2_varC_of_Eg1 y))C)  C.evalw" and
    eval_2: "(cC, mdsC, mem2CC, 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, mem1CC, Stop ;; tailC, mdsC,
               mem1C((Eg2_varC_of_Eg1 x) := z)C)  C.evalw" and
    eval_2: "(cC, mdsC, mem2CC, 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, mem1CC, 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, mem2CC, 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, mem1CC,
              Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC, mdsC, mem1CC)  C.evalw" and
    eval_2: "(cC, mdsC, mem2CC,
              Stmt.If (bexpC.Eq regC 0) thenC elseC ;; tailC, mdsC, mem2CC)  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, mem1CC,
              (if evBC mem1C (bexpC.Eq regC 0) then thenC else elseC) ;; tailC, mdsC, mem1CC)  C.evalw" and
    eval_2: "(cC, mdsC, mem2CC,
              (if evBC mem2C (bexpC.Eq regC 0) then thenC else elseC) ;; tailC, mdsC, mem2CC)  C.evalw"
      by (simp add: if_true_evalwC if_false_evalwC)+
    hence stops_eq: "stopsC cC, mdsC, mem1CC = stopsC cC, mdsC, mem2CC"
      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, mem1CC, c1C', mds1C', mem1C'C)  sifum_lang_no_dma.evalw evAC evBC 
           (cC, mdsC, mem2CC, 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, mem1CC, tailC, mdsC, mem1CC)  C.evalw" and
    eval_2: "(cC, mdsC, mem2CC, tailC, mdsC, mem2CC)  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, mem1CC" and
      stops_2: "stopsC cC, mdsC, mem2CC"
      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, mem1AA, c1C, mdsC, mem1CC)  RelS_Eg1Eg2 
       (c1C, mdsC, mem1CC, c1C', mdsC', mem1C'C)  C.evalw 
       c1A' mdsA' mem1A'.
          A.neval c1A, mdsA, mem1AA
           (abs_steps c1A, mdsA, mem1AA c1C, mdsC, mem1CC)
           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, memAA 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, memAA 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, memAA,?c1A', ?mdsA', ?mem1A'A)  A.evalw" and
    nevalA: "A.neval cA, mdsA, memAA 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, memAA,?c1A', ?mdsA', ?mem1A'A)  A.evalw" and
    nevalA: "A.neval cA, mdsA, memAA 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, memAA 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, memAA 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, memAA, ?c1A', ?mdsA', ?mem1A'A)  A.evalw"
    using if_seq_evalw_helperA A.if_evalw by presburger
  hence nevalA: "A.neval cA, mdsA, memAA (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, memAA 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 memCA,
        (tempC  aexpC.Const 0) ;; (Skip@[tempC -=m AsmNoReadOrWrite]),
                  (case_Mode {regC} {} {} {}) (AsmNoWrite := {control_varC},
                  AsmNoReadOrWrite := {tempC, regC}),
                  memCC)  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 memCA, C.read_bufferC, mds0, memCC)  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, mem1C, C.read_bufferC, mds0, mem2C)  (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