Theory Fun3_secure

subsection "Proof"
theory Fun3_secure
imports Fun3
begin 

type_synonym stateO = configS
type_synonym stateV = "config × val llist × val llist × loc set"
(* THE PROOF OF SECURITY *)
definition "PC ≡ {0..7}"

(* we read "before" as "before or at" *)
definition "beforeInput = {0,1}"
definition "afterInput = {2,3,4,5,6,7}"
definition "startOfThenBranch = 4"
definition "inThenBranchBeforeFence = {4,5}"
definition "elseBranch = 7"
definition "beforeFence = {2..4}" 
definition "beforeAssign_vv = {0..4}"

(* Common to all the unwinding relations in this proof: *)
definition common :: "stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" 
where 
"common = (λ
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO. 
(pstate3 = pstate4 ∧ 
 cfg1 = cfg3 ∧ cfg2 = cfg4 ∧ 
 pcOf cfg3 = pcOf cfg4 ∧ map pcOf cfgs3 = map pcOf cfgs4 ∧ 
 pcOf cfg3 ∈ PC ∧ pcOf ` (set cfgs3) ⊆ PC ∧
 ⌦‹   ›
 array_base aa1 (getAvstore (stateOf cfg3)) = array_base aa1 (getAvstore (stateOf cfg4)) ∧ 
 (∀cfg3'∈set cfgs3. array_base aa1 (getAvstore (stateOf cfg3')) = array_base aa1 (getAvstore (stateOf cfg3))) ∧ 
 (∀cfg4'∈set cfgs4. array_base aa1 (getAvstore (stateOf cfg4')) = array_base aa1 (getAvstore (stateOf cfg4))) ∧ 
 array_base aa2 (getAvstore (stateOf cfg3)) = array_base aa2 (getAvstore (stateOf cfg4)) ∧ 
 (∀cfg3'∈set cfgs3. array_base aa2 (getAvstore (stateOf cfg3')) = array_base aa2 (getAvstore (stateOf cfg3))) ∧ 
 (∀cfg4'∈set cfgs4. array_base aa2 (getAvstore (stateOf cfg4')) = array_base aa2 (getAvstore (stateOf cfg4))) ∧ 
 ⌦‹   ›
 (statA = Diff ⟶ statO = Diff)))"


lemma common_implies: "common    
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO ⟹ 
 pcOf cfg1 < 9 ∧ pcOf cfg2 = pcOf cfg1"
unfolding common_def PC_def by (auto simp: image_def subset_eq)


(* Before input is inserted *)
definition Δ0 :: "enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ0 = (λnum 
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
     statO.
 (common    (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
     statO  ∧ 
  ibUT1 = ibUT3 ∧ ibUT2 = ibUT4 ∧   
  (pcOf cfg3 > 1 ⟶ same_var_o xx cfg3 cfgs3 cfg4 cfgs4) ∧ 
  (pcOf cfg3 < 2 ⟶ ibUT1≠LNil ∧ ibUT2≠LNil ∧ ibUT3≠LNil ∧ ibUT4≠LNil) ∧
  pcOf cfg3 ∈ beforeInput ∧ 
  ls1 = ls3 ∧ ls2 = ls4 ∧ 
  noMisSpec cfgs3 
 ))"

lemmas Δ0_defs = Δ0_def common_def PC_def beforeInput_def noMisSpec_def same_var_o_def

lemma Δ0_implies: "Δ0 num 
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO ⟹ 
   (pcOf cfg3 = 1 ⟶ ibUT3 ≠ LNil) ∧
   (pcOf cfg4 = 1 ⟶ ibUT4 ≠ LNil) ∧
   pcOf cfg1 < 8 ∧ pcOf cfg2 = pcOf cfg1 ∧ 
   cfgs3 = [] ∧ pcOf cfg3 < 8 ∧
   cfgs4 = [] ∧ pcOf cfg4 < 8"
  unfolding Δ0_defs 
  apply(intro conjI)
  apply simp_all 
  by (metis map_is_Nil_conv)

(* After input is inserted, no mis-speculation *)
definition Δ1 :: "enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ1 = (λnum 
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
     statO.
 (common    
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
     statO ∧ 
  pcOf cfg3 ∈ afterInput ∧ 
  same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
  ls1 = ls3 ∧ ls2 = ls4 ∧ 
  noMisSpec cfgs3 
 ))"

lemmas Δ1_defs = Δ1_def common_def PC_def afterInput_def same_var_o_def noMisSpec_def

lemma Δ1_implies: "Δ1 num
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2)
   statO ⟹ 
   pcOf cfg1 < 8 ∧
   cfgs3 = [] ∧ pcOf cfg3 ≠ 1 ∧ pcOf cfg3 < 8 ∧
   cfgs4 = [] ∧ pcOf cfg4 ≠ 1 ∧ pcOf cfg4 < 8"
  unfolding Δ1_defs 
  apply(intro conjI) apply simp_all
  using One_nat_def verit_eq_simplify(10,12) apply linarith
  apply (metis list.map_disc_iff)
  by linarith


(* Left mis-speculation: *)
definition Δ2 :: "enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ2 = (λnum
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2)  
     statO.
 (common    
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2)  
     statO ∧ 
  pcOf cfg3 = startOfThenBranch ∧ 
  pcOf (last cfgs3) = elseBranch ∧ 
  same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
  ls1 = ls3 ∧ ls2 = ls4 ∧
  misSpecL1 cfgs3
 ))"

lemmas Δ2_defs = Δ2_def common_def PC_def same_var_def startOfThenBranch_def  
      misSpecL1_def elseBranch_def

lemma Δ2_implies: "Δ2 num    
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO ⟹ 
   pcOf (last cfgs3) = 7 ∧ pcOf cfg3 = 4 ∧ 
   pcOf (last cfgs4) = pcOf (last cfgs3) ∧
   pcOf cfg3 = pcOf cfg4 ∧
   length cfgs3 = Suc 0 ∧
   length cfgs3 = length cfgs4"
  apply(intro conjI)
  unfolding Δ2_defs apply simp_all
  apply (simp add: image_subset_iff) 
  apply (metis last_map map_is_Nil_conv)
  by (metis length_map)

(* Right mis-speculation: *)
definition Δ3 :: "enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ3 = (λnum 
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
     statO.
 (common (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2)  
     statO ∧ 
  pcOf cfg3 = elseBranch ∧ 
  pcOf (last cfgs3) ∈ inThenBranchBeforeFence ∧
  same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧ 
  Language_Prelims.dist ls3 ls4 ⊆ Language_Prelims.dist ls1 ls2 ∧
  (pcOf (last cfgs3) = 4 ⟶ ls1 = ls3 ∧ ls2 = ls4) ∧ 
  misSpecL1 cfgs3 
 ))"

lemmas Δ3_defs = Δ3_def common_def PC_def inThenBranchBeforeFence_def
           beforeAssign_vv_def misSpecL1_def elseBranch_def 
           same_var_o_def

lemma Δ3_implies: "Δ3 num
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO ⟹ 
   (pcOf (last cfgs3) = 4 ∨ pcOf (last cfgs3) = 5) ∧ pcOf cfg3 = 7 ∧ 
   pcOf (last cfgs4) = pcOf (last cfgs3) ∧
   pcOf cfg3 = pcOf cfg4 ∧
   array_base aa1 (getAvstore (stateOf (last cfgs3))) = array_base aa1 (getAvstore (stateOf cfg3)) ∧ 
   array_base aa1 (getAvstore (stateOf (last cfgs4))) = array_base aa1 (getAvstore (stateOf cfg4)) ∧
   length cfgs3 = Suc 0 ∧
   length cfgs3 = length cfgs4 ∧
   vstore (getVstore (stateOf (last cfgs3))) xx = vstore (getVstore (stateOf (last cfgs4))) xx"
apply(intro conjI)
  unfolding Δ3_defs apply simp_all
  apply (simp add: image_subset_iff) 
  apply (metis last_map map_is_Nil_conv)
  apply (metis last_in_set list.size(3) n_not_Suc_n)
  apply (metis One_nat_def last_in_set length_0_conv length_map zero_neq_one)
  apply (metis length_map)
  by (metis last_in_set list.map_disc_iff)


(* *)

definition Δ1' :: "enat ⇒ stateO ⇒ stateO ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ1' = (λnum 
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
     statO.
 (common    
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
     statO ∧ 
  pcOf cfg3 = elseBranch ∧ 
  same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
  Language_Prelims.dist ls3 ls4 ⊆ Language_Prelims.dist ls1 ls2 ∧
  noMisSpec cfgs3 
 ))"

lemmas Δ1'_defs = Δ1'_def common_def PC_def afterInput_def same_var_o_def noMisSpec_def
elseBranch_def

lemma Δ1'_implies: "Δ1' num
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2)
   statO ⟹ 
   pcOf cfg1 < 8 ∧
   cfgs3 = [] ∧ pcOf cfg3 ≠ 1 ∧ pcOf cfg3 < 8 ∧
   cfgs4 = [] ∧ pcOf cfg4 ≠ 1 ∧ pcOf cfg4 < 8"
  unfolding Δ1'_defs 
  apply(intro conjI) apply simp_all 
  by (metis list.map_disc_iff)


(* End: *)
definition Δ4 :: "enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ4 = (λnum 
   (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2)  
    statO.
   (pcOf cfg3 = endPC ∧ pcOf cfg4 = endPC ∧ cfgs3 = [] ∧ cfgs4 = [] ∧
    pcOf cfg1 = endPC ∧ pcOf cfg2 = endPC))"

lemmas Δ4_defs = Δ4_def common_def endPC_def  

(* *)

lemma init: "initCond Δ0" 
  unfolding initCond_def apply(intro allI) 
  subgoal for s3 s4 apply(cases s3, cases s4) 
  subgoal for pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 
    apply clarify 
    apply(rule exI[of _ "(cfg3, ibT3, ibUT3, ls3)"])
    apply(cases "getAvstore (stateOf cfg3)")
    apply(rule exI[of _ "(cfg4, ibT4, ibUT4, ls4)"])
    apply(cases "getAvstore (stateOf cfg4)")
  unfolding Δ0_defs array_base_def by auto  . .

(* *)
 lemma step0: "unwindIntoCond Δ0 (oor Δ0 Δ1)"
proof(rule unwindIntoCond_simpleI)  
  fix n ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ0: "Δ0 n ss3 ss4 statA ss1 ss2 statO"

  obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
  by (cases ss3, auto) 
  obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
  by (cases ss4, auto)
  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 = ss3 ss4 ss1 ss2 


  obtain pc3 vs3 avst3 h3 p3 where 
  cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
  by (cases cfg3) (metis state.collapse vstore.collapse)
  obtain pc4 vs4 avst4 h4 p4 where 
  cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
  by (cases cfg4) (metis state.collapse vstore.collapse)
  note cfg = cfg3 cfg4

  obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
  obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
  note hh = h3 h4

  have f1:"¬finalN ss1" 
    using Δ0 finalB_pc_iff' unfolding ss finalN_iff_finalB Δ0_defs
    by simp 

  have f2:"¬finalN ss2" 
    using Δ0 finalB_pc_iff' unfolding ss finalN_iff_finalB Δ0_defs
    by simp 

  have f3:"¬finalS ss3" 
    using Δ0 unfolding ss apply-apply(frule Δ0_implies)
    using finalS_cond by simp

  have f4:"¬finalS ss4" 
    using Δ0 unfolding ss apply-apply(frule Δ0_implies)
    using finalS_cond by simp


  note finals = f1 f2 f3 f4
  show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
    using finals by auto

  then show "isIntO ss3 = isIntO ss4" by simp


  show "match (oor Δ0 Δ1) ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposibT, ibUTle case since isIntO always holds *)
    show "match1 (oor Δ0 Δ1) ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_defs)
    show "match2 (oor Δ0 Δ1) ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_defs)
    show "match12 (oor Δ0 Δ1) ss3 ss4 statA ss1 ss2 statO"
    (* Choose the match12_12 case (since we have no mis-speculation yet) *)
    proof(rule match12_simpleI, rule disjI2, intro conjI)
      fix ss3' ss4' statA'
      assume statA': "statA' = sstatA' statA ss3 ss4"
      and v: "validTransO (ss3, ss3')" "validTransO (ss4, ss4')" 
      and sa: "Opt.eqAct ss3 ss4"
      note v3 = v(1) note v4 = v(2)
 
      obtain pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' where ss3': "ss3' = (pstate3', cfg3', cfgs3', ibT3', ibUT3', ls3')"
      by (cases ss3', auto) 
      obtain pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' where ss4': "ss4' = (pstate4', cfg4', cfgs4', ibT4', ibUT4', ls4')"
      by (cases ss4', auto)
      note ss = ss ss3' ss4'

      obtain pc3 vs3 avst3 h3 p3 where 
      cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
      by (cases cfg3) (metis state.collapse vstore.collapse)
      obtain pc4 vs4 avst4 h4 p4 where 
      cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
      by (cases cfg4) (metis state.collapse vstore.collapse)
      note cfg = cfg3 cfg4
 
      show "eqSec ss1 ss3"
      using v sa Δ0 unfolding ss 
      by (simp add: Δ0_defs eqSec_def)

      show "eqSec ss2 ss4"
      using v sa Δ0 unfolding ss 
      apply (simp add: Δ0_defs eqSec_def) 
      by (metis length_0_conv length_map) 

      show "Van.eqAct ss1 ss2"
      using v sa Δ0 unfolding ss   
      unfolding Opt.eqAct_def Van.eqAct_def
      apply(simp_all add: Δ0_defs)  
      by (metis f3 map_is_Nil_conv ss3)

      show "match12_12 (oor Δ0 Δ1) ss3' ss4' statA' ss1 ss2 statO"
      unfolding match12_12_def
      proof(rule exI[of _ "nextN ss1"], rule exI[of _ "nextN ss2"],unfold Let_def, intro conjI impI)
        show "validTransV (ss1, nextN ss1)" 
          by (simp add: f1 nextN_stepN)

        show "validTransV (ss2, nextN ss2)" 
          by (simp add: f2 nextN_stepN)

        {assume sstat: "statA' = Diff"
         show "sstatO' statO ss1 ss2 = Diff"
         using v sa Δ0 sstat unfolding ss cfg statA' apply simp
         apply(simp add: Δ0_defs sstatO'_def sstatA'_def finalS_def final_def) 
         using cases_7[of pc3] apply(elim disjE)
         apply simp_all apply(cases statO, simp_all) apply(cases statA, simp_all)
         apply(cases statO, simp_all) apply (cases statA, simp_all)
         by (smt (z3) status.distinct status.exhaust updStat.simps)+
        } note stat = this

        show "oor Δ0 Δ1 ∞ ss3' ss4' statA' (nextN ss1) (nextN ss2) (sstatO' statO ss1 ss2)"
        (* the cmbination of nonspec_normal and nonspec_normal is the only nontrivial possibT, ibUTility, deferred to the end *)
          using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
            case spec_normal
            then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
          next
            case spec_mispred
            then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
          next
            case spec_Fence
            then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
          next
            case spec_resolve
            then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
          next
            case nonspec_mispred 
            then show ?thesis using sa Δ0 stat unfolding ss apply (simp add: Δ0_defs) 
              by (metis is_If_pc less_Suc_eq nat_less_le numeral_1_eq_Suc_0 numeral_3_eq_3 
                  one_eq_numeral_iff semiring_norm(83) zero_less_numeral zero_neq_numeral)  
        next
          case nonspec_normal note nn3 = nonspec_normal
          show ?thesis 
          using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
            case nonspec_mispred
            then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
          next
            case spec_normal
            then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
          next
            case spec_mispred
            then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
          next
            case spec_Fence
            then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
          next
            case spec_resolve
            then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
          next
            case nonspec_normal note nn4=nonspec_normal
            show ?thesis  using sa stat Δ0 v3 v4 nn3 nn4 f4 unfolding ss cfg hh Opt.eqAct_def
            apply clarsimp
            using cases_7[of pc3] apply(elim disjE)
            subgoal apply(rule oorI1) by (simp add: Δ0_defs)
            subgoal apply(rule oorI2) apply (simp add: Δ0_defs,auto) 
              unfolding Δ1_defs 
              subgoal by (simp add: Δ0_defs) 
              subgoal by (simp add: Δ0_defs) .  
            by (simp add: Δ0_defs)+ 
          qed
        qed
      qed
    qed  
  qed
qed
(**)
lemma step1: "unwindIntoCond Δ1 (oor4 Δ1 Δ2 Δ3 Δ4)" 
proof(rule unwindIntoCond_simpleI) 
  fix n ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ1: "Δ1 n ss3 ss4 statA ss1 ss2 statO"

  obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
  by (cases ss3, auto) 
  obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
  by (cases ss4, auto)
  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 = ss3 ss4 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) 
  obtain pc3 vs3 avst3 h3 p3 where 
  cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
  by (cases cfg3) (metis state.collapse vstore.collapse)
  obtain pc4 vs4 avst4 h4 p4 where 
  cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
  by (cases cfg4) (metis state.collapse vstore.collapse)
  note cfg = cfg1 cfg2 cfg3 cfg4

  obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
  obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
  note hh = h3 h4

  have f1:"¬finalN ss1" 
    using Δ1 finalB_pc_iff' unfolding ss cfg finalN_iff_finalB Δ1_defs
    by simp linarith

  have f2:"¬finalN ss2" 
    using Δ1 finalB_pc_iff' unfolding ss cfg finalN_iff_finalB Δ1_defs
    by simp linarith


  have f3:"¬finalS ss3" 
    using Δ1 unfolding ss apply-apply(frule Δ1_implies)
    using finalS_cond by simp

  have f4:"¬finalS ss4" 
    using Δ1 unfolding ss apply-apply(frule Δ1_implies)
    using finalS_cond by simp

  note finals = f1 f2 f3 f4

  show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
    using finals by auto

  then show "isIntO ss3 = isIntO ss4" by simp

  show "match (oor4 Δ1 Δ2 Δ3 Δ4) ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposibT, ibUTle case since isIntO always holds *)
    show "match1 (oor4 Δ1 Δ2 Δ3 Δ4) ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 (oor4 Δ1 Δ2 Δ3 Δ4) ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 (oor4 Δ1 Δ2 Δ3 Δ4) ss3 ss4 statA ss1 ss2 statO"
    (* Choose the match12_12 case (since we have no mis-speculation yet) *)
    proof(rule match12_simpleI, rule disjI2, intro conjI)
      fix ss3' ss4' statA'
      assume statA': "statA' = sstatA' statA ss3 ss4"
      and v: "validTransO (ss3, ss3')" "validTransO (ss4, ss4')" 
      and sa: "Opt.eqAct ss3 ss4"
      note v3 = v(1) note v4 = v(2)

      obtain pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' where ss3': "ss3' = (pstate3', cfg3', cfgs3', ibT3', ibUT3', ls3')"
      by (cases ss3', auto) 
      obtain pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' where ss4': "ss4' = (pstate4', cfg4', cfgs4', ibT4', ibUT4', ls4')"
      by (cases ss4', auto)
      note ss = ss ss3' ss4'

      show "eqSec ss1 ss3"
      using v sa Δ1 unfolding ss
      by (simp add: Δ1_defs eqSec_def)

      show "eqSec ss2 ss4"
      using v sa Δ1 unfolding ss 
      apply (simp add: Δ1_defs eqSec_def) 
      by (metis length_0_conv length_map)
      
      show "Van.eqAct ss1 ss2"
      using v sa Δ1 unfolding ss Van.eqAct_def
      apply (simp_all add: Δ1_defs)  
      by linarith

      show "match12_12 (oor4 Δ1 Δ2 Δ3 Δ4) ss3' ss4' statA' ss1 ss2 statO"
      unfolding match12_12_def
      proof(rule exI[of _ "nextN ss1"], rule exI[of _ "nextN ss2"], unfold Let_def, intro conjI impI)
        show "validTransV (ss1, nextN ss1)" 
          by (simp add: f1 nextN_stepN)

        show "validTransV (ss2, nextN ss2)" 
          by (simp add: f2 nextN_stepN)


        {assume sstat: "statA' = Diff"
         show "sstatO' statO ss1 ss2 = Diff"
         using v sa Δ1 sstat unfolding ss cfg statA'
         apply(simp add: Δ1_defs sstatO'_def sstatA'_def) 
         using cases_7[of pc3] apply(elim disjE)
         defer 1 defer 1 
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all) 
             using cfg finals ss status.distinct(1) updStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all) 
             using cfg finals ss status.distinct(1) updStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all)
             using cfg finals ss status.distinct(1) updStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all) 
             using cfg finals ss status.distinct(1) updStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all) 
             using cfg finals ss status.distinct(1) updStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all) 
             using cfg finals ss status.distinct(1) updStat.simps by auto
           by simp+
        } note stat = this

        show "(oor4 Δ1 Δ2 Δ3 Δ4) ∞ ss3' ss4' statA' (nextN ss1) (nextN ss2) (sstatO' statO ss1 ss2)"
        (* nonspec_normal and nonspec_mispred are the only nontrivial possibT, ibUTility, deferred to the end *)
        using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
          case spec_normal
          then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs)  
        next
          case spec_mispred
          then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs) 
        next
          case spec_Fence
          then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs) 
        next
          case spec_resolve
          then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs) 
        next
          case nonspec_mispred note nm3 = nonspec_mispred
          show ?thesis using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
            (* trace 4 can only have the same case as trace 3 as nontrivial case, here nonspec_mispred -- deferred *)
              case nonspec_normal
              then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs) 
            next
              case spec_normal
              then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs) 
            next
              case spec_mispred
              then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs) 
            next
              case spec_Fence
              then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs) 
            next
              case spec_resolve
              then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs) 
            next
              case nonspec_mispred note nm4 = nonspec_mispred
              then show ?thesis
              using sa Δ1 stat v3 v4 nm3 nm4 unfolding ss cfg hh apply clarsimp
              using cases_7[of pc3] apply(elim disjE)
                subgoal by simp
                subgoal by simp   
                subgoal by simp
                subgoal using xx_NN_cases[of vs3] apply(elim disjE)
                  subgoal apply(rule oor4I2) by (simp add: Δ1_defs Δ2_defs) 
                  subgoal apply(rule oor4I3) by (simp add: Δ1_defs Δ3_defs) .
                by (simp_all add: Δ1_defs)+  
          qed
        next
          case nonspec_normal note nn3 = nonspec_normal
          show ?thesis using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
          (* trace 4 can only have the same case as trace 3 as nontrivial case, here nonspec_normal -- deferred *)
            case nonspec_mispred
            then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs) 
          next
            case spec_normal
            then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs) 
          next
            case spec_mispred
            then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs) 
          next
            case spec_Fence
            then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs) 
          next
            case spec_resolve
            then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs) 
          next
            case nonspec_normal
            then show ?thesis using sa Δ1 stat v3 v4 nn3 unfolding ss cfg hh apply clarsimp
            using cases_7[of pc3] apply(elim disjE)
              subgoal by (simp add: Δ1_defs)
              subgoal by (simp add: Δ1_defs)
              subgoal apply(rule oor4I1) by(simp add:Δ1_defs) 
              subgoal using xx_NN_cases[of vs3] apply(elim disjE)
                 subgoal apply(rule oor4I1) by (simp add: Δ1_defs)
                 subgoal apply(rule oor4I1) by (simp add: Δ1_defs) .
              subgoal apply(rule oor4I1) by (simp add: Δ1_defs) 
              subgoal apply(rule oor4I1) by (simp add: Δ1_defs) 
              subgoal apply(rule oor4I1) by (simp add: Δ1_defs) 
              subgoal apply(rule oor4I4) by (simp add: Δ1_defs Δ4_defs)
              subgoal apply(rule oor4I4) by (simp add: Δ1_defs Δ4_defs) .
          qed
        qed
      qed
    qed
  qed
qed

(* *)

lemma step2: "unwindIntoCond Δ2 Δ1" 
proof(rule unwindIntoCond_simpleI)
  fix n ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ2: "Δ2 n ss3 ss4 statA ss1 ss2 statO"

  obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
  by (cases ss3, auto) 
  obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
  by (cases ss4, auto)
  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 = ss3 ss4 ss1 ss2
 
  obtain pc3 vs3 avst3 h3 p3 where 
  lcfgs3: "last cfgs3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
  by (cases "last cfgs3") (metis state.collapse vstore.collapse)
  obtain pc4 vs4 avst4 h4 p4 where 
  lcfgs4: "last cfgs4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
  by (cases "last cfgs4") (metis state.collapse vstore.collapse)
  note lcfgs = lcfgs3 lcfgs4

  have f1:"¬finalN ss1" 
    using Δ2 finalB_pc_iff' unfolding ss finalN_iff_finalB Δ2_defs
    by auto

  have f2:"¬finalN ss2" 
    using Δ2 finalB_pc_iff' unfolding ss finalN_iff_finalB Δ2_defs
    by auto

  have f3:"¬finalS ss3" 
    using Δ2 unfolding ss apply-apply(frule Δ2_implies)
    using finalS_cond_spec by simp

  have f4:"¬finalS ss4" 
    using Δ2 unfolding ss apply-apply(frule Δ2_implies)
    using finalS_cond_spec by simp


  note finals = f1 f2 f3 f4
  show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
    using finals by auto

  then show "isIntO ss3 = isIntO ss4" by simp

  show "match Δ1 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposibT,ibUTle case since isIntO always holds *)
    show "match1 Δ1 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def) 
    show "match2 Δ1 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def) 
    show "match12 Δ1 ss3 ss4 statA ss1 ss2 statO"
    (* Choose the ignore case (since traces 3 and 4 do speculation) *)
    proof(rule match12_simpleI, rule disjI1, intro conjI)
      fix ss3' ss4' statA'
      assume statA': "statA' = sstatA' statA ss3 ss4"
      and v: "validTransO (ss3, ss3')" "validTransO (ss4, ss4')" 
      and sa: "Opt.eqAct ss3 ss4"
      note v3 = v(1)  note v4 = v(2)

      obtain pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' where ss3': "ss3' = (pstate3', cfg3', cfgs3', ibT3', ibUT3', ls3')"
      by (cases ss3', auto) 
      obtain pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' where ss4': "ss4' = (pstate4', cfg4', cfgs4', ibT4', ibUT4', ls4')"
      by (cases ss4', auto)
      note ss = ss ss3' ss4'

      obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
      obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
      note hh = h3 h4

      show "¬ isSecO ss3"
      using v sa Δ2 unfolding ss by (simp add: Δ2_defs) 

      show "¬ isSecO ss4"
      using v sa Δ2 unfolding ss apply clarsimp 
      by (simp add: Δ2_defs, linarith) 

      show stat: "statA = statA' ∨ statO = Diff"
      using v sa Δ2
      apply (cases ss3, cases ss4, cases ss1, cases ss2)
      apply (cases ss3', cases ss4', clarsimp)
      unfolding ss statA' apply clarsimp        
      apply(simp_all add: Δ2_defs sstatA'_def) 
      apply(cases statO, simp_all) apply(cases statA, simp_all)
      unfolding finalS_defs
      by (smt (verit, ccfv_SIG) updStat.simps(1))

      show "Δ1 ∞ ss3' ss4' statA' ss1 ss2 statO"
      (* the only nontrivial combination of cases will be spec_resolve and spec_resolve *)
      using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using sa stat Δ2 unfolding ss by (simp add: Δ2_defs)
      next
        case nonspec_mispred
        then show ?thesis using sa stat Δ2 unfolding ss by (simp add: Δ2_defs)
      next
        case spec_normal
        then show ?thesis using sa stat Δ2 v3 unfolding ss apply- 
          apply(frule Δ2_implies) by(simp add: Δ2_defs) 
      next
        case spec_mispred
        then show ?thesis using sa stat Δ2 unfolding ss apply-  
        apply(frule Δ2_implies) by (simp add: Δ2_defs) 
      next
        case spec_Fence 
        then show ?thesis using sa stat Δ2 unfolding ss apply-  
          apply(frule Δ2_implies) by (simp add: Δ2_defs)
      next
        case spec_resolve note sr3 = spec_resolve
        show ?thesis using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
          case nonspec_normal
          then show ?thesis using sa stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs)
        next
          case nonspec_mispred
          then show ?thesis using sa stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs)
        next
          case spec_normal
          then show ?thesis using sa stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs) 
        next
          case spec_mispred
          then show ?thesis using sa stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs)
        next
          case spec_Fence 
          then show ?thesis using sa stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs)
        next
          case spec_resolve note sr4 = spec_resolve
          show ?thesis using sa stat Δ2 v3 v4 sr3 sr4 
          unfolding ss lcfgs hh apply-
          apply(frule Δ2_implies) apply (simp add: Δ2_defs Δ1_defs) by clarsimp 
        qed 
      qed 
    qed
  qed  
qed 

(* *)

lemma step3: "unwindIntoCond Δ3 (oor Δ3 Δ1')" 
proof(rule unwindIntoCond_simpleI) 
  fix n ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ3: "Δ3 n ss3 ss4 statA ss1 ss2 statO"

  obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
  by (cases ss3, auto) 
  obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
  by (cases ss4, auto)
  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 = ss3 ss4 ss1 ss2

  obtain pc3 vs3 avst3 h3 p3 where 
  lcfgs3: "last cfgs3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
  by (cases "last cfgs3") (metis state.collapse vstore.collapse)
  obtain pc4 vs4 avst4 h4 p4 where 
  lcfgs4: "last cfgs4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
  by (cases "last cfgs4") (metis state.collapse vstore.collapse)
  note lcfgs = lcfgs3 lcfgs4

  obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
  obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
  note hh = h3 h4

  have f1:"¬finalN ss1" 
    using Δ3 finalB_pc_iff' unfolding ss finalN_iff_finalB Δ3_defs
    by auto

  have f2:"¬finalN ss2" 
    using Δ3 finalB_pc_iff' unfolding ss finalN_iff_finalB Δ3_defs
    by auto

  have f3:"¬finalS ss3" 
    using Δ3 unfolding ss apply-apply(frule Δ3_implies)
    using finalS_cond_spec by simp

  have f4:"¬finalS ss4" 
    using Δ3 unfolding ss apply-apply(frule Δ3_implies)
    using finalS_cond_spec by simp

  have "vs3 xx = vs4 xx"
    using Δ3 lcfgs unfolding ss  
    apply-by(frule Δ3_implies, simp)

  note finals = f1 f2 f3 f4
  show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
    using finals by auto

  then show "isIntO ss3 = isIntO ss4" by simp

  show "match (oor Δ3 Δ1') ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposibT,ibUTle case since isIntO always holds *)
    show "match1 (oor Δ3 Δ1') ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def) 
    show "match2 (oor Δ3 Δ1') ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def) 
    show "match12 (oor Δ3 Δ1') ss3 ss4 statA ss1 ss2 statO"
    proof(rule match12_simpleI, rule disjI1, intro conjI) 
      fix ss3' ss4' statA'
      assume statA': "statA' = sstatA' statA ss3 ss4"
      and v: "validTransO (ss3, ss3')" "validTransO (ss4, ss4')" 
      and sa: "Opt.eqAct ss3 ss4"
      note v3 = v(1) note v4 = v(2)

      obtain pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' where ss3': "ss3' = (pstate3', cfg3', cfgs3', ibT3', ibUT3', ls3')"
      by (cases ss3', auto) 
      obtain pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' where ss4': "ss4' = (pstate4', cfg4', cfgs4', ibT4', ibUT4', ls4')"
      by (cases ss4', auto)
      note ss = ss ss3' ss4'

      show "¬ isSecO ss3"
      using v sa Δ3 unfolding ss by (simp add: Δ3_defs) 

      show "¬ isSecO ss4"
      using v sa Δ3 unfolding ss  by (simp add: Δ3_defs)  

      show stat: "statA = statA' ∨ statO = Diff"
      using v sa Δ3 
      apply (cases ss3, cases ss4, cases ss1, cases ss2)
      apply(cases ss3', cases ss4', clarsimp)
      unfolding ss statA' apply clarsimp        
      apply(simp_all add: Δ3_defs sstatA'_def) 
      apply(cases statO, simp_all) apply(cases statA, simp_all)
      unfolding finalS_defs  
      by (smt (z3) list.size(3) map_eq_imp_length_eq 
          n_not_Suc_n status.exhaust updStat.simps)


      show "oor Δ3 Δ1' ∞ ss3' ss4' statA' ss1 ss2 statO"
      using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using sa stat Δ3 lcfgs unfolding ss by (simp_all add: Δ3_defs)  
      next
        case nonspec_mispred
        then show ?thesis using sa stat Δ3 lcfgs unfolding ss by (simp_all add: Δ3_defs) 
      next
        case spec_mispred
        then show ?thesis using sa stat Δ3 lcfgs  unfolding ss apply-         
          apply(frule Δ3_implies, clarsimp)
          by (auto simp add: Δ3_defs)
      next (* the nontrivial cases deferred to the end: *)
        case spec_normal note sn3 = spec_normal
        show ?thesis
        using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
          case nonspec_normal
          then show ?thesis using sa stat Δ3 lcfgs sn3 unfolding ss 
          by (simp add: Δ3_defs)
        next
          case nonspec_mispred
          then show ?thesis using sa stat Δ3 lcfgs sn3 unfolding ss 
          by (simp add: Δ3_defs)
        next
          case spec_mispred
          then show ?thesis using sa stat Δ3 lcfgs sn3 unfolding ss 
          apply (simp add: Δ3_defs)  
          by (metis config.sel(1) last_map)
        next
          case spec_Fence
          then show ?thesis using sa stat Δ3 lcfgs sn3 unfolding ss 
          apply (simp add: Δ3_defs) 
          by (metis config.sel(1) last_map)
        next
          case spec_resolve
          then show ?thesis using sa stat Δ3 lcfgs sn3 unfolding ss 
          by (simp add: Δ3_defs) 
        next (* the nontrivial case deferred to the end: *)
          case spec_normal note sn4 = spec_normal
          show ?thesis
          apply(intro oorI1)
          unfolding ss Δ3_def apply- apply(clarify,intro conjI)
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh
            apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs) 
            using cases_7[of pc3] apply simp apply(elim disjE)
            apply simp_all  
            by (metis config.collapse config.inject in_set_butlastD last_in_set length_1_butlast length_map state.sel(2))+  
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh
            apply- apply(frule Δ3_implies) by(simp add: Δ3_defs)  
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh
            apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs) 
            using cases_7[of pc3] apply simp apply(elim disjE)
            by simp_all 
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh 
            apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs ) 
            using cases_7[of pc3] apply simp apply(elim disjE, simp_all)
            unfolding array_loc_def by (metis config.sel(2) dist_insert_su last_in_set state.sel(1) vstore.sel)+
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh 
              apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs) 
            using cases_7[of pc3] apply simp apply(elim disjE)
            apply simp_all by (metis array_loc_def dist_insert_su)+
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh 
              apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs) 
              using cases_7[of pc3] by(elim disjE, simp_all)
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh 
            apply- apply(frule Δ3_implies) apply(simp_all add: Δ3_defs) 
              by (metis length_Suc_conv list.size(3)) .
          qed
        next
          case spec_Fence note sf3 = spec_Fence
          show ?thesis
          using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
            case nonspec_normal
            then show ?thesis using sa stat Δ3 lcfgs sf3 unfolding ss 
            by (simp add: Δ3_defs)
          next
            case nonspec_mispred
            then show ?thesis using sa stat Δ3 lcfgs sf3 unfolding ss 
            by (simp add: Δ3_defs)
          next
            case spec_mispred
            then show ?thesis using sa stat Δ3 lcfgs sf3 unfolding ss 
            apply (simp add: Δ3_defs) 
            by (metis com.disc config.sel(1) last_map)  
          next
            case spec_resolve
            then show ?thesis using sa stat Δ3 lcfgs sf3 unfolding ss 
            by (simp add: Δ3_defs) 
          next 
            case spec_normal 
            then show ?thesis using sa stat Δ3 lcfgs sf3 unfolding ss 
            apply (simp add: Δ3_defs)  
            by (metis last_map local.spec_Fence(3) local.spec_normal(1) local.spec_normal(4)) 
          next (* the nontrivial case deferred to the end: *)
            case spec_Fence note sf4 = spec_Fence
            show ?thesis
            apply(intro oorI2)
            unfolding ss Δ1'_defs
            using sa stat Δ3 lcfgs v3 v4 sf3 sf4 unfolding ss hh
            apply- by(simp_all add: Δ3_defs Δ1'_defs, blast) 
          qed
        next
          case spec_resolve note sr3 = spec_resolve
          show ?thesis
          using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
            case nonspec_normal
            then show ?thesis using sa stat Δ3 lcfgs sr3 unfolding ss 
            by (simp add: Δ3_defs)
          next
            case nonspec_mispred
            then show ?thesis using sa stat Δ3 lcfgs sr3 unfolding ss 
            by (simp add: Δ3_defs)
          next
            case spec_mispred
            then show ?thesis using sa stat Δ3 lcfgs sr3 unfolding ss 
            by (simp add: Δ3_defs)   
          next
            case spec_normal
            then show ?thesis using sa stat Δ3 lcfgs sr3 unfolding ss 
            by (simp add: Δ3_defs) 
          next 
            case spec_Fence  
            then show ?thesis using sa stat Δ3 lcfgs sr3 unfolding ss 
            by (simp add: Δ3_defs)    
          next (* the nontrivial case deferred to the end: *)
            case spec_resolve note sr4 = spec_resolve
            show ?thesis
            apply(intro oorI2)
            using sa stat Δ3 lcfgs v3 v4 sr3 sr4 unfolding ss hh
            by(simp add: Δ3_defs Δ1_defs) 
          qed 
        qed
    qed
  qed  
qed 

(**)


lemma step1': "unwindIntoCond Δ1' Δ4" 
proof(rule unwindIntoCond_simpleI) 
  fix n ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ1': "Δ1' n ss3 ss4 statA ss1 ss2 statO"

  obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
  by (cases ss3, auto) 
  obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
  by (cases ss4, auto)
  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 = ss3 ss4 ss1 ss2
 
  obtain pc3 vs3 avst3 h3 p3 where 
  cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
  by (cases cfg3) (metis state.collapse vstore.collapse)
  obtain pc4 vs4 avst4 h4 p4 where 
  cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
  by (cases cfg4) (metis state.collapse vstore.collapse)
  note cfg = cfg3 cfg4

  obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
  obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
  note hh = h3 h4

  have f1:"¬finalN ss1" 
    using Δ1' finalB_pc_iff' unfolding ss cfg finalN_iff_finalB Δ1'_defs
    by simp 

  have f2:"¬finalN ss2" 
    using Δ1' finalB_pc_iff' unfolding ss cfg finalN_iff_finalB Δ1'_defs
    by simp 


  have f3:"¬finalS ss3" 
    using Δ1' unfolding ss apply-apply(frule Δ1'_implies)
    using finalS_cond by simp

  have f4:"¬finalS ss4" 
    using Δ1' unfolding ss apply-apply(frule Δ1'_implies)
    using finalS_cond by simp

  note finals = f1 f2 f3 f4

  show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
    using finals by auto

  then show "isIntO ss3 = isIntO ss4" by simp

  show "match Δ4 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposibT,ibUTle case since isIntO always holds *)
    show "match1 Δ4 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 Δ4 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 Δ4 ss3 ss4 statA ss1 ss2 statO"
    (* Choose the match12_12 case (since we have no mis-speculation yet) *)
    proof(rule match12_simpleI, rule disjI2, intro conjI)
      fix ss3' ss4' statA'
      assume statA': "statA' = sstatA' statA ss3 ss4"
      and v: "validTransO (ss3, ss3')" "validTransO (ss4, ss4')" 
      and sa: "Opt.eqAct ss3 ss4"
      note v3 = v(1) note v4 = v(2)

      obtain pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' where ss3': "ss3' = (pstate3', cfg3', cfgs3', ibT3', ibUT3', ls3')"
      by (cases ss3', auto) 
      obtain pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' where ss4': "ss4' = (pstate4', cfg4', cfgs4', ibT4', ibUT4', ls4')"
      by (cases ss4', auto)
      note ss = ss ss3' ss4'

      show "eqSec ss1 ss3"
        using v sa Δ1' unfolding ss 
        by (simp add: Δ1'_defs eqSec_def) 

      show "eqSec ss2 ss4"
        using v sa Δ1' unfolding ss 
        by (simp add: Δ1'_defs eqSec_def) 
      
      
      show "Van.eqAct ss1 ss2"
      using v sa Δ1' unfolding ss Van.eqAct_def
      by (simp_all add: Δ1'_defs)  

      show "match12_12 Δ4 ss3' ss4' statA' ss1 ss2 statO"
      unfolding match12_12_def
      proof(rule exI[of _ "nextN ss1"], rule exI[of _ "nextN ss2"], unfold Let_def, intro conjI impI)
        show "validTransV (ss1, nextN ss1)" 
          by (simp add: f1 nextN_stepN)

        show "validTransV (ss2, nextN ss2)" 
          by (simp add: f2 nextN_stepN)

        {assume sstat: "statA' = Diff"
         show "sstatO' statO ss1 ss2 = Diff"
         using v sa Δ1' sstat unfolding ss cfg statA'
         apply(simp add: Δ1'_defs sstatO'_def sstatA'_def) 
         apply(cases statO, simp_all) apply(cases statA, simp_all) 
         using cfg finals ss status.distinct(1) updStat.simps by auto
        } note stat = this

        show "Δ4 ∞ ss3' ss4' statA' (nextN ss1) (nextN ss2) (sstatO' statO ss1 ss2)"
        (* nonspec_normal and nonspec_mispred are the only nontrivial possibT,ibUTility, deferred to the end *)
        using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
          case spec_normal
          then show ?thesis using sa Δ1' stat unfolding ss by (simp add: Δ1'_defs)  
        next
          case spec_mispred
          then show ?thesis using sa Δ1' stat unfolding ss by (simp add: Δ1'_defs) 
        next
          case spec_Fence
          then show ?thesis using sa Δ1' stat unfolding ss by (simp add: Δ1'_defs) 
        next
          case spec_resolve
          then show ?thesis using sa Δ1' stat unfolding ss by (simp add: Δ1'_defs)
        next
          case nonspec_mispred 
          then show ?thesis using sa Δ1' stat unfolding ss by (simp add: Δ1'_defs)
        next
          case nonspec_normal note nn3 = nonspec_normal
          show ?thesis using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
          (* trace 4 can only have the same case as trace 3 as nontrivial case, here nonspec_normal -- deferred *)
            case nonspec_mispred
            then show ?thesis using sa Δ1' stat nn3 unfolding ss by (simp add: Δ1'_defs) 
          next
            case spec_normal
            then show ?thesis using sa Δ1' stat nn3 unfolding ss by (simp add: Δ1'_defs) 
          next
            case spec_mispred
            then show ?thesis using sa Δ1' stat nn3 unfolding ss by (simp add: Δ1'_defs) 
          next
            case spec_Fence
            then show ?thesis using sa Δ1' stat nn3 unfolding ss by (simp add: Δ1'_defs) 
          next
            case spec_resolve
            then show ?thesis using sa Δ1' stat nn3 unfolding ss by (simp add: Δ1'_defs) 
          next
            case nonspec_normal
            then show ?thesis using sa Δ1' stat v3 v4 nn3 unfolding ss cfg hh apply clarsimp
              by (auto simp add: Δ1'_defs Δ4_defs)
          qed
        qed
      qed
    qed  
  qed
qed

(* *)

lemma stepe: "unwindIntoCond Δ4 Δ4" 
proof(rule unwindIntoCond_simpleI) 
  fix n ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ4: "Δ4 n ss3 ss4 statA ss1 ss2 statO"

  obtain pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 where ss3: "ss3 = (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3)"
  by (cases ss3, auto) 
  obtain pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 where ss4: "ss4 = (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4)"
  by (cases ss4, auto)
  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 = ss3 ss4 ss1 ss2
 
  obtain pc3 vs3 avst3 h3 p3 where 
  cfg3: "cfg3 = Config pc3 (State (Vstore vs3) avst3 h3 p3)"
  by (cases cfg3) (metis state.collapse vstore.collapse)
  obtain pc4 vs4 avst4 h4 p4 where 
  cfg4: "cfg4 = Config pc4 (State (Vstore vs4) avst4 h4 p4)"
  by (cases cfg4) (metis state.collapse vstore.collapse)
  note cfg = cfg3 cfg4

  obtain hh3 where h3: "h3 = Heap hh3" by(cases h3, auto)
  obtain hh4 where h4: "h4 = Heap hh4" by(cases h4, auto)
  note hh = h3 h4

  show "finalS ss3 = finalS ss4 ∧ finalN ss1 = finalS ss3 ∧ finalN ss2 = finalS ss4"
    using Δ4 Opt.final_def Prog.endPC_def finalS_def stepS_endPC endPC_def finalB_endPC 
    unfolding Δ4_defs ss by clarsimp 

  then show "isIntO ss3 = isIntO ss4" by simp

  show "match Δ4 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposibT,ibUTle case since isIntO always holds *)
    show "match1 Δ4 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 Δ4 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 Δ4 ss3 ss4 statA ss1 ss2 statO"
    apply(rule match12_simpleI) using Δ4 unfolding ss apply (simp add: Δ4_defs)
    by (simp add: stepS_endPC)
  qed
qed
 
(* *)

lemmas theConds = step0 step1 step2 step3 step1' stepe


proposition rsecure
proof-
  define m where m: "m ≡ (6::nat)"
  define Δs where Δs: "Δs ≡ λi::nat. 
  if i = 0 then Δ0
  else if i = 1 then Δ1 
  else if i = 2 then Δ2
  else if i = 3 then Δ3 
  else if i = 4 then Δ4 
  else Δ1'" 
  define nxt where nxt: "nxt ≡ λi::nat. 
  if i = 0 then {0,1::nat}
  else if i = 1 then {1,2,3,4}  
  else if i = 2 then {1} 
  else if i = 3 then {3,5} 
  else {4}"
  show ?thesis apply(rule distrib_unwind_rsecure[of m nxt Δs])
    subgoal unfolding m by auto
    subgoal unfolding nxt m by auto
    subgoal using init unfolding Δs by auto
    subgoal 
      unfolding m nxt Δs apply (simp split: if_splits)
      using theConds
      unfolding oor_def oor4_def by auto . 
qed
end