Theory Traceback_Properties

theory Traceback_Properties
imports Safety_Properties
begin


section ‹Traceback properties›

text ‹In this section, we prove various traceback properties,
by essentially giving trace-based justifications of certain
occurring situations that are relevant for access to information:
%
\begin{description}
\item{\bf Being an author. }
If a user is an author of a paper, then either the user has registered the paper in the first
place or, inductively, has been appointed as coauthor by another author.
%
\item{\bf Being a chair. }
If a user is a chair of a conference, then either that user has registered the conference
which has been approved by the superuser or, inductively, that user has been appointed
by an existing chair of that conference.
%
%
\item{\bf Being a PC member. }
If a user is a PC member in a conference, then the user either must have been the original chair or must
have been appointed by a chair.
%
\item{\bf Being a reviewer. }
If a user is a paper's reviewer, then the user must have been appointed by a chair (from
among the PC members who have not declared a conflict with the paper).
%
\item{\bf Having conflict. }
If a user has conflict with a paper, then the user is either an author of the paper or the
conflict has been declared by that user or by a paper's author, in such a way that between
the moment when the conflict has been last declared and the current moment there is no
transition that successfully removes the conflict.
%
\item{\bf Conference reaching a phase. }
If a conference is in a given phase different from ``no phase'', then this has happened as
a consequence of either a conference approval action by the superuser (if the phase is
Setup) or a phase change action by a chair (otherwise).
\end{description}

More details and explanations can be found in cite‹Section 3.6› in "cocon-JAR2021".
›


subsection ‹Preliminaries›

inductive trace_between :: "state  (state,act,out) trans trace  state  bool" where
  empty[simp]: "trace_between s [] s"
| step: "trace_between s tr sh; step sh a = (ou,s')  trace_between s (tr@[Trans sh a ou s']) s'"

inductive_simps
  trace_ft_empty[simp]: "trace_between s [] s'" and
  trace_ft_snoc: "trace_between s (tr@[trn]) s'"
thm trace_ft_empty trace_ft_snoc

lemma trace_ft_append: "trace_between s (tr1@tr2) s'
   (sh. trace_between s tr1 sh  trace_between sh tr2 s')"
  apply (induction tr2 arbitrary: s' rule: rev_induct)
   apply simp
  apply (subst append_assoc[symmetric], subst trace_ft_snoc)
  apply (auto simp: trace_ft_snoc)
  done

lemma trace_ft_Cons: "trace_between s (trn#tr) s'
   (sh ou a. trn = Trans s a ou sh  step s a = (ou,sh)  trace_between sh tr s')"
  apply (subst trace_ft_append[where ?tr1.0 = "[trn]", simplified])
  apply (subst trace_ft_snoc[where tr = "[]", simplified])
  by auto

lemmas trace_ft_simps = trace_ft_empty trace_ft_snoc trace_ft_Cons trace_ft_append

inductive trace_to :: " (state,act,out) trans trace  state  bool" where
  empty: "trace_to [] istate"
| step: "trace_to tr s; step s a = (ou,s')  trace_to (tr@[Trans s a ou s']) s'"

lemma trace_to_ft: "trace_to tr s  trace_between istate tr s"
proof (rule,goal_cases)
  case 1 thus ?case
    by induction (auto intro: trace_between.intros)
next
  case 2
  moreover
  {fix s' assume "trace_between s' tr s" hence "s' = istate  trace_to tr s"
   by induction (auto intro: trace_to.intros)
  }
  ultimately show ?case by auto
qed

inductive_simps trace_to_empty[simp]: "trace_to [] s"

lemma trace_to_reach: assumes "trace_to tr s" shows "reach s"
  using assms apply induction
   apply (rule reach.intros)
  by (metis reach_step snd_conv)

lemma reach_to_trace: assumes "reach s" obtains tr where "trace_to tr s"
  using assms apply (induction rule: reach_step_induct)
   apply (auto intro: trace_to.intros) []
  by (metis surjective_pairing trace_to.step)

lemma reach_trace_to_conv: "reach s  (tr. trace_to tr s)"
  by (blast intro: trace_to_reach elim: reach_to_trace)

thm trace_to.induct[no_vars]

lemma trace_to_induct[case_names empty step, induct set]:
  "trace_to x1 x2; P [] istate;
  tr s a ou s'.
    trace_to tr s; P tr s; reach s; reach s'; step s a = (ou, s')
     P (tr ## Trans s a ou s') s'
   P x1 x2"
  apply (erule trace_to.induct)
   apply simp
  apply (frule trace_to_reach)
  using reach_PairI by blast



subsection ‹Authorship›

text ‹
  Only the creator of a paper, and users explicitly added by other authors,
  are authors of a paper.
›

inductive isAut' :: "(state,act,out) trans trace  confID  userID  paperID  bool" where
  creator: " trn = Trans _ (Cact (cPaper cid uid _ pid _ _)) outOK _ 
     isAut' (tr@[trn]) cid uid pid"
  (* "The creator of a paper is an author"  *)
| co_author: "
  isAut' tr cid uid' pid;
  trn = Trans _ (Cact (cAuthor cid uid' _ pid uid)) outOK _ 
   isAut' (tr@[trn]) cid uid pid"
  (* "An author can add any other user as a coauthor" *)
| irrelevant: "isAut' tr cid uid' pid  isAut' (tr@[_]) cid uid' pid"

lemma justify_author:
  assumes "trace_to tr s"
  assumes "isAut s cid uid pid"
  shows "isAut' tr cid uid pid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def)
next
  case (step tr s a ou s')
  show ?case
  proof (cases "isAut s cid uid pid")
    case True with step.IH show ?thesis by (blast intro: isAut'.intros)
  next
    case False
    with step.hyps step.prems obtain
      pass s1 s2 uid' where
      "a=Cact (cPaper cid uid pass pid s1 s2)
       (a=Cact (cAuthor cid uid' pass pid uid)  isAut s cid uid' pid)"
      and [simp]: "ou=outOK"
      apply (cases a)
        subgoal for x1 apply (cases x1, auto simp add: c_defs) [] .
        subgoal for x2 apply (cases x2, auto simp add: u_defs) [] .
        subgoal for x3 apply (cases x3, auto simp add: uu_defs) [] .
        by simp_all
    thus ?thesis using step.IH
      apply (elim disjE)
      apply (rule isAut'.creator, auto) []
      apply (rule isAut'.co_author, auto) []
      done
  qed
qed


lemma author_justify:
  assumes "trace_to tr s"
  assumes "isAut' tr cid uid pid"
  shows "isAut s cid uid pid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim: isAut'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case (creator _ _ pass s1 s2)
    hence [simp]: "a=Cact (cPaper cid uid pass pid s1 s2)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (co_author _ uid' _ _ pass)
    hence [simp]: "a=Cact (cAuthor cid uid' pass pid uid)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (irrelevant) with step.IH have AUT: "isAut s cid uid pid" by simp

    note roles_confIDs[OF reach s AUT]
    with AUT step s a = (ou, s') show ?thesis
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
  qed
qed

theorem isAut_eq: "trace_to tr s  isAut s cid uid pid  isAut' tr cid uid pid"
  (* "Trace-based equivalent of authorship" *)
  using justify_author author_justify
  by (blast)


subsection ‹Becoming a Conference Chair›

inductive isChair' :: "(state,act,out) trans trace  confID  userID  bool" where
  creator: " trn=Trans _ (Cact (cConf cid uid _ _ _)) outOK _ 
     isChair' (tr@[trn]) cid uid"
| add_chair: " isChair' tr cid uid'; trn = Trans _ (Cact (cChair cid uid' _ uid)) outOK _ 
   isChair' (tr@[trn]) cid uid"
| irrelevant: "isChair' tr cid uid  isChair' (tr@[_]) cid uid"

lemma justify_chair:
  assumes "trace_to tr s"
  assumes "isChair s cid uid"
  shows "isChair' tr cid uid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def)
next
  case (step tr s a ou s')
  show ?case
  proof (cases "isChair s cid uid")
    case True with step.IH show ?thesis by (blast intro: isChair'.intros)
  next
    case False
    term cConf
    with step.hyps step.prems obtain
      pass s1 s2 uid' where
      "a=Cact (cConf cid uid pass s1 s2)
       (a=Cact (cChair cid uid' pass uid)  isChair s cid uid')"
      and [simp]: "ou=outOK"
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp add: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp add: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp add: uu_defs) [] .
      by simp_all
    thus ?thesis using step.IH
      apply (elim disjE)
      apply (rule isChair'.creator, auto) []
      apply (rule isChair'.add_chair, auto) []
      done
  qed
qed

lemma chair_justify:
  assumes "trace_to tr s"
  assumes "isChair' tr cid uid"
  shows "isChair s cid uid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim: isChair'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case (creator _ _ pass s1 s2)
    hence [simp]: "a=Cact (cConf cid uid pass s1 s2)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (add_chair _ uid' _ _ pass)
    hence [simp]: "a=Cact (cChair cid uid' pass uid)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (irrelevant) with step.IH have CH: "isChair s cid uid" by simp

    from CH step s a = (ou, s') show ?thesis
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
  qed
qed

theorem isChair_eq: "trace_to tr s  isChair s cid uid = isChair' tr cid uid"
  (* "Trace-based equivalent of being a chair" *)
  using justify_chair chair_justify
  by (blast)


subsection ‹Committee Membership›

inductive isPC' :: "(state,act,out) trans trace  confID  userID  bool" where
  chair: "isChair' tr cid uid  isPC' tr cid uid"
| add_com: " isChair' tr cid uid'; trn = Trans _ (Cact (cPC cid uid' _ uid)) outOK _ 
   isPC' (tr@[trn]) cid uid"
| irrelevant: "isPC' tr cid uid  isPC' (tr@[_]) cid uid"

lemma justify_com:
  assumes "trace_to tr s"
  assumes "isPC s cid uid"
  shows "isPC' tr cid uid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def)
next
  case (step tr s a ou s')

  show ?case
  proof (cases "isPC s cid uid")
    case True with step.IH show ?thesis by (blast intro: isPC'.irrelevant)
  next
    case False note noPC = this
    show ?thesis proof (cases "isChair s' cid uid")
      case True thus ?thesis
        by (metis chair justify_chair step.hyps(1) step.hyps(4) trace_to.step)
    next
      case False note noChair=this
      from noPC noChair step.hyps step.prems obtain
        pass uid' where "(a=Cact (cPC cid uid' pass uid))"
        and "isChair s cid uid'"
        and [simp]: "ou=outOK"
        apply (cases a)
        subgoal for x1 apply (cases x1, auto simp add: c_defs) [] .
        subgoal for x2 apply (cases x2, auto simp add: u_defs) [] .
        subgoal for x3 apply (cases x3, auto simp add: uu_defs) [] .
        by simp_all
      thus ?thesis
        apply -
        apply (rule isPC'.add_com, auto simp: isChair_eq[OF trace_to tr s]) []
        done
    qed
  qed
qed

lemma com_justify:
  assumes "trace_to tr s"
  assumes "isPC' tr cid uid"
  shows "isPC s cid uid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim!: isPC'.cases isChair'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case chair thus ?thesis
      by (metis isChair_eq isChair_isPC step.hyps(1) step.hyps(3) step.hyps(4) trace_to.step)
  next
    case (add_com _ uid' _ _ pass)
    hence [simp]: "a=Cact (cPC cid uid' pass uid)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs)
  next
    case (irrelevant) with step.IH have COM: "isPC s cid uid" by simp

    from COM step s a = (ou, s') show ?thesis
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
  qed
qed

theorem isPC_eq: "trace_to tr s  isPC s cid uid = isPC' tr cid uid"
  (* "Trace-based equivalent of committee membership" *)
  using justify_com com_justify
  by (blast)


subsection ‹Being a Reviewer›

inductive isRev' :: "(state,act,out) trans trace  confID  userID  paperID  bool" where
  add_rev: " isChair' tr cid uid'; trn = Trans _ (Cact (cReview cid uid' _ pid uid)) outOK _ 
   isRev' (tr@[trn]) cid uid pid"
| irrelevant: "isRev' tr cid uid pid  isRev' (tr@[_]) cid uid pid"

lemma justify_rev:
  assumes "trace_to tr s"
  assumes "isRev s cid uid pid"
  shows "isRev' tr cid uid pid"
  using assms
proof (induction)
  case empty thus ?case
    by (auto simp add: istate_def isRev_def)
next
  case (step tr s a ou s')

  show ?case
  proof (cases "isRev s cid uid pid")
    case True with step.IH show ?thesis by (blast intro: isRev'.irrelevant)
  next
    case False note noRev = this
    with step.hyps step.prems obtain
      pass uid' where "(a=Cact (cReview cid uid' pass pid uid))"
      and "isChair s cid uid'"
      and [simp]: "ou=outOK"
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp add: c_defs isRev_def) [] .
      subgoal for x2 apply (cases x2, auto simp add: u_defs isRev_def) [] .
      subgoal for x3 apply (cases x3, auto simp add: uu_defs isRev_def) [] .
      by simp_all
    thus ?thesis
      apply -
      apply (rule isRev'.add_rev, auto simp: isChair_eq[OF trace_to tr s]) []
      done
  qed
qed

lemma rev_justify:
  assumes "trace_to tr s"
  assumes "isRev' tr cid uid pid"
  shows "isRev s cid uid pid"
  using assms
proof (induction arbitrary: uid)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim!: isRev'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case (add_rev _ uid' _ _ pass)
    hence [simp]: "a=Cact (cReview cid uid' pass pid uid)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: c_defs isRev_def)
  next
    case (irrelevant) with step.IH have REV: "isRev s cid uid pid" by simp

    note roles_confIDs[OF step.hyps(2)]
    with REV step s a = (ou, s') show ?thesis
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs isRev_def) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs isRev_def) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs isRev_def) [] .
      by simp_all
  qed
qed

theorem isRev_eq: "trace_to tr s  isRev s cid uid pid = isRev' tr cid uid pid"
  (* "Trace-based equivalent of being a reviewer" *)
  using justify_rev rev_justify
  by (blast)



subsection "Conflicts"

fun irrev_conflict :: "userID  paperID  (state,act,out) trans  bool"
 (* "Transitions causing irrevokable conflicts" *)
where
  "irrev_conflict uid pid (Trans _ (Cact (cPaper _ uid' _ pid' _ _)) outOK _)
     uid'=uid  pid'=pid"
| "irrev_conflict uid pid (Trans _ (Cact (cAuthor _ _ _ pid' uid')) outOK _)
     uid'=uid  pid'=pid"
| "irrev_conflict uid pid _  False"

fun set_conflict :: "userID  paperID  (state,act,out) trans  bool"
  (* "Transitions setting conflict state, can be revoked by later reset-actions" *)
  where
  "set_conflict uid pid (Trans _ (Cact (cConflict _ _ _ pid' uid')) outOK _)
     uid'=uid  pid'=pid"
| "set_conflict uid pid (Trans _ (Uact (uPref _ uid' _ pid' Conflict)) outOK _)
     uid'=uid  pid'=pid"
| "set_conflict _ _ _  False"

fun reset_conflict :: "userID  paperID  (state,act,out)trans  bool"
  (* "Transitions re-setting conflict state, can be revoked by later set-actions" *)
  where
  "reset_conflict uid pid (Trans _ (Uact (uPref _ uid' _ pid' pr)) outOK _)
     uid'=uid  pid'=pid  prConflict"
| "reset_conflict _ _ _  False"

definition conflict_trace :: "userID  paperID  (state,act,out) trans trace  bool"
  (* "Trace that causes a conflict: It contains either an irrevokable conflict action,
    or the last action concerning conflicts was set-conflict" *)
  where
  "conflict_trace uid pid tr 
  (trnset tr. irrev_conflict uid pid trn)
 (tr1 trn tr2. tr=tr1@trn#tr2 
    set_conflict uid pid trn  (trnset tr2. ¬reset_conflict uid pid trn))"

lemma irrev_conflict_impl_author:
  assumes "trace_to tr s"
  assumes "trnset tr. irrev_conflict uid pid trn"
  shows "cid. isAut s cid uid pid"
  using assms
  apply induction
  apply (auto simp add: istate_def) []
  subgoal for _ _ a apply (cases a)
    subgoal for x1 apply (cases x1, auto simp: c_defs, (metis roles_confIDs)+) [] .
    subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
    subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
    by simp_all
  done

lemma irrev_conflict_impl_conflict:
  assumes "trace_to tr s"
  assumes "trnset tr. irrev_conflict uid pid trn"
  shows "pref s uid pid = Conflict"
  by (metis assms(1) assms(2) irrev_conflict_impl_author
    isAut_pref_Conflict reach_trace_to_conv)

lemma conflict_justify:
  assumes TR: "trace_to tr s"
  assumes "conflict_trace uid pid tr"
  shows "pref s uid pid = Conflict"
  using assms(2)
  unfolding conflict_trace_def
proof (cases rule: disjE[consumes 1, case_names irrev set])
  case irrev thus ?thesis by (simp add: irrev_conflict_impl_conflict[OF TR])
next
  case set
  then obtain tr1 trn tr2 where
    [simp]: "tr = tr1 @ trn # tr2" and
    SET: "set_conflict uid pid trn"
    and NRESET: "trnset tr2. ¬ reset_conflict uid pid trn"
    by blast

  from TR obtain s1 s2 a ou where
    [simp]: "trn = Trans s1 a ou s2" and
    TR1: "trace_to tr1 s1" and
    STEP: "step s1 a = (ou,s2)" and
    TR2: "trace_between s2 tr2 s"
    by (fastforce simp add: trace_to_ft trace_ft_simps)

  from STEP SET have "pref s2 uid pid = Conflict"
    apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) []
        subgoal for _ x65 apply (cases x65, auto) [] .
        subgoal for _ _ _ x65 apply (cases x65, auto) [] .
        subgoal for _ _ _ x65 apply (cases x65, auto) [] . .
      by simp_all

  with TR2 NRESET show ?thesis
    apply induction
    subgoal by simp
    subgoal for _ _ _ a apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
    done
qed

lemma justify_conflict:
  assumes TR: "trace_to tr s"
  assumes "pref s uid pid = Conflict"
  shows "conflict_trace uid pid tr"
  using assms
proof induction
  case empty thus ?case by (auto simp add: istate_def)
next
  case (step tr s a ou s')

  let ?trn = "Trans s a ou s'"

  show ?case proof (cases "pref s uid pid = Conflict")
    case False
    with step.prems step s a = (ou, s')
    have "irrev_conflict uid pid ?trn  set_conflict uid pid ?trn"
      apply (cases a)
      subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
      subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
      subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
      by simp_all
    thus ?thesis
      unfolding conflict_trace_def by fastforce
  next
    case True with step.IH have CT: "conflict_trace uid pid tr" .

    from step.prems step s a = (ou, s') have "¬reset_conflict uid pid ?trn"
      apply (cases a)
      subgoal by simp
      subgoal for x2 by (cases x2, auto simp: u_defs)
      by simp_all

    thus ?thesis using CT
      unfolding conflict_trace_def
      apply clarsimp
      by (metis rotate1.simps(2) set_ConsD set_rotate1)

  qed
qed

theorem conflict_eq:
  assumes "trace_to tr s"
  shows "pref s uid pid = Conflict  conflict_trace uid pid tr"
  using assms conflict_justify justify_conflict by auto


subsection ‹Conference Phases›

fun is_uPhase where
  "is_uPhase cid (Trans _ (Uact (uConfA cid' _ _)) outOK _)  cid'=cid"
| "is_uPhase cid (Trans _ (Uact (uPhase cid' _ _ _)) outOK _)  cid'=cid"
| "is_uPhase _ _  False"

inductive phase' :: "(state,act,out) trans trace  confID  nat  bool" where
  initial: "phase' [] cid noPH"
| approve: "phase' tr cid noPH; trn=Trans s (Uact (uConfA cid (voronkov s) _)) outOK _ 
   phase' (tr@[trn]) cid setPH"
| advance: "trn = (Trans _ (Uact (uPhase cid uid _ ph)) outOK _); isChair' tr cid uid
   phase' (tr@[trn]) cid ph"
| irrelevant: "phase' tr cid ph; ¬is_uPhase cid trn   phase' (tr@[trn]) cid ph"

lemma justify_phase:
  assumes "trace_to tr s"
  assumes "phase s cid = ph"
  shows "phase' tr cid ph"
  using assms
proof (induction arbitrary: ph)
  case (empty s) thus ?case
    by (auto simp add: istate_def phase'.initial)
next
  case (step tr s a ou s')
  thus ?case
    apply (cases a)
    subgoal for x1 apply (cases x1, auto simp: c_defs intro: phase'.advance phase'.irrelevant) [] .
    subgoal for x2 apply (cases x2,
      auto
        simp: u_defs isChair_eq
        intro: phase'.advance phase'.irrelevant phase'.approve,
      (fastforce intro: phase'.approve phase'.irrelevant phase'.advance)+
    ) [] .

    subgoal for x3 apply (cases x3, auto simp: uu_defs intro: phase'.irrelevant) [] .
    by (auto intro: phase'.advance phase'.irrelevant)
qed

lemma phase_justify:
  assumes "trace_to tr s"
  assumes "phase' tr cid ph"
  shows "phase s cid = ph"
  using assms
proof (induction arbitrary: ph)
  case (empty s) thus ?case
    by (auto simp add: istate_def elim: phase'.cases)
next
  case (step tr s a ou s')
  from step.prems
  show ?case
  proof (cases)
    case (approve _ _ _ pass _)
    hence [simp]: "a=Uact (uConfA cid (voronkov s) pass)" "ou=outOK" "ph=setPH" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: u_defs)
  next
    case (advance _ _ uid pass _ _)
    hence [simp]: "a=Uact (uPhase cid uid pass ph)" "ou=outOK" by simp_all
    from step.hyps show ?thesis
      by (auto simp add: u_defs)
  next
    case (irrelevant) with step.IH have PH: "phase s cid = ph" "¬ is_uPhase cid (Trans s a ou s')"
      by simp_all

    from PH step s a = (ou, s') show ?thesis
    apply (cases a)
    subgoal for x1 apply (cases x1, auto simp: c_defs) [] .
    subgoal for x2 apply (cases x2, auto simp: u_defs) [] .
    subgoal for x3 apply (cases x3, auto simp: uu_defs) [] .
    by simp_all
  qed auto
qed

theorem phase_eq:
  assumes "trace_to tr s"
  shows "phase s cid = ph  phase' tr cid ph"
  using assms phase_justify justify_phase by blast

end