Theory Decision_NCPC

theory Decision_NCPC
imports "../Observation_Setup" Decision_Value_Setup "Bounded_Deducibility_Security.Compositional_Reasoning"
begin

subsection ‹Confidentiality protection from non-PC-members›

text ‹We verify the following property:

\ \\
A group of users UIDs learn
nothing about the various updates of a paper's decision
except for the last edited version
unless/until
a user in UIDs becomes PC member in the paper's conference having no conflict with that paper
and the conference moves to the decision stage.

\ \\
›

(* perhaps this should further strengthened *)

fun T :: "(state,act,out) trans ⇒ bool" where
"T (Trans _ _ ou s') =
 (∃ uid ∈ UIDs. ∃ cid.
    PID ∈∈ paperIDs s' cid ∧ isPC s' cid uid ∧ pref s' uid PID ≠ Conflict ∧
    phase s' cid ≥ disPH
 )"

declare T.simps [simp del]

definition B :: "value list ⇒ value list ⇒ bool" where
"B vl vl1 ≡ vl ≠ [] ∧ vl1 ≠ [] ∧ last vl = last vl1"

interpretation BD_Security_IO where
istate = istate and step = step and
φ = φ and f = f and γ = γ and g = g and T = T and B = B
done

lemma reachNT_non_isPC_isChair:
assumes "reachNT s" and "uid ∈ UIDs"
shows
"(PID ∈∈ paperIDs s cid ∧ isPC s cid uid ∧ phase s cid ≥ disPH ⟶ pref s uid PID = Conflict) ∧
 (PID ∈∈ paperIDs s cid ∧ isChair s cid uid ∧ phase s cid ≥ disPH ⟶ pref s uid PID = Conflict)"
  using assms
  apply induct
   apply (auto simp: istate_def)[]
  apply(intro conjI)
  subgoal for trn apply(cases trn, auto simp: T.simps reachNT_reach)[] .
  by (metis T.elims(3) isChair_isPC reachNT_reach reach.Step tgtOf_simps)

(* important: *) lemma T_φ_γ:
assumes 1: "reachNT s" and 2: "step s a = (ou,s')" "φ (Trans s a ou s')"
shows "¬ γ (Trans s a ou s')"
using reachNT_non_isPC_isChair[OF 1] 2 unfolding T.simps φ_def2
by (fastforce simp add: uu_defs)

lemma eqExcPID2_eqExcPID:
"eqExcPID2 s s1 ⟹ eqExcPID s s1"
unfolding eqExcPID_def eqExcPID2_def eeqExcPID_def eeqExcPID2_def eqExcD2 eqExcD by auto

(* major *) lemma eqExcPID_step_out:
assumes s's1': "eqExcPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and sT: "reachNT s" and s1: "reach s1"
and PID: "PID ∈∈ paperIDs s cid"
and ph: "phase s cid = disPH"
and UIDs: "userOfA a ∈ UIDs"
shows "ou = ou1"
proof-
  note Inv = reachNT_non_isPC_isChair[OF sT UIDs]
  note eqs = eqExcPID_imp[OF s's1']
  note eqs' = eqExcPID_imp1[OF s's1']
  note s = reachNT_reach[OF sT]

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID_def eeqExcPID_def eqExcD
  note * = step step1 eqs eqs' s s1 PID UIDs ph paperIDs_equals[OF s] Inv

  show ?thesis
  proof (cases a)
    case (Cact x1)
    then show ?thesis using * by (cases x1) auto
  next
    case (Uact x2)
    then show ?thesis using * by (cases x2) auto
  next
    case (UUact x3)
    then show ?thesis using * by (cases x3) auto
  next
    case (Ract x4)
    show ?thesis
    proof (cases x4)
      case (rMyReview x81 x82 x83 x84)
      then show ?thesis using * Ract by (auto simp add: getNthReview_def)
    next
      case (rReviews x91 x92 x93 x94)
      then show ?thesis using * Ract by (clarsimp; metis eqExcPID_imp2 s's1')
    next
      case (rDecs x101 x102 x103 x104)
      then show ?thesis using * Ract by (clarsimp; metis)
    next
      case (rFinalDec x131 x132 x133 x134)
      then show ?thesis using * Ract by (clarsimp; metis Suc_n_not_le_n)
    qed (use * Ract in auto)
  next
    case (Lact x5)
    then show ?thesis using * by (cases x5; auto; presburger)
  qed
qed

(* major *) lemma eqExcPID2_step_out:
assumes ss1: "eqExcPID2 s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and sT: "reachNT s" and s1: "reach s1"
and PID: "PID ∈∈ paperIDs s cid"
and ph: "phase s cid ≥ disPH"
and UIDs: "userOfA a ∈ UIDs"
and decs_exit: "decsPaper (paper s PID) ≠ []" "decsPaper (paper s1 PID) ≠ []"
shows "ou = ou1"
proof-
  note Inv = reachNT_non_isPC_isChair[OF sT UIDs]
  note eqs = eqExcPID2_imp[OF ss1]
  note eqs' = eqExcPID2_imp1[OF ss1]
  note s = reachNT_reach[OF sT]

  have "PID ∈∈ paperIDs s1 cid" using PID ss1 unfolding eqExcPID2_def by auto
  hence decs_exit': "decsPaper (paper s' PID) ≠ []" "decsPaper (paper s1' PID) ≠ []"
  using nonempty_decsPaper_persist s s1 PID decs_exit step step1 by metis+

  note simps[simp] = c_defs u_defs uu_defs r_defs l_defs Paper_dest_conv eqExcPID2_def eeqExcPID2_def eqExcD2
  note * = step step1 eqs eqs' s s1 PID UIDs ph paperIDs_equals[OF s] Inv

  show ?thesis
  proof (cases a)
    case (Cact x1)
    then show ?thesis using * by (cases x1) auto
  next
    case (Uact x2)
    then show ?thesis using * by (cases x2) auto
  next
    case (UUact x3)
    then show ?thesis using * by (cases x3) auto
  next
    case (Ract x4)
    show ?thesis
    proof (cases x4)
      case (rMyReview x81 x82 x83 x84)
      then show ?thesis using * Ract by (auto simp add: getNthReview_def)
    next
      case (rReviews x91 x92 x93 x94)
      then show ?thesis using * Ract by (clarsimp; metis eqExcPID2_imp2 ss1)
    next
      case (rDecs x101 x102 x103 x104)
      then show ?thesis using * Ract by (clarsimp; metis)
    next
      case (rFinalDec x131 x132 x133 x134)
      then show ?thesis using * Ract by (clarsimp; metis decs_exit' list.sel(1) list.simps(5) neq_Nil_conv)
    qed (use * Ract in auto)
  next
    case (Lact x5)
    then show ?thesis using * by (cases x5; auto; presburger)
  qed
qed

lemma eqExcPID_step_eqExcPID2:
assumes a: "a = UUact (uuDec cid uid p PID dec)"
and ss1: "eqExcPID s s1"
and step: "step s a = (outOK,s')" and step1: "step s1 a = (outOK,s1')"
and s: "reach s" "reach s1" and PID: "PID ∈∈ paperIDs s cid" and ph: "phase s cid < notifPH"
shows "eqExcPID2 s' s1'"
proof-
  have "eqExcPID s' s1'" using assms by (metis eqExcPID_step)
  moreover have "hd (decsPaper (paper s' PID)) = hd (decsPaper (paper s1' PID))"
    using step step1 unfolding a
    apply(simp add: uu_defs)
    by (metis decsPaper.simps fun_upd_same list.sel(1) select_convs(8) surjective update_convs(8))
  ultimately show ?thesis
    unfolding eqExcPID_def eqExcPID2_def eeqExcPID_def eeqExcPID2_def eqExcD2 eqExcD by auto
qed

(* major *) lemma eqExcPID_step_φ_eqExcPID2:
assumes ss1: "eqExcPID s s1"
and step: "step s a = (ou,s')" and step1: "step s1 a = (ou1,s1')"
and φ: "φ (Trans s a ou s')"
and s: "reach s" "reach s1" and PID: "PID ∈∈ paperIDs s cid" and ph: "phase s cid ≤ disPH"
shows "eqExcPID2 s' s1'"
proof-
  obtain cid1 uid p dec where a: "a = UUact (uuDec cid1 uid p PID dec)" and ou: "ou = outOK"
  using φ unfolding φ_def2 by auto
  have PID1: "PID ∈∈ paperIDs s cid1" using step unfolding a ou by (auto simp: uu_defs)
  hence cid1: "cid1 = cid" using paperIDs_equals[OF s(1) PID] by auto
  have φ1: "φ (Trans s1 a ou1 s1')" using φ ss1 by (metis eqExcPID_step_φ_imp step step1)
  hence ou1: "ou1 = outOK" using φ unfolding φ_def2 by auto
  show ?thesis
  using eqExcPID_step_eqExcPID2[OF a ss1 step[unfolded ou] step1[unfolded ou1] s]
  PID ph unfolding cid1 by auto
qed

definition Δ1 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ1 s vl s1 vl1 ≡
 (∀ cid. PID ∈∈ paperIDs s cid ⟶ phase s cid < disPH) ∧
 s = s1 ∧ B vl vl1"
(* "Critical phase not yet reached: either PID not yet registered
    or the phase of its conference not yet submission  " *)

definition Δ2 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ2 s vl s1 vl1 ≡
 ∃ cid uid.
   PID ∈∈ paperIDs s cid ∧ phase s cid = disPH ∧
   isChair s cid uid ∧ pref s uid PID ≠ Conflict ∧
   eqExcPID s s1 ∧ B vl vl1"
(* "PID registered to a conference which is in the discussion phase, values not completely flushed,
    state equality only up to the decision for PID which is a singleton list;
    assumption that there exists at least a non-conflict chair of the conference
    (the situation when no such chair exists is covered by Δe,
    since then vl cannot be flushed)" *)

definition Δ3 :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δ3 s vl s1 vl1 ≡
 ∃ cid.
   PID ∈∈ paperIDs s cid ∧ phase s cid ≥ disPH ∧
   decsPaper (paper s PID) ≠ [] ∧ decsPaper (paper s1 PID) ≠ [] ∧ eqExcPID2 s s1 ∧
   vl = [] ∧ vl1 = []"
(* "During or after discussion, values flushed,
    state equality a bit tighter: up to the tail of the decision list (so strict equality on the head,
    which is the only thing a potential author may see);
    the list of decisions also have to be nonempty in order
    for eqExcPID2 to be preserved by transitions" *)

definition Δe :: "state ⇒ value list ⇒ state ⇒ value list ⇒ bool" where
"Δe s vl s1 vl1 ≡
 vl ≠ [] ∧
 ((∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid > disPH)
  ∨
  (∃ cid. PID ∈∈ paperIDs s cid ∧ phase s cid ≥ disPH ∧
          ¬ (∃ uid. isChair s cid uid ∧ pref s uid PID ≠ Conflict))
 )"

lemma istate_Δ1:
assumes B: "B vl vl1"
shows "Δ1 istate vl istate vl1"
using B unfolding Δ1_def B_def istate_def by auto

lemma unwind_cont_Δ1: "unwind_cont Δ1 {Δ1,Δ2,Δe}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ1 s vl s1 vl1 ∨ Δ2 s vl s1 vl1 ∨ Δe s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ1 s vl s1 vl1"
  hence rs: "reach s" and ss1: "s1 = s"
  and vl: "vl ≠ []" and vl1: "vl1 ≠ []" and vl_vl1: "last vl1 = last vl"
  and ph_PID: "⋀ cid. PID ∈∈ paperIDs s cid ⟹ phase s cid < disPH"
  using reachNT_reach unfolding Δ1_def B_def by auto
  note vlvl1 = vl vl1 vl_vl1
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"  let ?trn1 = "Trans s1 a ou s'"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      have φ: "¬ φ ?trn"
      proof (cases a)
        case (UUact x3)
        then show ?thesis
          using step ph_PID
          by (cases x3; fastforce simp: uu_defs)
      qed auto
      hence vl': "vl' = vl" using c unfolding consume_def by auto
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have ?match proof
          show "validTrans ?trn1" unfolding ss1 using step by simp
        next
          show "consume ?trn1 vl1 vl1" unfolding consume_def ss1 using φ by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1" unfolding ss1 by simp
        next
          show "?Δ s' vl' s' vl1"
          proof(cases "∃ cid. PID ∈∈ paperIDs s cid")
            case False note PID = False
            have ph_PID': "⋀ cid. PID ∈∈ paperIDs s' cid ⟹ phase s' cid < disPH" using PID step rs
            apply(cases a)
              subgoal for _ x1 apply(cases x1) apply(fastforce simp: c_defs)+ .
              subgoal for _ x2 apply(cases x2) apply(fastforce simp: u_defs)+ .
              subgoal for _ x3 apply(cases x3) apply(fastforce simp: uu_defs)+ .
              by auto
            hence "Δ1 s' vl' s' vl1" unfolding Δ1_def B_def vl' using ph_PID' vlvl1 by auto
            thus ?thesis by auto
          next
            case True
            then obtain CID where PID: "PID ∈∈ paperIDs s CID" by auto
            hence ph: "phase s CID < disPH" using ph_PID by auto
            have PID': "PID ∈∈ paperIDs s' CID" by (metis PID paperIDs_mono step)
            show ?thesis
            proof(cases "phase s' CID < disPH")
              case True note ph' = True
              hence "Δ1 s' vl' s' vl1" unfolding Δ1_def B_def vl' using vlvl1 ph' PID'
                by (auto; metis reach_PairI paperIDs_equals rs step)
              thus ?thesis by auto
            next
              case False note ph' = False
              hence ph': "phase s' CID = disPH" using ph PID step rs
              apply(cases a)
                subgoal for x1 apply(cases x1) apply(fastforce simp: c_defs)+ .
                subgoal for x2 apply(cases x2) apply(fastforce simp: u_defs)+ .
                subgoal for x3 apply(cases x3) apply(fastforce simp: uu_defs)+ .
              by auto
              show ?thesis
              proof(cases "∃uid. isChair s' CID uid ∧ pref s' uid PID ≠ Conflict")
                case True
                hence "Δ2 s' vl' s' vl1" unfolding Δ2_def B_def vl' using vlvl1 ph' PID' by auto
                thus ?thesis by auto
              next
                case False
                hence "Δe s' vl' s' vl1" unfolding Δe_def vl' using vlvl1 ph' PID' by auto
                thus ?thesis by auto
              qed
            qed
          qed
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl by auto
  qed
qed

lemma unwind_cont_Δ2: "unwind_cont Δ2 {Δ2,Δ3,Δe}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ2 s vl s1 vl1 ∨ Δ3 s vl s1 vl1 ∨ Δe s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ2 s vl s1 vl1"
  then obtain CID uid where uid: "isChair s CID uid" "pref s uid PID ≠ Conflict"
  and rs: "reach s" and ph: "phase s CID = disPH" (is "?ph = _")
  and PID: "PID ∈∈ paperIDs s CID" and ss1: "eqExcPID s s1"
  and vl: "vl ≠ []" and vl1: "vl1 ≠ []" and vl_vl1: "last vl = last vl1"
  using reachNT_reach unfolding Δ2_def B_def by auto
  note vlvl1 = vl vl1 vl_vl1
  from vl vl1 obtain v vl' v1 vl1' where vl: "vl = v # vl'" and vl1: "vl1 = v1 # vl1'" by (metis list.exhaust)
  have uid_notin: "uid ∉ UIDs"
  using ph uid reachNT_non_isPC_isChair[OF rsT] PID by fastforce
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof(cases "vl1' = []")
    case False note vl1' = False
    hence vl_vl1': "last vl = last vl1'" using vl_vl1 unfolding vl1 by simp
    have uid1: "isChair s1 CID uid" "pref s1 uid PID ≠ Conflict" using ss1 uid unfolding eqExcPID_def by auto
    define a1 where "a1 ≡ UUact (uuDec CID uid (pass s uid) PID v1)"
    obtain s1' ou1 where step1: "step s1 a1 = (ou1,s1')" by (metis prod.exhaust)
    let ?trn1 = "Trans s1 a1 ou1 s1'"
    have s1s1': "eqExcPID s1 s1'" using a1_def step1 UUact_uuDec_step_eqExcPID by auto
    have ss1': "eqExcPID s s1'" using eqExcPID_trans[OF ss1 s1s1'] .
    hence many_s1': "PID ∈∈ paperIDs s1' CID" "isChair s1' CID uid"
    "pref s1' uid PID ≠ Conflict" "phase s1' CID = disPH"
    "pass s1' uid = pass s uid"
    using uid PID ph unfolding eqExcPID_def by auto
    hence more_s1': "uid ∈∈ userIDs s1'" "CID ∈∈ confIDs s1'"
    by (metis paperIDs_confIDs reach_PairI roles_userIDs rs1 step1 many_s1'(1))+
    have f: "f ?trn1 = v1" unfolding a1_def by simp
    have rs1': "reach s1'" using rs1 step1 by (auto intro: reach_PairI)
    have ou1: "ou1 = outOK"
    using step1 uid1 ph unfolding a1_def by (auto simp add: uu_defs many_s1' more_s1')
    have ?iact proof
      show "step s1 a1 = (ou1,s1')" by fact
    next
      show φ: "φ ?trn1" using ou1 unfolding a1_def by simp
      thus "consume ?trn1 vl1 vl1'" using f unfolding consume_def vl1 by simp
    next
      show "¬ γ ?trn1" by (simp add: a1_def uid_notin)
    next
      have "Δ2 s vl s1' vl1'" unfolding Δ2_def B_def using ph PID ss1' uid vl_vl1' vl1' vl by auto
      thus "?Δ s vl s1' vl1'" by simp
    qed
    thus ?thesis by auto
  next
    case True hence vl1: "vl1 = [v1]" unfolding vl1 by simp
    have ?react proof
      fix a :: act and ou :: out and s' :: state and vll'
      let ?trn = "Trans s a ou s'"
      let ?ph' = "phase s' CID"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vll'"
      have PID': "PID ∈∈ paperIDs s' CID" using PID rs by (metis paperIDs_mono step)
      have uid': "isChair s' CID uid ∧ pref s' uid PID ≠ Conflict"
      using uid step rs ph PID pref_Conflict_disPH isChair_persistent by auto
      show "match ?Δ s s1 vl1 a ou s' vll' ∨ ignore ?Δ s s1 vl1 a ou s' vll'" (is "?match ∨ ?ignore")
      proof(cases "φ ?trn")
        case False note φ = False
        have vll': "vll' = vl" using c φ unfolding consume_def by (cases vl) auto
        obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust)
        let ?trn1 = "Trans s1 a ou1 s1'"
        have s's1': "eqExcPID s' s1'" using eqExcPID_step[OF ss1 step] step1 rs rs1 PID ph by auto
        have φ1: "¬ φ ?trn1" using φ unfolding eqExcPID_step_φ[OF ss1 step step1] .
        have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 vl1" unfolding consume_def using φ1 by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1"
          using eqExcPID_step_out[OF ss1 step step1 rsT rs1 PID ph] by simp
 (* note that in this setting eqExcPID_step_out needs the additional phase assumption *)
        next
          show "?Δ s' vll' s1' vl1"
          proof(cases "?ph' = disPH")
            case True
            hence "Δ2 s' vll' s1' vl1" using PID' s's1' uid' vlvl1 unfolding Δ2_def B_def vll' by auto
            thus ?thesis by auto
          next
            case False hence "?ph' > disPH" using ph rs step by (metis le_less phase_increases)
            hence "Δe s' vll' s1' vl1" unfolding Δe_def vll' using vlvl1 PID' by auto
            thus ?thesis by auto
          qed
        qed
        thus ?thesis by simp
      next
        case True note φ = True
        hence vll': "vll' = vl'" using c unfolding vl consume_def by simp
        obtain cid uid p where a: "a = UUact (uuDec cid uid p PID v)" and ou: "ou = outOK"
        using φ c PID unfolding vl consume_def φ_def2 vll' by fastforce
        (* hence cid: "cid = CID" using step PID rs by (auto simp add: uu_defs paperIDs_equals) *)
        hence γ: "¬ γ ?trn" using step T rsT by (metis T_φ_γ True)
        hence f: "f ?trn = v" using c φ unfolding consume_def vl by auto
        have s's: "eqExcPID s' s" using eqExcPID_sym[OF φ_step_eqExcPID[OF φ step]] .
        have s's1: "eqExcPID s' s1" using eqExcPID_trans[OF s's ss1] .
        have ph': "phase s' CID = disPH" using s's ph unfolding eqExcPID_def by auto
        show ?thesis
        proof(cases "vl' = []")
          case False note vl' = False
          hence vl'_vl1: "last vl' = last vl1" using vl_vl1 unfolding vl by auto
          have ?ignore proof
            show "¬ γ ?trn" by fact
          next
            show "?Δ s' vll' s1 vl1"
            proof(cases "?ph' = disPH")
              case True
              hence "Δ2 s' vll' s1 vl1" using s's1 PID' uid' vl' vl1 vl_vl1 unfolding Δ2_def B_def vl vll' by auto
              thus ?thesis by auto
            next
              case False hence "?ph' > disPH" using ph rs step by (metis le_less phase_increases)
              hence "Δe s' vll' s1 vl1" unfolding Δe_def vll' using vlvl1 vl' PID' by auto
              thus ?thesis by auto
            qed
          qed
          thus ?thesis by auto
        next
          case True note vl' = True hence vl: "vl = [v]" unfolding vl by simp
(* the transition to Δ3: φ holds and both vl and vl1 are singletons: *)
          hence v1v: "v1 = v" using vl_vl1 unfolding vl1 by simp
          obtain s1' ou1 where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust)
          let ?trn1 = "Trans s1 a ou1 s1'"
          have φ1: "φ ?trn1" using eqExcPID_step_φ_imp[OF ss1 step step1 φ] .
          hence ou1: "ou1 = outOK" unfolding φ_def2 by auto
          have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 []" unfolding consume_def using φ1 by (simp add: a vl1 v1v)
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1"
          using eqExcPID_step_out[OF ss1 step step1 rsT rs1 PID ph] by simp
        next
          have "Δ3 s' vll' s1' []" unfolding vll' vl' Δ3_def
          using PID' ph' eqExcPID_step_φ_eqExcPID2[OF ss1 step step1 φ rs rs1 PID] ph
          using step step1 unfolding a by (auto simp: uu_defs ou ou1)
          thus "?Δ s' vll' s1' []" by simp
        qed
        thus ?thesis by simp
        qed
      qed
    qed
    thus ?thesis using vl by auto
  qed
qed

lemma unwind_cont_Δ3: "unwind_cont Δ3 {Δ3,Δe}"
proof(rule, simp)
  let ?Δ = "λs vl s1 vl1. Δ3 s vl s1 vl1 ∨ Δe s vl s1 vl1"
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and "Δ3 s vl s1 vl1"
  then obtain CID where rs: "reach s" and ph: "phase s CID ≥ disPH" (is "?ph ≥ _")
  and PID: "PID ∈∈ paperIDs s CID"
  and decs: "decsPaper (paper s PID) ≠ []"  "decsPaper (paper s1 PID) ≠ []"
  and ss1: "eqExcPID2 s s1" and vl: "vl = []" and vl1: "vl1 = []"
  using reachNT_reach unfolding Δ3_def by auto
  show "iaction ?Δ s vl s1 vl1 ∨
        ((vl = [] ⟶ vl1 = []) ∧ reaction ?Δ s vl s1 vl1)" (is "?iact ∨ (_ ∧ ?react)")
  proof-
    have "?react"
    proof
      fix a :: act and ou :: out and s' :: state and vl'
      let ?trn = "Trans s a ou s'"
      let ?ph' = "phase s' CID"
      assume step: "step s a = (ou, s')" and T: "¬ T ?trn" and c: "consume ?trn vl vl'"
      have PID': "PID ∈∈ paperIDs s' CID" using PID rs by (metis paperIDs_mono step)
      have ph': "phase s' CID ≥ disPH" using ph rs step by (meson dual_order.trans phase_increases)
      show "match ?Δ s s1 vl1 a ou s' vl' ∨ ignore ?Δ s s1 vl1 a ou s' vl'" (is "?match ∨ ?ignore")
      proof-
        have φ: "¬ φ ?trn" and vl': "vl' = []" using c unfolding consume_def vl by auto
        obtain ou1 and s1' where step1: "step s1 a = (ou1,s1')" by (metis prod.exhaust)
        let ?trn1 = "Trans s1 a ou1 s1'"
        have s's1': "eqExcPID2 s' s1'" using eqExcPID2_step[OF ss1 step step1] .
        have φ1: "¬ φ ?trn1" using φ unfolding eqExcPID2_step_φ[OF ss1 step step1] .
        have PID1: "PID ∈∈ paperIDs s1 CID" using PID ss1 unfolding eqExcPID2_def by auto
        have decs': "decsPaper (paper s' PID) ≠ []"  "decsPaper (paper s1' PID) ≠ []"
        by (metis PID PID1 decs nonempty_decsPaper_persist rs step rs1 step1)+
        have ?match proof
          show "validTrans ?trn1" using step1 by simp
        next
          show "consume ?trn1 vl1 vl1" unfolding consume_def using φ1 by auto
        next
          show "γ ?trn = γ ?trn1" unfolding ss1 by simp
        next
          assume "γ ?trn" thus "g ?trn = g ?trn1"
          using eqExcPID2_step_out[OF ss1 step step1 rsT rs1 PID ph _ decs] by simp
        next
          have "Δ3 s' vl' s1' vl1" using ph' PID' s's1' unfolding Δ3_def vl1 vl' by (auto simp: decs')
          thus "?Δ s' vl' s1' vl1" by simp
        qed
        thus ?thesis by simp
      qed
    qed
    thus ?thesis using vl1 by simp
  qed
qed

(* Exit arguments: *)
definition K1exit where
"K1exit cid s ≡
 phase s cid ≥ disPH ∧ PID ∈∈ paperIDs s cid ∧ ¬ (∃ uid. isChair s cid uid ∧ pref s uid PID ≠ Conflict)"

lemma invarNT_K1exit: "invarNT (K1exit cid)"
unfolding invarNT_def apply (safe dest!: reachNT_reach)
  subgoal for _ a apply(cases a)
    subgoal for x1 apply(cases x1)
      apply (fastforce simp add: c_defs K1exit_def geq_noPH_confIDs)+ .
    subgoal for x2 apply(cases x2)
            apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
           apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
          apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
         apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
        apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)
      subgoal for x61 apply(cases "x61 = cid")
         apply (fastforce simp add: u_defs K1exit_def paperIDs_equals)+ .
      apply (fastforce simp add: u_defs K1exit_def paperIDs_equals) .
    subgoal for x3 apply(cases x3) apply (fastforce simp add: uu_defs K1exit_def)+ .
    apply (fastforce simp add: uu_defs K1exit_def)+ .
done

lemma noVal_K1exit: "noVal (K1exit cid) v"
apply(rule noφ_noVal)
unfolding noφ_def apply safe
  subgoal for _ a apply(cases a)
        apply (fastforce simp add: c_defs K1exit_def)
       apply (fastforce simp add: c_defs K1exit_def)
    subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs K1exit_def)
      apply (metis paperIDs_equals reachNT_reach) (* safety used *) .
    by auto
done

definition K2exit where
"K2exit cid s ≡ PID ∈∈ paperIDs s cid ∧ phase s cid > disPH"

lemma invarNT_K2exit: "invarNT (K2exit cid)"
unfolding invarNT_def apply (safe dest!: reachNT_reach)
  subgoal for _ a apply(cases a)
    subgoal for x1 apply(cases x1)
      apply (fastforce simp add: c_defs K2exit_def geq_noPH_confIDs)+ .
    subgoal for x2 apply(cases x2)
      apply (fastforce simp add: u_defs K2exit_def paperIDs_equals)+ .
    subgoal for x3 apply(cases x3) apply (fastforce simp add: uu_defs K2exit_def)+ .
    apply (fastforce simp add: uu_defs K2exit_def)+ .
done

lemma noVal_K2exit: "noVal (K2exit cid) v"
apply(rule noφ_noVal)
unfolding noφ_def apply safe
  subgoal for _ a apply(cases a)
        apply (fastforce simp add: c_defs K2exit_def)
       apply (fastforce simp add: c_defs K2exit_def)
    subgoal for x3 apply(cases x3) apply (auto simp add: uu_defs K2exit_def)
      using paperIDs_equals reachNT_reach apply fastforce (* safety used *) .
  by auto
done

lemma unwind_exit_Δe: "unwind_exit Δe"
proof
  fix s s1 :: state and vl vl1 :: "value list"
  assume rsT: "reachNT s" and rs1: "reach s1" and Δe: "Δe s vl s1 vl1"
  hence vl: "vl ≠ []" using reachNT_reach unfolding Δe_def by auto
  then obtain CID where "K1exit CID s ∨ K2exit CID s" using Δe unfolding K1exit_def K2exit_def Δe_def by auto
  thus "vl ≠ [] ∧ exit s (hd vl)" apply(simp add: vl)
  by (metis rsT exitI2 invarNT_K1exit noVal_K1exit invarNT_K2exit noVal_K2exit)
qed

theorem secure: secure
apply(rule unwind_decomp3_secure[of Δ1 Δ2 Δe Δ3])
using
istate_Δ1
unwind_cont_Δ1 unwind_cont_Δ2 unwind_cont_Δ3
unwind_exit_Δe
by auto


end