Theory Fun_mask_secure

subsection "Proof"
theory Fun_mask_secure
  imports Fun_mask                            
begin 

(* THE PROOF OF SECURITY *)

definition "PC ≡ {0..8}"

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

(* 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  ∧ 
  ibT3≠[[]] ∧ ibT4≠[[]] ∧ ibT1 = ibT3 ∧ ibT2 = ibT4 ∧ 
  pcOf cfg3 ∈ beforeInput ∧ 
  ls1 = ls3 ∧ ls2 = ls4 ∧ 
  noMisSpec cfgs3 
 ))"

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

lemma Δ0_implies: "Δ0 n
   (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 ⟶ ibT3 ≠ LNil) ∧
   (pcOf cfg4 = 1 ⟶ ibT4 ≠ 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, linarith+)
   apply (metis map_is_Nil_conv)+
  by linarith


(* 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 ∧ 
  same_var_o ii cfg3 cfgs3 cfg4 cfgs4 ∧ 
  pcOf cfg3 ∈ afterInput ∧   
  Dist ls1 ls2 ls3 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
  by (metis list.map_disc_iff)

(* 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 ∧ 
  same_var_o ii cfg3 cfgs3 cfg4 cfgs4 ∧  
  pcOf cfg3 = startOfThenBranch ∧ cfgs3 ≠ [] ∧ 
  pcOf (last cfgs3) = startOfElseBranch ∧ 
  Dist ls1 ls2 ls3 ls4 ∧
  misSpecL1 cfgs3
 ))"

lemmas Δ2_defs = Δ2_def common_def PC_def same_var_o_def startOfThenBranch_def startOfElseBranch_def 
      misSpecL1_def

lemma Δ2_implies: "Δ2 n (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 = 3 ∧ 
   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 add: image_subset_iff) 
  by (metis length_map last_map list.map_disc_iff)+

(* 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 ∧ 
  same_var_o ii cfg3 cfgs3 cfg4 cfgs4 ∧  
  vstore (getVstore (stateOf cfg3)) ii ≥ int size_aa1 ∧
  pcOf cfg3 = startOfElseBranch ∧ 
  pcOf (last cfgs3) ∈ inThenBranchBeforeOutput ∧ 
  Dist ls1 ls2 ls3 ls4 ∧
  misSpecL1 cfgs3 
 ))"

lemma Δ3_def':"Δ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 ∧ 
  same_var_o ii cfg3 cfgs3 cfg4 cfgs4 ∧  
  vstore (getVstore (stateOf cfg3)) ii ≥ int size_aa1 ∧
  pcOf cfg3 = startOfElseBranch ∧ 
  pcOf (last cfgs3) ∈ inThenBranchBeforeOutput ∧ 
  Dist ls1 ls2 ls3 ls4 ∧
  misSpecL1 cfgs3 
 )" unfolding Δ3_def by auto

lemmas Δ3_defs = Δ3_def common_def PC_def same_var_o_def 
           startOfElseBranch_def inThenBranchBeforeOutput_def
           beforeAssign_vv_def misSpecL1_def 

lemma Δ3_implies: "Δ3 n (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) = 3 ∨ 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"
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)
  by (metis length_map)

(* *)

(* End: *)
definition Δe :: "enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δe  = (λ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 Δe_defs = Δe_def common_def endPC

(* *)

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(rule exI[of _ "(cfg4, ibT4, ibUT4, ls4)"])
apply(cases "getAvstore (stateOf cfg3)", cases "getAvstore (stateOf cfg4)")
unfolding Δ0_defs  
unfolding 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 linarith

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

  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 "react (oor Δ0 Δ1) ss3 ss4 statA ss1 ss2 statO"
  unfolding react_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) 

      show "eqSec ss2 ss4"
      using v sa Δ0 unfolding ss 
      apply (simp add: Δ0_defs) 
      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)
      using finals map_is_Nil_conv ss 
      by (metis Δ0 Δ0_implies getActO_pcOf 
          numeral_1_eq_Suc_0 numerals(1))

      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_8[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 newStat.simps)+
        } note stat = this

        show "oor Δ0 Δ1 ∞ ss3' ss4' statA' (nextN ss1) (nextN ss2) (sstatO' statO ss1 ss2)"
        (* the combination of nonspec_normal and nonspec_normal is the only nontrivial possibility, 
           deferred to the end *)
        using v3[unfolded ss, simplified] proof(cases rule: stepS_cases)
          case nonspec_mispred
          then show ?thesis using sa Δ0 stat unfolding ss 
            apply- apply(frule Δ0_implies) 
            by (simp add: Δ0_defs) 
        next
          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 spec_resolveI
          then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
        next
          case spec_resolveO
          then show ?thesis using sa Δ0 stat unfolding ss by (simp add: Δ0_defs)
        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 spec_resolveI
            then show ?thesis using sa Δ0 stat nn3 unfolding ss by (simp add: Δ0_defs)
          next
            case spec_resolveO
            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 Δ0 stat finals v3 v4 nn3 nn4 unfolding ss cfg apply clarsimp
            apply(cases "pc3 = 0")
              subgoal apply(rule oorI1)
              by (simp add: Δ0_defs) 
              subgoal apply(subgoal_tac "pc4 = 1")
              defer subgoal by (simp add: Δ0_defs)
              apply(rule oorI2) 
              by (simp add: Δ0_defs Δ1_defs Opt.eqAct_def) .  
          qed
        qed
      qed
    qed  
  qed
qed

(* *)

lemma step1: "unwindIntoCond Δ1 (oor4 Δ1 Δ2 Δ3 Δe)" 
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 "react (oor4 Δ1 Δ2 Δ3 Δe) ss3 ss4 statA ss1 ss2 statO"
  unfolding react_def proof(intro conjI)
    (* match1 and match2 are imposibT, ibUTle case since isIntO always holds *)
    show "match1 (oor4 Δ1 Δ2 Δ3 Δe) ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 (oor4 Δ1 Δ2 Δ3 Δe) ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 (oor4 Δ1 Δ2 Δ3 Δe) 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) 
      
      show "Van.eqAct ss1 ss2"
      using v sa Δ1 unfolding ss Van.eqAct_def
      by (simp_all add: Δ1_defs) 

      show "match12_12 (oor4 Δ1 Δ2 Δ3 Δe) 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 status.distinct(1)
           unfolding ss cfg statA'
         apply(simp add: Δ1_defs sstatO'_def sstatA'_def) 
         using cases_8[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) newStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all) 
             using cfg finals ss status.distinct(1) newStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all)
             using cfg finals ss status.distinct(1) newStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all)
             using cfg finals ss status.distinct(1)  map_is_Nil_conv outOf.simps 
               unfolding Dist_def  by force
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all) 
             using cfg finals ss status.distinct(1) newStat.simps by auto
           subgoal apply(cases statO, simp_all) apply(cases statA, simp_all) 
             using cfg finals ss status.distinct(1)  
              map_is_Nil_conv outOf.simps unfolding Dist_def  by force
           by simp+        } note stat = this

        show "oor4 Δ1 Δ2 Δ3 Δe ∞ ss3' ss4' statA' (nextN ss1) (nextN ss2) (sstatO' statO ss1 ss2)"
        (* nonspec_normal and nonspec_mispred are the only nontrivial possibility, 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 spec_resolveI
          then show ?thesis using sa Δ1 stat unfolding ss by (simp add: Δ1_defs) 
        next
          case spec_resolveO
          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 spec_resolveI
            then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs) 
          next
            case spec_resolveO
            then show ?thesis using sa Δ1 stat nn3 unfolding ss by (simp add: Δ1_defs) 
          next
            case nonspec_normal note nn4 = nonspec_normal
            then show ?thesis using sa Δ1 stat v3 v4 nn3 nn4 unfolding ss cfg hh apply clarsimp
            using cases_8[of pc3] apply(elim disjE)
              subgoal by (simp add: Δ1_defs)
              subgoal by (simp add: Δ1_defs)
              subgoal using ii_aa1_cases[of vs3] apply(elim disjE)
                subgoal apply(rule oor4I1) apply (simp add: Δ1_defs) .
                subgoal apply(rule oor4I1) apply (simp add: Δ1_defs) . .
              subgoal apply(rule oor4I1) by (auto simp add: Δ1_defs)
              subgoal using ii_aa1_cases[of vs3] apply(elim disjE)
                subgoal apply(rule oor4I1) by (auto simp add: Δ1_defs)   
                subgoal apply(rule oor4I1) by (simp add: Δ1_defs) .
              subgoal apply(rule oor4I1) by (simp add: Δ1_defs array_loc_def)
              subgoal apply(rule oor4I4) by (simp add: Δ1_defs Δe_defs) 
              subgoal apply(rule oor4I4) by (simp add: Δ1_defs Δe_defs) 
              subgoal apply(rule oor4I4) by (simp add: Δ1_defs Δe_defs) 
              subgoal by (simp add: Δ1_defs Δe_defs) .
          qed
        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 spec_resolveI
            then show ?thesis using sa Δ1 stat nm3 unfolding ss by (simp add: Δ1_defs) 
          next
            case spec_resolveO
            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_8[of pc3] apply(elim disjE)
              subgoal by (simp add: Δ1_defs)
              subgoal by (simp add: Δ1_defs)
              subgoal using ii_aa1_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) .
              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 by (simp add: Δ1_defs Δe_defs) 
              subgoal by (simp add: Δ1_defs Δe_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 "react Δ1 ss3 ss4 statA ss1 ss2 statO"
  unfolding react_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 
      apply (simp add: Δ2_defs) by metis  

      show stat: "statA = statA' ∨ statO = Diff"
      using v sa Δ2
      apply (cases ss3, cases ss4, cases ss1, cases ss2, cases ss3', cases ss4', clarsimp)
      using v sa Δ2 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) newStat.simps(1))

      have isO:"is_Output (prog ! pcOf (last cfgs3))" "is_Output (prog ! pcOf (last cfgs4))" using Δ2_implies[OF Δ2[unfolded ss]] by (simp add: is_Output1)+


      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_resolveI
        then show ?thesis using isO by auto
      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_resolveI 
          then show ?thesis using isO by auto
        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) 
          by (simp add: Δ2_defs Δ1_defs, clarsimp)
        next
          case spec_resolveO note sr4 = spec_resolveO
          show ?thesis using sa stat Δ2 v3 v4 sr3 sr4 
          unfolding ss lcfgs hh apply-
          apply(frule Δ2_implies) 
          by (simp add: Δ2_defs Δ1_defs, clarsimp) 
      qed 
    next
        case spec_resolveO note sr3 = spec_resolveO
        then have cfgs4:"cfgs4 ≠ []" using Δ2_implies[OF Δ2[unfolded ss]] by auto
        show ?thesis using v4[unfolded ss, simplified] proof(cases rule: stepS_cases)
          case nonspec_normal
          then show ?thesis by(simp add:cfgs4)
        next
          case nonspec_mispred
          then show ?thesis by(simp add:cfgs4)
        next
          case spec_normal
          then show ?thesis by (simp add: isO) 
        next
          case spec_mispred
          then show ?thesis using isO by auto
        next
          case spec_Fence 
          then show ?thesis using isO by auto
        next
          case spec_resolveI
          then show ?thesis using isO by blast
        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) 
          by (simp add: Δ2_defs Δ1_defs, clarsimp)
        next
          case spec_resolveO note sr4 = spec_resolveO
          show ?thesis using sa stat Δ2 v3 v4 sr3 sr4 
          unfolding ss lcfgs hh apply-
          apply(frule Δ2_implies) 
          by (simp add: Δ2_defs Δ1_defs, 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


  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 "react (oor Δ3 Δ1) ss3 ss4 statA ss1 ss2 statO"
  unfolding react_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 = ss3 ss4 ss1 ss2 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, cases ss3', cases ss4', clarsimp)
      using v sa Δ3 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 newStat.simps)

    have notI_if_fence:"¬is_getInput (prog ! pcOf (last cfgs4))" "¬is_IfJump (prog ! pcOf (last cfgs4))" 
                 "prog ! pcOf (last cfgs3) ≠ Fence" 
        using is_Output_pcOf is_getTrustedInput_pcOf 
              Δ3_implies[OF Δ3[unfolded ss]] prog_def by auto
      have pc:"pcOf (last cfgs4) = pcOf (last cfgs3)" "cfgs3 ≠ []" "cfgs4 ≠ []" using Δ3_implies[OF Δ3[unfolded ss]] by auto 

      have vs_eq:"vstore (getVstore (stateOf cfg3)) ii = vs3 ii"
           "vs4 ii = vs3 ii"
        using Δ3[unfolded ss Δ3_def' same_var_o_def misSpecL1_def] 
              last_in_set[OF pc(2),unfolded lcfgs] last_in_set[OF pc(3),unfolded lcfgs] 
        by fastforce+

      hence condition:"int size_aa1 ≤ vs3 ii" "int size_aa1 ≤ vs4 ii" using vs_eq Δ3[unfolded ss Δ3_def'] by auto


      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 notI_if_fence pc by auto
      next
        case spec_resolveI
        then show ?thesis using notI_if_fence pc by auto
      next
        case spec_Fence
        then show ?thesis using notI_if_fence pc by auto
      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
          case spec_resolveO
          then show ?thesis using sn3 pc by auto
        next
          case spec_resolveI
          then show ?thesis using sn3 pc by auto
        next (* the nontrivial case deferred to the end: *)
          case spec_normal note sn4 = spec_normal
          show ?thesis apply(rule oorI1) 
            using cases_branch[of pc3] apply(elim disjE)
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh
                    apply- apply(frule Δ3_implies) by(simp add: Δ3_defs) 
            
            subgoal unfolding ss Δ3_def' apply- apply(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_branch[of pc3] apply simp apply(elim disjE)
                 apply simp_all 
                by (metis config.sel(2) empty_iff last_in_set length_1_butlast length_map set_empty2 state.sel(2))+
              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_branch[of pc3] apply simp apply(elim disjE)
                 apply simp_all 
                by (metis  config.sel(2) last_in_set state.sel(1) subset_code(1) vstore.sel)+
              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) by(simp add: Δ3_defs) 
              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 Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh 
                apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs array_loc_def) 
                by (metis Dist_ignore config.sel(2) 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) by(simp add: Δ3_defs).

            subgoal unfolding ss Δ3_def' apply- apply(intro conjI)
              subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 condition unfolding ss hh
                apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs) 
                by (metis config.sel(2) last_in_set state.sel(2))
              subgoal using vs_eq sa stat Δ3 lcfgs v3 v4 sn3 sn4 condition 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) by(simp add: Δ3_defs) 
              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 condition unfolding ss hh
                apply- apply(frule Δ3_implies) by(simp add: Δ3_defs) 
              subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 condition unfolding ss  
                apply- apply(frule Δ3_implies) by(simp add: Δ3_defs) 
              subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 condition unfolding ss hh 
                apply- apply(frule Δ3_implies) by(simp add: Δ3_defs) .
              subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 is_Output1 unfolding ss hh
                by(simp add: Δ3_defs) 
            subgoal using sa stat Δ3 lcfgs v3 v4 sn3 sn4 unfolding ss hh
              apply- apply(frule Δ3_implies) by(simp add: Δ3_defs) .
        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
            case spec_resolveI
            then show ?thesis using notI_if_fence pc by auto
          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
            apply(simp add: Δ3_defs Δ1_defs) 
            by (metis empty_iff empty_set length_1_butlast map_eq_imp_length_eq)
          next (* the nontrivial case deferred to the end: *)
            case spec_resolveO note sr4 = spec_resolveO
            show ?thesis
            apply(intro oorI2)
            using sa stat Δ3 lcfgs v3 v4 sr3 sr4 unfolding ss hh
            apply(simp add: Δ3_defs Δ1_defs) 
            by (metis empty_iff empty_set length_1_butlast map_eq_imp_length_eq)
          qed 
        next
          case spec_resolveO note sr3 = spec_resolveO
          hence isO: "is_Output (prog ! pcOf (last cfgs4))" unfolding pc by auto
          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 notI_if_fence pc by auto
          next
            case spec_normal
            then show ?thesis using isO by auto
          next 
            case spec_Fence  
            then show ?thesis using notI_if_fence pc by auto  
          next
            case spec_resolveI
            then show ?thesis using notI_if_fence pc by auto
          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
            apply(simp add: Δ3_defs Δ1_defs) 
            by (metis empty_iff empty_set length_1_butlast map_eq_imp_length_eq)
          next (* the nontrivial case deferred to the end: *)
            case spec_resolveO note sr4 = spec_resolveO
            show ?thesis
            apply(intro oorI2)
            using sa stat Δ3 lcfgs v3 v4 sr3 sr4 unfolding ss hh
            apply(simp add: Δ3_defs Δ1_defs) 
            by (metis empty_iff empty_set length_1_butlast map_eq_imp_length_eq)
          qed 
        qed
    qed
  qed  
qed 

(* *)

lemma stepe: "unwindIntoCond Δe Δe" 
proof(rule unwindIntoCond_simpleI) 
  fix n ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
    and Δe: "Δe 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 Δe Opt.final_def Prog.endPC_def finalS_def stepS_endPC
    unfolding Δe_defs ss by clarsimp

  then show "isIntO ss3 = isIntO ss4" by simp

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

lemmas theConds = step0 step1 step2 step3 stepe
find_theorems unwindIntoCond name: rsecure

proposition rsecure
proof-
  define m where m: "m ≡ (5::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 Δe" 
  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,1}  
  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 (auto split: if_splits)
      using theConds
      unfolding oor_def oor3_def oor4_def by auto . 
qed
end