Theory System_Specification

section ‹The CoSMeDis single node specification›

text ‹This is the specification of a CoSMeDis node, as described
in Sections II and IV.B of cite‹"cosmedis-SandP2017"›.
NB: What that paper refers to as "nodes" are referred in this formalization
as "APIs".

A CoSMeDis node extends CoSMed cite‹"cosmed-itp2016" and "cosmed-jar2018" and "cosmed-AFP"›
with inter-node communication actions.
›

theory System_Specification
  imports
    Prelim
    "Bounded_Deducibility_Security.IO_Automaton"
begin

text ‹An aspect not handled in this specification is the uniqueness of the node IDs. These
are assumed to be handled externally as follows: a node ID is an URI, and therefore is unique.›

declare List.insert[simp]

subsection ‹The state›

record state =
  admin :: userID
  (*  *)
  pendingUReqs :: "userID list"
  userReq :: "userID ⇒ requestInfo"
  userIDs :: "userID list"
  user :: "userID ⇒ user"
  pass :: "userID ⇒ password"
  (*  *)
  pendingFReqs :: "userID ⇒ userID list"
  friendReq :: "userID ⇒ userID ⇒ requestInfo"
  friendIDs :: "userID ⇒ userID list"
  (* Outer friendship, i.e., friendship with users of other (server) APIs. This will effectively
     mean access to the friend-only outer posts retrieved from that server.
     There are two lists:
      - friendship authorizations sent by users of this API, and
      - friendship authorizations received from other APIs. *)
  sentOuterFriendIDs :: "userID ⇒ (apiID × userID) list"
  recvOuterFriendIDs :: "userID ⇒ (apiID × userID) list"
  (*  *)
  postIDs :: "postID list"
  post :: "postID ⇒ post"
  owner :: "postID ⇒ userID"
  vis :: "postID ⇒ vis"
  (* The server-api IDs represents the apis whose posts can be read by this api. *)
  (* The following setting ensures that clashes on post IDs from different apis are harmless: *)
  (* Pending request sent by this API to other APIs with the wish that they become servers (and the current API
       becomes their client); this has to be approved by the respective APIs *)
  pendingSApiReqs :: "apiID list"
  sApiReq :: "apiID ⇒ requestInfo"
  serverApiIDs :: "apiID list"
  (* Password (key) to be used (by both parties) for communication with each server API. *)
  serverPass :: "apiID ⇒ password"
  outerPostIDs :: "apiID ⇒ postID list"
  outerPost :: "apiID ⇒ postID ⇒ post"
  outerOwner :: "apiID ⇒ postID ⇒ userID"
  outerVis :: "apiID ⇒ postID ⇒ vis"
  (*  *)
  (* The client-api IDs represents the apis that can read this api's posts *)
  (* Pending requests from APIs that want to become clients; this has to be approved by the admin *)
  pendingCApiReqs :: "apiID list"
  cApiReq :: "apiID ⇒ requestInfo"
  clientApiIDs :: "apiID list"
  (* Password (key) to be used (by both parties) for communication with each client API. *)
  clientPass :: "apiID ⇒ password"
  sharedWith :: "postID ⇒ (apiID × bool) list"
  (* for a post, stores the client apis with which the post was shared together with a boolean flag
     indicating whether the version the api has is up-to-date *)

(* The api IDs will be the URLs of the corresponding APIs *)
(* Note that only the client APIs need a password -- the server API are themselves contacted by this API. *)

(* Note that IDsOK refers only to the registered users, posts, server APIs and their served outerPosts,
and client apis. It does not refer to user IDs or api IDs contained in any pending requests.
*)
definition IDsOK :: "state ⇒ userID list ⇒ postID list ⇒ (apiID × postID list) list ⇒ apiID list ⇒ bool"
where
"IDsOK s uIDs pIDs saID_pIDs_s caIDs ≡
 list_all (λ uID. uID ∈∈ userIDs s) uIDs ∧
 list_all (λ pID. pID ∈∈ postIDs s) pIDs ∧
 list_all (λ (aID,pIDs). aID ∈∈ serverApiIDs s ∧
 list_all (λ pID. pID ∈∈ outerPostIDs s aID) pIDs) saID_pIDs_s ∧
 list_all (λ aID. aID ∈∈ clientApiIDs s) caIDs"


subsection ‹The actions›

subsubsection ‹Initialization of the system›


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

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

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

  sentOuterFriendIDs = (λ uID. []),
  recvOuterFriendIDs = (λ uID. []),

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

  pendingSApiReqs = [],
  sApiReq = (λ aID. emptyRequestInfo),
  serverApiIDs = [],
  serverPass = (λ aID. emptyPass),
  outerPostIDs = (λ aID. []),
  outerPost = (λ aID papID. emptyPost),
  outerOwner = (λ aID papID. emptyUserID),
  outerVis = (λ aID pID. FriendV),

  pendingCApiReqs = [],
  cApiReq = (λ aID. emptyRequestInfo),
  clientApiIDs = [],
  clientPass = (λ aID. emptyPass),
  sharedWith = (λpID. [])
 ⦈"


subsubsection ‹Starting action›

(* This initiates the current api. 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 ⇒ requestInfo ⇒ state"
where
"createNUReq s uID reqInfo ≡
 s ⦇pendingUReqs := pendingUReqs s @ [uID],
    userReq := (userReq s)(uID := reqInfo)
⦈"

definition e_createNUReq :: "state ⇒ userID ⇒ requestInfo ⇒ bool"
where
"e_createNUReq s uID requestInfo ≡
 admin s ∈∈ userIDs s ∧ ¬ uID ∈∈ userIDs s ∧ ¬ uID ∈∈ pendingUReqs s"
(* a new-user request can be created only if the api 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 := emptyRequestInfo)⦈"

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 API's interface will actually generate it, using getFresh. *)
definition createPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ state"
where
"createPost s uID p pID ≡
 s ⦇postIDs := pID # postIDs s,
    post := (post s) (pID := emptyPost),
    owner := (owner s) (pID := uID)⦈"
(* Recall from the initial state that the initial visibility is FriendV *)

definition e_createPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_createPost s uID p pID ≡
 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 ⇒ requestInfo ⇒ 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 ⇒ requestInfo ⇒ 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 emptyRequestInfo) uID uID' emptyRequestInfo⦈"

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 ‹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 ‹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"

definition updatePost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ post ⇒ state"
where
"updatePost s uID p pID pst ≡
 let sW = sharedWith s in
 s ⦇post := (post s) (pID := pst),
    sharedWith := sW (pID := map (λ (aID,_). (aID,False)) (sW pID))⦈"

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}"

(* Note: Of course, the outer posts cannot be updated from this API. *)


subsubsection ‹Reading actions›

(* Read new user request: *)
definition readNUReq :: "state ⇒ userID ⇒ password ⇒ userID ⇒ requestInfo"
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 so can all the other users), but not the password: *)
definition readUser :: "state ⇒ userID ⇒ password ⇒ userID ⇒ name"
where
"readUser s uID p uID' ≡ nameUser (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 ≡
 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 ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ 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 ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ owner s pID = uID ∨ uID ∈∈ friendIDs s (owner s pID) ∨ vis s pID = PublicV)"

(* Reading outer posts: *)

definition readOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ post"
where
"readOPost s uID p aID pID ≡ outerPost s aID pID"

definition e_readOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ bool"
where
"e_readOPost s uID p aID pID ≡
 IDsOK s [uID] [] [(aID,[pID])] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ (aID,outerOwner s aID pID) ∈∈ recvOuterFriendIDs s uID ∨ outerVis s aID pID = PublicV)"

definition readOwnerOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ userID"
where
"readOwnerOPost s uID p aID pID ≡ outerOwner s aID pID"

definition e_readOwnerOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ bool"
where
"e_readOwnerOPost s uID p aID pID ≡
 IDsOK s [uID] [] [(aID,[pID])] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ (aID,outerOwner s aID pID) ∈∈ recvOuterFriendIDs s uID ∨ outerVis s aID pID = PublicV)"

definition readVisOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ vis"
where
"readVisOPost s uID p aID pID ≡ outerVis s aID pID"

definition e_readVisOPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ bool"
where
"e_readVisOPost s uID p aID pID ≡
 let post = outerPost s aID pID in
 IDsOK s [uID] [] [(aID,[pID])] [] ∧ pass s uID = p ∧
 (admin s = uID ∨ (aID,outerOwner s aID pID) ∈∈ recvOuterFriendIDs s uID ∨
  outerVis s aID pID = PublicV)"



(* Friendship: *)
(* Read friendship request to me: *)
definition readFriendReqToMe :: "state ⇒ userID ⇒ password ⇒ userID ⇒ requestInfo"
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 ⇒ requestInfo"
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'"

(* Read request posted to a desired server api: *)
definition readSApiReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ requestInfo"
where
"readSApiReq s uID p uID' ≡ sApiReq s uID'"

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

(* Read request from possible client api: *)
definition readCApiReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ requestInfo"
where
"readCApiReq s uID p uID' ≡ cApiReq s uID'"

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


subsubsection ‹Listing actions›

(* list pending new user Reqs: *)
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 the outer friendship authorizations sent by a user: *)
definition listSentOuterFriends :: "state ⇒ userID ⇒ password ⇒ userID ⇒ (apiID × userID) list"
where
"listSentOuterFriends s uID p uID' ≡ sentOuterFriendIDs s uID'"

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

(* List the outer friendship authorizations received by a user: *)
definition listRecvOuterFriends :: "state ⇒ userID ⇒ password ⇒ (apiID × userID) list"
where
"listRecvOuterFriends s uID p ≡ recvOuterFriendIDs s uID"

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

(* list posts internal to the api: *)
definition listInnerPosts :: "state ⇒ userID ⇒ password ⇒ (userID × postID) list"
where
"listInnerPosts s uID p ≡
  [(owner s pID, pID).
    pID ← postIDs s,
    vis s pID ≠ FriendV ∨ uID ∈∈ friendIDs s (owner s pID) ∨ uID = owner s pID
  ]"

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

(* list posts from other apis: *)
definition listOuterPosts :: "state ⇒ userID ⇒ password ⇒ (apiID × postID) list"
where
"listOuterPosts s uID p ≡
  [(saID, pID).
    saID ← serverApiIDs s,
    pID ← outerPostIDs s saID,
    outerVis s saID pID = PublicV ∨ (saID, outerOwner s saID pID) ∈∈ recvOuterFriendIDs s uID
  ]"

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

(* List all the api clients who have already received this post: *)
definition listClientsPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ (apiID × bool) list"
where
"listClientsPost s uID p pID ≡ sharedWith s pID"

(* Only the admin can see these: *)
definition e_listClientsPost :: "state ⇒ userID ⇒ password ⇒ postID ⇒ bool"
where
"e_listClientsPost s uID p pID ≡
 IDsOK s [uID] [pID] [] [] ∧ pass s uID = p ∧ uID = admin s"


(* list the pending Reqs from the current API to other APIs for them to become servers:  *)
definition listPendingSApiReqs :: "state ⇒ userID ⇒ password ⇒ apiID list"
where
"listPendingSApiReqs s uID p ≡ pendingSApiReqs s"

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

(* list the IDs of the server apis: *)
definition listServerAPIs :: "state ⇒ userID ⇒ password ⇒ apiID list"
where
"listServerAPIs s uID p ≡ serverApiIDs s"

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


(* list the pending Reqs from APIs that want to become clients of the current API:  *)
definition listPendingCApiReqs :: "state ⇒ userID ⇒ password ⇒ apiID list"
where
"listPendingCApiReqs s uID p ≡ pendingCApiReqs s"

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

(* list the IDs of the client apis: *)
definition listClientAPIs :: "state ⇒ userID ⇒ password ⇒ apiID list"
where
"listClientAPIs s uID p ≡ clientApiIDs s"

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


subsubsection ‹Actions of communication with other APIs›

(* Note: Some of the communication actions are special in the following sense:
The initiator (the api's admin or, in the case of create outer friend, an arbitrary user, uID)
is different from the observer (another api, aID).  *)

(* The next 4 actions implement the protocol of connecting a server and a client:
-- It starts with the synchronized sendServerReq (with potential client as sender) and
  receiveClientReq (with potential server as receiver)
-- It finishes with the synchronized connectClient (with potential server as sender) and
 connectServer (with potential client as receiver)
 *)


(* Send request to potential server.
 sendServerReq s uID p aID reqInfo does the following: User uID (the admin)
send request to api aID wishing to subscribe to this server;
 In the implementation, the request info along with the URL of the current api (i.e., this api's ID)
 will be sent to the given api aID. *)
definition sendServerReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ requestInfo ⇒ (apiID × requestInfo) × state"
where
"sendServerReq s uID p aID reqInfo ≡
 ((aID,reqInfo),
  s ⦇pendingSApiReqs := pendingSApiReqs s @ [aID],
     sApiReq := (sApiReq s) (aID := reqInfo)⦈)"

definition e_sendServerReq :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ requestInfo ⇒ bool"
where
"e_sendServerReq s uID p aID reqInfo ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧
 uID = admin s ∧ ¬ aID ∈∈ pendingSApiReqs s"

(* Receive request from potential client.
receiveClientReq s aID reqInfo does the following: receives registration request from
potential client api aID (which is a URL) with request info reqInfo. This action is
not trigered from any user of the current API -- it is an even coming from outside.
*)

definition receiveClientReq :: "state ⇒ apiID ⇒ requestInfo ⇒ state"
where
"receiveClientReq s aID reqInfo ≡
 s ⦇pendingCApiReqs := pendingCApiReqs s @ [aID],
    cApiReq := (cApiReq s) (aID := reqInfo)⦈"

definition e_receiveClientReq :: "state ⇒ apiID ⇒ requestInfo ⇒ bool"
where
"e_receiveClientReq s aID reqInfo ≡
 ¬ aID ∈∈ pendingCApiReqs s ∧ admin s ∈∈ userIDs s"

(* Connect a client that had made a registration request.
connectClient s uID p aID cp does the following: The user uID (the admin)
picks up an api id aID from the list of pending requests and registers it as a client.
At the same time, it issues a password cp for the client, stores it and sends it to aID.
*)

definition connectClient :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ password ⇒ (apiID × password) × state"
where
"connectClient s uID p aID cp ≡
 ((aID, cp),
  s ⦇clientApiIDs := (aID # clientApiIDs s),
     clientPass := (clientPass s) (aID := cp),
     pendingCApiReqs := remove1 aID (pendingCApiReqs s),
     cApiReq := (cApiReq s)(aID := emptyRequestInfo)⦈
 )"

definition e_connectClient :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ password ⇒ bool"
where
"e_connectClient s uID p aID cp ≡
 IDsOK s [uID] [] [] [] ∧ pass s uID = p ∧
 uID = admin s ∧
 aID ∈∈ pendingCApiReqs s ∧ ¬ aID ∈∈ clientApiIDs s"

(* Connect server api
connectServer s aID sp does the following: receives the password sp issued
by the potential server aID and stores it. It will be used for communicating with that server.
Of course, this action only succeeds if a request to aID had really been posted (which was
recorded in pendingSApiReqs).
*)
definition connectServer :: "state ⇒ apiID ⇒ password ⇒ state"
where
"connectServer s aID sp ≡
 s ⦇serverApiIDs := (aID # serverApiIDs s),
    serverPass := (serverPass s) (aID := sp),
    pendingSApiReqs := remove1 aID (pendingSApiReqs s),
    sApiReq := (sApiReq s)(aID := emptyRequestInfo)⦈"

definition e_connectServer :: "state ⇒ apiID ⇒ password ⇒ bool"
where
"e_connectServer s aID sp ≡
 aID ∈∈ pendingSApiReqs s ∧ ¬ aID ∈∈ serverApiIDs s"

(* The next 2 actions represent server-client communication (always from server to client):
-- The server sends a post via sendPost
-- The client receives it via receivePost
Note that, since only the server sends messages to the client, it is the server who authenticates itself.
 *)

(* Send a post and its owner's ID (as well as the server credentials for communicating with that
client) to a client api. Also, recall that the post has now been shared with that client.  *)
definition sendPost ::
"state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ (apiID × password × postID × post × userID × vis) × state"
where
"sendPost s uID p aID pID ≡
 ((aID, clientPass s aID, pID, post s pID, owner s pID, vis s pID),
  s⦇sharedWith := (sharedWith s) (pID := insert2 aID True (sharedWith s pID))⦈)"

definition e_sendPost :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ postID ⇒ bool"
where
"e_sendPost s uID p aID pID ≡
 IDsOK s [uID] [pID] [] [aID] ∧ pass s uID = p ∧
 uID = admin s ∧ aID ∈∈ clientApiIDs s"

(* Receive a post and its owner's ID (as well as the server credentials) from a server api. *)
definition receivePost :: "state ⇒ apiID ⇒ password ⇒ postID ⇒ post ⇒ userID ⇒ vis ⇒ state"
where
"receivePost s aID sp pID pst uID vs ≡
 let opIDs = outerPostIDs s in
 s ⦇outerPostIDs := opIDs (aID :=  List.insert pID (opIDs aID)),
    outerPost := fun_upd2 (outerPost s) aID pID pst,
    outerOwner := fun_upd2 (outerOwner s) aID pID uID,
    outerVis := fun_upd2 (outerVis s) aID pID vs⦈"

definition e_receivePost :: "state ⇒ apiID ⇒ password ⇒ postID ⇒ post ⇒ userID ⇒ vis ⇒ bool"
where
"e_receivePost s aID sp pID nt uID vs ≡
 IDsOK s [] [] [(aID,[])] [] ∧ serverPass s aID = sp"


(* Create outer friend; unlike inner friendship, outer friendship is not necessarily symmetric.
It is always established from a user of a server to a user of a client, the former giving
unilateral access to the latter at his friend-only posts. These unilateral friendship permissions
are stored on the client.*)

(* sendCreateOFriend s uID p aID uID' means: User uID (of current api), with password p,
  sends an I-set-you-as-my-friend note to the presumptive user uID' on client api aID.
  The request uses the server credentials for the given client, as customary. *)
definition sendCreateOFriend ::
  "state ⇒ userID ⇒ password ⇒ apiID ⇒ userID ⇒ (apiID × password × userID × userID) × state"
where
"sendCreateOFriend s uID p aID uID' ≡
 let ofr = sentOuterFriendIDs s in
 ((aID, clientPass s aID, uID, uID'),
  s ⦇sentOuterFriendIDs := ofr (uID := ofr uID @ [(aID,uID')])⦈)"

(* Note that the server (who issues the note) cannot check if uID' is a valid user on the client.
This will be checked on the client api only.*)
definition e_sendCreateOFriend :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ userID ⇒ bool"
where
"e_sendCreateOFriend s uID p caID uID' ≡
 IDsOK s [uID] [] [] [caID] ∧ pass s uID = p ∧
 ¬ (caID,uID') ∈∈ sentOuterFriendIDs s uID"

(* receiveCreateOFriend s sp saID uID uID' means: The current api receives, from
 one of its registered server apis aAID with password sp, an I-set-you-as-my-friend
 note from aAID's presumptive user uID to the current api's user uID'. The effect
 is that the current api will mark (saID,uID) in the list of outer friends of uID'
 (hence will allow uID' access to friend-only outer posts from uID). *)

definition receiveCreateOFriend :: "state ⇒ apiID ⇒ password ⇒ userID ⇒ userID ⇒ state"
where
"receiveCreateOFriend s saID sp uID uID' ≡
 let ofr = recvOuterFriendIDs s in
 s ⦇recvOuterFriendIDs := ofr (uID' := ofr uID' @ [(saID,uID)])⦈"

definition e_receiveCreateOFriend :: "state ⇒ apiID ⇒ password ⇒ userID ⇒ userID ⇒ bool"
where
"e_receiveCreateOFriend s saID sp uID uID' ≡
 IDsOK s [] [] [(saID,[])] [] ∧ serverPass s saID = sp ∧
 ¬ (saID,uID) ∈∈ recvOuterFriendIDs s uID'"


(* Deletion of outer friends *)

definition sendDeleteOFriend ::
  "state ⇒ userID ⇒ password ⇒ apiID ⇒ userID ⇒ (apiID × password × userID × userID) × state"
where
"sendDeleteOFriend s uID p aID uID' ≡
 let ofr = sentOuterFriendIDs s in
 ((aID, clientPass s aID, uID, uID'),
  s ⦇sentOuterFriendIDs := ofr (uID := remove1 (aID,uID') (ofr uID))⦈)"

definition e_sendDeleteOFriend :: "state ⇒ userID ⇒ password ⇒ apiID ⇒ userID ⇒ bool"
where
"e_sendDeleteOFriend s uID p caID uID' ≡
 IDsOK s [uID] [] [] [caID] ∧ pass s uID = p ∧
 (caID,uID') ∈∈ sentOuterFriendIDs s uID"

definition receiveDeleteOFriend :: "state ⇒ apiID ⇒ password ⇒ userID ⇒ userID ⇒ state"
where
"receiveDeleteOFriend s saID sp uID uID' ≡
 let ofr = recvOuterFriendIDs s in
 s ⦇recvOuterFriendIDs := ofr (uID' := remove1 (saID,uID) (ofr uID'))⦈"

definition e_receiveDeleteOFriend :: "state ⇒ apiID ⇒ password ⇒ userID ⇒ userID ⇒ bool"
where
"e_receiveDeleteOFriend s saID sp uID uID' ≡
 IDsOK s [] [] [(saID,[])] [] ∧ serverPass s saID = sp ∧
 (saID,uID) ∈∈ recvOuterFriendIDs s uID'"




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| outName name |
  outPost post | outVis vis |
  outReq requestInfo |
  (* Outputs for listing actions: *)
  outUID "userID" | outUIDL "userID list" |
  outAIDL "apiID list"  |  outAIDBL "(apiID × bool) list"  |
  outUIDPIDL "(userID × postID)list" | outAIDPIDL "(apiID × postID)list" |
  outAIDUIDL "(apiID × userID) list" |
  (* Outputs specific to communication actions: *)
  O_sendServerReq "apiID × requestInfo" | O_connectClient "apiID × password" |
  O_sendPost "apiID × password × postID × post × userID × vis" |
  O_sendCreateOFriend "apiID × password × userID × userID" |
  O_sendDeleteOFriend "apiID × password × userID × userID"


(* The content from outAIDPIDTT outputs: *)
fun from_O_sendPost where
 "from_O_sendPost (O_sendPost antt) = antt"
|"from_O_sendPost _ = undefined"


(* 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 requestInfo
 |cUser userID password userID password
 |cPost userID password postID
 |cFriendReq userID password userID requestInfo
 |cFriend userID password userID

lemmas c_defs =
e_createNUReq_def createNUReq_def
e_createUser_def createUser_def
e_createPost_def createPost_def
e_createFriendReq_def createFriendReq_def
e_createFriend_def createFriend_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 (cPost uID p pID) =
 (if e_createPost s uID p pID
    then (outOK, createPost s uID p pID)
    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))"

fun cUserOfA :: "cActt ⇒ userID" where
 "cUserOfA (cNUReq uID req) = uID"
|"cUserOfA (cUser uID p uID' p') = uID"
|"cUserOfA (cPost uID p pID) = uID"
|"cUserOfA (cFriendReq uID p uID' req) = uID"
|"cUserOfA (cFriend uID p uID') = 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 =
  isuUser: uUser userID password password name inform
 |isuPost: uPost userID password postID post
 |isuVisPost: 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

 |rOwnerPost userID password postID
 |rVisPost userID password postID

 |rOPost userID password apiID postID

 |rOwnerOPost userID password apiID postID
 |rVisOPost userID password apiID postID

 |rFriendReqToMe userID password userID
 |rFriendReqFromMe userID password userID
 |rSApiReq userID password apiID
 |rCApiReq userID password apiID

lemmas r_defs =
 readNUReq_def e_readNUReq_def
 readUser_def e_readUser_def
 readAmIAdmin_def e_readAmIAdmin_def

 readPost_def e_readPost_def

 readOwnerPost_def e_readOwnerPost_def
 readVisPost_def e_readVisPost_def

 readOPost_def e_readOPost_def

 readOwnerOPost_def e_readOwnerOPost_def
 readVisOPost_def e_readVisOPost_def

 readFriendReqToMe_def e_readFriendReqToMe_def
 readFriendReqFromMe_def e_readFriendReqFromMe_def
 readSApiReq_def e_readSApiReq_def
 readCApiReq_def e_readCApiReq_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 outName (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 (rOwnerPost uID p pID) =
 (if e_readOwnerPost s uID p pID then outUID (readOwnerPost 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 (rOPost uID p aID pID) =
 (if e_readOPost s uID p aID pID then outPost (readOPost s uID p aID pID) else outErr)"
|
"rObs s (rOwnerOPost uID p aID pID) =
 (if e_readOwnerOPost s uID p aID pID then outUID (readOwnerOPost s uID p aID pID) else outErr)"
|
"rObs s (rVisOPost uID p aID pID) =
 (if e_readVisOPost s uID p aID pID then outVis (readVisOPost s uID p aID 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)"
|
"rObs s (rSApiReq uID p aID) =
 (if e_readSApiReq s uID p aID then outReq (readSApiReq s uID p aID) else outErr)"
|
"rObs s (rCApiReq uID p aID) =
 (if e_readCApiReq s uID p aID then outReq (readCApiReq s uID p aID) else outErr)"


fun rUserOfA :: "rActt ⇒ userID" where
 "rUserOfA (rNUReq uID p uID') = uID"
|"rUserOfA (rUser uID p uID') = uID"
|"rUserOfA (rAmIAdmin uID p) = uID"

|"rUserOfA (rPost uID p pID) = uID"
|"rUserOfA (rOwnerPost uID p pID) = uID"
|"rUserOfA (rVisPost uID p pID) = uID"

|"rUserOfA (rOPost uID p aID pID) = uID"
|"rUserOfA (rOwnerOPost uID p aID pID) = uID"
|"rUserOfA (rVisOPost uID p aID pID) = uID"

|"rUserOfA (rFriendReqToMe uID p uID') = uID"
|"rUserOfA (rFriendReqFromMe uID p uID') = uID"
|"rUserOfA (rSApiReq uID p aID) = uID"
|"rUserOfA (rCApiReq uID p aID) = uID"


(* Listing actions *)
datatype lActt =
  lPendingUReqs userID password
 |lAllUsers userID password
 |lFriends userID password userID
 |lSentOuterFriends userID password userID
 |lRecvOuterFriends userID password
 |lInnerPosts userID password
 |lOuterPosts userID password
 |lClientsPost userID password postID
 |lPendingSApiReqs userID password
 |lServerAPIs userID password
 |lPendingCApiReqs userID password
 |lClientAPIs userID password

lemmas l_defs =
 listPendingUReqs_def e_listPendingUReqs_def
 listAllUsers_def e_listAllUsers_def
 listFriends_def e_listFriends_def
 listSentOuterFriends_def e_listSentOuterFriends_def
 listRecvOuterFriends_def e_listRecvOuterFriends_def
 listInnerPosts_def e_listInnerPosts_def
 listOuterPosts_def e_listOuterPosts_def
 listClientsPost_def e_listClientsPost_def
 listPendingSApiReqs_def e_listPendingSApiReqs_def
 listServerAPIs_def e_listServerAPIs_def
 listPendingCApiReqs_def e_listPendingCApiReqs_def
 listClientAPIs_def e_listClientAPIs_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 (lSentOuterFriends uID p uID') =
 (if e_listSentOuterFriends s uID p uID' then outAIDUIDL (listSentOuterFriends s uID p uID') else outErr)"
|
"lObs s (lRecvOuterFriends uID p) =
 (if e_listRecvOuterFriends s uID p then outAIDUIDL (listRecvOuterFriends s uID p) else outErr)"
|
"lObs s (lInnerPosts uID p) =
 (if e_listInnerPosts s uID p then outUIDPIDL (listInnerPosts s uID p) else outErr)"
|
"lObs s (lOuterPosts uID p) =
 (if e_listOuterPosts s uID p then outAIDPIDL (listOuterPosts s uID p) else outErr)"
|
"lObs s (lClientsPost uID p pID) =
 (if e_listClientsPost s uID p pID then outAIDBL (listClientsPost s uID p pID) else outErr)"
|
"lObs s (lPendingSApiReqs uID p) =
 (if e_listPendingSApiReqs s uID p then outAIDL (listPendingSApiReqs s uID p) else outErr)"
|
"lObs s (lServerAPIs uID p) =
 (if e_listServerAPIs s uID p then outAIDL (listServerAPIs s uID p) else outErr)"
|
"lObs s (lClientAPIs uID p) =
 (if e_listClientAPIs s uID p then outAIDL (listClientAPIs s uID p) else outErr)"
|
"lObs s (lPendingCApiReqs uID p) =
 (if e_listPendingCApiReqs s uID p then outAIDL (listPendingCApiReqs s uID p) else outErr)"

fun lUserOfA :: "lActt ⇒ userID" where
 "lUserOfA (lPendingUReqs uID p) = uID"
|"lUserOfA (lAllUsers uID p) = uID"
|"lUserOfA (lFriends uID p uID') = uID"
|"lUserOfA (lSentOuterFriends uID p uID') = uID"
|"lUserOfA (lRecvOuterFriends uID p) = uID"
|"lUserOfA (lInnerPosts uID p) = uID"
|"lUserOfA (lOuterPosts uID p) = uID"
|"lUserOfA (lClientsPost uID p pID) = uID"
|"lUserOfA (lPendingSApiReqs uID p) = uID"
|"lUserOfA (lServerAPIs uID p) = uID"
|"lUserOfA (lClientAPIs uID p) = uID"
|"lUserOfA (lPendingCApiReqs uID p) = uID"


(* Communication actions *)

datatype comActt =
  comSendServerReq userID password apiID requestInfo
 |comReceiveClientReq apiID requestInfo
 |comConnectClient userID password apiID password
 |comConnectServer apiID password
 |comReceivePost apiID password postID post userID vis
 |comSendPost userID password apiID postID
 |comReceiveCreateOFriend apiID password userID userID
 |comSendCreateOFriend userID password apiID userID
 |comReceiveDeleteOFriend apiID password userID userID
 |comSendDeleteOFriend userID password apiID userID

lemmas com_defs =
 sendServerReq_def e_sendServerReq_def
 receiveClientReq_def e_receiveClientReq_def
 connectClient_def e_connectClient_def
 connectServer_def e_connectServer_def
 receivePost_def e_receivePost_def
 sendPost_def e_sendPost_def
 receiveCreateOFriend_def e_receiveCreateOFriend_def
 sendCreateOFriend_def e_sendCreateOFriend_def
 receiveDeleteOFriend_def e_receiveDeleteOFriend_def
 sendDeleteOFriend_def e_sendDeleteOFriend_def

fun comStep :: "state ⇒ comActt ⇒ out × state" where
"comStep s (comSendServerReq uID p aID reqInfo) =
 (if e_sendServerReq s uID p aID reqInfo
    then let (x,s) = sendServerReq s uID p aID reqInfo in (O_sendServerReq x, s)
    else (outErr, s))"
|
"comStep s (comReceiveClientReq aID reqInfo) =
 (if e_receiveClientReq s aID reqInfo then (outOK, receiveClientReq s aID reqInfo) else (outErr, s))"
|
"comStep s (comConnectClient uID p aID cp) =
 (if e_connectClient s uID p aID cp
    then let (aID_cp,s) = connectClient s uID p aID cp in (O_connectClient aID_cp, s)
    else (outErr, s))"
|
"comStep s (comConnectServer aID sp) =
 (if e_connectServer s aID sp then (outOK, connectServer s aID sp) else (outErr, s))"
|
"comStep s (comReceivePost aID sp pID nt uID vs) =
 (if e_receivePost s aID sp pID nt uID vs
    then (outOK, receivePost s aID sp pID nt uID vs)
    else (outErr, s))"
|
"comStep s (comSendPost uID p aID pID) =
 (if e_sendPost s uID p aID pID
    then let (x,s) = sendPost s uID p aID pID in (O_sendPost x, s)
    else (outErr, s))"
|
"comStep s (comReceiveCreateOFriend aID cp uID uID') =
 (if e_receiveCreateOFriend s aID cp uID uID'
    then (outOK, receiveCreateOFriend s aID cp uID uID')
    else (outErr, s))"
|
"comStep s (comSendCreateOFriend uID p aID uID') =
 (if e_sendCreateOFriend s uID p aID uID'
    then let (apuu,s) = sendCreateOFriend s uID p aID uID' in (O_sendCreateOFriend apuu, s)
    else (outErr, s))"
|
"comStep s (comReceiveDeleteOFriend aID cp uID uID') =
 (if e_receiveDeleteOFriend s aID cp uID uID'
    then (outOK, receiveDeleteOFriend s aID cp uID uID')
    else (outErr, s))"
|
"comStep s (comSendDeleteOFriend uID p aID uID') =
 (if e_sendDeleteOFriend s uID p aID uID'
    then let (apuu,s) = sendDeleteOFriend s uID p aID uID' in (O_sendDeleteOFriend apuu, s)
    else (outErr, s))"


fun comUserOfA :: "comActt ⇒ userID option" where
 "comUserOfA (comSendServerReq uID p aID reqInfo) = Some uID"
|"comUserOfA (comReceiveClientReq aID reqInfo) = None"
|"comUserOfA (comConnectClient uID p aID sp) = Some uID"
|"comUserOfA (comConnectServer aID sp) = None"
|"comUserOfA (comReceivePost aID sp pID nt uID vs) = None"
|"comUserOfA (comSendPost uID p aID pID) = Some uID"
|"comUserOfA (comReceiveCreateOFriend aID cp uID uID') = None"
|"comUserOfA (comSendCreateOFriend uID p aID uID') = Some uID"
|"comUserOfA (comReceiveDeleteOFriend aID cp uID uID') = None"
|"comUserOfA (comSendDeleteOFriend uID p aID uID') = Some uID"

fun comApiOfA :: "comActt ⇒ apiID" where
 "comApiOfA (comSendServerReq uID p aID reqInfo) = aID"
|"comApiOfA (comReceiveClientReq aID reqInfo) = aID"
|"comApiOfA (comConnectClient uID p aID sp) = aID"
|"comApiOfA (comConnectServer aID sp) = aID"
|"comApiOfA (comReceivePost aID sp pID nt uID vs) = aID"
|"comApiOfA (comSendPost uID p aID pID) = aID"
|"comApiOfA (comReceiveCreateOFriend aID cp uID uID') = aID"
|"comApiOfA (comSendCreateOFriend uID p aID uID') = aID"
|"comApiOfA (comReceiveDeleteOFriend aID cp uID uID') = aID"
|"comApiOfA (comSendDeleteOFriend uID p aID uID') = aID"


(* All actions: *)
datatype act =
  isSact: Sact sActt |
(* 3 kinds of effects: creation, deletion and update *)
  isCact: Cact cActt | isDact: Dact dActt | isUact: Uact uActt |
(* 2 kinds of observations: reading and listing (the latter mainly printing IDs) *)
  isRact: Ract rActt | isLact: Lact lActt |
(* Communications, which can themselves be either effects or ovbservations: *)
  isCOMact: COMact comActt

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)"
|
"step s (COMact ca) = comStep s ca"

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


interpretation IO_Automaton where
istate = istate and step = step
done


subsection ‹Code generation›

export_code step istate getFreshPostID in Scala

end