Theory Fun3

section "Proof of Relative Security for fun3"
theory Fun3
imports "../Instance_IMP/Instance_Secret_IMem" 
  "Relative_Security.Unwinding_fin"
begin 


subsection "Function definition and Boilerplate"
no_notation bot ("⊥")


consts NN::"nat"

lemma NN:"int NN ≥ 0" by auto
consts size_aa1 :: nat
consts size_aa2 :: nat
consts mispred :: "predState ⇒ pcounter list ⇒ bool"
consts update :: "predState ⇒ pcounter list ⇒ predState"
consts initPstate :: predState

definition aa1 :: "avname" where "aa1 = ''a1''" 
definition aa2 :: "avname" where "aa2 = ''a2''" 
definition vv :: "avname" where "vv = ''v''" 
definition xx :: "avname" where "xx = ''x''" 
definition tt :: "avname" where "tt = ''t''" 


lemmas vvars_defs = aa1_def aa2_def vv_def xx_def tt_def

lemma vvars_dff[simp]: 
"aa1 ≠ aa2" "aa1 ≠ vv" "aa1 ≠ xx" "aa1 ≠ tt"
"aa2 ≠ aa1" "aa2 ≠ vv" "aa2 ≠ xx" "aa2 ≠ tt"
"vv ≠ aa1" "vv ≠ aa2"  "vv ≠ xx" "vv ≠ tt"
"xx ≠ aa1" "xx ≠ aa2" "xx ≠ vv" "xx ≠ tt"
"tt ≠ aa1" "tt ≠ aa2" "tt ≠ vv" "tt ≠ xx"
unfolding vvars_defs by auto

(* The initial avstore contains two arrays named aa1 and aa2 located one after the other *)
fun initAvstore :: "avstore ⇒ bool" where
"initAvstore (Avstore as)  = (as aa1 = (0, size_aa1) ∧ as aa2 = (size_aa1, size_aa2))"
fun istate ::"state ⇒ bool" where
"istate s = (initAvstore (getAvstore s))"

definition "prog ≡ 
[
 ⌦‹0 › Start , 
 ⌦‹1 › Input U xx ,
 ⌦‹2 › tt ::= (N 0) ,
 ⌦‹3 › IfJump (Less (V xx) (N NN)) 4 7 ,
 ⌦‹4 ›   vv ::= VA aa1 (V xx) ,
 ⌦‹5 ›   Fence ,
 ⌦‹6 ›   tt ::= (VA aa2 (Times (V vv) (N 512))) ,
 ⌦‹7 › Output U (V tt)
]"

(* *)

lemma cases_7: "(i::pcounter) = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 ∨ i = 5 ∨ 
 i = 6 ∨ i = 7 ∨ i > 7"
apply(cases i, simp_all) 
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
subgoal for i apply(cases i, simp_all)
. . . . . . . .


lemma xx_NN_cases: "vs xx < int NN ∨ vs xx ≥ int NN" by auto

lemma is_If_pcOf[simp]: 
"pcOf cfg < 8 ⟹ is_IfJump (prog ! (pcOf cfg)) ⟷ pcOf cfg = 3"
apply(cases cfg) subgoal for pc s using cases_7[of "pcOf cfg "] 
by (auto simp: prog_def) .

lemma is_If_pc[simp]: 
"pc < 8 ⟹ is_IfJump (prog ! pc) ⟷ pc = 3"
using cases_7[of pc] 
by (auto simp: prog_def) 

lemma eq_Fence_pc[simp]: 
"pc < 8 ⟹ prog ! pc = Fence ⟷ pc = 5"
using cases_7[of pc] 
by (auto simp: prog_def) 


(* *)

fun resolve :: "predState ⇒ pcounter list ⇒ bool" where
  "resolve p pc = (if (pc = [4,7]) then True else False)"



(* *)
interpretation Prog_Mispred_Init where 
prog = prog and initPstate = initPstate and 
mispred = mispred and resolve = resolve and update = update and 
istate = istate
  by (standard, simp add: prog_def)
(* *)

(* Restoring the abbreviations: *)
abbreviation
  stepB_abbrev :: "config × val llist × val llist  ⇒ config × val llist × val llist ⇒ bool" (infix "→B" 55)
  where "x →B y == stepB x y"

abbreviation
  stepsB_abbrev :: "config × val llist × val llist ⇒ config × val llist × val llist ⇒ bool" (infix "→B*" 55)
  where "x →B* y == star stepB x y"

abbreviation
  stepM_abbrev :: "config × val llist × val llist ⇒ config × val llist × val llist ⇒ bool" (infix "→M" 55)
  where "x →M y == stepM x y"

abbreviation
  stepN_abbrev :: "config × val llist × val llist × loc set ⇒ config × val llist × val llist × loc set ⇒ bool" (infix "→N" 55)
  where "x →N y == stepN x y"

abbreviation
  stepsN_abbrev :: "config × val llist × val llist × loc set ⇒ config × val llist × val llist × loc set ⇒ bool" (infix "→N*" 55)
  where "x →N* y == star stepN x y"

abbreviation
  stepS_abbrev :: "configS ⇒ configS ⇒ bool" (infix "→S" 55)
  where "x →S y == stepS x y"

abbreviation
  stepsS_abbrev :: "configS ⇒ configS ⇒ bool" (infix "→S*" 55)
  where "x →S* y == star stepS x y"

(* *)

lemma endPC[simp]: "endPC = 8"
unfolding endPC_def unfolding prog_def by auto

(* *)

lemma is_getTrustedInput_pcOf[simp]: "pcOf cfg < 8 ⟹ is_getInput (prog!(pcOf cfg)) ⟷ pcOf cfg = 1"
using cases_7[of "pcOf cfg"] by (auto simp: prog_def)
lemma getUntrustedInput_pcOf[simp]: "prog!1 = Input U xx"
  by (auto simp: prog_def)

lemma getInput_not3[simp]: "¬is_getInput (prog ! 3)"
  by (auto simp: prog_def)

lemma getInput_not4[simp]: "¬is_getInput (prog ! 4)"
  by (auto simp: prog_def)
lemma Output_not4[simp]: "¬is_Output (prog ! 4)"
  by (auto simp: prog_def)

lemma is_Output_pcOf[simp]: "pcOf cfg < 8 ⟹ is_Output (prog!(pcOf cfg)) ⟷ pcOf cfg = 7"
using cases_7[of "pcOf cfg"] by (auto simp: prog_def)

lemma is_Output: "is_Output (prog ! 7)"
  unfolding is_Output_def prog_def by auto

lemma is_Fence[simp]: "(prog ! 5) = Fence"
unfolding prog_def by auto


lemma not_is_getTrustedInput[simp]:"cfg = Config 3 (State (Vstore vs) (Avstore as) (Heap h) p) ⟹ ¬ is_getInput (prog ! pcOf cfg)"
  unfolding is_getInput_def prog_def by simp


lemma not_is_Output[simp]:"cfg = Config pc (State (Vstore vs) (Avstore as) (Heap h) p) ⟹
        pc = 3 ⟹ ¬ is_Output (prog ! pcOf cfg)"
  unfolding is_Output prog_def by simp
(* *)

lemma isSecV_pcOf[simp]: 
"isSecV (cfg,ibT,ibUT) ⟷ pcOf cfg = 0"
using isSecV_def by simp

lemma isSecO_pcOf[simp]: 
"isSecO (pstate,cfg,cfgs,ibT,ibUT,ls) ⟷ (pcOf cfg = 0 ∧ cfgs = [])"
using isSecO_def by simp

(* *)

lemma getInputT_not[simp]: "pcOf cfg < 8 ⟹ 
(prog ! pcOf cfg) ≠ Input T inp"
apply(cases cfg) subgoal for pc s using cases_7[of "pcOf cfg "] 
by (auto simp: prog_def) .

lemma getActV_pcOf[simp]: 
"pcOf cfg < 8 ⟹ 
 getActV (cfg,ibT,ibUT,ls) = 
 (if pcOf cfg = 1 then lhd ibUT else ⊥)"
apply(subst getActV_simps) unfolding prog_def 
  apply simp  
  using cases_7[of "pcOf cfg"] apply(elim disjE)
  using getActV_simps not_is_getTrustedInput_getActV by auto
  
lemma getObsV_pcOf[simp]: 
"pcOf cfg < 8 ⟹  
 getObsV (cfg,ibT,ibUT,ls) = 
 (if pcOf cfg = 7 then 
  (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)
  else ⊥ 
 )"
apply(subst getObsV_simps) 
  unfolding prog_def apply simp
  using getObsV_simps not_is_Output_getObsV is_Output_pcOf prog_def by presburger

lemma getActO_pcOf[simp]: 
"pcOf cfg < 8 ⟹ 
 getActO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (if pcOf cfg = 1 ∧ cfgs = [] then lhd ibUT else ⊥)"
apply(subst getActO_simps)
apply(cases cfgs, auto)
  unfolding prog_def apply simp 
  using getActV_simps getActV_pcOf prog_def by presburger

lemma getObsO_pcOf[simp]: 
"pcOf cfg < 8 ⟹  
 getObsO (pstate,cfg,cfgs,ibT,ibUT,ls) = 
 (if (pcOf cfg = 7 ∧ cfgs = []) then 
  (outOf (prog!(pcOf cfg)) (stateOf cfg), ls)
  else ⊥ 
 )"
apply(subst getObsO_simps) 
apply(cases cfgs, auto)
unfolding prog_def apply simp
using getObsV_simps is_Output_pcOf not_is_Output_getObsV prog_def by presburger 

(* *)
(* *) 

lemma eqSec_pcOf[simp]: 
"eqSec (cfg1, ibT,ibUT1, ls1) (pstate3, cfg3, cfgs3, ibT,ibUT3, ls3) ⟷ 
 (pcOf cfg1 = 0 ⟷ pcOf cfg3 = 0 ∧ cfgs3 = []) ∧ 
 (pcOf cfg1 = 0 ⟶ stateOf cfg1 = stateOf cfg3)"
unfolding eqSec_def by simp


(* nextB, nextM and readLocs behavior 
(for nextM we are only interested at branching points, here only program counter 4): *)

lemma nextB_pc0[simp]: 
"nextB (Config 0 s, ibT,ibUT) = 
 (Config 1 s, ibT,ibUT)"
apply(subst nextB_Start_Skip_Fence)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc0[simp]: 
"readLocs (Config 0 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc1[simp]: 
"ibUT ≠ LNil ⟹ nextB (Config 1 (State (Vstore vs) avst h p), ibT,ibUT) = 
 (Config 2 (State (Vstore (vs(xx := lhd ibUT))) avst h p), ibT, ltl ibUT)"
apply(subst nextB_getUntrustedInput')
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc1[simp]: 
"readLocs (Config 1 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

lemma nextB_pc1'[simp]: 
"ibUT ≠ LNil ⟹ nextB (Config (Suc 0) (State (Vstore vs) avst h p), ibT,ibUT) = 
 (Config 2 (State (Vstore (vs(xx := lhd ibUT))) avst h p), ibT, ltl ibUT)"
apply(subst nextB_getUntrustedInput')
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc1'[simp]: 
"readLocs (Config (Suc 0) s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc2[simp]:
"nextB (Config 2 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 3 (State (Vstore (vs(tt := 0))) avst h p), ibT, ibUT)"
apply(subst nextB_Assign)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc2[simp]: 
"readLocs (Config 2 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc3_then[simp]: 
"vs xx < int NN ⟹
 nextB (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 4 (State (Vstore vs) avst h p), ibT, ibUT)"
apply(subst nextB_IfTrue)
unfolding endPC_def unfolding prog_def by auto

lemma nextB_pc3_else[simp]: 
"vs xx ≥ int NN ⟹
 nextB (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 7 (State (Vstore vs) avst h p), ibT, ibUT)"
apply(subst nextB_IfFalse)
unfolding endPC_def unfolding prog_def by auto

lemma nextB_pc3: 
"nextB (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config (if vs xx < NN then 4 else 7) (State (Vstore vs) avst h p), ibT, ibUT)"
  by(cases "vs xx < NN", auto)

lemma nextM_pc3_then[simp]: 
"vs xx ≥ int NN ⟹
 nextM (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 4 (State (Vstore vs) avst h p), ibT, ibUT)"
apply(subst nextM_IfTrue)
unfolding endPC_def unfolding prog_def by auto

lemma nextM_pc3_else[simp]: 
"vs xx < int NN ⟹
 nextM (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config 7 (State (Vstore vs) avst h p), ibT, ibUT)"
apply(subst nextM_IfFalse)
unfolding endPC_def unfolding prog_def by auto

lemma nextM_pc3: 
"nextM (Config 3 (State (Vstore vs) avst h p), ibT, ibUT) = 
 (Config (if vs xx < NN then 7 else 4) (State (Vstore vs) avst h p), ibT, ibUT)"
by(cases "vs xx < NN", auto)

lemma readLocs_pc3[simp]: 
"readLocs (Config 3 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto


(* *)

lemma nextB_pc4[simp]: 
"nextB (Config 4 (State (Vstore vs) avst (Heap h) p), ibT,ibUT) = 
 (let l = array_loc aa1 (nat (vs xx)) avst 
  in (Config 5 (State (Vstore (vs(vv := h l))) avst (Heap h) p)), ibT,ibUT)"
apply(subst nextB_Assign)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc4[simp]: 
"readLocs (Config 4 (State (Vstore vs) avst h p)) = {array_loc aa1 (nat (vs xx)) avst}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc5[simp]: 
"nextB (Config 5 s, ibT,ibUT) = (Config 6 s, ibT,ibUT)"
apply(subst nextB_Start_Skip_Fence)
unfolding endPC_def unfolding prog_def by auto

lemma readLocs_pc5[simp]: 
"readLocs (Config 5 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc6[simp]:
"nextB (Config 6 (State (Vstore vs) avst (Heap h) p), ibT,ibUT) =  
  (let l = array_loc aa2 (nat (vs vv * 512)) avst
  in (Config 7 (State (Vstore (vs(tt := h l))) avst (Heap h) p)), ibT,ibUT)"
apply(subst nextB_Assign)
unfolding endPC_def unfolding prog_def by auto


lemma readLocs_pc6[simp]: 
"readLocs (Config 6 (State (Vstore vs) avst h p)) = {array_loc aa2 (nat (vs vv * 512)) avst}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_pc7[simp]:
"nextB (Config 7 s, ibT,ibUT) = (Config 8 s, ibT,ibUT)"
apply(subst nextB_Output)
unfolding endPC_def unfolding prog_def by auto 

lemma readLocs_pc7[simp]: 
"readLocs (Config 7 s) = {}"
unfolding endPC_def readLocs_def unfolding prog_def by auto

(* *)

lemma nextB_stepB_pc: 
"pc < 8 ⟹ (pc = 1 ⟶ ibUT ≠ LNil) ⟹ 
(Config pc s, ibT,ibUT) →B nextB (Config pc s, ibT,ibUT)"
apply(cases s) subgoal for vst avst hh p apply(cases vst, cases avst, cases hh)
subgoal for vs as h
using cases_7[of pc] apply safe
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def)
  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def, metis llist.collapse)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def)
  (* *)
  subgoal apply(cases "vs xx < NN")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) .
  subgoal apply(cases "vs xx < NN")  
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) 
    subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
    by (simp add: prog_def) .
  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  (* *)
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal apply simp apply(subst stepB.simps) unfolding endPC_def 
  by (simp add: prog_def) 
  subgoal by auto          
  subgoal by auto 
  . . .

lemma not_finalB: 
"pc < 8 ⟹ (pc = 1 ⟶ ibUT ≠ LNil) ⟹ 
 ¬ finalB (Config pc s, ibT,ibUT)"
using nextB_stepB_pc by (simp add: stepB_iff_nextB)

lemma finalB_pc_iff': 
"pc < 8 ⟹
 finalB (Config pc s, ibT,ibUT) ⟷ 
 (pc = 1 ∧ ibUT = LNil)"
  subgoal apply safe
    subgoal using nextB_stepB_pc[of pc] by (auto simp add: stepB_iff_nextB) 
    subgoal using nextB_stepB_pc[of pc] by (auto simp add: stepB_iff_nextB) 
    subgoal using finalB_iff getUntrustedInput_pcOf by auto . .

lemma finalB_pc_iff: 
"pc ≤ 8 ⟹
 finalB (Config pc s, ibT,ibUT) ⟷ 
 (pc = 1 ∧ ibUT = LNil ∨ pc = 8)"
  using cases_7[of pc] apply (elim disjE, simp add: finalB_def)
  subgoal by (meson final_def stebB_0)
  by (simp add: finalB_pc_iff' finalB_endPC)+

lemma finalB_pcOf_iff[simp]:
"pcOf cfg ≤ 8 ⟹ 
 finalB (cfg, ibT,ibUT) ⟷ (pcOf cfg = 1 ∧ ibUT = LNil ∨ pcOf cfg = 8)"
by (metis config.collapse finalB_pc_iff) 




lemma finalS_cond:"pcOf cfg < 8 ⟹ cfgs = [] ⟹ (pcOf cfg = 1 ⟶ ibUT ≠ LNil) ⟹ ¬ finalS (pstate, cfg, cfgs, ibT,ibUT, ls)"
apply(rule notI, cases cfg)
subgoal for pc s apply(cases s)
subgoal for vst avst hh p apply(cases vst, cases avst, cases hh)
  subgoal for vs as h
    using cases_7[of pc] apply(elim disjE) unfolding finalS_defs
    subgoal by(erule allE[of _ "(pstate, Config 1 (State (Vstore vs) avst hh p), [], ibT,ibUT, ls)"], erule notE, rule nonspec_normal, auto)

      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                                    pstate pstate ibT ibUT 
                                    "Config 2 (State (Vstore (vs(xx:= lhd ibUT))) avst hh p)" 
                                    ibT "ltl ibUT" "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
              prefer 7 subgoal by metis by simp_all
      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)" 
                                    pstate pstate ibT ibUT 
                                    "Config 3 (State (Vstore (vs(tt:= 0))) avst hh p)" 
                                    ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
              prefer 7 subgoal by metis by simp_all

    subgoal apply(cases "mispred pstate [3]")
      subgoal by(erule allE[of _ "(update pstate [pcOf (Config pc (State (Vstore vs) avst hh p))], 
                                   Config (if vs xx < NN then 4 else 7) (State (Vstore vs) avst hh p), 
                                  [Config (if vs xx < NN then 7 else 4) (State (Vstore vs) avst hh p)], 
                                   ibT,ibUT, ls)"], erule notE, rule nonspec_mispred, auto simp: finalM_iff)

      subgoal apply(frule nonspec_normal[of cfgs "Config pc (State (Vstore vs) avst hh p)"
                                    pstate pstate ibT ibUT 
                                    "Config (if vs xx < NN then 4 else 7) (State (Vstore vs) avst hh p)" 
                                    ibT ibUT "[]" "ls ∪ readLocs (Config pc (State (Vstore vs) avst hh p))" ls])
              prefer 7 subgoal by metis apply simp_all by (simp add: nextB_pc3) .

    subgoal by(erule allE[of _ "(pstate, Config 5 (State (Vstore (vs(vv := h (array_loc aa1 (nat (vs xx)) avst)))) avst hh p), 
                                                                [], ibT,ibUT, ls ∪ {array_loc aa1 (nat (vs xx)) avst})"],
               erule notE, rule nonspec_normal, auto)

    subgoal by(erule allE[of _ "(pstate, Config 6 (State (Vstore vs) avst hh p), [], ibT,ibUT, ls)"], erule notE, rule nonspec_normal, auto)

    subgoal by(erule allE[of _ "(pstate, Config 7 (State (Vstore (vs(tt := h (array_loc aa2 (nat (vs vv * 512)) (Avstore as))))) avst hh p), 
                                 [], ibT,ibUT, ls ∪ {array_loc aa2 (nat (vs vv * 512)) (Avstore as)})"],
              erule notE, rule nonspec_normal, auto)

    subgoal by(erule allE[of _ "(pstate, Config 8 (State (Vstore vs) avst hh p), [], ibT,ibUT, ls)"], erule notE, rule nonspec_normal, auto)

    by simp_all . . .



lemma finalS_cond_spec:
      "pcOf cfg < 8 ⟹ 
       (((pcOf (last cfgs) = 4 ∨ pcOf (last cfgs) = 5) ∧ pcOf cfg = 7) ∨ 
        (pcOf (last cfgs) = 7 ∧ pcOf cfg = 4)) ⟹ 
       length cfgs = Suc 0 ⟹
      ¬ finalS (pstate, cfg, cfgs, ibT,ibUT, ls)"
using not_is_getTrustedInput not_is_Output
  apply(cases cfg)
  subgoal for pc s apply(cases s)
  subgoal for vst avst hh p apply(cases vst, cases avst, cases hh)
  subgoal for vs as h apply(cases "last cfgs")
  subgoal for pcs ss apply(cases ss)
  subgoal for vsts avsts hhs ps apply(cases vsts, cases avsts, cases hhs, simp)
    subgoal for vss ass hs apply(elim disjE, elim conjE, elim disjE, simp) 
      unfolding finalS_defs 
      subgoal apply(rule notI, 
      erule allE[of _ "(pstate,Config 7 (State (Vstore vs) (Avstore as) (Heap h) p),
                        [Config 5 (State (Vstore (vss(vv := hs (array_loc aa1 (nat (vss xx)) avsts)))) avsts hhs ps)],
                        ibT,ibUT,ls ∪ readLocs (last cfgs))"])
        by(erule notE, 
        rule spec_normal[of _ _ _ _ _ _"Config 5 (State (Vstore (vss(vv := hs (array_loc aa1 (nat (vss xx)) avsts)))) avsts hhs ps)"], auto)
      
      subgoal apply(rule notI, 
      erule allE[of _ "(pstate,Config 7 (State (Vstore vs) (Avstore as) (Heap h) p),[],ibT,ibUT,ls)"])
        apply(erule notE) by(rule spec_Fence, auto)

      subgoal apply(rule notI, 
      erule allE[of _ "(update pstate (4 # map pcOf cfgs),Config 4 (State (Vstore vs) (Avstore as) (Heap h) p),
                       [],ibT,ibUT,ls)"])
        by(erule notE, rule spec_resolve, auto)
      . . . . . . . 
end