Theory System_Specification

section ‹System specification›

theory System_Specification
imports Prelim
begin

(* This is the system specification of COSMED.
*)

declare List.insert[simp]

subsection ‹The state›

record state =
  admin :: userID
  (*  *)
  pendingUReqs :: "userID list"
  userReq :: "userID ⇒ req"
  userIDs :: "userID list"
  user :: "userID ⇒ user"
  pass :: "userID ⇒ password"
  (*  *)
  pendingFReqs :: "userID ⇒ userID list"
  friendReq :: "userID ⇒ userID ⇒ req"
  friendIDs :: "userID ⇒ userID list"
  (*  *)
  postIDs :: "postID list"
  post :: "postID ⇒ post"
  owner :: "postID ⇒ userID"
  vis :: "postID ⇒ vis"

definition IDsOK :: "state ⇒ userID list ⇒ postID list ⇒ bool"
where
"IDsOK s uIDs pIDs ≡
 list_all (λ uID. uID ∈∈ userIDs s) uIDs ∧
 list_all (λ pID. pID ∈∈ postIDs s) pIDs"


subsection ‹The actions›

subsubsection‹Initialization of the system›

definition istate :: state
where
"istate ≡
 ⦇
  admin = emptyUserID,

  pendingUReqs = [],
  userReq = (λ uID. emptyReq),
  userIDs = [],
  user = (λ uID. emptyUser),
  pass = (λ uID. emptyPass),

  pendingFReqs = (λ uID. []),
  friendReq = (λ uID uID'. emptyReq),
  friendIDs = (λ uID. []),

  postIDs = [],
  post = (λ papID. emptyPost),
  owner = (λ pID. emptyUserID),
  vis = (λ pID. FriendV)
 ⦈"


subsubsection‹Starting action›

(* This initiates the system. It has the following parameters:
  -- uID, p, name: the admin user id, name and password
*)
definition startSys ::
"state ⇒ userID ⇒ password ⇒ state"
where
"startSys s uID p ≡
 s ⦇admin := uID,
    userIDs := [uID],
    user := (user s) (uID := emptyUser),
    pass := (pass s) (uID := p)⦈"

definition e_startSys :: "state ⇒ userID ⇒ password ⇒  bool"
where
"e_startSys s uID p ≡ userIDs s = []"


subsubsection‹Creation actions›


(* Create new user request: we allow users to choose their own IDs; they could be their email addresses. *)
definition createNUReq :: "state ⇒ userID ⇒ req ⇒ state"
where
"createNUReq s uID reqInfo ≡
 s ⦇pendingUReqs := pendingUReqs s @ [uID],
    userReq := (userReq s)(uID := reqInfo)
⦈"

definition e_createNUReq :: "state ⇒ userID ⇒ req ⇒ bool"
where
"e_createNUReq s uID req ≡
 admin s ∈∈ userIDs s ∧ ¬ uID ∈∈ userIDs s ∧ ¬ uID ∈∈ pendingUReqs s"
(* a new-user request can be created only if the system has started, i.e., if an admin exists *)

(* The admin actually creates a user by approving a pending new-user request.
E.g., the admin can add an  arbitrary password and send it by email to that user.
Then the user can change his password. *)
definition createUser :: "state ⇒ userID ⇒ password ⇒ userID ⇒ password ⇒ state"
where
"createUser s uID p uID' p' ≡
 s ⦇userIDs := uID' # (userIDs s),
    user := (user s) (uID' := emptyUser),
    pass := (pass s) (uID' := p'),
    pendingUReqs := remove1 uID' (pendingUReqs s),
    userReq := (userReq s)(uID := emptyReq)⦈"

definition e_createUser :: "state ⇒ userID ⇒ password ⇒ userID ⇒ password ⇒ bool"
where
"e_createUser s uID p uID' p' ≡
 IDsOK s [uID] [] ∧ pass s uID = p ∧ uID = admin s ∧ uID' ∈∈ pendingUReqs s"


(* Create post: note that post ID is an action parameter, and that the enabledness action
checks that it is fresh.
The web interface will actually generate it, using getFresh. *)
definition createPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ title ⇒ state"
where
"createPost s uID p pID title ≡
 s ⦇postIDs := pID # postIDs s,
    post := (post s) (pID := Ntc title emptyText emptyImg),
    owner := (owner s) (pID := uID)⦈"
(* Recall from the initial state that the initial visibility is FriendV *)

definition e_createPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ title ⇒ bool"
where
"e_createPost s uID p pID title ≡
 IDsOK s [uID] [] ∧ pass s uID = p ∧
 ¬ pID ∈∈ postIDs s"

(* Friendship: *)
(* Create friend request, namely uID Reqs friendship of uID': *)
definition createFriendReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ req ⇒ state"
where
"createFriendReq s uID p uID' req ≡
 let pfr = pendingFReqs s in
 s ⦇pendingFReqs := pfr (uID' := pfr uID' @ [uID]),
    friendReq := fun_upd2 (friendReq s) uID uID' req⦈"

definition e_createFriendReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ req ⇒ bool"
where
"e_createFriendReq s uID p uID' req ≡
 IDsOK s [uID,uID'] [] ∧ pass s uID = p ∧
 ¬ uID ∈∈ pendingFReqs s uID' ∧ ¬ uID ∈∈ friendIDs s uID'"

(* Create friend, by approving a friend request (namely uID approves the request from uID').
Friendship is symmetric, hence the two updates to "friend";
also, the friendship request is canceled upon approval.  *)
definition createFriend :: "state ⇒ userID ⇒ password ⇒ userID ⇒ state"
where
"createFriend s uID p uID' ≡
 let fr = friendIDs s; pfr = pendingFReqs s in
 s ⦇friendIDs := fr (uID := fr uID @ [uID'], uID' := fr uID' @ [uID]),
    pendingFReqs := pfr (uID := remove1 uID' (pfr uID), uID' := remove1 uID (pfr uID')),
    friendReq := fun_upd2 (fun_upd2 (friendReq s) uID' uID emptyReq) uID uID' emptyReq⦈"

definition e_createFriend :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_createFriend s uID p uID' ≡
 IDsOK s [uID,uID'] [] ∧ pass s uID = p ∧
 uID' ∈∈ pendingFReqs s uID"


subsubsection‹Updating actions›

(* Users can update their passwords and names: *)
definition updateUser :: "state ⇒ userID ⇒ password ⇒ password ⇒ name ⇒ inform ⇒ state"
where
"updateUser s uID p p' name info ≡
 s ⦇user := (user s) (uID := Usr name info),
    pass := (pass s) (uID := p')⦈"

definition e_updateUser :: "state ⇒ userID ⇒ password ⇒ password ⇒ name ⇒ inform ⇒ bool"
where
"e_updateUser s uID p p' name info ≡
 IDsOK s [uID] [] ∧ pass s uID = p"


(* Updates of the post components: *)
definition updatePost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ post ⇒ state"
where
"updatePost s uID p pID pst ≡
 s ⦇post := (post s) (pID := pst)⦈"

definition e_updatePost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ post ⇒ bool"
where
"e_updatePost s uID p pID pst ≡
 IDsOK s [uID] [pID] ∧ pass s uID = p ∧
 owner s pID = uID"

definition updateVisPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ vis ⇒ state"
where
"updateVisPost s uID p pID vs ≡
 s ⦇vis := (vis s) (pID := vs)⦈"

definition e_updateVisPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ vis ⇒ bool"
where
"e_updateVisPost s uID p pID vs ≡
 IDsOK s [uID] [pID] ∧ pass s uID = p ∧
 owner s pID = uID ∧ vs ∈ {FriendV, PublicV}"



subsubsection‹Deletion (removal) actions›

(* Delete friend:   *)
definition deleteFriend :: "state ⇒ userID ⇒ password ⇒ userID ⇒ state"
where
"deleteFriend s uID p uID' ≡
 let fr = friendIDs s in
 s ⦇friendIDs := fr (uID := removeAll uID' (fr uID), uID' := removeAll uID (fr uID'))⦈"

definition e_deleteFriend :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_deleteFriend s uID p uID' ≡
 IDsOK s [uID,uID'] [] ∧ pass s uID = p ∧
 uID' ∈∈ friendIDs s uID"


subsubsection‹Reading actions›

(* Read new user request: *)
definition readNUReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ req"
where
"readNUReq s uID p uID' ≡ userReq s uID'"

definition e_readNUReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_readNUReq s uID p uID' ≡
 IDsOK s [uID] [] ∧ pass s uID = p ∧
 uID = admin s ∧ uID' ∈∈ pendingUReqs s"

(* A user can read their name and info (and so can all the other users), but not the password: *)
definition readUser :: "state ⇒ userID ⇒ password ⇒ userID ⇒ name × inform"
where
"readUser s uID p uID' ≡ niUser (user s uID')"

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

(* A user can check if he is the admin: *)
definition readAmIAdmin :: "state ⇒ userID ⇒ password ⇒ bool"
where
"readAmIAdmin s uID p ≡ uID = admin s"

definition e_readAmIAdmin :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_readAmIAdmin s uID p ≡
 IDsOK s [uID] [] ∧ pass s uID = p"

(* Reading posts: *)
definition readPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ post"
where
"readPost s uID p pID ≡ post s pID"

definition e_readPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_readPost s uID p pID ≡
 let post = post s pID in
 IDsOK s [uID] [pID] ∧ pass s uID = p ∧
 (owner s pID = uID ∨ uID ∈∈ friendIDs s (owner s pID) ∨ vis s pID = PublicV)"

definition readVisPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ vis"
where
"readVisPost s uID p pID ≡ vis s pID"

definition e_readVisPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_readVisPost s uID p pID ≡
 let post = post s pID in
 IDsOK s [uID] [pID] ∧ pass s uID = p ∧
 (owner s pID = uID ∨ uID ∈∈ friendIDs s (owner s pID) ∨ vis s pID = PublicV)"

definition readOwnerPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ userID"
where
"readOwnerPost s uID p pID ≡ owner s pID"

definition e_readOwnerPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_readOwnerPost s uID p pID ≡
 let post = post s pID in
 IDsOK s [uID] [pID] ∧ pass s uID = p ∧
 (owner s pID = uID ∨ uID ∈∈ friendIDs s (owner s pID) ∨ vis s pID = PublicV)"


(* Friendship: *)
(* Read friendship request to me: *)
definition readFriendReqToMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ req"
where
"readFriendReqToMe s uID p uID' ≡ friendReq s uID' uID"

definition e_readFriendReqToMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_readFriendReqToMe s uID p uID' ≡
 IDsOK s [uID,uID'] [] ∧ pass s uID = p ∧
 uID' ∈∈ pendingFReqs s uID"

(* Read friendship request from me: *)
definition readFriendReqFromMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ req"
where
"readFriendReqFromMe s uID p uID' ≡ friendReq s uID uID'"

definition e_readFriendReqFromMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_readFriendReqFromMe s uID p uID' ≡
 IDsOK s [uID,uID'] [] ∧ pass s uID = p ∧
 uID ∈∈ pendingFReqs s uID'"


subsubsection‹Listing actions›

(* list pending new user requests: *)
definition listPendingUReqs :: "state ⇒ userID ⇒ password ⇒ userID list"
where
"listPendingUReqs s uID p ≡ pendingUReqs s"

definition e_listPendingUReqs :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listPendingUReqs s uID p ≡
 IDsOK s [uID] [] ∧ pass s uID = p ∧ uID = admin s"

(* list all users of the system: *)
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 a user's friends: *)
definition listFriends :: "state ⇒ userID ⇒ password ⇒ userID ⇒ userID list"
where
"listFriends s uID p uID' ≡ friendIDs s uID'"

definition e_listFriends :: "state ⇒ userID ⇒ password ⇒ userID ⇒ bool"
where
"e_listFriends s uID p uID' ≡
 IDsOK s [uID,uID'] [] ∧ pass s uID = p ∧
 (uID = uID' ∨ uID ∈∈ friendIDs s uID')"

(* list posts:: *)
definition listPosts :: "state ⇒ userID ⇒ password ⇒ (userID × postID) list"
where
"listPosts s uID p ≡
  [(owner s pID, pID).
    pID ← postIDs s,
    vis s pID = PublicV ∨ uID ∈∈ friendIDs s (owner s pID) ∨ uID = owner s pID
  ]"

definition e_listPosts :: "state ⇒ userID ⇒ password ⇒ bool"
where
"e_listPosts s uID p ≡ IDsOK s [uID] [] ∧ pass s uID = p"



subsection‹The step function›

datatype out =
  (* Outputs for creation and update actions, as well as for other actions with errors: *)
  outOK | outErr |
  (* Outputs for reading actions: *)
  outBool bool| outNI "name × inform" | outPost post |
  outImg img | outVis vis | outReq req |
  (* Outputs for listing actions: *)
  outUID "userID" | outUIDL "userID list" |
  outUIDNIDL "(userID × postID)list"
  (* outNone (* Used later for global actions *) *)


(* Start actions (only one, but wrapped for uniformity): *)
datatype sActt =
  sSys userID password

lemmas s_defs =
e_startSys_def startSys_def

fun sStep :: "state ⇒ sActt ⇒ out * state" where
"sStep s (sSys uID p) =
 (if e_startSys s uID p
    then (outOK, startSys s uID p)
    else (outErr, s))"

fun sUserOfA :: "sActt ⇒ userID" where
 "sUserOfA (sSys uID p) = uID"

(* Creation actions: *)
datatype cActt =
  cNUReq userID req
 |cUser userID password userID password
 |cFriendReq userID password userID req
 |cFriend userID password userID
 |cPost userID password postID title

lemmas c_defs =
e_createNUReq_def createNUReq_def
e_createUser_def createUser_def
e_createFriendReq_def createFriendReq_def
e_createFriend_def createFriend_def
e_createPost_def createPost_def

fun cStep :: "state ⇒ cActt ⇒ out * state" where
"cStep s (cNUReq uID req) =
 (if e_createNUReq s uID req
    then (outOK, createNUReq s uID req)
    else (outErr, s))"
|
"cStep s (cUser uID p uID' p') =
 (if e_createUser s uID p uID' p'
    then (outOK, createUser s uID p uID' p')
    else (outErr, s))"
|
"cStep s (cFriendReq uID p uID' req) =
 (if e_createFriendReq s uID p uID' req
    then (outOK, createFriendReq s uID p uID' req)
    else (outErr, s))"
|
"cStep s (cFriend uID p uID') =
 (if e_createFriend s uID p uID'
    then (outOK, createFriend s uID p uID')
    else (outErr, s))"
|
"cStep s (cPost uID p pID title) =
 (if e_createPost s uID p pID title
    then (outOK, createPost s uID p pID title)
    else (outErr, s))"

fun cUserOfA :: "cActt ⇒ userID option" where
 "cUserOfA (cNUReq uID req) = Some uID"
|"cUserOfA (cUser uID p uID' p') = Some uID"
|"cUserOfA (cFriendReq uID p uID' req) = Some uID"
|"cUserOfA (cFriend uID p uID') = Some uID"
|"cUserOfA (cPost uID p pID title) = Some uID"



(* Deletion (removal) actions -- currently only friends can be deleted *)

datatype dActt =
  dFriend userID password userID

lemmas d_defs =
e_deleteFriend_def deleteFriend_def

fun dStep :: "state ⇒ dActt ⇒ out * state" where
"dStep s (dFriend uID p uID') =
 (if e_deleteFriend s uID p uID'
    then (outOK, deleteFriend s uID p uID')
    else (outErr, s))"

fun dUserOfA :: "dActt ⇒ userID" where
 "dUserOfA (dFriend uID p uID') = uID"

(* Update actions: *)
datatype uActt =
  uUser userID password password name inform
 |uPost userID password postID post
 |uVisPost userID password postID vis

lemmas u_defs =
e_updateUser_def updateUser_def
e_updatePost_def updatePost_def
e_updateVisPost_def updateVisPost_def

fun uStep :: "state ⇒ uActt ⇒ out * state" where
"uStep s (uUser uID p p' name info) =
 (if e_updateUser s uID p p' name info
    then (outOK, updateUser s uID p p' name info)
    else (outErr, s))"
|
"uStep s (uPost uID p pID pst) =
 (if e_updatePost s uID p pID pst
    then (outOK, updatePost s uID p pID pst)
    else (outErr, s))"
|
"uStep s (uVisPost uID p pID visStr) =
 (if e_updateVisPost s uID p pID visStr
    then (outOK, updateVisPost s uID p pID visStr)
    else (outErr, s))"

fun uUserOfA :: "uActt ⇒ userID" where
 "uUserOfA (uUser uID p p' name info) = uID"
|"uUserOfA (uPost uID p pID pst) = uID"
|"uUserOfA (uVisPost uID p pID visStr) = uID"


(* Read actions: *)
datatype rActt =
  rNUReq userID password userID
 |rUser userID password userID
 |rAmIAdmin userID password
 |rPost userID password postID
 |rVisPost userID password postID
 |rOwnerPost userID password postID
 |rFriendReqToMe userID password userID
 |rFriendReqFromMe userID password userID

lemmas r_defs =
 readNUReq_def e_readNUReq_def
 readUser_def e_readUser_def
 readAmIAdmin_def e_readAmIAdmin_def
 readPost_def e_readPost_def
 readVisPost_def e_readVisPost_def
 readOwnerPost_def e_readOwnerPost_def
 readFriendReqToMe_def e_readFriendReqToMe_def
 readFriendReqFromMe_def e_readFriendReqFromMe_def

fun rObs :: "state ⇒ rActt ⇒ out" where
"rObs s (rNUReq uID p uID') =
 (if e_readNUReq s uID p uID' then outReq (readNUReq s uID p uID') else outErr)"
|
"rObs s (rUser uID p uID') =
 (if e_readUser s uID p uID' then outNI (readUser s uID p uID') else outErr)"
|
"rObs s (rAmIAdmin uID p) =
 (if e_readAmIAdmin s uID p then outBool (readAmIAdmin s uID p) else outErr)"
|
"rObs s (rPost uID p pID) =
 (if e_readPost s uID p pID then outPost (readPost s uID p pID) else outErr)"
|
"rObs s (rVisPost uID p pID) =
 (if e_readVisPost s uID p pID then outVis (readVisPost s uID p pID) else outErr)"
|
"rObs s (rOwnerPost uID p pID) =
 (if e_readOwnerPost s uID p pID then outUID (readOwnerPost s uID p pID) else outErr)"
|
"rObs s (rFriendReqToMe uID p uID') =
 (if e_readFriendReqToMe s uID p uID' then outReq (readFriendReqToMe s uID p uID') else outErr)"
|
"rObs s (rFriendReqFromMe uID p uID') =
 (if e_readFriendReqFromMe s uID p uID' then outReq (readFriendReqFromMe s uID p uID') else outErr)"


fun rUserOfA :: "rActt ⇒ userID option" where
 "rUserOfA (rNUReq uID p uID') = Some uID"
|"rUserOfA (rUser uID p uID') = Some uID"
|"rUserOfA (rAmIAdmin uID p) = Some uID"
|"rUserOfA (rPost uID p pID) = Some uID"
|"rUserOfA (rVisPost uID p pID) = Some uID"
|"rUserOfA (rOwnerPost uID p pID) = Some uID"
|"rUserOfA (rFriendReqToMe uID p uID') = Some uID"
|"rUserOfA (rFriendReqFromMe uID p uID') = Some uID"


(* Listing actions *)
datatype lActt =
  lPendingUReqs userID password
 |lAllUsers userID password
 |lFriends userID password userID
 |lPosts userID password


lemmas l_defs =
 listPendingUReqs_def e_listPendingUReqs_def
 listAllUsers_def e_listAllUsers_def
 listFriends_def e_listFriends_def
 listPosts_def e_listPosts_def


fun lObs :: "state ⇒ lActt ⇒ out" where
"lObs s (lPendingUReqs uID p) =
 (if e_listPendingUReqs s uID p then outUIDL (listPendingUReqs s uID p) else outErr)"
|
"lObs s (lAllUsers uID p) =
 (if e_listAllUsers s uID p then outUIDL (listAllUsers s uID p) else outErr)"
|
"lObs s (lFriends uID p uID') =
 (if e_listFriends s uID p uID' then outUIDL (listFriends s uID p uID') else outErr)"
|
"lObs s (lPosts uID p) =
 (if e_listPosts s uID p then outUIDNIDL (listPosts s uID p) else outErr)"


fun lUserOfA :: "lActt ⇒ userID option" where
 "lUserOfA (lPendingUReqs uID p) = Some uID"
|"lUserOfA (lAllUsers uID p) = Some uID"
|"lUserOfA (lFriends uID p uID') = Some uID"
|"lUserOfA (lPosts uID p) = Some uID"



(* All actions: *)
datatype act =
  Sact sActt |
(* 3 kinds of effects: creation, deletion and update *)
  Cact cActt | Dact dActt | Uact uActt |
(* 2 kinds of observations: reading and listing (the latter mainly printing IDs) *)
  Ract rActt | Lact lActt


fun step :: "state ⇒ act ⇒ out * state" where
"step s (Sact sa) = sStep s sa"
|
"step s (Cact ca) = cStep s ca"
|
"step s (Dact da) = dStep s da"
|
"step s (Uact ua) = uStep s ua"
|
"step s (Ract ra) = (rObs s ra, s)"
|
"step s (Lact la) = (lObs s la, s)"

fun userOfA :: "act ⇒ userID option" where
"userOfA (Sact sa) = Some (sUserOfA sa)"
|
"userOfA (Cact ca) = cUserOfA ca"
|
"userOfA (Dact da) = Some (dUserOfA da)"
|
"userOfA (Uact ua) = Some (uUserOfA ua)"
|
"userOfA (Ract ra) = rUserOfA ra"
|
"userOfA (Lact la) = lUserOfA la"



subsection ‹Code generation›

export_code step istate getFreshPostID in Scala


end