Theory Example

(*
Title: Value-Dependent SIFUM-Type-Systems
Authors: Toby Murray, Robert Sison, Edward Pierzchalski, Christine Rizkallah
(Based on the SIFUM-Type-Systems AFP entry, whose authors
 are: Sylvia Grewe, Heiko Mantel, Daniel Schoepe)
*)
theory Example
imports "../Compositionality" "../Language" 
begin

datatype addr = control_var | buffer | high_var | low_var | temp
type_synonym val = nat
type_synonym mem = "addr ⇒ val"


datatype aexp = Const val |
                Load addr

fun 
  ev⇩A :: "mem ⇒ aexp ⇒ val"
where
  "ev⇩A mem (Const v) = v" |
  "ev⇩A mem (Load x) = mem x"
 

datatype bexp = Cmp "addr" "addr" |
                Eq "addr" "val" |
                Neq "addr" "val"

fun
  ev⇩B :: "mem ⇒ bexp ⇒ bool"
where
  "ev⇩B mem (Cmp x y) = ((mem x) = (mem y))" | 
  "ev⇩B mem (Eq x v) = ((mem x) = v)"

definition
  dma_control_var :: "val ⇒ Sec"
where
  "dma_control_var v ≡ if v = 0 then Low else High"

definition
  dma :: "mem ⇒ addr ⇒ Sec"
where
  "dma m x ≡ if x = buffer then dma_control_var (m control_var) else if x = high_var then High else Low"

definition
  𝒞_vars :: "addr ⇒ addr set"
where
  "𝒞_vars x ≡ if x = buffer then {control_var} else {}"

definition
  mds⇩s :: "Mode ⇒ 'Var set"
where 
  "mds⇩s ≡ λ_. {}"

locale sifum_example =
  sifum_lang_no_dma ev⇩A ev⇩B +
  assumes eval_det: "(lc, lc') ∈ sifum_lang_no_dma.eval⇩w ev⇩A ev⇩B ⟹ (lc, lc'') ∈ sifum_lang_no_dma.eval⇩w ev⇩A ev⇩B ⟹ lc' = lc''"
 

definition
  𝒞 :: "addr set"
where
  "𝒞 ≡ ⋃x. 𝒞_vars x"

sublocale sifum_example ⊆ sifum_security dma 𝒞_vars 𝒞 eval⇩w undefined
  apply(unfold_locales)
      apply(blast intro: eval_det)
     apply(rule Var_finite)
    apply(auto simp: 𝒞_vars_def dma_def 𝒞_def split: if_splits)
  done

context sifum_example begin


definition
  read_buffer :: "(addr, aexp, bexp) Stmt"
where
  "read_buffer ≡ 
     ModeDecl Skip (Acq buffer AsmNoWrite) ;; 
     ModeDecl Skip (Acq temp AsmNoReadOrWrite) ;;
     Assign temp (Load buffer) ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp))"


(* Note: this invariant ends up tracking mode changes, plus the values of
         variables with an AsmNoWrite assumption --- in this case
         control_var. Thus it feels like it is the sort of thing a 
         flow-sensitive type system should be able to track *)
inductive 
  inv :: "(((addr, aexp, bexp) Stmt, addr, val) LocalConf) ⇒ bool"
where
  inv⇩1: "⟦c = read_buffer; mds AsmNoReadOrWrite = {}; mds AsmNoWrite = {}⟧ ⟹ inv ⟨c, mds, mem⟩" |
  inv⇩1': "⟦c = (Stop ;; 
     ModeDecl Skip (Acq temp AsmNoReadOrWrite) ;;
     Assign temp (Load buffer) ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp)));
     buffer ∈ mds AsmNoWrite; buffer ∉ mds AsmNoReadOrWrite⟧ ⟹
   inv ⟨c, mds, mem⟩" |
  inv⇩2: "⟦c = (ModeDecl Skip (Acq temp AsmNoReadOrWrite) ;;
     Assign temp (Load buffer) ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp)));
     buffer ∈ mds AsmNoWrite;  buffer ∉ mds AsmNoReadOrWrite⟧ ⟹
   inv ⟨c, mds, mem⟩" |
  inv⇩2': "⟦c = (Stop ;; 
     Assign temp (Load buffer) ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp)));
     buffer ∈ mds AsmNoWrite; temp ∈ mds AsmNoReadOrWrite;  buffer ∉ mds AsmNoReadOrWrite⟧ ⟹
   inv ⟨c, mds, mem⟩" |
  inv⇩3: "⟦c = ( 
     Assign temp (Load buffer) ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp)));
     buffer ∈ mds AsmNoWrite; temp ∈ mds AsmNoReadOrWrite; buffer ∉ mds AsmNoReadOrWrite⟧ ⟹
   inv ⟨c, mds, mem⟩" |

  inv⇩3': "⟦c = (
     Stop ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp)));
     buffer ∈ mds AsmNoWrite; temp ∈ mds AsmNoReadOrWrite;  buffer ∉ mds AsmNoReadOrWrite⟧ ⟹
   inv ⟨c, mds, mem⟩" |
  inv⇩4: "⟦c = (
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp)));
     buffer ∈ mds AsmNoWrite; temp ∈ mds AsmNoReadOrWrite; buffer ∉ mds AsmNoReadOrWrite⟧ ⟹
   inv ⟨c, mds, mem⟩" |
  inv⇩5: "⟦c = (
     (Assign low_var (Load temp)));
     buffer ∈ mds AsmNoWrite; temp ∈ mds AsmNoReadOrWrite; mem control_var = 0; buffer ∉ mds AsmNoReadOrWrite⟧ ⟹
   inv ⟨c, mds, mem⟩" |
  inv⇩6: "⟦c = (
     (Assign high_var (Load temp)));
     buffer ∈ mds AsmNoWrite; temp ∈ mds AsmNoReadOrWrite; mem control_var ≠ 0; buffer ∉ mds AsmNoReadOrWrite⟧ ⟹
   inv ⟨c, mds, mem⟩" |
  inv⇩7: "⟦c = Stop⟧ ⟹
   inv ⟨c, mds, mem⟩"

(* Note: this relational invariant is tracking equalities on AsmNoRead
         variables, based on classification in formation which here we
         have encoded as ahead-of-time information about control_var but
         could be written instead as assertions about "dma buffer".
         Again it feels like something a flow-sensitive type system should
         be able to track, assuming we can accurately track changes to dma,
         which feels like it should be possible *)
inductive_set 
  rel_inv :: "(((addr, aexp, bexp) Stmt, addr, val) LocalConf) rel"
where
  "⟦c = ( Stop ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp))); mem control_var = 0; mem temp = mem' temp⟧ ⟹
      (⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ rel_inv" |
  "⟦c = ( Stop ;;
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp))); mem control_var ≠ 0⟧ ⟹
      (⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ rel_inv" |
  "⟦c = (
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp))); mem control_var = 0; mem temp = mem' temp⟧ ⟹
      (⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ rel_inv" |
     "⟦c = (
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp))); mem control_var ≠ 0⟧ ⟹
      (⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ rel_inv" |
  "⟦c = (Assign low_var (Load temp)); mem control_var = 0; 
      mem temp = mem' temp⟧ ⟹
      (⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ rel_inv" |
  "⟦c ≠ (Stop ;; (
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp)))); c ≠ (
     If (Eq control_var 0) (Assign low_var (Load temp)) (Assign high_var (Load temp))); c ≠ (Assign low_var (Load temp))⟧ ⟹
      (⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ rel_inv"

(* the bisimulation is phrased as a conjunction of a global invariant and a 
   relational invariant, defined above, plus the background requirement
   of low-equivalence modulo modes *)
inductive_set  
  R :: "(((addr, aexp, bexp) Stmt, addr, val) LocalConf) rel"
where
  "⟦c = c'; mds = mds'; low_mds_eq mds mem mem'; inv ⟨c,mds,mem⟩;
    (⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ rel_inv⟧ ⟹
   (⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ R"

lemma [simp]:
  "control_var ∈ 𝒞"
  apply(simp add: 𝒞_def)
  apply(rule_tac x=buffer in exI)
  apply(simp add: 𝒞_vars_def)
  done

lemma low_mds_eq_control_var_eq:
  "low_mds_eq mds mem mem' ⟹ mem control_var = mem' control_var"
  apply(auto simp: low_mds_eq_def dma_def)
  done

  
lemma inv_low_mds_eq:
  "⟦c = c'; mds = mds'; low_mds_eq mds mem mem'; inv ⟨c,mds,mem⟩⟧  ⟹
   inv ⟨c',mds',mem'⟩"
  apply(erule inv.cases)
  apply(auto intro: inv.intros dest!: low_mds_eq_control_var_eq)
  done

lemma rel_inv_sym:
  "low_mds_eq mds mem mem' ⟹ (⟨c, mds, mem⟩, ⟨c, mds, mem'⟩) ∈ rel_inv ⟹
    (⟨c, mds, mem'⟩, ⟨c, mds, mem⟩) ∈ rel_inv"
  apply(auto elim!: rel_inv.cases intro: rel_inv.intros simp: low_mds_eq_control_var_eq)
  done

lemma R_sym':
  "(⟨c, mds, mem⟩, ⟨c', mds', mem'⟩) ∈ R ⟹
   (⟨c', mds', mem'⟩, ⟨c, mds, mem⟩) ∈ R"
  apply(rule R.intros)
    apply(blast elim: R.cases dest: low_mds_eq_sym intro: inv_low_mds_eq dest: rel_inv_sym)+
  done

lemma R_sym:
  "sym R"
  by(rule symI, clarify, erule R_sym')


lemma inv_closed_glob_consistent:
  "inv ⟨c', mds', mem⟩ ⟹
       ∀x. case A x of None ⇒ True | Some (v, v') ⇒ mem x ≠ v ⟶ ¬ var_asm_not_written mds' x ⟹
       ∀x. dma mem [∥⇩1 A] x ≠ dma mem x ⟶ ¬ var_asm_not_written mds' x  ⟹
       inv ⟨c', mds', mem [∥⇩1 A]⟩"
  apply(erule inv.cases)
  apply(fastforce intro: inv.intros)+
    apply(clarsimp simp: apply_adaptation_def split: option.splits)
    apply(drule_tac x=control_var in spec)
    apply clarsimp
    apply(drule_tac x=buffer in spec)
    apply(clarsimp simp: dma_def dma_control_var_def split: if_splits)
    apply(auto intro: inv.intros simp: var_asm_not_written_def)[2]
  apply(drule_tac x=control_var in spec)
  apply(drule_tac x=buffer in spec)
  apply(clarsimp simp: dma_def dma_control_var_def split: if_splits option.splits)
  apply(auto intro: inv.intros simp: var_asm_not_written_def)
  done

lemma updates_to_control_var:
  "∀x. dma mem [∥⇩1 A] x ≠ dma mem x ⟶ ¬ var_asm_not_written mds' x  ⟹
    buffer ∈ mds' AsmNoWrite ⟹
    case A control_var of Some (x, y) ⇒ (x = 0) = (mem control_var = 0) | _ ⇒ True"
  apply(drule_tac x=buffer in spec)
  apply(auto simp: apply_adaptation_def split: option.splits simp: dma_def dma_control_var_def split: if_splits simp: var_asm_not_written_def)
  done

lemma blah:
  "∀x a b. A x = Some (a, b) ⟶ (mem x = a ⟶ mem' x ≠ b) ⟶ ¬ var_asm_not_written mds' x ⟹
    mem x = mem' x ⟹
    x ∈ mds' AsmNoReadOrWrite ∨ x ∈ mds' AsmNoWrite ⟹  mem [∥⇩1 A] x = mem' [∥⇩2 A] x"
  apply(auto simp: apply_adaptation_def split: option.splits simp: var_asm_not_written_def)
  done

lemma rel_inv_closed_glob_consistent:
  "inv ⟨c', mds', mem⟩ ⟹ (⟨c', mds', mem⟩, ⟨c', mds', mem'⟩) ∈ rel_inv ⟹
       ∀x a b.
          A x = Some (a, b) ⟶
          (mem x = a ⟶ mem' x ≠ b) ⟶ ¬ var_asm_not_written mds' x ⟹
       ∀x. dma mem [∥⇩1 A] x ≠ dma mem x ⟶ ¬ var_asm_not_written mds' x ⟹
       ∀x. dma mem [∥⇩1 A] x = Low ∧ (x ∈ mds' AsmNoReadOrWrite ⟶ x ∈ 𝒞) ⟶
           mem [∥⇩1 A] x = mem' [∥⇩2 A] x ⟹
       (⟨c', mds', mem [∥⇩1 A]⟩, ⟨c', mds', mem' [∥⇩2 A]⟩) ∈ rel_inv"
  apply(safe elim!: rel_inv.cases elim!: inv.cases)
  apply(unfold read_buffer_def)
  apply(simp_all)
       (* there are actually 14 goals at this point but 8 are solved at the end by auto, so
          we indent as if there were 6 *)
       apply(rule rel_inv.intros(1), simp+)
        apply(drule updates_to_control_var, simp+)
        apply(fastforce split: option.splits simp: apply_adaptation_def)
       apply(fastforce intro!: blah)
      apply(rule rel_inv.intros(2), simp+)
      apply(drule updates_to_control_var, simp+)
      apply(fastforce split: option.splits simp: apply_adaptation_def)
     apply(rule rel_inv.intros(3), simp+)
      apply(drule updates_to_control_var, simp+)
      apply(fastforce split: option.splits simp: apply_adaptation_def)
     apply(fastforce intro!: blah)
    apply(rule rel_inv.intros(4), simp+)
    apply(drule updates_to_control_var, simp+)
    apply(fastforce split: option.splits simp: apply_adaptation_def)
   apply(rule rel_inv.intros(5), simp+)
    apply(drule updates_to_control_var, simp+)
    apply(fastforce split: option.splits simp: apply_adaptation_def)
   apply(fastforce intro!: blah)
  apply(rule rel_inv.intros(6), simp+)
  apply(drule updates_to_control_var, simp+)
  by (auto intro: rel_inv.intros)

lemma R_closed_glob_consistent:
  "closed_glob_consistent R"
  unfolding closed_glob_consistent_def  
  apply(auto elim!: R.cases intro!: R.intros simp: low_mds_eq_def intro!: inv_closed_glob_consistent split: option.splits intro: rel_inv_closed_glob_consistent) 
  done

lemma R_low_mds_eq:
  "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ R ⟹
        low_mds_eq mds mem⇩1 mem⇩2"
  apply(blast elim: R.cases)
  done

lemma decl_eval⇩w':
  assumes mem_unchanged: "mem' = mem"
  assumes upd: "mds' = update_modes upd mds"
  shows "(⟨Skip@[upd], mds, mem⟩, ⟨Stop, mds', mem'⟩) ∈ eval⇩w"
  using decl[OF unannotated, OF skip, where E="[]", simplified, where E1="[]", simplified]
  assms by auto


lemmas decl_eval⇩w = decl[OF unannotated, OF skip, where E="[]", simplified, where E1="[]", simplified]
lemmas seq_stop_eval⇩w = unannotated[OF seq_stop, where E="[]", simplified]
lemmas assign_eval⇩w = unannotated[OF assign, where E="[]", simplified]
lemmas if_eval⇩w = unannotated[OF cond, where E="[]", simplified]
lemmas if_false_eval⇩w = unannotated[OF if_false, where E="[]", simplified]

lemma 𝒞_simp [simp]:
  "𝒞 = {control_var}"
  apply(auto simp: 𝒞_def 𝒞_vars_def split: if_splits)
  done

lemma buffer_eq:
  "mem⇩1 control_var = 0 ⟹ buffer ∉ mds' AsmNoReadOrWrite ⟹ low_mds_eq mds' mem⇩1 mem⇩2  ⟹
  mem⇩1 buffer = mem⇩2 buffer"
  apply(clarsimp simp: low_mds_eq_def)
  apply(drule spec, erule mp)
  apply(clarsimp simp: dma_def dma_control_var_def)
  done

lemma rel_inv_init:
  "buffer ∉ mds' AsmNoReadOrWrite ⟹ low_mds_eq mds' mem⇩1 mem⇩2 ⟹
    (⟨Stop ;;
      Stmt.If (Eq control_var 0) (low_var ← Load temp)
       (high_var ← Load temp), mds', mem⇩1
     (temp := ev⇩A mem⇩1 (Load buffer))⟩,
     ⟨Stop ;;
      Stmt.If (Eq control_var 0) (low_var ← Load temp)
       (high_var ← Load temp), mds', mem⇩2
     (temp := ev⇩A mem⇩2 (Load buffer))⟩)
    ∈ rel_inv"
  apply(case_tac "mem⇩1 control_var = 0")
   apply(frule (2) buffer_eq)    
  apply(fastforce intro: rel_inv.intros simp: ev⇩A.simps)+
  done

lemma R_inv:
  notes ev⇩A.simps[simp del]
  shows  "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ R ⟹
       (⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩1', mds', mem⇩1'⟩) ∈ eval⇩w ⟹
       ∃c⇩2' mem⇩2'.
          (⟨c⇩2, mds, mem⇩2⟩, ⟨c⇩2', mds', mem⇩2'⟩) ∈ eval⇩w ∧
          (⟨c⇩1', mds', mem⇩1'⟩, ⟨c⇩2', mds', mem⇩2'⟩) ∈ R"
  apply(erule R.cases)
  apply clarsimp
  apply(erule inv.cases)
           apply clarsimp
           apply(rule_tac x=c⇩1' in exI)
           apply(rule_tac x=mem⇩2 in exI)
           apply(unfold read_buffer_def)
           apply(drule seq_elim, simp)
           apply clarsimp
           apply(drule upd_elim, drule skip_elim, simp)
           apply clarsimp
           apply(rule conjI)
            apply(rule eval⇩w.seq)
            apply(rule decl_eval⇩w', simp+)
           apply(rule R.intros, simp+)
             apply(fastforce simp: low_mds_eq_def)
            apply(rule inv⇩1', simp+)
           apply(fastforce intro: rel_inv.intros)
          apply clarsimp
          apply(drule seq_stop_elim, clarsimp)
          apply(rule exI)+
          apply(intro conjI)
           apply(rule seq_stop_eval⇩w)
          apply(rule R.intros, simp+)
           apply(blast intro: inv.intros)
          apply(fastforce intro: rel_inv.intros)
         apply clarsimp
         apply(rule_tac x=c⇩1' in exI)
         apply(rule_tac x=mem⇩2 in exI)
         apply(drule seq_elim, simp)
         apply clarsimp
         apply(drule upd_elim, drule skip_elim, simp)
         apply clarsimp
         apply(rule conjI)
          apply(rule eval⇩w.seq)
          apply(rule decl_eval⇩w', simp+)
         apply(rule R.intros, simp+)
           apply(fastforce simp: low_mds_eq_def)
          apply(rule inv⇩2', simp+)
         apply(fastforce intro: rel_inv.intros)
        apply clarsimp
        apply(drule seq_stop_elim, clarsimp)
        apply(rule exI)+
        apply(intro conjI)
         apply(rule seq_stop_eval⇩w)
        apply(rule R.intros, simp+)
         apply(blast intro: inv.intros)
        apply(fastforce intro: rel_inv.intros)
       apply clarsimp
       apply(rule exI)+
       apply(drule seq_elim, simp)
       apply clarsimp
       apply(drule assign_elim)
       apply clarsimp
       apply(rule conjI)
        apply(rule eval⇩w.seq)
        apply(rule assign_eval⇩w)
       apply(rule R.intros, simp+)
         apply(clarsimp simp: low_mds_eq_def ev⇩A.simps)
         apply(fastforce simp: dma_def split: if_splits)[1]
        apply(rule inv⇩3', simp+)
       apply(fastforce intro: rel_inv_init)
      apply clarsimp
      apply(drule seq_stop_elim, clarsimp)
      apply(rule exI)+
      apply(intro conjI)
       apply(rule seq_stop_eval⇩w)
      apply(rule R.intros, simp+)
       apply(blast intro: inv.intros)
      apply(auto intro: rel_inv.intros elim!: rel_inv.cases)[1]    
     apply clarsimp
     apply(rule exI)+
     apply(erule if_elim)
      apply(rule conjI)
       apply simp
       apply(rule if_eval⇩w)
      apply simp
      apply(rule conjI)
       apply(rule impI)
       apply(rule R.intros, simp+)
        apply(blast intro: inv.intros)
       apply(auto intro: rel_inv.intros elim!: rel_inv.cases)[1]
      apply(simp add: low_mds_eq_control_var_eq)+
     apply(rule conjI)
      apply(rule if_false_eval⇩w, simp)
     apply(rule R.intros, simp+)
      apply(rule inv⇩6, (simp add: low_mds_eq_control_var_eq)+)
     apply(fastforce intro: rel_inv.intros)
    apply clarsimp
    apply(rule exI)+
    apply(drule assign_elim)
    apply(rule conjI)
     apply simp
     apply(rule assign_eval⇩w)
      apply(simp add: low_mds_eq_control_var_eq)
     apply(rule R.intros, simp+)
      apply(clarsimp simp: low_mds_eq_def dma_def)
      apply(simp add: ev⇩A.simps)
      apply(clarsimp split: if_splits)[1]
      apply(fastforce elim: rel_inv.cases)
     apply(fastforce intro: inv.intros)
    apply(fastforce intro: rel_inv.intros)
   apply clarsimp
   apply(rule exI)+
   apply(drule assign_elim)
   apply(rule conjI)
    apply simp
    apply(rule assign_eval⇩w)
     apply(simp add: low_mds_eq_control_var_eq)
    apply(rule R.intros, simp+)
     apply(clarsimp simp: low_mds_eq_def dma_def)
     apply(simp add: ev⇩A.simps)
     apply(clarsimp split: if_splits)[1]
    apply(fastforce intro: inv.intros)
   apply(fastforce intro: rel_inv.intros)
  using stop_no_eval by fastforce

lemma strong_low_bisim_mm_R:
  "strong_low_bisim_mm R"
unfolding strong_low_bisim_mm_def
proof(safe)
  show "sym R" by(rule R_sym)
next
  show "closed_glob_consistent R" by(rule R_closed_glob_consistent)
next
  fix c⇩1 mds mem⇩1 c⇩2  mem⇩2
  assume "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ R"
  thus "low_mds_eq mds mem⇩1 mem⇩2"
  by(rule R_low_mds_eq)
next
  fix c⇩1 mds mem⇩1 c⇩2  mem⇩2 c⇩1' mds' mem⇩1'
  assume "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩2, mds, mem⇩2⟩) ∈ R"
     and "(⟨c⇩1, mds, mem⇩1⟩, ⟨c⇩1', mds', mem⇩1'⟩) ∈ eval⇩w"
  thus "∃c⇩2' mem⇩2'.
        (⟨c⇩2, mds, mem⇩2⟩, ⟨c⇩2', mds', mem⇩2'⟩) ∈ eval⇩w ∧
        (⟨c⇩1', mds', mem⇩1'⟩, ⟨c⇩2', mds', mem⇩2'⟩) ∈ R"
    by(rule R_inv)
qed
    
lemma read_buffer_secure':
  "low_mds_eq mds⇩s mem⇩1 mem⇩2 ⟹
       (⟨read_buffer, mds⇩s, mem⇩1⟩, ⟨read_buffer, mds⇩s, mem⇩2⟩) ∈ R"
  apply(rule R.intros)
  apply simp_all
   apply(rule inv⇩1)
     apply (simp_all add: mds⇩s_def)
  unfolding read_buffer_def by(fastforce intro: rel_inv.intros)

lemma "com_sifum_secure (read_buffer,mds⇩s)"
  unfolding com_sifum_secure_def low_indistinguishable_def
  apply clarify
  apply(rule mm_equiv_intro)
   apply(rule strong_low_bisim_mm_R)
  by(rule read_buffer_secure')  

end
 
end