Theory Fun1_insecure

subsection "Proof"
theory Fun1_insecure
imports Fun1
begin


subsubsection "Concrete leak"

definition "PC ≡ {0..6}"

definition "same_xx cfg3 cfgs3 cfg4 cfgs4 ≡ 
 vstore (getVstore (stateOf cfg3)) xx = vstore (getVstore (stateOf cfg4)) xx ∧
 (∀cfg3'∈set cfgs3. vstore (getVstore (stateOf cfg3')) xx = vstore (getVstore (stateOf cfg3)) xx) ∧ 
 (∀cfg4'∈set cfgs4. vstore (getVstore (stateOf cfg4')) xx = vstore (getVstore (stateOf cfg4)) xx)"

(* two possible program traces for normal execution*)
definition "trueProg = {2,3,4,5,6}"
definition "falseProg = {2,3,5,6}"


(*pstate *)
definition "pstate⇩1 ≡ update pstate⇩0 [3]"
definition "pstate⇩2 ≡ update pstate⇩1 [5,5]"

lemmas pstate_def = pstate⇩1_def pstate⇩2_def

(*heap*)
(*provide different memories*)
fun hh⇩3:: "nat ⇒ int" where 
"hh⇩3 x =  (if x = (nat NN + 1) then 5 else 0)"

definition "h⇩3 ≡(Heap hh⇩3)"

fun hh⇩4:: "nat ⇒ int" where 
"hh⇩4 x = (if x = (nat NN + 1) then 6 else 0)"

definition "h⇩4 ≡(Heap hh⇩4)"

lemmas h_def = h⇩3_def h⇩4_def hh⇩3.simps hh⇩4.simps

(*used to show difference in heap vals*)
lemma ss_neq_aux1:"nat(5 * 512) ≠ nat (6 * 512)" by auto
lemma ss_neq_aux2:"nat(3 * 512) ≠ nat (5 * 512)" by auto
lemmas ss_neq = ss_neq_aux1 ss_neq_aux2
(*pointer*)
definition "p ≡ nat size_aa1 + nat size_aa2"

(*vstore and reads*)

definition "vs⇩1 ≡ (vs⇩0(xx := NN + 1))"


definition "vs⇩2 ≡ (vs⇩1(tt := 0))"

definition "aa1⇩i ≡ array_loc aa1 (nat (vs⇩2 xx)) avst'"

(*divergence between 3 and 4*)

definition "aa2⇩v⇩s⇩3 ≡ array_loc aa2 (nat (hh⇩3 aa1⇩i * 512)) avst'"

definition "vs⇩3⇩3 = vs⇩2(tt := hh⇩3 aa2⇩v⇩s⇩3)"

(**)
definition "aa2⇩v⇩s⇩4 ≡ array_loc aa2 (nat (hh⇩4 aa1⇩i * 512)) avst'"

definition "vs⇩3⇩4 = vs⇩2(tt := hh⇩4 aa2⇩v⇩s⇩4)"

lemmas reads⇩m_def = aa1⇩i_def aa2⇩v⇩s⇩3_def aa2⇩v⇩s⇩4_def
lemmas vs_def = vs⇩0.simps vs⇩1_def vs⇩2_def vs⇩3⇩3_def vs⇩3⇩4_def


(*states*)
definition "s⇩0⇩3 ≡ (State (Vstore vs⇩0) avst' h⇩3 p)"
definition "s⇩1⇩3 ≡ (State (Vstore vs⇩1) avst' h⇩3 p)"
definition "s⇩2⇩3 ≡ (State (Vstore vs⇩2) avst' h⇩3 p)"
definition "s⇩3⇩3 ≡ (State (Vstore vs⇩3⇩3) avst' h⇩3 p)"

definition "s⇩0⇩4 ≡ (State (Vstore vs⇩0) avst' h⇩4 p)"
definition "s⇩1⇩4 ≡ (State (Vstore vs⇩1) avst' h⇩4 p)"
definition "s⇩2⇩4 ≡ (State (Vstore vs⇩2) avst' h⇩4 p)"
definition "s⇩3⇩4 ≡ (State (Vstore vs⇩3⇩4) avst' h⇩4 p)"

lemmas s_def = s⇩0⇩3_def s⇩1⇩3_def s⇩2⇩3_def s⇩3⇩3_def 
               s⇩0⇩4_def s⇩1⇩4_def s⇩2⇩4_def s⇩3⇩4_def

(*s3 stateA's*)
definition "(s3⇩0:: stateO) ≡ (pstate⇩0, (Config 0 s⇩0⇩3), [], repeat (NN+1), repeat (NN+1), {})"
definition "(s3⇩1:: stateO) ≡ (pstate⇩0, (Config 1 s⇩0⇩3), [], repeat (NN+1), repeat (NN+1), {})"
definition "(s3⇩2:: stateO) ≡ (pstate⇩0, (Config 2 s⇩1⇩3), [], repeat (NN+1), repeat (NN+1), {})"
definition "(s3⇩3:: stateO) ≡ (pstate⇩0, (Config 3 s⇩2⇩3), [], repeat (NN+1), repeat (NN+1), {})"
definition "(s3⇩4:: stateO) ≡ (pstate⇩1, (Config 5 s⇩2⇩3), [Config 4 s⇩2⇩3], repeat (NN+1), repeat (NN+1), {})"
definition "(s3⇩5:: stateO) ≡ (pstate⇩1, (Config 5 s⇩2⇩3), [Config 5 s⇩3⇩3], repeat (NN+1), repeat (NN+1), {aa2⇩v⇩s⇩3, aa1⇩i})"
definition "(s3⇩6:: stateO) ≡ (pstate⇩2, (Config 5 s⇩2⇩3), [], repeat (NN+1), repeat (NN+1), {aa2⇩v⇩s⇩3, aa1⇩i})"
definition "(s3⇩7:: stateO) ≡ (pstate⇩2, (Config 6 s⇩2⇩3), [], repeat (NN+1), repeat (NN+1), {aa2⇩v⇩s⇩3, aa1⇩i})"

lemmas s3_def = s3⇩0_def s3⇩1_def s3⇩2_def s3⇩3_def s3⇩4_def s3⇩5_def s3⇩6_def s3⇩7_def

lemmas state_def = s_def h_def vs_def reads⇩m_def pstate_def avst_defs


(*s3 transition list*)
definition "s3_trans ≡ [s3⇩0, s3⇩1, s3⇩2, s3⇩3, s3⇩4, s3⇩5, s3⇩6, s3⇩7]"
lemmas s3_trans_defs = s3_trans_def s3_def 

lemma hd_s3_trans[simp]: "hd s3_trans = s3⇩0" by (simp add: s3_trans_def)
lemma s3_trans_nemp[simp]: "s3_trans ≠ []" by (simp add: s3_trans_def)


(*transitions*)
lemma s3⇩0⇩1[simp]:"s3⇩0 →S s3⇩1"
  unfolding s3_def
  using nonspec_normal
  by simp

lemma s3⇩1⇩2[simp]:"s3⇩1 →S s3⇩2"
  unfolding s3_def state_def
  using nonspec_normal
  by simp

lemma s3⇩2⇩3[simp]:"s3⇩2 →S s3⇩3"
  unfolding s3_def state_def
  by (simp add: finalM_iff)

lemma s3⇩3⇩4[simp]:"s3⇩3 →S s3⇩4"
  unfolding s3_def state_def
  using nonspec_mispred
  by (simp add: finalM_iff)

lemma s3⇩4⇩5[simp]:"s3⇩4 →S s3⇩5"
  unfolding s3_def state_def
  using spec_normal
  by (simp_all add: finalM_iff, blast) 

lemma s3⇩5⇩6[simp]:"s3⇩5 →S s3⇩6"
  unfolding s3_def state_def
  using spec_resolve
  by simp

lemma s3⇩6⇩7[simp]:"s3⇩6 →S s3⇩7"
  unfolding s3_def state_def
  using nonspec_normal
  by simp

lemma finalS_s3⇩7[simp]:"finalS s3⇩7"
  unfolding finalS_def final_def s3_def
  by (simp add: stepS_endPC)

lemmas s3_trans_simps = s3⇩0⇩1 s3⇩1⇩2 s3⇩2⇩3 s3⇩3⇩4 s3⇩4⇩5 s3⇩5⇩6 s3⇩6⇩7

(*s4 stateA's*)
definition "(s4⇩0:: stateO) ≡ (pstate⇩0, (Config 0 s⇩0⇩4), [], repeat (NN+1), repeat (NN+1), {})"
definition "(s4⇩1:: stateO) ≡ (pstate⇩0, (Config 1 s⇩0⇩4), [], repeat (NN+1), repeat (NN+1), {})"
definition "(s4⇩2:: stateO) ≡ (pstate⇩0, (Config 2 s⇩1⇩4), [], repeat (NN+1), repeat (NN+1), {})"
definition "(s4⇩3:: stateO) ≡ (pstate⇩0, (Config 3 s⇩2⇩4), [], repeat (NN+1), repeat (NN+1), {})"
definition "(s4⇩4:: stateO) ≡ (pstate⇩1, (Config 5 s⇩2⇩4), [Config 4 s⇩2⇩4], repeat (NN+1), repeat (NN+1), {})"
definition "(s4⇩5:: stateO) ≡ (pstate⇩1, (Config 5 s⇩2⇩4), [Config 5 s⇩3⇩4], repeat (NN+1), repeat (NN+1), {aa2⇩v⇩s⇩4, aa1⇩i})"
definition "(s4⇩6:: stateO) ≡ (pstate⇩2, (Config 5 s⇩2⇩4), [], repeat (NN+1), repeat (NN+1), {aa2⇩v⇩s⇩4, aa1⇩i})"
definition "(s4⇩7:: stateO) ≡ (pstate⇩2, (Config 6 s⇩2⇩4), [], repeat (NN+1), repeat (NN+1), {aa2⇩v⇩s⇩4, aa1⇩i})"

lemmas s4_def = s4⇩0_def s4⇩1_def s4⇩2_def s4⇩3_def s4⇩4_def s4⇩5_def s4⇩6_def s4⇩7_def


(*s4 transition list*)
definition "s4_trans ≡ [s4⇩0, s4⇩1, s4⇩2, s4⇩3, s4⇩4, s4⇩5, s4⇩6, s4⇩7]"
lemmas s4_trans_defs = s4_trans_def s4_def

lemma hd_s4_trans[simp]: "hd s4_trans = s4⇩0" by (simp add: s4_trans_def)
lemma s4_trans_nemp[simp]: "s4_trans ≠ []" by (simp add: s4_trans_def)


(*transitions*)
lemma s4⇩0⇩1[simp]:"s4⇩0 →S s4⇩1"
  unfolding s4_def
  using nonspec_normal
  by simp

lemma s4⇩1⇩2[simp]:"s4⇩1 →S s4⇩2"
  unfolding s4_def state_def
  using nonspec_normal
  by simp

lemma s4⇩2⇩4[simp]:"s4⇩2 →S s4⇩3"
  unfolding s4_def state_def
  using nonspec_normal
  by (simp add: finalM_iff)

lemma s4⇩3⇩4[simp]:"s4⇩3 →S s4⇩4"
  unfolding s4_def state_def
  using nonspec_mispred
  by (simp add: finalM_iff)

lemma s4⇩4⇩5[simp]:"s4⇩4 →S s4⇩5"
  unfolding s4_def state_def
  using spec_normal 
  by (simp add: finalM_iff, blast)

lemma s4⇩5⇩6[simp]:"s4⇩5 →S s4⇩6"
  unfolding s4_def state_def
  using spec_resolve
  by simp

lemma s4⇩6⇩7[simp]:"s4⇩6 →S s4⇩7"
  unfolding s4_def state_def
  using nonspec_normal
  by simp

lemma finalS_s4⇩7[simp]:"finalS s4⇩7"
  unfolding finalS_def final_def s4_def
  by (simp add: stepS_endPC)


lemmas s4_trans_simps = s4⇩0⇩1 s4⇩1⇩2 s4⇩2⇩4 s4⇩3⇩4 s4⇩4⇩5 s4⇩5⇩6 s4⇩6⇩7



subsubsection "Auxillary lemmas for disproof"
lemma validS_s3_trans[simp]:"Opt.validS s3_trans"
  unfolding Opt.validS_def validTransO.simps s3_trans_def
  apply safe  
  subgoal for i using cases_5[of i] 
    by(elim disjE, simp_all) .


lemma validS_s4_trans[simp]:"Opt.validS s4_trans"
  unfolding Opt.validS_def validTransO.simps s4_trans_def
  apply safe
  subgoal for i using cases_5[of i] 
  by(elim disjE, simp_all) .


lemma finalS_s3[simp]:"finalS (last s3_trans)" by (simp add: s3_trans_def)
lemma finalS_s4[simp]:"finalS (last s4_trans)" by (simp add: s4_trans_def)

lemma filter_s3[simp]:"(filter isIntO (butlast s3_trans)) = (butlast s3_trans)"
  unfolding s3_trans_def finalS_def final_def
  using s3_trans_simps validTransO.simps validTransO_iff_nextS 
  by (smt (verit) butlast.simps(2) filter.simps(1,2) isIntO.elims(3))

lemma filter_s4[simp]:"(filter isIntO (butlast s4_trans)) = (butlast s4_trans)"
  unfolding s4_trans_def finalS_def final_def
  using s4_trans_simps validTransO.simps validTransO_iff_nextS 
  by (smt (verit) butlast.simps(2) filter.simps(1,2) isIntO.elims(3))

lemma S_s3_trans[simp]:"Opt.S s3_trans = [s⇩0⇩3]"
  apply (simp add: Opt.S_def filtermap_def)
  unfolding s3_trans_defs by simp

lemma S_s4_trans[simp]:"Opt.S s4_trans = [s⇩0⇩4]"
  apply (simp add: Opt.S_def filtermap_def)
  unfolding s4_trans_defs by simp


lemma finalB_noStep[simp]:"⋀s1'. finalB (cfg1, ibT1, ibUT1) ⟹ (cfg1, ibT1, ibUT1, ls1) →N s1' ⟹ False"
  unfolding finalN_def final_def finalB_eq_finalN by auto

subsubsection "Disproof of fun1"
(*DISPROOF*)
fun common_memory::"config ⇒ config ⇒ bool" where 
"common_memory cfg1 cfg2 =
 (let h1 = (getHheap (stateOf cfg1)); 
      h2 = (getHheap (stateOf cfg2)) in
 ((∀x∈read_add. h1 x = h2 x ∧ h1 x = 0) ∧
  (getAvstore (stateOf cfg1)) = avst' ∧
  (getAvstore (stateOf cfg2)) = avst'))"
(*for proof ease*)
lemma heap_eq0[simp]: "∀x. x ≠ Suc NN ⟶ hh1' x = hh2' x ∧ hh1' x = 0 ⟹ hh2' NN = 0" 
  by (metis n_not_Suc_n)
lemma heap1_eq0[simp]:"∀x. x ≠ Suc NN ⟶ hh1' x = hh2' x ∧ hh1' x = 0 ⟹
               vs2 xx < NN ⟹
               hh2' (nat (vs2 xx)) = 0"
  using le_less_Suc_eq nat_le_eq_zle nat_less_eq_zless 
  by (metis lessI nat_int order.asym)

fun Γ_inv::"stateV ⇒ state list ⇒ stateV ⇒ state list ⇒ bool" where
"Γ_inv (cfg1,ibT1,ibUT1,ls1) sl1 (cfg2,ibT2,ibUT2,ls2) sl2 = 
(
 (pcOf cfg1 = pcOf cfg2) ∧ 

 (pcOf cfg1 < 2 ⟶ ibUT1 ≠ LNil ∧ ibUT2 ≠ LNil) ∧ 

 (pcOf cfg1 > 2 ⟶ same_var_val tt 0 cfg1 cfg2) ∧

 (pcOf cfg1 > 1 ⟶ (same_var xx cfg1 cfg2) ∧

                    (vs⇩i_t cfg1 ⟶ pcOf cfg1 ∈ trueProg) ∧

                    (vs⇩i_f cfg1 ⟶ pcOf cfg1 ∈ falseProg))
 ∧
 ls1 = ls2 ∧

 pcOf cfg1 ∈ PC ∧
 common_memory cfg1 cfg2
)"

declare Γ_inv.simps[simp del]
lemmas Γ_def = Γ_inv.simps
lemmas Γ_defs = Γ_def common_memory.simps PC_def aa1⇩i_def
                trueProg_def falseProg_def same_var_val_def same_var_def

lemma Γ_implies:"Γ_inv (cfg1,ibT1, ibUT1,ls1) sl1 (cfg2,ibT2,ibUT2,ls2) sl2 ⟹ 
  pcOf cfg1 ≤ 6 ∧ pcOf cfg2 ≤ 6 ∧ 

  (pcOf cfg1 = 4 ⟶ vs⇩i_t cfg1) ∧
  (pcOf cfg2 = 4 ⟶ vs⇩i_t cfg2) ∧
  (pcOf cfg1 > 1 ⟶ vs⇩i_t cfg1 ⟷ vs⇩i_t cfg2) ∧

  (finalB (cfg1,ibT1,ibUT1) ⟷ pcOf cfg1 = 6) ∧
  (finalB (cfg2,ibT2,ibUT2) ⟷ pcOf cfg2 = 6)
"
  unfolding Γ_defs
  apply(elim conjE, intro conjI)
  subgoal using atLeastAtMost_iff by blast
  subgoal using vs_xx_cases[of cfg2] by (elim disjE, simp_all) 
  subgoal apply (rule impI,simp) using vs_xx_cases[of cfg1] by (elim disjE, simp_all)
  subgoal apply (rule impI,simp) using vs_xx_cases[of cfg2] vs⇩i_defs by (elim disjE, simp_all)
  subgoal by (simp add: vs⇩i_defs)
  using finalB_pcOf_iff 
   apply (metis atLeastAtMost_iff one_less_numeral_iff semiring_norm(76))
  using finalB_pcOf_iff
  by (metis atLeastAtMost_iff numeral_One numeral_less_iff semiring_norm(76))

(*istate*)
lemma istateO_s3[simp]:"istateO s3⇩0" unfolding s3_def state_def by simp
lemma istateO_s4[simp]:"istateO s4⇩0" unfolding s4_def state_def by simp

(*validFromS*)
lemma validFromS_s3[simp]:"Opt.validFromS s3⇩0 s3_trans"
  unfolding Opt.validFromS_def by simp

lemma validFromS_s4[simp]:"Opt.validFromS s4⇩0 s4_trans"
  unfolding Opt.validFromS_def by simp

(*completedFromO*)

lemma completedFromO_s3[simp]:"completedFromO s3⇩0 s3_trans"
  unfolding Opt.completedFrom_def by simp

lemma completedFromO_s4[simp]:"completedFromO s4⇩0 s4_trans"
  unfolding Opt.completedFrom_def by simp

(*Act eq*)
lemma Act_eq[simp]:"Opt.A s3_trans = Opt.A s4_trans"
  apply (simp add: Opt.A_def filtermap_def)
  unfolding s3_trans_defs s4_trans_defs
  by simp

lemma aa2_neq:"aa2⇩v⇩s⇩3 ≠ aa2⇩v⇩s⇩4"
  unfolding vs_def reads⇩m_def avst_defs h_def array_loc_def  
  by (simp add: avst_defs array_base_def split: if_splits)

lemma aa1_neq:"aa2⇩v⇩s⇩3 ≠ aa1⇩i"
  apply(rule notI)
  unfolding vs_def reads⇩m_def avst_defs h_def array_loc_def  
  by (simp add: avst_defs array_base_def split: if_splits)

lemma aa1_neq2:"aa2⇩v⇩s⇩4 ≠ aa1⇩i"
  apply(rule notI)
  unfolding vs_def reads⇩m_def avst_defs h_def array_loc_def  
  by (simp add: avst_defs array_base_def split: if_splits)

(*Obs neq*)
lemma Obs_neq[simp]:"Opt.O s3_trans ≠ Opt.O s4_trans"
  apply (simp add: Opt.O_def filtermap_def)
  unfolding s3_trans_def s4_trans_def apply clarsimp
  unfolding s3_trans_defs s4_trans_defs apply simp
  using aa2_neq aa1_neq aa1_neq2 by blast
   
  

lemma Γ_init[simp]:"⋀s1 s2. istateV s1 ⟹ corrState s1 s3⇩0 ⟹ istateV s2 ⟹ corrState s2 s4⇩0 ⟹ Γ_inv s1 [s⇩0⇩3] s2 [s⇩0⇩4]"
  subgoal for s1 s2 apply(cases s1, cases s2, simp) 
    unfolding s3_def s4_def s_def h_def by (auto simp: Γ_defs) .

lemma val_neq_1:"nat (hh2' (nat (vs2 xx)) * 512) ≠ 1" 
  by (smt (z3) nat_less_eq_zless nat_one_as_int)


(*unwindSD*)
lemma unwindSD[simp]:"Rel_Sec.unwindSDCond validTransV istateV isSecV getSecV isIntV getIntV Γ_inv"
unfolding unwindSDCond_def
proof(intro allI, rule impI, elim conjE,intro conjI)
      fix ss1 ss2 sl1 sl2
      assume "reachV ss1" "reachV ss2" 
       and Γ:"Γ_inv ss1 sl1 ss2 sl2"

      obtain cfg1 ibT1 ibUT1 ls1 where ss1: "ss1 = (cfg1, ibT1, ibUT1, ls1)"
        by (cases ss1, auto) 
      obtain cfg2 ibT2 ibUT2 ls2 where ss2: "ss2 = (cfg2, ibT2, ibUT2, ls2)"
        by (cases ss2, auto) 
      note ss = ss1 ss2 

      obtain pc1 vs1 avst1 h1 p1 where 
        cfg1: "cfg1 = Config pc1 (State (Vstore vs1) avst1 h1 p1)"
        by (cases cfg1) (metis state.collapse vstore.collapse)
      obtain pc2 vs2 avst2 h2 p2 where 
        cfg2: "cfg2 = Config pc2 (State (Vstore vs2) avst2 h2 p2)"
        by (cases cfg2) (metis state.collapse vstore.collapse)
      note cfg = cfg1 cfg2

      obtain hh1 where h1: "h1 = Heap hh1" by(cases h1, auto)
      obtain hh2 where h2: "h2 = Heap hh2" by(cases h2, auto)
      note hh = h1 h2

      show "isIntV ss1 = isIntV ss2" 
        using  Γ unfolding isIntV.simps ss
        unfolding Γ_defs
        using vs_xx_cases[of cfg1]
        apply (elim disjE) by simp_all

      then have finalB:"finalB (cfg1, ibT1, ibUT1) = finalB (cfg2, ibT2, ibUT2)"
        unfolding isIntV.simps finalN_iff_finalB ss by blast

      show "¬ isIntV ss1 ⟶ move1 Γ_inv ss1 sl1 ss2 sl2 ∧ move2 Γ_inv ss1 sl1 ss2 sl2"
        apply(unfold ss, auto)
        subgoal unfolding move1_def finalB_defs by auto
        subgoal unfolding finalB 
                unfolding move2_def finalB_defs by auto . 

      show "isIntV ss1 ⟶ getActV ss1 = getActV ss2 ⟶ getObsV ss1 = getObsV ss2 ∧ move12 Γ_inv ss1 sl1 ss2 sl2"
      proof(unfold ss isIntV.simps finalN_iff_finalB, intro impI, rule conjI)
        assume final:"¬ finalB (cfg1, ibT1, ibUT1)" and
              getAct:"getActV (cfg1, ibT1, ibUT1, ls1) = getActV (cfg2, ibT2, ibUT2, ls2)"
        have not6:"pc1 = 6 ⟹ False"
          using cfg final Γ
          by simp

        show "getObsV (cfg1, ibT1, ibUT1, ls1) = getObsV (cfg2, ibT2, ibUT2, ls2)" 
          using Γ getAct unfolding ss 
          apply-apply(frule Γ_implies, elim conjE)
          using cases_5[of "pcOf cfg1"] cases_5[of "pcOf cfg2"] 
          by(elim disjE, simp_all add: Γ_defs final)

        show "move12 Γ_inv (cfg1, ibT1, ibUT1, ls1) sl1 (cfg2, ibT2, ibUT2, ls2) sl2" 
        unfolding move12_def validEtransO.simps 
      proof(intro allI, rule impI, elim conjE,unfold validTransV.simps isSecV_iff getSecV.simps fst_conv)
          fix ss1' ss2' sl1' sl2'

          assume v: "(cfg1, ibT1, ibUT1, ls1) →N ss1'" "(cfg2, ibT2, ibUT2, ls2) →N ss2'" and
               sec: "pcOf cfg1 ≠ 0 ∧ sl1 = sl1' ∨ pcOf cfg1 = 0 ∧ sl1 = stateOf cfg1 # sl1'"
                    "pcOf cfg2 ≠ 0 ∧ sl2 = sl2' ∨ pcOf cfg2 = 0 ∧ sl2 = stateOf cfg2 # sl2'"
          
          obtain cfg1' ibT1' ibUT1' ls1' where ss1': "ss1' = (cfg1', ibT1', ibUT1', ls1')"
            by (cases ss1', auto) 
          obtain cfg2' ibT2' ibUT2' ls2' where ss2': "ss2' = (cfg2', ibT2', ibUT2', ls2')"
            by (cases ss2', auto)

          obtain pc1' vs1' avst1' h1' p1' where 
            cfg1': "cfg1' = Config pc1' (State (Vstore vs1') avst1' h1' p1')"
            by (cases cfg1') (metis state.collapse vstore.collapse)
          obtain pc2' vs2' avst2' h2' p2' where 
            cfg2': "cfg2' = Config pc2' (State (Vstore vs2') avst2' h2' p2')"
            by (cases cfg2') (metis state.collapse vstore.collapse)
          note cfg = cfg cfg1' cfg2'

          obtain hh1' where h1': "h1' = Heap hh1'" by(cases h1', auto)
          obtain hh2' where h2': "h2' = Heap hh2'" by(cases h2', auto)
          note hh = hh h1' h2'

          note ss = ss1 ss2 ss1' ss2'
          have v':"(cfg1, ibT1, ibUT1) →B (cfg1', ibT1', ibUT1')" using v unfolding ss by simp
          then have v1:"nextB (cfg1, ibT1, ibUT1) = (cfg1', ibT1', ibUT1')" using stepB_nextB by auto

          have v'':"(cfg2, ibT2, ibUT2) →B (cfg2', ibT2', ibUT2')" using v unfolding ss by simp
          then have v2:"nextB (cfg2, ibT2, ibUT2) = (cfg2', ibT2', ibUT2')" using stepB_nextB by auto
          note valid = v' v1 v'' v2 

          have ls1':"ls1' = ls1 ∪ readLocs cfg1" using v unfolding ss by simp
          have ls2':"ls2' = ls2 ∪ readLocs cfg2" using v unfolding ss by simp
          note ls = ls1' ls2'


          note Γ_simps = cfg ls vs⇩i_defs hh array_loc_def 
                          array_base_def state_def PC_def

          show "Γ_inv ss1' sl1' ss2' sl2'" 
            using Γ valid getAct
            unfolding ss apply-apply(frule Γ_implies)
            using cases_5[of "pc1"] not6 apply(elim disjE, simp_all)
            unfolding Γ_def ss
            prefer 4 subgoal using vs_xx_cases[of cfg1]
            by (elim disjE, unfold Γ_defs, auto simp add: Γ_simps) 
            subgoal by (unfold Γ_defs, auto simp add: Γ_simps) 
            subgoal by (unfold Γ_defs, auto simp add: Γ_simps) 
            subgoal by (unfold Γ_defs, auto simp add: Γ_simps)
            subgoal using val_neq_1 apply (unfold Γ_defs, auto simp add: Γ_simps) 
              using val_neq_1 by (metis NN_suc add_left_cancel nat_int) 
            subgoal by (unfold Γ_defs, auto simp add: Γ_simps) 
            subgoal by (unfold Γ_defs, auto simp add: Γ_simps) .
        qed
      qed
    qed


theorem "¬rsecure"
  apply(rule unwindSD_rsecure[of s3⇩0 s3_trans s4⇩0 s4_trans Γ_inv]) 
  by simp_all

end