Theory System_Specification

section ‹System specification›

text ‹This section formalizes the CoCon system as an I/O automaton.
We call the inputs ``actions''.›

theory System_Specification
imports Prelim
begin

subsection ‹System state›


text ‹The superuser of the system is called ``voronkov'',
as a form acknowledgement for our inspiration from EasyChair
when creating CoCon.
›

record state =
  confIDs :: "confID list"
  conf :: "confID  conf"
  (*  *)
  userIDs :: "userID list"
  pass :: "userID  password"
  user :: "userID  user"
  roles :: "confID  userID  role list"
  (*  *)
  paperIDs :: "confID  paperID list"
  paper :: "paperID  paper"
  (*  *)
  pref :: "userID  paperID  preference" (* preference, including eventual conflicts *)
  (*  *)
  voronkov :: "userID"
  (*  *)
  news :: "confID  string list"
  phase :: "confID  phase" (* the current phase *)
  (*  *)


(* Note: Some of the fields are redundant, e.g., paperIDs can in principle be recovered from "roles";
however, this and other redundant fields are used very often, so it is efficient to keep them *)


(* Various discriminators ("is") and selectors ("get") on the database: *)
abbreviation isPC :: "state  confID  userID  bool" (*  program committee (PC) membership *) where
"isPC s confID uID  PC ∈∈ roles s confID uID"
abbreviation isChair :: "state  confID  userID  bool" (* being one of the conference chairs *)  where
"isChair s confID uID  Chair ∈∈ roles s confID uID"
abbreviation isAut :: "state  confID  userID  paperID  bool" (*  authorship of a certain paper *) where
"isAut s confID uID papID  Aut papID ∈∈ roles s confID uID"
definition isAutSome :: "state  confID  userID  bool" (*  authorship of some paper *) where
"isAutSome s confID uID  list_ex (isAut s confID uID) (paperIDs s confID)"
(* all the authors of a given paper: *)
definition authors :: "state  confID  paperID  userID list" where
"authors s confID papID  filter (λ uID. isAut s confID uID papID) (userIDs s)"
abbreviation isRevNth :: "state  confID  userID  paperID  nat  bool" (*  paper reviewer (nth review) *)
where
"isRevNth s confID uID papID n  Rev papID n ∈∈ roles s confID uID"
definition isRev :: "state  confID  userID  paperID  bool" (*  paper reviewer *) where
"isRev s confID uID papID  list_ex (isRevRoleFor papID) (roles s confID uID)"
(* Get the reviewer role for a certain triple (user, conference, paper), if any: *)
definition getRevRole :: "state  confID  userID  paperID  role option" where
"getRevRole s confID uID papID  List.find (isRevRoleFor papID) (roles s confID uID)"
(* get the n-th review of a paper *)
definition getNthReview :: "state  paperID  nat  review" where
"getNthReview s papID n  (reviewsPaper (paper s papID))!n"
(* get all the paper IDs (for all conferences) from the system: *)
definition getAllPaperIDs :: "state  paperID list" where
"getAllPaperIDs s  concat [paperIDs s confID. confID  confIDs s]"
definition getReviewIndex :: "state  confID  userID  paperID  nat" where
"getReviewIndex s confID uID papID 
 case getRevRole s confID uID papID of Some (Rev papID' n)  n"
(* get, for a conference and a paper, the reviews together with the IDs of the reviewers: *)
definition getReviewersReviews :: "state  confID  paperID  (userID * review) list" where
"getReviewersReviews s confID papID 
 [(uID, getNthReview s papID (getReviewIndex s confID uID papID)).
    uID  userIDs s,
    isRev s confID uID papID
 ]"

(* Not used in the implementation: *)
definition isAUT :: "state  userID  paperID  bool" where
"isAUT s uID papID   confID. isAut s confID uID papID"
definition isREVNth :: "state  userID  paperID  nat  bool" where
"isREVNth s uID papID n   confID. isRevNth s confID uID papID n"


lemma isRev_getRevRole:
assumes "isRev s confID uID papID"
shows "getRevRole s confID uID papID  None"
using assms list_ex_find unfolding isRev_def getRevRole_def by auto

lemma getRevRole_Some:
assumes "getRevRole s confID uID papID = Some role"
shows " n. role = Rev papID n"
using assms unfolding getRevRole_def unfolding find_Some_iff apply (cases role, auto)
by (metis isRevRoleFor.simps)+

lemma isRev_getRevRole2:
assumes "isRev s confID uID papID"shows " n. getRevRole s confID uID papID = Some (Rev papID n)"
using assms getRevRole_Some by (cases "getRevRole s confID uID papID") (auto simp: isRev_getRevRole)

lemma isRev_imp_isRevNth_getReviewIndex:
assumes "isRev s confID uID papID"
shows "isRevNth s confID uID papID (getReviewIndex s confID uID papID)"
proof-
  obtain n where 1: "getRevRole s confID uID papID = Some (Rev papID n)"
  using isRev_getRevRole2[OF assms] by auto
  hence "isRevNth s confID uID papID n"
  unfolding getRevRole_def unfolding find_Some_iff by auto
  moreover have "getReviewIndex s confID uID papID = n" using 1 unfolding getReviewIndex_def by simp
  ultimately show ?thesis by auto
qed

(* nonexecutable, but more useful version of the definition: *)
lemma isRev_def2:
"isRev s confID uID papID  ( n. isRevNth s confID uID papID n)" (is "?A  ?B")
proof
  assume ?A thus ?B using isRev_imp_isRevNth_getReviewIndex by blast
next
  assume ?B thus ?A unfolding isRev_def list_ex_iff by force
qed

(* more precise definition, but not always needed: *)
lemma isRev_def3:
"isRev s confID uID papID  isRevNth s confID uID papID (getReviewIndex s confID uID papID)"
by (metis isRev_def2 isRev_imp_isRevNth_getReviewIndex)

lemma getFreshPaperID_getAllPaperIDs[simp]:
  assumes "confID ∈∈ confIDs s"
  shows "¬ getFreshPaperID (getAllPaperIDs s) ∈∈ paperIDs s confID"
  using assms getFreshPaperID[of "getAllPaperIDs s"]
  by (auto simp: getAllPaperIDs_def)

lemma getRevRole_Some_Rev:
"getRevRole s cid uid pid = Some (Rev pid' n)  pid' = pid"
by (metis getRevRole_Some role.inject)

lemma getRevRole_Some_Rev_isRevNth:
"getRevRole s cid uid pid = Some (Rev pid' n)  isRevNth s cid uid pid n"
  unfolding getRevRole_def find_Some_iff
  apply (elim exE)
  subgoal for i
    apply(cases "roles s cid uid ! i")
       apply auto
    by (metis nth_mem)
  done

(* This assumes that the list of conference IDs has exactly one element: *)
definition IDsOK :: "state  confID list  userID list  paperID list  bool"
where
"IDsOK s cIDs uIDs papIDs 
 list_all (λ confID. confID ∈∈ confIDs s) cIDs 
 list_all (λ uID. uID ∈∈ userIDs s) uIDs 
 list_all (λ papID. papID ∈∈ paperIDs s (hd cIDs)) papIDs"


subsection ‹The actions›

subsubsection‹Initialization of the system›

definition istate :: state
where
"istate 
 
  confIDs = [],
  conf = (λ confID. emptyConf),
  userIDs = [voronkovUserID],
  pass = (λ uID. emptyPass),
  user = (λ uID. emptyUser),
  roles = (λ confID uID. []),
  paperIDs = (λ confID. []),
  paper = (λ papID. emptyPaper),
  pref = (λ uID papID. NoPref),
  voronkov = voronkovUserID,
  news = (λ confID. []),
  phase = (λ confID. noPH)
 "



subsubsection‹Actions unbound by any existing conference (with its phases)›

(* Create new user (user) in the system: *)
(* if given user ID already taken, generate a fresh one *)
definition createUser ::  "state  userID  password  string  string  string  state"
where
"createUser s uID p name info email 
 let uIDs = userIDs s
 in
 s userIDs := uID # uIDs,
    user := (user s) (uID := User name info email),
    pass := (pass s) (uID := p)"
(* the the web interface, one should prompt the user multiple times for entering
 an unused ID *)

definition e_createUser :: "state  userID  password  string  string  string  bool" where
"e_createUser s uID p name info email 
 ¬ uID ∈∈ userIDs s"

(* updates information for user (himself), including password: *)
definition updateUser :: "state  userID  password  password  string  string  string  state"
where
"updateUser s uID p p' name info email 
 s user := (user s) (uID := User name info email),
    pass := (pass s) (uID := p')"

definition e_updateUser :: "state  userID  password  password  string  string  string  bool"
where
"e_updateUser s uID p p' name info email 
 IDsOK s [] [uID] []  pass s uID = p"


(* read if the current user is the voronkov: *)
definition readAmIVoronkov :: "state  userID  password  bool"
where
"readAmIVoronkov s uID p 
 uID = voronkov s "

definition e_readAmIVoronkov :: "state  userID  password  bool"
where
"e_readAmIVoronkov s uID p 
 IDsOK s [] [uID] []  pass s uID = p"

(* Read the name and info of a user (except for password): *)
(* There are several needs for this primitive action:
   -- either I read my own info
   -- or I am an author, and therefore I read the PC members' name and info to declare a conflict
   -- or I am a chair, and therefore I read all PC members's info to assign papers for reviewing
   -- or I am an author and need to add coauthors
*)
definition readUser :: "state  userID  password  userID  string * string * string"
where
"readUser s uID p uID' 
 case user s uID' of User name info email  (name, info, email)"

definition e_readUser :: "state  userID  password  userID  bool"
where
"e_readUser s uID p uID' 
 IDsOK s [] [uID,uID'] []  pass s uID = p"

(* Request for a new conference *)

(* The request takes place by creating a new conference with ID assigned as above for users.
The conference will remain in the default "noPH" phase until aproval.
The creator becomes a chair (a fortiori a PC member). *)
definition createConf :: "state  confID  userID  password  string  string  state"
where
"createConf s confID uID p name info 
 let confIDs = confIDs s
 in
 s confIDs := confID # confIDs,
    conf := (conf s) (confID := Conf name info),
    roles := fun_upd2 (roles s) confID uID [PC,Chair]
   "
(* again, in the web interface the user will be prompted repeatedly until he gets it right *)

definition e_createConf :: "state  confID  userID  password  string  string  bool"
where
"e_createConf s confID uID p name info 
 IDsOK s [] [uID] []  pass s uID = p 
 ¬ confID ∈∈ confIDs s"

(* Read the info of a conference: any user can do it  *)
definition readConf :: "state  confID  userID  password  string * string * (role list) * phase"
where
"readConf s confID uID p 
 (nameConf (conf s confID), infoConf (conf s confID),
  [rl  roles s confID uID. ¬ isRevRole rl], phase s confID)"

definition e_readConf :: "state  confID  userID  password  bool"
where
"e_readConf s confID uID p 
 IDsOK s [confID] [uID] []  pass s uID = p"

(* list all conferences: *)
definition listConfs :: "state  userID  password  confID list"
where
"listConfs s uID p 
 confIDs s"

definition e_listConfs :: "state  userID  password  bool"
where
"e_listConfs s uID p 
 IDsOK s [] [uID] []  pass s uID = p 
 uID = voronkov s"

(* list conferences awaiting approval: *)
definition listAConfs :: "state  userID  password  confID list"
where
"listAConfs s uID p 
 [confID. confID  confIDs s, phase s confID = noPH]"

definition e_listAConfs :: "state  userID  password  bool"
where
"e_listAConfs s uID p 
 IDsOK s [] [uID] []  pass s uID = p 
 uID = voronkov s"

(* list conferences in the submission phase: any user can see this *)
definition listSConfs :: "state  userID  password  confID list"
where
"listSConfs s uID p 
 [confID. confID  confIDs s, phase s confID = subPH]"

definition e_listSConfs :: "state  userID  password  bool"
where
"e_listSConfs s uID p 
 IDsOK s [] [uID] []  pass s uID = p"

(* list my conferences: *)
definition listMyConfs :: "state  userID  password  confID list"
where
"listMyConfs s uID p 
 [confID. confID  confIDs s , roles s confID uID  []]"

definition e_listMyConfs :: "state  userID  password  bool"
where
"e_listMyConfs s uID p 
 IDsOK s [] [uID] []  pass s uID = p"

(* list all users of the system (useful when assigning coauthors to papers): *)
definition listAllUsers :: "state  userID  password  userID list"
where
"listAllUsers s uID p 
 userIDs s"

definition e_listAllUsers :: "state  userID  password  bool"
where
"e_listAllUsers s uID p 
 IDsOK s [] [uID] []  pass s uID = p"

(* list all paper IDs of the system (useful whn generating a fresh paper ID): *)
definition listAllPapers :: "state  userID  password  paperID list"
where
"listAllPapers s uID p 
 getAllPaperIDs s"

definition e_listAllPapers :: "state  userID  password  bool"
where
"e_listAllPapers s uID p 
 IDsOK s [] [uID] []  pass s uID = p"


subsubsection‹Actions available in the noPH phase›

(* Approving a new conference should be done by the voronkov, and happens by changing
the phase from noPH to setPH.
This is an update action: it updates the conference approval status
Note that, after approval, the voronkov should not have further access to the conference:
he can only act if the phase is noPH. *)
definition updateConfA :: "state  confID  userID  password  state"
where
"updateConfA s confID uID p 
 s phase := (phase s) (confID := setPH)"

definition e_updateConfA :: "state  confID  userID  password  bool"
where
"e_updateConfA s confID uID p 
 IDsOK s [confID] [uID] []  pass s uID = p 
 uID = voronkov s  phase s confID = noPH"


subsubsection‹Actions available in the setPH phase›

(* make a user a PC member *)
definition createPC :: "state  confID  userID  password  userID  state"
where
"createPC s confID uID p uID' 
 let rls = roles s confID uID'
 in
 s roles := fun_upd2 (roles s) confID uID' (List.insert PC rls)"

definition e_createPC :: "state  confID  userID  password  userID  bool"
where
"e_createPC s confID uID p uID' 
 let uIDs = userIDs s
 in
 IDsOK s [confID] [uID,uID'] []  pass s uID = p 
 phase s confID = setPH  isChair s confID uID"

(* make a user a chair (a fortiori a PC member) *)
definition createChair :: "state  confID  userID  password  userID  state"
where
"createChair s confID uID p uID' 
 let rls = roles s confID uID'
 in
 s roles := fun_upd2 (roles s) confID uID' (List.insert PC (List.insert Chair rls))"

definition e_createChair :: "state  confID  userID  password  userID  bool"
where
"e_createChair s confID uID p uID' 
 let uIDs = userIDs s
 in
 IDsOK s [confID] [uID,uID'] []  pass s uID = p 
 phase s confID = setPH  isChair s confID uID"


subsubsection‹Actions available starting from the setPH phase›

definition updatePhase :: "state  confID  userID  password  phase  state" where
"updatePhase s confID uID p ph 
 s phase := (phase s) (confID := ph)"

definition e_updatePhase :: "state  confID  userID  password  phase  bool" where
"e_updatePhase s confID uID p ph 
 IDsOK s [confID] [uID] []  pass s uID = p 
 phase s confID  setPH  phase s confID < closedPH  isChair s confID uID 
 ph = SucPH (phase s confID)"
(* The phase move is only allowed if the indicated phase is the successor of the current phase.
   Yet, in the kernel we also require the explicit indication of the phase for being able to track
   it for verification.  *)
(* In the web interface, the user is prompted with the question
"Are you sure you want to move to the next phase?" *)

(* Add an event, i.e., undestructively update the news: *)
definition uupdateNews :: "state  confID  userID  password  string  state"
where
"uupdateNews s confID uID p ev 
 let evs = news s confID
 in
 s news := (news s) (confID := ev # evs)"

definition e_uupdateNews :: "state  confID  userID  password  string  bool"
where
"e_uupdateNews s confID uID p ev 
 IDsOK s [confID] [uID] []  pass s uID = p 
 phase s confID  setPH  phase s confID < closedPH  isChair s confID uID"

definition readNews :: "state  confID  userID  password  string list"
where
"readNews s confID uID p 
 news s confID"

definition e_readNews :: "state  confID  userID  password  bool"
where
"e_readNews s confID uID p 
 IDsOK s [confID] [uID] []  pass s uID = p 
 phase s confID  setPH  isPC s confID uID"

(* list the committee members: *)
definition listPC :: "state  confID  userID  password  userID list"
where
"listPC s confID uID p 
 [uID. uID  userIDs s, isPC s confID uID]"

definition e_listPC :: "state  confID  userID  password  bool"
where
"e_listPC s confID uID p 
 IDsOK s [confID] [uID] []  pass s uID = p 
 (phase s confID  subPH  (phase s confID  setPH  isChair s confID uID))"

(* list the chairs: *)
definition listChair :: "state  confID  userID  password  userID list"
where
"listChair s confID uID p 
 [uID. uID  userIDs s, isChair s confID uID]"

definition e_listChair :: "state  confID  userID  password  bool"
where
"e_listChair s confID uID p 
 IDsOK s [confID] [uID] []  pass s uID = p 
 (phase s confID  subPH  (phase s confID  setPH  isChair s confID uID))"


subsubsection‹Actions available in the subPH phase›

(* create new paper: *)
definition createPaper :: "state  confID  userID  password  paperID  string  string  state"
where
"createPaper s confID uID p papID title abstract 
 let papIDs = paperIDs s confID;
     rls = roles s confID uID
 in
 s paperIDs := (paperIDs s) (confID := papID # papIDs),
    paper := (paper s) (papID := Paper title abstract NoPContent [] (Dis []) []),
    roles := fun_upd2 (roles s) confID uID (List.insert (Aut papID) rls),
    pref :=  fun_upd2 (pref s) uID papID Conflict"
(* this contains an update to the preference too, to make sure that a user does not end up
reviewing his own paper! note that preference can be set even if the author is not a reviewer,
which is OK*)

definition e_createPaper :: "state  confID  userID  password  paperID  string  string  bool"
where
"e_createPaper s confID uID p papID name info 
 IDsOK s [confID] [uID] []  pass s uID = p 
 phase s confID = subPH 
 ¬ papID ∈∈ getAllPaperIDs s"

(* add author to a paper: only an author can do this *)
definition createAuthor :: "state  confID  userID  password  paperID  userID  state"
where
"createAuthor s confID uID p papID uID' 
 let rls = roles s confID uID'
 in
 s roles := fun_upd2 (roles s) confID uID' (List.insert (Aut papID) rls),
    pref :=  fun_upd2 (pref s) uID' papID Conflict"
(* again, preference is set to Conflict *)

definition e_createAuthor :: "state  confID  userID  password  paperID  userID  bool"
where
"e_createAuthor s confID uID p papID uID' 
 IDsOK s [confID] [uID,uID'] [papID]  pass s uID = p 
 phase s confID = subPH  isAut s confID uID papID  uID  uID'"

(* update name (title) and info of paper: *)
definition updatePaperTA :: "state  confID  userID  password  paperID  string  string  state"
where
"updatePaperTA s confID uID p papID title abstract 
 case paper s papID of Paper title' abstract' pc reviews dis decs 
 s paper := (paper s) (papID := Paper title abstract pc reviews dis decs)"

definition e_updatePaperTA :: "state  confID  userID  password  paperID  string  string  bool"
where
"e_updatePaperTA s confID uID p papID name info 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID = subPH  isAut s confID uID papID"

(* upload new version of paper content: *)
definition updatePaperC :: "state  confID  userID  password  paperID  pcontent  state"
where
"updatePaperC s confID uID p papID pc 
 case paper s papID of Paper title abstract pc' reviews dis decs 
 s paper := (paper s) (papID := Paper title abstract pc reviews dis decs)"

definition e_updatePaperC :: "state  confID  userID  password  paperID  pcontent  bool"
where
"e_updatePaperC s confID uID p papID pc 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID = subPH  isAut s confID uID papID"

(* declare conflict of the authored paper with a committee member*)
definition createConflict :: "state  confID  userID  password  paperID  userID  state"
where
"createConflict s confID uID p papID uID' 
 s pref := fun_upd2 (pref s) uID' papID Conflict"

definition e_createConflict :: "state  confID  userID  password  paperID  userID  bool"
where
"e_createConflict s confID uID p papID uID' 
 IDsOK s [confID] [uID,uID'] [papID]  pass s uID = p 
 phase s confID = subPH  isAut s confID uID papID  isPC s confID uID'"


subsubsection‹Actions available starting from the subPH phase›

(* read a paper's title, abstract and authors: *)
definition readPaperTAA :: "state  confID  userID  password  paperID 
    (string * string *  userID list)"
where
"readPaperTAA s confID uID p papID 
 case paper s papID of Paper title abstract pc reviews dis decs 
   (title, abstract, [uID. uID  userIDs s , isAut s confID uID papID])"

definition e_readPaperTAA :: "state  confID  userID  password  paperID  bool"
where
"e_readPaperTAA s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  subPH  (isAut s confID uID papID  isPC s confID uID)"

(* read a paper's content: *)
definition readPaperC :: "state  confID  userID  password  paperID  pcontent"
where
"readPaperC s confID uID p papID 
 case paper s papID of Paper title abstract pc reviews dis decs  pc"

definition e_readPaperC :: "state  confID  userID  password  paperID  bool"
where
"e_readPaperC s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 (
  phase s confID  subPH  isAut s confID uID papID 
  phase s confID  bidPH  isPC s confID uID
 )"

(* Note that the difference between the enabledness of readPaperTAA and that of readPaperC is
that the latter is allowed for the PC members only in the bidding phase.  *)

(* list all papers associated to a conference (with which the committee member does not have conflict): *)
definition listPapers :: "state  confID  userID  password  paperID list"
where
"listPapers s confID uID p 
 let paps = paper s in
 [papID. papID  paperIDs s confID]"

definition e_listPapers :: "state  confID  userID  password  bool"
where
"e_listPapers s confID uID p 
 IDsOK s [confID] [uID] []  pass s uID = p 
 phase s confID  subPH  isPC s confID uID"

(* list my (authored) papers: *)
definition listMyPapers :: "state  confID  userID  password  paperID list"
where
"listMyPapers s confID uID p 
 let paps = paper s in
 [papID. papID  paperIDs s confID, isAut s confID uID papID]"

definition e_listMyPapers :: "state  confID  userID  password  bool"
where
"e_listMyPapers s confID uID p 
 IDsOK s [confID] [uID] []  pass s uID = p 
 phase s confID  subPH"


subsubsection‹Actions available in the bidPH phase›

(* update (my) preference: *)
definition updatePref :: "state  confID  userID  password  paperID  preference  state"
where
"updatePref s confID uID p papID pr 
 s pref := fun_upd2 (pref s) uID papID pr"

definition e_updatePref :: "state  confID  userID  password  paperID  preference  bool"
where
"e_updatePref s confID uID p papID pr 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID = bidPH  isPC s confID uID 
 ¬ isAut s confID uID papID"
(* note: if an author of the paper, conflict was marked in the first place,
   and updating is not allowed *)


subsubsection‹Actions available starting from the bidPH phase›

(* read (my) preference: *)
definition readPref :: "state  confID  userID  password  paperID  preference"
where
"readPref s confID uID p papID 
 pref s uID papID"

definition e_readPref :: "state  confID  userID  password  paperID  bool"
where
"e_readPref s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  bidPH  isPC s confID uID"


subsubsection‹Actions available in the revPH phase›

(* read preferences of a committee member (useful for the chair to read the preferences of the
committee members: *)

definition readPrefOfPC :: "state  confID  userID  password  paperID  userID  preference"
where
"readPrefOfPC s confID uID p papID uID' 
 pref s uID' papID"

definition e_readPrefOfPC :: "state  confID  userID  password  paperID  userID bool"
where
"e_readPrefOfPC s confID uID p papID uID' 
 IDsOK s [confID] [uID,uID'] [papID]  pass s uID = p 
 (phase s confID  bidPH  isChair s confID uID  isPC s confID uID'
  
  phase s confID = subPH  isAut s confID uID papID)"
(* unique violation of monotonicity for read actions: an author can read the preferences of the PC chair
  in the submission phase, but not later, as later they will have been updated by the chairs *)

(* create a review and assign a reviewer: *)
definition createReview :: "state  confID  userID  password  paperID  userID  state"
where
"createReview s confID uID p papID uID' 
 case paper s papID of Paper title abstract pc reviews dis decs 
   let rls = roles s confID uID'; n = length (reviewsPaper (paper s papID));
       reviews' = reviews @ [emptyReview]
   in
   s roles := fun_upd2 (roles s) confID uID' (List.insert (Rev papID n) rls),
      paper := fun_upd (paper s) papID (Paper title abstract pc reviews' dis decs)
     "
(* note: the new review is added at the end, in order not to disrupt the indexing of the other reviews *)

definition e_createReview :: "state  confID  userID  password  paperID  userID  bool"
where
"e_createReview s confID uID p papID uID' 
 IDsOK s [confID] [uID,uID'] [papID]  pass s uID = p 
 phase s confID = revPH 
 isChair s confID uID  pref s uID papID  Conflict 
 isPC s confID uID'  ¬ isRev s confID uID' papID  pref s uID' papID  Conflict"

(* update the review that I write: *)
definition updateReview ::
"state  confID  userID  password  paperID  nat  rcontent  state"
where
"updateReview s confID uID p papID n rc 
 case paper s papID of Paper title abstract pc reviews dis decs 
   let review = [rc]; reviews' = list_update reviews n review
   in
   s paper := fun_upd (paper s) papID (Paper title abstract pc reviews' dis decs)"

definition e_updateReview ::
"state  confID  userID  password  paperID  nat  rcontent  bool"
where
"e_updateReview s confID uID p papID n rc 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID = revPH  isRev s confID uID papID 
 getReviewIndex s confID uID papID = n"


subsubsection‹Actions available starting from the revPH phase›

(* read the review that I write: *)
definition readMyReview :: "state  confID  userID  password  paperID  nat * review"
where
"readMyReview s confID uID p papID 
 case getRevRole s confID uID papID of
   Some (Rev papID' n)  (n, getNthReview s papID n)"

definition e_readMyReview :: "state  confID  userID  password  paperID  bool"
where
"e_readMyReview s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  revPH  isRev s confID uID papID"

(* list my assigned papers: *)
definition listMyAssignedPapers :: "state  confID  userID  password  paperID list"
where
"listMyAssignedPapers s confID uID p 
 let paps = paper s in
 [papID. papID  paperIDs s confID, isRev s confID uID papID]"

definition e_listMyAssignedPapers :: "state  confID  userID  password  bool"
where
"e_listMyAssignedPapers s confID uID p 
 IDsOK s [confID] [uID] []  pass s uID = p 
 phase s confID  revPH  isPC s confID uID"


definition listAssignedReviewers :: "state  confID  userID  password  paperID  userID list"
where
"listAssignedReviewers s confID uID p papID 
 [uID  userIDs s. isRev s confID uID papID]"

definition e_listAssignedReviewers :: "state  confID  userID  password  paperID  bool"
where
"e_listAssignedReviewers s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  revPH 
 isChair s confID uID  pref s uID papID  Conflict"


subsubsection‹Actions available in the disPH phase›

(* undestructively update the discussion with a comment: *)
definition uupdateDis :: "state  confID  userID  password  paperID  string  state"
where
"uupdateDis s confID uID p papID comm 
 case paper s papID of Paper title abstract pc reviews (Dis comments) decs 
   s paper := fun_upd (paper s) papID (Paper title abstract pc reviews (Dis (comm # comments)) decs)"

definition e_uupdateDis :: "state  confID  userID  password  paperID  string  bool"
where
"e_uupdateDis s confID uID p papID comm 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID = disPH  isPC s confID uID  pref s uID papID  Conflict"

(* correct my review during the discussion
(instance of a undestructive update) *)
definition uupdateReview ::
"state  confID  userID  password  paperID  nat  rcontent  state"
where
"uupdateReview s confID uID p papID n rc 
 case paper s papID of Paper title abstract pc reviews dis decs 
   let review = rc # (reviews ! n); reviews' = list_update reviews n review
   in
   s paper := fun_upd (paper s) papID (Paper title abstract pc reviews' dis decs)"

definition e_uupdateReview ::
"state  confID  userID  password  paperID  nat  rcontent  bool"
where
"e_uupdateReview s confID uID p papID n rc 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID = disPH  isRev s confID uID papID 
 getReviewIndex s confID uID papID = n"

(* update the decision for a paper (again undestructive update) : *)
definition uupdateDec :: "state  confID  userID  password  paperID  decision  state"
where
"uupdateDec s confID uID p papID dec 
 case paper s papID of Paper title abstract pc reviews dis decs 
   s paper := fun_upd (paper s) papID (Paper title abstract pc reviews dis (dec # decs))"

definition e_uupdateDec :: "state  confID  userID  password  paperID  decision  bool"
where
"e_uupdateDec s confID uID p papID dec 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID = disPH  isChair s confID uID  pref s uID papID  Conflict"


subsubsection‹Actions available starting from the disPH phase›

(* read all the reviews to a paper (including all the updates) with the IDs of the reviewers: *)
definition readReviews :: "state  confID  userID  password  paperID  (userID * review) list"
where
"readReviews s confID uID p papID 
 getReviewersReviews s confID papID"

definition e_readReviews :: "state  confID  userID  password  paperID  bool"
where
"e_readReviews s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  disPH  isPC s confID uID  pref s uID papID  Conflict"

(* read the decisions (i.e., the decision history) for a paper: *)
definition readDecs :: "state  confID  userID  password  paperID  decision list"
where
"readDecs s confID uID p papID 
 case paper s papID of Paper title abstract pc reviews dis decs  decs"

definition e_readDecs :: "state  confID  userID  password  paperID  bool"
where
"e_readDecs s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  disPH  isPC s confID uID  pref s uID papID  Conflict"

(* read the discussion to a paper: *)
definition readDis :: "state  confID  userID  password  paperID  string list"
where
"readDis s confID uID p papID 
 case paper s papID of Paper title abstract pc reviews (Dis comments) decs  comments"

definition e_readDis :: "state  confID  userID  password  paperID  bool"
where
"e_readDis s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  disPH  isPC s confID uID  pref s uID papID  Conflict"



subsubsection‹Actions available starting from the notifPH phase›

(* read final reviews to a paper: available to the authors and all non-conflicted PC members *)
definition readFinalReviews :: "state  confID  userID  password  paperID  review list"
where
"readFinalReviews s confID uID p papID 
 map (λ rev. case rev of []  [(NoExp,NoScore,emptyStr)]
                        |((exp,score,comm) # rv)  [(exp,score,comm)])
 (reviewsPaper (paper s papID))"

definition e_readFinalReviews :: "state  confID  userID  password  paperID  bool"
where
"e_readFinalReviews s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  notifPH  (isAut s confID uID papID  (isPC s confID uID  pref s uID papID  Conflict))"

(* read the final decision for a paper available to the authors and all PC members (including conflicted PC members):*)
definition readFinalDec :: "state  confID  userID  password  paperID  decision"
where
"readFinalDec s confID uID p papID 
 case paper s papID of Paper title abstract pc reviews dis decs 
   case decs of []  NoDecision | dec # decs  dec"

definition e_readFinalDec :: "state  confID  userID  password  paperID  bool"
where
"e_readFinalDec s confID uID p papID 
 IDsOK s [confID] [uID] [papID]  pass s uID = p 
 phase s confID  notifPH  (isAut s confID uID papID  isPC s confID uID)"


subsection‹The step function›

datatype out =
  outOK | outErr | (* OK and error, outputs for list, update and u-update  actions *)
  outBool bool|
  outSTRT "string * string * string" | outSTRL "string list" | outCONF "string * string * role list * phase" |
  outPREF preference |
  outCON pcontent |
  outNREV "nat * review" | outREVL "review list" | outRREVL "(userID * review) list" |
  outDEC "decision" | outDECL "decision list" |
  outCIDL "confID list" |   outUIDL "userID list" | outPIDL "paperID list"|
  outSTRPAL "string * string * userID list"

datatype cAct =
  cUser userID password string string string
 |cConf confID userID password string string
 |cPC confID userID password userID
 |cChair confID userID password userID
 |cPaper confID userID password paperID string string
 |cAuthor confID userID password paperID userID
 |cConflict confID userID password paperID userID
 |cReview confID userID password paperID userID

lemmas c_defs =
e_createUser_def createUser_def
e_createConf_def createConf_def
e_createPC_def createPC_def
e_createChair_def createChair_def
e_createAuthor_def createAuthor_def
e_createConflict_def createConflict_def
e_createPaper_def createPaper_def
e_createReview_def createReview_def

fun cStep :: "state  cAct  out * state" where
"cStep s (cUser uID p name info email) =
 (if e_createUser s uID p name info email
    then (outOK, createUser s uID p name info email)
    else (outErr, s))"
|
"cStep s (cConf confID uID p name info) =
 (if e_createConf s confID uID p name info
    then (outOK, createConf s confID uID p name info)
    else (outErr, s))"
|
"cStep s (cPC confID uID p uID') =
 (if e_createPC s confID uID p uID'
    then (outOK, createPC s confID uID p uID')
    else (outErr, s))"
|
"cStep s (cChair confID uID p uID') =
 (if e_createChair s confID uID p uID'
    then (outOK, createChair s confID uID p uID')
    else (outErr, s))"
|
"cStep s (cPaper confID uID p papID name info) =
 (if e_createPaper s confID uID p papID name info
    then (outOK, createPaper s confID uID p papID name info)
    else (outErr, s))"
|
"cStep s (cAuthor confID uID p papID uID') =
 (if e_createAuthor s confID uID p papID uID'
    then (outOK, createAuthor s confID uID p papID uID')
    else (outErr, s))"
|
"cStep s (cConflict confID uID p papID uID') =
 (if e_createConflict s confID uID p papID uID'
    then (outOK, createConflict s confID uID p papID uID')
    else (outErr, s))"
|
"cStep s (cReview confID uID p papID uID') =
 (if e_createReview s confID uID p papID uID'
    then (outOK, createReview s confID uID p papID uID')
    else (outErr, s))"


datatype uAct =
  uUser userID password password string string string
 |uConfA confID userID password
 |uPhase confID userID password phase
 |uPaperTA confID userID password paperID string string
 |uPaperC confID userID password paperID pcontent
 |uPref confID userID password paperID preference
 |uReview confID userID password paperID nat rcontent

lemmas u_defs =
e_updateUser_def updateUser_def
e_updateConfA_def updateConfA_def
e_updatePhase_def updatePhase_def
e_updatePaperTA_def updatePaperTA_def
e_updatePaperC_def updatePaperC_def
e_updatePref_def updatePref_def
e_updateReview_def updateReview_def

fun uStep :: "state  uAct  out * state" where
"uStep s (uUser uID p p' name info email) =
 (if e_updateUser s uID p p' name info email
    then (outOK, updateUser s uID p p' name info email)
    else (outErr, s))"
|
"uStep s (uConfA confID uID p) =
 (if e_updateConfA s confID uID p
    then (outOK, updateConfA s confID uID p)
    else (outErr, s))"
|
"uStep s (uPhase confID uID p ph) =
 (if e_updatePhase s confID uID p ph
    then (outOK, updatePhase s confID uID p ph)
    else (outErr, s))"
|
"uStep s (uPaperTA confID uID p papID name info) =
 (if e_updatePaperTA s confID uID p papID name info
    then (outOK, updatePaperTA s confID uID p papID name info)
    else (outErr, s))"
|
"uStep s (uPaperC confID uID p papID pc) =
 (if e_updatePaperC s confID uID p papID pc
    then (outOK, updatePaperC s confID uID p papID pc)
    else (outErr, s))"
|
"uStep s (uPref confID uID p papID pr) =
 (if e_updatePref s confID uID p papID pr
    then (outOK, updatePref s confID uID p papID pr)
    else (outErr, s))"
|
"uStep s (uReview confID uID p papID n rc) =
 (if e_updateReview s confID uID p papID n rc
    then (outOK, updateReview s confID uID p papID n rc)
    else (outErr, s))"


datatype uuAct =
  uuNews confID userID password string
 |uuDis confID userID password paperID string
 |uuReview confID userID password paperID nat rcontent
 |uuDec confID userID password paperID decision

lemmas uu_defs =
e_uupdateNews_def uupdateNews_def
e_uupdateDis_def uupdateDis_def
e_uupdateReview_def uupdateReview_def
uupdateDec_def e_uupdateDec_def

fun uuStep :: "state  uuAct  out * state" where
"uuStep s (uuNews confID uID p ev) =
 (if e_uupdateNews s confID uID p ev
    then (outOK, uupdateNews s confID uID p ev)
    else (outErr, s))"
|
"uuStep s (uuDis confID uID p papID comm) =
 (if e_uupdateDis s confID uID p papID comm
    then (outOK, uupdateDis s confID uID p papID comm)
    else (outErr, s))"
|
"uuStep s (uuReview confID uID p papID n rc) =
 (if e_uupdateReview s confID uID p papID n rc
    then (outOK, uupdateReview s confID uID p papID n rc)
    else (outErr, s))"
|
"uuStep s (uuDec confID uID p papID dec) =
 (if e_uupdateDec s confID uID p papID dec
    then (outOK, uupdateDec s confID uID p papID dec)
    else (outErr, s))"

datatype rAct =
  rAmIVoronkov userID password
 |rUser userID password userID
 |rConf confID userID password
 |rNews confID userID password
 |rPaperTAA confID userID password paperID
 |rPaperC confID userID password paperID
 |rPref confID userID password paperID
 |rMyReview confID userID password paperID
 |rReviews confID userID password paperID
 |rDecs confID userID password paperID
 |rDis confID userID password paperID
 |rFinalReviews confID userID password paperID
 |rFinalDec confID userID password paperID
 |rPrefOfPC confID userID password paperID userID

lemmas r_defs =
  readAmIVoronkov_def e_readAmIVoronkov_def
 readUser_def e_readUser_def
 readConf_def e_readConf_def
 readNews_def e_readNews_def
 readPaperTAA_def e_readPaperTAA_def
 readPaperC_def e_readPaperC_def
 readPref_def e_readPref_def
 readMyReview_def e_readMyReview_def
 readReviews_def e_readReviews_def
 readDecs_def e_readDecs_def
 readDis_def e_readDis_def
 readFinalReviews_def e_readFinalReviews_def
 readFinalDec_def e_readFinalDec_def
 readPrefOfPC_def e_readPrefOfPC_def

fun<