Theory Fun5_secure

subsection "Proof"
theory Fun5_secure
imports Fun5
begin 

(* THE PROOF OF SECURITY *)


(* Common to all the unwinding relations in this proof: *)
definition common :: "enat ⇒ enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" 
where 
"common = (λw1 w2
   (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 ∧
 llength ibUT1 = ∞ ∧ llength ibUT2 = ∞ ∧
 ibUT1 = ibUT3 ∧ ibUT2 = ibUT4 ∧

  w1 = w2 ∧
 ⌦‹   ›
 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) ∧
  Dist ls1 ls2 ls3 ls4))"

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

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

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

lemma Δ0_implies: "Δ0 num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO ⟹ 
   pcOf cfg1 < 12 ∧ pcOf cfg2 = pcOf cfg1 ∧
   ibUT1 ≠ [[]] ∧ ibUT2 ≠ [[]] ∧ cfgs4 = []"
  apply (meson Δ0_def common_implies)
  by (simp_all add: Δ0_defs, metis Nil_is_map_conv)

(* After input is inserted, no mis-speculation *)
definition Δ1 :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ1 = (λ num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
     (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
     statA 
     (cfg1,ibT1,ibUT1,ls1) 
     (cfg2,ibT2,ibUT2,ls2) 
     statO.
 (common w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
     (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
     statA 
     (cfg1,ibT1,ibUT1,ls1) 
     (cfg2,ibT2,ibUT2,ls2) 
     statO ∧ 
  pcOf cfg3 ∈ inWhile ∧ 
  same_var_o xx cfg3 cfgs3 cfg4 cfgs4 ∧
  noMisSpec cfgs3
))"
lemmas Δ1_defs = Δ1_def common_def PC_def noMisSpec_def inWhile_def same_var_o_def
lemma Δ1_implies: "Δ1 n w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3)
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO ⟹ 
   pcOf cfg3 < 12 ∧ cfgs3 = [] ∧ ibUT3 ≠ [[]] ∧
   pcOf cfg4 < 12 ∧ cfgs4 = [] ∧ ibUT4 ≠ [[]]"
  unfolding Δ1_defs apply simp 
  by (metis Nil_is_map_conv infinity_ne_i0 llength_LNil)

(* WHILE mis-speculation: *)
definition Δ1' :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ1' = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
     (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
     statA 
     (cfg1,ibT1,ibUT1,ls1) 
     (cfg2,ibT2,ibUT2,ls2) 
     statO.
 (common w1 w2 (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 xx cfg3 cfgs3 cfg4 cfgs4 ∧  
  whileSpeculation cfg3 (last cfgs3) ∧
  misSpecL1 cfgs3 ∧ misSpecL1 cfgs4 ∧
  w1 = ∞
))"
lemmas Δ1'_defs = Δ1'_def common_def PC_def same_var_def 
                  startOfIfThen_def startOfElseBranch_def 
                  misSpecL1_def whileSpec_defs

lemma Δ1'_implies: "Δ1' num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO ⟹ 
   pcOf cfg3 < 12 ∧ pcOf cfg4 < 12 ∧
   whileSpeculation cfg3 (last cfgs3) ∧
   whileSpeculation cfg4 (last cfgs4) ∧
   length cfgs3 = Suc 0 ∧ length cfgs4 = Suc 0"
  unfolding Δ1'_defs 
  apply (simp add: lessI, clarify)
  by (metis last_map length_0_conv)


(* Left mis-speculation: *)
definition Δ2 :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ2 = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
     (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
     statA 
     (cfg1,ibT1,ibUT1,ls1) 
     (cfg2,ibT2,ibUT2,ls2) 
     statO. 
 (common w1 w2 (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 xx cfg3 cfgs3 cfg4 cfgs4 ∧  
  pcOf cfg3 = startOfIfThen ∧ pcOf (last cfgs3) ∈ inElseIf ∧ 
  misSpecL1 cfgs3 ∧ misSpecL1 cfgs4 ∧

  (pcOf (last cfgs3) = startOfElseBranch ⟶ w1 = ∞) ∧
  (pcOf (last cfgs3) = 3 ⟶ w1 = 3) ∧

  (pcOf (last cfgs3) = startOfWhileThen ∨
   pcOf (last cfgs3) = whileElse ⟶ w1 = 1)
))"

lemmas Δ2_defs = Δ2_def common_def PC_def same_var_o_def misSpecL1_def
                  startOfIfThen_def inElseIf_def same_var_def
                  startOfWhileThen_def whileElse_def startOfElseBranch_def

lemma Δ2_implies: "Δ2 num w1 w2 (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) ∈ inElseIf ∧ pcOf cfg3 = 6 ∧
   pcOf (last cfgs4) = pcOf (last cfgs3) ∧
   pcOf cfg4 = pcOf cfg3 ∧ length cfgs3 = Suc 0 ∧
   length cfgs4 = Suc 0 ∧ same_var xx (last cfgs3) (last cfgs4)"
apply(intro conjI)
  unfolding Δ2_defs  
        apply (simp_all add: image_subset_iff) 
  by (metis last_in_set length_0_conv Nil_is_map_conv last_map length_map)+

(* 2nd specualtion level: *)
definition Δ2' :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ2' = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
     (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
     statA 
     (cfg1,ibT1,ibUT1,ls1) 
     (cfg2,ibT2,ibUT2,ls2) 
     statO.
 (common w1 w2 (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 xx cfg3 cfgs3 cfg4 cfgs4 ∧  
  pcOf cfg3 = startOfIfThen ∧ 
  whileSpeculation (cfgs3!0) (last cfgs3) ∧
  misSpecL2 cfgs3 ∧ misSpecL2 cfgs4 ∧
  w1 = 2
))"

lemmas Δ2'_defs = Δ2'_def common_def PC_def same_var_def   
                   startOfElseBranch_def startOfIfThen_def
                   whileSpec_defs misSpecL2_def

lemma Δ2'_implies: "Δ2' num w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
   (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
   statA 
   (cfg1,ibT1,ibUT1,ls1) 
   (cfg2,ibT2,ibUT2,ls2) 
   statO ⟹ 
  pcOf cfg3 = 6 ∧ pcOf cfg4 = 6 ∧
  whileSpeculation (cfgs3!0) (last cfgs3) ∧
  whileSpeculation (cfgs4!0) (last cfgs4) ∧
  length cfgs3 = 2 ∧ length cfgs4 = 2"
  apply(intro conjI)
  unfolding Δ2'_defs apply (simp add: lessI, clarify) 
  apply linarith+ apply simp_all 
  by (metis list.inject map_L2)

(* Right mis-speculation: *)
definition Δ3 :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δ3 = (λnum w1 w2 (pstate3,cfg3,cfgs3,ibT3,ibUT3,ls3) 
     (pstate4,cfg4,cfgs4,ibT4,ibUT4,ls4)  
     statA 
     (cfg1,ibT1,ibUT1,ls1) 
     (cfg2,ibT2,ibUT2,ls2) 
     statO.
 (common w1 w2 (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 xx cfg3 cfgs3 cfg4 cfgs4 ∧  
  pcOf cfg3 = startOfElseBranch ∧ pcOf (last cfgs3) ∈ inThenIfBeforeFence ∧ 
  misSpecL1 cfgs3 ∧
  (pcOf (last cfgs3) = 6 ⟶ w1 = ∞) ∧
  (pcOf (last cfgs3) = 7 ⟶ w1 = 1)
))"

lemmas Δ3_defs = Δ3_def common_def PC_def same_var_o_def 
                  startOfElseBranch_def inThenIfBeforeFence_def

lemma Δ3_implies: "Δ3 num w1 w2 (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) ∈ inThenIfBeforeFence ∧ 
   pcOf (last cfgs4) = pcOf (last cfgs3) ∧
   pcOf cfg3 = 10 ∧ pcOf cfg3 = pcOf cfg4 ∧
   length cfgs3 = Suc 0 ∧ length cfgs4 = Suc 0"
apply(intro conjI)
  unfolding Δ3_defs 
  apply (simp_all add: image_subset_iff) 
  by (metis last_map map_is_Nil_conv length_map)+

(* *)

(* End: *)
definition Δe :: "enat ⇒ enat ⇒ enat ⇒ stateO ⇒ stateO  ⇒ status ⇒ stateV ⇒ stateV ⇒ status ⇒ bool" where 
"Δe = (λnum w1 w2 (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_def  

(* *)

lemma init: "initCond Δ0" 
unfolding initCond_def apply safe  
  subgoal for pstate3 cfg3 cfgs3 ibT3 ibUT3 ls3 pstate4 cfg4 cfgs4 ibT4 ibUT4 ls4 
  unfolding istateO.simps apply clarsimp 
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 w1 w2 ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ0: "Δ0 n w1 w2 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 unfolding ss 
    apply-by(frule Δ0_implies, simp)

  have f2:"¬finalN ss2" 
    using Δ0 unfolding ss 
    apply-by(frule Δ0_implies, simp)

  have f3:"¬finalS ss3" 
    using Δ0 unfolding ss 
    apply-apply(frule Δ0_implies, unfold Δ0_defs)
    by (clarify,metis finalS_cond')

  have f4:"¬finalS ss4" 
    using Δ0 unfolding ss 
    apply-apply(frule Δ0_implies, unfold Δ0_defs)
    by (clarify,metis finalS_cond')

  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) w1 w2 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposible case since isIntO always holds *)
    show "match1 (oor Δ0 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 (oor Δ0 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 (oor Δ0 Δ1) w1 w2 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 map_is_Nil_conv)

      show "Van.eqAct ss1 ss2"
        using v sa Δ0 unfolding ss   
        apply-apply(frule Δ0_implies)
      unfolding Opt.eqAct_def 
                Van.eqAct_def
      by(simp_all add: Δ0_defs, linarith) 

      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_12[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(1) updStat.simps(2,3) updStat_diff)+
        } 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
          by (simp add: Δ0_defs numeral_1_eq_Suc_0, linarith) 
        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 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 Δ0 stat v3 v4 nn3 nn4 unfolding ss cfg apply clarsimp
            apply(unfold Δ0_defs, clarsimp, elim disjE)
              subgoal by(rule oorI1, auto simp add: Δ0_defs) 
              subgoal by (rule oorI1, simp add: Δ0_defs) 
              subgoal by (rule oorI2, simp add: Δ1_defs) .
          qed
        qed
      qed
    qed  
  qed
qed

(* *)

lemma step1: "unwindIntoCond Δ1 (oor5 Δ1 Δ1' Δ2 Δ3 Δe)" 
proof(rule unwindIntoCond_simpleI) 
  fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ1: "Δ1 n w1 w2 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 unfolding ss Δ1_def apply clarify
  apply(frule common_implies) 
  using finalB_pcOf_iff finalN_iff_finalB nat_less_le by blast

  have f2:"¬finalN ss2" 
  using Δ1 unfolding ss Δ1_def apply clarify
  apply(frule common_implies) 
  using finalB_pcOf_iff finalN_iff_finalB nat_less_le by metis


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

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

  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 (oor5 Δ1 Δ1' Δ2 Δ3 Δe) w1 w2 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposible cases, since isIntO always holds *)
    show "match1 (oor5 Δ1 Δ1' Δ2 Δ3 Δe) w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 (oor5 Δ1 Δ1' Δ2 Δ3 Δe) w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 (oor5 Δ1 Δ1' Δ2 Δ3 Δe) w1 w2 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) 

      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   
      unfolding Opt.eqAct_def Van.eqAct_def
      apply(simp_all add: Δ1_defs)
      by (metis Nil_is_map_conv f3 infinity_ne_i0 llength_LNil ss3)

      show "match12_12 (oor5 Δ1 Δ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 finals unfolding ss cfg statA'
           apply-apply(frule Δ1_implies)
         apply(simp add: Δ1_defs sstatO'_def sstatA'_def updStat_EqI) 
         using cases_12[of pc3] apply(elim disjE, simp_all)
         subgoal apply(cases statO, simp_all) 
           by(cases statA, simp_all add: updStat_EqI)
         subgoal apply(cases statO, simp_all) 
           by(cases statA, simp_all add: updStat_EqI) 
         subgoal apply(cases statO, simp_all) 
           by(cases statA, simp_all add: updStat_EqI) 
         subgoal apply(cases statO, simp_all) 
           by(cases statA, simp_all add: updStat_EqI)
         subgoal apply(cases statO, simp_all) 
           by(cases statA, simp_all add: updStat_EqI)
         subgoal apply(cases statO, simp_all) 
           by(cases statA, simp_all add: updStat_EqI)
         subgoal apply(cases statO, simp_all, cases statA) 
           by (simp_all add: updStat_EqI split: if_splits)  
         subgoal apply(cases statO, simp_all) 
           by(cases statA, simp_all add: updStat_EqI)
         apply(cases statO, simp_all, cases statA) 
           by (simp_all add: updStat_EqI split: if_splits)
        } note stat = this

        show "oor5 Δ1 Δ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 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 note nn4 = nonspec_normal
            then show ?thesis using sa Δ1 stat v3 v4 nn3 nn4 f4 unfolding ss cfg Opt.eqAct_def
            apply clarsimp using cases_12[of pc3] apply(elim disjE)
              subgoal by (simp add: Δ1_defs)
              subgoal by (simp add: Δ1_defs)
              subgoal by (simp add: Δ1_defs)
              subgoal using xx_0_cases[of vs3] apply(elim disjE)
                subgoal by(rule oor5I1, auto simp add: Δ1_defs)
                subgoal by(rule oor5I1, auto simp add: Δ1_defs) .
              subgoal apply(rule oor5I1) by (auto simp add: Δ1_defs) 
              subgoal using xx_NN_cases[of vs3] apply(elim disjE)
                subgoal by(rule oor5I1, auto simp add: Δ1_defs)
                subgoal by(rule oor5I1, auto simp add: Δ1_defs) .
              subgoal by(rule oor5I1, auto simp add: Δ1_defs hh)
              subgoal by(rule oor5I1, auto simp add: Δ1_defs)   
              subgoal by(rule oor5I1, auto simp add: Δ1_defs hh) 
              subgoal by(rule oor5I1, auto simp add: Δ1_defs) 
              subgoal by(rule oor5I1, auto simp add: Δ1_defs) 
              by(rule oor5I5, simp_all 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 nonspec_mispred note nm4 = nonspec_mispred
            then show ?thesis using sa Δ1 stat v3 v4 nm3 nm4 unfolding ss cfg apply clarsimp
            using cases_12[of pc3] apply(elim disjE)
              prefer 4 subgoal using xx_0_cases[of vs3] apply(elim disjE)
                subgoal by(rule oor5I2, auto simp add: Δ1_defs Δ1'_defs) 
                subgoal by(rule oor5I2, auto simp add: Δ1_defs Δ1'_defs) .
              prefer 5 subgoal using xx_NN_cases[of vs3] apply(elim disjE)
                subgoal apply(rule oor5I3) by (auto simp add: Δ1_defs Δ2_defs)
                subgoal apply(rule oor5I4) by (auto simp add: Δ1_defs Δ3_defs) .
              by (simp_all add: Δ1_defs) 
          qed
        qed
      qed
    qed  
  qed
qed

(* *)

lemma step2: "unwindIntoCond Δ2 (oor3 Δ2 Δ2' Δ1)" 
proof(rule unwindIntoCond_simpleI)
  fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ2: "Δ2 n w1 w2 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 unfolding ss Δ2_def
  apply clarsimp 
  by(frule common_implies, simp)

  have f2:"¬finalN ss2" 
  using Δ2 unfolding ss Δ2_def
  apply clarsimp 
  by(frule common_implies, simp)


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

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

  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

  then have lpc3:"pcOf (last cfgs3) = 10 ∨ 
                  pcOf (last cfgs3) = 3 ∨
                  pcOf (last cfgs3) = 4 ∨
                  pcOf (last cfgs3) = 11"
    using Δ2 unfolding ss Δ2_defs by simp

  (*because of a spliting on the cases, it's simpler to prove these prior*)
  have sec3[simp]:"¬ isSecO ss3"
    using Δ2 unfolding ss by (simp add: Δ2_defs) 
  have sec4[simp]:"¬ isSecO ss4"
      using Δ2 unfolding ss by (simp add: Δ2_defs)   

    have stat[simp]:"⋀s3' s4' statA'. statA' = sstatA' statA ss3 ss4 ⟹ 
               validTransO (ss3, s3') ⟹ validTransO (ss4, s4') ⟹
               (statA = statA' ∨ statO = Diff)"
    subgoal for ss3' ss4'
      apply (cases ss3, cases ss4, cases ss1, cases ss2)
      apply (cases ss3', cases ss4', clarsimp)
      using Δ2 finals unfolding ss apply clarsimp        
      apply(simp_all add: Δ2_defs sstatA'_def) 
      apply(cases statO, simp_all) by (cases statA, simp_all add: updStat_EqI) .

  have xx:"vs3 xx = vs4 xx" using Δ2 lcfgs unfolding ss Δ2_defs apply clarsimp
    by (metis cfgs_Suc_zero config.sel(2) list.set_intros(1) state.sel(1) vstore.sel)
    
  have oor3_rule:"⋀ss3' ss4'. ss3 →S ss3' ⟹ ss4 →S ss4' ⟹
                    (pcOf (last cfgs3) = 10 ⟶ oor3 Δ2 Δ2' Δ1 ∞ 3 3 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO) 
                  ∧ (pcOf (last cfgs3) = 3 ∧ mispred pstate4 [6, 3] ⟶ oor3 Δ2 Δ2' Δ1 ∞ 2 2 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO)
                  ∧ (pcOf (last cfgs3) = 3 ∧ ¬mispred pstate4 [6, 3] ⟶ oor3 Δ2 Δ2' Δ1 ∞ 1 1 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO)
                  ∧ ((pcOf (last cfgs3) = 4 ∨ pcOf (last cfgs3) = 11) ⟶ oor3 Δ2 Δ2' Δ1 ∞ 0 0 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO) ⟹
                    ∃w1'<w1. ∃w2'<w2. oor3 Δ2 Δ2' Δ1 ∞ w1' w2' ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO"       
    subgoal for ss3' ss4' apply(cases ss3', cases ss4')
        subgoal for pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' 
                    pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' 
     subgoal premises p using lpc3 apply-apply(erule disjE)
          subgoal apply(intro exI[of _ 3], intro conjI)
            subgoal using Δ2 unfolding ss Δ2_defs apply clarify
              by (metis enat_ord_simps(4) numeral_ne_infinity)
            apply(intro exI[of _ 3], rule conjI)
            subgoal using Δ2 unfolding ss Δ2_defs apply clarify
              by (metis enat_ord_simps(4) numeral_ne_infinity)
            using p by (simp add: p)
          apply(erule disjE)
          subgoal apply(cases "mispred pstate4 [6, 3]")
             subgoal apply(intro exI[of _ 2], intro conjI)
              using Δ2 unfolding ss Δ2_defs apply clarify
                apply (metis enat_ord_number(2) eval_nat_numeral(3) lessI)
              apply(intro exI[of _ 2], rule conjI)
              using Δ2 unfolding ss Δ2_defs apply clarify
               apply (metis enat_ord_number(2) eval_nat_numeral(3) lessI)
             using Δ2 p unfolding ss Δ2_defs by clarify
          subgoal apply(intro exI[of _ 1], intro conjI)
          using Δ2 unfolding ss Δ2_defs apply clarify
            apply (metis one_less_numeral_iff semiring_norm(77))
          apply(intro exI[of _ 1], rule conjI)
          using Δ2 unfolding ss Δ2_defs apply clarify
           apply (metis one_less_numeral_iff semiring_norm(77))
          using Δ2 p unfolding ss Δ2_defs by clarify .
        subgoal apply(intro exI[of _ 0], intro conjI)
            using Δ2 unfolding ss Δ2_defs apply clarify
             apply (metis less_numeral_extra(1))
            apply(intro exI[of _ 0], rule conjI)
            using Δ2 unfolding ss Δ2_defs apply clarify
             apply (metis less_numeral_extra(1))
            using Δ2 p unfolding ss Δ2_defs by clarify . . . .

  show "match (oor3 Δ2 Δ2' Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposible case since isIntO always holds *)
    show "match1 (oor3 Δ2 Δ2' Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 (oor3 Δ2 Δ2' Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 (oor3 Δ2 Δ2' Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
      apply(rule match12_simpleI, simp_all, rule disjI1)
      subgoal for ss3' ss4' apply(cases ss3', cases ss4')
        subgoal for pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' 
                    pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' 
        apply-apply(rule oor3_rule, assumption+, intro conjI impI) 
      (*pc10*)
      subgoal premises prem using prem(1)[unfolded ss prem(4)] 
      proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs)  
      next
        case nonspec_mispred
        then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_mispred
        then show ?thesis using stat Δ2 prem(6) unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_Fence
        then show ?thesis using stat Δ2 prem(6) unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_resolve
        then show ?thesis 
          using Δ2 prem(6) resolve_106
          unfolding ss Δ2_defs  apply clarify 
          using cfgs_map misSpecL1_def  
          by (smt (z3) insert_commute list.simps(15) resolve.simps)
      next
        case spec_normal note sn3 = spec_normal
        show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
          case nonspec_normal
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs) 
        next
          case nonspec_mispred
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs)
        next
          case spec_Fence
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map) 
        next
          case spec_resolve
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map) 
        next
          case spec_mispred
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map) 
        next
          case spec_normal note sn4 = spec_normal
          have pc4:"pc4 = 10" using Δ2 prem lcfgs unfolding ss Δ2_defs by auto
          show ?thesis 
            using Δ2 prem sn3 sn4 finals stat unfolding ss prem(4,5) lcfgs
            apply-apply(frule Δ2_implies, unfold Δ2_defs) apply clarsimp
            apply(rule oor3I1) apply(simp_all add: Δ2_defs pc4) 
            using final_def config.sel(2) last_in_set 
                  lcfgs state.sel(1,2) vstore.sel xx 
            by (metis (mono_tags, lifting))
       qed
      qed

      (*pc3*)
     subgoal premises prem using prem(1)[unfolded ss prem(4)] 
     proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)  
      next
        case nonspec_mispred
        then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_Fence
        then show ?thesis using stat Δ2 prem(6) unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_normal
        then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_resolve
        then show ?thesis 
          using Δ2 prem(6) resolve_63 
          unfolding ss Δ2_defs using cfgs_map misSpecL1_def apply clarify
          by (smt (z3) insert_commute list.simps(15) resolve.simps)
      next
        case spec_mispred note sm3 = spec_mispred
        show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
          case nonspec_normal
          then show ?thesis using sm3 Δ2 unfolding ss by (simp add: Δ2_defs) 
        next
          case nonspec_mispred
          then show ?thesis using sm3 Δ2 unfolding ss by (simp add: Δ2_defs)
        next
          case spec_resolve
          then show ?thesis using sm3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map) 
        next
          case spec_Fence
          then show ?thesis using sm3 Δ2 unfolding ss apply-apply(frule Δ2_implies)
          by (simp add: Δ2_defs)
        next
          case spec_normal 
          then show ?thesis using sm3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map)
        next
          case spec_mispred note sm4 = spec_mispred
          have pc:"pc4 = 3" 
            using prem(6) lcfgs Δ2 unfolding ss apply-apply(frule Δ2_implies)
             by (simp add: Δ2_defs ) 
          show ?thesis apply(rule oor3I2)
            unfolding ss Δ2'_def using xx_0_cases[of vs3] apply(elim disjE)
            subgoal using Δ2 lcfgs prem pc sm3 sm4 xx finals stat unfolding ss
              apply- apply(simp add: Δ2_defs Δ2'_defs, clarify) 
              apply(intro conjI)
              subgoal by (metis config.sel(2) last_in_set state.sel(1,2) vstore.sel final_def)
              subgoal by (metis config.sel(2) last_in_set state.sel(2))
              subgoal by (metis config.sel(2) last_in_set state.sel(2))
              subgoal by (metis config.sel(2) last_in_set state.sel(2))
              subgoal by (smt (verit) prem(1) prem(2) ss3 ss4)
              subgoal by (metis config.sel(2) last_in_set state.sel(1) vstore.sel) .
            subgoal using Δ2 lcfgs prem pc sm3 sm4 xx finals stat unfolding ss
              apply- apply(simp add: Δ2_defs Δ2'_defs, clarify) 
              apply(intro conjI)
              subgoal by (metis config.sel(2) last_in_set state.sel(1,2) vstore.sel final_def)
              subgoal by (metis config.sel(2) last_in_set state.sel(2))
              subgoal by (metis config.sel(2) last_in_set state.sel(2))
              subgoal by (metis config.sel(2) last_in_set state.sel(2))
              subgoal by (smt (verit) prem(1) prem(2) ss3 ss4)
              subgoal by (metis config.sel(2) last_in_set state.sel(1) vstore.sel) . .
          qed
        qed
        (*¬mispred *)
     subgoal premises prem using prem(1)[unfolded ss prem(4)] 
     proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)  
      next
        case nonspec_mispred
        then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_Fence
        then show ?thesis using stat Δ2 prem(6) unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_mispred
        then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_resolve
        then show ?thesis 
          using Δ2 prem(6) resolve_63 
          unfolding ss Δ2_defs using cfgs_map misSpecL1_def  apply clarify
          by (smt (z3) insert_commute list.simps(15) resolve.simps)
        next
        case spec_normal note sn3 = spec_normal
        show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
          case nonspec_normal
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs) 
        next
          case nonspec_mispred
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs)
        next
          case spec_Fence
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map) 
        next
          case spec_resolve
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map) 
        next
          case spec_mispred
          then show ?thesis using sn3 Δ2 unfolding ss by (simp add: Δ2_defs, metis last_map) 
        next
          case spec_normal note sn4 = spec_normal
          show ?thesis 
            using Δ2 lcfgs prem sn3 sn4 finals unfolding ss
            apply-apply(frule Δ2_implies) apply clarify
            apply(rule oor3I1, clarsimp)
              using xx_0_cases[of vs3] apply(elim disjE)
                subgoal apply(simp_all add: Δ2_defs) 
                using config.sel(2) last_in_set stat state.sel(1,2) vstore.sel 
                by (smt (verit, ccfv_SIG) Opt.final_def config.sel(1) eval_nat_numeral(3) f3 f4 is_Output_1 le_imp_less_Suc le_refl nat_less_le ss)
                subgoal apply(simp_all add: Δ2_defs, clarify) 
                using config.sel(2) last_in_set stat state.sel(1,2) vstore.sel
                apply(intro conjI,unfold config.sel(1)) 
                subgoal by simp
                subgoal by simp
                subgoal by (metis array_baseSimp)
                subgoal by (metis array_baseSimp)
                subgoal by (metis array_baseSimp)
                subgoal by (metis array_baseSimp)
                subgoal by (smt (verit) cfgs_Suc_zero lcfgs list.set_intros(1))
                subgoal by (smt (verit) cfgs_Suc_zero lcfgs list.set_intros(1))
                subgoal by (smt (z3) Opt.final_def ss3 ss4)
                subgoal by (smt (z3) cfgs_Suc_zero lcfgs3 list.set_intros(1))
                subgoal by (smt (z3) cfgs_Suc_zero lcfgs3 list.set_intros(1))
                subgoal by linarith
                subgoal by linarith
                subgoal by linarith . . 
      qed qed 
      
     subgoal premises prem using prem(1)[unfolded ss prem(4)] 
     proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs)  
      next
        case nonspec_mispred
        then show ?thesis using stat Δ2 unfolding ss by (auto simp add: Δ2_defs) 
      next
        case spec_Fence
        then show ?thesis using stat Δ2 prem unfolding ss by (auto simp add: Δ2_defs) 
      next 
        case spec_mispred
        then show ?thesis using Δ2 prem unfolding ss by auto
      next
        case spec_normal
        then show ?thesis using Δ2 prem unfolding ss by auto
      next
        case spec_resolve note sr3 = spec_resolve
        show ?thesis using prem(2)[unfolded ss prem(5)] proof(cases rule: stepS_cases)
          case nonspec_normal
          then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs)
        next
          case nonspec_mispred
          then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs)
        next
          case spec_normal
          then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs, metis)
        next
          case spec_mispred
          then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs, metis)
        next
          case spec_Fence 
          then show ?thesis using stat Δ2 sr3 unfolding ss by (simp add: Δ2_defs, metis)
        next
          case spec_resolve note sr4 = spec_resolve
          show ?thesis using stat Δ2 prem sr3 sr4 
          unfolding ss lcfgs apply-
          apply(frule Δ2_implies) apply (simp add: Δ2_defs Δ1_defs)
          apply(rule oor3I3, simp add: Δ1_defs)
          by (smt(verit) prem(1) prem(2) ss)
      qed
    qed. . . 
  qed
qed


(* *)

lemma step3: "unwindIntoCond Δ3 (oor Δ3 Δ1)" 
proof(rule unwindIntoCond_simpleI) 
  fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ3: "Δ3 n w1 w2 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 unfolding ss Δ3_def
  apply clarsimp 
  by(frule common_implies, simp)

  have f2:"¬finalN ss2" 
  using Δ3 unfolding ss Δ3_def
  apply clarsimp 
  by(frule common_implies, simp)


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

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

  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

  then have lpc3:"pcOf (last cfgs3) = 6 ∨ 
                  pcOf (last cfgs3) = 7"
    using Δ3 unfolding ss Δ3_defs by simp

  (*because of a spliting on the cases, it's simpler to prove these prior*)
  have sec3[simp]:"¬ isSecO ss3"
    using Δ3 unfolding ss by (simp add: Δ3_defs) 
  have sec4[simp]:"¬ isSecO ss4"
      using Δ3 unfolding ss by (simp add: Δ3_defs)   

    have stat[simp]:"⋀s3' s4' statA'. statA' = sstatA' statA ss3 ss4 ⟹ 
               validTransO (ss3, s3') ⟹ validTransO (ss4, s4') ⟹
               (statA = statA' ∨ statO = Diff)"
    subgoal for ss3' ss4'
      apply (cases ss3, cases ss4, cases ss1, cases ss2)
      apply (cases ss3', cases ss4', clarsimp)
      using Δ3 finals unfolding ss apply clarsimp        
      apply(simp_all add: Δ3_defs sstatA'_def) 
      apply(cases statO, simp_all) by (cases statA, simp_all add: updStat_EqI) .

    have "vs3 xx = vs4 xx" using Δ3 lcfgs unfolding ss Δ3_defs apply clarsimp
      by (metis cfgs_Suc_zero config.sel(2) list.set_intros(1) state.sel(1) vstore.sel)
    
    then have a1x:"(array_loc aa1 (nat (vs4 xx)) avst4) =
                 (array_loc aa1 (nat (vs3 xx)) avst3)"
      using Δ3 lcfgs unfolding ss Δ3_defs array_loc_def apply clarsimp
      by (metis Zero_not_Suc config.sel(2) last_in_set list.size(3) state.sel(2))

    have oor2_rule:"⋀ss3' ss4'. ss3 →S ss3' ⟹ ss4 →S ss4' ⟹
                    (pcOf (last cfgs3) = 6 ⟶ oor Δ3 Δ1 ∞ 1 1 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO) 
                  ∧ (pcOf (last cfgs3) = 7 ⟶ oor Δ3 Δ1 ∞ 0 0 ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO)⟹
                    ∃w1'<w1. ∃w2'<w2. oor Δ3 Δ1 ∞ w1' w2' ss3' ss4' (sstatA' statA ss3 ss4) ss1 ss2 statO"       
      subgoal for ss3' ss4' apply(cases ss3', cases ss4')
        subgoal for pstate3' cfg3' cfgs3' ib3' ls3' 
                    pstate4' cfg4' cfgs4' ib4' ls4' 
        using lpc3 apply(elim disjE)
      (*pc6*)
      subgoal apply(intro exI[of _ 1], intro conjI)
      subgoal using Δ3 unfolding ss Δ3_defs apply clarify
        by (metis enat_ord_simps(4) infinity_ne_i1)
      apply(intro exI[of _ 1], rule conjI)
      subgoal using Δ3 unfolding ss Δ3_defs apply clarify
        by (metis enat_ord_simps(4) infinity_ne_i1)
      by simp
      (*pc7*)
      apply(intro exI[of _ 0], intro conjI)
      subgoal using Δ3 unfolding ss Δ3_defs by (clarify,metis zero_less_one)
      apply(intro exI[of _ 0], rule conjI)
      subgoal using Δ3 unfolding ss Δ3_defs by (clarify,metis zero_less_one) 
      by simp . . 

  show "match (oor Δ3 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposible case since isIntO always holds *)
    show "match1 (oor Δ3 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 (oor Δ3 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
  show "match12 (oor Δ3 Δ1) w1 w2 ss3 ss4 statA ss1 ss2 statO"
      apply(rule match12_simpleI, simp_all, rule disjI1)
    subgoal for ss3' ss4' apply(cases ss3', cases ss4')
        subgoal for pstate3' cfg3' cfgs3' ibT3' ibUT3' ls3' 
                    pstate4' cfg4' cfgs4' ibT4' ibUT4' ls4' 
        apply-apply(rule oor2_rule, assumption+, intro conjI impI)
      (*pc6*)
      subgoal premises prem using prem(1)[unfolded ss prem(4)] 
      proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using stat Δ3 unfolding ss by (auto simp add: Δ3_defs)  
      next
        case nonspec_mispred
        then show ?thesis using stat Δ3 unfolding ss by (auto simp add: Δ3_defs) 
      next
        case spec_mispred
        then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs) 
      next
        case spec_resolve
        then show ?thesis 
          using Δ3 prem(6) resolve_106 
          unfolding ss Δ3_defs by (clarify,metis cfgs_map misSpecL1_def)
      next
        case spec_Fence
        then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs) 
      next
        case spec_normal note sn3 = spec_normal
        show ?thesis
        using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
          case nonspec_normal
          then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss by (simp add: Δ3_defs)
        next
          case nonspec_mispred
          then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss by (simp add: Δ3_defs)
        next
          case spec_mispred
          then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss by (simp add: Δ3_defs, metis config.sel(1) last_map)  
        next
          case spec_Fence
          then show ?thesis using stat Δ3 lcfgs sn3 unfolding ss 
          by (simp add: Δ3_defs, metis config.sel(1) last_map) 
        next
          case spec_resolve
          then show ?thesis using 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 prem(4,5) apply clarify apply- apply(intro conjI)
            subgoal using stat Δ3 lcfgs prem(1,2) sn3 sn4 unfolding ss hh
              apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs) 
            using cases_12[of pc3] apply simp apply(elim disjE)
            apply simp_all by (metis config.sel(2) last_in_set state.sel(2) Dist_ignore a1x )
            subgoal using stat Δ3 lcfgs prem(1,2) sn3 sn4 unfolding ss prem(4,5) hh
            apply- apply(frule Δ3_implies) apply(simp_all add: Δ3_defs)  
            using cases_12[of pc3] apply simp apply(elim disjE)
            apply simp_all 
            by (metis config.collapse config.inject last_in_set state.sel(1) vstore.sel)
            subgoal using stat Δ3 lcfgs prem(1,2) sn3 sn4 unfolding ss prem(4,5) hh
            apply- apply(frule Δ3_implies) by(simp add: Δ3_defs) 
            subgoal using stat Δ3 lcfgs prem(1,2) sn3 sn4 unfolding ss hh 
            apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs) 
            using cases_12[of pc3] apply simp apply(elim disjE)
            by simp_all 
            subgoal using stat Δ3 lcfgs sn3 sn4 unfolding ss hh 
            apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs)  
            using cases_12[of pc3] apply (simp add: array_loc_def) apply(elim disjE)
            by (simp_all add: array_loc_def)
            subgoal using stat Δ3 lcfgs sn3 sn4 unfolding ss hh 
            apply- apply(frule Δ3_implies) apply(simp add: Δ3_defs)  
            using cases_12[of pc3] apply (simp add: array_loc_def) apply(elim disjE)
            by (simp_all add: array_loc_def)
            subgoal using stat Δ3 lcfgs sn3 sn4 unfolding ss hh 
            apply- apply(frule Δ3_implies) by(simp add: Δ3_defs) .
          qed 
      qed
      (*pc7*)
      subgoal premises prem using prem(1)[unfolded ss prem(4)] 
      proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using stat Δ3 unfolding ss by (auto simp add: Δ3_defs)  
      next
        case nonspec_mispred
        then show ?thesis using stat Δ3 unfolding ss by (auto simp add: Δ3_defs) 
      next
        case spec_mispred
        then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs) 
      next
        case spec_resolve
        then show ?thesis using stat Δ3 prem unfolding ss Δ3_defs apply simp
          by (smt (verit,del_insts) cfgs_map empty_set insertCI insert_absorb 
              list.set_map list.simps(15) numeral_eq_iff semiring_norm(87,89) 
              set_ConsD singleton_insert_inj_eq')
      next
        case spec_normal
        then show ?thesis using stat Δ3 prem(6) unfolding ss by (auto simp add: Δ3_defs) 
      next
        case spec_Fence note sf3 = spec_Fence
        show ?thesis
          using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
            case nonspec_normal
            then show ?thesis using stat Δ3 lcfgs sf3 unfolding ss by (simp add: Δ3_defs)
          next
            case nonspec_mispred
            then show ?thesis using stat Δ3 lcfgs sf3 unfolding ss by (simp add: Δ3_defs)
          next
            case spec_mispred
            then show ?thesis using 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 stat Δ3 lcfgs sf3 unfolding ss 
            by (simp add: Δ3_defs) 
          next 
            case spec_normal 
            then show ?thesis using 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_def prem(4,5) apply- apply(clarify,intro conjI)
              subgoal using Δ3 lcfgs prem(1,2) sf3 sf4 unfolding ss hh
              apply- by(simp add: Δ3_defs Δ1_defs, metis ss stat validTransO.simps)   
              subgoal using stat Δ3 lcfgs prem(4,5) sf3 sf4 unfolding ss hh
              apply- apply(frule Δ3_implies) by (simp add: Δ3_defs Δ1_defs)   
              subgoal using stat Δ3 lcfgs prem(4,5) sf3 sf4 unfolding ss hh
              apply- apply(frule Δ3_implies) by (simp add: Δ3_defs Δ1_defs)  
              subgoal using stat Δ3 lcfgs prem(4,5) sf3 sf4 unfolding ss hh 
              apply- apply(frule Δ3_implies) by (simp add: Δ3_defs Δ1_defs) . 
          qed

      qed . . .
    qed
qed


(* *)

lemma step4: "unwindIntoCond Δ1' Δ1" 
proof(rule unwindIntoCond_simpleI) 
  fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ1': "Δ1' n w1 w2 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' unfolding ss Δ1'_def
  apply clarsimp 
  by(frule common_implies, simp)

  have f2:"¬finalN ss2" 
  using Δ1' unfolding ss Δ1'_def
  apply clarsimp 
  by(frule common_implies, simp)


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

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

  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

  have match12_aux:"
 (⋀s1' s2' statA'.
      statA' = sstatA' statA ss3 ss4 ⟹
      validTransO (ss3, s1') ⟹
      validTransO (ss4, s2') ⟹
      Opt.eqAct ss3 ss4 ⟹
      (¬ isSecO ss3 ∧ ¬ isSecO ss4 ∧
       (statA = statA' ∨ statO = Diff) ∧
        Δ1 ∞ 1 1 s1' s2' statA' ss1 ss2 statO))
    ⟹ match12 Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
    apply(rule match12_simpleI, rule disjI1)
    (*the fillibustering *)
    apply(rule exI[of _ 1], rule conjI) 
      subgoal using Δ1'  unfolding ss Δ1'_defs apply clarify
       by(metis enat_ord_simps(4) infinity_ne_i1)
    apply(rule exI[of _ 1], rule conjI)  
      subgoal using Δ1'  unfolding ss Δ1'_defs apply clarify
        by(metis enat_ord_simps(4) infinity_ne_i1)
     by auto 

  show "match Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposible case since isIntO always holds *)
    show "match1 Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 Δ1 w1 w2 ss3 ss4 statA ss1 ss2 statO"
    proof(rule match12_aux,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 Δ1' unfolding ss by (simp add: Δ1'_defs, linarith) 

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

    show stat: "statA = statA' ∨ statO = Diff"

      using v sa Δ1'
      apply (cases ss3, cases ss4, cases ss1, cases ss2)
        apply(cases ss3', cases ss4', clarsimp)
      using v sa Δ1' unfolding ss statA' apply clarsimp        
      apply(simp_all add: Δ1'_defs sstatA'_def) 
      apply(cases statO, simp_all) 
      apply(cases statA, simp_all add: updStat_EqI)
      unfolding finalS_def final_def 
      using One_nat_def less_numeral_extra(4) 
          less_one list.size(3) map_is_Nil_conv 
      by (smt (verit) status.exhaust updStat_diff)

      show "Δ1 ∞ 1 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 Δ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 spec_Fence
          then show ?thesis using sa Δ1' unfolding ss 
            apply (simp add: Δ1'_defs, clarify, elim disjE)
            by (simp_all add: Δ1_defs Δ1'_defs)
        next
          case spec_mispred
          then show ?thesis using sa Δ1' unfolding ss 
            apply (simp add: Δ1'_defs, clarify, elim disjE)
            by (simp_all add: Δ1_defs Δ1'_defs)
        next
          case spec_normal note sn3 = spec_normal
          show ?thesis using Δ1' sn3(2) unfolding ss 
            apply (simp add: Δ1'_defs, clarsimp)
            by (smt (z3) insert_commute)
        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 Δ1' sr3 unfolding ss by (simp add: Δ1'_defs)
          next
            case nonspec_mispred
            then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs)
          next
            case spec_mispred
            then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs, metis) 
          next
            case spec_normal
            then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs, metis)
          next 
            case spec_Fence  
            then show ?thesis using Δ1' sr3 unfolding ss by (simp add: Δ1'_defs, metis) 
          next 
            case spec_resolve note sr4 = spec_resolve
            show ?thesis
            using sa stat Δ1'  v3 v4 sr3 sr4 unfolding ss hh
            apply(simp add: Δ1'_defs Δ1_defs)  
            by (metis atLeastAtMost_iff atLeastatMost_empty_iff empty_iff empty_set 
                      nat_le_linear numeral_le_iff semiring_norm(68,69,72)
                      length_1_butlast length_map in_set_butlastD)
          qed 
        qed
      qed
    qed
  qed
  

(* *)

lemma step5: "unwindIntoCond Δ2' Δ2" 
proof(rule unwindIntoCond_simpleI) 
  fix n w1 w2 ss3 ss4 statA ss1 ss2 statO
  assume r: "reachO ss3" "reachO ss4" "reachV ss1" "reachV ss2"
  and Δ2': "Δ2' n w1 w2 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 Δ2' unfolding ss Δ2'_def
  apply clarsimp 
  by(frule common_implies, simp)

  have f2:"¬finalN ss2" 
  using Δ2' unfolding ss Δ2'_def
  apply clarsimp 
  by(frule common_implies, simp)


  have f3:"¬finalS ss3" 
    using Δ2' unfolding ss 
    apply-apply(frule Δ2'_implies)
    using finalS_while_spec_L2 by force

  have f4:"¬finalS ss4" 
    using Δ2' unfolding ss 
    apply-apply(frule Δ2'_implies)
    using finalS_while_spec_L2 by force

  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

  (*because of a spliting on the cases, it's simpler to prove these prior*)
  have sec3[simp]:"¬ isSecO ss3"
    using Δ2' unfolding ss by (simp add: Δ2'_defs) 
  have sec4[simp]:"¬ isSecO ss4"
      using Δ2' unfolding ss by (simp add: Δ2'_defs)   

    have stat[simp]:"⋀s3' s4' statA'. statA' = sstatA' statA ss3 ss4 ⟹ 
               validTransO (ss3, s3') ⟹ validTransO (ss4, s4') ⟹
               (statA = statA' ∨ statO = Diff)"
    subgoal for ss3' ss4'
      apply (cases ss3, cases ss4, cases ss1, cases ss2)
        apply(cases ss3', cases ss4', clarsimp)
      using Δ2' finals unfolding ss apply clarsimp        
      apply(simp_all add: Δ2'_defs sstatA'_def) 
      apply(cases statO, simp_all) by (cases statA, simp_all add: updStat_EqI) .

  have match12_aux:"
 (⋀pstate3' cfg3' cfgs3' ib3' ibUT3' ls3' 
    pstate4' cfg4' cfgs4' ib4' ibUT4' ls4' statA'.
      (pstate3, cfg3, cfgs3, ibT3, ibUT3, ls3) →S (pstate3', cfg3', cfgs3', ib3', ibUT3', ls3') ⟹
      (pstate4, cfg4, cfgs4, ibT4, ibUT4, ls4) →S (pstate4', cfg4', cfgs4', ib4', ibUT4', ls4') ⟹
      Opt.eqAct ss3 ss4 ⟹ statA' = sstatA' statA ss3 ss4 ⟹
      (Δ2 ∞ 1 1 (pstate3', cfg3', cfgs3', ib3', ibUT3', ls3') (pstate4', cfg4', cfgs4', ib4', ibUT4', ls4') statA' ss1 ss2 statO))
    ⟹ match12 Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
    apply(rule match12_simpleI, simp_all, rule disjI1)
    (*the fillibustering *)
    apply(rule exI[of _ 1], rule conjI) 
      subgoal using Δ2'  unfolding ss Δ2'_defs apply clarify
        by (metis one_less_numeral_iff semiring_norm(76))
    apply(rule exI[of _ 1], rule conjI)  
      subgoal using Δ2'  unfolding ss Δ2'_defs apply clarify
        by (metis one_less_numeral_iff semiring_norm(76))
    subgoal for ss3' ss4' apply(cases ss3', cases ss4')
      subgoal for pstate3' cfg3' cfgs3' ib3' ibUT3' ls3' 
                  pstate4' cfg4' cfgs4' ib4' ibUT4' ls4' 
        using ss3 ss4 by blast . .

  show "match Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
  unfolding match_def proof(intro conjI)
    (* match1 and match2 are imposible case since isIntO always holds *)
    show "match1 Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match1_def by (simp add: finalS_def final_def)
    show "match2 Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO"
    unfolding match2_def by (simp add: finalS_def final_def)
    show "match12 Δ2 w1 w2 ss3 ss4 statA ss1 ss2 statO" 
    apply(rule match12_aux)
    (* Choose the match12_12 case (since we have no mis-speculation yet) *)
    subgoal premises prem using prem(1)[unfolded ss] 
      proof(cases rule: stepS_cases)
        case nonspec_normal
        then show ?thesis using stat Δ2' unfolding ss by (auto simp add: Δ2'_defs)  
      next
        case nonspec_mispred
        then show ?thesis using stat Δ2' unfolding ss by (auto simp add: Δ2'_defs) 
      next
        case spec_mispred
        then show ?thesis using stat Δ2' prem unfolding ss by (auto simp add: Δ2'_defs) 
      next
        case spec_normal
        then show ?thesis using stat Δ2' prem unfolding ss by (auto simp add: Δ2'_defs) 
      next
        case spec_Fence
        then show ?thesis using stat Δ2' prem unfolding ss by (auto simp add: Δ2'_defs) 
      next
        case spec_resolve note sr3 = spec_resolve
        show ?thesis using prem(2)[unfolded ss prem] proof(cases rule: stepS_cases)
            case nonspec_normal
            then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs)
          next
            case nonspec_mispred
            then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs)
          next
            case spec_mispred
            then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs) 
          next
            case spec_normal
            then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs)
          next 
            case spec_Fence  
            then show ?thesis using stat Δ2' sr3 unfolding ss by (simp add: Δ2'_defs) 
          next 
            case spec_resolve note sr4 = spec_resolve
            show ?thesis
            using stat Δ2' prem sr3 sr4 unfolding ss 
            apply(simp add: Δ2'_defs Δ2_defs)  
            apply(intro conjI)
            apply (metis last_map map_butlast map_is_Nil_conv)
            apply (metis image_subset_iff in_set_butlastD)
            apply(metis) apply(metis) apply (metis in_set_butlastD) 
            apply (metis in_set_butlastD) apply (metis in_set_butlastD)
            apply (metis in_set_butlastD) apply (metis prem(1) prem(2) ss3 ss4)
            apply (metis in_set_butlastD) apply (metis in_set_butlastD)
            apply (smt (verit, del_insts) butlast.simps(2) last_ConsL last_map 
                      list.simps(8) map_L2 map_butlast not_Cons_self2)
             apply clarify apply(elim disjE)
             using butlast.simps(2) insertCI last_ConsL last_map 
                 list.simps(15) list.simps(8) map_L2 map_butlast not_Cons_self2 
                 resolve.simps resolve_106 
             apply metis  
             using butlast.simps(2) insertCI last_ConsL last_map 
                 list.simps(15) list.simps(8) map_L2 map_butlast not_Cons_self2 
                 resolve.simps resolve_106 apply metis 
             using  butlast.simps(2) last.simps map_L2 
                 map_butlast map_is_Nil_conv neq_Nil_conv nth_Cons_0 
                 resolve_611 resolve_63 resolve_64 
             by (metis last_map list.simps(15)) 
        qed
      qed .    
  qed
qed

(**)

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

  then show "isIntO ss3 = isIntO ss4" by simp

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

lemmas theConds = step0 step1 step2 step3 step4 step5 stepe

proposition lrsecure
proof-
  define m where m: "m ≡ (7::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 Δ1'
  else if i = 5 then Δ2'
  else Δe" 
  define nxt where nxt: "nxt ≡ λi::nat. 
  if i = 0 then {0,1::nat}
  else if i = 1 then {1,4,2,3,6}  
  else if i = 2 then {2,5,1} 
  else if i = 3 then {3,1}  
  else if i = 4 then {1}
  else if i = 5 then {2} 
  else {6}"
  show ?thesis apply(rule distrib_unwind_lrsecure[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 oor3_def oor4_def oor5_def by auto . 
qed


end